1	import Base
2	import ../lib/common.bend as C
3	import ../../src/containers/types/stack.bend as E
4	import ../lib/sequence.bend as V
5	
6	# Independent LIFO sequence model; top is the first element.
7	def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
8	  match xs op:
9	    case +ys E.Push{x}:
10	      (Con{x, ys}, E.OUnit{})
11	    case +ys E.Length{}:
12	      (ys, E.ONat{C.length(T, ys)})
13	    case +ys E.ToList{}:
14	      (ys, E.OList{ys})
15	    case Nil{} E.Pop{}:
16	      (Nil{}, E.OItem{Fail{E.EmptyStack{}}})
17	    case Con{x, tail} E.Pop{}:
18	      (tail, E.OItem{Done{x}})
19	    case Nil{} E.Peek{}:
20	      (Nil{}, E.OItem{Fail{E.EmptyStack{}}})
21	    case Con{+x, +tail} E.Peek{}:
22	      (Con{x, tail}, E.OItem{Done{x}})
23	
24	# ---- contract (SPARK formal containers) ----
25	# Each `<Subprogram>.<clause>` definition below states one Post clause of
26	# that SPARK subprogram, as a proposition on this model; the table names the
27	# clauses. proofs/containers/stack/ proves every clause under its clause name,
28	# and its `impl` lemma carries them to the implementation.
29	#
30	# Contracts of the stack in the style of SPARK's formal vectors
31	# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
32	# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
33	# sequence with the top first, so push is Prepend, pop is Delete_First and
34	# peek is First_Element. Each lemma is one Post clause of step; `impl`
35	# (P.step_correct: D.step on the stack of a sequence is step lifted)
36	# carries every clause to the implementation.
37	#
38	#   SPARK subprogram (.ads line)   ours      clauses
39	#   Length (284)                   length    length_result, length_frame
40	#   Empty_Vector (292)             new       new_empty, new_impl
41	#   Prepend (624)                  push      push_length, push_first, push_shifted
42	#   Delete_First (825)             pop       pop_length, pop_shifted, pop_result, pop_empty
43	#   First_Element (913)            peek      peek_first, peek_frame, peek_empty
44	#   iteration (Iter_Model, 1193)   to_list   to_list_model, to_list_frame
45	#   implementation                 D.step    impl
46	# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
47	# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
48	# Reference, Insert*, Append*, Delete (at an index), Delete_Last,
49	# Last_Element, Reverse_Elements, Swap, Find_Index, Reverse_Find_Index,
50	# Contains, Has_Element. SPARK's Pre (not Is_Empty) is a defensive check:
51	# on an empty stack pop and peek return EmptyStack and change nothing
52	# (pop_empty, peek_empty).
53	
54	def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
55	  Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
56	
57	def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
58	  Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
59	
60	# Length (284)
61	def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
62	  {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
63	
64	# Length (284)
65	def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
66	  {nx(T, xs, E.Length{}) == xs : List<&2, T>}
67	
68	# iteration (Iter_Model, 1193)
69	def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
70	  {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
71	
72	# iteration (Iter_Model, 1193)
73	def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
74	  {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
75	
76	# Empty_Vector (292)
77	def Empty_Vector.new_empty(-T: Data) -> Type:
78	  {C.length(T, Nil{}) == 0n : Nat}
79	
80	# Prepend (624)
81	def Prepend.push_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
82	  {C.length(T, nx(T, xs, E.Push{v})) == 1n+C.length(T, xs) : Nat}
83	
84	# Prepend (624)
85	def Prepend.push_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
86	  {C.nth(T, nx(T, xs, E.Push{v}), 0n) == Some{v} : Maybe<&2, T>}
87	
88	# Prepend (624)
89	def Prepend.push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
90	  V.RangeShifted(T, xs, nx(T, xs, E.Push{v}), 0n, C.length(T, xs), 1n)
91	
92	# Delete_First (825)
93	def Delete_First.pop_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
94	  {1n+C.length(T, nx(T, Con{h, t}, E.Pop{})) == C.length(T, Con{h, t}) : Nat}
95	
96	# Delete_First (825)
97	def Delete_First.pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
98	  V.RangeShifted(T, nx(T, Con{h, t}, E.Pop{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.Pop{})), 1n)
99	
100	# Delete_First (825)
101	def Delete_First.pop_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
102	  {ob(T, Con{h, t}, E.Pop{}) == E.OItem{Done{h}} : E.Obs<T>}
103	
104	# Delete_First (825)
105	def Delete_First.pop_empty(-T: Data) -> Type:
106	  {step(T, Nil{}, E.Pop{}) == (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) : List<&2, T> & E.Obs<T>}
107	
108	# First_Element (913)
109	def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
110	  {ob(T, Con{h, t}, E.Peek{}) == E.OItem{Done{h}} : E.Obs<T>} & {C.nth(T, Con{h, t}, 0n) == Some{h} : Maybe<&2, T>}
111	
112	# First_Element (913)
113	def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
114	  {nx(T, xs, E.Peek{}) == xs : List<&2, T>}
115	
116	# First_Element (913)
117	def First_Element.peek_empty(-T: Data) -> Type:
118	  {step(T, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) : List<&2, T> & E.Obs<T>}