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.

Sign up for GitHub

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

Add basic prove_refinement tactic #1849

Merged
merged 16 commits into from
Apr 18, 2023
Merged

Add basic prove_refinement tactic #1849

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
446dffc
Start of something cool
Mar 2, 2023
ced11d7
add refinesS_eq, fix errors in Prelude.sawcore
m-yac Mar 3, 2023
55dfa7b
Move proveRefinement to builtins
Mar 8, 2023
4a6cffc
refactor to eliminate env and timeout params
Mar 8, 2023
44f23eb
Wire up prove_refinement in the interpreter
Mar 8, 2023
79004cf
Merge remote-tracking branch 'origin/master' into mrs-solver
Mar 8, 2023
d978cca
Debug info
Mar 12, 2023
658bacb
Start of refinesS_fun
Mar 14, 2023
20210d5
add args to askMRSolver, get first prove_refinemen tactic example wor…
m-yac Mar 28, 2023
1830a2c
add prove_refinement tactic tests in mr_solver_unit_tests.saw
m-yac Mar 28, 2023
368ace7
add docs, remove unused EqDep
m-yac Mar 28, 2023
6d81c44
move test_funs out of Prelude, add doc to MrSolverEvidence, some reverts
m-yac Mar 29, 2023
c0f364c
rename prove_refinement tactic to mrsolver
m-yac Mar 30, 2023
e99d03d
add docs to FunStackE-related defs in Prelude.sawcore
m-yac Mar 30, 2023
b25fb57
get List1#rec to translate to list_rect in Coq
m-yac Apr 10, 2023
2403b1d
Merge remote-tracking branch 'origin/master' into mrs-solver
m-yac Apr 13, 2023
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
67 changes: 67 additions & 0 deletions examples/mr_solver/mr_solver_test_funs.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
module test_funs where

import Prelude;

test_fun0 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
test_fun0 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0);

test_fun1 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
test_fun1 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1);

test_fun2 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
test_fun2 x = retS VoidEv emptyFunStack (Vec 64 Bool) x;

-- If x == 0 then x else 0; should be equal to 0
test_fun3 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
test_fun3 x =
ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
(retS VoidEv emptyFunStack (Vec 64 Bool) x)
(retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0));

{-
-- let rec f x = 0 in f x
test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun4 x =
letRecM1
(Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (y:Vec 64 Bool) ->
returnM (Vec 64 Bool) (bvNat 64 0))
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) ->
f x);

-- Alternate version of test_fun4 that uses letRecM directly
test_fun4_alt : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun4_alt x =
letRecM
(LRT_Cons (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool))
LRT_Nil)
(Vec 64 Bool)
(\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
((\ (y:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)), ()))
(\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) -> f x);

-- let rec f = f in f x
test_fun5 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun5 x =
letRecM1
(Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f)
(\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f x);

-- let rec f = g and g = f in f x
test_fun6 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun6 x =
letRecM
(LRT_Cons
(LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
(LRT_Cons
(LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
LRT_Nil))
(Vec 64 Bool)
(\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
(f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
(f2, (f1, ())))
(\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
(f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
f1 x);
-}
87 changes: 71 additions & 16 deletions examples/mr_solver/mr_solver_unit_tests.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
enable_experimental;

load_sawcore_from_file "mr_solver_test_funs.sawcore";

let eq_bool b1 b2 =
if b1 then
if b2 then true else false
Expand All @@ -15,56 +17,102 @@ let run_test name test expected =
do { print "Test failed\n"; exit 1; }; };

// The constant 0 function const0 x = 0
const0 <- parse_core
"\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)";
let ret0_core = "retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)";
let const0_core = str_concat "\\ (_:Vec 64 Bool) -> " ret0_core;
const0 <- parse_core const0_core;

// The constant 1 function const1 x = 1
const1 <- parse_core
"\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)";
let const1_core = "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)";
const1 <- parse_core const1_core;

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

/*
// The function test_fun0 from the prelude = const0
test_fun0 <- parse_core "test_fun0";
// (using mrsolver tactic)
let const0_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", const0_core, ") x) ", "((", const0_core, ") x)"];
prove_extcore mrsolver (parse_core const0_refines);

// The function test_fun0 = const0
test_fun0 <- parse_core_mod "test_funs" "test_fun0";
run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
// (using mrsolver tactic)
let const0_test_fun0_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", const0_core, ") x) ", "(test_fun0 x)"];
prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun0_refines);

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

// The function test_fun1 from the prelude = const1
test_fun1 <- parse_core "test_fun1";
// (using mrsolver tactic - fails as expected)
// let const0_const1_refines =
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
// "((", const0_core, ") x) ", "((", const1_core, ") x)"];
// prove_extcore mrsolver (parse_core const0_const1_refines);

// The function test_fun1 = const1
test_fun1 <- parse_core_mod "test_funs" "test_fun1";
run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true;
run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false;
*/
// (using mrsolver tactic)
let const1_test_fun1_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", const1_core, ") x) ", "(test_fun1 x)"];
prove_extcore mrsolver (parse_core_mod "test_funs" const1_test_fun1_refines);
// (using mrsolver tactic - fails as expected)
// let const0_test_fun1_refines =
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
// "((", const0_core, ") x) ", "(test_fun1 x)"];
// prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun1_refines);

// ifxEq0 x = If x == 0 then x else 0; should be equal to 0
ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \
let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
\ ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) \
\ (bvEq 64 x (bvNat 64 0)) \
\ (retS VoidEv emptyFunStack (Vec 64 Bool) x) \
\ (retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0))";
ifxEq0 <- parse_core ifxEq0_core;

// ifxEq0 <= const0
run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;
// (using mrsolver tactic)
let ifxEq0_const0_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", ifxEq0_core, ") x) ", "((", const0_core, ") x)"];
prove_extcore mrsolver (parse_core ifxEq0_const0_refines);

