proofs/containers/intrusive_doubly_linked_list/edits.bend checks

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

3 imports

import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
import ./shape.bend as S

Templates

template prepend_valid source · line 8 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @+rsame:{req(r, r) == True{} : Bool} -> @+un:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, xs) -> @+away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @+detached:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n) == None{} : Maybe<&2, N>} -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, None{}, xs, None{}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, r, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, xs, None{})), r, n <> xs)

Prepend preserves a whole reciprocal, unique chain. Identity comparison is proof-only; the production algorithm still performs only its field accesses.

template remove_head_valid source · line 23 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @+rsame:{req(r, r) == True{} : Bool} -> @+un:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, xs) -> @away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, Some{n}, xs, None{}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, None{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, xs, None{})), r, xs)

template optional_prefix source · line 32 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+prefix:List<&2, N> -> @+suffix:List<&2, N> -> @+p:N -> @+n:N -> @dis:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, prefix, suffix) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, None{}, prefix, Some{n}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.optional_prev(N, R, P, g, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, suffix, None{}), Some{p}), None{}, prefix, Some{n})

template optional_suffix source · line 37 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+suffix:List<&2, N> -> @+p:N -> @+n:N -> @un:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, suffix) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, Some{n}, suffix, None{}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.optional_prev(N, R, P, g, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, suffix, None{}), Some{p}), Some{p}, suffix, None{})

template cut_nonhead_root source · line 42 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:N -> @+q:Maybe<&2, N> -> @+x:R -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, Some{p}, q), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x) : Maybe<&2, N>}

template join_last source · line 47 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+p:N -> @+b:List<&2, N> -> @ga:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, None{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, b, None{})) -> @gb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, Some{p}, b, None{}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, None{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), b), None{})

template remove_nonhead_valid source · line 56 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+a:List<&2, N> -> @+p:N -> @+b:List<&2, N> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p])) -> @+ub:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, b) -> @+dis:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), b) -> @+np:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p])) -> @+nb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, b) -> @root:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), None{}) : Maybe<&2, N>} -> @prefix:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, None{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), Some{n}) -> @suffix:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, Some{n}, b, None{}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, Some{p}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, b, None{})), r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), b))

The input is a zipper around the known member. Its premises are exactly separate, unique prefix/member/suffix identities and their old field facts; no postcondition is assumed. Prefix and suffix can have arbitrary lengths.

template prepend_preserves source · line 70 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @rsame:{req(r, r) == True{} : Bool} -> @away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @detached:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n) == None{} : Maybe<&2, N>} -> @valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, xs) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prepend(N, R, P, req, g, r, n), r, n <> xs)

Public semantic statements: all input facts are taken from valid(g,order).

template remove_head_preserves source · line 76 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @rsame:{req(r, r) == True{} : Bool} -> @valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, n <> xs) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.remove(N, R, P, eq, g, r, n), r, xs)

template remove_nonhead_preserves source · line 83 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+a:List<&2, N> -> @+p:N -> @+b:List<&2, N> -> @valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), n <> b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.remove(N, R, P, eq, g, r, n), r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), b))

template attach_frame source · line 98 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+h:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, r, n, h)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}

template cut_frame source · line 103 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, p, q)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}