feat(realize): reuse certified method calls and complete linked runs

Complexity.lean

@@ -3065,6 +3065,7 @@ public import Complexity.DataStructure.StateTransition.Composition
 public import Complexity.DataStructure.StateTransition.CostHoare
 public import Complexity.DataStructure.StateTransition.Hoare
 public import Complexity.DataStructure.StateTransition.Impl
+public import Complexity.DataStructure.StateTransition.LinkCongr
 public import Complexity.DataStructure.StateTransition.Module
 public import Complexity.DataStructure.StateTransition.Oracle
 public import Complexity.DataStructure.StateTransition.Randomized

Complexity/DataStructure/StateTransition/LinkCongr.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.DataStructure.StateTransition.Module
+
+/-!
+# Linking methods with identical complete runs
+
+Changing a method's source syntax preserves a linked adaptive client when every method keeps
+its complete deterministic run: result, final state and lower-operation history. Equality of
+answers alone would not preserve the reached memories or the subsequent client behavior.
+
+## Main results
+
+* `StateTransitionSpec.runClient_link_congr`: equality of complete method runs lifts to every
+  adaptive client, retaining the entire lower-operation history and final state.
+
+This is a semantic transport result. It assigns no native cost to calling or argument staging;
+equal histories can be used with the existing `totalCost` function at any chosen charge.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.StateTransitionSpec
+
+universe u v w
+
+variable {D E : StateTransitionSpec.{u, v, w}}
+  {f : (s : E.State) → (o : E.Op) → E.State × E.Result o} [E.HasStepFn f]
+  {α : Type w}
+
+/-- Methods with identical complete deterministic runs can replace one another under linking.
+The equality retains the lower history, including operations of every reached continuation. -/
+theorem runClient_link_congr (methods methods' : Methods D E)
+    (hmethods : ∀ s o, E.runClient s (methods o) = E.runClient s (methods' o))
+    (p : D.Client α) (s : E.State) :
+    E.runClient s (link methods p) = E.runClient s (link methods' p) := by
+  induction p generalizing s with
+  | pure a => rfl
+  | liftBind o k ih =>
+    change E.runClient s ((methods o).bind fun a => link methods (k a)) =
+      E.runClient s ((methods' o).bind fun a => link methods' (k a))
+    rw [E.runClient_bind, E.runClient_bind, hmethods s o]
+    exact congrArg (fun r : α × E.State × List E.Op =>
+      (r.1, r.2.1, (E.runClient s (methods' o)).2.2 ++ r.2.2))
+      (ih (E.runClient s (methods' o)).1 (E.runClient s (methods' o)).2.1)
+
+end Cslib.DataStructure.StateTransitionSpec

Complexity/Tactic/Realize.lean

@@ -8,10 +8,14 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.WordRAM.Realization.WhileAbsorb
+public import Complexity.Computability.WordRAM.Realization.Reindex
 
 /-!
 # The `realize` tactic
 
+The tactic is available inside `Cslib.WordRAM`, or after `open Cslib.WordRAM` or
+`open scoped Cslib.WordRAM`. Importing this module alone does not activate its syntax.
+
 `realize` proves a goal `Realizes B p input output safe work` for a memory client `p`. It walks
 the client syntax, unfolding definitions, with one rule per form:
 
@@ -21,6 +25,8 @@ the client syntax, unfolding definitions, with one rule per form:
   from the closure rules of `Complexity.Computability.WordRAM.Glue`: projections, constants, and
   the exact- or standard-basis arithmetic and bitwise operations.
 * the four memory queries: `Realizes.read`, `write`, `alloc` and `allocDirty`.
+* a method with a local zero-work `Realizes` certificate: `Realizes.reindex`, selecting its
+  arguments from live words before unfolding its implementation.
 * `if` on `a = b`, `a < b` or `a > b`: `Realizes.branch₀`.
 * `match` on an optional word or word pair: the client equals the branch on its presence tag
   (`Realizes.congr`, proved by cases).
@@ -53,7 +59,10 @@ updated memories, or the interpreter's result of a called method; a loop contrib
 After the composition, `realize` introduces `w d s hwords hmem h`: the word width, the
 environment, the memory, the fit of the input words, memory well-formedness, and the goal's
 domain. It splits the conjunctions and `if`s of the synthesized domain and leaves each remaining
-condition as a goal. There is no search: an unsupported form is reported with its subterm.
+condition as a goal. Local method certificates are tried in context order; the remaining rule
+selection follows the client syntax, without searching for bounds. An unsupported form is
+reported with its subterm. A called method's arguments must already be live words; computed
+arguments need an explicit `pure` step, whose glue is certified and charged as usual.
 
 Each certificate is stated for the client form as written, with its domain in the client's terms
 (`certify`), so certificates compose syntactically. A bind's continuation domain is stated at the
@@ -719,13 +728,82 @@ private def bindRun (hP hQ reply next : Expr) : MetaM Expr := do
     lambdaBoundedTelescope f 2 fun xs b => do mkLambdaFVars xs (← mkEqRefl b)
   mkAppM ``Realizes.bind₀_of_run #[hP, hQ, reply, next, ← refl reply, ← refl next]
 
+/-- Expose pair projections to unification when a certificate packages curried arguments.
+Other types remain whole metavariables: no data constructor or runtime value is guessed. -/
+private partial def callArgument (ty : Expr) : MetaM Expr := do
+  let ty ← whnfR ty
+  if let some (a, b) := ty.app2? ``Prod then
+    return mkAppN (mkConst ``Prod.mk ty.getAppFn.constLevels!)
+      #[a, b, ← callArgument a, ← callArgument b]
+  if let some (a, b) := ty.app2? ``Sigma then
+    let x ← callArgument a
+    return mkAppN (mkConst ``Sigma.mk ty.getAppFn.constLevels!)
+      #[a, b, x, ← callArgument (b.beta #[x])]
+  mkFreshExprMVar ty
+
+/-- Reuse a local method certificate before unfolding its body. Every input word must already
+be live: `Realizes.reindex` supplies static wiring, without granting argument computation. -/
+private def tryRealizeCall (ctx : Ctx) (env : Env) (d : Expr) (atoms : Array Expr)
+    (body : Expr) (output? : Option Expr) : TermElabM (Option Out) := do
+  for decl in ← getLCtx do
+    if decl.isImplementationDetail then continue
+    let ty ← instantiateMVars decl.type
+    unless ty.isAppOfArity ``Realizes 10 do continue
+    let saved ← saveState
+    try
+      let args := ty.getAppArgs
+      unless ← withReducible (isDefEq args[4]! ctx.basis) do
+        throwError "realize: the method's basis differs"
+      unless ← withReducible (isDefEq args[9]! (← zeroWork args[2]!)) do
+        throwError "realize: a called certificate must have absorbed local work"
+      let arg ← callArgument args[2]!
+      let called := (mkApp args[5]! arg).headBeta
+      -- Solve dependent arguments in binder order without unfolding a matching method head.
+      let matched ← if called.getAppFn == body.getAppFn &&
+          called.getAppNumArgs == body.getAppNumArgs then
+          (called.getAppArgs.zip body.getAppArgs).allM fun (a, b) => do
+            withReducible (isDefEq (← whnfR a) (← whnfR b))
+        else withReducible (isDefEq called body)
+      unless matched do
+        throwError "realize: the method does not match"
+      let arg ← instantiateMVars arg
+      if arg.hasMVar then throwError "realize: the method argument is undetermined"
+      let out ← checkOutput decl.toExpr output?
+      let k ← encodingWidth args[6]!
+      let coords ← encodingAtoms args[6]! arg k
+      let positions ← coords.mapM fun a => do
+        let some i ← findAtom atoms a
+          | throwError "realize: a method argument must first be computed into a live word"
+        pure i
+      let finK := mkApp (mkConst ``Fin) (mkNatLit k)
+      let finEnv := mkApp (mkConst ``Fin) (mkNatLit env.k)
+      let rec indices : List Nat → MetaM Expr
+        | [] => mkAppOptM ``Matrix.vecEmpty #[finEnv]
+        | i :: is => do mkAppM ``Matrix.vecCons #[← finLit env.k i, ← indices is]
+      let ix ← indices positions.toList
+      let f ← mkLambdaFVars #[d] arg
+      let hwTy ← withLocalDeclD `e env.ty fun e => withLocalDeclD `i finK fun i => do
+        let lhs := mkApp (← mkAppM ``DFunLike.coe #[args[6]!, f.beta #[e]]) i
+        let rhs := mkApp (← mkAppM ``DFunLike.coe #[env.input, e]) (mkApp ix i)
+        mkForallFVars #[e, i] (← mkEq lhs rhs)
+      let hw ← proveResult hwTy k
+      let proof ← mkAppM ``Realizes.reindex #[decl.toExpr, f, env.input, ix, hw]
+      let safe ← withLocalDeclD `w (mkConst ``Nat) fun w =>
+        withLocalDeclD `s (mkConst ``Memory.State) fun s => do
+          mkLambdaFVars #[w, d, s] (← reducePairs (mkApp3 args[8]! w arg s))
+      return some { proof, output := out, safe }
+    catch _ => saved.restore
+  return none
+
 mutual
 
 /-- Certify a client `prog : δ → Memory.Prog α` in the environment `env`. -/
 private partial def realizeProg (ctx : Ctx) (env : Env) (prog : Expr) (output? : Option Expr) :
     TermElabM Out :=
   withLocalDeclD `d env.ty fun d => do
     let atoms := env.atoms.map (·.beta #[d])
+    if let some out ← tryRealizeCall ctx env d atoms (prog.beta #[d]).headBeta output? then
+      return { out with proof := ← certify ctx env out.proof prog out.output out.safe }
     let body ← normBody (prog.beta #[d]).headBeta
     let out ← realizeBody ctx env d atoms body output?
     return { out with proof := ← certify ctx env out.proof prog out.output out.safe }
@@ -1113,10 +1191,12 @@ private partial def splitDomain (g : MVarId) : MetaM (List MVarId) := g.withCont
 
 end Cslib.Tactic.Realize
 
+namespace Cslib.WordRAM
+
 open Lean Meta Elab Tactic Cslib.WordRAM Cslib.WordRAM.Realization Cslib.Tactic.Realize in
 /-- Prove `Realizes B p input output safe work` for a memory client `p`, leaving the genuine fit
 and domain conditions as goals in the context `w d s hwords hmem h`. -/
-elab "realize" : tactic => withMainContext do
+scoped elab "realize" : tactic => withMainContext do
   let goal ← getMainGoal
   let target ← instantiateMVars (← whnfR (← goal.getType))
   unless target.isAppOfArity ``Realizes 10 do
@@ -1163,3 +1243,5 @@ elab "realize" : tactic => withMainContext do
     | some g' => g.assign (mkMVar g')
     | none => kept := kept.push g
   setGoals kept.toList
+
+end Cslib.WordRAM

ComplexityTests/StateTransitionLinkCongr.lean

@@ -0,0 +1,48 @@
+/-
+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 (complete linked-run transport regressions)
+
+public import Complexity.DataStructure.Memory.Spec
+public import Complexity.DataStructure.StateTransition.LinkCongr
+
+/-! Complete method runs preserve adaptive replies, changed memory and the selected history.
+An extra read has the same result and final state but a different charged history. -/
+
+public section
+
+namespace Cslib.DataStructure.Tests.LinkCongr
+
+/-- Replacing every method by a result-staging wrapper preserves the complete adaptive run. -/
+theorem linked_write_read (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).runClient s
+      (link (D := Memory.spec w) (E := Memory.spec w)
+        (fun o => do let a ← PFunctor.FreeM.lift o; pure a)
+        (do let v ← Memory.read 1; Memory.write 2 (v + 1); Memory.read 2)) =
+      (s.mem 1 + 1, ⟨Function.update s.mem 2 (s.mem 1 + 1), s.frontier⟩,
+        [Memory.Op.read 1, Memory.Op.write 2 (s.mem 1 + 1), Memory.Op.read 2]) := by
+  have hmethods : ∀ t (o : Memory.Op),
+      (Memory.spec w).runClient t (PFunctor.FreeM.lift o) =
+        (Memory.spec w).runClient t (do let a ← PFunctor.FreeM.lift o; pure a) := by
+    intro t o
+    change (Memory.spec w).runClient t (PFunctor.FreeM.lift o) =
+      (Memory.spec w).runClient t ((PFunctor.FreeM.lift o).bind fun a => .pure a)
+    rw [StateTransitionSpec.runClient_bind]
+    rfl
+  rw [← StateTransitionSpec.runClient_link_congr _ _ hmethods]
+  rfl
+
+-- Keeping the answer and final state alone is insufficient: the lower history differs.
+example (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).runClient s (Memory.read 1) ≠
+      (Memory.spec w).runClient s (do let _ ← Memory.read 1; Memory.read 1) := by
+  intro h
+  have hlength := congrArg (fun r : ℕ × Memory.State × List Memory.Op => r.2.2.length) h
+  change 1 = 2 at hlength
+  omega
+
+end Cslib.DataStructure.Tests.LinkCongr

ComplexityTests/WordRAMRealizationCall.lean

@@ -0,0 +1,145 @@
+/-
+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 (realize certificate-call regression tests)
+
+public import Complexity.Tactic.Realize
+
+/-!
+# Calls to separately certified memory methods
+
+The methods are parameters, so their implementations cannot be unfolded. Calls select existing
+live words, may alias inputs, and carry their method domain to the reached memory. Argument
+computation requires an explicit, charged glue step.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Tests.Call
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev pairWords : ℕ × ℕ ↪ (Fin 2 → ℕ) := appendWords word word
+private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+-- A separately certified method consumes a projection of a larger live environment.
+theorem projection_call (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m (WordEncoding.encode (α := ℕ)) (WordEncoding.encode (α := ℕ))
+      P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => m d.2) (WordEncoding.encode (α := ℕ × ℕ))
+      (WordEncoding.encode (α := ℕ)) (fun w d s => P w d.2 s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A tuple-argument certificate can certify a curried method without unfolding its body.
+example (m : ℕ → ℕ → Memory.Prog ℕ) (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : ℕ × ℕ => m d.1 d.2) pairWords word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => m d.2 d.1) pairWords word
+      (fun w d s => P w (d.2, d.1) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A curried opaque extraction feeds the canonical three-word optional-pair continuation.
+example (extract : ℕ → ℕ → Memory.Prog (Option (ℕ × ℕ)))
+    (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : ℕ × ℕ => extract d.1 d.2) pairWords
+      (WordEncoding.encode (α := Option (ℕ × ℕ))) P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      match ← extract d.2 d.1 with
+      | none => pure (0, 0)
+      | some (v, k) => pure (v, k)) pairWords pairWords
+      (fun w d s => P w (d.2, d.1) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A small faithful dependent-index fixture pins the actual staged-call failure.
+private def indexedWords : (Σ n : ℕ, Fin n) ↪ (Fin 2 → ℕ) where
+  toFun d := ![d.1, d.2.val]
+  inj' := by
+    rintro ⟨n, i⟩ ⟨m, j⟩ h
+    have hn : n = m := congrFun h 0
+    subst m
+    have hi : i = j := Fin.ext (congrFun h 1)
+    cases hi
+    rfl
+
+private abbrev IndexedArgument := ((Σ n : ℕ, Fin n) × ℕ) × ℕ
+private abbrev indexedInput : IndexedArgument ↪ (Fin 4 → ℕ) :=
+  appendWords (appendWords indexedWords word) word
+
+-- The implicit index must be solved before its dependent argument after charged pair staging.
+example (m : {n : ℕ} → Fin n → ℕ → ℕ → Memory.Prog Unit)
+    (P : ℕ → IndexedArgument → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : IndexedArgument => m d.1.1.2 d.1.2 d.2)
+      indexedInput unitWords P (fun _ _ => 0)) :
+    Realizes .exact (fun d : IndexedArgument => do
+      let a ← pure (d.1.2, d.2)
+      m d.1.1.2 a.1 a.2) indexedInput unitWords P (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- Scalar staging also charges the subtraction and constant before entering the method domain.
+example (m : {n : ℕ} → Fin n → ℕ → ℕ → Memory.Prog Unit)
+    (P : ℕ → IndexedArgument → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : IndexedArgument => m d.1.1.2 d.1.2 d.2)
+      indexedInput unitWords P (fun _ _ => 0)) :
+    Realizes .exact (fun d : IndexedArgument => do
+      let size ← pure (d.1.2 - 1)
+      let start ← pure 1
+      m d.1.1.2 size start) indexedInput unitWords
+      (fun w d s => 1 ≤ d.1.2 ∧ P w ((d.1.1, d.1.2 - 1), 1) s)
+      (fun _ _ => 0) := by
+  realize <;> first | exact h.1 | exact h.2 | exact (hwords 2).of_le h.1
+
+-- Input registers need not be distinct: the existing reindex rule permits aliasing.
+example (m : ℕ × ℕ → Memory.Prog ℕ) (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m pairWords word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ => m (d, d)) word word
+      (fun w d s => P w (d, d) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- The returned word is live in the continuation, without revealing the method body.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      let a ← m d.1
+      Memory.write d.2 a) pairWords unitWords
+      (fun w d s => P w d.1 s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A call's domain is required at the actual state reached after a write.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      Memory.write d.1 d.2
+      m d.2) pairWords word
+      (fun w d s => P w d.2 ⟨Function.update s.mem d.1 d.2, s.frontier⟩)
+      (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- An arithmetic argument cannot be passed by free static rewiring.
+example (m : ℕ → Memory.Prog ℕ)
+    (_hm : Realizes .exact m word word (fun _ _ _ => True) (fun _ _ => 0)) : True := by
+  fail_if_success
+    have _ : Realizes .exact (fun d : ℕ => m (d + 1)) word word
+        (fun _ _ _ => True) (fun _ _ => 0) := by realize
+  trivial
+
+-- Its explicit pure step is certified glue; the fitting arithmetic result stays visible.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ => do
+      let a ← pure (d + 1)
+      m a) word word
+      (fun w d s => Fits w (d + 1) ∧ P w (d + 1) s) (fun _ _ => 0) := by
+  realize <;> first | exact h.1 | exact h.2
+
+end Cslib.WordRAM.Realization.Tests.Call