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

[O6lvl4]

Step 0 of the net/tcp-on-wasm plan (almide/almide#3620): the contracts land in the judge before any implementation, per the owner's rulings of 2026-10-12. All three are requirements-first: since = "0.68.0", status = "active" (the C-375 precedent; the provenance gate classes them requirements-first).

What each contract promises

• C-377 — the net.tcp_* family (13 fns, incl. the new net.tcp_local_port(listener) -> Result[Int, String], ruling 5) answers byte-identically on native, the embedded lane (almide run --target wasm) and the stock WASI 0.3 component. Handles: two tables (streams, listeners), each from 0, lowest free slot; unclosed handles live to the end of the run. Loopback in one sequential program; tcp_read answers 1..=n bytes, empty without waiting for n = 0 and at EOF (every time); tcp_read_exact exactly n; closing twice is ok on both tables; tcp_is_open false after own close and for never-issued handles, true after a peer close; a port-0 listener reports its OS-assigned port. IPv6 sockets are V6ONLY on every leg (ruling 6). Name resolution: addresses tried in resolver order, first success, else last failure.
• C-378 — every failure is errno-free text from one table, identical on every leg: <fn>(<host>:<port>): <class text> for connect/listen, <fn>: <class text> otherwise; the 13 wasi:sockets class texts plus network error, the two DNS texts; the Almide-local texts (handle texts kept from native, <fn>: negative length N, tcp_read_timeout: timeout must be positive (got N ms), tcp_read_exact: connection closed after K of N bytes, <fn>(<host>:<port>): port out of range 0..=65535). A stock run without the network grant loads, and bind/connect fail as permission denied (ruling 7).
• C-379 — timeouts and tcp_available are guest-enforced on p3 and answer what native and embedded answer. tcp_set_timeout bounds each underlying read/write; tcp_read_timeout restores the earlier tcp_set_timeout value (ruling 3); tcp_available counts bytes readable now without consuming, at most 65536, 0 when none/EOF, served on p3 by a lazily allocated ≤64 KiB lookahead buffer that reads drain first (ruling 4).

NOT covered (in the statements, C-367 style)

• C-377: the port numbers; dual-stack sockets (not offered); which addresses a name resolves to and their order across hosts; the stock grant (wasmtime run -S inherit-network [-S allow-ip-name-lookup]) as host configuration.
• C-378: other(some(m)) texts, equal only between native and embedded; which names resolve; the stock grant.
• C-379: the instant a timeout fires and the same-instant byte/timer race; when a peer's bytes become readable; the stock grant.

ALS-R5 gains the matching paragraph (Japanese, with its テスト line), and its validation row is re-stamped.

Evidence

Three in-program loopback fixtures (127.0.0.1, port 0 + tcp_local_port, no fixed ports, payloads well under 8 KiB, the OS port masked or printed as predicates):

• spec/embedded_cross/net_tcp_loopback.almd → C-377
• spec/embedded_cross/net_tcp_errors.almd → C-378
• spec/embedded_cross/net_tcp_timeouts.almd → C-379

Why spec/embedded_cross, not spec/wasm_cross: both the als cross leg and almide's wasm_cross_target_spec build the stock artifact and run wasmtime --dir=/ -S inherit-env=y with no network grant. Today the stock build of a net program is E081 (almide's harness panics on a failed wasm build), and after the p3 routing lands every bind/connect on that leg reads permission denied, so a wasm_cross fixture would be a permanent, untrue divergence (an @xt-allow that can never go stale) plus three new ref abstains above the ceiling. spec/embedded_cross is the established home for native ⇄ embedded host-op fixtures (C-328, C-374); the stock leg with -S inherit-network and the no-grant permission denied case are the implementation's three-leg driver, which the statements name but do not cite as evidence until that unit exists (CLAUDE.md: no citation without the implementation-side unit).

Measured on v0.67.1 (tcp_local_port shimmed to a fixed port, since it does not exist yet): all three fixtures type-check except E002 undefined function 'net.tcp_local_port', run deterministically (three identical runs), and print the transcript these contracts pin except exactly where the contracts change native: errno texts (Address already in use (os error 48), Connection refused (os error 61), Resource temporarily unavailable (os error 35), invalid port value, failed to fill whole buffer, cannot set a 0 duration timeout), the negative-length panic (capacity overflow, exit 101), and the wiped timeout (the read after tcp_read_timeout blocks forever). almide fmt --check is clean on all three.

Reference evaluator: als-ref run abstains on all three (stdlib:net.tcp_read for the errors fixture, stdlib:net.tcp_listen for the other two). spec/embedded_cross is outside the ref corpora, so the abstain ledger is unchanged (ceiling 18, 18 abstained).

Gates passed locally

check-contracts.sh, check-contract-provenance.py, check-als-element-coverage.sh, check-als-style.sh, check-als-validation.sh, check-links.sh, check-gate-verification.sh, check-ratchet-separation.sh --staged and --range origin/main..HEAD, selftest-conformance.py, check-runner-coverage.py, check-ref-totality.py and check-ref-kernel.py (ref built with cargo build --release), check-workflows.sh; README / conformance / ALS README regenerated. No ratchet moved.

After this merges: advance proofs/als-pin.txt in almide/almide in its own commit, then the implementation PRs (design §7 steps 1–4) copy the fixtures.

🤖 Generated with Claude Code