Executable specifications in flang Time: rule versions, snapshots, and retroactive audit
0%

Time: rule versions, snapshots, and retroactive audit

Time: rule versions, snapshots, and retroactive audit

A rule lives in time, a model does not. “The discount applies from March 1”, “the tariff was revised in July”, “a customer disputes the April charge” — these are three forms of one question: which rules apply to an event if the rules have changed since. A flang model is a snapshot of one edition of a rule. Everything about effective dates lives around it: in files, in an edition table and in the application code.

Minimal example

The rule we are about to change is a bonus accrual:

модуль «Лояльность 2025»

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

тотальная функция «Базовое начисление»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 1000 и притом покупка.«сумма» не больше 100000
    то (покупка.«сумма» умножить на 3) делить на 100
    иначе 0

тотальная функция «Надбавка постоянному»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«постоянный клиент» и притом покупка.«сумма» не больше 100000
    то (покупка.«сумма» умножить на 2) делить на 100
    иначе 0

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

тотальная функция «Начислить бонусы»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «бонус ограничен» результат не больше 5000
  пример «мелкая покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 500 и «постоянный клиент» равным нет
    ожидается 0
  пример «тысяча у обычного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 1000 и «постоянный клиент» равным нет
    ожидается 30
  пример «две тысячи у постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 2000 и «постоянный клиент» равным да
    ожидается 100
  пример «покупка ровно на потолок бонуса»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 5000
  пример «очень крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 200000 и «постоянный клиент» равным да
    ожидается 5000
  («Базовое начисление» от покупка) плюс («Надбавка постоянному» от покупка) плюс («Потолок крупной покупки» от покупка)

This model lives in static/spec/models/loyalty-tier.flang. On March 1, 2026 the thresholds were revised: the base rate is 5 percent from 5000, the regular customer bonus is 1 percent, the cap is 6000 instead of 5000. The new edition sits next to it, in loyalty-tier.v2.flang, with the module «Лояльность 2026». No file is written over another.

In both editions the cap is written as a number, and the kernel proves the promise of the large-purchase cap function for all inputs. The “bonus is capped” promise of the final function rests on examples only — the kernel does not bound a sum of percentages — so flang check --proof answers with code 3, and the printed code checks this promise on every call.

Why the model has no “today”

This is not an omission but a boundary of the language. A flang function is pure: its answer depends only on its input. The language has no current-date function. Only a plan (flang io) reads the clock — it is an action on the world, like reading a file, and the command has a key, --no-clock, that takes this action away.

There is no built-in date type either. The compiler accepts the field «дата события»: дата, but stores it as a string, and ordering comparisons on strings are refused:

модуль «Лояльность по дате»

объект «Начисление»
  «дата события»: дата
  «сумма»: неотрицательное

тотальная функция «Начислить»
  принимает начисление: «Начисление»
  возвращает число
  если начисление.«дата события» не меньше "2026-03-01"
    то (начисление.«сумма» умножить на 10) делить на 100
    иначе 0
FLANG_TYPE в файле date-err.flang, строка 10, столбец 18: левый операнд сравнения «gte» имеет тип строка: сравнения порядка допустимы только для чисел
FLANG_TYPE в файле date-err.flang, строка 10, столбец 44: правый операнд сравнения «gte» имеет тип строка: сравнения порядка допустимы только для чисел

The standard library has the module «Date and time»: a calendar day as a variant, «Дней от эпохи», parsing a timestamp. But importing it into a rule model is expensive. An imported module is checked together with the model — with all 134 examples of the library itself. On the machine where the course was prepared, the native flang binary checked such a model in 2 minutes 8 seconds, and in the sandbox’s WebAssembly the check hit the step limit (FLANG_RECURSION_LIMIT).

The workaround is simple: let the application pass the event day as a number, for example 20260410. Comparing numbers is allowed, and the rule is checked in a fraction of a second:

модуль «Лояльность с днём в числе»

объект «Начисление»
  «день события»: неотрицательное
  «сумма»: неотрицательное

тотальная функция «Начислить»
  принимает начисление: «Начисление»
  возвращает число
  пример «апрель»
    дано начисление равно запись «Начисление» с «день события» равным 20260410 и «сумма» равным 1000
    ожидается 100
  пример «февраль»
    дано начисление равно запись «Начисление» с «день события» равным 20260220 и «сумма» равным 1000
    ожидается 0
  если начисление.«день события» не меньше 20260301
    то (начисление.«сумма» умножить на 10) делить на 100
    иначе 0

Note that «день события» is an input field brought by the application. The model still does not know today’s date — it only knows what it was given. This trick works when there are two periods and they are never revised retroactively. Otherwise it is a bad idea: the file accumulates dead branches for every past year, each rule has to be read together with a calendar, and the examples stop answering the question “what does the current edition compute”. From here on the editions are kept separate.

A version as a file

The unit of versioning is the model file, and editions should be stored side by side rather than in git history. History is needed to investigate “who changed what and when”, while the April calculation must work on a deployed service without access to the repository.

