feat(validate): EB015–EB017 proof status from Rodin proof files#53
Open
evdenis wants to merge 1 commit into
Open
feat(validate): EB015–EB017 proof status from Rodin proof files#53evdenis wants to merge 1 commit into
evdenis wants to merge 1 commit into
Conversation
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.
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 standalone
proofsmodule that reads Rodin's proof artifacts(
.bpr/.bpo/.bps) and reports obligation status, auto-enabled wheneverproof files are present (no flag):
Confidence and broken state are read from the
.bpsstatus, matchingeventb-checker 1.6 (a broken-but-discharged obligation counts pending and
reports once, as EB016 — never also as EB015). SARIF output carries a proof
summary; the text summary prints a
Proofs: …line. Warnings keep the exitcode at 0.
Commits
feat(validate): EB015-EB017 proof status from Rodin proof filesTesting
proof_oracle_diffgate: proof status is byte-identical to eventb-checker 1.6across the model corpus (re-run green on this branch).
cli_testcovers the EB015/EB016 reporting and the proof-summary lines.Part of splitting #50 into reviewable PRs. Independent of the refactor and WD
PRs — can be reviewed and merged on its own.