C-367: compare http.serve by status code, header set and de-framed body, not raw bytes

docs/contracts/README.md

@@ -401,7 +401,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1
 | C-364 | A shape outside the scoped fragment is refused at check time, identically on both targets | 0.64.0 | active | fixture | 0 |
 | C-365 | A generic protocol with explicit conformance dispatches to the one declared implementation, identically on both targets | 0.64.0 | active | fixture | 1 |
 | C-366 | http call handle: per-call limits name themselves when they fire, cancel closes the connection, poll never blocks | 0.64.0 | active | fixture | 0 |
-| C-367 | http.serve runs on the embedded wasm lane with native's one-instance, sequential semantics and byte-identical responses | 0.64.0 | active | fixture | 0 |
+| C-367 | http.serve runs on the embedded wasm lane with native's one-instance, sequential semantics and the same status, header set and body | 0.64.0 | active | fixture | 0 |
 | C-368 | http router: a handler is a function, the most specific route answers, a broken table is refused, 404/405/400 come from the router, identically on both targets | 0.64.0 | active | fixture | 0 |
 | C-369 | a lambda's failure channel carries the error type its ! operands agree on; a String channel carries a typed error as its interpolation text, identically on both targets | 0.65.0 | active | fixture | 1 |
 

docs/contracts/contracts.toml

