Repository navigation
test(e2e): stop only this run's bep serve in the round-three walk
PASS_WITH_CONDITIONS
Baseline. This re-reviews b3e7c41c against the PASS_WITH_CONDITIONS on 208b4a57 (this PR), on arch checkout 109541a4. The checkout has no arch-map.md, so I started from the lines the baselines cite: Gatehouse §6.10 lines 836, 839 and 842, and networking §5.3 line 150 and §5.7 line 218. No findings.json was staged. I checked that since.diff equals git diff 208b4a57 b3e7c41c and that pr.diff equals git diff e8a7bd8c b3e7c41c.
Compare. One commit. A new r3_proxy_pids replaces pgrep -f '/bep serve ' with a match on serve --listener $XDG_STATE_HOME/minimal/providers/local-minvmd0/gvproxy-bep.sock. That is the argv that crates/minvmd/src/cmd/run.rs gives bep serve (serve, --listener <listener>, lifeline flag). The listener sits beside the switch socket under the provider directory. A person's own proxy, or a proxy from another checkout, no longer gets SIGKILL. When nothing matches, r3_proxy_down returns 1 and the widened-rule case fails on an empty wr_pid_before. So the narrower match fails closed (rule 7).
Governs. §6.10 line 842: redemption checks upstream and inject against the current registration, and jti is the audit correlation id (BEP-032, BEP-039, BEP-063). Line 839: creation refuses a colliding id, and the hash-chained log is restored from every retained segment (BEP-041, BEP-070). Line 836: the node-local BEP is the audit source of record. Networking §5.3 line 150 and §5.7 line 218: UDP/443 toward the steered BEP is actively rejected (BEP-018).
Ruling. The cases have the shape the design gives, and each fails closed. The spec-text, finalize-install and uninstall cases passed. Four cases are NOT RUN on the author's host. No CI lane calls proof_bep_round_three_conditions_closed, because it is not in the default walk (neither is the round-two walk). By rule 4 they stay open, so C1 makes the PR record a PASS or a filed issue for each of them. The --config-dir half is a residual on #2525, which crates/minimal/src/mint.rs links as the owner of the missing store kind.
Precedent. No departure. The ledger keeps only 400 characters of the baseline, so I cannot quote its conditions. I derived C1 again from the full diff. The compare does not touch the NOT RUN status that C1 and the residual cover.
Not checked. I did not run the e2e or compile, per the contract. Out of the design's scope: proof_bep_r3_pre_flip_udp_443_refused calls cargo nextest directly, not through a just recipe (AGENTS.md), and without --profile ci. That is for minimal-review.
Conditions
- C1: In the PR body
## Proof, give one line for each ofbep_r3_pre_flip_udp_443_refused,bep_r3_minted_id_checked_without_proxy,bep_r3_stranded_box_frees_client_keyandbep_r3_widened_store_rule_without_restart. Each line gives the case's PASS line from a lane that meets its gate, or the URL of a filed issue that owns that run. The three proxy cases need macOS with gvproxy and a GitHub sign-in. The pre-flip case needs native Linux with passwordless sudo and nft. The default walk inscripts/session-e2e.shand the CI lanes do not callproof_bep_round_three_conditions_closed. So no other step runs these legs, and NOT RUN is not a pass.
Ruled at b3e7c41 against gominimal/arch@109541a48c31 by claude-opus-5-5; arch_rulings 487, job f97cf106-ce55-48dc-ab73-a2dfa6883dc5.