Registry: the lock closes every form and resolution is proved by a corpus

.flangrc

@@ -200,6 +200,12 @@ script.releases:page = bootstrap/flang io scripts/site/releases-page.fscript --m
 script.releases:page:check = bootstrap/flang io scripts/site/releases-page-verify.fscript --max-steps 80000000 --на-веру
 script.registry:page = bootstrap/flang io scripts/site/registry-page.fscript --plan 'Напечатать страницу реестра'
 script.registry:publish = bootstrap/flang io scripts/site/registry-page.fscript --plan 'Выложить ведомость'
+script.registry-resolution:check = bootstrap/flang io scripts/guards/registry-resolution-guard.fscript --plan Check
+script.registry-resolution:forgery = bootstrap/flang io scripts/guards/registry-resolution-guard.fscript --plan Forgery
+script.registry-resolution:measure = bootstrap/flang io scripts/guards/registry-resolution-guard.fscript --plan Measure
+script.registry-prints:check = bootstrap/flang io scripts/registry-tool.fscript --plan 'Сверить отпечатки'
+script.lock-forms:check = bootstrap/flang io scripts/guards/lock-closes-every-form.fscript --plan Check
+script.lock-forms:forgery = bootstrap/flang io scripts/guards/lock-closes-every-form.fscript --plan Forgery
 script.reprint = sh scripts/bootstrap-reprint.sh
 script.reprint:check = sh scripts/bootstrap-reprint.sh --check
 script.bootstrap-point:check = bootstrap/flang io scripts/seed/bootstrap-point-by-binary.fscript --timeout 2400000 --на-веру

.githooks/pre-push.fscript

@@ -16,8 +16,11 @@
 
 тотальная функция «Checks»
   возвращает список «Check»
