ARM Machine State

This file defines the ARM machine state used for verification.

Main Definitions

• Reg - ARM register names (X0-X30, PC, SP)
• Flags - ARM condition flags (N, Z, C, V)
• ArmState - Complete machine state (registers, flags, memory)
• read, write - Access registers and memory

References

This corresponds to the ARM state in HOL Light's ARM model. Source: s2n-bignum/arm/proofs/arm.ml and instruction.ml

inductive Bignum.Arm.Reg : Type

ARM general-purpose registers and special registers.

• X : Fin 31 → Reg
• PC : Reg
• SP : Reg

def Bignum.Arm.instDecidableEqReg.decEq (x✝ x✝¹ : Reg) : Decidable (x✝ = x✝¹)

Equations

• Bignum.Arm.instDecidableEqReg.decEq (Bignum.Arm.Reg.X a) (Bignum.Arm.Reg.X b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Bignum.Arm.instDecidableEqReg.decEq (Bignum.Arm.Reg.X a) Bignum.Arm.Reg.PC = isFalse ⋯
• Bignum.Arm.instDecidableEqReg.decEq (Bignum.Arm.Reg.X a) Bignum.Arm.Reg.SP = isFalse ⋯
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.PC (Bignum.Arm.Reg.X a) = isFalse ⋯
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.PC Bignum.Arm.Reg.PC = isTrue ⋯
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.PC Bignum.Arm.Reg.SP = isFalse Bignum.Arm.instDecidableEqReg.decEq._proof_7
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.SP (Bignum.Arm.Reg.X a) = isFalse ⋯
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.SP Bignum.Arm.Reg.PC = isFalse Bignum.Arm.instDecidableEqReg.decEq._proof_9
• Bignum.Arm.instDecidableEqReg.decEq Bignum.Arm.Reg.SP Bignum.Arm.Reg.SP = isTrue ⋯

instance Bignum.Arm.instDecidableEqReg : DecidableEq Reg

Equations

• Bignum.Arm.instDecidableEqReg = Bignum.Arm.instDecidableEqReg.decEq

def Bignum.Arm.instReprReg.repr : Reg → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bignum.Arm.instReprReg.repr Bignum.Arm.Reg.PC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Reg.PC")).group prec✝
• Bignum.Arm.instReprReg.repr Bignum.Arm.Reg.SP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Reg.SP")).group prec✝

instance Bignum.Arm.instReprReg : Repr Reg

Equations

• Bignum.Arm.instReprReg = { reprPrec := Bignum.Arm.instReprReg.repr }

def Bignum.Arm.Reg.X0 : Reg

Equations

• Bignum.Arm.Reg.X0 = Bignum.Arm.Reg.X 0

def Bignum.Arm.Reg.X1 : Reg

Equations

• Bignum.Arm.Reg.X1 = Bignum.Arm.Reg.X 1

def Bignum.Arm.Reg.X2 : Reg

Equations

• Bignum.Arm.Reg.X2 = Bignum.Arm.Reg.X 2

def Bignum.Arm.Reg.X3 : Reg

Equations

• Bignum.Arm.Reg.X3 = Bignum.Arm.Reg.X 3

def Bignum.Arm.Reg.X4 : Reg

Equations

• Bignum.Arm.Reg.X4 = Bignum.Arm.Reg.X 4

def Bignum.Arm.Reg.X5 : Reg

Equations

• Bignum.Arm.Reg.X5 = Bignum.Arm.Reg.X 5

def Bignum.Arm.Reg.X6 : Reg

Equations

• Bignum.Arm.Reg.X6 = Bignum.Arm.Reg.X 6

def Bignum.Arm.Reg.X7 : Reg

Equations

• Bignum.Arm.Reg.X7 = Bignum.Arm.Reg.X 7

def Bignum.Arm.Reg.X8 : Reg

Equations

• Bignum.Arm.Reg.X8 = Bignum.Arm.Reg.X 8

def Bignum.Arm.Reg.X30 : Reg

Equations

• Bignum.Arm.Reg.X30 = Bignum.Arm.Reg.X 30

instance Bignum.Arm.instToStringReg : ToString Reg

Equations

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

inductive Bignum.Arm.Flag : Type

ARM condition flag identifiers.

In HOL Light (s2n-bignum/arm/proofs/instruction.ml:186-192), flags are defined as sub-components of a 4-bit field:

let NF = define `NF = flags :> bitelement 3`;;
let ZF = define `ZF = flags :> bitelement 2`;;
let CF = define `CF = flags :> bitelement 1`;;
let VF = define `VF = flags :> bitelement 0`;;

Note: Named CFlag (Condition Flag) to avoid conflict with Mathlib's Flag.

• N : Flag
• Z : Flag
• C : Flag
• V : Flag

instance Bignum.Arm.instDecidableEqFlag : DecidableEq Flag

Equations

• Bignum.Arm.instDecidableEqFlag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Bignum.Arm.instReprFlag : Repr Flag

Equations

• Bignum.Arm.instReprFlag = { reprPrec := Bignum.Arm.instReprFlag.repr }

def Bignum.Arm.instReprFlag.repr : Flag → ℕ → Std.Format

Equations

• Bignum.Arm.instReprFlag.repr Bignum.Arm.Flag.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Flag.N")).group prec✝
• Bignum.Arm.instReprFlag.repr Bignum.Arm.Flag.Z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Flag.Z")).group prec✝
• Bignum.Arm.instReprFlag.repr Bignum.Arm.Flag.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Flag.C")).group prec✝
• Bignum.Arm.instReprFlag.repr Bignum.Arm.Flag.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bignum.Arm.Flag.V")).group prec✝

structure Bignum.Arm.Flags : Type

ARM condition flags as a structure.

• N : Bool
• Z : Bool
• C : Bool
• V : Bool

instance Bignum.Arm.instDecidableEqFlags : DecidableEq Flags

Equations

• Bignum.Arm.instDecidableEqFlags = Bignum.Arm.instDecidableEqFlags.decEq

def Bignum.Arm.instDecidableEqFlags.decEq (x✝ x✝¹ : Flags) : Decidable (x✝ = x✝¹)

Equations

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

def Bignum.Arm.instReprFlags.repr : Flags → ℕ → Std.Format

Equations

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

instance Bignum.Arm.instReprFlags : Repr Flags

Equations

• Bignum.Arm.instReprFlags = { reprPrec := Bignum.Arm.instReprFlags.repr }

def Bignum.Arm.Flags.read (f : Flags) : Flag → Bool

Read an individual flag by its identifier.

Equations

• f.read Bignum.Arm.Flag.N = f.N
• f.read Bignum.Arm.Flag.Z = f.Z
• f.read Bignum.Arm.Flag.C = f.C
• f.read Bignum.Arm.Flag.V = f.V

def Bignum.Arm.Flags.write (f : Flags) (fl : Flag) (v : Bool) : Flags

Write an individual flag by its identifier.

Equations

• f.write Bignum.Arm.Flag.N v = { N := v, Z := f.Z, C := f.C, V := f.V }
• f.write Bignum.Arm.Flag.Z v = { N := f.N, Z := v, C := f.C, V := f.V }
• f.write Bignum.Arm.Flag.C v = { N := f.N, Z := f.Z, C := v, V := f.V }
• f.write Bignum.Arm.Flag.V v = { N := f.N, Z := f.Z, C := f.C, V := v }

@[simp]

theorem Bignum.Arm.Flags.read_write_same (f : Flags) (fl : Flag) (v : Bool) : (f.write fl v).read fl = v

@[simp]

theorem Bignum.Arm.Flags.read_write_diff (f : Flags) (fl1 fl2 : Flag) (v : Bool) (h : fl1 ≠ fl2) : (f.write fl1 v).read fl2 = f.read fl2

structure Bignum.Arm.ArmState : Type

ARM machine state

This corresponds to the armstate type in HOL Light. Source: s2n-bignum/arm/proofs/arm.ml

• regs : Reg → Word64
• flags : Flags
• mem : Memory

theorem Bignum.Arm.ArmState.ext {s1 s2 : ArmState} (h_regs : s1.regs = s2.regs) (h_flags : s1.flags = s2.flags) (h_mem : s1.mem = s2.mem) : s1 = s2

Extensionality theorem for ArmState: two states are equal if all fields are equal.

theorem Bignum.Arm.ArmState.ext_iff {s1 s2 : ArmState} : s1 = s2 ↔ s1.regs = s2.regs ∧ s1.flags = s2.flags ∧ s1.mem = s2.mem

def Bignum.Arm.ArmState.read_reg (s : ArmState) (r : Reg) : Word64

Read a register value from the state.

Corresponds to HOL Light's read function. Example from simple.ml:78: read X0 s = word a

Equations

• s.read_reg r = s.regs r

def Bignum.Arm.ArmState.write_reg (s : ArmState) (r : Reg) (v : Word64) : ArmState

Write a value to a register.

Corresponds to HOL Light's state update for registers.

Equations

• s.write_reg r v = { regs := fun (r' : Bignum.Arm.Reg) => if r' = r then v else s.regs r', flags := s.flags, mem := s.mem }

def Bignum.Arm.ArmState.read_flag (s : ArmState) (f : Flag) : Bool

Read an individual flag from the state.

Corresponds to HOL Light's read CF s, read ZF s, etc.

Equations

• s.read_flag f = s.flags.read f

def Bignum.Arm.ArmState.write_flag (s : ArmState) (f : Flag) (v : Bool) : ArmState

Write an individual flag in the state.

Corresponds to HOL Light's flag update, e.g., CF := b.

Equations

• s.write_flag f v = { regs := s.regs, flags := s.flags.write f v, mem := s.mem }

def Bignum.Arm.ArmState.read_mem_byte (s : ArmState) (addr : Address) : Option UInt8

Read a byte from memory.

Equations

• s.read_mem_byte addr = s.mem.read_byte addr

def Bignum.Arm.ArmState.write_mem_byte (s : ArmState) (addr : Address) (byte : UInt8) : ArmState

Write a byte to memory.

Equations

• s.write_mem_byte addr byte = { regs := s.regs, flags := s.flags, mem := s.mem.write_byte addr byte }

def Bignum.Arm.ArmState.read_mem_word64 (s : ArmState) (addr : Address) : Option Word64

Read a 64-bit word from memory.

Equations

• s.read_mem_word64 addr = s.mem.read_word64 addr

def Bignum.Arm.ArmState.write_mem_word64 (s : ArmState) (addr : Address) (w : Word64) : ArmState

Write a 64-bit word to memory.

Equations

• s.write_mem_word64 addr w = { regs := s.regs, flags := s.flags, mem := s.mem.write_word64 addr w }

def Bignum.Arm.ArmState.read_bignum (s : ArmState) (addr : Address) (n : ℕ) : Option ℕ

Read a bignum from memory.

Corresponds to HOL Light's bignum_from_memory. Example from bignum_add.ml:91-92:

bignum_from_memory (x,val m) s = a /\
bignum_from_memory (y,val n) s = b

Equations

• s.read_bignum addr n = s.mem.read_bignum addr n

def Bignum.Arm.ArmState.write_bignum (s : ArmState) (addr : Address) (n val : ℕ) : ArmState

Write a bignum to memory.

Equations

• s.write_bignum addr n val = { regs := s.regs, flags := s.flags, mem := s.mem.write_bignum addr n val }

def Bignum.Arm.ArmState.write_flags (s : ArmState) (f : Flags) : ArmState

Update condition flags.

Equations

• s.write_flags f = { regs := s.regs, flags := f, mem := s.mem }

def Bignum.Arm.termRead__ : Lean.ParserDescr

Convenience notation for reading registers. Following HOL Light convention: read PC s means read program counter from state s.

Equations

• Bignum.Arm.termRead__ = Lean.ParserDescr.node `Bignum.Arm.termRead__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "read_") (Lean.ParserDescr.cat `term 1024))

def Bignum.Arm.ArmState.init (regs : Reg → Word64) (mem : Memory) : ArmState

Helper: Create initial state with given register values.

Equations

• Bignum.Arm.ArmState.init regs mem = { regs := regs, flags := { N := false, Z := false, C := false, V := false }, mem := mem }

Simplification Lemmas for Register Read/Write

These lemmas enable automatic simplification of register access patterns in proofs. They are essential for symbolic execution and proving correctness of instruction sequences.

@[simp]

theorem Bignum.Arm.ArmState.read_write_same (s : ArmState) (r : Reg) (v : Word64) : (s.write_reg r v).read_reg r = v

Reading a register immediately after writing to it returns the written value.

@[simp]

theorem Bignum.Arm.ArmState.read_write_diff (s : ArmState) (r1 r2 : Reg) (v : Word64) (h : r1 ≠ r2) : (s.write_reg r1 v).read_reg r2 = s.read_reg r2

Reading a different register is not affected by a write to another register.

@[simp]

theorem Bignum.Arm.ArmState.write_write_same (s : ArmState) (r : Reg) (v1 v2 : Word64) : (s.write_reg r v1).write_reg r v2 = s.write_reg r v2

Writing twice to the same register: the second write overwrites the first.

@[simp]

theorem Bignum.Arm.ArmState.write_write_comm (s : ArmState) (r1 r2 : Reg) (v1 v2 : Word64) (h : r1 ≠ r2) : (s.write_reg r1 v1).write_reg r2 v2 = (s.write_reg r2 v2).write_reg r1 v1

Writes to different registers commute.

@[simp]

theorem Bignum.Arm.ArmState.read_init (regs : Reg → Word64) (mem : Memory) (r : Reg) : (init regs mem).read_reg r = regs r

Reading from initial state with explicit register function.

Simplification Lemmas for Flag Read/Write

@[simp]

theorem Bignum.Arm.ArmState.read_flag_write_flag_same (s : ArmState) (f : Flag) (v : Bool) : (s.write_flag f v).read_flag f = v

Reading a flag immediately after writing to it returns the written value.

@[simp]

theorem Bignum.Arm.ArmState.read_flag_write_flag_diff (s : ArmState) (f1 f2 : Flag) (v : Bool) (h : f1 ≠ f2) : (s.write_flag f1 v).read_flag f2 = s.read_flag f2

Reading a different flag is not affected by writing another flag.

@[simp]

theorem Bignum.Arm.ArmState.read_reg_write_flag (s : ArmState) (r : Reg) (f : Flag) (v : Bool) : (s.write_flag f v).read_reg r = s.read_reg r

Writing a flag does not affect registers.

@[simp]

theorem Bignum.Arm.ArmState.read_flag_write_reg (s : ArmState) (f : Flag) (r : Reg) (v : Word64) : (s.write_reg r v).read_flag f = s.read_flag f

Writing a register does not affect flags.