Skip to content

Commit 3e66169

Browse files
mtzguidomtzguido
committed
Update WP optimization test
1 parent 6156792 commit 3e66169

File tree

3 files changed

+33
-227
lines changed

3 files changed

+33
-227
lines changed

‎tests/error-messages/WPExtensionality.fst

+16-73
Original file line numberDiff line numberDiff line change
@@ -17,102 +17,45 @@ module WPExtensionality
1717

1818
open FStar.Tactics.V2
1919

20+
let term_eq = FStar.Reflection.V2.TermEq.term_eq
21+
2022
assume val wp1 : (int -> Type0) -> Type0
2123
assume val wp2 : (int -> unit -> Type0) -> Type0
2224

25+
let check_eq (s:string) (t1 t2 : term) : Tac unit =
26+
if term_eq t1 t2 then () else
27+
fail (Printf.sprintf "Test %s failed\nt1 = %s\nt2 = %s" s (term_to_string t1) (term_to_string t2))
28+
2329
(* 1 arg direct *)
2430
let direct_1 ()
2531
= assert True
26-
by (let tm = quote (forall p. (forall x. p x) ==> wp1 p) in
27-
debug ("before = " ^ term_to_string tm);
32+
by (let tm = `(forall p. (forall x. p x) ==> p 1) in
2833
let tm' = norm_term [simplify] tm in
29-
debug ("after= " ^ term_to_string tm');
30-
if term_eq tm' (`(wp1 (fun (_:int) -> True)))
31-
then ()
32-
else fail "failed")
34+
check_eq "direct_1" tm' (`True))
3335

3436
(* 2 arg direct *)
3537
let direct_2 ()
3638
= assert True
37-
by (let tm = quote (forall p. (forall x y. p x y) ==> wp2 p) in
38-
debug ("before = " ^ term_to_string tm);
39+
by (let tm = `(forall p. (forall x y. p x y) ==> p 12 ()) in
3940
let tm' = norm_term [simplify] tm in
40-
debug ("after= " ^ term_to_string tm');
41-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
42-
then ()
43-
else fail "failed")
41+
check_eq "direct_2" tm' (`True))
4442

4543
(* 1 arg indirect *)
4644
let indirect_1
4745
= assert True
48-
by (admit();
49-
let tm = quote (forall p. (forall x. p x <==> True) ==> wp1 p) in
50-
debug ("before = " ^ term_to_string tm);
46+
by (let tm = `(forall p. (forall x. p x <==> True) ==> p 1) in
5147
let tm' = norm_term [simplify] tm in
52-
debug ("after= " ^ term_to_string tm');
53-
if term_eq tm' (`(wp1 (fun (_:int) -> True)))
54-
then ()
55-
else fail "failed")
48+
check_eq "indirect_1" tm' (`True))
5649

