proofs/containers/intrusive_doubly_linked_list/adapter.bend
bend-collections-laws-containers@1.0.0.0 · 63 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/writes.bend as W
5import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_doubly_linked_list.bend as L
6
7
8# A shadow can contain proof-only history. real need not be injective: two
9# finite-map logs may denote the same physical array. This is a simulation
10# relation, not an impossible requirement that arrays retain the write log.
11def apply(~N: Data, ~R: Data, ~P: Data, ~I: Data, ~root: I -> R, g: G.Graph<N,R,P>, e: Spec.Edit<N,I>) -> G.Graph<N,R,P>:
12 match e:
13 case Spec.Next{n,m}: G.sn(~N, ~R, ~P,g,n,m)
14 case Spec.Prev{n,m}: G.sp(~N, ~R, ~P,g,n,m)
15 case Spec.Head{i,m}: G.sh(~N, ~R, ~P,g,root(i),m)
16 case Spec.Nonempty{i,n}: G.sh(~N, ~R, ~P,g,root(i),Some{n})
17
18def run(~N: Data, ~R: Data, ~P: Data, ~I: Data, ~root: I -> R, es: List<&2,Spec.Edit<N,I>>, g: G.Graph<N,R,P>) -> G.Graph<N,R,P>:
19 match es:
20 case Nil{}: g
21 case Con{e,rest}: run(~N, ~R, ~P, ~I, ~root,rest,apply(~N, ~R, ~P, ~I, ~root,g,e))
22
23# Only primitive setter equations are premises. They can be discharged for
24# each reachable, in-bounds state; no universal law about invalid IDs or an
25# out-of-bounds array operation is required. No list postcondition appears.
26def laws(~S: Type, ~N: Data, ~R: Data, ~P: Data, ~I: Data, ~real: G.Graph<N,R,P> -> S, ~root: I -> R, ~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, es: List<&2,Spec.Edit<N,I>>, +g: G.Graph<N,R,P>) -> Data:
27 match es:
28 case Nil{}: Unit
29 case Con{+e,+rest}: G.both({Spec.apply(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,real(g),e) == real(apply(~N, ~R, ~P, ~I, ~root,g,e)) : S},laws(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,rest,apply(~N, ~R, ~P, ~I, ~root,g,e)))
30
31def program_refines(~S: Type, ~N: Data, ~R: Data, ~P: Data, ~I: Data, ~real: G.Graph<N,R,P> -> S, ~root: I -> R, ~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, +es: List<&2,Spec.Edit<N,I>>, +g: G.Graph<N,R,P>, hs: laws(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,es,g)) -> {Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,es,real(g)) == real(run(~N, ~R, ~P, ~I, ~root,es,g)) : S}:
32 match es hs:
33 case Nil{} _: {==}
34 case Con{+e,+rest} Tuple{he,ht}:
35 %Equal.sym(S,Spec.apply(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,real(g),e),real(apply(~N, ~R, ~P, ~I, ~root,g,e)),he) : {Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,rest,_) == real(run(~N, ~R, ~P, ~I, ~root,rest,apply(~N, ~R, ~P, ~I, ~root,g,e))) : S}
36 program_refines(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,rest,apply(~N, ~R, ~P, ~I, ~root,g,e),ht)
37
38def remove_program(~N: Data, ~R: Data, ~P: Data, ~I: Data, ~root: I -> R, +g: G.Graph<N,R,P>, +i: I, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>) -> {run(~N, ~R, ~P, ~I, ~root,Spec.remove(N,I,i,n,p,q),g) == G.cut(~N, ~R, ~P,g,root(i),n,p,q) : G.Graph<N,R,P>}:
39 match p q:
40 case None{} None{}: {==}
41 case None{} Some{x}: {==}
42 case Some{x} None{}: {==}
43 case Some{x} Some{y}: {==}
44
45def prepend_program(~N: Data, ~R: Data, ~P: Data, ~I: Data, ~root: I -> R, +g: G.Graph<N,R,P>, +i: I, +n: N, +h: Maybe<&2,N>) -> {run(~N, ~R, ~P, ~I, ~root,Spec.prepend(N,I,i,n,h),g) == G.attach(~N, ~R, ~P,g,root(i),n,h) : G.Graph<N,R,P>}:
46 match h:
47 case None{}: {==}
48 case Some{x}: {==}
49
50
51# The source/model connection reaches the actual exported remove function.
52def remove_refines(~S: Type, ~N: Data, ~R: Data, ~P: Data, ~I: Data, ~real: G.Graph<N,R,P> -> S, ~root: I -> R, ~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, ~eq: N -> N -> Bool, ~next: S -> N -> S & Maybe<&2,N>, ~prev: S -> N -> S & Maybe<&2,N>, +g: G.Graph<N,R,P>, +i: I, +n: N, hn: {next(real(g),n) == (real(g),G.next(~N, ~R, ~P,~eq,g,n)) : S & Maybe<&2,N>}, hp: {prev(real(g),n) == (real(g),G.prev(~N, ~R, ~P,~eq,g,n)) : S & Maybe<&2,N>}, hs: laws(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),g)) -> {L.remove(~S,~N,~I,~next,~prev,~sn,~sp,~sh,real(g),i,n) == real(G.remove(~N, ~R, ~P,~eq,g,root(i),n)) : S}:
53 Equal.trans(S,L.remove(~S,~N,~I,~next,~prev,~sn,~sp,~sh,real(g),i,n),Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),real(g)),real(G.remove(~N, ~R, ~P,~eq,g,root(i),n)),
54 W.remove_writes(~S,~N,~I,~next,~prev,~sn,~sp,~sh,~sf,real(g),real(g),real(g),i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n),hn,hp),
55 Equal.trans(S,Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),real(g)),real(run(~N, ~R, ~P, ~I, ~root,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),g)),real(G.remove(~N, ~R, ~P,~eq,g,root(i),n)),program_refines(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),g,hs),Equal.cong(G.Graph<N,R,P>,S,real,run(~N, ~R, ~P, ~I, ~root,Spec.remove(N,I,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),g),G.cut(~N, ~R, ~P,g,root(i),n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)),remove_program(~N, ~R, ~P, ~I, ~root,g,i,n,G.prev(~N, ~R, ~P,~eq,g,n),G.next(~N, ~R, ~P,~eq,g,n)))))
56
57
58# H and I remain distinct. The read equation expresses coherence of the
59# particular reader/writer contexts; it does not force identical types.
60def prepend_refines(~S: Type, ~N: Data, ~R: Data, ~P: Data, ~I: Data, ~real: G.Graph<N,R,P> -> S, ~root: I -> R, ~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, ~H: Data, ~req: R -> R -> Bool, ~get: S -> H -> S & Maybe<&2,N>, +g: G.Graph<N,R,P>, +h: H, +i: I, +n: N, hg: {get(real(g),h) == (real(g),G.head(~N, ~R, ~P,~req,g,root(i))) : S & Maybe<&2,N>}, hs: laws(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),g)) -> {L.prepend_as(~S,~N,~H,~I,~get,~sn,~sp,~sf,real(g),h,i,n) == real(G.prepend(~N, ~R, ~P,~req,g,root(i),n)) : S}:
61 Equal.trans(S,L.prepend_as(~S,~N,~H,~I,~get,~sn,~sp,~sf,real(g),h,i,n),Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),real(g)),real(G.prepend(~N, ~R, ~P,~req,g,root(i),n)),
62 W.prepend_writes(~S,~N,~H,~I,~get,~sn,~sp,~sh,~sf,real(g),real(g),h,i,n,G.head(~N, ~R, ~P,~req,g,root(i)),hg),
63 Equal.trans(S,Spec.run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),real(g)),real(run(~N, ~R, ~P, ~I, ~root,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),g)),real(G.prepend(~N, ~R, ~P,~req,g,root(i),n)),program_refines(~S, ~N, ~R, ~P, ~I, ~real, ~root, ~sn, ~sp, ~sh, ~sf,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),g,hs),Equal.cong(G.Graph<N,R,P>,S,real,run(~N, ~R, ~P, ~I, ~root,Spec.prepend(N,I,i,n,G.head(~N, ~R, ~P,~req,g,root(i))),g),G.attach(~N, ~R, ~P,g,root(i),n,G.head(~N, ~R, ~P,~req,g,root(i))),prepend_program(~N, ~R, ~P, ~I, ~root,g,i,n,G.head(~N, ~R, ~P,~req,g,root(i))))))