2026-10-10 22:23:35 -04:00
16 changed files with 2900 additions and 191 deletions
--- a/.github/workflows/energy-hardware.yml
+++ b/.github/workflows/energy-hardware.yml
@ -33,6 +33,7 @@ on:
      - 'eoc/eoc-rs/crates/eoc-meter/**'
      - 'sandbox/sandbox-rs/crates/sandbox-meter/**'
      - 'sandbox/sandbox-rs/crates/sandbox-exec-microvm/**'
+      - 'sandbox/sandbox-rs/crates/sandbox-proof/**'
      - 'proof/proof-rs/crates/proof-cascade/**'
      - 'jouleclaw/jouleclaw-rs/crates/jouleclaw-energy/**'
      - '.github/workflows/energy-hardware.yml'
@ -44,6 +45,7 @@ on:
      - 'eoc/eoc-rs/crates/eoc-meter/**'
      - 'sandbox/sandbox-rs/crates/sandbox-meter/**'
      - 'sandbox/sandbox-rs/crates/sandbox-exec-microvm/**'
+      - 'sandbox/sandbox-rs/crates/sandbox-proof/**'
      - 'proof/proof-rs/crates/proof-cascade/**'
      - 'jouleclaw/jouleclaw-rs/crates/jouleclaw-energy/**'
      - '.github/workflows/energy-hardware.yml'
@ -106,6 +108,11 @@ jobs:
          log=$(mktemp)
          CARGO_TARGET_DIR="$HOME/hw-target/sandbox-rs" nice -n 10 cargo test -p sandbox-exec-microvm --test rapl_hardware -- --nocapture --test-threads=1 2>&1 | tee "$log"
          grep -q 'package-only inner' "$log" || { echo "::error::sandbox-exec-microvm: the RAPL live path never ran"; exit 1; }
+          # sandbox-proof's accelerator proof: the span over a real workload's
+          # run, its RAPL figure against the package zones read around it.
+          log=$(mktemp)
+          CARGO_TARGET_DIR="$HOME/hw-target/sandbox-rs" nice -n 10 cargo test -p sandbox-proof --lib accelerator -- --nocapture --test-threads=1 2>&1 | tee "$log"
+          grep -q 'RAPL package .* oracle around the call' "$log" || { echo "::error::sandbox-proof: the accelerator span's RAPL path never ran"; exit 1; }

      - name: proof-cascade (RAPL)
        shell: bash
--- a/.github/workflows/standards-build.yml
+++ b/.github/workflows/standards-build.yml
@ -419,3 +419,32 @@ jobs:
          log=$(mktemp)
          cargo test -p jcp-gateway -- --nocapture 2>&1 | tee "$log"
          grep -q 'upstream tree:' "$log"
+
+      # proof-solvers reads each resident z3 decision off z3's own process
+      # tree with that meter (tests/z3_tree.rs, Apple Silicon macOS only, on a
+      # real z3: Homebrew's, on this runner's PATH). The proof-rs matrix entry
+      # runs on Linux, where there is no tree meter, so these run nowhere
+      # else. Each decision they meter prints this line; a missing z3, or a
+      # per-process counter that is not live, prints another, and the grep
+      # fails.
+      - name: proof-solvers (resident z3 process tree)
+        shell: bash
+        working-directory: proof/proof-rs
+        run: |
+          set -o pipefail
+          log=$(mktemp)
+          cargo test -p proof-solvers -- --nocapture 2>&1 | tee "$log"
+          grep -q 'z3 tree meter:' "$log"
+
+      # sandbox-proof's local inference proof meters the engine on its own
+      # process tree, spawned suspended and read before it is reaped. Its
+      # real-engine tests are gated to Apple Silicon macOS; each run they
+      # meter prints this line.
+      - name: sandbox-proof (local engine process tree)
+        shell: bash
+        working-directory: sandbox/sandbox-rs
+        run: |
+          set -o pipefail
+          log=$(mktemp)
+          cargo test -p sandbox-proof -- --nocapture 2>&1 | tee "$log"
+          grep -q 'local engine tree:' "$log"
--- a/joule-code/joule-code-rs/Cargo.lock
+++ b/joule-code/joule-code-rs/Cargo.lock
@ -1899,6 +1899,7 @@ name = "proof-solvers"
 version = "0.1.0"
 dependencies = [
 "proof-schema",
+ "sandbox-meter",
 ]

 [[package]]
--- a/joulecontract/joulecontract-rs/Cargo.lock
+++ b/joulecontract/joulecontract-rs/Cargo.lock
@ -58,6 +58,33 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"

+[[package]]
+name = "ciborium"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "42e69ffd6f0917f5c029256a24d0161db17cea3997d185db0d35926308770f0e"
+dependencies = [
+ "ciborium-io",
+ "ciborium-ll",
+ "serde",
+]
+
+[[package]]
+name = "ciborium-io"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05afea1e0a06c9be33d539b876f1ce3692f4afea2cb41f740e7743225ed1c757"
+
+[[package]]
+name = "ciborium-ll"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57663b653d948a338bfb3eeba9bb2fd5fcfaecb9e199e87e1eda4d9e8b240fd9"
+dependencies = [
+ "ciborium-io",
+ "half",
+]
+
 [[package]]
 name = "const-oid"
 version = "0.9.6"
@ -88,6 +115,12 @@ dependencies = [
 "libc",
 ]

+[[package]]
+name = "crunchy"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "460fbee9c2c2f33933d720630a6a0bac33ba7053db5344fac858d4b8952d77d5"
+
 [[package]]
 name = "crypto-common"
 version = "0.1.7"
@ -203,6 +236,17 @@ dependencies = [
 "wasi",
 ]

+[[package]]
+name = "half"
+version = "2.7.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6ea2d84b969582b4b1864a92dc5d27cd2b77b622a8d79306834f1be5ba20d84b"
+dependencies = [
+ "cfg-if",
+ "crunchy",
+ "zerocopy",
+]
+
 [[package]]
 name = "hex"
 version = "0.4.3"
@ -308,6 +352,16 @@ version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

+[[package]]
+name = "libloading"
+version = "0.8.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55"
+dependencies = [
+ "cfg-if",
+ "windows-link",
+]
+
 [[package]]
 name = "memchr"
 version = "2.8.3"
