Skip to content

Commit 7d4b40f

Browse files
dfirsovdfirsov
authored
initial code upload
0 parents  commit 7d4b40f

24 files changed

+8331
-0
lines changed

‎Averaging.ec

Lines changed: 293 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,293 @@
1+
pragma Goals:printall.
2+
require import AllCore Distr List Binomial.
3+
require import Ring StdRing StdOrder StdBigop Discrete RealSeq RealSeries RealLub.
4+
(*---*) import IterOp Bigint Bigreal Bigreal.BRA.
5+
(*---*) import IntOrder RealOrder RField.
6+
require import Finite.
7+
require (*--*) FinType.
8+
require import RandomFacts.
9+
require FiniteApproximation.
10+
11+
theory Avg.
12+
13+
type at. (* argument type *)
14+
type rt. (* return type *)
15+
type at1, at2.
16+
17+
module type RunAvg = {
18+
proc main(r : at, i2 : at2) : rt
19+
}.
20+
21+
module WorkAvg(A : RunAvg) = {
22+
proc main(d : at distr, i2 : at2) = {
23+
var r, b,i22,dd;
24+
i22 <- i2;
25+
dd <- d;
26+
r <$ dd;
27+
b <- A.main(r,i22);
28+
return (b, r);
29+
}
30+
}.
31+
32+
33+
34+
section.
35+
36+
local module WorkAvg'(A : RunAvg) = {
37+
proc main(d : at distr, i2 : at2) = {
38+
var r, b;
39+
r <$ d;
40+
b <- A.main(r,i2);
41+
return r;
42+
}
43+
}.
44+
45+
46+
declare module A : RunAvg.
47+
48+
clone import FiniteApproximation.FinApprox with type rt <- at,
49+
type at <- at distr * at2.
50+
51+
52+
local lemma finApproxCons &m d :
53+
exists (D : at distr), exists (J : int -> at option),
54+
(forall M, mu D M = Pr[ WorkAvg'(A).main(d) @ &m : M res ])
55+
/\ enumerate J (support D)
56+
/\ (forall (epsilon : real), 0%r < epsilon
57+
=> exists (N : int),
58+
Pr[ WorkAvg'(A).main(d)
59+
@ &m : ! (res \in (pmap J (range 0 N))) ] < epsilon).
60+
elim (fin_approx_prog_no_glob (WorkAvg'(A)) &m d).
61+
progress. exists D. exists J. progress.
62+
qed.
63+
64+
65+
local lemma be &m P d : Pr[WorkAvg(A).main(d) @ &m : P res.`2 ]
66+
= Pr[WorkAvg'(A).main(d) @ &m : P res ].
67+
byequiv. proc.
68+
call (_:true).
69+
rnd. wp. skip. progress. progress. auto.
70+
qed.
71+
72+
73+
local lemma ebse &m P d i2 : Pr[WorkAvg'(A).main(d,i2) @ &m : P res ] <= mu d P.
74+
proof. byphoare (_: arg = (d , i2) ==> _). proc.
75+
seq 1 : (P r) (mu d P) 1%r 1%r 0%r.
76+
rnd. skip. auto.
77+
rnd. skip. smt.
78+
call (_: true ==> true). bypr. move => &m0 _. rewrite Pr[mu_le1]. auto. skip. auto.
79+
hoare. call (_:true). skip. auto. auto. auto. auto.
80+
qed.
81+
82+
83+
local lemma hzc ['a] : forall (d : 'a distr),
84+
mu d (fun x => x \in d) = mu d predT.
85+
proof. smt. qed.
86+
87+
88+
local lemma le7main &m (d : at distr) i2 :
89+
exists (J : int -> at option) ,
90+
enumerate J (support d)
91+
/\ (forall (epsilon : real), 0%r < epsilon =>
92+
exists (N : int), Pr[ WorkAvg(A).main(d,i2)
93+
@ &m : ! (res.`2 \in (pmap J (range 0 N))) ] < epsilon).
94+
proof.
95+
have : summable (mass d).
96+
smt.
97+
move => sd.
98+
have : exists (J : int -> at option) ,
99+
enumerate J (support (mass d)).
100+
apply (sum_to_enum (mass d) sd).
101+
elim. move => j smd. exists j.
102+
have : (support (mass d)) = (support d).
103+
apply fun_ext. move => a. smt.
104+
move => ee. split. rewrite - ee. apply smd.
105+
elim (finApproxCons &m (d,i2)). move => D J. progress.
106+
have ejD : enumerate j (support D).
107+
apply (jokk D d). move => M. rewrite H. apply (ebse &m M d).
108+
smt.
109+
elim (H1 epsilon H2). move => N prep.
110+
elim (prjokk D J j ejD H0 N).
111+
move => N0 prop2. exists N0.
112+
rewrite (be &m (fun r => !(r \in pmap j (range 0 N0)))).
113+
have opm1 : Pr[WorkAvg'(A).main(d,i2)
114+
@ &m : (fun (r : at) => ! (r \in pmap j (range 0 N0))) res]
115+
= Pr[WorkAvg'(A).main(d,i2)
116+
@ &m : res \in D /\ (fun r => !(r \in pmap j (range 0 N0))) res].
117+
rewrite - (H (fun r => (r \in D) /\ (fun r => !(r \in pmap j (range 0 N0))) r)).
118+
rewrite - (H (fun r => ! (r \in pmap j (range 0 N0)))). simplify.
119+
rewrite mu_and. smt.
120+
rewrite opm1.
121+
have : Pr[WorkAvg'(A).main(d,i2)
122+
@ &m : (res \in D) /\ (fun r => ! (r \in pmap j (range 0 N0))) res]
123+
<= Pr[WorkAvg'(A).main(d,i2)
124+
@ &m : res \in D /\ ! (res \in pmap J (range 0 N))].
125+
rewrite Pr[mu_sub]. smt. auto.
126+
move => ineq.
127+
have : Pr[WorkAvg'(A).main(d,i2)
128+
@ &m : (res \in D) /\ ! (res \in pmap J (range 0 N))]
129+
= Pr[WorkAvg'(A).main(d,i2) @ &m : ! (res \in pmap J (range 0 N))].
130+
rewrite - (H (fun r => (r \in D) /\ (fun r => ! (r \in pmap J (range 0 N))) r)).
131+
rewrite - (H (fun r => ! (r \in pmap J (range 0 N)))). simplify.
132+
rewrite mu_and. timeout 30. smt.
133+
smt.
134+
qed.
135+
136+
137+
local lemma oks' &m P d i2:
138+
summable (fun r => (mu1 d r) * Pr[ A.main(r,i2) @ &m : P res ]).
139+
simplify summable. exists 1%r.
140+
move => J u.
141+
have oks : big predT (fun (i : at) => `|mu1 d i|) J <= 1%r.
142+
have oks' : (fun (i : at) => `|mu1 d i|) = (fun (i : at) => mass d i).
143+
apply fun_ext. move => i. smt.
144+
rewrite oks'.
145+
smt.
146+
have : big predT (fun i => `|mu1 d i * Pr[A.main(i,i2) @ &m : P res]|) J
147+
<= big predT (fun i => `|mu1 d i|) J.
148+
apply ler_sum_seq .
149+
move => a aj _. simplify.
150+
have : 0%r <= Pr[A.main(a,i2) @ &m : P res] <= 1%r.
151+
rewrite Pr[mu_le1]. auto. rewrite Pr[mu_ge0]. auto.
152+
elim. move => q1 q2.
153+
rewrite abs1.
154+
rewrite (abs2 (Pr[A.main(a,i2) @ &m : P res])). progress.
155+
have : `|mu1 d a| >= 0%r. apply abs3.
156+
move => q. smt.
157+
smt.
158+
qed.
159+
160+
161+
local lemma oks'' &m P J (d : at distr) i2 :
162+
enumerate J (support d) =>
163+
enumerate J (support (fun (r : at) => mu1 d r * Pr[A.main(r,i2) @ &m : P res])).
164+
move => ep. split.
165+
elim ep. progress.
166+
simplify support.
167+
elim ep. move => _ qq.
168+
move => x xpr. apply qq.
169+
smt.
170+
qed.
171+
172+
173+
local lemma jk &m P d i2 : forall l, uniq l =>
174+
big predT (fun (r : at) => mu1 d r * Pr[A.main(r,i2) @ &m : P res]) l
175+
= Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 /\ mem l res.`2 ].
176+
proof. apply list_ind. simplify. rewrite Pr[mu_false]. smt.
177+
move => x l. simplify.
178+
move => ih ihp.
179+
have e : Pr[WorkAvg(A).main(d,i2)
180+
@ &m : P res.`1 /\ (res.`2 = x \/ (res.`2 \in l))] =
181+
Pr[WorkAvg(A).main(d,i2)
182+
@ &m : (P res.`1 /\ res.`2 = x) \/ (P res.`1 /\ res.`2 \in l)].
183+
rewrite Pr[mu_eq]. smt. auto. rewrite e. clear e.
184+
have e : Pr[WorkAvg(A).main(d,i2)
185+
@ &m : P res.`1 /\ res.`2 = x \/ P res.`1 /\ (res.`2 \in l)]
186+
= Pr[WorkAvg(A).main(d,i2)
187+
@ &m : P res.`1 /\ res.`2 = x ]
188+
+ Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 /\ (res.`2 \in l)].
189+
rewrite Pr[mu_disjoint]. smt. auto.
190+
rewrite e. clear e.
191+
have e : Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 /\ res.`2 = x]
192+
= mu1 d x * Pr[A.main(x,i2) @ &m : P res].
193+
byphoare (_: exists ga, ga = (glob A) /\ ga = (glob A){m} /\ arg = (d,i2) ==> _).
194+
proc. elim*. move => ga.
195+
pose z := (Pr[A.main(x,i2) @ &m : P res]).
196+
seq 2 : (ga = (glob A) /\ ga = (glob A){m} /\ (d, i2) = (dd, i22))
197+
1%r (mu1 d x * z) 0%r 0%r.
198+
wp. skip. auto.
199+
wp. skip.
200+
have zp : z = Pr[A.main(x, i2) @ &m : P res]. smt.
201+
progress.
202+
seq 1 : (r = x) (mu1 d x) z 1%r 0%r
203+
(glob A = ga /\ (glob A){m} = ga /\ i22 = i2 /\ d = d).
204+
sp. rnd. wp. skip. progress.
205+
rnd. skip. progress.
206+
have pp : phoare [ A.main : arg = (x,i2) /\ glob A = (glob A){m} /\ (glob A) = ga
207+
==> P res ] = Pr[A.main(x,i2) @ &m : P res].
208+
bypr. move => &m0 c.
209+
byequiv (_: (glob A){1} = ga /\ (glob A){2} = ga /\ ={r,i2} ==> _) .
210+
proc*. call (_:true). skip. progress. smt. progress.
211+
call pp. skip. progress. smt.
212+
hoare. call(_:true). skip. progress. smt. smt. hoare. wp. skip . smt.
213+
smt.
214+
smt.
215+
auto .
216+
smt.
217+
qed.
218+
219+
220+
local lemma oks &m P d i2 :
221+
exists (J : int -> at option),
222+
enumerate J (support (fun r => (mu1 d r) * Pr[ A.main(r,i2) @ &m : P res ]))
223+
/\ summable (fun r => (mu1 d r) * Pr[ A.main(r,i2) @ &m : P res ])
224+
/\ RealSeq.convergeto
225+
(fun N => big predT (fun r => (mu1 d r) * Pr[ A.main(r,i2) @ &m : P res])
226+
(pmap J (range 0 N)))
227+
(Pr[ WorkAvg(A).main(d,i2) @ &m : P res.`1 ]).
228+
proof. elim (le7main &m d i2). move => J. elim. progress. exists J.
229+
split.
230+
apply (oks'' &m P J d i2 H).
231+
split.
232+
apply oks'.
233+
move => epsilon eps_prop.
234+
elim (H0 epsilon eps_prop).
235+
move => N eq. exists N.
236+
move => n npr.
237+
rewrite jk. smt.
238+
have : Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 /\ (res.`2 \in pmap J (range 0 n))]
239+
<= Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1].
240+
rewrite Pr[mu_sub]. progress. auto.
241+
move => obv.
242+
have : `|Pr[WorkAvg(A).main(d,i2)
243+
@ &m : P res.`1 /\ (res.`2 \in pmap J (range 0 n))] -
244+
Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1]|
245+
= Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1]
246+
- Pr[WorkAvg(A).main(d,i2)
247+
@ &m : P res.`1 /\ (res.`2 \in pmap J (range 0 n))].
248+
smt.
249+
move => obve. rewrite obve.
250+
have : Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1]
251+
- Pr[WorkAvg(A).main(d,i2)
252+
@ &m : P res.`1 /\ (res.`2 \in pmap J (range 0 n))]
253+
= Pr[WorkAvg(A).main(d,i2)
254+
@ &m : P res.`1 /\ !(res.`2 \in pmap J (range 0 n))].
255+
have ze : Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 ]
256+
= Pr[WorkAvg(A).main(d,i2)
257+
@ &m : P res.`1 /\ (res.`2 \in pmap J (range 0 n)) ]
258+
+ Pr[WorkAvg(A).main(d,i2)
259+
@ &m : P res.`1 /\ !(res.`2 \in pmap J (range 0 n)) ].
260+
rewrite Pr[mu_split (res.`2 \in pmap J (range 0 n))]. auto.
261+
rewrite ze. smt.
262+
move => ze. rewrite ze.
263+
have : Pr[WorkAvg(A).main(d,i2) @ &m : P res.`1 /\ !(res.`2 \in pmap J (range 0 n))]
264+
<= Pr[WorkAvg(A).main(d,i2) @ &m : ! (res.`2 \in pmap J (range 0 N))].
265+
rewrite Pr[mu_sub]. progress.
266+
have : forall m x, N <= m => x \in pmap J (range 0 N) => x \in pmap J (range 0 m).
267+
smt.
268+
move => zne. clear ze obve obv. clear H0 H.
269+
smt (pmc). auto. smt.
270+
qed.
271+
272+
273+
lemma averaging &m M i d :
274+
Pr[ WorkAvg(A).main(d,i) @ &m : M res.`1 ]
275+
= sum (fun x => (mu1 d x) * Pr[ A.main(x,i) @ &m : M res ]).
276+
elim (oks &m M d i). move => J. elim. move => e s. elim s.
277+
move => s c1.
278+
have f2 : RealSeq.convergeto
279+
(fun N => big predT
280+
(fun r => (mu1 d r) * Pr[ A.main(r,i) @ &m : M res ])
281+
(pmap J (range 0 N)))
282+
(sum (fun r => (mu1 d r) * Pr[ A.main(r,i) @ &m : M res ])).
283+
apply (summable_cnvto
284+
(fun r => (mu1 d r) * Pr[ A.main(r,i) @ &m : M res ]) J
285+
(support (fun r => (mu1 d r) * Pr[ A.main(r,i) @ &m : M res ]))).
286+
progress. auto. auto.
287+
smt.
288+
qed.
289+
290+
291+
end section.
292+
end Avg.
293+

0 commit comments

Comments
 (0)