Machine certificates for stateful controllers

Refines relates a mathematical free-monad client to a fixed structured RAM program. Unlike an operation-count contract, its budget bounds an actual execution, including controller instructions and argument preparation. The final halt is added by Refines.executes.

The intermediate assertions record how answers are represented in registers or memory. The bind rule uses one continuation code fragment for every intermediate answer: Lean's semantic continuation is not an uncharged machine computation. Likewise returning a pure answer requires an execution certificate. Initialization is supplied as code using Refines.prepend.

Main definitions

• Refines: admissible client semantics and bounded RAM execution with a relational postcondition.

Main results

• Refines.bind, Refines.branch: sequential and conditional controller certificates.
• Refines.call: inlining a dynamic operation after charged register preparation.
• Refines.executes: a complete flat-program run, including its final halt.

References

The clients reuse Quang Dao's upstream PFunctor.FreeM. Machine execution and assembly reuse the word-RAM calculus based on the lean-trominoes formalization; see WordRAM.Defs.

def Cslib.WordRAM.Refines {D : Stateful.Spec} {α : Type a} {B : Basis} {r : ℕ} (w : ℕ) (pre : D.State → Data r → Prop) (p : D.Client α) (post : α → D.State → Data r → Prop) (budget : D.State → Data r → ℕ) (code : Code B r) : Prop

A fixed machine fragment implements the selected admissible client and its result/state representation, within a bound depending on the initial abstract and concrete states. As for ExecWithin, word boundedness is an entry assertion obligation: include Data.Bounded in pre when reasoning about arbitrary machine data. Standard Data.init inputs are bounded whenever InputFits holds.

