| Filename | Latest commit message | Latest commit date |
|---|---|---|
b1a13c4e35
Some checks failed
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Successful in 2m34s
repository checks / lockfiles, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 2m21s
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 19s
standards workspaces build + test / macOS energy backends (pull_request) Failing after 3s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 1m33s
`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]>
|
||
| .. | ||
| crates | ||
| Cargo.lock | ||
| Cargo.toml | ||