Add C-377, C-378 and C-379: net tcp on native, the embedded lane and the stock WASI 0.3 component

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 376 contracts: **requirements-first 71** (two-repo regime, since 2026-08-20),
+the `since` release was tagged). Of 379 contracts: **requirements-first 74** (two-repo regime, since 2026-08-20),
 contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 17.
 
-376 contracts
+379 contracts
 
 | ID | Contract | Since | Status | Strongest Evidence | # Fixtures |
 |----|----------|-------|--------|--------------------|-----------:|
@@ -411,4 +411,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1
 | C-374 | process on the embedded wasm host answers what native answers; a stand-alone artifact that starts a child carries the private almide:process/spawn import and is refused at load where it is not defined | 0.67.0 | active | fixture | 0 |
 | C-375 | a serve-shaped program built for stock wasm is a wasi:http/[email protected] export that wasmtime serve runs with no flags and that answers what native answers | 0.67.0 | active | fixture | 0 |
 | C-376 | A raw address taken from a Bytes block stays valid until the call it is handed to returns | 0.67.0 | active | fixture | 1 |
+| C-377 | net tcp: loopback, handle numbering, EOF, close, is_open and tcp_local_port agree on native, the embedded wasm lane and the stock WASI 0.3 component | 0.68.0 | active | fixture | 0 |
+| C-378 | net tcp: every failure reads as errno-free classified text from one table, identical on native, the embedded wasm lane and the stock WASI 0.3 component | 0.68.0 | active | fixture | 0 |
+| C-379 | net tcp: timeouts and tcp_available are guest-enforced on the stock WASI 0.3 component and answer what native and the embedded wasm lane answer | 0.68.0 | active | fixture | 0 |
 

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; 823 distinct executable fixtures.
+134 normative sections; 826 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)<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/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, C-377, C-378, C-379 | `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)<br>`spec/embedded_cross/net_tcp_loopback.almd` (both-target test)<br>`spec/embedded_cross/net_tcp_errors.almd` (both-target test)<br>`spec/embedded_cross/net_tcp_timeouts.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) |

docs/contracts/contracts.toml

@@ -4593,3 +4593,35 @@ status    = "active"
 evidence  = [
   { path = "spec/wasm_cross/bytes_rawptr.almd", class = "fixture" },
 ]
