1	import Base
2	import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as S
3	
4	def 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.
11	def 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	
18	def 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}: {==}