~/bend-docscommunity

proofs/containers/hash_table/setok.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/math/hash.bend as HSimport ../../../src/containers/hash_table.bend as Himport ./keys.bend as Kimport ./table.bend as TBimport ./buckets.bend as Bimport ./modn.bend as Mimport ./cyc.bend as CYimport ./inv.bend as IVimport ./state.bend as STimport ./size.bend as SZimport ./probe_impl.bend as PIimport ./probe_all.bend as PAimport ./get.bend as Gimport ./lookup.bend as LKimport ./set.bend as ST2import ./insert.bend as ISimport ./setins.bend as SI# THEOREM set_ok: for any key and value, the implementation's set is the# specification's set: every lookup and the size agree, and the invariant is# kept. (Precondition: after the insertion the map has at most 2^cap - 1# entries, cap <= 30, so the table stays below 2^31 buckets.)# the invariant for the probe's copy of the key treedef hg2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}) -> {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, K2), AR.perfect(String, sd, K2), vsT, nxT) == True{} : Bool}:  +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +hgT = L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), b, vsT, nxT) == True{} : Bool}, AR.perfect(String, sd, ksT), True{}, pkT, hg)  L.subst(List<&2, String>, z => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, z, AR.perfect(String, sd, K2), vsT, nxT) == True{} : Bool} , AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl2), L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), b, vsT, nxT) == True{} : Bool}, True{}, AR.perfect(String, sd, K2), Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2), hgT))# a new key: it was absent, so the key-preservation clause holds vacuouslydef keep_miss(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +sh2: ST.Sh<V>, +hp: {S.has(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key) == True{} : Bool}) -> {S.keys(~V, ST.model(~V, sh2)) == S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})) : List<&2, String>}:  +ln = L.subst(List<&2, String>, z => {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key) == None{} : Maybe<&2, V>}, AR.slots(String, K2), AR.slots(String, ksT), hsl2, LK.lookup_none(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), hno))  Empty.absurd({S.keys(~V, ST.model(~V, sh2)) == S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})) : List<&2, String>}, L.false_true(L.subst(Maybe<&2, V>, z => {S.is_some(~V, z) == True{} : Bool}, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), None{}, ln, hp)))def to_sh2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, -r: H.HashMap<&2, V>, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, sm: IS.SetM(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x, r)) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, r):  match sm:    case Tuple{+sh2, Tuple{+e, rest}}:      (sh2, (e, (rest, hp => keep_miss(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, hno, sh2, hp))))def to_sh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, -r: H.HashMap<&2, V>, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, sm: IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x, r)) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, r):  to_sh2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, r, hno, L.subst(List<&2, String>, z => IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x, r), AR.slots(String, K2), AR.slots(String, ksT), hsl2, sm))def miss_room(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +c: Bool, +hc: {U32.is_lt(fresh, sz) == c : Bool}) -> IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{})):  match c:    case True{}:      SI.set_room(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT, hg2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2), key, x, e, he, hz, hp, hno, hf, hc, cap, hc30, hcap)    case False{}:      SI.set_arena(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT, hg2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2), key, x, e, he, hz, hp, hno, hf, hc, cap, hc30, hcap)def miss_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(free, 0) == c : Bool}) -> IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, c)):  match c:    case False{}:      SI.set_free(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT, hg2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2), key, x, e, he, hz, hp, hno, hc, cap, hc30, hcap)    case True{}:      miss_room(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, e, he, hz, hp, hno, hc, U32.is_lt(fresh, sz), {==})# a new key: one of the three ways of choosing its slotdef set_miss(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_eq(free, 0))):  to_sh(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_eq(free, 0)), hno, miss_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, e, he, hz, hp, hno, U32.is_eq(free, 0), {==}))def set_hitb(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, bf: {Bool.not(U32.is_eq(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i))))) == True{} : Bool})) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, H.set_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), PA.stored(key), x, U32.is_eq(l, 0))):  match bf:    case Tuple{nz, Tuple{hr0, hlv0}}:      +nz2 = L.subst(U32, zz => {Bool.not(U32.is_eq(zz, 0)) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, nz)      +hr = L.subst(U32, zz => {Nat.is_lt(UD.v(H.slot(zz)), SC.pow2(sd)) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, hr0)      +hlv = L.subst(U32, zz => {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(zz))) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, hlv0)      +e0 = Equal.cong(Bool, H.HashMap<&2, V>, b => H.set_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), PA.stored(key), x, b), U32.is_eq(l, 0), False{}, K.not_true_eq(U32.is_eq(l, 0), nz2))      L.subst(H.HashMap<&2, V>, rr => ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, rr), H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), Some{x}), AR.thaw(U32, nxT)}, H.set_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), PA.stored(key), x, U32.is_eq(l, 0)), Equal.sym(H.HashMap<&2, V>, H.set_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), PA.stored(key), x, U32.is_eq(l, 0)), H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), Some{x}), AR.thaw(U32, nxT)}, e0), ST2.set_hit_case(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, K2, hsl2, pk2, i, l, hi, hk, hl, hr, hlv))def set_r(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r)) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, H.set_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), x, (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)))):  match r:    case B.RHit{+i, +l}:      (+hi, rest) = hres      (+hk, hl) = rest      set_hitb(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, i, l, hi, hk, hl, G.bf_ok(sd, ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi), B.all_inst(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, 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), i, hi), hk))    case B.REnd{+e}:      (he, rest) = hres      (hz, rest2) = rest      (hp, hno) = rest2      set_miss(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, e, he, L.subst(List<&2, String>, z => {B.at(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), e) == B.BE{} : B.Bk} , AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl2), hz), L.subst(List<&2, String>, z => {B.occpath(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool} , AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl2), hp), L.subst(List<&2, String>, z => {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool} , AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl2), hno))def set_po(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r), po: PA.ProbeOK(tabT, sd, AR.slots(String, ksT), PA.stored(key), K.kword(key), r, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))) -> ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, H.set(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x)):  match po:    case Tuple{+K2, Tuple{+e, rest}}:      (+hsl2, pk2) = rest      +eq = Equal.cong(H.Found & U32, H.HashMap<&2, V>, pr => H.set_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), x, pr), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)), e)      L.subst(H.HashMap<&2, V>, rr => ST2.SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, rr), H.set_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), x, (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), H.set(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x), Equal.sym(H.HashMap<&2, V>, H.set(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x), H.set_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), x, (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), eq), set_r(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap, key, x, K2, hsl2, pk2, r, hres))# THEOREM: set refines the specification's setdef 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)):  match sh:    case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:      +kl = AR.slots(String, ksT)      +pk = AR.perfect(String, sd, ksT)      +hk31 = L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))      +esz = Equal.trans(Nat, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), UD.v(n), SZ.size_absm(~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), SC.pow2(k), N.le_refl(SC.pow2(k))), Equal.sym(Nat, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))))      +hcap2 = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+z), SC.pow2(cap)) == True{} : Bool}, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)), UD.v(n), esz, hcap)      set_po(~V, 1n, {==}, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, cap, hc30, hcap2, key, x, B.pf(key, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k)))), G.res_of(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg, key), PA.probe_ok(1n, {==}, k, hk31, tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), sd, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), kl, ksT, {==}, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), key))