~/bend-docscommunity

proofs/containers/hash_table/proof.bend source

proofs/containers/hash_table/proof.bend on the hub · documented module

import Baseimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/lib/common.bend as SCimport ../../../src/containers/hash_table.bend as Himport ./state.bend as STimport ./new.bend as NWimport ./get.bend as Gimport ./has.bend as HAimport ./size.bend as SZimport ./set.bend as ST2import ./setok.bend as SOimport ./pop.bend as POimport ./keysw.bend as KWimport ./keys.bend as Kimport ./speclem.bend as SLimport ../../lib/logic.bend as Limport ../../lib/array.bend as ARimport ./poplem.bend as PLimport ./table.bend as TBimport ../../lib/u32div.bend as UD# Hash map (src/containers/hash_table.bend): public proof entry point.#   shadow       ST.Sh: the map's U32 fields, the table and arena exponents#                and a mirror tree for each array; ST.real(sh) is the map#   abstraction  ST.model(sh): the entries of the full buckets, in bucket#                order, as a proofs/spec/hash_table.bend association list#   invariant    ST.good(sh): clusters, check words, unique keys and links,#                live slots, the count and load, and the exact free list#                (proofs/hash_table/state.bend, generated by#                tools/generators/hash_table_state.py)## Every operation is proved for every shadow satisfying the invariant, keys# of every length, and every value type V (Data):#   new            the empty model#   get/has/size   the specification's answer; map and model kept#   set            every lookup and the size are the specification's set's#                  (precondition: 2(n + 1) <= 2^cap with cap <= 30, i.e. the#                  table stays below 2^31 buckets)#   pop/del        the specification's lookup, then its remove#   keys           the model's keys, in order# and each result shadow satisfies the invariant again.## The *_contract theorems restate set, pop, del and keys as SPARK-style# contracts (stated in spec/containers/hash_table.bend, after SPARKlib's# formal hashed maps): what each operation changes and what it preserves in# the model (the value of every key), the length and the key sequence. The# key_* laws make key comparison an equivalence under which equivalent keys# are identical, so every function of a key (the hash too) agrees on them.def new_ok(~V: Data) -> {H.new(&2, V) == ST.real(~V, NW.empty(~V)) : H.HashMap<&2, V>} & ({ST.good(~V, NW.empty(~V)) == True{} : Bool} & {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}):  NW.new_ok(~V)def get_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String) -> G.GetOK(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key)):  G.get_ok(~V, sh, hg, dflt, key)def has_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> HA.HasOK(~V, sh, key, H.has(&2, V, ST.real(~V, sh), key)):  HA.has_ok(~V, sh, hg, key)def size_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32} & {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}:  SZ.size_ok(~V, sh, hg)def set_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+S.size(~V, ST.model(~V, sh))), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V) -> ST2.SetOK(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x)):  SO.set_ok(~V, sh, hg, cap, hc30, hcap, key, x)def pop_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PO.PopOK(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key)):  PO.pop_ok(~V, sh, hg, key)def del_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PO.DelOK(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)):  PO.del_ok(~V, sh, hg, key)def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KW.KeysOK(~V, sh, H.keys(&2, V, ST.real(~V, sh))):  KW.keys_ok(~V, sh, hg)# ---- contracts ----# ==== the contract of hash_table (stated in spec/containers/hash_table.bend) ====================# ---- key equivalence ----def key_refl(+a: String) -> S.Equivalent_Keys.key_refl(a):  K.str_refl(a)def key_sym(+a: String, +b: String) -> S.Equivalent_Keys.key_sym(a, b):  K.str_sym(a, b)def key_trans(+a: String, +b: String, +c: String, +hab: {S.str_eq(a, b) == True{} : Bool}, +hbc: {S.str_eq(b, c) == True{} : Bool}) -> S.Equivalent_Keys.key_trans(a, b, c, hab, hbc):  SL.eq_tr(a, b, c, hab, True{}, hbc)# equivalent keys are the same stringdef key_same(+a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> S.Equivalent_Keys.key_same(a, b, h):  K.str_eq_of(a, b, h)# and so every function of a key (the hash included) agrees on themdef key_respect(~A: Data, ~f: String -> A, +a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> S.Equivalent_Keys.key_respect(~A, ~f, a, b, h):  Equal.cong(String, A, f, a, b, K.str_eq_of(a, b, h))# ---- facts about the specification ----def mh_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +q: String, +c: Bool, +hc: {S.str_eq(j, q) == c : Bool}, +ih: {S.mem(q, S.keys(~V, t)) == S.has(~V, t, q) : Bool}) -> {Bool.or(S.str_eq(j, q), S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q))) : Bool}:  match c:    case True{}:      %Equal.sym(Bool, S.str_eq(j, q), True{}, hc) : {Bool.or(_, S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, _, Some{v}, S.lookup(~V, t, q))) : Bool}      {==}    case False{}:      %Equal.sym(Bool, S.str_eq(j, q), False{}, hc) : {Bool.or(_, S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, _, Some{v}, S.lookup(~V, t, q))) : Bool}      ih# a key is in the key sequence exactly when the model has itdef mem_has(~V: Data, +m: List<&2, S.Entry<V>>, +q: String) -> {S.mem(q, S.keys(~V, m)) == S.has(~V, m, q) : Bool}:  match m:    case Nil{}:      {==}    case Con{S.E{+j, +v}, +t}:      mh_c(~V, j, v, t, q, S.str_eq(j, q), {==}, mem_has(~V, t, q))# the key sequence is as long as the mapdef keys_len(~V: Data, +m: List<&2, S.Entry<V>>) -> {SC.length(String, S.keys(~V, m)) == S.size(~V, m) : Nat}:  match m:    case Nil{}:      {==}    case Con{S.E{+j, +v}, +t}:      Equal.cong(Nat, Nat, z => 1n+z, SC.length(String, S.keys(~V, t)), S.size(~V, t), keys_len(~V, t))# has is false exactly when the lookup is Nonedef none_of(~V: Data, +mv: Maybe<&2, V>, +h: {S.is_some(~V, mv) == False{} : Bool}) -> {mv == None{} : Maybe<&2, V>}:  match mv:    case None{}:      {==}    case Some{v}:      Empty.absurd({Some{v} == None{} : Maybe<&2, V>}, L.true_false(h))def ssp(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +mv: Maybe<&2, V>, +hmv: {S.lookup(~V, m, key) == mv : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)) : Nat}:  match mv:    case None{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), None{}, hmv) : {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.is_some(~V, _), S.size(~V, m), 1n+S.size(~V, m)) : Nat}      SL.size_set_new(~V, m, key, x, hmv)    case Some{+v0}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), Some{v0}, hmv) : {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.is_some(~V, _), S.size(~V, m), 1n+S.size(~V, m)) : Nat}      SL.size_set_old(~V, m, key, x, v0, hmv)# set grows the map by one exactly when the key was absentdef size_set(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V) -> {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)) : Nat}:  ssp(~V, m, key, x, S.lookup(~V, m, key), {==})def srp(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +mv: Maybe<&2, V>, +hmv: {S.lookup(~V, m, key) == mv : Maybe<&2, V>}) -> {Bool.pick(Nat, S.has(~V, m, key), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}:  match mv:    case None{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), None{}, hmv) : {Bool.pick(Nat, S.is_some(~V, _), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}      Equal.cong(List<&2, S.Entry<V>>, Nat, z => S.size(~V, z), S.remove(~V, m, key), m, SL.remove_none(~V, m, key, hmv))    case Some{+v0}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), Some{v0}, hmv) : {Bool.pick(Nat, S.is_some(~V, _), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}      SL.size_remove_old(~V, m, key, v0, hmv)# remove shrinks the map by one exactly when the key was presentdef size_remove(~V: Data, +m: List<&2, S.Entry<V>>, +key: String) -> {Bool.pick(Nat, S.has(~V, m, key), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}:  srp(~V, m, key, S.lookup(~V, m, key), {==})def hso_c(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.has(~V, S.set(~V, m, key, x), q) == Bool.or(c, S.mem(q, S.keys(~V, m))) : Bool}:  match c:    case True{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m, key, x), q), Some{x}, SL.lookup_set_same(~V, m, key, x, q, hc)) : {S.is_some(~V, _) == Bool.or(True{}, S.mem(q, S.keys(~V, m))) : Bool}      {==}    case False{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m, key, x), q), S.lookup(~V, m, q), SL.lookup_set_other(~V, m, key, x, q, hc)) : {S.is_some(~V, _) == Bool.or(False{}, S.mem(q, S.keys(~V, m))) : Bool}      Equal.sym(Bool, S.mem(q, S.keys(~V, m)), S.has(~V, m, q), mem_has(~V, m, q))def hro_c(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +q: String, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.has(~V, S.remove(~V, m, key), q) == Bool.and(Bool.not(c), S.mem(q, S.keys(~V, m))) : Bool}:  match c:    case True{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, m, key), q), None{}, SL.lookup_remove_same(~V, m, key, q, hc, hnd)) : {S.is_some(~V, _) == Bool.and(Bool.not(True{}), S.mem(q, S.keys(~V, m))) : Bool}      {==}    case False{}:      %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), SL.lookup_remove_other(~V, m, key, q, hc)) : {S.is_some(~V, _) == Bool.and(Bool.not(False{}), S.mem(q, S.keys(~V, m))) : Bool}      Equal.sym(Bool, S.mem(q, S.keys(~V, m)), S.has(~V, m, q), mem_has(~V, m, q))# ---- the invariant keeps keys unique ----def model_nodup(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {S.nodup(S.keys(~V, ST.model(~V, sh))) == True{} : Bool}:  match sh:    case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:      PL.nodup_model(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))def keys_post(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.KeysPost(~V, ST.model(~V, sh)):  (model_nodup(~V, sh, hg), (keys_len(~V, ST.model(~V, sh)), q => mem_has(~V, ST.model(~V, sh), q)))# keys returns the key sequence and changes nothingdef KeysContract(~V: Data, +sh: ST.Sh<V>, r: H.HashMap<&2, V> & List<&2, String>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.keys(~V, ST.model(~V, sh))) : H.HashMap<&2, V> & List<&2, String>} & (({ST.good(~V, sh2) == True{} : Bool} & {ST.model(~V, sh2) == ST.model(~V, sh) : List<&2, S.Entry<V>>}) & S.KeysPost(~V, ST.model(~V, sh)))>def kc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, -r: H.HashMap<&2, V> & List<&2, String>, ko: KW.KeysOK(~V, sh, r)) -> KeysContract(~V, sh, r):  match ko:    case Tuple{+sh2, Tuple{+e, rest}}:      (sh2, (e, (rest, keys_post(~V, sh, hg))))def SetContract(~V: Data, +sh: ST.Sh<V>, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.SetPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key, x))>def set_same(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == Some{x} : Maybe<&2, V>}:  Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), Some{x}, hl, SL.lookup_set_same(~V, m, key, x, q, hq))def set_other(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:  Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), S.lookup(~V, m, q), hl, SL.lookup_set_other(~V, m, key, x, q, hq))def set_mem(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.mem(q, S.keys(~V, m2)) == Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))) : Bool}:  Equal.trans(Bool, S.mem(q, S.keys(~V, m2)), S.has(~V, m2, q), Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))), mem_has(~V, m2, q),    Equal.trans(Bool, S.has(~V, m2, q), S.has(~V, S.set(~V, m, key, x), q), Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))), Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), hl), hso_c(~V, m, key, x, q, S.str_eq(key, q), {==})))def set_post(~V: Data, ~m: List<&2, S.Entry<V>>, ~m2: List<&2, S.Entry<V>>, ~key: String, ~x: V, ~hp: (@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) & {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, +hnd: {S.nodup(S.keys(~V, m2)) == True{} : Bool}, hk: @+hq0: {S.has(~V, m, key) == True{} : Bool} -> {S.keys(~V, m2) == S.keys(~V, m) : List<&2, String>}) -> S.Include.set_post(~V, ~m, ~m2, ~key, ~x, ~hp, hnd, hk):  (Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, key), Some{x}, set_same(~V, m, m2, key, x, key, K.str_refl(key), Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(key))),   (q => hq => set_same(~V, m, m2, key, x, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)),    (q => hq => set_other(~V, m, m2, key, x, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)),     (Equal.trans(Nat, S.size(~V, m2), S.size(~V, S.set(~V, m, key, x)), Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)), Pair.snd(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp), size_set(~V, m, key, x)),      (q => set_mem(~V, m, m2, key, x, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)), (hnd, hk))))))def sc_from(~V: Data, +sh: ST.Sh<V>, +key: String, +x: V, -r: H.HashMap<&2, V>, so: ST2.SetOK(~V, sh, key, x, r)) -> SetContract(~V, sh, key, x, r):  match so:    case Tuple{+sh2, Tuple{+e, rest}}:      (old, kk) = rest      (+hg2, rest2) = old      (sh2, (e, (hg2, set_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~x, ~rest2, model_nodup(~V, sh2, hg2), kk))))def PopContract(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V> & Maybe<&2, V>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.lookup(~V, ST.model(~V, sh), key)) : H.HashMap<&2, V> & Maybe<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.DelPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key))>def DelContract(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.DelPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key))>def del_absent(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +hn: {S.has(~V, m, key) == False{} : Bool}, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:  Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), hl, Equal.cong(List<&2, S.Entry<V>>, Maybe<&2, V>, z => S.lookup(~V, z, q), S.remove(~V, m, key), m, SL.remove_none(~V, m, key, none_of(~V, S.lookup(~V, m, key), hn))))def del_other(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:  Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), hl, SL.lookup_remove_other(~V, m, key, q, hq))def del_mem(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.mem(q, S.keys(~V, m2)) == Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))) : Bool}:  Equal.trans(Bool, S.mem(q, S.keys(~V, m2)), S.has(~V, m2, q), Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))), mem_has(~V, m2, q),    Equal.trans(Bool, S.has(~V, m2, q), S.has(~V, S.remove(~V, m, key), q), Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))), Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), hl), hro_c(~V, m, key, q, hnd, S.str_eq(key, q), {==})))def del_post(~V: Data, ~m: List<&2, S.Entry<V>>, ~m2: List<&2, S.Entry<V>>, ~key: String, ~hp: (@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) & {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +hnd2: {S.nodup(S.keys(~V, m2)) == True{} : Bool}) -> S.DelPost(~V, m, m2, key):  (Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, key), None{}, Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, key), S.lookup(~V, S.remove(~V, m, key), key), None{}, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(key), SL.lookup_remove_same(~V, m, key, key, K.str_refl(key), hnd))),   (q => hq => del_other(~V, m, m2, key, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)),    (hn => q => del_absent(~V, m, m2, key, hn, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)),     (%Equal.sym(Nat, S.size(~V, m2), S.size(~V, S.remove(~V, m, key)), Pair.snd(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)) : {Bool.pick(Nat, S.has(~V, m, key), 1n+_, _) == S.size(~V, m) : Nat}      size_remove(~V, m, key),      (q => del_mem(~V, m, m2, key, hnd, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)), hnd2)))))def pc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, -r: H.HashMap<&2, V> & Maybe<&2, V>, po: PO.PopOK(~V, sh, key, r)) -> PopContract(~V, sh, key, r):  match po:    case Tuple{+sh2, Tuple{+e, rest}}:      (+hg2, rest2) = rest      (sh2, (e, (hg2, del_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~rest2, model_nodup(~V, sh, hg), model_nodup(~V, sh2, hg2)))))def dc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, -r: H.HashMap<&2, V>, po: PO.DelOK(~V, sh, key, r)) -> DelContract(~V, sh, key, r):  match po:    case Tuple{+sh2, Tuple{+e, rest}}:      (+hg2, rest2) = rest      (sh2, (e, (hg2, del_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~rest2, model_nodup(~V, sh, hg), model_nodup(~V, sh2, hg2)))))# ---- reads (SPARK's Element, Contains, Length, Empty_Map) ----def gv_of(~V: Data, +sh: ST.Sh<V>, +dflt: V, +key: String, -r: H.HashMap<&2, V> & V, ok: G.GetOK(~V, sh, dflt, key, r)) -> {Pair.snd(H.HashMap<&2, V>, V, r) == S.get(~V, dflt, ST.model(~V, sh), key) : V}:  match ok:    case Tuple{+sh2, Tuple{+e, rest}}:      %Equal.sym(H.HashMap<&2, V> & V, r, (ST.real(~V, sh2), S.get(~V, dflt, ST.model(~V, sh), key)), e) : {Pair.snd(H.HashMap<&2, V>, V, _) == S.get(~V, dflt, ST.model(~V, sh), key) : V}      {==}# Element (Container, Key) = Element (Model, Key) when the key is presentdef element_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String, +x: V, +hl: {S.lookup(~V, ST.model(~V, sh), key) == Some{x} : Maybe<&2, V>}) -> S.Element.element_value(~V, ST.model(~V, sh), key, x, hl, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key))):  %Equal.sym(V, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key)), S.get(~V, dflt, ST.model(~V, sh), key), gv_of(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key), G.get_ok(~V, sh, hg, dflt, key))) : {_ == x : V}  %Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.model(~V, sh), key), Some{x}, hl) : {S.get_m(~V, dflt, _) == x : V}  {==}# a missing key reads as the default (SPARK's Element has Pre => Contains)def element_default(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String, +hl: {S.lookup(~V, ST.model(~V, sh), key) == None{} : Maybe<&2, V>}) -> S.Element.element_default(~V, ST.model(~V, sh), key, dflt, hl, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key))):  %Equal.sym(V, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key)), S.get(~V, dflt, ST.model(~V, sh), key), gv_of(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key), G.get_ok(~V, sh, hg, dflt, key))) : {_ == dflt : V}  %Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.model(~V, sh), key), None{}, hl) : {S.get_m(~V, dflt, _) == dflt : V}  {==}def hv_of(~V: Data, +sh: ST.Sh<V>, +key: String, -r: H.HashMap<&2, V> & Bool, ok: HA.HasOK(~V, sh, key, r)) -> {Pair.snd(H.HashMap<&2, V>, Bool, r) == S.has(~V, ST.model(~V, sh), key) : Bool}:  match ok:    case Tuple{+sh2, Tuple{+e, rest}}:      %Equal.sym(H.HashMap<&2, V> & Bool, r, (ST.real(~V, sh2), S.has(~V, ST.model(~V, sh), key)), e) : {Pair.snd(H.HashMap<&2, V>, Bool, _) == S.has(~V, ST.model(~V, sh), key) : Bool}      {==}# Contains (Container, Key) = Has_Key (Model, Key)def contains_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> S.Contains.contains_value(~V, ST.model(~V, sh), key, Pair.snd(H.HashMap<&2, V>, Bool, H.has(&2, V, ST.real(~V, sh), key))):  hv_of(~V, sh, key, H.has(&2, V, ST.real(~V, sh), key), HA.has_ok(~V, sh, hg, key))# Length (Container) = Length (Model), and Length = the number of keysdef length_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.Length.length_value(~V, ST.model(~V, sh), U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh))))):  Equal.trans(Nat, U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))), S.size(~V, ST.model(~V, sh)), SC.length(String, S.keys(~V, ST.model(~V, sh))), Pair.snd({H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32}, {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}, SZ.size_ok(~V, sh, hg)), Equal.sym(Nat, SC.length(String, S.keys(~V, ST.model(~V, sh))), S.size(~V, ST.model(~V, sh)), keys_len(~V, ST.model(~V, sh))))# Length does not change the mapdef length_frame(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.Length.length_frame(~V, ST.real(~V, sh), Pair.fst(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))):  Equal.cong(H.HashMap<&2, V> & U32, H.HashMap<&2, V>, p => Pair.fst(H.HashMap<&2, V>, U32, p), H.size(&2, V, ST.real(~V, sh)), (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))), Pair.fst({H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32}, {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}, SZ.size_ok(~V, sh, hg)))# Empty_Map: Length = 0 and no key is presentdef new_model(~V: Data) -> S.Empty_Map.new_model(~V, ST.model(~V, NW.empty(~V))):  Pair.snd({ST.good(~V, NW.empty(~V)) == True{} : Bool}, {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}, Pair.snd({H.new(&2, V) == ST.real(~V, NW.empty(~V)) : H.HashMap<&2, V>}, {ST.good(~V, NW.empty(~V)) == True{} : Bool} & {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}, NW.new_ok(~V)))def new_length(~V: Data) -> S.Empty_Map.new_length(~V, ST.model(~V, NW.empty(~V))):  %Equal.sym(List<&2, S.Entry<V>>, ST.model(~V, NW.empty(~V)), Nil{}, new_model(~V)) : {S.size(~V, _) == 0n : Nat}  {==}def new_absent(~V: Data, +key: String) -> S.Empty_Map.new_absent(~V, ST.model(~V, NW.empty(~V)), key):  %Equal.sym(List<&2, S.Entry<V>>, ST.model(~V, NW.empty(~V)), Nil{}, new_model(~V)) : {S.lookup(~V, _, key) == None{} : Maybe<&2, V>}  {==}# ---- the four contracts on the implementation, re-exported ----def set_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+S.size(~V, ST.model(~V, sh))), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V) -> SetContract(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x)):  sc_from(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x), SO.set_ok(~V, sh, hg, cap, hc30, hcap, key, x))def pop_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PopContract(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key)):  pc_from(~V, sh, hg, key, H.pop(&2, V, ST.real(~V, sh), key), PO.pop_ok(~V, sh, hg, key))def del_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> DelContract(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)):  dc_from(~V, sh, hg, key, H.del(&2, V, ST.real(~V, sh), key), PO.del_ok(~V, sh, hg, key))def keys_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KeysContract(~V, sh, H.keys(&2, V, ST.real(~V, sh))):  kc_from(~V, sh, hg, H.keys(&2, V, ST.real(~V, sh)), KW.keys_ok(~V, sh, hg))