Merge pull request #1269 from GaloisInc/rpc/record-bug

[RPC] Fix bug in Cryptol JSON -> Python for records, add test

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

@@ -33,7 +33,7 @@ def from_cryptol_arg(val : Any) -> Any:
         elif tag == 'tuple':
             return tuple(from_cryptol_arg(x) for x in val['data'])
         elif tag == 'record':
-            return {k : from_cryptol_arg(val[k]) for k in val['data']}
+            return {k : from_cryptol_arg(val['data'][k]) for k in val['data']}
         elif tag == 'sequence':
             return [from_cryptol_arg(v) for v in val['data']]
         elif tag == 'bits':

cryptol-remote-api/python/tests/cryptol/test-files/Types.cry

@@ -0,0 +1,25 @@
+module Types where
+
+b : Bit
+b = True
+
+w : [16]
+w = 42
+
+z : Integer
+z = 420000
+
+m : Z 12
+m = 6
+
+q : Rational
+q = ratio 5 4
+
+t : (Bit, Integer)
+t = (False, 7)
+
+s : [3][3][8]
+s = [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
+
+r : {xCoord : [32], yCoord : [32]}
+r = {xCoord = 12 : [32], yCoord = 21 : [32]}

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)
 
-        self.assertTrue(c.safe("aesEncrypt"))
-        self.assertTrue(c.safe("aesDecrypt"))
+        self.assertTrue(c.safe("aesEncrypt").result())
+        self.assertTrue(c.safe("aesDecrypt").result())
         self.assertTrue(c.check("AESCorrect").result().success)
         # c.prove("AESCorrect") # probably takes too long for this script...?
 

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

@@ -7,7 +7,7 @@
 
 
 class TestDES(unittest.TestCase):
-    def test_SHA256(self):
+    def test_DES(self):
         c = cryptol.connect(verify=False)
         c.load_file(str(Path('tests','cryptol','test-files','examples','DEStest.cry')))
 

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

@@ -0,0 +1,45 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.opaque import OpaqueValue
+from cryptol.bitvector import BV
+
+
+class CryptolTypeTests(unittest.TestCase):
+    def test_types(self):
+        c = cryptol.connect(verify=False)
+        c.load_file(str(Path('tests','cryptol','test-files','Types.cry')))
+
+        # Bits
+        self.assertEqual(c.eval('b').result(), True)
+
+        # Words
+        self.assertEqual(c.eval('w').result(), BV(size=16, value=42))
+
+        # Integers
+        self.assertEqual(c.eval('z').result(), 420000)
+
+        # Modular integers - not supported at all
+        with self.assertRaises(ValueError):
+            c.eval('m').result()
+
+        # Rationals - supported only as opaque values
+        self.assertIsInstance(c.eval('q').result(), OpaqueValue)
+
+        # Tuples
+        self.assertEqual(c.eval('t').result(), (False, 7))
+
+        # Sequences
+        self.assertEqual(c.eval('s').result(),
+            [[BV(size=8, value=1), BV(size=8, value=2), BV(size=8, value=3)],
+             [BV(size=8, value=4), BV(size=8, value=5), BV(size=8, value=6)],
+             [BV(size=8, value=7), BV(size=8, value=8), BV(size=8, value=9)]])
+
+        # Records
+        self.assertEqual(c.eval('r').result(),
+            {'xCoord': BV(size=32, value=12),
+             'yCoord': BV(size=32, value=21)})
+
+if __name__ == "__main__":
+    unittest.main()