Skip to content

[distributions] in programmatic list sampling, make the distribution dynamic #1030

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
fdupress wants to merge 1 commit into
base: main
Choose a base branch
from
+37 −36
Draft

[distributions] in programmatic list sampling, make the distribution dynamic #1030

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions examples/MEE-CBC/CBC.eca
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
65 changes: 33 additions & 32 deletions theories/distributions/DList.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down Expand Up @@ -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;
Expand All @@ -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);
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -384,63 +383,65 @@ 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().
wp; rnd.
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.
Loading