Research proof index

Support-aware bind congruence: if two continuations agree on all elements in the support of mx, the resulting bind computations are equal.

Converse of log_entry_in_cache_and_mono: when running loggingOracle inside cachingOracle, every cache entry that was not in the initial cache has a corresponding log entry. Combined with log_entry_in_cache_and_mono, this shows that (starting from ∅) the cache entries and log entries have the same set of (input, output) pairs. Proof by stru...

After running cachingOracle on a single query at t, the resulting cache maps t to the returned value.

State-relation transfer for an expected output functional. Let impl : QueryImpl spec (StateT σ ProbComp) and let Rel : σ → σ → Prop be a relation on the handler state. Suppose: * every query step transfers Rel: for Rel-related start states and any Rel-invariant continuation functional K, the per-query expected K agrees at the two states...

Lazy random oracle equals eager full-table sampling , cache-parametrized form. Running oa under the lazy random oracle starting from cache c yields the same output distribution as: sample a full table g : D → R uniformly, then evaluate oa deterministically against the table that overlays c on g. This is the induction vehicle: the cache c...

Marginalized Jensen / Cauchy-Schwarz step for the forking lemma. If a per-element bound acc x · (acc x / q − hinv) ≤ B x holds for every x (with acc x ≤ 1), and we marginalize over the output distribution of any mx : m X with [MonadLiftT m SPMF], then the marginalized expectation μ := ∑' x, Pr[= x | mx] · acc x satisfies the same forking-b...