Query Implementations with State Monads #
This file gives lemmas about QueryImpl spec m when m is something like StateT σ n.
TODO: should generalize things to MonadState once laws for it exist.
Push an outer oracle interpretation through the base monad of a
StateT-valued query implementation.
Instances For
Running a StateT handler and then interpreting its base oracle
computations is the same as first mapping the handler's base through the
outer interpreter.
Output-only corollary of simulateQ_mapStateTBase_run.
Given implementations for oracles in spec₁ and spec₂ in terms of state monads for
two different contexts σ₁ and σ₂, implement the combined set spec₁ + spec₂ in terms
of a combined σ₁ × σ₂ state.
Instances For
Reassociate a nested state transformer into one product state.
The outer state is the first component of the product; the inner/base state is the second component. This is the state-transformer analogue of reassociating handler stacks into an explicit joint state before applying projection lemmas.
Instances For
Indexed version of QueryImpl.parallelStateT. Note that m cannot vary with t.
dtumad: The Function.update thing is nice but forces DecidableEq.
Instances For
Lift a stateful query implementation to a (state × Bool)-stateful version that threads
the boolean (bad) flag unchanged. The output value and updated state come from the
underlying impl; the second Bool component is preserved verbatim across each query.
Instances For
Lift a stateful query implementation to a (state × Bool)-stateful version that OR-updates
the boolean (bad) flag with a predicate f evaluated on the pre-state and produced output.
The flag is monotone: if it was already true, it stays true.
Instances For
Run-shape of withBadFlag: the lifted implementation maps the underlying run by tagging
each (value, state) pair with the unchanged bad flag b.
Run-shape of withBadUpdate: the lifted implementation maps the underlying run by
appending the OR-updated bad flag b || f t s vs.1.
If the state type is Subsingleton, then we can represent simulation in terms of simulate',
adding back any state at the end of the computation.
If a StateT implementation passes every query through unchanged after discarding state
((so t).run' s = query t), then simulating a computation and projecting out the final state
recovers the original computation.
Running a computation under a flattened nested-state implementation is the same as running the original nested computation and reassociating the final states into a product.
Output-only corollary of simulateQ_flattenStateT_run.
Running an adversary-side StateT handler under an outer stateful
interpreter produces the same distribution as the flattened product-state
handler, up to reassociating ((output, localState), outerState) and
(output, (localState, outerState)).
If a StateT oracle implementation preserves distributions (each oracle query produces a
uniform distribution after discarding state), then simulateQ followed by run' preserves
evalDist. This is the key lemma for security proofs: it shows that stateful oracle
implementations (e.g. counting/logging oracles) don't change outcome probabilities.
Stronger version with computational hypothesis: if the implementation passes through
queries exactly, then simulateQ preserves evalDist.
Corollary for probOutput: stateful simulation preserves output probabilities.
Corollary for probEvent: stateful simulation preserves event probabilities.
If two stateful oracle implementations agree on the post-run distribution of every
query (𝒟[(impl₁ t).run s] = 𝒟[(impl₂ t).run s]), then simulating any computation through
either yields the same distribution on the run.
Alias of OracleComp.evalDist_simulateQ_run_congr.
If two stateful oracle implementations agree on the post-run distribution of every
query (𝒟[(impl₁ t).run s] = 𝒟[(impl₂ t).run s]), then simulating any computation through
either yields the same distribution on the run.
Simulating an OracleComp through a stateful implementation in monad m can only shrink the
support: any output reachable after simulation was already reachable in the original computation
(where oracle queries may return any value). This is the support-level analogue of
evalDist_simulateQ_run'_eq_evalDist.
run'-level corollary of simulateQ_bind_map_eq_of_body: if the two bodies of a bind agree
under simulateQ up to a pure post-map f, then so do the run's of the simulated binds from
any initial state.
If all outputs of the original OracleComp are successful (some) and satisfy P, then
the simulated OptionT-wrapped computation satisfies P with probability one. The success
hypothesis is at the level of the original computation's support, which bounds the simulated
support by support_simulateQ_run'_subset.
Bind-prefixed variant of OptionT.probEvent_eq_one_of_simulateQ_support: the simulated
OptionT computation may sample its initial state s₀ from an arbitrary ProbComp σ. Since
support_simulateQ_run'_subset bounds the support uniformly in s₀, the support hypothesis
h (independent of s₀) still discharges both the never-fail and all-outputs-P
obligations.
Properties of Option-valued outputs of an underlying OracleComp propagate to elements
in the support of the simulated, run, and OptionT-wrapped version.