proofs/containers/hash_table/setok.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setok.bend as Setok
24 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC import ../../../spec/containers/hash_table.bend as S import ../../lib/u32div.bend as UD import ../../../src/math/hash.bend as HS import ../../../src/containers/hash_table.bend as H import ./keys.bend as K import ./table.bend as TB import ./buckets.bend as B import ./modn.bend as M import ./cyc.bend as CY import ./inv.bend as IV import ./state.bend as ST import ./size.bend as SZ import ./probe_impl.bend as PI import ./probe_all.bend as PA import ./get.bend as G import ./lookup.bend as LK import ./set.bend as ST2 import ./insert.bend as IS import ./setins.bend as SI
Templates
template hg2 source · line 33 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2), vsT, nxT) == True{} : Bool}the invariant for the probe's copy of the key tree
template keep_miss source · line 39 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+sh2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.has(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh2)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})) : List<&2, String>}a new key: it was absent, so the key-preservation clause holds vacuously
template to_sh2 source · line 43 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @sm:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x, r) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, r)
template to_sh source · line 48 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @sm:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key, x, r) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, r)
template miss_room source · line 52 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), e)) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hf:{U32.is_eq(free, 0) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_lt(fresh, sz) == c : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_new(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, True{}))
template miss_c source · line 59 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), e)) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(free, 0) == c : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0n), key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_new(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, c))
template set_miss source · line 67 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occpath(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), e)) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_new(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_eq(free, 0)))a new key: one of the three ways of choosing its slot
template set_hitb source · line 71 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+i:Nat -> @+l:U32 -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)) == l : U32} -> @bf:Pair({Bool.not(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)), 0)) == True{} : Bool}, Pair({Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), i))))) == True{} : Bool})) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set_hit(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), U32.from_nat(i), l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_eq(l, 0)))
template set_r source · line 80 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT) : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @hres:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), key, r) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set_f(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fresh, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_impl.fd_of(r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key))))
template set_po source · line 93 · raw
@-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:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.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+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @hres:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), key, r) -> @po:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.ProbeOK(tabT, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.probe(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), key)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key, x))
template set_ok source · line 101 · raw
@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> @+cap:Nat -> @+hc30:{Nat.is_le(cap, 30n) == True{} : Bool} -> @+hcap:{Nat.is_le(Nat.double(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.model(V, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cap)) == True{} : Bool} -> @+key:String -> @+x:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.SetOK(V, sh, key, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.set(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh), key, x))THEOREM: set refines the specification's set