Конвейер и визуализация: один прогон и диаграмма модели

В CI и в разговоре с агентом нужен один ответ на вопрос «готова ли модель»: одна команда, один JSON, один код возврата. Человеку нужен другой ответ — картинка, по которой за минуту видно, какие типы есть в модели и какие переходы между ними объявлены. Эта глава про оба: flang check --proof --json как единственный прогон и маленький скрипт, который превращает разобранную программу (flang ast) в mermaid-диаграмму.

Отдельной команды «конвейер» и отдельной команды «нарисовать» во flang 0.7.29 нет: в flang --help их нет среди пятнадцати команд. Обе задачи решаются тем, что уже есть.

Минимальный пример

модуль «Кредитная политика»

объект «Заявка на лимит»
  «номер»: строка
  «клиент»: строка
  «сумма»: неотрицательное
  «скоринг пройден»: признак
  «риски одобрили»: признак

тотальная функция «Риск-проверка разрешена»
  принимает заявка: «Заявка на лимит»
  возвращает признак
  обеспечивает «без скоринга риск-проверки нет» если не заявка.«скоринг пройден» то результат равен нет иначе да
  пример «скоринг пройден»
    дано заявка равно запись «Заявка на лимит» с «номер» равным "ЛМ-205" и «клиент» равным "АО Горизонт" и «сумма» равным 1000000 и «скоринг пройден» равным да и «риски одобрили» равным нет
    ожидается да
  заявка.«скоринг пройден»

тотальная функция «Лимит может быть установлен»
  принимает заявка: «Заявка на лимит»
  возвращает признак
  обеспечивает «лимит только после риск-проверки» если не («Риск-проверка разрешена» от заявка) то результат равен нет иначе да
  обеспечивает «без скоринга лимита нет» если не заявка.«скоринг пройден» то результат равен нет иначе да
  обеспечивает «лимит только с одобрением рисков» если не заявка.«риски одобрили» то результат равен нет иначе да
  пример «ЛМ-205 прошла оба шага»
    дано заявка равно запись «Заявка на лимит» с «номер» равным "ЛМ-205" и «клиент» равным "АО Горизонт" и «сумма» равным 1000000 и «скоринг пройден» равным да и «риски одобрили» равным да
    ожидается да
  пример «без одобрения рисков лимита нет»
    дано заявка равно запись «Заявка на лимит» с «номер» равным "ЛМ-206" и «клиент» равным "АО Горизонт" и «сумма» равным 1000000 и «скоринг пройден» равным да и «риски одобрили» равным нет
    ожидается нет
  если «Риск-проверка разрешена» от заявка
    то заявка.«риски одобрили»
    иначе нет

Это static/spec/models/credit-limit.flang: скоринг открывает риск-проверку, риск-проверка вместе с одобрением рисков разрешает лимит. Модель маленькая, но в ней есть всё, что нужно показать на диаграмме: запись, две функции, вызов одной из другой и четыре обещания.

Что делает компилятор

flang check разбирает модуль, проверяет типы полей и аргументов, доказывает завершение обеих функций и прогоняет три примера. С ключом --proof он ещё и судит каждое обещание. Здесь все четыре доказаны для любых входов, а не только для написанных:

  утверждений 4: доказано 4 (из них без теоремы 4), сетка 0, объявлено, не доказано 0
static/spec/models/credit-limit.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 4: доказано 4, условно 0, сетка 0, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 0

Обещание «без скоринга лимита нет» стоит у функции, которая сама поле «скоринг пройден» не читает: оно приходит через вызов «Риск-проверка разрешена». Ядро подставляет вызов и доказывает обещание без теоремы.

Один прогон вместо четырёх команд

Разбор, типы, завершение, примеры и доказательства — это одна команда:

flang check static/spec/models/credit-limit.flang --proof --json

