Objects in canonical form: sorting entries, and splitting an object between surfaces
A canonical ESM document has the keys of every object in strictly increasing order (the sorted-key canonical serialization). The document printer takes an object apart: some entries get a surface of their own (a declaration, a component directive), the rest is printed as a path block. The parser collects the entries back from wherever they were written, in whatever order, and sorts them. This module holds the two facts that make that sound:
sortKeys_ext: sorting a list that holds, key by key, the same entries as a canonical object gives that object;joinField_splitField: an object-valued field split between its own surfaces and a residue block is rebuilt exactly.
Equality of values
Decided structurally, so a decoder can check a candidate by encoding it again.
Sorting by key
def sortKeys (l : List (String × Json)) : List (String × Json)
The entries ordered by key (a stable merge sort).
def at_ (k : String) (l : List (String × Json)) : List (String × Json)
The entries of l with key k.
theorem sortKeys_eq {l l' : List (String × Json)} (hp : l.Perm l') (hs : keysSorted l' = true) :
sortKeys l = l'
Sorting a permutation of a canonical (strictly key-sorted) list gives that list.
theorem sortKeys_ext {R l : List (String × Json)} (hl : keysSorted l = true)
(h : ∀ k, at_ k R = at_ k l) : sortKeys R = l
Key-by-key extensionality. A list holding, for every key, exactly the entries a canonical list holds sorts to that list.
theorem at_of_sorted {l : List (String × Json)} (hl : keysSorted l = true) (k : String) :
at_ k l = match look k l with
In a canonical list, the entries with key k are the one look finds, or none.
Splitting an object-valued field
def splitField {β : Type} (pick : String → Json → Option β) : Json → List β × Option Json
The entries of an object-valued field that get a surface of their own (pick
returns their piece) and the residue, printed as a path block under the field’s key.
A value that is not an object is all residue. The residue block is omitted only when
some entry was picked and none is left; an object none of whose entries is picked
(including {}) is all residue, so an absent field and an empty one stay apart.
def splitOpt {β : Type} (pick : String → Json → Option β) : Option Json → List β × Option Json
splitField
of a field that may be absent.
def joinField {β : Type} (back : β → Option (String × Json)) (ps : List β) (r : Option Json) :
Option (Option Json)
The field rebuilt from its pieces (each mapped back to its entry) and its residue:
none when they do not fit together, some none when the field is absent.
theorem joinField_splitField {β : Type} (pick : String → Json → Option β)
(back : β → Option (String × Json)) (v : Json)
(hv : ∀ kvs, v = .obj kvs → keysSorted kvs = true)
(hb : ∀ kvs, v = .obj kvs → ∀ k w p, (k, w) ∈ kvs → pick k w = some p → back p = some (k, w)) :
joinField back (splitField pick v).1 (splitField pick v).2 = some (some v)
The split field is rebuilt exactly, when every piece maps back to its entry.
theorem joinField_splitOpt {β : Type} (pick : String → Json → Option β)
(back : β → Option (String × Json)) (o : Option Json)
(hv : ∀ kvs, o = some (.obj kvs) → keysSorted kvs = true)
(hb : ∀ kvs, o = some (.obj kvs) →
∀ k w p, (k, w) ∈ kvs → pick k w = some p → back p = some (k, w)) :
joinField back (splitOpt pick o).1 (splitOpt pick o).2 = some o
The same, for a field that may be absent.
theorem splitField_fst {β : Type} (pick : String → Json → Option β) (v : Json) :
(splitField pick v).1 = (match v with
| .obj kvs => kvs.filterMap (fun kv => pick kv.1 kv.2)
| _ => [])
The pieces of a split field are the picks of its entries.