~/bend-docscommunity

proofs/containers/intrusive_doubly_linked_list/costs.bend checks

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

2 imports
import Base
import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as S

Templates

template writes source · line 4 · raw

@-N:Data -> @-I:Data -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<N, I>> -> Nat

template remove_bound source · line 11 · raw

@-N:Data -> @-I:Data -> @+r:I -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> {Nat.is_lt(writes(N, I, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(N, I, r, n, p, q)), 5n) == True{} : Bool}

Combined with write refinement: the number of primitive field/root writes is bounded independently of list size. Accessor work is application-defined.

template prepend_bound source · line 18 · raw

@-N:Data -> @-I:Data -> @+r:I -> @+n:N -> @+h:Maybe<&2, N> -> {Nat.is_lt(writes(N, I, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(N, I, r, n, h)), 4n) == True{} : Bool}