Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions docs/contracts/conformance.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
> (spec-coverage + evidence-class >= fixture for every active contract), so this
> page cannot legitimately contain an empty Fixtures cell.

132 normative sections; 807 distinct executable fixtures.
132 normative sections; 808 distinct executable fixtures.

| Section | Contracts | Fixtures (how CI runs each) |
|---------|-----------|------------------------------|
Expand Down Expand Up @@ -103,7 +103,7 @@
| ALS-R2 | C-008, C-009, C-010, C-011, C-222 | `spec/wasm_cross/compound_repr_interp.almd` (byte-compare)<br>`spec/wasm_cross/repr_parity_pin.almd` (byte-compare)<br>`spec/wasm_cross/fuzz_found_nested_interp_capture.almd` (byte-compare)<br>`spec/wasm_cross/compound_repr_records_interp.almd` (byte-compare)<br>`spec/wasm_cross/compound_repr_recursive_interp.almd` (byte-compare)<br>`spec/integration/modules/cross_module_repr_test.almd` (both-target test)<br>`spec/integration/modules/cross_module_repr_derive_test.almd` (both-target test)<br>`tests/module_type_repr_test.rs` (cargo gate)<br>`spec/wasm_cross/recursive_generic_repr_interp.almd` (byte-compare)<br>`spec/wasm_cross/float_concrete.almd` (byte-compare)<br>`spec/wasm_cross/num_edge_to_string.almd` (byte-compare)<br>`spec/wasm_cross/int_float_ops.almd` (byte-compare)<br>`spec/wasm_cross/float_interp_forms.almd` (byte-compare)<br>`spec/wasm_cross/nested_unwrap_propagation.almd` (byte-compare) |
| ALS-R3 | C-004, C-005, C-006, C-199, C-321, C-349 | `spec/wasm_cross/fan_deterministic.almd` (byte-compare)<br>`spec/wasm_cross/fan_map_inline_lambda.almd` (byte-compare)<br>`spec/wasm_cross/fan_pure_thunks.almd` (byte-compare)<br>`spec/wasm_cross/fan_var_thunk_list.almd` (byte-compare)<br>`spec/wasm_cross/fan_effect_mapper.almd` (byte-compare)<br>`spec/wasm_cross/fan_effect_mapper_capability.almd` (byte-compare)<br>`spec/embedded_cross/fan_mapper_effect_callback_forms.almd` (both-target test)<br>`spec/wasm_cross/fan_map_err.almd` (byte-compare)<br>`spec/wasm_cross/fan_map_inline_err.almd` (byte-compare)<br>`spec/wasm_cross/fan_any_allfail.almd` (byte-compare)<br>`spec/wasm_cross/option_none_unwrap_term.almd` (byte-compare)<br>`tests/diagnostics/e027-fan-timeout-removed/broken.almd` (checker)<br>`tests/diagnostic_harness_test.rs` (cargo gate)<br>`spec/wasm_cross/fan_block_err_list_order.almd` (byte-compare)<br>`spec/wasm_cross/fan_prefetch_fs.almd` (byte-compare)<br>`tests/component_p3_test.rs` (cargo gate)<br>`spec/wasm_cross/fan_arm_unwrap_or.almd` (byte-compare) |
| ALS-R4 | C-012 | `spec/wasm_cross/const_fold_nonfinite_float.almd` (byte-compare) |
| ALS-R5 | C-096, C-112, C-118, C-133, C-189, C-214, C-215, C-290, C-327, C-330, C-328, C-329, C-331, C-366, C-367 | `spec/wasm_cross/process_args.almd` (byte-compare)<br>`spec/wasm_cross/random_int_entropy.almd` (byte-compare)<br>`spec/wasm_cross/env_args.almd` (byte-compare)<br>`spec/wasm_cross/env_get.almd` (byte-compare)<br>`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)<br>`spec/stdlib/process_timeout_test.almd` (both-target test)<br>`spec/stdlib/fs_if_exists_test.almd` (both-target test)<br>`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)<br>`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)<br>`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)<br>`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)<br>`tests/component_p3_test.rs` (cargo gate)<br>`spec/embedded_cross/http_client_errs.almd` (both-target test)<br>`spec/embedded_cross/http_framed_errs.almd` (both-target test)<br>`spec/wasm_cross/env_set_overlay.almd` (byte-compare)<br>`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)<br>`spec/stdlib/http_call_test.almd` (both-target test)<br>`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)<br>`spec/serve_cross/http_serve_replay.almd` (both-target test) |
| ALS-R5 | C-096, C-112, C-118, C-133, C-189, C-214, C-215, C-290, C-327, C-330, C-328, C-329, C-331, C-366, C-367 | `spec/wasm_cross/process_args.almd` (byte-compare)<br>`spec/wasm_cross/random_int_entropy.almd` (byte-compare)<br>`spec/wasm_cross/env_args.almd` (byte-compare)<br>`spec/wasm_cross/env_get.almd` (byte-compare)<br>`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)<br>`spec/stdlib/process_timeout_test.almd` (both-target test)<br>`spec/stdlib/fs_if_exists_test.almd` (both-target test)<br>`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)<br>`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)<br>`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)<br>`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)<br>`tests/component_p3_test.rs` (cargo gate)<br>`spec/embedded_cross/http_client_errs.almd` (both-target test)<br>`spec/embedded_cross/http_framed_errs.almd` (both-target test)<br>`spec/wasm_cross/env_set_overlay.almd` (byte-compare)<br>`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)<br>`spec/stdlib/http_call_test.almd` (both-target test)<br>`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)<br>`spec/serve_cross/http_serve_replay.almd` (both-target test)<br>`spec/serve_cross/http_serve_shutdown.almd` (both-target test) |
| ALS-R6 | C-042, C-137, C-220, C-225, C-227, C-228, C-229, C-230, C-270, C-272, C-273, C-278, C-282, C-283, C-284 | `spec/wasm_cross/fs_preopen_resolve.almd` (byte-compare)<br>`spec/wasm_cross/fs_relative_path.almd` (byte-compare)<br>`spec/stdlib/fs_stat_test.almd` (both-target test)<br>`spec/stdlib/fs_streaming_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_range_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_chunked_test.almd` (both-target test)<br>`spec/wasm_cross/fs_read_lines.almd` (byte-compare)<br>`spec/wasm_cross/fs_metadata_family.almd` (byte-compare)<br>`spec/wasm_cross/fs_composition_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows.almd` (byte-compare)<br>`spec/wasm_cross/fs_glob_segments.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_oob.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_q1_partial_block.almd` (byte-compare)<br>`spec/wasm_cross/bytes_negative_offset_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q1_full_loader_cols_beyond_buffer.almd` (byte-compare)<br>`spec/wasm_cross/flight_pid_control.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_fp16_scale_domain.almd` (byte-compare)<br>`spec/wasm_cross/fs_list_dir_multipass.almd` (byte-compare)<br>`spec/wasm_cross/fs_write_errno.almd` (byte-compare)<br>`spec/wasm_fail/rope_geometry_exceeds_aborts.almd` (both-target test)<br>`spec/wasm_cross/rope_geometry_family.almd` (byte-compare)<br>`spec/wasm_cross/rope_at_family.almd` (byte-compare)<br>`spec/wasm_fail/matrix_index_oob_aborts.almd` (both-target test)<br>`spec/wasm_cross/matrix_index_domain_family.almd` (byte-compare)<br>`spec/wasm_cross/callee_shadowing_family.almd` (byte-compare)<br>`spec/wasm_cross/fallible_hof_effect_callback_family.almd` (byte-compare) |
| ALS-R7 | C-274, C-335 | `spec/embedded_cross/fs_fallible_callback_compound.almd` (both-target test)<br>`spec/wasm_cross/fs_fallible_stream_callback.almd` (byte-compare)<br>`spec/stdlib/fs_streaming_test.almd` (both-target test)<br>`tests/fs_streaming_family_gate_test.rs` (cargo gate)<br>`spec/wasm_cross/path_extension_hidden.almd` (byte-compare) |
| ALS-R8 | C-275, C-368 | `spec/wasm_cross/http_response_headers.almd` (byte-compare)<br>`spec/stdlib/http_router_test.almd` (both-target test) |
Expand Down
3 changes: 2 additions & 1 deletion docs/contracts/contracts.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4485,11 +4485,12 @@ evidence = [
id = "C-367"
spec = "ALS-R5"
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."
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. A signal stops the server without losing its output (almide/almide#2692): on the first SIGTERM or SIGINT (on Windows, Ctrl-C or Ctrl-Break) while `http.serve` runs, the host stops accepting (a connection it has not accepted is closed unanswered), lets the request in flight finish and answers it, flushes stdout, and `http.serve` returns, so the statements after it run and the exit code is main's. A second signal, during that drain or after `serve` returned, or a drain still waiting when the request timeout (30 s) has passed, flushes stdout and exits 1 without answering the request in flight; no stop exits with 128+signal (C-350's `0..=125`). NOT covered: HTTP framing and connection reuse (the host's); other signals; on native Windows the forced stop exits 1 without flushing stdout, since only the serving thread can reach its stdout buffer until stdout becomes one process-global buffer (ADR-0020 §5.5 in almide/almide); 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; spec/serve_cross/http_serve_shutdown.almd, a server fixture the same driver starts on both legs with stdout redirected to a file: one SIGTERM while a request sleeps in its handler must answer that request, leave every stdout line in the file including the one main prints after `http.serve`, and exit 0; two SIGTERMs while a request stalls must exit 1 with every line printed before the stop."
since = "0.64.0"
status = "active"
evidence = [
{ path = "spec/serve_cross/http_serve_replay.almd", class = "fixture" },
{ path = "spec/serve_cross/http_serve_shutdown.almd", class = "fixture" },
]
[[contract]]
id = "C-368"
Expand Down
20 changes: 18 additions & 2 deletions docs/specs/als/runtime.md
Original file line number Diff line number Diff line change
Expand Up @@ -135,15 +135,31 @@ err を返さない型なので、呼び出し側の `!` は何もしない(
ストリーム規則を保つ。stderr はバッファしないので、実行が stderr に書く行はどれも
両レグでストリームに届き、2 つの記録は同じ行を持つ(要求をまたぐ行の順序は規範に
含まない)。stdout は端末なら書き込みごとに flush し、それ以外は 64 KiB でバッファする。
対象外: HTTP のフレーミングと接続の再利用(ホストが決める)。標準の p1 成果物(`almide build --target wasm`)は待ち受けソケットを持たず、
シグナルはサーバーの出力を失わせずに止める(almide/almide#2692)。`http.serve` が
動いている間に最初の SIGTERM か SIGINT(Windows では Ctrl-C か Ctrl-Break)が届くと、
ホストは受理をやめ(まだ受理していない接続は答えずに閉じる)、処理中の要求を最後まで
処理して答え、stdout を flush し、`http.serve` から戻る。したがって後続の文が走り、
終了コードは main のものになる。二つ目のシグナル(この後始末の間でも、`serve` が
戻った後でもよい)、または要求タイムアウト(30 秒)を過ぎても後始末が待っている
ことは、stdout を flush して終了コード 1 で終わらせ、処理中の要求には答えない。
どの停止も 128+シグナル番号では終わらない(C-350 の `0..=125`)。
対象外: HTTP のフレーミングと接続の再利用(ホストが決める)。その他のシグナル。
native の Windows では、強制停止は stdout を flush せずに終了コード 1 で終わる。
stdout のバッファには serve しているスレッドしか触れず、stdout がプロセス全体で
一つのバッファになる(almide/almide の ADR-0020 §5.5)まではそうなる。標準の 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 で、
汎用ランナーは実行しない。実装側のドライバが両レグで起動し、同じ要求列を再生して
各応答の status コード・ヘッダ集合・フレーミングを外した本文と、行の多重集合としての
stderr の記録を比べ、1 回の実行の 2 つの要求で捕捉した乱数が同じで
あることを確かめ、使用中のポートで起動して中断を比べる)
あることを確かめ、使用中のポートで起動して中断を比べる)、
`spec/serve_cross/http_serve_shutdown.almd`(同じドライバが stdout をファイルに
向けて両レグで起動する終了しないサーバー fixture。ハンドラが眠っている要求の最中に
SIGTERM を 1 回送ると、その要求に答え、`http.serve` の後に main が書く行まで
すべての行をファイルに残し、終了コード 0 で終わる。止まった要求の最中に SIGTERM を
2 回送ると、停止前に書いたすべての行を残して終了コード 1 で終わる)

Contracts: C-096, C-112, C-118, C-133, C-189, C-214, C-366, C-367。

Expand Down
Loading
Loading