~/bend-docscommunity

proofs/containers/hash_table/arr.bend checks

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

10 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 ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ./table.bend as TB
import ../../lib/words32.bend as W32

Definitions

def ix_w source · line 19 · raw

@+i:U32 -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(i)) == Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)) : Nat}

the word index 2i and the link index 2i + 1 of bucket i

def ix_l1 source · line 22 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+i:U32 -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))) == 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)) : Nat}

def ix_l source · line 27 · raw

@+i:U32 -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))) == 1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)) : Nat}

def getw source · line 31 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+j:U32 -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> {Array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), j) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(j))) : Pair(Array<U32>, U32)}

reading a word array at an index below its size

def nths_of source · line 35 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, t), j) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, t), j)} : Maybe<&2, String>}