proofs/containers/intrusive_doubly_linked_list/proof.bend
bend-collections-laws-containers@1.0.0.0 · 53 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/writes.bend as Writes
3import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as Graph
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/shape.bend as Shape
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/edits.bend as Edits
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/adapter.bend as Adapter
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/history.bend as History
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/array_adapter.bend as ArrayAdapter
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/links.bend as Links
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/frames.bend as Frames
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/example.bend as Example
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/costs.bend as Costs
13import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/main.bend as Contract
14import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
15
16# Checked entry point. The semantic theorems apply to arbitrary identity and
17# payload types through primitive adapter equations. array_adapter discharges
18# all those equations for an actual owned-array representation; history proves
19# arbitrary finite legal edit sequences, not a fixed test bound. links proves the
20# ready-made table src/containers/intrusive_links.bend for EVERY size: its
21# remove and prepend are the model graph's remove and prepend.
22# See docs/INTRUSIVE_LIST.md for theorem signatures and the adapter boundary.
23
24# ---- the contract clauses of spec/containers/intrusive_doubly_linked_list ----
25
26def prepend_valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +away: G.away(~N,~eq,n,xs), +detached: {G.prev(~N,~R,~P,~eq,g,n) == None{} : Maybe<&2,N>}, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,xs)) -> Contract.Prepend.valid(~N,~R,~P,~eq,~req,~reflex,g,r,n,xs,rsame,away,detached,valid):
27 Edits.prepend_preserves(~N,~R,~P,~eq,~req,~reflex,g,r,n,xs,rsame,away,detached,valid)
28
29def prepend_other_roots(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +x: R, +neq: {req(r,x) == False{} : Bool}) -> Contract.Prepend.other_roots(~N,~R,~P,~req,g,r,n,x,neq):
30 Frames.prepend_other_root(~N,~R,~P,~req,g,r,n,G.head(~N,~R,~P,~req,g,r),x,neq)
31
32def prepend_frame(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N) -> Contract.Prepend.frame(~N,~R,~P,~req,g,r,n):
33 Edits.attach_frame(~N,~R,~P,g,r,n,G.head(~N,~R,~P,~req,g,r))
34
35def delete_first(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,Con{n,xs})) -> Contract.Delete.first(~N,~R,~P,~eq,~req,~reflex,g,r,n,xs,rsame,valid):
36 Edits.remove_head_preserves(~N,~R,~P,~eq,~req,~reflex,g,r,n,xs,rsame,valid)
37
38def delete_inner(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +a: List<&2,N>, +p: N, +b: List<&2,N>, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}))) -> Contract.Delete.inner(~N,~R,~P,~eq,~req,~reflex,g,r,n,a,p,b,valid):
39 Edits.remove_nonhead_preserves(~N,~R,~P,~eq,~req,~reflex,g,r,n,a,p,b,valid)
40
41def delete_other_roots(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +x: R, +neq: {req(r,x) == False{} : Bool}) -> Contract.Delete.other_roots(~N,~R,~P,~eq,~req,g,r,n,x,neq):
42 Frames.remove_other_root(~N,~R,~P,~req,g,r,n,G.prev(~N,~R,~P,~eq,g,n),G.next(~N,~R,~P,~eq,g,n),x,neq)
43
44def delete_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N) -> Contract.Delete.frame(~N,~R,~P,~eq,g,r,n):
45 Edits.cut_frame(~N,~R,~P,g,r,n,G.prev(~N,~R,~P,~eq,g,n),G.next(~N,~R,~P,~eq,g,n))
46
47def delete_detached(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +same: {eq(n,n) == True{} : Bool}) -> Contract.Delete.detached(~N,~R,~P,~eq,g,r,n,same):
48 Frames.removed_next(~N,~R,~P,~eq,g,r,n,G.prev(~N,~R,~P,~eq,g,n),G.next(~N,~R,~P,~eq,g,n),same)
49
50def first_head(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +xs: List<&2,N>, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,xs)) -> Contract.First.head(~N,~R,~P,~eq,~req,g,r,xs,valid):
51 match valid:
52 case Tuple{un, Tuple{+h, s}}:
53 h