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.

134 normative sections; 824 distinct executable fixtures.
134 normative sections; 823 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_map_err_runs_every_element.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, C-370, C-374, C-375 | `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/embedded_cross/process_spawn_family.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/embedded_cross/http_error_classes.almd` (both-target test)<br>`spec/embedded_cross/http_response_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)<br>`spec/embedded_cross/http_header_refusal.almd` (both-target test)<br>`spec/serve_cross/http_serve_export.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, C-374, C-375 | `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/embedded_cross/process_spawn_family.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/embedded_cross/http_error_classes.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)<br>`spec/embedded_cross/http_header_refusal.almd` (both-target test)<br>`spec/serve_cross/http_serve_export.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/line_endings_bare_cr.almd` (byte-compare)<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: 1 addition & 2 deletions docs/contracts/contracts.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4041,14 +4041,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. 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 \"<url>\": <reason>`, refused-header (C-370), dns `cannot resolve the host of \"<url>\"`, connect `could not connect to \"<url>\" (connection refused or unreachable)`, timeout `timed out waiting for \"<url>\" (raise ALMIDE_HTTP_TIMEOUT_SECS; 0 = no timeout)`, tls `TLS handshake with \"<url>\" failed`, too-large `response from \"<url>\" is larger than <n> bytes (raise ALMIDE_HTTP_MAX_RESPONSE_BYTES; 0 = no limit)` and protocol `malformed or incomplete response from \"<url>\"` β€” `<url>` 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 \"<url>\" failed (<case>)`. On p3 the invalid-url reasons are the scheme's three (missing scheme, `expected \"//\" after \"<scheme>:\"`, 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. EXTENDED (#3620): the full-response family joins the EMBEDDED lane. The embedded host serves it as framed op 65 from the same rt-core request_response the native leg calls, answering `<status>\n<hlen>\n`, then hlen chars of name/value cells in wire order with repeats kept, then the body; the http_framed splice rebuilds the HttpResponse value from that answer, so the status, every header line and the body read the same through status_code / get_header / header_values / headers / body on native and embedded, and a failure reads the same text. The NATIVE-ONLY sentence above now holds for the stock-p1 and p3 lanes only, where proofs/target-availability.toml keeps the family unavailable. spec/embedded_cross/http_response_errs.almd runs the six verbs against closed ports, malformed and unsupported urls and a refused header value on both 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. 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 \"<url>\": <reason>`, refused-header (C-370), dns `cannot resolve the host of \"<url>\"`, connect `could not connect to \"<url>\" (connection refused or unreachable)`, timeout `timed out waiting for \"<url>\" (raise ALMIDE_HTTP_TIMEOUT_SECS; 0 = no timeout)`, tls `TLS handshake with \"<url>\" failed`, too-large `response from \"<url>\" is larger than <n> bytes (raise ALMIDE_HTTP_MAX_RESPONSE_BYTES; 0 = no limit)` and protocol `malformed or incomplete response from \"<url>\"` β€” `<url>` 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 \"<url>\" failed (<case>)`. On p3 the invalid-url reasons are the scheme's three (missing scheme, `expected \"//\" after \"<scheme>:\"`, 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" },
{ path = "spec/embedded_cross/http_response_errs.almd", class = "fixture" },
]
[[contract]]
id = "C-329"
Expand Down
Loading
Loading