Repository navigation
feat(proof): every checker move has a lean theorem or a debt row - #335
Merged
Merged
Conversation
flang/proof/lean/rules-guard.fscript reads the step dispatcher of flang/proof/checker/checker.c (every strcmp against the rule name between the first named move function and the step reader), the closed list of accepted rules in Acceptance.lean, the theorem names of Rules.lean and Term.lean and the new debt table flang/proof/tables/lean-acceptance-debt.tsv. Plans: Census (the table and five numbers), Numbers (one line), Check (red when a move has neither an acceptance constructor nor a debt row, when a debt row is paid or names an unknown move, when Lean knows a move the checker does not), Forgery (three forgeries on in-memory copies, each must go red). Measured on this tree, 5 October 2026: 83 moves, 83 with a lemma, 76 in the acceptance, 7 outside (Latin spelling of the codes: R3, R2, R5, R6, N6, O9, Vych), 5 in the debt table. N6 and O9 entered the checker on 26 September 2026 (task 1435) and never reached the acceptance; the prose counted "76 of 81" by hand ever since. Check is therefore red on this commit on purpose; the next commits add the two moves to the acceptance. Shortcuts: lean-rules:check, lean-rules:census, lean-rules:numbers, lean-rules:forgery.
Two moves the checker gained on 26 September 2026 (task 1435) now have a consistency theorem in Lean. N6 (an if-branch is non-negative when both branches are): a constructor of the step acceptance, the decidable check, its soundness lemma and the case of the block theorem, closed by the existing term lemma. O9 (a fold from zero with a counting step does not exceed the length of the same list): the model rounds addition above 2^53, so the step is exact only below the threshold. A new environment fact in Record.lean says every list bound to a name is shorter than 2^53 elements (true of the language, unknown to the model before), Rules.lean gets the bounded fold lemma, Consistency.lean the step-measure lemma and the term lemma. The acceptance is stricter than the checker here and says so in item 13 of the Acceptance.lean header: the list is a name, the step adds a literal of at most one, the left side is a bare fold. Covered rules: 78 of 83 (was 76 of 81 in the prose, 76 of 83 in fact), proven by decide. Axioms of the consistency theorem: propext, Classical.choice, Quot.sound. Two new traps (85: O9 with a step of two, 86: N6 without its second premise) fail to build, as they must; their counterexamples are proven in Rules.lean. Local chain build: Term 51 s, Acceptance 16 s, Consistency 20 s.
A job lean-rules-guard in ci.yml builds the bootstrap compiler and runs the three forgeries (each must go red) and then the check; Lean is not needed for either. The nightly lean-crosscheck.yml runs the same two commands before the verdict crosscheck, so a new checker move without a theorem is named as such instead of being counted among the old debt.
ADR-0064 records the decision: every checker move has a Lean theorem or a debt row with a task number, and a guard, not prose, keeps the two lists aligned. Task 4791 names the four moves that stay in debt besides the evaluator of task 1183 (two empty-list moves read the body line by line; two case-split moves depend on the evaluator and need a capture-free substitution in the model) with the measured cost. The zettel keeps the finding: two moves lived nine days without a theorem because the count "81" was copied by hand. road-to-1-0 section 3 and its table row carry the measured numbers with their primes; tables.md describes the debt table; the Lean report gets a dated note.
The case-split moves R2 and R3 (Latin spelling) recovered the condition
from the first difference between the formula and its first half and
substituted it as text into every occurrence, never asking whether an
occurrence stands under a binder. Under a binder a piece has no single
value: in "(fold [1,0] from 0 as a, e -> (if (e > 0) then e - a else
a - e)) < 1" the condition is true on the first element and false on
the second, the fold yields 1 and the formula is false, while with
"yes" or "no" in its place the fold yields -1 and both halves close by
evaluation. The checker accepted such a record with code 0 ("proven:
1"); the language itself violates that postcondition at run time.
Both moves now refuse any binder in the formula - the kernel's closed
list of six, the same one E3 and T2 use. The forgery
forgery-case-split-captures-a-bound-name joins the set as record-lies
(ratchet forgeries 38 -> 39); the pre-fix checker built from HEAD
answers 0 on it, the fixed one answers 1 at step 3. No honest record is
touched: the corpus holds three R2/R3 formulas, none with a binder.
The checker test suite is green with the forgery in the set; the full
Lean crosscheck of this branch is green (273 pairs, 1513 blocks, 0
disagreements, 57 traps refused), and its "outside the acceptance"
list no longer names N6 or O9.
Recorded as case-split-substitutes-under-a-binder (closed) in the
known violations, in a zettel, in task 4791 and in ADR-0064 3.1.
The forgery step calls rules-guard.fscript by file inside an if with exit 1, the only shape the forgery-probe guard recognises. Marks taken by lean-rules:numbers and run.fscript are removed: the prose-numbers guard knows five instruments and these are not among them; the prose keeps the date and the command. The share ledger gets the row of the audit-4791 program (1 claim, declared).
Sixteen marks and the C row of the tree inventory move to the values of this tree: checker.c 10497 to 10505, lean 12676 to 12895 lines, two zettel, one probe program, one corpus record.
records-nesting lists forgery-case-split-captures-a-bound-name among the records that lie on purpose (7 now); the zettel links the existing note checks-that-stopped-comparing instead of a name no note carries. Measured here on a rebuilt binary: 94 records, 0 unexplained.
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.
Что сделано
У каждого приёма сверщика (
шаг_выводавflang/proof/checker/checker.c) теперь либо теорема в приёмке Lean, либо строка долга с номером задачи — ADR-0064. Список приёмов снимается с кода прибором, а не пишется прозой.flang/proof/lean/rules-guard.fscript— четыре плана:Census(перепись приём → лемма → приёмка → долг),Numbers(пять чисел одной строкой),Check(сторож),Forgery(три порчи копий, каждая обязана покраснеть).Acceptance.leanс теоремами вRules.lean; девять дней они стояли без теоремы, и ничего не краснело.flang/proof/tables/lean-acceptance-debt.tsv— пять строк долга (Р2, Р3, Р5, Р6, Выч) под задачей 4791.lean-rules-guardвci.ymlна каждый пуш (Lean ему не нужен) и перед ночной сверкой вlean-crosscheck.yml.forgery-case-split-captures-a-bound-name.recordв корпусе, заметка вdocs/zettel/, запись вknown-soundness-violations.mdзакрыта.Замер 5 октября 2026 (прибором, ветка от
6b459ded0)Чего здесь нет
flang/selfне тронут.🤖 Generated with Claude Code
https://claude.ai/code/session_01X5n29umGpiervMVgnvvqht