Executable specifications in flang Generation and CI: code that does not drift from the rule
Русский
 0%

Generation and CI: code that does not drift from the rule

9 min 1805 words
#flang#code generation#ci#typescript#github actions

Generation and CI: code that does not drift from the rule

This chapter shows what flang emit prints, why --check mode catches a rule edited behind the model’s back, and how to order the CI steps so that a cheap check fails before an expensive one.

Minimal example

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Очень крупная покупка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «за очень крупную покупку не больше потолка» результат не больше 15000
  пример «сто тысяч — ещё не очень крупная»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным нет
    ожидается 0
  если покупка.«сумма» больше 100000
    то 15000
    иначе 0

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка ограничена» результат не больше 15000
  пример «большая покупка постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным да
    ожидается 3000
  пример «очень крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 200000 и «постоянный клиент» равным нет
    ожидается 15000
  если покупка.«сумма» больше 100000
    то «Очень крупная покупка» от покупка
    иначе если покупка.«постоянный клиент»
      то (покупка.«сумма» умножить на 15) делить на 100
      иначе (покупка.«сумма» умножить на 10) делить на 100

Two functions, two promises. The proof report (flang check --proof) says different things about them:

  постусловие «за очень крупную покупку не больше потолка» функции «Очень крупная покупка» — доказано сведением цели с телом функции: правило «ограниченность точным потолком по построению», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 2 значения (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

The first promise is proved for all inputs. The compiler checked the second one only on the two values from the examples — that is what the report calls a “grid” (сетка): the proof kernel does not bound a percentage of the amount. Below you will see what this changes in the printed code.

What the compiler does

flang emit prints a checked program into one of ten languages: c, cpp, go, rust, java, js, ts, elixir, python, csharp. Printing is preceded by the same check as flang check: parsing, types, termination and the proof kernel. A program with a type error is not printed at all.

flang emit order-discount.flang --target ts --out generated

проверок при работе снято 1: постусловие доказано ядром обо всех входах и
проверено примерами функции — в напечатанный код оно не едет.
напечатано файлов 5, байт 54350, в generated
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>

Two lines of this output matter more than the rest.

A proved promise does not travel into the code. If the kernel proved a promise for all inputs and the function has an example, there is no point in checking it on every call. For the model above the printed JavaScript looks like this:

export function ochenKrupnayaPokupka(pokupka) {
  if ($cond($gt($field(pokupka, "сумма"), 100000))) {
    return 15000;
  } else {
    return 0;
  }
}
export function rasschitatSkidku(pokupka) {
  let $t1;
  if ($cond($gt($field(pokupka, "сумма"), 100000))) {
    $t1 = ochenKrupnayaPokupka(pokupka);
  } else {
    let $t2;
    if ($cond($field(pokupka, "постоянный клиент"))) {
      $t2 = $div($mul($field(pokupka, "сумма"), 15), 100);
    } else {
      $t2 = $div($mul($field(pokupka, "сумма"), 10), 100);
    }
    $t1 = $t2;
  }
  // постусловие «скидка ограничена»
  if (!$post($lte($t1, 15000), "скидка ограничена", "Рассчитать скидку")) {
    $fail(
      "FLANG_PROPERTY",
      "нарушено свойство «скидка ограничена» функции «Рассчитать скидку»",
      { line: 21, column: 3 },
    );
  }
  return $t1;
}

The first function has no check: its promise is proved. The second keeps a runtime check: its promise rests on examples only, and the printed code will stop with an error coded FLANG_PROPERTY if the rule ever returns more than the cap. There will be no silently wrong number.

Printing does not run the examples. On a model with a failing example flang emit writes the files and exits with code 0. That is why flang test runs as a separate step before printing — both in the generation script and in CI.

Function names in the printed code are transliterated (rasschitatSkidku), and the mapping to the model’s names lives in the module itself: $PROGRAM.functions is a table from the flang name to the function. The course tests call functions through it: functions.get('Рассчитать скидку').

--check mode and how drift is caught

examples/spec/typescript-codegen/generate.mjs wraps printing in writeGenerated. The script first runs flang test, then flang emit --target ts. In --check mode it writes nothing and compares the printed output with what is in generated/:

node examples/spec/typescript-codegen/generate.mjs           # записать generated/
node examples/spec/typescript-codegen/generate.mjs --check   # сверить с моделью

If someone edits return 15000 directly in the .ts file instead of the model, --check sees the mismatch and exits with code 1:

Напечатанный код отстал от модели: program.ts
Запустите: node examples/spec/typescript-codegen/generate.mjs

generate.test.mjs checks this in a dedicated test: it prints the module into a temporary directory, overwrites program.ts with the line // правка мимо модели and expects stale: ['program.ts']. A second test guards against the opposite mistake — printing a model that fails its own examples. Replace the expectation 3000 with 4200, and the script stops before printing:

модель не проходит свои примеры:
/model.flang: примеров 10, прошло 8, не прошло 2
пример «большая покупка постоянного клиента» функции «Рассчитать скидку» не прошёл: значение не совпало с ожидаемым: ожидалось 4200, получено 3000

A third test imports the committed program.ts — Node 23.6 and later reads TypeScript by itself — and compares its answers with the model’s examples. Printed code that computes something other than the model fails this test.

Byte-for-byte comparison works because printing is deterministic: the native flang binary and the WebAssembly build print the same module, and --check gives the same answer with either of them.

Order of CI steps and what fails first

A ready workflow lives in examples/spec/ci/flang-check.yml (it goes into .github/workflows/flang-check.yml):

- run: npm ci
- name: Поставить flang
  run: |
    curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh \
      | PREFIX="$RUNNER_TEMP/flang" sh
    echo "$RUNNER_TEMP/flang/bin" >> "$GITHUB_PATH"
    echo "FLANG_BIN=$RUNNER_TEMP/flang/bin/flang" >> "$GITHUB_ENV"    
- name: Проверить модели
  run: |
    for model in static/spec/models/*.flang; do
      flang check "$model" --proof || [ $? -eq 3 ]
    done    
- name: Выполнить предметные примеры
  run: flang test static/spec/models/
- name: Сверить напечатанный код
  run: node examples/spec/typescript-codegen/generate.mjs --check
- name: Тесты интеграций
  run: npm run spec:examples

The compiler version is pinned by the variable FLANG_VERSION: 0.7.29 at the workflow level: install.sh reads it and verifies the archive against the release checksums. Upgrading the compiler is a separate change, not a surprise inside someone else’s pull request.

The order is not accidental — each step is cheaper and more precise than the next one:

  1. flang check --proof — parsing, types, termination and the proof report. A typo in a field name fails here in a fraction of a second. Code 1 is an error and the step turns red. Code 3 means “checked, but some promises rest on examples only”; the step lets it pass, and the report stays in the log.
  2. flang test — domain examples: the rule compiled but returns the wrong number. A whole directory is checked with one command: flang test static/spec/models/.
  3. generate.mjs --check — drift between the model and the committed TypeScript. The model is already correct at this step; a failure means someone forgot to reprint after editing the model.
  4. npm run spec:examples — integrations: the HTTP service, shipment admission, the form, equivalence tests. The most expensive layer, furthest from the model, fails last.

Code 3 is the team’s decision. flang check without --proof says nothing about proofs and exits with zero. With --proof, code 3 separates “proved” from “checked on examples”. The --strict key separates outcomes more strictly: 0 — everything proved, 3 — something rests on examples, 1 — refuted. For a model with a percentage discount --strict always gives 3, so the workflow does not use it. If your rules are proved completely, add --strict and remove || [ $? -eq 3 ].

Agent work

flang ships a service for an AI assistant — flang --mcp-mode, JSON-RPC over the standard streams. It offers two tools: flang_check (check a program and return the proof report) and flang_prove (what proves one named promise). Printing is not among them.

That is a convenient boundary. The agent edits the model and immediately sees three separate verdicts: proved, “grid N” and “stated, not proved” — the answer has no green “ok” tick. Printing code, writing files and committing remain a separate step carried out by a person or a pipeline with flang emit and generate.mjs.

Practice in the sandbox

The sandbox checks the model with the same compiler and shows which promises are proved. Change the cap of the very-large-purchase function from 15000 to 16000 and watch the proved promise turn into an error. Then restore 15000 and change an expectation in an example — this is what a broken example looks like, the kind flang emit alone would let through.

Common mistakes

  • FLANG_EXAMPLE — an example failed. flang check and flang test exit with code 1, while flang emit prints the model as if nothing happened. Never print without flang test before it.
  • FLANG_PROPERTY — the printed function broke a promise the kernel did not prove. In CI this is a failed integration test, not a silently wrong number.
  • FLANG_TYPE — an input value of the wrong type. The runner flang_cli.js next to the printed module checks the input against the declared types before the call; a direct call of a module function from your own code does not do that check — guard the input boundary yourself (like readPurchase in examples/spec/discount-api/server.mjs).

Checklist

  • The model passes flang check --proof and flang test before printing.
  • generate.mjs or your equivalent calls flang test before flang emit.
  • CI verifies the committed code with --check instead of trusting the developer to remember to reprint.
  • The flang version in CI is pinned.
  • CI steps go from the cheap check to the expensive integrations.
  • The decision about code 3 is written into the workflow explicitly: let it pass or require --strict.
  • A pull request that edits the model shows a small readable diff of the model, not only a large diff of the printed file.

Catalogue cases on this topic

Next: performance

Spotted a mistake? Select a fragment of the text — a bug icon will appear next to it.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов
Next