1	import Base
2	
3	# Carries the state for TransportLimits.
4	type TransportLimits is Data:
5	  TransportLimits{connections: U32, frame_bytes: U32,
6	    receive_bytes: U32, response_bytes: U32,
7	    frame_timeout_ms: U32, response_timeout_ms: U32}
8	
9	# Carries the state for QueueLimits.
10	type QueueLimits is Data:
11	  QueueLimits{requests: U32, bytes: U32, timeout_ms: U32}
12	
13	# Carries the state for ReaderLimits.
14	type ReaderLimits is Data:
15	  ReaderLimits{snapshots: U32, cursors: U32,
16	    cursors_per_snapshot: U32, retained_root_bytes: U32,
17	    retired_files: U32, index_page_bytes: U32,
18	    index_buffer_bytes: U32, restore_bytes: U32}
19	
20	# Carries the state for Options.
21	type Options is Data:
22	  Options{transport: TransportLimits, queue: QueueLimits,
23	    readers: ReaderLimits}
24	
25	# Carries the state for Decision.
26	type Decision is Data:
27	  Accepted{options: Options}
28	  InvalidTransport{}
29	  InvalidQueue{}
30	  InvalidReaders{}
31	
32	# Handles defaults.
33	def defaults() -> Options:
34	  Options{
35	    TransportLimits{64, 16777216, 16777216, 16777216,
36	      30000, 30000},
37	    QueueLimits{64, 16777216, 30000},
38	    ReaderLimits{64, 4096, 64, 67108864, 64,
39	      16384, 65536, 67108864}}
40	
41	def fields.transport(
42	  transport: TransportLimits,
43	  tail: List<&2, U32>
44	) -> List<&2, U32>:
45	  match transport:
46	    case TransportLimits{connections, frame_bytes, receive_bytes,
47	      response_bytes, frame_timeout_ms, response_timeout_ms}:
48	      Con{connections, Con{frame_bytes, Con{receive_bytes,
49	        Con{response_bytes, Con{frame_timeout_ms,
50	          Con{response_timeout_ms, tail}}}}}}
51	
52	def fields.queue(
53	  queue: QueueLimits,
54	  tail: List<&2, U32>
55	) -> List<&2, U32>:
56	  match queue:
57	    case QueueLimits{requests, bytes, timeout_ms}:
58	      Con{requests, Con{bytes, Con{timeout_ms, tail}}}
59	
60	def fields.readers(
61	  readers: ReaderLimits,
62	  tail: List<&2, U32>
63	) -> List<&2, U32>:
64	  match readers:
65	    case ReaderLimits{snapshots, cursors, cursors_per_snapshot,
66	      retained_root_bytes, retired_files, index_page_bytes,
67	      index_buffer_bytes, restore_bytes}:
68	      Con{snapshots, Con{cursors, Con{cursors_per_snapshot,
69	        Con{retained_root_bytes, Con{retired_files,
70	          Con{index_page_bytes, Con{index_buffer_bytes,
71	            Con{restore_bytes, tail}}}}}}}}
72	
73	def fields.value(options: Options) -> List<&2, U32>:
74	  match options:
75	    case Options{transport, queue, readers}:
76	      fields.transport(transport, fields.queue(queue,
77	        fields.readers(readers, Nil{})))
78	
79	# Handles fields.
80	def fields(+options: Options) -> List<&2, U32>:
81	  fields.value(options)
82	
83	def fields.same(
84	  left: List<&2, U32>,
85	  right: List<&2, U32>
86	) -> Bool:
87	  match left right:
88	    case Con{l1, Con{l2, Con{l3, Con{l4, Con{l5, Con{l6,
89	      Con{l7, Con{l8, Con{l9, Con{l10, Con{l11, Con{l12,
90	        Con{l13, Con{l14, Con{l15, Con{l16, Con{l17, Nil{}}}}}}}}}}}}}}}}}}
91	      Con{r1, Con{r2, Con{r3, Con{r4, Con{r5, Con{r6,
92	        Con{r7, Con{r8, Con{r9, Con{r10, Con{r11, Con{r12,
93	          Con{r13, Con{r14, Con{r15, Con{r16, Con{r17, Nil{}}}}}}}}}}}}}}}}}}:
94	      Bool.and(U32.is_eq(l1, r1), Bool.and(U32.is_eq(l2, r2),
95	        Bool.and(U32.is_eq(l3, r3), Bool.and(U32.is_eq(l4, r4),
96	          Bool.and(U32.is_eq(l5, r5), Bool.and(U32.is_eq(l6, r6),
97	            Bool.and(U32.is_eq(l7, r7), Bool.and(U32.is_eq(l8, r8),
98	              Bool.and(U32.is_eq(l9, r9), Bool.and(U32.is_eq(l10, r10),
99	                Bool.and(U32.is_eq(l11, r11), Bool.and(U32.is_eq(l12, r12),
100	                  Bool.and(U32.is_eq(l13, r13),
101	                    Bool.and(U32.is_eq(l14, r14),
102	                      Bool.and(U32.is_eq(l15, r15),
103	                        Bool.and(U32.is_eq(l16, r16),
104	                          U32.is_eq(l17, r17)))))))))))))))))
105	    case _ _: False{}
106	
107	# Handles same.
108	def same(+left: Options, +right: Options) -> Bool:
109	  fields.same(fields(left), fields(right))
110	
111	def snapshot.limits(options: Options) -> U32 & U32:
112	  match options:
113	    case Options{_, _, ReaderLimits{snapshots, _, _, retained_root_bytes, _, _, _, _}}:
114	      (snapshots, retained_root_bytes)
115	
116	def snapshot.retained.bytes(options: Options) -> U32:
117	  match options:
118	    case Options{_, _, ReaderLimits{_, _, _, retained_root_bytes, _, _, _, _}}:
119	      retained_root_bytes
120	
121	def snapshot.count(options: Options) -> U32:
122	  match options:
123	    case Options{_, _, ReaderLimits{snapshots, _, _, _, _, _, _, _}}:
124	      snapshots
125	
126	def cursor.per.snapshot(options: Options) -> U32:
127	  match options:
128	    case Options{_, _, ReaderLimits{_, _, cursors_per_snapshot, _, _, _, _, _}}:
129	      cursors_per_snapshot
130	
131	def cursor.count(options: Options) -> U32:
132	  match options:
133	    case Options{_, _, ReaderLimits{_, cursors, _, _, _, _, _, _}}:
134	      cursors
135	
136	def transport.frame.bytes(options: Options) -> U32:
137	  match options:
138	    case Options{TransportLimits{_, frame_bytes, _, _, _, _}, _, _}:
139	      frame_bytes
140	
141	def transport.receive.bytes(options: Options) -> U32:
142	  match options:
143	    case Options{TransportLimits{_, _, receive_bytes, _, _, _}, _, _}:
144	      receive_bytes
145	
146	def transport.connections(options: Options) -> U32:
147	  match options:
148	    case Options{TransportLimits{connections, _, _, _, _, _}, _, _}:
149	      connections
150	
151	def transport.frame.timeout(options: Options) -> U32:
152	  match options:
153	    case Options{TransportLimits{_, _, _, _, frame_timeout_ms, _}, _, _}:
154	      frame_timeout_ms
155	
156	def transport.response.timeout(options: Options) -> U32:
157	  match options:
158	    case Options{TransportLimits{_, _, _, _, _, response_timeout_ms}, _, _}:
159	      response_timeout_ms
160	
161	def queue.timeout(options: Options) -> U32:
162	  match options:
163	    case Options{_, QueueLimits{_, _, timeout_ms}, _}:
164	      timeout_ms
165	
166	def queue.requests(options: Options) -> U32:
167	  match options:
168	    case Options{_, QueueLimits{requests, _, _}, _}:
169	      requests
170	
171	def queue.bytes(options: Options) -> U32:
172	  match options:
173	    case Options{_, QueueLimits{_, bytes, _}, _}:
174	      bytes
175	
176	def transport.response.bytes(options: Options) -> U32:
177	  match options:
178	    case Options{TransportLimits{_, _, _, response_bytes, _, _}, _, _}:
179	      response_bytes
180	
181	def response.admitted(length: U32, max_bytes: U32) -> Bool:
182	  U32.is_le(length, max_bytes)
183	
184	# Handles positive.
185	def positive(value: U32) -> Bool:
186	  U32.is_lt(0, value)
187	
188	# Handles bounded.
189	def bounded(+value: U32, maximum: U32) -> Bool:
190	  positive(value) && U32.is_le(value, maximum)
191	
192	def frame.valid(+frame_bytes: U32, +receive_bytes: U32,
193	  +response_bytes: U32) -> Bool:
194	  bounded(frame_bytes, 1073741824) &&
195	    U32.is_le(frame_bytes, receive_bytes) &&
196	    U32.is_le(frame_bytes, response_bytes) &&
197	    bounded(receive_bytes, 1073741824) &&
198	    bounded(response_bytes, 1073741824)
199	
200	def transport.valid(limits: TransportLimits) -> Bool:
201	  match limits:
202	    case TransportLimits{connections, frame_bytes, receive_bytes,
203	      response_bytes, frame_timeout_ms, response_timeout_ms}:
204	      bounded(connections, 4294967295) &&
205	        frame.valid(frame_bytes, receive_bytes, response_bytes) &&
206	        bounded(frame_timeout_ms, 4294967295) &&
207	        bounded(response_timeout_ms, 4294967295)
208	
209	def queue.bytes.valid(+bytes: U32) -> Bool:
210	  bounded(bytes, 1073741824)
211	
212	def queue.valid(limits: QueueLimits) -> Bool:
213	  match limits:
214	    case QueueLimits{requests, bytes, timeout_ms}:
215	      bounded(requests, 4294967295) &&
216	        queue.bytes.valid(bytes) &&
217	        bounded(timeout_ms, 4294967295)
218	
219	def cursor.limits.valid(+cursors: U32,
220	  +cursors_per_snapshot: U32) -> Bool:
221	  bounded(cursors, 4096) &&
222	    bounded(cursors_per_snapshot, 64) &&
223	    U32.is_le(cursors_per_snapshot, cursors)
224	
225	def retained.limits.valid(+snapshots: U32,
226	  +retained_root_bytes: U32, +retired_files: U32) -> Bool:
227	  bounded(snapshots, 64) &&
228	    bounded(retained_root_bytes, 67108864) &&
229	    bounded(retired_files, 64)
230	
231	def index.limits.valid(+index_page_bytes: U32,
232	  +index_buffer_bytes: U32) -> Bool:
233	  bounded(index_page_bytes, 16384) &&
234	    bounded(index_buffer_bytes, 65536) &&
235	    U32.is_le(index_page_bytes, index_buffer_bytes)
236	
237	def readers.valid(limits: ReaderLimits) -> Bool:
238	  match limits:
239	    case ReaderLimits{snapshots, cursors, cursors_per_snapshot,
240	      retained_root_bytes, retired_files, index_page_bytes,
241	      index_buffer_bytes, restore_bytes}:
242	      cursor.limits.valid(cursors, cursors_per_snapshot) &&
243	        retained.limits.valid(snapshots, retained_root_bytes, retired_files) &&
244	        index.limits.valid(index_page_bytes, index_buffer_bytes) &&
245	        bounded(restore_bytes, 67108864)
246	
247	def validate.readers(options: Options, readers_ok: Bool) -> Decision:
248	  match readers_ok:
249	    case True{}: Accepted{options}
250	    case False{}: InvalidReaders{}
251	
252	def validate.queue(options: Options, queue_ok: Bool,
253	  readers_ok: Bool) -> Decision:
254	  match queue_ok:
255	    case True{}: validate.readers(options, readers_ok)
256	    case False{}: InvalidQueue{}
257	
258	def validate.transport(options: Options, transport_ok: Bool,
259	  queue_ok: Bool, readers_ok: Bool) -> Decision:
260	  match transport_ok:
261	    case True{}: validate.queue(options, queue_ok, readers_ok)
262	    case False{}: InvalidTransport{}
263	
264	# Handles validate.
265	def validate(+options: Options) -> Decision:
266	  match options:
267	    case Options{transport, queue, readers}:
268	      validate.transport(options, transport.valid(transport),
269	        queue.valid(queue), readers.valid(readers))
270	
271	def reader.retired.files(options: Options) -> U32:
272	  match options:
273	    case Options{_, _, ReaderLimits{_, _, _, _, retired_files, _, _, _}}:
274	      retired_files