open-standards/proof/proof-rs
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Transaction Science 974a8ebece
All checks were successful
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 10s
energy meters on real hardware / sink decode table · per-task energy and the GPU rail on macOS (pull_request) Successful in 2m16s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 2m26s
standards workspaces build + test / joulecontract-rs (joulecontract/joulecontract-rs, joulecontract-rs, linux-arm64, true) (pull_request) Successful in 1m0s
standards workspaces build + test / proof-rs (proof/conformance/v1/joulespec.toml, proof-conformance, proof/proof-rs, proof-rs, linux, true) (pull_request) Successful in 2m24s
energy meters on real hardware / RAPL and NVML on jetson-hub (pull_request) Successful in 36s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 6m4s
energy meters on real hardware / sink decode table · RAPL on jetson-hub (NVML surveyed) (pull_request) Successful in 2m25s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 10m58s
proof-cascade: RAPL MSR domains are per die on Intel, per package on AMD
Linux scopes Intel's RAPL energy-status MSRs per die: its RAPL PMU treats
the package counter as package-scope only on AMD and Hygon
(rapl_pkg_pmu_is_pkg_scope(), arch/x86/events/rapl.c: "AMD/HYGON platforms
have a per-PKG package energy counter", "CLX-AP is multi-die and its RAPL
MSRs are die-scope"), and its powercap driver names a zone
package-<p>-die-<d> where the MSRs are not package-scope and a package holds
more than one die (intel_rapl_common.c). The MSR fallback grouped CPUs by
physical_package_id alone, so on a multi-die Intel package it read one die
and missed the rest: an under-count, the unsafe direction at a ceiling.

MSR fallback: on Intel family 6 a domain is (physical_package_id, die_id),
die 0 where the kernel lists no die_id; on AMD Zen and Hygon it stays the
package, whatever die_id says. Each domain is read on its lowest-numbered
CPU and is a package zone of its own, indexed in (package, die) order, so
each die is a rail of its own in the liveness rule and every die is summed.
All-or-nothing, the zero unit, the wrap and powercap preferred are as
before. (MsrPackage is now MsrDomain.)

Powercap: is_package_name also accepts package-<digits>-die-<digits>, and
nothing looser, so a multi-die host's per-die zones are its packages:
powercap lists a package (the MSRs are not read), and both die zones are
summed. Before, such a host listed no package and fell to the MSRs, as root
only.

The RAPL hardware test's oracle follows the same rules with its own code.

Tests (fake files): two Intel packages of two dies each, four domains each
read on its own die's first CPU and summed; an AMD package whose CPUs carry
two die_ids, one domain; an Intel host with no die_id files, per package; a
two-die powercap tree summing both die zones and not psys; and the name rule
(package-0-die-0 yes; package-0-die-, package-0-die, package--die-0,
package-0-die-x, package-0-core-0 no). proof-cascade and proof-cli tests pass
on Linux, proof-cascade on macOS (with its ioreport liveness grep); clippy
is clean with -D warnings on Linux (proof-cascade, proof-cli) and macOS
(proof-cascade, proof-solvers).

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-11-04 21:19:50 -05:00
..
crates proof-cascade: RAPL MSR domains are per die on Intel, per package on AMD 2026-11-04 21:19:50 -05:00
Cargo.lock proof-solvers: read each resident z3 decision off z3's own process tree 2026-10-10 18:11:21 -04:00
Cargo.toml Cargo: no minimum-supported-version floor, because the policy is latest stable 2026-11-03 17:42:20 -05:00