From ec2a23abf12ba2318a2fcba1bb8ec13f2b77bf02 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 14 Apr 2021 17:33:06 -0400 Subject: [PATCH 1/5] add SHA256 test, add from_cryptol_arg to CryptolEvalExpr --- cryptol-remote-api/python/cryptol/__init__.py | 2 +- .../python/tests/cryptol/test_SHA256.py | 36 +++++++++++++++++++ 2 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 cryptol-remote-api/python/tests/cryptol/test_SHA256.py diff --git a/cryptol-remote-api/python/cryptol/__init__.py b/cryptol-remote-api/python/cryptol/__init__.py index 3a2ceecb6..17eef8ee9 100644 --- a/cryptol-remote-api/python/cryptol/__init__.py +++ b/cryptol-remote-api/python/cryptol/__init__.py @@ -112,7 +112,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: diff --git a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py new file mode 100644 index 000000000..5ff7a7d32 --- /dev/null +++ b/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() From ff26feb83c225a02d15f2d9980bf2de6cc9e5d92 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 15 Apr 2021 13:38:13 -0400 Subject: [PATCH 2/5] add test_DES, fix string literals in test_SHA256 --- .../python/tests/cryptol/test_DES.py | 48 +++++++++++++++++++ .../python/tests/cryptol/test_SHA256.py | 20 ++++---- 2 files changed, 58 insertions(+), 10 deletions(-) create mode 100644 cryptol-remote-api/python/tests/cryptol/test_DES.py diff --git a/cryptol-remote-api/python/tests/cryptol/test_DES.py b/cryptol-remote-api/python/tests/cryptol/test_DES.py new file mode 100644 index 000000000..4fd5057e9 --- /dev/null +++ b/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() diff --git a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py index 5ff7a7d32..26e8eaaf4 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py +++ b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py @@ -11,23 +11,23 @@ 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() + 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() + # 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() + 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) From bc03778420e260b87cb034dd3b0b182dd0a47b84 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 22 Apr 2021 14:55:52 -0400 Subject: [PATCH 3/5] add test_EvenMansour --- .../python/tests/cryptol/test_EvenMansour.py | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py diff --git a/cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py b/cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py new file mode 100644 index 000000000..e894a5f7e --- /dev/null +++ b/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() From 9572ddbbf4d78a6055d975b278a4d4cae35228c7 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 23 Apr 2021 14:02:29 -0400 Subject: [PATCH 4/5] update evaluate_expression call in test-cryptol-remote-api.py --- cryptol-remote-api/test-cryptol-remote-api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-remote-api/test-cryptol-remote-api.py b/cryptol-remote-api/test-cryptol-remote-api.py index 083a53b29..5b6e5474e 100644 --- a/cryptol-remote-api/test-cryptol-remote-api.py +++ b/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") == 2 From 90baa856f2969ef0ea61d2ee57d0704c1883034c Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 23 Apr 2021 14:54:36 -0400 Subject: [PATCH 5/5] whoops, added back result() to test-cryptol-remote-api.py --- cryptol-remote-api/test-cryptol-remote-api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-remote-api/test-cryptol-remote-api.py b/cryptol-remote-api/test-cryptol-remote-api.py index 5b6e5474e..fa086048c 100644 --- a/cryptol-remote-api/test-cryptol-remote-api.py +++ b/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") == 2 +assert c.evaluate_expression("1+1").result() == 2