Skip to content

Commit

Permalink
Ring/field tactics available as soon as an instance is found.
Browse files Browse the repository at this point in the history
  • Loading branch information
Boutry authored and strub committed Jul 20, 2023
1 parent e75a7cf commit fab074d
Show file tree
Hide file tree
Showing 5 changed files with 160 additions and 93 deletions.
107 changes: 53 additions & 54 deletions examples/PIR.ec
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ module PIR = {
proc query (s:int list) = {
return (big predT a s);
}
}
var s, s' : int list

Expand All @@ -57,7 +57,7 @@ module PIR = {

return r +^ r';
}
}.
lemma PIR_correct &m i0 : 0 <= i0 < N => Pr [PIR.main(i0) @ &m : res = a i0] = 1%r.
Expand All @@ -68,9 +68,9 @@ proof.
conseq (: _ ==> true) (: _ ==> res = a i0)=> //.
+ proc;inline *;wp.
conseq (_: _ ==> sxor2 PIR.s PIR.s' i) => //.
+ by move=> &m -> s s' [] [s1 s2 [-> ->]];rewrite !big_cat big_consT;ring.
+ by move=> &m -> s s' [] [s1 s2 [-> ->]]; rewrite !big_cat big_consT; ring.
while (j <= N /\ if j <= i then PIR.s = PIR.s' else sxor2 PIR.s PIR.s' i).
+ wp;rnd;skip => /= &m [[_]] + HjN.
+ wp;rnd;skip => /= &m [[_]] + HjN.
have -> /= : j{m} + 1 <= N by smt ().
case: (j{m} <= i{m}) => Hji;2: by smt ().
move=> -> b _;case: (j{m} = i{m}) => [->> | /#].
Expand All @@ -79,7 +79,7 @@ proof.
proc;inline *;wp.
while (true) (N-j).
+ move=> z;wp;rnd predT;skip => &hr />;smt (dbool_ll).
by auto=> /#.
by auto=> /#.
qed.
equiv PIR_secure1: PIR.main ~ PIR.main : true ==> ={PIR.s}.
Expand All @@ -100,11 +100,11 @@ proof.
rnd (fun x => !x);skip;smt (dbool_funi dbool_fu).
qed.
lemma PIR_secuity_s_byequiv i1 i2 &m1 &m2 x:
lemma PIR_secuity_s_byequiv i1 i2 &m1 &m2 x:
Pr[PIR.main(i1) @ &m1 : PIR.s = x] = Pr[PIR.main(i2) @ &m2 : PIR.s = x].
proof. by byequiv PIR_secure1. qed.
lemma PIR_secuity_s'_byequiv i1 i2 &m1 &m2 x:
lemma PIR_secuity_s'_byequiv i1 i2 &m1 &m2 x:
Pr[PIR.main(i1) @ &m1 : PIR.s' = x] = Pr[PIR.main(i2) @ &m2 : PIR.s' = x].
proof. by byequiv PIR_secure2. qed.

Expand All @@ -115,14 +115,14 @@ proof. by byequiv PIR_secure2. qed.
require import List FSet.
op restr (s : int fset) n =
op restr (s : int fset) n =
s `&` oflist (iota_ 0 n).
op is_restr (s : int fset) n =
op is_restr (s : int fset) n =
s = restr s n.
lemma restrS s j : 0 <= j =>
restr s (j + 1) =
lemma restrS s j : 0 <= j =>
restr s (j + 1) =
(if (j \in s) then fset1 j else fset0) `|` restr s j.
proof.
move=> H0j;rewrite /restr iotaSr //= -cats1 oflist_cat.
Expand All @@ -142,8 +142,8 @@ proof.
by apply Hs2;rewrite in_fsetU in_fset1.
qed.
lemma is_restr_Ueq n s1 s2 :
is_restr s1 n => is_restr s2 n =>
lemma is_restr_Ueq n s1 s2 :
is_restr s1 n => is_restr s2 n =>
(fset1 n `|` s1 = fset1 n `|` s2) = (s1 = s2).
proof.
move=> Hs1 Hs2;rewrite eq_iff;split => [ | -> //].
Expand All @@ -152,7 +152,7 @@ proof.
by rewrite !nin_is_restr.
qed.
lemma is_restr_addS n s :
lemma is_restr_addS n s :
0 <= n =>
is_restr s n => is_restr (fset1 n `|` s) (n + 1).
proof.
Expand All @@ -164,7 +164,7 @@ lemma is_restrS n s :
0 <= n =>
is_restr s n => is_restr s (n + 1).
proof.
by move=> Hn Hs;rewrite /is_restr restrS // (nin_is_restr _ _ Hs) /= fset0U.
by move=> Hn Hs; rewrite /is_restr restrS // (@nin_is_restr _ _ Hs) /= fset0U.
qed.
lemma is_restr_restr n s : is_restr (restr s n) n.
Expand All @@ -176,7 +176,7 @@ lemma is_restr_fset0 n : is_restr fset0 n.
proof. by apply fsetP => x;rewrite /restr in_fsetI in_fset0. qed.
lemma restr_0 s : restr s 0 = fset0.
proof.
proof.
apply fsetP => x;rewrite /restr in_fsetI in_fset0 mem_oflist mem_iota /#.
qed.
Expand All @@ -185,7 +185,7 @@ axiom N_pos : 0 <= N.
import RField StdOrder.RealOrder.
lemma Pr_PIR_s i0 &m x :
Pr[PIR.main(i0) @ &m : oflist PIR.s = x] =
Pr[PIR.main(i0) @ &m : oflist PIR.s = x] =
if is_restr x N then 1%r/2%r^N else 0%r.
proof.
byphoare=> // {i0};proc;inline *;wp.
Expand All @@ -196,7 +196,7 @@ proof.
+ by auto => &m1 />;rewrite oflist_cons;smt (is_restrS is_restr_addS).
auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s) = restr x j then 1%r/2%r^(N-j) else 0%r)).
+ move=> {&m} &m />;rewrite -set0E.
+ move=> {&m} &m />;rewrite -set0E.
have -> // : fset0 = restr x 0.
+ by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
Expand All @@ -210,16 +210,16 @@ proof.
+ 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.
+ 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=> /#.
+ by hoare;auto.
smt().
smt().
conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
exists * j, PIR.s;elim * => j0 s0.
seq 3: (b = j0 \in x) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
(1 <= j <= N /\ j = j0 + 1 /\ (PIR.s = if b then j0 :: s0 else s0) /\
exists * j, PIR.s;elim * => j0 s0.
seq 3: (b = j0 \in x) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
(1 <= j <= N /\ j = j0 + 1 /\ (PIR.s = if b then j0 :: s0 else s0) /\
is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
+ by auto => /> /#.
+ by wp => /=;rnd (pred1 (j0 \in x));skip => /> &hr;rewrite dbool1E.
Expand All @@ -239,7 +239,7 @@ proof.
qed.
lemma Pr_PIR_s' i0 &m x :
Pr[PIR.main(i0) @ &m : oflist PIR.s' = x] =
Pr[PIR.main(i0) @ &m : oflist PIR.s' = x] =
if is_restr x N then 1%r/2%r^N else 0%r.
proof.
byphoare=> // {i0};proc;inline *;wp.
Expand All @@ -250,16 +250,16 @@ proof.
+ auto;smt (oflist_cons is_restrS is_restr_addS).
auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s') = restr x j then 1%r/2%r^(N-j) else 0%r)).
+ move=> {&m} &m />;rewrite -set0E.
+ move=> {&m} &m />;rewrite -set0E.
have -> // : fset0 = restr x 0.
+ 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).
conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _).
conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _).
+ move=> />; smt(N_pos set0E is_restr_fset0).
while (0 <= j <= N /\ is_restr (oflist PIR.s') j) (N-j) N 1%r => //.
+ move=> /> s j *; have ->>: j = N by smt().
by rewrite subzz expr0.
+ move=> /> s j *; have ->>: j = N by smt().
by rewrite subzz expr0.
+ smt(N_pos).
+ move=> H.
case (oflist PIR.s' = restr x j);first last.
Expand All @@ -269,16 +269,16 @@ proof.
smt (is_restr_addS is_restrS is_restr_Ueq is_restr_diff fset0U is_restr_restr).
by conseq H => /#.
+ by hoare; auto.
smt().
smt().
conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
exists * j, PIR.s';elim * => j0 s0.
seq 3: (b = ((j0 = i) ^^ (j0 \in x))) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
(1 <= j <= N /\ j = j0 + 1 /\ (PIR.s' = if (j0=i) then (if b then s0 else j0::s0) else if b then j0 :: s0 else s0) /\
exists * j, PIR.s';elim * => j0 s0.
seq 3: (b = ((j0 = i) ^^ (j0 \in x))) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
(1 <= j <= N /\ j = j0 + 1 /\ (PIR.s' = if (j0=i) then (if b then s0 else j0::s0) else if b then j0 :: s0 else s0) /\
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}) => /=.
+ 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.
Expand All @@ -290,77 +290,76 @@ proof.
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 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).
+ 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).
+ 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).
by 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).
qed.

lemma PIR_secuity_s_bypr i1 i2 &m1 &m2 x:
lemma PIR_secuity_s_bypr i1 i2 &m1 &m2 x:
Pr[PIR.main(i1) @ &m1 : oflist PIR.s = x] = Pr[PIR.main(i2) @ &m2 : oflist PIR.s = x].
proof. by rewrite (Pr_PIR_s i1 &m1 x) (Pr_PIR_s i2 &m2 x). qed.
proof. by rewrite (@Pr_PIR_s i1 &m1 x) (@Pr_PIR_s i2 &m2 x). qed.

lemma PIR_secuity_s'_bypr i1 i2 &m1 &m2 x:
lemma PIR_secuity_s'_bypr i1 i2 &m1 &m2 x:
Pr[PIR.main(i1) @ &m1 : oflist PIR.s' = x] = Pr[PIR.main(i2) @ &m2 : oflist PIR.s' = x].
proof. by rewrite (Pr_PIR_s' i1 &m1 x) (Pr_PIR_s' i2 &m2 x). qed.
proof. by rewrite (@Pr_PIR_s' i1 &m1 x) (@Pr_PIR_s' i2 &m2 x). qed.
(* Other version without explicite computation of the probability,
we first show that the probability is uniform,
unfortunatly this does not allows to conclude in easycrypt.
We need to be able to do the projection of memories.
We need to be able to do the projection of memories.
So we need functions on memory
*)
lemma PIR_s_uniform (x1 x2 : int fset):
0 <= N =>
is_restr x1 N =>
is_restr x1 N =>
is_restr x2 N =>
equiv [PIR.main ~ PIR.main : ={i} ==> (oflist PIR.s{1} = x1) = (oflist PIR.s{2} = x2)].
proof.
move=> HN B1 B2;proc;inline *;wp.
while (={i,j} /\ 0 <= j{1} <= N /\
while (={i,j} /\ 0 <= j{1} <= N /\
is_restr (oflist PIR.s{1}) j{1} /\ is_restr (oflist PIR.s{2}) j{1} /\
((oflist PIR.s{1} = restr x1 j{1}) = (oflist PIR.s{2} = restr x2 j{1}))).
+ wp.
rnd (fun b => b ^^ (j{1} \in x1) ^^ (j{1} \in x2)).
rnd (fun b => b ^^ (j{1} \in x1) ^^ (j{1} \in x2)).
skip => &m1 &m2 /> H0j HjN Hrs1 Hrs2 Hs Hj; split.
+ by move=> b _;ring.
move=> _ b _;split;1: by ring.
move=> _; rewrite !oflist_cons !restrS //.
move=> _; rewrite !oflist_cons !restrS //.
smt (is_restr_addS is_restrS is_restr_diff is_restr_Ueq is_restr_restr fset0U).
auto; move => &m1 &m2 />.
rewrite !restr_0 -set0E /=;smt (is_restr_fset0).
qed.
lemma PIR_s'_uniform (x1 x2 : int fset):
0 <= N =>
is_restr x1 N =>
is_restr x1 N =>
is_restr x2 N =>
equiv [PIR.main ~ PIR.main : ={i} ==> (oflist PIR.s'{1} = x1) = (oflist PIR.s'{2} = x2)].
proof.
move=> HN B1 B2;proc;inline *;wp.
while (={i,j} /\ 0 <= j{1} <= N /\
while (={i,j} /\ 0 <= j{1} <= N /\
is_restr (oflist PIR.s'{1}) j{1} /\ is_restr (oflist PIR.s'{2}) j{1} /\
((oflist PIR.s'{1} = restr x1 j{1}) = (oflist PIR.s'{2} = restr x2 j{1}))).
+ wp.
rnd (fun b => b ^^ (j{1} \in x1) ^^ (j{1} \in x2)).
rnd (fun b => b ^^ (j{1} \in x1) ^^ (j{1} \in x2)).
skip => &m1 &m2 [#] 2!->> H0j HjN Hrs1 Hrs2 Hs Hj _; split.
+ move=> b _;ring.
move=> _ b _; split;1: by ring.
move=> _; rewrite /= !oflist_cons !restrS //.
move=> _; rewrite /= !oflist_cons !restrS //.
smt (is_restr_addS is_restrS is_restr_diff is_restr_Ueq is_restr_restr fset0U).
auto => &m1 &m2 />.
rewrite !restr_0 -set0E /=;smt (is_restr_fset0).
qed.

2 changes: 1 addition & 1 deletion examples/hashed_elgamal_generic.ec
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ section.
wp; rnd; call (_: ={LRO.m} /\ (forall x, x \in H.qs{2} = x \in LRO.m{2})).
+ by proc; inline *; auto => />; smt (get_setE).
inline *; auto => /> *; split; 1: by move=> *; rewrite mem_empty.
move=> _ ??? hdom ??; split; 1: by move=> *;ring.
move=> _ ??? hdom ??; split; 1: by move=> *; ring.
smt(eq_except_setl get_setE).
qed.
Expand Down
4 changes: 1 addition & 3 deletions src/ecAlgTactic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,7 @@ module Axioms = struct


let tmod_and_deps =
tmod :: [
EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"], "Field")
]
tmod :: []

let zero = "rzero"
let one = "rone"
Expand Down
Loading

0 comments on commit fab074d

Please sign in to comment.