feat(coinductive): let oracle machines implement OracleComp programs by dtumad · Pull Request #482 · Verified-zkEVM/VCVio

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

Motivation

The current PolyTime/Turing-machine draft contains a useful lower-level contribution that does
not depend on computational complexity: an operational presentation of an
OracleComp spec program by a PolyFun dynamical system and pointed machine.

This PR isolates that machinery so it can be reviewed and used independently of Cslib, Turing
machines, cost models, or polynomial-time claims.

The intended dictionary is:

VCVio notion	PolyFun notion
`OracleStrategy S spec`	`PFunctor.DynSystem S spec.toPFunctor`
`OracleMachine spec α β`	`PFunctor.PointedMachine spec.toPFunctor α β`
`QueryImpl spec m`	`PFunctor.Handler m spec.toPFunctor`
`OracleComp spec α`	`PFunctor.FreeM spec.toPFunctor α`

In particular, VCVio does not introduce a parallel model of interaction here. It specializes the
corresponding PolyFun notions to OracleSpec and supplies bridges to the existing oracle API.

What this adds

OracleStrategy as the OracleSpec specialization of PFunctor.DynSystem.
OracleMachine as the OracleSpec specialization of PFunctor.PointedMachine.
Fuelled execution through PolyFun's monad-parametric PointedMachine.runWith.
The implementation relation
```
machine.Implements program k
```
as a thin wrapper around PFunctor.PointedMachine.Implements.
A handler-parametric theorem turning implementation into execution equality:
```
machine.runK H k (machine.init x) =
  some <$> simulateQ H (program x)
```
A step-synchronised simulation relation for proving Implements from local machine/program
invariants.
Sequential composition of implementing machines.
Deterministic strategy execution, traces, query logging, and finite-run bridges reused from the
existing oracle framework.

PolyFun dependency update

The PolyFun revision is advanced to obtain the native PointedMachine.Implements theory and the
associated dynamical-system APIs. Four UC runtime files receive mechanical compatibility updates
for that revision.

Those compatibility edits do not change the UC model or introduce new VCVio protocol notions.

Deliberately out of scope

This PR contains no:

Cslib dependency;
Turing-machine encoding;
cost or query-complexity model;
asymptotic or polynomial-time statement;
computational security claim.

Those concerns can remain in the draft work while the basic operational tools land independently.

Review guide

The main files are:

VCVio/OracleComp/Coinductive/DynSystem.lean — the strategy/handler dictionary and run theory;
VCVio/OracleComp/Coinductive/Machine.lean — pointed machines, implementation, and simulations;
VCVio/OracleComp/Coinductive/Composition.lean — sequential composition.

The key architectural check is that the definitions remain aliases or thin wrappers over PolyFun,
rather than becoming a second implementation of dynamical systems inside VCVio.

Validation

lake build
git diff --check main..dtumad/oracle-machine-implements
no occurrences of Cslib, PolyTime, or new complexity definitions in the added modules

dtumad · 2026-07-13T06:47:53Z

Contains the non-TM specific portions of #481

github-actions · 2026-07-13T06:48:06Z

🤖 PR Summary

Mathematical Formalization

Coalgebraic formulation of oracle strategies and machines (VCVio/OracleComp/Coinductive/DynSystem.lean):

Introduces OracleStrategy S spec as a PFunctor.DynSystem on spec.toPFunctor (stateful adaptive querier) and OracleHandler spec as a PFunctor.Section (deterministic oracle).
Defines deterministic run helpers: OracleStrategy.runAgainst, advanceOnce, stateAfter, queryStream, answerStream, transcript.
Defines probabilistic run helpers via ProbHandler: kleisliStep, kleisliIterate, kleisliTranscript, transcriptDist.
Program-side dual: OracleComp.advance, stepsToHalt, evalSystem, runProgram, plus the headline theorem iterate_advance_eq_simulate (or iterate_evalSystem_eq_simulate) linking iteration under a deterministic handler to simulateQ.
Adds typed transcript tools (OracleComp.transcript, handlerPath, logOfPath), reduction lenses (OracleHandler.pullback, OracleComp.runAlong), and query-bound theorems: transcript_length_le_of_isTotalQueryBound, transcript_countQ_le_of_isQueryBoundP, transcript_countQ_le_of_isPerIndexQueryBound.
Subsumption bridge run_simulateQ_ofFn_withLogging linking the new transcript to existing QueryImpl.withLogging.