// not ifxEq0 <= const1
run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
// (using mrsolver tactic - fails as expected)
// let ifxEq0_const1_refines =
// str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
// "((", ifxEq0_core, ") x) ", "((", const1_core, ") x)"];
// prove_extcore mrsolver (parse_core ifxEq0_const1_refines);

// noErrors1 x = existsS x. retS x
noErrors1 <- parse_core
let noErrors1_core =
"\\ (_:Vec 64 Bool) -> existsS VoidEv emptyFunStack (Vec 64 Bool)";
noErrors1 <- parse_core noErrors1_core;

// const0 <= noErrors
run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;
// (using mrsolver tactic)
let noErrors1_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", noErrors1_core, ") x) ", "((", noErrors1_core, ") x)"];
prove_extcore mrsolver (parse_core noErrors1_refines);

// const1 <= noErrors
run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
// (using mrsolver tactic)
let const1_noErrors1_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", const1_core, ") x) ", "((", noErrors1_core, ") x)"];
prove_extcore mrsolver (parse_core const1_noErrors1_refines);

// noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x)
// Intuitively, this specifies functions that either return a value or loop
noErrorsRec1 <- parse_core
let noErrorsRec1_core =
"fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
\ (\\ (f: fixSFun VoidEv emptyFunStack \
\ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
Expand All @@ -76,13 +124,20 @@ noErrorsRec1 <- parse_core
\ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
\ (Vec 64 Bool)) \
\ (f x))";
noErrorsRec1 <- parse_core noErrorsRec1_core;

// loop x = loop x
loop1 <- parse_core
let loop1_core =
"fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
\ (\\ (f: fixSFun VoidEv emptyFunStack \
\ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
\ (x:Vec 64 Bool) -> f x)";
loop1 <- parse_core loop1_core;

// loop1 <= noErrorsRec1
run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;
// (using mrsolver tactic)
let loop1_noErrorsRec1_refines =
str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
"((", loop1_core, ") x) ", "((", noErrorsRec1_core, ") x)"];
prove_extcore mrsolver (parse_core loop1_noErrorsRec1_refines);
33 changes: 22 additions & 11 deletions saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -553,6 +553,17 @@ sawCorePreludeSpecialTreatmentMap configuration =
, ("FrameTuple", mapsToExpl specMModule "FrameTuple")
, ("callS", mapsToExpl specMModule "CallS")
, ("multiFixS", mapsToExpl specMModule "MultiFixS")
, ("FunStackE_type", mapsToExpl specMModule "FunStackE")
, ("FunStackE_enc", replace (Coq.Lambda [Coq.Binder "E" (Just (Coq.Var "SpecM.EvType"))]
(Coq.App (Coq.ExplVar "SpecM.FunStackE_encodes")
[Coq.App (Coq.Var "SpecM.evTypeType") [Coq.Var "E"],
Coq.App (Coq.Var "SpecM.evRetType") [Coq.Var "E"]])))
, ("SpecPreRel", mapsToExpl specMModule "SpecPreRel")
, ("SpecPostRel", mapsToExpl specMModule "SpecPostRel")
, ("eqPreRel", mapsToExpl specMModule "eqPreRel")
, ("eqPostRel", mapsToExpl specMModule "eqPostRel")
, ("refinesS", mapsToExpl specMModule "spec_refines")
, ("refinesS_eq", mapsToExpl specMModule "spec_refines_eq")
]

-- Dependent pairs
Expand All @@ -566,25 +577,25 @@ sawCorePreludeSpecialTreatmentMap configuration =

-- Lists
++
[ ("List", replace (Coq.ExplVar "Datatypes.list"))
, ("Nil", replace (Coq.ExplVar "Datatypes.nil"))
, ("Cons", replace (Coq.ExplVar "Datatypes.cons"))
, ("List__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
[ ("List", mapsToExpl datatypesModule "list")
, ("Nil", mapsToExpl datatypesModule "nil")
, ("Cons", mapsToExpl datatypesModule "cons")
, ("List__rec", mapsToExpl datatypesModule "list_rect")
]

-- Lists at sort 1
++
[ ("List1", replace (Coq.ExplVar "Datatypes.list"))
, ("Nil1", replace (Coq.ExplVar "Datatypes.nil"))
, ("Cons1", replace (Coq.ExplVar "Datatypes.cons"))
[ ("List1", mapsToExpl datatypesModule "list")
, ("Nil1", mapsToExpl datatypesModule "nil")
, ("Cons1", mapsToExpl datatypesModule "cons")
]

-- Lists at sort 2
++
[ ("List2", replace (Coq.ExplVar "Datatypes.list"))
, ("Nil2", replace (Coq.ExplVar "Datatypes.nil"))
, ("Cons2", replace (Coq.ExplVar "Datatypes.cons"))
, ("List2__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
[ ("List2", mapsToExpl datatypesModule "list")
, ("Nil2", mapsToExpl datatypesModule "nil")
, ("Cons2", mapsToExpl datatypesModule "cons")
, ("List2__rec", mapsToExpl datatypesModule "list_rect")
]

escapeIdent :: String -> String
Expand Down
2 changes: 1 addition & 1 deletion saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,7 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
Recursor (CompiledRecursor d parameters motive _motiveTy eliminators elimOrder) ->
do maybe_d_trans <- translateIdentToIdent (primName d)
rect_var <- case maybe_d_trans of
Just i -> return $ Coq.Var (show i ++ "_rect")
Just i -> return $ Coq.ExplVar (show i ++ "_rect")
Nothing ->
errorTermM ("Recursor for " ++ show d ++
" cannot be translated because the datatype " ++
Expand Down
Loading