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_demonic (and Refines.executes for deterministic specifications).

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: demonic caller admissibility, angelic client run semantics, and bounded RAM execution with a relational postcondition.

Main results

• refines_iff_ofFn: equivalence with the functional runClient formulation on deterministic specifications ([D.HasStepFn f]).
• Refines.bind, Refines.bind_ofFn, Refines.branch: sequential and conditional controller certificates.
• Refines.call: inlining a dynamic operation after charged register preparation.
• Refines.executes_demonic, 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 : DataStructure.StateTransitionSpec} {α : 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 certifies that the client p is demonically admissible (D.DemonicValid) and implements a permitted D.ClientRun 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_iff_ofFn {D : DataStructure.StateTransitionSpec} {α : Type a} {B : Basis} {r : ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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) : Refines w pre p post budget code ↔ ∀ (s : D.State) (x : Data r), pre s x → D.ValidHistory s (D.clientHistory s p) ∧ ∃ (y : Data r), ExecWithin w code x y (budget s x) ∧ post (D.clientResult s p) (D.clientState s p) y

On a deterministic specification ([D.HasStepFn f]), Refines is equivalent to D.ValidHistory s (D.clientHistory s p) and post (D.clientResult s p) (D.clientState s p) y.

theorem Cslib.WordRAM.Refines.ofFn {D : DataStructure.StateTransitionSpec} {α : 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 → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (h : ∀ (s : D.State) (x : Data r), pre s x → D.ValidHistory s (D.clientHistory s p) ∧ ∃ (y : Data r), ExecWithin w code x y (budget s x) ∧ post (D.clientResult s p) (D.clientState s p) y) : Refines w pre p post budget code

Construct a Refines proof on a deterministic specification ([D.HasStepFn f]) from D.ValidHistory and D.clientResult / D.clientState / D.clientHistory.

theorem Cslib.WordRAM.Refines.toOfFn {D : DataStructure.StateTransitionSpec} {α : 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 → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (h : Refines w pre p post budget code) {s : D.State} {x : Data r} (hx : pre s x) : D.ValidHistory s (D.clientHistory s p) ∧ ∃ (y : Data r), ExecWithin w code x y (budget s x) ∧ post (D.clientResult s p) (D.clientState s p) y

Unpack a Refines proof on a deterministic specification ([D.HasStepFn f]) into D.ValidHistory and D.clientResult / D.clientState / D.clientHistory.

theorem Cslib.WordRAM.Refines.consequence {D : DataStructure.StateTransitionSpec} {α : 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 : DataStructure.StateTransitionSpec} {α : 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 : DataStructure.StateTransitionSpec} {α β : 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) (hvalid : ∀ (s : D.State) (x : Data r), pre s x → ∀ (a : α) (s' : D.State) (tr : D.Transcript), D.ClientRun s p a s' tr → D.DemonicValid s' (k a)) : 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, while hvalid ensures demonic continuation admissibility across all permitted specification outcomes of p.

theorem Cslib.WordRAM.Refines.bind_ofFn {D : DataStructure.StateTransitionSpec} {α β : Type a} {B : Basis} {r w : ℕ} {pre : D.State → Data r → Prop} {p : D.Client α} {budget : D.State → Data r → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {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₂)

On a deterministic specification ([D.HasStepFn f]), sequential composition automatically discharges demonic continuation admissibility from hk at the unique reached outcome.

theorem Cslib.WordRAM.Refines.branch {D : DataStructure.StateTransitionSpec} {α : 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 : DataStructure.StateTransitionSpec} {α : 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 : DataStructure.StateTransitionSpec} {α : 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 : DataStructure.StateTransitionSpec.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_demonic {D : DataStructure.StateTransitionSpec} {α : 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) : ∃ (a : α) (s' : D.State) (tr : D.Transcript) (n : ℕ), D.ClientRun s p a s' tr ∧ Executes w (code.program out) { pc := 0, data := x } (encode a) n ∧ n ≤ budget s x + 1

A certificate produces a real halting machine execution realizing a valid D.ClientRun.

theorem Cslib.WordRAM.Refines.executes {D : DataStructure.StateTransitionSpec} {α : 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 → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.clientResult s p)) n ∧ n ≤ budget s x + 1

On a deterministic specification ([D.HasStepFn f]), a certificate produces a real halting machine execution returning encode (D.clientResult s p).

theorem Cslib.WordRAM.Refines.call {D : DataStructure.StateTransitionSpec} {r w : ℕ} {pre : D.State → Data r → Prop} {P : DynamicProgram D.signature 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 Basis.standard) (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 Basis.standard o y.regs = some a) (fun (s : D.State) (x : Data r) => setup s x + body s x) (prep.seq (P.code Basis.standard))

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.