Oracle machine implementation theory (VCVio/OracleComp/Coinductive/Machine.lean, ~504 lines):

Defines OracleMachine as PFunctor.PointedMachine over the spec’s polynomial.
Implements fuelled monad-parametric run runK (definitionally PointedMachine.runWith), deterministic run runD, and the Implements relation M ⊨[k] oa (definitionally PFunctor.PointedMachine.Implements).
Proves Implements.runK_eq and its converse of_runK_eq, plus runK_ofHandler (Dirac bridge), Implements.steadyBy, Implements.implementsDet, and lemmas about halted states.
Defines StableOutput, SteadyBy, and IsSimulation for step-synchronized simulation, with the main proof method implements_of_isSimulation.
Bidirectional bridge:
- OracleComp.toMachine constructs a machine from a program family (using pureOutput, headQuery, headUpdate) and proves it implements the family under a total query bound via toMachine_implements and toMachine_isSimulation.
- M.toComp (inherited from PolyFun) unrolls a machine into a program, with simulateQ_toComp definitional, isTotalQueryBound_toComp, and evalWithAnswerFn_toComp.

Sequential composition of implementations (VCVio/OracleComp/Coinductive/Composition.lean):

Theorem OracleMachine.Implements.seqComp: if M₁ implements oa with fuel k₁ and M₂ implements ob with fuel k₂, then M₁ ⨟ M₂ implements λ x => oa x >>= ob with fuel k₁ + k₂.

Refactoring – UC process type parameterisation

To align with the new oracle machinery, the ProcessOver type and all its downstream uses in the UC runtime have been extended with an explicit type parameter P (program counter). The affected files and changes are:

VCVio/Interaction/UC/StdDoBridge.lean: ProcessOver now takes (P : Type) as an explicit binder; all three theorems (runSteps_zero, runSteps_succ, runSteps_triple_preserves_invariant) gain an implicit {P : Type}. The private incrementProcess is rephrased from a structure with Proc := ℕ to ProcessOver ℕ trivCtx via ProcessOver.ofStep ℕ.
VCVio/Interaction/UC/Runtime.lean: ProcessOver.runSteps gains parameter P and its process argument changes from ProcessOver Γ to ProcessOver P Γ; call site in processSemantics updated accordingly.
VCVio/Interaction/UC/AsyncRuntime.lean: runStepsAsync and theorem runStepsAsync_empty_trivial_eq now accept an extra type parameter P and expect ProcessOver P Γ.
VCVio/Interaction/UC/AsyncSecurity.lean: AsyncRun structure and variable block now require explicit P for the process’s program counter; every theorem, definition, and instance in the AsyncRun namespace is affected by the signature change.

These changes are purely mechanical (no new sorry or admit introduced) and are required for compatibility with the updated PolyFun pin and the new oracle machine types.

Module re-export

VCVio.lean: Adds imports for the three new coinductive oracle modules (Composition, DynSystem, Machine), making them available project-wide.

Discrepancy with PR body

The PR body summarises the new oracle constructs and mentions “update the PolyFun pin needed by this machinery, with only the corresponding UC API compatibility edits”. It does not explicitly describe the pervasive ProcessOver parameterisation, which constitutes a non-trivial refactoring of the existing UC runtime infrastructure. The per-file summaries confirm that these changes are indeed the “UC API compatibility edits” referenced, but the body’s brevity may understate their extent.

Statistics

Metric	Count
📝 Files Changed	10
✅ Lines Added	1237
❌ Lines Removed	20

Lean Declarations

✏️ Added: 128 declaration(s)

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