policies/loyalty/
  loyalty-tier.flang        // редакция 1, события до 2026-03-01
  loyalty-tier.v2.flang     // редакция 2, события с 2026-03-01
  editions.json             // таблица периодов

Over time there will be many files, and that is fine: an edition that was ever applied to a real event is deleted only together with the retention period of the corresponding operations. A git branch, a release tag and an editions directory are three different things; do not mix them.

It helps to duplicate the edition mark in the module name: «Лояльность 2025» versus «Лояльность 2026». The module name shows up in the compiler report, in flang ast and in the printed code. A comment does not work that way: the compiler throws comments away, and // редакция 1.1 at the top of the file is visible neither in any function nor in the parsed program.

A fingerprint helps tell the files apart. flang check --proof --record writes a proof record, and it contains отпечаток256 — the sha256 of the source:

запись доказательства 1
исходник loyalty-tier.flang
строк 49
знаков 1815
отпечаток 354337829 725376771
ядро 2
утверждений 2
отпечаток256 beac695a764f4dac1da8b0a491547b367c6a30869d473eae05444b2c52632b69

The second edition has a different one — 34f496a3…. It is the same sha256 that sha256sum prints, so you can write it into the operation log without running the compiler. Any edit of the file, even of a comment, changes the fingerprint.

Who chooses the version

Choosing the edition is the application’s job. The rule is simple: the key is the event date, not the calculation date. Half-open intervals [since, until) rule out double coverage of a boundary; ISO dates compare lexicographically, so a plain < is enough. The code below runs from the root of the course repository; each edition is printed into JavaScript once (importModel from examples/spec/lib/flang.mjs):

import { importModel } from './examples/spec/lib/flang.mjs';

const editions = [
  { id: 'loyalty/2025', since: '2025-01-01', until: '2026-03-01', file: 'static/spec/models/loyalty-tier.flang' },
  { id: 'loyalty/2026', since: '2026-03-01', until: null, file: 'static/spec/models/loyalty-tier.v2.flang' },
];

const cache = new Map();

async function editionFor(eventDate) {
  const edition = editions.find((item) => item.since <= eventDate && (item.until === null || eventDate < item.until));
  if (edition === undefined) throw new Error(`нет редакции правил на дату ${eventDate}`);
  if (!cache.has(edition.id)) cache.set(edition.id, (await importModel(edition.file)).functions.get('Начислить бонусы'));
  return { ...edition, accrue: cache.get(edition.id) };
}

export async function accrue(purchase, eventDate) {
  const edition = await editionFor(eventDate);
  return { edition: edition.id, result: edition.accrue(purchase) };
}

The same snapshot { сумма: 2000, «постоянный клиент»: true } gives 100 on 2026-02-20 and 20 on 2026-04-11. A date outside all periods gives not a “default zero” but the exception “no rule edition for date 1899-05-05” — a gap in the table must be loud, otherwise it turns into a silent wrong charge. Printing is cached per edition: the compiler is not needed for every request.

In production it is better to print the models at build time (flang emit --target js) and ship them next to the service, as in the chapter on generation; importModel does the same on the fly.

Keep the edition table where the rest of the domain configuration lives, and version it together with the models: changing a period is as much a business rule change as changing a percentage. A separate case is a retroactive revision, when the business decides to recalculate a closed period. That is not an edit of the old file but a third edition with its own period and an explicit recalculation procedure: old operations stay in the log as they were, new ones are written alongside with a reference to the grounds.

A shadow run before switching

Before changing the edition table, run both versions on the same data and look at the delta. It is cheaper than any meeting: the numbers show exactly who the new edition will affect.

const было = current(snapshot);
const стало = candidate(snapshot);
if (было !== стало) report.push({ snapshot, было, стало, дельта: стало - было });

Here current and candidate are the bonus accrual function of the two printed editions. On six snapshots five differ: 1000/обычный gives 30 versus 0, 2000/постоянный gives 100 versus 20, 10000/постоянный gives 500 versus 600, and purchases at the cap and above (100000/постоянный and 200000/постоянный) give 5000 versus 6000. Such a report is a working artifact for the business, not a technical detail. In production the shadow mode runs next to the live calculation: the new edition computes but does not affect the result, and differences are logged until the switch day.

The flang language repository also has a ready “rule behaviour table” — the outcomes of a function over an enumeration of its inputs, and a diff of such tables between versions. It is not part of the installed 0.7.29 package: it is a repository script, and outside a clone the command refuses:

flang run-script: файла «.flangrc» нет ни в рабочем каталоге, ни выше до корня проекта

So a shadow run on your own data remains your tool.

Snapshot, result and a record of the decision

A customer disputes the April charge. Recalculating “now” does not answer the question: since then both the rules and the data may have changed — the customer status, a refund flag, the amount after an adjustment. So the operation log records the input, the edition and the result:

