digitable-lol · the-homeless-god · Oct 1, 2026 · Sep 29, 2026 · Sep 29, 2026 · Sep 29, 2026
diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml
@@ -1783,6 +1783,11 @@ jobs:
           LC_ALL: C.UTF-8
           FLANG_BIN: ${{ github.workspace }}/bootstrap/flang
 
+      - name: Check user programs are replayed by the checker
+        run: cd flang/proof/probes/user-programs && ../../../../bootstrap/flang io run.fscript
+        env:
+          FLANG_TMP: ${{ runner.temp }}
+
   # ── Дорогая половина: только тег и ручной запуск ──────────────────────────
   korpus:
     name: corpus-examples

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -164,8 +164,8 @@ permissions:
 
 jobs:
   # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c`
-  # планом на flang — 1029 файл; разбор в задаче 5821.
-  # СНЯТО 2026-09-17 файлов *.flang = 1029
+  # планом на flang — 1052 файл; разбор в задаче 5821.
+  # СНЯТО 2026-09-17 файлов *.flang = 1052
   #
   # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ
   # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в

diff --git a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md b/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md
@@ -192,7 +192,7 @@ flang check --proof --строго monoid.flang
   «Е не больше Е» не теорема, почему `0 × ∞` даёт не число, почему переставлять
   через скобки нельзя. Эти доводы не украшение: на них стоят посылки правил.
 - **Независимая проверяющая программа** — `flang/proof/checker/checker.c`,
-  10015 строк. <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10015 (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
+  10122 строк. <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10122 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
   Она переигрывает записи и о новом виде значения не знает ничего.
 
 **И встречное число, которое меняет разговор о втором варианте.** Тип `целое`

diff --git a/docs/course/README.md b/docs/course/README.md
@@ -172,7 +172,7 @@ docs/course/check.flang: проверено — разбор, типы, заве
 | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `cc`/`g++` 15.2.0, go 1.26.5, rustc 1.97.1, javac 26-internal, Elixir 1.20.3 на Erlang/OTP 29, node 26.7.0, Python 3.14.4, .NET 10.0.110 |
 | 82 задачи LeetCode, десятка самых коротких | `ls`, `wc -l`, счёт строк `пример` |
 | 51 файлов и 32 074 строки библиотеки <!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 --><!-- СНЯТО 2026-09-13 строк-в flang/stdlib/*.flang = 32074 --> | `ls flang/stdlib/*.flang`, `cat … \| wc -l` |
-| 724 заметки, 238 примеров, 361 файл доказательств <!-- СНЯТО 2026-09-17 файлов docs/zettel/*.md = 724 --><!-- СНЯТО 2026-09-17 файлов docs/examples/*.flang = 238 --><!-- СНЯТО 2026-09-17 файлов flang/proof/*.flang = 361 (задача 5502: проба пустой ведомости flang/proof/probes/strict/programs/no-obligations.flang; до неё 320, снято 2026-09-17) --> | `ls`, `find` |
+| 724 заметки, 238 примеров, 384 файл доказательств <!-- СНЯТО 2026-09-17 файлов docs/zettel/*.md = 724 --><!-- СНЯТО 2026-09-17 файлов docs/examples/*.flang = 238 --><!-- СНЯТО 2026-09-17 файлов flang/proof/*.flang = 384 (задача 5502: проба пустой ведомости flang/proof/probes/strict/programs/no-obligations.flang; до неё 320, снято 2026-09-17) --> | `ls`, `find` |
 | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа |
 
 **Чего переснять не удалось, и это надо знать.**

diff --git a/docs/design/nositel-tochnogo-celogo.md b/docs/design/nositel-tochnogo-celogo.md
@@ -441,7 +441,7 @@ flang check n-zapis-v-chislo.flang
    первая правка, и назвать её сейчас, не написав, значило бы выдумать.
 2. **Цену принуждения канона.** Сколько стоит запретить литерал-список в позиции нового
    типа — не мерил: это решение задачи 1412, а не замер.
-3. **Цену для проверяющей программы.** `checker.c` (10015 строк) <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10015 (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
+3. **Цену для проверяющей программы.** `checker.c` (10122 строк) <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10122 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
    о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по
    образцу ADR-0029. Это оценка, и моя записка её не улучшает.
 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ.

diff --git a/docs/site/index.md b/docs/site/index.md
@@ -143,7 +143,7 @@ recounted on every push by `sh scripts/guards/published-vs-tree.sh --числа`
 steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then …
 by property …), `индукция по …` (induction on …), `следовательно доказано`
 (hence proved). It reads like a proof in Isabelle's Isar, not like a script of
-tactics. There are **287** such theorems in the repository, 55 of them in the
+tactics. There are **288** such theorems in the repository, 55 of them in the
 standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`, summed
 with `awk`).
 

diff --git a/docs/site/index.ru.md b/docs/site/index.ru.md
@@ -141,7 +141,7 @@ bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000
 **Доказательство руками можно писать и здесь.** `теорема` пишется по шагам:
 `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`,
 `следовательно доказано`. Это читается как доказательство на Isar из Isabelle, а
-не как скрипт из тактик. Таких теорем в дереве языка **287**, из них **55** в
+не как скрипт из тактик. Таких теорем в дереве языка **288**, из них **55** в
 стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`,
 сумма по `awk`).
 

diff --git a/docs/site/proofs.md b/docs/site/proofs.md
@@ -66,7 +66,7 @@ proof by hand**, as in Coq or Isabelle. A `теорема` (theorem) is written
 steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then
 … by property …), `индукция по …` (induction on …), `следовательно доказано`
 (hence proved). It reads like Isar in Isabelle, and the prover checks each step;
-it searches for nothing. There are 287 such theorems in the repository, 55 of
+it searches for nothing. There are 288 such theorems in the repository, 55 of
 them in the standard library (`grep -rac '^\s*теорема ' flang
 --include='*.flang'`). Most postconditions need no theorem: the proof report
 shows, as a separate number, how many were proved **without a written proof**.

diff --git a/docs/site/proofs.ru.md b/docs/site/proofs.ru.md
@@ -64,7 +64,7 @@
 руками**, как в Coq или Isabelle. `теорема` пишется по шагам: `дано`,
 `утверждаем`, `затем … по свойству «…»`, `индукция по …`, `следовательно
 доказано`. Это читается как Isar в Isabelle, и prover проверяет каждый шаг,
-ничего не ища. В дереве языка таких теорем 287, из них 55 в стандартной
+ничего не ища. В дереве языка таких теорем 288, из них 55 в стандартной
 библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`). Большинству
 постусловий теорема не нужна: отчёт о доказательствах показывает отдельным
 числом, сколько доказано **без написанного доказательства**.