1 import Base 2 import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as Spec 3 import ./fold.bend as Fold 4 import ./clear.bend as Clear 5 import ../../lib/nat.bend as NN 6 import ../../../src/containers/internal/intrusive_list.bend as L 7 import ../../../src/containers/types/intrusive_doubly_linked_list.bend as E 8 9 # Quantified edit-program refinement over the ACTUAL public operations. 10 # Read-result premises describe primitive accessor observations, not list 11 # correctness or the result being proved. Setters are arbitrary: the theorem 12 # preserves their order, identity and distinction, including their effects. 13 # This does not certify application accessors, handle validity, races, the 14 # compiler, or every callback-driven traversal. See the validation document. 15 16 def remove_known(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> 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>) -> {L.remove_2(~S, ~N, ~I, ~next, ~prev, ~sn, ~sp, ~sh, i, node, after, (s2, before)) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.remove(N, I, i, node, before, after), s2) : S}: 17 match before after: 18 case None{} None{}: {==} 19 case None{} Some{q}: {==} 20 case Some{p} None{}: {==} 21 case Some{p} Some{q}: {==} 22 23 def remove_writes(~S: Type, ~N: Data, ~I: Data, ~next: S -> N -> S & Maybe<&2, N>, ~prev: S -> N -> 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) : S & Maybe<&2, N>}, hp: {prev(s1, node) == (s2, before) : S & Maybe<&2, N>}) -> {L.remove(~S, ~N, ~I, ~next, ~prev, ~sn, ~sp, ~sh, s, i, node) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.remove(N, I, i, node, before, after), s2) : S}: 24 %Equal.sym(S & Maybe<&2, N>, next(s, node), (s1, after), hn) : {L.remove_1(~S, ~N, ~I, ~next, ~prev, ~sn, ~sp, ~sh, i, node, _) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.remove(N, I, i, node, before, after), s2) : S} 25 %Equal.sym(S & Maybe<&2, N>, prev(s1, node), (s2, before), hp) : {L.remove_2(~S, ~N, ~I, ~next, ~prev, ~sn, ~sp, ~sh, i, node, after, _) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.remove(N, I, i, node, before, after), s2) : S} 26 remove_known(~S, ~N, ~I, ~next, ~prev, ~sn, ~sp, ~sh, ~sf, s2, i, node, before, after) 27 28 def prepend_known(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get: S -> H -> 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>) -> {L.prepend_as_1(~S, ~N, ~H, ~I, ~get, ~sn, ~sp, ~sf, i, node, (s1, head)) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.prepend(N, I, i, node, head), s1) : S}: 29 match head: 30 case None{}: {==} 31 case Some{q}: {==} 32 33 def prepend_writes(~S: Type, ~N: Data, ~H: Data, ~I: Data, ~get: S -> H -> 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) : S & Maybe<&2, N>}) -> {L.prepend_as(~S, ~N, ~H, ~I, ~get, ~sn, ~sp, ~sf, s, h, i, node) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.prepend(N, I, i, node, head), s1) : S}: 34 %Equal.sym(S & Maybe<&2, N>, get(s, h), (s1, head), hg) : {L.prepend_as_1(~S, ~N, ~H, ~I, ~get, ~sn, ~sp, ~sf, i, node, _) == Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, Spec.prepend(N, I, i, node, head), s1) : S} 35 prepend_known(~S, ~N, ~H, ~I, ~get, ~sn, ~sp, ~sh, ~sf, s1, i, node, head) 36 37 def pool_then_next(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~sn: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> S & N, c: C, r: S & E.Pool) -> S & (E.Pool & N): 38 (s, pool) = r 39 L.pool_next(~S, ~N, ~C, ~next, ~sn, ~make, s, pool, c) 40 41 def pool_lifo(~S: Type, ~N: Data, ~C: Data, ~next: S -> N -> S & Maybe<&2, N>, ~sn: S -> N -> Maybe<&2, N> -> S, ~make: S -> C -> 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) : S & Maybe<&2, N>}) -> {pool_then_next(~S, ~N, ~C, ~next, ~sn, ~make, c, L.pool_free(~S, ~N, ~sn, s, E.Pool{head, count}, node)) == (sn(sn(s, node, head), node, None{}), (E.Pool{head, count}, node)) : S & (E.Pool & N)}: 42 %Equal.sym(S & Maybe<&2, N>, next(sn(s, node, head), node), (sn(s, node, head), head), read_back) : {L.pool_take_1(~S, ~N, ~C, ~next, ~sn, ~make, node, 1n+count, _) == (sn(sn(s, node, head), node, None{}), (E.Pool{head, count}, node)) : S & (E.Pool & N)} 43 Equal.cong(Nat, S & (E.Pool & N), k => (sn(sn(s, node, head), node, None{}), (E.Pool{head, k}, node)), Nat.sub(count, 0n), count, NN.sub_zero(count)) 44 45 def default_node(~N: Data, ~V: Data, +v: V) -> {L.new_node(~N, ~V, v) == E.Node{None{}, None{}, v} : E.DefaultNode}: 46 {==}