Static live-register wiring #
A realization may consume selected words of a larger faithful environment without executing any computation. The equality of encoded inputs is explicit, and the register selection is fixed before runtime. This supplies layout arguments and query replies to existing method certificates while keeping other live words framed.
Main results #
Realizes.Spec.reindex,Realizes.reindex: pull a specified contract or certificate back along a fixed register-index map.
theorem Cslib.WordRAM.Realization.Realizes.Spec.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 : Spec 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)) :
Rewire a specified emitter's inputs by a fixed index map. The scratch size and exchange factor are unchanged; the semantic map must agree with that wiring on every encoded input.
theorem Cslib.WordRAM.Realization.Realizes.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 : Realizes 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)) :
Realizes 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
A fixed input-index map merely rewires registers. The semantic map must agree with that wiring on every encoded input; no host computation or runtime choice of code is granted.