Remove sort JSONList (#584)

* *.md, tests/*: rename sort JSONList => JSONs * web3: remaining renames
runtimeverification · Dec 2, 2019 · 16ac53f · 16ac53f
1 parent 62b5439
commit 16ac53f
Show file tree

Hide file tree

Showing 6 changed files with 179 additions and 184 deletions.
diff --git 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 <Int lengthString(STR)
-    rule #rlpDecodeList(STR, 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
@@ -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 <String KEY'
     rule #insertJSONKey( (KEY : VAL) , ((KEY' : VAL') , REST) ) => (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 <k> run { .JSONList } => . ... </k>
-    rule <k> run { TESTID : { TEST:JSONList } , TESTS }
-          => run ( TESTID : { #sortJSONList(TEST) } )
+    rule <k> run { .JSONs } => . ... </k>
+    rule <k> 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 <k> run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
       requires KEY in #loadKeys
 
-    rule <k> run TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, .JSONList ] , ( REST2 => KEY : VAL , REST2 ) } ... </k>
-    rule <k> run TESTID : { "blocks" : [ { .JSONList }, .JSONList ] , REST } => run TESTID : { REST }                   ... </k>
+    rule <k> run TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, .JSONs ] , ( REST2 => KEY : VAL , REST2 ) } ... </k>
+    rule <k> run TESTID : { "blocks" : [ { .JSONs }, .JSONs ] , REST } => run TESTID : { REST }                      ... </k>
 ```
 
 -   `#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 <k> load "account" : { ACCTID : ACCT } => loadAccount ACCTID ACCT ... </k>
 
-    rule <k> loadAccount _ { "balance" : ((VAL:String)         => #parseWord(VAL)),        _ } ... </k>
-    rule <k> loadAccount _ { "nonce"   : ((VAL:String)         => #parseWord(VAL)),        _ } ... </k>
-    rule <k> loadAccount _ { "code"    : ((CODE:String)        => #parseByteStack(CODE)),  _ } ... </k>
-    rule <k> loadAccount _ { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })), _ } ... </k>
+    rule <k> loadAccount _ { "balance" : ((VAL:String)      => #parseWord(VAL)),        _ } ... </k>
+    rule <k> loadAccount _ { "nonce"   : ((VAL:String)      => #parseWord(VAL)),        _ } ... </k>
+    rule <k> loadAccount _ { "code"    : ((CODE:String)     => #parseByteStack(CODE)),  _ } ... </k>
+    rule <k> loadAccount _ { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })), _ } ... </k>
 
     rule <k> loadTransaction _ { "gasLimit" : (TG:String => #asWord(#parseByteStackRaw(TG))), _      } ... </k>
     rule <k> loadTransaction _ { "gasPrice" : (TP:String => #asWord(#parseByteStackRaw(TP))), _      } ... </k>
@@ -344,27 +344,27 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
  // ---------------------------------------
     rule <k> #halt ~> check J:JSON => check J ~> #halt ... </k>
 
-    rule <k> check DATA : { .JSONList } => . ... </k> requires DATA =/=String "transactions"
-    rule <k> check DATA : [ .JSONList ] => . ... </k> requires DATA =/=String "ommerHeaders"
+    rule <k> check DATA : { .JSONs } => . ... </k> requires DATA =/=String "transactions"
+    rule <k> check DATA : [ .JSONs ] => . ... </k> requires DATA =/=String "ommerHeaders"
 
     rule <k> check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST } ... </k>
-      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 <k> check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] ... </k>
       requires DATA =/=String "transactions"
 
-    rule <k> check (KEY:String) : { JS:JSONList => #sortJSONList(JS) } ... </k>
+    rule <k> check (KEY:String) : { JS:JSONs => #sortJSONs(JS) } ... </k>
       requires KEY in (SetItem("callcreates")) andBool notBool #isSorted(JS)
 
     rule <k> check TESTID : { "post" : POST } => check "account" : POST ~> failure TESTID ... </k>
     rule <k> check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ... </k>
-      requires REST =/=K .JSONList
+      requires REST =/=K .JSONs
 
     rule <k> check "account" : { ((ACCTID:String) => #parseAddr(ACCTID)) : ACCT }                                ... </k>
-    rule <k> check "account" : { (ACCT:Int) : { "balance" : ((VAL:String)         => #parseWord(VAL)) } }        ... </k>
-    rule <k> check "account" : { (ACCT:Int) : { "nonce"   : ((VAL:String)         => #parseWord(VAL)) } }        ... </k>
-    rule <k> check "account" : { (ACCT:Int) : { "code"    : ((CODE:String)        => #parseByteStack(CODE)) } }  ... </k>
-    rule <k> check "account" : { (ACCT:Int) : { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })) } } ... </k>
+    rule <k> check "account" : { (ACCT:Int) : { "balance" : ((VAL:String)      => #parseWord(VAL)) } }        ... </k>
+    rule <k> check "account" : { (ACCT:Int) : { "nonce"   : ((VAL:String)      => #parseWord(VAL)) } }        ... </k>
+    rule <k> check "account" : { (ACCT:Int) : { "code"    : ((CODE:String)     => #parseByteStack(CODE)) } }  ... </k>
+    rule <k> check "account" : { (ACCT:Int) : { "storage" : ({ STORAGE:JSONs } => #parseMap({ STORAGE })) } } ... </k>
 
     rule <mode> EXECMODE </mode>
          <k> check "account" : { ACCT : { "balance" : (BAL:Int) } } => . ... </k>
@@ -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 <k> check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... </k>
-      requires REST =/=K .JSONList
+      requires REST =/=K .JSONs
 
     rule <k> check "blockHeader" : { KEY : (VALUE:String => #parseByteStack(VALUE)) } ... </k>
 
@@ -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 <k> check "genesisBlockHeader" : { KEY : VALUE , REST } => check "genesisBlockHeader" : { KEY : VALUE } ~> check "genesisBlockHeader" : { REST } ... </k>
-      requires REST =/=K .JSONList
+      requires REST =/=K .JSONs
 
     rule <k> check "genesisBlockHeader" : { KEY : VALUE } => .K ... </k> requires KEY =/=String "hash"
 
@@ -489,8 +489,8 @@ Here we check the other post-conditions associated with an EVM test.
 
     rule <k> check TESTID : { "transactions" : TRANSACTIONS } => check "transactions" : TRANSACTIONS ~> failure TESTID ... </k>
  // ---------------------------------------------------------------------------------------------------------------------------
-    rule <k> check "transactions" : [ .JSONList ] => . ... </k> <txOrder> .List                    </txOrder>
-    rule <k> check "transactions" : { .JSONList } => . ... </k> <txOrder> ListItem(_) => .List ... </txOrder>
+    rule <k> check "transactions" : [ .JSONs ] => . ... </k> <txOrder> .List                    </txOrder>
+    rule <k> check "transactions" : { .JSONs } => . ... </k> <txOrder> ListItem(_) => .List ... </txOrder>
 
     rule <k> check "transactions" : [ TRANSACTION , REST ] => check "transactions" : TRANSACTION   ~> check "transactions" : [ REST ] ... </k>
     rule <k> check "transactions" : { KEY : VALUE , REST } => check "transactions" : (KEY : VALUE) ~> check "transactions" : { REST } ... </k>
@@ -516,7 +516,7 @@ TODO: case with nonzero ommers.
 ```k
     rule <k> check TESTID : { "uncleHeaders" : OMMERS } => check "ommerHeaders" : OMMERS ~> failure TESTID ... </k>
  // ---------------------------------------------------------------------------------------------------------------
-    rule <k> check "ommerHeaders" : [ .JSONList ] => . ... </k> <ommerBlockHeaders> [ .JSONList ] </ommerBlockHeaders>
+    rule <k> check "ommerHeaders" : [ .JSONs ] => . ... </k> <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
 ```
 
 ```k

diff --git 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
               <mixHash>          0          </mixHash>          // I_Hm
               <blockNonce>       0          </blockNonce>       // I_Hn
 
-              <ommerBlockHeaders> [ .JSONList ] </ommerBlockHeaders>
+              <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
             </block>
 
           </evm>
@@ -658,8 +658,8 @@ After executing a transaction, it's necessary to have the effect of the substate
          <log> _ => .List </log>
          <logsBloom> _ => #padToWidth(256, .ByteArray) </logsBloom>
 
-    syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList )
- // ------------------------------------------------------------------------
+    syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONs )
+ // ---------------------------------------------------------------------
     rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
          <schedule> SCHED </schedule>
          <ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
@@ -677,7 +677,7 @@ After executing a transaction, it's necessary to have the effect of the substate
          <activeAccounts> ACCTS </activeAccounts>
       requires notBool MINER in ACCTS
 
-    rule <k> #rewardOmmers(.JSONList) => . ... </k>
+    rule <k> #rewardOmmers(.JSONs) => . ... </k>
     rule <k> #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... </k>
          <schedule> SCHED </schedule>
          <coinbase> MINER </coinbase>