Receipts as a training corpus + prove-local: attested offline inference #31
2026-07-20
sandbox-proof: prove-local — attested local inference, zero egress
The proof matrix showcased the cloud path and left the air-gap path
undemonstrated. prove-gpu and prove-lpu both reach across a network to
silicon the prover does not own; there was no counterpart proving the
case the sandbox ladder was built for. Every component existed —
mmap-only GGUF loading with no network fetch path, deny-by-default
NetworkGrant, offline Ed25519 attestation, hardware energy counters —
and nothing assembled them.
prove_local runs a local engine against local weights with no network
grant, meters it on this host's own counters, and seals a cell.
It is the deliberate inverse of prove_inference. There the silicon
belongs to someone else, so energy is an honest token Estimator. Here
the silicon is ours — the one case where joules can actually be
measured — so device records pass through verbatim from PowerMeter
with whatever provenance the hardware honestly supports. The meter can
degrade; this does not re-tag it.
Three properties, each checked rather than asserted:
1. Weights are local. Opened from disk and streamed into a BLAKE3
bound into the proof, so the cell attests inference against these
bytes and not merely "a model". An unresolvable path is an error.
2. No egress was granted. The NetworkGrant default — empty outbound,
inbound false — is asserted before the engine is spawned.
3. Energy is this host's, measured across the engine's execution.
A non-zero engine exit refuses to seal: a proof for a run that failed
would attest to work that did not happen.
The engine is operator-supplied and driven as a subprocess, exactly as
prove_accelerator drives a GPU workload, so the sandbox standard takes
no dependency on any particular inference runtime.
Verified end to end on Apple Silicon against a real checkpoint:
Devstral-Small-2-24B-Instruct Q4_K_M, 13.35 GiB, generating from the
local GGUF at 17.4 tok/s warm — 92.68 J measured over the span via
IOReport energy-model counters (HwShunt, sudo-free), sealed to receipt
b3:ARwbWCm… with attestation and signature both verified.
SPEC §7.2 caught the first cut: the Apple meter reports CPU, GPU and
ANE together, and a hardcoded CPU-only DeviceIdentity list left the
NPU energy record unnamed. Identities are now derived from the
measurement rather than assumed — the standard enforcing its own
invariant against an incomplete implementation.
4 guard tests: absent weights, failed engine, weight-hash binding,
zero-egress posture.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
jouleclaw-corpus: receipts → training corpus
Sealed receipts already record what a cascade walk did: which tier
closed the query, at what microjoule cost, at what counter honesty.
That is an observed execution outcome — the same class of supervision
a code model gets from "passes on head, fails on base", except it
arrives signed and energy-metered rather than reconstructed after the
fact. Until now receipts were terminal: written, verified, summed into
cost reports, never read again.
This projects them into the labelled (embedding, stage, success,
cost_microjoules) rows an EOC router trainer consumes, so the ledger
compounds instead of merely accumulating.
Derivation is honest about its limits:
- cost_microjoules is verbatim joules_uj — not modelled, not rescaled.
- stage prefers the runtime's own eoc_stage label, else maps from
CascadeTier only where unambiguous. L1Lawful has no EOC analogue and
nothing maps to Graph, so those receipts are skipped and counted in
CorpusStats rather than guessed into a bucket.
- success means "this tier closed the walk". The receipt carries no
failure discriminator; that is documented, not papered over.
- Monotone negatives (the cheaper rungs a strict cascade must have
escalated past) are opt-in, because they rest on an assumption a
rung-skipping router would break. Graph is never synthesised as a
negative.
Two traps absorbed. The receipt's eoc_stage is lower-case ("neural")
while the trainer's Stage deserialises capitalised ("Neural") and
rejects anything else — passing the field through fails at ingest, so
from_eoc_label converts and a test pins the emitted spelling. And the
bundled StructuralEmbedder deliberately excludes tier and joules: they
are the label side of every row, and a router that could read the
closing tier out of its own features would score perfectly while
learning nothing.
Receipts carry no vector, so the embedder is a trait. The bundled one
is deterministic and offline over receipt structure — it does not
encode query semantics, and says so.
Coupling is the wire format by design: EOC takes no dependency on
JouleClaw and JouleClaw none on EOC.
Verified end to end: emit_corpus → JSONL → the trainer's own loader →
train_logreg and train_mf both produce routers. 14 tests.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
eoc-route-learned: unbreak the build — rand_distr 0.4 pulled rand 0.8
The crate declared rand 0.10 but rand_distr 0.4, which transitively depends on rand 0.8. StdRng from 0.10 therefore did not satisfy rand_distr's Rng bound and the lib failed to compile — five E0277s across classifier.rs, matrix_factorization.rs and bandit.rs. Nothing in the tree depends on eoc-route-learned, so the rot went unnoticed: the router trainer has not compiled in some time. Bump rand_distr to 0.6, which tracks rand 0.10. Normal and Beta are the only distributions used and both carry over unchanged. Tests pass. Co-Authored-By: Claude Opus 4.8 <[email protected]>