{
  "event_date": "2026-04-11",
  "edition": "loyalty/2026",
  "module": "Лояльность 2026",
  "source_sha256": "34f496a3c9d0e975e28660fb4607df997236895ac5bf34763f343db0db4994d1",
  "snapshot": { "сумма": 2000, "постоянный клиент": true },
  "result": 20
}

A snapshot is exactly the fields declared by the model’s object, no more and no less. A reference to the customer record will not do: the record will change, and the dispute will remain.

Half a year later this record can be re-checked with flang facts. It evaluates a claim on facts and answers with a verdict and its steps:

flang facts loyalty-tier.v2.flang --facts snapshot.json --claims '["«Начислить бонусы» от покупка равно 20"]' --pretty

Here snapshot.json is {"покупка": {"сумма": 2000, "постоянный клиент": true}}. The answer is "holds": true plus the steps: which function, on which facts, which value, which comparison. The same command on the first edition exits with code 1 and names the mismatch:

«Начислить бонусы» от факта «покупка» = 100, а утверждение требует «равно 20». Исходные факты — «покупка»: сумма = 2000, постоянный клиент = да

What such a check does not give you. The flang facts verdict is a computation, not a proof: it says that this edition gives 20 on this snapshot, and nothing more. That the edition applied to that date remains the application’s claim, and it must go into the log as a separate field, together with the fingerprint of the file the calculation used.

Breaking changes and CI

A change is breaking if after it the old calling code stops working or starts getting a different meaning: renaming an object field, changing its type, deleting a field, renaming or deleting a function, changing the result type. These do not break the contract: new thresholds and percentages, adding an optional field (иногда является), new examples.

A dangerous trap: flang test does not catch this. Rename «постоянный клиент» to «статус клиента» and fix the examples along the way, and all examples stay green and the command exits with code 0. But a call with the old payload fails: the runner of the printed module answers FLANG_TYPE … не задано поле «статус клиента» записи «Покупка», and a direct function call gives FLANG_UNKNOWN_NAME: запись не содержит поле «статус клиента». Examples check behaviour, not the contract.

The contract is checked by comparing the parsed programs of two versions — a projection onto the types and function signatures from flang ast is enough:

import { flang } from './examples/spec/lib/flang.mjs';

const compiler = await flang();
const shape = async (file) => {
  const ast = await compiler.ast(file);
  return JSON.stringify({
    types: ast.types.map((type) => ({
      name: type.name,
      fields: (type.fields ?? []).map((field) => `${field.name}: ${JSON.stringify(field.type)}${field.optional ? '?' : ''}`).sort(),
    })),
    functions: ast.functions.map((fn) => ({
      name: fn.name,
      params: fn.params.map((param) => JSON.stringify(param.type)),
      returns: JSON.stringify(fn.returns),
    })),
  });
};

if ((await shape(previous)) !== (await shape(candidate))) process.exit(1);

For our editions the check passes: the input shapes match, only thresholds and percentages changed. For the variant with the renamed field it fails. A red result does not forbid the change; it demands a new major edition and a migration of the consumers.

Old examples are not moved into the new edition and are not “updated to the new numbers”. They stay in the old file and serve as a regression suite: if flang test loyalty-tier.flang suddenly turns red, someone edited history. A real regression is visible at once: remove the regular customer bonus from the first edition, and two examples fail and the command exits with code 1:

пример «две тысячи у постоянного клиента» функции «Начислить бонусы» не прошёл: значение не совпало с ожидаемым: ожидалось 100, получено 60
пример «покупка ровно на потолок бонуса» функции «Начислить бонусы» не прошёл: значение не совпало с ожидаемым: ожидалось 5000, получено 3000

Practice in the sandbox

Change the threshold не меньше 5000 in the base accrual to не меньше 1000 and see which examples turn red. This is a shadow run in miniature: the example set shows the boundary the new edition moves. Then open the first edition — loyalty-tier.flang — and compare which examples it has instead.

Common mistakes

  • Calculating with the rules “as of today” instead of the rules at the event date.
  • Keeping only the latest edition and relying on git: a deployed service cannot read the repository history.
  • Writing the version number in a comment: the compiler does not see it.
  • Logging a reference to the customer instead of a snapshot of the fields.
  • Treating a green flang test as proof of compatibility.
  • Rewriting old examples to the new numbers and losing the regression suite.
  • Leaving a gap in the period table and silently falling back to a default edition.
  • Presenting a flang facts verdict as proof that the edition applies to the date.

Checklist

  1. Each edition is a separate file; old ones are not rewritten.
  2. The edition mark is in the file name and in the module name.
  3. The period table is application data, intervals are half-open, with no gaps.
  4. The edition is chosen by the event date; a missing edition is an exception.
  5. A shadow run is done and the delta is computed before switching.
  6. The log records the snapshot, the edition, the sha256 of the model file and the result.
  7. CI compares types and signatures of two editions and fails on breaking changes.
  8. Old examples stay green on their own edition.

Related: proofs and certificates and generation and CI.

Catalogue cases on this topic

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

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

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

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