Graded realization of memory-oracle clients

Realization.Realizes certifies one uniform native emitter for an existing Memory.Prog family. Arguments and results have explicit faithful finite-register encodings. Its memory abstraction is the entire memory function together with one frontier register; scratch consists only of fresh registers. The entry predicate and local-work charge are visible parameters.

The charged currency adds certified local computation and control work to Memory.charge. In particular, a query-free loop cannot acquire a constant instruction bound merely because its memory history is empty. The emitter, scratch size and exchange constant precede every runtime argument, word width and initial memory. Refines is a semantic projection of this certificate, not a competing execution semantics or a second client language.

Main definitions

• memoryState: the functional whole-memory/frontier abstraction.
• memoryCost: the memory-level charge of the client's actual deterministic history.
• Realizes: uniform native realization with a combined instruction currency and register frame.
• Realizes.SpecBounded, RealizesBounded: frontier-bounded strengthening certifying ExecBounded w (y.regs frontier) for lifting to the Resizable Word RAM.

Main results

• Realizes.Spec.consequence, Realizes.consequence: strengthen the domain or enlarge work.
• Realizes.exists_refines: forget the fresh-register frame to the existing Refines API.
• RealizesBounded.toRealizes: erase the frontier-access bound back to Realizes.

The realization certificate and its grading are original infrastructure. The memory interface, free-monad interpreter and native execution rules are reused unchanged.

def Cslib.WordRAM.Realization.memoryState {r : ℕ} (frontier : Fin r) (x : Data r) : DataStructure.Memory.State

The abstraction retains every cell, including unallocated and inaccessible cells.

theorem Cslib.WordRAM.Realization.wellFormed_memoryState {r w : ℕ} {frontier : Fin r} {x : Data r} (hx : Data.Bounded w x) : DataStructure.Memory.WellFormed w (memoryState frontier x)

Bounded native data supplies the memory invariant, independently of any scratch layout.

def Cslib.WordRAM.Realization.memoryCost {α : Type} (p : DataStructure.Memory.Prog α) (s : DataStructure.Memory.State) : ℕ

The memory-level instruction currency uses the existing deterministic interpreter. Its transition function does not depend on the word width; admissibility is a separate premise.

theorem Cslib.WordRAM.Realization.runClient_width {α : Type} (w : ℕ) (p : DataStructure.Memory.Prog α) (s : DataStructure.Memory.State) : (DataStructure.Memory.spec w).runClient s p = (DataStructure.Memory.spec 0).runClient s p

Uniformity of the mathematical interpreter across widths: only valid depends on w.

theorem Cslib.WordRAM.Realization.clientResult_width {α : Type} (w : ℕ) (p : DataStructure.Memory.Prog α) (s : DataStructure.Memory.State) : (DataStructure.Memory.spec w).clientResult s p = (DataStructure.Memory.spec 0).clientResult s p

The result of the memory interpreter is independent of the admissibility width.

theorem Cslib.WordRAM.Realization.clientState_width {α : Type} (w : ℕ) (p : DataStructure.Memory.Prog α) (s : DataStructure.Memory.State) : (DataStructure.Memory.spec w).clientState s p = (DataStructure.Memory.spec 0).clientState s p

The final memory/frontier state is independent of the admissibility width.

theorem Cslib.WordRAM.Realization.validHistory_bind (w : ℕ) {α β : Type} (p : DataStructure.Memory.Prog α) (q : α → DataStructure.Memory.Prog β) (s : DataStructure.Memory.State) : (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (PFunctor.FreeM.bind p q)) ↔ (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s p) ∧ (DataStructure.Memory.spec w).ValidHistory ((DataStructure.Memory.spec w).clientState s p) ((DataStructure.Memory.spec w).clientHistory ((DataStructure.Memory.spec w).clientState s p) (q ((DataStructure.Memory.spec w).clientResult s p)))

Admissible sequential histories split at the actual returned value and memory state.

def Cslib.WordRAM.Realization.appendWords {k l : ℕ} {δ α : Type} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) : δ × α ↪ Fin (k + l) → ℕ

Faithfully append a returned word vector to the original input environment. This is static register wiring; it performs no native computation or copies.

@[simp]

theorem Cslib.WordRAM.Realization.memoryCost_pure {α : Type} (a : α) (s : DataStructure.Memory.State) : memoryCost (pure a) s = 0

A semantic return issues no memory operation. Its native glue is charged separately.

