Simple Example: Proving a Simple ARM Program

This is a line-by-line port of s2n-bignum/arm/tutorial/simple.ml with detailed correspondence documented. The program consists of two instructions:

0:   8b000022        add     x2, x1, x0
4:   cb010042        sub     x2, x2, x1

We prove that starting with X0 = a and X1 = b, after executing both instructions, we have X2 = a (the additions and subtractions cancel out).

Following HOL Light's architecture, programs are stored as bytes in memory. The arm step relation fetches, decodes, and executes instructions from memory.

Machine Code

The simple program as a byte sequence (machine code).

ARM is little-endian, so:

• Bytes [0x22, 0x00, 0x00, 0x8b] encode instruction 0x8b000022 = ADD X2, X1, X0
• Bytes [0x42, 0x00, 0x01, 0xcb] encode instruction 0xcb010042 = SUB X2, X2, X1

def Bignum.Arm.Tutorial.simple_mc : List UInt8

The simple program machine code (8 bytes = 2 instructions).

Equations

• Bignum.Arm.Tutorial.simple_mc = [34, 0, 0, 139, 66, 0, 1, 203]

Specification

The specification follows HOL Light's ensures arm style:

ensures arm
  (\s. aligned_bytes_loaded s (word pc) simple_mc /\
       read PC s = word pc /\
       read X0 s = word a /\
       read X1 s = word b)
  (\s. read PC s = word (pc+8) /\
       read X2 s = word a)
  (MAYCHANGE [PC;X2])

Source: s2n-bignum/arm/tutorial/simple.ml:65-84

def Bignum.Arm.Tutorial.simple_pre (pc a b : ℕ) (s : ArmState) : Prop

Precondition: program loaded, PC at start, registers initialized.

Equations

• One or more equations did not get rendered due to their size.

def Bignum.Arm.Tutorial.simple_post (pc a : ℕ) (s : ArmState) : Prop

Postcondition: PC advanced, X2 contains a.

Equations

• Bignum.Arm.Tutorial.simple_post pc a s = (s.read_reg Bignum.Arm.Reg.PC = Bignum.Word64.ofNat (pc + 8) ∧ s.read_reg Bignum.Arm.Reg.X2 = Bignum.Word64.ofNat a)

Symbolic Execution Helpers

To prove correctness, we need to show that when bytes are loaded in memory, arm_decode succeeds and returns the expected instruction.

theorem Bignum.Arm.Tutorial.simple_decode_instr1 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc simple_mc) : arm_decode s pc = some (Instruction.ADD Reg.X2 Reg.X1 Reg.X0)

Decode the first instruction (ADD X2, X1, X0) from loaded bytes.

The proof connects aligned_bytes_loaded (which gives us byte values at each offset) to arm_decode (which reads 4 bytes and decodes them).

This corresponds to HOL Light's ARM_MK_EXEC_RULE which pre-computes decode results. In Lean, we prove it as a theorem using the concrete byte values.

theorem Bignum.Arm.Tutorial.simple_decode_instr2 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc simple_mc) : arm_decode s (pc + 4) = some (Instruction.SUB Reg.X2 Reg.X2 Reg.X1)

Decode the second instruction (SUB X2, X2, X1) from loaded bytes.

Main Correctness Theorem

The proof follows HOL Light's structure:

1. ENSURES_INIT_TAC - establish initial state
2. ARM_STEPS_TAC (1--2) - symbolic execution of instructions
3. ENSURES_FINAL_STATE_TAC - verify postcondition
4. WORD_RULE - discharge word arithmetic

The key insight:

1. After instruction 1 (ADD): X2 = word(a + b)
2. After instruction 2 (SUB): X2 = word((a + b) - b) = word(a)

theorem Bignum.Arm.Tutorial.simple_correct (pc a b : ℕ) : ensures arm (simple_pre pc a b) (simple_post pc a) (maychange_regs [Reg.PC, Reg.X2])

Main correctness theorem: the simple program satisfies its specification. This corresponds to HOL Light's SIMPLE_SPEC theorem.