From b1a13c4e35973af87efb03bc4538c0cd629cc1ea Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sat, 17 Oct 2026 16:08:58 -0400 Subject: [PATCH] joule-code-joulecontract: an obligation nothing checked is not discharged MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- .../joule-code-joulecontract/src/lib.rs | 301 ++++++++++++++++-- 1 file changed, 275 insertions(+), 26 deletions(-) diff --git a/joule-code/joule-code-rs/crates/joule-code-joulecontract/src/lib.rs b/joule-code/joule-code-rs/crates/joule-code-joulecontract/src/lib.rs index 9d838924b..e9232e2dc 100644 --- a/joule-code/joule-code-rs/crates/joule-code-joulecontract/src/lib.rs +++ b/joule-code/joule-code-rs/crates/joule-code-joulecontract/src/lib.rs @@ -18,7 +18,7 @@ //! composing them to JR-3+ with sealed evidence, a key log, and anchored //! intervals is the deployment's verifier-of-record work, not this crate's. -use joule_code_cargo::CodingOp; +use joule_code_cargo::{CodingOp, SignedOp}; use joule_code_receipt::{Energy, Provenance}; use joule_code_schema::ContentId; use joulecontract_receipt::{ @@ -95,6 +95,77 @@ pub enum BindingError { OutOfFrame { path: String }, #[error("contract addressing failed: {0}")] Address(String), + /// The op's own id could not be derived, so no receipt can name the + /// operation it is about. + #[error("op id could not be derived: {0}")] + OpId(String), +} + +/// Decide one declared obligation against what this binder actually holds. +/// +/// Every arm either evaluates the obligation or reports it `Undischarged` +/// with the reason it was not evaluated. **There is no default `Closed`.** +/// `Closed` is JouleContract's positive "this obligation was discharged", and +/// it used to be the fall-through for every Pre, Post and Inv obligation — +/// signed, attributed to a named `Deterministic` tier, with nothing having +/// evaluated them. The worst case was the Post obligation below: it states +/// the same property as the frame obligation, so a single receipt could carry +/// `Frame = Undischarged { "out-of-frame edit: deploy/secrets.env" }` and +/// `Post = Closed` for "every edit applied within the declared frame" — one +/// signature asserting both that an edit escaped the frame and that every +/// edit stayed inside it. +fn discharge_for( + signed: &SignedOp, + prior: &ContentId, + frame_result: &DischargeResult, + ob: &joulecontract_schema::Obligation, +) -> DischargeResult { + use joulecontract_schema::ObligationKind as Kind; + match (&ob.kind, ob.text.as_str()) { + // Decided by `frame_check`. + (Kind::Frame, _) => frame_result.clone(), + + // The same property as the frame obligation, so it carries the same + // evidence rather than a second, contradictory verdict. + (Kind::Post, "every edit applied within the declared frame") => frame_result.clone(), + + // The contract names the tree the op must build on. `SignedOp::verify` + // below binds the op to `prior`; this checks the *contract* was + // written for that same prior, so the two cannot disagree silently. + (Kind::Pre, text) if text.starts_with("op builds on prior tree ") => { + let expected = format!("op builds on prior tree {}", prior.0); + if text == expected { + DischargeResult::Closed + } else { + DischargeResult::Undischarged { + reason: format!("contract declares `{text}`, this receipt states prior {}", prior.0), + } + } + } + + // 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. + (Kind::Inv, "op signature verifies over op_id ‖ prior") => match signed.verify(prior) { + Ok(()) => DischargeResult::Closed, + Err(e) => DischargeResult::Undischarged { + reason: format!("signature does not verify over op_id ‖ prior: {e}"), + }, + }, + + // Exactly what `CodingOp::validate` decides (SPEC §2: known alg, + // non-empty edits, ascending `(path, start)`, no overlap). + (Kind::Inv, "edits are ordered and pairwise disjoint") => match signed.op.validate() { + Ok(()) => DischargeResult::Closed, + Err(e) => DischargeResult::Undischarged { reason: e.to_string() }, + }, + + // An obligation this binder does not recognise. A caller may declare + // any prose it likes; none of it is discharged by being written down. + (_, text) => DischargeResult::Undischarged { + reason: format!("not evaluated by this binder: {text}"), + }, + } } /// Check every edit path against the contract's frame. A path is in-frame @@ -147,13 +218,33 @@ impl Binder { /// set, not analyzed from the artifact. An out-of-frame op still gets a /// receipt: the frame serializes `undischarged` with the offending path, /// because a breach recorded honestly beats a breach driven underground. + /// Seal a receipt for one signed op against a contract. + /// + /// Takes the **signed** op and the `prior` the verifier believes current, + /// because two of the contract's obligations are statements about exactly + /// those: the signature over `op_id ‖ prior`, and the tree the op builds + /// on. With an unsigned `CodingOp` and a caller-supplied `op_id` neither + /// could be decided — and both were nonetheless sealed as discharged. + /// + /// The op id is **derived** from the op rather than supplied, so + /// `transition` always names the operation whose obligations were checked; + /// a caller-supplied id was trusted and never re-derived, so a receipt + /// could carry one op's frame verdict under another op's id. + /// + /// # Errors + /// [`BindingError::OpId`] if the op's id cannot be derived (it is + /// structurally invalid), or [`BindingError::Address`] if the contract + /// cannot be addressed. A failing *obligation* is not an error: it is + /// recorded as `Undischarged` on the receipt, which is the point. pub fn receipt_for_op( &self, contract: &Contract, - op: &CodingOp, - op_id: &ContentId, + signed: &SignedOp, + prior: &ContentId, energy: &Energy, ) -> Result { + let op: &CodingOp = &signed.op; + let op_id = op.op_id().map_err(|e| BindingError::OpId(e.to_string()))?; let frame_result = match frame_check(contract, op) { Ok(()) => DischargeResult::Closed, Err(BindingError::OutOfFrame { path }) => DischargeResult::Undischarged { @@ -172,16 +263,13 @@ impl Binder { .into_iter() .map(|ob| { let is_frame = ob.kind == joulecontract_schema::ObligationKind::Frame; + let result = discharge_for(signed, prior, &frame_result, &ob); DischargeEntry { obligation: ob, tier: binding_tier.clone(), tier_class: TierClass::Deterministic, tier_operator_keys: self.tier_operator_keys.clone(), - result: if is_frame { - frame_result.clone() - } else { - DischargeResult::Closed - }, + result, mode: is_frame.then_some(FrameMode::Observed), qualification: Some(self.qualification.clone()), verifier_keys: self.verifier_keys.clone(), @@ -197,7 +285,7 @@ impl Binder { contract: contract .content_address() .map_err(|e| BindingError::Address(e.to_string()))?, - transition: bridge_id(op_id), + transition: bridge_id(&op_id), generator: self.generator.clone(), discharge, execution: vec![ContentAddress::of_bytes( @@ -240,24 +328,44 @@ mod tests { ContentAddress::of_bytes(label.as_bytes()) } - fn op(paths: &[&str]) -> (CodingOp, ContentId) { + fn author_key() -> ed25519_dalek::SigningKey { + ed25519_dalek::SigningKey::from_bytes(&[42u8; 32]) + } + + /// The tree `contract()` declares its op must build on. + fn prior() -> ContentId { + ContentId::of_bytes(b"prior tree") + } + + /// A real signed op. `author` is the signing key's own verifying key, and + /// the edits are sorted into canonical `(path, start)` order, because + /// `op_id` runs `validate` and `sign` runs `op_id` — an op that is not + /// canonical has no id and therefore no signature. + /// + /// This replaces a fixture that set `author: [7u8; 32]` (not a key) and + /// returned `ContentId::of_bytes(b"the op canonical bytes")` as the id — + /// a constant unrelated to the op, which is what let the untrusted + /// `op_id` parameter go unnoticed. + fn op(paths: &[&str]) -> SignedOp { + let key = author_key(); + let mut sorted: Vec<&&str> = paths.iter().collect(); + sorted.sort(); let op = CodingOp { alg: 0x01, - prior: ContentId::of_bytes(b"prior tree"), - edits: paths - .iter() + prior: prior(), + edits: sorted + .into_iter() .map(|p| Edit { - path: p.to_string(), + path: (*p).to_string(), anchor: Anchor::ByteRange { start: 0, end: 4 }, replacement: b"new!".to_vec(), }) .collect(), - author: [7u8; 32], + author: key.verifying_key().to_bytes(), intent: "rename the settlement index field".into(), tier: Tier::L1, }; - let id = ContentId::of_bytes(b"the op canonical bytes"); - (op, id) + op.sign(&key).expect("a canonical op signs") } fn binder() -> Binder { @@ -323,13 +431,13 @@ mod tests { #[test] fn in_frame_op_discharges_and_validates_to_jr2() { let c = contract(&["src/", "Cargo.toml"]); - let (op, id) = op(&["src/lib.rs", "Cargo.toml"]); + let signed = op(&["src/lib.rs", "Cargo.toml"]); let energy = Energy { measured_uj: Some(1_200), estimated_uj: 1_000, provenance: Provenance::HwShunt, }; - let r = binder().receipt_for_op(&c, &op, &id, &energy).unwrap(); + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); let v = validate(&c, &r).unwrap(); assert_eq!(v.max_profile.rigor, Rigor::Jr2); assert_eq!(v.max_profile.energy, EnergyClass::Metered); @@ -341,9 +449,9 @@ mod tests { #[test] fn out_of_frame_edit_is_caught_at_the_boundary() { let c = contract(&["src/"]); - let (op, id) = op(&["src/lib.rs", "deploy/secrets.env"]); + let signed = op(&["src/lib.rs", "deploy/secrets.env"]); assert_eq!( - frame_check(&c, &op), + frame_check(&c, &signed.op), Err(BindingError::OutOfFrame { path: "deploy/secrets.env".into() }) @@ -355,7 +463,7 @@ mod tests { estimated_uj: 900, provenance: Provenance::ModelBased, }; - let r = binder().receipt_for_op(&c, &op, &id, &energy).unwrap(); + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); let v = validate(&c, &r).unwrap(); assert!(v.demotions.iter().any(|d| matches!( d, @@ -364,12 +472,153 @@ mod tests { assert_eq!(v.max_profile.rigor, Rigor::Jr1, "undischarged frame caps rigor"); } + /// The contradiction this fix removes. The Post obligation states the same + /// property as the Frame obligation, so one receipt cannot carry + /// "an edit escaped the frame" and "every edit stayed inside it" at once. + #[test] + fn the_post_obligation_carries_the_frame_verdict() { + let c = contract(&["src/"]); + let signed = op(&["src/lib.rs", "deploy/secrets.env"]); + let energy = Energy { + measured_uj: Some(900), + estimated_uj: 900, + provenance: Provenance::HwShunt, + }; + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + + let post = r + .discharge + .iter() + .find(|d| d.obligation.text == "every edit applied within the declared frame") + .expect("the contract declares it"); + let frame = r + .discharge + .iter() + .find(|d| d.obligation.kind == joulecontract_schema::ObligationKind::Frame) + .expect("the contract declares it"); + + assert_eq!(post.result, frame.result, "same property, same verdict"); + assert!( + matches!(&post.result, DischargeResult::Undischarged { reason } if reason.contains("deploy/secrets.env")), + "got {:?}", + post.result + ); + } + + /// The signature obligation is decided, not assumed. A tampered signature + /// leaves it undischarged instead of sealing "verifies" over bytes that + /// do not. + #[test] + fn the_signature_obligation_is_decided_not_assumed() { + let c = contract(&["src/"]); + let mut signed = op(&["src/lib.rs"]); + let energy = Energy { + measured_uj: Some(900), + estimated_uj: 900, + provenance: Provenance::HwShunt, + }; + + // Intact: the obligation closes on a real check. + let good = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + let sig_of = |r: &Receipt| { + r.discharge + .iter() + .find(|d| d.obligation.text == "op signature verifies over op_id \u{2016} prior") + .map(|d| d.result.clone()) + .expect("the contract declares it") + }; + assert_eq!(sig_of(&good), DischargeResult::Closed); + + // Tampered: undischarged, with the reason on the record. + *signed.sig.last_mut().expect("signature bytes") ^= 1; + let bad = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + assert!( + matches!(sig_of(&bad), DischargeResult::Undischarged { .. }), + "got {:?}", + sig_of(&bad) + ); + } + + /// A caller may declare any prose it likes; none of it is discharged by + /// being written down. The fall-through used to be `Closed`. + #[test] + fn an_unrecognised_obligation_is_never_closed() { + let mut c = contract(&["src/"]); + c.post.push("the author was well rested".into()); + let signed = op(&["src/lib.rs"]); + let energy = Energy { + measured_uj: Some(900), + estimated_uj: 900, + provenance: Provenance::HwShunt, + }; + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + + let entry = r + .discharge + .iter() + .find(|d| d.obligation.text == "the author was well rested") + .expect("declared"); + assert!( + matches!(&entry.result, DischargeResult::Undischarged { reason } if reason.contains("not evaluated")), + "got {:?}", + entry.result + ); + } + + /// The receipt names the operation whose obligations it checked: the id is + /// derived from the op, not supplied beside it. + #[test] + fn the_transition_names_the_op_it_checked() { + let c = contract(&["src/"]); + let signed = op(&["src/lib.rs"]); + let energy = Energy { + measured_uj: Some(900), + estimated_uj: 900, + provenance: Provenance::HwShunt, + }; + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + assert_eq!(r.transition, bridge_id(&signed.op.op_id().unwrap())); + } + + /// A contract written for a different tree does not have its precondition + /// discharged by a receipt that states another prior. + #[test] + fn a_contract_for_a_different_prior_leaves_the_precondition_open() { + let c = contract_for_op( + "rename the settlement index field", + &ContentId::of_bytes(b"some other tree"), + &["src/".to_string()], + 0.01, + key("enb"), + None, + Rigor::Jr2, + ); + let signed = op(&["src/lib.rs"]); + let energy = Energy { + measured_uj: Some(900), + estimated_uj: 900, + provenance: Provenance::HwShunt, + }; + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); + + let pre = r + .discharge + .iter() + .find(|d| d.obligation.kind == joulecontract_schema::ObligationKind::Pre) + .expect("declared"); + assert!( + matches!(&pre.result, DischargeResult::Undischarged { .. }), + "got {:?}", + pre.result + ); + } + #[test] fn estimator_energy_is_unaccounted_never_promoted() { let c = contract(&["src/"]); - let (op, id) = op(&["src/lib.rs"]); + let signed = op(&["src/lib.rs"]); let energy = Energy::from_tokens(100, 10); - let r = binder().receipt_for_op(&c, &op, &id, &energy).unwrap(); + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); assert_eq!(r.provenance, EnergyClass::Unaccounted); assert!(r.meter.is_none(), "an estimator figure never carries a meter binding"); let v = validate(&c, &r).unwrap(); @@ -381,13 +630,13 @@ mod tests { // Receipt-time enforcement (JouleContract §5.3): the deviation is on // the record as a negative residual; amend-or-fix is the resolution. let c = contract(&["src/"]); - let (op, id) = op(&["src/lib.rs"]); + let signed = op(&["src/lib.rs"]); let energy = Energy { measured_uj: Some(50_000), // 0.05 J against a 0.01 J ceiling estimated_uj: 50_000, provenance: Provenance::HwShunt, }; - let r = binder().receipt_for_op(&c, &op, &id, &energy).unwrap(); + let r = binder().receipt_for_op(&c, &signed, &prior(), &energy).unwrap(); assert!(r.residual() < 0.0); assert!(validate(&c, &r).is_ok(), "the system keeps running; the record decides"); } -- 2.54.0 (Apple Git-157)