Write a rule (.rule)

A .rule file has one fixed shape, read from the top. There is no forward reference, so reading downwards is reading the dependencies in order. The keywords are English; the names and the cell values stay in the language of the business — English in the worked example this page runs on, and Japanese in the sections that quote a rule transcribed from a Japanese statute, which is the language it was published in.

These are all the words that may start a line.

A complete rule

This one is tests/corpus/parcel_rate.rule: it checks clean as it stands, and the repository's test suite generates it and runs it in every target language on every commit. The amounts are made up, but nothing else about it is.

rule parcel_rate v1
description "A parcel tariff in pounds and inches, written in English. A sketch, not a transcription: the amounts are made up"

# Nothing else in the corpus is priced in USD by weight, and nothing at all reached oz, lb
# or in — an unexercised unit is an unchecked unit (§15.9).

enum size_class = envelope | small | large
enum zone = domestic | canada | overseas

group north_america = domestic, canada

inputs
  weight    : mass[lb]    range >=1lb <=70lb
  girth     : length[in]  range >=1in <=130in
  dest      : zone
  signature : bool

outputs
  fee : money[USD, incl_tax]  round up(1USD)

# One table decides the class and the next one prices it: what the first produces is a
# column of the second.
table size_of
policy first
| girth  | -> size : size_class |
| <=22in | envelope             |
| <=60in | small                |
| -      | large                |

table base_rate
policy unique
| dest          | size     | weight  | -> base : money[USD, incl_tax] |
| north_america | envelope | -       | 6USD                           |
| north_america | small    | <=160oz | 12USD                          |
| north_america | small    | >160oz  | 18USD                          |
| north_america | large    | <=160oz | 22USD                          |
| north_america | large    | >160oz  | 30USD                          |
| overseas      | envelope | -       | 16USD                          |
| overseas      | small    | -       | 38USD                          |
| overseas      | large    | -       | 60USD                          |

# A fuel surcharge is a percentage of the base, which is what the rounding on the output is
# there to settle: 12USD at 5% is 12.60USD, and up(1USD) makes that 13USD.
table fuel_rate
policy unique
| dest          | -> fuel : rate[step 1%] |
| north_america | 5%                      |
| overseas      | 12%                     |

table signature_fee
policy unique
| signature | -> extra : money[USD, incl_tax] |
| true      | 4USD                            |
| false     | 0USD                            |

result fee = base + base × fuel + extra

examples
| weight | girth | dest     | signature | -> fee |
| 5lb    | 10in  | domestic | false     | 7USD   |
| 5lb    | 40in  | canada   | false     | 13USD  |
| 20lb   | 40in  | domestic | true      | 23USD  |
| 5lb    | 10in  | overseas | false     | 18USD  |

Names and ASCII aliases

What is in the parentheses is the ASCII alias, and it becomes the public name in the generated code — a kanji cannot be an exported Go identifier.

enum 会員区分(member_kind) = 一般(basic) | ゴールド(gold) | プラチナ(platinum)

An alias is required only where a non-ASCII name reaches the public surface — the rule name, the inputs, the outputs — because a kanji has no uppercase and cannot begin an exported Go identifier. A name that is already ASCII needs none: write the whole rule in English and there are no parentheses anywhere — as in the rule above, and in Article 7 of Regulation (EC) No 261/2004, which is transcribed into the corpus in English, in EUR and km.

Elsewhere the alias is optional, and writing one decides what the generated code calls the value: derive 残余(margin) becomes margin, group 遠隔地(remote) becomes _remote / isRemote, a table output column -> サイズ(size) becomes size. Leave it out and the declared name is the identifier — every target language takes a Japanese one for something that is not exported.

The alias on a table is the exception: accepted, and currently unused, because a table is inlined into the one generated function instead of becoming a function of its own. It is kept for SQL generation.

Types

Ten, and no others.

Quantities, money, rates and dates are all integers — a date is a day ordinal, a rate a count of steps. No floating point appears anywhere: how a fraction is settled is decided by round below, never by the host language's division.

Enums are closed, and there is no open enum. That is the point: when a value is added, every table that has not accounted for it breaks the completeness check.

enum member_tier = basic default | gold default | platinum

default declares "this value needs no row of its own; being caught by a - row is correct". Without it, a value no row names is reported.

A group is a named subset of an enum and may be used in a cell wherever a value may. Groups are always expanded before checking, so a hole in a table written with groups is still found.

