proofs/containers/intrusive_doubly_linked_list/history.bend
bend-collections-laws-containers@1.0.0.0 · 72 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/edits.bend as E
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as Logic
5
6
7# The split fields are proof witnesses, not runtime arguments to remove.
8# They name the old ordered sequence independently of the link algorithm.
9type Edit<-N: Data> is Data:
10 Prepend{node: N}
11 RemoveHead{node: N, rest: List<&2,N>}
12 RemoveAfter{prefix: List<&2,N>, previous: N, node: N, suffix: List<&2,N>}
13
14def order(~N: Data, op: Edit<N>, xs: List<&2,N>) -> List<&2,N>:
15 match op:
16 case Prepend{n}: Con{n,xs}
17 case RemoveHead{n,rest}: rest
18 case RemoveAfter{a,p,n,b}: G.append(~N,G.append(~N,a,Con{p,Nil{}}),b)
19
20def step(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, g: G.Graph<N,R,P>, r: R, op: Edit<N>) -> G.Graph<N,R,P>:
21 match op:
22 case Prepend{n}: G.prepend(~N, ~R, ~P,~req,g,r,n)
23 case RemoveHead{n,rest}: G.remove(~N, ~R, ~P, ~eq,g,r,n)
24 case RemoveAfter{a,p,n,b}: G.remove(~N, ~R, ~P, ~eq,g,r,n)
25
26def permitted(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, op: Edit<N>, +xs: List<&2,N>) -> Data:
27 match op:
28 case Prepend{+n}: G.both(G.away(~N,~eq,n,xs),G.both({G.prev(~N, ~R, ~P, ~eq,g,n) == None{} : Maybe<&2,N>},{G.next(~N, ~R, ~P, ~eq,g,n) == None{} : Maybe<&2,N>}))
29 case RemoveHead{n,rest}: {xs == Con{n,rest} : List<&2,N>}
30 case RemoveAfter{a,p,n,b}: {xs == G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}) : List<&2,N>}
31
32def legal(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ops: List<&2,Edit<N>>, +g: G.Graph<N,R,P>, +r: R, +xs: List<&2,N>) -> Data:
33 match ops:
34 case Nil{}: Unit
35 case Con{+op,+rest}: G.both(permitted(~N, ~R, ~P, ~eq,g,op,xs),legal(~N, ~R, ~P, ~eq, ~req,rest,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r,order(~N,op,xs)))
36
37def run(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ops: List<&2,Edit<N>>, g: G.Graph<N,R,P>, +r: R) -> G.Graph<N,R,P>:
38 match ops:
39 case Nil{}: g
40 case Con{op,rest}: run(~N, ~R, ~P, ~eq, ~req,rest,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r)
41
42def orders(~N: Data, ops: List<&2,Edit<N>>, xs: List<&2,N>) -> List<&2,N>:
43 match ops:
44 case Nil{}: xs
45 case Con{op,rest}: orders(~N,rest,order(~N,op,xs))
46
47def step_preserves(~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, +op: Edit<N>, +xs: List<&2,N>, rsame: {req(r,r) == True{} : Bool}, pre: permitted(~N, ~R, ~P, ~eq,g,op,xs), good: G.valid(~N, ~R, ~P, ~eq, ~req,g,r,xs)) -> G.valid(~N, ~R, ~P, ~eq, ~req,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r,order(~N,op,xs)):
48 match op pre:
49 case Prepend{+n} Tuple{away,Tuple{hp,hn}}: E.prepend_preserves(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,xs,rsame,away,hp,good)
50 case RemoveHead{+n,+rest} equation:
51 E.remove_head_preserves(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,rest,rsame,Logic.subst(List<&2,N>,ys => G.valid(~N, ~R, ~P, ~eq, ~req,g,r,ys),xs,Con{n,rest},equation,good))
52 case RemoveAfter{+a,+p,+n,+b} equation:
53 E.remove_nonhead_preserves(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,a,p,b,Logic.subst(List<&2,N>,ys => G.valid(~N, ~R, ~P, ~eq, ~req,g,r,ys),xs,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}),equation,good))
54
55# Induction over any finite legal history, not a bound or enumeration.
56def run_preserves(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +ops: List<&2,Edit<N>>, +g: G.Graph<N,R,P>, +r: R, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, history: legal(~N, ~R, ~P, ~eq, ~req,ops,g,r,xs), good: G.valid(~N, ~R, ~P, ~eq, ~req,g,r,xs)) -> G.valid(~N, ~R, ~P, ~eq, ~req,run(~N, ~R, ~P, ~eq, ~req,ops,g,r),r,orders(~N,ops,xs)):
57 match ops history:
58 case Nil{} _: good
59 case Con{+op,+rest} Tuple{pre,ht}:
60 run_preserves(~N, ~R, ~P, ~eq, ~req,~reflex,rest,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r,order(~N,op,xs),rsame,ht,step_preserves(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,op,xs,rsame,pre,good))
61
62def step_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +op: Edit<N>) -> {G.frame(~N, ~R, ~P,step(~N, ~R, ~P, ~eq, ~req,g,r,op)) == G.frame(~N, ~R, ~P,g) : P}:
63 match op:
64 case Prepend{+n}: E.attach_frame(~N, ~R, ~P,g,r,n,G.head(~N, ~R, ~P,~req,g,r))
65 case RemoveHead{+n,rest}: E.cut_frame(~N, ~R, ~P,g,r,n,G.prev(~N, ~R, ~P, ~eq,g,n),G.next(~N, ~R, ~P, ~eq,g,n))
66 case RemoveAfter{a,p,+n,b}: E.cut_frame(~N, ~R, ~P,g,r,n,G.prev(~N, ~R, ~P, ~eq,g,n),G.next(~N, ~R, ~P, ~eq,g,n))
67
68def run_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +ops: List<&2,Edit<N>>, +g: G.Graph<N,R,P>, +r: R) -> {G.frame(~N, ~R, ~P,run(~N, ~R, ~P, ~eq, ~req,ops,g,r)) == G.frame(~N, ~R, ~P,g) : P}:
69 match ops:
70 case Nil{}: {==}
71 case Con{+op,+rest}:
72 Equal.trans(P,G.frame(~N, ~R, ~P,run(~N, ~R, ~P, ~eq, ~req,rest,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r)),G.frame(~N, ~R, ~P,step(~N, ~R, ~P, ~eq, ~req,g,r,op)),G.frame(~N, ~R, ~P,g),run_frame(~N, ~R, ~P, ~eq, ~req,rest,step(~N, ~R, ~P, ~eq, ~req,g,r,op),r),step_frame(~N, ~R, ~P, ~eq, ~req,g,r,op))