diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index e11a91ce0..bf0baf5d8 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -340,8 +340,8 @@ jobs: # Примеры двух каталогов, которые СХОДЯТСЯ ЦЕЛИКОМ и потому годятся в # дешёвый гейт по голому коду возврата, без ведомости: # - # flang/stdlib 51 файлов, 3745 примера, прошли все 44 мин - # СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 + # flang/stdlib 52 файлов, 3745 примера, прошли все 44 мин + # СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 # СНЯТО 2026-09-13 примеров-в flang/stdlib/*.flang = 3745 # flang/core 4 файла, 184 примера, прошли все 15 с # СНЯТО 2026-09-05 файлов flang/core/*.flang = 4 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c030f39df..45d4bbecb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -164,8 +164,8 @@ permissions: jobs: # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c` - # планом на flang — 1052 файл; разбор в задаче 5821. - # СНЯТО 2026-09-17 файлов *.flang = 1052 + # планом на flang — 1081 файл; разбор в задаче 5821. + # СНЯТО 2026-09-17 файлов *.flang = 1081 # # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в diff --git a/docs/README.ru.md b/docs/README.ru.md index 6e35dc490..ee7dbcf1d 100644 --- a/docs/README.ru.md +++ b/docs/README.ru.md @@ -143,9 +143,9 @@ docs/tasks/ открытая и закрытая работа дерева, Внутри `flang/`: [`flang/self/`](../flang/self) — компилятор, 64 файла на flang — лексер, разбор, типы, завершаемость, ядро доказательств и по печати на каждую цель. -[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **51 модуль, 1764 функции и 3745 +[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **52 модуль, 1764 функции и 3745 примеров**, которые прогоняются при каждой проверке: - + списки, строки, числа, множества, словари, JSON, UTF-8, даты, два драйвера баз данных (`postgres`, `sqlite`), сеть (`http`, `tls`, `redis`), криптография, написанная на flang (`aes`, 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 0262a7d5a..40485c82b 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`, - 10122 строк. + 10257 строк. Она переигрывает записи и о новом виде значения не знает ничего. **И встречное число, которое меняет разговор о втором варианте.** Тип `целое` diff --git a/docs/course/11-boundaries.md b/docs/course/11-boundaries.md index ca51b0430..23e1e87c0 100644 --- a/docs/course/11-boundaries.md +++ b/docs/course/11-boundaries.md @@ -66,8 +66,8 @@ draft: false **Полноценной сети нет.** Ходить в сеть язык умеет — есть поручения «Запросить», «Открыть соединение», «Принять соединение», — но это примитивы, а не библиотека. -**Библиотека невелика:** 51 файл, 32 074 строки - +**Библиотека невелика:** 52 файла, 32 091 строки + (`ls flang/stdlib/*.flang | wc -l`, `cat flang/stdlib/*.flang | wc -l`, 10 сентября 2026). Есть списки, строки, числа, словари, деревья, множества, JSON, HTTP-разбор, SHA-256, Base64, UTF-8, дата и время, функции высшего порядка. diff --git a/docs/course/README.md b/docs/course/README.md index 9b8f08853..ee8cc2826 100644 --- a/docs/course/README.md +++ b/docs/course/README.md @@ -171,8 +171,8 @@ docs/course/check.flang: проверено — разбор, типы, заве | размеры напечатанного в восемь целей | `flang emit … --target …`, восемь прогонов подряд; байты — из собственной расшифровки `emit` | | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `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 примеров, 384 файл доказательств | `ls`, `find` | +| 52 файлов и 32 091 строки библиотеки | `ls flang/stdlib/*.flang`, `cat … \| wc -l` | +| 724 заметки, 238 примеров, 412 файл доказательств | `ls`, `find` | | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа | **Чего переснять не удалось, и это надо знать.** diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md index f4630fd0e..8a2b2a54e 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` (10122 строк) +3. **Цену для проверяющей программы.** `checker.c` (10257 строк) о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по образцу ADR-0029. Это оценка, и моя записка её не улучшает. 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ. diff --git a/docs/flang/proof/checker/README.md b/docs/flang/proof/checker/README.md index 56de19740..af5d1a4d3 100644 --- a/docs/flang/proof/checker/README.md +++ b/docs/flang/proof/checker/README.md @@ -145,6 +145,36 @@ bootstrap/flang run-script trust:ceiling каждое `требует` «Г» из этого же исходника) обязано быть столько же, сколько блоков, и ни одно не записано дважды. +18. **Шаг автора `по свойству` постусловия проверяется по существу, а не + привязкой.** Привязка `свойство строка N` обязана указывать на первое + объявление имени в модуле, но одной её мало: сверщик сам находит в теле + функции вызов той функции, которой принадлежит постусловие, строит его + инстанцию (те же проверки, что у хода «факт по свойству»: ребро, арность, + захват имён, оплата `требует` вызванной) и замыкает ею цель — модус-поненсом, + под охраной `если У то … иначе да` той же охраной, либо неотрицательностью по + построению, где инстанция стоит среди известного. Замкнуть не удалось — шаг + остаётся на слове ядра с названной причиной; вывод сверщик не выдумывает. + Постусловие, объявленное с ограничением `таких что`, фактом не берётся. +19. **Свойство из другого файла.** Имя, которого нет в этом исходнике, ищется в + поданном наборе (`--зависимость ИСХОДНИК ЗАПИСЬ`): годится ровно одно + объявление, его модуль ввезён словом `использует` (самим файлом или кем-то из + набора), каждое имя в тексте свойства объявлено в том же модуле, видно по + спискам `только` и не совпадает с именем, объявленным здесь. Запись модуля + сверщик перепроверяет сам, тем же приёмом и с тем же набором, и берёт из неё + только проверенное по существу. Шаг и ход «факт по свойству … подстановка» + читают заголовок, связывания и ограничения утверждения из исходника модуля. + Без набора имя из другого файла — «не берусь», а не «не сошлось». +20. **Поле результата и поле довода в узле тождества.** `результат.поле` — + это поле построенного значения, когда тело ветви — конструктор; `довод.поле` + под образцом случая — имя, связанное на этом поле. Допущение индукции + берётся только по полю того же типа, что и разбираемое значение. + +21. **Свободное утверждение «Т не меньше 0».** Утверждение без функции, чья цель + не говорит о `результат`, проигрывается той же грамматикой неотрицательности, + что тело функции: литерал, `длина`, сумма, произведение на положительный + литерал. Неотрицательным по объявлению считается только имя, связанное `для + всех` типом-отрезком (`неотрицательное`); ограничение `таких что` дна не даёт. + Сверх того: **ни одной непрочитанной строки**. Строка записи, вид которой чекеру не известен, — отказ, а не «ладно». Мутационная проба (3000 порченых записей, зерно 7) показала, что порча полей `вид`, `конец утверждения` и полей diff --git a/docs/fspec/clarifications.md b/docs/fspec/clarifications.md index 449afd6f4..2d3914625 100644 --- a/docs/fspec/clarifications.md +++ b/docs/fspec/clarifications.md @@ -102,8 +102,8 @@ FLANG_EXAMPLE: пример «с промо — тридцать процент ## Перепись по библиотеке — замер 8 сентября 2026 Замер устарел и здесь стоит как запись о прошлом: тогда мастер прогнали по -`flang/stdlib/`, сегодня там 51 файл -, то есть перепись +`flang/stdlib/`, сегодня там 52 файл +, то есть перепись покрывает часть каталога, а не весь. Померено 18 файлов. Восемь померить не удалось, и мастер сказал об этом diff --git a/docs/repository-layout.md b/docs/repository-layout.md index 36d52b937..26f8dbe73 100644 --- a/docs/repository-layout.md +++ b/docs/repository-layout.md @@ -32,9 +32,9 @@ docs/tasks/ the open and closed work of the tree, one file per task Inside `flang/`: [`flang/self/`](../flang/self) is the compiler, 64 files of flang — lexer, parser, types, totality, proof kernel and one printer per target. -[`flang/stdlib/`](../flang/stdlib) is the standard library — **51 modules, 1764 functions and 3745 +[`flang/stdlib/`](../flang/stdlib) is the standard library — **52 modules, 1764 functions and 3745 examples** that run on every check: - + lists, strings, numbers, sets, maps, JSON, UTF-8, dates, two database drivers (`postgres`, `sqlite`), networking (`http`, `tls`, `redis`), a cryptography set written in flang (`aes`, diff --git a/docs/repository-layout.ru.md b/docs/repository-layout.ru.md index 7dc69a900..daa75fb05 100644 --- a/docs/repository-layout.ru.md +++ b/docs/repository-layout.ru.md @@ -31,9 +31,9 @@ docs/tasks/ открытая и закрытая работа дерева, Внутри `flang/`: [`flang/self/`](../flang/self) — компилятор, 64 файлов на flang — лексер, разбор, типы, завершаемость, ядро доказательств и по печати на каждую цель. -[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **51 модуль, 1764 функции и 3745 +[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **52 модуль, 1764 функции и 3745 примеров**, которые прогоняются при каждой проверке: - + списки, строки, числа, множества, словари, JSON, UTF-8, даты, два драйвера баз данных (`postgres`, `sqlite`), сеть (`http`, `tls`, `redis`), криптография, написанная на flang (`aes`, diff --git a/docs/road-to-1-0.md b/docs/road-to-1-0.md index c8f317a9b..e4b04a587 100644 --- a/docs/road-to-1-0.md +++ b/docs/road-to-1-0.md @@ -155,7 +155,7 @@ Homebrew с тем, что собрал сам конвейер выпуска; ## 6. Полноценная история пакетов и модулей **Что уже есть.** `scripts/registry-example/` — образец описания пакета. -`flang/stdlib` — 51 файл, 32 074 строки. +`flang/stdlib` — 52 файла, 32 091 строки. **Чего нет.** Почти всего: установки, разрешения версий, замыкания зависимостей. diff --git a/docs/site/index.md b/docs/site/index.md index 4a6c7ad62..c5c545306 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 **288** such theorems in the repository, 55 of them in the +tactics. There are **303** 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 2e07f6885..6ac1ea0df 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, а -не как скрипт из тактик. Таких теорем в дереве языка **288**, из них **55** в +не как скрипт из тактик. Таких теорем в дереве языка **303**, из них **55** в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`, сумма по `awk`). diff --git a/docs/site/proofs.md b/docs/site/proofs.md index ec42606ca..c23f62138 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 288 such theorems in the repository, 55 of +it searches for nothing. There are 303 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 776c09e51..f57021269 100644 --- a/docs/site/proofs.ru.md +++ b/docs/site/proofs.ru.md @@ -64,7 +64,7 @@ руками**, как в Coq или Isabelle. `теорема` пишется по шагам: `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно доказано`. Это читается как Isar в Isabelle, и prover проверяет каждый шаг, -ничего не ища. В дереве языка таких теорем 288, из них 55 в стандартной +ничего не ища. В дереве языка таких теорем 303, из них 55 в стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Большинству постусловий теорема не нужна: отчёт о доказательствах показывает отдельным числом, сколько доказано **без написанного доказательства**. diff --git a/docs/site/stdlib.md b/docs/site/stdlib.md index 9847031cf..e40c9450c 100644 --- a/docs/site/stdlib.md +++ b/docs/site/stdlib.md @@ -2,7 +2,7 @@ The standard library is written in flang and is checked the same way as your program: types, termination, unit tests (`пример`) and postconditions. It has - 51 modules, one file + 52 modules, one file each in `flang/stdlib/`. This page lists every module and every function in it. ## Which module for which task diff --git a/docs/site/stdlib.ru.md b/docs/site/stdlib.ru.md index 54139ae50..67ecd300f 100644 --- a/docs/site/stdlib.ru.md +++ b/docs/site/stdlib.ru.md @@ -2,7 +2,7 @@ Стандартная библиотека написана на flang и проверяется так же, как ваша программа: типы, завершаемость, unit-тесты (`пример`) и постусловия. Модулей в -ней 51, по файлу на +ней 52, по файлу на модуль в `flang/stdlib/`. На этой странице — каждый модуль и каждая его функция. ## Какой модуль под какую задачу diff --git a/docs/tasks/1400-fmath-is-a-proof-library-about-programs.md b/docs/tasks/1400-fmath-is-a-proof-library-about-programs.md index 6db6a7819..5dad36a63 100644 --- a/docs/tasks/1400-fmath-is-a-proof-library-about-programs.md +++ b/docs/tasks/1400-fmath-is-a-proof-library-about-programs.md @@ -1,10 +1,10 @@ --- номер: 1400 заголовок: Библиотеки доказательств о программах «fmath» в дереве нет -статус: свободна +статус: в работе — первые четыре утверждения лежат в flang/stdlib/fmath.flang, ядро доказывает все четыре, независимая проверяющая программа переигрывает все четыре и ссылку на них из другого файла приоритет: P3 -исполнитель: — -ветка: — +исполнитель: a +ветка: a/1400-fmath-first-statements команда: любая карта: Куда идём рядом: 6134, 6202, 6203 @@ -110,3 +110,57 @@ flang/proof/checker/сверщик <файл библиотеки> <запись Правки под `flang/self/` доезжают до двоичного только пересборкой семени (bootstrap regeneration); проверяющая программа собирается отдельно, своим `flang/proof/checker/Makefile`. + +## Первые утверждения в дереве + +Модуль `flang/stdlib/fmath.flang` («Fmath»): четыре утверждения о всех значениях своих +типов — длина любого списка чисел и любой строки не меньше нуля, сумма двух +`неотрицательное` не меньше нуля (утверждение 2 записки), сумма длин двух строк не меньше +нуля. Ядро 0.7.23: «утверждений 4: доказано 4». Проверяющая программа на его записи — +код 0, «ПРОВЕРЕНО». + +Ссылка из программы разработчика — +`flang/proof/checker/tests/families/fmath/scores.flang`: `использует «Fmath»`, две +теоремы `по свойству «длина любого списка неотрицательна»` и `по свойству «сумма длин +двух строк неотрицательна»`. Ядро — код 0. Проверяющая программа с поданным модулем +(`--зависимость flang/stdlib/fmath.flang <запись модуля>`) — код 0, «Шагов по свойству +проверено по существу 2»; без модуля — код 3 «не берусь», а не ложь. Как она +проверяет ссылку между файлами — README проверяющей программы, п. 19: ищет утверждение в +исходнике поданного модуля, сама перепроверяет его запись и берёт только проверенное. + +Что для этого понадобилось в проверяющей программе (+11 строк кода, потолок 7938 → +7949): свободное утверждение «Т не меньше 0» без `результат` проигрывается той же +грамматикой неотрицательности, что тело функции, а дно дают только имена типа-отрезка +(README, п. 21). Без этого утверждение 2 записки и сумма длин оставались на слове ядра. +Подделки — строки раздела «1400» в `flang/proof/checker/tests/probes.tsv`: сумма с `число` без дна, разность длин и +ограничение `таких что` на одном слагаемом получают 3, а копия программы, которая +считает дном любое связанное имя, принимает две из них кодом 0. + +Из десяти утверждений записки сегодня (ядро 0.7.23, проверяющая программа этой ветки): + +| № | ядро | проверяющая программа | +|---|---|---| +| 1, 2 | доказано | проверено | +| 3, 4, 9, 10 | доказано | на слове ядра: в записи нет ни хода, ни вывода | +| 5, 6, 7 | FLANG_PARSE: квантор над функцией `у: функция из числа в признак` не разбирается | — | +| 8 | FLANG_PARSE: составное ограничение `таких что (…) и притом (…)` | — | + +Чего не хватает, чтобы разработчик ссылался на любое утверждение библиотеки: + +1. **Печать ходов у свободного утверждения** (`flang/self/zapis.flang`, «Ходы цели + утверждения записи»): законы меры, разбор и порядок, как у постусловий. Пока их + нет, утверждения 3, 4, 9, 10 уходят на слово ядра, а ссылка на них — тоже. Замер: + ходы `переписать формой … законом «Мера прибавления»` / `закрыть тождеством`, + дописанные в запись утверждения «приписывание удлиняет на один» руками, проверяющая + программа принимает кодом 0, а с `плюс 2` — кодом 1. +2. **Квантор над функцией и составное ограничение** в разборе — для утверждений 5–8. +3. **Запись называет файл утверждения.** Шаг теоремы печатает `свойство строка 0`, ход — + номер строки чужого файла без имени файла (задача 5583). Проверяющая программа + обходится поиском по поданному модулю (ровно одно объявление, модуль ввезён), но + тёзка в двух поданных модулях даёт «не берусь», а не проверку. +4. **Ссылка на постусловие с ограничением.** Ядро берёт `для всех н таких что … + обеспечивает` фактом, не снимая ограничения в точке вызова, и доказывает ложное + утверждение (задача 4573, раздел «Ядро: постусловие с ограничением…»). Пока это не + исправлено, утверждения библиотеки с `таких что` цитировать нельзя. +5. **Модуль в доле.** Запись `fmath` лежит пробой в `tests/families/fmath/`, в набор доли + библиотека не входит (задача 4573). 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 beb5b5ba3..fc8c99f6e 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 +статус: в работе — с набором кодов 1 на библиотеке 0 из 49; вся библиотека снята заново, проверено 1665 / 3671 (45,36 %), две дыры проверяющей программы закрыты, остальное ранжировано по причинам приоритет: P1 исполнитель: a -ветка: a/4573-checker-reads-module-types-and-dependency-sets +ветка: a/4573-standard-library-verified-by-the-checker команда: первая карта: Где именно упирается доказатель рядом: 9337, 4416, 6341, 2718 @@ -164,3 +164,133 @@ regeneration); правка на C её не требует. приняты (код 0 или 3), доля 1682 / 3693 = 45,55 %; прежним прогоном без набора — отвергнуто 23, доля 791 / 4351 = 18,18 %. +## Библиотека целиком: замер, причины отказов, правки сверщика + +Записи 49 модулей печатает ядро 0.7.23 (`bootstrap/flang check flang/stdlib/<м>.flang +--proof --record R/<м>.record`, не больше четырёх разом, предел 3600 с): у 42 модулей +ядро отвечает 0, у 7 — 3 (`aes`, `scram`, `sqlite`, `tls`, `tls-handshake`, +`trust-store`, `x25519`); `kdf` — код 1 без записи (FLANG_PROOF_STEP, уже в +`scripts/ledgers/stdlib-proof-debt.tsv`), `datetime` — не уложился в 3600 с. Доля — +`sh flang/proof/corpus-share.sh --набор <каталог записей> --проигрыванием`; набор +зависимостей прибор подаёт сам. + +В 49 записях 1720 функций, 3349 утверждений: ядро доказало 2065, условно — 38, без +вердикта — 1246; блоков тотальности 1199. Сверщик на всех 49 отвечает 3: лжи нет, но у +каждой записи есть места на слове ядра. + +### Доля по шагам + +| шаг | проверено / мест | доля | +|---|---:|---:| +| сверщик над `a/4573-checker-reads-module-types-and-dependency-sets` | 1684 / 3693 | 45,60 % | +| шаг «по свойству» проверяется по существу, свойство из другого файла | 1643 / 3671 | 44,76 % | +| поле довода и поле результата в узле тождества | 1665 / 3671 | 45,36 % | + +Доля упала, и это поправка счёта, а не потеря: 41 шаг «по свойству» сверщик +засчитывал проверенным одной привязкой строки (дыра 1 ниже), а 22 места считались +дважды — шаг «проверенным», а его утверждение с вердиктом «доказано при условии» — +ещё одним местом на слове ядра. Поле довода дало +22 места (`dictionary` 4, +`hashmap` 4, `http` 4, `json` 8, `postgres` 2). + +### Причины, ранжированные по числу строк «не взялся» + +| причина | строк | чья работа | +|---|---:|---| +| утверждение доказано ядром, а в записи нет ни хода, ни вывода («по объявлению да/нет») | 1304 | печать записи | +| посылка узла индукции сведена правилом, ходов 0 | 314 | печать записи | +| узел вердикта вне приёма сверщика (цель-дизъюнкция у типов-состояний — 105, тождество и порядок на носителях вне приёма — 45, прочее) | 216 | сверщик | +| булева цель случая не замкнулась | 43 | сверщик | +| шаг «по свойству» постусловия, которое само на слове ядра | 41 | следствие первой строки | +| вердикт «доказано при условии» | 38 | ядро (опора без теоремы) | +| тело случая длиннее пяти строк | 19 | сверщик | +| свойство из другого файла не проверено в записи своего модуля | 18 | следствие первой строки | +| стороны тождества не сошлись / порядок не выведен | 17 / 17 | сверщик | +| свёртка: начало или виток | 11 | сверщик | + +Утверждения первой строки по правилу ядра (снято по записям, утверждение доказано, +теоремы, ходов и вывода нет): «разбор цели по условию» 603, «разбор случаев по +внутреннему условию цели» 483, «тождество после переписки допущением» 321, «цель +есть допущение» 77, «вычисление замкнутой цели» 56, «порядок по построению» 40, +«равенство, решённое счётом замкнутых частей» 32, прочие 56; всего 1668. + +### Что нужно от печати записи (`flang/self/zapis.flang`, партия печати) + +1. **Пределы планировщика.** «Тело планировщику по силам записи» отказывает телу + длиннее 300 знаков вместе с утверждением, «Цепочка разбора записи» даёт + планировщику горючее 16. Копия двоичного вне дерева с пределом 100000 и горючим 64 + (правка двух чисел в `bootstrap/compiler_flang.c`): блоков ходов 347 → 385; + на 47 модулях без `tree` и `utf8` проверено 1625 / 3500 → 1666 / 3500 (+41 место). + `tree` под этой копией не уложился в 3600 с. `utf8` стал кодом 1: планировщик + печатает `вычислить ⟨( длина [… «Целая часть» от код …] ) не больше 4⟩`, а терм с + вызовом не замкнут — «Ход вычисления стороны записи» обязан брать только + замкнутый терм. Без этой оговорки снимать пределы нельзя. +2. **Свободное утверждение-тождество с законом меры.** «Ходы цели утверждения + записи» знает соседей, нейтральный ноль и замкнутый счёт, но не законы «Мера + прибавления» и «Мера склейки», которые у постусловий печатает «Ходы длины + постусловия записи». Ходы `переписать формой ⟨длина (приписать э к л)⟩ = + ⟨(длина л) плюс 1⟩ законом «Мера прибавления»` / `закрыть тождеством`, + дописанные в запись руками, сверщик принимает кодом 0; та же запись с `плюс 2` — + код 1. +3. **Остальные 1668** — правила, для которых печатного плана нет вовсе + («вычисление замкнутой цели», «равенство, решённое счётом», «порядок по + построению»), и формы тела, на которых план не строится (`разбор`, `свёртка`, + вызовы чужих функций в цели). Это работа задачи 6132 (ядро печатает вывод факта) + и 9616. + +### Две дыры сверщика, закрытые этой веткой (обе — код 0 на подделке) + +1. **Шаг `по свойству «П»` постусловия принимался привязкой.** Подделка: тело + `(0 минус 5) плюс (0 умножить на («Мера» от элементы))`, постусловие `результат + не меньше 0`, теорема `по свойству «мера неотрицательна»` — ядро отказывает + (FLANG_PROOF_STEP), сверщик отвечал 0. Теперь шаг проигрывается (README + сверщика, п. 18). В корпусе доли так были засчитаны 4 шага (`body-forms` 1, + `honest-modus-ponens-by-guard` 3) — все четыре теперь проигрываются по существу, + доля корпуса 650 / 650 не сдвинулась. +2. **Узел тождества переписывал цель самой собой.** `результат.поле` не + подставлялось телом ветви, а допущение индукции бралось по каждому имени образца, + и для нерекурсивного поля им оказывалась сама цель. Подделка `результат.с0 равен + тройка.с2` при теле `вариант «Тройка» с с0 равным п1 …` уходила кодом 0. Теперь + поле результата — поле построенного значения, допущение — только по рекурсивному + полю (README, п. 20). + +Свойство из другого файла (README, п. 19): 18 шагов библиотеки со `свойство строка 0` +читаются из набора; засчитывается лишь проверенное по существу в записи модуля. +Сегодня из 18 не засчитан ни один: цитируемые постусловия сами без вердикта либо на +слове ядра. Зато честная запись больше не зовётся ложью: на пробах семьи `citation` +программа, ссылающаяся на утверждение другого файла, без набора — 3, с набором — 0. + +### Пробы + +Строки разделов «4573: шаг «по свойству» по существу…» (17) и «4573: поле результата +и поле довода…» (5) в `flang/proof/checker/tests/probes.tsv`; исходники и записи — в +семьях `families/citation/` и `families/field-projection/`. Подделки — исходник правится, +шапка записи переподписывается. Копии сверщика без каждой части (все 22 строки под +каждой): без переигрывания шага — подделка с чужим телом 0; без перепроверки записи +модуля — две подделки 0; без проверки имён модуля — подделка с тёзкой 0; без «ровно +одно объявление» — тёзки в двух модулях 0; без «модуль ввезён» — модуль, которого +никто не ввозит, 0; без «не берусь» — честная запись без набора 1; без поиска в +наборе — честная с набором 3; без неотрицательности с фактом — `body-forms` 3. +`bootstrap/flang run-script checker:check` — «сошлось всё». Ответы на 533 прежние записи дерева — байт в байт как у сверщика +без этой правки. Потолок `checker-code-lines` 7815 → 7938. + +### Ядро: постусловие с ограничением берётся фактом без ограничения + +`flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang`: +`для всех н таких что н не меньше 0 обеспечивает «сдвиг неотрицателен» результат не +меньше 0` у функции, возвращающей `н`, и теорема другой функции (тело `«Сдвиг» от +н`, без ограничения) `по свойству «сдвиг неотрицателен»`. Ядро 0.7.23 с `--strict`: +«ДОКАЗАНО, утверждений 2: доказано 2»; `flang run … «Второй сдвиг» -3` отвечает +«нарушено свойство «сдвиг неотрицателен»». Ложное утверждение доказано: ссылка на +ограниченное постусловие не требует снять ограничение в точке вызова (у `требует` +это делает FLANG_PRECONDITION_CALL). Сверщик на этой записи — 3. Правка — в +`flang/self` (партия печати), задача отдельная. + +### Что нужно, чтобы библиотека вошла в главное число + +Главное число — доля проверенного на 86 записях корпуса, порог 100 %. Библиотека +сегодня 1665 / 3671, на слове ядра 1896 мест и 110 сняты счётом. Нужно: +печать ходов у 1668 утверждений и 314 посылок (пункты выше и задачи 6132, 9616); +приём узлов-дизъюнкций у типов-состояний и тел длиннее пяти строк в сверщике; +записи `kdf` (ядро — код 1) и `datetime` (ядро не укладывается в час); снять 38 +вердиктов «доказано при условии» теоремами у опор. Пока этого нет, включить +библиотеку в набор доли значит добавить в знаменатель главного числа 2006 непроверенных мест. diff --git a/docs/tasks/5583-a-proof-refers-to-a-statement-proved-in-another-file.md b/docs/tasks/5583-a-proof-refers-to-a-statement-proved-in-another-file.md index 2ab5eb779..541877a19 100644 --- a/docs/tasks/5583-a-proof-refers-to-a-statement-proved-in-another-file.md +++ b/docs/tasks/5583-a-proof-refers-to-a-statement-proved-in-another-file.md @@ -1,10 +1,10 @@ --- номер: 5583 заголовок: Запись доказательства со ссылкой на утверждение из другого файла независимая проверка отвергает -статус: свободна +статус: в работе приоритет: P2 -исполнитель: — -ветка: — +исполнитель: a +ветка: a/4573-standard-library-verified-by-the-checker команда: вторая карта: Сколько доказано на самом деле рядом: — diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 7ac0601e5..2bc1cf7f6 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 790 | 0 | 0 | +| C | 37 | 870 925 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | | HTML | 7 | 1 263 | 0 | 0 | diff --git a/flang/proof/checker/checker.c b/flang/proof/checker/checker.c index 7b8fd133f..c427bae14 100644 --- a/flang/proof/checker/checker.c +++ b/flang/proof/checker/checker.c @@ -974,6 +974,7 @@ typedef struct { Сп цели, дано, беды, не_взялся; long хо static long номер_свойства(Сп строки, const char *имя); static int среди(Сп v, const char *имя); +static Сп свойство_набора(Сп строки, const char *имя, int *чужое); /* 4416: ПЕРВАЯ БЕДА ГАСИТ ПРОГОН — И НА ЭТОМ ЖАЛОБЫ КОНЧАЮТСЯ. Прежде гашение `идёт` тянуло за собой две ЛОЖНЫЕ: следующий ход получал «стоит до «ход цель»», @@ -1309,13 +1310,13 @@ static int снято_в_точке(Прогон *p, Обст *o, const char *и обязано быть снято в точке хода. Цель и ограничения сверщик читает из исходника сам, из записи берутся только термы. Сторож круга (оба уровня) уже пройден в `ход_факта_свойством`: реестр держит и утверждения. */ -static void факт_утверждения(Прогон *p, const char *строка, Обст *o, const char *имя_п, long где) { +static void факт_утверждения(Прогон *p, const char *строка, Обст *o, Сп исх, const char *имя_п, long где) { Сп имена = ПУСТО, пн = ПУСТО, пт = ПУСТО, огр = ПУСТО; int i, j; long k; - char *инст = терм(из_высказывания(o->строки, где, NULL, &имена)); + char *инст = терм(из_высказывания(исх, где, NULL, &имена)); const char *q = strstr(строка, " подстановка ") + strlen(" подстановка "), *e; - if (строка_высказывания(o->строки, fmt("утверждение «%s»", имя_п)) != где) { + if (строка_высказывания(исх, fmt("утверждение «%s»", имя_п)) != где) { беда_прогона(p, fmt("факт по свойству «%s»: строка %ld исходника — не заголовок «утверждение «%s»»", имя_п, где, имя_п)); return; } - if (номер_свойства(o->строки, имя_п)) { + if (номер_свойства(исх, имя_п)) { беда_прогона(p, fmt("факт по свойству: имя «%s» носят и постусловие, и утверждение — назовите одно", имя_п)); return; } while (*q == ' ') q++; while (начинается(q, "«") && (e = strstr(q, "» ⟨")) != NULL && strstr(e, "⟩")) { @@ -1334,9 +1335,9 @@ static void факт_утверждения(Прогон *p, const char *стр if (есть_терм(терм(пт.e[i]), имена.e[j])) { беда_прогона(p, fmt("факт по свойству «%s»: подстановка захватила бы имя «%s» — инстанции нет", имя_п, имена.e[j])); return; } } - for (k = где + 1; k <= o->строки.n && начинается(часть(o->строки, k), " "); k++) - if (содержит(часть(o->строки, k), " таких что ")) - добавить(&огр, хвост_после(как_читает_язык(обрезать(часть(o->строки, k))), " таких что ")); + for (k = где + 1; k <= исх.n && начинается(часть(исх, k), " "); k++) + if (содержит(часть(исх, k), " таких что ")) + добавить(&огр, хвост_после(как_читает_язык(обрезать(часть(исх, k))), " таких что ")); for (i = 0; i < имена.n; i++) инст = вставить_вместо(инст, имена.e[i], терм(пт.e[i])); for (j = 0; j < огр.n; j++) { char *ог = терм(огр.e[j]); @@ -1359,7 +1360,7 @@ static void ход_факта_свойством(Прогон *p, const char *с long где = номер_после(строка, "строка "); char *вызов = терм(в_уголках(строка, 1)); char *имя_г = в_ёлочках(вызов, 1); - char *в_исх, *тело_п; Сп param, арги, треб_г; int i, j, раньше = 0, подст = содержит(строка, " подстановка "); + char *в_исх, *тело_п; Сп param, арги, треб_г, исх = o->строки; int i, j, раньше = 0, чужое = 0, подст = содержит(строка, " подстановка "); if (!*имя_п || где < 1 || (!*имя_г && !подст)) { беда_прогона(p, fmt("факт по свойству: ход «%s» неполон — нужны «имя-П», «строка N» и «вызов ⟨«Г» от …⟩»", строка)); return; } @@ -1374,6 +1375,10 @@ static void ход_факта_свойством(Прогон *p, const char *с `o->доказанные` держит имена постусловий, проверенных до текущего (порядок записи линеен). Нет в реестре — рекурсия начаться не может (проект §3). */ for (i = 0; i < o->доказанные.n; i++) if (strcmp(o->доказанные.e[i], имя_п) == 0) { раньше = 1; break; } + if (!раньше) { + Сп из_набора = свойство_набора(o->строки, имя_п, &чужое); + if (из_набора.n) { исх = из_набора; раньше = 1; } + } if (!раньше) { /* 4416: ДВА СЛУЧАЯ, И ОНИ РАЗНЫЕ. Имени нет в реестре проверенного ПО СУЩЕСТВУ по двум несхожим причинам. Либо запись вовсе не числит его доказанным (нет @@ -1382,27 +1387,29 @@ static void ход_факта_свойством(Прогон *p, const char *с переиграл, — тогда по собственной доктрине трёх исходов сверщику положено сказать «не взялся»: место на слове ядра, код 3. */ if (среди(o->объявленные, имя_п)) не_взялся_прогона(p, fmt("факт по свойству «%s»: утверждение, но оно не проверено по существу раньше этой цели", имя_п)); + else if (чужое) не_взялся_прогона(p, fmt("факт по свойству «%s»: в этом исходнике его нет, а файл ввозит модули — в поданном наборе оно либо не найдено ровно одно, либо не проверено по существу", имя_п)); else беда_прогона(p, fmt("факт по свойству «%s»: постусловие не доказано РАНЬШЕ этой цели — фактом брать нельзя (круг или обратный порядок)", имя_п)); return; } - if (подст) { факт_утверждения(p, строка, o, имя_п, где); return; } /* К3c: «И» — утверждение */ + if (подст) { факт_утверждения(p, строка, o, исх, имя_п, где); return; } /* К3c: «И» — утверждение */ /* (а) АТРИБУЦИЯ ПО РЕБРУ: строка N исходника несёт «обеспечивает «имя-П»», лежит в блоке ИМЕННО той «Г», что вызвана в узле (не первой одноимённой у чужой функции), и N — первое по файлу объявление (как ищет само правило, 3455). */ - в_исх = строка_по_номеру(o->строки, где); + в_исх = строка_по_номеру(исх, где); + if (начинается(в_исх, "для всех ") && !содержит(в_исх, " таких что ") && strstr(в_исх, " обеспечивает «")) в_исх = strstr(в_исх, " обеспечивает «") + 1; if (!начинается(в_исх, fmt("обеспечивает «%s» ", имя_п))) { беда_прогона(p, fmt("факт по свойству «%s»: строка %ld исходника не несёт «обеспечивает «%s»» (стоит «%s»)", имя_п, где, имя_п, в_исх)); return; } - if (strcmp(хозяин_строки(o->строки, где), имя_г) != 0) { + if (strcmp(хозяин_строки(исх, где), имя_г) != 0) { беда_прогона(p, fmt("факт по свойству «%s»: строка %ld стоит в функции «%s», а вызвана «%s» — привязка НЕ ПО РЕБРУ", - имя_п, где, хозяин_строки(o->строки, где), имя_г)); return; + имя_п, где, хозяин_строки(исх, где), имя_г)); return; } - if (номер_свойства(o->строки, имя_п) != где) { + if (номер_свойства(исх, имя_п) != где) { беда_прогона(p, fmt("факт по свойству «%s»: строка %ld — не первое объявление постусловия (первое — %ld)", - имя_п, где, номер_свойства(o->строки, имя_п))); return; + имя_п, где, номер_свойства(исх, имя_п))); return; } тело_п = цель_обещанная(обрезать(хвост_после(в_исх, fmt("обеспечивает «%s» ", имя_п)))); /* К7: У[м:=Т] */ - param = доводы_функции(o->строки, имя_г).голые; + param = доводы_функции(исх, имя_г).голые; арги = доводы_вызова(хвост_после(вызов, fmt("«%s» от ", имя_г))); if (param.n != арги.n) { беда_прогона(p, fmt("факт по свойству «%s»: у «%s» параметров %d, а в вызове аргументов %d — арность не совпала", @@ -1429,7 +1436,7 @@ static void ход_факта_свойством(Прогон *p, const char *с и факт ляжет под ту же охрану; цель БЕЗ охраны не снимает ничего; (3) ДОКАЗАННЫЙ ФАКТ `дано` — посчитанный самим сверщиком, не взятый из записи. Не снято ничем — факт НЕ берётся: соундность прежде полноты. */ - треб_г = все_требования_функции(o->строки, имя_г); + треб_г = все_требования_функции(исх, имя_г); for (i = 0; i < треб_г.n; i++) { char *п_инст = формула_требования(треб_г.e[i]); for (j = 0; j < param.n; j++) п_инст = вставить_вместо(п_инст, param.e[j], терм(арги.e[j])); @@ -3357,17 +3364,21 @@ static long номер_свойства(Сп строки, const char *имя) { она ищется среди доводов функции ТОГО ЖЕ типа, знак в знак, а довод, чьё имя совпало с ещё не подставленным связанным, отбрасывается (захват). */ static int есть_связыватель(const char *t); -static int шаг_утверждением(Сверка *s, Сп строки, const char *имя_т, const char *имя_п, +static int разрез_словом(const char *t, const char *чем, char **лево, char **право); +static int неотрицательно_algebra(const char *т_сырой, const char *чья, Сп bound, + Сп строки, int глубина, char **почему); +static int шаг_утверждением(Сверка *s, Сп строки, Сп исх, const char *имя_т, const char *имя_п, long p, long ут, const char *чья, const char *цель) { Сп имена = ПУСТО; Доводы д = доводы_функции(строки, чья); - char *ц_у = терм(из_высказывания(строки, ут, NULL, &имена)), *ц_ш, *тело = (char *)""; + char *ц_у = терм(из_высказывания(исх, ут, NULL, &имена)), *ц_ш, *тело = (char *)""; const char *почему; long a, b, k, всего = 1, c; int i, j, раньше = 0, огр = 0, читается; если_не(s, p == ут, fmt("теорема «%s»: свойство «%s» привязано к строке %ld, а заголовок утверждения «%s» — строка %ld", имя_т, имя_п, p, имя_п, ут)); if (p != ут) return 0; for (i = 0; i < s->доказанные_свойства.n; i++) раньше |= strcmp(s->доказанные_свойства.e[i], имя_п) == 0; - for (k = ут + 1; k <= строки.n && начинается(часть(строки, k), " "); k++) огр |= содержит(часть(строки, k), " таких что "); + раньше |= исх.e != строки.e; + for (k = ут + 1; k <= исх.n && начинается(часть(исх, k), " "); k++) огр |= содержит(часть(исх, k), " таких что "); a = блок_функции(строки, чья, &b); if (a > 0) тело = тело_функции_текст(строки, a, b); ц_ш = терм(вставить_вместо(терм(цель), "результат", тело)); @@ -3377,7 +3388,7 @@ static int шаг_утверждением(Сверка *s, Сп строки, c char *инст = ц_у; long r = c; int годен = 1; for (i = 0; i < имена.n; i++, r /= д.имена.n) { char *довод = голо(д.имена.e[r % д.имена.n]); - годен &= *довод && strcmp(обрезать(из_высказывания(строки, ут, имена.e[i], NULL)), + годен &= *довод && strcmp(обрезать(из_высказывания(исх, ут, имена.e[i], NULL)), обрезать(д.типы.e[r % д.имена.n])) == 0; for (j = i + 1; j < имена.n; j++) годен &= strcmp(довод, имена.e[j]) != 0; инст = вставить_вместо(инст, имена.e[i], довод); @@ -3392,10 +3403,39 @@ static int шаг_утверждением(Сверка *s, Сп строки, c имя_т, имя_п, почему)); return 0; } +static int шаг_постусловием(Сверка *s, Сп строки, Сп исх, const char *имя_т, const char *имя_п, + long где, const char *чья, const char *цель) { + char *г = хозяин_строки(исх, где), *зов = fmt("«%s» от ", г), *тело = (char *)"", *ц, *у, *в_то, *в_иначе, *л, *п, *лф, *пф, *почему = (char *)""; + const char *q; long a, b; Обст o; + if ((a = блок_функции(строки, чья, &b)) > 0) тело = тело_функции_текст(строки, a, b); + memset(&o, 0, sizeof o); o.строки = строки; o.свои = ПУСТО; o.функция = (char *)чья; o.цель = терм(цель); + o.тип = o.по = o.хвост = (char *)""; o.обяз = (char *)имя_т; o.доказанные = s->доказанные_свойства; o.объявленные = s->объявленные_доказанными; + ц = терм(вставить_вместо(терм(цель), "результат", в_скобки(терм(тело)))); + for (q = *тело && *г && !есть_связыватель(ц) ? strstr(тело, зов) : NULL; q; q = strstr(q + 1, зов)) { + Сп арги = доводы_вызова(q + strlen(зов)), одно = ПУСТО; Прогон p; + memset(&p, 0, sizeof p); добавить(&p.цели, ц); p.идёт = 1; p.посл_факт = (char *)""; + ход_факта_свойством(&p, fmt("ход 1 факт по свойству «%s» строка %ld вызов ⟨«%s» от %s⟩", имя_п, где, г, соединить(арги, " и ")), &o); + if (p.беды.n || p.не_взялся.n || !*p.посл_факт) continue; + if (разрез_словом(ужать(ц), " не меньше ", &л, &п) && strcmp(ужать(п), "0") == 0 && + разрез_словом(ужать(p.посл_факт), " не меньше ", &лф, &пф) && strcmp(ужать(пф), "0") == 0) { + добавить(&одно, ужать(лф)); + if (неотрицательно_algebra(л, чья, одно, строки, 0, &почему)) return 1; + } + закрыть_по_свойству(&p, разрез_выбора_цепочкой(ц, &у, &в_то, &в_иначе) && strcmp(ужать(в_иначе), "да") == 0 + ? fmt("ход 2 закрыть по свойству по охране ⟨%s⟩", у) : (char *)"ход 2 закрыть по свойству", ц); + if (!p.беды.n && !p.цели.n) return 1; + } + добавить(&s->не_взялся, fmt("теорема «%s»: шаг «по свойству «%s»» привязан верно, но вывод цели из постусловия сверщик не переиграл; место на слове ядра", имя_т, имя_п)); + return 0; +} static int сверить_шаг_свойством(Сверка *s, const char *ш, Сп строки, const char *имя_т, const char *чья, const char *цель) { char *имя_п = в_ёлочках(шаг_словами(ш), 1); long p = номер_после(ш, МЕТКА_СВОЙСТВА), настоящий; + if (p < 1) { int чужое = 0; Сп исх = свойство_набора(строки, имя_п, &чужое); + if (исх.n) { long ут = строка_высказывания(исх, fmt("утверждение «%s»", имя_п)); + return ут ? шаг_утверждением(s, строки, исх, имя_т, имя_п, ут, ут, чья, цель) + : шаг_постусловием(s, строки, исх, имя_т, имя_п, номер_свойства(исх, имя_п), чья, цель); } } /* Своё `добавить`, а не `не_взялся`: тот зашивает в текст слова «шаг „по примеру“», а шаг здесь другой. */ if (p < 1) { s->без_привязки++; @@ -3407,7 +3447,7 @@ static int сверить_шаг_свойством(Сверка *s, const char { long ут = строка_высказывания(строки, fmt("утверждение «%s»", имя_п)); если_не(s, !(ут && настоящий), fmt("теорема «%s»: имя «%s» носят и постусловие, и утверждение — назовите одно", имя_т, имя_п)); - if (ут) return настоящий ? 0 : шаг_утверждением(s, строки, имя_т, имя_п, p, ут, чья, цель); } + if (ут) return настоящий ? 0 : шаг_утверждением(s, строки, строки, имя_т, имя_п, p, ут, чья, цель); } если_не(s, настоящий >= 1, fmt("теорема «%s»: свойство «%s» привязано к строке %ld, а объявления «обеспечивает «%s»»" " в исходнике нет вовсе", @@ -3417,7 +3457,7 @@ static int сверить_шаг_свойством(Сверка *s, const char fmt("теорема «%s»: свойство «%s» привязано к строке %ld, а первое (и единственно" " законное — как ищет само правило) его объявление в модуле — строка %ld", имя_т, имя_п, p, настоящий)); - return p == настоящий; + return p == настоящий && шаг_постусловием(s, строки, строки, имя_т, имя_п, p, чья, цель); } static int неотрицательно_algebra(const char *т_сырой, const char *чья, Сп bound, @@ -3760,7 +3800,7 @@ static int разрез_словом(const char *t, const char *чем, char ** static int разрез_равенства(const char *t, char **лево, char **право); static int тождество_случая(Сп строки, const char *чья, const char *цель, const char *тип, const char *по, const char *тело, - const char *образец, Сп связанные, char **почему); + const char *образец, const char *хвост_сл, Сп связанные, char **почему); static int охраной_случая(Сп строки, const char *чья, const char *цель, const char *по, const char *тело, const char *образец, char **почему); @@ -4225,7 +4265,7 @@ static int проиграть_узел_algebra(Сверка *s, Сп строк if (!*образец) return не_проигран(s, имя, fmt("образец случая «%s» сверщику незнаком", вариант)); if (!тождество_случая(строки, чья, цель, тип, в_ёлочках(принцип, 2), тело, - образец, bound_имена_случая(хв_сл), &почему)) + образец, хв_сл, bound_имена_случая(хв_сл), &почему)) return не_проигран(s, имя, fmt("случай «%s»: %s", вариант, почему)); } else if (д.пор) { char *хв_сл = слова_после(как_читает_язык(часть(строки, ци)), 1); @@ -4852,23 +4892,48 @@ static int равенство_правилами(const char *сл, const char * return 0; } +static char *с_результатом(const char *цель, const char *тело) { + Сп им, тр, слова = разделить(терм(цель), " "); int i, k, конструктор; + конструктор = (начинается(ужать(тело), "запись «") || начинается(ужать(тело), "вариант «")) && поля(ужать(тело), " равным ", &им, &тр); + for (i = 0; конструктор && i < слова.n; i++) { + char *поле = начинается(слова.e[i], "результат.") ? слова.e[i] + strlen("результат.") : (char *)""; + if (*в_ёлочках(поле, 1)) поле = в_ёлочках(поле, 1); + for (k = 0; *поле && k < им.n; k++) if (strcmp(им.e[k], поле) == 0) слова.e[i] = в_скобки(тр.e[k]); + } + return вставить_вместо(соединить(слова, " "), "результат", тело); +} +static int связанное_рекурсивно(Сп строки, const char *тип, const char *хвост_сл, const char *имя) { + Сп св = bound_имена_случая(хвост_сл), им, тр; int k; + if (!начинается(хвост_сл, "вариант «")) return св.n == 2 && strcmp(св.e[1], имя) == 0; + for (k = 0; поля(заменить(хвост_сл, " как ", " равным "), " равным ", &им, &тр) && k < им.n; k++) + if (strcmp(тр.e[k], имя) == 0) { + Сп ч = разделить(справа_от(строка_варианта_типа(строки, тип, в_ёлочках(хвост_сл, 1)), "содержит"), ","); int j; + for (j = 0; j < ч.n; j++) { + Сп pr = разделить(ч.e[j], ":"); + if (strcmp(обрезать(часть(pr, 1)), им.e[k]) == 0) return strcmp(обрезать(часть(pr, 2)), fmt("«%s»", тип)) == 0; + } + } + return 0; +} static int тождество_случая(Сп строки, const char *чья, const char *цель, const char *тип, const char *по, const char *тело, - const char *образец, Сп связанные, char **почему) { + const char *образец, const char *хвост_сл, Сп связанные, char **почему) { Порядок o; char *ц, *L, *P; Сп лево = ПУСТО, право = ПУСТО; int i, k; - (void)тип; o.строки = строки; o.чья = чья; o.голова = (char *)""; - ц = вставить_вместо(терм(цель), "результат", - развернуть_плоское_тело(терм(тело), чья, строки)); + ц = с_результатом(цель, развернуть_плоское_тело(терм(тело), чья, строки)); + { Сп им, тр; + for (k = 0; поля(образец, " равным ", &им, &тр) && k < им.n; k++) + ц = вставить_вместо(вставить_вместо(ц, fmt("%s.%s", по, им.e[k]), тр.e[k]), fmt("%s.«%s»", по, им.e[k]), тр.e[k]); } ц = вставить_вместо(ц, по, образец); if (!разрез_равенства(ц, &L, &P)) { *почему = fmt("цель ветви «%s» — не равенство", ц); return 0; } for (i = 0; i < связанные.n; i++) { Сп один = ПУСТО, вызовы; + if (!связанное_рекурсивно(строки, тип, хвост_сл, связанные.e[i])) continue; добавить(&один, связанные.e[i]); вызовы = допущения_индукции(строки, чья, по, один); for (k = 0; k < вызовы.n; k++) { - char *ih = вставить_вместо(терм(цель), "результат", вызовы.e[k]), *a, *b; + char *ih = с_результатом(цель, вызовы.e[k]), *a, *b; ih = вставить_вместо(ih, по, связанные.e[i]); if (!разрез_равенства(ih, &a, &b)) continue; добавить(&лево, свести_порядком(a, &o, 6)); @@ -8965,6 +9030,17 @@ static int ходы_проиграны(Сверка *s, Сп свои, Сп ст return p.беды.n == 0 && p.проиграно > 0; } +static int неотрицательно_утверждение(Сп строки, const char *цель) { + char *л, *п, *почему = (char *)""; Сп имена = ПУСТО, дно = ПУСТО; long где; int k; + if (!МЕСТО_ВЫСКАЗЫВАНИЯ || есть_терм(терм(цель), "результат") || + !разрез_словом(ужать(терм(цель)), " не меньше ", &л, &п) || strcmp(ужать(п), "0") != 0) return 0; + где = строка_высказывания(строки, МЕСТО_ВЫСКАЗЫВАНИЯ); + из_высказывания(строки, где, NULL, &имена); + for (k = 0; k < имена.n; k++) + if (strcmp(объявление_типа(строки, имя_типа(из_высказывания(строки, где, имена.e[k], NULL))).вид, "отрезок") == 0) добавить(&дно, имена.e[k]); + return неотрицательно_algebra(л, "", дно, строки, 0, &почему); +} + /* ПЯТЬ КРЮКОВ ПО ТЕЛУ ФУНКЦИИ, И ПОРЯДОК ИХ — НЕ СТАРШИНСТВО ПРАВИЛ, А БЕРЕЖЛИВОСТЬ: место, снятое первым приёмом, второй раз снимать нечем, а снятое крюком не должно сменить породу под следующим. Сторож ложной переписки @@ -8985,6 +9061,7 @@ static Снято крюки_по_телу(Сверка *s, Сп свои, Сп if (начало_по_телу(строки, чья, цель)) { сн.ходами = 1; s->сведений++; s->мест_по_телу++; return сн; } if (strcmp(ужать(терм(цель)), "результат не меньше 0") == 0 && прямая_по_предположению(строки, чья)) { сн.узлом = 1; s->узел_булев = 0; } + else if (неотрицательно_утверждение(строки, цель)) { сн.ходами = 1; s->сведений++; s->мест_по_телу++; } return сн; } @@ -9927,6 +10004,63 @@ static void сверить_секцию_тотальности(Сверка *s, сверить_круги_тотальности(s, объед); } +static int *НАБОР_ХОД; static Сп *НАБОР_ДОКАЗАНО; +static Сверка сверить(const char *исходник, const char *запись, const char *путь, + const char *ждём, Сп набор_исх, Сп набор_зап); +static void проверить_набор(Сп набор_исх, Сп набор_зап) { + int d; + if (!НАБОР_ХОД) { + НАБОР_ХОД = дай((size_t)набор_исх.n * sizeof *НАБОР_ХОД); НАБОР_ДОКАЗАНО = дай((size_t)набор_исх.n * sizeof *НАБОР_ДОКАЗАНО); + for (d = 0; d < набор_исх.n; d++) { НАБОР_ХОД[d] = 0; НАБОР_ДОКАЗАНО[d] = ПУСТО; } + } + for (d = 0; d < набор_исх.n; d++) { + Сверка в; + if (НАБОР_ХОД[d]) continue; + НАБОР_ХОД[d] = 1; + в = сверить(набор_исх.e[d], набор_зап.e[d], хвост_после(часть(разделить(набор_зап.e[d], "\n"), 2), "исходник "), NULL, набор_исх, набор_зап); + if (!в.беды.n && в.крипто) НАБОР_ДОКАЗАНО[d] = в.доказанные_свойства; + НАБОР_ХОД[d] = 2; + } +} +static int имя_объявлено(Сп ст, const char *x) { + int i; + for (i = 0; i < ст.n; i++) { + char *l = обрезать(без_примечания(ст.e[i])); + if (strcmp(имя_функции(ст.e[i]), x) == 0 || начинается(l, fmt("тип «%s»", x)) || + начинается(l, fmt("объект «%s»", x)) || начинается(l, fmt("вариант «%s»", x))) return 1; + } + return 0; +} +static int ввезён(Сп строки, int d) { + char *зовут = fmt("использует «%s»", в_ёлочках(первая_с_началом(разделить(НАБОР_СТРОК.e[d], "\n"), "модуль «"), 1)); int i, k; + for (k = -1; k < НАБОР_СТРОК.n; k++) { + Сп ст = k < 0 ? строки : разделить(НАБОР_СТРОК.e[k], "\n"); + for (i = 0; i < ст.n; i++) if (начинается(обрезать(без_примечания(ст.e[i])), зовут)) return 1; + } + return 0; +} +static int имена_модуля(Сп строки, Сп ст, int d, const char *текст, const char *кроме) { + const char *q = текст, *k; + for (; (q = strstr(q, "«")) != NULL && (k = strstr(q, "»")) != NULL; q = k) { + char *x = копия(q + strlen("«"), (size_t)(k - q) - strlen("«")); + if (strcmp(x, кроме) != 0 && (!имя_объявлено(ст, x) || !видно(d, x) || имя_объявлено(строки, x))) return 0; + } + return 1; +} +static Сп свойство_набора(Сп строки, const char *имя, int *чужое) { + int d, где = -1, сколько = 0; char *заголовок = fmt("утверждение «%s»", имя), *текст; Сп ст = ПУСТО; long n, k; + *чужое = !номер_свойства(строки, имя) && !строка_высказывания(строки, заголовок) && ввозит(строки); + for (d = 0; *чужое && d < НАБОР_СТРОК.n; d++) { + Сп эти = разделить(НАБОР_СТРОК.e[d], "\n"); + if (!номер_свойства(эти, имя) && !строка_высказывания(эти, заголовок)) continue; + где = d; сколько++; ст = эти; + } + if (сколько != 1 || !НАБОР_ХОД || НАБОР_ХОД[где] != 2 || !среди(НАБОР_ДОКАЗАНО[где], имя) || !ввезён(строки, где)) return ПУСТО; + n = номер_свойства(ст, имя); k = n ? n : строка_высказывания(ст, заголовок); + текст = n ? fmt("«%s» %s", хозяин_строки(ст, n), часть(ст, n)) : часть(ст, k); + for (k++; !n && k <= ст.n && начинается(часть(ст, k), " "); k++) текст = fmt("%s %s", текст, часть(ст, k)); + return имена_модуля(строки, ст, где, текст, имя) ? ст : ПУСТО; +} static Сверка сверить(const char *исходник, const char *запись, const char *путь, const char *ждём, Сп набор_исх, Сп набор_зап) { Сверка s; @@ -9941,6 +10075,7 @@ static Сверка сверить(const char *исходник, const char *з Сп части = разделить(запись_голова, "\nутверждение "), блоки = ПУСТО; Сп шапка = разделить(часть(части, 1), "\n"), строки = разделить(исходник, "\n"); int i; + if (набор_исх.n && ввозит(строки) && содержит(запись, " по свойству ")) проверить_набор(набор_исх, набор_зап); memset(&s, 0, sizeof s); for (i = 2; i <= т_разрез.n; i++) добавить(&тотальности, часть(т_разрез, i)); for (i = 2; i <= п_разрез.n; i++) добавить(&планы, часть(п_разрез, i)); diff --git a/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang b/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang new file mode 100644 index 000000000..d6790ee60 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer of a stranger» + +использует «Citation measures» из "measures.flang" + +тотальная функция «Сколько элементов» + принимает элементы: список числа + возвращает число + обеспечивает «счёт неотрицателен» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +теорема «счёт неотрицателен» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «длина любого списка неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.record b/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.record new file mode 100644 index 000000000..0405abe1d --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-a-stranger.record @@ -0,0 +1,30 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang +строк 19 +знаков 492 +отпечаток 791906897 584107613 +ядро 2 +утверждений 1 +отпечаток256 ce2f5ea8da86f37958ea9531583ecd2be4ba2a1b4f51ab6d132b89fd6f8a5ea8 +тотальностей 1 +утверждение «счёт неотрицателен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано + теорема «счёт неотрицателен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько элементов» от ( элементы )⟩ строка 12 ⟨длина элементы⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 3 подстановка «л» ⟨элементы⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang new file mode 100644 index 000000000..f08defcdc --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer of false lemmas» + +использует «Citation false lemmas» из "false-lemmas.flang" + +тотальная функция «Сколько элементов» + принимает элементы: список числа + возвращает число + обеспечивает «счёт положителен» результат не меньше 1 + пример «один» + дано элементы равно [7] + ожидается 1 + длина элементы + +теорема «счёт положителен» + дано элементы: список числа + утверждаем результат не меньше 1 + по свойству «длина любого списка положительна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.forged.record b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.forged.record new file mode 100644 index 000000000..776154c6c --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.forged.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang +строк 19 +знаков 496 +отпечаток 179662160 917315652 +ядро 2 +утверждений 1 +отпечаток256 c6e75cea8e8f30d354882a401d61e7d46696bd182d93737f312c9e8e3efea011 +тотальностей 1 +утверждение «счёт положителен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано + теорема «счёт положителен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка положительна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.record b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.record new file mode 100644 index 000000000..ac976477e --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang +строк 19 +знаков 496 +отпечаток 179662160 917315652 +ядро 2 +утверждений 1 +отпечаток256 c6e75cea8e8f30d354882a401d61e7d46696bd182d93737f312c9e8e3efea011 +тотальностей 1 +утверждение «счёт положителен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано при условии + теорема «счёт положителен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка положительна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang b/flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang new file mode 100644 index 000000000..91c4454c0 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer of false measures» + +использует «Citation false measures» из "false-measures.flang" + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -5 + «Мера» от элементы + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-false-measures.forged.record b/flang/proof/checker/tests/families/citation/consumer-of-false-measures.forged.record new file mode 100644 index 000000000..e3129bd2f --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-false-measures.forged.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang +строк 19 +знаков 508 +отпечаток 252139343 309981491 +ядро 2 +утверждений 1 +отпечаток256 4e0bf2eb2b517b18f2e9b48402df5c94b4f77c33e494bf647c5fe0450c196eea +тотальностей 1 +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 8 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «мера неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Вторая мера» строка 5 + вид composition + зовёт «Мера» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang b/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang new file mode 100644 index 000000000..d7cca9df1 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer of measures unrelated» + +использует «Citation measures» из "measures.flang" + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -5 + (0 минус 5) плюс (0 умножить на («Мера» от элементы)) + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.record b/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.record new file mode 100644 index 000000000..8683527e1 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang +строк 19 +знаков 535 +отпечаток 665043564 132223162 +ядро 2 +утверждений 1 +отпечаток256 b466b48f11b77e026bb7a35b06fec13a36b9f4ead86624c0852fa97a55676bc7 +тотальностей 1 +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 8 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «мера неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Вторая мера» строка 5 + вид composition + зовёт «Мера» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-measures.flang b/flang/proof/checker/tests/families/citation/consumer-of-measures.flang new file mode 100644 index 000000000..ae1f870aa --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-measures.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer of measures» + +использует «Citation measures» из "measures.flang" + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + «Мера» от элементы + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-measures.record b/flang/proof/checker/tests/families/citation/consumer-of-measures.record new file mode 100644 index 000000000..de0733b07 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-measures.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-measures.flang +строк 19 +знаков 489 +отпечаток 713291905 378810207 +ядро 2 +утверждений 1 +отпечаток256 e21894892e2236979f86b60d54ecb65a861c3faaa9808eb57226510886dd7f77 +тотальностей 1 +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 8 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «мера неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Вторая мера» строка 5 + вид composition + зовёт «Мера» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-of-twins.flang b/flang/proof/checker/tests/families/citation/consumer-of-twins.flang new file mode 100644 index 000000000..e9cc233d4 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-twins.flang @@ -0,0 +1,19 @@ +модуль «Citation consumer of twins» + +использует «Citation lemmas» из "lemmas.flang" +использует «Citation lemmas twin» из "lemmas-twin.flang" + +тотальная функция «Сколько элементов» + принимает элементы: список числа + возвращает число + обеспечивает «счёт неотрицателен» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +теорема «счёт неотрицателен» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «длина любого списка неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-of-twins.record b/flang/proof/checker/tests/families/citation/consumer-of-twins.record new file mode 100644 index 000000000..b3470f744 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-of-twins.record @@ -0,0 +1,30 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-of-twins.flang +строк 20 +знаков 540 +отпечаток 891591141 55558145 +ядро 2 +утверждений 1 +отпечаток256 ea741acc3c0adce69e21b50247a3332b88e953e7822edd78ce159d41f565d773 +тотальностей 1 +утверждение «счёт неотрицателен» функции «Сколько элементов» строка 9 + вид postcondition + вердикт доказано + теорема «счёт неотрицателен» строка 15 + дано «элементы» строка 16 + цель строка 17 + шаг 1 строка 18 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько элементов» от ( элементы )⟩ строка 13 ⟨длина элементы⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 3 подстановка «л» ⟨элементы⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько элементов» строка 6 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer-with-namesake.flang b/flang/proof/checker/tests/families/citation/consumer-with-namesake.flang new file mode 100644 index 000000000..09c2ff2a4 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-with-namesake.flang @@ -0,0 +1,26 @@ +модуль «Citation consumer with namesake» + +использует «Citation namesake measures» из "namesake-measures.flang" только «Иное» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + пример «пусто» + дано элементы равно [] + ожидается -5 + ((длина элементы) плюс («Иное» от элементы)) минус 5 + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -5 + «Мера» от элементы + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer-with-namesake.record b/flang/proof/checker/tests/families/citation/consumer-with-namesake.record new file mode 100644 index 000000000..1a2fb3dc7 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer-with-namesake.record @@ -0,0 +1,33 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer-with-namesake.flang +строк 27 +знаков 720 +отпечаток 319968165 148367705 +ядро 2 +утверждений 1 +отпечаток256 76843d13da50f0cb287fe3da97c96b4e9f72de042dfac2eb556255accb26cdad +тотальностей 2 +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 16 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 22 + дано «элементы» строка 23 + цель строка 24 + шаг 1 строка 25 закрывающий по свойству «мера неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Мера» строка 5 + вид composition + зовёт примитив «длина» + зовёт «Иное» строка 12 тотальна + зовёт примитив «плюс» + зовёт примитив «минус» + самовызова нет + конец тотальности +тотальность «Вторая мера» строка 13 + вид composition + зовёт «Мера» строка 5 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer.flang b/flang/proof/checker/tests/families/citation/consumer.flang new file mode 100644 index 000000000..47840f4f5 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer.flang @@ -0,0 +1,18 @@ +модуль «Citation consumer» + +использует «Citation lemmas» из "lemmas.flang" + +тотальная функция «Сколько элементов» + принимает элементы: список числа + возвращает число + обеспечивает «счёт неотрицателен» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +теорема «счёт неотрицателен» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «длина любого списка неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/consumer.record b/flang/proof/checker/tests/families/citation/consumer.record new file mode 100644 index 000000000..6b652d11f --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer.record @@ -0,0 +1,30 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer.flang +строк 19 +знаков 474 +отпечаток 901624015 901631433 +ядро 2 +утверждений 1 +отпечаток256 ebf085339f0c7b7ed853ff9f8582610383cb41c93595df2b20610ee083f2b908 +тотальностей 1 +утверждение «счёт неотрицателен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано + теорема «счёт неотрицателен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько элементов» от ( элементы )⟩ строка 12 ⟨длина элементы⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 3 подстановка «л» ⟨элементы⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer.wrong-line.record b/flang/proof/checker/tests/families/citation/consumer.wrong-line.record new file mode 100644 index 000000000..546474722 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer.wrong-line.record @@ -0,0 +1,30 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer.flang +строк 19 +знаков 474 +отпечаток 901624015 901631433 +ядро 2 +утверждений 1 +отпечаток256 ebf085339f0c7b7ed853ff9f8582610383cb41c93595df2b20610ee083f2b908 +тотальностей 1 +утверждение «счёт неотрицателен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано + теорема «счёт неотрицателен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько элементов» от ( элементы )⟩ строка 12 ⟨длина элементы⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 4 подстановка «л» ⟨элементы⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/consumer.wrong-substitution.record b/flang/proof/checker/tests/families/citation/consumer.wrong-substitution.record new file mode 100644 index 000000000..44707954b --- /dev/null +++ b/flang/proof/checker/tests/families/citation/consumer.wrong-substitution.record @@ -0,0 +1,30 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/consumer.flang +строк 19 +знаков 474 +отпечаток 901624015 901631433 +ядро 2 +утверждений 1 +отпечаток256 ebf085339f0c7b7ed853ff9f8582610383cb41c93595df2b20610ee083f2b908 +тотальностей 1 +утверждение «счёт неотрицателен» функции «Сколько элементов» строка 8 + вид postcondition + вердикт доказано + теорема «счёт неотрицателен» строка 14 + дано «элементы» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько элементов» от ( элементы )⟩ строка 12 ⟨длина элементы⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 3 подстановка «л» ⟨пустой список⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько элементов» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/false-lemmas.flang b/flang/proof/checker/tests/families/citation/false-lemmas.flang new file mode 100644 index 000000000..7ec629994 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/false-lemmas.flang @@ -0,0 +1,5 @@ +модуль «Citation false lemmas» + +утверждение «длина любого списка положительна» + для всех л: список числа + утверждаем (длина л) не меньше 1 diff --git a/flang/proof/checker/tests/families/citation/false-lemmas.forged.record b/flang/proof/checker/tests/families/citation/false-lemmas.forged.record new file mode 100644 index 000000000..f38c2db55 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/false-lemmas.forged.record @@ -0,0 +1,19 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/false-lemmas.flang +строк 6 +знаков 141 +отпечаток 399233118 906880537 +ядро 2 +утверждений 1 +отпечаток256 7f73ea643ceecbea7d84d7df5ad16d3e06b9bf1e956144e7f35ebe58afb11e69 + +утверждение «длина любого списка положительна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/citation/false-lemmas.record b/flang/proof/checker/tests/families/citation/false-lemmas.record new file mode 100644 index 000000000..fa51da10e --- /dev/null +++ b/flang/proof/checker/tests/families/citation/false-lemmas.record @@ -0,0 +1,17 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/false-lemmas.flang +строк 6 +знаков 141 +отпечаток 399233118 906880537 +ядро 2 +утверждений 1 +отпечаток256 7f73ea643ceecbea7d84d7df5ad16d3e06b9bf1e956144e7f35ebe58afb11e69 + +утверждение «длина любого списка положительна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт нет вердикта + теоремы нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/citation/false-measures.flang b/flang/proof/checker/tests/families/citation/false-measures.flang new file mode 100644 index 000000000..70b297315 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/false-measures.flang @@ -0,0 +1,10 @@ +модуль «Citation false measures» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -5 + (длина элементы) минус 5 diff --git a/flang/proof/checker/tests/families/citation/false-measures.forged.record b/flang/proof/checker/tests/families/citation/false-measures.forged.record new file mode 100644 index 000000000..4542bc3cf --- /dev/null +++ b/flang/proof/checker/tests/families/citation/false-measures.forged.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/false-measures.flang +строк 11 +знаков 260 +отпечаток 366782500 56681318 +ядро 2 +утверждений 1 +отпечаток256 e9b6c29f041ed71fa4dae9775ff109e80f7eea67198f4d2aa35610c14271860f +тотальностей 1 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/lemmas-twin.flang b/flang/proof/checker/tests/families/citation/lemmas-twin.flang new file mode 100644 index 000000000..51d7a8197 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/lemmas-twin.flang @@ -0,0 +1,5 @@ +модуль «Citation lemmas twin» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 diff --git a/flang/proof/checker/tests/families/citation/lemmas-twin.record b/flang/proof/checker/tests/families/citation/lemmas-twin.record new file mode 100644 index 000000000..35b109ded --- /dev/null +++ b/flang/proof/checker/tests/families/citation/lemmas-twin.record @@ -0,0 +1,19 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/lemmas-twin.flang +строк 6 +знаков 142 +отпечаток 425778174 449502655 +ядро 2 +утверждений 1 +отпечаток256 584293c7c67246de0ebb9d489e0ea7d04afd72a3bfb813f84b2242236289278d + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/citation/lemmas.flang b/flang/proof/checker/tests/families/citation/lemmas.flang new file mode 100644 index 000000000..9be655d6a --- /dev/null +++ b/flang/proof/checker/tests/families/citation/lemmas.flang @@ -0,0 +1,5 @@ +модуль «Citation lemmas» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 diff --git a/flang/proof/checker/tests/families/citation/lemmas.record b/flang/proof/checker/tests/families/citation/lemmas.record new file mode 100644 index 000000000..4f96236e1 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/lemmas.record @@ -0,0 +1,19 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/lemmas.flang +строк 6 +знаков 137 +отпечаток 826038993 653965058 +ядро 2 +утверждений 1 +отпечаток256 1c45f0e1de8149cc92399c4dcf3757eeaf2dcad9e4fe667a26f4a052e45d0393 + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/citation/measures.flang b/flang/proof/checker/tests/families/citation/measures.flang new file mode 100644 index 000000000..eebe0d7e8 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/measures.flang @@ -0,0 +1,10 @@ +модуль «Citation measures» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы diff --git a/flang/proof/checker/tests/families/citation/measures.record b/flang/proof/checker/tests/families/citation/measures.record new file mode 100644 index 000000000..ccca2ac53 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/measures.record @@ -0,0 +1,27 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/measures.flang +строк 11 +знаков 243 +отпечаток 61085692 600219212 +ядро 2 +утверждений 1 +отпечаток256 9cdb3931645f5ef553589fa9336afac48d8dc3f19551340bfb89ff5c584b132e +тотальностей 1 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/namesake-measures.flang b/flang/proof/checker/tests/families/citation/namesake-measures.flang new file mode 100644 index 000000000..20d2e1c76 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/namesake-measures.flang @@ -0,0 +1,18 @@ +модуль «Citation namesake measures» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +тотальная функция «Иное» + принимает элементы: список числа + возвращает число + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы diff --git a/flang/proof/checker/tests/families/citation/namesake-measures.record b/flang/proof/checker/tests/families/citation/namesake-measures.record new file mode 100644 index 000000000..0e2db0404 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/namesake-measures.record @@ -0,0 +1,32 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/namesake-measures.flang +строк 19 +знаков 409 +отпечаток 335624628 937726874 +ядро 2 +утверждений 1 +отпечаток256 88843ceec1dd62269f8edbd70321f65f79a7d26026dd5bf8ec3b1f979c718e4a +тотальностей 2 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Иное» строка 12 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang b/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang new file mode 100644 index 000000000..7601fbf5d --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang @@ -0,0 +1,25 @@ +модуль «Citation by bound subtracts» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -7 + («Мера» от элементы) минус 7 + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.record b/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.record new file mode 100644 index 000000000..563ad47fa --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-bound-subtracts.record @@ -0,0 +1,43 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang +строк 26 +знаков 662 +отпечаток 62768720 310581392 +ядро 2 +утверждений 2 +отпечаток256 cf1b9de493b08207a7168575262f9d260e0552966809d026573aa82dda208c09 +тотальностей 2 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 15 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 21 + дано «элементы» строка 22 + цель строка 23 + шаг 1 строка 24 закрывающий по свойству «мера неотрицательна» свойство строка 6 правило «неотрицательность по построению» + следовательно доказано да +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Вторая мера» строка 12 + вид composition + зовёт «Мера» строка 3 тотальна + зовёт примитив «плюс» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/step-by-bound.flang b/flang/proof/checker/tests/families/citation/step-by-bound.flang new file mode 100644 index 000000000..9b2316e61 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-bound.flang @@ -0,0 +1,25 @@ +модуль «Citation by bound» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 2 + 2 плюс («Мера» от элементы) + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/step-by-bound.record b/flang/proof/checker/tests/families/citation/step-by-bound.record new file mode 100644 index 000000000..1ce01f133 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-bound.record @@ -0,0 +1,43 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/step-by-bound.flang +строк 26 +знаков 650 +отпечаток 869244503 566442796 +ядро 2 +утверждений 2 +отпечаток256 1e2e14b194512ac9e68c0980ff672c59c3909360d6ffcadcc51fa3368924998a +тотальностей 2 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 15 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 21 + дано «элементы» строка 22 + цель строка 23 + шаг 1 строка 24 закрывающий по свойству «мера неотрицательна» свойство строка 6 правило «неотрицательность по построению» + следовательно доказано да +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Вторая мера» строка 12 + вид composition + зовёт «Мера» строка 3 тотальна + зовёт примитив «плюс» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/step-by-postcondition.flang b/flang/proof/checker/tests/families/citation/step-by-postcondition.flang new file mode 100644 index 000000000..b5fb95300 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-postcondition.flang @@ -0,0 +1,25 @@ +модуль «Citation by postcondition» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + «Мера» от элементы + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/step-by-postcondition.record b/flang/proof/checker/tests/families/citation/step-by-postcondition.record new file mode 100644 index 000000000..df9a5e200 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-postcondition.record @@ -0,0 +1,42 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/step-by-postcondition.flang +строк 26 +знаков 649 +отпечаток 842068182 748288548 +ядро 2 +утверждений 2 +отпечаток256 c8cac314009c865bc637baa36820b00424c4fcdae4ccf4f545b95ecdf432f58c +тотальностей 2 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 15 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 21 + дано «элементы» строка 22 + цель строка 23 + шаг 1 строка 24 закрывающий по свойству «мера неотрицательна» свойство строка 6 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Вторая мера» строка 12 + вид composition + зовёт «Мера» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang b/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang new file mode 100644 index 000000000..fde9be943 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang @@ -0,0 +1,25 @@ +модуль «Citation by restricted postcondition» + +тотальная функция «Сдвиг» + принимает н: число + возвращает число + для всех н таких что н не меньше 0 обеспечивает «сдвиг неотрицателен» результат не меньше 0 + пример «ноль» + дано н равно 0 + ожидается 0 + н + +тотальная функция «Второй сдвиг» + принимает н: число + возвращает число + обеспечивает «второй сдвиг неотрицателен» результат не меньше 0 + пример «ноль» + дано н равно 0 + ожидается 0 + «Сдвиг» от н + +теорема «второй сдвиг неотрицателен» + дано н: число + утверждаем результат не меньше 0 + по свойству «сдвиг неотрицателен» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.record b/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.record new file mode 100644 index 000000000..e41fd2597 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.record @@ -0,0 +1,39 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang +строк 26 +знаков 618 +отпечаток 353706341 151641263 +ядро 2 +утверждений 2 +отпечаток256 93e1613235bed5e4fa97ff30a68ee4191447635cad9ab745107f45ae8bd81e9f +тотальностей 2 +утверждение «сдвиг неотрицателен» функции «Сдвиг» строка 6 + вид postcondition + для всех «н» строка 6 + таких что ⟨н не меньше 0⟩ строка 6 + вердикт доказано + теоремы нет + правило «цель есть допущение» + по объявлению нет +конец утверждения + +утверждение «второй сдвиг неотрицателен» функции «Второй сдвиг» строка 15 + вид postcondition + вердикт доказано + теорема «второй сдвиг неотрицателен» строка 21 + дано «н» строка 22 + цель строка 23 + шаг 1 строка 24 закрывающий по свойству «сдвиг неотрицателен» свойство строка 6 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Сдвиг» строка 3 + вид composition + самовызова нет + конец тотальности +тотальность «Второй сдвиг» строка 12 + вид composition + зовёт «Сдвиг» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang b/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang new file mode 100644 index 000000000..e0f0a8b09 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang @@ -0,0 +1,25 @@ +модуль «Citation by unrelated postcondition» + +тотальная функция «Мера» + принимает элементы: список числа + возвращает число + обеспечивает «мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается 0 + длина элементы + +тотальная функция «Вторая мера» + принимает элементы: список числа + возвращает число + обеспечивает «вторая мера неотрицательна» результат не меньше 0 + пример «пусто» + дано элементы равно [] + ожидается -5 + (0 минус 5) плюс (0 умножить на («Мера» от элементы)) + +теорема «вторая мера неотрицательна» + дано элементы: список числа + утверждаем результат не меньше 0 + по свойству «мера неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.record b/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.record new file mode 100644 index 000000000..f1e951bc3 --- /dev/null +++ b/flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.record @@ -0,0 +1,42 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang +строк 26 +знаков 695 +отпечаток 234728548 629997522 +ядро 2 +утверждений 2 +отпечаток256 6b01070d7323b1355872175f1e498703d4b6481439a18c1cf9c20f778dddca36 +тотальностей 2 +утверждение «мера неотрицательна» функции «Мера» строка 6 + вид postcondition + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет + ход цель + ход 1 развернуть ⟨«Мера» от ( элементы )⟩ строка 10 ⟨длина элементы⟩ + ход 2 закон «мера неотрицательна» + ход конец +конец утверждения + +утверждение «вторая мера неотрицательна» функции «Вторая мера» строка 15 + вид postcondition + вердикт доказано + теорема «вторая мера неотрицательна» строка 21 + дано «элементы» строка 22 + цель строка 23 + шаг 1 строка 24 закрывающий по свойству «мера неотрицательна» свойство строка 6 правило «цель есть допущение» + следовательно доказано да +конец утверждения + +тотальность «Мера» строка 3 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Вторая мера» строка 12 + вид composition + зовёт «Мера» строка 3 тотальна + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/field-projection/accessor-other-field.flang b/flang/proof/checker/tests/families/field-projection/accessor-other-field.flang new file mode 100644 index 000000000..796d14fc8 --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor-other-field.flang @@ -0,0 +1,15 @@ +модуль «Field projection of the other field» + +тип «Пара» + вариант «Пара» содержит первое: число, второе: число + +тотальная функция «Первое пары» + принимает пара: «Пара» + возвращает число + обеспечивает «первое пары — это первое, записанное в паре» результат равен пара.второе + пример «пара один и два» + дано пара равно вариант «Пара» с первое равным 1 и второе равным 2 + ожидается 1 + разбор пара + случай вариант «Пара» с первое как левое и второе как правое + то левое diff --git a/flang/proof/checker/tests/families/field-projection/accessor-other-field.record b/flang/proof/checker/tests/families/field-projection/accessor-other-field.record new file mode 100644 index 000000000..6a92bf5b0 --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor-other-field.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/field-projection/accessor-other-field.flang +строк 16 +знаков 486 +отпечаток 659735482 497990262 +ядро 2 +утверждений 1 +отпечаток256 73062f0dfb2db6e0ff84eb68e878813810eb91730f57339e1b616bef253a6526 +тотальностей 1 +утверждение «первое пары — это первое, записанное в паре» функции «Первое пары» строка 9 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Пара» по «пара» носитель algebra база 1 шаг 0 + объявление сумма «Пара» строка 3 варианты «Пара» 0 + сведение «тождество после переписки допущением» + посылка «Пара» вид base вариант «Пара» вердикт доказано закрыта reduction шагов 0 правило «тождество после переписки допущением» +конец утверждения + +тотальность «Первое пары» строка 6 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang b/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang new file mode 100644 index 000000000..a5bef1bf3 --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang @@ -0,0 +1,15 @@ +модуль «Field projection with swapped binding» + +тип «Пара» + вариант «Пара» содержит первое: число, второе: число + +тотальная функция «Первое пары» + принимает пара: «Пара» + возвращает число + обеспечивает «первое пары — это первое, записанное в паре» результат равен пара.первое + пример «пара один и два» + дано пара равно вариант «Пара» с первое равным 1 и второе равным 2 + ожидается 1 + разбор пара + случай вариант «Пара» с первое как правое и второе как левое + то левое diff --git a/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.record b/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.record new file mode 100644 index 000000000..4c78a6ee1 --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang +строк 16 +знаков 488 +отпечаток 214511613 956442356 +ядро 2 +утверждений 1 +отпечаток256 1fa1a63b8c013716ffcb543cacff8689d131ebedb626f9c99dfa82d482dc8ff6 +тотальностей 1 +утверждение «первое пары — это первое, записанное в паре» функции «Первое пары» строка 9 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Пара» по «пара» носитель algebra база 1 шаг 0 + объявление сумма «Пара» строка 3 варианты «Пара» 0 + сведение «тождество после переписки допущением» + посылка «Пара» вид base вариант «Пара» вердикт доказано закрыта reduction шагов 0 правило «тождество после переписки допущением» +конец утверждения + +тотальность «Первое пары» строка 6 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/field-projection/accessor.flang b/flang/proof/checker/tests/families/field-projection/accessor.flang new file mode 100644 index 000000000..60fccfced --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor.flang @@ -0,0 +1,15 @@ +модуль «Field projection» + +тип «Пара» + вариант «Пара» содержит первое: число, второе: число + +тотальная функция «Первое пары» + принимает пара: «Пара» + возвращает число + обеспечивает «первое пары — это первое, записанное в паре» результат равен пара.первое + пример «пара один и два» + дано пара равно вариант «Пара» с первое равным 1 и второе равным 2 + ожидается 1 + разбор пара + случай вариант «Пара» с первое как левое и второе как правое + то левое diff --git a/flang/proof/checker/tests/families/field-projection/accessor.record b/flang/proof/checker/tests/families/field-projection/accessor.record new file mode 100644 index 000000000..8c514419d --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/accessor.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/field-projection/accessor.flang +строк 16 +знаков 467 +отпечаток 972270327 273216167 +ядро 2 +утверждений 1 +отпечаток256 49b3f907169c8696005f36e96f2744efd8d4613708f9a8275010aa87023c8eb0 +тотальностей 1 +утверждение «первое пары — это первое, записанное в паре» функции «Первое пары» строка 9 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Пара» по «пара» носитель algebra база 1 шаг 0 + объявление сумма «Пара» строка 3 варианты «Пара» 0 + сведение «тождество после переписки допущением» + посылка «Пара» вид base вариант «Пара» вердикт доказано закрыта reduction шагов 0 правило «тождество после переписки допущением» +конец утверждения + +тотальность «Первое пары» строка 6 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/field-projection/result-field-other.flang b/flang/proof/checker/tests/families/field-projection/result-field-other.flang new file mode 100644 index 000000000..ca2c49331 --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/result-field-other.flang @@ -0,0 +1,16 @@ +модуль «Field projection of a result claims another field» + +тип «Тройка» + вариант «Тройка» содержит с0: число, с1: число, с2: число + +тотальная функция «Сдвинуть тройку» + принимает тройка: «Тройка», слово: число + возвращает «Тройка» + обеспечивает «сдвиг: поле 0 берёт прежнее поле 1» (результат.с0 равен тройка.с2) + пример «сдвиг» + дано тройка равно вариант «Тройка» с с0 равным 1 и с1 равным 2 и с2 равным 3 + дано слово равно 9 + ожидается вариант «Тройка» с с0 равным 2 и с1 равным 3 и с2 равным 9 + разбор тройки + случай вариант «Тройка» с с0 как п0 и с1 как п1 и с2 как п2 + то вариант «Тройка» с с0 равным п1 и с1 равным п2 и с2 равным слово diff --git a/flang/proof/checker/tests/families/field-projection/result-field-other.record b/flang/proof/checker/tests/families/field-projection/result-field-other.record new file mode 100644 index 000000000..541acba1c --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/result-field-other.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/field-projection/result-field-other.flang +строк 17 +знаков 666 +отпечаток 432206838 816565888 +ядро 2 +утверждений 1 +отпечаток256 b823eeacc5fccbe28200a18ba89f337bca952fbb9f2d250f29ce89209b652e9a +тотальностей 1 +утверждение «сдвиг: поле 0 берёт прежнее поле 1» функции «Сдвинуть тройку» строка 9 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Тройка» по «тройка» носитель algebra база 1 шаг 0 + объявление сумма «Тройка» строка 3 варианты «Тройка» 0 + сведение «тождество после переписки допущением» + посылка «Тройка» вид base вариант «Тройка» вердикт доказано закрыта reduction шагов 0 правило «тождество после переписки допущением» +конец утверждения + +тотальность «Сдвинуть тройку» строка 6 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/field-projection/result-field.flang b/flang/proof/checker/tests/families/field-projection/result-field.flang new file mode 100644 index 000000000..976ce6c4a --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/result-field.flang @@ -0,0 +1,16 @@ +модуль «Field projection of a result» + +тип «Тройка» + вариант «Тройка» содержит с0: число, с1: число, с2: число + +тотальная функция «Сдвинуть тройку» + принимает тройка: «Тройка», слово: число + возвращает «Тройка» + обеспечивает «сдвиг: поле 0 берёт прежнее поле 1» (результат.с0 равен тройка.с1) + пример «сдвиг» + дано тройка равно вариант «Тройка» с с0 равным 1 и с1 равным 2 и с2 равным 3 + дано слово равно 9 + ожидается вариант «Тройка» с с0 равным 2 и с1 равным 3 и с2 равным 9 + разбор тройки + случай вариант «Тройка» с с0 как п0 и с1 как п1 и с2 как п2 + то вариант «Тройка» с с0 равным п1 и с1 равным п2 и с2 равным слово diff --git a/flang/proof/checker/tests/families/field-projection/result-field.record b/flang/proof/checker/tests/families/field-projection/result-field.record new file mode 100644 index 000000000..026f06b8a --- /dev/null +++ b/flang/proof/checker/tests/families/field-projection/result-field.record @@ -0,0 +1,25 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/field-projection/result-field.flang +строк 17 +знаков 645 +отпечаток 238704231 598316322 +ядро 2 +утверждений 1 +отпечаток256 f0cc6aced5859a43297ab1714d45cb9157fab077bf6c57dd9ed40f9107d5616f +тотальностей 1 +утверждение «сдвиг: поле 0 берёт прежнее поле 1» функции «Сдвинуть тройку» строка 9 + вид postcondition + вердикт доказано + теоремы нет + принцип тип «Тройка» по «тройка» носитель algebra база 1 шаг 0 + объявление сумма «Тройка» строка 3 варианты «Тройка» 0 + сведение «тождество после переписки допущением» + посылка «Тройка» вид base вариант «Тройка» вердикт доказано закрыта reduction шагов 0 правило «тождество после переписки допущением» +конец утверждения + +тотальность «Сдвинуть тройку» строка 6 + вид composition + зовёт примитив «разбор» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/fmath/difference-of-lengths.flang b/flang/proof/checker/tests/families/fmath/difference-of-lengths.flang new file mode 100644 index 000000000..ce8e99ebb --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/difference-of-lengths.flang @@ -0,0 +1,17 @@ +модуль «Fmath difference of lengths» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 + +утверждение «длина любой строки неотрицательна» + для всех т: строка + утверждаем (длина т) не меньше 0 + +утверждение «сумма неотрицательных неотрицательна» + для всех а: неотрицательное и б: неотрицательное + утверждаем (а плюс б) не меньше 0 + +утверждение «сумма длин двух строк неотрицательна» + для всех а: строка и б: строка + утверждаем ((длина а) минус (длина б)) не меньше 0 diff --git a/flang/proof/checker/tests/families/fmath/difference-of-lengths.record b/flang/proof/checker/tests/families/fmath/difference-of-lengths.record new file mode 100644 index 000000000..b91108472 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/difference-of-lengths.record @@ -0,0 +1,48 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/fmath/difference-of-lengths.flang +строк 18 +знаков 531 +отпечаток 288389360 471296390 +ядро 2 +утверждений 4 +отпечаток256 aa64c53e4ece7ef609c60fd67ffd6adab59774fa962d8684faa60c65801f6425 + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «длина любой строки неотрицательна» строка 7 + вид statement + для всех «т» ⟨строка⟩ строка 8 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «сумма неотрицательных неотрицательна» строка 11 + вид statement + для всех «а» ⟨неотрицательное⟩ строка 12 + для всех «б» ⟨неотрицательное⟩ строка 12 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению да +конец утверждения + +утверждение «сумма длин двух строк неотрицательна» строка 15 + вид statement + для всех «а» ⟨строка⟩ строка 16 + для всех «б» ⟨строка⟩ строка 16 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/fmath/fmath.record b/flang/proof/checker/tests/families/fmath/fmath.record new file mode 100644 index 000000000..cd63cb5a8 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/fmath.record @@ -0,0 +1,48 @@ +запись доказательства 1 +исходник flang/stdlib/fmath.flang +строк 18 +знаков 508 +отпечаток 474593887 616663954 +ядро 2 +утверждений 4 +отпечаток256 0a38bde3596b1631f5509a30a8f9441e8bacfec24cc2c196f585ad2a99108875 + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «длина любой строки неотрицательна» строка 7 + вид statement + для всех «т» ⟨строка⟩ строка 8 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «сумма неотрицательных неотрицательна» строка 11 + вид statement + для всех «а» ⟨неотрицательное⟩ строка 12 + для всех «б» ⟨неотрицательное⟩ строка 12 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению да +конец утверждения + +утверждение «сумма длин двух строк неотрицательна» строка 15 + вид statement + для всех «а» ⟨строка⟩ строка 16 + для всех «б» ⟨строка⟩ строка 16 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/fmath/restricted-sum.flang b/flang/proof/checker/tests/families/fmath/restricted-sum.flang new file mode 100644 index 000000000..4220819f8 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/restricted-sum.flang @@ -0,0 +1,17 @@ +модуль «Fmath restricted sum» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 + +утверждение «длина любой строки неотрицательна» + для всех т: строка + утверждаем (длина т) не меньше 0 + +утверждение «сумма неотрицательных неотрицательна» + для всех а: число и б: число таких что а не меньше 0 + утверждаем (а плюс б) не меньше 0 + +утверждение «сумма длин двух строк неотрицательна» + для всех а: строка и б: строка + утверждаем ((длина а) плюс (длина б)) не меньше 0 diff --git a/flang/proof/checker/tests/families/fmath/restricted-sum.record b/flang/proof/checker/tests/families/fmath/restricted-sum.record new file mode 100644 index 000000000..238c5a0ce --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/restricted-sum.record @@ -0,0 +1,49 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/fmath/restricted-sum.flang +строк 18 +знаков 527 +отпечаток 575431033 374006290 +ядро 2 +утверждений 4 +отпечаток256 27e43270155106c7a577a15141214310b018bc16ae565a909ca047b9900cf4f7 + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «длина любой строки неотрицательна» строка 7 + вид statement + для всех «т» ⟨строка⟩ строка 8 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «сумма неотрицательных неотрицательна» строка 11 + вид statement + для всех «а» ⟨число⟩ строка 12 + для всех «б» ⟨число⟩ строка 12 + таких что ⟨а не меньше 0⟩ строка 12 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению да +конец утверждения + +утверждение «сумма длин двух строк неотрицательна» строка 15 + вид statement + для всех «а» ⟨строка⟩ строка 16 + для всех «б» ⟨строка⟩ строка 16 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/families/fmath/scores.flang b/flang/proof/checker/tests/families/fmath/scores.flang new file mode 100644 index 000000000..19f688303 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/scores.flang @@ -0,0 +1,35 @@ +модуль «Scores» + +использует «Fmath» + +тотальная функция «Сколько оценок» + принимает оценки: список числа + возвращает число + обеспечивает «оценок не меньше нуля» результат не меньше 0 + пример «три оценки» + дано оценки равно [5, 4, 5] + ожидается 3 + длина оценки + +теорема «оценок не меньше нуля» + дано оценки: список числа + утверждаем результат не меньше 0 + по свойству «длина любого списка неотрицательна» + следовательно доказано + +тотальная функция «Длина подписи» + принимает имя: строка, фамилия: строка + возвращает число + обеспечивает «подпись не короче нуля» результат не меньше 0 + пример «Анна Ким» + дано имя равно "Анна" + дано фамилия равно "Ким" + ожидается 7 + (длина имя) плюс (длина фамилия) + +теорема «подпись не короче нуля» + дано имя: строка + дано фамилия: строка + утверждаем результат не меньше 0 + по свойству «сумма длин двух строк неотрицательна» + следовательно доказано diff --git a/flang/proof/checker/tests/families/fmath/scores.record b/flang/proof/checker/tests/families/fmath/scores.record new file mode 100644 index 000000000..d03aa5a81 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/scores.record @@ -0,0 +1,53 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/fmath/scores.flang +строк 36 +знаков 914 +отпечаток 277234357 707248324 +ядро 2 +утверждений 2 +отпечаток256 af98464814a1d61b55a7c9cafbb9d5d8dd7cce36f5ee2d22173ac844d7f26e79 +тотальностей 2 +утверждение «оценок не меньше нуля» функции «Сколько оценок» строка 8 + вид postcondition + вердикт доказано + теорема «оценок не меньше нуля» строка 14 + дано «оценки» строка 15 + цель строка 16 + шаг 1 строка 17 закрывающий по свойству «длина любого списка неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Сколько оценок» от ( оценки )⟩ строка 12 ⟨длина оценки⟩ + ход 2 факт по свойству «длина любого списка неотрицательна» строка 3 подстановка «л» ⟨оценки⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +утверждение «подпись не короче нуля» функции «Длина подписи» строка 23 + вид postcondition + вердикт доказано + теорема «подпись не короче нуля» строка 30 + дано «имя» строка 31 + дано «фамилия» строка 32 + цель строка 33 + шаг 1 строка 34 закрывающий по свойству «сумма длин двух строк неотрицательна» свойство строка 0 правило «цель есть допущение» + следовательно доказано да + ход цель + ход 1 развернуть ⟨«Длина подписи» от ( имя ) и фамилия⟩ строка 28 ⟨(длина имя) плюс (длина фамилия)⟩ + ход 2 факт по свойству «сумма длин двух строк неотрицательна» строка 15 подстановка «а» ⟨имя⟩ «б» ⟨фамилия⟩ + ход 3 закрыть по свойству + ход конец +конец утверждения + +тотальность «Сколько оценок» строка 5 + вид composition + зовёт примитив «длина» + самовызова нет + конец тотальности +тотальность «Длина подписи» строка 20 + вид composition + зовёт примитив «длина» + зовёт примитив «длина» + зовёт примитив «плюс» + самовызова нет + конец тотальности +конец записи diff --git a/flang/proof/checker/tests/families/fmath/sum-of-a-number.flang b/flang/proof/checker/tests/families/fmath/sum-of-a-number.flang new file mode 100644 index 000000000..4f4546a4f --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/sum-of-a-number.flang @@ -0,0 +1,17 @@ +модуль «Fmath sum of a number» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 + +утверждение «длина любой строки неотрицательна» + для всех т: строка + утверждаем (длина т) не меньше 0 + +утверждение «сумма неотрицательных неотрицательна» + для всех а: число и б: неотрицательное + утверждаем (а плюс б) не меньше 0 + +утверждение «сумма длин двух строк неотрицательна» + для всех а: строка и б: строка + утверждаем ((длина а) плюс (длина б)) не меньше 0 diff --git a/flang/proof/checker/tests/families/fmath/sum-of-a-number.record b/flang/proof/checker/tests/families/fmath/sum-of-a-number.record new file mode 100644 index 000000000..216307f45 --- /dev/null +++ b/flang/proof/checker/tests/families/fmath/sum-of-a-number.record @@ -0,0 +1,48 @@ +запись доказательства 1 +исходник flang/proof/checker/tests/families/fmath/sum-of-a-number.flang +строк 18 +знаков 514 +отпечаток 3417952 892587936 +ядро 2 +утверждений 4 +отпечаток256 e76e6930d99faa98868cf0493bf1c772e3480d8b32ede3b9bf8400a293136648 + +утверждение «длина любого списка неотрицательна» строка 3 + вид statement + для всех «л» ⟨список числа⟩ строка 4 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «длина любой строки неотрицательна» строка 7 + вид statement + для всех «т» ⟨строка⟩ строка 8 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +утверждение «сумма неотрицательных неотрицательна» строка 11 + вид statement + для всех «а» ⟨число⟩ строка 12 + для всех «б» ⟨неотрицательное⟩ строка 12 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению да +конец утверждения + +утверждение «сумма длин двух строк неотрицательна» строка 15 + вид statement + для всех «а» ⟨строка⟩ строка 16 + для всех «б» ⟨строка⟩ строка 16 + вердикт доказано + теоремы нет + правило «неотрицательность по построению» + по объявлению нет +конец утверждения + +конец записи diff --git a/flang/proof/checker/tests/probes.tsv b/flang/proof/checker/tests/probes.tsv index 877858a21..308170266 100644 --- a/flang/proof/checker/tests/probes.tsv +++ b/flang/proof/checker/tests/probes.tsv @@ -924,3 +924,34 @@ P 4573 Б: варианты типа из модуля не те flang/proof/che 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 «Шаг» не примитив и не имеет блока тотальности - - +say ── 4573: шаг «по свойству» по существу, свойство из другого файла ── - - - - - - - - - - +C a step cites a postcondition that closes the goal flang/proof/checker/tests/families/citation/step-by-postcondition.flang flang/proof/checker/tests/families/citation/step-by-postcondition.record - - - - 0 Шагов по свойству проверено по существу 1 - - +P forged: a step cites a true postcondition that does not close the goal flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.record - - - - 3 вывод цели из постусловия сверщик не переиграл - - +C a statement cited from another file, its module not given flang/proof/checker/tests/families/citation/consumer.flang flang/proof/checker/tests/families/citation/consumer.record - - - - 3 в этом исходнике его нет, а файл ввозит модули - - +C a statement cited from another file, its module given flang/proof/checker/tests/families/citation/consumer.flang flang/proof/checker/tests/families/citation/consumer.record - - --зависимость flang/proof/checker/tests/families/citation/lemmas.flang flang/proof/checker/tests/families/citation/lemmas.record - 0 Шагов по свойству проверено по существу 1 - - +P forged: the move names a line that is not the statement flang/proof/checker/tests/families/citation/consumer.flang flang/proof/checker/tests/families/citation/consumer.wrong-line.record - - --зависимость flang/proof/checker/tests/families/citation/lemmas.flang flang/proof/checker/tests/families/citation/lemmas.record - 1 не заголовок «утверждение - - +P forged: the move substitutes a term that does not give the goal flang/proof/checker/tests/families/citation/consumer.flang flang/proof/checker/tests/families/citation/consumer.wrong-substitution.record - - --зависимость flang/proof/checker/tests/families/citation/lemmas.flang flang/proof/checker/tests/families/citation/lemmas.record - 1 закрыть по свойству - - +C a statement the kernel did not prove is no fact for another file flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.record - - --зависимость flang/proof/checker/tests/families/citation/false-lemmas.flang flang/proof/checker/tests/families/citation/false-lemmas.record - 3 доказано при условии - - +P forged: both records call the false statement proved flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.forged.record - - --зависимость flang/proof/checker/tests/families/citation/false-lemmas.flang flang/proof/checker/tests/families/citation/false-lemmas.forged.record - 3 не проверен по существу - - +C a postcondition cited from another file, its module given flang/proof/checker/tests/families/citation/consumer-of-measures.flang flang/proof/checker/tests/families/citation/consumer-of-measures.record - - --зависимость flang/proof/checker/tests/families/citation/measures.flang flang/proof/checker/tests/families/citation/measures.record - 0 Шагов по свойству проверено по существу 1 - - +P forged: the cited postcondition of another file does not close the goal flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.record - - --зависимость flang/proof/checker/tests/families/citation/measures.flang flang/proof/checker/tests/families/citation/measures.record - 3 вывод цели из постусловия сверщик не переиграл - - +P forged: the module record calls a false postcondition proved flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang flang/proof/checker/tests/families/citation/consumer-of-false-measures.forged.record - - --зависимость flang/proof/checker/tests/families/citation/false-measures.flang flang/proof/checker/tests/families/citation/false-measures.forged.record - 3 не проверен по существу - - +C the cited name lives in two given modules flang/proof/checker/tests/families/citation/consumer-of-twins.flang flang/proof/checker/tests/families/citation/consumer-of-twins.record - - --зависимость flang/proof/checker/tests/families/citation/lemmas.flang flang/proof/checker/tests/families/citation/lemmas.record --зависимость flang/proof/checker/tests/families/citation/lemmas-twin.flang flang/proof/checker/tests/families/citation/lemmas-twin.record - 3 не проверен по существу - - +P forged: the cited postcondition belongs to a hidden namesake of a local function flang/proof/checker/tests/families/citation/consumer-with-namesake.flang flang/proof/checker/tests/families/citation/consumer-with-namesake.record - - --зависимость flang/proof/checker/tests/families/citation/namesake-measures.flang flang/proof/checker/tests/families/citation/namesake-measures.record - 3 не проверен по существу - - +P forged: the cited statement lives in a given module that nobody imports flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang flang/proof/checker/tests/families/citation/consumer-of-a-stranger.record - - --зависимость flang/proof/checker/tests/families/citation/measures.flang flang/proof/checker/tests/families/citation/measures.record --зависимость flang/proof/checker/tests/families/citation/lemmas.flang flang/proof/checker/tests/families/citation/lemmas.record - 3 не проверен по существу - - +C a step cites a postcondition that bounds a part of the sum flang/proof/checker/tests/families/citation/step-by-bound.flang flang/proof/checker/tests/families/citation/step-by-bound.record - - - - 0 Шагов по свойству проверено по существу 1 - - +P forged: the cited bound does not survive a subtraction flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang flang/proof/checker/tests/families/citation/step-by-bound-subtracts.record - - - - 3 вывод цели из постусловия сверщик не переиграл - - +C a postcondition under a restriction is no fact outside the restriction flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.record - - - - 3 вывод цели из постусловия сверщик не переиграл - - +say ── 4573: поле результата и поле довода в узле тождества ── - - - - - - - - - - +C an accessor returns the field bound by the pattern flang/proof/checker/tests/families/field-projection/accessor.flang flang/proof/checker/tests/families/field-projection/accessor.record - - - - 0 разбором по случаям» проиграно заново 1 (снято со слова ядра мест 2) - - +P forged: the postcondition names the other field flang/proof/checker/tests/families/field-projection/accessor-other-field.flang flang/proof/checker/tests/families/field-projection/accessor-other-field.record - - - - 3 не сошлись знак в знак - - +P forged: the pattern binds the fields the other way round flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.record - - - - 3 не сошлись знак в знак - - +C a result field is the field of the constructed value flang/proof/checker/tests/families/field-projection/result-field.flang flang/proof/checker/tests/families/field-projection/result-field.record - - - - 0 разбором по случаям» проиграно заново 1 (снято со слова ядра мест 2) - - +P forged: the postcondition claims a result field that is not the one built flang/proof/checker/tests/families/field-projection/result-field-other.flang flang/proof/checker/tests/families/field-projection/result-field-other.record - - - - 3 не сошлись знак в знак - - +say ── 1400: fmath — свободное утверждение «Т не меньше 0», ссылка на библиотеку из другого файла ── - - - - - - - - - - +C the library statements are replayed by the checker flang/stdlib/fmath.flang flang/proof/checker/tests/families/fmath/fmath.record - - - - 0 ПРОВЕРЕНО — запись сошлась - - +C a program cites two library statements, the library given flang/proof/checker/tests/families/fmath/scores.flang flang/proof/checker/tests/families/fmath/scores.record - - --зависимость flang/stdlib/fmath.flang flang/proof/checker/tests/families/fmath/fmath.record - 0 Шагов по свойству проверено по существу 2 - - +C a program cites two library statements, the library not given flang/proof/checker/tests/families/fmath/scores.flang flang/proof/checker/tests/families/fmath/scores.record - - - - 3 в этом исходнике его нет, а файл ввозит модули - - +P forged: a sum with a number of no floor is called non-negative flang/proof/checker/tests/families/fmath/sum-of-a-number.flang flang/proof/checker/tests/families/fmath/sum-of-a-number.record - - - - 3 сумма неотрицательных неотрицательна - - +P forged: a difference of lengths is called non-negative flang/proof/checker/tests/families/fmath/difference-of-lengths.flang flang/proof/checker/tests/families/fmath/difference-of-lengths.record - - - - 3 сумма длин двух строк неотрицательна - - +P forged: a restriction on one summand is taken for a floor on both flang/proof/checker/tests/families/fmath/restricted-sum.flang flang/proof/checker/tests/families/fmath/restricted-sum.record - - - - 3 сумма неотрицательных неотрицательна - - diff --git a/flang/proof/ratchets.txt b/flang/proof/ratchets.txt index f9f983e71..c8441a3e8 100644 --- a/flang/proof/ratchets.txt +++ b/flang/proof/ratchets.txt @@ -1,7 +1,7 @@ forgeries 36 forgery-numerator 155 -forgery-probes 596 -checker-code-lines 7815 +forgery-probes 611 +checker-code-lines 7949 checker-primitives 15 trap-kinds 38 trap-goals-on-kernel-word 3 diff --git a/flang/scripts/count-guard.mjs b/flang/scripts/count-guard.mjs index b43b64bd0..8da01360d 100644 --- a/flang/scripts/count-guard.mjs +++ b/flang/scripts/count-guard.mjs @@ -43,8 +43,8 @@ * * • ЧИСЛО ФАЙЛОВ он не сверяет. «AST всех 60 файлов `.flang` репозитория * напечатан до и после правки» — не утверждение о размере дерева, а запись о - * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1052 файла, но - * СНЯТО 2026-09-17 файлов *.flang = 1052 + * том, что ПОКРЫЛ прошлый прогон. Дерево с тех пор выросло до 1081 файла, но + * СНЯТО 2026-09-17 файлов *.flang = 1081 * прогон-то был на шестидесяти, и подставить туда 168 значило бы соврать про * работу, которой не делали. Отличить «столько в дереве» от «столько прошло * через прогон» нечем, кроме чтения, — значит сторож сюда не лезет. diff --git a/flang/scripts/name-guard.mjs b/flang/scripts/name-guard.mjs index ac59fe99f..7d8a928dc 100644 --- a/flang/scripts/name-guard.mjs +++ b/flang/scripts/name-guard.mjs @@ -130,8 +130,8 @@ * переставшая сравнивать, продолжает зеленеть. * * Поэтому охват ПЕЧАТАЕТСЯ каждым прогоном и закреплён тестом «охват сторожа - * назван числом»: 300 файлов из 1052. Остальные 1099 — не упущение: - * СНЯТО 2026-09-17 файлов *.flang = 1052 + * назван числом»: 300 файлов из 1081. Остальные 1099 — не упущение: + * СНЯТО 2026-09-17 файлов *.flang = 1081 * * • 503 — печать замеров (`docs/benchmark*`): * это ВЫВОД прогона, а не исходник, и правилам имени он не подчиняется; diff --git a/flang/stdlib/fmath.flang b/flang/stdlib/fmath.flang new file mode 100644 index 000000000..0d9d6dc80 --- /dev/null +++ b/flang/stdlib/fmath.flang @@ -0,0 +1,17 @@ +модуль «Fmath» + +утверждение «длина любого списка неотрицательна» + для всех л: список числа + утверждаем (длина л) не меньше 0 + +утверждение «длина любой строки неотрицательна» + для всех т: строка + утверждаем (длина т) не меньше 0 + +утверждение «сумма неотрицательных неотрицательна» + для всех а: неотрицательное и б: неотрицательное + утверждаем (а плюс б) не меньше 0 + +утверждение «сумма длин двух строк неотрицательна» + для всех а: строка и б: строка + утверждаем ((длина а) плюс (длина б)) не меньше 0 diff --git a/scripts/ledgers/file-name-words.txt b/scripts/ledgers/file-name-words.txt index 1f31ae13a..ff5d4b158 100644 --- a/scripts/ledgers/file-name-words.txt +++ b/scripts/ledgers/file-name-words.txt @@ -9,6 +9,7 @@ acceptance accepted accepts access +accessor account accumulates accumulating @@ -613,12 +614,14 @@ flatness flattened floating floor +fmath fold folds follows for foreign forever +forged forgeries forgery forgotten @@ -1018,6 +1021,7 @@ n7 name named names +namesake namesigns naming nan @@ -1454,6 +1458,7 @@ scan schedule scheduler score +scores screen script scrutinee @@ -1591,6 +1596,7 @@ stops storage stored stories +stranger strategy stray stream @@ -1620,6 +1626,7 @@ substituted substitution subtracted subtraction +subtracts success such suffix @@ -1798,6 +1805,7 @@ unreachable unreadable unreducible unregistered +unrelated unrevoked unstatable untied diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index 9a7a89aff..32d998374 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1711,3 +1711,32 @@ ba12a7e782c1bdf155b39b990c48e9a0|1|1|0|0|0|flang/proof/probes/syllogism/assumpti a8eee38c95df323b25bba18cc80c8e82|1|1|0|0|0|flang/proof/probes/syllogism/assumptions/programs/socrates-with-premises-only-in-the-theorem.flang 85eba61c3667f614954f787efe8a6bd3|1|0|0|0|0|flang/proof/probes/syllogism/assumptions/programs/undistributed-middle.flang 08cfc8c8533721f22dcd06592e2cfc1b|3|3|0|0|0|flang/proof/probes/kernel-memo/run.fscript +08dadecb64d1ad3c2991d19366373208|1|×|×|×|0|flang/proof/checker/tests/families/citation/consumer-of-a-stranger.flang +a8f3582356d643db63b442a3247682eb|1|0|0|1|0|flang/proof/checker/tests/families/citation/consumer-of-false-lemmas.flang +e0d8dc3a6077a258fd52fa78ad1497cb|1|×|×|×|0|flang/proof/checker/tests/families/citation/consumer-of-false-measures.flang +0c27275a5727f9ce93e557e1b01831af|1|×|×|×|0|flang/proof/checker/tests/families/citation/consumer-of-measures-unrelated.flang +fd17a1ce26ce2bd301dc0cd0b43df293|1|1|0|0|0|flang/proof/checker/tests/families/citation/consumer-of-measures.flang +910dd58c8a2d1c30368e5240f4eb3251|1|1|0|0|0|flang/proof/checker/tests/families/citation/consumer-of-twins.flang +6fc0f0ae042ecf7f6fc4027f3ac43324|1|×|×|×|0|flang/proof/checker/tests/families/citation/consumer-with-namesake.flang +441c2716228cab91fd58fdaeba5e6edc|1|1|0|0|0|flang/proof/checker/tests/families/citation/consumer.flang +5e47bf36289eef43739bc8559e2f1f0f|1|0|0|1|0|flang/proof/checker/tests/families/citation/false-lemmas.flang +f51c5ea1191c9bfa24242bf7c08d01db|1|×|×|×|0|flang/proof/checker/tests/families/citation/false-measures.flang +436bb918c262042b7cb575af1498c8cc|1|1|0|0|0|flang/proof/checker/tests/families/citation/lemmas-twin.flang +0d43cb4f7d74933b220ad332c21d1879|1|1|0|0|0|flang/proof/checker/tests/families/citation/lemmas.flang +42c4aec6ee34fc2f8c018ce087a02d5d|1|1|0|0|0|flang/proof/checker/tests/families/citation/measures.flang +9019e480de2f86f3cbedb1d522cab9a5|1|1|0|0|0|flang/proof/checker/tests/families/citation/namesake-measures.flang +f7593b53bb5c1feea6448642d7a93ee4|2|×|×|×|0|flang/proof/checker/tests/families/citation/step-by-bound-subtracts.flang +b909a78d4e203dc3d28d6e934804122d|2|2|0|0|0|flang/proof/checker/tests/families/citation/step-by-bound.flang +bee24a1757bb2379e78abcc1ee919cf6|2|2|0|0|0|flang/proof/checker/tests/families/citation/step-by-postcondition.flang +c25faaf80c68feb10f948be8dd2b761e|2|2|0|0|0|flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang +a848b074fe267661bfe3f1316aa8b2fd|2|×|×|×|0|flang/proof/checker/tests/families/citation/step-by-unrelated-postcondition.flang +cba7ff01e5be6222aa70291cf1823888|1|×|×|×|0|flang/proof/checker/tests/families/field-projection/accessor-other-field.flang +1afa256a140ade1fb4f0710f556d01cb|1|×|×|×|0|flang/proof/checker/tests/families/field-projection/accessor-swapped-binding.flang +c2c3d6fc379b940f0a2baccf8a3c2ca4|1|1|0|0|0|flang/proof/checker/tests/families/field-projection/accessor.flang +0c125f724f5673513efd0d8b9b1605d1|1|×|×|×|0|flang/proof/checker/tests/families/field-projection/result-field-other.flang +f8065d1d57b972e091c656779e5cad7d|1|1|0|0|0|flang/proof/checker/tests/families/field-projection/result-field.flang +23f4e082d1c2a514a9e319fdb0272bf9|4|4|0|0|0|flang/stdlib/fmath.flang +5313bb0cd8663e23ae50a33f07205966|4|3|0|1|0|flang/proof/checker/tests/families/fmath/difference-of-lengths.flang +6a0ff051db5f51bd386f210884f440d7|4|3|0|1|0|flang/proof/checker/tests/families/fmath/restricted-sum.flang +cf872d516e34dd69bc73a4e95995017f|2|2|0|0|0|flang/proof/checker/tests/families/fmath/scores.flang +1d3bc37e838ba54753e02518e95dad9b|4|3|0|1|0|flang/proof/checker/tests/families/fmath/sum-of-a-number.flang