CI for Cryptol monadification and Mr. Solver (#1593)

* add CI for Cryptol monadification and Mr. Solver * add `is_convertible`, check terms against expected in monadify tests * remove outdated comment
GaloisInc · Feb 22, 2022 · d31f778 · d31f778
1 parent 70f5197
commit d31f778
Show file tree

Hide file tree

Showing 4 changed files with 142 additions and 38 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -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:

diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw
@@ -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;
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -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

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -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)