feat(WordRAM/Realization): randomized realization of memory clients with coins (#2205 K1)

Complexity.lean

@@ -2655,6 +2655,8 @@ 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.Program.Standard
+public import Complexity.Computability.WordRAM.Realization.Random
+public import Complexity.Computability.WordRAM.Realization.RandomLoop
 public import Complexity.Computability.WordRAM.Realization.Reindex
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.While

Complexity/Computability/WordRAM/Randomized/Law.lean

@@ -44,6 +44,9 @@ with `f` (`Cslib.WordRAM.ExecRandLaw.program`).
   `Cslib.WordRAM.ExecRandLaw.loop_iter`: composition rules.
 * `Cslib.WordRAM.ExecRandLaw.rename`: renaming registers.
 * `Cslib.WordRAM.ExecRandLaw.execRandWithin`: forgetting the law.
+* `Cslib.WordRAM.ExecRandLaw.map`, `Cslib.WordRAM.ExecRandLaw.withBounded`,
+  `Cslib.WordRAM.ExecRandLaw.withSupport`: mapping the observation, and the boundedness and the
+  support of every final observation.
 * `Cslib.WordRAM.ExecRandLaw.program`: the compiled program halts within the bound, respects the
   call budget and the postcondition, and has the law `μ`.
 -/
@@ -83,6 +86,28 @@ theorem congr_law {μ' : PMF α} (h : ExecRandLaw w c x P T R f μ) (hμ : μ =
     ExecRandLaw w c x P T R f μ' :=
   hμ ▸ h
 
+/-- Post-composing the observation with `g` maps the law by `g`. -/
+theorem map (h : ExecRandLaw w c x P T R f μ) (g : α → β) :
+    ExecRandLaw w c x P T R (fun y => g (f y)) (μ.map g) := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  refine ⟨m, hm, hq, hsup, ?_⟩
+  rw [← hlaw, ProbComp.eval_map, ProbComp.eval_map, PMF.map_comp]
+  rfl
+
+/-- Strengthening the postcondition with word-boundedness, from bounded initial data. -/
+theorem withBounded (h : ExecRandLaw w c x P T R f μ) (hx : x.Bounded w) :
+    ExecRandLaw w c x (fun y => P y ∧ y.Bounded w) T R f μ := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  exact ⟨m, hm, hq, fun z hz => ⟨⟨(hsup z hz).1, hm.bounded hx hz⟩, (hsup z hz).2⟩, hlaw⟩
+
+/-- Strengthening the postcondition: every final observation lies in the support of the law. -/
+theorem withSupport (h : ExecRandLaw w c x P T R f μ) :
+    ExecRandLaw w c x (fun y => P y ∧ f y ∈ μ.support) T R f μ := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  refine ⟨m, hm, hq, fun z hz => ⟨⟨(hsup z hz).1, ?_⟩, (hsup z hz).2⟩, hlaw⟩
+  rw [← hlaw, ProbComp.eval_map, PMF.support_map, ProbComp.support_eval]
+  exact ⟨z, hz, rfl⟩
+
 /-- Strengthening the postcondition with a register that `c` never writes. -/
 theorem withPreserves {i : Fin r} (h : ExecRandLaw w c x P T R f μ) (hi : c.Preserves i) :
     ExecRandLaw w c x (fun y => P y ∧ y.regs i = x.regs i) T R f μ := by

Complexity/Computability/WordRAM/Realization/Bind.lean

@@ -18,6 +18,10 @@ Its source registers append the first computation's answer slots to the original
 Two disjoint static scratch banks preserve that environment without client-written intermediate
 assertions. The continuation's bank already contains the final output slots, so no copy is needed.
 
+## Main definitions
+
+* `bindLeft`, `bindRight`: the two scratch banks inside a sequential composition's bank.
+
 ## Main results
 
 * `Realizes.bind`: sequential realization with additive memory and local-work charges.
@@ -29,10 +33,14 @@ namespace Cslib.WordRAM.Realization
 
 open Cslib.DataStructure
 
-private def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) :
+/-- The continuation's scratch bank inside a sequential composition's bank: its first slots, so
+its result slots are the composition's. -/
+def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) :
     Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨i.val, by omega⟩
 
-private def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) :
+/-- The first computation's scratch bank inside a sequential composition's bank, after the
+continuation's. -/
+def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) :
     Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨m + n₂ + 1 + i.val, by omega⟩
 
 namespace Realizes

Complexity/Computability/WordRAM/Realization/Branch.lean

@@ -22,6 +22,7 @@ The two-instruction allowance includes the jump on the negative path.
 
 ## Main results
 
+* `test_rename`: a renamed native condition tests the words in its source registers.
 * `Realizes.branch`: compose two realizations using an actual native conditional.
 -/
 
@@ -40,7 +41,9 @@ instance (c : Cond k) (v : Fin k → ℕ) : Decidable (test c v) := by
   unfold test
   infer_instance
 
-private theorem test_rename {r : ℕ} (c : Cond k) (src : Fin k → Fin r)
+/-- A renamed condition holds of native data exactly when it holds of the words in its source
+registers. -/
+theorem test_rename {r : ℕ} (c : Cond k) (src : Fin k → Fin r)
     (x : Data r) (v : Fin k → ℕ) (h : x.regs ∘ src = v) :
     (c.rename src).Holds x ↔ test c v := by
   cases c <;> simp only [Cond.rename, Cond.Holds, test] <;>

Complexity/Computability/WordRAM/Realization/Loop.lean

@@ -20,6 +20,8 @@ uses one fixed body emitter and static registers for the mutable state and count
 
 * `iterate`: bounded iteration in the existing memory-client monad.
 * `iterationWork`, `iterationSafe`: local work and domains along the actual semantic states.
+* `loopEmit`, `loopBody`: the native loop with a fixed body emitter, and one native iteration,
+  over the register bank `stateSlot`, `counterSlot`, `zeroSlot`, `oneSlot`, `bodySlot`.
 
 ## Main results
 
@@ -192,17 +194,24 @@ theorem iterationSum_eq (body : δ × σ → Memory.Prog σ)
     dsimp only [iterationStep] at *
     omega
 
-private def stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1) :=
+/-- The loop's state words, which are also its result slots. -/
+def stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1) :=
   ⟨i.val, by omega⟩
 
-private def counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l, by omega⟩
-private def zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 1, by omega⟩
-private def oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 2, by omega⟩
+/-- The loop's countdown register. -/
+def counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l, by omega⟩
+/-- A register holding zero, for the loop test. -/
+def zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 1, by omega⟩
+/-- A register holding one, for the countdown. -/
+def oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 2, by omega⟩
 
-private def bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1) :=
+/-- The body's scratch bank inside the loop's bank. -/
+def bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1) :=
   ⟨l + 3 + i.val, by omega⟩
 
-private def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
+/-- One native iteration: run the body on the environment and state words, copy its result into
+the state words and count down. -/
+def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
     (Fin (l + n + 1) → Fin r) → Code .exact r)
     (frontier : Fin r) (src : Fin (k + l + 1) → Fin r)
     (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r :=
@@ -214,7 +223,9 @@ private def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) →
         (.op (.exactBin .sub (tmp (counterSlot l n))
           (tmp (counterSlot l n)) (tmp (oneSlot l n))))
 
-private def loopEmit {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
+/-- The native loop: install the state words and the counter, then iterate `loopBody` while the
+counter is positive. -/
+def loopEmit {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
     (Fin (l + n + 1) → Fin r) → Code .exact r)
     (frontier : Fin r) (src : Fin (k + l + 1) → Fin r)
     (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r :=