Repository navigation
T14 — Give each box its own loopback address and answer its name from finalize to destroy - #1765
Merged
norrietaylor merged 38 commits intoOct 1, 2026
Conversation
NET-010 needs every published box to hold a host loopback address of its own, leased from the reserved local range and never shared with a live neighbour. This adds the pure half of that decision: - `core::loopback` carves `127.64.0.0/24` at a /27 into 8 disjoint slices, one per gvproxy daemon, and leases addresses within a slice from a `u32` bitmask: branch-free `lease`/`release`, no sockets, no clock, no randomness, so the decision stays separable from the publish call (NET-010 is T2). - The carve restates `switch::DEFAULT_ADDRESS_PLAN` address for address, pinned to it by the unit tests; `minimald` cross-checks the two in the next commit. - `kani_loopback_alloc_injective` proves the property: two symbolic slices prove the carve's disjoint half, eight live boxes published, a symbolic subset withdrawn and re-published prove the leased half, with same-slice daemons sharing the one owned set. - `scripts/kani.sh` expects one more sessions harness (8 -> 9). The Kani lane does not run on this box; the harness is written and its bound reasoning documented, and the count gate is bumped to match.
A box with the own-address mode now leases a host loopback address of its own out of this daemon's slice of the reserved local range at finalize, publishes its declared ingress there, and answers its name at that address from finalize to destroy whether or not a client is attached. - sessions: build one LoopbackAllocator over the daemon's own gvproxy slice beside the hostname registry; a VM daemon derives its slice octet from its instance id (mirroring the start line's derivation), a native one from its own /24, and a VM node leases one address for its shared-address boxes before any box leases - dns: the registry holds the publish (address + declared ports) keyed by the stable session id, reports shared-address port collisions instead of translating them, and answers NODATA for a box whose host has exited while its name still lives at the node's shared address - session: finalize leases, publishes and registers; destroy unpublishes, releases and deregisters so the name answers NXDOMAIN - session_host: the host marks its box's name running at start and stopped at exit - policy/gvproxy_network: the request a box's ingress is applied with binds the box's own published address, not the host loopback, and the attach passes the published address through
…0s ran out the coder's uncommitted work as it stood when its 7200s ran out The coder was stopped at the end of its time with these changes not committed. The runtime committed its working tree as it stood so the work is kept: this commit is a snapshot, not a finished step, and may not build or pass its tests.
…box-its-own-loopback-address-and-answe
Contributor
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
The work the previous round committed as it stood did not compile: the release path named `Ipv4Addr` without its path, the `zone_answer_for` test helper awaited inside a synchronous function, and one call passed `&record` where the record is already a reference. The new `apply_ingress` signature also left the netns root integration test calling it with the old three arguments; it now publishes on the node's shared loopback address, which is the shared-address lane that proof's own host connect has always exercised. These are compile and lint repairs only; no behaviour changes.
T67 moved the reserved local range the switch crate's default address plan carves from 127.64.0.0/24 to the design's 127.0.64.0/24. This branch's allocator restates that plan address for address and is pinned to it by minimald's carve cross-check, but it was cut before the move and still carried the old block — so the carve assertion failed on every test that published a box, and the daemon's own test literals and the session tests' octet arithmetic named the abandoned block too. Every one follows the move: the allocator's constant, the dns and policy test literals that stand in for a leased address or a node's allocated one, and the session tests, which now read the range from the one definition through a prefix mask instead of restating its octets.
The lease and release events name the box through tracing's `session_name` field, which the fmt layer records the way it records every string field there — Debug, so quoted: `session_name="web"`, the same spelling the R3.5 registration line beside them carries. The two assertions looked for the unquoted form and so never found the line.
The registry's own_route reads the box's lease from the own-address map by session id, so a report of a freshly attached lease has to record it before deriving the route from it. The report did it the other way round, so the first report always missed its own lease and installed a route at the published address instead: on a VM host the box's name then answered the host at the node's shared loopback address rather than answering NODATA while it held nothing the host could reach — the leak NET-127's answerer test exists to catch. Recording first puts the report back where the doc comment says it is: the moment a VM host's route turns from the published address onto the lease the attach just reported.
The double-release assertion re-leased the address it was about to release, so it asserted against a lease that was live again — the one case where a release is legitimate. Release twice first, then show the freed address is the next one handed out, so the property the message names is the one the code proves.
Member
|
/revise T14 toward answerer-granted leases |
…box-its-own-loopback-address-and-answe
Contributor
Author
|
Round 1 of 10 on a failed check suite, pushed as
Verify Outside the task's
Converted to a draft: something above needs a person before review. At this branch two own-address boxes that declare the same port each lease their own host loopback address out of the daemon's slice of 127.0.64.0/24, answer by name at those two different addresses, and publish their ports there un-translated (each_box_gets_own_loopback_address); two daemons' slices are pinned disjoint against the switch plan's carve, so boxes behind two gvproxies on one host never share an address (loopback_slice_carve_matches_the_switch_plan, loopback_allocators_follow_the_daemon_s_slice_octet, and the deferred Kani proof); a box's name is registered at FinalizeSession, answers with no client ever attached, and holds until destroy, where every later lookup answers NXDOMAIN and the address returns to the slice (name_registered_at_finalize, name_answers_without_attached_client, destroyed_box_name_is_nxdomain); and a box that shares its node's address answers NODATA while stopped with the collision reported rather than translated (stopped_shared_address_box_is_nodata, host_ip_box_answers_node_loopback_address, shared_address_port_collision_reported_not_translated). Notes from the agent: This round repaired the previous round's commits, which did not compile, so all four failed checks were build failures first. (1) Build/lints: a missing Ipv4Addr path on the release path, an await inside a synchronous test helper, one needless borrow, and the netns root-integration call site still on apply_ingress's old three-argument signature. (2) The allocator restated the switch plan's carve but still carried the pre-T67 block 127.64.0.0/24 while the plan had moved to the design's 127.0.64.0/24 — the carve cross-check failed on every test that published a box, and nine dns/policy test literals plus the session tests' octet arithmetic named the abandoned block; the session tests now read the range from the one definition through a prefix mask instead of restating its octets. (3) The lease/release assertions looked for an unquoted |
Member
|
/revise two things, the first is a design conformance failure against gominimal/arch 1. Allocation must be arbitrated by the answerer, not tiled per daemon.
2. Native lane regression on 47f5f06. |
…owned set NET-010 allocation was tiled per daemon: every gvproxy carved its own /27 of the reserved local range out of a 'slice octet', with the wrap-around collision that scheme documents (octet % 8). The answerer round rejects the carve itself: allocation in 127.0.64.0/24 is host-global, arbitrated through the answerer's authenticated channel, and co-resident nodes MUST NOT self-assign (design section 7.1). Replace the slice model with one owned set over the answerer's whole leasable pool: 127.0.64.2 through 127.0.64.254, with 127.0.64.1 held back as the answerer's own address (its Linux listener) and the range's network and broadcast addresses never granted. The allocator is still pure -- a fixed-width bitmask, one bit per grantable address, lease and release still branch-free arithmetic -- so the Kani harness keeps its shape. restore(owned) rebuilds the set from the answerer's record, which is how a restarted daemon re-derives its live grants; a foreign address in the record narrows the pool rather than widening it. The Kani harness keeps its name and its eight-box schedule but drops the symbolic per-box daemon: a lease is now a function of the host's owned set alone, since no daemon contributes state the allocator reads. It gains a restore phase in the middle, so the record's half of the property -- live boxes keep their addresses across a restart -- is in the proof. The minimald wrapper that built its allocator from a slice octet is gone in the next commit.
…record NET-010's allocation was tiled per daemon: the manager built its allocator from a slice octet, so two gvproxies on one host could only stay apart by the octet arithmetic, and the carve's wrap-around — about one derived pair in eight — handed two daemons one address between them. The answerer round replaces that arbitration: allocation in 127.0.64.0/24 is host-global, through the answerer's authenticated channel, and co-resident nodes must not self-assign (design section 7.1). The channel is the lease book (net::dns::LoopbackLeaseBook): one durable record per host under the shared state root, every read-modify-write serialized by its own flock, written staged-then-renamed like every other record there. Grants are keyed by namespace — a box by its stable session id, the node once — so the record survives a daemon restart and a resumed session's re-registration is answered with the address it already held. A record that cannot be read or written withholds grants rather than guessing an address another namespace may hold: the one failure NET-010 cannot tolerate. The pool is the answerer's whole grantable range, 127.0.64.2 through 127.0.64.254; 127.0.64.1 is held back as the answerer's own and never granted. Daemon start now owes the range probe too (NET-123): Manager::init runs the real bind probe once — never the process-global stand-in the CreateSession tests install — and its verdict gates every grant, so an absent range publishes on the 127.0.0.1 interim instead of granting an unbindable address. Before the first grant the daemon sweeps the record against the session store's live ids, freeing the grants of boxes that were destroyed while no daemon was running. The slice octet keeps only its switch-side meaning: it places a native daemon's gvproxy /24 inside the host /16, and the start line logs that switch beside the one host-wide pool. server.rs's carve tests go with it, replaced by a start-line test that two daemons on pinned octets — and a microVM daemon on the host's /16 — all name the same pool; the disjointness they used to prove is now the book's, proven by the dns.rs tests over two books on one state root.
…0s ran out the coder's uncommitted work as it stood when its 7200s ran out The coder was stopped at the end of its time with these changes not committed. The runtime committed its working tree as it stood so the work is kept: this commit is a snapshot, not a finished step, and may not build or pass its tests.
Contributor
Author
|
Round 2 of 10 on a /revise note, pushed as The coder ran out of its 7200s before it finished. If it left work uncommitted, its last commit is the runtime's snapshot of that work as it stood — the commit message says so — and not a finished step: it may not build or pass its tests.
Verify Outside the task's
Converted to a draft: something above needs a person before review. Two boxes listening on the same port answer at two different loopback addresses by name, boxes behind two gvproxies on one host never share an address, a name works from finalize until destroy whether or not a client is attached, and a destroyed box's name answers NXDOMAIN. Commit headers reworded by the runtime to fit commitlint. The header the coder wrote is the first paragraph of each of these commits' bodies:
|
norrietaylor
requested changes
Sep 30, 2026
Member
There was a problem hiding this comment.
Review of round 2 (8a6797d) against the T14 plan block, my earlier /revise, and the design check with gominimal/arch deployment-and-egress-gateway.md §7.1.
What round 2 got right: the per-daemon slice is gone, allocation is one host-wide set over 127.0.64.2–254 with restore-from-record, the native e2e ingress proof follows the box's own address, and all seven plan test lines exist and assert real claims. The linux native lane is green with the address-following proof.
What blocks:
- Grant released on daemon Stop, not only on Destroy (thread on session.rs). Design §7.1 line 254: the address is per published namespace, session-stable, assigned at session start; the box outlives the daemon, so a grant is released on destroy, never on daemon shutdown, and across a restart the daemon restores from the record with the address unchanged.
- Allocation model (thread on dns.rs): a flock-serialised file under one state root is not the design's arbiter (§7.1 lines 250 and 257: the host-side answerer over its authenticated channel, co-resident nodes MUST NOT self-assign). It cannot cover the LocalVM style at all, since the guest daemon cannot hold a host flock. It is acceptable as a bounded interim for native nodes on one state root only if the PR states and guards what the thread lists.
- The start sweep's liveness race (thread on sessions.rs) breaks line 254's guarantee for a live peer's box.
The macOS lane on this head failed before the session proof in an unrelated minvmd volume test; I re-ran it. The remaining threads are MEDIUM and LOW.
The macOS e2e lane failed because an own-address box's activate publishes its declared ports at its granted reserved-range address through the host gvproxy, and on a stock macOS host -- whose lo0 carries none of 127.0.64.0/24 -- that forwarder bind is refused, so apply_ingress failed the whole attach. The daemon-start bind probe measured the guest's own loopback, which always carries the whole 127/8, so it read the range present on every VM host and vouched for addresses the host cannot bind. NET-123's probe now measures the loopback the publishes bind on. A daemon on the gvproxy switch is inside a microVM and cannot see that host, so the walk is conducted through the forwarder itself, over the same shuttle the publishes ride: one expose per address of the range, released by its unexpose as each answers, classified exactly as the local probe classifies its own binds. A refusal, an unreachable control channel or a stalled walk reads the range absent, which withholds the grants and publishes own-address boxes on the node's shared address -- the interim, the shape that keeps activate working on a host without the aliases. A native daemon still probes its own loopback: it spawns the forwarder, so its own host is the publish surface. The create response's interim flag still carries the guest's own verdict -- the module doc's documented position until the publish-surface verdict is plumbed into it (rpc.rs, outside this task's layers).
The strict clippy gate holds the lines this branch changed to clippy::indexing_slicing; the budget-overrun arm of the forwarder range probe was its one hit on a line this round added. The stuck address is read with get() and a never-empty expectation instead, which names the invariant the index silently leaned on: the reserved range's usable-host list is never empty.
Contributor
Author
|
Round 3 of 10 on a failed check suite, pushed as
Verify Outside the task's
Converted to a draft: something above needs a person before review. On this branch the task's own proof holds and is pinned by its seven tests: two boxes listening on one port answer at two different loopback addresses by name, a name answers from finalize until destroy whether or not a client is attached, a destroyed box's name answers NXDOMAIN, a stopped shared-address box answers NODATA, a host-address box answers its node's address, and a shared-address port collision is reported, never translated. This round makes that feature survivable on a microVM host: the daemon-start range probe now measures the loopback the publishes actually bind on (the forwarder's, over the control shuttle, on a HostShuttle daemon; its own host on a native one), so a VM host whose lo0 carries none of 127.0.64.0/24 reads the range absent and its own-address boxes publish on the node's shared address — the interim — instead of failing their activate, which is what was turning the macOS e2e lane red. Notes from the agent: Diagnosis (derived, not observed): the two failed checks are the one macOS lane and its aggregator. On it, the branch's own-address publish has the HOST gvproxy bind the box's granted 127.0.64.x address; a stock macOS lo0 carries no range alias, so gvproxy's expose fails and apply_ingress fails the whole own-ip attach — and the two VM-lane e2e proofs that activate own-address boxes with --ingress (min_internal_names_through_proxy, proxy parity) die there. The KVM lane runs the same VM harness green (Linux binds all of 127/8) and the Linux-native lane is green, which is why only the macOS pair is red. I could not read the CI log or run the lane from this box (no macOS, no libkrun/KVM, no network credential), so the fix is verified by unit tests and the mechanism; the macOS lane itself must re-run in CI to confirm. Fix: NET-123's probe now measures the publish surface — sessions.rs picks the probe by transport, and policy.rs conducts the whole-range walk through the forwarder (one expose per reserved address at a fixed obscur…[truncated] |
Contributor
Author
|
Round 4 of 10 on a failed check suite: the coder changed nothing. Round 4's directive names the two failed checks from GitHub run 36699032946 (ci-macos-success, e2e). That run built the pre-fix head 8a6797d (committed 08:41; the fix landed 09:45-09:50 and the directive was cut 10:08 with the latest completed checks — a macOS lane cannot start at 09:50 and finish by 10:08), so this round verified the fix already at the head rather than adding to it; no file changed. Failure traced from code, this box having no CI credentials to read the logs: at 8a6797d a guest daemon probed its own guest loopback — where all of 127/8 binds — granted itself a 127.64.x node address, and published an own-address box's declared --ingress at that address through the host gvproxy; a stock macOS lo0 refuses the bind (EADDRNOTAVAIL, gvproxy answering 500 per expose), so 'min session activate --network own_ip --ingress ...' failed in proof_min_internal_names_through_proxy's own-address half and proof_proxy_refuses_like_direct's PAR_OWN half — the e2e job, and wi…[truncated] |
…box-its-own-loopback-address-and-answe # Conflicts: # scripts/session-e2e.sh
Contributor
Author
|
Round 5 of 10 on a conflict with the base branch, pushed as Resolved conflicts in:
Verify Outside the task's
Converted to a draft: something above needs a person before review. At this branch head, with main merged in, two boxes listening on the same port answer at two different loopback addresses by name, boxes behind two gvproxies on one host never share an address, a box's name answers from finalize until destroy whether or not a client is attached, and a destroyed box's name answers NXDOMAIN — all seven proof tests pass on the merged tree. Notes from the agent: Round 5 was a conflict round only; no review threads were listed. Resolved the one conflicted path, scripts/session-e2e.sh, by keeping both sides verbatim: our published_loopback_host() helper (the daemon-log reader the fresh-install and posture proofs call at three sites) and main's new proof_own_ip_egress_declared_and_enforced() (NET T20, called from main's driver), each verified byte-identical against its parent; both call sites survive in the merged file, bash -n passes, and the repo's shellcheck harness (scripts/lint-shell.sh, a CI gate) passes all 47 scripts. Completing the merge also carries main's auto-merged crates/minvmd/src/cmd/run.rs and crates/minvmd/src/image.rs (T57 fresh-Linux KVM activation) onto the branch — the runner started that merge, I only finished it. All seven minimald test lines were run as written on the merged tree and pass (first run compiled the crate, 8m14s). Deferred: 'cargo nextest run -p sessions kani_loopback_alloc_injective' (lane kani, no such lane on this box) — the harness is present as kani_loopback_alloc_injective under #[cfg(kani)] in crates/sessions/src/core/loopback.rs, and scripts/kani.sh's 'expect sessions 9' matches the 9 #[kani::proof] functions now in the crate; nothing was run for it. scripts/session-e2e.sh itself cannot run here (needs a KVM/VM lane); its resolution is syntax- and shellcheck-verified only. |
norrietaylor
requested changes
Sep 30, 2026
Member
There was a problem hiding this comment.
REQUEST_CHANGES (re-post of review 5364028288, which round 3 did not read: its status comment judged no threads, and round 4 was dispatched in the same failed-check mode that carries no threads).
Round 3 (f1d2996, 633bc7b) changed net/policy.rs (new probe_publish_surface) and the probe arm in sessions.rs only. That addresses one of my seven threads (sessions.rs:293, the VM-backed daemon acting on the guest's bind probe): the HostShuttle arm now walks the range through gvproxy expose/unexpose (sessions.rs:304-316, policy.rs:241-320). Two caveats carried forward, not blocking: the walk runs under the net_switch lock at daemon start with a 20 s budget (policy.rs:590), and only TimedOut breaks it; and the macOS session proof still has not run on this PR because the lane dies earlier (below).
The other six threads are unchanged at the head and are re-posted below with the same severities. The BLOCKING design threads stand on ARCH-EXPERT's ruling: release-on-Stop violates §7.1 l254 (an address per published namespace, session-stable), and the daemon-local lease book is a bounded native interim only under the four conditions in the original thread (answerer-arbitrated allocation per l257, cross-node collision reporting per l250, no LocalVM scope, and the interim recorded in the PR body).
Correction to my earlier attribution of the macOS red. I said on the Stop thread that the release path is what the failing quiesce test exercises. It is not: volume_quiesce_integration.rs creates no session, so no Stop runs. The actual holder is the lease book's lock file, opened .write(true) on the state volume and held for the daemon's lifetime; see the new thread at dns.rs:1220 with the green/red bracket. The Stop-release thread stays BLOCKING on design grounds, not as the cause of this failure.
Rounds 4 and 5 pushed no change to any of these threads (round 4 pushed nothing; round 5 was the base merge), so the seven threads below stand on head 0d95812 at the same lines.
Round 6 of the loopback PR review, the lease-record findings: - The lock file's handle is now created once and reopened read-only, so the one fd the book holds open across its lifetime is not the write-open descriptor on the state volume that defeats the quiesce contract (flock needs no write access). The manager's shutdown arm closes it beside the cache's read-tracker release, and the book's unit tests now assert the fd's presence, its read-only access mode, and its absence after the close. - Grants are stamped with the wall clock they were made at, and the daemon-start sweep frees only lines stamped before this daemon began starting: a grant another daemon makes while this one is starting is never read as dead by the stale liveness snapshot that predates it. A pre-stamp record reads as stamped at the epoch, which the sweep decides on liveness alone - the behaviour before the guard. - The daemon-start collision report the review asked for: every reserved-range address a live publish holds on this host that this record does not name is reported at session start, like a port collision. The kernel's socket table is the one list of what is published that is global to the whole host, so a second state root whose own record re-granted an address cannot dodge the check the way it dodges the first root's file. - The module docs state the interim's bound plainly: file arbitration covers the daemons sharing one state root, the design's LocalVM condition is unmet (a second root keeps a second record), and the host-side answerer is what closes it. The PoolSpent doc no longer claims the box publishes nothing - it publishes on the node's shared 127.0.0.1 interim.
NET-129: when an OwnIp box finalizes on the node's shared address (spent pool, absent range, pending verdict, or unreadable record), the session actor now runs the same-address collision check that own-address boxes get. The collision warn and SharedPortCollision report fire without recording the node address as the box's own, so future lease asks and node-address repoints keep working. The registry gains a separate shared_published map for interim ports so that two shared-address boxes can see each other's declared ports, and so that listings can surface the collision. The map is cleaned up on deregister/destroy. A session-path test exercises two boxes finalizing while the range verdict is held pending.
…box-its-own-loopback-address-and-answe
Contributor
Author
|
Round 1 of 10 on a /revise note, pushed as
Verify Outside the task's
Converted to a draft: something above needs a person before review. Review threads the coder judged:
When an OwnIp box finalizes on the node's shared address — because the reserved local range is spent, absent, pending verdict, or the lease record is unreadable — the session path now emits the same Notes from the agent: Reverted the earlier out-of-scope rpc.rs visibility changes (the test no longer needs the rpc probe mutex). The shared-address collision check is implemented without touching the lease book, the range walk, or the socket-table report. The registry's new |
The shared-publish branch of the collision check matched any box that shared a port, so a granted own address was reported colliding with interim boxes on the node's shared address; it now applies only when the asking box publishes on the node address. A box that later publishes its own address drops its shared-address entry, and the node_address accessor sits below set_node_address so each keeps its own doc.
norrietaylor
marked this pull request as ready for review
October 1, 2026 09:34
norrietaylor
approved these
8
changes
10BC8
Oct 1, 2026
Member
There was a problem hiding this comment.
Approved at 99cc72a: round 11 stays inside NET-129 (shared-address collision warn and report for interim boxes, node address never recorded as the box's own; +234/−19 in dns.rs, session.rs, session/tests.rs), and the two LOW threads plus a doc-attachment slip and a stale comment are hand-fixed on top. Remaining gate is commitlint on the coder's commit body, a message rewrite.
…box-its-own-loopback-address-and-answe
norrietaylor
approved these changes
Oct 1, 2026
Contributor
Author
|
Round 2 of 10 on a failed check suite: the coder changed nothing. every commit this round put on the branch above |
norrietaylor
force-pushed
the
agent/1645-give-each-box-its-own-loopback-address-and-answe
branch
from
October 1, 2026 22:31
dcd0e6c to
c5287ab
Compare
norrietaylor
approved these changes
Oct 1, 2026
Member
There was a problem hiding this comment.
Head c5287ab is the commitlint re-wrap of the reviewed tree (trees identical, merge-base unchanged). Every lane is green on this head and minimal-review approved it with no findings; the loopback allocation, the finalize-to-destroy name answer, and the T14 test lines all landed in the earlier rounds.
norrietaylor
deleted the
agent/1645-give-each-box-its-own-loopback-address-and-answe
branch
October 1, 2026 23:13
norrietaylor
added a commit
that referenced
this pull request
Oct 2, 2026
…ost at merge T66 (#1789) added box_addresses to SessionConfig and SandboxLauncher; #1768 and #1765 each added an initializer without it on a base that predated the field, and their green lanes never re-ran against the merged main. The minimald test targets no longer compile on main; this fills the field the way every other initializer does. The merge queue this PR enables is what catches that class of stale green before it lands.
norrietaylor
added a commit
that referenced
this pull request
Oct 2, 2026
* ci: trigger the required lanes on merge_group A merge queue on main needs the five required aggregators to report on every queue commit. Each lane already gates its jobs on `github.event_name != 'pull_request' || <changes output>` and runs the dorny filter only on pull_request, so a queue commit runs the full set, which is what docs/ci-strategy.md section 5 prescribes for the queue. No job logic changes. * fix(minimald): fill box_addresses in the two test initializers main lost at merge T66 (#1789) added box_addresses to SessionConfig and SandboxLauncher; #1768 and #1765 each added an initializer without it on a base that predated the field, and their green lanes never re-ran against the merged main. The minimald test targets no longer compile on main; this fills the field the way every other initializer does. The merge queue this PR enables is what catches that class of stale green before it lands. * ci: pin the merge_group trigger to main and release branches The sibling push and pull_request triggers in all five lanes pin branches to main and release/**; the merge_group trigger now matches them, so a queue opened on any other branch does not run the lanes.
minimal-foundry Bot
added a commit
that referenced
this pull request
Oct 2, 2026
T14's (#1765) merged session tests construct `SessionConfig` and `SandboxLauncher` without the `box_addresses` field their declarations require, so minimald's test targets fail on E0063 and every lane that builds them — tests, minimald-root-integration, clippy — goes red with them. Both mean a session the activating client did not register, which self-allocates as it always has, so the value is `None`.
yermakoffivan
pushed a commit
to yermakoffivan/minimal
that referenced
this pull request
Oct 2, 2026
…ts ports (gominimal#1788) * feat(sessions): pure publish-verb decision for the host-side gate The frame half of NET-081's gate decides what a box may send out; this adds the other half, the decision over what its daemon may ask the switch to publish. applied() is pure over an owned request summary (verb, switch address, up to four records as ports or name indices), the host-side table NET-138 fills, and the unregistered-source phase: a publish is applied only where a row holds the address and admits every record; a retraction is decided table-wide, by what the rows hold rather than where the guest sits; an address no row holds is the phase's to decide, mirroring the frame verdict's lease-block interim. The Kani harness pins the decision as an iff over a fully symbolic request and row, in the frame verdict harness's shape. * feat(minvmd): the coder's uncommitted work as it stood when its 7200s ran out the coder's uncommitted work as it stood when its 7200s ran out The coder was stopped at the end of its time with these changes not committed. The runtime committed its working tree as it stood so the work is kept: this commit is a snapshot, not a finished step, and may not build or pass its tests. * fix(minvmd): drain box-table withdrawals from the registry itself The drainer took the report channel's receiver from a clone, whose withdrawal_reports_rx is always None by the Clone contract — so no drainer thread ever spawned and no row was ever withdrawn; a box's row outlived its shuttle connection past the box-end bound (NET-133). Take the receiver from the registry that created the channel. * fix(minvmd): quiet node-port helpers on libkrun-less hosts The node-port assignment helpers compile everywhere but are only called from run_foreground, which is libkrun-gated — so every libkrun-less build of the lib warned them dead. Allow them under not(minvmd_libkrun), the pattern DetachPoll and vm.rs's helpers already carry; the tests still cover them on every target. * docs(sessions): document the publish decision's refusal cases clippy asks a # Errors section of a fn returning Result; applied's refusals (UnknownAddress, Undeclared, Unheld) get theirs. * feat(minimald): bind the ports the boot line hands the guest daemon minvmd assigns the node's hostname-proxy (TCP) and zone-answerer (UDP) ports before the VM boots and hands them on the kernel command line; pid-1 reads the tokens off the environment the kernel passes through and binds them as handed: pinned, never re-picked, never relocated. The host's box table already names exactly these ports, so a daemon-chosen replacement would publish a listener the host gate refuses to carry. A boot without tokens — an older minvmd, a native run — keeps the pre-handoff default-then-select behaviour. * test(sessions): split the publish decision table into section helpers The exhaustive decision test was 177 lines, over clippy's too-many-lines ceiling, and summed its width range the pedantic lints reject. The sections become named helpers the survey-named test still drives in the same order; no case changes. * style(minimald): rustfmt the handed-port test * fix(minvmd): race the control relay's legs and pin its tests to the gate Three control-relay tests failed against the gate they shipped with: - the pipelined-request and connect-path-body tests read the relayed bytes through gate_over_control, which already consumes and asserts the whole admitted request — the body re-read found the head's bytes under it, and the pipelined test asserted the smuggled request was forwarded. Both now write by hand and read exactly the bytes the gate owes the switch. - a switch hanging up on an idle control connection ended only the response leg; the relay_control implementation never raced its legs, so the per-connection close a keep-alive control channel makes went unseen until the guest spoke again or the drain bound passed. Race the response leg against the request-leg probe like the frame relay does, and say which leg ended. * test(minvmd): hold the node-port probe on the wildcard it probes The test held its busy port on 127.0.0.1 while assign_node_port probes 0.0.0.0, a collision Linux raises and other hosts do not, so the busy case's fall-through was not asserted everywhere. Holding each probe on the wildcard address the assigner itself addresses makes the collision unconditional, and the freed case the same inverse of the busy one. * fix(sessions): bound the harness's interim arm to an address no row holds The publish-verb proof restated the announced interim as any in-plan address, so a publish at a held address whose row refuses a record read as applied while the decision refuses it under either phase. The oracle now grants the interim only where no row holds the address, and a retraction's interim only where no row holds its records. The Kani lane expects the ninth sessions harness. * fix(minvmd): hand the node row its ports in the merged-in spoofer test The merge of main brings gominimal#1792's vm_escape test, which registers the node namespace with the signature main had; this branch's takes the node's proxy and answerer ports. * fix(sessions): key the switch retract by the row at its own address A retraction was decided table-wide: it applied whenever any published row held the record it names, so a retraction could withdraw a record a publication at another address had made. Read the row at the address the summary carries — the publication's own, as the gate attributes it — and apply only when that row holds every record; otherwise Refusal::Unheld, which now carries the address for the refusal line to name. The announced interim stays for an in-plan address no row holds, as for a publish. The Kani harness restates the admit per address for every verb, and the unit test pins a retraction justified only by another namespace's row as refused. * fix(minvmd): attribute each switch retract to its publication's address The unexpose body names only the loopback listener it retracts, and the pure decision now applies a retract by the row at its own address — so the gate supplies that address itself, from a publish ledger kept beside its limiter: every applied publish files its listener and the address it was applied at, and an applied retraction takes its listener out. A retraction for a listener no applied publish names is keyed at the unspecified address, which no row holds, and refused under either phase; the same request was applied table-wide before, so a fabricated retract of a port some row declared travelled to the switch. The interim's own teardowns key at the lease their publish went out at, under the announced phase that applied them. The interim's admit line is marked interim and reads verb-neutral, and the phase's docs now say the two bounds its admits carry: read once per build, never changed while a VM runs; lease-run addresses only, never the node's own address or the plan's reserved pair. The withdrawal test is renamed for the connection it proves — the box's shuttle relay, which ends with the box's traffic, not with the box: creator-driven withdrawal at destroy lands with T66 (gominimal#1711) — and the registry drainer's doc says the same. * fix(minimald): fail the boot on a handed node port that cannot serve A boot token present but unusable — unparseable, out of range — was warned about and counted as absent, sending the daemon into its own default-then-select and publishing listeners the host's box table does not name. The read is now a Result: only an absent token, or the host's own 0 as 'pick one yourself', leaves the pre-handoff fallback; anything else is a surfaced boot error naming the token and the value it carried. The pid-1 branch reads the tokens once the log sink is live and probes the handed pair in the microVM's bind base before the daemon starts, so a port something in the guest already holds ends the boot with the error surfaced, never after READY when the host already believes the VM healthy and never rescued by a re-pick. * fix(minvmd): resolve the node ports once for the handoff and the row Directive finding 4 (T63 round 5): run.rs resolved the pair itself while vm.rs re-read MINVMD_NODE_*_PORT off its own env and silently fell back to absent on garbage, so a half-set or mistyped override could boot the guest onto ports different from the ones the node row registered. Now run.rs resolves each port once — the operator's override in the supervisor's own env (the same names the child transport decodes), refused fail-closed when it is unparseable or 0, else the default-first probe — and the one resolved pair is written twice from the same value: onto the VMM child's env (the explicit .env shadows any inherited override) and into the node row's own publishes. vm.rs's decode becomes strict transport decoding: both-or-neither, a half-pair or an undecodable value fails the boot naming the variable and the value. Its read stays in vm.rs because the decode's only production caller is apply(); moving it to cmd/vmm_child.rs is out of this task's layers. node_port_assigned_on_host_and_handed_to_daemon (both the run.rs and the vm.rs test of that name) now pins the resolution through the override and asserts handed == registered, plus the decode's strict cases. * fix(minimald): set the dropped box_addresses in two test constructors T14's (gominimal#1765) merged session tests construct `SessionConfig` and `SandboxLauncher` without the `box_addresses` field their declarations require, so minimald's test targets fail on E0063 and every lane that builds them — tests, minimald-root-integration, clippy — goes red with them. Both mean a session the activating client did not register, which self-allocates as it always has, so the value is `None`. * fix(minvmd): keep the node's row off the relay's withdrawal report A frame relay's end files a withdrawal report naming every admitted frame's source, and the node plane's own frames were among them: their source is the daemon's own address, admitted by the node's row, so one relay end — a shuttle error, an oversized frame claim — withdrew the row the run path registered once at boot. Nothing re-registers it, and the announced interim cannot reach it (the plan keeps the node's address outside the lease run), so the in-VM daemon stayed frameless and unpublishable for the rest of the VM's life over a close its control path rode out. The gate now attributes the node's own address to nothing: the row that decides its frames is the host's registration for the VM's lifetime, not a box's row that goes with its shuttle connection (NET-133). Pinned by node_row_survives_the_relay_that_carried_its_frames, which watches a box's row go with its relay while the node's row stands and its frames still pass on the next connection. The withdrawal test takes its surveyed name, host_table_row_withdrawn_within_60s_of_box_end, so the plan's line runs it: it sat under ..._of_relay_end, which a nextest filter for the surveyed name matches nothing of and exits 4 on. * ci(kani): count the publish-verb harness in the lane's gate The lane asserts the harness count, not just the exit status, so a `#[cfg(kani)]` module that stops compiling cannot go green having proved nothing. The publish-verb decision's harness (kani_switch_request_applied_iff_table_admits) raises the sessions suite to ten; the gate still said nine, so the lane failed its own count with every harness verified — reproduced locally on 0.68.0: "Complete - 10 successfully verified harnesses, 0 failures" against an expectation of nine. * fix(minvmd): publish by the listener and defer the name-declaring drop The row's publish decision read both ends of an exposed mapping, but the registration wire carries only the external ports, so every mapping whose ends differ — most of them, an own-address box's whole ingress — was refused and the attach died with it. The record is now the host-side listener alone; the inside end is the target's own, decided by its in-guest ingress rules. A row that declared DNS hosts now defers the undeclared-destination drop to the in-guest decision: name-based admission is resolution-time pins the host's static rules cannot see, so making the drop here vetoed every pinned frame the box's own declaration granted. Denied ranges, protocols, sources and families stay host-made. The zone-adds the daemon publishes its box's name with — the bare form and the deprecated host-qualified one beside it, host ids unbounded — map onto the row's own name now instead of dying as undeclared; a foreign name is still refused, and the address keying keeps the mapping the owner's. * style: cargo fmt the publish-verb edits * fix(minvmd): refuse frames from a box to the switch's gateway address The switch's own address is a control surface, not a destination a box's egress rules decide (design $4.1, $7.1). The gate's frame decision now refuses every frame to the plan's gateway on a port that is neither the resolver's nor the source namespace's declared exposure, before the row's decision and the interim, under every phase - so no allow-all row, no announced concession, and no per-box default can admit a frame at the switch's own address. The exceptions fall through to the decision behind the refusal, which still decides them, so the resolver carve-out and a declared exposure admit what they admitted before. The refusal's warn line is rate-limited like a drop's and names the box's address and the port. Pins at the pure decision and at a live gate: two allow-all boxes (one with no egress section, one with a declared one) and an unregistered in-plan source are refused at the gateway while the resolver's port still answers and the declared exposure passes. * test(minvmd): pin the node row's exclusion in the withdrawal report The round-6 finding's fix - the relay never attributes the node plane's own address, so its row is never filed for withdrawal - is watched at the report itself: one relay carries a node-sourced frame and a lease-run frame, ends, and the report the host files names the lease-run address only, with the node's row still standing. The report is read off the channel the drainer acts on, not inferred from the rows left after it. * style: cargo fmt the gateway-refusal edits * fix(minvmd): admit only the resolver port at the switch's own address The control-surface refusal at the gateway excepted a port the source row admits as well as the resolver's. Those admitted ports are the box's ingress - what others reach on the box's own address through the switch's forwarders - and no box-to-gateway flow at them exists in the design, while gvproxy's API listens on the gateway address, so a box declaring ingress port 80 could reach the switch API. The exception is gone: at the gateway the gate admits TCP or UDP to port 53 only (a query falls back to TCP on truncation, so the carve-out is by address and port, not protocol), and every other port and every other protocol, ICMP included, is refused before any row or phase is consulted. The relay test drops the admitted-port cases, adds a TCP 53 frame from each registered box that reaches the switch, and an ICMP frame from a registered box that is refused; the pure decision pins a frame to the gateway at the row's admitted ingress port as a control-surface refusal. * fix(minvmd): cut a rendered target name on a char boundary render_record truncated a dictionary name to MAX_NAMED_TARGET with String::truncate, which panics when byte 64 falls inside a multi-byte UTF-8 character. The name is a guest's bytes, so a hostile name could panic the gate's warn path. The cut now lands on the largest char boundary at or below the bound (str::floor_char_boundary, stable on the pinned 1.97.0 toolchain). Adds render_record_cuts_names_on_a_char_boundary: 63 ASCII bytes then a 3-byte character, exactly 64 bytes of 2-byte characters, and every ASCII run length up to the bound, each rendering without a panic to at most 64 bytes of valid UTF-8. The test panicked at the old truncate before the fix. * fix(sessions,minvmd): refuse a guest withdrawal of a declared port The pure decision applied a Retract when the row at the retraction's attributed address HELD the record, and a row's held set is its declaration, so a guest unexpose of a declared forward was applied and the forward withdrawn. Design $7.1 binds a declared port's forward for the session's lifetime, unbound only by host-side ingress revocation (NET-121); a guest request withdraws only what its own listens published (NET-016, NET-017). SwitchRow gains a runtime-published port set, empty from SwitchRow::of (every call site compiles unchanged) and filled by with_published, which the Retract arm now decides against instead of the declaration: applied only when every record is in the runtime set, refused with Refusal::Unheld otherwise. The unheld-address arms are unchanged, so the announced interim still applies an in-plan retraction no row holds. minvmd's projection leaves the set empty until listen-publishing lands, so today no guest retraction at a held address is applied. Tests: switch_request's retract_of_declared_port_refused pins the refusal at the row's own address for a declared port and the node's assigned port, with and without other runtime publications, and the applied case moves to a listen-published port; egress_gate's retract_of_declared_port_refused publishes a declared forward, has the guest unexpose it on the shuttle, and sees it refused and logged with the row still admitting 8080 and the forward publishing again. The keyed-retraction test now reads the attribution off the refusal's source. The Kani harness kani_switch_request_applied_iff_table_admits models the published set as a second symbolic list and restates "admits" per verb: declaration for a publish, runtime set for a retraction. The harness count is unchanged. * fix(minvmd): bound the control-body read like the head `serve_connection` bounded only the handshake, so a guest that sent a control head declaring a `Content-Length` and then withheld the body held the relay task, the gate's dial, both socket halves and one of the `MAX_LIVE_RELAYS` slots for the gate's lifetime; 64 such connections had `accept_loop` refuse every guest connection after them, frame relays included. `relay_control` now reads the body under `drain_timeout`, the bound the leg already gives a guest gone quiet past its request (the same value `serve_connection` reads the head under). A read that times out is handled like a guest that closed mid-body: nothing is written on, one rate-limited line names `egress-undeclared-verb`, and the relay ends so the slot is returned. `accept_loop` takes the bound as a parameter so a test can shrink it; `EgressGate` still passes `HANDSHAKE_TIMEOUT`. The new test fills the cap with withheld bodies and checks each is closed within the bound with nothing written to the switch, then that the next connection is served. * fix(minvmd): accept a leased-loopback local in the publish gate The gate's loopback_port parsed only 127.0.0.1:<port>, so every own-address box's ingress expose - and its teardown - was refused as malformed before the row decision: on a VM-backed host the daemon's client builds local from the box's granted address in the reserved local range (NET-010, NET-129), never 127.0.0.1. Accept both spellings the client builds - 127.0.0.1 and the reserved local range - and keep refusing every other spelling as malformed, with a test on each side of the line. * test(minvmd): prove a name-resolving row keeps every other host-side drop The gate defers one drop class for a row that declared DNS hosts: the undeclared destination, decided in the guest where the resolution-time pins are. Pin the edge of that deferral from the other side: for the same row shape, a destination in its own deny_subnets, the switch's own address, a protocol its rules do not allow, and a source no row holds are all still dropped on the host, under their own rules, with no undeclared-destination line. Say so at registration: BoxRegistry::register emits one info line per name-declaring row, naming its switch address, so the host's log carries the deferral rather than leaving it to be inferred from a frame that reached the switch. The line goes away with the deferral; moving the decision host-side is gominimal#1808. * docs(minvmd): name the withdrawal drainer as process-lifetime The drainer's doc comment claimed the thread runs until the reports' senders are all gone — the gate and every table handed out. That exit is unreachable: the thread holds a clone of the registry, and a clone carries a withdrawal_reports Sender — the very channel the thread is draining — so recv() never reports the channel dead and the loop never exits. Say the process-lifetime truth instead, and say outright that teardown cannot rely on the thread exiting, so no future reader builds teardown on an exit that cannot happen. * feat(minvmd): refuse infrastructure destinations at the host gate for every row The design's infrastructure deny set (section 5.3) applies to every box-plane packet, CIDR-admitted direct-IP flows included, so the host-side gate now decides it as a frame rule for every row, between the source's routing and the row's own rules: link-local and the metadata services in it, loopback, the fabric plane outside the node's own switch block, and RFC 1918 space the row's allow_subnets does not cover. A row that declared DNS hosts defers only its undeclared-destination drop; this one is the host's own, whatever the row. The switch's gateway stays with the control-surface rule, and the node's own block is local reach the row's CIDR rules and the target's ingress decide. The host rule is built beside the sessions crate's InfrastructureDenySet rather than from it: that set keeps its ranges private, names the gateway's addresses, and admits or refuses the whole plane by whether a name is a box-zone name, which the rebinding intersection relies on and a frame cannot answer. An undeclared allow_subnets counts as covering private space, as the rebinding exemption holds it, so the two allow-all spellings keep the same reach. The drop is egress-infrastructure-destination, rate-limited per source like the other drops and naming the destination and port. The spoof-union test's db box moves from 192.168.0.0/16 to TEST-NET-1 so its own subnet is not private space, and its two spoofs into web's private subnet are pinned to the new rule. * fix(minvmd): apply the infrastructure rule to interim-admitted sources A source the announced interim admits without a row returned before the infrastructure check, so its frames reached link-local and other nodes' blocks unrefused. The set applies to every box-plane packet: the interim now takes it too, as allow-all for RFC 1918 space, and the infrastructure test covers such a source. * fix(minvmd): key the publish ledger by loopback address and port A forwarder listener is its loopback address and port. Two boxes publishing one port at their own reserved-range leases are two listeners, so the ledger now keys each publish and retraction by the pair the body's local names. --------- Co-authored-by: minimal-foundry[bot] <327719912+minimal-foundry[bot]@users.noreply.github.com>
yermakoffivan
pushed a commit
to yermakoffivan/minimal
that referenced
this pull request
Oct 3, 2026
…ished ports instantly (gominimal#1798) * fix(minimald): fill box_addresses in two test initializers gominimal#1765 added SandboxLauncher.box_addresses and SessionConfig.box_addresses but updated only one of the three initializers, so the package's test targets no longer compiled. Fill the two it missed (the own-ip session request fixture and the sandbox launcher fixture) with None, the value every other initializer carries. * feat(minimald): refuse unpublished ports and revoked ingress at the gate The switch relay's ingress leg dropped every refused TCP frame silently, so a connection to a port nothing published hung until the peer's timeout; and a revoked port (NET-121) had no way to end the connections its forwarder held. - a SYN to a port the box's ingress declaration does not name is now answered with a reset built from the SYN itself (tuple swapped, the box's address as the source, RST|ACK, ack riding the SYN's sequence plus its flag weight, honest IPv4 and TCP checksums), so the peer's connect fails at once with connection refused while the box's kernel never sees the connection (NET-014). Unsolicited UDP stays a drop: a datagram is not a connection. - the gate now tracks the tail of every admitted inbound TCP flow and revokes a port on demand: it admits the port no longer, answers every packet to it with a reset, and terminates each held connection with a reset built from the flow's own last packet, which an established peer reads in-window (NET-121). Revocation is wired to the ingress forwarders in the next commit. - the reset legs write through the same framed switch write half as the egress leg, under a shared mutex, and unbind revocation says 'revoked ingress port' where a mapping refusal says 'no ingress mapping' — both rate-limited with the peer and port, so the daemon log's tail names each refusal. - compile fallout of the gate's new Arc signature: the DNS-gate tests' L4Packet literals gain the sequence pair, the netns harness wraps its gate as the attach now takes it. unpublished_port_connection_refused drives the refusal end to end on the relay harness: the reset's bytes, the silent box end, the still- forwarded declared port, and the log line. * feat(minimald): the coder's uncommitted work as it stood when its 7200s ran out the coder's uncommitted work as it stood when its 7200s ran out The coder was stopped at the end of its time with these changes not committed. The runtime committed its working tree as it stood so the work is kept: this commit is a snapshot, not a finished step, and may not build or pass its tests. * test(minimald): fix the NET-121 proofs' fixture and teardown driving Three of the four NET-121 proofs had fixture bugs that kept them from passing: the registry route is looked up as the full zone name the registry answers (web.min.internal), not the bare two-label box name; the fixture switch now carries the same instance host id the proofs' registry is built with (aaaa1), the pairing the daemon itself makes, so the attach publishes both host ids' dns/add requests the revocation proof counts; and the bound-forwarder proof drives the guard's explicit teardown instead of dropping it, which only aborts the relay and leaves the forwards standing. * fix(minimald): keep the expose record's message the session e2e reads The per-forwarder bind line's wording is a contract beside its fields: scripts/session-e2e.sh's published_loopback_host reads the publish record — the host address the forwarder actually bound — out of the daemon log by exactly the phrase 'exposed ingress port on the host loopback', three call sites. Renaming the line to 'bound declared ingress port' left that reader matching nothing, and the native-daemon e2e lane failed in the fresh-install loopback-publish proof at the record read. Restore the wording and note the contract at the line. * style(minimald): rustfmt the test imports * fix(minimald): bound the reset channel and shape the gate's resets The ingress gate's resets now ride a bounded channel — a send past the bound is dropped, never queued — and are drawn against a per-source windowed budget, so a box flooding SYNs at another's ports degrades to a timeout alone while every other peer is still refused at once; the first refusal a window refuses is one audited warn line per source per window. The two reset shapes follow RFC 793 §3.4, and both are built only from state the gate holds: a bare SYN to an unpublished port (NET-014) is answered RST|ACK from sequence zero acknowledging the SYN, and a connection a revocation ended (NET-121) is answered from the tail the gate tracked, so the self-healing second reset stays in the window the gate watched. A segment of a flow the gate holds nothing for — a spoofed one — is answered with no reset at all, so this box can never be made to emit a reset carrying a spoofed sequence to a victim; every reset is addressed to the frame's source. The refusal stays TCP-only by design (design §7.1): a UDP datagram is not a connection and keeps its silent drop. * fix(minimald): publish a handed box at the address its row gave it A VM-backed box's registration carries the addresses the VM host daemon handed it (T66), and the host loopback half is the address the host-side table's row owns — not a grant this daemon's in-guest book could hand out. The finalize publish now prefers the handed address over the lease, so the attach path's expose requests name exactly it as their local: never the node's shared 127.0.0.1 interim, never an address the daemon chose. A handed box never draws from the loopback pool: the row owns the address, so neither the grant's info line nor the release at destroy runs for it. * test(minimald): prove NET-121 from the host client's side of the port The gvproxy stand-in now answers with reason bodies, so the failed-bind proof covers both shapes a bind can fail in: the switch's gate refusing an expose (403 with its reason) is a failed bind exactly like a bind that errors — the attach fails, the refusal's reason reaches the caller beside its port, and every bind that landed is rolled back, so a half-bound box holds nothing. The revocation proof is now end to end against a forwarding stand-in that binds real host listeners: a real client socket connects to the port, the stand-in opens the client's leg through the relay, and the revocation ends the client's connection — EOF or reset within the bound, never a hang — while the next connect is refused, not accepted-then-dropped, because the unexpose dropped the listener before the revocation returned. The reset that ended the connection is the gate's, read off the relay and addressed to the leg. A new proof pins the attach's local as the handed host loopback address: the binds and the teardown both name the row's address and the declared ports, never the node's shared interim. * test(minimald): frame the budget proof's flood one prefix per frame * fix(minimald): carry the TCP protocol in its own pseudo-header byte The pseudo-header's fourth word is big-endian [zero][protocol], so the protocol contributes itself (6) unshifted; the << 8 it was built with parked it in the zero byte's place (0x0600), giving a checksum no TCP stack verifies, so every reset this module built was dropped at the peer that was meant to receive it. RFC 793 §3.1 is the reference. The test helpers that judged resets now verify the checksum by the wire's own definition — assemble the pseudo-header from the frame and fold the sum to 0xffff — instead of recomputing it with the same function under test, and a known-answer unit test pins 0x23f2 for a fixed segment, checked against an independent implementation off-tree. * fix(minimald): scope a revoked port's termination to its own forwarder revoke_ingress found its forwarder by external port but revoked the gate by internal port, so with two mappings publishing the same in-box port, revoking one ended the sibling's connections too. The gate cannot tell forwarded connections apart — a box's inbound frames carry only the internal port — so the revocation now withholds the gate's termination while another live forwarder still serves that port, and the port's connections end when the last forwarder to it is revoked: the first moment they can be told apart at all. The forwarder records a successful unbind on an Arc<AtomicBool>, so teardown skips the unexpose for a port already revoked and a revocation that failed at the switch stays unrevoked, with both retry and teardown still having work to do. The end-to-end test drives two external ports into one internal port, revokes the first, and shows the sibling's established connection surviving and new ones still completing its handshake; the last revocation ends all three. * test(e2e): expect the unpublished port's refusal, not its timeout NET-014 makes the ingress gate answer a SYN to a port the box never declared with a reset, so the parity proof's pair-4 direct leg is connection-refused (curl 7) rather than the dropped-SYN connect timeout (curl 28) the proof was asserting — the macOS e2e run at this head failed on that stale expectation, which is what the ci-macos lane was red on. The pair's parity claim stands: the proxy's 403 beside the direct refusal, both by the one declaration. The caller-egress pair keeps its connect timeout: NET-062 binds a denied egress connection to a drop without a reset, and that path is untouched — the unit proof 'disallowed_egress_dropped_not_reset' still holds it. * fix(net): end a revoked connection at the box and never answer a reset A revocation terminated only the switch side of the connections it held: the peer's socket was reset, while the box's own half rode on into a forwarder that no longer existed. The gate now carries a second bounded channel of box-directed resets, taken by the relay's spawn and drained by a writer into the tap, and a revocation sends each tracked flow one reset from the peer's address at the peer's next sequence — the sequence the box's socket is windowed to receive, so the kernel ends the connection at once. The refusal half learns RFC 793's one forbidden exchange: a segment that is itself a reset is answered with nothing, before any budget is spent — the ended connection's stragglers are resets, and charging them against the source's window would let one ended connection spend the peer's refusals on answers that cannot exist. * fix(net): publish only at a handed address and withdraw on a failed bind NET-010/NET-011's hand model, item 7: the daemon never chooses a box's published address. `published_or_node` and its loopback fallback are gone — `own_route` answers only from a published row, so `register_own_ip` holds a name only when a publish stands behind it, and finalize's pool lease is gone with it: the only address a box ever publishes at is the one its record's `box_addresses` row hands (T66) or one an earlier finalize published. Consequences, each proved: - A launch nobody handed an address registers no name and publishes nothing; its attach fails with "no published address handed for box B" after the same rollback a failed bind takes, instead of binding forwards at an address nobody chose (gvproxy proofs: no-reporter and reporter-with-no-hand shapes). - The daemon registers only the in-guest zone. Host-OS name publication belongs to the host-side creator whose row handed the address in; the registry's interim (shared-address) mode is removed, along with its collision report — the cross-record report at session start and the cross-node one at the daemon's start stay. - A bind failure at attach withdraws the name finalize registered (item 4): a box whose forwarders cannot bind answers NXDOMAIN rather than a name routing at an address nothing binds, so both gvproxy proofs now drive the real finalize sequence and assert the name held before the binds and absent after a failed one. - A handed 127.0.0.1 is used exactly as handed — the address the old default published at, now sourced from the hand that named it. The session-side lease tests become hand tests: each box hands its address through its create's registration row, a box nobody handed one registers no name, and the shared-address collision proof reports two boxes handed one address rather than two interim publishes. provider, proxy and answerer follow the same model at their report sites. * fix(net): publish at the answerer's grant when no creator handed one e6e21ef read "the daemon never chooses a box's published address" as "finalize never asks for one" and removed the pool lease outright, so a box nobody handed an address — a native `min session activate --network own_ip --ingress`, whose creator is the daemon itself (NET-040), or a VM lane whose client spelled no provider to register with — published nowhere, registered no name, and failed its attach with "no published address handed for box B". Both e2e lanes that activate an own-IP box with a declared ingress run exactly that shape. Restore the finalize lease: the hand (T66) still stands first, an already-published row second, and the answerer's record third — the host-global allocation NET-010 binds, arbitrated through the answerer's authenticated channel, which no daemon self-assigns beside. The grant is asked before any forwarder binds, so the binds and the name answer at the one address it granted; a grant withheld (spent pool, absent range, pending verdict, unreadable record) still publishes nothing and registers no name, and the attach of a box that declared ingress still fails with "no published address handed" rather than binding forwards at an address nobody granted — reported, never substituted. The session-side no-hand proof becomes the grant proof it always was: a finalized box nobody handed one publishes at the record's first grant, the route and the zone answer name it, and the lease says its line. The handed proofs and the attach-level refusal proofs are untouched. * fix(net): publish the interim when the surface cannot bind the range The macOS e2e lane failed at the first exec into an own-address box activated with `--network own_ip --ingress`: activate succeeds (the host launches lazily at the first exec), and the exec fails because the attach does. minvmd hands the box's registration a slice address of the reserved local range without measuring the loopback it binds on, and on a stock macOS host the deferred forwarder-conducted walk lands the range absent — so finalize published the hand verbatim and the attach asked the host gvproxy to bind a declared port at an address the surface refuses at every bind (EADDRNOTAVAIL), failing the whole attach. Main stays green on the same lane by publishing at the node's interim; the branch's fail-closed reading dropped that and made the lane red. NET-123's absent arm is the rule the branch dropped: a host whose publish surface cannot bind the range publishes the box at `127.0.0.1`, never at an address nothing has vouched for. Restore it in the publish decision, where the address is chosen: - `LoopbackLeaseBook::vouches_for` gates a handed address on the verdict the host's publish surface holds. A verdict still walking trusts the hand's own provenance — the host-side table row a resumed box keeps its address on inside the walk's window (NET-013, and the pending-window proof stays green) — while a landed absent verdict overrules it: an address the surface cannot bind is not publishable, whatever handed it. - `LoopbackGrant::publishable_address` says what each ask's answer publishes at: the granted address; the interim for the two answers that are facts about the surface (absent range, pending verdict); nothing for the two that are faults (spent pool, unreadable record), which still fail the attach of a box that declared ingress with "no published address handed" — reported, never substituted. A failed bind is untouched: the forwarders still bind before the name registers, a bind that fails still fails the attach and withdraws the name with one warn per port, and the interim is not a substitute — it is the surface's own answer about what it can bind. The KVM lane is unchanged (Linux binds the whole 127/8, so the walk lands present and the hand stands), and the native lane is unchanged (the probe reads present before the book opens). The two dns units pin the gate and the mapping; the macOS lane is the end-to-end proof. * fix(net): re-point the window's publishes when the verdict lands The deferred walk's landing only moved the book's verdict; the publishes the pending window had already made kept whatever address the window gave them, and two of those cannot stand under the verdict that replaces it: - A handed reserved-range box finalized inside the window was published at the hand the pending verdict vouched for by provenance alone — an address the host has not measured. When the walk landed absent, the arm only warned: the hand stayed in the registry, `already_published` kept it on every later finalize, and only destroy cleared it, so the box failed its attach with EADDRNOTAVAIL at an address the surface cannot bind. - A box nobody handed an address was published at the `127.0.0.1` interim the window's ask answers with. When the walk landed present, the interim stayed: it is recorded as the box's own publish, so the record kept it until destroy. The landing is the one moment the daemon holds both facts — the verdict and every publish it contradicts — so it now runs the verdict's arms (`land_range_verdict`): an absent landing re-publishes every own-address publish inside the reserved range at the interim, name and route with it; a present landing re-asks for every publish standing at the interim and re-publishes the grant it is given, with one warn line per box the re-ask is refused for. The finalize path reads through the same gate: a recorded publish the verdict now contradicts, or one standing at the interim, asks again rather than answering from the record — so the interim cannot outstay the window that made it, in either direction. The verdict is set before either arm runs, so a finalize racing the landing reads the landed verdict and its filters agree with the sweep. minvmd measuring the host's loopback before it hands is the root fix for the hand (gominimal#1818); the verdict gate and this landing hold the interim until it does. Proofs: a handed box finalized inside the window publishes at the hand, then moves to the interim when the verdict lands absent and the name answers there; a box nobody handed publishes at the interim, then takes its grant when the verdict lands present and the name answers there; and a handed reserved address finalizes to the interim under an absent book and to the hand under a pending one — the wiring test for the hand's `vouches_for` gate, which fails when the filter is removed. * fix(net): publish a handed box only under a landed present verdict NET-123 §7.1/NET-013: a hand now vouches only for a landed Present verdict, so a finalize holding an unvouched hand waits for the verdict — bounded by the session-start deadline the client already uses (5 s) — and publishes once at its final address; an expired wait publishes the 127.0.0.1 interim, which the present landing's sweep upgrades to the hand it now vouches for. The landing is broadcast on a watch channel whose opening receiver the book holds, so a verdict landed before any waiter subscribes is still read. The present landing's arm draws each move's grant outside every registry lock and re-checks — under the write lock — that the box still exists and stands on the interim before it publishes; a box destroyed inside that window is not resurrected, and the grant drawn for it is released. Every move (hand to interim, interim to grant or hand, interim back under an absent landing) logs one warn naming the box and both addresses. * style(net): normalize the new verdict-wait code to rustfmt * fix(net): store a landed verdict past the watch channel's zero-receiver edge set_range_verdict moves the landing through send_replace rather than send: a watch send with no receiver is dropped on the floor by the channel itself, and a landing often arrives while nothing waits on it, so the registration that subscribes afterwards must still read the verdict that landed. This replaces the book's held witness receiver. * fix(net): wait on one daemon-wide verdict deadline and never grant a handed box A handed box whose hand the range verdict does not vouch for now publishes at the 127.0.0.1 interim and never asks the pool for a grant. Under the registry write lock, a registration re-reads the verdict and promotes the interim to the hand when a present landing has raced it. The verdict wait is one deadline for the daemon, the book's open plus HAND_VERDICT_WAIT, and every waiter races that same instant. Only a box's first finalize waits. Session::run (resume, create, destroy-hook bring-up) and rename never wait: they publish the interim and the present landing moves them. Under a pending verdict the grant answers every namespace with the interim, a recorded one too, and keeps the record's line, so no reserved-range address publishes before a landed present. The present landing restores the recorded address. The present landing's discard releases a drawn grant only when the box's publish is gone, and its draw no longer grants for a handed box whose hand is unvouched. Tests poll a verdict-waiter count before landing, prove the discard's own release, and cover no-wait resume and destroy, the shared deadline, the resumed recorded address, and a re-registered box keeping its grant. * test(net): pin the landing's re-check and the finalize-destroy order The present landing runs on the deferred walk's spawned task, off every mailbox, so its apply's write-lock re-check is the runtime guard; say so at the spawn site and on apply_interim_upgrade. Add a test that destroys a box between the landing's enumeration and its grant: nothing is re-published and the grant is released exactly once, by the discard. Add a test that queues a destroy behind a finalize waiting at the verdict deadline: the publish at the hand precedes the removal, and no name is left. * test(net): pin the write-lock promotion of an interim to a vouched hand Extract the decision register_hostname takes under the registry write lock into promote_interim_to_hand and test it directly with no timers: an interim publish with a hand moves to the hand under a present verdict, stays on the interim under an absent one, and never moves over a name another session holds (HostnameRegistry::name_held_by_another). * test(net): pin register_hostname's own promotion of an interim The helper's unit test pins the decision promote_interim_to_hand makes; this one pins that register_hostname makes the call: drive the registration itself, with the ask answered "not vouched" and the verdict landed present before the write lock — the exact window the re-read under the lock exists for. The drive is the box's first finalize parked on the pending verdict, the one await between its ask and its publish; the test holds the registry's write lock across that park, wakes the ask with an absent landing, waits for its waiter to drain (the proof the ask consumed the absent answer), stores the present verdict through the raw book store — never the landing's sweep, which would take the very lock being held — and then releases the lock. Nothing decides by a deadline. Removing the call leaves the box standing at 127.0.0.1 and fails the test; restoring it publishes and answers at the hand. --------- Co-authored-by: minimal-foundry[bot] <327719912+minimal-foundry[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
T14 — Give each box its own loopback address and answer its name from finalize to destroy
slice: S3
kind: task
covers: NET-010, NET-011, NET-012, NET-013, NET-128, NET-129
size: L
est: 400 code, 480 tests
executor: agent
difficulty: needs care
model: strongest
diagnostics: the bundle's zone dump shows each box's loopback address and state, and the daemon log tail names each lease, release and shared-address collision
observability: one info log line per address lease and release naming the box and the address; one warn line per shared-address port collision
layers:
- core:
- crates/sessions/src/core/loopback.rs (new): the pure allocator over one gvproxy's slice of the reserved range, with its Kani harness; injective within the slice, and the slices are disjoint, so no two live boxes on the host share an address
- crates/sessions/src/core/mod.rs: declares the loopback module
- scripts/kani.sh: expects one more sessions harness
test (deferred: kani): cargo nextest run -p sessions kani_loopback_alloc_injective
- daemon:
- crates/minimald/src/net/policy.rs: expose_request publishes on the box's own address at the box's own port numbers and reports shared-address collisions
- crates/minimald/src/net/gvproxy_network.rs: passes the box's loopback address through the attach
- crates/minimald/src/net/dns.rs: holds per-box state: address, stopped as NODATA, a host-address box answering its node's address
- crates/minimald/src/session.rs: allocates at finalize and applies declared ingress there, so the name answers with no client attached
- crates/minimald/src/session_host.rs: marks the name stopped when the host exits
- crates/minimald/src/sessions.rs: builds the allocator over the daemon's own gvproxy slice beside the registry; no daemon asks another
- crates/minimald/src/session/tes 8000 ts.rs: hosts the finalize, destroy and no-client name tests
test: cargo nextest run -p minimald each_box_gets_own_loopback_address
test: cargo nextest run -p minimald name_registered_at_finalize
test: cargo nextest run -p minimald destroyed_box_name_is_nxdomain
test: cargo nextest run -p minimald name_answers_without_attached_client
test: cargo nextest run -p minimald stopped_shared_address_box_is_nodata
test: cargo nextest run -p minimald host_ip_box_answers_node_loopback_address
test: cargo nextest run -p minimald shared_address_port_collision_reported_not_translated
produces:
- crates/sessions/src/core/loopback.rs
consumes:
- crates/minimald/src/net/answerer.rs
proof: Two boxes listening on the same port answer at two different loopback addresses by name, boxes behind two gvproxies on one host never share an address, a name works from finalize until destroy whether or not a client is attached, and a destroyed box's name answers NXDOMAIN.
depends on:
- blocked by #1633
- blocked by #1616
Out of time
The coder ran out of its 7200s before it finished. If it left work uncommitted, its last commit is the runtime's snapshot of that work as it stood — the commit message says so — and not a finished step: it may not build or pass its tests. So this PR is a draft.
Proof
Two boxes listening on the same port answer at two different loopback addresses by name, boxes behind two gvproxies on one host never share an address, a name works from finalize until destroy whether or not a client is attached, and a destroyed box's name answers NXDOMAIN.
Proof
Two boxes listening on the same port answer at two different loopback addresses by name, boxes behind two gvproxies on one host never share an address, a name works from finalize until destroy whether or not a client is attached, and a destroyed box's name answers NXDOMAIN.
This is an interim. One daemon's state root holds one lease record, so the record arbitrates addresses across the boxes of that root only; the cross-root case (two roots on one host, or a VM guest beside its
minvmdhost) is reported from the kernel's socket table at session start and warned about at grant time, not prevented. The host-side answerer as the one arbiter over every root's allocation is filed as #1772.Rounds 1 through 10 ran under the runtime; the last round landed the grant-time duplicate check under the existing flock, the book doc naming the one-root scope, and the per-box warn on a landed absent-range verdict. A bot-authored hand commit after round 10 removed an unreachable refusal arm, renamed the duplicate-record test to what it proves, and linked #1772 from the module doc.
Tests
The plan's seven
minimaldtest lines run in thetestsandminimald-root-integrationlanes of this PR's CI; thekanilane runs the deferredkani_loopback_alloc_injectiveharness. See the checks on the head commit.Verify
Proved by the PR's CI lanes (
ci-success,ci-linux-native-success,ci-linux-kvm-success,ci-kani-success) on the head commit rather than by the runtime's verify task, which ran out of time on earlier rounds.Out of layer
These files are outside the task's
layers:and were changed because the per-box address has to reach the places that read it:crates/minimald/src/net/provider.rs: the provider carries the box's loopback address through to policy.crates/minimald/src/server.rs: the daemon wires the lease book beside the registry.crates/minimald/src/session_host/tests.rs: the host-exit test asserts the stopped name.crates/minimald/tests/netns_root_integration.rs: the root integration test publishes on the box's own address.scripts/session-e2e.sh: the e2e expects the per-box address in the zone dump.Closes #1645