Repository navigation
feat(guards): сторож «проверки, которых никто не зовёт» видит судей в замыкании - #329
Merged
Merged
Conversation
the-homeless-god
force-pushed
the
a/the-law-judges-are-called-at-last
branch
from
October 7, 2026 21:04
1c577fa to
ade4890
Compare
Tasks 2277, 3311, 4433 and 6752 are one family: the law judges are written and nobody calls them. Header fields filled before the work so that a neighbour sees the claim: status, assignee, branch.
Second half of the census: the top points of judges in flang/self. A declared function named "Proverit ..." whose name is spelled out exactly once in the whole tree is declared and called by nobody, and a rule nobody runs is indistinguishable from an unwritten one. Measured 4 October 2026, tree 4d76abd, binary built in this tree: 201 top points, 190 called, 11 without a call -- the four law judges of task 2277 (monoid 683, functor 525, monad 484, iso 323) and seven the task did not know about (sets 790 and 526, commutative 150, monotone 269, distributive 234, check-sources 385, check-with-source-compiler 11). Guard run 8.4 s -> 15.2 s; obligations in the file 14 -> 31, all 107 functions with proved termination, all 31 obligations proved by the kernel, so the shortcut still runs without --na-veru. Counting happens in the shell, not in the plan: counting occurrences over the whole tree inside "flang io" would not fit the step limit. Two spellings are counted, because entry points are called both ways: a name in guillemets in .flang and .fscript, and the same name as a C string in the runtime (repl_call, 48 such names in flang/src/emit/c/flang_repl.c). Negative controls, all run: the category judge (2 occurrences) is NOT named; with its call at compiler.flang:1256 spoiled in a copy the guard does name it; a ledger record without a point and a record about a called judge both go red, and a point written into the ledger goes silent; plan "Podlog sudi" plants an uncalled judge under flang/self, demands code 1 and its name, and removes the file after itself; blinded on purpose the guard refuses on its own promise (code 3) and the forgery probe reports an idle probe. The guard nearly hid the judges with its own examples, which name them: its own file is now excluded from the call half, for the same reason the path half excludes its own file. The debt ledger is deliberately empty: not one of the 11 points has an honest "written ahead of time" reason. The sibling points of the same files have two occurrences each, but the second one is a self-call inside the same file, and the modules are imported by nobody. Does not touch the closure. No seed reprint needed.
The five note lines added to checks-nobody-calls.fscript leave, the new plan is named Judge forgery, and the debt ledger of uncalled judges loses its comment header: the plan already skips the column header row. Task 4433 is done by this branch and leaves the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Task 4433 left the tree with this branch, so the neighbour lists of tasks 1177, 1188, 2277 and 3311 no longer name it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
the-homeless-god
force-pushed
the
a/the-law-judges-are-called-at-last
branch
from
October 7, 2026 23:13
ade4890 to
4022a7a
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Закрывает задачу 4433. Семья четырёх задач P1 (2277, 3311, 4433, 6752) про одно:
судьи законов написаны и их никто не зовёт. Здесь — сторож, который это видит.
Что теперь правда
Опись сторожа
scripts/guards/checks-nobody-calls.fscriptстала двойной. Втораяполовина (
@@JUDGES) берёт ВЕРХНИЕ ТОЧКИ судей — объявленные функции«Проверить …»вflang/self/**— и считает, сколько раз имя названо во всёмдереве. Названо один раз значит «это само объявление и больше ничего»: правило,
которое никто не запускает, от ненаписанного неотличимо.
Прогон 4 октября 2026, дерево
4d76abd53, двоичный собран в этом дереве:uncalled-checks:check, времяВсе 107 функций с доказанным завершением, все 31 обязательство доказаны ядром —
ярлык по-прежнему гоняется без
--на-веру.Одиннадцать точек без зова: четыре судьи законов из задачи 2277 (моноид 683,
функтор 525, монада 484, изоморфизм 323) и ещё семь, которых задача не знала:
sets.flang:790и:526,commutative.flang:150,monotone.flang:269,distributive.flang:234,compiler.flang:385(«Проверить исходники»—рантайм на C повторяет тот же порядок сам,
flang_repl.c:45,:4707,:8392),check-with-source-compiler.flang:11.Считает оболочка, а не план: счёт вхождений по всему дереву внутри
flang ioвпредел шагов не укладывается — задача об этом и предупреждала. Считаются ДВА
вида записи имени, потому что точки входа зовут и так и так:
«Имя»в.flang/.fscriptи"Имя"строкой в рантайме на C (repl_call, таких имён48).
Отрицательные контроли, все прогнаны
незваного.
compiler.flang:1256испорчен в копии — сторож назвал«Проверить законы категории»; строка возвращена, сторож снова молчит.дереве больше нет»; запись о ЗВАНОМ судье — «а его зовут»; точка, вписанная в
ведомость, из красного уходит.
flang/self/uncalled-judge-forgery.flangс одной функцией
«Проверить подложного судью», спрашивает этого же сторожапланом «Проверка», ждёт код 1 и имя подлога — получает оба, файл убирает за
собой (
trapна выходе; после прогонаgit statusчист).flang/nikogo/**— прогон отказался кодом 3 на СВОЁМ ЖЕ обещании «в описьидут верхние точки из flang/self». Образец имени подменён на
«Проверитьь …»— проба подлога ответила «ПРОБА ХОЛОСТА: подлог не назван».Оба раза правка возвращена.
Что стоит знать рецензенту
называют судей по имени, и вхождений у трёх из них стало 2. Свой файл из
половины зовов исключён — ровно по той причине, по которой половина путей
исключает
«Свой файл».«написано впрок» не нашлось: соседние точки тех же файлов имеют по 2
вхождения, но ВТОРОЕ у каждой — самовызов внутри того же файла, а модули
«Монада»,«Законы изоморфизма»,«Закон коммутативности»,«Закон монотонности»,«Закон дистрибутивности»не ввезены ни одной строкойиспользует. Выдуманный довод хуже честного красного.их не трогает.
bootstrap/flang io .githooks/pre-push.fscript --plan Проверкане бывает — вхуке ровно один план,
«Pre push». Сторож и до правки был зван ярлыкомscript.uncalled-checks:check(.flangrc:105).Замыкание правка НЕ трогает: перепечатка семени не нужна.
Хук перед пушем зелен весь, 21 из 21, за 63 с.