~/bend-docscommunity

proofs/containers/hash_table/rehash.bend checks

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

17 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./keys.bend as K
import ./words.bend as WR
import ./buckets.bend as B
import ./state.bend as ST
import ./lookup.bend as LK
import ./tools.bend as T
import ./insm.bend as IM
import ./tools.bend as TL
import ../../lib/u32.bend as UW

Definitions

def bk_refl source · line 23 · raw

@+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bk_eq(b, b) == True{} : Bool}

def bk_eq_of source · line 30 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bk_eq(a, b) == True{} : Bool} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def ai_c source · line 45 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+q:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+q) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bk_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j), b) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(j, q) == c : Bool} -> @rec:(@hlt:{Nat.is_lt(j, q) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, q, b) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, 1n+q, b) == True{} : Bool}

def anyeq_intro source · line 54 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+j:Nat -> @+hj:{Nat.is_lt(j, m) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bk_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j), b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, m, b) == True{} : Bool}

a bucket equal to b below m: some bucket below m equals b

def anyeq_up source · line 61 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, m, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, 1n+m, b) == True{} : Bool}

def EqAt source · line 64 · raw

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

def eqat_up source · line 67 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+q:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @e:EqAt(bs, q, b) -> EqAt(bs, 1n+q, b)

def fe_c source · line 72 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+q:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bk_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, q), b) == c : Bool} -> @+h:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, q, b)) == True{} : Bool} -> @rec:(@hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, q, b) == True{} : Bool} -> EqAt(bs, q, b)) -> EqAt(bs, 1n+q, b)

def find_eq source · line 80 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, m, b) == True{} : Bool} -> EqAt(bs, m, b)

THEOREM: some bucket below m equals b: one is found

def from_at source · line 90 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n2) == True{} : Bool} -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)) == True{} : Bool} -> EqAt(obs, j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i))

def pf_at source · line 93 · raw

@+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+key:String -> @+j:Nat -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nohb(obs, key, j) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @e:EqAt(obs, j, b) -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, b)) == True{} : Bool}

def pno_c source · line 98 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+key:String -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nohb(obs, key, j) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n2) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)) == c : Bool} -> {Bool.not(c) == True{} : Bool}

def pno_from source · line 107 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+key:String -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nohb(obs, key, j) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{nbs, key}, m) == True{} : Bool}

THEOREM: a key held by no moved bucket is held by no copy

def ns_at source · line 115 · raw

@+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+t:Nat -> @+j:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(obs, t, j) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @e:EqAt(obs, j, b) -> {Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b))), t))) == True{} : Bool}

def ns_c source · line 120 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+t:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(obs, t, j) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n2) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)) == c : Bool} -> {Bool.not(Bool.and(c, Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)))), t))) == True{} : Bool}

def ns_from source · line 128 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+t:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(obs, t, j) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(nbs, t, m) == True{} : Bool}

THEOREM: a slot used by no moved bucket is used by no copy

def lv_at source · line 137 · raw

@+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+lv:List<&2, Bool> -> @+fr:Nat -> @+j:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{obs, lv, fr}, j) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @e:EqAt(obs, j, b) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(lv, fr, b) == True{} : Bool}

def live_empty source · line 142 · raw

@+lv:List<&2, Bool> -> @+fr:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(lv, fr, b) == True{} : Bool}

def lvf_c source · line 149 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+lv:List<&2, Bool> -> @+fr:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{obs, lv, fr}, j) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n2) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(lv, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, i)) == True{} : Bool}

def live_from source · line 157 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+lv:List<&2, Bool> -> @+fr:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{obs, lv, fr}, j) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{nbs, lv, fr}, m) == True{} : Bool}

THEOREM: copies of live buckets are live

def nsl_bit source · line 167 · raw

@+o:Bool -> @+a:U32 -> @+l:U32 -> @+h:{Bool.not(Bool.and(o, U32.is_eq(a, l))) == True{} : Bool} -> {Bool.not(Bool.and(o, Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(a)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))) == True{} : Bool}

def noslot_nolb source · line 175 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+l:U32 -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nolb(bs, l, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), m) == True{} : Bool}

