proof: z3 could be made to prove a false claim; meter solver subprocesses where they ran #213

Merged

dcharlot merged 18 commits from feat/meter-solver-subprocesses into main 2026-10-10 22:23:35 -04:00

Conversation 0 Commits 18 Files changed 16 +2900 -191

dcharlot commented 2026-10-10 18:22:38 -04:00

Owner

Copy link

Soundness first: z3 could be made to prove a false claim

Reviewing this branch turned up a hole that predates it.

Resident session. proof-solvers' resident z3 session used a fixed end marker to find each answer. A goal containing that marker, (echo "@@END@@"), shifted every later verdict by one, so a FALSE claim (x > 0 for all x) came back Proved and was sealed.

Four more holes with the same root:

• The one-shot path proved a false claim that began with (echo "unsat").
• An erroring goal came back Refuted with a model.
• A goal's options carried over to every later goal: z3 keeps set-option across (reset).
• An unclosed string or an output-channel option hung the session forever with its lock held, and (exit) disabled it for every later goal.

Fixed in 82b27962, its own commit:

• Every script now ends with the crate's own (check-sat) and a marker drawn fresh per script, and the answer is the line just before that marker.
• Any (error makes the goal undecided.
• A small SMT-LIB lexer admits only whole commands. It refuses unclosed strings or quoted symbols, the marker prefix, exit, include and output-channel options.
• The resident session is retired after any goal that sets an option, any goal not answered with a clean verdict, and any break.
• Six real-z3 tests failed before the fix: the false claim came back Proved, and the wedge test hung. The reviewer's reproduction now gives the false claim Refuted.

Metering

• proof-solvers Z3Server. It used to model each decision as wall time × 15 W. Each resident decision is now read off z3's own process tree with sandbox-meter's TreeMeter.
  • When a reading is sealed: only when the reading has no gap and the operator declared z3 self-contained. The declaration is Z3Server::declared_self_contained, or PROOF_Z3_SELF_CONTAINED=1 for proof-cli. Such a reading is sealed HwShunt, rounded up to whole µJ.
  • Otherwise: the model figure stands, with the reason recorded. proof-schema's Energy has no coverage field, so a gapped reading is never sealed.
  • Why a declaration: the z3 on PATH could be a wrapper forwarding to a container or a remote host. Such a wrapper read about 50× short and was sealed as a reading. The resolved absolute path of z3 is recorded with each account.
  • Refutations: a refutation's one-shot z3 runs outside the resident tree, so the attempt is modelled.
  • API change: resident_z3_ladder(self_contained: bool).
• proof-cascade.
  • A goal's headline cost carries the weakest grade it sums.
  • A cache hit seals Estimator, never a measured zero graded above the proof it reuses. Older cache files still load. SPEC §7 now says this.
• sandbox-proof prove_local.
  • Lifecycle: the engine is spawned suspended, read at rest, resumed, and held as a zombie for its stop reading. A drop guard kills and reaps it on any unwind.
  • Never a reading in practice: its exit always loses the last slice on a core, so the proof cell keeps the machine records and prints the tree figure beside them.
  • Refusals: it refuses to seal when the reading shows GPU or in-process Neural Engine use the records cannot hold (§6.2).
• sandbox-proof prove_accelerator (Linux). The workload's actual run is spanned by the machine meter: RAPL and NVML, each only where live, labelled machine-wide. A zero GPU delta is no reading: power samples stand in, and with no samples the proof is refused. sample_secs is removed.
• CI. The macOS energy job runs the z3 and local-engine tests, each gated on a line it prints. The jetson-hub hardware job runs the accelerator test.

Evidence

• z3 decisions: each equals an independent proc_pid_rusage oracle on the z3 pid, to the nanojoule. At the production settle bound, every decision read whole.
• jetson-hub accelerator proof: a real CUDA load sealed Cpu 308 J (RAPL, HwShunt) and Gpu 160 J (ModelBased, because NVML is implausible on that GPU), and the cell verified. The RAPL span equals the sysfs oracle (ratio 1.000).
• Review: an independent review found 7 defects plus the soundness hole, all fixed. Each fix has a test that fails before it, except the documentation-only fixes and the unit tests of the new declaration API.
• Suites:
  • proof-rs workspace: 160 passed. proof-conformance passes, and gen-vectors output is byte-identical to proof/conformance/v1.
  • sandbox-proof: 27 passed; sandbox-conformance passes.
  • The joulecontract-rs and joule-code-rs dependents build.
  • Linux cross-checks are clean.

Not covered

• No read timeout. A legitimately long z3 goal can still block the resident session. Every hang a goal could cause on purpose is refused at admission.
• sandbox-proof's 4 older rustdoc warnings are untouched.

🤖 Generated with Claude Code

## Soundness first: z3 could be made to prove a false claim Reviewing this branch turned up a hole that predates it. **Resident session.** proof-solvers' resident z3 session used a fixed end marker to find each answer. A goal containing that marker, `(echo "@@END@@")`, shifted every later verdict by one, so a FALSE claim (`x > 0` for all `x`) came back `Proved` and was sealed. **Four more holes with the same root:** - The one-shot path proved a false claim that began with `(echo "unsat")`. - An erroring goal came back `Refuted` with a model. - A goal's options carried over to every later goal: z3 keeps `set-option` across `(reset)`. - An unclosed string or an output-channel option hung the session forever with its lock held, and `(exit)` disabled it for every later goal. **Fixed in `82b27962`, its own commit:** - Every script now ends with the crate's own `(check-sat)` and a marker drawn fresh per script, and the answer is the line just before that marker. - Any `(error` makes the goal undecided. - A small SMT-LIB lexer admits only whole commands. It refuses unclosed strings or quoted symbols, the marker prefix, `exit`, `include` and output-channel options. - The resident session is retired after any goal that sets an option, any goal not answered with a clean verdict, and any break. - Six real-z3 tests failed before the fix: the false claim came back `Proved`, and the wedge test hung. The reviewer's reproduction now gives the false claim `Refuted`. ## Metering - **proof-solvers `Z3Server`.** It used to model each decision as wall time × 15 W. Each resident decision is now read off z3's own process tree with sandbox-meter's `TreeMeter`. - **When a reading is sealed:** only when the reading has no gap **and** the operator declared z3 self-contained. The declaration is `Z3Server::declared_self_contained`, or `PROOF_Z3_SELF_CONTAINED=1` for proof-cli. Such a reading is sealed `HwShunt`, rounded up to whole µJ. - **Otherwise:** the model figure stands, with the reason recorded. `proof-schema`'s `Energy` has no coverage field, so a gapped reading is never sealed. - **Why a declaration:** the `z3` on `PATH` could be a wrapper forwarding to a container or a remote host. Such a wrapper read about 50× short and was sealed as a reading. The resolved absolute path of z3 is recorded with each account. - **Refutations:** a refutation's one-shot z3 runs outside the resident tree, so the attempt is modelled. - **API change:** `resident_z3_ladder(self_contained: bool)`. - **proof-cascade.** - A goal's headline cost carries the weakest grade it sums. - A cache hit seals `Estimator`, never a measured zero graded above the proof it reuses. Older cache files still load. SPEC §7 now says this. - **sandbox-proof `prove_local`.** - **Lifecycle:** the engine is spawned suspended, read at rest, resumed, and held as a zombie for its stop reading. A drop guard kills and reaps it on any unwind. - **Never a reading in practice:** its exit always loses the last slice on a core, so the proof cell keeps the machine records and prints the tree figure beside them. - **Refusals:** it refuses to seal when the reading shows GPU or in-process Neural Engine use the records cannot hold (§6.2). - **sandbox-proof `prove_accelerator` (Linux).** The workload's actual run is spanned by the machine meter: RAPL and NVML, each only where live, labelled machine-wide. A zero GPU delta is no reading: power samples stand in, and with no samples the proof is refused. `sample_secs` is removed. - **CI.** The macOS energy job runs the z3 and local-engine tests, each gated on a line it prints. The jetson-hub hardware job runs the accelerator test. ## Evidence - **z3 decisions:** each equals an independent `proc_pid_rusage` oracle on the z3 pid, to the nanojoule. At the production settle bound, every decision read whole. - **jetson-hub accelerator proof:** a real CUDA load sealed `Cpu` 308 J (RAPL, `HwShunt`) and `Gpu` 160 J (`ModelBased`, because NVML is implausible on that GPU), and the cell verified. The RAPL span equals the sysfs oracle (ratio 1.000). - **Review:** an independent review found 7 defects plus the soundness hole, all fixed. Each fix has a test that fails before it, except the documentation-only fixes and the unit tests of the new declaration API. - **Suites:** - proof-rs workspace: 160 passed. proof-conformance passes, and gen-vectors output is byte-identical to `proof/conformance/v1`. - sandbox-proof: 27 passed; sandbox-conformance passes. - The joulecontract-rs and joule-code-rs dependents build. - Linux cross-checks are clean. ## Not covered - **No read timeout.** A legitimately long z3 goal can still block the resident session. Every hang a goal could cause on purpose is refused at admission. - **sandbox-proof's 4 older rustdoc warnings** are untouched. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 18 commits 2026-10-10 18:22:38 -04:00

proof-solvers: read each resident z3 decision off z3's own process tree ... effb4e3c8e

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

proof-cascade: a goal's headline cost carries the weakest grade it sums ... f24ae5f7a9

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-cli, proof README: say which rung is read off hardware ... 8cd9efaba2

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

sandbox-proof: meter the local engine on its own process tree, seal it only whole ... 79efad0b0a

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

sandbox-proof: meter the accelerator proof over the workload's actual run ... e275e69a20

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

ci: run the new platform-gated meter tests where their platform is ... 4e8350def7

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

proof-solvers: a goal's output is never read as another goal's verdict ... 82b2796233

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

proof-cascade: a cache hit never seals its zero as a hardware reading ... 0edb0d18cd

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: seal a resident z3 reading only on its operator's declaration ... d7e3b81c03

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

sandbox-proof: refuse a local proof that would fold accelerator use into Cpu ... 8b327b956d

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

sandbox-proof: a GPU counter that did not advance is no reading of the GPU ... 296532b132

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: a panicking hook never leaves the local engine behind ... cc47856dda

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

proof-solvers: say what metering a resident decision adds to its latency ... 2cb1ee0067

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

proof-solvers: Z3Server's public doc linked the private shape guard ... 866c8aa23d

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

sandbox-proof: prove_local's public doc linked a private item ... 5bcb48498b

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: name the check-sat answer CheckSat, so clippy stays clean ... 97070fa194

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: name the hook type in the panicking-hook test ... 88052772bb

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 SPEC §7: a cache hit's zero is sealed Estimator ... 10360d246e

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

dcharlot merged commit 2d9d2a2753 into main 2026-10-10 22:23:35 -04:00

dcharlot referenced this pull request from a commit 2026-10-10 22:23:36 -04:00

Merge pull request 'proof: z3 could be made to prove a false claim; meter solver subprocesses where they ran' (#213) from feat/meter-solver-subprocesses into main

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!213

No description provided.