From 84a529c3b4768da3d95d30d782494fd821202131 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 23 Oct 2023 18:04:53 -0400 Subject: [PATCH] Update ecdsa.k --- test/ecdsa/ecdsa.k | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/test/ecdsa/ecdsa.k b/test/ecdsa/ecdsa.k index 349e8c78c0..37cda84540 100644 --- a/test/ecdsa/ecdsa.k +++ b/test/ecdsa/ecdsa.k @@ -4,15 +4,13 @@ module ECDSA imports STRING imports BOOL - syntax String ::= Hex2Raw ( String ) [function] - | Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] - | ECDSAPubKey ( String ) [function, hook(KRYPTO.ecdsaPubKey)] + syntax String ::= Keccak256 ( Bytes ) [function, hook(KRYPTO.keccak256)] + | ECDSAPubKey ( Bytes ) [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 ) ) ) ) ) ) + rule [addrFromPrivateKey]: #addrFromPrivateKey ( KEY ) => #addr( #parseHexWord( Keccak256( #parseByteStack( ECDSAPubKey( #parseByteStack( KEY ) ) ) ) ) ) syntax Int ::= #parseHexWord ( String ) [function] // -------------------------------------------------- @@ -36,10 +34,6 @@ module ECDSA 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] // ------------------------------------------------------------