Skip to content

Commit 85241bc

Browse files
gebnergebner
authored
Merge pull request #573 from FStarLang/gebner_rmoldwhile
Remove legacy while-loop syntax
2 parents 827fc0f + 2c2570d commit 85241bc

40 files changed

Lines changed: 138 additions & 779 deletions

‎lib/pulse/lib/Pulse.Lib.Sort.Merge.Array.fst‎

Lines changed: 13 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ let merge_invariant_prop
2020
(hi: SZ.t)
2121
(l1_0: Ghost.erased (list t))
2222
(l2_0: Ghost.erased (list t))
23-
(cont: bool)
2423
i1 i2 (res: bool) accu l1 l2
2524
: Tot prop
2625
=
@@ -31,8 +30,7 @@ let merge_invariant_prop
3130
if res
3231
then spec_merge compare accu l1 l2
3332
else (false, accu `List.Tot.append` (l1 `List.Tot.append` l2))
34-
) /\
35-
cont == (res && not (i1 = i2 || i2 = hi))
33+
)
3634

3735
let merge_invariant // FIXME: WHY WHY WHY?
3836
(#tl #th: Type)
@@ -47,7 +45,6 @@ let merge_invariant // FIXME: WHY WHY WHY?
4745
(pi1: R.ref SZ.t)
4846
(pi2: R.ref SZ.t)
4947
(pres: R.ref bool)
50-
(cont: bool)
5148
i1 i2 (res: bool) c c1 c2 accu l1 l2
5249
: Tot slprop
5350
=
@@ -61,7 +58,7 @@ let merge_invariant // FIXME: WHY WHY WHY?
6158
Trade.trade
6259
(SM.seq_list_match c accu vmatch ** (SM.seq_list_match c1 l1 vmatch ** SM.seq_list_match c2 l2 vmatch))
6360
(SM.seq_list_match c1_0 l1_0 vmatch ** SM.seq_list_match c2_0 l2_0 vmatch) **
64-
pure (merge_invariant_prop compare lo hi l1_0 l2_0 cont i1 i2 res accu l1 l2)
61+
pure (merge_invariant_prop compare lo hi l1_0 l2_0 i1 i2 res accu l1 l2)
6562

6663
inline_for_extraction
6764
fn merge
@@ -107,27 +104,22 @@ requires
107104
let mut pi2 = mi;
108105
let mut pres = true;
109106
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres
110-
(not (lo = mi || mi = hi))
111107
lo mi true
112108
c1l c1 c2 [] l1_0 l2_0
113109
);
114110
while (
115-
with gcont gi1 gi2 gres c c1' c2' accu l1' l2' .
116-
assert (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gcont gi1 gi2 gres c c1' c2' accu l1' l2');
117-
unfold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gcont gi1 gi2 gres c c1' c2' accu l1' l2');
111+
unfold merge_invariant;
118112
let i1 = !pi1;
119113
let i2 = !pi2;
120114
let res = !pres;
121-
let cont = (res && not (i1 = i2 || i2 = hi));
122-
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres cont gi1 gi2 gres c c1' c2' accu l1' l2');
123-
cont
115+
(res && not (i1 = i2 || i2 = hi))
124116
)
125-
invariant cont . exists* i1 i2 res c c1' c2' accu l1' l2' .
126-
merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres cont i1 i2 res c c1' c2' accu l1' l2'
117+
invariant exists* i1 i2 res c c1' c2' accu l1' l2'.
118+
merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2'
127119
{
128120
with gi1 gi2 gres c c1' c2' accu l1 l2 .
129-
assert (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres true gi1 gi2 gres c c1' c2' accu l1 l2);
130-
unfold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres true gi1 gi2 gres c c1' c2' accu l1 l2);
121+
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gi1 gi2 gres c c1' c2' accu l1 l2);
122+
unfold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gi1 gi2 gres c c1' c2' accu l1 l2);
131123
let prf_res : squash (gres == true) = ();
132124
SM.seq_list_match_length vmatch c1' l1;
133125
SM.seq_list_match_length vmatch c2' l2;
@@ -158,7 +150,7 @@ requires
158150
Trade.elim (vmatch x2 (List.Tot.hd l2) ** _) _;
159151
if (comp = 0s) {
160152
pres := false;
161-
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres false gi1 gi2 false c
153+
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gi1 gi2 false c
162154
c1'
163155
c2'
164156
accu
@@ -181,8 +173,7 @@ requires
181173
as (pts_to_range a (SZ.v gi2) (SZ.v hi) c2');
182174
rewrite (pts_to_range a (SZ.v i1') (Ghost.reveal (SZ.v gi2)) (Seq.tail c1'))
183175
as (pts_to_range a (SZ.v i1') (SZ.v gi2) (Seq.tail c1'));
184-
let gcont' = Ghost.hide (gres && not (i1' `size_eq` gi2 || gi2 `size_eq` hi));
185-
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gcont' i1' gi2 gres
176+
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres i1' gi2 gres
186177
(Seq.append c (Seq.cons x1 Seq.empty))
187178
(Seq.tail c1')
188179
c2'
@@ -208,8 +199,7 @@ requires
208199
pi2 := i2';
209200
merge_aux_consume_2 vmatch c accu c1' l1 c2' l2 x2 ();
210201
Trade.trans _ _ (SM.seq_list_match c1 l1_0 vmatch ** SM.seq_list_match c2 l2_0 vmatch);
211-
let gcont' = Ghost.hide (gres && not (i1' `size_eq` i2' || i2' `size_eq` hi));
212-
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres gcont' i1' i2' gres
202+
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres i1' i2' gres
213203
(Seq.append c (Seq.cons x2 Seq.empty))
214204
c1'
215205
(Seq.tail c2')
@@ -220,8 +210,8 @@ requires
220210
}
221211
};
222212
with i1 i2 res c c1' c2' accu l1' l2' .
223-
assert (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres false i1 i2 res c c1' c2' accu l1' l2');
224-
unfold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres false i1 i2 res c c1' c2' accu l1' l2');
213+
fold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2');
214+
unfold (merge_invariant vmatch compare a c1 c2 lo hi l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2');
225215
SM.seq_list_match_length vmatch c1' l1';
226216
SM.seq_list_match_length vmatch c2' l2';
227217
List.Tot.append_l_nil l1';

‎lib/pulse/lib/Pulse.Lib.Sort.Merge.Slice.fst‎

Lines changed: 13 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ let merge_invariant_prop
2020
(len: SZ.t)
2121
(l1_0: Ghost.erased (list t))
2222
(l2_0: Ghost.erased (list t))
23-
(cont: bool)
2423
i1 i2 (res: bool) accu l1 l2
2524
: Tot prop
2625
=
@@ -33,8 +32,7 @@ let merge_invariant_prop
3332
if res
3433
then spec_merge compare accu l1 l2
3534
else (false, accu `List.Tot.append` (l1 `List.Tot.append` l2))
36-
) /\
37-
cont == (res && not (i1 = i2 || i2 = len))
35+
)
3836

