Skip to content

fix(cli): capture the explain and html source once - #950

Open
rizumita wants to merge 2 commits into
mainfrom
fix/932-explain-html-single-read
Open

fix(cli): capture the explain and html source once#950
rizumita wants to merge 2 commits into
mainfrom
fix/932-explain-html-single-read

Conversation

@rizumita

Copy link
Copy Markdown
Collaborator

Second slice of #932, after #943 did check and db check.

Problem

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. #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 explain that means weakening_candidates,
reachable_counterfactuals, invariant_violation_explanation,
invariant_counterfactuals, and readable_implements_text as well as the command
body.

Scope is explain and html only. ledger and analyze stay for the third
slice; #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:

  • explainbyte-for-byte identical.
  • html — differs only in verification.cost's elapsed_s and
    solver.check_elapsed_s. Those are wall-clock measurements of the run that
    produced 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_reports keeps that exclusion
from 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 a
    second source is opened. Unix-gated by necessity; a #[cfg(not(unix))] marker test
    keeps a passing non-Unix run from being mistaken for their evidence.
  • main.rs exit_status_tests — deterministic controls with no #[cfg(unix)],
    so Windows carries the same guarantee.

Calibration: the explain entry re-read mutation failed explain's FIFO detector
with a second open while all three sibling controls, including html's, stayed
green — the locality that makes it a detector for that route rather than for the
shared renderer. Restore proven by SHA-256 05bf08…f8c9e with an empty git 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 html mutation made
both html and explain react, so it could not be cited as either route's
detector; it was replaced with an entry-only mutation. analyze shares paths
between its plain and --ai-review modes, so the third slice is more exposed to
this, not less.

Two out-of-scope edits survived that switch. run_replay was left calling
load_model_from_source(path, source) with no source in scope — it would not
compile — and run_scenarios_mode_from_source had been reverted to a path read,
which would have regressed already-shipped scenarios behaviour. Proving the
mutated 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 to
is 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) and clippy exit=101
(needless_borrow ×2 at 8545:60 and 9034:60) — caught before committing, which
is 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 a
different commit:

gate exit
cargo fmt --all -- --check 0
cargo clippy --workspace --all-targets --locked -- -D warnings 0
cargo test -p fslc-rust --locked 0 (143 suites)

cargo test --workspace --locked returned 0 before the rebase; the rebase only
dropped the commit that #943 had squashed, so the workspace result is carried
forward rather than re-run.

rust/fslc/tests/issue_868_result_option_verdict_census.rs is updated for the
renamed 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.

`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.
…#932 fragment

`changelog.d/README.md` forbids reusing an (id, category) pair, and #943 already
landed `932-...fixed.md`. This slice fixes the same defect in two more commands
rather than producing a separate notable effect, so it belongs in that one bullet.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant