From 1ea02371b82a549dfd989e80001078c35871af37 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 13 May 2022 17:39:59 -0700 Subject: [PATCH 1/7] added eta-expanded versions of the Left and Right constructors to the prelude --- saw-core/prelude/Prelude.sawcore | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index f559e19926..95f573818e 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -680,10 +680,19 @@ Either__rec : (s t : sort 0) -> (p : Either s t -> sort 0) -> (e : Either s t) -> p e; Either__rec s t p f1 f2 e = Either#rec s t p f1 f2 e; +-- The eliminator for the Either type either : (a b c : sort 0) -> (a -> c) -> (b -> c) -> Either a b -> c; either a b c f g e = Either__rec a b (\ (p: Either a b) -> c) f g e; +-- Eta-expanded version of the Left constructor +left : (a b : sort 0) -> a -> Either a b; +left a b x = Left a b x; + +-- Eta-expanded version of the Right constructor +right : (a b : sort 0) -> b -> Either a b; +right a b x = Right a b x; + eitherCong0 : (t x y : sort 0) -> Eq (sort 0) x y -> Eq (sort 0) (Either x t) (Either y t); eitherCong0 t x y eq = From 60b6bf5bd400ec0dbbe8ddebd7c436ff8da8d86c Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 13 May 2022 17:40:17 -0700 Subject: [PATCH 2/7] added support to the monadifier for monadifying the unit type --- cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index be8cf2a241..53656dd6f7 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -880,6 +880,9 @@ monadifyTerm' _ (asLocalVar -> Just ix) = ctx | ix >= length ctx -> fail "Monadification failed: vaiable out of scope!" ctx | (_,_,Right mtrm) <- ctx !! ix -> return mtrm _ -> fail "Monadification failed: type variable used in term position!" +monadifyTerm' _ (asTupleValue -> Just []) = + return $ ArgMonTerm $ + fromSemiPureTerm (mkMonType0 unitTypeOpenTerm) unitOpenTerm monadifyTerm' _ (asCtor -> Just (pn, args)) = monadifyApply (ArgMonTerm $ mkCtorArgMonTerm pn) args monadifyTerm' _ (asApplyAll -> (asTypedGlobalDef -> Just glob, args)) = From cf91641c2f01d8455b0976efe937cbcdad9a1058 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 13 May 2022 17:40:48 -0700 Subject: [PATCH 3/7] fixed the monadification of the Left and Right cryptol primitives so they now use the new eta-expanded left and right functions in the saw-core prelude --- heapster-saw/examples/either.saw | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heapster-saw/examples/either.saw b/heapster-saw/examples/either.saw index b711c9a8fb..01a35e6042 100644 --- a/heapster-saw/examples/either.saw +++ b/heapster-saw/examples/either.saw @@ -3,10 +3,10 @@ eith_tp <- parse_core "\\ (a b:sort 0) -> Either a b"; cryptol_add_prim_type "Either" "Either" eith_tp; -left_fun <- parse_core "\\ (a b:sort 0) (x:a) -> Left a b x"; +left_fun <- parse_core "left"; cryptol_add_prim "Either" "Left" left_fun; -right_fun <- parse_core "\\ (a b:sort 0) (x:b) -> Right a b x"; +right_fun <- parse_core "right"; cryptol_add_prim "Either" "Right" right_fun; either_fun <- parse_core "either"; From 534ffda0895d8c8628a8af85d55db070c2055dd9 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 13 May 2022 17:41:29 -0700 Subject: [PATCH 4/7] added MR solver test case for sorted_insert_no_malloc --- heapster-saw/examples/linked_list.cry | 13 +++++++++++++ heapster-saw/examples/linked_list_mr_solver.saw | 10 ++++++++++ 2 files changed, 23 insertions(+) diff --git a/heapster-saw/examples/linked_list.cry b/heapster-saw/examples/linked_list.cry index 85e63ec8c4..f32250d025 100644 --- a/heapster-saw/examples/linked_list.cry +++ b/heapster-saw/examples/linked_list.cry @@ -8,7 +8,20 @@ primitive type List : * -> * primitive foldList : {a} Either () (a, List a) -> List a primitive unfoldList : {a} List a -> Either () (a, List a) +nil : {a} List a +nil = foldList (Left ()) + +cons : {a} a -> List a -> List a +cons x l = foldList (Right (x,l)) + is_elem_spec : [64] -> List [64] -> [64] is_elem_spec x l = either (\ _ -> 0) (\ (y,l') -> if x == y then 1 else is_elem_spec x l') (unfoldList l) + +sorted_insert_spec : [64] -> List [64] -> List [64] +sorted_insert_spec x l = + either (\ _ -> cons x nil) + (\ (y,l') -> if x <= y then cons x (cons y l) + else cons y (sorted_insert_spec x l')) + (unfoldList l) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index 98f1196b02..50b187258d 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -67,3 +67,13 @@ run_test "is_elem |= noErrorsSpec" (mr_solver is_elem is_elem_noErrorsSpec) true */ run_test "is_elem |= is_elem_spec" (mr_solver is_elem {{ is_elem_spec }}) true; + + +monadify_term {{ Right }}; +monadify_term {{ Left }}; +monadify_term {{ nil }}; +monadify_term {{ cons }}; + +sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc"; +run_test "sorted_insert_no_malloc |= sorted_insert_spec" + (mr_solver_debug 3 sorted_insert_no_malloc {{ sorted_insert_spec }}) true; From 488281913325e4b7a367937889763bf95a2a1a20 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 16 May 2022 09:36:28 -0700 Subject: [PATCH 5/7] whoops, fixed a bug in the cryptol spec for sorted_insert_spec --- heapster-saw/examples/linked_list.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/linked_list.cry b/heapster-saw/examples/linked_list.cry index f32250d025..0e40864965 100644 --- a/heapster-saw/examples/linked_list.cry +++ b/heapster-saw/examples/linked_list.cry @@ -22,6 +22,6 @@ is_elem_spec x l = sorted_insert_spec : [64] -> List [64] -> List [64] sorted_insert_spec x l = either (\ _ -> cons x nil) - (\ (y,l') -> if x <= y then cons x (cons y l) + (\ (y,l') -> if x <= y then cons x (cons y l') else cons y (sorted_insert_spec x l')) (unfoldList l) From 13a1a8636ef1e47627964aa72c317bf3664f9d61 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 16 May 2022 13:02:23 -0700 Subject: [PATCH 6/7] fixed a bug in sorted_insert_spec: need to use signed instead of unsigned comparison --- heapster-saw/examples/linked_list.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/linked_list.cry b/heapster-saw/examples/linked_list.cry index 0e40864965..113c3f2571 100644 --- a/heapster-saw/examples/linked_list.cry +++ b/heapster-saw/examples/linked_list.cry @@ -22,6 +22,6 @@ is_elem_spec x l = sorted_insert_spec : [64] -> List [64] -> List [64] sorted_insert_spec x l = either (\ _ -> cons x nil) - (\ (y,l') -> if x <= y then cons x (cons y l') + (\ (y,l') -> if x <=$ y then cons x (cons y l') else cons y (sorted_insert_spec x l')) (unfoldList l) From 477a051d6da94ddba3a847179051e8ac8d80c34f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 16 May 2022 13:15:50 -0700 Subject: [PATCH 7/7] removed the debug output from linked_list_mr_solver.saw --- heapster-saw/examples/linked_list_mr_solver.saw | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index 50b187258d..2bf75117d9 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -76,4 +76,4 @@ monadify_term {{ cons }}; sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc"; run_test "sorted_insert_no_malloc |= sorted_insert_spec" - (mr_solver_debug 3 sorted_insert_no_malloc {{ sorted_insert_spec }}) true; + (mr_solver sorted_insert_no_malloc {{ sorted_insert_spec }}) true;