proofs/containers/intrusive_doubly_linked_list/array_adapter.bend
bend-collections-laws-containers@1.0.0.0 · 213 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/proofs/containers/intrusive_doubly_linked_list/adapter.bend as A
4import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/history.bend as H
6import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_doubly_linked_list.bend as L
7
8# A concrete owned-array witness for the adapter laws, for every graph over
9# these nominal IDs, every payload P, and every primitive write. This is not
10# a sampled test and it does not claim to prove arbitrary user adapters.
11type Node is Data:
12 A{}
13 B{}
14 C{}
15 D{}
16
17type Root is Data:
18 Ready{}
19 Waiting{}
20
21type Reader is Data:
22 Reader{root: Root}
23
24type Writer is Data:
25 Writer{root: Root}
26
27type Store<-P: Data> is Type:
28 Store{cells: Array<Maybe<&2,Node>>, payload: P}
29
30def eq(a: Node, b: Node) -> Bool:
31 match a b:
32 case A{} A{}: True{}
33 case B{} B{}: True{}
34 case C{} C{}: True{}
35 case D{} D{}: True{}
36 case _ _: False{}
37
38def req(a: Root, b: Root) -> Bool:
39 match a b:
40 case Ready{} Ready{}: True{}
41 case Waiting{} Waiting{}: True{}
42 case _ _: False{}
43
44def reflex(+n: Node) -> {eq(n,n) == True{} : Bool}:
45 match n:
46 case A{}: {==}
47 case B{}: {==}
48 case C{}: {==}
49 case D{}: {==}
50
51def root(i: Writer) -> Root:
52 Writer{r} = i
53 r
54
55def ni(n: Node) -> U32:
56 match n:
57 case A{}: 0
58 case B{}: 1
59 case C{}: 2
60 case D{}: 3
61
62def pi(n: Node) -> U32:
63 match n:
64 case A{}: 4
65 case B{}: 5
66 case C{}: 6
67 case D{}: 7
68
69def ri(r: Root) -> U32:
70 match r:
71 case Ready{}: 8
72 case Waiting{}: 9
73
74def real(~P: Data, +g: G.Graph<Node,Root,P>) -> Store<P>:
75 Store{ANode{
76 ANode{ANode{ANode{ALeaf{G.next(~Node,~Root,~P,~eq,g,A{})},ALeaf{G.next(~Node,~Root,~P,~eq,g,B{})}},ANode{ALeaf{G.next(~Node,~Root,~P,~eq,g,C{})},ALeaf{G.next(~Node,~Root,~P,~eq,g,D{})}}},
77 ANode{ANode{ALeaf{G.prev(~Node,~Root,~P,~eq,g,A{})},ALeaf{G.prev(~Node,~Root,~P,~eq,g,B{})}},ANode{ALeaf{G.prev(~Node,~Root,~P,~eq,g,C{})},ALeaf{G.prev(~Node,~Root,~P,~eq,g,D{})}}}},
78 ANode{ANode{ANode{ALeaf{G.head(~Node,~Root,~P,~req,g,Ready{})},ALeaf{G.head(~Node,~Root,~P,~req,g,Waiting{})}},ANode{ALeaf{None{}},ALeaf{None{}}}},ANode{ANode{ALeaf{None{}},ALeaf{None{}}},ANode{ALeaf{None{}},ALeaf{None{}}}}}},G.frame(~Node,~Root,~P,g)}
79
80def read_result(~P: Data, f: P, r: Array<Maybe<&2,Node>> & Maybe<&2,Node>) -> Store<P> & Maybe<&2,Node>:
81 (cells,n) = r
82 (Store{cells,f},n)
83
84def read(~P: Data, s: Store<P>, i: U32) -> Store<P> & Maybe<&2,Node>:
85 Store{cells,f} = s
86 read_result(~P,f,Array.get(Maybe<&2,Node>,cells,i))
87
88def write(~P: Data, s: Store<P>, i: U32, v: Maybe<&2,Node>) -> Store<P>:
89 Store{cells,f} = s
90 Store{Array.set(Maybe<&2,Node>,cells,i,v),f}
91
92def next(~P: Data, s: Store<P>, n: Node) -> Store<P> & Maybe<&2,Node>:
93 read(~P,s,ni(n))
94
95def prev(~P: Data, s: Store<P>, n: Node) -> Store<P> & Maybe<&2,Node>:
96 read(~P,s,pi(n))
97
98def head(~P: Data, s: Store<P>, h: Reader) -> Store<P> & Maybe<&2,Node>:
99 Reader{r} = h
100 read(~P,s,ri(r))
101
102def sn(~P: Data, s: Store<P>, n: Node, v: Maybe<&2,Node>) -> Store<P>:
103 write(~P,s,ni(n),v)
104
105def sp(~P: Data, s: Store<P>, n: Node, v: Maybe<&2,Node>) -> Store<P>:
106 write(~P,s,pi(n),v)
107
108def sh(~P: Data, s: Store<P>, i: Writer, v: Maybe<&2,Node>) -> Store<P>:
109 write(~P,s,ri(root(i)),v)
110
111def sf(~P: Data, s: Store<P>, i: Writer, n: Node) -> Store<P>:
112 sh(~P,s,i,Some{n})
113
114def next_law(~P: Data, +g: G.Graph<Node,Root,P>, +n: Node) -> {next(~P,real(~P,g),n) == (real(~P,g),G.next(~Node,~Root,~P,~eq,g,n)) : Store<P> & Maybe<&2,Node>}:
115 match n:
116 case A{}: {==}
117 case B{}: {==}
118 case C{}: {==}
119 case D{}: {==}
120
121def prev_law(~P: Data, +g: G.Graph<Node,Root,P>, +n: Node) -> {prev(~P,real(~P,g),n) == (real(~P,g),G.prev(~Node,~Root,~P,~eq,g,n)) : Store<P> & Maybe<&2,Node>}:
122 match n:
123 case A{}: {==}
124 case B{}: {==}
125 case C{}: {==}
126 case D{}: {==}
127
128def head_law(~P: Data, +g: G.Graph<Node,Root,P>, +r: Root) -> {head(~P,real(~P,g),Reader{r}) == (real(~P,g),G.head(~Node,~Root,~P,~req,g,r)) : Store<P> & Maybe<&2,Node>}:
129 match r:
130 case Ready{}: {==}
131 case Waiting{}: {==}
132
133def sn_law(~P: Data, +g: G.Graph<Node,Root,P>, +n: Node, +v: Maybe<&2,Node>) -> {sn(~P,real(~P,g),n,v) == real(~P,G.sn(~Node,~Root,~P,g,n,v)) : Store<P>}:
134 match g n:
135 case G.Graph{ns,ps,rs,f} A{}: {==}
136 case G.Graph{ns,ps,rs,f} B{}: {==}
137 case G.Graph{ns,ps,rs,f} C{}: {==}
138 case G.Graph{ns,ps,rs,f} D{}: {==}
139
140def sp_law(~P: Data, +g: G.Graph<Node,Root,P>, +n: Node, +v: Maybe<&2,Node>) -> {sp(~P,real(~P,g),n,v) == real(~P,G.sp(~Node,~Root,~P,g,n,v)) : Store<P>}:
141 match g n:
142 case G.Graph{ns,ps,rs,f} A{}: {==}
143 case G.Graph{ns,ps,rs,f} B{}: {==}
144 case G.Graph{ns,ps,rs,f} C{}: {==}
145 case G.Graph{ns,ps,rs,f} D{}: {==}
146
147def sh_law(~P: Data, +g: G.Graph<Node,Root,P>, +i: Writer, +v: Maybe<&2,Node>) -> {sh(~P,real(~P,g),i,v) == real(~P,G.sh(~Node,~Root,~P,g,root(i),v)) : Store<P>}:
148 match g i:
149 case G.Graph{ns,ps,rs,f} Writer{Ready{}}: {==}
150 case G.Graph{ns,ps,rs,f} Writer{Waiting{}}: {==}
151
152
153
154def write_law(~P: Data, +g: G.Graph<Node,Root,P>, +e: Spec.Edit<Node,Writer>) -> {Spec.apply(~Store<P>, ~Node, ~Writer, ~(s => n => v => sn(~P,s,n,v)), ~(s => n => v => sp(~P,s,n,v)), ~(s => i => v => sh(~P,s,i,v)), ~(s => i => n => sf(~P,s,i,n)),real(~P,g),e) == real(~P,A.apply(~Node, ~Root, ~P, ~Writer, ~root,g,e)) : Store<P>}:
155 match e:
156 case Spec.Next{n,v}: sn_law(~P,g,n,v)
157 case Spec.Prev{n,v}: sp_law(~P,g,n,v)
158 case Spec.Head{i,v}: sh_law(~P,g,i,v)
159 case Spec.Nonempty{i,n}: sh_law(~P,g,i,Some{n})
160
161def write_laws(~P: Data, +es: List<&2,Spec.Edit<Node,Writer>>, +g: G.Graph<Node,Root,P>) -> A.laws(~Store<P>, ~Node, ~Root, ~P, ~Writer, ~(g => real(~P,g)), ~root, ~(s => n => v => sn(~P,s,n,v)), ~(s => n => v => sp(~P,s,n,v)), ~(s => i => v => sh(~P,s,i,v)), ~(s => i => n => sf(~P,s,i,n)),es,g):
162 match es:
163 case Nil{}: Unit{}
164 case Con{+e,+rest}: (write_law(~P,g,e),write_laws(~P,rest,A.apply(~Node, ~Root, ~P, ~Writer, ~root,g,e)))
165
166def remove(~P: Data, s: Store<P>, r: Root, n: Node) -> Store<P>:
167 L.remove(~Store<P>,~Node,~Writer,~(s => n => next(~P,s,n)),~(s => n => prev(~P,s,n)),~(s => n => v => sn(~P,s,n,v)),~(s => n => v => sp(~P,s,n,v)),~(s => i => v => sh(~P,s,i,v)),s,Writer{r},n)
168
169def prepend(~P: Data, s: Store<P>, +r: Root, n: Node) -> Store<P>:
170 L.prepend_as(~Store<P>,~Node,~Reader,~Writer,~(s => h => head(~P,s,h)),~(s => n => v => sn(~P,s,n,v)),~(s => n => v => sp(~P,s,n,v)),~(s => i => n => sf(~P,s,i,n)),s,Reader{r},Writer{r},n)
171
172def remove_refines(~P: Data, +g: G.Graph<Node,Root,P>, +r: Root, +n: Node) -> {remove(~P,real(~P,g),r,n) == real(~P,G.remove(~Node, ~Root, ~P,~eq,g,r,n)) : Store<P>}:
173 A.remove_refines(~Store<P>, ~Node, ~Root, ~P, ~Writer, ~(g => real(~P,g)), ~root, ~(s => n => v => sn(~P,s,n,v)), ~(s => n => v => sp(~P,s,n,v)), ~(s => i => v => sh(~P,s,i,v)), ~(s => i => n => sf(~P,s,i,n)),~eq,~(s => n => next(~P,s,n)),~(s => n => prev(~P,s,n)),g,Writer{r},n,next_law(~P,g,n),prev_law(~P,g,n),write_laws(~P,Spec.remove(Node,Writer,Writer{r},n,G.prev(~Node, ~Root, ~P,~eq,g,n),G.next(~Node, ~Root, ~P,~eq,g,n)),g))
174
175def prepend_refines(~P: Data, +g: G.Graph<Node,Root,P>, +r: Root, +n: Node) -> {prepend(~P,real(~P,g),r,n) == real(~P,G.prepend(~Node, ~Root, ~P,~req,g,r,n)) : Store<P>}:
176 A.prepend_refines(~Store<P>, ~Node, ~Root, ~P, ~Writer, ~(g => real(~P,g)), ~root, ~(s => n => v => sn(~P,s,n,v)), ~(s => n => v => sp(~P,s,n,v)), ~(s => i => v => sh(~P,s,i,v)), ~(s => i => n => sf(~P,s,i,n)),~Reader,~req,~(s => h => head(~P,s,h)),g,Reader{r},Writer{r},n,head_law(~P,g,r),write_laws(~P,Spec.prepend(Node,Writer,Writer{r},n,G.head(~Node, ~Root, ~P,~req,g,r)),g))
177
178def step(~P: Data, s: Store<P>, r: Root, op: H.Edit<Node>) -> Store<P>:
179 match op:
180 case H.Prepend{n}: prepend(~P,s,r,n)
181 case H.RemoveHead{n,rest}: remove(~P,s,r,n)
182 case H.RemoveAfter{a,p,n,b}: remove(~P,s,r,n)
183
184def run(~P: Data, ops: List<&2,H.Edit<Node>>, s: Store<P>, +r: Root) -> Store<P>:
185 match ops:
186 case Nil{}: s
187 case Con{op,rest}: run(~P,rest,step(~P,s,r,op),r)
188
189def step_refines(~P: Data, +op: H.Edit<Node>, +g: G.Graph<Node,Root,P>, +r: Root) -> {step(~P,real(~P,g),r,op) == real(~P,H.step(~Node, ~Root, ~P,~eq,~req,g,r,op)) : Store<P>}:
190 match op:
191 case H.Prepend{n}: prepend_refines(~P,g,r,n)
192 case H.RemoveHead{n,rest}: remove_refines(~P,g,r,n)
193 case H.RemoveAfter{a,p,n,b}: remove_refines(~P,g,r,n)
194
195# Every actual array-backed history refines the independent graph execution.
196# Combine with history.run_preserves for arbitrary-length legal sequences.
197def run_refines(~P: Data, +ops: List<&2,H.Edit<Node>>, +g: G.Graph<Node,Root,P>, +r: Root) -> {run(~P,ops,real(~P,g),r) == real(~P,H.run(~Node, ~Root, ~P,~eq,~req,ops,g,r)) : Store<P>}:
198 match ops:
199 case Nil{}: {==}
200 case Con{+op,+rest}:
201 %Equal.sym(Store<P>,step(~P,real(~P,g),r,op),real(~P,H.step(~Node, ~Root, ~P,~eq,~req,g,r,op)),step_refines(~P,op,g,r)) : {run(~P,rest,_,r) == real(~P,H.run(~Node, ~Root, ~P,~eq,~req,rest,H.step(~Node, ~Root, ~P,~eq,~req,g,r,op),r)) : Store<P>}
202 run_refines(~P,rest,H.step(~Node, ~Root, ~P,~eq,~req,g,r,op),r)
203
204def root_reflex(+r: Root) -> {req(r,r) == True{} : Bool}:
205 match r:
206 case Ready{}: {==}
207 case Waiting{}: {==}
208
209# End-to-end corollary: the actual public functions return the represented
210# final sequence, all its bidirectional links remain valid, and every payload
211# in P (which can also hold another association) is preserved.
212def histories_correct(~P: Data, +ops: List<&2,H.Edit<Node>>, +g: G.Graph<Node,Root,P>, +r: Root, +xs: List<&2,Node>, legal: H.legal(~Node, ~Root, ~P,~eq,~req,ops,g,r,xs), initial: G.valid(~Node, ~Root, ~P,~eq,~req,g,r,xs)) -> G.both({run(~P,ops,real(~P,g),r) == real(~P,H.run(~Node, ~Root, ~P,~eq,~req,ops,g,r)) : Store<P>},G.both(G.valid(~Node, ~Root, ~P,~eq,~req,H.run(~Node, ~Root, ~P,~eq,~req,ops,g,r),r,H.orders(~Node,ops,xs)),{G.frame(~Node, ~Root, ~P,H.run(~Node, ~Root, ~P,~eq,~req,ops,g,r)) == G.frame(~Node, ~Root, ~P,g) : P})):
213 (run_refines(~P,ops,g,r),(H.run_preserves(~Node, ~Root, ~P,~eq,~req,~(x => reflex(x)),ops,g,r,xs,root_reflex(r),legal,initial),H.run_frame(~Node, ~Root, ~P,~eq,~req,ops,g,r)))