Requirements that are checked before implementation: specs, the promise snapshot and fspec

Today a new requirement is checked by memory. Someone on the team remembers that the board capped the discount at thirty percent in March, and notices that the fresh spec promises forty. If nobody remembers, the contradiction goes into the implementation and surfaces in production, when both branches of the code are already written and shipped.

Part of this check can be made mechanical and run before the first line of code is written. There is one condition: the carrier of the requirement is not markdown but a flang program in which the requirement is written as an обеспечивает promise. The compiler answers whether it is proved. And the spec catalogue created by flang new checks the specs against each other: whether a new spec has weakened an earlier one, and whether two specs promise something incompatible.

Minimal example

Two specs about one rule — the discount for a subscriber. The first one, fspec/spec/02-discount-cap.flang, was written by finance:

модуль «Спека 2: потолок скидки»

тотальная функция «Скидка подписчику»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше тридцати» результат не больше 30
  пример «обычная подписка»
    дано сумма равно 1000
    ожидается 10
  если сумма больше 100000
    то 30
    иначе 10

The second one, fspec/spec/03-loyal-subscriber.flang, by sales, half a year later:

модуль «Спека 3: давнему подписчику»

тотальная функция «Скидка подписчику»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «давнему подписчику не меньше сорока» результат не меньше 40
  пример «давний подписчик»
    дано сумма равно 1000
    ожидается 40
  если сумма больше 100000
    то 50
    иначе 40

Each spec is fine on its own: flang check --proof proves its promise for all inputs and exits with code 0. Not a single line is marked as “disputed”. The conflict is found by the spec catalogue check — flang io fspec/guard.flang:

02-discount-cap.flang: спеки 02-discount-cap.flang и 03-loyal-subscriber.flang об одном правиле «Скидка подписчику» НЕСОВМЕСТИМЫ: 02-discount-cap.flang обещает «скидка не больше тридцати» целью «результат не больше 30», 03-loyal-subscriber.flang обещает «давнему подписчику не меньше сорока» целью «результат не меньше 40» — вместе эти цели не выполнимы ни на одном входе. Это противоречие НАБОРА требований: рёбер «использует» между этими спеками нет, и потому до сих пор их не сверяло ничто. Решите, какое из двух правил верно

Exit code 1, error code FLANG_SPEC_РАЗЛАД.

What the compiler does

