Semantics.lean🔗

Whole-Binary ELF Process Semantics & Safety/Correctness Specifications (Arm64.Trusted.Process.Semantics)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: Process-level termination and safety relations over Arm64.Step / Arm64.Steps (Program.pureWithSvc, Program.pureMem, ProcessTerminatedOutcome, ProcessExitsWith, the partial-correctness ProcessPartialRunsTo, ProcessTerminates, and the total ProcessRunsTo := ProcessTerminates ∧ ProcessPartialRunsTo) and the top-level whole-binary specifications over raw ELF bytes, an input precondition pre, and a relational postcondition post: total ElfRunsTo (with the wrappers ElfCorrect (exit 0) and ElfSafe (exit 0, trivial post)) and partial ElfPartialRunsTo (no termination claim).
When to read: Read when auditing a whole-binary theorem statement (ElfRunsTo, ElfPartialRunsTo, ElfCorrect, ElfSafe). Proof rules, per-image stepping stones, and executable runners live in ProofLib/Process.lean.

@[expose] public section

namespace Arm64

7 declarations not shown (lines 35–61): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Program.pureWithSvc, Arm64.Program.noSyscalls, Arm64.Program.stdioWrite, Arm64.Program.stdioCli, Arm64.Program.fileIo, Arm64.Program.alloc, Arm64.Program.pureMem

namespace Process

def ProcessTerminatedOutcomeL65–70 ↗#

State sf has terminated normally (SYS_exit / SYS_exit_group with signal = none) or by fatal signal (ExecStatus.Signaled sig with exitCode = 128 + sig.toNat and signal = some sig.toNat), yielding observable outcome out.

def ProcessTerminatedOutcome (sf : State) (out : ProcessOutcome) : Prop :=
  (∃ code, sf.status = .Exited code ∧ out = ProcessOutcome.ofState code sf) ∨
  (∃ sig, sf.status = .Signaled sig ∧ out = ProcessOutcome.ofSignal sig sf)

def ProcessExitsWithL72–78 ↗#

Execution of prog from initial state s0 reaches a terminated state sf (.Exited or .Signaled) whose observable outcome (exitCode, signal, stdout, stderr, fs) is out.

def ProcessExitsWith (prog : Program) (s0 : State) (out : ProcessOutcome) : Prop :=
  ∃ sf,
    Steps prog s0 sf ∧
    ProcessTerminatedOutcome sf out

def ProcessPartialRunsToL80–97 ↗#

Partial correctness (step safety) of the process run of prog from initial state s0: every state s' reachable from s0 under Steps prog either

has terminated (ProcessTerminatedOutcome s' out, .Exited or .Signaled) with post out,
has stopped with virtual or physical memory exhaustion (.OutOfMemory in brk/mmap/mprotect/mremap) and satisfies oom s' (default False), or
is .Running and can take a valid Step prog transition. In particular, no reachable state ever faults (.Exception), halts on unmapped/undecodable memory (.Halted), or hits a hook panic (.Panicked), and every terminated outcome satisfies post. This makes no termination claim: a run that never stops satisfies it as long as it never gets stuck, so post and oom constrain only the runs that do stop.

def ProcessPartialRunsTo (prog : Program) (s0 : State)
    (post : ProcessOutcome → Prop)
    (oom : State → Prop := fun _ => False) : Prop :=
  ∀ s', Steps prog s0 s' →
    (∃ out, ProcessTerminatedOutcome s' out ∧ post out) ∨
    (s'.status = .OutOfMemory ∧ oom s') ∨
    (s'.status = .Running ∧ ∃ s'', Step prog s' s'')

def ProcessTerminatesL99–107 ↗#

Termination of the process run of prog from initial state s0: some run reaches a terminated state (ProcessExitsWith prog s0 out, .Exited or .Signaled) whose outcome satisfies post out, or stops with .OutOfMemory in a state satisfying oom (default False).

def ProcessTerminates (prog : Program) (s0 : State)
    (post : ProcessOutcome → Prop)
    (oom : State → Prop := fun _ => False) : Prop :=
  (∃ out, ProcessExitsWith prog s0 out ∧ post out) ∨
  (∃ sf, Steps prog s0 sf ∧ sf.status = .OutOfMemory ∧ oom sf)

def ProcessRunsToL109–115 ↗#

Total correctness of the process run of prog from initial state s0: the run terminates (ProcessTerminates) and satisfies step safety (ProcessPartialRunsTo) with the same post and oom.

def ProcessRunsTo (prog : Program) (s0 : State)
    (post : ProcessOutcome → Prop)
    (oom : State → Prop := fun _ => False) : Prop :=
  ProcessTerminates prog s0 post oom ∧ ProcessPartialRunsTo prog s0 post oom

4 declarations not shown (lines 117–178): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Process.ElfRunsTo, Arm64.Process.ElfPartialRunsTo, Arm64.Process.ElfCorrect, Arm64.Process.ElfSafe

end Process

end Arm64