theorem Implements.seqComp {M₁ : OracleMachine spec α mid} {M₂ : OracleMachine spec mid β}

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 (53)

@[simp] theorem headQuery_pure (x : β) :
@[simp] theorem headQuery_queryBind (t : spec.Domain)
@[simp] theorem headUpdate_pure (x : β)
@[simp] theorem headUpdate_queryBind (t : spec.Domain)
@[simp] theorem pureOutput_pure (x : β) :
@[simp] theorem pureOutput_queryBind (t : spec.Domain)
@[simp] theorem runD_zero (h : OracleHandler spec) (s : M.State) :
@[simp] theorem runK_ofHandler (h : OracleHandler spec) (k : ℕ) (s : M.State) :
@[simp] theorem runK_zero (H : QueryImpl spec m) (s : M.State) :
abbrev IsSimulation (R : M.State → OracleComp spec β → Prop) : Prop
abbrev OracleMachine (spec : OracleSpec.{u, u} ι) (α β : Type u)
def Implements (oa : α → OracleComp spec β) (k : ℕ) : Prop
def ImplementsDet (oa : α → OracleComp spec β) (k : ℕ) : Prop
def StableOutput : Prop
def SteadyBy (h : OracleHandler spec) (s : M.State) (k : ℕ) : Prop
def headQuery (ob : OracleComp spec β) : ι
def headUpdate : (ob : OracleComp spec β) → spec.Range (headQuery ob) → OracleComp spec β
def pureOutput (ob : OracleComp spec β) : Option β
def runD (h : OracleHandler spec) (k : ℕ) (s : M.State) : Option β
def runK (H : QueryImpl spec m) : ℕ → M.State → m (Option β)
def toMachine (oa : α → OracleComp spec β) : OracleMachine spec α β where
example {m : Type u → Type u} : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor
theorem Implements.implementsDet {M : OracleMachine spec α β}
theorem Implements.of_runK_eq {M : OracleMachine spec α β} {oa : α → OracleComp spec β} {k : ℕ}
theorem Implements.runK_eq {M : OracleMachine spec α β} {oa : α → OracleComp spec β} {k : ℕ}
theorem Implements.runK_none_eq_zero {M : OracleMachine spec α β}
theorem Implements.steadyBy {M : OracleMachine spec α β} {oa : α → OracleComp spec β}
theorem StableOutput.output_stateAfter {M : OracleMachine spec α β} (hst : M.StableOutput)
theorem evalWithAnswerFn_toComp (h : OracleHandler spec) (k : ℕ) (s : M.State) :
theorem implements_of_isSimulation {M : OracleMachine spec α β}
theorem isTotalQueryBound_toComp (k : ℕ) (s : M.State) :
theorem iterate_advance_eq_of_le (h : OracleHandler spec) {ob : OracleComp spec β}
theorem pureOutput_headUpdate_of_eq_some {ob : OracleComp spec β} {b : β}
theorem runD_eq_output_stateAfter {M : OracleMachine spec α β} (hst : M.StableOutput)
theorem runD_of_output_eq_some (h : OracleHandler spec) {s : M.State} {b : β}
theorem runD_succ_of_output_eq_none (h : OracleHandler spec) {s : M.State}
theorem runD_succ_of_output_eq_some (h : OracleHandler spec) {s : M.State} {b : β}
theorem runK_of_output_eq_some (H : QueryImpl spec m) {s : M.State} {b : β}
theorem runK_succ_of_output_eq_none (H : QueryImpl spec m) {s : M.State}
theorem runK_succ_of_output_eq_none' (H : ProbHandler spec) {s : M.State}
theorem runK_succ_of_output_eq_some (H : QueryImpl spec m) {s : M.State} {b : β}
theorem simulateQ_ofHandler (h : OracleHandler spec) (ob : OracleComp spec β) :
theorem simulateQ_queryBind {r : Type u → Type w} [Monad r] [LawfulMonad r]
theorem simulateQ_toComp {m : Type u → Type u} [Monad m] (H : QueryImpl spec m)
theorem steadyBy_iff_isSome_runD {M : OracleMachine spec α β} (hst : M.StableOutput)
theorem toComp_of_output_eq_some {s : M.State} {b : β} (hb : M.output s = some b)
theorem toComp_succ_of_output_eq_none {s : M.State} (hb : M.output s = none) (k : ℕ) :
theorem toComp_succ_of_output_eq_some {s : M.State} {b : β} (hb : M.output s = some b)
theorem toMachine_advanceOnce (h : OracleHandler spec) (oa : α → OracleComp spec β) :
theorem toMachine_implements {oa : α → OracleComp spec β} {k : ℕ}
theorem toMachine_isSimulation (oa : α → OracleComp spec β) :
theorem toMachine_stableOutput (oa : α → OracleComp spec β) :
theorem toMachine_steadyBy {oa : α → OracleComp spec β} (h : OracleHandler spec)

