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

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.

Author: fdupress

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.
 

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,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.