~/bend-docscommunity

proofs/containers/intrusive_doubly_linked_list/adapter.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/adapter.bend as Adapter

5 imports
import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
import ./writes.bend as W
import ../../../src/containers/intrusive_doubly_linked_list.bend as L

Templates

template apply source · line 11 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-root:(@_:I -> R) -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<N, I> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>

A shadow can contain proof-only history. real need not be injective: two finite-map logs may denote the same physical array. This is a simulation relation, not an impossible requirement that arrays retain the write log.

template run source · line 18 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-root:(@_:I -> R) -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<N, I>> -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>

template laws source · line 26 · raw

@-S:Type -> @-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-real:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> S) -> @-root:(@_:I -> R) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sp:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, N> -> S) -> @-sf:(@_:S -> @_:I -> @_:N -> S) -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<N, I>> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> Data

Only primitive setter equations are premises. They can be discharged for each reachable, in-bounds state; no universal law about invalid IDs or an out-of-bounds array operation is required. No list postcondition appears.

template program_refines source · line 31 · raw

@-S:Type -> @-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-real:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> S) -> @-root:(@_:I -> R) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sp:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, N> -> S) -> @-sf:(@_:S -> @_:I -> @_:N -> S) -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<N, I>> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @hs:laws(S, N, R, P, I, real, root, sn, sp, sh, sf, es, g) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.run(S, N, I, sn, sp, sh, sf, es, real(g)) == real(run(N, R, P, I, root, es, g)) : S}

template remove_program source · line 38 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-root:(@_:I -> R) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+i:I -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> {run(N, R, P, I, root, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(N, I, i, n, p, q), g) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, root(i), n, p, q) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>}

template prepend_program source · line 45 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-root:(@_:I -> R) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+i:I -> @+n:N -> @+h:Maybe<&2, N> -> {run(N, R, P, I, root, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(N, I, i, n, h), g) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, root(i), n, h) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>}

template remove_refines source · line 52 · raw

@-S:Type -> @-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-real:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> S) -> @-root:(@_:I -> R) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sp:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, N> -> S) -> @-sf:(@_:S -> @_:I -> @_:N -> S) -> @-eq:(@_:N -> @_:N -> Bool) -> @-next:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-prev:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+i:I -> @+n:N -> @hn:{next(real(g), n) == (real(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, n)) : Pair(S, Maybe<&2, N>)} -> @hp:{prev(real(g), n) == (real(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n)) : Pair(S, Maybe<&2, N>)} -> @hs:laws(S, N, R, P, I, real, root, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(N, I, i, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, n)), g) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_doubly_linked_list.remove(S, N, I, next, prev, sn, sp, sh, real(g), i, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.remove(N, R, P, eq, g, root(i), n)) : S}

The source/model connection reaches the actual exported remove function.

template prepend_refines source · line 60 · raw

@-S:Type -> @-N:Data -> @-R:Data -> @-P:Data -> @-I:Data -> @-real:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> S) -> @-root:(@_:I -> R) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sp:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, N> -> S) -> @-sf:(@_:S -> @_:I -> @_:N -> S) -> @-H:Data -> @-req:(@_:R -> @_:R -> Bool) -> @-get:(@_:S -> @_:H -> Pair(S, Maybe<&2, N>)) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+h:H -> @+i:I -> @+n:N -> @hg:{get(real(g), h) == (real(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, root(i))) : Pair(S, Maybe<&2, N>)} -> @hs:laws(S, N, R, P, I, real, root, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(N, I, i, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, root(i))), g) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_doubly_linked_list.prepend_as(S, N, H, I, get, sn, sp, sf, real(g), h, i, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prepend(N, R, P, req, g, root(i), n)) : S}

H and I remain distinct. The read equation expresses coherence of the particular reader/writer contexts; it does not force identical types.