Два слова контракта конкурентности уже были именами: «начальное» и «порог»

Шаг 1 модели конкурентности: поверхность, проверки, планировщик эталона.

Слова из контракта проверялись `grep -rn` по .flang и .fts до того, как стать
ключевыми, — и два не прошли. «начальное» — переменная в flang/core/lexer.flang,
четыре места; «порог» — параметр в flang/stdlib/optional.flang. Ключевое слово
запрещает одноимённую переменную, значит завести их значило бы сломать файлы, к
конкурентности отношения не имеющие. Ровно это уже случилось со «символами».
Поэтому начальное состояние называется занятым `начинает с`, а порог — формой из
двух частей `порог отказов`; «витков», «за» и «миллисекунд» не заняты вовсе —
парсер пропускает их как слова-пояснения.

Проверки: обработчик обязан принимать объявленные состояние и сообщение и
возвращать отклик; адресат `отправить` обязан быть объявленным процессом, а груз
— того типа, который адресат объявил в `принимает`; нетотальный обработчик без
запаса витков — ошибка, а не предупреждение.

Планировщик эталона: очередь готовых, ящики, виртуальное время, семя. Семя
решает ровно одно — выбор процесса из готовых; всё остальное определено. Отсюда
«одно семя — один журнал доставок, побайтово», и это проверяется повторным
прогоном после повторного разбора исходника, а не на глаз.

Зависаний нет ни в одном случае: тишина даёт «покой», исчерпание запаса —
FLANG_BUDGET_EXHAUSTED и остановленный процесс, бесконечная работа — «предел
пробегов».

Что из контракта не влезло и записано в SPEC: `породить` не сделан вовсе
(описанное действие не может вернуть имя), `продолжить` сделан без поля (отклик
уже несёт состояние, второе поле было бы вторым источником правды), надзор
разбирается и проверяется, но стратегий не применяет, адресат обязан быть
литералом.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01P6ehGNnEcrkCK1V5iMHNYi

Author: Marat Zimnurov

flang/SPEC.md

@@ -234,6 +234,29 @@ Pattern := { "kind": "empty" }                                  пустой с
 
 У каждого узла — необязательное `span` (`{line, column}`) для диагностик.
 
+### Конкурентность
+
+Контракт модели — `flang/conc/SPEC.md`. В AST она добавляет три необязательных
+списка верхнего уровня; появляются они только там, где соответствующие
+объявления в файле есть, — как `morphisms` и `legacy`.
+
+```jsonc
+"processes":   [{ "kind": "process", "name": "Счётчик", "state": "Счёт",
+                  "initial": "пустой счёт", "accepts": "Команда счёта",
+                  "handler": "шаг счёта", "budget": 100000 | null }],
+"supervisors": [{ "kind": "supervisor", "name": "Учёт",
+                  "watch": [{ "process": "Счётчик", "strategy": "перезапустить" }],
+                  "threshold": { "failures": 3, "window": 5000,
+                                 "otherwise": "передать выше" } | null }],
+"runs":        [{ "kind": "run", "name": "…", "seed": 4172,
+                  "inbox":    [{ "process": "Счётчик", "message": … }],
+                  "expected": [{ "process": "Счётчик", "state": … }] }]
+```
+
+Программе с процессами парсер приписывает сумму `«Действие»` — словарь языка, а
+не объявление пользователя (`flang/src/conc.mjs`). Поэтому у такой программы в
+`types` есть тип, которого нет в исходнике.
+
 ### Постусловия функции
 
 Свойства утилиты FTS («результат не больше 20 процентов от поля сумма») — это
@@ -277,6 +300,7 @@ flang/
     types.mjs        проверка типов, вывод типов, исчерпывающность разбора
     totality.mjs     анализ структурного убывания
     interpret.mjs    вычисление AST
+    conc.mjs         конкурентность: словарь действий и планировщик эталона
     builtins.mjs     строки, списки, числа
     factcheck.mjs    встраиваемый режим: утверждения о данных
     emit/js.mjs      печать в JavaScript
@@ -302,6 +326,10 @@ flang/
 | `FLANG_NOT_TOTAL` | `тотальная` без доказуемого убывания |
 | `FLANG_RECURSION_LIMIT` | обычная функция исчерпала лимит вызовов |
 | `FLANG_BUILTIN_ARGS` | неверные аргументы встроенной формы |