-  обеспечивает «there are exactly twenty-one checks» (длина результат) равен 21
+  обеспечивает «there are exactly twenty-four checks» (длина результат) равен 24
   [запись «Check» с «name» равным "prose-numbers-guard" и «command» равным "bootstrap/flang io scripts/guards/prose-numbers-guard.fscript --plan Check",
+   запись «Check» с «name» равным "registry" и «command» равным "bootstrap/flang run-script registry-resolution:check",
+   запись «Check» с «name» равным "prints" и «command» равным "bootstrap/flang run-script registry-prints:check",
+   запись «Check» с «name» равным "lock-forms" и «command» равным "bootstrap/flang run-script lock-forms:check",
    запись «Check» с «name» равным "seed-runtime-is-source" и «command» равным "bootstrap/flang io scripts/seed/seed-runtime-is-source.fscript --plan Check",
    запись «Check» с «name» равным "seed-refresh" и «command» равным "bootstrap/flang io scripts/seed/seed-refresh.fscript --plan Check",
    запись «Check» с «name» равным "version-derivations-guard" и «command» равным "bootstrap/flang io scripts/guards/version-derivations-guard.fscript --plan Проверка",
@@ -318,7 +321,7 @@
 тотальная функция «Leftovers»
   принимает directory: строка
   возвращает список строки
-  обеспечивает «one file for every check and the directory itself» (длина результат) равен 22
+  обеспечивает «one file for every check and the directory itself» (длина результат) равен 25
   добавить directory к (отобразить («Checks») как check → («Output path» от directory и check))
 
 тотальная функция «Remove files»

.github/workflows/ci.yml

@@ -1913,3 +1913,86 @@ jobs:
         env:
           FLANG_TMP: ${{ runner.temp }}
 
+
+  registry-resolution:
+    name: registry-resolution
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - name: Check verdict cache
+        uses: ./.github/actions/release-without-cache
+      - run: make -C bootstrap -j"$(nproc)"
+      - name: Probe registry resolution by a forged corpus
+        run: |
+          if bootstrap/flang run-script registry-resolution:forgery; then
+            echo "the guard stayed green on a forged corpus" >&2
+            exit 1
+          fi
+      - name: Probe registry resolution by a cut ledger
+        run: |
+          ledger=packaging/registry/cases/ledger.list
+          cp "$ledger" "$RUNNER_TEMP/ledger.list"
+          grep -v '^Логика | 1.2.0' "$RUNNER_TEMP/ledger.list" > "$ledger"
+          if cmp -s "$ledger" "$RUNNER_TEMP/ledger.list"; then
+            cp "$RUNNER_TEMP/ledger.list" "$ledger"
+            echo "the row was not cut, nothing to probe" >&2
+            exit 1
+          fi
+          if bootstrap/flang run-script registry-resolution:check > "$RUNNER_TEMP/cut.out" 2>&1; then
+            cp "$RUNNER_TEMP/ledger.list" "$ledger"
+            cat "$RUNNER_TEMP/cut.out" >&2
+            echo "the guard stayed green with a chosen version cut out" >&2
+            exit 1
+          fi
+          cp "$RUNNER_TEMP/ledger.list" "$ledger"
+          cmp "$ledger" "$RUNNER_TEMP/ledger.list"
+      - name: Check registry resolution
+        run: bootstrap/flang run-script registry-resolution:check
+      - name: Probe registry fingerprints
+        run: |
+          ledger=scripts/registry-example/registry.list
+          cp "$ledger" "$RUNNER_TEMP/registry.list"
+          sed -i '2s/| 1dc6/| Xdc6/' "$ledger"
+          if cmp -s "$ledger" "$RUNNER_TEMP/registry.list"; then
+            cp "$RUNNER_TEMP/registry.list" "$ledger"
+            echo "the forged fingerprint did not land, nothing to probe" >&2
+            exit 1
+          fi
+          if bootstrap/flang run-script registry-prints:check > "$RUNNER_TEMP/probe.out" 2>&1; then
+            cp "$RUNNER_TEMP/registry.list" "$ledger"
+            cat "$RUNNER_TEMP/probe.out" >&2
+            echo "the guard stayed green on a bent fingerprint" >&2
+            exit 1
+          fi
+          cp "$RUNNER_TEMP/registry.list" "$ledger"
+          cmp "$ledger" "$RUNNER_TEMP/registry.list"
+      - name: Check registry fingerprints
+        run: bootstrap/flang run-script registry-prints:check
+      - name: Probe lock forms by a forged measurement
+        run: |
+          if bootstrap/flang run-script lock-forms:forgery; then
+            echo "the guard stayed green on a forged measurement" >&2
+            exit 1
+          fi
+      - name: Probe lock forms by the old binary
+        run: |
+          cp bootstrap/flang_repl.c "$RUNNER_TEMP/flang_repl.c"
+          sed -i 's/wanted_bytes != 0/wanted_bytes == 0/' bootstrap/flang_repl.c
+          if cmp -s bootstrap/flang_repl.c "$RUNNER_TEMP/flang_repl.c"; then
+            cp "$RUNNER_TEMP/flang_repl.c" bootstrap/flang_repl.c
+            echo "the old behaviour did not land in the seed, nothing to probe" >&2
+            exit 1
+          fi
+          make -C bootstrap -j"$(nproc)"
+          if bootstrap/flang run-script lock-forms:check > "$RUNNER_TEMP/old.out" 2>&1; then
+            cp "$RUNNER_TEMP/flang_repl.c" bootstrap/flang_repl.c
+            make -C bootstrap -j"$(nproc)"
+            cat "$RUNNER_TEMP/old.out" >&2
+            echo "the guard stayed green on the old lock behaviour" >&2
+            exit 1
+          fi
+          cp "$RUNNER_TEMP/flang_repl.c" bootstrap/flang_repl.c
+          cmp bootstrap/flang_repl.c "$RUNNER_TEMP/flang_repl.c"
+          make -C bootstrap -j"$(nproc)"
+      - name: Check lock forms
+        run: bootstrap/flang run-script lock-forms:check

docs/DESCRIPTION.md

@@ -1440,8 +1440,9 @@ $ flang io доводы.flang -- раз два три
 Модули стандартной библиотеки импортируются по имени, например
 `использует «Lists»`.
 
-`flang lock` печатает lock-файл — JSON с исходниками модулей, импортированных
-формой `из "путь"`, и sha256 каждого. Если файл `flang.lock` лежит рядом с
+`flang lock` печатает lock-файл — JSON с исходниками всех модулей замыкания и
+sha256 каждого: и названных формой `из "путь"`, и найденных по имени, и
+привезённых пакетом `.flang-package`. Если файл `flang.lock` лежит рядом с
 программой, команды берут эти модули из него, и исходники на диске не нужны.
 
 `flang package` печатает пакет: тот же JSON с именем и версией из файла
@@ -1670,8 +1671,6 @@ script.site:build = node docs/site/build.mjs
   не полностью: `flang check` отвечает кодом 2, `flang emit` на программе с
   морфизмами, моноидами или монадами — кодом 3. На программе с процессами
   `flang check --proof` отвечает кодом 0, хотя `flang check` — кодом 2.
-- В lock-файл `flang lock` попадают только модули, импортированные формой
-  `из "путь"`; модуль, найденный по имени, в него не записывается.
 - Независимый checker перепроверяет не каждое доказательство: часть мест он
   принимает со слов ядра и называет их в отчёте. На пробе
   [`step-by-restricted-postcondition.flang`](../flang/proof/checker/tests/families/citation/step-by-restricted-postcondition.flang)

docs/adr/0059-the-registry-is-a-ledger-of-names-not-a-store-of-code.md

@@ -93,6 +93,13 @@ ADR-0021 обещает воспроизводимость: «После уст
 двоичным. Пакет из реестра рядом с двоичным не лежит, и для него тот же прогон
 даст отказ.
 
+**Замок после правки задачи 2031.** `flang lock` замыкает все три формы: по
+имени — код 0, **модулей 3**; `из "путь"` на `.flang` — код 0, **модулей 3**
+(замыкание `hmac.flang` само ввозит модули по имени); пакет по пути — **код 0**,
+модулей 1. У каждой формы модулей ровно «файлов вместе с импортами» минус
+входной файл. Сторож — `scripts/guards/lock-closes-every-form.fscript`
+(`lock-forms:check`).
+
 **Дерево после прогонов.** План `«Собрать реестр»` из
 `scripts/registry-tool.fscript` пишет в `scripts/registry-example/registry.list`
 и во время замера его перезаписал (4 строки из 7); файл возвращён
@@ -212,19 +219,32 @@ ADR-0021 обещает воспроизводимость: «После уст
 
 ## 7. Как разрешение сдаётся прибором, а не обещанием
 
-Четыре прогона, у каждого своя подделка. Прибор кладёт задача 4909; корпус
-случаев — `packaging/registry/cases/`, сторож — `scripts/guards/`.
+Четыре прогона, у каждого своя подделка. Корпус
+случаев — `packaging/registry/cases/`, сторож —
+`scripts/guards/registry-resolution-guard.fscript`, работа CI —
+`registry-resolution` в `.github/workflows/ci.yml`.
 
-| что проверяется | прогон | подделка, на которой сторож ОБЯЗАН покраснеть | состояние 4 октября 2026 |
+| что проверяется | прогон | подделка, на которой сторож ОБЯЗАН покраснеть | состояние |
 |---|---|---|---|
-| ответ не зависит от порядка строк ведомости | разрешение на N перестановок, ответы сверяются побайтово | убрать из ведомости версию, которая выбиралась: ответ обязан измениться | измерено руками: 7 порядков → 1 ответ; подделка меняет ответ. Сторожа нет |
-| ведомость согласна с файлами | пересчёт `sha256` каждого адреса против поля `отпечаток` | подкрутить один знак отпечатка | план есть, **краснеет сегодня: 3 из 7** (§4). CI его не зовёт |
-| отказ назван, а не проглочен | четыре запроса из таблицы §5 | снять причину из текста отказа — сторож сверяет код И текст | измерено руками, четыре кода. Сторожа нет |
-| замок замыкает поставленное | поставить пакет, собрать замок, собрать программу в пустом каталоге | тот же каталог без замка обязан отказать | **невозможно сегодня** (§3). Задача 2031 |
+| ответ не зависит от порядка строк ведомости | разрешение на N перестановок, ответы сверяются побайтово | убрать из ведомости версию, которая выбиралась: ответ обязан измениться | **сдано прибором** (`registry-resolution:check`): случаев 6, порядков ведомости 20, снятых выбранных записей 4, код 0. Снятие `Логика 1.2.0` краснит сторожа кодом 1 |
+| ведомость согласна с файлами | пересчёт `sha256` каждого адреса против поля `отпечаток` | подкрутить один знак отпечатка | **сошлось: 7 из 7** (`registry-prints:check`, код 0). Подкрученный знак — «не сошлось: 1, сошлось 6», код 1. CI зовёт работой `registry-resolution` |
+| отказ назван, а не проглочен | четыре запроса из таблицы §5 | снять причину из текста отказа — сторож сверяет код И текст | **сдано прибором**: четыре кода и четыре текста знак в знак; план `Forgery` краснит все 6 случаев кодом 1 |
+| замок замыкает поставленное | поставить пакет, собрать замок, собрать программу в пустом каталоге | тот же каталог без замка обязан отказать | **сдано прогоном** (задача 2031): `flang lock` над `shop.flang` — код 0, в пустом каталоге `flang check` код 0 и «файлов вместе с импортами 2», без замка — `FLANG_PACKAGE`, код 1. Сторож `lock-forms:check` держит все три формы |
 
 Первая строка — та, ради которой §5 несёт подделку. Сверка «ответ один на всех
 перестановках» без неё зеленеет и на приборе, который вовсе не читает ведомость.
 
+Корпус — два файла. `ledger.list` — своя копия ведомости в формате реестра:
+корпус отвечает одно и то же, когда ведомость примера меняют. `resolution.cases`
+— случаи, по строке «ключ = значение» на поле, значение режется по первому
+«=». Случай начинается ключом `случай` (имя, которым его называет сторож) и
+кончается перед следующим `случай`. `род` — `выбор` или `отказ`; `нужды` —
+запрос, как его пишут в `request.needs`; `строчка` — лишняя строка ведомости
+для случаев порчи самой ведомости; `ответ` — одна выбранная запись «имя версия
+адрес», строк столько, сколько пакетов в ответе, и порядок строк значим; `код`
+и `причина` — код и текст отказа, знак в знак. Пути поручений `flang io` считает
+от каталога плана, поэтому сторож называет корпус путём от своего каталога.
+
 ## 8. ADR-0012 не задет — и вот чем это снято
 
 Запрет, который легко спутать с этим решением, лежит **не в ADR-0012.**