proof: z3 could be made to prove a false claim; meter solver subprocesses where they ran #213
2026-10-10
proof SPEC §7: a cache hit's zero is sealed Estimator
All checks were successful
energy meters on real hardware / RAPL and NVML on jetson-hub (pull_request) Successful in 1m12s
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 2m4s
standards workspaces build + test / aac-rs (pull_request) Successful in 1m35s
standards workspaces build + test / joule-code-rs (pull_request) Successful in 49s
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 36s
standards workspaces build + test / map-rs (pull_request) Successful in 27s
standards workspaces build + test / mesh-rs (pull_request) Successful in 29s
standards workspaces build + test / openpay (pull_request) Successful in 1m20s
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Successful in 2m27s
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
no-vanity-metrics / WAI public text names no comparison (pull_request) Successful in 4s
no-vanity-metrics / WAI public text names no company or product (pull_request) Successful in 6s
standards workspaces build + test / arl-rs (pull_request) Successful in 1m14s
standards workspaces build + test / eoc-rs (pull_request) Successful in 2m17s
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m49s
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 1m20s
standards workspaces build + test / joulehook-rs (pull_request) Successful in 1m20s
standards workspaces build + test / proof-rs (pull_request) Successful in 1m30s
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m32s
standards workspaces build + test / sense-rs (pull_request) Successful in 1m10s
workflow hygiene / every workflow supersedes its own queue (pull_request) Successful in 5s
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 3m46s
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 4m46s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 9m31s
proof-cascade now seals every cache hit as Estimator (0edb0d18): the zero
of a hit was never metered, and carrying the closing solver's grade let a
hit present a measured 0 µJ graded above the proof it reused. Say so in
the normative text.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: name the hook type in the panicking-hook test
clippy's type_complexity flagged the tuple of boxed hooks the test added for the engine guard; a local alias names it. sandbox-proof is clippy-clean again. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: name the check-sat answer CheckSat, so clippy stays clean
The answer enum added with the per-goal end marker was `Sat`, with a variant `Sat`, which clippy's enum_variant_names flags. The README says proof-rs is clippy-clean on Linux and has two macOS lints, both in proof-cascade's IOReport FFI; renaming the enum keeps that true. Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: prove_local's public doc linked a private item
rustdoc warned that the Accelerators paragraph linked `unrecorded_accelerator_use`, a private function; it is named in code font instead. (The four other rustdoc warnings in this crate predate it.) Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: Z3Server's public doc linked the private shape guard
rustdoc warned that the Isolation paragraph linked `admit`, a private item; it is named in code font instead. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: say what metering a resident decision adds to its latency
The Cost paragraph counted only the settle walks, "tens of µs each" on a quiet host and up to the settle bound under load. It left out the I/O Registry read of the GPU clients at each end, before the start walk and after the stop walk, outside the settle bound: about a millisecond, and seen at tens of milliseconds under heavy load. Measured overhead per goal on the loaded development host at the production bound is a few ms typically, several at p90, tens at worst. The paragraph now describes that shape and points at the test that logs the figures per host, rather than pinning numbers that move with load. Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: a panicking hook never leaves the local engine behind
run_engine calls on_suspended before it sends SIGCONT. If that hook panicked, the unwind left the engine suspended forever, orphaned once the process exited; a panic in on_exited left an unreaped zombie. (Production passes hooks that do nothing; the tests' oracle reads run there.) A drop guard now holds the engine from its spawn until it is reaped: on any unwind it SIGKILLs it (which ends a stopped process too) and reaps it. The test panics from each hook in turn and checks the pid is already reaped, reaping anything left before it asserts so a failure leaves nothing; before the fix the suspended engine was still there. Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: a GPU counter that did not advance is no reading of the GPU
Span::stop's held-counter rule turns a CPU counter that did not advance into the estimator, but checks the CPU class alone, and the accelerator proof passed the meter's Gpu record through verbatim. So on an NVML-live host, a workload shorter than one counter publish (or a counter that held) sealed Gpu HwShunt measured 0: a measured zero for a GPU that ran. accelerator_records now treats a zero Gpu record as no reading: the nvidia-smi power samples stand in (ModelBased), and with no sample the proof is refused, as with no GPU counter at all. Fixed in sandbox-proof; sandbox-meter's probe is left as it is. The Linux hardware test now expects HwShunt only where NVML's record over the run is non-zero. Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: refuse a local proof that would fold accelerator use into Cpu
With positive evidence in the engine tree's reading that the engine used
the GPU (Gpu { ns }: its clients' recorded time), prove_local still sealed
the machine-wide meter's records, which on every Apple Silicon host checked
are the estimator's single Cpu record for the run. SPEC 6.2 forbids exactly
that: accelerator energy is neither folded into the Cpu record nor
omitted. prove_accelerator refuses the analogous run (no GPU figure), and
the doc called the fold acceptable ("the GPU's share included").
prove_local now refuses to seal, saying why, when the reading shows GPU
time, a member holding a GPU client whose time is unknown, or in-process
Neural Engine model memory (the Npu class, same rule), and the records to
be sealed carry no record of that class. A GPU reader that could not read
is no evidence; a machine meter with its own Gpu/Npu records (IOReport
live) carries each class and is unaffected. Tested on synthetic reading
shapes. A real run-to-completion Metal child was tried: its GPU client had
lost its time by the stop walk in every run (only the Exited gap), so the
doc now says the evidence is what the reading holds and is usually gone
for an exited engine.
The same doc said the span "holds the whole run of every process in the
tree"; the suspended child already carries a little energy at the start
walk (its creation), taken as the baseline. It now says the span holds the
tree from the engine's first instruction to its exit.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: seal a resident z3 reading only on its operator's declaration
A whole reading of the resident z3's tree was sealed HwShunt on a declaration the code made itself: "this crate spawned the z3". That covers nothing about what answers to `z3` on PATH. A wrapper that forwards each goal to a z3 in a container, a VM or on another host reads whole here (only the forwarding client is in the tree) while the decision is charged elsewhere; the review's wrapper was sealed HwShunt about 50x short of the work. As jcp-gateway does for an upstream and sandbox-proof for a local engine, the reading is now sealed only on the operator's declaration that the z3 it runs decides each goal in its own process tree: Z3Server::declared_self_contained(bool), resident_z3_ladder(bool), and in proof-cli PROOF_Z3_SELF_CONTAINED=1. Undeclared, the default, a reading keeps the model figure with Modelled::NotDeclaredSelfContained beside any gaps. The session now starts z3 from the first z3 on PATH resolved to an absolute path (symlinks followed), and Z3EnergyAccount::z3 records that binary: the declaration is about it. The z3 tree tests declare their Homebrew z3 explicitly; a new test shows an undeclared server seals ModelBased for a whole reading (it was HwShunt before), and a unit test checks the recorded path against the shell's own lookup. README and proof-cli docs say when T1 is read off hardware. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-cascade: a cache hit never seals its zero as a hardware reading
A hit returned the cached proof's stored grade, which is the closing solver's own, beside a total of 0. So a goal whose first proof sealed ModelBased (T0's modelled waste in its total) came back from the cache sealed HwShunt 0 uJ: a measured zero for a span nothing metered, graded above the proof it serves. A hit's zero is the lookup's nominal cost, neither read nor modelled, so it is Estimator. The stored CachedProof.provenance keeps its meaning, the grade of the stored figure (the closing solver's own) and nothing else, so cache files written before load and round-trip unchanged; the test loads one such line, with HwShunt stored, and checks the hit is Estimator. Published proof vectors regenerate byte-identical (no hit in the pack). Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: a goal's output is never read as another goal's verdict
The resident z3 session delimited each goal's output with a fixed marker, `(echo "@@END@@")`. A goal could print that marker itself: the read stopped early, the goal's real answer stayed in the pipe, and every later goal was read off the answer of the goal before it. A FALSE claim (`y > 0` for all `y`) came back Proved and was sealed. The same root, trusting goal-controlled output, opened more: - one-shot `Z3Smt` read the FIRST verdict-shaped line, so a goal that began `(echo "unsat")` proved a false claim; - the resident path never checked for `(error`: z3 answers `(check-sat)` over the part of a script that parsed, so an erroring goal came back REFUTED with a model, while one-shot returned Unproved; - z3 keeps `set-option` across `(reset)`, so one goal's options (`:rlimit`, `:timeout`, an output channel) reached every later goal; - a goal leaving a string literal or quoted symbol open swallowed the appended `(check-sat)` and marker, and a goal redirecting `:regular-output-channel` sent them to a file: either wedged the session forever with its lock held; `(exit)` killed it for every later goal. Now every script, resident or one-shot, is framed the same way: the statement, this crate's own `(check-sat)`, then an end marker drawn fresh per script (128 bits keyed from the OS's randomness via RandomState). The answer is the line just before the marker, and only when no line of the output is an error. The counter-model is read between two fresh markers after a `sat` this same run produced. A shape guard (a small SMT-LIB lexer) admits only whole parenthesized commands, refusing an open string or quoted symbol, the marker prefix, `exit`, `include` and output-channel options. The resident session is retired (killed, reaped, replaced with a new meter) after a goal that sets an option, any goal not answered with a clean verdict, and whenever it breaks. Tests drive each case on a real z3 and failed before the fix: the injected marker sequence (the false claim was Proved), the echoed verdict (one-shot proved a false claim), the erroring goal (resident Refuted), the persisted option, the killed session, and the wedging goals (the session hung). Published proof vectors regenerate byte-identical. Co-Authored-By: Claude Opus 5.5 <[email protected]>
ci: run the new platform-gated meter tests where their platform is
The resident z3 tree tests (proof-solvers tests/z3_tree.rs) and the local
engine tree tests (sandbox-proof) are gated to Apple Silicon macOS, and the
matrix legs for proof-rs and sandbox-rs run on Linux, so they would run
nowhere. The macOS energy job now runs both and greps the line each metered
run prints ('z3 tree meter:', 'local engine tree:'): a missing z3 or a
per-process counter that is not live prints another line and fails the
step. Likewise the accelerator proof's RAPL path only runs on real
counters: the jetson-hub hardware job now runs sandbox-proof's accelerator
tests and fails unless the RAPL bracket line was printed, and triggers on
sandbox-proof changes.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: meter the accelerator proof over the workload's actual run
prove_accelerator sealed a GPU record of nvidia-smi power.draw samples x a fixed sample_secs window (ModelBased) and a constant 1 mJ CPU placeholder (Estimator), and never checked the workload's exit. The run is now spanned by PowerMeter::detect() from just before the workload is spawned to once it has exited: RAPL package counters for Cpu and NVML's total-energy counter for Gpu, each HwShunt and each only where its liveness probe passed. Both are machine-wide, and the docs and the log line say so. A class with no live counter gets the honest fallback: Cpu the meter's wall-clock estimator, Gpu nvidia-smi power samples x the run's actual time (ModelBased); with no GPU figure at all, or a failed workload, the proof is refused instead of sealing a zero. sample_secs is gone from the signature: the span is the run, however long it is; the CLI still passes the duration to the workload as its argument. Run on jetson-hub (i9-13900H, RTX 4050; NVML implausible there, so the GPU falls back to samples): the span's RAPL figure equals an independent sysfs read of the package zones around the call (ratio 1.000), and prove-gpu on a real CUDA matmul load sealed Cpu 308 J HwShunt + Gpu 160 J ModelBased over the 6.5 s run, verified. Co-Authored-By: Claude Opus 5.5 <[email protected]>
sandbox-proof: meter the local engine on its own process tree, seal it only whole
prove_local ran the operator's engine under PowerMeter::detect() alone: machine-wide, and on macOS 27 the wall x TDP estimator. On macOS the engine is now spawned suspended (posix_spawn START_SUSPENDED), a TreeMeter rooted at it reads the start walk before it runs its first instruction, it is resumed with SIGCONT, and its exit is waited for without reaping (waitid WNOWAIT) so its exited record is read before the reap. The machine-wide span still covers the whole run. Which records the JCR-1 cell carries is decided by SPEC section 6: one record per class used, no coverage field, HwShunt claiming the class's hardware reading, accelerator energy neither omitted nor folded into Cpu. So the tree reading is sealed, as the run's only record (Cpu, HwShunt), only when it has no gap of any kind and the operator declared the engine self-contained (new LocalInferenceInputs::engine_self_contained; CLI SANDBOX_LOCAL_SELF_CONTAINED=1); otherwise the machine-wide records stand, verbatim, as before. A Cpu HwShunt record of a partial reading would claim the class's whole energy, and a tree Cpu record beside the estimator for "the rest" cannot be built: the estimator is one whole-run Cpu figure. On this kernel a run-to-completion engine is never read whole: its root exits in the span and an exiting thread's last time on a core is never folded into its record (TreeGap::Exited). So the cell keeps the machine records, and the tree's reading and why it was not sealed are printed beside the proof. Measured: awk burning a fixed loop read exactly the oracle's advance (proc_pid_rusage raw, suspended to exited) with Exited as its only gap; sh reaping its awk worker read with ReapedDescendant named. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-cli, proof README: say which rung is read off hardware
The CLI's module docs and the README said both real rungs' energy is modeled. The resident z3's decisions are now read off its own process tree where that reading is whole, and a goal's figure is graded by the weakest attempt it sums, so an SMT goal that T0 tries first is still ModelBased. The text says so; the CLI's output and tests are unchanged. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-cascade: a goal's headline cost carries the weakest grade it sums
CascadeResult.provenance, sealed as the receipt's energy_provenance, was the closing solver's grade, while total_uj sums the closing attempt and every cheaper one that failed before it. That was harmless while every real rung was ModelBased; with the resident z3 now reading HwShunt above the modelled T0 decider, an SMT goal's receipt would have sealed a total holding a model as a hardware reading. The run's provenance is now the weakest of the attempts summed (Estimator < ModelBased < HwShunt), which is the closing solver's own whenever the rungs share one grade, so the published reference vectors regenerate byte-identical (checked with gen-vectors). A cached proof keeps the closing solver's grade, because its figure is that solver's alone. Tested with canned graded rungs, and end to end through the cascade with a real resident z3: T0 ModelBased, T1 HwShunt, goal sealed ModelBased. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof-solvers: read each resident z3 decision off z3's own process tree
Z3Server::attempt sealed wall time x 15 W (ModelBased) on every OS, though the decision runs in a resident z3 child whose CPU energy this host's kernel counts per process. Each decide() is now spanned with sandbox-meter's TreeMeter on the resident z3's pid (built once with the session, so the counter's liveness probe never lands on a goal), and the attempt is sealed HwShunt at the reading, rounded up to the uJ, only when the reading has no gap at all and the decision ran entirely in the tree. The code spawned z3 itself and z3 is a single-process solver that hands no work elsewhere: that is the in-code equivalent of jcp-gateway's operator declaration, and the docs say so and where it ends. Every other case keeps today's model figure and says why, in-process (Z3Server::last_account): a gapped reading (Energy has no coverage field, so a partial reading sealed HwShunt would claim the whole decision), no reading, no tree meter (Linux, or the counter not live), a goal that never reached z3, and a refutation, whose counter-model a one-shot z3 fetches outside the resident tree after the span has stopped. The model figure now times the solver's work alone, never the meter's settling. Measured on an M5 Max at load ~150: every reading equal to an independent proc_pid_rusage oracle on the z3 pid to the nanojoule; under the default 50 ms bound 30 of 30 decisions read whole, metering overhead per goal median 2.5 ms, p90 4.7 ms, max 34 ms. The bound is configurable (with_settle_bound). The dependents' lockfiles gain sandbox-meter. Co-Authored-By: Claude Opus 5.5 <[email protected]>