open-standards/proof/proof-rs
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Transaction Science 546b13287a
All checks were successful
energy meters on real hardware / RAPL and NVML on jetson-hub (pull_request) Successful in 43s
energy meters on real hardware / sink decode table · RAPL on jetson-hub (NVML surveyed) (pull_request) Successful in 2m52s
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 11s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 3m1s
energy meters on real hardware / sink decode table · per-task energy and the GPU rail on macOS (pull_request) Successful in 2m18s
standards workspaces build + test / proof-rs (proof-conformance, proof/proof-rs, proof-rs, linux, true) (pull_request) Successful in 1m33s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 5m34s
standards workspaces build + test / joulecontract-rs (joulecontract/joulecontract-rs, joulecontract-rs, linux-arm64, true) (pull_request) Successful in 1m22s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 6m48s
proof-cascade: the raw-reader pin counts the subscriptions it hands over
The pin compared the raw reader's listing of two subscriptions with the
oracle's count of a third, its own, opened first. An all-channel
subscription holds the channels registered when it opened, and a laptop
registers more as it runs: on the M5 Max runner the oracle's held 12,862
and open()'s 13,014 a moment later, so the pin failed with the reader
listing the same 13,014 on every read. The reader was right; the pin
measured the wrong subscription.

The oracle's reader is now a function of any live subscription
(oracle_read), and the pin counts the probe's group subscription and the
all-channel one with it: the reader must list as many as the oracle reads
in the very subscription it was handed, every time. It also checks that
the group subscription holds only the group, that the all-channel one
holds the whole group, and that the group is the smaller.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-10-29 20:27:40 -04:00
..
crates proof-cascade: the raw-reader pin counts the subscriptions it hands over 2026-10-29 20:27:40 -04: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