3937
let merge_invariant
4038
(#tl #th: Type)
@@ -47,7 +45,6 @@ let merge_invariant
4745
(pi1: R.ref SZ.t)
4846
(pi2: R.ref SZ.t)
4947
(pres: R.ref bool)
50-
(cont: bool)
5148
i1 i2 (res: bool) c c1 c2 accu l1 l2
5249
: Tot slprop
5350
= exists* ca .
@@ -60,7 +57,7 @@ let merge_invariant
6057
(SM.seq_list_match c accu vmatch ** (SM.seq_list_match c1 l1 vmatch ** SM.seq_list_match c2 l2 vmatch))
6158
(SM.seq_list_match c1_0 l1_0 vmatch ** SM.seq_list_match c2_0 l2_0 vmatch) **
6259
pure (ca == (Seq.append c (Seq.append c1 c2))) **
63-
pure (merge_invariant_prop compare (S.len a) l1_0 l2_0 cont i1 i2 res accu l1 l2)
60+
pure (merge_invariant_prop compare (S.len a) l1_0 l2_0 i1 i2 res accu l1 l2)
6461

6562
let merge_case_1
6663
(#t: Type)
@@ -139,27 +136,22 @@ requires
139136
let mut pi2 = mi;
140137
let mut pres = true;
141138
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres
142-
(not (0sz = mi || mi = S.len a))
143139
0sz mi true
144140
Seq.empty c1 c2 [] l1_0 l2_0
145141
);
146142
while (
147-
with gcont gi1 gi2 gres c c1' c2' accu l1' l2' .
148-
assert (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gcont gi1 gi2 gres c c1' c2' accu l1' l2');
149-
unfold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gcont gi1 gi2 gres c c1' c2' accu l1' l2');
143+
unfold merge_invariant;
150144
let i1 = !pi1;
151145
let i2 = !pi2;
152146
let res = !pres;
153-
let cont = (res && not (i1 = i2 || i2 = S.len a));
154-
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres cont gi1 gi2 gres c c1' c2' accu l1' l2');
155-
cont
147+
(res && not (i1 = i2 || i2 = S.len a))
156148
)
157-
invariant cont . exists* i1 i2 res c c1' c2' accu l1' l2' .
158-
merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres cont i1 i2 res c c1' c2' accu l1' l2'
149+
invariant exists* i1 i2 res c c1' c2' accu l1' l2' .
150+
merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2'
159151
{
160152
with gi1 gi2 gres c c1' c2' accu l1 l2 .
161-
assert (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres true gi1 gi2 gres c c1' c2' accu l1 l2);
162-
unfold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres true gi1 gi2 gres c c1' c2' accu l1 l2);
153+
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gi1 gi2 gres c c1' c2' accu l1 l2);
154+
unfold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gi1 gi2 gres c c1' c2' accu l1 l2);
163155
let prf_res : squash (gres == true) = ();
164156
S.pts_to_len a;
165157
SM.seq_list_match_length vmatch c accu;
@@ -186,7 +178,7 @@ requires
186178
Trade.elim (vmatch x2 (List.Tot.hd l2) ** _) _;
187179
if (comp = 0s) {
188180
pres := false;
189-
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 (* pc pc1 pc2 *) pi1 pi2 pres false gi1 gi2 false c
181+
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 (* pc pc1 pc2 *) pi1 pi2 pres gi1 gi2 false c
190182
c1'
191183
c2'
192184
accu
@@ -202,12 +194,11 @@ requires
202194
seq_helper_1 c1' x1;
203195
merge_aux_consume_1 vmatch c accu c1' l1 c2' l2 x1 ();
204196
Trade.trans _ _ (SM.seq_list_match c1 l1_0 vmatch ** SM.seq_list_match c2 l2_0 vmatch);
205-
let gcont' = Ghost.hide (gres && not (i1' `size_eq` gi2 || gi2 `size_eq` S.len a));
206197
List.Tot.append_assoc accu l1 l2;
207198
List.Tot.append_assoc accu [List.Tot.hd l1] (List.Tot.tl l1);
208199
List.Tot.append_assoc (List.Tot.append accu [List.Tot.hd l1]) (List.Tot.tl l1) l2;
209200
merge_case_1 c x1 c1' c2';
210-
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gcont' i1' gi2 gres
201+
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres i1' gi2 gres
211202
(Seq.append c (Seq.cons x1 Seq.empty))
212203
(Seq.tail c1')
213204
c2'
@@ -230,13 +221,12 @@ requires
230221
pi2 := i2';
231222
merge_aux_consume_2 vmatch c accu c1' l1 c2' l2 x2 ();
232223
Trade.trans _ _ (SM.seq_list_match c1 l1_0 vmatch ** SM.seq_list_match c2 l2_0 vmatch);
233-
let gcont' = Ghost.hide (gres && not (i1' `size_eq` i2' || i2' `size_eq` S.len a));
234224
List.Tot.append_assoc l1 [List.Tot.hd l2] (List.Tot.tl l2);
235225
List.Tot.append_assoc accu (List.Tot.append l1 [List.Tot.hd l2]) (List.Tot.tl l2);
236226
List.Tot.append_assoc accu l1 [List.Tot.hd l2];
237227
List.Tot.append_assoc accu [List.Tot.hd l2] l1;
238228
List.Tot.append_assoc (List.Tot.append accu [List.Tot.hd l2]) l1 (List.Tot.tl l2);
239-
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres gcont' i1' i2' gres
229+
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres i1' i2' gres
240230
(Seq.append c (Seq.cons x2 Seq.empty))
241231
c1'
242232
(Seq.tail c2')
@@ -247,8 +237,8 @@ requires
247237
}
248238
};
249239
with i1 i2 res c c1' c2' accu l1' l2' .
250-
assert (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres false i1 i2 res c c1' c2' accu l1' l2');
251-
unfold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres false i1 i2 res c c1' c2' accu l1' l2');
240+
fold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2');
241+
unfold (merge_invariant vmatch compare a c1 c2 l1_0 l2_0 pi1 pi2 pres i1 i2 res c c1' c2' accu l1' l2');
252242
SM.seq_list_match_append_intro_trade vmatch c1' l1' c2' l2';
253243
List.Tot.append_length l1' l2';
254244
Trade.trans_hyp_r (SM.seq_list_match c accu vmatch) (SM.seq_list_match (Seq.append c1' c2') (List.Tot.append l1' l2') vmatch) (SM.seq_list_match c1' l1' vmatch ** SM.seq_list_match c2' l2' vmatch) _;

