From 3824e3e4a6f0ad12ecea141cc3422485c890f135 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 13:11:38 +0000 Subject: [PATCH 1/7] fix(checker): replay what the kernel proves in user programs On a set of 14 short user programs the kernel proves 28 places and the checker replayed 13; now it replays 26. Seven readings, all rules already in the ledger or evaluator equations: a goal closed by the checked promise of a called function, a result field of a written record, the any-case branch, a closed statement, the run line under a closed statement, N11, N7 with a length step, N3 for declared floors, a lower bound above zero. Adds the user-program probe plan with a CI step and 27 checker probes. Code lines 7711 -> 7788, ceiling raised by exactly that. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/binary.yml | 5 + ...r-is-a-new-kind-of-value-not-a-new-name.md | 2 +- docs/design/nositel-tochnogo-celogo.md | 2 +- flang/proof/checker/checker.c | 108 ++++++++-- .../user-program/callee-argument.flang | 13 ++ .../user-program/callee-argument.record | 39 ++++ .../user-program/callee-precondition.flang | 15 ++ .../user-program/callee-precondition.record | 48 +++++ .../user-program/callee-promise.flang | 16 ++ .../user-program/callee-promise.record | 36 ++++ .../tests/families/user-program/maybe.record | 44 ++++ .../tests/families/user-program/point.record | 42 ++++ .../tests/families/user-program/shapes.record | 49 +++++ .../user-program/shopping-cart.record | 44 ++++ .../families/user-program/socrates.record | 54 +++++ .../tests/families/user-program/tree.record | 35 ++++ .../families/user-program/word-lengths.record | 45 +++++ flang/proof/checker/tests/probes.tsv | 28 +++ .../user-programs/programs/account.flang | 21 ++ .../user-programs/programs/counter.flang | 29 +++ .../user-programs/programs/discount.flang | 21 ++ .../probes/user-programs/programs/door.flang | 32 +++ .../user-programs/programs/greeting.flang | 15 ++ .../probes/user-programs/programs/maybe.flang | 36 ++++ .../probes/user-programs/programs/point.flang | 20 ++ .../user-programs/programs/positives.flang | 20 ++ .../user-programs/programs/shapes.flang | 32 +++ .../programs/shopping-cart.flang | 26 +++ .../user-programs/programs/socrates.flang | 25 +++ .../user-programs/programs/statements.flang | 12 ++ .../probes/user-programs/programs/tree.flang | 31 +++ .../user-programs/programs/word-lengths.flang | 19 ++ flang/proof/probes/user-programs/run.fscript | 191 ++++++++++++++++++ flang/proof/ratchets.txt | 2 +- 34 files changed, 1140 insertions(+), 17 deletions(-) create mode 100644 flang/proof/checker/tests/families/user-program/callee-argument.flang create mode 100644 flang/proof/checker/tests/families/user-program/callee-argument.record create mode 100644 flang/proof/checker/tests/families/user-program/callee-precondition.flang create mode 100644 flang/proof/checker/tests/families/user-program/callee-precondition.record create mode 100644 flang/proof/checker/tests/families/user-program/callee-promise.flang create mode 100644 flang/proof/checker/tests/families/user-program/callee-promise.record create mode 100644 flang/proof/checker/tests/families/user-program/maybe.record create mode 100644 flang/proof/checker/tests/families/user-program/point.record create mode 100644 flang/proof/checker/tests/families/user-program/shapes.record create mode 100644 flang/proof/checker/tests/families/user-program/shopping-cart.record create mode 100644 flang/proof/checker/tests/families/user-program/socrates.record create mode 100644 flang/proof/checker/tests/families/user-program/tree.record create mode 100644 flang/proof/checker/tests/families/user-program/word-lengths.record create mode 100644 flang/proof/probes/user-programs/programs/account.flang create mode 100644 flang/proof/probes/user-programs/programs/counter.flang create mode 100644 flang/proof/probes/user-programs/programs/discount.flang create mode 100644 flang/proof/probes/user-programs/programs/door.flang create mode 100644 flang/proof/probes/user-programs/programs/greeting.flang create mode 100644 flang/proof/probes/user-programs/programs/maybe.flang create mode 100644 flang/proof/probes/user-programs/programs/point.flang create mode 100644 flang/proof/probes/user-programs/programs/positives.flang create mode 100644 flang/proof/probes/user-programs/programs/shapes.flang create mode 100644 flang/proof/probes/user-programs/programs/shopping-cart.flang create mode 100644 flang/proof/probes/user-programs/programs/socrates.flang create mode 100644 flang/proof/probes/user-programs/programs/statements.flang create mode 100644 flang/proof/probes/user-programs/programs/tree.flang create mode 100644 flang/proof/probes/user-programs/programs/word-lengths.flang create mode 100644 flang/proof/probes/user-programs/run.fscript diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index caed090c7..e11a91ce0 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -1783,6 +1783,11 @@ jobs: LC_ALL: C.UTF-8 FLANG_BIN: ${{ github.workspace }}/bootstrap/flang + - name: Check user programs are replayed by the checker + run: cd flang/proof/probes/user-programs && ../../../../bootstrap/flang io run.fscript + env: + FLANG_TMP: ${{ runner.temp }} + # ── Дорогая половина: только тег и ручной запуск ────────────────────────── korpus: name: corpus-examples 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 dad868bbc..1a41db9bc 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`, - 10015 строк. + 10095 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index f5c339bef..3fbfef109 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` (10015 строк) +3. **Цену для проверяющей программы.** `checker.c` (10095 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index 27d3fd23c..84d8816c4 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -2606,16 +2606,17 @@ static long строка_разбора(Сп строки, long a, long b, char впереди, и без него, потому что язык пишет оба. Ветвь берётся только однострочная: склейка многострочной была бы догадкой об отступе. */ static char *ветвь_по_значению(Сп строки, long a, long b, Знач з) { - long i; + long i; int неясно = 0; for (i = a + 1; i < b; i++) { char *z = строка_по_номеру(строки, i), *обр; int совпал = 0; double ч; if (!начинается(z, "случай ")) continue; обр = хвост_после(z, "случай "); - if (з.вид == 7) + if (strcmp(обр, "любое") == 0) совпал = !неясно; + else if (з.вид == 7) совпал = strcmp(обр, з.s) == 0 || (начинается(з.s, "вариант «") && strcmp(обр, з.s + strlen("вариант ")) == 0); else if (з.вид == 2 && число_точно(обр, &ч)) совпал = (ч == з.ч); - if (!совпал) continue; + if (!совпал) { неясно |= з.вид == 2 ? !число_точно(обр, &ч) : (!*в_ёлочках(обр, 1) || !strcmp(в_ёлочках(обр, 1), в_ёлочках(з.s, 1))); continue; } if (i + 1 < b && начинается(строка_по_номеру(строки, i + 1), "то ")) return слова_после(строка_по_номеру(строки, i + 1), 1); return (char *)""; @@ -2658,7 +2659,7 @@ static int ветви_парами(Сп строки, long где, long b) { } static Знач ветвь_разбора(Сп строки, long где, long b, Знач с, int глубина) { Сп чл = с.вид == 4 ? члены_списка(с.s) : ПУСТО, ост = ПУСТО, им, тр, зим, зтр; - long i; int j, k, связано = 0, нужно = 0; Знач итог = НЕ_БЕРУСЬ; + long i; int j, k, связано = 0, нужно = 0, неясно = 0; Знач итог = НЕ_БЕРУСЬ; if (!ветви_парами(строки, где, b) || (с.вид == 4 && !чл.n && с.ч != 0)) return не_берусь_потому(ПР_РАЗБОР_ЗВЕНА); for (i = где + 1; i + 1 < b; i++) { char *обр = слова_после(строка_по_номеру(строки, i), 1), *то = слова_после(строка_по_номеру(строки, i + 1), 1); @@ -2674,8 +2675,9 @@ static Знач ветвь_разбора(Сп строки, long где, long b связано += связать_оба(сл.n == 5 ? сл.e[4] : "хвост", как_список(fmt("[%s]", соединить(ост, ",")), ост.n)); нужно = 4; } else { + if (strcmp(обр, "любое") == 0) return неясно ? НЕ_БЕРУСЬ : оценить_терм(то, строки, НЕ_БЕРУСЬ, глубина + 1); if (начинается(обр, "вариант ")) обр += strlen("вариант "); - if (strcmp(в_ёлочках(обр, 1), в_ёлочках(с.s, 1)) != 0) continue; + if (strcmp(в_ёлочках(обр, 1), в_ёлочках(с.s, 1)) != 0) { неясно |= !*в_ёлочках(обр, 1); continue; } if (strstr(обр, "» с ") && (!поля(обр, " как ", &им, &тр) || !поля(с.s, " равным ", &зим, &зтр))) return НЕ_БЕРУСЬ; for (j = 0; strstr(обр, "» с ") && j < им.n; j++, нужно += 2) { for (k = 0; k < зим.n && strcmp(зим.e[k], им.e[j]) != 0; k++) ; @@ -3396,10 +3398,22 @@ static int сверить_шаг_свойством(Сверка *s, const char static int неотрицательно_algebra(const char *т_сырой, const char *чья, Сп bound, Сп строки, int глубина, char **почему); +static char *тело_случая(Сп строки, long ци, long конец_блока); +static Сп bound_имена_случая(const char *хвост); +static Сп имена_доводов_функции(Сп строки, const char *функция); static int прямая_по_предположению(Сп строки, const char *чья) { - long a, b; char *тело, *почему = (char *)""; + long a, b, i; int n = 0; char *тело, *почему = (char *)""; a = блок_функции(строки, чья, &b); if (a < 1) return 0; + if (строка_разбора(строки, a, b, &тело) > 0) { + for (i = a + 1; i < b; i++) { + char *l = как_читает_язык(часть(строки, i)); Сп св = bound_имена_случая(слова_после(l, 1)); int k; + if (!начинается(l, "случай ")) continue; + for (k = 0, n++; k < св.n; k++) if (среди(имена_доводов_функции(строки, чья), св.e[k])) return 0; + if (!неотрицательно_algebra(тело_случая(строки, i, b), чья, ПУСТО, строки, 0, &почему)) return 0; + } + return n > 0; + } тело = тело_функции_текст(строки, a, b); return *тело && неотрицательно_algebra(тело, чья, ПУСТО, строки, 0, &почему); } @@ -3830,6 +3844,14 @@ static int развернуть_вызов(const char *t, const char *чья, С static int шаг_счёта(const char *ш, const char *акк, double предел); /* `глубина` — не от бесконечной рекурсии (терм строго мельчает, кроме одной развёртки, а её берут лишь у плоского тела), а порукой на всякий случай. */ +static int мера_простого(const char *т) { + char *u = без_внешних(т); + return начинается(u, "длина ") && простой(слова_после(u, 1)); +} +static int шаг_с_мерой(const char *ш, const char *акк) { + Разрез р = разрез_по(ужать(ш), "плюс"); + return р.есть && ((!strcmp(ужать(р.лево), акк) && мера_простого(р.право)) || (!strcmp(ужать(р.право), акк) && мера_простого(р.лево))); +} static int неотрицательно_algebra(const char *т_сырой, const char *чья, Сп bound, Сп строки, int глубина, char **почему) { char *t = ужать(т_сырой); double v; Разрез sum; char *u, *a, *b; int i, взялся; @@ -3883,7 +3905,7 @@ static int неотрицательно_algebra(const char *т_сырой, const Разрез нач = разрез_по(до_имён.лево, "начиная с"), имена = разрез_по(до_имён.право, "и"); char *акк = ужать(имена.лево), *эл = ужать(имена.право); if (до_шага.есть && до_имён.есть && нач.есть && имена.есть && *акк && *эл && !содержит(акк, " ") && - !содержит(эл, " ") && strcmp(акк, эл) != 0 && шаг_счёта(до_шага.право, акк, БЕЗ_ПРЕДЕЛА)) + !содержит(эл, " ") && strcmp(акк, эл) != 0 && (шаг_счёта(до_шага.право, акк, БЕЗ_ПРЕДЕЛА) || шаг_с_мерой(до_шага.право, акк))) return неотрицательно_algebra(нач.право, чья, bound, строки, глубина + 1, почему); *почему = fmt("свёртка «%s»: шаг не счёт по форме (Н7) — знак не держится", t); return 0; @@ -4067,7 +4089,7 @@ static int булево_правило(const char *пр) { /* ДОМЕН ЦЕЛИ УЗЛА algebra — по какому из пяти доводов узел будет проигран. Тождество, порядок и охрана решаются ДО булева и ВМЕСТО него: булево замыкание зовёт вычислитель, а эти три переписываются законами и сличаются знак в знак. */ -typedef struct { int неотр, тожд, пор, охр; } Домен; +typedef struct { int неотр, тожд, пор, охр; double дно; } Домен; /* У КАЖДОЙ названной посылки правило обязано быть одним из двух названных (второе имя необязательно). Посылка с ПУСТЫМ правилом не в счёт: она закрыта шагами @@ -4087,9 +4109,12 @@ static int все_посылки_правилом(Сп посылки, const cha тем же тождеством. */ static Домен домен_цели(const char *цель, Сп посылки) { Домен д; char *l0, *p0, *у0, *т0, *и0; - д.тожд = д.пор = д.охр = 0; + д.тожд = д.пор = д.охр = 0; д.дно = 0; д.неотр = strcmp(цель, "результат не меньше 0") == 0; if (д.неотр) return д; + if (разрез_словом(терм(цель), " не меньше ", &l0, &p0) && !strcmp(ужать(l0), "результат") && число_точно(ужать(p0), &д.дно) && д.дно > 0 && д.дно <= 9007199254740991.0 + && все_посылки_правилом(посылки, "ограниченность точным потолком по построению", "порядок по построению")) return д; + д.дно = 0; д.тожд = разрез_равенства(терм(цель), &l0, &p0) && все_посылки_правилом(посылки, "тождество после переписки допущением", "разбор цели по условию"); if (д.тожд) return д; @@ -4106,6 +4131,7 @@ static Домен домен_цели(const char *цель, Сп посылки) цель ветви, только читает её из строки `требует`. */ static int правило_вне_домена(Домен д, const char *пр) { if (!*пр) return 0; + if (д.дно > 0) return strcmp(пр, "ограниченность точным потолком по построению") != 0 && strcmp(пр, "порядок по построению") != 0; if (д.неотр) return strcmp(пр, "неотрицательность по построению") != 0 && strcmp(пр, "цель есть допущение") != 0; if (д.тожд) return strcmp(пр, "тождество после переписки допущением") != 0 && @@ -4116,6 +4142,29 @@ static int правило_вне_домена(Домен д, const char *пр) { return !булево_правило(пр); } +static int дно_поля(Сп строки, const char *вариант, const char *поле) { + int i, n = 0; char *т = (char *)""; + for (i = 0; i < строки.n; i++) + if (начинается(как_читает_язык(строки.e[i]), fmt("вариант «%s» содержит ", вариант)) && ++n) + т = тип_довода_в_строке(fmt("принимает %s", хвост_после(как_читает_язык(строки.e[i]), " содержит ")), поле); + return n == 1 && *т && strcmp(объявление_типа(строки, имя_типа(т)).вид, "отрезок") == 0; +} +static Сп с_дном_по_объявлению(Сп bound, Сп строки, const char *чья, long a, long b, const char *вариант, const char *обр) { + Сп св = bound_имена_случая(обр), дов = имена_доводов_функции(строки, чья), им, тр; int k; + for (k = 0; k < дов.n; k++) if (!среди(св, дов.e[k]) && довод_с_дном(строки, a, b, дов.e[k])) добавить(&bound, дов.e[k]); + for (k = 0; strstr(обр, "» с ") && поля(обр, " как ", &им, &тр) && k < им.n; k++) if (дно_поля(строки, вариант, им.e[k])) добавить(&bound, тр.e[k]); + return bound; +} +static int не_ниже_дна(const char *т, double дно, const char *чья, Сп bound, Сп строки, char **почему) { + char *t = ужать(т); double v; int i; Разрез р = разрез_по(t, "плюс"); + if (число_точно(t, &v)) return v >= дно; + for (i = 0; i < bound.n; i++) if (strcmp(t, bound.e[i]) == 0) return 1; + if (р.есть && ((не_ниже_дна(р.лево, дно, чья, bound, строки, почему) && неотрицательно_algebra(р.право, чья, bound, строки, 0, почему)) || + (не_ниже_дна(р.право, дно, чья, bound, строки, почему) && неотрицательно_algebra(р.лево, чья, bound, строки, 0, почему)))) return 1; + *почему = fmt("«%s» не держит дна %s по построению", t, знач_в_строку(как_число(дно))); + return 0; +} + static int проиграть_узел_algebra(Сверка *s, Сп строки, const char *имя, const char *чья, const char *цель, const char *принцип, Сп посылки) { @@ -4140,10 +4189,11 @@ static int проиграть_узел_algebra(Сверка *s, Сп строк тело = тело_случая(строки, ци, b); if (!*тело) return не_проигран(s, имя, fmt("тело случая «%s» не читается одним термом", вариант)); - if (д.неотр) { + if (д.неотр || д.дно > 0) { bound = допущения_индукции(строки, чья, в_ёлочках(принцип, 2), bound_имена_случая(слова_после(как_читает_язык(часть(строки, ци)), 1))); - if (!неотрицательно_algebra(тело, чья, bound, строки, 0, &почему)) + if (д.неотр) bound = с_дном_по_объявлению(bound, строки, чья, a, b, вариант, слова_после(как_читает_язык(часть(строки, ци)), 1)); + if (д.дно > 0 ? !не_ниже_дна(тело, д.дно, чья, bound, строки, &почему) : !неотрицательно_algebra(тело, чья, bound, строки, 0, &почему)) return не_проигран(s, имя, fmt("случай «%s»: %s", вариант, почему)); } else if (д.тожд) { char *хв_сл = слова_после(как_читает_язык(часть(строки, ци)), 1); @@ -5800,6 +5850,15 @@ static int невыполнимая_посылка(Сп строки, long a, lo return 0; } +static char *поля_результата(const char *цель, const char *тело) { + Сп им, тр; int i; char *t = (char *)цель, *k, *w; + if (!начинается(тело, "запись «") || !поля(тело, " равным ", &им, &тр)) return t; + for (i = 0; i < им.n; i++) + for (w = fmt("результат.«%s»", им.e[i]); (k = strstr(t, w)) != NULL; t = fmt("%s%s%s", копия(t, (size_t)(k - t)), в_скобки(тр.e[i]), k + strlen(w))) + if (k != t && k[-1] != ' ' && k[-1] != '(') return (char *)цель; + return t; +} + static int разбором_цели(Сверка *s, Сп свои, Сп строки, const char *чья, const char *цель_сырая) { char *цель, *тело; long a, b; @@ -5808,11 +5867,12 @@ static int разбором_цели(Сверка *s, Сп свои, Сп стр не вправе; счёт снятого держится на этой строке. */ if (*первая_с_началом(свои, "принцип тип ") || все_с_началом(свои, "посылка ").n) return 0; if (!*цель_сырая || !кавычки_чисты(цель_сырая)) return 0; + if (!*чья && !есть_связыватель(терм(цель_сырая)) && половина_закрыта(терм(цель_сырая), строки, 0, NULL)) return 1; a = блок_функции(строки, чья, &b); if (a < 1) return 0; /* функции в исходнике нет — скажет сверка имён */ тело = тело_без_пуст(строки, a, b); if (!*тело || !кавычки_чисты(тело)) { s->разбор_мимо++; return 0; } - цель = вставить_вместо(терм(цель_сырая), "результат", тело); + цель = вставить_вместо(поля_результата(терм(цель_сырая), тело), "результат", тело); if (есть_связыватель(цель)) { s->разбор_мимо++; return 0; } if (половина_закрыта(цель, строки, 0, NULL)) return 1; if (из_объявленного(цель, строки, a, b)) return 1; @@ -8555,7 +8615,7 @@ static const char *МЕСТА_СТРОК[][3] = { { "свидетель ", "вид postcondition|вид statement|для всех |таких что ", "вид postcondition" }, { "после подстановки ", "свидетель ", "свидетель" }, - { "прогон «", "для всех |таких что ", "для всех" }, + { "прогон «", "для всех |таких что |вид statement", "для всех" }, /* Строка, вставшая не на своё место, сличается не с тем: разрешённое — со строкой `разрешает`, выданное — со списком разрешённого. Подмена места — подлог. */ { "разрешено «", "план «|разрешено «", "план" }, @@ -8790,6 +8850,25 @@ static int начало_от_вызванной(Сверка *s, Сп строк return 0; } +static int цель_от_вызванной(Сверка *s, Сп строки, const char *чья, const char *цель) { + char *ц = ужать(терм(цель)), *тело, *f; long a, b, i, где; int k; Сп дов, им; + if ((a = блок_функции(строки, чья, &b)) < 1) return 0; + тело = без_внешних(тело_без_пуст(строки, a, b)); f = в_ёлочках(тело, 1); им = имена_доводов_функции(строки, чья); + дов = найти_сверху(тело, ОТ_, 1, &где, &k) ? доводы_вызова(тело + где + strlen(ОТ_[0])) : ПУСТО; + if (!*f || strcmp(обрезать(копия(тело, (size_t)(дов.n ? где : (long)strlen(тело)))), fmt("«%s»", f)) != 0 || + все_требования_функции(строки, f).n || (a = блок_функции(строки, f, &b)) < 1) return 0; + for (k = 0; k < дов.n; k++) if (!простой(дов.e[k])) return 0; + for (k = 0, дов = имена_доводов_функции(строки, f); k < дов.n; k++) добавить(&им, дов.e[k]); + for (k = 0; k < им.n; k++) if (свободно_в(ц, им.e[k])) return 0; + for (i = a; i < b; i++) { + char *l = как_читает_язык(часть(строки, i)), *и = в_ёлочках(l, 1); + if ((!начинается(l, "обеспечивает «") && !(начинается(l, "для всех ") && содержит(l, " обеспечивает «"))) || + содержит(l, " таких что ") || (i + 1 < b && начинается(часть(строки, i + 1), " "))) continue; + if (среди(s->доказанные_свойства, и) && strcmp(ужать(терм(хвост_после(l, fmt("обеспечивает «%s» ", и)))), ц) == 0) return 1; + } + return 0; +} + /* Терм начинается с литерала П, если он сам П, литерал с таким началом (сличение написанного, не счёт), склейка с таким левым или выбор, у которого начинаются ОБЕ ветви. Иное — не взялся, а не «ладно». */ @@ -8876,6 +8955,7 @@ static Снято крюки_по_телу(Сверка *s, Сп свои, Сп if (сн.узлом || сн.разбором || !доказано || !без_посылок) return сн; if (свёртка_не_длиннее(строки, чья, цель)) { сн.узлом = 1; s->узел_булев = 0; return сн; } if (начало_от_вызванной(s, строки, чья, цель)) { сн.ходами = 1; s->сведений++; s->мест_по_телу++; return сн; } + if (цель_от_вызванной(s, строки, чья, цель)) { сн.ходами = 1; s->сведений++; s->мест_по_телу++; return сн; } if (начало_по_телу(строки, чья, цель)) { сн.ходами = 1; s->сведений++; s->мест_по_телу++; return сн; } if (strcmp(ужать(терм(цель)), "результат не меньше 0") == 0 && прямая_по_предположению(строки, чья)) { сн.узлом = 1; s->узел_булев = 0; } @@ -9856,7 +9936,7 @@ static Сверка сверить(const char *исходник, const char *з сверить_полноту(&s, строки, блоки); for (i = 0; i < блоки.n; i++) if (strcmp(слово_после(первая_с_началом(разделить(блоки.e[i], "\n"), "вердикт "), "вердикт "), "доказано") == 0) добавить(&s.объявленные_доказанными, в_ёлочках(часть(разделить(блоки.e[i], "\n"), 1), 1)); - if (содержит(запись_голова, "по свойству ")) реестр_доказанного(&s, блоки, строки); + if (содержит(запись_голова, "по свойству ") || содержит(запись_голова, "теоремы нет")) реестр_доказанного(&s, блоки, строки); for (i = 0; i < блоки.n; i++) сверить_блок_утверждения(&s, блоки.e[i], строки); сверить_круги(&s, блоки); /* Снятия — ПОСЛЕ утверждений: факт обещания вызванной берётся из реестра diff --git a/flang/proof/checker/tests/families/user-program/callee-argument.flang b/flang/proof/checker/tests/families/user-program/callee-argument.flang new file mode 100644 index 000000000..60f1242a3 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-argument.flang @@ -0,0 +1,13 @@ +модуль «Callee argument» + +тотальная функция «Себе» + принимает а: число + возвращает число + обеспечивает «отдаёт довод» результат равен а + а + +тотальная функция «Через себя» + принимает а: число + возвращает число + обеспечивает «отдаёт довод через вызов» результат равен а + «Себе» от а diff --git a/flang/proof/checker/tests/families/user-program/callee-argument.record b/flang/proof/checker/tests/families/user-program/callee-argument.record new file mode 100644 index 000000000..0fc016ea1 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-argument.record @@ -0,0 +1,39 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/user-program/callee-argument.flang +строк 14 +знаков 289 +отпечаток 620333743 644851864 +ядро 2 +утверждений 2 +отпечаток256 8a5d27a3f2b8008db0951ffba7e4dbaed7fc44a550e3bb84d7d7bdba08c9f7cc +тотальностей 2 +утверждение «отдаёт довод» функции «Себе» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Себе» от ( а )⟩ строка 7 ⟨а⟩ + ход 2 закрыть тождеством + ход конец +конец утверждения + +утверждение «отдаёт довод через вызов» функции «Через себя» строка 12 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет +конец утверждения + +тотальность «Себе» строка 3 + вид composition + самовызова нет + конец тотальности +тотальность «Через себя» строка 9 + вид composition + зовёт «Себе» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/callee-precondition.flang b/flang/proof/checker/tests/families/user-program/callee-precondition.flang new file mode 100644 index 000000000..7611d9b9c --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-precondition.flang @@ -0,0 +1,15 @@ +модуль «Callee precondition» + +тотальная функция «Неотрицательный» + принимает х: число + возвращает число + требует «довод неотрицателен» х не меньше 0 + обеспечивает «ответ неотрицателен» результат не меньше 0 + х + +тотальная функция «Через неотрицательный» + принимает довод: число + возвращает число + требует «свой довод неотрицателен» довод не меньше 0 + обеспечивает «ответ через вызов неотрицателен» результат не меньше 0 + «Неотрицательный» от довод diff --git a/flang/proof/checker/tests/families/user-program/callee-precondition.record b/flang/proof/checker/tests/families/user-program/callee-precondition.record new file mode 100644 index 000000000..1c54410ec --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-precondition.record @@ -0,0 +1,48 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/user-program/callee-precondition.flang +строк 16 +знаков 457 +отпечаток 409664684 695857331 +ядро 2 +утверждений 2 +отпечаток256 bb406ebbccb7944f580188a03856e8fd403e9ae6288c6c6e8be12694b3027f94 +тотальностей 2 +утверждение «ответ неотрицателен» функции «Неотрицательный» строка 7 + вид postcondition + вердикт доказано + теоремы нет + правило «цель есть допущение» + по объявлению нет + вывод цель ⟨результат не меньше 0⟩ + вывод 1 Н2 ⟨х не меньше 0⟩ строка 6 + вывод 2 Разв2 ⟨результат не меньше 0⟩ из 1 строка 8 + вывод конец +конец утверждения + +утверждение «ответ через вызов неотрицателен» функции «Через неотрицательный» строка 14 + вид postcondition + вердикт доказано + теоремы нет + правило «цель есть допущение» + по объявлению нет +конец утверждения + +снятие «довод неотрицателен» функции «Через неотрицательный» зовёт «Неотрицательный» строка 15 столбец 3 + вид precondition-at-call + вердикт доказано + правило «цель есть допущение» + вывод цель ⟨довод не меньше 0⟩ + вывод 1 Т1 ⟨довод не меньше 0⟩ строка 13 + вывод конец +конец снятия + +тотальность «Неотрицательный» строка 3 + вид composition + самовызова нет + конец тотальности +тотальность «Через неотрицательный» строка 10 + вид composition + зовёт «Неотрицательный» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/callee-promise.flang b/flang/proof/checker/tests/families/user-program/callee-promise.flang new file mode 100644 index 000000000..b9f21974f --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-promise.flang @@ -0,0 +1,16 @@ +модуль «Callee promise» + +объект «Человек» + «имя»: строка + +тотальная функция «Смертен ли» + принимает кто: «Человек» + возвращает признак + для всех кто обеспечивает «этот человек смертен» результат + «Смертен» от кто + +тотальная функция «Смертен» + принимает человек: «Человек» + возвращает признак + обеспечивает «всякий человек смертен» результат + да diff --git a/flang/proof/checker/tests/families/user-program/callee-promise.record b/flang/proof/checker/tests/families/user-program/callee-promise.record new file mode 100644 index 000000000..a509c8084 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/callee-promise.record @@ -0,0 +1,36 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/user-program/callee-promise.flang +строк 17 +знаков 354 +отпечаток 818071803 54880234 +ядро 2 +утверждений 2 +отпечаток256 d1ced38c8fcb0b61d08f2b1bec63021948a98facb0d0638839e557b4b8c655e4 +тотальностей 2 +утверждение «этот человек смертен» функции «Смертен ли» строка 9 + вид postcondition + для всех «кто» строка 9 + вердикт доказано + теоремы нет + правило «цель есть допущение» + по объявлению нет +конец утверждения + +утверждение «всякий человек смертен» функции «Смертен» строка 15 + вид postcondition + вердикт доказано + теоремы нет + правило «вычисление замкнутой цели» + по объявлению нет +конец утверждения + +тотальность «Смертен ли» строка 6 + вид composition + зовёт «Смертен» строка 12 тотальна + самовызова нет + конец тотальности +тотальность «Смертен» строка 12 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/maybe.record b/flang/proof/checker/tests/families/user-program/maybe.record new file mode 100644 index 000000000..8c1bc6695 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/maybe.record @@ -0,0 +1,44 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/maybe.flang +строк 37 +знаков 899 +отпечаток 355871831 632953843 +ядро 2 +утверждений 2 +отпечаток256 89e6fb85aa66a94d66b0068b7614bf1c6eeb09ebb474d212455b9d28bcb6e8f9 +тотальностей 3 +утверждение «ответ не меньше нуля» функции «Или по умолчанию» строка 10 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Может быть» по «может» носитель algebra база 2 шаг 0 + объявление сумма «Может быть» строка 3 варианты «Нет значения» 0 «Есть» 0 + сведение «неотрицательность по построению» + посылка «Нет значения» вид base вариант «Нет значения» вердикт доказано закрыта reduction шагов 0 правило «неотрицательность по построению» + посылка «Есть» вид base вариант «Есть» вердикт доказано закрыта reduction шагов 0 правило «неотрицательность по построению» +конец утверждения + +утверждение «пять есть значение» функции «Пять есть» строка 35 + вид postcondition + вердикт доказано + теоремы нет + правило «вычисление замкнутой цели» + по объявлению нет +конец утверждения + +тотальность «Или по умолчанию» строка 7 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +тотальность «Есть ли» строка 21 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +тотальность «Пять есть» строка 33 + вид composition + зовёт «Есть ли» строка 21 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/point.record b/flang/proof/checker/tests/families/user-program/point.record new file mode 100644 index 000000000..23022612c --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/point.record @@ -0,0 +1,42 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/point.flang +строк 21 +знаков 643 +отпечаток 762965101 127655548 +ядро 2 +утверждений 3 +отпечаток256 84309c898cc2a08c72a16a1c1c27566f3846ae87e25fb2ef9138fe1db7bb8c01 +тотальностей 2 +утверждение «отражение меняет х на у» функции «Отразить» строка 10 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет +конец утверждения + +утверждение «отражение меняет у на х» функции «Отразить» строка 11 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет +конец утверждения + +утверждение «начало лежит на нуле» функции «Начало» строка 19 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет +конец утверждения + +тотальность «Отразить» строка 7 + вид composition + самовызова нет + конец тотальности +тотальность «Начало» строка 17 + вид composition + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/shapes.record b/flang/proof/checker/tests/families/user-program/shapes.record new file mode 100644 index 000000000..06a718563 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/shapes.record @@ -0,0 +1,49 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/shapes.flang +строк 33 +знаков 1066 +отпечаток 778172214 914394229 +ядро 2 +утверждений 3 +отпечаток256 2ba150001bb31d99a9aa68ba213e952d9f14321667bd0dab6b98ace1256788eb +тотальностей 2 +утверждение «углов не больше четырёх» функции «Углов» строка 11 + вид postcondition + для всех «фигура» строка 11 + вердикт доказано + теоремы нет + принцип тип «Фигура» по «фигура» носитель algebra база 3 шаг 0 + объявление сумма «Фигура» строка 3 варианты «Круг» 0 «Прямоугольник» 0 «Треугольник» 0 + сведение «ограниченность точным потолком по построению» + посылка «Круг» вид base вариант «Круг» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» + посылка «Прямоугольник» вид base вариант «Прямоугольник» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» + посылка «Треугольник» вид base вариант «Треугольник» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» +конец утверждения + +утверждение «углов не меньше нуля» функции «Углов» строка 12 + вид postcondition + для всех «фигура» строка 12 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «круглая, либо углы есть» функции «Круглая ли» строка 27 + вид postcondition + для всех «фигура» строка 27 + вердикт нет вердикта + теоремы нет +конец утверждения + +тотальность «Углов» строка 8 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +тотальность «Круглая ли» строка 24 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/shopping-cart.record b/flang/proof/checker/tests/families/user-program/shopping-cart.record new file mode 100644 index 000000000..a9d2b3d25 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/shopping-cart.record @@ -0,0 +1,44 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/shopping-cart.flang +строк 27 +знаков 928 +отпечаток 926420799 120532736 +ядро 2 +утверждений 3 +отпечаток256 5314315f4ea34aed225fed0d729fb7dc9c1de25a79eb1a2b7f35cefb2fde3d76 +тотальностей 2 +утверждение «стоимость не отрицательна» функции «Стоимость позиции» строка 10 + вид postcondition + вердикт нет вердикта + теоремы нет +конец утверждения + +утверждение «итог не отрицателен» функции «Итог корзины» строка 19 + вид postcondition + для всех «позиции» строка 19 + вердикт нет вердикта + теоремы нет +конец утверждения + +утверждение «пустая корзина стоит ноль» строка 25 + вид statement + прогон «Итог корзины» шаг «Стоимость позиции» строка 16 + вердикт доказано + теоремы нет + правило «равенство, решённое счётом замкнутых частей» + по объявлению да +конец утверждения + +тотальность «Стоимость позиции» строка 7 + вид composition + зовёт примитив «умножить» + самовызова нет + конец тотальности +тотальность «Итог корзины» строка 16 + вид composition + зовёт «Стоимость позиции» строка 7 тотальна + зовёт примитив «плюс» + зовёт примитив «свёртка» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/socrates.record b/flang/proof/checker/tests/families/user-program/socrates.record new file mode 100644 index 000000000..3f31c059a --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/socrates.record @@ -0,0 +1,54 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/socrates.flang +строк 26 +знаков 570 +отпечаток 786211224 812602448 +ядро 2 +утверждений 3 +отпечаток256 a672a1d32140fe41c61a7246c3ebc288509cd47bcc8399fe2f1e1caabeed1b89 +тотальностей 4 +утверждение «всякий человек смертен» функции «Смертен» строка 9 + вид postcondition + вердикт доказано + теоремы нет + правило «вычисление замкнутой цели» + по объявлению нет +конец утверждения + +утверждение «этот человек смертен» функции «Смертен ли» строка 15 + вид postcondition + для всех «кто» строка 15 + вердикт доказано + теоремы нет + правило «цель есть допущение» + по объявлению нет +конец утверждения + +утверждение «Сократ смертен» функции «Сократ смертен» строка 24 + вид postcondition + вердикт доказано + теоремы нет + правило «вычисление замкнутой цели» + по объявлению нет +конец утверждения + +тотальность «Смертен» строка 6 + вид composition + самовызова нет + конец тотальности +тотальность «Смертен ли» строка 12 + вид composition + зовёт «Смертен» строка 6 тотальна + самовызова нет + конец тотальности +тотальность «Сократ» строка 18 + вид composition + самовызова нет + конец тотальности +тотальность «Сократ смертен» строка 22 + вид composition + зовёт «Сократ» строка 18 тотальна + зовёт «Смертен ли» строка 12 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/user-program/tree.record b/flang/proof/checker/tests/families/user-program/tree.record new file mode 100644 index 000000000..a2c7b7c4f --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/tree.record @@ -0,0 +1,35 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/tree.flang +строк 32 +знаков 925 +отпечаток 231080772 655856521 +ядро 2 +утверждений 2 +отпечаток256 0fe828117b6c5e6372a51efc95f57efaa46154fcc16c3ba16f8c70e7a3664065 + +утверждение «узлов не меньше нуля» функции «Узлов» строка 10 + вид postcondition + для всех «дерево» строка 10 + вердикт доказано + теоремы нет + принцип тип «Дерево» по «дерево» носитель algebra база 1 шаг 1 + объявление сумма «Дерево» строка 3 варианты «Лист» 0 «Узел» 2 + сведение «неотрицательность по построению» + посылка «Лист» вид base вариант «Лист» вердикт доказано закрыта reduction шагов 0 правило «неотрицательность по построению» + посылка «Узел» вид step вариант «Узел» вердикт доказано закрыта reduction шагов 0 правило «неотрицательность по построению» +конец утверждения + +утверждение «листьев хотя бы один» функции «Листьев» строка 23 + вид postcondition + для всех «дерево» строка 23 + вердикт доказано + теоремы нет + принцип тип «Дерево» по «дерево» носитель algebra база 1 шаг 1 + объявление сумма «Дерево» строка 3 варианты «Лист» 0 «Узел» 2 + сведение «ограниченность точным потолком по построению» + сведение «порядок по построению» + посылка «Лист» вид base вариант «Лист» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» + посылка «Узел» вид step вариант «Узел» вердикт доказано закрыта reduction шагов 0 правило «порядок по построению» +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/user-program/word-lengths.record b/flang/proof/checker/tests/families/user-program/word-lengths.record new file mode 100644 index 000000000..531d59cc7 --- /dev/null +++ b/flang/proof/checker/tests/families/user-program/word-lengths.record @@ -0,0 +1,45 @@ +запись доказательства 1 +исходник flang/proof/probes/user-programs/programs/word-lengths.flang +строк 20 +знаков 634 +отпечаток 419109214 344247649 +ядро 2 +утверждений 2 +отпечаток256 f84f127d99190f2e2a640b37b0140efc529f9dfec5981ea768d3cbd06750ffad +тотальностей 2 +утверждение «сумма длин не отрицательна» функции «Сумма длин» строка 6 + вид postcondition + для всех «слова» строка 6 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «длин столько же, сколько слов» функции «Длины» строка 15 + вид postcondition + вердикт доказано + теоремы нет + правило «тождество после переписки допущением» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Длины» от ( слова )⟩ строка 19 ⟨отобразить слова как слово → длина слово⟩ + ход 2 переписать формой ⟨длина (отобразить слова как слово → длина слово)⟩ = ⟨длина слова⟩ законом «Мера построения» + ход 3 закрыть тождеством + ход конец +конец утверждения + +тотальность «Сумма длин» строка 3 + вид composition + зовёт примитив «длина» + зовёт примитив «плюс» + зовёт примитив «свёртка» + самовызова нет + конец тотальности +тотальность «Длины» строка 12 + вид composition + зовёт примитив «длина» + зовёт примитив «отобразить» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 34d18a6bb..67a5c32d3 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -888,3 +888,31 @@ say ── захват при развёртке (аудит 2844): Разв2 P 2844 Разв2: тело под связывателем цели flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang flang/proof/checker/tests/records/corpus/poddelka-razv2-sebya.record - - - - 1 подстановка захватила бы имя - - P 2844 Разв3: доводы по одному дают «а минус а» flang/proof/checker/tests/programs/audit-2844/unfold3-difference.flang flang/proof/checker/tests/records/corpus/poddelka-razv3-raznost.record - - - - 1 не развёртывается в посылку шага 1 «( а минус а ) равен 0» - - C 2844 опора: честная развёртка «Разность» от б и а под требованием «( б минус а ) равен 0» flang/proof/checker/tests/programs/audit-2844/unfold3-control-honest.flang flang/proof/checker/tests/records/audit-2844/unfold3-control-honest.record - - - - 0 - - - +say ── 2748: пользовательские программы — обещание вызванной, поле записи, «случай любое», дно объявленного типа ── - - - - - - - - - - +C 2748: Сократ — цель по обещанию вызванной и замкнутая цель через вызов flang/proof/probes/user-programs/programs/socrates.flang flang/proof/checker/tests/families/user-program/socrates.record - - - - 0 - - - +C 2748: обещание вызванной, объявленной ниже зовущей flang/proof/checker/tests/families/user-program/callee-promise.flang flang/proof/checker/tests/families/user-program/callee-promise.record - - - - 0 - - - +C 2748: цель называет довод — подстановки нет, место на слове ядра flang/proof/checker/tests/families/user-program/callee-argument.flang flang/proof/checker/tests/families/user-program/callee-argument.record - - - - 3 - - - +C 2748: предусловие вызванной оплачено предусловием зовущей flang/proof/checker/tests/families/user-program/callee-precondition.flang flang/proof/checker/tests/families/user-program/callee-precondition.record - - - - 0 - - - +C 2748: поле результата — поле выписанной записи flang/proof/probes/user-programs/programs/point.flang flang/proof/checker/tests/families/user-program/point.record - - - - 0 - - - +C 2748: «случай любое», дно объявленного довода и поля варианта flang/proof/probes/user-programs/programs/maybe.flang flang/proof/checker/tests/families/user-program/maybe.record - - - - 0 - - - +C 2748: строка прогона у замкнутого утверждения flang/proof/probes/user-programs/programs/shopping-cart.flang flang/proof/checker/tests/families/user-program/shopping-cart.record - - - - 0 - - - +C 2748: Н11 — разбор с неотрицательными ветвями flang/proof/probes/user-programs/programs/shapes.flang flang/proof/checker/tests/families/user-program/shapes.record - - - - 0 - - - +C 2748: Н7 — шаг свёртки прибавляет длину flang/proof/probes/user-programs/programs/word-lengths.flang flang/proof/checker/tests/families/user-program/word-lengths.record - - - - 0 - - - +C 2748: дно выше нуля по индукции flang/proof/probes/user-programs/programs/tree.flang flang/proof/checker/tests/families/user-program/tree.record - - - - 0 - - - +P 2748: обещание вызванной, ослабленное строкой продолжения, не берётся целью flang/proof/checker/tests/families/user-program/callee-promise.flang flang/proof/checker/tests/families/user-program/callee-promise.record /«всякий человек смертен» результат$/s/$/\n или да/; s/^ да$/ нет/ - - - 3 - - - +P 2748: цель, называющая довод, не берётся по обещанию вызванной flang/proof/checker/tests/families/user-program/callee-argument.flang flang/proof/checker/tests/families/user-program/callee-argument.record s/^ «Себе» от а$/ «Себе» от 5/ - - - 3 - - - +P 2748: обещание вызванной с неоплаченным предусловием не берётся, и блока снятия нет flang/proof/checker/tests/families/user-program/callee-precondition.flang flang/proof/checker/tests/families/user-program/callee-precondition.record s/^ требует «свой довод неотрицателен» довод не меньше 0$// /^снятие /,/^конец снятия/d - - 3 - - - +P 2748: тело — не голый вызов, обещание вызванной не берётся flang/proof/checker/tests/families/user-program/callee-promise.flang flang/proof/checker/tests/families/user-program/callee-promise.record s/^ «Смертен» от кто$/ не («Смертен» от кто)/ - - - 3 - - - +P 2748: поле выписанной записи не то, что обещано flang/proof/probes/user-programs/programs/point.flang flang/proof/checker/tests/families/user-program/point.record s/^ запись «Точка» с «х» равным точка.«у» и «у» равным точка.«х»$/ запись «Точка» с «х» равным точка.«х» и «у» равным точка.«у»/ - - - 3 - - - +P 2748: «случай любое» считается своей ветвью flang/proof/probes/user-programs/programs/maybe.flang flang/proof/checker/tests/families/user-program/maybe.record /^тотальная функция «Есть ли»/,/^$/{/случай любое/{n;s/то да/то нет/}} - - - 3 - - - +P 2748: поле варианта без дна не даёт неотрицательности flang/proof/probes/user-programs/programs/maybe.flang flang/proof/checker/tests/families/user-program/maybe.record s/значение: нат$/значение: число/ - - - 3 - - - +P 2748: довод с дном, перекрытый образцом случая, дна не даёт flang/proof/probes/user-programs/programs/maybe.flang flang/proof/checker/tests/families/user-program/maybe.record s/значение: нат$/значение: число/; s/с значение как значение$/с значение как запас/; s/^ то значение$/ то запас/ - - - 3 - - - +P 2748: Н11 — отрицательная ветвь разбора flang/proof/probes/user-programs/programs/shapes.flang flang/proof/checker/tests/families/user-program/shapes.record s/^ то 3$/ то 0 минус 3/ - - - 3 - - - +P 2748: Н7 — шаг свёртки вычитает длину flang/proof/probes/user-programs/programs/word-lengths.flang flang/proof/checker/tests/families/user-program/word-lengths.record s/итог плюс (длина слово)$/итог минус (длина слово)/ - - - 3 - - - +P 2748: Н7 — прибавка не голая длина flang/proof/probes/user-programs/programs/word-lengths.flang flang/proof/checker/tests/families/user-program/word-lengths.record s/итог плюс (длина слово)$/итог плюс ((длина слово) минус 9)/ - - - 3 - - - +P 2748: Н7 — прибавка «длина Х минус 9» не мера flang/proof/probes/user-programs/programs/word-lengths.flang flang/proof/checker/tests/families/user-program/word-lengths.record s/итог плюс (длина слово)$/итог плюс (длина слово минус 9)/ - - - 3 - - - +P 2748: дно выше нуля — вторая прибавка отрицательна flang/proof/probes/user-programs/programs/tree.flang flang/proof/checker/tests/families/user-program/tree.record s/^ то («Листьев» от левое) плюс («Листьев» от правое)$/ то («Листьев» от левое) плюс (0 минус 5)/ - - - 3 - - - +P 2748: дно выше нуля — база ниже дна flang/proof/probes/user-programs/programs/tree.flang flang/proof/checker/tests/families/user-program/tree.record /^тотальная функция «Листьев»/,$ s/^ то 1$/ то 0/ - - - 3 - - - +P 2748: дно выше нуля — шаг вычитает flang/proof/probes/user-programs/programs/tree.flang flang/proof/checker/tests/families/user-program/tree.record s/^ то («Листьев» от левое) плюс («Листьев» от правое)$/ то («Листьев» от левое) минус («Листьев» от правое)/ - - - 3 - - - +P 2748: замкнутое утверждение ложно flang/proof/probes/user-programs/programs/shopping-cart.flang flang/proof/checker/tests/families/user-program/shopping-cart.record s/пустой список) равен 0$/пустой список) равен 1/ - - - 3 - - - +P 2748: строка прогона у замкнутого утверждения сличается с исходником flang/proof/probes/user-programs/programs/shopping-cart.flang flang/proof/checker/tests/families/user-program/shopping-cart.record - s/шаг «Стоимость позиции» строка 16$/шаг «Чужой шаг» строка 16/ - - 1 свёртка не зовёт шаг «Чужой шаг» - - diff --git a/flang/proof/probes/user-programs/programs/account.flang b/flang/proof/probes/user-programs/programs/account.flang new file mode 100644 index 000000000..0efb54c91 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/account.flang @@ -0,0 +1,21 @@ +модуль «Account» + +объект «Счёт» + «владелец»: строка + «остаток»: число + +тотальная функция «Пополнить» + принимает счёт: «Счёт», сумма: нат + возвращает «Счёт» + обеспечивает «владелец не меняется» результат.«владелец» равен счёт.«владелец» + пример «сто и пятьдесят» + дано счёт равно запись «Счёт» с «владелец» равным "Анна" и «остаток» равным 100 + дано сумма равно 50 + ожидается запись «Счёт» с «владелец» равным "Анна" и «остаток» равным 150 + запись «Счёт» с «владелец» равным счёт.«владелец» и «остаток» равным (счёт.«остаток» плюс сумма) + +тотальная функция «Переименовать» + принимает счёт: «Счёт», имя: строка + возвращает «Счёт» + обеспечивает «остаток при переименовании цел» результат.«остаток» равен счёт.«остаток» + запись «Счёт» с «владелец» равным имя и «остаток» равным счёт.«остаток» diff --git a/flang/proof/probes/user-programs/programs/counter.flang b/flang/proof/probes/user-programs/programs/counter.flang new file mode 100644 index 000000000..0578a4a62 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/counter.flang @@ -0,0 +1,29 @@ +модуль «Counter» + +тип «Счёт» + вариант «Ноль» + вариант «Следующий» содержит прежний: «Счёт» + +тотальная функция «К числу» + принимает счёт: «Счёт» + возвращает число + пример «два шага от нуля» + дано счёт равно вариант «Следующий» с прежний равным (вариант «Следующий» с прежний равным (вариант «Ноль»)) + ожидается 2 + разбор счёт + случай вариант «Ноль» + то 0 + случай вариант «Следующий» с прежний как прежний + то («К числу» от прежний) плюс 1 + +утверждение «шаг растит счёт на один» + для всех счёт: «Счёт» + утверждаем («К числу» от (вариант «Следующий» с прежний равным счёт)) равно ((«К числу» от счёт) плюс 1) + +теорема «шаг растит счёт на один» + дано счёт: «Счёт» + утверждаем («К числу» от (вариант «Следующий» с прежний равным счёт)) равно ((«К числу» от счёт) плюс 1) + индукция по счёт + случай вариант «Следующий» с прежний как прежний + то по предположению + следовательно доказано diff --git a/flang/proof/probes/user-programs/programs/discount.flang b/flang/proof/probes/user-programs/programs/discount.flang new file mode 100644 index 000000000..e8c6fa070 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/discount.flang @@ -0,0 +1,21 @@ +модуль «Discount» + +тотальная функция «Цена со скидкой» + принимает цена: неотрицательное, скидка: неотрицательное + возвращает число + требует «скидка не больше цены» скидка не больше цена + обеспечивает «цена не ушла в минус» результат не меньше 0 + пример «сто минус тридцать» + дано цена равно 100 + дано скидка равно 30 + ожидается 70 + цена минус скидка + +тотальная функция «Цена без скидки» + принимает цена: неотрицательное + возвращает число + обеспечивает «цена без скидки не ушла в минус» результат не меньше 0 + пример «скидка ноль цену не меняет» + дано цена равно 100 + ожидается 100 + «Цена со скидкой» от цена и 0 diff --git a/flang/proof/probes/user-programs/programs/door.flang b/flang/proof/probes/user-programs/programs/door.flang new file mode 100644 index 000000000..a7597cd93 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/door.flang @@ -0,0 +1,32 @@ +модуль «Door» + +тип «Дверь» + вариант «Открыта» + вариант «Закрыта» + вариант «Заперта» + +тотальная функция «Открыть» + принимает дверь: «Дверь» + возвращает «Дверь» + обеспечивает «после открытия дверь открыта» результат равен (вариант «Открыта») + пример «закрытую открыли» + дано дверь равно вариант «Закрыта» + ожидается вариант «Открыта» + вариант «Открыта» + +тотальная функция «Открыта ли» + принимает дверь: «Дверь» + возвращает признак + пример «запертая не открыта» + дано дверь равно вариант «Заперта» + ожидается нет + разбор дверь + случай вариант «Открыта» + то да + случай любое + то нет + +тотальная функция «Открытая открыта» + возвращает признак + обеспечивает «открытая дверь открыта» результат + «Открыта ли» от (вариант «Открыта») diff --git a/flang/proof/probes/user-programs/programs/greeting.flang b/flang/proof/probes/user-programs/programs/greeting.flang new file mode 100644 index 000000000..8eca9b28d --- /dev/null +++ b/flang/proof/probes/user-programs/programs/greeting.flang @@ -0,0 +1,15 @@ +модуль «Greeting» + +тотальная функция «Приветствие» + принимает имя: строка + возвращает строка + обеспечивает «приветствие начинается со слова» результат начинается с "Привет, " + пример «Анне» + дано имя равно "Анна" + ожидается "Привет, Анна" + соединить ["Привет, ", имя] по "" + +тотальная функция «Приветствие миру» + возвращает строка + обеспечивает «миру тоже привет» результат начинается с "Привет" + «Приветствие» от "мир" diff --git a/flang/proof/probes/user-programs/programs/maybe.flang b/flang/proof/probes/user-programs/programs/maybe.flang new file mode 100644 index 000000000..694d2d2d2 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/maybe.flang @@ -0,0 +1,36 @@ +модуль «Maybe» + +тип «Может быть» + вариант «Нет значения» + вариант «Есть» содержит значение: нат + +тотальная функция «Или по умолчанию» + принимает может: «Может быть», запас: нат + возвращает нат + обеспечивает «ответ не меньше нуля» результат не меньше 0 + пример «пусто — запас» + дано может равно вариант «Нет значения» + дано запас равно 7 + ожидается 7 + разбор может + случай вариант «Нет значения» + то запас + случай вариант «Есть» с значение как значение + то значение + +тотальная функция «Есть ли» + принимает может: «Может быть» + возвращает признак + пример «пусто» + дано может равно вариант «Нет значения» + ожидается нет + разбор может + случай вариант «Нет значения» + то нет + случай любое + то да + +тотальная функция «Пять есть» + возвращает признак + обеспечивает «пять есть значение» результат + «Есть ли» от (вариант «Есть» с значение равным 5) diff --git a/flang/proof/probes/user-programs/programs/point.flang b/flang/proof/probes/user-programs/programs/point.flang new file mode 100644 index 000000000..ee99285fe --- /dev/null +++ b/flang/proof/probes/user-programs/programs/point.flang @@ -0,0 +1,20 @@ +модуль «Point» + +объект «Точка» + «х»: число + «у»: число + +тотальная функция «Отразить» + принимает точка: «Точка» + возвращает «Точка» + обеспечивает «отражение меняет х на у» результат.«х» равен точка.«у» + обеспечивает «отражение меняет у на х» результат.«у» равен точка.«х» + пример «один и два» + дано точка равно запись «Точка» с «х» равным 1 и «у» равным 2 + ожидается запись «Точка» с «х» равным 2 и «у» равным 1 + запись «Точка» с «х» равным точка.«у» и «у» равным точка.«х» + +тотальная функция «Начало» + возвращает «Точка» + обеспечивает «начало лежит на нуле» результат.«х» равен 0 + запись «Точка» с «х» равным 0 и «у» равным 0 diff --git a/flang/proof/probes/user-programs/programs/positives.flang b/flang/proof/probes/user-programs/programs/positives.flang new file mode 100644 index 000000000..605bad54e --- /dev/null +++ b/flang/proof/probes/user-programs/programs/positives.flang @@ -0,0 +1,20 @@ +модуль «Positives» + +тотальная функция «Только положительные» + принимает числа: список числа + возвращает список числа + обеспечивает «все положительны» для всех число из результат: число больше 0 + обеспечивает «отбор список не удлиняет» (длина результат) не больше (длина числа) + пример «ноль и минус выброшены» + дано числа равно [3, 0, -2, 5] + ожидается [3, 5] + отфильтровать числа где число → число больше 0 + +тотальная функция «Удвоить все» + принимает числа: список числа + возвращает список числа + обеспечивает «длина сохраняется» (длина результат) равен (длина числа) + пример «три числа» + дано числа равно [1, 2, 3] + ожидается [2, 4, 6] + отобразить числа как число → число умножить на 2 diff --git a/flang/proof/probes/user-programs/programs/shapes.flang b/flang/proof/probes/user-programs/programs/shapes.flang new file mode 100644 index 000000000..52bd33b2a --- /dev/null +++ b/flang/proof/probes/user-programs/programs/shapes.flang @@ -0,0 +1,32 @@ +модуль «Shapes» + +тип «Фигура» + вариант «Круг» содержит радиус: число + вариант «Прямоугольник» содержит ширина: число, высота: число + вариант «Треугольник» содержит основание: число, высота: число + +тотальная функция «Углов» + принимает фигура: «Фигура» + возвращает число + для всех фигура обеспечивает «углов не больше четырёх» результат не больше 4 + для всех фигура обеспечивает «углов не меньше нуля» результат не меньше 0 + пример «у круга углов нет» + дано фигура равно вариант «Круг» с радиус равным 1 + ожидается 0 + разбор фигура + случай вариант «Круг» с радиус как радиус + то 0 + случай вариант «Прямоугольник» с ширина как ширина и высота как высота + то 4 + случай вариант «Треугольник» с основание как основание и высота как высота + то 3 + +тотальная функция «Круглая ли» + принимает фигура: «Фигура» + возвращает признак + для всех фигура обеспечивает «круглая, либо углы есть» результат или ((«Углов» от фигура) больше 0) + разбор фигура + случай вариант «Круг» с радиус как радиус + то да + случай любое + то нет diff --git a/flang/proof/probes/user-programs/programs/shopping-cart.flang b/flang/proof/probes/user-programs/programs/shopping-cart.flang new file mode 100644 index 000000000..a51576052 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/shopping-cart.flang @@ -0,0 +1,26 @@ +модуль «Shopping cart» + +объект «Позиция» + «цена»: неотрицательное + «штук»: нат + +тотальная функция «Стоимость позиции» + принимает позиция: «Позиция» + возвращает число + обеспечивает «стоимость не отрицательна» результат не меньше 0 + пример «три по десять» + дано позиция равно запись «Позиция» с «цена» равным 10 и «штук» равным 3 + ожидается 30 + позиция.«цена» умножить на позиция.«штук» + +тотальная функция «Итог корзины» + принимает позиции: список «Позиция» + возвращает число + для всех позиции обеспечивает «итог не отрицателен» результат не меньше 0 + пример «две позиции» + дано позиции равно [запись «Позиция» с «цена» равным 10 и «штук» равным 3, запись «Позиция» с «цена» равным 5 и «штук» равным 1] + ожидается 35 + свёртка позиции начиная с 0 как итог и позиция → итог плюс («Стоимость позиции» от позиция) + +утверждение «пустая корзина стоит ноль» + утверждаем («Итог корзины» от пустой список) равен 0 diff --git a/flang/proof/probes/user-programs/programs/socrates.flang b/flang/proof/probes/user-programs/programs/socrates.flang new file mode 100644 index 000000000..21e9df361 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/socrates.flang @@ -0,0 +1,25 @@ +модуль «Socrates» + +объект «Человек» + «имя»: строка + +тотальная функция «Смертен» + принимает человек: «Человек» + возвращает признак + обеспечивает «всякий человек смертен» результат + да + +тотальная функция «Смертен ли» + принимает кто: «Человек» + возвращает признак + для всех кто обеспечивает «этот человек смертен» результат + «Смертен» от кто + +тотальная функция «Сократ» + возвращает «Человек» + запись «Человек» с «имя» равным "Сократ" + +тотальная функция «Сократ смертен» + возвращает признак + обеспечивает «Сократ смертен» результат + «Смертен ли» от («Сократ») diff --git a/flang/proof/probes/user-programs/programs/statements.flang b/flang/proof/probes/user-programs/programs/statements.flang new file mode 100644 index 000000000..21a3e2cb3 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/statements.flang @@ -0,0 +1,12 @@ +модуль «Statements» + +утверждение «длина пустого списка нулевая» + утверждаем (длина пустой список) равен 0 + +утверждение «ноль нейтрален при сложении» + для всех число: неотрицательное таких что число больше 0 + утверждаем (число плюс 0) равен число + +утверждение «склейка с пустой строкой ничего не меняет» + для всех текст: строка + утверждаем (соединить [текст, ""] по "") равен текст diff --git a/flang/proof/probes/user-programs/programs/tree.flang b/flang/proof/probes/user-programs/programs/tree.flang new file mode 100644 index 000000000..4934aefa0 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/tree.flang @@ -0,0 +1,31 @@ +модуль «Tree» + +тип «Дерево» + вариант «Лист» + вариант «Узел» содержит значение: число, левое: «Дерево», правое: «Дерево» + +тотальная функция «Узлов» + принимает дерево: «Дерево» + возвращает число + для всех дерево обеспечивает «узлов не меньше нуля» результат не меньше 0 + пример «в листе узлов нет» + дано дерево равно вариант «Лист» + ожидается 0 + разбор дерево + случай «Лист» + то 0 + случай вариант «Узел» с левое как левое и правое как правое + то 1 плюс («Узлов» от левое) плюс («Узлов» от правое) + +тотальная функция «Листьев» + принимает дерево: «Дерево» + возвращает число + для всех дерево обеспечивает «листьев хотя бы один» результат не меньше 1 + пример «в листе один лист» + дано дерево равно вариант «Лист» + ожидается 1 + разбор дерево + случай «Лист» + то 1 + случай вариант «Узел» с левое как левое и правое как правое + то («Листьев» от левое) плюс («Листьев» от правое) diff --git a/flang/proof/probes/user-programs/programs/word-lengths.flang b/flang/proof/probes/user-programs/programs/word-lengths.flang new file mode 100644 index 000000000..4cc6bee02 --- /dev/null +++ b/flang/proof/probes/user-programs/programs/word-lengths.flang @@ -0,0 +1,19 @@ +модуль «Word lengths» + +тотальная функция «Сумма длин» + принимает слова: список строки + возвращает число + для всех слова обеспечивает «сумма длин не отрицательна» результат не меньше 0 + пример «три слова» + дано слова равно ["раз", "дважды", "трижды"] + ожидается 15 + свёртка слова начиная с 0 как итог и слово → итог плюс (длина слово) + +тотальная функция «Длины» + принимает слова: список строки + возвращает список числа + обеспечивает «длин столько же, сколько слов» (длина результат) равен (длина слова) + пример «два слова» + дано слова равно ["а", "бб"] + ожидается [1, 2] + отобразить слова как слово → длина слово diff --git a/flang/proof/probes/user-programs/run.fscript b/flang/proof/probes/user-programs/run.fscript new file mode 100644 index 000000000..6ac562f88 --- /dev/null +++ b/flang/proof/probes/user-programs/run.fscript @@ -0,0 +1,191 @@ +модуль «User program probes» + +объект «Program» + «name»: строка + «expected»: строка + +тотальная функция «Measure» + принимает name: строка + возвращает строка + пример «one program is checked by the kernel and replayed by the checker in a temporary directory» + дано name равно "socrates" + ожидается "d=$(mktemp -d -p \"${FLANG_TMP:-/srv/tmp}\" user-programs.XXXXXX) || exit 2; p=flang/proof/probes/user-programs/programs/socrates.flang; LC_ALL=C.UTF-8 bootstrap/flang check $p --proof --record $d/r --memory-limit 16G > $d/k 2>&1; k=$?; flang/proof/checker/сверщик --по-утверждениям $p $d/r > $d/c 2>&1; c=$?; printf 'proved=%s verified=%s kernel=%s checker=%s\\n' \"$(sed -n 's/.*утверждений [0-9]*: доказано \\([0-9]*\\).*/\\1/p' $d/k | head -1)\" \"$(grep -c ': ПРОВЕРЕНО (' $d/c)\" $k $c; grep '^ утверждение «.*: НЕ \\|^НЕ ВЗЯЛСЯ\\|^НЕ СОШЛОСЬ' $d/c; rm -rf \"$d\"" + соединить ["d=$(mktemp -d -p \"${FLANG_TMP:-/srv/tmp}\" user-programs.XXXXXX) || exit 2; p=flang/proof/probes/user-programs/programs/", name, ".flang; LC_ALL=C.UTF-8 bootstrap/flang check $p --proof --record $d/r --memory-limit 16G > $d/k 2>&1; k=$?; flang/proof/checker/сверщик --по-утверждениям $p $d/r > $d/c 2>&1; c=$?; printf 'proved=%s verified=%s kernel=%s checker=%s\\n' \"$(sed -n 's/.*утверждений [0-9]*: доказано \\([0-9]*\\).*/\\1/p' $d/k | head -1)\" \"$(grep -c ': ПРОВЕРЕНО (' $d/c)\" $k $c; grep '^ утверждение «.*: НЕ \\|^НЕ ВЗЯЛСЯ\\|^НЕ СОШЛОСЬ' $d/c; rm -rf \"$d\""] по "" + +тотальная функция «Expect» + принимает name: строка, wanted: строка + возвращает «Program» + обеспечивает «the program keeps its name» (результат.«name») равен name + запись «Program» с «name» равным name и «expected» равным wanted + +тотальная функция «Programs» + возвращает список «Program» + обеспечивает «there are fourteen user programs» (длина результат) равен 14 + [(«Expect» от "account" и "proved=2 verified=2 kernel=0 checker=0"), + («Expect» от "counter" и "proved=1 verified=1 kernel=0 checker=0"), + («Expect» от "discount" и "proved=2 verified=1 kernel=0 checker=3"), + («Expect» от "door" и "proved=2 verified=2 kernel=0 checker=0"), + («Expect» от "greeting" и "proved=1 verified=0 kernel=0 checker=3"), + («Expect» от "maybe" и "proved=2 verified=2 kernel=0 checker=0"), + («Expect» от "point" и "proved=3 verified=3 kernel=0 checker=0"), + («Expect» от "positives" и "proved=3 verified=3 kernel=0 checker=0"), + («Expect» от "shapes" и "proved=2 verified=2 kernel=3 checker=0"), + («Expect» от "shopping-cart" и "proved=1 verified=1 kernel=0 checker=0"), + («Expect» от "socrates" и "proved=3 verified=3 kernel=0 checker=0"), + («Expect» от "statements" и "proved=2 verified=2 kernel=3 checker=0"), + («Expect» от "tree" и "proved=2 verified=2 kernel=0 checker=0"), + («Expect» от "word-lengths" и "proved=2 verified=2 kernel=0 checker=0")] + +тотальная функция «Field» + принимает line: строка, key: строка + возвращает строка + пример «a field is read up to the next space» + дано line равно "proved=3 verified=2 kernel=0 checker=3" + дано key равно "verified=" + ожидается "2" + пример «a missing field is empty» + дано line равно "proved=3" + дано key равно "verified=" + ожидается "" + разбор (хвост (разделить line по key)) + случай пусто + то "" + случай голова и хвост + то голова (разделить голова по " ") + +тотальная функция «Count» + принимает text: строка + возвращает число + пример «digits become a number» + дано text равно "12" + ожидается 12 + пример «anything else counts as zero» + дано text равно "" + ожидается 0 + разбор (к числу или беда text) + случай вариант «Разобрано» с значение как значение + то значение + случай любое + то 0 + +тотальная функция «First line» + принимает text: строка + возвращает строка + пример «the summary line comes first» + дано text равно "proved=1 verified=1 kernel=0 checker=0\nНЕ ВЗЯЛСЯ" + ожидается "proved=1 verified=1 kernel=0 checker=0" + разбор (разделить text по "\n") + случай пусто + то "" + случай голова и хвост + то голова + +тотальная функция «Report line» + принимает program: «Program», output: строка + возвращает строка + пример «a program replayed in full has no reasons» + дано program равно запись «Program» с «name» равным "door" и «expected» равным "" + дано output равно "proved=2 verified=2 kernel=0 checker=0\n" + ожидается "door: kernel proved 2, checker verified 2, declined 0" + пример «a declined place is listed with the checker's own words» + дано program равно запись «Program» с «name» равным "greeting" и «expected» равным "" + дано output равно "proved=1 verified=0 kernel=0 checker=3\n утверждение «а»: НЕ ПРОВЕРЕНО\n" + ожидается "greeting: kernel proved 1, checker verified 0, declined 1\n утверждение «а»: НЕ ПРОВЕРЕНО" + пусть summary равно («First line» от output) + пусть proved равно («Count» от («Field» от summary и "proved=")) + пусть verified равно («Count» от («Field» от summary и "verified=")) + пусть reasons равно (отфильтровать (хвост (разделить output по "\n")) где line → (длина line) больше 0) + соединить (свёртка reasons начиная с [(соединить [(program.«name»), ": kernel proved ", (к строке proved), ", checker verified ", (к строке verified), ", declined ", (к строке (proved минус verified))] по "")] как lines и line → (добавить (соединить [" ", line] по "") к lines)) по "\n" + +объект «Tally» + «lines»: список строки + «complaints»: список строки + «proved»: число + «verified»: число + +тотальная функция «Empty tally» + возвращает «Tally» + обеспечивает «nothing is counted before the first program» (результат.«proved») равен 0 + запись «Tally» с «lines» равным пустой список и «complaints» равным пустой список и «proved» равным 0 и «verified» равным 0 + +тотальная функция «Add» + принимает tally: «Tally», program: «Program», output: строка + возвращает «Tally» + пример «a match adds the counts and no complaint» + дано tally равно запись «Tally» с «lines» равным пустой список и «complaints» равным пустой список и «proved» равным 0 и «verified» равным 0 + дано program равно запись «Program» с «name» равным "door" и «expected» равным "proved=2 verified=2 kernel=0 checker=0" + дано output равно "proved=2 verified=2 kernel=0 checker=0\n" + ожидается запись «Tally» с «lines» равным ["door: kernel proved 2, checker verified 2, declined 0"] и «complaints» равным пустой список и «proved» равным 2 и «verified» равным 2 + пример «a mismatch is a complaint that names both lines» + дано tally равно запись «Tally» с «lines» равным пустой список и «complaints» равным пустой список и «proved» равным 0 и «verified» равным 0 + дано program равно запись «Program» с «name» равным "door" и «expected» равным "proved=2 verified=2 kernel=0 checker=0" + дано output равно "proved=2 verified=1 kernel=0 checker=3\n" + ожидается запись «Tally» с «lines» равным ["door: kernel proved 2, checker verified 1, declined 1"] и «complaints» равным ["door: expected «proved=2 verified=2 kernel=0 checker=0», got «proved=2 verified=1 kernel=0 checker=3»"] и «proved» равным 2 и «verified» равным 1 + пусть summary равно («First line» от output) + пусть complaint равно (соединить [(program.«name»), ": expected «", (program.«expected»), "», got «", summary, "»"] по "") + запись «Tally» с «lines» равным (добавить («Report line» от program и output) к (tally.«lines»)) и «complaints» равным (если summary равен (program.«expected») то (tally.«complaints») иначе (добавить complaint к (tally.«complaints»))) и «proved» равным ((tally.«proved») плюс («Count» от («Field» от summary и "proved="))) и «verified» равным ((tally.«verified») плюс («Count» от («Field» от summary и "verified="))) + +тотальная функция «Outcome» + принимает tally: «Tally» + возвращает «Продолжение» + пусть total равно (соединить ["user programs: kernel proved ", (к строке (tally.«proved»)), ", checker verified ", (к строке (tally.«verified»))] по "") + пусть text равно (соединить (добавить total к (tally.«lines»)) по "\n") + разбор (tally.«complaints») + случай пусто + то вариант «Конец работы» с значение равным text + случай голова и хвост + то вариант «Провал» с код равным "FLANG_USER_PROGRAM_PROBES" и сообщение равным (соединить (добавить (соединить ["user program probes DIVERGED:\n · ", (соединить (tally.«complaints») по "\n · ")] по "") к [text]) по "\n") + +тип «Stage» + вариант «Start» + вариант «Awaiting program» содержит program: «Program», remaining: список «Program», tally: «Tally» + +тотальная функция «Begin» + возвращает «Stage» + пример «the plan starts with the first program» + ожидается вариант «Start» + вариант «Start» + +тотальная функция «Walk» + принимает queue: список «Program», tally: «Tally» + возвращает «Продолжение» + разбор queue + случай пусто + то «Outcome» от tally + случай голова и хвост + то вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", (соединить ["cd ../../../.. && ", («Measure» от (голова.«name»))] по "")]) и потом равным (вариант «Awaiting program» с program равным голова и remaining равным хвост и tally равным tally) + +тотальная функция «Nothing to look with» + принимает reason: строка + возвращает «Продолжение» + пример «a program that could not run is not a verdict on the checker» + дано reason равно "sh did not start" + ожидается вариант «Не проверено» с код равным "FLANG_USER_PROGRAM_PROBES_CANNOT_LOOK" и сообщение равным "sh did not start" + вариант «Не проверено» с код равным "FLANG_USER_PROGRAM_PROBES_CANNOT_LOOK" и сообщение равным reason + +тотальная функция «After program» + принимает program: «Program», remaining: список «Program», tally: «Tally», reply: «Отклик» + возвращает «Продолжение» + разбор reply + случай вариант «Процесс завершён» с код как code и вывод как output и ошибки как errors + то «Walk» от remaining и («Add» от tally и program и output) + случай вариант «Процесс убит» с сигнал как signal и вывод как output и ошибки как errors + то «Nothing to look with» от (соединить ["program «", (program.«name»), "» was killed by ", signal] по "") + случай вариант «Сбой» с код как code и сообщение как message + то «Nothing to look with» от (соединить ["program «", (program.«name»), "» did not run (", code, "): ", message] по "") + случай любое + то «Nothing to look with» от (соединить ["expected a process answer on program «", (program.«name»), "»"] по "") + +тотальная функция «Next» + принимает stage: «Stage», reply: «Отклик» + возвращает «Продолжение» + разбор stage + случай вариант «Start» + то «Walk» от («Programs») и («Empty tally») + случай вариант «Awaiting program» с program как program и remaining как remaining и tally как tally + то «After program» от program и remaining и tally и reply + +план «User program probes» + состояние «Stage» + начинает с «Begin» + обрабатывает «Next» diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index bc49d3b65..5b8f0fc0b 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,7 +1,7 @@ forgeries 36 forgery-numerator 155 forgery-probes 572 -checker-code-lines 7711 +checker-code-lines 7788 checker-primitives 15 trap-kinds 38 trap-goals-on-kernel-word 3 From e8a9d3da927fd72cca21119a45e7f1a918deaa6f Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 13:11:38 +0000 Subject: [PATCH 2/7] docs(tasks): record task 2748 results and its print batch entry Co-Authored-By: Claude Opus 5.5 --- ...a-verdict-that-rests-on-a-declared-type.md | 112 +++++++++++++++++- 1 file changed, 108 insertions(+), 4 deletions(-) diff --git a/docs/tasks/2748-the-checker-cannot-replay-a-verdict-that-rests-on-a-declared-type.md b/docs/tasks/2748-the-checker-cannot-replay-a-verdict-that-rests-on-a-declared-type.md index 4a4b1a02a..11ab751bd 100644 --- a/docs/tasks/2748-the-checker-cannot-replay-a-verdict-that-rests-on-a-declared-type.md +++ b/docs/tasks/2748-the-checker-cannot-replay-a-verdict-that-rests-on-a-declared-type.md @@ -1,10 +1,10 @@ --- номер: 2748 заголовок: Проверяющая программа не переигрывает утверждение, у которого в записи стоит только имя правила -статус: свободна +статус: сделана частично — на 14 пользовательских программах проверяющая программа переигрывает 26 мест из 28, доказанных компилятором (было 13); два места остаются с названной причиной приоритет: P1 -исполнитель: — -ветка: — +исполнитель: a +ветка: a/4573-checker-reads-module-types-and-dependency-sets команда: первая карта: Где именно упирается доказатель рядом: 3846, 1183 @@ -87,6 +87,110 @@ $ flang/proof/checker/сверщик …/syllogism-socrates.flang <запись> строкой с посылками, а приём для него добавляется в `flang/proof/checker/checker.c` (место отказа — `сверить_объявление`); пересборка семени не нужна, но растёт размер проверяющей программы, у - которого есть потолок в `flang/proof/checker/ratchet.txt`. + которого есть потолок (`checker-code-lines` в `flang/proof/ratchets.txt`). Вычислитель в проверяющую программу не добавлять: она нарочно без него. + +## Что сделано + +### Набор пользовательских программ + +`flang/proof/probes/user-programs/programs/` — 14 программ в духе +`docs/examples/guide`: записи, суммы, списки, свёртки, предусловие, теорема по +индукции, свободные утверждения. План `run.fscript` прогоняет ядро с записью и +сверщик на каждой и печатает «ядро доказало / сверщик переиграл / отказы с причинами»; +расхождение с ожидаемой строкой — провал. Шаг CI «Check user programs are replayed by +the checker» в `binary.yml`, работа `storozha`. Прогон — 2 секунды. + +| программа | ядро доказало | сверщик до | сверщик после | что осталось | +|---|---:|---:|---:|---| +| account | 2 | 0 | 2 | | +| counter | 1 | 1 | 1 | | +| discount | 2 | 1 | 1 | предусловие вызванной, см. ниже | +| door | 2 | 2 | 2 | | +| greeting | 1 | 0 | 0 | литерал с пробелом, см. ниже | +| maybe | 2 | 0 | 2 | | +| point | 3 | 0 | 3 | | +| positives | 3 | 3 | 3 | | +| shapes | 2 | 1 | 2 | | +| shopping-cart | 1 | 0 (код 1!) | 1 | | +| socrates | 3 | 1 | 3 | | +| statements | 2 | 2 | 2 | | +| tree | 2 | 1 | 2 | | +| word-lengths | 2 | 1 | 2 | | +| **всего** | **28** | **13 (46 %)** | **26 (93 %)** | | + +«До» снято сверщиком `gh/dev` `dcfd766d4` на тех же записях; «после» — этой веткой. + +**shopping-cart до правки — ложное обвинение**: сверщик отвечал кодом 1 («строка +записи 25 «прогон …» стоит не сразу под строкой «для всех»»). Печать ставит строку +«прогон» и у замкнутого утверждения, без `для всех`, а сверщик требовал её только под +связыванием. + +### Правки проверяющей программы + +Все семь — правила, уже стоящие в ведомости, либо уравнения вычислителя; новых строк +ведомости, лемм Lean и примитивов нет. +77 строк кода, потолок 7711 → 7788 ровно на +съеденное (`checker-code-lines` в `flang/proof/ratchets.txt`). + +1. **Цель по обещанию вызванной** (`цель_от_вызванной`): тело — голый вызов «F» с + простыми доводами, у F нет `требует`, её обещание с той же целью знак в знак + проверено сверщиком по существу, цель не называет ни одного довода. Реестр + проверенного собирается предпроходом и там, где в записи есть «теоремы нет»: + иначе вызванная, объявленная ниже зовущей, давала отказ. +2. **Поле результата при теле-записи**: `результат.«п»` становится значением поля + выписанной записи (К↑ на конструкторе записи). +3. **«случай любое» в вычислителе примера** — ветвь берётся, только если каждый + образец выше заведомо про другой вариант. +4. **Замкнутое утверждение без функции** закрывается тем же `половина_закрыта`. +5. **Строка «прогон»** допускается прямо под «вид statement»; её содержание + сверяется, как прежде. +6. **Неотрицательность**: Н11 — тело-разбор, каждая ветвь неотрицательна и образец не + перекрывает довода; Н7 — шаг «накопитель плюс длина Х» при простом Х; Н3 — довод и + поле варианта, объявленные типом с дном и не перекрытые образцом. +7. **Дно выше нуля в узле индукции** (`результат не меньше К`, К > 0): литерал не + ниже К, допущение индукции, либо сумма, где одна часть не ниже К, а другая + неотрицательна. + +Пробы — строки «2748» в `flang/proof/checker/tests/probes.tsv`, семья +`flang/proof/checker/tests/families/user-program/`: десять честных, семнадцать +подделок. Каждая часть правки снята копией сверщика без неё, и покраснело: + +| снятая часть | что покраснело | +|---|---| +| правило 1 целиком | обе честные пробы Сократа — код 3 | +| предпроход реестра | вызванная ниже зовущей — код 3 | +| проверка «цель не называет доводов» | подделка `«Себе» от 5` — **принята кодом 0** | +| проверка «тело — голый вызов» | подделка `не («Смертен» от кто)` — **принята кодом 0** | +| проверка «у вызванной нет требует» | подделка без `требует` у зовущей и без блока снятия — **принята кодом 0** | +| правило 2 / чтение имени поля | честная point — код 3 | +| правило 3 | честная maybe — код 3 | +| дно поля по объявлению | подделки «поле без дна» и «перекрытый довод» — **приняты кодом 0** | +| проверка перекрытия довода образцом | подделка «перекрытый довод» — **принята кодом 0** | +| Н11 | честная shapes — код 3 | +| Н7 с длиной / «Х простой» | честная word-lengths — 3 / подделка «длина слово минус 9» — **0** | +| дно выше нуля / сравнение литерала / вторая часть суммы | честная tree — 3 / «база 0» — **0** / «плюс (0 минус 5)» — **0** | +| правило 4 | честная shopping-cart — код 3 | +| правило 5 | честная shopping-cart — код 1 | + +Одна часть пробой не держится: отказ брать обещание, у которого есть строка +продолжения ниже. Сверщик сегодня проверяет обещание по первой строке, так что +сравнение по первой строке честно и без этой оговорки; оговорка оставлена на случай, +когда сверщик начнёт читать продолжение (строк кода она не стоит). + +Приёмка: ответы сверщика на 518 записей дерева с исходником — байт в байт прежние; +`sh scripts/доказуемость.sh` — ДОКАЗУЕМ, 650 из 650; Lean — «сошлось всё», +расхождений 0. + +### Что осталось, с причиной + +* **discount, «цена без скидки не ушла в минус»** — вызванная «Цена со скидкой» имеет + `требует`, и правило 1 её не берёт. Нужно два шага: (а) печать — блок снятия + `0 не больше цена` печатается без вывода, это в партию печати: компилятор печатает блок снятия «0 не больше цена» выводом; (б) сверщик — правило 1 берёт вызванную с `требует`, когда каждое её снятие + в этой точке вызова проиграно заново. Без (а) (б) делать нечем. +* **greeting, «миру тоже привет»** — в теле литерал `"Привет, "` с пробелом внутри; + сверщик нарочно не разбирает терм с пробелом или скобкой в литерале + (`кавычки_чисты`). Это предел чтения термов строкой, отдельная работа. +* **Попутная находка**: запись без блока снятия у вызова с `требует` сверщик считает + («мест вызова без блока снятия 1»), но на вердикт это не влияет. Проверка «у + вызванной нет требует» в правиле 1 держит этот случай; сама дыра шире правила 1. From db7159ca886df389f4d6e183cecc032af097b4bb Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 14:20:19 +0000 Subject: [PATCH 3/7] fix(checker): read module types and dependency sets as the linker does The checker now narrows a dependency set by the importers' "only" lists, so a hidden namesake no longer collides (tls, tls-handshake), looks up a type declared in a visible module of the set (hmac, postgres, redis) and declines instead of lying when no set is given. The share runner passes each record the transitive dependency set. With a set, stdlib code 1 goes from 5 of 49 to 0 of 49. Co-Authored-By: Claude Opus 5.5 --- ...hecker-verdicts-on-the-standard-library.md | 78 +++++++++++++++++-- flang/proof/checker/checker.c | 35 ++++++++- .../tests/families/module-type-consumer.flang | 12 +++ .../families/module-type-consumer.record | 26 +++++++ .../families/module-type-dependency.flang | 5 ++ .../families/module-type-dependency.record | 10 +++ .../tests/families/same-name-consumer.flang | 8 ++ .../tests/families/same-name-consumer.record | 16 ++++ .../families/same-name-first-self-call.flang | 6 ++ .../tests/families/same-name-first.flang | 6 ++ .../tests/families/same-name-first.record | 15 ++++ .../tests/families/same-name-second.flang | 11 +++ .../tests/families/same-name-second.record | 20 +++++ flang/proof/checker/tests/probes.tsv | 8 ++ flang/proof/ratchets.txt | 2 +- scripts/ledgers/proved-share-ledger.txt | 1 + 16 files changed, 246 insertions(+), 13 deletions(-) create mode 100644 flang/proof/checker/tests/families/module-type-consumer.flang create mode 100644 flang/proof/checker/tests/families/module-type-consumer.record create mode 100644 flang/proof/checker/tests/families/module-type-dependency.flang create mode 100644 flang/proof/checker/tests/families/module-type-dependency.record create mode 100644 flang/proof/checker/tests/families/same-name-consumer.flang create mode 100644 flang/proof/checker/tests/families/same-name-consumer.record create mode 100644 flang/proof/checker/tests/families/same-name-first-self-call.flang create mode 100644 flang/proof/checker/tests/families/same-name-first.flang create mode 100644 flang/proof/checker/tests/families/same-name-first.record create mode 100644 flang/proof/checker/tests/families/same-name-second.flang create mode 100644 flang/proof/checker/tests/families/same-name-second.record diff --git a/docs/tasks/4573-checker-verdicts-on-the-standard-library.md b/docs/tasks/4573-checker-verdicts-on-the-standard-library.md index 3cde84186..beb5b5ba3 100644 --- a/docs/tasks/4573-checker-verdicts-on-the-standard-library.md +++ b/docs/tasks/4573-checker-verdicts-on-the-standard-library.md @@ -1,10 +1,10 @@ --- номер: 4573 заголовок: Проверяющая программа отвечает кодом 1 на честных записях пяти модулей библиотеки: типы чужого модуля и тёзки в наборе -статус: свободна +статус: сделана — с набором кодов 1 на библиотеке 0 из 49 приоритет: P1 -исполнитель: — -ветка: — +исполнитель: a +ветка: a/4573-checker-reads-module-types-and-dependency-sets команда: первая карта: Где именно упирается доказатель рядом: 9337, 4416, 6341, 2718 @@ -80,20 +80,19 @@ flang 0.7.23). Прогон из шагов воспроизведения на hmac, postgres, redis, tls, tls-handshake с набором отвечает кодом 0 или 3, кодом 1 — ни один. -`sh flang/proof/checker/tests/run.sh` — «сошлось всё», принятых кодом 0 подделок 0, +`bootstrap/flang run-script checker:check` — «сошлось всё», принятых кодом 0 подделок 0, отвергнутых честных 0; в семействах проб есть честная запись с типом чужого модуля и честная с тёзками в наборе, и у каждой подделка (объявление подменено, тёзка подсунута вместо вызванной) — код 1. Ответы на прежние записи дерева -с исходником — байт в байт прежние. `LEAN=~/.elan/bin/lean sh flang/proof/lean/run.sh` +с исходником — байт в байт прежние. прогон Lean `flang/proof/lean/run.fscript` — «сошлось всё». ## Где живёт правка Проверяющая программа: `flang/proof/checker/checker.c` — сверка строки «объявление» у принципа индукции (сообщение «объявления типа в исходнике нет») -и реестр набора `предпроход`; потолок строк — `flang/proof/checker/ratchet.txt`; -храповик подделок — `flang/proof/forgeries/ratchet.txt`; пробы — -`flang/proof/checker/tests/run.sh` и `flang/proof/checker/tests/families/`. +и реестр набора `предпроход`; потолок строк и храповик подделок — `flang/proof/ratchets.txt`; пробы — +`flang/proof/checker/tests/probes.tsv` и `flang/proof/checker/tests/families/`. Если строке «объявление» нужен модуль, печать записи — `flang/self/zapis.flang`, и эта половина доезжает до двоичного только пересборкой семени (bootstrap regeneration); правка на C её не требует. @@ -102,3 +101,66 @@ regeneration); правка на C её не требует. (`scripts/provability.fscript`) подаёт проверяющей программе набор по транзитивному замыканию `использует`, и после этого решается, включать ли библиотеку в набор доли. + +## Что сделано + +Как компилятор связывает модули (`flang/self/link.flang`, «Запомнить просьбу», +«Слить просьбы», «Сузить видимость», «Повтор функции»): пространство имён +программы одно; функция и тип модуля М входят в него, только если видны — +`использует «М»` без `только` делает видным всё, иначе видно объединение списков +`только` всех ввозящих; два видимых определения одного имени — `FLANG_DUPLICATE_NAME`. +Сверщик читает набор так же. + +1. **В. Тёзки в наборе.** Блок зависимости, чьё имя скрыто списками `только` + (`видно`, `видно_из_модуля`, `задать_набор`), не входит ни в сторож коллизии, + ни в реестр, ни в граф кругов (`предпроход`). В `tls` «Шаг начала» из + `aes.flang` и «Цифра 16» из `der.flang` скрыты (`tls.flang:2`, `:4`), видны + только их тёзки из `hmac.flang` и `sha256.flang`. Модуль, которого в наборе не + ввозит никто, виден целиком, как прежде; сужение только убирает блоки. + Объединение просьб — над-оценка видимости: у компилятора файл, уже привезённый + с узким списком, второй раз не сливается, так что видно у него бывает меньше. + Лишнее видимое даёт сверщику больше тёзок (код 1), а не приём кодом 0. +2. **Б. Тип из модуля.** `объявление_типа`: тип, не объявленный в своём + исходнике, ищется у видимых модулей набора; годится ровно одно объявление, и + строка записи `объявление сумма «Т» строка N …` сверяется с ним. Не нашлось, а + файл ввозит модули (`ввозит`) — «не берусь» (3) с названной причиной вместо + прежнего кода 1 «принципа индукции нет». Печать ядра модуль по-прежнему не + называет: однозначность даёт правило связывания «два видимых — ошибка». +3. **Д. Прогон доли подаёт набор.** `corpus-share.sh` (`nabor_zavisimostey`, + `modul_po_imeni`): у каждого исходника транзитивное замыкание `использует` + (с `из "…"` — путь от каталога файла; без — файл с `модуль «М»` в каталоге и + выше до корня дерева, затем `flang/stdlib`, `flang/core`), и каждому зовомому, + чья запись лежит в том же каталоге записей, — `--зависимость ИСХОДНИК ЗАПИСЬ`. + На корпусе доли ответ не изменился (650 / 650 = 100.00 % до и после): из 86 + исходников `использует` есть у одного (`poddelka-sortirovka-ne-ubyvaet.flang`), + а записи `lists.flang` в корпусе нет. + +### Пробы + +Строки «4573 Б, В» в `flang/proof/checker/tests/probes.tsv`: тип из модуля без набора — +3, с набором — 0; строка объявления и вариант подменены — 1; тёзка, скрытый +списком `только`, — 0; `только` снят — 1; «Шаг» в `same-name-first` зовёт сам +себя, а честный тёзка скрыт (`families/same-name-first-self-call.flang`) — 1. +Потолок `checker-code-lines` 7788 → 7815. + +### Библиотека с набором + +Ядро: записей 49 из 51 (`kdf.flang` — ядро само код 1; `datetime.flang` — не +уложилось в 3600 с), как 27 сентября. Набор — транзитивное замыкание +`использует` тем же правилом, что в прогоне доли; у кого из зовомых нет записи +(`kdf`), тот не подан. + +| сверщик | один файл: 0 / 1 / 3 | с набором: 0 / 1 / 3 | +|---|---:|---:| +| `dcfd766d4` (до Б, В) | 0 / 23 / 26 | 0 / 5 / 44 | +| эта ветка | 0 / 23 / 26 | 0 / **0** / 49 | + +С набором код 1 ушёл у `hmac`, `postgres`, `redis` (Б), `tls`, `tls-handshake` +(В); `http` — уже у `dcfd766d4` (план А). Одним файлом все 23 кода 1 — нехватка +набора: жалоба «… НИ в записи, НИ в поданном наборе», у `tls-handshake` ещё +нульместные вызовы модуля, узнаваемые только по исходнику набора. + +Прогон доли на одной библиотеке (49 записей в своём каталоге): с набором — все 49 +приняты (код 0 или 3), доля 1682 / 3693 = 45,55 %; прежним прогоном без набора — +отвергнуто 23, доля 791 / 4351 = 18,18 %. + diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index 84d8816c4..7b8fd133f 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -755,7 +755,31 @@ static Объявление объявление_типа_(Сп строки, co if (о.варианты.n == 0) { о.вид = ""; о.откуда = (char *)""; } /* `тип «Т»` без единого варианта — не сумма */ return о; } -static Объявление объявление_типа(Сп строки, const char *имя) { return объявление_типа_(строки, имя, 0); } +static Сп НАБОР_СТРОК, НАБОР_ВИДНО; +static int ввозит(Сп строки) { int i, есть = 0; for (i = 0; i < строки.n; i++) есть |= начинается(обрезать(строки.e[i]), "использует «"); return есть; } +static char *видно_из_модуля(Сп все, const char *модуль) { + char *r = (char *)"", *l; int d, i; Сп ст; + for (d = 0; *модуль && d < все.n; d++) + for (ст = разделить(все.e[d], "\n"), i = 0; i < ст.n; i++) + if (начинается(l = обрезать(без_примечания(ст.e[i])), "использует «") && strcmp(в_ёлочках(l, 1), модуль) == 0) { + if (!strstr(l, " только ")) return (char *)""; + r = fmt("%s%s,", r, strstr(l, " только ")); + } + return r; +} +static int видно(int d, const char *имя) { return d >= НАБОР_ВИДНО.n || !*НАБОР_ВИДНО.e[d] || strstr(НАБОР_ВИДНО.e[d], fmt("«%s»", имя)); } +static void задать_набор(const char *исходник, Сп набор_исх) { + Сп все = ПУСТО; int d; + НАБОР_СТРОК = набор_исх; НАБОР_ВИДНО = ПУСТО; добавить(&все, (char *)исходник); + for (d = 0; d < набор_исх.n; d++) добавить(&все, набор_исх.e[d]); + for (d = 0; d < набор_исх.n; d++) добавить(&НАБОР_ВИДНО, видно_из_модуля(все, в_ёлочках(первая_с_началом(разделить(набор_исх.e[d], "\n"), "модуль «"), 1))); +} +static Объявление объявление_типа(Сп строки, const char *имя) { + Объявление о = объявление_типа_(строки, имя, 0), н, один = о; int d, найдено = 0; + for (d = 0; !*о.откуда && d < НАБОР_СТРОК.n; d++) + if (видно(d, обрезать(имя)) && *(н = объявление_типа_(разделить(НАБОР_СТРОК.e[d], "\n"), имя, 0)).откуда) { один = н; найдено++; } + return найдено > 1 ? о : один; +} static Сп варианты_типа(Сп строки, const char *имя) { Объявление о = объявление_типа(строки, имя); if (strcmp(о.вид, "сумма") == 0 || strcmp(о.вид, "встроенная-сумма") == 0) return о.варианты; @@ -8194,6 +8218,8 @@ static void сверить_покрытие(Сверка *s, Сп свои, Сп int отрезок = strcmp(об.вид, "отрезок") == 0; int ладно = strcmp(носитель, "segment") == 0 ? отрезок : (strcmp(носитель, "algebra") == 0 || strcmp(носитель, "fold") == 0) ? сумма : 0; + if (*объявлено && !*об.откуда && ввозит(строки)) { s->на_слово++; + добавить(&s->не_взялся, fmt("теорема «%s»: тип «%s» довода «%s» объявлен не в этом файле и не в поданном наборе — сверять объявление не с чем, не берусь", имя_т, имя_об, по0)); return; } if (*объявлено) { если_не(s, *об.вид, fmt("теорема «%s»: довод «%s» объявлен типом «%s» — принципа индукции по нему нет: объявление не сумма, не запись, не отрезок", @@ -9555,6 +9581,7 @@ static void предпроход(Сверка *s, Сп набор_исх, Сп for (i = 0; i < блоки.n; i++) { char *имя = имя_блока_т(блоки.e[i]); char *раз = fmt("%s|%s|%ld", имя, sha, строка_блока_т(блоки.e[i])); + if (!видно(d, имя)) continue; добавить(все_блоки, блоки.e[i]); for (j = 0; j < имена.n; j++) if (strcmp(имена.e[j], имя) == 0 && strcmp(ключи.e[j], раз) != 0) { @@ -9588,7 +9615,7 @@ static void предпроход(Сверка *s, Сп набор_исх, Сп char *имя = имя_блока_т(блоки.e[i]); Сверка tmp; Сп зовёт; int уже = 0, k, все_в_реестре = 1; for (k = 0; k < реестр->n; k++) if (strcmp(реестр->e[k], имя) == 0) { уже = 1; break; } - if (уже) continue; + if (уже || !видно(d, имя)) continue; memset(&tmp, 0, sizeof tmp); сверить_тотальность(&tmp, блоки.e[i], строки, все_имена, *реестр, известные); if (tmp.беды.n != 0) continue; @@ -9849,8 +9876,7 @@ static int объявлено_в_файле(const char *текст, const char * return 0; } static Сп чужие_имена(Сп строки, Сп известные) { - Сп r = ПУСТО; int i, есть = 0; char *текст = соединить(строки, "\n"), *p = текст, *k; - for (i = 0; i < строки.n; i++) есть |= начинается(обрезать(строки.e[i]), "использует «"); + Сп r = ПУСТО; int есть = ввозит(строки); char *текст = соединить(строки, "\n"), *p = текст, *k; while (есть && (p = strstr(p, "«")) != NULL && (k = strstr(p, "»")) != NULL) { char *имя = копия(p + strlen("«"), (size_t)(k - p) - strlen("«")); if (!среди(известные, имя) && !среди(r, имя) && !объявлено_в_файле(текст, имя)) добавить(&r, имя); @@ -9923,6 +9949,7 @@ static Сверка сверить(const char *исходник, const char *з ОГЛАВЛЕНИЕ = ПУСТО; ОГЛ_БЕДЫ = ПУСТО; for (i = 0; i < шапка.n; i++) if (начинается(обрезать(шапка.e[i]), "таблица «")) добавить(&ОГЛАВЛЕНИЕ, обрезать(шапка.e[i])); + задать_набор(исходник, набор_исх); привязка_отпечатком(&s, исходник, ждём); for (i = 0; i < части.n; i++) if (!начинается(части.e[i], "запись доказательства")) добавить(&блоки, части.e[i]); diff --git a/flang/proof/checker/tests/families/module-type-consumer.flang b/flang/proof/checker/tests/families/module-type-consumer.flang new file mode 100644 index 000000000..91975f768 --- /dev/null +++ b/flang/proof/checker/tests/families/module-type-consumer.flang @@ -0,0 +1,12 @@ +модуль «Type consumer» + использует «Type dependency» из "module-type-dependency.flang" + +тотальная функция «Номер цвета» + принимает цвет: «Цвет» + возвращает число + обеспечивает «номер не меньше единицы» результат не меньше 1 + разбор цвет + случай вариант «Красный» + то 1 + случай вариант «Зелёный» + то 2 diff --git a/flang/proof/checker/tests/families/module-type-consumer.record b/flang/proof/checker/tests/families/module-type-consumer.record new file mode 100644 index 000000000..d84f7a55d --- /dev/null +++ b/flang/proof/checker/tests/families/module-type-consumer.record @@ -0,0 +1,26 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/module-type-consumer.flang +строк 13 +знаков 322 +отпечаток 556848695 705135320 +ядро 2 +утверждений 1 +отпечаток256 640fe3940cfcd239d334e05ac88f1a50584668fa73d7e40e1eaf354fd85f7a79 +тотальностей 1 +утверждение «номер не меньше единицы» функции «Номер цвета» строка 7 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Цвет» по «цвет» носитель algebra база 2 шаг 0 + объявление сумма «Цвет» строка 3 варианты «Красный» 0 «Зелёный» 0 + сведение «ограниченность точным потолком по построению» + посылка «Красный» вид base вариант «Красный» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» + посылка «Зелёный» вид base вариант «Зелёный» вердикт доказано закрыта reduction шагов 0 правило «ограниченность точным потолком по построению» +конец утверждения + +тотальность «Номер цвета» строка 4 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/module-type-dependency.flang b/flang/proof/checker/tests/families/module-type-dependency.flang new file mode 100644 index 000000000..4030400af --- /dev/null +++ b/flang/proof/checker/tests/families/module-type-dependency.flang @@ -0,0 +1,5 @@ +модуль «Type dependency» + +тип «Цвет» + вариант «Красный» + вариант «Зелёный» diff --git a/flang/proof/checker/tests/families/module-type-dependency.record b/flang/proof/checker/tests/families/module-type-dependency.record new file mode 100644 index 000000000..5f9212fc4 --- /dev/null +++ b/flang/proof/checker/tests/families/module-type-dependency.record @@ -0,0 +1,10 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/module-type-dependency.flang +строк 6 +знаков 77 +отпечаток 566736251 805762207 +ядро 2 +утверждений 0 +отпечаток256 f883004c3d3a0b8f909f1f3fc92da780bfb466c0c092c3b9d1870dc48eaa7770 + +конец записи diff --git a/flang/proof/checker/tests/families/same-name-consumer.flang b/flang/proof/checker/tests/families/same-name-consumer.flang new file mode 100644 index 000000000..8457e5c54 --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-consumer.flang @@ -0,0 +1,8 @@ +модуль «Namesake consumer» + использует «Namesake A» из "same-name-first.flang" + использует «Namesake B» из "same-name-second.flang" только «Второе» + +тотальная функция «Оба шага» + принимает н: число + возвращает число + «Второе» от («Шаг» от н) diff --git a/flang/proof/checker/tests/families/same-name-consumer.record b/flang/proof/checker/tests/families/same-name-consumer.record new file mode 100644 index 000000000..3332c0b6b --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-consumer.record @@ -0,0 +1,16 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/same-name-consumer.flang +строк 9 +знаков 247 +отпечаток 465100589 952691768 +ядро 2 +утверждений 0 +отпечаток256 27f915c519b802ec0ea86c3a75f39f15dcabc4b22e513553cbd531042f6937be +тотальностей 1 +тотальность «Оба шага» строка 5 + вид composition + зовёт «Шаг» строка 3 тотальна + зовёт «Второе» строка 8 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/same-name-first-self-call.flang b/flang/proof/checker/tests/families/same-name-first-self-call.flang new file mode 100644 index 000000000..f57a610a4 --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-first-self-call.flang @@ -0,0 +1,6 @@ +модуль «Namesake A» + +тотальная функция «Шаг» + принимает н: число + возвращает число + «Шаг» от н diff --git a/flang/proof/checker/tests/families/same-name-first.flang b/flang/proof/checker/tests/families/same-name-first.flang new file mode 100644 index 000000000..493ead718 --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-first.flang @@ -0,0 +1,6 @@ +модуль «Namesake A» + +тотальная функция «Шаг» + принимает н: число + возвращает число + н плюс 1 diff --git a/flang/proof/checker/tests/families/same-name-first.record b/flang/proof/checker/tests/families/same-name-first.record new file mode 100644 index 000000000..0c5098fda --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-first.record @@ -0,0 +1,15 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/same-name-first.flang +строк 7 +знаков 96 +отпечаток 984214978 903244102 +ядро 2 +утверждений 0 +отпечаток256 7eebec7cff44e846599dfd58c6140e5f7426244ff27551cde4839e4a2394950b +тотальностей 1 +тотальность «Шаг» строка 3 + вид composition + зовёт примитив «плюс» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/same-name-second.flang b/flang/proof/checker/tests/families/same-name-second.flang new file mode 100644 index 000000000..d4396a008 --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-second.flang @@ -0,0 +1,11 @@ +модуль «Namesake B» + +тотальная функция «Шаг» + принимает н: число + возвращает число + н плюс 2 + +тотальная функция «Второе» + принимает н: число + возвращает число + н умножить на 2 diff --git a/flang/proof/checker/tests/families/same-name-second.record b/flang/proof/checker/tests/families/same-name-second.record new file mode 100644 index 000000000..d854b3cde --- /dev/null +++ b/flang/proof/checker/tests/families/same-name-second.record @@ -0,0 +1,20 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/same-name-second.flang +строк 12 +знаков 182 +отпечаток 876512817 708593930 +ядро 2 +утверждений 0 +отпечаток256 563c8512a04a5546a754f3c4c2ececcd87fa9a14f900bc70e1fccc7fee483095 +тотальностей 2 +тотальность «Шаг» строка 3 + вид composition + зовёт примитив «плюс» + самовызова нет + конец тотальности +тотальность «Второе» строка 8 + вид composition + зовёт примитив «умножить» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 67a5c32d3..877858a21 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -916,3 +916,11 @@ P 2748: дно выше нуля — база ниже дна flang/proof/probes P 2748: дно выше нуля — шаг вычитает flang/proof/probes/user-programs/programs/tree.flang flang/proof/checker/tests/families/user-program/tree.record s/^ то («Листьев» от левое) плюс («Листьев» от правое)$/ то («Листьев» от левое) минус («Листьев» от правое)/ - - - 3 - - - P 2748: замкнутое утверждение ложно flang/proof/probes/user-programs/programs/shopping-cart.flang flang/proof/checker/tests/families/user-program/shopping-cart.record s/пустой список) равен 0$/пустой список) равен 1/ - - - 3 - - - P 2748: строка прогона у замкнутого утверждения сличается с исходником flang/proof/probes/user-programs/programs/shopping-cart.flang flang/proof/checker/tests/families/user-program/shopping-cart.record - s/шаг «Стоимость позиции» строка 16$/шаг «Чужой шаг» строка 16/ - - 1 свёртка не зовёт шаг «Чужой шаг» - - +say ── 4573 Б, В: тип из модуля; тёзки в наборе, скрытые списком «только» ── - - - - - - - - - - +C 4573 Б: тип из модуля, набор не подан — не берусь flang/proof/checker/tests/families/module-type-consumer.flang flang/proof/checker/tests/families/module-type-consumer.record - - - - 3 объявлен не в этом файле и не в поданном наборе - - +C 4573 Б: тип из модуля сверяется с объявлением в наборе flang/proof/checker/tests/families/module-type-consumer.flang flang/proof/checker/tests/families/module-type-consumer.record - - --зависимость flang/proof/checker/tests/families/module-type-dependency.flang flang/proof/checker/tests/families/module-type-dependency.record - 0 - - - +P 4573 Б: строка объявления типа из модуля не та flang/proof/checker/tests/families/module-type-consumer.flang flang/proof/checker/tests/families/module-type-consumer.record - s/объявление сумма «Цвет» строка 3/объявление сумма «Цвет» строка 4/ --зависимость flang/proof/checker/tests/families/module-type-dependency.flang flang/proof/checker/tests/families/module-type-dependency.record - 1 объявление сумма «Цвет» строка 4 - - +P 4573 Б: варианты типа из модуля не те flang/proof/checker/tests/families/module-type-consumer.flang flang/proof/checker/tests/families/module-type-consumer.record - s/варианты «Красный» 0 «Зелёный» 0/варианты «Красный» 0 «Синий» 0/ --зависимость flang/proof/checker/tests/families/module-type-dependency.flang flang/proof/checker/tests/families/module-type-dependency.record - 1 «Синий» - - +C 4573 В: тёзка, скрытый списком «только», не спорит flang/proof/checker/tests/families/same-name-consumer.flang flang/proof/checker/tests/families/same-name-consumer.record - - --зависимость flang/proof/checker/tests/families/same-name-first.flang flang/proof/checker/tests/families/same-name-first.record --зависимость flang/proof/checker/tests/families/same-name-second.flang flang/proof/checker/tests/families/same-name-second.record - 0 - - - +P 4573 В: два видимых тёзки — сторож коллизии цел flang/proof/checker/tests/families/same-name-consumer.flang flang/proof/checker/tests/families/same-name-consumer.record s/ только «Второе»$// - --зависимость flang/proof/checker/tests/families/same-name-first.flang flang/proof/checker/tests/families/same-name-first.record --зависимость flang/proof/checker/tests/families/same-name-second.flang flang/proof/checker/tests/families/same-name-second.record - 1 в наборе два разных определения «Шаг» - - +P 4573 В: скрытый честный тёзка не отмывает ложный видимый блок flang/proof/checker/tests/families/same-name-consumer.flang flang/proof/checker/tests/families/same-name-consumer.record - - --зависимость flang/proof/checker/tests/families/same-name-first-self-call.flang flang/proof/checker/tests/families/same-name-first.record --зависимость flang/proof/checker/tests/families/same-name-second.flang flang/proof/checker/tests/families/same-name-second.record - 1 «Шаг» не примитив и не имеет блока тотальности - - diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index 5b8f0fc0b..3fbe7c2bf 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,7 +1,7 @@ forgeries 36 forgery-numerator 155 forgery-probes 572 -checker-code-lines 7788 +checker-code-lines 7815 checker-primitives 15 trap-kinds 38 trap-goals-on-kernel-word 3 diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index da8965bc6..e65b4ea4e 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1646,6 +1646,7 @@ b07768e93f07c719e5308625d33aa9fb|1|1|0|0|0|flang/proof/checker/tests/families/st 8e14992c133eedfc079cbeff033ca00c|1|1|0|0|0|flang/proof/checker/tests/families/boolean-goal/negation-binds-tighter.flang 47b79056590d79634a29ca75e78c214e|1|1|0|0|0|flang/proof/checker/tests/families/totality-postcondition-over-several-lines.flang afc8a388476719fb2c821b83b8b80200|1|0|0|1|0|flang/proof/checker/tests/families/boolean-goal/negation-before-a-conjunction.flang +b7cd548c89af8a7e4863ce474cfbff6c|1|1|0|0|0|flang/proof/checker/tests/families/module-type-consumer.flang fe51d1d52d0266bdec14f79a067c0dbd|4|4|0|0|0|flang/proof/probes/memory-limit/run.fscript 6ad60a03be2f80c5573400fe1879c8f7|3|3|0|0|0|flang/proof/probes/module-root/run.fscript 24e692b2bca339493e8e7601ec41fb12|1|1|0|0|0|docs/examples/guide/ladder-as-table.flang From c86b63a7478833b2171f9d14378ee24b5ffe5c23 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 14:47:33 +0000 Subject: [PATCH 4/7] chore(numbers): sync counts, ledger lines and file name words Measured counts follow the rebase onto the user-program checker work; its new probe files get their proved-share ledger lines and their English file name words, so the pre-push hook is green. Co-Authored-By: Claude Opus 5.5 --- ...er-is-a-new-kind-of-value-not-a-new-name.md | 2 +- docs/design/nositel-tochnogo-celogo.md | 2 +- scripts/ledgers/file-name-words.txt | 7 +++++++ scripts/ledgers/proved-share-ledger.txt | 18 ++++++++++++++++++ 4 files changed, 27 insertions(+), 2 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 1a41db9bc..0262a7d5a 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`, - 10095 строк. + 10122 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index 3fbfef109..f4630fd0e 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` (10095 строк) +3. **Цену для проверяющей программы.** `checker.c` (10122 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/scripts/ledgers/file-name-words.txt b/scripts/ledgers/file-name-words.txt index 24434087c..1f31ae13a 100644 --- a/scripts/ledgers/file-name-words.txt +++ b/scripts/ledgers/file-name-words.txt @@ -9,6 +9,7 @@ acceptance accepted accepts access +account accumulates accumulating across @@ -211,6 +212,7 @@ carrier carries carry carrying +cart case cases catalog @@ -678,6 +680,7 @@ graph gratis greater green +greeting grep grid group @@ -866,6 +869,7 @@ legal lemma lemmas length +lengths less lesson let @@ -952,6 +956,7 @@ material math mathematics may +maybe md5 mean means @@ -1484,12 +1489,14 @@ shadow shadows shape shaped +shapes share shared shares shell shifted shipment +shopping shortcut shortcuts shortener diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index e65b4ea4e..9a7a89aff 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1647,6 +1647,24 @@ b07768e93f07c719e5308625d33aa9fb|1|1|0|0|0|flang/proof/checker/tests/families/st 47b79056590d79634a29ca75e78c214e|1|1|0|0|0|flang/proof/checker/tests/families/totality-postcondition-over-several-lines.flang afc8a388476719fb2c821b83b8b80200|1|0|0|1|0|flang/proof/checker/tests/families/boolean-goal/negation-before-a-conjunction.flang b7cd548c89af8a7e4863ce474cfbff6c|1|1|0|0|0|flang/proof/checker/tests/families/module-type-consumer.flang +11d8e0373a4f516cdfd685e0664eb2a4|2|2|0|0|0|flang/proof/checker/tests/families/user-program/callee-promise.flang +5c302d4b67c4d23e60a7ad1fa44c80eb|2|2|0|0|0|flang/proof/probes/user-programs/programs/maybe.flang +3f2013188158b5e1052e16b4782abcbd|2|1|1|0|0|flang/proof/probes/user-programs/programs/greeting.flang +ef35a92bbd654d9b49661c21d8e8a51c|3|×|×|×|0|flang/proof/probes/user-programs/run.fscript +0d59946a1c36817d12819685c1dfc13f|1|1|0|0|0|flang/proof/probes/user-programs/programs/counter.flang +21d7c8aac933da43dd1a394e5d317fd3|2|2|0|0|0|flang/proof/probes/user-programs/programs/tree.flang +2c032ea4181211738fa012decd4cda5d|3|2|0|1|0|flang/proof/probes/user-programs/programs/statements.flang +e3f824a35733612eed8e45a0ab0ded4b|2|2|0|0|1|flang/proof/probes/user-programs/programs/discount.flang +d1906b63610f4ccc9208e7e0d43f5c1b|2|2|0|0|2|flang/proof/checker/tests/families/user-program/callee-precondition.flang +4680750a85981cdb30d0e5488ba97501|3|2|0|1|0|flang/proof/probes/user-programs/programs/shapes.flang +e5eeb82a3f3104ea5f92dc323bb86977|3|1|2|0|0|flang/proof/probes/user-programs/programs/shopping-cart.flang +115c9184cbcdd94769361ccaa6fc938a|3|3|0|0|0|flang/proof/probes/user-programs/programs/point.flang +b82dff9d6801e17aceb4993dac771be6|3|3|0|0|0|flang/proof/probes/user-programs/programs/positives.flang +e40c5b6e77a7648e670421ae545d79aa|2|2|0|0|0|flang/proof/probes/user-programs/programs/door.flang +261c3a969c7ece381b55394d780ede0e|2|2|0|0|0|flang/proof/checker/tests/families/user-program/callee-argument.flang +5745ad3ceb42865f0c9e3da4f4cd38db|3|3|0|0|0|flang/proof/probes/user-programs/programs/socrates.flang +9dd5cff79c8be02e1548f4318b90ef0d|2|2|0|0|0|flang/proof/probes/user-programs/programs/account.flang +94a03a7ae4f586c48a221f51f833e880|2|2|0|0|0|flang/proof/probes/user-programs/programs/word-lengths.flang fe51d1d52d0266bdec14f79a067c0dbd|4|4|0|0|0|flang/proof/probes/memory-limit/run.fscript 6ad60a03be2f80c5573400fe1879c8f7|3|3|0|0|0|flang/proof/probes/module-root/run.fscript 24e692b2bca339493e8e7601ec41fb12|1|1|0|0|0|docs/examples/guide/ladder-as-table.flang From b04c20badbf114e1ec8bc105575d3b959bb52997 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 17:00:37 +0000 Subject: [PATCH 5/7] chore(numbers): sync counts after rebase and raise the probe ratchet The probes of tasks 2748 and 4573 are now rows of probes.tsv, and the forgery-probe ratchet follows the measured count, 572 to 596. Counts quoted in prose and the tree inventory are re-measured after the rebase onto dev. 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 +- flang/proof/ratchets.txt | 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 e6d34647a..c030f39df 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -164,8 +164,8 @@ permissions: jobs: # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c` - # планом на flang — 1029 файл; разбор в задаче 5821. - # СНЯТО 2026-09-17 файлов *.flang = 1029 + # планом на flang — 1052 файл; разбор в задаче 5821. + # СНЯТО 2026-09-17 файлов *.flang = 1052 # # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в diff --git a/docs/course/README.md b/docs/course/README.md index e2ea7de7c..9b8f08853 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`, счёт строк `пример` | | 51 файлов и 32 074 строки библиотеки | `ls flang/stdlib/*.flang`, `cat … \| wc -l` | -| 724 заметки, 238 примеров, 361 файл доказательств | `ls`, `find` | +| 724 заметки, 238 примеров, 384 файл доказательств | `ls`, `find` | | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа | **Чего переснять не удалось, и это надо знать.** diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index 3fbe7c2bf..f9f983e71 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,6 +1,6 @@ forgeries 36 forgery-numerator 155 -forgery-probes 572 +forgery-probes 596 checker-code-lines 7815 checker-primitives 15 trap-kinds 38 diff --git a/flang/scripts/count-guard.mjs b/flang/scripts/count-guard.mjs index 4d7f5a039..b43b64bd0 100644 --- a/flang/scripts/count-guard.mjs +++ b/flang/scripts/count-guard.mjs @@ -43,8 +43,8 @@ * * • ЧИСЛО ФАЙЛОВ он не сверяет. «AST всех 60 файлов `.flang` репозитория * напечатан до и после правки» — не утверждение о размере дерева, а запись о - * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1029 файла, но - * СНЯТО 2026-09-17 файлов *.flang = 1029 + * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1052 файла, но + * СНЯТО 2026-09-17 файлов *.flang = 1052 * прогон-то был на шестидесяти, и подставить туда 168 значило бы соврать про * работу, которой не делали. Отличить «столько в дереве» от «столько прошло * через прогон» нечем, кроме чтения, — значит сторож сюда не лезет. diff --git a/flang/scripts/name-guard.mjs b/flang/scripts/name-guard.mjs index 1bdc77b53..ac59fe99f 100644 --- a/flang/scripts/name-guard.mjs +++ b/flang/scripts/name-guard.mjs @@ -130,8 +130,8 @@ * переставшая сравнивать, продолжает зеленеть. * * Поэтому охват ПЕЧАТАЕТСЯ каждым прогоном и закреплён тестом «охват сторожа - * назван числом»: 300 файлов из 1029. Остальные 1099 — не упущение: - * СНЯТО 2026-09-17 файлов *.flang = 1029 + * назван числом»: 300 файлов из 1052. Остальные 1099 — не упущение: + * СНЯТО 2026-09-17 файлов *.flang = 1052 * * • 503 — печать замеров (`docs/benchmark*`): * это ВЫВОД прогона, а не исходник, и правилам имени он не подчиняется; From 043076ec5dcf8fac10aa7a7a607479ceafc0bf44 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 18:59:32 +0000 Subject: [PATCH 6/7] docs(site): name 288 theorems after the new probes Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- docs/site/index.md | 2 +- docs/site/index.ru.md | 2 +- docs/site/proofs.md | 2 +- docs/site/proofs.ru.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/site/index.md b/docs/site/index.md index e8f5b6dfa..4a6c7ad62 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 **287** such theorems in the repository, 55 of them in the +tactics. There are **288** 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 0aa6b195a..2e07f6885 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, а -не как скрипт из тактик. Таких теорем в дереве языка **287**, из них **55** в +не как скрипт из тактик. Таких теорем в дереве языка **288**, из них **55** в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`, сумма по `awk`). diff --git a/docs/site/proofs.md b/docs/site/proofs.md index a6c61c089..ec42606ca 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 287 such theorems in the repository, 55 of +it searches for nothing. There are 288 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 6ed0cfa53..776c09e51 100644 --- a/docs/site/proofs.ru.md +++ b/docs/site/proofs.ru.md @@ -64,7 +64,7 @@ руками**, как в Coq или Isabelle. `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как Isar в Isabelle, и prover проверяет каждый шаг, -ничего не ища. В дереве языка таких теорем 287, из них 55 в стандартной +ничего не ища. В дереве языка таких теорем 288, из них 55 в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Большинству постусловий теорема не нужна: отчёт о доказательствах показывает отдельным числом, сколько доказано **без написанного доказательства**. From be7b87edf87a848cb649bb173ca9b91a57c8b725 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Thu, 1 Oct 2026 22:31:40 +0000 Subject: [PATCH 7/7] chore(numbers): sync measured counts after rebase Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- docs/tree-inventory.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 319384a65..7ac0601e5 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 | 870 683 | 0 | 0 | +| C | 37 | 870 790 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | | HTML | 7 | 1 263 | 0 | 0 |