From d021bb1cce19f1c2fe752300942d7606055c3584 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 May 2021 18:11:48 -0400 Subject: [PATCH 1/2] make readBack of an empty list actually return an empty list --- cryptol-remote-api/src/CryptolServer/Data/Expression.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index 553276875..ba537997a 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -389,8 +389,6 @@ readBack ty val = VInteger i -> pure (IntegerModulo i n) _ -> mismatchPanic TVSeq len contents - | len == 0 -> - return Unit | contents == TVBit , VWord width wv <- val -> do BV w v <- asWordVal C.Concrete wv From be72b86cba8d4eedd1a24c3420f7b4a333741c54 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 May 2021 18:18:10 -0400 Subject: [PATCH 2/2] update test_SHA256 --- cryptol-remote-api/python/tests/cryptol/test_SHA256.py | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py index 26e8eaaf4..56b45fd36 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py +++ b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py @@ -17,11 +17,9 @@ def test_SHA256(self): 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() expected_h2 = BV(size=256, value=0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) self.assertEqual(h2, expected_h2)