~/bend-docscommunity

proofs/containers/balanced_search_tree/arr.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/dynamic_array.bend as D
import ../../../src/containers/types/dynamic_array.bend as DE
import ../dynamic_array/layout.bend as LY
import ../dynamic_array/state.bend as DAS
import ./mk.bend as MK
import ./da.bend as DA

Definitions

def somes_mk source · line 17 · 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/containers/dynamic_array/layout.somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs))) == xs : List<&2, T>}

def good_mk source · line 21 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}) == True{} : Bool}

def len_upd source · line 30 · raw

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

def len_snoc source · line 51 · raw

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

Templates

template blk_get source · line 26 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.get_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, xs, i))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

template blk_set source · line 33 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.set_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v))}), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template blk_set_out source · line 39 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.set_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template blk_swap source · line 42 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, xs, i, v))}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, xs, i))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

template blk_swap_out source · line 48 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

template blk_push_room source · line 54 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:T -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v))}), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template blk_push_grow source · line 59 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:T -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+hdl:{Nat.is_lt(d, l) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, xs, v))}), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template blk_push_full source · line 66 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:T -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+hdl:{Nat.is_lt(d, l) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)}), Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template blk_clear source · line 69 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, xs)})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.mk(T, d, [])}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}