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 11 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
73 changes: 63 additions & 10 deletions examples/mr_solver/mr_solver_unit_tests.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,56 +15,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;
// (using prove_refinement 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 prove_refinement (parse_core const0_refines);

/*
// The function test_fun0 from the prelude = const0
test_fun0 <- parse_core "test_fun0";
run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
// (using prove_refinement 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 prove_refinement (parse_core const0_test_fun0_refines);

// not const0 <= const1
run_test "const0 |= const1" (mr_solver_query const0 const1) false;
// (using prove_refinement 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 prove_refinement (parse_core const0_const1_refines);

// The function test_fun1 from the prelude = const1
test_fun1 <- parse_core "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 prove_refinement 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 prove_refinement (parse_core const1_test_fun1_refines);
// (using prove_refinement 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 prove_refinement (parse_core 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 prove_refinement 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 prove_refinement (parse_core ifxEq0_const0_refines);

// not ifxEq0 <= const1
run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
// (using prove_refinement 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 prove_refinement (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 prove_refinement 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 prove_refinement (parse_core noErrors1_refines);

// const1 <= noErrors
run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
// (using prove_refinement 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 prove_refinement (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 +122,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 prove_refinement 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 prove_refinement (parse_core loop1_noErrorsRec1_refines);
211 changes: 146 additions & 65 deletions saw-core/prelude/Prelude.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2785,71 +2785,6 @@ multiArgFixM lrt F =
(multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(1);


-- Test computations
test_fun0 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun0 _ = returnM (Vec 64 Bool) (bvNat 64 0);

test_fun1 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun1 _ = returnM (Vec 64 Bool) (bvNat 64 1);

test_fun2 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun2 x = returnM (Vec 64 Bool) x;

-- If x == 0 then x else 0; should be equal to 0
test_fun3 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun3 x =
ite (CompM (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
(returnM (Vec 64 Bool) x)
(returnM (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 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun4 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);


--------------------------------------------------------------------------------
-- ITree Specification monad

Expand Down Expand Up @@ -2989,10 +2924,88 @@ emptyFunStack = Nil1 (List1 LetRecType);
pushFunStack : List1 LetRecType -> FunStack -> FunStack;
pushFunStack frame stack = Cons1 (List1 LetRecType) frame stack;

-- The type of FunStackE
m-yac marked this conversation as resolved.
Show resolved Hide resolved
FunStackE_type : (E:EvType) -> FunStack -> sort 0;
FunStackE_type E stack =
List1#rec
(List1 LetRecType)
(\ (_:FunStack) -> sort 0)
(Either String (evTypeType E))
(\ (frame:List1 LetRecType) -> \ (_:FunStack) -> \ (E':sort 0) ->
Either (FrameCall frame) E')
stack;

-- The encoding of FunStackE
FunStackE_enc : (E:EvType) -> (stack:FunStack) -> FunStackE_type E stack -> sort 0;
FunStackE_enc E stack =
List1#rec
(List1 LetRecType)
(\ (stack:FunStack) -> FunStackE_type E stack -> sort 0)
(\ (e:Either String (evTypeType E)) ->
Either#rec String (evTypeType E) (\ (_:Either String (evTypeType E)) -> sort 0)
(\ (_:String) -> Void) (evRetType E) e)
(\ (frame:List1 LetRecType) -> \ (stack:FunStack) -> \ (rec:FunStackE_type E stack -> sort 0) ->
\ (e:Either (FrameCall frame) (FunStackE_type E stack)) ->
Either#rec (FrameCall frame) (FunStackE_type E stack) (\ (_:Either (FrameCall frame) (FunStackE_type E stack)) -> sort 0)
(FrameCallRet frame) rec e)
stack;

-- The event type corresponding to a FunStack
FunStackE : (E:EvType) -> FunStack -> EvType;
FunStackE E stack = Build_EvType (FunStackE_type E stack) (FunStackE_enc E stack);


-- The monad for specifications (FIXME: document this!)
primitive SpecM : (E:EvType) -> FunStack -> sort 0 -> sort 0;


-- The type of the preconditions needed for refinesS
m-yac marked this conversation as resolved.
Show resolved Hide resolved
SpecPreRel : (E1:EvType) -> (E2:EvType) ->
(stack1:FunStack) -> (stack2:FunStack) -> sort 0;
SpecPreRel E1 E2 stack1 stack2 =
FunStackE_type E1 stack1 -> FunStackE_type E2 stack2 -> Prop;

-- The type of the postconditions needed for refinesS
m-yac marked this conversation as resolved.
Show resolved Hide resolved
SpecPostRel : (E1:EvType) -> (E2:EvType) ->
(stack1:FunStack) -> (stack2:FunStack) -> sort 0;
SpecPostRel E1 E2 stack1 stack2 =
(e1:FunStackE_type E1 stack1) -> (e2:FunStackE_type E2 stack2) ->
FunStackE_enc E1 stack1 e1 -> FunStackE_enc E2 stack2 e2 -> Prop;

-- The type of the return relations needed for refinesS
SpecRetRel : (R1:sort 0) -> (R1:sort 0) -> sort 0;
SpecRetRel R1 R2 = R1 -> R2 -> Prop;

-- The precondition requiring events on both sides to be equal
eqPreRel : (E:EvType) -> (stack:FunStack) -> SpecPreRel E E stack stack;
eqPreRel E stack e1 e2 =
Eq (FunStackE_type E stack) e1 e2;

-- The postcondition requiring return values on both sides to be equal
eqPostRel : (E:EvType) -> (stack:FunStack) -> SpecPostRel E E stack stack;
eqPostRel E stack e1 e2 a1 a2 =
EqDep (FunStackE_type E stack) (FunStackE_enc E stack) e1 a1 e2 a2;

-- The return relation requiring the returned values on both sides to be equal
eqRR : (R:sort 0) -> SpecRetRel R R;
eqRR R r1 r2 = Eq R r1 r2;

-- Refinement of SpecM computations
primitive refinesS : (E1:EvType) -> (E2:EvType) ->
(stack1:FunStack) -> (stack2:FunStack) ->
(RPre:SpecPreRel E1 E2 stack1 stack2) ->
(RPost:SpecPostRel E1 E2 stack1 stack2) ->
(R1:sort 0) -> (R2:sort 0) -> (RR:SpecRetRel R1 R2) ->
SpecM E1 stack1 R1 -> SpecM E2 stack2 R2 -> Prop;

-- Homogeneous refinement of SpecM computations - i.e. refinesS with eqPreRel for
-- the precondition, eqPostRel for the postcondition, and eqRR for the return relation
refinesS_eq : (E:EvType) -> (stack:FunStack) -> (R:sort 0) ->
SpecM E stack R -> SpecM E stack R -> Prop;
refinesS_eq E stack R =
refinesS E E stack stack (eqPreRel E stack) (eqPostRel E stack) R R (eqRR R);


-- Return for SpecM
primitive retS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> a ->
SpecM E stack a;
Expand Down Expand Up @@ -3294,6 +3307,74 @@ appendCastBVVecS E stack n len1 len2 len3 a v1 v2 =
(bvEqWithProof n (bvAdd n len1 len2) len3);


--------------------------------------------------------------------------------
-- Monadic test functions

test_fun0 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
m-yac marked this conversation as resolved.
Show resolved Hide resolved
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);
-}


--------------------------------------------------------------------------------
-- SMT Array

Expand Down
Loading