CoqToLeanAsm: x86 Macro Assembler in Lean 4

14.2. Operand Size Consistency

The OpSize type ensures operand sizes are consistent across an instruction. You cannot mix 8-bit and 32-bit operands:

Instr.BOP OpSize.Op32 BinOp.ADD (DstSrc.RR EAX EBX) : Instr#check Instr.BOP OpSize.Op32 BinOp.ADD (DstSrc.RR EAX EBX) -- Valid: 8-bit operation with 8-bit registers Instr.BOP OpSize.Op8 BinOp.ADD (DstSrc.RR AL BL) : Instr#check Instr.BOP OpSize.Op8 BinOp.ADD (DstSrc.RR AL BL)

The VReg and VWord type families enforce this:

VReg OpSize.Op32 : Type#check (VReg OpSize.Op32) -- = Reg (32-bit registers like EAX) VReg OpSize.Op8 : Type#check (VReg OpSize.Op8) -- = ByteReg (8-bit registers like AL)