✏️ Affected: 4 declaration(s) (line number changed)

private def incrementProcess : ProcessOver ℕ trivCtx in VCVio/Interaction/UC/StdDoBridge.lean moved from L177 to L177
theorem ProcessOver.runSteps_succ {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L109 to L109
theorem ProcessOver.runSteps_zero {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L104 to L104
theorem runSteps_triple_preserves_invariant {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L136 to L136

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

Diff follows project conventions: file headers, module docstrings, no ASCII banners, correct prologue layout, no local linter suppressions, and respects module layering by adding files to the intended Coinductive subdirectory. No style or documentation violations found.

📄 **Per-File Summaries**

VCVio.lean: Added imports for three new modules: VCVio.OracleComp.Coinductive.Composition, VCVio.OracleComp.Coinductive.DynSystem, and VCVio.OracleComp.Coinductive.Machine, making these coinductive oracle computation constructs available to the rest of the project.
VCVio/Interaction/UC/AsyncRuntime.lean: The diff modifies runStepsAsync and the theorem runStepsAsync_empty_trivial_eq in AsyncRuntime.lean. Both declarations now accept a type parameter P and expect a ProcessOver P Γ argument instead of ProcessOver Γ. This changes the process type to be indexed over an additional type P, aligning the interface with a broader refactor of the process type definition elsewhere in the project. No sorry or admit statements are present in this diff.
VCVio/Interaction/UC/AsyncSecurity.lean: The AsyncRun structure and the accompanying variable block now require an explicit type parameter P for the process's program counter (so the process signature is Concurrent.ProcessOver P Γ rather than Concurrent.ProcessOver Γ). Every theorem, definition, and instance in the AsyncRun namespace that implicitly used the old arities will be affected by this signature change because the generic process variable now carries the extra type argument P. No sorries or admits were introduced.
VCVio/Interaction/UC/Runtime.lean: The ProcessOver.runSteps function signature was changed to add an explicit type parameter P and update its process argument type from ProcessOver Γ to ProcessOver P Γ. The call site in processSemantics was updated accordingly, now calling ProcessOver.runSteps process.toProcess process.stepSampler ... instead of process.toProcess.runSteps process.stepSampler ..., making the module-qualified call explicit.
VCVio/Interaction/UC/StdDoBridge.lean: The file VCVio/Interaction/UC/StdDoBridge.lean now parameterizes ProcessOver by a type P (added as an explicit binder). The theorems ProcessOver.runSteps_zero, ProcessOver.runSteps_succ, and runSteps_triple_preserves_invariant each gain an implicit {P : Type} binder before the process argument. The private definition incrementProcess is rewritten from a ProcessOver trivCtx structure (with an explicit Proc := ℕ field) to a ProcessOver ℕ trivCtx constructed via ProcessOver.ofStep ℕ. The Std.Do.Triple predicate and the Std.Do comment remain unchanged.
VCVio/OracleComp/Coinductive/Composition.lean: The new file VCVio/OracleComp/Coinductive/Composition.lean introduces the theorem OracleMachine.Implements.seqComp, which states that if M₁ implements oa with fuel k₁ and M₂ implements ob with fuel k₂, then their sequential composition M₁ ⨟ M₂ implements λ x => oa x >>= ob with fuel k₁ + k₂.
VCVio/OracleComp/Coinductive/DynSystem.lean: This new file VCVio/OracleComp/Coinductive/DynSystem.lean introduces the coalgebraic dual of OracleComp: OracleStrategy S spec (a PFunctor.DynSystem on spec.toPFunctor, representing a stateful adaptive querier) and OracleHandler spec (a PFunctor.Section, a deterministic oracle). It provides OracleStrategy.runAgainst to close a strategy with a handler, OracleStrategy.advanceOnce/stateAfter/queryStream/answerStream/transcript for deterministic runs, and OracleStrategy.kleisliStep/kleisliIterate/kleisliTranscript/transcriptDist for probabilistic runs with a ProbHandler (randomized oracle). On the program side, OracleComp.advance/stepsToHalt/evalSystem/runProgram and the headline theorem iterate_advance_eq_simulate (or iterate_evalSystem_eq_simulate) establish that iterating the program as a coalgebra under a deterministic handler computes simulateQ. The file also defines OracleComp.transcript, handlerPath/logOfPath (typed transcripts via PFunctor.FreeM.Path), OracleHandler.pullback and OracleComp.runAlong for reduction lenses, and proves query‑bound theorems (transcript_length_le_of_isTotalQueryBound, transcript_countQ_le_of_isQueryBoundP, transcript_countQ_le_of_isPerIndexQueryBound) and a subsumption bridge (run_simulateQ_ofFn_withLogging) linking the new transcript to the existing QueryImpl.withLogging instrumentation.
VCVio/OracleComp/Coinductive/Machine.lean: This new file Machine.lean (504 lines) defines the core OracleMachine type as an abbreviation for PFunctor.PointedMachine over the spec's polynomial, and develops its run, implements, and simulation theory. It provides the fuelled monad-parametric run runK (definitionally PointedMachine.runWith), the deterministic run runD, and the Implements relation M ⊨[k] oa (definitionally PFunctor.PointedMachine.Implements), together with a handler-based reading Implements.runK_eq and its converse Implements.of_runK_eq. It defines StableOutput, SteadyBy, and an IsSimulation abbreviation for step-synchronized simulation, with the main proof method implements_of_isSimulation. A bidirectional bridge is established: OracleComp.toMachine constructs a machine from a program family (using pureOutput, headQuery, headUpdate) and proves it implements the family under a total query bound via toMachine_implements and toMachine_isSimulation; conversely, M.toComp (inherited from PolyFun) unrolls a machine into a program, with simulateQ_toComp holding definitionally, isTotalQueryBound_toComp providing a query bound, and evalWithAnswerFn_toComp giving the deterministic form. The file also proves runK_ofHandler (Dirac bridge), Implements.steadyBy, Implements.implementsDet, and several lemmas about runK and runD at halted states; no sorry or admit appear in the diff.
2 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json, lakefile.lean

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

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

Build Timing Report

Commit: e477052
Message: Merge 149b32f into cbd4144
Ref: dtumad/oracle-machine-implements
Comparison baseline: cbd4144 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 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	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	755.84	770.90	+15.06	ok
Warm rebuild	4.50	4.39	-0.11	ok
Smoke test	2.97	2.99	+0.02	ok

Incremental Rebuild Signal

Warm rebuild saved 766.51s vs clean (175.60x 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
66.00	67.00	-1.00	`LatticeCrypto/MLKEM/Concrete/NTT.lean`
66.00	69.00	-3.00	`LatticeCrypto/MLDSA/Concrete/NTT.lean`
37.00	41.00	-4.00	`VCVio/CryptoFoundations/ReplayFork.lean`
35.00	31.00	+4.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean`
33.00	34.00	-1.00	`VCVio/ProgramLogic/Relational/SimulateQ.lean`
30.00	40.00	-10.00	`VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean`
30.00	32.00	-2.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean`
28.00	31.00	-3.00	`VCVio/ProgramLogic/Tactics/Unary/Internals.lean`
27.00	26.00	+1.00	`VCVio/OracleComp/Coercions/Add.lean`
26.00	25.00	+1.00	`LatticeCrypto/MLKEM/Concrete/Encoding.lean`
24.00	24.00	+0.00	`VCVio/ProgramLogic/Tactics/Relational/Internals.lean`
23.00	22.00	+1.00	`VCVio/CryptoFoundations/SecExp.lean`
23.00	24.00	-1.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean`
23.00	24.00	-1.00	`Examples/SimpleTwoServerPIR.lean`
20.00	21.00	-1.00	`VCVio/OracleComp/QueryTracking/Birthday.lean`
20.00	23.00	-3.00	`VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean`
19.00	19.00	+0.00	`VCVio/EvalDist/Defs/Basic.lean`
19.00	19.00	+0.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean`
18.00	21.00	-3.00	`VCVio/CryptoFoundations/Fischlin/Completeness.lean`
16.00	14.00	+2.00	`VCVio/ProgramLogic/Relational/Quantitative.lean`

github-actions · 2026-07-14T10:02:25Z

🤖 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/Interaction/UC/AsyncRuntime.lean
Agent B failed for VCVio/Interaction/UC/AsyncSecurity.lean
Agent B failed for VCVio/Interaction/UC/Runtime.lean
Agent B failed for VCVio/Interaction/UC/StdDoBridge.lean
Agent B failed for VCVio/OracleComp/Coinductive/Composition.lean
Agent B failed for VCVio/OracleComp/Coinductive/DynSystem.lean
Agent B failed for VCVio/OracleComp/Coinductive/Machine.lean
Agent B failed for lakefile.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/Interaction/UC/AsyncRuntime.lean`**

An error occurred while analyzing VCVio/Interaction/UC/AsyncRuntime.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/Interaction/UC/AsyncSecurity.lean`**

An error occurred while analyzing VCVio/Interaction/UC/AsyncSecurity.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/Interaction/UC/Runtime.lean`**

An error occurred while analyzing VCVio/Interaction/UC/Runtime.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/Interaction/UC/StdDoBridge.lean`**

An error occurred while analyzing VCVio/Interaction/UC/StdDoBridge.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/Composition.lean`**

An error occurred while analyzing VCVio/OracleComp/Coinductive/Composition.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/DynSystem.lean`**

An error occurred while analyzing VCVio/OracleComp/Coinductive/DynSystem.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/Machine.lean`**

An error occurred while analyzing VCVio/OracleComp/Coinductive/Machine.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 `lakefile.lean`**

An error occurred while analyzing lakefile.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.'}]}}

dtumad added 2 commits July 13, 2026 01:24

feat(coinductive): oracle machines implement OracleComp programs

0065759

style(coinductive): trim module ending

149b32f

dtumad mentioned this pull request Jul 13, 2026

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

Draft

dtumad mentioned this pull request Jul 15, 2026

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

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(coinductive): let oracle machines implement OracleComp programs#482

feat(coinductive): let oracle machines implement OracleComp programs#482
dtumad wants to merge 2 commits into
mainfrom
dtumad/oracle-machine-implements

dtumad commented Jul 13, 2026 •

edited

Loading

Uh oh!

dtumad commented Jul 13, 2026

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 14, 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!

Motivation

What this adds

PolyFun dependency update

Deliberately out of scope

Review guide

Validation

Uh oh!

dtumad commented Jul 13, 2026

Uh oh!

github-actions Bot commented Jul 13, 2026

🤖 PR Summary

Mathematical Formalization

Refactoring – UC process type parameterisation

Module re-export

Discrepancy with PR body

Uh oh!

github-actions Bot commented Jul 13, 2026

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

github-actions Bot commented Jul 14, 2026

🤖 AI Review

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

dtumad commented Jul 13, 2026 •

edited

Loading