Repository navigation
PASS_WITH_CONDITIONS
Governs: Gatehouse §6.10 line 839 (un-enrolled sign-in lifecycle: logout deletes the item and every reference refuses at its next request. A login after a logout is a new instance that no earlier reference names. A box revocation is written at min session destroy and covers exactly that creation's values. Box ids are UUIDv7 and never return. The two incident levers: destroy, and logout, which keeps processes running and re-arms nothing on re-login). Line 823 (redemption step 2, box attribution MUST match the blob's sub, and revocation ≤60 s). Line 836 (min box audit reads the records whose subject is the box). The checkout 109541a4 has no arch-map.md, so I started from these lines, as the sibling BEP rulings did. No findings.json and no since.diff were staged. This is the first ruling on PR 2610.
Ruling: the change adds one e2e case, proof_bep_revoke_and_sign_out_end_to_end, to scripts/session-e2e.sh, the layer that the task names. It is registered in the whole-lane order after the logout case, in the dispatch, and in the usage text. Each step asserts a design line with a hard check. The case does not relax a gate (rule 3). The gate is E2E_BEP_LOGOUT=1 and then bep_live_gate, the same gate as bep_logout_refuses_every_reference_at_next_request. Both call not_run, so a whole-lane pass never hides the case. The new counters bep_e2e_refus
2E04
als and bep_e2e_admits read the same record fields (kind, decision, marker, upstream, identifier) as the existing bep_slice_jsonl_check. They count where that helper only tests for presence, and the 'one more refusal' checks need a count. The design names no marker strings. cross_box and github_sign_in_required come from spec 24 and the sibling cases. I checked by reading the code that BoxRedeemer::credential() in crates/bep/src/redeemer.rs returns None when metadata.instance != instance. The test reference_to_another_sign_in_instance_is_refused in crates/bep/src/forward.rs pairs that path with SIGN_IN_REQUIRED. So the expected marker after re-login agrees with the code. The one open point is rule 4: the leg ran NOT RUN on Linux, and the PR states that the macOS live evidence is still owed. C1 closes it with a transcript, or with a filed residual.
Not checked: the live run itself. It needs macOS, a live proxy and a person at the device flow, and this sandbox has none. I did not build or run anything.
Conditions
- C1: Run
E2E_BEP_LOGOUT=1 ./scripts/session-e2e.sh bep_revoke_and_sign_out_end_to_endon a macOS host with a live Box Egress Proxy and a GitHub sign-in. Post the transcript on PR #2610. It must show each step line and the finalRevoke and sign out OKline. If nobody can run it before the merge, file an issue that owns the live run and name it in the PR body as a residual. Until one of these exists, the leg is NOT RUN and stays open. Thegithub_sign_in_requiredmarker for a pre-logout reference after a new sign-in is also unconfirmed live until then.
Ruled at 1570de3 against gominimal/arch@109541a48c31 by claude-opus-5-5; arch_rulings 408, job 47611f61-6f1d-4b87-a5fa-64836f38f2a4.