Specification Framework for ARM Verification

This file defines the specification framework for verifying ARM programs, following the relational Hoare logic approach from s2n-bignum.

The framework is organized following the article "Relational Hoare Logic for Realistically Modelled Machine Code" (CAV 2025):

Unary Hoare Logic L₁

• eventually step P s - Reachability predicate (operational semantics)
• ensures step pre post frame - Hoare triple with frame condition

Relational Logic L₂ (for future extension)

• eventuallyn - Eventually with explicit step count
• ensuresn - Stronger ensures with step function
• ensures2 - Relational Hoare triple for two programs

Frame Conditions

• maychange_regs - MAYCHANGE for registers
• maychange_mem - MAYCHANGE for memory

References

Source: s2n-bignum/common/relational.ml (HOL Light implementation)

Operational Semantics - Eventually

eventually step P s holds if predicate P is reachable from state s through the transition relation step.

The two inference rules:

1. base: If P s already holds, then eventually step P s
2. step: If there exists a next state AND all next states satisfy eventually step P, then eventually step P s

inductive Bignum.Arm.eventually {α : Sort u_1} (step : α → α → Prop) (P : α → Prop) : α → Prop

Reachability predicate: eventually step P s holds if P is reachable from s via the transition relation step.

• base {α : Sort u_1} {step : α → α → Prop} {P : α → Prop} {s : α} : P s → eventually step P s
• ind {α : Sort u_1} {step : α → α → Prop} {P : α → Prop} {s : α} (h₁ : ∃ (s' : α), step s s') (h₂ : ∀ (s' : α), step s s' → eventually step P s') : eventually step P s

Hoare Triple - Ensures

The ensures predicate defines Hoare triples with frame conditions:

"If precondition P holds in state s, then following the operational semantics (step), we eventually reach a state s' where:

• The postcondition Q s' holds
• The frame C s s' holds (only allowed components changed)"

This corresponds to the axiomatic semantics (Hoare logic) built ON TOP of the operational semantics (eventually).

def Bignum.Arm.ensures {α : Sort u_1} (step : α → α → Prop) (pre post : α → Prop) (frame : α → α → Prop) : Prop

ensures step pre post frame is the formal specification that from any state satisfying pre, we eventually reach a state satisfying post ∧ frame.

Equations

• Bignum.Arm.ensures step pre post frame = ∀ (s : α), pre s → Bignum.Arm.eventually step (fun (s' : α) => post s' ∧ frame s s') s

Theorems for Eventually and Ensures

theorem Bignum.Arm.eventually_mono {α : Sort u_1} {step : α → α → Prop} {P Q : α → Prop} (h : ∀ (s : α), P s → Q s) (s : α) : eventually step P s → eventually step Q s

Monotonicity of eventually: if P implies Q, then eventually P implies eventually Q.

Relational Composition

We use Mathlib's Relation.Comp for frame composition, which corresponds to HOL Light's ,, operator from s2n-bignum/common/relational.ml:26-27:

def Bignum.Arm.«term_,,_» : Lean.TrailingParserDescr

Notation for relational composition matching HOL Light's ,, operator.

Equations

• Bignum.Arm.«term_,,_» = Lean.ParserDescr.trailingNode `Bignum.Arm.«term_,,_» 13 14 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ,, ") (Lean.ParserDescr.cat `term 13))

theorem Bignum.Arm.eventually_trans {α : Sort u_1} {step : α → α → Prop} {P Q : α → Prop} (h : ∀ (s : α), P s → eventually step Q s) (s : α) : eventually step P s → eventually step Q s

theorem Bignum.Arm.ensures_trans {α : Sort u_1} {step : α → α → Prop} {P Q R : α → Prop} {C1 C2 : α → α → Prop} (h1 : ensures step P Q C1) (h2 : ensures step Q R C2) : ensures step P R (C1 ,, C2)

Transitivity of ensures: composing two ensures specifications.

Source: s2n-bignum/common/relational.ml:1373-1393 (ENSURES_TRANS)

theorem Bignum.Arm.ensures_trans_simple {α : Sort u_1} {step : α → α → Prop} {P Q R : α → Prop} {C : α → α → Prop} (h_idem : ∀ (s₀ s₂ : α), (C ,, C) s₀ s₂ → C s₀ s₂) (h1 : ensures step P Q C) (h2 : ensures step Q R C) : ensures step P R C

Simplified transitivity when frames are idempotent under relational composition (C ,, C = C).

This holds for MAYCHANGE-style frames where C s s' means "only certain components may differ between s and s'". Such frames are idempotent because if only certain components may change from s to s₁, and only those same components may change from s₁ to s', then only those components may change from s to s'.

Source: s2n-bignum/common/relational.ml:1394-1399 (ENSURES_TRANS_SIMPLE)

ARM Step Relation

The arm step relation defines single-instruction execution using fetch-decode- execute from memory, matching HOL Light's architecture where programs live in memory rather than as a separate structure.

def Bignum.Arm.arm (s s' : ArmState) : Prop

ARM single-step relation: arm s s' holds if s' is the result of executing one instruction from state s.

This corresponds to HOL Light's arm step relation. The execution:

1. Reads the PC
2. Fetches and decodes the instruction at PC from memory
3. Executes the instruction
4. Advances the PC (handled by step)

This definition keeps programs in memory, matching the paper's model where the machine state includes both data and code memory.

Equations

• Bignum.Arm.arm s s' = match Bignum.Arm.arm_decode s (s.read_reg Bignum.Arm.Reg.PC) with | some instr => s' = Bignum.Arm.step instr s | none => False

def Bignum.Arm.program_loaded (s : ArmState) (base : Word64) (mc : List UInt8) : Prop

A program (as machine code bytes) is loaded at the given base address.

This corresponds to HOL Light's aligned_bytes_loaded combined with a PC check. Used in preconditions to assert that the program bytes are in memory.

Equations

• Bignum.Arm.program_loaded s base mc = (Bignum.aligned_bytes_loaded s.mem base mc ∧ s.read_reg Bignum.Arm.Reg.PC = base)

def Bignum.Arm.program_bytes_loaded (s : ArmState) (base : Word64) (mc : List UInt8) : Prop

Alternative: program bytes loaded without PC constraint.

Equations

• Bignum.Arm.program_bytes_loaded s base mc = Bignum.aligned_bytes_loaded s.mem base mc

@[reducible, inline]

abbrev Bignum.Arm.ensures_arm (pre post : ArmState → Prop) (frame : ArmState → ArmState → Prop) : Prop

Convenience: ensures_arm specialized to the ARM step relation.

This is the primary interface for ARM program verification:

ensures_arm
  (fun s => program_loaded s base mc ∧ ...)  -- precondition
  (fun s => s.read_reg Reg.PC = ... ∧ ...)   -- postcondition
  (maychange_regs [Reg.PC, ...])             -- frame

Equations

• Bignum.Arm.ensures_arm = Bignum.Arm.ensures Bignum.Arm.arm

Frame Conditions (MAYCHANGE)

Frame conditions specify which components of the state MAY change during program execution. Everything not in the frame must remain unchanged.

source: s2n-bignum/common/relational.ml

In HOL Light, ASSIGNS and MAYCHANGE have the following semantics:

(* ASSIGNS c s s' means: there exists some value y such that s' = write c y s *)
(* i.e., s' differs from s only in component c *)
ASSIGNS (c:(A,B)component) s s' <=> exists y. (c := y) s s'

(* MAYCHANGE is relational composition of ASSIGNS *)
MAYCHANGE [] = (=)   (* equality relation: nothing changes *)
MAYCHANGE (CONS c cs) = ASSIGNS c ,, MAYCHANGE cs

For example: MAYCHANGE [PC; X2] = ASSIGNS PC ,, ASSIGNS X2

The key insight is that ASSIGNS c is trivially satisfiable for any two states (we can always choose y = read c s'). The real constraint comes from the composition: if only components in the list may change, then all other components must remain equal.

We use a simplified but equivalent formulation:

• unchanged_reg r s₁ s₂: register r has the same value in both states
• maychange_regs regs s₁ s₂: all registers NOT in regs are unchanged

Constructive vs Observational equivalence: HOL Light's ASSIGNS c s s' is constructive: it asserts s' = write c y s for some y. Our formulation is observational: it only asserts equality of values. These are equivalent when write is "pure" (only affects the target component) and the state has no hidden fields.

def Bignum.Arm.unchanged_reg (r : Reg) (s₁ s₂ : ArmState) : Prop

A register must not change between two states.

Equations

• Bignum.Arm.unchanged_reg r s₁ s₂ = (s₁.read_reg r = s₂.read_reg r)

def Bignum.Arm.unchanged_mem (addr : Address) (s₁ s₂ : ArmState) : Prop

Memory at an address must not change.

Equations

• Bignum.Arm.unchanged_mem addr s₁ s₂ = (s₁.read_mem_byte addr = s₂.read_mem_byte addr)

def Bignum.Arm.unchanged_flags (s₁ s₂ : ArmState) : Prop

All flags must not change between two states.

Equations

• Bignum.Arm.unchanged_flags s₁ s₂ = (s₁.flags = s₂.flags)

def Bignum.Arm.unchanged_flag (f : Flag) (s₁ s₂ : ArmState) : Prop

An individual flag must not change between two states.

Equations

• Bignum.Arm.unchanged_flag f s₁ s₂ = (s₁.read_flag f = s₂.read_flag f)

def Bignum.Arm.maychange_regs (regs : List Reg) (s₁ s₂ : ArmState) : Prop

maychange_regs regs s₁ s₂ holds when all registers NOT in regs are unchanged. This is equivalent to HOL Light's MAYCHANGE [r1; r2; ...] for registers: the registers in the list MAY change (no constraint), while all others must remain equal.

Source: s2n-bignum/common/relational.ml

Equations

• Bignum.Arm.maychange_regs regs s₁ s₂ = ∀ r ∉ regs, Bignum.Arm.unchanged_reg r s₁ s₂

def Bignum.Arm.maychange_mem (addrs : List Address) (s₁ s₂ : ArmState) : Prop

maychange_mem addrs s₁ s₂ holds when all memory addresses NOT in addrs are unchanged.

Equations

• Bignum.Arm.maychange_mem addrs s₁ s₂ = ∀ a ∉ addrs, Bignum.Arm.unchanged_mem a s₁ s₂

def Bignum.Arm.maychange_flags (flags : List Flag) (s₁ s₂ : ArmState) : Prop

maychange_flags flags s₁ s₂ holds when all flags NOT in flags are unchanged.

This allows fine-grained control like MAYCHANGE [CF; ZF] in HOL Light.

Source: s2n-bignum/arm/proofs/instruction.ml:186-192

Equations

• Bignum.Arm.maychange_flags flags s₁ s₂ = ∀ f ∉ flags, Bignum.Arm.unchanged_flag f s₁ s₂

def Bignum.Arm.maychange_and (f1 f2 : ArmState → ArmState → Prop) : ArmState → ArmState → Prop

Combine frame conditions via conjunction.

When we have maychange_regs regs ∧ maychange_mem addrs, both constraints must hold: registers outside regs are unchanged AND memory outside addrs is unchanged.

Equations

• (f1 ⊓ f2) s₁ s₂ = (f1 s₁ s₂ ∧ f2 s₁ s₂)

def Bignum.Arm.«term_⊓_» : Lean.TrailingParserDescr

Equations

• Bignum.Arm.«term_⊓_» = Lean.ParserDescr.trailingNode `Bignum.Arm.«term_⊓_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 35))

Idempotence of Frame Conditions

A key property for ensures_trans_simple is that MAYCHANGE-style frames are idempotent under relational composition: C ,, C = C.

This holds because:

• If only regs R may change from s₀ to s₁, and only R may change from s₁ to s₂
• Then only R may change from s₀ to s₂ (by transitivity of equality on other regs)

theorem Bignum.Arm.maychange_regs_idem (regs : List Reg) (s₀ s₂ : ArmState) : (maychange_regs regs ,, maychange_regs regs) s₀ s₂ → maychange_regs regs s₀ s₂

maychange_regs is idempotent under relational composition.

Source: s2n-bignum/common/relational.ml:188-192 (ASSIGNS_ABSORB_SAME_COMPONENTS)

theorem Bignum.Arm.maychange_regs_refl (regs : List Reg) (s : ArmState) : maychange_regs regs s s

Reflexivity: maychange_regs regs s s always holds (nothing changed).

This corresponds to HOL Light's (=) subsumed MAYCHANGE [...].