Sequence Example: Proving by Sequential Composition #

This is a line-by-line port of s2n-bignum/arm/tutorial/sequence.ml.

The key technique demonstrated is compositional verification: instead of symbolically executing all instructions at once, we split the program into sequential chunks with intermediate assertions.

The Program #

0:   8b000021        add     x1, x1, x0
4:   8b000042        add     x2, x2, x0
8:   d2800043        mov     x3, #0x2
c:   9b037c21        mul     x1, x1, x3

The Approach #

Split at pc+8 into two chunks:
- First chunk (pc to pc+8): two add instructions
- Second chunk (pc+8 to pc+16): mov and mul
Intermediate assertion at pc+8: X1 = a + b
Prove each chunk independently and compose the proofs.

Memory-Based Model #

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 sequence program machine code (16 bytes = 4 instructions).

ARM is little-endian, so:

Bytes [0x21, 0x00, 0x00, 0x8b] encode instruction 0x8b000021 = ADD X1, X1, X0
Bytes [0x42, 0x00, 0x00, 0x8b] encode instruction 0x8b000042 = ADD X2, X2, X0
Bytes [0x43, 0x00, 0x80, 0xd2] encode instruction 0xd2800043 = MOV X3, #2
Bytes [0x21, 0x7c, 0x03, 0x9b] encode instruction 0x9b037c21 = MUL X1, X1, X3

source

def Bignum.Arm.Tutorial.sequence_mc :

List UInt8

Equations

Bignum.Arm.Tutorial.sequence_mc = [33, 0, 0, 139, 66, 0, 0, 139, 67, 0, 128, 210, 33, 124, 3, 155]

Instances For

Specification #

The specification follows HOL Light's ensures arm style:

ensures arm
  (\s. aligned_bytes_loaded s (word pc) sequence_mc /\
       read PC s = word pc /\
       read X0 s = word a /\
       read X1 s = word b /\
       read X2 s = word c)
  (\s. read PC s = word (pc+16) /\
       read X1 s = word ((a + b) * 2))
  (MAYCHANGE [PC;X1;X2;X3])

source

def Bignum.Arm.Tutorial.sequence_pre (pc a b c : ℕ) (s : ArmState) :

Prop

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

Equations

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

Instances For

source

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

Prop

Intermediate assertion at pc+8: X1 = a + b.

This is the \s. read X1 s = word (a + b) from HOL Light's ENSURES_SEQUENCE_TAC.

Source: s2n-bignum/arm/tutorial/sequence.ml:77

Equations

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

Instances For

source

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

Prop

Postcondition: PC at pc+16, X1 = (a+b)*2.

Equations

Bignum.Arm.Tutorial.sequence_post pc a b s = (s.read_reg Bignum.Arm.Reg.PC = Bignum.Word64.ofNat (pc + 16) ∧ s.read_reg Bignum.Arm.Reg.X1 = Bignum.Word64.ofNat ((a + b) * 2))

Instances For

Symbolic Execution Helpers #

Decode lemmas for each instruction in the sequence program.

source

theorem Bignum.Arm.Tutorial.sequence_decode_instr1 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc sequence_mc) :

arm_decode s pc = some (Instruction.ADD Reg.X1 Reg.X1 Reg.X0)

Decode instruction 1: ADD X1, X1, X0

source

theorem Bignum.Arm.Tutorial.sequence_decode_instr2 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc sequence_mc) :

arm_decode s (pc + 4) = some (Instruction.ADD Reg.X2 Reg.X2 Reg.X0)

Decode instruction 2: ADD X2, X2, X0

source

theorem Bignum.Arm.Tutorial.sequence_decode_instr3 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc sequence_mc) :

arm_decode s (pc + 8) = some (Instruction.MOVZ Reg.X3 2 0)

Decode instruction 3: MOV X3, #2 (encoded as MOVZ)

source

theorem Bignum.Arm.Tutorial.sequence_decode_instr4 (s : ArmState) (pc : Word64) (h : aligned_bytes_loaded s.mem pc sequence_mc) :

arm_decode s (pc + 12) = some (Instruction.MUL Reg.X1 Reg.X1 Reg.X3)

Decode instruction 4: MUL X1, X1, X3

Compositional Verification #

The key insight from sequence.ml is that we can split a program into sequential chunks and prove each separately. This corresponds to HOL Light's ENSURES_SEQUENCE_TAC.

Given:

ensures arm pre mid frame1 (for first chunk)
ensures arm mid post frame2 (for second chunk)

We can derive:

ensures arm pre post (frame1 ∪ frame2) (for whole program)

source

theorem Bignum.Arm.Tutorial.ensures_sequence {α : Sort u_1} {step : α → α → Prop} (pre mid post : α → Prop) (frame : α → α → Prop) (h1 : ensures step pre mid frame) (h2 : ensures step mid post frame) (h_frame_trans : ∀ (s1 s2 s3 : α), frame s1 s2 → frame s2 s3 → frame s1 s3) :

ensures step pre post frame

Sequential composition of ensures: if we can prove ensures for two sequential chunks, we can derive ensures for the whole program.

This corresponds to HOL Light's ENSURES_SEQUENCE_TAC.

source