Json refactors and cleanups

data.md

@@ -16,7 +16,7 @@ module EVM-DATA
     imports STRING-BUFFER
     imports MAP-SYMBOLIC
     imports COLLECTIONS
-    imports JSON
+    imports JSON-EXT
 ```
 
 ```{.k .concrete .bytes}

driver.md

@@ -39,25 +39,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 ```k
     syntax JSON ::= ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
  // -----------------------------------------------------------------------------
-
-    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 ( JSONs ) [function]
- // ----------------------------------------------
-    rule #isSorted( .JSONs  ) => true
-    rule #isSorted( KEY : _ ) => true
-    rule #isSorted( (KEY : _) , (KEY' : VAL) , REST ) => KEY <=String KEY' andThenBool #isSorted((KEY' : VAL) , REST)
 ```
 
 ### Driving Execution
@@ -229,7 +210,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
  // -------------------------------------
     rule <k> run { .JSONs } => . ... </k>
     rule <k> run { TESTID : { TEST:JSONs } , TESTS }
-          => run ( TESTID : { #sortJSONs(TEST) } )
+          => run ( TESTID : { qsortJSONs(TEST) } )
           ~> #if #hasPost?( { TEST } ) #then .K #else exception #fi
           ~> clear
           ~> run { TESTS }
@@ -353,8 +334,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     rule <k> check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] ... </k>
       requires DATA =/=String "transactions"
 
-    rule <k> check (KEY:String) : { JS:JSONs => #sortJSONs(JS) } ... </k>
-      requires KEY in (SetItem("callcreates")) andBool notBool #isSorted(JS)
+    rule <k> check (KEY:String) : { JS:JSONs => qsortJSONs(JS) } ... </k>
+      requires KEY in (SetItem("callcreates")) andBool notBool sortedJSONs(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>

json.md

@@ -1,7 +1,11 @@
-### JSON Formatting
+KJSON
+=====
 
-The JSON format is used extensively for communication in the Ethereum circles.
-Writing a JSON-ish parser in K takes 6 lines.
+This is a non-faithful implementation of the [ECMA-404 JSON Data Interchange Format](http://www.ecma-international.org/publications/files/ECMA-ST/ECMA-404.pdf).
+There are issues with how `JSONNumber` and `JSONString` are specified here, because we use K's `String` and `Int` sort directly, which are not quite correct.
+
+JSON Syntax
+-----------
 
 ```k
 module JSON
@@ -12,16 +16,36 @@ module JSON
     syntax JSONs   ::= List{JSON,","}      [klabel(JSONs)      , symbol]
     syntax JSONKey ::= String
     syntax JSON    ::= "null"              [klabel(JSONnull)   , symbol]
-                     | String | Int | Bool
+                     | JSONKey | Bool
                      | JSONKey ":" JSON    [klabel(JSONEntry)  , symbol]
                      | "{" JSONs "}"       [klabel(JSONObject) , symbol]
                      | "[" JSONs "]"       [klabel(JSONList)   , symbol]
  // --------------------------------------------------------------------
 ```
 
+```k
+endmodule
+```
+
+JSON Extensions
+---------------
+
+Some common functions and extensions of JSON are provided here.
+
+```k
+module JSON-EXT
+    imports JSON
+```
+
+-   `+JSONs` appends two JSON lists.
 -   `reverseJSONs` reverses a JSON list.
 
 ```k
+    syntax JSONs ::= JSONs "+JSONs" JSONs [function]
+ // ------------------------------------------------
+    rule .JSONs   +JSONs JS' => JS'
+    rule (J , JS) +JSONs JS' => J , (JS +JSONs JS')
+
     syntax JSONs ::= reverseJSONs    ( JSONs         ) [function]
                    | reverseJSONsAux ( JSONs , JSONs ) [function]
  // -------------------------------------------------------------
@@ -31,6 +55,32 @@ module JSON
     rule reverseJSONsAux((J, JS:JSONs), JS') => reverseJSONsAux(JS, (J, JS'))
 ```
 
+-   `qsortJSONs` quick-sorts a list of key-value pairs.
+-   `sortedJSONs` is a predicate saying whether a given list of JSONs is sorted or not.
+
+```k
+    syntax JSONs ::= qsortJSONs ( JSONs )          [function]
+                   | #entriesLT ( String , JSONs ) [function]
+                   | #entriesGE ( String , JSONs ) [function]
+ // ---------------------------------------------------------
+    rule qsortJSONs(.JSONs)            => .JSONs
+    rule qsortJSONs(KEY : VALUE, REST) => qsortJSONs(#entriesLT(KEY, REST)) +JSONs (KEY : VALUE , qsortJSONs(#entriesGE(KEY, REST)))
+
+    rule #entriesLT(KEY, .JSONs)              => .JSONs
+    rule #entriesLT(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesLT(KEY, REST) requires         KEY' <String KEY
+    rule #entriesLT(KEY, (KEY': VALUE, REST)) =>               #entriesLT(KEY, REST) requires notBool KEY' <String KEY
+
+    rule #entriesGE(KEY, .JSONs)              => .JSONs
+    rule #entriesGE(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesGE(KEY, REST) requires         KEY' >=String KEY
+    rule #entriesGE(KEY, (KEY': VALUE, REST)) =>               #entriesGE(KEY, REST) requires notBool KEY' >=String KEY
+
+    syntax Bool ::= sortedJSONs ( JSONs ) [function]
+ // ------------------------------------------------
+    rule sortedJSONs( .JSONs  ) => true
+    rule sortedJSONs( KEY : _ ) => true
+    rule sortedJSONs( (KEY : _) , (KEY' : VAL) , REST ) => KEY <=String KEY' andThenBool sortedJSONs((KEY' : VAL) , REST)
+```
+
 **TODO**: Adding `Int` to `JSONKey` is a hack to make certain parts of semantics easier.
 
 ```k
@@ -49,7 +99,7 @@ JSON-RPC
 module JSON-RPC
     imports K-IO
     imports LIST
-    imports JSON
+    imports JSON-EXT
 
     configuration
       <json-rpc>

serialization.md

@@ -12,7 +12,7 @@ module SERIALIZATION
     imports KRYPTO
     imports EVM-TYPES
     imports STRING-BUFFER
-    imports JSON
+    imports JSON-EXT
 ```
 
 Address/Hash Helpers

state-loader.md

@@ -1,7 +1,7 @@
 State Manager
 -------------
 
-```{.k}
+```k
 requires "evm.k"
 requires "asm.k"
 
@@ -19,7 +19,7 @@ module STATE-LOADER
 -   `clear` clears all the execution state of the machine.
 -   `clearX` clears the substate `X`, for `TX`, `BLOCK`, and `NETWORK`.
 
-```{.k}
+```k
     syntax EthereumCommand ::= "clear"
  // ----------------------------------
     rule <k> clear => clearTX ~> clearBLOCK ~> clearNETWORK ... </k>
@@ -84,15 +84,15 @@ module STATE-LOADER
 
 -   `mkAcct_` creates an account with the supplied ID (assuming it's already been chopped to 160 bits).
 
-```{.k}
+```k
     syntax EthereumCommand ::= "mkAcct" Int
  // ---------------------------------------
     rule <k> mkAcct ACCT => #newAccount ACCT ... </k>
 ```
 
 -   `load` loads an account or transaction into the world state.
 
-```{.k}
+```k
     syntax EthereumCommand ::= "load" JSON
  // --------------------------------------
     rule <k> load DATA : { .JSONs }             => .                                                   ... </k>
@@ -105,7 +105,7 @@ module STATE-LOADER
 
 Here we perform pre-proccesing on account data which allows "pretty" specification of input.
 
-```{.k}
+```k
     rule <k> load "pre" : { (ACCTID:String) : ACCT } => mkAcct #parseAddr(ACCTID) ~> loadAccount #parseAddr(ACCTID) ACCT ... </k>
 
     syntax EthereumCommand ::= "loadAccount" Int JSON
@@ -127,7 +127,7 @@ Here we perform pre-proccesing on account data which allows "pretty" specificati
 
 Here we load the environmental information.
 
-```{.k}
+```k
     rule <k> load "env" : { KEY : ((VAL:String) => #parseWord(VAL)) } ... </k>
       requires KEY in (SetItem("currentTimestamp") SetItem("currentGasLimit") SetItem("currentNumber") SetItem("currentDifficulty"))
     rule <k> load "env" : { KEY : ((VAL:String) => #parseHexWord(VAL)) } ... </k>
@@ -158,7 +158,7 @@ Here we load the environmental information.
 
 The `"network"` key allows setting the fee schedule inside the test.
 
-```{.k}
+```k
     rule <k> load "network" : SCHEDSTRING => . ... </k>
          <schedule> _ => #asScheduleString(SCHEDSTRING) </schedule>
 
@@ -176,7 +176,7 @@ The `"network"` key allows setting the fee schedule inside the test.
 
 The `"rlp"` key loads the block information.
 
-```{.k}
+```k
     rule <k> load "rlp"        : (VAL:String => #rlpDecode(#unparseByteStack(#parseByteStack(VAL)))) ... </k>
     rule <k> load "genesisRLP" : (VAL:String => #rlpDecode(#unparseByteStack(#parseByteStack(VAL)))) ... </k>
  // ---------------------------------------------------------------------------------------------------------
@@ -267,7 +267,7 @@ The `"rlp"` key loads the block information.
 
 ### Block Identifiers
 
-```{.k}
+```k
     syntax BlockIdentifier ::= Int
                              | "LATEST"
                              | "PENDING"
@@ -281,6 +281,6 @@ The `"rlp"` key loads the block information.
     rule #parseBlockIdentifier("earliest") => EARLIEST
     rule #parseBlockIdentifier(BLOCKNUM)   => #parseHexWord(BLOCKNUM) requires substrString(BLOCKNUM,0,2) ==String "0x"
 ```
-```{.k}
+```k
 endmodule
 ```