theorem Cslib.WordRAM.Refines.consequence {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre pre' : D.State → Data r → Prop} {post post' : α → D.State → Data r → Prop} {p : D.Client α} {code : Code B r} {budget budget' : D.State → Data r → ℕ} (h : Refines w pre p post budget code) (hp : ∀ (s : D.State) (x : Data r), pre' s x → pre s x) (hq : ∀ (a : α) (s : D.State) (x : Data r), post a s x → post' a s x) (ht : ∀ (s : D.State) (x : Data r), pre' s x → budget s x ≤ budget' s x) : Refines w pre' p post' budget' code

Strengthen an entry assertion, weaken the exit assertion, or increase the instruction bound.

theorem Cslib.WordRAM.Refines.pure {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {post : α → D.State → Data r → Prop} {code : Code B r} {budget : D.State → Data r → ℕ} (a : α) (h : ∀ (s : D.State) (x : Data r), pre s x → ∃ (y : Data r), ExecWithin w code x y (budget s x) ∧ post a s y) : Refines w pre (PFunctor.FreeM.pure a) post budget code

Even a pure semantic computation needs actual code realizing its output assertion.

theorem Cslib.WordRAM.Refines.bind {D : Stateful.Spec} {α β : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {p : D.Client α} {budget : D.State → Data r → ℕ} {mid : α → D.State → Data r → Prop} {post : β → D.State → Data r → Prop} {k : α → D.Client β} {first : D.State → Data r → ℕ} {next : α → D.State → Data r → ℕ} {c₁ c₂ : Code B r} (hp : Refines w pre p mid first c₁) (hk : ∀ (a : α), Refines w (mid a) (k a) post (next a) c₂) (ht : ∀ (s : D.State) (x : Data r), pre s x → ∀ (a : α) (s' : D.State) (y : Data r), mid a s' y → first s x + next a s' y ≤ budget s x) : Refines w pre (PFunctor.FreeM.bind p k) post budget (c₁.seq c₂)

Compose with one fixed continuation fragment valid for every represented intermediate answer. The continuation budget is evaluated at the state actually reached by the first fragment.

theorem Cslib.WordRAM.Refines.branch {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {post : α → D.State → Data r → Prop} {budget : D.State → Data r → ℕ} (b : Prop) [Decidable b] {cond : Cond r} {yes no : D.Client α} {pos neg : Code B r} (hc : ∀ (s : D.State) (x : Data r), pre s x → (cond.Holds x ↔ b)) (hp : Refines w (fun (s : D.State) (x : Data r) => pre s x ∧ b) yes post budget pos) (hn : Refines w (fun (s : D.State) (x : Data r) => pre s x ∧ ¬b) no post budget neg) : Refines w pre (if b then yes else no) post (fun (s : D.State) (x : Data r) => budget s x + 2) (Code.branch cond pos neg)

A machine branch must test the same proposition as the semantic client. Both paths include all their control instructions; the common bound allows the larger two-instruction overhead.

theorem Cslib.WordRAM.Refines.prepend {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {post : α → D.State → Data r → Prop} {p : D.Client α} {code : Code B r} {budget budget' : D.State → Data r → ℕ} {entry : D.State → Data r → Prop} {init : Code B r} {setup : D.State → Data r → ℕ} (hinit : ∀ (s : D.State) (x : Data r), pre s x → ∃ (y : Data r), ExecWithin w init x y (setup s x) ∧ entry s y) (h : Refines w entry p post budget code) (ht : ∀ (s : D.State) (x : Data r), pre s x → ∀ (y : Data r), entry s y → setup s x + budget s y ≤ budget' s x) : Refines w pre p post budget' (init.seq code)

Charge initialization or argument computation preceding a certified client. The prefix preserves the abstract initial state, while establishing its concrete entry representation.

theorem Cslib.WordRAM.Refines.hoare {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {post : α → D.State → Data r → Prop} {p : D.Client α} {code : Code B r} {budget : D.State → Data r → ℕ} {abstractPre : D.State → Prop} {abstractPost : α → D.State → Prop} (h : Refines w pre p post budget code) (hspec : Stateful.Spec.Hoare abstractPre p abstractPost) (hp : ∀ (s : D.State) (x : Data r), pre s x → abstractPre s) : Refines w pre p (fun (a : α) (s : D.State) (y : Data r) => post a s y ∧ abstractPost a s) budget code

Discharge a client's abstract postcondition using an independently proved semantic contract.

theorem Cslib.WordRAM.Refines.executes {D : Stateful.Spec} {α : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {post : α → D.State → Data r → Prop} {p : D.Client α} {code : Code B r} {budget : D.State → Data r → ℕ} (h : Refines w pre p post budget code) (out : Fin r) (encode : α → ℕ) (hout : ∀ (a : α) (s : D.State) (y : Data r), post a s y → y.regs out = encode a) {s : D.State} {x : Data r} (hx : pre s x) : ∃ (n : ℕ), Executes w (code.program out) { pc := 0, data := x } (encode (D.runClient s p).1) n ∧ n ≤ budget s x + 1

A certificate produces a real halting machine execution. The output relation specifies which word represents the abstract answer; observing this word does not evaluate a host decoder.

theorem Cslib.WordRAM.Refines.call {D : Stateful.Spec} {r w : ℕ} {pre : D.State → Data r → Prop} {P : DynamicProgram D r} (C : DynamicCertificate P w) (o : D.Op) {prep : Code Basis.standard r} {setup body : D.State → Data r → ℕ} (hp : ∀ (s : D.State) (x : Data r), pre s x → C.rep s x ∧ D.valid s o) (hprep : ∀ (s : D.State) (x : Data r), pre s x → ExecWithin w prep x (P.prepare o x) (setup s x)) (hbody : ∀ (s : D.State) (x : Data r), pre s x → ∀ (y : Data r) (n : ℕ), Exec w P.code (P.prepare o x) y n → n ≤ body s x) : Refines w pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) (fun (a : D.signature.B o) (s : D.State) (y : Data r) => C.rep s y ∧ P.decode o y.regs = some a) (fun (s : D.State) (x : Data r) => setup s x + body s x) (prep.seq P.code)

Inline a dynamic operation after a machine-certified preparation fragment. The body bound excludes a halt because execution continues in the caller; only the complete program halts.