Repository navigation
fix(bep): refuse an unknown breadth as unbounded_member
PASS
Governs: Gatehouse §6.10 (specs/authn-authz/gatehouse-spec.md). Sealed secret (line 817): breadth is required and fail-closed, and mode is audit-only at redemption. Redemption (line 823): step 2 box attribution must match the blob's sub. A host_ip cohort source admits only a live host_ip box of that node, and a cohort-sourced redemption carries cohort_attributed. The BEP refuses a malformed blob. Attribution layering (line 825) and Theft gradient (line 827): a blob decrypts only under its own key.
Ruling: this is a re-review of b6d62189 against the baseline on fad5ba62. The compare changes only crates/bep/src/redeem.rs. It adds Unsealed::Unbounded, maps OpenError::UnknownBreadth to it in from_open, and refuses it in decide as Check::UnboundedMember. It also adds a unit test and extends the Kani generator and kani_redeem_refuses_unbounded_member to the new variant. I read seal::open. It raises UnknownBreadth only after AEAD decryption, binding and expiry, so the Unbounded fact is true: the value decrypted. The earlier head returned UnknownBreadth to the shell unmapped. That gap was the open item on the baseline. It is now closed in the right owner, the pure decision module, as line 817 requires. A missing mode is still OpenError::Malformed before decryption. The shell refuses it, and line 823 lists a malformed blob as a refusal, so the path fails closed. Nothing else in the compare touches BEP-019, BEP-020, the check order or placement, so the baseline stands for those.
Departure from precedent: the baseline was PASS_WITH_CONDITIONS. This head is PASS because the compare resolves the BEP-058 real-path item against line 817, and I find no remaining deviation. The audit marker in min box audit and on the connection span belongs to the shell and the audit writer (line 836). Those are later tasks of this spec and are outside this task's layers:. This change owes Check::marker only, and it supplies it.
Not checked: I did not build or run anything. The three Kani harnesses are deferred to the kani lane, which is advisory (ci-kani-success). I read them and they match the cited rules, but nothing ran them. scripts/kani.sh now expects bep 3, and that count matches the three #[kani::proof] harnesses in redeem.rs. The nextest verify: lines for BEP-019, BEP-020 and BEP-058 report exit 0 in the PR body. I took that from the body and did not reproduce it.
Ruled at b6d6218 against gominimal/arch@3dab1097cda1 by claude-opus-5-5; arch_rulings 23, job 53b715b4-43ef-4680-b383-25c4617fb52a.