proof-cascade: the raw-reader pin counts the subscriptions it hands the reader (a laptop registers IOReport channels as it runs) #543

Merged

dcharlot merged 1 commit from proof/ioreport-same-subscription into main 2026-10-29 21:09:22 -04:00

Conversation 0 Commits 1 Files changed 1 +91 -48

dcharlot commented 2026-10-29 20:29:33 -04:00

Owner

Copy link

The macOS energy job went red on #541, in a crate #541 does not touch: meter::macos_ioreport::tests::the_raw_reader_reads_the_subscription_it_is_given_every_time, on the new M5 Max laptop runner (tx-mbp-m5max-48).

What failed. The pin compared the raw reader's listing of two subscriptions with the oracle's count of a third subscription, the oracle's own, opened first. An all-channel subscription holds the channels registered when it was opened, and a laptop registers more as it runs. On that runner the oracle's subscription held 12,862 channels, and open()'s, opened a moment later, held 13,014. The reader listed 13,014 on all three reads: it was right, and the pin was measuring the wrong subscription. The Energy Model group (364) matched every time. The Studio's channel set holds still, which is why the pin never failed there.

The change.

• The oracle's reader is now a function of any live subscription (oracle_read), with its own sampling and parsing, as before. OracleSub::read calls it.
• The pin counts, with that function, the two subscriptions it hands the reader: the probe's group subscription and the all-channel one. The reader must list as many channels as the oracle reads in the very subscription it was handed, on every read.
• A reader that hands back an earlier read still fails, as before.
• New checks: the group subscription holds only the group; the all-channel one holds the whole group; the group is the smaller.

No production code changes. The only change is to the test module's oracle.

Tests

• Studio (M3 Ultra): cargo test -p proof-cascade -- --nocapture, plus the job's clippy line -p proof-cascade -p proof-solvers -- -D warnings.
• M5 Max laptop runner: the same test line.

Falsification, on the M5 Max laptop runner, running only this pin:

Run	What happened	Result
New pin, 15 times	Passed every time. On run 8 the channel set moved inside the test: the oracle's own subscription held 12,862 channels, and the two subscriptions opened a moment later held 12,710. The reader listed 12,710 on all three reads, matching the subscriptions it was handed.	pass
Old pin (main 7473e6d7e), 15 times	The set held at 12,710 on every run, so these runs passed. The failure is intermittent: CI hit the transition (12,862 against 13,014), and run 8 above shows it recurring.	pass
Mutation: the all-channel read is handed the group's subscription	Listed (364, 364) against the oracle's (364, 12,710). Reverted afterwards.	refused (panicked at meter.rs:4523)

Totals seen on this one host: 12,710, 12,862 and 13,014. The Studio held 15,055 throughout.

🤖 Generated with Claude Code

The macOS energy job went red on #541, in a crate #541 does not touch: `meter::macos_ioreport::tests::the_raw_reader_reads_the_subscription_it_is_given_every_time`, on the new M5 Max laptop runner (`tx-mbp-m5max-48`). **What failed.** The pin compared the raw reader's listing of two subscriptions with the oracle's count of a third subscription, the oracle's own, opened first. An all-channel subscription holds the channels registered when it was opened, and a laptop registers more as it runs. On that runner the oracle's subscription held 12,862 channels, and `open()`'s, opened a moment later, held 13,014. The reader listed 13,014 on all three reads: it was right, and the pin was measuring the wrong subscription. The Energy Model group (364) matched every time. The Studio's channel set holds still, which is why the pin never failed there. **The change.** - The oracle's reader is now a function of any live subscription (`oracle_read`), with its own sampling and parsing, as before. `OracleSub::read` calls it. - The pin counts, with that function, the two subscriptions it hands the reader: the probe's group subscription and the all-channel one. The reader must list as many channels as the oracle reads in the very subscription it was handed, on every read. - A reader that hands back an earlier read still fails, as before. - New checks: the group subscription holds only the group; the all-channel one holds the whole group; the group is the smaller. No production code changes. The only change is to the test module's oracle. **Tests** - Studio (M3 Ultra): `cargo test -p proof-cascade -- --nocapture`, plus the job's clippy line `-p proof-cascade -p proof-solvers -- -D warnings`. - M5 Max laptop runner: the same test line. **Falsification**, on the M5 Max laptop runner, running only this pin: | Run | What happened | Result | |---|---|---| | New pin, 15 times | Passed every time. On run 8 the channel set moved inside the test: the oracle's own subscription held 12,862 channels, and the two subscriptions opened a moment later held 12,710. The reader listed 12,710 on all three reads, matching the subscriptions it was handed. | pass | | Old pin (main 7473e6d7e), 15 times | The set held at 12,710 on every run, so these runs passed. The failure is intermittent: CI hit the transition (12,862 against 13,014), and run 8 above shows it recurring. | pass | | Mutation: the all-channel read is handed the group's subscription | Listed (364, 364) against the oracle's (364, 12,710). Reverted afterwards. | refused (panicked at meter.rs:4523) | Totals seen on this one host: 12,710, 12,862 and 13,014. The Studio held 15,055 throughout. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-10-29 20:29:33 -04:00

proof-cascade: the raw-reader pin counts the subscriptions it hands over ... 546b13287a

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

dcharlot merged commit d630ad2055 into main 2026-10-29 21:09:22 -04:00

dcharlot referenced this pull request from a commit 2026-10-29 21:09:24 -04:00

Merge pull request 'proof-cascade: the raw-reader pin counts the subscriptions it hands the reader (a laptop registers IOReport channels as it runs)' (#543) from proof/ioreport-same-subscription into main

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

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

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!543

No description provided.