group north_america = domestic, canada

Imports

Two lines start with import, and both bring in the values of an enum — nothing else crosses a file boundary. A rule stays one file: what arrives is a set of names, not rows and not amounts.

Built-in enums

The first-level divisions of thirteen countries are built in: import std/us/states brings in the 56 values of us_state, and std/gb/nations, std/cn/provinces, std/tw/divisions, std/kr/provinces, std/in/states, std/fr/regions, std/es/communities, std/it/regions, std/de/states, std/au/states, std/br/states and std/jp/prefectures the rest. A value is the English name in ASCII (New_York, Bavaria, Tokyo), and a cell may also write a division in the local spelling (Bayern) or by its ISO code (NY): each is the same value. import std/都道府県 is the same 47 prefectures with the values spelled in Japanese. See the reference.

When the set belongs to somebody else

An enum like a member tier or a status is usually declared in a .proto, and whether it gains a value is decided outside this rule. Say where the set comes from, and the two are held together.

import proto "api/v1/order.proto" MemberTier -> member_tier
enum member_tier = basic | gold | platinum default

The .proto owns which values exist; the .rule owns what they are called here and how each one is treated. Every rulec check reads that file and holds the two together.

• A value on one side only is E032. It is usually the proto that gained one, and on the wire that is a compatible change.
• Once the sets agree, a value that no row names and no default marks is E033. For an enum you wrote yourself that state is a warning (W111); for an imported one it is an error, because the value arrived through a change nobody has read yet.

A table with a - row passes the completeness check when a new value turns up, and the value quietly takes the default amount. That is what E033 stops.

From a JSON Schema or an OpenAPI document

The same binding, written with a JSON Pointer, because one document holds hundreds of enums:

import jsonschema "api/openapi.json" "#/components/schemas/MemberTier" -> member_tier
enum member_tier = basic | gold | platinum default

The pointer may land on the schema or on its enum array, and an enum written inline in a property is reached the same way. The values become the aliases exactly — nothing taken off the front, no case folded — because a schema has no naming convention to earn a transformation from.

YAML is not read. A reader for the subset one file happens to use is a reader that goes wrong quietly on the next one. Point at a JSON form of the document; most toolchains can write one.

Inputs and outputs

inputs
  weight    : mass[lb]    range >=1lb <=70lb
  girth     : length[in]  range >=1in <=130in
  dest      : zone
  signature : bool

outputs
  fee : money[USD, incl_tax]  round up(1USD)

There may be several outputs. They become a NamedTuple in Python, an interface in TypeScript, a plain object in JavaScript, a Struct in Ruby, a final class in PHP, a record in Java, a struct in Rust, Swift and Go, one array per output in NumPy, one column each in SQL, and the keys of the answer's observed object from the Wasm module — and rounding applies once per output.

outputs
  accepted : bool
  raw_fee  : money[USD, excl_tax]  round down(1USDc)

An output returns the binding of its own name — a define or a table output column called raw_fee is what the output raw_fee returns. result is sugar for that, and it reaches the first output only: naming a later one is E015, and a second result line is E016.

range and round — the two you are not allowed to forget

These are not decoration. They are where this language is aimed.

range, on every numeric input and every derive

One declaration does three jobs.

1. Overflow proof. Whether an intermediate fits in int64 is computed from the declared ranges and steps.
2. The universe of the completeness check. "Every input matches some row" means every input within these ranges.
3. The entry guard of the generated code. Called outside the range, it returns an error instead of silently computing.

A derive whose range does not contain the interval it can actually reach is an error — if inputs of 0 to 1,000,000 yen can produce −100,000, then −100,000 has to be in the range.

An input that only ever acts as an entry check takes contract_only: "this does not appear in any table's conditions, but the contract still holds it to its range". That silences the unused warning, and nothing else does.

round, on every numeric output

Without it, the generated code would settle fractions on its own. Four modes, each pinned down for negative values too.

What is in the parentheses is the grid: up(10USDc) rounds to a multiple of ten cents, so −4.2 cents becomes −10 cents.

The negative direction is pinned because integer division in Python and Ruby rounds toward −∞ while in Rust, Swift, Go, Java, TypeScript, JavaScript, NumPy, PHP's intdiv, SQL and the Wasm module it truncates toward zero. Left to the host language, one rule would answer differently in each. The generated code goes through its own helper, and that they all agree is checked by unit vectors on every run.

