~/bend-docscommunity

proofs/containers/deque/trace.bend checks

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

9 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../../spec/containers/deque.bend as S
import ../../../src/containers/deque.bend as DQ
import ../../../src/containers/types/deque.bend as E
import ./state.bend as ST
import ./stepok.bend as K
import ./steps.bend as PS

Definitions

def srun_obs source · line 41 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @m:List<&2, T> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>>

def srun_state source · line 44 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @m:List<&2, T> -> List<&2, T>

def spec_run_cons source · line 47 · raw

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

Templates

template so_sh source · line 19 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T>

template so_obs source · line 24 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>

template so_step source · line 29 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(T, sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, so_sh(T, sh, op, so)), so_obs(T, sh, op, so)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>)}

template so_spec source · line 34 · raw

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

template RunOK source · line 52 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>> -> Type

template ro_sh source · line 55 · raw

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

template ro_run source · line 60 · raw

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

template ro_model source · line 65 · raw

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

template run_ok source · line 70 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>> -> RunOK(T, ops, sh, acc)

template run_from source · line 91 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh0)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, ro_sh(T, ops, sh0, [], run_ok(T, ops, sh0, []))), srun_obs(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh0))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>>)}

template TraceOK source · line 98 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> Type

template trace_from source · line 101 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> TraceOK(T, ops, sh0)