import Base import ../../../spec/containers/balanced_search_tree/main.bend as S import ../../../spec/lib/common.bend as SC import ../../../spec/lib/order.bend as SO import ../../../src/containers/balanced_search_tree.bend as M import ../../../src/containers/dynamic_array.bend as D import ../../lib/list.bend as LL import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/order.bend as O import ./api.bend as API import ./capi.bend as CA import ./ccv.bend as CV import ./cnx.bend as CX import ./crm.bend as CR import ./csv.bend as CS import ./cur.bend as CU import ./ends.bend as EN import ./life.bend as LF import ./mirror.bend as MI import ./navm.bend as NM import ./ok.bend as OK import ./ord.bend as OR import ./prim.bend as PR import ./putm.bend as PM import ./reads.bend as RD import ./rmi.bend as RI import ./rmp.bend as RP import ./rmv.bend as RV import ./sim.bend as SM import ./state.bend as ST import ./vapi.bend as VA import ./vclr.bend as VC import ./vdef.bend as VD import ./vit.bend as VI import ./vnav.bend as VN import ./vsp.bend as VS import ./vsz.bend as VZ import ./vw.bend as VW # Indexed TreeMap (src/containers/balanced_search_tree.bend): public proof # entry point, generated by tools/generators/tm_gate.py. # shadow ST.Sh: the map's Nat fields (size, root, first and last ids, # free head, limit and depth), the node and payload arrays as # lists, and two ghost values: the tree of ids (ST.Tr) and the # free list; ST.real(sh) is the map # abstraction ST.model(sh): the limit and the entries of the tree's ids in # order, as a spec map (sorted entries); # a mirror cursor's model is the specification's cursor over # that map with the keys of its next and current ids # (CU.cmod), a mirror view's the specification's view # (VD.vmod) # invariant ST.good(sh): the arrays laid out within the limit, the ghost # tree the red-black tree the links describe (parents, sides, # colours, black height), every id of the tree a live node with # a payload, the free list chained through the vacant slots, # the ids of tree and free list without repeats and covering # the slots, the entries sorted by a lawful comparator, and the # size, root and first/last ids those of the tree # (state.bend); a cursor is good when its # shadow is and its ids are 0 or ids of the tree (CU.cgood) # # Proved for every lawful comparator (O.Order: flip, antisymmetry, # transitivity), every key and value type (Data), every good shadow, cursor # and view, and every argument: each operation's result is the real map (or # cursor, or view) of a good shadow whose model is the specification's # result, with the same answer (OK.POK / CU.CPOK / VD.VPOK and the like). # new, with_limit a good shadow of the specification's empty map # reads size, is_empty, get, get_or_default, contains_key, # contains_value, first/last entry and key, the # lower/floor/ceiling/higher entries and keys # updates put, put_if_absent, replace, replace_if_equal, # remove, remove_if_equal, poll_first/last_entry, # clear # cursors iterator, descending_iterator, key_set, values, # entry_set, iterator_next(_key, _value), # iterator_has_next, iterator_set_value, # iterator_remove, iterator_finish # views sub_map, head_map, tail_map, descending_map, # view_reverse, view_finish, view_get, # view_contains_key, view_put, view_remove, # view_size, view_clear, view_first/last_entry, # view_lower/floor/ceiling/higher_entry, # view_iterator 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}): LF.new_ok(~K, ~V, ~cmp) 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}): LF.with_limit_ok(~K, ~V, ~cmp, k) 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)): API.get_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.contains_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.get_or_default_ok(~K, ~V, ~cmp, ~o, sh, hg, k, fb) 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))): API.size_ok(~K, ~V, ~cmp, sh, hg) 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))): API.is_empty_ok(~K, ~V, ~cmp, sh, hg) 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))): API.first_entry_ok(~K, ~V, ~cmp, sh, hg) 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))): API.last_entry_ok(~K, ~V, ~cmp, sh, hg) 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))): API.first_key_ok(~K, ~V, ~cmp, sh, hg) 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))): API.last_key_ok(~K, ~V, ~cmp, sh, hg) 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)): API.lower_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.lower_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.floor_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.floor_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.ceiling_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.ceiling_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.higher_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.higher_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.put_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 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)): API.put_if_absent_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 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)): API.replace_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v) 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)): API.replace_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e, w) 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)): API.remove_ok(~K, ~V, ~cmp, ~o, sh, hg, k) 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)): API.remove_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e) 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))): API.poll_first_entry_ok(~K, ~V, ~cmp, ~o, sh, hg) 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))): API.poll_last_entry_ok(~K, ~V, ~cmp, ~o, sh, hg) 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})>: API.clear_ok(~K, ~V, ~cmp, sh, hg) 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})>: CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 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})>: CA.descending_iterator_ok(~K, ~V, ~cmp, sh, hg) 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))): CA.iterator_has_next_ok(~K, ~V, ~cmp, c, hc) 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))): CA.iterator_next_ok(~K, ~V, ~cmp, ~o, c, hc) 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))): CA.iterator_next_key_ok(~K, ~V, ~cmp, ~o, c, hc) 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))): CA.iterator_next_value_ok(~K, ~V, ~cmp, ~o, c, hc) 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)): CA.iterator_set_value_ok(~K, ~V, ~cmp, ~o, c, hc, v) 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))): CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, c, hc) 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})>: CA.iterator_finish_ok(~K, ~V, ~cmp, c, hc) 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)): CA.contains_value_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, w) 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)): VW.head_map_ok(~K, ~V, ~cmp, sh, hg, up) 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)): VW.tail_map_ok(~K, ~V, ~cmp, sh, hg, lw) 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))): VW.descending_map_ok(~K, ~V, ~cmp, sh, hg) 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))): VW.view_reverse_ok(~K, ~V, ~cmp, w, hw) 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})>: VW.view_finish_ok(~K, ~V, ~cmp, w, hw) 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)): VW.sub_map_ok(~K, ~V, ~cmp, sh, hg, lw, up) 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)): VW.view_get_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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)): VW.view_contains_key_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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)): VW.view_put_ok(~K, ~V, ~cmp, ~o, w, hw, k, v) 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)): VW.view_remove_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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})>: VA.view_iterator_ok(~K, ~V, ~cmp, ~o, w, hw) 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)): VA.view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, first) 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))): VA.view_first_entry_ok(~K, ~V, ~cmp, ~o, w, hw) 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))): VA.view_last_entry_ok(~K, ~V, ~cmp, ~o, w, hw) 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)): VA.view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, higher, incl) 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)): VA.view_lower_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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)): VA.view_floor_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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)): VA.view_ceiling_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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)): VA.view_higher_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k) 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))): VA.view_size_ok(~K, ~V, ~cmp, ~o, w, hw) 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))): VA.view_clear_ok(~K, ~V, ~cmp, ~o, w, hw) 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})>: CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 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})>: CA.iterator_ok(~K, ~V, ~cmp, sh, hg) 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})>: CA.iterator_ok(~K, ~V, ~cmp, sh, hg) # ==== the contract of main (stated in spec/containers/balanced_search_tree/main.bend) ==================== # ---- lookups after an insertion ---- 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>}: match c: case LT{}: %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>} {==} case EQ{}: 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))) case GT{}: %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>} ih(ha) # the inserted key is found, with its value 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>}: match es: case Nil{}: %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>} {==} case Con{+e, +t}: 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)) 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>}: match c: case LT{}: %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>} {==} case EQ{}: 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) case GT{}: 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) # every other key is unchanged 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): match es: case Nil{}: %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>} {==} case Con{+e, +t}: 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)) 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}: match c: case LT{}: {==} case EQ{}: 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) case GT{}: 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) 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): match es: case Nil{}: {==} case Con{+e, +t}: 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)) # ---- lookups after a replacement ---- 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>}: match c: case EQ{}: %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>} {==} case LT{}: %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>} ih(hp) case GT{}: %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>} ih(hp) # a present key reads the new value 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): match es: case Nil{}: Empty.absurd({None{} == Some{v} : Maybe<&2, V>}, L.none_some(M.Entry, e0, hp)) case Con{+e, +t}: 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)) 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>}: match c: case EQ{}: %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>} %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>} {==} case LT{}: 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) case GT{}: 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) # every other key is unchanged 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): match es: case Nil{}: {==} case Con{+e, +t}: 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)) 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}: match c: case EQ{}: {==} case LT{}: 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) case GT{}: 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) 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): match es: case Nil{}: {==} case Con{+e, +t}: 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)) # ---- lookups after a deletion ---- 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>}: match c: case EQ{}: %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>} %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>} {==} case LT{}: 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) case GT{}: 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) # every other key is unchanged 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): match es: case Nil{}: {==} case Con{+e, +t}: 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)) 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>}: match c: case EQ{}: %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>} OR.gt_none(~K, ~V, ~cmp, S.key(K, V, e), t, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, hord)) case LT{}: %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>} ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord)) case GT{}: %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>} ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord)) # in an ordered map the deleted key is gone 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): match es: case Nil{}: {==} case Con{+e, +t}: 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)) 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}: match c: case EQ{}: {==} case LT{}: 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)) case GT{}: 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)) # deleting a present key removes exactly one entry 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): match es: case Nil{}: 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)) case Con{+e, +t}: 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)) 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>}: match c: case EQ{}: 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))) case LT{}: Equal.cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha)) case GT{}: Equal.cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha)) # deleting an absent key changes nothing 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>}: match es: case Nil{}: {==} case Con{+e, +t}: 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)) # ---- the operations, on the model ---- def new_empty(-K: Data, -V: Data) -> S.Empty_Map.new_empty(K, V): {==} def size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Length.size_value(K, V, l, es): {==} def is_empty_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Length.is_empty_value(K, V, l, es): {==} def clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Clear.clear_empty(K, V, l, es): {==} # Element / Find: the model's value, the map unchanged 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): {==} 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): {==} 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): {==} # Include: a present key is replaced (put_found, put_others via find_set_*) 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): %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>>} {==} # an absent key with room is inserted (put_found, put_others via find_ins_*) 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): %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>>} %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>>} {==} # a full map rejects a new key and changes nothing (SPARK: Pre => Length < Capacity) 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): %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>>} %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>>} {==} # the included key is found with its value, whether it was present or not 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): find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp) 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): 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)) # Insert (put_if_absent): a present key is left as it is 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): %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>>} {==} 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): %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>>} %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>>} {==} # Replace: only a present key, returning the old value 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): %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>} {==} 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): %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>} {==} # Delete / Exclude: a present key is removed and its value returned # (remove_gone: find_del_same, remove_others: find_del_other, # remove_length: del_length) 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): %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>} {==} # an absent key: nothing changes 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): %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>} %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>} {==} # First / Last: the first and last entries of the order, the map unchanged def first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.First.first_value(K, V, l, es): {==} def last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry>) -> S.Last.last_value(K, V, l, es): {==} # Floor / Ceiling (and the strict lower / higher): the model's nav 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): {==}