1 import Base 2 import ../spec/cache.bend as S 3 import ../spec/operations.bend as O 4 import ../spec/equivalence.bend as E 5 import ../types/model.bend as T 6 import ./map_routing.bend as Routing 7 8 # Generic algebra of the independent canonical model form (spec/equivalence). 9 # Key equality contracts are explicit; the String instance discharges them. 10 11 def reflects(~K: Data, ~same: K -> K -> Bool) -> Type: 12 @+a: K -> @+b: K -> {same(a)(b) == True{} : Bool} -> {a == b : K} 13 14 def reflexive(~K: Data, ~same: K -> K -> Bool) -> Type: 15 @+a: K -> {same(a)(a) == True{} : Bool} 16 17 def clash(x: Bool, yes: {x == True{} : Bool}, no: {x == False{} : Bool}) -> Empty: 18 Routing.false_true(Equal.trans(Bool, False{}, x, True{}, Equal.sym(Bool, x, False{}, no), yes)) 19 20 def moved(~K: Data, ~same: K -> K -> Bool, order: List<&2, K>, +key: K) -> List<&2, K>: 21 List.append(&2, K, S.unlist(~K, ~same, order, key), Con{key, Nil{}}) 22 23 def or_false(b: Bool) -> {Bool.or(b, False{}) == b : Bool}: 24 match b: 25 case False{}: {==} 26 case True{}: {==} 27 28 def or_true(b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}: 29 match b: 30 case False{}: {==} 31 case True{}: {==} 32 33 # Symmetry of an inequality from reflection and reflexivity. 34 def symmetric_decide(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), +a: K, +b: K, no: {same(a)(b) == False{} : Bool}, r: Bool, e: {same(b)(a) == r : Bool}) -> {same(b)(a) == False{} : Bool}: 35 match r: 36 case False{}: e 37 case True{}: 38 eq = refl(b, a, e) 39 self = Equal.trans(Bool, same(a)(a), same(a)(b), False{}, Equal.cong(K, Bool, x => same(a)(x), a, b, Equal.sym(K, b, a, eq)), no) 40 Empty.absurd({same(b)(a) == False{} : Bool}, clash(same(a)(a), rfx(a), self)) 41 42 def symmetric_false(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), +a: K, +b: K, no: {same(a)(b) == False{} : Bool}) -> {same(b)(a) == False{} : Bool}: 43 symmetric_decide(~K, ~same, ~refl, ~rfx, a, b, no, same(b)(a), {==}) 44 45 # A binding matching q is not removed by erasing a key different from q. 46 def erase_other_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +k: K, +v: V, +d: T.Int64, +t: List<&2, T.Entry>, +key: K, +q: K, +h: {same(q)(key) == False{} : Bool}, x: Bool, +ex: {same(k)(key) == x : Bool}, y: Bool, +ey: {same(k)(q) == y : Bool}, ih: {S.find(~K, ~same, V, S.erase(~K, ~same, V, t, key), q) == S.find(~K, ~same, V, t, q) : Maybe<&2, T.Entry>}) -> {S.find(~K, ~same, V, S.omit_entry(K, V, T.Item{k, v, d}, S.erase(~K, ~same, V, t, key), x), q) == S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, t, q), y) : Maybe<&2, T.Entry>}: 47 match x: 48 case True{}: 49 match y: 50 case False{}: ih 51 case True{}: 52 eq = refl(k, q, ey) 53 bad = Equal.trans(Bool, same(q)(key), same(k)(key), True{}, Equal.cong(K, Bool, z => same(z)(key), q, k, Equal.sym(K, k, q, eq)), ex) 54 Empty.absurd({S.find(~K, ~same, V, S.erase(~K, ~same, V, t, key), q) == Some{T.Item{k, v, d}} : Maybe<&2, T.Entry>}, clash(same(q)(key), bad, h)) 55 case False{}: 56 %Equal.sym(Bool, same(k)(q), y, ey) : {S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, S.erase(~K, ~same, V, t, key), q), _) == S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, t, q), y) : Maybe<&2, T.Entry>} 57 Equal.cong(Maybe<&2, T.Entry>, Maybe<&2, T.Entry>, rest => S.choose_entry(K, V, T.Item{k, v, d}, rest, y), S.find(~K, ~same, V, S.erase(~K, ~same, V, t, key), q), S.find(~K, ~same, V, t, q), ih) 58 59 def find_erase_other(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, b: List<&2, T.Entry>, +key: K, +q: K, +h: {same(q)(key) == False{} : Bool}) -> {S.find(~K, ~same, V, S.erase(~K, ~same, V, b, key), q) == S.find(~K, ~same, V, b, q) : Maybe<&2, T.Entry>}: 60 match b: 61 case Nil{}: {==} 62 case Con{T.Item{+k, +v, +d}, +t}: 63 erase_other_step(~K, ~same, ~refl, V, k, v, d, t, key, q, h, same(k)(key), {==}, same(k)(q), {==}, find_erase_other(~K, ~same, ~refl, V, t, key, q, h)) 64 65 # Removing a key from the recency list does not change membership of others. 66 def member_unlist_skip(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), +oi: K, +ot: List<&2, K>, +key: K, +k: K, +h: {same(k)(key) == False{} : Bool}, +ex: {same(oi)(key) == True{} : Bool}, y: Bool, +ey: {same(oi)(k) == y : Bool}, ih: {E.member(~K, ~same, S.unlist(~K, ~same, ot, key), k) == E.member(~K, ~same, ot, k) : Bool}) -> {E.member(~K, ~same, S.unlist(~K, ~same, ot, key), k) == Bool.or(y, E.member(~K, ~same, ot, k)) : Bool}: 67 match y: 68 case False{}: ih 69 case True{}: 70 eq = refl(oi, k, ey) 71 bad = Equal.trans(Bool, same(k)(key), same(oi)(key), True{}, Equal.cong(K, Bool, z => same(z)(key), k, oi, Equal.sym(K, oi, k, eq)), ex) 72 Empty.absurd({E.member(~K, ~same, S.unlist(~K, ~same, ot, key), k) == True{} : Bool}, clash(same(k)(key), bad, h)) 73 74 def member_unlist_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), +oi: K, +ot: List<&2, K>, +key: K, +k: K, +h: {same(k)(key) == False{} : Bool}, x: Bool, +ex: {same(oi)(key) == x : Bool}, ih: {E.member(~K, ~same, S.unlist(~K, ~same, ot, key), k) == E.member(~K, ~same, ot, k) : Bool}) -> {E.member(~K, ~same, S.omit_key(K, oi, S.unlist(~K, ~same, ot, key), x), k) == Bool.or(same(oi)(k), E.member(~K, ~same, ot, k)) : Bool}: 75 match x: 76 case False{}: Equal.cong(Bool, Bool, m => Bool.or(same(oi)(k), m), E.member(~K, ~same, S.unlist(~K, ~same, ot, key), k), E.member(~K, ~same, ot, k), ih) 77 case True{}: member_unlist_skip(~K, ~same, ~refl, oi, ot, key, k, h, ex, same(oi)(k), {==}, ih) 78 79 def member_unlist(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), o: List<&2, K>, +key: K, +k: K, +h: {same(k)(key) == False{} : Bool}) -> {E.member(~K, ~same, S.unlist(~K, ~same, o, key), k) == E.member(~K, ~same, o, k) : Bool}: 80 match o: 81 case Nil{}: {==} 82 case Con{+oi, +ot}: 83 member_unlist_step(~K, ~same, ~refl, oi, ot, key, k, h, same(oi)(key), {==}, member_unlist(~K, ~same, ~refl, ot, key, k, h)) 84 85 def or_assoc(a: Bool, b: Bool, c: Bool) -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}: 86 match a: 87 case True{}: {==} 88 case False{}: {==} 89 90 def member_append(~K: Data, ~same: K -> K -> Bool, xs: List<&2, K>, +ys: List<&2, K>, +k: K) -> {E.member(~K, ~same, List.append(&2, K, xs, ys), k) == Bool.or(E.member(~K, ~same, xs, k), E.member(~K, ~same, ys, k)) : Bool}: 91 match xs: 92 case Nil{}: {==} 93 case Con{+x, +rest}: 94 Equal.trans(Bool, Bool.or(same(x)(k), E.member(~K, ~same, List.append(&2, K, rest, ys), k)), Bool.or(same(x)(k), Bool.or(E.member(~K, ~same, rest, k), E.member(~K, ~same, ys, k))), Bool.or(Bool.or(same(x)(k), E.member(~K, ~same, rest, k)), E.member(~K, ~same, ys, k)), Equal.cong(Bool, Bool, m => Bool.or(same(x)(k), m), E.member(~K, ~same, List.append(&2, K, rest, ys), k), Bool.or(E.member(~K, ~same, rest, k), E.member(~K, ~same, ys, k)), member_append(~K, ~same, rest, ys, k)), Equal.sym(Bool, Bool.or(Bool.or(same(x)(k), E.member(~K, ~same, rest, k)), E.member(~K, ~same, ys, k)), Bool.or(same(x)(k), Bool.or(E.member(~K, ~same, rest, k), E.member(~K, ~same, ys, k))), or_assoc(same(x)(k), E.member(~K, ~same, rest, k), E.member(~K, ~same, ys, k)))) 95 96 # Membership in the moved recency list (key re-appended at the newest end). 97 def member_moved_other(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), +o: List<&2, K>, +key: K, +k: K, +h: {same(k)(key) == False{} : Bool}) -> {E.member(~K, ~same, moved(~K, ~same, o, key), k) == E.member(~K, ~same, o, k) : Bool}: 98 %Equal.sym(Bool, E.member(~K, ~same, List.append(&2, K, S.unlist(~K, ~same, o, key), Con{key, Nil{}}), k), Bool.or(E.member(~K, ~same, S.unlist(~K, ~same, o, key), k), Bool.or(same(key)(k), False{})), member_append(~K, ~same, S.unlist(~K, ~same, o, key), Con{key, Nil{}}, k)) : {_ == E.member(~K, ~same, o, k) : Bool} 99 %Equal.sym(Bool, same(key)(k), False{}, symmetric_false(~K, ~same, ~refl, ~rfx, k, key, h)) : {Bool.or(E.member(~K, ~same, S.unlist(~K, ~same, o, key), k), Bool.or(_, False{})) == E.member(~K, ~same, o, k) : Bool} 100 %Equal.sym(Bool, E.member(~K, ~same, S.unlist(~K, ~same, o, key), k), E.member(~K, ~same, o, k), member_unlist(~K, ~same, ~refl, o, key, k, h)) : {Bool.or(_, False{}) == E.member(~K, ~same, o, k) : Bool} 101 or_false(E.member(~K, ~same, o, k)) 102 103 def member_moved_key(~K: Data, ~same: K -> K -> Bool, ~rfx: reflexive(~K, ~same), +o: List<&2, K>, +key: K) -> {E.member(~K, ~same, moved(~K, ~same, o, key), key) == True{} : Bool}: 104 %Equal.sym(Bool, E.member(~K, ~same, List.append(&2, K, S.unlist(~K, ~same, o, key), Con{key, Nil{}}), key), Bool.or(E.member(~K, ~same, S.unlist(~K, ~same, o, key), key), Bool.or(same(key)(key), False{})), member_append(~K, ~same, S.unlist(~K, ~same, o, key), Con{key, Nil{}}, key)) : {_ == True{} : Bool} 105 %Equal.sym(Bool, same(key)(key), True{}, rfx(key)) : {Bool.or(E.member(~K, ~same, S.unlist(~K, ~same, o, key), key), Bool.or(_, False{})) == True{} : Bool} 106 or_true(E.member(~K, ~same, S.unlist(~K, ~same, o, key), key)) 107 108 def member_moved_same(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), +o: List<&2, K>, +key: K, +k: K, +h: {same(k)(key) == True{} : Bool}) -> {E.member(~K, ~same, moved(~K, ~same, o, key), k) == True{} : Bool}: 109 %Equal.sym(K, k, key, refl(k, key, h)) : {E.member(~K, ~same, moved(~K, ~same, o, key), _) == True{} : Bool} 110 member_moved_key(~K, ~same, ~rfx, o, key) 111 112 # --------------------------------------------------------------------------- 113 # Lookups at recency keys after removing/moving a key. 114 def keep_or_drop(-K: Data, -V: Data, l: Maybe<&2, T.Entry>, rest: List<&2, Maybe<&2, T.Entry>>, drop: Bool) -> List<&2, Maybe<&2, T.Entry>>: 115 match drop: 116 case True{}: rest 117 case False{}: Con{l, rest} 118 119 def ldrop(~K: Data, ~same: K -> K -> Bool, -V: Data, o: List<&2, K>, xs: List<&2, Maybe<&2, T.Entry>>, +key: K) -> List<&2, Maybe<&2, T.Entry>>: 120 match o xs: 121 case Con{oi, ot} Con{l, lt}: keep_or_drop(K, V, l, ldrop(~K, ~same, V, ot, lt, key), same(oi)(key)) 122 case a b: Nil{} 123 124 def lookups_unlist_step(~K: Data, ~same: K -> K -> Bool, -V: Data, +oi: K, +ot: List<&2, K>, +b: List<&2, T.Entry>, +key: K, x: Bool, ih: {E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), b) == ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key) : List<&2, Maybe<&2, T.Entry>>}) -> {E.lookups(~K, ~same, V, S.omit_key(K, oi, S.unlist(~K, ~same, ot, key), x), b) == keep_or_drop(K, V, S.find(~K, ~same, V, b, oi), ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key), x) : List<&2, Maybe<&2, T.Entry>>}: 125 match x: 126 case True{}: ih 127 case False{}: Equal.cong(List<&2, Maybe<&2, T.Entry>>, List<&2, Maybe<&2, T.Entry>>, zs => Con{S.find(~K, ~same, V, b, oi), zs}, E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), b), ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key), ih) 128 129 def lookups_unlist(~K: Data, ~same: K -> K -> Bool, -V: Data, o: List<&2, K>, +b: List<&2, T.Entry>, +key: K) -> {E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), b) == ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key) : List<&2, Maybe<&2, T.Entry>>}: 130 match o: 131 case Nil{}: {==} 132 case Con{+oi, +ot}: lookups_unlist_step(~K, ~same, V, oi, ot, b, key, same(oi)(key), lookups_unlist(~K, ~same, V, ot, b, key)) 133 134 def lookups_unlist_erase_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +oi: K, +ot: List<&2, K>, +b: List<&2, T.Entry>, +key: K, x: Bool, +ex: {same(oi)(key) == x : Bool}, ih: {E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), S.erase(~K, ~same, V, b, key)) == ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key) : List<&2, Maybe<&2, T.Entry>>}) -> {E.lookups(~K, ~same, V, S.omit_key(K, oi, S.unlist(~K, ~same, ot, key), x), S.erase(~K, ~same, V, b, key)) == keep_or_drop(K, V, S.find(~K, ~same, V, b, oi), ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key), x) : List<&2, Maybe<&2, T.Entry>>}: 135 match x: 136 case True{}: ih 137 case False{}: 138 %Equal.sym(Maybe<&2, T.Entry>, S.find(~K, ~same, V, S.erase(~K, ~same, V, b, key), oi), S.find(~K, ~same, V, b, oi), find_erase_other(~K, ~same, ~refl, V, b, key, oi, ex)) : {Con{_, E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), S.erase(~K, ~same, V, b, key))} == Con{S.find(~K, ~same, V, b, oi), ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key)} : List<&2, Maybe<&2, T.Entry>>} 139 Equal.cong(List<&2, Maybe<&2, T.Entry>>, List<&2, Maybe<&2, T.Entry>>, zs => Con{S.find(~K, ~same, V, b, oi), zs}, E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), S.erase(~K, ~same, V, b, key)), ldrop(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), key), ih) 140 141 def lookups_unlist_erase(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, o: List<&2, K>, +b: List<&2, T.Entry>, +key: K) -> {E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)) == ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key) : List<&2, Maybe<&2, T.Entry>>}: 142 match o: 143 case Nil{}: {==} 144 case Con{+oi, +ot}: lookups_unlist_erase_step(~K, ~same, ~refl, V, oi, ot, b, key, same(oi)(key), {==}, lookups_unlist_erase(~K, ~same, ~refl, V, ot, b, key)) 145 146 def lookups_append(~K: Data, ~same: K -> K -> Bool, -V: Data, o1: List<&2, K>, +o2: List<&2, K>, +b: List<&2, T.Entry>) -> {E.lookups(~K, ~same, V, List.append(&2, K, o1, o2), b) == List.append(&2, Maybe<&2, T.Entry>, E.lookups(~K, ~same, V, o1, b), E.lookups(~K, ~same, V, o2, b)) : List<&2, Maybe<&2, T.Entry>>}: 147 match o1: 148 case Nil{}: {==} 149 case Con{+x, +rest}: Equal.cong(List<&2, Maybe<&2, T.Entry>>, List<&2, Maybe<&2, T.Entry>>, zs => Con{S.find(~K, ~same, V, b, x), zs}, E.lookups(~K, ~same, V, List.append(&2, K, rest, o2), b), List.append(&2, Maybe<&2, T.Entry>, E.lookups(~K, ~same, V, rest, b), E.lookups(~K, ~same, V, o2, b)), lookups_append(~K, ~same, V, rest, o2, b)) 150 151 def lookups_prepend_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +oi: K, +ot: List<&2, K>, +key: K, +v: V, +d: T.Int64, +rest: List<&2, T.Entry>, x: Bool, +ex: {same(oi)(key) == x : Bool}, ih: {E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), Con{T.Item{key, v, d}, rest}) == E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), rest) : List<&2, Maybe<&2, T.Entry>>}) -> {E.lookups(~K, ~same, V, S.omit_key(K, oi, S.unlist(~K, ~same, ot, key), x), Con{T.Item{key, v, d}, rest}) == E.lookups(~K, ~same, V, S.omit_key(K, oi, S.unlist(~K, ~same, ot, key), x), rest) : List<&2, Maybe<&2, T.Entry>>}: 152 match x: 153 case True{}: ih 154 case False{}: 155 %Equal.sym(Bool, same(key)(oi), False{}, symmetric_false(~K, ~same, ~refl, ~rfx, oi, key, ex)) : {Con{S.choose_entry(K, V, T.Item{key, v, d}, S.find(~K, ~same, V, rest, oi), _), E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), Con{T.Item{key, v, d}, rest})} == Con{S.find(~K, ~same, V, rest, oi), E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), rest)} : List<&2, Maybe<&2, T.Entry>>} 156 Equal.cong(List<&2, Maybe<&2, T.Entry>>, List<&2, Maybe<&2, T.Entry>>, zs => Con{S.find(~K, ~same, V, rest, oi), zs}, E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), Con{T.Item{key, v, d}, rest}), E.lookups(~K, ~same, V, S.unlist(~K, ~same, ot, key), rest), ih) 157 158 # A new binding for key is invisible at the other (unlisted) recency keys. 159 def lookups_prepend(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, o: List<&2, K>, +key: K, +v: V, +d: T.Int64, +rest: List<&2, T.Entry>) -> {E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), Con{T.Item{key, v, d}, rest}) == E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), rest) : List<&2, Maybe<&2, T.Entry>>}: 160 match o: 161 case Nil{}: {==} 162 case Con{+oi, +ot}: lookups_prepend_step(~K, ~same, ~refl, ~rfx, V, oi, ot, key, v, d, rest, same(oi)(key), {==}, lookups_prepend(~K, ~same, ~refl, ~rfx, V, ot, key, v, d, rest)) 163 164 # --------------------------------------------------------------------------- 165 # Stray bindings under erase/unlist/move. 166 def erase_keep_true(~K: Data, ~same: K -> K -> Bool, -V: Data, +k: K, +v: V, +d: T.Int64, +lhs: List<&2, T.Entry>, +st: List<&2, T.Entry>, +key: K, +ex: {same(k)(key) == True{} : Bool}, y: Bool, ih: {lhs == S.erase(~K, ~same, V, st, key) : List<&2, T.Entry>}) -> {lhs == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, st, y), key) : List<&2, T.Entry>}: 167 match y: 168 case True{}: ih 169 case False{}: 170 %Equal.sym(Bool, same(k)(key), True{}, ex) : {lhs == S.omit_entry(K, V, T.Item{k, v, d}, S.erase(~K, ~same, V, st, key), _) : List<&2, T.Entry>} 171 ih 172 173 def erase_keep_false(~K: Data, ~same: K -> K -> Bool, -V: Data, +k: K, +v: V, +d: T.Int64, +lhs: List<&2, T.Entry>, +st: List<&2, T.Entry>, +key: K, +ex: {same(k)(key) == False{} : Bool}, y: Bool, ih: {lhs == S.erase(~K, ~same, V, st, key) : List<&2, T.Entry>}) -> {E.keep_stray(K, V, T.Item{k, v, d}, lhs, y) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, st, y), key) : List<&2, T.Entry>}: 174 match y: 175 case True{}: ih 176 case False{}: 177 %Equal.sym(Bool, same(k)(key), False{}, ex) : {Con{T.Item{k, v, d}, lhs} == S.omit_entry(K, V, T.Item{k, v, d}, S.erase(~K, ~same, V, st, key), _) : List<&2, T.Entry>} 178 Equal.cong(List<&2, T.Entry>, List<&2, T.Entry>, zs => Con{T.Item{k, v, d}, zs}, lhs, S.erase(~K, ~same, V, st, key), ih) 179 180 def stray_unlist_erase_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +o: List<&2, K>, +k: K, +v: V, +d: T.Int64, +t: List<&2, T.Entry>, +key: K, x: Bool, +ex: {same(k)(key) == x : Bool}, ih: {E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, t), key) : List<&2, T.Entry>}) -> {E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.omit_entry(K, V, T.Item{k, v, d}, S.erase(~K, ~same, V, t, key), x)) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>}: 181 match x: 182 case True{}: erase_keep_true(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 183 case False{}: 184 %Equal.sym(Bool, E.member(~K, ~same, S.unlist(~K, ~same, o, key), k), E.member(~K, ~same, o, k), member_unlist(~K, ~same, ~refl, o, key, k, ex)) : {E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), _) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>} 185 erase_keep_false(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 186 187 def stray_unlist_erase(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +o: List<&2, K>, b: List<&2, T.Entry>, +key: K) -> {E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key) : List<&2, T.Entry>}: 188 match b: 189 case Nil{}: {==} 190 case Con{T.Item{+k, +v, +d}, +t}: stray_unlist_erase_step(~K, ~same, ~refl, V, o, k, v, d, t, key, same(k)(key), {==}, stray_unlist_erase(~K, ~same, ~refl, V, o, t, key)) 191 192 def stray_moved_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +o: List<&2, K>, +k: K, +v: V, +d: T.Int64, +t: List<&2, T.Entry>, +key: K, x: Bool, +ex: {same(k)(key) == x : Bool}, ih: {E.stray(~K, ~same, V, moved(~K, ~same, o, key), t) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, t), key) : List<&2, T.Entry>}) -> {E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, moved(~K, ~same, o, key), t), E.member(~K, ~same, moved(~K, ~same, o, key), k)) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>}: 193 match x: 194 case True{}: 195 %Equal.sym(Bool, E.member(~K, ~same, moved(~K, ~same, o, key), k), True{}, member_moved_same(~K, ~same, ~refl, ~rfx, o, key, k, ex)) : {E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, moved(~K, ~same, o, key), t), _) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>} 196 erase_keep_true(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, moved(~K, ~same, o, key), t), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 197 case False{}: 198 %Equal.sym(Bool, E.member(~K, ~same, moved(~K, ~same, o, key), k), E.member(~K, ~same, o, k), member_moved_other(~K, ~same, ~refl, ~rfx, o, key, k, ex)) : {E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, moved(~K, ~same, o, key), t), _) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>} 199 erase_keep_false(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, moved(~K, ~same, o, key), t), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 200 201 def stray_moved(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +o: List<&2, K>, b: List<&2, T.Entry>, +key: K) -> {E.stray(~K, ~same, V, moved(~K, ~same, o, key), b) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key) : List<&2, T.Entry>}: 202 match b: 203 case Nil{}: {==} 204 case Con{T.Item{+k, +v, +d}, +t}: stray_moved_step(~K, ~same, ~refl, ~rfx, V, o, k, v, d, t, key, same(k)(key), {==}, stray_moved(~K, ~same, ~refl, ~rfx, V, o, t, key)) 205 206 def stray_moved_erase_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +o: List<&2, K>, +k: K, +v: V, +d: T.Int64, +t: List<&2, T.Entry>, +key: K, x: Bool, +ex: {same(k)(key) == x : Bool}, ih: {E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, t), key) : List<&2, T.Entry>}) -> {E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.omit_entry(K, V, T.Item{k, v, d}, S.erase(~K, ~same, V, t, key), x)) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>}: 207 match x: 208 case True{}: erase_keep_true(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 209 case False{}: 210 %Equal.sym(Bool, E.member(~K, ~same, moved(~K, ~same, o, key), k), E.member(~K, ~same, o, k), member_moved_other(~K, ~same, ~refl, ~rfx, o, key, k, ex)) : {E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), _) == S.erase(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), E.member(~K, ~same, o, k)), key) : List<&2, T.Entry>} 211 erase_keep_false(~K, ~same, V, k, v, d, E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, t, key)), E.stray(~K, ~same, V, o, t), key, ex, E.member(~K, ~same, o, k), ih) 212 213 def stray_moved_erase(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +o: List<&2, K>, b: List<&2, T.Entry>, +key: K) -> {E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)) == S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key) : List<&2, T.Entry>}: 214 match b: 215 case Nil{}: {==} 216 case Con{T.Item{+k, +v, +d}, +t}: stray_moved_erase_step(~K, ~same, ~refl, ~rfx, V, o, k, v, d, t, key, same(k)(key), {==}, stray_moved_erase(~K, ~same, ~refl, ~rfx, V, o, t, key)) 217 218 # --------------------------------------------------------------------------- 219 # Lookup of ANY key from the canonical form. 220 def choose_lookup(-K: Data, -V: Data, l: Maybe<&2, T.Entry>, rest: Maybe<&2, T.Entry>, hit: Bool) -> Maybe<&2, T.Entry>: 221 match hit: 222 case True{}: l 223 case False{}: rest 224 225 def pick(~K: Data, ~same: K -> K -> Bool, -V: Data, o: List<&2, K>, xs: List<&2, Maybe<&2, T.Entry>>, +q: K) -> Maybe<&2, T.Entry>: 226 match o xs: 227 case Con{oi, ot} Con{l, lt}: choose_lookup(K, V, l, pick(~K, ~same, V, ot, lt, q), same(oi)(q)) 228 case a b: None{} 229 230 def decide_lookup(-K: Data, -V: Data, bound: Bool, inside: Maybe<&2, T.Entry>, outside: Maybe<&2, T.Entry>) -> Maybe<&2, T.Entry>: 231 match bound: 232 case True{}: inside 233 case False{}: outside 234 235 def cfind(~K: Data, ~same: K -> K -> Bool, -V: Data, +o: List<&2, K>, xs: List<&2, Maybe<&2, T.Entry>>, x: List<&2, T.Entry>, +q: K) -> Maybe<&2, T.Entry>: 236 decide_lookup(K, V, E.member(~K, ~same, o, q), pick(~K, ~same, V, o, xs, q), S.find(~K, ~same, V, x, q)) 237 238 def canonical_find(~K: Data, ~same: K -> K -> Bool, -V: Data, c: E.Canonical, +q: K) -> Maybe<&2, T.Entry>: 239 E.Canon{cap, o, l, m, f, xs, x} = c 240 cfind(~K, ~same, V, o, xs, x, q) 241 242 def bindings(-K: Data, -V: Data, s: S.Model) -> List<&2, T.Entry>: 243 S.Abstract{cap, b, o, l, m, f} = s 244 b 245 246 def pick_hit(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +oi: K, +ot: List<&2, K>, +b: List<&2, T.Entry>, +q: K, y: Bool, +ey: {same(oi)(q) == y : Bool}, rest: {Bool.or(y, E.member(~K, ~same, ot, q)) == True{} : Bool}, ih: @h: {E.member(~K, ~same, ot, q) == True{} : Bool} -> {S.find(~K, ~same, V, b, q) == pick(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), q) : Maybe<&2, T.Entry>}) -> {S.find(~K, ~same, V, b, q) == choose_lookup(K, V, S.find(~K, ~same, V, b, oi), pick(~K, ~same, V, ot, E.lookups(~K, ~same, V, ot, b), q), y) : Maybe<&2, T.Entry>}: 247 match y: 248 case False{}: ih(rest) 249 case True{}: Equal.cong(K, Maybe<&2, T.Entry>, z => S.find(~K, ~same, V, b, z), q, oi, Equal.sym(K, oi, q, refl(oi, q, ey))) 250 251 def pick_member(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, o: List<&2, K>, +b: List<&2, T.Entry>, +q: K, +h: {E.member(~K, ~same, o, q) == True{} : Bool}) -> {S.find(~K, ~same, V, b, q) == pick(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), q) : Maybe<&2, T.Entry>}: 252 match o: 253 case Nil{}: Empty.absurd({S.find(~K, ~same, V, b, q) == None{} : Maybe<&2, T.Entry>}, Routing.false_true(h)) 254 case Con{+oi, +ot}: pick_hit(~K, ~same, ~refl, V, oi, ot, b, q, same(oi)(q), {==}, h, hh => pick_member(~K, ~same, ~refl, V, ot, b, q, hh)) 255 256 def outside_step(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +o: List<&2, K>, +k: K, +v: V, +d: T.Int64, +t: List<&2, T.Entry>, +q: K, +h: {E.member(~K, ~same, o, q) == False{} : Bool}, y: Bool, +ey: {E.member(~K, ~same, o, k) == y : Bool}, z: Bool, +ez: {same(k)(q) == z : Bool}, ih: {S.find(~K, ~same, V, t, q) == S.find(~K, ~same, V, E.stray(~K, ~same, V, o, t), q) : Maybe<&2, T.Entry>}) -> {S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, t, q), z) == S.find(~K, ~same, V, E.keep_stray(K, V, T.Item{k, v, d}, E.stray(~K, ~same, V, o, t), y), q) : Maybe<&2, T.Entry>}: 257 match y: 258 case True{}: 259 match z: 260 case False{}: ih 261 case True{}: 262 bad = Equal.trans(Bool, E.member(~K, ~same, o, q), E.member(~K, ~same, o, k), True{}, Equal.cong(K, Bool, w => E.member(~K, ~same, o, w), q, k, Equal.sym(K, k, q, refl(k, q, ez))), ey) 263 Empty.absurd({Some{T.Item{k, v, d}} == S.find(~K, ~same, V, E.stray(~K, ~same, V, o, t), q) : Maybe<&2, T.Entry>}, clash(E.member(~K, ~same, o, q), bad, h)) 264 case False{}: 265 %Equal.sym(Bool, same(k)(q), z, ez) : {S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, t, q), z) == S.choose_entry(K, V, T.Item{k, v, d}, S.find(~K, ~same, V, E.stray(~K, ~same, V, o, t), q), _) : Maybe<&2, T.Entry>} 266 Equal.cong(Maybe<&2, T.Entry>, Maybe<&2, T.Entry>, rest => S.choose_entry(K, V, T.Item{k, v, d}, rest, z), S.find(~K, ~same, V, t, q), S.find(~K, ~same, V, E.stray(~K, ~same, V, o, t), q), ih) 267 268 def outside_member(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +o: List<&2, K>, b: List<&2, T.Entry>, +q: K, +h: {E.member(~K, ~same, o, q) == False{} : Bool}) -> {S.find(~K, ~same, V, b, q) == S.find(~K, ~same, V, E.stray(~K, ~same, V, o, b), q) : Maybe<&2, T.Entry>}: 269 match b: 270 case Nil{}: {==} 271 case Con{T.Item{+k, +v, +d}, +t}: outside_step(~K, ~same, ~refl, V, o, k, v, d, t, q, h, E.member(~K, ~same, o, k), {==}, same(k)(q), {==}, outside_member(~K, ~same, ~refl, V, o, t, q, h)) 272 273 def find_decide(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +o: List<&2, K>, +b: List<&2, T.Entry>, +q: K, m: Bool, +em: {E.member(~K, ~same, o, q) == m : Bool}) -> {S.find(~K, ~same, V, b, q) == decide_lookup(K, V, m, pick(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), q), S.find(~K, ~same, V, E.stray(~K, ~same, V, o, b), q)) : Maybe<&2, T.Entry>}: 274 match m: 275 case True{}: pick_member(~K, ~same, ~refl, V, o, b, q, em) 276 case False{}: outside_member(~K, ~same, ~refl, V, o, b, q, em) 277 278 # Every lookup is determined by the canonical form. 279 def find_canonical(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, s: S.Model, +q: K) -> {S.find(~K, ~same, V, bindings(K, V, s), q) == canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, s), q) : Maybe<&2, T.Entry>}: 280 S.Abstract{cap, +b, +o, l, m, f} = s 281 find_decide(~K, ~same, ~refl, V, o, b, q, E.member(~K, ~same, o, q), {==}) 282 283 # Meaning of the relation: related models agree on lookup of EVERY key. 284 def lookup_agreement(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +a: S.Model, +b: S.Model, related: E.states(~K, ~same, V, a, b), +q: K) -> {S.find(~K, ~same, V, bindings(K, V, a), q) == S.find(~K, ~same, V, bindings(K, V, b), q) : Maybe<&2, T.Entry>}: 285 Equal.trans(Maybe<&2, T.Entry>, S.find(~K, ~same, V, bindings(K, V, a), q), canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, a), q), S.find(~K, ~same, V, bindings(K, V, b), q), find_canonical(~K, ~same, ~refl, V, a, q), Equal.trans(Maybe<&2, T.Entry>, canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, a), q), canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, b), q), S.find(~K, ~same, V, bindings(K, V, b), q), Equal.cong(E.Canonical, Maybe<&2, T.Entry>, c => canonical_find(~K, ~same, V, c, q), E.canonical(~K, ~same, V, a), E.canonical(~K, ~same, V, b), related), Equal.sym(Maybe<&2, T.Entry>, S.find(~K, ~same, V, bindings(K, V, b), q), canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, b), q), find_canonical(~K, ~same, ~refl, V, b, q)))) 286 287 # Ordered enumeration (Keys/Values/aggregate input) from the canonical form. 288 def somes(-K: Data, -V: Data, xs: List<&2, Maybe<&2, T.Entry>>) -> List<&2, T.Entry>: 289 match xs: 290 case Nil{}: Nil{} 291 case Con{l, lt}: O.collect(K, V, l, somes(K, V, lt)) 292 293 def ordered_somes(~K: Data, ~same: K -> K -> Bool, -V: Data, o: List<&2, K>, +b: List<&2, T.Entry>) -> {O.ordered(~K, ~same, V, o, b) == somes(K, V, E.lookups(~K, ~same, V, o, b)) : List<&2, T.Entry>}: 294 match o: 295 case Nil{}: {==} 296 case Con{+k, +t}: Equal.cong(List<&2, T.Entry>, List<&2, T.Entry>, rest => O.collect(K, V, S.find(~K, ~same, V, b, k), rest), O.ordered(~K, ~same, V, t, b), somes(K, V, E.lookups(~K, ~same, V, t, b)), ordered_somes(~K, ~same, V, t, b)) 297 298 def canonical_entries(-K: Data, -V: Data, c: E.Canonical) -> List<&2, T.Entry>: 299 E.Canon{cap, o, l, m, f, xs, x} = c 300 somes(K, V, xs) 301 302 def entries_canonical(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model) -> {O.all_entries(~K, ~same, V, s) == canonical_entries(K, V, E.canonical(~K, ~same, V, s)) : List<&2, T.Entry>}: 303 S.Abstract{cap, +b, +o, l, m, f} = s 304 ordered_somes(~K, ~same, V, o, b) 305 306 def entries_agreement(~K: Data, ~same: K -> K -> Bool, -V: Data, +a: S.Model, +b: S.Model, related: E.states(~K, ~same, V, a, b)) -> {O.all_entries(~K, ~same, V, a) == O.all_entries(~K, ~same, V, b) : List<&2, T.Entry>}: 307 Equal.trans(List<&2, T.Entry>, O.all_entries(~K, ~same, V, a), canonical_entries(K, V, E.canonical(~K, ~same, V, a)), O.all_entries(~K, ~same, V, b), entries_canonical(~K, ~same, V, a), Equal.trans(List<&2, T.Entry>, canonical_entries(K, V, E.canonical(~K, ~same, V, a)), canonical_entries(K, V, E.canonical(~K, ~same, V, b)), O.all_entries(~K, ~same, V, b), Equal.cong(E.Canonical, List<&2, T.Entry>, c => canonical_entries(K, V, c), E.canonical(~K, ~same, V, a), E.canonical(~K, ~same, V, b), related), Equal.sym(List<&2, T.Entry>, O.all_entries(~K, ~same, V, b), canonical_entries(K, V, E.canonical(~K, ~same, V, b)), entries_canonical(~K, ~same, V, b)))) 308 309 # --------------------------------------------------------------------------- 310 # Canonical effect of each primitive state change used by the specification. 311 def c_drop(~K: Data, ~same: K -> K -> Bool, -V: Data, c: E.Canonical, +key: K) -> E.Canonical: 312 E.Canon{cap, +o, l, m, f, xs, x} = c 313 E.Canon{cap, S.unlist(~K, ~same, o, key), l, m, f, ldrop(~K, ~same, V, o, xs, key), S.erase(~K, ~same, V, x, key)} 314 315 def c_write(~K: Data, ~same: K -> K -> Bool, -V: Data, c: E.Canonical, +key: K, value: V, deadline: T.Int64) -> E.Canonical: 316 E.Canon{cap, +o, l, m, f, xs, x} = c 317 E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, xs, key), Con{Some{T.Item{key, value, deadline}}, Nil{}}), S.erase(~K, ~same, V, x, key)} 318 319 def c_move(~K: Data, ~same: K -> K -> Bool, -V: Data, c: E.Canonical, +key: K) -> E.Canonical: 320 E.Canon{cap, +o, l, m, f, +xs, +x} = c 321 E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, xs, key), Con{cfind(~K, ~same, V, o, xs, x, key), Nil{}}), S.erase(~K, ~same, V, x, key)} 322 323 def c_counts(-K: Data, -V: Data, c: E.Canonical, m: T.Metrics) -> E.Canonical: 324 E.Canon{cap, o, l, old, f, xs, x} = c 325 E.Canon{cap, o, l, m, f, xs, x} 326 327 def drop_transform(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +cap: Nat, +b: List<&2, T.Entry>, +o: List<&2, K>, +l: T.Int64, +m: T.Metrics, +f: Bool, +key: K) -> {E.canonical(~K, ~same, V, S.Abstract{cap, S.erase(~K, ~same, V, b, key), S.unlist(~K, ~same, o, key), l, m, f}) == c_drop(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical}: 328 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), lookups_unlist_erase(~K, ~same, ~refl, V, o, b, key)) : {E.Canon{cap, S.unlist(~K, ~same, o, key), l, m, f, _, E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key))} == c_drop(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 329 %Equal.sym(List<&2, T.Entry>, E.stray(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key), stray_unlist_erase(~K, ~same, ~refl, V, o, b, key)) : {E.Canon{cap, S.unlist(~K, ~same, o, key), l, m, f, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), _} == c_drop(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 330 {==} 331 332 def write_transform(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +cap: Nat, +b: List<&2, T.Entry>, +o: List<&2, K>, +l: T.Int64, +m: T.Metrics, +f: Bool, +key: K, +value: V, +deadline: T.Int64) -> {E.canonical(~K, ~same, V, S.Abstract{cap, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)}, moved(~K, ~same, o, key), l, m, f}) == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical}: 333 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, List.append(&2, K, S.unlist(~K, ~same, o, key), Con{key, Nil{}}), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)}), List.append(&2, Maybe<&2, T.Entry>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)}), E.lookups(~K, ~same, V, Con{key, Nil{}}, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})), lookups_append(~K, ~same, V, S.unlist(~K, ~same, o, key), Con{key, Nil{}}, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, _, E.stray(~K, ~same, V, moved(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 334 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)}), E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), lookups_prepend(~K, ~same, ~refl, ~rfx, V, o, key, value, deadline, S.erase(~K, ~same, V, b, key))) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, _, E.lookups(~K, ~same, V, Con{key, Nil{}}, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})), E.stray(~K, ~same, V, moved(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 335 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), lookups_unlist_erase(~K, ~same, ~refl, V, o, b, key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, _, E.lookups(~K, ~same, V, Con{key, Nil{}}, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})), E.stray(~K, ~same, V, moved(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 336 %Equal.sym(Bool, same(key)(key), True{}, rfx(key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), Con{S.choose_entry(K, V, T.Item{key, value, deadline}, S.find(~K, ~same, V, S.erase(~K, ~same, V, b, key), key), _), Nil{}}), E.stray(~K, ~same, V, moved(~K, ~same, o, key), Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, b, key)})} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 337 %Equal.sym(Bool, E.member(~K, ~same, moved(~K, ~same, o, key), key), True{}, member_moved_key(~K, ~same, ~rfx, o, key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), Con{Some{T.Item{key, value, deadline}}, Nil{}}), E.keep_stray(K, V, T.Item{key, value, deadline}, E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), _)} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 338 %Equal.sym(List<&2, T.Entry>, E.stray(~K, ~same, V, moved(~K, ~same, o, key), S.erase(~K, ~same, V, b, key)), S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key), stray_moved_erase(~K, ~same, ~refl, ~rfx, V, o, b, key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), Con{Some{T.Item{key, value, deadline}}, Nil{}}), _} == c_write(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key, value, deadline) : E.Canonical} 339 {==} 340 341 def move_transform(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), ~rfx: reflexive(~K, ~same), -V: Data, +cap: Nat, +b: List<&2, T.Entry>, +o: List<&2, K>, +l: T.Int64, +m: T.Metrics, +f: Bool, +key: K) -> {E.canonical(~K, ~same, V, S.Abstract{cap, b, moved(~K, ~same, o, key), l, m, f}) == c_move(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical}: 342 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, List.append(&2, K, S.unlist(~K, ~same, o, key), Con{key, Nil{}}), b), List.append(&2, Maybe<&2, T.Entry>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), b), E.lookups(~K, ~same, V, Con{key, Nil{}}, b)), lookups_append(~K, ~same, V, S.unlist(~K, ~same, o, key), Con{key, Nil{}}, b)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, _, E.stray(~K, ~same, V, moved(~K, ~same, o, key), b)} == c_move(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 343 %Equal.sym(List<&2, Maybe<&2, T.Entry>>, E.lookups(~K, ~same, V, S.unlist(~K, ~same, o, key), b), ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), lookups_unlist(~K, ~same, V, o, b, key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, _, Con{S.find(~K, ~same, V, b, key), Nil{}}), E.stray(~K, ~same, V, moved(~K, ~same, o, key), b)} == c_move(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 344 %Equal.sym(Maybe<&2, T.Entry>, S.find(~K, ~same, V, b, key), decide_lookup(K, V, E.member(~K, ~same, o, key), pick(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), S.find(~K, ~same, V, E.stray(~K, ~same, V, o, b), key)), find_decide(~K, ~same, ~refl, V, o, b, key, E.member(~K, ~same, o, key), {==})) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), Con{_, Nil{}}), E.stray(~K, ~same, V, moved(~K, ~same, o, key), b)} == c_move(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 345 %Equal.sym(List<&2, T.Entry>, E.stray(~K, ~same, V, moved(~K, ~same, o, key), b), S.erase(~K, ~same, V, E.stray(~K, ~same, V, o, b), key), stray_moved(~K, ~same, ~refl, ~rfx, V, o, b, key)) : {E.Canon{cap, moved(~K, ~same, o, key), l, m, f, List.append(&2, Maybe<&2, T.Entry>, ldrop(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), key), Con{cfind(~K, ~same, V, o, E.lookups(~K, ~same, V, o, b), E.stray(~K, ~same, V, o, b), key), Nil{}}), _} == c_move(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, m, f}), key) : E.Canonical} 346 {==} 347 348 def stray_of(-K: Data, -V: Data, c: E.Canonical) -> List<&2, T.Entry>: 349 E.Canon{cap, o, l, m, f, xs, x} = c 350 x 351 352 def c_removed(-K: Data, -V: Data, c: E.Canonical) -> E.Canonical: 353 E.Canon{cap, o, l, T.Counts{i, e, r, h, m}, f, xs, x} = c 354 E.Canon{cap, o, l, T.Counts{i, e, Word.inc(64n, r), h, m}, f, xs, x} 355 356 def remove_choice(-K: Data, -V: Data, found: Maybe<&2, T.Entry>, kept: E.Canonical, dropped: E.Canonical) -> E.Canonical: 357 match found: 358 case None{}: kept 359 case Some{entry}: dropped 360 361 def c_remove(~K: Data, ~same: K -> K -> Bool, -V: Data, +c: E.Canonical, +key: K) -> E.Canonical: 362 remove_choice(K, V, canonical_find(~K, ~same, V, c, key), c, c_drop(~K, ~same, V, c_removed(K, V, c), key)) 363 364 def remove_found_transform(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +cap: Nat, +b: List<&2, T.Entry>, +o: List<&2, K>, +l: T.Int64, +i: Word(64n), +e: Word(64n), +r: Word(64n), +h: Word(64n), +m: Word(64n), +f: Bool, +key: K, found: Maybe<&2, T.Entry>) -> {E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove_decision(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}, key, found))) == remove_choice(K, V, found, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}), c_drop(~K, ~same, V, c_removed(K, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f})), key)) : E.Canonical}: 365 match found: 366 case None{}: {==} 367 case Some{entry}: drop_transform(~K, ~same, ~refl, V, cap, b, o, l, T.Counts{i, e, Word.inc(64n, r), h, m}, f, key) 368 369 # Canonical effect of the specification's Remove (either branch). 370 def remove_transform(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, s: S.Model, +key: K) -> {E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, s, key))) == c_remove(~K, ~same, V, E.canonical(~K, ~same, V, s), key) : E.Canonical}: 371 S.Abstract{+cap, +b, +o, +l, T.Counts{+i, +e, +r, +h, +m}, +f} = s 372 %Equal.sym(Maybe<&2, T.Entry>, S.find(~K, ~same, V, b, key), canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}), key), find_canonical(~K, ~same, ~refl, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}, key)) : {E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove_decision(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}, key, _))) == c_remove(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}), key) : E.Canonical} 373 remove_found_transform(~K, ~same, ~refl, V, cap, b, o, l, i, e, r, h, m, f, key, canonical_find(~K, ~same, V, E.canonical(~K, ~same, V, S.Abstract{cap, b, o, l, T.Counts{i, e, r, h, m}, f}), key)) 374 375 def remove_congruence(~K: Data, ~same: K -> K -> Bool, ~refl: reflects(~K, ~same), -V: Data, +a: S.Model, +b: S.Model, +key: K, related: E.states(~K, ~same, V, a, b)) -> E.states(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, a, key)), O.observed_state(K, V, S.remove(~K, ~same, V, b, key))): 376 Equal.trans(E.Canonical, E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, a, key))), c_remove(~K, ~same, V, E.canonical(~K, ~same, V, a), key), E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, b, key))), remove_transform(~K, ~same, ~refl, V, a, key), Equal.trans(E.Canonical, c_remove(~K, ~same, V, E.canonical(~K, ~same, V, a), key), c_remove(~K, ~same, V, E.canonical(~K, ~same, V, b), key), E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, b, key))), Equal.cong(E.Canonical, E.Canonical, c => c_remove(~K, ~same, V, c, key), E.canonical(~K, ~same, V, a), E.canonical(~K, ~same, V, b), related), Equal.sym(E.Canonical, E.canonical(~K, ~same, V, O.observed_state(K, V, S.remove(~K, ~same, V, b, key))), c_remove(~K, ~same, V, E.canonical(~K, ~same, V, b), key), remove_transform(~K, ~same, ~refl, V, b, key))))