CoqToLeanAsm: x86 Macro Assembler in Lean 4

12.3. Register Operations

Clear registers using XOR (standard idiom):

def clearRegs : Program := x86! {
  xor eax, eax
  xor ebx, ebx
}

Arithmetic operations:

def arithmetic : Program := x86! {
  mov eax, (imm 42)   -- Load immediate
  add eax, ebx        -- EAX += EBX
  sub eax, ecx        -- EAX -= ECX
  shl eax, (imm 2)    -- EAX *= 4
}