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 5f0e965. * 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
runtimeverification · Dec 6, 2019 · f84c925 · f84c925
1 parent f9036d5
commit f84c925
Show file tree

Hide file tree

Showing 8 changed files with 67 additions and 62 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 <Int #sizeByteArray(PGM) andBool PGM [ I ] ==Int 91
-    rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) [owise]
+    rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) requires I <Int #sizeByteArray(PGM) andBool notBool PGM [ I ] ==Int 91
 ```
 
 ```k
@@ -2180,7 +2180,7 @@ There are several helpers for calculating gas (most of them also specified in th
     rule #allBut64th(N) => 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
@@ -32,7 +32,7 @@
     _0
   #Equals
     <output>
-      .WordStack
+      b""
     </output>
   }
 #And
@@ -65,7 +65,7 @@
   #Equals
     <callState>
       <program>
-        96 : 3 : 96 : 4 : 1 : 96 : 8 : 20 : 96 : 12 : 87 : 254 : 91 : 0 : .WordStack
+        b"6003600401600814600c57fe5b00"
       </program>
       <jumpDests>
         SetItem ( 12 )
@@ -77,7 +77,7 @@
         .Account
       </caller>
       <callData>
-        .WordStack
+        b""
       </callData>
       <callValue>
         0
@@ -172,7 +172,7 @@
         0
       </receiptsRoot>
       <logsBloom>
-        .WordStack
+        b""
       </logsBloom>
       <difficulty>
         0
@@ -190,7 +190,7 @@
         0
       </timestamp>
       <extraData>
-        .WordStack
+        b""
       </extraData>
       <mixHash>
         0

diff --git a/tests/interactive/search/straight-line.evm.search-expected b/tests/interactive/search/straight-line.evm.search-expected
@@ -32,7 +32,7 @@
     _0
   #Equals
     <output>
-      .WordStack
+      b""
     </output>
   }
 #And
@@ -65,7 +65,7 @@
   #Equals
     <callState>
       <program>
-        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"
       </program>
       <jumpDests>
         .Set
@@ -77,7 +77,7 @@
         .Account
       </caller>
       <callData>
-        .WordStack
+        b""
       </callData>
       <callValue>
         0
@@ -172,7 +172,7 @@
         0
       </receiptsRoot>
       <logsBloom>
-        .WordStack
+        b""
       </logsBloom>
       <difficulty>
         0
@@ -190,7 +190,7 @@
         0
       </timestamp>
       <extraData>
-        .WordStack
+        b""
       </extraData>
       <mixHash>
         0

diff --git 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
@@ -14,31 +14,31 @@ endmodule
 module MERKLE-SPEC
     imports VERIFICATION
 
-    rule <k> runMerkle ( MerkleUpdate( .MerkleTree, .WordStack, VALUE ) )
-          => doneMerkle( MerkleLeaf( .WordStack, VALUE ) ) </k>
+    rule <k> runMerkle ( MerkleUpdate( .MerkleTree, .ByteArray, VALUE ) )
+          => doneMerkle( MerkleLeaf( .ByteArray, VALUE ) ) </k>
 
     // Update on MerkleLeaf
-    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 7 : .WordStack, V ) )
-          => doneMerkle( MerkleLeaf ( 6 : 7 : .WordStack, V ) ) </k>
+    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0607"), V ) )
+          => doneMerkle( MerkleLeaf ( #parseByteStack("0x0607"), V ) ) </k>
 
-    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 8 : .WordStack, _ ) )
-          => doneMerkle( MerkleExtension( 6 : .WordStack, _ ) ) </k>
+    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x0607"), _ ), #parseByteStack("0x0608"), _ ) )
+          => doneMerkle( MerkleExtension( #parseByteStack("0x06"), _ ) ) </k>
 
-    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 5 : .WordStack, _ ), 6 : .WordStack, _ ) )
+    rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( #parseByteStack("0x05"), _ ), #parseByteStack("0x06"), _ ) )
           => doneMerkle( MerkleBranch( _, _ ) ) </k>
 
     // Update on MerkleExtension
-    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 6 : .WordStack, .MerkleTree ), 6 : .WordStack, V ) )
-          => doneMerkle( MerkleExtension( 6 : .WordStack, MerkleLeaf( .WordStack, V ) ) ) </k>
+    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x06"), .MerkleTree ), #parseByteStack("0x06"), V ) )
+          => doneMerkle( MerkleExtension( #parseByteStack("0x06"), MerkleLeaf( .ByteArray, V ) ) ) </k>
 
-    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 7 : .WordStack, _ ), 6 : .WordStack, _ ) )
+    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x07"), _ ), #parseByteStack("0x06"), _ ) )
           => doneMerkle( MerkleBranch( _, _ ) ) </k>
 
-    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 7 : 8 : .WordStack, _ ), 7 : 9 : .WordStack, _ ) )
-          => doneMerkle( MerkleExtension( 7 : .WordStack, MerkleBranch( _, _ ) ) ) </k>
+    rule <k> runMerkle ( MerkleUpdate( MerkleExtension( #parseByteStack("0x0708"), _ ), #parseByteStack("0x0709"), _ ) )
+          => doneMerkle( MerkleExtension( #parseByteStack("0x07"), MerkleBranch( _, _ ) ) ) </k>
 
     // Update on MerkleBranch
-    rule <k> runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .WordStack, V ) )
+    rule <k> runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .ByteArray, V ) )
           => doneMerkle( MerkleBranch( M, V ) ) </k>
 
     rule <k> runMerkle ( .MerkleBranch )