Std.Do handler specifications for OracleComp simulators #
Connects the oracle-simulation handlers (cachingOracle, seededOracle,
loggingOracle) to Std.Do's Triple / mvcgen framework via the
instWPOracleComp bridge in StdDoBridge.lean.
Architecture #
The bridge is two-layered:
- Per-query (leaf) specs are proven once. Modern handlers (
cachingOracle,loggingOracle,cachingLoggingOracle) are written indonotation withget/match/query/modify/tell, and their_triplelemmas usemvcgendirectly to walk the body. Eachquerystep is bridged to a support-based statement viawpProp_iff_forall_support; this is the only point where the proof leaves pureStd.Do.Triplereasoning. Older handlers (seededOracle) are still proved viatriple_stateT_iff_forall_supportbecause theirStateT.mk-style body doesn't reduce undermvcgen. Specs admitting a single canonical postcondition are@[spec]-tagged. - Composite (program-level) reasoning is then done by
mvcgen. Each example below ends withmvcgen [handler_triple](optionally<;> grind) and the tactic walks the bind tree, instantiating the leaf spec at each occurrence and discharging side conditions. No per-program induction is required from the user.
loggingOracle is the original WriterT (QueryLog spec) (OracleComp spec)
implementation in VCVio/OracleComp/QueryTracking/LoggingOracle.lean.
The bridge WriterTBridge.lean interprets the writer log ω = QueryLog spec
as a state component of Std.Do's (.arg ω .pure) post-shape, so the
mvcgen workflow for WriterT and StateT handlers is identical.
For whole-simulateQ results, the structural recursion on OracleComp is
isolated in the single helper simulateQ_triple_preserves_invariant. A
direct Triple.bind-based proof currently triggers a typeclass-search
timeout on WPMonad (StateT σ (OracleComp spec)) (.arg σ .pure); the
helper bails out to support reasoning once and downstream consumers stay in
the Std.Do world. See StdDoBridge.lean's architectural note for the
two mvcgen-side issues (spurious MonadLift OracleComp OracleComp and
DiscrTree liftM/MonadLift.monadLift mismatch) that prevent a fully
spec-driven leaf proof; both are worked around there with @[spec]
registrations, but the underlying WPMonad synthesis remains expensive.
Main results #
simulateQ_triple_preserves_invariant- generic invariant-preservation forsimulateQ; lifts per-handler invariant triples to whole-program triples.cachingOracle_triple,seededOracle_triple,seededOracle_triple_of_cons,seededOracle_triple_of_nil,loggingOracle_triple,loggingOracle_triple_prefix- per-handler specifications consumable bymvcgen.simulateQ_cachingOracle_preserves_cache_le- worked whole-program example liftingcachingOracle_triple.
Worked mvcgen examples #
Each handler section ends with one or more example blocks demonstrating
that mvcgen actually closes goals composed from the per-query specs:
two-, three-, and four-query bind chains for caching; a no-fallthrough
chain for seeded; an in-order log-extension chain for logging; and prefix /
replacement chains for the replay fork in
VCVio.CryptoFoundations.ReplayForkStdDo.
Stacked / multi-handler examples #
The stackedHandlers section combines two state-tracking handlers into a
single StateT (σ₁ × σ₂) (OracleComp spec) layer. The worked example
cachingLoggingOracle simultaneously caches and logs every query; its
@[spec] lemma asserts both invariants together, and the generic
simulateQ_triple_preserves_invariant lifts each component invariant
(cache₀ ≤ cache' and log₀ <+: log') to whole-program statements.
This single-StateT-layer pattern is preferred over genuinely stacked
StateT-over-StateT because:
mvcgenandTriple.bindalready struggle with oneStateTlayer overOracleComp(see theWPMonadtimeout discussion above); two layers amplify the issue.- The product-state representation matches the FiatShamir / forking
proofs already in
VCVio/CryptoFoundations, so there is a direct path from these examples to research-grade proofs.
Related #
The replay-fork handler replayOracle lives in
VCVio.CryptoFoundations.ReplayFork; its Std.Do.Triple specifications
are in VCVio.CryptoFoundations.ReplayForkStdDo.
Limitations #
simulateQ_triple_preserves_invariantis still proved by induction on the support, not byTriple.bind/Triple.pure. Two roadblocks make the structural proof unaffordable today:WPMonad (StateT σ (OracleComp spec)) (.arg σ .pure)instance synthesis times out onisDefEq(verified up to 1M heartbeats with several proof variations). The cost appears to be in(wp x).monoreduction insideTriple.bindfor theStateT σ (OracleComp spec)instance.- The
mvcgenDiscrTreeonly matchesliftM-headed query terms after ourSpec.monadLift_queryworkaround inStdDoBridge.lean; the pre-workaround failure mode silently dropped applicable specs rather than producing a clear error, which makes diagnosing mvcgen-side blockers expensive.
Both are upstream
Std.Doissues worth filing; the support fallback is a one-shot escape hatch and downstream consumers stay in theStd.Doworld.seededOracle's leaf specs (seededOracle_triple,seededOracle_triple_of_cons,seededOracle_triple_of_nil) still bail out to support-based reasoning. TheStateT.mk-style definition branches on the seed list, and rewriting it indonotation conflicts withMonadStateOfinstance resolution. RefactoringseededOracleto usedowithget/set/purewould make itmvcgen-friendly, but is non-trivial given the existing dependents.
Generic simulation triple: if every handler call handler t preserves an
invariant I on the simulation state, then simulateQ handler oa preserves
I for any oa : OracleComp spec α.
The invariant-only form (same I as pre- and post-condition, independent of
return value) is the most common case; stronger per-call specs can be derived
by instantiating I appropriately or composing via Triple.and/Triple.mp.
Specialized simulation triple: combine a starting-state precondition
s = s₀ with an invariant that holds of s₀. The invariant is threaded
through the entire simulation.
WriterT analogue of simulateQ_triple_preserves_invariant.
If every per-query handler call preserves an invariant I on the
accumulated writer (stated as a Std.Do.Triple), then the whole
simulation simulateQ handler oa preserves I across the accumulated
writer output.
Bridges through triple_writerT_iff_forall_support_monoid and
OracleComp.simulateQ_run_writerPreservesInv, mirroring the StateT
helper above. Typical handler values are countingOracle and
costOracle costFn.
Cache-monotonicity spec for cachingOracle t in Std.Do.Triple form.
If the cache on entry is ≥ cache₀, then after a single call to
cachingOracle t, the updated cache is still ≥ cache₀ and, moreover,
contains the returned value at key t.
Global cache-monotonicity for simulateQ cachingOracle: an arbitrary
OracleComp simulated under caching never shrinks the cache. Derived via the
generic simulateQ_triple_preserves_invariant.
Specification for seededOracle t in Std.Do.Triple form.
The call consumes at most one value at index t: either the seed was empty at
t (state unchanged, returned value fresh) or the seed started with a value
v at t that is returned and popped from the state.
seededOracle is defined via StateT.mk, so we open the structure with
triple_stateT_iff_forall_support to bring the match-on-seed under
support reasoning, then close each branch directly. The other handlers
(cachingOracle, loggingOracle, cachingLoggingOracle) are defined in
do-notation form and admit pure mvcgen proofs; this one follows the
same pattern only after the StateT.mk is unfolded.
Specialized spec: if the seed has at least one value at t, seededOracle t
deterministically pops the head and updates the state.
Note: neither seededOracle_triple_of_cons nor seededOracle_triple_of_nil
is tagged @[spec]. mvcgen's DiscrTree cannot discriminate between them
based on the numerical residue of seed t — they share a head symbol
(seededOracle), and their preconditions differ only by an unrelated
equation about the seed. Registering both would cause findSpec to fire
one arbitrarily and drop the other, producing obscure goals. Instead, we
leave the disjunction-shaped seededOracle_triple as the @[spec]-tagged
version and derive both specialised forms by case-analysis when needed.
Specialized spec: if the seed is empty at t, seededOracle t makes a live
query and leaves the state untouched.
Spec for loggingOracle t over WriterT (QueryLog spec) (OracleComp spec):
the writer log accumulates the query / response pair ⟨t, v⟩. Proved purely
with mvcgen plus a single bridging step to bring the residual
wpProp (liftM (query t)) goal to support form so the universally-quantified
obligation can be discharged by a second mvcgen.
Note: the writer log ω = QueryLog spec is interpreted by
WriterTBridge.lean as a state component (post-shape (.arg ω .pure)),
so the precondition / postcondition shape is identical to that of the
StateT-based reformulation.
Log-monotonicity corollary: the log only grows (as a list-prefix). Derived
directly from loggingOracle_triple via mvcgen (no support-layer escape).
Spec for countingOracle t over WriterT (QueryCount ι) (OracleComp spec):
the query count is incremented by QueryCount.single t (i.e., +1 at index
t, +0 elsewhere). Uses the [Monoid (QueryCount ι)] parameterization of
WriterTBridge, so the post-state is s * QueryCount.single t, which is
s + QueryCount.single t by QueryCount.monoid_mul_def.
Proved via mvcgen plus a single bridging step for the lifted query t leaf:
the tactic walks the body do tell (...); liftM (query t), consumes the
tell-spec (Monoid variant), and wpProp_iff_forall_support discharges the
query t residual.
Whole-program monotonicity for countingOracle: the accumulated query
count under simulateQ countingOracle oa only ever grows. Derived from the
generic simulateQ_writerT_triple_preserves_invariant with invariant
I qc := qc₀ ≤ qc.
Spec for costOracle costFn t over WriterT ω (OracleComp spec):
the cost accumulates by exactly costFn t. Generalises
countingOracle_triple to arbitrary monoidal cost functions.
Whole-program submonoid closure for costOracle: if costFn t ∈ S
for every query t (where S : Submonoid ω), then the accumulated cost
of simulateQ (costOracle costFn) oa stays in S starting from any
s₀ ∈ S. Derived from the generic
simulateQ_writerT_triple_preserves_invariant with I s := s ∈ S.
Stacked handlers #
This section demonstrates the architecture's behavior under "stacked"
handlers, where the simulation state is itself a product of two
independent sub-states. The single-StateT-layer pattern (with
σ := σ₁ × σ₂) is the most ergonomic way to combine two state-tracking
handlers, because it stays inside the (.arg σ .pure) postcondition
shape that our Std.Do bridge supports cleanly.
The worked example is cachingLoggingOracle, which on every query both:
- logs the query/response pair into the right component, and
- caches the response in the left component (querying the underlying oracle only on a cache miss).
Each per-query specification is a conjunction of the cache invariant
(cache₀ ≤ cache' ∧ cache' t = some v) and the log invariant
(log' = log₀ ++ [⟨t, v⟩]). mvcgen walks composite chains the same
way as for the single-state handlers; only the leaf spec changes shape.
Whole-program lifting via simulateQ_triple_preserves_invariant works
unchanged: the invariant is now I : (QueryCache spec × QueryLog spec) → Prop,
typically a conjunction of one cache property and one log property.
A combined caching + logging handler over a product state.
Behavior on a query t:
- if the cache already has a value
vatt, returnv, leave the cache unchanged, and append⟨t, v⟩to the log; - otherwise sample
vfrom the underlying oracle, install(t, v)into the cache, and append⟨t, v⟩to the log.
The log always grows by exactly one entry per call; the cache grows by at
most one entry per call. Defined in do-notation form so that mvcgen
walks the body directly.
Instances For
Per-call spec for cachingLoggingOracle t: the log is extended by exactly
one entry ⟨t, v⟩, the cache only grows, and the returned value is now
cached at t. Proved purely with mvcgen plus a single bridging step in
the cache-miss branch (where liftM (query t) needs to be brought to
OracleComp.query form so that the support-quantified obligation can be
discharged by a second mvcgen).
Whole-program lift: simulateQ cachingLoggingOracle oa preserves cache
monotonicity for any oa. Derived via the generic
simulateQ_triple_preserves_invariant.
Whole-program lift: simulateQ cachingLoggingOracle oa preserves the
log-prefix invariant (the log only grows).