feat(coinductive): wire PolyFun responders into IND-CPA by dtumad · Pull Request #483 · Verified-zkEVM/VCVio

dtumad · 2026-07-13T06:46:05Z

Stack

This PR is based on and should be reviewed after #482.

Motivation

#482 supplies the machine/program correspondence. This PR exercises it on an existing
cryptographic construction without moving protocol semantics into VCVio-specific machine types.

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

Probabilistic responders

The primitive data stored by ProbResponder spec is an actual PolyFun handler:

structure ProbResponder (spec : OracleSpec ι) where
  State : Type
  handler : PFunctor.Handler (StateT State SPMF) spec.toPFunctor

Thus a response is an effectful Mealy transition in the Kleisli category of SPMF: for a query it
jointly samples an answer and the next private responder state. ProbResponder contributes only
the existential state packaging and the specialization to VCVio's probability monad.

The new bridges include:

ofQueryImpl for an existing StateT σ SPMF PolyFun handler;
ofStateQueryImpl for an existing StateT σ ProbComp implementation, transported by
StateT.mapHom (MonadHom.ofLift ProbComp SPMF);
ofResponder for a deterministic PFunctor.Responder σ q, using
Responder.toStateHandler and the pure monad morphism;
pullback along a PFunctor.Lens.

The distributional bridge is an instance of PolyFun fold naturality rather than a fresh induction
over OracleComp:

(simulateQ responder.toQueryImpl oa).run state =
  𝒟[(simulateQ impl oa).run state]

Wired machine execution

The finite responder/strategy run is directly PolyFun's stateful Kleisli execution:

PFunctor.DynSystem.stepWith responder.toQueryImpl strategy
PFunctor.DynSystem.iterWith responder.toQueryImpl strategy

Similarly, pointed-machine execution is based on PointedMachine.runWith. The important
one-step law for an unresolved machine state is inherited from PolyFun:

wireKRun R (k + 1) (r, s) =
  wireKStep machine.toDynSystem R (r, s) >>= fun p =>
    wireKRun R k p

Lenses as reductions

For a lens

w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor

wrapping the querying machine and pulling back the responder are observationally the same:

(machine.wrapIface w).wireKRun responder k (r, s) =
  machine.wireKRun (responder.pullback w) k (r, s)

This is the concrete reduction principle exercised by the IND-CPA example.

IND-CPA application

The existing cached implementation

encAlg.IND_CPA_queryImpl' pk b :
  QueryImpl encAlg.IND_CPA_oracleSpec
    (StateT encAlg.IND_CPA_Cache ProbComp)

is wrapped as encAlg.IND_CPA_responder pk b. A machine satisfying

machine.Implements adversary k

then has the same joint result/cache distribution as the existing simulateQ execution. No
second IND-CPA semantics is introduced.

The left/right message transformation is represented by a PolyFun lens:

(m₀, m₁) ↦ (m₁, m₀)

It leaves uniform-sampling queries and oracle responses unchanged. The corresponding machine
reduction theorem is a one-line specialization of the generic wrap/pullback law, replacing a
protocol-specific run induction.

Proposed PolyFun follow-up

The remaining existential wrapper points to a useful generic PolyFun notion:

structure KleisliResponder (m : Type u → Type v) (q : PFunctor) where
  State : Type u
  handler : PFunctor.Handler (StateT State m) q

Useful accompanying theory would include:

pullback along PFunctor.Lens;
transport along MonadHom;
stepWith / iterWith laws;
a responder homomorphism or state-simulation notion.

The last item would express conjugacies between responder states—for example, swapping the keys
of the cached IND-CPA oracle—without a VCVio-specific induction. Once this exists upstream,
ProbResponder can become an even thinner specialization or alias.

Deliberately out of scope

computational complexity and PolyTime;
Cslib and concrete Turing machines;
asymptotic security;
a complete branch-flip/cache-conjugacy theorem, pending the generic responder-hom notion above.

Review guide

VCVio/OracleComp/Coinductive/Responder.lean — the thin handler-backed wrapper;
VCVio/OracleComp/Coinductive/WiredRun.lean — generic machine/responder wiring;
VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean — the existing-protocol application.

Validation

