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

CI for Cryptol monadification and Mr. Solver #1593

Merged
merged 4 commits into from
Feb 22, 2022
Merged

CI for Cryptol monadification and Mr. Solver #1593

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fd59d74
add CI for Cryptol monadification and Mr. Solver
m-yac Feb 21, 2022
c36858a
Merge branch 'master' into mr-solver/ci
m-yac Feb 22, 2022
a766811
add `is_convertible`, check terms against expected in monadify tests
m-yac Feb 22, 2022
e72b832
remove outdated comment
m-yac Feb 22, 2022
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
34 changes: 34 additions & 0 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,40 @@ jobs:
name: "saw-${{ runner.os }}-${{ matrix.ghc }}"
path: "dist/bin/saw"

mr-solver-tests:
needs: [build]
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-10.15]
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v2
with:
submodules: true

- shell: bash
run: .github/ci.sh install_system_deps
env:
BUILD_TARGET_OS: ${{ matrix.os }}

- uses: actions/download-artifact@v2
with:
name: "${{ runner.os }}-bins"
path: dist/bin

- name: Update PATH to include SAW
shell: bash
run: |
chmod +x dist/bin/*
echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH

- working-directory: examples/mr_solver
shell: bash
run: |
saw monadify.saw
saw mr_solver_unit_tests.saw

heapster-tests:
needs: [build]
strategy:
Expand Down
123 changes: 93 additions & 30 deletions examples/mr_solver/monadify.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,50 +2,113 @@
enable_experimental;
import "SpecPrims.cry" as SpecPrims;
import "monadify.cry";
load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore";
set_monadification "SpecPrims::exists" "Prelude.existsM";
set_monadification "SpecPrims::forall" "Prelude.forallM";

let run_test name cry_term mon_term_expected =
do { print (str_concat "Test: " name);
print "Original term:";
print_term cry_term;
mon_term <- monadify_term cry_term;
print "Monadified term:";
print_term mon_term;
success <- is_convertible mon_term mon_term_expected;
if success then print "Success - monadified term matched expected\n" else
do { print "Test failed - did not match expected monadified term:";
print_term mon_term_expected;
exit 1; }; };

my_abs <- unfold_term ["my_abs"] {{ my_abs }};
print "[my_abs] original term:";
print_term my_abs;
my_absM <- monadify_term my_abs;
print "[my_abs] monadified term:";
print_term my_absM;
my_abs_M <- parse_core_mod "CryptolM" "\
\ \\(x : (mseq (TCNum 64) Bool)) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x' : (isFinite (TCNum 64))) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x'' : (isFinite (TCNum 64))) -> \
\ ite (CompM (mseq (TCNum 64) Bool)) \
\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \
\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x''' : (isFinite (TCNum 64))) -> \
\ returnM (mseq (TCNum 64) Bool) (ecNeg (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x))) \
\ (returnM (mseq (TCNum 64) Bool) x)))";
run_test "my_abs" my_abs my_abs_M;

/*
err_if_lt0 <- unfold_term ["err_if_lt0"] {{ err_if_lt0 }};
print "[err_if_lt0] original term:";
err_if_lt0M <- monadify_term err_if_lt0;
print "[err_if_lt0] monadified term:";
print_term err_if_lt0M;
*/
err_if_lt0_M <- parse_core_mod "CryptolM" "\
\ \\(x : (mseq (TCNum 64) Bool)) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x' : (isFinite (TCNum 64))) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x'' : (isFinite (TCNum 64))) -> \
\ ite (CompM (mseq (TCNum 64) Bool)) \
\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \
\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
\ (bindM (isFinite (TCNum 8)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 8)) \
\ (\\(x''' : (isFinite (TCNum 8))) -> \
\ ecErrorM (mseq (TCNum 64) Bool) (TCNum 5) \
\ (seqToMseq (TCNum 5) (mseq (TCNum 8) Bool) \
\ [ ecNumber (TCNum 120) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \
\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \
\ , ecNumber (TCNum 60) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \
\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \
\ , ecNumber (TCNum 48) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') ]))) \
\ (returnM (mseq (TCNum 64) Bool) x)))";
run_test "err_if_lt0" err_if_lt0 err_if_lt0_M;

/*
sha1 <- {{ sha1 }};
print "[SHA1] original term:";
print "Test: sha1";
print "Original term:";
print_term sha1;
mtrm <- monadify_term sha1;
print "[SHA1] monadified term:";
print_term mtrm;
sha1M <- monadify_term sha1;
print "Monadified term:";
print_term sha1M;
*/

fib <- unfold_term ["fib"] {{ fib }};
print "[fib] original term:";
print_term fib;
fibM <- monadify_term fib;
print "[fib] monadified term:";
print_term fibM;
fibM <- parse_core_mod "CryptolM" "\
\ \\(_x : (mseq (TCNum 64) Bool)) -> \
\ multiArgFixM (LRT_Fun (mseq (TCNum 64) Bool) (\\(_ : (mseq (TCNum 64) Bool)) -> LRT_Ret (mseq (TCNum 64) Bool))) \
\ (\\(fib : ((mseq (TCNum 64) Bool) -> (CompM (mseq (TCNum 64) Bool)))) -> \
\ \\(x : (mseq (TCNum 64) Bool)) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x' : (isFinite (TCNum 64))) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x'' : (isFinite (TCNum 64))) -> \
\ ite (CompM (mseq (TCNum 64) Bool)) \
\ (ecEq (mseq (TCNum 64) Bool) (PEqMSeqBool (TCNum 64) x') x \
\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x''' : (isFinite (TCNum 64))) -> \
\ returnM (mseq (TCNum 64) Bool) \
\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \
\ (PLiteralSeqBoolM (TCNum 64) x''')))) \
\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x''' : (isFinite (TCNum 64))) -> \
\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
\ (\\(x'''' : (isFinite (TCNum 64))) -> \
\ bindM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \
\ (fib \
\ (ecMinus (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \
\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \
\ (PLiteralSeqBoolM (TCNum 64) x'''')))) \
\ (\\(x''''' : (mseq (TCNum 64) Bool)) -> \
\ returnM (mseq (TCNum 64) Bool) \
\ (ecMul (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \
\ x''''')))))))) \
\ _x";
run_test "fib" fib fibM;

noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }};
print "[noErrors] original term:";
print_term noErrors;
noErrorsM <- monadify_term noErrors;
print "[noErrors] monadified term:";
print_term noErrorsM;
noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsM a a (\\(x : a) -> returnM a x)";
run_test "noErrors" noErrors noErrorsM;

fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }};
print "[fibSpecNoErrors] original term:";
print_term fibSpecNoErrors;
fibSpecNoErrorsM <- monadify_term fibSpecNoErrors;
print "[fibSpecNoErrors] monadified term:";
print_term fibSpecNoErrorsM;
fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\
\ \\(__p1 : (mseq (TCNum 64) Bool)) -> \
\ existsM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \
\ (\\(x : (mseq (TCNum 64) Bool)) -> \
\ returnM (mseq (TCNum 64) Bool) x)";
run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM;
16 changes: 9 additions & 7 deletions src/SAWScript/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -323,15 +323,17 @@ hoistIfsPrim t = do

return t{ ttTerm = t' }

isConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel Bool
isConvertiblePrim x y = do
sc <- getSharedContext
io $ scConvertible sc False (ttTerm x) (ttTerm y)

checkConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel ()
checkConvertiblePrim x y = do
sc <- getSharedContext
str <- io $ do
c <- scConvertible sc False (ttTerm x) (ttTerm y)
pure (if c
then "Convertible"
else "Not convertible")
printOutLnTop Info str
c <- isConvertiblePrim x y
printOutLnTop Info (if c
then "Convertible"
else "Not convertible")


readCore :: FilePath -> TopLevel TypedTerm
Expand Down
7 changes: 6 additions & 1 deletion src/SAWScript/Interpreter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1071,10 +1071,15 @@ primitives = Map.fromList
, "object that can be passed to 'read_sbv'."
]

, prim "is_convertible" "Term -> Term -> TopLevel Bool"
(pureVal isConvertiblePrim)
Current
[ "Returns true iff the two terms are convertible." ]

, prim "check_convertible" "Term -> Term -> TopLevel ()"
(pureVal checkConvertiblePrim)
Current
[ "Check if two terms are convertible." ]
[ "Check if two terms are convertible and print the result." ]

, prim "replace" "Term -> Term -> Term -> TopLevel Term"
(pureVal replacePrim)
Expand Down