Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve MRSolver interface #1675

Merged
merged 7 commits into from
May 24, 2022
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
add mr_solver_test which adds no assumps, rn mr_solver_check to _query
m-yac committed May 23, 2022

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 25633e3b0e44aaa79b1e98dacc37cebf803a61e5
20 changes: 10 additions & 10 deletions examples/mr_solver/mr_solver_unit_tests.saw
Original file line number Diff line number Diff line change
@@ -21,19 +21,19 @@ const0 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)";
const1 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 1)";

// const0 <= const0
run_test "const0 |= const0" (mr_solver_check const0 const0) true;
run_test "const0 |= const0" (mr_solver_query const0 const0) true;

// The function test_fun0 from the prelude = const0
test_fun0 <- parse_core "test_fun0";
run_test "const0 |= test_fun0" (mr_solver_check const0 test_fun0) true;
run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;

// not const0 <= const1
run_test "const0 |= const1" (mr_solver_check const0 const1) false;
run_test "const0 |= const1" (mr_solver_query const0 const1) false;

// The function test_fun1 from the prelude = const1
test_fun1 <- parse_core "test_fun1";
run_test "const1 |= test_fun1" (mr_solver_check const1 test_fun1) true;
run_test "const0 |= test_fun1" (mr_solver_check const0 test_fun1) false;
run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true;
run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false;

// ifxEq0 x = If x == 0 then x else 0; should be equal to 0
ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \
@@ -42,21 +42,21 @@ ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \
\ (returnM (Vec 64 Bool) (bvNat 64 0))";

// ifxEq0 <= const0
run_test "ifxEq0 |= const0" (mr_solver_check ifxEq0 const0) true;
run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;

// not ifxEq0 <= const1
run_test "ifxEq0 |= const1" (mr_solver_check ifxEq0 const1) false;
run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;

// noErrors1 x = exists x. returnM x
noErrors1 <- parse_core "\\ (x:Vec 64 Bool) -> \
\ existsM (Vec 64 Bool) (Vec 64 Bool) \
\ (\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool) x)";

// const0 <= noErrors
run_test "noErrors1 |= noErrors1" (mr_solver_check noErrors1 noErrors1) true;
run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;

// const1 <= noErrors
run_test "const1 |= noErrors1" (mr_solver_check const1 noErrors1) true;
run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;

// noErrorsRec1 x = orM (existsM x. returnM x) (noErrorsRec1 x)
// Intuitively, this specifies functions that either return a value or loop
@@ -74,4 +74,4 @@ loop1 <- parse_core
\ (\\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (x:Vec 64 Bool) -> f x)";

// loop1 <= noErrorsRec1
run_test "loop1 |= noErrorsRec1" (mr_solver_check loop1 noErrorsRec1) true;
run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;
2 changes: 1 addition & 1 deletion heapster-saw/examples/arrays_mr_solver.saw
Original file line number Diff line number Diff line change
@@ -2,7 +2,7 @@ include "arrays.saw";

// Test that contains0 |= contains0
contains0 <- parse_core_mod "arrays" "contains0";
// mr_solver_prove contains0 contains0;
mr_solver_test contains0 contains0;

noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
mr_solver_prove contains0 noErrorsContains0;
11 changes: 4 additions & 7 deletions heapster-saw/examples/linked_list_mr_solver.saw
Original file line number Diff line number Diff line change
@@ -26,15 +26,13 @@ heapster_typecheck_fun env "is_head"
"(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
\ arg0:true, arg1:true, ret:int64<>";

/*
is_head <- parse_core_mod "linked_list" "is_head";
mr_solver_prove is_head is_head;
*/
mr_solver_test is_head is_head;

is_elem <- parse_core_mod "linked_list" "is_elem";
// mr_solver_prove is_elem is_elem;

/*
mr_solver_test is_elem is_elem;

is_elem_noErrorsSpec <- parse_core
"\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \
\ fixM (Vec 64 Bool * List (Vec 64 Bool)) \
@@ -44,8 +42,7 @@ is_elem_noErrorsSpec <- parse_core
\ orM (Vec 64 Bool) \
\ (existsM (Vec 64 Bool) (Vec 64 Bool) (returnM (Vec 64 Bool))) \
\ (rec x)) (x, y)";
mr_solver_prove is_elem is_elem_noErrorsSpec;
*/
mr_solver_test is_elem is_elem_noErrorsSpec;

mr_solver_prove is_elem {{ is_elem_spec }};

8 changes: 4 additions & 4 deletions heapster-saw/examples/sha512_mr_solver.saw
Original file line number Diff line number Diff line change
@@ -86,10 +86,10 @@ processBlock <- parse_core_mod "SHA512" "processBlock";
processBlocks <- parse_core_mod "SHA512" "processBlocks";

// Test that every function refines itself
// mr_solver_prove processBlocks processBlocks;
// mr_solver_prove processBlock processBlock;
// mr_solver_prove round_16_80 round_16_80;
// mr_solver_prove round_00_15 round_00_15;
// mr_solver_test processBlocks processBlocks;
// mr_solver_test processBlock processBlock;
// mr_solver_test round_16_80 round_16_80;
// mr_solver_test round_00_15 round_00_15;

import "sha512.cry";
// FIXME: Why aren't we monadifying these automatically when they're used?
52 changes: 27 additions & 25 deletions src/SAWScript/Builtins.hs
Original file line number Diff line number Diff line change
@@ -38,7 +38,6 @@ import Data.IORef
import Data.List (isPrefixOf, isInfixOf)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.Either (isRight)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
@@ -1634,24 +1633,26 @@ askMRSolver printStr sc t1 t2 =
ppTmHead _ = "..."

