proofs/containers/queue/steps.bend
bend-collections-laws-containers@1.0.0.0 · 140 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/queue.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/queue.bend as Q
8import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as E
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/state.bend as ST
10
11# Every public queue operation, including the errors (dequeue/peek on an
12# empty queue: Fail{EmptyQueue}, queue unchanged), refines the spec step.
13
14def StepOK(~T: Data, sh: ST.Shadow<T>, op: E.Op<T>) -> Type:
15 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {Q.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : Q.Queue<T> & E.Obs<T>} & {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs<T>}>>
16
17def mk(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, sh2: ST.Shadow<T>, o: E.Obs<T>, e1: {Q.step(~T, ST.real(T, sh), op) == (ST.real(T, sh2), o) : Q.Queue<T> & E.Obs<T>}, e2: {(ST.model(T, sh2), o) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs<T>}) -> StepOK(~T, sh, op):
18 (sh2, (o, (e1, e2)))
19
20# ---- ready: reverse the back into an empty front ----
21
22def is_nil(-T: Data, xs: List<&2, T>) -> Bool:
23 match xs:
24 case Nil{}:
25 True{}
26 case Con{h, t}:
27 False{}
28
29# the front can be read: nonempty, or the queue is empty
30def rdy(-T: Data, sh: ST.Shadow<T>) -> Bool:
31 match sh:
32 case ST.Sh{Nil{}, b}:
33 is_nil(T, b)
34 case ST.Sh{Con{x, f}, b}:
35 True{}
36
37def rdy_nil_back(-T: Data, +m: List<&2, T>) -> {rdy(T, ST.Sh{m, Nil{}}) == True{} : Bool}:
38 match m:
39 case Nil{}:
40 {==}
41 case Con{x, t}:
42 {==}
43
44def Ready(~T: Data, sh: ST.Shadow<T>) -> Type:
45 Sigma<&1, &1, ST.Shadow<T>, sh1 => {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue<T>} & ({ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>} & {rdy(T, sh1) == True{} : Bool})>
46
47def ready(~T: Data, +sh: ST.Shadow<T>) -> Ready(~T, sh):
48 match sh:
49 case ST.Sh{Con{x, f}, b}:
50 (ST.Sh{Con{x, f}, b}, ({==}, ({==}, {==})))
51 case ST.Sh{Nil{}, +b}:
52 +rb = SC.reverse(T, b)
53 +en = Equal.sym(Nat, Nat.add(SC.length(T, rb), 0n), SC.length(T, b), Equal.trans(Nat, Nat.add(SC.length(T, rb), 0n), SC.length(T, rb), SC.length(T, b), N.add_zero(SC.length(T, rb)), LL.length_rev(T, b)))
54 +e1 = Equal.cong(List<&2, T>, Q.Queue<T>, z => Q.QU{z, Nil{}, SC.length(T, b)}, List.reverse(&2, T, b), rb, LL.base_rev(T, b))
55 +e2 = Equal.cong(Nat, Q.Queue<T>, z => Q.QU{rb, Nil{}, z}, SC.length(T, b), Nat.add(SC.length(T, rb), 0n), en)
56 (ST.Sh{rb, Nil{}}, (Equal.trans(Q.Queue<T>, Q.QU{List.reverse(&2, T, b), Nil{}, SC.length(T, b)}, Q.QU{rb, Nil{}, SC.length(T, b)}, ST.real(T, ST.Sh{rb, Nil{}}), e1, e2), (LL.append_nil(T, rb), rdy_nil_back(T, rb))))
57
58# ---- reading the front of a readied shadow ----
59
60def Read(~T: Data, sh: ST.Shadow<T>, r: Q.Queue<T> & E.Obs<T>, spec: List<&2, T> & E.Obs<T>) -> Type:
61 Sigma<&1, &1, ST.Shadow<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {r == (ST.real(T, sh2), o) : Q.Queue<T> & E.Obs<T>} & {(ST.model(T, sh2), o) == spec : List<&2, T> & E.Obs<T>}>>
62
63def dequeue_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {rdy(T, sh) == True{} : Bool}) -> Read(~T, sh, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh))), S.dequeue(T, ST.model(T, sh))):
64 match sh:
65 case ST.Sh{Con{+x, +t}, +b}:
66 +e = Equal.cong(Nat, Q.Queue<T>, z => Q.QU{t, b, z}, Nat.sub(Nat.add(SC.length(T, Con{x, t}), SC.length(T, b)), 1n), Nat.add(SC.length(T, t), SC.length(T, b)), N.sub_zero(Nat.add(SC.length(T, t), SC.length(T, b))))
67 (ST.Sh{t, b}, (E.OItem{Done{x}}, (Equal.cong(Q.Queue<T>, Q.Queue<T> & E.Obs<T>, q => (q, E.OItem{Done{x}}), Q.QU{t, b, Nat.sub(Nat.add(SC.length(T, Con{x, t}), SC.length(T, b)), 1n)}, ST.real(T, ST.Sh{t, b}), e), {==})))
68 case ST.Sh{Nil{}, Nil{}}:
69 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyQueue{}}}, ({==}, {==})))
70 case ST.Sh{Nil{}, Con{y, t}}:
71 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), S.dequeue(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}}))), L.false_true(hr))
72
73def peek_ready(~T: Data, +sh: ST.Shadow<T>, +hr: {rdy(T, sh) == True{} : Bool}) -> Read(~T, sh, Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh))), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))})):
74 match sh:
75 case ST.Sh{Con{x, t}, b}:
76 (ST.Sh{Con{x, t}, b}, (E.OItem{Done{x}}, ({==}, {==})))
77 case ST.Sh{Nil{}, Nil{}}:
78 (ST.Sh{Nil{}, Nil{}}, (E.OItem{Fail{E.EmptyQueue{}}}, ({==}, {==})))
79 case ST.Sh{Nil{}, Con{y, t}}:
80 Empty.absurd(Read(~T, ST.Sh{Nil{}, Con{y, t}}, Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, ST.Sh{Nil{}, Con{y, t}}))), (ST.model(T, ST.Sh{Nil{}, Con{y, t}}), E.OItem{S.item(T, SC.head(T, ST.model(T, ST.Sh{Nil{}, Con{y, t}})))})), L.false_true(hr))
81
82def dq_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh1))), S.dequeue(T, ST.model(T, sh1)))) -> StepOK(~T, sh, E.Dequeue{}):
83 match rd:
84 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
85 mk(~T, sh, E.Dequeue{}, sh2, o,
86 Equal.trans(Q.Queue<T> & E.Obs<T>, Q.obs_item(~T, Q.dequeue_ready(~T, Q.ready(~T, ST.real(T, sh)))), Q.obs_item(~T, Q.dequeue_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(Q.Queue<T>, Q.Queue<T> & E.Obs<T>, d => Q.obs_item(~T, Q.dequeue_ready(~T, d)), Q.ready(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
87 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), S.dequeue(T, ST.model(T, sh1)), S.dequeue(T, ST.model(T, sh)), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => S.dequeue(T, z), ST.model(T, sh1), ST.model(T, sh), em)))
88
89def dq_rd(~T: Data, +sh: ST.Shadow<T>, r: Ready(~T, sh)) -> StepOK(~T, sh, E.Dequeue{}):
90 match r:
91 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
92 dq_fin(~T, sh, sh1, e, em, dequeue_ready(~T, sh1, hr))
93
94def pk_fin(~T: Data, +sh: ST.Shadow<T>, +sh1: ST.Shadow<T>, +e: {Q.ready(~T, ST.real(T, sh)) == ST.real(T, sh1) : Q.Queue<T>}, +em: {ST.model(T, sh1) == ST.model(T, sh) : List<&2, T>}, rd: Read(~T, sh1, Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh1))), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}))) -> StepOK(~T, sh, E.Peek{}):
95 match rd:
96 case Tuple{+sh2, Tuple{+o, Tuple{e1, e2}}}:
97 mk(~T, sh, E.Peek{}, sh2, o,
98 Equal.trans(Q.Queue<T> & E.Obs<T>, Q.obs_item(~T, Q.peek_ready(~T, Q.ready(~T, ST.real(T, sh)))), Q.obs_item(~T, Q.peek_ready(~T, ST.real(T, sh1))), (ST.real(T, sh2), o), Equal.cong(Q.Queue<T>, Q.Queue<T> & E.Obs<T>, d => Q.obs_item(~T, Q.peek_ready(~T, d)), Q.ready(~T, ST.real(T, sh)), ST.real(T, sh1), e), e1),
99 Equal.trans(List<&2, T> & E.Obs<T>, (ST.model(T, sh2), o), (ST.model(T, sh1), E.OItem{S.item(T, SC.head(T, ST.model(T, sh1)))}), (ST.model(T, sh), E.OItem{S.item(T, SC.head(T, ST.model(T, sh)))}), e2, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OItem{S.item(T, SC.head(T, z))}), ST.model(T, sh1), ST.model(T, sh), em)))
100
101def pk_rd(~T: Data, +sh: ST.Shadow<T>, r: Ready(~T, sh)) -> StepOK(~T, sh, E.Peek{}):
102 match r:
103 case Tuple{+sh1, Tuple{e, Tuple{em, hr}}}:
104 pk_fin(~T, sh, sh1, e, em, peek_ready(~T, sh1, hr))
105
106# ---- each operation ----
107
108def op_length(~T: Data, +sh: ST.Shadow<T>) -> StepOK(~T, sh, E.Length{}):
109 match sh:
110 case ST.Sh{+f, +b}:
111 +n = Nat.add(SC.length(T, f), SC.length(T, b))
112 +el = Equal.trans(Nat, n, Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), SC.length(T, SC.append(T, f, SC.reverse(T, b))), Equal.cong(Nat, Nat, z => Nat.add(SC.length(T, f), z), SC.length(T, b), SC.length(T, SC.reverse(T, b)), Equal.sym(Nat, SC.length(T, SC.reverse(T, b)), SC.length(T, b), LL.length_rev(T, b))), Equal.sym(Nat, SC.length(T, SC.append(T, f, SC.reverse(T, b))), Nat.add(SC.length(T, f), SC.length(T, SC.reverse(T, b))), LL.length_append(T, f, SC.reverse(T, b))))
113 mk(~T, ST.Sh{f, b}, E.Length{}, ST.Sh{f, b}, E.ONat{n}, {==}, Equal.cong(Nat, List<&2, T> & E.Obs<T>, z => (ST.model(T, ST.Sh{f, b}), E.ONat{z}), n, SC.length(T, ST.model(T, ST.Sh{f, b})), el))
114
115def op_enqueue(~T: Data, +sh: ST.Shadow<T>, +x: T) -> StepOK(~T, sh, E.Enqueue{x}):
116 match sh:
117 case ST.Sh{+f, +b}:
118 +en = Equal.sym(Nat, Nat.add(SC.length(T, f), 1n+SC.length(T, b)), 1n+Nat.add(SC.length(T, f), SC.length(T, b)), N.add_succ(SC.length(T, f), SC.length(T, b)))
119 +e1 = Equal.cong(Nat, Q.Queue<T> & E.Obs<T>, z => (Q.QU{f, Con{x, b}, z}, E.OUnit{}), 1n+Nat.add(SC.length(T, f), SC.length(T, b)), Nat.add(SC.length(T, f), 1n+SC.length(T, b)), en)
120 mk(~T, ST.Sh{f, b}, E.Enqueue{x}, ST.Sh{f, Con{x, b}}, E.OUnit{}, e1, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (z, E.OUnit{}), ST.model(T, ST.Sh{f, Con{x, b}}), SC.snoc(T, ST.model(T, ST.Sh{f, b}), x), LL.append_snoc(T, f, SC.reverse(T, b), x)))
121
122def op_to_list(~T: Data, +sh: ST.Shadow<T>) -> StepOK(~T, sh, E.ToList{}):
123 match sh:
124 case ST.Sh{+f, +b}:
125 +el = Equal.trans(List<&2, T>, List.append(&2, T, f, List.reverse(&2, T, b)), List.append(&2, T, f, SC.reverse(T, b)), SC.append(T, f, SC.reverse(T, b)), Equal.cong(List<&2, T>, List<&2, T>, z => List.append(&2, T, f, z), List.reverse(&2, T, b), SC.reverse(T, b), LL.base_rev(T, b)), LL.base_append(T, f, SC.reverse(T, b)))
126 mk(~T, ST.Sh{f, b}, E.ToList{}, ST.Sh{f, b}, E.OList{List.append(&2, T, f, List.reverse(&2, T, b))}, {==}, Equal.cong(List<&2, T>, List<&2, T> & E.Obs<T>, z => (ST.model(T, ST.Sh{f, b}), E.OList{z}), List.append(&2, T, f, List.reverse(&2, T, b)), ST.model(T, ST.Sh{f, b}), el))
127
128# every public operation refines the spec step
129def step_ok(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>) -> StepOK(~T, sh, op):
130 match op:
131 case E.Length{}:
132 op_length(~T, sh)
133 case E.Enqueue{+x}:
134 op_enqueue(~T, sh, x)
135 case E.Dequeue{}:
136 dq_rd(~T, sh, ready(~T, sh))
137 case E.Peek{}:
138 pk_rd(~T, sh, ready(~T, sh))
139 case E.ToList{}:
140 op_to_list(~T, sh)