~/bend-docscommunity

proofs/containers/hash_table/insgrow.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insgrow.bend as Insgrow

28 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 ./speclem.bend as SL
import ./probe_all.bend as PA
import ./insm.bend as IM
import ./insu.bend as IU
import ./insert.bend as IS
import ./words.bend as WR
import ./rawins.bend as RI
import ./rehash.bend as RH
import ./grow.bend as GR
import ../../lib/nat_list.bend as NL
import ../../lib/words32.bend as W32

Definitions

def plt_c source · line 58 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(b)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {c == True{} : Bool}

def pow2_lt_inv source · line 65 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def lng_c source · line 70 · raw

@+c:Cmp -> @+h:{Cmp.is_le(c) == True{} : Bool} -> {Cmp.is_gt(c) == False{} : Bool}

def le_not_gt source · line 79 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_gt(a, b) == False{} : Bool}

def fl_from source · line 83 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+nxl:List<&2, U32> -> @+cnt:Nat -> @+f:U32 -> @+fr:Nat -> @+seen:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(obs, j, nxl, cnt, f, fr, seen) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(nbs, n2, nxl, cnt, f, fr, seen) == True{} : Bool}

Templates

template sle_c source · line 37 · raw

@-V:Data -> @+m1:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+q:String -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m1, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) : Maybe<&2, V>} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(key, q) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m1, key, x), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m2, key, x), q) : Maybe<&2, V>}

template ssz_c source · line 44 · raw

@-V:Data -> @+m1:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m2) : Nat} -> @+mv:Maybe<&2, V> -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m1, key) == mv : Maybe<&2, V>} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, key) == mv : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m1, key, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.set(V, m2, key, x)) : Nat}

template setm_tr source · line 53 · raw

@-V:Data -> @+m1:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+m2:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+key:String -> @+x:V -> @heq:(@+q:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m1, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, q) : Maybe<&2, V>}) -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m1, key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, m2, key) : Maybe<&2, V>} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.size(V, m2) : Nat} -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @sm:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, m1, key, x, r) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.SetM(V, m2, key, x, r)

THEOREM: an update refining set on one model refines it on any model with the same lookups and size

template k30 source · line 101 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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} -> @+hovi:{U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == True{} : Bool} -> {Nat.is_lt(1n+k, 31n) == True{} : Bool}

with 2(n + 1) <= 2^cap and cap <= 30, growth stays below 2^31 buckets

template ig_2 source · line 107 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hovi:{U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+eg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.grow_tab(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT) : Array<U32>} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/grow.rinv(tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), k, sd, NT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @fe:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/rawins.FirstE(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+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(1n+k)))) -> 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, ksT), 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_slot(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fr, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), s, U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

template ig_1 source · line 137 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hovi:{U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @gg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/grow.GrowOK(tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), k, sd, td) -> 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, ksT), 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_slot(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fr, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), s, U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

template ins_grow source · line 147 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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} -> @+hovi:{U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == True{} : 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, ksT), 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_slot(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fr, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), s, U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

THEOREM: placing a new entry into a table that must grow refines set

template ia_c source · line 155 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hcl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(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/containers/hash_table/cyc.msk(k)) == True{} : Bool} -> @+hsdk2:{Bool.or(Nat.is_lt(sd, k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))) == True{} : Bool} -> @+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, ksT), 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, 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))), 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} -> @+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} -> @+c:Bool -> @+hc:{U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == 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, ksT), 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_slot(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fr, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), s, U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

template ins_any source · line 165 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fr: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> -> @+s:U32 -> @+e:Nat -> @+key:String -> @+x:V -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hsdk1:{Nat.is_le(sd, k) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, ksT) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, sd, nxT) == True{} : Bool} -> @+htd:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td), 1n+k) == True{} : Bool} -> @+hsz:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+hsdu:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sdU), sd) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{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)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{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)) == True{} : Bool} -> @+hcn:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(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))) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{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/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, vsT)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(sz)) == True{} : Bool} -> @+hnf:{Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(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/array.slots(U32, nxT), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), [0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s)]) == True{} : Bool} -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(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/proofs/lib/u32div.v(s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == 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, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), key}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hcl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(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/containers/hash_table/cyc.msk(k)) == True{} : Bool} -> @+hsdk2:{Bool.or(Nat.is_lt(sd, k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))) == True{} : Bool} -> @+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, ksT), 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, 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))), 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} -> @+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} -> 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, ksT), 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_slot(&2, V, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, fr, sz, sdU, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, vsT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nxT), s, U32.from_nat(e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))))

THEOREM: placing a new entry, whether or not the table grows, refines set