theorem Cslib.WordRAM.Realization.memoryCost_bind {α β : Type} (p : DataStructure.Memory.Prog α) (q : α → DataStructure.Memory.Prog β) (s : DataStructure.Memory.State) : memoryCost (PFunctor.FreeM.bind p q) s = memoryCost p s + memoryCost (q ((DataStructure.Memory.spec 0).clientResult s p)) ((DataStructure.Memory.spec 0).clientState s p)

Memory charges add at the actual intermediate state; the local bind charge is separate.

theorem Cslib.WordRAM.Realization.memoryCost_bind' {α β : Type} (p : DataStructure.Memory.Prog α) (q : α → DataStructure.Memory.Prog β) (s : DataStructure.Memory.State) : memoryCost (p >>= q) s = memoryCost p s + memoryCost (q ((DataStructure.Memory.spec 0).clientResult s p)) ((DataStructure.Memory.spec 0).clientState s p)

memoryCost_bind stated with >>=, the form do blocks elaborate to.

def Cslib.WordRAM.Realization.Realizes.Spec {k l : ℕ} {δ α : Type} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) (n C : ℕ) (emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r) : Prop

The execution contract for specified scratch, exchange factor and emitter. Both the existential judgment and data witnesses use this same contract.

def Cslib.WordRAM.Realization.Realizes {k l : ℕ} {δ α : Type} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) : Prop

Existing Memory.Prog clients have a fixed emitter and a combined charge. The explicit safe predicate may contain glue domains and fit envelopes; it is never existentially chosen. The existing valid-history premise supplies memory admissibility. The extra one pays uniform entry/exit overhead, so the native bound is C * charged + C with one fixed C.

Input registers may alias each other. The injective scratch bank is disjoint from all inputs and the frontier; its first l registers hold the faithfully encoded result. Every other register, except the frontier, is framed. All native registers and memory are bounded at entry, separately from the functional representation.

theorem Cslib.WordRAM.Realization.Realizes.Spec.consequence {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work' : δ → DataStructure.Memory.State → ℕ} {n C : ℕ} {emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r} (he : Spec B p input output safe work n C fun {r : ℕ} => emit) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → safe' w d s → safe w d s) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ work' d s) : Spec B p input output safe' work' n C fun {r : ℕ} => emit

Strengthen the visible entry domain or enlarge the local-work charge for a specified scratch size, exchange factor and emitter, all of which are unchanged.

theorem Cslib.WordRAM.Realization.Realizes.consequence {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work' : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → safe' w d s → safe w d s) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ work' d s) : Realizes B p input output safe' work'

Strengthen the visible entry domain or enlarge the local-work charge. The entry word and memory bounds may discharge fit conditions; no executable code or domain is hidden by this rule.

theorem Cslib.WordRAM.Realization.Realizes.mapSimulates {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {B' : Basis} (h : Realizes B p input output safe work) (φ : B.Simulates B') : Realizes B' p input output safe work

Existing defined-evaluation basis simulation preserves the complete realization certificate.

theorem Cslib.WordRAM.Realization.Realizes.exists_refines {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) : ∃ (n : ℕ) (C : ℕ) (emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r), ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) (tmp : Fin (l + n + 1) → Fin r), Function.Injective tmp → (∀ (i : Fin k) (j : Fin (l + n + 1)), src i ≠ tmp j) → (∀ (j : Fin (l + n + 1)), tmp j ≠ frontier) → (∀ (i : Fin k), src i ≠ frontier) → ∀ (w : ℕ) (d : δ), Refines w (fun (s : (DataStructure.Memory.spec w).State) (x : Data r) => s = memoryState frontier x ∧ Data.Bounded w x ∧ x.regs ∘ src = input d ∧ safe w d s ∧ (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (p d))) (p d) (fun (a : α) (s : (DataStructure.Memory.spec w).State) (y : Data r) => memoryState frontier y = s ∧ ∀ (i : Fin l), y.regs (tmp (Fin.castAdd (n + 1) i)) = output a i) (fun (s : (DataStructure.Memory.spec w).State) (x : Data r) => C * (memoryCost (p d) s + work d s + 1)) (emit frontier src tmp)

The same witness derives the existing semantic Refines judgment. The intermediate representation is fixed by the functional memory abstraction and argument/result registers.

def Cslib.WordRAM.Realization.Realizes.SpecBounded {k l : ℕ} {δ α : Type} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) (n C : ℕ) (emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r) : Prop

Frontier-bounded execution contract strengthening Realizes.Spec with ExecBounded w (y.regs frontier).

