fix(checker): reject a record whose hypothesis is not the statement's - #216
Merged
Merged
Conversation
the-homeless-god
force-pushed
the
a/checker-replays-steps-from-assumptions
branch
from
October 2, 2026 00:41
f2296da to
1d07c09
Compare
The independent checker accepted a theorem's assumption lines without asking where they came from. It now requires each one to be a conjunct of the statement's such-that clause, a precondition of the function, or "X >= 0" for a variable of a built-in segment type; otherwise code 1. New family flang/proof/checker/tests/families/hypothesis has an honest and a forged record per rule; the k2b record (a postcondition proved under a hypothesis it does not have) moves from honest to forged; two record-lies forgeries join the manifest and the forgeries ratchet. The checker-code-lines ceiling rises by the 32 lines spent. Prose numbers, the proved-share ledger and the tree inventory follow the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The forged precondition probe of the hypothesis family carried a word outside the file-name word list; it is now named like its siblings, and its proved-share ledger row counts the one postcondition the ledger counts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The independent checker left every "by assumption" step outside induction on the kernel's word, so the five valid syllogism moods proved from premises got code 3, Darii with the existence word got code 1 and a statement whose premises sit only in its such-that clause got code 1. For a statement without a function whose theorem steps are all "by assumption", whose formulas are built from boolean fields of objects bound by the statement, the checker now takes the conjuncts of the statement's such-that clause as premises and replays each step: it must follow in one move (a premise, modus ponens from "if A then F else yes", a conjunction of such, or "no" from X and "not X"). An existence goal is compared and replayed with the witness substituted, also inside field access. Each step is also judged by a truth table over the fields: a valuation where the premises hold and the step fails is code 1 with that valuation; a true step that needs more than one move stays on the kernel's word. The step's assumption number may now point at the such-that clause. New family tests/families/assumption-replay: eight honest records now checked (code 0), ten forged ones refused with code 1 (five invalid moods, premise about another object, witness without premises, witness differing from the statement, refutation without its minor premise, a swapped assumption line) and one valid but two-move record kept at code 3. checker-code-lines rises by the 102 lines spent, forgery-probes by the 11 new forged rows. The missing probe program named by the forgeries manifest comes from the kernel change of task 5311. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The checker grew by 103 lines and the tree by five flang probe files; the prose numbers and the inventory cell that count them are retaken. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The refutation and witness forgeries carried words outside the file-name word list; they are renamed and their records rewritten for the new paths. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Five new probe programs carry one obligation each; the proved-share ledger names them with the kernel's verdict: one proved, four refused. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
GCC on the CI runner refused the build with -Werror=string-compare: the conditional handed the theorem literal to a comparison with the proved-step literal. The theorem line now takes its own branch; behaviour is unchanged and the probe set gives the same answers. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The two checker branches together give 7952 code lines in checker.c, 613 forged probes (0 accepted) and 297 honest ones (0 refused); the forgery catalogue catches 38 of 38. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Together with the merged checker work, checker.c holds 8086 code lines; 628 forged probes are all refused and 310 honest ones accepted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The program came with the checker work, its row did not. The kernel row joins after the print that carries the kernel fix. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
the-homeless-god
force-pushed
the
a/checker-replays-steps-from-assumptions
branch
from
October 2, 2026 02:48
1d07c09 to
1a49b78
Compare
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.
Verified on the tree of dev plus this branch (f2296da): the checker test set passes, the provability verdict is green with all four checks, the proved-share ledger and the rule tables agree with the tree, pre-push is green, commit messages follow the convention.
🤖 Generated with Claude Code