+
+# ── NET TCP ON EVERY LEG (almide/almide#3620) ──────────────────────
+[[contract]]
+id        = "C-377"
+spec      = "ALS-R5"
+title     = "net tcp: loopback, handle numbering, EOF, close, is_open and tcp_local_port agree on native, the embedded wasm lane and the stock WASI 0.3 component"
+statement = "ALS-R5 (almide/almide#3620): the `net.tcp_*` family (`tcp_listen`, `tcp_accept`, `tcp_connect`, `tcp_read`, `tcp_read_exact`, `tcp_read_timeout`, `tcp_write`, `tcp_available`, `tcp_set_timeout`, `tcp_close`, `tcp_close_listener`, `tcp_is_open`, `tcp_local_port`) answers byte-identically on the native leg, the EMBEDDED wasm lane (`almide run --target wasm`) and the stock WASI 0.3 component (`almide build --target wasm` of a program that names a net operation, run with the network granted). Handles are plain `Int`s from two tables, one for streams and one for listeners, each numbered from 0; a new handle takes the lowest free slot of its table, so a printed handle is the same number on every leg, and an unclosed handle lives until the run ends. On a loopback address one sequential program can listen, connect, accept, write and read: `tcp_connect` completes against the listen backlog before `tcp_accept` runs. `tcp_write` hands over every byte or fails; `tcp_read(s, n)` answers between 1 and n bytes once any are readable, and answers empty bytes without waiting when n is 0 and at end of stream, every time it is asked again; `tcp_read_exact(s, n)` answers exactly n bytes. `tcp_close` and `tcp_close_listener` of a handle that is already closed answer ok. `tcp_is_open` is false after the program's own `tcp_close` and for a handle never issued (negative included), and stays true after the peer closes. `net.tcp_local_port(listener) -> Result[Int, String]` answers the port the listener is bound to: a listener bound to port 0 reports the port the OS assigned, in 1..=65535, and two listeners bound to port 0 report different ports. IPv6 sockets are IPv6-only (`IPV6_V6ONLY`) on every leg, native included, so a listener on `::` accepts no IPv4 client anywhere. A host argument that is a name is resolved by the host, its addresses are tried in the resolver's order, and the first success wins, else the last address's failure. NOT covered: the port numbers themselves; dual-stack sockets, which are not offered; which addresses a name resolves to and their order across hosts (on one machine every leg asks the same resolver); the stock component's network grant: a stock host denies every socket address unless the run grants it (`wasmtime run -S inherit-network`, plus `-S allow-ip-name-lookup` when a host argument is a name rather than an IP literal); the grant is host configuration, not part of this promise. Evidence: spec/embedded_cross/net_tcp_loopback.almd, a loopback transcript on 127.0.0.1 (both handle tables with slot reuse, an echo both ways, a 0-length read, end of stream twice, close twice on both tables, `tcp_is_open`, `tcp_local_port` of two listeners bound to port 0) that the spec/embedded_cross net runs on native and on the embedded lane, and that the implementation's driver also runs as a stock component under `-S inherit-network`."
+since     = "0.68.0"
+status    = "active"
+evidence  = [
+  { path = "spec/embedded_cross/net_tcp_loopback.almd", class = "fixture" },
+]
+[[contract]]
+id        = "C-378"
+spec      = "ALS-R5"
+title     = "net tcp: every failure reads as errno-free classified text from one table, identical on native, the embedded wasm lane and the stock WASI 0.3 component"
+statement = "ALS-R5 (almide/almide#3620): every failure of a `net.tcp_*` call is an `err` whose text comes from one table and is identical on native, the EMBEDDED wasm lane and the stock WASI 0.3 component; no text carries an OS errno or the OS's own wording. `tcp_connect` and `tcp_listen` read `<fn>(<host>:<port>): <class text>`, with the host and port the program passed, and every other call reads `<fn>: <class text>`. A transport failure is classified once, as the `wasi:sockets` `error-code` case it is (native and the embedded host map the OS error the way wasmtime does), and the class texts are: access-denied `permission denied`, not-supported `operation not supported`, invalid-argument `invalid argument`, out-of-memory `out of memory`, timeout `timed out`, invalid-state `invalid socket state`, address-not-bindable `address not available`, address-in-use `address already in use`, remote-unreachable `host unreachable`, connection-refused `connection refused`, connection-broken `connection broken`, connection-reset `connection reset`, connection-aborted `connection aborted`, and `network error` for an unclassified failure that carries no message; a name that does not resolve reads `cannot resolve host \"<host>\"` and a resolver failure `name resolution failed for \"<host>\"`. These texts are decided in Almide before any transport call, the same on every leg: `invalid TcpStream handle: N` and `invalid TcpListener handle: N` for a handle never issued (negative included), `TcpStream handle N is closed` and `TcpListener handle N is closed` for a closed one (except `tcp_close` and `tcp_close_listener`, which answer ok), `<fn>: negative length N` from `tcp_read`, `tcp_read_exact` and `tcp_read_timeout` (never a panic), `tcp_read_timeout: timeout must be positive (got N ms)` for N <= 0, `tcp_read_exact: connection closed after K of N bytes` when the stream ends after K of the N bytes, and `<fn>(<host>:<port>): port out of range 0..=65535` from `tcp_connect` and `tcp_listen`. A stock run without the host's network grant loads and runs, and each bind or connect it attempts fails as access-denied, e.g. `tcp_connect(127.0.0.1:8080): permission denied`. NOT covered: the text of an unclassified failure that carries a message m (`other(some(m))` on p3), which is m and is equal only between native and the embedded lane; which names resolve, and to what (the host's resolver); the stock component's network grant: a stock host denies every socket address unless the run grants it (`wasmtime run -S inherit-network`, plus `-S allow-ip-name-lookup` when a host argument is a name rather than an IP literal); the grant is host configuration, not part of this promise. Evidence: spec/embedded_cross/net_tcp_errors.almd (handles never issued and closed on both tables, the argument-domain texts, an occupied port, a peer that closes after 3 of 5 bytes, a port whose listener was closed; the OS-assigned port masked as `<port>`), which the spec/embedded_cross net runs on native and on the embedded lane and the implementation's driver also runs as a stock component under `-S inherit-network`; the same driver runs a stock component without the grant for the `permission denied` text."
+since     = "0.68.0"
+status    = "active"
+evidence  = [
+  { path = "spec/embedded_cross/net_tcp_errors.almd", class = "fixture" },
+]
+[[contract]]
+id        = "C-379"
+spec      = "ALS-R5"
+title     = "net tcp: timeouts and tcp_available are guest-enforced on the stock WASI 0.3 component and answer what native and the embedded wasm lane answer"
+statement = "ALS-R5 (almide/almide#3620): on the stock WASI 0.3 component the guest enforces read and write timeouts and answers `tcp_available` (WASI offers no receive timeout, no peek and no readable-byte count), and every leg (native, the EMBEDDED wasm lane, the stock component) answers the same. `tcp_set_timeout(s, ms)` bounds each later read and write on s by ms milliseconds, and ms <= 0 removes the bound; the bound applies to each underlying read or write, not to a whole `tcp_read_exact` or `tcp_write`, and a call that reaches it fails `<fn>: timed out`. `tcp_read_timeout(s, n, ms)` is one read bounded by ms > 0: it answers the bytes readable within ms (at most n) or fails `tcp_read_timeout: timed out`, and afterwards s is bounded again by the `tcp_set_timeout` value it had before the call. `tcp_available(s)` answers how many bytes a read could take now without waiting, at most 65536, without consuming them, and 0 when none are readable or the stream has ended. On the stock component that count comes from a lookahead buffer the guest fills without waiting (at most 64 KiB per stream, allocated by the stream's first `tcp_available`), and every read takes the buffered bytes first, so reads answer the same bytes in the same order as on native. NOT covered: the instant a timeout fires (the wall clock), and whether bytes that arrive in the same instant as the timer are answered or the call times out (native has the same race); when a peer's bytes become readable, so `tcp_available` agrees across legs once they have arrived; the stock component's network grant: a stock host denies every socket address unless the run grants it (`wasmtime run -S inherit-network`, plus `-S allow-ip-name-lookup` when a host argument is a name rather than an IP literal); the grant is host configuration, not part of this promise. Evidence: spec/embedded_cross/net_tcp_timeouts.almd (timeouts on a stream nobody writes to, so no byte races the timer; the restored `tcp_set_timeout` bound after `tcp_read_timeout`; `tcp_available` before and after partial reads of one small write whose first byte was read, and after the peer closes), which the spec/embedded_cross net runs on native and on the embedded lane and the implementation's driver also runs as a stock component under `-S inherit-network`."
+since     = "0.68.0"
+status    = "active"
+evidence  = [
+  { path = "spec/embedded_cross/net_tcp_timeouts.almd", class = "fixture" },
+]