AR-1: the Action Receipt, its verifier, and CI for every workspace #65

Merged

dcharlot merged 12 commits from ar-1-on-main into main 2026-08-30 15:49:48 -04:00

Conversation 0 Commits 12 Files changed 25 +3051 -48

2026-08-29

Transaction Science

ci: note the linux-arm64 cache-volume constraint for jouleclaw-rs ...

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 <[email protected]>

d128eaa6ba

• View at this point in history

2026-08-29 21:49:43 -04:00

Transaction Science

ci: cover jouleclaw-rs — the workspace nothing was compiling ...

`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]>

cbc5c82fd4

• View at this point in history

2026-08-29 21:01:41 -04:00

Transaction Science

jouleclaw-fabric: gate probe_metal_mpp to macOS, like its two siblings ...

`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]>

5c0b1110d4

• View at this point in history

2026-08-29 12:05:16 -04:00

Transaction Science

Merge origin/main into ar-1-on-main — reconcile the two stand-in markers ...

Main landed PR #62's soundness work (`Solver::is_reference_stub`,
`CascadeResult::closed_by_stub`, `require_substantive_proof`, and
proof-conformance's `soundness.rs`) after this branch diverged. That work and
the ladder fix here address the same defect from opposite ends:

  * main **detects** a fabricated proof — the stand-ins declare themselves, the
    result is marked, the cache does not launder the marker, and a relying
    party can refuse it.
  * this branch **prevents** it — the real ladders hold decision procedures
    only, so a solverless machine yields Unproved instead of escalating into a
    rung that proves anything.

Both are wanted, but two overlapping markers are worse than one. Resolution:

  * Dropped `is_decision_procedure` in favour of main's published
    `is_reference_stub`, and re-expressed `ladder_is_sound` in its terms. The
    marker I added had the safer default (a new stand-in is excluded unless it
    claims to be checkable) but a second trait method meaning nearly the same
    thing is a worse outcome than losing that default.
  * Recovered the safety that default was buying at the ladder instead:
    `ladder_is_sound` now also pins the real ladders' exact tiers, so a
    stand-in that forgets to override `is_reference_stub` still cannot slip in
    unnoticed. Documented on the trait so the two halves are findable together.
  * `soundness.rs`'s `a_stand_in_proof_is_detectable_before_it_is_trusted`
    proved an open conjecture through `real_ladder()` to demonstrate detection.
    That premise is gone — it now exercises `reference_ladder()`, where
    stand-ins legitimately live, and the property it tests is unchanged.
  * Added `the_real_ladder_never_reaches_a_stand_in` as its companion. Detection
    is a last line of defence that only works if the relying party remembers to
    call it; not reaching a stand-in at all does not depend on anyone
    remembering.

Note the defect was still live on main: main's `real_ladder()` still ends in
`FrontierModel`, and main's own `joulecontract-proof` test asserts the SMT rung
returns Unproved when no solver is present — which fails there on any machine
without `z3`.

402 tests pass across proof-rs, joule-code and joulecontract, both with and
without `z3` on PATH. The conformance vector pack is byte-identical.

Co-Authored-By: Claude Opus 5 <[email protected]>

fa88c5c9d2

• View at this point in history

2026-08-29 05:13:10 -04:00

Transaction Science

proof: an absent solver yields Unproved, never a fabricated proof ...

`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]>

3645849e2d

• View at this point in history

2026-08-29 05:06:17 -04:00

2026-08-28

Transaction Science

ci: build + test every Rust workspace ...

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]>

a12d5c202d

• View at this point in history

2026-08-28 08:47:01 -04:00

Transaction Science

jouledesk: the test was wrong, not the ledger ...

`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 <[email protected]>

ff27d74dfc

• View at this point in history

2026-08-28 08:47:01 -04:00

Transaction Science

cascade: the egress contract — per-resolution, and never stronger than evidence ...

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 commit 95f1c00238)

fce6e6eb98

• View at this point in history

2026-08-28 08:44:08 -04:00

Transaction Science

ar: bind the real emitters, not placeholder ids ...

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 commit 453280c328)

f6e0e8c665

• View at this point in history

2026-08-28 08:44:08 -04:00

Transaction Science

ar: end-to-end proof on real hardware — 11.09 J, measured ...

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 commit 96255f720b)

4d4b87cf19

• View at this point in history

2026-08-28 08:44:08 -04:00

Transaction Science

ar-verify: the standalone Action Receipt verifier ...

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 commit 0b29405ea0)

b4d8af688f

• View at this point in history

2026-08-28 08:44:08 -04:00

Transaction Science

jcp-action-receipt: AR-1, the composition envelope ...

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 commit d3e1c2adda)

72aec523d2

• View at this point in history

2026-08-28 08:44:07 -04:00