feat(WordRAM): extract static input reindexing as a leaf

Complexity.lean

@@ -2644,6 +2644,7 @@ public import Complexity.Computability.WordRAM.Realization.MemoryBackend
 public import Complexity.Computability.WordRAM.Realization.Module
 public import Complexity.Computability.WordRAM.Realization.Primitive
 public import Complexity.Computability.WordRAM.Realization.Program
+public import Complexity.Computability.WordRAM.Realization.Reindex
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.While
 public import Complexity.Computability.WordRAM.Realization.WhileAbsorb

Complexity/Computability/WordRAM/Realization/Reindex.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Realization.Basic
+
+/-!
+# 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.reindex`: pull a certificate back along a fixed register-index map.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.Realizes
+
+open Cslib.DataStructure
+
+variable {B : Basis} {ε δ α : Type} {k m l : ℕ}
+
+/-- 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. -/
+theorem reindex {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)}
+    {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop}
+    {work : δ → Memory.State → ℕ} (h : Realizes B p input output safe work)
+    (f : ε → δ) (env : ε ↪ (Fin m → ℕ)) (ix : Fin k → Fin m)
+    (hw : ∀ e i, input (f e) i = env e (ix i)) :
+    Realizes B (fun e => p (f e)) env output
+      (fun w e s => safe w (f e) s) (fun e s => work (f e) s) := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨n, C, fun frontier src tmp => emit frontier (src ∘ ix) tmp, ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  obtain ⟨hnw, hrun⟩ := he frontier (src ∘ ix) tmp hi
+    (fun i j => hd (ix i) j) hf (fun i => hs (ix i))
+  refine ⟨hnw, ?_⟩
+  intro w e x hx hin hsafe hv
+  have hin' : x.regs ∘ (src ∘ ix) = input (f e) := by
+    funext i
+    exact (congrFun hin (ix i)).trans (hw e i).symm
+  exact hrun w (f e) x hx hin' hsafe hv
+
+end Cslib.WordRAM.Realization.Realizes

ComplexityTests/WordRAMRealizationReindex.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: local-only (regression client for static input reindexing)
+
+public import Complexity.Computability.WordRAM.Realization.Primitive
+public import Complexity.Computability.WordRAM.Realization.Reindex
+
+/-!
+# Re-layout a memory read without runtime computation
+
+The original one-word read certificate selects the second word of a larger faithful
+environment. Native execution returns the maximal four-bit word, retains the unused first
+input and the entire memory/frontier, and pays the unchanged memory-query charge.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Tests.Reindex
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev environment : ℕ × ℕ ↪ (Fin 2 → ℕ) := appendWords word word
+
+private theorem readSecond :
+    Realizes .exact (fun d : ℕ × ℕ => Memory.read d.2) environment word
+      (fun _ _ _ => True) (fun _ _ => 0) :=
+  (Realizes.read word 0).reindex Prod.snd environment ![1]
+    (by intro d i; fin_cases i; rfl)
+
+/-- Reindexing preserves the unused input word and the inaccessible memory tail. -/
+theorem readSecond_native : ∃ r C, ∃ code : Code .exact r, ∃ x y : Data r,
+    ∃ result tag frontier : Fin r,
+      x.Bounded 4 ∧ x.regs tag = 7 ∧
+      ExecWithin 4 code x y (C * 2) ∧ y.regs result = 15 ∧ y.regs tag = 7 ∧
+      y.mem 100 = 5 ∧ y.regs frontier = 4 ∧ ¬code.ReadsWidth := by
+  obtain ⟨n, C, emit, he⟩ := readSecond
+  let r := 3 + (1 + n + 1)
+  let frontier : Fin r := ⟨0, by omega⟩
+  let src : Fin 2 → Fin r := fun i => ⟨1 + i.val, by omega⟩
+  let tmp : Fin (1 + n + 1) → Fin r := fun i => ⟨3 + i.val, by omega⟩
+  have hi : Function.Injective tmp := by
+    intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    dsimp only [tmp] at this
+    omega
+  have hd (i : Fin 2) (j : Fin (1 + n + 1)) : src i ≠ tmp j := by
+    intro h
+    have := congrArg Fin.val h
+    dsimp only [src, tmp] at this
+    have := i.isLt
+    omega
+  have hf (j : Fin (1 + n + 1)) : tmp j ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    dsimp only [tmp, frontier] at this
+    omega
+  have hs (i : Fin 2) : src i ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    dsimp only [src, frontier] at this
+    omega
+  let x : Data r := ⟨fun i => if i = src 0 then 7 else if i = src 1 then 2 else
+    if i = frontier then 4 else 0, fun a => if a = 2 then 15 else 5⟩
+  have hx : x.Bounded 4 := by
+    constructor
+    · intro i
+      change Fits 4 (if i = src 0 then 7 else if i = src 1 then 2 else
+        if i = frontier then 4 else 0)
+      split_ifs <;> decide
+    · intro a
+      change Fits 4 (if a = 2 then 15 else 5)
+      split_ifs <;> decide
+  have hin : x.regs ∘ src = environment (7, 2) := by
+    funext i
+    fin_cases i <;> rfl
+  have hm : memoryState frontier x =
+      (⟨fun a => if a = 2 then 15 else 5, 4⟩ : Memory.State) := rfl
+  have hv : (Memory.spec 4).ValidHistory (memoryState frontier x)
+      ((Memory.spec 4).clientHistory (memoryState frontier x) (Memory.read 2)) := by
+    rw [hm]
+    decide
+  obtain ⟨hnw, hrun⟩ := he frontier src tmp hi hd hf hs
+  obtain ⟨y, hy, hmem, hout, hframe⟩ := hrun 4 (7, 2) x hx hin trivial hv
+  rw [hm] at hy hmem hout
+  have htag := hframe (src 0) (hs 0) (fun j => (hd 0 j).symm)
+  refine ⟨r, C, emit frontier src tmp, x, y, tmp 0, src 0, frontier, hx, ?_, hy,
+    hout 0, ?_, congrArg (fun s : Memory.State => s.mem 100) hmem,
+    congrArg Memory.State.frontier hmem, hnw⟩
+  · simp [x]
+  · simpa [x] using htag
+
+end Cslib.WordRAM.Realization.Tests.Reindex