Update WP optimization test

FStarLang · Feb 12, 2024 · 3e66169 · 3e66169
1 parent 6156792
commit 3e66169
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 227 deletions.
diff --git a/tests/error-messages/WPExtensionality.fst b/tests/error-messages/WPExtensionality.fst
@@ -17,102 +17,45 @@ module WPExtensionality
 
 open FStar.Tactics.V2
 
+let term_eq = FStar.Reflection.V2.TermEq.term_eq
+
 assume val wp1 : (int -> Type0) -> Type0
 assume val wp2 : (int -> unit -> Type0) -> Type0
 
+let check_eq (s:string) (t1 t2 : term) : Tac unit =
+  if term_eq t1 t2 then () else
+    fail (Printf.sprintf "Test %s failed\nt1 = %s\nt2 = %s" s (term_to_string t1) (term_to_string t2))
+
 (* 1 arg direct *)
 let direct_1 ()
 = assert True
-      by (let tm = quote (forall p. (forall x. p x) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x. p x) ==> p 1) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "direct_1" tm' (`True))
 
 (* 2 arg direct *)
 let direct_2 ()
 = assert True
-      by (let tm = quote (forall p. (forall x y. p x y) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x y. p x y) ==> p 12 ()) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "direct_2" tm' (`True))
 
 (* 1 arg indirect *)
 let indirect_1
 = assert True
-      by (admit();
-          let tm = quote (forall p. (forall x. p x <==> True) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x. p x <==> True) ==> p 1) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "indirect_1" tm' (`True))
 
 (* 2 arg indirect *)
 let indirect_2 ()
 = assert True
       by (admit ();
-          let tm = quote (forall p. (forall x y. p x y <==> True) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
-          then ()
-          else fail "failed")
-
-(* 1 arg negated direct *)
-let neg_direct_1 ()
-= assert True
-      by (let tm = quote (forall p. (forall x. ~(p x)) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> False)))
-          then ()
-          else fail "failed")
-
-(* 2 arg negated direct *)
-let neg_direct_2 ()
-= assert True
-      by (let tm = quote (forall p. (forall x y. ~(p x y)) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
-          then ()
-          else fail "failed")
-
-(* 1 arg negated indirect *)
-let neg_indirect_1 ()
-= assert True
-      by (admit();
-          let tm = quote (forall p. (forall x. p x <==> False) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> False)))
-          then ()
-          else fail "failed")
-
-(* 2 arg negated indirect *)
-let neg_indirect_2 ()
-= assert True
-      by (admit ();
-          let tm = quote (forall p. (forall x y. p x y <==> False) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
+          let tm = `(forall p. (forall x y. p x y <==> True) ==> p 12 ()) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
-          then ()
-          else fail "failed")
+          check_eq "indirect_2" tm' (`True))
 
-// Bug reported by Jay
-[@@expect_failure]
+// Bug reported by Jay Bosamiya
+[@@expect_failure [19]]
 let bug () : Lemma False =
    ((if true then () else ()); ())
diff --git a/tests/error-messages/WPExtensionality.fst.expected b/tests/error-messages/WPExtensionality.fst.expected
@@ -1,90 +1,10 @@
 >> Got issues: [
-* Error 19 at WPExtensionality.fst(118,3-118,34):
+* Error 19 at WPExtensionality.fst(61,3-61,34):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
   - See also prims.fst(430,90-430,102)
 
 >>]
-* Warning 288 at WPExtensionality.fst(25,2-25,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(30,13-30,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(36,2-36,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(41,13-41,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(47,2-47,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(53,13-53,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(59,2-59,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(65,13-65,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(71,2-71,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(76,13-76,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(82,2-82,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(87,13-87,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(93,2-93,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(99,13-99,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(105,2-105,8):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
-* Warning 288 at WPExtensionality.fst(111,13-111,20):
-  - FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated
-  - Use FStar.Reflection.V2.TermEq.term_eq
-  - See also FStar.Stubs.Reflection.V2.Builtins.fsti(150,0-150,48)
-
 Verified module: WPExtensionality
 All verification conditions discharged successfully
diff --git a/tests/micro-benchmarks/WPExtensionality.fst b/tests/micro-benchmarks/WPExtensionality.fst
@@ -17,102 +17,45 @@ module WPExtensionality
 
 open FStar.Tactics.V2
 
+let term_eq = FStar.Reflection.V2.TermEq.term_eq
+
 assume val wp1 : (int -> Type0) -> Type0
 assume val wp2 : (int -> unit -> Type0) -> Type0
 
+let check_eq (s:string) (t1 t2 : term) : Tac unit =
+  if term_eq t1 t2 then () else
+    fail (Printf.sprintf "Test %s failed\nt1 = %s\nt2 = %s" s (term_to_string t1) (term_to_string t2))
+
 (* 1 arg direct *)
 let direct_1 ()
 = assert True
-      by (let tm = quote (forall p. (forall x. p x) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x. p x) ==> p 1) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "direct_1" tm' (`True))
 
 (* 2 arg direct *)
 let direct_2 ()
 = assert True
-      by (let tm = quote (forall p. (forall x y. p x y) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x y. p x y) ==> p 12 ()) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "direct_2" tm' (`True))
 
 (* 1 arg indirect *)
 let indirect_1
 = assert True
-      by (admit();
-          let tm = quote (forall p. (forall x. p x <==> True) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
+      by (let tm = `(forall p. (forall x. p x <==> True) ==> p 1) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> True)))
-          then ()
-          else fail "failed")
+          check_eq "indirect_1" tm' (`True))
 
 (* 2 arg indirect *)
 let indirect_2 ()
 = assert True
       by (admit ();
-          let tm = quote (forall p. (forall x y. p x y <==> True) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> True)))
-          then ()
-          else fail "failed")
-
-(* 1 arg negated direct *)
-let neg_direct_1 ()
-= assert True
-      by (let tm = quote (forall p. (forall x. ~(p x)) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> False)))
-          then ()
-          else fail "failed")
-
-(* 2 arg negated direct *)
-let neg_direct_2 ()
-= assert True
-      by (let tm = quote (forall p. (forall x y. ~(p x y)) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
-          then ()
-          else fail "failed")
-
-(* 1 arg negated indirect *)
-let neg_indirect_1 ()
-= assert True
-      by (admit();
-          let tm = quote (forall p. (forall x. p x <==> False) ==> wp1 p) in
-          debug ("before = " ^ term_to_string tm);
-          let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp1 (fun (_:int) -> False)))
-          then ()
-          else fail "failed")
-
-(* 2 arg negated indirect *)
-let neg_indirect_2 ()
-= assert True
-      by (admit ();
-          let tm = quote (forall p. (forall x y. p x y <==> False) ==> wp2 p) in
-          debug ("before = " ^ term_to_string tm);
+          let tm = `(forall p. (forall x y. p x y <==> True) ==> p 12 ()) in
           let tm' = norm_term [simplify] tm in
-          debug ("after= " ^ term_to_string tm');
-          if term_eq tm' (`(wp2 (fun (_:int) (_:unit) -> False)))
-          then ()
-          else fail "failed")
+          check_eq "indirect_2" tm' (`True))
 
-// Bug reported by Jay
-[@@expect_failure]
+// Bug reported by Jay Bosamiya
+[@@expect_failure [19]]
 let bug () : Lemma False =
    ((if true then () else ()); ())