Semantics.lean🔗

Declarations on this page (9)

ARM64 Small-Step Operational Semantics (Arm64.Semantics)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: Read-only relocated code image (Program), instruction fetch and decode from executable memory (Program.fetchMem) and from the static image (Program.fetch), code-in-memory invariant (Program.CodeLoaded), single-step transition relation (Step), and multi-step closure (Steps). The executable fuel-bounded evaluators (ProofLib.stepState, execN, execUntilPC) and the test-memory builder Program.loadCode are untrusted and live in ProofLib/Exec.lean.
When to read: Read when auditing how Step fetches from s.mem (fetchMem), dispatches externs/overrides hooks (Step.extern), or enforces Memory.KeepsFrozen. For proof stepping lemmas, see ProofLib/Semantics.lean.

Instructions are fetched from memory (Program.fetchMem) at an aligned, executable pc. Because executable memory is never writable (canWrite requires ¬x) and every Step preserves frozen bytes (Memory.KeepsFrozen), Program.CodeLoaded is invariant across execution and Program.fetch agrees with Program.fetchMem on loaded states.

@[expose] public section

namespace Arm64

1 declaration not shown (lines 43–44): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.execInst

def evalSvcL46–53 ↗#

Apply supervisor-call handler svc while preserving frozen memory (Perm.frozen), tpidrEl0, and symtab, matching architectural user-space supervisor-call invariants.

def evalSvc (svc : State → State) (s : State) : State :=
  let s' := svc s
  { s' with
    mem := ⟨fun a => if (s.mem.perm a).frozen then s.mem.cells a else s'.mem.cells a⟩
    tpidrEl0 := s.tpidrEl0
    symtab := s.symtab }

structure ProgramL55–71 ↗#

A read-only AArch64 code image:

