~/bend-docscommunity

proofs/containers/hash_table/insf.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./words.bend as WR
import ./buckets.bend as B
import ./state.bend as ST
import ./insm.bend as IM
import ../../lib/nat_list.bend as NL
import ../../lib/words32.bend as W32

Definitions

def mem_ne_c source · line 18 · raw

@+a:Nat -> @+t:Nat -> @+seen:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(a, seen) == True{} : Bool} -> @+ht:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, seen)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(a, t) == c : Bool} -> {c == False{} : Bool}

def mem_ne source · line 27 · raw

@+a:Nat -> @+t:Nat -> @+seen:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(a, seen) == True{} : Bool} -> @+ht:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, seen)) == True{} : Bool} -> {Nat.is_eq(a, t) == False{} : Bool}

a slot on the list and a slot not on it differ

def mem_cons source · line 30 · raw

@+a:Nat -> @+t:Nat -> @+seen:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(a, seen) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(a, t <> seen) == True{} : Bool}

def fl_tr source · line 34 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+w:U32 -> @+L:U32 -> @+key:String -> @+nb:Nat -> @+nxl:List<&2, U32> -> @+cnt:Nat -> @+f:U32 -> @+fr:Nat -> @+seen:List<&2, Nat> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(L)), seen) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{w, L, key}), nb, nxl, cnt, f, fr, seen) == True{} : Bool}

THEOREM: filling bucket e with a slot the list has visited keeps the list valid

def subl source · line 55 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> Bool

def ms_c source · line 62 · raw

@+t:Nat -> @+x:Nat -> @+r:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(x, t) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, r)) == True{} : Bool} -> @rec:(@hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, r) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, ys) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, ys) == True{} : Bool}

def memn_sub source · line 69 · raw

@+t:Nat -> @+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+hs:{subl(xs, ys) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, ys) == True{} : Bool}

def nm_c source · line 76 · raw

@+t:Nat -> @+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+hs:{subl(xs, ys) == True{} : Bool} -> @+h:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, ys)) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(t, xs) == c : Bool} -> {Bool.not(c) == True{} : Bool}

def subl_cons source · line 83 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+y:Nat -> @+h:{subl(xs, ys) == True{} : Bool} -> {subl(xs, y <> ys) == True{} : Bool}

def subl_both source · line 90 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+t:Nat -> @+h:{subl(xs, ys) == True{} : Bool} -> {subl(t <> xs, t <> ys) == True{} : Bool}

def fl_weak source · line 94 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+nb:Nat -> @+nxl:List<&2, U32> -> @+cnt:Nat -> @+f:U32 -> @+fr:Nat -> @+seen:List<&2, Nat> -> @+seen2:List<&2, Nat> -> @+hs:{subl(seen2, seen) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(bs, nb, nxl, cnt, f, fr, seen2) == True{} : Bool}

THEOREM: a valid list stays valid when fewer slots count as visited

def cnt_zero source · line 112 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+nb:Nat -> @+nxl:List<&2, U32> -> @+cnt:Nat -> @+fr:Nat -> @+seen:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(bs, nb, nxl, cnt, 0, fr, seen) == True{} : Bool} -> {cnt == 0n : Nat}

an empty list (link 0) has no links

def cnt_pos source · line 120 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+nb:Nat -> @+nxl:List<&2, U32> -> @+cnt:Nat -> @+f:U32 -> @+fr:Nat -> @+seen:List<&2, Nat> -> @+hf:{U32.is_eq(f, 0) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool} -> Sigma<&1, &1, Nat, p => {cnt == 1n+p : Nat}>

a list that is not empty has a first link

def sub_zero_eq source · line 128 · raw

@+fr:Nat -> @+n:Nat -> @+hle:{Nat.is_le(n, fr) == True{} : Bool} -> @+h:{Nat.sub(fr, n) == 0n : Nat} -> {fr == n : Nat}

with n <= fr and fr - n = 0: fr = n

def sub_step source · line 132 · raw

@+fr:Nat -> @+n:Nat -> @+p:Nat -> @+hle:{Nat.is_le(n, fr) == True{} : Bool} -> @+h:{Nat.sub(fr, n) == 1n+p : Nat} -> Pair({Nat.sub(fr, 1n+n) == p : Nat}, {Nat.is_le(1n+n, fr) == True{} : Bool})

with n <= fr and fr - n = p + 1: n + 1 <= fr and fr - (n + 1) = p

def ns_live_b source · line 141 · raw

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

def noslot_live source · line 149 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+lv:List<&2, Bool> -> @+fr:Nat -> @+n:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{bs, lv, fr}, n) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(bs, fr, m) == True{} : Bool}

THEOREM: every bucket's slot is below fresh, so fresh is unused