Fixed-program implementations of dynamic data structures

DynamicProgram depends only on the existing PFunctor operation signature and its instruction basis, which defaults to .standard. Deterministic and relational specifications supply their signatures by coercion; correctness certificates retain the actual specification separately.

An implementation has one structured program, one output register, and a register-only calling convention. Each call replaces designated input registers with encoded words, preserving all other registers and the entire memory. Argument encoding, external delivery, and result decoding are not charged; all instructions of the operation, including its final halt, are charged. Initialization is a separate obligation expressed by the initial representation hypothesis. Argument encoding depends on the requested operation, without access to the maintained machine data.

Certificates require bounded configurations and bounded arguments, and a successful exact machine execution for every admissible operation. Determinism supplies correctness for every execution. The generic history theorem then preserves all observations and adds actual costs. The same single compiled program is used at every call; the interface does not generate code from the requested operation.

Evaluating calls

P.eval w fuel o x delivers the arguments, runs the fixed program and decodes the operation's typed observation. It returns some (y, answer, cost), with final data y for the next call and a cost that already includes halt. fuel bounds each structured loop's iterations per entry, not the total instruction count. Exhaustion, a machine fault or decoder rejection returns outer none; a successful empty stack pop instead has observation none.

Evaluation does not establish admissibility or check untouched memory for word bounds. C.execOp_of_eval hr hv he turns a successful evaluation he into exact execution evidence using representation hr and admissibility hv. Argument delivery and decoding remain uncharged. Whole-client bounds remain separate resource proofs.

See the checked examples in CslibFrontierTests/WordRAMDynamic.lean for typed stack observations, the seven-body/eight-charged push and certificate lifting, and CslibFrontierTests/WordRAMPrefixSums.lean for repeated calls retaining persistent data.

Main definitions

• DynamicProgram, DynamicProgram.prepare: fixed code, an input-register convention, an output decoder, and argument-delivery state update.
• DynamicProgram.eval: typed call evaluation with halt-inclusive instruction cost.
• DynamicProgram.OperationTrace, DynamicProgram.ExecOp: call trace and execution of a call, including the final halt charge.
• DynamicCertificate: representation, word bounds, and per-operation semantic machine proofs.

Main results

• DynamicProgram.ExecOp.executes: calls execute the same flat program.
• DynamicCertificate.execOp_of_eval: certify an evaluated admissible call.
• DynamicCertificate.impl: machine certificates instantiate shared adaptive execution.
• DynamicCertificate.instruction_bound: separate native instruction-cost certificates.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms.

structure Cslib.WordRAM.DynamicProgram (S : PFunctor.{v, z}) (r : ℕ) (B : Basis := Basis.standard) : Type (max v z)

A single program serving an operation signature through a fixed register calling convention. Deterministic and relational stateful specifications supply their signatures by coercion; the program itself makes no assumption about abstract states or permitted transitions.

• code : Code B r

  The same code is executed for every operation.

• output : Fin r

  Register returned by the final halt instruction.

• input : Fin r → Bool

  Registers overwritten by externally supplied operation arguments.

• encode : S.A → Fin r → ℕ

  Encoded arguments, independent of the maintained machine state.

• decode (o : S.A) : (Fin r → ℕ) → Option (S.B o)

  Interpretation of the final register tuple as the operation's typed observation.

def Cslib.WordRAM.DynamicProgram.prepare {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) (o : S.A) (x : Data r) : Data r

Deliver operation arguments without changing maintained memory or non-input registers.

@[simp]

theorem Cslib.WordRAM.DynamicProgram.prepare_mem {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) (o : S.A) (x : Data r) : (P.prepare o x).mem = x.mem

Delivering operation arguments preserves the machine memory unchanged.

