~/bend-docscommunity

proofs/containers/binary_heap/sorted.bend checks

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

19 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 ./u32idx.bend as UX
import ./slots.bend as SL
import ./vals.bend as V
import ./root.bend as RT
import ./down.bend as DN
import ./state.bend as ST
import ./pop.bend as PO

Templates

template drain_unfold source · line 27 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+depth:Nat -> @+m:Nat -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool} -> @+hs:{Nat.is_le(1n+m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>} -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(1n+m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == root <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.sift_down(A, cmp, depth, U32.from_nat(m), U32.from_nat(0n), last, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)))) : List<&2, A>}

One drain iteration: the root comes out and the last element is sifted down over the copy -- the same reduction pop performs, on the copy.

template drain_one source · line 41 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+depth:Nat -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool} -> @+hs:{Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{last} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(1n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == [root] : List<&2, A>}

The last element of the copy: the drain stops with it.

template DrainRec source · line 55 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @f:Nat -> @depth:Nat -> @m:Nat -> Type

The recursive call the drain makes, as a (linear) function argument: Bend has no mutual recursion, so the induction hands its own instance down.

template drain_move source · line 58 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+f:Nat -> @+k:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 1n+k) == Some{last} : Maybe<&2, A>} -> @rec:DrainRec(A, cmp, f, depth, 1n+k) -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/down.SiftDownOK(A, cmp, depth, 1n+k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/pop.hole(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 1n+k, last), 1n+k)), depth, t, 0n, last) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(2n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) : List<&2, A>}

template drain_single source · line 77 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+depth:Nat -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n, depth, t}) == True{} : Bool} -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(1n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n, depth, t}) : List<&2, A>}

the one-element copy

template drain_two source · line 85 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+f:Nat -> @+k:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @rec:DrainRec(A, cmp, f, depth, 1n+k) -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 1n+k) == Some{v} : Maybe<&2, A>}> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(2n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) : List<&2, A>}

template drain_pair source · line 91 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+f:Nat -> @+k:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) == True{} : Bool} -> @rec:DrainRec(A, cmp, f, depth, 1n+k) -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, 1n+f, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(2n+k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{2n+k, depth, t}) : List<&2, A>}

template drain_ok source · line 98 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @fuel:Nat -> @+depth:Nat -> @size:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> @+hf:{Nat.is_le(size, fuel) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_go(A, cmp, fuel, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.drain_probe(A, U32.from_nat(size), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) : List<&2, A>}

The whole drain: as many iterations as the copy has elements.

template to_sorted_ok source · line 118 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.to_sorted_list(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, List<&2, A>)}

---- to_sorted_list ----

The heap is returned unchanged and the observation is its sorted multiset: the drain runs on the clone.