Repository navigation
feat(bep): decide redemption as a pure function over host key, attribution and bounds - #2359
Conversation
Add redeem::decide over owned values, apart from the TLS shell. It refuses a value that does not decrypt under this host's key (BEP-019), a member without a mode or a recognised breadth (BEP-058), and a source that is not the named box or its host_ip cohort (BEP-020). A refusal names its first failing check as an audit marker. Add three Kani harnesses and expect them in scripts/kani.sh.
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
|
Approved: no findings at Nothing to do. Clobber: none, the files are new or appended. |
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The redemption decision conforms to Gatehouse §6.10. It refuses an undecryptable value, an unbounded member and a misattributed source, as lines 817, 823 and 827 require. The PR body declares shell work that this task leaves undone, but it links no issue. On the real path, Unsealed::from_open passes UnknownBreadth and ContextMismatch(BoxId) through, so those refusals do not get the unbounded_member and cross_box markers yet. File the issue and link it, as C1 says. Then the change can merge.
Ruled at fad5ba6 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
seal::open reports a missing or unknown breadth as UnknownBreadth, with no context. Map it to Unsealed::Unbounded, so decide refuses it with the unbounded_member marker on the real path. Cover it in the Kani harness.
|
/revise complete shell work found by arch review |
|
That Nothing to type again: the command gets a rocket when its round starts, or a refusal that names the reason. No round was counted for it yet. |
|
Round 1 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
redeem::decide refuses a value sealed to another host's key (undecryptable), a value sent from an own-address box other than the one it names or from a host_ip cohort the named box is not in (cross_box), and a member with no mode or no recognised breadth (unbounded_member). A member with an unknown breadth that seal::open rejects now also reaches decide and is refused with the unbounded_member marker. Notes from the agent: Revise round 1. Added Unsealed::Unbounded: seal::open returns UnknownBreadth without the value's context, so the reviewer's first option (Opened with None bounds) was not possible without a box id. BadMembers stays an error: it says the list does not hold exactly one member, which is not a bounds check of BEP-058. A header with no mode does not parse, so open reports it as Malformed before decryption, and from_open passes it through. The new test calls from_open on Err(UnknownBreadth) directly, because seal_plaintext is private to seal.rs, which is outside this task's layers. seal.rs already tests that open returns UnknownBreadth for such plaintexts. Deferred (lane: kani), not run: kani_redeem_refuses_undecryptable, kani_redeem_refuses_misattributed, kani_redeem_refuses_unbounded_member. The harnesses now also generate Unsealed::Unbounded. |
There was a problem hiding this comment.
arch-review: PASS · the full ruling
This head conforms to Gatehouse §6.10. The new commit maps OpenError::UnknownBreadth to Unsealed::Unbounded. decide then refuses it as unbounded_member. Line 817 requires this: a missing or unknown breadth is refused and never treated as unbounded. seal::open raises that error only after decryption, so the mapping is accurate. The earlier ruling on BEP-019, BEP-020 and placement stands. The Kani harnesses are still deferred to the advisory kani lane.
Ruled at b6d6218 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
seal::open reports a value from another own_ip box as ContextMismatch(BoxId), after it decrypts. Map it to Unsealed::OtherBox, so decide refuses it with the cross_box marker (no_live_box when the source resolves to no live box). Document how the shell sets named_box_in_cohort while every VM-hosted box shares one attachment.
|
Round 2 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
redeem::decide refuses a value sealed to another host's key as undecryptable, a value sent from another own_ip box as cross_box, and a member without a mode or a recognised breadth as unbounded_member. The refusals also hold on the real seal::open path, because from_open maps UnknownBreadth to Unbounded and ContextMismatch(BoxId) to OtherBox. Notes from the agent: This round adds Unsealed::OtherBox. from_open maps OpenError::ContextMismatch(BoundField::BoxId) to it. decide refuses it as cross_box, or as no_live_box when the source resolves to no live box. A new test, from_open_other_box_is_refused_as_cross_box, runs seal::open with a different bound box id. The Kani harness kani_redeem_refuses_misattributed covers OtherBox. The named_box_in_cohort doc now records the NET-132/NET-133 interim, where every VM-hosted box, own_ip included, arrives as HostIpCohort. I cannot file or edit issues, so the C1 issue needs a person to record these two items. A residual for the shell: seal::open needs an expected box id, but a HostIpCohort source names no box. The shell must take the box id from the value before it binds the open, and seal.rs exposes no API for that yet. Deferred to the kani lane, not run: kani_redeem_refuses_undecryptable, kani_redeem_refuses_misattributed, kani_redeem_refuses_unbounded_member. I did not run just clippy-strict. |
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The new OtherBox path conforms. It refuses as cross_box or no_live_box and never admits, as §6.10 step 2 requires. The interim comment on named_box_in_cohort is wider than the design. Section 6.10 line 827 and T28 limit the cohort interim to un-enrolled nodes, and they put the host shell in the cohort. Make the doc-comment edit in C1. No code change is necessary.
Ruled at 25ae5e7 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
An unsupported header is not a value sealed to another key, so from_open returns it unchanged. The docs now scope the shared-attachment interim to an un-enrolled node, name the host shell, and say how the shell opens a value from a cohort source. A test goes from open to an admission attributed to the cohort.
|
Round 3 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
In crates/bep/src/redeem.rs, decide refuses a value sealed to another host's key as undecryptable. It refuses a value sent from another own_ip box, or bound to another box id, as cross_box. It refuses a member with no mode or no recognised breadth as unbounded_member. The property tests and the from_open tests show each refusal and its audit marker. Notes from the agent: Revise round 3. This round: from_open returns OpenError::Unsupported unchanged and maps only NotOpenable to Undecryptable. The docs scope the shared-attachment interim to un-enrolled nodes and name the host shell. They also state how the shell opens a value from a cohort source: it binds the open to each live cohort box in turn. New tests: cohort_open_bound_to_named_box_is_admitted_as_cohort and from_open_unsupported_comes_back_unchanged. All 8 redeem tests pass (cargo nextest run -p bep redeem). Deferred to the kani lane, not run: kani_redeem_refuses_undecryptable, kani_redeem_refuses_misattributed, kani_redeem_refuses_unbounded_member. A header-peek call in seal.rs would let the shell open a cohort value once, but seal.rs is outside this task's layers. The C1 issue entries that minimal-arch asked for need a person. I have no issue access. |
There was a problem hiding this comment.
minimal-review — approval withheld
Verdict COMMENT — APPROVE withheld: 7 unresolved threads — minimal-foundry[bot] crates/bep/src/redeem.rs:106, minimal-arch[bot] crates/bep/src/redeem.rs:105, minimal-arch[bot] crates/bep/src/redeem.rs:156, minimal-foundry[bot] crates/bep/src/redeem.rs, minimal-arch[bot] crates/bep/src/redeem.rs, …. No findings.
Panel: 3 of 3 personas ran (correctness, security, supply-chain).
There was a problem hiding this comment.
arch-review: PASS · the full ruling
This head conforms to Gatehouse §6.10. OpenError::Unsupported now goes back to the shell, so the undecryptable marker means only a value that this key cannot open (line 823, line 827). The cohort docs now state the enrolled rule, a live host_ip box (line 823). They also state the un-enrolled interim, which includes the host shell, with NET-132/133 as its flip condition (lines 839, 1745). The shell task must record cohort_attributed and the marker. The three Kani harnesses did not run, and the Kani lane must prove them.
Ruled at 54c8047 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
There was a problem hiding this comment.
Babysitter review of 54c8047a against the T4 plan block (#2260), its three plan test lines, and the arch rulings (last: 118306302506, PASS).
Matches the plan. bep::redeem::decide (crates/bep/src/redeem.rs lines 220 to 254) is a pure function over owned values with the box id as a type parameter. The check order is decrypt (BEP-019), bounds (BEP-058), attribution (BEP-020), and every path that cannot admit refuses with the first failing Check, whose marker() gives the audit word. Unsealed::from_open (lines 93 to 107) maps only NotOpenable to Undecryptable, UnknownBreadth to Unbounded, ContextMismatch(BoxId) to OtherBox, and returns every other OpenError unchanged, so Unsupported, Malformed and Expired go back to the shell. The three plan tests ran at exit 0 per the PR body; the off-host test uses real seal and open with two keys. The three Kani harnesses are present under cfg(kani) and scripts/kani.sh expects them; the plan marks those lines deferred to the kani lane, which is advisory.
Threads. Six of the seven open threads are addressed on this head, each verified at the line it names; I resolve them with the evidence. The seventh (redeem.rs line 244, the runtime's HIGH security finding on named_box_in_cohort) is disputed by the coder and accepted by the arch as the design's recorded interim residual (T28, Gatehouse §6.10 line 839). A security thread is the person's to close, so it stays open for them.
Findings. None that hold the merge. One note for the shell task: on the real path a missing mode is OpenError::Malformed from seal::open before any context exists, so Check::UnboundedMember for a missing mode is reachable only with hand-built values; the PR body says so, and the refusal is still fail-closed.
Not checked. I did not compile or run the tests. The lanes and the runtime's round comments did.
Generated by Claude Code
There was a problem hiding this comment.
minimal-review — approved
Verdict APPROVE — every review thread is resolved; @norrietaylor closed the last one. The review of 54c8047a6c85 withheld this approval on the threads open then. Posted as a comment: the App cannot approve its own pull request; the check and the label carry it.
There was a problem hiding this comment.
Babysitter approval of 54c8047 for the epic owner. Gate: arch PASS on this head, runtime review released its approval once the last thread was resolved, every lane aggregator green, no open threads, squash subject lints as Conventional Commits. The HIGH security thread was ruled a spec-recorded residual by the epic owner.
Generated by Claude Code
|
/revise Base merge only. main moved to f8431d0 (T2, #2363) and this branch now conflicts with it in Generated by Claude Code |
…emption-as-one-pure-function-over-host # Conflicts: # crates/bep/src/lib.rs
|
Round 4 of 10 on a /revise note, pushed as Resolved conflicts in:
Verify On the merged head, a v 10BC8 alue sealed to another host, sent from another own-address box, or missing its bounds is refused. The three property tests show it, and the bep crate now also carries the keys and publish modules from main. Notes from the agent: Base merge only. I resolved the conflict in crates/bep/src/lib.rs with the module lines keys, module, publish, redeem and seal, in alphabetical order, and committed the merge. I changed nothing else. redeem.rs and scripts/kani.sh are as they were. Git merged scripts/kani.sh with no conflict, and main adds no Kani harness to bep, so |
There was a problem hiding this comment.
arch-review: PASS · the full ruling
The new head merges main and does not change redeem.rs or scripts/kani.sh. The PASS on 54c8047 stands. Main adds OpenError::Key. Unsealed::from_open returns it unchanged, so the shell refuses. That is fail closed, as Gatehouse §6.10 line 817 and line 823 require. No condition.
Ruled at 5b7da0a against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
There was a problem hiding this comment.
Babysitter review of 5b7da0a: this head is 54c8047 plus one merge of origin/main (f8431d0). The compare against 54c8047 touches only crates/bep/src/lib.rs, which now lists keys, module, publish, redeem and seal once each; redeem.rs and scripts/kani.sh are unchanged. My review 5577821368 of 54c8047 and the epic owner's ruling on the cohort thread stand; no new finding.
Generated by Claude Code
There was a problem hiding this comment.
arch-review: PASS · the full ruling
This head is a merge of main into the branch. It does not change redeem.rs or scripts/kani.sh. The only change to a PR file is the pub mod audit; line from #2361 in lib.rs. The PASS on 5b7da0ab against Gatehouse §6.10 lines 817, 823 and 827 stands for this head.
Ruled at 7677744 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
There was a problem hiding this comment.
Own review carried to 7677744. This head is the person's merge of main (767c59f, T13) into the branch: compare 5b7da0ab...76777440 lists exactly the 17 files that main changed between f8431d0 and 767c59f, and nothing of the branch's own. The review of 54c8047 (approved) and the carries on 5b7da0a stand. minimal-arch ruled PASS on this head (check run 118442556422). license/cla is success on this head. Gate waits on the runtime review and the lanes.
Generated by Claude Code
There was a problem hiding this comment.
Approving for merge: T4 on the person's merge-only head 7677744 (arch PASS 118442556422, license/cla success). Gate passes on 7677744 (arch PASS, review concluded with no open threads, lanes green, squash subject lint-clean).
Generated by Claude Code
T4 — Decide redemption as one pure function over host key, attribution and member bounds
slice: S0
kind: task
covers: BEP-019, BEP-020, BEP-058
size: L
est: 300 code, 360 tests
executor: agent
difficulty: needs care
model: strongest
diagnostics: every refusal names its first failing check in the audit record's marker, which
min box audit <box>showsobservability: the connection span and the audit marker name a refusal's first failing check
layers:
- decide:
- crates/bep/src/redeem.rs (new): the pure decision over owned values, apart from the TLS shell; the BEP-019, BEP-020 and BEP-058 checks
- crates/bep/src/lib.rs: module line
- scripts/kani.sh: expects the bep crate's harnesses
test: cargo nextest run -p bep prop_off_host_sealed_value_is_refused
test: cargo nextest run -p bep prop_cross_box_sealed_value_is_refused
test: cargo nextest run -p bep prop_member_without_bounds_is_refused
test (deferred: kani): cargo nextest run -p bep kani_redeem_refuses_undecryptable
test (deferred: kani): cargo nextest run -p bep kani_redeem_refuses_misattributed
test (deferred: kani): cargo nextest run -p bep kani_redeem_refuses_unbounded_member
produces:
- crates/bep/src/redeem.rs
consumes:
- crates/bep/src/seal.rs
proof: A value sealed to another host, sent from another own-address box, or missing its bounds is refused.
depends on:
- blocked by #2258
Proof
In crates/bep/src/redeem.rs, bep::redeem::decide refuses a value sealed to another host's key (Check::Undecryptable), a value sent from an own_ip box other than the one it names or from no live box (Check::CrossBox, Check::NoLiveBox), and a member with no mode or no recognised breadth (Check::UnboundedMember). Each refusal names its first failing check, and Check::marker gives the word for the audit record. The three property tests show this, and the off-host test uses real seal and open with two keys.
Notes from the agent: Deferred (lane: kani): kani_redeem_refuses_undecryptable, kani_redeem_refuses_misattributed and kani_redeem_refuses_unbounded_member are #[kani::proof] harnesses in redeem.rs under cfg(kani). They are not nextest tests, so the deferred
cargo nextest runlines select nothing. scripts/kani.sh now runsexpect bep 3. I did not run Kani. Design: the decide function is generic over the box id type, so Kani uses u8 ids. The check order is decrypt (BEP-019), then bounds (BEP-058), then attribution (BEP-020). A host_ip cohort source is admitted only when the named box is a live host_ip box of this host, and the admission says Attributed::Cohort for the cohort_attributed audit field. Unsealed::from_open maps seal::open's NotOpenable and Unsupported to Undecryptable and returns every other OpenError unchanged. Gap for the shell task: seal::open refuses a missing or unknown breadth as OpenError::UnknownBreadth, and a header with no mode as OpenError::Malformed, before it returns a context. So on the real path those cases do not reach decide as Bounds with None. The shell must map UnknownBreadth to the unbounded_member marker, and a missing mode now surfaces as Malformed. The diagnostics and observability lines (the marker inmin box auditoutput and on the connection span) need the shell and the audit writer, which are not in this task's layers. This task gives only Check::marker.Tests
cargo nextest run -p bep prop_off_host_sealed_value_is_refusedcargo nextest run -p bep prop_cross_box_sealed_value_is_refusedcargo nextest run -p bep prop_member_without_bounds_is_refusedVerify
min task run agent-verifypassed ([tasks.verify]).Deferred
The plan marked these test lines deferred: the executor lacks the lane, so nothing here ran them and they still owe evidence.
cargo nextest run -p bep kani_redeem_refuses_undecryptablecargo nextest run -p bep kani_redeem_refuses_misattributedcargo nextest run -p bep kani_redeem_refuses_unbounded_memberCloses #2260