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]>
27 lines
1,015 B
TOML
27 lines
1,015 B
TOML
[package]
|
|
name = "proof-solvers"
|
|
version.workspace = true
|
|
edition.workspace = true
|
|
license.workspace = true
|
|
repository.workspace = true
|
|
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
|
|
# and ladder, not in either alone. proof-cascade does not depend on this crate,
|
|
# 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
|