6.2. Byte Registers

The 8-bit registers defined by ByteReg access low/high bytes of AX, BX, CX, DX:

X86.AL : ByteReg#check AL   -- Low byte of EAX
X86.CL : ByteReg#check CL   -- Low byte of ECX (used for shift counts)

-- High bytes (bits 8-15)
X86.AH : ByteReg#check AH   -- High byte of EAX
X86.CH : ByteReg#check CH   -- High byte of ECX

Use ByteReg.toReg to get the parent 32-bit register:

X86.Reg.nonSPReg (X86.NonSPReg.EAX)#eval AL.toReg  -- EAX