Inputs taken from the caller's object: shape and from

A rule's inputs are flat values, and what the caller holds is usually a nested object — an API request, a message on a queue. When its shape is already described by a JSON Schema or a .proto, shape borrows that description, and a from at the end of an input's line says where in it the value stands.

shape order = jsonschema "contracts/order.schema.json" "#/$defs/Order"

inputs
  dest    : zone    from order.shipping.zone
  chilled : bool    from any order.lines where chilled = true
  lines   : number  range >=1 <=50  from count order.lines

A .proto is named by its file and message: shape shipment = proto "contracts/shipment.proto" shop.v1.CreateShipmentRequest.

from comes in four shapes:

Four things follow.

• The code that reads the inputs out is generated. Beside the rule's own function, rulec gen writes a second one that takes the whole order object. If the rule's function is order_shipping, this one is order_shipping_from(order): it reads the inputs out as the froms say, calls the rule's function and returns its answer, so the caller hands it the order as it is. It is written for Python, TypeScript, JavaScript, Ruby and PHP. In each of them, parsed JSON is usually used as it comes, as a plain map (a dict in Python, a Hash in Ruby), so the function takes a plain map too. Go, Swift, Java, Rust, SQL, NumPy and Wasm do not get it. From a .proto, it reads the JSON protojson writes: a field under its lowerCamelCase name or its .proto name, and one left out as its proto default. How to call it, and why the other seven do not get it, are in Generate and call.
• The paths are held to the contract. Every rulec check reads the contract's file. A path it does not have is E121, which says how far the path got and which fields were there; a type that does not fit is E120; a shape no input reads from is W122. A field the contract renames stops CI instead of raising a KeyError in production.
• The contract's validation is held to the inputs' declarations. A value the contract lets through and an input refuses is E122: without a maxItems on the contract's lines, an order of 51 lines passes the contract, and lines, declared range >=1 <=50, refuses it. fix.text is the annotation or keyword to add to the contract. A row reached only by values the contract never lets through is W123.
• The contract's conditions across fields are held to the rule. A CEL expression on the message, a oneof and JSON Schema's combinators relate fields to each other. A constraint the contract does not keep is E123, and a row asking for a combination the contract never lets through is W124.

No check of the table changes. What comes out of a projection is a scalar input like any other, and completeness and overlap are decided as they would be without from.

One collection, and a unary test on a field of an element, is as far as it goes. A join, a nested quantifier and a path inside a cell cannot be written: the cell language is where this tool's boundary is.

Examples has two worked rules with their contracts beside them, one on a JSON Schema and one on a .proto; the details are in the grammar.

Tables

table base_rate
policy unique
| dest          | size     | weight  | -> base : money[USD, incl_tax] |
| north_america | envelope | -       | 6USD                           |
| north_america | small    | <=160oz | 12USD                          |
| north_america | small    | >160oz  | 18USD                          |
| north_america | large    | <=160oz | 22USD                          |
| north_america | large    | >160oz  | 30USD                          |
| overseas      | envelope | -       | 16USD                          |
| overseas      | small    | -       | 38USD                          |
| overseas      | large    | -       | 60USD                          |

Left of -> are input columns, right of it output columns. A column may name an input, a derive, a boolean or enum intermediate, or an output of an earlier table.

That last one is how tables stack, and stacking is how a complicated rule gets written: in the rule above, table size_of produces size, which is a column of table base_rate. There is no limit on the depth, and one table may produce several output columns.

There are exactly two policies.

• unique (the default) — any overlap is an error. The order carries no meaning, so reordering the rows cannot change the answer.
• first — the earliest matching row wins. It exists to accept the way the business actually writes: the exceptions first, the general case last.

DMN's Any, Priority and Collect are not adopted, and completeness cannot be waived — it is always required. A table that tolerates a hole cannot be written.

What a cell may hold

Seven kinds, and no others.

The symbols are ASCII. →, ・ and 、 are still read, and rulec fmt rewrites them to -> and ,; outside names and cell values, no IME is needed.

Range notation with .. is a syntax error. "Up to 2000g" does not say whether the endpoint is included; a comparison operator does. A boundary stitched together wrongly is caught by the overlap check, with a witness.

derive, define, result

A table holds the branching and nothing else. The arithmetic lives in three places outside it.

