diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 68460074..fe1e0b99 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -28,10 +28,10 @@ Evidence classes (weakest → strongest): `doc-only` < `by-construction` < Measured per contract in [`proofs/contract-provenance.toml`](../../proofs/contract-provenance.toml) (`scripts/check-contract-provenance.py`: the instant the id entered this ledger against the instant -the `since` release was tagged). Of 369 contracts: **requirements-first 64** (two-repo regime, since 2026-08-20), +the `since` release was tagged). Of 370 contracts: **requirements-first 65** (two-repo regime, since 2026-08-20), contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 17. -369 contracts +370 contracts | ID | Contract | Since | Status | Strongest Evidence | # Fixtures | |----|----------|-------|--------|--------------------|-----------:| @@ -404,4 +404,5 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | 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 | +| C-370 | An http header that would split the request, or that the client manages, is refused with the same err on every lane | 0.66.0 | active | fixture | 0 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index a7776f70..7833a0e3 100644 --- a/docs/contracts/conformance.md +++ b/docs/contracts/conformance.md @@ -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; 810 distinct executable fixtures. +132 normative sections; 812 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------| @@ -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)
`spec/wasm_cross/repr_parity_pin.almd` (byte-compare)
`spec/wasm_cross/fuzz_found_nested_interp_capture.almd` (byte-compare)
`spec/wasm_cross/compound_repr_records_interp.almd` (byte-compare)
`spec/wasm_cross/compound_repr_recursive_interp.almd` (byte-compare)
`spec/integration/modules/cross_module_repr_test.almd` (both-target test)
`spec/integration/modules/cross_module_repr_derive_test.almd` (both-target test)
`tests/module_type_repr_test.rs` (cargo gate)
`spec/wasm_cross/recursive_generic_repr_interp.almd` (byte-compare)
`spec/wasm_cross/float_concrete.almd` (byte-compare)
`spec/wasm_cross/num_edge_to_string.almd` (byte-compare)
`spec/wasm_cross/int_float_ops.almd` (byte-compare)
`spec/wasm_cross/float_interp_forms.almd` (byte-compare)
`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)
`spec/wasm_cross/fan_map_inline_lambda.almd` (byte-compare)
`spec/wasm_cross/fan_pure_thunks.almd` (byte-compare)
`spec/wasm_cross/fan_var_thunk_list.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper_capability.almd` (byte-compare)
`spec/embedded_cross/fan_mapper_effect_callback_forms.almd` (both-target test)
`spec/wasm_cross/fan_map_err.almd` (byte-compare)
`spec/wasm_cross/fan_map_inline_err.almd` (byte-compare)
`spec/wasm_cross/fan_any_allfail.almd` (byte-compare)
`spec/wasm_cross/option_none_unwrap_term.almd` (byte-compare)
`tests/diagnostics/e027-fan-timeout-removed/broken.almd` (checker)
`tests/diagnostic_harness_test.rs` (cargo gate)
`spec/wasm_cross/fan_block_err_list_order.almd` (byte-compare)
`spec/wasm_cross/fan_prefetch_fs.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`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)
`spec/wasm_cross/random_int_entropy.almd` (byte-compare)
`spec/wasm_cross/env_args.almd` (byte-compare)
`spec/wasm_cross/env_get.almd` (byte-compare)
`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)
`spec/stdlib/process_timeout_test.almd` (both-target test)
`spec/stdlib/fs_if_exists_test.almd` (both-target test)
`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)
`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)
`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)
`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`spec/embedded_cross/http_client_errs.almd` (both-target test)
`spec/embedded_cross/http_framed_errs.almd` (both-target test)
`spec/wasm_cross/env_set_overlay.almd` (byte-compare)
`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)
`spec/stdlib/http_call_test.almd` (both-target test)
`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)
`spec/serve_cross/http_serve_replay.almd` (both-target test)
`spec/serve_cross/http_serve_shutdown.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, C-370 | `spec/wasm_cross/process_args.almd` (byte-compare)
`spec/wasm_cross/random_int_entropy.almd` (byte-compare)
`spec/wasm_cross/env_args.almd` (byte-compare)
`spec/wasm_cross/env_get.almd` (byte-compare)
`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)
`spec/stdlib/process_timeout_test.almd` (both-target test)
`spec/stdlib/fs_if_exists_test.almd` (both-target test)
`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)
`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)
`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)
`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`spec/embedded_cross/http_client_errs.almd` (both-target test)
`spec/embedded_cross/http_framed_errs.almd` (both-target test)
`spec/embedded_cross/http_error_classes.almd` (both-target test)
`spec/wasm_cross/env_set_overlay.almd` (byte-compare)
`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)
`spec/stdlib/http_call_test.almd` (both-target test)
`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)
`spec/serve_cross/http_serve_replay.almd` (both-target test)
`spec/serve_cross/http_serve_shutdown.almd` (both-target test)
`spec/embedded_cross/http_header_refusal.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)
`spec/wasm_cross/fs_relative_path.almd` (byte-compare)
`spec/stdlib/fs_stat_test.almd` (both-target test)
`spec/stdlib/fs_streaming_test.almd` (both-target test)
`spec/stdlib/fs_fold_lines_range_test.almd` (both-target test)
`spec/stdlib/fs_fold_lines_chunked_test.almd` (both-target test)
`spec/wasm_cross/line_endings_bare_cr.almd` (byte-compare)
`spec/wasm_cross/fs_read_lines.almd` (byte-compare)
`spec/wasm_cross/fs_metadata_family.almd` (byte-compare)
`spec/wasm_cross/fs_composition_family.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows.almd` (byte-compare)
`spec/wasm_cross/fs_glob_segments.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows_oob.almd` (byte-compare)
`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows_q1_partial_block.almd` (byte-compare)
`spec/wasm_cross/bytes_negative_offset_family.almd` (byte-compare)
`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare)
`spec/wasm_cross/matrix_q1_full_loader_cols_beyond_buffer.almd` (byte-compare)
`spec/wasm_cross/flight_pid_control.almd` (byte-compare)
`spec/wasm_cross/matrix_q_fp16_scale_domain.almd` (byte-compare)
`spec/wasm_cross/fs_list_dir_multipass.almd` (byte-compare)
`spec/wasm_cross/fs_write_errno.almd` (byte-compare)
`spec/wasm_fail/rope_geometry_exceeds_aborts.almd` (both-target test)
`spec/wasm_cross/rope_geometry_family.almd` (byte-compare)
`spec/wasm_cross/rope_at_family.almd` (byte-compare)
`spec/wasm_fail/matrix_index_oob_aborts.almd` (both-target test)
`spec/wasm_cross/matrix_index_domain_family.almd` (byte-compare)
`spec/wasm_cross/callee_shadowing_family.almd` (byte-compare)
`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)
`spec/wasm_cross/fs_fallible_stream_callback.almd` (byte-compare)
`spec/stdlib/fs_streaming_test.almd` (both-target test)
`tests/fs_streaming_family_gate_test.rs` (cargo gate)
`spec/wasm_cross/path_extension_hidden.almd` (byte-compare) | | ALS-R8 | C-275, C-368 | `spec/wasm_cross/http_response_headers.almd` (byte-compare)
`spec/stdlib/http_router_test.almd` (both-target test) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 4ef424eb..9336e207 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -4022,7 +4022,7 @@ evidence = [ id = "C-330" spec = "ALS-R5" title = "The http string family answers on the stock runtime through the p3 component's async-lowered exchange" -statement = "http.get/post/put/patch/delete (fs_call ops 43..=47) and the framed family — request / request_status / get_status / request_bytes / get_bytes (ops 48..=50: the method as its named variant case or `other(string)`, the headers through `fields.append`, `request_status` prefixed with the decimal status) — are served by the ALMIDE_COMPONENT_P3 artifact over wasi:http@0.3 on a stock wasmtime (`-S p3=y -S http=y`, the pin-policy flag surface): ok answers carry the decoded response body and transport failures answer err with the static E_HTTP text (host-specific wording is NOT promised across lanes — C-328's shared-client wording guarantee is embedded/native only). The exchange shape is load-bearing, not stylistic: the trailers future-write, the body stream-writes and client.send are all [async-lower] builtins joined on one waitable set and drained by a guest scheduler loop, because each sync lower parks the fiber on a rendezvous whose reader only appears inside send — the bring-up bisect hung exactly at the sync trailers write, and a body past the host's 1MiB http-outgoing-body-buffer-chunks rendezvous buffer deadlocks any shape that cannot keep feeding the stream while send is in flight. The pinning fixture drives all five family members through a live local server in one component run, with a 2MiB PUT crossing that buffer on purpose, under a deadlock watchdog. FOUR SHAPES CLOSED TOGETHER (#1924): a transport-errored exchange leaves the shim's bookkeeping intact — send's result is parked in its own 112-byte slot (SENDRET), not the RET scratch where the trailers future's pending ok(none) buffer lives, because an `err` payload's string pointers scribbled that buffer and the NEXT exchange trapped lifting it (`failed to read result … unknown handle index `); the waitable set is dropped on every leg, not leaked per failed exchange; the status of `request_status`/`get_status` is read BEFORE consume-body takes the response by value (a bare `get_status` as the first call trapped `index 3 is not a resource`); the framed family's header NAME keeps its own locals (parked in the authority's, it clobbered `set-authority` with the first header name — a DNS error on every framed request carrying a header); and a non-empty body carries `content-length` (before, the host's default `transfer-encoding: chunked` read as an EMPTY body on a server without chunked support, where the native lane's client always sends content-length). The echo test reflects the framing (`framing:cl`), and `p3_http_transport_error_leaves_the_next_exchange_intact` runs every shape in sequence against one echo with a refused port between them." +statement = "http.get/post/put/patch/delete (fs_call ops 43..=47) and the framed family — request / request_status / get_status / request_bytes / get_bytes (ops 48..=50: the method as its named variant case or `other(string)`, the headers through `fields.append`, `request_status` prefixed with the decimal status) — are served by the ALMIDE_COMPONENT_P3 artifact over wasi:http@0.3 on a stock wasmtime (`-S http=y`, the pin-policy flag surface: the capability grant, with no `-W` or `-S p3` flag since ADR-0023 step 1): ok answers carry the decoded response body, and a failure answers err in C-328's classified text, the same as on native and the embedded lane (ADR-0023 step 2). The exchange shape is load-bearing, not stylistic: the trailers future-write, the body stream-writes and client.send are all [async-lower] builtins joined on one waitable set and drained by a guest scheduler loop, because each sync lower parks the fiber on a rendezvous whose reader only appears inside send — the bring-up bisect hung exactly at the sync trailers write, and a body past the host's 1MiB http-outgoing-body-buffer-chunks rendezvous buffer deadlocks any shape that cannot keep feeding the stream while send is in flight. The pinning fixture drives all five family members through a live local server in one component run, with a 2MiB PUT crossing that buffer on purpose, under a deadlock watchdog. FOUR SHAPES CLOSED TOGETHER (#1924): a transport-errored exchange leaves the shim's bookkeeping intact — send's result is parked in its own 112-byte slot (SENDRET), not the RET scratch where the trailers future's pending ok(none) buffer lives, because an `err` payload's string pointers scribbled that buffer and the NEXT exchange trapped lifting it (`failed to read result … unknown handle index `); the waitable set is dropped on every leg, not leaked per failed exchange; the status of `request_status`/`get_status` is read BEFORE consume-body takes the response by value (a bare `get_status` as the first call trapped `index 3 is not a resource`); the framed family's header NAME keeps its own locals (parked in the authority's, it clobbered `set-authority` with the first header name — a DNS error on every framed request carrying a header); and a non-empty body carries `content-length` (before, the host's default `transfer-encoding: chunked` read as an EMPTY body on a server without chunked support, where the native lane's client always sends content-length). The echo test reflects the framing (`framing:cl`), and `p3_http_transport_error_leaves_the_next_exchange_intact` runs every shape in sequence against one echo with a refused port between them." since = "0.62.0" status = "active" evidence = [ @@ -4034,12 +4034,13 @@ evidence = [ id = "C-328" spec = "ALS-R5" title = "The http string family answers identically on the native and embedded-wasm lanes" -statement = "http.get/post/put/patch/delete answer byte-identically on the native leg and the EMBEDDED wasm lane (`almide run --target wasm`, #1710 increment 1): the embedded host serves fs_call ops 43..=47 with the shared rt-core client (crates/almide-rt-core), so transport-error texts — connection refusal, DNS failure, the timeout wording and its env-var hint, the close-without-close_notify tolerance, chunked framing — match by shared code, and a drift fails the spec/embedded_cross net (tests/embedded_cross_test.rs). Increment 3 extends the same promise to the FRAMED family — http.request / request_status / get_status / request_bytes / get_bytes ride ops 48..=50 with (method, body, headers) serialized into one decimal char-length frame by the http_framed splice and parsed by the host with the same char arithmetic; a frame-protocol drift between splice and host diverges the net (spec/embedded_cross/http_framed_errs.almd). E081 is a PER-LEG verdict from the same increment: the run/bench route walls only on rows declaring the embedded leg, so the served family runs without the ALMIDE_NO_AVAIL_CHECK escape (retired from the net harness), while STOCK artifacts keep refusing these ops at BUILD time through the emitted-op audit — never a runtime refusal on a runtime the developer never ran; the stock/component story is the rest of #1710. EXTENDED (#1791, 0.61.2): the full-response family (http.get_response / post_response / put_response / patch_response / delete_response / request_response, answering the whole HttpResponse record — status, every header line in wire order with repeats kept, body — for ANY complete response, redirects never followed) is NATIVE-ONLY: proofs/target-availability.toml declares it unavailable on the structural, stock-p1 and embedded legs until the wasi:http port (#1710) grows the response shape. The body-only and (status, body) shapes are PROJECTIONS of the same rt-core exchange (request_response), so this promise's byte-identity for the served shapes is inherited, not re-measured; the family's completeness rule is pinned by tests/http_response_family_gate_test.rs and its native behaviour (status, first / all / lowercased-map header reads, body) by the loopback round-trip in spec/stdlib/http_status_test.almd." +statement = "http.get/post/put/patch/delete answer byte-identically on the native leg and the EMBEDDED wasm lane (`almide run --target wasm`, #1710 increment 1): the embedded host serves fs_call ops 43..=47 with the shared rt-core client (crates/almide-rt-core), so transport-error texts — connection refusal, DNS failure, the timeout wording and its env-var hint, the close-without-close_notify tolerance, chunked framing — match by shared code, and a drift fails the spec/embedded_cross net (tests/embedded_cross_test.rs). Increment 3 extends the same promise to the FRAMED family — http.request / request_status / get_status / request_bytes / get_bytes ride ops 48..=50 with (method, body, headers) serialized into one decimal char-length frame by the http_framed splice and parsed by the host with the same char arithmetic; a frame-protocol drift between splice and host diverges the net (spec/embedded_cross/http_framed_errs.almd). E081 is a PER-LEG verdict from the same increment: the run/bench route walls only on rows declaring the embedded leg, so the served family runs without the ALMIDE_NO_AVAIL_CHECK escape (retired from the net harness), while STOCK artifacts keep refusing these ops at BUILD time through the emitted-op audit — never a runtime refusal on a runtime the developer never ran; the stock/component story is the rest of #1710. EXTENDED (#1791, 0.61.2): the full-response family (http.get_response / post_response / put_response / patch_response / delete_response / request_response, answering the whole HttpResponse record — status, every header line in wire order with repeats kept, body — for ANY complete response, redirects never followed) is NATIVE-ONLY: proofs/target-availability.toml declares it unavailable on the structural, stock-p1 and embedded legs until the wasi:http port (#1710) grows the response shape. The body-only and (status, body) shapes are PROJECTIONS of the same rt-core exchange (request_response), so this promise's byte-identity for the served shapes is inherited, not re-measured; the family's completeness rule is pinned by tests/http_response_family_gate_test.rs and its native behaviour (status, first / all / lowercased-map header reads, body) by the loopback round-trip in spec/stdlib/http_status_test.almd. EXTENDED (ADR-0023 step 2, 0.66.0): the promise has a third lane, the stock WASI 0.3 component (`wasmtime run -S http=y`, C-330), and an exchange compares on status, the lowercased header set, the body and the error class on native, embedded and p3 (the header set is observable only through the full-response family, native-only above). Every client failure is classified once and written by one renderer from the table in crates/almide-rt-core/src/http_error_core.rs, which native and the embedded host render from and the p3 shim lays out as data, so a classified failure reads the same on the three lanes: invalid-url `invalid URL \"\": `, refused-header (C-370), dns `cannot resolve the host of \"\"`, connect `could not connect to \"\" (connection refused or unreachable)`, timeout `timed out waiting for \"\" (raise ALMIDE_HTTP_TIMEOUT_SECS; 0 = no timeout)`, tls `TLS handshake with \"\" failed`, too-large `response from \"\" is larger than bytes (raise ALMIDE_HTTP_MAX_RESPONSE_BYTES; 0 = no limit)` and protocol `malformed or incomplete response from \"\"` — `` is the URL the program passed, quoted with `\\\"`, `\\\\`, `\\t`, `\\r`, `\\n`, `\\0` and `\\u{..}` (lowercase hex) for the other ASCII controls and DEL, and no text carries an OS errno or a TLS library's reason. The p3 shim maps the wasi:http `error-code` cases by name: DNS-timeout, DNS-error and destination-not-found to dns; destination-unavailable, destination-IP-prohibited, destination-IP-unroutable, connection-refused and connection-limit-reached to connect; connection-timeout, connection-read-timeout, connection-write-timeout and HTTP-response-timeout to timeout; the three TLS cases to tls; connection-terminated and the response-side HTTP cases to protocol. It reads ALMIDE_HTTP_TIMEOUT_SECS (default 30 s, as the connect, first-byte and between-bytes request options; 0 leaves the host's default) and ALMIDE_HTTP_MAX_RESPONSE_BYTES (default 1 GiB, counted on the body as it arrives) from the component's environment. What is not classified keeps a text of its own, equal between native and embedded only: a proxy's failure (naming the proxy), a trust store the SSL_CERT_* variables name that does not load, and on p3 `internal-error(some(msg))` as `msg` and any other case as `http request to \"\" failed ()`. On p3 the invalid-url reasons are the scheme's three (missing scheme, `expected \"//\" after \":\"`, unsupported scheme); a bad host or port is refused by the runtime and reads as the unclassified text naming HTTP-request-URI-invalid. WHETHER a limit fires near its boundary is the lane's (native counts the whole response, p3 the body) while the text is pinned. spec/embedded_cross/http_error_classes.almd (the scheme reasons, the escapes, a closed port) runs on the three lanes, and the implementation adds a stalled server, a plain-TCP server under https and an oversized response to the same comparison." since = "0.61.1" status = "active" evidence = [ { path = "spec/embedded_cross/http_client_errs.almd", class = "fixture" }, { path = "spec/embedded_cross/http_framed_errs.almd", class = "fixture" }, + { path = "spec/embedded_cross/http_error_classes.almd", class = "fixture" }, ] [[contract]] id = "C-329" @@ -4477,7 +4478,7 @@ evidence = [ id = "C-366" spec = "ALS-R5" title = "http call handle: per-call limits name themselves when they fire, cancel closes the connection, poll never blocks" -statement = "`http.start(method, url, body, headers, limits)` returns at once with an `HttpCall`; `poll` and `read_new` never block, `wait` blocks until the call ends, and `cancel` (or dropping the last copy of the handle) ends a running call as `err(\"request cancelled\")` and shuts its connection down, so the server observes the close and `read_new` answers `\"\"` from then on. The limits are per call, `{ total_ms, idle_ms }` in milliseconds with 0 = no limit: `total_ms` is a wall clock from `start` (dial, first byte and body all count) and `idle_ms` the longest gap between arrivals of bytes (the wait for the first byte included); a fired limit ends the call as exactly `err(\"request timeout: total_ms exceeded\")` or `err(\"request timeout: idle_ms exceeded\")`, the `_with_limits` twins of request_stream / openai_streaming_call / anthropic_streaming_call end the same way, and ALMIDE_HTTP_TIMEOUT_SECS stays the default of the calls without limits only. As with C-214, WHETHER a limit fires is the host's (the fixtures use wide margins) while the error shape is pinned. On the wasm target the embedded lane (`almide run --target wasm`) serves `start` / `poll` / `read_new` / `wait` / `cancel` and `request_stream_with_limits` with the same observables — the same error texts, the connection shut on cancel, and dropping the last copy of a handle cancelling its call — while the stock artifact (`almide build --target wasm`, the route `almide check --target wasm` checks) refuses the family with E081, and the openai / anthropic `_with_limits` twins stay native-only." +statement = "`http.start(method, url, body, headers, limits)` returns at once with an `HttpCall`; `poll` and `read_new` never block, `wait` blocks until the call ends, and `cancel` (or dropping the last copy of the handle) ends a running call as `err(\"request cancelled\")` and shuts its connection down, so the server observes the close and `read_new` answers `\"\"` from then on. The limits are per call, `{ total_ms, idle_ms }` in milliseconds with 0 = no limit: `total_ms` is a wall clock from `start` (dial, first byte and body all count) and `idle_ms` the longest gap between arrivals of bytes (the wait for the first byte included); a fired limit ends the call as exactly `err(\"request timeout: total_ms exceeded\")` or `err(\"request timeout: idle_ms exceeded\")`, the `_with_limits` twins of request_stream / openai_streaming_call / anthropic_streaming_call end the same way, and ALMIDE_HTTP_TIMEOUT_SECS stays the default of the calls without limits only. As with C-214, WHETHER a limit fires is the host's (the fixtures use wide margins) while the error shape is pinned. On the wasm target the embedded lane (`almide run --target wasm`) serves `start` / `poll` / `read_new` / `wait` / `cancel` and `request_stream_with_limits` with the same observables — the same error texts, the connection shut on cancel, and dropping the last copy of a handle cancelling its call — while the stock artifact (`almide build --target wasm`, the route `almide check --target wasm` checks) refuses the family with E081, and the openai / anthropic `_with_limits` twins stay native-only. The stock p3 component (ALMIDE_COMPONENT_P3 under `--component`, run as `wasmtime run -S http=y`) refuses the family at build time with E081 as the p1 artifact does; it does not serve the call handle, so the guest-enforced `total_ms`, `idle_ms` and `cancel` of ADR-0023 §4.3 are not observable there." since = "0.64.0" status = "active" evidence = [ @@ -4488,7 +4489,7 @@ 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:` 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: ` with `Content-Type: text/plain`; a bind failure ABORTS the run with `Error: bind failed: ` 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." +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:` 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: ` with `Content-Type: text/plain`; a bind failure ABORTS the run with `Error: bind failed: ` 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 the stock p3 component (ALMIDE_COMPONENT_P3 under `--component`) refuses it at build time with E081 too: it exports no `wasi:http/handler@0.3.0`, which is ADR-0023 step 8's shape and not described here (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 = [ @@ -4515,3 +4516,13 @@ status = "active" evidence = [ { path = "spec/wasm_cross/lambda_failure_channel.almd", class = "fixture" }, ] +[[contract]] +id = "C-370" +spec = "ALS-R5" +title = "An http header that would split the request, or that the client manages, is refused with the same err on every lane" +statement = "Before anything is dialled, the http client checks each header of a request in order: its name, then its value, then its name against the fields the client manages, and answers `err` with the first refusal. A name that is not an RFC 9110 token (empty, or holding a space, colon, control or line break) is `invalid header name \"\": a field name is a token (RFC 9110) — no spaces, colons, controls or line breaks`; a value holding CR, LF, NUL or any other control but HTAB, or DEL, is `invalid header value for \"\": it contains CR, LF, NUL or another control character, which would split the request`; and a name equal, ASCII case-insensitively, to connection, keep-alive, proxy-authenticate, proxy-authorization, proxy-connection, transfer-encoding, upgrade, host or http2-settings (the fields the client writes itself or a stock wasi:http host forbids) is `forbidden header name \"\": the HTTP client manages this field`. The name is quoted with C-328's escapes, and the text is the same on native, the embedded lane (`almide run --target wasm`) and the stock p3 component, whose shim checks the framed family's headers itself before any request exists and answers a host's `header-error` with the third text. It is a runtime `err`, never a compile rejection. Before it, native sent the nine names and the p3 shim dropped a header its host refused without a word. spec/embedded_cross/http_header_refusal.almd pins every refusal on a closed port, where a header that passes reads as C-328's connect text." +since = "0.66.0" +status = "active" +evidence = [ + { path = "spec/embedded_cross/http_header_refusal.almd", class = "fixture" }, +] diff --git a/docs/specs/als/README.md b/docs/specs/als/README.md index 74effd99..d73e4243 100644 --- a/docs/specs/als/README.md +++ b/docs/specs/als/README.md @@ -116,7 +116,7 @@ | [ALS-R2](./runtime.md#als-r2-補間の表示形) | 補間の表示形 | C-008, C-009, C-010, C-011, C-222 | | [ALS-R3](./runtime.md#als-r3-fan-並行コンビネータの決定性) | fan 並行コンビネータの決定性 | C-004, C-005, C-006, C-199, C-321, C-349 | | [ALS-R4](./runtime.md#als-r4-非有限浮動小数の定数表示) | 非有限浮動小数の定数表示 | C-012 | -| [ALS-R5](./runtime.md#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 | +| [ALS-R5](./runtime.md#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, C-370 | | [ALS-R6](./runtime.md#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 | | [ALS-R7](./runtime.md#als-r7-ストリーミング行走査の可謬コールバック) | ストリーミング行走査の可謬コールバック | C-274, C-335 | | [ALS-R8](./runtime.md#als-r8-http-レスポンスヘッダの規範) | HTTP レスポンスヘッダの規範 | C-275, C-368 | diff --git a/proofs/contract-provenance.toml b/proofs/contract-provenance.toml index 0464412b..70684c38 100644 --- a/proofs/contract-provenance.toml +++ b/proofs/contract-provenance.toml @@ -2779,3 +2779,10 @@ since = "0.65.0" entry = "2026-09-27T19:00:23+09:00" entry_commit = "d6177e1" class = "requirements-first" + +[[contract]] +id = "C-370" +since = "0.66.0" +entry = "2026-09-28T14:56:42+09:00" +entry_commit = "e854238" +class = "requirements-first" diff --git a/spec/embedded_cross/http_error_classes.almd b/spec/embedded_cross/http_error_classes.almd new file mode 100644 index 00000000..76497407 --- /dev/null +++ b/spec/embedded_cross/http_error_classes.almd @@ -0,0 +1,27 @@ +// @contract: C-328 +// The client's error classes (ADR-0023 §4.2) that need no server: the three +// scheme reasons of invalid-url (a URL with a tab and a quote shows the +// operand's escapes) and connect, on a closed local port. Every text names +// the URL the program passed and carries no OS errno, so native, the +// embedded lane and the stock p3 component read the same; +// tests/http_error_class_cross_test.rs runs this file on all three and +// adds the classes that need a local server (timeout, tls, too-large). +import http + +fn show(tag: String, r: Result[String, String]) -> Unit = { + match r { + ok(_) => println("${tag}: unexpected ok"), + err(e) => println("${tag}: ${e}"), + } +} + +effect fn main() -> Unit = { + show("unsupported", http.get("ftp://example.com/x")) + show("unsupported-upper", http.get("FTP://example.com/x")) + show("no-scheme", http.get("example.com/x")) + show("slashes", http.get("HTTP:/x")) + show("escaped", http.get("x\ty\"z")) + show("connect-get", http.get("http://127.0.0.1:9/")) + show("connect-post", http.post("http://127.0.0.1:9/x", "{}")) + show("connect-framed", http.request("PUT", "http://127.0.0.1:9/x", "y", ["X-Ok": "fine"])) +} diff --git a/spec/embedded_cross/http_header_refusal.almd b/spec/embedded_cross/http_header_refusal.almd new file mode 100644 index 00000000..3e5e4b38 --- /dev/null +++ b/spec/embedded_cross/http_header_refusal.almd @@ -0,0 +1,35 @@ +// @contract: C-370 +// Header refusal (C-370): before anything is dialled, a header name that is +// not a token, a value holding a control, and a name the client manages +// (any case) answer err with the name quoted — the same text on native, +// the embedded lane and the stock p3 component, where the shim checks the +// frame itself (tests/http_error_class_cross_test.rs runs all three). The +// port is closed, so a header that passes reads as the connect class. +import http + +fn show(tag: String, r: Result[String, String]) -> Unit = { + match r { + ok(_) => println("${tag}: unexpected ok"), + err(e) => println("${tag}: ${e}"), + } +} + +effect fn main() -> Unit = { + let url = "http://127.0.0.1:9/" + show("name-space", http.request("GET", url, "", ["x bad": "v"])) + show("name-colon", http.request("GET", url, "", ["x:y": "v"])) + show("value-crlf", http.request("GET", url, "", ["X-A": "a\r\nInjected: 1"])) + show("value-nul", http.request("GET", url, "", ["X-A": "a\u{0}b"])) + show("host", http.request("GET", url, "", ["Host": "evil.example"])) + show("connection", http.request("GET", url, "", ["connection": "keep-alive"])) + show("transfer-encoding", http.request("POST", url, "b", ["Transfer-Encoding": "chunked"])) + show( + "upgrade", + http.request_status("GET", url, "", ["UPGRADE": "h2c"]) |> result.map(((c, b)) => b), + ) + show( + "proxy-authorization", + http.request_bytes("GET", url, "", ["Proxy-Authorization": "x"]) |> result.map((b) => "bytes"), + ) + show("sendable", http.request("GET", url, "", ["X-Ok": "fine"])) +}