15.3. Comparison with NASM

Our assembler produces identical output to NASM. Given this NASM source:

; NASM assembly
section .text
global _start
_start:
    xor eax, eax      ; 31 C0
    mov ebx, 42       ; BB 2A 00 00 00
    add eax, ebx      ; 01 D8
    ret               ; C3

Our Lean code produces the same bytes:

def nasmExample : List Instr := [
  .BOP .Op32 .XOR (.RR EAX EAX),
  .MOVOP .Op32 (.RI EBX 42),
  .BOP .Op32 .ADD (.RR EAX EBX),
  .RETOP 0
]