1	# ezhttp/src/packed: a response read off its packed octets (bend-kit-bytes),
2	# so its body is never turned into text. Only the heads and the chunk-size
3	# lines are read as text, a few octets each; every decision is
4	# src/http.bend's, the same one its text parse makes (SPEC.md HTTP-CLI-15):
5	# which head is final and what its plan is (head.final), its reason phrase
6	# (phrase.line), and what each chunk-size line says (chunk.size). This module
7	# only finds those lines and copies the body's octets out (SPEC.md
8	# HTTP-TRUST-9).
9	import Base
10	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
11	import ./http.bend as Http
12	
13	# a response read off its octets: torn, or its status, its header fields and
14	# reason phrase as octet text, and its body's octets
15	type Got is Type:  # noqa: L001 holds packed Bytes, which no law reaches (HTTP-TRUST-9)
16	  Torn{why: String}
17	  Got{status: U32, headers: List<&2, Http.Header>, reason: String,
18	    body: Bytes.Bytes}
19	
20	# a chunked body's octets so far, newest first, or why it was torn
21	type Parts is Type:  # noqa: L001 holds packed Bytes, which no law reaches (HTTP-TRUST-9)
22	  Bad{why: String}
23	  Parts{parts: List<&1, Bytes.Bytes>}
24	
25	# a slice's copy as text, the buffer kept
26	def packed.text.of(r: Bytes.Bytes & Bytes.Bytes) -> Bytes.Bytes & String:
27	  (b, piece) = r
28	  (b, Bytes.to_string(piece))
29	
30	# n octets from `at` as text (a head or a chunk-size line), the buffer kept
31	def packed.text(b: Bytes.Bytes, +at: U32, +n: U32) -> Bytes.Bytes & String:
32	  packed.text.of(Bytes.slice(b, at, n))
33	
34	# n octets from `at`, the buffer dropped
35	def packed.copy(b: Bytes.Bytes, +at: U32, +n: U32) -> Bytes.Bytes:
36	  Bytes.snd(Bytes.slice(b, at, n))
37	
38	# --- a chunked body (RFC 9112 §7.1), as chunk.size decides ---
39	
40	# a chunk's octets copied out, then on to the chunk-size line after its CRLF
41	def packed.chunk.take(r: Bytes.Bytes & Bytes.Bytes, +next: U32,
42	  acc: List<&1, Bytes.Bytes>,
43	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
44	  (b, part) = r
45	  go(b)(next)(part <> acc)
46	
47	# a chunk of k octets from d, ready when its CRLF follows them
48	def packed.chunk.ready.is(b: Bytes.Bytes, +d: U32, +k: U32,
49	  acc: List<&1, Bytes.Bytes>, ready: Bool,
50	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
51	  match ready:
52	    case False{}:
53	      Bad{Http.chunk.short()}
54	    case True{}:
55	      packed.chunk.take(Bytes.slice(b, d, k), (d + k + 2 : U32), acc, go)
56	
57	# a chunk of k octets from d whose CRLF has been looked for (chunks.ready)
58	def packed.chunk.ready(r: Bytes.Bytes & String, +d: U32, +k: U32,
59	  acc: List<&1, Bytes.Bytes>,
60	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
61	  (b, crlf) = r
62	  packed.chunk.ready.is(b, d, k, acc, String.eq(crlf, "\r\n"), go)
63	
64	# a chunk of n octets from d: its octets must all be there, and a CRLF after
65	# them
66	def packed.chunk.data(b: Bytes.Bytes, +d: U32, +n: Nat,
67	  acc: List<&1, Bytes.Bytes>, fits: Bool,
68	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
69	  match fits:
70	    case False{}:
71	      Bad{Http.chunk.short()}
72	    case True{}:
73	      +k = U32.from_nat(n)
74	      packed.chunk.ready(packed.text(b, (d + k : U32), 2), d, k, acc, go)
75	
76	# what a chunk-size line says, acted on with the octets after it
77	def packed.chunk.size(b: Bytes.Bytes, +d: U32, +len: U32,
78	  acc: List<&1, Bytes.Bytes>, z: Http.Size,
79	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
80	  match z:
81	    case Http.SizeBad{why}:
82	      Bad{why}
83	    case Http.SizeLast{}:
84	      Parts{acc}
85	    case Http.SizeData{+n}:
86	      packed.chunk.data(b, d, n, acc,
87	        Bool.not(Nat.is_lt(U32.to_nat((len - d : U32)), Nat.add(n, 2n))), go)
88	
89	# a chunk-size line read, its octets after its CRLF
90	def packed.chunk.line(r: Bytes.Bytes & String, +d: U32, +len: U32,
91	  acc: List<&1, Bytes.Bytes>,
92	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
93	  (b, line) = r
94	  packed.chunk.size(b, d, len, acc, Http.chunk.size(line), go)
95	
96	# a chunk-size line that ends at i, or none ends: the body ends there
97	def packed.chunk.at(r: Bytes.Bytes & Maybe<&2, U32>, +p: U32,
98	  +len: U32, acc: List<&1, Bytes.Bytes>,
99	  go: Bytes.Bytes -> U32 -> List<&1, Bytes.Bytes> -> Parts) -> Parts:
100	  (b, at) = r
101	  match at:
102	    case None{}:
103	      Parts{acc}
104	    case Some{+i}:
105	      packed.chunk.line(packed.text(b, p, (i - p : U32)), (i + 2 : U32),
106	        len, acc, go)
107	
108	# the chunks from the chunk-size line at p, at most `fuel` of them
109	def packed.chunks(fuel: Nat, b: Bytes.Bytes, +p: U32, +len: U32,
110	  acc: List<&1, Bytes.Bytes>) -> Parts:
111	  match fuel:
112	    case 0n:
113	      Bad{"the chunked body is truncated"}
114	    case 1n+f:
115	      packed.chunk.at(Bytes.find.from(b, "\r\n", p), p, len, acc,
116	        b2 => q => a2 => packed.chunks(f, b2, q, len, a2))
117	
118	# a chunked body's octets in order, or why it was torn
119	def packed.chunked(st: U32, hs: List<&2, Http.Header>, reason: String,
120	  r: Parts) -> Got:
121	  match r:
122	    case Bad{why}:
123	      Torn{why}
124	    case Parts{ps}:
125	      Got{st, hs, reason, Bytes.concat(List.reverse(&1, Bytes.Bytes, ps))}
126	
127	# --- the body under its framing (RFC 9112 §6.3) ---
128	
129	# a body framed by Content-Length: torn when fewer octets arrived
130	def packed.sized(st: U32, hs: List<&2, Http.Header>, reason: String,
131	  b: Bytes.Bytes, +q: U32, +n: Nat, short: Bool) -> Got:
132	  match short:
133	    case True{}:
134	      Torn{"the response body stopped before its Content-Length"}
135	    case False{}:
136	      Got{st, hs, reason, packed.copy(b, q, U32.from_nat(n))}
137	
138	# the octets after the final head, as its framing says
139	def packed.body(st: U32, hs: List<&2, Http.Header>, reason: String,
140	  f: Http.Frame, b: Bytes.Bytes, +q: U32, +len: U32) -> Got:
141	  match f:
142	    case Http.Bare{}:
143	      Got{st, hs, reason, Bytes.new(0)}
144	    case Http.Sized{+n}:
145	      packed.sized(st, hs, reason, b, q, n,
146	        Nat.is_lt(U32.to_nat((len - q : U32)), n))
147	    case Http.Chunked{}:
148	      packed.chunked(st, hs, reason,
149	        packed.chunks(U32.to_nat((len - q : U32)), b, q, len, []))
150	    case Http.Closed{}:
151	      Got{st, hs, reason, packed.copy(b, q, (len - q : U32))}
152	
153	# the final head's plan carried out on the octets after it
154	def packed.final(p: Http.Plan, reason: String, b: Bytes.Bytes, +q: U32,
155	  +len: U32) -> Got:
156	  match p:
157	    case Http.Unplanned{why}:
158	      Torn{why}
159	    case Http.Planned{st, hs, f}:
160	      packed.body(st, hs, reason, f, b, q, len)
161	
162	# --- the heads (RFC 9112 §2.1, RFC 9110 §15.2) ---
163	
164	# an interim head is skipped, any other is the final one
165	def packed.step(+asked: Bool, b: Bytes.Bytes, +q: U32, +len: U32,
166	  +ls: List<&2, String>, skip: Bool, rest: Bytes.Bytes -> U32 -> Got) -> Got:
167	  match skip:
168	    case True{}:
169	      rest(b)(q)
170	    case False{}:
171	      packed.final(Http.head.final(asked, ls), Http.phrase.line(Http.first(ls)),
172	        b, q, len)
173	
174	# a head read as text, and the octets after its blank line from q
175	def packed.head.text(+asked: Bool, r: Bytes.Bytes & String, +q: U32,
176	  +len: U32, rest: Bytes.Bytes -> U32 -> Got) -> Got:
177	  (b, before) = r
178	  +ls = String.lines(before)
179	  packed.step(asked, b, q, len, ls,
180	    Http.interim.skip.of(Http.status.of(ls), U32.is_lt(q, len)), rest)
181	
182	# a head that ends at i, or none ends
183	def packed.head(+asked: Bool, r: Bytes.Bytes & Maybe<&2, U32>, +p: U32,
184	  +len: U32, rest: Bytes.Bytes -> U32 -> Got) -> Got:
185	  (b, at) = r
186	  match at:
187	    case None{}:
188	      Torn{"the response head has no blank line after it"}
189	    case Some{+i}:
190	      packed.head.text(asked, packed.text(b, p, (i - p : U32)), (i + 4 : U32),
191	        len, rest)
192	
193	# the heads in turn from p, at most `fuel` of them
194	def packed.heads(fuel: Nat, +asked: Bool, b: Bytes.Bytes, +p: U32, +len: U32)
195	  -> Got:
196	  match fuel:
197	    case 0n:
198	      Torn{"the response head has no blank line after it"}
199	    case 1n+f:
200	      packed.head(asked, Bytes.find.from(b, "\r\n\r\n", p), p, len,
201	        b2 => q => packed.heads(f, asked, b2, q, len))
202	
203	# the response to a request with this method, its octets counted
204	def packed.reply.of(+method: String, r: Bytes.Bytes & U32) -> Got:
205	  (b, +len) = r
206	  packed.heads(U32.to_nat(len), String.eq(method, "HEAD"), b, 0, len)
207	
208	# the response to a request with this method, read off its octets as
209	# parse.to reads its text (SPEC.md HTTP-CLI-9, HTTP-CLI-15, HTTP-TRUST-9)
210	def packed.reply(+method: String, b: Bytes.Bytes) -> Got:
211	  packed.reply.of(method, Bytes.length(b))