From f84c925c08fb8cfbbf7a25d8e673b7ad0a5cdbe0 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 5 Dec 2019 18:26:46 -0600 Subject: [PATCH] Use Bytes for the Haskell backend (#596) * Makefile: separate tangles * data: separate tanglers for bytes/nobytes * Use Bytes for Haskell backend * test totalSupply spec * data.md: #range is substrBytes * evm.md: #computeValidJumpDests: No owise * TMP sum-to-n-spec.k: Remove edsl.k * revert #range impl * Revert "test totalSupply spec" This reverts commit 5f0e96585510d2f0a64f21ff9b95d2e0d5397a49. * Restore deps/k * deps/k: Use BYTES-HOOKED with Haskell backend * optimize #parseByteStack function * add functional to alignHexString * fix merkle-spec.k * update .nobytes version of #parseHexBytes * update search expected output * fix typo * fix side condition --- Makefile | 11 ++-- asm.md | 4 +- data.md | 56 ++++++++++--------- evm.md | 10 ++-- .../branching-invalid.evm.search-expected | 10 ++-- .../search/straight-line.evm.search-expected | 10 ++-- tests/specs/examples/sum-to-n-spec.k | 2 - tests/specs/functional/merkle-spec.k | 26 ++++----- 8 files changed, 67 insertions(+), 62 deletions(-) diff --git a/Makefile b/Makefile index 569c96d459..798c16dc36 100644 --- a/Makefile +++ b/Makefile @@ -180,9 +180,10 @@ llvm_kompiled := $(llvm_dir)/$(MAIN_DEFN_FILE)-kompiled/interpreter # Tangle definition from *.md files -concrete_tangle := .k:not(.node):not(.symbolic),.standalone,.concrete -symbolic_tangle := .k:not(.node):not(.concrete),.standalone,.symbolic -node_tangle := .k:not(.standalone):not(.symbolic),.node,.concrete +concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes),.standalone,.concrete,.bytes +java_tangle := .k:not(.node):not(.concrete):not(.bytes),.standalone,.symbolic,.nobytes +haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes),.standalone,.symbolic,.bytes +node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes),.node,.concrete,.bytes defn: $(defn_files) ocaml-defn: $(ocaml_files) @@ -202,11 +203,11 @@ $(llvm_dir)/%.k: %.md $(TANGLER) $(java_dir)/%.k: %.md $(TANGLER) @mkdir -p $(java_dir) - pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(symbolic_tangle)" $< > $@ + pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(java_tangle)" $< > $@ $(haskell_dir)/%.k: %.md $(TANGLER) @mkdir -p $(haskell_dir) - pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(symbolic_tangle)" $< > $@ + pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(haskell_tangle)" $< > $@ $(node_dir)/%.k: %.md $(TANGLER) @mkdir -p $(node_dir) diff --git a/asm.md b/asm.md index d93d34967b..99a9858cea 100644 --- a/asm.md +++ b/asm.md @@ -40,7 +40,7 @@ Operator `#revOps` can be used to reverse a program. // ------------------------------------------------------- ``` -```{.k .symbolic} +```{.k .nobytes} syntax ByteArray ::= #asmOpCodes ( OpCodes, ByteArray ) [function, klabel(#asmOpCodesAux)] // ------------------------------------------------------------------------------------------ rule #asmOpCodes( OPS ) => #asmOpCodes(#revOps(OPS), .ByteArray) @@ -50,7 +50,7 @@ Operator `#revOps` can be used to reverse a program. rule #asmOpCodes( .OpCodes, WS ) => WS ``` -```{.k .concrete} +```{.k .bytes} syntax ByteArray ::= #asmOpCodes ( OpCodes, StringBuffer ) [function, klabel(#asmOpCodesAux)] // --------------------------------------------------------------------------------------------- rule #asmOpCodes( OPS ) => #asmOpCodes(OPS, .StringBuffer) diff --git a/data.md b/data.md index e76582f055..867715ca6f 100644 --- a/data.md +++ b/data.md @@ -40,7 +40,7 @@ module EVM-DATA imports JSON ``` -```{.k .concrete} +```{.k .concrete .bytes} imports BYTES ``` @@ -517,10 +517,10 @@ The local memory of execution is a byte-array (instead of a word-array). - `#sizeByteArray` calculates the size of a `ByteArray`. - `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `WordStack` is the correct size. -```{.k .concrete} +```{.k .bytes} syntax ByteArray = Bytes - syntax ByteArray ::= ".ByteArray" [function] - // -------------------------------------------- + syntax ByteArray ::= ".ByteArray" [function, functional] + // -------------------------------------------------------- rule .ByteArray => .Bytes syntax Int ::= #asWord ( ByteArray ) [function, smtlib(asWord)] @@ -562,7 +562,7 @@ The local memory of execution is a byte-array (instead of a word-array). rule #padToWidth(N, WS) => padLeftBytes(WS, N, 0) ``` -```{.k .symbolic} +```{.k .nobytes} syntax ByteArray = WordStack syntax ByteArray ::= ".ByteArray" [function] // -------------------------------------------- @@ -721,7 +721,7 @@ We are using the polymorphic `Map` sort for these word maps. - `WM [ N := WS ]` assigns a contiguous chunk of $WM$ to $WS$ starting at position $W$. - `#range(M, START, WIDTH)` reads off $WIDTH$ elements from $WM$ beginning at position $START$ (padding with zeros as needed). -```{.k .concrete} +```{.k .bytes} syntax Map ::= Map "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)] // ------------------------------------------------------------------------------- rule WM[ N := WS ] => WM [ N := WS, 0, #sizeByteArray(WS) ] @@ -739,7 +739,7 @@ We are using the polymorphic `Map` sort for these word maps. rule #range(WM, I, J, WIDTH, WS) => #range(WM, I +Int 1, J +Int 1, WIDTH, WS [ J <- {WM[I] orDefault 0}:>Int ]) [owise] ``` -```{.k .symbolic} +```{.k .nobytes} syntax Map ::= Map "[" Int ":=" ByteArray "]" [function, functional] // -------------------------------------------------------------------- rule [mapWriteBytes.base]: WM[ N := .WordStack ] => WM @@ -788,6 +788,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `ByteArray`s, and `M - `#parseHexWord` interprets a string as a single hex-encoded `Word`. - `#parseHexBytes` interprets a string as a hex-encoded stack of bytes. +- `#alignHexString` makes sure that the length of a (hex)string is even. - `#parseByteStack` interprets a string as a hex-encoded stack of bytes, but makes sure to remove the leading "0x". - `#parseByteStackRaw` casts a string as a stack of bytes, ignoring any encoding. - `#parseWordStack` interprets a JSON list as a stack of `Word`. @@ -805,36 +806,41 @@ These parsers can interperet hex-encoded strings as `Int`s, `ByteArray`s, and `M rule #parseWord("") => 0 rule #parseWord(S) => #parseHexWord(S) requires lengthString(S) >=Int 2 andBool substrString(S, 0, 2) ==String "0x" rule #parseWord(S) => String2Int(S) [owise] + + syntax String ::= #alignHexString ( String ) [function, functional] + // ------------------------------------------------------------------- + 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 ``` -```{.k .concrete} +```{.k .bytes} syntax ByteArray ::= #parseHexBytes ( String ) [function] - | #parseByteStack ( String ) [function] + | #parseHexBytesAux ( String ) [function] + | #parseByteStack ( String ) [function, memo] | #parseByteStackRaw ( String ) [function] - // ------------------------------------------------------------- + // ------------------------------------------------------------------- rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", "")) - rule #parseHexBytes("") => .ByteArray - rule #parseHexBytes(S) => #parseHexBytes("0" +String S) - requires notBool lengthString(S) modInt 2 ==Int 0 - rule #parseHexBytes(S) => Int2Bytes(1, #parseHexWord(substrString(S, 0, 2)), BE) +Bytes #parseHexBytes(substrString(S, 2, lengthString(S))) - requires lengthString(S) modInt 2 ==Int 0 - andBool lengthString(S) >Int 0 + + rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S)) + rule #parseHexBytesAux("") => .ByteArray + rule #parseHexBytesAux(S) => Int2Bytes(1, String2Base(substrString(S, 0, 2), 16), BE) +Bytes #parseHexBytesAux(substrString(S, 2, lengthString(S))) + requires lengthString(S) >=Int 2 rule #parseByteStackRaw(S) => String2Bytes(S) ``` -```{.k .symbolic} +```{.k .nobytes} syntax ByteArray ::= #parseHexBytes ( String ) [function] + | #parseHexBytesAux ( String ) [function] | #parseByteStack ( String ) [function] | #parseByteStackRaw ( String ) [function] // ------------------------------------------------------------- rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", "")) - rule #parseHexBytes("") => .WordStack - rule #parseHexBytes(S) => #parseHexBytes("0" +String S) - requires notBool lengthString(S) modInt 2 ==Int 0 - rule #parseHexBytes(S) => #parseHexWord(substrString(S, 0, 2)) : #parseHexBytes(substrString(S, 2, lengthString(S))) - requires lengthString(S) modInt 2 ==Int 0 - andBool lengthString(S) >Int 0 + + rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S)) + rule #parseHexBytesAux("") => .WordStack + rule #parseHexBytesAux(S) => #parseHexWord(substrString(S, 0, 2)) : #parseHexBytesAux(substrString(S, 2, lengthString(S))) + requires lengthString(S) >=Int 2 rule #parseByteStackRaw(S) => ordChar(substrString(S, 0, 1)) : #parseByteStackRaw(substrString(S, 1, lengthString(S))) requires lengthString(S) >=Int 1 rule #parseByteStackRaw("") => .WordStack @@ -860,13 +866,13 @@ We need to interperet a `ByteArray` as a `String` again so that we can call `Kec - `#unparseByteStack` turns a stack of bytes (as a `ByteArray`) into a `String`. - `#padByte` ensures that the `String` interperetation of a `Int` is wide enough. -```{.k .concrete} +```{.k .bytes} syntax String ::= #unparseByteStack ( ByteArray ) [function, klabel(unparseByteStack), symbol] // ---------------------------------------------------------------------------------------------- rule #unparseByteStack(WS) => Bytes2String(WS) ``` -```{.k .symbolic} +```{.k .nobytes} syntax String ::= #unparseByteStack ( ByteArray ) [function, klabel(unparseByteStack), symbol] | #unparseByteStack ( ByteArray , StringBuffer ) [function, klabel(#unparseByteStackAux)] // --------------------------------------------------------------------------------------------------------- diff --git a/evm.md b/evm.md index 52e292d23e..7b06972d8c 100644 --- a/evm.md +++ b/evm.md @@ -1374,16 +1374,16 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, .List) ``` -```{.k .symbolic} +```{.k .nobytes} rule #computeValidJumpDests(.WordStack, _, RESULT) => List2Set(RESULT) rule #computeValidJumpDests(91 : WS, I, RESULT) => #computeValidJumpDests(WS, I +Int 1, ListItem(I) RESULT) rule #computeValidJumpDests(W : WS, I, RESULT) => #computeValidJumpDests(#drop(#widthOpCode(W), W : WS), I +Int #widthOpCode(W), RESULT) requires W =/=Int 91 ``` -```{.k .concrete} +```{.k .bytes} rule #computeValidJumpDests(PGM, I, RESULT) => List2Set(RESULT) requires I >=Int #sizeByteArray(PGM) rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int 1, ListItem(I) RESULT) requires I #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) [owise] + rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) requires I N -Int (N /Int 64) ``` -```{.k .symbolic} +```{.k .nobytes} syntax Int ::= G0 ( Schedule , ByteArray , Bool ) [function] // ------------------------------------------------------------ rule G0(SCHED, .WordStack, true) => Gtxcreate < SCHED > @@ -2190,7 +2190,7 @@ There are several helpers for calculating gas (most of them also specified in th rule G0(SCHED, N : REST, ISCREATE) => Gtxdatanonzero < SCHED > +Int G0(SCHED, REST, ISCREATE) requires N =/=Int 0 ``` -```{.k .concrete} +```{.k .bytes} syntax Int ::= G0 ( Schedule , ByteArray , Bool ) [function] | G0 ( Schedule , ByteArray , Int , Int ) [function, klabel(G0data)] | G0 ( Schedule , Bool ) [function, klabel(G0base)] diff --git a/tests/interactive/search/branching-invalid.evm.search-expected b/tests/interactive/search/branching-invalid.evm.search-expected index f42de8da97..d42220cf3a 100644 --- a/tests/interactive/search/branching-invalid.evm.search-expected +++ b/tests/interactive/search/branching-invalid.evm.search-expected @@ -32,7 +32,7 @@ _0 #Equals - .WordStack + b"" } #And @@ -65,7 +65,7 @@ #Equals - 96 : 3 : 96 : 4 : 1 : 96 : 8 : 20 : 96 : 12 : 87 : 254 : 91 : 0 : .WordStack + b"6003600401600814600c57fe5b00" SetItem ( 12 ) @@ -77,7 +77,7 @@ .Account - .WordStack + b"" 0 @@ -172,7 +172,7 @@ 0 - .WordStack + b"" 0 @@ -190,7 +190,7 @@ 0 - .WordStack + b"" 0 diff --git a/tests/interactive/search/straight-line.evm.search-expected b/tests/interactive/search/straight-line.evm.search-expected index 89b77e5227..1c4b89b7de 100644 --- a/tests/interactive/search/straight-line.evm.search-expected +++ b/tests/interactive/search/straight-line.evm.search-expected @@ -32,7 +32,7 @@ _0 #Equals - .WordStack + b"" } #And @@ -65,7 +65,7 @@ #Equals - 127 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 3 : 127 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 4 : 1 : 254 : .WordStack + b"7f00000000000000000000000000000000000000000000000000000000000000037f000000000000000000000000000000000000000000000000000000000000000401fe" .Set @@ -77,7 +77,7 @@ .Account - .WordStack + b"" 0 @@ -172,7 +172,7 @@ 0 - .WordStack + b"" 0 @@ -190,7 +190,7 @@ 0 - .WordStack + b"" 0 diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k index 042fc4225d..6b791f39d6 100644 --- a/tests/specs/examples/sum-to-n-spec.k +++ b/tests/specs/examples/sum-to-n-spec.k @@ -1,8 +1,6 @@ requires "asm.k" -requires "edsl.k" module VERIFICATION - imports EDSL imports EVM-ASSEMBLY rule #sizeWordStack ( WS , N:Int ) diff --git a/tests/specs/functional/merkle-spec.k b/tests/specs/functional/merkle-spec.k index 07efe6d1bb..b514a7b55d 100644 --- a/tests/specs/functional/merkle-spec.k +++ b/tests/specs/functional/merkle-spec.k @@ -14,31 +14,31 @@ endmodule module MERKLE-SPEC imports VERIFICATION - rule runMerkle ( MerkleUpdate( .MerkleTree, .WordStack, VALUE ) ) - => doneMerkle( MerkleLeaf( .WordStack, VALUE ) ) + rule runMerkle ( MerkleUpdate( .MerkleTree, .ByteArray, VALUE ) ) + => doneMerkle( MerkleLeaf( .ByteArray, VALUE ) ) // Update on MerkleLeaf - rule runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 7 : .WordStack, V ) ) - => doneMerkle( MerkleLeaf ( 6 : 7 : .WordStack, V ) ) + rule runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0607"), V ) ) + => doneMerkle( MerkleLeaf ( #parseByteStack("0x0607"), V ) ) - rule runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 8 : .WordStack, _ ) ) - => doneMerkle( MerkleExtension( 6 : .WordStack, _ ) ) + rule runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0608"), _ ) ) + => doneMerkle( MerkleExtension( #parseByteStack("0x06"), _ ) ) - rule runMerkle ( MerkleUpdate( MerkleLeaf( 5 : .WordStack, _ ), 6 : .WordStack, _ ) ) + rule runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x05"), _ ), #parseByteStack("0x06"), _ ) ) => doneMerkle( MerkleBranch( _, _ ) ) // Update on MerkleExtension - rule runMerkle ( MerkleUpdate( MerkleExtension( 6 : .WordStack, .MerkleTree ), 6 : .WordStack, V ) ) - => doneMerkle( MerkleExtension( 6 : .WordStack, MerkleLeaf( .WordStack, V ) ) ) + rule runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x06"), .MerkleTree ), #parseByteStack("0x06"), V ) ) + => doneMerkle( MerkleExtension( #parseByteStack("0x06"), MerkleLeaf( .ByteArray, V ) ) ) - rule runMerkle ( MerkleUpdate( MerkleExtension( 7 : .WordStack, _ ), 6 : .WordStack, _ ) ) + rule runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x07"), _ ), #parseByteStack("0x06"), _ ) ) => doneMerkle( MerkleBranch( _, _ ) ) - rule runMerkle ( MerkleUpdate( MerkleExtension( 7 : 8 : .WordStack, _ ), 7 : 9 : .WordStack, _ ) ) - => doneMerkle( MerkleExtension( 7 : .WordStack, MerkleBranch( _, _ ) ) ) + rule runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x0708"), _ ), #parseByteStack("0x0709"), _ ) ) + => doneMerkle( MerkleExtension( #parseByteStack("0x07"), MerkleBranch( _, _ ) ) ) // Update on MerkleBranch - rule runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .WordStack, V ) ) + rule runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .ByteArray, V ) ) => doneMerkle( MerkleBranch( M, V ) ) rule runMerkle ( .MerkleBranch )