Repository navigation
feat(lean): the last five checker moves enter the acceptance - #339
Merged
Merged
Conversation
Vych, R2, R3, R5, R6 and Razv1 over a function body now have a soundness theorem in the Lean model, so every one of the 83 moves of shag_vyvoda is accepted and the debt table is empty. Vych is judged by a closed evaluation of the parsed formula that answers only where the value is the same in every world. R2 and R3 replace a subformula by the literals da and net and lean on zamF-verno; the condition is also recovered from the text, as the checker does it. R5, R6 and Razv1 by line use the fact that the result equals the body; the reader now assembles a body of several lines (razbor with its cases, a fold header on its own line), and the term model gains razborS, a list case analysis whose result is a list. The model equality is Object.is, as in the language: not-a-number equals itself. Tozhd1 loses its "both are numbers" premise and its model-only counterexample. The reader takes the sort of a name from its declaration, reads a postcondition that continues on deeper lines, and keeps those lines out of the body. Kol1 and Kol-zapret give the two ring rows of the table their lemmas. A step the model does not read (a text case analysis, M2 through the registry of proven postconditions) is outside the model, not refused. The crosscheck: 274 pairs, 1514 blocks, both accepted 1286, both refused 204, outside the model 13, disagreements 0; traps 62 of 62. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The pages that counted 78 accepted moves and five debt rows now say 83 and none, name the 13 blocks that stay outside the model and why, and list what the crosscheck found on the way. Tasks 1183 and 4791 are done and leave the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The kernel rule "ravenstvo, reshyonnoe schyotom zamknutyh chastey" had no row in the inference table, so a place proved by it was judged neither by Lean nor by the table check. It gets the row Tozhd4 and the lemma Tozhd4: a side whose closed parts are replaced by their values keeps its value, and two sides equal sign for sign are equal under Object.is. Kol1 and Kol-zapret already gave the ring rows their lemmas. The Lean rules guard now turns red on a kernel rule of the checker with no table row, and a fourth forgery on a copy (every row of one kernel rule dropped) shows that it does. The descriptions of Tozhd1 and M1 no longer speak of a model where not-a-number is unequal to itself. The table digest is taken again. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The checker answered exit code 0 and "PROVERENO VPUSTUYU" on a record in which nothing was proved, and the success code read as "proved". Such a record now gets code 3 and the words "NE PROVERENO - VPUSTUYU". A record without statements still gets 0 when its totalities or its plan are checked against the source. The strict key keeps its words. The line count of checker.c does not grow. In the corpus 15 of the 16 empty records now answer 3; the sixteenth has no statements and ten checked totalities. Seven probes that expected 0 on an empty record expect 3, and a new probe keeps the plain "PROVERENO" case on a record with proved statements. The share measure allows one empty record in its numerator instead of sixteen. With this and the table row for every kernel rule, both open rows of consistency-violations.tsv are closed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Two probes of the share self test forged an empty record and expected the share measure to catch it in the numerator. The checker now answers such a record with code 3, so it never reaches the numerator: the probes expect that answer instead. The record that may stay empty in the numerator by name is poddelka-slova-celey, the one empty record that still gets code 0. P11/P12 and P15 pass; P6 fails as it did before this change, on a verdict of types.record that is no longer printed over several lines. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Task 1313 asks for a second implementation of the record checker that shares neither language nor build tool with checker.c and is not flang. ADR-0076 records the choice: Lean 4, the language the model already lives in, built by its own toolchain with one command, make -C flang/proof/checker second. The second checker reads the binding (lines, signs, two polynomial fingerprints, SHA-256, the source path), the header, completeness, the postcondition of each statement and its derivation block, which it judges with the Lean acceptance that carries the soundness theorem. Anything else it names and answers code 4, "not taken whole". flang/proof/second-checker.fscript runs both checkers on every record of the probe set: 603 records with a source, the second gives a verdict on 72 of them, disagreements 0; a forged copy fed only to the second is named as the one disagreement. Both plans have short commands and run in the Lean crosscheck workflow. The record reader now treats "...", '...' and the guillemets with escapes as literals when it cuts a trailing comment, as checker.c does; the crosscheck found a record where it did not. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
The Lean source of the second checker is second/Checker.lean, a name the file-name guard knows. The short commands carry their timeout in the plan declaration, as the shortcut collector reads them. Task 1313 names its owner and branch, and two tasks stop pointing at the closed task 1183. Seven prose marks follow the table, now 116 lines with the row Tozhd4, and the Lean files, now 13741 lines. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
With both checker branches in, checker.c holds 8260 code lines, the probe set has 634 forged probes (0 accepted) and 319 honest ones. A record with nothing proved now answers 3 by default, so the strict family default row expects 3. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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 (9caa7dc): 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