Complete the eventb-checker EB001–EB019 rule catalogue in rossi validate#50
Closed
evdenis wants to merge 8 commits into
Closed
Complete the eventb-checker EB001–EB019 rule catalogue in rossi validate#50evdenis wants to merge 8 commits into
evdenis wants to merge 8 commits into
Conversation
Precedence, associativity and operator-compatibility tables move out of the pretty-printer into a new `rossi::op_info` module, a single source of truth that the well-definedness renderer will also consume.
The static checker now retains the enriched ASTs and source positions of every clause: CheckedMachine carries its MachineRecord and answers chain_parameters / event_env, axiom and event records keep a source index, and PredicateCheck / ActionCheck expose the typed formula. A new ScModel bundles the per-component records and is returned by the new build_with_model wrapper; the existing build is unchanged. Adds TypeEnv::remove for shadow masking and a reserved relational-atom helper shared with type inference.
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.
A standalone proofs module streams the Rodin .bpr/.bpo/.bps files and reports undischarged obligations (EB015), broken proof scripts (EB016) and unparseable proof files (EB017), plus an obligation summary. The scan runs automatically whenever an archive or directory ships proof files. validate surfaces the findings and a Proofs: ... summary line, the SARIF output carries the summary as run properties, and the proof_oracle_diff gate compares the counts and finding multiset against eventb-checker. Reading the archive once now feeds the recovery parse, the build and the proof scan from the same bytes.
Loose `.eventb` text the Camille grammar rejects as a whole was reported as EB005 (a formula-level error). It is now EB004, matching the eventb-checker catalogue; EB005 stays for formula attributes inside Rodin XML that the grammar rejects. rule_for_parse_error now maps a MalformedAttribute envelope to EB005 so the distinction holds end to end.
This was referenced Jun 14, 2026
Contributor
Author
|
Superseded by a split into four reviewable PRs:
Closing in favor of those. |
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
Completes
rossi validate's parity with theeventb-checkerEB001–EB019rule catalogue. The remaining rules are implemented and surfaced:
port of Rodin's WD calculus, shown under the new
--show-infoflag(hidden by default, like
eventb-checker).unparseable) scraped from
.bpr/.bpo/.bps, auto-enabled when prooffiles are present and carried into the SARIF summary.
EB005, now match
eventb-checker(EB005 stays for rejected formulaattributes).
Commits (reviewable in order)
Refactors first, then features bottom-up — each commit builds and passes
the full pre-commit gate (fmt, clippy
-D warnings, doc-D warnings,tests) on its own:
refactor(rossi)— centralize operator metadata in a sharedop_infomodule (single source of truth for precedence / associativity / compat).
refactor(sc)— expose the typed model viabuild_with_model(
ScModel, enriched records, source positions) for post-check passes.feat(wd)— port Rodin's well-definedness calculus as a standalonemodule, with no rule coupling.
feat(wd)— drive the calculus over the typed model to emit EB010.test(wd)— pin the WD output to theeventb-checkeroracle.feat(validate)— surface EB010 via--show-info.feat(validate)— EB015–EB017 proof status from Rodin proof files.fix(validate)— relabel whole-file Camille parse errors EB004.Testing
Three
#[ignore]oracle gates compare rossi againsteventb-checker1.6over a corpus of Rodin archives (set
EVENTB_CORPUS_DIR; skipped when unset):type_oracle_diff— type inference ✓wd_oracle_diff— WD messages byte-identical ✓proof_oracle_diff— proof status ✓All green, and the full pre-commit gate is clean at every commit.