~/bend-docscommunity

proofs/containers/balanced_search_tree/mk.bend checks

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

9 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
import ../dynamic_array/layout.bend as LY

Definitions

def fill source · line 16 · raw

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

the first k slots of the items xs

def headm source · line 25 · raw

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

def mk source · line 32 · raw

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

def mk_perfect source · line 39 · raw

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

def fill_add source · line 46 · raw

@-T:Data -> @+a:Nat -> @+b:Nat -> @+xs:List<&2, T> -> {fill(T, Nat.add(a, b), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, fill(T, a, xs), fill(T, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(T, xs, a))) : List<&2, Maybe<&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> -> {fill(T, 1n, xs) == [headm(T, xs)] : List<&2, Maybe<&2, T>>}

def mk_slots source · line 66 · raw

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

the slots of the canonical block

def fill_somes source · line 79 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, fill(T, k, xs)) == xs : List<&2, T>}

def fill_nones source · line 90 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.nones(T, fill(T, k, [])) == True{} : Bool}

def fill_lay source · line 97 · raw

@-T:Data -> @+k:Nat -> @+xs:List<&2, T> -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, fill(T, k, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool}

def fill_len source · line 108 · raw

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

def fill_upd source · line 117 · raw

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

def fill_snoc source · line 128 · 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.update(Maybe<&2, T>, fill(T, k, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), Some{v}) == fill(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v)) : List<&2, Maybe<&2, T>>}

def mk_eq source · line 139 · raw

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

def mk_set source · line 143 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v: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(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}) == mk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>>}

a slot written below the length

def mk_push source · line 149 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, T> -> @+v: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(Maybe<&2, T>, d, mk(T, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), Some{v}) == mk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>>}

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

def fill_rep source · line 153 · raw

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

def drop_all source · line 160 · 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 mk_grow source · line 170 · raw

@-T:Data -> @+d:Nat -> @+xs:List<&2, 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{mk(T, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})} == mk(T, 1n+d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>>}

the doubled block of a full list (old block and an empty half)

def mk_empty source · line 174 · raw

@-T:Data -> @+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{}) == mk(T, d, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>>}