Merge remote-tracking branch 'origin/master' into lisanna/release-imp…

…rovements

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

@@ -86,7 +86,7 @@ def __init__(self, connection : HasProtocolState, expr : Any) -> None:
         )
 
     def process_result(self, res : Any) -> Any:
-        return res
+        return from_cryptol_arg(res['value'])
 
 class CryptolCall(argo.Command):
     def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None:

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

@@ -0,0 +1,48 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
+from cryptol.bitvector import BV
+
+
+class TestDES(unittest.TestCase):
+    def test_SHA256(self):
+        c = cryptol.connect()
+        c.load_file(str(Path('tests','cryptol','test-files','examples','DEStest.cry')))
+
+        # we can run the test suite as indended...
+        # vkres = c.eval('vktest DES').result()
+        # self.assertTrue(all(passed for (_,_,passed) in vkres))
+        # vtres = c.eval('vttest DES').result()
+        # self.assertTrue(all(passed for (_,_,passed) in vtres))
+        # kares = c.eval('katest DES').result()
+        # self.assertTrue(all(passed for (_,_,passed) in kares))
+
+        # ...but we can also do it manually, using the python bindings more
+        def test(key, pt0, ct0):
+            ct1 = c.call('DES.encrypt', key, pt0).result()
+            pt1 = c.call('DES.decrypt', key, ct0).result()
+            self.assertEqual(ct0, ct1)
+            self.assertEqual(pt0, pt1)
+
+        # vktest
+        vk = c.eval('vk').result()
+        pt0 = BV(size=64, value=0)
+        for (key, ct0) in vk:
+            test(key, pt0, ct0)
+
+        # vttest
+        vt = c.eval('vt').result()
+        key = BV(size=64, value=0x0101010101010101)
+        for (pt0, ct0) in vt:
+            test(key, pt0, ct0)
+
+        # katest
+        ka = c.eval('ka').result()
+        for (key, pt0, ct0) in ka:
+            test(key, pt0, ct0)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -0,0 +1,26 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
+from cryptol.bitvector import BV
+
+
+class TestEvenMansour(unittest.TestCase):
+    def test_EvenMansour(self):
+        c = cryptol.connect()
+        c.load_file(str(Path('tests','cryptol','test-files','examples','contrib','EvenMansour.cry')))
+
+        F_10_4 = c.eval('F:[10][4]').result()
+        self.assertTrue(c.call('is_a_permutation', F_10_4).result())
+
+        Finv_10_4 = c.eval("F':[10][4]").result()
+        digits = [ BV(size=4, value=i) for i in range(0,10) ]
+                 # ^ the same as: c.eval('[0..9]:[_][4]').result()
+        self.assertTrue(c.call('is_inverse_permutation', digits, F_10_4, Finv_10_4).result())
+
+        self.assertTrue(c.check('E_and_D_are_inverses').result().success)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -0,0 +1,36 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
+from cryptol.bitvector import BV
+
+
+class TestSHA256(unittest.TestCase):
+    def test_SHA256(self):
+        c = cryptol.connect()
+        c.load_file(str(Path('tests','cryptol','test-files','examples','param_modules','SHA.cry')))
+
+        m1 = CryptolLiteral('"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"')
+        j1 = c.call('join', m1).result()
+        h1 = c.call('sha256', j1).result()
+        expected_h1 = BV(size=256, value=0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1)
+        self.assertEqual(h1, expected_h1)
+
+        # ugh, this gives a type error...
+        # m2 = CryptolLiteral('""')
+        # j2 = c.call('join', m2).result()
+        # h2 = c.call('sha256', j2).result()
+        h2 = c.eval('sha256 (join "")').result()
+        expected_h2 = BV(size=256, value=0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
+        self.assertEqual(h2, expected_h2)
+
+        m3 = CryptolLiteral('"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"')
+        j3 = c.call('join', m3).result()
+        h3 = c.call('sha256', j3).result()
+        expected_h3 = BV(size=256, value=0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
+        self.assertEqual(h3, expected_h3)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -14,4 +14,4 @@
     raise Exception('specify socket or http for connection type')
 
 c.load_module('Cryptol')
-assert c.evaluate_expression("1+1").result()['value'] == 2
+assert c.evaluate_expression("1+1").result() == 2