From 16ac53f3f857d757b00542a6014d495f7dac0535 Mon Sep 17 00:00:00 2001 From: ehildenb Date: Sun, 1 Dec 2019 19:41:09 -0700 Subject: [PATCH] Remove sort JSONList (#584) * *.md, tests/*: rename sort JSONList => JSONs * web3: remaining renames --- data.md | 33 ++-- driver.md | 76 ++++----- evm.md | 8 +- state-loader.md | 52 +++--- tests/templates/output-success-ocaml.json | 2 +- web3.md | 192 +++++++++++----------- 6 files changed, 179 insertions(+), 184 deletions(-) diff --git a/data.md b/data.md index 5c6e4954fe..f552c08e6f 100644 --- a/data.md +++ b/data.md @@ -16,19 +16,14 @@ module JSON 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] - // --------------------------------------------------------------------- + syntax JSONs ::= List{JSON,","} [klabel(JSONs) , symbol] + syntax JSONKey ::= String + syntax JSON ::= "null" [klabel(JSONnull) , symbol] + | String | Int | Bool + | JSONKey ":" JSON [klabel(JSONEntry) , symbol] + | "{" JSONs "}" [klabel(JSONObject) , symbol] + | "[" JSONs "]" [klabel(JSONList) , symbol] + // -------------------------------------------------------------------- endmodule ``` @@ -840,7 +835,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `ByteArray`s, and `M ```k syntax Map ::= #parseMap ( JSON ) [function] // -------------------------------------------- - rule #parseMap( { .JSONList } ) => .Map + rule #parseMap( { .JSONs } ) => .Map rule #parseMap( { _ : (VALUE:String) , REST } ) => #parseMap({ REST }) requires #parseHexWord(VALUE) ==K 0 rule #parseMap( { KEY : (VALUE:String) , REST } ) => #parseMap({ REST }) [ #parseHexWord(KEY) <- #parseHexWord(VALUE) ] requires #parseHexWord(VALUE) =/=K 0 @@ -993,7 +988,7 @@ Decoding -------- - `#rlpDecode` RLP decodes a single `String` into a `JSON`. -- `#rlpDecodeList` RLP decodes a single `String` into a `JSONList`, interpereting the string as the RLP encoding of a list. +- `#rlpDecodeList` RLP decodes a single `String` into a `JSONs`, interpereting the string as the RLP encoding of a list. ```k syntax JSON ::= #rlpDecode(String) [function] @@ -1003,11 +998,11 @@ Decoding rule #rlpDecode(STR, #str(LEN, POS)) => substrString(STR, POS, POS +Int LEN) rule #rlpDecode(STR, #list(LEN, POS)) => [#rlpDecodeList(STR, POS)] - syntax JSONList ::= #rlpDecodeList(String, Int) [function] - | #rlpDecodeList(String, Int, LengthPrefix) [function, klabel(#rlpDecodeListAux)] - // --------------------------------------------------------------------------------------------------- + syntax JSONs ::= #rlpDecodeList(String, Int) [function] + | #rlpDecodeList(String, Int, LengthPrefix) [function, klabel(#rlpDecodeListAux)] + // ------------------------------------------------------------------------------------------------ rule #rlpDecodeList(STR, POS) => #rlpDecodeList(STR, POS, #decodeLengthPrefix(STR, POS)) requires POS .JSONList [owise] + rule #rlpDecodeList(STR, POS) => .JSONs [owise] rule #rlpDecodeList(STR, POS, _:LengthPrefixType(L, P)) => #rlpDecode(substrString(STR, POS, L +Int P)) , #rlpDecodeList(STR, L +Int P) syntax LengthPrefixType ::= "#str" | "#list" diff --git a/driver.md b/driver.md index a4efd7184e..f1820879f5 100644 --- a/driver.md +++ b/driver.md @@ -40,23 +40,23 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax JSON ::= ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account // ----------------------------------------------------------------------------- - syntax JSONList ::= #sortJSONList ( JSONList ) [function] - | #sortJSONList ( JSONList , JSONList ) [function, klabel(#sortJSONListAux)] - // ---------------------------------------------------------------------------------------------- - rule #sortJSONList(JS) => #sortJSONList(JS, .JSONList) - rule #sortJSONList(.JSONList, LS) => LS - rule #sortJSONList(((KEY : VAL) , REST), LS) => #insertJSONKey((KEY : VAL), #sortJSONList(REST, LS)) - - syntax JSONList ::= #insertJSONKey ( JSON , JSONList ) [function] - // ----------------------------------------------------------------- - rule #insertJSONKey( JS , .JSONList ) => JS , .JSONList + syntax JSONs ::= #sortJSONs ( JSONs ) [function] + | #sortJSONs ( JSONs , JSONs ) [function, klabel(#sortJSONsAux)] + // ------------------------------------------------------------------------------- + rule #sortJSONs(JS) => #sortJSONs(JS, .JSONs) + rule #sortJSONs(.JSONs, LS) => LS + rule #sortJSONs(((KEY : VAL) , REST), LS) => #insertJSONKey((KEY : VAL), #sortJSONs(REST, LS)) + + syntax JSONs ::= #insertJSONKey ( JSON , JSONs ) [function] + // ----------------------------------------------------------- + rule #insertJSONKey( JS , .JSONs ) => JS , .JSONs rule #insertJSONKey( (KEY : VAL) , ((KEY' : VAL') , REST) ) => (KEY : VAL) , (KEY' : VAL') , REST requires KEY (KEY' : VAL') , #insertJSONKey((KEY : VAL) , REST) requires KEY >=String KEY' - syntax Bool ::= #isSorted ( JSONList ) [function] - // ------------------------------------------------- - rule #isSorted( .JSONList ) => true - rule #isSorted( KEY : _ ) => true + syntax Bool ::= #isSorted ( JSONs ) [function] + // ---------------------------------------------- + rule #isSorted( .JSONs ) => true + rule #isSorted( KEY : _ ) => true rule #isSorted( (KEY : _) , (KEY' : VAL) , REST ) => KEY <=String KEY' andThenBool #isSorted((KEY' : VAL) , REST) ``` @@ -227,9 +227,9 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` ```k syntax EthereumCommand ::= "run" JSON // ------------------------------------- - rule run { .JSONList } => . ... - rule run { TESTID : { TEST:JSONList } , TESTS } - => run ( TESTID : { #sortJSONList(TEST) } ) + rule run { .JSONs } => . ... + rule run { TESTID : { TEST:JSONs } , TESTS } + => run ( TESTID : { #sortJSONs(TEST) } ) ~> #if #hasPost?( { TEST } ) #then .K #else exception #fi ~> clear ~> run { TESTS } @@ -238,7 +238,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` syntax Bool ::= "#hasPost?" "(" JSON ")" [function] // --------------------------------------------------- - rule #hasPost? ({ .JSONList }) => false + rule #hasPost? ({ .JSONs }) => false rule #hasPost? ({ (KEY:String) : _ , REST }) => (KEY in #postKeys) orBool #hasPost? ({ REST }) ``` @@ -252,8 +252,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` rule run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... requires KEY in #loadKeys - rule run TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, .JSONList ] , ( REST2 => KEY : VAL , REST2 ) } ... - rule run TESTID : { "blocks" : [ { .JSONList }, .JSONList ] , REST } => run TESTID : { REST } ... + rule run TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, .JSONs ] , ( REST2 => KEY : VAL , REST2 ) } ... + rule run TESTID : { "blocks" : [ { .JSONs }, .JSONs ] , REST } => run TESTID : { REST } ... ``` - `#execKeys` are all the JSON nodes which should be considered for execution (between loading and checking). @@ -319,10 +319,10 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` ```{.k .standalone} rule load "account" : { ACCTID : ACCT } => loadAccount ACCTID ACCT ... - rule loadAccount _ { "balance" : ((VAL:String) => #parseWord(VAL)), _ } ... - rule loadAccount _ { "nonce" : ((VAL:String) => #parseWord(VAL)), _ } ... - rule loadAccount _ { "code" : ((CODE:String) => #parseByteStack(CODE)), _ } ... - rule loadAccount _ { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })), _ } ... + rule loadAccount _ { "balance" : ((VAL:String) => #parseWord(VAL)), _ } ... + rule loadAccount _ { "nonce" : ((VAL:String) => #parseWord(VAL)), _ } ... + rule loadAccount _ { "code" : ((CODE:String) => #parseByteStack(CODE)), _ } ... + rule loadAccount _ { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })), _ } ... rule loadTransaction _ { "gasLimit" : (TG:String => #asWord(#parseByteStackRaw(TG))), _ } ... rule loadTransaction _ { "gasPrice" : (TP:String => #asWord(#parseByteStackRaw(TP))), _ } ... @@ -344,27 +344,27 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` // --------------------------------------- rule #halt ~> check J:JSON => check J ~> #halt ... - rule check DATA : { .JSONList } => . ... requires DATA =/=String "transactions" - rule check DATA : [ .JSONList ] => . ... requires DATA =/=String "ommerHeaders" + rule check DATA : { .JSONs } => . ... requires DATA =/=String "transactions" + rule check DATA : [ .JSONs ] => . ... requires DATA =/=String "ommerHeaders" rule check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST } ... - requires REST =/=K .JSONList andBool notBool DATA in (SetItem("callcreates") SetItem("transactions")) + requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions")) rule check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] ... requires DATA =/=String "transactions" - rule check (KEY:String) : { JS:JSONList => #sortJSONList(JS) } ... + rule check (KEY:String) : { JS:JSONs => #sortJSONs(JS) } ... requires KEY in (SetItem("callcreates")) andBool notBool #isSorted(JS) rule check TESTID : { "post" : POST } => check "account" : POST ~> failure TESTID ... rule check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ... - requires REST =/=K .JSONList + requires REST =/=K .JSONs rule check "account" : { ((ACCTID:String) => #parseAddr(ACCTID)) : ACCT } ... - rule check "account" : { (ACCT:Int) : { "balance" : ((VAL:String) => #parseWord(VAL)) } } ... - rule check "account" : { (ACCT:Int) : { "nonce" : ((VAL:String) => #parseWord(VAL)) } } ... - rule check "account" : { (ACCT:Int) : { "code" : ((CODE:String) => #parseByteStack(CODE)) } } ... - rule check "account" : { (ACCT:Int) : { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })) } } ... + rule check "account" : { (ACCT:Int) : { "balance" : ((VAL:String) => #parseWord(VAL)) } } ... + rule check "account" : { (ACCT:Int) : { "nonce" : ((VAL:String) => #parseWord(VAL)) } } ... + rule check "account" : { (ACCT:Int) : { "code" : ((CODE:String) => #parseByteStack(CODE)) } } ... + rule check "account" : { (ACCT:Int) : { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })) } } ... rule EXECMODE check "account" : { ACCT : { "balance" : (BAL:Int) } } => . ... @@ -431,7 +431,7 @@ Here we check the other post-conditions associated with an EVM test. rule check TESTID : { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ~> failure TESTID // ---------------------------------------------------------------------------------------------------------- rule check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... - requires REST =/=K .JSONList + requires REST =/=K .JSONs rule check "blockHeader" : { KEY : (VALUE:String => #parseByteStack(VALUE)) } ... @@ -479,7 +479,7 @@ Here we check the other post-conditions associated with an EVM test. rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID // ------------------------------------------------------------------------------------------------------------------------ rule check "genesisBlockHeader" : { KEY : VALUE , REST } => check "genesisBlockHeader" : { KEY : VALUE } ~> check "genesisBlockHeader" : { REST } ... - requires REST =/=K .JSONList + requires REST =/=K .JSONs rule check "genesisBlockHeader" : { KEY : VALUE } => .K ... requires KEY =/=String "hash" @@ -489,8 +489,8 @@ Here we check the other post-conditions associated with an EVM test. rule check TESTID : { "transactions" : TRANSACTIONS } => check "transactions" : TRANSACTIONS ~> failure TESTID ... // --------------------------------------------------------------------------------------------------------------------------- - rule check "transactions" : [ .JSONList ] => . ... .List - rule check "transactions" : { .JSONList } => . ... ListItem(_) => .List ... + rule check "transactions" : [ .JSONs ] => . ... .List + rule check "transactions" : { .JSONs } => . ... ListItem(_) => .List ... rule check "transactions" : [ TRANSACTION , REST ] => check "transactions" : TRANSACTION ~> check "transactions" : [ REST ] ... rule check "transactions" : { KEY : VALUE , REST } => check "transactions" : (KEY : VALUE) ~> check "transactions" : { REST } ... @@ -516,7 +516,7 @@ TODO: case with nonzero ommers. ```k rule check TESTID : { "uncleHeaders" : OMMERS } => check "ommerHeaders" : OMMERS ~> failure TESTID ... // --------------------------------------------------------------------------------------------------------------- - rule check "ommerHeaders" : [ .JSONList ] => . ... [ .JSONList ] + rule check "ommerHeaders" : [ .JSONs ] => . ... [ .JSONs ] ``` ```k diff --git a/evm.md b/evm.md index 1291080b8d..2199dc6b2a 100644 --- a/evm.md +++ b/evm.md @@ -104,7 +104,7 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 // I_Hm 0 // I_Hn - [ .JSONList ] + [ .JSONs ] @@ -658,8 +658,8 @@ After executing a transaction, it's necessary to have the effect of the substate _ => .List _ => #padToWidth(256, .ByteArray) - syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList ) - // ------------------------------------------------------------------------ + syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONs ) + // --------------------------------------------------------------------- rule #finalizeBlock => #rewardOmmers(OMMERS) ... SCHED [ OMMERS ] @@ -677,7 +677,7 @@ After executing a transaction, it's necessary to have the effect of the substate ACCTS requires notBool MINER in ACCTS - rule #rewardOmmers(.JSONList) => . ... + rule #rewardOmmers(.JSONs) => . ... rule #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... SCHED MINER diff --git a/state-loader.md b/state-loader.md index 73629694e1..8a99c6360c 100644 --- a/state-loader.md +++ b/state-loader.md @@ -52,23 +52,23 @@ module STATE-LOADER syntax EthereumCommand ::= "clearBLOCK" // --------------------------------------- rule clearBLOCK => . ... - _ => 0 - _ => 0 - _ => 0 - _ => 0 - _ => 0 - _ => 0 - _ => .ByteArray - _ => 0 - _ => 0 - _ => 0 - _ => 0 - _ => 0 - _ => .ByteArray - _ => 0 - _ => 0 - _ => [ .JSONList ] - _ => .List + _ => 0 + _ => 0 + _ => 0 + _ => 0 + _ => 0 + _ => 0 + _ => .ByteArray + _ => 0 + _ => 0 + _ => 0 + _ => 0 + _ => 0 + _ => .ByteArray + _ => 0 + _ => 0 + _ => [ .JSONs ] + _ => .List syntax EthereumCommand ::= "clearNETWORK" // ----------------------------------------- @@ -95,11 +95,11 @@ module STATE-LOADER ```{.k} syntax EthereumCommand ::= "load" JSON // -------------------------------------- - rule load DATA : { .JSONList } => . ... + rule load DATA : { .JSONs } => . ... rule load DATA : { KEY : VALUE , REST } => load DATA : { KEY : VALUE } ~> load DATA : { REST } ... - requires REST =/=K .JSONList andBool DATA =/=String "transaction" + requires REST =/=K .JSONs andBool DATA =/=String "transaction" - rule load DATA : [ .JSONList ] => . ... + rule load DATA : [ .JSONs ] => . ... rule load DATA : [ { TEST } , REST ] => load DATA : { TEST } ~> load DATA : [ REST ] ... ``` @@ -110,7 +110,7 @@ Here we perform pre-proccesing on account data which allows "pretty" specificati syntax EthereumCommand ::= "loadAccount" Int JSON // ------------------------------------------------- - rule loadAccount _ { .JSONList } => . ... + rule loadAccount _ { .JSONs } => . ... rule loadAccount ACCT { "balance" : (BAL:Int), REST => REST } ... ACCT _ => BAL ... @@ -153,7 +153,7 @@ Here we load the environmental information. rule loadCallState { "value" : VALUE:Int, REST => REST } ... _ => VALUE rule loadCallState { "data" : DATA:ByteArray, REST => REST } ... _ => DATA - rule loadCallState { .JSONList } => . ... + rule loadCallState { .JSONs } => . ... ``` The `"network"` key allows setting the fee schedule inside the test. @@ -179,7 +179,7 @@ The `"rlp"` key loads the block information. rule load "rlp" : (VAL:String => #rlpDecode(#unparseByteStack(#parseByteStack(VAL)))) ... rule load "genesisRLP" : (VAL:String => #rlpDecode(#unparseByteStack(#parseByteStack(VAL)))) ... // --------------------------------------------------------------------------------------------------------- - rule load "rlp" : [ [ HP , HO , HC , HR , HT , HE , HB , HD , HI , HL , HG , HS , HX , HM , HN , .JSONList ] , BT , BU , .JSONList ] + rule load "rlp" : [ [ HP , HO , HC , HR , HT , HE , HB , HD , HI , HL , HG , HS , HX , HM , HN , .JSONs ] , BT , BU , .JSONs ] => load "transaction" : BT ... @@ -200,7 +200,7 @@ The `"rlp"` key loads the block information. _ => #asWord(#parseByteStackRaw(HN)) _ => BU - rule load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:String, HB, HD, HI, HL, HG, HS, HX, HM, HN, .JSONList ], _, _, .JSONList ] => .K ... + rule load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:String, HB, HD, HI, HL, HG, HS, HX, HM, HN, .JSONs ], _, _, .JSONs ] => .K ... .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)) ListItem(#asWord(#parseByteStackRaw(HP))) ... syntax EthereumCommand ::= "mkTX" Int @@ -225,7 +225,7 @@ The `"rlp"` key loads the block information. ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP , "nonce" : TN , "r" : TR , "s" : TS , "to" : TT , "v" : TW , "value" : TV - , .JSONList + , .JSONs } ~> load "transaction" : [ REST ] ... @@ -233,7 +233,7 @@ The `"rlp"` key loads the block information. syntax EthereumCommand ::= "loadTransaction" Int JSON // ----------------------------------------------------- - rule loadTransaction _ { .JSONList } => . ... + rule loadTransaction _ { .JSONs } => . ... rule loadTransaction TXID { GLIMIT : TG:Int, REST => REST } ... TXID _ => TG ... diff --git a/tests/templates/output-success-ocaml.json b/tests/templates/output-success-ocaml.json index eb4af48a30..65e6d29240 100644 --- a/tests/templates/output-success-ocaml.json +++ b/tests/templates/output-success-ocaml.json @@ -139,7 +139,7 @@ 0 - [ .JSONList ] + [ .JSONs ] diff --git a/web3.md b/web3.md index d0c712a205..02512ffcd6 100644 --- a/web3.md +++ b/web3.md @@ -20,7 +20,7 @@ module JSON-RPC "":JSON 0:JSON "":JSON - [ .JSONList ] + [ .JSONs ] undef .List @@ -29,9 +29,9 @@ module JSON-RPC syntax JSON ::= "undef" [klabel(JSON-RPCundef), symbol] // ------------------------------------------------------- - syntax Bool ::= isProperJson ( JSON ) [function] - | isProperJsonList ( JSONList ) [function] - // -------------------------------------------------------- + syntax Bool ::= isProperJson ( JSON ) [function] + | isProperJsonList ( JSONs ) [function] + // ----------------------------------------------------- rule isProperJson(_) => false [owise] rule isProperJson(null) => true @@ -45,8 +45,8 @@ module JSON-RPC rule isProperJson([ JS ]) => isProperJsonList(JS) rule isProperJson({ JS }) => isProperJsonList(JS) - rule isProperJsonList(.JSONList) => true - rule isProperJsonList(J, JS) => isProperJson(J) andBool isProperJsonList(JS) + rule isProperJsonList(.JSONs) => true + rule isProperJsonList(J, JS) => isProperJson(J) andBool isProperJsonList(JS) endmodule ``` @@ -178,7 +178,7 @@ WEB3 JSON RPC syntax JSON ::= #getJSON ( JSONKey , JSON ) [function] // ------------------------------------------------------ rule #getJSON( KEY, { KEY : J, _ } ) => J - rule #getJSON( _, { .JSONList } ) => undef + rule #getJSON( _, { .JSONs } ) => undef rule #getJSON( KEY, { KEY2 : _, REST } ) => #getJSON( KEY, { REST } ) requires KEY =/=K KEY2 @@ -233,7 +233,7 @@ WEB3 JSON RPC _ => J _ => .List - rule #loadRPCCall(_:String #Or null #Or _:Int #Or [ .JSONList ]) => #rpcResponseError(-32600, "Invalid Request") ... + rule #loadRPCCall(_:String #Or null #Or _:Int #Or [ .JSONs ]) => #rpcResponseError(-32600, "Invalid Request") ... _ => null rule #loadRPCCall(undef) => #rpcResponseError(-32700, "Parse error") ... @@ -245,19 +245,19 @@ WEB3 JSON RPC [ J , JS => JS ] rule #loadFromBatch ~> _ => #putResponse(List2JSON(RESPONSE), SOCK) ~> getRequest() - [ .JSONList ] + [ .JSONs ] SOCK RESPONSE requires size(RESPONSE) >Int 0 rule #loadFromBatch ~> _ => getRequest() - [ .JSONList ] + [ .JSONs ] .List - syntax JSON ::= List2JSON(List) [function] - | List2JSON(List, JSONList) [function, klabel(List2JSONAux)] - // -------------------------------------------------------------------------- - rule List2JSON(L) => List2JSON(L, .JSONList) + syntax JSON ::= List2JSON(List) [function] + | List2JSON(List, JSONs) [function, klabel(List2JSONAux)] + // ----------------------------------------------------------------------- + rule List2JSON(L) => List2JSON(L, .JSONs) rule List2JSON(L ListItem(J), JS) => List2JSON(L, (J, JS)) rule List2JSON(.List , JS) => [ JS ] @@ -417,18 +417,18 @@ WEB3 JSON RPC rule #eth_accounts => #rpcResponseSuccess([ #acctsToJArray( qsort(Set2List(ACCTS)) ) ]) ... ACCTS - syntax JSONList ::= #acctsToJArray ( List ) [function] - // ------------------------------------------------------ - rule #acctsToJArray( .List ) => .JSONList + syntax JSONs ::= #acctsToJArray ( List ) [function] + // --------------------------------------------------- + rule #acctsToJArray( .List ) => .JSONs rule #acctsToJArray( ListItem( ACCT ) ACCTS:List ) => #unparseData( ACCT, 20 ), #acctsToJArray( ACCTS ) syntax KItem ::= "#eth_getBalance" // ---------------------------------- rule #eth_getBalance ... - [ (DATA => #parseHexWord(DATA)), _, .JSONList ] + [ (DATA => #parseHexWord(DATA)), _, .JSONs ] rule #eth_getBalance => #getAccountAtBlock(#parseBlockIdentifier(TAG), DATA) ~> #eth_getBalance ... - [ DATA, TAG, .JSONList ] + [ DATA, TAG, .JSONs ] rule ... ACCTBALANCE ... ~> #eth_getBalance => #rpcResponseSuccess(#unparseQuantity( ACCTBALANCE )) ... @@ -439,13 +439,13 @@ WEB3 JSON RPC syntax KItem ::= "#eth_getStorageAt" // ------------------------------------ rule #eth_getStorageAt ... - [ (DATA => #parseHexWord(DATA)), (QUANTITY => #parseHexWord(QUANTITY)), _, .JSONList ] + [ (DATA => #parseHexWord(DATA)), (QUANTITY => #parseHexWord(QUANTITY)), _, .JSONs ] rule #eth_getStorageAt => #getAccountAtBlock(#parseBlockIdentifier(TAG), DATA) ~> #eth_getStorageAt ... - [ DATA, QUANTITY, TAG, .JSONList ] + [ DATA, QUANTITY, TAG, .JSONs ] rule ... STORAGE ... ~> #eth_getStorageAt => #rpcResponseSuccess(#unparseQuantity( #lookup (STORAGE, QUANTITY) )) ... - [ DATA, QUANTITY, TAG, .JSONList ] + [ DATA, QUANTITY, TAG, .JSONs ] rule .AccountItem ~> #eth_getStorageAt => #rpcResponseSuccess(#unparseQuantity( 0 )) ... @@ -454,10 +454,10 @@ WEB3 JSON RPC syntax KItem ::= "#eth_getCode" // ------------------------------- rule #eth_getCode ... - [ (DATA => #parseHexWord(DATA)), _, .JSONList ] + [ (DATA => #parseHexWord(DATA)), _, .JSONs ] rule #eth_getCode => #getAccountAtBlock(#parseBlockIdentifier(TAG), DATA) ~> #eth_getCode ... - [ DATA, TAG, .JSONList ] + [ DATA, TAG, .JSONs ] rule ... CODE ... ~> #eth_getCode => #rpcResponseSuccess(#unparseDataByteArray( CODE )) ... @@ -468,10 +468,10 @@ WEB3 JSON RPC syntax KItem ::= "#eth_getTransactionCount" // ------------------------------------------- rule #eth_getTransactionCount ... - [ (DATA => #parseHexWord(DATA)), _, .JSONList ] + [ (DATA => #parseHexWord(DATA)), _, .JSONs ] rule #eth_getTransactionCount => #getAccountAtBlock(#parseBlockIdentifier(TAG), DATA) ~> #eth_getTransactionCount ... - [ DATA, TAG, .JSONList ] + [ DATA, TAG, .JSONs ] rule ... NONCE ... ~> #eth_getTransactionCount => #rpcResponseSuccess(#unparseQuantity( NONCE )) ... @@ -482,7 +482,7 @@ WEB3 JSON RPC syntax KItem ::= "#eth_sign" // ---------------------------- rule #eth_sign => #signMessage(KEY, #hashMessage(#unparseByteStack(#parseByteStack(MESSAGE)))) ... - [ ACCTADDR, MESSAGE, .JSONList ] + [ ACCTADDR, MESSAGE, .JSONs ] ... #parseHexWord(ACCTADDR) |-> KEY ... rule #eth_sign => #rpcResponseError(3, "Execution error", [{ "code": 100, "message": "Account key doesn't exist, account locked!" }]) ... @@ -527,27 +527,27 @@ WEB3 JSON RPC syntax KItem ::= "#evm_revert" // ------------------------------ rule #evm_revert => #popNetworkState ~> #rpcResponseSuccess(true) ... - [ DATA:Int, .JSONList ] + [ DATA:Int, .JSONs ] SNAPSHOTS requires DATA ==Int ( size(SNAPSHOTS) -Int 1 ) rule #evm_revert ... - [ (DATA => #parseHexWord(DATA)), .JSONList ] + [ (DATA => #parseHexWord(DATA)), .JSONs ] rule #evm_revert ... - ( [ DATA:Int, .JSONList ] ) + ( [ DATA:Int, .JSONs ] ) ( SNAPSHOTS => range(SNAPSHOTS, 0, DATA ) ) requires size(SNAPSHOTS) >Int (DATA +Int 1) rule #evm_revert => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'evm_revert' requires exactly 1 arguments. Request specified 0 arguments: [null].") ... - [ .JSONList ] + [ .JSONs ] rule #evm_revert => #rpcResponseSuccess(false) ... [owise] syntax KItem ::= "#evm_increaseTime" // ------------------------------------ rule #evm_increaseTime => #rpcResponseSuccess(Int2String(TS +Int DATA)) ... - [ DATA:Int, .JSONList ] + [ DATA:Int, .JSONs ] ( TS:Int => ( TS +Int DATA ) ) syntax KItem ::= "#eth_newBlockFilter" @@ -569,10 +569,10 @@ WEB3 JSON RPC syntax KItem ::= "#eth_uninstallFilter" // --------------------------------------- rule #eth_uninstallFilter ... - [ (DATA => #parseHexWord(DATA)), .JSONList ] + [ (DATA => #parseHexWord(DATA)), .JSONs ] rule #eth_uninstallFilter => #rpcResponseSuccess(true) ... - [ FILTID, .JSONList ] + [ FILTID, .JSONs ] ( FILTID @@ -597,11 +597,11 @@ eth_sendTransaction | "#eth_sendTransaction_final" Int // ------------------------------------------------- rule #eth_sendTransaction => #eth_sendTransaction_load J ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] requires isString( #getJSON("from",J) ) rule #eth_sendTransaction => #rpcResponseError(-32000, "\"from\" field not found; is required") ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] requires notBool isString( #getJSON("from",J) ) rule #eth_sendTransaction => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'eth_sendTransaction' requires exactly 1 argument.") ... [owise] @@ -723,10 +723,10 @@ eth_sendRawTransaction | "#eth_sendRawTransactionSend" Int // ---------------------------------------------------- rule #eth_sendRawTransaction => #eth_sendRawTransactionLoad ... - [ RAWTX:String, .JSONList ] => #rlpDecode( Hex2Raw( RAWTX ) ) + [ RAWTX:String, .JSONs ] => #rlpDecode( Hex2Raw( RAWTX ) ) rule #eth_sendRawTransaction => #rpcResponseError(-32000, "\"value\" argument must not be a number") ... - [ _:Int, .JSONList ] + [ _:Int, .JSONs ] rule #eth_sendRawTransaction => #rpcResponseError(-32000, "Invalid Signature") ... [owise] @@ -735,12 +735,12 @@ eth_sendRawTransaction ~> loadTransaction !ID { "data" : Raw2Hex(TI) , "gas" : Raw2Hex(TG) , "gasPrice" : Raw2Hex(TP) , "nonce" : Raw2Hex(TN) , "r" : Raw2Hex(TR) , "s" : Raw2Hex(TS) , "to" : Raw2Hex(TT) , "v" : Raw2Hex(TW) , "value" : Raw2Hex(TV) - , .JSONList + , .JSONs } ~> #eth_sendRawTransactionVerify !ID ... - [ TN, TP, TG, TT, TV, TI, TW, TR, TS, .JSONList ] + [ TN, TP, TG, TT, TV, TI, TW, TR, TS, .JSONs ] rule #eth_sendRawTransactionLoad => #rpcResponseError(-32000, "Invalid Signature") ... [owise] @@ -776,14 +776,14 @@ Retrieving Blocks syntax KItem ::= "#eth_getBlockByNumber" // ---------------------------------------- rule #eth_getBlockByNumber => #eth_getBlockByNumber_finalize( #getBlockByNumber( #parseBlockIdentifier(TAG), BLOCKLIST)) ... - [ TAG:String, TXOUT:Bool, .JSONList ] + [ TAG:String, TXOUT:Bool, .JSONs ] BLOCKLIST rule #eth_getBlockByNumber => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'eth_getBlockByNumber' requires exactly 2 arguments.") ... - [ VALUE, .JSONList ] + [ VALUE, .JSONs ] requires notBool isJSONs( VALUE ) rule #eth_getBlockByNumber => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'eth_getBlockByNumber' requires exactly 2 arguments.") ... - [ VALUE, VALUE2, _, .JSONList ] + [ VALUE, VALUE2, _, .JSONs ] requires notBool isJSONs( VALUE ) andBool notBool isJSONs( VALUE2 ) syntax KItem ::= "#eth_getBlockByNumber_finalize" "(" BlockchainItem ")" @@ -826,7 +826,7 @@ Retrieving Blocks , "gasUsed": #unparseQuantity( GUSED ) , "timestamp": #unparseQuantity( TIME ) , "transactions": [ #getTransactionList( BLOCKITEM ) ] - , "uncles": [ .JSONList ] + , "uncles": [ .JSONs ] } ) ... @@ -834,13 +834,13 @@ Retrieving Blocks rule #eth_getBlockByNumber_finalize ( .BlockchainItem )=> #rpcResponseSuccess(null) ... - syntax JSONList ::= "#getTransactionList" "(" BlockchainItem ")" [function] - | #getTransactionHashList ( List, JSONList ) [function] - // --------------------------------------------------------------------------- + syntax JSONs ::= "#getTransactionList" "(" BlockchainItem ")" [function] + | #getTransactionHashList ( List, JSONs ) [function] + // ------------------------------------------------------------------------ rule [[ #getTransactionList ( { TXIDLIST ... | _ } ) - => #getTransactionHashList (TXIDLIST, .JSONList) + => #getTransactionHashList (TXIDLIST, .JSONs) ]] - [ _ , false, .JSONList ] + [ _ , false, .JSONs ] rule #getTransactionHashList ( .List, RESULT ) => RESULT rule [[ #getTransactionHashList ( ( ListItem(TXID) => .List ) TXIDLIST, ( RESULT => TXHASH, RESULT ) ) ]] @@ -901,7 +901,7 @@ Transaction Receipts | "#eth_getTransactionReceipt_final" "(" BlockchainItem ")" // -------------------------------------------------------------------------- rule #eth_getTransactionReceipt => #eth_getTransactionReceipt_final(#getBlockByNumber (BN, BLOCKLIST)) ... - [TXHASH:String, .JSONList] + [TXHASH:String, .JSONs] TXHASH BN @@ -947,7 +947,7 @@ Transaction Receipts ) ... - [TXHASH:String, .JSONList] + [TXHASH:String, .JSONs] TXHASH TXID @@ -976,18 +976,18 @@ Transaction Receipts rule #unparseAccount (.Account) => null rule #unparseAccount (ACCT:Int) => #unparseQuantity(ACCT) - syntax JSONList ::= #unparseIntList ( List ) [function] - // ------------------------------------------------------- - rule #unparseIntList (L) => #unparseIntListAux( L, .JSONList) + syntax JSONs ::= #unparseIntList ( List ) [function] + // ---------------------------------------------------- + rule #unparseIntList (L) => #unparseIntListAux( L, .JSONs) - syntax JSONList ::= #unparseIntListAux ( List, JSONList ) [function] - // -------------------------------------------------------------------- + syntax JSONs ::= #unparseIntListAux ( List, JSONs ) [function] + // -------------------------------------------------------------- rule #unparseIntListAux(.List, RESULT) => RESULT rule #unparseIntListAux(L ListItem(I), RESULT) => #unparseIntListAux(L, (#unparseDataByteArray(#padToWidth(32,#asByteStack(I))), RESULT)) - syntax JSONList ::= #serializeLogs ( List, Int, Int, String, Int, Int ) [function] - // ---------------------------------------------------------------------------------- - rule #serializeLogs (.List, _, _, _, _, _) => .JSONList + syntax JSONs ::= #serializeLogs ( List, Int, Int, String, Int, Int ) [function] + // ------------------------------------------------------------------------------- + rule #serializeLogs (.List, _, _, _, _, _) => .JSONs rule #serializeLogs (ListItem({ ACCT | TOPICS:List | DATA }) L, LI, TI, TH, BH, BN) => { "logIndex": #unparseQuantity(LI), "transactionIndex": #unparseQuantity(TI), @@ -1196,11 +1196,11 @@ Transaction Receipts syntax KItem ::= "#personal_importRawKey" // ----------------------------------------- rule #personal_importRawKey => #acctFromPrivateKey PRIKEY ~> #rpcResponseSuccess(#unparseData( #addrFromPrivateKey( PRIKEY ), 20 )) ... - [ PRIKEY:String, PASSPHRASE:String, .JSONList ] + [ PRIKEY:String, PASSPHRASE:String, .JSONs ] requires lengthString( PRIKEY ) ==Int 66 rule #personal_importRawKey => #rpcResponseError(-32000, "Private key length is invalid. Must be 32 bytes.") ... - [ PRIKEY:String, _:String, .JSONList ] + [ PRIKEY:String, _:String, .JSONs ] requires lengthString( PRIKEY ) =/=Int 66 rule #personal_importRawKey => #rpcResponseError(-32000, "Method 'personal_importRawKey' requires exactly 2 parameters") ... [owise] @@ -1213,30 +1213,30 @@ Transaction Receipts syntax KItem ::= "#firefly_addAccount" | "#firefly_addAccountByAddress" Int | "#firefly_addAccountByKey" String // --------------------------------------------------------------------------------------------------------------- rule #firefly_addAccount => #firefly_addAccountByAddress #parseHexWord(#getString("address", J)) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] requires isString(#getJSON("address", J)) rule #firefly_addAccount => #firefly_addAccountByKey #getString("key", J) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] requires isString(#getJSON("key", J)) rule #firefly_addAccountByAddress ACCT_ADDR => #newAccount ACCT_ADDR ~> loadAccount ACCT_ADDR J ~> #rpcResponseSuccess(true) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] ACCTS requires notBool ACCT_ADDR in ACCTS rule #firefly_addAccountByAddress ACCT_ADDR => #rpcResponseSuccess(false) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] ACCTS requires ACCT_ADDR in ACCTS rule #firefly_addAccountByKey ACCT_KEY => #acctFromPrivateKey ACCT_KEY ~> loadAccount #addrFromPrivateKey(ACCT_KEY) J ~> #rpcResponseSuccess(true) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] ACCTS requires notBool #addrFromPrivateKey(ACCT_KEY) in ACCTS rule #firefly_addAccountByKey ACCT_KEY => #rpcResponseSuccess(false) ... - [ ({ _ } #as J), .JSONList ] + [ ({ _ } #as J), .JSONs ] ACCTS requires #addrFromPrivateKey(ACCT_KEY) in ACCTS @@ -1245,7 +1245,7 @@ Transaction Receipts rule loadAccount _ { "balance" : ((VAL:String) => #parseHexWord(VAL)), _ } ... rule loadAccount _ { "nonce" : ((VAL:String) => #parseHexWord(VAL)), _ } ... rule loadAccount _ { "code" : ((CODE:String) => #parseByteStack(CODE)), _ } ... - rule loadAccount _ { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })), _ } ... + rule loadAccount _ { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })), _ } ... rule loadAccount _ { "key" : _, REST => REST } ... rule loadAccount _ { "address" : _, REST => REST } ... ``` @@ -1267,12 +1267,12 @@ Transaction Receipts ~> #eth_call_finalize ... - [ ({ _ } #as J), TAG, .JSONList ] + [ ({ _ } #as J), TAG, .JSONs ] requires isString( #getJSON("to", J) ) andBool isString(#getJSON("from",J) ) rule #eth_call => #rpcResponseError(-32027, "Method 'eth_call' has invalid arguments") ... - [ ({ _ } #as J), TAG, .JSONList ] + [ ({ _ } #as J), TAG, .JSONs ] requires notBool isString( #getJSON("from", J) ) syntax KItem ::= "#eth_call_finalize" @@ -1304,12 +1304,12 @@ Transaction Receipts ~> #eth_estimateGas_finalize GUSED ... - [ ({ _ } #as J), TAG, .JSONList ] + [ ({ _ } #as J), TAG, .JSONs ] GUSED requires isString(#getJSON("from", J) ) rule #eth_estimateGas => #rpcResponseError(-32028, "Method 'eth_estimateGas' has invalid arguments") ... - [ ({ _ } #as J), TAG, .JSONList ] + [ ({ _ } #as J), TAG, .JSONs ] requires notBool isString( #getJSON("from", J) ) syntax KItem ::= "#eth_estimateGas_finalize" Int @@ -1424,30 +1424,30 @@ Collecting Coverage Data "programs": [#serializePrograms(keys_list(PGMS),PGMS)] } - syntax JSONList ::= #serializeCoverage ( List, Map ) [function] - // --------------------------------------------------------------- - rule #serializeCoverage (.List, _ ) => .JSONList - rule #serializeCoverage ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:Set COVERAGE:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [IntList2JSONList(qsort(Set2List(X)))] }}, #serializeCoverage(KEYS, COVERAGE) + syntax JSONs ::= #serializeCoverage ( List, Map ) [function] + // ------------------------------------------------------------ + rule #serializeCoverage (.List, _ ) => .JSONs + rule #serializeCoverage ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:Set COVERAGE:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [IntList2JSONs(qsort(Set2List(X)))] }}, #serializeCoverage(KEYS, COVERAGE) - syntax JSONList ::= #serializePrograms ( List, Map ) [function] - // --------------------------------------------------------------- - rule #serializePrograms (.List, _ ) => .JSONList - rule #serializePrograms ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:List PGMS:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [CoverageIDList2JSONList(X)] }}, #serializePrograms(KEYS, PGMS) + syntax JSONs ::= #serializePrograms ( List, Map ) [function] + // ------------------------------------------------------------ + rule #serializePrograms (.List, _ ) => .JSONs + rule #serializePrograms ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:List PGMS:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [CoverageIDList2JSONs(X)] }}, #serializePrograms(KEYS, PGMS) syntax String ::= Phase2String ( Phase ) [function] // ---------------------------------------------------- rule Phase2String (CONSTRUCTOR) => "CONSTRUCTOR" rule Phase2String (RUNTIME) => "RUNTIME" - syntax JSONList ::= CoverageIDList2JSONList ( List ) [function] - // --------------------------------------------------------------- - rule CoverageIDList2JSONList (.List) => .JSONList - rule CoverageIDList2JSONList (ListItem({I:Int | _:OpCode }) L) => I, CoverageIDList2JSONList(L) + syntax JSONs ::= CoverageIDList2JSONs ( List ) [function] + // --------------------------------------------------------- + rule CoverageIDList2JSONs (.List) => .JSONs + rule CoverageIDList2JSONs (ListItem({I:Int | _:OpCode }) L) => I, CoverageIDList2JSONs(L) - syntax JSONList ::= IntList2JSONList ( List ) [function] - // -------------------------------------------------------- - rule IntList2JSONList (.List) => .JSONList - rule IntList2JSONList (ListItem(I:Int) L) => I, IntList2JSONList(L) + syntax JSONs ::= IntList2JSONs ( List ) [function] + // -------------------------------------------------- + rule IntList2JSONs (.List) => .JSONs + rule IntList2JSONs (ListItem(I:Int) L) => I, IntList2JSONs(L) syntax List ::= getIntElementsSmallerThan ( Int, List, List ) [function] // ------------------------------------------------------------------------ @@ -1466,9 +1466,9 @@ Collecting Coverage Data rule qsort ( .List ) => .List rule qsort (ListItem(I:Int) L) => qsort(getIntElementsSmallerThan(I, L, .List)) ListItem(I) qsort(getIntElementsGreaterThan(I, L, .List)) - syntax JSONList ::= #coveragePercentages ( List, Map, Map) [function] - // --------------------------------------------------------------------- - rule #coveragePercentages (.List, _, _) => .JSONList + syntax JSONs ::= #coveragePercentages ( List, Map, Map) [function] + // ------------------------------------------------------------------ + rule #coveragePercentages (.List, _, _) => .JSONs rule #coveragePercentages ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:Set COVERAGE:Map, KEY |-> Y:List PGMS:Map) => { Int2String(CODEHASH):{ Phase2String(EPHASE): #computePercentage(size(X),size(Y)) }}, #coveragePercentages(KEYS,COVERAGE,PGMS) syntax Int ::= #computePercentage ( Int, Int ) [function] @@ -1696,7 +1696,7 @@ Timestamp Calls syntax KItem ::= "#firefly_setTime" // ----------------------------------- rule #firefly_setTime => #rpcResponseSuccess(true) ... - [ TIME:String, .JSONList ] + [ TIME:String, .JSONs ] _ => #parseHexWord( TIME ) rule #firefly_setTime => #rpcResponseSuccess(false) ... [owise] @@ -1709,11 +1709,11 @@ Gas Limit Call syntax KItem ::= "#firefly_setGasLimit" // --------------------------------------- rule #firefly_setGasLimit => #rpcResponseSuccess(true) ... - [ GLIMIT:String, .JSONList ] + [ GLIMIT:String, .JSONs ] _ => #parseWord( GLIMIT ) rule #firefly_setGasLimit => #rpcResponseSuccess(true) ... - [ GLIMIT:Int, .JSONList ] + [ GLIMIT:Int, .JSONs ] _ => GLIMIT rule #firefly_setGasLimit => #rpcResponseError(-32000, "firefly_setGasLimit requires exactly 1 argument") ... [owise] @@ -1728,11 +1728,11 @@ Mining rule #evm_mine => #mineBlock ~> #rpcResponseSuccess("0x0") ... [owise] rule #evm_mine => #mineBlock ~> #rpcResponseSuccess("0x0") ... - [ TIME:String, .JSONList ] + [ TIME:String, .JSONs ] _ => #parseWord( TIME ) rule #evm_mine => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'evm_mine' requires between 0 and 1 arguments.") ... - [ _ , _ , _:JSONList ] + [ _ , _ , _:JSONs ] syntax KItem ::= "#firefly_genesisBlock" // ----------------------------------------