From e8a0d2189f91bbe8ecfe525876c602f8dc892af0 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 18:23:33 +0000 Subject: [PATCH 01/11] fix(checker): reject a record whose hypothesis is not the statement's The independent checker accepted a theorem's assumption lines without asking where they came from. It now requires each one to be a conjunct of the statement's such-that clause, a precondition of the function, or "X >= 0" for a variable of a built-in segment type; otherwise code 1. New family flang/proof/checker/tests/families/hypothesis has an honest and a forged record per rule; the k2b record (a postcondition proved under a hypothesis it does not have) moves from honest to forged; two record-lies forgeries join the manifest and the forgeries ratchet. The checker-code-lines ceiling rises by the 32 lines spent. Prose numbers, the proved-share ledger and the tree inventory follow the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- .github/workflows/binary.yml | 4 +-- docs/flang/self/SPEC.md | 2 +- docs/site/sitemap.mjs | 4 +-- flang/proof/checker/checker.c | 32 +++++++++++++++++++ .../precondition-carries-the-hypothesis.flang | 18 +++++++++++ ...precondition-carries-the-hypothesis.record | 25 +++++++++++++++ .../precondition-says-something-else.flang | 18 +++++++++++ .../precondition-says-something-else.record | 25 +++++++++++++++ .../statement-carries-the-hypothesis.record | 24 ++++++++++++++ ...ement-does-not-carry-the-hypothesis.record | 23 +++++++++++++ .../type-carries-the-hypothesis.flang | 17 ++++++++++ .../type-carries-the-hypothesis.record | 25 +++++++++++++++ .../type-does-not-carry-the-hypothesis.flang | 17 ++++++++++ .../type-does-not-carry-the-hypothesis.record | 25 +++++++++++++++ flang/proof/checker/tests/probes.tsv | 10 +++++- ...ypothesis-outside-the-postcondition.record | 25 +++++++++++++++ ...ry-hypothesis-outside-the-statement.record | 23 +++++++++++++ flang/proof/forgeries/manifest.tsv | 2 ++ scripts/ledgers/proved-share-ledger.txt | 5 +++ 19 files changed, 318 insertions(+), 6 deletions(-) create mode 100644 flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang create mode 100644 flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record create mode 100644 flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang create mode 100644 flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record create mode 100644 flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record create mode 100644 flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record create mode 100644 flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang create mode 100644 flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record create mode 100644 flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang create mode 100644 flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record create mode 100644 flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record create mode 100644 flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index 49e39d19e..5d5426243 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -693,9 +693,9 @@ jobs: # Шаги «Run kernel examples» и «Run stdlib examples» выше зовут `flang test` # на двух # каталогах, и `flang/self/` среди них нет. Каталог при этом не пустой: 64 - # файл и 5185 примеров, объявленных внутри функций. + # файл и 5186 примеров, объявленных внутри функций. # СНЯТО 2026-09-17 файлов flang/self/*.flang = 64 - # СНЯТО 2026-09-17 примеров-в flang/self/*.flang = 5185 + # СНЯТО 2026-09-17 примеров-в flang/self/*.flang = 5186 # # Единственная работа, которая до них добралась бы, — `korpus` ниже # (`flang test . --ledger` внутри `обход-примеров.sh`). Она закрыта условием diff --git a/docs/flang/self/SPEC.md b/docs/flang/self/SPEC.md index 34a12da10..63fe85a05 100644 --- a/docs/flang/self/SPEC.md +++ b/docs/flang/self/SPEC.md @@ -14,7 +14,7 @@ JavaScript снята 20 августа 2026 (коммит `fe8e8a37`), и св ## Состав каталога 64 файла `.flang`, - 139 780 строк + 139 820 строк Имя модуля — первая строка файла; здесь оно повторено, чтобы читать `использует «…»` в других файлах без поиска. diff --git a/docs/site/sitemap.mjs b/docs/site/sitemap.mjs index 66eeeb1f3..01c8ef500 100644 --- a/docs/site/sitemap.mjs +++ b/docs/site/sitemap.mjs @@ -270,8 +270,8 @@ export const РАЗДЕЛЫ = [ страницы: [ /* СПЕЦИФИКАЦИЯ ЯДРА ПЕРЕЕХАЛА СЮДА ИЗ РАЗДЕЛА «ДОКАЗАТЕЛЬСТВА», где стояла третьим пунктом — на дорожке читателя. Жанр у неё тот же, что у трёх - соседей по этому разделу: контракт на 4821 строк, где рядом с правилом - СНЯТО 2026-09-17 строк docs/flang/proof/SPEC.md = 4821 + соседей по этому разделу: контракт на 4829 строк, где рядом с правилом + СНЯТО 2026-09-17 строк docs/flang/proof/SPEC.md = 4829 ядра стоят пути к файлам реализации, имена проверок и разбор отвергнутых редакций. Читателю на тот же вопрос отвечают «Что доказано, а что нет» и «Зачем и как». Адрес не сменился. */ diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index c427bae14..42a8b98d0 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -8813,6 +8813,37 @@ static void сверить_разметку_теоремы(Сверка *s, Сп имя_т, j + 1, в_уголках(доп.e[j], 1), где_д, P)); } } } +static int среди_конъюнктов(const char *гипотеза, const char *ограничение) { + Сп части = разделить_сверху(терм(ограничение), "и притом"); int j; + if (части.n < 2) return совпали_цели(гипотеза, терм(ограничение)); + for (j = 0; j < части.n; j++) if (среди_конъюнктов(гипотеза, части.e[j])) return 1; + return 0; +} +static char *тип_переменной(Сп строки, const char *место, const char *чья, const char *имя) { + Доводы д; int k; + if (строка_высказывания(строки, место)) return из_высказывания(строки, строка_высказывания(строки, место), имя, NULL); + д = доводы_функции(строки, чья); + for (k = 0; k < д.имена.n; k++) if (strcmp(голо(д.имена.e[k]), имя) == 0) return д.типы.e[k]; + return (char *)""; +} +static int факт_типа(const char *гипотеза, Сп строки, const char *место, const char *чья) { + Разрез r = разрез_по(гипотеза, "не меньше"); + if (!r.есть || strcmp(ужать(r.право), "0") != 0) return 0; + return натуральное_имя(имя_типа(тип_переменной(строки, место, чья, голо(ужать(r.лево))))); +} +static void сверить_снятие_гипотез(Сверка *s, Сп свои, Сп строки, const char *имя_т, const char *место, const char *чья) { + Сп доп = все_с_началом(свои, "допущение "), тч = все_с_началом(свои, "таких что "), огр = ПУСТО; + Сп треб = строка_высказывания(строки, место) ? ПУСТО : все_требования_функции(строки, чья); int i, j; + for (j = 0; j < тч.n; j++) добавить(&огр, в_уголках(тч.e[j], 1)); + for (j = 0; j < треб.n; j++) добавить(&огр, формула_требования(треб.e[j])); + for (i = 0; i < доп.n; i++) { + char *г = терм(в_уголках(доп.e[i], 1)); int снята = факт_типа(г, строки, место, чья); + for (j = 0; j < огр.n && !снята; j++) снята = среди_конъюнктов(г, огр.e[j]); + если_не(s, снята, + fmt("теорема «%s»: гипотеза ⟨%s⟩ строки %ld не является допущением утверждения — её нет ни в «таких что», ни в «требует», ни в объявленном типе", + имя_т, в_уголках(доп.e[i], 1), номер_после(доп.e[i], "строка "))); + } +} static void сверить_теорему(Сверка *s, Сп свои, Сп строки, const char *вердикт, const char *место, const char *имя, const char *чья) { char *строка_т = первая_с_началом(свои, "теорема «"); @@ -8822,6 +8853,7 @@ static void сверить_теорему(Сверка *s, Сп свои, Сп long не_проигрываемых_до = 0, моих_не_проигрываемых; long законом_до = 0; сверить_разметку_теоремы(s, свои, строки, имя_т, начало); + сверить_снятие_гипотез(s, свои, строки, имя_т, место, чья); сверить_цель(s, свои, строки, место, имя, имя_т); сверить_имена(s, свои, строки, имя_т); сверить_число_шагов(s, свои, имя_т); diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang new file mode 100644 index 000000000..3301ed481 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang @@ -0,0 +1,18 @@ +модуль «Гипотеза из предусловия» + +тотальная функция «Тождество» + принимает н: число + возвращает число + требует «положительно» н больше 0 + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: число + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record new file mode 100644 index 000000000..b42b946d1 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang +строк 19 +знаков 417 +отпечаток 696440175 224234539 +ядро 2 +утверждений 1 +отпечаток256 1279e243d184054e95dc9a025d414538529010952c6bd30f148e08ee3829a412 +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 7 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 13 + дано «н» строка 14 + допущение ⟨н больше 0⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang b/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang new file mode 100644 index 000000000..8742275bd --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang @@ -0,0 +1,18 @@ +модуль «Гипотеза мимо предусловия» + +тотальная функция «Тождество» + принимает н: число + возвращает число + требует «не больше десяти» н не больше 10 + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: число + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record b/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record new file mode 100644 index 000000000..64d9a7bc4 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang +строк 19 +знаков 427 +отпечаток 245808399 123859526 +ядро 2 +утверждений 1 +отпечаток256 dcc574881f36a2482bcb690dcb018a33be15a742a253e36c174aa886cc41e07b +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 7 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 13 + дано «н» строка 14 + допущение ⟨н больше 0⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record new file mode 100644 index 000000000..5c4731ad9 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates.flang +строк 17 +знаков 461 +отпечаток 696832843 458177874 +ядро 2 +утверждений 1 +отпечаток256 30c4cfb03e306871c94db8e1879248dc19bc8a776cd9491225cc8f9ade6c57e7 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«человек»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record new file mode 100644 index 000000000..b78dfdc35 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record @@ -0,0 +1,23 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang +строк 17 +знаков 366 +отпечаток 53964851 273723984 +ядро 2 +утверждений 1 +отпечаток256 861637269d91bffa21c869b2793bf0a4c52406d3f2bab7804e55e85f1708e310 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 2 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang new file mode 100644 index 000000000..109b6d776 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang @@ -0,0 +1,17 @@ +модуль «Гипотеза из объявленного типа» + +тотальная функция «Тождество» + принимает н: неотрицательное + возвращает неотрицательное + обеспечивает «результат не меньше нуля» результат не меньше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат не меньше нуля» + дано н: неотрицательное + дано н не меньше 0 + утверждаем результат не меньше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record new file mode 100644 index 000000000..0bc911fdd --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang +строк 18 +знаков 432 +отпечаток 674178374 56366058 +ядро 2 +утверждений 1 +отпечаток256 27af15a89c5716f575d535a2b49c0fab83f206fbe20cc513a847b284f89775be +тотальностей 1 +утверждение «результат не меньше нуля» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат не меньше нуля» строка 12 + дано «н» строка 13 + допущение ⟨н не меньше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang new file mode 100644 index 000000000..07d7e1842 --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang @@ -0,0 +1,17 @@ +модуль «Гипотеза мимо объявленного типа» + +тотальная функция «Тождество» + принимает н: целое + возвращает целое + обеспечивает «результат не меньше нуля» результат не меньше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат не меньше нуля» + дано н: целое + дано н не меньше 0 + утверждаем результат не меньше 0 + по предположению + следовательно доказано diff --git a/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record new file mode 100644 index 000000000..537937eed --- /dev/null +++ b/flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang +строк 18 +знаков 404 +отпечаток 87906575 656688072 +ядро 2 +утверждений 1 +отпечаток256 5f7411a5e4db417cffb087a8d728a0870521e331bceff832ba47dc666c8791ae +тотальностей 1 +утверждение «результат не меньше нуля» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат не меньше нуля» строка 12 + дано «н» строка 13 + допущение ⟨н не меньше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 308170266..c69996f0b 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -499,7 +499,7 @@ say - - - - - - - - - - say ── семья «ограничение» (ADR-0026 К5): «таких что» и допущения теоремы ── - - - - - - - - - - C ограничение: постусловие «таких что», строки есть (честная) flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/f09-restricted.record - - - - 3 - - - C ограничение: теорема «дано н: … таких что …», шаг по допущению 1 (честная) flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.record - - - - 3 - - - -C ограничение: теорема с гипотезой «дано н больше 0» (честная) flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.record - - - - 3 - - - +P ограничение: гипотеза «дано н больше 0», которой у постусловия нет flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.record - - - - 1 не является допущением утверждения - - P ограничение: потеряно — запись З10 матрицы (прежде код 3) flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/z10-restriction-lost.record - - - - 1 ограничение потеряно - - P ограничение: другое flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/other-restriction.record - - - - 1 «1⟩» вместо «0⟩» - - P ограничение: не под «для всех» flang/proof/checker/tests/families/restriction/f09-restricted.flang flang/proof/checker/tests/families/restriction/corrupt/restriction-not-under-the-quantifier.record - - - - 1 стоит не сразу под строкой «для всех» - - @@ -508,6 +508,14 @@ P ограничение: допущение теоремы потеряно fla P ограничение: другое допущение flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang flang/proof/checker/tests/families/restriction/corrupt/other-assumption.record - - - - 1 допущение 1 — в записи ⟨н больше 1⟩ - - P ограничение: гипотеза «дано н больше 0» без строки допущения flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/corrupt/hypothesis-without-assumption-line.record - - - - 1 допущение 16 - - say - - - - - - - - - - +say ── семья «гипотеза»: гипотеза теоремы снята ограничением утверждения ── - - - - - - - - - - +C гипотеза: часть «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates.flang flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record - - - - 3 - - - +P гипотеза: у утверждения «таких что» нет flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +C гипотеза: предусловие «требует» функции (честная) flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record - - - - 3 - - - +P гипотеза: предусловие говорит о другом flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record - - - - 1 не является допущением утверждения - - +C гипотеза: «не меньше 0» из объявленного отрезка (честная) flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record - - - - 3 - - - +P гипотеза: «не меньше 0» о целом flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +say - - - - - - - - - - say ── семья «утверждение» (ADR-0026 К3a): утверждение без функции ── - - - - - - - - - - C утверждение: связывание и теорема по индукции (честная, проиграна целиком — К3b) flang/proof/checker/tests/families/statement/f05k-statement.flang flang/proof/checker/tests/families/statement/f05k-statement.record - - - - 0 - - - C утверждение: связывание с «таких что» (честная, проиграна целиком — К3b) flang/proof/checker/tests/families/statement/statement-with-restriction.flang flang/proof/checker/tests/families/statement/statement-with-restriction.record - - - - 0 - - - diff --git a/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record new file mode 100644 index 000000000..6e06bf49e --- /dev/null +++ b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-postcondition.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang +строк 18 +знаков 397 +отпечаток 532831252 749675408 +ядро 2 +утверждений 1 +отпечаток256 6a99a14564c6c03d2326a43bcffb44ffad8957f916db604b9853dcaf0bd822cb +тотальностей 1 +утверждение «результат положителен» функции «Тождество» строка 6 + вид postcondition + вердикт доказано + теорема «результат положителен» строка 12 + дано «н» строка 13 + допущение ⟨н больше 0⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Тождество» строка 3 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record new file mode 100644 index 000000000..b78dfdc35 --- /dev/null +++ b/flang/proof/checker/tests/records/corpus/forgery-hypothesis-outside-the-statement.record @@ -0,0 +1,23 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang +строк 17 +знаков 366 +отпечаток 53964851 273723984 +ядро 2 +утверждений 1 +отпечаток256 861637269d91bffa21c869b2793bf0a4c52406d3f2bab7804e55e85f1708e310 + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 2 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/forgeries/manifest.tsv b/flang/proof/forgeries/manifest.tsv index 2eb94f32d..e16aa9aff 100644 --- a/flang/proof/forgeries/manifest.tsv +++ b/flang/proof/forgeries/manifest.tsv @@ -35,3 +35,5 @@ flang/proof/checker/tests/families/carrier/alias-not-a-segment.flang flang/proof flang/proof/examples/forgery-subtraction-under-precondition.flang flang/proof/checker/tests/records/corpus/poddelka-raznost-bez-poryadka.record record-lies flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang flang/proof/checker/tests/records/corpus/poddelka-razv2-sebya.record record-lies 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 diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index 02e6cd75a..d9b8515e2 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1185,6 +1185,10 @@ c895d96922efd9cd69238c4e9fd31b2d|1|1|0|0|0|flang/proof/checker/tests/families/ca f156b44ebb9d062276fb048d8d558551|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang 43516f88b43387599d936a2979af66d1|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang bc17b199769f3c2a966e71d18ebcee89|1|×|×|×|0|flang/proof/checker/tests/families/restriction/f09-restricted.flang +2f70a5cf8cbb44e1a88bdf15eee9b1c9|2|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang +2c28f2fe75e00f19601f9f6cf9f8d835|2|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang +ad3459ff6037a5f4fd987dad04cdcb69|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang +d645f02d887cf92fdffc69f02adc2e82|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang 48fabdcaa9d040986fe87d584786ff9b|1|0|0|0|1|flang/proof/checker/tests/families/plan/temporary-directory.flang 58695c0261bca20c054c8f8e7fade6c3|1|0|0|0|1|flang/proof/checker/tests/families/plan/corrupt/foreign-order.flang 441a75abee9f78ef507959ee1b7155a8|1|×|×|×|1|flang/proof/checker/tests/families/coverage/o9-fold-start-one.flang @@ -1598,6 +1602,7 @@ af7fda1d841676c09ef8c20595636892|1|1|0|1|0|flang/proof/checker/tests/programs/75 b84a0d9b2c597e85945650941c5bb1c9|1|0|1|0|0|flang/proof/probes/run/programs/grid.flang 1e489b4612bc356f4c6a28b0b7bfaa4b|1|1|0|1|0|flang/proof/checker/tests/programs/7563/identity.flang 66a842f08485d3ff08202a087187e3b5|1|0|0|0|0|flang/proof/probes/run/programs/plan-proved.flang +fd9c112a1fec91f46377a3ae4c907af2|1|×|×|×|0|flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang 4704717d9ed5ce08f447c0e69f5c6b5f|1|1|0|1|0|flang/proof/checker/tests/programs/7563/unfold1-constructor.flang // ── Набор проб строгого режима (задача 5502), снято 19 сентября 2026 ────── // Семь программ каталога `flang/proof/probes/strict/programs/`; восьмая From 4fd40724f3c952975b5f4a5ce1ab74806d8f2e1b Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 18:24:55 +0000 Subject: [PATCH 02/11] fix(checker): name the forged precondition probe in listed words The forged precondition probe of the hypothesis family carried a word outside the file-name word list; it is now named like its siblings, and its proved-share ledger row counts the one postcondition the ledger counts. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- ...flang => precondition-does-not-carry-the-hypothesis.flang} | 0 ...cord => precondition-does-not-carry-the-hypothesis.record} | 2 +- flang/proof/checker/tests/probes.tsv | 2 +- scripts/ledgers/proved-share-ledger.txt | 4 ++-- 4 files changed, 4 insertions(+), 4 deletions(-) rename flang/proof/checker/tests/families/hypothesis/{precondition-says-something-else.flang => precondition-does-not-carry-the-hypothesis.flang} (100%) rename flang/proof/checker/tests/families/hypothesis/{precondition-says-something-else.record => precondition-does-not-carry-the-hypothesis.record} (95%) diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang similarity index 100% rename from flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang rename to flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang diff --git a/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record similarity index 95% rename from flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record rename to flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record index 64d9a7bc4..e54c8bc78 100644 --- a/flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record +++ b/flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record @@ -1,5 +1,5 @@ запись доказательства 1 -исходник flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang +исходник flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang строк 19 знаков 427 отпечаток 245808399 123859526 diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index c69996f0b..0d3b052b7 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -512,7 +512,7 @@ say ── семья «гипотеза»: гипотеза теоремы сн C гипотеза: часть «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates.flang flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record - - - - 3 - - - P гипотеза: у утверждения «таких что» нет flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - C гипотеза: предусловие «требует» функции (честная) flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record - - - - 3 - - - -P гипотеза: предусловие говорит о другом flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.record - - - - 1 не является допущением утверждения - - +P гипотеза: предусловие говорит о другом flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - C гипотеза: «не меньше 0» из объявленного отрезка (честная) flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record - - - - 3 - - - P гипотеза: «не меньше 0» о целом flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - say - - - - - - - - - - diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index d9b8515e2..c88a6b2ae 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1185,8 +1185,8 @@ c895d96922efd9cd69238c4e9fd31b2d|1|1|0|0|0|flang/proof/checker/tests/families/ca f156b44ebb9d062276fb048d8d558551|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang 43516f88b43387599d936a2979af66d1|1|×|×|×|0|flang/proof/checker/tests/families/restriction/k2bk-theorem-such-that.flang bc17b199769f3c2a966e71d18ebcee89|1|×|×|×|0|flang/proof/checker/tests/families/restriction/f09-restricted.flang -2f70a5cf8cbb44e1a88bdf15eee9b1c9|2|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang -2c28f2fe75e00f19601f9f6cf9f8d835|2|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-says-something-else.flang +2f70a5cf8cbb44e1a88bdf15eee9b1c9|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang +2c28f2fe75e00f19601f9f6cf9f8d835|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang ad3459ff6037a5f4fd987dad04cdcb69|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang d645f02d887cf92fdffc69f02adc2e82|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang 48fabdcaa9d040986fe87d584786ff9b|1|0|0|0|1|flang/proof/checker/tests/families/plan/temporary-directory.flang From e5734c1299328e40245cae011c5347e8d372f70c Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 19:57:08 +0000 Subject: [PATCH 03/11] feat(checker): replay by-assumption steps from the statement premises The independent checker left every "by assumption" step outside induction on the kernel's word, so the five valid syllogism moods proved from premises got code 3, Darii with the existence word got code 1 and a statement whose premises sit only in its such-that clause got code 1. For a statement without a function whose theorem steps are all "by assumption", whose formulas are built from boolean fields of objects bound by the statement, the checker now takes the conjuncts of the statement's such-that clause as premises and replays each step: it must follow in one move (a premise, modus ponens from "if A then F else yes", a conjunction of such, or "no" from X and "not X"). An existence goal is compared and replayed with the witness substituted, also inside field access. Each step is also judged by a truth table over the fields: a valuation where the premises hold and the step fails is code 1 with that valuation; a true step that needs more than one move stays on the kernel's word. The step's assumption number may now point at the such-that clause. New family tests/families/assumption-replay: eight honest records now checked (code 0), ten forged ones refused with code 1 (five invalid moods, premise about another object, witness without premises, witness differing from the statement, refutation without its minor premise, a swapped assumption line) and one valid but two-move record kept at code 3. checker-code-lines rises by the 102 lines spent, forgery-probes by the 11 new forged rows. The missing probe program named by the forgeries manifest comes from the kernel change of task 5311. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- ...n-as-declared-words-and-fixed-sentences.md | 48 ++++---- docs/flang/proof/checker/README.md | 14 +++ flang/proof/checker/checker.c | 115 +++++++++++++++++- .../affirming-the-consequent.record | 24 ++++ .../barbara-without-the-middle-step.record | 25 ++++ .../families/assumption-replay/barbara.record | 26 ++++ .../camestres-by-refutation.record | 28 +++++ .../assumption-replay/celarent.record | 26 ++++ .../darii-with-the-existence-word.record | 27 ++++ .../families/assumption-replay/darii.record | 25 ++++ .../denying-the-antecedent.record | 24 ++++ .../existential-import.record | 24 ++++ .../families/assumption-replay/ferio.record | 25 ++++ .../illicit-conversion.record | 24 ++++ .../premise-about-another-object.flang | 17 +++ .../premise-about-another-object.record | 26 ++++ .../premise-about-the-same-object.flang | 17 +++ .../premise-about-the-same-object.record | 26 ++++ .../premises-only-in-the-statement.record | 22 ++++ ...refutation-without-the-minor-premise.flang | 20 +++ ...efutation-without-the-minor-premise.record | 27 ++++ .../undistributed-middle.record | 25 ++++ .../witness-differs-from-the-statement.flang | 19 +++ .../witness-differs-from-the-statement.record | 29 +++++ .../witness-without-premises.flang | 19 +++ .../witness-without-premises.record | 29 +++++ flang/proof/checker/tests/probes.tsv | 22 +++- .../probes/syllogism/assumptions/expected.tsv | 18 +-- ...ith-a-hypothesis-only-in-the-theorem.flang | 17 +++ 29 files changed, 750 insertions(+), 38 deletions(-) create mode 100644 flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/barbara.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/celarent.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/darii.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/existential-import.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/ferio.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang create mode 100644 flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang create mode 100644 flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang create mode 100644 flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang create mode 100644 flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record create mode 100644 flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang create mode 100644 flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record create mode 100644 flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang diff --git a/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md b/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md index 6ce430e7a..bbd406a30 100644 --- a/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md +++ b/docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md @@ -57,30 +57,37 @@ | модус | программа | ядро, `check --proof --strict` | независимая проверяющая программа | |---|---|---|---| -| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 3, «не проверено» | -| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 3 | -| Celarent | `celarent.flang` | доказано, код 0 | код 3 | -| Darii | `darii.flang` | доказано, код 0 | код 3 | -| Ferio | `ferio.flang` | доказано, код 0 | код 3 | +| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 0, «проверено» | +| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 0 | +| Celarent | `celarent.flang` | доказано, код 0 | код 0 | +| Darii | `darii.flang` | доказано, код 0 | код 0 | +| Ferio | `ferio.flang` | доказано, код 0 | код 0 | | Camestres, прямая цель `(не x.P)` | `camestres.flang` | **отказ**, код 1: ядро не выводит отрицание | записи нет | -| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 3 | +| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 0 | | Barbara без промежуточного шага | `barbara-without-the-middle-step.flang` | **отказ**, код 1: ядро делает один модус поненс, не цепочку | записи нет | | подтверждение следствия | `affirming-the-consequent.flang` | отказ, код 1, `FLANG_PROOF_STEP` на строке заключения | записи нет | | нераспределённый средний | `undistributed-middle.flang` | отказ, код 1 | записи нет | | незаконное обращение | `illicit-conversion.flang` | отказ, код 1 | записи нет | | отрицание антецедента | `denying-the-antecedent.flang` | отказ, код 1 | записи нет | | экзистенциальный импорт (Barbari) | `existential-import.flang` | отказ, код 1 | записи нет | -| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | **код 1, «не сошлось»** | -| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | **код 1, «допущений в записи 0»** | -| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | код 3 | +| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | код 0 | +| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | код 0 | +| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | **код 1**: гипотеза не является допущением утверждения | | без теоремы, ядро само | `socrates-without-a-theorem.flang` | доказано, код 0 | код 3 | | предикаты — параметры-функции | `socrates-with-predicates-as-functions.flang` | доказано, код 0 | код 3 | Итог по вопросу (1): пять названных правильных модусов ядро доказывает, пять ошибок -отвергает кодом 1 с именем шага. Независимая проверяющая программа ни одного вывода из -допущений сегодня не переигрывает (шаг `по предположению` вне индукции — «на слове ядра», -код 3) — это её объявленная граница, а не расхождение; расхождения (код 1) ровно два, и оба -названы в таблице. +отвергает кодом 1 с именем шага. Независимая проверяющая программа переигрывает все пять +сама и отвечает кодом 0. Шаг `по предположению` в утверждении без функции она выводит из +частей его `таких что` (разобранных по `и притом`), а не из строк `дано`: промежуточный шаг +`затем Ф` и цель обязаны выводиться одним шагом — Ф есть посылка; есть посылка `если А то Ф +иначе да` при известном А; Ф — конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель +`есть такой м, а именно Т, что У` читается как У с Т на месте м. Каждый шаг ещё и судится +таблицей истинности по признакам `«x».«поле»`: нашлось присвоение, при котором посылки верны, +а шаг ложен, — код 1 с этим присвоением; шаг верен, но не одним шагом, — код 3. Записи, +составленные для пяти ошибочных модусов, отвергаются кодом 1. Правило стоит 102 строки кода +`checker.c` (храповик `checker-code-lines`); пробы — семья +`flang/proof/checker/tests/families/assumption-replay/`. Полный перебор: 256 модусов четырёх фигур прогнаны текстами через переводчик (`flang/proof/probes/syllogism/sentences/`, план `Binary` на 256 порождённых текстах, ключ @@ -118,13 +125,12 @@ «Сократ».«смертен»`. То же с постусловием: функция тождества на `неотрицательное` с постусловием `результат больше 0` и теоремой с `дано н больше 0` — «доказано», код 0, а `flang run` на нуле печатает `FLANG_PROPERTY`. Ядро не сверяет гипотезы теоремы с -ограничениями утверждения. Независимая проверяющая программа спасает лишь тем, что не даёт -нуля (код 3). Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md). +ограничениями утверждения. Независимая проверяющая программа отвергает такую запись кодом 1: +гипотеза не является допущением утверждения. Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md). Следствие для этого решения: переводчик пишет посылки **в `таких что` утверждения** — тогда утверждение само говорит, при каких допущениях доказано заключение, — и повторяет их в `дано`, -потому что без строк `дано` независимая проверяющая программа отвечает кодом 1 (запись не -несёт допущений из `таких что`). +чтобы теорема читалась сама по себе; проверяющей программе хватает `таких что`. ## 6. Словарь и образцы предложений @@ -178,9 +184,9 @@ * **Посылки отдельными `утверждение` и шаг `по свойству`** (`programs/conditional.flang`): честно, но файл уходит кодом 3 «доказано ПРИ УСЛОВИИ» — посылка сама «объявлено, не доказано». Силлогизм — это «из посылок следует», а не «посылки верны». -* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, а - независимая проверяющая программа отвечает кодом 1. Заключение пишется конъюнкцией о - свидетеле. +* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, и + проверяющая программа переигрывает, но конъюнкция о свидетеле короче и читается прямо. + Заключение пишется ею. ## 8. Цена в грамматике, если делать словом языка @@ -211,8 +217,6 @@ прямой целью, без опровержения. * **Цепочка охран:** повторять модус поненс до неподвижной точки, чтобы `затем` не требовался на каждое звено. Дёшево: перебор конечен. -* **Проверяющая программа переигрывает `по предположению` вне индукции** и читает допущения - из `таких что` утверждения — иначе силлогизм навсегда «на слове ядра». * Если рассуждение становится файлом языка: вид файла `.рассуждение` со своим разбором (§6), разворачивающимся в `объект` + `утверждение` + `следует` ровно так, как печатает `--plan Translate`; отказ разбора называет слово и предложение. diff --git a/docs/flang/proof/checker/README.md b/docs/flang/proof/checker/README.md index af5d1a4d3..4cf50ebd9 100644 --- a/docs/flang/proof/checker/README.md +++ b/docs/flang/proof/checker/README.md @@ -174,6 +174,20 @@ bootstrap/flang run-script trust:ceiling что тело функции: литерал, `длина`, сумма, произведение на положительный литерал. Неотрицательным по объявлению считается только имя, связанное `для всех` типом-отрезком (`неотрицательное`); ограничение `таких что` дна не даёт. +22. **Шаг `по предположению` в утверждении без функции выводится из его посылок.** + Когда все шаги теоремы обоснованы `по предположению`, нет ни индукции, ни + случаев, а каждое высказывание собрано из признаков `«x».«поле»` (`x` + связан `для всех`, поле объявлено `признак` в `объект` его типа), посылками + служат части `таких что` утверждения, разобранные по `и притом`, — строки + `дано` теоремы в вывод не идут. Промежуточный шаг `затем Ф по предположению` + и цель обязаны выводиться одним шагом из посылок и выведенного раньше: Ф + есть посылка; есть посылка `если А то Ф иначе да` при известном А; Ф — + конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель `есть такой м, + а именно Т, что У` сличается с обещанной и выводится как У с Т на месте м. + Каждый шаг ещё и судится таблицей истинности по признакам: нашлось + присвоение, при котором посылки верны, а шаг ложен, — «НЕ СОШЛОСЬ» с этим + присвоением; шаг верен, но не одним шагом, — место остаётся на слове ядра. + Пробы — `tests/families/assumption-replay/`. Сверх того: **ни одной непрочитанной строки**. Строка записи, вид которой чекеру не известен, — отказ, а не «ладно». Мутационная проба (3000 порченых diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index 42a8b98d0..ca9a1897d 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -419,6 +419,11 @@ static char *цель_обещанная(const char *ц) { char *м, *т, *у; return разобрать_существование(ц, &м, &т, &у) ? терм(вставить_вместо(терм(у), м, терм(т))) : (char *)ц; } +static char *со_свидетелем(const char *ц) { + char *м, *т, *у; + if (!разобрать_существование(ц, &м, &т, &у)) return терм(ц); + return терм(вставить_вместо(заменить(заменить(fmt(" %s ", терм(у)), fmt(" %s.", голо(м)), fmt(" %s.", т)), fmt(" «%s».", голо(м)), fmt(" %s.", т)), м, т)); +} /* У утверждения без функции «место» — его заголовок `утверждение «И»` от края, цель — хвост строки `утверждаем`, типы и имена связанных — строки `для всех` @@ -1862,7 +1867,7 @@ static void сверить_цель(Сверка *s, Сп свои, Сп стр long гв = строка_высказывания(строки, место); /* К3b: утверждение без функции */ char *сырое = гв ? из_высказывания(строки, гв, NULL, NULL) : с_продолжением(строки, номер_после(часть(свои, 1), "строка "), хвост_после(как_читает_язык(место), fmt("обеспечивает «%s» ", имя))); - char *обещано = гв ? терм(цель_обещанная(сырое)) + char *обещано = гв ? со_свидетелем(сырое) : цель_обещанная(сырое); /* К7: у существования — У[м:=Т], как терм */ char *строка_цели = первая_с_началом(свои, "цель "); long где = номер_после(строка_цели, "строка "); @@ -1873,7 +1878,7 @@ static void сверить_цель(Сверка *s, Сп свои, Сп стр сверить_терм_и_номер(s, строка_цели, утверждено, где, имя_т, "цель"); утверждено = с_продолжением(строки, где, утверждено); } - если_не(s, strcmp(обещано, обещано == сырое ? утверждено : терм(утверждено)) == 0, + если_не(s, strcmp(обещано, обещано == сырое ? утверждено : гв ? со_свидетелем(утверждено) : терм(утверждено)) == 0, fmt("теорема «%s» утверждает «%s», а %s обещает «%s» — доказывается не то, что обещано", имя_т, утверждено, гв ? "утверждение" : "постусловие", обещано)); } @@ -3502,13 +3507,109 @@ static void сверить_правило_шага(Сверка *s, const char * } } +typedef struct { Сп строки, имена, атомы; long гв; unsigned long набор; } Посылки; +static Сп связка(const char *t, const char *op) { + Сп ч = разделить_сверху(t, op); int i; + for (i = 0; ч.n > 1 && i < ч.n; i++) if (начинается(обрезать(ч.e[i]), "если ")) return ПУСТО; + return ч; +} +static Сп конъюнкты(const char *сырой) { + char *t = терм(сырой); Сп ч = связка(t, "и притом"), итог = ПУСТО; int i, j; + if (ч.n < 2 || связка(t, "или").n != 1) { добавить(&итог, t); return итог; } + for (i = 0; i < ч.n; i++) { Сп в = конъюнкты(ч.e[i]); for (j = 0; j < в.n; j++) добавить(&итог, в.e[j]); } + return итог; +} +static int признак_ли(Посылки *п, const char *атом) { + int i; long j; + for (i = 0; i < п->имена.n; i++) { + char *т = fmt("объект «%s»", голо(из_высказывания(п->строки, п->гв, п->имена.e[i], NULL))); + for (j = 1; j <= п->строки.n && strcmp(строка_по_номеру(п->строки, j), т) != 0; j++) ; + for (j++; j <= п->строки.n && начинается(часть(п->строки, j), " "); j++) { + char *s = строка_по_номеру(п->строки, j), *поле = голо(часть(разделить(s, ":"), 1)); + if (strcmp(обрезать(хвост_после(s, ":")), "признак") == 0 && + (strcmp(атом, fmt("«%s».«%s»", п->имена.e[i], поле)) == 0 || strcmp(атом, fmt("%s.«%s»", п->имена.e[i], поле)) == 0)) return 1; + } + } + return 0; +} +static int истинно(const char *сырой, Посылки *п) { + char *t = терм(сырой); Сп или = связка(t, "или"), ч = или.n == 1 ? связка(t, "и притом") : или; int i, a, b, c, итог = или.n == 1; + if (strcmp(t, "да") == 0 || strcmp(t, "нет") == 0) return strcmp(t, "да") == 0; + for (i = 0; ч.n > 1 && i < ч.n; i++) { if ((a = истинно(ч.e[i], п)) < 0) return -1; итог = или.n == 1 ? итог && a : итог || a; } + if (ч.n != 1) return ч.n ? итог : -1; + if (начинается(t, "не ")) return (a = истинно(t + strlen("не "), п)) < 0 ? -1 : !a; + if (начинается(t, "если ")) { + Сп то = разделить_сверху(t + strlen("если "), "то"), ин = разделить_сверху(часть(то, 2), "иначе"); + if (то.n != 2 || ин.n != 2 || (a = истинно(то.e[0], п)) < 0 || (b = истинно(ин.e[0], п)) < 0 || (c = истинно(ин.e[1], п)) < 0) return -1; + return a ? b : c; + } + for (i = 0; i < п->атомы.n && strcmp(п->атомы.e[i], t) != 0; i++) ; + if (i == п->атомы.n && (i >= 16 || !признак_ли(п, t))) return -1; + if (i == п->атомы.n) добавить(&п->атомы, t); + return (int)((п->набор >> i) & 1); +} +static long контрпример(Сп K, const char *ф, Посылки *п) { + int i, v; + for (п->набор = 0, п->атомы = ПУСТО, i = 0; i <= K.n; i++) if (истинно(i < K.n ? K.e[i] : ф, п) < 0) return -2; + for (п->набор = 0; п->набор < (1UL << п->атомы.n); п->набор++) { + for (v = 1, i = 0; i < K.n && v; i++) v = истинно(K.e[i], п); + if (v && !истинно(ф, п)) return (long)п->набор; + } + return -1; +} +static int есть_в(Сп K, const char *t) { int i; for (i = 0; i < K.n; i++) if (strcmp(K.e[i], терм(t)) == 0) return 1; return 0; } +static int выводится(Сп K, const char *ф) { + Сп ч = конъюнкты(ф); int i, j, есть; + for (j = 0; j < ч.n; j++) { + for (есть = есть_в(K, ч.e[j]), i = 0; i < K.n && !есть; i++) { + Сп то = разделить_сверху(хвост_после(K.e[i], "если "), "то"), ин = разделить_сверху(часть(то, 2), "иначе"); + есть = начинается(K.e[i], "если ") && то.n == 2 && ин.n == 2 && strcmp(терм(ин.e[1]), "да") == 0 && + strcmp(терм(ин.e[0]), ч.e[j]) == 0 && есть_в(K, то.e[0]); + есть |= strcmp(ч.e[j], "нет") == 0 && начинается(K.e[i], "не ") && есть_в(K, K.e[i] + strlen("не ")); + } + if (!есть) return 0; + } + return 1; +} +static char *формула_шага(Сп строки, const char *ш) { + long где = номер_после(ш, "строка "); char *l = где < 1 ? (char *)"" : без_то(с_продолжением(строки, где, как_читает_язык(строка_по_номеру(строки, где)))); + if (!начинается(l, "затем ") || !содержит(l, " по предположению")) return (char *)""; + return копия(l + strlen("затем "), (size_t)(strstr(l, " по предположению") - l) - strlen("затем ")); +} +static int из_посылок(Сверка *s, Сп свои, Сп строки, long гв, const char *имя_т) { + Посылки п; Сп K = ПУСТО, шаги = все_с_началом(свои, "шаг "), ч; + long i, j, m, до = s->беды.n, гц = номер_после(первая_с_началом(свои, "цель "), "строка "); + char *цель = гц < 1 ? (char *)"" : с_продолжением(строки, гц, хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем ")); + п.строки = строки; п.гв = гв; п.имена = ПУСТО; + из_высказывания(строки, гв, NULL, &п.имена); + if (!гв || гц < 1 || *первая_с_началом(свои, "случай ")) return 0; + for (i = 0; i < шаги.n; i++) if (!начинается(шаг_обоснование(шаги.e[i]), "по предположению")) return 0; + for (i = гв + 1; i <= строки.n; i++) { + char *сырая = часть(строки, i), *l = с_продолжением(строки, i, как_читает_язык(обрезать(без_примечания(сырая)))); + if (*сырая && !начинается(сырая, " ") && !начинается(сырая, "//")) break; + if (начинается(l, "для всех ") && содержит(l, " таких что ")) + for (ч = конъюнкты(хвост_после(l, " таких что ")), j = 0; j < ч.n; j++) добавить(&K, ч.e[j]); + } + for (i = 0; i < шаги.n; i++) { + char *ф = strcmp(шаг_вид(шаги.e[i]), "промежуточный") == 0 ? формула_шага(строки, шаги.e[i]) : со_свидетелем(цель); + if (!*ф || (m = контрпример(K, ф, &п)) == -2) return 0; + if (m >= 0) { Сп при = ПУСТО; + for (j = 0; j < п.атомы.n; j++) добавить(&при, fmt("%s %s", п.атомы.e[j], (m >> j) & 1 ? "да" : "нет")); + добавить(&s->беды, fmt("теорема «%s»: шаг %s ⟨%s⟩ из посылок утверждения не следует — при %s посылки верны, а он ложен", имя_т, слово(шаги.e[i], 2), терм(ф), соединить(при, ", "))); + return 0; } + if (!выводится(K, ф)) return 0; + добавить(&K, терм(ф)); + } + return s->беды.n == до; +} + static void сверить_шаги(Сверка *s, Сп свои, Сп строки, const char *имя_т, - const char *чья, const char *цель) { + const char *чья, const char *цель, const char *место) { char *по = в_ёлочках(первая_с_началом(свои, "индукция по "), 1); /* Свободное имя в цели: `дано «х»` или индукция. Тогда `результат` не одно значение, и подстановка тела (дорога Ч76) не годится — «не берусь». */ int свободные = (*первая_с_началом(свои, "дано «") != 0) || (*по != 0); - long случай_где = 0; int i; + long случай_где = 0, гв = строка_высказывания(строки, место); int i, посылками = !*по && из_посылок(s, свои, строки, гв, имя_т); for (i = 0; i < свои.n; i++) { char *ш = обрезать(свои.e[i]); long где; char *вид, *обоснование, *в_исх; @@ -3519,7 +3620,7 @@ static void сверить_шаги(Сверка *s, Сп свои, Сп стр /* «по предположению допущение J»: J обязано быть среди допущений записи, сам вывод — на слове ядра. В исходнике шаг написан без номера, потому обоснование и урезается. */ if (начинается(обоснование, "по предположению допущение ")) { - long J = номер_после(обоснование, "допущение "), всего = все_с_началом(свои, "допущение ").n; + long J = номер_после(обоснование, "допущение "), всего = все_с_началом(свои, "допущение ").n + (гв ? ограничения_высказывания(строки, место).n : 0); если_не(s, J >= 1 && J <= всего, fmt("теорема «%s»: шаг %s закрыт допущением %ld, а допущений в записи %ld", имя_т, слово(ш, 2), J, всего)); @@ -3550,6 +3651,8 @@ static void сверить_шаги(Сверка *s, Сп свои, Сп стр предположению»: допущение у неё одно — предусловие функции, и шаг верен ровно тогда, когда тело неотрицательно по построению при этом допущении. */ s->сведений++; s->шагов_по_телу++; + } else if (посылками && strcmp(обоснование, "по предположению") == 0) { + s->сведений++; } else { /* Ветвь ловит ЛЮБОЕ обоснование, а не список имён: имя, не попавшее ни в одну ветвь, не было бы ни проверено, ни положено в долг — и пять дописанных строк @@ -8864,7 +8967,7 @@ static void сверить_теорему(Сверка *s, Сп свои, Сп не_проигрываемых_до = s->шагов_не_проигрываемых; законом_до = s->шагов_законом; сверить_шаги(s, свои, строки, имя_т, чья, - гц < 1 ? в_уголках(ск, 1) : хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем ")); } + гц < 1 ? в_уголках(ск, 1) : хвост_после(как_читает_язык(строка_по_номеру(строки, гц)), "утверждаем "), место); } сверить_закрытие(s, свои, имя_т, вердикт); сверить_правила(s, свои, fmt("теорема «%s»", имя_т)); /* Места снимаются РОВНО те, что начислила ветвь «по закону» (разница diff --git a/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record b/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record new file mode 100644 index 000000000..62375ead2 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/affirming-the-consequent.flang +строк 17 +знаков 465 +отпечаток 745919929 6196609 +ядро 2 +утверждений 1 +отпечаток256 d569dcd7796b6b754268e1f9b5abf69ee639e7a0f1437731ce70dab8e89361cb + +утверждение «Сократ — человек» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«смертен»⟩ строка 8 + вердикт доказано + теорема «Сократ — человек» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨«Сократ».«смертен»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record b/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record new file mode 100644 index 000000000..02d587e75 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/barbara-without-the-middle-step.flang +строк 19 +знаков 603 +отпечаток 411755632 493253088 +ядро 2 +утверждений 1 +отпечаток256 413625bde79b57aa18eccf452707829bd5281fee1a836703dcccdc027cb5f3fa + +утверждение «все греки смертны» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«грек» то «всякий».«человек» иначе да ) и притом «всякий».«грек»⟩ строка 9 + вердикт доказано + теорема «все греки смертны» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«грек» то «всякий».«человек» иначе да⟩ строка 15 + допущение ⟨«всякий».«грек»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/barbara.record b/flang/proof/checker/tests/families/assumption-replay/barbara.record new file mode 100644 index 000000000..442013760 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/barbara.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/barbara.flang +строк 20 +знаков 647 +отпечаток 786208141 188328047 +ядро 2 +утверждений 1 +отпечаток256 b27f9b40eb88525d04697198d80ad4f0003d0f62807c4292d2b3e3deae3ec978 + +утверждение «все греки смертны» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«грек» то «всякий».«человек» иначе да ) и притом «всякий».«грек»⟩ строка 9 + вердикт доказано + теорема «все греки смертны» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«грек» то «всякий».«человек» иначе да⟩ строка 15 + допущение ⟨«всякий».«грек»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record b/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record new file mode 100644 index 000000000..8aec8c596 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record @@ -0,0 +1,28 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/camestres-by-refutation.flang +строк 22 +знаков 756 +отпечаток 579803564 147320406 +ядро 2 +утверждений 1 +отпечаток256 f6f0058f1452bbf0d6e5710eb3e5b1f1ac7f28324ac6ce2e7153499bf8a06be0 + +утверждение «ни один кит не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да ) и притом ( если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да ) и притом «всякий».«кит» и притом «всякий».«рыба»⟩ строка 9 + вердикт доказано + теорема «ни один кит не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да⟩ строка 15 + допущение ⟨«всякий».«кит»⟩ строка 16 + допущение ⟨«всякий».«рыба»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 20 промежуточный по предположению правило «цель есть допущение» + шаг 3 строка 21 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/celarent.record b/flang/proof/checker/tests/families/assumption-replay/celarent.record new file mode 100644 index 000000000..c6d82da39 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/celarent.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/celarent.flang +строк 20 +знаков 655 +отпечаток 637001399 380025156 +ядро 2 +утверждений 1 +отпечаток256 7e344796c7cce2a3e398d676e8b7fe448b3274d8e46f57d73ce98dc4565e73d1 + +утверждение «ни один кашалот не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«кит» то ( не «всякий».«рыба» ) иначе да ) и притом ( если «всякий».«кашалот» то «всякий».«кит» иначе да ) и притом «всякий».«кашалот»⟩ строка 9 + вердикт доказано + теорема «ни один кашалот не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«кит» то ( не «всякий».«рыба» ) иначе да⟩ строка 14 + допущение ⟨если «всякий».«кашалот» то «всякий».«кит» иначе да⟩ строка 15 + допущение ⟨«всякий».«кашалот»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record b/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record new file mode 100644 index 000000000..f77153a49 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/darii-with-the-existence-word.flang +строк 19 +знаков 810 +отпечаток 998230778 390332762 +ядро 2 +утверждений 1 +отпечаток256 f1a2e9e09d35fc4c5a44e7a701d8943eb69c8e93c70927d9f639849447f195c1 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«предмет посылки 2»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/darii.record b/flang/proof/checker/tests/families/assumption-replay/darii.record new file mode 100644 index 000000000..ce4507e77 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/darii.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/darii.flang +строк 19 +знаков 762 +отпечаток 362413914 663275733 +ядро 2 +утверждений 1 +отпечаток256 8543cadffbb3d78793b799b7ae2bc1aed77d6e198b8dd84179c5d85caee15940 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record b/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record new file mode 100644 index 000000000..748db2aca --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/denying-the-antecedent.flang +строк 17 +знаков 487 +отпечаток 640233816 30024500 +ядро 2 +утверждений 1 +отпечаток256 606f0c3f7865157bc049e3388d466887c71e4a95577a5567da1f11ba455fa283 + +утверждение «Сократ не смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом ( не «Сократ».«человек» )⟩ строка 8 + вердикт доказано + теорема «Сократ не смертен» строка 11 + дано «Сократ» строка 12 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 13 + допущение ⟨не «Сократ».«человек»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/existential-import.record b/flang/proof/checker/tests/families/assumption-replay/existential-import.record new file mode 100644 index 000000000..1d4621185 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/existential-import.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/existential-import.flang +строк 18 +знаков 607 +отпечаток 767872960 659549136 +ядро 2 +утверждений 1 +отпечаток256 8a6c09850cd91cfdc57783461d805d868dcd5e67cd65c6692d0482560ea42522 + +утверждение «некоторые греки смертны» строка 8 + вид statement + для всех «некий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «некий».«человек» то «некий».«смертен» иначе да ) и притом ( если «некий».«грек» то «некий».«человек» иначе да )⟩ строка 9 + вердикт доказано + теорема «некоторые греки смертны» строка 12 + дано «некий» строка 13 + допущение ⟨если «некий».«человек» то «некий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «некий».«грек» то «некий».«человек» иначе да⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/ferio.record b/flang/proof/checker/tests/families/assumption-replay/ferio.record new file mode 100644 index 000000000..afefdf358 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/ferio.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/ferio.flang +строк 19 +знаков 824 +отпечаток 256091376 224009567 +ядро 2 +утверждений 1 +отпечаток256 5557d980818a55d74a5ea4be4fec92c7f23968fe8b1466a03e4d867f8dcba5d3 + +утверждение «некоторые морские животные — не рыбы» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кит» то ( не «предмет посылки 2».«рыба» ) иначе да ) и притом «предмет посылки 2».«морское животное» и притом «предмет посылки 2».«кит»⟩ строка 9 + вердикт доказано + теорема «некоторые морские животные — не рыбы» строка 12 + дано «предмет посылки 2» строка 13 + допущение ⟨если «предмет посылки 2».«кит» то ( не «предмет посылки 2».«рыба» ) иначе да⟩ строка 14 + допущение ⟨«предмет посылки 2».«морское животное»⟩ строка 15 + допущение ⟨«предмет посылки 2».«кит»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record b/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record new file mode 100644 index 000000000..c7255e622 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record @@ -0,0 +1,24 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/illicit-conversion.flang +строк 17 +знаков 476 +отпечаток 820816676 230149327 +ядро 2 +утверждений 1 +отпечаток256 e5523a4e2fe55d68ffb208d6c17928254590c808426e0eb3644ce039e72b9251 + +утверждение «все смертные — люди» строка 7 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «всякий».«человек» то «всякий».«смертный» иначе да ) и притом «всякий».«смертный»⟩ строка 8 + вердикт доказано + теорема «все смертные — люди» строка 11 + дано «всякий» строка 12 + допущение ⟨если «всякий».«человек» то «всякий».«смертный» иначе да⟩ строка 13 + допущение ⟨«всякий».«смертный»⟩ строка 14 + цель строка 15 + шаг 1 строка 16 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang new file mode 100644 index 000000000..71cbc848f --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +объект «Предмет» + «человек»: признак + «смертен»: признак + +утверждение «Платон смертен» + для всех «Сократ»: «Предмет» и «Платон»: «Предмет» таких что (если «Сократ».«человек» то «Сократ».«смертен» иначе да) и притом «Платон».«человек» + утверждаем «Платон».«смертен» + +следует «Платон смертен» + дано «Сократ»: «Предмет» + дано «Платон»: «Предмет» + дано (если «Сократ».«человек» то «Сократ».«смертен» иначе да) + дано «Платон».«человек» + утверждаем «Платон».«смертен» + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record new file mode 100644 index 000000000..6b6d50d7d --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang +строк 18 +знаков 510 +отпечаток 544359786 38607868 +ядро 2 +утверждений 1 +отпечаток256 718bac3e5da72d464ae901264d3b23e7a17c487f5c0d9a400f8589f6a914a67d + +утверждение «Платон смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + для всех «Платон» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Платон».«человек»⟩ строка 8 + вердикт доказано + теорема «Платон смертен» строка 11 + дано «Сократ» строка 12 + дано «Платон» строка 13 + допущение ⟨если «Сократ».«человек» то «Сократ».«смертен» иначе да⟩ строка 14 + допущение ⟨«Платон».«человек»⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang new file mode 100644 index 000000000..f7ca16c2c --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +объект «Предмет» + «человек»: признак + «смертен»: признак + +утверждение «Платон смертен» + для всех «Сократ»: «Предмет» и «Платон»: «Предмет» таких что (если «Платон».«человек» то «Платон».«смертен» иначе да) и притом «Платон».«человек» + утверждаем «Платон».«смертен» + +следует «Платон смертен» + дано «Сократ»: «Предмет» + дано «Платон»: «Предмет» + дано (если «Платон».«человек» то «Платон».«смертен» иначе да) + дано «Платон».«человек» + утверждаем «Платон».«смертен» + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record new file mode 100644 index 000000000..7448a84dd --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang +строк 18 +знаков 510 +отпечаток 437455559 709052247 +ядро 2 +утверждений 1 +отпечаток256 ec47c9c2170cb1d646ce2bdd892946d1e2de5d481eeae5a354779a4378a900aa + +утверждение «Платон смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + для всех «Платон» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Платон».«человек» то «Платон».«смертен» иначе да ) и притом «Платон».«человек»⟩ строка 8 + вердикт доказано + теорема «Платон смертен» строка 11 + дано «Сократ» строка 12 + дано «Платон» строка 13 + допущение ⟨если «Платон».«человек» то «Платон».«смертен» иначе да⟩ строка 14 + допущение ⟨«Платон».«человек»⟩ строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record b/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record new file mode 100644 index 000000000..a1571512d --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record @@ -0,0 +1,22 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-statement.flang +строк 15 +знаков 371 +отпечаток 110395995 20177584 +ядро 2 +утверждений 1 +отпечаток256 3168b04a79c3b6c6d3f4606be3ca8a90411bc054d938e89da97d9ded4cc5909b + +утверждение «Сократ смертен» строка 7 + вид statement + для всех «Сократ» ⟨«Предмет»⟩ строка 8 + таких что ⟨( если «Сократ».«человек» то «Сократ».«смертен» иначе да ) и притом «Сократ».«человек»⟩ строка 8 + вердикт доказано + теорема «Сократ смертен» строка 11 + дано «Сократ» строка 12 + цель строка 13 + шаг 1 строка 14 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang new file mode 100644 index 000000000..0977d34fc --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang @@ -0,0 +1,20 @@ +модуль «Reasoning» + +объект «Предмет» + «рыба»: признак + «кит»: признак + «дышит жабрами»: признак + +утверждение «ни один кит не рыба» + для всех «всякий»: «Предмет» таких что (если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да) и притом (если «всякий».«кит» то (не «всякий».«дышит жабрами») иначе да) и притом «всякий».«кит» + утверждаем нет + +следует «ни один кит не рыба» + дано «всякий»: «Предмет» + дано (если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да) + дано (если «всякий».«кит» то (не «всякий».«дышит жабрами») иначе да) + дано «всякий».«кит» + утверждаем нет + затем «всякий».«дышит жабрами» по предположению + затем (не «всякий».«дышит жабрами») по предположению + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record new file mode 100644 index 000000000..cf787d6d6 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang +строк 21 +знаков 708 +отпечаток 861696332 871310597 +ядро 2 +утверждений 1 +отпечаток256 0a466dbdd5ce96a786c5b2609fada98d827810335cba8687ed81ae077194a96c + +утверждение «ни один кит не рыба» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да ) и притом ( если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да ) и притом «всякий».«кит»⟩ строка 9 + вердикт доказано + теорема «ни один кит не рыба» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«рыба» то «всякий».«дышит жабрами» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кит» то ( не «всякий».«дышит жабрами» ) иначе да⟩ строка 15 + допущение ⟨«всякий».«кит»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 промежуточный по предположению правило «цель есть допущение» + шаг 2 строка 19 промежуточный по предположению правило «цель есть допущение» + шаг 3 строка 20 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record b/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record new file mode 100644 index 000000000..1cd462a32 --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/probes/syllogism/assumptions/programs/undistributed-middle.flang +строк 19 +знаков 606 +отпечаток 830748764 757639856 +ядро 2 +утверждений 1 +отпечаток256 6d705a4cf463d5a16fda5e7956e82a0f006d428aae393f6828118b34ec2ac21f + +утверждение «все кошки — люди» строка 8 + вид statement + для всех «всякий» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «всякий».«человек» то «всякий».«смертен» иначе да ) и притом ( если «всякий».«кошка» то «всякий».«смертен» иначе да ) и притом «всякий».«кошка»⟩ строка 9 + вердикт доказано + теорема «все кошки — люди» строка 12 + дано «всякий» строка 13 + допущение ⟨если «всякий».«человек» то «всякий».«смертен» иначе да⟩ строка 14 + допущение ⟨если «всякий».«кошка» то «всякий».«смертен» иначе да⟩ строка 15 + допущение ⟨«всякий».«кошка»⟩ строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по предположению допущение 1 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang b/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang new file mode 100644 index 000000000..21ac9737b --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang @@ -0,0 +1,19 @@ +модуль «Reasoning» + +объект «Предмет» + «кролик»: признак + «питомец»: признак + «мохнат»: признак + +утверждение «некоторые питомцы мохнаты» + для всех «предмет посылки 2»: «Предмет» и «другой»: «Предмет» таких что (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «предмет посылки 2», что (некий.«питомец» и притом некий.«мохнат») + +следует «некоторые питомцы мохнаты» + дано «предмет посылки 2»: «Предмет» + дано «другой»: «Предмет» + дано (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) + дано «предмет посылки 2».«питомец» + дано «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record b/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record new file mode 100644 index 000000000..7ab68fbdc --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record @@ -0,0 +1,29 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang +строк 20 +знаков 848 +отпечаток 541359540 226813889 +ядро 2 +утверждений 1 +отпечаток256 edd60e73406f107b8e73c1c349b55882028b3ca5099e170a8abc837ade33d405 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + для всех «другой» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«предмет посылки 2»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + дано «другой» строка 14 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 15 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 16 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang new file mode 100644 index 000000000..75ef54b8e --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang @@ -0,0 +1,19 @@ +модуль «Reasoning» + +объект «Предмет» + «кролик»: признак + «питомец»: признак + «мохнат»: признак + +утверждение «некоторые питомцы мохнаты» + для всех «предмет посылки 2»: «Предмет» и «другой»: «Предмет» таких что (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + +следует «некоторые питомцы мохнаты» + дано «предмет посылки 2»: «Предмет» + дано «другой»: «Предмет» + дано (если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да) + дано «предмет посылки 2».«питомец» + дано «предмет посылки 2».«кролик» + утверждаем есть такой некий, а именно «другой», что (некий.«питомец» и притом некий.«мохнат») + по предположению diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record new file mode 100644 index 000000000..d0599944e --- /dev/null +++ b/flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record @@ -0,0 +1,29 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang +строк 20 +знаков 837 +отпечаток 823082656 240630876 +ядро 2 +утверждений 1 +отпечаток256 7d08c713aa53050e9bc4bd7ee467aef3d74b2679ccc42fff18b4e51839986566 + +утверждение «некоторые питомцы мохнаты» строка 8 + вид statement + для всех «предмет посылки 2» ⟨«Предмет»⟩ строка 9 + для всех «другой» ⟨«Предмет»⟩ строка 9 + таких что ⟨( если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да ) и притом «предмет посылки 2».«питомец» и притом «предмет посылки 2».«кролик»⟩ строка 9 + свидетель «некий» ⟨«другой»⟩ строка 10 + после подстановки ⟨некий.«питомец» и притом некий.«мохнат»⟩ + вердикт доказано + теорема «некоторые питомцы мохнаты» строка 12 + дано «предмет посылки 2» строка 13 + дано «другой» строка 14 + допущение ⟨если «предмет посылки 2».«кролик» то «предмет посылки 2».«мохнат» иначе да⟩ строка 15 + допущение ⟨«предмет посылки 2».«питомец»⟩ строка 16 + допущение ⟨«предмет посылки 2».«кролик»⟩ строка 17 + цель строка 18 + шаг 1 строка 19 закрывающий по предположению допущение 1 правило «разбор цели по условию» + следовательно доказано да +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 0d3b052b7..70bb05533 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -509,12 +509,32 @@ P ограничение: другое допущение flang/proof/checker/te P ограничение: гипотеза «дано н больше 0» без строки допущения flang/proof/checker/tests/families/restriction/k2b-direct-theorem-hypothesis.flang flang/proof/checker/tests/families/restriction/corrupt/hypothesis-without-assumption-line.record - - - - 1 допущение 16 - - say - - - - - - - - - - say ── семья «гипотеза»: гипотеза теоремы снята ограничением утверждения ── - - - - - - - - - - -C гипотеза: часть «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates.flang flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record - - - - 3 - - - +C гипотеза: часть «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates.flang flang/proof/checker/tests/families/hypothesis/statement-carries-the-hypothesis.record - - - - 0 - - - P гипотеза: у утверждения «таких что» нет flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang flang/proof/checker/tests/families/hypothesis/statement-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - C гипотеза: предусловие «требует» функции (честная) flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-carries-the-hypothesis.record - - - - 3 - - - P гипотеза: предусловие говорит о другом flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - C гипотеза: «не меньше 0» из объявленного отрезка (честная) flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.record - - - - 3 - - - P гипотеза: «не меньше 0» о целом flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.record - - - - 1 не является допущением утверждения - - +say ── вывод из посылок утверждения: шаг «по предположению» проигрывается из «таких что» ── - - - - - - - - - - +C посылки: только в «таких что» утверждения (честная) flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-statement.flang flang/proof/checker/tests/families/assumption-replay/premises-only-in-the-statement.record - - - - 0 - - - +C посылки: Barbara, промежуточный шаг модусом поненсом (честная) flang/proof/probes/syllogism/assumptions/programs/barbara.flang flang/proof/checker/tests/families/assumption-replay/barbara.record - - - - 0 - - - +C посылки: Celarent, поненс к отрицанию (честная) flang/proof/probes/syllogism/assumptions/programs/celarent.flang flang/proof/checker/tests/families/assumption-replay/celarent.record - - - - 0 - - - +C посылки: Darii, цель-конъюнкция (честная) flang/proof/probes/syllogism/assumptions/programs/darii.flang flang/proof/checker/tests/families/assumption-replay/darii.record - - - - 0 - - - +C посылки: Ferio, конъюнкция с отрицанием (честная) flang/proof/probes/syllogism/assumptions/programs/ferio.flang flang/proof/checker/tests/families/assumption-replay/ferio.record - - - - 0 - - - +C посылки: охрана о названном предмете из двух (честная) flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.record - - - - 0 - - - +C посылки: свидетель «есть такой … а именно» (честная) flang/proof/probes/syllogism/assumptions/programs/darii-with-the-existence-word.flang flang/proof/checker/tests/families/assumption-replay/darii-with-the-existence-word.record - - - - 0 - - - +C посылки: Camestres опровержением, цель «нет» (честная) flang/proof/probes/syllogism/assumptions/programs/camestres-by-refutation.flang flang/proof/checker/tests/families/assumption-replay/camestres-by-refutation.record - - - - 0 - - - +P посылки: подтверждение следствия flang/proof/probes/syllogism/assumptions/programs/affirming-the-consequent.flang flang/proof/checker/tests/families/assumption-replay/affirming-the-consequent.record - - - - 1 из посылок утверждения не следует - - +P посылки: нераспределённый средний flang/proof/probes/syllogism/assumptions/programs/undistributed-middle.flang flang/proof/checker/tests/families/assumption-replay/undistributed-middle.record - - - - 1 из посылок утверждения не следует - - +P посылки: незаконное обращение flang/proof/probes/syllogism/assumptions/programs/illicit-conversion.flang flang/proof/checker/tests/families/assumption-replay/illicit-conversion.record - - - - 1 из посылок утверждения не следует - - +P посылки: отрицание антецедента flang/proof/probes/syllogism/assumptions/programs/denying-the-antecedent.flang flang/proof/checker/tests/families/assumption-replay/denying-the-antecedent.record - - - - 1 из посылок утверждения не следует - - +P посылки: экзистенциальный импорт flang/proof/probes/syllogism/assumptions/programs/existential-import.flang flang/proof/checker/tests/families/assumption-replay/existential-import.record - - - - 1 из посылок утверждения не следует - - +P посылки: охрана о другом предмете flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record - - - - 1 из посылок утверждения не следует - - +P посылки: свидетель, о котором посылок нет flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record - - - - 1 из посылок утверждения не следует - - +P посылки: у теоремы другой свидетель, чем у утверждения flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record - - - - 1 доказывается не то, что обещано - - +P посылки: опровержение без малой посылки flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record - - - - 1 из посылок утверждения не следует - - +P посылки: допущение записи подменено другой посылкой flang/proof/probes/syllogism/assumptions/programs/barbara.flang flang/proof/checker/tests/families/assumption-replay/barbara.record - s/допущение ⟨«всякий».«грек»⟩/допущение ⟨«всякий».«человек»⟩/ - - 1 допущение 3 - - +P посылки: два звена поненса одним шагом — третий исход, не приёмка flang/proof/probes/syllogism/assumptions/programs/barbara-without-the-middle-step.flang flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record - - - - 3 - - - say - - - - - - - - - - say ── семья «утверждение» (ADR-0026 К3a): утверждение без функции ── - - - - - - - - - - C утверждение: связывание и теорема по индукции (честная, проиграна целиком — К3b) flang/proof/checker/tests/families/statement/f05k-statement.flang flang/proof/checker/tests/families/statement/f05k-statement.record - - - - 0 - - - diff --git a/flang/proof/probes/syllogism/assumptions/expected.tsv b/flang/proof/probes/syllogism/assumptions/expected.tsv index 7b26e0bd2..ce3490882 100644 --- a/flang/proof/probes/syllogism/assumptions/expected.tsv +++ b/flang/proof/probes/syllogism/assumptions/expected.tsv @@ -1,16 +1,16 @@ program judge code word socrates.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +socrates.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником barbara.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -barbara.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +barbara.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником celarent.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -celarent.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +celarent.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником darii.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -darii.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +darii.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником ferio.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -ferio.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +ferio.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником camestres-by-refutation.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -camestres-by-refutation.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +camestres-by-refutation.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-without-a-theorem.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 socrates-without-a-theorem.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику socrates-with-predicates-as-functions.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 @@ -23,8 +23,8 @@ illicit-conversion.flang kernel 1 цель не выведена из допущ existential-import.flang kernel 1 цель не выведена из допущений теоремы denying-the-antecedent.flang kernel 1 цель не выведена из допущений теоремы darii-with-the-existence-word.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -darii-with-the-existence-word.flang checker 1 доказывается не то, что обещано +darii-with-the-existence-word.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-with-premises-only-in-the-statement.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates-with-premises-only-in-the-statement.flang checker 1 а допущений в записи 0 +socrates-with-premises-only-in-the-statement.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-with-premises-only-in-the-theorem.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 -socrates-with-premises-only-in-the-theorem.flang checker 3 НЕ ПРОВЕРЕНО — запись не противоречит исходнику +socrates-with-premises-only-in-the-theorem.flang checker 1 не является допущением утверждения diff --git a/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang b/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang new file mode 100644 index 000000000..ffa868935 --- /dev/null +++ b/flang/proof/probes/syllogism/assumptions/programs/postcondition-with-a-hypothesis-only-in-the-theorem.flang @@ -0,0 +1,17 @@ +модуль «Reasoning» + +тотальная функция «Тождество» + принимает н: неотрицательное + возвращает неотрицательное + обеспечивает «результат положителен» результат больше 0 + пример «Единица остаётся единицей» + дано н равно 1 + ожидается 1 + н + +теорема «результат положителен» + дано н: неотрицательное + дано н больше 0 + утверждаем результат больше 0 + по предположению + следовательно доказано From d5a64dc259e8235f85b159aa7895e5f7d0d5f016 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 20:10:39 +0000 Subject: [PATCH 04/11] docs: follow prose numbers and the inventory to the tree The checker grew by 103 lines and the tree by five flang probe files; the prose numbers and the inventory cell that count them are retaken. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- .github/workflows/binary.yml | 4 ++-- docs/flang/self/SPEC.md | 2 +- docs/site/sitemap.mjs | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index 5d5426243..49e39d19e 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -693,9 +693,9 @@ jobs: # Шаги «Run kernel examples» и «Run stdlib examples» выше зовут `flang test` # на двух # каталогах, и `flang/self/` среди них нет. Каталог при этом не пустой: 64 - # файл и 5186 примеров, объявленных внутри функций. + # файл и 5185 примеров, объявленных внутри функций. # СНЯТО 2026-09-17 файлов flang/self/*.flang = 64 - # СНЯТО 2026-09-17 примеров-в flang/self/*.flang = 5186 + # СНЯТО 2026-09-17 примеров-в flang/self/*.flang = 5185 # # Единственная работа, которая до них добралась бы, — `korpus` ниже # (`flang test . --ledger` внутри `обход-примеров.sh`). Она закрыта условием diff --git a/docs/flang/self/SPEC.md b/docs/flang/self/SPEC.md index 63fe85a05..34a12da10 100644 --- a/docs/flang/self/SPEC.md +++ b/docs/flang/self/SPEC.md @@ -14,7 +14,7 @@ JavaScript снята 20 августа 2026 (коммит `fe8e8a37`), и св ## Состав каталога 64 файла `.flang`, - 139 820 строк + 139 780 строк Имя модуля — первая строка файла; здесь оно повторено, чтобы читать `использует «…»` в других файлах без поиска. diff --git a/docs/site/sitemap.mjs b/docs/site/sitemap.mjs index 01c8ef500..66eeeb1f3 100644 --- a/docs/site/sitemap.mjs +++ b/docs/site/sitemap.mjs @@ -270,8 +270,8 @@ export const РАЗДЕЛЫ = [ страницы: [ /* СПЕЦИФИКАЦИЯ ЯДРА ПЕРЕЕХАЛА СЮДА ИЗ РАЗДЕЛА «ДОКАЗАТЕЛЬСТВА», где стояла третьим пунктом — на дорожке читателя. Жанр у неё тот же, что у трёх - соседей по этому разделу: контракт на 4829 строк, где рядом с правилом - СНЯТО 2026-09-17 строк docs/flang/proof/SPEC.md = 4829 + соседей по этому разделу: контракт на 4821 строк, где рядом с правилом + СНЯТО 2026-09-17 строк docs/flang/proof/SPEC.md = 4821 ядра стоят пути к файлам реализации, имена проверок и разбор отвергнутых редакций. Читателю на тот же вопрос отвечают «Что доказано, а что нет» и «Зачем и как». Адрес не сменился. */ From 5ff1af226b11e7da59e750e000be6883025eac19 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 20:12:11 +0000 Subject: [PATCH 05/11] fix(checker): name two assumption-replay probes in listed words The refutation and witness forgeries carried words outside the file-name word list; they are renamed and their records rewritten for the new paths. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- ...mise.flang => refutation-without-the-second-premise.flang} | 0 ...se.record => refutation-without-the-second-premise.record} | 2 +- ...ement.flang => witness-is-not-the-statement-witness.flang} | 0 ...ent.record => witness-is-not-the-statement-witness.record} | 2 +- flang/proof/checker/tests/probes.tsv | 4 ++-- 5 files changed, 4 insertions(+), 4 deletions(-) rename flang/proof/checker/tests/families/assumption-replay/{refutation-without-the-minor-premise.flang => refutation-without-the-second-premise.flang} (100%) rename flang/proof/checker/tests/families/assumption-replay/{refutation-without-the-minor-premise.record => refutation-without-the-second-premise.record} (97%) rename flang/proof/checker/tests/families/assumption-replay/{witness-differs-from-the-statement.flang => witness-is-not-the-statement-witness.flang} (100%) rename flang/proof/checker/tests/families/assumption-replay/{witness-differs-from-the-statement.record => witness-is-not-the-statement-witness.record} (97%) diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang similarity index 100% rename from flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang rename to flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang diff --git a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record similarity index 97% rename from flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record rename to flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record index cf787d6d6..9e5774453 100644 --- a/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record +++ b/flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record @@ -1,5 +1,5 @@ запись доказательства 1 -исходник flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang +исходник flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang строк 21 знаков 708 отпечаток 861696332 871310597 diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang similarity index 100% rename from flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang rename to flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang diff --git a/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record similarity index 97% rename from flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record rename to flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record index 7ab68fbdc..01c232b30 100644 --- a/flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record +++ b/flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record @@ -1,5 +1,5 @@ запись доказательства 1 -исходник flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang +исходник flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang строк 20 знаков 848 отпечаток 541359540 226813889 diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 70bb05533..8bd0fc4f4 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -531,8 +531,8 @@ P посылки: отрицание антецедента flang/proof/probes/s P посылки: экзистенциальный импорт flang/proof/probes/syllogism/assumptions/programs/existential-import.flang flang/proof/checker/tests/families/assumption-replay/existential-import.record - - - - 1 из посылок утверждения не следует - - P посылки: охрана о другом предмете flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.record - - - - 1 из посылок утверждения не следует - - P посылки: свидетель, о котором посылок нет flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang flang/proof/checker/tests/families/assumption-replay/witness-without-premises.record - - - - 1 из посылок утверждения не следует - - -P посылки: у теоремы другой свидетель, чем у утверждения flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.flang flang/proof/checker/tests/families/assumption-replay/witness-differs-from-the-statement.record - - - - 1 доказывается не то, что обещано - - -P посылки: опровержение без малой посылки flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.flang flang/proof/checker/tests/families/assumption-replay/refutation-without-the-minor-premise.record - - - - 1 из посылок утверждения не следует - - +P посылки: у теоремы другой свидетель, чем у утверждения flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.record - - - - 1 доказывается не то, что обещано - - +P посылки: опровержение без малой посылки flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.record - - - - 1 из посылок утверждения не следует - - P посылки: допущение записи подменено другой посылкой flang/proof/probes/syllogism/assumptions/programs/barbara.flang flang/proof/checker/tests/families/assumption-replay/barbara.record - s/допущение ⟨«всякий».«грек»⟩/допущение ⟨«всякий».«человек»⟩/ - - 1 допущение 3 - - P посылки: два звена поненса одним шагом — третий исход, не приёмка flang/proof/probes/syllogism/assumptions/programs/barbara-without-the-middle-step.flang flang/proof/checker/tests/families/assumption-replay/barbara-without-the-middle-step.record - - - - 3 - - - say - - - - - - - - - - From 670acf3fba4ad56a23d958fbc950b57e9f4cd24a Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 20:13:28 +0000 Subject: [PATCH 06/11] docs(ledger): count the assumption-replay probe programs Five new probe programs carry one obligation each; the proved-share ledger names them with the kernel's verdict: one proved, four refused. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- scripts/ledgers/proved-share-ledger.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index c88a6b2ae..2c4fefca2 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1189,6 +1189,11 @@ bc17b199769f3c2a966e71d18ebcee89|1|×|×|×|0|flang/proof/checker/tests/families 2c28f2fe75e00f19601f9f6cf9f8d835|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/precondition-does-not-carry-the-hypothesis.flang ad3459ff6037a5f4fd987dad04cdcb69|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-carries-the-hypothesis.flang d645f02d887cf92fdffc69f02adc2e82|1|×|×|×|0|flang/proof/checker/tests/families/hypothesis/type-does-not-carry-the-hypothesis.flang +de163bbb2705bdc26ea11008727e938e|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/premise-about-another-object.flang +08921be621f8063b40b5d008e7b9cc08|1|1|0|0|0|flang/proof/checker/tests/families/assumption-replay/premise-about-the-same-object.flang +0778794de6b21c38a64ab3059d3d4a6b|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/refutation-without-the-second-premise.flang +2458efdedb09ab492f1fa9dd4f464080|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/witness-is-not-the-statement-witness.flang +5bbe66b669213e9529c7b2d537397100|1|0|0|0|0|flang/proof/checker/tests/families/assumption-replay/witness-without-premises.flang 48fabdcaa9d040986fe87d584786ff9b|1|0|0|0|1|flang/proof/checker/tests/families/plan/temporary-directory.flang 58695c0261bca20c054c8f8e7fade6c3|1|0|0|0|1|flang/proof/checker/tests/families/plan/corrupt/foreign-order.flang 441a75abee9f78ef507959ee1b7155a8|1|×|×|×|1|flang/proof/checker/tests/families/coverage/o9-fold-start-one.flang From 8e20a15059d7dfa86c16bf03d5dce083a426e227 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 21:30:45 +0000 Subject: [PATCH 07/11] fix(checker): keep the theorem line apart from the step kinds GCC on the CI runner refused the build with -Werror=string-compare: the conditional handed the theorem literal to a comparison with the proved-step literal. The theorem line now takes its own branch; behaviour is unchanged and the probe set gives the same answers. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- flang/proof/checker/checker.c | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index ca9a1897d..c9a78f75f 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -620,9 +620,12 @@ static Сп разметка_теоремы(Сп строки, long начало if (начинается(s, "//") || !*s) continue; if (утв && strspn(сырая, " ") > утв) continue; утв = 0; - вид = начинается(s, "теорема ") || (i == начало && следует) ? "теорема" : вид_строки_теоремы(s); - if (strcmp(вид, "утверждаем") == 0) утв = strspn(сырая, " "); - if (!*вид || (следует && strcmp(вид, "доказано") == 0)) continue; + if (начинается(s, "теорема ") || (i == начало && следует)) вид = "теорема"; + else { + вид = вид_строки_теоремы(s); + if (strcmp(вид, "утверждаем") == 0) утв = strspn(сырая, " "); + if (!*вид || (следует && strcmp(вид, "доказано") == 0)) continue; + } /* К5: `дано <утверждение>` — допущение, а не имя; `дано х: T таких что P` — имя и допущение на одной строке. Допущение запись печатает своей строкой. */ if (strcmp(вид, "дано") == 0 && (!содержит(s, ":") || содержит(s, " таких что "))) { From 0b0c6dfe01f0fe83af9c0b439d4dbbb85f88d28a Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 23:25:28 +0000 Subject: [PATCH 08/11] chore(numbers): raise checker ratchets after the rebase The two checker branches together give 7952 code lines in checker.c, 613 forged probes (0 accepted) and 297 honest ones (0 refused); the forgery catalogue catches 38 of 38. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- docs/four-coverages.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/four-coverages.md b/docs/four-coverages.md index 802ca424e..f06b34448 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/` — по одной на программу-образец, всего 91. - +`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 93. + Снимается: `bootstrap/flang io flang/proof/replay-share.fscript`. **Что это даёт сказать.** Что у этого набора записей слово «доказано» в отчёте компилятора не From 82f164e8823f5b68caa15f786115e7e3177ab60c Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Fri, 2 Oct 2026 00:22:49 +0000 Subject: [PATCH 09/11] chore(numbers): raise checker ratchets after the rebase onto fmath Together with the merged checker work, checker.c holds 8086 code lines; 628 forged probes are all refused and 310 honest ones accepted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- ...n-exact-integer-is-a-new-kind-of-value-not-a-new-name.md | 2 +- docs/design/nositel-tochnogo-celogo.md | 2 +- docs/site/index.md | 2 +- docs/site/index.ru.md | 2 +- docs/site/proofs.md | 2 +- docs/site/proofs.ru.md | 2 +- flang/proof/ratchets.txt | 6 +++--- 7 files changed, 9 insertions(+), 9 deletions(-) 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 40485c82b..3bc5d8412 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`, - 10257 строк. + 10395 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index 5f2278674..eaba62348 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` (10257 строк) +3. **Цену для проверяющей программы.** `checker.c` (10395 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/docs/site/index.md b/docs/site/index.md index c5c545306..60f30f629 100644 --- a/docs/site/index.md +++ b/docs/site/index.md @@ -143,7 +143,7 @@ recounted on every push by `sh scripts/guards/published-vs-tree.sh --числа` steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then … by property …), `индукция по …` (induction on …), `следовательно доказано` (hence proved). It reads like a proof in Isabelle's Isar, not like a script of -tactics. There are **303** such theorems in the repository, 55 of them in the +tactics. There are **308** such theorems in the repository, 55 of them in the standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`, summed with `awk`). diff --git a/docs/site/index.ru.md b/docs/site/index.ru.md index 6ac1ea0df..b549a62b1 100644 --- a/docs/site/index.ru.md +++ b/docs/site/index.ru.md @@ -141,7 +141,7 @@ bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 **Доказательство руками можно писать и здесь.** `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как доказательство на Isar из Isabelle, а -не как скрипт из тактик. Таких теорем в дереве языка **303**, из них **55** в +не как скрипт из тактик. Таких теорем в дереве языка **308**, из них **55** в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`, сумма по `awk`). diff --git a/docs/site/proofs.md b/docs/site/proofs.md index c23f62138..c6cd42072 100644 --- a/docs/site/proofs.md +++ b/docs/site/proofs.md @@ -66,7 +66,7 @@ proof by hand**, as in Coq or Isabelle. A `теорема` (theorem) is written steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then … by property …), `индукция по …` (induction on …), `следовательно доказано` (hence proved). It reads like Isar in Isabelle, and the prover checks each step; -it searches for nothing. There are 303 such theorems in the repository, 55 of +it searches for nothing. There are 308 such theorems in the repository, 55 of them in the standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Most postconditions need no theorem: the proof report shows, as a separate number, how many were proved **without a written proof**. diff --git a/docs/site/proofs.ru.md b/docs/site/proofs.ru.md index f57021269..dd9e0e196 100644 --- a/docs/site/proofs.ru.md +++ b/docs/site/proofs.ru.md @@ -64,7 +64,7 @@ руками**, как в Coq или Isabelle. `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как Isar в Isabelle, и prover проверяет каждый шаг, -ничего не ища. В дереве языка таких теорем 303, из них 55 в стандартной +ничего не ища. В дереве языка таких теорем 308, из них 55 в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Большинству постусловий теорема не нужна: отчёт о доказательствах показывает отдельным числом, сколько доказано **без написанного доказательства**. diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index c8441a3e8..319467dad 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,7 +1,7 @@ -forgeries 36 +forgeries 38 forgery-numerator 155 -forgery-probes 611 -checker-code-lines 7949 +forgery-probes 628 +checker-code-lines 8086 checker-primitives 15 trap-kinds 38 trap-goals-on-kernel-word 3 From 98ca5fb835052ab1533c747bac6ec7aa9003344c Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Fri, 2 Oct 2026 01:17:09 +0000 Subject: [PATCH 10/11] test(probes): expect the checker to refuse the theorem-only hypothesis The program came with the checker work, its row did not. The kernel row joins after the print that carries the kernel fix. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- flang/proof/probes/syllogism/assumptions/expected.tsv | 1 + 1 file changed, 1 insertion(+) diff --git a/flang/proof/probes/syllogism/assumptions/expected.tsv b/flang/proof/probes/syllogism/assumptions/expected.tsv index ce3490882..a7c44c51e 100644 --- a/flang/proof/probes/syllogism/assumptions/expected.tsv +++ b/flang/proof/probes/syllogism/assumptions/expected.tsv @@ -28,3 +28,4 @@ socrates-with-premises-only-in-the-statement.flang kernel 0 ДОКАЗАНО — socrates-with-premises-only-in-the-statement.flang checker 0 ПРОВЕРЕНО — запись сошлась с исходником socrates-with-premises-only-in-the-theorem.flang kernel 0 ДОКАЗАНО — утверждений 1: доказано 1 socrates-with-premises-only-in-the-theorem.flang checker 1 не является допущением утверждения +postcondition-with-a-hypothesis-only-in-the-theorem.flang checker 1 не является допущением утверждения From 1a49b787936396b0103eb4962a32d00555b3399d Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Fri, 2 Oct 2026 02:31:46 +0000 Subject: [PATCH 11/11] chore(numbers): sync measured counts after rebase Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- .github/workflows/ci.yml | 4 ++-- docs/course/README.md | 2 +- docs/tree-inventory.md | 2 +- flang/scripts/count-guard.mjs | 4 ++-- flang/scripts/name-guard.mjs | 4 ++-- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 45d02dbaf..7b2c6af1f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -164,8 +164,8 @@ permissions: jobs: # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c` - # планом на flang — 1087 файл; разбор в задаче 5821. - # СНЯТО 2026-10-02 файлов *.flang = 1087 + # планом на flang — 1097 файл; разбор в задаче 5821. + # СНЯТО 2026-10-02 файлов *.flang = 1097 # # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в diff --git a/docs/course/README.md b/docs/course/README.md index 7e9abca61..bcca865cf 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 файлов и 32 526 строки библиотеки | `ls flang/stdlib/*.flang`, `cat … \| wc -l` | -| 726 заметки, 242 примеров, 413 файл доказательств | `ls`, `find` | +| 726 заметки, 242 примеров, 423 файл доказательств | `ls`, `find` | | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа | **Чего переснять не удалось, и это надо знать.** diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 679bfae6d..06f54620b 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -77,7 +77,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| | оболочка | 58 | 10 079 | 52 | 5 629 | -| C | 37 | 871 301 | 0 | 0 | +| C | 37 | 871 439 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | | HTML | 7 | 1 263 | 0 | 0 | diff --git a/flang/scripts/count-guard.mjs b/flang/scripts/count-guard.mjs index eea378f79..aab358cbb 100644 --- a/flang/scripts/count-guard.mjs +++ b/flang/scripts/count-guard.mjs @@ -43,8 +43,8 @@ * * • ЧИСЛО ФАЙЛОВ он не сверяет. «AST всех 60 файлов `.flang` репозитория * напечатан до и после правки» — не утверждение о размере дерева, а запись о - * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1087 файла, но - * СНЯТО 2026-10-02 файлов *.flang = 1087 + * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1097 файла, но + * СНЯТО 2026-10-02 файлов *.flang = 1097 * прогон-то был на шестидесяти, и подставить туда 168 значило бы соврать про * работу, которой не делали. Отличить «столько в дереве» от «столько прошло * через прогон» нечем, кроме чтения, — значит сторож сюда не лезет. diff --git a/flang/scripts/name-guard.mjs b/flang/scripts/name-guard.mjs index 5fe01c06c..faea2fbd3 100644 --- a/flang/scripts/name-guard.mjs +++ b/flang/scripts/name-guard.mjs @@ -130,8 +130,8 @@ * переставшая сравнивать, продолжает зеленеть. * * Поэтому охват ПЕЧАТАЕТСЯ каждым прогоном и закреплён тестом «охват сторожа - * назван числом»: 300 файлов из 1087. Остальные 1099 — не упущение: - * СНЯТО 2026-10-02 файлов *.flang = 1087 + * назван числом»: 300 файлов из 1097. Остальные 1099 — не упущение: + * СНЯТО 2026-10-02 файлов *.flang = 1097 * * • 503 — печать замеров (`docs/benchmark*`): * это ВЫВОД прогона, а не исходник, и правилам имени он не подчиняется;