Skip to content

Commit

Permalink
Factor out JSON modules (#571)
Browse files Browse the repository at this point in the history 
* data, web3, {kast,kore}-json.py: factor out JSON and JSON-RPC modules

* data: remove `Int` from JSONKey by default in JSON module

* data: add klabels for JSON

* data, kast-json, kore-json: update to separate JSON modules

* kore-json: correct labels used

* web3: final rename

* tests/interactive: update test output

* web3: klabel for undef

* deps/plugin: 5f0f896 - Rename labels for factored out JSON modules (#70)

* web3: correct sort name

* data: add intermediate sort for JSONs

* data, web3: add syntax alias

* tests/: update expected output
  • Loading branch information
@ehildenb
ehildenb authored Nov 29, 2019
1 parent f56982d commit 4a1a105
Show file tree
Hide file tree
Showing 15 changed files with 110 additions and 78 deletions.
48 changes: 34 additions & 14 deletions data.md
View file
Original file line number Diff line number Diff line change
@@ -1,39 +1,59 @@
EVM Words
=========

### Module `EVM-DATA`
```k
requires "krypto.k"
```

### JSON Formatting

The JSON format is used extensively for communication in the Ethereum circles.
Writing a JSON-ish parser in K takes 6 lines.

```k
module JSON
imports INT
imports STRING
imports BOOL
syntax JSONs ::= List{JSON,","} [klabel(JSONs), symbol]
| ".JSONList"
syntax JSONList = JSONs
// -----------------------
rule .JSONList => .JSONs [macro]
syntax JSONKey ::= String
syntax JSON ::= "null" [klabel(JSONnull) , symbol]
| String | Int | Bool
| JSONKey ":" JSON [klabel(JSONEntry) , symbol]
| "{" JSONList "}" [klabel(JSONObject) , symbol]
| "[" JSONList "]" [klabel(JSONList) , symbol]
// ---------------------------------------------------------------------
endmodule
```

EVM uses bounded 256 bit integer words, and sometimes also bytes (8 bit words).
Here we provide the arithmetic of these words, as well as some data-structures over them.
Both are implemented using K's `Int`.

```k
requires "krypto.k"
module EVM-DATA
imports KRYPTO
imports STRING-BUFFER
imports MAP-SYMBOLIC
imports COLLECTIONS
imports JSON
```

```{.k .concrete}
imports BYTES
```

### JSON Formatting

The JSON format is used extensively for communication in the Ethereum circles.
Writing a JSON-ish parser in K takes 6 lines.
**TODO**: Adding `Int` to `JSONKey` is a hack to make certain parts of semantics easier.

```k
syntax JSONList ::= List{JSON,","}
syntax JSONKey ::= String | Int
syntax JSON ::= String | Int | Bool
| JSONKey ":" JSON
| "{" JSONList "}"
| "[" JSONList "]"
// ------------------------------------
syntax JSONKey ::= Int
// ----------------------
```

Utilities
Expand Down
2 changes: 1 addition & 1 deletion deps/plugin
Submodule plugin updated 3 files
+21 −2 Dockerfile
+0 −1 Jenkinsfile
+48 −46 client-c/json.cpp
12 changes: 6 additions & 6 deletions kast-json.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,24 +14,24 @@ def escape(data):

def print_kast(data):
if isinstance(data, list):
sys.stdout.write('`[_]_EVM-DATA`(')
sys.stdout.write('`JSONList`(')
for elem in data:
sys.stdout.write('`_,__EVM-DATA`(')
sys.stdout.write('`JSONs`(')
print_kast(elem)
sys.stdout.write(',')
sys.stdout.write('`.List{"_,__EVM-DATA"}`(.KList)')
sys.stdout.write('`.List{"JSONs"}`(.KList)')
for elem in data:
sys.stdout.write(')')
sys.stdout.write(')')
elif isinstance(data, OrderedDict):
sys.stdout.write('`{_}_EVM-DATA`(')
sys.stdout.write('`JSONObject`(')
for key, value in data.items():
sys.stdout.write('`_,__EVM-DATA`(`_:__EVM-DATA`(')
sys.stdout.write('`JSONs`(`JSONEntry`(')
print_kast(key)
sys.stdout.write(',')
print_kast(value)
sys.stdout.write('),')
sys.stdout.write('`.List{"_,__EVM-DATA"}`(.KList)')
sys.stdout.write('`.List{"JSONs"}`(.KList)')
for key in data:
sys.stdout.write(')')
sys.stdout.write(')')
Expand Down
12 changes: 6 additions & 6 deletions kore-json.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,24 +14,24 @@ def escape(data):

def print_kast(data, sort="SortJSON"):
if isinstance(data, list):
sys.stdout.write("Lbl'LSqBUndsRSqBUnds'EVM-DATA'Unds'JSON'Unds'JSONList{}(")
sys.stdout.write("LblJSONList{}(")
for elem in data:
sys.stdout.write("Lbl'UndsCommUndsUnds'EVM-DATA'Unds'JSONList'Unds'JSON'Unds'JSONList{}(")
sys.stdout.write("LblJSONs{}(")
print_kast(elem)
sys.stdout.write(',')
sys.stdout.write("Lbl'Stop'List'LBraQuotUndsCommUndsUnds'EVM-DATA'Unds'JSONList'Unds'JSON'Unds'JSONList'QuotRBraUnds'JSONList{}()")
sys.stdout.write("Lbl'Stop'List'LBraQuot'JSONs'QuotRBraUnds'JSONs{}()")
for elem in data:
sys.stdout.write(')')
sys.stdout.write(')')
elif isinstance(data, OrderedDict):
sys.stdout.write("Lbl'LBraUndsRBraUnds'EVM-DATA'Unds'JSON'Unds'JSONList{}(")
sys.stdout.write("LblJSONObject{}(")
for key, value in data.items():
sys.stdout.write("Lbl'UndsCommUndsUnds'EVM-DATA'Unds'JSONList'Unds'JSON'Unds'JSONList{}(Lbl'UndsColnUndsUnds'EVM-DATA'Unds'JSON'Unds'JSONKey'Unds'JSON{}(")
sys.stdout.write("LblJSONs{}(LblJSONEntry{}(")
print_kast(key, "SortJSONKey")
sys.stdout.write(',')
print_kast(value)
sys.stdout.write('),')
sys.stdout.write("Lbl'Stop'List'LBraQuotUndsCommUndsUnds'EVM-DATA'Unds'JSONList'Unds'JSON'Unds'JSONList'QuotRBraUnds'JSONList{}()")
sys.stdout.write("Lbl'Stop'List'LBraQuot'JSONs'QuotRBraUnds'JSONs{}()")
for key in data:
sys.stdout.write(')')
sys.stdout.write(')')
Expand Down
4 changes: 2 additions & 2 deletions tests/failing/ContractCreationSpam_d0g0v0.json.expected
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<kevm>
<k>
check "account" : { 244687034288125203496486448490407391986876152250 : { "balance" : 3000017592186844416 , .JSONList } , .JSONList } ~> check "account" : { 244687034288125203496486448490407391986876152250 : { "code" : "" , "nonce" : "0x00" , "storage" : { .JSONList } , .JSONList } , .JSONList } ~> check "account" : { "0x6a0a0fc761c612c340a0e98d33b37a75e5268472" : { "balance" : "0x0de0b6b3a7640000" , "code" : "0x7f6004600c60003960046000f3600035ff00000000000000000000000000000000600052602060006000f0600054805b6001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1505a616000106200002f57600055" , "nonce" : "0x00" , "storage" : { .JSONList } , .JSONList } , "0xa94f5374fce5edbc8e2a8697c15331677e6ebf0b" : { "balance" : "0xe8d498db00" , "code" : "" , "nonce" : "0x01" , "storage" : { .JSONList } , .JSONList } , .JSONList } ~> failure "ContractCreationSpam_d0g0v0_Byzantium" ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "genesisBlockHeader" : { "bloom" : "0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" , "coinbase" : "0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba" , "difficulty" : "0x020000" , "extraData" : "0x42" , "gasLimit" : "0x174876e800" , "gasUsed" : "0x00" , "hash" : "0x24a30e4305ac41674b26493c800c05f507e98d3b8bceb0a314f9b9bc43622736" , "mixHash" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "nonce" : "0x0102030405060708" , "number" : "0x00" , "parentHash" : "0x0000000000000000000000000000000000000000000000000000000000000000" , "receiptTrie" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "stateRoot" : "0xd54ec35ca872c653659ad91eaa355665c286183b541a0519b3ab765a2d6733c3" , "timestamp" : "0x03b6" , "transactionsTrie" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "uncleHash" : "0x1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347" , .JSONList } , .JSONList } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "blockHeader" : { "bloom" : "0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" , "coinbase" : "0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba" , "difficulty" : "0x020000" , "extraData" : "" , "gasLimit" : "0x174876e800" , "gasUsed" : "0x0c3500" , "hash" : "0x395c1b94f8f4fe9f239719e27d11c86cec9b0c5ae063482fe187e7cdbc9ca9fa" , "mixHash" : "0x0000000000000000000000000000000000000000000000000000000000000000" , "nonce" : "0x0000000000000000" , "number" : "0x01" , "parentHash" : "0x24a30e4305ac41674b26493c800c05f507e98d3b8bceb0a314f9b9bc43622736" , "receiptTrie" : "0x1723da285b2c748c2ca379879c0cc2319ff26a9feb6d0779c6821ebe1a8122f6" , "stateRoot" : "0x0344321ea672cbc56b9b51fa730cb2e67fe4b5a7f8c4a14a291ce4d0292e2352" , "timestamp" : "0x03e8" , "transactionsTrie" : "0x202c09237fc2d6599e3cce6c9775000e3714d184832789143ef1ec871492f7fa" , "uncleHash" : "0x1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347" , .JSONList } , .JSONList } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "transactions" : [ { "data" : "0x" , "gasLimit" : "0x0c3500" , "gasPrice" : "0x01" , "nonce" : "0x00" , "r" : "0xaca0d145ae5d27ed427ff0e463b8a46181d4786c437d6efb9937a6990694af7a" , "s" : "0x0f9bd68ece8f38ef2836153cd0bb85ec92f8386177f6e68d5437ab7b7d0d6361" , "to" : "0x6a0a0fc761c612c340a0e98d33b37a75e5268472" , "v" : "0x1b" , "value" : "0x00" , .JSONList } , .JSONList ] , .JSONList } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "uncleHeaders" : [ .JSONList ] , .JSONList } ~> clear ~> run { .JSONList } ~> success .EthereumSimulation
check "account" : { 244687034288125203496486448490407391986876152250 : { "balance" : 3000017592186844416 , .JSONs } , .JSONs } ~> check "account" : { 244687034288125203496486448490407391986876152250 : { "code" : "" , "nonce" : "0x00" , "storage" : { .JSONs } , .JSONs } , .JSONs } ~> check "account" : { "0x6a0a0fc761c612c340a0e98d33b37a75e5268472" : { "balance" : "0x0de0b6b3a7640000" , "code" : "0x7f6004600c60003960046000f3600035ff00000000000000000000000000000000600052602060006000f0600054805b6001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1506001018060005260008060208180876006f1505a616000106200002f57600055" , "nonce" : "0x00" , "storage" : { .JSONs } , .JSONs } , "0xa94f5374fce5edbc8e2a8697c15331677e6ebf0b" : { "balance" : "0xe8d498db00" , "code" : "" , "nonce" : "0x01" , "storage" : { .JSONs } , .JSONs } , .JSONs } ~> failure "ContractCreationSpam_d0g0v0_Byzantium" ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "genesisBlockHeader" : { "bloom" : "0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" , "coinbase" : "0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba" , "difficulty" : "0x020000" , "extraData" : "0x42" , "gasLimit" : "0x174876e800" , "gasUsed" : "0x00" , "hash" : "0x24a30e4305ac41674b26493c800c05f507e98d3b8bceb0a314f9b9bc43622736" , "mixHash" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "nonce" : "0x0102030405060708" , "number" : "0x00" , "parentHash" : "0x0000000000000000000000000000000000000000000000000000000000000000" , "receiptTrie" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "stateRoot" : "0xd54ec35ca872c653659ad91eaa355665c286183b541a0519b3ab765a2d6733c3" , "timestamp" : "0x03b6" , "transactionsTrie" : "0x56e81f171bcc55a6ff8345e692c0f86e5b48e01b996cadc001622fb5e363b421" , "uncleHash" : "0x1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347" , .JSONs } , .JSONs } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "blockHeader" : { "bloom" : "0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" , "coinbase" : "0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba" , "difficulty" : "0x020000" , "extraData" : "" , "gasLimit" : "0x174876e800" , "gasUsed" : "0x0c3500" , "hash" : "0x395c1b94f8f4fe9f239719e27d11c86cec9b0c5ae063482fe187e7cdbc9ca9fa" , "mixHash" : "0x0000000000000000000000000000000000000000000000000000000000000000" , "nonce" : "0x0000000000000000" , "number" : "0x01" , "parentHash" : "0x24a30e4305ac41674b26493c800c05f507e98d3b8bceb0a314f9b9bc43622736" , "receiptTrie" : "0x1723da285b2c748c2ca379879c0cc2319ff26a9feb6d0779c6821ebe1a8122f6" , "stateRoot" : "0x0344321ea672cbc56b9b51fa730cb2e67fe4b5a7f8c4a14a291ce4d0292e2352" , "timestamp" : "0x03e8" , "transactionsTrie" : "0x202c09237fc2d6599e3cce6c9775000e3714d184832789143ef1ec871492f7fa" , "uncleHash" : "0x1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347" , .JSONs } , .JSONs } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "transactions" : [ { "data" : "0x" , "gasLimit" : "0x0c3500" , "gasPrice" : "0x01" , "nonce" : "0x00" , "r" : "0xaca0d145ae5d27ed427ff0e463b8a46181d4786c437d6efb9937a6990694af7a" , "s" : "0x0f9bd68ece8f38ef2836153cd0bb85ec92f8386177f6e68d5437ab7b7d0d6361" , "to" : "0x6a0a0fc761c612c340a0e98d33b37a75e5268472" , "v" : "0x1b" , "value" : "0x00" , .JSONs } , .JSONs ] , .JSONs } ~> check "ContractCreationSpam_d0g0v0_Byzantium" : { "uncleHeaders" : [ .JSONs ] , .JSONs } ~> clear ~> run { .JSONs } ~> success .EthereumSimulation
</k>
<exit-code>
1
Expand Down Expand Up @@ -143,7 +143,7 @@
0
</blockNonce>
<ommerBlockHeaders>
[ .JSONList ]
[ .JSONs ]
</ommerBlockHeaders>
</block>
</evm>
Expand Down
Loading

0 comments on commit 4a1a105

Please sign in to comment.