A rate can be multiplied in (base_fee × pay_rate); it stays a rate to the end and the rounding happens once. Everything is an integer — no floating point anywhere.

A derive is a linear combination of inputs only, and can sit in a table column while still being a quantity.

derive net : money[USD, incl_tax] = subtotal - discount  range >=0USD <=10000USD

Policies that judge on the amount after a discount are real ("if the post-coupon total is at least 3,980 yen…"). If that could not be a column, the most error-prone subtraction in the whole rule would live as one bare line on the calling side.

A define names a boolean or an intermediate value. A boolean one may sit in a column.

define bulk : bool = subtotal >= 300USD
define a_earlier : bool = a_due <= b_due

Its condition holds either one value compared with a constant, or a comparison of two values whose difference cannot be subtracted (two dates, say). Comparing two numbers directly is refused, with a message asking you to declare the difference as a derive — that way the analysis is exact.

A result assembles an output.

result fee = base + base × fuel + extra

The operations are addition and subtraction, multiplication by a constant, multiplication by a rate, min, max, allocate, and the five rounding modes. There is no loop and no recursion.

allocate hands an amount out over a run of lines, in the ratio of their prices. It is the one place a rule divides by something that is not a constant.

constraint price_upto <= price_total

derive share_upto : money[USD] = allocate(discount_total, price_upto, price_total)  range >=0USD <=10000USD

result share = share_upto - share_before

Each line gets the share up to it minus the share up to the line before, so the odd yen lands on the last line and the parts add up to the amount exactly — which proofs/ states and proves rather than leaving to the examples. It asks for three names with declared ranges, none of them negative, a positive whole, and the constraint above; anything missing is E117.

Something complicated is written by stacking tables

Because a cell can only see its own column, tables stack as deep as you like. What one table produces is written as a column of the next.

What to look at is the word that appears twice. band leaves the first table and arrives as a column of the second. Not every table is in the chain: reduction reads the rule's inputs directly, because Article 7(2) restates the distance conditions rather than referring back to them.

Depth costs no visibility. When a check fails it names the row that fired in each table.

Fired rows: table band_of row 4 / table amount row 3 / table reduction row 8

Four things matter when stacking.

A rule that does this, and runs, is Examples → "Three tables stacked, two outputs returned".

A main rule and its exceptions as two tables

A tariff usually comes with a main rule and an exception that takes precedence over it: "a contract for more than 100,000 yen is taxed at the reduced rate until 31 March 2027". It can be written as one table with a reduced column, but when the sources are two — the appendix table of the Stamp Tax Act and Article 91 of the Special Taxation Measures Act — two tables read better against them.

table base  @stamp_act 別表第一
policy unique
   | stated | amount                     | -> tax : money[JPY] |
r1 | false  | -                          | 200JPY              |
r3 | true   | >=10_000JPY <=100_000JPY   | 200JPY              |
r4 | true   | >100_000JPY <=500_000JPY   | 400JPY              |
r5 | true   | >500_000JPY <=1_000_000JPY | 1000JPY             |

table reduced_rate  @measures_act 第91条
policy unique
overrides base
| reduced | stated | amount                     | -> tax |
| true    | true   | >100_000JPY <=500_000JPY   | 200JPY |
| true    | true   | >500_000JPY <=1_000_000JPY | 500JPY |

overrides base declares that the rows of this table take precedence over the rows of table base (an excerpt; the real tables have more rows). r1 at the head of a row is a label, which is how a single row is named: overrides base:r4.

The checks treat the tables that define one output as one set. Completeness is judged over both together, and when there is a hole, which table gets the row is a person's decision. Where rows meet, an overrides line settles it and the overlap passes; without one it is E105. A row of the main table that the exception covers entirely is E102, and an overrides line whose rows meet none of the other's is W117.

The generated code tries the later table first and takes the first row that applies. The trace names the table the row was written in and its position there, plus the label when it has one. The page for people says, in one sentence, "table reduced_rate takes precedence over table base. in all 10 pairs that meet, the rows of table reduced_rate lie inside the other's (an exception)".

A rule written as a sentence: clause

A one-line rule whose conditions do not line up as columns — a proviso, typically — is not forced into a table. It is a clause.

clause regular -> fee  # Article 3(1), the main text
  when always
  then base

clause free -> fee  # Article 3(2), the proviso
  when total >=3900JPY and member true
  then 0JPY
  overrides regular

