~/bend-docscommunity

proofs/containers/balanced_search_tree/bk.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/bk.bend as Bk

8 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 ../../lib/array_ext.bend as AX
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC

Definitions

def fillv source · line 16 · raw

@-T:Data -> @+k:Nat -> @xs:List<&2, T> -> @+v:T -> List<&2, T>

the first k slots: the items xs, then v

def headv source · line 25 · raw

@-T:Data -> @xs:List<&2, T> -> @+v:T -> T

def bk source · line 32 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>

def bk_perfect source · line 39 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(T, d, bk(T, d, xs, v)) == True{} : Bool}

def fill_add source · line 46 · raw

@-T:Data -> @+a:Nat -> @+b:Nat -> @+xs:List<&2, T> -> @+v:T -> {fillv(T, Nat.add(a, b), xs, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, fillv(T, a, xs, v), fillv(T, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(T, xs, a), v)) : List<&2, T>}

def dbl source · line 55 · raw

@+p:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+p) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)) : Nat}

def fill_one source · line 58 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> {fillv(T, 1n, xs, v) == [headv(T, xs, v)] : List<&2, T>}

def bk_slots source · line 66 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, bk(T, d, xs, v)) == fillv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), xs, v) : List<&2, T>}

the slots of the block

def fill_len source · line 77 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, fillv(T, k, xs, v)) == k : Nat}

def fill_nth source · line 87 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> @+hk:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, fillv(T, k, xs, v), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, xs, i) : Maybe<&2, T>}

a slot below the length reads the item

def fill_upd source · line 100 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> @+i:Nat -> @+y:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, k, xs, v), i, y) == fillv(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, y), v) : List<&2, T>}

def fill_snoc source · line 111 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> @+y:T -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, k, xs, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), y) == fillv(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, y), v) : List<&2, T>}

def fill_init_c source · line 120 · raw

@-T:Data -> @+j:Nat -> @+x:T -> @+r:List<&2, T> -> @+v:T -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, x <> r) == 1n+m : Nat} -> @ih:(@+m2:Nat -> @+hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, r) == 1n+m2 : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, j, r, v), m2, v) == fillv(T, j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, r), v) : List<&2, T>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, 1n+j, x <> r, v), m, v) == fillv(T, 1n+j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, x <> r), v) : List<&2, T>}

def fill_init source · line 132 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs) == 1n+m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, k, xs, v), m, v) == fillv(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, xs), v) : List<&2, T>}

the last item reset to the default (a pop)

def bk_eq source · line 143 · raw

@-T:Data -> @+d:Nat -> @+u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T> -> @+xs:List<&2, T> -> @+v:T -> @+pu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(T, d, u) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, u) == fillv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), xs, v) : List<&2, T>} -> {u == bk(T, d, xs, v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

def bk_upd source · line 146 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+i:Nat -> @+y:T -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ys:List<&2, T> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, fillv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), xs, v), i, y) == fillv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), ys, v) : List<&2, T>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, bk(T, d, xs, v), i, y) == bk(T, d, ys, v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

def bk_set source · line 151 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+i:Nat -> @+y:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, bk(T, d, xs, v), i, y) == bk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, y), v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

a slot written below the length

def bk_push source · line 155 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+y:T -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, bk(T, d, xs, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), y) == bk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, y), v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

the slot at the length written (a push with room)

def bk_pop source · line 159 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs) == 1n+m : Nat} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, bk(T, d, xs, v), m, v) == bk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, xs), v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

the last slot reset to the default (a pop)

def fill_rep source · line 163 · raw

@-T:Data -> @+k:Nat -> @+v:T -> {fillv(T, k, [], v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(T, k, v) : List<&2, T>}

def drop_all source · line 170 · raw

@-T:Data -> @+xs:List<&2, T> -> @+k:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(T, xs, k) == [] : List<&2, T>}

def bk_empty source · line 179 · raw

@-T:Data -> @+d:Nat -> @+v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(T, d, v) == bk(T, d, [], v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

def bk_grow source · line 183 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{bk(T, d, xs, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(T, d, v)} == bk(T, 1n+d, xs, v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T>}

the doubled block (the old block and a default half)

def fill_at_len source · line 188 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+v:T -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, fillv(T, k, xs, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == Some{v} : Maybe<&2, T>}

the slot at the length (inside the capacity) holds the default