diff --git a/.flangrc b/.flangrc index 52a4d2b83..2b06a626a 100644 --- a/.flangrc +++ b/.flangrc @@ -11,7 +11,7 @@ issues = https://github.com/digitable-lol/flang/issues unproven = refuse -script.build = sh scripts/bootstrap-reprint.sh --telo && make -C bootstrap -j"$(getconf _NPROCESSORS_ONLN)" && sh flang/proof/corpus-share.sh --отпечаток +script.build = sh scripts/bootstrap-reprint.sh --telo && make -C bootstrap -j"$(getconf _NPROCESSORS_ONLN)" && bootstrap/flang io flang/proof/binary-fingerprint.fscript script.scripts:check = bootstrap/flang io scripts/shortcut-collector.fscript --plan Целость && bootstrap/flang io scripts/shortcut-collector.fscript --plan Сбор --max-orders 20000 script.licenses:check = bootstrap/flang io scripts/guards/license-guard.fscript script.claims:check = bootstrap/flang io flang/scripts/claim-guard.fscript --plan 'Утверждения о недостаче сверены с лексером' --max-steps 2000000000 --max-orders 100000 --на-веру @@ -54,10 +54,10 @@ script.record-source:forgery = bootstrap/flang io scripts/guards/record-follows- script.checker:check = bootstrap/flang io flang/proof/checker/tests/run.fscript --max-steps 4000000000 --timeout 600000 script.translation:check = sh flang/translation/run.sh script.proved-share:check = sh flang/proof/corpus-share.sh --набор корпус -script.proved-share:forgery = sh flang/proof/corpus-share.sh --подлог -script.kernel-verdict:check = sh flang/proof/corpus-share.sh --приговор-ядра -script.kernel-verdict:forgery = sh flang/proof/corpus-share.sh --подлог-ядра -script.proof-records:freshness = sh flang/proof/corpus-share.sh --вложенность +script.proved-share:forgery = bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000 +script.kernel-verdict:check = bootstrap/flang io flang/proof/kernel-verdict.fscript --max-steps 4000000000 --timeout 900000 +script.kernel-verdict:forgery = bootstrap/flang io flang/proof/kernel-verdict-forgery.fscript --max-steps 4000000000 --timeout 900000 +script.proof-records:freshness = bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 script.provability = bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 script.share:replay = sh flang/proof/corpus-share.sh --проигрыванием script.share:forgery = sh flang/proof/corpus-share.sh --проигрыванием --самопроверка diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index 5c478336c..7d51f27c6 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -394,9 +394,9 @@ jobs: # # Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md, # docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН - # язык: JavaScript. Оболочка (54 файлов, 12045 строк), HTML, CSS, пробы на + # язык: JavaScript. Оболочка (54 файлов, 11512 строк), HTML, CSS, пробы на # СНЯТО 2026-09-17 файлов *.sh = 54 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17) - # СНЯТО 2026-09-17 строк-в *.sh = 12045 (задача 1400: девять проб на подлог и две честные под правила Н6 и О9 прибавили 42 строки в flang/proof/checker/tests/run.sh) (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 23372, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 23980, снято 2026-09-22) (ADR-0046: довод в шапках двух сторожей имён — сперва почему flang/proof не судится, потом почему вошёл в область — прибавил 9 строк; до него 23971, снято 2026-09-17) + # СНЯТО 2026-09-17 строк-в *.sh = 11512 (задача 1400: девять проб на подлог и две честные под правила Н6 и О9 прибавили 42 строки в flang/proof/checker/tests/run.sh) (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 23372, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 23980, снято 2026-09-22) (ADR-0046: довод в шапках двух сторожей имён — сперва почему flang/proof не судится, потом почему вошёл в область — прибавил 9 строк; до него 23971, снято 2026-09-17) # C, Python, awk и Erlang не считались нигде и ни в одной проверке. Долг, # которого никто не считает, не убывает: его не видно ни в отчёте, ни в # ленте, и растёт он молча. @@ -1460,10 +1460,12 @@ jobs: # работа охраны. - name: Probe corpus ledger run: | - if ! sh flang/proof/corpus-share.sh --подлог; then + if ! bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000; then echo "сторож ведомости промолчал на подлоге — проверять им нечего" >&2 exit 1 fi + env: + FLANG_TMP: ${{ runner.temp }} - name: Check corpus ledger run: sh flang/proof/corpus-share.sh --набор корпус @@ -1594,13 +1596,17 @@ jobs: # и прибор его для них не требует; шаг сборки чекера при коммите ae42220a2 # отсюда выпал, и `--вложенность` осталась бы без него — возвращён. - name: Record seed fingerprint - run: sh flang/proof/corpus-share.sh --отпечаток + run: bootstrap/flang io flang/proof/binary-fingerprint.fscript - name: Probe seed fingerprint - run: sh flang/proof/corpus-share.sh --подлог-отпечатка + run: bootstrap/flang io flang/proof/binary-fingerprint.fscript -- --forgery + env: + FLANG_TMP: ${{ runner.temp }} - name: Build proof checker run: make -C flang/proof/checker - name: Check corpus records - run: sh flang/proof/corpus-share.sh --вложенность + run: bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 + env: + FLANG_TMP: ${{ runner.temp }} # Предмет тут другой — сторож кодов, — но работа та же по той же причине, # по которой `imena` не стала шагом в `sborka`: сборка двоичного стоит diff --git a/.github/workflows/provability.yml b/.github/workflows/provability.yml index b6e25d0a4..5e997f866 100644 --- a/.github/workflows/provability.yml +++ b/.github/workflows/provability.yml @@ -94,7 +94,7 @@ jobs: # в обе стороны (кеш отдаёт двоичный со старым временем, checkout кладёт # семя свежим). - name: Record seed fingerprint - run: sh flang/proof/corpus-share.sh --отпечаток + run: bootstrap/flang io flang/proof/binary-fingerprint.fscript # `--вложенность` — единственная проверка этого дерева, где предмет суда # есть САМ СОБРАННЫЙ ДВОИЧНЫЙ: каждая запись корпуса печатается заново @@ -103,7 +103,7 @@ jobs: # Без этого шага вердикт ниже говорил бы о записях, напечатанных когда-то, # а не о двоичном, который выйдет в выпуск. - name: Check corpus records - run: sh flang/proof/corpus-share.sh --вложенность + run: bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 # Сторож, которого нельзя покрасить, неотличим от выключенного. Двоичный # уносится в RUNNER_TEMP и возвращается при ЛЮБОМ исходе: иначе неудача @@ -112,7 +112,7 @@ jobs: run: | set +e mv bootstrap/flang "$RUNNER_TEMP/flang.отложен" - sh flang/proof/corpus-share.sh --вложенность > "$RUNNER_TEMP/без-двоичного.log" 2>&1 + bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 > "$RUNNER_TEMP/без-двоичного.log" 2>&1 kod=$? mv "$RUNNER_TEMP/flang.отложен" bootstrap/flang cat "$RUNNER_TEMP/без-двоичного.log" diff --git a/.gitignore b/.gitignore index 56084110e..7b4680a46 100644 --- a/.gitignore +++ b/.gitignore @@ -41,7 +41,7 @@ bootstrap/*.a bootstrap/flang bootstrap/flang_cli # Отпечаток семени при двоичном (sha256 двоичного и входов сборки) — пишет -# `sh flang/proof/corpus-share.sh --отпечаток` после make; по нему прибор +# `bootstrap/flang io flang/proof/binary-fingerprint.fscript` после make; по нему прибор # `--вложенность` судит, из этого ли семени собран двоичный, не глядя на время. bootstrap/flang.seed-sha256 diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 9642c64ff..82fac7f45 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -325,7 +325,7 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000 «100 % утверждений дерева доказаны». О собранном коде оно не говорит ничего (этап 2), и о собранном ДВОИЧНОМ тоже: замер 19 сентября 2026 — `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000` печатает ДОКАЗУЕМ и кодом 0 даже тогда, когда `bootstrap/flang` из дерева убран. Двоичный судит -отдельная проверка `sh flang/proof/corpus-share.sh --вложенность`, и она заведена в ту же +отдельная проверка `bootstrap/flang io flang/proof/records-nesting.fscript`, и она заведена в ту же работу CI. Полный разбор четырёх покрытий — [`docs/four-coverages.md`](four-coverages.md). **Правила.** 109 строк перечня `flang/proof/tables/inference-rules.tsv`, у всех 109 есть лемма в @@ -511,7 +511,7 @@ make -C bootstrap -j8 собрать комп bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000 четыре покрытия порознь, с датой и SHA bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 ДОКАЗУЕМ / НЕ ДОКАЗУЕМ по четырём числам, ≈18 с sh flang/proof/corpus-share.sh --проигрыванием из чего сложена доля первого покрытия -sh flang/proof/corpus-share.sh --вложенность записи — то, что печатает СОБРАННЫЙ двоичный +bootstrap/flang io flang/proof/records-nesting.fscript записи — то, что печатает СОБРАННЫЙ двоичный bootstrap/flang run-script checker:check пробы на подлог у независимого проверяющего ./bootstrap/flang check --proof ФАЙЛ отчёт о доказательствах файла ./bootstrap/flang check --proof ФАЙЛ --записать З запись доказательства diff --git a/docs/flang/proof/checker/tests/families/by-declaration/README.md b/docs/flang/proof/checker/tests/families/by-declaration/README.md index 376efba37..15a5603c7 100644 --- a/docs/flang/proof/checker/tests/families/by-declaration/README.md +++ b/docs/flang/proof/checker/tests/families/by-declaration/README.md @@ -42,7 +42,7 @@ перепечаткой. **В корпус эти записи не положены.** Корпус обязан быть печатью семени байт в -байт — это стережёт `sh flang/proof/corpus-share.sh --вложенность` на каждом +байт — это стережёт `bootstrap/flang io flang/proof/records-nesting.fscript` на каждом пуше, и две записи шага А, положенные в корпус, покрасили его в PR #21 («РАЗОШЛАСЬ» ×2). Путь тот же, что у 6205: печать ядра живёт здесь пробой, а в корпус ложится перепечаткой партии. Доля «после перепечатки» мерится тем же diff --git a/docs/flang/proof/checker/tests/families/contradiction/README.md b/docs/flang/proof/checker/tests/families/contradiction/README.md index 3f600d1c2..c6c6738fb 100644 --- a/docs/flang/proof/checker/tests/families/contradiction/README.md +++ b/docs/flang/proof/checker/tests/families/contradiction/README.md @@ -34,4 +34,4 @@ Записи — печать ядра, снятая толкованием исходников `flang/self` семенем 0.7.19 (зонд `flang/self/bootstrap/check-with-source-compiler.flang`): семя правок `zapis.flang` не несёт, в двоичное они доедут перепечаткой (задача 5190). В корпус записи не положены — -корпус обязан быть печатью семени байт в байт (`corpus-share.sh --вложенность`). +корпус обязан быть печатью семени байт в байт (`records-nesting.fscript`). diff --git a/docs/four-coverages.md b/docs/four-coverages.md index f8452e19e..84d3772d4 100644 --- a/docs/four-coverages.md +++ b/docs/four-coverages.md @@ -38,7 +38,7 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000 - Не «100 % программ доказаны». Знаменатель — обязательства этих записей, а не ваши программы. - Не утверждение о собранном двоичном. Записи лежат в дереве готовыми; совпадают ли они с тем, что печатает `bootstrap/flang` СЕГОДНЯ, — отдельный вопрос и отдельная проверка - (`sh flang/proof/corpus-share.sh --вложенность`). + (`bootstrap/flang io flang/proof/records-nesting.fscript`). - Не «проверено всё, что есть в наборе». Часть записей проверяющий отвергает ЦЕЛИКОМ — это нарочные подделки, и их обязательства вынесены из знаменателя; сколько именно, прибор печатает отдельной строкой. diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index f5306cf60..7ea6c9908 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -76,7 +76,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| -| оболочка | 60 | 12 362 | 54 | 7 912 | +| оболочка | 60 | 11 829 | 54 | 7 379 | | C | 37 | 870 683 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | diff --git a/flang/proof/binary-fingerprint.fscript b/flang/proof/binary-fingerprint.fscript new file mode 100644 index 000000000..012aa7c59 --- /dev/null +++ b/flang/proof/binary-fingerprint.fscript @@ -0,0 +1,295 @@ +модуль «Binary fingerprint» + использует «Rules» из "../../scripts/rules.fscript" + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Reading» из "../../scripts/reading.fscript" + использует «Tables» из "../../scripts/tables.fscript" + использует «Lists» только «Соединить списки» + +объект «Look» + «binary»: строка + «seed»: строка + «sources»: признак + «make»: число + «written binary»: строка + «written seed»: строка + +тотальная функция «Root» + возвращает строка + пример «The root of the tree lies two directories up» + ожидается "../.." + "../.." + +тотальная функция «File name» + возвращает строка + пример «The fingerprint lies beside the binary» + ожидается "flang.seed-sha256" + "flang.seed-sha256" + +тотальная функция «Look command» + возвращает строка + пример «One shell line tells all a freshness verdict needs» + ожидается "cd \"$0\" || exit 2; printf 'binary %s\\n' \"$(sha256sum flang 2>/dev/null | cut -d' ' -f1)\"; printf 'seed %s\\n' \"$(/bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat | sha256sum | cut -d' ' -f1)\"; if [ -f Makefile ] && [ -f compiler_flang.c ]; then echo 'sources yes'; else echo 'sources no'; fi; make -q flang >/dev/null 2>&1; echo \"make $?\"; sed -n 's/^двоичный /written-binary /p; s/^семя /written-seed /p' flang.seed-sha256 2>/dev/null; exit 0" + "cd \"$0\" || exit 2; printf 'binary %s\\n' \"$(sha256sum flang 2>/dev/null | cut -d' ' -f1)\"; printf 'seed %s\\n' \"$(/bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat | sha256sum | cut -d' ' -f1)\"; if [ -f Makefile ] && [ -f compiler_flang.c ]; then echo 'sources yes'; else echo 'sources no'; fi; make -q flang >/dev/null 2>&1; echo \"make $?\"; sed -n 's/^двоичный /written-binary /p; s/^семя /written-seed /p' flang.seed-sha256 2>/dev/null; exit 0" + +тотальная функция «Copy command» + возвращает строка + пример «The bootstrap directory is copied with the times of its files» + ожидается "mkdir -p \"$0\" && for f in \"$1\"/*.c \"$1\"/*.h \"$1\"/Makefile \"$1\"/*.o \"$1\"/*.a \"$1\"/flang; do [ -e \"$f\" ] && cp -p \"$f\" \"$0/\"; done; [ -x \"$0/flang\" ]" + "mkdir -p \"$0\" && for f in \"$1\"/*.c \"$1\"/*.h \"$1\"/Makefile \"$1\"/*.o \"$1\"/*.a \"$1\"/flang; do [ -e \"$f\" ] && cp -p \"$f\" \"$0/\"; done; [ -x \"$0/flang\" ]" + +тотальная функция «Look of» + принимает text: строка + возвращает «Look» + пример «What the shell line printed» + дано text равно "binary aa\nseed bb\nsources yes\nmake 1\nwritten-binary aa\nwritten-seed cc\n" + ожидается запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным да и «make» равным 1 и «written binary» равным "aa" и «written seed» равным "cc" + пусть lines равно («Lines» от text) + запись «Look» с «binary» равным («Value after» от "binary " и text) и «seed» равным («Value after» от "seed " и text) и «sources» равным (не (пусто («Beginning with» от "sources yes" и lines))) и «make» равным («Count» от («Value after» от "make " и text)) и «written binary» равным («Value after» от "written-binary " и text) и «written seed» равным («Value after» от "written-seed " и text) + +тотальная функция «Verdict of» + принимает look: «Look» + возвращает строка + пример «The fingerprint names this binary and the same seed» + дано look равно запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным да и «make» равным 1 и «written binary» равным "aa" и «written seed» равным "bb" + ожидается "свежее" + пример «The fingerprint names this binary and another seed» + дано look равно запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным да и «make» равным 0 и «written binary» равным "aa" и «written seed» равным "cc" + ожидается "отстало" + пример «Without a fingerprint of this binary the times decide» + дано look равно запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным да и «make» равным 1 и «written binary» равным "zz" и «written seed» равным "bb" + ожидается "отстало" + пример «No seed sources, nothing can be stale» + дано look равно запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным нет и «make» равным 1 и «written binary» равным "" и «written seed» равным "" + ожидается "свежее" + «Chosen» от [(«When» от (не (look.«sources»)) и "свежее"), + («When» от (((look.«written binary») равен (look.«binary»)) и притом ((look.«written seed») равен (look.«seed»))) и "свежее"), + («When» от ((look.«written binary») равен (look.«binary»)) и "отстало"), + («When» от ((look.«make») равен 1) и "отстало")] и "свежее" + +тотальная функция «Fingerprint text» + принимает look: «Look» + возвращает строка + пример «Two lines: the binary and the seed it was built from» + дано look равно запись «Look» с «binary» равным "aa" и «seed» равным "bb" и «sources» равным да и «make» равным 1 и «written binary» равным "" и «written seed» равным "" + ожидается "двоичный aa\nсемя bb\n" + соединить ["двоичный ", (look.«binary»), "\nсемя ", (look.«seed»), "\n"] по "" + +тотальная функция «Probes» + возвращает список список строки + пример «Four probes and the answer each awaits» + ожидается [["кеш CI: двоичный старше по времени, семя то же", "свежее"], ["семя правлено, двоичный подмолодили: ловится по содержимому", "отстало"], ["отпечаток переписан при новом семени", "свежее"], ["отпечатка нет: по времени, двоичный старше семени", "отстало"]] + [["кеш CI: двоичный старше по времени, семя то же", "свежее"], ["семя правлено, двоичный подмолодили: ловится по содержимому", "отстало"], ["отпечаток переписан при новом семени", "свежее"], ["отпечатка нет: по времени, двоичный старше семени", "отстало"]] + +тотальная функция «Forging» + принимает answers: список «Answer» + возвращает признак + пример «Without the key the fingerprint is written» + дано answers равно пустой список + ожидается нет + не (пусто (отфильтровать («Given of» от "arguments" и answers) где word → word равен "--forgery")) + +тотальная функция «Copy» + принимает answers: список «Answer» + возвращает строка + пример «The copy lies in the work directory» + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается "/w/bootstrap" + соединить [(«Made of» от "work" и answers), "/bootstrap"] по "" + +тотальная функция «Look at» + принимает name: строка, directory: строка + возвращает «Question» + пример «The bootstrap directory of the tree is looked at from the root» + дано name равно "look" + дано directory равно "bootstrap" + ожидается запись «Question» с «name» равным "look" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && exec \"$@\"", "../..", "sh", "-c", "cd \"$0\" || exit 2; printf 'binary %s\\n' \"$(sha256sum flang 2>/dev/null | cut -d' ' -f1)\"; printf 'seed %s\\n' \"$(/bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat | sha256sum | cut -d' ' -f1)\"; if [ -f Makefile ] && [ -f compiler_flang.c ]; then echo 'sources yes'; else echo 'sources no'; fi; make -q flang >/dev/null 2>&1; echo \"make $?\"; sed -n 's/^двоичный /written-binary /p; s/^семя /written-seed /p' flang.seed-sha256 2>/dev/null; exit 0", "bootstrap"]) + «Run from» от name и («Root») и "sh" и ["-c", («Look command»), directory] + +тотальная функция «Look answer» + принимает name: строка, answers: список «Answer» + возвращает «Look» + пример «Nothing looked at» + дано name равно "look" + дано answers равно пустой список + ожидается запись «Look» с «binary» равным "" и «seed» равным "" и «sources» равным нет и «make» равным 0 и «written binary» равным "" и «written seed» равным "" + «Look of» от («Output of» от name и answers) + +тотальная функция «Shell» + принимает name: строка, command: строка, directory: строка + возвращает «Question» + пример «A shell line runs in the copy» + дано name равно "touch" + дано command равно "touch flang" + дано directory равно "/w/bootstrap" + ожидается запись «Question» с «name» равным "touch" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && touch flang", "/w/bootstrap"]) + «Run» от name и "sh" и ["-c", (соединить ["cd \"$0\" && ", command] по ""), directory] + +тотальная функция «Setup» + возвращает список «Question» + пример «The arguments and the place of temporary files» + ожидается [запись «Question» с «name» равным "arguments" и «order» равным (вариант «Прочитать доводы»), запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] + [(«Arguments» от "arguments"), («Environment» от "temporary" и "FLANG_TMP")] + +тотальная функция «Start» + принимает answers: список «Answer» + возвращает список «Question» + пример «Writing the fingerprint looks at the bootstrap directory of the tree» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "binary present" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && exec \"$@\"", "../..", "test", "-x", "bootstrap/flang"]), запись «Question» с «name» равным "look" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && exec \"$@\"", "../..", "sh", "-c", "cd \"$0\" || exit 2; printf 'binary %s\\n' \"$(sha256sum flang 2>/dev/null | cut -d' ' -f1)\"; printf 'seed %s\\n' \"$(/bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat | sha256sum | cut -d' ' -f1)\"; if [ -f Makefile ] && [ -f compiler_flang.c ]; then echo 'sources yes'; else echo 'sources no'; fi; make -q flang >/dev/null 2>&1; echo \"make $?\"; sed -n 's/^двоичный /written-binary /p; s/^семя /written-seed /p' flang.seed-sha256 2>/dev/null; exit 0", "bootstrap"])] + если «Forging» от answers + то [(«Temporary directory» от "work" и (соединить [(«Setting of» от "temporary" и "/srv/tmp" и answers), "/fingerprint."] по ""))] + иначе [(«Run from» от "binary present" и («Root») и "test" и ["-x", "bootstrap/flang"]), («Look at» от "look" и "bootstrap")] + +тотальная функция «Copying» + принимает answers: список «Answer» + возвращает список «Question» + пример «Writing the fingerprint writes it beside the binary» + дано answers равно [запись «Answer» с «name» равным "look" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "binary aa\nseed bb\nsources yes\nmake 1\n" и ошибки равным "")] + ожидается [запись «Question» с «name» равным "written" и «order» равным (вариант «Записать файл» с путь равным "../../bootstrap/flang.seed-sha256" и содержимое равным "двоичный aa\nсемя bb\n")] + если «Forging» от answers + то [(«Run from» от "copied" и («Root») и "sh" и ["-c", («Copy command»), («Copy» от answers), "bootstrap"]), («Look at» от "look 0" и («Copy» от answers))] + иначе [(«Write» от "written" и (соединить [(«Root»), "/bootstrap/", («File name»)] по "") и («Fingerprint text» от («Look answer» от "look" и answers)))] + +тотальная функция «Probe one» + принимает answers: список «Answer» + возвращает список «Question» + пример «Nothing to probe without the key» + дано answers равно пустой список + ожидается пустой список + пусть copy равно («Copy» от answers) + если не («Forging» от answers) + то пустой список + иначе [(«Write» от "fingerprint 1" и (соединить [copy, "/", («File name»)] по "") и («Fingerprint text» от («Look answer» от "look 0" и answers))), («Shell» от "aged 1" и "touch ./*.c ./*.h && touch -d '2000-01-01' flang" и copy), («Look at» от "look 1" и copy), («Shell» от "spoiled 2" и "printf '\\n/* подлог */\\n' >> compiler_flang.c && touch flang" и copy), («Look at» от "look 2" и copy)] + +тотальная функция «Probe three» + принимает answers: список «Answer» + возвращает список «Question» + пример «Nothing to probe without the key» + дано answers равно пустой список + ожидается пустой список + пусть copy равно («Copy» от answers) + если не («Forging» от answers) + то пустой список + иначе [(«Write» от "fingerprint 3" и (соединить [copy, "/", («File name»)] по "") и («Fingerprint text» от («Look answer» от "look 2" и answers))), («Look at» от "look 3" и copy), («Write» от "fingerprint 4" и (соединить [copy, "/", («File name»)] по "") и "двоичный не-тот\nсемя не-то\n"), («Shell» от "aged 4" и "touch -d '2000-01-01' flang ./*.o ./*.a" и copy), («Look at» от "look 4" и copy)] + +тотальная функция «Cleaning» + принимает answers: список «Answer» + возвращает список «Question» + пример «No work directory, nothing to clean» + дано answers равно пустой список + ожидается пустой список + если пусто («Made of» от "work" и answers) то пустой список иначе [(«Run» от "cleaned" и "rm" и ["-rf", («Made of» от "work" и answers)])] + +тотальная функция «Stage» + принимает stages: число, answers: список «Answer» + возвращает список «Question» + пример «A stage outside the plan asks nothing» + дано stages равно 9 + дано answers равно пустой список + ожидается пустой список + разбор stages + случай 5 + то «Setup» + случай 4 + то «Start» от answers + случай 3 + то «Copying» от answers + случай 2 + то «Probe one» от answers + случай 1 + то «Probe three» от answers + случай 0 + то «Cleaning» от answers + случай любое + то пустой список + +тотальная функция «Probe line» + принимает entry: список строки, answers: список «Answer» + возвращает строка + пример «An answer that was not awaited» + дано entry равно ["1", "кеш CI: двоичный старше по времени, семя то же", "свежее"] + дано answers равно [запись «Answer» с «name» равным "look 1" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "binary aa\nseed bb\nsources yes\nmake 1\nwritten-binary zz\n" и ошибки равным "")] + ожидается " ПРОВАЛ кеш CI: двоичный старше по времени, семя то же: ждали «свежее», прибор ответил «отстало»" + пусть said равно («Verdict of» от («Look answer» от (соединить ["look ", («Cell» от 1 и entry)] по "") и answers)) + если said равен («Cell» от 3 и entry) + то соединить [" сошлось ", («Cell» от 2 и entry), ": ", said] по "" + иначе соединить [" ПРОВАЛ ", («Cell» от 2 и entry), ": ждали «", («Cell» от 3 и entry), "», прибор ответил «", said, "»"] по "" + +тотальная функция «Numbered probes» + возвращает список список строки + пример «The probes are numbered from one» + ожидается [["1", "кеш CI: двоичный старше по времени, семя то же", "свежее"], ["2", "семя правлено, двоичный подмолодили: ловится по содержимому", "отстало"], ["3", "отпечаток переписан при новом семени", "свежее"], ["4", "отпечатка нет: по времени, двоичный старше семени", "отстало"]] + свёртка («Probes») начиная с (пустой список) как numbered и probe → добавить (приписать (к строке ((длина numbered) плюс 1)) к probe) к numbered + +тотальная функция «Verdict» + принимает answers: список «Answer» + возвращает «Продолжение» + пример «The fingerprint written» + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "отпечаток семени записан: bootstrap/flang.seed-sha256" + пусть lines равно (отобразить («Numbered probes») как entry → «Probe line» от entry и answers) + пусть copied равно ((«Exit code of» от "copied" и answers) равен 0) + пусть failed равно (длина (отфильтровать lines где line → line начинается с " ПРОВАЛ")) + «Chosen» от [(«When» от (не («Forging» от answers)) и (вариант «Конец работы» с значение равным "отпечаток семени записан: bootstrap/flang.seed-sha256")), + («When» от (не copied) и (вариант «Не проверено» с код равным "FLANG_FINGERPRINT_NOT_MEASURED" и сообщение равным "нет двоичного bootstrap/flang — подлог ставить не на чем")), + («When» от (failed больше 0) и (вариант «Провал» с код равным "FLANG_FINGERPRINT_FORGERY" и сообщение равным (соединить («Соединить списки» от lines и [(соединить ["подлог отпечатка: провалов ", (к строке failed)] по "")]) по "\n")))] и (вариант «Конец работы» с значение равным (соединить («Соединить списки» от lines и ["подлог отпечатка: четыре пробы сошлись — ловит семя по содержимому, а без отпечатка — по времени, как прежде"]) по "\n")) + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «No binary, nothing to write» + дано asked равно "binary present" + дано answers равно [запись «Answer» с «name» равным "binary present" и «reply» равным (вариант «Процесс завершён» с код равным 1 и вывод равным "" и ошибки равным "")] + ожидается ["нет двоичного bootstrap/flang — записывать отпечаток не при чем"] + пример «An unknown key» + дано asked равно "arguments" + дано answers равно [запись «Answer» с «name» равным "arguments" и «reply» равным (вариант «Доводы» с доводы равным ["--мягко"])] + ожидается ["не знаю ключа: --мягко; звать: bootstrap/flang io flang/proof/binary-fingerprint.fscript [-- --forgery]"] + пусть failed равно (не ((«Exit code of» от asked и answers) равен 0)) + «Chosen» от [(«When» от (asked равен "arguments") и (отобразить (отфильтровать («Given of» от "arguments" и answers) где word → не (word равен "--forgery")) как word → соединить ["не знаю ключа: ", word, "; звать: bootstrap/flang io flang/proof/binary-fingerprint.fscript [-- --forgery]"] по "")), + («When» от ((asked равен "binary present") и притом failed) и ["нет двоичного bootstrap/flang — записывать отпечаток не при чем"]), + («When» от ((asked равен "copied") и притом failed) и ["нет двоичного bootstrap/flang — подлог ставить не на чем"]), + («When» от ((asked равен "work") и притом (пусто («Made of» от "work" и answers))) и ["временный каталог не заведён: каталога из FLANG_TMP (по умолчанию /srv/tmp) нет либо он не для записи"])] и (пустой список) + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + пример «An empty queue at the last stage gives the verdict» + дано queue равно пустой список + дано stages равно 0 + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "отпечаток семени записан: bootstrap/flang.seed-sha256" + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Verdict» от answers + иначе «Proceed» от («Stage» от (stages минус 1) и answers) и (stages минус 1) и answers + +тотальная функция «Begin» + возвращает «Inquiry» + пример «Six stages lie ahead» + ожидается запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + «Begin with» от 6 + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пример «The first turn asks for the arguments» + дано inquiry равно запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + дано reply равно вариант «Пока ничего» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать доводы») и потом равным (запись «Inquiry» с «asked» равным "arguments" и «queue» равным [запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] и «stages» равным 5 и «answers» равным пустой список) + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то если пусто («Made of» от "work" и answers) + то вариант «Не проверено» с код равным "FLANG_FINGERPRINT_NOT_MEASURED" и сообщение равным голова + иначе «Proceed» от («Cleaning» от answers) и 0 и answers + случай пусто + то «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Binary fingerprint» + состояние «Inquiry» + начинает с «Begin» + обрабатывает «Next» diff --git a/flang/proof/corpus-share.sh b/flang/proof/corpus-share.sh index ee9091052..36d882400 100755 --- a/flang/proof/corpus-share.sh +++ b/flang/proof/corpus-share.sh @@ -19,9 +19,6 @@ # sh flang/proof/corpus-share.sh --набор примеры # 43, печатает ядром # sh flang/proof/corpus-share.sh --набор КАТАЛОГ # любой каталог с *.record # sh flang/proof/corpus-share.sh --оба # корпус и примеры рядом -# sh flang/proof/corpus-share.sh --вложенность # вложен ли меньший набор в больший -# sh flang/proof/corpus-share.sh --отпечаток # после make: записать отпечаток семени при двоичном -# sh flang/proof/corpus-share.sh --подлог-отпечатка # четыре пробы на признак свежести ядра # sh flang/proof/corpus-share.sh --самопроверка # десять проб на сам прибор # Ключи: # --разбор ФАЙЛ положить построчный разбор (TSV) в ФАЙЛ @@ -29,12 +26,6 @@ # --коммит X из какого коммита строить ведомость (по умолчанию HEAD) # --ведомость Ф взять готовую ведомость из файла, а не строить из коммита # --выписать-ведомость Ф положить построенную ведомость в файл -# --подлог проба порчи на саму ведомость: подделка обязана получить -# отказ, честная запись — зелёный -# --приговор-ядра ядро судит САМ ФАЙЛ: всякий исходник, названный записью -# дерева, обязан получить у ядра код 0. Нужен bootstrap/flang -# --подлог-ядра проба порчи на приговор ядра: подделка, проведённая в -# коммит вместе с записью, обязана покраснеть # # ЦЕНА ЗАМЕРА, И ГДЕ ОНА ЛЕЖИТ. Прогон чекера по 86 записям — единицы секунд. # Дорога не проверка, а ПЕЧАТЬ: сборка ядра (`make -C bootstrap`, один файл в @@ -90,7 +81,7 @@ # Ведомость удостоверяет «файл такой, каким его положили», а не «положенное # истинно», и первое здесь ПРАВДА. Ловить такое нечем, кроме одного: ядро # обязано судить сам файл. Вопрос переходит из «что проверяет чекер» в «кто и -# когда обязан прогнать ядро» — и на это заведён ключ `--приговор-ядра`. +# когда обязан прогнать ядро» — и на это заведён план `kernel-verdict.fscript`. # # ПРИГОВОР ЯДРА — ОХРАНА ОДНОСТОРОННЯЯ, и это сказано вслух. Код 1 ядра есть # ОПРОВЕРЖЕНИЕ с названным контрпримером; код 0 ядра доверия не прибавляет @@ -177,8 +168,8 @@ LC_ALL=C.UTF-8; export LC_ALL self=$0 root=$(CDPATH= cd -- "$(dirname -- "$self")/../.." && pwd) -nabor=""; dump=""; oba=0; selftest=0; vlozh=0; proigr=0 -kommit=HEAD; vedfile=""; vedout=""; podlog=0; prigovor=0; podlog_yad=0; otpechatok=0; podlog_otp=0 +nabor=""; dump=""; oba=0; selftest=0; proigr=0 +kommit=HEAD; vedfile=""; vedout="" while [ $# -gt 0 ]; do case $1 in @@ -189,12 +180,6 @@ while [ $# -gt 0 ]; do --ведомость) vedfile=${2:-}; shift 2 ;; --выписать-ведомость) vedout=${2:-}; shift 2 ;; --оба) oba=1; shift ;; - --подлог) podlog=1; shift ;; - --приговор-ядра) prigovor=1; shift ;; - --подлог-ядра) podlog_yad=1; shift ;; - --вложенность) vlozh=1; shift ;; - --отпечаток) otpechatok=1; shift ;; - --подлог-отпечатка) podlog_otp=1; shift ;; --самопроверка) selftest=1; shift ;; # Ш5: доля-ПРОИГРЫВАНИЕМ — иной вопрос, чем разряды помех Р0–Р5 этой линейки. # Не «сошлась ли запись кодом 0», а «сколько обязательств корпуса РЕАЛЬНО @@ -204,21 +189,16 @@ while [ $# -gt 0 ]; do # записей, которые чекер отверг). Ниже, в блоке `proigr`, это разобрано. --проигрыванием) proigr=1; shift ;; *) echo "линейка не знает ключа «$1»" >&2 - echo "ключи: --набор {корпус|примеры|КАТАЛОГ} --оба --вложенность --отпечаток --подлог-отпечатка --разбор ФАЙЛ --корень ПУТЬ --самопроверка" >&2 - echo " --коммит X --ведомость Ф --выписать-ведомость Ф --подлог" >&2 - echo " --приговор-ядра --подлог-ядра --проигрыванием" >&2 + echo "ключи: --набор {корпус|примеры|КАТАЛОГ} --оба --разбор ФАЙЛ --корень ПУТЬ --самопроверка" >&2 + echo " --коммит X --ведомость Ф --выписать-ведомость Ф" >&2 + echo " --проигрыванием" >&2 exit 2 ;; esac done checker=$root/flang/proof/checker/сверщик -# Отпечатку семени и его подлогу чекер не нужен: они смотрят только на -# bootstrap/. Требовать его здесь значило бы ронять шаг CI «Отпечаток семени -# записан при двоичном», стоящий ДО сборки чекера (прогон 34637639507, код 2). -if [ "$otpechatok" -eq 0 ] && [ "$podlog_otp" -eq 0 ]; then - [ -x "$checker" ] || { echo "нет чекера $checker — собрать: make -C flang/proof/checker" >&2; exit 2; } - [ "$root/flang/proof/checker/checker.c" -nt "$checker" ] && { echo "чекер $checker старше checker.c — пересобрать: make -C flang/proof/checker" >&2; exit 2; } -fi +[ -x "$checker" ] || { echo "нет чекера $checker — собрать: make -C flang/proof/checker" >&2; exit 2; } +[ "$root/flang/proof/checker/checker.c" -nt "$checker" ] && { echo "чекер $checker старше checker.c — пересобрать: make -C flang/proof/checker" >&2; exit 2; } tmp=${TMPDIR:-/tmp}/доля-корпуса.$$ mkdir -p "$tmp" || exit 2 @@ -738,7 +718,7 @@ porody() { # (1029 утверждений) таких мест НОЛЬ, значит примета чиста и краснеет # только на подделке. Полного закрытия она не даёт: подделыватель # снимет и эти строки — тогда остаётся один свидетель, печать ядра - # (`--вложенность`), и её цену надо называть отдельно. + # (`records-nesting.fscript`), и её цену надо называть отдельно. if (verd != "доказано" && (prav || obyav || sled)) pv++ inb=0; next } @@ -1269,7 +1249,7 @@ proba_snyatogo_verdikta() { # оставляет ни пустого числителя, ни приметы: строение блока законно, оба # прибора линейки сходятся, отпечаток исходника цел, приговор ядра зелен — # ядро судит ИСХОДНИК, а лгут в ЗАПИСИ. Свидетель здесь ровно один: печать - # ядра (`--вложенность`). Проба показывает дыру, а не закрывает её. + # ядра (`records-nesting.fscript`). Проба показывает дыру, а не закрывает её. snyat_chast() { awk 'BEGIN{ srezano=0 } { if (srezano < 2 && $0 ~ /^[ \t]*вердикт доказано[ \t]*$/) { print " вердикт нет вердикта"; srezano++; next } @@ -1386,7 +1366,7 @@ proba_pustogo_chislitelya() { # ── ПЕЧАТЬ ЯДРА КАК ЕДИНСТВЕННЫЙ СВИДЕТЕЛЬ ЗАПИСИ (задача 7102) ───────────── # Ведомость отвечает «тот ли это ФАЙЛ», приговор ядра — «не отвергает ли ядро # ФАЙЛ». Ни один из них не спрашивает «то ли написано в ЗАПИСИ», а разряд Г4 -# считается по записи. Спрашивает это ровно один прибор дерева — `--вложенность`: +# считается по записи. Спрашивает это ровно один прибор дерева — `records-nesting.fscript`: # он печатает запись ядром заново и сличает побайтово. Проба показывает, что он # краснеет на той самой подделке, которую два дешёвых сторожа пропускают. # ЦЕНА НАЗВАНА ЧИСЛОМ: на 86 записях корпуса — 47 секунд и собранный @@ -1423,11 +1403,11 @@ proba_pechati_yadra() { vedom_k "$rab/ч" "$rab/ч.tsv" || return 1 vedom_k "$rab/п" "$rab/п.tsv" || return 1 - sh "$self" --корень "$rab/ч" --ведомость "$rab/ч.tsv" --вложенность >"$rab/ч.out" 2>&1; k=$? + (cd "$root" && bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 -- --root "$rab/ч") >"$rab/ч.out" 2>&1; k=$? if [ "$k" -eq 0 ]; then echo "контроль: честная запись против печати ядра ЦЕЛА (побайтово, код 0)" else echo "контроль: честная запись против печати ядра ПРОВАЛ (код $k)"; bad=1; fi - sh "$self" --корень "$rab/п" --ведомость "$rab/п.tsv" --вложенность >"$rab/п.out" 2>&1; k=$? + (cd "$root" && bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 -- --root "$rab/п") >"$rab/п.out" 2>&1; k=$? if [ "$k" -eq 1 ] && /usr/bin/grep -aq 'РАЗОШЛАСЬ' "$rab/п.out"; then echo "охрана: печать ядра на той же подделке ОТВЕРГНУТА (код 1)" else @@ -1555,14 +1535,14 @@ samoproverka() { then echo "П8 ведомость знает дерево и не знает выдуманного ЦЕЛА" else echo "П8 ведомость знает дерево и не знает выдуманного ПРОВАЛ (в ведомости «$v8», у файла «$f8», выдуманный «$n8»)"; beda_sam=1; fi # П9. ПРОБА ПОРЧИ НА САМУ ВЕДОМОСТЬ, целиком — тремя прогонами линейки. - if proba_podloga; then echo "П9 подлог отвергнут, честная запись зелена ЦЕЛА" + if (cd "$root" && bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000) >/dev/null 2>&1; then echo "П9 подлог отвергнут, честная запись зелена ЦЕЛА" else echo "П9 подлог отвергнут, честная запись зелена ПРОВАЛ"; beda_sam=1; fi # П10. ПРОБА ПОРЧИ НА ПРИГОВОР ЯДРА (задача 2390), целиком — тремя прогонами. # Двоичного нет — проба НЕ ЗАСЧИТЫВАЕТСЯ ни в одну сторону, и об этом # говорится вслух: молчаливый пропуск читался бы как зелёный. if [ ! -x "$root/bootstrap/flang" ]; then echo "П10 подлог, проведённый в коммит, ловится приговором ядра НЕ ЗВАЛАСЬ (нет bootstrap/flang)" - elif podlog_yadra; then echo "П10 подлог, проведённый в коммит, ловится приговором ядра ЦЕЛА" + elif (cd "$root" && bootstrap/flang io flang/proof/kernel-verdict-forgery.fscript --max-steps 4000000000 --timeout 900000) >/dev/null 2>&1; then echo "П10 подлог, проведённый в коммит, ловится приговором ядра ЦЕЛА" else echo "П10 подлог, проведённый в коммит, ловится приговором ядра ПРОВАЛ"; beda_sam=1; fi # П11 и П12. ДВА СТОРОЖА ЛОЖНО-ЗЕЛЁНОЙ ЗАПИСИ, целиком — четырьмя прогонами # линейки. До 6 сентября 2026 линейка на такую подделку не краснела @@ -1616,515 +1596,6 @@ samoproverka() { return $beda_sam } -# ── вложены ли наборы друг в друга ────────────────────────────────────────── -# Вопрос «что считать корпусом» дешевеет вдвое, если наборы не соперники, а -# вложены. Проба печатает ядром КАЖДЫЙ исходник, названный записями корпуса, и -# сличает напечатанное с лежащим в дереве побайтово. Строка «исходник» -# нормализуется: ядро пишет путь так, как его позвали, и это не предмет спора. -# ── КТО ВПРАВЕ РАСХОДИТЬСЯ С ПЕЧАТЬЮ ЯДРА (замер 11 сентября 2026) ───── -# Прибор задуман ловить ОТСТАВШУЮ запись: исходник правили, ядро печатает -# теперь другое, а запись в дереве осталась прежней — так было дважды, и оба -# раза молча роняло долю Г4. Но ровно тем же расхождением выглядит и ПОДДЕЛКА -# класса «лжёт-запись»: запись нарочно объявляет доказанным то, чего ядро на -# этом исходнике не печатает. Для двух таких записей расхождение с печатью — -# не беда, а САМА ИХ ЛОЖЬ, ради которой они в дереве и лежат (manifest.tsv, -# класс «лжёт-запись»; 6203 §2.3 П1 и З2: носителя `segment` у довода типа -# «число» и у псевдонима к нему нет, принцип по нему ядро не печатает). -# -# Пока список не назван, прибор красен ВСЕГДА — а сторож, который не умеет -# зеленеть, не сторож: его красноту перестают читать. Замер, ради которого -# список и заведён: на этом дереве расходятся ровно эти две записи, остальные -# 86 из 88 — печать нынешнего ядра байт в байт. -# -# Список ЗАКРЫТ и двусторонен, по тому же доводу, что оговорки приговора ядра: -# открытый список — способ увести любую запись из-под сличения одной строкой. -# Запись из списка, которая СОВПАЛА с печатью, роняет прогон тоже: её ложь -# протухла (ядро стало печатать то же самое), и подделку надо перечитать, а не -# подпереть. Третья «лжёт-запись» дерева, poddelka-svyortka-nad-pustym, здесь -# НЕ названа намеренно: она — печать ядра байт в байт, а лжёт перед чекером, -# который строже печати; её место сторожит прогон проб, а не этот прибор. -# Третья в списке с 12 сентября 2026: poddelka-raznost-bez-poryadka (правило Н12, -# ADR-0032 §2, задача 1403). Её ложь сделана руками поверх печати ядра ДО -# перепечатки партии №2; после перепечатки ядро печатает иное, и расхождение -# у неё — по замыслу, как у двух соседних. Ложь цела: набор проб на неё не -# жалуется, чекер по-прежнему отвергает её кодом 1. Двусторонность списка -# действует и здесь: если печать совпадёт с записью, прогон упадёт словами -# «ложь протухла», и подделку придётся перечитать, а не подпереть. -# Четвёртая в списке с 17 сентября 2026: poddelka-svyortka-nad-pustym. До перепечатки -# 5190 она была печатью ядра байт в байт и лгала только перед чекером, который строже -# печати, — потому и стояла здесь как НЕ названная. Новое ядро (семя из 68ff03b34) -# печатает этот ход иначе, и расхождение у неё стало таким же по замыслу, как у трёх -# соседних. Ложь цела и померена: сверщик отвергает запись кодом 1 («НЕ СОШЛОСЬ: -# утверждение «свёртка по выписанному пустому есть основание»»), а набор проб не -# жалуется — «подделок 529, принято кодом 0 — 0». -PECHAT_RASHODITSYA_ZAKONNO="poddelka-nositel-chislo-segment.record -poddelka-nositel-psevdonim-ne-otrezok.record -poddelka-raznost-bez-poryadka.record -poddelka-svyortka-nad-pustym.record -poddelka-razv2-sebya.record -poddelka-razv3-raznost.record" - -# ── ОТСТАЛО ЛИ САМО ЯДРО ОТ СЕМЕНИ (замер 11 сентября 2026) ──────── -# Прибор судит записи печатью bootstrap/flang и молча верит, что двоичный -# собран из того семени, что лежит в дереве. Цена этой веры померена: -# двоичным от 10 сентября (до перепечатки семени 0ce948bfd) прибор на этом же -# дереве объявил «напечатало другое 45» — все 45 ложно, потому что записи -# догоняли НОВОЕ ядро, а печатало их СТАРОЕ. Хуже красноты то, что следует -# из неё: честный перевыпуск этих 45 старым двоичным уронил долю 625/651 до -# 308/574. Прибор обязан отказываться мерить, а не мерить неверно. -# -# ПРИЗНАК — СОДЕРЖИМОЕ, А НЕ ВРЕМЯ ФАЙЛА. Первая редакция спрашивала `make -q`, -# то есть сравнивала ВРЕМЯ двоичного со временем семени, и в CI это врало в -# обе стороны: работа guards-selftest берёт двоичный из кеша (actions/cache -# восстанавливает его со старым временем, а checkout кладёт семя свежим), и -# прибор объявлял «ЯДРО ОТСТАЛО» на двоичном, собранном ровно из этого семени -# (прогон 34614243521 на dev, код 2). А подложенный `cp` старого двоичного -# он, наоборот, пропускал — время становилось нынешним. -# -# Теперь рядом с двоичным лежит ОТПЕЧАТОК — файл bootstrap/flang.seed-sha256 -# из двух строк: sha256 самого двоичного и sha256 входов его сборки (те же -# `bootstrap/*.c`, `*.h`, `Makefile`, что в ключе кеша CI). Пишет его тот, кто -# собрал: `--отпечаток` сразу после `make` (CI и `bootstrap/flang run-script build` зовут его -# сами). Проверка: отпечаток есть и назван ИМЕННО этот двоичный — решает -# сравнение семени, и время файлов не спрашивается вовсе; отпечатка нет или -# он о другом двоичном (собрали голым `make`, отпечаток не переписали) — -# остаётся прежний признак по времени, и об этом говорится вслух. -# Что ловит и чего нет — снято `--подлог-отпечатка` (четыре пробы ниже). -OTPECHATOK_IMYA=flang.seed-sha256 - -# Входы сборки двоичного — одним отпечатком. Порядок имён закреплён `sort`, -# иначе один и тот же каталог давал бы разные отпечатки на разных машинах. -otpechatok_semeni() { # каталог bootstrap - ( cd "$1" && /bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat ) | sha256sum | cut -d' ' -f1 -} -otpechatok_faila() { sha256sum "$1" | cut -d' ' -f1; } - -# Записать отпечаток при двоичном. Зовётся ПОСЛЕ сборки тем, кто собрал; сам -# факт сборки прибор не проверяет — за это отвечает зовущий (make только что -# прошёл, либо кеш CI отдал двоичный по ключу из тех же входов). -zapisat_otpechatok() { # каталог bootstrap - [ -x "$1/flang" ] || { echo "нет двоичного $1/flang — записывать отпечаток не при чем" >&2; return 2; } - printf 'двоичный %s\nсемя %s\n' "$(otpechatok_faila "$1/flang")" "$(otpechatok_semeni "$1")" > "$1/$OTPECHATOK_IMYA" -} - -# Ответ 0 — ОТСТАЛО (как у `make -q`: «цель старше исходников»), 1 — свежее. -# Каким признаком решено, печатается в stderr: молчаливый выбор признака -# неотличим от его отсутствия. -yadro_otstalo_ot_semeni() { # каталог bootstrap - b=$1 - [ -f "$b/Makefile" ] && [ -f "$b/compiler_flang.c" ] || return 1 - if [ -f "$b/$OTPECHATOK_IMYA" ] && - [ "$(sed -n 's/^двоичный //p' "$b/$OTPECHATOK_IMYA")" = "$(otpechatok_faila "$b/flang")" ]; then - if [ "$(sed -n 's/^семя //p' "$b/$OTPECHATOK_IMYA")" = "$(otpechatok_semeni "$b")" ]; then - echo "свежесть ядра: по отпечатку семени ($OTPECHATOK_IMYA) — семя то же" >&2; return 1 - fi - echo "свежесть ядра: по отпечатку семени ($OTPECHATOK_IMYA) — семя ДРУГОЕ" >&2; return 0 - fi - echo "свежесть ядра: отпечатка при этом двоичном нет — по времени файлов (make -q); записать: $0 --отпечаток" >&2 - ( cd "$b" && make -q flang ) >/dev/null 2>&1 - [ $? -eq 1 ] -} - -# ── ПРОБА ПОРЧИ НА ОТПЕЧАТОК (--подлог-отпечатка) ───────────────────────── -# Копия bootstrap/ во временном каталоге (с временами файлов, `cp -p`), и на -# ней четыре вопроса. Ответ «свежее»/«отстало» сверяется с ожиданием; любое -# расхождение — код 1 с именем пробы. -podlog_otpechatka() { - b=$tmp/подлог-отпечатка/bootstrap; mkdir -p "$b" - for f in "$root"/bootstrap/*.c "$root"/bootstrap/*.h "$root"/bootstrap/Makefile \ - "$root"/bootstrap/*.o "$root"/bootstrap/*.a "$root"/bootstrap/flang; do - [ -e "$f" ] && cp -p "$f" "$b/" - done - [ -x "$b/flang" ] || { echo "нет двоичного $root/bootstrap/flang — подлог ставить не на чем" >&2; return 2; } - bed=0 - proba() { # имя, ожидание (свежее|отстало) - if yadro_otstalo_ot_semeni "$b" 2>/dev/null; then otvet=отстало; else otvet=свежее; fi - if [ "$otvet" = "$2" ]; then echo " сошлось $1: $otvet" - else echo " ПРОВАЛ $1: ждали «$2», прибор ответил «$otvet»"; bed=$((bed+1)); fi - } - # 1. Отпечаток записан при этом двоичном, семя то же, а время двоичного - # СТАРШЕ семени — ровно случай кеша CI. Старый признак краснел; новый — свежее. - zapisat_otpechatok "$b"; touch "$b"/*.c "$b"/*.h; touch -d '2000-01-01' "$b/flang" - proba "кеш CI: двоичный старше по времени, семя то же" свежее - # 2. Семя правлено, двоичный тот же, отпечаток прежний, а время двоичного - # НОВЕЕ семени (`cp` без -p). Старый признак пропускал; новый — отстало. - printf '\n/* подлог */\n' >> "$b/compiler_flang.c"; touch "$b/flang" - proba "семя правлено, двоичный подмолодили: ловится по содержимому" отстало - # 3. Тот же подлог, но отпечаток переписан честно ПОСЛЕ порчи семени — - # значит собрали заново, и это свежее. - zapisat_otpechatok "$b" - proba "отпечаток переписан при новом семени" свежее - # 4. Отпечатка при этом двоичном нет (он о другом файле): остаётся признак по - # времени, и он ловит двоичный старше семени. Здесь .o тоже старятся — иначе - # `make -q` спросил бы про них, а не про двоичный. - printf 'двоичный не-тот\nсемя не-то\n' > "$b/$OTPECHATOK_IMYA" - touch -d '2000-01-01' "$b/flang" "$b"/*.o "$b"/*.a - proba "отпечатка нет: по времени, двоичный старше семени" отстало - [ "$bed" -eq 0 ] || { echo "подлог отпечатка: провалов $bed" >&2; return 1; } - echo "подлог отпечатка: четыре пробы сошлись — ловит семя по содержимому, а без отпечатка — по времени, как прежде" -} - -vlozhennost() { - yadro=$root/bootstrap/flang - [ -x "$yadro" ] || { echo "нет двоичного ядра $yadro — собрать: make -C bootstrap" >&2; return 2; } - if yadro_otstalo_ot_semeni "$root/bootstrap"; then - echo "ЯДРО ОТСТАЛО ОТ СЕМЕНИ: $yadro собран не из нынешнего bootstrap/*.c, *.h, Makefile." >&2 - echo "Мерить нечем — старое ядро печатает старые записи и объявит свежие отставшими." >&2 - echo "Пересобрать: make -C bootstrap -j8 && sh $0 --отпечаток" >&2 - return 2 - fi - corp=$root/flang/proof/checker/tests/records/corpus - out=$tmp/свежие; mkdir -p "$out" - printf '%s\n' "$PECHAT_RASHODITSYA_ZAKONNO" > "$tmp/расхождение-законно.txt" - vsego=0; sovpalo=0; razoshlos=0; otkaz=0; net=0; zakonno=0; usnulo=0; spisok="" - for z in "$corp"/*.record; do - vsego=$((vsego+1)); b=$(basename "$z" .record) - d=$(grep -a -m1 '^исходник ' "$z" | cut -d' ' -f2) - if [ ! -f "$root/$d" ]; then net=$((net+1)); spisok="$spisok ИСХОДНИКА-НЕТ:$b"; continue; fi - ( cd "$root" && "$yadro" check --proof --записать "$out/$b.record" "$d" ) >/dev/null 2>&1 - if [ ! -s "$out/$b.record" ]; then otkaz=$((otkaz+1)); spisok="$spisok ПЕЧАТЬ-ОТКАЗАЛА:$b"; continue; fi - sed '2s#.*#исходник —#' "$out/$b.record" > "$tmp/a" - sed '2s#.*#исходник —#' "$z" > "$tmp/b" - if /usr/bin/grep -aqxF "$b.record" "$tmp/расхождение-законно.txt"; then - if cmp -s "$tmp/a" "$tmp/b"; then - usnulo=$((usnulo+1)); spisok="$spisok ОГОВОРКА-ПРОСНУЛАСЬ:$b" - else - zakonno=$((zakonno+1)); spisok="$spisok РАСХОДИТСЯ-ЗАКОННО:$b" - fi - continue - fi - if cmp -s "$tmp/a" "$tmp/b"; then sovpalo=$((sovpalo+1)) - else razoshlos=$((razoshlos+1)); spisok="$spisok РАЗОШЛАСЬ:$b"; fi - done - echo "записей корпуса $vsego" - echo "ядро напечатало ту же запись побайтово $sovpalo" - echo "напечатало другое $razoshlos" - echo "расходится законно (подделка «лжёт-запись», названа поимённо) $zakonno" - echo "оговорка проснулась (подделка совпала с печатью — ложь протухла) $usnulo" - echo "печать отказала $otkaz" - echo "исходника в дереве нет $net" - [ -n "$spisok" ] && printf 'поимённо:%s\n' "$spisok" - echo "" - echo "-- откуда исходники записей корпуса --" - for z in "$corp"/*.record; do grep -a -m1 '^исходник ' "$z"; done \ - | awk '{ sub(/\/[^\/]*$/,"",$2); a[$2]++ } END{ for (k in a) printf "%s\t%d\n", k, a[k] }' | sort -k2 -rn - [ $((razoshlos+otkaz+net+usnulo)) -eq 0 ] || return 1 - return 0 -} - -# ── ПРОБА ПОРЧИ НА ВЕДОМОСТЬ ──────────────────────────────────────────────── -# Сторож, которого нельзя покрасить, неотличим от выключенного. Проба строит -# ЖИВОГО подделывателя — своё дерево, свою копию честного исходника вне -# коммита, свою ложь на месте честного файла — и требует от линейки трёх -# разных ответов подряд: -# -# контроль честная запись на честном дереве — Р0, код 0 -# подлог А запись зовёт исходником файл ВНЕ коммита — Р5, код 1 -# подлог Б файл дерева подменён ложью, запись цела — Р5, код 1 -# -# Контроль обязателен: без него подлог, отвергнутый по любой посторонней -# причине, читался бы как работа охраны. Ни одна из трёх проб не пишет в -# дерево — подделыватель живёт целиком во временном каталоге. -# -# ИЗЪЯТИЕ В ОБЕ СТОРОНЫ, названное честно по половинам (замер 5 сентября 2026): -# А — настоящая дыра. Линейка ДО правки на этом же подлоге: разряд Р0 -# «ПРОВЕРЕНО», прогон зелёный, а ядро на файле дерева даёт контрпример. -# Б — линейка ДО правки на этом подлоге тоже краснела, но по другому доводу: -# у записи не сходился её СОБСТВЕННЫЙ «отпечаток256». Этот довод -# подделыватель снимает переподписью записи — прогон Л2b задачи 4820: -# запись переподписана под ложь, старая линейка зелена (код 0, «код 0 -# ПРОВЕРЕНО 27»), новая — код 1. Проба Б сторожит новую половину; своим -# изъятием на старом приборе она НЕ отличается, и это сказано вслух. -proba_podloga() { - rab=$tmp/подлог - ish=flang/proof/examples/corpus-natural.flang - zap=$root/flang/proof/checker/tests/records/corpus/corpus-natural.record - [ -f "$root/$ish" ] && [ -f "$zap" ] \ - || { echo "ПОДЛОГ НЕ СОБРАЛСЯ: нет «$ish» или его записи — поправить пробу, линейка ни при чём" >&2; return 1; } - - mkdir -p "$rab/честные" "$rab/подмена" "$rab/дерево/$(dirname "$ish")" \ - "$rab/дерево/flang/proof/checker" "$rab/дерево/свои" || return 1 - cp "$checker" "$rab/дерево/flang/proof/checker/сверщик" || return 1 - # Ложь: тот же файл, но постусловие в нём НЕ ДЕРЖИТСЯ. Ядро на нём даёт - # контрпример «нарушено свойство «сумма пары неотрицательна»». - sed 's/^ первое плюс второе$/ первое минус второе/' "$root/$ish" > "$rab/дерево/$ish" - if cmp -s "$root/$ish" "$rab/дерево/$ish"; then - echo "ПОДЛОГ НЕ СОБРАЛСЯ: строки «первое плюс второе» в «$ish» больше нет — поправить пробу, линейка ни при чём" >&2 - return 1; fi - # Нетронутая копия честного исходника, лежащая ВНЕ коммита: подделыватель - # показывает чекеру именно её, а лгать оставляет файлу дерева. - cp "$root/$ish" "$rab/дерево/свои/наглая.flang" || return 1 - cp "$zap" "$rab/честные/corpus-natural.record" || return 1 - sed 's|^исходник .*|исходник свои/наглая.flang|' "$zap" > "$rab/подмена/corpus-natural.record" - - razr() { awk -F'\t' -v r="$2" 'NR>1 && $16==r {n++} END{print n+0}' "$1"; } - bad=0 - # контроль - sh "$self" --корень "$root" --ведомость "$ved" --набор "$rab/честные" \ - --разбор "$rab/контроль.tsv" >"$rab/контроль.out" 2>&1; k=$? - if [ "$k" -eq 0 ] && [ "$(razr "$rab/контроль.tsv" Р0)" -eq 1 ]; then - echo "контроль: честная запись на честном дереве ЦЕЛА (Р0, код 0)" - else - echo "контроль: честная запись на честном дереве ПРОВАЛ (код $k, Р0=$(razr "$rab/контроль.tsv" Р0))"; bad=1; fi - # подлог А - sh "$self" --корень "$rab/дерево" --ведомость "$ved" --набор "$rab/подмена" \ - --разбор "$rab/А.tsv" >"$rab/А.out" 2>&1; k=$? - if [ "$k" -eq 1 ] && [ "$(razr "$rab/А.tsv" Р5)" -eq 1 ]; then - echo "подлог А: исходник вне коммита ОТВЕРГНУТ (Р5, код 1)" - else - echo "подлог А: исходник вне коммита ПРОШЁЛ — охраны нет (код $k, Р5=$(razr "$rab/А.tsv" Р5))"; bad=1; fi - # подлог Б - sh "$self" --корень "$rab/дерево" --ведомость "$ved" --набор "$rab/честные" \ - --разбор "$rab/Б.tsv" >"$rab/Б.out" 2>&1; k=$? - if [ "$k" -eq 1 ] && [ "$(razr "$rab/Б.tsv" Р5)" -eq 1 ]; then - echo "подлог Б: файл дерева разошёлся с коммитом ОТВЕРГНУТ (Р5, код 1)" - else - echo "подлог Б: файл дерева разошёлся с коммитом ПРОШЁЛ — охраны нет (код $k, Р5=$(razr "$rab/Б.tsv" Р5))"; bad=1; fi - [ "$bad" -eq 0 ] && echo "проба порчи на ведомость: подделка отвергнута, честная запись зелена" - return $bad -} - -# ── ПРИГОВОР ЯДРА НА САМОМ ФАЙЛЕ (задача 2390) ────────────────────────────── -# Ведомость отвечает на вопрос «тот ли это файл», и отвечает верно. Вопроса -# «а не отвергает ли ядро сам этот файл» она не задаёт вовсе — и подделыватель, -# проведший ложь в коммит вместе с записью, проходит её честно. -# -# Здесь этот вопрос задан. Всякий исходник, названный записью ДЕРЕВА, обязан -# получить у ядра код 0. Ядро зовётся на файле, чей отпечаток сошёлся с -# ведомостью коммита, — иначе судили бы правку рабочей копии. -# -# ОГОВОРКИ ЗАКРЫТЫ И ДВУСТОРОННИ. В дереве есть исходники, которые ядро обязано -# отвергать: на них стоят пробы чекера. Такой файл назван поимённо, и правило -# для него обратное — перестал отвергаться, значит проба протухла, и это тоже -# беда. Список открытым быть не может: открытый список — это способ увести -# любой файл из-под приговора одной строкой. -# -# ЗАМЕР 6 сентября 2026 (задача 2390): записи дерева называют 138 исходников, -# 30 из них лежат вне коммита (ведомость молчит, и это разряд Р5 линейки), 108 -# судимы ядром — код 0 у 101, код 1 у семи. Все семь названы ниже. -YADRO_OTVERGAET_ZAKONNO="flang/proof/forgeries/circle.flang -flang/proof/checker/tests/records/3314-conditional-by-branches/false-negation.flang -flang/proof/checker/tests/records/9991-starts-with/false-prefix.flang -flang/proof/checker/tests/records/goal-split-by-condition/p3-let-binds-a-foreign-name.flang -flang/proof/checker/tests/programs/lie-collision.flang -flang/proof/checker/tests/programs/note-instead-of-postcondition.flang -flang/proof/checker/tests/programs/intermediate-step-by-note.flang -flang/proof/checker/tests/programs/measure-not-value-zero-character-lie.flang" - -prigovor_yadra() { - yadro=$root/bootstrap/flang - [ -x "$yadro" ] || { echo "нет двоичного ядра $yadro — собрать: make -C bootstrap" >&2; return 2; } - printf '%s\n' "$YADRO_OTVERGAET_ZAKONNO" > "$tmp/оговорки.txt" - # Дела берутся ИЗ ВЕДОМОСТИ: список записей задаёт коммит, а не каталог на - # диске. Путь исходника из записи — по-прежнему только ключ поиска. - awk -F'\t' '$2 ~ /\.record$/ {print $2}' "$ved" > "$tmp/записи-дерева.txt" - : > "$tmp/дела-ядра.txt" - while IFS= read -r zrel; do - [ -f "$root/$zrel" ] || continue - d=$(/usr/bin/grep -a -m1 '^исходник ' "$root/$zrel" | cut -d' ' -f2-) - [ -n "$d" ] && printf '%s\n' "$d" - done < "$tmp/записи-дерева.txt" | sort -u > "$tmp/дела-ядра.txt" - - vsego=0; ne_iz_dereva=0; sudimo=0; zeleno=0; otvergnuto=0; ogovoreno=0; nedokazano=0 - bedy=""; usnulo="" - while IFS= read -r rel; do - [ -n "$rel" ] || continue - vsego=$((vsego+1)) - otp=$(v_sha "$rel") - if [ -z "$otp" ]; then ne_iz_dereva=$((ne_iz_dereva+1)); continue; fi - if [ ! -f "$root/$rel" ] || [ "$(sha256sum "$root/$rel" | cut -d' ' -f1)" != "$otp" ]; then - bedy="$bedy - РАЗОШЁЛСЯ С КОММИТОМ, судить нечего: $rel"; continue; fi - sudimo=$((sudimo+1)) - # 7102: судить НАДО тем же ключом, о котором спрашивает гейт. Голый `check` - # проверяет строение и типы; доказательства он не спрашивает вовсе и на - # файле, где не доказано ни одного утверждения, отвечает кодом 0. Замер 6 - # сентября 2026: из 101 файла, «принятого ядром» без ключа, 24 разворачива- - # ются в код 3 с `--proof`, 19 из них — «доказано 0». То есть прибор - # заверял файлы, на которых ядро ничего не доказало. - ( cd "$root" && "$yadro" check --proof "$rel" ) >/dev/null 2>&1; k=$? - if /usr/bin/grep -aqxF "$rel" "$tmp/оговорки.txt"; then - ogovoreno=$((ogovoreno+1)) - [ "$k" -eq 0 ] && usnulo="$usnulo - ОГОВОРКА ПРОСНУЛАСЬ (ядро больше не отвергает — проба протухла): $rel" - continue - fi - # ТРИ ИСХОДА, А НЕ ДВА, И РАЗНИЦА МЕЖДУ НИМИ — ВСЯ ОХРАНА. Код 1 ядра есть - # ОПРОВЕРЖЕНИЕ с названным контрпримером: он снимает сертификат, и на нём - # прогон краснеет. Код 3 — «не доказано»: это не вина файла, а тот же - # пустой числитель, только со стороны ядра, и записывать его в вину значило - # бы уронить прогон на всех пробах подделок, которые в дереве лежат - # законно. Поэтому он считается ОТДЕЛЬНО и печатается числом: молчать о нём - # нельзя, судить им — тоже. - if [ "$k" -eq 0 ]; then zeleno=$((zeleno+1)) - elif [ "$k" -eq 3 ]; then nedokazano=$((nedokazano+1)) - else - otvergnuto=$((otvergnuto+1)) - bedy="$bedy - ЯДРО ОТВЕРГАЕТ ФАЙЛ (код $k), а запись о нём лежит в дереве: $rel" - fi - done < "$tmp/дела-ядра.txt" - - echo "═══ ПРИГОВОР ЯДРА НА ФАЙЛАХ, НАЗВАННЫХ ЗАПИСЯМИ ═══" - echo "ведомость дела $vedimya" - echo "исходников названо записями дерева $vsego" - echo " из них дела в дереве нет (ведомость молчит) $ne_iz_dereva" - echo "судимо ядром $sudimo" - echo " ядро приняло (код 0) $zeleno" - echo " ядро приняло, но НЕ ДОКАЗАЛО ничего (код 3 с --proof) $nedokazano" - echo " ядро отвергло, оговорено поимённо $ogovoreno" - echo " ЯДРО ОТВЕРГЛО БЕЗ ОГОВОРКИ $otvergnuto" - [ -n "$bedy" ] && printf '%s\n' "$bedy" - [ -n "$usnulo" ] && printf '%s\n' "$usnulo" - if [ -n "$bedy" ] || [ -n "$usnulo" ]; then - echo "" - echo "ЯДРО СУДИТ ФАЙЛ САМО: запись о файле, который ядро отвергает, проверенной не считается" - return 1 - fi - echo "приговор ядра: ни один судимый файл ядром не опровергнут, оговорки на месте" - echo " (это ВСЯ охрана: «не опровергнут» — не «доказан». Файлов, на которых" - echo " ядро не доказало ничего, здесь $nedokazano, и они прошли эту дверь честно.)" - return 0 -} - -# Шапка исходника ТЕМ ЖЕ СЧЁТОМ, что у чекера (`checker.c`: znakov, otpechatok): -# строк, знаков-кодовых-точек, два многочлена, SHA-256. Нужна только пробе — -# подделыватель переподписывает шапку записи, и проба обязана уметь то же. -shapka_ishodnika() { - od -An -tu1 -v < "$1" | awk -v sha="$(sha256sum "$1" | cut -d' ' -f1)" ' - { for (i = 1; i <= NF; i++) b[++n] = $i + 0 } - END{ - strok = 1; znakov = 0; h1 = 7; h2 = 7; i = 1 - while (i <= n) { - v = b[i] - if (v < 128) { c = v; k = 1 } - else if (v < 224) { c = v % 32; k = 2 } - else if (v < 240) { c = v % 16; k = 3 } - else { c = v % 8; k = 4 } - for (j = 1; j < k; j++) c = c * 64 + (b[i+j] % 64) - i += k; znakov++ - if (c == 10) strok++ - h1 = (h1 * 131 + c) % 1000000007 - h2 = (h2 * 137 + c) % 998244353 - } - printf "%d %d %d %d %s\n", strok, znakov, h1, h2, sha - }' -} - -# ── ПРОБА ПОРЧИ НА ПРИГОВОР ЯДРА ──────────────────────────────────────────── -# Подделыватель здесь не подменяет дела и не лжёт в записи НИ ОДНИМ ПОЛЕМ. Он -# дописывает к честному исходнику функцию с ложным постусловием и добавляет в -# запись честное утверждение о ней — «нет вердикта». Оба файла кладутся в -# коммит; ведомость подтверждает их обоих, чекер даёт код 0 «ПРОВЕРЕНО», ядро -# на файле даёт код 1 с названным контрпримером. -# -# Три ответа подряд, и средний — не охрана, а ПОКАЗАННАЯ ДЫРА: -# контроль честный файл — линейка Р0 код 0, приговор ядра код 0 -# дыра подделка в коммите — линейка Р0 код 0 (ведомость её НЕ ловит) -# охрана та же подделка — приговор ядра код 1 -# Без контроля покрасневший приговор читался бы как работа охраны на чём -# угодно; без «дыры» — нельзя было бы показать, что ведомости тут не хватает. -podlog_yadra() { - yadro=$root/bootstrap/flang - [ -x "$yadro" ] || { echo "нет двоичного ядра $yadro — собрать: make -C bootstrap" >&2; return 2; } - rab=$tmp/подлог-ядра - ish=flang/proof/examples/corpus-natural.flang - zap=$root/flang/proof/checker/tests/records/corpus/corpus-natural.record - [ -f "$root/$ish" ] && [ -f "$zap" ] \ - || { echo "ПОДЛОГ НЕ СОБРАЛСЯ: нет «$ish» или его записи — поправить пробу, линейка ни при чём" >&2; return 1; } - - for d in ч г; do - mkdir -p "$rab/$d/$(dirname "$ish")" "$rab/$d/records" "$rab/$d/flang/proof/checker" "$rab/$d/bootstrap" || return 1 - cp "$checker" "$rab/$d/flang/proof/checker/сверщик" || return 1 - ln -sf "$yadro" "$rab/$d/bootstrap/flang" || return 1 - done - cp "$root/$ish" "$rab/ч/$ish" || return 1 - cp "$zap" "$rab/ч/records/проба.record" || return 1 - - # Ложь дописывается В КОНЕЦ: номера строк честной части не съезжают, и чекеру - # нечего заметить. Постусловие ложно по IEEE-754 — «не число» живёт в типе - # «число» и стоит вне порядка; ядро называет контрпример словами. - { cat "$root/$ish" - printf '\nтотальная функция «Ложь 2390»\n принимает первое: число, второе: число\n' - printf ' возвращает число\n обеспечивает «ложь 2390 неотрицательна» результат не меньше 0\n' - printf ' первое плюс второе\n'; } > "$rab/г/$ish" - ( cd "$rab/г" && ./bootstrap/flang check "$ish" ) >/dev/null 2>&1 - if [ $? -eq 0 ]; then - echo "ПОДЛОГ НЕ СОБРАЛСЯ: ядро приняло файл с ложным постусловием — поправить пробу, линейка ни при чём" >&2 - return 1; fi - nl=$(/usr/bin/grep -an '^ обеспечивает «ложь 2390' "$rab/г/$ish" | cut -d: -f1) - [ -n "$nl" ] || { echo "ПОДЛОГ НЕ СОБРАЛСЯ: дописка не легла в файл" >&2; return 1; } - nf=$(/usr/bin/grep -an '^тотальная функция «Ложь 2390»' "$rab/г/$ish" | cut -d: -f1) - [ -n "$nf" ] || { echo "ПОДЛОГ НЕ СОБРАЛСЯ: заголовок дописки не лёг в файл" >&2; return 1; } - # Запись остаётся ЧЕСТНОЙ: «нет вердикта» — правда, шапка пересчитана честно. - # С 7 сентября 2026 запись несёт блоки «тотальность …» (после утверждений, до - # «конец записи») и шапку «тотальностей N», и сверщик сличает то и другое с - # исходником. Подлог обязан быть записью ТОЙ ЖЕ формы: утверждение — перед - # первым блоком тотальности, своя тотальность «Ложь 2390» (та же композиция - # через «плюс», что у «Сумма пары») — перед «конец записи», счётчик +1. - # Прежняя редакция клала утверждение после тотальностей, и сверщик отвечал - # «тотальность записана не целиком: вид 2, конец 1» — проба ломалась на форме - # записи (Р3, код 1), а не показывала дыру; П10 была красна с перепечатки. - set -- $(shapka_ishodnika "$rab/г/$ish") - awk -v s="$1" -v z="$2" -v p1="$3" -v p2="$4" -v sh="$5" -v nl="$nl" -v nf="$nf" ' - function utv() { - printf "утверждение «ложь 2390 неотрицательна» функции «Ложь 2390» строка %s\n", nl - print " вид postcondition"; print " вердикт нет вердикта" - print " теоремы нет"; print "конец утверждения"; print ""; ulozheno = 1 } - /^строк / { print "строк " s; next } - /^знаков / { print "знаков " z; next } - /^отпечаток256 /{ print "отпечаток256 " sh; next } - /^отпечаток / { print "отпечаток " p1 " " p2; next } - /^утверждений / { print "утверждений " ($2 + 1); next } - /^тотальностей /{ print "тотальностей " ($2 + 1); next } - /^тотальность «/{ if (!ulozheno) utv() } - /^конец записи$/{ if (!ulozheno) utv() - printf "тотальность «Ложь 2390» строка %s\n", nf - print " вид composition"; print " зовёт примитив «плюс»" - print " самовызова нет"; print " конец тотальности" - print; next } - { print }' "$zap" > "$rab/г/records/проба.record" - - vedom() { # каталог → ведомость того же вида, что строит git archive - ( cd "$1" && find . -type f \( -name '*.flang' -o -name '*.record' \) -print0 \ - | LC_ALL=C sort -z | xargs -0 sha256sum ) | sed 's| \./|\t|' > "$2" - } - vedom "$rab/ч" "$rab/ч.tsv" || return 1 - vedom "$rab/г" "$rab/г.tsv" || return 1 - - razr() { awk -F'\t' -v r="$2" 'NR>1 && $16==r {n++} END{print n+0}' "$1"; } - bad=0 - sh "$self" --корень "$rab/ч" --ведомость "$rab/ч.tsv" --набор "$rab/ч/records" \ - --разбор "$rab/ч.tsv.разбор" >"$rab/ч.out" 2>&1; k=$? - sh "$self" --корень "$rab/ч" --ведомость "$rab/ч.tsv" --приговор-ядра >"$rab/ч.ядро" 2>&1; ky=$? - if [ "$k" -eq 0 ] && [ "$(razr "$rab/ч.tsv.разбор" Р0)" -eq 1 ] && [ "$ky" -eq 0 ]; then - echo "контроль: честный файл в коммите ЦЕЛА (линейка Р0 код 0, приговор ядра код 0)" - else - echo "контроль: честный файл в коммите ПРОВАЛ (линейка код $k, Р0=$(razr "$rab/ч.tsv.разбор" Р0), приговор код $ky)"; bad=1; fi - - sh "$self" --корень "$rab/г" --ведомость "$rab/г.tsv" --набор "$rab/г/records" \ - --разбор "$rab/г.tsv.разбор" >"$rab/г.out" 2>&1; k=$? - if [ "$k" -eq 0 ] && [ "$(razr "$rab/г.tsv.разбор" Р0)" -eq 1 ]; then - echo "дыра: ложь в коммите, ведомость её НЕ ловит ПОКАЗАНА (линейка Р0 код 0, Р5 ноль)" - else - echo "дыра: ложь в коммите, ведомость её НЕ ловит НЕ ПОКАЗАНА (код $k, Р0=$(razr "$rab/г.tsv.разбор" Р0)) — подделка не собралась либо линейку правили"; bad=1; fi - - sh "$self" --корень "$rab/г" --ведомость "$rab/г.tsv" --приговор-ядра >"$rab/г.ядро" 2>&1; ky=$? - if [ "$ky" -eq 1 ] && /usr/bin/grep -aq 'ЯДРО ОТВЕРГАЕТ ФАЙЛ' "$rab/г.ядро"; then - echo "охрана: приговор ядра на той же подделке ОТВЕРГНУТА (код 1)" - else - echo "охрана: приговор ядра на той же подделке ПРОШЛА — охраны нет (код $ky)"; bad=1; fi - - [ "$bad" -eq 0 ] && echo "проба порчи на приговор ядра: дыра показана, охрана краснеет, честный файл зелен" - return $bad -} - -if [ "$podlog" -eq 1 ]; then proba_podloga; exit $?; fi -if [ "$prigovor" -eq 1 ]; then prigovor_yadra; exit $?; fi -if [ "$podlog_yad" -eq 1 ]; then podlog_yadra; exit $?; fi -if [ "$vlozh" -eq 1 ]; then vlozhennost; exit $?; fi -if [ "$otpechatok" -eq 1 ]; then zapisat_otpechatok "$root/bootstrap" && echo "отпечаток семени записан: bootstrap/$OTPECHATOK_IMYA"; exit $?; fi -if [ "$podlog_otp" -eq 1 ]; then podlog_otpechatka; exit $?; fi if [ "$selftest" -eq 1 ]; then samoproverka; exit $?; fi pechat_primerov() { @@ -2162,9 +1633,5 @@ case ${nabor:-} in *) izmerit "каталог $nabor" "$nabor" из-записи ;; esac # короткая команда «proved-share:check» sh --набор корпус — дело чекеру называет дерево, а не проверяемая запись: путь исходника и его отпечаток берутся из описи коммита; запись, назвавшая исходником не то, что лежит в коммите, роняет прогон -# короткая команда «proved-share:forgery» sh --подлог — проверка описи краснеет на живом подделывателе — своё дерево, копия честного исходника вне коммита, ложь на месте честного файла — и зеленеет на честной записи -# короткая команда «kernel-verdict:check» sh --приговор-ядра — ядро судит САМ ФАЙЛ: всякий исходник, названный записью дерева, обязан получить у ядра код 0, иначе запись о нём проверенной не считается; опись коммита этого не ловит и поймать не может -# короткая команда «kernel-verdict:forgery» sh --подлог-ядра — подделка, проведённая в коммит вместе с честной записью: опись её пропускает — это показано прогоном, — а приговор ядра краснеет -# короткая команда «proof-records:freshness» sh --вложенность — ядро печатает заново каждый исходник, названный записями набора программ, и напечатанное сличается с записью в дереве байт в байт. ЛОВИТ ДВЕ РАЗНЫЕ БЕДЫ. Первая: запись отстала от нынешней печати ядра — так было дважды, и оба раза молча роняло долю Г4. Вторая: запись подделана снятием слова «вердикт доказано» вместе со следами — на такой подделке это ЕДИНСТВЕННАЯ улика дерева, потому что исходник цел и обе дешёвые проверки зелены: опись спрашивает «тот ли ФАЙЛ», приговор ядра — «не отвергает ли ядро ФАЙЛ», а лжёт ЗАПИСЬ (показано прогоном 7102 и повторено здесь: контроль код 0, та же запись со снятым вердиктом — код 1 и РАЗОШЛАСЬ поимённо, опись на обеих код 0). НЕ ЛОВИТ отставания самого ДВОИЧНОГО от flang/self: отстал двоичный — записи совпадут с ним байт в байт и проба будет зелена честно; на это отвечает sh scripts/bootstrap-reprint.sh --bystro --strogo, и сегодня оно не нулевое. Цена: 46–47 с на 86 записей плюс собранный bootstrap/flang — дороже прочих дешёвых проверок, оттого место в CI, а не в хуке # короткая команда «share:replay» sh --проигрыванием — проверка 2 доказуемости числом: доля-проигрыванием = Σ «сведений проиграно заново» / Σ «утверждений» по 86 записям набора программ. Мерит РЕАЛЬНО проигранное записанными ходами (числитель растёт только на честной игре, калькулятор perepiskoy/razborom_celi в него не пишет), а не «сошлась ли запись кодом 0», как разряды Р0–Р5 той же линейки. Сегодня мало и честно: ходы несёт лишь тождество С1–С5, маршрут «по объявлению»/композиция ходов не печатает и уходит в знаменатель на слово ядра # короткая команда «share:forgery» sh --проигрыванием --самопроверка — проба по числу: у записи-носителя снимаются записанные ходы, и числитель обязан упасть — иначе прибор держал бы долю на снятых ходах и мерил бы вердикт, а не игру diff --git a/flang/proof/kernel-verdict-forgery.fscript b/flang/proof/kernel-verdict-forgery.fscript new file mode 100644 index 000000000..95fd7260f --- /dev/null +++ b/flang/proof/kernel-verdict-forgery.fscript @@ -0,0 +1,361 @@ +модуль «Kernel verdict forgery» + использует «Rules» из "../../scripts/rules.fscript" + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Reading» из "../../scripts/reading.fscript" + использует «Tables» из "../../scripts/tables.fscript" + использует «Lists» только «Соединить списки» + +объект «Head» + «lines»: число + «signs»: число + «first»: число + «second»: число + +объект «Rewrite» + «lines»: список строки + «placed»: признак + +тотальная функция «Source» + возвращает строка + пример «The source the probe spoils» + ожидается "flang/proof/examples/corpus-natural.flang" + "flang/proof/examples/corpus-natural.flang" + +тотальная функция «Record» + возвращает строка + пример «The record of that source» + ожидается "flang/proof/checker/tests/records/corpus/corpus-natural.record" + "flang/proof/checker/tests/records/corpus/corpus-natural.record" + +тотальная функция «Lie» + возвращает строка + пример «A total function with a false postcondition» + ожидается "\nтотальная функция «Ложь 2390»\n принимает первое: число, второе: число\n возвращает число\n обеспечивает «ложь 2390 неотрицательна» результат не меньше 0\n первое плюс второе\n" + "\nтотальная функция «Ложь 2390»\n принимает первое: число, второе: число\n возвращает число\n обеспечивает «ложь 2390 неотрицательна» результат не меньше 0\n первое плюс второе\n" + +тотальная функция «Build command» + возвращает строка + пример «Two small trees share the checker and the kernel» + ожидается "for d in honest forged; do mkdir -p \"$0/$d/flang/proof/examples\" \"$0/$d/records\" \"$0/$d/flang/proof/checker\" \"$0/$d/bootstrap\" && cp \"$1/flang/proof/checker/сверщик\" \"$0/$d/flang/proof/checker/сверщик\" && ln -sf \"$1/bootstrap/flang\" \"$0/$d/bootstrap/flang\" || exit 1; done; cp \"$1/flang/proof/examples/corpus-natural.flang\" \"$0/honest/flang/proof/examples/\" && cp \"$1/flang/proof/checker/tests/records/corpus/corpus-natural.record\" \"$0/honest/records/probe.record\"" + "for d in honest forged; do mkdir -p \"$0/$d/flang/proof/examples\" \"$0/$d/records\" \"$0/$d/flang/proof/checker\" \"$0/$d/bootstrap\" && cp \"$1/flang/proof/checker/сверщик\" \"$0/$d/flang/proof/checker/сверщик\" && ln -sf \"$1/bootstrap/flang\" \"$0/$d/bootstrap/flang\" || exit 1; done; cp \"$1/flang/proof/examples/corpus-natural.flang\" \"$0/honest/flang/proof/examples/\" && cp \"$1/flang/proof/checker/tests/records/corpus/corpus-natural.record\" \"$0/honest/records/probe.record\"" + +тотальная функция «Ledger command» + возвращает строка + пример «A ledger of the same kind as one built from a commit» + ожидается "(cd \"$0\" && find . -type f \\( -name '*.flang' -o -name '*.record' \\) -print0 | LC_ALL=C sort -z | xargs -0 sha256sum) | sed 's| \\./|\\t|' > \"$1\"" + "(cd \"$0\" && find . -type f \\( -name '*.flang' -o -name '*.record' \\) -print0 | LC_ALL=C sort -z | xargs -0 sha256sum) | sed 's| \\./|\\t|' > \"$1\"" + +тотальная функция «Root» + возвращает строка + пример «The tree lies two directories up» + ожидается "../.." + "../.." + +тотальная функция «Work» + принимает answers: список «Answer» + возвращает строка + пример «No work directory yet» + дано answers равно пустой список + ожидается "" + «Made of» от "work" и answers + +тотальная функция «In work» + принимает name: строка, answers: список «Answer» + возвращает строка + пример «A file in the work directory» + дано name равно "honest.tsv" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается "/w/honest.tsv" + соединить [(«Work» от answers), "/", name] по "" + +тотальная функция «Absolute root» + принимает answers: список «Answer» + возвращает строка + пример «The root as the shell sees it» + дано answers равно [запись «Answer» с «name» равным "root" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "/t\n" и ошибки равным "")] + ожидается "/t" + «First line» от («Output of» от "root" и answers) + +тотальная функция «Head of» + принимает text: строка + возвращает «Head» + пример «Two lines of two signs, counted as the checker counts them» + дано text равно "a\n" + ожидается запись «Head» с «lines» равным 2 и «signs» равным 2 и «first» равным 132844 и «second» равным 144682 + пусть codes равно (отобразить (разложить text на символы) как sign → код символа sign) + запись «Head» с «lines» равным (длина (разделить text по "\n")) и «signs» равным (длина codes) и «first» равным (свёртка codes начиная с 7 как h и code → ((h умножить на 131) плюс code) остаток от 1000000007) и «second» равным (свёртка codes начиная с 7 как h и code → ((h умножить на 137) плюс code) остаток от 998244353) + +тотальная функция «Line of» + принимает text: строка, start: строка + возвращает строка + пример «The number of the first line that starts so» + дано text равно "a\nб\nб\n" + дано start равно "б" + ожидается "2" + «Cell» от 1 и (отобразить (отфильтровать («Numbered» от (разделить text по "\n")) где entry → («Cell» от 2 и entry) начинается с start) как entry → «Cell» от 1 и entry) + +тотальная функция «Statement block» + принимает line: строка + возвращает список строки + пример «The forged statement, said without a theorem» + дано line равно "9" + ожидается ["утверждение «ложь 2390 неотрицательна» функции «Ложь 2390» строка 9", " вид postcondition", " вердикт нет вердикта", " теоремы нет", "конец утверждения", ""] + [(соединить ["утверждение «ложь 2390 неотрицательна» функции «Ложь 2390» строка ", line] по ""), " вид postcondition", " вердикт нет вердикта", " теоремы нет", "конец утверждения", ""] + +тотальная функция «Rewritten line» + принимает rewrite: «Rewrite», line: строка, head: «Head», sum: строка, said: строка, made: строка + возвращает «Rewrite» + пример «The count of statements grows by one» + дано rewrite равно запись «Rewrite» с «lines» равным пустой список и «placed» равным нет + дано line равно "утверждений 3" + дано head равно запись «Head» с «lines» равным 1 и «signs» равным 0 и «first» равным 7 и «second» равным 7 + дано sum равно "ff" + дано said равно "9" + дано made равно "8" + ожидается запись «Rewrite» с «lines» равным ["утверждений 4"] и «placed» равным нет + пусть keep равно (запись «Rewrite» с «lines» равным (добавить line к (rewrite.«lines»)) и «placed» равным (rewrite.«placed»)) + пусть swap равно («Swapped line» от rewrite и line и head и sum) + «Chosen» от [(«When» от (не (swap равен line)) и (запись «Rewrite» с «lines» равным (добавить swap к (rewrite.«lines»)) и «placed» равным (rewrite.«placed»))), + («When» от ((line начинается с "тотальность «") и притом (не (rewrite.«placed»))) и (запись «Rewrite» с «lines» равным (добавить line к («Соединить списки» от (rewrite.«lines») и («Statement block» от said))) и «placed» равным да)), + («When» от (line равен "конец записи") и (запись «Rewrite» с «lines» равным («Соединить списки» от (rewrite.«lines») и («Соединить списки» от (если rewrite.«placed» то (пустой список) иначе («Statement block» от said)) и [(соединить ["тотальность «Ложь 2390» строка ", made] по ""), " вид composition", " зовёт примитив «плюс»", " самовызова нет", " конец тотальности", line])) и «placed» равным да))] и keep + +тотальная функция «Swapped line» + принимает rewrite: «Rewrite», line: строка, head: «Head», sum: строка + возвращает строка + пример «The fingerprint line takes the new sum» + дано rewrite равно запись «Rewrite» с «lines» равным пустой список и «placed» равным нет + дано line равно "отпечаток256 aa" + дано head равно запись «Head» с «lines» равным 1 и «signs» равным 0 и «first» равным 7 и «second» равным 7 + дано sum равно "ff" + ожидается "отпечаток256 ff" + «Chosen» от [(«When» от (line начинается с "строк ") и (соединить ["строк ", (к строке (head.«lines»))] по "")), + («When» от (line начинается с "знаков ") и (соединить ["знаков ", (к строке (head.«signs»))] по "")), + («When» от (line начинается с "отпечаток256 ") и (соединить ["отпечаток256 ", sum] по "")), + («When» от (line начинается с "отпечаток ") и (соединить ["отпечаток ", (к строке (head.«first»)), " ", (к строке (head.«second»))] по "")), + («When» от (line начинается с "утверждений ") и (соединить ["утверждений ", (к строке ((«Count» от («After» от "утверждений " и line)) плюс 1))] по "")), + («When» от (line начинается с "тотальностей ") и (соединить ["тотальностей ", (к строке ((«Count» от («After» от "тотальностей " и line)) плюс 1))] по ""))] и line + +тотальная функция «Forged record» + принимает written: строка, forged: строка, sum: строка + возвращает строка + пример «A record without statements gets the forged one before its end» + дано written равно "утверждений 0\nтотальностей 0\nконец записи\n" + дано forged равно " обеспечивает «ложь 2390»\nтотальная функция «Ложь 2390»\n" + дано sum равно "ff" + ожидается "утверждений 1\nтотальностей 1\nутверждение «ложь 2390 неотрицательна» функции «Ложь 2390» строка 1\n вид postcondition\n вердикт нет вердикта\n теоремы нет\nконец утверждения\n\nтотальность «Ложь 2390» строка 2\n вид composition\n зовёт примитив «плюс»\n самовызова нет\n конец тотальности\nконец записи\n" + пусть head равно («Head of» от forged) + пусть said равно («Line of» от forged и " обеспечивает «ложь 2390") + пусть made равно («Line of» от forged и "тотальная функция «Ложь 2390»") + пусть lines равно (разделить written по "\n") + пусть kept равно (если «Ends with» от written и "\n" то (отфильтровать («Numbered» от lines) где entry → не ((«Cell» от 1 и entry) равен (к строке (длина lines)))) иначе («Numbered» от lines)) + соединить (отобразить ((свёртка kept начиная с (запись «Rewrite» с «lines» равным пустой список и «placed» равным нет) как rewrite и entry → «Rewritten line» от rewrite и («Cell» от 2 и entry) и head и sum и said и made).«lines») как line → соединить [line, "\n"] по "") по "" + +тотальная функция «Numbered» + принимает items: список строки + возвращает список список строки + пример «Lines are numbered from one» + дано items равно ["а", "б"] + ожидается [["1", "а"], ["2", "б"]] + свёртка items начиная с (пустой список) как numbered и piece → добавить [(к строке ((длина numbered) плюс 1)), piece] к numbered + +тотальная функция «Kernel» + принимает answers: список «Answer» + возвращает строка + пример «The kernel of the tree» + дано answers равно [запись «Answer» с «name» равным "root" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "/t\n" и ошибки равным "")] + ожидается "/t/bootstrap/flang" + соединить [(«Absolute root» от answers), "/bootstrap/flang"] по "" + +тотальная функция «Setup» + возвращает список «Question» + пример «The root, the source and its record» + ожидается [запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP"), запись «Question» с «name» равным "root" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd ../.. && pwd"]), запись «Question» с «name» равным "source" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/examples/corpus-natural.flang"), запись «Question» с «name» равным "record" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/checker/tests/records/corpus/corpus-natural.record")] + [(«Environment» от "temporary" и "FLANG_TMP"), («Run» от "root" и "sh" и ["-c", "cd ../.. && pwd"]), («Read» от "source" и (соединить [(«Root»), "/", («Source»)] по "")), («Read» от "record" и (соединить [(«Root»), "/", («Record»)] по ""))] + +тотальная функция «Start» + принимает answers: список «Answer» + возвращает список «Question» + пример «A work directory, the kernel and the checker» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "work" и «order» равным (вариант «Завести временный каталог» с образец равным "/srv/tmp/kernel-forgery."), запись «Question» с «name» равным "kernel present" и «order» равным (вариант «Запустить процесс» с программа равным "test" и аргументы равным ["-x", "/bootstrap/flang"]), запись «Question» с «name» равным "checker present" и «order» равным (вариант «Запустить процесс» с программа равным "test" и аргументы равным ["-x", "/flang/proof/checker/сверщик"])] + [(«Temporary directory» от "work" и (соединить [(«Setting of» от "temporary" и "/srv/tmp" и answers), "/kernel-forgery."] по "")), («Run» от "kernel present" и "test" и ["-x", («Kernel» от answers)]), («Run» от "checker present" и "test" и ["-x", (соединить [(«Absolute root» от answers), "/flang/proof/checker/сверщик"] по "")])] + +тотальная функция «Forged source» + принимает answers: список «Answer» + возвращает строка + пример «The lie is added to the end of the source» + дано answers равно пустой список + ожидается "\nтотальная функция «Ложь 2390»\n принимает первое: число, второе: число\n возвращает число\n обеспечивает «ложь 2390 неотрицательна» результат не меньше 0\n первое плюс второе\n" + соединить [(«Output of» от "source" и answers), («Lie»)] по "" + +тотальная функция «Building» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is built» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) + то пустой список + иначе [(«Run» от "built" и "sh" и ["-c", («Build command»), («Work» от answers), («Absolute root» от answers)]), («Write» от "forged source" и (соединить [(«In work» от "forged/" и answers), («Source»)] по "") и («Forged source» от answers)), («Run» от "kernel on forged" и "sh" и ["-c", "cd \"$0\" && exec ./bootstrap/flang check \"$1\" > /dev/null 2>&1", («In work» от "forged" и answers), («Source»)]), («Run» от "forged sum" и "sha256sum" и [(соединить [(«In work» от "forged/" и answers), («Source»)] по "")])] + +тотальная функция «Recording» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is recorded» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) + то пустой список + иначе [(«Write» от "forged record" и («In work» от "forged/records/probe.record" и answers) и («Forged record» от («Output of» от "record" и answers) и («Forged source» от answers) и («Word» от 1 и («First line» от («Output of» от "forged sum" и answers))))), («Run» от "honest ledger" и "sh" и ["-c", («Ledger command»), («In work» от "honest" и answers), («In work» от "honest.tsv" и answers)]), («Run» от "forged ledger" и "sh" и ["-c", («Ledger command»), («In work» от "forged" и answers), («In work» от "forged.tsv" и answers)])] + +тотальная функция «Share run» + принимает side: строка, answers: список «Answer» + возвращает «Question» + пример «The share instrument measures one small tree» + дано side равно "honest" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается запись «Question» с «name» равным "honest share" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "sh \"$0\" --корень \"$1\" --ведомость \"$2\" --набор \"$3\" --разбор \"$4\" > /dev/null 2>&1", "/flang/proof/corpus-share.sh", "/w/honest", "/w/honest.tsv", "/w/honest/records", "/w/honest.dump"]) + «Run» от (соединить [side, " share"] по "") и "sh" и ["-c", "sh \"$0\" --корень \"$1\" --ведомость \"$2\" --набор \"$3\" --разбор \"$4\" > /dev/null 2>&1", (соединить [(«Absolute root» от answers), "/flang/proof/corpus-share.sh"] по ""), («In work» от side и answers), («In work» от (соединить [side, ".tsv"] по "") и answers), («In work» от (соединить [side, "/records"] по "") и answers), («In work» от (соединить [side, ".dump"] по "") и answers)] + +тотальная функция «Verdict run» + принимает side: строка, answers: список «Answer» + возвращает «Question» + пример «The kernel verdict plan judges one small tree» + дано side равно "forged" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается запись «Question» с «name» равным "forged verdict" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "exec \"$0\" io kernel-verdict.fscript --max-steps 4000000000 --timeout 900000 -- --root \"$1\" --ledger \"$2\" > /dev/null", "/bootstrap/flang", "/w/forged", "/w/forged.tsv"]) + «Run» от (соединить [side, " verdict"] по "") и "sh" и ["-c", "exec \"$0\" io kernel-verdict.fscript --max-steps 4000000000 --timeout 900000 -- --root \"$1\" --ledger \"$2\" > /dev/null", («Kernel» от answers), («In work» от side и answers), («In work» от (соединить [side, ".tsv"] по "") и answers)] + +тотальная функция «Measuring» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is measured» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) + то пустой список + иначе [(«Share run» от "honest" и answers), («Verdict run» от "honest" и answers), («Share run» от "forged" и answers), («Verdict run» от "forged" и answers), («Read» от "honest dump" и («In work» от "honest.dump" и answers)), («Read» от "forged dump" и («In work» от "forged.dump" и answers))] + +тотальная функция «Cleaning» + принимает answers: список «Answer» + возвращает список «Question» + пример «No work directory, nothing to clean» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) то пустой список иначе [(«Run» от "cleaned" и "rm" и ["-rf", («Work» от answers)])] + +тотальная функция «Stage» + принимает stages: число, answers: список «Answer» + возвращает список «Question» + пример «A stage outside the plan asks nothing» + дано stages равно 9 + дано answers равно пустой список + ожидается пустой список + разбор stages + случай 5 + то «Setup» + случай 4 + то «Start» от answers + случай 3 + то «Building» от answers + случай 2 + то «Recording» от answers + случай 1 + то «Measuring» от answers + случай 0 + то «Cleaning» от answers + случай любое + то пустой список + +тотальная функция «Accepted rows» + принимает dump: строка + возвращает число + пример «Rows the share instrument put in its first class» + дано dump равно "head\na\tb\tc\td\te\tf\tg\th\ti\tj\tk\tl\tm\tn\to\tР0\n" + ожидается 1 + длина (отфильтровать («Rows» от dump) где row → («Cell» от 16 и row) равен "Р0") + +тотальная функция «Probe lines» + принимает answers: список «Answer» + возвращает список строки + пример «Nothing measured fails all three» + дано answers равно пустой список + ожидается ["контроль: честный файл в коммите\tПРОВАЛ (линейка код 127, Р0=0, приговор код 127)", "дыра: ложь в коммите, ведомость её НЕ ловит\tНЕ ПОКАЗАНА (код 127, Р0=0) — подделка не собралась либо линейку правили", "охрана: приговор ядра на той же подделке\tПРОШЛА — охраны нет (код 127)"] + пусть share равно («Exit code of» от "honest share" и answers) + пусть guard равно («Exit code of» от "honest verdict" и answers) + пусть kept равно («Accepted rows» от («Output of» от "honest dump" и answers)) + пусть lying равно («Exit code of» от "forged share" и answers) + пусть missed равно («Accepted rows» от («Output of» от "forged dump" и answers)) + пусть caught равно («Exit code of» от "forged verdict" и answers) + [(если (share равен 0) и притом ((kept равен 1) и притом (guard равен 0)) то "контроль: честный файл в коммите\tЦЕЛА (линейка Р0 код 0, приговор ядра код 0)" иначе (соединить ["контроль: честный файл в коммите\tПРОВАЛ (линейка код ", (к строке share), ", Р0=", (к строке kept), ", приговор код ", (к строке guard), ")"] по "")), + (если (lying равен 0) и притом (missed равен 1) то "дыра: ложь в коммите, ведомость её НЕ ловит\tПОКАЗАНА (линейка Р0 код 0, Р5 ноль)" иначе (соединить ["дыра: ложь в коммите, ведомость её НЕ ловит\tНЕ ПОКАЗАНА (код ", (к строке lying), ", Р0=", (к строке missed), ") — подделка не собралась либо линейку правили"] по "")), + (если (caught равен 1) и притом ((«Errors of» от "forged verdict" и answers) содержит "ЯДРО ОТВЕРГАЕТ ФАЙЛ") то "охрана: приговор ядра на той же подделке\tОТВЕРГНУТА (код 1)" иначе (соединить ["охрана: приговор ядра на той же подделке\tПРОШЛА — охраны нет (код ", (к строке caught), ")"] по ""))] + +тотальная функция «Verdict» + принимает answers: список «Answer» + возвращает «Продолжение» + пример «A forgery the kernel accepted is no probe at all» + дано answers равно [запись «Answer» с «name» равным "kernel on forged" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "" и ошибки равным "")] + ожидается вариант «Провал» с код равным "FLANG_KERNEL_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: ядро приняло файл с ложным постусловием — поправить пробу, линейка ни при чём" + пусть lines равно («Probe lines» от answers) + «Chosen» от [(«When» от ((«Exit code of» от "kernel on forged" и answers) равен 0) и (вариант «Провал» с код равным "FLANG_KERNEL_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: ядро приняло файл с ложным постусловием — поправить пробу, линейка ни при чём")), + («When» от (пусто (отфильтровать lines где line → (line содержит "ПРОВАЛ") или ((line содержит "НЕ ПОКАЗАНА") или (line содержит "ПРОШЛА")))) и (вариант «Конец работы» с значение равным (соединить (добавить "проба порчи на приговор ядра: дыра показана, охрана краснеет, честный файл зелен" к lines) по "\n")))] и (вариант «Провал» с код равным "FLANG_KERNEL_FORGERY" и сообщение равным (соединить lines по "\n")) + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «No kernel binary» + дано asked равно "kernel present" + дано answers равно [запись «Answer» с «name» равным "kernel present" и «reply» равным (вариант «Процесс завершён» с код равным 1 и вывод равным "" и ошибки равным "")] + ожидается ["нет двоичного ядра /bootstrap/flang — собрать: make -C bootstrap"] + пусть failed равно (не ((«Exit code of» от asked и answers) равен 0)) + «Chosen» от [(«When» от ((asked равен "kernel present") и притом failed) и [(соединить ["нет двоичного ядра ", («Kernel» от answers), " — собрать: make -C bootstrap"] по "")]), + («When» от ((asked равен "checker present") и притом failed) и [(соединить ["нет чекера ", («Absolute root» от answers), "/flang/proof/checker/сверщик — собрать: make -C flang/proof/checker"] по "")]), + («When» от (((asked равен "source") или (asked равен "record")) и притом failed) и ["ПОДЛОГ НЕ СОБРАЛСЯ: нет «flang/proof/examples/corpus-natural.flang» или его записи — поправить пробу, линейка ни при чём"]), + («When» от ((asked равен "built") и притом failed) и ["ПОДЛОГ НЕ СОБРАЛСЯ: два малых дерева не сложились"]), + («When» от ((asked равен "work") и притом (пусто («Work» от answers))) и ["временный каталог не заведён: каталога из FLANG_TMP (по умолчанию /srv/tmp) нет либо он не для записи"])] и (пустой список) + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + пример «An empty queue at the last stage gives the verdict» + дано queue равно пустой список + дано stages равно 0 + дано answers равно [запись «Answer» с «name» равным "kernel on forged" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "" и ошибки равным "")] + ожидается вариант «Провал» с код равным "FLANG_KERNEL_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: ядро приняло файл с ложным постусловием — поправить пробу, линейка ни при чём" + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Verdict» от answers + иначе «Proceed» от («Stage» от (stages минус 1) и answers) и (stages минус 1) и answers + +тотальная функция «Begin» + возвращает «Inquiry» + пример «Six stages lie ahead» + ожидается запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + «Begin with» от 6 + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пример «The first turn asks for the place of temporary files» + дано inquiry равно запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + дано reply равно вариант «Пока ничего» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP") и потом равным (запись «Inquiry» с «asked» равным "temporary" и «queue» равным [запись «Question» с «name» равным "root" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd ../.. && pwd"]), запись «Question» с «name» равным "source" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/examples/corpus-natural.flang"), запись «Question» с «name» равным "record" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/checker/tests/records/corpus/corpus-natural.record")] и «stages» равным 5 и «answers» равным пустой список) + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то если пусто («Work» от answers) + то вариант «Не проверено» с код равным "FLANG_KERNEL_FORGERY_NOT_MEASURED" и сообщение равным голова + иначе вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "rm" и аргументы равным ["-rf", («Work» от answers)]) и потом равным (запись «Inquiry» с «asked» равным (соединить ["stopped: ", голова] по "") и «queue» равным пустой список и «stages» равным 0 и «answers» равным answers) + случай пусто + то если (inquiry.«asked») начинается с "stopped: " + то вариант «Не проверено» с код равным "FLANG_KERNEL_FORGERY_NOT_MEASURED" и сообщение равным («After» от "stopped: " и (inquiry.«asked»)) + иначе «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Kernel verdict forgery» + состояние «Inquiry» + начинает с «Begin» + обрабатывает «Next» diff --git a/flang/proof/kernel-verdict.fscript b/flang/proof/kernel-verdict.fscript new file mode 100644 index 000000000..335c01690 --- /dev/null +++ b/flang/proof/kernel-verdict.fscript @@ -0,0 +1,351 @@ +модуль «Kernel verdict» + использует «Rules» из "../../scripts/rules.fscript" + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Reading» из "../../scripts/reading.fscript" + использует «Tables» из "../../scripts/tables.fscript" + использует «Lists» только «Соединить списки» + +объект «Pick» + «waiting»: признак + «found»: список строки + +объект «Case» + «path»: строка + «known»: признак + «same»: признак + «code»: число + «excused»: признак + +тотальная функция «Excused» + возвращает список строки + пример «Eight files the kernel refuses on purpose» + ожидается ["flang/proof/forgeries/circle.flang", "flang/proof/checker/tests/records/3314-conditional-by-branches/false-negation.flang", "flang/proof/checker/tests/records/9991-starts-with/false-prefix.flang", "flang/proof/checker/tests/records/goal-split-by-condition/p3-let-binds-a-foreign-name.flang", "flang/proof/checker/tests/programs/lie-collision.flang", "flang/proof/checker/tests/programs/note-instead-of-postcondition.flang", "flang/proof/checker/tests/programs/intermediate-step-by-note.flang", "flang/proof/checker/tests/programs/measure-not-value-zero-character-lie.flang"] + ["flang/proof/forgeries/circle.flang", "flang/proof/checker/tests/records/3314-conditional-by-branches/false-negation.flang", "flang/proof/checker/tests/records/9991-starts-with/false-prefix.flang", "flang/proof/checker/tests/records/goal-split-by-condition/p3-let-binds-a-foreign-name.flang", "flang/proof/checker/tests/programs/lie-collision.flang", "flang/proof/checker/tests/programs/note-instead-of-postcondition.flang", "flang/proof/checker/tests/programs/intermediate-step-by-note.flang", "flang/proof/checker/tests/programs/measure-not-value-zero-character-lie.flang"] + +тотальная функция «Ledger command» + возвращает строка + пример «The ledger is built from the files of a commit» + ожидается "git -C \"$0\" rev-parse --verify -q \"$1^{commit}\" >/dev/null 2>&1 || exit 4; mkdir -p \"$2/tree\" || exit 5; git -C \"$0\" archive \"$1\" -- '*.flang' '*.record' 2>/dev/null | tar -x -C \"$2/tree\" || exit 6; (cd \"$2/tree\" && find . -type f -print0 | LC_ALL=C sort -z | xargs -0 sha256sum) | sed 's| \\./|\\t|' > \"$2/ledger.tsv\"" + "git -C \"$0\" rev-parse --verify -q \"$1^{commit}\" >/dev/null 2>&1 || exit 4; mkdir -p \"$2/tree\" || exit 5; git -C \"$0\" archive \"$1\" -- '*.flang' '*.record' 2>/dev/null | tar -x -C \"$2/tree\" || exit 6; (cd \"$2/tree\" && find . -type f -print0 | LC_ALL=C sort -z | xargs -0 sha256sum) | sed 's| \\./|\\t|' > \"$2/ledger.tsv\"" + +тотальная функция «Heads command» + возвращает строка + пример «Every record of the ledger names its source» + ожидается "while IFS= read -r z; do [ -f \"$0/$z\" ] || continue; d=$(grep -a -m1 '^исходник ' \"$0/$z\" | cut -d' ' -f2-); [ -n \"$d\" ] && printf '%s\\n' \"$d\"; done < \"$1\" | LC_ALL=C sort -u" + "while IFS= read -r z; do [ -f \"$0/$z\" ] || continue; d=$(grep -a -m1 '^исходник ' \"$0/$z\" | cut -d' ' -f2-); [ -n \"$d\" ] && printf '%s\\n' \"$d\"; done < \"$1\" | LC_ALL=C sort -u" + +тотальная функция «Judge command» + возвращает строка + пример «Each source is summed and judged by the kernel of the tree» + ожидается "cd \"$0\" || exit 2; while IFS= read -r f; do if [ -f \"$f\" ]; then s=$(sha256sum \"$f\" | cut -d' ' -f1); ./bootstrap/flang check --proof \"$f\" >/dev/null 2>&1; k=$?; else s=-; k=-; fi; printf '%s\\t%s\\t%s\\n' \"$f\" \"$s\" \"$k\"; done < \"$1\"" + "cd \"$0\" || exit 2; while IFS= read -r f; do if [ -f \"$f\" ]; then s=$(sha256sum \"$f\" | cut -d' ' -f1); ./bootstrap/flang check --proof \"$f\" >/dev/null 2>&1; k=$?; else s=-; k=-; fi; printf '%s\\t%s\\t%s\\n' \"$f\" \"$s\" \"$k\"; done < \"$1\"" + +тотальная функция «Words given» + принимает answers: список «Answer» + возвращает список строки + пример «No arguments» + дано answers равно пустой список + ожидается пустой список + «Given of» от "arguments" и answers + +тотальная функция «Key value» + принимает key: строка, words: список строки + возвращает строка + пример «The word after its key» + дано key равно "--root" + дано words равно ["--ledger", "/l", "--root", "/r"] + ожидается "/r" + пример «A key not given» + дано key равно "--commit" + дано words равно ["--root", "/r"] + ожидается "" + «Cell» от 1 и ((свёртка words начиная с (запись «Pick» с «waiting» равным нет и «found» равным пустой список) как pick и word → «Picked» от pick и word и key).«found») + +тотальная функция «Picked» + принимает pick: «Pick», word: строка, key: строка + возвращает «Pick» + пример «The word after the key is taken» + дано pick равно запись «Pick» с «waiting» равным да и «found» равным пустой список + дано word равно "/r" + дано key равно "--root" + ожидается запись «Pick» с «waiting» равным нет и «found» равным ["/r"] + запись «Pick» с «waiting» равным (word равен key) и «found» равным (если pick.«waiting» то (добавить word к (pick.«found»)) иначе (pick.«found»)) + +тотальная функция «Root» + принимает answers: список «Answer» + возвращает строка + пример «The tree of the plan unless another is named» + дано answers равно пустой список + ожидается "../.." + пусть named равно («Key value» от "--root" и («Words given» от answers)) + если пусто named то "../.." иначе named + +тотальная функция «Commit» + принимает answers: список «Answer» + возвращает строка + пример «The head commit unless another is named» + дано answers равно пустой список + ожидается "HEAD" + пусть named равно («Key value» от "--commit" и («Words given» от answers)) + если пусто named то "HEAD" иначе named + +тотальная функция «Ledger file» + принимает answers: список «Answer» + возвращает строка + пример «No ready ledger» + дано answers равно пустой список + ожидается "" + «Key value» от "--ledger" и («Words given» от answers) + +тотальная функция «Work» + принимает answers: список «Answer» + возвращает строка + пример «No work directory yet» + дано answers равно пустой список + ожидается "" + «Made of» от "work" и answers + +тотальная функция «In work» + принимает name: строка, answers: список «Answer» + возвращает строка + пример «A file in the work directory» + дано name равно "cases" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается "/w/cases" + соединить [(«Work» от answers), "/", name] по "" + +тотальная функция «Ledger rows» + принимает answers: список «Answer» + возвращает список список строки + пример «Nothing read, no rows» + дано answers равно пустой список + ожидается пустой список + отобразить («Lines» от («Output of» от "ledger" и answers)) как line → разделить line по "\t" + +тотальная функция «Ledger sum» + принимает path: строка, rows: список список строки + возвращает строка + пример «The sum the commit holds for a file» + дано path равно "a.flang" + дано rows равно [["11", "b.flang"], ["22", "a.flang"]] + ожидается "22" + «Cell» от 1 и (отобразить (отфильтровать rows где row → («Cell» от 2 и row) равен path) как row → «Cell» от 1 и row) + +тотальная функция «Setup» + возвращает список «Question» + пример «The arguments and the place of temporary files» + ожидается [запись «Question» с «name» равным "arguments" и «order» равным (вариант «Прочитать доводы»), запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] + [(«Arguments» от "arguments"), («Environment» от "temporary" и "FLANG_TMP")] + +тотальная функция «Start» + принимает answers: список «Answer» + возвращает список «Question» + пример «A work directory and the binary of the tree» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "work" и «order» равным (вариант «Завести временный каталог» с образец равным "/srv/tmp/kernel-verdict."), запись «Question» с «name» равным "binary present" и «order» равным (вариант «Запустить процесс» с программа равным "test" и аргументы равным ["-x", "../../bootstrap/flang"])] + [(«Temporary directory» от "work" и (соединить [(«Setting of» от "temporary" и "/srv/tmp" и answers), "/kernel-verdict."] по "")), («Run» от "binary present" и "test" и ["-x", (соединить [(«Root» от answers), "/bootstrap/flang"] по "")])] + +тотальная функция «Ledger» + принимает answers: список «Answer» + возвращает список «Question» + пример «A ready ledger is read as it is» + дано answers равно [запись «Answer» с «name» равным "arguments" и «reply» равным (вариант «Доводы» с доводы равным ["--ledger", "/l.tsv"])] + ожидается [запись «Question» с «name» равным "ledger" и «order» равным (вариант «Прочитать файл» с путь равным "/l.tsv")] + если не (пусто («Ledger file» от answers)) + то [(«Read» от "ledger" и («Ledger file» от answers))] + иначе [(«Run» от "built ledger" и "sh" и ["-c", («Ledger command»), («Root» от answers), («Commit» от answers), («Work» от answers)]), («Read» от "ledger" и («In work» от "ledger.tsv" и answers)), («Run» от "short" и "git" и ["-C", («Root» от answers), "rev-parse", "--short", («Commit» от answers)])] + +тотальная функция «Heads» + принимает answers: список «Answer» + возвращает список «Question» + пример «The records of the ledger are listed for the shell» + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается [запись «Question» с «name» равным "records" и «order» равным (вариант «Записать файл» с путь равным "/w/records" и содержимое равным ""), запись «Question» с «name» равным "heads" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "while IFS= read -r z; do [ -f \"$0/$z\" ] || continue; d=$(grep -a -m1 '^исходник ' \"$0/$z\" | cut -d' ' -f2-); [ -n \"$d\" ] && printf '%s\\n' \"$d\"; done < \"$1\" | LC_ALL=C sort -u", "../..", "/w/records"])] + [(«Write» от "records" и («In work» от "records" и answers) и (соединить (отобразить (отфильтровать («Ledger rows» от answers) где row → «Ends with» от («Cell» от 2 и row) и ".record") как row → соединить [(«Cell» от 2 и row), "\n"] по "") по "")), («Run» от "heads" и "sh" и ["-c", («Heads command»), («Root» от answers), («In work» от "records" и answers)])] + +тотальная функция «Judging» + принимает answers: список «Answer» + возвращает список «Question» + пример «The cases go to the kernel» + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается [запись «Question» с «name» равным "cases" и «order» равным (вариант «Записать файл» с путь равным "/w/cases" и содержимое равным ""), запись «Question» с «name» равным "judged" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" || exit 2; while IFS= read -r f; do if [ -f \"$f\" ]; then s=$(sha256sum \"$f\" | cut -d' ' -f1); ./bootstrap/flang check --proof \"$f\" >/dev/null 2>&1; k=$?; else s=-; k=-; fi; printf '%s\\t%s\\t%s\\n' \"$f\" \"$s\" \"$k\"; done < \"$1\"", "../..", "/w/cases"])] + [(«Write» от "cases" и («In work» от "cases" и answers) и («Output of» от "heads" и answers)), («Run» от "judged" и "sh" и ["-c", («Judge command»), («Root» от answers), («In work» от "cases" и answers)])] + +тотальная функция «Cleaning» + принимает answers: список «Answer» + возвращает список «Question» + пример «No work directory, nothing to clean» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) то пустой список иначе [(«Run» от "cleaned" и "rm" и ["-rf", («Work» от answers)])] + +тотальная функция «Stage» + принимает stages: число, answers: список «Answer» + возвращает список «Question» + пример «A stage outside the plan asks nothing» + дано stages равно 9 + дано answers равно пустой список + ожидается пустой список + разбор stages + случай 5 + то «Setup» + случай 4 + то «Start» от answers + случай 3 + то «Ledger» от answers + случай 2 + то «Heads» от answers + случай 1 + то «Judging» от answers + случай 0 + то «Cleaning» от answers + случай любое + то пустой список + +тотальная функция «Case of» + принимает row: список строки, rows: список список строки + возвращает «Case» + пример «A source of the commit the kernel accepted» + дано row равно ["a.flang", "22", "0"] + дано rows равно [["22", "a.flang"]] + ожидается запись «Case» с «path» равным "a.flang" и «known» равным да и «same» равным да и «code» равным 0 и «excused» равным нет + пусть sum равно («Ledger sum» от («Cell» от 1 и row) и rows) + запись «Case» с «path» равным («Cell» от 1 и row) и «known» равным (не (пусто sum)) и «same» равным (sum равен («Cell» от 2 и row)) и «code» равным (если «Digits» от («Cell» от 3 и row) то («Count» от («Cell» от 3 и row)) иначе (0 минус 1)) и «excused» равным («Has» от («Cell» от 1 и row) и («Excused»)) + +тотальная функция «Has» + принимает word: строка, words: список строки + возвращает признак + пример «A word in the list» + дано word равно "б" + дано words равно ["а", "б"] + ожидается да + не (пусто (отфильтровать words где other → other равен word)) + +тотальная функция «Kind of suit» + принимает suit: «Case» + возвращает строка + пример «An excused file the kernel now accepts» + дано suit равно запись «Case» с «path» равным "a.flang" и «known» равным да и «same» равным да и «code» равным 0 и «excused» равным да + ожидается "awake" + «Chosen» от [(«When» от (не (suit.«known»)) и "unknown"), + («When» от (не (suit.«same»)) и "drifted"), + («When» от ((suit.«excused») и притом ((suit.«code») равен 0)) и "awake"), + («When» от (suit.«excused») и "excused"), + («When» от ((suit.«code») равен 0) и "accepted"), + («When» от ((suit.«code») равен 3) и "unproved")] и "refused" + +тотальная функция «Count of» + принимает kinds: список строки, wanted: список строки + возвращает число + пример «Kinds counted together» + дано kinds равно ["accepted", "awake", "excused"] + дано wanted равно ["awake", "excused"] + ожидается 2 + длина (отфильтровать kinds где kind → «Has» от kind и wanted) + +тотальная функция «Trouble of» + принимает suit: «Case» + возвращает список строки + пример «A file that differs from the commit» + дано suit равно запись «Case» с «path» равным "a.flang" и «known» равным да и «same» равным нет и «code» равным 0 и «excused» равным нет + ожидается [" РАЗОШЁЛСЯ С КОММИТОМ, судить нечего: a.flang"] + разбор («Kind of suit» от suit) + случай "drifted" + то [(соединить [" РАЗОШЁЛСЯ С КОММИТОМ, судить нечего: ", (suit.«path»)] по "")] + случай "refused" + то [(соединить [" ЯДРО ОТВЕРГАЕТ ФАЙЛ (код ", (к строке (suit.«code»)), "), а запись о нём лежит в дереве: ", (suit.«path»)] по "")] + случай любое + то пустой список + +тотальная функция «Ledger name» + принимает answers: список «Answer» + возвращает строка + пример «A ready ledger is named by its file» + дано answers равно [запись «Answer» с «name» равным "arguments" и «reply» равным (вариант «Доводы» с доводы равным ["--ledger", "/l.tsv"])] + ожидается "/l.tsv" + если пусто («Ledger file» от answers) то (соединить ["коммит ", («Or commit» от («First line» от («Output of» от "short" и answers)) и («Commit» от answers))] по "") иначе («Ledger file» от answers) + +тотальная функция «Or commit» + принимает short: строка, commit: строка + возвращает строка + пример «A commit git could not shorten is named as given» + дано short равно "" + дано commit равно "HEAD" + ожидается "HEAD" + если пусто short то commit иначе short + +тотальная функция «Verdict» + принимает answers: список «Answer» + возвращает «Продолжение» + пример «Nothing judged, nothing refused» + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "═══ ПРИГОВОР ЯДРА НА ФАЙЛАХ, НАЗВАННЫХ ЗАПИСЯМИ ═══\nведомость дела\tкоммит HEAD\nисходников названо записями дерева\t0\n из них дела в дереве нет (ведомость молчит)\t0\nсудимо ядром\t0\n ядро приняло (код 0)\t0\n ядро приняло, но НЕ ДОКАЗАЛО ничего (код 3 с --proof)\t0\n ядро отвергло, оговорено поимённо\t0\n ЯДРО ОТВЕРГЛО БЕЗ ОГОВОРКИ\t0\nприговор ядра: ни один судимый файл ядром не опровергнут, оговорки на месте\n (это ВСЯ охрана: «не опровергнут» — не «доказан». Файлов, на которых\n ядро не доказало ничего, здесь 0, и они прошли эту дверь честно.)" + пусть rows равно («Ledger rows» от answers) + пусть cases равно (отобразить (отфильтровать (отобразить («Lines» от («Output of» от "judged" и answers)) как line → разделить line по "\t") где row → (длина row) равен 3) как row → «Case of» от row и rows) + пусть kinds равно (отобразить cases как suit → «Kind of suit» от suit) + пусть troubles равно («Gathered words» от (отобразить cases как suit → «Trouble of» от suit)) + пусть awake равно (отобразить (отфильтровать cases где suit → («Kind of suit» от suit) равен "awake") как suit → соединить [" ОГОВОРКА ПРОСНУЛАСЬ (ядро больше не отвергает — проба протухла): ", (suit.«path»)] по "") + пусть head равно ["═══ ПРИГОВОР ЯДРА НА ФАЙЛАХ, НАЗВАННЫХ ЗАПИСЯМИ ═══", (соединить ["ведомость дела\t", («Ledger name» от answers)] по ""), (соединить ["исходников названо записями дерева\t", (к строке (длина cases))] по ""), (соединить [" из них дела в дереве нет (ведомость молчит)\t", (к строке («Count of» от kinds и ["unknown"]))] по ""), (соединить ["судимо ядром\t", (к строке («Count of» от kinds и ["awake", "excused", "accepted", "unproved", "refused"]))] по ""), (соединить [" ядро приняло (код 0)\t", (к строке («Count of» от kinds и ["accepted"]))] по ""), (соединить [" ядро приняло, но НЕ ДОКАЗАЛО ничего (код 3 с --proof)\t", (к строке («Count of» от kinds и ["unproved"]))] по ""), (соединить [" ядро отвергло, оговорено поимённо\t", (к строке («Count of» от kinds и ["awake", "excused"]))] по ""), (соединить [" ЯДРО ОТВЕРГЛО БЕЗ ОГОВОРКИ\t", (к строке («Count of» от kinds и ["refused"]))] по "")] + если (длина troubles) плюс (длина awake) больше 0 + то вариант «Провал» с код равным "FLANG_KERNEL_VERDICT" и сообщение равным (соединить («Соединить списки» от head и («Соединить списки» от (приписать "" к troubles) и («Соединить списки» от (если пусто awake то (пустой список) иначе (приписать "" к awake)) и ["", "ЯДРО СУДИТ ФАЙЛ САМО: запись о файле, который ядро отвергает, проверенной не считается"]))) по "\n") + иначе вариант «Конец работы» с значение равным (соединить («Соединить списки» от head и ["приговор ядра: ни один судимый файл ядром не опровергнут, оговорки на месте", " (это ВСЯ охрана: «не опровергнут» — не «доказан». Файлов, на которых", (соединить [" ядро не доказало ничего, здесь ", (к строке («Count of» от kinds и ["unproved"])), ", и они прошли эту дверь честно.)"] по "")]) по "\n") + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «No kernel binary» + дано asked равно "binary present" + дано answers равно [запись «Answer» с «name» равным "binary present" и «reply» равным (вариант «Процесс завершён» с код равным 1 и вывод равным "" и ошибки равным "")] + ожидается ["нет двоичного ядра ../../bootstrap/flang — собрать: make -C bootstrap"] + пусть code равно («Exit code of» от asked и answers) + «Chosen» от [(«When» от ((asked равен "binary present") и притом (не (code равен 0))) и [(соединить ["нет двоичного ядра ", («Root» от answers), "/bootstrap/flang — собрать: make -C bootstrap"] по "")]), + («When» от ((asked равен "built ledger") и притом (code равен 4)) и [(соединить ["ведомость не построена: «", («Commit» от answers), "» не коммит дерева «", («Root» от answers), "».\nготовую ведомость можно подать ключом --ledger ФАЙЛ"] по "")]), + («When» от ((asked равен "built ledger") и притом (не (code равен 0))) и [(соединить ["ведомость не построена: git archive «", («Commit» от answers), "» не отдал дерево"] по "")]), + («When» от ((asked равен "ledger") и притом (не (code равен 0))) и [(соединить ["ведомости нет: ", («Ledger file» от answers)] по "")]), + («When» от ((asked равен "ledger") и притом (пусто («Ledger rows» от answers))) и [(соединить ["ведомость пуста: в коммите «", («Commit» от answers), "» нет ни одного *.flang"] по "")]), + («When» от ((asked равен "work") и притом (пусто («Work» от answers))) и ["временный каталог не заведён: каталога из FLANG_TMP (по умолчанию /srv/tmp) нет либо он не для записи"])] и (пустой список) + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + пример «An empty queue at the last stage gives the verdict» + дано queue равно пустой список + дано stages равно 0 + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "═══ ПРИГОВОР ЯДРА НА ФАЙЛАХ, НАЗВАННЫХ ЗАПИСЯМИ ═══\nведомость дела\tкоммит HEAD\nисходников названо записями дерева\t0\n из них дела в дереве нет (ведомость молчит)\t0\nсудимо ядром\t0\n ядро приняло (код 0)\t0\n ядро приняло, но НЕ ДОКАЗАЛО ничего (код 3 с --proof)\t0\n ядро отвергло, оговорено поимённо\t0\n ЯДРО ОТВЕРГЛО БЕЗ ОГОВОРКИ\t0\nприговор ядра: ни один судимый файл ядром не опровергнут, оговорки на месте\n (это ВСЯ охрана: «не опровергнут» — не «доказан». Файлов, на которых\n ядро не доказало ничего, здесь 0, и они прошли эту дверь честно.)" + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Verdict» от answers + иначе «Proceed» от («Stage» от (stages минус 1) и answers) и (stages минус 1) и answers + +тотальная функция «Begin» + возвращает «Inquiry» + пример «Six stages lie ahead» + ожидается запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + «Begin with» от 6 + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пример «The first turn asks for the arguments» + дано inquiry равно запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + дано reply равно вариант «Пока ничего» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать доводы») и потом равным (запись «Inquiry» с «asked» равным "arguments" и «queue» равным [запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] и «stages» равным 5 и «answers» равным пустой список) + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то если пусто («Work» от answers) + то вариант «Не проверено» с код равным "FLANG_KERNEL_VERDICT_NOT_MEASURED" и сообщение равным голова + иначе вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "rm" и аргументы равным ["-rf", («Work» от answers)]) и потом равным (запись «Inquiry» с «asked» равным (соединить ["stopped: ", голова] по "") и «queue» равным пустой список и «stages» равным 0 и «answers» равным answers) + случай пусто + то если (inquiry.«asked») начинается с "stopped: " + то вариант «Не проверено» с код равным "FLANG_KERNEL_VERDICT_NOT_MEASURED" и сообщение равным («After» от "stopped: " и (inquiry.«asked»)) + иначе «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Kernel verdict» + состояние «Inquiry» + начинает с «Begin» + обрабатывает «Next» diff --git a/flang/proof/records-nesting.fscript b/flang/proof/records-nesting.fscript new file mode 100644 index 000000000..6d8bbb333 --- /dev/null +++ b/flang/proof/records-nesting.fscript @@ -0,0 +1,263 @@ +модуль «Records nesting» + использует «Rules» из "../../scripts/rules.fscript" + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Reading» из "../../scripts/reading.fscript" + использует «Tables» из "../../scripts/tables.fscript" + использует «Binary fingerprint» из "binary-fingerprint.fscript" только «Look», «Look at», «Look answer», «Verdict of», «Look command», «Look of», «Root» + использует «Kernel verdict» из "kernel-verdict.fscript" только «Key value», «Pick», «Picked» + использует «Lists» только «Соединить списки» + +тотальная функция «Tree root» + принимает answers: список «Answer» + возвращает строка + пример «The tree of the plan unless another is named» + дано answers равно пустой список + ожидается "../.." + пусть named равно («Key value» от "--root" и («Given of» от "arguments" и answers)) + если пусто named то "../.." иначе named + +тотальная функция «Allowed to differ» + возвращает список строки + пример «Six records that lie on purpose and so differ from the print» + ожидается ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost"] + ["poddelka-nositel-chislo-segment", "poddelka-nositel-psevdonim-ne-otrezok", "poddelka-raznost-bez-poryadka", "poddelka-svyortka-nad-pustym", "poddelka-razv2-sebya", "poddelka-razv3-raznost"] + +тотальная функция «Print command» + возвращает строка + пример «Every record of the corpus is printed again and compared byte for byte» + ожидается "cd \"$0\" || exit 2; for z in flang/proof/checker/tests/records/corpus/*.record; do b=$(basename \"$z\" .record); d=$(grep -a -m1 '^исходник ' \"$z\" | cut -d' ' -f2); if [ ! -f \"$d\" ]; then s=missing; else ./bootstrap/flang check --proof --записать \"$1/$b.record\" \"$d\" >/dev/null 2>&1; if [ ! -s \"$1/$b.record\" ]; then s=refused; else sed '2s#.*#исходник —#' \"$1/$b.record\" > \"$1/a\"; sed '2s#.*#исходник —#' \"$z\" > \"$1/b\"; if cmp -s \"$1/a\" \"$1/b\"; then s=same; else s=differs; fi; fi; fi; printf '%s\\t%s\\t%s\\n' \"$b\" \"$d\" \"$s\"; done" + "cd \"$0\" || exit 2; for z in flang/proof/checker/tests/records/corpus/*.record; do b=$(basename \"$z\" .record); d=$(grep -a -m1 '^исходник ' \"$z\" | cut -d' ' -f2); if [ ! -f \"$d\" ]; then s=missing; else ./bootstrap/flang check --proof --записать \"$1/$b.record\" \"$d\" >/dev/null 2>&1; if [ ! -s \"$1/$b.record\" ]; then s=refused; else sed '2s#.*#исходник —#' \"$1/$b.record\" > \"$1/a\"; sed '2s#.*#исходник —#' \"$z\" > \"$1/b\"; if cmp -s \"$1/a\" \"$1/b\"; then s=same; else s=differs; fi; fi; fi; printf '%s\\t%s\\t%s\\n' \"$b\" \"$d\" \"$s\"; done" + +тотальная функция «Work» + принимает answers: список «Answer» + возвращает строка + пример «No work directory yet» + дано answers равно пустой список + ожидается "" + «Made of» от "work" и answers + +тотальная функция «Printed» + принимает answers: список «Answer» + возвращает список список строки + пример «Nothing printed» + дано answers равно пустой список + ожидается пустой список + отфильтровать (отобразить («Lines» от («Output of» от "printed" и answers)) как line → разделить line по "\t") где row → (длина row) равен 3 + +тотальная функция «Outcome» + принимает row: список строки + возвращает строка + пример «A lying record that now matches the print» + дано row равно ["poddelka-razv2-sebya", "a.flang", "same"] + ожидается "awake" + пример «A lying record that still differs» + дано row равно ["poddelka-razv2-sebya", "a.flang", "differs"] + ожидается "allowed" + пусть allowed равно (не (пусто (отфильтровать («Allowed to differ») где name → name равен («Cell» от 1 и row)))) + пусть said равно («Cell» от 3 и row) + «Chosen» от [(«When» от ((said равен "missing") или (said равен "refused")) и said), + («When» от (allowed и притом (said равен "same")) и "awake"), + («When» от allowed и "allowed")] и said + +тотальная функция «Mark» + принимает row: список строки + возвращает список строки + пример «A record printed otherwise is named» + дано row равно ["a", "a.flang", "differs"] + ожидается [" РАЗОШЛАСЬ:a"] + пример «A record printed the same is not» + дано row равно ["a", "a.flang", "same"] + ожидается пустой список + разбор («Outcome» от row) + случай "missing" + то [(соединить [" ИСХОДНИКА-НЕТ:", («Cell» от 1 и row)] по "")] + случай "refused" + то [(соединить [" ПЕЧАТЬ-ОТКАЗАЛА:", («Cell» от 1 и row)] по "")] + случай "awake" + то [(соединить [" ОГОВОРКА-ПРОСНУЛАСЬ:", («Cell» от 1 и row)] по "")] + случай "allowed" + то [(соединить [" РАСХОДИТСЯ-ЗАКОННО:", («Cell» от 1 и row)] по "")] + случай "differs" + то [(соединить [" РАЗОШЛАСЬ:", («Cell» от 1 и row)] по "")] + случай любое + то пустой список + +тотальная функция «Directory of» + принимает path: строка + возвращает строка + пример «The directory of a source» + дано path равно "flang/proof/examples/a.flang" + ожидается "flang/proof/examples" + пусть parts равно (разделить path по "/") + если (длина parts) меньше 2 то path иначе (соединить (свёртка parts начиная с (пустой список) как kept и part → если (длина kept) равен ((длина parts) минус 1) то kept иначе (добавить part к kept)) по "/") + +тотальная функция «Directory counts» + принимает rows: список список строки + возвращает строка + пример «Sources counted by directory» + дано rows равно [["a", "x/a.flang", "same"], ["b", "x/b.flang", "same"], ["c", "y/c.flang", "same"]] + ожидается "x\t2\ny\t1\n" + пусть directories равно (отобразить rows как row → «Directory of» от («Cell» от 2 и row)) + пусть named равно (свёртка directories начиная с (пустой список) как seen и directory → если пусто (отфильтровать seen где other → other равен directory) то (добавить directory к seen) иначе seen) + соединить (отобразить named как directory → соединить [directory, "\t", (к строке (длина (отфильтровать directories где other → other равен directory))), "\n"] по "") по "" + +тотальная функция «Setup» + возвращает список «Question» + пример «The binary and the place of temporary files» + ожидается [запись «Question» с «name» равным "arguments" и «order» равным (вариант «Прочитать доводы»), запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] + [(«Arguments» от "arguments"), («Environment» от "temporary" и "FLANG_TMP")] + +тотальная функция «Bootstrap» + принимает answers: список «Answer» + возвращает строка + пример «The bootstrap directory of the tree of the plan, seen from its root» + дано answers равно пустой список + ожидается "bootstrap" + пример «Of another tree, by its own path» + дано answers равно [запись «Answer» с «name» равным "arguments" и «reply» равным (вариант «Доводы» с доводы равным ["--root", "/r"])] + ожидается "/r/bootstrap" + если («Tree root» от answers) равен "../.." то "bootstrap" иначе (соединить [(«Tree root» от answers), "/bootstrap"] по "") + +тотальная функция «Start» + принимает answers: список «Answer» + возвращает список «Question» + пример «The root, the binary, its freshness, then a work directory» + дано answers равно [запись «Answer» с «name» равным "arguments" и «reply» равным (вариант «Доводы» с доводы равным ["--root", "/r"])] + ожидается [запись «Question» с «name» равным "root" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && pwd", "/r"]), запись «Question» с «name» равным "binary present" и «order» равным (вариант «Запустить процесс» с программа равным "test" и аргументы равным ["-x", "/r/bootstrap/flang"])] + [(«Run» от "root" и "sh" и ["-c", "cd \"$0\" && pwd", («Tree root» от answers)]), («Run» от "binary present" и "test" и ["-x", (соединить [(«Tree root» от answers), "/bootstrap/flang"] по "")])] + +тотальная функция «Looking» + принимает answers: список «Answer» + возвращает список «Question» + пример «Freshness first, then a work directory» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "look" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd \"$0\" && exec \"$@\"", "../..", "sh", "-c", "cd \"$0\" || exit 2; printf 'binary %s\\n' \"$(sha256sum flang 2>/dev/null | cut -d' ' -f1)\"; printf 'seed %s\\n' \"$(/bin/ls *.c *.h Makefile 2>/dev/null | LC_ALL=C sort | xargs cat | sha256sum | cut -d' ' -f1)\"; if [ -f Makefile ] && [ -f compiler_flang.c ]; then echo 'sources yes'; else echo 'sources no'; fi; make -q flang >/dev/null 2>&1; echo \"make $?\"; sed -n 's/^двоичный /written-binary /p; s/^семя /written-seed /p' flang.seed-sha256 2>/dev/null; exit 0", "bootstrap"]), запись «Question» с «name» равным "work" и «order» равным (вариант «Завести временный каталог» с образец равным "/srv/tmp/nesting.")] + [(«Look at» от "look" и («Bootstrap» от answers)), («Temporary directory» от "work" и (соединить [(«Setting of» от "temporary" и "/srv/tmp" и answers), "/nesting."] по ""))] + +тотальная функция «Printing» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is printed» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) то пустой список иначе [(«Run» от "printed" и "sh" и ["-c", («Print command»), («Tree root» от answers), («Work» от answers)])] + +тотальная функция «Sorting» + принимает answers: список «Answer» + возвращает список «Question» + пример «Nothing printed, nothing sorted» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "sorted" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "printf '%s' \"$0\" | sort -k2 -rn", ""])] + [(«Run» от "sorted" и "sh" и ["-c", "printf '%s' \"$0\" | sort -k2 -rn", («Directory counts» от («Printed» от answers))])] + +тотальная функция «Cleaning» + принимает answers: список «Answer» + возвращает список «Question» + пример «No work directory, nothing to clean» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) то пустой список иначе [(«Run» от "cleaned" и "rm" и ["-rf", («Work» от answers)])] + +тотальная функция «Stage» + принимает stages: число, answers: список «Answer» + возвращает список «Question» + пример «A stage outside the plan asks nothing» + дано stages равно 9 + дано answers равно пустой список + ожидается пустой список + разбор stages + случай 5 + то «Setup» + случай 4 + то «Start» от answers + случай 3 + то «Looking» от answers + случай 2 + то «Printing» от answers + случай 1 + то «Sorting» от answers + случай 0 + то «Cleaning» от answers + случай любое + то пустой список + +тотальная функция «Counted» + принимает outcomes: список строки, wanted: строка + возвращает число + пример «Outcomes of one kind» + дано outcomes равно ["same", "differs", "same"] + дано wanted равно "same" + ожидается 2 + длина (отфильтровать outcomes где outcome → outcome равен wanted) + +тотальная функция «Verdict» + принимает answers: список «Answer» + возвращает «Продолжение» + пример «An empty corpus is no failure» + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "записей корпуса\t0\nядро напечатало ту же запись побайтово\t0\nнапечатало другое\t0\nрасходится законно (подделка «лжёт-запись», названа поимённо)\t0\nоговорка проснулась (подделка совпала с печатью — ложь протухла)\t0\nпечать отказала\t0\nисходника в дереве нет\t0\n\n-- откуда исходники записей корпуса --" + пусть rows равно («Printed» от answers) + пусть outcomes равно (отобразить rows как row → «Outcome» от row) + пусть marks равно (соединить («Gathered words» от (отобразить rows как row → «Mark» от row)) по "") + пусть lines равно («Соединить списки» от [(соединить ["записей корпуса\t", (к строке (длина rows))] по ""), (соединить ["ядро напечатало ту же запись побайтово\t", (к строке («Counted» от outcomes и "same"))] по ""), (соединить ["напечатало другое\t", (к строке («Counted» от outcomes и "differs"))] по ""), (соединить ["расходится законно (подделка «лжёт-запись», названа поимённо)\t", (к строке («Counted» от outcomes и "allowed"))] по ""), (соединить ["оговорка проснулась (подделка совпала с печатью — ложь протухла)\t", (к строке («Counted» от outcomes и "awake"))] по ""), (соединить ["печать отказала\t", (к строке («Counted» от outcomes и "refused"))] по ""), (соединить ["исходника в дереве нет\t", (к строке («Counted» от outcomes и "missing"))] по "")] и («Соединить списки» от (если пусто marks то (пустой список) иначе [(соединить ["поимённо:", marks] по "")]) и («Соединить списки» от ["", "-- откуда исходники записей корпуса --"] и («Lines» от («Output of» от "sorted" и answers))))) + пусть troubles равно (длина (отфильтровать outcomes где outcome → не ((outcome равен "same") или (outcome равен "allowed")))) + если troubles равен 0 + то вариант «Конец работы» с значение равным (соединить lines по "\n") + иначе вариант «Провал» с код равным "FLANG_RECORDS_NESTING" и сообщение равным (соединить lines по "\n") + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «No kernel binary» + дано asked равно "binary present" + дано answers равно [запись «Answer» с «name» равным "binary present" и «reply» равным (вариант «Процесс завершён» с код равным 1 и вывод равным "" и ошибки равным "")] + ожидается ["нет двоичного ядра /bootstrap/flang — собрать: make -C bootstrap"] + пусть kernel равно (соединить [(«First line» от («Output of» от "root" и answers)), "/bootstrap/flang"] по "") + «Chosen» от [(«When» от ((asked равен "binary present") и притом (не ((«Exit code of» от asked и answers) равен 0))) и [(соединить ["нет двоичного ядра ", kernel, " — собрать: make -C bootstrap"] по "")]), + («When» от ((asked равен "look") и притом ((«Verdict of» от («Look answer» от "look" и answers)) равен "отстало")) и [(соединить ["ЯДРО ОТСТАЛО ОТ СЕМЕНИ: ", kernel, " собран не из нынешнего bootstrap/*.c, *.h, Makefile.\nМерить нечем — старое ядро печатает старые записи и объявит свежие отставшими.\nПересобрать: make -C bootstrap -j8 && bootstrap/flang io flang/proof/binary-fingerprint.fscript"] по "")]), + («When» от ((asked равен "work") и притом (пусто («Work» от answers))) и ["временный каталог не заведён: каталога из FLANG_TMP (по умолчанию /srv/tmp) нет либо он не для записи"])] и (пустой список) + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + пример «An empty queue at the last stage gives the verdict» + дано queue равно пустой список + дано stages равно 0 + дано answers равно пустой список + ожидается вариант «Конец работы» с значение равным "записей корпуса\t0\nядро напечатало ту же запись побайтово\t0\nнапечатало другое\t0\nрасходится законно (подделка «лжёт-запись», названа поимённо)\t0\nоговорка проснулась (подделка совпала с печатью — ложь протухла)\t0\nпечать отказала\t0\nисходника в дереве нет\t0\n\n-- откуда исходники записей корпуса --" + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Verdict» от answers + иначе «Proceed» от («Stage» от (stages минус 1) и answers) и (stages минус 1) и answers + +тотальная функция «Begin» + возвращает «Inquiry» + пример «Six stages lie ahead» + ожидается запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + «Begin with» от 6 + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пример «The first turn asks for the arguments» + дано inquiry равно запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 6 и «answers» равным пустой список + дано reply равно вариант «Пока ничего» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать доводы») и потом равным (запись «Inquiry» с «asked» равным "arguments" и «queue» равным [запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP")] и «stages» равным 5 и «answers» равным пустой список) + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то если пусто («Work» от answers) + то вариант «Не проверено» с код равным "FLANG_RECORDS_NESTING_NOT_MEASURED" и сообщение равным голова + иначе вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "rm" и аргументы равным ["-rf", («Work» от answers)]) и потом равным (запись «Inquiry» с «asked» равным (соединить ["stopped: ", голова] по "") и «queue» равным пустой список и «stages» равным 0 и «answers» равным answers) + случай пусто + то если (inquiry.«asked») начинается с "stopped: " + то вариант «Не проверено» с код равным "FLANG_RECORDS_NESTING_NOT_MEASURED" и сообщение равным («After» от "stopped: " и (inquiry.«asked»)) + иначе «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Records nesting» + состояние «Inquiry» + начинает с «Begin» + обрабатывает «Next» diff --git a/flang/proof/share-ledger-forgery.fscript b/flang/proof/share-ledger-forgery.fscript new file mode 100644 index 000000000..1a895d3db --- /dev/null +++ b/flang/proof/share-ledger-forgery.fscript @@ -0,0 +1,235 @@ +модуль «Share ledger forgery» + использует «Rules» из "../../scripts/rules.fscript" + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Reading» из "../../scripts/reading.fscript" + использует «Tables» из "../../scripts/tables.fscript" + использует «Kernel verdict» из "kernel-verdict.fscript" только «Ledger command» + использует «Lists» только «Соединить списки» + +тотальная функция «Source» + возвращает строка + пример «The source the probe spoils» + ожидается "flang/proof/examples/corpus-natural.flang" + "flang/proof/examples/corpus-natural.flang" + +тотальная функция «Record» + возвращает строка + пример «The honest record of that source» + ожидается "flang/proof/checker/tests/records/corpus/corpus-natural.record" + "flang/proof/checker/tests/records/corpus/corpus-natural.record" + +тотальная функция «Work» + принимает answers: список «Answer» + возвращает строка + пример «No work directory yet» + дано answers равно пустой список + ожидается "" + «Made of» от "work" и answers + +тотальная функция «In work» + принимает name: строка, answers: список «Answer» + возвращает строка + пример «A file in the work directory» + дано name равно "a.tsv" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается "/w/a.tsv" + соединить [(«Work» от answers), "/", name] по "" + +тотальная функция «Root» + принимает answers: список «Answer» + возвращает строка + пример «The root as the shell sees it» + дано answers равно [запись «Answer» с «name» равным "root" и «reply» равным (вариант «Процесс завершён» с код равным 0 и вывод равным "/t\n" и ошибки равным "")] + ожидается "/t" + «First line» от («Output of» от "root" и answers) + +тотальная функция «Minus» + принимает text: строка + возвращает строка + пример «The sum becomes a difference» + дано text равно "а\n первое плюс второе\nб\n" + ожидается "а\n первое минус второе\nб\n" + соединить (отобразить (разделить text по "\n") как line → если line равен " первое плюс второе" то " первое минус второе" иначе line) по "\n" + +тотальная функция «Swapped» + принимает text: строка + возвращает строка + пример «The record names a file outside the commit» + дано text равно "запись\nисходник flang/a.flang\nконец\n" + ожидается "запись\nисходник own/brazen.flang\nконец\n" + соединить (отобразить (разделить text по "\n") как line → если line начинается с "исходник " то "исходник own/brazen.flang" иначе line) по "\n" + +тотальная функция «Build command» + возвращает строка + пример «A spoiled tree and two sets of records» + ожидается "mkdir -p \"$0/honest\" \"$0/swapped\" \"$0/tree/flang/proof/examples\" \"$0/tree/flang/proof/checker\" \"$0/tree/own\" && cp \"$1/flang/proof/checker/сверщик\" \"$0/tree/flang/proof/checker/сверщик\" && cp \"$1/flang/proof/examples/corpus-natural.flang\" \"$0/tree/own/brazen.flang\" && cp \"$1/flang/proof/checker/tests/records/corpus/corpus-natural.record\" \"$0/honest/corpus-natural.record\"" + "mkdir -p \"$0/honest\" \"$0/swapped\" \"$0/tree/flang/proof/examples\" \"$0/tree/flang/proof/checker\" \"$0/tree/own\" && cp \"$1/flang/proof/checker/сверщик\" \"$0/tree/flang/proof/checker/сверщик\" && cp \"$1/flang/proof/examples/corpus-natural.flang\" \"$0/tree/own/brazen.flang\" && cp \"$1/flang/proof/checker/tests/records/corpus/corpus-natural.record\" \"$0/honest/corpus-natural.record\"" + +тотальная функция «Share run» + принимает name: строка, root: строка, set: строка, dump: строка, answers: список «Answer» + возвращает «Question» + пример «The share instrument on a tree, a ledger and a set» + дано name равно "control" + дано root равно "/t" + дано set равно "/w/honest" + дано dump равно "/w/control.tsv" + дано answers равно [запись «Answer» с «name» равным "work" и «reply» равным (вариант «Заведено» с путь равным "/w")] + ожидается запись «Question» с «name» равным "control" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "sh \"$0\" --корень \"$1\" --ведомость \"$2\" --набор \"$3\" --разбор \"$4\" > /dev/null 2>&1", "/flang/proof/corpus-share.sh", "/t", "/w/ledger.tsv", "/w/honest", "/w/control.tsv"]) + «Run» от name и "sh" и ["-c", "sh \"$0\" --корень \"$1\" --ведомость \"$2\" --набор \"$3\" --разбор \"$4\" > /dev/null 2>&1", (соединить [(«Root» от answers), "/flang/proof/corpus-share.sh"] по ""), root, («In work» от "ledger.tsv" и answers), set, dump] + +тотальная функция «Setup» + возвращает список «Question» + пример «The root, the source and its record» + ожидается [запись «Question» с «name» равным "temporary" и «order» равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP"), запись «Question» с «name» равным "root" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd ../.. && pwd"]), запись «Question» с «name» равным "source" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/examples/corpus-natural.flang"), запись «Question» с «name» равным "record" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/checker/tests/records/corpus/corpus-natural.record")] + [(«Environment» от "temporary" и "FLANG_TMP"), («Run» от "root" и "sh" и ["-c", "cd ../.. && pwd"]), («Read» от "source" и (соединить ["../../", («Source»)] по "")), («Read» от "record" и (соединить ["../../", («Record»)] по ""))] + +тотальная функция «Start» + принимает answers: список «Answer» + возвращает список «Question» + пример «A work directory and the checker» + дано answers равно пустой список + ожидается [запись «Question» с «name» равным "work" и «order» равным (вариант «Завести временный каталог» с образец равным "/srv/tmp/ledger-forgery."), запись «Question» с «name» равным "checker present" и «order» равным (вариант «Запустить процесс» с программа равным "test" и аргументы равным ["-x", "/flang/proof/checker/сверщик"])] + [(«Temporary directory» от "work" и (соединить [(«Setting of» от "temporary" и "/srv/tmp" и answers), "/ledger-forgery."] по "")), («Run» от "checker present" и "test" и ["-x", (соединить [(«Root» от answers), "/flang/proof/checker/сверщик"] по "")])] + +тотальная функция «Building» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is built» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) + то пустой список + иначе [(«Run» от "ledger" и "sh" и ["-c", («Ledger command»), («Root» от answers), "HEAD", («Work» от answers)]), («Run» от "built" и "sh" и ["-c", («Build command»), («Work» от answers), («Root» от answers)]), («Write» от "spoiled source" и (соединить [(«In work» от "tree/" и answers), («Source»)] по "") и («Minus» от («Output of» от "source" и answers))), («Write» от "swapped record" и («In work» от "swapped/corpus-natural.record" и answers) и («Swapped» от («Output of» от "record" и answers)))] + +тотальная функция «Measuring» + принимает answers: список «Answer» + возвращает список «Question» + пример «Without a work directory nothing is measured» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) + то пустой список + иначе [(«Share run» от "control" и («Root» от answers) и («In work» от "honest" и answers) и («In work» от "control.tsv" и answers) и answers), («Share run» от "outside" и («In work» от "tree" и answers) и («In work» от "swapped" и answers) и («In work» от "a.tsv" и answers) и answers), («Share run» от "drifted" и («In work» от "tree" и answers) и («In work» от "honest" и answers) и («In work» от "b.tsv" и answers) и answers), («Read» от "control dump" и («In work» от "control.tsv" и answers)), («Read» от "outside dump" и («In work» от "a.tsv" и answers)), («Read» от "drifted dump" и («In work» от "b.tsv" и answers))] + +тотальная функция «Cleaning» + принимает answers: список «Answer» + возвращает список «Question» + пример «No work directory, nothing to clean» + дано answers равно пустой список + ожидается пустой список + если пусто («Work» от answers) то пустой список иначе [(«Run» от "cleaned" и "rm" и ["-rf", («Work» от answers)])] + +тотальная функция «Stage» + принимает stages: число, answers: список «Answer» + возвращает список «Question» + пример «A stage outside the plan asks nothing» + дано stages равно 9 + дано answers равно пустой список + ожидается пустой список + разбор stages + случай 4 + то «Setup» + случай 3 + то «Start» от answers + случай 2 + то «Building» от answers + случай 1 + то «Measuring» от answers + случай 0 + то «Cleaning» от answers + случай любое + то пустой список + +тотальная функция «Class rows» + принимает dump: строка, wanted: строка + возвращает число + пример «Rows the share instrument put in one class» + дано dump равно "head\na\tb\tc\td\te\tf\tg\th\ti\tj\tk\tl\tm\tn\to\tР5\n" + дано wanted равно "Р5" + ожидается 1 + длина (отфильтровать («Rows» от dump) где row → («Cell» от 16 и row) равен wanted) + +тотальная функция «Probe lines» + принимает answers: список «Answer» + возвращает список строки + пример «Nothing measured fails all three» + дано answers равно пустой список + ожидается ["контроль: честная запись на честном дереве\tПРОВАЛ (код 127, Р0=0)", "подлог А: исходник вне коммита\tПРОШЁЛ — охраны нет (код 127, Р5=0)", "подлог Б: файл дерева разошёлся с коммитом\tПРОШЁЛ — охраны нет (код 127, Р5=0)"] + пусть control равно («Exit code of» от "control" и answers) + пусть kept равно («Class rows» от («Output of» от "control dump" и answers) и "Р0") + пусть outside равно («Exit code of» от "outside" и answers) + пусть stranger равно («Class rows» от («Output of» от "outside dump" и answers) и "Р5") + пусть drifted равно («Exit code of» от "drifted" и answers) + пусть changed равно («Class rows» от («Output of» от "drifted dump" и answers) и "Р5") + [(если (control равен 0) и притом (kept равен 1) то "контроль: честная запись на честном дереве\tЦЕЛА (Р0, код 0)" иначе (соединить ["контроль: честная запись на честном дереве\tПРОВАЛ (код ", (к строке control), ", Р0=", (к строке kept), ")"] по "")), + (если (outside равен 1) и притом (stranger равен 1) то "подлог А: исходник вне коммита\tОТВЕРГНУТ (Р5, код 1)" иначе (соединить ["подлог А: исходник вне коммита\tПРОШЁЛ — охраны нет (код ", (к строке outside), ", Р5=", (к строке stranger), ")"] по "")), + (если (drifted равен 1) и притом (changed равен 1) то "подлог Б: файл дерева разошёлся с коммитом\tОТВЕРГНУТ (Р5, код 1)" иначе (соединить ["подлог Б: файл дерева разошёлся с коммитом\tПРОШЁЛ — охраны нет (код ", (к строке drifted), ", Р5=", (к строке changed), ")"] по ""))] + +тотальная функция «Verdict» + принимает answers: список «Answer» + возвращает «Продолжение» + пример «A source without the line to spoil is no probe at all» + дано answers равно пустой список + ожидается вариант «Провал» с код равным "FLANG_LEDGER_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: строки «первое плюс второе» в «flang/proof/examples/corpus-natural.flang» больше нет — поправить пробу, линейка ни при чём" + пусть lines равно («Probe lines» от answers) + «Chosen» от [(«When» от ((«Minus» от («Output of» от "source" и answers)) равен («Output of» от "source" и answers)) и (вариант «Провал» с код равным "FLANG_LEDGER_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: строки «первое плюс второе» в «flang/proof/examples/corpus-natural.flang» больше нет — поправить пробу, линейка ни при чём")), + («When» от (пусто (отфильтровать lines где line → (line содержит "ПРОВАЛ") или (line содержит "ПРОШЁЛ"))) и (вариант «Конец работы» с значение равным (соединить (добавить "проба порчи на ведомость: подделка отвергнута, честная запись зелена" к lines) по "\n")))] и (вариант «Провал» с код равным "FLANG_LEDGER_FORGERY" и сообщение равным (соединить lines по "\n")) + +тотальная функция «Obstacles» + принимает asked: строка, answers: список «Answer» + возвращает список строки + пример «No checker» + дано asked равно "checker present" + дано answers равно [запись «Answer» с «name» равным "checker present" и «reply» равным (вариант «Процесс завершён» с код равным 1 и вывод равным "" и ошибки равным "")] + ожидается ["нет чекера /flang/proof/checker/сверщик — собрать: make -C flang/proof/checker"] + пусть failed равно (не ((«Exit code of» от asked и answers) равен 0)) + «Chosen» от [(«When» от ((asked равен "checker present") и притом failed) и [(соединить ["нет чекера ", («Root» от answers), "/flang/proof/checker/сверщик — собрать: make -C flang/proof/checker"] по "")]), + («When» от (((asked равен "source") или (asked равен "record")) и притом failed) и ["ПОДЛОГ НЕ СОБРАЛСЯ: нет «flang/proof/examples/corpus-natural.flang» или его записи — поправить пробу, линейка ни при чём"]), + («When» от ((asked равен "ledger") и притом failed) и ["ведомость не построена: коммит HEAD не отдал дерево"]), + («When» от ((asked равен "built") и притом failed) и ["ПОДЛОГ НЕ СОБРАЛСЯ: подменное дерево не сложилось"]), + («When» от ((asked равен "work") и притом (пусто («Work» от answers))) и ["временный каталог не заведён: каталога из FLANG_TMP (по умолчанию /srv/tmp) нет либо он не для записи"])] и (пустой список) + +тотальная функция «Proceed» + принимает queue: список «Question», stages: число, answers: список «Answer» + возвращает «Продолжение» + пример «An empty queue at the last stage gives the verdict» + дано queue равно пустой список + дано stages равно 0 + дано answers равно пустой список + ожидается вариант «Провал» с код равным "FLANG_LEDGER_FORGERY" и сообщение равным "ПОДЛОГ НЕ СОБРАЛСЯ: строки «первое плюс второе» в «flang/proof/examples/corpus-natural.flang» больше нет — поправить пробу, линейка ни при чём" + разбор queue + случай голова и хвост + то «Ask» от (голова) и (хвост) и stages и answers + случай пусто + то если stages не больше 0 + то «Verdict» от answers + иначе «Proceed» от («Stage» от (stages минус 1) и answers) и (stages минус 1) и answers + +тотальная функция «Begin» + возвращает «Inquiry» + пример «Five stages lie ahead» + ожидается запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 5 и «answers» равным пустой список + «Begin with» от 5 + +тотальная функция «Next» + принимает inquiry: «Inquiry», reply: «Отклик» + возвращает «Продолжение» + пример «The first turn asks for the place of temporary files» + дано inquiry равно запись «Inquiry» с «asked» равным "" и «queue» равным пустой список и «stages» равным 5 и «answers» равным пустой список + дано reply равно вариант «Пока ничего» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "FLANG_TMP") и потом равным (запись «Inquiry» с «asked» равным "temporary" и «queue» равным [запись «Question» с «name» равным "root" и «order» равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", "cd ../.. && pwd"]), запись «Question» с «name» равным "source" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/examples/corpus-natural.flang"), запись «Question» с «name» равным "record" и «order» равным (вариант «Прочитать файл» с путь равным "../../flang/proof/checker/tests/records/corpus/corpus-natural.record")] и «stages» равным 4 и «answers» равным пустой список) + пусть answers равно («Heard» от inquiry и reply) + разбор («Obstacles» от (inquiry.«asked») и answers) + случай голова и хвост + то если пусто («Work» от answers) + то вариант «Не проверено» с код равным "FLANG_LEDGER_FORGERY_NOT_MEASURED" и сообщение равным голова + иначе вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "rm" и аргументы равным ["-rf", («Work» от answers)]) и потом равным (запись «Inquiry» с «asked» равным (соединить ["stopped: ", голова] по "") и «queue» равным пустой список и «stages» равным 0 и «answers» равным answers) + случай пусто + то если (inquiry.«asked») начинается с "stopped: " + то вариант «Не проверено» с код равным "FLANG_LEDGER_FORGERY_NOT_MEASURED" и сообщение равным («After» от "stopped: " и (inquiry.«asked»)) + иначе «Proceed» от (inquiry.«queue») и (inquiry.«stages») и answers + +план «Share ledger forgery» + состояние «Inquiry» + начинает с «Begin» + обрабатывает «Next» diff --git a/scripts/ledgers/file-name-words.txt b/scripts/ledgers/file-name-words.txt index 95fd49700..32aa31a37 100644 --- a/scripts/ledgers/file-name-words.txt +++ b/scripts/ledgers/file-name-words.txt @@ -1032,6 +1032,7 @@ neighbour neighbours neither nested +nesting network neutral never diff --git a/scripts/ledgers/guards-without-forgery-probe.json b/scripts/ledgers/guards-without-forgery-probe.json index 3573ed396..e012e6505 100644 --- a/scripts/ledgers/guards-without-forgery-probe.json +++ b/scripts/ledgers/guards-without-forgery-probe.json @@ -39,5 +39,7 @@ "claims:check": "сторож КРАСЕН по делу и в CI не стоит — пробу строить рано: сперва закрыть долг, на котором он краснеет. КРАСЕН по делу (5 с). Ставить в CI нельзя, пока долг не закрыт; глушит", "homebrew-formula:check": "CI ЗОВЁТ ЕГО И ЕМУ ВЕРИТ, а покраснеть на порче не показано ни разу. Самый опасный род: выпотрошенный сторож останется зелёным, и сказать об этом будет некому. Пробу строить в первую очередь.", "checker:check": "CI ЗОВЁТ ЕГО И ЕМУ ВЕРИТ, а покраснеть на порче не показано ни разу. Самый опасный род: выпотрошенный сторож останется зелёным, и сказать об этом будет некому. Пробу строить в первую очередь.", - "numbers:check": "СТОРОЖ ПРОГНАН ЦЕЛИКОМ, пробы всё ещё нет: код 1 за 6864 с — 1 ч 54 мин (перемер 6 сентября 2026, свой прогон), бед 20. Цена та же, что у подсчётов: обход 295 файлов корпуса. Прежняя запись 5 сентября: код 124 на 200 с (задача 5612)." + "numbers:check": "СТОРОЖ ПРОГНАН ЦЕЛИКОМ, пробы всё ещё нет: код 1 за 6864 с — 1 ч 54 мин (перемер 6 сентября 2026, свой прогон), бед 20. Цена та же, что у подсчётов: обход 295 файлов корпуса. Прежняя запись 5 сентября: код 124 на 200 с (задача 5612).", + "kernel-verdict:check": "проба есть — flang/proof/kernel-verdict-forgery.fscript (короткая команда kernel-verdict:forgery), но в CI её не ставят вместе с самим сторожем: сторож КРАСЕН по делу (37 файлов, замер 1 октября 2026).", + "proved-share:check": "проба есть и стоит в CI — flang/proof/share-ledger-forgery.fscript (binary.yml, «if ! … share-ledger-forgery.fscript»), но это другой файл, чем сам сторож corpus-share.sh, и сличение по имени файла её не видит." } diff --git a/scripts/ledgers/uncalled-guards.json b/scripts/ledgers/uncalled-guards.json index 11a0217ac..1af62d628 100644 --- a/scripts/ledgers/uncalled-guards.json +++ b/scripts/ledgers/uncalled-guards.json @@ -25,5 +25,6 @@ "child-timeout:check": "ЗЕЛЕН и не дёшев (72 с). В CI не поставлен: сторожу верят только после того, как он покраснел на подлоге, а подлог не построен.", "bootstrap-point:check": "НЕ ЗАМЕР, А РАБОТА НА ПОЛСУТОК: сторож печатает семя целиком — flang emit flang/self/bootstrap/compiler.flang --target c. Два своих захода 6 сентября сняты на 3014 с и свыше 3900 с, оба стояли на этой печати и вывода не дали. Цена дошедшего захода печати — 12 ч 05 мин 21 с (docs/reprint-cost.md, замер 3 сентября, чужой). В смену не влезает и в CI не влезет; различать «дорого» и «не сходится» тут нечего. Прежняя запись 5 сентября: дороже предела замера, код 124 на 200 с (задача 5612).", "claims:check": "КРАСЕН по делу (5 с). Ставить в CI нельзя, пока долг не закрыт; глушить — тем более.", - "numbers:check": "КРАСЕН по делу и ОЧЕНЬ ДОРОГ: код 1 за 6864 с, то есть 1 ч 54 мин (перемер 6 сентября 2026, свой прогон). Сходится. Бед 20, среди них «утверждения.сеткой: в numbers.json 556, в дереве 791»; сам печатает «лечится одной командой: bootstrap/flang run-script numbers:build». Цена та же, что у подсчётов: обход 295 файлов корпуса через flang check --proof. Прежняя запись 5 сентября: дороже предела замера, код 124 на 200 с (задача 5612)." + "numbers:check": "КРАСЕН по делу и ОЧЕНЬ ДОРОГ: код 1 за 6864 с, то есть 1 ч 54 мин (перемер 6 сентября 2026, свой прогон). Сходится. Бед 20, среди них «утверждения.сеткой: в numbers.json 556, в дереве 791»; сам печатает «лечится одной командой: bootstrap/flang run-script numbers:build». Цена та же, что у подсчётов: обход 295 файлов корпуса через flang check --proof. Прежняя запись 5 сентября: дороже предела замера, код 124 на 200 с (задача 5612).", + "kernel-verdict:check": "КРАСЕН по делу: на дереве a4ab61a07 ядро отвергает 37 файлов, о которых в дереве лежат записи (замер 1 октября 2026, прогон flang/proof/kernel-verdict.fscript и прежнего corpus-share.sh --приговор-ядра дал один и тот же текст). Званым он прежде числился только потому, что CI звал тот же файл corpus-share.sh другими ключами; ставить в CI нельзя, пока долг не закрыт." } diff --git a/scripts/report-provenance.fscript b/scripts/report-provenance.fscript index dfe537490..f1e4024ba 100644 --- a/scripts/report-provenance.fscript +++ b/scripts/report-provenance.fscript @@ -115,7 +115,7 @@ возвращает строка пусть beside равно («Output of» от "fingerprint beside binary" и answers) пусть binary равно («Sum of» от "bootstrap/flang" и («Output of» от "sums" и answers)) - «Chosen» от [(«When» от ((пусто beside) или (не ((«Value after» от "двоичный " и beside) равен binary))) и ("отпечатка при этом двоичном нет — свежесть НЕ ПРОВЕРЕНА (записать: sh flang/proof/corpus-share.sh --отпечаток)")), + «Chosen» от [(«When» от ((пусто beside) или (не ((«Value after» от "двоичный " и beside) равен binary))) и ("отпечатка при этом двоичном нет — свежесть НЕ ПРОВЕРЕНА (записать: bootstrap/flang io flang/proof/binary-fingerprint.fscript)")), («When» от ((«Value after» от "семя " и beside) равен («Build inputs» от answers)) и ("собран из нынешнего семени (по отпечатку bootstrap/flang.seed-sha256)"))] и ("ОТСТАЛ ОТ СЕМЕНИ: собран не из нынешних bootstrap/*.c — пересобрать: make -C bootstrap") тотальная функция «Binary present»