Skip to content

Commit 3b55cb1

Browse files
namasikanamnamasikanam
committed
another example for eHoare
1 parent 7035747 commit 3b55cb1

2 files changed

Lines changed: 203 additions & 1 deletion

File tree

‎examples/ehoare/random_boolean_matrix.ec‎

Lines changed: 191 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,191 @@
1+
require import AllCore Array Real RealExp List.
2+
(*---*) import RField.
3+
require import Distr DBool Xreal.
4+
(*---*) import Biased.
5+
require import StdOrder.
6+
(*---*) import RealOrder.
7+
8+
(* uniformly sampling a 2-d boolean array of size n x m *)
9+
module M = {
10+
proc sample (n : int, m : int, a : bool array) : (bool array) = {
11+
var i, j : int;
12+
var b : bool;
13+
i <- 0;
14+
while (i < n) {
15+
j <- 0;
16+
while (j < m) {
17+
b <$ dbiased 0.5;
18+
a.[i * m + j] <- b;
19+
j <- j + 1;
20+
}
21+
i <- i + 1;
22+
}
23+
return a;
24+
}
25+
}.
26+
27+
op row_eq_upto (i m : int) (a1 a2 : bool array) =
28+
forall (i' j' : int),
29+
0 <= i' < i
30+
=> 0 <= j' < m
31+
=> a1.[i' * m + j'] = a2.[i' * m + j'].
32+
33+
op cell_eq_upto (i j m : int) (a1 a2 : bool array) =
34+
forall (j' : int),
35+
0 <= j' < j
36+
=> a1.[i * m + j'] = a2.[i * m + j'].
37+
38+
lemma row_eq_upto_increase (i m : int) (a1 a2 : bool array):
39+
0 <= i
40+
=> (row_eq_upto i m a1 a2 /\ cell_eq_upto i m m a1 a2
41+
<=> row_eq_upto (i + 1) m a1 a2).
42+
proof.
43+
move => ? @/row_eq_upto @/cell_eq_upto; split.
44+
- move => ? i' j' ??.
45+
by case: (i' < i) => /#.
46+
- move => H; split.
47+
- move => i' j' ??.
48+
have ?: 0 <= i' < i + 1 by smt().
49+
by have := H i' j' _ _.
50+
- by have := H i => /#.
51+
qed.
52+
53+
lemma cell_eq_upto_false (i j' j m : int) (a1 a2 : bool array) :
54+
0 <= j' < j
55+
=> a1.[i * m + j'] <> a2.[i * m + j']
56+
=> cell_eq_upto i j m a1 a2 = false.
57+
proof. by smt(). qed.
58+
59+
lemma cell_eq_upto_split (i j m : int) (a1 a2 : bool array) :
60+
0 <= j < m
61+
=> (cell_eq_upto i (j + 1) m a1 a2
62+
<=> (cell_eq_upto i j m a1 a2
63+
/\ a1.[i * m + j] = a2.[i * m + j])
64+
).
65+
proof.
66+
move => ? @/cell_eq_upto; split.
67+
- move => H; split.
68+
- move => j' ?.
69+
have ?: 0 <= j' < j + 1 by smt().
70+
by have := H j' _.
71+
- by smt().
72+
- move => ? j' ?.
73+
by case (j' < j) => /#.
74+
qed.
75+
76+
lemma row_eq_upto_unrelated_set (i m x : int) (v : bool) (a1 a2 : bool array):
77+
i * m <= x < size a1
78+
=> (row_eq_upto i m a1 a2 <=> row_eq_upto i m a1.[x <- v] a2).
79+
proof.
80+
move => ? @/row_eq_upto; split.
81+
- move => ? i' j' ??.
82+
rewrite get_set 1:/#.
83+
have -> /=: !(i' * m + j' = x) by smt().
84+
by smt().
85+
- move => ? i' j' ??.
86+
by rewrite (_: a1.[_] = a1.[x <- v].[i' * m + j']) 1:get_set /#.
87+
qed.
88+
89+
lemma cell_eq_upto_unrelated_set (i j m x : int) (v : bool) (a1 a2 : bool array) :
90+
0 <= i /\ 0 <= j < m /\ i * m + j <= x < size a1
91+
=> (cell_eq_upto i j m a1 a2 <=> cell_eq_upto i j m a1.[x <- v] a2).
92+
proof.
93+
move => [#] ????? @/cell_eq_upto; split.
94+
- move => ? j' ?.
95+
rewrite get_set 1:/#.
96+
have -> /=: !(i * m + j' = x) by smt().
97+
by smt().
98+
- move => ? j' ?.
99+
by rewrite (_: a1.[_] = a1.[x <- v].[i * m + j']) 1:get_set /#.
100+
qed.
101+
102+
(* The probability of every possible boolean matrix of size n x m is no more than 2 ^ -(n * m) *)
103+
lemma L:
104+
forall (a0 : bool array),
105+
ehoare [M.sample :
106+
(0 <= arg.`1
107+
/\ 0 <= arg.`2
108+
/\ size arg.`3 = arg.`1 * arg.`2
109+
/\ size arg.`3 = size a0)
110+
`|` (1%r / (2%r ^ (n * m)))%xr ==> (res = a0)%xr].
111+
proof.
112+
move => a0.
113+
proc.
114+
while ((0 <= i <= n
115+
/\ 0 <= m
116+
/\ size a = n * m
117+
/\ size a0 = size a)
118+
`|` (2%r ^ ((-(n - i) * m)%r))%xr
119+
* (row_eq_upto i m a a0)%xr).
120+
(* !cond => inv => pos_f <= inv_f *)
121+
+ move => &hr.
122+
apply xle_cxr_r => ?.
123+
apply xle_cxr_r => ?.
124+
have ->: n{hr} - i{hr} = 0 by smt().
125+
rewrite Ring.IntID.mul0r Ring.IntID.oppr0 rpow0 mul1m_simpl.
126+
apply xle_rle; split => *; 1: by smt().
127+
exact le_b2r.
128+
(* {cond /\ inv | inv_f} c {inv | inv_f} *)
129+
+ wp.
130+
while (( 0 <= i < n
131+
/\ 0 <= j <= m
132+
/\ size a = n * m
133+
/\ size a = size a0)
134+
`|` (2%r ^ ((-((n - i) * m - j))%r))%xr
135+
* (row_eq_upto i m a a0 /\ cell_eq_upto i j m a a0)%xr).
136+
(* !cond => inv => pos_f <= inv_f *)
137+
+ move => &hr />.
138+
rewrite xle_cxr_r => ?.
139+
rewrite xle_cxr_l 1:/#.
140+
rewrite (_: - _ * m{hr} = - ((n{hr} - i{hr}) * m{hr} - j{hr})) //= 1:/#.
141+
rewrite (_: j{hr} = m{hr}) 1:/#.
142+
by rewrite -row_eq_upto_increase 1:/# ler_eqVlt; left; reflexivity.
143+
(* {cond /\ inv | inv_f} c {inv | inv_f} *)
144+
+ wp; skip => /> &hr.
145+
rewrite xle_cxr_r => [#] 5? Hsize ?.
146+
rewrite Ep_dbiased /= 1:/#.
147+
have -> /=: 0 <= i{hr} < n{hr} by smt().
148+
have -> /=: 0 <= j{hr} + 1 <= m{hr} by smt().
149+
rewrite !size_set !Hsize /=.
150+
have -> /=: n{hr} * m{hr} = size a0 by smt().
151+
rewrite !to_pos_pos 1,2,3,4,5:#smt:(rpow_gt0 b2r_ge0).
152+
rewrite !cell_eq_upto_split 1,2:/# !get_set //=.
153+
- split; 1: by smt().
154+
move => ?.
155+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
156+
- split; 1: by smt().
157+
move => ?.
158+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
159+
case (a0.[i{hr} * m{hr} + j{hr}]) => Hcase /=.
160+
+ rewrite -row_eq_upto_unrelated_set.
161+
- split; 1: by smt().
162+
move => ?.
163+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
164+
rewrite -cell_eq_upto_unrelated_set.
165+
- do! split; 1,2,3: by smt().
166+
move => ?.
167+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
168+
rewrite -{2}(rpow1 2%r) // -rpowN // -mulrA.
169+
rewrite (mulrC (b2r _) (2%r ^ - 1%r)).
170+
by rewrite mulrA -rpowD // /#.
171+
+ rewrite /= -row_eq_upto_unrelated_set.
172+
- split; 1: by smt().
173+
move => ?.
174+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
175+
rewrite -cell_eq_upto_unrelated_set.
176+
- do! split; 1,2,3: by smt().
177+
move => ?.
178+
by apply (IntOrder.ltr_le_trans ((n{hr} - 1) * m{hr} + m{hr})) => /#.
179+
rewrite -{2}(rpow1 2%r) // -rpowN // -mulrA.
180+
rewrite (mulrC (b2r _) (2%r ^ - 1%r)).
181+
by rewrite mulrA -rpowD // /#.
182+
(* pre => inv *)
183+
+ wp; skip => &hr />.
184+
rewrite xle_cxr_r => [#] ??????.
185+
rewrite xle_cxr_l 1:/#.
186+
by have-> //: cell_eq_upto i{hr} 0 m{hr} a{hr} a0 by smt().
187+
auto => /> &hr.
188+
rewrite xle_cxr_r => [#] ????.
189+
rewrite xle_cxr_l 1:/# fromintN rpowN //= rpow_int //=.
190+
by have ->: row_eq_upto 0 m{hr} a{hr} a0 by smt().
191+
qed.

‎theories/datatypes/Xreal.ec‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
require import AllCore RealSeries List Distr StdBigop DBool DInterval.
22
require import StdOrder.
33
require Subtype Bigop.
4-
import Bigreal Bigint RealOrder.
4+
import Bigreal Bigint RealOrder Biased.
55

66
(* -------------------------------------------------------------------- *)
77
(* Definition of R+ *)
@@ -399,6 +399,9 @@ proof. case: x y => [x|] [y|] //=; smt(@Rp). qed.
399399
lemma xle_add_l x y : x <= y + x.
400400
proof. rewrite addmC xle_add_r. qed.
401401

402+
lemma xle_rle (x y : real) : 0%r <= x <= y => x%xr <= y%xr.
403+
proof. by move => [??] /=; rewrite !to_pos_pos // &(ler_trans x). qed.
404+
402405
lemma xler_add2r (x:realp) (y z : xreal) : y + x%xr <= z + x%xr <=> y <= z.
403406
proof. case: z => // z; case: y => //= y; smt(@Rp). qed.
404407

@@ -963,6 +966,14 @@ proof.
963966
by rewrite big_consT big_seq1 /= !dbool1E.
964967
qed.
965968

969+
lemma Ep_dbiased (p : real) (f : bool -> xreal) :
970+
0%r <= p <= 1%r => Ep (dbiased p) f = p ** f true + (1%r - p) ** f false.
971+
proof.
972+
move => ?.
973+
rewrite (Ep_fin [true; false]) //; 1: by case.
974+
by rewrite /BXA.big /predT /= !dbiased1E /= !clamp_id //.
975+
qed.
976+
966977
(* -------------------------------------------------------------------- *)
967978
lemma Ep_dinterval (f : int -> xreal) i j:
968979
Ep [i..j] f =

0 commit comments

Comments
 (0)