Update KRYPTO hooks to use Bytes instead of String (#3684)

Fixes #3683 

The `KRYPTO` hooks now use `Bytes` for raw strings instead of `String`,
so this PR updates the evaluators here accordingly.

Additionally, I updated all tests that reference `KRYPTO` lest they give
errors about hooked symbols having incorrect sorts. Specifically,
- I regenerated the `regression-evm` tests by running
`generate-regression-tests.sh` with my branch of KEVM that uses the
updated hooks.
- For all the tests that I couldn't regenerate, I manually patched them
by changing the existing `KRYPTO` symbols into functions which wrap the
new hooks with appropriate calls to `String2Bytes` and `Bytes2String`.

Corresponding PR testing this on the booster:
runtimeverification/hs-backend-booster#370

docs/hooks.md

@@ -856,16 +856,16 @@ If-then-else: if condition then something, else something else.
 
 ## KRYPTO
 
-All hash functions in this module interpret their input string as a sequence of 8-bit bytes
-and output the digest in base-16 encoding
+All hash functions in this module interpret their input byte string as a raw sequence of 
+8-bit bytes and output the digest in base-16 encoding
 (a sequence of hexademical numerals `[0-9a-f]` each corresponding to 4 bits).
 
 ### KRYPTO.keccak256
 
 Compute the Keccak-256 hash of the input string.
 
 ~~~
-    hooked-symbol keccak256{}(String{}) : String{}
+    hooked-symbol keccak256{}(Bytes{}) : String{}
         [hook{}("KRYPTO.keccak256")]
 ~~~
 
@@ -874,7 +874,7 @@ Compute the Keccak-256 hash of the input string.
 Compute the RIPEMD-160 hash of the input string.
 
 ~~~
-    hooked-symbol ripemd160{}(String{}) : String{}
+    hooked-symbol ripemd160{}(Bytes{}) : String{}
         [hook{}("KRYPTO.ripemd160")]
 ~~~
 
@@ -883,7 +883,7 @@ Compute the RIPEMD-160 hash of the input string.
 Compute the SHA256 hash of the input string.
 
 ~~~
-    hooked-symbol sha256{}(String{}) : String{}
+    hooked-symbol sha256{}(Bytes{}) : String{}
         [hook{}("KRYPTO.sha256")]
 ~~~
 
@@ -892,7 +892,7 @@ Compute the SHA256 hash of the input string.
 Compute the SHA512/256 hash of the input string, returning raw bytes.
 
 ~~~
-    hooked-symbol sha512_256raw{}(String{}) : String{}
+    hooked-symbol sha512_256raw{}(Bytes{}) : Bytes{}
         [hook{}("KRYPTO.sha512_256raw")]
 ~~~
 
@@ -901,7 +901,7 @@ Compute the SHA512/256 hash of the input string, returning raw bytes.
 Compute the SHA3-256 hash of the input string.
 
 ~~~
-    hooked-symbol sha3256{}(String{}) : String{}
+    hooked-symbol sha3256{}(Bytes{}) : String{}
         [hook{}("KRYPTO.sha3256")]
 ~~~
 
@@ -910,7 +910,7 @@ Compute the SHA3-256 hash of the input string.
 `ecdsaPubKey` takes a 32-character byte string of a private key, and returns the 64 byte hex-encoded public key.
 
 ~~~
-    hooked-symbol ecdsaPubKey{}(String{}) : String{}
+    hooked-symbol ecdsaPubKey{}(Bytes{}) : String{}
         [hook{}("KRYPTO.ecdsaPubKey")]
 ~~~
 

kore/src/Kore/Builtin/InternalBytes.hs

@@ -7,6 +7,7 @@ module Kore.Builtin.InternalBytes (
     assertSort,
     verifiers,
     builtinFunctions,
+    expectBuiltinBytes,
     asInternal,
     internalize,
     asPattern,
@@ -222,17 +223,17 @@ dotBytesVerifier =
         symbol = applicationSymbolOrAlias application
         internalBytesSort = applicationSortsResult . symbolSorts $ symbol
 
-matchBuiltinBytes :: Monad m => TermLike variable -> MaybeT m ByteString
-matchBuiltinBytes (InternalBytes_ _ byteString) = return $ ShortByteString.fromShort byteString
-matchBuiltinBytes _ = empty
+expectBuiltinBytes :: Monad m => TermLike variable -> MaybeT m ByteString
+expectBuiltinBytes (InternalBytes_ _ byteString) = return $ ShortByteString.fromShort byteString
+expectBuiltinBytes _ = empty
 
 evalBytes2String :: BuiltinAndAxiomSimplifier
 evalBytes2String =
     Builtin.functionEvaluator evalBytes2String0
   where
     evalBytes2String0 :: Builtin.Function
     evalBytes2String0 _ resultSort [_bytes] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         Encoding.decode8Bit _bytes
             & String.asPattern resultSort
             & return
@@ -258,7 +259,7 @@ evalDecodeBytes = Builtin.applicationEvaluator evalDecodeBytes0
             let Application{applicationSymbolOrAlias = symbol} = app
                 resultSort = symbolSorts symbol & applicationSortsResult
             _str <- String.expectBuiltinString decodeBytesKey _strTerm
-            _bytes <- matchBuiltinBytes _bytesTerm
+            _bytes <- expectBuiltinBytes _bytesTerm
             decodeUtf app resultSort (Text.unpack _str) _bytes
     evalDecodeBytes0 _ _ = Builtin.wrongArity decodeBytesKey
 
@@ -316,7 +317,7 @@ evalUpdate =
   where
     evalUpdate0 :: Builtin.Function
     evalUpdate0 _ resultSort [_bytes, _index, _value] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _index <- fromInteger <$> Int.expectBuiltinInt updateKey _index
         _value <- fromInteger <$> Int.expectBuiltinInt updateKey _value
         let result
@@ -336,7 +337,7 @@ evalGet =
   where
     evalGet0 :: Builtin.Function
     evalGet0 _ resultSort [_bytes, _index] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _index <- fromInteger <$> Int.expectBuiltinInt getKey _index
         let result
                 | _index >= 0
@@ -355,7 +356,7 @@ evalSubstr =
   where
     evalSubstr0 :: Builtin.Function
     evalSubstr0 _ resultSort [_bytes, _start, _end] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _start <- fromInteger <$> Int.expectBuiltinInt substrKey _start
         _end <- fromInteger <$> Int.expectBuiltinInt substrKey _end
         let result
@@ -376,9 +377,9 @@ evalReplaceAt =
   where
     evalReplaceAt0 :: Builtin.Function
     evalReplaceAt0 _ resultSort [_bytes, _index, _new] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _index <- fromInteger <$> Int.expectBuiltinInt replaceAtKey _index
-        _new <- matchBuiltinBytes _new
+        _new <- expectBuiltinBytes _new
         go _bytes _index _new
             & maybe (Pattern.bottomOf resultSort) (asPattern resultSort)
             & return
@@ -403,7 +404,7 @@ evalPadRight =
   where
     evalPadRight0 :: Builtin.Function
     evalPadRight0 _ resultSort [_bytes, _length, _value] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _length <- fromInteger <$> Int.expectBuiltinInt padRightKey _length
         _value <- fromInteger <$> Int.expectBuiltinInt padRightKey _value
         (return . asPattern resultSort) (go _bytes _length _value)
@@ -421,7 +422,7 @@ evalPadLeft =
   where
     evalPadLeft0 :: Builtin.Function
     evalPadLeft0 _ resultSort [_bytes, _length, _value] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         _length <- fromInteger <$> Int.expectBuiltinInt padLeftKey _length
         _value <- fromInteger <$> Int.expectBuiltinInt padLeftKey _value
         return . asPattern resultSort $ go _bytes _length _value
@@ -439,7 +440,7 @@ evalReverse =
   where
     evalReverse0 :: Builtin.Function
     evalReverse0 _ resultSort [_bytes] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         ByteString.reverse _bytes
             & asPattern resultSort
             & return
@@ -451,7 +452,7 @@ evalLength =
   where
     evalLength0 :: Builtin.Function
     evalLength0 _ resultSort [_bytes] = do
-        _bytes <- matchBuiltinBytes _bytes
+        _bytes <- expectBuiltinBytes _bytes
         toInteger (ByteString.length _bytes)
             & Int.asPattern resultSort
             & return
@@ -463,8 +464,8 @@ evalConcat =
   where
     evalConcat0 :: Builtin.Function
     evalConcat0 _ resultSort [_lhs, _rhs] = do
-        _lhs <- matchBuiltinBytes _lhs
-        _rhs <- matchBuiltinBytes _rhs
+        _lhs <- expectBuiltinBytes _lhs
+        _rhs <- expectBuiltinBytes _rhs
         _lhs <> _rhs
             & asPattern resultSort
             & return
@@ -517,7 +518,7 @@ evalBytes2int =
     evalBytes2int0 _ resultSort [bytes, _end, _sign] = do
         _end <- matchEndianness _end
         _sign <- matchSignedness _sign
-        bytes' <- matchBuiltinBytes bytes
+        bytes' <- expectBuiltinBytes bytes
         bytes2int bytes' _end _sign
             & Int.asPattern resultSort
             & return

kore/src/Kore/Builtin/Krypto.hs

@@ -49,7 +49,6 @@ import Data.ByteString (
     ByteString,
  )
 import Data.ByteString qualified as ByteString
-import Data.Char as Char
 import Data.HashMap.Strict qualified as HashMap
 import Data.String (
     IsString,
@@ -58,18 +57,17 @@ import Data.String (
 import Data.Text (
     Text,
  )
-import Data.Text qualified as Text
 import Data.Word (
     Word8,
  )
 import Foreign (alloca, allocaBytes, peek, poke)
 import Kore.Builtin.Builtin qualified as Builtin
 import Kore.Builtin.Encoding (
     decode8Bit,
-    encode8Bit,
     toBase16,
  )
 import Kore.Builtin.Int qualified as Int
+import Kore.Builtin.InternalBytes qualified as InternalBytes
 import Kore.Builtin.String qualified as String
 import Kore.Simplify.Simplify (
     BuiltinAndAxiomSimplifier,
@@ -127,28 +125,28 @@ symbolVerifiers =
         , (hashSha256Key, verifyHashFunction)
         , (sha3256Key, verifyHashFunction)
         , (hashSha3_256Key, verifyHashFunction)
-        , (sha512_256RawKey, verifyHashFunction)
+        , (sha512_256RawKey, verifyHashFunctionRaw)
         , (ripemd160Key, verifyHashFunction)
         , (hashRipemd160Key, verifyHashFunction)
         , (ecdsaPubKey, verifyHashFunction)
         ,
             ( ecdsaRecoverKey
             , Builtin.verifySymbol
-                String.assertSort
-                [ String.assertSort
+                InternalBytes.assertSort
+                [ InternalBytes.assertSort
                 , Int.assertSort
-                , String.assertSort
-                , String.assertSort
+                , InternalBytes.assertSort
+                , InternalBytes.assertSort
                 ]
             )
         ,
             ( secp256k1EcdsaRecoverKey
             , Builtin.verifySymbol
-                String.assertSort
-                [ String.assertSort
+                InternalBytes.assertSort
+                [ InternalBytes.assertSort
                 , Int.assertSort
-                , String.assertSort
-                , String.assertSort
+                , InternalBytes.assertSort
+                , InternalBytes.assertSort
                 ]
             )
         ]
@@ -171,11 +169,14 @@ builtinFunctions key
     | otherwise = Nothing
 
 verifyHashFunction :: Builtin.SymbolVerifier
-verifyHashFunction = Builtin.verifySymbol String.assertSort [String.assertSort]
+verifyHashFunction = Builtin.verifySymbol String.assertSort [InternalBytes.assertSort]
+
+verifyHashFunctionRaw :: Builtin.SymbolVerifier
+verifyHashFunctionRaw = Builtin.verifySymbol InternalBytes.assertSort [InternalBytes.assertSort]
 
 {- | A function evaluator for builtin hash function hooks.
 
-The symbol's argument must be a string which will be interpreted as a sequence
+The symbol's argument is a byte string which will be interpreted as a raw sequence
 of 8-bit bytes. The result is the hash as a string in big-endian base-16
 encoding.
 -}
@@ -191,17 +192,16 @@ evalHashFunction context algorithm =
   where
     evalHashFunctionWorker :: Builtin.Function
     evalHashFunctionWorker _ resultSort [input] = do
-        str <- String.expectBuiltinString context input
-        let bytes = encode8Bit str
-            digest = hashWith algorithm bytes
+        bytes <- InternalBytes.expectBuiltinBytes input
+        let digest = hashWith algorithm bytes
             result = fromString (show digest)
         return (String.asPattern resultSort result)
     evalHashFunctionWorker _ _ _ = Builtin.wrongArity context
 
 {- | A function evaluator for builtin hash function hooks.
 
-The symbol's argument must be a string which will be interpreted as a sequence
-of 8-bit bytes. The result is the hash as raw string.
+The symbol's argument is a byte string which will be interpreted as a raw sequence
+of 8-bit bytes. The result is the hash as a raw byte string.
 -}
 evalHashFunctionRaw ::
     HashAlgorithm algorithm =>
@@ -215,9 +215,8 @@ evalHashFunctionRaw context algorithm =
   where
     evalHashFunctionWorker :: Builtin.Function
     evalHashFunctionWorker _ resultSort [input] = do
-        str <- String.expectBuiltinString context input
-        let bytes = encode8Bit str
-            digest = hashWith algorithm bytes
+        bytes <- InternalBytes.expectBuiltinBytes input
+        let digest = hashWith algorithm bytes
             result = decode8Bit digest
         return (String.asPattern resultSort result)
     evalHashFunctionWorker _ _ _ = Builtin.wrongArity context
@@ -247,7 +246,7 @@ evalECDSAPubKey =
   where
     evalWorker :: Builtin.Function
     evalWorker _ resultSort [input] = do
-        sec_key <- encode8Bit <$> String.expectBuiltinString ecdsaPubKey input
+        sec_key <- InternalBytes.expectBuiltinBytes input
         return $
             String.asPattern resultSort $
                 if ByteString.length sec_key /= 32
@@ -276,19 +275,14 @@ evalECDSARecover =
     eval0 :: Builtin.Function
     eval0 _ resultSort [messageHash0, v0, r0, s0] = do
         messageHash <-
-            string2Integer . Text.unpack
-                <$> String.expectBuiltinString "" messageHash0
+            bstring2Integer <$> InternalBytes.expectBuiltinBytes messageHash0
         v <- Int.expectBuiltinInt "" v0
         r <-
-            string2Integer . Text.unpack
-                <$> String.expectBuiltinString "" r0
+            bstring2Integer <$> InternalBytes.expectBuiltinBytes r0
         s <-
-            string2Integer . Text.unpack
-                <$> String.expectBuiltinString "" s0
+            bstring2Integer <$> InternalBytes.expectBuiltinBytes s0
         pad 64 0 (signatureToKey messageHash r s v)
-            & byteString2String
-            & Text.pack
-            & String.asPattern resultSort
+            & InternalBytes.asPattern resultSort
             & return
     eval0 _ _ _ = Builtin.wrongArity ecdsaRecoverKey
 
@@ -408,19 +402,6 @@ encodePoint compressed (Point x y)
             ]
 encodePoint _ _ = error "Should never obtain point-at-infinity here!"
 
-{- | Converts a 'String' to a 'ByteString'.
-
-Will error if the string contains any characters above @\255@.
--}
-byteString2String :: ByteString -> String
-byteString2String = map (chr . fromIntegral) . ByteString.unpack
-
-{- | Interprets a 'String' as an 'Integer' in big-endian unsigned
- representation.
--}
-string2Integer :: String -> Integer
-string2Integer = bstring2Integer . ByteString.pack . map (fromIntegral . ord)
-
 {- | Interprets a 'ByteString' as an 'Integer' in big-endian unsigned
  representation.
 -}