Skip to content

Commit dbeb478

Browse files
nikswamynikswamy
authored
Merge branch 'main' into nik_testcase_for_extraction_with_interfaces
2 parents cb2e5e2 + 85241bc commit dbeb478

47 files changed

Lines changed: 357 additions & 836 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.devcontainer/fromscratch/minimal.Dockerfile‎

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FROM ubuntu:24.04
1+
FROM mcr.microsoft.com/devcontainers/base:ubuntu
22

33
# Base dependencies: opam
44
# CI dependencies: jq (to identify F* branch)
@@ -28,17 +28,13 @@ RUN apt-get update \
2828
# Same for pkg-config. OPAM prompts even if we're giving --yes
2929
# and setting OPAMYES.
3030

31-
# Create a new user and give them sudo rights
32-
ARG USER=vscode
33-
RUN useradd -d /home/$USER -s /bin/bash -m $USER
34-
RUN echo "$USER ALL=NOPASSWD: ALL" >> /etc/sudoers
35-
USER $USER
36-
ENV HOME /home/$USER
37-
WORKDIR $HOME
38-
RUN mkdir -p $HOME/bin
31+
USER vscode
32+
ENV HOME=/home/vscode
33+
WORKDIR /home/vscode
3934

4035
# Make sure ~/bin is in the PATH
41-
RUN echo 'export PATH=$HOME/bin:$HOME/.local/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
36+
RUN mkdir -p $HOME/bin
37+
RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
4238

4339
# Install Rust
4440
RUN rustup install stable
@@ -51,7 +47,7 @@ ARG OCAML_VERSION=5.3.0
5147
RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
5248
RUN opam option depext-run-installs=true
5349
ENV OPAMYES=1
54-
RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
50+
RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace domainslib
5551

5652
# Get F* master and build (install opam deps too)
5753
RUN eval $(opam env) \
@@ -68,8 +64,9 @@ RUN ./FStar/.scripts/get_fstar_z3.sh $HOME/bin
6864
# Get karamel master and build (installing opam deps too, but ignoring fstar dependency)
6965
RUN eval $(opam env) \
7066
&& . $HOME/.profile \
71-
&& git clone --depth=1 https://github.com/FStarLang/karamel \
67+
&& git clone https://github.com/FStarLang/karamel \
7268
&& cd karamel/ \
69+
&& git checkout d6607b99477640cb1e5d423d5cbe709d76da61f7 \
7370
&& sed -i '/"fstar"/d' karamel.opam \
7471
&& opam install --yes --deps-only ./karamel.opam \
7572
&& make -j$(nproc)

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ jobs:
5858
with:
5959
path: karamel
6060
repository: FStarLang/karamel
61-
ref: master
61+
ref: d6607b99477640cb1e5d423d5cbe709d76da61f7
6262

6363
- name: Try fetch built karamel
6464
id: cache-karamel

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -376,7 +376,7 @@ fn length_iter (#t:Type) (x: llist t)
376376
Pulse.Lib.Reference.(cur := next);
377377
Pulse.Lib.Reference.(ctr := n + 1);
378378
};
379-
with _n ll _sfx. _;
379+
with _ _n ll _sfx. _;
380380
is_list_cases_none ll;
381381
T.elim _ _;
382382
let n = Pulse.Lib.Reference.(!ctr);
@@ -523,7 +523,7 @@ fn append_iter (#t:Type) (x y:llist t)
523523
as (forall* tl. is_list next tl @==> is_list x ((pfx@[reveal hd])@tl));
524524
Pulse.Lib.Reference.(cur := next);
525525
};
526-
with ll pfx sfx. _;
526+
with _ ll pfx sfx. _;
527527
append_at_last_cell Pulse.Lib.Reference.(!cur) y;
528528
(* finally, use the quqnatified postcondition of the invariant *)
529529
FA.elim_forall_imp (is_list ll) (fun sfx' -> is_list x (pfx @ sfx')) (sfx@'l2);
@@ -596,7 +596,7 @@ fn split (#t:Type0) (x:llist t) (n:U32.t) (#xl:erased (list t))
596596
List.Tot.append_length pfx [hd];
597597
non_empty_list next; (* need to prove Some? next *)
598598
};
599-
with i ll pfx sfx. _;
599+
with _ i ll pfx sfx. _;
600600
let last = Pulse.Lib.Reference.(!cur);
601601
let y = detach_next last;
602602
with hd tl. _;
@@ -679,7 +679,7 @@ fn reverse (#t:Type0) (x:llist t)
679679
List.Tot.Properties.rev_rev' _rev_pfx;
680680
List.Tot.Properties.append_assoc (List.Tot.rev _rev_pfx) [n.head] tl;
681681
};
682-
with _p _c _rev_pfx _suffix. _;
682+
with _ _p _c _rev_pfx _suffix. _;
683683
is_list_cases_none _c;
684684
drop_ (is_list _c _suffix);
685685
List.Tot.Properties.append_l_nil (List.Tot.rev _rev_pfx);

‎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))

0 commit comments

Comments
 (0)