feat(rpc): safe for python api

cryptol-remote-api/python/cryptol/__init__.py

@@ -200,7 +200,7 @@ def process_result(self, res : Any) -> Any:
         if res['result'] == 'unsatisfiable':
             if self.qtype == 'sat':
                 return False
-            elif self.qtype == 'prove':
+            elif self.qtype == 'prove' or self.qtype == 'safe':
                 return True
             else:
                 raise ValueError("Unknown prove/sat query type: " + self.qtype)
@@ -212,7 +212,7 @@ def process_result(self, res : Any) -> Any:
                     for m in res['models']
                     for arg in m]
         else:
-            raise ValueError("Unknown sat result " + str(res))
+            raise ValueError("Unknown prove or sat result " + str(res))
 
 class CryptolProve(CryptolProveSat):
     def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
@@ -222,6 +222,10 @@ class CryptolSat(CryptolProveSat):
     def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None:
         super(CryptolSat, self).__init__(connection, 'sat', expr, solver, count)
 
+class CryptolSafe(CryptolProveSat):
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
+        super(CryptolSafe, self).__init__(connection, 'safe', expr, solver, 1)
+
 class CryptolNames(argo.Command):
     def __init__(self, connection : HasProtocolState) -> None:
         super(CryptolNames, self).__init__('visible names', {}, connection)
@@ -456,6 +460,13 @@ def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
         self.most_recent_result = CryptolProve(self, expr, solver)
         return self.most_recent_result
 
+    def safe(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
+        """Check via an external SMT solver that the given term is safe for all inputs,
+        which means it cannot encounter a run-time error.
+        """
+        self.most_recent_result = CryptolSafe(self, expr, solver)
+        return self.most_recent_result
+
     def names(self) -> argo.Command:
         """Discover the list of names currently in scope in the current context."""
         self.most_recent_result = CryptolNames(self)

cryptol-remote-api/python/tests/cryptol/test_AES.py

@@ -28,8 +28,8 @@ def test_AES(self):
         decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
         self.assertEqual(pt, decrypted_ct)
 
-        # c.safe("aesEncrypt")
-        # c.safe("aesDecrypt")
+        self.assertTrue(c.safe("aesEncrypt"))
+        self.assertTrue(c.safe("aesDecrypt"))
         self.assertTrue(c.check("AESCorrect").result().success)
         # c.prove("AESCorrect") # probably takes too long for this script...?
 

cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py

@@ -138,6 +138,15 @@ def test_check(self):
         self.assertEqual(len(res.args), 1)
         self.assertIsInstance(res.error_msg, str)
 
+    def test_safe(self):
+        c = self.c
+        res = c.safe("\\x -> x==(x:[8])").result()
+        self.assertTrue(res)
+
+        res = c.safe("\\x -> x / (x:[8])").result()
+        self.assertEqual(res, [BV(size=8, value=0)])
+
+
     def test_many_usages_one_connection(self):
         c = self.c
         for i in range(0,100):

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -157,6 +157,7 @@ instance FromJSON ProveSatParams where
            \case
              "sat" -> pure (SatQuery numResults)
              "prove" -> pure ProveQuery
+             "safe" -> pure SafetyQuery
              _ -> empty)
       num v = ((JSON.withText "all" $
                \t -> if t == "all" then pure AllSat else empty) v) <|>
@@ -174,17 +175,23 @@ instance Doc.DescribedParams ProveSatParams where
                      ++ (concat (map (\p -> [Doc.Literal (T.pack p), Doc.Text ", "]) proverNames))
                      ++ [Doc.Text "."]))
     , ("expression",
-      Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check for satisfiability; "
-                    , Doc.Text "must be a monomorphic function with return type Bit." ])
+      Doc.Paragraph [ Doc.Text "The function to check for validity, satisfiability, or safety"
+                    , Doc.Text " depending on the specified value for "
+                    , Doc.Literal "query type"
+                    , Doc.Text ". For validity and satisfiability checks, the function must be a predicate"
+                    , Doc.Text " (i.e., monomorphic function with return type Bit)."
+                    ])
     , ("result count",
       Doc.Paragraph [Doc.Text "How many satisfying results to search for; either a positive integer or "
-                    , Doc.Literal "all", Doc.Text"."])
+                    , Doc.Literal "all", Doc.Text". Only affects satisfiability checks."])
     , ("query type",
-      Doc.Paragraph [ Doc.Text "Whether to attempt to prove ("
+      Doc.Paragraph [ Doc.Text "Whether to attempt to prove the predicate is true for all possible inputs ("
                     , Doc.Literal "prove"
-                    , Doc.Text ") or satisfy ("
+                    , Doc.Text "), find some inputs which make the predicate true ("
                     , Doc.Literal "sat"
-                    , Doc.Text ") the predicate."
+                    , Doc.Text "), or prove a function is safe ("
+                    , Doc.Literal "safe"
+                    , Doc.Text ")."
                     ]
       )
     ]