Simulation Semantics through OptionT Handlers #
Distributivity lemmas for simulateQ over OptionT-shaped operations
(Option.elim, Option.elimM, OptionT.bind, OptionT.lift).
These lemmas appeal to the central simulateQ theory in
VCVio.OracleComp.SimSemantics.SimulateQ; the file is grouped under
SimSemantics/OptionT/ to mirror the per-transformer organization used for
StateT, WriterT, and ReaderT.
simulateQ distributes through OptionT.bind, stated via OptionT.run.
Alias of simulateQ_optionT_bind_run.
simulateQ distributes through OptionT.bind, stated via OptionT.run.
simulateQ distributes through OptionT.bind, stated via Option.elimM.
Alias of simulateQ_optionT_bind_elimM.
simulateQ distributes through OptionT.bind, stated via Option.elimM.
simulateQ distributes through OptionT.bind: the simulated OptionT-bind is the
OptionT-bind of the simulated pieces.
simulateQ commutes with OptionT.lift.
mapM over OptionT #
When every step of a mapM resolves to pure (some _) under simulateQ,
the whole mapM resolves to pure (some _) of the pointwise mapped collection.
These are the List and Vector companions to simulateQ_optionT_bind_run /
simulateQ_optionT_lift.
simulateQ over List.mapM in OptionT: when each step is pure (some (g x))
under simulateQ, the whole mapM is pure (some (l.map g)).
simulateQ over Vector.mapM in OptionT: when each step is pure (some (g x))
under simulateQ, the whole mapM is pure (some (xs.map g)).
forIn over OptionT #
The List companions to simulateQ_optionT_bind/_lift for an OptionT-monadic loop.
simulateQ distributes over an OptionT-monadic forIn on a list: the OptionT-loop
sibling of simulateQ_list_forIn. The body lives in OptionT (OracleComp spec), so the loop is
decomposed via simulateQ_optionT_bind (rather than the OracleComp-level simulateQ_bind that
simulateQ_list_forIn uses). Needed to push simulateQ past a verifier's spot-check
for j in List.finRange t do … when that loop is OptionT-monadic.
If under simulateQ every loop body resolves to pure (some (ForInStep.yield init)) (yields
the accumulator unchanged at the initial value), the whole OptionT-monadic forIn resolves to
pure (some init). Discharges a verifier spot-check loop whose body is a sequence of oracle reads
followed by an always-passing guard (under the relevant accept hypothesis). The constant-yield
OptionT companion to simulateQ_list_forIn.
simulateQ maps an OptionT failure (whose run is the underlying pure none) to
failure: the failure companion of simulateQ_pure for OptionT-monadic computations.
Both sides are definitionally pure none, but the failure spelling is what a failed
guard rewrites to in a simulated verifier body.
Failing companion to simulateQ_optionT_forIn_yield_pure_some: if each loop body, under
simulateQ, resolves to pure (some (ForInStep.yield init)) when its per-element condition
cond a holds and to pure none otherwise, and some element of the list fails its
condition, then the whole OptionT-monadic forIn resolves to pure none (the failure
propagates through the remaining OptionT binds). Together the two lemmas characterize a
guarded spot-check loop: pure (some init) iff every condition holds, pure none
otherwise.
Alias of simulateQ_optionT_vector_mapM_pure.
simulateQ over Vector.mapM in OptionT: when each step is pure (some (g x))
under simulateQ, the whole mapM is pure (some (xs.map g)).