feat(realizability): generalize and pre-upstream the VCVio polytime machine layer

AGENTS.md

@@ -76,6 +76,16 @@ and depend on this library.
     (interfaces, par, wire, plug), corruption models, environment
     actions, leakage. *Generic only* — security-flavored UC layers
     (computational equivalence, asymptotic security) live in VCVio.
+- `PolyFun/Realizability/`: step classes (`StepClass` — a wide subcategory of
+  `Type u` presented by a representation structure on types and an
+  admissibility predicate on functions; with products, sums and distributivity
+  it is exactly a distributive category) and realizability of `FreeM` program
+  families by `DynComputation` machines whose first-order step maps are
+  admissible. Closed under `ofFn`, input precomposition, result
+  postcomposition, `bind`, interface transport, and class refinement.
+  Instances: unconstrained, finite-state, Mathlib-`Computable`, and a bridge
+  from any class of word functions. *Generic only* — cost measures and
+  concrete complexity classes live downstream.
 - `PolyFun/Control/`: monad and comonad infrastructure transitively
   required by the above (coalgebra, comonad, free / freecont monad
   algebra, monad iter / hom, lawful re-exports).
@@ -228,6 +238,8 @@ too specific or too changeable to keep at the repo root.
 - [`docs/wiki/itree.md`](docs/wiki/itree.md): interaction trees layer.
 - [`docs/wiki/interaction.md`](docs/wiki/interaction.md): generic interaction
   framework (`TypeTree`, two-party, multiparty, concurrent, UC).
+- [`docs/wiki/realizability.md`](docs/wiki/realizability.md): step classes and
+  realizability of free programs by admissible state machines.
 - [`docs/wiki/notation.md`](docs/wiki/notation.md): notation reference (UC
   composition operators).
 - [`docs/wiki/gotchas.md`](docs/wiki/gotchas.md): recurring traps and

PolyFun.lean

@@ -223,3 +223,8 @@ public import PolyFun.PFunctor.SubstMonoid.Extension
 public import PolyFun.PFunctor.Trace
 public import PolyFun.PFunctor.Wiring
 public import PolyFun.PFunctor.Wiring.Parallel
+public import PolyFun.Realizability.Basic
+public import PolyFun.Realizability.Closure
+public import PolyFun.Realizability.Instances
+public import PolyFun.Realizability.Machine
+public import PolyFun.Realizability.StepClass

PolyFun/PFunctor/Bound.lean

@@ -31,7 +31,7 @@ witnesses the equivalence by `Iff.rfl`.
 
 @[expose] public section
 
-universe v w uA uB
+universe v w uA uB uA₂ uB₂
 
 namespace PFunctor.FreeM
 
@@ -240,4 +240,18 @@ lemma isTotalRollBound_seq {og : FreeM P (α → β)} {oa : FreeM P α}
     IsTotalRollBound (og <*> oa) (n₁ + n₂) := by
   refine isRollBound_seq (fun a b => a + b) ?_ ?_ h₁ h₂ <;> grind
 
+/-- Interface transport along a lens preserves total roll bounds. A lens relabels
+positions and reindexes directions, leaving the branching structure — and hence the
+number of rolls along each branch — untouched. -/
+lemma isTotalRollBound_mapLens {Q : PFunctor.{uA₂, uB₂}} (l : Lens P Q)
+    (oa : FreeM P α) {n : ℕ} (h : oa.IsTotalRollBound n) :
+    (oa.mapLens l).IsTotalRollBound n := by
+  induction oa generalizing n with
+  | pure x => simp
+  | lift_bind a cont ih =>
+      rw [isTotalRollBound_lift_bind_iff] at h
+      rw [FreeM.mapLens_lift_bind, FreeM.liftBind_eq,
+        isTotalRollBound_lift_bind_iff]
+      exact ⟨h.1, fun d => ih _ (h.2 _)⟩
+
 end PFunctor.FreeM

PolyFun/PFunctor/Dynamical/DynComputation.lean

