diff --git a/.github/workflows/energy-hardware.yml b/.github/workflows/energy-hardware.yml index 801826740..f16020c42 100644 --- 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 diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 9e9f7d9fe..b5272685d 100644 --- 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" diff --git a/joule-code/joule-code-rs/Cargo.lock b/joule-code/joule-code-rs/Cargo.lock index 2a79280ef..9b6eea4e3 100644 --- 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]] diff --git a/joulecontract/joulecontract-rs/Cargo.lock b/joulecontract/joulecontract-rs/Cargo.lock index f826b1102..cc4ec3a48 100644 --- 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" diff --git a/proof/README.md b/proof/README.md index 5d3a3e945..ebb6e255a 100644 --- 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__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__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 diff --git a/proof/SPEC.md b/proof/SPEC.md index a48379529..654a26638 100644 --- 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: diff --git a/proof/proof-rs/Cargo.lock b/proof/proof-rs/Cargo.lock index 8fcdfca75..65921975f 100644 --- 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" diff --git a/proof/proof-rs/crates/proof-cascade/src/lib.rs b/proof/proof-rs/crates/proof-cascade/src/lib.rs index be72394ab..64657dbc0 100644 --- 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, pub artifact: Option, - /// 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>, @@ -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 = 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> = 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![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> { + 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> { + 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()); + } } diff --git a/proof/proof-rs/crates/proof-cli/src/main.rs b/proof/proof-rs/crates/proof-cli/src/main.rs index 65259f3c1..94d88654e 100644 --- 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 { diff --git a/proof/proof-rs/crates/proof-solvers/Cargo.toml b/proof/proof-rs/crates/proof-solvers/Cargo.toml index 6b02fa855..539039bca 100644 --- 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 diff --git a/proof/proof-rs/crates/proof-solvers/src/lib.rs b/proof/proof-rs/crates/proof-solvers/src/lib.rs index 7cbd8568f..c48935ebc 100644 --- a/proof/proof-rs/crates/proof-solvers/src/lib.rs +++ b/proof/proof-rs/crates/proof-solvers/src/lib.rs @@ -1,12 +1,17 @@ //! Solvers for the proof tier ladder (SPEC §4). //! //! The two bottom rungs are **real** and report energy with `ModelBased` -//! provenance (measured wall time × a power model): +//! provenance (measured wall time × a power model), but for one case: //! //! - [`Propositional`] (T0) → parses a boolean goal and decides validity by //! truth-table, in process. //! - [`Z3Smt`] (T1) → shells out to `z3` on an SMT-LIB2 goal (assert the -//! negation; `unsat` ⇒ valid). [`Z3Server`] keeps `z3` resident across goals. +//! negation; `unsat` ⇒ valid). [`Z3Server`] keeps `z3` resident across goals, +//! and where this host's kernel counts each process's CPU energy live +//! (macOS), reads each decision off the resident `z3`'s own process tree: +//! `HwShunt` when the reading saw nothing missing and the operator has +//! declared that `z3` decides in its own tree, the model otherwise (see +//! [`Z3Server`] for exactly when). //! - [`LeanVerifier`] → runs Lean and reports what the kernel accepted. //! //! The model rungs are stand-ins that gate on `GoalKind` until real backends are @@ -28,11 +33,13 @@ pub mod prop; use std::io::{BufRead, BufReader, Write}; +use std::path::{Path, PathBuf}; use std::process::{Child, ChildStdin, ChildStdout, Command, Stdio}; use std::sync::Mutex; -use std::time::Instant; +use std::time::{Duration, Instant}; use proof_schema::{Attempt, ContentId, Energy, GoalKind, ProofGoal, Solver, Tier, Verdict}; +use sandbox_meter::{TreeError, TreeGap, TreeMeter, TreeReading}; /// Convert elapsed nanoseconds to microjoules under a documented single-core /// power model (~15 W active). The reading is `ModelBased`: a hardware interface @@ -168,10 +175,111 @@ impl Solver for Propositional { } } -/// Run `z3` on an SMT-LIB2 script (piped over stdin) and return the first -/// `check-sat` verdict. `None` if `z3` is absent or errored — the router reads -/// that as "escalate", never as proof. -fn run_z3(script: &str) -> Option { +/// The prefix of the end marker that closes z3's output for each script +/// ([`end_marker`]). A goal statement containing it is refused, never run. +const END_MARKER_PREFIX: &str = "@@END@@"; + +/// A fresh end marker for one script: [`END_MARKER_PREFIX`] and 128 bits no +/// goal can predict, in hex. The bits are two keyed hashes of a counter, under +/// keys std's `RandomState` draws from the operating system's randomness. +/// +/// Every script's output is read up to its own marker. A fixed marker let a +/// goal print it (`(echo "@@END@@")`): the read stopped early, the goal's real +/// answer stayed in the pipe, and every later goal on the resident session +/// was read off the answer of the goal before it — a FALSE claim came back +/// proved. A goal cannot print a marker drawn after it was written. +fn end_marker() -> String { + use std::collections::hash_map::RandomState; + use std::hash::{BuildHasher, Hasher}; + use std::sync::atomic::{AtomicU64, Ordering}; + static DRAWN: AtomicU64 = AtomicU64::new(0); + let n = DRAWN.fetch_add(1, Ordering::Relaxed); + let keys = RandomState::new(); + let word = |lane: u8| { + let mut h = keys.build_hasher(); + h.write_u64(n); + h.write_u8(lane); + h.finish() + }; + format!("{END_MARKER_PREFIX}{:016x}{:016x}", word(0), word(1)) +} + +/// The text written to `z3` for a goal: the statement, then this crate's own +/// `(check-sat)`, then the end marker. The answer is the line that +/// `(check-sat)` printed, which is the line just before the marker +/// ([`Reply`]): every command of the statement has run, and printed whatever +/// it prints, before it. +fn framed(statement: &str, marker: &str) -> String { + format!("{statement}\n(check-sat)\n(echo \"{marker}\")\n") +} + +/// `z3`'s answer to this crate's `(check-sat)`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum CheckSat { + Sat, + Unsat, + Unknown, +} + +/// What `z3` said of one script, read up to its end marker. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Answer { + /// A decision: the line before the marker is a verdict, and nothing in + /// the script's output was an error. + Verdict(CheckSat), + /// `z3` answered, but not with a decision: an error anywhere in the + /// output, or no verdict where this crate's `(check-sat)` answers. + Undecided, +} + +/// The resident session cannot be trusted any more: the script could not be +/// written, or `z3`'s output ended or failed before the marker. The session +/// is retired, never reused. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +struct Broken; + +/// `z3`'s output for one script, line by line up to (not including) its end +/// marker. +#[derive(Debug, Default)] +struct Reply { + error: bool, + last: Option, +} + +impl Reply { + fn line(&mut self, line: &str) { + // z3 reports parse and command errors as `(error "...")` on STDOUT, + // then carries on and answers `(check-sat)` anyway — against the part + // of the script that parsed, or an empty stack if nothing did. Read as + // a verdict, "I could not understand the goal" becomes a decision + // about some other formula; and a refutation is terminal in this + // cascade, the strongest wrong answer the ladder can give. So any + // error at all makes the whole script undecided. + if line.contains("(error") { + self.error = true; + } + self.last = Some(line.trim().to_string()); + } + + /// The answer: the verdict on the line just before the marker, which is + /// this crate's `(check-sat)`'s, never a verdict-shaped line the goal + /// printed itself (`(echo "unsat")`) — the first such line was once read + /// as the answer, and proved a false claim. + fn answer(&self) -> Answer { + if self.error { + return Answer::Undecided; + } + match self.last.as_deref() { + Some("sat") => Answer::Verdict(CheckSat::Sat), + Some("unsat") => Answer::Verdict(CheckSat::Unsat), + Some("unknown") => Answer::Verdict(CheckSat::Unknown), + _ => Answer::Undecided, + } + } +} + +/// `input` on a one-shot `z3`: its stdout, or `None` if `z3` could not be run. +fn run_one_shot(input: &str) -> Option { let mut child = Command::new("z3") .args(["-in", "-smt2"]) .stdin(Stdio::piped()) @@ -179,32 +287,38 @@ fn run_z3(script: &str) -> Option { .stderr(Stdio::null()) .spawn() .ok()?; - let full = if script.contains("check-sat") { - script.to_string() - } else { - format!("{script}\n(check-sat)\n") - }; { let mut stdin = child.stdin.take()?; - stdin.write_all(full.as_bytes()).ok()?; + stdin.write_all(input.as_bytes()).ok()?; } let out = child.wait_with_output().ok()?; - let stdout = String::from_utf8_lossy(&out.stdout); - // z3 reports parse and command errors as `(error "...")` on STDOUT, then - // carries on and answers `(check-sat)` anyway — against an assertion stack - // that is empty because nothing parsed. That answer is `sat`, and reading it - // as a verdict turns "I could not understand the goal" into "the goal is - // FALSE". Since a refutation is terminal in this cascade, that is the - // strongest wrong answer the ladder can give, so any error at all makes the - // whole run undecided. - if stdout.contains("(error") { - return None; + Some(String::from_utf8_lossy(&out.stdout).into_owned()) +} + +/// Read `lines` up to `marker` into a [`Reply`]: `None` if the marker never +/// came (`z3` ended first). +fn reply_until<'a>(lines: &mut impl Iterator, marker: &str) -> Option { + let mut reply = Reply::default(); + for line in lines { + if line.trim() == marker { + return Some(reply); + } + reply.line(line); + } + None +} + +/// Run a one-shot `z3` on an SMT-LIB2 script (piped over stdin) and return +/// the answer to this crate's `(check-sat)`. `None` if `z3` is absent, the +/// script errored, or no verdict came — the router reads that as "escalate", +/// never as proof. +fn run_z3(script: &str) -> Option { + let marker = end_marker(); + let out = run_one_shot(&framed(script, &marker))?; + match reply_until(&mut out.lines(), &marker)?.answer() { + Answer::Verdict(v) => Some(v), + Answer::Undecided => None, } - stdout - .lines() - .map(str::trim) - .find(|l| matches!(*l, "sat" | "unsat" | "unknown")) - .map(str::to_string) } /// Fetch the counter-model for a refuted goal: re-run `z3` with `(get-model)` @@ -217,7 +331,7 @@ fn run_z3(script: &str) -> Option { /// often it means nothing was asserted — and since a refutation halts the /// cascade as a final decision, an unsubstantiated one is worse than no answer. fn refutation_or_undecided(script: &str) -> Verdict { - let cm = z3_counter_model(script); + let cm = z3_counter_model(script).unwrap_or_default(); // A model with no assignments in it: "(", ")", whitespace, and nothing else. let substantive = cm.chars().any(|c| !matches!(c, '(' | ')' | ' ' | '\n' | '\t' | '\r')); if substantive { @@ -227,33 +341,29 @@ fn refutation_or_undecided(script: &str) -> Verdict { } } -fn z3_counter_model(script: &str) -> String { - let full = if script.contains("check-sat") { - format!("{script}\n(get-model)\n") - } else { - format!("{script}\n(check-sat)\n(get-model)\n") - }; - let Ok(mut child) = Command::new("z3") - .args(["-in", "-smt2"]) - .stdin(Stdio::piped()) - .stdout(Stdio::piped()) - .stderr(Stdio::null()) - .spawn() - else { - return String::new(); - }; - if let Some(mut stdin) = child.stdin.take() { - let _ = stdin.write_all(full.as_bytes()); +/// The model `z3` gives for `script`, framed like every other script: this +/// run must itself answer `sat` to this crate's `(check-sat)` with no error, +/// and the model is the output of the `(get-model)` after it, between two +/// fresh markers — never text the goal printed. `None` otherwise. +fn z3_counter_model(script: &str) -> Option { + let (decided, modelled) = (end_marker(), end_marker()); + let input = format!("{}(get-model)\n(echo \"{modelled}\")\n", framed(script, &decided)); + let out = run_one_shot(&input)?; + let mut lines = out.lines(); + if reply_until(&mut lines, &decided)?.answer() != Answer::Verdict(CheckSat::Sat) { + return None; } - let Ok(out) = child.wait_with_output() else { - return String::new(); - }; - let text = String::from_utf8_lossy(&out.stdout); - // Keep the model block (everything from the first "sat" line onward), - // trimmed; drop the leading bare "sat". - let mut lines = text.lines().map(str::trim_end).skip_while(|l| l.trim() != "sat"); - lines.next(); // the "sat" line itself - lines.collect::>().join("\n").trim().to_string() + let mut model = Vec::new(); + for line in lines { + if line.trim() == modelled { + return Some(model.join("\n").trim().to_string()); + } + if line.contains("(error") { + return None; + } + model.push(line.trim_end()); + } + None } /// T1 — a **real** SMT backend that shells out to `z3`. The goal's statement is @@ -271,13 +381,13 @@ impl Solver for Z3Smt { let start = Instant::now(); // The same shape guard the resident session applies. One-shot `z3` was // missing it, so prose reached the solver and came back "refuted". - let outcome = if looks_like_smt(&goal.statement) { + let outcome = if admit(&goal.statement).is_some() { run_z3(&goal.statement) } else { None }; - let verdict = match outcome.as_deref() { - Some("unsat") => Verdict::Proved { + let verdict = match outcome { + Some(CheckSat::Unsat) => Verdict::Proved { artifact: ContentId::of_bytes(goal.statement.as_bytes()), }, // `sat` = the negated claim is satisfiable = the claim is FALSE. A @@ -289,7 +399,7 @@ impl Solver for Z3Smt { // assertion stack means "no constraints", not "here is a // counter-example". A disproof is terminal, so it must carry // evidence or it is not a disproof. - Some("sat") => refutation_or_undecided(&goal.statement), + Some(CheckSat::Sat) => refutation_or_undecided(&goal.statement), _ => Verdict::Unproved, }; let uj = ns_to_uj(start.elapsed().as_nanos()).max(1); @@ -303,16 +413,47 @@ impl Solver for Z3Smt { /// A long-lived `z3 -in` process that decides many goals across one startup — /// the fix for the per-spawn startup tax. Each goal is isolated with `(reset)` -/// and delimited by an `(echo)` marker. +/// and framed like a one-shot script ([`framed`]): this crate's own +/// `(check-sat)`, then a fresh, unpredictable end marker ([`end_marker`]). +/// +/// `(reset)` clears assertions and declarations but NOT options: `z3` keeps +/// every `set-option` across it, so one goal's `:rlimit` or `:timeout` would +/// reach every goal after it. A session is therefore retired — killed and +/// replaced — after a goal that sets an option, and after any goal it did not +/// answer cleanly ([`Z3Server`]). struct Z3Session { child: Child, stdin: ChildStdin, stdout: BufReader, } +/// The `z3` a resident session runs: the first `z3` on `PATH`, as a spawn by +/// name finds it, with symlinks resolved — the file the kernel executes. The +/// session is started from this path, so the path recorded is the binary +/// that ran. +fn resolve_z3() -> Option { + let name = if cfg!(windows) { "z3.exe" } else { "z3" }; + std::env::split_paths(&std::env::var_os("PATH")?) + .map(|dir| dir.join(name)) + .find(|p| is_executable(p)) + .and_then(|p| p.canonicalize().ok()) +} + +fn is_executable(p: &Path) -> bool { + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + p.metadata().is_ok_and(|m| m.is_file() && m.permissions().mode() & 0o111 != 0) + } + #[cfg(not(unix))] + { + p.is_file() + } +} + impl Z3Session { - fn spawn() -> Option { - let mut child = Command::new("z3") + fn spawn(z3: &Path) -> Option { + let mut child = Command::new(z3) .args(["-in", "-smt2"]) .stdin(Stdio::piped()) .stdout(Stdio::piped()) @@ -328,27 +469,32 @@ impl Z3Session { }) } - fn decide(&mut self, script: &str) -> Option { - write!( - self.stdin, - "(reset)\n{script}\n(check-sat)\n(echo \"@@END@@\")\n" - ) - .ok()?; - self.stdin.flush().ok()?; - let mut verdict = None; + /// The resident `z3`'s pid. It names this `z3` for as long as the session + /// lives: the session holds the [`Child`] unreaped until it is dropped. + fn pid(&self) -> u32 { + self.child.id() + } + + /// Decide one script (the caller has [`admit`]ted it): reset, write it + /// framed, and read up to this script's own marker. + fn decide(&mut self, script: &str) -> Result { + let marker = end_marker(); + let input = format!("(reset)\n{}", framed(script, &marker)); + self.stdin.write_all(input.as_bytes()).map_err(|_| Broken)?; + self.stdin.flush().map_err(|_| Broken)?; + let mut reply = Reply::default(); let mut line = String::new(); loop { line.clear(); - if self.stdout.read_line(&mut line).ok()? == 0 { - return None; + match self.stdout.read_line(&mut line) { + Ok(0) | Err(_) => return Err(Broken), + Ok(_) => {} } - match line.trim() { - "@@END@@" => break, - v @ ("sat" | "unsat" | "unknown") => verdict = Some(v.to_string()), - _ => {} + if line.trim() == marker { + return Ok(reply.answer()); } + reply.line(&line); } - verdict } } @@ -359,42 +505,438 @@ impl Drop for Z3Session { } } -/// A balanced, paren-delimited SMT-LIB script is safe to feed the resident -/// session; anything else is refused without touching it, so a malformed goal -/// can never desync the long-lived process. -fn looks_like_smt(s: &str) -> bool { - let t = s.trim(); - if !t.starts_with('(') { - return false; +/// What the shape guard ([`admit`]) found in a script it admitted. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +struct Admitted { + /// The script sets a solver option, which `z3` keeps across `(reset)`: + /// the resident session that runs it is retired after it. + sets_option: bool, +} + +/// The shape guard on every script written to `z3`, resident or one-shot. A +/// script is admitted only when it is a sequence of whole SMT-LIB commands +/// that cannot take over the framing around it; anything else is refused +/// without touching `z3` (undecided), so no goal can desync, wedge or end the +/// long-lived process. Refused: +/// +/// - a statement containing the end marker's prefix ([`END_MARKER_PREFIX`]); +/// - anything but whole parenthesized commands at the top level: an atom +/// there, an unbalanced parenthesis, no command at all, or a string literal +/// or quoted symbol left open — an open one swallows this crate's +/// `(check-sat)` and marker, and the read never ends. Parentheses inside +/// strings, quoted symbols and comments are not counted; +/// - a command that ends `z3` (`exit`) or reads a file (`include`); +/// - a `set-option` of an output channel (`:regular-output-channel`, +/// `:diagnostic-output-channel`), which sends `z3`'s answers — and the +/// marker — elsewhere, and keeps them there across `(reset)`. +/// +/// Command names are read as `z3` reads them: `|exit|` is `exit`. +fn admit(statement: &str) -> Option { + if statement.contains(END_MARKER_PREFIX) { + return None; } - let mut depth: i32 = 0; - for c in t.chars() { - match c { - '(' => depth += 1, - ')' => { + let b = statement.as_bytes(); + let mut i = 0; + let mut depth: u32 = 0; + let mut commands = 0u32; + let mut sets_option = false; + // The next token is a command's name / a `set-option`'s keyword. + let (mut want_head, mut want_option) = (false, false); + while i < b.len() { + let token: &str = match b[i] { + b' ' | b'\t' | b'\n' | b'\r' => { + i += 1; + continue; + } + b';' => { + while i < b.len() && b[i] != b'\n' { + i += 1; + } + continue; + } + b'(' => { + if want_head { + return None; + } + if depth == 0 { + want_head = true; + commands += 1; + } + want_option = false; + depth += 1; + i += 1; + continue; + } + b')' => { + if depth == 0 || want_head { + return None; + } + want_option = false; depth -= 1; - if depth < 0 { - return false; + i += 1; + continue; + } + b'"' => { + // A string literal; `""` inside it is an escaped quote. + i += 1; + loop { + match b.get(i) { + None => return None, + Some(b'"') if b.get(i + 1) == Some(&b'"') => i += 2, + Some(b'"') => break, + Some(_) => i += 1, + } + } + i += 1; + if depth == 0 || want_head { + return None; + } + want_option = false; + continue; + } + b'|' => { + // A quoted symbol: no escapes, ends at the next `|`. + let start = i + 1; + i = start; + while i < b.len() && b[i] != b'|' { + i += 1; + } + if i >= b.len() { + return None; + } + i += 1; + &statement[start..i - 1] + } + _ => { + let start = i; + while i < b.len() && !matches!(b[i], b' ' | b'\t' | b'\n' | b'\r' | b'(' | b')' | b'"' | b'|' | b';') { + i += 1; + } + &statement[start..i] + } + }; + if depth == 0 { + return None; + } + if want_head { + want_head = false; + match token { + "exit" | "include" => return None, + "set-option" => { + sets_option = true; + want_option = true; } + _ => {} + } + } else if want_option { + want_option = false; + if token.contains("output-channel") { + return None; } - _ => {} } } - depth == 0 + (depth == 0 && commands > 0).then_some(Admitted { sets_option }) } /// T1 — `z3` kept **resident** across goals. Same decision semantics as -/// [`Z3Smt`], but the per-goal energy excludes process startup. +/// [`Z3Smt`], but the per-goal energy excludes process startup — and, where +/// this host can read it, is the resident `z3`'s own energy. +/// +/// **Isolation.** Every goal passes the shape guard (`admit`) before it is +/// written, and is read up to an end marker drawn fresh for it, so no goal's +/// output can be read as another's. The session is retired — its `z3` killed +/// and reaped, a new one started (with a new meter) — after a goal that sets +/// an option (`z3` keeps options across `(reset)`), after any goal it did not +/// answer with a clean verdict (an error, or no verdict where this crate's +/// `(check-sat)` answers), and whenever it breaks (the script cannot be +/// written, or `z3`'s output ends before the marker). Each goal is therefore +/// decided as a fresh `z3` would decide it. The new session is started after +/// the attempt's span has stopped; its startup is in the attempt's overhead, +/// never in its figure. +/// +/// **Metering.** Each decision is written to the resident `z3` and its +/// verdict read back; the work runs in that process while this thread waits, +/// so this process's own energy count would read the waiting. Where the +/// host's kernel counts each process's CPU energy live +/// ([`sandbox_meter::TreeMeter`]: macOS, where its liveness probe passed), the +/// decision is read off the resident `z3`'s own process tree instead — the +/// CPU energy the kernel attributes to `z3`'s threads (and any descendant's) +/// from just before the script is written to just after the verdict's end +/// marker is read, each end walked until the tree is quiet (up to the +/// settle bound, [`Z3Server::with_settle_bound`]). A session's meter is built +/// when the session starts: the first one in a process pays the counter's +/// liveness probe, about 300 ms of CPU on the constructing thread, so the +/// first goal does not. +/// +/// The attempt's figure is that reading, `HwShunt` ([`Energy::measured`]), +/// rounded UP to a whole µJ (a reading of 1 to 999 nJ is 1 µJ, never a +/// measured zero), only when **both** hold: +/// +/// 1. **Nothing was seen missing from the tree.** The reading has no gap +/// ([`TreeReading::is_whole`]): every member read and quiet at both ends, +/// no descendant reaped or exited in the span, no GPU client held, no +/// in-process Neural Engine memory — and no gap of any kind the meter +/// reports now or comes to report. +/// 2. **There is nothing outside the tree to miss, on the operator's +/// declaration.** A tree reading cannot see work its process hands to +/// another (a system service, a server, a solver in a container, a VM or +/// on another host): that is charged to the other process. A `z3` on +/// `PATH` that forwards each goal elsewhere reads whole — only the +/// forwarding client is in the tree — and would be sealed far short of +/// the decision. This crate cannot tell: it names `z3` by `PATH`, and +/// spawning it says nothing about what answers to that name. So, as +/// jcp-gateway seals an upstream's reading and sandbox-proof a local +/// engine's only on its operator's declaration that it delegates +/// nothing, a reading here is sealed only on the operator's declaration +/// that the `z3` it runs — the binary at [`Z3EnergyAccount::z3`], the +/// first on `PATH` with symlinks resolved — decides each goal in its own +/// process tree ([`Z3Server::declared_self_contained`]; proof-cli reads +/// `PROOF_Z3_SELF_CONTAINED=1`). Undeclared, the default, a whole reading +/// keeps the model figure ([`Modelled::NotDeclaredSelfContained`]). +/// Condition 1 still applies to every reading, so a declared `z3` that +/// forked or used the GPU is graded down by its gaps. +/// +/// Otherwise the attempt keeps the model figure it always had — the +/// solver's wall time × the crate's ~15 W model, [`Energy::modeled`] — and +/// never seals the reading: [`Energy`] has no coverage field, so a reading of +/// part of the decision sealed as `HwShunt` would claim the whole. The +/// model is the figure when: +/// +/// - the reading has a gap ([`Modelled::Gaps`]: it is short of the tree's +/// energy, or with a member still running at the start may hold a little +/// from before the span); +/// - the reading was taken, but the `z3` is not declared self-contained +/// ([`Modelled::NotDeclaredSelfContained`]); +/// - the span gave no reading ([`Modelled::NoReading`]: `z3` gone, or its +/// count not advanced); +/// - there is no tree meter ([`Modelled::NoTreeMeter`]: off macOS, or the +/// per-process counter is not live here); +/// - the goal never reached `z3` ([`Modelled::NotRun`]: refused by the shape +/// guard, or no session); +/// - the goal was refuted ([`Modelled::CounterModelOutsideTree`]): the +/// counter-model is fetched by a ONE-SHOT `z3`, a child of this process, +/// not of the resident one, so it is outside the tree. Its span is never +/// opened over it — the tree span covers the resident decision alone — and +/// its work is in the attempt's figure only through the model, which then +/// covers the whole attempt: the resident decision and the one-shot run. +/// +/// Why each attempt was graded as it was is kept beside it, not on the wire: +/// [`Z3Server::last_account`]. +/// +/// **Cost.** The span adds two things to each goal's latency, at each end. +/// The tree is walked until it is quiet: `z3` blocks on its next read as +/// soon as it has written the end marker, so on a quiet host that is a few +/// walks of one process (tens of µs each), and on a loaded one up to the +/// settle bound, after which a reading still unsettled is a gap (the model +/// figure). And the GPU clients are read from the I/O Registry — before the +/// start walk and after the stop walk, outside the settle bound — which +/// takes about a millisecond on the hosts measured and has been seen at +/// tens of milliseconds under heavy load. Together, on a loaded development +/// host at the production bound, that has come to a few milliseconds for a +/// typical goal, several at the 90th percentile and tens at worst; the test +/// `the_production_settle_bound_grades_every_attempt_consistently` logs the +/// figures on the host it runs on. The model figure times the solver's work +/// alone — the resident decision and, when it runs, the one-shot `z3` — +/// never the meter's walks or reads, nor a retired session's replacement +/// starting after the span. pub struct Z3Server { - session: Mutex>, + /// The resident session and its meter: `None` when `z3` could not be + /// started. + resident: Mutex>, + /// The settle bound each session's meter is built with; `None`: the + /// meter's default. + settle_bound: Option, + /// The operator's declaration that the `z3` it runs decides each goal in + /// its own process tree ([`Z3Server::declared_self_contained`]). + self_contained: bool, + /// How the last attempt's energy was obtained. + last: Mutex>, +} + +/// A resident session and the tree meter of its `z3`, retired together. +struct Resident { + session: Z3Session, + /// The binary the session was started from ([`resolve_z3`]). + z3: PathBuf, + /// The resident `z3`'s tree meter: `None` off macOS, or where the + /// per-process counter is not live. + meter: Option, +} + +impl Resident { + /// Start a session on the `z3` on `PATH` and, where this host can read + /// it, its meter. + fn start(settle_bound: Option) -> Option { + let z3 = resolve_z3()?; + let session = Z3Session::spawn(&z3)?; + let meter = TreeMeter::for_process(session.pid()).map(|m| match settle_bound { + Some(bound) => m.with_settle_bound(bound), + None => m, + }); + Some(Self { session, z3, meter }) + } +} + +/// Why a [`Z3Server`] attempt's figure is the model rather than a reading of +/// the resident `z3`'s tree. An attempt can have several. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Modelled { + /// The goal never reached the resident `z3`: the shape guard refused it, + /// or there is no session (`z3` absent). Nothing ran that could be read. + NotRun, + /// This host has no tree meter for the resident `z3`: not macOS, or the + /// kernel's per-process CPU energy counter is not live here. + NoTreeMeter, + /// The span over the decision gave no reading at all: `z3` gone or + /// unreadable at an end, or its count did not advance. + NoReading(TreeError), + /// The reading saw part of the tree's energy missing (or, for a member + /// still running at the start, possibly some from before the span): a + /// partial figure, never sealed as the decision's. + Gaps(Vec), + /// A reading was taken, but the operator has not declared that the `z3` + /// it runs decides in its own process tree + /// ([`Z3Server::declared_self_contained`]). Work handed outside the tree + /// — to a solver in a container, a VM or on another host — is charged + /// to the process that does it, so no reading of the tree can show it, + /// and a forwarding `z3` reads whole. + NotDeclaredSelfContained, + /// The goal was refuted, and its counter-model fetched by a one-shot `z3` + /// outside the resident tree, which no span read. + CounterModelOutsideTree, +} + +/// How one [`Z3Server`] attempt's energy was obtained: the figure the attempt +/// reported, the reading it was graded from, and why the model was kept where +/// it was. The gateway's plaintext account, in-process: the attempt's figure +/// and its provenance are what travels; this says why. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Z3EnergyAccount { + /// The attempt's figure, exactly as [`Attempt::energy`] reported it. + pub energy: Energy, + /// The resident `z3`'s tree reading over the decision, when a span was + /// opened: `None` when the goal never reached `z3` or there is no meter. + pub reading: Option>, + /// Empty when the figure is the reading; otherwise every reason the + /// model figure was kept. + pub modelled_because: Vec, + /// The model figure, µJ: the solver's wall time (the resident decision, + /// and the one-shot `z3` when it ran) × the crate's ~15 W model, at least + /// 1. The attempt's figure whenever `modelled_because` is not empty. + pub modelled_uj: u64, + /// The solver's own wall time: what `modelled_uj` is computed from. + pub work: Duration, + /// The attempt's wall time beyond `work`: the meter's settling at both + /// ends of the span, and the rest of the attempt's bookkeeping. The + /// latency the metering adds to the goal. + pub overhead: Duration, + /// The binary of the resident `z3` the goal was written to: the absolute + /// path its session was started from (the first `z3` on `PATH`, symlinks + /// resolved). What an operator's declaration is about. `None` when the + /// goal reached no session. + pub z3: Option, +} + +/// Grade a [`Z3Server`] attempt's energy. `reading`: the resident tree's span +/// over the decision, `None` when no span was opened; `ran`: the goal reached +/// the resident `z3`; `self_contained`: the operator's declaration; +/// `one_shot`: a one-shot `z3` fetched a counter-model outside the tree; +/// `modelled_uj`: the model figure. +/// +/// `HwShunt` only for a reading with no gap at all, of a decision that ran +/// entirely in the tree, of a `z3` declared self-contained; otherwise the +/// model, with every reason. Pure, so its tests drive every case without a +/// process. +fn grade_attempt( + reading: Option<&Result>, + ran: bool, + self_contained: bool, + one_shot: bool, + modelled_uj: u64, +) -> (Energy, Vec) { + let mut because: Vec = Vec::new(); + if !ran { + because.push(Modelled::NotRun); + } + match reading { + Some(Ok(r)) => { + if !r.is_whole() { + because.push(Modelled::Gaps(r.gaps.clone())); + } + if !self_contained { + because.push(Modelled::NotDeclaredSelfContained); + } + } + Some(Err(e)) => because.push(Modelled::NoReading(e.clone())), + None if ran => because.push(Modelled::NoTreeMeter), + None => {} + } + if one_shot { + because.push(Modelled::CounterModelOutsideTree); + } + match reading { + Some(Ok(r)) if because.is_empty() => (Energy::measured(r.cpu_nj.div_ceil(1_000)), because), + _ => (Energy::modeled(modelled_uj.max(1)), because), + } } impl Z3Server { + /// Start the resident `z3` and, where this host can read it, its tree + /// meter (the first one in a process pays the counter's liveness probe: + /// see [`Z3Server`]). pub fn new() -> Self { Self { - session: Mutex::new(Z3Session::spawn()), + resident: Mutex::new(Resident::start(None)), + settle_bound: None, + self_contained: false, + last: Mutex::new(None), } } + + /// The same server, its tree meter waiting up to `bound` at each end of + /// a decision for the resident `z3` to go quiet (default + /// [`sandbox_meter::probe::SETTLE_BOUND`]). A `z3` still running when it + /// runs out is a gap, so that decision keeps the model figure; a longer + /// bound trades latency on a loaded host for fewer of those. It holds for + /// every session the server starts. + pub fn with_settle_bound(mut self, bound: Duration) -> Self { + self.settle_bound = Some(bound); + if let Ok(Some(r)) = self.resident.get_mut() { + r.meter = r.meter.take().map(|m| m.with_settle_bound(bound)); + } + self + } + + /// The same server, on its operator's declaration that the `z3` it runs + /// — the binary at [`Z3EnergyAccount::z3`] — decides each goal in its + /// own process tree, handing no work to any other process: no container, + /// VM, service or remote solver. A whole reading of a decision is sealed + /// `HwShunt` only with it. Only the operator can make it: this crate + /// names `z3` by `PATH`, and whatever answers to that name is what runs. + /// Undeclared (the default), every decision keeps the model figure + /// ([`Modelled::NotDeclaredSelfContained`]). proof-cli reads it from + /// `PROOF_Z3_SELF_CONTAINED=1`. + pub fn declared_self_contained(mut self, declared: bool) -> Self { + self.self_contained = declared; + self + } + + /// The resident `z3`'s pid, while there is a session. A retired session's + /// replacement has a new one. + pub fn pid(&self) -> Option { + self.resident.lock().ok()?.as_ref().map(|r| r.session.pid()) + } + + /// Whether decisions are read off the resident `z3`'s tree: a session, + /// and a live per-process counter on this host. + pub fn is_tree_metered(&self) -> bool { + self.resident.lock().is_ok_and(|g| g.as_ref().is_some_and(|r| r.meter.is_some())) + } + + /// How the last attempt's energy was obtained ([`Z3EnergyAccount`]). + pub fn last_account(&self) -> Option { + self.last.lock().ok()?.clone() + } } impl Default for Z3Server { @@ -409,29 +951,80 @@ impl Solver for Z3Server { } fn attempt(&self, goal: &ProofGoal) -> Attempt { let start = Instant::now(); - let outcome = if looks_like_smt(&goal.statement) { - self.session - .lock() - .ok() - .and_then(|mut g| g.as_mut().and_then(|s| s.decide(&goal.statement))) - } else { - None - }; - let verdict = match outcome.as_deref() { - Some("unsat") => Verdict::Proved { + let mut work = Duration::ZERO; + let mut reading: Option> = None; + let mut ran = false; + let mut z3: Option = None; + let outcome = admit(&goal.statement).and_then(|script| { + let mut g = self.resident.lock().ok()?; + let r = g.as_mut()?; + ran = true; + z3 = Some(r.z3.clone()); + let session = &mut r.session; + // The span is the resident decision and nothing else: opened + // just before the script is written, stopped once the end + // marker is read. + let mut decide = || { + let t = Instant::now(); + let v = session.decide(&goal.statement); + work += t.elapsed(); + v + }; + let answer = match &r.meter { + Some(m) => { + let (v, rd) = m.measure(decide); + reading = Some(rd); + v + } + None => decide(), + }; + // Retire the session unless it answered cleanly and holds no + // option of this goal's: the next goal must meet a fresh `z3`. + if script.sets_option || !matches!(answer, Ok(Answer::Verdict(_))) { + *g = None; + *g = Resident::start(self.settle_bound); + } + match answer { + Ok(Answer::Verdict(v)) => Some(v), + Ok(Answer::Undecided) | Err(Broken) => None, + } + }); + let mut one_shot = false; + let verdict = match outcome { + Some(CheckSat::Unsat) => Verdict::Proved { artifact: ContentId::of_bytes(goal.statement.as_bytes()), }, // `sat` ⇒ refuted. The resident session decided it; fetch the // witness with a one-shot `z3` (the refutation path is terminal, so - // the extra spawn never touches the hot proved path). - Some("sat") => refutation_or_undecided(&goal.statement), + // the extra spawn never touches the hot proved path). That `z3` is + // not in the resident tree, and runs after its span has stopped. + Some(CheckSat::Sat) => { + one_shot = true; + let t = Instant::now(); + let v = refutation_or_undecided(&goal.statement); + work += t.elapsed(); + v + } _ => Verdict::Unproved, }; - let uj = ns_to_uj(start.elapsed().as_nanos()).max(1); + let modelled_uj = ns_to_uj(work.as_nanos()).max(1); + let (energy, modelled_because) = + grade_attempt(reading.as_ref(), ran, self.self_contained, one_shot, modelled_uj); + if let Ok(mut last) = self.last.lock() { + *last = Some(Z3EnergyAccount { + energy, + reading, + modelled_because, + modelled_uj, + work, + overhead: start.elapsed().saturating_sub(work), + z3, + }); + } Attempt { tier: Tier::Smt, verdict, - energy: Energy::modeled(uj), + energy, } } } @@ -633,9 +1226,15 @@ pub fn real_ladder() -> Vec> { vec![Box::new(Propositional), Box::new(Z3Smt)] } -/// Like [`real_ladder`] but with `z3` kept resident at T1. -pub fn resident_z3_ladder() -> Vec> { - vec![Box::new(Propositional), Box::new(Z3Server::new())] +/// Like [`real_ladder`] but with `z3` kept resident at T1, on its +/// operator's declaration (`self_contained`) or without it +/// ([`Z3Server::declared_self_contained`]): undeclared, no T1 decision is +/// sealed as a hardware reading. +pub fn resident_z3_ladder(self_contained: bool) -> Vec> { + vec![ + Box::new(Propositional), + Box::new(Z3Server::new().declared_self_contained(self_contained)), + ] } /// Whether a working `z3` is on PATH — lets callers/tests adapt honestly. @@ -661,7 +1260,8 @@ mod tests { fn ladder_is_sound() { for (name, ladder) in [ ("real_ladder", real_ladder()), - ("resident_z3_ladder", resident_z3_ladder()), + ("resident_z3_ladder", resident_z3_ladder(false)), + ("resident_z3_ladder declared", resident_z3_ladder(true)), ] { assert!(!ladder.is_empty(), "{name}: a real ladder needs a rung"); for rung in &ladder { @@ -685,7 +1285,7 @@ mod tests { "real_ladder membership changed — is the new rung a decision procedure?" ); assert_eq!( - resident_z3_ladder() + resident_z3_ladder(false) .iter() .map(|r| r.tier()) .collect::>(), @@ -886,9 +1486,403 @@ mod tests { assert!(server.attempt(&comm).verdict.is_proved()); assert!(server.attempt(&thm).verdict.is_proved()); // still healthy after prose } - assert_eq!(resident_z3_ladder().len(), 2); // decision procedures only - assert!(looks_like_smt("(assert (> x 0))")); - assert!(!looks_like_smt("∃ continuous f")); - assert!(!looks_like_smt("(unbalanced")); + assert_eq!(resident_z3_ladder(false).len(), 2); // decision procedures only + assert!(admit("(assert (> x 0))").is_some()); + assert!(admit("∃ continuous f").is_none()); + assert!(admit("(unbalanced").is_none()); + } + + fn smt(s: &str) -> ProofGoal { + ProofGoal::new(s, "smt2", GoalKind::Decidable) + } + + /// Valid, asserted negated: `unsat`, so proved. + const VALID_X: &str = "(declare-const x Int)(assert (not (= x x)))"; + const VALID_BV: &str = "(declare-const x (_ BitVec 32))\n\ + (assert (not (= (bvmul x #x00000003) (bvadd x (bvadd x x)))))"; + /// FALSE (`y > 0` for every `y`), asserted negated: `sat`, so refuted. + const FALSE_Y: &str = "(declare-const y Int)(assert (not (> y 0)))"; + + /// `f` on a thread of its own, its value if it returns within `limit`. A + /// goal that wedges the resident session would hang the test run, so a + /// hang is a failure here rather than a stuck suite. + fn within(limit: Duration, f: impl FnOnce() -> T + Send + 'static) -> T { + let (tx, rx) = std::sync::mpsc::channel(); + std::thread::spawn(move || { + let _ = tx.send(f()); + }); + rx.recv_timeout(limit).expect("the attempt did not return: the z3 session is wedged") + } + + /// A goal that prints the session's end marker must not shift every + /// later verdict by one. With a fixed marker it did: the FALSE claim + /// after it was read off the previous goal's `unsat` and sealed proved. + /// A marker-shaped statement is refused (undecided), and the goals + /// after it are decided on their own output. + #[test] + fn an_injected_end_marker_never_desyncs_the_resident_session() { + if !z3_available() { + eprintln!("z3 not installed: no resident session to desync"); + return; + } + let server = Z3Server::new(); + let a = server.attempt(&smt(&format!("(echo \"@@END@@\"){VALID_X}"))); + let b = server.attempt(&smt(FALSE_Y)); + let c = server.attempt(&smt(VALID_X)); + assert!(!b.verdict.is_proved(), "a FALSE claim came back proved: {:?}", b.verdict); + assert!(b.verdict.is_refuted(), "the false claim is refuted on its own output: {:?}", b.verdict); + assert!(c.verdict.is_proved(), "{:?}", c.verdict); + assert_eq!(a.verdict, Verdict::Unproved, "a marker-shaped goal is refused, never decided"); + } + + /// Below the refusal: the marker is fresh and unpredictable per goal, so + /// even a script that prints the old fixed marker (or anything else) + /// cannot end a read early. Driven on the session itself. + #[test] + fn the_session_marker_is_fresh_per_goal() { + if !z3_available() { + eprintln!("z3 not installed: no session"); + return; + } + let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH")).expect("a z3 session"); + let injected = format!("(echo \"@@END@@\")(echo \"unsat\"){FALSE_Y}"); + assert_eq!(s.decide(&injected), Ok(Answer::Verdict(CheckSat::Sat))); + assert_eq!(s.decide(FALSE_Y), Ok(Answer::Verdict(CheckSat::Sat))); + assert_eq!(s.decide(VALID_X), Ok(Answer::Verdict(CheckSat::Unsat))); + assert_ne!(end_marker(), end_marker()); + assert!(end_marker().starts_with(END_MARKER_PREFIX)); + } + + /// A goal can print a verdict-shaped line itself. The one-shot rung read + /// the FIRST such line, so `(echo "unsat")` before a false claim proved + /// it. The answer is the line this crate's own `(check-sat)` printed, + /// just before the end marker, on both rungs. + #[test] + fn an_echoed_verdict_is_never_read_as_the_answer() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let spoof = smt(&format!("(echo \"unsat\"){FALSE_Y}")); + let one_shot = Z3Smt.attempt(&spoof); + assert!(!one_shot.verdict.is_proved(), "one-shot proved a FALSE claim: {:?}", one_shot.verdict); + let resident = Z3Server::new().attempt(&spoof); + assert!(!resident.verdict.is_proved(), "resident proved a FALSE claim: {:?}", resident.verdict); + // And a goal ending in its own `(check-sat)` and more output. + let tail = smt(&format!("{FALSE_Y}(check-sat)(echo \"unsat\")")); + assert!(!Z3Smt.attempt(&tail).verdict.is_proved()); + assert!(!Z3Server::new().attempt(&tail).verdict.is_proved()); + } + + /// z3 reports an error and carries on, answering `(check-sat)` over the + /// part that parsed. One-shot read that as undecided; the resident rung + /// read the `sat` of the partial stack and came back REFUTED with a + /// model. An error anywhere is undecided on both rungs. + #[test] + fn a_goal_that_errors_is_undecided_on_both_rungs() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let err = smt("(declare-const x Int)(assert (> x 0))(assert (bogus x))"); + assert_eq!(Z3Smt.attempt(&err).verdict, Verdict::Unproved); + let server = Z3Server::new(); + assert_eq!(server.attempt(&err).verdict, Verdict::Unproved); + // The session goes on deciding after it. + assert!(server.attempt(&smt(VALID_BV)).verdict.is_proved()); + assert!(server.attempt(&smt(FALSE_Y)).verdict.is_refuted()); + } + + /// z3 keeps `set-option` across `(reset)`: a goal's options reached + /// every later goal on the resident session (`:rlimit 1` turned the next + /// valid claim `unknown`). A goal that sets an option is decided, and + /// its session is retired after it. + #[test] + fn a_goal_option_never_reaches_the_next_goal() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let server = Z3Server::new(); + let before = server.pid(); + let _ = server.attempt(&smt(&format!("(set-option :rlimit 1){VALID_X}"))); + assert_ne!(server.pid(), before, "the session that ran a set-option goal was kept"); + let next = server.attempt(&smt(VALID_BV)); + assert!(next.verdict.is_proved(), "the previous goal's option reached this one: {:?}", next.verdict); + } + + /// A session that breaks (here: its `z3` killed) is replaced, not reused: + /// the attempt that found it broken is undecided, the next is decided on + /// a fresh `z3`. + #[test] + fn a_broken_session_is_replaced() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let server = Z3Server::new(); + let pid = server.pid().expect("a resident z3"); + let killed = Command::new("kill").args(["-9", &pid.to_string()]).status().expect("kill"); + assert!(killed.success()); + std::thread::sleep(Duration::from_millis(50)); + assert_eq!(server.attempt(&smt(VALID_X)).verdict, Verdict::Unproved); + assert_ne!(server.pid(), Some(pid), "the broken session was kept"); + assert!(server.attempt(&smt(VALID_X)).verdict.is_proved()); + } + + /// Goals that would wedge the session — leave a string or quoted symbol + /// open (swallowing the marker), send z3's answers elsewhere, end z3, + /// or read a file — are refused at once, and the session decides on. + #[test] + fn a_goal_that_would_wedge_the_session_is_refused_at_once() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let verdicts = within(Duration::from_secs(60), || { + let server = Z3Server::new(); + let mut out = Vec::new(); + for wedge in [ + format!("{VALID_X}(echo \"x)"), + format!("{VALID_X}(declare-const |a) Int)"), + format!("(set-option :regular-output-channel \"/dev/null\"){VALID_X}"), + format!("(|set-option| :diagnostic-output-channel \"/dev/null\"){VALID_X}"), + format!("{VALID_X}(exit)"), + format!("{VALID_X}(|exit|)"), + format!("(include \"/dev/null\"){VALID_X}"), + ] { + out.push((wedge.clone(), server.attempt(&smt(&wedge)).verdict, Z3Smt.attempt(&smt(&wedge)).verdict)); + } + out.push(("after".into(), server.attempt(&smt(VALID_X)).verdict, Verdict::Unproved)); + out + }); + let (last, rest) = verdicts.split_last().expect("verdicts"); + for (goal, resident, one_shot) in rest { + assert_eq!(resident, &Verdict::Unproved, "{goal}"); + assert_eq!(one_shot, &Verdict::Unproved, "{goal}"); + } + assert!(last.1.is_proved(), "the session decides on after the refusals: {:?}", last.1); + } + + /// The shape guard, case by case, without `z3`. + #[test] + fn the_shape_guard_admits_whole_commands_only() { + let admitted = |s: &str| admit(s).is_some(); + // Whole commands, with parentheses inside strings, quoted symbols and + // comments not counted, and `""` an escaped quote. + assert!(admitted(VALID_X)); + assert!(admitted("(declare-const |a (b| Int)(assert (= |a (b| |a (b|))")); + assert!(admitted("(echo \"(\")(echo \"say \"\"hi\"\" )\")")); + assert!(admitted("; a comment ) with ( parens\n(assert true) ; trailing comment")); + assert_eq!(admit("(set-option :rlimit 1)(assert true)"), Some(Admitted { sets_option: true })); + assert_eq!(admit("(|set-option| :timeout 5)"), Some(Admitted { sets_option: true })); + assert_eq!(admit(VALID_X), Some(Admitted { sets_option: false })); + // Refused. + for s in [ + "", + " ; only a comment", + "∃ continuous f", + "(assert true) stray", + "\"top-level string\"", + "(assert true))(", + "(assert (> x 0)", + "()", + "((assert true))", + "(echo \"x)", + "(declare-const |a) Int)", + "(echo \"@@END@@\")", + "(declare-const @@END@@x Int)", + "(exit)", + "(|exit|)", + "(include \"goal.smt2\")", + "(set-option :regular-output-channel \"/dev/null\")", + "(set-option ; sneaky\n :diagnostic-output-channel \"x\")", + ] { + assert!(!admitted(s), "admitted {s:?}"); + } + } + + /// The answer is the line just before the marker, and only when no + /// line of the output is an error. + #[test] + fn the_answer_is_the_line_before_the_marker_with_no_error() { + let answer = |lines: &[&str]| { + let mut r = Reply::default(); + for l in lines { + r.line(l); + } + r.answer() + }; + assert_eq!(answer(&["unsat"]), Answer::Verdict(CheckSat::Unsat)); + assert_eq!(answer(&["unsat", "sat\n"]), Answer::Verdict(CheckSat::Sat)); + assert_eq!(answer(&["sat", "unknown"]), Answer::Verdict(CheckSat::Unknown)); + assert_eq!(answer(&["unsat", "x"]), Answer::Undecided, "a verdict before other output is the goal's"); + assert_eq!(answer(&[]), Answer::Undecided); + assert_eq!(answer(&["(error \"line 1: unknown constant\")", "sat"]), Answer::Undecided); + assert_eq!(answer(&["unsat", "(error \"oops\")", "unsat"]), Answer::Undecided); + } + + /// A reading of the resident tree, as the meter would give it. + fn reading(cpu_nj: u64, gaps: Vec) -> TreeReading { + TreeReading { + cpu_uj: cpu_nj.div_ceil(1_000), + cpu_nj, + processes: 1, + pids: vec![4242], + wall: Duration::from_millis(3), + gaps, + } + } + + /// The one case a Z3Server attempt is a hardware reading: a span over a + /// decision that ran entirely in the resident tree, with nothing seen + /// missing. Its figure is the reading's nanojoules rounded UP to the + /// attempt's microjoule, so a reading is never sealed as a measured zero. + #[test] + fn a_whole_reading_of_a_resident_decision_is_hwshunt_rounded_up() { + for (nj, uj) in [(2_345_001, 2_346), (2_345_000, 2_345), (1, 1), (999, 1)] { + let r: Result = Ok(reading(nj, Vec::new())); + let (e, because) = grade_attempt(Some(&r), true, true, false, 77); + assert_eq!(e, Energy::measured(uj), "{nj} nJ"); + assert!(because.is_empty(), "{because:?}"); + assert!(e.check_provenance().is_ok()); + } + } + + /// Every gap the meter can report grades the attempt down to the model, + /// and the reading is never sealed: Energy has no coverage field, so a + /// partial reading as `HwShunt` would claim the whole decision. This + /// includes the gap that can put energy from BEFORE the span into the + /// figure (`Unsettled` at the start), and the GPU and Neural Engine gaps + /// a CPU reading cannot cover. + #[test] + fn a_reading_with_any_gap_keeps_the_model_figure() { + use sandbox_meter::SpanEnd; + let gaps = [ + TreeGap::Unreadable { pid: 7, errno: 1, end: SpanEnd::Stop }, + TreeGap::Unlisted { pid: 7, errno: 1, end: SpanEnd::Start }, + TreeGap::Unsettled { pid: 4242, end: SpanEnd::Start }, + TreeGap::Unsettled { pid: 4242, end: SpanEnd::Stop }, + TreeGap::Changing { end: SpanEnd::Stop }, + TreeGap::PredatesSpan { pid: 7 }, + TreeGap::Gone { pid: 7 }, + TreeGap::EnergyWentBack { pid: 4242 }, + TreeGap::ReapedDescendant { pid: 4242, cpu: Duration::from_millis(2) }, + TreeGap::Exited { pid: 4242 }, + TreeGap::Gpu { ns: 5_000 }, + TreeGap::GpuUnknown { pid: None }, + TreeGap::GpuUnknown { pid: Some(4242) }, + TreeGap::NeuralEngine { pid: 4242, bytes: 1 << 20 }, + ]; + for gap in gaps { + let r: Result = Ok(reading(5_000_000, vec![gap.clone()])); + let (e, because) = grade_attempt(Some(&r), true, true, false, 77); + assert_eq!(e, Energy::modeled(77), "{gap:?} was sealed as the reading"); + assert_eq!(because, vec![Modelled::Gaps(vec![gap])]); + } + } + + /// No reading, no meter, nothing run: the model figure, each with its + /// reason. And a refuted goal, whose counter-model a one-shot `z3` + /// fetched outside the resident tree, keeps the model for the whole + /// attempt even when the resident decision's reading was whole: the + /// one-shot run is in no span, and a reading of the decision alone + /// sealed as `HwShunt` would claim the attempt. + #[test] + fn an_attempt_with_no_whole_reading_of_all_its_work_keeps_the_model() { + let gone: Result = Err(TreeError::RootGone { pid: 4242 }); + let (e, because) = grade_attempt(Some(&gone), true, true, false, 12); + assert_eq!((e, because), (Energy::modeled(12), vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })])); + + let (e, because) = grade_attempt(None, true, true, false, 12); + assert_eq!((e, because), (Energy::modeled(12), vec![Modelled::NoTreeMeter])); + + let (e, because) = grade_attempt(None, false, true, false, 0); + assert_eq!((e, because), (Energy::modeled(1), vec![Modelled::NotRun]), "the model figure is at least 1 µJ"); + + let whole: Result = Ok(reading(3_000_000, Vec::new())); + let (e, because) = grade_attempt(Some(&whole), true, true, true, 900); + assert_eq!((e, because), (Energy::modeled(900), vec![Modelled::CounterModelOutsideTree])); + + // Both reasons, when both hold. + let gapped: Result = Ok(reading(3_000_000, vec![TreeGap::Gone { pid: 9 }])); + let (e, because) = grade_attempt(Some(&gapped), true, true, true, 900); + assert_eq!(e, Energy::modeled(900)); + assert_eq!(because, vec![Modelled::Gaps(vec![TreeGap::Gone { pid: 9 }]), Modelled::CounterModelOutsideTree]); + } + + /// Without the operator's declaration a reading — even a whole one — is + /// never sealed: the tree cannot show work its `z3` hands elsewhere. The + /// reason rides beside any other; with no reading there is nothing the + /// declaration would change, and it is not given as a reason. + #[test] + fn an_undeclared_z3_keeps_the_model_for_any_reading() { + let whole: Result = Ok(reading(5_000_000, Vec::new())); + let (e, because) = grade_attempt(Some(&whole), true, false, false, 77); + assert_eq!((e, because), (Energy::modeled(77), vec![Modelled::NotDeclaredSelfContained])); + + let gapped: Result = Ok(reading(5_000_000, vec![TreeGap::Gone { pid: 9 }])); + let (e, because) = grade_attempt(Some(&gapped), true, false, true, 77); + assert_eq!(e, Energy::modeled(77)); + assert_eq!( + because, + vec![ + Modelled::Gaps(vec![TreeGap::Gone { pid: 9 }]), + Modelled::NotDeclaredSelfContained, + Modelled::CounterModelOutsideTree + ] + ); + + let gone: Result = Err(TreeError::RootGone { pid: 4242 }); + assert_eq!(grade_attempt(Some(&gone), true, false, false, 12).1, vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })]); + assert_eq!(grade_attempt(None, true, false, false, 12).1, vec![Modelled::NoTreeMeter]); + } + + /// The account names the binary the goal was written to: absolute, + /// symlinks resolved, and the one a spawn by name finds on `PATH` (the + /// shell's own lookup is the oracle). The default server is undeclared. + #[cfg(unix)] + #[test] + fn the_account_names_the_z3_binary_that_ran() { + if !z3_available() { + eprintln!("z3 not installed"); + return; + } + let server = Z3Server::new(); + assert!(server.attempt(&smt(VALID_X)).verdict.is_proved()); + let acct = server.last_account().expect("an account"); + let z3 = acct.z3.expect("the account names the z3 it ran"); + let shell = Command::new("sh").args(["-c", "command -v z3"]).output().expect("sh"); + let found = PathBuf::from(String::from_utf8_lossy(&shell.stdout).trim()).canonicalize().expect("canonical"); + assert!(z3.is_absolute(), "{z3:?}"); + assert_eq!(z3, found); + if acct.reading.as_ref().is_some_and(Result::is_ok) { + assert!(acct.modelled_because.contains(&Modelled::NotDeclaredSelfContained), "{:?}", acct.modelled_because); + } + // A goal refused before any session is reached names none. + let _ = server.attempt(&smt("(exit)")); + assert_eq!(server.last_account().expect("an account").z3, None); + } + + /// Off macOS there is no per-process energy counter, so no tree meter: + /// every attempt that reaches `z3` keeps the model figure and says why. + #[cfg(not(target_os = "macos"))] + #[test] + fn off_macos_a_resident_decision_keeps_the_model_and_says_why() { + // Declared, so the one reason is the missing meter. + let server = Z3Server::new().declared_self_contained(true); + assert!(!server.is_tree_metered()); + if !z3_available() { + eprintln!("z3 not installed: the resident session is absent, nothing to decide"); + return; + } + let thm = ProofGoal::new("(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))", "smt2", GoalKind::Decidable); + let a = server.attempt(&thm); + assert!(a.verdict.is_proved()); + let acct = server.last_account().expect("an account of the attempt"); + eprintln!("z3 resident (no tree meter): {acct:?}"); + assert_eq!(a.energy, Energy::modeled(acct.modelled_uj)); + assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]); + assert_eq!(acct.reading, None); } } diff --git a/proof/proof-rs/crates/proof-solvers/tests/z3_tree.rs b/proof/proof-rs/crates/proof-solvers/tests/z3_tree.rs new file mode 100644 index 000000000..f4cf9ec29 --- /dev/null +++ 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 { + 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 { + 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(¬_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 = Vec::new(); + let mut works: Vec = 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 = 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); + } +} diff --git a/sandbox/sandbox-rs/Cargo.lock b/sandbox/sandbox-rs/Cargo.lock index 0777052a6..6d18834e5 100644 --- 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", diff --git a/sandbox/sandbox-rs/crates/sandbox-proof/Cargo.toml b/sandbox/sandbox-rs/crates/sandbox-proof/Cargo.toml index 16cfa1053..9cde06843 100644 --- 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" diff --git a/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs b/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs index ed5e5e77b..69284d685 100644 --- a/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs +++ b/sandbox/sandbox-rs/crates/sandbox-proof/src/lib.rs @@ -445,16 +445,112 @@ fn nvidia_smi(query: &str) -> Option { .and_then(|s| s.lines().next().map(|l| l.trim().to_string())) } +/// One run of the accelerator workload to completion: its exit, the +/// machine-wide meter's span over exactly that run, and the GPU power +/// samples taken while it ran. +struct AcceleratorRun { + status: std::process::ExitStatus, + /// [`sandbox_meter::PowerMeter::detect`]'s span, opened just before the + /// workload was spawned and closed once it had exited. + machine: sandbox_meter::Measurement, + /// `nvidia-smi` power-draw samples, W, about one a second while the + /// workload ran: the GPU figure's fallback where the meter has no GPU + /// counter. + powers: Vec, +} + +/// Run `cmd args` to completion inside a span of `meter`, sampling the GPU's +/// power with `sample_power` about once a second while it runs. +fn run_accelerator_workload( + cmd: &str, + args: &[String], + meter: &mut sandbox_meter::PowerMeter, + mut sample_power: impl FnMut() -> Option, +) -> std::io::Result { + use std::time::{Duration, Instant}; + let span = meter.start(); + let mut child = std::process::Command::new(cmd).args(args).spawn()?; + let mut powers: Vec = Vec::new(); + let mut next = Instant::now() + Duration::from_secs(1); + let status = loop { + if let Some(status) = child.try_wait()? { + break status; + } + if Instant::now() >= next { + powers.extend(sample_power()); + next += Duration::from_secs(1); + } + std::thread::sleep(Duration::from_millis(20)); + }; + let machine = span.stop(meter); + Ok(AcceleratorRun { status, machine, powers }) +} + +/// The accelerator proof's two device records (SPEC §6.2: one per class +/// used, the GPU's never folded into the CPU's or left out), each the best +/// figure for its class this host gave, sealed as what it is: +/// +/// - `Cpu`: the machine meter's `Cpu` record over the run — the RAPL package +/// counters' reading, `HwShunt`, where every package counter is live (or +/// the meter's own estimator record, where the span's CPU counter held) — +/// else `cpu_estimate`, the meter's wall-clock estimator for the run. +/// - `Gpu`: the machine meter's `Gpu` record — NVML's total-energy counter, +/// `HwShunt`, where every GPU's counter is live and advanced over the run +/// — else `gpu_sampled_uj`, sampled power × the run's time, `ModelBased`; +/// with neither, there is no GPU figure to seal and the proof is refused. +/// A GPU record of zero is no reading: the meter's held-counter rule turns +/// a CPU counter that did not advance into its estimator, but covers the +/// CPU class alone, so a GPU counter that did not advance (a run shorter +/// than one counter publish, or one that held) comes through as `HwShunt`, +/// measured 0 — a measured zero for a GPU that ran. It is not sealed. +fn accelerator_records( + machine: &sandbox_meter::Measurement, + cpu_estimate: sandbox_meter::DeviceEnergy, + gpu_sampled_uj: Option, +) -> Result, ProofError> { + use sandbox_meter::{DeviceEnergy, Provenance}; + let of = |class: DeviceClass| machine.devices.iter().find(|d| d.class == class).copied(); + let cpu = of(DeviceClass::Cpu).unwrap_or(cpu_estimate); + let gpu_read = of(DeviceClass::Gpu).filter(|g| g.estimated_uj > 0 && g.measured_uj != Some(0)); + let gpu = match (gpu_read, gpu_sampled_uj) { + (Some(g), _) => g, + (None, Some(uj)) => DeviceEnergy { + class: DeviceClass::Gpu, + measured_uj: None, + estimated_uj: uj, + provenance: Provenance::ModelBased, + }, + (None, None) => { + return Err(ProofError::Conformance( + "no GPU energy figure: no NVML counter that advanced over the run and no power sample while it ran".into(), + )) + } + }; + Ok(vec![cpu, gpu]) +} + /// Prove the **accelerator (GPU) fabric**: identify the GPU, run a real GPU -/// workload while sampling its power via `nvidia-smi`, and seal a cell whose -/// receipt carries a **separate `Gpu` energy record** and whose attestation -/// names the GPU (model + driver) — the heterogeneity wedge. GPU energy is -/// power × time, honestly tagged `ModelBased` (an integrated power sample, not a -/// hardware energy counter). +/// workload to completion, and seal a cell whose receipt carries a +/// **separate `Gpu` energy record** and whose attestation names the GPU +/// (model + driver) — the heterogeneity wedge. +/// +/// The energy is [`PowerMeter::detect`](sandbox_meter::PowerMeter::detect)'s +/// span over the workload's actual run, from just before it is spawned to +/// once it has exited: on Linux the RAPL package counters for `Cpu` and +/// NVML's total-energy counter for `Gpu`, each `HwShunt` and each only where +/// its liveness probe saw every counter it sums keep advancing (and, for the +/// GPU, where its counter advanced over the run: a zero is no reading). Both are +/// MACHINE-WIDE: the package counters hold every process's CPU energy over +/// the span, and NVML's the whole board's, whatever else ran on it — a +/// hardware reading of the host over the run, not of the workload alone. +/// Where a class has no live counter its record says so: `Cpu` is the +/// meter's wall-clock estimator (`Estimator`), and `Gpu` is `nvidia-smi`'s +/// power samples × the run's time (`ModelBased`: an integrated power sample, +/// not an energy counter); see [`accelerator_records`]. A workload that +/// exits unsuccessfully is not sealed. pub fn prove_accelerator( gpu_cmd: &str, gpu_args: Vec, - sample_secs: u64, cloud: &str, at_unix_us: u64, proof_key: &SigningKey, @@ -462,7 +558,7 @@ pub fn prove_accelerator( use ed25519_dalek::SigningKey as Sk; use sandbox_attest::{DeviceIdentity, Outcome}; use sandbox_capability::{ComputeGrant, Grants}; - use sandbox_meter::{DeviceEnergy, Provenance}; + use sandbox_meter::PowerMeter; use sandbox_runtime::{grants_content_id, unit_content_id, Host, RunReport}; let id = nvidia_smi("name,driver_version") @@ -484,46 +580,43 @@ pub fn prove_accelerator( return Err(ProofError::Conformance("in-code pack did not pass".into())); } - // Launch the GPU workload and sample power while it runs. - let mut child = std::process::Command::new(gpu_cmd) - .args(&gpu_args) - .spawn() - .map_err(|e| { - ProofError::Run(sandbox_runtime::ExecError::Unavailable(format!("spawn {gpu_cmd}: {e}")).into()) - })?; - let mut powers: Vec = Vec::new(); - for _ in 0..sample_secs.max(1) { - std::thread::sleep(std::time::Duration::from_secs(1)); - if let Some(p) = nvidia_smi("power.draw").and_then(|s| s.parse::().ok()) { - powers.push(p); - } + // The meter first: its liveness probes (about a second of CPU on this + // thread, the first time in a process) run before the span, never in it. + let mut meter = PowerMeter::detect(); + let sources = meter.sources().join(","); + let run = run_accelerator_workload(gpu_cmd, &gpu_args, &mut meter, || { + nvidia_smi("power.draw").and_then(|s| s.parse::().ok()) + }) + .map_err(|e| { + ProofError::Run(sandbox_runtime::ExecError::Unavailable(format!("spawn {gpu_cmd}: {e}")).into()) + })?; + if !run.status.success() { + return Err(ProofError::Run( + sandbox_runtime::ExecError::Unavailable(format!( + "GPU workload exited with {}; refusing to seal a proof for a run that failed", + run.status + )) + .into(), + )); } - let _ = child.wait(); - let avg_w = if powers.is_empty() { - 0.0 + let wall = run.machine.wall; + let avg_w = if run.powers.is_empty() { + None } else { - powers.iter().sum::() / powers.len() as f64 + Some(run.powers.iter().sum::() / run.powers.len() as f64) }; - let peak_w = powers.iter().cloned().fold(0.0_f64, f64::max); - // Energy = average power × window, in microjoules. Integer result; the float + // Sampled power × the run's time, µJ. Integer result; the float // arithmetic never enters a canonical form (SPEC §4). - let gpu_uj = (avg_w * sample_secs.max(1) as f64 * 1_000_000.0) as u64; + let gpu_sampled_uj = avg_w.map(|w| (w * wall.as_secs_f64() * 1_000_000.0) as u64); + let cpu_estimate = meter.estimate(wall).devices[0]; + let device_energy = accelerator_records(&run.machine, cpu_estimate, gpu_sampled_uj)?; + let described: Vec = device_energy + .iter() + .map(|d| format!("{} {} uj {}", d.class.wire_tag(), d.estimated_uj, d.provenance.label())) + .collect(); let run = RunReport { - device_energy: vec![ - DeviceEnergy { - class: DeviceClass::Cpu, - measured_uj: None, - estimated_uj: 1_000, - provenance: Provenance::Estimator, - }, - DeviceEnergy { - class: DeviceClass::Gpu, - measured_uj: None, - estimated_uj: gpu_uj, - provenance: Provenance::ModelBased, - }, - ], + device_energy, device_identity: vec![ DeviceIdentity { class: DeviceClass::Cpu, @@ -581,7 +674,11 @@ pub fn prove_accelerator( .map_err(|e| ProofError::Crypto(format!("attestation: {e}")))?; eprintln!( - " GPU: {gpu_name} (driver {gpu_driver}) — avg {avg_w:.1} W, peak {peak_w:.1} W over {sample_secs}s" + " GPU: {gpu_name} (driver {gpu_driver}) — {} over the workload's {:.1}s run [meter: {}; machine-wide]{}", + described.join(", "), + wall.as_secs_f64(), + if sources.is_empty() { "estimator" } else { &sources }, + avg_w.map(|w| format!(", sampled GPU power avg {w:.1} W")).unwrap_or_default(), ); let hardware: Vec = sealed.receipt.devices.iter().map(|d| d.class).collect(); let attestation_id = sealed @@ -1007,6 +1104,13 @@ pub struct LocalInferenceInputs { /// consults a [`WeightHashCache`] keyed on `(size, mtime)` so a multi-GiB /// model is not re-hashed each run — see that type for the trade-off. pub hash_cache: Option, + /// The operator's declaration that the engine hands no work to a process + /// outside its own process tree: no system service, no daemon, no + /// server. No reader of the tree can see such work (it is charged to the + /// process that does it), so only the operator, who knows the engine, + /// can say there is none. Without it (the default) the engine tree's + /// reading is never sealed; see [`prove_local`]. + pub engine_self_contained: bool, } /// Stream a BLAKE3 over a file without loading it into memory — weights are @@ -1142,6 +1246,319 @@ fn resolve_weight_hash( Ok((blake3, HashSource::Fresh)) } +/// One run of a local engine to completion, metered two ways over the same +/// run: machine-wide, and on the engine's own process tree where this host +/// can read it. +struct EngineRun { + status: std::process::ExitStatus, + /// The machine-wide meter's span ([`sandbox_meter::PowerMeter::detect`]), + /// opened before the engine was spawned and closed after it was reaped: + /// every process's energy on the counters it reads, or its estimator. + machine: sandbox_meter::Measurement, + /// The engine's own process tree ([`sandbox_meter::TreeMeter`]), from + /// before its first instruction (it is spawned suspended, and the start + /// walk read before it is resumed) to after its exit (waited for without + /// reaping, so its exited record is still readable). `None` where there + /// is no tree meter: off macOS, or the per-process counter is not live. + tree: Option>, +} + +/// Run `engine args` to completion under `meter`, and, on macOS, under a +/// tree meter rooted at the engine. `on_suspended` and `on_exited` are +/// called with the engine's pid before it is resumed and after it has +/// exited, before it is reaped: the tests read their oracle there, and +/// production passes nothing that does anything. A hook that panics unwinds +/// with the engine killed and reaped ([`EngineGuard`]). +/// +/// The engine inherits this process's environment and standard streams, as +/// `Command::status` gives it, with `SIGPIPE` at its default disposition and +/// no signal blocked, as Rust's own spawn leaves a child. +#[cfg(target_os = "macos")] +fn run_engine( + engine: &str, + args: &[String], + meter: &mut sandbox_meter::PowerMeter, + on_suspended: &mut dyn FnMut(u32), + on_exited: &mut dyn FnMut(u32), +) -> std::io::Result { + use std::ffi::CString; + use std::io::{Error, ErrorKind}; + use std::os::unix::process::ExitStatusExt; + + let nul = |_| Error::new(ErrorKind::InvalidInput, "an engine argument holds a NUL byte"); + let prog = CString::new(engine).map_err(nul)?; + let argv_c: Vec = std::iter::once(engine) + .chain(args.iter().map(String::as_str)) + .map(CString::new) + .collect::>() + .map_err(nul)?; + let mut argv: Vec<*mut libc::c_char> = argv_c.iter().map(|c| c.as_ptr() as *mut libc::c_char).collect(); + argv.push(std::ptr::null_mut()); + + // The per-process counter's liveness probe burns about 300 ms of CPU on + // this thread the first time it runs in a process: paid here, before + // either span opens, never inside the machine-wide one. + let _ = sandbox_meter::process_energy_status(); + + let span = meter.start(); + let pid = spawn_suspended(&prog, &argv)?; + // From here until it is reaped, an unwind (a hook that panics) kills and + // reaps the engine rather than leave it suspended forever. + let mut guard = EngineGuard { pid, armed: true }; + let tree = u32::try_from(pid).ok().and_then(sandbox_meter::TreeMeter::for_process); + let tree_start = tree.as_ref().map(sandbox_meter::TreeMeter::start); + on_suspended(pid as u32); + // SAFETY: `pid` is this process's child, not yet reaped. + unsafe { libc::kill(pid, libc::SIGCONT) }; + let exited = wait_exited(pid); + if exited.is_ok() { + on_exited(pid as u32); + } + let reading = match (tree, tree_start, &exited) { + (Some(t), Some(s), Ok(())) => Some(t.stop(s)), + _ => None, + }; + let status = reap(pid).map(std::process::ExitStatus::from_raw); + guard.armed = false; + let machine = span.stop(meter); + Ok(EngineRun { status: status?, machine, tree: reading }) +} + +/// The engine, while [`run_engine`] has not reaped it: dropped armed — an +/// unwind out of a hook, or the meter — it is killed and reaped. A hook that +/// panics while the engine is suspended would otherwise leave it suspended +/// forever, and orphaned once this process exits. +#[cfg(target_os = "macos")] +struct EngineGuard { + pid: libc::pid_t, + armed: bool, +} + +#[cfg(target_os = "macos")] +impl Drop for EngineGuard { + fn drop(&mut self) { + if self.armed { + // SAFETY: `pid` is this process's child, not yet reaped. SIGKILL + // ends a stopped process as well as a running one. + unsafe { libc::kill(self.pid, libc::SIGKILL) }; + let _ = reap(self.pid); + } + } +} + +/// `posix_spawnp` the engine suspended (`POSIX_SPAWN_START_SUSPENDED`): it +/// exists, so its tree meter can pin it and read it, and has run none of +/// its own code; `SIGCONT` resumes it. +#[cfg(target_os = "macos")] +fn spawn_suspended(prog: &std::ffi::CStr, argv: &[*mut libc::c_char]) -> std::io::Result { + use std::io::Error; + extern "C" { + // The process environment, for posix_spawnp, as sandbox-meter's + // attributed runner binds it. + fn _NSGetEnviron() -> *mut *const *mut libc::c_char; + } + // SAFETY: each call is given initialised, writable structures of the + // types it takes; `attr` is destroyed on every path after its init. + unsafe { + let mut attr: libc::posix_spawnattr_t = std::mem::zeroed(); + let rc = libc::posix_spawnattr_init(&mut attr); + if rc != 0 { + return Err(Error::from_raw_os_error(rc)); + } + let mut none: libc::sigset_t = std::mem::zeroed(); + libc::sigemptyset(&mut none); + let mut pipe: libc::sigset_t = std::mem::zeroed(); + libc::sigemptyset(&mut pipe); + libc::sigaddset(&mut pipe, libc::SIGPIPE); + let flags = libc::POSIX_SPAWN_START_SUSPENDED | libc::POSIX_SPAWN_SETSIGMASK | libc::POSIX_SPAWN_SETSIGDEF; + let mut rc = libc::posix_spawnattr_setflags(&mut attr, flags as libc::c_short); + if rc == 0 { + rc = libc::posix_spawnattr_setsigmask(&mut attr, &none); + } + if rc == 0 { + rc = libc::posix_spawnattr_setsigdefault(&mut attr, &pipe); + } + let mut pid: libc::pid_t = 0; + if rc == 0 { + rc = libc::posix_spawnp(&mut pid, prog.as_ptr(), std::ptr::null(), &attr, argv.as_ptr(), *_NSGetEnviron()); + } + libc::posix_spawnattr_destroy(&mut attr); + if rc != 0 { + return Err(Error::from_raw_os_error(rc)); + } + Ok(pid) + } +} + +/// Wait for child `pid` to exit WITHOUT reaping it (`waitid` with +/// `WNOWAIT`): an exited child stays readable until it is reaped. +#[cfg(target_os = "macos")] +fn wait_exited(pid: libc::pid_t) -> std::io::Result<()> { + loop { + // SAFETY: an all-zero `siginfo_t` is a valid out-parameter. + let mut info: libc::siginfo_t = unsafe { std::mem::zeroed() }; + // SAFETY: `info` is writable for the call; `pid` is our child. + let rc = unsafe { libc::waitid(libc::P_PID, pid as libc::id_t, &mut info, libc::WEXITED | libc::WNOWAIT) }; + if rc == 0 { + return Ok(()); + } + let e = std::io::Error::last_os_error(); + if e.raw_os_error() != Some(libc::EINTR) { + return Err(e); + } + } +} + +/// Reap child `pid`: its wait status. +#[cfg(target_os = "macos")] +fn reap(pid: libc::pid_t) -> std::io::Result { + loop { + let mut status: libc::c_int = 0; + // SAFETY: `status` is writable; `pid` is our child. + let rc = unsafe { libc::waitpid(pid, &mut status, 0) }; + if rc == pid { + return Ok(status); + } + let e = std::io::Error::last_os_error(); + if rc >= 0 || e.raw_os_error() != Some(libc::EINTR) { + return Err(e); + } + } +} + +/// Off macOS there is no per-process energy counter, so no tree meter: the +/// engine runs as `Command::status` runs it, inside the machine-wide span. +#[cfg(not(target_os = "macos"))] +fn run_engine( + engine: &str, + args: &[String], + meter: &mut sandbox_meter::PowerMeter, + _on_suspended: &mut dyn FnMut(u32), + _on_exited: &mut dyn FnMut(u32), +) -> std::io::Result { + let span = meter.start(); + let status = std::process::Command::new(engine).args(args).status(); + let machine = span.stop(meter); + Ok(EngineRun { status: status?, machine, tree: None }) +} + +/// Why a local proof's cell carries the machine-wide meter's records rather +/// than a reading of the engine's own process tree. A run can have several. +#[derive(Debug, Clone, PartialEq, Eq)] +enum MachineBecause { + /// No tree meter on this host: off macOS, or the per-process counter is + /// not live. + NoTreeMeter, + /// The tree span gave no reading. + NoReading(sandbox_meter::TreeError), + /// The reading saw part of the tree's energy missing. A run-to-completion + /// engine always has one: its root exits inside the span, and an exiting + /// thread's last time on a core is never folded into its record. + Gaps(Vec), + /// The operator has not declared that the engine hands no work to a + /// process outside its tree ([`LocalInferenceInputs::engine_self_contained`]), + /// which no reader of the tree can see. + NotDeclaredSelfContained, +} + +/// The device records a local proof seals, from the run's two readings +/// ([`prove_local`] says why this is the rule): one `Cpu` record, `HwShunt`, +/// of the engine tree's own CPU energy, only for a reading with no gap at +/// all of an engine its operator declared self-contained; otherwise the +/// machine-wide meter's records verbatim, with every reason. Pure, so its +/// tests drive every case without a process. +fn local_records( + tree: Option<&Result>, + self_contained: bool, + machine: &sandbox_meter::Measurement, +) -> (Vec, Vec) { + use sandbox_meter::{DeviceEnergy, Provenance}; + let mut because: Vec = Vec::new(); + match tree { + Some(Ok(r)) if r.is_whole() => {} + Some(Ok(r)) => because.push(MachineBecause::Gaps(r.gaps.clone())), + Some(Err(e)) => because.push(MachineBecause::NoReading(e.clone())), + None => because.push(MachineBecause::NoTreeMeter), + } + if !self_contained { + because.push(MachineBecause::NotDeclaredSelfContained); + } + match tree { + Some(Ok(r)) if because.is_empty() => ( + vec![DeviceEnergy { + class: DeviceClass::Cpu, + measured_uj: Some(r.cpu_uj), + estimated_uj: r.cpu_uj, + provenance: Provenance::HwShunt, + }], + because, + ), + _ => (machine.devices.clone(), because), + } +} + +/// The accelerator use the engine tree's reading shows positive evidence +/// of, for a class the records to be sealed carry no record of — each as +/// the reading's gap says it. Empty when there is none. Evidence: GPU time +/// the tree's clients recorded ([`TreeGap::Gpu`](sandbox_meter::TreeGap::Gpu)), +/// a member holding a GPU client whose time is unknown (`GpuUnknown` with a +/// pid), and Neural Engine model memory held in-process (`NeuralEngine`, the +/// `Npu` class). A GPU reader that could not read (`GpuUnknown` with no pid) +/// is no evidence either way. Pure, so its tests drive every case. +/// +/// [`prove_local`] refuses to seal when this is not empty: SPEC §6.2 gives +/// each accelerator class used a record of its own and forbids folding its +/// energy into the `Cpu` record or omitting it — which is what sealing the +/// estimator's single `Cpu` record for the run would do. +fn unrecorded_accelerator_use( + tree: Option<&Result>, + records: &[sandbox_meter::DeviceEnergy], +) -> Vec { + use sandbox_meter::TreeGap; + let Some(Ok(reading)) = tree else { return Vec::new() }; + let recorded = |class: DeviceClass| records.iter().any(|d| d.class == class); + reading + .gaps + .iter() + .filter(|g| match g { + TreeGap::Gpu { .. } | TreeGap::GpuUnknown { pid: Some(_) } => !recorded(DeviceClass::Gpu), + TreeGap::NeuralEngine { .. } => !recorded(DeviceClass::Npu), + _ => false, + }) + .map(ToString::to_string) + .collect() +} + +/// The engine tree's reading, for the CLI line: what it read and what +/// became of it. Never a figure the cell carries unless `sealed`. +fn tree_line( + tree: Option<&Result>, + because: &[MachineBecause], +) -> String { + let fate = if because.is_empty() { + "sealed".to_string() + } else { + let why: Vec = because + .iter() + .map(|b| match b { + MachineBecause::NoTreeMeter => "no tree meter on this host".to_string(), + MachineBecause::NoReading(e) => e.to_string(), + MachineBecause::Gaps(gaps) => gaps.iter().map(ToString::to_string).collect::>().join("; "), + MachineBecause::NotDeclaredSelfContained => "engine not declared self-contained".to_string(), + }) + .collect(); + format!("not sealed: {}", why.join("; ")) + }; + match tree { + Some(Ok(r)) => format!( + "engine tree: {:.3} mJ of CPU over {} process(es) [{fate}]", + r.cpu_nj as f64 / 1e6, + r.processes + ), + _ => format!("engine tree: no reading [{fate}]"), + } +} + /// Prove **local, offline inference**: run a local engine against local weights /// with no network grant, meter it on this host's own energy counters, and seal /// a cell. @@ -1171,6 +1588,65 @@ fn resolve_weight_hash( /// by the best source the platform offers — a live counter, else the /// estimator — and labelled by the span's own records. /// +/// **Which records the cell carries.** The run is metered two ways at once. +/// Machine-wide, by [`PowerMeter::detect`](sandbox_meter::PowerMeter::detect) +/// over the whole run: every process's energy on the counters it reads (so +/// it includes this host's other work), or its wall-clock estimator where no +/// counter is live — on macOS 27.0.1 every Apple Silicon host checked. And, +/// where this host's kernel counts each process's CPU energy live (macOS), +/// on the engine's own process tree ([`sandbox_meter::TreeMeter`]): the +/// engine is spawned suspended, the tree's start walk read before it runs +/// its first instruction, and its exit waited for without reaping. The +/// span therefore holds the tree from the engine's first instruction to its +/// exit. Not its creation: the suspended engine already carries a little +/// energy at the start walk (the kernel's work making it, charged to it +/// before it is suspended; well under a millijoule in the tests), which is +/// the reading's baseline and so not in it. What the run's last moments +/// lack is said by the `Exited` gap below. +/// +/// The receipt (SPEC §6) has one record per device class used, each a +/// figure for the class with a provenance, and no field to say a figure +/// covers part of the class's energy; `HwShunt` with a measured figure +/// claims the hardware reading OF THE CLASS (§6.3), and accelerator energy +/// may be neither omitted nor folded into the `Cpu` record (§6.2). So the +/// tree's reading is sealed — as the run's only record, `Cpu`, `HwShunt` — +/// only when it is a reading of everything the run spent: no gap of any kind +/// ([`TreeReading::is_whole`](sandbox_meter::TreeReading::is_whole): no GPU +/// client and no Neural Engine memory in the tree, which leaves `Cpu` the +/// only class used; every member read and quiet; nothing reaped or exited +/// unread), AND the operator has declared that the engine delegates nothing +/// outside its tree ([`LocalInferenceInputs::engine_self_contained`]), which +/// no reader of the tree can see. Otherwise the cell carries the +/// machine-wide meter's records verbatim, as it always has. Two +/// alternatives are not honest under the spec: a `Cpu` `HwShunt` record of +/// a partial tree reading claims the class's whole energy; and a tree `Cpu` +/// record beside the estimator for "the rest" cannot be built, because the +/// estimator's figure is one wall-clock figure for the whole run, not a +/// figure for the GPU or for what the tree missed, and it is a `Cpu` record +/// itself (a second `Cpu` record is a duplicate class). +/// +/// On this kernel a run-to-completion engine is never read whole: its root +/// exits inside the span, and an exiting thread's last time on a core is +/// never folded into its energy record ([`TreeGap::Exited`](sandbox_meter::TreeGap::Exited)), +/// so the reading is short of the run by an unknown amount. The cell +/// therefore carries the machine-wide records; the tree's reading, and why +/// it was not sealed, are printed beside the proof. +/// +/// **Accelerators.** Where the tree reading shows positive evidence that +/// the engine used an accelerator — GPU time, a member holding a GPU client +/// whose time is unknown, Neural Engine model memory — and the records to +/// be sealed carry no record of that class, the proof is REFUSED +/// (`unrecorded_accelerator_use`): §6.2 forbids folding accelerator +/// energy into the `Cpu` record or omitting it, and the estimator's single +/// `Cpu` record for the run (every Apple Silicon host checked on macOS +/// 27.0.1) would do exactly that, as [`prove_accelerator`] refuses a run +/// with no GPU figure. The evidence is only what the reading holds: a GPU +/// client loses its recorded time about 2 ms after its process exits and +/// is gone soon after, so a run-to-completion Metal engine's GPU use has +/// usually left no trace by the stop walk (its `Exited` gap says its GPU +/// time is unknown), and a run whose evidence is gone is sealed on the +/// machine-wide records as before. +/// /// The engine is supplied by the operator and driven as a subprocess, exactly /// as [`prove_accelerator`] drives a GPU workload. That keeps the sandbox /// standard free of any dependency on a particular inference runtime — this @@ -1231,21 +1707,28 @@ pub fn prove_local( } // (3) Meter this host's own counters across the engine's execution. The - // engine is a subprocess, so the meter is `detect()`'s machine-wide one, - // never `detect_in_process()`: this process's own energy counter does not - // cover a child process, and would read the proof waiting. + // engine is a subprocess, so the machine meter is `detect()`'s + // machine-wide one, never `detect_in_process()`: this process's own + // energy counter does not cover a child process, and would read the + // proof waiting. Beside it, the engine's own process tree where this + // host can read it; `local_records` decides which the cell carries. let mut meter = PowerMeter::detect(); - let sources = meter.sources().join(","); - let (status, measurement) = meter.measure(|| { - std::process::Command::new(&inputs.engine) - .args(&inputs.args) - .status() - }); - let status = status.map_err(|e| { + let engine_run = run_engine(&inputs.engine, &inputs.args, &mut meter, &mut |_| {}, &mut |_| {}).map_err(|e| { ProofError::Run( sandbox_runtime::ExecError::Unavailable(format!("spawn {}: {e}", inputs.engine)).into(), ) })?; + let status = engine_run.status; + let (records, machine_because) = + local_records(engine_run.tree.as_ref(), inputs.engine_self_contained, &engine_run.machine); + let unrecorded = unrecorded_accelerator_use(engine_run.tree.as_ref(), &records); + let from_tree = machine_because.is_empty(); + let sources = if from_tree { "process-tree-energy".to_string() } else { meter.sources().join(",") }; + let measurement = sandbox_meter::Measurement { + devices: records, + wall: engine_run.machine.wall, + source: if from_tree { "process-tree-energy" } else { engine_run.machine.source }, + }; if !status.success() { return Err(ProofError::Run( sandbox_runtime::ExecError::Unavailable(format!( @@ -1254,10 +1737,18 @@ pub fn prove_local( .into(), )); } + if !unrecorded.is_empty() { + eprintln!(" {}", tree_line(engine_run.tree.as_ref(), &machine_because)); + return Err(ProofError::Conformance(format!( + "refusing to seal: the engine used an accelerator the records have no class for ({}); \ + SPEC §6.2 forbids folding its energy into the Cpu record or omitting it", + unrecorded.join("; ") + ))); + } - // Device records pass through verbatim — the meter's provenance is the - // proof's provenance. Re-tagging here is exactly the lie the ladder exists - // to prevent. + // Device records pass through verbatim — the chosen meter's provenance + // is the proof's provenance. Re-tagging here is exactly the lie the + // ladder exists to prevent. // One identity per metered class — SPEC §7.2 requires every device that // reports energy to be named. The meter decides which classes it can see // (on Apple Silicon that is CPU, GPU and ANE together), so the identity @@ -1330,6 +1821,7 @@ pub fn prove_local( measurement.avg_watts(), sources, ); + eprintln!(" {}", tree_line(engine_run.tree.as_ref(), &machine_because)); let hardware: Vec = sealed.receipt.devices.iter().map(|d| d.class).collect(); let attestation_id = sealed @@ -1532,6 +2024,7 @@ mod tests { args: vec![], weights: weights.to_string(), hash_cache: None, + engine_self_contained: false, } } @@ -1672,4 +2165,515 @@ mod tests { assert!(g.network.outbound.is_empty()); assert!(!g.network.inbound); } + + // ── which records a local proof seals ──────────────────────────── + + use sandbox_meter::{DeviceEnergy, Measurement, Provenance, SpanEnd, TreeError, TreeGap, TreeReading}; + + /// A reading of the engine's tree, as the meter would give it. + fn tree_reading(cpu_nj: u64, gaps: Vec) -> TreeReading { + TreeReading { + cpu_uj: cpu_nj.div_ceil(1_000), + cpu_nj, + processes: 1, + pids: vec![4242], + wall: std::time::Duration::from_millis(900), + gaps, + } + } + + /// The machine-wide meter's span on an estimator-only host: one `Cpu` + /// record, wall × TDP. + fn machine_estimate() -> Measurement { + Measurement { + devices: vec![DeviceEnergy { + class: DeviceClass::Cpu, + measured_uj: None, + estimated_uj: 18_000_000, + provenance: Provenance::Estimator, + }], + wall: std::time::Duration::from_millis(900), + source: "estimator", + } + } + + /// The one case the engine's own reading is sealed: no gap of any kind, + /// and the operator's declaration. It is the run's only record — `Cpu`, + /// `HwShunt`, its measured figure the reading rounded up to the µJ — and + /// a receipt builds from it. + #[test] + fn a_whole_reading_of_a_declared_engine_is_sealed_as_its_only_record() { + let r: Result = Ok(tree_reading(2_000_000_001, Vec::new())); + let (records, because) = local_records(Some(&r), true, &machine_estimate()); + assert!(because.is_empty(), "{because:?}"); + assert_eq!( + records, + vec![DeviceEnergy { + class: DeviceClass::Cpu, + measured_uj: Some(2_000_001), + estimated_uj: 2_000_001, + provenance: Provenance::HwShunt, + }] + ); + let receipt = sandbox_meter::Receipt::build(ContentId::of_bytes(b"u"), Tier::S0, records, 1, [0; 8]); + assert!(receipt.is_ok(), "{receipt:?}"); + } + + /// Every gap keeps the machine-wide records, declared or not: the + /// receipt has no coverage field, so a partial reading sealed `HwShunt` + /// would claim the class's whole energy. The root's exit, which every + /// run-to-completion engine has, is among them; so are the GPU and + /// Neural Engine gaps, whose classes a `Cpu` record cannot stand for. + #[test] + fn a_reading_with_any_gap_keeps_the_machine_records() { + let gaps = [ + TreeGap::Exited { pid: 4242 }, + TreeGap::ReapedDescendant { pid: 4242, cpu: std::time::Duration::from_millis(40) }, + TreeGap::Unsettled { pid: 4242, end: SpanEnd::Start }, + TreeGap::Unsettled { pid: 4242, end: SpanEnd::Stop }, + TreeGap::Changing { end: SpanEnd::Stop }, + TreeGap::Unreadable { pid: 77, errno: 1, end: SpanEnd::Stop }, + TreeGap::Unlisted { pid: 77, errno: 1, end: SpanEnd::Start }, + TreeGap::PredatesSpan { pid: 77 }, + TreeGap::Gone { pid: 77 }, + TreeGap::EnergyWentBack { pid: 4242 }, + TreeGap::Gpu { ns: 9_000_000 }, + TreeGap::GpuUnknown { pid: None }, + TreeGap::GpuUnknown { pid: Some(4242) }, + TreeGap::NeuralEngine { pid: 4242, bytes: 1 << 24 }, + ]; + for gap in gaps { + let r: Result = Ok(tree_reading(2_000_000_000, vec![gap.clone()])); + let (records, because) = local_records(Some(&r), true, &machine_estimate()); + assert_eq!(records, machine_estimate().devices, "{gap:?}: the partial reading was sealed"); + assert_eq!(because, vec![MachineBecause::Gaps(vec![gap])]); + } + } + + /// No declaration, no reading, no meter: the machine-wide records, with + /// every reason. + #[test] + fn without_a_whole_declared_reading_the_machine_records_stand() { + let whole: Result = Ok(tree_reading(2_000_000_000, Vec::new())); + let (records, because) = local_records(Some(&whole), false, &machine_estimate()); + assert_eq!(records, machine_estimate().devices); + assert_eq!(because, vec![MachineBecause::NotDeclaredSelfContained]); + + let gone: Result = Err(TreeError::RootGone { pid: 4242 }); + let (records, because) = local_records(Some(&gone), true, &machine_estimate()); + assert_eq!(records, machine_estimate().devices); + assert_eq!(because, vec![MachineBecause::NoReading(TreeError::RootGone { pid: 4242 })]); + + let (records, because) = local_records(None, false, &machine_estimate()); + assert_eq!(records, machine_estimate().devices); + assert_eq!(because, vec![MachineBecause::NoTreeMeter, MachineBecause::NotDeclaredSelfContained]); + } + + /// Positive evidence in the tree reading that the engine used an + /// accelerator — GPU time its clients recorded, a member holding a GPU + /// client whose time is unknown, Neural Engine model memory — with no + /// record of that class among the records to be sealed: the proof is + /// refused (SPEC §6.2: accelerator energy is neither folded into `Cpu` + /// nor omitted), as the accelerator proof refuses a run with no GPU + /// figure. The estimator's single `Cpu` record is exactly that fold. + /// A GPU reader that could not read (`GpuUnknown { pid: None }`) is no + /// evidence of use, and a machine meter with its own `Gpu` and `Npu` + /// records (IOReport live) carries each class. + #[test] + fn accelerator_use_with_no_record_of_its_class_is_refused() { + let with = |gaps: Vec| -> Result { + Ok(tree_reading(2_000_000_000, [vec![TreeGap::Exited { pid: 4242 }], gaps].concat())) + }; + let cpu_only = machine_estimate().devices; + for gap in [ + TreeGap::Gpu { ns: 9_000_000 }, + TreeGap::GpuUnknown { pid: Some(4242) }, + TreeGap::NeuralEngine { pid: 4242, bytes: 1 << 24 }, + ] { + let r = with(vec![gap.clone()]); + let why = unrecorded_accelerator_use(Some(&r), &cpu_only); + assert_eq!(why, vec![gap.to_string()], "{gap:?} was folded into the Cpu record"); + } + let both = with(vec![TreeGap::Gpu { ns: 1 }, TreeGap::NeuralEngine { pid: 4242, bytes: 1 }]); + assert_eq!(unrecorded_accelerator_use(Some(&both), &cpu_only).len(), 2); + + // No evidence: nothing to refuse. + for r in [with(Vec::new()), with(vec![TreeGap::GpuUnknown { pid: None }]), Err(TreeError::RootGone { pid: 4242 })] { + assert!(unrecorded_accelerator_use(Some(&r), &cpu_only).is_empty(), "{r:?}"); + } + assert!(unrecorded_accelerator_use(None, &cpu_only).is_empty()); + + // Each class carried by a record of its own: nothing folded. + let ioreport = vec![ + record(DeviceClass::Cpu, Some(9_000_000), 9_000_000, Provenance::HwShunt), + record(DeviceClass::Gpu, Some(700_000), 700_000, Provenance::HwShunt), + record(DeviceClass::Npu, Some(0), 0, Provenance::HwShunt), + ]; + assert!(unrecorded_accelerator_use(Some(&both), &ioreport).is_empty()); + let gpu_only = vec![ioreport[0], ioreport[1]]; + assert_eq!( + unrecorded_accelerator_use(Some(&both), &gpu_only), + vec![TreeGap::NeuralEngine { pid: 4242, bytes: 1 }.to_string()] + ); + } + + /// The engine's own CPU energy, on a real run-to-completion engine + /// (awk burning a fixed loop: CPU only, one process), read on its tree + /// from suspended to exited. The oracle shares no code with the meter: + /// the engine's `proc_pid_rusage(pid, RUSAGE_INFO_V6)` into a raw + /// buffer, energy at byte 336, read while it is suspended (it has run + /// none of its own code, and nothing moves its count) and once it has + /// exited (its record is final until it is reaped). The reading must + /// equal the oracle's advance to the nanojoule, and name the root's exit + /// as its one gap — so even with the operator's declaration the cell + /// keeps the machine-wide records. Each run is logged (`local engine + /// tree:`). + #[cfg(all(target_os = "macos", target_arch = "aarch64"))] + #[test] + fn a_cpu_only_engine_is_read_on_its_own_tree_and_its_exit_keeps_it_unsealed() { + if sandbox_meter::process_energy_status() != sandbox_meter::CounterStatus::Live { + let mut meter = sandbox_meter::PowerMeter::detect(); + let run = run_engine("/usr/bin/true", &[], &mut meter, &mut |_| {}, &mut |_| {}).expect("spawn"); + assert!(run.tree.is_none(), "a tree reading with no live counter"); + return; + } + let mut meter = sandbox_meter::PowerMeter::detect(); + let script = "BEGIN { for (i = 0; i < 4000000; i++) x += i; exit (x < 0) }".to_string(); + for rep in 0..3 { + let (mut at_start, mut at_exit) = (None, None); + let run = run_engine( + "awk", + std::slice::from_ref(&script), + &mut meter, + &mut |pid| at_start = Some((pid, oracle_energy_nj(pid))), + &mut |pid| at_exit = Some((pid, oracle_energy_nj(pid))), + ) + .expect("spawn awk"); + assert!(run.status.success(), "{:?}", run.status); + let (pid, start) = at_start.expect("the suspended hook ran"); + let (_, end) = at_exit.expect("the exited hook ran"); + let oracle = end - start; + let r = run.tree.clone().expect("a tree meter on a live counter").expect("a reading"); + let (records, because) = local_records(run.tree.as_ref(), true, &run.machine); + eprintln!( + "local engine tree: awk rep {rep}: {} nJ over {:?}, oracle {oracle} nJ (suspended {start}), gaps {:?}; sealed {records:?}", + r.cpu_nj, r.pids, r.gaps + ); + assert!(start < 1_000_000, "the suspended engine ran its own code before the span: {start} nJ"); + assert_eq!(r.pids, vec![pid], "awk is one process"); + assert_eq!(r.cpu_nj, oracle, "the reading is not the oracle's advance from suspended to exited"); + assert_eq!(r.gaps, vec![TreeGap::Exited { pid }], "a CPU-only engine's only gap is its exit"); + assert_eq!(because, vec![MachineBecause::Gaps(vec![TreeGap::Exited { pid }])]); + assert_eq!(records, run.machine.devices, "the exited engine's partial reading was sealed"); + } + } + + /// A hook that panics must not leave the engine behind: before the + /// engine is resumed it would stay suspended forever (and orphaned when + /// this process exits); after it exits, an unreaped zombie. Either way + /// the engine is killed and reaped on the unwind. The test reaps + /// whatever it finds left before it asserts, so a failure leaves nothing. + #[cfg(target_os = "macos")] + #[test] + fn a_panicking_hook_never_leaves_the_engine_behind() { + type Hook<'a> = Box; + let mut meter = sandbox_meter::PowerMeter::detect(); + for at_exit in [false, true] { + let seen = std::cell::Cell::new(0u32); + let unwound = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + let (args, mut suspended, mut exited): (Vec, Hook, Hook) = if at_exit { + (vec![], Box::new(|p| seen.set(p)), Box::new(|_| panic!("the exited hook panicked"))) + } else { + (vec!["30".into()], Box::new(|p| { + seen.set(p); + panic!("the suspended hook panicked") + }), Box::new(|_| {})) + }; + let engine = if at_exit { "/usr/bin/true" } else { "/bin/sleep" }; + run_engine(engine, &args, &mut meter, &mut *suspended, &mut *exited) + })); + assert!(unwound.is_err(), "the hook's panic did not unwind"); + let pid = seen.get() as libc::pid_t; + assert!(pid > 0, "the suspended hook saw no pid"); + let mut status = 0; + // SAFETY: `status` is writable; WNOHANG never blocks. + let left = unsafe { libc::waitpid(pid, &mut status, libc::WNOHANG) }; + if left == 0 { + // SAFETY: `pid` is this test's child, still unreaped. + unsafe { + libc::kill(pid, libc::SIGKILL); + libc::waitpid(pid, &mut status, 0); + } + } + assert_eq!(left, -1, "at_exit={at_exit}: the engine was left behind (waitpid {left}: 0 running or suspended, the pid an unreaped zombie)"); + } + } + + /// An engine that runs its work in a descendant it reaps (`sh` forking + /// `awk` and waiting for it): the descendant's energy is in no counter, + /// and the reading names it, so the machine-wide records stand. + #[cfg(all(target_os = "macos", target_arch = "aarch64"))] + #[test] + fn an_engine_that_reaps_its_worker_is_read_with_the_worker_named_missing() { + if sandbox_meter::process_energy_status() != sandbox_meter::CounterStatus::Live { + return; + } + let mut meter = sandbox_meter::PowerMeter::detect(); + let forked = "awk 'BEGIN { for (i = 0; i < 4000000; i++) x += i; exit (x < 0) }'; true".to_string(); + let run = run_engine("sh", &["-c".to_string(), forked], &mut meter, &mut |_| {}, &mut |_| {}).expect("spawn sh"); + assert!(run.status.success()); + let r = run.tree.clone().expect("a tree meter").expect("a reading"); + eprintln!("local engine tree: sh+awk: {} nJ over {:?}, gaps {:?}", r.cpu_nj, r.pids, r.gaps); + assert!( + r.gaps.iter().any(|g| matches!(g, TreeGap::ReapedDescendant { .. })), + "the reaped awk is not named: {:?}", + r.gaps + ); + let (records, because) = local_records(run.tree.as_ref(), true, &run.machine); + assert_eq!(records, run.machine.devices); + assert!(matches!(because.as_slice(), [MachineBecause::Gaps(_)]), "{because:?}"); + } + + /// The whole local proof on a real engine: the cell seals and verifies, + /// and its receipt carries the machine-wide meter's classes (on this + /// fleet's macOS hosts, the estimator's single `Cpu` record), not the + /// engine tree's partial reading. + #[cfg(target_os = "macos")] + #[test] + fn a_local_proof_on_a_real_engine_seals_the_machine_records() { + let dir = unique_dir("local-real-engine"); + let w = dir.join("weights.bin"); + std::fs::write(&w, b"weights on this disk").unwrap(); + let inputs = LocalInferenceInputs { + engine: "awk".to_string(), + args: vec!["BEGIN { for (i = 0; i < 2000000; i++) x += i; exit (x < 0) }".to_string()], + weights: w.to_string_lossy().into_owned(), + hash_cache: None, + engine_self_contained: true, + }; + let sk = SigningKey::from_bytes(&[9u8; 32]); + let cell = prove_local(&inputs, "local", 0, &sk).expect("a local proof on awk"); + assert!(verify(&cell)); + let classes = sandbox_meter::PowerMeter::detect().estimate(std::time::Duration::from_millis(1)).devices; + if !sandbox_meter::PowerMeter::detect().is_hardware() { + assert_eq!(cell.cell.hardware, classes.iter().map(|d| d.class).collect::>()); + } + assert!(cell.cell.total_estimated_uj > 0); + } + + // ── the accelerator proof's records ────────────────────────────── + + fn record(class: DeviceClass, measured: Option, estimated: u64, provenance: Provenance) -> DeviceEnergy { + DeviceEnergy { class, measured_uj: measured, estimated_uj: estimated, provenance } + } + + fn span_of(devices: Vec) -> Measurement { + Measurement { devices, wall: std::time::Duration::from_secs(3), source: "composite" } + } + + /// The meter's wall-clock estimator for a 3 s run at 20 W. + fn cpu_estimate() -> DeviceEnergy { + record(DeviceClass::Cpu, None, 60_000_000, Provenance::Estimator) + } + + /// Each class's record is the best figure this host gave for it, as it + /// is: RAPL and NVML readings pass through; a class with no live counter + /// gets the estimator (`Cpu`) or the sampled power × the run's time + /// (`Gpu`, `ModelBased`); with no GPU figure at all the proof is refused. + /// Every record set builds a receipt. + #[test] + fn the_accelerator_records_are_each_class_best_figure_as_it_is() { + let rapl = record(DeviceClass::Cpu, Some(41_000_000), 41_000_000, Provenance::HwShunt); + let nvml = record(DeviceClass::Gpu, Some(19_000_000), 19_000_000, Provenance::HwShunt); + let cases = [ + // RAPL and NVML both live: both readings, verbatim. + (span_of(vec![rapl, nvml]), Some(30_000_000), vec![rapl, nvml]), + // NVML alone (RAPL root-only): the CPU is the estimator's. + (span_of(vec![nvml]), Some(30_000_000), vec![cpu_estimate(), nvml]), + // RAPL alone (NVML implausible or absent): the GPU is sampled. + ( + span_of(vec![rapl]), + Some(30_000_000), + vec![rapl, record(DeviceClass::Gpu, None, 30_000_000, Provenance::ModelBased)], + ), + // The span came back estimated (no counter, or the CPU counter + // held): the meter's own estimator record, and the samples. + ( + span_of(vec![cpu_estimate()]), + Some(30_000_000), + vec![cpu_estimate(), record(DeviceClass::Gpu, None, 30_000_000, Provenance::ModelBased)], + ), + ]; + for (span, sampled, want) in cases { + let got = accelerator_records(&span, cpu_estimate(), sampled).expect("records"); + assert_eq!(got, want, "{span:?}"); + let receipt = sandbox_meter::Receipt::build(ContentId::of_bytes(b"u"), Tier::S0, got, 1, [0; 8]); + assert!(receipt.is_ok(), "{receipt:?}"); + } + // No NVML reading and no sample: nothing to seal for the GPU. + let r = accelerator_records(&span_of(vec![rapl]), cpu_estimate(), None); + assert!(matches!(r, Err(ProofError::Conformance(_))), "{r:?}"); + } + + /// A GPU counter that did not advance over the run is no reading of the + /// GPU's energy over it — a workload shorter than one counter publish, + /// or a counter that held — and the meter's held-counter rule covers the + /// CPU class alone, so it passes through as `HwShunt`, measured 0. It is + /// never sealed: the samples stand in for it (`ModelBased`), and with no + /// sample the proof is refused, as with no GPU counter at all. + #[test] + fn a_gpu_counter_that_held_is_no_reading() { + let rapl = record(DeviceClass::Cpu, Some(41_000_000), 41_000_000, Provenance::HwShunt); + let held = record(DeviceClass::Gpu, Some(0), 0, Provenance::HwShunt); + let sampled = record(DeviceClass::Gpu, None, 30_000_000, Provenance::ModelBased); + for span in [span_of(vec![rapl, held]), span_of(vec![held])] { + let cpu = if span.devices.len() == 2 { rapl } else { cpu_estimate() }; + let got = accelerator_records(&span, cpu_estimate(), Some(30_000_000)).expect("records"); + assert_eq!(got, vec![cpu, sampled], "a held GPU counter was sealed: {span:?}"); + let r = accelerator_records(&span, cpu_estimate(), None); + assert!(matches!(r, Err(ProofError::Conformance(_))), "{r:?}"); + } + } + + /// The span is the workload's own run, however long it is (not a fixed + /// sampling window), and the GPU's power is sampled while it runs. + #[cfg(unix)] + #[test] + fn the_accelerator_span_is_the_workloads_actual_run() { + let mut meter = sandbox_meter::PowerMeter::detect(); + let mut samples = 0; + let t = std::time::Instant::now(); + let run = run_accelerator_workload("sh", &["-c".to_string(), "sleep 1.6".to_string()], &mut meter, || { + samples += 1; + Some(12.5) + }) + .expect("spawn sh"); + let outer = t.elapsed(); + eprintln!("accelerator span: sleep 1.6: wall {:?} (outer {outer:?}), {samples} sample(s), {:?}", run.machine.wall, run.machine.devices); + assert!(run.status.success()); + assert!(run.machine.wall >= std::time::Duration::from_millis(1600), "{:?}", run.machine.wall); + assert!(run.machine.wall <= outer); + assert!(samples >= 1 && run.powers.len() == samples, "sampled {samples}, kept {}", run.powers.len()); + assert!(run.powers.iter().all(|&w| w == 12.5)); + let failed = run_accelerator_workload("sh", &["-c".to_string(), "exit 3".to_string()], &mut meter, || None).expect("spawn sh"); + assert!(!failed.status.success(), "a failing workload's status is kept for the refusal"); + } + + /// On Linux, the host's own counters over a real run of a couple of + /// seconds: RAPL's package counters for `Cpu` where every package counter + /// is live, read against the package zones' `energy_uj` read here, around + /// the call, wrap included (the span is inside that window, so its figure + /// is at most the oracle's and, the window being the span plus a spawn, + /// most of it); NVML for `Gpu` where its counter is live and advanced + /// over the run, else `nvidia-smi`'s power × the run's time. Where neither GPU figure exists + /// (no GPU, as in a CI container) the proof is refused. The test says + /// which branches it took (`accelerator span:`). + #[cfg(target_os = "linux")] + #[test] + fn on_linux_the_accelerator_records_read_the_hosts_counters_over_the_run() { + use sandbox_meter::{nvml_status, rapl_status, CounterStatus}; + let mut meter = sandbox_meter::PowerMeter::detect(); + let (rapl, nvml) = (rapl_status(), nvml_status()); + let before = oracle_package_uj(); + let script = "BEGIN { for (i = 0; i < 100000000; i++) x += i; exit (x < 0) }".to_string(); + let run = run_accelerator_workload("awk", std::slice::from_ref(&script), &mut meter, || { + nvidia_smi("power.draw").and_then(|s| s.parse::().ok()) + }) + .expect("spawn awk"); + let after = oracle_package_uj(); + assert!(run.status.success()); + let wall = run.machine.wall; + eprintln!( + "accelerator span: rapl {rapl:?} nvml {nvml:?} sources {:?} wall {wall:?} samples {:?} machine {:?}", + meter.sources(), + run.powers, + run.machine.devices + ); + + // The CPU: the machine span's own `Cpu` record, against the oracle. + let cpu = run.machine.devices.iter().find(|d| d.class == DeviceClass::Cpu).copied(); + match (rapl, cpu) { + (CounterStatus::Live, Some(c)) if c.provenance == Provenance::HwShunt => { + let span = c.measured_uj.expect("HwShunt carries its reading"); + let (b, a) = (before.expect("package zones"), after.expect("package zones")); + let outer = a.0.iter().zip(&b.0).zip(&a.1).map(|((x, y), range)| (x + range - y) % range).sum::(); + eprintln!( + "accelerator span: RAPL package {span} uj over the run, oracle around the call {outer} uj, ratio {:.3}", + span as f64 / outer as f64 + ); + assert!(span <= outer, "the span read more than the window around it: {span} > {outer}"); + assert!(span * 2 >= outer, "the span read under half the window around it: {span} vs {outer}"); + } + // A live RAPL whose span came back estimated (its counter held) + // is the meter's rule, not this test's; anything else must not + // be a hardware reading. + (CounterStatus::Live, _) => {} + (_, c) => assert!(c.is_none_or(|c| c.provenance != Provenance::HwShunt), "{c:?} without live RAPL"), + } + + // The records, both classes. + let sampled = (!run.powers.is_empty()) + .then(|| (run.powers.iter().sum::() / run.powers.len() as f64 * wall.as_secs_f64() * 1e6) as u64); + let records = match accelerator_records(&run.machine, meter.estimate(wall).devices[0], sampled) { + Ok(r) => r, + Err(e) => { + let nvml_read = run + .machine + .devices + .iter() + .any(|d| d.class == DeviceClass::Gpu && d.measured_uj.is_some_and(|uj| uj > 0)); + assert!(!nvml_read && run.powers.is_empty(), "refused with a GPU figure: {e}"); + eprintln!("accelerator span: no GPU figure on this host, refused: {e}"); + return; + } + }; + eprintln!("accelerator span: sealed {records:?}"); + assert_eq!(records[0], cpu.unwrap_or(meter.estimate(wall).devices[0])); + let gpu = records[1]; + assert_eq!(gpu.class, DeviceClass::Gpu); + let nvml_read = run + .machine + .devices + .iter() + .any(|d| d.class == DeviceClass::Gpu && d.measured_uj.is_some_and(|uj| uj > 0)); + match nvml { + CounterStatus::Live if nvml_read => assert_eq!(gpu.provenance, Provenance::HwShunt, "{gpu:?}"), + _ => assert_eq!( + (gpu.provenance, gpu.measured_uj, Some(gpu.estimated_uj)), + (Provenance::ModelBased, None, sampled), + "the GPU's power samples × the run's time" + ), + } + } + + /// Each RAPL `package-` zone's `energy_uj` and `max_energy_range_uj`, + /// read from sysfs here; `None` if there is none or one is unreadable. + #[cfg(target_os = "linux")] + fn oracle_package_uj() -> Option<(Vec, Vec)> { + let mut zones: Vec = std::fs::read_dir("/sys/class/powercap") + .ok()? + .filter_map(|e| e.ok().map(|e| e.path())) + .filter(|p| { + std::fs::read_to_string(p.join("name")).is_ok_and(|n| n.trim().starts_with("package-")) + && !p.to_string_lossy().contains("mmio") + }) + .collect(); + zones.sort(); + let read = |p: &std::path::Path, f: &str| std::fs::read_to_string(p.join(f)).ok()?.trim().parse::().ok(); + let energy: Option> = zones.iter().map(|z| read(z, "energy_uj")).collect(); + let range: Option> = zones.iter().map(|z| read(z, "max_energy_range_uj")).collect(); + let (energy, range) = (energy?, range?); + (!energy.is_empty()).then_some((energy, range)) + } + + /// The engine's `ri_energy_nj`: `proc_pid_rusage(pid, 6)` into a raw + /// buffer larger than `rusage_info_v6`, the u64 at byte 336. + #[cfg(all(target_os = "macos", target_arch = "aarch64"))] + fn oracle_energy_nj(pid: u32) -> u64 { + let mut buf = [0u64; 64]; + // SAFETY: `buf` is writable and larger than `rusage_info_v6`. + let rc = unsafe { libc::proc_pid_rusage(pid as i32, 6, buf.as_mut_ptr() as *mut libc::rusage_info_t) }; + assert_eq!(rc, 0, "oracle read of pid {pid}"); + buf[336 / 8] + } } diff --git a/sandbox/sandbox-rs/crates/sandbox-proof/src/main.rs b/sandbox/sandbox-rs/crates/sandbox-proof/src/main.rs index 610ab8050..bee7b8ad6 100644 --- 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(),