Fixed-program implementations of dynamic data structures

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 ComplexityTests/WordRAMDynamic.lean for typed stack observations, the seven-body/eight-charged push and certificate lifting, and ComplexityTests/WordRAMPrefixSums.lean for repeated calls retaining persistent data.

Main definitions

• DynamicProgram: fixed code, an input-register convention, and an output decoder.
• DynamicProgram.eval: typed call evaluation with halt-inclusive instruction cost.
• DynamicProgram.ExecOp: 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.realization: machine certificates instantiate shared adaptive execution.
• DynamicCertificate.instruction_bound: separate native instruction-cost certificates.

structure Cslib.WordRAM.DynamicProgram (D : Stateful.Spec) (r : ℕ) : Type (max v z)

A single program serving all operations through a fixed register calling convention.

• code : Code Basis.standard 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 : D.Op → Fin r → ℕ

  Encoded arguments, independent of the maintained machine state.

• decode (o : D.Op) : (Fin r → ℕ) → Option (D.Result o)

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

def Cslib.WordRAM.DynamicProgram.prepare {r : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) (o : D.Op) (x : Data r) : Data r

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

@[simp]

theorem Cslib.WordRAM.DynamicProgram.prepare_mem {r : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) (o : D.Op) (x : Data r) : (P.prepare o x).mem = x.mem

theorem Cslib.WordRAM.DynamicProgram.prepare_regs_of_not_input {r : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {i : Fin r} (hi : P.input i = false) (o : D.Op) (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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w : ℕ} {o : D.Op} {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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) (w fuel : ℕ) (o : D.Op) (x : Data r) : Option (Data r × D.Result 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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) (w : ℕ) : Stateful.Execution D (Data r) OperationTrace

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

theorem Cslib.WordRAM.DynamicProgram.ExecOp.of_eval {r : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w fuel k : ℕ} {o : D.Op} {x y : Data r} {a : D.Result 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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w : ℕ} {x y : Data r} {o : D.Op} {a : D.Result 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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w : ℕ} {x y : Data r} {o : D.Op} {a : D.Result 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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w : ℕ} {x y y' : Data r} {o : D.Op} {a a' : D.Result 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 : ℕ} {D : Stateful.Spec} {P : DynamicProgram D r} {w : ℕ} {x y z : Data r} {o : D.Op} {a : D.Result 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 : ℕ} {D : Stateful.Spec} (P : DynamicProgram D r) {w : ℕ} {x y : Data r} {o : D.Op} {a : D.Result 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 : Stateful.Spec} (P : DynamicProgram D r) (w : ℕ) : Type u

Per-operation semantic proof obligations tied to fixed bounded-word code. Performance claims are supplied separately, as Stateful.Bound 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 i = true → Fits w (P.encode 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) (n : ℕ), Exec w P.code (P.prepare o x) y n ∧ P.decode o y.regs = some (D.step s o).2 ∧ self.rep (D.step s o).1 y

  A machine execution implements an admissible operation.

theorem Cslib.WordRAM.DynamicCertificate.execOp_of_eval {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D 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.realization {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D r} {w : ℕ} (C : DynamicCertificate P w) : Stateful.Realization D (P.ExecOp w)

Fixed-program certificates realize the common dynamic specification, without choosing a cost.

theorem Cslib.WordRAM.DynamicCertificate.instruction_bound {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D 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 (P.prepare o x) y n → n + 1 ≤ charge s o) : Stateful.Bound C.realization DynamicProgram.OperationTrace.instructions charge

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

theorem Cslib.WordRAM.DynamicCertificate.instruction_bound_const {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D 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 (P.prepare o x) y n ∧ n + 1 ≤ K) : Stateful.Bound C.realization 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 : Stateful.Spec} {P : DynamicProgram D r} {w : ℕ} (C : DynamicCertificate P w) {K : ℕ} (B : Stateful.Bound C.realization 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.runClient s p).2.2) : ∃ (y : Data r) (traces : List DynamicProgram.OperationTrace), Stateful.Executes (P.ExecOp w) p x (D.runClient s p).1 y traces ∧ C.rep (D.runClient s p).2.1 y ∧ Stateful.total DynamicProgram.OperationTrace.instructions traces ≤ (D.runClient s p).2.2.length * K

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

theorem Cslib.WordRAM.DynamicCertificate.frame_of_execute {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D 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 (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 : Stateful.Spec} {P : DynamicProgram D 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 (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_client_frame {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D r} {w : ℕ} (C : DynamicCertificate P w) {j : ℕ} (hframe : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.Result 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.runClient s p).2.2) (he : Stateful.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.

theorem Cslib.WordRAM.DynamicCertificate.executes_client_modifies {r : ℕ} {D : Stateful.Spec} {P : DynamicProgram D r} {w : ℕ} (C : DynamicCertificate P w) {F : Finset ℕ} (hmod : ∀ {s : D.State} {x y : Data r} {o : D.Op} {a : D.Result 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.runClient s p).2.2) (he : Stateful.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.

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

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