From 1e1003600b45d4922ca7aed963a4f433efde58af Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 17 Jun 2026 15:01:44 +0100 Subject: [PATCH] =?UTF-8?q?R=C3=A9nyi-=E2=88=9E=20divergence=20machinery?= =?UTF-8?q?=20for=20oracle-bounded=20reductions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- tests/rdiv-instantiate.ec | 42 ++ theories/distributions/BoundedPreSample.ec | 553 ++++++++++++++ theories/distributions/RDiv.ec | 826 ++++++++++++++++++++ theories/distributions/RDivOracle.ec | 836 +++++++++++++++++++++ 4 files changed, 2257 insertions(+) create mode 100644 tests/rdiv-instantiate.ec create mode 100644 theories/distributions/BoundedPreSample.ec create mode 100644 theories/distributions/RDiv.ec create mode 100644 theories/distributions/RDivOracle.ec diff --git a/tests/rdiv-instantiate.ec b/tests/rdiv-instantiate.ec new file mode 100644 index 000000000..e027b3827 --- /dev/null +++ b/tests/rdiv-instantiate.ec @@ -0,0 +1,42 @@ +(* Smoke instantiation of the Rényi-∞ oracle theories. + + Realizes every parameter axiom of [RDivOracle] and [RDivOracleValid] + at a trivial instance (unit parameter, identical kernels, M = 1), + checking that the two axiom sets are jointly satisfiable — i.e. that + the abstract theories cannot be used to derive an inconsistency. *) + +require import AllCore Distr RDivOracle. + +clone RDivOracle as Triv with + type out_t <- bool, + type param_t <- unit, + op d_param <- dunit tt, + op d1 <- fun (_ : unit) => dunit true, + op d2 <- fun (_ : unit) => dunit true, + op N <- 1, + op M <- 1%r + proof *. +realize d_param_ll by exact dunit_ll. +realize d1_ll by move => *; exact dunit_ll. +realize d2_ll by move => *; exact dunit_ll. +realize N_ge0 by trivial. +realize M_ge0 by trivial. +realize d1_dominated_d2 by move => *; smt(). + +clone RDivOracleValid as TrivV with + type out_t <- bool, + type param_t <- unit, + op d_full <- dunit tt, + op valid <- predT, + op d1 <- fun (_ : unit) => dunit true, + op d2 <- fun (_ : unit) => dunit true, + op N <- 1, + op M <- 1%r + proof *. +realize d_full_ll by exact dunit_ll. +realize d1_ll by move => *; exact dunit_ll. +realize d2_ll by move => *; exact dunit_ll. +realize N_ge0 by trivial. +realize M_ge0 by trivial. +realize d1_dominated_d2 by move => *; smt(). +realize valid_nondegenerate by smt(dunit_ll). diff --git a/theories/distributions/BoundedPreSample.ec b/theories/distributions/BoundedPreSample.ec new file mode 100644 index 000000000..7f94f596c --- /dev/null +++ b/theories/distributions/BoundedPreSample.ec @@ -0,0 +1,553 @@ +(* ========================================================================== + + BoundedPreSample: presampling library for bounded-query sequential + adversaries, parametric over a shared parameter [p : param_t]. The + parameter is NOT hidden from the adversary: the games hand [p] to + [A.main] in the clear (the exported equality holds a fortiori for + parameter-aware adversaries). + + Exports one probability equality per event, [eq_pr_fresh_ref_ev] + (with [eq_pr_fresh_ref] the [res] specialization): + + Pr[G(Fresh, A).main(p) : E res] = Pr[G(Ref, A).main(p) : E res] + + between A run against a bare fresh sampler ([Fresh] draws from [d p] on + every query) and A run against a pre-sampled list of N draws ([Ref] pops + successive elements of a [dlist (d p) N]). + + Hypotheses (section context): [A_bound] — A makes at most N queries — + and [A_ll] — A is lossless whenever its oracle is. Losslessness is not + an afterthought: the internal bridge is an upto-bad step relating + [Fresh] to the [BCount]-guarded sampler, whose bad event ("A asked for + query N+1") has probability 0 precisely because A is N-bounded; the + guarded sampler then ticks in lockstep with list exhaustion, and eager + sampling (via [PROM.FullRO]'s [FullEager.RO_LRO_D]) converts the + guarded fresh draws into the pre-sampled list. + + Module-type sharing: [Oracle] and [Adv] are declared in a nested + sub-theory [Iface], which is cloned into the main theory. Consumers + that clone [BoundedPreSample] multiple times (e.g., for different + distributions [d1], [d2]) can share a single external [Iface] clone + across all uses via [theory I <- ...] substitution, preserving the + nominal identity of [Oracle]/[Adv] across the clones. + + Typical use: clone this theory, instantiate d/N, compose the public + [eq_pr_fresh_ref_ev] lemma with downstream reasoning on the + pre-sampled list (e.g., RDiv.DistinguisherList for Rényi-∞, or direct + coupling arguments). + + ========================================================================== *) + +require import AllCore List Distr DList FMap. + +require (*..*) PROM. + +(* ---- Shared interface: Oracle and Adv module types ---------------------- *) + +abstract theory BPS_Iface. + +type out_t, param_t. + +module type Sampler = { + proc init(_: param_t): unit + proc get(): out_t +}. + +module type Oracle = { + include Sampler [get] +}. + +module type Adv (O : Oracle) = { + proc main(p : param_t) : bool +}. + +end BPS_Iface. +(* NOTE: Iface must contain ONLY types and module types — no concrete + modules (EC clone substitution rejects theories containing modules). + Count lives in the main BoundedPreSample theory. *) + +(* ---- Main theory -------------------------------------------------------- *) + +abstract theory BoundedPreSample. + +type out_t, param_t. + +(* -- Parameters ----------------------------------------------------------- *) + +op d: param_t -> out_t distr. +axiom d_ll p: is_lossless (d p). + +op N : { int | 0 <= N } as N_ge0. + +clone import BPS_Iface as Iface with + type out_t <= out_t, + type param_t <= param_t. +(* Iface sub-theory created; Oracle/Adv in scope via import. *) + +(* Query counter — Count lives outside Iface (EC clone subst limitation). + Per-clone Count.n; consumers state A_bound against their specific + clone's Count (e.g. BPS1.Count for the d1 side). *) +module Count (S : Sampler) = { + var n : int + + proc init(p: param_t) = { + S.init(p); + n <- 0; + } + + proc get() = { + var r; + n <- n + 1; + r <@ S.get(); + return r; + } +}. + +(* -- Public modules ------------------------------------------------------- *) + +(* Fresh sampler (parameter-aware). The parameter [p] is set by the + enclosing game (e.g., [G.main]) before A is invoked. *) +module Fresh : Sampler = { + var p : param_t + + proc init(p') = { + p <- p'; + } + + proc get() = { + var r; + + r <$ d p; + return r; + } +}. + +(* Pre-sampled list consumer. After N pops the list is empty; subsequent + calls return [head witness [] = witness] — same witness-after-exhaust + behavior as BCount. *) +module Ref : Oracle = { + var xs : out_t list + + proc init(p) = { + xs <$ dlist (d p) N; + } + + proc get() = { + var r; + r <- head witness xs; + xs <- behead xs; + return r; + } +}. + +module G (S : Sampler) (A : Adv) = { + proc main(p_val: param_t): bool = { + var r; + + S.init(p_val); + r <@ A(S).main(p_val); + return r; + } +}. + +(* -- Section: main exports ------------------------------------------------ + + PROOF MAP. [eq_pr_fresh_ref] is the composition of a chain of Pr + equalities between [G(-, A)] games; each link below names the local + lemma that proves it and the nature of the argument: + + Fresh the fresh sampler, one draw per query + | [pr_Fresh_BCount] composition of the upto-bad cluster: + | Fresh ≡ FreshC [pr_Fresh_FreshC] (add flag) + | BCount(Fresh) ≡ BCountB [pr_BCount_BCountB] (add flag) + | FreshC ≡ BCountB up to bad [eq_FreshC_BCountB] (upto-bad) + | bad has probability 0 [pr_FreshC_bad0] (by A_bound) + BCount(Fresh) fresh draws, guarded at N queries + | [pr_BCount_ROlazy] lockstep: query i reads RO cell (p, i) + ROSampler(LRO) lazily-sampled indexed RO + | [pr_ROlazy_ROeager] eager sampling [FullEager.RO_LRO_D] + ROSampler(RO) eagerly-sampled indexed RO + | [pr_BCountRef_ROeager] lockstep: cell (p, i) = i-th list entry + BCount(Ref) pre-sampled list, guarded at N + | [final byequiv] guard at N = list exhaustion at N + Ref pre-sampled list + + [eq_pr_fresh_ref_ev] then transports the equality to an arbitrary + event over the boolean result (four cases; needs both games lossless, + which is where [A_ll] earns its keep at the export surface). + ------------------------------------------------------------------------- *) + +section. + +declare module A <: Adv { -Count, -Fresh, -Ref }. + +declare axiom A_ll : + forall (O <: Oracle { -A }), + islossless O.get => islossless A(O).main. + +declare axiom A_bound: + hoare[ A(Count(Fresh)).main : Count.n = 0 ==> Count.n <= N ]. + +(* Bounded-Count wrapper: tick-and-call under a structural guard at N. + Past N calls, returns [witness] — mirrors list exhaustion in Ref. + Internal: consumers only ever see [Fresh], [Ref] and [Count]. *) +local module BCount (O : Sampler) : Sampler = { + proc init(p) = { + Count(O).init(p); + } + + proc get() : out_t = { + var r; + + r <- witness; + if (Count.n < N) { + r <@ Count(O).get(); + } + return r; + } +}. + +local clone import PROM.FullRO as RF with + type in_t <- param_t * int, + type out_t <- out_t, + op dout <- fun (ab : _ * _) => d ab.`1, + type d_in_t <- param_t, + type d_out_t <- bool +proof *. + +local module BadFlag = { + var bad : bool +}. + +local module FreshC : Oracle = { + proc init(p) = { + BadFlag.bad <- false; + Count.n <- 0; + Fresh.init(p); + } + + proc get() : out_t = { + var r; + + r <- witness; + if (Count.n < N) { + Count.n <- Count.n + 1; + r <@ Fresh.get(); + } else { + BadFlag.bad <- true; + r <@ Fresh.get(); + } + return r; + } +}. + +local module BCountB : Oracle = { + proc init(p) = { + BadFlag.bad <- false; + Count.n <- 0; + Fresh.init(p); + } + + proc get() : out_t = { + var r; + + r <- witness; + if (Count.n < N) { + Count.n <- Count.n + 1; + r <@ Fresh.get(); + } else { + BadFlag.bad <- true; + } + return r; + } +}. + +local lemma pr_Fresh_FreshC (p_val : param_t) &m : + Pr[G(Fresh, A).main(p_val) @ &m : res] = + Pr[G(FreshC, A).main(p_val) @ &m : res]. +proof. +byequiv => //; proc. +call (_: ={Fresh.p}). ++ proc *; inline *. + by sp; if{2}; auto. +by inline*; auto. +qed. + +local lemma pr_BCount_BCountB (p_val : param_t) &m : + Pr[G(BCount(Fresh), A).main(p_val) @ &m : res] = + Pr[G(BCountB, A).main(p_val) @ &m : res]. +proof. +byequiv => //; proc. +call (_: ={Fresh.p, Count.n}). ++ by proc; inline *; sp; if; auto. +by inline *; auto. +qed. + +local equiv eq_FreshC_BCountB: + G(FreshC, A).main ~ G(BCountB, A).main: ={glob A, arg} ==> ={BadFlag.bad} /\ (!BadFlag.bad{2} => ={res}). +proof. +proc. +call (: BadFlag.bad + , ={BadFlag.bad, Fresh.p, Count.n} + , ={BadFlag.bad}). ++ exact: A_ll. ++ proc; sp; if=> //. + + by inline *; auto. + + inline *; auto=> |>. + by move=> &0 _ _; exact: d_ll. + + move=> &2 bad; proc; inline *. + by sp; if; auto=> |>; smt(d_ll). + + move=> &1; proc; inline *. + by sp; if; auto=> |>; smt(d_ll). +by inline *; auto=> |> /#. +qed. + +local lemma pr_FreshC_BCountB_good (p_val : param_t) &m : + Pr[G(FreshC, A).main(p_val) @ &m : res /\ !BadFlag.bad] = + Pr[G(BCountB, A).main(p_val) @ &m : res /\ !BadFlag.bad]. +proof. by byequiv eq_FreshC_BCountB=> /#. qed. + +local lemma pr_FreshC_BCountB_bad (p_val : param_t) &m : + Pr[G(FreshC, A).main(p_val) @ &m : BadFlag.bad] = + Pr[G(BCountB, A).main(p_val) @ &m : BadFlag.bad]. +proof. by byequiv eq_FreshC_BCountB=> /#. qed. + +local lemma pr_FreshC_bad0 (p_val : param_t) &m : + Pr[G(FreshC, A).main(p_val) @ &m : BadFlag.bad] = 0%r. +proof. +have hub : + Pr[G(FreshC, A).main(p_val) @ &m : BadFlag.bad] <= + Pr[G(Count(Fresh), A).main(p_val) @ &m : N < Count.n]. ++ byequiv (: ={glob A, arg} ==> BadFlag.bad{1} => N < Count.n{2}) => //; proc. + sp; call(: ={Fresh.p} + /\ Count.n{1} <= Count.n{2} + /\ Count.n{1} <= N + /\ (BadFlag.bad{1} => N < Count.n{2})). + + proc; inline Fresh.get. + seq 1 0 : #pre; 1: by auto. + if {1}; auto; 1:smt(). + by auto=> /#. + by inline *; auto; smt(N_ge0). +have hzero : Pr[G(Count(Fresh), A).main(p_val) @ &m : N < Count.n] = 0%r. ++ byphoare => //; hoare. + proc; call A_bound; inline *; auto. + smt(mu_bounded). +smt(mu_bounded). +qed. + +local lemma pr_FreshC_resbad0 (p_val : param_t) &m : + Pr[G(FreshC, A).main(p_val) @ &m : res /\ BadFlag.bad] = 0%r. +proof. +suff: Pr[G(FreshC, A).main(p_val) @ &m: res /\ BadFlag.bad] + <= Pr[G(FreshC, A).main(p_val) @ &m: BadFlag.bad]. ++ by rewrite (pr_FreshC_bad0 p_val &m); smt(ge0_mu). +by rewrite Pr[mu_sub]. +qed. + +local lemma pr_BCountB_bad0 (p_val : param_t) &m : + Pr[G(BCountB, A).main(p_val) @ &m : BadFlag.bad] = 0%r. +proof. +by rewrite -(pr_FreshC_BCountB_bad p_val &m) (pr_FreshC_bad0 p_val &m). +qed. + +local lemma pr_BCountB_resbad0 (p_val : param_t) &m : + Pr[G(BCountB, A).main(p_val) @ &m : res /\ BadFlag.bad] = 0%r. +proof. +suff: Pr[G(BCountB, A).main(p_val) @ &m: res /\ BadFlag.bad] + <= Pr[G(BCountB, A).main(p_val) @ &m: BadFlag.bad]. ++ by rewrite (pr_BCountB_bad0 p_val &m) #smt:(ge0_mu). +by rewrite Pr[mu_sub]. +qed. + +local lemma pr_Fresh_BCount (p_val : param_t) &m : + Pr[G(Fresh, A).main(p_val) @ &m : res] = + Pr[G(BCount(Fresh), A).main(p_val) @ &m : res]. +proof. +rewrite (pr_Fresh_FreshC p_val &m). +rewrite (pr_BCount_BCountB p_val &m). +rewrite Pr[mu_split BadFlag.bad]. +rewrite eq_sym Pr[mu_split BadFlag.bad] eq_sym. +congr. ++ by rewrite (pr_BCountB_resbad0 p_val &m) (pr_FreshC_resbad0 p_val &m). +exact: pr_FreshC_BCountB_good. +qed. + +local module ROSampler (O : RO) = { + proc init(p) = { + var i; + + Fresh.p <- p; + Count.n <- 0; + O.init(); + + i <- 0; + while (i < N) { + O.sample(p, i); + i <- i + 1; + } + } + + proc get() = { + var r; + + if (Count.n < N) { + r <@ O.get(Fresh.p, Count.n); + Count.n <- Count.n + 1; + } else { + r <- witness; + } + return r; + } +}. + +local lemma pr_BCount_ROlazy p_val &m: + Pr[G(BCount(Fresh), A).main(p_val) @ &m: res] + = Pr[G(ROSampler(LRO), A).main(p_val) @ &m: res]. +proof. +byequiv=> //; proc. +call (: ={Fresh.p, Count.n} + /\ (0 <= Count.n){2} + /\ (forall i, 0 <= i < Count.n <=> (Fresh.p, i) \in RO.m){2}). ++ proc; sp; if; auto=> //. + inline *. + rcondt {2} 3; 1:by auto=> /#. + auto=> |> &2 ge0_n inv n_lt_N r _. + rewrite get_set_sameE //=. + by split=> [/#|i]; rewrite !mem_set // -inv //= /#. +inline *. +kill {2} 6. ++ while (true) (N - i). + + by auto=> |> &2 /#. + by auto=> |> /#. +by auto=> |>; smt(emptyE). +qed. + +local clone DList.ParametricProgram with + type t <- out_t +proof *. + +local module RODist (RO : RO) = { + proc distinguish = G(ROSampler(RO), A).main +}. + +local lemma pr_ROlazy_ROeager p_val &m: + Pr[G(ROSampler(LRO), A).main(p_val) @ &m: res] + = Pr[G(ROSampler(RO), A).main(p_val) @ &m: res]. +proof. +rewrite eq_sym. +byequiv (: ={glob A, glob RO, glob Count, glob Fresh, arg} ==> _)=> //. +conseq (FullEager.RO_LRO_D RODist _)=> |>. +by move=> [] |> +; exact: d_ll. +qed. + +local lemma pr_BCountRef_ROeager p_val &m: + Pr[G(BCount(Ref), A).main(p_val) @ &m: res] + = Pr[G(ROSampler(RO), A).main(p_val) @ &m: res]. +proof. +byequiv=> //; proc. +call (: ={Count.n} + /\ (0 <= Count.n <= N){1} + /\ (forall i, Count.n{2} <= i < N + => RO.m.[Fresh.p, i]{2} = Some (nth witness Ref.xs{1} (i - Count.n){2})) + /\ (forall i, 0 <= i < N <=> (Fresh.p, i) \in RO.m){2}). ++ proc; sp; if; auto=> //. + inline *; rcondf {2} 3; 1:by auto=> /#. + auto=> |> &1 &2 ge0_count _ inv dom_ro count_lt_N. + rewrite d_ll inv //= nth0_head=> /= _ _. + smt(nth_behead). +inline *; wp; sp. +conseq (: _ ==> (forall i, 0 <= i < N + <=> RO.m.[Fresh.p, i]{2} = Some (nth witness Ref.xs i){1}) + /\ (forall i, 0 <= i < N <=> (Fresh.p, i) \in RO.m){2}). ++ by auto=> |>; smt(N_ge0). +proc change {1} 1: [ (i: int) (r0: out_t) ] +{ + Ref.xs <- []; + i <- 0; + while (i < N) { + r0 <$ d p1; + Ref.xs <- Ref.xs ++ [r0]; + i <- i + 1; + } +}. ++ outline {1} 1 ~ ParametricProgram.Sample.sample. + rewrite equiv [{1} 1 ParametricProgram.Sample_LoopSnoc_eq]. + inline {1} ^Ref.xs<@. + by wp; while (={i} /\ l{1} = Ref.xs{2} /\ n{1} = N /\ d{1} = BoundedPreSample.d p1{2}); auto. +while (={i} + /\ p1{1} = p{2} + /\ (p = Fresh.p){2} + /\ (size Ref.xs = i){1} + /\ (forall j, 0 <= j < i{2} <=> RO.m.[Fresh.p, j]{2} = Some (nth witness Ref.xs j){1}) + /\ (0 <= i <= N){1} + /\ (forall j, 0 <= j < i <=> (Fresh.p, j) \in RO.m){2}). ++ rcondt {2} 4; 1:by auto=> /#. + auto=> |> &1 &2 inv ge0_i _ dom_ro i_lt_N r _. + split; 1:by rewrite size_cat. + split=> [j|]; 2:split=> [/#|j]. + + by rewrite get_setE cats1 nth_rcons; case: (j = size Ref.xs{1})=> |> /#. + by rewrite mem_set; case: (j = size Ref.xs{1})=> |> /#. +by auto=> |>; smt(N_ge0 emptyE). +qed. + +lemma eq_pr_fresh_ref p_val &m: + Pr[G(Fresh, A).main(p_val) @ &m: res] + = Pr[G(Ref, A).main(p_val) @ &m: res]. +proof. +rewrite (pr_Fresh_BCount _ &m). +rewrite (pr_BCount_ROlazy _ &m). +rewrite (pr_ROlazy_ROeager _ &m). +rewrite -(pr_BCountRef_ROeager _ &m). +byequiv=> //. +proc; inline *. +call (: ={glob Ref} /\ 0 <= Count.n{1} <= N /\ size Ref.xs{1} = N - Count.n{1}). ++ proc; inline *. + auto=> |> &1 &2 ge0_count size_le_count size_count; split. + + by rewrite size_behead /#. + smt(size_eq0). +by auto=> |> xs; rewrite supp_dlist 1:N_ge0 N_ge0=> - [] ->. +qed. + +(* Event-generic export. [Fresh] and [Ref] are only Pr-equal (the internal + chain crosses an upto-bad step), so a per-event Pr equality is the + strongest exportable form; over the boolean result the four possible + events reduce to [res], [!res] (via losslessness of both games, which + is where [A_ll] earns its keep at the export surface), [true], and + [false]. *) +lemma eq_pr_fresh_ref_ev (E : bool -> bool) p_val &m: + Pr[G(Fresh, A).main(p_val) @ &m: E res] + = Pr[G(Ref, A).main(p_val) @ &m: E res]. +proof. +have F_ll : Pr[G(Fresh, A).main(p_val) @ &m : true] = 1%r. ++ byphoare => //; proc; call (A_ll Fresh _); 1: by proc; auto; smt(d_ll). + by inline *; auto. +have R_ll : Pr[G(Ref, A).main(p_val) @ &m : true] = 1%r. ++ byphoare => //; proc; call (A_ll Ref _); 1: by proc; auto. + by inline *; auto; smt(dlist_ll d_ll N_ge0). +have base := eq_pr_fresh_ref p_val &m. +case (E true) => Et; case (E false) => Ef. ++ have -> : Pr[G(Fresh, A).main(p_val) @ &m : E res] + = Pr[G(Fresh, A).main(p_val) @ &m : true] by rewrite Pr[mu_eq] // /#. + have -> : Pr[G(Ref, A).main(p_val) @ &m : E res] + = Pr[G(Ref, A).main(p_val) @ &m : true] by rewrite Pr[mu_eq] // /#. + by rewrite F_ll R_ll. ++ have -> : Pr[G(Fresh, A).main(p_val) @ &m : E res] + = Pr[G(Fresh, A).main(p_val) @ &m : res] by rewrite Pr[mu_eq] // /#. + have -> : Pr[G(Ref, A).main(p_val) @ &m : E res] + = Pr[G(Ref, A).main(p_val) @ &m : res] by rewrite Pr[mu_eq] // /#. + exact base. ++ have -> : Pr[G(Fresh, A).main(p_val) @ &m : E res] + = Pr[G(Fresh, A).main(p_val) @ &m : !res] by rewrite Pr[mu_eq] // /#. + have -> : Pr[G(Ref, A).main(p_val) @ &m : E res] + = Pr[G(Ref, A).main(p_val) @ &m : !res] by rewrite Pr[mu_eq] // /#. + by rewrite Pr[mu_not] Pr[mu_not] F_ll R_ll base. +have -> : Pr[G(Fresh, A).main(p_val) @ &m : E res] + = Pr[G(Fresh, A).main(p_val) @ &m : false] by rewrite Pr[mu_eq] // /#. +have -> : Pr[G(Ref, A).main(p_val) @ &m : E res] + = Pr[G(Ref, A).main(p_val) @ &m : false] by rewrite Pr[mu_eq] // /#. +by rewrite Pr[mu_false] Pr[mu_false]. +qed. + +end section. + +end BoundedPreSample. diff --git a/theories/distributions/RDiv.ec b/theories/distributions/RDiv.ec new file mode 100644 index 000000000..32ffafe45 --- /dev/null +++ b/theories/distributions/RDiv.ec @@ -0,0 +1,826 @@ +require import AllCore List Distr DProd DList Dexcepted StdBigop StdOrder RealFLub. +require import FinType. +require (*--*) SDist. +(*---*) import Bigreal RealSeries RealOrder RField BRA. + +(* ========================================================================== + + Rényi divergence — max-divergence (α = ∞). + + For subdistributions [d1], [d2], the max-divergence is the supremum of + the pointwise Radon–Nikodym derivative: + + rdiv_inf d1 d2 = sup_x (mu1 d1 x / mu1 d2 x). + + Its flagship property is *probability preservation*: for any event [E], + + mu d1 E <= M * mu d2 E. + + CAVEAT — [rdiv_inf] alone is not the max-divergence. EasyCrypt's + division is total with [x / 0%r = 0%r], so when [d1] is not absolutely + continuous w.r.t. [d2] the supremum does NOT escape to +∞: points where + [mu1 d2 x = 0] contribute ratio 0, and [rdiv_inf d1 d2] evaluates to a + well-defined but cryptographically meaningless finite value — e.g. + [rdiv_inf (duniform [a; b]) (dunit a) = 1%r/2%r] although the true + max-divergence is infinite and probability preservation fails. A bare + inequality [rdiv_inf d1 d2 <= M] therefore carries no guarantee by + itself. The meaningful hypothesis is the predicate [dominated M d1 d2] + ([M >= 0] plus the pointwise bound [mu1 d1 x <= M * mu1 d2 x]): every + lemma below is guarded by it, and downstream developments must state + their assumptions via [dominated] (or pair any [rdiv_inf] bound with a + [dominated] witness), never via bare [rdiv_inf] inequalities. + + Contents: + Definitions — [dominated], [rdiv_inf]. + Section 1 — Dominance and basic bounds. + Section 2 — Probability preservation ([dominated_pr], [rdiv_inf_pr]). + Section 3 — Structural lemmas: dmap, dlet, dprod, dlist, + dexcepted, drestrict, dcond, djoinmap, djoin, + dfst, dsnd, dopt, dlet_dep (dependent kernels), dfold. + [RDivFun] — abstract theory: [dominated_dfun] (+[_cst]), + [rdiv_inf_dfun] (clone with [theory FT <- YourFinType]). + [Distinguisher] — abstract theory: [Sample] game, [Sample_dletE] + (Pr-to-distr transport), [adv_rdiv_inf], + [adv_rdiv_inf_le], fused variants (dmap, dlet, + dexcepted, dcond). + [DistinguisherList] — abstract theory: [adv_rdiv_inf_dlist]. + + Companion file: + [RDivOracle.ec] — oracle-access bound via presampling + ([rdiv_bound_sampler]). + + ========================================================================== *) + +(* -- Dominance predicate --------------------------------------------------- *) + +(* [dominated M d1 d2]: d1 is M-dominated by d2 — the pointwise ratio is + bounded by M. Equivalent to absolute continuity plus a bounded + Radon–Nikodym derivative with explicit bound. *) +pred dominated (M : real) (d1 d2 : 'a distr) = + 0%r <= M /\ forall x, mu1 d1 x <= M * mu1 d2 x. + +(* -- Max-divergence -------------------------------------------------------- *) + +op rdiv_inf (d1 d2 : 'a distr) = + flub (fun x => mu1 d1 x / mu1 d2 x). + +(* ========================================================================== + Section 1 — dominance and basic bounds. + ========================================================================== *) + +lemma dominated_refl (d : 'a distr) : dominated 1%r d d. +proof. by split => // x; rewrite mul1r. qed. + +lemma dominated_ac (M : real) (d1 d2 : 'a distr) x : + dominated M d1 d2 => mu1 d2 x = 0%r => mu1 d1 x = 0%r. +proof. +case => [_ le_mu1] mu2x_eq0. +have := le_mu1 x; rewrite mu2x_eq0 mulr0. +smt(ge0_mu1). +qed. + +lemma has_fub_ratio (M : real) (d1 d2 : 'a distr) : + dominated M d1 d2 => has_fub (fun x => mu1 d1 x / mu1 d2 x). +proof. +case => [ge0_M le_mu1]; exists M => x /=. +case (mu1 d2 x = 0%r) => [-> | ne0]. +- by rewrite invr0 mulr0. +- have pos : 0%r < mu1 d2 x by smt(ge0_mu1). + by rewrite ler_pdivr_mulr //; apply le_mu1. +qed. + +(* The defining sup form, exposed as a rewrite rule. *) +lemma rdiv_infE (d1 d2 : 'a distr) : + rdiv_inf d1 d2 = flub (fun x => mu1 d1 x / mu1 d2 x). +proof. by []. qed. + +lemma rdiv_inf_upper_bound (M : real) (d1 d2 : 'a distr) x : + dominated M d1 d2 => mu1 d1 x <= rdiv_inf d1 d2 * mu1 d2 x. +proof. +move => dom. +have hf := has_fub_ratio M _ _ dom. +have ratio_le : mu1 d1 x / mu1 d2 x <= rdiv_inf d1 d2. + by apply (flub_upper_bound<:'a> (fun x => mu1 d1 x / mu1 d2 x) x). +case (mu1 d2 x = 0%r) => [eq0 | ne0]. +- by rewrite eq0 mulr0 (dominated_ac M _ _ _ dom eq0). +- have pos : 0%r < mu1 d2 x by smt(ge0_mu1). + by rewrite -(ler_pdivr_mulr _ _ _ pos). +qed. + +lemma rdiv_inf_le_ub (d1 d2 : 'a distr) (r : real) : + 0%r <= r => + (forall x, mu1 d1 x <= r * mu1 d2 x) => + rdiv_inf d1 d2 <= r. +proof. +move => ge0_r le_r; apply flub_le_ub => x /=. +case (mu1 d2 x = 0%r) => [eq0 | ne0]. +- have mu1_eq0 : mu1 d1 x = 0%r. + + by have := le_r x; rewrite eq0 mulr0; smt(ge0_mu1). + by rewrite mu1_eq0 eq0 invr0 mulr0. +- have pos : 0%r < mu1 d2 x by smt(ge0_mu1). + by rewrite ler_pdivr_mulr //; apply le_r. +qed. + +(* [rdiv_inf_le]: any explicit M that dominates yields an upper bound. *) +lemma rdiv_inf_le (M : real) (d1 d2 : 'a distr) : + dominated M d1 d2 => rdiv_inf d1 d2 <= M. +proof. by case => [ge0_M le_mu1]; apply rdiv_inf_le_ub. qed. + +lemma rdiv_inf_ge0 (M : real) (d1 d2 : 'a distr) : + dominated M d1 d2 => 0%r <= rdiv_inf d1 d2. +proof. +move => dom. +have hf := has_fub_ratio M _ _ dom. +(* Every value of the ratio is >= 0; pick [witness]. *) +apply (ler_trans (mu1 d1 witness / mu1 d2 witness)); last first. +- by apply (flub_upper_bound<:'a> (fun x => mu1 d1 x / mu1 d2 x) witness). +smt(ge0_mu1 invr_ge0 mulr_ge0). +qed. + +(* The tight dominance witness: [rdiv_inf d1 d2] is itself a valid M. *) +lemma rdiv_inf_dominated (M : real) (d1 d2 : 'a distr) : + dominated M d1 d2 => dominated (rdiv_inf d1 d2) d1 d2. +proof. +move => dom; split. +- exact (rdiv_inf_ge0 M _ _ dom). +- move => x; exact (rdiv_inf_upper_bound M _ _ x dom). +qed. + +(* Reflexive case. When [weight d = 0] the distribution is [dnull] and the + ratio is 0/0 = 0 everywhere, giving rdiv_inf d d = 0, not 1. *) +lemma rdiv_inf_dd (d : 'a distr) : + 0%r < weight d => rdiv_inf d d = 1%r. +proof. +move => pos_w; apply ler_anti; split => [|_]. +- by apply rdiv_inf_le_ub => // x; rewrite mul1r. +(* There exists x0 with mu1 d x0 > 0; at that x0 the ratio is 1. *) +have [x0 pos] : exists x, 0%r < mu1 d x. +- have: 0%r < mu d predT by apply pos_w. + move=> /witness_support [x0 [_ in_d]]. + have ne0 : mu1 d x0 <> 0%r by apply/supportP. + exists x0; rewrite lt0r; split; [exact ne0 | apply ge0_mu1]. +apply (ler_trans (mu1 d x0 / mu1 d x0)); first by smt(divff). +apply (flub_upper_bound<:'a> (fun x => mu1 d x / mu1 d x) x0). +by apply (has_fub_ratio 1%r); exact dominated_refl. +qed. + +(* dnull case. *) +lemma rdiv_inf_dnull (d : 'a distr) : + rdiv_inf dnull<:'a> d = 0%r. +proof. +apply ler_anti; split => [|_]. +- by apply rdiv_inf_le_ub => // x; rewrite mul0r dnull1E. +by apply (rdiv_inf_ge0 0%r); split => // x; rewrite mul0r dnull1E. +qed. + +(* ========================================================================== + Section 2 — probability preservation. + ========================================================================== *) + +(* Direct bound with the user-supplied M. *) +lemma dominated_pr (M : real) (d1 d2 : 'a distr) E : + dominated M d1 d2 => mu d1 E <= M * mu d2 E. +proof. +case => [ge0_M le_mu1]. +rewrite muE (muE d2) -sumZ. +apply ler_sum => [x /= | |]. +- case (E x) => _; last by rewrite mulr0. + exact (le_mu1 x). +- exact/summable_cond/summable_mu1. +- apply (summable_le_pos _ (fun x => M * mu1 d2 x)) => /=. + + exact/summableZ/summable_mu1. + move => x; case (E x) => _; smt(ge0_mu1 mulr_ge0). +qed. + +(* Tight bound via [rdiv_inf]. *) +lemma rdiv_inf_pr (M : real) (d1 d2 : 'a distr) E : + dominated M d1 d2 => mu d1 E <= rdiv_inf d1 d2 * mu d2 E. +proof. +move => dom; exact (dominated_pr _ _ _ _ (rdiv_inf_dominated M _ _ dom)). +qed. + +(* ========================================================================== + Section 3 — data-processing and composition. + + All bounds here are consequences of the pointwise upper bound: + mu1 d1 x <= M * mu1 d2 x + applied to the appropriate event or sum. + + The "dominated" lemma propagates the explicit bound M through the + construction; the "rdiv_inf" lemma gives the tighter bound via + the supremum of the pointwise ratio. + + PROOF DISCIPLINE: every [rdiv_inf_*] bound below is its [dominated_*] + counterpart applied at the tight witness [rdiv_inf d1 d2] (via + [rdiv_inf_dominated]), then closed by [rdiv_inf_le]. No structural + argument is proved twice: to audit a pair, read the [dominated_*] + proof; the [rdiv_inf_*] one is an instance of this single principle. + ========================================================================== *) + +(* -- dmap ------------------------------------------------------------------ *) + +lemma dominated_dmap (M : real) (d1 d2 : 'a distr) (F : 'a -> 'b) : + dominated M d1 d2 => dominated M (dmap d1 F) (dmap d2 F). +proof. +move => dom; split; first by case: dom. +move => b; rewrite !dmap1E. +exact (dominated_pr M _ _ _ dom). +qed. + +lemma rdiv_inf_dmap (M : real) (d1 d2 : 'a distr) (F : 'a -> 'b) : + dominated M d1 d2 => rdiv_inf (dmap d1 F) (dmap d2 F) <= rdiv_inf d1 d2. +proof. +by move => dom; apply/rdiv_inf_le/dominated_dmap/(rdiv_inf_dominated M). +qed. + +(* -- dlet ------------------------------------------------------------------ *) + +(* Pointwise upper bound for [dlet]. Shared by [dominated_dlet] and + [rdiv_inf_dlet]. *) +lemma dlet_pointwise (M : real) (d1 d2 : 'a distr) (F : 'a -> 'b distr) y : + dominated M d1 d2 => + mu1 (dlet d1 F) y <= M * mu1 (dlet d2 F) y. +proof. +case => [ge0_M le_mu1]; rewrite !dlet1E -sumZ. +apply ler_sum => [x /= | |]. +- rewrite mulrA; apply ler_wpmul2r; first exact ge0_mu1. + exact (le_mu1 x). +- by apply summable_mu1_wght => x; smt(ge0_mu1 le1_mu1). +- apply summableZ; apply summable_mu1_wght => x; smt(ge0_mu1 le1_mu1). +qed. + +lemma dominated_dlet (M : real) (d1 d2 : 'a distr) (F : 'a -> 'b distr) : + dominated M d1 d2 => dominated M (dlet d1 F) (dlet d2 F). +proof. +move => dom; split; first by case: dom. +by move => y; apply (dlet_pointwise M). +qed. + +lemma rdiv_inf_dlet (M : real) (d1 d2 : 'a distr) (F : 'a -> 'b distr) : + dominated M d1 d2 => rdiv_inf (dlet d1 F) (dlet d2 F) <= rdiv_inf d1 d2. +proof. +by move => dom; apply/rdiv_inf_le/dominated_dlet/(rdiv_inf_dominated M). +qed. + +(* -- dprod ----------------------------------------------------------------- *) + +lemma dprod_pointwise (Ml Mr : real) (dl1 dl2 : 'a distr) (dr1 dr2 : 'b distr) p : + dominated Ml dl1 dl2 => dominated Mr dr1 dr2 => + mu1 (dl1 `*` dr1) p <= (Ml * Mr) * mu1 (dl2 `*` dr2) p. +proof. +case => [ge0_Ml le_l]; case => [ge0_Mr le_r]. +case: p => a b; rewrite !dprod1E. +have -> : + Ml * Mr * (mu1 dl2 a * mu1 dr2 b) + = (Ml * mu1 dl2 a) * (Mr * mu1 dr2 b) by ring. +by apply ler_pmul; smt(ge0_mu1). +qed. + +lemma dominated_dprod (Ml Mr : real) (dl1 dl2 : 'a distr) (dr1 dr2 : 'b distr) : + dominated Ml dl1 dl2 => dominated Mr dr1 dr2 => + dominated (Ml * Mr) (dl1 `*` dr1) (dl2 `*` dr2). +proof. +move => doml domr; split. +- by case: doml => [??]; case: domr => [??]; apply mulr_ge0. +by move => p; apply (dprod_pointwise Ml Mr). +qed. + +lemma rdiv_inf_dprod (Ml Mr : real) (dl1 dl2 : 'a distr) (dr1 dr2 : 'b distr) : + dominated Ml dl1 dl2 => dominated Mr dr1 dr2 => + rdiv_inf (dl1 `*` dr1) (dl2 `*` dr2) <= rdiv_inf dl1 dl2 * rdiv_inf dr1 dr2. +proof. +move => doml domr; apply rdiv_inf_le. +by apply dominated_dprod; + [exact (rdiv_inf_dominated Ml) | exact (rdiv_inf_dominated Mr)]. +qed. + +(* -- dlist ----------------------------------------------------------------- *) + +lemma dominated_dlist (M : real) (d1 d2 : 'a distr) n : + 0 <= n => dominated M d1 d2 => + dominated (RField.exp M n) (dlist d1 n) (dlist d2 n). +proof. +move => ge0_n dom; elim: n ge0_n => [|n ge0_n IHn]. +- by rewrite !dlist0 // RField.expr0; exact dominated_refl. +rewrite !dlistS // RField.exprS //. +apply dominated_dmap. +exact (dominated_dprod M (RField.exp M n) _ _ _ _ dom IHn). +qed. + +lemma rdiv_inf_dlist (M : real) (d1 d2 : 'a distr) n : + 0 <= n => dominated M d1 d2 => + rdiv_inf (dlist d1 n) (dlist d2 n) <= RField.exp (rdiv_inf d1 d2) n. +proof. +move => ge0_n dom; apply rdiv_inf_le. +by apply dominated_dlist => //; exact (rdiv_inf_dominated M). +qed. + +(* -- dexcepted / drestrict / dcond ---------------------------------------- + + Code-level rejection and conditioning. These come up every time a + cryptographic scheme uses rejection sampling or samples conditional on + an event, and the Rényi cost is simply [1 / (1 - rejection prob)]. *) + +(* [d \ P]: reject [P]-satisfying elements, rescale to weight 1. + Ratio [mu1 (d \ P) x / mu1 d x] is [1/(weight d - mu d P)] for [!P x], + and 0 otherwise. Cite this whenever you have a rejection step. *) +lemma dominated_dexcepted (d : 'a distr) (P : 'a -> bool) : + mu d P < weight d => + dominated (1%r / (weight d - mu d P)) (d \ P) d. +proof. +move => lt_P. +pose M := 1%r / (weight d - mu d P). +have pos_wP : 0%r < weight d - mu d P by rewrite subr_gt0. +have ge0_M : 0%r <= M by rewrite /M; smt(invr_gt0). +split => // x; rewrite dexcepted1E. +case (P x) => _. +- by rewrite /M; smt(ge0_mu1 mulr_ge0 invr_gt0). +by rewrite /M; smt(ge0_mu1). +qed. + +lemma rdiv_inf_dexcepted (d : 'a distr) (P : 'a -> bool) : + mu d P < weight d => + rdiv_inf (d \ P) d <= 1%r / (weight d - mu d P). +proof. +by move => lt_P; exact/rdiv_inf_le/dominated_dexcepted. +qed. + +(* Lossless specialization — the crypto-facing form. For a lossless [d] + with rejection probability [mu d P], the Rényi-∞ cost is [1/Pr[!P]]. *) +lemma rdiv_inf_dexcepted_ll (d : 'a distr) (P : 'a -> bool) : + is_lossless d => mu d P < 1%r => + rdiv_inf (d \ P) d <= 1%r / (1%r - mu d P). +proof. +move => ll_d lt_P; have := rdiv_inf_dexcepted d P _; smt(). +qed. + +(* [drestrict d P]: zero out [!P], no rescaling — stays sub-distribution. + Trivially dominated by [d]. *) +lemma dominated_drestrict (d : 'a distr) (P : 'a -> bool) : + dominated 1%r (drestrict d P) d. +proof. +split => // x; rewrite drestrict1E mul1r. +by case (P x) => _; smt(ge0_mu1). +qed. + +lemma rdiv_inf_drestrict (d : 'a distr) (P : 'a -> bool) : + rdiv_inf (drestrict d P) d <= 1%r. +proof. +exact/rdiv_inf_le/dominated_drestrict. +qed. + +(* [dcond d P = dscale (drestrict d P)]: condition on [P] (normalize). + Equivalent to [d \ (predC P)]. *) +lemma dominated_dcond (d : 'a distr) (P : 'a -> bool) : + 0%r < mu d P => + dominated (1%r / mu d P) (dcond d P) d. +proof. +move => pos_P. +pose M := 1%r / mu d P. +have ge0_M : 0%r <= M by rewrite /M; smt(invr_gt0). +split => // x; rewrite dcond1E. +case (P x) => _. +- by rewrite /M; smt(ge0_mu1 mulr_ge0 invr_gt0). +by rewrite /M; smt(ge0_mu1 mulr_ge0). +qed. + +lemma rdiv_inf_dcond (d : 'a distr) (P : 'a -> bool) : + 0%r < mu d P => + rdiv_inf (dcond d P) d <= 1%r / mu d P. +proof. +by move => pos_P; exact/rdiv_inf_le/dominated_dcond. +qed. + +(* -- djoinmap ------------------------------------------------------------- + + [djoinmap F xs = djoin (map F xs)]: the heterogeneous product of a list + of distributions indexed by [xs]. Generalizes [dlist] (which is the + homogeneous case). The Rényi cost multiplies across indices; the + per-index bounds [Mf x] need not be uniform ([_cst] gives the uniform + corollary with cost [M ^ size xs]). *) +lemma dominated_djoinmap ['a 'b] (Mf : 'a -> real) (F1 F2 : 'a -> 'b distr) (xs : 'a list) : + (forall x, x \in xs => dominated (Mf x) (F1 x) (F2 x)) => + dominated (BRM.big predT Mf xs) (djoinmap F1 xs) (djoinmap F2 xs). +proof. +elim: xs => [_|x xs IHxs dom_cons] /=. +- by rewrite BRM.big_nil; exact dominated_refl. +have dom_head := dom_cons x _; first by rewrite mem_head. +have dom_tail : dominated (BRM.big predT Mf xs) (djoinmap F1 xs) (djoinmap F2 xs). +- by apply IHxs => y y_in; apply dom_cons; rewrite in_cons y_in. +rewrite !djoin_cons BRM.big_cons /predT /=. +apply dominated_dmap. +exact (dominated_dprod (Mf x) (BRM.big predT Mf xs) _ _ _ _ dom_head dom_tail). +qed. + +lemma dominated_djoinmap_cst ['a 'b] (M : real) (F1 F2 : 'a -> 'b distr) (xs : 'a list) : + (forall x, x \in xs => dominated M (F1 x) (F2 x)) => + dominated (RField.exp M (size xs)) (djoinmap F1 xs) (djoinmap F2 xs). +proof. +move => dom. +have := dominated_djoinmap (fun _ => M) F1 F2 xs dom. +by rewrite mulr_const. +qed. + +lemma rdiv_inf_djoinmap ['a 'b] (Mf : 'a -> real) (F1 F2 : 'a -> 'b distr) (xs : 'a list) : + (forall x, x \in xs => dominated (Mf x) (F1 x) (F2 x)) => + rdiv_inf (djoinmap F1 xs) (djoinmap F2 xs) <= + BRM.big predT (fun x => rdiv_inf (F1 x) (F2 x)) xs. +proof. +move => dom; apply rdiv_inf_le. +apply (dominated_djoinmap (fun x => rdiv_inf (F1 x) (F2 x))) => x x_in /=. +exact (rdiv_inf_dominated (Mf x) _ _ (dom x x_in)). +qed. + +(* -- djoin ---------------------------------------------------------------- + + [djoin (ds : 'a distr list) : 'a list distr] is the heterogeneous + product of a list of distributions. One-line corollary of djoinmap + via the identity realization. *) + +lemma djoinmap_nth ['a] (ds : 'a distr list) : + djoinmap (fun i => nth witness ds i) (range 0 (size ds)) = djoin ds. +proof. by congr; apply map_nth_range. qed. + +lemma dominated_djoin ['a] (M : real) (ds1 ds2 : 'a distr list) : + size ds1 = size ds2 => + (forall i, 0 <= i < size ds1 => + dominated M (nth witness ds1 i) (nth witness ds2 i)) => + dominated (RField.exp M (size ds1)) (djoin ds1) (djoin ds2). +proof. +move => eq_sz dom_pt. +rewrite -(djoinmap_nth ds1) -(djoinmap_nth ds2) -eq_sz. +have -> : RField.exp M (size ds1) + = RField.exp M (size (range 0 (size ds1))). +- by congr; rewrite size_range; smt(size_ge0). +by apply dominated_djoinmap_cst => i /mem_range rg_i; exact (dom_pt i rg_i). +qed. + +lemma rdiv_inf_djoin ['a] (M : real) (ds1 ds2 : 'a distr list) : + size ds1 = size ds2 => + (forall i, 0 <= i < size ds1 => + dominated M (nth witness ds1 i) (nth witness ds2 i)) => + rdiv_inf (djoin ds1) (djoin ds2) <= + BRM.big predT (fun i => rdiv_inf (nth witness ds1 i) (nth witness ds2 i)) + (range 0 (size ds1)). +proof. +move => eq_sz dom_pt. +rewrite -(djoinmap_nth ds1) -(djoinmap_nth ds2) -eq_sz. +by apply (rdiv_inf_djoinmap (fun _ => M)) => i /mem_range rg_i; exact (dom_pt i rg_i). +qed. + +(* -- dfst / dsnd --------------------------------------------------------- + + Marginals of a pair distribution. Trivially follows from dmap. *) + +lemma dominated_dfst ['a 'b] (M : real) (d1 d2 : ('a * 'b) distr) : + dominated M d1 d2 => dominated M (dfst d1) (dfst d2). +proof. exact (dominated_dmap M _ _ fst). qed. + +lemma rdiv_inf_dfst ['a 'b] (M : real) (d1 d2 : ('a * 'b) distr) : + dominated M d1 d2 => rdiv_inf (dfst d1) (dfst d2) <= rdiv_inf d1 d2. +proof. exact (rdiv_inf_dmap M _ _ fst). qed. + +lemma dominated_dsnd ['a 'b] (M : real) (d1 d2 : ('a * 'b) distr) : + dominated M d1 d2 => dominated M (dsnd d1) (dsnd d2). +proof. exact (dominated_dmap M _ _ snd). qed. + +lemma rdiv_inf_dsnd ['a 'b] (M : real) (d1 d2 : ('a * 'b) distr) : + dominated M d1 d2 => rdiv_inf (dsnd d1) (dsnd d2) <= rdiv_inf d1 d2. +proof. exact (rdiv_inf_dmap M _ _ snd). qed. + +(* -- dopt ---------------------------------------------------------------- + + [dopt d : 'a option distr] adds a [None] branch with the remaining + mass [1 - weight d]. If [d2]'s weight is at most [d1]'s (so [dopt d1] + puts no more mass on [None] than [dopt d2] does), dominance is + preserved up to [maxr 1%r M] — the [None] branch may need factor 1 + even when [M < 1]. *) + +lemma dominated_dopt (M : real) (d1 d2 : 'a distr) : + weight d2 <= weight d1 => + dominated M d1 d2 => + dominated (maxr 1%r M) (dopt d1) (dopt d2). +proof. +move => le_w dom. +case: dom => [ge0_M le_mu1]; split; first smt(). +case => [|y]; rewrite !dopt1E /=. +- smt(mu_bounded). +apply (ler_trans (M * mu1 d2 y)); first exact (le_mu1 y). +apply ler_wpmul2r; smt(ge0_mu1). +qed. + +lemma rdiv_inf_dopt (M : real) (d1 d2 : 'a distr) : + weight d2 <= weight d1 => + dominated M d1 d2 => + rdiv_inf (dopt d1) (dopt d2) <= maxr 1%r (rdiv_inf d1 d2). +proof. +move => le_w dom; apply rdiv_inf_le. +by apply dominated_dopt => //; exact (rdiv_inf_dominated M). +qed. + +(* -- Dependent-kernel dlet dominance -------------------------------------- + + Strengthens [dominated_dlet] to allow the kernel to differ between the + two sides, at the cost of a *uniform* pointwise bound on the kernel (a + single constant [Mf]). The kernel bound is only required on the + support of [d1] — parameterized families are typically dominated only + at well-formed parameters. *) + +lemma dominated_dlet_dep ['a 'b] (Md Mf : real) (d1 d2 : 'a distr) (F1 F2 : 'a -> 'b distr) : + 0%r <= Mf => + dominated Md d1 d2 => + (forall x, x \in d1 => dominated Mf (F1 x) (F2 x)) => + dominated (Md * Mf) (dlet d1 F1) (dlet d2 F2). +proof. +move => ge0_Mf; case => [ge0_Md dom_d] dom_F. +split; first by apply mulr_ge0. +move => y; rewrite !dlet1E -sumZ. +apply ler_sum => [x /= | |]. +- case (x \in d1) => [x_in | x_nin]; last first. + + have -> : mu1 d1 x = 0%r by smt(supportP). + by rewrite mul0r; smt(ge0_mu1 mulr_ge0). + have h1 := dom_d x. + have [_ h2] := dom_F x x_in; have h2' := h2 y. + have : mu1 d1 x * mu1 (F1 x) y <= (Md * mu1 d2 x) * (Mf * mu1 (F2 x) y). + + by apply ler_pmul; smt(ge0_mu1). + by rewrite mulrACA. +- apply summable_mu1_wght => x; smt(ge0_mu1 le1_mu1). +- apply summableZ; apply summable_mu1_wght => x; smt(ge0_mu1 le1_mu1). +qed. + +(* -- dfold --------------------------------------------------------------- + + [dfold f x n] iterates [f] for [n] steps starting from [x]. Analogue + of [dlist] for state-carrying iteration. The Rényi cost composes + multiplicatively over the loop. *) + +(* Dominance of [dfold] under step-wise domination. The per-step bound + [Ms i] dominates the i-th step's kernel at every accumulator value + *reachable* by the first i steps ([y \in dfold f1 x i]) — unreachable + states need no bound. Conclusion: the product of step-wise bounds. *) +lemma dominated_dfold ['a] (f1 f2 : int -> 'a -> 'a distr) (x : 'a) (n : int) + (Ms : int -> real) : + 0 <= n => + (forall i, 0 <= i < n => + 0%r <= Ms i /\ + forall y, y \in dfold f1 x i => + forall z, mu1 (f1 i y) z <= Ms i * mu1 (f2 i y) z) => + dominated (BRM.big predT Ms (range 0 n)) (dfold f1 x n) (dfold f2 x n). +proof. +move => ge0_n; elim: n ge0_n => [|n ge0_n IHn] step. +- by rewrite !dfold0 range_geq // BRM.big_nil; exact dominated_refl. +rewrite !dfoldS // BRM.big_int_recr //. +have IH := IHn _; first by move => i rng_i; apply step; smt(). +have [ge0_Mn step_n] := step n _; first smt(). +apply (dominated_dlet_dep (BRM.big predT Ms (range 0 n)) (Ms n) _ _ _ _ ge0_Mn IH). +by move => y y_in; split => //; exact (step_n y y_in). +qed. + +(* rdiv_inf bound for dfold — corollary of [dominated_dfold]. *) +lemma rdiv_inf_dfold ['a] (f1 f2 : int -> 'a -> 'a distr) (x : 'a) (n : int) + (Ms : int -> real) : + 0 <= n => + (forall i, 0 <= i < n => + 0%r <= Ms i /\ + forall y, y \in dfold f1 x i => + forall z, mu1 (f1 i y) z <= Ms i * mu1 (f2 i y) z) => + rdiv_inf (dfold f1 x n) (dfold f2 x n) <= BRM.big predT Ms (range 0 n). +proof. +move => ge0_n step. +exact (rdiv_inf_le _ _ _ (dominated_dfold f1 f2 x n Ms ge0_n step)). +qed. + +(* -- dfun ---------------------------------------------------------------- + + [dfun F : (t -> 'u) distr] samples a function over a finite domain + [t] by sampling [F x] at each point independently. Rényi multiplies + across the domain. [dfun] requires a [FinType] on [t], so unlike + the structural lemmas above this is an abstract theory. Clone with + [theory FT <- YourFinType]; the internal [MUniFinFun] is wired + automatically. If [YourFinType] is itself a direct [FinType] clone, + instantiate its [t] with [<=], not [<-]: the outer [theory FT <- ...] + matches on [t], and [<-] clears the very symbol it matches on. (A + clone that only substitutes *upstream* parameters is unaffected — e.g. + [FinProdType with type t1 <- ..., type t2 <- ...] leaves [t] intact.) + See the [Iface] clone in [RDivOracle.ec] for a worked instance. *) + +abstract theory RDivFun. + clone FinType as FT. + + clone import MUniFinFun with + type t <- FT.t, + theory FinT <- FT + proof *. + + lemma dominated_dfun ['u] (Mf : FT.t -> real) (F1 F2 : FT.t -> 'u distr) : + (forall x, dominated (Mf x) (F1 x) (F2 x)) => + dominated (BRM.big predT Mf FT.enum) (dfun F1) (dfun F2). + proof. + move => dom_pt; rewrite !dfun_dmap; apply dominated_dmap. + by apply dominated_djoinmap => x _; exact (dom_pt x). + qed. + + lemma dominated_dfun_cst ['u] (M : real) (F1 F2 : FT.t -> 'u distr) : + (forall x, dominated M (F1 x) (F2 x)) => + dominated (RField.exp M (size FT.enum)) (dfun F1) (dfun F2). + proof. + move => dom_pt. + have := dominated_dfun (fun _ => M) F1 F2 dom_pt. + by rewrite mulr_const. + qed. + + lemma rdiv_inf_dfun ['u] (M : real) (F1 F2 : FT.t -> 'u distr) : + (forall x, dominated M (F1 x) (F2 x)) => + rdiv_inf (dfun F1) (dfun F2) <= + BRM.big predT (fun x => rdiv_inf (F1 x) (F2 x)) FT.enum. + proof. + move => dom_pt; apply rdiv_inf_le. + apply (dominated_dfun (fun x => rdiv_inf (F1 x) (F2 x))) => x /=. + exact (rdiv_inf_dominated M _ _ (dom_pt x)). + qed. + +end RDivFun. + +(* ========================================================================== + Section 4 — Distinguisher layer. + + Lifts probability preservation from events to adversaries. The main + lemma [adv_rdiv_inf] says: + + Pr[Sample(A).main(d1) @ &m : P res] + <= rdiv_inf d1 d2 * Pr[Sample(A).main(d2) @ &m : P res]. + + Design: + - Generic output type [out_t], not just bool — events [P : out_t -> bool] + transport through unchanged. + - Distributions are [main] arguments, not theory parameters, so a single + clone serves every pair of distributions. + - The Pr-to-distr transport machinery ([S], [sampleE], [adv_isdistr], + [adv_mu1]) is reused from [SDist.GenDist] rather than re-proved. + ========================================================================== *) + +abstract theory Distinguisher. +type in_t, out_t. + +module type Dist = { + proc guess(x : in_t) : out_t +}. + +(* Pr-to-distr transport: [S], [sampleE], [uniq_big_res], [adv_isdistr], + [adv_mu1]. [GD.Distinguisher] is structurally identical to [Dist]. *) +clone import SDist.GenDist as GD with + type in_t <- in_t, + type out_t <- out_t + proof*. + +clone import DProd.DLetSampling as DLS with + type t <- in_t, + type u <- out_t + proof*. + +(* The sample-then-distinguish game. Users reshape their concrete + adversaries into this shape to cite [adv_rdiv_inf]. *) +module Sample (A : Dist) = { + proc main(d : in_t distr) = { + var x, r; + + x <$ d; + r <@ A.guess(x); + return r; + } +}. + +(* Main transport lemma: the adversary game reduces to a [dlet]. + The continuation [F x] is the output distribution of [A.guess(x)]. *) +lemma Sample_dletE (A <: Dist) (P : out_t -> bool) &m d' : + Pr[Sample(A).main(d') @ &m : P res] = + mu (dlet d' (fun x => mk (fun z => Pr[A.guess(x) @ &m : res = z]))) P. +proof. +pose F := fun x => mk (fun z => Pr[A.guess(x) @ &m : res = z]). +have -> : Pr[Sample(A).main(d') @ &m : P res] = + Pr[SampleDep.sample(d', F) @ &m : P res]. +- byequiv => //; proc. + seq 1 1 : ((glob A){1} = (glob A){m} /\ du{2} = F /\ x{1} = t{2}); first by auto. + outline {2} 1 ~ S.sample. + call (: d{2} = (F x){1} /\ (glob A){1} = (glob A){m} ==> ={res}). + bypr (res{1}) (res{2}); first smt(). + move => &1 &2 a [-> eq_globA]; rewrite sampleE -(adv_mu1 A). + byequiv (: ={x, glob A} ==> ={res}) => //; 1: by sim. + by auto. +have -> : Pr[SampleDep.sample(d', F) @ &m : P res] = + Pr[SampleDLet.sample(d', F) @ &m : P res]. +- by byequiv => //; conseq SampleDepDLet; move: F; auto. +byphoare (: dt = d' /\ du = F ==> _) => //; proc. +by rnd; skip => /> &1 -> ->. +qed. + +(* Flagship: probability preservation at the adversary level. *) +lemma adv_rdiv_inf (A <: Dist) (P : out_t -> bool) &m (M : real) (d1 d2 : in_t distr) : + dominated M d1 d2 => + Pr[Sample(A).main(d1) @ &m : P res] <= + rdiv_inf d1 d2 * Pr[Sample(A).main(d2) @ &m : P res]. +proof. +move => dom. +rewrite !(Sample_dletE A). +pose F := fun x => mk (fun z => Pr[A.guess(x) @ &m : res = z]). +apply (ler_trans (rdiv_inf (dlet d1 F) (dlet d2 F) * mu (dlet d2 F) P)). +- exact (rdiv_inf_pr M _ _ P (dominated_dlet M _ _ F dom)). +apply ler_wpmul2r; first exact ge0_mu. +exact (rdiv_inf_dlet M _ _ F dom). +qed. + +(* [adv_rdiv_inf] with the divergence replaced by any explicit upper + bound — the form every composed variant below reduces to. *) +lemma adv_rdiv_inf_le (A <: Dist) (P : out_t -> bool) &m + (M r : real) (d1 d2 : in_t distr) : + dominated M d1 d2 => rdiv_inf d1 d2 <= r => + Pr[Sample(A).main(d1) @ &m : P res] <= + r * Pr[Sample(A).main(d2) @ &m : P res]. +proof. +move => dom le_r. +apply (ler_trans (rdiv_inf d1 d2 * Pr[Sample(A).main(d2) @ &m : P res])). +- exact (adv_rdiv_inf A P &m M _ _ dom). +by apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +qed. + +(* -- Pre-composed adversary bounds ---------------------------------------- + + Fuse [adv_rdiv_inf] with the structural lemmas so users cite a single + composed result instead of chaining three applications. *) + +lemma adv_rdiv_inf_dmap ['a] (A <: Dist) (P : out_t -> bool) &m + (M : real) (G : 'a -> in_t) (d1 d2 : 'a distr) : + dominated M d1 d2 => + Pr[Sample(A).main(dmap d1 G) @ &m : P res] <= + rdiv_inf d1 d2 * Pr[Sample(A).main(dmap d2 G) @ &m : P res]. +proof. +move => dom; apply (adv_rdiv_inf_le A P &m M). +- exact (dominated_dmap M). +- exact (rdiv_inf_dmap M). +qed. + +lemma adv_rdiv_inf_dlet ['a] (A <: Dist) (P : out_t -> bool) &m + (M : real) (G : 'a -> in_t distr) (d1 d2 : 'a distr) : + dominated M d1 d2 => + Pr[Sample(A).main(dlet d1 G) @ &m : P res] <= + rdiv_inf d1 d2 * Pr[Sample(A).main(dlet d2 G) @ &m : P res]. +proof. +move => dom; apply (adv_rdiv_inf_le A P &m M). +- exact (dominated_dlet M). +- exact (rdiv_inf_dlet M). +qed. + +(* Rejection sampling: the sample source is [d \ Q] — the adversary sees + a sample from [d] restricted to [!Q] and rescaled. The cost is + [1/(weight d - mu d Q)], i.e., the inverse acceptance probability. *) +lemma adv_rdiv_inf_dexcepted (A <: Dist) (P : out_t -> bool) &m + (d : in_t distr) (Q : in_t -> bool) : + mu d Q < weight d => + Pr[Sample(A).main(d \ Q) @ &m : P res] <= + (1%r / (weight d - mu d Q)) * Pr[Sample(A).main(d) @ &m : P res]. +proof. +move => lt_Q; apply (adv_rdiv_inf_le A P &m (1%r / (weight d - mu d Q))). +- exact dominated_dexcepted. +- exact rdiv_inf_dexcepted. +qed. + +(* Sampling conditioned on [Q]: the adversary sees a sample from [dcond]. + Cost is [1/mu d Q] — inverse conditioning probability. *) +lemma adv_rdiv_inf_dcond (A <: Dist) (P : out_t -> bool) &m + (d : in_t distr) (Q : in_t -> bool) : + 0%r < mu d Q => + Pr[Sample(A).main(dcond d Q) @ &m : P res] <= + (1%r / mu d Q) * Pr[Sample(A).main(d) @ &m : P res]. +proof. +move => pos_Q; apply (adv_rdiv_inf_le A P &m (1%r / mu d Q)). +- exact dominated_dcond. +- exact rdiv_inf_dcond. +qed. + +end Distinguisher. + +(* Pre-composed dlist bound. [dlist] fixes the sample type to a list, + so it lives in a separate sub-theory that clones [Distinguisher] at + [in_t <- t list]. *) +abstract theory DistinguisherList. +type t, out_t. + +clone import Distinguisher as DL with + type in_t <- t list, + type out_t <- out_t + proof*. + +lemma adv_rdiv_inf_dlist (A <: DL.Dist) (P : out_t -> bool) &m + (M : real) (d1 d2 : t distr) n : + 0 <= n => dominated M d1 d2 => + Pr[DL.Sample(A).main(dlist d1 n) @ &m : P res] <= + RField.exp (rdiv_inf d1 d2) n + * Pr[DL.Sample(A).main(dlist d2 n) @ &m : P res]. +proof. +move => ge0_n dom. +apply (DL.adv_rdiv_inf_le A P &m (RField.exp M n)). +- exact (dominated_dlist M). +- exact (rdiv_inf_dlist M). +qed. + +end DistinguisherList. diff --git a/theories/distributions/RDivOracle.ec b/theories/distributions/RDivOracle.ec new file mode 100644 index 000000000..493404bc6 --- /dev/null +++ b/theories/distributions/RDivOracle.ec @@ -0,0 +1,836 @@ +(* ========================================================================== + + Rényi-∞ oracle bound for bounded-query sequential adversaries, + PARAMETRIC over a shared parameter [p : param_t]. The parameter is + NOT hidden from the adversary: the games pass [p] to [A.main] in the + clear (the bound holds a fortiori for parameter-aware adversaries). + + User-facing lemma [rdiv_bound_sampler] concludes, for any event + [E : bool -> bool] and any A that makes at most N sampler queries + ([A_bound1]/[A_bound2]) and is lossless whenever its oracle is + ([A_ll]): + + Pr[Game1(A).main @ &m : E res] <= M ^ N * Pr[Game2(A).main @ &m : E res] + + where: + - [Game_i] samples [p <$ d_param], sets [Sampler_i.p := p], then runs A. + - [Sampler_i.get] returns a fresh draw from [d_i p] for every [p] the + game can draw (its literal kernel is the classically totalized + [dtot_i], equal to [d_i] on [supp d_param] — see the plumbing note). + - [M] is an explicit uniform dominance witness: + forall p ∈ supp d_param, forall x, mu1 (d1 p) x ≤ M * mu1 (d2 p) x. + - [N] is A's query budget. + All per-parameter hypotheses ([d_i_ll], dominance) are required only on + [supp d_param]; restricting to a subset of good parameters is done by + conditioning [d_param] ([RDivOracleValid] packages exactly that). + + Non-parametric specialization: + [param_t := unit, d_param := dunit (), d1 := fun _ => d, d2 := fun _ => d']. + + ARCHITECTURE: presampling is fully delegated to [BoundedPreSample.ec]. + BPS1, BPS2 (clones for d1, d2) provide the [eq_pr_fresh_ref_ev] + Pr-equality between fresh-sampling and pre-sampled-list games. Two + clones share [Iface] (Oracle/Adv module types) so a single [A] applies. + + The internal chain routes through JOINT distributions — the per-p + fresh≡ref equality cannot be lifted through the p-sampling directly: + + Game1(A) + ≡ [Game1_eq_Joint1] + (couple the p-draw; per-p [BPS1.eq_pr_fresh_ref_ev] via bypr) + G_Joint1 — p <$ d_param; xs <$ dlist (dtot1 p) N; run A on BPS1.Ref + ≡ [G_Joint1_vs_Sample] (shape rename) + Sample(B).main(joint1), + joint1 = dlet d_param (fun p => dmap (dlist (dtot1 p) N) + (fun xs => (p, xs))) + + (and mirrored on side 2 with 1 -> 2 in every name). One + [adv_rdiv_inf_le] application on the joints ([Joint_rdiv_bound]) closes + the bound: [joint_pt_bound] gives [rdiv_inf joint1 joint2 <= M ^ N] + pointwise, the [d_param] marginal cancelling in the ratio; the public + [rdiv_bound_sampler] is the composition of the three steps. + + ========================================================================== *) + +require import AllCore List Distr DList StdOrder StdBigop RealSeries. +require import RDiv. +require import BoundedPreSample. +(*---*) import RField RealOrder Bigreal.BRA. + +abstract theory RDivOracle. + +(* -- Parameters ----------------------------------------------------------- *) + +type out_t. +type param_t. + +(* Single Iface clone — both top-level access target (consumers use + [RDO.Iface.Oracle]/[RDO.Iface.Adv]) and BPS substitution target. + [<=] (inline-and-keep), not [<-]: the symbols must survive the clone + because [theory Iface <- Iface] below matches BPS's own [Iface] + structurally, and [<-] would clear the very names it matches on. *) +clone import BPS_Iface as Iface with + type out_t <= out_t, + type param_t <= param_t. + +op [lossless] d_param : param_t distr. + +op d1 : param_t -> out_t distr. +op d2 : param_t -> out_t distr. + +(* Per-parameter hypotheses are required only on the support of [d_param] + — the parameters the games can actually draw. Restricting the theorem + to a subset of "good" parameters is therefore an *instantiation*: + condition [d_param] (see [RDivOracleValid] below for the packaged + valid-predicate surface). *) +axiom d1_ll : forall p, p \in d_param => is_lossless (d1 p). +axiom d2_ll : forall p, p \in d_param => is_lossless (d2 p). + +op N : { int | 0 <= N } as N_ge0. +op M : { real | 0%r <= M } as M_ge0. + +axiom d1_dominated_d2 : + forall p, p \in d_param => + forall x, mu1 (d1 p) x <= M * mu1 (d2 p) x. + +(* -- Internal plumbing: totalized kernels --------------------------------- + BPS demands losslessness at EVERY parameter (its eager-sampling engine + indexes a PROM by all (p, i) pairs), while [d1_ll]/[d2_ll] speak only + about [supp d_param]. [dtot_i] bridges the gap classically, defaulting + to [dunit witness] wherever [d_i] is lossy — which, by [d_i_ll], can + only happen outside [supp d_param], where the games never sample. On + [supp d_param], [Sampler_i.get] draws exactly [d_i p]. *) +op dtot1 = fun p => if is_lossless (d1 p) then d1 p else dunit witness. +op dtot2 = fun p => if is_lossless (d2 p) then d2 p else dunit witness. + +lemma dtot1_ll p : is_lossless (dtot1 p). +proof. by rewrite /dtot1; case (is_lossless (d1 p)) => // _; exact dunit_ll. qed. + +lemma dtot2_ll p : is_lossless (dtot2 p). +proof. by rewrite /dtot2; case (is_lossless (d2 p)) => // _; exact dunit_ll. qed. + +lemma dtot1E p : p \in d_param => dtot1 p = d1 p. +proof. by move => p_in; rewrite /dtot1 (d1_ll p p_in). qed. + +lemma dtot2E p : p \in d_param => dtot2 p = d2 p. +proof. by move => p_in; rewrite /dtot2 (d2_ll p p_in). qed. + +(* -- BoundedPreSample clones ---------------------------------------------- *) + +clone BoundedPreSample as BPS1 with + type out_t <- out_t, + type param_t <- param_t, + theory Iface <- Iface, + op d <- dtot1, + op N <- N + proof *. +realize d_ll by exact dtot1_ll. +realize N_ge0 by exact N_ge0. + +clone BoundedPreSample as BPS2 with + type out_t <- out_t, + type param_t <- param_t, + theory Iface <- Iface, + op d <- dtot2, + op N <- N + proof *. +realize d_ll by exact dtot2_ll. +realize N_ge0 by exact N_ge0. + +(* -- Public surface ------------------------------------------------------- *) + +(* Re-export BPS_i.Fresh (the fresh sampler) under the public-facing names. *) +module Sampler1 = BPS1.Fresh. +module Sampler2 = BPS2.Fresh. + +module Game1 (A : Adv) = { + proc main() : bool = { + var p, r; + p <$ d_param; + Sampler1.p <- p; + r <@ A(Sampler1).main(p); + return r; + } +}. + +module Game2 (A : Adv) = { + proc main() : bool = { + var p, r; + p <$ d_param; + Sampler2.p <- p; + r <@ A(Sampler2).main(p); + return r; + } +}. + +(* -- Section: A, axioms, internal Rényi chain, user-facing lemma ---------- + + MIRRORING. Everything below comes in side-1/side-2 pairs (Game1/Game2, + BPS1/BPS2, joint1/joint2, ...). EC lemmas cannot abstract over which + sampler *module* is in play (module types expose no state), so each + side-2 proof is a verbatim mirror of its side-1 twin with 1 -> 2 + renamings. Audit side 1; diff side 2 against it. *) + +section. + +declare module A <: Adv + { -Sampler1, -Sampler2, -BPS1.Count, -BPS2.Count, -BPS1.Ref, -BPS2.Ref }. + +declare axiom A_ll : + forall (O <: Oracle { -A }), + islossless O.get => islossless A(O).main. + +declare axiom A_bound1 : + hoare[ A(BPS1.Count(Sampler1)).main : + BPS1.Count.n = 0 ==> BPS1.Count.n <= N ]. + +declare axiom A_bound2 : + hoare[ A(BPS2.Count(Sampler2)).main : + BPS2.Count.n = 0 ==> BPS2.Count.n <= N ]. + +(* Distinguisher clone for the joint Rényi step. Inputs are pairs + [(p, xs) : param_t * out_t list] so [B.guess] can install both [p] + (passed as A's argument) and [xs] (consumed by [Ref]) in a single + step — no out-of-band [Sampler.p] coupling needed. *) +local clone import Distinguisher as DistJoint with + type in_t <- param_t * out_t list, + type out_t <- bool + proof *. + +(* List-consuming oracle (RDO-internal). *) +local module Ref : Iface.Oracle = { + var xs : out_t list + proc get() = { + var r; + r <- head witness xs; + xs <- behead xs; + return r; + } +}. + +local module B : DistJoint.Dist = { + proc guess(px : param_t * out_t list) : bool = { + var r; + Ref.xs <- px.`2; + r <@ A(Ref).main(px.`1); + return r; + } +}. + +(* -- Joint pre-sampled experiments --------------------------------------- + [G_Joint_i] integrates the [d_param] sample with the per-[p] dlist + into a single experiment. Each [Game_i] is provably equivalent to + the corresponding [G_Joint_i], and the two [G_Joint_i] sides differ + only in [d_i] (the [d_param] marginal cancels in the pointwise + ratio), so a single Rényi-∞ application bounds them by [M^N]. *) + +local module G_Joint1 = { + proc main() : bool = { + var p_val, xs, r; + p_val <$ d_param; + Sampler1.p <- p_val; + xs <$ dlist (dtot1 p_val) N; + BPS1.Ref.xs <- xs; + r <@ A(BPS1.Ref).main(p_val); + return r; + } +}. + +local module G_Joint2 = { + proc main() : bool = { + var p_val, xs, r; + p_val <$ d_param; + Sampler2.p <- p_val; + xs <$ dlist (dtot2 p_val) N; + BPS2.Ref.xs <- xs; + r <@ A(BPS2.Ref).main(p_val); + return r; + } +}. + +(* Transitivity 1: [Game_i] ≡ [G_Joint_i], per event. Couple the [p] + draw, then lift the per-[p] fresh≡ref equality through it (bypr + the + event-generic [BPS_i.eq_pr_fresh_ref_ev]). *) +local lemma Game1_eq_Joint1 (E : bool -> bool) &m : + Pr[Game1(A).main() @ &m : E res] = Pr[G_Joint1.main() @ &m : E res]. +proof. +byequiv => //; proc. +(* Lift each side to a single procedure call to its BPS game. *) +proc change {1} [2..3] : { r <@ BPS1.G(BPS1.Fresh, A).main(p); }; + 1: by inline; wp; sim. +proc change {2} [2..5] : { r <@ BPS1.G(BPS1.Ref, A).main(p_val); }; + 1: by inline; wp; sim. +(* Couple the [p] sampling. *) +seq 1 1 : (={glob A} /\ p{1} = p_val{2}). ++ rnd; auto. +(* Both sides are now a single procedure call with equal arguments. + Discharge via [call] + [bypr] using [eq_pr_fresh_ref_ev] per-p. *) +call (_: ={glob A, arg} ==> ={res}). ++ proc*; call (_: ={glob A, arg} ==> ={res}); auto. + bypr (res{1}) (res{2}) => /> &1 &2 ga gA. + (* Memory swap: glob A coincides at &1, &2; both procs only read glob A. *) + have ->: Pr[BPS1.G(BPS1.Fresh, A).main(arg{2}) @ &1 : res = ga] + = Pr[BPS1.G(BPS1.Fresh, A).main(arg{2}) @ &2 : res = ga]. + + byequiv (_: ={arg, glob A} ==> ={res}) => //; sim. + exact (BPS1.eq_pr_fresh_ref_ev A A_ll A_bound1 (fun r => r = ga) arg{2} &2). +by auto => />. +qed. + +local lemma Game2_eq_Joint2 (E : bool -> bool) &m : + Pr[Game2(A).main() @ &m : E res] = Pr[G_Joint2.main() @ &m : E res]. +proof. +byequiv => //; proc. +proc change {1} [2..3] : { r <@ BPS2.G(BPS2.Fresh, A).main(p); }; + 1: by inline; wp; sim. +proc change {2} [2..5] : { r <@ BPS2.G(BPS2.Ref, A).main(p_val); }; + 1: by inline; wp; sim. +seq 1 1 : (={glob A} /\ p{1} = p_val{2}). ++ rnd; auto. +call (_: ={glob A, arg} ==> ={res}). ++ proc*; call (_: ={glob A, arg} ==> ={res}); auto. + bypr (res{1}) (res{2}) => /> &1 &2 ga gA. + have ->: Pr[BPS2.G(BPS2.Fresh, A).main(arg{2}) @ &1 : res = ga] + = Pr[BPS2.G(BPS2.Fresh, A).main(arg{2}) @ &2 : res = ga]. + + byequiv (_: ={arg, glob A} ==> ={res}) => //; sim. + exact (BPS2.eq_pr_fresh_ref_ev A A_ll A_bound2 (fun r => r = ga) arg{2} &2). +by auto => />. +qed. + +(* Joint distribution of (p, xs): sample p from d_param, sample xs from + the per-p dlist, return the pair. Internal proof plumbing — [local] + so they do not survive section closure into the public API. *) +local op joint1 = dlet d_param (fun p => dmap (dlist (dtot1 p) N) (fun xs => (p, xs))). +local op joint2 = dlet d_param (fun p => dmap (dlist (dtot2 p) N) (fun xs => (p, xs))). + +(* Pointwise simplification: the joint distribution at [(a, ys)] + collapses to [mu1 d_param a * mu1 (dlist (d_i a) N) ys] because the + inner [dmap] concentrates on pairs whose first component equals the + sampled [p]. *) +local lemma joint_pt (di : param_t -> out_t distr) a ys : + mu1 (dlet d_param (fun p => dmap (dlist (di p) N) (fun xs => (p, xs)))) (a, ys) + = mu1 d_param a * mu1 (dlist (di a) N) ys. +proof. +rewrite dlet1E (@sumE_fin _ [a]) //=. +- move=> p /=. + apply contraR => /=; move=> pne_a. + rewrite dmap1E. + have -> : ((pred1 (a, ys)) \o (fun xs => (p, xs))) = pred0. + + by apply/fun_ext => xs; rewrite /pred1 /(\o) /pred0; smt(). + by rewrite mu0. +rewrite big_seq1 /= dmap1E. +congr. +apply mu_eq => xs. +by rewrite /pred1 /(\o) /=; smt(). +qed. + +(* Bridge: G_Joint_i ≡ Sample(B)(joint_i). G_Joint_i has Sampler_i.p + set externally (a "dead store" since A doesn't read Sampler_i.p); + Sample(B) doesn't. Both pass [p] as A's argument and supply [xs] + to the same list-consuming oracle (Ref ≅ BPS_i.Ref by shape). *) +local lemma G_Joint1_vs_Sample (E : bool -> bool) &m : + Pr[G_Joint1.main() @ &m : E res] = Pr[Sample(B).main(joint1) @ &m : E res]. +proof. +byequiv => //; proc; inline B.guess. +swap{1} 2 1. +(* Replace RHS one-step sampling with explicit two-step. *) +proc change {2} [1..2] : [(p_aux : param_t) (xs_aux : out_t list)] { + p_aux <$ d_param; + xs_aux <$ dlist (dtot1 p_aux) N; + px <- (p_aux, xs_aux); +}. ++ wp; rnd : *0 *0; auto. + move=> &1 _ -> /=; rewrite dmap_id /= !andaE. + by split=> [? // | [a ys] H_in /=]. +seq 2 3 : (={glob A} /\ p_val{1} = px{2}.`1 /\ xs{1} = px{2}.`2). ++ by wp; rnd; rnd; auto. +wp. +call (_: BPS1.Ref.xs{1} = Ref.xs{2}); first by proc; auto. +by auto. +qed. + +local lemma G_Joint2_vs_Sample (E : bool -> bool) &m : + Pr[G_Joint2.main() @ &m : E res] = Pr[Sample(B).main(joint2) @ &m : E res]. +proof. +byequiv => //; proc; inline B.guess. +swap{1} 2 1. +proc change {2} [1..2] : [(p_aux : param_t) (xs_aux : out_t list)] { + p_aux <$ d_param; + xs_aux <$ dlist (dtot2 p_aux) N; + px <- (p_aux, xs_aux); +}. ++ wp; rnd : *0 *0; auto. + move=> &1 _ -> /=; rewrite dmap_id /= !andaE. + by split=> [? // | [a ys] H_in /=]. +seq 2 3 : (={glob A} /\ p_val{1} = px{2}.`1 /\ xs{1} = px{2}.`2). ++ by wp; rnd; rnd; auto. +wp. +call (_: BPS2.Ref.xs{1} = Ref.xs{2}); first by proc; auto. +by auto. +qed. + +(* Pointwise [M^N] uniform bound of joint1 by joint2: for p ∉ supp d_param + the dlet integrand vanishes; for p ∈ supp d_param we use + [d1_dominated_d2] composed with dlist tensorization. *) +local lemma joint_pt_bound (a : param_t) ys : + mu1 joint1 (a, ys) <= M ^ N * mu1 joint2 (a, ys). +proof. +rewrite /joint1 /joint2 !joint_pt. +case (a \in d_param) => a_in. ++ rewrite (dtot1E a a_in) (dtot2E a a_in). + have dom_a : dominated M (d1 a) (d2 a) + by split; [exact M_ge0 | exact (d1_dominated_d2 a a_in)]. + have [_ dlist_all] := dominated_dlist M (d1 a) (d2 a) N N_ge0 dom_a. + have dlist_pt := dlist_all ys. + have ge0_mup : 0%r <= mu1 d_param a by exact ge0_mu1. + smt(ge0_mu1). ++ have -> : mu1 d_param a = 0%r by smt(supportP). + by rewrite mul0r mulr0; smt(M_ge0 expr_ge0 N_ge0). +qed. + +local lemma joint_dom : dominated (M ^ N) joint1 joint2. +proof. +split; first by smt(M_ge0 expr_ge0 N_ge0). +by case=> a ys; exact (joint_pt_bound a ys). +qed. + +local lemma joint_rdiv_inf_bound : rdiv_inf joint1 joint2 <= M ^ N. +proof. exact (rdiv_inf_le _ _ _ joint_dom). qed. + +(* Transitivity 2 (the Rényi step): single application of [adv_rdiv_inf_le] + on the joint distribution. *) +local lemma Joint_rdiv_bound (E : bool -> bool) &m : + Pr[G_Joint1.main() @ &m : E res] <= + M ^ N * + Pr[G_Joint2.main() @ &m : E res]. +proof. +rewrite (G_Joint1_vs_Sample E &m) (G_Joint2_vs_Sample E &m). +apply (adv_rdiv_inf_le B E &m (M ^ N)). +- exact joint_dom. +- exact joint_rdiv_inf_bound. +qed. + +(* -- PUBLIC: parametric user-facing lemma, per event ---------------------- *) + +lemma rdiv_bound_sampler (E : bool -> bool) &m : + Pr[Game1(A).main() @ &m : E res] <= + M ^ N * + Pr[Game2(A).main() @ &m : E res]. +proof. +rewrite (Game1_eq_Joint1 E &m) (Game2_eq_Joint2 E &m). +exact (Joint_rdiv_bound E &m). +qed. + +end section. + +end RDivOracle. + +(* ========================================================================== + + Restricted layer: the valid-parameter surface over the REAL experiment. + + Some developments only have the per-parameter hypotheses (losslessness, + dominance) on a subset of "good" parameters — e.g. MAYO's rejection- + sampling guarantee holds except for a negligible set of bad keys. In + [RDivOracle] that restriction is an instantiation: condition [d_param]. + This theory packages that instantiation for the common shape where the + consumer's games sample from the FULL distribution [d_full] (the real + key-generation) and excise bad parameters at the event level: + + [rdiv_bound_sampler] : + Pr[GameV1(A) : E res /\ valid Sampler1.p] + <= M ^ N * Pr[GameV2(A) : E res /\ valid Sampler2.p] + + — validity as an event conjunct over the game-stored parameter, with NO + additive slack and NO [M >= 1] assumption: bad parameters behave + identically in both games, and the validity conjunct removes their mass + from both sides. The corollary [rdiv_bound_sampler_le] trades the + conjunct for the additive bad-parameter mass: + + Pr[GameV1(A) : E res] + <= M ^ N * Pr[GameV2(A) : E res] + mu d_full (predC valid). + + (An [M >= 1]-free bound for arbitrary events without the additive term + is impossible: events that count bad-parameter runs weigh their equal + mass on both sides, which only [M ^ N >= 1] could absorb.) + + Internally: clone [RDivOracle] at [d_param <- dcond d_full valid] + ([Core]) and prove the conditioning hop once per side ([cond_factor1], + mirrored as [cond_factor2]), + + Pr[GameV1(A) : E res /\ valid p] + = mu d_full valid * Pr[Core.Game1(A) : E res] + + by reflecting both game families into [Distinguisher.Sample] over a + distinguisher returning [(p, r)] pairs ([GameV1_Sample], + [CoreGame1_Sample]), where the hop is plain distribution theory: + [Sample1_dcond_valid] makes the validity conjunct free on the + conditioned source, and [Sample1_cond_factor] factors out + [mu d_full valid] ([dletE] + [dcond1E]). The public + [rdiv_bound_sampler] chains [cond_factor1], [Core.rdiv_bound_sampler] + and [cond_factor2]; [rdiv_bound_sampler_le] adds [GameV1_invalid_le] + for the bad-parameter mass. + + The consumer's own bad-key payment (e.g. MAYO's [eps_key] hop from + "wins" to "wins on valid keys") stays on the consumer side, where the + key-generation procedure lives. + + ========================================================================== *) + +abstract theory RDivOracleValid. + +type out_t. +type param_t. + +(* Same sharing story as [RDivOracle.Iface] — see the note there. *) +clone import BPS_Iface as Iface with + type out_t <= out_t, + type param_t <= param_t. + +op [lossless] d_full : param_t distr. +op valid : param_t -> bool. + +op d1 : param_t -> out_t distr. +op d2 : param_t -> out_t distr. + +axiom d1_ll : forall p, p \in d_full => valid p => is_lossless (d1 p). +axiom d2_ll : forall p, p \in d_full => valid p => is_lossless (d2 p). + +op N : { int | 0 <= N } as N_ge0. +op M : { real | 0%r <= M } as M_ge0. + +axiom d1_dominated_d2 : + forall p, p \in d_full => valid p => + forall x, mu1 (d1 p) x <= M * mu1 (d2 p) x. + +(* Good parameters have positive mass (in MAYO: >= 1 - eps_key > 0). *) +axiom valid_nondegenerate : 0%r < mu d_full valid. + +clone RDivOracle as Core with + type out_t <- out_t, + type param_t <- param_t, + theory Iface <- Iface, + op d_param <- dcond d_full valid, + op d1 <- d1, + op d2 <- d2, + op N <- N, + op M <- M + proof *. +realize d_param_ll by apply dcond_ll; exact valid_nondegenerate. +realize d1_ll by move => p /dcond_supp [p_in v_p]; exact (d1_ll p p_in v_p). +realize d2_ll by move => p /dcond_supp [p_in v_p]; exact (d2_ll p p_in v_p). +realize N_ge0 by exact N_ge0. +realize M_ge0 by exact M_ge0. +realize d1_dominated_d2 + by move => p /dcond_supp [p_in v_p]; exact (d1_dominated_d2 p p_in v_p). + +(* Public sampler names (aliases of the Core samplers). *) +module Sampler1 = Core.Sampler1. +module Sampler2 = Core.Sampler2. + +(* Consumer-facing kernel identities: on valid parameters of [d_full], + the samplers draw exactly [d_i p]. Cite these instead of unfolding + the internal totalized kernels ([Core.dtot_i]). *) +lemma Sampler1_dE p : p \in d_full => valid p => Core.dtot1 p = d1 p. +proof. by move => p_in v_p; apply Core.dtot1E; rewrite dcond_supp. qed. + +lemma Sampler2_dE p : p \in d_full => valid p => Core.dtot2 p = d2 p. +proof. by move => p_in v_p; apply Core.dtot2E; rewrite dcond_supp. qed. + +(* The REAL experiments: parameter drawn from the full distribution. *) +module GameV1 (A : Adv) = { + proc main() : bool = { + var p, r; + p <$ d_full; + Sampler1.p <- p; + r <@ A(Sampler1).main(p); + return r; + } +}. + +module GameV2 (A : Adv) = { + proc main() : bool = { + var p, r; + p <$ d_full; + Sampler2.p <- p; + r <@ A(Sampler2).main(p); + return r; + } +}. + +(* -- Section: the conditioning hop and the public bounds ------------------ + MIRRORING: as in [RDivOracle], side-2 items are verbatim mirrors of + their side-1 twins (1 -> 2 in every name); audit side 1, diff side 2. *) + +section. + +declare module A <: Adv + { -Core.Sampler1, -Core.Sampler2, -Core.BPS1.Count, -Core.BPS2.Count, + -Core.BPS1.Ref, -Core.BPS2.Ref }. + +declare axiom A_ll : + forall (O <: Oracle { -A }), + islossless O.get => islossless A(O).main. + +declare axiom A_bound1 : + hoare[ A(Core.BPS1.Count(Core.Sampler1)).main : + Core.BPS1.Count.n = 0 ==> Core.BPS1.Count.n <= N ]. + +declare axiom A_bound2 : + hoare[ A(Core.BPS2.Count(Core.Sampler2)).main : + Core.BPS2.Count.n = 0 ==> Core.BPS2.Count.n <= N ]. + +(* Distinguisher clone for the conditioning hop: inputs are parameters, + outputs are [(p, r)] pairs so events can inspect the drawn parameter. *) +local clone import Distinguisher as DistP with + type in_t <- param_t, + type out_t <- param_t * bool + proof *. + +local module BP1 : DistP.Dist = { + proc guess(p : param_t) : param_t * bool = { + var r; + Core.Sampler1.p <- p; + r <@ A(Core.Sampler1).main(p); + return (p, r); + } +}. + +local module BP2 : DistP.Dist = { + proc guess(p : param_t) : param_t * bool = { + var r; + Core.Sampler2.p <- p; + r <@ A(Core.Sampler2).main(p); + return (p, r); + } +}. + +(* Shape lemmas: both game families are [Sample] in disguise. *) +local lemma GameV1_Sample (F : bool -> param_t -> bool) &m : + Pr[GameV1(A).main() @ &m : F res Core.Sampler1.p] + = Pr[Sample(BP1).main(d_full) @ &m : F res.`2 res.`1]. +proof. +byequiv (: ={glob A, glob Core.Sampler1} /\ arg{2} = d_full + ==> res{2} = (Core.Sampler1.p{1}, res{1})) => //. +proc; inline BP1.guess; wp. +call (: ={glob Core.Sampler1}); first by proc; auto. +by auto. +qed. + +local lemma GameV2_Sample (F : bool -> param_t -> bool) &m : + Pr[GameV2(A).main() @ &m : F res Core.Sampler2.p] + = Pr[Sample(BP2).main(d_full) @ &m : F res.`2 res.`1]. +proof. +byequiv (: ={glob A, glob Core.Sampler2} /\ arg{2} = d_full + ==> res{2} = (Core.Sampler2.p{1}, res{1})) => //. +proc; inline BP2.guess; wp. +call (: ={glob Core.Sampler2}); first by proc; auto. +by auto. +qed. + +local lemma CoreGame1_Sample (E : bool -> bool) &m : + Pr[Core.Game1(A).main() @ &m : E res] + = Pr[Sample(BP1).main(dcond d_full valid) @ &m : E res.`2]. +proof. +byequiv (: ={glob A, glob Core.Sampler1} /\ arg{2} = dcond d_full valid + ==> res{1} = res{2}.`2) => //. +proc; inline BP1.guess; wp. +call (: ={glob Core.Sampler1}); first by proc; auto. +by auto. +qed. + +local lemma CoreGame2_Sample (E : bool -> bool) &m : + Pr[Core.Game2(A).main() @ &m : E res] + = Pr[Sample(BP2).main(dcond d_full valid) @ &m : E res.`2]. +proof. +byequiv (: ={glob A, glob Core.Sampler2} /\ arg{2} = dcond d_full valid + ==> res{1} = res{2}.`2) => //. +proc; inline BP2.guess; wp. +call (: ={glob Core.Sampler2}); first by proc; auto. +by auto. +qed. + +(* Concentration: [BP_i.guess(x)] always returns a pair with first + component [x]. *) +local lemma BP1_fst &m (x0 : param_t) (z : param_t * bool) : + z.`1 <> x0 => Pr[BP1.guess(x0) @ &m : res = z] = 0%r. +proof. +move => neq; byphoare (: arg = x0 ==> res = z) => //. +hoare; proc; wp; call (: true); auto => /> /#. +qed. + +local lemma BP2_fst &m (x0 : param_t) (z : param_t * bool) : + z.`1 <> x0 => Pr[BP2.guess(x0) @ &m : res = z] = 0%r. +proof. +move => neq; byphoare (: arg = x0 ==> res = z) => //. +hoare; proc; wp; call (: true); auto => /> /#. +qed. + +(* Support form of concentration, phrased on the [mk] kernels that + [Sample_dletE] introduces. *) +local lemma BP1_supp_fst &m (x : param_t) (z : param_t * bool) : + z \in mk (fun z0 => Pr[BP1.guess(x) @ &m : res = z0]) => z.`1 = x. +proof. +case (z.`1 = x) => // neq z_in. +move: z_in; rewrite supportP -(GD.adv_mu1 BP1 &m z x). +by rewrite (BP1_fst &m x z neq). +qed. + +local lemma BP2_supp_fst &m (x : param_t) (z : param_t * bool) : + z \in mk (fun z0 => Pr[BP2.guess(x) @ &m : res = z0]) => z.`1 = x. +proof. +case (z.`1 = x) => // neq z_in. +move: z_in; rewrite supportP -(GD.adv_mu1 BP2 &m z x). +by rewrite (BP2_fst &m x z neq). +qed. + +(* On the conditioned source, every reachable pair carries a valid + parameter — the validity conjunct is free. *) +local lemma Sample1_dcond_valid (E : bool -> bool) &m : + Pr[Sample(BP1).main(dcond d_full valid) @ &m : E res.`2] + = Pr[Sample(BP1).main(dcond d_full valid) @ &m : E res.`2 /\ valid res.`1]. +proof. +rewrite (Sample_dletE BP1 (fun (z : param_t * bool) => E z.`2) &m). +rewrite (Sample_dletE BP1 (fun (z : param_t * bool) => E z.`2 /\ valid z.`1) &m). +apply mu_eq_support => z /supp_dlet [x [x_in z_in]] /=. +have z1 : z.`1 = x by exact (BP1_supp_fst &m x z z_in). +by move: x_in => /dcond_supp [_ v_x]; rewrite z1 v_x. +qed. + +local lemma Sample2_dcond_valid (E : bool -> bool) &m : + Pr[Sample(BP2).main(dcond d_full valid) @ &m : E res.`2] + = Pr[Sample(BP2).main(dcond d_full valid) @ &m : E res.`2 /\ valid res.`1]. +proof. +rewrite (Sample_dletE BP2 (fun (z : param_t * bool) => E z.`2) &m). +rewrite (Sample_dletE BP2 (fun (z : param_t * bool) => E z.`2 /\ valid z.`1) &m). +apply mu_eq_support => z /supp_dlet [x [x_in z_in]] /=. +have z1 : z.`1 = x by exact (BP2_supp_fst &m x z z_in). +by move: x_in => /dcond_supp [_ v_x]; rewrite z1 v_x. +qed. + +(* The conditioning hop at the distribution level: for validity-entailing + events, sampling from [d_full] equals [mu d_full valid] times sampling + from the conditioned distribution. *) +local lemma Sample1_cond_factor (G : param_t * bool -> bool) &m : + (forall z, G z => valid z.`1) => + Pr[Sample(BP1).main(d_full) @ &m : G res] + = mu d_full valid * Pr[Sample(BP1).main(dcond d_full valid) @ &m : G res]. +proof. +move => G_valid. +rewrite (Sample_dletE BP1 G &m d_full). +rewrite (Sample_dletE BP1 G &m (dcond d_full valid)). +have T0 : forall x, !valid x => + mu (mk (fun z0 => Pr[BP1.guess(x) @ &m : res = z0])) G = 0%r. ++ move => x nv. + rewrite (mu_eq_support _ G pred0) 2:mu0 // => z /(BP1_supp_fst &m x) z1. + by rewrite /pred0 /=; smt(). +rewrite !dletE -sumZ. +apply eq_sum => x /=. +rewrite dcond1E. +case (valid x) => v_x; last first. ++ by rewrite (T0 x v_x) !mulr0. +have nz : mu d_full valid <> 0%r by smt(valid_nondegenerate). +by field. +qed. + +local lemma Sample2_cond_factor (G : param_t * bool -> bool) &m : + (forall z, G z => valid z.`1) => + Pr[Sample(BP2).main(d_full) @ &m : G res] + = mu d_full valid * Pr[Sample(BP2).main(dcond d_full valid) @ &m : G res]. +proof. +move => G_valid. +rewrite (Sample_dletE BP2 G &m d_full). +rewrite (Sample_dletE BP2 G &m (dcond d_full valid)). +have T0 : forall x, !valid x => + mu (mk (fun z0 => Pr[BP2.guess(x) @ &m : res = z0])) G = 0%r. ++ move => x nv. + rewrite (mu_eq_support _ G pred0) 2:mu0 // => z /(BP2_supp_fst &m x) z1. + by rewrite /pred0 /=; smt(). +rewrite !dletE -sumZ. +apply eq_sum => x /=. +rewrite dcond1E. +case (valid x) => v_x; last first. ++ by rewrite (T0 x v_x) !mulr0. +have nz : mu d_full valid <> 0%r by smt(valid_nondegenerate). +by field. +qed. + +(* The conditioning hop, per side. *) +local lemma cond_factor1 (E : bool -> bool) &m : + Pr[GameV1(A).main() @ &m : E res /\ valid Core.Sampler1.p] + = mu d_full valid * Pr[Core.Game1(A).main() @ &m : E res]. +proof. +rewrite (GameV1_Sample (fun r p => E r /\ valid p) &m) /=. +rewrite (CoreGame1_Sample E &m) (Sample1_dcond_valid E &m). +apply (Sample1_cond_factor (fun (z : param_t * bool) => E z.`2 /\ valid z.`1) &m). +by move => z []. +qed. + +local lemma cond_factor2 (E : bool -> bool) &m : + Pr[GameV2(A).main() @ &m : E res /\ valid Core.Sampler2.p] + = mu d_full valid * Pr[Core.Game2(A).main() @ &m : E res]. +proof. +rewrite (GameV2_Sample (fun r p => E r /\ valid p) &m) /=. +rewrite (CoreGame2_Sample E &m) (Sample2_dcond_valid E &m). +apply (Sample2_cond_factor (fun (z : param_t * bool) => E z.`2 /\ valid z.`1) &m). +by move => z []. +qed. + +(* -- PUBLIC: the restricted bound, per validity-entailing event ----------- *) + +lemma rdiv_bound_sampler (E : bool -> bool) &m : + Pr[GameV1(A).main() @ &m : E res /\ valid Core.Sampler1.p] <= + M ^ N * + Pr[GameV2(A).main() @ &m : E res /\ valid Core.Sampler2.p]. +proof. +rewrite (cond_factor1 E &m) (cond_factor2 E &m) mulrCA. +apply ler_wpmul2l; first by smt(valid_nondegenerate). +exact (Core.rdiv_bound_sampler A A_ll A_bound1 A_bound2 E &m). +qed. + +(* Bad-parameter mass at the game level. *) +local lemma GameV1_invalid_le &m : + Pr[GameV1(A).main() @ &m : !valid Core.Sampler1.p] + <= mu d_full (predC valid). +proof. +rewrite (GameV1_Sample (fun _ p => !valid p) &m) /=. +rewrite (Sample_dletE BP1 (fun (z : param_t * bool) => !valid z.`1) &m). +rewrite dletE muE. +apply ler_sum. ++ move => x /=. + case (valid x) => v_x. + - have -> : mu (mk (fun z0 => Pr[BP1.guess(x) @ &m : res = z0])) + (fun (z : param_t * bool) => !valid z.`1) = 0%r. + * rewrite (mu_eq_support _ _ pred0) 2:mu0 //. + by move => z /(BP1_supp_fst &m x) z1; rewrite /pred0 /= z1 v_x. + by rewrite mulr0 /=. + - rewrite /=. + apply (ler_trans (mu1 d_full x * 1%r)); 2: by rewrite mulr1. + by apply ler_wpmul2l; [exact ge0_mu1 | exact le1_mu]. ++ by apply summable_mu1_wght => x; smt(ge0_mu le1_mu). ++ apply (summable_le (mu1 d_full)); first exact summable_mu1. + by move => x /=; smt(ge0_mu1). +qed. + +(* Corollary: trade the validity conjunct for the additive bad-parameter + mass. No [M >= 1] needed: the conjunct form absorbs on the good side + and the bad side is bounded outright. *) +lemma rdiv_bound_sampler_le (E : bool -> bool) &m : + Pr[GameV1(A).main() @ &m : E res] <= + M ^ N * Pr[GameV2(A).main() @ &m : E res] + + mu d_full (predC valid). +proof. +rewrite Pr[mu_split (valid Core.Sampler1.p)]. +apply (ler_trans (M ^ N * Pr[GameV2(A).main() @ &m : E res /\ valid Core.Sampler2.p] + + mu d_full (predC valid))). ++ apply ler_add; first exact (rdiv_bound_sampler E &m). + apply (ler_trans (Pr[GameV1(A).main() @ &m : !valid Core.Sampler1.p])); + first by rewrite Pr[mu_sub] // /#. + exact (GameV1_invalid_le &m). +rewrite ler_add2r. +apply ler_wpmul2l; first by smt(M_ge0 expr_ge0 N_ge0). +by rewrite Pr[mu_sub]. +qed. + +end section. + +end RDivOracleValid.