Finish updating KRYPTO test suite to use Bytes

runtimeverification · Oct 23, 2023 · d2face5 · d2face5
1 parent 8c862de
commit d2face5
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 17 deletions.
diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs
@@ -1746,7 +1746,8 @@ kryptoModule =
         { moduleName = kryptoModuleName
         , moduleAttributes = Attributes []
         , moduleSentences =
-            [ importParsedModule stringModuleName
+            [ importParsedModule bytesModuleName
+            , importParsedModule stringModuleName
             , importParsedModule intModuleName
             , importParsedModule listModuleName
             , hookedSymbolDecl ecdsaRecoverSymbol

diff --git a/kore/test/Test/Kore/Builtin/Krypto.hs b/kore/test/Test/Kore/Builtin/Krypto.hs
@@ -72,13 +72,13 @@ test_ecdsaRecover =
   where
     test messageHash v r s result =
         testCase (Text.unpack name) $ do
-            let expect = InternalBytes.asPattern internalBytesSort (BS.pack result)
+            let expect = InternalBytes.asPattern bytesSort (BS.pack result)
             actual <-
                 ecdsaRecoverKrypto
-                    (InternalBytes.asInternal internalBytesSort (BS.pack messageHash))
+                    (InternalBytes.asInternal bytesSort (BS.pack messageHash))
                     (Test.Int.asInternal v)
-                    (InternalBytes.asInternal internalBytesSort (BS.pack r))
-                    (InternalBytes.asInternal internalBytesSort (BS.pack s))
+                    (InternalBytes.asInternal bytesSort (BS.pack r))
+                    (InternalBytes.asInternal bytesSort (BS.pack s))
                     & evaluate "KRYPTO.ecdsaRecover"
             assertEqual "" expect actual
       where
@@ -104,13 +104,13 @@ test_secp256k1EcdsaRecover =
   where
     test messageHash v r s result =
         testCase (Text.unpack name) $ do
-            let expect = String.asPattern stringSort result
+            let expect = InternalBytes.asPattern bytesSort (BS.pack result)
             actual <-
                 ecdsaRecoverKrypto
-                    (String.asInternal stringSort messageHash)
+                    (InternalBytes.asInternal bytesSort (BS.pack messageHash))
                     (Test.Int.asInternal v)
-                    (String.asInternal stringSort r)
-                    (String.asInternal stringSort s)
+                    (InternalBytes.asInternal bytesSort (BS.pack r))
+                    (InternalBytes.asInternal bytesSort (BS.pack s))
                     & evaluate "SECP256K1.ecdsaRecover"
             assertEqual "" expect actual
       where
@@ -133,7 +133,7 @@ test_keccak256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                keccak256Krypto (String.asInternal stringSort input)
+                keccak256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "KRYPTO.keccak256"
             assertEqual "" expect actual
 
@@ -152,7 +152,7 @@ test_hashKeccak256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                keccak256Krypto (String.asInternal stringSort input)
+                keccak256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "HASH.keccak256"
             assertEqual "" expect actual
 
@@ -171,7 +171,7 @@ test_sha256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                sha256Krypto (String.asInternal stringSort input)
+                sha256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "KRYPTO.sha256"
             assertEqual "" expect actual
 
@@ -190,7 +190,7 @@ test_hashSha256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                sha256Krypto (String.asInternal stringSort input)
+                sha256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "HASH.sha256"
             assertEqual "" expect actual
 
@@ -209,7 +209,7 @@ test_sha3256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                sha3256Krypto (String.asInternal stringSort input)
+                sha3256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "KRYPTO.sha3256"
             assertEqual "" expect actual
 
@@ -228,7 +228,7 @@ test_hashSha3_256 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                sha3256Krypto (String.asInternal stringSort input)
+                sha3256Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "HASH.sha3_256"
             assertEqual "" expect actual
 
@@ -253,7 +253,7 @@ test_ripemd160 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                ripemd160Krypto (String.asInternal stringSort input)
+                ripemd160Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "KRYPTO.ripemd160"
             assertEqual "" expect actual
 
@@ -278,7 +278,7 @@ test_hashRipemd160 =
         testCase (show input) $ do
             let expect = String.asPattern stringSort result
             actual <-
-                ripemd160Krypto (String.asInternal stringSort input)
+                ripemd160Krypto (InternalBytes.asInternal bytesSort (BS.pack input))
                     & evaluate "HASH.ripemd160"
             assertEqual "" expect actual