Add hook for KRYPTO.keccak256raw (#3966)

There are a few more of these `KRYPTO.&_raw` functions declared with
hook without implementation. We could add them now, or as needed later.

The `*raw` family of (hooked) functions differs from the non-`raw`
functions in that they return their result as a (byte) string of
characters instead of encoding it as a sequence of hexa-decimal digits.

Example:
* when `keccak256(X)` returns `"deadbeef"`,
* then `keccak256raw(X)` returns `"\xde\xad\xbe\xef"`, or
`"\222\173\190\239"` in the notation used by Haskell

---------

Co-authored-by: github-actions <github-actions@github.com>

Author: jberthold

kore/src/Kore/Builtin/Krypto.hs

@@ -21,6 +21,7 @@ module Kore.Builtin.Krypto (
 
     -- * Constants
     keccak256Key,
+    keccak256RawKey,
     sha256Key,
     hashSha256Key,
     sha3256Key,
@@ -79,6 +80,7 @@ import Prelude.Kore
 import System.IO.Unsafe (unsafePerformIO)
 
 keccak256Key
+    , keccak256RawKey
     , ecdsaRecoverKey
     , ecdsaPubKey
     , sha256Key
@@ -87,6 +89,7 @@ keccak256Key
     , ripemd160Key ::
         IsString s => s
 keccak256Key = "KRYPTO.keccak256"
+keccak256RawKey = "KRYPTO.keccak256raw"
 ecdsaRecoverKey = "KRYPTO.ecdsaRecover"
 ecdsaPubKey = "KRYPTO.ecdsaPubKey"
 sha256Key = "KRYPTO.sha256"
@@ -123,6 +126,7 @@ symbolVerifiers :: Builtin.SymbolVerifiers
 symbolVerifiers =
     HashMap.fromList
         [ (keccak256Key, verifyHashFunction)
+        , (keccak256RawKey, verifyHashFunctionRaw)
         , (hashKeccak256Key, verifyHashFunction)
         , (sha256Key, verifyHashFunction)
         , (hashSha256Key, verifyHashFunction)
@@ -158,6 +162,7 @@ symbolVerifiers =
 builtinFunctions :: Text -> Maybe BuiltinAndAxiomSimplifier
 builtinFunctions key
     | key == keccak256Key = Just evalKeccak
+    | key == keccak256RawKey = Just evalKeccakRaw
     | key == hashKeccak256Key = Just evalKeccak
     | key == sha256Key = Just evalSha256
     | key == hashSha256Key = Just evalSha256
@@ -227,6 +232,9 @@ evalHashFunctionRaw context algorithm =
 evalKeccak :: BuiltinAndAxiomSimplifier
 evalKeccak = evalHashFunction keccak256Key Keccak_256
 
+evalKeccakRaw :: BuiltinAndAxiomSimplifier
+evalKeccakRaw = evalHashFunctionRaw keccak256RawKey Keccak_256
+
 evalSha256 :: BuiltinAndAxiomSimplifier
 evalSha256 = evalHashFunction sha256Key SHA256
 

kore/test/Test/Kore/Builtin/Definition.hs

@@ -852,6 +852,10 @@ keccak256Symbol :: Internal.Symbol
 keccak256Symbol =
     builtinSymbol "keccak256Krypto" stringSort [bytesSort]
         & hook "KRYPTO.keccak256"
+keccak256RawSymbol :: Internal.Symbol
+keccak256RawSymbol =
+    builtinSymbol "keccak256RawKrypto" bytesSort [bytesSort]
+        & hook "KRYPTO.keccak256raw"
 sha256Symbol :: Internal.Symbol
 sha256Symbol =
     builtinSymbol "sha256Krypto" stringSort [bytesSort]
@@ -874,6 +878,9 @@ ecdsaRecoverKrypto m v r s = mkApplySymbol ecdsaRecoverSymbol [m, v, r, s]
 keccak256Krypto ::
     TermLike RewritingVariableName -> TermLike RewritingVariableName
 keccak256Krypto message = mkApplySymbol keccak256Symbol [message]
+keccak256RawKrypto ::
+    TermLike RewritingVariableName -> TermLike RewritingVariableName
+keccak256RawKrypto message = mkApplySymbol keccak256RawSymbol [message]
 sha256Krypto ::
     TermLike RewritingVariableName -> TermLike RewritingVariableName
 sha256Krypto message = mkApplySymbol sha256Symbol [message]

kore/test/Test/Kore/Builtin/Krypto.hs

@@ -5,6 +5,7 @@ module Test.Kore.Builtin.Krypto (
     test_ecdsaRecover,
     test_secp256k1EcdsaRecover,
     test_keccak256,
+    test_keccak256Raw,
     test_hashKeccak256,
     test_sha256,
     test_hashSha256,
@@ -16,12 +17,14 @@ module Test.Kore.Builtin.Krypto (
 
 import Control.Lens qualified as Lens
 import Data.ByteString.Char8 qualified as BS
+import Data.Char (chr)
 import Data.Generics.Sum.Constructors
 import Data.Proxy
 import Data.Text (
     Text,
  )
 import Data.Text qualified as Text
+import Data.Text.Encoding qualified as Text
 import GHC.TypeLits qualified as TypeLits
 import Kore.Attribute.Symbol qualified as Attribute
 import Kore.Builtin.InternalBytes qualified as InternalBytes
@@ -137,6 +140,36 @@ test_keccak256 =
                     & evaluate "KRYPTO.keccak256"
             assertEqual "" expect actual
 
+test_keccak256Raw :: [TestTree]
+test_keccak256Raw =
+    [ -- from the blockchain-k-plugin tests:
+      test
+        "foo"
+        "A\xb1\xa0\&d\x97R\xaf\x1b(\xb3\xdc)\xa1Un\xeex\x1eJL:\x1f\x7fS\xf9\x0f\xa8\&4\xde\t\x8cM"
+    , -- from above:
+      test
+        "\249\SOH\245\160\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\160\GS\204M\232\222\199]z\171\133\181g\182\204\212\SUB\211\DC2E\ESC\148\138t\DC3\240\161B\253@\212\147G\148*\220%fP\CAN\170\US\224\230\188fm\172\143\194i\DEL\249\186\160h\172|e\163\163\ESC}\139\230!\217\157/\"w\SOHX]\232s\219\218\162\181\248\215K\225Z\241\178\160V\232\US\ETB\ESC\204U\166\255\131E\230\146\192\248n[H\224\ESC\153l\173\192\SOHb/\181\227c\180!\160V\232\US\ETB\ESC\204U\166\255\131E\230\146\192\248n[H\224\ESC\153l\173\192\SOHb/\181\227c\180!\185\SOH\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\131\STX\NUL\NUL\128\131\SIB@\128\130\ETX\182B\160V\232\US\ETB\ESC\204U\166\255\131E\230\146\192\248n[H\224\ESC\153l\173\192\SOHb/\181\227c\180!\136\SOH\STX\ETX\EOT\ENQ\ACK\a\b"
+        (asBytes "417ece6e4175ae7f1bf6b8ed90b4ea22206353a7450aa10bdd5e2ba3cb2bd953")
+    , -- from above:
+      test
+        "testing"
+        (asBytes "5f16f4c7f149ac4f9510d9cf8cf384038ad348b3bcdc01915f95de12df9d1b02")
+    ]
+  where
+    asBytes = Text.decodeLatin1 . BS.pack . map (chr . read . ("0x" <>)) . groupEach2
+      where
+        groupEach2 [] = []
+        groupEach2 [_] = error "odd number of characters in input"
+        groupEach2 (a : b : rest) = [a, b] : groupEach2 rest
+
+    test input result =
+        testCase (show input) $ do
+            let expect = String.asPattern bytesSort result
+            actual <-
+                keccak256RawKrypto (InternalBytes.asInternal bytesSort (BS.pack input))
+                    & evaluate "KRYPTO.keccak256raw"
+            assertEqual "" expect actual
+
 test_hashKeccak256 :: [TestTree]
 test_hashKeccak256 =
     [ test