From 55a5f359d73b0044a3646b139a9e5d780a175c47 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 24 Aug 2021 18:50:06 -0400 Subject: [PATCH 1/3] fix bug in dict case of from_cryptol_arg --- cryptol-remote-api/python/cryptol/commands.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index 888aee744..90e4f0b4e 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/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': From c66ecedef22a4c90f7e5bef7f3db4fc037bd94c8 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 24 Aug 2021 18:52:18 -0400 Subject: [PATCH 2/3] add `test_types.py` --- .../python/tests/cryptol/test-files/Types.cry | 25 +++++++++++ .../python/tests/cryptol/test_types.py | 45 +++++++++++++++++++ 2 files changed, 70 insertions(+) create mode 100644 cryptol-remote-api/python/tests/cryptol/test-files/Types.cry create mode 100644 cryptol-remote-api/python/tests/cryptol/test_types.py diff --git a/cryptol-remote-api/python/tests/cryptol/test-files/Types.cry b/cryptol-remote-api/python/tests/cryptol/test-files/Types.cry new file mode 100644 index 000000000..bcc3a683e --- /dev/null +++ b/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]} diff --git a/cryptol-remote-api/python/tests/cryptol/test_types.py b/cryptol-remote-api/python/tests/cryptol/test_types.py new file mode 100644 index 000000000..cf20595e8 --- /dev/null +++ b/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() From 0a5537e1c00f12718952a03517b353f498c203f6 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 24 Aug 2021 18:53:01 -0400 Subject: [PATCH 3/3] fix .result() bug in AES test, fix typo in DES test --- cryptol-remote-api/python/tests/cryptol/test_AES.py | 4 ++-- cryptol-remote-api/python/tests/cryptol/test_DES.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cryptol-remote-api/python/tests/cryptol/test_AES.py b/cryptol-remote-api/python/tests/cryptol/test_AES.py index 65e155a07..a5289febd 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_AES.py +++ b/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...? diff --git a/cryptol-remote-api/python/tests/cryptol/test_DES.py b/cryptol-remote-api/python/tests/cryptol/test_DES.py index 9fd2b43e4..492e713ad 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_DES.py +++ b/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')))