~/bend-docscommunity

proofs/containers/binary_heap/trace.bend checks

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

13 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 ../../../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 ./state.bend as ST
import ./steps.bend as SP
import ./root.bend as RT
import ./budget.bend as BG

Definitions

def add_le_a source · line 15 · raw

@+a:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> {Nat.is_le(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}

def add_le_l source · line 40 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

def slen_pop source · line 56 · raw

@-A:Data -> @xs:List<&2, A> -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, Pair.fst(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.pop(A, xs))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs), 0n)) == True{} : Bool}

Templates

template pushes source · line 33 · raw

@-A:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> Nat

template budget_head source · line 45 · raw

@-A:Data -> @+d:Nat -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+q:Nat -> @+h:{Nat.is_lt(Nat.add(d, pushes(A, op <> rest)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> {Nat.is_lt(Nat.add(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool}

template budget_tail source · line 49 · raw

@-A:Data -> @+d:Nat -> @+d2:Nat -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+q:Nat -> @+hd2:{Nat.is_le(d2, Nat.add(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op))) == True{} : Bool} -> @+h:{Nat.is_lt(Nat.add(d, pushes(A, op <> rest)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> {Nat.is_lt(Nat.add(d2, pushes(A, rest)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool}

template slen_step source · line 63 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, Pair.fst(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.step(A, cmp, xs, op))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op))) == True{} : Bool}

template so_sh source · line 82 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A>

template so_obs source · line 87 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>

template so_step source · line 92 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.step(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, so_sh(A, cmp, sh, op, so)), so_obs(A, cmp, sh, op, so)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>)}

template so_good source · line 97 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, so_sh(A, cmp, sh, op, so)) == True{} : Bool}

template so_spec source · line 102 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, so_sh(A, cmp, sh, op, so)), so_obs(A, cmp, sh, op, so)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.step(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh), op) : Pair(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>)}

template so_depth source · line 107 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_depth(A, so_sh(A, cmp, sh, op, so)), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_depth(A, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op))) == True{} : Bool}

template so_size source · line 113 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, so_sh(A, cmp, sh, op, so)), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op))) == True{} : Bool}

the size grows by at most the step's push count

template srun_obs source · line 126 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @m:List<&2, A> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>>

template srun_state source · line 129 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @m:List<&2, A> -> List<&2, A>

template spec_run_cons source · line 132 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+m:List<&2, A> -> @+m1:List<&2, A> -> @+o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A> -> @+e:{(m1, o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.step(A, cmp, m, op) : Pair(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>)} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.run(A, cmp, op <> rest, m) == (srun_state(A, cmp, rest, m1), o <> srun_obs(A, cmp, rest, m1)) : Pair(List<&2, A>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>>)}

template RunOK source · line 137 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> Type

template ro_sh source · line 140 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> @r:RunOK(A, cmp, ops, sh, acc) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A>

template ro_run source · line 145 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> @r:RunOK(A, cmp, ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.run_acc(A, cmp, ops, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh), acc)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, ro_sh(A, cmp, ops, sh, acc, r)), List.reverse.go(&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>, srun_obs(A, cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh)), acc)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>>)}

template ro_good source · line 150 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> @r:RunOK(A, cmp, ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, ro_sh(A, cmp, ops, sh, acc, r)) == True{} : Bool}

template ro_model source · line 155 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> @r:RunOK(A, cmp, ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, ro_sh(A, cmp, ops, sh, acc, r)) == srun_state(A, cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh)) : List<&2, A>}

template run_ok source · line 160 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh), pushes(A, ops)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> RunOK(A, cmp, ops, sh, acc)

template run_from source · line 185 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh0) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh0), pushes(A, ops)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.run(A, cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh0)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, ro_sh(A, cmp, ops, sh0, [], run_ok(A, cmp, o, ops, sh0, [], g0, q, hq, room))), srun_obs(A, cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh0))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>>)}

template TraceOK source · line 192 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> Type

template trace_from source · line 195 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh0) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh0), pushes(A, ops)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> TraceOK(A, cmp, ops, sh0)