proofs/containers/stack/proof.bend
bend-collections-laws-containers@1.0.0.0 · 138 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/stack.bend as D
3import bend-collections-laws-containers@1.0.0.0/spec/containers/stack.bend as S
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/stack.bend as E
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
10
11# Universal one-step refinement, including cached count preservation and
12# empty errors. Concrete instances in STACK_COMPONENT_PROOF.bend.
13def real(~T: Data, +xs: List<&2, T>) -> D.Stack<T>:
14 D.ST{xs, C.length(T, xs)}
15
16def lift(~T: Data, r: List<&2, T> & E.Obs<T>) -> D.Stack<T> & E.Obs<T>:
17 (xs, obs) = r
18 (real(~T, xs), obs)
19
20def step_correct(~T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> {D.step(~T, real(~T, xs), op) == lift(~T, S.step(T, xs, op)) : D.Stack<T> & E.Obs<T>}:
21 match xs op:
22 case Nil{} E.Push{v}:
23 {==}
24 case Nil{} E.Length{}:
25 {==}
26 case Nil{} E.ToList{}:
27 {==}
28 case Nil{} E.Peek{}:
29 {==}
30 case Nil{} E.Pop{}:
31 {==}
32 case Con{+x, +tail} E.Push{v}:
33 {==}
34 case Con{+x, +tail} E.Length{}:
35 {==}
36 case Con{+x, +tail} E.ToList{}:
37 {==}
38 case Con{+x, +tail} E.Peek{}:
39 {==}
40 case Con{+x, +tail} E.Pop{}:
41 Equal.cong(Nat, D.Stack<T> & E.Obs<T>, n => (D.ST{tail, n}, E.OItem{Done{x}}), Nat.sub(C.length(T, tail), 0n), C.length(T, tail), N.sub_zero(C.length(T, tail)))
42
43def constructor(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:
44 {==}
45
46# ==== the contract of stack (stated in spec/containers/stack.bend) ====================
47
48# ---- the implementation ----
49def impl(~T: Data, +xs: List<&2, T>, +op: E.Op<T>, -Post: (D.Stack<T> & E.Obs<T>) -> Type, pf: Post(lift(~T, S.step(T, xs, op)))) -> Post(D.step(~T, real(~T, xs), op)):
50 L.subst(D.Stack<T> & E.Obs<T>, Post, lift(~T, S.step(T, xs, op)), D.step(~T, real(~T, xs), op), Equal.sym(D.Stack<T> & E.Obs<T>, D.step(~T, real(~T, xs), op), lift(~T, S.step(T, xs, op)), step_correct(~T, xs, op)), pf)
51
52# ---- Length, iteration ----
53def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
54 match xs:
55 case Nil{}:
56 {==}
57 case Con{h, t}:
58 {==}
59
60def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
61 match xs:
62 case Nil{}:
63 {==}
64 case Con{h, t}:
65 {==}
66
67def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
68 match xs:
69 case Nil{}:
70 {==}
71 case Con{h, t}:
72 {==}
73
74def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
75 match xs:
76 case Nil{}:
77 {==}
78 case Con{h, t}:
79 {==}
80
81# ---- Empty_Vector ----
82def new_empty(-T: Data) -> S.Empty_Vector.new_empty(T):
83 {==}
84
85def new_impl(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:
86 constructor(~T)
87
88# ---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ----
89def push_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_length(T, xs, v):
90 match xs:
91 case Nil{}:
92 {==}
93 case Con{h, t}:
94 {==}
95
96def push_first(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_first(T, xs, v):
97 match xs:
98 case Nil{}:
99 {==}
100 case Con{h, t}:
101 {==}
102
103def push_is(-T: Data, +xs: List<&2, T>, +v: T) -> {S.nx(T, xs, E.Push{v}) == Con{v, xs} : List<&2, T>}:
104 match xs:
105 case Nil{}:
106 {==}
107 case Con{h, t}:
108 {==}
109
110def push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_shifted(T, xs, v):
111 L.subst(List<&2, T>, z => V.RangeShifted(T, xs, z, 0n, C.length(T, xs), 1n), Con{v, xs}, S.nx(T, xs, E.Push{v}), Equal.sym(List<&2, T>, S.nx(T, xs, E.Push{v}), Con{v, xs}, push_is(T, xs, v)), VL.cons_shifted(T, xs, v))
112
113# ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop returns First_Element'Old ----
114def pop_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_length(T, h, t):
115 {==}
116
117def pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_shifted(T, h, t):
118 VL.tail_shifted(T, h, t)
119
120def pop_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_result(T, h, t):
121 {==}
122
123def pop_empty(-T: Data) -> S.Delete_First.pop_empty(T):
124 {==}
125
126# ---- First_Element: Element (Model, First); nothing changes ----
127def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):
128 ({==}, {==})
129
130def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):
131 match xs:
132 case Nil{}:
133 {==}
134 case Con{h, t}:
135 {==}
136
137def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):
138 {==}