Certified local computation in memory clients

The source computation is an ordinary pure in Memory.Prog, but its native cost is the certified word-glue budget. The input domain and top-level fit envelope remain visible. Uniform emitter witnesses are chosen before the runtime environment, width or memory, including when this rule supplies the continuation of a previous memory read.

Main results

• Realizes.glue: reuse a GlueComputes emitter, preserving the entire memory and frontier.

theorem Cslib.WordRAM.Realization.Realizes.glue {B : Basis} {δ : Type} {k : ℕ} {P : (Fin k → ℕ) → Prop} {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} (input : δ ↪ Fin k → ℕ) (h : GlueComputes B P f bound time) : Realizes B (fun (d : δ) => pure (f (input d))) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ Fits w (bound (input d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => time

Certified scalar computation returns its word, frames memory/frontier/live registers, and charges its instruction budget even though its source memory-operation history is empty.