Исполняемые спецификации на flang Генерация и CI: код, который не расходится с правилом
English
 0%

Генерация и CI: код, который не расходится с правилом

8 мин 1584 слова
#flang#code generation#ci#typescript#github actions

Генерация и CI: код, который не расходится с правилом

Глава показывает, что печатает flang emit, почему режим --check ловит правку правила мимо модели и как выстроить шаги CI так, чтобы дешёвая проверка падала раньше дорогой.

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

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

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

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

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

Две функции, два обещания. Отчёт о доказательствах (flang check --proof) говорит о них разное:

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

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

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

flang emit печатает проверенную программу в один из десяти языков: c, cpp, go, rust, java, js, ts, elixir, python, csharp. Перед печатью идёт та же проверка, что у flang check: разбор, типы, завершение и ядро доказательств. Программа с ошибкой типов не печатается вовсе.

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

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

Две строки из этого вывода важнее остальных.

Доказанное обещание в код не едет. Если ядро доказало обещание для всех входов и у функции есть пример, проверять его при каждом вызове незачем. Для модели выше напечатанный JavaScript выглядит так:

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;
}

У первой функции проверки нет: обещание доказано. У второй осталась проверка при работе: обещание держится только на примерах, и напечатанный код остановится ошибкой с кодом FLANG_PROPERTY, если правило когда-нибудь выдаст больше потолка. Тихо неверного числа не будет.

Примеры печать не гоняет. На модели с несошедшимся примером flang emit печатает файлы и выходит кодом 0. Поэтому flang test стоит перед печатью отдельным шагом — и в скрипте генерации, и в CI.

Имена функций в напечатанном коде — латиницей (rasschitatSkidku), а соответствие с именами модели лежит в самом модуле: $PROGRAM.functions — таблица «имя во flang → функция». Тесты курса зовут функции через неё: functions.get('Рассчитать скидку').

Режим --check и как ловится drift

examples/spec/typescript-codegen/generate.mjs оборачивает печать в writeGenerated. Сначала скрипт прогоняет flang test, потом flang emit --target ts. В режиме --check он не пишет файлы, а сравнивает напечатанное с тем, что лежит в generated/:

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

Если кто-то поправил return 15000 прямо в .ts, а не в модели, --check увидит несовпадение и завершится с кодом 1:

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

generate.test.mjs проверяет это отдельным тестом: печатает модуль во временный каталог, перезаписывает program.ts строкой // правка мимо модели и ждёт stale: ['program.ts']. Второй тест защищает от обратной ошибки — печати модели, которая сама не проходит свои примеры. Если заменить ожидание 3000 на 4200, скрипт останавливается до печати:

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

Третий тест подключает закоммиченный program.ts — Node 23.6 и новее читает TypeScript сам — и сверяет его ответы с примерами модели. Напечатанный код, который считает не то, что модель, тест не пройдёт.

Сверка байт в байт работает потому, что печать детерминирована: двоичный flang и сборка в WebAssembly печатают один и тот же модуль, и --check даёт одинаковый ответ на любой из них.

Порядок шагов в CI и что падает первым

Готовый workflow лежит в examples/spec/ci/flang-check.yml (кладётся в .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

Версия компилятора закреплена переменной FLANG_VERSION: 0.7.29 на уровне workflow: install.sh её читает и сверяет архив с контрольными суммами выпуска. Обновление компилятора — отдельная правка, а не сюрприз в чужом pull request.

Порядок не случаен — каждый шаг дешевле и точнее следующего:

  1. flang check --proof — разбор, типы, завершение и отчёт о доказательствах. Опечатка в имени поля падает здесь за доли секунды. Код 1 — ошибка, шаг красный. Код 3 значит «проверено, но часть обещаний держится только на примерах»; шаг его пропускает, а отчёт остаётся в логе.
  2. flang test — предметные примеры: правило собралось, но даёт не то число. Каталог проверяется одной командой: flang test static/spec/models/.
  3. generate.mjs --check — drift между моделью и закоммиченным TypeScript. Модель на этом шаге уже верна; ошибка значит, что печать забыли перезапустить после правки модели.
  4. npm run spec:examples — интеграции: HTTP-сервис, допуск отгрузки, форма, тесты эквивалентности. Самый дорогой и самый дальний от модели слой падает последним.

Про код 3 решает команда. flang check без --proof о доказательствах не говорит ничего и выходит нулём. С --proof код 3 отличает «доказано» от «проверено на примерах». Ключ --strict разводит исходы строже: 0 — доказано всё, 3 — что-то держится на примерах, 1 — опровергнуто. Для модели с процентной скидкой --strict всегда даст 3, поэтому в workflow он не стоит. Если ваши правила доказываются целиком, поставьте --strict и уберите || [ $? -eq 3 ].

Работа агента

У flang есть служба для ИИ-помощника — flang --mcp-mode, JSON-RPC по стандартным потокам. Средств у неё два: flang_check (проверить программу и вернуть отчёт о доказательствах) и flang_prove (чем доказано одно названное обещание). Печати среди них нет.

Это удобная граница. Агент правит модель и сразу видит три вердикта порознь: «доказано», «сетка N» и «объявлено, не доказано» — зелёной галочки «ок» в ответе нет. А печать кода, запись файлов и коммит остаются отдельным шагом, который выполняет человек или pipeline командами flang emit и generate.mjs.

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

Песочница проверяет модель тем же компилятором и показывает, какие обещания доказаны. Поменяйте потолок в «Очень крупной покупке» с 15000 на 16000 и посмотрите, как доказанное обещание станет ошибкой. Затем верните 15000 и поменяйте ожидание в примере — так выглядит сломанный пример, который flang emit в одиночку пропустил бы.

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

  • FLANG_EXAMPLE — пример не сошёлся. flang check и flang test выходят кодом 1, а flang emit печатает модель как ни в чём не бывало. Не печатайте без flang test перед печатью.
  • FLANG_PROPERTY — напечатанная функция нарушила обещание, которое ядро не доказало. В CI это падение теста интеграции, а не молча неверное число.
  • FLANG_TYPE — на входе значение не того типа. Прогонщик flang_cli.js рядом с напечатанным модулем сверяет вход с объявленными типами до вызова; прямой вызов функции модуля из своего кода такой сверки не делает — границу входа держите сами (как readPurchase в examples/spec/discount-api/server.mjs).

Чек-лист

  • Модель проходит flang check --proof и flang test до печати.
  • generate.mjs или ваш аналог зовёт flang test перед flang emit.
  • CI сверяет закоммиченный код через --check, а не доверяет тому, что разработчик не забыл перепечатать.
  • Версия flang в CI закреплена.
  • Порядок шагов в CI — от дешёвой проверки к дорогим интеграциям.
  • Решение про код 3 записано в workflow явно: пропускать или требовать --strict.
  • Pull request с правкой модели показывает маленький читаемый diff модели, а не только большой diff напечатанного файла.

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

Дальше: performance

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

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

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

Доска запросов
Дальше