-
Notifications
You must be signed in to change notification settings - Fork 63
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[MRSolver] Changes to Mr. Solver to get zero_array working (#1624)
* add exp_explosion_mr_solver.saw, add is_elem_noErrorsSpec * progress on mr_solver zero_array |= zero_array_spec * fix mrFunOutType, fix lifting and use asApplyAll in askMRSolverH * implement vecMapM, (ec)atM, (ec)updateM without Nat__rec * add maybe elim for IsLe(/Lt)Nat * make `bvNat w (bvToNat w' n)` reduce to `n` in the simulator * add cases for vecMapM, atM, updateM to normComp/normBind * remove maybe elim for IsLe(/Lt)Nat, always unfold is_bvule(t) in maybe * add macro for precondHint in Monadify.hs * do beta reds + look past asserts in mrGetPrecond, get loop spec working * added specification primitives for cryptol * add precondHint to specPrims.saw, lookup macros in set_monadification * rename precondHint to invariantHint * add assertingM, assumingM, and their monadification macros * add assertingM, assumingM to Mr. Solver * add bvVecMapInvarM, get zero_array_spec refinement working * update Prelude.v, clean up comments * whoops remove SAWCorePrelude.v * attempt to fix CI build failure on GHC 8.8.4 Co-authored-by: Eddy Westbrook <westbrook@galois.com>
- Loading branch information
Showing
21 changed files
with
719 additions
and
195 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,6 +15,7 @@ Description: | |
|
|
||
| extra-source-files: | ||
| saw/Cryptol.sawcore | ||
| saw/CryptolM.sawcore | ||
|
|
||
| library | ||
| build-depends: | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| module SpecPrims where | ||
|
|
||
| /* Specification primitives */ | ||
|
|
||
| // The specification that holds for f x for some input x | ||
| exists : {a, b} (a -> b) -> b | ||
| exists f = error "Cannot run exists" | ||
|
|
||
| // The specification that holds for f x for all inputs x | ||
| forall : {a, b} (a -> b) -> b | ||
| forall f = error "Cannot run forall" | ||
|
|
||
| // The specification that a computation returns some value with no errors | ||
| returnsSpec : {a} a | ||
| returnsSpec = exists (\x -> x) | ||
|
|
||
| // The specification that matches any computation. This calls exists at the | ||
| // function type () -> a, which is monadified to () -> CompM a. This means that | ||
| // the exists does not just quantify over all values of type a like noErrors, | ||
| // but it quantifies over all computations of type a, including those that | ||
| // contain errors. | ||
| anySpec : {a} a | ||
| anySpec = exists (\f -> f ()) | ||
|
|
||
| // The specification which asserts that the first argument is True and then | ||
| // returns the second argument | ||
| asserting : {a} Bit -> a -> a | ||
| asserting b x = if b then x else error "Assertion failed" | ||
|
|
||
| // The specification which assumes that the first argument is True and then | ||
| // returns the second argument | ||
| assuming : {a} Bit -> a -> a | ||
| assuming b x = if b then x else anySpec | ||
|
|
||
| // A hint to Mr Solver that a recursive function has the given loop invariant | ||
| invariantHint : {a} Bit -> a -> a | ||
| invariantHint b x = x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
|
|
||
| module Arrays where | ||
|
|
||
| import SpecPrims | ||
|
|
||
| zero_array_loop_spec : {n} Literal n [64] => [n][64] -> [n][64] | ||
| zero_array_loop_spec ys = loop 0 ys | ||
| where loop : [64] -> [n][64] -> [n][64] | ||
| loop i xs = invariantHint (i <= 0x0fffffffffffffff) | ||
| (if i < `n then loop (i+1) (update xs i 0) | ||
| else xs) | ||
|
|
||
| zero_array_spec : {n} Literal n [64] => [n][64] -> [n][64] | ||
| zero_array_spec xs = assuming (`n <= 0x0fffffffffffffff) | ||
| [ 0 | _ <- xs ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
|
|
||
| module ExpExplosion where | ||
|
|
||
| op : [64] -> [64] -> [64] | ||
| op x y = x ^ (y << (1 : [6])) | ||
|
|
||
| exp_explosion_spec : [64] -> [64] | ||
| exp_explosion_spec x0 = x15 | ||
| where x1 = op x0 x0 | ||
| x2 = op x1 x1 | ||
| x3 = op x2 x2 | ||
| x4 = op x3 x3 | ||
| x5 = op x4 x4 | ||
| x6 = op x5 x5 | ||
| x7 = op x6 x6 | ||
| x8 = op x7 x7 | ||
| x9 = op x8 x8 | ||
| x10 = op x9 x9 | ||
| x11 = op x10 x10 | ||
| x12 = op x11 x11 | ||
| x13 = op x12 x12 | ||
| x14 = op x13 x13 | ||
| x15 = op x14 x14 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| include "exp_explosion.saw"; | ||
|
|
||
| let eq_bool b1 b2 = | ||
| if b1 then | ||
| if b2 then true else false | ||
| else | ||
| if b2 then false else true; | ||
|
|
||
| let fail = do { print "Test failed"; exit 1; }; | ||
| let run_test name test expected = | ||
| do { if expected then print (str_concat "Test: " name) else | ||
| print (str_concat (str_concat "Test: " name) " (expecting failure)"); | ||
| actual <- test; | ||
| if eq_bool actual expected then print "Success\n" else | ||
| do { print "Test failed\n"; exit 1; }; }; | ||
|
|
||
|
|
||
|
|
||
| import "exp_explosion.cry"; | ||
| monadify_term {{ op }}; | ||
|
|
||
| exp_explosion <- parse_core_mod "exp_explosion" "exp_explosion"; | ||
| run_test "exp_explosion |= exp_explosion_spec" (mr_solver exp_explosion {{ exp_explosion_spec }}) true; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.