diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 3aa81d51..f2415c7d 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. -134 normative sections; 824 distinct executable fixtures. +134 normative sections; 823 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_map_err_runs_every_element.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, C-370, C-374, C-375 | `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/embedded_cross/process_spawn_family.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/embedded_cross/http_response_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)
`spec/embedded_cross/http_header_refusal.almd` (both-target test)
`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)
`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/embedded_cross/process_spawn_family.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)
`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)
`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 dbadece3..f92c831a 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -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 \"\": `, 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. 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 `\n\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 \"\": `, 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" }, - { path = "spec/embedded_cross/http_response_errs.almd", class = "fixture" }, ] [[contract]] id = "C-329" diff --git a/spec/embedded_cross/http_response_errs.almd b/spec/embedded_cross/http_response_errs.almd deleted file mode 100644 index 828f298a..00000000 --- a/spec/embedded_cross/http_response_errs.almd +++ /dev/null @@ -1,46 +0,0 @@ -// @contract: C-328 -// The full-response family (#1791) on the embedded lane (#3620, op 65): every -// probe is deterministic — closed local ports and malformed urls, no live -// network — and the err texts must match native byte-for-byte (the shared -// rt-core client guarantees it by construction; this net catches a -// frame-protocol drift between the splice and the host). -import http - -effect fn main() -> Unit = { - match http.get_response("http://127.0.0.1:1/") { - ok(_) => println("get:unexpected-ok"), - err(e) => println("get:${e}"), - } - match http.post_response("http://127.0.0.1:1/x", "body") { - ok(_) => println("post:unexpected-ok"), - err(e) => println("post:${e}"), - } - match http.put_response("http://127.0.0.1:1/x", "12345") { - ok(_) => println("put:unexpected-ok"), - err(e) => println("put:${e}"), - } - match http.patch_response("http://127.0.0.1:1/x", "") { - ok(_) => println("patch:unexpected-ok"), - err(e) => println("patch:${e}"), - } - match http.delete_response("http://127.0.0.1:1/x") { - ok(_) => println("delete:unexpected-ok"), - err(e) => println("delete:${e}"), - } - match http.request_response("OPTIONS", "http://127.0.0.1:1/x", "b", ["K": "v"]) { - ok(_) => println("request:unexpected-ok"), - err(e) => println("request:${e}"), - } - match http.get_response("not-a-url") { - ok(_) => println("badurl:unexpected-ok"), - err(e) => println("badurl:${e}"), - } - match http.get_response("ftp://127.0.0.1:1/") { - ok(_) => println("scheme:unexpected-ok"), - err(e) => println("scheme:${e}"), - } - match http.request_response("GET", "http://127.0.0.1:1/x", "", ["X-A": "1\r\nX-B: 2"]) { - ok(_) => println("inject:unexpected-ok"), - err(e) => println("inject:${e}"), - } -}