docs: name the three open soundness holes

docs/DESCRIPTION.md

@@ -825,6 +825,11 @@ enum или по `неотрицательное` (`индукция по н у
 `следует «имя»` — вывод из уже доказанных свойств. Это теорема, у которой
 последняя строка `следовательно доказано` подразумевается.
 
+В примере ниже посылка «все люди смертны» верна потому, что функция «Смертен»
+определена как `да`: посылка задана определением, а не допущением. Как записать
+посылки допущениями и что prover тогда доказывает — ADR-0050 и пробы
+`flang/proof/probes/syllogism/assumptions/`.
+
 ```flang
 модуль «Силлогизм»
 
@@ -1246,7 +1251,7 @@ FLANG_MEMORY: прогон остановлен на пределе памяти
 в начале пропускается, незнакомый ключ пропускается. Файл ищется от рабочего
 каталога вверх до корня проекта, затем в домашнем каталоге.
 
-Компилятор читает из файла один ключ — `unproven`: что делать `flang run` и
+Компилятор сам читает из файла ключ `unproven` — что делать `flang run` и
 `flang io` с программой, в которой не всё доказано.
 
 | Значение | Поведение |
@@ -1267,9 +1272,10 @@ $ flang run гарантии.flang --function «Удвоить» --args '{"н":
 `FLANG_UNPROVEN`, `.flangrc`, значение по умолчанию. Значение не из списка —
 ошибка с кодом возврата 2.
 
-Остальные ключи файла (`language`, `surface`, `color`, `page`, `version`,
-`name`, `license`, `repository`, `issues`) читают скрипты репозитория и сборка
-сайта: [`guide/settings.ru.md`](guide/settings.ru.md).
+Строки `script.<имя> = <команда>` — короткие команды проекта; их запускает
+`flang run-script <имя>`. Остальные ключи (`language`, `surface`, `color`, `page`,
+`version`, `name`, `license`, `repository`, `issues`) читают скрипты репозитория и
+сборка сайта: [`guide/settings.ru.md`](guide/settings.ru.md).
 
 ## Ограничения
 
@@ -1320,6 +1326,15 @@ $ flang run гарантии.flang --function «Удвоить» --args '{"н":
   UDP нет.
 - Компилятор отвечает по-русски; ключ `language` файла настроек язык его
   сообщений не меняет.
+- Известны три места, где prover говорит «доказано» о неверном утверждении; их
+  закрывает следующая печать компилятора. Теорема с гипотезой (`дано н больше
+  0`) доказывает утверждение без этого условия; вызов через значение-функцию
+  `функция «Имя»` не учитывается проверкой завершаемости, и бесконечная петля
+  проходит как тотальная; постусловие с `таких что` используется как факт без
+  проверки ограничения. Список с пробами —
+  [`flang/proof/known-soundness-violations.md`](flang/proof/known-soundness-violations.md);
+  `bootstrap/flang io scripts/four-coverages.fscript --plan Measure` печатает
+  открытые пункты.
 - Компилятор не является формально верифицированным. Без доказательства
   принимаются сам prover, компилятор, рантайм, компилятор C и железо. Для
   safety-critical систем язык не предназначен.

docs/flang/proof/known-soundness-violations.md

@@ -26,6 +26,27 @@
 Сколько таких записей в корпусе, печатает
 `sh flang/proof/corpus-share.sh --набор корпус`.
 
+## `theorem-hypothesis-not-discharged` — открыто
+
+Ядро не сверяет гипотезы теоремы (`дано …`) с условиями утверждения, которое она
+доказывает. Теорема с `дано н больше 0` «доказывает» постусловие `результат
+больше 0` для всех `неотрицательное`, и `--strict` отвечает «доказано», а `flang
+run` на нуле нарушает постусловие. Пробы — в `flang/proof/probes/syllogism/assumptions/`.
+Задача 5311.
+
+## `loop-through-function-value` — открыто
+
+Проверка завершаемости не видит вызова через значение-функцию: бесконечная петля
+«Петля» → «Применить» от функция «Петля» проходит `flang check` как тотальная, а
+`flang run` упирается в предел шагов. Задача 3870.
+
+## `restricted-postcondition-cited-undischarged` — открыто
+
+Постусловие с ограничением `таких что` используется в доказательстве как факт без
+проверки ограничения в месте вызова. `--strict` отвечает «доказано» на ложном
+утверждении. Проба — `flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang`;
+независимый checker на этой записи отвечает кодом 3. Задача 4573.
+
 ## `verdicts-c-lean` — закрыто
 
 Проверяющая программа на C и приёмка Lean подставляют доводы развёртки

flang/proof/tables/consistency-violations.tsv

@@ -2,3 +2,6 @@ key	state
 verdicts-c-lean	closed
 rule-outside-the-table	open
 verified-in-vain	open
+theorem-hypothesis-not-discharged	open
+loop-through-function-value	open
+restricted-postcondition-cited-undischarged	open