THEOREM: no bucket below m has link l: none uses slot(l)

def imp_true source · line 185 · raw

@+a:Bool -> @+x:Bool -> @+h:{x == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(a, x) == True{} : Bool}

def imp_up source · line 192 · raw

@+a:Bool -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, m, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(bs, 1n+m, b)) == True{} : Bool}

def from_skip source · line 200 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, 1n+j}, m) == True{} : Bool}

copies stay copies of the longer prefix

def from_mv_i source · line 209 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, nbs)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, j) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n2) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(e, i) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.eval(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), obs, 1n+j}, i) == True{} : Bool}

def from_mv source · line 219 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, nbs)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, j) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, j}, n2) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), obs, 1n+j}, m) == True{} : Bool}

THEOREM: after moving old bucket j into e, every full new bucket is a copy

def ne_occ source · line 227 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+i:Nat -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(e, i) == c : Bool} -> {c == False{} : Bool}

def to_w source · line 235 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+n2:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hox:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == True{} : Bool} -> @w0:EqAt(nbs, n2, x) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), n2, x) == True{} : Bool}

def to_i source · line 243 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+n2:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(nbs, n2, x)) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(x) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.anyeq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), n2, x)) == True{} : Bool}

def to_old source · line 250 · raw

@+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+n2:Nat -> @+j:Nat -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, j) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), n2}, m) == True{} : Bool}

def to_mv source · line 260 · raw

@+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, nbs)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, j) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(nbs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hen:{Nat.is_lt(e, n2) == True{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(nbs, e, b), n2}, 1n+j) == True{} : Bool}

THEOREM: after moving old bucket j into e, every moved old bucket has a copy

def to_skip source · line 265 · raw

@+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+j:Nat -> @+n2:Nat -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, j)) == False{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, 1n+j) == True{} : Bool}

THEOREM: skipping an empty old bucket keeps every moved one copied

Templates

template lkc_held source · line 270 · raw

@-V:Data -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+no:Nat -> @+n2:Nat -> @+huqn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{nbs}, n2) == True{} : Bool} -> @+huqo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{obs}, no) == True{} : Bool} -> @+vsl:List<&2, Maybe<&2, V>> -> @+q:String -> @+i:Nat -> @+hi:{Nat.is_lt(i, no) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, i)) == True{} : Bool} -> @w0:EqAt(nbs, n2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(obs, i)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, nbs, vsl, n2, 0n), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, obs, vsl, no, 0n), q) : Maybe<&2, V>}

template lkc_h source · line 277 · raw

@-V:Data -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+no:Nat -> @+n2:Nat -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, no) == True{} : Bool} -> @+huqn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{nbs}, n2) == True{} : Bool} -> @+huqo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{obs}, no) == True{} : Bool} -> @+vsl:List<&2, Maybe<&2, V>> -> @+q:String -> @e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/tools.Holder(obs, q, no) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, nbs, vsl, n2, 0n), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, obs, vsl, no, 0n), q) : Maybe<&2, V>}

template lkc_c source · line 283 · raw

@-V:Data -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+no:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, no}, n2) == True{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, no) == True{} : Bool} -> @+huqn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{nbs}, n2) == True{} : Bool} -> @+huqo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{obs}, no) == True{} : Bool} -> @+vsl:List<&2, Maybe<&2, V>> -> @+q:String -> @+d:Bool -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{obs, q}, no) == d : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, nbs, vsl, n2, 0n), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, obs, vsl, no, 0n), q) : Maybe<&2, V>}

template lookup_copy source · line 293 · raw

@-V:Data -> @+nbs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+obs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+no:Nat -> @+n2:Nat -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PFrom{nbs, obs, no}, n2) == True{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PTo{obs, nbs, n2}, no) == True{} : Bool} -> @+huqn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{nbs}, n2) == True{} : Bool} -> @+huqo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{obs}, no) == True{} : Bool} -> @+vsl:List<&2, Maybe<&2, V>> -> @+q:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, nbs, vsl, n2, 0n), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.lookup(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, obs, vsl, no, 0n), q) : Maybe<&2, V>}

THEOREM: a table of copies of all the old full buckets looks every key up as the old table does