diff --git a/docs/contracts/README.md b/docs/contracts/README.md
index c293635a..efe49e8f 100644
--- a/docs/contracts/README.md
+++ b/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/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"
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"
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")
+}