Skip to content

Commit

Permalink
Fix PIR with Benjamin
Browse files Browse the repository at this point in the history 
Benjamin thinks we need to get rid of the if in the code as well.
  • Loading branch information
@fdupress
fdupress committed Jun 27, 2022
1 parent 7b8a319 commit 68f0b01
Showing 1 changed file with 51 additions and 35 deletions.
86 changes: 51 additions & 35 deletions examples/PIR.ec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -201,15 +201,17 @@ proof.
+ by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
+ while(0 <= j <= N);auto;smt (N_pos).
while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r;2,3:smt(N_pos).
while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r; 2,3:smt(N_pos).
+ by move=> &hr /> _;rewrite -set0E N_pos /=; apply is_restr_fset0.
+ move=> H.
case (oflist PIR.s = restr x j);first last.
+ seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s) j /\ oflist PIR.s <> restr x j).
+ auto => /> &hr H0j ???? b ?.
rewrite restrS //= oflist_cons.
smt (is_restr_addS is_restrS is_restr_Ueq is_restr_diff fset0U is_restr_restr).
by conseq H => /#.
+ if.
+ by conseq H=> /#.
by hoare.
+ by hoare;auto.
smt().
conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
Expand All @@ -219,19 +221,23 @@ proof.
is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
+ by auto => /> /#.
+ by wp => /=;rnd (pred1 (j0 \in x));skip => /> &hr;rewrite dbool1E.
+ conseq H => />.
+ case: (j0 \in x) => Hjx ?? His Hof.
+ by rewrite oflist_cons restrS 1:/# Hjx Hof.
by rewrite restrS 1:/# Hjx Hof /= fset0U.
smt (is_restrS is_restr_addS oflist_cons).
+ conseq H => />.
+ move=> &hr ?? His Hof Hb.
rewrite restrS 1:/# (negbRL _ _ Hb).
case (j0 \in x) => /= Hj0x.
+ by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His).
by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
smt (is_restrS is_restr_addS oflist_cons).
+ if.
+ conseq H=> />.
+ case: (j0 \in x) => Hjx ?? His Hof.
+ by rewrite oflist_cons restrS 1:/# Hjx Hof.
by rewrite restrS 1:/# Hjx Hof /= fset0U.
smt (is_restrS is_restr_addS oflist_cons).
skip=> [/> ge1_Sj0 ge_Sj_N s0_j0 s0_x_j0 Sj0_N|].
+ have ->: j0 + 1 = N by smt().
by rewrite expr0.
smt(restrS oflist_cons fset0U).
+ if.
+ conseq H=> /> &0 />.
+ smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
smt(is_restr_addS oflist_cons is_restrS fset0U).
by hoare; skip; smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
move=> &hr /> ?????; rewrite -exprS 1:/#; congr;congr;ring.
+ wp;rnd predT;skip => /> &hr.
smt (dbool_ll oflist_cons is_restrS is_restr_addS).
move=> z;auto=> />;smt (dbool_ll).
Expand Down Expand Up @@ -260,9 +266,11 @@ proof.
case (oflist PIR.s' = restr x j);first last.
+ seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s') j /\ oflist PIR.s' <> restr x j).
+ auto => /> &hr 5? b _.
case: (j{hr}=i{hr}) => />; rewrite restrS //= oflist_cons;
case: (j{hr}=i{hr}) => />; rewrite restrS //= oflist_cons;
smt (is_restr_addS is_restrS is_restr_Ueq is_restr_diff fset0U is_restr_restr).
by conseq H => /#.
if.
+ by conseq H => /#.
by hoare; auto.
+ by hoare;auto.
smt().
conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
Expand All @@ -272,29 +280,37 @@ proof.
is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
+ by auto => /#.
+ by wp => /=;rnd (pred1 ((j0 = i) ^^ (j0 \in x)));skip => /> &hr;rewrite dbool1E.
+ conseq H => />.
+ move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=.
+ rewrite xorC xor_true => <<-.
+ if.
+ conseq H => />.
+ move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=.
+ rewrite xorC xor_true => <<-.
case: (j0 \in x) => Hjx.
+ by rewrite restrS 1:/# Hjx /= oflist_cons Hof.
by rewrite /= restrS 1:/# Hjx /= fset0U Hof.
rewrite xorC xor_false => ?.
case: (j0 \in x) => Hjx.
+ by rewrite restrS 1:/# Hjx /= oflist_cons Hof.
by rewrite /= restrS 1:/# Hjx /= fset0U Hof.
rewrite xorC xor_false => ?.
case: (j0 \in x) => Hjx.
+ by rewrite oflist_cons restrS 1:/# Hjx Hof.
by rewrite restrS 1:/# Hjx Hof /= fset0U.
smt (is_restrS is_restr_addS oflist_cons).
+ conseq H => />.
+ move=> &hr ?? His Hof Hb.
rewrite restrS 1:/# (negbRL _ _ Hb);case: (j0 = i{hr}) => /= [<<- | ?].
+ rewrite xorC xor_true /=.
+ by rewrite oflist_cons restrS 1:/# Hjx Hof.
by rewrite restrS 1:/# Hjx Hof /= fset0U.
smt (is_restrS is_restr_addS oflist_cons).
skip=> /> &0 *.
+ have ->: j0 + 1 = N by smt().
by rewrite expr0.
smt(oflist_cons restrS fset0U).
+ if.
+ conseq H => />.
+ move=> &hr ?? His Hof Hb.
rewrite restrS 1:/# (negbRL _ _ Hb);case: (j0 = i{hr}) => /= [<<- | ?].
+ rewrite xorC xor_true /=.
case (j0 \in x) => /= Hj0x /=.
+ by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His).
by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
rewrite xorC xor_false.
case (j0 \in x) => /= Hj0x /=.
+ by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His).
by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
rewrite xorC xor_false.
case (j0 \in x) => /= Hj0x /=.
+ by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His).
by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
smt (is_restrS is_restr_addS oflist_cons).
smt (is_restrS is_restr_addS oflist_cons).
hoare; auto=> /> &0.
smt(oflist_cons restrS in_fsetU in_fset1 nin_is_restr fset0U).
by move=> &hr /> ?????;rewrite -exprS 1:/#;congr;congr;ring.
+ wp;rnd predT;skip => &hr.
smt (dbool_ll oflist_cons is_restrS is_restr_addS).
Expand Down

0 comments on commit 68f0b01

Please sign in to comment.