From 5a014e798699581f40209376afc89341a674ed16 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 The Rényi-∞ (max-divergence / dominance) machinery for bounded-query reductions: - RDiv.ec: Rényi-∞ / max-divergence (rdiv_inf, dominated) with probability preservation (dominated_pr / rdiv_inf_pr), structural composition (dmap/dlet/dprod/dlist/dexcepted/dcond/djoin/dfold/dfun), and a distinguisher layer (Sample, adv_rdiv_inf, adv_rdiv_inf_dlist). - BoundedPreSample.ec: fresh-sampling = presampling-a-list equivalence (eq_pr_fresh_ref) for bounded-query adversaries; admit-free. - RDivOracle.ec: parametric bounded-query advantage bound rdiv_bound_sampler (Pr[Game1] <= M^N * Pr[Game2]) via BoundedPreSample + dlist tensorization. --- theories/distributions/BoundedPreSample.ec | 500 ++++++++++++ theories/distributions/RDiv.ec | 898 +++++++++++++++++++++ theories/distributions/RDivOracle.ec | 441 ++++++++++ 3 files changed, 1839 insertions(+) create mode 100644 theories/distributions/BoundedPreSample.ec create mode 100644 theories/distributions/RDiv.ec create mode 100644 theories/distributions/RDivOracle.ec diff --git a/theories/distributions/BoundedPreSample.ec b/theories/distributions/BoundedPreSample.ec new file mode 100644 index 000000000..3fdf17da9 --- /dev/null +++ b/theories/distributions/BoundedPreSample.ec @@ -0,0 +1,500 @@ +(* ========================================================================== + + BoundedPreSample: presampling library for bounded-query sequential + adversaries, parametric over a secret parameter [p : param_t]. + + Exports a single probability equivalence between: + - G_Bounded: A run against a bounded fresh-sampler (BCount-guarded), + - G_PreSampled: A run against a pre-sampled list of N draws. + + Both games share the BCount structural guard [if Count.n < N], so the + oracle-call-count bound matches list exhaustion — no upto-bad, no + asymmetric-tick issues. Consumers that want to relate a bare fresh + sampler to G_Bounded thread their own A_bound axiom at the outer + site (e.g., via Pr[bad]=0 under A_bound and a standard Pr-slice + argument). This library is agnostic to that bridge. + + 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/d_param/N, compose the + public [pr_bounded_eq_presampled] 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 import FinType. + +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 [lossless] d_param : param_t distr. + +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; + } +}. + +(* Bounded-Count wrapper: tick-and-call under a structural guard at N. + Past N calls, returns [witness] — mirrors list exhaustion in Ref. *) +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; + } +}. + +(* -- Public modules ------------------------------------------------------- *) + +(* Fresh sampler (parameter-aware). The parameter [p] is set by the + enclosing game (e.g., G_Bounded.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 ------------------------------------------------ *) + +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 ]. + +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 lemma A_bound_BCount : + hoare[ A(BCount(Fresh)).main : Count.n = 0 ==> Count.n <= N ]. +proof. +proc (Count.n <= N). ++ smt(N_ge0). ++ smt(). ++ proc; sp; if; auto. + by inline *; auto=> |> /#. +qed. + +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_eq_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_bounded_eq_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_eq_BCountB (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_bad_freshC_eq_BCountB (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_bad (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_resbad (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] <= 0%r. ++ smt(ge0_mu). +rewrite -(pr_freshC_bad p_val &m). +by byequiv (: _ ==> ={BadFlag.bad})=> //; sim. +qed. + +local lemma pr_BCountB_bad (p_val : param_t) &m : + Pr[G(BCountB, A).main(p_val) @ &m : BadFlag.bad] = 0%r. +proof. +by rewrite -(pr_bad_freshC_eq_BCountB p_val &m) (pr_freshC_bad p_val &m). +qed. + +local lemma pr_BCountB_resbad (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_bad p_val &m) #smt:(ge0_mu). +by byequiv=> //; conseq (: _ ==> ={BadFlag.bad})=> //; sim. +qed. + +local lemma pr_fresh_eq_bounded (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_eq_freshC p_val &m). +rewrite (pr_bounded_eq_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_resbad p_val &m) (pr_freshC_resbad p_val &m). +exact: pr_freshC_eq_BCountB. +qed. + +local module Wobble (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 eq_freshB_wobbleL p_val &m: + Pr[G(BCount(Fresh), A).main(p_val) @ &m: res] + = Pr[G(Wobble(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 R (RO : RO) = { + proc distinguish = G(Wobble(RO), A).main +}. + +local lemma eq_wobbleL_wobbleE p_val &m: + Pr[G(Wobble(LRO), A).main(p_val) @ &m: res] + = Pr[G(Wobble(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 R _)=> |>. +by move=> [] |> +; exact: d_ll. +qed. + +local lemma eq_refB_wobbleE p_val &m: + Pr[G(BCount(Ref), A).main(p_val) @ &m: res] + = Pr[G(Wobble(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_eq_bounded _ &m). +rewrite (eq_freshB_wobbleL _ &m). +rewrite (eq_wobbleL_wobbleE _ &m). +rewrite -(eq_refB_wobbleE _ &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. + +(* +Remaining to do: +- Generalize stdlib's DList procedure-based sampling to work with + parameterized distributions; (breaking change pending release) +- Fix proc change bug; +- Generalize the overall result here to avoid having to bound up + front. (Equivalence between lazy sampling, and eagerly-sampled + prefix + lazy.) +*) + +end section. + +end BoundedPreSample. diff --git a/theories/distributions/RDiv.ec b/theories/distributions/RDiv.ec new file mode 100644 index 000000000..7934851f5 --- /dev/null +++ b/theories/distributions/RDiv.ec @@ -0,0 +1,898 @@ +require import AllCore List Distr DProd DList Dexcepted StdBigop StdOrder RealFLub. +require import FinType. +(*---*) 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. + + The definition is only meaningful when the ratio is bounded — otherwise + the supremum escapes to +∞, which we cannot represent. We package the + finite-bound requirement in the predicate [dominated M d1 d2], which + asserts [M >= 0] and [mu1 d1 x <= M * mu1 d2 x] pointwise. Under + [dominated M d1 d2] every lemma below goes through; without it the + [flub]-definition is unspecified and the lemmas are unprovable. + + 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' (bilinear), dfold. + [RDivFun] — abstract theory: [dominated_dfun], [rdiv_inf_dfun] + (clone with [theory FT <- YourFinType]). + [Distinguisher] — abstract theory: [Sample] game, [adv_rdiv_inf], + fused variants (dmap, dlet, dexcepted, dcond). + [DistinguisherList] — abstract theory: [adv_rdiv_inf_dlist]. + + Companion files: + [SmoothRDiv.ec] — smooth max-divergence (Rényi + sdist hop). + [RDivOracle.ec] — oracle-access bound via PROM ([rdiv_inf_oracleRO]). + + ========================================================================== *) + +(* -- 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. Fix (9). *) +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. + ========================================================================== *) + +(* -- 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. +move => dom. +apply rdiv_inf_le_ub; first exact (rdiv_inf_ge0 M _ _ dom). +move => b; rewrite !dmap1E. +exact (rdiv_inf_pr M _ _ _ dom). +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. +move => dom. +apply rdiv_inf_le_ub; first exact (rdiv_inf_ge0 M _ _ dom). +by move => y; exact (dlet_pointwise _ _ _ _ y (rdiv_inf_dominated M _ _ dom)). +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_ub. +- by apply mulr_ge0; [exact (rdiv_inf_ge0 Ml _ _ doml) | + exact (rdiv_inf_ge0 Mr _ _ domr)]. +move => p. +exact (dprod_pointwise _ _ _ _ _ _ p + (rdiv_inf_dominated Ml _ _ doml) (rdiv_inf_dominated Mr _ _ domr)). +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. +have ge0_rdiv : 0%r <= rdiv_inf d1 d2 by exact (rdiv_inf_ge0 M _ _ dom). +elim: n ge0_n => [|n ge0_n IHn]. +- rewrite !dlist0 // RField.expr0 rdiv_inf_dd //. + by rewrite dunit_ll. +rewrite !dlistS // RField.exprS //. +have dom_dlist := dominated_dlist M _ _ n ge0_n dom. +apply (ler_trans (rdiv_inf (d1 `*` dlist d1 n) (d2 `*` dlist d2 n))). +- by apply (rdiv_inf_dmap (M * RField.exp M n)); + exact (dominated_dprod M (RField.exp M n) _ _ _ _ dom dom_dlist). +apply (ler_trans (rdiv_inf d1 d2 * rdiv_inf (dlist d1 n) (dlist d2 n))). +- exact (rdiv_inf_dprod M (RField.exp M n) _ _ _ _ dom dom_dlist). +by apply ler_wpmul2l. +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 smt(). +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. +move => lt_P. +have pos_wP : 0%r < weight d - mu d P by smt(). +apply rdiv_inf_le_ub; first by smt(invr_gt0). +move => x; rewrite dexcepted1E. +case (P x) => _; smt(ge0_mu1 mulr_ge0 invr_gt0). +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. +apply rdiv_inf_le_ub => // x; rewrite drestrict1E mul1r. +by case (P x) => _; smt(ge0_mu1). +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. +move => pos_P. +apply rdiv_inf_le_ub; first by smt(invr_gt0). +move => x; rewrite dcond1E. +case (P x) => _; smt(ge0_mu1 mulr_ge0 invr_gt0). +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. *) +lemma dominated_djoinmap ['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. +elim: xs => [_|x xs IHxs dom_cons] /=. +- by rewrite /djoinmap /= RField.expr0; exact dominated_refl. +have dom_head := dom_cons x _; first by rewrite mem_head. +have dom_tail : dominated (RField.exp M (size xs)) (djoinmap F1 xs) (djoinmap F2 xs). +- by apply IHxs => y y_in; apply dom_cons; rewrite in_cons y_in. +rewrite /djoinmap /= !djoin_cons addzC RField.exprS ?size_ge0 //. +apply dominated_dmap. +exact (dominated_dprod M (RField.exp M (size xs)) _ _ _ _ dom_head dom_tail). +qed. + +lemma rdiv_inf_djoinmap ['a 'b] (M : real) (F1 F2 : 'a -> 'b distr) (xs : 'a list) : + (forall x, x \in xs => dominated M (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. +elim: xs => [_|x xs IHxs dom_cons]. +- rewrite /djoinmap /= djoin_nil BRM.big_nil. + by apply rdiv_inf_le_ub => // y; rewrite mul1r. +have dom_head := dom_cons x _; first by rewrite mem_head. +have dom_tail_all : forall y, y \in xs => dominated M (F1 y) (F2 y). +- by move => y y_in; apply dom_cons; rewrite in_cons y_in. +have dom_tail : dominated (RField.exp M (size xs)) (djoinmap F1 xs) (djoinmap F2 xs) + by apply dominated_djoinmap. +have ge0_head : 0%r <= rdiv_inf (F1 x) (F2 x) by exact (rdiv_inf_ge0 M _ _ dom_head). +have ge0_tail_rdiv : 0%r <= rdiv_inf (djoinmap F1 xs) (djoinmap F2 xs) + by exact (rdiv_inf_ge0 (RField.exp M (size xs)) _ _ dom_tail). +rewrite /djoinmap /= !djoin_cons BRM.big_cons /predT /=. +apply (ler_trans + (rdiv_inf (F1 x `*` djoinmap F1 xs) (F2 x `*` djoinmap F2 xs))). +- by apply (rdiv_inf_dmap (M * RField.exp M (size xs))); + exact (dominated_dprod M (RField.exp M (size xs)) _ _ _ _ dom_head dom_tail). +apply (ler_trans + (rdiv_inf (F1 x) (F2 x) * rdiv_inf (djoinmap F1 xs) (djoinmap F2 xs))). +- exact (rdiv_inf_dprod M (RField.exp M (size xs)) _ _ _ _ dom_head dom_tail). +by apply ler_wpmul2l => //; apply IHxs. +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. +elim: ds1 ds2 => [|d1 ds1 IH] [|d2 ds2] /=. +- rewrite /dominated RField.expr0 djoin_nil; smt(ge0_mu1). +- smt(size_ge0). +- smt(size_ge0). +move => eq_sz dom_pt. +have eq_sz' : size ds1 = size ds2 by smt(). +have dom_head : dominated M d1 d2. +- have h := dom_pt 0 _; first smt(size_ge0). + by move: h => /=. +have dom_tail : dominated (RField.exp M (size ds1)) (djoin ds1) (djoin ds2). +- by apply IH => // i i_bound; have := dom_pt (i + 1) _; smt(). +rewrite !djoin_cons addzC RField.exprS ?size_ge0 //. +apply dominated_dmap. +exact (dominated_dprod M (RField.exp M (size ds1)) _ _ _ _ dom_head dom_tail). +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. +elim: ds1 ds2 => [|d1 ds1 IH] [|d2 ds2] /=. +- rewrite djoin_nil range_geq // BRM.big_nil. + rewrite rdiv_inf_dd //; smt(dunit_ll). +- smt(size_ge0). +- smt(size_ge0). +move => eq_sz dom_pt. +have eq_sz' : size ds1 = size ds2 by smt(). +have dom_head : dominated M d1 d2. +- have h := dom_pt 0 _; first smt(size_ge0). + by move: h => /=. +have dom_tail_all : forall i, 0 <= i < size ds1 => + dominated M (nth witness ds1 i) (nth witness ds2 i). +- move => i i_bound; have := dom_pt (i + 1) _; first smt(). + smt(). +have dom_tail : dominated (RField.exp M (size ds1)) (djoin ds1) (djoin ds2) + by apply (dominated_djoin M) => //. +have ge0_head : 0%r <= rdiv_inf d1 d2 by exact (rdiv_inf_ge0 M _ _ dom_head). +rewrite !djoin_cons range_ltn; first smt(size_ge0). +rewrite BRM.big_cons /predT /=. +apply (ler_trans (rdiv_inf (d1 `*` djoin ds1) (d2 `*` djoin ds2))). +- by apply (rdiv_inf_dmap (M * RField.exp M (size ds1))); + exact (dominated_dprod M (RField.exp M (size ds1)) _ _ _ _ dom_head dom_tail). +apply (ler_trans (rdiv_inf d1 d2 * rdiv_inf (djoin ds1) (djoin ds2))). +- exact (rdiv_inf_dprod M (RField.exp M (size ds1)) _ _ _ _ dom_head dom_tail). +apply ler_wpmul2l => //. +apply (ler_trans + (BRM.big predT (fun i => rdiv_inf (nth witness ds1 i) (nth witness ds2 i)) + (range 0 (size ds1)))). +- by apply IH. +rewrite (addzC 1 (size ds1)) range_addr BRM.big_map /(\o) /=. +apply lerr_eq; apply BRM.eq_big_seq => i hi /=. +by congr; smt(nth_behead behead_cons mem_range). +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 [d1] and [d2] have equal weights, [dopt] + preserves dominance with the same bound. *) + +lemma dominated_dopt (M : real) (d1 d2 : 'a distr) : + weight d1 = weight d2 => + dominated M d1 d2 => + dominated (maxr 1%r M) (dopt d1) (dopt d2). +proof. +move => eq_w dom. +case: dom => [ge0_M le_mu1]; split; first smt(). +case => [|y]; rewrite !dopt1E /=. +- by rewrite eq_w; 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 d1 = weight d2 => + dominated M d1 d2 => + rdiv_inf (dopt d1) (dopt d2) <= maxr 1%r (rdiv_inf d1 d2). +proof. +move => eq_w dom. +have ge0_rdiv : 0%r <= rdiv_inf d1 d2 by exact (rdiv_inf_ge0 M _ _ dom). +apply rdiv_inf_le_ub; first smt(). +case => [|y]; rewrite !dopt1E /=. +- by rewrite eq_w; smt(mu_bounded). +apply (ler_trans (rdiv_inf d1 d2 * mu1 d2 y)); first exact (rdiv_inf_upper_bound M _ _ y dom). +apply ler_wpmul2r; smt(ge0_mu1). +qed. + +(* -- Bilinear 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] works for every [x]). *) + +lemma dominated_dlet' ['a 'b] (Md Mf : real) (d1 d2 : 'a distr) (F1 F2 : 'a -> 'b distr) : + dominated Md d1 d2 => + (forall x, dominated Mf (F1 x) (F2 x)) => + dominated (Md * Mf) (dlet d1 F1) (dlet d2 F2). +proof. +case => [ge0_Md dom_d] dom_F. +have [ge0_Mf _] := dom_F witness. +split; first by apply mulr_ge0. +move => y; rewrite !dlet1E -sumZ. +apply ler_sum => [x /= | |]. +- have h1 := dom_d x. + have [_ h2] := dom_F x; 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). + smt(). +- 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 uniform domination. The per-step + bound [Ms i] uniformly dominates the i-th step's kernel across all + accumulator values. 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 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' (BRM.big predT Ms (range 0 n)) (Ms n) _ _ _ _ IH). +by move => y; split => //; exact (step_n y). +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 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. Your [FinType] clone must use [<=] for type/op + substitutions — see [RDivOracle.ec] header for details. *) + +abstract theory RDivFun. + clone FinType as FT. + + clone import MUniFinFun with + type t <- FT.t, + theory FinT <- FT + proof *. + + lemma dominated_dfun ['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. + rewrite !dfun_dmap. + apply dominated_dmap. + apply (dominated_djoinmap M) => x _; exact (dom_pt x). + 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. + rewrite !dfun_dmap. + apply (ler_trans (rdiv_inf (djoinmap F1 FT.enum) (djoinmap F2 FT.enum))). + - apply (rdiv_inf_dmap (RField.exp M (size FT.enum))). + apply (dominated_djoinmap M) => x _; exact (dom_pt x). + apply (rdiv_inf_djoinmap M) => x _; exact (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 (see .claude/pull-requests/rdiv.md): + - Generic output type [out_t] — no bool specialization (SDist fix 3). + - Distributions as [main] arguments, not fixed ops (SDist fix 2). + - [adv_rdiv_inf] takes the pRHL judgment directly, no reshape (fix 8). + ========================================================================== *) + +abstract theory Distinguisher. +type in_t, out_t. + +module type Dist = { + proc guess(x : in_t) : out_t +}. + +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; + } +}. + +(* Elementary sampler, used to encode [A.guess]'s per-input output + distribution as a first-class distr. *) +module S = { + proc sample (d : out_t distr) = { + var r; + + r <$ d; + return r; + } +}. + +lemma sampleE (d' : out_t distr) &m a : + Pr[S.sample(d') @ &m : res = a] = mu1 d' a. +proof. by byphoare (: d = d' ==> _) => //; proc; rnd; auto. qed. + +(* The per-input adversary output distribution is well-formed. *) +lemma uniq_big_res (A <: Dist) &m x' (zs : out_t list) : + uniq zs => + big predT (fun z => Pr[A.guess(x') @ &m : res = z]) zs = + Pr[A.guess(x') @ &m : res \in zs]. +proof. +elim: zs => [_|z zs IHzs /= [zNzs uq_zs]]. +- by rewrite big_nil; byphoare => //; hoare; auto. +by rewrite big_cons {1}/predT /= IHzs // Pr[mu_disjoint] /#. +qed. + +lemma adv_isdistr (A <: Dist) &m x' : + isdistr (fun z => Pr[A.guess(x') @ &m : res = z]). +proof. +split => [z /=|zs uq_zs]; first by byphoare. +by rewrite (uniq_big_res A &m) //; byphoare. +qed. + +lemma adv_mu1 (A <: Dist) &m x' z : + Pr[A.guess(x') @ &m : res = z] = + mu1 (mk (fun z' => Pr[A.guess(x') @ &m : res = z'])) z. +proof. by rewrite muK //; exact (adv_isdistr A &m x'). qed. + +(* 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. + +(* -- Pre-composed adversary bounds ---------------------------------------- + + Fuse [adv_rdiv_inf] with the structural lemmas so users cite a single + composed result instead of chaining three applications. Each saves one + ler_trans hop and one explicit module argument per call site. *) + +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 (ler_trans + (rdiv_inf (dmap d1 G) (dmap d2 G) * Pr[Sample(A).main(dmap d2 G) @ &m : P res])). +- by apply (adv_rdiv_inf A _ _ M); apply (dominated_dmap M). +apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +exact (rdiv_inf_dmap M _ _ G dom). +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 (ler_trans + (rdiv_inf (dlet d1 G) (dlet d2 G) * Pr[Sample(A).main(dlet d2 G) @ &m : P res])). +- by apply (adv_rdiv_inf A _ _ M); apply (dominated_dlet M). +apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +exact (rdiv_inf_dlet M _ _ G dom). +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 (ler_trans + (rdiv_inf (d \ Q) d * Pr[Sample(A).main(d) @ &m : P res])). +- by apply (adv_rdiv_inf A _ _ (1%r / (weight d - mu d Q))); + apply dominated_dexcepted. +apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +exact (rdiv_inf_dexcepted _ _ lt_Q). +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 (ler_trans + (rdiv_inf (dcond d Q) d * Pr[Sample(A).main(d) @ &m : P res])). +- by apply (adv_rdiv_inf A _ _ (1%r / mu d Q)); apply dominated_dcond. +apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +exact (rdiv_inf_dcond _ _ pos_Q). +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 (ler_trans + (rdiv_inf (dlist d1 n) (dlist d2 n) + * Pr[DL.Sample(A).main(dlist d2 n) @ &m : P res])). +- by apply (DL.adv_rdiv_inf A _ _ (RField.exp M n)); + apply (dominated_dlist M). +apply ler_wpmul2r; first by rewrite Pr [mu_ge0]. +exact (rdiv_inf_dlist M _ _ _ ge0_n dom). +qed. + +end DistinguisherList. diff --git a/theories/distributions/RDivOracle.ec b/theories/distributions/RDivOracle.ec new file mode 100644 index 000000000..240f24ecf --- /dev/null +++ b/theories/distributions/RDivOracle.ec @@ -0,0 +1,441 @@ +(* ========================================================================== + + Rényi-∞ oracle bound for bounded-query sequential adversaries, + PARAMETRIC over a shared secret parameter [p : param_t]. + + User-facing lemma [rdiv_bound_sampler] concludes, for an A with bounded + query count N against fresh i.i.d. samplers: + + Pr[Game1(A).main @ &m : res] <= M ^ N * Pr[Game2(A).main @ &m : res] + + where: + - [Game_i] samples [p <$ d_param], sets [Sampler_i.p := p], then runs A. + - [Sampler1.get] returns a fresh draw from [d1 p]. + - [Sampler2.get] returns a fresh draw from [d2 p]. + - [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. + + 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 [pr_fresh_eq_presampled] + 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 per-p chain is just two hops: + + BPS_i.G_Fresh(A).main(p) + ≡ (via BPS_i.pr_fresh_eq_presampled, requires A_bound_i) + BPS_i.G_PreSampled(A).main(p) + ≡ (trivial byequiv, shape rename) + DL.Sample(B).main(dlist (d_i p) N) + + Then [adv_rdiv_inf_dlist] gives M^N · Sample(B) on d2. + + ========================================================================== *) + +require import AllCore List Distr DList StdOrder StdRing StdBigop FMap RealSeries. +require import RDiv. +require import FinType. +require import BoundedPreSample. +(*---*) import RField RealOrder Bigreal.BRA. + +abstract theory RDivOracle. + +(* -- Parameters ----------------------------------------------------------- *) + +type out_t. +type param_t. + +clone FinType as ParamFin with type t <- param_t. + +(* 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, + 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. + +axiom d1_ll : forall p, is_lossless (d1 p). +axiom d2_ll : forall p, is_lossless (d2 p). + +op N : { int | 0 <= N } as N_ge0. +op M : { real | 0%r <= M } as M_ge0. + +axiom dominated_12_uniform : + forall p, p \in d_param => + forall x, mu1 (d1 p) x <= M * mu1 (d2 p) x. + +(* -- BoundedPreSample clones ---------------------------------------------- *) + +clone BoundedPreSample as BPS1 with + type out_t = out_t, + type param_t = param_t, + theory Iface <- Iface, + op d <- d1, + op d_param <- d_param, + op N <- N + proof *. +realize d_ll by exact d1_ll. +realize N_ge0 by exact N_ge0. +realize d_param_ll by exact d_param_ll. + +clone BoundedPreSample as BPS2 with + type out_t = out_t, + type param_t = param_t, + theory Iface <- Iface, + op d <- d2, + op d_param <- d_param, + op N <- N + proof *. +realize d_ll by exact d2_ll. +realize N_ge0 by exact N_ge0. +realize d_param_ll by exact d_param_ll. + +(* -- 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 ---------- *) + +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 (d1 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 (d2 p_val) N; + BPS2.Ref.xs <- xs; + r <@ A(BPS2.Ref).main(p_val); + return r; + } +}. + +(* Fresh ≡ Ref at the Pr level on any [res] event. BPS exposes + [eq_pr_fresh_ref] for the event [res]; this lifts it to [res = E] using + losslessness of both games — the one delicate step, isolated here so the + transitivity bridges below read cleanly. *) +local lemma pr1_fresh_ref_ev (p : param_t) (E : bool) &n : + Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : res = E] + = Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : res = E]. +proof. +have BPSeq := BPS1.eq_pr_fresh_ref A A_ll A_bound1 p &n. +have F_ll : Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : true] = 1%r. ++ byphoare => //; proc; call (A_ll BPS1.Fresh _); 1: by proc; auto; smt(d1_ll). + by inline*; auto. +have P_ll : Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : true] = 1%r. ++ byphoare => //; proc; call (A_ll BPS1.Ref _); 1: by proc; auto. + by inline*; auto; smt(dlist_ll d1_ll N_ge0). +case E => _. ++ have ->: Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : res = true] + = Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : res] by rewrite Pr[mu_eq] // /#. + have ->: Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : res = true] + = Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : res] by rewrite Pr[mu_eq] // /#. + exact BPSeq. +have ->: Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : res = false] + = Pr[BPS1.G(BPS1.Fresh, A).main(p) @ &n : !res] by rewrite Pr[mu_eq] // /#. +have ->: Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : res = false] + = Pr[BPS1.G(BPS1.Ref, A).main(p) @ &n : !res] by rewrite Pr[mu_eq] // /#. +by rewrite Pr[mu_not] Pr[mu_not] F_ll P_ll BPSeq. +qed. + +local lemma pr2_fresh_ref_ev (p : param_t) (E : bool) &n : + Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : res = E] + = Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : res = E]. +proof. +have BPSeq := BPS2.eq_pr_fresh_ref A A_ll A_bound2 p &n. +have F_ll : Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : true] = 1%r. ++ byphoare => //; proc; call (A_ll BPS2.Fresh _); 1: by proc; auto; smt(d2_ll). + by inline*; auto. +have P_ll : Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : true] = 1%r. ++ byphoare => //; proc; call (A_ll BPS2.Ref _); 1: by proc; auto. + by inline*; auto; smt(dlist_ll d2_ll N_ge0). +case E => _. ++ have ->: Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : res = true] + = Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : res] by rewrite Pr[mu_eq] // /#. + have ->: Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : res = true] + = Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : res] by rewrite Pr[mu_eq] // /#. + exact BPSeq. +have ->: Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : res = false] + = Pr[BPS2.G(BPS2.Fresh, A).main(p) @ &n : !res] by rewrite Pr[mu_eq] // /#. +have ->: Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : res = false] + = Pr[BPS2.G(BPS2.Ref, A).main(p) @ &n : !res] by rewrite Pr[mu_eq] // /#. +by rewrite Pr[mu_not] Pr[mu_not] F_ll P_ll BPSeq. +qed. + +(* Transitivity 1: [Game_i] ≡ [G_Joint_i]. Couple the [p] draw, then lift the + per-[p] fresh≡ref equality through it (bypr + the [prX_fresh_ref_ev] helper). *) +local lemma Game1_eq_Joint1 &m : + Pr[Game1(A).main() @ &m : res] = Pr[G_Joint1.main() @ &m : 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] 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 (pr1_fresh_ref_ev arg{2} ga &2). +auto. +qed. + +local lemma Game2_eq_Joint2 &m : + Pr[Game2(A).main() @ &m : res] = Pr[G_Joint2.main() @ &m : 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 (pr2_fresh_ref_ev arg{2} ga &2). +auto. +qed. + +(* Joint distribution of (p, xs): sample p from d_param, sample xs from + the per-p dlist, return the pair. *) +op joint1 = dlet d_param (fun p => dmap (dlist (d1 p) N) (fun xs => (p, xs))). +op joint2 = dlet d_param (fun p => dmap (dlist (d2 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 &m : + Pr[G_Joint1.main() @ &m : res] = Pr[Sample(B).main(joint1) @ &m : 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 (d1 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 &m : + Pr[G_Joint2.main() @ &m : res] = Pr[Sample(B).main(joint2) @ &m : 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 (d2 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 + [dominated_12_uniform] 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. ++ have dom_a : dominated M (d1 a) (d2 a) + by split; [exact M_ge0 | exact (dominated_12_uniform a a_in)]. + have rinf_dlist : rdiv_inf (dlist (d1 a) N) (dlist (d2 a) N) <= M ^ N. + + apply (ler_trans (RField.exp (rdiv_inf (d1 a) (d2 a)) N)); + first exact (rdiv_inf_dlist _ _ _ _ N_ge0 dom_a). + apply ler_pexp; first by smt(N_ge0). + split; first exact (rdiv_inf_ge0 _ _ _ dom_a). + by move=> _; apply rdiv_inf_le_ub; + [exact M_ge0 | exact (dominated_12_uniform a a_in)]. + have dlist_pt : mu1 (dlist (d1 a) N) ys <= M ^ N * mu1 (dlist (d2 a) N) ys. + + apply (ler_trans (rdiv_inf (dlist (d1 a) N) (dlist (d2 a) N) * mu1 (dlist (d2 a) N) ys)). + + exact (rdiv_inf_upper_bound _ _ _ _ (dominated_dlist _ _ _ _ N_ge0 dom_a)). + by apply ler_wpmul2r; [exact ge0_mu1 | exact rinf_dlist]. + 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. +apply rdiv_inf_le_ub; first by smt(M_ge0 expr_ge0 N_ge0). +by case=> a ys; exact (joint_pt_bound a ys). +qed. + +(* Transitivity 2 (the Rényi step): single application of [adv_rdiv_inf] + on the joint distribution. *) +local lemma Joint_rdiv_bound &m : + Pr[G_Joint1.main() @ &m : res] <= + M ^ N * + Pr[G_Joint2.main() @ &m : res]. +proof. +rewrite (G_Joint1_vs_Sample &m) (G_Joint2_vs_Sample &m). +apply (ler_trans _ _ _ (adv_rdiv_inf B (fun b => b) &m (M ^ N) joint1 joint2 joint_dom)). +apply ler_wpmul2r; first by rewrite Pr[mu_ge0]. +exact joint_rdiv_inf_bound. +qed. + +(* -- PUBLIC: parametric user-facing lemma -------------------------------- *) + +lemma rdiv_bound_sampler &m : + Pr[Game1(A).main() @ &m : res] <= + M ^ N * + Pr[Game2(A).main() @ &m : res]. +proof. +rewrite (Game1_eq_Joint1 &m) (Game2_eq_Joint2 &m). +exact (Joint_rdiv_bound &m). +qed. + +end section. + +end RDivOracle.