import Base import ../../../spec/containers/hash_table.bend as S import ../../../spec/lib/common.bend as SC import ../../../src/containers/hash_table.bend as H import ./state.bend as ST import ./new.bend as NW import ./get.bend as G import ./has.bend as HA import ./size.bend as SZ import ./set.bend as ST2 import ./setok.bend as SO import ./pop.bend as PO import ./keysw.bend as KW import ./keys.bend as K import ./speclem.bend as SL import ../../lib/logic.bend as L import ../../lib/array.bend as AR import ./poplem.bend as PL import ./table.bend as TB import ../../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>}): NW.new_ok(~V) def get_ok(~V: Data, +sh: ST.Sh, +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, +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, +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, +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, +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, +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, +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 string def 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 them def 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>, +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 it def mem_has(~V: Data, +m: List<&2, S.Entry>, +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 map def keys_len(~V: Data, +m: List<&2, S.Entry>) -> {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 None def 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>, +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 absent def size_set(~V: Data, +m: List<&2, S.Entry>, +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>, +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>, 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 present def size_remove(~V: Data, +m: List<&2, S.Entry>, +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>, +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>, +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, +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, +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 nothing def KeysContract(~V: Data, +sh: ST.Sh, r: H.HashMap<&2, V> & List<&2, String>) -> Type: Sigma<&1, &1, ST.Sh, 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>}) & S.KeysPost(~V, ST.model(~V, sh)))> def kc_from(~V: Data, +sh: ST.Sh, +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, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type: Sigma<&1, &1, ST.Sh, 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>, +m2: List<&2, S.Entry>, +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>, +m2: List<&2, S.Entry>, +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>, +m2: List<&2, S.Entry>, +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>, ~m2: List<&2, S.Entry>, ~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, +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, +key: String, r: H.HashMap<&2, V> & Maybe<&2, V>) -> Type: Sigma<&1, &1, ST.Sh, 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, +key: String, r: H.HashMap<&2, V>) -> Type: Sigma<&1, &1, ST.Sh, 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>, +m2: List<&2, S.Entry>, +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>, 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>, +m2: List<&2, S.Entry>, +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>, +m2: List<&2, S.Entry>, +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>, ~m2: List<&2, S.Entry>, ~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, +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, +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, +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 present def element_value(~V: Data, +sh: ST.Sh, +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, +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, +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, +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 keys def length_value(~V: Data, +sh: ST.Sh, +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 map def length_frame(~V: Data, +sh: ST.Sh, +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 present def 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>}, 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>}, 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>, 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>, 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, +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, +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, +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, +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))