when joins <column> <cell> pairs with and, the cell being any of the seven kinds a table cell may hold. A rule with no condition writes when always (so that a forgotten line cannot be mistaken for one, the same reason a blank cell is refused). then holds what an output cell holds: a literal or a name.

A clause is treated as a table with one row: checked, generated and traced by the same machinery, firing as {"table":"free","row":1}. It mixes with tables through overrides.

Where it was transcribed from: source and @

A rule transcribed from a published policy or a statute can say where each part came from: source declares a document, and @source at the end of a table, clause, row, derive or define line cites it.

source japanpost = file "yupack_tariff.pdf" sha256:9e4edb5b6a1c0f42
source measures_act = law "332AC0000000026" asof 2026-04-01
  第91条 sha256:85faf53f6f6e8196
source osha = law ecfr "29 CFR 1910" asof 2026-01-01
  "§1910.157" sha256:c2a9ce966c7e2269

define reduced : bool = made <= 2027-03-31  @measures_act 第91条

table fee_table  @japanpost
table distance          @osha "§1910.157"

There are two kinds of document, cited and copied a little differently.

Two statute databases, and the word after law says which.

A fragment the language cannot read as one word is quoted, in the citation and on the pin line alike: @osha "§1910.157". A paragraph of a CFR section ((d)(2)) is not addressed yet, because the eCFR serves a section at a time.

From then on every rulec check confirms that the copies are there and that their digests are what the rule says. When a copy differs — the file was replaced, or the article was fetched again after an amendment — the check stops and names the tables, clauses and rows that cite it (E038), which is all there is to reread. check itself never reads the network.

rulec source outdated asks whether the original moved on. For a statute it asks the database whether an amendment after asof changes the text of a cited fragment — e-Gov by the revision's enforcement date, the eCFR by the amendment date of that very section, and in both a re-issue that only moved the markup does not count; for a file with a url "…", it looks where the file came from and says whether a cited table changed, or only something this rule does not transcribe. check cannot know of an amendment until the copy is fetched again, so this belongs in a scheduled CI job.

Cite a table and its amounts are held to the copy

@japanpost table1 on a file source makes rulec source fetch take that table out of the document and write it beside it. A sheet is a table in a workbook (.xlsx), a table is a table in a Word file (.docx), and Markdown and CSV are what they look like. A PDF or a scan cannot be read here: hand an extractor (docling and the like) to rulec source fetch --via <cmd>, or cite the document whole as @japanpost.

What the copy then holds is the amounts the table writes.

$ rulec check rules/uk_minimum_wage.rule
error[E116]: The amount of row 2 is not in the copy it cites
  --> rules/uk_minimum_wage.rule:26 table by_age row 2
   |
26 | | >=18 <=20 | 1058GBPc                |
   |               ^^^^^^^^ not in the copy: 1058GBPc
   |
 The copy cited: gov table1
 An amount is not rewritten as it is transcribed, so either it was mistyped or it came from
 somewhere else. …

A mistyped digit is E116 — here 1058 for 1085, in a table whose rows still tile the whole input space and overlap nowhere. The other half of the same slip is a figure the copy states that no row uses, W120 (The copy of table1 states values no row uses), and W120 alone catches a row that was never transcribed. Only amounts are compared: a threshold is rewritten as it is transcribed (Not over $11,925 becomes <=1192500USDc) and an amount is not.

The page for people quotes the cited text, or the cited table, from the copies.

Applying another rule: apply

"The provisions of Article 20 apply to part-time staff. In this case, 'years of service' shall be read as 'period in office'." A statute written this way is saying that the rule of Article 20 is used once more with its inputs replaced. apply writes exactly that.

apply retirement = "retirement_pay.rule" sha256:b58648ea2767ebbd  # Article 31
  years = tenure
  reason = end_reason with term_end -> retirement_age, resignation -> voluntary
  base_pay = monthly_pay
  except reduction
  allowance -> part_time_allowance