В stdout приходит отчёт о доказательствах одним JSON, в коде возврата — итог. Верхние ключи отчёта: functions (чем доказано завершение каждой функции), claims (каждое обещание с вердиктом proved, grid, declared или violated), obligations (сами цели доказательства), laws, assumed и totals со счётом. Человеческий вывод уходит в stderr, поэтому JSON можно разбирать без фильтров.

Коды возврата и есть ответ для CI:

Практическая разница с цепочкой отдельных шагов — в форме отказа:

• Одна точка отказа. Ошибка разбора или типа останавливает прогон с кодом 1 и тем же сообщением, что и голая flang check. Писать в CI цепочку из четырёх команд с проверкой кода после каждой не нужно.
• Один JSON для CI. Отчёт сохраняется как артефакт сборки целиком и разбирается одним вызовом JSON.parse.
• Один ответ для агента. flang --mcp-mode поднимает службу для ИИ-помощника с двумя средствами: flang_check (вся проверка и отчёт целиком) и flang_prove (чем доказано одно названное обещание). Три вердикта — «доказано», «сетка» и «объявлено, не доказано» — служба отдаёт порознь, поля «ок» в ответе нет.

Чего в этом прогоне нет: flang check не печатает код и не пишет TypeScript. Печать — отдельная команда flang emit, и она, наоборот, примеров не прогоняет: перед печатью в CI стоит flang test. Это одна из типичных ошибок ниже.

Диаграмма категории

Диаграмму строят из разобранной программы, а не рисуют руками, поэтому она точна ровно настолько, насколько точна модель. flang ast печатает программу JSON-ом: types (записи с полями, типы с вариантами), functions (параметры, тип результата, examples, postconditions) и morphisms, если объявлены стрелки категорной поверхности. Скрипт ниже — двадцать строк без зависимостей:

// flang ast модель.flang | node ast-to-mermaid.mjs
const ast = JSON.parse(await new Response(process.stdin).text());
const word = { flag: 'признак', string: 'строка', number: 'число' };
const name = (t) => t.kind === 'named' ? t.name : t.kind === 'list' ? `список ${name(t.of)}` : word[t.kind] ?? t.kind;
const ids = new Map();
const id = (label) => ids.get(label) ?? (ids.set(label, `n${ids.size}`), ids.get(label));
const lines = ['flowchart LR', `  subgraph M["модуль ${ast.module}"]`];
for (const type of ast.types) {
  const parts = type.kind === 'record'
    ? type.fields.map((f) => `${f.name}: ${name(f.type)}${f.optional ? '?' : ''}`)
    : type.variants.map((v) => `вариант ${v.name}`);
  lines.push(`    ${id(type.name)}["${[type.name, ...parts].join('<br/>')}"]`);
}
for (const fn of ast.functions) {
  const to = id(name(fn.returns));
  const label = `${fn.name}<br/>обещаний ${fn.postconditions?.length ?? 0}, примеров ${fn.examples?.length ?? 0}`;
  for (const p of fn.params) lines.push(`    ${id(name(p.type))} -->|"${label}"| ${to}`);
}
for (const m of ast.morphisms ?? []) {
  if (m.kind === 'morphism') lines.push(`    ${id(m.domain)} ==>|"морфизм ${m.name}"| ${id(m.codomain)}`);
  if (m.kind === 'composition') lines.push(`    %% ${m.name}: сначала «${m.right}», затем «${m.left}»`);
}
for (const [label, key] of ids) if (!ast.types.some((t) => t.name === label)) lines.splice(2, 0, `    ${key}(["${label}"])`);
lines.push('  end');
console.log(lines.join('\n'));

Вывод flang ast static/spec/models/order-shipment.flang | node ast-to-mermaid.mjs:

Вопрос, который снимает эта картинка: «какие типы есть в модели и какие функции между ними объявлены» — без чтения файла построчно. Узел записи показывает все поля, узел типа с вариантами — все варианты, стрелка идёт от типа аргумента к типу результата. Подпись стрелки сразу говорит, сколько у функции обещаний и примеров: функция без единого обещания видна с первого взгляда. Изменили поле — подпись узла изменится при следующем прогоне.

