~/bend-docscommunity

proofs/containers/hash_table/keysw.bend checks

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

21 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./strings.bend as STR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./cyc.bend as CY
import ./arr.bend as AX
import ./state.bend as ST
import ./probe_all.bend as PA
import ./grow.bend as GR
import ./insa.bend as IA
import ./arena.bend as AN
import ../../lib/words32.bend as W32

Definitions

def kof source · line 28 · raw

@b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> List<&2, String>

the key of a bucket, as a list

def kb source · line 36 · raw

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

the keys of buckets j .. j + m - 1

def WStep source · line 82 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+q:Nat -> @+kk:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> Type

def acc_eq source · line 85 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+q:Nat -> @+hq:{Nat.is_lt(q, n) == True{} : Bool} -> {kb(bs, Nat.sub(n, q), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kof(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, q)), kb(bs, Nat.sub(n, 1n+q), 1n+q)) : List<&2, String>}

def w_ew source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(kk)) == Nat.double(q) : Nat}

def w_el source · line 96 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(q) : Nat}

def w_get source · line 100 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), U32.shl(kk)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q))) : Pair(Array<U32>, U32)}

def w_getl source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), U32.inc(U32.shl(kk))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 1n+Nat.double(q))) : Pair(Array<U32>, U32)}

def w_at source · line 108 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 1n+Nat.double(q)), kl, c) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def w_accx source · line 111 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), q) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> {kb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), q), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kof(b), kb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 1n+q), 1n+q)) : List<&2, String>}

def nth_upd_same source · line 114 · raw

@+xs:List<&2, String> -> @+i:Nat -> @+v:String -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, xs, i, v), i) == Some{v} : Maybe<&2, String>}

def w_long source · line 124 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q))) == False{} : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

def w_short source · line 149 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q))) == True{} : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

def w_empty source · line 158 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == True{} : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

def w_full source · line 164 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool} -> @+d:Bool -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q))) == d : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

def w_c source · line 171 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(q)), 0) == c : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

def wstep source · line 179 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> WStep(tabT, kl, k, sd, q, kk, KT)

THEOREM: one step of the walk prepends bucket q's key

def WalkOK source · line 183 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+sd:Nat -> @+q:Nat -> @+kk:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> Type

def walk_0 source · line 186 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @st:WStep(tabT, kl, k, sd, 0n, kk, KT) -> WalkOK(tabT, kl, k, sd, 0n, kk, KT)

def walk_s2 source · line 192 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+p:Nat -> @+kk:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.wk_step(kk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, KT), kb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 2n+p), 2n+p)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K2), kb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 1n+p), 1n+p)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Walk} -> @wo:WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT)

def walk_s source · line 198 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+p:Nat -> @+kk:U32 -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @st:WStep(tabT, kl, k, sd, 1n+p, kk, KT) -> @rec:(@+K2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hs2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K2) == kl : List<&2, String>} -> @+pk2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K2) == True{} : Bool} -> WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2)) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT)

def walk source · line 205 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+kl:List<&2, String> -> @+sd:Nat -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+kk:U32 -> @+hkk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(kk) == q : Nat} -> @+KT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, KT) == kl : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, KT) == True{} : Bool} -> WalkOK(tabT, kl, k, sd, q, kk, KT)

THEOREM: the walk over buckets q, q - 1, .., 0 lists every key in bucket order

Templates

template keys_app source · line 45 · raw

@-V:Data -> @+a:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> @+b:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, b)) : List<&2, String>}

template ek_m source · line 52 · raw

@-V:Data -> @+k:String -> @+m:Maybe<&2, V> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.ent_m(V, k, m)) == [k] : List<&2, String>}

template ent_keys source · line 59 · raw

@-V:Data -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+vsl:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, vsl), fr, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.ent(V, b, vsl)) == kof(b) : List<&2, String>}

template keys_absm source · line 69 · raw

@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+vsl:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+n:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, vsl), fr}, n) == True{} : Bool} -> @+m:Nat -> @+j:Nat -> @+hjm:{Nat.is_le(Nat.add(j, m), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, bs, vsl, m, j)) == kb(bs, m, j) : List<&2, String>}

THEOREM: the model's keys are the buckets' keys in bucket order

template KeysOK source · line 216 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V>, List<&2, String>) -> Type

template keys_w source · line 220 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool} -> @wo:WalkOK(tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), k, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), ksT) -> @+ew:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.wk_go(U32.to_nat(U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.wk_go(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.WK{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), kb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k)))}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Walk} -> KeysOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})))

template keys_ok source · line 236 · raw

@-V:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.good(V, sh) == True{} : Bool} -> KeysOK(V, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.real(V, sh)))

THEOREM: keys lists the model's keys in order and keeps the map and its model