joule-code-joulecontract: an obligation nothing checked is not discharged #307
Loading…
Reference in a new issue
No description provided.
Delete branch "fix/joule-code-joulecontract-no-fabricated-discharge"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The defect
receipt_for_opcomputed one obligation and sealed the rest as discharged:Closedis JouleContract's positive "this obligation was discharged". Every Pre, Post and Inv obligationcontract_for_opdeclares was sealed with it — attributed to a namedTierClass::Deterministictier, carrying the binder's verifier keys, qualification and engagement, and signed — although no code evaluated any of them. The crate doc presents this binding as "not an analogy; the objects line up field by field".The sharpest case is a self-contradicting receipt
The Post obligation states the same property as the Frame obligation. The crate's own test
out_of_frame_edit_is_caught_at_the_boundaryproduced a receipt carrying, in onedischargevector:One signature asserting both that an edit escaped the frame and that every edit stayed inside it.
validatereported only the frame demotion, so a relying party reading the Post entry saw a passed check that was never run.The fix
Every obligation
contract_for_opwrites is now decided — and all four were decidable from primitives that already existed:SignedOp::verify, which recomputesop_id, rebuildsop_id ‖ prior, checks againstop.author, and rejects replay onto a different baseCodingOp::validate(SPEC §2: known alg, non-empty, ascending(path, start), no overlap)Undischarged { "not evaluated by this binder: …" }There is no default
Closed. That fall-through was the defect.Two signature changes
receipt_for_ophas no callers outside its own tests, so both are free:&SignedOpand thepriorthe verifier believes current, because two obligations are statements about exactly those. With an unsignedCodingOpneither could be decided — and both were sealed as discharged anyway.op_idwas trusted and never re-derived, sotransition: bridge_id(op_id)could name a different operation than the one whose frame was checked.The fixture told the same story
It set
author: [7u8; 32]— not a key — and returnedContentId::of_bytes(b"the op canonical bytes")as the op id, a constant unrelated to the op. That is what let the untrustedop_idparameter go unnoticed. It now signs with a real key and sorts the edits into canonical order, becauseop_idrunsvalidateandsignrunsop_id: an op that is not canonical has no id and therefore no signature.Nothing was traded away
in_frame_op_discharges_and_validates_to_jr2passes unchanged, still assertingRigor::Jr2. An honest check of a valid, in-frame, signed op closes all four obligations — so the receipt stopped fabricating discharges without losing any rigor it was entitled to.Tests
the_post_obligation_carries_the_frame_verdict— the contradiction, pinned:post.result == frame.result, and both namedeploy/secrets.env.the_signature_obligation_is_decided_not_assumed— intact signature closes it; one flipped byte leaves it undischarged.an_unrecognised_obligation_is_never_closed— a caller pushes "the author was well rested"; it comes back undischarged.the_transition_names_the_op_it_checked—transition == bridge_id(op.op_id()).a_contract_for_a_different_prior_leaves_the_precondition_open.Falsification
Closedfall-through (the original defect)In every run the five pre-existing tests kept passing, so the mutations are isolated to the behaviour under test.
Verification
cargo test -p joule-code-joulecontract— 10 passed, 0 failedcargo check --workspace --all-targets(joule-code-rs) — exit 0cargo test --workspace(joule-code-rs) — exit 0, 0 failed suites, 44 passing suitesThe crate is consumed only by
joule-code-releaseandjoule-code-remediate, both inside this workspace, and neither callsreceipt_for_op— so the gate above covers the whole blast radius.🤖 Generated with Claude Code
`receipt_for_op` computed one obligation and sealed the rest as discharged: result: if is_frame { frame_result.clone() } else { DischargeResult::Closed }, `Closed` is JouleContract's positive "this obligation was discharged". Every Pre, Post and Inv obligation `contract_for_op` declares was sealed with it — attributed to a named `TierClass::Deterministic` tier, carrying the binder's verifier keys, qualification and engagement, and signed — although no code evaluated any of them. The crate doc presents this binding as "not an analogy; the objects line up field by field". The sharpest case is the Post obligation, because it states the *same property* as the Frame obligation. The crate's own test `out_of_frame_edit_is_caught_at_the_boundary` produced a receipt carrying, in one `discharge` vector: Frame: Undischarged { reason: "out-of-frame edit: deploy/secrets.env" } Post ("every edit applied within the declared frame"): Closed One signature asserting both that an edit escaped the frame and that every edit stayed inside it. `validate` reported only the frame demotion, so a relying party reading the Post entry saw a passed check that was never run. Every obligation `contract_for_op` writes is now decided, and all four are decidable from primitives that already existed: - **Post** "every edit applied within the declared frame" carries the frame verdict — same property, same evidence. - **Inv** "op signature verifies over op_id ‖ prior" is exactly what `SignedOp::verify` decides: it recomputes `op_id`, rebuilds `op_id ‖ prior`, checks the signature against `op.author`, and rejects replay onto a different base. - **Inv** "edits are ordered and pairwise disjoint" is exactly what `CodingOp::validate` decides (SPEC §2). - **Pre** "op builds on prior tree X" checks the contract was written for the prior this receipt states, so the contract and the receipt cannot disagree silently. - Anything else a caller declared is `Undischarged { "not evaluated by this binder: …" }`. **There is no default `Closed`** — that fall-through was the defect. Two signature changes make the undecidable decidable, and `receipt_for_op` has no callers outside its own tests: - It takes `&SignedOp` and the `prior` the verifier believes current, because two obligations are statements about exactly those. With an unsigned `CodingOp` neither could be decided — and both were sealed as discharged anyway. - The op id is **derived** from the op instead of supplied. A caller-supplied `op_id` was trusted and never re-derived, so `transition: bridge_id(op_id)` could name a different operation than the one whose frame was checked. The fixture told the same story: it set `author: [7u8; 32]`, which is not a key, and returned `ContentId::of_bytes(b"the op canonical bytes")` as the op id — a constant unrelated to the op. It now signs with a real key and sorts the edits into canonical order, because `op_id` runs `validate` and `sign` runs `op_id`. `in_frame_op_discharges_and_validates_to_jr2` still passes unchanged: an honest check of a valid in-frame signed op closes all four obligations, so nothing was traded away to stop fabricating them. Co-Authored-By: Claude Opus 5 <[email protected]>