cryptol-remote-api: initial support for :sat and python tests

cryptol-remote-api/cryptol-remote-api/Main.hs

@@ -47,5 +47,5 @@ cryptolMethods =
   , ("call",                Query,   method call)
   , ("visible names",       Query,   method visibleNames)
   , ("check type",          Query,   method checkType)
-  , ("satisfy",             Query,   method sat)
+  , ("sat",                 Query,   method sat)
   ]

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

@@ -71,27 +71,38 @@ sat (ProveSatParams (Prover name) jsonExpr num) =
                 Satisfied <$> traverse satResult results
 
   where
-    satResult :: [(Type, Expr, Value)] -> Method ServerState [(JSONType, Expression)]
-    satResult es = traverse result es
+    satResult :: [(Type, Expr, Value)] -> Method ServerState Model
+    satResult es = Model <$> traverse mkAssignment es
 
-    result (t, _, v) =
+    mkAssignment (t, _, v) =
       do prims <- runModuleCmd getPrimMap
          e <- observe $ readBack prims t v
-         return (JSONType mempty t, e)
+         return $ SatArgAssignment { assignmentType = JSONType mempty t
+                                   , assignmentExpr = e}
 
-data SatResult = Unsatisfiable | Satisfied [[(JSONType, Expression)]]
+data SatArgAssignment
+  = SatArgAssignment
+    { assignmentType :: JSONType
+    , assignmentExpr :: Expression
+    }
+
+newtype Model = Model {modelAssignments :: [SatArgAssignment]}
+
+data SatResult
+  = Unsatisfiable
+  | Satisfied [Model]
 
 instance ToJSON SatResult where
-  toJSON Unsatisfiable = JSON.object ["result" .= ("unsatisfiable" :: Text)]
-  toJSON (Satisfied xs) =
-    JSON.object [ "result" .= ("satisfied" :: Text)
-                , "model" .=
-                  [ [ JSON.object [ "type" .= t
-                                  , "expr" .= e
+  toJSON Unsatisfiable = JSON.object ["result" .= ("unsat" :: Text)]
+  toJSON (Satisfied models) =
+    JSON.object [ "result" .= ("sat" :: Text)
+                , "models" .=
+                  [ [ JSON.object [ "type" .= assignmentType a
+                                  , "expr" .= assignmentExpr a
                                   ]
-                    | (t, e) <- res
+                    | a <- modelAssignments m
                     ]
-                  | res <- xs
+                  | m <- models
                   ]
                 ]
 

cryptol-remote-api/test-scripts/Foo.cry

@@ -49,3 +49,6 @@ op10 a = 0
 
 op11 : {n} (fin n) => [n] -> [lg2 n]
 op11 a = 0
+
+isSqrtOf9 : [8] -> Bit
+isSqrtOf9 x = x*x == 9

cryptol-remote-api/test-scripts/cryptol-api_test.py

@@ -4,6 +4,7 @@ from cryptol import CryptolConnection, CryptolContext, cry
 import cryptol
 import cryptol.cryptoltypes
 from cryptol.bitvector import BV
+import cryptol.solver as solver
 from BitVector import *
 
 dir_path = os.path.dirname(os.path.realpath(__file__))
@@ -38,4 +39,28 @@ class CryptolTests(unittest.TestCase):
         self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0))
 
 
+    def test_sat(self):
+        # test a single sat model can be returned
+        rootsOf9 = c.sat('isSqrtOf9').result()
+        self.assertEqual(len(rootsOf9), 1)
+        self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9)
+
+        # check we can specify the solver
+        rootsOf9 = c.sat('isSqrtOf9', solver = solver.ANY).result()
+        self.assertEqual(len(rootsOf9), 1)
+        self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9)
+
+        # check we can ask for a specific number of results
+        rootsOf9 = c.sat('isSqrtOf9', sat_num = 3).result()
+        self.assertEqual(len(rootsOf9), 3)
+        self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9])
+
+        # check we can ask for all results
+        rootsOf9 = c.sat('isSqrtOf9', sat_num = None).result()
+        self.assertEqual(len(rootsOf9), 4)
+        self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9,9])
+
+        # check for an unsat condition
+        self.assertFalse(c.sat('\\x -> isSqrtOf9 x && ~(elem x [3,131,125,253])').result())
+
 unittest.main()

deps/argo

@@ -1 +1 @@
-Subproject commit 5217d1da928a5d1902186db991dacb047d1da5d7
+Subproject commit b76fa11601d53566c492da3b9af176b53ad1c560