@ -367,6 +421,7 @@ name = "proof-solvers"
 version = "0.1.0"
 dependencies = [
 "proof-schema",
+ "sandbox-meter",
 ]

 [[package]]
@ -417,6 +472,29 @@ dependencies = [
 "semver",
 ]

+[[package]]
+name = "sandbox-meter"
+version = "0.1.0"
+dependencies = [
+ "ed25519-dalek",
+ "libc",
+ "libloading",
+ "sandbox-schema",
+ "serde",
+ "thiserror",
+]
+
+[[package]]
+name = "sandbox-schema"
+version = "0.1.0"
+dependencies = [
+ "base64",
+ "blake3",
+ "ciborium",
+ "serde",
+ "thiserror",
+]
+
 [[package]]
 name = "semver"
 version = "1.0.28"
@ -574,6 +652,12 @@ version = "0.11.1+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"

+[[package]]
+name = "windows-link"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5"
+
 [[package]]
 name = "zerocopy"
 version = "0.8.56"
--- a/proof/README.md
+++ b/proof/README.md
@ -36,8 +36,8 @@ proof/
 ### The reference implementation (`proof-rs/`)

 - **`proof-schema`** — the content-addressed goal (`blake3(statement‖0x00‖context)`), the cheapest-first tier ladder, the honest energy model (`HwShunt`/`ModelBased`/`Estimator` with the coupling enforced), `SpecGrounding`, the verdict, and the `Solver` trait every backend implements. Canonical det-CBOR content addressing.