Диаграмма морфизмов и доказательства

Если переходы между состояниями записаны стрелками категорной поверхности, flang ast отдаёт их в morphisms, а скрипт рисует их жирными стрелками:

модуль «Шаги кредита»

объект «Заявка»
  «скоринг пройден»: признак

объект «Риск-проверка»
  «разрешена»: признак

объект «Лимит»
  «можно установить»: признак

тотальная функция «Открыть риск-проверку»
  принимает заявка: «Заявка»
  возвращает «Риск-проверка»
  запись «Риск-проверка» с «разрешена» равным заявка.«скоринг пройден»

тотальная функция «Решить о лимите»
  принимает проверка: «Риск-проверка»
  возвращает «Лимит»
  запись «Лимит» с «можно установить» равным проверка.«разрешена»

морфизм «скоринг открывает риск-проверку» из «Заявка» в «Риск-проверка»
  даёт «Открыть риск-проверку»

морфизм «риск-проверка разрешает лимит» из «Риск-проверка» в «Лимит»
  даёт «Решить о лимите»

цепочка «от заявки к лимиту»
  сначала «скоринг открывает риск-проверку»
  затем «риск-проверка разрешает лимит»

Вопрос этой диаграммы — «в каком порядке применяются переходы». В JSON цепочка записана как композиция: left — «риск-проверка разрешает лимит», right — «скоринг открывает риск-проверку», то есть справа налево, как в математике. Две явные стрелки снимают двусмысленность быстрее, чем разбор пары полей.

Цена у этой формы есть, и компилятор называет её сам. flang check на таком файле (здесь он сохранён как chain.flang) выходит кодом 2:

законы категории НЕ СЧИТАЛИСЬ: стрелки объявлены, а категории нет — равенство, через которое закон только и выразим, объявляет категория
chain.flang: проверено НЕ ДО КОНЦА — разбор, типы, завершаемость, ядро и примеры прошли

Типы, концы стрелок и функции проверены, а законы категории — нет. Поэтому в моделях курса переходы записаны обычными функциями с обещаниями-импликациями, как в credit-limit.flang: такие обещания ядро доказывает.

Третья диаграмма строится не из модели, а из отчёта о доказательствах. Подход тот же, вход другой:

// flang check модель.flang --proof --json | node proof-to-mermaid.mjs
const ledger = JSON.parse(await new Response(process.stdin).text());
const words = { proved: 'доказано', grid: 'сетка', declared: 'объявлено, не доказано', violated: 'НАРУШЕНО' };
const lines = ['flowchart LR'];
const fns = [...new Set(ledger.claims.map((claim) => claim.of))];
fns.forEach((fn, i) => lines.push(`  f${i}["${fn}"]`));
ledger.claims.forEach((claim, i) => {
  const verdict = words[claim.verdict] ?? claim.verdict;
  lines.push(`  c${i}{{"${claim.name}<br/>${verdict}"}}`);
  lines.push(`  f${fns.indexOf(claim.of)} --> c${i}`);
});
console.log(lines.join('\n'));

На модели скидки order-discount.flang (код возврата 3) она показывает, какое обещание доказано, а какое проверено только на примерах:

«Сетка» значит «проверено на примерах функции, доказательства нет». На картинке это видно сразу, а в тексте отчёта легко пропустить.

Вопрос «на основании чего система отказала на конкретных данных» решает не диаграмма, а flang facts. Он вычисляет утверждение на снимке данных и отдаёт шаги вычисления:

flang facts static/spec/models/order-shipment.flang \
  --facts static/spec/models/order-shipment.blocked.facts.json \
  --claims '["«Заказ с номером отгружается» от заказы, номер равно да"]'