+| `FLANG_PROCESS` | объявление процесса, надзора или прогона не той формы |
+| `FLANG_UNKNOWN_PROCESS` | адресат `отправить`, поднадзорный или получатель в прогоне не объявлен |
+| `FLANG_HANDLER_NOT_TOTAL` | нетотальный обработчик процесса без запаса витков |
+| `FLANG_BUDGET_EXHAUSTED` | запас витков обработчика исчерпан во время прогона |
 
 ## 8. Встраиваемый факт-чекинг
 

flang/conc/SPEC.md

@@ -0,0 +1,64 @@
+// Запас витков: исчерпание — определённый исход, а не зависание.
+//
+// Обработчик здесь НЕ тотальный: завершение его не доказано, и доказать нечем —
+// «крутить» уходит вниз по числу, а число анализ завершаемости частью значения
+// не считает. Поэтому язык требует назвать запас; без строки «с запасом» эта
+// программа не собирается, и это ошибка проверки, а не предупреждение.
+//
+// Что происходит при исчерпании: сообщение отвергается, процесс падает,
+// состояние остаётся тем, каким было ДО пробега (обработчик чист, поэтому
+// половины изменения не бывает). Дальше решал бы надзор — в шаге 1 его нет,
+// поэтому процесс остаётся остановленным, и прогон это фиксирует.
+
+модуль «Разбор пакетов»
+
+объект «Разбор»
+  «сделано»: число
+
+тип «Пакет»
+  вариант «короткий» содержит «длина»: число
+  вариант «бесконечный»
+
+объект «Отклик разбора»
+  «состояние»: «Разбор»
+  «действия»: список «Действие»
+
+процесс «Разборщик»
+  состояние «Разбор»
+  начинает с «ничего не разобрано»
+  принимает «Пакет»
+  обрабатывает «разобрать пакет» с запасом 2000 витков
+
+тотальная функция «ничего не разобрано»
+  возвращает «Разбор»
+  запись «Разбор» с «сделано» равным 0
+
+// Обычная функция: на отрицательном входе не завершается вовсе. Ровно поэтому
+// она и стоит здесь — исчерпание запаса надо на чём-то показать.
+функция «крутить»
+  принимает сколько: число
+  возвращает число
+  если сколько равен 0
+    то 0
+    иначе «крутить» от (сколько минус 1)
+
+функция «разобрать пакет»
+  принимает разобрано: «Разбор», сообщение: «Пакет»
+  возвращает «Отклик разбора»
+  разбор сообщение
+    случай вариант «короткий» с «длина» как длина
+      пусть потрачено равно «крутить» от длина
+      пусть новое равно (запись «Разбор» с «сделано» равным (разобрано.«сделано» плюс 1 плюс потрачено))
+      запись «Отклик разбора» с «состояние» равным новое и «действия» равным []
+    случай вариант «бесконечный»
+      пусть напрасно равно «крутить» от -1
+      пусть новое равно (запись «Разбор» с «сделано» равным (разобрано.«сделано» плюс напрасно))
+      запись «Отклик разбора» с «состояние» равным новое и «действия» равным []
+
+// Первый пакет по силам, второй — нет. Итог определён: «сделано» равно 1, и
+// это состояние после первого сообщения. Второе не изменило ничего.
+прогон «посильный пакет, потом непосильный»
+  семя 1
+  дано «Разборщик» принимает (вариант «короткий» с «длина» равным 5)
+  дано «Разборщик» принимает (вариант «бесконечный»)
+  ожидается «Разборщик» равен (запись «Разбор» с «сделано» равным 1)

flang/conc/examples/budget.flang