@@ -4484,8 +4484,8 @@ evidence  = [
 [[contract]]
 id        = "C-367"
 spec      = "ALS-R5"
-title     = "http.serve runs on the embedded wasm lane with native's one-instance, sequential semantics and byte-identical responses"
-statement = "`http.serve(port, f)` serves on the EMBEDDED wasm lane (`almide run --target wasm`, almide/almide#2650) with native's semantics. ONE instance serves every request of the run, sequentially and in accept order: main runs once and calls `http.serve` exactly as it does natively, the host binds `0.0.0.0:<port>` and hands the guest one parsed request at a time, and the handler runs in the same instance and heap as main, so a value main computed before `serve` (a random draw, a clock read) and captured by the handler is the same on every request of the run, and main's effects before `serve` happen once — never the per-request instance of a `wasi:http` proxy host. The request is read and the response written by the SAME code on both legs: the request line's method and target, header lines split at the first colon and trimmed, in wire order, and a Content-Length body decoded as UTF-8 with replacement; the response is `HTTP/1.1 <status> <reason>` (the fixed reason table, `OK` for any status outside it), the response's headers in their order, `Content-Length`, the body, then the connection closes. So the status line, the headers and the body are byte-identical across the legs; `req_method` / `req_path` / `req_body` / `req_header` (first match, ASCII case-insensitive) / `query_params` (the target's text after the first `?`, split on `&`, each pair split at its first `=`, a pair without `=` skipped, `+` and `%XX` decoded, a later key winning) answer the same values; a handler `err(m)` is a `500` whose body is `Internal error: <m>` with `Content-Type: text/plain`; a bind failure ABORTS the run with `Error: bind failed: <os message>` on stderr and exit 1 wherever the call sits — `http.serve` is typed never-err, so a caller's `!` is a no-op, and before this contract the native runtime's returned err surfaced only when the call was a fn's tail (elsewhere the program silently went on without a server). The lane keeps native's stream rules while the server runs: stderr is unbuffered, so a run's stderr transcript matches native line for line, and stdout is flushed per write on a terminal and 64 KiB-buffered otherwise. NOT covered: the stock p1 artifact (`almide build --target wasm`) has no listening socket, so `http.serve` stays refused there at check time (E081 on the stock-p1 leg), and a `wasi:http/incoming-handler` component export is a different shape that this contract does not describe (both are almide/almide#2659). Evidence: spec/serve_cross/http_serve_replay.almd, a server fixture that no generic runner executes (it never exits); the implementation's driver starts it on both legs, replays one request script (GET, POST with a UTF-8 body and a header, a percent-encoded query, a status outside the reason table, a redirect, a 404, a handler err, another method) and compares the raw response bytes and the stderr transcript, asserts that the captured draw answers the same on two requests of one run, and starts it on an occupied port to compare the abort."
+title     = "http.serve runs on the embedded wasm lane with native's one-instance, sequential semantics and the same status, header set and body"
+statement = "`http.serve(port, f)` serves on the EMBEDDED wasm lane (`almide run --target wasm`, almide/almide#2650) with native's semantics. ONE instance serves every request of the run, sequentially and in accept order: main runs once and calls `http.serve` exactly as it does natively, the host binds `0.0.0.0:<port>` and hands the guest one parsed request at a time, and the handler runs in the same instance and heap as main, so a value main computed before `serve` (a random draw, a clock read) and captured by the handler is the same on every request of the run, and main's effects before `serve` happen once — never the per-request instance of a `wasi:http` proxy host. The request is read by the SAME code on both legs: the request line's method and target, header lines split at the first colon and trimmed, in wire order, and a Content-Length body decoded as UTF-8 with replacement. Every request is answered with the same status code, header set and body on both legs. The header set is the response's header fields as (name, value) pairs, where names compare ASCII-case-insensitively; fields with different names are unordered, and fields with the same name keep their relative order (RFC 9110 §5.3). The fields a host manages are excluded: `date`, `connection`, `keep-alive`, `transfer-encoding` and `content-length` (the framing; the body is compared de-framed). The reason phrase is not part of the contract: HTTP/2 and HTTP/3 carry none (RFC 9113 §8.3.2, RFC 9114 §4.3.2), and a host's HTTP library writes its own (`418 OK` from the native core, `418 I'm a teapot` under hyper, measured by the almide/almide#2659 prototype). `req_method` / `req_path` / `req_body` / `req_header` (first match, ASCII case-insensitive) / `query_params` (the target's text after the first `?`, split on `&`, each pair split at its first `=`, a pair without `=` skipped, `+` and `%XX` decoded, a later key winning) answer the same values; a handler `err(m)` is a `500` whose body is `Internal error: <m>` with `Content-Type: text/plain`; a bind failure ABORTS the run with `Error: bind failed: <os message>` on stderr and exit 1 wherever the call sits — `http.serve` is typed never-err, so a caller's `!` is a no-op, and before this contract the native runtime's returned err surfaced only when the call was a fn's tail (elsewhere the program silently went on without a server). The lane keeps native's stream rules while the server runs: stderr is unbuffered, so every stderr line of a run reaches the stream on both legs and the two transcripts hold the same lines, whose order across requests is not promised, and stdout is flushed per write on a terminal and 64 KiB-buffered otherwise. NOT covered: HTTP framing and connection reuse (the host's); the stock p1 artifact (`almide build --target wasm`) has no listening socket, so `http.serve` stays refused there at check time (E081 on the stock-p1 leg), and a `wasi:http/incoming-handler` component export is a different shape that this contract does not describe (both are almide/almide#2659). Evidence: spec/serve_cross/http_serve_replay.almd, a server fixture that no generic runner executes (it never exits); the implementation's driver starts it on both legs, replays one request script (GET, POST with a UTF-8 body and a header, a percent-encoded query, a status outside the reason table, a redirect, a 404, a handler err, another method) and compares each response's status code, header set and de-framed body and the stderr transcripts as multisets of lines, asserts that the captured draw answers the same on two requests of one run, and starts it on an occupied port to compare the abort."
 since     = "0.64.0"
 status    = "active"
 evidence  = [

docs/specs/als/runtime.md

@@ -1,6 +1,6 @@
 # ALS — 実行時規範（Runtime）
 
-> Last updated: 2026-09-26
+> Last updated: 2026-09-28
 
 プログラム実行の観測規範（エラー終了・文字列補間の表示形・並行コンビネータ）。
 参照方法は [strings.md](strings.md) 冒頭と同じ。
@@ -111,12 +111,18 @@ native と同じ意味で動く。1 回の実行のすべての要求を 1 つ
 ハンドラは main と同じインスタンス・同じヒープで走る。したがって main が `serve`
 の前に計算してハンドラが捕捉した値（乱数・時刻）は、その実行のどの要求でも同じで
 あり、`serve` の前の main の効果は 1 回だけ起こる。要求ごとにインスタンスを作る
-`wasi:http` proxy ホストの形ではない。要求の読み取りと応答の書き出しは両レグで同じ
-コードが行う。要求行のメソッドとターゲット、最初のコロンで分けて前後の空白を除いた
-ヘッダ行（到着順）、Content-Length の本文（UTF-8、不正バイトは置換文字）を読む。
-応答は `HTTP/1.1 <status> <reason>`（固定の理由句表、表にない status は `OK`）、
-応答のヘッダ（その順）、`Content-Length`、本文の順に書き、接続を閉じる。
-よって status 行・ヘッダ・本文は両レグでバイト一致する。`req_method`・`req_path`・
+`wasi:http` proxy ホストの形ではない。要求の読み取りは両レグで同じコードが行う。
+要求行のメソッドとターゲット、最初のコロンで分けて前後の空白を除いたヘッダ行
+（到着順）、Content-Length の本文（UTF-8、不正バイトは置換文字）を読む。
+どの要求にも両レグは同じ status コード・ヘッダ集合・本文で答える。ヘッダ集合は
+応答のヘッダフィールドを (名前, 値) の組として見たもので、名前は ASCII の大小を
+区別せずに比べる。名前の異なるフィールドの順序は問わず、同じ名前のフィールドは
+互いの相対順序を保つ（RFC 9110 §5.3）。ホストが管理するフィールド `date`・
+`connection`・`keep-alive`・`transfer-encoding`・`content-length` は除く（これは
+フレーミングであり、本文はフレーミングを外して比べる）。理由句は規範に含まない。
+HTTP/2 と HTTP/3 は理由句を持たず（RFC 9113 §8.3.2、RFC 9114 §4.3.2）、ホストの
+HTTP ライブラリは自分の理由句を書く（native コアは `418 OK`、hyper は
+`418 I'm a teapot`。almide/almide#2659 の試作で測定）。`req_method`・`req_path`・
 `req_body`・`req_header`（最初の一致、ASCII 大小無視）・`query_params`（最初の
 `?` 以降を `&` で分け、各組を最初の `=` で分け、`=` の無い組は捨て、`+` と `%XX`
 を復号し、後のキーが勝つ）は同じ値を返す。ハンドラの `err(m)` は本文
@@ -126,15 +132,17 @@ native と同じ意味で動く。1 回の実行のすべての要求を 1 つ
 err を返さない型なので、呼び出し側の `!` は何もしない（この規範以前、native
 ランタイムが返す err が現れるのは呼び出しが関数の末尾にあるときだけで、それ以外の
 位置ではプログラムはサーバー無しで先へ進んでいた）。サーバーが走る間もレーンは native の
-ストリーム規則を保つ。stderr はバッファしないので、stderr の記録は native と行ごとに
-一致する。stdout は端末なら書き込みごとに flush し、それ以外は 64 KiB でバッファする。
-対象外: 標準の p1 成果物（`almide build --target wasm`）は待ち受けソケットを持たず、
+ストリーム規則を保つ。stderr はバッファしないので、実行が stderr に書く行はどれも
+両レグでストリームに届き、2 つの記録は同じ行を持つ（要求をまたぐ行の順序は規範に
+含まない）。stdout は端末なら書き込みごとに flush し、それ以外は 64 KiB でバッファする。
+対象外: HTTP のフレーミングと接続の再利用（ホストが決める）。標準の p1 成果物（`almide build --target wasm`）は待ち受けソケットを持たず、
 `http.serve` は check 時に拒否される（E081）。`wasi:http/incoming-handler`
 コンポーネントの export は別の形であり、この規範は記述しない（どちらも
 almide/almide#2659）。
 テスト: `spec/serve_cross/http_serve_replay.almd`（終了しないサーバー fixture で、
 汎用ランナーは実行しない。実装側のドライバが両レグで起動し、同じ要求列を再生して
-応答の生バイトと stderr の記録を比べ、1 回の実行の 2 つの要求で捕捉した乱数が同じで
+各応答の status コード・ヘッダ集合・フレーミングを外した本文と、行の多重集合としての
+stderr の記録を比べ、1 回の実行の 2 つの要求で捕捉した乱数が同じで
 あることを確かめ、使用中のポートで起動して中断を比べる）
 
 Contracts: C-096, C-112, C-118, C-133, C-189, C-214, C-366, C-367。

proofs/als-validation.toml

@@ -693,9 +693,9 @@ verdict = "accurate"
 
 [[section]]
 id = "ALS-R5"
-hash = "sha256:dbaf0d3f5485"
-reviewed = "2026-09-26"
-by = "O6lvl4 (via the Claude session; C-367 http.serve embedded-lane paragraph checked against the C-367 statement and spec/serve_cross/http_serve_replay.almd, whose replay driver is tests/http_serve_cross_test.rs of almide#2650, bind-failure sentence re-checked against the amended C-367 statement (abort with `Error: bind failed: <os message>` and exit 1 in every call position, almide#2659); C-366 wasm-lane paragraph checked against spec/embedded_cross/http_call_handle_errs.almd and almide#2633's loopback test run on both legs of that branch's build — native vs `almide run --target wasm` byte-identical, E081 kept on the stock route; implementation updates follow judge merge)"
+hash = "sha256:231d5efabf44"
+reviewed = "2026-09-28"
+by = "O6lvl4 (via the Claude session; C-367 http.serve paragraph rewritten from raw-byte identity to status code, header set and de-framed body with the reason phrase excluded and stderr as a line multiset, checked against the C-367 statement, ADR-0020 §7.1 in almide/almide and the replay driver tests/http_serve_cross_test.rs)"
 independent = "no"
 verdict = "accurate"
 

spec/serve_cross/http_serve_replay.almd

@@ -3,7 +3,9 @@
 // driver (tests/http_serve_cross_test.rs in almide/almide) starts it with
 // `almide run` natively and with `almide run --target wasm`, waits for the
 // "ready" line on stderr, replays one request script against each and
-// compares the raw response bytes and the stderr transcript byte for byte.
+// compares each response's status code, header set and de-framed body (the
+// reason phrase and the framing fields are the host's) and the stderr
+// transcripts as multisets of lines.
 // Usage: almide run http_serve_replay.almd [--target wasm] -- <port>
 import env
 import http