Merge remote-tracking branch 'origin/master' into _update-deps/runtim…

…everification/k

.github/workflows/release.yml

@@ -42,7 +42,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - name: Check out code
         uses: actions/checkout@v3
@@ -76,7 +76,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - name: Check out code
         uses: actions/checkout@v3
@@ -110,7 +110,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - name: Check out code
         uses: actions/checkout@v3

.github/workflows/test.yml

@@ -156,7 +156,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - uses: actions/checkout@v3
         with:
@@ -196,7 +196,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - uses: actions/checkout@v3
         with:
@@ -239,7 +239,7 @@ jobs:
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes z3
+          sudo apt install --yes z3 libsecp256k1-dev
 
       - uses: actions/checkout@v3
         with:

docs/hooks.md

@@ -905,6 +905,15 @@ Compute the SHA3-256 hash of the input string.
         [hook{}("KRYPTO.sha3256")]
 ~~~
 
+### KRYPTO.ecdsaPubKey
+
+`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{}
+        [hook{}("KRYPTO.ecdsaPubKey")]
+~~~
+
 ## BYTES
 
 Represents a sequence of bytes with update/get/padding operations as well as

flake.nix

@@ -116,7 +116,7 @@
               };
             };
             nativeBuildInputs = with nixpkgs.legacyPackages.${pkgs.system};
-              [ nixpkgs-fmt ]
+              [ nixpkgs-fmt secp256k1 ]
               ++ lib.optional (pkgs.system == "aarch64-darwin") pkgs.llvm_12;
           };
 

kore/kore.cabal

@@ -153,6 +153,7 @@ common library
   build-depends: process >=1.6
   build-depends: profunctors >=5.3
   build-depends: recursion-schemes >=5.1
+  build-depends: secp256k1-haskell>=0.6
   build-depends: semialign >=1
   build-depends: sqlite-simple >=0.4
   build-depends: stm >=2.5

kore/src/Kore/Builtin/Krypto.hs

@@ -43,6 +43,7 @@ import Crypto.Hash (
  )
 import Crypto.PubKey.ECC.Prim
 import Crypto.PubKey.ECC.Types
+import Crypto.Secp256k1.Internal qualified as Secp256k1
 import Data.Bits
 import Data.ByteString (
     ByteString,
@@ -61,27 +62,32 @@ 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.String qualified as String
 import Kore.Simplify.Simplify (
     BuiltinAndAxiomSimplifier,
  )
 import Prelude.Kore
+import System.IO.Unsafe (unsafePerformIO)
 
 keccak256Key
     , ecdsaRecoverKey
+    , ecdsaPubKey
     , sha256Key
     , sha512_256RawKey
     , sha3256Key
     , ripemd160Key ::
         IsString s => s
 keccak256Key = "KRYPTO.keccak256"
 ecdsaRecoverKey = "KRYPTO.ecdsaRecover"
+ecdsaPubKey = "KRYPTO.ecdsaPubKey"
 sha256Key = "KRYPTO.sha256"
 sha512_256RawKey = "KRYPTO.sha512_256raw"
 sha3256Key = "KRYPTO.sha3256"
@@ -124,6 +130,7 @@ symbolVerifiers =
         , (sha512_256RawKey, verifyHashFunction)
         , (ripemd160Key, verifyHashFunction)
         , (hashRipemd160Key, verifyHashFunction)
+        , (ecdsaPubKey, verifyHashFunction)
         ,
             ( ecdsaRecoverKey
             , Builtin.verifySymbol
@@ -159,6 +166,7 @@ builtinFunctions key
     | key == ripemd160Key = Just evalRipemd160
     | key == hashRipemd160Key = Just evalRipemd160
     | key == ecdsaRecoverKey = Just evalECDSARecover
+    | key == ecdsaPubKey = Just evalECDSAPubKey
     | key == secp256k1EcdsaRecoverKey = Just evalECDSARecover
     | otherwise = Nothing
 
@@ -229,6 +237,38 @@ evalSha3256 = evalHashFunction sha3256Key SHA3_256
 evalRipemd160 :: BuiltinAndAxiomSimplifier
 evalRipemd160 = evalHashFunction ripemd160Key RIPEMD160
 
+secp256k1Ctx :: Secp256k1.Ctx
+secp256k1Ctx = unsafePerformIO $ Secp256k1.contextCreate Secp256k1.sign
+{-# NOINLINE secp256k1Ctx #-}
+
+evalECDSAPubKey :: BuiltinAndAxiomSimplifier
+evalECDSAPubKey =
+    Builtin.functionEvaluator evalWorker
+  where
+    evalWorker :: Builtin.Function
+    evalWorker _ resultSort [input] = do
+        sec_key <- encode8Bit <$> String.expectBuiltinString ecdsaPubKey input
+        return $
+            String.asPattern resultSort $
+                if ByteString.length sec_key /= 32
+                    then ""
+                    else unsafePerformIO $ Secp256k1.unsafeUseByteString sec_key $ \(sec_key_ptr, _) -> allocaBytes 64 $ \pub_key_ptr -> do
+                        createdKeySuccessfully <-
+                            Secp256k1.isSuccess <$> Secp256k1.ecPubKeyCreate secp256k1Ctx pub_key_ptr sec_key_ptr
+                        if not createdKeySuccessfully
+                            then pure ""
+                            else alloca $ \len_ptr -> allocaBytes 65 $ \out_ptr -> do
+                                poke len_ptr 65
+                                serializedKeySuccessfully <-
+                                    Secp256k1.isSuccess
+                                        <$> Secp256k1.ecPubKeySerialize secp256k1Ctx out_ptr len_ptr pub_key_ptr Secp256k1.uncompressed
+                                if not serializedKeySuccessfully
+                                    then pure ""
+                                    else do
+                                        final_len <- peek len_ptr
+                                        toBase16 . ByteString.tail <$> Secp256k1.packByteString (out_ptr, final_len)
+    evalWorker _ _ _ = Builtin.wrongArity ecdsaPubKey
+
 evalECDSARecover :: BuiltinAndAxiomSimplifier
 evalECDSARecover =
     Builtin.functionEvaluator eval0

test/ecdsa/Makefile

@@ -0,0 +1,3 @@
+DEF = ecdsa
+include $(CURDIR)/../include.mk
+KOMPILE_OPTS += --hook-namespaces KRYPTO

test/ecdsa/addr1.ecdsa

@@ -0,0 +1 @@
+#unparseData(#addrFromPrivateKey("0x2b8ba85ff7f2c7fa62cddb20ae40ef2553b9fdbff086f60d1647ecaab15af867"), 20)

test/ecdsa/addr1.ecdsa.out.golden

@@ -0,0 +1,3 @@
+<k>
+  "0xd308979bf428e38b458a99da348e28933a4cddb1" ~> .
+</k>

test/ecdsa/addr2.ecdsa

@@ -0,0 +1 @@
+#unparseData(#addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000001"), 20)

test/ecdsa/addr2.ecdsa.out.golden

@@ -0,0 +1,3 @@
+<k>
+  "0x7e5f4552091a69125d5dfcb7b8c2659029395bdf" ~> .
+</k>

test/ecdsa/addr3.ecdsa

@@ -0,0 +1 @@
+#unparseData(#addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000002"), 20)

test/ecdsa/addr3.ecdsa.out.golden

@@ -0,0 +1,3 @@
+<k>
+  "0x2b5ad5c4795c026514f8317c7a215e218dccd6cf" ~> .
+</k>

test/ecdsa/ecdsa.k

@@ -0,0 +1,85 @@
+module ECDSA
+    imports INT
+    imports BYTES
+    imports STRING
+    imports BOOL
+
+    syntax String ::= Hex2Raw ( String ) [function]
+                    | Keccak256 ( String ) [function, hook(KRYPTO.keccak256)]
+                    | ECDSAPubKey ( String ) [function, hook(KRYPTO.ecdsaPubKey)]
+ // -----------------------------------------------
+    rule Hex2Raw ( S ) => #unparseByteStack( #parseByteStack ( S ) )
+
+    syntax Int ::= #addrFromPrivateKey ( String ) [function, klabel(addrFromPrivateKey)]
+ // ------------------------------------------------------------------------------------
+    rule [addrFromPrivateKey]: #addrFromPrivateKey ( KEY ) => #addr( #parseHexWord( Keccak256 ( Hex2Raw ( ECDSAPubKey( Hex2Raw ( KEY ) ) ) ) ) )
+
+    syntax Int ::= #parseHexWord ( String ) [function]
+ // --------------------------------------------------
+    rule #parseHexWord("")   => 0
+    rule #parseHexWord("0x") => 0
+    rule #parseHexWord(S)    => String2Base(replaceAll(S, "0x", ""), 16) requires (S =/=String "") andBool (S =/=String "0x")
+
+    syntax Bytes ::= #parseByteStack   ( String ) [function, memo]
+                   | #parseHexBytes    ( String ) [function]
+                   | #parseHexBytesAux ( String ) [function]
+ // --------------------------------------------------------
+    rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", ""))
+
+    rule #parseHexBytes(S)  => #parseHexBytesAux(#alignHexString(S))
+    rule #parseHexBytesAux("") => .Bytes
+    rule #parseHexBytesAux(S)  => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE)
+      requires lengthString(S) >=Int 2
+
+    syntax String ::= #alignHexString ( String ) [function, total]
+ // --------------------------------------------------------------
+    rule #alignHexString(S) => S             requires         lengthString(S) modInt 2 ==Int 0
+    rule #alignHexString(S) => "0" +String S requires notBool lengthString(S) modInt 2 ==Int 0
+
+    syntax String ::= #unparseByteStack ( Bytes ) [function, klabel(unparseByteStack), symbol]
+ // ------------------------------------------------------------------------------------------
+    rule #unparseByteStack(WS) => Bytes2String(WS)
+
+    syntax String ::= #unparseData      ( Int, Int  ) [function]
+                    | #unparseDataBytes ( Bytes )     [function]
+ // ------------------------------------------------------------
+    rule #unparseData( DATA, LENGTH ) => #unparseDataBytes(#padToWidth(LENGTH,#asByteStack(DATA)))
+
+    rule #unparseDataBytes( DATA ) => replaceFirst(Base2String(#asInteger(#asByteStack(1) +Bytes DATA), 16), "1", "0x")
+
+    syntax Int ::= #asInteger ( Bytes ) [function, total]
+ // -----------------------------------------------------
+    rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
+
+    syntax Bytes ::= #asByteStack ( Int ) [function, total]
+ // -------------------------------------------------------
+    rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete]
+
+    syntax Bytes ::= #padToWidth      ( Int , Bytes ) [function, total]
+                   | #padRightToWidth ( Int , Bytes ) [function, total]
+ // -------------------------------------------------------------------
+    rule                            #padToWidth(N, BS)      =>               BS        requires notBool (N >=Int 0)
+    rule [padToWidthNonEmpty]:      #padToWidth(N, BS)      =>  padLeftBytes(BS, N, 0) requires          N >=Int 0
+    rule                            #padRightToWidth(N, BS) =>               BS        requires notBool (N >=Int 0)
+    rule [padRightToWidthNonEmpty]: #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires          N >=Int 0
+
+    syntax Int ::= #addr ( Int ) [function]
+ // ---------------------------------------
+    rule #addr(W) => W %Word pow160
+
+    syntax Int ::= Int "%Word" Int [function, total]
+ // ------------------------------------------------
+    rule  _ %Word W1 => 0            requires W1  ==Int 0
+    rule W0 %Word W1 => W0 modInt W1 requires W1 =/=Int 0
+
+    syntax Int ::= "pow160" [alias] /* 2 ^Int 160 */
+ // ------------------------------------------------
+    rule pow160 => 1461501637330902918203684832716283019655932542976
+
+    configuration
+       <k> $PGM:Pgm </k>
+
+    syntax Pgm ::= Bytes | String | Int
+ // -----------------------------------
+
+endmodule