theorem Cslib.WordRAM.DynamicProgram.prepare_regs_of_not_input {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {i : Fin r} (hi : P.input i = false) (o : S.A) (x : Data r) : (P.prepare o x).regs i = x.regs i

Registers outside the calling convention retain their contents.

theorem Cslib.WordRAM.DynamicProgram.prepare_bounded {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w : ℕ} {o : S.A} {x : Data r} (hx : Data.Bounded w x) (ho : ∀ (i : Fin r), P.input i = true → Fits w (P.encode o i)) : Data.Bounded w (P.prepare o x)

Argument delivery preserves bounded words when the arguments fit.

def Cslib.WordRAM.DynamicProgram.eval {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) (w fuel : ℕ) (o : S.A) (x : Data r) : Option (Data r × S.B o × ℕ)

Evaluate one typed call, delivering its arguments and decoding its observation. The returned cost includes the final halt. fuel bounds iterations of each structured loop per entry, not instructions; exhaustion, a machine fault, or decoder failure returns none.

This interpreter does not check the initial state's global word bound or operation admissibility. Use DynamicCertificate.execOp_of_eval to connect a successful call to certified execution.

structure Cslib.WordRAM.DynamicProgram.OperationTrace : Type

Native evidence for one call: instruction count including halt and the memory transcript.

• instructions : ℕ

  Number of executed machine instructions, including the final halt.

• probes : List Probe

  All reads and writes, in execution order.

def Cslib.WordRAM.DynamicProgram.ExecOp {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) (w : ℕ) : DataStructure.Execution S (Data r) OperationTrace

A bounded machine call with native execution evidence independent of any resource bound.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.of_eval {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w fuel k : ℕ} {o : S.A} {x y : Data r} {a : S.B o} (hb : Data.Bounded w (P.prepare o x)) (h : P.eval w fuel o x = some (y, a, k)) : ∃ (probes : List Probe), P.ExecOp w x o a y { instructions := k, probes := probes }

Successful typed evaluation supplies an exact operation trace when the delivered state is bounded. Evaluator success alone does not imply a bound on untouched memory.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.executes {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w : ℕ} {x y : Data r} {o : S.A} {a : S.B o} {trace : OperationTrace} (h : P.ExecOp w x o a y trace) : Executes w (P.code.program P.output) { pc := 0, data := P.prepare o x } (y.regs P.output) trace.instructions

Every call is an execution of one fixed flat machine program. The returned register tuple is observed at the final state; the designated output register is also the halt value.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.bounded {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w : ℕ} {x y : Data r} {o : S.A} {a : S.B o} {trace : OperationTrace} (h : P.ExecOp w x o a y trace) : Data.Bounded w y

A call preserves bounded words, including every word in the observed register tuple.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.unique {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w : ℕ} {x y y' : Data r} {o : S.A} {a a' : S.B o} {trace trace' : OperationTrace} (h : P.ExecOp w x o a y trace) (h' : P.ExecOp w x o a' y' trace') : y = y' ∧ a = a' ∧ trace.instructions = trace'.instructions

Calls are deterministic in their final representation, observation, and instruction count.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.eq_of_exec {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} {P : DynamicProgram S r B} {w : ℕ} {x y z : Data r} {o : S.A} {a : S.B o} {trace : OperationTrace} {m : ℕ} (he : P.ExecOp w x o a y trace) (h : Exec w P.code (P.prepare o x) z m) : y = z ∧ trace.instructions = m + 1

A call's final state and instruction count agree with any structured execution of the code.

theorem Cslib.WordRAM.DynamicProgram.ExecOp.frame {r : ℕ} {S : PFunctor.{v, z}} {B : Basis} (P : DynamicProgram S r B) {w : ℕ} {x y : Data r} {o : S.A} {a : S.B o} {trace : OperationTrace} (h : P.ExecOp w x o a y trace) {Q : HeapAssertion} (hQ : Q.holds x.mem) (hd : Disjoint Q.footprint (Probe.writes trace.probes)) : Q.holds y.mem

The write transcript supplies a frame rule for a call, including register-only delivery.

structure Cslib.WordRAM.DynamicCertificate {r : ℕ} {D : DataStructure.StateTransitionSpec} (P : DynamicProgram D.signature r) (w : ℕ) : Type u

Per-operation relational semantic proof obligations tied to fixed bounded-word code. Performance claims are supplied separately, as DataStructure.Bound or DataStructure.Amortized certificates.

• rep : D.State → Data r → Prop

  Abstract state represented by the persistent machine data.

• bounded {s : D.State} {x : Data r} : self.rep s x → Data.Bounded w x

  Represented configurations contain only machine words.

• arguments_fit {s : D.State} (o : D.Op) : D.valid s o → ∀ (i : Fin r), P.input Basis.standard i = true → Fits w (P.encode Basis.standard o i)

  Admissible arguments fit the machine's word size.

• execute {s : D.State} {x : Data r} (o : D.Op) : self.rep s x → D.valid s o → ∃ (y : Data r) (s' : D.State) (a : D.Result o) (n : ℕ), Exec w (P.code Basis.standard) (P.prepare o x) y n ∧ D.step s o s' a ∧ P.decode Basis.standard o y.regs = some a ∧ self.rep s' y

  A machine execution implements some permitted outcome (s', a) of an admissible operation.

def Cslib.WordRAM.DynamicCertificate.ofFn {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (rep : D.State → Data r → Prop) (bounded : ∀ {s : D.State} {x : Data r}, rep s x → Data.Bounded w x) (arguments_fit : ∀ {s : D.State} (o : D.Op), D.valid s o → ∀ (i : Fin r), P.input Basis.standard i = true → Fits w (P.encode Basis.standard o i)) (execute : ∀ {s : D.State} {x : Data r} (o : D.Op), rep s x → D.valid s o → ∃ (y : Data r) (n : ℕ), Exec w (P.code Basis.standard) (P.prepare o x) y n ∧ P.decode Basis.standard o y.regs = some (D.stepFn s o).2 ∧ rep (D.stepFn s o).1 y) : DynamicCertificate P w

Construct a DynamicCertificate for a deterministic specification ([D.HasStepFn f]) from a functional execute obligation at (D.stepFn s o).

theorem Cslib.WordRAM.DynamicCertificate.execOp_of_eval {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {s : D.State} {x y : Data r} {o : D.Op} {a : D.Result o} {fuel k : ℕ} (hr : C.rep s x) (hv : D.valid s o) (h : P.eval w fuel o x = some (y, a, k)) : ∃ (probes : List Probe), P.ExecOp w x o a y { instructions := k, probes := probes }

A represented state and an admissible operation supply the word bounds needed to turn typed evaluation into a certified call, including its final halt charge.

def Cslib.WordRAM.DynamicCertificate.impl {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) : DataStructure.StateTransitionImpl D (P.ExecOp w)

Fixed-program certificates implement the relational dynamic specification, without choosing a cost.

theorem Cslib.WordRAM.DynamicCertificate.instruction_bound {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) (charge : D.State → D.Op → ℕ) (hbound : ∀ {s : D.State} {x : Data r} (o : D.Op) {y : Data r} {n : ℕ}, C.rep s x → D.valid s o → Exec w (P.code Basis.standard) (P.prepare o x) y n → n + 1 ≤ charge s o) : DataStructure.Bound C.impl DynamicProgram.OperationTrace.instructions charge

A separate per-operation instruction estimate supplies a reusable resource certificate.

theorem Cslib.WordRAM.DynamicCertificate.instruction_bound_const {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) (K : ℕ) (hbound : ∀ {s : D.State} {x : Data r} (o : D.Op), C.rep s x → D.valid s o → ∃ (y : Data r) (n : ℕ), Exec w (P.code Basis.standard) (P.prepare o x) y n ∧ n + 1 ≤ K) : DataStructure.Bound C.impl DynamicProgram.OperationTrace.instructions fun (x : D.State) (x_1 : D.Op) => K

A uniform constant instruction bound follows from an existential per-operation execution.

theorem Cslib.WordRAM.DynamicCertificate.run_client_const {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {K : ℕ} (B : DataStructure.Bound C.impl DynamicProgram.OperationTrace.instructions fun (x : D.State) (x_1 : D.Op) => K) {α : Type u_1} (p : D.Client α) {s : D.State} {x : Data r} (hr : C.rep s x) (hv : D.ValidHistory s (D.clientHistory s p)) : ∃ (y : Data r) (traces : List DynamicProgram.OperationTrace), DataStructure.Executes (P.ExecOp w) p x (D.clientResult s p) y traces ∧ C.rep (D.clientState s p) y ∧ DataStructure.total DynamicProgram.OperationTrace.instructions traces ≤ (D.clientHistory s p).length * K

Adaptive client execution, final representation, and linear total instruction bound for a uniform constant per-operation instruction certificate on a deterministic specification.

theorem Cslib.WordRAM.DynamicCertificate.frame_of_execute {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {j : ℕ} (hframe : ∀ {s : D.State} {x : Data r} (o : D.Op), C.rep s x → D.valid s o → ∃ (z : Data r) (n : ℕ), Exec w (P.code Basis.standard) (P.prepare o x) z n ∧ z.mem j = x.mem j) {s : D.State} {x y : Data r} {o : D.Op} {a : D.Result o} {trace : DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.valid s o) (he : P.ExecOp w x o a y trace) : y.mem j = x.mem j

Lift a per-operation pointwise memory frame from Exec to ExecOp.

theorem Cslib.WordRAM.DynamicCertificate.modifies_of_execute {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {F : Finset ℕ} (hmod : ∀ {s : D.State} {x : Data r} (o : D.Op), C.rep s x → D.valid s o → ∃ (z : Data r) (n : ℕ), Exec w (P.code Basis.standard) (P.prepare o x) z n ∧ Modifies F x.mem z.mem) {s : D.State} {x y : Data r} {o : D.Op} {a : D.Result o} {trace : DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.valid s o) (he : P.ExecOp w x o a y trace) : Modifies F x.mem y.mem

Lift a per-operation Modifies bound from Exec to ExecOp.

theorem Cslib.WordRAM.DynamicCertificate.executes_demonic_frame {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {j : ℕ} (hframe : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.signature.B o} {trace : DynamicProgram.OperationTrace}, C.rep s x → D.valid s o → P.ExecOp w x o a y trace → y.mem j = x.mem j) {α : Type u_1} {p : D.Client α} {s : D.State} {x y : Data r} {val : α} {traces : List DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.DemonicValid s p) (he : DataStructure.Executes (P.ExecOp w) p x val y traces) : y.mem j = x.mem j

Lift a per-operation pointwise memory frame across a demonically admissible adaptive client execution.

theorem Cslib.WordRAM.DynamicCertificate.executes_demonic_modifies {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {F : Finset ℕ} (hmod : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.signature.B o} {trace : DynamicProgram.OperationTrace}, C.rep s x → D.valid s o → P.ExecOp w x o a y trace → Modifies F x.mem y.mem) {α : Type u_1} {p : D.Client α} {s : D.State} {x y : Data r} {val : α} {traces : List DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.DemonicValid s p) (he : DataStructure.Executes (P.ExecOp w) p x val y traces) : Modifies F x.mem y.mem

Lift a per-operation Modifies bound across a demonically admissible adaptive client execution.

theorem Cslib.WordRAM.DynamicCertificate.executes_client_frame {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {j : ℕ} (hframe : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.signature.B o} {trace : DynamicProgram.OperationTrace}, C.rep s x → D.valid s o → P.ExecOp w x o a y trace → y.mem j = x.mem j) {α : Type u_1} {p : D.Client α} {s : D.State} {x y : Data r} {val : α} {traces : List DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.ValidHistory s (D.clientHistory s p)) (he : DataStructure.Executes (P.ExecOp w) p x val y traces) : y.mem j = x.mem j

Lift a per-operation pointwise memory frame across an adaptive client execution on a deterministic specification.

theorem Cslib.WordRAM.DynamicCertificate.executes_client_modifies {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {F : Finset ℕ} (hmod : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.signature.B o} {trace : DynamicProgram.OperationTrace}, C.rep s x → D.valid s o → P.ExecOp w x o a y trace → Modifies F x.mem y.mem) {α : Type u_1} {p : D.Client α} {s : D.State} {x y : Data r} {val : α} {traces : List DynamicProgram.OperationTrace} (hr : C.rep s x) (hv : D.ValidHistory s (D.clientHistory s p)) (he : DataStructure.Executes (P.ExecOp w) p x val y traces) : Modifies F x.mem y.mem

Lift a per-operation Modifies bound across an adaptive client execution on a deterministic specification.

theorem Cslib.WordRAM.DynamicCertificate.probe_bound {r : ℕ} {D : DataStructure.StateTransitionSpec} {P : DynamicProgram D.signature r} {w : ℕ} (C : DynamicCertificate P w) (charge : D.State → D.Op → ℕ) (B : DataStructure.Bound C.impl DynamicProgram.OperationTrace.instructions charge) : DataStructure.Bound C.impl (fun (t : DynamicProgram.OperationTrace) => t.probes.length) charge

The same native evidence separately bounds memory probes by the instruction charge.