~/bend-docscommunity

proofs/containers/binary_heap/push.bend checks

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

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 ./up.bend as UPS
import ./grow.bend as GR
import ./state.bend as ST

Definitions

def room_bridge source · line 107 · raw

@+size:Nat -> @+depth:Nat -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+hs:{Nat.is_le(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> {U32.is_lt(U32.from_nat(size), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(depth)) == Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) : Bool}

def succ_le_double source · line 113 · raw

@+p:Nat -> @+h:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.is_le(1n+p, Nat.double(p)) == True{} : Bool}

Templates

template pair_off source · line 32 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @m:Nat -> @+hmi:{Nat.is_lt(m, i) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), m) == True{} : Bool}

template exc_step source · line 41 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+m:Nat -> @+hm:{Nat.is_lt(m, 1n+i) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(m, i) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_skip(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), m, i) == True{} : Bool}

template exc_up source · line 50 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @k:Nat -> @+hk:{Nat.is_le(k, 1n+i) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), k, i) == True{} : Bool}

template kids_leaf source · line 61 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+u:Nat -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ss, 1n+i, u, i) == True{} : Bool}

template lay_off source · line 68 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+v:Maybe<&2, A> -> @k:Nat -> @+hk:{Nat.is_le(k, i) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, v), k) == True{} : Bool}

template lay_push source · line 78 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), 1n+i) == True{} : Bool}

template ms_push source · line 85 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), 1n+i)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), i))) : List<&2, A>}

template PushOK source · line 91 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @x:A -> Type

template push_from source · line 96 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+size:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+x:A -> @+tgt:List<&2, A> -> @+hd:{Nat.is_le(d, 31n) == True{} : Bool} -> @+hs:{Nat.is_le(1n+size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hdd:{Nat.is_le(d, 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_depth(A, sh0)) == True{} : Bool} -> @+eq0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.push(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh0), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.BH{1n+size, U32.from_nat(1n+size), d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.sift_up(A, cmp, d, U32.from_nat(size), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t))} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>} -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.SiftOK(A, cmp, d, 1n+size, tgt, d, t, size, x) -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A>, sh2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.push(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh0), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh2) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh2) == tgt : List<&2, A>}, {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_depth(A, sh2), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_depth(A, sh0)) == True{} : Bool})))>

The sift-up result, packaged as the new shadow. d is the depth of the block the element is written into (the grown depth if the block was full).

template push_room_ok source · line 122 · 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>> -> @+x:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> @+hlt:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> PushOK(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}, x)

template push_grow_ok source · line 139 · 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>> -> @+x:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> @+hfull:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == False{} : Bool} -> @+hroom:{Nat.is_lt(depth, 31n) == True{} : Bool} -> PushOK(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}, x)

template push_ok source · line 160 · 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>> -> @+x:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> @+hroom:{Bool.or(Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)), Nat.is_lt(depth, 31n)) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_lt(size, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == b : Bool} -> PushOK(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}, x)