theorem Cslib.WordRAM.Realization.Realizes.SpecBounded.toSpec {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {n C : ℕ} {emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r} (he : SpecBounded B p input output safe work n C fun {r : ℕ} => emit) : Spec B p input output safe work n C fun {r : ℕ} => emit

Erase the frontier-access bound from SpecBounded back to Spec.

theorem Cslib.WordRAM.Realization.Realizes.SpecBounded.consequence {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work' : δ → DataStructure.Memory.State → ℕ} {n C : ℕ} {emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r} (he : SpecBounded B p input output safe work n C fun {r : ℕ} => emit) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → safe' w d s → safe w d s) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ work' d s) : SpecBounded B p input output safe' work' n C fun {r : ℕ} => emit

Strengthen the visible entry domain or enlarge the local-work charge for SpecBounded.

def Cslib.WordRAM.Realization.RealizesBounded {k l : ℕ} {δ α : Type} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) : Prop

Uniform frontier-bounded realization of a Memory.Prog family, certifying that every native load and store accesses an address strictly below y.regs frontier.

theorem Cslib.WordRAM.Realization.RealizesBounded.toRealizes {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B p input output safe work) : Realizes B p input output safe work

Erase the frontier-access bound back to Realizes.

theorem Cslib.WordRAM.Realization.RealizesBounded.consequence {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work' : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → safe' w d s → safe w d s) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ work' d s) : RealizesBounded B p input output safe' work'

Strengthen the visible entry domain or enlarge the local-work charge.

theorem Cslib.WordRAM.Realization.RealizesBounded.mapSimulates {B : Basis} {k l : ℕ} {δ α : Type} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {B' : Basis} (h : RealizesBounded B p input output safe work) (φ : B.Simulates B') : RealizesBounded B' p input output safe work

Transport a frontier-bounded realization certificate along a basis simulation.

theorem Cslib.WordRAM.Realization.Realizes.SpecBounded.reindex {B : Basis} {ε δ α : Type} {k m l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {n C : ℕ} {emit : {r : ℕ} → Fin r → (Fin k → Fin r) → (Fin (l + n + 1) → Fin r) → Code B r} (he : SpecBounded B p input output safe work n C fun {r : ℕ} => emit) (f : ε → δ) (env : ε ↪ Fin m → ℕ) (ix : Fin k → Fin m) (hw : ∀ (e : ε) (i : Fin k), input (f e) i = env e (ix i)) : SpecBounded B (fun (e : ε) => p (f e)) env output (fun (w : ℕ) (e : ε) (s : DataStructure.Memory.State) => safe w (f e) s) (fun (e : ε) (s : DataStructure.Memory.State) => work (f e) s) n C fun {r : ℕ} (frontier : Fin r) (src : Fin m → Fin r) (tmp : Fin (l + n + 1) → Fin r) => emit frontier (src ∘ ix) tmp

Rewire a SpecBounded emitter's inputs by a fixed index map.

theorem Cslib.WordRAM.Realization.RealizesBounded.reindex {B : Basis} {ε δ α : Type} {k m l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B p input output safe work) (f : ε → δ) (env : ε ↪ Fin m → ℕ) (ix : Fin k → Fin m) (hw : ∀ (e : ε) (i : Fin k), input (f e) i = env e (ix i)) : RealizesBounded B (fun (e : ε) => p (f e)) env output (fun (w : ℕ) (e : ε) (s : DataStructure.Memory.State) => safe w (f e) s) fun (e : ε) (s : DataStructure.Memory.State) => work (f e) s

Pull a RealizesBounded certificate back along a fixed register-index map.

theorem Cslib.WordRAM.Realization.RealizesBounded.mono_mul {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work work' : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B p input output safe work) (K : ℕ) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ K * (memoryCost (p d) s + work' d s + 1)) : RealizesBounded B p input output safe work'

Absorb local work dominated by a constant multiple of the memory charge plus another grading.

theorem Cslib.WordRAM.Realization.RealizesBounded.congr {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {p' : δ → DataStructure.Memory.Prog α} (h : RealizesBounded B p input output safe work) (hp : ∀ (d : δ), p d = p' d) : RealizesBounded B p' input output safe work

Pointwise equal programs have the same frontier-bounded certificates.

theorem Cslib.WordRAM.Realization.RealizesBounded.consequence_valid {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} (h : RealizesBounded B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (p d)) → safe' w d s → safe w d s) : RealizesBounded B p input output safe' work

Strengthen the visible domain under the client's own valid history.