From fd1de9071032d1304ba47fb12d745e4daa5199c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 3 Jun 2026 18:56:53 +0100 Subject: [PATCH] in list sampling, make distribution a parameter This allows the equivalences to be used when the distribution cannot be fixed at cloning time, in particular when it is parameterised by a dynamically generated value. --- examples/MEE-CBC/CBC.eca | 8 ++-- theories/distributions/DList.ec | 65 +++++++++++++++++---------------- 2 files changed, 37 insertions(+), 36 deletions(-) diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca index 919539f18..cf5a4e417 100644 --- a/examples/MEE-CBC/CBC.eca +++ b/examples/MEE-CBC/CBC.eca @@ -180,16 +180,16 @@ module Random = { section Random_Ideal. local clone import Program as Sampling with - type t <- block, - op d <- dBlock + type t <- block proof *. equiv Random_Ideal: Random.enc ~ Ideal.enc: size p{1} = size p{2} ==> ={res}. proof. proc. - outline {2} 1 by { r <@ Sampling.Sample.sample(size p + 1); }. + outline {2} 1 by { r <@ Sampling.Sample.sample(dBlock, size p + 1); }. rewrite equiv[{2} 1 Sampling.Sample_LoopSnoc_eq]. - by inline; wp; while (={i} /\ c{1} = l{2} /\ size p{1} + 1 = n{2}); auto=> /#. + inline; wp. + by while (={i} /\ c{1} = l{2} /\ size p{1} + 1 = n{2} /\ d{2} = dBlock); auto=> /#. qed. end section Random_Ideal. diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec index da0ba6d61..54e8835b0 100644 --- a/theories/distributions/DList.ec +++ b/theories/distributions/DList.ec @@ -174,7 +174,7 @@ lemma dlist_fu (d: 'a distr) (xs:'a list): xs \in dlist d (size xs). proof. move=> fu; rewrite /support dlist1E 1:size_ge0 /=. -by apply Bigreal.prodr_gt0_seq => /= a Hin _;apply fu. +by apply Bigreal.prodr_gt0_seq => /= a Hin _; apply fu. qed. lemma dlist_uni (d:'a distr) n : @@ -333,10 +333,9 @@ qed. abstract theory Program. type t. - op d: t distr. module Sample = { - proc sample(n:int): t list = { + proc sample(d: t distr, n:int): t list = { var r; r <$ dlist d n; @@ -345,7 +344,7 @@ abstract theory Program. }. module SampleCons = { - proc sample(n:int): t list = { + proc sample(d: t distr, n:int): t list = { var r, rs; rs <$ dlist d (n - 1); @@ -355,7 +354,7 @@ abstract theory Program. }. module Loop = { - proc sample(n:int): t list = { + proc sample(d: t distr, n:int): t list = { var i, r, l; i <- 0; @@ -370,7 +369,7 @@ abstract theory Program. }. module LoopSnoc = { - proc sample(n:int): t list = { + proc sample(d: t distr, n:int): t list = { var i, r, l; i <- 0; @@ -384,45 +383,47 @@ abstract theory Program. } }. - lemma pr_Sample _n &m xs: Pr[Sample.sample(_n) @ &m: res = xs] = mu (dlist d _n) (pred1 xs). - proof. by byphoare (_: n = _n ==> res = xs)=> //=; proc; rnd. qed. + lemma pr_Sample _d _n &m xs: + Pr[Sample.sample(_d, _n) @ &m: res = xs] = mu (dlist _d _n) (pred1 xs). + proof. by byphoare (: d = _d /\ n = _n ==> res = xs)=> //=; proc; rnd. qed. - equiv Sample_SampleCons_eq: Sample.sample ~ SampleCons.sample: 0 < n{1} /\ ={n} ==> ={res}. + equiv Sample_SampleCons_eq: Sample.sample ~ SampleCons.sample: 0 < n{1} /\ ={d, n} ==> ={res}. proof. - bypr (res{1}) (res{2})=> //= &1 &2 xs [lt0_n] <-. - rewrite (pr_Sample n{1} &1 xs); case (size xs = n{1})=> [<<-|]. - case xs lt0_n=> [|x xs lt0_n]; 1: smt(). + bypr (res{1}) (res{2})=> //= &1 &2 xs [lt0_n] [] <- <-. + rewrite (pr_Sample d{1} n{1} &1 xs); move: lt0_n; case (size xs = n{1})=> [<-|]. + + case: xs=> [|x xs lt0_n]; 1: smt(). rewrite dlistS1E. - byphoare (_: n = size xs + 1 ==> x::xs = res)=> //=; 2: by rewrite addrC. - proc; seq 1: (rs = xs) (mu (dlist d (size xs)) (pred1 xs)) (mu d (pred1 x)) _ 0%r => //. - by rnd (pred1 xs); skip; smt(). - by rnd (pred1 x); skip; smt(). - by hoare; auto; smt(). - smt(). - move=> len_xs; rewrite dlist1E 1:/# ifF 1:/#. + byphoare (: d = d{1} /\ n = size xs + 1 ==> x::xs = res)=> //=; 2: by rewrite addrC. + proc; seq 1: (rs = xs) (mu (dlist d{1} (size xs)) (pred1 xs)) (mu d{1} (pred1 x)) _ 0%r (d = d{1}) => //. + + by auto. + + by rnd (pred1 xs); skip; smt(). + + by rnd (pred1 x); skip; smt(). + + by hoare; auto; smt(). + + smt(). + move=> len_xs gt0_n; rewrite dlist1E 1:/# ifF 1:/#. byphoare (_: n = n{1} ==> xs = res)=> //=; hoare. proc; auto=> />; smt(supp_dlist_size). qed. - equiv Sample_Loop_eq: Sample.sample ~ Loop.sample: ={n} ==> ={res}. + equiv Sample_Loop_eq: Sample.sample ~ Loop.sample: ={d, n} ==> ={res}. proof. proc*; exists* n{1}; elim* => _n. move: (eq_refl _n); case (_n <= 0)=> //= h. - + inline *;rcondf{2} 4;auto;smt (supp_dlist0 weight_dlist0). + + inline *;rcondf{2} 5;auto;smt (supp_dlist0 weight_dlist0). have {h} h: 0 <= _n by smt (). - call (_: _n = n{1} /\ ={n} ==> ={res})=> //=. + call (_: _n = n{1} /\ ={d, n} ==> ={res})=> //=. elim _n h=> //= [|_n le0_n ih]. - proc; rcondf{2} 3; auto=> />. smt(supp_dlist0 weight_dlist0). + + by proc; rcondf{2} 3; auto=> />; smt(supp_dlist0 weight_dlist0). case (_n = 0)=> [-> | h]. - proc; rcondt{2} 3; 1:(by auto); rcondf{2} 6; 1:by auto. + + proc; rcondt{2} 3; 1:(by auto); rcondf{2} 6; 1:by auto. wp; rnd (fun x => head witness x) (fun x => [x]). - auto => />;split => [ rR ? | _ rL ]. + auto => /> &0;split => [ rR ? | _ rL ]. + by rewrite dlist1E //= big_consT big_nil. - rewrite supp_dlist //;case rL => //=; smt (size_eq0). + by rewrite supp_dlist //;case rL => //=; smt (size_eq0). transitivity SampleCons.sample - (={n} /\ 0 < n{1} ==> ={res}) - (_n + 1 = n{1} /\ ={n} /\ 0 < n{1} ==> ={res})=> //=; 1:smt(). - by conseq Sample_SampleCons_eq. + (={d, n} /\ 0 < n{1} ==> ={res}) + (_n + 1 = n{1} /\ ={d, n} /\ 0 < n{1} ==> ={res})=> //=; 1:smt(). + + by conseq Sample_SampleCons_eq. proc; splitwhile{2} 3: (i < n - 1). rcondt{2} 4; 1:by auto; while (i < n); auto; smt(). rcondf{2} 7; 1:by auto; while (i < n); auto; smt(). @@ -430,17 +431,17 @@ abstract theory Program. outline {1} 1 ~ Sample.sample. rewrite equiv[{1} 1 ih]. inline. - by wp; while (={i} /\ ={l} /\ n0{1} = n{2} - 1); auto; smt(). + by wp; while (={i, l} /\ d0{1} = d{2} /\ n0{1} = n{2} - 1); auto; smt(). qed. - equiv Sample_LoopSnoc_eq: Sample.sample ~ LoopSnoc.sample: ={n} ==> ={res}. + equiv Sample_LoopSnoc_eq: Sample.sample ~ LoopSnoc.sample: ={d, n} ==> ={res}. proof. proc*. replace* {1} { x } by { x; r <- rev r; }. inline *; wp; rnd rev; auto. smt(revK dlist_rev). rewrite equiv[{1} 1 Sample_Loop_eq]. - inline *; wp; while (={i, n0} /\ rev l{1} = l{2}); auto => />. + inline *; wp; while (={i, n0, d0} /\ rev l{1} = l{2}); auto => />. smt(rev_cons cats1). qed. end Program.