From f99fe81f5ecd56d0deff1ae645688e9743d69a2f Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Mon, 5 Oct 2026 20:57:53 +0000 Subject: [PATCH 1/8] feat(proof): a guard counts checker moves against the lean acceptance 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. --- .flangrc | 4 + flang/proof/lean/rules-guard.fscript | 739 ++++++++++++++++++++ flang/proof/tables/lean-acceptance-debt.tsv | 6 + 3 files changed, 749 insertions(+) create mode 100644 flang/proof/lean/rules-guard.fscript create mode 100644 flang/proof/tables/lean-acceptance-debt.tsv diff --git a/.flangrc b/.flangrc index 61ce9f3d6..1ee6fd83d 100644 --- a/.flangrc +++ b/.flangrc @@ -68,6 +68,10 @@ script.ring-rules:probe = bootstrap/flang io flang/proof/probes/ring-laws/run.fs script.translation:check = bootstrap/flang io flang/translation/run.fscript --plan Проверка script.proved-share:check = bootstrap/flang io flang/proof/share-measure.fscript --max-steps 4000000000 --timeout 900000 -- --set corpus script.proved-share:forgery = bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000 +script.lean-rules:check = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Check +script.lean-rules:census = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Census +script.lean-rules:numbers = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Numbers +script.lean-rules:forgery = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Forgery script.kernel-verdict:check = bootstrap/flang io flang/proof/kernel-verdict.fscript --max-steps 4000000000 --timeout 900000 script.kernel-verdict:forgery = bootstrap/flang io flang/proof/kernel-verdict-forgery.fscript --max-steps 4000000000 --timeout 900000 script.proof-records:freshness = bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 diff --git a/flang/proof/lean/rules-guard.fscript b/flang/proof/lean/rules-guard.fscript new file mode 100644 index 000000000..2b1da58c9 --- /dev/null +++ b/flang/proof/lean/rules-guard.fscript @@ -0,0 +1,739 @@ +модуль «Lean rules guard» + использует «Inquiry» из "../../../scripts/inquiry.fscript" + использует «Tables» из "../../../scripts/tables.fscript" + использует «Lists» только «Соединить списки» + +объект «Row» + «name»: строка + «lemma»: признак + «accepted»: признак + «debt»: признак + +объект «Toggle» + «inside»: признак + «found»: список строки + +объект «Counted» + «at»: число + «kept»: список строки + +тотальная функция «Has» + принимает name: строка, names: список строки + возвращает признак + пример «A name in the list» + дано name равно "Н6" + дано names равно ["О9", "Н6"] + ожидается да + пример «A name not in the list» + дано name равно "Выч" + дано names равно ["О9", "Н6"] + ожидается нет + (длина (отфильтровать names где other → other равен name)) больше 0 + +тотальная функция «Unique» + принимает names: список строки + возвращает список строки + пример «A name stays once, in its first place» + дано names равно ["Н6", "О9", "Н6"] + ожидается ["Н6", "О9"] + свёртка names начиная с (пустой список) как kept и n → если «Has» от n и kept то kept иначе (добавить n к kept) + +тотальная функция «Before» + принимает text: строка, sign: строка + возвращает строка + пример «The text before the first sign» + дано text равно "Н6\") == 0) {" + дано sign равно "\"" + ожидается "Н6" + пример «A text without the sign is kept whole» + дано text равно "Н6" + дано sign равно "\"" + ожидается "Н6" + разбор (разделить text по sign) + случай пусто + то "" + случай голова и хвост + то голова + +тотальная функция «After first» + принимает text: строка, sign: строка + возвращает строка + пример «The text after the first sign keeps the later signs» + дано text равно "a:b:c" + дано sign равно ":" + ожидается "b:c" + пример «A text without the sign gives nothing» + дано text равно "abc" + дано sign равно ":" + ожидается "" + разбор (разделить text по sign) + случай пусто + то "" + случай голова и хвост + то соединить хвост по sign + +тотальная функция «Pieces after» + принимает text: строка, sign: строка + возвращает список строки + пример «Every piece that follows the sign» + дано text равно "x strcmp(имя, \"Н6\") y strcmp(имя, \"О9\") z" + дано sign равно "strcmp(имя, \"" + ожидается ["Н6\") y ", "О9\") z"] + разбор (разделить text по sign) + случай пусто + то пустой список + случай голова и хвост + то хвост + +тотальная функция «Names after» + принимает text: строка, sign: строка, closing: строка + возвращает список строки + пример «The non-empty names after the sign, cut at the closing sign, once each» + дано text равно "x strcmp(имя, \"Н6\") y strcmp(имя, \"О9\") strcmp(имя, \"Н6\")" + дано sign равно "strcmp(имя, \"" + дано closing равно "\"" + ожидается ["Н6", "О9"] + пусть names равно (отобразить («Pieces after» от text и sign) как piece → «Before» от piece и closing) + «Unique» от (отфильтровать names где name → не (пусто name)) + +тотальная функция «Region start» + возвращает строка + пример «The first named move of the checker opens the region» + ожидается "static char *правило_т1(" + "static char *правило_т1(" + +тотальная функция «Region end» + возвращает строка + пример «The step reader closes the region» + ожидается "static char *разобрать_шаг_вывода(" + "static char *разобрать_шаг_вывода(" + +тотальная функция «Dispatched» + принимает checker: строка + возвращает список строки + пример «Every name the step dispatcher compares against, once each» + дано checker равно "static char *правило_т1(\nstrcmp(имя, \"Т1\")\nstatic char *разобрать_шаг_вывода(" + ожидается ["Т1"] + пример «Without the region there are no names» + дано checker равно "strcmp(имя, \"Т1\")" + ожидается пустой список + пусть region равно («Before» от («After first» от checker и («Region start»)) и («Region end»)) + «Names after» от region и "strcmp(имя, \"" и "\"" + +тотальная функция «List start» + возвращает строка + пример «The closed list of the acceptance» + ожидается "def «правила» : List «Правило» :=" + "def «правила» : List «Правило» :=" + +тотальная функция «Accepted» + принимает acceptance: строка + возвращает список строки + пример «Every constructor of the closed list» + дано acceptance равно "x\ndef «правила» : List «Правило» :=\n [.«Т1», .«Н6»,\n .«О9»]\n\ndef «покрыто» := 3\n" + ожидается ["Т1", "Н6", "О9"] + пример «Without the list there are no names» + дано acceptance равно "def «покрыто» : Nat := 0" + ожидается пустой список + пусть block равно («Before» от («After first» от acceptance и («List start»)) и "]") + «Names after» от block и ".«" и "»" + +тотальная функция «Theorems» + принимает text: строка + возвращает список строки + пример «The name of every theorem» + дано text равно "theorem «Н6» (u : Bool) :\n by simp\ntheorem «О9-шаг» (s : X)\n/- theorem «нет» -/\n" + ожидается ["Н6", "О9-шаг"] + пусть lines равно (отфильтровать (разделить text по "\n") где line → line начинается с "theorem «") + отобразить lines как line → «Before» от («After first» от line и "theorem «") и "»" + +тотальная функция «Has lemma» + принимает name: строка, theorems: список строки + возвращает признак + пример «A theorem of the same name» + дано name равно "Н6" + дано theorems равно ["Н6", "Н12"] + ожидается да + пример «A theorem that continues the name after a dash» + дано name равно "Выч" + дано theorems равно ["Выч-звено", "Н12"] + ожидается да + пример «A longer name is not this name» + дано name равно "Н1" + дано theorems равно ["Н10", "Н12"] + ожидается нет + пусть dashed равно (соединить name с "-") + (длина (отфильтровать theorems где t → (t равен name) или (t начинается с dashed))) больше 0 + +тотальная функция «Debt names» + принимает debt: строка + возвращает список строки + пример «The first cell of every data row» + дано debt равно "name\ttask\treason\nВыч\t1183\tвычислитель\nР5\t1183\tтело по строкам\n" + ожидается ["Выч", "Р5"] + отобразить («Rows» от debt) как row → «Cell» от 1 и row + +тотальная функция «Quote step» + принимает t: «Toggle», part: строка + возвращает «Toggle» + пример «A part inside quotes is kept» + дано t равно запись «Toggle» с «inside» равным да и «found» равным пустой список + дано part равно "а" + ожидается запись «Toggle» с «inside» равным нет и «found» равным ["а"] + пример «A part outside quotes is dropped» + дано t равно запись «Toggle» с «inside» равным нет и «found» равным ["а"] + дано part равно ", " + ожидается запись «Toggle» с «inside» равным да и «found» равным ["а"] + пусть found равно (если t.«inside» то (добавить part к (t.«found»)) иначе (t.«found»)) + запись «Toggle» с «inside» равным (не (t.«inside»)) и «found» равным found + +тотальная функция «Quoted» + принимает text: строка + возвращает список строки + пример «The parts between quotes, empty ones dropped» + дано text равно " \"\", \"а\",\n \"б в\"\n" + ожидается ["а", "б в"] + пусть start равно (запись «Toggle» с «inside» равным нет и «found» равным (пустой список)) + пусть found равно ((свёртка (разделить text по "\"") начиная с start как t и part → «Quote step» от t и part).«found») + отфильтровать found где part → не (пусто part) + +тотальная функция «Kernel rules» + принимает checker: строка + возвращает список строки + пример «The literals of the closed array of kernel rules, the empty one dropped» + дано checker равно "x\nstatic const char *ПРАВИЛА[] = {\n \"\", \"порядок\",\n \"вхождение\"\n};\n\"y\"\n" + ожидается ["порядок", "вхождение"] + «Quoted» от («Before» от («After first» от checker и "static const char *ПРАВИЛА[] = {") и "};") + +тотальная функция «Rows of kernel rule» + принимает kernel: строка, table: строка + возвращает список список строки + пример «The rows whose kernel-rule cell names the rule, alone or among others» + дано kernel равно "порядок" + дано table равно "h\nО1\tО\trule\tпорядок\ta\tc\nД1\tД\trule\tпорядок|строгий\ta\tc\nН1\tН\trule\tзнак\ta\tc\n" + ожидается [["О1", "О", "rule", "порядок", "a", "c"], ["Д1", "Д", "rule", "порядок|строгий", "a", "c"]] + отфильтровать («Rows» от table) где row → «Has» от kernel и (разделить («Cell» от 4 и row) по "|") + +тотальная функция «Replaced» + принимает inputs: список строки, place: число, text: строка + возвращает список строки + пример «The element at the position is replaced» + дано inputs равно ["a", "b", "c"] + дано place равно 2 + дано text равно "x" + ожидается ["a", "x", "c"] + пусть start равно (запись «Counted» с «at» равным 0 и «kept» равным (пустой список)) + (свёртка inputs начиная с start как c и e → «Counting» от c и e и place и text).«kept» + +тотальная функция «Counting» + принимает c: «Counted», e: строка, place: число, text: строка + возвращает «Counted» + пример «The counted position takes the text» + дано c равно запись «Counted» с «at» равным 1 и «kept» равным ["a"] + дано e равно "b" + дано place равно 2 + дано text равно "x" + ожидается запись «Counted» с «at» равным 2 и «kept» равным ["a", "x"] + пусть grown равно ((c.«at») плюс 1) + запись «Counted» с «at» равным grown и «kept» равным (добавить (если grown равен place то text иначе e) к (c.«kept»)) + +тотальная функция «Row of» + принимает name: строка, theorems: список строки, accepted: список строки, debt: список строки + возвращает «Row» + пример «A covered move» + дано name равно "Н6" + дано theorems равно ["Н6"] + дано accepted равно ["Н6"] + дано debt равно пустой список + ожидается запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет + пусть lemma равно («Has lemma» от name и theorems) + пусть owed равно («Has» от name и debt) + пусть taken равно («Has» от name и accepted) + запись «Row» с «name» равным name и «lemma» равным lemma и «accepted» равным taken и «debt» равным owed + +тотальная функция «All theorems» + принимает inputs: список строки + возвращает список строки + пример «The theorems of the rules file and of the term file together» + дано inputs равно ["", "", "theorem «Н6» x\ntheorem «О1» y", "theorem «Т1-терм» z", "", ""] + ожидается ["Н6", "О1", "Т1-терм"] + «Соединить списки» от («Theorems» от («Cell» от 3 и inputs)) и («Theorems» от («Cell» от 4 и inputs)) + +тотальная функция «Census rows» + принимает inputs: список строки + возвращает список «Row» + пример «One row per dispatched name» + дано inputs равно ["static char *правило_т1(\n strcmp(имя, \"Н6\")\nstatic char *разобрать_шаг_вывода(", + "def «правила» : List «Правило» :=\n [.«Н6»]", "theorem «Н6» x", "", "name\ttask\treason\n", ""] + ожидается [запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет] + пусть theorems равно («All theorems» от inputs) + пусть accepted равно («Accepted» от («Cell» от 2 и inputs)) + пусть debt равно («Debt names» от («Cell» от 5 и inputs)) + отобразить («Dispatched» от («Cell» от 1 и inputs)) как name → «Row of» от name и theorems и accepted и debt + +тотальная функция «Mark» + принимает holds: признак, word: строка + возвращает строка + пример «A held mark is the word» + дано holds равно да + дано word равно "лемма" + ожидается "лемма" + пример «An unheld mark is a dash» + дано holds равно нет + дано word равно "лемма" + ожидается "—" + если holds то word иначе "—" + +тотальная функция «Row line» + принимает row: «Row» + возвращает строка + пример «A covered move prints its three marks» + дано row равно запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет + ожидается "Н6\tлемма\tприёмка\t—" + соединить [(row.«name»), "\t", («Mark» от (row.«lemma») и "лемма"), "\t", + («Mark» от (row.«accepted») и "приёмка"), "\t", («Mark» от (row.«debt») и "долг")] по "" + +тотальная функция «Outside» + принимает rows: список «Row» + возвращает список строки + пример «The moves outside the acceptance» + дано rows равно [запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет, + запись «Row» с «name» равным "Выч" и «lemma» равным да и «accepted» равным нет и «debt» равным да] + ожидается ["Выч"] + отобразить (отфильтровать rows где row → не (row.«accepted»)) как row → row.«name» + +тотальная функция «Without lemma» + принимает rows: список «Row» + возвращает список строки + пример «The moves without a lemma» + дано rows равно [запись «Row» с «name» равным "Н6" и «lemma» равным нет и «accepted» равным да и «debt» равным нет] + ожидается ["Н6"] + отобразить (отфильтровать rows где row → не (row.«lemma»)) как row → row.«name» + +тотальная функция «Owed» + принимает rows: список «Row» + возвращает список строки + пример «The moves outside the acceptance that have a debt row» + дано rows равно [запись «Row» с «name» равным "Р5" и «lemma» равным да и «accepted» равным нет и «debt» равным нет, + запись «Row» с «name» равным "Выч" и «lemma» равным да и «accepted» равным нет и «debt» равным да] + ожидается ["Выч"] + отобразить (отфильтровать rows где row → (не (row.«accepted»)) и притом (row.«debt»)) как row → row.«name» + +тотальная функция «Unpaid» + принимает rows: список «Row» + возвращает список строки + пример «The moves outside the acceptance without a debt row» + дано rows равно [запись «Row» с «name» равным "О9" и «lemma» равным да и «accepted» равным нет и «debt» равным нет] + ожидается ["О9"] + отобразить (отфильтровать rows где row → (не (row.«accepted»)) и притом (не (row.«debt»))) как row → row.«name» + +тотальная функция «Paid» + принимает rows: список «Row» + возвращает список строки + пример «The moves inside the acceptance that still have a debt row» + дано rows равно [запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным да] + ожидается ["Н6"] + отобразить (отфильтровать rows где row → (row.«accepted») и притом (row.«debt»)) как row → row.«name» + +тотальная функция «Comma list» + принимает names: список строки + возвращает строка + пример «Names are listed with commas» + дано names равно ["Выч", "Р5"] + ожидается "Выч, Р5" + пример «No names is a dash» + дано names равно пустой список + ожидается "—" + если пусто names то "—" иначе (соединить names по ", ") + +тотальная функция «Numbers line» + принимает rows: список «Row» + возвращает строка + пример «The five numbers of the census» + дано rows равно [запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет, + запись «Row» с «name» равным "Выч" и «lemma» равным да и «accepted» равным нет и «debt» равным да] + ожидается "приёмов 2, с леммой 2, в приёмке 1, вне приёмки 1, в долге 1" + пусть total равно (длина rows) + соединить ["приёмов ", (к строке total), + ", с леммой ", (к строке (total минус (длина («Without lemma» от rows)))), + ", в приёмке ", (к строке (total минус (длина («Outside» от rows)))), + ", вне приёмки ", (к строке (длина («Outside» от rows))), + ", в долге ", (к строке (длина («Owed» от rows)))] по "" + +тотальная функция «Kernel line» + принимает kernel: строка, table: строка, theorems: список строки + возвращает строка + пример «A kernel rule names its rows and how many of them carry a lemma» + дано kernel равно "порядок" + дано table равно "h\nО1\tО\trule\tпорядок\ta\tcode\nД1\tД\trule\tпорядок|строгий\ta\tcode\n" + дано theorems равно ["О1"] + ожидается " порядок\tстрок 2\tс леммой 1" + пусть rows равно («Rows of kernel rule» от kernel и table) + пусть named равно (отфильтровать rows где row → «Has lemma» от («Cell» от 1 и row) и theorems) + соединить [" ", kernel, "\tстрок ", (к строке (длина rows)), "\tс леммой ", (к строке (длина named))] по "" + +тотальная функция «Census head» + возвращает строка + пример «The heading of the census table» + ожидается "── приёмы сверщика (шаг_вывода) против Lean: лемма, приёмка, долг ──" + "── приёмы сверщика (шаг_вывода) против Lean: лемма, приёмка, долг ──" + +тотальная функция «Kernel head» + возвращает строка + пример «The heading of the kernel view» + ожидается "── правила ядра ПРАВИЛА[] сверщика: строк ведомости и лемм к ним ──" + "── правила ядра ПРАВИЛА[] сверщика: строк ведомости и лемм к ним ──" + +тотальная функция «Census lines» + принимает inputs: список строки + возвращает список строки + пример «The table, its numbers and the kernel view» + дано inputs равно ["static char *правило_т1(\n strcmp(имя, \"Н6\")\nstatic char *разобрать_шаг_вывода(", + "def «правила» : List «Правило» :=\n [.«Н6»]", "theorem «Н6» x\ntheorem «О1» y", "", "name\ttask\treason\n", + "h\nО1\tО\trule\tпорядок\ta\tcode\n"] + ожидается ["── приёмы сверщика (шаг_вывода) против Lean: лемма, приёмка, долг ──", "Н6\tлемма\tприёмка\t—", "", + "приёмов 1, с леммой 1, в приёмке 1, вне приёмки 0, в долге 0", "вне приёмки: —", "", + "── правила ядра ПРАВИЛА[] сверщика: строк ведомости и лемм к ним ──"] + пусть rows равно («Census rows» от inputs) + пусть theorems равно («All theorems» от inputs) + пусть table равно («Cell» от 6 и inputs) + пусть rules равно («Kernel rules» от («Cell» от 1 и inputs)) + пусть kernel равно (отобразить rules как r → «Kernel line» от r и table и theorems) + пусть outside равно (соединить ["вне приёмки: ", («Comma list» от («Outside» от rows))] по "") + пусть tail равно ["", («Numbers line» от rows), outside, "", + («Kernel head»)] + пусть body равно (приписать («Census head») к (отобразить rows как row → «Row line» от row)) + «Соединить списки» от body и («Соединить списки» от tail и kernel) + +тотальная функция «Broken» + принимает rows: список «Row», accepted: список строки + возвращает список строки + пример «Fewer than fifty names on either side means the reading broke» + дано rows равно пустой список + дано accepted равно пустой список + ожидается ["сверщик: вычитано 0 приёмов — разбор области шаг_вывода сломан", + "Acceptance.lean: вычитано 0 правил — разбор списка «правила» сломан"] + пусть few равно (соединить ["сверщик: вычитано ", (к строке (длина rows)), + " приёмов — разбор области шаг_вывода сломан"] по "") + пусть short равно (соединить ["Acceptance.lean: вычитано ", (к строке (длина accepted)), + " правил — разбор списка «правила» сломан"] по "") + пусть a равно (если (длина rows) не меньше 50 то (пустой список) иначе [few]) + пусть b равно (если (длина accepted) не меньше 50 то (пустой список) иначе [short]) + «Соединить списки» от a и b + +тотальная функция «Named» + принимает head: строка, names: список строки, tail: строка + возвращает список строки + пример «Each name is wrapped in the same words» + дано head равно "приём «" + дано names равно ["О9", "Н6"] + дано tail равно "» без теоремы" + ожидается ["приём «О9» без теоремы", "приём «Н6» без теоремы"] + отобразить names как name → соединить [head, name, tail] по "" + +тотальная функция «Drift» + принимает rows: список «Row», accepted: список строки, debt: список строки + возвращает список строки + пример «Names known to Lean or to the debt that the checker does not dispatch are named» + дано rows равно [запись «Row» с «name» равным "Н6" и «lemma» равным да и «accepted» равным да и «debt» равным нет] + дано accepted равно ["Н6", "Т1"] + дано debt равно ["Р5"] + ожидается ["приёмка Lean знает «Т1», а сверщик такого приёма не ведёт", + "долг «Р5» о приёме, которого в сверщике нет"] + пусть names равно (отобразить rows как row → row.«name») + пусть lean равно (отфильтровать accepted где name → не («Has» от name и names)) + пусть owed равно (отфильтровать debt где name → не («Has» от name и names)) + пусть a равно («Named» от "приёмка Lean знает «" и lean и "», а сверщик такого приёма не ведёт") + пусть b равно («Named» от "долг «" и owed и "» о приёме, которого в сверщике нет") + «Соединить списки» от a и b + +тотальная функция «Troubles» + принимает inputs: список строки + возвращает список строки + пример «A move outside the acceptance without a debt row is a trouble» + дано inputs равно ["static char *правило_т1(\n strcmp(имя, \"Н6\")\nstatic char *разобрать_шаг_вывода(", + "def «правила» : List «Правило» :=\n [.«Т1»]", "theorem «Н6» x", "", "name\ttask\treason\nР5\t1183\tтело\n", ""] + ожидается ["сверщик: вычитано 1 приёмов — разбор области шаг_вывода сломан", + "Acceptance.lean: вычитано 1 правил — разбор списка «правила» сломан", + "приём «Н6» без приёмки Lean и без строки долга", + "приёмка Lean знает «Т1», а сверщик такого приёма не ведёт", "долг «Р5» о приёме, которого в сверщике нет"] + пусть rows равно («Census rows» от inputs) + пусть accepted равно («Accepted» от («Cell» от 2 и inputs)) + пусть unpaid равно («Named» от "приём «" и («Unpaid» от rows) и "» без приёмки Lean и без строки долга") + пусть lemmaless равно («Named» от "приём «" и («Without lemma» от rows) и "» без леммы в Rules.lean и Term.lean") + пусть paid равно («Named» от "долг «" и («Paid» от rows) и "» уплачен — приём в приёмке Lean, строку долга снять") + пусть drift равно («Drift» от rows и accepted и («Debt names» от («Cell» от 5 и inputs))) + пусть tail равно («Соединить списки» от paid и drift) + пусть rest равно («Соединить списки» от unpaid и («Соединить списки» от lemmaless и tail)) + «Соединить списки» от («Broken» от rows и accepted) и rest + +тотальная функция «Red» + принимает trouble: строка + возвращает строка + пример «A trouble is printed red» + дано trouble равно "x" + ожидается "КРАСНО x" + соединить ["КРАСНО ", trouble] по "" + +тотальная функция «Check lines» + принимает inputs: список строки + возвращает список строки + пример «Troubles go red, the numbers follow» + дано inputs равно пустой список + ожидается ["КРАСНО сверщик: вычитано 0 приёмов — разбор области шаг_вывода сломан", + "КРАСНО Acceptance.lean: вычитано 0 правил — разбор списка «правила» сломан", + "приёмов 0, с леммой 0, в приёмке 0, вне приёмки 0, в долге 0"] + пусть reds равно (отобразить («Troubles» от inputs) как trouble → «Red» от trouble) + «Соединить списки» от reds и [(«Numbers line» от («Census rows» от inputs))] + +тотальная функция «Forged acceptance» + принимает inputs: список строки + возвращает список строки + пример «The copy of the acceptance loses the constructor Н5» + дано inputs равно ["", "[.«Н4», .«Н5», .«Н9»]", "", "", "", ""] + ожидается ["", "[.«Н4», .«Н9»]", "", "", "", ""] + «Replaced» от inputs и 2 и (соединить (разделить («Cell» от 2 и inputs) по " .«Н5»,") по "") + +тотальная функция «Forged checker» + принимает inputs: список строки + возвращает список строки + пример «The copy of the checker gains a move nobody proved, right inside the region» + дано inputs равно ["static char *правило_т1(x", "", "", "", "", ""] + ожидается ["static char *правило_т1( strcmp(имя, \"Ъ1\") x", "", "", "", "", ""] + пусть rest равно («After first» от («Cell» от 1 и inputs) и («Region start»)) + пусть head равно (соединить («Region start») с " strcmp(имя, \"Ъ1\") ") + «Replaced» от inputs и 1 и (соединить [head, rest] по "") + +тотальная функция «Forged debt» + принимает inputs: список строки + возвращает список строки + пример «The copy of the debt table owes a move that is already accepted» + дано inputs равно ["", "", "", "", "name\ttask\treason\n", ""] + ожидается ["", "", "", "", "name\ttask\treason\nН5\t0\tподлог\n", ""] + «Replaced» от inputs и 5 и (соединить («Cell» от 5 и inputs) с "Н5\t0\tподлог\n") + +тотальная функция «Probe lines» + принимает number: строка, what: строка, troubles: список строки + возвращает список строки + пример «A forgery the guard caught» + дано number равно "1" + дано what равно "Н5 убран из приёмки" + дано troubles равно ["x"] + ожидается ["СОШЛОСЬ подлог 1 (Н5 убран из приёмки) — красных 1", " КРАСНО x"] + пример «A forgery the guard missed» + дано number равно "2" + дано what равно "лишний приём" + дано troubles равно пустой список + ожидается ["ПРОВАЛ подлог 2 (лишний приём) — сторож остался зелёным"] + пусть missed равно (соединить ["ПРОВАЛ подлог ", number, " (", what, ") — сторож остался зелёным"] по "") + пусть caught равно (соединить ["СОШЛОСЬ подлог ", number, " (", what, ") — красных ", + (к строке (длина troubles))] по "") + приписать (если пусто troubles то missed иначе caught) к («Named» от " КРАСНО " и troubles и "") + +тотальная функция «New troubles» + принимает forged: список строки, clean: список строки + возвращает список строки + пример «Only the troubles the forgery added are its own» + дано forged равно пустой список + дано clean равно ["сверщик: вычитано 0 приёмов — разбор области шаг_вывода сломан"] + ожидается ["Acceptance.lean: вычитано 0 правил — разбор списка «правила» сломан"] + отфильтровать («Troubles» от forged) где t → не («Has» от t и clean) + +тотальная функция «Forgery head» + возвращает строка + пример «The heading of the forgery report» + ожидается "── три подлога на КОПИЯХ, дерево не тронуто ──" + "── три подлога на КОПИЯХ, дерево не тронуто ──" + +тотальная функция «Forgery lines» + принимает inputs: список строки + возвращает список строки + пример «Three forgeries on copies, the tree untouched» + дано inputs равно пустой список + ожидается ["── три подлога на КОПИЯХ, дерево не тронуто ──", + "ПРОВАЛ подлог 1 (Н5 убран из приёмки Lean) — сторож остался зелёным", + "ПРОВАЛ подлог 2 (в сверщике приём Ъ1 без теоремы) — сторож остался зелёным", + "ПРОВАЛ подлог 3 (долг на Н5, который в приёмке есть) — сторож остался зелёным"] + пусть clean равно («Troubles» от inputs) + пусть fa равно («New troubles» от («Forged acceptance» от inputs) и clean) + пусть fc равно («New troubles» от («Forged checker» от inputs) и clean) + пусть fd равно («New troubles» от («Forged debt» от inputs) и clean) + пусть one равно («Probe lines» от "1" и "Н5 убран из приёмки Lean" и fa) + пусть two равно («Probe lines» от "2" и "в сверщике приём Ъ1 без теоремы" и fc) + пусть three равно («Probe lines» от "3" и "долг на Н5, который в приёмке есть" и fd) + «Соединить списки» от [(«Forgery head»)] и («Соединить списки» от one и («Соединить списки» от two и three)) + +тотальная функция «Reds of» + принимает lines: список строки + возвращает число + пример «Red lines and failed probes are counted» + дано lines равно ["КРАСНО x", "ПРОВАЛ подлог 1", "СОШЛОСЬ подлог 2", " КРАСНО y"] + ожидается 2 + длина (отфильтровать lines где line → (line начинается с "КРАСНО") или (line начинается с "ПРОВАЛ")) + +тотальная функция «Judged» + принимает lines: список строки + возвращает «Продолжение» + пример «A red line fails the plan» + дано lines равно ["КРАСНО x"] + ожидается вариант «Провал» с код равным "FLANG_LEAN_RULES" и сообщение равным "КРАСНО x\nРАЗОШЛОСЬ: красных 1" + пример «No red line ends the work» + дано lines равно ["приёмов 83"] + ожидается вариант «Конец работы» с значение равным "приёмов 83\nсошлось" + пусть reds равно («Reds of» от lines) + пусть failed равно (соединить (добавить (соединить ["РАЗОШЛОСЬ: красных ", (к строке reds)] по "") к lines) по "\n") + если reds больше 0 + то вариант «Провал» с код равным "FLANG_LEAN_RULES" и сообщение равным failed + иначе вариант «Конец работы» с значение равным (соединить (добавить "сошлось" к lines) по "\n") + +тотальная функция «Files» + возвращает список список строки + пример «Six files, named and placed relative to this plan» + ожидается [["checker", "../checker/checker.c"], ["acceptance", "Acceptance.lean"], ["rules", "Rules.lean"], + ["term", "Term.lean"], ["debt", "../tables/lean-acceptance-debt.tsv"], ["table", "../tables/inference-rules.tsv"]] + [["checker", "../checker/checker.c"], ["acceptance", "Acceptance.lean"], ["rules", "Rules.lean"], + ["term", "Term.lean"], ["debt", "../tables/lean-acceptance-debt.tsv"], ["table", "../tables/inference-rules.tsv"]] + +тотальная функция «Reading» + возвращает список «Question» + отобразить («Files») как file → «Read» от («Cell» от 1 и file) и («Cell» от 2 и file) + +тотальная функция «Inputs of» + принимает answers: список «Answer» + возвращает список строки + пример «Unanswered files are empty» + дано answers равно пустой список + ожидается ["", "", "", "", "", ""] + отобразить («Files») как file → «Output of» от («Cell» от 1 и file) и answers + +тотальная функция «Mode» + принимает answers: список «Answer» + возвращает строка + пример «The mode is the word the plan started with» + дано answers равно [запись «Answer» с «name» равным "x" и «reply» равным (вариант «Пока ничего»), + запись «Answer» с «name» равным "mode" и «reply» равным (вариант «Доводы» с доводы равным ["census"])] + ожидается "census" + пример «Without the word the plan checks» + дано answers равно пустой список + ожидается "check" + разбор («Given of» от "mode" и answers) + случай пусто + то "check" + случай голова и хвост + то голова + +тотальная функция «Report» + принимает mode: строка, inputs: список строки + возвращает «Продолжение» + пример «The numbers of nothing» + дано mode равно "numbers" + дано inputs равно пустой список + ожидается вариант «Конец работы» с значение равным "приёмов 0, с леммой 0, в приёмке 0, вне приёмки 0, в долге 0" + разбор mode + случай "census" + то вариант «Конец работы» с значение равным (соединить («Census lines» от inputs) по "\n") + случай "numbers" + то вариант «Конец работы» с значение равным («Numbers line» от («Census rows» от inputs)) + случай "forgery" + то «Judged» от («Forgery lines» от inputs) + случай любое + то «Judged» от («Check lines» от inputs) + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «A file not read stops the guard» + дано asked равно "debt" + дано answers равно [запись «Answer» с «name» равным "x" и «reply» равным (вариант «Пока ничего»), + запись «Answer» с «name» равным "debt" и «reply» равным (вариант «Сбой» с код равным "E" и сообщение равным "x")] + ожидается ["не прочитан: debt (../tables/lean-acceptance-debt.tsv)"] + пример «An answered question is no obstacle» + дано asked равно "rules" + дано answers равно [запись «Answer» с «name» равным "y" и «reply» равным (вариант «Пока ничего»), + запись «Answer» с «name» равным "rules" и «reply» равным (вариант «Прочитано» с содержимое равным "x")] + ожидается пустой список + пусть paths равно (отобразить (отфильтровать («Files») где f → («Cell» от 1 и f) равен asked) как f → «Cell» от 2 и f) + если (пусто paths) или ((«Exit code of» от asked и answers) равен 0) + то пустой список + иначе [(соединить ["не прочитан: ", asked, " (", (соединить paths по ""), ")"] по "")] + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Report» от («Mode» от answers) и («Inputs of» от answers) + иначе «Proceed» от («Reading») и (stages минус 1) и answers + +тотальная функция «Started» + принимает mode: строка + возвращает «Inquiry» + пусть said равно (вариант «Доводы» с доводы равным [mode]) + пусть remembered равно [(запись «Answer» с «name» равным "mode" и «reply» равным said)] + пусть none равно (пустой список) + запись «Inquiry» с «asked» равным "" и «queue» равным none и «stages» равным 1 и «answers» равным remembered + +тотальная функция «Begin check» + возвращает «Inquiry» + «Started» от "check" + +тотальная функция «Begin census» + возвращает «Inquiry» + «Started» от "census" + +тотальная функция «Begin numbers» + возвращает «Inquiry» + «Started» от "numbers" + +тотальная функция «Begin forgery» + возвращает «Inquiry» + «Started» от "forgery" + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то вариант «Не проверено» с код равным "FLANG_LEAN_RULES_NOT_MEASURED" и сообщение равным голова + случай пусто + то «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Check» + состояние «Inquiry» + начинает с «Begin check» + обрабатывает «Next» + +план «Census» + состояние «Inquiry» + начинает с «Begin census» + обрабатывает «Next» + +план «Numbers» + состояние «Inquiry» + начинает с «Begin numbers» + обрабатывает «Next» + +план «Forgery» + состояние «Inquiry» + начинает с «Begin forgery» + обрабатывает «Next» + +тотальная функция «Объявление короткой команды lean-rules:check» + возвращает строка + "bootstrap/flang io --plan Check — каждый приём сверщика либо в приёмке Lean, либо в долге с номером задачи" + +тотальная функция «Объявление короткой команды lean-rules:census» + возвращает строка + "bootstrap/flang io --plan Census — перепись приёмов сверщика против лемм и приёмки Lean, таблицей и числом" + +тотальная функция «Объявление короткой команды lean-rules:numbers» + возвращает строка + "bootstrap/flang io --plan Numbers — пять чисел переписи одной строкой, для примет в прозе" + +тотальная функция «Объявление короткой команды lean-rules:forgery» + возвращает строка + "bootstrap/flang io --plan Forgery — три подлога на копиях: сторож обязан покраснеть на каждом" diff --git a/flang/proof/tables/lean-acceptance-debt.tsv b/flang/proof/tables/lean-acceptance-debt.tsv new file mode 100644 index 000000000..5d112de2c --- /dev/null +++ b/flang/proof/tables/lean-acceptance-debt.tsv @@ -0,0 +1,6 @@ +name task reason +Выч 1183 вычислитель половин — второй вычислитель языка внутри сверщика, модель его не воспроизводит +Р2 1183 посылки — только шаги Выч, условие восстанавливается текстом; без Выч не судится +Р3 1183 посылки — только шаги Выч, условие восстанавливается текстом; без Выч не судится +Р5 1183 тело функции читается по строкам (строка_разбора, найти_случай, тело_случая), читатель записи многострочного тела не собирает +Р6 1183 тело функции читается по строкам (тело_функции_текст), читатель записи многострочного тела не собирает From 0013728b6b09c7f4ecd3edc087487925a1304902 Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Mon, 5 Oct 2026 21:14:21 +0000 Subject: [PATCH 2/8] feat(lean): moves n6 and o9 enter the acceptance with their theorems 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. --- flang/proof/lean/Acceptance.lean | 96 ++++++++++++++++++++++++++++--- flang/proof/lean/Consistency.lean | 72 +++++++++++++++++++++-- flang/proof/lean/Record.lean | 21 +++++-- flang/proof/lean/Rules.lean | 39 +++++++++++++ flang/proof/lean/Trap.lean | 21 +++++++ 5 files changed, 232 insertions(+), 17 deletions(-) diff --git a/flang/proof/lean/Acceptance.lean b/flang/proof/lean/Acceptance.lean index 70e624e6e..6879ee51a 100644 --- a/flang/proof/lean/Acceptance.lean +++ b/flang/proof/lean/Acceptance.lean @@ -12,23 +12,32 @@ import «Запись» ## Что покрыто — считано, а не сказано -Сверщик именует в `шаг_вывода` 81 приём (70 до задачи 9616, после неё — ещё -Кон2, Разв1, Ч5, после ADR-0042 — Пр1, М1, М2, К↑, Разв3, после ADR-0037 §4.3 — Т2, Э5, Э6). Здесь их **76** — `«покрыто»`, проверено `decide` в -`Consistency.lean`; список закрыт: имя вне списка даёт отказ, как и в -сверщике имя вне его списка. +Сверщик именует в `шаг_вывода` 83 приёма (70 до задачи 9616, после неё — ещё +Кон2, Разв1, Ч5, после ADR-0042 — Пр1, М1, М2, К↑, Разв3, после ADR-0037 §4.3 — Т2, +Э5, Э6, после задачи 1435 — Н6, О9). Здесь их **78** — `«покрыто»`, проверено +`decide` в `Consistency.lean`; список закрыт: имя вне списка даёт отказ, как и в +сверщике имя вне его списка. Что приёмов у сверщика ровно столько и каждый либо +здесь, либо строкой долга в `flang/proof/tables/lean-acceptance-debt.tsv`, стережёт +`flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, ADR-0064): число +81 до 5 октября 2026 стояло в прозе от руки и девять дней не замечало Н6 и О9. - именованные — 15 из 15: ГипД ГипО И1 И2 Или1 Или2 Кон1 Кон2 Кон3 Разв1 Разв2 Св1 Т1 Цел1 Цел2; Разв1 — лишь «из N», разбор выписанного конструктора суммы в самой формуле (ADR-0042 §2); Разв1 по строке тела — разбор списка — вне приёмки (`«внеПриёмки»`); -- семейные — 61: О6, Ч5 (задача 1130: О6 — левая сторона представима, факт окружения «числа-представимы» в `Record.lean`; Ч5 — точные тексты, «к строке» от точного числа, граница 11 в `Term.lean`); Т2, Э5, Э6 (ADR-0037 §4.3, задачи 3123 и 4058: Т2 — допущение-квантор со строки `требует` с другим именем элемента, Э5 — выписанный список, Э6 — отображение; список функций — список кодов, граница 10 в `Term.lean`); К↑, Разв3, Пр1, М1, М2 (ADR-0042 §2; К↑ — поле выписанного конструктора, прочитанное числом, Разв3 — развёртка своего тела на месте «результат» и вызова функции с телом одной строкой, М1 — со второй стороной-литералом меньше 2⁵³ по модулю, М2 — шаг «добавить|приписать Х к а» без вызова); Р1 Р4; Н1–Н5 Н7–Н10 Н12; Пред1 П1–П3 П5 П6; Д1 Д3–Д6; О1–О6 - О8 О10; С1–С4; СС1–СС4; В1–В4; Э1–Э4; Ч1–Ч6. +- семейные — 63: Н6, О9 (задача 1435, приёмка 5 октября 2026: Н6 — копара ветвей + выбора, условие не читается; О9 — свёртка по списку-имени от нуля шагом меры не + выше единицы, под фактом окружения «списки-коротки» из `Record.lean`); О6, Ч5 (задача 1130: О6 — левая сторона представима, факт окружения «числа-представимы» в `Record.lean`; Ч5 — точные тексты, «к строке» от точного числа, граница 11 в `Term.lean`); Т2, Э5, Э6 (ADR-0037 §4.3, задачи 3123 и 4058: Т2 — допущение-квантор со строки `требует` с другим именем элемента, Э5 — выписанный список, Э6 — отображение; список функций — список кодов, граница 10 в `Term.lean`); К↑, Разв3, Пр1, М1, М2 (ADR-0042 §2; К↑ — поле выписанного конструктора, прочитанное числом, Разв3 — развёртка своего тела на месте «результат» и вызова функции с телом одной строкой, М1 — со второй стороной-литералом меньше 2⁵³ по модулю, М2 — шаг «добавить|приписать Х к а» без вызова); Р1 Р4; Н1–Н10 Н12; Пред1 П1–П3 П5 П6; Д1 Д3–Д6; О1–О6 + О8–О10; С1–С4; СС1–СС4; В1–В4; Э1–Э4; Ч1–Ч6. Цел1 и Цел2 — с задачи 3855: «Т : цел» в модели есть «числом» (`Term.lean`, граница 3), и лемма проверяет правило на бесконечностях и не-числе, а на дробях — нет. -Чего нет и почему — пять приёмов (задачи 1130, 4058): +Чего нет и почему — пять приёмов (задачи 1130, 4058); те же пять стоят строками +долга в `flang/proof/tables/lean-acceptance-debt.tsv`, по строке на приём с номером +задачи, и сторож `lean-rules:check` краснеет, едва приём без строки долга появится в +сверщике или строка переживёт свой приём: - Выч, Р2, Р3 — вычислитель половин (`половина_закрыта`): модель его не воспроизводит, а Р2 и Р3 берут посылками только шаги Выч. Это второй @@ -96,6 +105,12 @@ import «Запись» списка (`«точноеЧисло?»`); сверщик берёт литерал любой длины и пишет его текстом как написан — «к строке 007» у сверщика «007», в модели и в языке «7». +13. О9 (задача 1435): список свёртки — имя (как у О8), левая сторона — голая + свёртка, шаг меры — «накопитель» либо «накопитель плюс литерал» с литералом + 0 или 1, либо выбор из двух таких (`«шагМеры»`); сверщик берёт список любым + простым термом и слева ещё «длина (свёртка …)». Лемма стоит на факте окружения + «списки-коротки» — всякое имя-список короче 2⁵³ элементов: в языке так, а + модель этого сама не знает (как «числа-представимы» у О6). Каждое место — кандидат в расхождение сверки вердиктов (`run.fscript`); на наборе проб сверщика (1362 блока, 14 сентября 2026) ни одно вердикта не развело. @@ -651,6 +666,19 @@ def «ветвьСчёта» (s : «ТермЧ») (a : String) : Bool := def «шагСчёта» (s : «ТермЧ») (a : String) : Bool := «ветвьСчёта» s a || (match s with | .«если» _ b c => «ветвьСчёта» b a && «ветвьСчёта» c a | _ => false) +/-- Ветвь шага МЕРЫ (О9): накопитель как есть либо «накопитель плюс литерал» с + литералом от 0 до 1 — сверщик: `ветвь_счёта` с пределом 1. -/ +def «ветвьМеры» (s : «ТермЧ») (a : String) : Bool := + match s with + | .«имя» x => x == a + | .«плюс» (.«имя» x) (.«лит» k) => x == a && decide (0 ≤ k) && decide (k ≤ 1) + | .«плюс» (.«лит» k) (.«имя» x) => x == a && decide (0 ≤ k) && decide (k ≤ 1) + | _ => false + +/-- Шаг меры: такая ветвь либо выбор из двух таких; условие выбора не читается. -/ +def «шагМеры» (s : «ТермЧ») (a : String) : Bool := + «ветвьМеры» s a || (match s with | .«если» _ b c => «ветвьМеры» b a && «ветвьМеры» c a | _ => false) + /-- Сомножитель Н8 — положительный целый литерал не выше 2⁵³ − 1. -/ def «литералН8» : «ТермЧ» → Bool | .«лит» z => decide (0 < z ∧ z ≤ «К-предст») @@ -821,6 +849,12 @@ inductive «ШагПринят» (u : «Утверждение») («преж» (h1 : «шагПо» «преж» n = some p1) (h2 : «шагПо» «преж» m = some p2) (hf : «ш».«формула» = «≥0» (.«плюс» l r)) (hp1 : p1.«формула» = «≥0» l) (hp2 : p2.«формула» = «≥0» r) : «ШагПринят» u «преж» «ш» («итог» «ш» (p1.«откр» ++ p2.«откр»)) + /-- Н6: выбор неотрицателен, когда обе ветви неотрицательны; условие не читается + (сверщик: `выбор_вывода` + `шаг_дна` на обеих ветвях, задача 1435). -/ + | «Н6» (n m : Nat) (p1 p2 : «Принятый») (c : «Форм») (a b : «ТермЧ») (ho : «ш».«основание» = .«из2» n m) (hp : «ш».«правило» = "Н6") + (h1 : «шагПо» «преж» n = some p1) (h2 : «шагПо» «преж» m = some p2) + (hf : «ш».«формула» = «≥0» (.«если» c a b)) (hp1 : p1.«формула» = «≥0» a) (hp2 : p2.«формула» = «≥0» b) : + «ШагПринят» u «преж» «ш» («итог» «ш» (p1.«откр» ++ p2.«откр»)) /-- Н9: квадрат конечного. -/ | «Н9» (n : Nat) (p : «Принятый») (t : «ТермЧ») (ho : «ш».«основание» = .«из» n) (hp : «ш».«правило» = "Н9") (h1 : «шагПо» «преж» n = some p) (hf : «ш».«формула» = «≥0» (.«умножить» t t)) @@ -1022,6 +1056,13 @@ inductive «ШагПринят» (u : «Утверждение») («преж» | «О8» (x : String) (y : String) (c : «Форм») (ho : «ш».«основание» = .«сам») (hp : «ш».«правило» = "О8") (hf : «порядок?» «ш».«формула» = some (.«длина» (.«отбор» (.«имяС» x) y c), .«длина» (.«имяС» x))) : «ШагПринят» u «преж» «ш» («итог» «ш» []) + /-- О9: свёртка по списку-имени от нуля шагом меры не обгоняет длину того же списка; + лист («сам») — обе посылки ведомости суть сличения формы (сверщик: + `свёртка_под_длиной`, задача 1435). Список — имя, как у О8. -/ + | «О9» (x a e : String) (s : «ТермЧ») (ho : «ш».«основание» = .«сам») (hp : «ш».«правило» = "О9") + (hf : «порядок?» «ш».«формула» = some (.«свёртка» (.«имяС» x) (.«лит» 0) a e s, .«длина» (.«имяС» x))) + (hae : a ≠ e) (hs : «шагМеры» s a = true) : + «ШагПринят» u «преж» «ш» («итог» «ш» []) /-- О4: литерал не выше дна верхней стороны — дно «Г не меньше ⟨литерал⟩» шагом. -/ | «О4» (n : Nat) (p : «Принятый») (a d : Int) (g : «ТермЧ») (ho : «ш».«основание» = .«из» n) (hp : «ш».«правило» = "О4") (h1 : «шагПо» «преж» n = some p) @@ -1332,6 +1373,8 @@ inductive «Правило» where | «Э6» | «О6» | «Ч5» + | «Н6» + | «О9» deriving DecidableEq, Repr def «Правило».«имя» : «Правило» → String @@ -1388,11 +1431,13 @@ def «Правило».«имя» : «Правило» → String | .«Э6» => "Э6" | .«О6» => "О6" | .«Ч5» => "Ч5" + | .«Н6» => "Н6" + | .«О9» => "О9" def «правила» : List «Правило» := [.«Т1», .«Кон1», .«Кон3», .«Цел1», .«Цел2», .«Св1», .«Или1», .«Или2», .«И1», .«И2», .«ГипО», .«ГипД», .«Р1», .«Р4», .«Н1», .«Н2», .«Н3», .«Н4», .«Н5», .«Н9», .«Н12», .«Пред1», .«П1», .«П2», .«П3», .«П5», - .«Э1», .«Э2», .«Э3», .«Э4», .«Разв2», .«СС1», .«О1», .«В2», .«Ч1», .«В1», .«Д1», .«Д6», .«С1», .«Н10», .«П6», .«О2», .«С4», .«Ч2», .«Ч6», .«Д5», .«О8», .«О4», .«О10», .«Ч3», .«В3», .«В4», .«Ч4», .«О3», .«С2», .«С3», .«Д4», .«СС2», .«СС3», .«СС4», .«Кон2», .«Н7», .«Н8», .«О5», .«Д3», .«Пр1», .«М1», .«М2», .«К↑», .«Разв1», .«Разв3», .«Т2», .«Э5», .«Э6», .«О6», .«Ч5»] + .«Э1», .«Э2», .«Э3», .«Э4», .«Разв2», .«СС1», .«О1», .«В2», .«Ч1», .«В1», .«Д1», .«Д6», .«С1», .«Н10», .«П6», .«О2», .«С4», .«Ч2», .«Ч6», .«Д5», .«О8», .«О4», .«О10», .«Ч3», .«В3», .«В4», .«Ч4», .«О3», .«С2», .«С3», .«Д4», .«СС2», .«СС3», .«СС4», .«Кон2», .«Н7», .«Н8», .«О5», .«Д3», .«Пр1», .«М1», .«М2», .«К↑», .«Разв1», .«Разв3», .«Т2», .«Э5», .«Э6», .«О6», .«Ч5», .«Н6», .«О9»] /-- Сколько правил покрыто приёмкой — число из шапки задачи 2907. -/ def «покрыто» : Nat := «правила».length @@ -1540,6 +1585,13 @@ def «Н5?» (u : «Утверждение») («преж» : List «Приня «при» (p1.«формула» = «≥0» l ∧ p2.«формула» = «≥0» r) («итог» «ш» (p1.«откр» ++ p2.«откр»)) | _ => none +def «Н6?» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») : Option «Принятый» := + («из2?» «преж» «ш»).bind fun (p1, p2) => + match «ш».«формула» with + | .«неМеньше» (.«если» c a b) (.«лит» 0) => + «при» (p1.«формула» = «≥0» a ∧ p2.«формула» = «≥0» b) («итог» «ш» (p1.«откр» ++ p2.«откр»)) + | _ => none + def «Н9?» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») : Option «Принятый» := («из1?» «преж» «ш»).bind fun p => match «ш».«формула» with @@ -1772,6 +1824,12 @@ def «О8?» (u : «Утверждение») («преж» : List «Приня «при» («ш».«основание» = .«сам» ∧ x = x') («итог» «ш» []) | _ => none +def «О9?» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») : Option «Принятый» := + match «порядок?» «ш».«формула» with + | some (.«свёртка» (.«имяС» x) (.«лит» 0) a e s, .«длина» (.«имяС» x')) => + «при» («ш».«основание» = .«сам» ∧ x = x' ∧ a ≠ e ∧ «шагМеры» s a = true) («итог» «ш» []) + | _ => none + def «О4?» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») : Option «Принятый» := («из1?» «преж» «ш»).bind fun p => match «порядок?» «ш».«формула», p.«формула» with @@ -2089,6 +2147,8 @@ def «приём» : «Правило» → «Утверждение» → List | .«Э6» => «Э6?» | .«О6» => «О6?» | .«Ч5» => «Ч5?» + | .«Н6» => «Н6?» + | .«О9» => «О9?» /-- Приём одного шага: имя правила выбирает проверку; имя вне списка — отказ. -/ def «шаг?» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») : Option «Принятый» := @@ -2344,6 +2404,16 @@ theorem «Н5?-верно» (h : «Н5?» u «преж» «ш» = some p) (hn : obtain ⟨n, m, ho, hsn, hm⟩ := «из2?-верно» hq exact .«Н5» n m p1 p2 l r ho hn hsn hm hf h1 h2 +theorem «Н6?-верно» (h : «Н6?» u «преж» «ш» = some p) (hn : «ш».«правило» = "Н6") : «ШагПринят» u «преж» «ш» p := by + simp only [«Н6?», Option.bind_eq_some_iff] at h + obtain ⟨⟨p1, p2⟩, hq, h⟩ := h + split at h <;> try cases h + rename_i c a b hf + rw [«при-some»] at h + obtain ⟨⟨h1, h2⟩, rfl⟩ := h + obtain ⟨n, m, ho, hsn, hm⟩ := «из2?-верно» hq + exact .«Н6» n m p1 p2 c a b ho hn hsn hm hf h1 h2 + theorem «Н9?-верно» (h : «Н9?» u «преж» «ш» = some p) (hn : «ш».«правило» = "Н9") : «ШагПринят» u «преж» «ш» p := by simp only [«Н9?», Option.bind_eq_some_iff] at h obtain ⟨q, hq, h⟩ := h @@ -2659,6 +2729,14 @@ theorem «О8?-верно» (h : «О8?» u «преж» «ш» = some p) (hn : obtain ⟨⟨ho, rfl⟩, rfl⟩ := h exact .«О8» _ y c ho hn hf +theorem «О9?-верно» (h : «О9?» u «преж» «ш» = some p) (hn : «ш».«правило» = "О9") : «ШагПринят» u «преж» «ш» p := by + unfold «О9?» at h + split at h <;> try cases h + rename_i x a e s x' hf + rw [«при-some»] at h + obtain ⟨⟨ho, rfl, hae, hs⟩, rfl⟩ := h + exact .«О9» _ a e s ho hn hf hae hs + theorem «О4?-верно» (h : «О4?» u «преж» «ш» = some p) (hn : «ш».«правило» = "О4") : «ШагПринят» u «преж» «ш» p := by simp only [«О4?», Option.bind_eq_some_iff] at h obtain ⟨q, hq, h⟩ := h @@ -3060,6 +3138,8 @@ theorem «приём-верно» (u : «Утверждение») («преж» | .«Э6», h, hn => «Э6?-верно» u «преж» «ш» p h hn | .«О6», h, hn => «О6?-верно» u «преж» «ш» p h hn | .«Ч5», h, hn => «Ч5?-верно» u «преж» «ш» p h hn + | .«Н6», h, hn => «Н6?-верно» u «преж» «ш» p h hn + | .«О9», h, hn => «О9?-верно» u «преж» «ш» p h hn /-- Каждый шаг, принятый функцией, принят отношением. -/ theorem «шаг?-верно» (u : «Утверждение») («преж» : List «Принятый») («ш» : «Шаг») (p : «Принятый») diff --git a/flang/proof/lean/Consistency.lean b/flang/proof/lean/Consistency.lean index 1030bc827..54532f139 100644 --- a/flang/proof/lean/Consistency.lean +++ b/flang/proof/lean/Consistency.lean @@ -23,11 +23,12 @@ import «Приёмка» | Р1 | «Р1» | своё «если-да» | | Р4 | «Р4» | сечение по факту «Л или П» из окружения | | Или1, Или2, И1, И2 | «Или1», «Или2», «И1», «И2» | «…-терм» | -| Н1, Н4, Н5, Н7, Н8, Н9, Н10, Н12 | «Н1», «Н4», «Н5», «Н7», «Н8-второй», «Н9», «Н10», «Н12» | «…-терм» | +| Н1, Н4, Н5, Н6, Н7, Н8, Н9, Н10, Н12 | «Н1», «Н4», «Н5», «Н6», «Н7», «Н8-второй», «Н9», «Н10», «Н12» | «…-терм» | | Пред1, П1, П2, П3, П5, П6 | «Пред1», «П1», «П2», «П3», «П5», «П6» | «…-терм» | | Д1, Д3, Д4, Д5, Д6 | «Д1», «Д3-днами», «Д4», «Д5», «Д6» | «…-терм» | | О1, О2, О3, О4, О5, О8, О10 | «О1», «О2», «О3», «О4», «О5» (прибавка-имя — с «отрезок-числом»), «О8», «О10» | «…-терм» | | О6 | «О6» (левая сторона представима — факт окружения «числа-представимы») | «О6-терм», «представимаЛевая-верно» | +| О9 | «О9-под-порогом» (шаг меры точен под порогом; список короче порога — факт окружения «списки-коротки») | «О9-терм», «шагМеры-верно» здесь | | С1, С2, С3, С4 | «С1», «С2», «С3», «С4» | «…-терм» | | СС1, СС2, СС3, СС4 | «СС1», «СС2», «СС3», «СС4», «СС4-противоречием» | «…-терм» | | В1, В2, В3, В4 | «В1», «В2-…», «В3-…», «В4» | «…-терм» | @@ -50,10 +51,11 @@ import «Приёмка» ## Подмножество — числом -Теорема доказана для 76 правил приёмки (`«покрыто» = 76`, проверено -`decide`) из 81 приёма `шаг_вывода`; из 15 именованных — для 15 (Разв1 — для +Теорема доказана для 78 правил приёмки (`«покрыто» = 78`, проверено +`decide`) из 83 приёмов `шаг_вывода`; из 15 именованных — для 15 (Разв1 — для разбора выписанного конструктора суммы, Разв1 по строке тела вне приёмки). -Пять непокрытых и почему — в шапке `Acceptance.lean`. +Пять непокрытых и почему — в шапке `Acceptance.lean`; что их ровно пять и у каждого +есть строка долга, стережёт `rules-guard.fscript` (ADR-0064). -/ set_option linter.unusedVariables false @@ -263,6 +265,59 @@ theorem «шагСчёта-верно» {s : «ТермЧ»} {a e : String} (hae exact «Н6» _ _ _ («ветвьСчёта-верно» hae h.1 w acc v hacc) («ветвьСчёта-верно» hae h.2 w acc v hacc) · cases h +/-! ## О9: шаг меры и свёртка под длиной (задача 1435) + +Модель округляет «плюс» за порогом 2⁵³, поэтому «накопитель плюс 1» точен, лишь +пока накопитель под порогом. Список языка короче порога — факт окружения +«списки-коротки» (`Record.lean`), — и по индукции («О9-под-порогом», `Rules.lean`) +накопитель не превосходит числа пройденных элементов на всём пути. -/ + +theorem «ветвьМеры-верно» {s : «ТермЧ»} {a e : String} (hae : a ≠ e) (h : «ветвьМеры» s a = true) + (w : «Мир») (m : Int) (v : «Знач») (hm : 0 ≤ m) (hB : m + 1 ≤ «порог» - 1) : + ∃ m2 : Int, «оценить» s («обновить» («обновить» w a («кон» m)) e v) = «кон» m2 ∧ 0 ≤ m2 ∧ m2 ≤ m + 1 := by + unfold «ветвьМеры» at h + split at h + · rename_i x + have hx : x = a := by simpa using h + subst hx; rw [«имя-накопителя» w x e («кон» m) v hae]; exact ⟨m, rfl, hm, by omega⟩ + · rename_i x k + simp only [Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq] at h + obtain ⟨⟨rfl, hk0⟩, hk1⟩ := h + simp only [«оценить», «имя-накопителя-знач» w x e («кон» m) v hae, «плюс», «чис», «обновить», «связать-о»] + refine ⟨m + k, ?_, by omega, by omega⟩ + exact w.«о».«точно» (m + k) (by unfold «порог» at *; omega) (by unfold «порог» at *; omega) + · rename_i k x + simp only [Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq] at h + obtain ⟨⟨rfl, hk0⟩, hk1⟩ := h + simp only [«оценить», «имя-накопителя-знач» w x e («кон» m) v hae, «плюс», «чис», «обновить», «связать-о»] + refine ⟨k + m, ?_, by omega, by omega⟩ + exact w.«о».«точно» (k + m) (by unfold «порог» at *; omega) (by unfold «порог» at *; omega) + · cases h + +theorem «шагМеры-верно» {s : «ТермЧ»} {a e : String} (hae : a ≠ e) (h : «шагМеры» s a = true) + (w : «Мир») (m : Int) (v : «Знач») (hm : 0 ≤ m) (hB : m + 1 ≤ «порог» - 1) : + ∃ m2 : Int, «оценить» s («обновить» («обновить» w a («кон» m)) e v) = «кон» m2 ∧ 0 ≤ m2 ∧ m2 ≤ m + 1 := by + unfold «шагМеры» at h + simp only [Bool.or_eq_true] at h + rcases h with h | h + · exact «ветвьМеры-верно» hae h w m v hm hB + · split at h + · rename_i c b d + simp only [Bool.and_eq_true] at h + simp only [«оценить»] + cases «оценитьФ» c («обновить» («обновить» w a («кон» m)) e v) + · simp only [«выбор»]; exact «ветвьМеры-верно» hae h.2 w m v hm hB + · simp only [«выбор»]; exact «ветвьМеры-верно» hae h.1 w m v hm hB + · cases h + +theorem «О9-терм» (Γ : List («Факт» «Мир»)) (x a e : String) (s : «ТермЧ») (hae : a ≠ e) + (hs : «шагМеры» s a = true) (hR : «списки-коротки» ∈ Γ) : + «Выводится» Γ (.«неБольше» (.«свёртка» (.«имяС» x) (.«лит» 0) a e s) (.«длина» (.«имяС» x))) := by + intro w hw + have hshort : ((«какСписок» (w.«имя» x)).length : Int) < «порог» := hw _ hR x + simp only [«Факт-из», «оценитьФ», «оценить», «оценитьС»] + exact «О9-под-порогом» _ _ («порог» - 1) (fun m v hm hmB => «шагМеры-верно» hae hs w m v hm hmB) (by omega) + theorem «положителенН8» (u : «Утверждение») (Γ : List («Факт» «Мир»)) (t : «ТермЧ») (hΓ : ∀ f ∈ «окружение» u, f ∈ Γ) (h : «литералН8» t = true ∨ «отрезокН8» u t = true) : «Выводится» Γ (.«меньше» (.«лит» 0) t) ∧ «Выводится» Γ (.«кон» t) := by @@ -1555,6 +1610,10 @@ theorem «шаг-верен» (u : «Утверждение») («преж» : L simp only [«итог»] rw [hf] exact «Н5-терм» _ l r («слева» _ _ (hp1 ▸ hinv p1 («шагПо-в» h1))) («справа» _ _ (hp2 ▸ hinv p2 («шагПо-в» h2))) + | «Н6» n m p1 p2 c a b ho hp h1 h2 hf hp1 hp2 => + simp only [«итог»] + rw [hf] + exact «Н6-терм» _ c a b («слева» _ _ (hp1 ▸ hinv p1 («шагПо-в» h1))) («справа» _ _ (hp2 ▸ hinv p2 («шагПо-в» h2))) | «Н9» n q t ho hp h1 hf hp1 hkon => simp only [«итог»] rw [hf]; exact «Н9-терм» _ t (hp1 ▸ hinv q («шагПо-в» h1)) @@ -1724,6 +1783,9 @@ theorem «шаг-верен» (u : «Утверждение») («преж» : L | «О8» x y c ho hp hf => simp only [«итог», «гип», List.map_nil, List.nil_append] rw [«порядок?-факт» hf]; exact «О8-терм» _ _ y c + | «О9» x a e s ho hp hf hae hs => + simp only [«итог», «гип», List.map_nil, List.nil_append] + rw [«порядок?-факт» hf]; exact «О9-терм» _ x a e s hae hs («списки-в-окружении» u) | «О4» n q a d g ho hp h1 hf hp1 had => simp only [«итог»] rw [«порядок?-факт» hf] @@ -1980,4 +2042,4 @@ theorem «состоятельность-разрешимо» (u : «Утвер «состоятельность» u («принят?-верно» u h) /-- Число покрытых правил; сверщик именует 81 приём в `шаг_вывода`. -/ -theorem «покрыто-число» : «покрыто» = 76 := by decide +theorem «покрыто-число» : «покрыто» = 78 := by decide diff --git a/flang/proof/lean/Record.lean b/flang/proof/lean/Record.lean index c483f4b72..db54c4073 100644 --- a/flang/proof/lean/Record.lean +++ b/flang/proof/lean/Record.lean @@ -29,8 +29,9 @@ SHA-256), тотальности, теоремы с ходами, посылки довода, объявленного типом с дном («нат», «вес», …), обязательства входа (6202: их несёт зовущий) и, если тело функции читается одним термом, факт «результат равен телу». Ровно на эти факты и опираются шаги «строка N». -Сверх них — факт языка «числа-представимы» (О6): всякое имя, носящее число, -носит число двойной точности, и округление его не двигает. +Сверх них — два факта языка: «числа-представимы» (О6): всякое имя, носящее число, +носит число двойной точности, и округление его не двигает; «списки-коротки» (О9): +всякое имя, носящее список, носит список короче 2⁵³ элементов. -/ set_option linter.unusedVariables false @@ -179,6 +180,14 @@ def «определение-есть» (d : «Определение») : «Ф def «числа-представимы» : «Факт» «Мир» := fun w => ∀ x, «представимо» w.«о» («какЧисло» (w.«имя» x)) +/-- Факт языка (О9, задача 1435): всякое имя, носящее список, носит список короче + 2⁵³ элементов. Счётчик «накопитель плюс 1» по такому списку не доходит до порога + округления и потому точен на всём пути; без этого факта модель шире языка: + список модели любой длины, и за порогом округление могло бы поднять накопитель + выше числа пройденных элементов. -/ +def «списки-коротки» : «Факт» «Мир» := + fun w => ∀ x, ((«какСписок» (w.«имя» x)).length : Int) < «порог» + /-- Γ утверждения: допущения, дно объявленных доводов, обязательства входа, результат равен телу, функции исходника равны своим телам, факт языка о представимости чисел. -/ @@ -190,7 +199,7 @@ def «окружение» (u : «Утверждение») : List («Факт» | some (_, t) => [«результат-есть» t] | none => []) ++ u.«определения».map «определение-есть» ++ - [«числа-представимы»] + [«числа-представимы», «списки-коротки»] theorem «допущение-в-окружении» (u : «Утверждение») (n : Nat) (f : «Форм») (h : u.«допущение» n = some f) : «Факт-из» f ∈ «окружение» u := by @@ -262,4 +271,8 @@ theorem «определение-в-окружении» (u : «Утвержде theorem «числа-в-окружении» (u : «Утверждение») : «числа-представимы» ∈ «окружение» u := by simp only [«окружение»] - exact List.mem_append_right _ (List.mem_singleton.mpr rfl) + exact List.mem_append_right _ List.mem_cons_self + +theorem «списки-в-окружении» (u : «Утверждение») : «списки-коротки» ∈ «окружение» u := by + simp only [«окружение»] + exact List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_singleton.mpr rfl)) diff --git a/flang/proof/lean/Rules.lean b/flang/proof/lean/Rules.lean index 1999019f0..2d861e7e1 100644 --- a/flang/proof/lean/Rules.lean +++ b/flang/proof/lean/Rules.lean @@ -185,6 +185,10 @@ theorem «Н6» (u : Bool) (a b : «Знач») «неотр» («выбор» u a b) = true := by cases u <;> simp [«выбор», h1, h2] +/- Встречный пример к ловушке 86: без второй посылки правило ложно. -/ +theorem «Н6-без-второй-посылки-ложна» : + «неотр» («выбор» false («кон» 1) («кон» (-1))) = false := by decide + /- flang/proof/tables/inference-rules.tsv, строка «Н7» — дословно: имя Н7 семейство Н @@ -955,6 +959,41 @@ theorem «О9» (s : «Знач» → «Знач» → «Знач») (l : «Сп simp [«неБольше»] omega +/- О9 С УЧЁТОМ ОКРУГЛЕНИЯ (приёмка, задача 1435). Лемма «О9» выше говорит о шаге, + точном при любом накопителе; «плюс» модели за порогом 2⁵³ округляет, и шаг + «накопитель плюс 1» точен лишь под порогом. Здесь тот же вывод при шаге, точном + под границей B, для списка короче B: накопитель на всём пути не выше числа + пройденных элементов, значит под B, значит шаг всякий раз точен. -/ +theorem «О9-шаг-под-порогом» (s : «Знач» → «Знач» → «Знач») (l : «Список») (B : Int) + (hs : ∀ (m : Int) x, 0 ≤ m → m + 1 ≤ B → + ∃ m2 : Int, s («кон» m) x = «кон» m2 ∧ 0 ≤ m2 ∧ m2 ≤ m + 1) + (m0 : Int) (h0 : 0 ≤ m0) (hB : m0 + l.length ≤ B) : + ∃ k : Int, «свёртка» s («кон» m0) l = «кон» k ∧ 0 ≤ k ∧ k ≤ m0 + l.length := by + induction l generalizing m0 with + | nil => exact ⟨m0, rfl, h0, by simp⟩ + | cons hd tl ih => + simp only [List.length_cons] at hB ⊢ + obtain ⟨m2, he, hn, hle⟩ := hs m0 hd h0 (by omega) + obtain ⟨k, hk, hk0, hk1⟩ := ih m2 hn (by omega) + refine ⟨k, ?_, hk0, by omega⟩ + simp only [«свёртка», he]; exact hk + +theorem «О9-под-порогом» (s : «Знач» → «Знач» → «Знач») (l : «Список») (B : Int) + (hs : ∀ (m : Int) x, 0 ≤ m → m + 1 ≤ B → + ∃ m2 : Int, s («кон» m) x = «кон» m2 ∧ 0 ≤ m2 ∧ m2 ≤ m + 1) + (hl : (l.length : Int) ≤ B) : + «неБольше» («свёртка» s («кон» 0) l) («кон» (l.length : Int)) = true := by + obtain ⟨k, hk, _, hk1⟩ := «О9-шаг-под-порогом» s l B hs 0 (Int.le_refl 0) (by omega) + rw [hk] + simp [«неБольше»] + omega + +/- Встречный пример к ловушке 85: шаг, прибавляющий двойку, обгоняет длину уже на + одном элементе. -/ +theorem «О9-шагом-два-ложна» : + «неБольше» («свёртка» (fun acc _ => match acc with | «кон» m => «кон» (m + 2) | x => x) + («кон» 0) [«кон» 0]) («кон» 1) = false := by decide + /- flang/proof/tables/inference-rules.tsv, строка «О10» — дословно: имя О10 семейство О diff --git a/flang/proof/lean/Trap.lean b/flang/proof/lean/Trap.lean index 357ec3207..e355c2e4d 100644 --- a/flang/proof/lean/Trap.lean +++ b/flang/proof/lean/Trap.lean @@ -543,3 +543,24 @@ theorem «ловушка59» («о» : «Округление») (a b c : «Зн theorem «ловушка60» («о» : «Округление») (a : «Знач») : «равен» («плюс» «о» a («минус» «о» («кон» 0) a)) («кон» 0) = true := by cases a <;> simp_all [«минус», «плюс», «отр», «чис», «равен»] + +/- ИСКАЖЕНИЕ 85 — у О9 шагу меры разрешено прибавлять двойку. + Приёмка (задача 1435): шаг «накопитель плюс литерал» с литералом не выше 1. + Здесь — не выше 2. Ложно: на списке из одного элемента накопитель 2 при + длине 1; встречный пример — «О9-шагом-два-ложна» в «Rules.lean». -/ +theorem «ловушка85» (s : «Знач» → «Знач» → «Знач») (l : «Список») + (hs : ∀ (m : Int) x, 0 ≤ m → + ∃ m2 : Int, s («кон» m) x = «кон» m2 ∧ 0 ≤ m2 ∧ m2 ≤ m + 2) : + «неБольше» («свёртка» s («кон» 0) l) («кон» (l.length : Int)) = true := by + obtain ⟨k, hk, _, hk1⟩ := «О9-шаг» s l hs 0 (Int.le_refl 0) + rw [hk] + simp [«неБольше»] + omega + +/- ИСКАЖЕНИЕ 86 — у Н6 отброшена вторая посылка. + Перечень правил: «1) А : неотр; 2) Б : неотр». Здесь только первая. + Ложно: при ложном условии выбор отдаёт Б, а Б может быть −1; + встречный пример — «Н6-без-второй-посылки-ложна» в «Rules.lean». -/ +theorem «ловушка86» (u : Bool) (a b : «Знач») (h1 : «неотр» a = true) : + «неотр» («выбор» u a b) = true := by + cases u <;> simp [«выбор», h1] From 6720dbfd51f4440c7f3f2f5363d1ab64804719b3 Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Mon, 5 Oct 2026 21:14:24 +0000 Subject: [PATCH 3/8] ci(lean): the move guard runs on every push and before the crosscheck 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. --- .github/workflows/ci.yml | 19 +++++++++++++++++++ .github/workflows/lean-crosscheck.yml | 10 ++++++++++ 2 files changed, 29 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7252bfb79..3d384de17 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1168,6 +1168,25 @@ jobs: env: FLANG_TMP: ${{ runner.temp }} + # КАЖДЫЙ ПРИЁМ СВЕРЩИКА — С ТЕОРЕМОЙ ИЛИ СО СТРОКОЙ ДОЛГА (ADR-0064). Сторож + # читает `шаг_вывода` в checker.c, закрытый список приёмки Acceptance.lean, + # имена теорем Rules.lean и Term.lean и таблицу долга + # flang/proof/tables/lean-acceptance-debt.tsv; Lean ему не нужен, поэтому он + # идёт на каждый пуш, а не ночью со сверкой. Замер 5 октября 2026: приёмов 83, + # в приёмке 78, в долге 5. Заведён потому, что Н6 и О9 (задача 1435, 26 сентября) + # девять дней не имели теоремы, а проза считала «76 из 81» от руки. Сначала + # подлог: три порчи копий, каждая обязана покраснеть, иначе сторож слеп. + lean-rules-guard: + name: lean-rules-guard + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 + - run: make -C bootstrap -j"$(nproc)" + - name: Forgery goes red + run: bootstrap/flang run-script lean-rules:forgery + - name: Every checker move has a theorem or a debt row + run: bootstrap/flang run-script lean-rules:check + # ВТОРАЯ ПОЛОВИНА — ЖИВОЙ ПРОГОН — на метке, и без ключа: там зовутся ОБЕ. # 19 мин 37 с со сборкой против границы в пять минут; на пуш она не идёт, и # это названо ценой, а не удобством. diff --git a/.github/workflows/lean-crosscheck.yml b/.github/workflows/lean-crosscheck.yml index d0c28902a..94a7453f8 100644 --- a/.github/workflows/lean-crosscheck.yml +++ b/.github/workflows/lean-crosscheck.yml @@ -65,6 +65,16 @@ jobs: - name: Build flang run: make -C bootstrap -j4 + # Каждый приём `шаг_вывода` сверщика либо в приёмке Lean, либо строкой + # долга с номером задачи (ADR-0064): иначе теоремы состоятельности у него + # нет, а сверка ниже молча считает его «вне приёмки». Н6 и О9 прожили так + # девять дней (26 сентября — 5 октября 2026), пока число 81 переписывалось + # в прозе от руки. Lean этому шагу не нужен; подлог — три порчи копий. + - name: Every checker move has a theorem or a debt row + run: | + bootstrap/flang run-script lean-rules:forgery + bootstrap/flang run-script lean-rules:check + # ПОЧЕМУ ЗДЕСЬ FLANG_TMP. План просит временный каталог по образцу # «FLANG_TMP, а если переменной нет — /srv/tmp». `/srv/tmp` есть на машине # разработки и нет у работника, поэтому на работнике каталог не заводился From e4260dee0758f2af6decf7d4461ab644d242fe0e Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Mon, 5 Oct 2026 21:14:46 +0000 Subject: [PATCH 4/8] docs(proof): the move ledger, adr-0064, task 4791 and a zettel 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. --- ...-has-a-lean-theorem-or-a-named-debt-row.md | 108 ++++++++++++ docs/flang/proof/tables.md | 17 +- docs/lean-checks-the-inference-rules.md | 6 + docs/road-to-1-0.md | 6 +- ...ecker-evaluator-or-proves-why-it-cannot.md | 2 +- ...the-body-by-lines-and-stay-outside-lean.md | 96 +++++++++++ docs/zettel/README.md | 161 +++++++++--------- ...rem-while-the-count-was-written-by-hand.md | 39 +++++ 8 files changed, 351 insertions(+), 84 deletions(-) create mode 100644 docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md create mode 100644 docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md create mode 100644 docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md diff --git a/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md new file mode 100644 index 000000000..b0f7e43b6 --- /dev/null +++ b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md @@ -0,0 +1,108 @@ +# ADR-0064. У каждого приёма проверяющей программы есть теорема состоятельности в Lean либо строка долга с номером задачи, и это стережёт прибор, а не проза + +**Состояние:** предложено. Принимает владелец. +**Дата:** 5 октября 2026. +**Основание:** строка «состоятельность последних правил» таблицы «Доказывалка +против Lean» в `docs/road-to-1-0.md` и задача 1183: теорема есть не для всех +приёмов сверщика, а сколько их и какие — считалось от руки. +**Замер:** ветка `a/checker-rules-are-sound-in-lean` от `origin/dev` `6b459ded0`, +двоичный `bootstrap/flang` 0.7.24 из этого же дерева, Lean 4.34.1 по +`flang/proof/lean/lean-toolchain`. Числа сняты прогонами 5 октября 2026; где +прогона нет, стоит «не мерено». +**Рядом:** [ADR-0041](0041-the-checker-is-proven-sound-against-a-mechanised-semantics.md) — +обещание состоятельности сверщика против модели, которое этот документ делает +проверяемым прибором; [ADR-0042](0042-the-last-places-of-the-corpus.md) — последнее +расширение приёмки, после которого число приёмов считалось вручную. +**Новые задачи:** 4791. + +--- + +## 1. Задача + +Сверщик (`flang/proof/checker/checker.c`) принимает блок «вывод» по закрытому +списку приёмов `шаг_вывода`. Приёмка Lean (`flang/proof/lean/Acceptance.lean`) +держит свой закрытый список `«правила»`, и теорема «состоятельность» +(`Consistency.lean`) доказана ровно для него. Между двумя списками до сих пор +стояла проза: «приёмов 81, покрыто 76» — в шапках `Acceptance.lean` и +`Consistency.lean`, в `docs/road-to-1-0.md`, в задаче 1183. + +26 сентября 2026 задача 1435 добавила в сверщик два приёма — Н6 (выбор +неотрицателен, когда неотрицательны обе ветви) и О9 (свёртка от нуля шагом не +больше единицы не обгоняет длину списка). В приёмку Lean они не попали, в прозу +тоже; ночная сверка `lean-crosscheck.yml` честно считала их блоки «вне приёмки» +(задача 1183, прогон 2 октября: О9 — 7 блоков, Н6 — 5), но «вне приёмки» читается +как известный долг, а не как новая дыра. Девять дней у двух приёмов сверщика не +было теоремы, и ни одна проверка не краснела. + + +Замер прибором 5 октября, до правки приёмки: приёмов 83, в приёмке 76, вне +приёмки 7 (Р2, Р3, Р5, Р6, Выч и те самые Н6, О9). + +## 2. Решение + +1. **Список приёмов снимается с кода, а не пишется.** Прибор + `flang/proof/lean/rules-guard.fscript` читает `шаг_вывода` сверщика (каждое + сличение имени между первым именованным приёмом и читателем шага), список + `«правила»` приёмки, имена теорем `Rules.lean` и `Term.lean` и печатает + перепись: приём — лемма ведомости — приёмка — долг (план `Census`), пять чисел + одной строкой (план `Numbers`). +2. **Долг — таблица, а не абзац.** `flang/proof/tables/lean-acceptance-debt.tsv`: + имя приёма, номер задачи, причина. Приём без теоремы законен только строкой + здесь. Устройство — в `docs/flang/proof/tables.md`. +3. **Сторож краснеет в обе стороны** (план `Check`, ярлык `lean-rules:check`): + приём сверщика без приёмки и без строки долга; строка долга о приёме, который + в приёмке уже есть («долг уплачен — строку снять»); строка долга или правило + приёмки об имени, которого сверщик не ведёт; приём без леммы в `Rules.lean` и + `Term.lean`; разбор, вычитавший меньше пятидесяти имён с любой стороны. +4. **Отрицательный контроль встроен** (план `Forgery`, ярлык `lean-rules:forgery`): + три порчи КОПИЙ — из приёмки убрано правило Н5, в сверщик дописан приём без + теоремы, в долг вписан принятый приём; каждая обязана покраснеть, и прогон + печатает «СОШЛОСЬ» либо «ПРОВАЛ» поимённо. +5. **Зовут его на каждый пуш**, а не ночью: работа `lean-rules-guard` в + `.github/workflows/ci.yml` (Lean сторожу не нужен) и шаг в + `lean-crosscheck.yml` перед сверкой вердиктов, чтобы ночной отчёт не называл + новую дыру старым долгом. +6. **Н6 и О9 входят в приёмку** этим же решением: Н6 — через «Н6-терм» + (`Term.lean`), О9 — через «О9-под-порогом» (`Rules.lean`: шаг меры точен под + порогом округления, список короче порога) и новый факт окружения + «списки-коротки» (`Record.lean`: всякое имя-список короче 2⁵³ элементов — так в + языке, модель этого сама не знала). Ловушки 85 и 86 (`Trap.lean`) — О9 с шагом в + двойку и Н6 без второй посылки — Lean обязан отвергнуть. + +## 3. Замер после правки + + +`bootstrap/flang run-script lean-rules:numbers`: приёмов 83, с леммой 83, в +приёмке Lean 78, вне приёмки 5, в долге 5. `lean-rules:check` зелен; +`lean-rules:forgery` — три подлога, пойманы три. `Consistency.lean`: +`«покрыто-число» : «покрыто» = 78` проверено `decide`; аксиомы теоремы +«состоятельность» — три стандартные. Сборка цепочки Lean на машине +разработки: `Term.lean` 51 с, `Acceptance.lean` 16 с, `Consistency.lean` 20 с. + +Пять приёмов остаются долгом, и причина у каждого названа в таблице: Выч — +второй вычислитель языка внутри сверщика (задача 1183); Р2, Р3 — посылками берут +только шаги Выч, а своя лемма требует подстановки без захвата (задача 4791); Р5, +Р6 — тело функции читается по строкам, читатель записи многострочного тела не +собирает (задача 4791). + +## 4. Последствия + +- Число «приёмов N, покрыто M» в прозе больше не пишется от руки: его печатает + `lean-rules:numbers`, и в документах оно стоит с приметой `СНЯТО`. +- Новый приём сверщика без теоремы ломает `ci.yml` на том же пуше. Обойти можно + только строкой долга — с номером задачи, то есть вслух. +- Приёмка Lean теперь строже сверщика ещё в одном месте (О9: список — имя, шаг — + литерал не выше 1, левая сторона — голая свёртка); это названо тринадцатым + пунктом шапки `Acceptance.lean` и остаётся кандидатом в расхождение вердиктов, + которое ловит ночная сверка. + +## 5. Отвергнутые пути + +- **Держать долг в шапке `Acceptance.lean`.** Так и было; прозу никто не сличает + с кодом, и она отстала на два приёма за девять дней. +- **Снимать список приёмов с таблицы `inference-rules.tsv`.** В таблице 112 + строк, из них правил и запретов больше, чем приёмов сверщика (О7, Н11, Р7, Инд, + Тожд, Св читаются ядром узлом, а не шагом); сличать надо то, что сверщик + действительно принимает, — его `шаг_вывода`. +- **Гонять сторож только ночью вместе со сверкой.** Сверке нужен Lean и двадцать + минут; сторожу — три файла и секунды, и красный на пуше дешевле красного утром. diff --git a/docs/flang/proof/tables.md b/docs/flang/proof/tables.md index f20ef06de..91e8f81f7 100644 --- a/docs/flang/proof/tables.md +++ b/docs/flang/proof/tables.md @@ -1,6 +1,6 @@ # Таблицы доказательного слоя: `flang/proof/tables/` -Четыре таблицы, у каждой первая строка — заголовок, разделитель — табуляция, +Пять таблиц, у каждой первая строка — заголовок, разделитель — табуляция, комментариев нет. Их читают программы; прозу о строках держат страницы `docs/`. ## `inference-rules.tsv` — правила вывода @@ -54,6 +54,21 @@ sha256sum flang/proof/tables/inference-rules.tsv | cut -d' ' -f1 > flang/proof/t Читает `scripts/guards/kernel-abilities-guard.fscript`: ядро, описание и улики обязаны сходиться на каждой строке. +## `lean-acceptance-debt.tsv` — приёмы сверщика без приёмки Lean + +| колонка | что в ней | +|---|---| +| `name` | имя приёма `шаг_вывода` проверяющей программы на C (Выч, Р5, …) | +| `task` | номер задачи, которая этот долг закрывает | +| `reason` | почему приёма нет в `flang/proof/lean/Acceptance.lean`, одной строкой | + +Читает `flang/proof/lean/rules-guard.fscript` (ярлыки `lean-rules:check`, +`lean-rules:census`, `lean-rules:numbers`, `lean-rules:forgery`; ADR-0064): каждый +приём сверщика обязан стоять либо в закрытом списке `«правила»` приёмки, либо +строкой здесь; строка о приёме, который в приёмку уже вошёл или которого в сверщике +нет, красит сторож так же, как приём без строки. Список закрытый в обе стороны: +«долг уплачен» видно по красному, а не по памяти. + ## `consistency-violations.tsv` — известные нарушения состоятельности Колонки `key` и `state` (`open` либо `closed`); что стоит за каждым именем — diff --git a/docs/lean-checks-the-inference-rules.md b/docs/lean-checks-the-inference-rules.md index 5d76195af..7ad8acff5 100644 --- a/docs/lean-checks-the-inference-rules.md +++ b/docs/lean-checks-the-inference-rules.md @@ -19,6 +19,12 @@ > машине не повторён: `lean` не установлен, `run.sh` отвечает кодом 2 «НИЧЕГО НЕ > ПРОВЕРЕНО». Числа §1 (78 / 77) — снимок 9–10 сентября (`729b29799`). +> **Сверка 5 октября 2026** (ADR-0064, `bootstrap/flang run-script lean-rules:numbers`): +> приёмов `шаг_вывода` у сверщика **83**, с леммой в `Rules.lean`/`Term.lean` — 83, в +> приёмке Lean — **78**, вне приёмки — 5, и все пять стоят строками долга в +> `flang/proof/tables/lean-acceptance-debt.tsv`. +> Число снимает прибор `flang/proof/lean/rules-guard.fscript`, а не рука. + Проверялись ПРАВИЛА, а не записи доказательств. Правил конечное число, и каждая запись собрана из них: если правило несостоятельно, рушится всё, что на нём стоит. diff --git a/docs/road-to-1-0.md b/docs/road-to-1-0.md index 658ba082a..00b7ea1bc 100644 --- a/docs/road-to-1-0.md +++ b/docs/road-to-1-0.md @@ -118,7 +118,9 @@ Homebrew с тем, что собрал сам конвейер выпуска; **15 сент, позже** (задача 1130; `sh flang/proof/lean/run.sh`, ветка `a/lean-o6-ch5-representable-and-number-text`): **теорема о состоятельности есть для 76 правил из 81** — прибавились О6 (окружение знает факт языка «числа-представимы») и Ч5 (модель терма переводит число в текст). Сверка вердиктов (508 подделок, 237 честных; 242 пары, 1503 блока): расхождений 0; вне приёмки 91 блок — Выч, Р5, Р6 и запреты; ловушек 37 из 37. К↑ и Разв3 Lean теперь судит в самом прогоне — проба `развёртка/box-round-trip-by-assumption` с базой Т1. -**Чего нет.** Теоремы для пяти приёмов из 81 — Выч, Р2, Р3, Р5, Р6 — и для Разв1 по строке тела (причины — в шапке `Acceptance.lean`, задачи 1130, 4058, 6432). Теоремы о самом `checker.c`: код с моделью связан сверкой вердиктов на наборе, а не выводом. Модель значений округляет «грубо», не по binary64, и её совпадение с вычислителем не доказано (ADR-0041 §2.3). Чтение текста записи (`flang/proof/lean/RecordReader.lean`) стоит вне теоремы. +**5 окт** (задача 1435 → ADR-0064; `bootstrap/flang run-script lean-rules:numbers`, ветка `a/checker-rules-are-sound-in-lean`): приёмов `шаг_вывода` у сверщика **83**, а не 81 — Н6 и О9 вошли в сверщик 26 сентября (задача 1435) и девять дней не имели теоремы, пока число 81 переписывалось в прозе от руки. **Теорема о состоятельности есть для 78 приёмов из 83**: Н6 и О9 вошли в приёмку (`Acceptance.lean`, `Consistency.lean`; О9 — под фактом окружения «списки-коротки» в `Record.lean`), ловушек стало 55 файлов-искажений (две новые: 85 — О9 с шагом в двойку, 86 — Н6 без второй посылки). Пять приёмов без теоремы — Выч, Р2, Р3, Р5, Р6 — стоят строками долга в `flang/proof/tables/lean-acceptance-debt.tsv` с номером задачи (1183, 4791); сторож `flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, работа `lean-rules-guard` в `ci.yml` и шаг в `lean-crosscheck.yml`) краснеет на приёме без приёмки и без строки долга, на уплаченном долге и на имени, которого нет у сверщика; три подлога на копиях (`lean-rules:forgery`) пойманы все три. + +**Чего нет.** Теоремы для пяти приёмов из 83 — Выч, Р2, Р3, Р5, Р6 (строки долга, задачи 1183 и 4791) — и для Разв1 по строке тела (причины — в шапке `Acceptance.lean`, задачи 1130, 4058, 6432). Теоремы о самом `checker.c`: код с моделью связан сверкой вердиктов на наборе, а не выводом. Модель значений округляет «грубо», не по binary64, и её совпадение с вычислителем не доказано (ADR-0041 §2.3). Чтение текста записи (`flang/proof/lean/RecordReader.lean`) стоит вне теоремы. **Как узнаем, что взято.** Названо утверждение о состоятельности ядра, и оно доказано — не пробами, а выводом. @@ -268,7 +270,7 @@ Homebrew с тем, что собрал сам конвейер выпуска; | **квантор внутри формулы и существование без свидетеля** | кванторы — обычные термы, вкладываются свободно | оба квантора связывают только цель целиком; существование требует названного свидетеля | задачи 1177, 1188 | разбор + ядро; **перепечатка семени** | | **законы кольца** | `ring` | доказывается только перестановка операндов одного узла | задача 1412 | правила на точном целом (задача 1908); **перепечатка семени** | | **суд над категорной поверхностью** | классы типов с законами, проверяемыми как теоремы | моноиды, монады, функторы и блоки `закон` не судятся, код 2 | задачи 6752, 9963 | ядро + поверхность; **перепечатка семени** | -| **состоятельность последних правил** | ядро Lean мало и проверено само | теорема есть не для всех приёмов сверщика; что не покрыто — пункт 3 выше | задача 1183 | только `flang/proof/lean/**` — **перепечатки НЕ требует** | +| **состоятельность последних правил** | ядро Lean мало и проверено само | теорема есть для 78 приёмов сверщика из 83 ; пять без теоремы названы строками долга, сторож `lean-rules:check` не даёт появиться шестому молча — пункт 3 выше | задачи 1183, 4791; ADR-0064 | только `flang/proof/lean/**` — **перепечатки НЕ требует** | | **вторая реализация сличителя** | `lean4lean`, `lean4export` — чужие перепроверяющие | сличитель один, и его пробы написал его же автор | задача 1313 | только `flang/proof/checker/**` — **перепечатки НЕ требует** | Почему «перепечатка семени» — это цена, а не сноска: правка под `flang/self/**` diff --git a/docs/tasks/1183-lean-models-the-checker-evaluator-or-proves-why-it-cannot.md b/docs/tasks/1183-lean-models-the-checker-evaluator-or-proves-why-it-cannot.md index 4b59c7a29..b6036f7db 100644 --- a/docs/tasks/1183-lean-models-the-checker-evaluator-or-proves-why-it-cannot.md +++ b/docs/tasks/1183-lean-models-the-checker-evaluator-or-proves-why-it-cannot.md @@ -7,7 +7,7 @@ ветка: — команда: первая карта: Сколько доказано на самом деле -рядом: 1130, 3449, 3448 +рядом: 1130, 3449, 3448, 4791 нужность: шаги «Выч» принимает вычислитель внутри проверяющей программы, и его состоятельность моделью Lean не покрыта --- diff --git a/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md new file mode 100644 index 000000000..b2f3c5818 --- /dev/null +++ b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md @@ -0,0 +1,96 @@ +--- +номер: 4791 +заголовок: Приёмы Р5 и Р6 читают тело функции по строкам, и приёмка Lean их не судит; Р2 и Р3 судятся только через Выч +статус: свободна +приоритет: P2 +исполнитель: — +ветка: — +команда: первая +карта: Сколько доказано на самом деле +рядом: 1183, 1435 +нужность: пять приёмов сверщика стоят строками долга в flang/proof/tables/lean-acceptance-debt.tsv, и долг гасится только теоремой +--- + +# 4791. Приёмы Р5 и Р6 читают тело функции по строкам, и приёмка Lean их не судит; Р2 и Р3 судятся только через Выч + +## Шаги воспроизведения + +1. Спросить дерево, какие приёмы `шаг_вывода` проверяющей программы стоят вне + приёмки Lean: + +``` +bootstrap/flang run-script lean-rules:census +``` + +2. Смотреть строки с пометкой «долг» в третьей колонке и строку «вне приёмки». + +## Что происходит + +``` +$ bootstrap/flang run-script lean-rules:numbers +приёмов 83, с леммой 83, в приёмке 78, вне приёмки 5, в долге 5 код 0 +``` + + + +Версия: flang 0.7.24, Lean 4.34.1. Дата прогона: 5 октября 2026, ветка +`a/checker-rules-are-sound-in-lean`. + +Вне приёмки — Выч, Р2, Р3, Р5, Р6. Выч ведёт задача 1183 (вычислитель половин +внутри проверяющей программы). Остальные четыре — здесь: + +- **Р5, Р6** (пустота списка отдаёт ветвь «случай пусто» либо начало свёртки): + проверяющая программа читает тело функции ПО СТРОКАМ — `блок_функции`, + `строка_разбора`, `найти_случай`, `тело_случая`, `тело_функции_текст` + (`flang/proof/checker/checker.c`, `семейство_р`). Читатель записи + `flang/proof/lean/RecordReader.lean` собирает тело только одной строкой + (`«Функция».«тело»`), многострочный `разбор` с ветвями в терм не собирает. + Цена по графу вызовов (15 сентября 2026): 41 функция и 350 строк C, из них + 29 функций общие с вычислителем половин. +- **Р2, Р3** (условие В, подставленное в Ф литералами «да» и «нет», даёт две + половины): посылками проверяющая программа берёт ТОЛЬКО шаги Выч, и пока Выч + вне приёмки, блок с Р2/Р3 всё равно упирается в Выч. Сама же лемма приёма — + «обе половины истинны, значит истинна Ф» — требует в модели поиска куска В по + первому расхождению и подстановки без захвата; у проверяющей программы + подстановка текстовая (`вставить_вместо`) и о связывателях над В она не + спрашивает. + +## Что должно быть + +Каждый приём `шаг_вывода` — с теоремой состоятельности в Lean (ADR-0041 §2.1, +ADR-0064). Для четырёх приёмов это значит: + +- Р5, Р6 — читатель записи собирает многострочное тело (`разбор Л` с ветвями + «случай пусто» / «случай голова и хвост», `свёртка Л начиная с Н как …` первой + строкой), в модели есть разбор списка списочного сорта, и приёмка принимает + шаг «результат равен Т» при факте пустоты того же списка; +- Р2, Р3 — приёмка восстанавливает В из первого расхождения разобранных деревьев + Ф и о1, проверяет, что В не стоит под связывателем, связывающим его свободное + имя, и что замены В на «да» и «нет» дают о1 и о2; лемма — разбор случаев по + значению В в мире. Приёмка здесь строже проверяющей программы (она захвата не + спрашивает), и это надо назвать в шапке `Acceptance.lean`. + +Либо, если цена названа и решено не платить, — строка долга остаётся, а в ADR +стоит довод с числом строк Lean. + +## Обходной путь + +Обхода нет: шаги Р2, Р3, Р5, Р6 сверяются только самой проверяющей программой. + +## Когда задача сделана + +`bootstrap/flang run-script lean-rules:check` зелен при пустых строках долга на +Р5 и Р6 (а при закрытии 1183 — и на Р2, Р3); строки из +`flang/proof/tables/lean-acceptance-debt.tsv` сняты, иначе сторож краснеет +словами «долг уплачен — строку долга снять». В +`bootstrap/flang io flang/proof/lean/run.fscript` число «вне приёмки» падает на +блоки этих приёмов (на 2 октября 2026 — Р5 24, Р6 7), расхождений 0, ловушки на +новые приёмы отвергнуты. + +## Где живёт правка + +`flang/proof/lean/RecordReader.lean` — сборка многострочного тела; +`flang/proof/lean/Term.lean`, `Model.lean` — разбор списка в модели; +`flang/proof/lean/Acceptance.lean`, `Consistency.lean` — приёмы и случаи теоремы; +`flang/proof/lean/Trap.lean` — ловушки; `flang/proof/tables/lean-acceptance-debt.tsv` +— снять строки. Двоичное не меняется, перепечатка семени не нужна. diff --git a/docs/zettel/README.md b/docs/zettel/README.md index 9ecfe2999..35e5deeb3 100644 --- a/docs/zettel/README.md +++ b/docs/zettel/README.md @@ -28,7 +28,6 @@ ## Числа -- [Ядро читает условие ветвления, только когда утверждение ветвится так же, как тело](the-kernel-reads-a-branch-condition-only-when-the-claim-branches-the-same-way.md) - [У double ломается ассоциативность, а равенство даже не рефлексивно](double-has-no-laws.md) - [Точные десятичные стоят ноль, а не в сто раз дороже](exact-decimals-are-free.md) - [Вопрос не «точно или приблизительно», а «точно в какой системе счисления»](exact-in-which-base.md) @@ -37,15 +36,17 @@ - [Счётчик типа `нат` внутри записи написать нельзя, и это меняет устройство программы, а не одну строку](nat-counter-in-a-record-is-unwritable.md) - [Числа описываются категорией, но категория не вычисляет](numbers-as-a-category.md) - [Доказано 8147 обязательств дерева из 13341 написанных — 61,1 %; снято одним двоичным за один заход, доля файла отделена от доли ввоза, и на 2072 обязательств приговора нет вовсе](one-binary-one-ledger-the-whole-tree.md) +- [Ядро читает условие ветвления, только когда утверждение ветвится так же, как тело](the-kernel-reads-a-branch-condition-only-when-the-claim-branches-the-same-way.md) - [Языку нужны три типа чисел с разными гарантиями](three-number-types.md) ## Доказательства - [Обещание о ВЕТВИ тела ядро берёт там, где обещание о функции целиком не берётся](a-branch-promise-is-what-the-kernel-can-take-when-the-whole-promise-is-not.md) -- [Силлогизм доказывается из допущений сегодняшним ядром, а русские предложения читаются без словаря морфологии](premises-as-assumptions-prove-a-syllogism-without-a-morphology-dictionary.md) - [Ядро подставляет равенство вызванной, но не ослабляет её неравенство: «не больше одного» у помощника не доказывает «не больше чем на один длиннее» у зовущего](a-callee-promise-reaches-the-handler-through-seven-branches-not-fifteen.md) - [Про значение объявленной суммы в постусловии нельзя сказать ничего: ни сравнить, ни разобрать](a-declared-sum-cannot-be-spoken-about-in-a-postcondition.md) +- [Дизъюнкция в допущении разбирается СЛУЧАЯМИ, а расщеплять её нельзя ни в какую сторону](a-disjunction-in-a-hypothesis-is-split-by-cases-not-torn-apart.md) - [Сумма трёх слагаемых в тексте — это вложенная сумма в дереве, и записывать ход про неё нельзя](a-flat-sum-in-text-is-a-nested-sum-in-the-tree.md) +- [Даровое утверждение узнаётся подменой тела заглушкой, и в двух модулях библиотеки таких оказалось 17 из 32](a-free-statement-is-exposed-by-replacing-the-body-with-a-stub.md) - [Охрана меняет истинность и не меняет доказуемость: стена стоит до неё](a-guard-changes-truth-not-provability.md) - [Список стен, переписанный руками из отчёта в отчёт, устарел на две трети: из 24 записанных «ядро не берёт» держатся 9](a-hand-copied-wall-list-goes-stale-in-silence.md) - [Новая форма языка, не доехавшая до генераторов кода, расходится с типами молча — и вылезает у того, кто собирает двоичное](a-language-form-must-reach-code-generation.md) @@ -68,15 +69,11 @@ - [Замкнутую цель надо считать, а не выводить: 50 доказательств без единого нового правила](closed-goals-must-be-computed.md) - [Постоянные в цели можно складывать только вокруг ОДНОЙ длины: вокруг произвольного числа это ложь на 10¹⁶](constants-in-a-goal-fold-only-around-one-length.md) - [Сила Coq не в ядре, а в библиотеке доказанных лемм](coq-strength-is-in-its-lemmas.md) -- [Даровое утверждение узнаётся подменой тела заглушкой, и в двух модулях библиотеки таких оказалось 17 из 32](a-free-statement-is-exposed-by-replacing-the-body-with-a-stub.md) -- [Дизъюнкция в допущении разбирается СЛУЧАЯМИ, а расщеплять её нельзя ни в какую сторону](a-disjunction-in-a-hypothesis-is-split-by-cases-not-torn-apart.md) -- [Два правила завершаемости поодиночке дают 54 и 74, а вместе — 574: узкое место в их произведении](two-termination-rules-together-give-574.md) - [Зазор между двумя печатями в C ловится только пятиминутной сборкой, и на файлах `self/` не ловится вовсе](emitter-twin-gap-is-only-caught-by-a-five-minute-build.md) - [Запрет равенства в теле оказался засидевшимся, а не границей: довод «запрет держит цену видимой» падает от двух прогонов, а спека языка требовала обратного](equality-in-a-body-was-a-stale-restriction-not-a-boundary.md) - [Равенство над параметром типа запрещено только в ТЕЛЕ: в утверждении оно разрешено, и упирается в него девять мест, а не вся библиотека](equality-on-a-type-parameter-is-banned-only-in-bodies.md) - [Условие цели ядро сличает с условием тела ЗНАК В ЗНАК — равносильная запись не считается](goal-condition-must-match-body-condition-sign-for-sign.md) - [Тело-«если» получило посылку индукции, и это дало по библиотеке ноль](if-bodies-get-induction-but-assertions-still-block.md) -- [Индукция по строке закрыла ОДНО утверждение на весь корпус, а не сотню: за стеной стоит вторая](string-induction-closed-one-statement-not-a-hundred.md) - [Свёртка в flang левая, поэтому индукцию по списку к ней прицепить нельзя — и это свойство свёртки, а не пробел ядра](left-fold-gives-no-list-induction.md) - [Библиотека доказана на 63 %: 2786 → 3630, и оба числа сняты прогоном, а не сложены из чужих отчётов](library-proof-ledger.md) - [Зеркало допущений закрыло пробу и не закрыло ни одного обещания библиотеки](mirroring-assumptions-costs-nothing-and-gave-nothing.md) @@ -86,6 +83,7 @@ - [Три файла компилятора обещают 788 раз, недоказанных 220, и треть из них держит ОДИН ход — деление цели по `разбор`](one-move-holds-a-third-of-what-three-compiler-files-promise.md) - [Перенесённое правило состоит из ТРЁХ частей: самого правила, места вызова и текста отказа](porting-a-rule-means-porting-its-refusal-text.md) - [Постусловие вычисляется и при вложенных вызовах, поэтому граф «кто кого называет» обязан быть без циклов — и часть функций сказать о себе не может вовсе](postcondition-runs-on-nested-calls-so-some-functions-cannot-be-stated-about.md) +- [Силлогизм доказывается из допущений сегодняшним ядром, а русские предложения читаются без словаря морфологии](premises-as-assumptions-prove-a-syllogism-without-a-morphology-dictionary.md) - [Цена доказательства измерена: 0 из 20, и тесты нашли четыре ошибки против нуля](proof-cost-0-of-20.md) - [Поиск доказательства не должен ничему верить — тогда его можно делать сколь угодно наглым](proof-search-must-trust-nothing.md) - [Файл, записанный на четырёх поверхностях, доказательство нести не может](proof-words-live-on-two-surfaces-of-four.md) @@ -99,6 +97,7 @@ - [Цель, разложенная по исходам сравнения, доказывается там, где та же цель с оговоркой остаётся сеткой](splitting-a-goal-by-comparison-outcome-beats-a-guarded-goal.md) - [Строгое «больше» в цели ядро берёт, если написать его целочисленно: «Е плюс 1 не больше Г»](strict-greater-is-taken-as-plus-one-not-greater.md) - [Спуск по строке в библиотеке пишут свёрткой по знакам, а не разбором — принцип строки к таким телам не цеплялся](string-descent-is-written-as-a-fold-over-characters.md) +- [Индукция по строке закрыла ОДНО утверждение на весь корпус, а не сотню: за стеной стоит вторая](string-induction-closed-one-statement-not-a-hundred.md) - [Содержательных доказанных утверждений пишется много, если выбирать не правило ядра, а ФОРМУ утверждения: 53 из 53 в корпусе спек](substantive-claims-are-provable-when-you-pick-the-shape.md) - [Тавтология закрывается даром, поэтому число «доказано без теоремы» само по себе ничего не значит](tautologies-close-for-free.md) - [Терм в сверщике можно держать строкой, потому что flang скобит каждую двуместную форму](terms-as-strings-work-because-flang-parenthesises-every-binary-form.md) @@ -107,15 +106,17 @@ - [Доказали самое видное утверждение сортировки — цена при работе не сдвинулась: платит не оно](the-guard-that-costs-the-time-is-not-the-one-you-proved.md) - [Заключение посылки — это уже развёрнутое тело ветви, поэтому первый ход записи ядру ничего не стоит](the-premise-goal-is-already-the-unfolded-body-so-the-first-move-is-free.md) - [Доказанное постусловие при `flang test` стоит не прогона, а ВТОРОГО прохода ядра по всем утверждениям модуля — и потому снимать его в проверке нечего и нельзя](the-price-of-a-proved-claim-is-one-extra-kernel-pass.md) -- [Прослеживаемость собирается из того, что уже лежит в дереве: постусловие, пример и запись доказательства сшиваются по трём ключам, и разрывов сегодня 62 и 68](traceability-is-a-join-over-files-that-already-exist.md) - [Три факта о длине строки дали три утверждения на весь корпус, и самым дорогим из трёх был не факт, а место, где факт читается](three-length-facts-gave-three-statements.md) +- [Прослеживаемость собирается из того, что уже лежит в дереве: постусловие, пример и запись доказательства сшиваются по трём ключам, и разрывов сегодня 62 и 68](traceability-is-a-join-over-files-that-already-exist.md) - [Отказ «инстанцировано на 2 вызовах» держит не `пусть`-имя, а тело вызванной: с телом-`разбор` он остаётся, с телом, которое ядро сводит, — исчезает](two-calls-refusal-is-about-the-callee-body-not-the-let-name.md) +- [Два правила завершаемости поодиночке дают 54 и 74, а вместе — 574: узкое место в их произведении](two-termination-rules-together-give-574.md) - [Невысказываемое утверждение дороже недоказуемого](unstatable-costs-more-than-unprovable.md) - [Ветвь `разбор` по варианту без полей берётся равенством варианту, а `не результат` на такой ветви — нет](variant-equality-opens-a-case-branch.md) - [Равенство варианту открывает ветвь `разбор` только тогда, когда ветвь — прямой терм](variant-equality-opens-a-match-branch-only-when-the-branch-is-a-direct-term.md) - [Вывод, снятый на одной ветке, — не вывод о дереве](vyvod-na-vetke-ne-vyvod-o-dereve.md) - [Узкое место переехало четвёртый раз: теперь мешает индукция, которую негде объявить](what-blocks-the-kernel-now-is-induction-without-a-theorem.md) - [Ноль аксиом — проверяемое свойство, а не лозунг](zero-axioms.md) +- [Два приёма сверщика девять дней стояли без теоремы состоятельности, потому что число приёмов «81» переписывалось в прозе от руки](two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md) ## Теория категорий @@ -166,9 +167,12 @@ - [Веер запусков двоичного помещается в ОДНО поручение плана — через `sh -c`](a-fan-out-of-binary-runs-fits-one-io-order-through-sh.md) - [Рост встроенной суммы «Отклик» не красит старый разбор `случай`ами, пока семя не перепечатано, и единственный обход, который бы это поймал, идёт только по тегу](a-grown-builtin-sum-stays-silent-until-the-seed-reprints.md) - [Пропавший узел объявляется мёртвым, а его работу забирает выживший — и две живые копии при этом не гипотеза, а снятое число](a-node-that-vanishes-is-declared-dead-and-its-work-is-taken-over.md) +- [Постусловие о сбое доказуемо для конкретного отклика и не пишется для всякого](a-postcondition-about-failure-is-provable-for-one-reply-not-for-any.md) +- [Обещание с условием «аргумент равен вариант» разворачивает ветвь `разбор`а](a-promise-conditioned-on-a-variant-unfolds-the-case-branch.md) - [Обход дерева надзора написан свёрткой, потому что взаимная рекурсия четырёх функций завершения не доказывает](a-supervisor-tree-walk-folds-because-mutual-recursion-is-not-provable.md) - [Значение flang переживает данные, из которых собрано, — и в C это ловится только прогоном](a-value-outlives-the-data-it-was-built-from.md) - [Асинхронный `connect` рвёт связь, не дав ей завестись, если сокет назначен каналу раньше события «Сокет завёлся»](an-async-connect-tears-the-link-before-it-is-made.md) +- [Ветка `если` разворачивается в обе стороны и на второй ярус, а `разбор` списка — ни в какую](an-if-branch-unfolds-both-ways-a-list-case-does-not.md) - [BEAM не обходит операционную систему, и C зависит от неё ровно так же](beam-does-not-bypass-the-os.md) - [Оценку витков нельзя ввезти ни в один слой компилятора: имена совпадают, а переименования при ввозе в языке нет](boundedness-cannot-be-imported.md) - [Постусловие на обработчике заводит восьмой вид отказа мимо замкнутого множества](handler-postcondition-escapes-the-closed-set.md) @@ -185,14 +189,11 @@ - [Надзор не удалось ввезти из `flang/self/conc.flang`: тот модуль не проходит проверку, и виноват один встроенный](supervision-could-not-be-imported-because-its-module-does-not-compile.md) - [Тексты рантайма двоичный читает ИЗ ДЕРЕВА при печати, а не несёт в себе](the-binary-reads-its-runtime-texts-from-the-tree.md) - [Цена хозяина узла считается по ТРЁМ осям, а не по одной](the-host-price-has-three-axes-not-one.md) +- [Оценка витков и счётчик шагов рантайма считают разное под одним словом](the-loop-estimate-and-the-runtime-step-counter-count-different-things.md) - [Синхронный планировщик умеет ждать сеть, не останавливаясь: «ждать» — это «спросить и не получить письма»](the-scheduler-waits-for-the-network-without-stopping.md) - [Пару живых узлов на проводе словарь поручений не поднимет: «Запустить процесс» ждёт конца, и всё же одна оболочка это делает](two-live-nodes-on-a-wire-need-a-shell-because-orders-run-one-process-at-a-time.md) - [Типизированная ссылка на процесс выражается сегодняшним языком без единой правки компилятора, и подделка с чужим грузом отвергается](typed-process-reference-is-already-expressible.md) - [Из четырёх утверждений, которых ждут от планировщика процессов, ядро не берёт ни одного — и причина у каждого своя](what-a-scheduler-needs-proved.md) -- [Ветка `если` разворачивается в обе стороны и на второй ярус, а `разбор` списка — ни в какую](an-if-branch-unfolds-both-ways-a-list-case-does-not.md) -- [Обещание с условием «аргумент равен вариант» разворачивает ветвь `разбор`а](a-promise-conditioned-on-a-variant-unfolds-the-case-branch.md) -- [Оценка витков и счётчик шагов рантайма считают разное под одним словом](the-loop-estimate-and-the-runtime-step-counter-count-different-things.md) -- [Постусловие о сбое доказуемо для конкретного отклика и не пишется для всякого](a-postcondition-about-failure-is-provable-for-one-reply-not-for-any.md) ## Самораскрутка и метод проверки @@ -202,6 +203,7 @@ - [Порча попадает туда, где считают, только если корпус сверки доходит до каталога с единственным случаем](a-corruption-lands-only-where-the-corpus-reaches.md) - [Объявленный и ни разу не вызванный список — это обещание без исполнителя, и комментарий над ним читается как гарантия](a-declared-and-never-called-list-is-a-promise-with-no-executor.md) - [Приставка семейства в прозе (`FLANG_MONOID_*`) — не имя кода, и сторож кодов теперь это различает](a-family-prefix-in-prose-names-a-family-not-a-code.md) +- [Быстрый пересев семени законен ровно тогда, когда замыкание и пределы не тронуты относительно отпечатка](a-fast-reseed-is-legal-only-while-the-closure-and-limits-match-the-stamp.md) - [Сторож подделок обязан принимать код 3: с 0.7.17 «объявлено, не доказано» — это код возврата, а не только строка отчёта](a-forgery-guard-must-accept-exit-code-three.md) - [Вторую сторону сверки можно заморозить, но проверка при этом меняет род, и это надо назвать вслух](a-frozen-reference-changes-the-check.md) - [Имя порождённого файла чинится в имени модуля, а не в генераторе кода](a-generated-file-name-is-fixed-in-the-module-name.md) @@ -210,18 +212,22 @@ - [Пульс, чей `trap` на TERM не выходит, переживает веер и держит план `flang io` без конца](a-heartbeat-whose-term-trap-does-not-exit-hangs-the-plan-forever.md) - [Работа CI останавливается на первом красном шаге и скрывает остальные — полный список красных даёт только локальный прогон всех шагов подряд](a-job-that-stops-at-the-first-red-step-hides-the-rest.md) - [Слой, попавший в точку раскрутки, заморожен до её перепечатки](a-layer-inside-the-bootstrap-point-is-frozen-until-it-is-reprinted.md) -- [Исходник лексера под интерпретатором стоит минуты на сто килобайт, поэтому сверка потока токенов идёт по выборке, а не по дереву](the-lexer-source-under-the-interpreter-costs-minutes-per-hundred-kilobytes.md) +- [Двоичный для ведомости, собранный рядом с деревом, не видит его библиотеку и подаёт это как долг автора](a-ledger-binary-beside-the-tree-cannot-see-the-library-and-blames-the-author.md) - [Измеренный ноль ценнее ненайденного правила](a-measured-zero-is-valuable.md) - [Слияние не умеет сливать напечатанное семя: любая сторона теряет правило, и на стволе `4c1b6aef` потерялась индукция по строке](a-merge-cannot-merge-a-generated-seed-either-side-loses-a-rule.md) - [Число, у которого нет ключа подстановки, расходится не с другой страницей, а со своим же отчётом](a-number-with-no-key-drifts-from-its-own-report.md) - [Число прозы без названного измерителя не перепроверяется, а заменяется другим числом](a-number-without-a-named-measure.md) +- [Напечатанный двоичный без клейма пределов не тянет ни одного набора проб, и красный набор выглядит поломкой набора](a-printed-binary-without-the-stamp-runs-no-probe-suite.md) +- [Ведомость доказательств при отставшем семени показывает дерево, которого нет, — поэтому сторож блокирует, а не советует](a-proof-ledger-taken-with-a-stale-seed-shows-a-tree-that-does-not-exist.md) - [Красное после слияния — не обязательно своё: мерить его надо на самом стволе, отдельным рабочим деревом](a-red-inherited-from-the-trunk-must-be-measured-on-the-trunk.md) - [Снятая правка обязана красить тест — иначе она ничего не держит](a-removal-must-turn-a-test-red.md) - [Страж семени, спрашивающий про НЫНЕШНЕЕ дерево, красен по устройству, а не по нерадивости](a-seed-guard-asking-about-the-current-tree-is-red-by-construction.md) - [Прогон в общем каталоге теряется молча: чужой процесс пишет в файл с тем же именем](a-shared-log-path-silently-replaces-your-run.md) - [Отставшая ведомость чаще отстала на стволе, чем на ветке, — и раскладывать её надо пофайльно, иначе убыль спрячется](a-stale-ledger-must-be-split-per-file-or-the-decrease-hides.md) - [Липкий бит на чужом каталоге останавливает `git merge` целиком, а обходится одним коммитом](a-sticky-bit-in-a-shared-tree-stops-git-merge.md) +- [После удаления реализации на JavaScript набор проб отдаёт ноль, а не «почти всё»](after-the-second-implementation-is-deleted-the-test-suite-returns-zero.md) - [Журнал, записывающий короткий хеш коммита, догнать правкой коммита нельзя](amend-cannot-catch-up-a-journal-that-records-hashes.md) +- [Примета приёмки, которой не досталось материала, обязана сказать «не снята», а не «сошлась»](an-acceptance-sign-without-material-must-say-not-taken-not-passed.md) - [Пустой раздел отчёта и посчитанный ноль — разные новости](an-empty-section-and-a-counted-zero-are-not-the-same-news.md) - [Внутренний предел витков умножается на цену витка и обязан помещаться во внешний бюджет слоя](an-inner-step-limit-multiplies-into-the-outer-budget.md) - [Подделка, не вписанная в сторожа, оставляет своё правило без надзора — таких оказалось пять из тринадцати](an-unregistered-forgery-leaves-its-rule-unwatched.md) @@ -233,24 +239,21 @@ - [Команда может ответить «проверено», не проверив ничего, — и это хуже отказа](checked-without-checking.md) - [Проверка, переставшая сравнивать, продолжает зеленеть — за один день поймано трижды](checks-that-stopped-comparing.md) - [Замер скорости проверяет себя контрольной суммой — иначе «стало быстро, но неверно»](checksum-inside-the-benchmark.md) -- [Цикл поручений принадлежит хозяину, а не языку: `flang io` в двоичном стоил 1289 строк C и трёх точек на flang](the-command-loop-belongs-to-the-host-not-the-language.md) - [Долг, закрытый на неслитой ветке, остаётся открытым долгом](debt-closed-on-an-unmerged-branch.md) - [Утверждения под одним именем сторож видит как одно — вписать подделку в список мало, надо развести имена](duplicate-claim-names-hide-halves-from-the-guard.md) -- [Закоммиченный в `main` двоичный отстал от исходников того же коммита: им не разбирается `stdlib/lists.flang`](the-binary-in-main-lagged-its-own-sources.md) -- [flang-близнец сторожа столкновений зеленел на трёх настоящих столкновениях](the-flang-twin-of-the-collision-guard-stayed-green-on-three-real-collisions.md) - [`flang io` не может быть точкой входа для ярлыков: доводов он не принимает, вывод потомка копит до конца, а код возврата теряет](flang-io-cannot-be-the-entry-point-for-shortcuts.md) - [Самораскрутка меряется четырьмя кусками JavaScript, три закрыты](four-pieces-of-javascript.md) - [`git cherry` не видит содержимое, приехавшее в ветку слиянием, — «своего ноль» надо перепроверять сравнением деревьев](git-cherry-does-not-see-content-that-arrived-by-merge.md) - [`git ls-files | grep '\.flang$'` насчитал 390 файлов там, где их 826: git берёт пути с не-ASCII в кавычки](git-quotes-non-ascii-paths-and-a-count-loses-them.md) -- [Измеритель числа умирает раньше, чем само число в прозе, и тогда честного способа обновить страницу не остаётся](the-measurer-dies-before-the-number-in-prose.md) - [Двоичный не может напечатать сам себя в Java: список занятых имён пересобирается на КАЖДУЮ функцию, и на 4257 функциях это упирается в предел шагов](java-printer-rebuilds-the-taken-name-list-per-function.md) +- [Отставание от семени определяется графом импортов, а не долей отсутствующих имён: порог 80 % отнёс две трети «отставания» не туда](lag-behind-the-seed-is-told-by-the-import-graph-not-by-a-share-of-missing-names.md) - [Номера строк и числа в задании — это дешёвая проверка того, на той ли ветке заведено рабочее дерево](line-numbers-in-a-task-verify-the-branch-it-was-written-against.md) - [Замер собранного артефакта врёт молча: `make` не пересобирает, а отвечает «nothing to be done»](measuring-a-stale-artifact.md) - [Объединение вариантов закрытой суммы — законное слияние, и оно обязано покраснеть у каждого, кто эту сумму разбирает](merging-two-branches-into-one-closed-sum.md) - [Числа в прозе сторожатся, имена модулей — нет, и врут дольше](module-names-in-prose-are-unguarded.md) - [Node ушёл с пути сборки: точку раскрутки печатает сам двоичный, и обе печати совпали байт в байт](node-left-the-build-path.md) +- [Печать одного модуля в двух средах — необходимое условие гейта Г6, а не сам гейт](one-module-printed-in-two-environments-is-a-necessary-condition-of-gate-six-not-the-gate.md) - [Одна причина, названная сразу за группу, прячет остальные — и держит в долге тех, кого не держит ничто](one-named-reason-for-a-group-hides-the-others.md) -- [После удаления реализации на JavaScript набор проб отдаёт ноль, а не «почти всё»](after-the-second-implementation-is-deleted-the-test-suite-returns-zero.md) - [Вычтенный в сверке блок «границы входа» был не лишней частью, а дырой: напечатанная Java без него не запускается вовсе](printed-java-without-entry-table-does-not-start.md) - [Относительная ссылка ломается ровно при копировании каталога — и первой ломается та, ради которой всё написано](relative-links-break-on-copy.md) - [Переименование файла не краснеет, а тихо выключает проверку чисел в прозе](renaming-a-file-silently-disables-the-guard.md) @@ -259,10 +262,19 @@ - [Разрешать конфликт «по блоку за раз» — лотерея: автослияние уже применило удаления другой стороны, и блоки не независимы](resolving-a-conflict-block-by-block-is-a-lottery.md) - [Отказ прогона, отданный значением, — граница, а не одна функция: её ловят исключением 33 места, а не одно](run-outcome-as-a-value-is-a-boundary-not-a-function.md) - [Бывают конфликты слияния, которых git не показывает](silent-merge-conflicts.md) -- [Сторож столкновений имён не знал о вариантах суммы и молчал о шести настоящих столкновениях](the-collision-guard-did-not-know-sum-variants.md) - [Структурный размер значения доказывается тотальным, если спускаться в поле образца, а не в результат поиска по ключу](structural-size-becomes-total-when-you-descend-into-the-pattern-field.md) +- [Закоммиченный в `main` двоичный отстал от исходников того же коммита: им не разбирается `stdlib/lists.flang`](the-binary-in-main-lagged-its-own-sources.md) +- [Двоичный судится по именам из его таблицы символов, а не по размеру и строкам: 80 байт разницы прятали код двух невлитых веток](the-binary-is-judged-by-its-symbol-names-not-by-its-size-or-strings.md) +- [Ведомость двоичного бывает слабее ведомости на Node и никогда не сильнее — и сверять её надо в одну сторону, а не побайтово](the-binary-ledger-can-be-weaker-and-never-stronger.md) +- [Сторож столкновений имён не знал о вариантах суммы и молчал о шести настоящих столкновениях](the-collision-guard-did-not-know-sum-variants.md) +- [Цикл поручений принадлежит хозяину, а не языку: `flang io` в двоичном стоил 1289 строк C и трёх точек на flang](the-command-loop-belongs-to-the-host-not-the-language.md) - [Компилятор ЧИТАЕТ свои исходники — «прогона по `flang/self/**` не существует» было свойством места, где лежал двоичный, а не свойством дерева](the-compiler-library-is-found-next-to-the-binary-not-next-to-the-file.md) +- [flang-близнец сторожа столкновений зеленел на трёх настоящих столкновениях](the-flang-twin-of-the-collision-guard-stayed-green-on-three-real-collisions.md) - [Дважды за один замер врал прибор, а не предмет — и оба раза это выглядело как находка](the-instrument-lied-not-the-subject.md) +- [Исходник лексера под интерпретатором стоит минуты на сто килобайт, поэтому сверка потока токенов «исходник против двоичного» идёт по выборке, а не по дереву](the-lexer-source-under-the-interpreter-costs-minutes-per-hundred-kilobytes.md) +- [Измеритель числа умирает раньше, чем само число в прозе, и тогда честного способа обновить страницу не остаётся](the-measurer-dies-before-the-number-in-prose.md) +- [Счётчик шагов печати обнуляется на каждой стадии, поэтому её ход читается по отметкам времени, а не по процентам](the-reprint-step-counter-resets-per-stage-so-progress-is-read-from-tick-marks.md) +- [Семя рантайма — это источник плюс шапка, и отставание посреди правки — норма, а беда — только сломанное копирование](the-runtime-seed-is-the-source-plus-a-header-and-lagging-mid-work-is-normal.md) - [Вторую независимую реализацию возместить нечем — её можно только сохранить в проверках](the-second-implementation-cannot-be-replaced.md) - [Седьмое действие исчезло вместе с удалённым JavaScript: у двоичного словарь «Действие» остался шестивариантным](the-seventh-action-vanished-with-the-deleted-javascript.md) - [Ядро доказательств из исходников под интерпретатором до вердикта не доходит: стек хозяина кончается на глубине 2 074 974](the-source-proof-kernel-cannot-be-driven-by-the-interpreter.md) @@ -272,20 +284,9 @@ - [Файл, взятый целиком из другой ветки, приносит с собой её долги — мерить надо теми же проверками до и после](transplanted-file-brings-its-own-debt.md) - [Эталон отстаёт от свидетеля, который уехал, — и отставание надо мерить, а не оговаривать](twin-lags-behind-the-reference.md) - [Два ядра, выросшие порознь от одной точки, текстом не сливаются](two-cores-do-not-merge-as-text.md) +- [Два журнала рядом с деревом печати — это неизвестность, а не «взять посвежее»: так отказ печати прочитали как успех](two-logs-beside-a-print-tree-mean-unknown-not-take-the-newer.md) - [Две реализации одного файла, выросшие порознь, бывают не соперниками, а половинами — решает пересечение имён, а не размер](two-rewrites-of-one-file-may-be-halves.md) - [Набранное число расходится между страницами; подставленное — не может](typed-numbers-drift-substituted-ones-cannot.md) -- [Ведомость двоичного бывает слабее ведомости на Node и никогда не сильнее — и сверять её надо в одну сторону, а не побайтово](the-binary-ledger-can-be-weaker-and-never-stronger.md) -- [Двоичный судится по именам из его таблицы символов, а не по размеру и строкам: 80 байт разницы прятали код двух невлитых веток](the-binary-is-judged-by-its-symbol-names-not-by-its-size-or-strings.md) -- [Двоичный для ведомости, собранный рядом с деревом, не видит его библиотеку и подаёт это как долг автора](a-ledger-binary-beside-the-tree-cannot-see-the-library-and-blames-the-author.md) -- [Примета приёмки, которой не досталось материала, обязана сказать «не снята», а не «сошлась»](an-acceptance-sign-without-material-must-say-not-taken-not-passed.md) -- [Счётчик шагов печати обнуляется на каждой стадии, поэтому её ход читается по отметкам времени, а не по процентам](the-reprint-step-counter-resets-per-stage-so-progress-is-read-from-tick-marks.md) -- [Ведомость доказательств при отставшем семени показывает дерево, которого нет, — поэтому сторож блокирует, а не советует](a-proof-ledger-taken-with-a-stale-seed-shows-a-tree-that-does-not-exist.md) -- [Два журнала рядом с деревом печати — это неизвестность, а не «взять посвежее»: так отказ печати прочитали как успех](two-logs-beside-a-print-tree-mean-unknown-not-take-the-newer.md) -- [Отставание от семени определяется графом импортов, а не долей отсутствующих имён: порог 80 % отнёс две трети «отставания» не туда](lag-behind-the-seed-is-told-by-the-import-graph-not-by-a-share-of-missing-names.md) -- [Печать одного модуля в двух средах — необходимое условие гейта Г6, а не сам гейт](one-module-printed-in-two-environments-is-a-necessary-condition-of-gate-six-not-the-gate.md) -- [Быстрый пересев семени законен ровно тогда, когда замыкание и пределы не тронуты относительно отпечатка](a-fast-reseed-is-legal-only-while-the-closure-and-limits-match-the-stamp.md) -- [Семя рантайма — это источник плюс шапка, и отставание посреди правки — норма, а беда — только сломанное копирование](the-runtime-seed-is-the-source-plus-a-header-and-lagging-mid-work-is-normal.md) -- [Напечатанный двоичный без клейма пределов не тянет ни одного набора проб, и красный набор выглядит поломкой набора](a-printed-binary-without-the-stamp-runs-no-probe-suite.md) ## Устройство репозитория @@ -300,55 +301,56 @@ - [Подстановка, не попавшая в образец, доезжает до читателя двойными скобками — и молча](a-substitution-that-misses-the-pattern-reaches-the-reader.md) - [Режим `--mode=u=rw,go=r`, заданный ради повторимости архива, запирает каталоги наглухо](a-tar-mode-for-files-locks-directories.md) - [Проверку пути установки нельзя целиком написать на flang: хозяин убивает процесс на 30 000 мс, а сборка идёт 128 000 мс](host-timeout-of-30-seconds-keeps-builds-out-of-flang-plans.md) +- [У столкновений имён три судьи, и третий молчит, пока первое столкновение не разведут переименованием](name-collisions-have-three-judges-and-the-third-is-silent-until-you-rename.md) - [`package.json` давно не источник версии, а её отпечаток — и убирать из корня нечего](package-json-is-no-longer-the-source-of-the-version.md) - [Расшифровка прогона на странице — это замер, и после тега его надо переснимать](stale-pages-are-measurements-nobody-retakes.md) - [Таблица описи дерева расходится при каждой правке файла оболочки, и ловить это дешевле до пуша](the-inventory-table-drifts-with-every-shell-line-so-the-hook-checks-it-before-push.md) - [Лицензионный гейт берёт новый каталог под опубликованным путём сразу, и первый же файл без шапки красит CI](the-license-gate-covers-new-files-from-birth.md) -- [Старый проект FTS нельзя вынести из репозитория дёшево: от него зависят все восемь генераторов кода flang](two-projects-tied-by-generators.md) - [Выпуск был замкнут сам на себя: набор тестов требовал релизного архива, а собрать его прогону было нечем](the-release-was-closed-on-itself-the-suite-needed-an-archive-nobody-built.md) - [Версия пишется один раз в источнике и разносится одной командой, а sha256 формулы из числа не выводится](the-version-is-written-once-and-spread-by-one-command-but-sha256-is-not-derived-from-it.md) -- [У столкновений имён три судьи, и третий молчит, пока первое столкновение не разведут переименованием](name-collisions-have-three-judges-and-the-third-is-silent-until-you-rename.md) +- [Старый проект FTS нельзя вынести из репозитория дёшево: от него зависят все восемь генераторов кода flang](two-projects-tied-by-generators.md) ## Интерфейс инструмента - [Знак сайта на 24 пикселях держит одну строку брусков, а не две — и видно это только на растре в натуральную величину](a-24-pixel-mark-holds-one-row-not-two.md) +- [Проверку, которая зовёт компилятор, а не разбирает `.flang` сама, переносить на flang почти нечего — мешает только чтение ответа](a-check-that-calls-the-compiler-ports-to-flang-mechanically.md) - [Клавиша, которую не нажимает ни одна проверка, — это обещание справки, а не поведение](a-key-no-probe-presses-is-a-promise-not-a-behaviour.md) +- [Ключ предела задаёт предел, а не поднимает его: число «с запасом» меньше вшитого опускает предел и роняет прогон](a-limit-flag-sets-the-limit-and-a-smaller-number-lowers-it.md) - [Идущая программа сама пишет, где она](a-running-program-writes-its-own-pulse-to-a-file.md) +- [Пробе под терминалом не нужен Python: `script` и подача со сроками нажимают те же клавиши](a-terminal-probe-needs-no-python-script-and-a-timed-feeder-press-the-keys.md) - [Сообщение, объясняющее устройство инструмента, читается как поломка — и признак у таких сообщений всего три](a-tool-that-explains-itself-instead-of-the-persons-work.md) - [Числовой код выхода нельзя вывести из именованного кода отказа — его берут из природы беды](an-exit-code-cannot-come-from-a-named-failure.md) - [Голая команда открывает оболочку, а справку печатает только тот, кого о ней спросили](bare-command-opens-the-shell.md) - [Проверки переезжают на flang планами ввода-вывода, а упираются в журнал поручений](checks-move-to-flang-as-io-plans.md) - [Справка командной строки расходится между двумя реализациями чаще всего остального — и молча](cli-help-diverges-between-the-two-implementations.md) - [Ключевых поверхностей четыре, все приняты одновременно, и переключателя нет ни одного](four-keyword-surfaces-are-accepted-at-once-and-nothing-switches-them.md) -- [Прогонщик корпуса написан на flang целиком; на C осталось 59 строк невыразимого и 419 строк перевозки](the-corpus-runner-is-written-in-flang-except-for-effects.md) - [Ключ `--предел-шагов` ЗАДАЁТ предел, а не поднимает его, — и умолчание лежит НЕ там, где его ищут](library-step-limit-key-sets-not-raises.md) -- [«Показать» у двоичного отвечает отказом, а прогон продолжается — прежний замер устарел](show-answers-with-a-refusal-and-does-not-crash-the-run.md) -- [Проверку, которая зовёт компилятор, а не разбирает `.flang` сама, переносить на flang почти нечего — мешает только чтение ответа](a-check-that-calls-the-compiler-ports-to-flang-mechanically.md) - [Предел глубины поднимается только вместе со стеком, поэтому ключ к нему разбирается ДО команды](raising-the-depth-limit-means-raising-the-stack.md) +- [«Показать» у двоичного отвечает отказом, а прогон продолжается — прежний замер устарел](show-answers-with-a-refusal-and-does-not-crash-the-run.md) - [Написание, которого нет в таблице слов, в документацию не попадает вовсе](spellings-outside-the-word-table-stay-undocumented.md) - [Отвечает flang только по-русски, и выбрать язык ответа сегодня нечем](the-compiler-answers-only-in-russian-and-nothing-can-change-that.md) +- [Прогонщик корпуса написан на flang целиком; на C осталось 59 строк невыразимого и 419 строк перевозки](the-corpus-runner-is-written-in-flang-except-for-effects.md) - [Ссылка на «полный список кодов» вела туда, где нет ни одного отказа ядра: 0 из 13](the-full-list-of-codes-named-none-of-the-kernel-refusals.md) - [Функция, названную которой печатает отказ при исчерпании предела, — не та, где уходит время](the-function-named-when-the-limit-runs-out-is-not-where-the-time-goes.md) - [Двоичный файл — подмножество языка, и подмножество обязано называть себя, а не отвечать «неизвестная команда»](the-installed-binary-is-a-named-subset.md) - [Путь установки не проходил целиком никто, и потому `flang emit --target c` не работал НИ У ОДНОГО поставившего язык](the-installed-path-was-never-walked-end-to-end.md) - [Номер выпуска не отвечает на вопрос «что у меня в руках»: два двоичных 0.7.14 вели себя по-разному, и отличить их можно было только по поведению](the-release-number-cannot-say-what-is-inside-the-binary.md) - [Оболочка читала строку каноническим fgets, и стрелку печатал терминал, а не она; клавиш flang-tui не разбирает, а файл оболочки уезжает в семя дословно — правка доезжает быстрым пересевом, не перепечаткой](the-shell-read-the-line-with-fgets-and-the-terminal-printed-the-arrow.md) -- [Пробе под терминалом не нужен Python: `script` и подача со сроками нажимают те же клавиши](a-terminal-probe-needs-no-python-script-and-a-timed-feeder-press-the-keys.md) - [Два плана postgres держит не предел шагов, а стек хозяина: 1 ГиБ и 2 074 970 кадров, и ключами это не двигается](two-postgres-plans-are-held-by-the-host-stack-not-the-step-limit.md) -- [Ключ предела задаёт предел, а не поднимает его: число «с запасом» меньше вшитого опускает предел и роняет прогон](a-limit-flag-sets-the-limit-and-a-smaller-number-lowers-it.md) ## Найденные ошибки -- [Функция-значение, применённая к записи с самой собой, проходит как тотальная и не останавливается](a-self-applied-function-value-passes-the-totality-check.md) +- [Перепись целей без двоичного печатает нули и выходит кодом 0 — поэтому отсутствие прибора это «не проверено»](a-census-without-the-binary-prints-zeros-and-exits-zero.md) - [Изменившийся вердикт при снятии правки — ещё не доказанная ложь: доказанным надо проверить, ложь ли это](a-changed-verdict-on-removal-is-not-a-proven-lie.md) - [Проверка, живущая внутри одной команды, — это класс дефектов, и он всплыл трижды](a-check-that-skips-a-check-is-a-class.md) +- [Список замыкания, взятый грепом, сторожит форму записи ввоза, а не ввоз, — и пустая база при этом читается как «столкновений нет»](a-closure-list-taken-by-grep-guards-the-spelling-of-the-import-not-the-import.md) - [Новую цель печати можно прогнать до перепечатки семени: компилятор, напечатанный в JavaScript, отвечает за секунды там, где интерпретатор идёт десять минут](a-compiler-printed-to-javascript-runs-a-new-target-in-seconds.md) - [Поправка, написанная под деление с усечением, применённая к делению вниз, срабатывает дважды — и календарь до нашей эры уезжает на год](a-correction-written-for-truncation-fires-twice-under-floor-division.md) - [Нарочная подделка и отставшая запись выглядят для побайтового сличения одинаково, и потому сторож без поимённого списка красен всегда](a-deliberate-forgery-and-a-stale-record-look-identical-to-a-byte-comparison.md) -- [Запись доказательства без SHA-256 в шапке принимает другую программу той же меры — и сходится](a-proof-record-without-sha256-accepts-another-program-of-the-same-measure.md) - [Ведущий нулевой октет DER делал отозванный сертификат неотозванным: 1 серийный номер из 7 разошёлся с openssl](a-der-leading-zero-turns-a-revoked-certificate-into-an-unrevoked-one.md) - [Словарь встроенных форм лежал в девяти местах, и три копии уже разошлись](a-dictionary-copied-into-nine-places-drifts-silently.md) - [Поле встроенного словаря, названное ключевым словом, ставится и не читается — и проверять это надо ДО того, как имя выбрано](a-dictionary-field-named-like-a-keyword-cannot-be-read.md) +- [Дизъюнкция без внешних скобок отвечает за всё тело, и ни разбор, ни типы на это не краснеют](a-disjunction-without-outer-parentheses-answers-for-the-whole-body.md) - [Макрос `_POSIX_C_SOURCE` открывает функцию на glibc и закрывает её на Darwin](a-feature-macro-that-opens-on-glibc-closes-on-darwin.md) - [Отказ ворот приходит тем же кодом, что вердикт проверки](a-gate-refusal-looks-like-a-verdict.md) - [Сетка спрятала ложное утверждение: «результат не больше довода» неверно на не-числе](a-grid-hid-a-claim-false-on-not-a-number.md) @@ -357,43 +359,42 @@ - [Тип функции на английской поверхности не записывается словами: `to number` съедает встроенная форма](a-longer-builtin-phrase-eats-a-type-on-the-english-surface.md) - [Модуль, проходящий `flang check` в одиночку, всё ещё может сломать раскрутку столкновением имён](a-module-that-checks-alone-still-collides-in-the-closure.md) - [Строка плана, прочитанная как результат, — вот как страницы начинают обещать несуществующее](a-plan-row-read-as-a-result-is-how-pages-start-promising.md) +- [Запись доказательства без SHA-256 в шапке принимает другую программу той же меры — и сходится](a-proof-record-without-sha256-accepts-another-program-of-the-same-measure.md) - [Поле записи отмывало значение из-за симметричного сравнения типов](a-record-field-laundered-a-value.md) - [Перепечатанное семя может нести квантор, которым не может воспользоваться ни одна программа: разбор, ядро, печать и проверяющая программа есть, а типизатор — нет](a-reprinted-seed-can-carry-a-quantifier-that-no-program-can-use.md) +- [Функция-значение, применённая к записи с самой собой, проходит как тотальная и не останавливается](a-self-applied-function-value-passes-the-totality-check.md) - [Сторона на flang может уже существовать под чужим именем — проверять до того, как писать](a-side-may-already-exist-check-before-writing.md) - [Прибор свежести, которому подсунули старый двоичный, объявляет отставшими ровно те записи, которые свежее всего](a-stale-kernel-binary-turns-a-freshness-check-into-a-liar.md) +- [Файл проверок, упавший на загрузке, в отчёте прогона неотличим от отсутствующего](a-test-file-that-failed-to-load-looks-absent-in-the-report.md) - [Пример зеленеет на варианте, которого разбор не производит никогда, — и это класс](an-example-can-green-on-a-variant-the-parser-never-produces.md) -- [Дизъюнкция без внешних скобок отвечает за всё тело, и ни разбор, ни типы на это не краснеют](a-disjunction-without-outer-parentheses-answers-for-the-whole-body.md) - [Жирный вокруг встроенного кода не собирался на сайте ни разу, и это было видно только глазом](bold-around-inline-code-never-rendered.md) - [Байтовый поиск и знаковый счёт — это две меры на всякой строке, которая не является правильным UTF-8](byte-search-and-character-count-are-two-measures-on-every-ill-formed-string.md) - [Печать в C ломается на параметре, чьё имя транслитерируется в ключевое слово C — но только у рекурсивной функции](c-backend-emits-a-c-keyword-as-a-parameter-name.md) -- [Четыре вещи, которых в `обеспечивает` написать нельзя, и одна из них ВЕШАЕТ проверку вместо отказа](four-things-a-postcondition-cannot-say.md) - [Проверка замкнутости цели стояла только на ветви индукции, и прямой шаг «по примеру» шёл мимо неё](closedness-check-guarded-only-the-induction-branch.md) -- [У строки flang БЫЛО две меры, и делило формы между ними представление строки у цели печати, а не язык](two-string-measures-divided-the-builtin-forms.md) - [Граница входа у программ, напечатанных двоичным, была пуста, и закрыл её перенос одной таблицы на flang](entry-table-moved-to-flang-closes-the-binary-border.md) +- [Четыре вещи, которых в `обеспечивает` написать нельзя, и одна из них ВЕШАЕТ проверку вместо отказа](four-things-a-postcondition-cannot-say.md) - [`git stash` общий на все рабочие деревья репозитория, поэтому в рабочих деревьях им пользоваться нельзя](git-stash-is-shared-across-worktrees.md) - [Обещание `json.flang` «разбор печати даёт то же значение» ложно, и ломается оно тремя разными способами](json-print-parse-round-trip-is-false.md) - [Чему учить ядро следующим: свод семи каталогов отказов, а не догадка](kernel-gaps-ranked-across-shares.md) - [Минус ноль чинили дважды подряд — и оба раза мимо, в разные стороны](minus-zero-fixed-twice-and-both-times-past-the-mark.md) - [Минус ноль всплыл четыре раза — это класс, а не отдельные ошибки](minus-zero-is-a-class.md) - [NaN достижим изнутри языка и делает «очевидные» правила ложными](nan-is-reachable.md) -- [Файл проверок, упавший на загрузке, в отчёте прогона неотличим от отсутствующего](a-test-file-that-failed-to-load-looks-absent-in-the-report.md) - [В WebAssembly нет сторожевой страницы, поэтому заниженная константа стека портит память молча](no-guard-page-in-wasm.md) - [Одна ссылка на ненаписанную заметку останавливает публикацию сайта целиком](one-dangling-note-link-stops-the-whole-site.md) - [Печать плана обещана наизнанку: семь целей молча забывают план, восьмая отказывает не про него](plan-printing-is-promised-inside-out-and-nothing-verifies-it.md) - [У напечатанной программы две двери, а граница входа стояла только у одной](printed-program-has-two-doors.md) - [Возврат работы, потерянной чужим слиянием, из второй ветки даёт не конфликт, а недостижимый случай — и файл молча выпадает из всех замеров](restoring-lost-work-in-a-second-branch-yields-an-unreachable-case.md) - [Поиск по сайту не находил код отказа ни разу из тринадцати, и ломался он с двух сторон сразу](search-never-found-a-refusal-code.md) +- [Отказ ядра «у цели нет вида» на ограничении `таких что` был не нехваткой правила, а нераспакованной обёрткой](such-that-was-an-unpacked-wrapper-not-a-missing-rule.md) - [Ядро принимает ложь дважды за сутки — это класс дефектов, а не случайность](the-core-accepts-falsehood-a-class.md) - [Ядро печатало «доказано индукцией» об утверждении, которое рантайм тут же отвергал](the-core-proved-a-falsehood.md) - [Ворота раздают места по ЗАПРОШЕННОМУ пределу, а не по съеденной памяти — и просьба «с запасом» отнимает места у всех](the-gate-hands-out-slots-by-what-you-ask-not-by-what-you-use.md) +- [Ворота пропускают код команды насквозь: один код 75 не отличает отказ ворот от команды, вернувшей 75](the-gate-passes-the-command-exit-code-through-so-75-alone-proves-nothing.md) +- [Веер оснастки считается по ядрам, а кончается память — и правило «не больше двух прогонов» тут не помогает](the-harness-fan-is-sized-by-cores-but-memory-runs-out-first.md) - [Сторож жаргона считает имя ключа подстановки за жаргон в прозе, и это 39 ложных срабатываний на десяти читательских страницах](the-jargon-guard-counts-a-substitution-key-as-prose.md) - [Слой законов не различает списки по типу элемента: ключ у всякого списка — `list:null`](the-law-layer-cannot-tell-two-list-types-apart.md) - [Страница `man` показывала вместо примера `--args` обрывок `'{`, и проверка была зелёной](the-man-page-swallowed-the-args-example.md) -- [Веер оснастки считается по ядрам, а кончается память — и правило «не больше двух прогонов» тут не помогает](the-harness-fan-is-sized-by-cores-but-memory-runs-out-first.md) -- [Ворота пропускают код команды насквозь: один код 75 не отличает отказ ворот от команды, вернувшей 75](the-gate-passes-the-command-exit-code-through-so-75-alone-proves-nothing.md) -- [Список замыкания, взятый грепом, сторожит форму записи ввоза, а не ввоз, — и пустая база при этом читается как «столкновений нет»](a-closure-list-taken-by-grep-guards-the-spelling-of-the-import-not-the-import.md) -- [Перепись целей без двоичного печатает нули и выходит кодом 0 — поэтому отсутствие прибора это «не проверено»](a-census-without-the-binary-prints-zeros-and-exits-zero.md) -- [Отказ ядра «у цели нет вида» на ограничении `таких что` был не нехваткой правила, а нераспакованной обёрткой: два места из трёх распаковывали, третье — нет](such-that-was-an-unpacked-wrapper-not-a-missing-rule.md) +- [У строки flang БЫЛО две меры, и делило формы между ними представление строки у цели печати, а не язык](two-string-measures-divided-the-builtin-forms.md) ## Отвергнутые пути @@ -408,15 +409,15 @@ - [Модуль находится по имени из своей первой строки, а места поиска — свой каталог, каждый каталог выше и библиотека компилятора](a-module-is-found-by-the-name-on-its-first-line.md) - [Чужой черновик каталогом выше перекрывает библиотеку дерева молча, и ловушка стоит ровно в корне репозитория](a-stray-draft-above-the-tree-shadows-the-library-silently.md) +- [Кешировать доказательство сегодня дороже, чем доказать заново: 111 мс против 145 мс на всём корпусе](caching-a-proof-costs-more-than-proving-it.md) - [Адресация по содержимому: версий нет, есть хеши](content-addressing.md) - [Хеш содержимого — идентичность внутри, имена и версии — интерфейс снаружи](hash-inside-names-outside.md) -- [Кешировать доказательство сегодня дороже, чем доказать заново: 111 мс против 145 мс на всём корпусе](caching-a-proof-costs-more-than-proving-it.md) +- [Законы годятся указателем, а не выводом — но в стандартной библиотеке их объявлено ноль](laws-as-a-pointer-not-a-conclusion.md) - [Гипотеза про адресацию по содержимому не работает у нас — и не из-за хешей](names-not-hashes.md) - [Предел шагов у прогона примеров — один на весь запуск, и примеры ввезённых модулей считаются в него же](one-step-budget-covers-a-whole-run-including-imported-examples.md) - [Выборочный ввоз обязан перечислить и те имена, которые зовёт КОНТРАКТ функции, а не только её тело](only-import-must-list-what-the-contract-calls.md) - [Unison установлен и измерен: ромб он решает не так, как обещает лозунг](unison-measured.md) - [В хеш входит контракт, но не доказательство — у теоремы свой адрес](what-goes-into-the-hash.md) -- [Законы годятся указателем, а не выводом — но в стандартной библиотеке их объявлено ноль](laws-as-a-pointer-not-a-conclusion.md) ## Внешнее и объёмы @@ -461,13 +462,17 @@ - [Поле чужого ответа берётся ПО МЕСТУ, а не поиском ключа: поиск находит ближайший ключ, а не ваш](a-field-of-a-foreign-reply-is-taken-by-position-not-by-key-search.md) - [Имя файла теряется между разбором и «Бедой», и языковой сервер в двоичном упирается именно в этот разрыв, а не в транспорт](a-file-name-is-lost-between-the-parser-and-the-failure.md) - [Отбор по выписанному списку считается только у замкнутой цели](a-filter-over-a-written-out-list-is-computed-only-in-a-closed-goal.md) +- [Починка, пролежавшая через разрез файла на мелкие функции, переписывается заново — и выходит дешевле патча](a-fix-that-waited-through-a-refactor-is-rewritten-not-rebased.md) - [Признак, прочитанный печатью, ложен на каждом входе — и сверка этого не видит](a-flag-read-by-the-printer-is-false-on-every-input.md) - [Свёртка, отмечающая находку пустотой накопленного, теряет ПУСТОЙ ответ — и это класс](a-fold-that-marks-a-find-by-emptiness-loses-the-empty-answer.md) - [Свёртка, забирающая каждое совпадение, оставляет ПОСЛЕДНЕЕ — и это ловушка на разборе по меткам](a-fold-that-overwrites-keeps-the-last-match.md) +- [Подделочная программа и лгущая запись — разные вещи, и в знаменатель они идут по-разному](a-forgery-and-a-forged-record-are-different-things.md) - [Дробная степень в flang выражается точно — через целую степень и корень Ньютона](a-fractional-power-is-exact-through-an-integer-power-and-a-newton-root.md) - [Условие цели ядро подставляет значением, но фактом его не делает](a-goal-condition-is-substituted-as-a-value-but-never-becomes-a-fact.md) +- [Греп по словам выдал отклонённый пуш за зелёный: крючок печатает «КРАСЕН», а я искал «красен»](a-grep-on-words-let-a-rejected-push-look-green.md) - [Сторож, поставленный раньше стадий, заполняющих отчёт, заставляет отчёт врать — а правильное место стоит 5,7 % прогона, не больше](a-guard-placed-before-the-reporting-stages-makes-the-report-lie.md) - [Второй, ручной список полей записи «Настройки» отстал от таблицы EMIT_FIELDS_C и ронял КАЖДЫЙ ввод живой оболочки, а не только «разложить … на символы»](a-hand-rolled-settings-record-drifts-from-the-field-table-silently.md) +- [Заголовок «ВЗЯТО N ИЗ M» рядом с таблицей, из которой он вычисляется, лжёт при первой же смене ряда](a-hand-typed-score-next-to-its-table-drifts-silently.md) - [Рукописная копия обнаруживает себя столкновением имён ровно в тот день, когда библиотека дорастает до неё](a-hand-written-copy-reveals-itself-as-a-name-collision.md) - [Рукописный хозяин живёт по правилам напечатанного проекта, а не по своим](a-hand-written-host-lives-by-the-printed-projects-rules.md) - [Словарь хешем стал параметрическим по значению, и параметр ввоз переживает — ломала ввоз ЧУЖАЯ КОПИЯ МОДУЛЯ](a-hash-dictionary-became-parametric-and-a-foreign-module-copy-broke-the-import.md) @@ -483,6 +488,7 @@ - [Строчное имя варианта в голом «случай «имя»» читается как связывание имени, а не как вариант](a-lowercase-variant-name-in-a-bare-case-reads-as-a-binding.md) - [Мерка сама сторожит порог: лёгкое считает на месте, тяжёлое уводит под ворота](a-measurement-that-guards-its-own-threshold-sends-heavy-runs-through-the-gate.md) - [Замерщик обязан печатать, сколько точек ПОСМОТРЕЛ, а не только сколько прошло](a-measurer-must-print-how-many-points-it-looked-at.md) +- [Предел памяти на прогон — контрольная группа за воротами, и после падения он объясняет, а не пишет «Killed»](a-memory-limit-per-run-is-a-cgroup-behind-a-gate-with-an-explanation.md) - [Груз письма едет билетом, а не значением, — и этим отсутствие полиморфизма перестаёт мешать](a-message-payload-travels-as-a-ticket-not-as-a-value.md) - [Адрес модуля в замке — sha256 его исходника, а сжатия в формате нет вовсе](a-module-address-is-the-sha256-of-its-source.md) - [Круг взаимной рекурсии по дереву разрезается записью-нагрузкой, слияние функций не обязательно](a-mutual-recursion-circle-over-a-tree-is-cut-by-a-payload-record.md) @@ -492,6 +498,7 @@ - [Поле «не минус ноль» на числовом типе закрыло два места, а не одиннадцать](a-not-minus-zero-field-closed-two-places-not-eleven.md) - [Функцию без аргументов нельзя позвать через ввоз, хотя местную — можно](a-nullary-function-cannot-be-called-through-an-import.md) - [Охрана равенством варианту открывает ветвь `разбор`, только если вариант НУЛЬМЕСТНЫЙ, а разбираемое — вызов](a-nullary-variant-guard-opens-one-branch-of-a-match-over-a-call.md) +- [Число, полученное прибором вне хранилища, — не замер, а слух: 61 % работы ячеек жил только во временном каталоге](a-number-taken-outside-the-repository-is-a-rumour-not-a-measurement.md) - [Пакет — это замок, которому дали имя и версию: семь шагов подключения стали двумя](a-package-is-a-lock-given-a-name-and-a-version.md) - [Пара живых узлов поднимается одним `sh -c`, а судит их flang по журналам](a-pair-of-live-nodes-starts-from-one-shell-and-flang-judges-them-by-journals.md) - [Путь, названный в прозе обратными кавычками, не сверяется с деревом ничем — так контракт категорной поверхности пережил свои файлы на 28 упоминаний](a-path-in-backticks-is-checked-against-nothing.md) @@ -504,6 +511,7 @@ - [Запись доказательства печатается из ИСХОДНИКА `proof-record.flang` толкователем двоичного за двенадцать минут — правку печати можно измерить без перепечатки семени](a-proof-record-prints-from-source-in-twelve-minutes-without-a-reprint.md) - [Доказанное постусловие снимает проверку при работе только вместе с примером — условий у печати ДВА, а не одно](a-proved-postcondition-drops-its-runtime-check-only-with-an-example.md) - [Доказанное постусловие в напечатанный код больше не едет, и цена утверждений на сортировке упала с 3,23× до 2,72×](a-proved-postcondition-no-longer-reaches-printed-code.md) +- [Разошедшееся опубликованное число либо устарело, либо было неверным — различает их только пересчёт по дереву коммита съёмки](a-published-number-is-stale-or-wrong-and-only-a-recount-at-the-snapshot-tells-which.md) - [Квантор по соседним парам стоил ДВУХ файлов вместо двадцати девяти — потому что разбор собрал его из уже существующих узлов](a-quantifier-over-adjacent-pairs-cost-two-files-not-twenty-nine.md) - [Квантор по соседним парам выразим СЕГОДНЯ и работает сторожем — стена не в записи, а в доказуемости](a-quantifier-over-adjacent-pairs-is-expressible-today-but-not-provable.md) - [Библиотеку сегодня не выводят из спеки — её пишут агентом, а теорема работает храповиком: 85 680 строк, 1212 теорем, ноль `sorry`](a-ratchet-instead-of-derivation.md) @@ -511,10 +519,12 @@ - [Обещание «печатается записью» было ЛОЖНЫМ на ветви, отдающей «ничто», и никто этого не заметил](a-record-promise-can-be-false-on-the-nothing-branch.md) - [Когда свидетеля не отдают наружу, эталон сверяют с третьим тем, что в дереве уже есть](a-reference-is-checked-against-a-third-artifact-in-the-tree.md) - [Отказ, полученный отставшим двоичным, нельзя приписывать проверяемому файлу](a-refusal-from-a-stale-binary-must-not-be-blamed-on-the-checked-file.md) +- [Прогон на чужой машине превращает отсутствующий тулчейн из пропуска в провал — иначе половина целей не проверена ни разу](a-remote-run-turns-a-missing-toolchain-into-a-failure-not-a-skip.md) - [Снятое препятствие — не цена: `lock` и `package` стоили 2 066 строк C при оценке в 280](a-removed-obstacle-is-not-the-price-of-a-command.md) - [Переименование, разводящее столкновение у одного судьи, создаёт столкновение у следующего, и до правки его не видно ни одним пересечением множеств](a-rename-that-separates-one-collision-creates-the-next-one.md) - [Правило, въехавшее в двоичный, ещё не спрошено двоичным: двенадцать подделок из двенадцати принимались молча, а компилятор при этом писал, что сверил](a-rule-inside-the-binary-is-not-a-rule-the-binary-asks.md) - [Правило, на которое не наступает ни одна программа корпуса, невидимо для сверки эталона — и живёт только в свидетеле](a-rule-no-corpus-program-touches-is-invisible-to-the-reference-check.md) +- [На негодном октете прогонщик обязан отказать одинаково на всех целях — а было пять разных поведений, и отказом не было ни одно](a-runner-must-refuse-a-bad-octet-identically-across-nine-targets.md) - [Проба порчей, которая ничего не испортила, выглядит как успех](a-sabotage-test-that-sabotages-nothing-looks-like-success.md) - [Воспроизводимость по семени кончается ровно на границе узла, и обе половины теперь числа, а не слова](a-seed-orders-only-inside-one-node.md) - [Семя с рантаймом дерева бьёт стек, если не перенести блок настроек из его шапки](a-seed-with-tree-runtime-smashes-the-stack-without-its-limits-block.md) @@ -555,12 +565,12 @@ - [Срок хозяина был не называем, и это одно держало сборку на JavaScript](an-unnameable-host-deadline-alone-kept-the-build-on-javascript.md) - [Автопочинка чисел правит лист и оставляет итог — предложение начинает врать связнее](auto-repair-of-numbers-fixes-the-leaf-and-leaves-the-total.md) - [Тела-связыватели держат две трети недоказанного — 1475 обещаний из 2227, — но сама стена «ядро не заходит внутрь связывателя» не показалась ни на одной из шести проб](binder-bodies-hold-two-thirds-of-the-unproven-but-the-binder-wall-itself-did-not-show-on-six-probes.md) +- [Пределы печати точки раскрутки — одна запись на оба пути, и совпадение проверяется, а не обещается](bootstrap-reprint-limits-are-one-record-shared-with-the-print-script-and-checked.md) - [Сборка двоичного стоит минуту, а не час, — поэтому её место в CI на каждом пуше](building-the-binary-costs-a-minute-not-an-hour.md) - [Счёт вызовов, счёт шагов и часы — три разных ответа, и путать их дорого](calls-steps-and-the-clock-are-three-different-answers.md) - [Доказанное обещание без примера всё равно стоит проверки при работе](certificates-a-proved-promise-without-an-example-still-costs-a-runtime-check.md) - [Пока сборщик записи молчит о своих полях, наверху не доказывается ничего](certificates-a-record-builder-that-says-nothing-blocks-every-promise-above-it.md) - [Длину склейки ядро считает по одному куску за раз, а тремя слагаемыми — нет](certificates-concat-length-adds-one-piece-at-a-time-not-three.md) -- [Числа сайта тухнут той же правкой, что и словарь, а лечатся одной командой — которая под нагрузкой не успевает](site-numbers-go-stale-with-the-dictionary-and-one-command-cures-both.md) - [Цена утверждений линейна по числу ЭЛЕМЕНТАРНЫХ ДЕЙСТВИЙ внутри них, а не по числу утверждений, — поэтому одного дорогого виновника не находится, и переписывать надо не «самое дорогое», а самое частое](claim-cost-is-linear-in-elementary-actions-not-in-claims.md) - [Из хеша код не выводится: у средней функции flang вдвое больше содержания, чем влезает в адрес](code-cannot-be-derived-from-its-hash.md) - [`http.flang` считает Content-Length ЗНАКАМИ в обе стороны, и потому чинить одну сторону нельзя](content-length-is-counted-in-characters-on-both-sides.md) @@ -568,6 +578,7 @@ - [Свёртка под проекцией «Принципу свёртки» НЕ мешает: стена проходит по границе самой свёртки, а не по тому, как снят её результат](crypto-hashes-a-fold-under-a-projection-is-not-what-blocks-the-fold-principle.md) - [Модуль со списком `только` у ввозящих ломается НЕ там, где его правили: заводя функцию, снимай отчёт по каждому ввозящему](crypto-hashes-a-named-import-list-breaks-the-importer-not-the-edited-file.md) - [Доказанного мало: сторожа снимает ПАРА «доказано + пример»](crypto-keys-a-proved-postcondition-still-guards-without-an-example.md) +- [Кириллица в именах файлов вне flang/proof не прибавляется — храповик по ведомости, а не запрет](cyrillic-file-names-are-a-ledger-ratchet-outside-flang-proof.md) - [Вывод из спецификации работает там, где область сузили нарочно, — и у flang такая область уже есть: словарь между спеками](derivation-works-where-the-domain-was-narrowed-on-purpose.md) - [Таблица, разложенная на несколько строк ради поиска, расходится молча — и ловит это только тот, кто её ПЕРЕЧИСЛЯЕТ](derived-tables-of-one-fact-drift-apart-in-silence.md) - [Дизъюнкция — самый частый верхний вид цели в библиотеке (344 из 1011, доказано 4), но упирается она НЕ в дизъюнкцию](disjunction-is-the-most-common-goal-kind-but-not-the-bottleneck.md) @@ -594,11 +605,13 @@ - [Один пример снимает ВСЕ доказанные постусловия функции, а не одно](front-end-one-example-per-function-lifts-all-its-proven-guards.md) - [Охрана берётся не только из ВЕРХНЕГО `если`: замеры на стенде, приложениях и правиле приёмки спек](fspec-guard-copied-from-a-nested-if-and-from-a-substituted-let.md) - [Двадцать шесть спек из сорока двух не читаются НИ ОДНИМ существующим двоичным, и проверка спек красна — применили `неотрицательное`, не перепечатав семени](fspec-spec-catalog-is-unreadable-by-every-binary.md) +- [Разбор цели по условию закрывает места, но доли не двигает](goal-case-split-closes-sites-but-misses-the-numerator.md) - [Цель flang — доказуемость, доступная обычному программисту](goal-of-the-language.md) +- [Переписи сторожей берут имена только из позиции элемента списка, а вызовы — только из ключа run: подстрочный поиск лгал в обе стороны](guard-censuses-read-shortcuts-from-list-position-and-calls-from-run-keys.md) - [Ложное обещание о длине прячется в отчёте под видом недоказанного](guards-a-false-length-promise-hides-as-undeclared.md) - [Запас шагов — общий кошелёк замыкания, а не свойство файла](guards-step-budget-is-a-shared-purse.md) - [Сторож, который поймал бы отставание, сам не заводился — и отставание накопилось](guards-the-guard-that-would-have-caught-it-was-itself-red.md) -- [Греп по словам выдал отклонённый пуш за зелёный: крючок печатает заглавными](a-grep-on-words-let-a-rejected-push-look-green.md) +- [Перепись перечней, набранных руками, не держит списка мест — иначе стала бы сто шестым перечнем; без двоичного она лжёт](hand-written-lists-census-keeps-no-list-of-places-and-needs-the-binary.md) - [Чистота обработчика превращает восстановление из журнала в одну свёртку](handler-purity-turns-journal-recovery-into-one-fold.md) - [Предусловие принадлежит функции границы, а не внутренней: ветка «если» его не снимает](host-boundary-a-precondition-belongs-to-the-boundary-function-not-the-inner-one.md) - [У границы слоёв два стыка, а не один: словарь поручений и рукописный хозяин над напечатанным кодом](host-boundary-the-second-junction-is-the-printed-one-not-the-order-dictionary.md) @@ -609,6 +622,7 @@ - [Индукция по телу-`разбор` цепляется, только когда разбирают ДОВОД-сумму и названы ВСЕ варианты](induction-on-match-needs-a-parameter-scrutinee-and-all-variants-named.md) - [Целочисленное деление не даёт ядру `нат` — границу приходится называть постусловием](integer-division-does-not-give-the-kernel-nat.md) - [Целость терма не проходит через сумму и произведение, и столбик хеша заперт не списком целых](integrality-does-not-pass-through-a-sum-or-a-product.md) +- [На негодном UTF-8 формы над строкой расходятся на две меры — октеты и знаки, — и всякое утверждение, сшитое из них, ложно](invalid-utf8-splits-string-forms-into-two-measures.md) - [Совпадение вывода знак в знак не даёт снести старый прогон — считать надо режимы, а не строки](javascript-out-matching-output-does-not-mean-the-old-guard-can-go.md) - [Печать в JavaScript упирается не в рантайм внутри модуля, а в отсутствие границы входа: 102 программы из 102 разойдутся с Node](javascript-printing-is-blocked-by-the-entry-boundary-not-by-the-runtime.md) - [От JavaScript остаётся только цель печати, второе мнение отменено вместе с ловушкой Томпсона](javascript-stays-only-as-a-print-target.md) @@ -632,6 +646,7 @@ - [Вынос шага свёртки в обычную функцию открыл шаг и УРОНИЛ доказательство у самой свёртки: 16 → 15](math-lifting-a-fold-step-out-of-a-lambda-cost-one-proof-and-gained-none.md) - [Двух заглушек не хватает обещанию-границе: и `0`, и `1` лежат внутри границы, поэтому обе его переживают](math-two-stubs-cannot-catch-a-bound-shaped-promise.md) - [Слияние двух редакций одного файла роняет общий кусок, и разбор этого не видит](merging-two-editions-drops-the-shared-part.md) +- [Откуда приедет модуль, сторож пересчитывает обходом каталогов, а не спрашивает у двоичного, — чтобы видеть подмену, когда подменён сам](module-origin-is-recomputed-by-walking-directories-not-asked-of-the-binary.md) - [Столкновения имён в замыкании компилятора считаются обходом текста за 0,1 с — там же, где связывание отвечает за 6 минут](name-collisions-are-counted-by-a-text-walk-in-tenths-of-a-second.md) - [`нат` в объявлении снимает отказ по целости, но почти не добавляет доказанных мест](nat-in-a-declaration-removes-integrality-refusals-not-bounds.md) - [Объявить `нат` и снять проверку из напечатанного кода удаётся только там, где вызывающий уже даёт натуральное: один случай из шести](nat-removes-a-guard-only-when-the-caller-already-gives-a-natural.md) @@ -650,8 +665,10 @@ - [Из двух таблиц слов на flang сторожится одна, и вторая уже отстала на четыре фразы](only-one-of-two-word-tables-is-guarded-and-the-other-is-four-phrases-behind.md) - [Ход переписки заводит одно правило из шести, и недоказанных с ним — одно из восьми](only-the-equality-rule-walks-and-it-is-one-obligation-in-eight.md) - [Чужие пакеты надо хранить: из трёх укладов два — это один в два слоя, а третий не про наше десятилетие](other-peoples-packages-must-be-stored.md) +- [Сторож длинной постоянной задаёт три разных вопроса, и разрезать литерал на соседние — не лечит: предел C99 считается после склейки](overlong-string-guard-asks-three-different-questions-and-concatenation-does-not-help.md) - [Параметрический тип в языке ЕСТЬ, и упирается в него сегодня одиннадцать мест — все объявления, читающие тип именем; ссылка на процесс к ним не относилась никогда](parametric-types-exist-and-eleven-places-depend-on-them.md) - [Девять мест библиотеки обваливаются на «не числе» и пустой строке: встроенные формы `символ`, `элемент` и `код символа` частичны, а тип этого не запрещает](partial-builtin-forms-crash-the-stdlib-on-nan-and-the-empty-string.md) +- [Перестановка двух блоков честной записи — самая дешёвая проба на вердикт, зависящий от порядка](permuting-two-blocks-of-an-honest-record-is-the-cheapest-test-for-an-order-dependent-verdict.md) - [Планы не судит никто, и в отличие от процессов двоичный об этом молчит — двенадцать нарочных подделок из тринадцати проходят кодом 0](plans-are-not-judged-at-all-and-unlike-processes-the-binary-says-nothing.md) - [Перепечатка 30 августа увезла в семя круг машины БЕЗ батута — и всякий план `flang io` умирает на шаге длиннее 6 666 витков; до возврата батута планы зовут прежним двоичным](plans-run-on-the-previous-seed-until-the-machine-loop-gets-its-trampoline-back.md) - [Перенос оракула яруса III — не одна задача, а пять разных, и две из них другого рода](porting-the-tier-three-oracle-splits-into-five-different-tasks.md) @@ -660,8 +677,10 @@ - [Печать обязана спросить у проверки, а урезанное подмножество — назвать себя числом, а не молчанием](printing-must-ask-the-checker-and-name-its-subset-as-a-number.md) - [Печать в C и в Python выводит двунаправленные управляющие сырыми — в комментарий шапки](printing-to-c-and-python-emits-bidirectional-controls-raw.md) - [Печать в C ищет исходники рантайма рядом с ДВОИЧНЫМ, и в дереве репозитория это работает по совпадению раскладки](printing-to-c-looks-for-runtime-sources-next-to-the-binary.md) +- [У сторожа чисел в прозе пять приборов и закрытый список, а цитату от приметы отличает он сам, а не пишущий](prose-numbers-guard-has-five-closed-instruments-and-tells-a-quote-from-a-mark.md) +- [Вердикт «доказуем» снимается ловушкой, а не grep-ом по имени, и все четыре проверки гоняются всегда](provability-verdict-measures-by-a-trap-and-runs-all-four-checks-always.md) +- [У ведомости доказанного знаменатель сверяется точно, а числитель только датируется — и первая редакция сверки врала сама](proved-share-ledger-denominator-is-exact-and-numerator-is-only-dated.md) - [Втаскивание модуля в самоприменённый компилятор стоит не по размеру модуля, а по числу столкновений имён с уже втащенными](pulling-a-module-into-the-self-hosted-compiler-pays-for-meetings-not-size.md) -- [Разбор цели по условию закрывает места, но доли не двигает](goal-case-split-closes-sites-but-misses-the-numerator.md) - [Отпечаток, снятый заново, делает красное зелёным, не перепечатав ни байта](re-taking-a-fingerprint-turns-red-green-without-reprinting.md) - [Заявленных чисел о дереве 1693 строки в 89 файлах, и делятся они на три кучи: перемеряемое за минуту, перемеряемое за часы и не перемеряемое никогда](recount-claimed-numbers-have-three-kinds-and-only-one-can-be-rechecked.md) - [У общего двоичного нет воспроизводимой родословной: время сборки известно, дерево — нет, а называемый коммит на два часа его моложе](recount-the-shared-binary-has-no-reproducible-pedigree.md) @@ -670,13 +689,18 @@ - [Снятый в одном месте прувер-переписыватель немедленно переезжает в другое](removing-the-rewriting-prover-from-one-place-moves-it-to-another.md) - [Переименовать заметку стоит не переименования, а правки ссылающихся: 191 имя потянуло 443 ссылки в 234 файлах](renaming-a-note-costs-the-referrers-not-the-rename.md) - [Кэш перепечатки по отпечатку неверен не редко, а по устройству: зависимость идёт ВВЕРХ по ввозам, а ключ смотрит вниз](reprint-cache-key-cannot-name-the-dependency-that-exists.md) +- [Снятие работы по памяти неотличимо от отказа по существу, пока запас раннера не назван числом](runner-memory-headroom-is-named-as-a-number-on-every-run.md) - [Прогон примеров по каталогу копит память до 44 ГиБ и гибнет от нехватки, а тот же корпус по одному файлу проходит за 19 минут малой памятью](running-examples-by-directory-accumulates-memory-by-file-does-not.md) +- [Дисциплину семени стерегут два сторожа — по словам и по разбору, — и второй под своим пределом слеп, о чём честно говорит](seed-discipline-is-guarded-twice-by-words-and-by-parsing.md) - [Откат применения прошёл по компилятору и остановился на его границе — в дереве осталось вчетверо больше](seed-discipline-revert-covered-the-compiler-and-left-the-tree.md) - [Словарь семени лежит в самом напечатанном C, и он отвечает за секунду там, где компилятор просит четверть часа](seed-word-tables-tell-in-a-second-what-the-seed-can-parse.md) - [Ёлочки внутри имени примера роняют разбор всего файла, и отказ не называет ни файла, ни примера](service-files-nested-guillemets-in-an-example-name-break-the-lexer.md) - [Прибавка снятых проверок равна числу ДОКАЗАННЫХ постусловий у функций, получивших первый пример — считается по ведомости, без второго прогона печати](service-files-removed-checks-equal-proven-postconditions-of-newly-exampled-functions.md) +- [Поиск файла настроек обрывается на корне проекта, потому что поиск модулей этого не делал — и однажды взял чужой черновик](settings-file-search-stops-at-the-project-root-because-module-search-did-not.md) - [SHA-256 без единой битовой операции стоит 925 195 шагов интерпретатора на блок, и это уложилось в предел только после трёх названных правок](sha256-without-bit-operations-costs-925-thousand-steps-per-block.md) +- [Пробу оболочки нельзя снять с одного конца: труба обязана остаться голой байт в байт, а клавиши видны только псевдотерминалу](shell-probe-judges-the-pipe-and-the-pty-separately.md) - [Тихая потеря байтов у файлов была ДВУМЯ бедами в разных местах, и лечатся они разным лекарством](silent-byte-loss-in-files-was-two-failures-with-two-cures.md) +- [Числа сайта тухнут той же правкой, что и словарь, а лечатся одной командой — которая под нагрузкой не успевает](site-numbers-go-stale-with-the-dictionary-and-one-command-cures-both.md) - [«Результат сортировки не убывает» — утверждение ЛОЖНОЕ, и ложно оно ровно на «не числе»](sort-result-is-non-decreasing-is-false-on-not-a-number.md) - [Разложение конъюнкции в заключении на арифметике даёт ноль: тридцать две части, ни одной доказанной](splitting-a-conjunction-in-the-conclusion-buys-nothing-on-arithmetic.md) - [«Меньше» — это не «не больше И не равно»: разложение ложно на минус нуле](strict-less-is-not-not-greater-and-not-equal.md) @@ -686,11 +710,13 @@ - [Содержательное и доказуемое почти не пересекаются: 83 содержательных утверждения, 19 доказанных, общих девять](substantive-and-provable-claims-barely-overlap.md) - [Переключение слоя не всегда опускает потолок: у `sets` он ВЫРОС, и это не провал](switching-a-layer-does-not-always-lower-the-ceiling.md) - [Синтез из спецификации упирается в 75 узлов дерева — и медианная функция нашей библиотеки ровно этого размера](synthesis-from-a-spec-hits-75-tree-nodes.md) +- [Номер задачи проверяется без двоичного и сразу по четырём каталогам — двойник спрятался в закрытых](task-numbers-are-checked-without-the-binary-across-four-directories.md) - [Остановки на 807 секунд не было: это четыре стадии подряд, а не одно событие](the-807-second-stall-was-four-stages-not-one-event.md) - [Обмер живого в арене делает квадратом ЛЮБУЮ свёртку с растущим накопителем](the-arena-liveness-check-makes-every-accumulating-fold-quadratic.md) - [Двоичный уже отвечает про любую свою функцию, и новую команду под это заводить не надо](the-binary-already-answers-about-any-of-its-functions-through-the-runner.md) - [Двоичный хозяин обрывает содержимое на первом нулевом октете, и потому драйвер PostgreSQL по проводу не идёт вовсе](the-binary-host-cuts-content-at-the-first-zero-octet.md) - [Двоичный хозяин не знает поручения «Запустить процесс с вводом», хотя словарь его объявляет](the-binary-host-does-not-know-run-with-input.md) +- [Экран двоичного хозяина — управляющий терминал, и трубу он экраном не считает](the-binary-hosts-screen-is-the-controlling-terminal.md) - [У двоичного нет целых проверок, а не только более слабая ведомость, — и его собственная справка об этом молчит](the-binary-is-silent-about-checks-it-does-not-have.md) - [Двоичный `flang lsp` не отвечает, пока стандартный ввод открыт, — и потому редактору не годится, хотя побайтовую сверку проходит](the-binary-lsp-answers-nothing-while-stdin-stays-open.md) - [Прогонщик двоичного открывает ВСЁ замыкание компилятора — новая команда нужна только там, где у ответа свой вид вывода](the-binary-runner-opens-the-whole-compiler-closure.md) @@ -703,6 +729,7 @@ - [Срок потомка у хозяина — главное препятствие для переноса долгих проверок, и в справке его нет](the-child-deadline-is-the-main-obstacle-for-long-checks.md) - [Сверка эталона командной строки не ловила забытую команду: на ключе свидетель отказывает раньше, чем доходит до команды](the-cli-reference-check-missed-a-forgotten-command.md) - [Закрытый список правил сверщика разошёлся с ядром: было восемь, стало тринадцать](the-closed-rule-list-of-the-checker-drifted-from-the-kernel.md) +- [Компилятор принимает имя в ёлочках, в прямых кавычках и без кавычек одинаково — провал новичка в проводнике был не от кавычек, а от вызова вне функции](the-compiler-takes-a-name-in-guillemets-in-quotes-and-bare-alike.md) - [Делимая часть суда ядра — сотые доли процента, а вся его цена сидит в неподвижной точке «Закрыть без теорем»](the-divisible-part-of-the-kernel-judgment-is-a-fraction-of-a-percent.md) - [Ветвь «пусто» у тела-`разбора` закрыта ОБЕИМИ записями охраны, и литерал не помогает](the-empty-branch-of-a-match-is-shut-in-both-spellings.md) - [Двоичный расходится с Node на корпусе не печатью, а границей входа: у уже втащенной цели C расходится 161 программа из 163, и всегда одним и тем же блоком](the-entry-boundary-not-printing-splits-the-binary-from-node.md) @@ -761,41 +788,15 @@ - [Типизация узла сама по себе чинит одно ребро рекурсии из шести, а на двух из пяти узел едет неизменным](typed-ast-typing-alone-fixes-one-recursion-edge-in-six.md) - [TypeScript уже проверяет нашу печать в JavaScript: девятая цель купила бы перенос 702 пометок из комментария в синтаксис, и четверть из них строгому режиму всё равно не годится](typescript-target-buys-almost-nothing.md) - [`pull` у Unison привозит весь код, а не ссылки: хеш — способ не дублировать, а не способ не хранить](unison-pull-brings-all-the-code-not-references.md) +- [Все производные места версии сверяются с одним источником дёшево — так, чтобы стоять в хуке перед пушем](version-derivations-are-checked-cheaply-against-one-source.md) - [`нат` в теле производят ровно два места — числовой литерал и `длина`, поэтому счётчик, посчитанный арифметикой, под точный шаг не подставить](walk-fuel-is-carried-as-a-list-not-as-a-number.md) - [Всякое «ядро этого не умеет», снятое `bootstrap/flang`, — утверждение о семени, а не о языке: трёх решающих правил из двенадцати в семени нет](what-the-kernel-cannot-do-is-a-statement-about-the-seed-not-the-language.md) - [Из семи утверждений, которые ядро доказывало в трёх строковых модулях, пять оказались даровыми — ядро берёт ровно тот класс, который переживает подмену тела заглушкой](what-the-kernel-proves-is-almost-exactly-what-is-gratis.md) - [Запись ответов свидетеля снимается ДО удаления, и замораживать надо не только ответы, но и список входов](witness-answers-must-be-recorded-before-the-deletion.md) - [Разбиение имени на слова в эталонах печати сделано таблицей ASCII, а у свидетеля — классами Юникода, и на любой не-кириллической букве они расходятся](word-splitting-is-ascii-in-flang-and-unicode-in-the-witness.md) -- [Компилятор принимает имя в ёлочках, в прямых кавычках и без кавычек одинаково — провал новичка в проводнике был не от кавычек, а от вызова вне функции](the-compiler-takes-a-name-in-guillemets-in-quotes-and-bare-alike.md) -- [Подделочная программа и лгущая запись — разные вещи, и в знаменатель они идут по-разному](a-forgery-and-a-forged-record-are-different-things.md) ## Ещё не разобранное -- [Заголовок «ВЗЯТО N ИЗ M» рядом с таблицей, из которой он вычисляется, лжёт при первой же смене ряда](a-hand-typed-score-next-to-its-table-drifts-silently.md) -- [Предел памяти на прогон — контрольная группа за воротами, и после падения он объясняет, а не пишет «Killed»](a-memory-limit-per-run-is-a-cgroup-behind-a-gate-with-an-explanation.md) -- [Число, полученное прибором вне хранилища, — не замер, а слух: 61 % работы ячеек жил только во временном каталоге](a-number-taken-outside-the-repository-is-a-rumour-not-a-measurement.md) -- [Разошедшееся опубликованное число либо устарело, либо было неверным — различает их только пересчёт по дереву коммита съёмки](a-published-number-is-stale-or-wrong-and-only-a-recount-at-the-snapshot-tells-which.md) -- [Прогон на чужой машине превращает отсутствующий тулчейн из пропуска в провал — иначе половина целей не проверена ни разу](a-remote-run-turns-a-missing-toolchain-into-a-failure-not-a-skip.md) -- [На негодном октете прогонщик обязан отказать одинаково на всех целях — а было пять разных поведений, и отказом не было ни одно](a-runner-must-refuse-a-bad-octet-identically-across-nine-targets.md) -- [Пределы печати точки раскрутки — одна запись на оба пути, и совпадение проверяется, а не обещается](bootstrap-reprint-limits-are-one-record-shared-with-the-print-script-and-checked.md) -- [Кириллица в именах файлов вне flang/proof не прибавляется — храповик по ведомости, а не запрет](cyrillic-file-names-are-a-ledger-ratchet-outside-flang-proof.md) -- [Переписи сторожей берут имена только из позиции элемента списка, а вызовы — только из ключа run: подстрочный поиск лгал в обе стороны](guard-censuses-read-shortcuts-from-list-position-and-calls-from-run-keys.md) -- [Перепись перечней, набранных руками, не держит списка мест — иначе стала бы сто шестым перечнем; без двоичного она лжёт](hand-written-lists-census-keeps-no-list-of-places-and-needs-the-binary.md) -- [На негодном UTF-8 формы над строкой расходятся на две меры — октеты и знаки, — и всякое утверждение, сшитое из них, ложно](invalid-utf8-splits-string-forms-into-two-measures.md) -- [Откуда приедет модуль, сторож пересчитывает обходом каталогов, а не спрашивает у двоичного, — чтобы видеть подмену, когда подменён сам](module-origin-is-recomputed-by-walking-directories-not-asked-of-the-binary.md) -- [Сторож длинной постоянной задаёт три разных вопроса, и разрезать литерал на соседние — не лечит: предел C99 считается после склейки](overlong-string-guard-asks-three-different-questions-and-concatenation-does-not-help.md) -- [У сторожа чисел в прозе пять приборов и закрытый список, а цитату от приметы отличает он сам, а не пишущий](prose-numbers-guard-has-five-closed-instruments-and-tells-a-quote-from-a-mark.md) -- [Вердикт «доказуем» снимается ловушкой, а не grep-ом по имени, и все четыре проверки гоняются всегда](provability-verdict-measures-by-a-trap-and-runs-all-four-checks-always.md) -- [У ведомости доказанного знаменатель сверяется точно, а числитель только датируется — и первая редакция сверки врала сама](proved-share-ledger-denominator-is-exact-and-numerator-is-only-dated.md) -- [Снятие работы по памяти неотличимо от отказа по существу, пока запас раннера не назван числом](runner-memory-headroom-is-named-as-a-number-on-every-run.md) -- [Дисциплину семени стерегут два сторожа — по словам и по разбору, — и второй под своим пределом слеп, о чём честно говорит](seed-discipline-is-guarded-twice-by-words-and-by-parsing.md) -- [Поиск файла настроек обрывается на корне проекта, потому что поиск модулей этого не делал — и однажды взял чужой черновик](settings-file-search-stops-at-the-project-root-because-module-search-did-not.md) -- [Пробу оболочки нельзя снять с одного конца: труба обязана остаться голой байт в байт, а клавиши видны только псевдотерминалу](shell-probe-judges-the-pipe-and-the-pty-separately.md) -- [Номер задачи проверяется без двоичного и сразу по четырём каталогам — двойник спрятался в закрытых](task-numbers-are-checked-without-the-binary-across-four-directories.md) -- [Все производные места версии сверяются с одним источником дёшево — так, чтобы стоять в хуке перед пушем](version-derivations-are-checked-cheaply-against-one-source.md) -- [Починка, пролежавшая через разрез файла на мелкие функции, переписывается заново — и выходит дешевле патча](a-fix-that-waited-through-a-refactor-is-rewritten-not-rebased.md) -- [Перестановка двух блоков честной записи — самая дешёвая проба на вердикт, зависящий от порядка](permuting-two-blocks-of-an-honest-record-is-the-cheapest-test-for-an-order-dependent-verdict.md) -- [Экран двоичного хозяина — управляющий терминал, и трубу он экраном не считает](the-binary-hosts-screen-is-the-controlling-terminal.md) ## Как добавлять diff --git a/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md new file mode 100644 index 000000000..14bd05fa9 --- /dev/null +++ b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md @@ -0,0 +1,39 @@ +# Два приёма сверщика девять дней стояли без теоремы состоятельности, потому что число приёмов «81» переписывалось в прозе от руки + +Проверяющая программа на C принимает блок «вывод» по закрытому списку приёмов +`шаг_вывода`; приёмка Lean держит свой закрытый список, и теорема +«состоятельность» доказана ровно для него. Сколько приёмов у сверщика и сколько +из них в приёмке, до 5 октября 2026 знала только проза: «81, покрыто 76» — в +шапках `Acceptance.lean` и `Consistency.lean`, в `docs/road-to-1-0.md`, в задаче +1183. 26 сентября задача 1435 добавила в сверщик Н6 и О9; прозу не тронули, в +приёмку их не внесли, и девять дней у двух приёмов не было теоремы — при зелёных +проверках. + +**Чем подтверждено.** Прибор `flang/proof/lean/rules-guard.fscript`, ветка +`a/checker-rules-are-sound-in-lean` от `6b459ded0`, 5 октября 2026: + + +- до правки: приёмов 83 (не 81), в приёмке 76, вне приёмки 7 — Р2, Р3, Р5, Р6, + Выч и незамеченные Н6, О9; в долге с номером задачи 5; + +- после правки приёмки: в приёмке 78, вне приёмки 5, в долге 5, сторож + `lean-rules:check` зелен, `«покрыто» = 78` в `Consistency.lean` проверено + `decide`; +- отрицательный контроль: три порчи копий (`lean-rules:forgery`) — убрано правило + Н5 из приёмки, дописан приём без теоремы в сверщик, вписан принятый приём в + долг — покраснели все три. + +Ночная сверка вердиктов (`lean-crosscheck.yml`) эти два приёма видела: в прогоне +2 октября «вне приёмки» стояло «О9 7, Н6 5» рядом с «Выч 60». Но «вне приёмки» +читается как известный долг, а не как новая дыра: отличить их могла бы только +таблица долга, которой не было. + +**Чем ограничено.** Сторож сличает ИМЕНА приёмов, а не их смысл: что одноимённый +приём сверщика и правило приёмки делают одно и то же, по-прежнему проверяет +сверка вердиктов на наборе проб. И он читает `шаг_вывода` по форме +`strcmp(имя, "…")` между первым именованным приёмом и читателем шага; приём, +разобранный иначе, он не увидит — потому порог «меньше пятидесяти имён — разбор +сломан» и подлог с дописанным приёмом. + +Связано: [[a-hand-copied-wall-list-goes-stale-in-silence]], +[[checks-that-do-not-check]], [[zero-axioms]] From c6c131994146f81df814c8560b6621c5ef1fdcbd Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Mon, 5 Oct 2026 21:27:26 +0000 Subject: [PATCH 5/8] fix(checker): a case split refuses its condition under a binder 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. --- ...-has-a-lean-theorem-or-a-named-debt-row.md | 16 +++++++++ docs/flang/proof/forgeries.md | 1 + .../flang/proof/known-soundness-violations.md | 18 ++++++++++ docs/road-to-1-0.md | 2 +- ...the-body-by-lines-and-stay-outside-lean.md | 15 ++++---- docs/zettel/README.md | 3 +- ...der-a-binder-and-proved-a-false-formula.md | 34 +++++++++++++++++++ flang/proof/checker/checker.c | 8 +++++ .../case-split-under-a-binder.flang | 7 ++++ ...ry-case-split-captures-a-bound-name.record | 27 +++++++++++++++ flang/proof/forgeries/manifest.tsv | 1 + flang/proof/lean/Acceptance.lean | 6 +++- flang/proof/ratchets.txt | 2 +- flang/proof/tables/consistency-violations.tsv | 1 + scripts/ledgers/file-name-words.txt | 1 + 15 files changed, 132 insertions(+), 10 deletions(-) create mode 100644 docs/zettel/a-case-split-pasted-the-condition-as-text-under-a-binder-and-proved-a-false-formula.md create mode 100644 flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang create mode 100644 flang/proof/checker/tests/records/corpus/forgery-case-split-captures-a-bound-name.record diff --git a/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md index b0f7e43b6..59039c086 100644 --- a/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md +++ b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md @@ -78,6 +78,11 @@ `«покрыто-число» : «покрыто» = 78` проверено `decide`; аксиомы теоремы «состоятельность» — три стандартные. Сборка цепочки Lean на машине разработки: `Term.lean` 51 с, `Acceptance.lean` 16 с, `Consistency.lean` 20 с. +Полная сверка `flang/proof/lean/run.fscript` (632 с, Lean 4.34.0 по +`lean-toolchain`): +ловушек 57, Lean отверг 57; строк перечня 112, с леммой 112; пар 273, блоков 1513, +расхождений 0; вне приёмки — Выч 60, Р5 24, Р6 7 (на 2 октября там же стояли О9 7 +и Н6 5). Пять приёмов остаются долгом, и причина у каждого названа в таблице: Выч — второй вычислитель языка внутри сверщика (задача 1183); Р2, Р3 — посылками берут @@ -85,6 +90,17 @@ Р6 — тело функции читается по строкам, читатель записи многострочного тела не собирает (задача 4791). +### 3.1. Побочная находка: Р2/Р3 подставляли условие под связыватель + +Оценивая цену леммы Р2/Р3 в модели (подстановка без захвата), проба показала, +что у сверщика этого условия не было: условие В подставлялось текстом во все +вхождения, и ложная формула из двух свёрток проходила кодом 0 +(`docs/flang/proof/known-soundness-violations.md`, +`case-split-substitutes-under-a-binder`). Р2 и Р3 теперь отказывают на любом +связывателе в формуле; подделка `forgery-case-split-captures-a-bound-name` стоит +в наборе (класс `record-lies`, храповик `forgeries` 38 → 39); честных записей +корпуса с таким блоком нет (формул Р2/Р3 в корпусе три, со связывателем — ноль). + ## 4. Последствия - Число «приёмов N, покрыто M» в прозе больше не пишется от руки: его печатает diff --git a/docs/flang/proof/forgeries.md b/docs/flang/proof/forgeries.md index bc329aff7..dfe0f14a3 100644 --- a/docs/flang/proof/forgeries.md +++ b/docs/flang/proof/forgeries.md @@ -86,3 +86,4 @@ | `poddelka-raznost-bez-poryadka` | `record-lies` | разность под порядком (правило Н12): вывод «( цена минус скидка ) не меньше 0» подсунут трём функциям, у которых допущения «скидка не больше цена» нет — оно о другой паре, перевёрнуто либо отсутствует; проверяющая программа обязана назвать «порядок не записан» | | `poddelka-razv2-sebya` | `record-lies` | развёртка Разв2 спрашивает о захвате имён: тело «э» встаёт под квантор цели «для всех э из [1, 2] : не ( э больше результат )», и связанное э цели ловит свободное э тела; при э = 0 обещание ложно | | `poddelka-razv3-raznost` | `record-lies` | развёртка Разв3 подставляет доводы разом: «Разность» от б и а при теле «а минус б» есть «б минус а», а подстановка по одному дала бы «а минус а»; при а = 0, б = 1 результат 1, обещано 0 | +| `forgery-case-split-captures-a-bound-name` | `record-lies` | разбор случаев по условию (Р2, Р3) не подставляет условие текстом под связыватель: «(э больше 0)» в свёртке по [1,0] истинно на одном элементе и ложно на другом, обе половины «да»/«нет» замыкаются счётом, а формула ложна — и язык при запуске её нарушает; проверяющая программа обязана отказать на связывателе в формуле | diff --git a/docs/flang/proof/known-soundness-violations.md b/docs/flang/proof/known-soundness-violations.md index 077a6b0fa..20d19e70f 100644 --- a/docs/flang/proof/known-soundness-violations.md +++ b/docs/flang/proof/known-soundness-violations.md @@ -49,6 +49,24 @@ run` на нуле нарушает постусловие. Ядро отказ независимый checker на этой записи отвечает кодом 3. С 0.7.24 цитата принимается только после снятия ограничения; пробы — в `flang/proof/probes/syllogism/`. Задача 4573. +## `case-split-substitutes-under-a-binder` — закрыто + +Разбор случаев по условию (приёмы Р2 и Р3 проверяющей программы) восстанавливал +условие В из первого расхождения формулы с половиной и подставлял его ТЕКСТОМ во +все вхождения, не спрашивая, стоит ли вхождение под связывателем. Под +связывателем у куска нет одного значения: в «(свёртка [1,0] начиная с 0 как а и э +→ (если (э больше 0) то э минус а иначе а минус э)) меньше 1» условие истинно на +первом элементе и ложно на втором, свёртка даёт 1, и формула ложна; с «да» и с +«нет» на месте условия свёртка даёт −1, и обе половины замыкаются счётом (Выч). +Язык при запуске такое постусловие нарушает. Запись с таким блоком проверяющая программа принимала +кодом 0 и словами «числятся доказанными 1» (проба 5 октября 2026, ветка +`a/checker-rules-are-sound-in-lean`). С этого же дня Р2 и Р3 отказывают на любом +связывателе в формуле (закрытый список ядра, тот же, что у Э3 и Т2); подделка — +`forgery-case-split-captures-a-bound-name` в наборе подделок, класс `record-lies`, +ответ 1. Честных записей корпуса это не задело: формул Р2/Р3 в корпусе три, со +связывателем — ни одной. Приёмка Lean приёмов Р2 и Р3 не судит (задача 4791), и +расхождение вердиктов её поэтому не ловило. Задачи 4791, 1183. + ## `verdicts-c-lean` — закрыто Проверяющая программа на C и приёмка Lean подставляют доводы развёртки diff --git a/docs/road-to-1-0.md b/docs/road-to-1-0.md index 00b7ea1bc..80556776b 100644 --- a/docs/road-to-1-0.md +++ b/docs/road-to-1-0.md @@ -118,7 +118,7 @@ Homebrew с тем, что собрал сам конвейер выпуска; **15 сент, позже** (задача 1130; `sh flang/proof/lean/run.sh`, ветка `a/lean-o6-ch5-representable-and-number-text`): **теорема о состоятельности есть для 76 правил из 81** — прибавились О6 (окружение знает факт языка «числа-представимы») и Ч5 (модель терма переводит число в текст). Сверка вердиктов (508 подделок, 237 честных; 242 пары, 1503 блока): расхождений 0; вне приёмки 91 блок — Выч, Р5, Р6 и запреты; ловушек 37 из 37. К↑ и Разв3 Lean теперь судит в самом прогоне — проба `развёртка/box-round-trip-by-assumption` с базой Т1. -**5 окт** (задача 1435 → ADR-0064; `bootstrap/flang run-script lean-rules:numbers`, ветка `a/checker-rules-are-sound-in-lean`): приёмов `шаг_вывода` у сверщика **83**, а не 81 — Н6 и О9 вошли в сверщик 26 сентября (задача 1435) и девять дней не имели теоремы, пока число 81 переписывалось в прозе от руки. **Теорема о состоятельности есть для 78 приёмов из 83**: Н6 и О9 вошли в приёмку (`Acceptance.lean`, `Consistency.lean`; О9 — под фактом окружения «списки-коротки» в `Record.lean`), ловушек стало 55 файлов-искажений (две новые: 85 — О9 с шагом в двойку, 86 — Н6 без второй посылки). Пять приёмов без теоремы — Выч, Р2, Р3, Р5, Р6 — стоят строками долга в `flang/proof/tables/lean-acceptance-debt.tsv` с номером задачи (1183, 4791); сторож `flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, работа `lean-rules-guard` в `ci.yml` и шаг в `lean-crosscheck.yml`) краснеет на приёме без приёмки и без строки долга, на уплаченном долге и на имени, которого нет у сверщика; три подлога на копиях (`lean-rules:forgery`) пойманы все три. +**5 окт** (задача 1435 → ADR-0064; `bootstrap/flang run-script lean-rules:numbers`, ветка `a/checker-rules-are-sound-in-lean`): приёмов `шаг_вывода` у сверщика **83**, а не 81 — Н6 и О9 вошли в сверщик 26 сентября (задача 1435) и девять дней не имели теоремы, пока число 81 переписывалось в прозе от руки. **Теорема о состоятельности есть для 78 приёмов из 83**: Н6 и О9 вошли в приёмку (`Acceptance.lean`, `Consistency.lean`; О9 — под фактом окружения «списки-коротки» в `Record.lean`), ловушек стало 55 файлов-искажений (две новые: 85 — О9 с шагом в двойку, 86 — Н6 без второй посылки). Пять приёмов без теоремы — Выч, Р2, Р3, Р5, Р6 — стоят строками долга в `flang/proof/tables/lean-acceptance-debt.tsv` с номером задачи (1183, 4791); сторож `flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, работа `lean-rules-guard` в `ci.yml` и шаг в `lean-crosscheck.yml`) краснеет на приёме без приёмки и без строки долга, на уплаченном долге и на имени, которого нет у сверщика; три подлога на копиях (`lean-rules:forgery`) пойманы все три. Сверка вердиктов (`bootstrap/flang io flang/proof/lean/run.fscript`, 632 с, Lean 4.34.0): 273 пары, 1513 блоков, расхождений 0, ловушек 57 из 57; вне приёмки остались Выч 60, Р5 24, Р6 7 — О9 (7 блоков) и Н6 (5 блоков) из списка ушли в «оба приняли». **Чего нет.** Теоремы для пяти приёмов из 83 — Выч, Р2, Р3, Р5, Р6 (строки долга, задачи 1183 и 4791) — и для Разв1 по строке тела (причины — в шапке `Acceptance.lean`, задачи 1130, 4058, 6432). Теоремы о самом `checker.c`: код с моделью связан сверкой вердиктов на наборе, а не выводом. Модель значений округляет «грубо», не по binary64, и её совпадение с вычислителем не доказано (ADR-0041 §2.3). Чтение текста записи (`flang/proof/lean/RecordReader.lean`) стоит вне теоремы. diff --git a/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md index b2f3c5818..5e4a7a0b3 100644 --- a/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md +++ b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md @@ -52,8 +52,12 @@ $ bootstrap/flang run-script lean-rules:numbers вне приёмки, блок с Р2/Р3 всё равно упирается в Выч. Сама же лемма приёма — «обе половины истинны, значит истинна Ф» — требует в модели поиска куска В по первому расхождению и подстановки без захвата; у проверяющей программы - подстановка текстовая (`вставить_вместо`) и о связывателях над В она не - спрашивает. + подстановка текстовая (`вставить_вместо`), и до 5 октября 2026 о связывателях + над В она не спрашивала — подделка `forgery-case-split-captures-a-bound-name` + проходила кодом 0 (`docs/flang/proof/known-soundness-violations.md`, + `case-split-substitutes-under-a-binder`). Теперь Р2 и Р3 отказывают на любом + связывателе в Ф, и приёмке Lean достаточно того же отказа: без связывателей + замена В на литерал — подстановка без захвата по построению. ## Что должно быть @@ -65,10 +69,9 @@ ADR-0064). Для четырёх приёмов это значит: строкой), в модели есть разбор списка списочного сорта, и приёмка принимает шаг «результат равен Т» при факте пустоты того же списка; - Р2, Р3 — приёмка восстанавливает В из первого расхождения разобранных деревьев - Ф и о1, проверяет, что В не стоит под связывателем, связывающим его свободное - имя, и что замены В на «да» и «нет» дают о1 и о2; лемма — разбор случаев по - значению В в мире. Приёмка здесь строже проверяющей программы (она захвата не - спрашивает), и это надо назвать в шапке `Acceptance.lean`. + Ф и о1, отказывает на связывателе в Ф (как теперь и проверяющая программа) и + проверяет, что замены В на «да» и «нет» дают о1 и о2; лемма — разбор случаев по + значению В в мире, без захвата по построению. Либо, если цена названа и решено не платить, — строка долга остаётся, а в ADR стоит довод с числом строк Lean. diff --git a/docs/zettel/README.md b/docs/zettel/README.md index 35e5deeb3..62aee883d 100644 --- a/docs/zettel/README.md +++ b/docs/zettel/README.md @@ -109,6 +109,7 @@ - [Три факта о длине строки дали три утверждения на весь корпус, и самым дорогим из трёх был не факт, а место, где факт читается](three-length-facts-gave-three-statements.md) - [Прослеживаемость собирается из того, что уже лежит в дереве: постусловие, пример и запись доказательства сшиваются по трём ключам, и разрывов сегодня 62 и 68](traceability-is-a-join-over-files-that-already-exist.md) - [Отказ «инстанцировано на 2 вызовах» держит не `пусть`-имя, а тело вызванной: с телом-`разбор` он остаётся, с телом, которое ядро сводит, — исчезает](two-calls-refusal-is-about-the-callee-body-not-the-let-name.md) +- [Два приёма сверщика девять дней стояли без теоремы состоятельности, потому что число приёмов «81» переписывалось в прозе от руки](two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md) - [Два правила завершаемости поодиночке дают 54 и 74, а вместе — 574: узкое место в их произведении](two-termination-rules-together-give-574.md) - [Невысказываемое утверждение дороже недоказуемого](unstatable-costs-more-than-unprovable.md) - [Ветвь `разбор` по варианту без полей берётся равенством варианту, а `не результат` на такой ветви — нет](variant-equality-opens-a-case-branch.md) @@ -116,7 +117,6 @@ - [Вывод, снятый на одной ветке, — не вывод о дереве](vyvod-na-vetke-ne-vyvod-o-dereve.md) - [Узкое место переехало четвёртый раз: теперь мешает индукция, которую негде объявить](what-blocks-the-kernel-now-is-induction-without-a-theorem.md) - [Ноль аксиом — проверяемое свойство, а не лозунг](zero-axioms.md) -- [Два приёма сверщика девять дней стояли без теоремы состоятельности, потому что число приёмов «81» переписывалось в прозе от руки](two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md) ## Теория категорий @@ -340,6 +340,7 @@ ## Найденные ошибки +- [Разбор случаев по условию подставлял условие текстом под связыватель — и проверяющая программа приняла ложное постусловие кодом 0](a-case-split-pasted-the-condition-as-text-under-a-binder-and-proved-a-false-formula.md) - [Перепись целей без двоичного печатает нули и выходит кодом 0 — поэтому отсутствие прибора это «не проверено»](a-census-without-the-binary-prints-zeros-and-exits-zero.md) - [Изменившийся вердикт при снятии правки — ещё не доказанная ложь: доказанным надо проверить, ложь ли это](a-changed-verdict-on-removal-is-not-a-proven-lie.md) - [Проверка, живущая внутри одной команды, — это класс дефектов, и он всплыл трижды](a-check-that-skips-a-check-is-a-class.md) diff --git a/docs/zettel/a-case-split-pasted-the-condition-as-text-under-a-binder-and-proved-a-false-formula.md b/docs/zettel/a-case-split-pasted-the-condition-as-text-under-a-binder-and-proved-a-false-formula.md new file mode 100644 index 000000000..d63d769f6 --- /dev/null +++ b/docs/zettel/a-case-split-pasted-the-condition-as-text-under-a-binder-and-proved-a-false-formula.md @@ -0,0 +1,34 @@ +# Разбор случаев по условию подставлял условие текстом под связыватель — и проверяющая программа приняла ложное постусловие кодом 0 + +Приёмы Р2 и Р3 проверяющей программы на C доказывают Ф из двух половин: Ф с +условием В, заменённым на «да», и Ф с В, заменённым на «нет». В они не ищут +спуском по дереву, а восстанавливают из первого расхождения текста Ф и первой +половины и подставляют текстом во все вхождения (`вставить_вместо`). О +связывателях над вхождением вопроса не было — а под связывателем у куска нет +одного значения. + +**Чем подтверждено.** Проба 5 октября 2026, ветка `a/checker-rules-are-sound-in-lean`: +постусловие + + (свёртка [1,0] начиная с 0 как а и э → (если (э больше 0) то э минус а иначе а минус э)) меньше 1 + +ложно: условие истинно на первом элементе и ложно на втором, свёртка даёт 1. С «да» +на месте условия свёртка даёт −1, с «нет» — тоже −1, обе половины истинны. +(Первая проба была на дизъюнкции двух свёрток — тот же исход кодом 0; в набор +пошла короткая форма.) Запись с блоком «Выч ⟨Ф[да]⟩, Выч ⟨Ф[нет]⟩, Р3 ⟨Ф⟩ из 1 2» и словом +«доказано» проверяющая программа приняла: код 0, «числятся доказанными 1». Та же +запись с испорченной второй половиной — код 1 на шаге 2, то есть приём шёл через +настоящий счёт половин и настоящий Р3. После отказа на связывателе в Ф та же +подделка — код 1 на шаге 3; подделка стоит в наборе как +`forgery-case-split-captures-a-bound-name`, класс `record-lies`. + +**Чем ограничено.** Корпус это не задело — формул Р2/Р3 в записях три, со +связывателем ни одной, — потому и расхождение вердиктов не могло поймать: +приёмка Lean эти два приёма не судит вовсе (задача 4791). Нашлось не прогоном, а +при оценке того, что лемме Р2/Р3 в модели нужна подстановка без захвата: там, +где у Lean обязано стоять условие, у сверщика его не было. Квантор «для всех» +внутри формулы ядро не берёт (ADR-0026), поэтому закрытый список связывателей — +шесть слов ядра — покрывает все вхождения. + +Связано: [[two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand]], +[[a-record-that-names-only-the-rule-proves-nothing-about-the-rule]] diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index 3814fddba..61d7f77eb 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -7133,6 +7133,14 @@ static char *семейство_р(ШагВывода *ш, ШагВывода * if (strcmp(преж[ш->из1 - 1].правило, "Выч") != 0 || strcmp(преж[ш->из2 - 1].правило, "Выч") != 0) return fmt("шаг %ld: %s — половины (шаги %ld и %ld) обязаны быть выведены правилом Выч", ш->номер, имя, ш->из1, ш->из2); + /* Условие подставляется ТЕКСТОМ во все вхождения, а под связывателем у куска + нет одного значения: «( э больше 0 )» в свёртке по [1,0] истинно на одном + элементе и ложно на другом, и обе половины замыкаются при ложной Ф (проба + 5 октября 2026, подделка forgery-case-split-captures-a-bound-name). Отказ + на любом связывателе в Ф — тот же закрытый список, что у Э3 и Т2. */ + if (есть_связыватель(ф)) + return fmt("шаг %ld: %s — в формуле «%s» стоит связыватель, и условие, подставленное текстом, под ним" + " захватилось бы: у куска под связывателем нет одного значения", ш->номер, имя, ф); for (i = 0; ф[i] && ф[i] == о1[i]; i++) ; if (!ф[i] || strncmp(о1 + i, "да", strlen("да")) != 0) return fmt("шаг %ld: %s — на месте первого расхождения «%s» с половиной «%s» стоит не «да»", diff --git a/flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang b/flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang new file mode 100644 index 000000000..d53a68d7b --- /dev/null +++ b/flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang @@ -0,0 +1,7 @@ +модуль «Проба захвата» + +тотальная функция «Тождество» + принимает х: число + возвращает число + обеспечивает «ложь» (свёртка [1,0] начиная с 0 как а и э → (если (э больше 0) то э минус а иначе а минус э)) меньше 1 + х diff --git a/flang/proof/checker/tests/records/corpus/forgery-case-split-captures-a-bound-name.record b/flang/proof/checker/tests/records/corpus/forgery-case-split-captures-a-bound-name.record new file mode 100644 index 000000000..c1cc42eb0 --- /dev/null +++ b/flang/proof/checker/tests/records/corpus/forgery-case-split-captures-a-bound-name.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang +строк 8 +знаков 218 +отпечаток 826134182 349359672 +ядро 2 +утверждений 1 +отпечаток256 0b2f23a3eb1485820191ccf7d8e4243057667fa87df6fe3ca07b87736a3cbba1 +тотальностей 1 +утверждение «ложь» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «разбор случаев по внутреннему условию цели» + по объявлению нет + вывод цель ⟨(свёртка [1,0] начиная с 0 как а и э → (если (э больше 0) то э минус а иначе а минус э)) меньше 1⟩ + вывод 1 Выч ⟨(свёртка [1,0] начиная с 0 как а и э → (если да то э минус а иначе а минус э)) меньше 1⟩ сам + вывод 2 Выч ⟨(свёртка [1,0] начиная с 0 как а и э → (если нет то э минус а иначе а минус э)) меньше 1⟩ сам + вывод 3 Р3 ⟨(свёртка [1,0] начиная с 0 как а и э → (если (э больше 0) то э минус а иначе а минус э)) меньше 1⟩ из 1 2 + вывод конец +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/forgeries/manifest.tsv b/flang/proof/forgeries/manifest.tsv index e16aa9aff..91798094b 100644 --- a/flang/proof/forgeries/manifest.tsv +++ b/flang/proof/forgeries/manifest.tsv @@ -37,3 +37,4 @@ flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang flang/proof/c flang/proof/checker/tests/programs/audit-2844/unfold3-difference.flang flang/proof/checker/tests/records/corpus/poddelka-razv3-raznost.record record-lies flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record record-lies flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record record-lies +flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang flang/proof/checker/tests/records/corpus/forgery-case-split-captures-a-bound-name.record record-lies diff --git a/flang/proof/lean/Acceptance.lean b/flang/proof/lean/Acceptance.lean index 6879ee51a..ba7e8889d 100644 --- a/flang/proof/lean/Acceptance.lean +++ b/flang/proof/lean/Acceptance.lean @@ -40,7 +40,11 @@ import «Запись» сверщике или строка переживёт свой приём: - Выч, Р2, Р3 — вычислитель половин (`половина_закрыта`): модель его не - воспроизводит, а Р2 и Р3 берут посылками только шаги Выч. Это второй + воспроизводит, а Р2 и Р3 берут посылками только шаги Выч. С 5 октября 2026 + сверщик отказывает Р2/Р3 на связывателе в формуле (подделка + `forgery-case-split-captures-a-bound-name` проходила кодом 0), и приёмке + хватит того же отказа: замена куска на литерал без связывателей — подстановка + без захвата по построению (задача 4791). Это второй вычислитель языка внутри сверщика: от `половина_закрыта` достижимы 78 функций и 1228 строк кода из 7401 (из них `оценить_терм` — 261; счёт по графу вызовов, 15 сентября 2026, main `8c1fee225` с починкой Т2/Э2). Взять Выч значит завести diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index 7c084e78b..e2acc3534 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,4 +1,4 @@ -forgeries 38 +forgeries 39 forgery-numerator 155 forgery-probes 628 checker-code-lines 8127 diff --git a/flang/proof/tables/consistency-violations.tsv b/flang/proof/tables/consistency-violations.tsv index 9bfa4dca4..31257c8b7 100644 --- a/flang/proof/tables/consistency-violations.tsv +++ b/flang/proof/tables/consistency-violations.tsv @@ -5,3 +5,4 @@ verified-in-vain open theorem-hypothesis-not-discharged closed loop-through-function-value closed restricted-postcondition-cited-undischarged closed +case-split-substitutes-under-a-binder closed diff --git a/scripts/ledgers/file-name-words.txt b/scripts/ledgers/file-name-words.txt index 83c3cb8a2..be4944aca 100644 --- a/scripts/ledgers/file-name-words.txt +++ b/scripts/ledgers/file-name-words.txt @@ -1185,6 +1185,7 @@ pass passed passes past +pasted patched path paths From 285d005a846323aa25dc3da82854ff2c6d953576 Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Tue, 6 Oct 2026 07:25:04 +0000 Subject: [PATCH 6/8] fix(proof): the lean rules guard is probed in ci, its marks go 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). --- .github/workflows/ci.yml | 11 ++++++++++- ...ker-move-has-a-lean-theorem-or-a-named-debt-row.md | 8 ++++---- docs/lean-checks-the-inference-rules.md | 2 +- docs/road-to-1-0.md | 4 ++-- ...es-read-the-body-by-lines-and-stay-outside-lean.md | 2 -- ...t-a-theorem-while-the-count-was-written-by-hand.md | 3 +-- scripts/ledgers/proved-share-ledger.txt | 1 + 7 files changed, 19 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3d384de17..80ddecbaf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1182,8 +1182,17 @@ jobs: steps: - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 - run: make -C bootstrap -j"$(nproc)" + # Зовётся ФАЙЛОМ и в условии: прибор проб порчи + # (scripts/guards/guards-without-forgery-probe.fscript) признаёт пробу + # только по вызову в `if` с `exit 1` в том же теле и относит её к сторожу + # по файлу. План «Forgery» кончается кодом 0, когда все три порчи + # покраснели, и кодом 1, когда хоть одна прошла, — отсюда `if !`. - name: Forgery goes red - run: bootstrap/flang run-script lean-rules:forgery + run: | + if ! bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Forgery; then + echo "сторож приёмов промолчал на подлоге — проверять им нечего" >&2 + exit 1 + fi - name: Every checker move has a theorem or a debt row run: bootstrap/flang run-script lean-rules:check diff --git a/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md index 59039c086..ff7093aa2 100644 --- a/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md +++ b/docs/adr/0064-every-checker-move-has-a-lean-theorem-or-a-named-debt-row.md @@ -34,7 +34,6 @@ как известный долг, а не как новая дыра. Девять дней у двух приёмов сверщика не было теоремы, и ни одна проверка не краснела. - Замер прибором 5 октября, до правки приёмки: приёмов 83, в приёмке 76, вне приёмки 7 (Р2, Р3, Р5, Р6, Выч и те самые Н6, О9). @@ -71,7 +70,6 @@ ## 3. Замер после правки - `bootstrap/flang run-script lean-rules:numbers`: приёмов 83, с леммой 83, в приёмке Lean 78, вне приёмки 5, в долге 5. `lean-rules:check` зелен; `lean-rules:forgery` — три подлога, пойманы три. `Consistency.lean`: @@ -79,7 +77,7 @@ «состоятельность» — три стандартные. Сборка цепочки Lean на машине разработки: `Term.lean` 51 с, `Acceptance.lean` 16 с, `Consistency.lean` 20 с. Полная сверка `flang/proof/lean/run.fscript` (632 с, Lean 4.34.0 по -`lean-toolchain`): +`lean-toolchain`): ловушек 57, Lean отверг 57; строк перечня 112, с леммой 112; пар 273, блоков 1513, расхождений 0; вне приёмки — Выч 60, Р5 24, Р6 7 (на 2 октября там же стояли О9 7 и Н6 5). @@ -104,7 +102,9 @@ ## 4. Последствия - Число «приёмов N, покрыто M» в прозе больше не пишется от руки: его печатает - `lean-rules:numbers`, и в документах оно стоит с приметой `СНЯТО`. + `lean-rules:numbers`, и рядом с числом в документах названы дата и команда. + Приметой `СНЯТО` его не пометить: сторож чисел в прозе знает пять приборов + (строк, файлов, строк-в, примеров-в, список), и перепись приёмов не из них. - Новый приём сверщика без теоремы ломает `ci.yml` на том же пуше. Обойти можно только строкой долга — с номером задачи, то есть вслух. - Приёмка Lean теперь строже сверщика ещё в одном месте (О9: список — имя, шаг — diff --git a/docs/lean-checks-the-inference-rules.md b/docs/lean-checks-the-inference-rules.md index 7ad8acff5..9e5caaf3b 100644 --- a/docs/lean-checks-the-inference-rules.md +++ b/docs/lean-checks-the-inference-rules.md @@ -22,7 +22,7 @@ > **Сверка 5 октября 2026** (ADR-0064, `bootstrap/flang run-script lean-rules:numbers`): > приёмов `шаг_вывода` у сверщика **83**, с леммой в `Rules.lean`/`Term.lean` — 83, в > приёмке Lean — **78**, вне приёмки — 5, и все пять стоят строками долга в -> `flang/proof/tables/lean-acceptance-debt.tsv`. +> `flang/proof/tables/lean-acceptance-debt.tsv`. > Число снимает прибор `flang/proof/lean/rules-guard.fscript`, а не рука. Проверялись ПРАВИЛА, а не записи доказательств. Правил конечное число, и diff --git a/docs/road-to-1-0.md b/docs/road-to-1-0.md index 80556776b..afa1c1b11 100644 --- a/docs/road-to-1-0.md +++ b/docs/road-to-1-0.md @@ -118,7 +118,7 @@ Homebrew с тем, что собрал сам конвейер выпуска; **15 сент, позже** (задача 1130; `sh flang/proof/lean/run.sh`, ветка `a/lean-o6-ch5-representable-and-number-text`): **теорема о состоятельности есть для 76 правил из 81** — прибавились О6 (окружение знает факт языка «числа-представимы») и Ч5 (модель терма переводит число в текст). Сверка вердиктов (508 подделок, 237 честных; 242 пары, 1503 блока): расхождений 0; вне приёмки 91 блок — Выч, Р5, Р6 и запреты; ловушек 37 из 37. К↑ и Разв3 Lean теперь судит в самом прогоне — проба `развёртка/box-round-trip-by-assumption` с базой Т1. -**5 окт** (задача 1435 → ADR-0064; `bootstrap/flang run-script lean-rules:numbers`, ветка `a/checker-rules-are-sound-in-lean`): приёмов `шаг_вывода` у сверщика **83**, а не 81 — Н6 и О9 вошли в сверщик 26 сентября (задача 1435) и девять дней не имели теоремы, пока число 81 переписывалось в прозе от руки. **Теорема о состоятельности есть для 78 приёмов из 83**: Н6 и О9 вошли в приёмку (`Acceptance.lean`, `Consistency.lean`; О9 — под фактом окружения «списки-коротки» в `Record.lean`), ловушек стало 55 файлов-искажений (две новые: 85 — О9 с шагом в двойку, 86 — Н6 без второй посылки). Пять приёмов без теоремы — Выч, Р2, Р3, Р5, Р6 — стоят строками долга в `flang/proof/tables/lean-acceptance-debt.tsv` с номером задачи (1183, 4791); сторож `flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, работа `lean-rules-guard` в `ci.yml` и шаг в `lean-crosscheck.yml`) краснеет на приёме без приёмки и без строки долга, на уплаченном долге и на имени, которого нет у сверщика; три подлога на копиях (`lean-rules:forgery`) пойманы все три. Сверка вердиктов (`bootstrap/flang io flang/proof/lean/run.fscript`, 632 с, Lean 4.34.0): 273 пары, 1513 блоков, расхождений 0, ловушек 57 из 57; вне приёмки остались Выч 60, Р5 24, Р6 7 — О9 (7 блоков) и Н6 (5 блоков) из списка ушли в «оба приняли». +**5 окт** (задача 1435 → ADR-0064; `bootstrap/flang run-script lean-rules:numbers`, ветка `a/checker-rules-are-sound-in-lean`): приёмов `шаг_вывода` у сверщика **83**, а не 81 — Н6 и О9 вошли в сверщик 26 сентября (задача 1435) и девять дней не имели теоремы, пока число 81 переписывалось в прозе от руки. **Теорема о состоятельности есть для 78 приёмов из 83**: Н6 и О9 вошли в приёмку (`Acceptance.lean`, `Consistency.lean`; О9 — под фактом окружения «списки-коротки» в `Record.lean`), ловушек стало 55 файлов-искажений (две новые: 85 — О9 с шагом в двойку, 86 — Н6 без второй посылки). Пять приёмов без теоремы — Выч, Р2, Р3, Р5, Р6 — стоят строками долга в `flang/proof/tables/lean-acceptance-debt.tsv` с номером задачи (1183, 4791); сторож `flang/proof/lean/rules-guard.fscript` (ярлык `lean-rules:check`, работа `lean-rules-guard` в `ci.yml` и шаг в `lean-crosscheck.yml`) краснеет на приёме без приёмки и без строки долга, на уплаченном долге и на имени, которого нет у сверщика; три подлога на копиях (`lean-rules:forgery`) пойманы все три. Сверка вердиктов (`bootstrap/flang io flang/proof/lean/run.fscript`, 632 с, Lean 4.34.0): 273 пары, 1513 блоков, расхождений 0, ловушек 57 из 57; вне приёмки остались Выч 60, Р5 24, Р6 7 — О9 (7 блоков) и Н6 (5 блоков) из списка ушли в «оба приняли». **Чего нет.** Теоремы для пяти приёмов из 83 — Выч, Р2, Р3, Р5, Р6 (строки долга, задачи 1183 и 4791) — и для Разв1 по строке тела (причины — в шапке `Acceptance.lean`, задачи 1130, 4058, 6432). Теоремы о самом `checker.c`: код с моделью связан сверкой вердиктов на наборе, а не выводом. Модель значений округляет «грубо», не по binary64, и её совпадение с вычислителем не доказано (ADR-0041 §2.3). Чтение текста записи (`flang/proof/lean/RecordReader.lean`) стоит вне теоремы. @@ -270,7 +270,7 @@ Homebrew с тем, что собрал сам конвейер выпуска; | **квантор внутри формулы и существование без свидетеля** | кванторы — обычные термы, вкладываются свободно | оба квантора связывают только цель целиком; существование требует названного свидетеля | задачи 1177, 1188 | разбор + ядро; **перепечатка семени** | | **законы кольца** | `ring` | доказывается только перестановка операндов одного узла | задача 1412 | правила на точном целом (задача 1908); **перепечатка семени** | | **суд над категорной поверхностью** | классы типов с законами, проверяемыми как теоремы | моноиды, монады, функторы и блоки `закон` не судятся, код 2 | задачи 6752, 9963 | ядро + поверхность; **перепечатка семени** | -| **состоятельность последних правил** | ядро Lean мало и проверено само | теорема есть для 78 приёмов сверщика из 83 ; пять без теоремы названы строками долга, сторож `lean-rules:check` не даёт появиться шестому молча — пункт 3 выше | задачи 1183, 4791; ADR-0064 | только `flang/proof/lean/**` — **перепечатки НЕ требует** | +| **состоятельность последних правил** | ядро Lean мало и проверено само | теорема есть для 78 приёмов сверщика из 83; пять без теоремы названы строками долга, сторож `lean-rules:check` не даёт появиться шестому молча — пункт 3 выше | задачи 1183, 4791; ADR-0064 | только `flang/proof/lean/**` — **перепечатки НЕ требует** | | **вторая реализация сличителя** | `lean4lean`, `lean4export` — чужие перепроверяющие | сличитель один, и его пробы написал его же автор | задача 1313 | только `flang/proof/checker/**` — **перепечатки НЕ требует** | Почему «перепечатка семени» — это цена, а не сноска: правка под `flang/self/**` diff --git a/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md index 5e4a7a0b3..0bc0e5306 100644 --- a/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md +++ b/docs/tasks/4791-the-empty-list-moves-read-the-body-by-lines-and-stay-outside-lean.md @@ -31,8 +31,6 @@ $ bootstrap/flang run-script lean-rules:numbers приёмов 83, с леммой 83, в приёмке 78, вне приёмки 5, в долге 5 код 0 ``` - - Версия: flang 0.7.24, Lean 4.34.1. Дата прогона: 5 октября 2026, ветка `a/checker-rules-are-sound-in-lean`. diff --git a/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md index 14bd05fa9..0f858f8a1 100644 --- a/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md +++ b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md @@ -12,10 +12,9 @@ **Чем подтверждено.** Прибор `flang/proof/lean/rules-guard.fscript`, ветка `a/checker-rules-are-sound-in-lean` от `6b459ded0`, 5 октября 2026: - - до правки: приёмов 83 (не 81), в приёмке 76, вне приёмки 7 — Р2, Р3, Р5, Р6, Выч и незамеченные Н6, О9; в долге с номером задачи 5; - + - после правки приёмки: в приёмке 78, вне приёмки 5, в долге 5, сторож `lean-rules:check` зелен, `«покрыто» = 78` в `Consistency.lean` проверено `decide`; diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index 3246822c5..122836e98 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1671,6 +1671,7 @@ aa65f3785b0c62edf336a36297e30b38|1|1|0|0|0|flang/proof/probes/unproven/programs/ 8c27388a17ff86d5bb9e415d3dd3d5dd|1|1|0|1|1|flang/proof/checker/tests/programs/audit-2844/unfold3-difference.flang 86e0e447b270b761bff6ae33fe3ffd12|1|1|0|1|0|flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang eb5b390d34c90eb95ad3b4382c2a3a1f|1|0|0|0|1|flang/proof/checker/tests/programs/audit-2844/unfold3-control-honest.flang +6d472ad507bec881b4b1a91cce883f79|1|0|0|1|0|flang/proof/checker/tests/programs/audit-4791/case-split-under-a-binder.flang b1b137536d045c4fdd205ece597d4acf|1|0|1|0|0|flang/proof/probes/orders/programs/arguments.fscript a9553eaffc7cba5c190df9e076ef0b9c|2|2|0|0|0|flang/proof/probes/io-timeout/run.fscript 5750e56d208d017c3ef036fe93fce6f7|3|3|0|0|0|flang/proof/probes/non-negative-field/run.fscript From 976e2386ccf526e7d5a6f00b87aed3581a8c0618 Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Tue, 6 Oct 2026 07:56:03 +0000 Subject: [PATCH 7/8] chore(marks): the numbers follow the lean rules line 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. --- .github/workflows/ci.yml | 4 ++-- ...-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md | 2 +- docs/course/00-overview.md | 2 +- docs/course/13-where-next.md | 2 +- docs/course/README.md | 2 +- docs/design/nositel-tochnogo-celogo.md | 2 +- docs/four-coverages.md | 4 ++-- docs/road-to-1-0.md | 4 ++-- ...5771-integrality-does-not-tighten-a-strict-order-by-one.md | 2 +- ...ement-over-a-finite-sum-has-no-way-to-exhaust-its-cases.md | 2 +- ...ion-in-a-free-statement-refuses-the-nonnegative-segment.md | 2 +- docs/tree-inventory.md | 2 +- flang/scripts/count-guard.mjs | 4 ++-- flang/scripts/name-guard.mjs | 4 ++-- 14 files changed, 19 insertions(+), 19 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 80ddecbaf..b4d63559a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -164,8 +164,8 @@ permissions: jobs: # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c` - # планом на flang — 1152 файлов; разбор в задаче 5821. - # СНЯТО 2026-10-05 файлов *.flang = 1152 (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него + # планом на flang — 1153 файлов; разбор в задаче 5821. + # СНЯТО 2026-10-06 файлов *.flang = 1153 (задача 4791: программа-проба захвата под связывателем; до них 1152, снято 2026-10-05) (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него # 1127, снято 2026-10-04) (задача 1116: три программы пробы # поверхностей вердикта о прогонах и задача 1113: семь программ пробы # порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары diff --git a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md b/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md index cb14f0ebf..72fa66a0b 100644 --- a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md +++ b/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md @@ -192,7 +192,7 @@ flang check --proof --строго monoid.flang «Е не больше Е» не теорема, почему `0 × ∞` даёт не число, почему переставлять через скобки нельзя. Эти доводы не украшение: на них стоят посылки правил. - **Независимая проверяющая программа** — `flang/proof/checker/checker.c`, - 10497 строк. + 10505 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/course/00-overview.md b/docs/course/00-overview.md index cc76557cf..bd140c0b3 100644 --- a/docs/course/00-overview.md +++ b/docs/course/00-overview.md @@ -179,7 +179,7 @@ JavaScript, Python, Rust и TypeScript. Не «транспилирует при - [Операции языка](https://digitable-lol.github.io/flang/operations.html) — что чем делается; - [База знаний проекта](https://github.com/digitable-lol/flang/tree/main/docs/zettel) - — 729 заметка о том, **почему** решили так: что померили, что оказалось ложным, + — 731 заметка о том, **почему** решили так: что померили, что оказалось ложным, какой путь отвергли и по какому доводу. Курс на неё опирается и ссылается поимённо. diff --git a/docs/course/13-where-next.md b/docs/course/13-where-next.md index 05d5d3243..657955305 100644 --- a/docs/course/13-where-next.md +++ b/docs/course/13-where-next.md @@ -47,7 +47,7 @@ bootstrap/flang run-script numbers:build ## База знаний проекта — самое недооценённое, что там есть -`docs/zettel/` — **729 заметка**. Это не документация и не журнал изменений. Там +`docs/zettel/` — **731 заметка**. Это не документация и не журнал изменений. Там записано **почему решили так**: что померили, что оказалось ложным, какой путь отвергли и по какому доводу. diff --git a/docs/course/README.md b/docs/course/README.md index f3c216b50..95ed05ebc 100644 --- a/docs/course/README.md +++ b/docs/course/README.md @@ -172,7 +172,7 @@ docs/course/check.flang: проверено — разбор, типы, заве | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `cc`/`g++` 15.2.0, go 1.26.5, rustc 1.97.1, javac 26-internal, Elixir 1.20.3 на Erlang/OTP 29, node 26.7.0, Python 3.14.4, .NET 10.0.110 | | 82 задачи LeetCode, десятка самых коротких | `ls`, `wc -l`, счёт строк `пример` | | 53 файлов и 33 153 строк библиотеки | `ls flang/stdlib/*.flang`, `cat … \| wc -l` | -| 729 заметок, 242 примеров, 475 файлов доказательств | `ls`, `find` | +| 731 заметок, 242 примеров, 476 файлов доказательств | `ls`, `find` | | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа | **Чего переснять не удалось, и это надо знать.** diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index 97f129616..64dcd34c1 100644 --- a/docs/design/nositel-tochnogo-celogo.md +++ b/docs/design/nositel-tochnogo-celogo.md @@ -441,7 +441,7 @@ flang check n-zapis-v-chislo.flang первая правка, и назвать её сейчас, не написав, значило бы выдумать. 2. **Цену принуждения канона.** Сколько стоит запретить литерал-список в позиции нового типа — не мерил: это решение задачи 1412, а не замер. -3. **Цену для проверяющей программы.** `checker.c` (10497 строк) +3. **Цену для проверяющей программы.** `checker.c` (10505 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/docs/four-coverages.md b/docs/four-coverages.md index b136b1428..e5e6c58d6 100644 --- a/docs/four-coverages.md +++ b/docs/four-coverages.md @@ -25,8 +25,8 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000 **Что меряет.** Долю мест в СОБСТВЕННЫХ записях доказательства компилятора, которые независимый проверяющий на C ([`flang/proof/checker/checker.c`](../flang/proof/checker/checker.c)) переиграл сам, а не принял на слово у ядра. Записи лежат готовыми в -`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 93. - +`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 94. + Снимается: `bootstrap/flang io flang/proof/replay-share.fscript`. **Что это даёт сказать.** Что у этого набора записей слово «доказано» в отчёте компилятора не diff --git a/docs/road-to-1-0.md b/docs/road-to-1-0.md index afa1c1b11..3d445044c 100644 --- a/docs/road-to-1-0.md +++ b/docs/road-to-1-0.md @@ -205,10 +205,10 @@ Homebrew с тем, что собрал сам конвейер выпуска; с шапкой: 97 правил и 15 запретов, 19 семей (`awk -F'\t' 'NR>1{print $3}' | sort | uniq -c`, 4 октября 2026). Независимая проверяющая программа на C — `flang/proof/checker/checker.c`, - 10 497 строк. + 10 505 строк. Состоятельность правил сверена моделью Lean: 9 файлов, - 12 676 строк, + 12 895 строк, `sorry` — ноль (`grep -c sorry`, 4 октября 2026); сколько правил покрыто теоремой и чего в приёмке нет — выше, в пункте 3. diff --git a/docs/tasks/5771-integrality-does-not-tighten-a-strict-order-by-one.md b/docs/tasks/5771-integrality-does-not-tighten-a-strict-order-by-one.md index aa6b2ca20..a493ad65f 100644 --- a/docs/tasks/5771-integrality-does-not-tighten-a-strict-order-by-one.md +++ b/docs/tasks/5771-integrality-does-not-tighten-a-strict-order-by-one.md @@ -96,7 +96,7 @@ | --- | --- | --- | | правило ужатия | `flang/self/proof-kernel.flang`, рядом с анкерами `С4 proof-kernel.flang:3041` «Строгое дно по порядкам» и `Цел1 proof-kernel.flang:3365` «Это целость терма» | новое правило, не случай прежнего | | снятие предусловия как допущения | `flang/self/proof-kernel.flang`, анкер `Т1 proof-kernel.flang:4540` «Есть допущением» | допущение уже доходит: отказ пишет «известно: предусловие функции» | -| печать и чтение хода | `flang/self/proof-record.flang`, `flang/proof/checker/checker.c` ( 10 497 строк), `flang/proof/checker.flang` | список ходов закрытый | +| печать и чтение хода | `flang/self/proof-record.flang`, `flang/proof/checker/checker.c` ( 10 505 строк), `flang/proof/checker.flang` | список ходов закрытый | | перечень и лемма | `flang/proof/tables/inference-rules.tsv` ( 115 строк с шапкой), `flang/proof/lean/Rules.lean` | строка и теорема | Потолок строк независимой проверяющей программы — ключ `checker-code-lines` в diff --git a/docs/tasks/7328-a-free-statement-over-a-finite-sum-has-no-way-to-exhaust-its-cases.md b/docs/tasks/7328-a-free-statement-over-a-finite-sum-has-no-way-to-exhaust-its-cases.md index 5b19cf951..94f3d6d6a 100644 --- a/docs/tasks/7328-a-free-statement-over-a-finite-sum-has-no-way-to-exhaust-its-cases.md +++ b/docs/tasks/7328-a-free-statement-over-a-finite-sum-has-no-way-to-exhaust-its-cases.md @@ -89,7 +89,7 @@ | закрытие базы свободного утверждения ядром | `flang/self/proof-kernel.flang` (анкеры `Инд1`, `Р1`) | новый случай, не новое правило | | смысл `по примеру` у свободного утверждения | `flang/self/proof-kernel.flang`, `flang/self/proof.flang` | решение: брать пример у ВЫЗЫВАЕМОЙ функции или отказывать дальше | | печать хода в запись | `flang/self/proof-record.flang` | ход уже есть у постусловия | -| чтение хода | `flang/proof/checker/checker.c` ( 10 497 строк), `flang/proof/checker.flang` | список ходов закрытый | +| чтение хода | `flang/proof/checker/checker.c` ( 10 505 строк), `flang/proof/checker.flang` | список ходов закрытый | | строка перечня и лемма | `flang/proof/tables/inference-rules.tsv`, `flang/proof/lean/Rules.lean` | если правило новое, а не случай прежнего | Потолок строк независимой проверяющей программы — ключ `checker-code-lines` в diff --git a/docs/tasks/7367-induction-in-a-free-statement-refuses-the-nonnegative-segment.md b/docs/tasks/7367-induction-in-a-free-statement-refuses-the-nonnegative-segment.md index 7fcd9046c..a30a4d434 100644 --- a/docs/tasks/7367-induction-in-a-free-statement-refuses-the-nonnegative-segment.md +++ b/docs/tasks/7367-induction-in-a-free-statement-refuses-the-nonnegative-segment.md @@ -113,7 +113,7 @@ FLANG_PROOF_INDUCTION_TYPE … строка 10, столбец 3: утвержд | --- | --- | --- | | выбор носителя принципа | `flang/self/proof-kernel.flang`, анкер `Инд1 proof-kernel.flang:1012` «Имя конструктора образца» | носителей сегодня два, перебор закрытый | | отказ, который снимается | `flang/self/proof-kernel.flang` либо `flang/self/proof.flang`: место, печатающее `FLANG_PROOF_INDUCTION_TYPE` | один код беды | -| печать и чтение хода | `flang/self/proof-record.flang`, `flang/proof/checker/checker.c` ( 10 497 строк), `flang/proof/checker.flang` | список ходов закрытый | +| печать и чтение хода | `flang/self/proof-record.flang`, `flang/proof/checker/checker.c` ( 10 505 строк), `flang/proof/checker.flang` | список ходов закрытый | | перечень и лемма | `flang/proof/tables/inference-rules.tsv` ( 115 строк с шапкой), `flang/proof/lean/Rules.lean` | семья `Инд` — четыре строки перечня (`awk -F'\t' '$2=="Инд"'`, 4 октября 2026) | Ядро решений — `flang/self/proof-kernel.flang`, diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 9b7a8ad00..b5fc9cb71 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -83,7 +83,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| | оболочка | 53 | 9 247 | 48 | 5 017 | -| C | 40 | 893 517 | 1 | 107 | +| C | 40 | 893 525 | 1 | 107 | | C++ | 2 | 511 | 1 | 107 | | Python | 5 | 2 997 | 0 | 0 | | HTML | 7 | 1 263 | 0 | 0 | diff --git a/flang/scripts/count-guard.mjs b/flang/scripts/count-guard.mjs index 4f605abb0..64124c916 100644 --- a/flang/scripts/count-guard.mjs +++ b/flang/scripts/count-guard.mjs @@ -43,8 +43,8 @@ * * • ЧИСЛО ФАЙЛОВ он не сверяет. «AST всех 60 файлов `.flang` репозитория * напечатан до и после правки» — не утверждение о размере дерева, а запись о - * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1152 файлов, но - * СНЯТО 2026-10-05 файлов *.flang = 1152 (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него 1127, снято 2026-10-04) (задача 1116: три программы пробы поверхностей вердикта о прогонах и задача 1113: семь программ пробы порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 1115, снято 2026-10-03) (задача 1908: четыре программы набора проб точного целого; до них 1111) (задача 1116: три программы пробы неисполненных блоков «прогон»; до них 1098, снято 2026-10-02) + * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1153 файлов, но + * СНЯТО 2026-10-06 файлов *.flang = 1153 (задача 4791: программа-проба захвата под связывателем; до них 1152, снято 2026-10-05) (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него 1127, снято 2026-10-04) (задача 1116: три программы пробы поверхностей вердикта о прогонах и задача 1113: семь программ пробы порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 1115, снято 2026-10-03) (задача 1908: четыре программы набора проб точного целого; до них 1111) (задача 1116: три программы пробы неисполненных блоков «прогон»; до них 1098, снято 2026-10-02) * прогон-то был на шестидесяти, и подставить туда 168 значило бы соврать про * работу, которой не делали. Отличить «столько в дереве» от «столько прошло * через прогон» нечем, кроме чтения, — значит сторож сюда не лезет. diff --git a/flang/scripts/name-guard.mjs b/flang/scripts/name-guard.mjs index bb3904596..0785abb22 100644 --- a/flang/scripts/name-guard.mjs +++ b/flang/scripts/name-guard.mjs @@ -130,8 +130,8 @@ * переставшая сравнивать, продолжает зеленеть. * * Поэтому охват ПЕЧАТАЕТСЯ каждым прогоном и закреплён тестом «охват сторожа - * назван числом»: 300 файлов из 1152. Остальные — не упущение: - * СНЯТО 2026-10-05 файлов *.flang = 1152 (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него 1127, снято 2026-10-04) (задача 1116: три программы пробы поверхностей вердикта о прогонах и задача 1113: семь программ пробы порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 1115, снято 2026-10-03) (задача 1908: четыре программы набора проб точного целого; до них 1111) (задача 1116: три программы пробы неисполненных блоков «прогон»; до них 1098, снято 2026-10-02) + * назван числом»: 300 файлов из 1153. Остальные — не упущение: + * СНЯТО 2026-10-06 файлов *.flang = 1153 (задача 4791: программа-проба захвата под связывателем; до них 1152, снято 2026-10-05) (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него 1127, снято 2026-10-04) (задача 1116: три программы пробы поверхностей вердикта о прогонах и задача 1113: семь программ пробы порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 1115, снято 2026-10-03) (задача 1908: четыре программы набора проб точного целого; до них 1111) (задача 1116: три программы пробы неисполненных блоков «прогон»; до них 1098, снято 2026-10-02) * * • 503 — печать замеров (`docs/benchmark*`): * это ВЫВОД прогона, а не исходник, и правилам имени он не подчиняется; From 345bbe2cc165948fdc2c0da790969de3cde1b3e5 Mon Sep 17 00:00:00 2001 From: the-homeless-god Date: Tue, 6 Oct 2026 08:20:49 +0000 Subject: [PATCH 8/8] fix(proof): the new forgery is named and the zettel link resolves 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. --- ...ut-a-theorem-while-the-count-was-written-by-hand.md | 2 +- flang/proof/records-nesting.fscript | 10 +++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md index 0f858f8a1..9fba4827c 100644 --- a/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md +++ b/docs/zettel/two-checker-moves-without-a-theorem-while-the-count-was-written-by-hand.md @@ -35,4 +35,4 @@ сломан» и подлог с дописанным приёмом. Связано: [[a-hand-copied-wall-list-goes-stale-in-silence]], -[[checks-that-do-not-check]], [[zero-axioms]] +[[checks-that-stopped-comparing]], [[zero-axioms]] diff --git a/flang/proof/records-nesting.fscript b/flang/proof/records-nesting.fscript index 81bcaa095..d76984819 100644 --- a/flang/proof/records-nesting.fscript +++ b/flang/proof/records-nesting.fscript @@ -18,9 +18,13 @@ тотальная функция «Allowed to differ» возвращает список строки - пример «Six records that lie on purpose and so differ from the print» - ожидается ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost"] - ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost"] + пример «Seven records that lie on purpose and so differ from the print» + ожидается ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", + "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost", + "forgery-case-split-captures-a-bound-name"] + ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", + "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost", + "forgery-case-split-captures-a-bound-name"] тотальная функция «Allowed to be refused» возвращает список строки