~/bend-docscommunity

proofs/containers/hash_table/rawins.bend checks

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

19 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 ../../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 ./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 ./probe_impl.bend as PI
import ./probe_all.bend as PA
import ./keys.bend as K2
import ../../lib/words32.bend as W32

Definitions

def ri source · line 26 · raw

@+tb:List<&2, U32> -> @+n:Nat -> @f:Nat -> @+i:Nat -> Maybe<&2, Nat>

the walk: the first empty bucket within f steps of i

def rput source · line 33 · raw

@tab:Array<U32> -> @m:Maybe<&2, Nat> -> @+w:U32 -> @+l:U32 -> Array<U32>

def go0 source · line 42 · raw

@+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+mask:U32 -> @+i:U32 -> @+w:U32 -> @+l:U32 -> @+c:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_go(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rs_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), c), mask, i, w, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T) : Array<U32>}

def rstep_eq source · line 49 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+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} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rs_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i))), 0)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.RStep}

def go_c source · line 56 · raw

@+K:Nat -> @+T:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+p:Nat -> @+i:U32 -> @+hk:{Nat.is_le(K, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+hnext:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))) == Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) : Nat} -> @+rec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_go(p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)), w, l) == rput(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), ri(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K), p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K)))), w, l) : Array<U32>} -> @+c:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_go(1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rs_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), i, w, l) == rput(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), Bool.pick(Maybe<&2, Nat>, c, Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)}, ri(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K), p, Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)))), w, l) : Array<U32>}

def raw_impl source · line 64 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+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} -> @+f:Nat -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_go(f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.rstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), i, w, l) == rput(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), ri(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K), f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), w, l) : Array<U32>}

THEOREM: the implementation's insertion loop places the pair where the walk ends

def occ_dec source · line 82 · raw

@+w:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+c:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, c)) == Bool.not(c) : Bool}

def occ_flag source · line 89 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j)) == Bool.not(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, Nat.double(j)), 0)) : Bool}

def rp_t source · line 92 · raw

@+t:Nat -> @+d:Nat -> @+ht:{Nat.is_le(t, d) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(t, d) == c : Bool} -> @+no:{c == False{} : Bool} -> {t == d : Nat}

def rp_true source · line 95 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+bp:Nat -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, 1n+bp), 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(tb, kl, 1n+bp), 1n+bp, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+t:Nat -> @+ht:{Nat.is_le(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t))), 0) == True{} : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == c2 : Bool} -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)} == Some{e} : Maybe<&2, Nat>}

def rp_false source · line 105 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+bp:Nat -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, 1n+bp), 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(tb, kl, 1n+bp), 1n+bp, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+t:Nat -> @+ht:{Nat.is_le(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t))), 0) == False{} : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_eq(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == c2 : Bool} -> {Nat.is_le(1n+t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool}

def rp_c source · line 115 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+bp:Nat -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, 1n+bp), 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(tb, kl, 1n+bp), 1n+bp, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+p:Nat -> @+t:Nat -> @+ht:{Nat.is_le(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t))), 0) == c : Bool} -> @rec:(@ht2:{Nat.is_le(1n+t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> {ri(tb, 1n+bp, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, 1n+t)) == Some{e} : Maybe<&2, Nat>}) -> {Bool.pick(Maybe<&2, Nat>, c, Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)}, ri(tb, 1n+bp, p, Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t), 1n+bp))) == Some{e} : Maybe<&2, Nat>}

def ri_path source · line 122 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+bp:Nat -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, 1n+bp), 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(tb, kl, 1n+bp), 1n+bp, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+f:Nat -> @+t:Nat -> @+ht:{Nat.is_le(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(1n+bp, h, e)) == True{} : Bool} -> @+hft:{Nat.add(t, f) == 1n+bp : Nat} -> {ri(tb, 1n+bp, f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)) == Some{e} : Maybe<&2, Nat>}

def ri_n source · line 131 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+h:Nat -> @+hh:{Nat.is_lt(h, n) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, n) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), 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(tb, kl, n), n, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.dist(n, h, e)) == True{} : Bool} -> {ri(tb, n, n, h) == Some{e} : Maybe<&2, Nat>}

def raw_ok source · line 140 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+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} -> @+kl:List<&2, String> -> @+w:U32 -> @+l:U32 -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, T), kl, 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, T), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(K), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bucket(w, 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(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K))), e)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.ins_raw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(K), w, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.put_bucket(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, T), U32.from_nat(e), w, l) : Array<U32>}

THEOREM: ins_raw writes the pair into the first empty bucket of its path

def pno_home source · line 149 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+n:Nat -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, n) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PHome{bs, mask, key, h}, m) == True{} : Bool}

def FirstE source · line 158 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> Type

def fe_r source · line 161 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+h:Nat -> @+key:String -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, n) == True{} : Bool} -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @ok:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.ResOK(bs, n, h, key, r) -> FirstE(bs, n, h)

def fe_0 source · line 173 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, n) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(bs, n, mask) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, n) == True{} : Bool} -> @e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.Empty0(bs, n) -> FirstE(bs, n, h)

def find_e source · line 180 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, n) == True{} : Bool} -> @+cl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.cluster(bs, n, mask) == True{} : Bool} -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, n) == True{} : Bool} -> @+hem:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.occn(bs, n), n) == True{} : Bool} -> FirstE(bs, n, h)

THEOREM: in a table with a free bucket, a key held nowhere has an empty bucket on its path, every bucket before it on the path full