diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index e2dff687c..31e168c82 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -1790,6 +1790,12 @@ jobs: env: FLANG_BIN: ${{ github.workspace }}/bootstrap/flang + - name: Check non-negative field + run: bootstrap/flang io flang/proof/probes/non-negative-field/run.fscript + env: + LC_ALL: C.UTF-8 + FLANG_BIN: ${{ github.workspace }}/bootstrap/flang + # ── Дорогая половина: только тег и ручной запуск ────────────────────────── korpus: name: corpus-examples diff --git a/docs/tasks/8281-a-number-does-not-narrow-to-a-natural.md b/docs/tasks/8281-a-number-does-not-narrow-to-a-natural.md index 4048ecab2..59deaefb5 100644 --- a/docs/tasks/8281-a-number-does-not-narrow-to-a-natural.md +++ b/docs/tasks/8281-a-number-does-not-narrow-to-a-natural.md @@ -1,102 +1,244 @@ --- номер: 8281 -заголовок: «Число» сужается до «нат» хоть чем-нибудь, а поле записи проверяется на самом деле -статус: свободна -исполнитель: — -ветка: — +заголовок: Поле записи неотрицательного типа принимает −7, и на этом ядро доказывает ложь +статус: сделана 29 сентября 2026 (правка в семени выпуска 0.7.23; вторая половина заявки — сужение число → нат — названа ниже и остаётся) +приоритет: P0 +исполнитель: a +ветка: a/8281-a-negative-number-in-a-non-negative-field команда: любая -карта: — +карта: Что мешает больше всего рядом: 9528 -нужность: 1 — 27 сентября 2026, flang 0.7.22: «запись «Мера» с «шаг» равным -7» при поле `неотрицательное` — check код 0 «замечаний нет», run → {"шаг":-7} код 0 +нужность: 1 — снято 27 сентября 2026 на двоичном 0.7.22: «--strict» отвечает ДОКАЗАНО, кодом 0, на утверждении «результат не меньше 0» у функции без входов, которая на деле даёт −7 --- -# 8281. «Число» сужается до «нат» хоть чем-нибудь, а поле записи проверяется +# 8281. Поле записи неотрицательного типа принимает −7, и на этом ядро доказывает ложь -Найдено при переносе раскладки оконного менеджера digitwm на спеки: девять -политик легли на язык, а десятая — сверка целой раскладки — не писалась, пока -не обошли сужение типа руками. +Приоритет P0 по `docs/zero-bug-policy.md`: вердикт лжёт — ложное утверждение +доказано. -## Что замерено +## Шаги воспроизведения -Компилятор **0.7.10**, собранный из тега `v0.7.10` (`flang --version` → -`0.7.10`). +1. Наименьшая программа — `literal.flang`: -**1. Ни одна форма не сужает `число` до `нат`.** Проверены четыре, все -отвергнуты компилятором как несовпадение типов: + ```flang + модуль «Мера» -| попытка | итог | -|---|---| -| условие `если н не меньше 0 то …` | ветвь по-прежнему даёт `число` | -| `требует «неотрицательно» н не меньше 0` | тип параметра не меняется | -| `нат плюс нат` | результат `число`, а не `нат` | -| присваивание через `пусть` | тип берётся у выражения, то есть `число` | + объект «Мера» + «шаг»: нат -**2. Единственный переход, который компилятор принимает, — поле записи -объявленного типа. И он не проверяется вовсе:** + тотальная функция «Проверка» + возвращает «Мера» + запись «Мера» с «шаг» равным -7 + ``` -```flang -объект «Мера» - «шаг»: нат +2. Ложное доказательство — `false-proof.flang`: -тотальная функция «Проверка» - возвращает «Мера» - запись «Мера» с «шаг» равным -7 -``` + ```flang + модуль «Ложь» -`flang check` на этом файле молчит и отвечает «замечаний нет»: **−7 лежит в -поле типа `нат`**. То есть единственная дверь между двумя типами не заперта. + объект «Мера» + «шаг»: неотрицательное -## Почему это важнее, чем кажется + тотальная функция «Шаг» + принимает н: неотрицательное + возвращает неотрицательное + обеспечивает «шаг не меньше нуля» результат не меньше 0 + н -`нат` объявлен в языке ради обещаний, которые иначе не выразить: «длина -неотрицательна», «шаг не уходит вниз». Обещание, опирающееся на тип, стоит -ровно столько, сколько стоит проверка этого типа. Сейчас она равна нулю в -единственном месте, где переход вообще возможен. + тотальная функция «Отрицательный шаг» + возвращает число + обеспечивает «итог не меньше нуля» результат не меньше 0 + «Шаг» от (запись «Мера» с «шаг» равным -7).«шаг» + ``` -Обходной путь, которым пришлось воспользоваться в digitwm: завести запись с -полем `нат`, зажимать отрицательное руками перед записью и разобрать это в -шапке спеки. Обход работает, но он — признание, что типу нельзя верить. +3. Команды: `flang check`, `flang check --proof --strict`, `flang run`. + Смотреть код возврата и слово вердикта. -## Как понять, что сделано +## Что происходит -```sh -# должен ОТКАЗАТЬ с названной причиной, а не молчать: -flang check <файл с «запись «Мера» с «шаг» равным -7»> -``` +Версия `flang 0.7.22`, двоичный из `gh/dev` `7e4634dec`, прогон 27 сентября +2026. Это запись «до»: так отвечает двоичный без правки. -Зелёным считается: отрицательный литерал в поле `нат` отвергнут кодом -диагностики; у хотя бы одной из четырёх форм таблицы выше появился способ -сузить `число` до `нат`, и он назван в `docs/flang/SPEC.md`. Если сужение решено НЕ -заводить — это тоже ответ, но тогда проверка поля обязана быть настоящей, а в -спецификации должно стоять, что единственный переход — через запись. +Ложное доказательство: -## ⚑ Перепроверено координатором 5 сентября — дыра ГЛУБЖЕ, чем описана +``` +$ flang check false-proof.flang --proof --strict +false-proof.flang: ДОКАЗАНО — утверждений 2: доказано 2, условно 0, сетка 0, + объявлено, не доказано 0, отвергнуто 0, нарушено 0 код 0 + постусловие «итог не меньше нуля» функции «Отрицательный шаг» — доказано + сведением цели с телом функции: правило «цель есть допущение» + +$ flang run false-proof.flang --function «Отрицательный шаг» --args '{}' +доказано: утверждений 2 +FLANG_PROPERTY: нарушено свойство «шаг не меньше нуля» функции «Шаг» код 1 + +$ flang emit false-proof.flang --target c --out outn --no-postconditions +$ echo '{"fn":"Отрицательный шаг","args":[]}' | outn/flang_cli --json +{"ok":true,"value":{"n":"-7"}} код 0 +``` -Оба примера воспроизведены дословно двоичным из dev: +У функции без входов утверждение «результат не меньше 0» ДОКАЗАНО, а значение +её −7. Рантайм сам называет доказанное свойство нарушенным. Печать без сторожей +постусловий, которая вправе их снимать именно потому, что они доказаны, отдаёт +−7 молча. + +Все случаи задачи, дословно: + +| случай | `flang check` | `flang run` | +|---|---|---| +| поле `неотрицательное` ← литерал −7 | код 0, «замечаний нет» | код 0, `{"шаг":-7}` | +| поле `нат` ← `(0 минус 7)` | код 0, «замечаний нет» | код 0, `{"шаг":-7}` | +| поле `список нат` ← `[1, (0 минус 2)]` | код 0, «замечаний нет» | код 0, `{"шаг":[1,-2]}` | +| поле `целое` ← `2.5` | код 0, «замечаний нет» | код 0, `{"шаг":2.5}` | +| поле `вес` ← `(0 минус 1)` | код 0, «замечаний нет» | код 0 | +| та же запись внутри списка `[запись …]` | код 0, «замечаний нет» | код 0 | +| параметр `неотрицательное` ← литерал −7 при вызове | код 1, `FLANG_TYPE … аргумент «н» функции «Взять»: ожидался неотрицательное, получен целое` | код 3, не запущено | +| параметр `неотрицательное` ← `--args '{"н":-7}'` | — | код 1, `FLANG_TYPE: вызов функции «Взять»: аргумент «н»: -7 вне неотрицательное` | +| поле варианта `нат` ← −7 | код 1, `FLANG_TYPE … поле «длина» варианта «Шаг»: ожидался неотрицательное, получен целое` | код 3, не запущено | +| тело `[1, -7, 3]` при `возвращает список из нат` | код 1, `FLANG_TYPE … объявлена как список неотрицательного, а тело даёт список целого` | код 3, не запущено | + +Разбор подтвердил: параметр закрыт и при проверке, и при работе; поле варианта +и элемент списка закрыты. Открыто ровно одно место — поле ЗАПИСИ, и не только +для `нат`: любой уточнённый числовой тип поля (`целое`, `вес`, `сотых`, +`список нат`) принимает что угодно того же носителя. + +## Где дыра + +`flang/self/types.flang`, на `7e4634dec`: + +- `«Сверить аргумент»` (строка 4882) — параметр: строка 4891 сверяет данное с + объявленным через `«Годится»`, направленную вложенность отрезков; +- `«Сверить поле конструктора»` (строка 5452) — поле варианта: строка 5461, + тоже `«Годится»`; +- `«Сверить поле записи»` (строка 5544) — поле записи: строка 5553 сверяет через + `«Одинаковые типы»`. Это равенство НОСИТЕЛЕЙ: `«Одинаковые виды»` (строка + 848) у двух числовых видов уходит в `случай любое то да`, границ отрезка не + смотрит. Поэтому `целое` [−7, −7] «одинаково» с `неотрицательное`. + +Шапка `«Годится»` (строка 881) обещает: «На нём стоят ровно те десять мест, где +значение ВТЕКАЕТ в объявленную позицию». Поле записи — такое место, и в +перечень не попало. + +При работе параметр сверяет `«Проверить аргументы вызова»` (строка 8523) — +только значения, пришедшие снаружи через `--args`. Записи снаружи не приходят +(`--args` — плоский объект скаляров), а внутри программы тип значения при +работе не сверяет никто: вычислитель `flang/self/interpret.flang` строит +`«Знач запись»` без имени записи (`«Завершить»`, строка 1461). + +## Что должно быть + +Значение, втекающее в поле записи, судится так же, как аргумент и поле +варианта: литерал или вычисленное значение обязано по выводу типа лежать в +объявленном отрезке, иначе отказ `FLANG_TYPE` с местом. `docs/flang/SPEC.md`, +раздел о подтипизации: «работает только на втекании значения в объявленную +позицию (аргумент, тело против `возвращает`, элемент списка, поле варианта, +накопитель свёртки)». + +## Обходной путь + +Нет такого, который закрывал бы доказательство. Зажимать значение руками перед +записью защищает только того, кто о дыре знает. + +## Стоп-кран при работе — снят, в ствол не идёт + +В первом заходе стоял отказ при работе с собственным кодом ошибки в +`flang/src/emit/c/flang_repl.c`. Координатор решил везти настоящую правку сразу, +и стоп-кран из ветки убран целиком: перехватчик в `flang_runtime.{c,h}`, +`field_guard` в `flang_repl.c`, зеркало `bootstrap/`, отпечаток семени и строка +кода в `docs/flang/SPEC.md`. Отказ при работе ложного доказательства всё равно +не чинил: `check --proof --strict` на `false-proof.flang` оставался ДОКАЗАНО. + +## Правка — сделана, в семени выпуска 0.7.23 + +В `gh/dev` правка — коммит `e9d7daa12` «fix(types): check a record field with +fits, not with equal carriers», семя с ней — `94dea9942`, выпуск 0.7.23 (тег на +`dcfd766d4`). + +Файл `flang/self/types.flang`, функция `«Сверить поле записи»` (строка 5544), +строка 5553. Правило: значение, втекающее в поле записи, — литерал или +вычисленное — обязано годиться объявленному типу поля так же, как аргумент +(`«Сверить аргумент»`, строка 4891) и поле варианта (`«Сверить поле +конструктора»`, строка 5461): ``` -запись «Мера» с «шаг» равным -7 flang check → код 0, «замечаний нет» +- (если («Одинаковые типы» от («итог».«тип») и «решённый») то … ++ (если («Годится» от («итог».«тип») и «решённый») то … ``` -**И это не всё.** В задаче сказано, что проверка молчит. На деле молчит и -ПРОГОН: +Остальное в строке не меняется: текст отказа уже есть — `поле «шаг» записи +«Мера»: ожидался неотрицательное, получен целое`. В шапке `«Годится»` (строка +881) «десять мест» становится «одиннадцать». + +Правка замерена ДО печати. В копии `bootstrap/compiler_flang.c` один вызов +`compiler_flang_odinakovye_tipy` в теле «Сверить поле записи» заменён на +`compiler_flang_goditsya`, двоичный собран во временном каталоге, и +`flang check --fast` прогнан обоими двоичными по всем 1067 файлам `*.flang` и +`*.fscript` дерева: + +- `literal.flang`, `(0 минус 7)`, запись внутри списка, `false-proof.flang` — + все дают код 1 и `FLANG_TYPE в файле …: поле «шаг» записи «Мера»: ожидался + неотрицательное, получен целое`; +- по дереву новых замечаний `поле «…» записи «…»: ожидался` — ноль; выводы + двух двоичных по файлам совпали, кроме строк хода «шагов N из M». Шесть + файлов замыкания компилятора (`flang/self/bootstrap/compiler.flang` и зонды) + не проверяются по отдельности ни тем, ни другим двоичным + (`FLANG_IMPORT_NOT_FOUND`), их модули сверены поштучно. + +## Независимый сверщик + +`flang/proof/checker/checker.c` на записи `false-proof.flang` отвечает +`НЕ ПРОВЕРЕНО`, код 3: «НЕ ВЗЯЛСЯ … утверждение «итог не меньше нуля»: значение +«по объявлению нет» — сверщик не повторяет изъятие объявленного типа, место на +слове ядра». То есть ложное утверждение он не подтверждает, но и не +опровергает. На программе, где доказано только истинное «шаг не меньше нуля» +у «Шаг», а −7 втекает в него через поле, сверщик отвечает `ПРОВЕРЕНО`, код 0: +типы программы он не переписывает, факт `Н3 ⟨н не меньше 0⟩` берёт из +объявления параметра. Подделки в `flang/proof/forgeries/manifest.tsv` не +заведено: сверщик ложь не принял, а класса «ядро ошиблось в типах, запись +честна» у набора нет. + +## Когда задача сделана + +Сделана. Прогон 29 сентября 2026, `flang 0.7.23`, двоичный из `gh/dev` +`dcfd766d4` (`make -C bootstrap -j8`): ``` -flang run --function «Проверка» --args '{}' - вывод {"шаг":-7} - КОД 0 +$ flang check literal.flang +FLANG_TYPE в файле literal.flang, строка 8, столбец 32: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое +literal.flang: не проверено — замечаний 1 код 1 +$ flang run literal.flang --function «Проверка» --args '{}' +не доказано: … замечаний проверки 1, первое — FLANG_TYPE: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое — запуск только по явному согласию: --на-веру код 3 +$ flang check false-proof.flang --proof --strict +FLANG_TYPE в файле false-proof.flang, строка 15, столбец 42: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое +false-proof.flang: не проверено — ведомость не печатается у программы с замечаниями код 1 +$ flang run false-proof.flang --function «Отрицательный шаг» --args '{}' +не доказано: … FLANG_TYPE: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое … код 3 +$ bootstrap/flang io flang/proof/probes/non-negative-field/run.fscript +поле записи против объявленного типа: проб 15, разошлось 0 код 0 ``` -Поле типа `нат` держит −7 **в работе**, и ни одна из двух дорог не -возражает. Это не «недостающая проверка при разборе», а дыра в самом типе: -значение живёт, течёт дальше и попадает в чужие обещания как `нат`. +До правки (0.7.22) те же команды давали: `check` — код 0, «замечаний нет»; +`check --proof --strict` на `false-proof.flang` — ДОКАЗАНО, код 0; проба — +«расхождений 9 из 15», код 1 (раздел «Что происходит» выше). -Для сравнения — ложное ПОСТУСЛОВИЕ прогон ловит: +Проба `flang/proof/probes/non-negative-field/run.fscript` стоит шагом «Check +non-negative field» в `.github/workflows/binary.yml` и покраснеет, если поле +записи снова станут сверять равенством носителей. -``` -обеспечивает «...» результат не меньше 5 при н=0 → КОД 1, FLANG_PROPERTY -``` +Вторая половина исходной заявки — сужение `число` → `нат` формами `если`, +`требует`, `нат плюс нат`, `пусть` — не P0 и этой правкой не решается. Теперь поле +записи перестало быть обходной дверью, и в `docs/flang/SPEC.md` +надо либо назвать форму сужения, либо записать, что её нет. + +## Где живёт правка + +- `flang/self/types.flang`, «Сверить поле записи»: `«Годится»` вместо + `«Одинаковые типы»`, шапка «Годится» — «одиннадцать мест»; в `gh/dev` + коммитом `e9d7daa12`, в двоичный — семенем `94dea9942` (0.7.23); +- проба и шаг CI — ветка `a/8281-a-negative-number-in-a-non-negative-field`. + +## История -Значит охрана постусловий в рантайме есть, а охраны сужения типа — нет. -Обходной путь «зажимать отрицательное руками» защищает только того, кто о -дыре знает. +Найдено при переносе раскладки digitwm на спеки, компилятор 0.7.10: `flang +check` на `запись «Мера» с «шаг» равным -7` молчал. 5 сентября координатор +показал, что молчит и прогон: `{"шаг":-7}`, код 0. diff --git a/flang/proof/probes/non-negative-field/run.fscript b/flang/proof/probes/non-negative-field/run.fscript new file mode 100644 index 000000000..2002abac9 --- /dev/null +++ b/flang/proof/probes/non-negative-field/run.fscript @@ -0,0 +1,262 @@ +модуль «Non-negative field probes» + +тип «Дело» + вариант «Записать» содержит путь: строка, текст: строка + вариант «Позвать» содержит программа: строка, доводы: список строки + +объект «Шаг» + «зачем»: строка + «дело»: «Дело» + «ждём»: число + «слово»: строка + «запрет»: строка + +тотальная функция «Двоичный по умолчанию» + возвращает строка + пример «путь считается от каталога плана, а не от корня дерева» + ожидается "../../../../bootstrap/flang" + "../../../../bootstrap/flang" + +тотальная функция «Образец каталога» + возвращает строка + пример «каталог заводится во временном, а не в дереве» + ожидается "/tmp/probes-non-negative-field-" + "/tmp/probes-non-negative-field-" + +тотальная функция «Строки» + принимает строки: список строки + возвращает строка + пример «строки склеиваются переводом строки» + дано строки равно ["а", "б"] + ожидается "а\nб" + соединить строки по "\n" + +тотальная функция «Мера с полем» + принимает «вид»: строка, тело: строка + возвращает строка + пример «запись с одним полем и функцией, которая её строит» + дано «вид» равно "нат" + дано тело равно "-7" + ожидается "модуль «Мера»\n\nобъект «Мера»\n «шаг»: нат\n\nтотальная функция «Проверка»\n возвращает «Мера»\n запись «Мера» с «шаг» равным -7" + «Строки» от ["модуль «Мера»", "", "объект «Мера»", (соединить [" «шаг»: ", «вид»] по ""), "", "тотальная функция «Проверка»", " возвращает «Мера»", (соединить [" запись «Мера» с «шаг» равным ", тело] по "")] + +тотальная функция «Взятие нат» + возвращает строка + «Строки» от ["модуль «Взятие»", "", "тотальная функция «Взять»", " принимает н: неотрицательное", " возвращает число", " н"] + +тотальная функция «Вызов с литералом» + возвращает строка + «Строки» от ["модуль «Вызов»", "", "тотальная функция «Взять»", " принимает н: неотрицательное", " возвращает число", " н", "", "тотальная функция «Вызов»", " возвращает число", " «Взять» от -7"] + +тотальная функция «Вариант с полем» + возвращает строка + «Строки» от ["модуль «Ход»", "", "тип «Ход»", " вариант «Стоп»", " вариант «Шаг» содержит длина: нат", "", "тотальная функция «Проверка»", " возвращает «Ход»", " вариант «Шаг» с длина равным -7"] + +тотальная функция «Список нат» + возвращает строка + «Строки» от ["модуль «Список»", "", "тотальная функция «Проверка»", " возвращает список из нат", " [1, -7, 3]"] + +тотальная функция «Ложное доказательство» + возвращает строка + пример «утверждение о функции без входов опирается на тип поля» + ожидается "модуль «Ложь»\n\nобъект «Мера»\n «шаг»: неотрицательное\n\nтотальная функция «Шаг»\n принимает н: неотрицательное\n возвращает неотрицательное\n обеспечивает «шаг не меньше нуля» результат не меньше 0\n н\n\nтотальная функция «Отрицательный шаг»\n возвращает число\n обеспечивает «итог не меньше нуля» результат не меньше 0\n «Шаг» от (запись «Мера» с «шаг» равным -7).«шаг»" + «Строки» от ["модуль «Ложь»", "", "объект «Мера»", " «шаг»: неотрицательное", "", "тотальная функция «Шаг»", " принимает н: неотрицательное", " возвращает неотрицательное", " обеспечивает «шаг не меньше нуля» результат не меньше 0", " н", "", "тотальная функция «Отрицательный шаг»", " возвращает число", " обеспечивает «итог не меньше нуля» результат не меньше 0", " «Шаг» от (запись «Мера» с «шаг» равным -7).«шаг»"] + + +тотальная функция «Настройка» + принимает дело: «Дело» + возвращает «Шаг» + обеспечивает «у настройки нет ожиданий» (результат.«зачем») равен "" + запись «Шаг» с «зачем» равным "" и «дело» равным дело и «ждём» равным 0 и «слово» равным "" и «запрет» равным "" + +тотальная функция «Файл» + принимает корень: строка, имя: строка, текст: строка + возвращает «Шаг» + «Настройка» от (вариант «Записать» с путь равным (соединить [корень, "/", имя] по "") и текст равным текст) + +тотальная функция «Доводы» + принимает двоичный: строка, корень: строка, команда: строка, имя: строка, хвост: список строки + возвращает список строки + пример «вызов идёт через env под локалью UTF-8» + дано двоичный равно "flang" + дано корень равно "/т" + дано команда равно "check" + дано имя равно "a.flang" + дано хвост равно пустой список + ожидается ["LC_ALL=C.UTF-8", "flang", "check", "/т/a.flang"] + свёртка хвост начиная с ["LC_ALL=C.UTF-8", двоичный, команда, (соединить [корень, "/", имя] по "")] как собрано и довод → (добавить довод к собрано) + +тотальная функция «Проба» + принимает зачем: строка, доводы: список строки, ждём: число, слово: строка, запрет: строка + возвращает «Шаг» + обеспечивает «проба названа тем, зачем она ставилась» (результат.«зачем») равен зачем + запись «Шаг» с «зачем» равным зачем и «дело» равным (вариант «Позвать» с программа равным "env" и доводы равным доводы) и «ждём» равным ждём и «слово» равным слово и «запрет» равным запрет + +тотальная функция «Шаги» + принимает корень: строка, двоичный: строка + возвращает список «Шаг» + обеспечивает «шагов ровно двадцать шесть» (длина результат) равен 26 + пусть проверка равно ["--function", "Проверка", "--args", "{}"] + [(«Файл» от корень и "literal.flang" и («Мера с полем» от "нат" и "-7")), + («Файл» от корень и "computed.flang" и («Мера с полем» от "нат" и "(0 минус 7)")), + («Файл» от корень и "list.flang" и («Мера с полем» от "список нат" и "[1, (0 минус 2)]")), + («Файл» от корень и "integer.flang" и («Мера с полем» от "целое" и "2.5")), + («Файл» от корень и "honest.flang" и («Мера с полем» от "нат" и "1")), + («Файл» от корень и "parameter.flang" и («Взятие нат»)), + («Файл» от корень и "call.flang" и («Вызов с литералом»)), + («Файл» от корень и "variant.flang" и («Вариант с полем»)), + («Файл» от корень и "list-body.flang" и («Список нат»)), + («Файл» от корень и "false-proof.flang" и («Ложное доказательство»)), + («Проба» от "литерал -7 в поле нат: проверка отказывает, названы поле и запись" и («Доводы» от двоичный и корень и "check" и "literal.flang" и пустой список) и 1 и "FLANG_TYPE в файле" и "замечаний нет"), + («Проба» от "литерал -7 в поле нат: отказ называет поле, запись и типы" и («Доводы» от двоичный и корень и "check" и "literal.flang" и пустой список) и 1 и "поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое" и "замечаний нет"), + («Проба» от "литерал -7 в поле нат: прогон не считает" и («Доводы» от двоичный и корень и "run" и "literal.flang" и проверка) и 3 и "FLANG_TYPE" и "{\"шаг\":-7}"), + («Проба» от "вычисленное 0 минус 7 в поле нат: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "computed.flang" и пустой список) и 1 и "поле «шаг» записи «Мера»: ожидался неотрицательное" и "замечаний нет"), + («Проба» от "вычисленное 0 минус 7 в поле нат: прогон не считает" и («Доводы» от двоичный и корень и "run" и "computed.flang" и проверка) и 3 и "FLANG_TYPE" и "{\"шаг\":-7}"), + («Проба» от "отрицательный элемент в поле список нат: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "list.flang" и пустой список) и 1 и "поле «шаг» записи «Мера»: ожидался" и "замечаний нет"), + («Проба» от "дробное в поле целое: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "integer.flang" и пустой список) и 1 и "поле «шаг» записи «Мера»: ожидался целое" и "замечаний нет"), + («Проба» от "честная запись: проверка молчит" и («Доводы» от двоичный и корень и "check" и "honest.flang" и пустой список) и 0 и "замечаний нет" и "FLANG_TYPE"), + («Проба» от "честная запись: прогон отдаёт значение" и («Доводы» от двоичный и корень и "run" и "honest.flang" и проверка) и 0 и "{\"шаг\":1}" и "FLANG_TYPE"), + («Проба» от "параметр нат получает -7 снаружи: прогон отказывает" и («Доводы» от двоичный и корень и "run" и "parameter.flang" и ["--function", "Взять", "--args", "{\"н\":-7}"]) и 1 и "-7 вне неотрицательное" и ""), + («Проба» от "параметр нат получает литерал -7: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "call.flang" и пустой список) и 1 и "ожидался неотрицательное, получен целое" и ""), + («Проба» от "поле варианта нат получает -7: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "variant.flang" и пустой список) и 1 и "поле «длина» варианта «Шаг»" и ""), + («Проба» от "список нат из литерала с -7: проверка отказывает" и («Доводы» от двоичный и корень и "check" и "list-body.flang" и пустой список) и 1 и "FLANG_TYPE" и ""), + («Проба» от "ложное доказательство: ведомость под --strict не говорит ДОКАЗАНО" и («Доводы» от двоичный и корень и "check" и "false-proof.flang" и ["--proof", "--strict"]) и 1 и "поле «шаг» записи «Мера»: ожидался неотрицательное" и "ДОКАЗАНО"), + («Проба» от "ложное доказательство: прогон не считает -7" и («Доводы» от двоичный и корень и "run" и "false-proof.flang" и ["--function", "Отрицательный шаг", "--args", "{}"]) и 3 и "FLANG_TYPE" и "-7"), + («Настройка» от (вариант «Позвать» с программа равным "rm" и доводы равным ["-rf", корень]))] + +тотальная функция «Поручение шага» + принимает шаг: «Шаг» + возвращает «Поручение» + разбор (шаг.«дело») + случай вариант «Записать» с путь как путь и текст как текст + то вариант «Записать файл» с путь равным путь и содержимое равным текст + случай вариант «Позвать» с программа как программа и доводы как доводы + то вариант «Запустить процесс» с программа равным программа и аргументы равным доводы + +тотальная функция «Сошлась ли» + принимает шаг: «Шаг», код: число, вывод: строка + возвращает признак + пример «код и слово сошлись, запрета нет» + дано шаг равно запись «Шаг» с «зачем» равным "п" и «дело» равным (вариант «Позвать» с программа равным "env" и доводы равным пустой список) и «ждём» равным 1 и «слово» равным "поле «шаг» записи «Мера»" и «запрет» равным "замечаний нет" + дано код равно 1 + дано вывод равно "FLANG_TYPE в файле a.flang, строка 8, столбец 32: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое\n" + ожидается да + пример «запрещённое слово найдено — не сошлась» + дано шаг равно запись «Шаг» с «зачем» равным "п" и «дело» равным (вариант «Позвать» с программа равным "env" и доводы равным пустой список) и «ждём» равным 0 и «слово» равным "" и «запрет» равным "ДОКАЗАНО" + дано код равно 0 + дано вывод равно "a.flang: ДОКАЗАНО — утверждений 2" + ожидается нет + (код равен (шаг.«ждём»)) и притом ((вывод содержит (шаг.«слово»)) и притом (((шаг.«запрет») равен "") или (не (вывод содержит (шаг.«запрет»))))) + +тотальная функция «Про беду» + принимает шаг: «Шаг», код: число, вывод: строка + возвращает строка + соединить [(шаг.«зачем»), ": ждали код ", (к строке (шаг.«ждём»)), " и «", (шаг.«слово»), "», вышло код ", (к строке код), " — ", вывод] по "" + +тотальная функция «Нечем смотреть» + принимает почему: строка + возвращает «Продолжение» + пример «невозможность смотреть — не приговор полю» + дано почему равно "двоичного нет на месте" + ожидается вариант «Не проверено» с код равным "FLANG_NON_NEGATIVE_FIELD_PROBES_NO_MEANS" и сообщение равным "двоичного нет на месте" + вариант «Не проверено» с код равным "FLANG_NON_NEGATIVE_FIELD_PROBES_NO_MEANS" и сообщение равным почему + +тотальная функция «Итог» + принимает беды: список строки, сделано: число + возвращает «Продолжение» + пример «все пробы сошлись — план доходит до конца» + дано беды равно пустой список + дано сделано равно 15 + ожидается вариант «Конец работы» с значение равным "поле записи против объявленного типа: проб 15, разошлось 0" + разбор беды + случай пусто + то вариант «Конец работы» с значение равным (соединить ["поле записи против объявленного типа: проб ", (к строке сделано), ", разошлось 0"] по "") + случай голова и хвост + то вариант «Провал» с код равным "FLANG_NON_NEGATIVE_FIELD_PROBES" и сообщение равным (соединить (приписать (соединить ["ПОЛЕ ЗАПИСИ НЕ СВЕРЯЕТСЯ С ТИПОМ, расхождений ", (к строке (длина беды)), " из ", (к строке сделано), ":"] по "") к беды) по "\n · ") + +тип «Ход» + вариант «Ждём двоичный» + вариант «Ждём каталог» содержит двоичный: строка + вариант «Ждём шаг» содержит шаг: «Шаг», осталось: список «Шаг», беды: список строки, сделано: число + +тотальная функция «Начать» + возвращает «Ход» + пример «первым делом спрашивается, каким двоичным мерить» + ожидается вариант «Ждём двоичный» + вариант «Ждём двоичный» + +тотальная функция «Завести» + принимает двоичный: строка + возвращает «Продолжение» + пример «каталог заводится один, и в нём вся работа» + дано двоичный равно "../../../../bootstrap/flang" + ожидается вариант «Сделать» с поручение равным (вариант «Завести временный каталог» с образец равным "/tmp/probes-non-negative-field-") и потом равным (вариант «Ждём каталог» с двоичный равным "../../../../bootstrap/flang") + вариант «Сделать» с поручение равным (вариант «Завести временный каталог» с образец равным («Образец каталога»)) и потом равным (вариант «Ждём каталог» с двоичный равным двоичный) + +тотальная функция «Пойти» + принимает очередь: список «Шаг», беды: список строки, сделано: число + возвращает «Продолжение» + разбор очередь + случай пусто + то «Итог» от беды и сделано + случай голова и хвост + то вариант «Сделать» с поручение равным («Поручение шага» от голова) и потом равным (вариант «Ждём шаг» с шаг равным голова и осталось равным хвост и беды равным беды и сделано равным сделано) + +тотальная функция «После настройки» + принимает осталось: список «Шаг», беды: список строки, сделано: число, код: число, вывод: строка + возвращает «Продолжение» + если код равен 0 + то «Пойти» от осталось и беды и сделано + иначе «Нечем смотреть» от (соединить ["настройка проб не вышла, код ", (к строке код), ": ", вывод] по "") + +тотальная функция «После процесса» + принимает шаг: «Шаг», осталось: список «Шаг», беды: список строки, сделано: число, код: число, вывод: строка + возвращает «Продолжение» + если (шаг.«зачем») равен "" + то «После настройки» от осталось и беды и сделано и код и вывод + иначе «Пойти» от осталось и (если («Сошлась ли» от шаг и код и вывод) то беды иначе (добавить («Про беду» от шаг и код и вывод) к беды)) и (сделано плюс 1) + +тотальная функция «После шага» + принимает шаг: «Шаг», осталось: список «Шаг», беды: список строки, сделано: число, отклик: «Отклик» + возвращает «Продолжение» + разбор отклик + случай вариант «Процесс завершён» с код как код и вывод как вывод и ошибки как ошибки + то «После процесса» от шаг и осталось и беды и сделано и код и (соединить [вывод, ошибки] по "") + случай вариант «Записано» с сколько как сколько + то «Пойти» от осталось и беды и сделано + случай вариант «Процесс убит» с сигнал как сигнал и вывод как вывод и ошибки как ошибки + то «Нечем смотреть» от (соединить ["шаг «", (шаг.«зачем»), "» убит сигналом ", сигнал] по "") + случай вариант «Сбой» с код как код и сообщение как сообщение + то «Нечем смотреть» от (соединить ["шаг не вышел (", код, "): ", сообщение] по "") + случай любое + то «Нечем смотреть» от "ждали ответа на шаг пробы" + +тотальная функция «Дальше» + принимает ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём двоичный» + то разбор отклик + случай вариант «Пока ничего» + то вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "FLANG_BIN") и потом равным (вариант «Ждём двоичный») + случай вариант «Значение среды» с значение как значение + то «Завести» от значение + случай вариант «Переменной среды нет» + то «Завести» от («Двоичный по умолчанию») + случай любое + то «Нечем смотреть» от "ждали ответа о переменной FLANG_BIN" + случай вариант «Ждём каталог» с двоичный как двоичный + то разбор отклик + случай вариант «Заведено» с путь как путь + то «Пойти» от («Шаги» от путь и двоичный) и пустой список и 0 + случай вариант «Сбой» с код как код и сообщение как сообщение + то «Нечем смотреть» от (соединить ["временный каталог не заведён (", код, "): ", сообщение] по "") + случай любое + то «Нечем смотреть» от "ждали временного каталога" + случай вариант «Ждём шаг» с шаг как шаг и осталось как осталось и беды как беды и сделано как сделано + то «После шага» от шаг и осталось и беды и сделано и отклик + +план «Non-negative field probes» + состояние «Ход» + начинает с «Начать» + обрабатывает «Дальше» diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index a7049be87..d7a3a53b2 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1627,6 +1627,7 @@ aa65f3785b0c62edf336a36297e30b38|1|1|0|0|0|flang/proof/probes/unproven/programs/ eb5b390d34c90eb95ad3b4382c2a3a1f|1|0|0|0|1|flang/proof/checker/tests/programs/audit-2844/unfold3-control-honest.flang b1b137536d045c4fdd205ece597d4acf|1|0|1|0|0|flang/proof/probes/orders/programs/arguments.fscript a9553eaffc7cba5c190df9e076ef0b9c|2|2|0|0|0|flang/proof/probes/io-timeout/run.fscript +5750e56d208d017c3ef036fe93fce6f7|3|3|0|0|0|flang/proof/probes/non-negative-field/run.fscript 1f4a2a844b39793dc79f661223b3dc08|1|0|1|0|0|docs/examples/io/progress-bar-on-screen.flang 227913e61eb3388807d0420cd8ec4fd3|5|5|0|0|0|flang/proof/probes/syllogism/programs/chain.flang 9ee2cd59eeca8e29bd5985c51b49e252|3|3|0|0|0|flang/proof/probes/syllogism/programs/honest.flang