feat(validate): EB010 non-trivial well-definedness conditions#52
Open
evdenis wants to merge 4 commits into
Open
feat(validate): EB010 non-trivial well-definedness conditions#52evdenis wants to merge 4 commits into
evdenis wants to merge 4 commits into
Conversation
Add the calculus eventb-checker borrows from Rodin to decide whether a formula is well-defined, as a self-contained rossi-build module: - computer: the L-operator deriving a formula's WD lemma - builder: FormulaBuilder smart constructors keeping the lemma in normal form - improve: the WDImprover simplifier dropping trivial/subsumed conjuncts - normal: binder flattening and capture-aware binder renaming - render: a Formula#toString renderer, byte-identical to Rodin The module is the calculus only and is not yet wired to any checker; its inline unit tests exercise each layer directly.
Drive the calculus over a checked project: for every formula the static check kept, compute its WD lemma, simplify it, and report the survivors as INFO diagnostics carrying RuleId::WellDefinedness (EB010), the message rendered byte-identically to eventb-checker. Raw component ASTs supply the formulas (the lemma embeds verbatim source fragments); the typed model supplies the environments and decides which clauses the check kept, paired by source position rather than label. Registers EB010 in the rule catalogue.
Add the wd_oracle_diff gate: build each corpus model, run the WD pipeline, and assert the rendered findings are byte-identical to eventb-checker's EB010 output. The gate is #[ignore] and skips unless EVENTB_CORPUS_DIR and the oracle CLI are available. Factor the corpus plumbing it shares with the other oracle gates (eventb_checker_bin, oracle_available, collect_zips) into tests/common.
Wire the WD pipeline into `rossi validate`: build the typed model once, run wd:: over it, and fold the EB010 findings into the results. They are INFO-severity and, like eventb-checker, dropped from every output format unless the new --show-info flag is set; the WD pass is skipped entirely when its rows would be discarded. Text output gains an INFO glyph.
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
1 participant
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.
What
A faithful port of Rodin's well-definedness calculus, surfaced as INFO findings
(EB010) through a new
--show-infoflag onrossi validate.For every formula the static check accepted, rossi computes its WD lemma
(Rodin's L-operator), simplifies it (Rodin's
WDImprover), and reports thesurvivors as INFO diagnostics with the message
Well-definedness condition: <lemma>— byte-identical to eventb-checker, whichprints Rodin's
Predicate#toString(). Coverage matches eventb-checker: contextaxioms/theorems; machine invariants/theorems/variant; event guards/actions/
witnesses (including INITIALISATION).
Default output is unchanged: WD findings are INFO-severity, hidden unless
--show-infois passed, and never affect the exit code.Commits
feat(wd): port Rodin's well-definedness calculusfeat(wd): emit EB010 well-definedness findings from the typed modeltest(wd): pin well-definedness output to the eventb-checker oraclefeat(validate): surface EB010 well-definedness via --show-infoTesting
wd_oracle_diffgate: WD messages are byte-identical to eventb-checker 1.6across the model corpus.
cli_testcovers default-hidden /--show-info/ JSONrule_id: EB010.Part of splitting #50 into reviewable PRs.