@@ -170,6 +170,32 @@ def contramapInput {γ : Type uγ} (M : DynComputation.{u} p α β) (f : γ →
     (M : DynComputation.{u} p α β) (input : γ) :
     (M.contramapInput f).denote input = M.denote (f input) := rfl
 
+/-- Replace a returning computation's initialization map, possibly changing the
+input type, while keeping its dynamics untouched. Reducible so that the state
+type, one-step views, and behaviors of `M.setInit g` reduce to those of `M`:
+computations sharing `toMachine` share every derived step map definitionally. -/
+@[reducible] def setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) : DynComputation.{u} p γ β :=
+  ⟨M.toMachine, g⟩
+
+@[simp] theorem setInit_State {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) : (M.setInit g).State = M.State := rfl
+
+@[simp] theorem setInit_init {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (input : γ) : (M.setInit g).init input = g input := rfl
+
+@[simp] theorem setInit_view {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (state : M.State) :
+    (M.setInit g).view state = M.view state := rfl
+
+@[simp] theorem setInit_denote {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (input : γ) :
+    (M.setInit g).denote input = M.toDynSystem.behavior (g input) := rfl
+
+/-- Reindexing inputs is exactly precomposing the initialization map. -/
+theorem contramapInput_eq_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : γ → α) : M.contramapInput f = M.setInit (M.init ∘ f) := rfl
+
 private def mapResultLift {γ : Type uγ} (f : β → γ) :
     Lens.{max uβ uA, uB, max uγ uA, uB}
       (C.{uβ, uB} β + p) (C.{uγ, uB} γ + p) :=
@@ -660,6 +686,36 @@ theorem seqComp_ofFn_obsEq {γ : Type uγ} (M : DynComputation.{u} p α β)
   funext value
   exact denote_ofFn f value
 
+/-! ## Realizations from a raw step function -/
+
+/-- Realize a returning computation from a one-step transition — returning either
+a value or a visible query with an explicit state-valued continuation — together
+with an initialization.
+
+This is the primary constructor for a hand-built machine: the supplied step
+function is exactly what `view` reads back, so no repackaging is visible to the
+caller. Reducible, so the state type and one-step views of a computation built
+this way are transparently those of the supplied data. -/
+@[reducible] def ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S) (init : α → S) :
+    DynComputation.{u} p α β where
+  State := S
+  toDynSystem :=
+    (fun state => (Resumption.pack (β := β) (stepFn state)).1) ⇆
+      fun state => (Resumption.pack (β := β) (stepFn state)).2
+  init := init
+
+@[simp] theorem ofStep_State {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) : (ofStep (p := p) stepFn init).State = S := rfl
+
+@[simp] theorem ofStep_init {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) (input : α) :
+    (ofStep (p := p) stepFn init).init input = init input := rfl
+
+@[simp] theorem view_ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) (state : S) :
+    (ofStep (p := p) stepFn init).view state = stepFn state :=
+  Resumption.unpack_pack (stepFn state)
+
 /-! ## Resumption realizations -/
 
 /-- Realize a family of resumptions directly, using the resumption itself as

PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean

@@ -29,7 +29,7 @@ bridges inherit their existing `Classical.choice` footprint.
 
 @[expose] public section
 
-universe u v uA uB uα uβ uγ
+universe u v uA uB uA₂ uB₂ uα uβ uγ
 
 namespace PFunctor
 
@@ -127,6 +127,93 @@ theorem isTotalRollBound_unroll (M : DynComputation.{u} p α β)
   rw [unroll_eq_truncate]
   exact Resumption.isTotalRollBound_truncate k (M.toDynSystem.behavior state)
 
+/-! ## Transport of bounded unrolling
+
+Bounded unrolling commutes with each of the three reindexings of a returning
+computation: replacing the initialization leaves it untouched, mapping the
+returned value maps the optional result, and interface transport along a lens
+transports the resulting syntax along the same lens.
+
+Each proof is a fuel induction rather than a definitional equality, because
+`unroll` is defined by cases on the computation's one-step view and so does not
+reduce until that view is exposed.
+-/
+
+/-- Replacing the initialization map leaves bounded unrolling from a hidden state
+unchanged: the two computations share `toMachine`, hence share their views. -/
+theorem unroll_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (k : ℕ) (state : M.State) :
+    (M.setInit g).unroll k state = M.unroll k state := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.setInit g) state, unroll_zero M state, setInit_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.setInit g) k state, unroll_succ M k state, setInit_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind position)
+            (funext fun direction => ih (next direction))
+
+theorem run_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (k : ℕ) (input : γ) :
+    (M.setInit g).run k input = M.unroll k (g input) :=
+  M.unroll_setInit g k (g input)
+
+/-- Mapping returned values maps the optional result of a bounded unrolling. -/
+@[simp] theorem unroll_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : β → γ) (k : ℕ) (state : M.State) :
+    (M.mapResult f).unroll k state =
+      FreeM.map (Option.map f) (M.unroll k state) := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.mapResult f) state, unroll_zero M state, mapResult_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.mapResult f) k state, unroll_succ M k state, mapResult_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind position)
+            (funext fun direction => ih (next direction))
+
+@[simp] theorem run_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : β → γ) (k : ℕ) (input : α) :
+    (M.mapResult f).run k input = FreeM.map (Option.map f) (M.run k input) :=
+  M.unroll_mapResult f k (M.init input)
+
+/-- Interface transport along a lens transports bounded unrolling along the same
+lens. -/
+@[simp] theorem unroll_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β)
+    (lens : Lens p q) (k : ℕ) (state : M.State) :
+    (M.wrap lens).unroll k state = (M.unroll k state).mapLens lens := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.wrap lens) state, unroll_zero M state, wrap_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.wrap lens) k state, unroll_succ M k state, wrap_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind (lens.toFunA position))
+            (funext fun direction => ih (next (lens.toFunB position direction)))
+
+@[simp] theorem run_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β)
+    (lens : Lens p q) (k : ℕ) (input : α) :
+    (M.wrap lens).run k input = (M.run k input).mapLens lens :=
+  M.unroll_wrap lens k (M.init input)
+
 /-! ## Resolution within a uniform query budget -/
 
 /-- Every answer branch from `state` returns within `k` visible queries. -/