lake build
git diff --check dtumad/oracle-machine-implements..dtumad/polyfun-indcpa-responder
no new sorry declarations
no Cslib, PolyTime, or asymptotic-complexity dependency

github-actions · 2026-07-13T06:47:31Z

🤖 PR Summary

The PR body accurately describes the additions, and the per-file summaries confirm the code changes. No sorry or admit placeholders are present. The overview below synthesizes both sources.

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	371
❌ Lines Removed	0

Lean Declarations

✏️ Added: 41 declaration(s)

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

@[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) :
noncomputable def IND_CPA_responder (encAlg : AsymmEncAlg ProbComp M PK SK C)
theorem run_IND_CPA_responder_eq (encAlg : AsymmEncAlg ProbComp M PK SK C)
theorem wireKRun_IND_CPA_responder_eq (encAlg : AsymmEncAlg ProbComp M PK SK C)
theorem wireKRun_IND_CPA_swap (encAlg : AsymmEncAlg ProbComp M PK SK C)

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

@[simp] theorem ofHandlerFamily_state {Γ : Type u} (h : Γ → ProbHandler spec) :
@[simp] theorem ofQueryImpl_toQueryImpl (R : ProbResponder spec) :
@[simp] theorem ofResponder_state {σ : Type u}
@[simp] theorem ofStateQueryImpl_state {ι₀ : Type} {spec₀ : OracleSpec.{0, 0} ι₀}
@[simp] theorem toQueryImpl_ofQueryImpl {σ : Type u}
@[simp] theorem toQueryImpl_pullback {ι' : Type u} {spec' : OracleSpec.{u, u} ι'}
@[simp] theorem wireKIterate_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
@[simp] theorem wireKIterate_zero (A : OracleStrategy S spec) (R : ProbResponder spec)
@[simp] theorem wireKStep_apply (A : OracleStrategy S spec) (R : ProbResponder spec)
@[simp] theorem wireKStep_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
@[simp] theorem wireKStep_ofResponder {σ : Type u}
def answer (R : ProbResponder spec) (s : R.State) (t : spec.Domain) :
def ofQueryImpl {σ : Type u} (impl : QueryImpl spec (StateT σ SPMF)) : ProbResponder spec where
def toQueryImpl (R : ProbResponder spec) : QueryImpl spec (StateT R.State SPMF)
noncomputable def ofHandler (H : ProbHandler spec) : ProbResponder spec
noncomputable def ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec) :
noncomputable def ofResponder {σ : Type u}
noncomputable def ofStateQueryImpl {ι₀ : Type} {spec₀ : OracleSpec.{0, 0} ι₀}
noncomputable def pullback {ι' : Type u} {spec' : OracleSpec.{u, u} ι'}
noncomputable def wireKIterate (A : OracleStrategy S spec) (R : ProbResponder spec) :
noncomputable def wireKStep (A : OracleStrategy S spec) (R : ProbResponder spec) :
theorem run_simulateQ_toQueryImpl_ofStateQueryImpl {ι₀ : Type}
theorem wireKIterate_succ (A : OracleStrategy S spec) (R : ProbResponder spec)

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

@[simp] theorem wireKRun_ofHandlerFamily {Γ : Type u} (h : Γ → ProbHandler spec)
@[simp] theorem wireKRun_zero (M : OracleMachine spec α β) (R : ProbResponder spec)
def wrapIface (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)
noncomputable def wireKRun (M : OracleMachine spec α β) (R : ProbResponder spec)
theorem runK_wrap (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)
theorem wireKRun_of_output_eq_some (M : OracleMachine spec α β) (R : ProbResponder spec)
theorem wireKRun_succ_of_output_eq_none (M : OracleMachine spec α β)
theorem wireKRun_wrap (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)
theorem wrapIface_eq_wrap (w : PFunctor.Lens spec.toPFunctor spec'.toPFunctor)

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff largely adheres to the contributing guidelines, with one notable violation: the copyright year in both new files is 2026, but the current year is 2025. The project's instructions require CURRENT_YEAR to be the calendar year when the file is created. Additionally, no other style or documentation violations were found. All other requirements (module docstrings, declaration docstrings, section headers, prologue layout, no sorry, no linter suppressions, correct import placement, no ASCII banners) are satisfied.

📄 **Per-File Summaries**

VCVio.lean: VCVio.lean now imports VCVio.OracleComp.Coinductive.Responder and VCVio.OracleComp.Coinductive.WiredRun, making the definitions and theorems from those modules available in this file.
VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean: This file adds several new definitions and theorems to the IND-CPA oracle framework. It introduces IND_CPA_responder, a ProbResponder wrapper around the existing IND_CPA_queryImpl', along with the simp lemma IND_CPA_responder_state confirming its state. It proves run_IND_CPA_responder_eq (equating simulation via the responder with simulation via queryImpl') and wireKRun_IND_CPA_responder_eq (showing that a machine's wireKRun with the responder matches the distribution of the adversary's output). It also defines IND_CPA_swapChallengeLens and IND_CPA_swapLens (PolyFun lenses that swap the two messages in a challenge query), proves IND_CPA_swapLens_query_left and IND_CPA_swapLens_query_right, and establishes wireKRun_IND_CPA_swap (a machine-level reduction stating that wrapping a machine with the swap lens is equivalent to responder pullback along the same lens).
VCVio/OracleComp/Coinductive/Responder.lean: This new file Responder.lean defines ProbResponder spec, a structure that bundles a polynomial functor handler in the StateT State SPMF Kleisli category to represent stateful probabilistic responders for an oracle specification. It provides conversion functions (toQueryImpl, ofQueryImpl, ofHandlerFamily, ofHandler, ofStateQueryImpl, ofResponder), a pullback operation along an interface lens, and a naturality theorem run_simulateQ_toQueryImpl_ofStateQueryImpl relating stateful evaluation to a lifted ProbComp handler. In the OracleStrategy namespace, it defines wireKStep and wireKIterate as PolyFun‑wired one‑step and iterated runs against a responder, along with simplification lemmas (wireKStep_ofResponder, wireKStep_ofHandlerFamily, wireKIterate_ofHandlerFamily) connecting these operations to the deterministic closed game and to kleisliStep/kleisliIterate. No sorry or admit are present.
VCVio/OracleComp/Coinductive/WiredRun.lean: Adds OracleMachine.wireKRun, a noncomputable function that runs a pointed oracle machine against a stateful probabilistic responder for at most k rounds, along with a suite of equational theorems (wireKRun_zero, wireKRun_of_output_eq_some, wireKRun_succ_of_output_eq_none) that relate it to the underlying runK. The file also defines wrapIface, which transports a machine along a PFunctor.Lens, and proves that wrapIface coincides with the existing wrap (wrapIface_eq_wrap), that runK commutes with wrapping and responder pullback (runK_wrap), and the adjunction wireKRun_wrap — running a wrapped machine against a responder equals running the original machine against the pulled‑back responder.

Last updated: 2026-07-13 06:47 UTC.

github-actions · 2026-07-13T07:01:04Z

🤖 AI Review

Overall Summary:
An error occurred while synthesizing the summary: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

Errors during review:

Agent B failed for VCVio.lean
Agent B failed for VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean
Agent B failed for VCVio/OracleComp/Coinductive/Responder.lean
Agent B failed for VCVio/OracleComp/Coinductive/WiredRun.lean

🔗 **Cross-File Analysis**

Cross-file analysis failed: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio.lean`**

An error occurred while analyzing VCVio.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean`**

An error occurred while analyzing VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/Oracle.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio/OracleComp/Coinductive/Responder.lean`**

An error occurred while analyzing VCVio/OracleComp/Coinductive/Responder.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio/OracleComp/Coinductive/WiredRun.lean`**

An error occurred while analyzing VCVio/OracleComp/Coinductive/WiredRun.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

github-actions · 2026-07-13T07:07:20Z

Build Timing Report

Commit: 05b7cb3
Message: Merge d1639d4 into 149b32f
Ref: dtumad/polyfun-indcpa-responder
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Wall (s)	Status
Clean build	760.26	ok
Warm rebuild	4.50	ok
Smoke test	3.25	ok

Incremental Rebuild Signal

Warm rebuild saved 755.76s vs clean (168.95x 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 of 388 repo targets parsed from the current clean build log.

Wall (s)	Path
65.00	`LatticeCrypto/MLDSA/Concrete/NTT.lean`
64.00	`LatticeCrypto/MLKEM/Concrete/NTT.lean`
38.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean`
37.00	`VCVio/CryptoFoundations/ReplayFork.lean`
35.00	`VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean`
31.00	`VCVio/ProgramLogic/Relational/SimulateQ.lean`
29.00	`VCVio/ProgramLogic/Tactics/Unary/Internals.lean`
27.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean`
26.00	`LatticeCrypto/MLKEM/Concrete/Encoding.lean`
22.00	`VCVio/OracleComp/Coercions/Add.lean`
22.00	`VCVio/ProgramLogic/Tactics/Relational/Internals.lean`
22.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean`
21.00	`VCVio/CryptoFoundations/SecExp.lean`
21.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean`
21.00	`Examples/SimpleTwoServerPIR.lean`
20.00	`VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean`
19.00	`VCVio/OracleComp/QueryTracking/Birthday.lean`
17.00	`VCVio/CryptoFoundations/Fischlin/Completeness.lean`
17.00	`Examples/ProgramLogic/RelationalStep.lean`
16.00	`VCVio/EvalDist/Defs/Basic.lean`

dtumad · 2026-07-25T17:18:06Z

Closing as a reference draft rather than reworking in place. This was stacked on #482, whose PolyFun pin (the #29 PointedMachine.Implements branch) was closed upstream in favor of the merged #34–#37 DynComputation stack, so the base API this PR wraps no longer resolves at the current pin. Meanwhile the generic follow-up proposed at the end of this PR's description landed upstream as PolyFun#101 Handler.Stateful (with stepWith/iterWith restated over it and Responder.toStateHandler reshaped accordingly), which covers most of what ProbResponder's existential wrapper did by hand. A much thinner responder/IND-CPA presentation against the current pin will follow as a fresh PR; this branch remains the reference for the lens-as-reduction statements and the IND-CPA bridge lemmas.

…the IND-CPA responder presentation (#499) Reintroduce the responder layer over current PolyFun, replacing the closed reference draft #483: - ProbResponder: stateful probabilistic challengers as SPMF Kleisli-Mealy coalgebras, definitionally interchangeable with stateful QueryImpls; smart constructors are reducible so responder State spellings stay interchangeable during unification. - Strategy wiring stepAgainst/iterateAgainst as PolyFun stepWith/iterWith at SPMF (renamed from the legacy wireK* family, whose runK namesake no longer exists). - OracleMachine.runAgainst: fuelled machine-vs-responder runs, with the wrap/pullback interface adjunction factored through the new DynComputation.unroll_wrap and ProbResponder.liftM_mapLens_pullback rather than fuel induction. - IND-CPA: the cached LR oracle as a responder, the machine-level distribution bridge, and message swapping as a lens with the reduction a one-line instance of the generic adjunction. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

feat(coinductive): wire PolyFun responders into IND-CPA

d1639d4

dtumad marked this pull request as draft July 14, 2026 09:47

dtumad mentioned this pull request Jul 15, 2026

refactor(CryptoFoundations): derive replay forking from PolyFun contexts #488

Merged

dtumad closed this Jul 25, 2026

dtumad mentioned this pull request Jul 25, 2026

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

Merged

Navigation Menu

Uh oh!

feat(coinductive): wire PolyFun responders into IND-CPA - #483

feat(coinductive): wire PolyFun responders into IND-CPA#483
dtumad wants to merge 1 commit into
dtumad/oracle-machine-implementsfrom
dtumad/polyfun-indcpa-responder

dtumad commented Jul 13, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 13, 2026

Uh oh!

github-actions Bot commented Jul 13, 2026

Uh oh!

github-actions Bot commented Jul 13, 2026

Uh oh!

dtumad commented Jul 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

dtumad commented Jul 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Stack

Motivation

Probabilistic responders

Wired machine execution

Lenses as reductions

IND-CPA application

Proposed PolyFun follow-up

Deliberately out of scope

Review guide

Validation

Uh oh!

github-actions Bot commented Jul 13, 2026

🤖 PR Summary

Uh oh!

github-actions Bot commented Jul 13, 2026

🤖 AI Review

Uh oh!

github-actions Bot commented Jul 13, 2026

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

dtumad commented Jul 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

dtumad commented Jul 13, 2026 •

edited

Loading