proofs/containers/hash_table/grow.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/grow.bend as Grow
26 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/u32.bend as U import ../../lib/u32alg.bend as A import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC import ../../lib/word.bend as WD 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 ./arr.bend as AX import ./inv.bend as IV import ./state.bend as ST import ./probe_all.bend as PA import ./insm.bend as IM import ./insa.bend as IA import ./rawins.bend as RI import ./rehash.bend as RH import ./insert.bend as IS import ../../lib/words32.bend as W32
Definitions
def mskv source · line 33 · raw
@+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> {Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)), 1n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k) : Nat}
def msk_up source · line 38 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{Nat.is_lt(k, 31n) == True{} : Bool} -> {U32.inc(U32.shl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k) : U32}THEOREM: the grown mask is the mask of twice the buckets
def p_ev source · line 53 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(e)) == e : Nat}
def p_h source · line 56 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(e))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+K)) == True{} : Bool}
def p_i1 source · line 59 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))) == Nat.double(e) : Nat}
def p_i2 source · line 62 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))) == 1n+Nat.double(e) : Nat}
def p_h1 source · line 65 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+K)) == True{} : Bool}
def p_h2 source · line 68 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+K)) == True{} : Bool}
def put_perf source · line 71 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == True{} : Bool}
def put_eq source · line 75 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.put_bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), U32.from_nat(e), w, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) : Array<U32>}THEOREM: writing bucket e is the tree update at 2e and 2e + 1
def put_slots source · line 82 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l) : List<&2, U32>}
def put_bs source · line 93 · raw
@+K:Nat -> @+hK:{Nat.is_lt(K, 31n) == True{} : Bool} -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+K, T) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+n:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), n) == True{} : Bool} -> @+hw0:{U32.is_eq(w, 0) == False{} : Bool} -> @+hkl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+K, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), kl, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, n), e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))}) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}THEOREM: the written tree decodes to the buckets with bucket e filled, the key read from the unchanged arena
def nth0_rep source · line 101 · raw
@+m:Nat -> @+x:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0), x) == 0 : U32}
def nth0_z source · line 111 · raw
@+d:Nat -> @+x:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), x) == 0 : U32}
def at_z source · line 114 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+i:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}
def z_clus source · line 117 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+mask:U32 -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PClus{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n), n, mask}, m) == True{} : Bool}
def z_well source · line 125 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+sd:Nat -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n), sd}, m) == True{} : Bool}
def z_uniq source · line 133 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n)}, m) == True{} : Bool}
def z_from source · line 141 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+src:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n), src, j}, m) == True{} : Bool}
def z_occn source · line 149 · raw
@+d:Nat -> @+kl:List<&2, String> -> @+n:Nat -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, d, 0)), kl, n), m) == 0n : Nat}
def rinv source · line 159 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> Bool
the rehash loop invariant after moving old buckets 0 .. j - 1
def r_1 source · line 162 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 2n+k, NT) == True{} : Bool}
def r_2 source · line 165 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k)) == True{} : Bool}
def r_3 source · line 168 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {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, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool}
def r_4 source · line 171 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {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, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool}
def r_5 source · line 174 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j)) == True{} : Bool}
def r_6 source · line 177 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool}
def r_7 source · line 180 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)}, j) == True{} : Bool}
def r_mk source · line 183 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:Nat -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 2n+k, NT) == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k)) == True{} : Bool} -> @+h3:{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, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool} -> @+h4:{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, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool} -> @+h5:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j)) == True{} : Bool} -> @+h6:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool} -> @+h7:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)}, j) == True{} : Bool} -> {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}
def StepOK source · line 189 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+j:Nat -> @+kk:U32 -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Type
def s_hh source · line 192 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool}
def s_ew source · line 195 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(kk)) == Nat.double(j) : Nat}
def s_el source · line 198 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(j) : Nat}
def eqA source · line 201 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_step(kk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_if(kk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Mv}
def eqB source · line 206 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_if(kk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), False{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_raw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), 1n+Nat.double(j)))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Mv}
def s_occ source · line 211 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j)) == Bool.not(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0)) : Bool}
def step_skip source · line 215 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0) == True{} : Bool} -> StepOK(OT, kl, k, sd, j, kk, NT)an empty old bucket: nothing moves
def s_hb source · line 222 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), 1n+Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), 1n+Nat.double(j))))))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}
def step_e source · line 225 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool} -> @+pno:{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, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), 1n+Nat.double(j))))))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool} -> @+nsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, NT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), 1n+Nat.double(j)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+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), kl, 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/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k)))) -> StepOK(OT, kl, k, sd, j, kk, NT)
def step_mv source · line 247 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool} -> StepOK(OT, kl, k, sd, j, kk, NT)a full old bucket: it moves to the first empty bucket of its path
def step_c source · line 258 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), Nat.double(j)), 0) == c : Bool} -> StepOK(OT, kl, k, sd, j, kk, NT)
def step source · line 266 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hoc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> StepOK(OT, kl, k, sd, j, kk, NT)THEOREM: one step of the move loop keeps the loop invariant
def occn_le source · line 271 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+d:Nat -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(bs, j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(bs, Nat.add(j, d))) == True{} : Bool}
def LoopOK source · line 281 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+f:Nat -> @+kk:U32 -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> Type
def loop_s2 source · line 284 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+p:Nat -> @+kk:U32 -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+T2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_step(kk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, NT)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T2)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Mv} -> @lo:LoopOK(OT, kl, k, sd, p, U32.inc(kk), T2) -> LoopOK(OT, kl, k, sd, 1n+p, kk, NT)
def loop_s source · line 289 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+p:Nat -> @+j:Nat -> @+kk:U32 -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @st:StepOK(OT, kl, k, sd, j, kk, NT) -> @rec:(@+T2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr2:{rinv(OT, kl, k, sd, T2, 1n+j) == True{} : Bool} -> LoopOK(OT, kl, k, sd, p, U32.inc(kk), T2)) -> LoopOK(OT, kl, k, sd, 1n+p, kk, NT)
def loop source · line 295 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+f:Nat -> @+j:Nat -> @+hjf:{Nat.add(j, f) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k) : Nat} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == j : Nat} -> @+NT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hr:{rinv(OT, kl, k, sd, NT, j) == True{} : Bool} -> LoopOK(OT, kl, k, sd, f, kk, NT)THEOREM: the loop moves the remaining old buckets keeping the invariant
def GrowOK source · line 310 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+td:U32 -> Type
def grow_fin source · line 313 · raw
@+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+td:U32 -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.grow_tab(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), td, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_fin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.mv_go(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(1n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, OT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, 2n+k, 0))})) : Array<U32>} -> @lo:LoopOK(OT, kl, k, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(U32, 2n+k, 0)) -> GrowOK(OT, kl, k, sd, td)
def grow_ok source · line 320 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk30:{Nat.is_lt(1n+k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+OT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pot:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, OT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+huo:{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, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hld:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, OT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+td:U32 -> @+htd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(td) == 1n+k : Nat} -> GrowOK(OT, kl, k, sd, td)THEOREM: growing the table yields a table of twice the buckets holding a copy of every full old bucket and nothing else, with the table invariants