proofs/containers/intrusive_doubly_linked_list/costs.bend

bend-collections-laws-containers@1.0.0.0 · 21 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as S
3
4def writes(~N: Data, ~I: Data, es: List<&2,S.Edit<N,I>>) -> Nat:
5  match es:
6    case Nil{}: 0n
7    case Con{e,rest}: 1n+writes(~N,~I,rest)
8
9# Combined with write refinement: the number of primitive field/root writes
10# is bounded independently of list size. Accessor work is application-defined.
11def remove_bound(~N: Data, ~I: Data, +r: I, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>) -> {Nat.is_lt(writes(~N,~I,S.remove(N,I,r,n,p,q)),5n) == True{} : Bool}:
12  match p q:
13    case None{} None{}: {==}
14    case None{} Some{b}: {==}
15    case Some{a} None{}: {==}
16    case Some{a} Some{b}: {==}
17
18def prepend_bound(~N: Data, ~I: Data, +r: I, +n: N, +h: Maybe<&2,N>) -> {Nat.is_lt(writes(~N,~I,S.prepend(N,I,r,n,h)),4n) == True{} : Bool}:
19  match h:
20    case None{}: {==}
21    case Some{a}: {==}