-- | Run Mr Solver to prove that the first term refines the second, adding
-- any relevant 'Prover.FunAssump's to the 'Prover.MREnv' if this can be done,
-- or printing an error message and exiting if it cannot.
mrSolverProve :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel ()
mrSolverProve sc t1 t2 =
-- any relevant 'Prover.FunAssump's to the 'Prover.MREnv' if the first argument
-- is true and this can be done, or printing an error message and exiting if it
-- cannot.
mrSolverProve :: Bool -> SharedContext -> TypedTerm -> TypedTerm -> TopLevel ()
mrSolverProve addToEnv sc t1 t2 =
do dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get
(diff, res) <- askMRSolver (Just "Proving") sc t1 t2
let printStr = if addToEnv then "Proving" else "Testing"
(diff, res) <- askMRSolver (Just printStr) sc t1 t2
case res of
Left err | dlvl == 0 ->
io (putStrLn $ Prover.showMRFailure err) >>
printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >>
io (Exit.exitWith $ Exit.ExitFailure 1)
Left err | otherwise ->
Left err ->
-- we ignore the MRFailure context here since it will have already
-- been printed by the debug trace
io (putStrLn $ Prover.showMRFailureNoCtx err) >>
printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >>
io (Exit.exitWith $ Exit.ExitFailure 1)
Right (Just (fnm, fassump)) ->
Right (Just (fnm, fassump)) | addToEnv ->
let assump_str = case Prover.fassumpRHS fassump of
Prover.OpaqueFunAssump _ _ -> "an opaque"
Prover.RewriteFunAssump _ -> "a rewrite" in
@@ -1660,27 +1661,28 @@ mrSolverProve sc t1 t2 =
(show diff) (assump_str :: String)) >>
modify (\rw -> rw { rwMRSolverEnv =
Prover.mrEnvAddFunAssump fnm fassump (rwMRSolverEnv rw) })
Right Nothing ->
_ ->
printOutLnTop Info $ printf "[MRSolver] Success in %s" (show diff)

-- | Run Mr Solver to prove that the first term refines the second, returning
-- true iff this can be done. This function will not modify the 'Prover.MREnv'.
mrSolverCheck :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel Bool
mrSolverCheck sc t1 t2 =
Prover.mreDebugLevel <$> rwMRSolverEnv <$> get >>= \case
0 -> isRight <$> snd <$> askMRSolver Nothing sc t1 t2
_ -> do
(diff, res) <- askMRSolver (Just "Checking") sc t1 t2
case res of
Left err ->
-- we ignore the MRFailure context here since it will have already
-- been printed by the debug trace
io (putStrLn $ Prover.showMRFailureNoCtx err) >>
printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >>
return False
Right _ ->
printOutLnTop Info (printf "[MRSolver] Success in %s" (show diff)) >>
return True
mrSolverQuery :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel Bool
mrSolverQuery sc t1 t2 =
do dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get
(diff, res) <- askMRSolver (Just "Querying") sc t1 t2
case res of
Left _ | dlvl == 0 ->
printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >>
return False
Left err ->
-- we ignore the MRFailure context here since it will have already
-- been printed by the debug trace
io (putStrLn $ Prover.showMRFailureNoCtx err) >>
printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >>
return False
Right _ ->
printOutLnTop Info (printf "[MRSolver] Success in %s" (show diff)) >>
return True

-- | Set the debug level of the 'Prover.MREnv'
mrSolverSetDebug :: Int -> TopLevel ()
25 changes: 18 additions & 7 deletions src/SAWScript/Interpreter.hs
Original file line number Diff line number Diff line change
@@ -3191,21 +3191,32 @@ primitives = Map.fromList
---------------------------------------------------------------------

, prim "mr_solver_prove" "Term -> Term -> TopLevel ()"
(scVal mrSolverProve)
(scVal (mrSolverProve True))
Experimental
[ "Call the monadic-recursive solver (that's MR. Solver to you)"
, " to prove that one monadic term refines another. If this can"
, " be done, this refinement will be used in future calls to"
, " Mr. Solver, and if it cannot, the script will exit." ]
, " Mr. Solver, and if it cannot, the script will exit. See also:"
, " mr_solver_test, mr_solver_query." ]

, prim "mr_solver_check" "Term -> Term -> TopLevel Bool"
(scVal mrSolverCheck)
, prim "mr_solver_test" "Term -> Term -> TopLevel ()"
(scVal (mrSolverProve False))
Experimental
[ "Call the monadic-recursive solver (that's MR. Solver to you)"
, " to prove that one monadic term refines another. If this cannot"
, " be done, the script will exit. See also: mr_solver_prove,"
, " mr_solver_query - unlike the former, this refinement will not"
, " be used in future calls to Mr. Solver." ]

, prim "mr_solver_query" "Term -> Term -> TopLevel Bool"
(scVal mrSolverQuery)
Experimental
[ "Call the monadic-recursive solver (that's MR. Solver to you)"
, " to prove that one monadic term refines another, returning"
, " true iff this can be done. Unlike mr_solver_prove, this"
, " refinement will not be considered in future calls to"
, " Mr. Solver." ]
, " true iff this can be done. See also: mr_solver_prove,"
, " mr_solver_test - unlike the former, this refinement will not"
, " be considered in future calls to Mr. Solver, and unlike both,"
, " this command will never fail." ]

, prim "mr_solver_set_debug_level" "Int -> TopLevel ()"
(pureVal mrSolverSetDebug)