base: load address of code,
code: instruction bytes, with relocations applied,
symbols: defined symbols (demangled names) and their offsets from base,
stubs: extern functions and the offsets of their stubs,
externs: behaviour of extern functions, consulted at stub offsets,
overrides: replacement behaviour for defined functions, consulted at symbol offsets,
svc: supervisor-call (SVC #0) handler bundle, defaulting to Syscall.standard. See Step.extern and Step.exec.

structure Program where
  base : BitVec 64 := 0#64
  code : List (BitVec 8) := []
  symbols : List (String × Nat) := []
  stubs : List (String × Nat) := []
  externs : String → Option (State → State) := fun _ => none
  overrides : String → Option (State → State) := fun _ => none
  svc : State → State := Syscall.standard

namespace Program

2 declarations not shown (lines 75–86): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Program.ofSvc, Arm64.Program.withSvc

def evalInstL88–90 ↗#

Execute a single decoded Instr under prog's supervisor-call handler (evalSvc prog.svc).

def evalInst (prog : Program) (inst : Instr) (s : State) : State :=
  execInstWithSvc (evalSvc prog.svc) inst s

6 declarations not shown (lines 92–122): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Program.wordToBytesLE, Arm64.Program.ofWords, Arm64.Program.findSymbol?, Arm64.Program.fnOff, Arm64.Program.fnAddr, Arm64.Program.rebase

def hookAtOff?L124–127 ↗#

The hook at offset off: an extern at a stub, or an override at a defined symbol.

def hookAtOff? (prog : Program) (off : Nat) : Option (State → State) :=
  (prog.stubs.findSome? fun (n, o) => if o == off then prog.externs n else none).or
    (prog.symbols.findSome? fun (n, o) => if o == off then prog.overrides n else none)

def externAt?L129–131 ↗#

The hook, if any, whose entry point is pc.

def externAt? (prog : Program) (pc : BitVec 64) : Option (State → State) :=
  prog.hookAtOff? (pc - prog.base).toNat

2 declarations not shown (lines 133–149): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Program.readWordOff, Arm64.Program.fetch

def fetchMemL151–159 ↗#

Fetch and decode the instruction at pc from memory m: the 32-bit little-endian word at pc, which must be 4-byte aligned and executable (Memory.canExec); otherwise none (the real machine faults). At a hooked entry point fetchMem returns none, as fetch does.

def fetchMem (prog : Program) (m : Memory) (pc : BitVec 64) : Option Instr :=
  if (prog.externAt? pc).isSome then none
  else if pc.toNat % 4 ≠ 0 then none
  else if !m.canExec pc 4 then none
  else decode (m.read32 pc)

6 declarations not shown (lines 161–228): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Program.CodeLoaded, Arm64.Program.hookFree, Arm64.Program.hasWordsOff, Arm64.Program.hasWords, Arm64.Program.hasCode, Arm64.Program.decidableForallLT

end Program

inductive StepL232–268 ↗#

Trusted small-step operational semantics relation Step prog s s'.

At an extern entry point (prog.externAt? s.pc = some f) exactly one of extern / extern_fault applies (fetchMem returns none there); elsewhere exactly one of exec / halt_unmapped applies, so Step is deterministic.

inductive Step (prog : Program) : State → State → Prop where
  /-- Execute one instruction, fetched from memory and decoded, when `s.status = .Running`. -/
  | exec {s : State} {inst : Instr}
      (h_run : s.status = .Running)
      (h_fetch : prog.fetchMem s.mem s.pc = some inst) :
      Step prog s (prog.evalInst inst s)
  /-- Halt when no valid instruction can be fetched at `s.pc` (unmapped, not executable,
      misaligned, or not decodable) and `s.pc` is not a hooked entry point. This includes an
      extern stub with no `externs` entry. -/
  | halt_unmapped {s : State}
      (h_run : s.status = .Running)
      (h_fetch : prog.fetchMem s.mem s.pc = none)
      (h_ext : prog.externAt? s.pc = none) :
      Step prog s { s with status := .Halted }
  /-- A call to a hooked function at `s.pc` takes effect in one step: the architectural
      state `s` is mapped to `f s`, provided `f` keeps every frozen (mapped, non-writable)
      byte (`Memory.KeepsFrozen`) and preserves `symtab`, as any real function must. Otherwise
      `extern_fault` applies. Beyond that the semantics places no constraint on `f`; whoever
      supplies it is responsible for `f` representing a sensible return. -/
  | extern {s : State} {f : State → State}
      (h_run : s.status = .Running)
      (h_ext : prog.externAt? s.pc = some f)
      (h_keep : s.mem.KeepsFrozen (f s).mem)
      (h_symtab : (f s).symtab = s.symtab := by rfl) :
      Step prog s (f s)
  /-- A hook that would change a frozen byte (e.g. code or read-only data) or the symbol
      table faults instead, leaving the state unchanged except for the status. -/
  | extern_fault {s : State} {f : State → State}
      (h_run : s.status = .Running)
      (h_ext : prog.externAt? s.pc = some f)
      (h_nkeep : ¬ (s.mem.KeepsFrozen (f s).mem ∧ (f s).symtab = s.symtab)) :
      Step prog s { s with status := .Exception "extern hook modified read-only memory or symbol table" }

inductive StepsL270–273 ↗#

Reflexive-transitive closure of Step.

inductive Steps (prog : Program) : State → State → Prop where
  | refl (s : State) : Steps prog s s
  | step {s1 s2 s3 : State} (h1 : Step prog s1 s2) (h2 : Steps prog s2 s3) : Steps prog s1 s3

inductive StepsUntilL275–283 ↗#

Reflexive-transitive execution of prog that stops as soon as stop s holds: no intermediate state prior to the final state satisfies stop.

inductive StepsUntil (prog : Program) (stop : State → Prop) : State → State → Prop where
  | refl (s : State) : StepsUntil prog stop s s
  | step {s1 s2 s3 : State}
      (h_cont : ¬ stop s1)
      (h_step : Step prog s1 s2)
      (h_rest : StepsUntil prog stop s2 s3) :
      StepsUntil prog stop s1 s3

end Arm64