feat(coinductive): oracle strategies and DynComputation-backed oracle machines by dtumad · Pull Request #498 · Verified-zkEVM/VCVio

dtumad · 2026-07-25T17:39:03Z

Motivation

Fresh implementation of the coinductive machine layer, replacing the closed reference draft
#482. That draft wrapped PFunctor.PointedMachine from the closed PolyFun#29 branch; upstream
replaced that API with the merged DynComputation stack (PolyFun#34–#37), so this layer is
rebuilt against the current pin rather than rebased.

The intended dictionary is unchanged, but more of it is now definitional or inherited:

VCVio notion	PolyFun notion	status
`OracleComp spec α`	`PFunctor.FreeM spec.toPFunctor α`	definitional (#490)
`QueryImpl spec m`	`PFunctor.Handler m spec.toPFunctor`	definitional (#490)
`OracleStrategy S spec`	`PFunctor.DynSystem S spec.toPFunctor`	alias
`OracleMachine spec α β`	`DynComputation spec.toPFunctor α β`	alias
`M.Implements` / `M.ImplementsWithin`	`DynComputation.Implements` / `.ImplementsWithin`	inherited

VCVio introduces no parallel model of interaction: the machine type, both implementation
relations, fuelled execution (runWith), sequential composition (ImplementsWithin.seqComp),
interface transport (wrap), and the simulation proof method
(implementsWithin_of_isSimulation) are all consumed from PolyFun directly. The VCVio layer is
the OracleSpec reading plus the probabilistic semantics.

The two-carrier reading

Machines are the intensional, state-carrying presentation (the carrier that cost and
complexity notions must live on); behaviors are the extensional carrier. The upstream
unbounded relation is already stated as behavior equality —

M.Implements program ↔ ∀ x, M.toDynSystem.behavior (M.init x) = FreeM.toResumption (program x)

— recorded here as implements_iff_behavior_eq (an Iff.rfl). So implementation facts proved
for machines are mate-facts about behaviors by definition, and remain consumable if a
behavior-first model of the interaction layer lands later.

What this adds

VCVio/OracleComp/Coinductive/DynSystem.lean — OracleStrategy, OracleHandler,
ProbHandler, and the strategy run theory: runAgainst, kleisli iteration under
probabilistic handlers, the OracleComp-as-coalgebra run (advance, evalSystem,
runProgram), typed transcripts via PFunctor.FreeM.Path, reduction lenses, and the
denotational query-bound bridges.
VCVio/OracleComp/Coinductive/Machine.lean — OracleMachine, OracleComp.toMachine
(via DynComputation.ofFreeM, implementing by implements_ofFreeM), the definitional
simulateQ bridges, implements_iff_behavior_eq, and the ImplementsWithin readings:
simulateQ_run_eq (any lawful QueryImpl), runWithInput_ofFn_eq (deterministic), and
probOutput_none_runWithInput (no mass on fuel exhaustion).

Deliberately out of scope

No sequential-composition file: ImplementsWithin.seqComp is consumed from PolyFun as-is.
wrapIface (the pointed re-cut of DynSystem.wrap with its runK_wrapIface adjunction
against responder pullback) waits for the responder layer, where the handler-level pullback
(Handler.Stateful.reindex) gives the right statement.
Probabilistic responders, IND-CPA wiring, run limits, and anything complexity/PPT-related.

Validation

lake build (2995 jobs, green)
scripts/check-extern-isolation.sh, scripts/check-interop-isolation.sh
no new sorry/axioms; the two salvaged-and-rewritten files build with zero warnings

… machines Reintroduce the coinductive machine layer over current PolyFun: - OracleStrategy/OracleHandler/ProbHandler and the strategy run theory (runAgainst, kleisli iteration, evalSystem, typed transcripts via FreeM.Path) as OracleSpec specializations of PFunctor.DynSystem. - OracleMachine := DynComputation spec.toPFunctor, inheriting Implements, ImplementsWithin, runWith, seqComp, wrap, and the simulation proof method from PolyFun rather than wrapping a bespoke machine type. - The simulateQ bridges (runWith_eq_simulateQ) are definitional, and implements_iff_behavior_eq records that the implementation relation is behavior equality in the cofree carrier. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

github-actions · 2026-07-25T17:40:20Z

🤖 PR Summary

AddREADME

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	821
❌ Lines Removed	0

Lean Declarations

✏️ Added: 84 declaration(s)

VCVio/OracleComp/Coinductive/DynSystem.lean (74)

@[simp] theorem advanceK_pure (H : ProbHandler spec) (x : α) :
@[simp] theorem advanceK_queryBind (H : ProbHandler spec) (t : spec.Domain)
@[simp] theorem advance_pure (h : OracleHandler spec) (x : α) :
@[simp] theorem advance_queryBind (h : OracleHandler spec) (t : spec.Domain)
@[simp] theorem coe_ofFn (f : (t : spec.Domain) → spec.Range t) : ⇑(ofFn f) = f
@[simp] theorem evalSystem_iterate (h : OracleHandler spec) (oa : OracleComp spec α) (n : ℕ) :
@[simp] theorem evalSystem_step (h : OracleHandler spec) (oa : OracleComp spec α) :
@[simp] theorem evalWithAnswerFn_queryBind (f : QueryImpl spec Id) (t : spec.Domain)
@[simp] theorem kleisliIterate_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
@[simp] theorem kleisliStep_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
@[simp] theorem kleisliTranscript_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
@[simp] theorem ofFn_apply (f : (t : spec.Domain) → spec.Range t) (t : spec.Domain) :
@[simp] theorem runAgainst_step (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
@[simp] theorem stateAfter_zero (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
@[simp] theorem stepsToHalt_pure (h : OracleHandler spec) (x : α) :
@[simp] theorem stepsToHalt_queryBind (h : OracleHandler spec) (t : spec.Domain)
@[simp] theorem toQueryImpl_apply (h : OracleHandler spec) (t : spec.Domain) :
@[simp] theorem transcriptDist_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
@[simp] theorem transcript_countQ_pure (h : OracleHandler spec) (p : ι → Prop) [DecidablePred p]
@[simp] theorem transcript_length (h : OracleHandler spec) (oa : OracleComp spec α) :
@[simp] theorem transcript_pure (h : OracleHandler spec) (x : α) :
@[simp] theorem transcript_queryBind (h : OracleHandler spec) (t : spec.Domain)
@[simp] theorem transcript_succ (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S)
@[simp] theorem transcript_zero (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
abbrev OracleHandler (spec : OracleSpec.{u, v} ι) : Type _
abbrev OracleStrategy (S : Type w) (spec : OracleSpec ι) : Type _
abbrev ProbHandler {ι : Type u} (spec : OracleSpec.{u, u} ι) : Type u
def _root_.OracleHandler.pullback (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec) :
def advance (h : OracleHandler spec) (oa : OracleComp spec α) : OracleComp spec α
def advanceOnce (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) : S
def answerStream (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
def evalSystem (h : OracleHandler spec) (α : Type v) :
def handlerPath (h : OracleHandler spec) : (oa : OracleComp spec α) → PFunctor.FreeM.Path oa
def juxtapose {ι₁ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {ι₂ : Type u}
def logOfPath : (oa : OracleComp spec α) → PFunctor.FreeM.Path oa → QueryLog spec
def ofFn (f : (t : spec.Domain) → spec.Range t) : OracleHandler spec
def pair {ι₁ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {ι₂ : Type u} {spec₂ : OracleSpec.{u, v} ι₂}
def queryStream (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
def reduce {τ : Type u} {superSpec : OracleSpec.{u, v} τ} (h : spec ⊂ₒ superSpec)
def runAgainst (h : OracleHandler spec) (A : OracleStrategy S spec) : PFunctor.Closed S
def runAlong (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec) :
def runProgram (h : OracleHandler spec) (oa : OracleComp spec α) : OracleComp spec α
def stateAfter (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) : S
def stepsToHalt (h : OracleHandler spec) (oa : OracleComp spec α) : ℕ
def toFn (h : OracleHandler spec) (t : spec.Domain) : spec.Range t
def toQueryImpl (h : OracleHandler spec) : QueryImpl spec Id
def transcript (h : OracleHandler spec) (oa : OracleComp spec α) : QueryLog spec
instance instDFunLike : DFunLike (OracleHandler spec) spec.Domain (fun t => spec.Range t) where
noncomputable def _root_.ProbHandler.ofHandler (h : OracleHandler spec) : ProbHandler spec
noncomputable def advanceK (H : ProbHandler spec) (oa : OracleComp spec α) :
noncomputable def kleisliIterate (H : ProbHandler spec) (A : OracleStrategy S spec) :
noncomputable def kleisliStep (H : ProbHandler spec) (A : OracleStrategy S spec) (s : S) :
noncomputable def kleisliTranscript (H : ProbHandler spec) (A : OracleStrategy S spec) :
noncomputable def probHandler {ι : Type} (spec : OracleSpec.{0, 0} ι)
noncomputable def transcriptDist (H : ProbHandler spec) (A : OracleStrategy S spec) (s : S)
theorem iterate_advance_eq_simulate (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem iterate_evalSystem_eq_simulate (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem logOfPath_handlerPath (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem next_iterate_trajectory_runAgainst (h : OracleHandler spec) (A : OracleStrategy S spec)
theorem outputAlong_runAlong (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec)
theorem output_handlerPath (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem reduce_trans {τ : Type u} {superSpec : OracleSpec.{u, v} τ}
theorem runProgram_eq (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem run_simulateQ_ofFn_withLogging (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem simulateQ_eq_advanceK_bind (H : ProbHandler spec) (oa : OracleComp spec α) :
theorem simulateQ_probHandler {ι : Type} {spec : OracleSpec.{0, 0} ι}
theorem stateAfter_eq_iterate (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S)
theorem stateAfter_succ (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
theorem stepsToHalt_le_of_isTotalQueryBound (h : OracleHandler spec) :
theorem trajectory_evalSystem_stabilizes (h : OracleHandler spec) (oa : OracleComp spec α) :
theorem transcript_countQ_le_of_isPerIndexQueryBound (h : OracleHandler spec) [DecidableEq ι]
theorem transcript_countQ_le_of_isQueryBoundP (h : OracleHandler spec) (p : ι → Prop)
theorem transcript_countQ_queryBind (h : OracleHandler spec) (p : ι → Prop) [DecidablePred p]
theorem transcript_length_le_of_isTotalQueryBound (h : OracleHandler spec)

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

@[simp] theorem toMachine_implements {α β : Type u} (program : α → OracleComp spec β) :
abbrev OracleMachine (spec : OracleSpec.{u, u} ι) (α : Type u) (β : Type u) : Type _
abbrev toMachine {α β : Type u} (program : α → OracleComp spec β) :
example : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor
theorem implements_iff_behavior_eq (M : OracleMachine spec α β)
theorem probOutput_none_runWithInput {M : OracleMachine spec α β}
theorem runWithInput_eq_simulateQ (M : OracleMachine spec α β) (impl : QueryImpl spec m)
theorem runWithInput_ofFn_eq {M : OracleMachine spec α β}
theorem runWith_eq_simulateQ (M : OracleMachine spec α β) (impl : QueryImpl spec m)
theorem simulateQ_run_eq [LawfulMonad m] {M : OracleMachine spec α β}

sorry Tracking

No sorrys were added, removed, or affected.

📄 **Per-File Summaries**

VCVio.lean: Two new imports have been added to VCVio.lean: VCVio.OracleComp.Coinductive.DynSystem and VCVio.OracleComp.Coinductive.Machine. This makes the definitions and theorems from those modules (dynamic systems and machines in the coinductive oracle computation framework) available to any file that imports VCVio without needing separate import statements.
VCVio/OracleComp/Coinductive/DynSystem.lean: This new file introduces the coalgebraic dual of OracleComp — OracleStrategy S spec (a PFunctor.DynSystem on spec.toPFunctor), OracleHandler spec (a PFunctor.Section), and ProbHandler spec (a randomized QueryImpl spec SPMF). It defines deterministic run operations (runAgainst, advanceOnce, stateAfter, queryStream, answerStream, transcript) and probabilistic ones (kleisliStep, kleisliIterate, kleisliTranscript, transcriptDist), together with Dirac-bridge theorems (kleisliStep_ofHandler, kleisliTranscript_ofHandler, transcriptDist_ofHandler). The headline correspondences iterate_advance_eq_simulate (deterministic) and simulateQ_eq_advanceK_bind (probabilistic) show that coalgebraic state iteration computes simulateQ/evalWithAnswerFn. The file also provides OracleComp.transcript, handlerPath, logOfPath, OracleHandler.pullback, and runAlong for reduction lenses, establishes denotational query bounds (transcript_length_le_of_isTotalQueryBound, transcript_countQ_le_of_isQueryBoundP, transcript_countQ_le_of_isPerIndexQueryBound), and proves the subsumption theorem run_simulateQ_ofFn_withLogging that the coalgebraic transcript equals the output of the existing logging oracle.
VCVio/OracleComp/Coinductive/Machine.lean: This file introduces the OracleMachine abbreviation, defined as DynComputation spec.toPFunctor α β, and provides the OracleComp-specific reading of the upstream DynComputation theory. It adds the implements_iff_behavior_eq theorem equating the Implements relation with behavior equality of the machine's cofree denotation and the program's query tree, the toMachine abbreviation (via DynComputation.ofFreeM) mapping a program family to its canonical residual-program machine with toMachine_implements, and definitional bridges (runWith_eq_simulateQ, runWithInput_eq_simulateQ) linking machine execution through a QueryImpl to simulateQ of the fuelled unrolling. In the ImplementsWithin namespace, it provides simulateQ_run_eq (via h.runWithInput_eq), its deterministic specialization runWithInput_ofFn_eq, and the probabilistic probOutput_none_runWithInput theorem showing no probability mass on fuel exhaustion. The diff adds no sorry or admit.

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

github-actions · 2026-07-25T18:43:06Z

Build Timing Report

Commit: 0c5ab29
Message: Merge 2a01028 into 53fdbbd
Ref: dtumad/oracle-machine-dyncomp
Comparison baseline: 2ceb2d8 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	677.08	686.04	+8.96	ok
Warm rebuild	4.43	4.74	+0.31	ok
Smoke test	2.91	3.01	+0.10	ok

Incremental Rebuild Signal

Warm rebuild saved 681.30s vs clean (144.73x 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
65.00	64.00	+1.00	`LatticeCrypto/MLKEM/Concrete/NTT.lean`
64.00	65.00	-1.00	`LatticeCrypto/MLDSA/Concrete/NTT.lean`
34.00	29.00	+5.00	`LatticeCrypto/MLKEM/Concrete/Encoding.lean`
33.00	32.00	+1.00	`VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean`
33.00	31.00	+2.00	`VCVio/ProgramLogic/Relational/SimulateQ.lean`
30.00	27.00	+3.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean`
26.00	24.00	+2.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean`
25.00	25.00	+0.00	`VCVio/OracleComp/Coercions/Add.lean`
22.00	20.00	+2.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean`
21.00	20.00	+1.00	`VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean`
21.00	21.00	+0.00	`VCVio/ProgramLogic/Tactics/Unary/Internals.lean`
20.00	23.00	-3.00	`VCVio/CryptoFoundations/SecExp.lean`
19.00	18.00	+1.00	`VCVio/OracleComp/QueryTracking/Birthday.lean`
19.00	18.00	+1.00	`VCVio/ProgramLogic/Tactics/Relational/Internals.lean`
18.00	16.00	+2.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean`
17.00	16.00	+1.00	`VCVio/EvalDist/Defs/Basic.lean`
17.00	16.00	+1.00	`VCVio/CryptoFoundations/Fischlin/Completeness.lean`
17.00	15.00	+2.00	`Examples/SimpleTwoServerPIR.lean`
16.00	14.00	+2.00	`Examples/ProgramLogic/UnaryStep.lean`
15.00	15.00	+0.00	`VCVio/EvalDist/Monad/Basic.lean`

Merge branch 'main' into dtumad/oracle-machine-dyncomp

5644bbd

dtumad marked this pull request as ready for review July 25, 2026 18:45

dtumad merged commit 65d9d3e into main Jul 25, 2026
7 checks passed

This was referenced Jul 25, 2026

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

Merged

Design the VCVio × PolyFun integration #494

Draft

feat(polytime): non-vacuous PPT/IsPolyTime over the DynComputation carrier, sorry-free #500

Draft

Navigation Menu

Uh oh!

feat(coinductive): oracle strategies and DynComputation-backed oracle machines - #498

feat(coinductive): oracle strategies and DynComputation-backed oracle machines#498
dtumad merged 2 commits into
mainfrom
dtumad/oracle-machine-dyncomp

dtumad commented Jul 25, 2026

Uh oh!

github-actions Bot commented Jul 25, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 25, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

dtumad commented Jul 25, 2026

Motivation

The two-carrier reading

What this adds

Deliberately out of scope

Validation

Uh oh!

github-actions Bot commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

github-actions Bot commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Jul 25, 2026 •

edited

Loading

github-actions Bot commented Jul 25, 2026 •

edited

Loading