diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index f92c831a..1768d331 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -4041,7 +4041,7 @@ 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." +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 (ADR-0023 step 4): the full-response family is served on the stock WASI 0.3 component. The wasi:http shim answers it from the response's own fields and body (`response.get-headers`, `fields.copy-all`) and the http_framed splice rebuilds the HttpResponse value, so on native and p3 the status, `get_header`, every value of a repeated field in order (`header_values`), the lowercased header set (`headers`), the body and a failure's text read the same; the NATIVE-ONLY sentence above now holds for the embedded and stock-p1 lanes, and the embedded lane reaches the family when it runs the component (ADR-0023 step 7). The same step fixes the request framing of an empty body on p3: the shim sends `content-length: 0` unless the method is GET or HEAD, because without a length the host framed it chunked and an empty PATCH or DELETE reached the server as `0\\r\\n\\r\\n` where native sends no content." since = "0.61.1" status = "active" evidence = [