proofs/containers/hash_table/tools.bend checks

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

11 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/u32.bend as U
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./keys.bend as K
import ./buckets.bend as B
import ./state.bend as ST

Definitions

def Holder source · line 16 · raw

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

def hold_up source · line 19 · raw

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

def fh_c source · line 24 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+key:String -> @+q:Nat -> @+c:Bool -> @+hc:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, q))) == c : Bool} -> @+h:{Bool.and(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, q)) == False{} : Bool} -> @rec:(@hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, q) == False{} : Bool} -> Holder(bs, key, q)) -> Holder(bs, key, 1n+q)

def find_hold source · line 32 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+key:String -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{bs, key}, m) == False{} : Bool} -> Holder(bs, key, m)

not every bucket is free of key: one holds it

def slot_inj source · line 42 · raw

@+a:U32 -> @+b:U32 -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(a)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(b)) : Nat} -> {a == b : U32}

slot(l) = l - 1 is injective

def nolb_c source · line 46 · raw

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

def nolb_inst source · line 53 · 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} -> @+j:Nat -> @+hj:{Nat.is_lt(j, m) == True{} : Bool} -> {Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)), l))) == True{} : Bool}

def link_ne_b source · line 61 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+i:Nat -> @+j:Nat -> @+hji:{Nat.is_lt(j, i) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.uq_b(bs, i, b) == True{} : Bool} -> @+hob:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b) == True{} : Bool} -> @+hoj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)) == True{} : Bool} -> {U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b)) == False{} : Bool}

the full bucket b at index i and the full bucket at j < i have different links

def slots_ne_of source · line 69 · raw

@+a:U32 -> @+b:U32 -> @+h:{U32.is_eq(a, b) == False{} : Bool} -> @+c:Bool -> @+hc:{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(b))) == c : Bool} -> {c == False{} : Bool}

def slot_ne_lt source · line 77 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{bs}, n) == True{} : Bool} -> @+i:Nat -> @+j:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> @+hji:{Nat.is_lt(j, i) == True{} : Bool} -> @+oi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool} -> @+oj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)) == True{} : Bool} -> {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(bs, j)))), 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(bs, i))))) == False{} : Bool}

def slot_ne_c source · line 80 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{bs}, n) == True{} : Bool} -> @+i:Nat -> @+j:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hne:{Nat.is_eq(j, i) == False{} : Bool} -> @+oi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool} -> @+oj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(j, i) == c : Bool} -> {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(bs, j)))), 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(bs, i))))) == False{} : Bool}

def slot_ne source · line 88 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+huq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PUniq{bs}, n) == True{} : Bool} -> @+i:Nat -> @+j:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hne:{Nat.is_eq(j, i) == False{} : Bool} -> @+oi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool} -> @+oj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)) == True{} : Bool} -> {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(bs, j)))), 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(bs, i))))) == False{} : Bool}

THEOREM: distinct full buckets use distinct slots

Templates

template nthm_upd_same source · line 93 · raw

@-V:Data -> @+vsl:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+h:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, vsl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, vsl, s, m), s) == m : Maybe<&2, V>}

template nthm_upd_other source · line 102 · raw

@-V:Data -> @+vsl:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+t:Nat -> @+m:Maybe<&2, V> -> @+h:{Nat.is_eq(s, t) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, vsl, s, m), t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, vsl, t) : Maybe<&2, V>}