Правило, на которое не наступает ни одна программа корпуса, невидимо для сверки эталона — и живёт только в свидетеле

Сверка стороны на flang со свидетелем на JavaScript — дифференциальная: обе стороны гоняют по программам репозитория и сравниваются побайтово. Значит она слепа ровно к тем правилам, на которые корпус не наступает. Правило, проверяемое только свидетелем, при этом зелено у сверки и выглядит перенесённым.

Это класс, а не случай: он встретился уже дважды.

Случай первый (записан отдельно): тотальная функция, зовущая обычную ИЗ ПОСТУСЛОВИЯ. Свидетель отвергает, flang/self/totality.flang поле постусловий не читает вовсе. См. totality-twin-does-not-read-postconditions.

Случай второй, измерен 20 августа: функция без строки «возвращает».

программа: функция «Ф» принимает н: число н плюс 1

node flang/bin/flang.mjs check → FLANG_TYPE «функция «Ф» не объявляет, что возвращает: без строки «возвращает» не сверяются ни тело, ни вызовы, ни примеры» эталон flang/self/types.flang → отказов нет, пустая строка

flang/self/types.flang при отсутствии объявленного типа возврата молча выдаёт «тип неизвестного», то есть джокер. Сильная типизация выключается пропуском одной строки, и не краснеет ничего.

Наступать на это правило корпусу незачем: в дереве нет ни одной программы без «возвращает» — писать так никто не станет. Поэтому дыра видна только на нарочно сломанной программе, а нарочно сломанные лежат в проверках на JavaScript, которые выбрасывают вместе со второй реализацией.

Признак, по которому третий случай ищется заранее. Возьмите правило, записанное в flang/src/*.mjs, и спросите: есть ли в дереве хоть одна программа, которая его нарушает? Если нет — сверка про это правило не говорит ничего, каким бы зелёным ни был её цвет. Проверять надо прогоном нарочно сломанной программы через ОБЕ стороны и сравнением ответов, а не чтением сверки.

Чем подтверждено. Ветка vypusk/zamestit-proverki, дерево на коммите 4780c595. Обе стороны прогнаны: свидетель — flang check, эталон — flang run по цепочке «Разбор исходника» → «Проверить типы» (файл flang/self/otkazy-tipov.flang). Ответы приведены дословно.

Снял правило из свидетеля и посмотрел, что покраснеет: из flang/src/types.mjs убран отказ про «возвращает» — красным стал ровно один тест во всём дереве, flang/test/types.test.mjs «функция без «возвращает» — отказ, а не молчаливый джокер». Прогнаны types, self-types, corpus-claims, stdlib-claims, claim-guard, spec-guard; остальное красное на этих файлах было красным и до правки (сверено с полным прогоном дерева).

Чем ограничено. Найдено два правила, и искали не переборно: разбор шёл по 128 утверждениям totality.test.mjs и types.test.mjs. Сколько таких правил во всём дереве — не мерено.

Связано: totality-twin-does-not-read-postconditions, checks-that-stopped-comparing, flang-test-is-always-green-on-a-layer-with-no-examples-of-its-own, a-compiler-refusal-on-the-flang-side-is-a-value-so-an-example-sees-it