"holds": false,
"why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». Исходные факты — «заказы»: [{\"номер\":\"ЗК-7781\",\"клиент\":\"ООО Маяк\",\"оплачен\":true,\"склад подтвердил\":false}]; «номер»: «ЗК-7781»",
"steps": ["разбор", "тотальность", "факт", "факт", "вычисление", "сравнение"]

Код возврата 1 здесь значит «утверждение опровергнуто», а не «сломалось». Из шагов легко нарисовать ту же цепочку картинкой, но ответ уже есть в поле why: склад не подтвердил заказ.

Кому и когда показывать диаграмму

• Аналитику — диаграмму типов и функций, до код-ревью. Она проверяется глазами за минуту: совпадают ли имена узлов со словами из задачи, не потерялся ли переход, который аналитик считал очевидным. Файл модели для этого читать не обязательно.
• Новому разработчику — ту же диаграмму при первом знакомстве с моделью. Один граф показывает границы: какие записи существуют, какие функции между ними объявлены, а каких похожих функций в модели нет вовсе.
• Тому, кто принимает модель в работу, — диаграмму обещаний. Она отвечает на вопрос «что здесь доказано, а что держится на примерах».
• При разборе инцидента — вердикт flang facts на снимке данных того момента. Это единственный из ответов, который говорит не «что вообще возможно», а «что именно произошло на этих данных».

Практика в песочнице

1. Песочница сразу проверит модель и покажет отчёт: четыре обещания доказаны. Замените тело «Лимит может быть установлен» одной строкой заявка.«риски одобрили» и проверьте снова. Два обещания станут «сетка 2 значения»: примеры по-прежнему сходятся, но для всех входов ядро больше ничего не утверждает. Обещание «без скоринга лимита нет» теперь просто ложно — заявка без скоринга, но с одобрением рисков получит лимит, — и поймать такой вход может только пример.
2. Песочница диаграмм не рисует. Скопируйте оба скрипта из главы в файлы и прогоните их локально на credit-limit.flang и order-discount.flang. Вставьте вывод в любой просмотрщик mermaid и сравните с текстом модели.
3. Добавьте в «Риск-проверка разрешена» обещание результат равен заявка.«риски одобрили». Пример «скоринг пройден» его нарушит, и проверка остановится с FLANG_PROPERTY и кодом 1: пример, попавший в нарушение, краснеет, даже когда ядро обещание не доказывает.

Типичные ошибки

• Ждать от flang check печати кода. Проверка и печать — разные команды: flang check --proof судит модель, flang emit печатает её в целевой язык. Печать проверяет программу перед печатью, но примеров не прогоняет — в CI перед ней стоит flang test.
• Проверять в CI без --proof. Голая flang check о доказательствах не спрашивает и на модели с недоказанными обещаниями выходит кодом 0. Ответ «всё доказано» даёт только --proof, а различить «доказано» и «сетка» кодом — --proof --strict.
• Считать код 3 зелёным. Код 3 значит «проверено, но доказано не всё». Шаг CI, который считает успехом любой код, кроме 1, превращает «не доказано» в «доказано».
• Считать код 2 мелочью. Код 2 говорит, что в программе есть конструкции, которых двоичный не судит, — например, законы категорной поверхности. Типы и примеры при этом проверены, законы — нет.
• Рисовать диаграмму руками. Нарисованная от руки схема расходится с моделью после первой правки поля. Диаграмма из flang ast расходиться не может: её печатает прогон.

Чек-лист

• Для CI и агента используется один прогон flang check --proof --json, а не цепочка отдельных шагов.
• Известно, что flang check не печатает код, а flang emit не прогоняет примеры: в конвейере flang test и flang emit стоят отдельно.
• Коды 2 и 3 в CI не считаются успехом.
• Диаграмма типов и функций строится из flang ast и показана аналитику до код-ревью.
• Диаграмма обещаний показывает, что доказано, а что держится на примерах.
• При разборе инцидента вердикт берётся у flang facts на снимке данных, а не у общей схемы модели.

Кейсы каталога по этой теме