feat(coinductive): probabilistic responders, wired runs, and the IND-CPA responder presentation

[dtumad]

Motivation

Fresh implementation of the responder layer, replacing the closed reference draft #483. That
draft was stacked on the retired PointedMachine API; this version sits on the merged machine
layer (#498) and on PolyFun's current Handler.Stateful/stepWith/iterWith (PolyFun#101),
which delivered the generic stateful-handler theory the old draft had to hand-roll.

The guiding principle is unchanged: cryptography in VCVio is a thin probabilistic layer over
PolyFun interaction. The existing cached IND-CPA oracle remains the source of truth; this PR
gives it a PolyFun-compatible responder presentation via lenses.

What this adds

Coinductive/Responder.lean — ProbResponder spec: stateful probabilistic challengers as
Mealy coalgebras in the Kleisli category of SPMF (a joint answer/next-state draw — essential
for lazily sampled oracles, where the cached entry must be the answer actually returned).
Definitionally interchangeable with QueryImpl spec (StateT State SPMF); the deterministic
(Id) sibling of PolyFun's Responder.equivStateHandler. Constructors from handlers, handler
families, deterministic responders, and stateful ProbComp implementations (the lazy random
oracle is the motivating instance). Strategy wiring stepAgainst/iterateAgainst is PolyFun's
stepWith/iterWith at m := SPMF, plus transcriptAgainst on QueryLog.

Coinductive/WiredRun.lean — OracleMachine.runAgainst: fuelled machine-vs-responder
runs, definitionally runWith at m := StateT R.State SPMF. The step laws are inherited from
DynComputation bounded execution; the memoryless collapse recovers the plain handler run.
The interface-wrapping adjunction runAgainst_wrap — wrapping the adversary forward along
a lens equals pulling the responder back — is now a two-step factoring rather than a fuel
induction: DynComputation.unroll_wrap (added in Machine.lean; pure FreeM-level, an
upstream candidate) composed with ProbResponder.liftM_mapLens_pullback (handler-level
naturality, machine-free).

INDCPA/Oracle.lean — the cached LR oracle as IND_CPA_responder (a thin
ofStateQueryImpl wrapper; IND_CPA_queryImpl' stays the source of truth), the machine-level
distribution bridge runAgainst_IND_CPA_responder_eq, and left/right message swapping as a
PolyFun lens whose machine reduction runAgainst_IND_CPA_swap is a one-line instance of the
generic adjunction.

Naming and API notes

• The legacy wireK* names are gone: they referenced the old runK (fuel-k run on the
  retired PointedMachine), which no longer exists. The run family is now
  runAgainst/stepAgainst/iterateAgainst/transcriptAgainst, matching the
  pattern-runs-on-matter vocabulary (runAgainst = run the adversary pattern against the
  challenger matter).
• Responder smart constructors are @[reducible]: statements freely mix (pullback w R).State
  with R.State (and similar), and keeping those interchangeable at reducible transparency is
  what lets rw/simp traverse such goals — the earlier draft needed trailing rfls exactly
  where this was missing. Remaining handler-layer normalization uses PolyFun#103's
  handler_nf simp set.

Proposed PolyFun follow-ups

• DynComputation.unroll_wrap (unrolling commutes with wrap) belongs next to the other
  bounded-execution lemmas.
• The generic form of liftM_mapLens_pullback — FreeM.liftM h (FreeM.mapLens w f) = FreeM.liftM (fun t => w.toFunB t <$> h (w.toFunA t)) f for any lawful monad — is
  Handler-level naturality with no responder content.

Deliberately out of scope

• Computational complexity / PPT (returns as its own stack on the machine carrier).
• Branch-flip/cache-conjugacy for the IND-CPA cache (wants a responder-homomorphism notion —
  PresentationHom territory upstream).

Validation

• lake build (3002 jobs, green; only pre-existing sorry warnings on main)
• scripts/check-extern-isolation.sh, scripts/check-interop-isolation.sh
• no new sorry/axioms; no linter warnings in the added files

[github-actions]

🤖 PR Summary

This PR adds a probabilistic responder layer to the coinductive oracle machine framework, replacing the retired PointedMachine-based draft. It introduces ProbResponder (stateful probabilistic challengers as Mealy coalgebras in the Kleisli category of SPMF), wired runs (stepAgainst/iterateAgainst/transcriptAgainst), and OracleMachine.runAgainst (fuelled machine-vs-responder runs). The IND-CPA oracle is given a responder presentation via IND_CPA_responder, and a lens-based swap reduction is proved using the generic runAgainst_wrap adjunction. A supporting lemma unroll_wrap is added to Machine.lean. All proofs are complete; no new sorry or admit are introduced. Legacy wireK* names are removed and replaced by the runAgainst family. The PR passes lake build and isolation scripts with no linter warnings.

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	671
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 47 declaration(s)

VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean (9)

• @[reducible] noncomputable def IND_CPA_responder (encAlg : AsymmEncAlg ProbComp M PK SK C)
• @[simp] theorem IND_CPA_responder_state (encAlg : AsymmEncAlg ProbComp M PK SK C)
• @[simp] theorem IND_CPA_swapLens_query_left (encAlg : AsymmEncAlg ProbComp M PK SK C)
• @[simp] theorem IND_CPA_swapLens_query_right (encAlg : AsymmEncAlg ProbComp M PK SK C)
• def IND_CPA_swapChallengeLens :
• def IND_CPA_swapLens (encAlg : AsymmEncAlg ProbComp M PK SK C) :
• theorem runAgainst_IND_CPA_responder_eq (encAlg : AsymmEncAlg ProbComp M PK SK C)
• theorem runAgainst_IND_CPA_swap (encAlg : AsymmEncAlg ProbComp M PK SK C)
• theorem run_IND_CPA_responder_eq (encAlg : AsymmEncAlg ProbComp M PK SK C)

VCVio/OracleComp/Coinductive/Machine.lean (1)

• theorem unroll_wrap (M : DynComputation.{u'} p α β) (w : PFunctor.Lens p q)

VCVio/OracleComp/Coinductive/Responder.lean (29)

• @[reducible] def ofQueryImpl {σ : Type u} (impl : QueryImpl spec (StateT σ SPMF)) :
• @[reducible] noncomputable def ofDet {σ : Type u} (C : PFunctor.Responder σ spec.toPFunctor) :
• @[reducible] noncomputable def ofHandler (H : ProbHandler spec) : ProbResponder spec
• @[reducible] noncomputable def ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec) :
• @[reducible] noncomputable def ofStateQueryImpl {ι₀ : Type} {spec₀ : OracleSpec.{0, 0} ι₀}
• @[reducible] noncomputable def pullback {ι' : Type u} {spec' : OracleSpec.{u, u} ι'}
• @[simp] lemma ofQueryImpl_toQueryImpl (R : ProbResponder spec) :
• @[simp] lemma toQueryImpl_ofQueryImpl {σ : Type u}
• @[simp] theorem iterateAgainst_ofHandler (H : ProbHandler spec) (A : OracleStrategy S spec)
• @[simp] theorem iterateAgainst_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
• @[simp] theorem iterateAgainst_zero (A : OracleStrategy S spec) (R : ProbResponder spec)
• @[simp] theorem ofStateQueryImpl_state {ι₀ : Type} {spec₀ : OracleSpec.{0, 0} ι₀} {σ : Type}
• @[simp] theorem stepAgainst_apply (A : OracleStrategy S spec) (R : ProbResponder spec)
• @[simp] theorem stepAgainst_ofDet (A : OracleStrategy S spec) {σ : Type u}
• @[simp] theorem stepAgainst_ofHandler (H : ProbHandler spec) (A : OracleStrategy S spec)
• @[simp] theorem stepAgainst_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
• @[simp] theorem toQueryImpl_pullback {ι' : Type u} {spec' : OracleSpec.{u, u} ι'}
• def toQueryImpl (R : ProbResponder spec) : QueryImpl spec (StateT R.State SPMF)
• example (H : ProbHandler spec) (A : OracleStrategy S spec) (n : ℕ) (s : S) :
• example (H : ProbHandler spec) (A : OracleStrategy S spec) (s : S) :
• noncomputable def iterateAgainst (A : OracleStrategy S spec) (R : ProbResponder spec) :
• noncomputable def randomOracleResponder {ι₀ : Type} [DecidableEq ι₀]
• noncomputable def stepAgainst (A : OracleStrategy S spec) (R : ProbResponder spec) :
• noncomputable def transcriptAgainst (A : OracleStrategy S spec) (R : ProbResponder spec) :
• noncomputable def transcriptDistAgainst (A : OracleStrategy S spec) (R : ProbResponder spec)
• theorem iterateAgainst_succ (A : OracleStrategy S spec) (R : ProbResponder spec) (n : ℕ)
• theorem liftM_mapLens_pullback {ι' : Type u} {spec' : OracleSpec.{u, u} ι'}
• theorem run_map_simulateQ_toQueryImpl_ofStateQueryImpl {ι₀ : Type}
• theorem run_simulateQ_toQueryImpl_ofStateQueryImpl {ι₀ : Type}

VCVio/OracleComp/Coinductive/WiredRun.lean (8)

• @[simp] theorem runAgainst_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
• noncomputable def runAgainst (M : OracleMachine spec α β) (R : ProbResponder spec)
• theorem runAgainst_eq_runWith_run (M : OracleMachine spec α β) (R : ProbResponder spec)
• theorem runAgainst_of_view_return (M : OracleMachine spec α β) (R : ProbResponder spec)
• theorem runAgainst_succ_of_view_query (M : OracleMachine spec α β)
• theorem runAgainst_wrap (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)
• theorem runAgainst_zero_of_view_query (M : OracleMachine spec α β)
• theorem runWith_wrap (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff is largely well-structured and adheres to the documentation, style, and attribution requirements. Two new files violate the prologue layout by missing a blank line between the copyright header and the imports block, as required by the style guide.

---

📄 **Per-File Summaries**

• VCVio.lean: This change adds two new imports to the VCVio.lean file: VCVio.OracleComp.Coinductive.Responder and VCVio.OracleComp.Coinductive.WiredRun. These imports make the definitions and theorems from those modules available project-wide, supporting coinductive reasoning about oracle computations and their execution.
• VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean: The diff adds a new IND_CPA_responder definition wrapping the existing IND_CPA_queryImpl' as a ProbResponder, along with three theorems: IND_CPA_responder_state (state type equality), run_IND_CPA_responder_eq (simulation equivalence), and runAgainst_IND_CPA_responder_eq (machine execution equivalence). It also introduces IND_CPA_swapChallengeLens and IND_CPA_swapLens (PFunctor lenses that swap the two messages in a challenge query), two simp lemmas about their action on left/right queries, and the theorem runAgainst_IND_CPA_swap (a specialization of OracleMachine.runAgainst_wrap). A new import of VCVio.OracleComp.Coinductive.WiredRun is added.
• VCVio/OracleComp/Coinductive/Machine.lean: 在 VCVio/OracleComp/Coinductive/Machine.lean 文件中，新增了 PFunctor.DynSystem.DynComputation 命名空间下的 UnrollWrap 小节，其中定义并证明了定理 unroll_wrap。该定理断言：对任意 DynComputation 机器 M、透镜 w、自然数 k 和状态 s，经过接口包装后的机器 (M.wrap w) 的燃料式展开 (M.wrap w).unroll k s 等于透镜翻译后的原始展开 PFunctor.FreeM.mapLens w (M.unroll k s)。证明通过归纳法完成，利用了 unroll_return 和 unroll_query_zero / unroll_query_succ 等辅助引理。此定理建立了燃料式展开与接口传输的可交换性，为后续处理 handler 级别的包装律提供了语法基础。
• VCVio/OracleComp/Coinductive/Responder.lean: This new file introduces ProbResponder spec, a probabilistic stateful responder (challenger) as a Mealy coalgebra in the Kleisli category of SPMF, with bundled/unbundled identification toQueryImpl/ofQueryImpl. It provides responder pullback (pullback, liftM_mapLens_pullback), a bridge from StateT σ ProbComp implementations (ofStateQueryImpl, run_simulateQ_toQueryImpl_ofStateQueryImpl, run_map_simulateQ_toQueryImpl_ofStateQueryImpl), and the lazy random oracle as an instance (randomOracleResponder). The file also defines wired runs (stepAgainst, iterateAgainst, transcriptAgainst, transcriptDistAgainst) and proves deterministic and memoryless recovery theorems (stepAgainst_ofDet, stepAgainst_ofHandlerFamily, iterateAgainst_ofHandlerFamily, stepAgainst_ofHandler, iterateAgainst_ofHandler), along with examples that confirm definitional equality with PFunctor.DynSystem.kleisliStep/kleisliIterate. No sorry or admit appear.
• VCVio/OracleComp/Coinductive/WiredRun.lean: This new file defines OracleMachine.runAgainst, the fuelled run of a machine against a stateful probabilistic responder (ProbResponder), implemented as (M.runWith R.toQueryImpl k s).run r. It proves the definitional canary runAgainst_eq_runWith_run, the Dirac-return lemma runAgainst_of_view_return, the zero-fuel cut-off lemma runAgainst_zero_of_view_query, and the wired step law runAgainst_succ_of_view_query. The memoryless recovery runAgainst_ofHandlerFamily collapses the stateful run to a functor-mapped memoryless run. The interface-wrapping adjunctions runWith_wrap and runAgainst_wrap equate running a wrapped machine against a spec'-responder with running the original machine against the responder pulled back along a lens.

---

Last updated: 2026-07-25 18:56 UTC.

[github-actions]

Build Timing Report

• Commit: 0ae64b7
• Message: Merge 47d6d77 into 65d9d3e
• Ref: dtumad/responder-layer
• Comparison baseline: 65d9d3e from the latest successful main run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	610.45	706.06	+95.61	ok
Warm rebuild	5.29	4.60	-0.69	ok
Smoke test	1.99	2.71	+0.72	ok

Incremental Rebuild Signal

• Warm rebuild saved 701.46s vs clean (153.49x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
68.00	73.00	-5.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
67.00	71.00	-4.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
35.00	30.00	+5.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
35.00	31.00	+4.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
32.00	24.00	+8.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
32.00	28.00	+4.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
27.00	23.00	+4.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
25.00	22.00	+3.00	VCVio/OracleComp/Coercions/Add.lean
23.00	18.00	+5.00	VCVio/CryptoFoundations/SecExp.lean
23.00	20.00	+3.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
23.00	21.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
22.00	18.00	+4.00	VCVio/OracleComp/QueryTracking/Birthday.lean
21.00	16.00	+5.00	VCVio/CryptoFoundations/ReplayFork.lean
21.00	16.00	+5.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
20.00	16.00	+4.00	VCVio/EvalDist/Defs/Basic.lean
20.00	18.00	+2.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
19.00	18.00	+1.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
17.00	16.00	+1.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
16.00	15.00	+1.00	VCVio/EvalDist/Monad/Basic.lean
16.00	14.00	+2.00	Examples/SimpleTwoServerPIR.lean