Rényi-∞ divergence machinery for oracle-bounded reductions - #1076
Draft
Gustavo2622 wants to merge 3 commits into
Draft
Gustavo2622 wants to merge 3 commits into
Gustavo2622 wants to merge 3 commits into
Conversation
strub
force-pushed
the
library_renyi_divergence
branch
from
July 15, 2026 18:49
abd5301 to
5a014e7
Compare
fdupress
reviewed
Jul 15, 2026
| (* Single Iface clone — both top-level access target (consumers use | ||
| [RDO.Iface.Oracle]/[RDO.Iface.Adv]) and BPS substitution target. *) | ||
| clone import BPS_Iface as Iface with | ||
| type out_t = out_t, |
Member
There was a problem hiding this comment.
Use <- to avoid proliferation.
|
|
||
| declare axiom A_bound1 : | ||
| hoare[ A(BPS1.Count(Sampler1)).main : | ||
| BPS1.Count.n = 0 ==> BPS1.Count.n <= N ]. |
Member
There was a problem hiding this comment.
Here you probably want a quantification over the initial value of the counter, so the result can be applied generally where there is a preamble that cannot trigger distinguishing behaviour. (Did we discuss this already? If so, ignore this.)
fdupress
reviewed
Jul 15, 2026
| }. | ||
|
|
||
| module type Adv (O : Oracle) = { | ||
| proc main(p : param_t) : bool |
Member
There was a problem hiding this comment.
We could generalise this to arbitrary return types. This would require replace all the raw res events in probabilities below with a "for all event over res (and perhaps the game's globals)".
Not super clear what value this would add, but the presampling argument certainly doesn't rely on the event being the game's output only.
If you choose to generalise, be careful: if you include the globals in scope, you will need to post-sample unused queries in the lazy version.
strub
force-pushed
the
library_renyi_divergence
branch
from
July 22, 2026 14:21
5a014e7 to
9fa0ec3
Compare
Adds a Rényi-∞ (max-divergence) toolkit for probability-preservation
arguments in bounded-query reductions — e.g. rejection-sampling hops
where each of N oracle queries costs a multiplicative factor M.
- theories/distributions/RDiv.ec: the dominance predicate
[dominated M d1 d2] and the divergence [rdiv_inf], probability
preservation (mu d1 E <= M * mu d2 E), and closure under the standard
constructions (dmap, dlet, dprod, dlist, djoin(map), dexcepted,
drestrict, dcond, dfst/dsnd, dopt, dfold, dfun), each in an
explicit-bound and a tight (rdiv_inf) form. An abstract
[Distinguisher] theory lifts preservation to adversaries
([adv_rdiv_inf], [adv_rdiv_inf_le], pre-composed variants), reusing
SDist.GenDist for the Pr-to-distribution transport.
- theories/distributions/BoundedPreSample.ec: for an adversary making
at most N oracle queries, answering queries by fresh sampling is
Pr-equal, per event, to pre-sampling a list of N draws
([eq_pr_fresh_ref_ev]); proved by a counting/up-to-bad step plus
eager sampling via PROM.
- theories/distributions/RDivOracle.ec: the user-facing bound
[rdiv_bound_sampler],
Pr[Game1(A) : E res] <= M ^ N * Pr[Game2(A) : E res],
for any N-query-bounded A against per-parameter samplers d1/d2 that
are uniformly M-dominated on the support of the parameter
distribution. A second theory [RDivOracleValid] packages the common
"valid parameters only" restriction (conditioning the parameter
distribution), stating validity as an event conjunct — no additive
slack and no M >= 1 assumption — with a corollary paying the
invalid-parameter mass additively.
- tests/rdiv-instantiate.ec: smoke instantiation realizing all
parameter axioms of both oracle theories at a trivial instance.
Gustavo2622
force-pushed
the
library_renyi_divergence
branch
from
September 1, 2026 10:48
9fa0ec3 to
1e10036
Compare
Adds a third theory to RDivOracle.ec for developments where the per-parameter hypotheses hold only on a subset of good SAMPLES, i.e. validity is decided per draw rather than per parameter. The samplers return [None] on an invalid draw, which makes invalidity observable to the adversary, and the core bound then applies to the guarded kernels [dmap (d_i p) (fun x => if valid p x then Some x else None)]. Dominance is required at valid points only, together with dominance of the total invalid mass ([invalid_mass_dominated]); [invalid_mass_of_eq] discharges the common case of equal invalid masses on both sides with [1 <= M]. Everything else (presampling, the joint reflection, the M^N bound) is inherited from [RDivOracle]. Also adds a smoke instantiation of the new theory to tests/rdiv-instantiate.ec.
RDivOracleQ packages the shape where each oracle query first draws an auxiliary value [q] from a fixed distribution, validity is decided on [(p, q)] alone, and the kernels [k_i p q] are only meaningful (and only lossless) at valid [q]: the samplers draw [q], then one draw from the tagged kernel [kt_i p q] (Some (q, x) at valid q, None otherwise). The core bound applies to the tagged kernels; dominance is required at valid (p, q) only, plus [1 <= M] at the shared None mass. Both the one-draw games and PRE-SAMPLED-q games ([GameP_i], the q's drawn as a list up front and consumed in order) are exported, with [GameP_i_eq_Game_i] and the public bound stated on [GameP_i]. The pre-sampled/fresh identification needs no hypothesis on the adversary: BoundedPreSample gains [RefL], a pre-sampled list with a lazy tail, and [eq_pr_fresh_refl], equating it with [Fresh] for every adversary (no query bound, no losslessness) by the eager/lazy step alone. tests/rdiv-instantiate.ec gains a smoke instantiation of RDivOracleQ.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The Rényi-∞ (max-divergence / dominance) machinery for bounded-query reductions: