1 import Base 2 import ../../../spec/containers/balanced_search_tree/main.bend as S 3 import ../../../spec/lib/common.bend as SC 4 import ../../../spec/lib/order.bend as SO 5 import ../../../src/containers/balanced_search_tree.bend as M 6 import ../../../src/containers/dynamic_array.bend as D 7 import ../../lib/list.bend as LL 8 import ../../lib/logic.bend as L 9 import ../../lib/nat.bend as N 10 import ../../lib/order.bend as O 11 import ./api.bend as API 12 import ./capi.bend as CA 13 import ./ccv.bend as CV 14 import ./cnx.bend as CX 15 import ./crm.bend as CR 16 import ./csv.bend as CS 17 import ./cur.bend as CU 18 import ./ends.bend as EN 19 import ./life.bend as LF 20 import ./mirror.bend as MI 21 import ./navm.bend as NM 22 import ./ok.bend as OK 23 import ./ord.bend as OR 24 import ./prim.bend as PR 25 import ./putm.bend as PM 26 import ./reads.bend as RD 27 import ./rmi.bend as RI 28 import ./rmp.bend as RP 29 import ./rmv.bend as RV 30 import ./sim.bend as SM 31 import ./state.bend as ST 32 import ./vapi.bend as VA 33 import ./vclr.bend as VC 34 import ./vdef.bend as VD 35 import ./vit.bend as VI 36 import ./vnav.bend as VN 37 import ./vsp.bend as VS 38 import ./vsz.bend as VZ 39 import ./vw.bend as VW 40 41 # Indexed TreeMap (src/containers/balanced_search_tree.bend): public proof 42 # entry point, generated by tools/generators/tm_gate.py. 43 # shadow ST.Sh: the map's Nat fields (size, root, first and last ids, 44 # free head, limit and depth), the node and payload arrays as 45 # lists, and two ghost values: the tree of ids (ST.Tr) and the 46 # free list; ST.real(sh) is the map 47 # abstraction ST.model(sh): the limit and the entries of the tree's ids in 48 # order, as a spec map (sorted entries); 49 # a mirror cursor's model is the specification's cursor over 50 # that map with the keys of its next and current ids 51 # (CU.cmod), a mirror view's the specification's view 52 # (VD.vmod) 53 # invariant ST.good(sh): the arrays laid out within the limit, the ghost 54 # tree the red-black tree the links describe (parents, sides, 55 # colours, black height), every id of the tree a live node with 56 # a payload, the free list chained through the vacant slots, 57 # the ids of tree and free list without repeats and covering 58 # the slots, the entries sorted by a lawful comparator, and the 59 # size, root and first/last ids those of the tree 60 # (state.bend); a cursor is good when its 61 # shadow is and its ids are 0 or ids of the tree (CU.cgood) 62 # 63 # Proved for every lawful comparator (O.Order: flip, antisymmetry, 64 # transitivity), every key and value type (Data), every good shadow, cursor 65 # and view, and every argument: each operation's result is the real map (or 66 # cursor, or view) of a good shadow whose model is the specification's 67 # result, with the same answer (OK.POK / CU.CPOK / VD.VPOK and the like). 68 # new, with_limit a good shadow of the specification's empty map 69 # reads size, is_empty, get, get_or_default, contains_key, 70 # contains_value, first/last entry and key, the 71 # lower/floor/ceiling/higher entries and keys 72 # updates put, put_if_absent, replace, replace_if_equal, 73 # remove, remove_if_equal, poll_first/last_entry, 74 # clear 75 # cursors iterator, descending_iterator, key_set, values, 76 # entry_set, iterator_next(_key, _value), 77 # iterator_has_next, iterator_set_value, 78 # iterator_remove, iterator_finish 79 # views sub_map, head_map, tail_map, descending_map, 80 # view_reverse, view_finish, view_get, 81 # view_contains_key, view_put, view_remove, 82 # view_size, view_clear, view_first/last_entry, 83 # view_lower/floor/ceiling/higher_entry, 84 # view_iterator 85 86 def new_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.new(~K, ~V, ~cmp) : M.TreeMap} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.new(K, V) : S.Model} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}): 87 LF.new_ok(~K, ~V, ~cmp) 88 89 def with_limit_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: Nat) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.with_limit(~K, ~V, ~cmp, k) : M.TreeMap} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.with_limit(K, V, k) : S.Model} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}): 90 LF.with_limit_ok(~K, ~V, ~cmp, k) 91 92 def get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.get(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.get(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 93 API.get_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 94 95 def contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.contains_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 96 API.contains_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 97 98 def get_or_default_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +fb: V) -> OK.POK(~K, ~V, ~cmp, V, S.get_or_default(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, fb), M.get_or_default(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, fb)): 99 API.get_or_default_ok(~K, ~V, ~cmp, ~o, sh, hg, k, fb) 100 101 def size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Nat, S.size(K, V, ST.model(~K, ~V, ~cmp, sh)), M.size(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 102 API.size_ok(~K, ~V, ~cmp, sh, hg) 103 104 def is_empty_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Bool, S.is_empty(K, V, ST.model(~K, ~V, ~cmp, sh)), M.is_empty(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 105 API.is_empty_ok(~K, ~V, ~cmp, sh, hg) 106 107 def first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 108 API.first_entry_ok(~K, ~V, ~cmp, sh, hg) 109 110 def last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 111 API.last_entry_ok(~K, ~V, ~cmp, sh, hg) 112 113 def first_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.first_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 114 API.first_key_ok(~K, ~V, ~cmp, sh, hg) 115 116 def last_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.last_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 117 API.last_key_ok(~K, ~V, ~cmp, sh, hg) 118 119 def lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 120 API.lower_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 121 122 def lower_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 123 API.lower_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 124 125 def floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 126 API.floor_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 127 128 def floor_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 129 API.floor_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 130 131 def ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 132 API.ceiling_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 133 134 def ceiling_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 135 API.ceiling_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 136 137 def higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 138 API.higher_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 139 140 def higher_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 141 API.higher_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 142 143 def put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)): 144 API.put_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 145 146 def put_if_absent_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put_if_absent(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)): 147 API.put_if_absent_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 148 149 def replace_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.replace(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)): 150 API.replace_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 151 152 def replace_if_equal_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +e: V, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e, w), M.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e, w)): 153 API.replace_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e, w) 154 155 def remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.remove(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)): 156 API.remove_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 157 158 def remove_if_equal_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +e: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e), M.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e)): 159 API.remove_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e) 160 161 def poll_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 162 API.poll_first_entry_ok(~K, ~V, ~cmp, ~o, sh, hg) 163 164 def poll_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 165 API.poll_last_entry_ok(~K, ~V, ~cmp, ~o, sh, hg) 166 167 def clear_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, s2_ => {M.clear(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == ST.real(~K, ~V, ~cmp, s2_) : M.TreeMap} & ({S.clear(K, V, ST.model(~K, ~V, ~cmp, sh)) == ST.model(~K, ~V, ~cmp, s2_) : S.Model} & {ST.good(~K, ~V, ~cmp, s2_) == True{} : Bool})>: 168 API.clear_ok(~K, ~V, ~cmp, sh, hg) 169 170 def iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 171 CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 172 173 def descending_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 174 CA.descending_iterator_ok(~K, ~V, ~cmp, sh, hg) 175 176 def iterator_has_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))): 177 CA.iterator_has_next_ok(~K, ~V, ~cmp, c, hc) 178 179 def iterator_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))): 180 CA.iterator_next_ok(~K, ~V, ~cmp, ~o, c, hc) 181 182 def iterator_next_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))): 183 CA.iterator_next_key_ok(~K, ~V, ~cmp, ~o, c, hc) 184 185 def iterator_next_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))): 186 CA.iterator_next_value_ok(~K, ~V, ~cmp, ~o, c, hc) 187 188 def iterator_set_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +v: V) -> CU.CPOK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c), v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c), v)): 189 CA.iterator_set_value_ok(~K, ~V, ~cmp, ~o, c, hc, v) 190 191 def iterator_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))): 192 CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, c, hc) 193 194 def iterator_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, s2 => {M.iterator_finish(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} & ({S.iterator_finish(K, V, CU.cmod(~K, ~V, ~cmp, c)) == ST.model(~K, ~V, ~cmp, s2) : S.Model} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>: 195 CA.iterator_finish_ok(~K, ~V, ~cmp, c, hc) 196 197 def contains_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, sh), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), w)): 198 CA.contains_value_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, w) 199 200 def head_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +up: M.Bound) -> VD.VOK(~K, ~V, ~cmp, S.head_map(K, V, ST.model(~K, ~V, ~cmp, sh), up), M.head_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), up)): 201 VW.head_map_ok(~K, ~V, ~cmp, sh, hg, up) 202 203 def tail_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound) -> VD.VOK(~K, ~V, ~cmp, S.tail_map(K, V, ST.model(~K, ~V, ~cmp, sh), lw), M.tail_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw)): 204 VW.tail_map_ok(~K, ~V, ~cmp, sh, hg, lw) 205 206 def descending_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.descending_map(K, V, ST.model(~K, ~V, ~cmp, sh)), M.descending_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 207 VW.descending_map_ok(~K, ~V, ~cmp, sh, hg) 208 209 def view_reverse_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_reverse(K, V, VD.vmod(~K, ~V, ~cmp, w)), M.view_reverse(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 210 VW.view_reverse_ok(~K, ~V, ~cmp, w, hw) 211 212 def view_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, s2 => {M.view_finish(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} & ({S.view_finish(K, V, VD.vmod(~K, ~V, ~cmp, w)) == ST.model(~K, ~V, ~cmp, s2) : S.Model} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>: 213 VW.view_finish_ok(~K, ~V, ~cmp, w, hw) 214 215 def sub_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound, +up: M.Bound) -> VW.ROK(~K, ~V, ~cmp, S.sub_map(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), lw, up), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up)): 216 VW.sub_map_ok(~K, ~V, ~cmp, sh, hg, lw, up) 217 218 def view_get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 219 VW.view_get_ok(~K, ~V, ~cmp, ~o, w, hw, k) 220 221 def view_contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 222 VW.view_contains_key_ok(~K, ~V, ~cmp, ~o, w, hw, k) 223 224 def view_put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +v: V) -> VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, v)): 225 VW.view_put_ok(~K, ~V, ~cmp, ~o, w, hw, k, v) 226 227 def view_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 228 VW.view_remove_ok(~K, ~V, ~cmp, ~o, w, hw, k) 229 230 def view_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.view_iterator(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.view_iterator(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 231 VA.view_iterator_ok(~K, ~V, ~cmp, ~o, w, hw) 232 233 def view_extreme_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +first: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_extreme(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), first), M.view_extreme(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), first)): 234 VA.view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, first) 235 236 def view_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_first_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_first_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 237 VA.view_first_entry_ok(~K, ~V, ~cmp, ~o, w, hw) 238 239 def view_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_last_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_last_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 240 VA.view_last_entry_ok(~K, ~V, ~cmp, ~o, w, hw) 241 242 def view_nav_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +higher: Bool, +incl: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, higher, incl), M.view_nav(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, higher, incl)): 243 VA.view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, higher, incl) 244 245 def view_lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, False{}), M.view_lower_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 246 VA.view_lower_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 247 248 def view_floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, True{}), M.view_floor_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 249 VA.view_floor_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 250 251 def view_ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, True{}), M.view_ceiling_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 252 VA.view_ceiling_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 253 254 def view_higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, False{}), M.view_higher_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 255 VA.view_higher_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 256 257 def view_size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Nat, S.view_size(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_size(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 258 VA.view_size_ok(~K, ~V, ~cmp, ~o, w, hw) 259 260 def view_clear_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_clear(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 261 VA.view_clear_ok(~K, ~V, ~cmp, ~o, w, hw) 262 263 def key_set_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.key_set(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 264 CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 265 266 def values_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.values(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 267 CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 268 269 def entry_set_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.entry_set(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 270 CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 271 272 273 # ==== the contract of main (stated in spec/containers/balanced_search_tree/main.bend) ==================== 274 275 # ---- lookups after an insertion ---- 276 def fis_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ha: {S.pick(Maybe<&2, M.Entry>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry>}, ih: @+ha2: {S.find_e(~K, ~V, ~cmp, k, t) == None{} : Maybe<&2, M.Entry>} -> {S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, t)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>}: 277 match c: 278 case LT{}: 279 %Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{M.Entry{k, v}}, S.find_e(~K, ~V, ~cmp, k, Con{e, t})) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>} 280 {==} 281 case EQ{}: 282 Empty.absurd({S.find_e(~K, ~V, ~cmp, k, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)}) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>}, L.none_some(M.Entry, e, Equal.sym(Maybe<&2, M.Entry>, Some{e}, None{}, ha))) 283 case GT{}: 284 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, t))) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>} 285 ih(ha) 286 287 # the inserted key is found, with its value 288 def find_ins_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +es: List<&2, M.Entry>, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, es)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>}: 289 match es: 290 case Nil{}: 291 %Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{M.Entry{k, v}}, None{}) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry>} 292 {==} 293 case Con{+e, +t}: 294 fis_c(~K, ~V, ~cmp, ~o, k, v, e, t, cmp(k, S.key(K, V, e)), {==}, ha, ha2 => find_ins_same(~K, ~V, ~cmp, ~o, k, v, t, ha2)) 295 296 def fio_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +ih: {S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry>}: 297 match c: 298 case LT{}: 299 %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry>, _, Some{M.Entry{k, v}}, S.find_e(~K, ~V, ~cmp, q, Con{e, t})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry>} 300 {==} 301 case EQ{}: 302 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 303 case GT{}: 304 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 305 306 # every other key is unchanged 307 def find_ins_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry>) -> S.Include.find_ins_other(~K, ~V, ~cmp, k, v, q, hq, es): 308 match es: 309 case Nil{}: 310 %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry>, _, Some{M.Entry{k, v}}, None{}) == None{} : Maybe<&2, M.Entry>} 311 {==} 312 case Con{+e, +t}: 313 fio_c(~K, ~V, ~cmp, k, v, q, hq, e, t, cmp(k, S.key(K, V, e)), find_ins_other(~K, ~V, ~cmp, k, v, q, hq, t)) 314 315 def ins_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +ih: {SC.length(M.Entry, S.ins(~K, ~V, ~cmp, k, v, t)) == 1n+SC.length(M.Entry, t) : Nat}) -> {SC.length(M.Entry, S.pick(List<&2, M.Entry>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == 1n+SC.length(M.Entry, Con{e, t}) : Nat}: 316 match c: 317 case LT{}: 318 {==} 319 case EQ{}: 320 Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry, S.ins(~K, ~V, ~cmp, k, v, t)), 1n+SC.length(M.Entry, t), ih) 321 case GT{}: 322 Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry, S.ins(~K, ~V, ~cmp, k, v, t)), 1n+SC.length(M.Entry, t), ih) 323 324 def ins_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry>) -> S.Include.ins_length(~K, ~V, ~cmp, k, v, es): 325 match es: 326 case Nil{}: 327 {==} 328 case Con{+e, +t}: 329 ins_len_c(~K, ~V, ~cmp, k, v, e, t, cmp(k, S.key(K, V, e)), ins_length(~K, ~V, ~cmp, k, v, t)) 330 331 # ---- lookups after a replacement ---- 332 def fss_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +hp: {S.pick(Maybe<&2, M.Entry>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == Some{e0} : Maybe<&2, M.Entry>}, ih: @+hp2: {S.find_e(~K, ~V, ~cmp, k, t) == Some{e0} : Maybe<&2, M.Entry>} -> {S.find(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)) == Some{v} : Maybe<&2, V>}) -> {S.find(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == Some{v} : Maybe<&2, V>}: 333 match c: 334 case EQ{}: 335 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), EQ{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, k, t))) == Some{v} : Maybe<&2, V>} 336 {==} 337 case LT{}: 338 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)))) == Some{v} : Maybe<&2, V>} 339 ih(hp) 340 case GT{}: 341 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)))) == Some{v} : Maybe<&2, V>} 342 ih(hp) 343 344 # a present key reads the new value 345 def find_set_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry, +es: List<&2, M.Entry>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Replace.find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp): 346 match es: 347 case Nil{}: 348 Empty.absurd({None{} == Some{v} : Maybe<&2, V>}, L.none_some(M.Entry, e0, hp)) 349 case Con{+e, +t}: 350 fss_c(~K, ~V, ~cmp, k, v, e0, e, t, cmp(k, S.key(K, V, e)), {==}, hp, hp2 => find_set_same(~K, ~V, ~cmp, k, v, e0, t, hp2)) 351 352 def fso_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ih: {S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry>}: 353 match c: 354 case EQ{}: 355 %O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, _)), Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, q, t)) == S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, _)), Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry>} 356 %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry>, _, Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, q, t)) == S.pick(Maybe<&2, M.Entry>, _, Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry>} 357 {==} 358 case LT{}: 359 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 360 case GT{}: 361 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 362 363 # every other key is unchanged 364 def find_set_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry>) -> S.Include.find_set_other(~K, ~V, ~cmp, ~o, k, v, q, hq, es): 365 match es: 366 case Nil{}: 367 {==} 368 case Con{+e, +t}: 369 fso_c(~K, ~V, ~cmp, ~o, k, v, q, hq, e, t, cmp(k, S.key(K, V, e)), {==}, find_set_other(~K, ~V, ~cmp, ~o, k, v, q, hq, t)) 370 371 def set_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +ih: {SC.length(M.Entry, S.set_val(~K, ~V, ~cmp, k, v, t)) == SC.length(M.Entry, t) : Nat}) -> {SC.length(M.Entry, S.pick(List<&2, M.Entry>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == SC.length(M.Entry, Con{e, t}) : Nat}: 372 match c: 373 case EQ{}: 374 {==} 375 case LT{}: 376 Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry, S.set_val(~K, ~V, ~cmp, k, v, t)), SC.length(M.Entry, t), ih) 377 case GT{}: 378 Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry, S.set_val(~K, ~V, ~cmp, k, v, t)), SC.length(M.Entry, t), ih) 379 380 def set_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry>) -> S.Include.set_length(~K, ~V, ~cmp, k, v, es): 381 match es: 382 case Nil{}: 383 {==} 384 case Con{+e, +t}: 385 set_len_c(~K, ~V, ~cmp, k, v, e, t, cmp(k, S.key(K, V, e)), set_length(~K, ~V, ~cmp, k, v, t)) 386 387 # ---- lookups after a deletion ---- 388 def fdo_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ih: {S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry>}: 389 match c: 390 case EQ{}: 391 %O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc) : {S.find_e(~K, ~V, ~cmp, q, t) == S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, _)), Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry>} 392 %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.find_e(~K, ~V, ~cmp, q, t) == S.pick(Maybe<&2, M.Entry>, _, Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry>} 393 {==} 394 case LT{}: 395 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 396 case GT{}: 397 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, q, t), ih) 398 399 # every other key is unchanged 400 def find_del_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry>) -> S.Exclude.find_del_other(~K, ~V, ~cmp, ~o, k, q, hq, es): 401 match es: 402 case Nil{}: 403 {==} 404 case Con{+e, +t}: 405 fdo_c(~K, ~V, ~cmp, ~o, k, q, hq, e, t, cmp(k, S.key(K, V, e)), {==}, find_del_other(~K, ~V, ~cmp, ~o, k, q, hq, t)) 406 407 def fds_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +hord: {S.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, ih: @+h2: {S.ordered(~K, ~V, ~cmp, t) == True{} : Bool} -> {S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry>}) -> {S.find_e(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == None{} : Maybe<&2, M.Entry>}: 408 match c: 409 case EQ{}: 410 %Equal.sym(K, k, S.key(K, V, e), O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc)) : {S.find_e(~K, ~V, ~cmp, _, t) == None{} : Maybe<&2, M.Entry>} 411 OR.gt_none(~K, ~V, ~cmp, S.key(K, V, e), t, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, hord)) 412 case LT{}: 413 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t))) == None{} : Maybe<&2, M.Entry>} 414 ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord)) 415 case GT{}: 416 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.pick(Maybe<&2, M.Entry>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t))) == None{} : Maybe<&2, M.Entry>} 417 ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord)) 418 419 # in an ordered map the deleted key is gone 420 def find_del_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +es: List<&2, M.Entry>, +hord: {S.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> S.Exclude.find_del_same(~K, ~V, ~cmp, ~o, k, es, hord): 421 match es: 422 case Nil{}: 423 {==} 424 case Con{+e, +t}: 425 fds_c(~K, ~V, ~cmp, ~o, k, e, t, cmp(k, S.key(K, V, e)), {==}, hord, h2 => find_del_same(~K, ~V, ~cmp, ~o, k, t, h2)) 426 427 def del_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +hp: {S.pick(Maybe<&2, M.Entry>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == Some{e0} : Maybe<&2, M.Entry>}, ih: @+hp2: {S.find_e(~K, ~V, ~cmp, k, t) == Some{e0} : Maybe<&2, M.Entry>} -> {1n+SC.length(M.Entry, S.del(~K, ~V, ~cmp, k, t)) == SC.length(M.Entry, t) : Nat}) -> {1n+SC.length(M.Entry, S.pick(List<&2, M.Entry>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == SC.length(M.Entry, Con{e, t}) : Nat}: 428 match c: 429 case EQ{}: 430 {==} 431 case LT{}: 432 Equal.cong(Nat, Nat, z => 1n+z, 1n+SC.length(M.Entry, S.del(~K, ~V, ~cmp, k, t)), SC.length(M.Entry, t), ih(hp)) 433 case GT{}: 434 Equal.cong(Nat, Nat, z => 1n+z, 1n+SC.length(M.Entry, S.del(~K, ~V, ~cmp, k, t)), SC.length(M.Entry, t), ih(hp)) 435 436 # deleting a present key removes exactly one entry 437 def del_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry, +es: List<&2, M.Entry>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Exclude.del_length(~K, ~V, ~cmp, k, e0, es, hp): 438 match es: 439 case Nil{}: 440 Empty.absurd({1n+SC.length(M.Entry, S.del(~K, ~V, ~cmp, k, Nil{})) == SC.length(M.Entry, Nil{}) : Nat}, L.none_some(M.Entry, e0, hp)) 441 case Con{+e, +t}: 442 del_len_c(~K, ~V, ~cmp, k, e0, e, t, cmp(k, S.key(K, V, e)), hp, hp2 => del_length(~K, ~V, ~cmp, k, e0, t, hp2)) 443 444 def del_abs_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e: M.Entry, +t: List<&2, M.Entry>, +c: Cmp, +ha: {S.pick(Maybe<&2, M.Entry>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry>}, ih: @+ha2: {S.find_e(~K, ~V, ~cmp, k, t) == None{} : Maybe<&2, M.Entry>} -> {S.del(~K, ~V, ~cmp, k, t) == t : List<&2, M.Entry>}) -> {S.pick(List<&2, M.Entry>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)}) == Con{e, t} : List<&2, M.Entry>}: 445 match c: 446 case EQ{}: 447 Empty.absurd({t == Con{e, t} : List<&2, M.Entry>}, L.none_some(M.Entry, e, Equal.sym(Maybe<&2, M.Entry>, Some{e}, None{}, ha))) 448 case LT{}: 449 Equal.cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha)) 450 case GT{}: 451 Equal.cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha)) 452 453 # deleting an absent key changes nothing 454 def del_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +es: List<&2, M.Entry>, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}) -> {S.del(~K, ~V, ~cmp, k, es) == es : List<&2, M.Entry>}: 455 match es: 456 case Nil{}: 457 {==} 458 case Con{+e, +t}: 459 del_abs_c(~K, ~V, ~cmp, k, e, t, cmp(k, S.key(K, V, e)), ha, ha2 => del_absent(~K, ~V, ~cmp, k, t, ha2)) 460 461 # ---- the operations, on the model ---- 462 def new_empty(-K: Data, -V: Data) -> S.Empty_Map.new_empty(K, V): 463 {==} 464 465 def size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Length.size_value(K, V, l, es): 466 {==} 467 468 def is_empty_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Length.is_empty_value(K, V, l, es): 469 {==} 470 471 def clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Clear.clear_empty(K, V, l, es): 472 {==} 473 474 # Element / Find: the model's value, the map unchanged 475 def get_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K) -> S.Element.get_value(~K, ~V, ~cmp, l, es, k): 476 {==} 477 478 def get_or_default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +d: V) -> S.Element.get_or_default_value(~K, ~V, ~cmp, l, es, k, d): 479 {==} 480 481 def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K) -> S.Contains.contains_value(~K, ~V, ~cmp, l, es, k): 482 {==} 483 484 # Include: a present key is replaced (put_found, put_others via find_set_*) 485 def put_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +e0: M.Entry, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Include.put_present(~K, ~V, ~cmp, l, es, k, v, e0, hp): 486 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{S.val(K, V, e0)}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 487 {==} 488 489 # an absent key with room is inserted (put_found, put_others via find_ins_*) 490 def put_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}, +hr: {Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)) == True{} : Bool}) -> S.Include.put_absent(~K, ~V, ~cmp, l, es, k, v, ha, hr): 491 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 492 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)), True{}, hr) : {S.pick(S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 493 {==} 494 495 # a full map rejects a new key and changes nothing (SPARK: Pre => Length < Capacity) 496 def put_full(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}, +hr: {Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)) == False{} : Bool}) -> S.Include.put_full(~K, ~V, ~cmp, l, es, k, v, ha, hr): 497 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 498 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)), False{}, hr) : {S.pick(S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 499 {==} 500 501 # the included key is found with its value, whether it was present or not 502 def put_found_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +e0: M.Entry, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Include.put_found_present(~K, ~V, ~cmp, l, es, k, v, e0, hp): 503 find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp) 504 505 def put_found_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}) -> S.Include.put_found_absent(~K, ~V, ~cmp, ~o, l, es, k, v, ha): 506 Equal.cong(Maybe<&2, M.Entry>, Maybe<&2, V>, z => S.val_m(K, V, z), S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, es)), Some{M.Entry{k, v}}, find_ins_same(~K, ~V, ~cmp, ~o, k, v, es, ha)) 507 508 # Insert (put_if_absent): a present key is left as it is 509 def put_if_absent_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +e0: M.Entry, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Insert.put_if_absent_present(~K, ~V, ~cmp, l, es, k, v, e0, hp): 510 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.absent_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, Done{Some{S.val(K, V, e0)}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 511 {==} 512 513 def put_if_absent_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}, +hr: {Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)) == True{} : Bool}) -> S.Insert.put_if_absent_absent(~K, ~V, ~cmp, l, es, k, v, ha, hr): 514 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.absent_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 515 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry, es), SC.pow2(l)), True{}, hr) : {S.pick(S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>} 516 {==} 517 518 # Replace: only a present key, returning the old value 519 def replace_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +e0: M.Entry, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Replace.replace_present(~K, ~V, ~cmp, l, es, k, v, e0, hp): 520 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.replace_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.set_val(~K, ~V, ~cmp, k, v, es)}, Some{S.val(K, V, e0)}) : S.Model & Maybe<&2, V>} 521 {==} 522 523 def replace_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}) -> S.Replace.replace_absent(~K, ~V, ~cmp, l, es, k, v, ha): 524 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.replace_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, None{}) : S.Model & Maybe<&2, V>} 525 {==} 526 527 # Delete / Exclude: a present key is removed and its value returned 528 # (remove_gone: find_del_same, remove_others: find_del_other, 529 # remove_length: del_length) 530 def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +e0: M.Entry, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry>}) -> S.Exclude.remove_present(~K, ~V, ~cmp, l, es, k, e0, hp): 531 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {(S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, S.val_m(K, V, _)) == (S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, Some{S.val(K, V, e0)}) : S.Model & Maybe<&2, V>} 532 {==} 533 534 # an absent key: nothing changes 535 def remove_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry>}) -> S.Exclude.remove_absent(~K, ~V, ~cmp, l, es, k, ha): 536 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {(S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, S.val_m(K, V, _)) == (S.TM{l, es}, None{}) : S.Model & Maybe<&2, V>} 537 %Equal.sym(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, k, es), es, del_absent(~K, ~V, ~cmp, k, es, ha)) : {(S.TM{l, _}, None{}) == (S.TM{l, es}, None{}) : S.Model & Maybe<&2, V>} 538 {==} 539 540 # First / Last: the first and last entries of the order, the map unchanged 541 def first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.First.first_value(K, V, l, es): 542 {==} 543 544 def last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Last.last_value(K, V, l, es): 545 {==} 546 547 # Floor / Ceiling (and the strict lower / higher): the model's nav 548 def nav_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry>, +k: K, +up: Bool, +inclusive: Bool) -> S.Floor.nav_value(~K, ~V, ~cmp, l, es, k, up, inclusive): 549 {==}