From e786ba3d941911fa27da93e8432703b20d8fc0e6 Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Tue, 13 Oct 2026 01:32:57 +0900 Subject: [PATCH 1/3] Add the net tcp loopback, error-text and timeout fixtures for the embedded and stock wasm legs Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/embedded_cross/net_tcp_errors.almd | 72 +++++++++++++++++++++++ spec/embedded_cross/net_tcp_loopback.almd | 67 +++++++++++++++++++++ spec/embedded_cross/net_tcp_timeouts.almd | 66 +++++++++++++++++++++ 3 files changed, 205 insertions(+) create mode 100644 spec/embedded_cross/net_tcp_errors.almd create mode 100644 spec/embedded_cross/net_tcp_loopback.almd create mode 100644 spec/embedded_cross/net_tcp_timeouts.almd diff --git a/spec/embedded_cross/net_tcp_errors.almd b/spec/embedded_cross/net_tcp_errors.almd new file mode 100644 index 00000000..6b3bf10b --- /dev/null +++ b/spec/embedded_cross/net_tcp_errors.almd @@ -0,0 +1,72 @@ +// @contract: C-378 +// net tcp failure texts (#3620): every failure is errno-free text from one +// table, identical on native, the embedded lane and the stock WASI 0.3 +// component. Connect and listen read `(:): `, +// the rest `: `, and the Almide-local texts (handles, +// argument domains, an early EOF under read_exact) are decided before any +// transport call. The OS-assigned port differs per run, so it is masked as +// `` before printing. Staged in one program on 127.0.0.1: an occupied +// port (address in use) and a port whose listener was closed (connection +// refused). No name lookup: a literal IP needs only the network grant. +import net + +fn show_int(r: Result[Int, String]) -> String = match r { + ok(v) => "ok ${v}", + err(e) => "err ${e}", +} + +fn show_masked(r: Result[Int, String], port: Int) -> String = match r { + ok(_) => "ok", + err(e) => "err ${string.replace(e, int.to_string(port), "")}", +} + +fn show_bytes(r: Result[Bytes, String]) -> String = match r { + ok(b) => "ok ${bytes.len(b)} [${bytes.to_string(b) ?? ""}]", + err(e) => "err ${e}", +} + +fn show_unit(r: Result[Unit, String]) -> String = match r { + ok(_) => "ok", + err(e) => "err ${e}", +} + +effect fn main() -> Unit = { + // Handles that were never issued, and argument domains. + println(show_bytes(net.tcp_read(7, 1))) + println(show_bytes(net.tcp_read(-1, 1))) + println(show_unit(net.tcp_write(7, bytes.from_string("x")))) + println(show_unit(net.tcp_close(99))) + println(show_int(net.tcp_accept(5))) + println(show_unit(net.tcp_close_listener(99))) + println(show_int(net.tcp_local_port(5))) + println(show_int(net.tcp_connect("127.0.0.1", 70000))) + println(show_int(net.tcp_listen("127.0.0.1", -1))) + let l = net.tcp_listen("127.0.0.1", 0)! + let port = net.tcp_local_port(l)! + let c = net.tcp_connect("127.0.0.1", port)! + let s = net.tcp_accept(l)! + println("handles: listener=${l} client=${c} accepted=${s}") + println(show_bytes(net.tcp_read(c, -1))) + println(show_bytes(net.tcp_read_exact(c, -3))) + println(show_bytes(net.tcp_read_timeout(c, -2, 50))) + println(show_bytes(net.tcp_read_timeout(c, 4, 0))) + println(show_bytes(net.tcp_read_timeout(c, 4, -5))) + // An occupied port. + println(show_masked(net.tcp_listen("127.0.0.1", port), port)) + // The peer closes after 3 of the 5 bytes read_exact waits for. + net.tcp_write(c, bytes.from_string("abc"))! + println("close client: ${show_unit(net.tcp_close(c))}") + println(show_bytes(net.tcp_read_exact(s, 5))) + // Closed stream handles. + println(show_bytes(net.tcp_read(c, 1))) + println(show_unit(net.tcp_write(c, bytes.from_string("x")))) + println(show_int(net.tcp_available(c))) + println(show_unit(net.tcp_set_timeout(c, 10))) + println("close accepted: ${show_unit(net.tcp_close(s))}") + // A port nobody listens on any more, and a closed listener handle. + println("close listener: ${show_unit(net.tcp_close_listener(l))}") + println(show_masked(net.tcp_connect("127.0.0.1", port), port)) + println(show_int(net.tcp_accept(l))) + println(show_int(net.tcp_local_port(l))) + println("done") +} diff --git a/spec/embedded_cross/net_tcp_loopback.almd b/spec/embedded_cross/net_tcp_loopback.almd new file mode 100644 index 00000000..5c29f1c5 --- /dev/null +++ b/spec/embedded_cross/net_tcp_loopback.almd @@ -0,0 +1,67 @@ +// @contract: C-377 +// net tcp loopback inside one program (#3620): listen on 127.0.0.1 port 0, +// read the OS-assigned port with `net.tcp_local_port`, connect, accept, +// write, read, close. `connect` completes against the listen backlog before +// `accept` runs, so one sequential program stages both ends on every leg. +// Every line is a value native, the embedded lane (`almide run --target +// wasm`) and the stock WASI 0.3 component (`wasmtime run -S inherit-network`) +// print byte for byte: the port itself differs per run, so it is printed only +// as predicates. Handles are plain Ints from two tables (streams, listeners), +// each numbered from 0, a new handle taking the lowest free slot, so the +// numbers below are part of the transcript. Payloads stay far below 8 KiB: +// a large write before the peer reads can stall a single-threaded program. +import net + +fn show_bytes(r: Result[Bytes, String]) -> String = match r { + ok(b) => "ok ${bytes.len(b)} [${bytes.to_string(b) ?? ""}]", + err(e) => "err ${e}", +} + +fn show_unit(r: Result[Unit, String]) -> String = match r { + ok(_) => "ok", + err(e) => "err ${e}", +} + +effect fn main() -> Unit = { + let l0 = net.tcp_listen("127.0.0.1", 0)! + println("listener l0=${l0}") + let port = net.tcp_local_port(l0)! + println("l0 port in 1..=65535: ${port >= 1 and port <= 65535}") + let c0 = net.tcp_connect("127.0.0.1", port)! + let s1 = net.tcp_accept(l0)! + println("client c0=${c0} accepted s1=${s1}") + println("open: c0=${net.tcp_is_open(c0)} s1=${net.tcp_is_open(s1)}") + net.tcp_write(c0, bytes.from_string("hello"))! + println("s1 read_exact 5: ${show_bytes(net.tcp_read_exact(s1, 5))}") + net.tcp_write(s1, bytes.from_string("world!"))! + println("c0 read_exact 6: ${show_bytes(net.tcp_read_exact(c0, 6))}") + println("c0 read 0: ${show_bytes(net.tcp_read(c0, 0))}") + // EOF reads as empty bytes, every time; a peer close is not seen by is_open. + println("close c0: ${show_unit(net.tcp_close(c0))}") + println("s1 read after peer close: ${show_bytes(net.tcp_read(s1, 16))}") + println("s1 read again: ${show_bytes(net.tcp_read(s1, 16))}") + println("open after peer close: s1=${net.tcp_is_open(s1)}") + println("open after own close: c0=${net.tcp_is_open(c0)}") + println("close c0 twice: ${show_unit(net.tcp_close(c0))}") + // Stream slot 0 is free again: the next stream takes it, the one after takes 2. + let c2 = net.tcp_connect("127.0.0.1", port)! + let s3 = net.tcp_accept(l0)! + println("reused: client=${c2} accepted=${s3}") + net.tcp_write(s3, bytes.from_string("again"))! + println("client read_exact 5: ${show_bytes(net.tcp_read_exact(c2, 5))}") + // Listener numbering: a second listener is 1; after closing 0 the next is 0. + let l1 = net.tcp_listen("127.0.0.1", 0)! + let port1 = net.tcp_local_port(l1)! + println("listener l1=${l1} distinct port: ${port1 != port and port1 >= 1}") + println("close l0: ${show_unit(net.tcp_close_listener(l0))}") + println("close l0 twice: ${show_unit(net.tcp_close_listener(l0))}") + let l2 = net.tcp_listen("127.0.0.1", 0)! + println("listener after close: ${l2}") + println("open(-1)=${net.tcp_is_open(-1)} open(99)=${net.tcp_is_open(99)}") + println("close s1: ${show_unit(net.tcp_close(s1))}") + println("close c2: ${show_unit(net.tcp_close(c2))}") + println("close s3: ${show_unit(net.tcp_close(s3))}") + println("close l1: ${show_unit(net.tcp_close_listener(l1))}") + println("close l2: ${show_unit(net.tcp_close_listener(l2))}") + println("done") +} diff --git a/spec/embedded_cross/net_tcp_timeouts.almd b/spec/embedded_cross/net_tcp_timeouts.almd new file mode 100644 index 00000000..dae05899 --- /dev/null +++ b/spec/embedded_cross/net_tcp_timeouts.almd @@ -0,0 +1,66 @@ +// @contract: C-379 +// net tcp timeouts and `tcp_available` (#3620). Both are guest-enforced on +// the stock WASI 0.3 component (WASI has no SO_RCVTIMEO, no peek and no +// FIONREAD), and the transcript below is the same on native, the embedded +// lane and the component. Every timeout here fires on a stream nobody +// writes to, so no byte can race the timer and the outcome is fixed; only +// WHEN it fires is the clock's. `tcp_available` is asked only after the +// first byte of the writer's one small write was read, so the count is +// settled. `tcp_read_timeout` restores the earlier `tcp_set_timeout` value: +// the plain `tcp_read` after it times out at 100 ms instead of blocking. +import net + +fn show_bytes(r: Result[Bytes, String]) -> String = match r { + ok(b) => "ok ${bytes.len(b)} [${bytes.to_string(b) ?? ""}]", + err(e) => "err ${e}", +} + +fn show_int(r: Result[Int, String]) -> String = match r { + ok(v) => "ok ${v}", + err(e) => "err ${e}", +} + +fn show_unit(r: Result[Unit, String]) -> String = match r { + ok(_) => "ok", + err(e) => "err ${e}", +} + +effect fn main() -> Unit = { + let l = net.tcp_listen("127.0.0.1", 0)! + let port = net.tcp_local_port(l)! + let c = net.tcp_connect("127.0.0.1", port)! + let s = net.tcp_accept(l)! + // read_timeout: nothing sent, then bytes already waiting. + println("read_timeout, idle: ${show_bytes(net.tcp_read_timeout(s, 4, 50))}") + net.tcp_write(c, bytes.from_string("ping"))! + println("read_timeout, waiting: ${show_bytes(net.tcp_read_timeout(s, 16, 5000))}") + // available: bytes readable now, without consuming them. + println("available, idle: ${show_int(net.tcp_available(s))}") + // When bytes arrive is the network's: block for the first byte of one + // small write, after which the rest of that write is readable too. + net.tcp_write(c, bytes.from_string("abcdef"))! + println("read_exact 1: ${show_bytes(net.tcp_read_exact(s, 1))}") + println("available after 1 of 6: ${show_int(net.tcp_available(s))}") + println("available again: ${show_int(net.tcp_available(s))}") + println("read 2: ${show_bytes(net.tcp_read(s, 2))}") + println("available after read 2: ${show_int(net.tcp_available(s))}") + println("read_exact 3: ${show_bytes(net.tcp_read_exact(s, 3))}") + println("available drained: ${show_int(net.tcp_available(s))}") + // set_timeout bounds plain reads; read_timeout leaves it in place. + println("set_timeout 100: ${show_unit(net.tcp_set_timeout(s, 100))}") + println("read, idle: ${show_bytes(net.tcp_read(s, 4))}") + println("read_exact, idle: ${show_bytes(net.tcp_read_exact(s, 4))}") + println("read_timeout 30, idle: ${show_bytes(net.tcp_read_timeout(s, 4, 30))}") + println("read after read_timeout: ${show_bytes(net.tcp_read(s, 4))}") + // <= 0 clears it: this read waits for the byte instead of timing out. + println("set_timeout 0: ${show_unit(net.tcp_set_timeout(s, 0))}") + net.tcp_write(c, bytes.from_string("z"))! + println("read after clear: ${show_bytes(net.tcp_read(s, 4))}") + // After the peer closes: nothing is available and a read is EOF. + println("close client: ${show_unit(net.tcp_close(c))}") + println("available after peer close: ${show_int(net.tcp_available(s))}") + println("read after peer close: ${show_bytes(net.tcp_read(s, 4))}") + println("close: ${show_unit(net.tcp_close(s))}") + println("close listener: ${show_unit(net.tcp_close_listener(l))}") + println("done") +} From 2d345882f4f0203a4b57545aaf7f452d9b3ef92e Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Tue, 13 Oct 2026 01:40:00 +0900 Subject: [PATCH 2/3] Add C-377, C-378 and C-379: net tcp loopback and handles, one error table, and guest-enforced timeouts and tcp_available on every leg Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/contracts/README.md | 5 ++- docs/contracts/conformance.md | 4 +- docs/contracts/contracts.toml | 32 ++++++++++++++ docs/specs/als/README.md | 2 +- docs/specs/als/runtime.md | 83 ++++++++++++++++++++++++++++++++++- proofs/als-validation.toml | 6 +-- 6 files changed, 123 insertions(+), 9 deletions(-) diff --git a/docs/contracts/README.md b/docs/contracts/README.md index c293635a..43e4a49c 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -31,7 +31,7 @@ Measured per contract in [`proofs/contract-provenance.toml`](../../proofs/contra the `since` release was tagged). Of 376 contracts: **requirements-first 71** (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/handler@0.3.0 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 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index f2415c7d..bcf7a506 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; 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)
`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/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, C-377, C-378, C-379 | `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)
`spec/embedded_cross/net_tcp_loopback.almd` (both-target test)
`spec/embedded_cross/net_tcp_errors.almd` (both-target test)
`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)
`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 1768d331..796b57e5 100644 --- a/docs/contracts/contracts.toml +++ b/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 `(:): `, with the host and port the program passed, and every other call reads `: `. 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 \"\"` and a resolver failure `name resolution failed for \"\"`. 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), `: 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 `(:): 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 ``), 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 `: 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" }, +] diff --git a/docs/specs/als/README.md b/docs/specs/als/README.md index 3d2306b7..e1396800 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, C-370, C-374, C-375 | +| [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, C-374, C-375, C-377, C-378, C-379 | | [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/docs/specs/als/runtime.md b/docs/specs/als/runtime.md index 0cf8fed4..69b1c345 100644 --- a/docs/specs/als/runtime.md +++ b/docs/specs/als/runtime.md @@ -1,6 +1,6 @@ # ALS — 実行時規範（Runtime） -> Last updated: 2026-10-05 +> Last updated: 2026-10-13 プログラム実行の観測規範（エラー終了・文字列補間の表示形・並行コンビネータ）。 参照方法は [strings.md](strings.md) 冒頭と同じ。 @@ -210,7 +210,86 @@ serve の形のプログラム（`main` の本体がちょうど 1 つの `http. 集合・フレーミングを外した本文を比べ、成果物に上限超えの本文と長すぎる要求行を送り、 最後に `/trap` を要求する） -Contracts: C-096, C-112, C-118, C-133, C-189, C-214, C-366, C-367, C-375。 +`net.tcp_*` 族（`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`）は、native、埋め込み wasm レーン（`almide run --target wasm`）、 +標準の WASI 0.3 コンポーネント（net 操作を含むプログラムの +`almide build --target wasm`。ネットワークを許可して走らせる）で同一バイトの観測を +返す（almide/almide#3620）。ハンドルは素の `Int` で、ストリームとリスナーの 2 つの +表から出る。どちらの表も 0 から番号を振り、新しいハンドルは空いている最小の枠を取る。 +閉じないハンドルは実行の終わりまで生きる。ループバックアドレスでは、1 つの逐次 +プログラムが listen・connect・accept・write・read を行える（`tcp_connect` は +`tcp_accept` の前に listen のバックログに対して完了する）。`tcp_write` はすべての +バイトを渡すか失敗する。`tcp_read(s, n)` は読めるバイトが現れると 1 以上 n 以下の +バイトを返し、n が 0 のときとストリームの終わりでは待たずに空のバイト列を返す +（何度尋ねても同じ）。`tcp_read_exact(s, n)` はちょうど n バイトを返す。閉じた +ハンドルへの `tcp_close` と `tcp_close_listener` は ok を返す。`tcp_is_open` は +プログラム自身の `tcp_close` の後と、発行していないハンドル（負を含む）で false を +返し、相手が閉じても true のままである。`net.tcp_local_port(listener)` は +リスナーが bind しているポートを `Result[Int, String]` で返す。ポート 0 に bind した +リスナーは OS が割り当てたポート（1..=65535）を返し、ポート 0 の 2 つのリスナーは +異なるポートを返す。IPv6 ソケットは native を含むすべてのレグで IPv6 専用 +（`IPV6_V6ONLY`）であり、`::` のリスナーは IPv4 のクライアントを受理しない。 +host 引数が名前ならホストが解決し、リゾルバの順にアドレスを試し、最初の成功を返す +（すべて失敗すれば最後のアドレスの失敗を返す）。 +失敗はすべて `err` で、その文字列は 1 つの表から出てすべてのレグで同一であり、OS の +errno も OS 自身の文言も含まない。`tcp_connect` と `tcp_listen` は +`(:): <分類の文言>`、他の呼び出しは `: <分類の文言>` と書く。 +転送の失敗は `wasi:sockets` の `error-code` の場合として 1 回だけ分類する（native と +埋め込みホストは OS のエラーを wasmtime と同じく対応づける）。分類の文言は +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`、メッセージを持たない未分類の失敗は +`network error` である。解決できない名前は `cannot resolve host ""`、 +リゾルバの失敗は `name resolution failed for ""` と読む。次の文言は転送の前に +Almide が決め、すべてのレグで同じである。発行していないハンドル（負を含む）には +`invalid TcpStream handle: N` と `invalid TcpListener handle: N`、閉じたハンドルには +`TcpStream handle N is closed` と `TcpListener handle N is closed`（`tcp_close` と +`tcp_close_listener` は除く）、`tcp_read`・`tcp_read_exact`・`tcp_read_timeout` の +負の長さには `: negative length N`（パニックしない）、0 以下の N には +`tcp_read_timeout: timeout must be positive (got N ms)`、N バイトのうち K バイトで +ストリームが終われば `tcp_read_exact: connection closed after K of N bytes`、 +`tcp_connect` と `tcp_listen` の範囲外のポートには +`(:): port out of range 0..=65535`。ネットワークを許可されない標準の +実行も読み込まれて走り、試みる bind と connect はそれぞれ access-denied として +失敗する（例: `tcp_connect(127.0.0.1:8080): permission denied`）。 +標準のコンポーネントでは、読み書きのタイムアウトと `tcp_available` をゲストが +実施する（WASI には受信タイムアウトも peek も読めるバイト数もない）。どのレグも同じ +答えを返す。`tcp_set_timeout(s, ms)` は s のその後の読み書きを 1 回ごとに ms +ミリ秒で区切り、ms が 0 以下なら区切りを外す。区切りは下位の読み書き 1 回ごとに +かかり、`tcp_read_exact` や `tcp_write` の全体にはかからない。区切りに達した呼び出しは +`: timed out` で失敗する。`tcp_read_timeout(s, n, ms)` は ms > 0 で区切った +1 回の読み取りで、ms 以内に読めたバイト（n 以下）を返すか +`tcp_read_timeout: timed out` で失敗し、その後の s は呼び出し前の +`tcp_set_timeout` の値で再び区切られる。`tcp_available(s)` は待たずに読めるバイト数を +消費せずに返す。上限は 65536 で、読めるバイトが無いときとストリームが終わったときは +0 である。標準のコンポーネントではこの数を、ゲストが待たずに満たす先読みバッファ +（ストリームごとに 64 KiB 以下、そのストリームの最初の `tcp_available` で確保）から +数え、どの読み取りもバッファのバイトを先に取るので、読み取りは native と同じバイトを +同じ順に返す。 +対象外: ポート番号そのもの。デュアルスタックのソケット（提供しない）。名前が解決される +アドレスとホスト間でのその順序（同じ機械ではどのレグも同じリゾルバに尋ねる）。 +メッセージ m を持つ未分類の失敗（p3 の `other(some(m))`）の文言は m で、native と +埋め込みレーンの間でだけ一致する。タイムアウトが発火する時刻（壁時計）と、タイマーと +同じ瞬間に届いたバイトが返るかタイムアウトするか（native にも同じ競合がある）。相手の +バイトが読めるようになる時刻（`tcp_available` はバイトが届いた後でレグ間で一致する）。 +標準のコンポーネントのネットワーク許可（標準のホストは許可の無いソケットアドレスを +すべて拒否する。許可は `wasmtime run -S inherit-network` で、host 引数が IP +リテラルでなく名前なら `-S allow-ip-name-lookup` も要る。ホストの設定であり、 +この規範には含まない）。 +テスト: `spec/embedded_cross/net_tcp_loopback.almd`・ +`spec/embedded_cross/net_tcp_errors.almd`・`spec/embedded_cross/net_tcp_timeouts.almd` +（127.0.0.1 のポート 0 で listen し、`tcp_local_port` でポートを読む 1 プログラム内の +ループバック。spec/embedded_cross の網が native と埋め込みレーンで走らせ、実装側の +ドライバが `-S inherit-network` の標準のコンポーネントとしても走らせる。同じドライバが +許可の無い標準のコンポーネントで `permission denied` の文言を確かめる） + +Contracts: C-096, C-112, C-118, C-133, C-189, C-214, C-366, C-367, C-375, C-377, C-378, C-379。 ## ALS-R6 ファイルシステムのパス解決 diff --git a/proofs/als-validation.toml b/proofs/als-validation.toml index 73ac4ff3..4ca32bfd 100644 --- a/proofs/als-validation.toml +++ b/proofs/als-validation.toml @@ -693,9 +693,9 @@ verdict = "accurate" [[section]] id = "ALS-R5" -hash = "sha256:0ae9dc01126a" -reviewed = "2026-10-06" -by = "O6lvl4 (via the Claude session, on the owner's instruction of 2026-10-06 to run the A-wasm goal unattended; the stock-artifact clause of C-367 rescoped now that a serve-shaped program builds as the C-375 wasi:http/handler@0.3.0 export and only other programs reaching http.serve are refused with E081 (almide/almide#2659); checked against the C-367 and C-375 statements and the almide/almide stock-serve-2659b branch: wasmtime serve answers the http_serve_export.almd request script as native does, and a non-serve-shaped main reaching http.serve is E081 at check and build time)" +hash = "sha256:b4f569fbf4e9" +reviewed = "2026-10-13" +by = "O6lvl4 (via the Claude session, on the owner's rulings of 2026-10-12 for net/tcp on wasm (almide/almide#3620, items 1-7); the net.tcp_* paragraph added for C-377, C-378 and C-379: handle numbering, loopback, end of stream, close, is_open and tcp_local_port; the one error table and the Almide-local texts; guest-enforced timeouts with the tcp_set_timeout restore and the tcp_available lookahead; checked against the three statements and the owner-approved design (net-tcp-design.md, sections 0-7). Requirements-first: no almide build implements tcp_local_port or the new texts yet; the three spec/embedded_cross fixtures were checked against v0.67.1 with tcp_local_port shimmed to a fixed port, which prints the current transcript except at the points this paragraph changes (errno text, the negative-length panic, the wiped timeout))" independent = "no" verdict = "accurate" From e9adb101067705dfefe13c4baf778149210c568a Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Tue, 13 Oct 2026 01:43:40 +0900 Subject: [PATCH 3/3] Record the provenance rows of C-377, C-378 and C-379, keeping the existing rows and short hashes Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/contracts/README.md | 2 +- proofs/contract-provenance.toml | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 43e4a49c..efe49e8f 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -28,7 +28,7 @@ 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. 379 contracts diff --git a/proofs/contract-provenance.toml b/proofs/contract-provenance.toml index 7cb6f605..48535eb5 100644 --- a/proofs/contract-provenance.toml +++ b/proofs/contract-provenance.toml @@ -2828,3 +2828,24 @@ since = "0.67.0" entry = "2026-10-05T22:33:29+09:00" entry_commit = "340b859c" class = "requirements-first" + +[[contract]] +id = "C-377" +since = "0.68.0" +entry = "2026-10-13T01:40:00+09:00" +entry_commit = "2d345882" +class = "requirements-first" + +[[contract]] +id = "C-378" +since = "0.68.0" +entry = "2026-10-13T01:40:00+09:00" +entry_commit = "2d345882" +class = "requirements-first" + +[[contract]] +id = "C-379" +since = "0.68.0" +entry = "2026-10-13T01:40:00+09:00" +entry_commit = "2d345882" +class = "requirements-first"