~/bend-docscommunity

proofs/containers/intrusive_doubly_linked_list/writes.bend checks

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

7 imports
import Base
import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
import ./fold.bend as Fold
import ./clear.bend as Clear
import ../../lib/nat.bend as NN
import ../../../src/containers/internal/intrusive_list.bend as L
import ../../../src/containers/types/intrusive_doubly_linked_list.bend as E

Templates

template remove_known source · line 16 · raw

@-S:Type -> @-N:Data -> @-I:Data -> @-next:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-prev:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-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) -> @s2:S -> @+i:I -> @+node:N -> @+before:Maybe<&2, N> -> @+after:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.remove_2(S, N, I, next, prev, sn, sp, sh, i, node, after, (s2, before)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.run(S, N, I, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(N, I, i, node, before, after), s2) : S}

template remove_writes source · line 23 · raw

@-S:Type -> @-N:Data -> @-I:Data -> @-next:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-prev:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-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) -> @s:S -> @s1:S -> @s2:S -> @+i:I -> @+node:N -> @+before:Maybe<&2, N> -> @+after:Maybe<&2, N> -> @hn:{next(s, node) == (s1, after) : Pair(S, Maybe<&2, N>)} -> @hp:{prev(s1, node) == (s2, before) : Pair(S, Maybe<&2, N>)} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.remove(S, N, I, next, prev, sn, sp, sh, s, i, node) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.run(S, N, I, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(N, I, i, node, before, after), s2) : S}

template prepend_known source · line 28 · raw

@-S:Type -> @-N:Data -> @-H:Data -> @-I:Data -> @-get:(@_:S -> @_:H -> Pair(S, Maybe<&2, N>)) -> @-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) -> @s1:S -> @+i:I -> @+node:N -> @+head:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.prepend_as_1(S, N, H, I, get, sn, sp, sf, i, node, (s1, head)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.run(S, N, I, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(N, I, i, node, head), s1) : S}

template prepend_writes source · line 33 · raw

@-S:Type -> @-N:Data -> @-H:Data -> @-I:Data -> @-get:(@_:S -> @_:H -> Pair(S, Maybe<&2, N>)) -> @-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) -> @s:S -> @s1:S -> @+h:H -> @+i:I -> @+node:N -> @+head:Maybe<&2, N> -> @hg:{get(s, h) == (s1, head) : Pair(S, Maybe<&2, N>)} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.prepend_as(S, N, H, I, get, sn, sp, sf, s, h, i, node) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.run(S, N, I, sn, sp, sh, sf, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(N, I, i, node, head), s1) : S}

template pool_then_next source · line 37 · raw

@-S:Type -> @-N:Data -> @-C:Data -> @-next:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-make:(@_:S -> @_:C -> Pair(S, N)) -> @c:C -> @r:Pair(S, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Pool<N>) -> Pair(S, Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Pool<N>, N))

template pool_lifo source · line 41 · raw

@-S:Type -> @-N:Data -> @-C:Data -> @-next:(@_:S -> @_:N -> Pair(S, Maybe<&2, N>)) -> @-sn:(@_:S -> @_:N -> @_:Maybe<&2, N> -> S) -> @-make:(@_:S -> @_:C -> Pair(S, N)) -> @s:S -> @+c:C -> @+node:N -> @+head:Maybe<&2, N> -> @+count:Nat -> @read_back:{next(sn(s, node, head), node) == (sn(s, node, head), head) : Pair(S, Maybe<&2, N>)} -> {pool_then_next(S, N, C, next, sn, make, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.pool_free(S, N, sn, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Pool{head, count}, node)) == (sn(sn(s, node, head), node, None{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Pool{head, count}, node) : Pair(S, Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Pool<N>, N))}

template default_node source · line 45 · raw

@-N:Data -> @-V:Data -> @+v:V -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.new_node(N, V, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Node{None{}, None{}, v} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.DefaultNode<N, V>}