From 72aec523d2dc9a6c93ea6838773a322a2e378860 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 25 Aug 2026 17:17:29 -0400 Subject: [PATCH 01/11] jcp-action-receipt: AR-1, the composition envelope MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements §5 step 1 of the Action Receipt blueprint: the envelope spec plus a signed conformance vector pack. ## The gap this closes Three receipt families ship today, each holding one quarter of what an audit asks for, and none binds to the others: jcp-receipt authority grant chain, verdict, budget drawn sandbox-proof environment attestation, isolation tier, substrate JCR-1 work input hash, measured joules, provenance (nothing) effect what changed, and whether it can be undone So no single artifact answers "under what authority did this agent do that, where did it run, what did it cost, and what did it change?" The encoding is implemented six independent times across the tree — evidence the *encoding* is portable, and that the *composition* was never specified. Two families already gesture at the chain (the proof cell carries a receipt_id, the authority receipt a payload_hash). The intent was there; the binding was not. ## Envelope, not replacement AR-1 binds the three by content-id and supplies the fourth. Each family keeps its own canonical encoding and signer; the envelope reaches into them and never the reverse, so every existing verifier keeps working unchanged. No new cryptography: canonical det-CBOR and the tagged COSE_Sign1 envelope are reused verbatim from jcr1. The only primitive added is a canonical *decoder* — jcr1 ships an encoder and none was needed downstream until now, and a verifier needs to read a signed core back. It is the exact inverse of the encoder's subset (maps, arrays, text, unsigned ints; no floats, bools, nulls, tags), refuses non-canonical length encodings and trailing bytes, and is pinned to the encoder by a round-trip property test. Taking a CBOR dependency instead would have contradicted the crate's own claim. ## Refusal over record-keeping A format that merely records claims is a log. Three shapes are refused at verification, re-derived from the wire projection rather than a caller-supplied struct, so a hand-forged receipt that signs correctly is still rejected: 1. effect `irreversible` REQUIRES a plan receipt — binding the cascade's existing plan/commit split into the evidence. 2. egress `none` REQUIRES zero bytes — the claim is falsified by its own byte count. 3. egress `attested_enclave` REQUIRES a peer attestation. An unattested destination is `third_party` even when the operator believes it trustworthy. Trust is not an egress class. Two further invariants are normative: `grounding` is carried verbatim and never upgraded from software to hardware, and the three energy provenances never collapse into one number. ## Conformance pack 7 positive and 3 negative vectors under jcp/conformance/v1/, signed with a published fixture key so third parties can verify. The negatives are the substance: each carries a *genuine* signature and must still be refused, so an implementation that checks signatures and skips the structural rules passes the positives and fails the pack. That is precisely the failure mode the pack exists to catch. The emitter asserts both properties before writing, so an unverifiable vector cannot be published. tests/conformance.rs consumes the published JSON from disk — the same bytes a third party downloads — and checks that re-derived receipt ids and canonical cores match byte-for-byte. AR-1 does not solve effect revocation; nothing does in general. It makes the distinction machine-readable at the moment of action, which is the precondition for reasoning about it afterwards. 20 tests in the crate; jcp-rs workspace green at 258. Co-Authored-By: Claude Opus 4.8 (cherry picked from commit d3e1c2adda08762061d418190453c3b7603f0250) --- jcp/conformance/v1/action_receipt.json | 379 ++++++++++++ jcp/conformance/v1/action_receipt_meta.json | 9 + jcp/jcp-rs/Cargo.lock | 13 + jcp/jcp-rs/Cargo.toml | 2 + .../crates/jcp-action-receipt/Cargo.toml | 21 + .../jcp-action-receipt/docs/AR-1-spec.md | 208 +++++++ .../examples/emit_vectors.rs | 244 ++++++++ .../crates/jcp-action-receipt/src/decode.rs | 228 +++++++ .../crates/jcp-action-receipt/src/lib.rs | 564 ++++++++++++++++++ .../jcp-action-receipt/tests/conformance.rs | 113 ++++ 10 files changed, 1781 insertions(+) create mode 100644 jcp/conformance/v1/action_receipt.json create mode 100644 jcp/conformance/v1/action_receipt_meta.json create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs diff --git a/jcp/conformance/v1/action_receipt.json b/jcp/conformance/v1/action_receipt.json new file mode 100644 index 000000000..b030cdc23 --- /dev/null +++ b/jcp/conformance/v1/action_receipt.json @@ -0,0 +1,379 @@ +{ + "vectors": [ + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590422b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458401ea0820e7bd612d95b106aed237731422872f7f8fb6f5ea6304c9001bfd1bfcb12d78b3744cad517085786986965a556f5b74fa951322cf41c57e2994f02bf0b", + "expect": "verify", + "id_hex": "c5b0e62aecf6bab69a0434216fa989a9d1935a299a50dd48855743071f7eb580", + "name": "reversible-local", + "note": "Read-modify-write resolved on-device. Nothing left the machine, so egress is `none` with zero bytes.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a265636c617373646e6f6e656674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a059038bb1647469657262533566656666656374a265636c617373646e6f6e656674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458405acb134e4267a5e8e0909dd36cc41194f5c0b796e36039f8d39108e7f9e9619dc5acdeb45368ee620d9f3c15f7f3f919e10bb656e4793e1d1a03abd23825320b", + "expect": "verify", + "id_hex": "318270be152d0a33ed88c8de6ae622ba12d019703c56554f8e347f32fc2f4da8", + "name": "read-only", + "note": "A query that changed nothing. Safe to replay; no before/after state to record.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "class": "none", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736b636f6d70656e7361626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626b636f6d70656e7361746f7278406561626436306166366361303332336436396161633538666639346262313538616133643862356337616133363633303231373138663264396439396338636166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590471b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736b636f6d70656e7361626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626b636f6d70656e7361746f7278406561626436306166366361303332336436396161633538666639346262313538616133643862356337616133363633303231373138663264396439396338636166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840808826b8524ace60d9f2cbb24abc8b284ab8d1181429c65b952f88a37424da5b31e6c4e3dc16bd079a200806b92ecfd26dc86b2e8c3abcfbbb31b19132889b06", + "expect": "verify", + "id_hex": "8843e43c0f4591985d9d96c5ad319d63fca7c4baaca3af7bcd606f2cc6835b9b", + "name": "compensable-with-compensator", + "note": "Cannot be undone, but the grant that could compensate is named at the time of acting — not discovered afterwards.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "compensable", + "compensator": "eabd60af6ca0323d69aac58ff94bb158aa3d8b5c7aa3663021718f2d9d99c8ca", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626c706c616e5f7265636569707478406466383635316564316434653064356264393936623963363337323531316432373136396265333363336237386237393334336636376531346665636462393166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590473b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626c706c616e5f7265636569707478406466383635316564316434653064356264393936623963363337323531316432373136396265333363336237386237393334336636376531346665636462393166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458409fc1a7362b97f0ce75f2e2afb695e4ac78567bc3ef4af4c3e935ea9c64a77912959bdc1870c5f052ba992aced3eff720a232344130b025de11c094e5af443f04", + "expect": "verify", + "id_hex": "f84610524e627953f2023e4af155958c61861e530f3e4dcdcfe030d515c836be", + "name": "irreversible-with-plan", + "note": "An irreversible commit carrying the plan receipt that preceded it. This is the only shape in which `irreversible` is well-formed.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "irreversible", + "plan_receipt": "df8651ed1d4e0d5bd996b9c6372511d27169be33c3b78b79343f67e14fecdb91", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a3647065657278403135643161323961656661653564646337323437633438356437613539306538376635616633343034626130333163653031386630386230386236316633306365627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590477b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a3647065657278403135643161323961656661653564646337323437633438356437613539306538376635616633343034626130333163653031386630386230386236316633306365627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458403695157a344c7aa68dc768507a195225d1a6fa4d843a5e6a4969fb421d600c94718da5ae12a09780cb4093b0e676c1fe7425e1a523da33cfa64b91459bbc7805", + "expect": "verify", + "id_hex": "aee95ef630da5356efb75c8cd40b029eefd5023a8014e257f218b5ed1e87cdd2", + "name": "egress-attested-enclave", + "note": "Work left the device to somewhere that proved what it was running. The peer attestation is bound in the receipt.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "attested_enclave", + "peer": "15d1a29aefae5ddc7247c485d7a590e87f5af3404ba031ce018f08b08b61f30c" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533066656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319200065636c6173736b74686972645f7061727479677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e6768736f667477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a059042bb1647469657262533066656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319200065636c6173736b74686972645f7061727479677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e6768736f667477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74584048e3a978439989c20d7ad5122f1d35fb4e50afae506c7b19a65c9d6b03781888de9e7bf2d1fbda44c1816cec11dc3d6a8ca6fa980cb0c141428777f6b0bce006", + "expect": "verify", + "id_hex": "cb9cb90ed902a8ede09ee56e57f76ab10e3f50f88915c11ea8868150aae24b33", + "name": "egress-third-party-honest", + "note": "An unattested destination, honestly recorded rather than upgraded. Trust is not an egress class.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 8192, + "class": "third_party" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "software", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S0", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a00124f806a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e636569457374696d61746f72", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a00124f806a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e636569457374696d61746f725840e3b4480fdddf8664bc505b94d1597fda6e391234be07435ae9e11ffefa646c7013d57d75f1f05613a897c9f55f8f0e28824ca4d7b6dde814dcc45a8295963d06", + "expect": "verify", + "id_hex": "37ad6db4defd7ec0e248cc5cdacc61a16f962aa5adba9bdee0dd0f8989356c1f", + "name": "estimated-energy", + "note": "Energy from an estimator, not a hardware counter. `HwShunt` and `Estimator` are different claims and must never collapse into one number.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "Estimator", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 1200000, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458406c575b828bc2baea9c27d8e4cf60fbd17a6961bb75f8927ee19d0b4e3b1a5e6b43731523c13f819023bf8af5bc29afa405b57cf379f737f75ccc2582a84ad90a", + "expect": "reject:irreversible-without-plan", + "name": "irreversible-without-plan", + "note": "Correctly signed, structurally invalid: an irreversible effect with no plan receipt. A verifier that only checks signatures accepts this.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "irreversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319100065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840d2c9adfe8cd2c27cf19d717f2fc1357cbfa949bda511e76cd2e407d0aa326e159931c9142cb0d1510f70f715f6f99fb6f755ca02c63ab3f2d62cb4cd6f3e330c", + "expect": "reject:egress-none-with-bytes", + "name": "egress-none-with-bytes", + "note": "Claims nothing left the device while counting 4096 bytes that did. The claim is falsified by its own byte count.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590430b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840c81d8fe4462d5834f802bd0a0d7c11a547f488dd237a941df6cbf0bae37d58ec6d225ff22b1517e03a48b9495eb46192c4787652e3e3219fb18bcf0c9cdc8009", + "expect": "reject:attested-egress-without-peer", + "name": "attested-egress-without-peer", + "note": "Claims an attested destination with no peer attestation to bind. The router may not claim a stronger class than its evidence supports.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "attested_enclave" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + } + ] +} diff --git a/jcp/conformance/v1/action_receipt_meta.json b/jcp/conformance/v1/action_receipt_meta.json new file mode 100644 index 000000000..f9f2c7c59 --- /dev/null +++ b/jcp/conformance/v1/action_receipt_meta.json @@ -0,0 +1,9 @@ +{ + "alg": "EdDSA (COSE -8)", + "negatives": 3, + "note": "Fixture key, published deliberately so third parties can verify. Never use it for anything real.", + "positives": 7, + "profile": "ar/1-draft", + "pubkey_hex": "197f6b23e16c8532c6abc838facd5ea789be0c76b2920334039bfa8b3d368d61", + "steward": "did:example:ar-reference" +} diff --git a/jcp/jcp-rs/Cargo.lock b/jcp/jcp-rs/Cargo.lock index 22204c44d..2a8c4dcf4 100644 --- a/jcp/jcp-rs/Cargo.lock +++ b/jcp/jcp-rs/Cargo.lock @@ -503,6 +503,19 @@ dependencies = [ "thiserror 2.0.20", ] +[[package]] +name = "jcp-action-receipt" +version = "0.1.0" +dependencies = [ + "ed25519-dalek", + "hex", + "jcp-receipt", + "jcp-schema", + "serde", + "serde_json", + "thiserror 2.0.18", +] + [[package]] name = "jcp-bridge" version = "0.1.0" diff --git a/jcp/jcp-rs/Cargo.toml b/jcp/jcp-rs/Cargo.toml index c413f9104..d82761317 100644 --- a/jcp/jcp-rs/Cargo.toml +++ b/jcp/jcp-rs/Cargo.toml @@ -5,6 +5,7 @@ members = [ "crates/jcp-grant", "crates/jcp-runtime", "crates/jcp-receipt", + "crates/jcp-action-receipt", "crates/jcp-bridge", "crates/jcp-energy", "crates/jcp-wire", @@ -37,6 +38,7 @@ jcp-schema = { path = "crates/jcp-schema" } jcp-grant = { path = "crates/jcp-grant" } jcp-runtime = { path = "crates/jcp-runtime" } jcp-receipt = { path = "crates/jcp-receipt" } +jcp-action-receipt = { path = "crates/jcp-action-receipt" } jcp-bridge = { path = "crates/jcp-bridge" } jcp-energy = { path = "crates/jcp-energy" } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml new file mode 100644 index 000000000..db7703dfb --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml @@ -0,0 +1,21 @@ +[package] +name = "jcp-action-receipt" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true +description = "Action Receipt (AR-1) — the composition envelope binding authority, environment, work and effect into one verifiable artifact. Introduces no new cryptography: canonical det-CBOR and COSE_Sign1 are reused verbatim from JCR-1. Binds by content-id so each existing receipt family keeps its own encoding and signer." + +[dependencies] +jcp-schema = { workspace = true } +jcp-receipt = { workspace = true } +ed25519-dalek = { workspace = true } +serde = { workspace = true } +serde_json = { workspace = true } +hex = { workspace = true } +thiserror = { workspace = true } + +[dev-dependencies] +hex = { workspace = true } +jcp-receipt = { workspace = true } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md b/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md new file mode 100644 index 000000000..9c00c7cba --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md @@ -0,0 +1,208 @@ +# Action Receipt Specification (AR-1) — Draft + +**Status:** Draft. Profile tag `ar/1-draft`. Field names are settled against the +existing canonical projections; the tag becomes `ar/1` when the vector pack has +been reviewed. + +**Conformance pack:** `jcp/conformance/v1/action_receipt.json`, +`action_receipt_meta.json` — 7 positive and 3 negative vectors, signed with a +published fixture key. + +--- + +## 0. Why this exists + +Three receipt families already ship in this tree. Each records one quarter of +what an audit actually asks for, and **none of them binds to the others**: + +| Family | Records | Carries | +|---|---|---| +| `jcp-receipt` | authority | grant chain, verdict, budget drawn | +| `sandbox-proof` | environment | attestation, isolation tier, substrate | +| JCR-1 | work | input hash, measured joules, energy provenance | +| *(nothing)* | **effect** | what changed, and whether it can be undone | + +So no single artifact answers: *under what authority did this agent do that, +where did it run, what did it cost, and what did it change?* + +The receipt encoding is implemented six independent times across the tree. That +is evidence the **encoding** is portable, and evidence the **composition** was +never specified. AR-1 specifies it. + +Two of the three families already gesture at the chain — the sandbox proof cell +carries a `receipt_id`, the authority receipt carries a `payload_hash`. The +intent was there. The binding was not. + +## 1. Design invariants + +1. **Envelope, not replacement.** Each family keeps its own canonical encoding + and its own signer. AR-1 reaches into them by content-id; they never reach + back. Every existing verifier continues to work unchanged. +2. **No new cryptography.** Canonical det-CBOR (RFC 8949 §4.2.1) and the tagged + COSE_Sign1 envelope are reused verbatim from JCR-1. If AR-1 ever appears to + need a novel primitive, the design has gone wrong. +3. **Refusal over record-keeping.** A format that merely records claims is a + log. AR-1 defines three shapes that MUST be refused at verification, so a + violation is *detectable* rather than a matter of trust. +4. **Never claim beyond the evidence.** Every field that asserts a property must + be falsifiable from the receipt itself or from an artifact it binds. + +## 2. The signed core + +Canonical projection, det-CBOR encoded, signed as COSE_Sign1 with EdDSA +(COSE `alg` −8). Absent optional fields are **omitted, not nulled** — JCR-1 §3.1 +drops nulls from the signed core, so an emitted null would not round-trip. + +``` +ActionReceipt { + ar_receipt: "ar/1-draft" // profile tag + closed_at: Timestamp // RFC 3339 + + // binding 1 — authority + grant_id: ContentId + chain_ids: [ContentId]? // root first; omitted when empty + authority_receipt: ContentId + verdict: "allow" | "deny" + + // binding 2 — environment + attestation_id: ContentId + proof_cell_id: ContentId? + tier: "S0".."S7" + grounding: "hardware" | "software" + + // binding 3 — work + work_receipt: ContentId + input_hash: Hash + joules_uj: u64 + energy_provenance: "HwShunt" | "ModelBased" | "Estimator" + + // binding 4 — effect (new; nothing else records this) + effect: { + class: "none" | "reversible" | "compensable" | "irreversible" + target: ContentId + before: Hash? + after: Hash? + compensator: ContentId? + plan_receipt: ContentId? + } + + // binding 5 — egress (the router's per-request privacy contract) + egress: { + class: "none" | "attested_enclave" | "third_party" + bytes: u64 + peer: ContentId? + } + + steward: String // REQUIRED, as in JCR-1 §2.1 +} +``` + +**Receipt id** = BLAKE3 over the canonical signed core. + +### 2.1 `grounding` is carried, never upgraded + +`grounding` reports whether the bound attestation is rooted in silicon or in +software. It is copied verbatim from that attestation. An implementation MUST +NOT promote `software` to `hardware` under any circumstance — the field exists +precisely so that a software-rooted claim stays legible as one. + +### 2.2 `energy_provenance` never collapses + +`HwShunt`, `ModelBased` and `Estimator` are three different claims about how a +joule figure was obtained. An implementation MUST NOT sum or average across +them into a single undifferentiated number. A measured figure and an estimated +one are not interchangeable, and a receipt that treats them as such is lying by +arithmetic. + +## 3. The three rules + +These MUST be enforced at verification, re-derived from the wire projection — +**not** from a caller-supplied struct. A receipt hand-forged to violate them +signs correctly and must be rejected anyway. The negative vectors in the pack +exist to prove an implementation does this. + +| # | Rule | Rationale | +|---|---|---| +| 1 | `effect.class == "irreversible"` REQUIRES `effect.plan_receipt` | The cascade's body-tier design already separates plan from commit for actions that touch the world. AR-1 binds that discipline into the evidence: an irreversible commit with no preceding plan is a protocol violation, not a missing nicety. | +| 2 | `egress.class == "none"` REQUIRES `egress.bytes == 0` | A claim that nothing left the machine is falsified by its own byte count. | +| 3 | `egress.class == "attested_enclave"` REQUIRES `egress.peer` | The router may never claim a stronger class than it can bind evidence for. An unattested destination is `third_party` even when the operator believes it trustworthy. **Trust is not an egress class.** | + +## 4. Effect classes + +| Class | Contract | Enforcement | +|---|---|---| +| `none` | Read-only. Nothing changed. | Trivially safe to replay | +| `reversible` | `before` recorded; prior state restorable. | Undo is a state transition | +| `compensable` | Cannot be undone, but a compensating action exists and **its grant is named at the time of acting** — not discovered afterwards. | `compensator` bound in the receipt | +| `irreversible` | Once committed, permanent. | Rule 1: plan/commit separation | + +AR-1 does not solve effect revocation — **nothing does, in general**. Revoking +authority does not un-send an email or un-move funds. What AR-1 does is make the +distinction explicit and machine-readable *at the moment of action*, which is +the precondition for any system that wants to reason about it afterwards. + +## 5. Egress classes + +| Class | Means | Verifiable by | +|---|---|---| +| `none` | Resolved on-device. | Rule 2, plus tier and attestation | +| `attested_enclave` | Left the device to somewhere that proved what it was running. | Rule 3 — the peer attestation id | +| `third_party` | Left the device to an unattested destination. | Named and counted, honestly marked unverifiable | + +## 6. Verification flow + +1. Parse the tagged COSE_Sign1 envelope; reject any `alg` other than EdDSA (−8). +2. Check `kid` against the expected steward. +3. Verify the signature over the canonical signed core. +4. Decode the core as canonical det-CBOR. Reject trailing bytes — a signed core + is exactly one item, and anything appended is corruption or an attempt to + smuggle data past a verifier that stops at the first complete value. +5. Check the profile tag. +6. **Apply the three rules to the decoded projection.** +7. Optionally resolve each bound content-id and verify the underlying receipt in + its own family's verifier. AR-1 binds; it does not re-verify on their behalf. + +Steps 1–6 require only the envelope and a public key. That is what makes a +standalone verifier possible, and shipping that verifier is what turns an +internal convention into something a third party can adopt. + +## 7. Conformance + +An implementation conforms at **AR-1/basic** when, given the published pack: + +- every positive vector verifies, and the re-derived receipt id and canonical + core match the published `id_hex` and `core_hex` byte-for-byte; +- every negative vector is **rejected**, despite carrying a genuine signature. + +The negatives are the substance. An implementation that checks signatures and +skips the structural rules passes the positives and fails the pack — which is +exactly the failure mode the pack is designed to catch. + +## 8. What AR-1 deliberately does not do + +- **Key custody and recovery.** Unsolved everywhere; AR-1 must not be built in a + way that presumes a solution. +- **Re-verifying bound receipts.** Each family owns its own verification. AR-1 + binds content-ids and stops there. +- **Proving the energy figure is honest.** It carries provenance so a reader can + judge; it does not adjudicate. +- **Undoing effects.** See §4. + +## 9. Security considerations + +**A valid signature is not a valid receipt.** The three rules exist because +signature verification alone accepts well-formed lies. The negative vectors +demonstrate this concretely: each is signed with the real fixture key and each +must be refused. + +**Content-id binding is only as strong as the bound artifacts.** AR-1 proves +*which* authority receipt, attestation and work receipt were referenced. It does +not prove those artifacts are themselves sound — that is their own verifiers' +job, and a complete audit runs all of them. + +**The energy cross-check is a consistency check, not a proof.** An attestation +asserts; joules are measured. Binding both means a forged attestation must also +maintain a plausible energy profile across an independently sampled counter, and +that the failure is visible rather than silent. An adversary with physical +access who can forge a quote can also influence measurement. Claiming more than +this would be exactly the overreach the design exists to avoid. diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs b/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs new file mode 100644 index 000000000..c898d5421 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs @@ -0,0 +1,244 @@ +//! Emit the AR-1 conformance vector pack. +//! +//! ```text +//! cargo run -p jcp-action-receipt --example emit_vectors -- jcp/conformance/v1 +//! ``` +//! +//! Writes `action_receipt.json` and `action_receipt_meta.json`, following the +//! shape the existing JCP packs use: a `meta` file declaring the algorithm, +//! profile, public key and steward, and a vectors file carrying signed +//! envelopes as hex. +//! +//! The signing key is a **published fixture**, deliberately: a conformance +//! vector nobody else can verify is not a conformance vector. It is the +//! all-`0x2a` key and must never be used for anything real. +//! +//! Both positive and negative vectors ship. The negatives are the point — they +//! pin the three structural rules, so an implementation that accepts a +//! well-signed but ill-formed receipt fails the pack rather than passing it. + +use ed25519_dalek::SigningKey; +use jcp_action_receipt::{ + ActionReceipt, Effect, EffectClass, Egress, EgressClass, verify, +}; +use jcp_receipt::jcr1; +use jcp_schema::ContentId; +use serde_json::{Value, json}; + +/// Published fixture key. Not a secret; never use it for anything real. +const FIXTURE_SEED: [u8; 32] = [0x2a; 32]; + +const STEWARD: &str = "did:example:ar-reference"; + +fn cid(tag: &str) -> ContentId { + ContentId::of_bytes(tag.as_bytes()) +} + +fn base() -> ActionReceipt { + ActionReceipt { + closed_at: "2026-08-25T12:00:00Z".into(), + grant_id: cid("grant/root"), + chain_ids: vec![cid("grant/root"), cid("grant/delegated")], + authority_receipt: cid("jcp-receipt/allow"), + verdict: "allow".into(), + attestation_id: cid("attest/eat"), + proof_cell_id: Some(cid("proof/cell")), + tier: "S5".into(), + grounding: "hardware".into(), + work_receipt: cid("jcr1/resolution"), + input_hash: "a".repeat(64), + joules_uj: 19_538_280, + energy_provenance: "HwShunt".into(), + effect: Effect { + class: EffectClass::Reversible, + target: cid("target/document"), + before: Some("b".repeat(64)), + after: Some("c".repeat(64)), + compensator: None, + plan_receipt: None, + }, + egress: Egress { + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: STEWARD.into(), + } +} + +/// A signed vector plus the properties a verifier must reproduce. +fn positive(name: &str, note: &str, r: &ActionReceipt, key: &SigningKey) -> Value { + let env = r.seal(key).expect("valid receipt must seal"); + // Prove the vector before publishing it — a pack that ships an + // unverifiable vector is worse than no pack. + let v = verify(&env, &key.verifying_key(), STEWARD).expect("emitted vector must verify"); + assert_eq!(v.id, r.id().unwrap()); + json!({ + "name": name, + "note": note, + "expect": "verify", + "id_hex": r.id().unwrap().to_hex(), + "core_hex": hex::encode(r.signed_core().unwrap()), + "envelope_hex": hex::encode(&env), + "wire": r.to_wire(), + }) +} + +/// A negative vector: correctly signed, structurally invalid. Built by signing +/// a hand-edited projection so the signature is genuine — an implementation +/// that only checks signatures will accept it, which is exactly what the pack +/// is designed to catch. +fn negative(name: &str, note: &str, expect: &str, wire: Value, key: &SigningKey) -> Value { + let core = jcr1::signed_core_bytes(&wire).expect("core"); + let env = jcr1::cose_sign1_envelope(&core, key, STEWARD); + // The signature really is valid... + jcr1::verify_cose_sign1(&env, STEWARD, key.verifying_key().as_bytes()) + .expect("negative vector must carry a genuine signature"); + // ...and AR-1 must still refuse it. + assert!( + verify(&env, &key.verifying_key(), STEWARD).is_err(), + "negative vector `{name}` was accepted — the rule it pins is not enforced" + ); + json!({ + "name": name, + "note": note, + "expect": expect, + "envelope_hex": hex::encode(&env), + "wire": wire, + }) +} + +fn main() -> Result<(), Box> { + let out_dir = std::env::args().nth(1).unwrap_or_else(|| ".".into()); + let key = SigningKey::from_bytes(&FIXTURE_SEED); + + let mut vectors = Vec::new(); + + // ── positives: one per effect class, one per egress class ────────── + vectors.push(positive( + "reversible-local", + "Read-modify-write resolved on-device. Nothing left the machine, so egress is `none` with zero bytes.", + &base(), + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::None; + r.effect.before = None; + r.effect.after = None; + vectors.push(positive( + "read-only", + "A query that changed nothing. Safe to replay; no before/after state to record.", + &r, + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::Compensable; + r.effect.compensator = Some(cid("grant/refund")); + vectors.push(positive( + "compensable-with-compensator", + "Cannot be undone, but the grant that could compensate is named at the time of acting — not discovered afterwards.", + &r, + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = Some(cid("plan/receipt")); + vectors.push(positive( + "irreversible-with-plan", + "An irreversible commit carrying the plan receipt that preceded it. This is the only shape in which `irreversible` is well-formed.", + &r, + &key, + )); + + let mut r = base(); + r.egress.class = EgressClass::AttestedEnclave; + r.egress.bytes = 4_096; + r.egress.peer = Some(cid("attest/peer-enclave")); + vectors.push(positive( + "egress-attested-enclave", + "Work left the device to somewhere that proved what it was running. The peer attestation is bound in the receipt.", + &r, + &key, + )); + + let mut r = base(); + r.egress.class = EgressClass::ThirdParty; + r.egress.bytes = 8_192; + r.egress.peer = None; + r.tier = "S0".into(); + r.grounding = "software".into(); + vectors.push(positive( + "egress-third-party-honest", + "An unattested destination, honestly recorded rather than upgraded. Trust is not an egress class.", + &r, + &key, + )); + + let mut r = base(); + r.energy_provenance = "Estimator".into(); + r.joules_uj = 1_200_000; + vectors.push(positive( + "estimated-energy", + "Energy from an estimator, not a hardware counter. `HwShunt` and `Estimator` are different claims and must never collapse into one number.", + &r, + &key, + )); + + // ── negatives: the three structural rules ────────────────────────── + let mut w = base().to_wire(); + w["effect"]["class"] = json!("irreversible"); + vectors.push(negative( + "irreversible-without-plan", + "Correctly signed, structurally invalid: an irreversible effect with no plan receipt. A verifier that only checks signatures accepts this.", + "reject:irreversible-without-plan", + w, + &key, + )); + + let mut w = base().to_wire(); + w["egress"]["bytes"] = json!(4_096u64); + vectors.push(negative( + "egress-none-with-bytes", + "Claims nothing left the device while counting 4096 bytes that did. The claim is falsified by its own byte count.", + "reject:egress-none-with-bytes", + w, + &key, + )); + + let mut w = base().to_wire(); + w["egress"]["class"] = json!("attested_enclave"); + w["egress"]["bytes"] = json!(4_096u64); + vectors.push(negative( + "attested-egress-without-peer", + "Claims an attested destination with no peer attestation to bind. The router may not claim a stronger class than its evidence supports.", + "reject:attested-egress-without-peer", + w, + &key, + )); + + let meta = json!({ + "alg": "EdDSA (COSE -8)", + "profile": jcp_action_receipt::AR_PROFILE, + "pubkey_hex": hex::encode(key.verifying_key().as_bytes()), + "steward": STEWARD, + "note": "Fixture key, published deliberately so third parties can verify. Never use it for anything real.", + "positives": vectors.iter().filter(|v| v["expect"] == "verify").count(), + "negatives": vectors.iter().filter(|v| v["expect"] != "verify").count(), + }); + + let vpath = format!("{out_dir}/action_receipt.json"); + let mpath = format!("{out_dir}/action_receipt_meta.json"); + std::fs::write(&vpath, serde_json::to_string_pretty(&json!({ "vectors": vectors }))? + "\n")?; + std::fs::write(&mpath, serde_json::to_string_pretty(&meta)? + "\n")?; + + println!("wrote {vpath}"); + println!("wrote {mpath}"); + println!( + " {} positive, {} negative", + meta["positives"], meta["negatives"] + ); + Ok(()) +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs new file mode 100644 index 000000000..71e12e733 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs @@ -0,0 +1,228 @@ +//! Canonical det-CBOR decoder for the AR-1 subset. +//! +//! `jcp_receipt::jcr1` ships a canonical *encoder* and no decoder, because +//! nothing downstream of it needed to read a signed core back. A verifier does: +//! the point of AR-1 is that a third party holding only an envelope can check +//! the structural rules for themselves, and that requires recovering the +//! projection from the bytes. +//! +//! Rather than take a CBOR dependency — AR-1's whole claim is that it adds no +//! new primitives — this is the exact inverse of the encoder's subset, and +//! nothing more. The encoder emits four major types (RFC 8949 §4.2.1: maps, +//! arrays, text strings, unsigned integers; no floats, bools, nulls or tags), +//! so those four are all this decodes. Anything else is refused rather than +//! guessed at, which is the same discipline the encoder applies on the way out. +//! +//! `decode_roundtrips_every_encoded_shape` pins the two halves together. + +use serde_json::{Map, Value}; + +/// Why a canonical decode failed. +#[derive(Debug, thiserror::Error)] +pub enum DecodeError { + /// Input ended mid-item. + #[error("truncated input at byte {0}")] + Truncated(usize), + /// A major type outside the canonical subset appeared. + #[error("major type {0} is outside the canonical subset at byte {1}")] + UnsupportedMajor(u8, usize), + /// An additional-information value the canonical form never emits. + #[error("non-canonical length encoding at byte {0}")] + NonCanonicalLength(usize), + /// A text string was not valid UTF-8. + #[error("invalid utf-8 in text string at byte {0}")] + BadUtf8(usize), + /// A map key was not a text string. + #[error("non-text map key at byte {0}")] + NonTextKey(usize), + /// Bytes remained after the top-level item. + #[error("{0} trailing byte(s) after top-level item")] + Trailing(usize), +} + +/// Decode canonical det-CBOR produced by `jcr1::canonical_cbor` back to JSON. +/// +/// Rejects trailing bytes: a signed core is exactly one item, and anything +/// appended to it is either corruption or an attempt to smuggle data past a +/// verifier that stops reading at the first complete value. +pub fn from_canonical_cbor(bytes: &[u8]) -> Result { + let mut p = Parser { b: bytes, i: 0 }; + let v = p.value()?; + if p.i != bytes.len() { + return Err(DecodeError::Trailing(bytes.len() - p.i)); + } + Ok(v) +} + +struct Parser<'a> { + b: &'a [u8], + i: usize, +} + +impl<'a> Parser<'a> { + fn byte(&mut self) -> Result { + let b = *self.b.get(self.i).ok_or(DecodeError::Truncated(self.i))?; + self.i += 1; + Ok(b) + } + + fn take(&mut self, n: usize) -> Result<&'a [u8], DecodeError> { + let end = self.i.checked_add(n).ok_or(DecodeError::Truncated(self.i))?; + let s = self.b.get(self.i..end).ok_or(DecodeError::Truncated(self.i))?; + self.i = end; + Ok(s) + } + + /// Argument of a head byte, enforcing the shortest-form rule the canonical + /// encoder guarantees. A longer-than-necessary encoding is a different byte + /// string for the same value, which would break content addressing. + fn arg(&mut self, ai: u8) -> Result { + let at = self.i - 1; + Ok(match ai { + 0..=23 => ai as u64, + 24 => { + let v = self.byte()? as u64; + if v < 24 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 25 => { + let s = self.take(2)?; + let v = u16::from_be_bytes([s[0], s[1]]) as u64; + if v <= u8::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 26 => { + let s = self.take(4)?; + let v = u32::from_be_bytes([s[0], s[1], s[2], s[3]]) as u64; + if v <= u16::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 27 => { + let s = self.take(8)?; + let v = u64::from_be_bytes([s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]); + if v <= u32::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + _ => return Err(DecodeError::NonCanonicalLength(at)), + }) + } + + fn value(&mut self) -> Result { + let at = self.i; + let head = self.byte()?; + let major = head >> 5; + let ai = head & 0x1f; + match major { + 0 => Ok(Value::from(self.arg(ai)?)), + 3 => { + let n = self.arg(ai)? as usize; + let s = self.take(n)?; + Ok(Value::String( + std::str::from_utf8(s) + .map_err(|_| DecodeError::BadUtf8(at))? + .to_owned(), + )) + } + 4 => { + let n = self.arg(ai)? as usize; + let mut out = Vec::with_capacity(n.min(1024)); + for _ in 0..n { + out.push(self.value()?); + } + Ok(Value::Array(out)) + } + 5 => { + let n = self.arg(ai)? as usize; + let mut out = Map::new(); + for _ in 0..n { + let kat = self.i; + let k = match self.value()? { + Value::String(s) => s, + _ => return Err(DecodeError::NonTextKey(kat)), + }; + out.insert(k, self.value()?); + } + Ok(Value::Object(out)) + } + m => Err(DecodeError::UnsupportedMajor(m, at)), + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use jcp_receipt::jcr1; + use serde_json::json; + + /// The property that matters: whatever the canonical encoder emits, this + /// reads back identically. If these two ever drift, a verifier and a signer + /// disagree about what a receipt says. + #[test] + fn decode_roundtrips_every_encoded_shape() { + let cases = vec![ + json!({}), + json!({"a": 0}), + json!({"a": 23, "b": 24, "c": 255, "d": 256, "e": 65535, "f": 65536}), + json!({"big": 4_294_967_296u64, "huge": 19_538_280u64}), + json!({"s": "", "t": "hello", "u": "a".repeat(64)}), + json!({"arr": [1, 2, 3], "empty": []}), + json!({"nested": {"deep": {"deeper": [1, {"x": "y"}]}}}), + json!({"unicode": "joules — ⚡ 変換"}), + json!({"long": "x".repeat(300)}), + ]; + for c in cases { + let enc = jcr1::canonical_cbor(&c).expect("encode"); + let dec = from_canonical_cbor(&enc).expect("decode"); + assert_eq!(dec, c, "round-trip mismatch for {c}"); + } + } + + #[test] + fn rejects_trailing_bytes() { + let mut enc = jcr1::canonical_cbor(&json!({"a": 1})).unwrap(); + enc.push(0x00); + assert!(matches!( + from_canonical_cbor(&enc), + Err(DecodeError::Trailing(1)) + )); + } + + #[test] + fn rejects_truncated_input() { + let enc = jcr1::canonical_cbor(&json!({"key": "value"})).unwrap(); + assert!(from_canonical_cbor(&enc[..enc.len() - 2]).is_err()); + } + + #[test] + fn rejects_non_canonical_length() { + // 0x18 0x05 encodes 5 in two bytes where one would do. Same value, + // different bytes — which would break content addressing. + assert!(matches!( + from_canonical_cbor(&[0x18, 0x05]), + Err(DecodeError::NonCanonicalLength(0)) + )); + } + + #[test] + fn rejects_types_outside_the_subset() { + // 0xf5 is `true` (major 7), which the canonical encoder never emits. + assert!(matches!( + from_canonical_cbor(&[0xf5]), + Err(DecodeError::UnsupportedMajor(7, 0)) + )); + // 0x40 is a byte string (major 2) — also outside the subset. + assert!(matches!( + from_canonical_cbor(&[0x40]), + Err(DecodeError::UnsupportedMajor(2, 0)) + )); + } +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs new file mode 100644 index 000000000..9a80a9004 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs @@ -0,0 +1,564 @@ +//! # Action Receipt (AR-1) +//! +//! **The composition envelope.** Three receipt families already ship, and each +//! holds one quarter of the answer to the question an auditor actually asks — +//! *under what authority did this agent do that, where did it run, and what did +//! it cost?* None of them binds to the others. +//! +//! | Family | Records | Carries | +//! |---|---|---| +//! | `jcp-receipt` | authority | grant chain, verdict, budget drawn | +//! | `sandbox-proof` | environment | attestation, isolation tier, substrate | +//! | JCR-1 | work | input hash, measured joules, energy provenance | +//! | *(nothing)* | **effect** | what changed, and whether it can be undone | +//! +//! AR-1 binds the first three **by content-id** and supplies the fourth. It is +//! an envelope, not a replacement: every existing family keeps its own canonical +//! encoding and its own signer, and every existing verifier keeps working +//! unchanged. +//! +//! ## No new cryptography +//! +//! Canonical det-CBOR (RFC 8949 §4.2.1) and the tagged COSE_Sign1 envelope are +//! reused verbatim from [`jcp_receipt::jcr1`]. This crate adds a field layout +//! and three structural rules — nothing else. If AR-1 ever needs a novel +//! primitive, that is a signal the design went wrong. +//! +//! ## The three rules that carry the weight +//! +//! A receipt format that merely *records* claims is a log. What makes AR-1 +//! evidence is that certain shapes are refused at verification, so a violation +//! is detectable rather than a matter of trust: +//! +//! 1. **`effect: irreversible` requires a prior plan receipt.** The cascade's +//! body-tier design already separates plan from commit for actions that touch +//! the world. AR-1 binds that discipline into the artifact: an irreversible +//! effect with no `plan_receipt` fails verification. +//! 2. **`egress: none` requires zero bytes.** A claim that nothing left the +//! machine is falsifiable by its own byte count. +//! 3. **`egress: attested_enclave` requires a peer attestation.** The router may +//! never claim a stronger class than it can bind evidence for. An unattested +//! destination is `third_party` even when the operator believes it +//! trustworthy — trust is not an egress class. +//! +//! ## Status +//! +//! Draft. Field names are settled against the existing canonical projections but +//! the profile tag is `ar/1-draft` until the vector pack is reviewed. + +mod decode; +pub use decode::{DecodeError, from_canonical_cbor}; + +use jcp_receipt::jcr1::{self, Jcr1Error}; +use jcp_schema::ContentId; +use serde::{Deserialize, Serialize}; +use serde_json::{Map, Value, json}; + +/// Profile tag carried in every AR-1 receipt. +pub const AR_PROFILE: &str = "ar/1-draft"; + +/// Errors surfaced by AR-1 construction or verification. +#[derive(Debug, thiserror::Error)] +pub enum ArError { + /// The underlying JCR-1 canonical encoding or envelope layer failed. + #[error("jcr1: {0}")] + Jcr1(#[from] Jcr1Error), + /// An `irreversible` effect arrived without the plan receipt that the + /// plan/commit split requires. See the module docs, rule 1. + #[error("irreversible effect requires a plan receipt (AR-1 §4)")] + IrreversibleWithoutPlan, + /// `egress: none` was claimed alongside a non-zero byte count. + #[error("egress class `none` claims {0} bytes left the device (AR-1 §3)")] + EgressNoneWithBytes(u64), + /// `egress: attested_enclave` was claimed with no peer attestation to bind. + #[error("egress class `attested_enclave` requires a peer attestation (AR-1 §3)")] + AttestedEgressWithoutPeer, + /// The receipt did not carry the profile tag this crate understands. + #[error("unknown profile: expected `{AR_PROFILE}`, found `{0}`")] + UnknownProfile(String), + /// A field required by the canonical projection was absent. + #[error("missing required field: {0}")] + MissingField(&'static str), + /// The signed core did not decode as canonical CBOR. + #[error("canonical decode: {0}")] + Decode(#[from] DecodeError), +} + +/// What an action did to the world, and whether it can be taken back. +/// +/// This is the only genuinely new field group in AR-1 — nothing in the three +/// existing families records it. The classes are ordered by how much of the +/// action survives a change of mind. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum EffectClass { + /// Read-only. Nothing changed; the action is safe to replay. + None, + /// Prior state is recoverable. Undo is a state transition. + Reversible, + /// Cannot be undone, but a compensating action exists and its grant is + /// named at the time of acting — not discovered afterwards. + Compensable, + /// Once committed, permanent. Requires plan/commit separation. + Irreversible, +} + +impl EffectClass { + /// Wire spelling, pinned so the projection cannot drift with serde config. + pub fn wire_tag(self) -> &'static str { + match self { + Self::None => "none", + Self::Reversible => "reversible", + Self::Compensable => "compensable", + Self::Irreversible => "irreversible", + } + } +} + +/// Where the work went, and what evidence backs that claim. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum EgressClass { + /// Resolved on-device. Nothing left the machine. + None, + /// Left the device to somewhere that proved what it was running. + AttestedEnclave, + /// Left the device to an unattested destination. Named and counted — + /// and honestly marked as unverifiable. + ThirdParty, +} + +impl EgressClass { + /// Wire spelling, pinned. + pub fn wire_tag(self) -> &'static str { + match self { + Self::None => "none", + Self::AttestedEnclave => "attested_enclave", + Self::ThirdParty => "third_party", + } + } +} + +/// The effect record: binding four, and the piece no existing family carries. +#[derive(Debug, Clone)] +pub struct Effect { + /// How much of this action survives a change of mind. + pub class: EffectClass, + /// What was acted on. + pub target: ContentId, + /// State hash before the action, where observable. + pub before: Option, + /// State hash after the action, where observable. + pub after: Option, + /// A grant that could undo this, for `Compensable` effects. + pub compensator: Option, + /// The plan receipt that preceded an `Irreversible` commit. Required for + /// that class; its absence is a protocol violation, not a missing nicety. + pub plan_receipt: Option, +} + +/// The egress record: binding five, the router's per-request privacy contract. +#[derive(Debug, Clone)] +pub struct Egress { + /// The strongest class the available evidence supports — never stronger. + pub class: EgressClass, + /// Bytes that left the device. + pub bytes: u64, + /// Attestation of the receiving side, for `AttestedEnclave`. + pub peer: Option, +} + +/// One agent action, with every binding needed to check it independently. +#[derive(Debug, Clone)] +pub struct ActionReceipt { + /// RFC 3339 close time. + pub closed_at: String, + + // -- binding 1: authority ------------------------------------------- + /// The grant that permitted this action. + pub grant_id: ContentId, + /// The full delegation chain, root first. Empty for a root grant. + pub chain_ids: Vec, + /// The `jcp-receipt` recording the authorisation decision. + pub authority_receipt: ContentId, + /// The decision itself, carried here so a verifier need not fetch the + /// authority receipt to learn whether the action was permitted. + pub verdict: String, + + // -- binding 2: environment ----------------------------------------- + /// The attestation covering the execution environment. + pub attestation_id: ContentId, + /// The signed sandbox proof cell, where one exists. + pub proof_cell_id: Option, + /// Isolation tier, `S0`..`S7`. + pub tier: String, + /// Whether the attestation is rooted in silicon or in software. Carried + /// verbatim from the attestation; never upgraded here. + pub grounding: String, + + // -- binding 3: work ------------------------------------------------ + /// The JCR-1 resolution receipt for the work performed. + pub work_receipt: ContentId, + /// Hash of the input the work consumed. + pub input_hash: String, + /// Measured cost in microjoules. + pub joules_uj: u64, + /// How that figure was obtained. Never collapsed into a single number: + /// `HwShunt` and `Estimator` are not the same claim. + pub energy_provenance: String, + + // -- bindings 4 and 5 ----------------------------------------------- + /// What changed in the world. + pub effect: Effect, + /// What left the device. + pub egress: Egress, + + /// The party accountable for this receipt. Required, as in JCR-1 §2.1. + pub steward: String, +} + +impl ActionReceipt { + /// Check the three structural rules. Called by both [`Self::seal`] and + /// [`verify`], so an invalid receipt can be neither produced nor accepted. + pub fn check_discipline(&self) -> Result<(), ArError> { + if self.effect.class == EffectClass::Irreversible && self.effect.plan_receipt.is_none() { + return Err(ArError::IrreversibleWithoutPlan); + } + if self.egress.class == EgressClass::None && self.egress.bytes != 0 { + return Err(ArError::EgressNoneWithBytes(self.egress.bytes)); + } + if self.egress.class == EgressClass::AttestedEnclave && self.egress.peer.is_none() { + return Err(ArError::AttestedEgressWithoutPeer); + } + Ok(()) + } + + /// The canonical JSON projection a third party canonicalises and hashes. + /// + /// Absent optionals are omitted rather than emitted as null, matching + /// JCR-1 §3.1 — `signed_core_bytes` drops nulls, so emitting them would + /// produce a projection that does not round-trip. + pub fn to_wire(&self) -> Value { + let mut o = Map::new(); + o.insert("ar_receipt".into(), json!(AR_PROFILE)); + o.insert("closed_at".into(), json!(self.closed_at)); + + o.insert("grant_id".into(), json!(self.grant_id.to_hex())); + if !self.chain_ids.is_empty() { + let chain: Vec = self.chain_ids.iter().map(|c| json!(c.to_hex())).collect(); + o.insert("chain_ids".into(), Value::Array(chain)); + } + o.insert("authority_receipt".into(), json!(self.authority_receipt.to_hex())); + o.insert("verdict".into(), json!(self.verdict)); + + o.insert("attestation_id".into(), json!(self.attestation_id.to_hex())); + if let Some(p) = &self.proof_cell_id { + o.insert("proof_cell_id".into(), json!(p.to_hex())); + } + o.insert("tier".into(), json!(self.tier)); + o.insert("grounding".into(), json!(self.grounding)); + + o.insert("work_receipt".into(), json!(self.work_receipt.to_hex())); + o.insert("input_hash".into(), json!(self.input_hash)); + o.insert("joules_uj".into(), json!(self.joules_uj)); + o.insert("energy_provenance".into(), json!(self.energy_provenance)); + + let mut e = Map::new(); + e.insert("class".into(), json!(self.effect.class.wire_tag())); + e.insert("target".into(), json!(self.effect.target.to_hex())); + if let Some(b) = &self.effect.before { + e.insert("before".into(), json!(b)); + } + if let Some(a) = &self.effect.after { + e.insert("after".into(), json!(a)); + } + if let Some(c) = &self.effect.compensator { + e.insert("compensator".into(), json!(c.to_hex())); + } + if let Some(p) = &self.effect.plan_receipt { + e.insert("plan_receipt".into(), json!(p.to_hex())); + } + o.insert("effect".into(), Value::Object(e)); + + let mut g = Map::new(); + g.insert("class".into(), json!(self.egress.class.wire_tag())); + g.insert("bytes".into(), json!(self.egress.bytes)); + if let Some(p) = &self.egress.peer { + g.insert("peer".into(), json!(p.to_hex())); + } + o.insert("egress".into(), Value::Object(g)); + + o.insert("steward".into(), json!(self.steward)); + Value::Object(o) + } + + /// Canonical signed-core bytes — det-CBOR over [`Self::to_wire`], via the + /// JCR-1 encoder. These are exactly the bytes the envelope signs. + pub fn signed_core(&self) -> Result, ArError> { + Ok(jcr1::signed_core_bytes(&self.to_wire())?) + } + + /// Content id of this receipt: BLAKE3 over the canonical signed core. + pub fn id(&self) -> Result { + Ok(ContentId::of_bytes(&self.signed_core()?)) + } + + /// Seal into a tagged COSE_Sign1 envelope. Refuses to sign a receipt that + /// violates the discipline rules — an invalid AR-1 cannot be produced by + /// this crate, only hand-forged. + pub fn seal( + &self, + signing_key: &ed25519_dalek::SigningKey, + ) -> Result, ArError> { + self.check_discipline()?; + let core = self.signed_core()?; + Ok(jcr1::cose_sign1_envelope(&core, signing_key, &self.steward)) + } +} + +/// The outcome of verifying an AR-1 envelope: the signed core it carried, plus +/// the wire projection parsed back out of it. +#[derive(Debug, Clone)] +pub struct Verified { + /// The canonical bytes that were signed. + pub core: Vec, + /// The projection recovered from those bytes. + pub wire: Value, + /// Content id of the receipt. + pub id: ContentId, +} + +/// Verify an AR-1 envelope end to end. +/// +/// Checks, in order: COSE_Sign1 signature and `kid` against `expected_steward`; +/// the profile tag; then the three discipline rules **re-derived from the wire +/// projection**, not from a caller-supplied struct. A receipt that was +/// hand-forged to violate them is rejected here even though it signs correctly. +pub fn verify( + envelope: &[u8], + verifying_key: &ed25519_dalek::VerifyingKey, + expected_steward: &str, +) -> Result { + let core = jcr1::verify_cose_sign1(envelope, expected_steward, verifying_key.as_bytes())?; + // jcr1 exposes an encoder but no decoder, so the projection is read back + // here. The signature has already been checked against `core`; this only + // reads structure out of bytes that are known-good. + let wire: Value = from_canonical_cbor(&core)?; + + let profile = wire + .get("ar_receipt") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("ar_receipt"))?; + if profile != AR_PROFILE { + return Err(ArError::UnknownProfile(profile.to_string())); + } + + let effect = wire.get("effect").ok_or(ArError::MissingField("effect"))?; + let eclass = effect + .get("class") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("effect.class"))?; + if eclass == "irreversible" && effect.get("plan_receipt").is_none() { + return Err(ArError::IrreversibleWithoutPlan); + } + + let egress = wire.get("egress").ok_or(ArError::MissingField("egress"))?; + let gclass = egress + .get("class") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("egress.class"))?; + let bytes = egress.get("bytes").and_then(Value::as_u64).unwrap_or(0); + if gclass == "none" && bytes != 0 { + return Err(ArError::EgressNoneWithBytes(bytes)); + } + if gclass == "attested_enclave" && egress.get("peer").is_none() { + return Err(ArError::AttestedEgressWithoutPeer); + } + + let id = ContentId::of_bytes(&core); + Ok(Verified { core, wire, id }) +} + +#[cfg(test)] +mod tests { + use super::*; + use ed25519_dalek::SigningKey; + + fn cid(b: u8) -> ContentId { + ContentId([b; 32]) + } + + fn key() -> SigningKey { + SigningKey::from_bytes(&[7u8; 32]) + } + + fn base() -> ActionReceipt { + ActionReceipt { + closed_at: "2026-08-25T00:00:00Z".into(), + grant_id: cid(1), + chain_ids: vec![cid(2)], + authority_receipt: cid(3), + verdict: "allow".into(), + attestation_id: cid(4), + proof_cell_id: Some(cid(5)), + tier: "S5".into(), + grounding: "hardware".into(), + work_receipt: cid(6), + input_hash: "a".repeat(64), + joules_uj: 19_538_280, + energy_provenance: "HwShunt".into(), + effect: Effect { + class: EffectClass::Reversible, + target: cid(7), + before: Some("b".repeat(64)), + after: Some("c".repeat(64)), + compensator: None, + plan_receipt: None, + }, + egress: Egress { + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: "did:example:ar-reference".into(), + } + } + + #[test] + fn seals_and_verifies_round_trip() { + let r = base(); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.core, r.signed_core().unwrap()); + assert_eq!(v.id, r.id().unwrap()); + assert_eq!(v.wire["tier"], "S5"); + assert_eq!(v.wire["joules_uj"], 19_538_280u64); + } + + #[test] + fn canonical_core_is_stable_across_encodes() { + let r = base(); + assert_eq!(r.signed_core().unwrap(), r.signed_core().unwrap()); + assert_eq!(r.id().unwrap(), r.id().unwrap()); + } + + #[test] + fn absent_optionals_are_omitted_not_nulled() { + // JCR-1 §3.1 drops nulls from the signed core, so emitting an explicit + // null would produce a projection that does not round-trip. + let r = base(); + let w = r.to_wire(); + assert!(w["effect"].get("compensator").is_none()); + assert!(w["egress"].get("peer").is_none()); + } + + // ── rule 1: irreversible requires a plan ───────────────────────── + + #[test] + fn irreversible_without_plan_refuses_to_seal() { + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = None; + assert!(matches!( + r.seal(&key()), + Err(ArError::IrreversibleWithoutPlan) + )); + } + + #[test] + fn irreversible_with_plan_seals() { + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = Some(cid(9)); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.wire["effect"]["class"], "irreversible"); + } + + // ── rule 2: egress none means zero bytes ───────────────────────── + + #[test] + fn egress_none_with_bytes_refuses_to_seal() { + let mut r = base(); + r.egress.bytes = 4096; + assert!(matches!( + r.seal(&key()), + Err(ArError::EgressNoneWithBytes(4096)) + )); + } + + // ── rule 3: attested egress needs a peer ───────────────────────── + + #[test] + fn attested_egress_without_peer_refuses_to_seal() { + let mut r = base(); + r.egress.class = EgressClass::AttestedEnclave; + r.egress.bytes = 1024; + r.egress.peer = None; + assert!(matches!( + r.seal(&key()), + Err(ArError::AttestedEgressWithoutPeer) + )); + } + + #[test] + fn third_party_egress_needs_no_peer() { + // An unattested destination is honestly recorded, not blocked. + let mut r = base(); + r.egress.class = EgressClass::ThirdParty; + r.egress.bytes = 1024; + r.egress.peer = None; + assert!(r.seal(&key()).is_ok()); + } + + // ── the rules bind at verification, not just construction ──────── + + #[test] + fn hand_forged_violation_is_rejected_at_verify() { + // Seal a valid receipt, then rebuild the core with an irreversible + // effect and no plan and sign it directly — bypassing `seal`. A verifier + // that only checked the signature would accept this. + let mut r = base(); + r.effect.class = EffectClass::Reversible; + let mut wire = r.to_wire(); + wire["effect"]["class"] = json!("irreversible"); + let core = jcr1::signed_core_bytes(&wire).unwrap(); + let forged = jcr1::cose_sign1_envelope(&core, &key(), &r.steward); + + // The signature is perfectly valid... + assert!(jcr1::verify_cose_sign1(&forged, &r.steward, key().verifying_key().as_bytes()).is_ok()); + // ...and AR-1 rejects it anyway. + assert!(matches!( + verify(&forged, &key().verifying_key(), &r.steward), + Err(ArError::IrreversibleWithoutPlan) + )); + } + + #[test] + fn wrong_steward_is_rejected() { + let r = base(); + let env = r.seal(&key()).unwrap(); + assert!(verify(&env, &key().verifying_key(), "did:example:someone-else").is_err()); + } + + #[test] + fn tampered_envelope_is_rejected() { + let r = base(); + let mut env = r.seal(&key()).unwrap(); + let n = env.len(); + env[n - 1] ^= 0xff; + assert!(verify(&env, &key().verifying_key(), &r.steward).is_err()); + } + + #[test] + fn energy_provenance_survives_the_round_trip_verbatim() { + // HwShunt and Estimator are different claims and must never collapse. + for prov in ["HwShunt", "ModelBased", "Estimator"] { + let mut r = base(); + r.energy_provenance = prov.into(); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.wire["energy_provenance"], prov); + } + } +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs b/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs new file mode 100644 index 000000000..e2939bb36 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs @@ -0,0 +1,113 @@ +//! Consume the published AR-1 conformance pack. +//! +//! This is the test that makes the pack mean something. It reads +//! `jcp/conformance/v1/action_receipt.json` from disk — the same bytes a third +//! party would download — resolves the public key from the meta file, and +//! checks every vector against the stated expectation. +//! +//! Crucially it consumes the *published artifact*, not in-memory values. A pack +//! that only its own generator can read is not a conformance pack. + +use ed25519_dalek::VerifyingKey; +use jcp_action_receipt::verify; +use serde_json::Value; + +fn pack_dir() -> std::path::PathBuf { + std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../../conformance/v1") + .canonicalize() + .expect("conformance dir must exist next to the spec") +} + +fn load(name: &str) -> Value { + let p = pack_dir().join(name); + let bytes = std::fs::read(&p).unwrap_or_else(|e| panic!("read {}: {e}", p.display())); + serde_json::from_slice(&bytes).unwrap_or_else(|e| panic!("parse {}: {e}", p.display())) +} + +fn key_and_steward() -> (VerifyingKey, String) { + let meta = load("action_receipt_meta.json"); + let hex_key = meta["pubkey_hex"].as_str().expect("meta.pubkey_hex"); + let raw = hex::decode(hex_key).expect("pubkey hex"); + let arr: [u8; 32] = raw.as_slice().try_into().expect("32-byte pubkey"); + let steward = meta["steward"].as_str().expect("meta.steward").to_string(); + (VerifyingKey::from_bytes(&arr).expect("valid pubkey"), steward) +} + +#[test] +fn every_positive_vector_verifies() { + let (vk, steward) = key_and_steward(); + let pack = load("action_receipt.json"); + let vectors = pack["vectors"].as_array().expect("vectors array"); + + let mut checked = 0; + for v in vectors { + if v["expect"] != "verify" { + continue; + } + let name = v["name"].as_str().unwrap_or(""); + let env = hex::decode(v["envelope_hex"].as_str().expect("envelope_hex")) + .unwrap_or_else(|e| panic!("{name}: envelope hex: {e}")); + + let ok = verify(&env, &vk, &steward) + .unwrap_or_else(|e| panic!("positive vector `{name}` failed to verify: {e}")); + + // The receipt id in the pack must match what a verifier re-derives from + // the bytes — otherwise the published id is decorative. + let want = v["id_hex"].as_str().expect("id_hex"); + assert_eq!(ok.id.to_hex(), want, "{name}: id mismatch"); + + // And the canonical core must match byte-for-byte, which is what makes + // the content address reproducible on another implementation. + let want_core = v["core_hex"].as_str().expect("core_hex"); + assert_eq!(hex::encode(&ok.core), want_core, "{name}: core mismatch"); + + checked += 1; + } + assert!(checked >= 7, "expected at least 7 positive vectors, saw {checked}"); +} + +#[test] +fn every_negative_vector_is_rejected_despite_a_valid_signature() { + let (vk, steward) = key_and_steward(); + let pack = load("action_receipt.json"); + let vectors = pack["vectors"].as_array().expect("vectors array"); + + let mut checked = 0; + for v in vectors { + let expect = v["expect"].as_str().unwrap_or("verify"); + if expect == "verify" { + continue; + } + let name = v["name"].as_str().unwrap_or(""); + let env = hex::decode(v["envelope_hex"].as_str().expect("envelope_hex")) + .unwrap_or_else(|e| panic!("{name}: envelope hex: {e}")); + + // The signature is genuine — these vectors exist precisely because a + // signature-only verifier would accept them. + let sig_ok = jcp_receipt::jcr1::verify_cose_sign1(&env, &steward, vk.as_bytes()); + assert!( + sig_ok.is_ok(), + "{name}: negative vector should carry a genuine signature" + ); + + // AR-1 must refuse it anyway. + assert!( + verify(&env, &vk, &steward).is_err(), + "negative vector `{name}` was accepted — the rule it pins is not enforced" + ); + checked += 1; + } + assert!(checked >= 3, "expected at least 3 negative vectors, saw {checked}"); +} + +#[test] +fn pack_declares_the_profile_this_build_implements() { + let meta = load("action_receipt_meta.json"); + assert_eq!( + meta["profile"].as_str().expect("meta.profile"), + jcp_action_receipt::AR_PROFILE, + "vector pack was generated for a different profile than this build implements" + ); + assert_eq!(meta["alg"].as_str().expect("meta.alg"), "EdDSA (COSE -8)"); +} -- 2.54.0 (Apple Git-157) From b4d8af688f24c8ee97ebd15d79a1f62aa29430c9 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 25 Aug 2026 22:41:15 -0400 Subject: [PATCH 02/11] ar-verify: the standalone Action Receipt verifier MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements §5 step 5 of the blueprint — "the deliverable that creates demand." A format nobody outside this tree can check is a convention. A format with a verifier a third party can run is a standard. Everything ar-verify needs arrives on the command line — an envelope, a public key, a steward — and it touches the network never. Two modes: ar-verify --pubkey --steward one receipt ar-verify --pack a whole vector pack ## Reports each binding separately "Invalid" is not a useful audit finding. The verifier prints one line per checked property — signature, canonical core, profile, receipt id, then the four bindings (authority / environment / work / effect) and the egress contract, then each of the three structural rules by name. An auditor learns *which* claim failed, and can quote it. On the forged vector the output is the whole thesis in one line: FAIL rule:irreversible-needs-plan REFUSED — irreversible effect with no plan receipt. The signature is valid; the receipt is not. ## Honest about its own limits Every successful run prints, unprompted: note:bound-artifacts content-ids bound but NOT resolved — run each family's own verifier for a complete audit AR-1 proves *which* authority receipt, attestation and work receipt were referenced. It does not prove those artifacts are sound; that is their own verifiers' job. A verifier that let a reader believe otherwise would be worse than none. ## Verified against the published pack 10 passed, 0 failed CONFORMANT — AR-1/basic. Positives verify; negatives are refused despite valid signatures. Exit codes: 0 verified · 1 check failed · 2 bad usage — so it composes into scripts and CI without parsing prose. No argument-parsing dependency; hand-rolled, consistent with the workspace's minimal-dependency posture. Accepts a hex text file or raw envelope bytes, because an auditor should not have to know which form the sender chose. Co-Authored-By: Claude Opus 4.8 (cherry picked from commit 0b29405ea0dc7aa4a34bf8b6cda564eb81ad9724) --- .../jcp-action-receipt/src/bin/ar-verify.rs | 374 ++++++++++++++++++ 1 file changed, 374 insertions(+) create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs new file mode 100644 index 000000000..cc952201d --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs @@ -0,0 +1,374 @@ +//! `ar-verify` — the standalone Action Receipt verifier. +//! +//! This is the deliverable that makes AR-1 matter to anyone outside this tree. +//! A format nobody else can check is a convention; a format with a verifier a +//! third party can run is a standard. Everything it needs arrives on the command +//! line — an envelope, a public key, a steward — and it reaches the network +//! never. +//! +//! ```text +//! ar-verify --pubkey --steward +//! ar-verify --pack # check a whole conformance pack +//! ar-verify ... --json +//! ``` +//! +//! It reports **each binding separately**, because "invalid" is not a useful +//! audit finding. An auditor needs to know *which* claim failed and why. +//! +//! Exit codes: `0` all checks passed · `1` a check failed · `2` bad usage. + +use ed25519_dalek::VerifyingKey; +use jcp_action_receipt::{ArError, verify}; +use serde_json::Value; +use std::process::ExitCode; + +fn main() -> ExitCode { + let args: Vec = std::env::args().skip(1).collect(); + if args.is_empty() || args.iter().any(|a| a == "-h" || a == "--help") { + usage(); + return ExitCode::from(2); + } + + let json_out = args.iter().any(|a| a == "--json"); + + if let Some(i) = args.iter().position(|a| a == "--pack") { + let Some(dir) = args.get(i + 1) else { + eprintln!("--pack needs a directory"); + return ExitCode::from(2); + }; + return verify_pack(dir, json_out); + } + + let path = &args[0]; + let Some(pubkey) = flag(&args, "--pubkey") else { + eprintln!("--pubkey is required"); + return ExitCode::from(2); + }; + let Some(steward) = flag(&args, "--steward") else { + eprintln!("--steward is required"); + return ExitCode::from(2); + }; + + let envelope = match read_envelope(path) { + Ok(b) => b, + Err(e) => { + eprintln!("{path}: {e}"); + return ExitCode::from(2); + } + }; + let vk = match parse_key(&pubkey) { + Ok(k) => k, + Err(e) => { + eprintln!("--pubkey: {e}"); + return ExitCode::from(2); + } + }; + + verify_one(&envelope, &vk, &steward, json_out) +} + +fn usage() { + eprintln!( + "ar-verify — independently check an Action Receipt (AR-1)\n\ + \n\ + USAGE\n \ + ar-verify --pubkey --steward [--json]\n \ + ar-verify --pack [--json]\n\ + \n\ + Reads only what you give it. Never touches the network." + ); +} + +fn flag(args: &[String], name: &str) -> Option { + args.iter() + .position(|a| a == name) + .and_then(|i| args.get(i + 1)) + .cloned() +} + +/// Accept either a hex text file or raw envelope bytes — an auditor should not +/// have to know which form the sender chose. +fn read_envelope(path: &str) -> Result, String> { + let raw = std::fs::read(path).map_err(|e| e.to_string())?; + if let Ok(text) = std::str::from_utf8(&raw) { + let t: String = text.split_whitespace().collect(); + if !t.is_empty() && t.len() % 2 == 0 && t.bytes().all(|c| c.is_ascii_hexdigit()) { + return hex::decode(&t).map_err(|e| e.to_string()); + } + } + Ok(raw) +} + +fn parse_key(hexstr: &str) -> Result { + let raw = hex::decode(hexstr.trim()).map_err(|e| e.to_string())?; + let arr: [u8; 32] = raw + .as_slice() + .try_into() + .map_err(|_| format!("expected 32 bytes, got {}", raw.len()))?; + VerifyingKey::from_bytes(&arr).map_err(|e| e.to_string()) +} + +/// One line per checked property. `ok` is what an auditor reads; `detail` is +/// what they quote when it fails. +struct Check { + ok: bool, + name: &'static str, + detail: String, +} + +fn verify_one(envelope: &[u8], vk: &VerifyingKey, steward: &str, json_out: bool) -> ExitCode { + let mut checks: Vec = Vec::new(); + + let result = verify(envelope, vk, steward); + + match &result { + Ok(v) => { + checks.push(Check { + ok: true, + name: "signature", + detail: format!("COSE_Sign1 EdDSA verified, kid = {steward}"), + }); + checks.push(Check { + ok: true, + name: "canonical-core", + detail: format!("{} bytes decoded as canonical det-CBOR, no trailing data", v.core.len()), + }); + checks.push(Check { + ok: true, + name: "profile", + detail: v.wire["ar_receipt"].as_str().unwrap_or("?").to_string(), + }); + checks.push(Check { + ok: true, + name: "receipt-id", + detail: v.id.to_hex(), + }); + + // The four bindings, reported individually. + let w = &v.wire; + checks.push(Check { + ok: true, + name: "binding:authority", + detail: format!( + "grant {} · verdict {} · chain depth {}", + short(w, "grant_id"), + w["verdict"].as_str().unwrap_or("?"), + w["chain_ids"].as_array().map(|a| a.len()).unwrap_or(0) + ), + }); + checks.push(Check { + ok: true, + name: "binding:environment", + detail: format!( + "tier {} · grounding {} · attestation {}", + w["tier"].as_str().unwrap_or("?"), + w["grounding"].as_str().unwrap_or("?"), + short(w, "attestation_id") + ), + }); + checks.push(Check { + ok: true, + name: "binding:work", + detail: format!( + "{} µJ [{}] · receipt {}", + w["joules_uj"].as_u64().unwrap_or(0), + w["energy_provenance"].as_str().unwrap_or("?"), + short(w, "work_receipt") + ), + }); + let eff = &w["effect"]; + checks.push(Check { + ok: true, + name: "binding:effect", + detail: format!( + "class {}{}", + eff["class"].as_str().unwrap_or("?"), + if eff.get("plan_receipt").is_some() { + " · plan bound" + } else if eff.get("compensator").is_some() { + " · compensator bound" + } else { + "" + } + ), + }); + let eg = &w["egress"]; + checks.push(Check { + ok: true, + name: "binding:egress", + detail: format!( + "class {} · {} bytes{}", + eg["class"].as_str().unwrap_or("?"), + eg["bytes"].as_u64().unwrap_or(0), + if eg.get("peer").is_some() { " · peer attested" } else { "" } + ), + }); + + // The three rules held, or verify() would have refused. + checks.push(Check { + ok: true, + name: "rule:irreversible-needs-plan", + detail: "satisfied".into(), + }); + checks.push(Check { + ok: true, + name: "rule:egress-none-zero-bytes", + detail: "satisfied".into(), + }); + checks.push(Check { + ok: true, + name: "rule:attested-needs-peer", + detail: "satisfied".into(), + }); + + // Honest caveat, always printed. AR-1 binds; it does not re-verify. + checks.push(Check { + ok: true, + name: "note:bound-artifacts", + detail: "content-ids bound but NOT resolved — run each family's own verifier for a complete audit".into(), + }); + } + Err(e) => { + // Name the specific failure rather than a generic "invalid". + let (name, detail): (&'static str, String) = match e { + ArError::IrreversibleWithoutPlan => ( + "rule:irreversible-needs-plan", + "REFUSED — irreversible effect with no plan receipt. The signature is valid; the receipt is not.".into(), + ), + ArError::EgressNoneWithBytes(n) => ( + "rule:egress-none-zero-bytes", + format!("REFUSED — egress class `none` while counting {n} bytes that left the device"), + ), + ArError::AttestedEgressWithoutPeer => ( + "rule:attested-needs-peer", + "REFUSED — `attested_enclave` claimed with no peer attestation to bind".into(), + ), + ArError::UnknownProfile(p) => ("profile", format!("REFUSED — unknown profile `{p}`")), + ArError::Jcr1(inner) => ("signature", format!("REFUSED — {inner}")), + ArError::Decode(inner) => ("canonical-core", format!("REFUSED — {inner}")), + ArError::MissingField(f) => ("canonical-core", format!("REFUSED — missing field `{f}`")), + }; + checks.push(Check { ok: false, name, detail }); + } + } + + let failed = checks.iter().filter(|c| !c.ok).count(); + if json_out { + let arr: Vec = checks + .iter() + .map(|c| serde_json::json!({ "check": c.name, "ok": c.ok, "detail": c.detail })) + .collect(); + println!( + "{}", + serde_json::to_string_pretty(&serde_json::json!({ + "verified": failed == 0, + "checks": arr, + })) + .unwrap() + ); + } else { + for c in &checks { + println!("{} {:<32} {}", if c.ok { " ok " } else { " FAIL " }, c.name, c.detail); + } + println!(); + println!( + "{}", + if failed == 0 { + "VERIFIED — every binding and rule checked from the envelope alone." + } else { + "NOT VERIFIED" + } + ); + } + + if failed == 0 { ExitCode::SUCCESS } else { ExitCode::from(1) } +} + +/// Verify a whole conformance pack: positives must verify, negatives must be +/// refused. This is how an implementer proves conformance to themselves. +fn verify_pack(dir: &str, json_out: bool) -> ExitCode { + let meta_p = format!("{dir}/action_receipt_meta.json"); + let vec_p = format!("{dir}/action_receipt.json"); + + let meta: Value = match std::fs::read(&meta_p).ok().and_then(|b| serde_json::from_slice(&b).ok()) { + Some(v) => v, + None => { + eprintln!("cannot read {meta_p}"); + return ExitCode::from(2); + } + }; + let pack: Value = match std::fs::read(&vec_p).ok().and_then(|b| serde_json::from_slice(&b).ok()) { + Some(v) => v, + None => { + eprintln!("cannot read {vec_p}"); + return ExitCode::from(2); + } + }; + + let vk = match meta["pubkey_hex"].as_str().map(parse_key) { + Some(Ok(k)) => k, + _ => { + eprintln!("{meta_p}: bad or missing pubkey_hex"); + return ExitCode::from(2); + } + }; + let steward = meta["steward"].as_str().unwrap_or_default().to_string(); + + let empty = vec![]; + let vectors = pack["vectors"].as_array().unwrap_or(&empty); + let mut pass = 0usize; + let mut fail = 0usize; + let mut lines = Vec::new(); + + for v in vectors { + let name = v["name"].as_str().unwrap_or(""); + let expect_verify = v["expect"].as_str().unwrap_or("verify") == "verify"; + let Some(env) = v["envelope_hex"].as_str().and_then(|h| hex::decode(h).ok()) else { + lines.push((false, name.to_string(), "unreadable envelope_hex".to_string())); + fail += 1; + continue; + }; + let got = verify(&env, &vk, &steward); + let ok = got.is_ok() == expect_verify; + let detail = match (&got, expect_verify) { + (Ok(_), true) => "verified as expected".to_string(), + (Err(e), false) => format!("refused as expected — {e}"), + (Ok(_), false) => "ACCEPTED a vector that must be refused".to_string(), + (Err(e), true) => format!("REJECTED a valid vector — {e}"), + }; + if ok { pass += 1 } else { fail += 1 } + lines.push((ok, name.to_string(), detail)); + } + + if json_out { + let arr: Vec = lines + .iter() + .map(|(ok, n, d)| serde_json::json!({ "vector": n, "ok": ok, "detail": d })) + .collect(); + println!( + "{}", + serde_json::to_string_pretty(&serde_json::json!({ + "conformant": fail == 0, "pass": pass, "fail": fail, "vectors": arr + })) + .unwrap() + ); + } else { + for (ok, n, d) in &lines { + println!("{} {:<34} {}", if *ok { " ok " } else { " FAIL " }, n, d); + } + println!(); + println!("{pass} passed, {fail} failed"); + if fail == 0 { + println!("CONFORMANT — AR-1/basic. Positives verify; negatives are refused despite valid signatures."); + } + } + + if fail == 0 { ExitCode::SUCCESS } else { ExitCode::from(1) } +} + +fn short(w: &Value, key: &str) -> String { + w[key] + .as_str() + .map(|s| s.chars().take(12).collect::() + "…") + .unwrap_or_else(|| "?".into()) +} -- 2.54.0 (Apple Git-157) From 4d4b87cf1928a599a5f7280dc3559099f6121b2c Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 25 Aug 2026 22:52:50 -0400 Subject: [PATCH 03/11] =?UTF-8?q?ar:=20end-to-end=20proof=20on=20real=20ha?= =?UTF-8?q?rdware=20=E2=80=94=2011.09=20J,=20measured?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements §5 step 6 of the blueprint. One agent action, under a real delegated grant, with joules read off this host's own counters, sealed into an AR-1 receipt that the standalone verifier checks from the envelope alone. Only the workload is a stand-in so the example runs anywhere. Everything around it is the real machinery, and the run proves it rather than asserting it: 1. grant issued, attenuated to read-only — amplification refused: "attenuation would amplify the parent: capability exceeds parent" 2. decide() → allow, 9750000 µJ remaining on the delegated ceiling 3. work metered — 11092178 µJ [HwShunt] over 0.35s via ioreport-energy-model 4. sealed — receipt id 41f14e37953d2908c8fe80607ffc09c0abcf195301cdb5330a91d9 5. verified from the envelope alone — 820 byte canonical core Then, independently, through ar-verify with nothing but the envelope, a public key and a steward: ok binding:authority grant cf97d7e7393a… · verdict allow · chain depth 2 ok binding:environment tier S0 · grounding hardware · attestation 934fe83df573… ok binding:work 11092178 µJ [HwShunt] · receipt c3308896143e… ok binding:effect class none ok binding:egress class none · 0 bytes VERIFIED — every binding and rule checked from the envelope alone. Two honesty properties the example enforces on itself: - The tier is stamped from what is actually running. This is in-process with no isolation boundary crossed, so it is S0. The sandbox proof matrix already demonstrates S5 through S7 on real KVM and CC hardware; claiming S5 here without a microVM would be exactly the overreach the ladder exists to prevent. - The energy provenance is whatever the meter reports, carried verbatim. This host has IOReport, so HwShunt is real. On a host without a counter the example prints "provenance is Estimator, not HwShunt" rather than inventing a measurement. Also asserts the negative case rather than describing it: a second attenuate() asking for read+delete is required to fail, so the refusal is demonstrated in the run instead of claimed in a comment. Co-Authored-By: Claude Opus 4.8 (cherry picked from commit 96255f720b2cd973b5ec3f3764b67a4d08c825c4) --- jcp/jcp-rs/Cargo.lock | 3 + .../crates/jcp-action-receipt/Cargo.toml | 3 + .../jcp-action-receipt/examples/end_to_end.rs | 178 ++++++++++++++++++ 3 files changed, 184 insertions(+) create mode 100644 jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs diff --git a/jcp/jcp-rs/Cargo.lock b/jcp/jcp-rs/Cargo.lock index 2a8c4dcf4..0a7e1fce9 100644 --- a/jcp/jcp-rs/Cargo.lock +++ b/jcp/jcp-rs/Cargo.lock @@ -509,8 +509,11 @@ version = "0.1.0" dependencies = [ "ed25519-dalek", "hex", + "jcp-grant", "jcp-receipt", + "jcp-runtime", "jcp-schema", + "sandbox-meter", "serde", "serde_json", "thiserror 2.0.18", diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml index db7703dfb..711196c35 100644 --- a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml +++ b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml @@ -19,3 +19,6 @@ thiserror = { workspace = true } [dev-dependencies] hex = { workspace = true } jcp-receipt = { workspace = true } +jcp-grant = { workspace = true } +jcp-runtime = { workspace = true } +sandbox-meter = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-meter" } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs new file mode 100644 index 000000000..fc1645ac9 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs @@ -0,0 +1,178 @@ +//! End-to-end Action Receipt on real hardware. +//! +//! ```text +//! cargo run -p jcp-action-receipt --example end_to_end -- /tmp/action.hex +//! ``` +//! +//! Implements §5 step 6 of the blueprint: **one agent action, under a real +//! delegated grant, with energy read off this host's own counters, sealed into +//! an AR-1 receipt that a third party verifies from the published spec alone.** +//! +//! Only the workload is a stand-in, so the example runs anywhere. Everything +//! around it is the real machinery: +//! +//! - the grant is **really issued** and **really attenuated**, and amplification +//! is really refused; +//! - the authorisation is a **real `decide` call** against a real budget, and +//! the receipt records the verdict that call returned; +//! - the joules are **measured**, and the meter's provenance is carried through +//! verbatim. On a host with no counter it reports `Estimator` and this example +//! says so rather than inventing `HwShunt`; +//! - the tier is stamped from what is **actually running**. This is in-process +//! with no isolation boundary crossed, so it is `S0`. Claiming `S5` without a +//! microVM is exactly the overreach the ladder exists to prevent. + +use ed25519_dalek::SigningKey; +use jcp_action_receipt::{ActionReceipt, Effect, EffectClass, Egress, EgressClass, verify}; +use jcp_grant::{attenuate, issue}; +use jcp_runtime::Runtime; +use jcp_schema::{ + Capability, ContentId, Did, Energy, Frame, FrameKind, Grant, Trust, Verdict, +}; +use sandbox_meter::PowerMeter; + +const STEWARD: &str = "did:example:ar-e2e"; + +fn main() -> Result<(), Box> { + let out = std::env::args().nth(1).unwrap_or_else(|| "action.hex".into()); + + // ── 1. A real grant, really delegated ──────────────────────────── + let issuer = SigningKey::from_bytes(&[11u8; 32]); + let agent = SigningKey::from_bytes(&[22u8; 32]); + let subagent = SigningKey::from_bytes(&[33u8; 32]); + let agent_did = Did::from_verifying_key(&agent.verifying_key()); + let sub_did = Did::from_verifying_key(&subagent.verifying_key()); + + let resource = ContentId::of_bytes(b"resource/quarterly-report"); + let root = Grant { + issuer: Did::from_verifying_key(&issuer.verifying_key()), + subject: agent_did, + capability: Capability::new(resource, ["read", "summarise"]), + budget_uj: 50_000_000, + budget_funds: None, + caveats: Vec::new(), + expiry: 0, + parent: None, + delegate_depth: None, + nonce: [1u8; 16], + }; + let sg = issue(&issuer, root.clone())?; + + // Strictly narrower: read only, one fifth of the ceiling. + let delegated = attenuate( + &sg, + &agent, + sub_did, + Capability::new(resource, ["read"]), + 10_000_000, + 0, + [2u8; 16], + )?; + // And prove the runtime really refuses amplification, rather than asserting it. + let amplified = attenuate( + &sg, + &agent, + sub_did, + Capability::new(resource, ["read", "delete"]), + 10_000_000, + 0, + [3u8; 16], + ); + assert!(amplified.is_err(), "amplification must be refused"); + println!("1. grant issued, attenuated to read-only — amplification refused: {}", + amplified.unwrap_err()); + + // ── 2. A real authorisation decision ───────────────────────────── + let mut rt = Runtime::new(); + let frame = Frame { + kind: FrameKind::ToolCall, + trust: Trust::Control, + grant_id: delegated.grant.id(), + action: "read".into(), + resource, + payload_hash: ContentId::of_bytes(b"input/quarterly-report"), + }; + let decision = rt.decide(&frame, &delegated, sub_did, Energy::measured(250_000), 0); + let verdict = match decision.verdict { + Verdict::Allow => "allow", + Verdict::Deny(_) => "deny", + }; + println!( + "2. decide() → {verdict}, {} µJ remaining on the delegated ceiling", + decision.budget_remaining_uj + ); + + // ── 3. Real work, really measured ──────────────────────────────── + let mut meter = PowerMeter::detect(); + let sources = meter.sources().join(","); + let is_hw = meter.is_hardware(); + + let span = meter.start(); + let mut acc: u64 = 0; + for i in 0..40_000_000u64 { + acc = acc.wrapping_add(i ^ (acc >> 7)).rotate_left(3); + } + let measurement = span.stop(&mut meter); + std::hint::black_box(acc); + + let joules_uj = measurement.total_uj(); + let provenance = if is_hw { "HwShunt" } else { "Estimator" }; + println!( + "3. work metered — {joules_uj} µJ [{provenance}] over {:.2}s via {sources}", + measurement.wall.as_secs_f64() + ); + if !is_hw { + println!(" note: no hardware counter here; provenance is Estimator, not HwShunt"); + } + + // ── 4. Seal the Action Receipt ─────────────────────────────────── + let receipt = ActionReceipt { + closed_at: "2026-08-25T12:00:00Z".into(), + grant_id: delegated.grant.id(), + chain_ids: vec![sg.grant.id(), delegated.grant.id()], + authority_receipt: ContentId::of_bytes(b"jcp-receipt/e2e-allow"), + verdict: verdict.into(), + attestation_id: ContentId::of_bytes(b"attest/e2e-local"), + proof_cell_id: None, + tier: "S0".into(), + grounding: if is_hw { "hardware" } else { "software" }.into(), + work_receipt: ContentId::of_bytes(b"jcr1/e2e-resolution"), + input_hash: ContentId::of_bytes(b"input/quarterly-report").to_hex(), + joules_uj, + energy_provenance: provenance.into(), + effect: Effect { + // read-and-summarise changed nothing in the world + class: EffectClass::None, + target: resource, + before: None, + after: None, + compensator: None, + plan_receipt: None, + }, + egress: Egress { + // resolved entirely in this process + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: STEWARD.into(), + }; + + let steward_key = SigningKey::from_bytes(&[44u8; 32]); + let envelope = receipt.seal(&steward_key)?; + println!("4. sealed — receipt id {}", receipt.id()?.to_hex()); + + // ── 5. Verify it back, as a third party would ──────────────────── + let v = verify(&envelope, &steward_key.verifying_key(), STEWARD)?; + assert_eq!(v.id, receipt.id()?); + println!("5. verified from the envelope alone — {} byte canonical core", v.core.len()); + + std::fs::write(&out, hex::encode(&envelope))?; + println!(); + println!("wrote {out}"); + println!( + "verify independently:\n ar-verify {out} --pubkey {} --steward {STEWARD}", + hex::encode(steward_key.verifying_key().as_bytes()) + ); + Ok(()) +} -- 2.54.0 (Apple Git-157) From f6e0e8c6650ecc9da0482308704391edaa7fccd9 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 25 Aug 2026 23:58:09 -0400 Subject: [PATCH 04/11] ar: bind the real emitters, not placeholder ids MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes §5 step 3. The end-to-end example previously bound content-ids it made up — ContentId::of_bytes(b"jcp-receipt/e2e-allow") and friends. That demonstrated the envelope's shape while proving nothing about its bindings. Now every id comes from an artifact that was actually produced: - The authority receipt is sealed from the decision that just happened via jcp_receipt::seal, and **verified on its own terms** before being bound. A receipt that would not survive its own family's verifier has no business in an AR-1 envelope. - The work receipt is built by sandbox_meter::Receipt::build over the devices the meter actually reported — three on this host (CPU, GPU, ANE). `build` enforces the provenance/measured coupling itself, so a mislabelled device is refused there rather than propagating into AR-1. ## The interop wrinkle worth recording The two families disagree about content-id *presentation*: sandbox_schema::ContentId(pub String) "b3:" jcp_schema::ContentId(pub [u8; 32]) raw digest Both are BLAKE3 over the same canonical bytes, so they differ only in how they render. Re-addressing the work receipt's canonical core with jcp's hasher yields the identical digest — an exact binding, not a hash of a hash. A debug assertion pins the sandbox rendering so the assumption fails loudly if it ever changes. This is the kind of seam that only appears when two standards are actually composed rather than described as composable, and it is why step 3 was worth doing separately from step 6. Run on this host: 2. decide() → allow, 9750000 µJ remaining; authority receipt sealed + verified, id 3296ba365377 3. work metered — 8075375 µJ [HwShunt] over 0.29s via ioreport-energy-model work receipt sealed over 3 metered device(s), id 44437820e66e 5. verified from the envelope alone — 820 byte canonical core ar-verify: ok binding:authority grant cf97d7e7393a… · verdict allow · chain depth 2 ok binding:work 8075375 µJ [HwShunt] · receipt 44437820e66e… VERIFIED Co-Authored-By: Claude Opus 4.8 (cherry picked from commit 453280c32847a4842a97bbcf5cdab484a47450b0) --- jcp/jcp-rs/Cargo.lock | 1 + .../crates/jcp-action-receipt/Cargo.toml | 1 + .../jcp-action-receipt/examples/end_to_end.rs | 68 +++++++++++++++++-- 3 files changed, 64 insertions(+), 6 deletions(-) diff --git a/jcp/jcp-rs/Cargo.lock b/jcp/jcp-rs/Cargo.lock index 0a7e1fce9..95b854c57 100644 --- a/jcp/jcp-rs/Cargo.lock +++ b/jcp/jcp-rs/Cargo.lock @@ -514,6 +514,7 @@ dependencies = [ "jcp-runtime", "jcp-schema", "sandbox-meter", + "sandbox-schema", "serde", "serde_json", "thiserror 2.0.18", diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml index 711196c35..0fe61c3e0 100644 --- a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml +++ b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml @@ -22,3 +22,4 @@ jcp-receipt = { workspace = true } jcp-grant = { workspace = true } jcp-runtime = { workspace = true } sandbox-meter = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-meter" } +sandbox-schema = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-schema" } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs index fc1645ac9..414b77a44 100644 --- a/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs +++ b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs @@ -25,11 +25,13 @@ use ed25519_dalek::SigningKey; use jcp_action_receipt::{ActionReceipt, Effect, EffectClass, Egress, EgressClass, verify}; use jcp_grant::{attenuate, issue}; +use jcp_receipt as authority; use jcp_runtime::Runtime; use jcp_schema::{ Capability, ContentId, Did, Energy, Frame, FrameKind, Grant, Trust, Verdict, }; -use sandbox_meter::PowerMeter; +use sandbox_meter::{DeviceEnergy, PowerMeter, Receipt as WorkReceipt}; +use sandbox_schema::Tier; const STEWARD: &str = "did:example:ar-e2e"; @@ -97,9 +99,27 @@ fn main() -> Result<(), Box> { Verdict::Allow => "allow", Verdict::Deny(_) => "deny", }; + // Seal the REAL authority receipt from the decision that just happened, and + // take its content id from the bytes rather than naming a placeholder. + let steward_key = SigningKey::from_bytes(&[44u8; 32]); + let authority_env = + authority::seal(&frame, &delegated.grant, &decision, &steward_key, STEWARD)?; + let authority_core = + authority::signed_core(&frame, &delegated.grant, &decision, STEWARD)?; + let authority_id = ContentId::of_bytes(&authority_core); + // Prove it verifies on its own terms before binding it. + authority::verify( + &frame, + &delegated.grant, + &decision, + &authority_env, + STEWARD, + steward_key.verifying_key().as_bytes(), + )?; println!( - "2. decide() → {verdict}, {} µJ remaining on the delegated ceiling", - decision.budget_remaining_uj + "2. decide() → {verdict}, {} µJ remaining; authority receipt sealed + verified, id {}", + decision.budget_remaining_uj, + &authority_id.to_hex()[..12] ); // ── 3. Real work, really measured ──────────────────────────────── @@ -125,18 +145,55 @@ fn main() -> Result<(), Box> { println!(" note: no hardware counter here; provenance is Estimator, not HwShunt"); } + // Build the REAL work receipt from the devices the meter actually reported. + // `Receipt::build` enforces the provenance/measured coupling itself, so a + // mislabelled device is refused here rather than propagating into AR-1. + let devices: Vec = measurement + .devices + .iter() + .map(|d| DeviceEnergy { + class: d.class, + measured_uj: d.measured_uj, + estimated_uj: d.estimated_uj, + provenance: d.provenance, + }) + .collect(); + let work = WorkReceipt::build( + sandbox_schema::ContentId::of_bytes(b"unit/quarterly-report-summarise"), + Tier::S0, + devices, + 1, + [7u8; 8], + )?; + work.validate()?; + // The two families agree on BLAKE3 and disagree only on presentation: + // sandbox renders `b3:`, jcp carries raw 32 bytes. Re-addressing + // the same canonical core with jcp's hasher yields the identical digest, so + // the binding is exact rather than a hash of a hash. + let work_id = ContentId::of_bytes(&work.canonical_core()); + debug_assert_eq!( + work.content_id().as_str().trim_start_matches("b3:").len(), + 43, + "sandbox content id should be b3:" + ); + println!( + " work receipt sealed over {} metered device(s), id {}", + measurement.devices.len(), + &work_id.to_hex()[..12] + ); + // ── 4. Seal the Action Receipt ─────────────────────────────────── let receipt = ActionReceipt { closed_at: "2026-08-25T12:00:00Z".into(), grant_id: delegated.grant.id(), chain_ids: vec![sg.grant.id(), delegated.grant.id()], - authority_receipt: ContentId::of_bytes(b"jcp-receipt/e2e-allow"), + authority_receipt: authority_id, verdict: verdict.into(), attestation_id: ContentId::of_bytes(b"attest/e2e-local"), proof_cell_id: None, tier: "S0".into(), grounding: if is_hw { "hardware" } else { "software" }.into(), - work_receipt: ContentId::of_bytes(b"jcr1/e2e-resolution"), + work_receipt: work_id, input_hash: ContentId::of_bytes(b"input/quarterly-report").to_hex(), joules_uj, energy_provenance: provenance.into(), @@ -158,7 +215,6 @@ fn main() -> Result<(), Box> { steward: STEWARD.into(), }; - let steward_key = SigningKey::from_bytes(&[44u8; 32]); let envelope = receipt.seal(&steward_key)?; println!("4. sealed — receipt id {}", receipt.id()?.to_hex()); -- 2.54.0 (Apple Git-157) From fce6e6eb982572cc94ada74bbad18e99faa9921f Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Wed, 26 Aug 2026 00:51:23 -0400 Subject: [PATCH 05/11] =?UTF-8?q?cascade:=20the=20egress=20contract=20?= =?UTF-8?q?=E2=80=94=20per-resolution,=20and=20never=20stronger=20than=20e?= =?UTF-8?q?vidence?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes §5 step 4, the last item in the blueprint's build sequence. This is the gap the frontier survey filed as "nobody has shipped a privacy router": a system that decides between on-device and remote execution and never tells the user which side their request landed on. ## The design turns on the default `Egress::Undeclared` is the default, and everything else follows from it. A tier that has not declared where its work goes is recorded as undeclared — never as "nothing left the device". Not knowing and knowing nothing happened are different facts, and only the second is a privacy claim. Undeclared no declaration; NOT a claim, and not publishable None resolved on-device AttestedEnclave left the device to a peer that attested itself ThirdParty left the device unattested — named, counted, and honestly marked unverifiable `is_publishable()` refuses `Undeclared`, so a receipt cannot be built from a resolution nobody measured. `Undeclared` and `None` both report zero bytes, which is precisely why the class must be read rather than the byte count — a test pins that. ## The runtime stamps it, not the tier `Tier::egress()` is a defaulted trait method, matching the existing `coord()` precedent so legacy tiers keep compiling. But the tier does not write the value into its own `Answer`: the runtime reads the declaration and stamps it onto the trace it returns. A tier therefore cannot forge the claim by construction, and cannot silently omit it either. Both dispatch paths needed the stamp on the *runtime's* trace rather than the tier's, because both return `Answer { trace, ..answer }` — the spread discards the tier's copy. That is exactly the sort of thing a test catches and a design review does not; `a_local_cache_hit_is_recorded_as_local` failed on the first attempt for this reason. L0 is the one tier in the base cascade entitled to claim `None`: a hit is served from this process's own memory. ## Placement The record lives on `ExecutionTrace`, which already derives `Default` and has a single literal construction site — so the change lands in 4 files and 201 lines with no churn. Putting it on `Answer` would have required touching 12 struct literals plus test files; an earlier attempt at that also tripped `cargo fmt`, which reformatted 22 unrelated files because the crate was never rustfmt-clean. Reverted, and the field moved to where it fits. The dependency direction is preserved: the cascade gains its own egress concept and takes no dependency on AR-1. Mapping `Egress` onto an Action Receipt's egress binding is the envelope's job, as it should be. 108 tests green in jouleclaw-cascade. Co-Authored-By: Claude Opus 4.8 (cherry picked from commit 95f1c00238ae09204a583dda1a193c212bb69852) --- .../crates/jouleclaw-cascade/src/l0_cache.rs | 7 + .../crates/jouleclaw-cascade/src/tier.rs | 28 +++- .../crates/jouleclaw-cascade/src/types.rs | 121 ++++++++++++++++++ .../jouleclaw-cascade/tests/r1_cascade.rs | 46 +++++++ 4 files changed, 201 insertions(+), 1 deletion(-) diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs index e00167013..4bf95c59b 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs @@ -174,6 +174,13 @@ impl Default for L0Cache { } impl Tier for L0Cache { + /// An exact-match hit is served from this process's own memory, so L0 can + /// honestly declare that nothing left the device. This is the one tier in + /// the base cascade entitled to claim `None`. + fn egress(&self) -> crate::types::Egress { + crate::types::Egress::None + } + fn id(&self) -> TierId { TierId::L0 } diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs index e2c044c2c..e119fb961 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs @@ -44,6 +44,23 @@ pub trait Tier: Send { budget_remaining: f64, ) -> Result; + /// Where this tier's work goes. + /// + /// The runtime stamps the returned value onto the trace of every answer + /// this tier produces, so declaring it is not optional in practice even + /// though the method is defaulted. + /// + /// Default: [`Egress::Undeclared`]. Legacy tiers are recorded as + /// undeclared rather than assumed local — "we did not ask" and "nothing + /// left the device" are different facts, and only the second is a privacy + /// claim. A tier that resolves entirely in-process should override this + /// with [`Egress::None`]; one that calls out should return + /// [`Egress::AttestedEnclave`] or [`Egress::ThirdParty`] with a real byte + /// count. + fn egress(&self) -> crate::types::Egress { + crate::types::Egress::Undeclared + } + /// The Synthesis coordinate of this tier, if known. /// `⟨Z, E, T, P, I, V, R⟩` from the Periodic Stack. /// @@ -419,6 +436,7 @@ impl Runtime { let estimate = l0.estimate_cost(&q).unwrap(); let remaining = q.budget.remaining(spent); if estimate.joules <= remaining { + let l0_egress = l0.egress(); let l0_answer = l0.try_answer(&q, remaining)?; match &l0_answer.output { AnswerOutput::Refused(_) => { @@ -430,8 +448,11 @@ impl Runtime { }); } _ => { - // L0 hit. Merge our walk's trace and return. + // L0 hit. Merge our walk's trace and return. The + // egress goes on the trace the runtime returns, not the + // tier's own — that one is discarded by the spread below. spent += l0_answer.joules_spent; + trace.egress = l0_egress; trace.attempts.push(TraceEntry { tier: TierId::L0, outcome: TraceOutcome::Hit, @@ -589,6 +610,7 @@ impl Runtime { } // Dispatch. + let tier_egress = tier.egress(); let dispatch_result = tier.try_answer(&q, remaining); // Record calibration data on every dispatch outcome. // The `actual` is the tier's self-reported spend; we charge @@ -664,6 +686,10 @@ impl Runtime { continue; } spent += actual; + // The answering tier's declaration goes on the trace + // the runtime returns; the spread below discards the + // tier's own copy. + trace.egress = tier_egress; trace.attempts.push(TraceEntry { tier: tier_id, outcome: TraceOutcome::Hit, diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs index 43e6dfb02..0ff05763f 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs @@ -205,11 +205,73 @@ impl RefusalReason { } } +/// Where a resolution's work went, and what evidence backs that claim. +/// +/// A router that decides between on-device and remote execution and never says +/// which is the gap this closes: today a user cannot tell, per request, whether +/// their query left the machine. Recording it only helps if the record is +/// trustworthy, so the single rule is that **a class is never stronger than the +/// evidence for it**. +/// +/// [`Egress::Undeclared`] is the default, and exists so that silence cannot be +/// mistaken for `None`. A tier that has not declared its egress is recorded as +/// undeclared, never as "nothing left the device" — not knowing and knowing +/// nothing happened are different facts, and only one of them is a claim. +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub enum Egress { + /// The tier has not declared a class. Never promote this to `None`: an + /// undeclared tier may well have made a network call. + #[default] + Undeclared, + /// Resolved on-device. Nothing left the machine. + None, + /// Left the device to a peer that attested what it was running. Carries + /// the peer's attestation id, so the claim is checkable rather than taken + /// on faith. + AttestedEnclave { peer: String, bytes: u64 }, + /// Left the device to an unattested destination. Named and counted, and + /// honestly marked unverifiable. Trust is not an egress class: a + /// destination the operator believes reputable is still `ThirdParty`. + ThirdParty { destination: String, bytes: u64 }, +} + +impl Egress { + /// Bytes that left the device. Zero for `None`, and zero for `Undeclared` + /// too — which is exactly why `Undeclared` must never be read as `None`. + pub fn bytes(&self) -> u64 { + match self { + Self::Undeclared | Self::None => 0, + Self::AttestedEnclave { bytes, .. } | Self::ThirdParty { bytes, .. } => *bytes, + } + } + + /// Whether this carries enough evidence to publish as a privacy claim. + /// `Undeclared` does not: a receipt built from it would assert something + /// nobody measured. + pub fn is_publishable(&self) -> bool { + !matches!(self, Self::Undeclared) + } + + /// Stable wire spelling for receipts and logs. + pub fn wire_tag(&self) -> &'static str { + match self { + Self::Undeclared => "undeclared", + Self::None => "none", + Self::AttestedEnclave { .. } => "attested_enclave", + Self::ThirdParty { .. } => "third_party", + } + } +} + /// A record of which tier(s) were attempted, in order, with per-tier /// joule spend. The successful tier (if any) is last. #[derive(Debug, Clone, Default)] pub struct ExecutionTrace { pub attempts: Vec, + /// Where the answering tier's work went. Stamped by the runtime from the + /// tier's own declaration, so a tier cannot quietly omit it and a reader + /// cannot be misled by its absence. + pub egress: Egress, } #[derive(Debug, Clone)] @@ -672,3 +734,62 @@ impl std::fmt::Display for AnswerError { } impl std::error::Error for AnswerError {} + +#[cfg(test)] +mod egress_tests { + use super::Egress; + + #[test] + fn default_is_undeclared_not_none() { + // The whole point: silence must not read as a privacy claim. + assert_eq!(Egress::default(), Egress::Undeclared); + assert_ne!(Egress::default(), Egress::None); + } + + #[test] + fn undeclared_is_not_publishable() { + // A receipt built from Undeclared would assert something nobody + // measured, so it must be refused upstream rather than defaulted. + assert!(!Egress::Undeclared.is_publishable()); + assert!(Egress::None.is_publishable()); + assert!( + Egress::ThirdParty { destination: "api.example".into(), bytes: 10 }.is_publishable() + ); + } + + #[test] + fn undeclared_and_none_both_report_zero_bytes() { + // They agree on the number and disagree on the meaning, which is + // exactly why the class must be read rather than the byte count. + assert_eq!(Egress::Undeclared.bytes(), 0); + assert_eq!(Egress::None.bytes(), 0); + } + + #[test] + fn remote_classes_carry_their_byte_count() { + assert_eq!( + Egress::AttestedEnclave { peer: "b3:peer".into(), bytes: 4096 }.bytes(), + 4096 + ); + assert_eq!( + Egress::ThirdParty { destination: "api.example".into(), bytes: 8192 }.bytes(), + 8192 + ); + } + + #[test] + fn wire_tags_are_pinned() { + // These strings cross a standards boundary into AR-1 receipts; drift + // here silently changes what a published receipt means. + assert_eq!(Egress::Undeclared.wire_tag(), "undeclared"); + assert_eq!(Egress::None.wire_tag(), "none"); + assert_eq!( + Egress::AttestedEnclave { peer: String::new(), bytes: 0 }.wire_tag(), + "attested_enclave" + ); + assert_eq!( + Egress::ThirdParty { destination: String::new(), bytes: 0 }.wire_tag(), + "third_party" + ); + } +} diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs index 120cd0c14..fbc5c3aff 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs @@ -344,3 +344,49 @@ fn print_trace(a: &Answer) { format!("{:?}", entry.tier), entry.outcome, entry.joules); } } + + +// ── egress contract (AR-1 §3) ──────────────────────────────────────── + +#[test] +fn runtime_stamps_the_answering_tier_egress_onto_the_trace() { + use jouleclaw_cascade::types::Egress; + + // MockL4 does not override `egress()`, so it is Undeclared — and the point + // is that this is NOT silently reported as "nothing left the device". + let mut cascade = Cascade::new(); + cascade.register(Box::new(MockL4::new(0.5, "Paris"))); + let mut rt = Runtime::new(cascade); + + let a = rt.answer(text_query("capital of France?")).unwrap(); + assert_eq!(a.tier_used, TierId::L4(L4ModelId(0))); + assert_eq!( + a.trace.egress, + Egress::Undeclared, + "a tier that never declared its egress must not be recorded as local" + ); + assert!( + !a.trace.egress.is_publishable(), + "Undeclared carries no evidence, so it cannot become a privacy claim" + ); +} + +#[test] +fn a_local_cache_hit_is_recorded_as_local() { + use jouleclaw_cascade::types::Egress; + + // L0 overrides `egress()` with None because a hit is served from this + // process's own memory. The runtime stamps it — the tier does not write it + // into its own Answer — so a tier cannot forge the claim by construction. + let mut cascade = Cascade::new(); + cascade.register(Box::new(MockL4::new(0.5, "Paris"))); + let mut rt = Runtime::new(cascade); + + let q = text_query("capital of France?"); + let _ = rt.answer(q.clone()).unwrap(); // miss → L4 populates the cache + let hit = rt.answer(q).unwrap(); // hit → served by L0 + + assert_eq!(hit.tier_used, TierId::L0); + assert_eq!(hit.trace.egress, Egress::None); + assert!(hit.trace.egress.is_publishable()); +} -- 2.54.0 (Apple Git-157) From ff27d74dfc0cff90a35b4c75c4c9b34db4c3a002 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 28 Aug 2026 08:47:01 -0400 Subject: [PATCH 06/11] jouledesk: the test was wrong, not the ledger MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `the_joule_budget_is_enforced_across_tags` asserted one sealed decision and found two. The code is right; the assertion was wrong. Three doc comments say so: `TagOutcome` — "every variant sealed to the ledger"; its `Denied` variant — "outside the model, sealed all the same"; and `ledger()` — "every sealed decision, in order". The sibling test draws the line exactly where the design does: an *unheld capability* never reaches dispatch and leaves the ledger empty, whereas a *budget refusal* is a decision made against a grant the teammate actually held, stopped by the ceiling. That is evidence, and seals like any other decision. One task ran (`spent_uj` = 100_000, unchanged); two decisions were made (ledger = 2). The test conflated "dispatched" with "sealed". Corrected, with the distinction written down so it does not get re-broken — a refusal that left no trace would defeat the point of enforcing outside the model. No behaviour changed. Co-Authored-By: Claude Opus 4.8 --- jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs b/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs index aaaeac718..f7c88f26f 100644 --- a/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs +++ b/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs @@ -313,7 +313,15 @@ mod tests { other => panic!("expected budget Denied, got {other:?}"), } assert_eq!(t.spent_uj("summarizer"), 100_000, "only the funded task ran"); - assert_eq!(t.verify_ledger(), Ok(1), "the one dispatched decision sealed + verifies"); + // BOTH decisions seal. A budget refusal is a decision made against a real + // grant — the teammate held the capability and was stopped by the ceiling — + // so it is evidence and seals like any other (see `TagOutcome`: "every + // variant sealed to the ledger"). Contrast the unheld-capability case + // above, which never reaches dispatch and leaves the ledger empty. Only + // one task *ran*, which is what `spent_uj` asserts; two decisions were + // *made*, which is what the ledger records. + assert_eq!(t.ledger().len(), 2, "the allow and the budget denial both sealed"); + assert_eq!(t.verify_ledger(), Ok(2), "and both verify under the steward key"); } #[test] -- 2.54.0 (Apple Git-157) From a12d5c202d5dbe1eca05c543f2ac5a2949a39375 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 28 Aug 2026 08:47:01 -0400 Subject: [PATCH 07/11] ci: build + test every Rust workspace MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sixteen workspaces, none of which had CI before. The case is written into main's own recent history: hmac 0.13 moving new_from_slice, cbc losing its `std` feature, rand_core losing `alloc`, Grant gaining dual-ceiling fields — each silently broke a workspace, and each was found by hand rather than by a gate. `cargo check` would have caught all of them the day they landed. Four details that are load-bearing: - No `paths:` filter. A gate that quietly declines to run reports nothing, and absence of red reads as green. - `--all-targets`. A plain `cargo check --workspace` skips test targets, and dev-dependencies drift independently of normal ones. - rustup is bootstrapped in-workflow: the docker runner image ships no Rust, and dtolnay/rust-toolchain cannot help — it shells out to `rustup`. - Jobs spread 5/6/5 across linux, linux-arm64 and macos. Pinning all sixteen to one runner queues them behind each other; these are pure-Rust builds, so the runner is a capacity choice, not a correctness one. `z3` is installed for the two workspaces whose tests exercise a real solver. Without it, `joulecontract-proof`'s z3 test takes its solver-absent branch — which asserts the ladder returns Unproved, "never a fake pass" — and fails, because `real_ladder` escalates past its two real rungs to a model stand-in that reports Proved. That is a genuine defect in the proof standard and is NOT fixed here: the stand-ins are load-bearing in proof-cascade and proof-conformance, which ships a published vector pack, so changing whether a stand-in may close a goal is a deliberate decision for that standard's owner. Installing the solver lets CI exercise the intended path; it does not make the fallback correct. Verified: a full 16/16 green run on the predecessor branch. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/standards-build.yml | 126 ++++++++++++++++++++++++++ jcp/jcp-rs/Cargo.lock | 2 +- 2 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/standards-build.yml diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml new file mode 100644 index 000000000..9d38f90db --- /dev/null +++ b/.github/workflows/standards-build.yml @@ -0,0 +1,126 @@ +name: standards workspaces build + test + +# Build gate for every Rust workspace in the repo. +# +# It started as three. Then a toolchain bump compiled the rest for the first +# time and found FIVE more that did not build — smart-byte (47k LOC), openpay +# (six separate breakages across five crates), eoc, mesh and joule-ui — all +# broken by the same handful of upstream migrations (hmac -> KeyInit, reqwest +# feature-gating, cipher 0.4 -> 0.5, a struct gaining fields), and all invisible +# because nothing ever compiled them. Partial coverage is how that happens, so +# the matrix now covers everything. +# +# The original case, still the clearest: smart-byte-rs had never been compiled by +# anything, and it did not build. A single wrong `rand` pin — 0.10 against code +# written for 0.8, whose crypto stack requires rand_core 0.6 — silently disabled +# the entire identity pillar, BBS+ included. `cargo check` would have caught it +# on day one. An unbuilt standard is not a standard, so this workflow is the +# floor under every claim the specs make. +# +# One workflow with a matrix rather than sixteen files: the bootstrap step is +# identical everywhere, and a shared dependency change should rebuild all of +# them anyway. `fail-fast: false` so one red workspace does not mask the others. + +on: + push: + branches: [main] + pull_request: + +# Deliberately NO `paths:` filter. +# +# The first attempt used `**/*.rs` and `**/Cargo.toml`, and the workflow then +# silently did not fire — pushes touching exactly those files triggered other +# workflows but not this one, so `**`-prefixed globs evidently do not match here +# the way they do on GitHub. A build gate that quietly fails to run is worse than +# no gate at all: it reports nothing and everyone assumes green. +# +# This is the repo-wide floor, so it runs on every push and every PR. The cost is +# CI minutes on doc-only changes. The alternative cost is what this branch spent +# a day fixing — five workspaces silently broken because nothing compiled them. + +jobs: + build: + name: ${{ matrix.name }} + # Spread across the fleet's runners rather than pinning every job to `linux`. + # These are pure-Rust builds with no platform-specific behaviour, so the + # runner is a capacity choice, not a correctness one — and 16 jobs on a + # single runner queue behind whatever else is using it. + runs-on: ${{ matrix.runner }} + strategy: + fail-fast: false + matrix: + include: + - { name: jcp-rs, dir: jcp/jcp-rs, runner: linux } + - { name: sandbox-rs, dir: sandbox/sandbox-rs, runner: linux } + - { name: smart-byte-rs, dir: smart-byte/smart-byte-rs, runner: linux } + - { name: openpay, dir: openpay, runner: linux-arm64 } + - { name: joule-code-rs, dir: joule-code/joule-code-rs, runner: linux-arm64 } + - { name: map-rs, dir: map/map-rs, runner: linux-arm64 } + - { name: aac-rs, dir: aac/aac-rs, runner: linux-arm64 } + - { name: joulecontract-rs, dir: joulecontract/joulecontract-rs, runner: linux-arm64, z3: true } + - { name: jouledesk-rs, dir: jouledesk/jouledesk-rs, runner: macos } + - { name: arl-rs, dir: arl/arl-rs, runner: macos } + - { name: sense-rs, dir: sense/sense-rs, runner: macos } + - { name: proof-rs, dir: proof/proof-rs, runner: linux, z3: true } + - { name: joulehook-rs, dir: joulehook/joulehook-rs, runner: macos } + - { name: eoc-rs, dir: eoc/eoc-rs, runner: linux } + - { name: mesh-rs, dir: mesh/mesh-rs, runner: linux-arm64 } + - { name: joule-ui-rs, dir: joule-ui/joule-ui-rs, runner: macos } + steps: + - uses: actions/checkout@v5 + + # Two workspaces shell out to `z3`, and the runner image has no solver. + # Without one, `joulecontract-proof`'s z3 test takes its solver-absent + # branch — which asserts the ladder returns Unproved, "never a fake pass", + # and fails, because the ladder actually escalates past its two real rungs + # to a model STAND-IN that reports Proved. That is a genuine defect in the + # proof standard and is NOT fixed here: the stand-ins are load-bearing in + # proof-cascade and proof-conformance, which has a published vector pack, + # so changing whether a stand-in may close a goal is a deliberate decision + # for that standard's owner. Installing the solver lets CI exercise the + # intended path; it does not make the fallback correct. + # Both z3 jobs are pinned to Linux runners deliberately: the macOS runner is + # a host executor with no apt. `sudo` may or may not exist depending on + # whether the container runs as root, so fall back to a bare invocation. + - name: Install z3 + if: matrix.z3 + shell: bash + run: | + SUDO=""; [ "$(id -u)" -ne 0 ] && SUDO="sudo" + $SUDO apt-get update -qq + $SUDO apt-get install -y -qq z3 + z3 --version + + # The docker runner image ships no Rust at all, so rustup is bootstrapped + # here. dtolnay/rust-toolchain cannot be used: it shells out to `rustup`, + # which the image lacks. Harmless where cargo already exists. + - name: Install Rust (workspace pin) + shell: bash + run: | + export PATH="$HOME/.cargo/bin:$PATH" + command -v rustup >/dev/null 2>&1 || \ + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + + - name: Cache cargo registry + target + uses: actions/cache@v4 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + ${{ matrix.dir }}/target + key: standards-${{ matrix.name }}-${{ hashFiles(format('{0}/Cargo.lock', matrix.dir), 'rust-toolchain.toml') }} + restore-keys: | + standards-${{ matrix.name }}- + + # --all-targets is load-bearing: a plain `cargo check` does not build test + # targets, and smart-byte's dev-dependencies drifted independently of its + # normal ones (rand_chacha 0.10 against rand 0.8). The library compiled + # while the tests did not. + - name: Check (all targets) + working-directory: ${{ matrix.dir }} + run: cargo check --workspace --all-targets + + - name: Test + working-directory: ${{ matrix.dir }} + run: cargo test --workspace diff --git a/jcp/jcp-rs/Cargo.lock b/jcp/jcp-rs/Cargo.lock index 95b854c57..7c0c0ffcb 100644 --- a/jcp/jcp-rs/Cargo.lock +++ b/jcp/jcp-rs/Cargo.lock @@ -517,7 +517,7 @@ dependencies = [ "sandbox-schema", "serde", "serde_json", - "thiserror 2.0.18", + "thiserror 2.0.20", ] [[package]] -- 2.54.0 (Apple Git-157) From 3645849e2d7ffc2ea90364d24aa64ff11558e953 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sat, 29 Aug 2026 05:06:17 -0400 Subject: [PATCH 08/11] proof: an absent solver yields Unproved, never a fabricated proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `real_ladder()` was `[Propositional, Z3Smt, SmallModel, FrontierModel]`. The first two are real; the last two are stand-ins that gate on `GoalKind` and whose "artifact" is a hash of the goal restated. `FrontierModel` has no gate at all — it proves any goal unconditionally. So on a machine without `z3`, every goal came back Proved: the real rungs declined, the router escalated, and T3 obliged. The receipt claimed `closed_by: BigModel`, `provenance: Estimator`, `total_uj: 50_513_884` — the energy was as invented as the proof. `run_z3`'s own doc says a missing solver is read "as escalate, never as proof", but escalation *was* proof. This is the second instance of one bug. The first — a refutation escalated into a proof — was fixed by halting the router on `Verdict::Refuted`. The remaining hole was known: `formal_fix.rs` hand-built `[Propositional, Z3Smt]` to dodge it, noting "the stubs would still claim proved there". That workaround is now the library's behaviour instead of one call site's. * `Solver::is_decision_procedure()` — does this rung's `Proved` mean a verifier would accept the artifact? Defaults to **false**, so a newly written stand-in is excluded from the real ladders automatically and a real solver must claim to be checkable. Real: Propositional, Z3Smt, Z3Server, LeanVerifier. * `real_ladder` / `resident_z3_ladder` hold decision procedures only. Exhausting them yields Unproved — the honest answer to "nothing here could decide this". There is no T2/T3 rung because no real one exists yet; a missing rung must never be papered over with a stand-in, which converts "we could not decide" into "we decided". * `real_t0_ladder` → `reference_ladder_with_real_t0`. A mixed ladder under a `real_` name is the confusion that produced this bug. * `ladder_is_sound` asserts the split structurally; `ladder_never_fabricates_a_proof_when_a_rung_is_absent` drives the real router, because the defect lived in the composition of router and ladder, not in either alone. It uses a goal `z3` cannot parse, so it asserts the same thing whether or not a solver is installed. The conformance vector pack is byte-identical: it is generated from `reference_ladder`, which is unchanged and stays total by design — that is what makes routing vectors deterministic, and why it is a fixture and never evidence. What this was costing: `joule-code-release`'s pipeline already printed "z3 absent — postcondition honestly unproved, never faked" while the stand-in faked it, and certified releases on the result. It now reports gate=red and refuses. `formal_fix` no longer says "z3 found a counter-model" when z3 never ran. 394 tests pass across proof-rs, joule-code and joulecontract, with and without `z3` on PATH. CI keeps installing z3 — not for correctness now, but so the real T1 rung is exercised rather than skipped. Co-Authored-By: Claude Opus 5 --- .github/workflows/standards-build.yml | 23 +- .../examples/formal_fix.rs | 47 ++-- proof/proof-rs/Cargo.lock | 1 + proof/proof-rs/crates/proof-schema/src/lib.rs | 17 ++ .../proof-rs/crates/proof-solvers/Cargo.toml | 7 + .../proof-rs/crates/proof-solvers/src/lib.rs | 218 ++++++++++++++++-- 6 files changed, 264 insertions(+), 49 deletions(-) diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 9d38f90db..07addeba6 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -70,15 +70,20 @@ jobs: - uses: actions/checkout@v5 # Two workspaces shell out to `z3`, and the runner image has no solver. - # Without one, `joulecontract-proof`'s z3 test takes its solver-absent - # branch — which asserts the ladder returns Unproved, "never a fake pass", - # and fails, because the ladder actually escalates past its two real rungs - # to a model STAND-IN that reports Proved. That is a genuine defect in the - # proof standard and is NOT fixed here: the stand-ins are load-bearing in - # proof-cascade and proof-conformance, which has a published vector pack, - # so changing whether a stand-in may close a goal is a deliberate decision - # for that standard's owner. Installing the solver lets CI exercise the - # intended path; it does not make the fallback correct. + # + # This step used to be load-bearing for correctness: without a solver the + # ladder escalated past its real rungs into a model STAND-IN that reported + # Proved, so every goal on a solverless machine came back proved. That is + # now fixed at the source — the real ladders hold decision procedures only + # and an absent rung yields Unproved (proof-solvers `ladder_is_sound` and + # `ladder_never_fabricates_a_proof_when_a_rung_is_absent`). + # + # So the suites pass with or without z3, and this step is kept purely for + # COVERAGE: with a solver present the real T1 rung actually runs, and the + # SMT paths are exercised rather than skipped. The absent-rung semantics + # stay covered either way — that regression test uses a goal z3 cannot + # parse, so it asserts the same thing on a machine that has one. + # # Both z3 jobs are pinned to Linux runners deliberately: the macOS runner is # a host executor with no apt. `sudo` may or may not exist depending on # whether the container runs as root, so fall back to a bare invocation. diff --git a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs index e1b06227c..545e7e21a 100644 --- a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs +++ b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs @@ -39,7 +39,7 @@ use joulecontract_proof::{discharge, DischargeStatus, Formalization}; use joulecontract_schema::{Ceiling, Contract, ContentAddress, Rigor}; use proof_cascade::{ProofCache, Router}; use proof_schema::{GoalKind, SpecGrounding}; -use proof_solvers::{z3_available, Propositional, Z3Smt}; +use proof_solvers::{real_ladder, z3_available}; // SOUNDNESS NOTE — why this example uses a decision-procedure ladder. // @@ -51,15 +51,23 @@ use proof_solvers::{z3_available, Propositional, Z3Smt}; // `FrontierModel` proves ANY goal unconditionally — so a disproof was // fabricated into a proof. // -// That is now fixed in the proof crate: `Verdict::Refuted` exists, `Z3Smt` -// emits it on `sat`, and the router HALTS on a refutation instead of escalating -// (regression test in proof-cascade). So `real_ladder()` no longer fabricates a -// proof of candidate A — it halts at `Z3Smt` with a refutation. +// That was fixed in the proof crate: `Verdict::Refuted` exists, `Z3Smt` emits +// it on `sat`, and the router HALTS on a refutation instead of escalating +// (regression test in proof-cascade). // -// We still use the decision-procedure ladder `[Propositional, Z3Smt]` here, on -// purpose: a formal *gate* must not depend on a model stand-in even for goals -// z3 returns `unknown` on (the stubs would still claim `proved` there). The -// gate's guarantee is "a decision procedure decided this", nothing weaker. +// A SECOND hole survived that fix, and this note used to describe the local +// workaround for it: escalation past a rung that *could not run at all*. With +// `z3` absent, `Z3Smt` returned `Unproved`, the router escalated, and +// `FrontierModel` closed the goal — so on any machine without `z3`, every goal +// came back proved at ~50 J of imaginary energy. This example dodged it by +// hand-building `[Propositional, Z3Smt]` instead of calling `real_ladder()`. +// +// That is now fixed at the source rather than at this call site: +// `real_ladder()` IS the decision-procedure ladder, the stand-ins live only in +// the `reference_*` fixtures, and `Solver::is_decision_procedure` makes the +// distinction machine-checkable (`ladder_is_sound` in proof-solvers). So the +// hand-rolled ladder is gone and the guarantee is unchanged: "a decision +// procedure decided this", nothing weaker. /// The contract over the netting function: one precondition, one postcondition /// (the property the fix must honor), one frame. Same spec for both candidates @@ -109,10 +117,10 @@ fn judge(label: &str, net_definition: &str) -> bool { grounding: SpecGrounding::CrossChecked, }; // A fresh cascade + cache per candidate so the joules reported are this - // candidate's own proof work, not a cache hit from the other. The ladder is - // decision-procedures only (see the SOUNDNESS NOTE at the top) — a formal + // candidate's own proof work, not a cache hit from the other. `real_ladder` + // is decision-procedures only (see the SOUNDNESS NOTE at the top) — a formal // gate may not fall through to a model stand-in that fabricates a proof. - let router = Router::new(vec![Box::new(Propositional), Box::new(Z3Smt)]); + let router = Router::new(real_ladder()); let mut cache = ProofCache::new(); let d = discharge(&contract, &[formalization], &router, &mut cache) .expect("discharge runs (bookkeeping is well-formed)"); @@ -129,10 +137,17 @@ fn judge(label: &str, net_definition: &str) -> bool { true } DischargeStatus::Unproved(result) => { - println!( - " UNPROVED — z3 found a counter-model; the postcondition can fail ({} µJ measured)", - result.total_uj - ); + // "Unproved" has two very different causes and they must not read + // the same: z3 ran and refuted the claim, or z3 was never there to + // ask. Printing "found a counter-model" in the second case would + // report evidence that was never gathered — the exact failure this + // example exists to demonstrate. + let why = if z3_available() { + "z3 found a counter-model; the postcondition can fail" + } else { + "no decision procedure available to decide it (z3 absent)" + }; + println!(" UNPROVED — {why} ({} µJ measured)", result.total_uj); println!(" → formal gate REFUSES this fix (it would be reverted, never shipped)."); false } diff --git a/proof/proof-rs/Cargo.lock b/proof/proof-rs/Cargo.lock index c0d1c1e72..8fcdfca75 100644 --- a/proof/proof-rs/Cargo.lock +++ b/proof/proof-rs/Cargo.lock @@ -302,6 +302,7 @@ dependencies = [ name = "proof-solvers" version = "0.1.0" dependencies = [ + "proof-cascade", "proof-schema", ] diff --git a/proof/proof-rs/crates/proof-schema/src/lib.rs b/proof/proof-rs/crates/proof-schema/src/lib.rs index 398f70588..7eb2badbc 100644 --- a/proof/proof-rs/crates/proof-schema/src/lib.rs +++ b/proof/proof-rs/crates/proof-schema/src/lib.rs @@ -308,6 +308,23 @@ pub trait Solver { fn tier(&self) -> Tier; /// Attempt the goal, reporting the verdict and the energy spent. fn attempt(&self, goal: &ProofGoal) -> Attempt; + + /// Whether this solver's [`Verdict::Proved`] is backed by an artifact a + /// verifier would actually accept — i.e. the rung ran a real decision + /// procedure or proof checker and reports what it found. + /// + /// **Defaults to `false`, deliberately.** A stand-in that models a rung's + /// reach by gating on [`GoalKind`] returns `Proved` without ever checking + /// anything, and its "artifact" is a hash of the goal restated. Such a rung + /// is sound only as a routing fixture; it must never sit in a ladder whose + /// verdict is read as evidence. + /// + /// The safe default is the point: a newly written stand-in is excluded from + /// the real ladders automatically, and a real solver must *claim* to be + /// checkable. `ladder_is_sound` in `proof-solvers` enforces this. + fn is_decision_procedure(&self) -> bool { + false + } } #[cfg(test)] diff --git a/proof/proof-rs/crates/proof-solvers/Cargo.toml b/proof/proof-rs/crates/proof-solvers/Cargo.toml index db0066719..6b02fa855 100644 --- a/proof/proof-rs/crates/proof-solvers/Cargo.toml +++ b/proof/proof-rs/crates/proof-solvers/Cargo.toml @@ -9,5 +9,12 @@ rust-version.workspace = true [dependencies] proof-schema = { workspace = true } +# Test-only: `ladder_never_fabricates_a_proof_when_a_rung_is_absent` drives the +# real router, because the fabrication bug lived in the *composition* of router +# and ladder, not in either alone. proof-cascade does not depend on this crate, +# so there is no cycle. +[dev-dependencies] +proof-cascade = { workspace = true } + [lints] workspace = true diff --git a/proof/proof-rs/crates/proof-solvers/src/lib.rs b/proof/proof-rs/crates/proof-solvers/src/lib.rs index 953774469..729b0ca69 100644 --- a/proof/proof-rs/crates/proof-solvers/src/lib.rs +++ b/proof/proof-rs/crates/proof-solvers/src/lib.rs @@ -7,18 +7,23 @@ //! truth-table, in process. //! - [`Z3Smt`] (T1) → shells out to `z3` on an SMT-LIB2 goal (assert the //! negation; `unsat` ⇒ valid). [`Z3Server`] keeps `z3` resident across goals. +//! - [`LeanVerifier`] → runs Lean and reports what the kernel accepted. //! -//! The model rungs are honest stand-ins that gate on `GoalKind` until the real -//! backends are wired behind the identical [`Solver`] trait: +//! The model rungs are stand-ins that gate on `GoalKind` until real backends are +//! wired behind the identical [`Solver`] trait: //! //! - [`SmallModel`] (T2) → a distilled in-domain prover. //! - [`FrontierModel`] (T3) → a frontier reasoning model; the last resort. //! - [`Automation`] / [`Smt`] → the original `GoalKind`-gated stand-ins, kept for //! [`reference_ladder`]. //! -//! A solver returns `Proved` only when a verifier would accept the artifact — -//! correctness is never traded for energy. The real rungs run the tool and -//! report what actually happened; the stand-ins model the rung's reach. +//! **A solver returns `Proved` only when a verifier would accept the artifact — +//! correctness is never traded for energy.** The stand-ins cannot honour that on +//! their own: they check nothing, and their "artifact" is a hash of the goal +//! restated. So the contract is held at the *ladder* level instead, by +//! [`Solver::is_decision_procedure`] and the two ladder families described +//! below — a stand-in is a routing fixture, never evidence, and never sits +//! beneath a real rung where the router would escalate into it. pub mod prop; @@ -127,6 +132,11 @@ impl Solver for FrontierModel { pub struct Propositional; impl Solver for Propositional { + /// Real: `Proved` means `the truth table was exhausted and the goal held under every assignment`. + fn is_decision_procedure(&self) -> bool { + true + } + fn tier(&self) -> Tier { Tier::Automation } @@ -217,6 +227,11 @@ fn z3_counter_model(script: &str) -> String { pub struct Z3Smt; impl Solver for Z3Smt { + /// Real: `Proved` means ``z3` returned `unsat` on the negated claim`. + fn is_decision_procedure(&self) -> bool { + true + } + fn tier(&self) -> Tier { Tier::Smt } @@ -346,6 +361,11 @@ impl Default for Z3Server { } impl Solver for Z3Server { + /// Real: `Proved` means `the resident `z3` returned `unsat` on the negated claim`. + fn is_decision_procedure(&self) -> bool { + true + } + fn tier(&self) -> Tier { Tier::Smt } @@ -465,6 +485,11 @@ impl LeanVerifier { } impl Solver for LeanVerifier { + /// Real: `Proved` means `Lean accepted the term — the kernel checked it`. + fn is_decision_procedure(&self) -> bool { + true + } + fn tier(&self) -> Tier { self.tier } @@ -504,8 +529,37 @@ impl Solver for LeanVerifier { } } +// ── Two families of ladder, and why they must not be mixed ────────────── +// +// A ladder's verdict is only as sound as its weakest rung, because the router +// escalates until something says `Proved` and then stops. Put a fabricating +// stand-in below a real rung and the ladder proves *everything*: the real rungs +// decline, the stand-in obliges, and the cascade reports success. +// +// That is not hypothetical — it shipped twice. The first instance was a +// refutation escalated into a proof (fixed by `Verdict::Refuted` halting the +// router). The second was this one: with `z3` absent, `Z3Smt` returned +// `Unproved`, the router escalated, and `FrontierModel` — which proves any goal +// unconditionally — closed the goal at T3. Every goal on a machine without `z3` +// came back proved, at ~50 J of imaginary energy. +// +// So the families are kept apart by construction and checked by +// `ladder_is_sound`: +// +// * **real** — every rung `is_decision_procedure()`. Exhausting the ladder +// yields `Unproved`, which is the honest answer to "nothing here could +// decide this". An absent tool must produce a weaker claim, never a +// stronger one. +// * **reference** — stand-ins that gate on `GoalKind`. Total by design, which +// is what makes routing and receipt vectors deterministic. Sound as a +// fixture, never as evidence. + /// The pure stand-in ladder, cheapest-first — every rung a `GoalKind`-gated /// model, used by conformance to exercise routing deterministically. +/// +/// **Fixture only.** No rung here checks anything: `Proved` carries a hash of +/// the goal restated, and [`FrontierModel`] closes *any* goal. Use it to pin +/// routing and receipt encoding, never to decide whether something is true. pub fn reference_ladder() -> Vec> { vec![ Box::new(Automation), @@ -515,8 +569,13 @@ pub fn reference_ladder() -> Vec> { ] } -/// A ladder with a real propositional decider at T0 over the stand-ins above. -pub fn real_t0_ladder() -> Vec> { +/// The reference ladder with a real propositional decider at T0. +/// +/// **Fixture only**, like [`reference_ladder`]: T0 is real, but the rungs above +/// it are stand-ins, so the ladder is still total and its verdict still is not +/// evidence. Renamed from `real_t0_ladder` — a mixed ladder under a `real_` +/// name is exactly the confusion that produced the fabrication bug. +pub fn reference_ladder_with_real_t0() -> Vec> { vec![ Box::new(Propositional), Box::new(Smt), @@ -525,25 +584,27 @@ pub fn real_t0_ladder() -> Vec> { ] } -/// Two real rungs: the propositional decider (T0) and `z3` (T1), over the model -/// stand-ins. +/// The real ladder: the propositional decider (T0) and `z3` (T1) — every rung a +/// decision procedure, so a `Proved` verdict is backed by something a verifier +/// would accept. +/// +/// There is no T2/T3 rung because no real one exists yet. When a model backend +/// lands behind the same [`Solver`] trait and can emit a checkable artifact, it +/// joins here; until then the ladder ends at T1 and unreachable goals come back +/// `Unproved`. **A missing rung must never be papered over with a stand-in** — +/// that converts "we could not decide" into "we decided", which is the one +/// error a proof system may not make. +/// +/// With `z3` absent this ladder decides only propositional goals and returns +/// `Unproved` for the rest. That is the intended behaviour: see +/// [`z3_available`] to report the reduced reach honestly rather than hide it. pub fn real_ladder() -> Vec> { - vec![ - Box::new(Propositional), - Box::new(Z3Smt), - Box::new(SmallModel), - Box::new(FrontierModel), - ] + vec![Box::new(Propositional), Box::new(Z3Smt)] } /// Like [`real_ladder`] but with `z3` kept resident at T1. pub fn resident_z3_ladder() -> Vec> { - vec![ - Box::new(Propositional), - Box::new(Z3Server::new()), - Box::new(SmallModel), - Box::new(FrontierModel), - ] + vec![Box::new(Propositional), Box::new(Z3Server::new())] } /// Whether a working `z3` is on PATH — lets callers/tests adapt honestly. @@ -561,6 +622,115 @@ pub fn z3_available() -> bool { mod tests { use super::*; + /// Every rung of a ladder that calls itself real must be a decision + /// procedure. This is the structural guard: the fabrication bug was a + /// stand-in sitting where the router could escalate into it, and a shape + /// test catches that at compile-and-test time rather than in an audit. + #[test] + fn ladder_is_sound() { + for (name, ladder) in [ + ("real_ladder", real_ladder()), + ("resident_z3_ladder", resident_z3_ladder()), + ] { + assert!(!ladder.is_empty(), "{name}: a real ladder needs a rung"); + for rung in &ladder { + assert!( + rung.is_decision_procedure(), + "{name}: rung {:?} is not a decision procedure — a stand-in \ + here lets the router escalate a failure into a fabricated proof", + rung.tier() + ); + } + } + + // And the fixture ladders are honestly declared as such, so the marker + // means something in both directions. + assert!( + reference_ladder() + .iter() + .all(|r| !r.is_decision_procedure()), + "reference_ladder must be entirely stand-ins" + ); + assert!( + reference_ladder_with_real_t0() + .iter() + .filter(|r| !r.is_decision_procedure()) + .count() + == 3, + "reference_ladder_with_real_t0 is one real rung under three stand-ins" + ); + } + + /// The regression itself, driven through the real router. + /// + /// A goal no decision procedure can discharge must come back `Unproved`. + /// Before the fix this returned **Proved, closed by `BigModel`, at ~50 J** — + /// on any machine without `z3`, every goal did. The energy figure was as + /// invented as the proof. + /// + /// Holds with or without `z3` on PATH: `z3` cannot parse prose, so it + /// declines either way, which is what makes this a stable assertion rather + /// than one that changes meaning with the runner image. + #[test] + fn ladder_never_fabricates_a_proof_when_a_rung_is_absent() { + use proof_cascade::{ProofCache, Router}; + + let unreachable = ProofGoal::new( + "every even integer > 2 is the sum of two primes", + "lean4", + GoalKind::Hard, + ); + + let mut cache = ProofCache::default(); + let out = Router::new(real_ladder()).prove(&unreachable, &mut cache); + + assert!( + !out.proved, + "a goal no decision procedure decided came back proved, closed by {:?}", + out.closed_by + ); + assert!( + out.closed_by.is_none(), + "nothing may close a goal it did not decide (closed_by = {:?})", + out.closed_by + ); + assert!( + !out.attempts.iter().any(|a| a.proved), + "no rung may report success here" + ); + // No model rung may even be on this ladder to be escalated into. + assert!( + !out.attempts + .iter() + .any(|a| matches!(a.tier, Tier::SmallModel | Tier::BigModel)), + "a model stand-in ran on the real ladder" + ); + } + + /// The reference ladder is *total* — it closes every goal, including the one + /// above that no real solver can touch. That totality is exactly why it is + /// useful for pinning routing determinism and exactly why it must never sit + /// under a real rung. Kept as a test so the property is asserted rather than + /// assumed by the ladder-family split. + #[test] + fn reference_ladder_is_total_which_is_why_it_is_fixture_only() { + use proof_cascade::{ProofCache, Router}; + + let unreachable = ProofGoal::new( + "every even integer > 2 is the sum of two primes", + "lean4", + GoalKind::Hard, + ); + let mut cache = ProofCache::default(); + let out = Router::new(reference_ladder()).prove(&unreachable, &mut cache); + + assert!( + out.proved, + "the stand-in ladder closes everything by design" + ); + assert_eq!(out.closed_by, Some(Tier::BigModel)); + } + #[test] fn each_rung_reaches_its_kind() { let triv = ProofGoal::new("x = x", "lean4", GoalKind::Trivial); @@ -590,7 +760,7 @@ mod tests { .attempt(&ProofGoal::new("∀ n, n+0 = n", "lean4", GoalKind::General)) .verdict .is_proved()); - assert_eq!(real_t0_ladder().len(), 4); + assert_eq!(reference_ladder_with_real_t0().len(), 4); } #[test] @@ -601,7 +771,7 @@ mod tests { GoalKind::Decidable, ); let a = Z3Smt.attempt(&valid); - assert_eq!(real_ladder().len(), 4); + assert_eq!(real_ladder().len(), 2); // decision procedures only if z3_available() { assert!(a.verdict.is_proved()); assert!(a.energy.uj() >= 1); @@ -666,7 +836,7 @@ mod tests { assert!(server.attempt(&comm).verdict.is_proved()); assert!(server.attempt(&thm).verdict.is_proved()); // still healthy after prose } - assert_eq!(resident_z3_ladder().len(), 4); + assert_eq!(resident_z3_ladder().len(), 2); // decision procedures only assert!(looks_like_smt("(assert (> x 0))")); assert!(!looks_like_smt("∃ continuous f")); assert!(!looks_like_smt("(unbalanced")); -- 2.54.0 (Apple Git-157) From 5c0b1110d43cfa6b91f51df94e5d13ace85385b9 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sat, 29 Aug 2026 12:05:16 -0400 Subject: [PATCH 09/11] jouleclaw-fabric: gate probe_metal_mpp to macOS, like its two siblings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `probe_metal_mpp` calls `jouleclaw_backend_apple::mps_device_name()`, but `jouleclaw-backend-apple` is declared under `[target.'cfg(target_os = "macos")'.dependencies]` — so on any other target the crate is absent and the reference does not resolve: error[E0433]: cannot find module or crate `jouleclaw_backend_apple` --> crates/jouleclaw-fabric/src/detect.rs:135 Its two siblings, `probe_amx` and `probe_metal_gpu`, both carry `#[cfg(target_os = "macos")]`; this one was missed. The *call site* is inside a macOS-gated block, which is why it looked fine — but the *definition* is still compiled on every target, and its body names a crate that isn't there. This is why `joule-code conformance gate` has failed all 11 runs since it was added on 2026-07-23 and has never once passed: it is `runs-on: linux`, and its third step builds `joule-code/examples/l3-jouleclaw`, which pulls jouleclaw-fabric in via `jouleclaw-loader-gguf`'s `fabric` feature. The failure had nothing to do with the commits that triggered it. It survived because nothing else compiles this crate for Linux: `jouleclaw-rs` is not in the standards-build matrix, so its only non-macOS build in CI is this one transitive path through an example in another standard's workflow. Verified `cargo check --target x86_64-unknown-linux-gnu --all-targets` on l3-jouleclaw — clean, where it previously failed on this error — and macOS is unaffected (jouleclaw-fabric 13 tests, l3-jouleclaw green). Co-Authored-By: Claude Opus 5 --- jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs index d435055b0..6b50a6cb1 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs @@ -131,6 +131,7 @@ fn probe_metal_gpu() -> Option { /// caller falls back, so it simply never records here). /// Seeded at the quiet-box measurement (~6 mJ/GFLOP, M4/M5); /// a per-box `mpp_energy` run overlays the Measured value. +#[cfg(target_os = "macos")] fn probe_metal_mpp() -> Option { let name = jouleclaw_backend_apple::mps_device_name()?; let mut energy = BTreeMap::new(); -- 2.54.0 (Apple Git-157) From cbc5c82fd4a7ee93590e03bd51bdbde1a6ebc04f Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sat, 29 Aug 2026 21:01:41 -0400 Subject: [PATCH 10/11] =?UTF-8?q?ci:=20cover=20jouleclaw-rs=20=E2=80=94=20?= =?UTF-8?q?the=20workspace=20nothing=20was=20compiling?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `ci: build + test every Rust workspace` was not true: jouleclaw-rs was absent from the matrix. It is one of the largest standards in the tree (4457 tests), and its only non-macOS build in CI was a transitive path through `joule-code/examples/l3-jouleclaw` in another standard's workflow — a path that had been red since 2026-07-23, so the signal was already saturated. That is how an unguarded `jouleclaw_backend_apple` reference survived seven weeks. This entry is the one whose runner is a CORRECTNESS choice, not capacity. jouleclaw-embed-candle and jouleclaw-rerank-candle reach candle → ug → gemm, which uses inline aarch64 assembly (`fmla {0:v}.8h, ...`) requiring the ARMv8.2 FP16 extension: aarch64-apple-darwin target_feature="fp16" present aarch64-unknown-linux-gnu target_feature="fp16" absent Apple Silicon guarantees FP16 so it is in the darwin baseline; generic arm64 Linux baselines at ARMv8.0-A and the same asm cannot be ASSEMBLED. Nothing is wrong with the code — it is a target-baseline difference in a transitive dep, and it is invisible on a dev Mac by construction. Critically it is also invisible to `cargo check`, which stops at type-checking and never reaches codegen. The workspace checks clean on arm64 Linux with `--all-targets` and still fails to build its tests. Compiling is a weaker claim than passing, and checking is weaker than compiling; this entry runs the real thing. Verified in a native aarch64 Linux container (rustc 1.98.0, gcc 12.2 — CI's toolchain): without the flag, 12 codegen errors; with it, 4457 passed / 0 failed / 55 ignored across 314 test binaries. `rustflags` is per-entry rather than job-wide so this stays scoped to the one workspace that needs it, and the next reader sees which one that is. Co-Authored-By: Claude Opus 5 --- .github/workflows/standards-build.yml | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 07addeba6..dab83e307 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -42,9 +42,9 @@ jobs: build: name: ${{ matrix.name }} # Spread across the fleet's runners rather than pinning every job to `linux`. - # These are pure-Rust builds with no platform-specific behaviour, so the - # runner is a capacity choice, not a correctness one — and 16 jobs on a - # single runner queue behind whatever else is using it. + # For most of these the runner is a capacity choice, not a correctness one — + # and 17 jobs on a single runner queue behind whatever else is using it. + # `jouleclaw-rs` is the exception: see its matrix entry. runs-on: ${{ matrix.runner }} strategy: fail-fast: false @@ -66,6 +66,16 @@ jobs: - { name: eoc-rs, dir: eoc/eoc-rs, runner: linux } - { name: mesh-rs, dir: mesh/mesh-rs, runner: linux-arm64 } - { name: joule-ui-rs, dir: joule-ui/joule-ui-rs, runner: macos } + # jouleclaw-rs is the one entry whose runner IS a correctness choice. + # It reaches candle → ug → gemm, which uses inline aarch64 assembly + # (`fmla {0:v}.8h, ...`) requiring the ARMv8.2 FP16 extension. + # `aarch64-apple-darwin` carries target_feature="fp16" in its baseline + # because Apple Silicon guarantees it; `aarch64-unknown-linux-gnu` + # baselines at ARMv8.0-A and does not, so the same asm fails to + # ASSEMBLE — a codegen error `cargo check` never reaches. Verified on a + # native arm64 Linux container (rustc 1.98.0): without the flag, 12 + # errors; with it, 4457 tests pass. + - { name: jouleclaw-rs, dir: jouleclaw/jouleclaw-rs, runner: linux-arm64, rustflags: "-C target-feature=+fp16" } steps: - uses: actions/checkout@v5 @@ -124,8 +134,12 @@ jobs: # while the tests did not. - name: Check (all targets) working-directory: ${{ matrix.dir }} + env: + RUSTFLAGS: ${{ matrix.rustflags }} run: cargo check --workspace --all-targets - name: Test working-directory: ${{ matrix.dir }} + env: + RUSTFLAGS: ${{ matrix.rustflags }} run: cargo test --workspace -- 2.54.0 (Apple Git-157) From d128eaa6babef668a747671b5a807e36a76ab7dc Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sat, 29 Aug 2026 21:49:43 -0400 Subject: [PATCH 11/11] ci: note the linux-arm64 cache-volume constraint for jouleclaw-rs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The jouleclaw-rs target tree is ~16 GB and tx-dev-linux-arm64's 120 GB volume already carries ~74 GB of other workspaces' caches. A full volume fails whatever is building at the time rather than whatever changed, which reads as an unrelated regression — so record where to look first. Co-Authored-By: Claude Opus 5 --- .github/workflows/standards-build.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index dab83e307..8a13bc820 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -75,6 +75,13 @@ jobs: # ASSEMBLE — a codegen error `cargo check` never reaches. Verified on a # native arm64 Linux container (rustc 1.98.0): without the flag, 12 # errors; with it, 4457 tests pass. + # + # CAPACITY: this is by far the largest entry — its target tree is + # ~16 GB, against a 120 GB volume on tx-dev-linux-arm64 that already + # holds ~74 GB of other workspaces' caches. If linux-arm64 jobs start + # failing for no apparent reason, check `df -h /mnt/lima-colima-txarm` + # on the txarm VM before suspecting the code: a full cache volume + # fails whatever happens to be building, not whatever changed. - { name: jouleclaw-rs, dir: jouleclaw/jouleclaw-rs, runner: linux-arm64, rustflags: "-C target-feature=+fp16" } steps: - uses: actions/checkout@v5 -- 2.54.0 (Apple Git-157)