~/bend-docscommunity

proofs/containers/binary_heap/budget.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/budget.bend as Budget

8 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/binary_heap.bend as S
import ./root.bend as RT
import ./state.bend as ST

Definitions

def pow2_inv_c source · line 15 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(b)) == True{} : Bool} -> @c:Bool -> @+ec:{Nat.is_lt(a, b) == c : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def pow2_inv source · line 23 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def room_or_c source · line 26 · raw

@+size:Nat -> @+depth:Nat -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+hs:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == b : Bool} -> {Bool.or(Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)), Nat.is_lt(depth, 31n)) == True{} : Bool}

def room_or source · line 36 · raw

@+size:Nat -> @+depth:Nat -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+hs:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> {Bool.or(Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)), Nat.is_lt(depth, 31n)) == True{} : Bool}

the push premise the block needs, from the size budget

Templates

template sz_len source · line 40 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh)) : Nat}

the size of a good shadow is the length of its model

template push_size source · line 46 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+y:A -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> @+g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh1) == True{} : Bool} -> @+ems:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh)) : List<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh1) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh) : Nat}

a push onto a good shadow adds one element

template len_from_list source · line 55 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ys:List<&2, A> -> @+acc:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.from_list(A, cmp, ys, acc)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, ys), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, acc)) : Nat}