- **`proof-solvers`** — two **real** rungs, their energy modeled from measured wall time (`ModelBased`, a ~15 W power model — not a hardware reading): a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it runs a real proof on every spare core and returns its measured microjoules from the first live source — on macOS **this process's own CPU energy counter** (`proc_pid_rusage`'s `ri_energy_nj`, public API, no privilege), read before the workers start and after they are joined, so other processes are excluded by construction and no idle baseline is subtracted; else IOReport's Energy Model, read directly through its C API on Apple Silicon and bracketed against idle; on Linux RAPL's package counters, bracketed against idle — so the headline `joules per verified proof` can be a real reading, not only a model. A vendor or kernel counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it meters anything, by one rule for every source (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): the process counter itself, every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), every RAPL package counter the figure sums (`psys` is neither summed nor probed). Each figure carries its domain: the process counter's is this process's CPU energy only — not other processes, child processes, GPU, ANE or DRAM. Returns nothing where no source is live — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
+- **`proof-solvers`** — two **real** rungs, their energy modeled from measured wall time (`ModelBased`, a ~15 W power model — not a hardware reading): a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). The resident `z3` is the one rung read off hardware: where the kernel counts each process's CPU energy live (macOS), each decision is read off the resident `z3`'s own process tree, and the attempt is that reading (`HwShunt`) only when the reading saw nothing missing — no gap of any kind — the decision ran entirely in the tree, and the operator has declared that the `z3` it runs decides in its own process (`Z3Server::declared_self_contained`; `proof` reads `PROOF_Z3_SELF_CONTAINED=1`) — a tree reading cannot see work handed to a container, VM or remote solver, so a forwarding `z3` would read whole. Otherwise (a gapped reading, no declaration, a refutation whose counter-model a one-shot `z3` fetches outside the tree, Linux) it keeps the model figure and records why, beside the absolute path of the `z3` binary that ran. Each goal is decided as a fresh `z3` would decide it: the answer is read off the crate's own `(check-sat)` before an unpredictable per-goal end marker, an error anywhere is undecided, and the resident session is replaced after any goal that sets an option or is not answered cleanly. Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
+- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed, and a goal's figure graded by the weakest of the attempts it sums), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it runs a real proof on every spare core and returns its measured microjoules from the first live source — on macOS **this process's own CPU energy counter** (`proc_pid_rusage`'s `ri_energy_nj`, public API, no privilege), read before the workers start and after they are joined, so other processes are excluded by construction and no idle baseline is subtracted; else IOReport's Energy Model, read directly through its C API on Apple Silicon and bracketed against idle; on Linux RAPL's package counters, bracketed against idle — so the headline `joules per verified proof` can be a real reading, not only a model. A vendor or kernel counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it meters anything, by one rule for every source (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): the process counter itself, every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), every RAPL package counter the figure sums (`psys` is neither summed nor probed). Each figure carries its domain: the process counter's is this process's CPU energy only — not other processes, child processes, GPU, ANE or DRAM. Returns nothing where no source is live — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
 - **`proof-receipt`** — the `proof/1` JCR-1 receipt: canonical det-CBOR + COSE_Sign1/EdDSA, vendored byte-compatible with the family's cross-language verifiers; refuses to seal an unproved goal.
 - **`proof-conformance`** — C1–C5 + a negative pack, all checks real, published vectors in `conformance/v1/`.
 - **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline — like for like, charged only for the goals the cascade proved, with the all-goals figure and its goal count beside it — the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`) where the meter produces one, and prints which source metered it, its domain, and why each other source was not used; that needs a counter the meter has seen to be live. On the Macs measured so far (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, but this process's CPU energy counter is live, so `--measure` meters with it; the receipt still seals the cascade's own `ModelBased` figure for the first goal. On Linux, RAPL's `energy_uj` is root-only on current kernels.
@ -45,8 +45,9 @@ proof/
 `cargo test --workspace` green; `cargo clippy --workspace --all-targets` is
 warning-free for Linux, and on macOS reports two lints in proof-cascade's
 IOReport FFI. The two bottom rungs decide for real, with energy modeled from
-wall time; the model rungs are honestly marked as stand-ins until inference
-backends are wired.
+wall time (the resident `z3`'s decisions read off its own process tree where
+that reading is whole and the `z3` declared self-contained); the model rungs are honestly marked as stand-ins until
+inference backends are wired.

 ## Honesty the standard records

--- a/proof/SPEC.md
+++ b/proof/SPEC.md
@ -247,6 +247,11 @@ A verified proof SHOULD be memoized by goal id. An identical goal then closes fo
 corpus of verified proofs — not the routing — is the durable asset. The cache is
 the energy flywheel: the more proved, the cheaper future proofs become.

+A cache hit's zero is not a reading: nothing was metered to close it. Its
+`energy_provenance` **MUST** be `Estimator`, never the grade of the solver that
+closed the goal when it was first proved, so a hit can never be graded above the
+proof it reuses or present a measured zero.
+
 ## 8. Conformance

 A conforming implementation passes, with real checks:
--- a/proof/proof-rs/Cargo.lock
+++ b/proof/proof-rs/Cargo.lock
@ -8,6 +8,12 @@ version = "0.7.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d3fb67a6e08acf24fdeccbac2cb6ac4305825bd1f117462e0e6f2f193345ad56"

+[[package]]
+name = "base64"
+version = "0.22.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
+
 [[package]]
 name = "base64ct"
 version = "1.8.3"
@ -52,6 +58,33 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"

+[[package]]
+name = "ciborium"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "42e69ffd6f0917f5c029256a24d0161db17cea3997d185db0d35926308770f0e"
+dependencies = [
+ "ciborium-io",
+ "ciborium-ll",
+ "serde",
+]
+
+[[package]]
+name = "ciborium-io"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05afea1e0a06c9be33d539b876f1ce3692f4afea2cb41f740e7743225ed1c757"
+
+[[package]]
+name = "ciborium-ll"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57663b653d948a338bfb3eeba9bb2fd5fcfaecb9e199e87e1eda4d9e8b240fd9"
+dependencies = [
+ "ciborium-io",
+ "half",
+]
+
 [[package]]
 name = "const-oid"
 version = "0.9.6"
@ -82,6 +115,12 @@ dependencies = [
 "libc",
 ]

+[[package]]
+name = "crunchy"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "460fbee9c2c2f33933d720630a6a0bac33ba7053db5344fac858d4b8952d77d5"
+
 [[package]]
 name = "crypto-common"
 version = "0.1.7"
@ -197,6 +236,17 @@ dependencies = [
 "wasi",
 ]

+[[package]]
+name = "half"
+version = "2.7.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6ea2d84b969582b4b1864a92dc5d27cd2b77b622a8d79306834f1be5ba20d84b"
+dependencies = [
+ "cfg-if",
+ "crunchy",
+ "zerocopy",
+]
+
 [[package]]
 name = "hex"
 version = "0.4.3"
@ -215,6 +265,16 @@ version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"

+[[package]]
+name = "libloading"
+version = "0.8.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55"
+dependencies = [
+ "cfg-if",
+ "windows-link",
+]
+
 [[package]]
 name = "memchr"
 version = "2.8.3"
@ -302,8 +362,10 @@ dependencies = [
 name = "proof-solvers"
 version = "0.1.0"
 dependencies = [
+ "libc",
 "proof-cascade",
 "proof-schema",
+ "sandbox-meter",
 ]

 [[package]]
@ -333,6 +395,29 @@ dependencies = [
 "semver",
 ]

+[[package]]
+name = "sandbox-meter"
+version = "0.1.0"
+dependencies = [
+ "ed25519-dalek",
+ "libc",
+ "libloading",
+ "sandbox-schema",
+ "serde",
+ "thiserror",
+]
+
+[[package]]
+name = "sandbox-schema"
+version = "0.1.0"
+dependencies = [
+ "base64",
+ "blake3",
+ "ciborium",
+ "serde",
+ "thiserror",
+]
+
 [[package]]
 name = "semver"
 version = "1.0.28"
@ -490,6 +575,32 @@ version = "0.11.1+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"

+[[package]]
+name = "windows-link"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.62"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "86502bf56ac7c77571a32e2647bb2a15894565e981fb2a48d7bde2d91c965a9d"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.62"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5457206954b06561e2608c7e19cf58b1926586d999c246eebe4502f7e2039d1a"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+]
+
 [[package]]
 name = "zeroize"
 version = "1.9.0"
--- a/proof/proof-rs/crates/proof-cascade/src/lib.rs
+++ b/proof/proof-rs/crates/proof-cascade/src/lib.rs
@ -34,8 +34,18 @@ pub struct CascadeResult {
    pub proved: bool,
    pub closed_by: Option<Tier>,
    pub artifact: Option<ContentId>,
-    /// The provenance of the closing solver's energy reading (the honest tag for
-    /// the proof's headline cost). `Estimator` when unproved or served from cache.
+    /// The provenance of the proof's headline cost, `total_uj`: the weakest of
+    /// the attempts it sums, the closing one and every cheaper one that failed
+    /// before it, because a sum is only as good as its weakest part. It is the
+    /// closing solver's own whenever every earlier attempt was graded at least
+    /// as well, which holds on any ladder whose rungs share one grade. A rung
+    /// that reads hardware (`HwShunt`) above one that models its figure
+    /// therefore seals as `ModelBased` while the modelled waste is in the
+    /// total, never as a hardware reading of it. `Estimator` when unproved,
+    /// and for a proof served from cache: a hit's `total_uj` of 0 is the
+    /// lookup's nominal cost, nothing read and nothing modelled, so it never
+    /// carries the grade of the solver whose proof it serves — a hardware
+    /// grade there would seal a measured zero for a span nothing metered.
    pub provenance: Provenance,
    /// Total joules spent closing this goal, including failed cheaper attempts.
    pub total_uj: u64,
@ -135,7 +145,12 @@ impl CascadeResult {
 pub struct CachedProof {
    pub closed_by: Tier,
    pub artifact: ContentId,
+    /// The closing solver's own figure for the proof.
    pub uj: u64,
+    /// The grade of `uj`, the closing solver's own, and of nothing else. A
+    /// hit never carries it ([`CascadeResult::provenance`]): it spends no new
+    /// joules and reads nothing. Cache files written when a hit did carry it
+    /// load unchanged, since the stored field always meant this.
    pub provenance: Provenance,
    /// The proof came from a reference stand-in. Persisted with the entry so a
    /// cache hit cannot launder an unearned proof into an unmarked one — the
@ -219,6 +234,23 @@ impl ProofCache {
    }
 }

+/// The weaker of two grades (`Estimator` < `ModelBased` < `HwShunt`): the
+/// grade a sum of figures graded `a` and `b` can honestly carry.
+fn weaker(a: Provenance, b: Provenance) -> Provenance {
+    fn rank(p: Provenance) -> u8 {
+        match p {
+            Provenance::Estimator => 0,
+            Provenance::ModelBased => 1,
+            Provenance::HwShunt => 2,
+        }
+    }
+    if rank(b) < rank(a) {
+        b
+    } else {
+        a
+    }
+}
+
 /// The cascade router: solvers sorted cheapest-first.
 pub struct Router {
    solvers: Vec<Box<dyn Solver>>,
@ -270,7 +302,8 @@ impl Router {
                proved: true,
                closed_by: Some(c.closed_by),
                artifact: Some(c.artifact),
-                provenance: c.provenance,
+                // Nothing was read or modelled for this zero.
+                provenance: Provenance::Estimator,
                // A cache hit spends nothing, so no ceiling can be breached by
                // it — but the ceiling that was in force is still recorded, so
                // a reader can tell a free hit from an unbounded run.
@ -293,6 +326,9 @@ impl Router {
        let mut closed_by = None;
        let mut artifact = None;
        let mut provenance = Provenance::Estimator; // until a solver closes it
+        // The weakest grade among the attempts summed so far: the grade
+        // `total_uj` can honestly carry once a solver closes the goal.
+        let mut weakest: Option<Provenance> = None;
        let mut refuted = false;
        let mut counter_model = None;
        let mut closed_by_stub = false;
@ -314,6 +350,7 @@ impl Router {
            let a = solver.attempt(goal);
            let uj = a.energy.uj();
            total_uj = total_uj.saturating_add(uj);
+            weakest = Some(weakest.map_or(a.energy.provenance, |w| weaker(w, a.energy.provenance)));
            let proved = a.verdict.is_proved();
            attempts.push(AttemptRecord {
                tier: a.tier,
@ -326,14 +363,16 @@ impl Router {
                    closed_by = Some(a.tier);
                    closed_by_stub = solver.is_reference_stub();
                    artifact = Some(art);
-                    provenance = a.energy.provenance;
+                    provenance = weakest.unwrap_or(a.energy.provenance);
                    cache.insert(
                        goal_id.clone(),
                        CachedProof {
                            closed_by: a.tier,
                            artifact: art,
                            uj,
-                            provenance,
+                            // The cached figure is the closing solver's
+                            // alone, so it keeps that solver's grade.
+                            provenance: a.energy.provenance,
                            closed_by_stub,
                        },
                    );
@ -768,4 +807,109 @@ mod tests {
        assert!(s.saved_uj() > 0);
        assert!(s.energy_ratio_milli() > 1000); // > 1× cheaper than frontier-only
    }
+
+    /// A rung that reports a fixed figure at a fixed grade, proving or not.
+    struct Graded {
+        tier: Tier,
+        proves: bool,
+        energy: Energy,
+    }
+    impl Solver for Graded {
+        fn tier(&self) -> Tier {
+            self.tier
+        }
+        fn attempt(&self, _goal: &ProofGoal) -> Attempt {
+            let verdict = if self.proves {
+                Verdict::Proved { artifact: ContentId::of_bytes(b"graded") }
+            } else {
+                Verdict::Unproved
+            };
+            Attempt { tier: self.tier, verdict, energy: self.energy }
+        }
+    }
+
+    /// The headline cost sums every attempt, so it carries the weakest grade
+    /// among them: a hardware reading at T1 above a modelled failure at T0
+    /// seals as `ModelBased`, never as a hardware reading of a total that
+    /// holds a model. The cached proof keeps the closing solver's own grade,
+    /// because its figure is that solver's alone.
+    #[test]
+    fn the_headline_cost_carries_the_weakest_grade_it_sums() {
+        let run = |below: Energy, closer: Energy| {
+            let solvers: Vec<Box<dyn Solver>> = vec![
+                Box::new(Graded { tier: Tier::Automation, proves: false, energy: below }),
+                Box::new(Graded { tier: Tier::Smt, proves: true, energy: closer }),
+            ];
+            let mut cache = ProofCache::new();
+            let goal = ProofGoal::new("(assert false)", "smt2", GoalKind::Decidable);
+            let r = Router::new(solvers).prove(&goal, &mut cache);
+            let cached = cache.get(&r.goal_id).cloned().expect("the proof is cached");
+            (r, cached)
+        };
+        // Modelled waste under a hardware reading: the sum is modelled.
+        let (r, cached) = run(Energy::modeled(3), Energy::measured(4_000));
+        assert_eq!((r.total_uj, r.wasted_uj), (4_003, 3));
+        assert_eq!(r.provenance, Provenance::ModelBased);
+        assert_eq!(r.attempts.iter().map(|a| a.provenance).collect::<Vec<_>>(), vec![Provenance::ModelBased, Provenance::HwShunt]);
+        assert_eq!((cached.uj, cached.provenance), (4_000, Provenance::HwShunt));
+        // Hardware all the way: hardware.
+        let (r, _) = run(Energy::measured(2), Energy::measured(4_000));
+        assert_eq!(r.provenance, Provenance::HwShunt);
+        // An estimated attempt anywhere in the sum makes it an estimate.
+        let (r, cached) = run(Energy::estimate_tier(Tier::Automation), Energy::modeled(900));
+        assert_eq!(r.provenance, Provenance::Estimator);
+        assert_eq!(cached.provenance, Provenance::ModelBased);
+        // A better-graded failure under a worse-graded closer: the closer's.
+        let (r, _) = run(Energy::measured(2), Energy::modeled(900));
+        assert_eq!(r.provenance, Provenance::ModelBased);
+        // A proof served from the cache: its zero is not a reading of
+        // anything, so it is an estimate, never better than the proof it
+        // serves (which here sealed ModelBased, T0's model in its total).
+        let mut cache = ProofCache::new();
+        let goal = ProofGoal::new("(assert true)", "smt2", GoalKind::Decidable);
+        let ladder = || -> Vec<Box<dyn Solver>> {
+            vec![
+                Box::new(Graded { tier: Tier::Automation, proves: false, energy: Energy::modeled(3) }),
+                Box::new(Graded { tier: Tier::Smt, proves: true, energy: Energy::measured(4_000) }),
+            ]
+        };
+        let first = Router::new(ladder()).prove(&goal, &mut cache);
+        let hit = Router::new(ladder()).prove(&goal, &mut cache);
+        assert_eq!((first.provenance, first.from_cache), (Provenance::ModelBased, false));
+        assert_eq!((hit.provenance, hit.from_cache, hit.total_uj), (Provenance::Estimator, true, 0));
+    }
+
+    /// A cache hit spends no new joules and reads nothing, so its zero is
+    /// never sealed with a hardware grade: not when the closing solver read
+    /// hardware (even a ladder that is hardware all the way), and not from
+    /// a cache file written before this rule, whose stored grade is the
+    /// closing solver's own. The stored grade still loads, and still
+    /// qualifies the stored figure alone.
+    #[test]
+    fn a_cache_hit_never_seals_its_zero_as_a_reading() {
+        let hw = || -> Vec<Box<dyn Solver>> {
+            vec![Box::new(Graded { tier: Tier::Smt, proves: true, energy: Energy::measured(4_000) })]
+        };
+        let goal = ProofGoal::new("(assert false)", "smt2", GoalKind::Decidable);
+        let mut cache = ProofCache::new();
+        let first = Router::new(hw()).prove(&goal, &mut cache);
+        assert_eq!(first.provenance, Provenance::HwShunt, "a whole hardware ladder is a reading");
+        let hit = Router::new(hw()).prove(&goal, &mut cache);
+        assert_eq!((hit.from_cache, hit.total_uj, hit.provenance), (true, 0, Provenance::Estimator));
+
+        // A cache file from before: the closing solver's HwShunt stored.
+        let line = format!(
+            r#"{{"goal_id":"{}","proof":{{"closed_by":"Smt","artifact":{},"uj":4000,"provenance":"HwShunt"}}}}"#,
+            first.goal_id,
+            serde_json::to_string(&first.artifact.expect("an artifact")).expect("artifact json"),
+        );
+        let mut old = ProofCache::new();
+        old.load_jsonl(&line);
+        let stored = old.get(&first.goal_id).cloned().expect("an older cache line still loads");
+        assert_eq!((stored.uj, stored.provenance, stored.closed_by_stub), (4_000, Provenance::HwShunt, false));
+        let hit = Router::new(Vec::new()).prove(&goal, &mut old);
+        assert_eq!((hit.from_cache, hit.proved, hit.total_uj, hit.provenance), (true, true, 0, Provenance::Estimator));
+        // And the round trip writes the same stored grade back.
+        assert_eq!(old.to_jsonl(), cache.to_jsonl());
+    }
 }
--- a/proof/proof-rs/crates/proof-cli/src/main.rs
+++ b/proof/proof-rs/crates/proof-cli/src/main.rs
@ -1,9 +1,18 @@
 //! `proof` — a headless demonstration of the energy-optimized cascade.
 //!
 //! Runs a proof workload through the cheapest-sufficient ladder — the T0
-//! propositional decider and T1 resident `z3`, both real deciders whose energy
-//! is modeled, not measured: each attempt's wall time × proof-solvers' ~15 W
-//! power model, tagged `ModelBased`. There is no T2/T3 rung, so goals that need
+//! propositional decider and T1 resident `z3`, both real deciders. T0's
+//! energy is modeled, not measured: each attempt's wall time × proof-solvers'
+//! ~15 W power model, tagged `ModelBased`. T1's is the same model, except
+//! where this host reads the resident `z3`'s own process tree (macOS, with
+//! the kernel's per-process energy counter live), the decision's reading
+//! saw nothing missing, and the operator has declared that the `z3` on
+//! `PATH` decides each goal in its own process (`PROOF_Z3_SELF_CONTAINED=1`:
+//! no container, VM or remote solver behind it, which no reading of the
+//! tree could show): then that attempt is the reading, `HwShunt`. A goal's
+//! figure sums every attempt on it, so an SMT goal, which T0 tries first and
+//! fails, is still `ModelBased`: its total holds T0's modelled attempt.
+//! There is no T2/T3 rung, so goals that need
 //! one come back unproved. It reports, per goal, the tier that closed it and
 //! the joules it cost; then the headline — joules spent versus a frontier-only
 //! run charged for the goals the cascade proved, the same verified output,
@ -21,7 +30,10 @@ use proof_solvers::{resident_z3_ladder, z3_available};

 fn main() {
    let measure = std::env::args().any(|a| a == "--measure");
-    let router = Router::new(resident_z3_ladder());
+    // The operator's declaration about the `z3` on PATH. Without it no T1
+    // decision is sealed as a hardware reading, whole or not.
+    let z3_self_contained = std::env::var("PROOF_Z3_SELF_CONTAINED").as_deref() == Ok("1");
+    let router = Router::new(resident_z3_ladder(z3_self_contained));
    let mut cache = ProofCache::new();
    let mut summary = EnergySummary::default();

@ -48,7 +60,11 @@ fn main() {

    println!(
        "proof — cheapest-sufficient cascade (T0 prop + T1 z3 are real; z3 {})\n",
-        if z3_available() { "present" } else { "ABSENT — T1 goals escalate" }
+        match (z3_available(), z3_self_contained) {
+            (false, _) => "ABSENT — T1 goals escalate",
+            (true, true) => "present, declared self-contained",
+            (true, false) => "present, not declared self-contained: T1 stays modelled (PROOF_Z3_SELF_CONTAINED=1 declares it)",
+        }
    );
    let mut first = None;
    for (statement, kind, label) in workload {
--- a/proof/proof-rs/crates/proof-solvers/Cargo.toml
+++ b/proof/proof-rs/crates/proof-solvers/Cargo.toml
@ -8,6 +8,10 @@ rust-version.workspace = true

 [dependencies]
 proof-schema = { workspace = true }
+# The resident z3's own process tree is metered with the family's tree meter
+# (the kernel's per-process CPU energy count, read for every member): the same
+# meter, by the same path, as jcp-gateway's upstream server.
+sandbox-meter = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-meter" }

 # 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
@ -15,6 +19,9 @@ proof-schema = { workspace = true }
 # so there is no cycle.
 [dev-dependencies]
 proof-cascade = { workspace = true }
+# tests/z3_tree.rs's oracle reads the resident z3's energy count with
+# proc_pid_rusage into a raw buffer, sharing no code with the meter.
+libc = "0.2"

 [lints]
 workspace = true
--- a/proof/proof-rs/crates/proof-solvers/src/lib.rs
+++ b/proof/proof-rs/crates/proof-solvers/src/lib.rs
--- a/proof/proof-rs/crates/proof-solvers/tests/z3_tree.rs
+++ b/proof/proof-rs/crates/proof-solvers/tests/z3_tree.rs
@ -0,0 +1,290 @@
+//! The resident `z3`'s decisions read off its own process tree, on a real
+//! `z3`. Each test starts a [`Z3Server`] of its own and decides real SMT-LIB
+//! goals on it.
+//!
+//! The oracle shares no code with the meter or the server: the resident
+//! `z3`'s `proc_pid_rusage(pid, RUSAGE_INFO_V6)` read into a raw buffer and
+//! taken at the SDK's byte offset (energy at 336), read before and after each
+//! attempt once `z3` is quiet on the oracle's own terms: no thread on a core
+//! or queued (`proc_pidinfo(PROC_PIDTASKINFO)` into a raw buffer,
+//! `pti_numrunning` at byte 88) at two reads 20 ms apart whose energy agrees.
+//! A resident `z3` blocked on its next read does not move its count, so
+//! between the meter's reads and the oracle's nothing is spent: a decision's
+//! reading must EQUAL the oracle's advance across the attempt, to the
+//! nanojoule, and the attempt's `HwShunt` figure must be that advance rounded
+//! UP to a whole µJ.
+//!
+//! Every server here but one is declared self-contained
+//! ([`Z3Server::declared_self_contained`]): the Homebrew `z3` these tests run
+//! is the solver itself, deciding in its own process. The one undeclared
+//! server shows that a whole reading is never sealed without it.
+//!
+//! Without `z3` on `PATH` there is nothing to decide, and each test says so
+//! and returns; CI's proof-rs legs install `z3`. The tests log what they saw
+//! (`z3 tree meter:`), and run one at a time (a lock) so one test's solver is
+//! not loading the host under another's.
+
+#![cfg(all(target_os = "macos", target_arch = "aarch64"))]
+
+use proof_schema::{Energy, GoalKind, ProofGoal, Provenance, Solver, Verdict};
+use proof_solvers::{z3_available, Modelled, Z3Server};
+use sandbox_meter::{process_energy_status, CounterStatus};
+use std::sync::{Mutex, MutexGuard};
+use std::time::{Duration, Instant};
+
+static ONE_AT_A_TIME: Mutex<()> = Mutex::new(());
+
+fn alone() -> MutexGuard<'static, ()> {
+    ONE_AT_A_TIME.lock().unwrap_or_else(|e| e.into_inner())
+}
+
+/// How long the meter may wait for `z3` to go quiet in these tests: far past
+/// the production bound, because the host runs at a load of 14 to 260 and a
+/// reply's tail can wait that long for a core. A `z3` still running after it
+/// is a gap, which fails a test that expects a whole reading: a whole
+/// reading is never a stale one.
+const TEST_SETTLE: Duration = Duration::from_secs(2);
+
+/// `pid`'s `rusage_info_v6`, raw: `proc_pid_rusage(pid, 6)` into a buffer
+/// larger than the struct's 464 bytes, as 64-bit words.
+fn oracle_rusage(pid: i32) -> Option<[u64; 64]> {
+    let mut buf = [0u64; 64];
+    // SAFETY: `buf` is writable and larger than `rusage_info_v6`.
+    let rc = unsafe { libc::proc_pid_rusage(pid, 6, buf.as_mut_ptr() as *mut libc::rusage_info_t) };
+    (rc == 0).then_some(buf)
+}
+
+fn energy_nj(ru: &[u64; 64]) -> u64 {
+    ru[336 / 8]
+}
+
+/// `pti_numrunning` of `pid`: `proc_pidinfo(pid, PROC_PIDTASKINFO = 4)` into
+/// a raw 96-byte buffer, the int32 at byte 88.
+fn oracle_running(pid: i32) -> Option<i32> {
+    let mut buf = [0u8; 96];
+    // SAFETY: `buf` is writable for the 96 bytes passed.
+    let n = unsafe { libc::proc_pidinfo(pid, 4, 0, buf.as_mut_ptr().cast(), 96) };
+    (n == 96).then(|| i32::from_ne_bytes(buf[88..92].try_into().unwrap()))
+}
+
+/// `pid`'s energy count once it is quiet by the oracle's rule: not running
+/// or queued at two reads 20 ms apart, with the same energy at both. Panics
+/// after 20 s.
+fn quiet_energy(pid: i32) -> u64 {
+    let deadline = Instant::now() + Duration::from_secs(20);
+    loop {
+        let first = oracle_rusage(pid).expect("oracle read");
+        let before = oracle_running(pid) == Some(0);
+        std::thread::sleep(Duration::from_millis(20));
+        let second = oracle_rusage(pid).expect("oracle read");
+        let after = oracle_running(pid) == Some(0);
+        if before && after && energy_nj(&first) == energy_nj(&second) {
+            return energy_nj(&second);
+        }
+        assert!(Instant::now() < deadline, "the oracle never saw z3 (pid {pid}) quiet");
+    }
+}
+
+/// Valid claims, each asserted negated: `unsat`, so proved.
+fn theorems() -> Vec<(&'static str, ProofGoal)> {
+    let goal = |s: &str| ProofGoal::new(s, "smt2", GoalKind::Decidable);
+    vec![
+        ("x>0 → x≥0", goal("(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))")),
+        ("a+b = b+a", goal("(declare-const a Int)(declare-const b Int)\n(assert (not (= (+ a b) (+ b a))))")),
+        (
+            "3x = x+x+x (bv32)",
+            goal(
+                "(declare-const x (_ BitVec 32))\n\
+                 (assert (not (= (bvmul x #x00000003) (bvadd x (bvadd x x)))))",
+            ),
+        ),
+    ]
+}
+
+/// The server for a test, or `None` (said) when there is no `z3` to decide
+/// with. On a host whose per-process counter is not live there is no tree
+/// meter, and an attempt keeps the model and says why: checked here, so
+/// that branch also asserts before the test returns.
+fn server(bound: Duration) -> Option<Z3Server> {
+    if !z3_available() {
+        eprintln!("z3 not installed: no resident z3 to meter");
+        return None;
+    }
+    let server = Z3Server::new().with_settle_bound(bound).declared_self_contained(true);
+    let status = process_energy_status();
+    if status != CounterStatus::Live {
+        assert!(!server.is_tree_metered(), "a tree meter without a live counter ({status:?})");
+        let (_, goal) = &theorems()[0];
+        let a = server.attempt(goal);
+        let acct = server.last_account().expect("an account");
+        eprintln!("z3 resident (counter {status:?}): {acct:?}");
+        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj));
+        assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]);
+        return None;
+    }
+    assert!(server.is_tree_metered(), "the per-process counter is live, yet no tree meter for z3");
+    Some(server)
+}
+
+/// Each resident decision of a proved goal is read whole off `z3`'s tree
+/// and sealed `HwShunt`: the reading equals the oracle's advance across the
+/// attempt to the nanojoule, and the attempt's figure is that advance
+/// rounded up to the µJ.
+#[test]
+fn a_resident_decision_is_hwshunt_and_equals_the_oracle() {
+    let _one = alone();
+    let Some(server) = server(TEST_SETTLE) else { return };
+    let pid = server.pid().expect("a resident z3") as i32;
+    for rep in 0..4 {
+        for (name, goal) in theorems() {
+            let before = quiet_energy(pid);
+            let a = server.attempt(&goal);
+            let after = quiet_energy(pid);
+            let oracle = after - before;
+            let acct = server.last_account().expect("an account of the attempt");
+            let r = acct.reading.clone().expect("a span was opened").expect("a reading");
+            eprintln!(
+                "z3 tree meter: {name} rep {rep}: {} nJ over {:?}, oracle {oracle} nJ, sealed {:?}, work {:?}, overhead {:?}, gaps {:?}",
+                r.cpu_nj, r.pids, a.energy, acct.work, acct.overhead, r.gaps
+            );
+            assert!(a.verdict.is_proved(), "{name}: {:?}", a.verdict);
+            assert!(r.is_whole(), "{name}: the resident z3 was not read whole: {:?}", r.gaps);
+            assert_eq!(r.pids, vec![pid as u32], "{name}: z3 is a single process");
+            assert_eq!(r.cpu_nj, oracle, "{name}: the reading is not the oracle's advance");
+            assert!(acct.modelled_because.is_empty(), "{name}: {:?}", acct.modelled_because);
+            assert_eq!(a.energy, Energy::measured(oracle.div_ceil(1_000)), "{name}");
+            assert_eq!(a.energy.provenance, Provenance::HwShunt);
+            assert!(a.energy.check_provenance().is_ok());
+        }
+    }
+}
+
+/// A refuted goal: the resident `z3` decides `sat`, and a one-shot `z3`,
+/// outside the resident tree, fetches the counter-model. The span read the
+/// resident decision alone — exactly the oracle's advance on the resident
+/// `z3`, no other process in it — and the attempt keeps the model figure
+/// for the whole attempt, saying why.
+#[test]
+fn a_refuted_goal_keeps_the_model_because_its_counter_model_ran_outside_the_tree() {
+    let _one = alone();
+    let Some(server) = server(TEST_SETTLE) else { return };
+    let pid = server.pid().expect("a resident z3") as i32;
+    let not_thm = ProofGoal::new("(declare-const x Int)\n(assert (not (> x 0)))", "smt2", GoalKind::Decidable);
+    for rep in 0..3 {
+        let before = quiet_energy(pid);
+        let a = server.attempt(&not_thm);
+        let after = quiet_energy(pid);
+        let oracle = after - before;
+        let acct = server.last_account().expect("an account of the attempt");
+        let r = acct.reading.clone().expect("a span was opened").expect("a reading");
+        eprintln!(
+            "z3 tree meter: refuted rep {rep}: resident {} nJ over {:?}, oracle {oracle} nJ, sealed {:?}, work {:?}, because {:?}",
+            r.cpu_nj, r.pids, a.energy, acct.work, acct.modelled_because
+        );
+        assert!(matches!(a.verdict, Verdict::Refuted { .. }), "{:?}", a.verdict);
+        assert_eq!(acct.modelled_because, vec![Modelled::CounterModelOutsideTree]);
+        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj));
+        assert_eq!(a.energy.provenance, Provenance::ModelBased);
+        assert!(r.is_whole(), "{:?}", r.gaps);
+        assert_eq!(r.pids, vec![pid as u32], "the one-shot z3 is not in the resident tree");
+        assert_eq!(r.cpu_nj, oracle, "the span is the resident decision alone");
+    }
+}
+
+/// The production settle bound, on this host as it is: what the metering
+/// adds to a goal's latency, and how often a decision is read whole. Every
+/// attempt is graded consistently either way — a whole reading `HwShunt` at
+/// its rounded-up figure, a gapped one the model with its gaps — and the
+/// numbers are logged for the record rather than asserted, because they
+/// depend on the host's load.
+#[test]
+fn the_production_settle_bound_grades_every_attempt_consistently() {
+    let _one = alone();
+    let Some(server) = server(sandbox_meter::probe::SETTLE_BOUND) else { return };
+    let mut overheads: Vec<Duration> = Vec::new();
+    let mut works: Vec<Duration> = Vec::new();
+    let (mut whole, mut gapped) = (0, 0);
+    for _ in 0..10 {
+        for (name, goal) in theorems() {
+            let a = server.attempt(&goal);
+            assert!(a.verdict.is_proved(), "{name}");
+            let acct = server.last_account().expect("an account of the attempt");
+            let r = acct.reading.clone().expect("a span was opened").expect("a reading");
+            if r.is_whole() {
+                whole += 1;
+                assert_eq!(a.energy, Energy::measured(r.cpu_nj.div_ceil(1_000)), "{name}");
+                assert!(acct.modelled_because.is_empty());
+            } else {
+                gapped += 1;
+                assert_eq!(a.energy, Energy::modeled(acct.modelled_uj), "{name}: {:?}", r.gaps);
+                assert_eq!(acct.modelled_because, vec![Modelled::Gaps(r.gaps.clone())]);
+            }
+            overheads.push(acct.overhead);
+            works.push(acct.work);
+        }
+    }
+    overheads.sort_unstable();
+    works.sort_unstable();
+    let n = overheads.len();
+    eprintln!(
+        "z3 tree meter: production bound {:?}: {whole} whole, {gapped} gapped of {n}; overhead per goal median {:?} p90 {:?} max {:?}; solver work median {:?} max {:?}",
+        sandbox_meter::probe::SETTLE_BOUND,
+        overheads[n / 2],
+        overheads[n * 9 / 10],
+        overheads[n - 1],
+        works[n / 2],
+        works[n - 1]
+    );
+}
+
+/// Through the cascade: an SMT goal fails the T0 propositional decider (its
+/// figure modelled) and is proved by the resident `z3` (read whole,
+/// `HwShunt`). The goal's headline cost sums both, so it is sealed
+/// `ModelBased`, never as a hardware reading of a total that holds a model;
+/// the T1 attempt's own record keeps its hardware grade.
+#[test]
+fn a_cascade_total_holding_modelled_waste_is_not_sealed_as_hardware() {
+    use proof_cascade::{ProofCache, Router};
+    use proof_solvers::Propositional;
+    let _one = alone();
+    let Some(server) = server(TEST_SETTLE) else { return };
+    let router = Router::new(vec![Box::new(Propositional), Box::new(server)]);
+    let (_, goal) = &theorems()[1];
+    let r = router.prove(goal, &mut ProofCache::new());
+    eprintln!(
+        "z3 tree meter: cascade: total {} uj ({} wasted) sealed {:?}, attempts {:?}",
+        r.total_uj, r.wasted_uj, r.provenance, r.attempts
+    );
+    assert!(r.proved);
+    let grades: Vec<Provenance> = r.attempts.iter().map(|a| a.provenance).collect();
+    assert_eq!(grades, vec![Provenance::ModelBased, Provenance::HwShunt]);
+    assert_eq!(r.provenance, Provenance::ModelBased);
+}
+
+/// Without its operator's declaration, a resident decision read whole off
+/// `z3`'s tree is NOT sealed as hardware. The tree cannot show work handed
+/// outside it: a `z3` on `PATH` that forwards each goal to a solver in a
+/// container or on another host reads whole here (only the forwarding
+/// client is in the tree) while the decision's energy is charged elsewhere.
+#[test]
+fn an_undeclared_resident_decision_keeps_the_model() {
+    let _one = alone();
+    if !z3_available() || process_energy_status() != CounterStatus::Live {
+        eprintln!("no z3, or no live per-process counter: nothing to seal either way");
+        return;
+    }
+    let server = Z3Server::new().with_settle_bound(TEST_SETTLE);
+    for (name, goal) in theorems() {
+        let a = server.attempt(&goal);
+        assert!(a.verdict.is_proved(), "{name}");
+        let acct = server.last_account().expect("an account of the attempt");
+        eprintln!("z3 tree meter: undeclared {name}: sealed {:?}, because {:?}", a.energy, acct.modelled_because);
+        assert_eq!(a.energy.provenance, Provenance::ModelBased, "{name}: an undeclared z3 was sealed as hardware");
+        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj), "{name}");
+        let r = acct.reading.clone().expect("a span was opened").expect("a reading");
+        let mut want = if r.is_whole() { Vec::new() } else { vec![Modelled::Gaps(r.gaps.clone())] };
+        want.push(Modelled::NotDeclaredSelfContained);
+        assert_eq!(acct.modelled_because, want, "{name}");
+        assert!(acct.z3.as_ref().is_some_and(|p| p.is_absolute()), "{name}: {:?}", acct.z3);
+    }
+}
--- a/sandbox/sandbox-rs/Cargo.lock
+++ b/sandbox/sandbox-rs/Cargo.lock
@ -1827,6 +1827,7 @@ dependencies = [
 "blake3",
 "ed25519-dalek",
 "hex",
+ "libc",
 "sandbox-attest",
 "sandbox-capability",
 "sandbox-conformance",
--- a/sandbox/sandbox-rs/crates/sandbox-proof/Cargo.toml
+++ b/sandbox/sandbox-rs/crates/sandbox-proof/Cargo.toml
@ -28,3 +28,10 @@ ureq.workspace = true
 hex.workspace = true
 blake3.workspace = true
 thiserror.workspace = true
+
+# macOS: the local engine is spawned suspended (posix_spawn), so its tree
+# meter's start walk is read before it runs, and waited for without reaping
+# (waitid WNOWAIT), so its exited record is read before it goes. The tests'
+# oracle reads proc_pid_rusage into a raw buffer with it too.
+[target.'cfg(target_os = "macos")'.dependencies]
+libc = "0.2"
--- a/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs
+++ b/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs
--- a/sandbox/sandbox-rs/crates/sandbox-proof/src/main.rs
+++ b/sandbox/sandbox-rs/crates/sandbox-proof/src/main.rs
@ -159,11 +159,16 @@ fn prove_local(path: &str) {
        Ok(p) => Some(std::path::PathBuf::from(p)),
        Err(_) => Some(std::env::temp_dir().join("sandbox-proof-weights-hash.json")),
    };
+    // The operator's declaration that the engine hands no work to another
+    // process (`SANDBOX_LOCAL_SELF_CONTAINED=1`): without it, the engine's
+    // own process-tree reading is never sealed.
+    let engine_self_contained = std::env::var("SANDBOX_LOCAL_SELF_CONTAINED").as_deref() == Ok("1");
    let inputs = sandbox_proof::LocalInferenceInputs {
        engine,
        args,
        weights,
        hash_cache,
+        engine_self_contained,
    };
    let cloud = env("SANDBOX_CLOUD", "local");
    let cell = match sandbox_proof::prove_local(&inputs, &cloud, now_us(), &proof_key()) {
@ -188,8 +193,10 @@ fn prove_local(path: &str) {
    println!("\n  appended to {path}");
 }

-/// Prove the accelerator (GPU) fabric: run a GPU workload, meter it via
-/// nvidia-smi, seal a cell with a separate Gpu energy record + GPU identity.
+/// Prove the accelerator (GPU) fabric: run a GPU workload, meter its run
+/// machine-wide (RAPL + NVML where live, else the estimator and nvidia-smi
+/// power samples), seal a cell with a separate Gpu energy record + GPU
+/// identity.
 fn prove_gpu(path: &str) {
    let secs: u64 = std::env::var("SANDBOX_GPU_SECS")
        .ok()
@ -197,10 +204,11 @@ fn prove_gpu(path: &str) {
        .unwrap_or(5);
    let cmd = std::env::var("SANDBOX_GPU_CMD").unwrap_or_else(|_| "gpu_load.exe".to_string());
    let cloud = std::env::var("SANDBOX_CLOUD").unwrap_or_else(|_| "local".to_string());
+    // `secs` is the workload's own argument (how long to load the GPU); the
+    // energy span is the workload's actual run, however long that is.
    let cell = match sandbox_proof::prove_accelerator(
        &cmd,
        vec![secs.to_string()],
-        secs,
        &cloud,
        now_us(),
        &proof_key(),