1. flang check --proof judges every promise of every spec: “proved” for all inputs, “grid N” (checked only on N examples) or “stated, not proved”. A spec with an example that does not match fails the check altogether.
2. The catalogue check is itself a flang program, fspec/guard.flang. It is run with flang io: it reads the settings file settings.txt (the compiler path and the spec directory), lists the files spec/*.flang, calls flang check --proof --json for each and parses the report.
3. The agreement rules sit next to it, in fspec/policy.flang, as ordinary functions with promises and examples. A spec is accepted only if every one of its promises has the verdict “proved”; “grid” and “stated, not proved” do not count as proved.
4. The result is one line of JSON on stdout and an exit code: 0 if the specs agree, 1 and FLANG_SPEC_РАЗЛАД with the list of problems if they do not.

Catalogue layout

flang new скидки creates a package:

скидки/скидки.flang                    модуль пакета
скидки/flang.package                   имя и версия
скидки/README.md
скидки/fspec/spec/01-order-steps.flang образец спеки
скидки/fspec/guard.flang               проверка каталога
скидки/fspec/policy.flang              правила согласия спек
скидки/fspec/settings.txt              компилятор и каталог спек
скидки/fspec/snapshot.txt              слепок обещаний
скидки/fspec/README.md

One spec is one file in fspec/spec/ with a number at the start of its name and a module «Спека N: …». The number gives the order, and the file name appears in every message of the check — so it is convenient to name the spec the same way as the task in the tracker.

snapshot.txt is the promise snapshot: one line per promise, with the file, the function, the name and the goal:

01-order-steps.flang :: Шаги приёмки заказа :: шагов ровно три :: (длина результат) равен 3
01-order-steps.flang :: Шаги приёмки заказа :: первый шаг — оплата :: результат содержит "оплата"
02-discount-cap.flang :: Скидка подписчику :: скидка не больше тридцати :: результат не больше 30

The snapshot lives in the repository and changes through review, like code. It records what the team has already accepted — and it is the snapshot the check compares the specs with.

Two caveats about the distribution, both verified on 0.7.29. The build that install.sh installs does not ship the fspec/ template, and flang new refuses:

FLANG_NEW: не найден образец fspec/ (guard.flang рядом с policy.flang) — искали
в $FLANG_FSPEC_TEMPLATE_DIR и в <каталог двоичного>/../fspec. Пакет не создан.

The fix is the variable FLANG_FSPEC_TEMPLATE_DIR pointing at the fspec/ directory from the language repository of the same version. The second: the catalogue README calls flang io fspec/snapshot.flang to rewrite the snapshot, but flang new does not copy this file. Take it from the same repository directory — or add the line to snapshot.txt by hand: the check prints which one.

What the machine checks

A requirement is a promise with a verdict

A requirement is written as an обеспечивает promise on the function that computes the rule. The compiler answers with three different words, and they must not be confused: “proved” — true for all inputs; “grid N” — checked on N examples, like unit tests; “stated, not proved” — neither a proof nor examples. The spec catalogue accepts only the first. A spec whose promise rests on examples (here, fspec/spec/04-volume.flang) is rejected:

04-volume.flang: спека не проходит проверку языка — {"ledger":1,"module":"Спека 4: скидка за объём", …

This is the narrowest point of the method: the promise «скидка за объём не больше десяти тысяч» (the volume discount is at most ten thousand) on a function that computes ten percent of an amount is not proved by the kernel — it does not derive arithmetic with percentages. Such a requirement stays checked only on examples, and it does not get into the spec catalogue.

The snapshot keeps a rule from being weakened silently

When a spec is edited, the check compares its promises with the snapshot. A removed promise and a rewritten goal are errors, not warnings:

03-loyal-subscriber.flang: утверждение «давнему подписчику не меньше сорока» функции «Скидка подписчику» стояло в слепке целью «результат не меньше 40», а в спеках его больше нет — правило снято молча
02-discount-cap.flang: у утверждения «скидка не больше тридцати» функции «Скидка подписчику» переписана ЦЕЛЬ. В слепке: «результат не больше 30». Сейчас: «результат не больше 1000». Имя прежнее, обещание другое

The second case is trickier than it looks: the function body stayed the same, and the new promise “at most 1000” is still proved. Without the snapshot such an edit would pass green — the compiler checks that a promise is true, not that it has not become weaker.

Incompatible limits between specs

The check finds pairs of promises about one function from different spec files whose goals cannot hold together on any input. This is the example from the start of the chapter: “at most 30” against “at least 40”. It compares limits of the form результат не больше N, результат не меньше N and equality to a number.

A counterexample for one function

Two incompatible promises on one function (file contra.flang):

модуль «Два требования»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «требование продаж: скидка не меньше сорока» результат не меньше 40
  обеспечивает «требование финансов: скидка не больше тридцати» результат не больше 30
  если сумма больше 100000
    то 50
    иначе 10

flang 0.7.32 stops verification with exit code 1. At an amount of 0 the function returns 10, violating the sales requirement. The diagnostic names one broken promise and the input. The spec check compares the two requirements.

The honest boundary

This is not a proof that the requirements are consistent. Three specific things are checked, and none of them is complete.

• Only limits on a number are compared. The pair “at most 30” and “at least 40” is found. Goals of another form — содержит, a call to a predicate function, a condition on an input field — are not compared: «цель не о числе — спора не видно» (the goal is not about a number, no dispute is seen).
• Only functions with the same name are compared. If two specs speak about one rule under different names — «Скидка подписчику» and «Скидка давнему клиенту» — the conflict will not be found. flang 0.7.29 has no way to link two names of one concept.
• Only between spec files. Two promises of one function in one file are not compared — just as in plain flang check.
• Only proved requirements. A requirement that rests on examples does not get into the catalogue at all, and so it is never checked for disputes either. For rules with percentages this is a common case.
• External data, time, state. A rule that depends on a reference table, an exchange rate, a date or the order history cannot be checked: the logic of the language has neither time nor side effects.
• The check itself is not proved. flang io fspec/guard.flang without the --trust flag judges the provability of the check itself, computes for 2 minutes 43 seconds, takes 2.6 GiB of memory and refuses: “not proved: 133 claims: 80 proved, 53 grid”. With --trust the same check runs in 9–11 seconds. In CI it is run with --trust, and this is said out loud.

In other words, the tool answers the question “has the new spec weakened what was accepted, and do two specs promise incompatible numeric limits for one rule”. It does not see anything else — and you need to know this rather than guess.

The agent’s role

An AI agent is good at turning a conversation with a client into a draft spec: a function, a promise and examples. It is also good at explaining in words why the check refused. To make the agent check itself with the same compiler, it is connected to the flang --mcp-mode service: the tool flang_check returns the whole report, and flang_prove answers what proves one named promise. The service returns the three verdicts separately, and the agent cannot pass off a “grid” as “proved”.

The agent does not act as the arbiter. The decision is made not by the text of its answer but by a deterministic check: the exit code of flang io fspec/guard.flang and the line with the list of problems are reproducible, while “there seem to be no contradictions” is not. The same rule is in the chapter about agents (https://courses.digitable.life/en/post/spec/10-ai-agents/).

How this differs from GitHub Spec Kit

Spec Kit solves a similar task and arranges similar entities: a constitution, per-feature specs, a plan, tasks. The difference is the carrier. There the spec is markdown, and consistency is judged by a language model: the answer depends on the wording of the prompt, on the model version and on what got into the context, and two runs on the same corpus can disagree. Here the spec is a program, the check is deterministic, a refusal names the file, the function and the goal, and the step goes into CI and blocks the merge. From the same program flang emit prints code in ten languages, so the spec and the implementation cannot physically diverge.

The price is named honestly. A narrow class of requirements is proved — inequalities and equalities over numbers, strings and lists, and implications over flags; arithmetic with percentages stays on examples. Specs are compared with each other only by numeric limits of one function. Requirements that do not fit stay text and are checked by eye — as before. The choice is not between “everything is checked” and “nothing is checked”, but between “part is checked by a machine, and it is known which part” and “everything is checked by the memory of whoever was at the meeting”.

Practice in the sandbox

1. The sandbox report shows four promises: one proved, three “grid”. Which of them would fit into the spec catalogue as they are? Only «за очень крупную покупку не больше потолка»: the catalogue check would reject the other three as unproved.
2. Add a second promise результат не меньше 20000 to the function «Рассчитать скидку» and check. The report will not say that it is incompatible with «скидка ограничена»; the examples where the discount is below 20,000 turn red — with FLANG_PROPERTY and code 1.
3. Rewrite «Очень крупная покупка» so that it returns 20000 instead of 15000, and check. The edit is caught by the example «очень крупная покупка»: it violates the promise «за очень крупную покупку не больше потолка», and the check stops with FLANG_PROPERTY and code 1. In the spec catalogue the snapshot would catch the same edit as well.

Common mistakes

• Closing FLANG_SPEC_РАЗЛАД by renaming the function. The dispute disappears, because the check compares functions by name, but the requirements do not stop contradicting each other. Only changed limits make them stop diverging.
• Rewriting the snapshot together with the spec without looking. The snapshot exists precisely so that weakening is visible in review. Rewritten along with the spec, it catches nothing.
• Writing a requirement the kernel will not prove and expecting the catalogue to accept it. A promise on examples is a “grid”, and the catalogue check rejects it. This is not a bug: the requirement is either rewritten so that its condition matches a branch of the body, or left checked on examples outside the catalogue.
• Treating the check’s silence as cleanliness. No dispute means no pair of numeric limits about one function. The check does not see disputes about functions with different names, about non-numeric goals or inside one file.
• Putting the check into CI without --trust and being surprised by code 3. The catalogue check is not proved itself. Without the flag it does not run, and with the flag this has to be stated in the step description.

Checklist

• The requirement is written as an обеспечивает promise with examples before the implementation branch is created.
• flang check --proof on the spec exits with code 0: all its promises are proved.
• Each feature is a separate file in fspec/spec/ with a number in the name; the number matches the task in the tracker.
• One rule is named by one function with one name in all specs — otherwise disputes between them are not searched for.
• The snapshot snapshot.txt lives in the repository and changes only through review.
• Every pull request runs flang io fspec/guard.flang --trust, and a non-zero code blocks the merge.
• It is known what the check does not see: non-numeric goals, synonyms, disputes inside one file, requirements on examples.
• A dispute that was found is reviewed by a person: the check shows that the requirements diverge, but not which of them is right.

Catalogue cases on this topic