5750
(* 2 arg indirect *)
5851
let indirect_2 ()
5952
= assert True
6053
by (admit ();
61-
let tm = quote (forall p. (forall x y. p x y <==> True) ==> wp2 p) in
62-
debug ("before = " ^ term_to_string tm);
63-
let tm' = norm_term [simplify] tm in
64-
debug ("after= " ^ term_to_string tm');
65-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
66-
then ()
67-
else fail "failed")
68-
69-
(* 1 arg negated direct *)
70-
let neg_direct_1 ()
71-
= assert True
72-
by (let tm = quote (forall p. (forall x. ~(p x)) ==> wp1 p) in
73-
debug ("before = " ^ term_to_string tm);
74-
let tm' = norm_term [simplify] tm in
75-
debug ("after= " ^ term_to_string tm');
76-
if term_eq tm' (`(wp1 (fun (_:int) -> False)))
77-
then ()
78-
else fail "failed")
79-
80-
(* 2 arg negated direct *)
81-
let neg_direct_2 ()
82-
= assert True
83-
by (let tm = quote (forall p. (forall x y. ~(p x y)) ==> wp2 p) in
84-
debug ("before = " ^ term_to_string tm);
85-
let tm' = norm_term [simplify] tm in
86-
debug ("after= " ^ term_to_string tm');
87-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
88-
then ()
89-
else fail "failed")
90-
91-
(* 1 arg negated indirect *)
92-
let neg_indirect_1 ()
93-
= assert True
94-
by (admit();
95-
let tm = quote (forall p. (forall x. p x <==> False) ==> wp1 p) in
96-
debug ("before = " ^ term_to_string tm);
97-
let tm' = norm_term [simplify] tm in
98-
debug ("after= " ^ term_to_string tm');
99-
if term_eq tm' (`(wp1 (fun (_:int) -> False)))
100-
then ()
101-
else fail "failed")
102-
103-
(* 2 arg negated indirect *)
104-
let neg_indirect_2 ()
105-
= assert True
106-
by (admit ();
107-
let tm = quote (forall p. (forall x y. p x y <==> False) ==> wp2 p) in
108-
debug ("before = " ^ term_to_string tm);
54+
let tm = `(forall p. (forall x y. p x y <==> True) ==> p 12 ()) in
10955
let tm' = norm_term [simplify] tm in
110-
debug ("after= " ^ term_to_string tm');
111-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
112-
then ()
113-
else fail "failed")
56+
check_eq "indirect_2" tm' (`True))
11457

115-
// Bug reported by Jay
116-
[@@expect_failure]
58+
// Bug reported by Jay Bosamiya
59+
[@@expect_failure [19]]
11760
let bug () : Lemma False =
11861
((if true then () else ()); ())

‎tests/error-messages/WPExtensionality.fst.expected

+1-81
Original file line numberDiff line numberDiff line change
@@ -1,90 +1,10 @@
11
>> Got issues: [
2-
* Error 19 at WPExtensionality.fst(118,3-118,34):
2+
* Error 19 at WPExtensionality.fst(61,3-61,34):
33
- Assertion failed
44
- The SMT solver could not prove the query. Use --query_stats for more
55
details.
66
- See also prims.fst(430,90-430,102)
77

88
>>]
9-
* Warning 288 at WPExtensionality.fst(25,2-25,8):
10-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
11-
- Use FStar.Reflection.V2.TermEq.term_eq
12-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
13-
14-
* Warning 288 at WPExtensionality.fst(30,13-30,20):
15-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
16-
- Use FStar.Reflection.V2.TermEq.term_eq
17-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
18-
19-
* Warning 288 at WPExtensionality.fst(36,2-36,8):
20-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
21-
- Use FStar.Reflection.V2.TermEq.term_eq
22-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
23-
24-
* Warning 288 at WPExtensionality.fst(41,13-41,20):
25-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
26-
- Use FStar.Reflection.V2.TermEq.term_eq
27-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
28-
29-
* Warning 288 at WPExtensionality.fst(47,2-47,8):
30-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
31-
- Use FStar.Reflection.V2.TermEq.term_eq
32-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
33-
34-
* Warning 288 at WPExtensionality.fst(53,13-53,20):
35-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
36-
- Use FStar.Reflection.V2.TermEq.term_eq
37-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
38-
39-
* Warning 288 at WPExtensionality.fst(59,2-59,8):
40-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
41-
- Use FStar.Reflection.V2.TermEq.term_eq
42-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
43-
44-
* Warning 288 at WPExtensionality.fst(65,13-65,20):
45-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
46-
- Use FStar.Reflection.V2.TermEq.term_eq
47-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
48-
49-
* Warning 288 at WPExtensionality.fst(71,2-71,8):
50-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
51-
- Use FStar.Reflection.V2.TermEq.term_eq
52-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
53-
54-
* Warning 288 at WPExtensionality.fst(76,13-76,20):
55-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
56-
- Use FStar.Reflection.V2.TermEq.term_eq
57-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
58-
59-
* Warning 288 at WPExtensionality.fst(82,2-82,8):
60-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
61-
- Use FStar.Reflection.V2.TermEq.term_eq
62-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
63-
64-
* Warning 288 at WPExtensionality.fst(87,13-87,20):
65-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
66-
- Use FStar.Reflection.V2.TermEq.term_eq
67-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
68-
69-
* Warning 288 at WPExtensionality.fst(93,2-93,8):
70-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
71-
- Use FStar.Reflection.V2.TermEq.term_eq
72-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
73-
74-
* Warning 288 at WPExtensionality.fst(99,13-99,20):
75-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
76-
- Use FStar.Reflection.V2.TermEq.term_eq
77-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
78-
79-
* Warning 288 at WPExtensionality.fst(105,2-105,8):
80-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
81-
- Use FStar.Reflection.V2.TermEq.term_eq
82-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
83-
84-
* Warning 288 at WPExtensionality.fst(111,13-111,20):
85-
- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
86-
- Use FStar.Reflection.V2.TermEq.term_eq
87-
- See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
88-
899
Verified module: WPExtensionality
9010
All verification conditions discharged successfully

‎tests/micro-benchmarks/WPExtensionality.fst

+16-73
Original file line numberDiff line numberDiff line change
@@ -17,102 +17,45 @@ module WPExtensionality
1717

1818
open FStar.Tactics.V2
1919

20+
let term_eq = FStar.Reflection.V2.TermEq.term_eq
21+
2022
assume val wp1 : (int -> Type0) -> Type0
2123
assume val wp2 : (int -> unit -> Type0) -> Type0
2224

25+
let check_eq (s:string) (t1 t2 : term) : Tac unit =
26+
if term_eq t1 t2 then () else
27+
fail (Printf.sprintf "Test %s failed\nt1 = %s\nt2 = %s" s (term_to_string t1) (term_to_string t2))
28+
2329
(* 1 arg direct *)
2430
let direct_1 ()
2531
= assert True
26-
by (let tm = quote (forall p. (forall x. p x) ==> wp1 p) in
27-
debug ("before = " ^ term_to_string tm);
32+
by (let tm = `(forall p. (forall x. p x) ==> p 1) in
2833
let tm' = norm_term [simplify] tm in
29-
debug ("after= " ^ term_to_string tm');
30-
if term_eq tm' (`(wp1 (fun (_:int) -> True)))
31-
then ()
32-
else fail "failed")
34+
check_eq "direct_1" tm' (`True))
3335

3436
(* 2 arg direct *)
3537
let direct_2 ()
3638
= assert True
37-
by (let tm = quote (forall p. (forall x y. p x y) ==> wp2 p) in
38-
debug ("before = " ^ term_to_string tm);
39+
by (let tm = `(forall p. (forall x y. p x y) ==> p 12 ()) in
3940
let tm' = norm_term [simplify] tm in
40-
debug ("after= " ^ term_to_string tm');
41-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
42-
then ()
43-
else fail "failed")
41+
check_eq "direct_2" tm' (`True))
4442

4543
(* 1 arg indirect *)
4644
let indirect_1
4745
= assert True
48-
by (admit();
49-
let tm = quote (forall p. (forall x. p x <==> True) ==> wp1 p) in
50-
debug ("before = " ^ term_to_string tm);
46+
by (let tm = `(forall p. (forall x. p x <==> True) ==> p 1) in
5147
let tm' = norm_term [simplify] tm in
52-
debug ("after= " ^ term_to_string tm');
53-
if term_eq tm' (`(wp1 (fun (_:int) -> True)))
54-
then ()
55-
else fail "failed")
48+
check_eq "indirect_1" tm' (`True))
5649

5750
(* 2 arg indirect *)
5851
let indirect_2 ()
5952
= assert True
6053
by (admit ();
61-
let tm = quote (forall p. (forall x y. p x y <==> True) ==> wp2 p) in
62-
debug ("before = " ^ term_to_string tm);
63-
let tm' = norm_term [simplify] tm in
64-
debug ("after= " ^ term_to_string tm');
65-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
66-
then ()
67-
else fail "failed")
68-
69-
(* 1 arg negated direct *)
70-
let neg_direct_1 ()
71-
= assert True
72-
by (let tm = quote (forall p. (forall x. ~(p x)) ==> wp1 p) in
73-
debug ("before = " ^ term_to_string tm);
74-
let tm' = norm_term [simplify] tm in
75-
debug ("after= " ^ term_to_string tm');
76-
if term_eq tm' (`(wp1 (fun (_:int) -> False)))
77-
then ()
78-
else fail "failed")
79-
80-
(* 2 arg negated direct *)
81-
let neg_direct_2 ()
82-
= assert True
83-
by (let tm = quote (forall p. (forall x y. ~(p x y)) ==> wp2 p) in
84-
debug ("before = " ^ term_to_string tm);
85-
let tm' = norm_term [simplify] tm in
86-
debug ("after= " ^ term_to_string tm');
87-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
88-
then ()
89-
else fail "failed")
90-
91-
(* 1 arg negated indirect *)
92-
let neg_indirect_1 ()
93-
= assert True
94-
by (admit();
95-
let tm = quote (forall p. (forall x. p x <==> False) ==> wp1 p) in
96-
debug ("before = " ^ term_to_string tm);
97-
let tm' = norm_term [simplify] tm in
98-
debug ("after= " ^ term_to_string tm');
99-
if term_eq tm' (`(wp1 (fun (_:int) -> False)))
100-
then ()
101-
else fail "failed")
102-
103-
(* 2 arg negated indirect *)
104-
let neg_indirect_2 ()
105-
= assert True
106-
by (admit ();
107-
let tm = quote (forall p. (forall x y. p x y <==> False) ==> wp2 p) in
108-
debug ("before = " ^ term_to_string tm);
54+
let tm = `(forall p. (forall x y. p x y <==> True) ==> p 12 ()) in
10955
let tm' = norm_term [simplify] tm in
110-
debug ("after= " ^ term_to_string tm');
111-
if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
112-
then ()
113-
else fail "failed")
56+
check_eq "indirect_2" tm' (`True))
11457

115-
// Bug reported by Jay
116-
[@@expect_failure]
58+
// Bug reported by Jay Bosamiya
59+
[@@expect_failure [19]]
11760
let bug () : Lemma False =
11861
((if true then () else ()); ())

0 commit comments

Comments
 (0)