‎lib/pulse/lib/Pulse.Lib.WhileLoop.fst‎

Lines changed: 2 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -20,27 +20,7 @@ open Pulse.Main
2020
open Pulse.Lib.Core
2121

2222

23-
fn rec while_loop'
24-
(inv:bool -> slprop)
25-
(cond:unit -> stt bool (exists* x. inv x) (fun b -> inv b))
26-
(body:unit -> stt unit (inv true) (fun _ -> exists* x. inv x))
27-
norewrite
28-
requires exists* x. inv x
29-
ensures inv false
30-
{
31-
let b = cond ();
32-
if b {
33-
body ();
34-
while_loop' inv cond body;
35-
}
36-
}
37-
38-
39-
let while_loop inv cond body =
40-
while_loop' inv (fun _ -> cond) (fun _ -> body)
41-
42-
43-
fn rec nu_while_loop
23+
fn rec while_loop
4424
(inv:slprop)
4525
(post:bool -> slprop)
4626
(cond:unit -> stt bool inv (fun b -> post b))
@@ -51,6 +31,6 @@ fn rec nu_while_loop
5131
let b = cond ();
5232
if b {
5333
body ();
54-
nu_while_loop inv post cond body;
34+
while_loop inv post cond body;
5535
}
5636
}

‎lib/pulse/lib/Pulse.Lib.WhileLoop.fsti‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,6 @@ open Pulse.Lib.Core
77
(* Not to be called directly. *)
88

