proofs/containers/hash_table/insu.bend checks

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

10 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../../spec/lib/common.bend as SC
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ./cyc.bend as CY
import ./probe_all.bend as PA
import ../../lib/words32.bend as W32

Definitions

def is_gt_nat source · line 25 · raw

@+a:U32 -> @+b:U32 -> {U32.is_gt(a, b) == Nat.is_gt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) : Bool}

def gt_le_c source · line 28 · raw

@+a:Nat -> @+b:Nat -> @+c:Cmp -> @+hc:{Nat.cmp(a, b) == c : Cmp} -> @+h:{Cmp.is_gt(c) == False{} : Bool} -> {Cmp.is_le(c) == True{} : Bool}

def gt_false_le source · line 37 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_gt(a, b) == False{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def gt_le_t source · line 40 · raw

@+a:Nat -> @+b:Nat -> @+c:Cmp -> @+h:{Cmp.is_gt(c) == True{} : Bool} -> {Cmp.is_le(c) == False{} : Bool}

def gt_true_nle source · line 50 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_gt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == False{} : Bool}

a > b: not a <= b

def dle_c source · line 55 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(x, y) == c : Bool} -> {c == True{} : Bool}

def dbl_le_inv source · line 62 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool} -> {Nat.is_le(x, y) == True{} : Bool}

def succ_le_pow source · line 66 · raw

@+x:Nat -> @+p:Nat -> @+h:{Nat.is_le(Nat.double(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+p)) == True{} : Bool} -> {Nat.is_le(1n+x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+p)) == True{} : Bool}

2x <= 2^(p+1): x + 1 <= 2^(p+1)

def over_c source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+x:Nat -> @+h:{Nat.is_le(Nat.double(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {Nat.is_le(1n+x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool}

def inc_n source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+n:U32 -> @+hl:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(n)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n) : Nat}

THEOREM: with at most half the buckets full, one more entry is n + 1 and the load test compares 2(n + 1) with the bucket count

def over_val source · line 81 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+hk0:{Nat.is_lt(0n, k) == True{} : Bool} -> @+n:U32 -> @+hl:{Nat.is_le(Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k))) == Nat.is_gt(Nat.double(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) : Bool}