Pipeline and visualization: one run and a model diagram

CI and a conversation with an agent need one answer to the question “is the model ready”: one command, one JSON, one exit code. A person needs a different answer — a picture that shows within a minute which types the model has and which transitions between them are declared. This chapter covers both: flang check --proof --json as the single run, and a small script that turns the parsed program (flang ast) into a mermaid diagram.

flang 0.7.29 has no separate “pipeline” command and no separate “draw” command: flang --help lists fifteen commands, and neither is among them. Both tasks are solved with what already exists.

Minimal example

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

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

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

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

This is static/spec/models/credit-limit.flang: scoring opens the risk check, and the risk check together with risk approval allows the limit. The model is small, but it holds everything a diagram needs to show: a record, two functions, a call from one to the other and four promises.

What the compiler does

flang check parses the module, checks the types of fields and arguments, proves that both functions terminate and runs the three examples. With --proof it also judges every promise. Here all four are proved for any input, not only for the written ones:

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

The promise «без скоринга лимита нет» (no limit without scoring) sits on a function that does not read the scoring field itself: it arrives through the call to «Риск-проверка разрешена». The kernel substitutes the call and proves the promise without a theorem.

One run instead of four commands

Parsing, types, termination, examples and proofs are one command:

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

The proof report arrives on stdout as one JSON, the verdict in the exit code. The top-level keys of the report: functions (how termination of each function is proved), claims (each promise with the verdict proved, grid, declared or violated), obligations (the proof goals themselves), laws, assumed and totals with the counts. The human-readable output goes to stderr, so the JSON can be parsed without filters.

The exit codes are the answer for CI:

The practical difference from a chain of separate steps is in how it fails:

• One point of failure. A parse or type error stops the run with code 1 and the same message as plain flang check. There is no need to write a chain of four commands in CI and check the code after each one.
• One JSON for CI. The report is saved whole as a build artifact and is parsed with a single JSON.parse call.
• One answer for the agent. flang --mcp-mode starts a service for an AI assistant with two tools: flang_check (the whole check and the full report) and flang_prove (what proves one named promise). The three verdicts — “proved”, “grid” and “stated, not proved” — come back separately, and there is no “ok” field in the answer.

What this run does not do: flang check prints no code and writes no TypeScript. Printing is a separate command, flang emit, and it, in turn, does not run the examples: in CI flang test stands before it. This is one of the typical mistakes below.

Category diagram

The diagram is built from the parsed program rather than drawn by hand, so it is exactly as accurate as the model. flang ast prints the program as JSON: types (records with fields, types with variants), functions (parameters, result type, examples, postconditions) and morphisms, if arrows of the categorical surface are declared. The script below is twenty lines with no dependencies:

// 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'));

The output of flang ast static/spec/models/order-shipment.flang | node ast-to-mermaid.mjs:

The question this picture answers: “which types does the model have and which functions are declared between them” — without reading the file line by line. A record node shows all fields, a node of a type with variants shows all variants, an arrow goes from the argument type to the result type. The arrow label tells at once how many promises and examples the function has: a function without a single promise stands out at first glance. Change a field, and the node label changes on the next run.

Diagram of morphisms and proof

If transitions between states are written as arrows of the categorical surface, flang ast returns them in morphisms, and the script draws them as bold arrows:

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

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

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

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

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

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

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

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

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

The question of this diagram is “in which order are the transitions applied”. In the JSON the chain is stored as a composition: left is «риск-проверка разрешает лимит», right is «скоринг открывает риск-проверку», that is, right to left, as in mathematics. Two explicit arrows remove the ambiguity faster than reading a pair of fields.

This form has a price, and the compiler names it itself. flang check on such a file (saved here as chain.flang) exits with code 2:

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

Types, arrow ends and functions are checked; the laws of the category are not. That is why the course models write transitions as ordinary functions with implication promises, as in credit-limit.flang: the kernel proves such promises.

The third diagram is built not from the model but from the proof report. The approach is the same, the input is different:

// 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'));

On the discount model order-discount.flang (exit code 3) it shows which promise is proved and which is checked only on examples:

“Grid” (сетка) means “checked on the function’s examples, no proof”. In the picture this is visible at once, while in the report text it is easy to miss.

The question “on what grounds did the system refuse on this particular data” is answered not by a diagram but by flang facts. It evaluates a claim on a data snapshot and returns the evaluation steps:

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": ["разбор", "тотальность", "факт", "факт", "вычисление", "сравнение"]

Exit code 1 here means “the claim is refuted”, not “something broke”. The same chain is easy to draw as a picture from the steps, but the answer is already in the why field: the warehouse did not confirm the order.

Who should see the diagram, and when

• The analyst — the diagram of types and functions, before code review. It is checked by eye within a minute: do the node names match the words of the task, is there a transition the analyst considered obvious that got lost. Reading the model file is not required for this.
• A new developer — the same diagram on first contact with the model. One graph shows the boundaries: which records exist, which functions are declared between them, and which similar functions the model does not have at all.
• Whoever takes the model into work — the diagram of promises. It answers the question “what is proved here and what rests on examples”.
• During an incident review — the flang facts verdict on the data snapshot of that moment. It is the only one of these answers that says not “what is possible in general” but “what exactly happened on this data”.

Practice in the sandbox

1. The sandbox checks the model right away and shows the report: four promises are proved. Replace the body of «Лимит может быть установлен» with the single line заявка.«риски одобрили» and check again. Two promises become “grid 2 values”: the examples still match, but the kernel no longer claims anything for all inputs. The promise «без скоринга лимита нет» is now simply false — an application without scoring but with risk approval gets a limit — and only an example can catch such an input.
2. The sandbox draws no diagrams. Copy both scripts from the chapter into files and run them locally on credit-limit.flang and order-discount.flang. Paste the output into any mermaid viewer and compare it with the model text.
3. Add the promise результат равен заявка.«риски одобрили» to «Риск-проверка разрешена». The example «скоринг пройден» violates it, and the check stops with FLANG_PROPERTY and code 1: an example that lands on a violation turns red even when the kernel does not prove the promise.

Common mistakes

• Expecting flang check to print code. Checking and printing are different commands: flang check --proof judges the model, flang emit prints it into the target language. Printing checks the program before it prints, but does not run the examples — in CI flang test stands before it.
• Checking in CI without --proof. Plain flang check does not ask about proofs and exits with code 0 on a model with unproved promises. Only --proof answers “everything is proved”, and only --proof --strict tells “proved” from “grid” by the exit code.
• Treating code 3 as green. Code 3 means “checked, but not everything is proved”. A CI step that accepts any code other than 1 turns “not proved” into “proved”.
• Treating code 2 as a detail. Code 2 says the program contains constructs the binary does not judge — for example, the laws of the categorical surface. Types and examples are checked; the laws are not.
• Drawing the diagram by hand. A hand-drawn chart drifts away from the model after the first field edit. A diagram from flang ast cannot drift: a run prints it.

Checklist

• CI and the agent use one run of flang check --proof --json, not a chain of separate steps.
• It is known that flang check prints no code and flang emit runs no examples: flang test and flang emit stand in the pipeline separately.
• Codes 2 and 3 do not count as success in CI.
• The diagram of types and functions is built from flang ast and shown to the analyst before code review.
• The diagram of promises shows what is proved and what rests on examples.
• During an incident review the verdict comes from flang facts on the data snapshot, not from a general chart of the model.

Catalogue cases on this topic