From 3e661696b555f4c4339d0080c904e925b99b298e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 12 Feb 2024 14:53:33 -0800 Subject: [PATCH] Update WP optimization test --- tests/error-messages/WPExtensionality.fst | 89 ++++--------------- .../WPExtensionality.fst.expected | 82 +---------------- tests/micro-benchmarks/WPExtensionality.fst | 89 ++++--------------- 3 files changed, 33 insertions(+), 227 deletions(-) diff --git a/tests/error-messages/WPExtensionality.fst b/tests/error-messages/WPExtensionality.fst index bf52e540c19..2dd558f66db 100644 --- 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 index bfba5ef6c1c..7619e515aa9 100644 --- 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 index bf52e540c19..2dd558f66db 100644 --- 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 ()); ())