Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science f1b662078b energy tests: the load-sensitive tick floor in proof-cascade and sandbox-meter ... #166 fixed this class of defect in `eoc-meter` and `jouleclaw-energy`: an energy-probe test asserting a floor on thread CPU per tick, which the host's scheduler controls, failing on the dev Mac because the dev Mac is also the macOS runner. The same code exists in two more crates, and the same assertion with it. CI surfaced `proof-cascade` by failing an unrelated PR; sweeping for the pattern found `sandbox-meter` as well, rather than waiting for another round. A tick spins until the thread's CPU clock advances 25 ms **or** a 500 ms wall cap passes. Both copies carried a comment asserting the opposite — "the tick burns thread CPU time, so host load does not shorten it; only its wall-clock cap can" — a sentence containing its own refutation, since the cap is how load shortens a tick. The two outcomes that matter are not separable by time: a spin the host starved into the cap and a tick that simply slept both show a long wall span against little CPU. I tried a per-turn CPU floor first, reasoning that a turn is fixed work so starvation lowers turns-per-second rather than the cost of a turn. Measuring refuted it: a turn that sleeps 1 ms costs 13.3-15.8 µs of thread CPU against a real turn's 2.13-2.92 µs, because a blocking body's context switch is charged to the thread. Even the direction was wrong. So each tick reports what it did. `spin_tick` / `spin_for` return a `TickOutcome` — the CPU it saw itself burn, and how many turns of the spin loop it ran — and each probe collects one per tick, alongside the interval's wall span beside its CPU span. Per tick: the loop ran at all (a tick that never span did not burn CPU, at any load), and the tick stopped for one of its two stated reasons rather than early. The gaps measured by the tests' own clocks still bound it from above and keep CPU under wall. - **proof-cascade**: three load-sensitive sites — `assert_sampling`'s per-interval floor, an aggregate floor over a whole scripted call, and a per-interval floor in the live-rail test. `ProbeRun` gains `interval_wall` and the per-tick outcomes; `burn_thread_cpu` reports the CPU it was already computing. - **sandbox-meter**: the per-interval `PROBE_TICK / 2` floor. This crate already had `assert_tick` using the either-condition rule for the tick itself, so the interval check now matches the crate's own convention — and both are stronger for the spin count, since that rule alone admits a tick that slept through its cap. `TickOutcome` becomes public because it already appears in a public signature: `RaplPackages::live_in` and `counter_liveness` take a tick that returns it, so `sandbox-exec-microvm` has to name it and build one. Where a scripted tick stands in for the burn — fake powercap trees, the MSR fakes, the hardware test's own oracle — it reports a turn, with a comment saying that this is the test declaring a real spin ran and not a figure chosen to clear a threshold. The hardware test's tick keeps using `oracle::burn`, so the oracle stays independent of what it checks. Three doc comments asserting "a tick burns a full tick however loaded the machine is" are corrected in place; leaving that beside a fixed assertion would reinvite the mistake. Two call sites are `cfg(target_os = "linux")` and invisible to every run on this host: `sandbox-meter/tests/rapl_hardware.rs`, which CI's jetson-hub job caught, and `probe::counter_liveness_tick`, reached on the Linux side through `MsrRaplMeter::host`, which `cargo check --target aarch64-unknown-linux-gnu --all-targets` caught. That check is a weak oracle — it runs nothing — but it is the right shape for a type mismatch in code the host never compiles. `CARGO_FEATURE_NO_NEON=1` is needed, or blake3's build script wants Linux C headers. The whole sandbox workspace cannot cross-check (`zstd-sys` needs a real cross compiler), so instead I confirmed that nothing outside these crates references the changed entry points, which makes the per-crate checks exhaustive for callers. Falsified in both crates: a tick that sleeps instead of spinning, and a tick skipped entirely. One sleep falsification first looked like a pass and was a compile error — checked, not assumed. In proof-cascade a tick cut short of both stopping conditions is caught too. Verified: proof-rs 139 passed, sandbox-rs 324 passed, and the five touched crates check clean for aarch64-unknown-linux-gnu. The two clippy warnings in proof-cascade are in untouched code, the same pair that predates the change in eoc-meter — these files are copies of one another, which is why the defect was in four places. Co-Authored-By: Claude Opus 5 <[email protected]>		2026-10-07 10:03:30 -04:00
..
crates	energy tests: the load-sensitive tick floor in proof-cascade and sandbox-meter	2026-10-07 10:03:30 -04:00
Cargo.lock	proof: an absent solver yields Unproved, never a fabricated proof	2026-08-29 05:06:17 -04:00
Cargo.toml	msrv: raise the rust-version floor to 1.97 across the workspaces	2026-07-23 00:17:08 -04:00