Hoare.lean🔗

ARM64 Subroutine Specifications

Relational separation-logic contracts (Spec), AAPCS64 calling-convention invariants (CalleeSavedPreserved, CallingConventionPreserved, Returned, SubroutineStop, SubroutineOutcome), execution judgments (reaches_stop, safe_until, safe_reaches, reaches_outcome, exits_with), framed Hoare triples (subroutine_ok, safe_subroutine_ok, exit_ok, HookOk, HookSat), symbol-addressed program judgments (Program.subroutineOk, Program.safeSubroutineOk, Program.exitOk), and subroutine-to-hook primitives (subroutineHook).

reaches_outcome and subroutine_ok are defined inside a plain public section (not @[expose]), so client modules see only their abstract signatures while ProofLib rules and adequacy tests in Arm64/Testing import all Arm64.Trusted.Spec.Hoare explicitly. Frame, consequence, and bare-machine adequacy properties are checked in Arm64/Testing/Tours/SepLogicLawsTour.lean and Arm64/Testing/Tours/SpecAdequacyTour.lean.

All judgments assume prog.CodeLoaded s0.mem and quantify over an arbitrary frame R : SepProp. subroutine_ok states total correctness: from any 16-byte-aligned .Running entry state satisfying spec.pre x s0 ∗ R, execution terminates in a valid SubroutineOutcome. safe_subroutine_ok states safety-style partial correctness: execution either reaches a valid SubroutineOutcome or runs forever in .Running with a Step successor at every reachable state, so faulting (.Exception) and halting (.Halted) runs are excluded.

namespace Arm64

@[expose] public section

5 declarations not shown (lines 52–96): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.VRegFile.calleeSaved, Arm64.calleeSavedVRegs, Arm64.CalleeSavedVRegsPreserved, Arm64.CalleeSavedPreserved, Arm64.CallingConventionPreserved

def ReturnedL98–101 ↗#

The machine has returned to the caller of entry state s0: pc is at s0.readReg64 Reg.lr, the stack pointer sp is restored to s0.sp, and status = .Running.

def Returned (s0 s : State) : Prop :=
  s.pc = s0.readReg64 Reg.lr ∧ s.sp = s0.sp ∧ s.status = .Running

def SubroutineStopL103–107 ↗#

Terminal stopping condition for a subroutine entered at s0: normal return (Returned s0 s), panic (s.status = .Panicked), process exit (s.status = .Exited code), or out-of-memory in brk/mmap/mprotect/mremap (s.status = .OutOfMemory).

def SubroutineStop (s0 s : State) : Prop :=
  Returned s0 s ∨ s.status = .Panicked ∨ (∃ code, s.status = .Exited code) ∨ s.status = .OutOfMemory

10 declarations not shown (lines 111–199): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.reaches_stop, Arm64.safe_until, Arm64.safe_until_pc, Arm64.safe_reaches, Arm64.Spec, Arm64.Spec.post, Arm64.Spec.onPanic, Arm64.Spec.onOom, Arm64.Spec.onExit, Arm64.Spec.pre, Arm64.Spec.allowPanicWhen, Arm64.Spec.allowOomWhen, Arm64.Spec.allowOom, Arm64.SubroutineOutcome, Arm64.AapcsEntry

end -- @[expose] public section

38 declarations not shown (lines 205–526): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.reaches_outcome, Arm64.subroutine_ok, Arm64.FnPtrSpec, Arm64.safe_subroutine_ok, Arm64.SafeFnPtrSpec, Arm64.exits_with, Arm64.exit_ok, Arm64.HookOk, Arm64.HookSat, Arm64.Program.codeAt, Arm64.Program.codeAtOff, Arm64.Program.codeAtAddr, Arm64.FnPin.none, Arm64.FnPin.addr, Arm64.FnPin.off, Arm64.FnPin, Arm64.FnCode.hex, Arm64.FnCode, Arm64.FnCode.fnName, Arm64.FnCode.pin, Arm64.FnCode.words, Arm64.FnCode.ofFn, Arm64.FnCode.atAddr, Arm64.FnCode.holds, Arm64.CodeBundle, Arm64.Program.hasCodeBundle, Arm64.Program.instDecidableHasCodeBundle, Arm64.BaseSpec, Arm64.ToBaseSpec.toSpec, Arm64.ToBaseSpec, Arm64.instToBaseSpecId, Arm64.instToBaseSpecFn, Arm64.Program.subroutineOk, Arm64.Program.safeSubroutineOk, Arm64.fn_subroutine_ok, Arm64.Program.relocSubroutineOk, Arm64.Program.alignedSubroutineOk, Arm64.Program.exitOk, Arm64.allHold, Arm64.Program.calleesOk, Arm64.loadCodeMem, Arm64.restoreCodeMem, Arm64.subroutineHookEntry, Arm64.subroutineHookExit, Arm64.subroutineHook

end Arm64