~/bend-docscommunity

proofs/containers/hash_table/arena.bend checks

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

14 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./state.bend as ST
import ./insa.bend as IA
import ../../lib/words32.bend as W32

Definitions

def nths_app source · line 30 · raw

@+xs:List<&2, String> -> @+r:List<&2, String> -> @+t:Nat -> @+h:{Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, xs, r), t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(xs, t) : String}

def len_eq_lt source · line 51 · raw

@-T:Data -> @+xs:List<&2, T> -> @+d:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat} -> @+t:Nat -> @+h:{Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool}

def dec_app_c source · line 56 · raw

@+w:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+r:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+emp:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, emp)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, r), emp) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, emp) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

def dl_app source · line 65 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+r:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+n:Nat -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), sd}, n) == True{} : Bool} -> @+m:Nat -> @+i:Nat -> @+hmi:{Nat.is_le(Nat.add(i, m), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, r), m, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dlist(tb, kl, m, i) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

def bs_app source · line 75 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+r:List<&2, String> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+n:Nat -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), sd}, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, r), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk>}

THEOREM: appending cells to the key arena leaves every bucket as it was

def wb_mono source · line 80 · raw

@+sd:Nat -> @+sd2:Nat -> @+hle:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd2)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd2, b) == True{} : Bool}

def well_mono source · line 88 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sd:Nat -> @+sd2:Nat -> @+hle:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd2)) == True{} : Bool} -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{bs, sd}, n) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{bs, sd2}, m) == True{} : Bool}

Templates

template vac_eq source · line 21 · raw

@-V:Data -> @+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.vac(&2, V, d) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, V>, d, None{})) : Array<Maybe<&2, V>>}

the blank value half

template nthm_app source · line 39 · raw

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

template nthb_app source · line 48 · raw

@-V:Data -> @+xs:List<&2, Maybe<&2, V>> -> @+r:List<&2, Maybe<&2, V>> -> @+t:Nat -> @+h:{Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, xs, r)), t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.nthb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, xs), t) : Bool}

template live_app_b source · line 96 · raw

@-V:Data -> @+vsl:List<&2, Maybe<&2, V>> -> @+r:List<&2, Maybe<&2, V>> -> @+f:Nat -> @+hf:{Nat.is_le(f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, vsl)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, vsl), f, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.live_b(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, vsl, r)), f, b) == True{} : Bool}

template live_app source · line 106 · raw

@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+vsl:List<&2, Maybe<&2, V>> -> @+r:List<&2, Maybe<&2, V>> -> @+f:Nat -> @+hf:{Nat.is_le(f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, vsl)) == True{} : Bool} -> @+n:Nat -> @+h:{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), f}, n) == True{} : Bool} -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PLive{bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.lvs(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, vsl, r)), f}, m) == True{} : Bool}

template ent_app source · line 116 · raw

@-V:Data -> @+vsl:List<&2, Maybe<&2, V>> -> @+r:List<&2, Maybe<&2, V>> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, vsl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.ent(V, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, vsl, r)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.ent(V, b, vsl) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}

template absm_app source · line 124 · raw

@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+vsl:List<&2, Maybe<&2, V>> -> @+r:List<&2, Maybe<&2, V>> -> @+sd:Nat -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, vsl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+n:Nat -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{bs, sd}, n) == True{} : Bool} -> @+m:Nat -> @+j:Nat -> @+hjm:{Nat.is_le(Nat.add(j, m), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, vsl, r), m, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.absm(V, bs, vsl, m, j) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.Entry<V>>}