easycrypt-rewinding/RewSumBindingGeneric.ec at main · dfirsov/easycrypt-rewinding · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
pragma Goals:printall.
require import AllCore DBool.
require import Distr.
require import List.
require import AllCore List Binomial.
require import Ring StdRing StdOrder StdBigop Discrete RealSeq RealSeries.
(*---*) import IterOp Bigint Bigreal Bigreal.BRA.
(*---*) import IntOrder RealOrder RField.
require import Finite.
require (*--*) FinType.
require import RandomFacts.

require RewBasics.
theory RSBA.


type sbits, irt, rrt,iat.

op pair_sbits : sbits * sbits -> sbits.
op unpair: sbits -> sbits * sbits.
axiom ips: injective pair_sbits.
axiom unpair_pair x : unpair (pair_sbits x) = x.


clone import RewBasics as RW with type sbits <- sbits,
                                  type rrt <- rrt,
                                  type irt <- irt,
                                  type iat <- iat,
                                  op pair_sbits <- pair_sbits,
                                  op unpair <- unpair.


require RewWithInit.
clone import RewWithInit.RWI as RWAW with type sbits <- sbits,
                                         type iat   <- iat,
                                         type irt   <- irt,
                                         type rrt <- rrt,
                                         op pair_sbits <- pair_sbits,
                                         op unpair <- unpair.


require RewCommutes.
clone import RewCommutes.SpecRewCommutes as SRC with type rt1 <- rrt,
                                                     type rt2 <- rrt,
                                                     type iat <- iat,
                                                     type sbits <- sbits,
                                                     type irt <- irt,
                                                     type rrt <- rrt,
                                                     op pair_sbits <- pair_sbits,
                                                     op unpair <- unpair.

require RewSumBindingAux.
clone import RewSumBindingAux.RSBH as RSBH with type sbits <- sbits,
                                                    type rrt <- rrt,
                                                    type irt <- irt,
                                                    type iat <- iat,
                                                    op pair_sbits <- pair_sbits,
                                                    op unpair <- unpair.


section.
declare module A <: RewRunExec1Exec2.
declare module B <: Initializer.


declare axiom Afl : islossless A.ex1.
declare axiom Agl : islossless A.ex2.
declare axiom Bin : islossless B.init.

(* due to EC restrictions (bug) these are not provable and not reduciable to one another  *)
declare axiom Bsens    : equiv[ B.init ~ B.init : ={arg, glob A, glob B} ==> ={glob A, res} ].
declare axiom Bsens'   : equiv[ B.init ~ B.init : ={arg, glob A, glob B} ==> ={glob A, glob B, res} ].
declare axiom Bsens''  : equiv[ B.init ~ B.init : ={arg, glob A, glob B} ==> ={glob A} ].
declare axiom Bsens''' : equiv[ B.init ~ B.init : ={arg, glob A, glob B} ==> ={res, glob A} ].


declare axiom RewProp :
  exists (f : glob A -> sbits),
  injective f /\
  (forall &m, Pr[ A.getState() @ &m : (glob A) = ((glob A){m})
                                   /\ res = f ((glob A){m} ) ] = 1%r) /\
  (forall &m b (x: glob A), b = f x =>
    Pr[A.setState(b) @ &m : glob A = x] = 1%r) /\
  islossless A.setState.


local lemma Ass : islossless A.setState.
proof. elim RewProp. progress. qed.


local lemma fact1 &m P i : Pr[ SB(A,B).main(i) @ &m : P res.`1 /\ P res.`2 ] >= Pr[ SB(A,B).main_run(i) @ &m : P res ]^2.
have : forall &m,
      Pr[QQ(SBB(A), B).main_run(i) @ &m : (fun (x : irt * rrt) => P x.`2) res] ^ 2 <=
      Pr[QQ(SBB(A), B).main(i) @ &m : (fun (x : irt * rrt) => P x.`2) res.`1 /\ (fun (x : irt * rrt) => P x.`2)  res.`2 ].
move => &m0.
apply (rew_with_init (SBB(A)) B).
elim (rewindable_A A RewProp). move => fA [s1 [s2 [s3]]] s4. simplify. apply Bsens''.
simplify.
apply Bsens'''.
elim RewProp. progress.
exists f. progress.
rewrite - (H0 &m1). byequiv. proc*.  inline*. wp. call (_:true).
      skip. progress. auto. auto.
