1	# RFC 9113 HTTP/2 frames and RFC 7541 HPACK header blocks over packed Bytes.
2	import Base
3	import bend-kit-bytes@0.3.1.0/bytes.bend as Bytes
4	import ./hpack.bend as Hpack
5	
6	type Frame is Type:
7	  Frame{kind: U32, flags: U32, stream: U32, payload: Bytes.Bytes}
8	
9	type Error is Data:
10	  Error{code: U32, connection: Bool, stream: U32}
11	
12	type Decode is Type:
13	  Need{input: Bytes.Bytes}
14	  Got{frame: Frame, rest: Bytes.Bytes}
15	  Bad{error: Error}
16	
17	type Checked is Type:
18	  Valid{frame: Frame}
19	  Invalid{error: Error}
20	
21	# Error codes from RFC 9113 §7: 1=PROTOCOL_ERROR, 3=FLOW_CONTROL_ERROR,
22	# 6=FRAME_SIZE_ERROR. A connection error uses stream 0.
23	def fail(+code: U32, +connection: Bool, +stream: U32) -> Maybe<&2, Error>:
24	  Some{Error{code, connection, Bool.pick(U32, connection, 0, stream)}}
25	
26	def reject(bad: Bool, +code: U32, +connection: Bool, +stream: U32) -> Maybe<&2, Error>:
27	  match bad:
28	    case True{}:
29	      fail(code, connection, stream)
30	    case False{}:
31	      None{}
32	
33	def first(m: Maybe<&2, Error>, n: Maybe<&2, Error>) -> Maybe<&2, Error>:
34	  match m:
35	    case Some{e}:
36	      Some{e}
37	    case None{}:
38	      n
39	
40	def number(m: Maybe<&2, U32>) -> U32:
41	  match m:
42	    case Some{x}:
43	      x
44	    case None{}:
45	      0
46	
47	def with_number(-R: Type, r: Bytes.Bytes & Maybe<&2, U32>, k: Bytes.Bytes -> U32 -> R) -> R:
48	  (b, m) = r
49	  k(b, number(m))
50	
51	def with_slice(-R: Type, r: Bytes.Bytes & Bytes.Bytes, k: Bytes.Bytes -> Bytes.Bytes -> R) -> R:
52	  (b, part) = r
53	  k(b, part)
54	
55	def has(+flags: U32, +bit: U32) -> Bool:
56	  U32.is_ne((flags .&. bit : U32), 0)
57	
58	# Field blocks, SETTINGS, and stream 0 make frame-size faults connection-wide.
59	def size.scope(+kind: U32, +stream: U32) -> Bool:
60	  match kind:
61	    case 1:
62	      True{}
63	    case 4:
64	      True{}
65	    case 5:
66	      True{}
67	    case 9:
68	      True{}
69	    case _:
70	      U32.is_eq(stream, 0)
71	
72	def size.error(+kind: U32, +stream: U32) -> Error:
73	  +connection = size.scope(kind, stream)
74	  Error{6, connection, Bool.pick(U32, connection, 0, stream)}
75	
76	def size.reject(oversized: Bool, +kind: U32, +stream: U32) -> Maybe<&2, Error>:
77	  match oversized:
78	    case True{}:
79	      Some{size.error(kind, stream)}
80	    case False{}:
81	      None{}
82	
83	# A PADDED payload must contain the pad-length octet and all the padding.
84	def padding(+flags: U32, +len: U32, +fixed: U32, +pad: U32) -> Bool:
85	  Bool.and(has(flags, 8), Bool.or(U32.is_le(len, fixed), U32.is_gt(pad, (len - fixed - 1 : U32))))
86	
87	def setting(+id: U32, +value: U32) -> Maybe<&2, Error>:
88	  match id:
89	    case 2:
90	      reject(U32.is_gt(value, 1), 1, True{}, 0)
91	    case 4:
92	      reject(U32.is_gt(value, 2147483647), 3, True{}, 0)
93	    case 5:
94	      reject(Bool.or(U32.is_lt(value, 16384), U32.is_gt(value, 16777215)), 1, True{}, 0)
95	    case _:
96	      None{}
97	
98	def settings.go(n: Nat, b: Bytes.Bytes, +at: U32, m: Maybe<&2, Error>) -> Bytes.Bytes & Maybe<&2, Error>:
99	  match n:
100	    case 0n:
101	      (b, m)
102	    case 1n+p:
103	      with_number(Bytes.Bytes & Maybe<&2, Error>, Bytes.get.u16be(b, at), b => id =>
104	        with_number(Bytes.Bytes & Maybe<&2, Error>, Bytes.get.u32be(b, (at + 2 : U32)), b => value =>
105	          settings.go(p, b, (at + 6 : U32), first(m, setting(id, value)))))
106	
107	def rules(+kind: U32, +flags: U32, +stream: U32, +len: U32, +pad: U32, +promised: U32, +value: U32, m: Maybe<&2, Error>) -> Maybe<&2, Error>:
108	  match kind:
109	    case 0:
110	      first(reject(U32.is_eq(stream, 0), 1, True{}, stream),
111	        first(reject(Bool.and(has(flags, 8), U32.is_eq(len, 0)), 6, False{}, stream),
112	          reject(padding(flags, len, 0, pad), 1, True{}, stream)))
113	    case 1:
114	      +fixed = Bool.pick(U32, has(flags, 32), 5, 0)
115	      +prefix = Bool.pick(U32, has(flags, 8), 1, 0)
116	      first(reject(U32.is_eq(stream, 0), 1, True{}, stream),
117	        first(reject(U32.is_lt(len, (fixed + prefix : U32)), 6, True{}, stream),
118	          reject(padding(flags, len, fixed, pad), 1, True{}, stream)))
119	    case 2:
120	      first(reject(U32.is_ne(len, 5), 6, U32.is_eq(stream, 0), stream),
121	        reject(U32.is_eq(stream, 0), 1, True{}, stream))
122	    case 3:
123	      first(reject(U32.is_ne(len, 4), 6, True{}, stream),
124	        reject(U32.is_eq(stream, 0), 1, True{}, stream))
125	    case 4:
126	      first(reject(U32.is_ne(stream, 0), 1, True{}, stream),
127	        first(reject(Bool.and(has(flags, 1), U32.is_ne(len, 0)), 6, True{}, stream),
128	          first(reject(U32.is_ne((len % 6 : U32), 0), 6, True{}, stream), m)))
129	    case 5:
130	      +prefix = Bool.pick(U32, has(flags, 8), 1, 0)
131	      first(reject(U32.is_eq(stream, 0), 1, True{}, stream),
132	        first(reject(U32.is_lt(len, (prefix + 4 : U32)), 6, True{}, stream),
133	          first(reject(padding(flags, len, 4, pad), 1, True{}, stream),
134	            reject(U32.is_eq(promised, 0), 1, True{}, stream))))
135	    case 6:
136	      first(reject(U32.is_ne(len, 8), 6, True{}, stream),
137	        reject(U32.is_ne(stream, 0), 1, True{}, stream))
138	    case 7:
139	      first(reject(U32.is_lt(len, 8), 6, True{}, stream),
140	        reject(U32.is_ne(stream, 0), 1, True{}, stream))
141	    case 8:
142	      first(reject(U32.is_ne(len, 4), 6, U32.is_eq(stream, 0), stream),
143	        reject(U32.is_eq((value .&. 2147483647 : U32), 0), 1, U32.is_eq(stream, 0), stream))
144	    case 9:
145	      reject(U32.is_eq(stream, 0), 1, True{}, stream)
146	    case _:
147	      None{}
148	
149	def checked(m: Maybe<&2, Error>, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Checked:
150	  match m:
151	    case Some{e}:
152	      Invalid{e}
153	    case None{}:
154	      Valid{Frame{kind, flags, stream, b}}
155	
156	def with_settings(r: Bytes.Bytes & Maybe<&2, Error>, +flags: U32, +stream: U32) -> Checked:
157	  (b, m) = r
158	  checked(m, 4, flags, stream, b)
159	
160	def inspect.settings(m: Maybe<&2, Error>, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked:
161	  match m:
162	    case Some{e}:
163	      Invalid{e}
164	    case None{}:
165	      with_settings(settings.go(U32.to_nat((len / 6 : U32)), b, 0, None{}), flags, stream)
166	
167	def inspect.promised(+kind: U32, +flags: U32, +stream: U32, +len: U32, +pad: U32, b: Bytes.Bytes) -> Checked:
168	  match kind:
169	    case 5:
170	      +prefix = Bool.pick(U32, has(flags, 8), 1, 0)
171	      with_number(Checked, Bytes.get.u32be(b, prefix), b => promised =>
172	        checked(rules(kind, flags, stream, len, pad, (promised .&. 2147483647 : U32), 0, None{}), kind, flags, stream, b))
173	    case _:
174	      checked(rules(kind, flags, stream, len, pad, 0, 0, None{}), kind, flags, stream, b)
175	
176	def inspect.padded.if(padded: Bool, +kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked:
177	  match padded:
178	    case True{}:
179	      with_number(Checked, Bytes.get(b, 0), b => pad =>
180	        inspect.promised(kind, flags, stream, len, pad, b))
181	    case False{}:
182	      inspect.promised(kind, flags, stream, len, 0, b)
183	
184	def inspect.padded(+kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked:
185	  inspect.padded.if(has(flags, 8), kind, flags, stream, len, b)
186	
187	def inspect.detail(+kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked:
188	  match kind:
189	    case 0:
190	      inspect.padded(kind, flags, stream, len, b)
191	    case 1:
192	      inspect.padded(kind, flags, stream, len, b)
193	    case 4:
194	      inspect.settings(rules(kind, flags, stream, len, 0, 0, 0, None{}), flags, stream, len, b)
195	    case 5:
196	      inspect.padded(kind, flags, stream, len, b)
197	    case 8:
198	      with_number(Checked, Bytes.get.u32be(b, 0), b => value =>
199	        checked(rules(kind, flags, stream, len, 0, 0, value, None{}), kind, flags, stream, b))
200	    case _:
201	      checked(rules(kind, flags, stream, len, 0, 0, 0, None{}), kind, flags, stream, b)
202	
203	
204	def inspect.basic(m: Maybe<&2, Error>, +kind: U32, +flags: U32, +stream: U32, +len: U32, b: Bytes.Bytes) -> Checked:
205	  match m:
206	    case Some{e}:
207	      Invalid{e}
208	    case None{}:
209	      inspect.detail(kind, flags, stream, len, b)
210	
211	def inspect(max: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Checked:
212	  Bytes.Bytes{+len, buf} = b
213	  +basic = first(size.reject(Bool.or(U32.is_gt(len, max), U32.is_gt(len, 16777215)), kind, stream),
214	    first(reject(U32.is_gt(kind, 255), 1, True{}, stream),
215	      first(reject(U32.is_gt(flags, 255), 1, True{}, stream),
216	        reject(U32.is_gt(stream, 2147483647), 1, True{}, stream))))
217	  inspect.basic(basic, kind, flags, stream, len, Bytes.Bytes{len, buf})
218	
219	# max is the peer's SETTINGS_MAX_FRAME_SIZE, initially 16384.
220	def allowed(+kind: U32) -> U32:
221	  match kind:
222	    case 0:
223	      9
224	    case 1:
225	      45
226	    case 2:
227	      0
228	    case 3:
229	      0
230	    case 4:
231	      1
232	    case 5:
233	      12
234	    case 6:
235	      1
236	    case 7:
237	      0
238	    case 8:
239	      0
240	    case 9:
241	      4
242	    case _:
243	      255
244	
245	def encode.buffer(b: Bytes.Bytes, src: Array<U32>, +len: U32) -> Result<&1, &1, Error, Bytes.Bytes>:
246	  Bytes.Bytes{_, dst} = b
247	  Done{Bytes.Bytes{(len + 9 : U32), Bytes.dst(Bytes.copy(len, src, dst, 0, 9))}}
248	
249	def encode.flags(ok: Bool, +kind: U32, +flags: U32, +stream: U32, payload: Bytes.Bytes) -> Result<&1, &1, Error, Bytes.Bytes>:
250	  match ok:
251	    case False{}:
252	      Fail{Error{1, True{}, 0}}
253	    case True{}:
254	      Bytes.Bytes{+len, src} = payload
255	      encode.buffer(Bytes.set.u32be(Bytes.set(Bytes.set(Bytes.put(Bytes.new((len + 9 : U32)), 0, 3, True{}, len), 3, kind), 4, flags), 5, stream), src, len)
256	
257	def encode.checked(c: Checked) -> Result<&1, &1, Error, Bytes.Bytes>:
258	  match c:
259	    case Invalid{e}:
260	      Fail{e}
261	    case Valid{Frame{+kind, +flags, +stream, payload}}:
262	      encode.flags(U32.is_eq((flags .&. U32.not(allowed(kind)) : U32), 0), kind, flags, stream, payload)
263	def encode(max: U32, f: Frame) -> Result<&1, &1, Error, Bytes.Bytes>:
264	  Frame{+kind, +flags, +stream, payload} = f
265	  encode.checked(inspect(max, kind, flags, stream, payload))
266	
267	def parse.result(c: Checked, b: Bytes.Bytes, +len: U32) -> Decode:
268	  match c:
269	    case Invalid{e}:
270	      Bad{e}
271	    case Valid{f}:
272	      Bytes.Bytes{+n, buf} = b
273	      with_slice(Decode, Bytes.slice(Bytes.Bytes{n, buf}, (len + 9 : U32), (n - len - 9 : U32)),
274	        unused => rest => Got{f, rest})
275	
276	def parse.payload(max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode:
277	  with_slice(Decode, Bytes.slice(b, 9, len), b => payload =>
278	    parse.result(inspect(max, kind, flags, stream, payload), b, len))
279	
280	def parse.full(enough: Bool, max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode:
281	  match enough:
282	    case True{}:
283	      parse.payload(max, len, kind, flags, stream, b)
284	    case False{}:
285	      Need{b}
286	
287	def parse.size(oversized: Bool, max: U32, +len: U32, +kind: U32, +flags: U32, +stream: U32, b: Bytes.Bytes) -> Decode:
288	  match oversized:
289	    case True{}:
290	      Bad{size.error(kind, stream)}
291	    case False{}:
292	      Bytes.Bytes{+n, buf} = b
293	      parse.full(U32.is_le(len, (n - 9 : U32)), max, len, kind, flags, stream, Bytes.Bytes{n, buf})
294	
295	def parse.header(+max: U32, b: Bytes.Bytes) -> Decode:
296	  with_number(Decode, Bytes.uint(b, 0, 3, True{}), b => +len =>
297	    with_number(Decode, Bytes.get(b, 3), b => kind =>
298	      with_number(Decode, Bytes.get(b, 4), b => flags =>
299	        with_number(Decode, Bytes.get.u32be(b, 5), b => stream =>
300	          parse.size(U32.is_gt(len, max), max, len, kind, flags, (stream .&. 2147483647 : U32), b)))))
301	
302	def parse.start(short: Bool, max: U32, b: Bytes.Bytes) -> Decode:
303	  match short:
304	    case True{}:
305	      Need{b}
306	    case False{}:
307	      parse.header(max, b)
308	
309	# A partial header or payload returns Need with the original input intact.
310	def parse(max: U32, b: Bytes.Bytes) -> Decode:
311	  Bytes.Bytes{+n, buf} = b
312	  parse.start(U32.is_lt(n, 9), max, Bytes.Bytes{n, buf})