AR-1: the Action Receipt, its verifier, and CI for every workspace #65
Loading…
Reference in a new issue
No description provided.
Delete branch "ar-1-on-main"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Replaces #58, which went unmergeable when main independently landed the same repair work.
Why a new branch
In the last two days main fixed everything #58 fixed —
hmac 0.13→KeyInit,cbc's missingstdfeature,rand_core's missingalloc,Grant's dual-ceiling fields, the 1.98.0 toolchain bump and the dependency update. Same diagnoses, reached independently, and in tidier form (use hmac::{Hmac, KeyInit, Mac}beats the qualified-path version #58 used).That left #58 with twelve conflicts, all in files where both sides had fixed the same thing. Forcing it through to re-land work that already exists would be risk for no gain, so this branch is rebuilt on current main with only what main does not have. Every AR-1 commit applied cleanly — no conflicts, because it is genuinely new.
What this adds
AR-1 — the Action Receipt. Three receipt families already ship, each holding one quarter of what an audit asks for, and none binds to the others:
jcp-receipt(authority),sandbox-proof(environment), JCR-1 (work) — and nothing at all records effect. AR-1 is an envelope that binds the three by content-id and supplies the fourth. No new cryptography: canonical det-CBOR and COSE_Sign1 are reused verbatim from jcr1.Three structural rules 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:
effect: irreversiblerequires a plan receiptegress: nonerequires zero bytesegress: attested_enclaverequires a peer attestation — trust is not an egress classar-verify— the standalone verifier. A format nobody outside this repo can check is a convention; one with a verifier a third party can run is a standard. On the forged vector it prints the whole thesis in one line: "The signature is valid; the receipt is not."Conformance pack — 7 positive, 3 negative, published fixture key. 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.
End-to-end on real hardware — a real grant, really attenuated (amplification refused in the run, not asserted in a comment), a real
decidecall, and 11.09 J measured off IOReport, sealed and verified from the envelope alone. Tier stampedS0because that is what actually ran; claimingS5without a microVM is the overreach the ladder exists to prevent.The cascade egress contract — closes the "nobody ships a privacy router" gap.
Egress::Undeclaredis the default so silence cannot be mistaken for "nothing left the device", and the runtime stamps the tier's declaration rather than letting the tier write its own claim.CI for all sixteen workspaces — none had it before.
One defect deliberately left unfixed
With
z3absent,real_ladderescalates past both real rungs to a model stand-in that reportsProved— breakingproof-solvers' own contract that "a solver returns Proved only when a verifier would accept the artifact". This branch installs z3 so CI exercises the intended path; it does not touch the ladder, becauseproof-conformanceships a published vector pack that a semantics change would invalidate. That call belongs to the proof standard's owner. Full diagnosis in the CI commit.Verified
jcp-rs258 ·jouleclaw-cascade108 ·jouledesk23 — all green on this branch against current main. The 16/16 matrix ran green on the predecessor.🤖 Generated with Claude Code
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 <[email protected]> (cherry picked from commitd3e1c2adda)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 <envelope> --pubkey <hex> --steward <did> one receipt ar-verify --pack <dir> 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 <[email protected]> (cherry picked from commit0b29405ea0)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 <[email protected]> (cherry picked from commit96255f720b)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:<base64url of 32 bytes>" 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 <[email protected]> (cherry picked from commit453280c328)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 <[email protected]> (cherry picked from commit95f1c00238)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 <[email protected]>`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 <[email protected]>`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 <[email protected]>`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 <[email protected]>