Repository navigation
Merge remote-tracking branch 'origin/main' into agent/2277-record-a-r…
CONDITIONS
Governs: Gatehouse §6.10 line 839 (v1.24, Identity, attribution, and revocation).
3FC1
A box revocation is written when a live box is destroyed, and this is the mode's one revocation event. It names an id that never returns and covers exactly that creation's values. The records live in the helper's hash-chained log, are restored at start, and are consulted at step 2 before any resolution. The same line requires that the host-side creator withdraws a box's attachment at its end. Also §6.10 line 836 and architecture.md line 501, which say the local log holds the destroyed box's standing revocation record. The checkout (109541a4) has no arch-map.md, so I started from §6.10, as the earlier BEP rulings did. No findings.json and no since.diff were staged. This is the first ruling on this PR. pr.diff equals git diff 17ce321a dff33084.
Ruling: the shape conforms. minvmd, outside the VM, sends revoke_box then forget_box from withdraw_client_box. That is the creator's destroy path, and the attachment is retired first under the row lock. The stop and detach-expiry path (withdraw_where) sends none. The proxy is the log's only writer, and the control socket shares the decisions' Arc<Mutex<AuditLog>>. A revocation is in force before its record is written, and decide refuses it before the keychain is read. Three conditions remain. C1: both e2e legs are NOT RUN, and BEP-043 has no other proof (rubric rule 4). C2: redeemer.rs still states the interim this PR flips (rule 2). C3: the BEP-071 property proves revoke::covers and in_force_for, which the redeemer never calls (rule 3).
Observations, not conditions:
- The creator's rollbacks in
crates/minimal/src/cmd/boxes/create.rs(an abandoned activation, a skewed daemon, a failed upload) also callwithdraw_box_row. So with this PR they send a revocation and, with the proxy down, log the "the destroy completed" warning. I read an abandoned creation's row as the remove of a live box, so this is not a deviation. The warning text is wrong for that path. AuditWriter::writereturns no result. If the append fails, the revocation is in force in memory andrevoke_boxstill repliesok, but T33 cannot restore it. The proxy logs an error, and the withdrawn attachment refuses the values anyway (the BEP-043 sub-requirement).min box auditshows arevocationrecord withdecision: refuseandresource/permissionmodule_unmapped, and amintrecord withadmitand an emptyupstream. The design gives the field set for admit/refuse events only, so it is silent on these values.- The e2e refusal case checks
cross_box, notrevoked. Attribution refuses first, as the PR notes. BEP-043's two clauses (the record, then the refusal) are still both checked.
Not checked: I did not build or run anything. I did not check a destroy whose DestroySession takes more than DETACH_GRACE (45 s, for a slow on_destroy hook). In that case the drainer can withdraw the row first, and the creator's withdrawal then finds a dormant creation and sends no revocation. The attachment still refuses, but no record is written. The ledger keeps only 400 characters of each precedent, so I cite them for the governing line, not for their conditions.
Conditions
- C1: Run
./scripts/session-e2e.sh bep_destroyed_box_values_refused_within_60sand./scripts/session-e2e.sh bep_destroy_with_proxy_down_refuses_by_attachmenton the macOS lane (just e2eon the Apple Silicon runner, live proxy and GitHub sign-in). Record each as PASS in the PR's Tests table. Today both print NOT RUN, and BEP-043 has no other verify line. - C2:
crates/bep/src/redeemer.rs: rewrite the interim in theBoxRedeemer::newdoc comment (lines 107-113) and in the facts-gathering doc comment (lines 223-224). Today both say that nothing inbep servewrites a revocation until T20 (#2277). Make them say thatrevoke_boxon the control socket puts a revocation in force (crate::revoke::record). Make them say that the one interim left is the empty set at start until T33 (#2290) restores it, which matches thebep servewarning incrates/bep/src/main.rsline 945. This file is outside the task's layers. Edit it in this PR, because this PR is the flip those comments name. - C3:
crates/bep/src/redeemer.rslines 301-305: buildrevokedascrate::revoke::in_force_for(&set, &box_id)(cloned into aVec<String>), in place of a clone of the whole set. Thenredeem::decidereads only the revocations that cover this value, andprop_revocation_covers_exactly_its_boxproves the filter the redemption path uses. KeepCheck::Revokedand its order indecideunchanged.
Ruled at dff3308 against gominimal/arch@109541a48c31 by claude-opus-5-5; arch_rulings 266, job 672605cf-440c-476e-8fa7-55280747843a.