fix(cli): capture the explain and html source once - #950
Open
rizumita wants to merge 2 commits into
Open
Conversation
`explain` and `html` read the root spec path more than once per invocation, so a single invocation could describe two different sources if the file changed between reads. Both now acquire the source at entry and pass that one snapshot through every downstream helper. FIFO controls fail if either command opens a second source; platform-neutral controls carry the same guarantee without `#[cfg(unix)]`, so Windows is covered too.
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.
Second slice of #932, after #943 did
checkanddb check.Problem
explainandhtmlread the root spec path more than once per invocation, so asingle invocation could describe two different sources if the file changed between
reads. #943's requirement recovery measured all six command families with a FIFO
whose second open is fatal; every one opened the root path twice. These are two of
the four remaining.
Contract change
Both commands acquire the source at entry and pass that one snapshot through every
downstream helper — for
explainthat meansweakening_candidates,reachable_counterfactuals,invariant_violation_explanation,invariant_counterfactuals, andreadable_implements_textas well as the commandbody.
Scope is
explainandhtmlonly.ledgerandanalyzestay for the thirdslice; #943's measurement table is their starting point, so that slice needs no
re-survey.
Output equivalence
Compared before and after in full, not field by field:
explain— byte-for-byte identical.html— differs only inverification.cost'selapsed_sandsolver.check_elapsed_s. Those are wall-clock measurements of the run thatproduced them; there is no value they could be compared against, which is why
they are excluded rather than "they may vary".
html_parity_timing_exclusions_are_present_in_both_reportskeeps that exclusionfrom going dead: it asserts both independently rendered reports actually contain
those two keys, so the exclusion fails if either key disappears. An exclusion of a
key that is no longer emitted weakens nothing while reading as deliberate.
Controls
Two independent families, so neither platform coverage nor determinism rests on the
other:
rust/fslc/tests/issue_932_check_snapshot.rs— FIFO controls(
explain_reads_one_fifo_snapshot,html_reads_one_fifo_snapshot) that fail if asecond source is opened. Unix-gated by necessity; a
#[cfg(not(unix))]marker testkeeps a passing non-Unix run from being mistaken for their evidence.
main.rsexit_status_tests— deterministic controls with no#[cfg(unix)],so Windows carries the same guarantee.
Calibration: the
explainentry re-read mutation failedexplain's FIFO detectorwith a second open while all three sibling controls, including
html's, stayedgreen — the locality that makes it a detector for that route rather than for the
shared renderer. Restore proven by SHA-256
05bf08…f8c9ewith an emptygit diff.The FIFO controls were run twice in one session after restore (4/4 both times),
since their verdict touches the filesystem.
Two things that went wrong, recorded because the third slice will hit them
A calibration mutation landed on a shared path. The first
htmlmutation madeboth
htmlandexplainreact, so it could not be cited as either route'sdetector; it was replaced with an entry-only mutation.
analyzeshares pathsbetween its plain and
--ai-reviewmodes, so the third slice is more exposed tothis, not less.
Two out-of-scope edits survived that switch.
run_replaywas left callingload_model_from_source(path, source)with nosourcein scope — it would notcompile — and
run_scenarios_mode_from_sourcehad been reverted to a path read,which would have regressed already-shipped
scenariosbehaviour. Proving themutated site's revert by hash did not cover either, because both sat elsewhere in
the same file. Walking every
@@header and naming which scope item it belongs tois what found them; the second one would otherwise have shipped.
Verification
Each gate's exit status was read from its log, not inferred from launching it. The
first round returned
fmt exit=1(main.rs:16926) andclippy exit=101(
needless_borrow×2 at8545:60and9034:60) — caught before committing, whichis the concrete form of the known failure where focused tests pass and workspace
clippy is skipped.
Re-measured after rebasing onto
93439c5, because the pre-rebase run measured adifferent commit:
cargo fmt --all -- --checkcargo clippy --workspace --all-targets --locked -- -D warningscargo test -p fslc-rust --lockedcargo test --workspace --lockedreturned 0 before the rebase; the rebase onlydropped the commit that
#943had squashed, so the workspace result is carriedforward rather than re-run.
rust/fslc/tests/issue_868_result_option_verdict_census.rsis updated for therenamed helpers and their new lines.
Fragment:
changelog.d/932-explain-html-single-snapshot.fixed.md.Authorship note for review: this branch was produced under my orchestration, so
please read it as an authored change rather than an independently reviewed one.