The heading names the rule file being applied and the digest of that file. The lines under it are the substitutions: every input of the applied rule, without exception, and what this rule passes for it (an input, a derive, a define, an earlier table's output, or a literal). Two enums are matched value by value with with; a value spelled the same on both sides needs no entry. except leaves definitions of the applied rule out ("Article 20 (excluding paragraph 2)"). The applied rule's outputs become values of this rule, renamed with ->.

rulec check first checks the applied rule whole, on its own ground, then expands its tables and clauses into this rule under names like retirement:schedule and checks the result as one rule — so completeness and overlaps are proved on the rule as applied. Three things more are checked: that no substitution is missing (E041), that the types agree (E042), and that what this rule passes stays inside the applied rule's ranges (E043). Declare the period in office from 0 and it stops at E043, years = 0 being outside the >=1 <=40 range of years in retirement_pay.rule: the applied rule's completeness was proved over that range and no further, and whether to narrow the range or to define the excess in a clause of this rule is a business decision.

When the applied rule is amended, the digest no longer matches and the check stops with E040. rulec diff shows which inputs of this rule move — with past records, how many of them and by how much; once that is accepted, rulec source pin writes the new digest. Rows of the applied rule's tables that this rule's ranges never reach are not errors: the page for people lists them as unused by this apply, and only a table none of whose rows is reached draws W118.

The generated code carries the applied rule expanded, and the trace says {"table":"retirement:schedule","row":1,"label":"short"}. An apply goes one level, and a rule that walks a sequence cannot be applied (E044).

Saying which combinations cannot happen

A relation between two inputs, guaranteed by the caller.

constraint valid_from <= valid_to

It computes nothing. It says which combinations of inputs can happen, and three things follow from the one line.

• The completeness check stops demanding rows for what cannot happen. A table covering everything reachable is complete.
• A witness becomes a case somebody could really send. Every input the checks construct satisfies the constraints.
• The generated code refuses a violating input at the door. The proof assumed the constraint, so the code has to insist on it.

The shape is constraint <input> <comparison> <input>, with one of <=, <, >=, >, an input on each side, and both of a type that has an order — money, a quantity, a rate, a number or a date. Several lines hold at once, and A = B is the two lines A <= B and A >= B. An example that breaks a constraint is an error (E019), not a case.

Taking a sequence whose length is not fixed

Every rule so far took a fixed number of values and decided once. When the case carries a sequence instead — the rows of a tariff sheet, the candidates a filter left — elements declares what one element carries and fold declares how the walk ends.

elements fee_rows
  row_zone  : zone
  threshold : money[JPY, incl_tax]  range >=0JPY <=1_000_000JPY
  row_fee   : money[JPY, incl_tax]  range >=0JPY <=100_000JPY

table row_of
policy unique
| row_zone | threshold | -> verdict : pick |
| kinki    | <=1000JPY | take              |
| …

fold verdict over fee_rows
  skip      -> next
  halt      -> stop with 0JPY
  take      -> take_unique row_fee
  hold      -> keep_max row_fee by threshold
  empty     -> 0JPY
  exhausted -> held

What judges an element is an ordinary table. One element is one case, so completeness, overlap and units are proved over it as they always were, and the fields are declared exactly like inputs, ranges and units included. The one difference is that the caller fills them in once per element.

What fold adds is a single line per verdict: what the walk does next.

Every verdict the table can produce needs an arm (E024): the table's own completeness check, applied to the fold. An arm for a verdict nothing can reach is W115.

None of this costs the checks their termination. The table is complete and unique, so every element lands on exactly one verdict, the sequence becomes a string of verdicts, and how the walk reads them is a matter of finitely many states — independent of how many elements arrive at run time.

An example names the sequence, because a cell holds one value.

sequence near
| row_zone | threshold | row_fee |
| kinki    | 500JPY    | 800JPY  |
| kinki    | 2000JPY   | 1500JPY |

examples
| fee_rows | -> fee |
| near     | 800JPY |

A sequence with no rows is the example for a sequence with nothing in it. What comes out is the same function with one more argument — for every target but SQL, where one query has no place to carry a value from row to row and stop partway.

A rule that runs is in Examples, under "A sequence walked into one answer".

Counting instead: count

A fold turns a sequence into one answer. A count turns it into one number and hands the rule back to the tables.

count hits over candidates where kind = same  range >=0 <=50

What where names is a column of one element — a field, or a column a per-element table produces — whose values are a closed set. For an enum, = <value> says which one to count; a bool column needs nothing after it (where chilled).

From there the count is a number, so it can be a column.

| hits | auto_ok | -> action : action_kind |
| 0    | -       | register                |
| 1    | true    | auto                    |
| 1    | false   | review                  |
| >=2  | -       | review                  |

That is why count exists beside fold: when an ordinary table turns the number into a decision, the boundaries of that decision are checked — a gap or an overlap between 0, 1 and >=2 stops the rule as any other would.

The range is required and says two things: the universe the completeness check quantifies over, and the cap on the sequence. A longer sequence is refused at the door by the generated code, for the reason a number outside its range is — the proof was made over what was declared.

A count counts and a sum adds one column up — sum total over lines of amount. An average does not follow: dividing by a count is dividing by a variable, so it belongs before the call, as a value. A rule cannot hold both a fold and a count or sum (E031): two endings for one walk, and a fold may stop partway.

A rule that runs is in Examples, under "Counting a sequence, and deciding from the count".

A state carried from call to call: machine

Some rules are one step of something that goes on: an order is paid, shipped and delivered, or cancelled. The state lives with the caller — in the order's row of a database — and every call is passed the state and answers the next one. The table is written as always, with the state as a column and the next state as an output; state in an output cell hands the state back as it was.

table step
policy unique
| state     | event  | -> next_state | refund      | accepted |
| received  | pay    | paid          | 0JPY        | true     |
| received  | cancel | cancelled     | 0JPY        | true     |
| paid      | cancel | cancelled     | amount_paid | true     |
| …
| cancelled | -      | state         | 0JPY        | false    |

machine order over step
  carry   state -> next_state
  held    amount_paid
  initial received
  final   delivered, cancelled
  never   shipped after cancelled
  once    refund >0JPY

carry is the one line with new meaning: the output a call answers is passed back as that input on the next call. The generated function does not change — it keeps nothing, and the caller keeps the state. What the section adds is claims about every sequence of calls, and check proves them:

held amount_paid says that one case passes the same paid amount on every call, so the claims are about the sequences that keep it, and a sequence that changes it halfway is never offered as a counterexample.

A claim that fails comes back with the shortest sequence of calls that breaks it, each call an input the rule takes. The rest is the table's own checks: a state and an event with no row is E101 as it always was, so what happens when a cancel request arrives after shipment is asked before anybody runs the code.

A scenario is an example that runs for several calls. It has no column for the carried input: the first call starts in initial, and each later one where the call before it ended.

scenario late_pay
| event  | amount_paid | -> next_state | refund  | accepted |
| pay    | 3000JPY     | paid          | 0JPY    | true     |
| cancel | 3000JPY     | cancelled     | 3000JPY | true     |
| pay    | 3000JPY     | cancelled     | 0JPY    | false    |

Beside the function, each language gets the initial state and a test for a final one. The vector suite gets sequences of calls, and rulec test has every language play them, handing the state it answered to its own next call. Between two versions, rulec diff gives the shortest sequence of calls the two answer differently, and the states from which a case in progress could no longer finish.

The claims stay decidable because the state is a finite enum and nothing else is carried. A total so far — refunds paid, a balance — is kept by the caller and passed in, as it always was.

A rule that runs is in Examples, under "One event in an order that goes on".

Examples

examples
| dest    | weight | total     | member   | -> fee |
| Okinawa | 2500g  | 40_000JPY | basic    | 0JPY   |
| Tokyo   | 1999g  | 12_000JPY | platinum | 400JPY |

examples is an executable specification. rulec check runs every row through the reference evaluator and reports a failure with the rows that fired.

Every output must have a column. Dropping one is an error, and the reason is worth knowing: the agreement of the reference evaluator, the generated Python and the generated Go stays green when all three share the same mistake. That happened — rounding for multiple outputs was missing in all of them at once, and the agreement check was green to the end. The only thing that can break it is an expectation a person wrote.

What cannot be written

• Nested objects (order.destination.state) — flatten at the boundary and pass the scalar in.
• Iteration anywhere you like, and recursion — a sequence is walked once, by fold (the section above); every other repetition, a stack of coupons applied in order among them, stays with the caller.
• An average over the elements — it divides by how many there are, which is dividing by a variable. Compute it before the call and pass it in (the count and the total are written with count and sum).
• A number carried from one call to the next — a balance, how many times so far. The state a machine carries is an enum; a running total is kept by the caller and passed in.
• Date arithmetic — comparison and range only.

Allowing these would stop the completeness and overlap checks from terminating. What cannot be written is the price of the checks finishing.

The complete grammar, down to the lexical rules and the reserved words, is in Grammar.

What it proves Grammar