@@ -0,0 +1,112 @@
+// Счётчик и журнал: два процесса, которые разговаривают друг с другом.
+//
+// Самый маленький пример, на котором видно всё, ради чего затевалась модель:
+// состояние принадлежит одному процессу, обработчик чист и возвращает «новое
+// состояние плюс список действий», а действие «отправить» описывается, а не
+// выполняется — исполняет его планировщик.
+//
+// Оба обработчика тотальны, поэтому запас витков им не нужен: про них доказано,
+// что они завершатся, и отсчитывать планировщику нечего.
+
+модуль «Счётчик и журнал»
+
+объект «Счёт»
+  «всего»: число
+
+объект «Записи»
+  «строки»: список строки
+
+тип «Команда счёта»
+  вариант «прибавить» содержит «сколько»: число
+  вариант «доложить» содержит «повод»: строка
+
+тип «Команда журнала»
+  вариант «записать» содержит «текст»: строка
+
+// Отклик — запись из нового состояния и списка действий. Имена полей
+// («состояние», «действия») — часть контракта модели, а не соглашение файла:
+// по ним планировщик и находит, что процесс решил.
+объект «Отклик счёта»
+  «состояние»: «Счёт»
+  «действия»: список «Действие»
+
+объект «Отклик журнала»
+  «состояние»: «Записи»
+  «действия»: список «Действие»
+
+процесс «Счётчик»
+  состояние «Счёт»
+  начинает с «пустой счёт»
+  принимает «Команда счёта»
+  обрабатывает «шаг счёта»
+
+процесс «Журнал»
+  состояние «Записи»
+  начинает с «пустой журнал»
+  принимает «Команда журнала»
+  обрабатывает «шаг журнала»
+
+// Надзор объявляется данными. В шаге 1 он разбирается и проверяется, но
+// планировщик эталона стратегий ещё не применяет — см. flang/conc/SPEC.md.
+надзор «Учёт»
+  процесс «Счётчик» стратегия «перезапустить»
+  процесс «Журнал» стратегия «остановить»
+  порог отказов 3 за 5000 миллисекунд иначе «передать выше»
+
+тотальная функция «пустой счёт»
+  возвращает «Счёт»
+  запись «Счёт» с «всего» равным 0
+
+тотальная функция «пустой журнал»
+  возвращает «Записи»
+  запись «Записи» с «строки» равным пустой список
+
+// Обработчик — обычная функция языка: чистая, тотальная, проверяемая примерами.
+тотальная функция «шаг счёта»
+  принимает текущее: «Счёт», сообщение: «Команда счёта»
+  возвращает «Отклик счёта»
+  пример «прибавление меняет состояние и ничего не шлёт»
+    дано текущее равно (запись «Счёт» с «всего» равным 1)
+    дано сообщение равно (вариант «прибавить» с «сколько» равным 2)
+    ожидается (запись «Отклик счёта» с «состояние» равным (запись «Счёт» с «всего» равным 3) и «действия» равным [])
+  разбор сообщение
+    случай вариант «прибавить» с «сколько» как сколько
+      пусть новое равно (запись «Счёт» с «всего» равным (текущее.«всего» плюс сколько))
+      запись «Отклик счёта» с «состояние» равным новое и «действия» равным []
+    случай вариант «доложить» с «повод» как повод
+      пусть строчка равно (соединить повод с (к строке текущее.«всего»))
+      пусть доклад равно (вариант «отправить» с «кому» равным "Журнал" и «что» равным (вариант «записать» с «текст» равным строчка))
+      запись «Отклик счёта» с «состояние» равным текущее и «действия» равным [доклад]
+
+тотальная функция «шаг журнала»
+  принимает записанное: «Записи», сообщение: «Команда журнала»
+  возвращает «Отклик журнала»
+  пример «строка копится»
+    дано записанное равно (запись «Записи» с «строки» равным [])
+    дано сообщение равно (вариант «записать» с «текст» равным "итог: 3")
+    ожидается (запись «Отклик журнала» с «состояние» равным (запись «Записи» с «строки» равным ["итог: 3"]) и «действия» равным [])
+  разбор сообщение
+    случай вариант «записать» с «текст» как строчка
+      пусть новое равно (запись «Записи» с «строки» равным (добавить строчка к записанное.«строки»))
+      запись «Отклик журнала» с «состояние» равным новое и «действия» равным []
+
+// Пример конкурентной программы — это семя, входные сообщения и ожидаемый итог.
+// Итог здесь от чередования не зависит: сложение коммутативно, а доклад приходит
+// после прибавлений, потому что все три сообщения лежат в одном ящике и
+// разбираются по очереди. Программа, итог которой зависел бы от чередования,
+// была бы неверна — и это её свойство, а не недостаток проверки.
+прогон «два прибавления и доклад»
+  семя 4172
+  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
+  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
+  дано «Счётчик» принимает (вариант «доложить» с «повод» равным "итог: ")
+  ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)
+  ожидается «Журнал» равен (запись «Записи» с «строки» равным ["итог: 5"])
+
+прогон «то же самое на другом семени»
+  семя 99
+  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
+  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
+  дано «Счётчик» принимает (вариант «доложить» с «повод» равным "итог: ")
+  ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)
+  ожидается «Журнал» равен (запись «Записи» с «строки» равным ["итог: 5"])