rewrite -  (H1 &m1 (f x) x). auto.
byequiv. proc*. inline*. sp.   call(_:true). skip. progress. auto. auto.
proc. call H2. skip. auto.
proc. seq 1 : (true). rnd. auto. rnd.  skip. auto. smt(@DBool).
if. call Afl. skip. auto. call Agl. skip. auto.  hoare.  simplify. rnd. skip. auto.  auto.
apply Bin.
simplify.
have q : Pr[QQ(SBB(A), B).main_run(i) @ &m : P res.`2] = Pr[SB(A, B).main_run(i) @ &m : P res].
        byequiv (_: (={i, glob A, glob B}) ==> _). proc.
seq 1 1 : (={glob A} /\ r0{1} = ix{2}). call Bsens. skip. auto.
inline*. wp.
conseq (_: exists ga, ga = (glob A){1} /\ ={glob A} /\ r0{1} = ix{2} ==> _). smt(). sp.
simplify.
seq 1 1 : (i0{2} = ix{2} /\
  i0{1} = r0{1} /\
  exists (ga : (glob A)), ga = (glob A){1} /\ ={glob A} /\ r0{1} = ix{2} /\ ={x}).
rnd. skip. progress. smt().
if.  smt(). call (_:true). skip. progress. call(_:true). skip. progress. auto.
auto.
rewrite - q. clear q.
have q : Pr[QQ(SBB(A), B).main(i) @ &m : P res.`1.`2 /\ P res.`2.`2] = Pr[SB(A, B).main(i) @ &m : P res.`1 /\ P res.`2].
byequiv (_: (={i, glob A, glob B}) ==> _). proc. simplify.
conseq (_: P r1{1} /\  P r2{1} <=>  (P r1{2} /\ P r2{2})).
seq 1 1 : (={glob A} /\ r0{1} = ix{2}). call Bsens. skip. auto.
call (_: ={glob A, i} ==> ={res}). proc.
seq 1 1 : (={i,x, glob A}). rnd. skip. progress.
if. auto. call(_:true). skip. progress.
call (_:true). skip. progress.
inline {1} SBB(A).setState. call (_:true).
wp.
call (_:(={glob A})).
seq 1 1 : (={i,x, glob A}). rnd. skip. progress.
if.  auto. call (_:true). skip. progress.
call (_:true). skip. progress.
inline {1} SBB(A).getState. wp. call (_:true). skip. progress. auto. auto.
rewrite - q.
move => eqr.
rewrite eqr.
qed.


local lemma fact3' P &m i : Pr[SB(A,B).main_run(i) @ &m : P res] = 1%r / 2%r * Pr[SB(A,B).main_1(i) @ &m : P res]
                                                                 + 1%r / 2%r * Pr[SB(A,B).main_2(i) @ &m : P res].
apply (fact3 A B). apply Afl. apply Agl. apply Ass. apply Bsens.
qed.


local lemma fact4 &m P i : Pr[SB(A,B).main_11(i) @ &m : P res.`1 /\ P res.`2] <= Pr[SB(A,B).main_1(i) @ &m : P res].
byequiv (_: (={i, glob A, glob B}) ==> _). proc.
seq 1 1 : (={glob A, ix}). call Bsens. skip. auto.
seq 2 1 : (r1{1} = r{2}).
elim (rewindable_A A RewProp). move => fA [s1 [s2 [s3]]] s4.
call (_:true). conseq (_: exists ga, ga = (glob A){1} /\ ={glob A, ix} ==> _). smt().
elim*. move => ga.
call {1} (s2 ga). skip. smt().
call {1} (_:true ==> true). apply Afl.
call {1} (_:true ==> true). apply Ass.
skip. auto. auto. auto.
qed.


local lemma fact5 &m P i : Pr[SB(A,B).main_22(i) @ &m : P res.`1 /\ P res.`2] <= Pr[SB(A,B).main_2(i) @ &m : P res].
byequiv (_: (={i,glob A, glob B}) ==> _). proc.
seq 1 1 : (={glob A, ix}). call Bsens. skip. auto.
seq 2 1 : (r1{1} = r{2}).
elim (rewindable_A A RewProp). move => fA [s1 [s2 [s3]]] s4.
call (_:true). conseq (_: exists ga, ga = (glob A){1} /\ ={glob A, ix} ==> _). smt().
elim*. move => ga.
call {1} (s2 ga). skip. smt().
call {1} (_:true ==> true). apply Agl.
call {1} (_:true ==> true). apply Ass.
skip. auto. auto. auto.
qed.


local lemma deriv &m P i :
   1%r/2%r * Pr[ SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2 ]
   + 1%r/2%r * Pr[ SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2 ]
    >= 2%r * Pr[ SB(A,B).main_run(i) @ &m :  P res ] *  (Pr[ SB(A,B).main_run(i) @ &m :  P res ] - (1%r/2%r)).
proof.
pose V_rnd_rnd := Pr[SB(A,B).main(i) @ &m : P res.`1 /\ P res.`2].
pose V_rnd := Pr[SB(A,B).main_run(i) @ &m : P res ].
pose V_12  := Pr[SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2].
pose V_21  := Pr[SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2].
pose V_22  := Pr[SB(A,B).main_22(i) @ &m : P res.`1 /\ P res.`2].
pose V_11  := Pr[SB(A,B).main_11(i) @ &m : P res.`1 /\ P res.`2].
pose V_1  := Pr[SB(A,B).main_1(i) @ &m : P res].
pose V_2  := Pr[SB(A,B).main_2(i) @ &m : P res].
have tr1 :
   1%r/2%r * V_12
 + 1%r/2%r * V_21
 = 2%r * (1%r/4%r * V_12 + 1%r/4%r * V_21 + 1%r/4%r * V_11 + 1%r/4%r * V_22
   - (1%r/4%r * V_11 + 1%r/4%r * V_22)).
smt().
rewrite tr1. clear tr1.
rewrite - (fact2  A B). apply Afl.  apply Agl. apply Ass. apply Bsens.
have se : Pr[SB(A,B).main(i) @ &m : P res.`1 /\ P res.`2 ] = V_rnd_rnd. reflexivity.
rewrite se. clear se.
have v_1_11 : V_11 <= V_1. apply fact4.
have v_2_22 : V_22 <= V_2. apply fact5.
have ntg :
  2%r * (V_rnd ^ 2 - 1%r / 2%r * V_rnd) <= 2%r * (V_rnd_rnd - (1%r / 4%r * V_1 + 1%r / 4%r * V_2)).
have tr3 : (1%r / 4%r * V_1 + 1%r / 4%r * V_2) = (1%r/2%r * ((1%r / 2%r * V_1 + 1%r / 2%r * V_2))).
smt(). rewrite tr3.
have tr4 : V_rnd = (1%r / 2%r * V_1 + 1%r / 2%r * V_2).
apply fact3'.
rewrite - tr4.
have lk : V_rnd ^ 2 <= V_rnd_rnd . apply fact1.
smt().
smt(@Real).
qed.


local lemma fin_deriv' &m P i :
  Pr[ SB(A,B).main_1(i) @ &m : P res ] + Pr[ SB(A,B).main_2(i) @ &m : P res ]
   <= 1%r +  Pr[ SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2 ] + Pr[ SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2 ].
case (Pr[ SB(A,B).main_run(i) @ &m :  P res ] <= 1%r/2%r).
move => ass1.
have s1 : 1%r/2%r * Pr[ SB(A,B).main_1(i) @ &m :  P res ]
         + 1%r/2%r * Pr[ SB(A,B).main_2(i) @ &m :  P res ] <= 1%r/2%r.
rewrite - fact3'. apply ass1.
smt(@Distr).
move => pr_reln.
have pr_rel : Pr[SB(A,B).main_run(i) @ &m : P res] > 1%r/2%r. smt(). clear pr_reln.
have fr_ab : 1%r/2%r * Pr[ SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2 ]
           + 1%r/2%r * Pr[ SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2 ]
   >= 2%r * Pr[ SB(A,B).main_run(i) @ &m :  P res ] *  (Pr[ SB(A,B).main_run(i) @ &m :  P res ] - (1%r/2%r)). apply deriv.
have : 1%r/2%r * Pr[ SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2 ] + 1%r/2%r * Pr[ SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2 ]
   >= (Pr[ SB(A,B).main_run(i) @ &m :  P res ] - (1%r/2%r)).
smt().
rewrite (fact3').
move => strfr_ab.
have qqq : Pr[SB(A,B).main_1(i) @ &m : P res] +
           Pr[SB(A,B).main_2(i) @ &m : P res] - 1%r <=
           Pr[SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2] +
           Pr[SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2].
smt().
smt().
qed.


lemma sum_binding_generic : forall &m M i,
  Pr[ SB(A,B).main_1(i) @ &m : M res ] + Pr[ SB(A,B).main_2(i) @ &m : M res ]
   <= 1%r +  2%r * Pr[ SB(A,B).main_12(i) @ &m : M res.`1 /\ M res.`2 ].
proof. move => &m P i.
have d : 1%r + 2%r * Pr[SB(A, B).main_12(i) @ &m : P res.`1 /\ P res.`2]
          = 1%r + Pr[SB(A, B).main_12(i) @ &m : P res.`1 /\ P res.`2] + Pr[SB(A, B).main_21(i) @ &m : P res.`1 /\ P res.`2].
    have q : Pr[ SB(A,B).main_12(i) @ &m : P res.`1 /\ P res.`2 ]
         = Pr[ SB(A,B).main_21(i) @ &m : P res.`1 /\ P res.`2 ].
  pose M := fun (x : rrt * rrt) => P x.`1 /\ P x.`2.
    have q1 : Pr[ SpecRewComm(A,B).iex1ex2(i) @ &m : M res.`2 ] = Pr[SB(A, B).main_12(i) @ &m : P res.`1 /\ P res.`2 ].
    byequiv (_: (={arg, glob A, glob B}) ==> _ ). proc.
    seq 1 1 : (={glob A} /\ r0{1} = ix{2}). call Bsens. skip. auto.
    call(_:true). call (_:true). call(_:true). call(_:true). skip. progress. smt(). smt().  smt(). smt(). auto.
    auto.
    rewrite - q1. clear q1.
    have q2 : Pr[ SpecRewComm(A,B).iex2ex1(i) @ &m : M res.`2 ] = Pr[SB(A, B).main_21(i) @ &m : P res.`1 /\ P res.`2 ].
    byequiv (_: (={arg,glob A, glob B}) ==> _ ). proc.
    seq 1 1 : (={glob A} /\ r0{1} = ix{2}). call Bsens. skip. auto.
    call(_:true). call (_:true). call(_:true). call(_:true). skip. progress. smt(). smt().  smt(). smt(). auto.
    auto.
    rewrite - q2. clear q2.
    rewrite  (rew_comm_law A B Bsens' RewProp &m (fun (x : irt * (rrt * rrt)) => M x.`2)).  auto.
  rewrite q. smt().
rewrite d.
 apply (fin_deriv' &m P).
qed.


end section.
end RSBA.