~/bend-docscommunity

proofs/containers/doubly_linked_list/trace.bend checks

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

13 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./ok.bend as OK
import ./valid.bend as VD
import ./step.bend as SP

Definitions

def room source · line 21 · raw

@-T:Data -> @m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+cz:Nat -> Bool

fewer than 2^cz ids issued

def fits source · line 27 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+cz:Nat -> Bool

room before every operation of ops

def new_sh source · line 92 · raw

@-T:Data -> @+tag:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T>

Templates

template step_sh source · line 35 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), op))

template RunOK source · line 42 · raw

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

template run_c2 source · line 47 · raw

@-T:Data -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T> -> @+er:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh1), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh1), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @q:RunOK(T, rest, sh1, o <> acc) -> RunOK(T, op <> rest, sh, acc)

after the rest

template run_c1 source · line 58 · raw

@-T:Data -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>> -> @+cz:Nat -> @+hf:{fits(T, rest, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op)), cz) == True{} : Bool} -> @p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), op)) -> @rec:(@+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+acc1:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>> -> @+hg1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh1) == True{} : Bool} -> @+hf1:{fits(T, rest, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh1), cz) == True{} : Bool} -> RunOK(T, rest, sh1, acc1)) -> RunOK(T, op <> rest, sh, acc)

after the first operation

template run_ok source · line 65 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hf:{fits(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> RunOK(T, ops, sh, acc)

template TraceOK source · line 74 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> Type

template fin_c source · line 77 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @q:RunOK(T, ops, sh, []) -> TraceOK(T, ops, sh)

template trace_ok source · line 86 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hf:{fits(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> TraceOK(T, ops, sh)

THEOREM (traces from a good shadow)

template new_ok source · line 97 · raw

@-T:Data -> @+tag:U32 -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, 1, 0, 0, 0, 0, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{None{}}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, [], []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.new(T, tag) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, 1, 0, 0, 0, 0, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{None{}}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, [], []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.empty(T, tag) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, 1, 0, 0, 0, 0, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{None{}}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, [], []}) == True{} : Bool}))

THEOREM (new): the new list is the real list of a good shadow whose model is the specification's empty list

template run_new source · line 102 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+hf:{fits(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.empty(T, tag), cz) == True{} : Bool} -> TraceOK(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, 1, 0, 0, 0, 0, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{None{}}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TLeaf{0}, [], []})

THEOREM (observations): every trace on a new list whose specification states keep fewer than 2^cz issued ids observes what the specification does