VCR-RA-010: const-remat eligibility DERIVED from the stream, the hint only gates (#242) - #920
Merged
Merged
Conversation
…y gates (#242) scry's singleton-interval signal is promoted from a dev-dependency test to an allocator input — under the rule the release is named for: verified or refused, never believed. A wrong --proven-safe verdict opens a memory-safety hole; a wrong const-remat verdict re-emits the WRONG VALUE, i.e. a miscompile. So this seam follows the --wcet-hints shape, not the trusted-fact shape: plan_const_remat walks the FINAL ARM stream and admits a reload only where it can see the constant definition reaching the spill with no intervening write. The hint can only SHRINK that set. Conservative by construction and reported as such: unclassifiable ops clear all state, and reloads_seen/windows_closed accompany every site count. Mutation-checked — and the mutation paid for itself by exposing that the red-first test passed for the wrong reason (the gate's value comparison was doing the rejecting, not the stream check). Fixed; it is now potent. 7/7 tests, clippy clean, flag-off so bytes are unchanged. Refs #242
The original push landed during the GitHub Actions major outage, so no workflow ever started for this branch — zero checks, not failing checks.
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wave-2 lane L2 of the v0.55 "scry seam" hub. Flag-off; bytes unchanged.
scry's interval domain identifies locals with a singleton interval
[c, c]— provably constant values the allocator can rematerialize at the use instead of spilling and reloading. That signal was a dev-dependency test (scry_const_remat_signal.rs); this promotes it to an allocator input.The design question
A wrong
--proven-safeverdict (#901) elides a bounds guard — a memory-safety hole. A wrong const-remat verdict would re-emit the wrong value — a miscompile. So this seam follows the--wcet-hintsshape, not the trusted-fact shape:plan_const_rematwalks the final stream and admits a reload only where it can itself see the constant definition reaching the spill with no intervening write.MOVTover an unknown low half stays unknown; a non-constant store retires the slot; a branch/call/label closes the window.Conservatism is reported, not hidden
Any op the walk cannot classify clears all state — a large amount of missed opportunity, deliberate for a first increment, because an op wrongly treated as harmless could hide a write to the slot and turn a stale constant into a miscompile.
reloads_seenandwindows_closedaccompany every site count so a small number reads as narrow window, never as small opportunity. Widening the safe set op-by-op is the named follow-up.Mutation earned its keep
Mutating the walk to treat an unknown register as the constant 0 exposed that the red-first test
lying_hint_yields_no_candidatespassed for the wrong reason: it offered hint value999while a broken walk invents0, so the gate's value comparison did the rejecting, not the stream check. Fixed to run the gate OPEN so only the stream can reject — it now goes red under that mutation, as do two other tests.7/7 tests, clippy clean,
cargo fmtclean.Refs #242