~/bend-docscommunity

proofs/containers/binary_heap/state.bend checks

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

15 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S
import ../../../src/containers/binary_heap.bend as H
import ../../../src/containers/types/binary_heap.bend as E
import ./idx.bend as IX
import ./slots.bend as SL
import ./vals.bend as V
import ./root.bend as RT

Types

type Shadow source · line 22 · raw

@-A:Data -> Data

Definitions

def depth_lt32 source · line 108 · raw

@+depth:Nat -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> {Nat.is_lt(depth, 32n) == True{} : Bool}

depth <= 31 in the form the U32 bridges want it

Templates

template real source · line 25 · raw

@-A:Data -> @sh:Shadow<A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>

template good source · line 32 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:Shadow<A> -> Bool

Representation invariant: the block is a perfect tree of depth levels, the elements occupy exactly the slots [0, size), and heap order holds over them.

template model source · line 43 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:Shadow<A> -> List<&2, A>

Abstraction: the multiset of the occupied slots, sorted -- which is what the specification calls a priority queue.

template abs source · line 50 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> List<&2, A>

Abstraction of an actual heap (proof level; reads the Base.Array through AR.freeze).

template abs_real source · line 55 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+sh:Shadow<A> -> {abs(A, cmp, real(A, sh)) == model(A, cmp, sh) : List<&2, A>}

template Inv source · line 62 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> Type

Invariant of an actual heap: it is the realization of a good shadow.

template g_depth source · line 67 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {Nat.is_le(depth, 31n) == True{} : Bool}

template g_rest1 source · line 70 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t), Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size), Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size), Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth))))) == True{} : Bool}

template g_perfect source · line 73 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool}

template g_rest2 source · line 76 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size), Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size), Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)))) == True{} : Bool}

template g_lay source · line 79 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size) == True{} : Bool}

template g_rest3 source · line 82 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size), Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth))) == True{} : Bool}

template g_ho source · line 85 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size) == True{} : Bool}

template g_size source · line 88 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{good(A, cmp, Sh{size, depth, t}) == True{} : Bool} -> {Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool}

template good_intro source · line 91 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), size) == True{} : Bool} -> @+hs:{Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> {good(A, cmp, Sh{size, depth, t}) == True{} : Bool}

template sh_depth source · line 97 · raw

@-A:Data -> @sh:Shadow<A> -> Nat

template sh_size source · line 102 · raw

@-A:Data -> @sh:Shadow<A> -> Nat

template initial source · line 113 · raw

@-A:Data -> Shadow<A>

template new_real source · line 116 · raw

@-A:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(A) == real(A, initial(A)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}

template new_good source · line 119 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {good(A, cmp, initial(A)) == True{} : Bool}

template new_model source · line 122 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {model(A, cmp, initial(A)) == [] : List<&2, A>}