99
fn while_loop
10-
(inv : bool -> slprop)
11-
(cond : stt bool (exists* x. inv x) (fun b -> inv b))
12-
(body : stt unit (inv true) (fun _ -> exists* x. inv x))
13-
norewrite
14-
requires exists* x. inv x
15-
ensures inv false
16-
17-
fn nu_while_loop
1810
(inv:slprop)
1911
(post:bool -> slprop)
2012
(cond:unit -> stt bool inv (fun b -> post b))

‎share/pulse/examples/AuxPredicate.fst‎

Lines changed: 6 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,10 @@ module R = Pulse.Lib.Reference
2626

2727
// Defining a slprop using F* syntax. We do not yet allow
2828
// writing Pulse syntax for slprops in predicates
29-
let my_inv (b:bool) (r:R.ref int) : slprop
29+
let my_inv (r:R.ref int) : slprop
3030
= exists* v.
3131
pts_to r v **
32-
pure ( (v==0 \/ v == 1) /\ b == (v = 0) )
32+
pure ( (v==0 \/ v == 1) )
3333

3434

3535

@@ -40,54 +40,30 @@ fn invar_introduces_ghost (r:R.ref int)
4040
{
4141
r := 0;
4242

43-
fold (my_inv true r); //to prove the precondition of the while loop
43+
fold (my_inv r); //to prove the precondition of the while loop
4444

4545
while
4646
( //unfold the predicate to expose its contents to the prover context
47-
with b. unfold (my_inv b r);
47+
unfold my_inv;
4848
let vr = !r;
4949
let res = (vr = 0);
5050
//show that the condition restores the invariant by explicitly folding it back
51-
fold (my_inv res r);
5251
res
5352
)
54-
invariant b. my_inv b r
53+
invariant my_inv r
5554
{
5655
// Same in the body;
5756
// unfold to expose it
58-
unfold (my_inv true r);
5957
r := 1;
6058
// fold it back to show its preserved
61-
fold (my_inv false r)
59+
fold (my_inv r)
6260
};
6361

6462
// unfold after the loop for the postcondition
65-
unfold (my_inv false r)
6663
}
6764

6865

6966

70-
[@@expect_failure]
71-
72-
fn invar_introduces_orig (r:R.ref int)
73-
requires pts_to r 0
74-
ensures pts_to r 1
75-
{
76-
r := 0;
77-
78-
fold (my_inv true r);
79-
80-
while (let vr = !r; //fails here, as expected; we have my_inv, not pts_to
81-
(vr = 0))
82-
invariant b. my_inv b r
83-
{
84-
r := 1;
85-
};
86-
87-
()
88-
}
89-
90-
9167
// If you don't introduce the indirection of my_inv
9268
// it just works without further ado
9369

@@ -104,38 +80,3 @@ fn invar_introduces_ghost_alt (r:R.ref int)
10480
r := 1;
10581
}
10682
}
107-
108-
109-
// Some other examples
110-
111-
112-
fn exists_introduces_ghost (r:R.ref int)
113-
requires pts_to r 0
114-
ensures exists* v. pts_to r v ** pure (v == 0 \/ v == 1)
115-
{
116-
r := 0;
117-
118-
fold (my_inv true r);
119-
120-
introduce exists* b. (my_inv b r) with _;
121-
// once you hide the witness in the existential
122-
// you lose knowledge about it, i.e., we do not know that r = 0
123-
with b. unfold (my_inv b r)
124-
}
125-
126-
127-
128-
fn with_assert_OK (r:R.ref int)
129-
preserves pts_to r 0
130-
{
131-
r := 0;
132-
133-
fold (my_inv true r);
134-
135-
with b. assert (my_inv b r); // similar to above but we don't lose access
136-
// to witness b=true because with...assert...
137-
// puts b=true into the typing context
138-
139-
assert (my_inv true r);
140-
unfold (my_inv true r);
141-
}

0 commit comments

Comments
 (0)