この資料は英語です
リファレンス(文法・形式・生成物・エージェント向けの手順)は、第一の読み手がエージェントなので英語で書いています。日本語で読めるのは、ホーム・インストール・表を書く・何を証明するか・生成して呼ぶ・突き合わせと再生・例で見る・自分のルールが入るか、そして診断コードの台帳と互換性です。
The .rule language
The complete definition of the syntax. It is meant to be read by something that has to write
a .rule correctly the first time, so it states what is allowed rather than motivating it.
The reasoning behind each restriction is in DESIGN.md; the diagnostics you get for breaking
one are in codes.md, and rulec explain <CODE> prints any of them.
Two things to know before anything else.
- Keywords are English and there is exactly one spelling of each. No synonyms and no abbreviations. Names and cell values are the business's own words: the rules in this repository are written with English ones, and each one transcribed from a Japanese document has its Japanese original beside it.
- The file is read top to bottom and there is no forward reference. A name is declared above every line that uses it.
1. File structure
One .rule is one rule, and becomes one generated function. Sections appear in this order;
every one except rule is optional, but an order that differs from this one is an error.
rule <name>(<alias>) v<version>
description "<one line>"
import std/<name>
import proto "<file>" <Enum> -> <enum of this rule>
import jsonschema "<file>" "<pointer>" -> <enum of this rule>
source <name> = law [<database>] "<law id>" asof <date>
<fragment> sha256:<digest>
source <name> = file "<file>" [url "<url>"] sha256:<digest>
shape <name>(<alias>) = jsonschema "<file>" "<pointer>"
shape <name>(<alias>) = proto "<file>" <Message>
enum …
group …
inputs
…
outputs
…
derive … ┐
define … │ these three interleave freely, in dependency order
table … ┘
policy …
overrides …
clause … (a one-row definition written as prose; interleaves with the three above)
apply … (another rule, applied with its inputs bound; interleaves too)
<callee input> = <value>
except <definition>, …
<callee output> -> <name>
result …
machine <name>(<alias>) over <table> (the rule is one step of a state machine, §6.4)
carry <input> -> <output>
initial <state>
final <state>, …
never <state>, … after <state>, …
once <output> <cell>
scenario <name>(<alias>) (a sequence of calls from the initial state, §6.4)
| … |
examples
…
ruleis the first line of the file.v1is the version; it is free text and appears in the generated header.descriptionis one line, in quotes.inputsandoutputsare followed by indented declarations, one per line.derive,defineandtableare a pipeline: each may use anything declared above it.policybelongs to thetableimmediately above it, and so doesoverrides: the tables or labelled rows, declared above, that every row of this table takes precedence over (§7).applyis an item likederive,defineandtable: another rule file, applied with every one of its inputs bound to a value of this rule (§7, "Applying another rule"). The lines under it are indented by two spaces.machinenames the table that decides the state it carries;scenarioblocks follow it.examplescomes last. There may be more than one section of them (§9).
A blank line separates sections. # starts a comment that runs to the end of the line;
comments may appear anywhere, including at the end of a table row and on a line of their own
in the middle of a block — a line that holds nothing but a comment does not end the
section, where a blank one does. A comment at the end of a declaration, of a table line or
of a row is shown on the page rulec doc renders, which is where the source a table or a row
was transcribed from belongs.
2. Lexical structure
Encoding is UTF-8 without a BOM. Identifiers are normalised to NFC. A cell never contains a line break.
Identifiers start with a letter or _ and run to the next delimiter. Kanji, kana and
Latin letters are all identifier characters; - never is (it is always an operator or the
don't-care cell). Anything else at the start of a name is E002.
ASCII aliases are written in parentheses after the name: 届け先(dest). They become the
identifiers the generated code uses.
An alias is required wherever a non-ASCII name reaches the public surface — the rule name, an input, an output — because a kanji has no uppercase and so cannot begin an exported Go identifier. A missing one is E011. A name that is already ASCII needs no alias: it is its own identifier, so a rule written entirely in ASCII carries no parentheses at all.
rule bulk_fee v1 # no alias: the name is already an identifier
inputs
weight : mass[g] range >=1g <=40kg
Everywhere else an alias is optional, and writing one changes what the generated code
calls the value: derive 残余(margin) becomes margin, group 遠隔地(remote) becomes
_remote / isRemote, and a table output column -> サイズ(size) becomes size. Leave the
alias out and the declared name is used as it stands — every target language accepts a
Japanese identifier for something that does not have to be exported.
The alias on a table is the one exception: it is accepted and currently unused, because
a table is inlined into the one generated function rather than becoming a function of its
own. It is kept for SQL generation, where a table will need a name of its own.
An alias that is a word one of the targets has taken is W121. A keyword is the hard case
— type as an input's alias generates Rust that does not compile — and a builtin is the
quiet one: the rule's alias names the generated function and an enum's alias names a type,
so sum or list there hides Python's. A parameter or a local hides nothing outside its own
body, so the warning is raised for those only when the word is a keyword. It is a warning
because a target you do not generate cannot hurt you.
Numbers are digits, optionally with _ as a separator, optionally preceded by -,
optionally followed by a multiplier and then a unit:
| part | values |
|---|---|
| multiplier | 万 (10⁴), 億 (10⁸), 兆 (10¹²) |
| unit | mass mg g kg t oz lb · length mm cm m km in ft yd mi · rate % · money 円 銭, or an ISO 4217 code, whose hundredth is that code plus c (USD and USDc). Two currencies never convert: there is no exchange rate here, so mixing them is E103 |
1000万円 is 10,000,000 yen, which 10_000_000JPY writes as well. A number in a cell must carry its unit: a bare 2000 where
a quantity is expected is an error. 2kg and 2000g are the same value; the stored integer
is always in the unit the type declares.
A thousands separator is not written (E049): , separates the members of a set, so the
1,000JPY a document prints would be two values. Write 1000JPY, or 1_000JPY to group the
digits; the diagnostic's fix.text is the literal rewritten.
Dates are written YYYY-MM-DD. They are held as day ordinals, which is what makes an
interval over dates exact.
Strings are double-quoted and must close on the same line (E001).
Symbols. The canonical spellings are ASCII:
| written | means |
|---|---|
-> |
the boundary between input and output columns |
, |
the separator inside a set, and between type attributes |
- |
don't care (a cell of its own) |
<= >= < > |
comparison |
+ - * / |
arithmetic in an expression |
\| |
a table cell boundary |
: ( ) [ ] ? |
declarations |
→, ・, 、, ,, ≦, ≧, ×, ÷, −, and fullwidth digits are all read, and
rulec fmt rewrites them to the ASCII forms. .. is never read: see §7.
3. Types
Fourteen, and no others.
| type | written | notes |
|---|---|---|
| boolean | bool |
|
| enum | the enum's name | a closed finite set, declared with enum or brought in with import |
| mass | mass[g], mass[lb], … |
the unit is part of the type. mg g kg t oz lb |
| length | length[cm], length[in], … |
mm cm m km in ft yd mi |
| area | area[m2], area[坪], … |
mm2 cm2 m2 a ha km2 坪 in2 ft2 yd2 mi2 ac. A dimension of its own: width * depth is E103, because there is no dimensional analysis here (§2.1) |
| volume | volume[m3], volume[L], … |
mm3 cm3 m3 mL L kL. cm3 and mL are the same size, and so are m3 and kL. There is no gallon — the US one is 3.785411784 L and the imperial one 4.54609 L |
| duration | duration[h], duration[min], … |
ms s min h d w. A minute is min, because m is the metre. This is a span of time; a calendar day is date |
| temperature | temperature[℃], temperature[℉] |
℃ ℉. Ordered, not arithmetic: comparison and range only (E048). 41℉ is exactly 5℃, and a literal converts between them; a difference of two temperatures is not written at all |
| sound | sound[dB] |
dB, a sound pressure level. Ordered, not arithmetic (E048): a decibel is a logarithm, so adding two of them is not two sounds' worth |
| money | money[JPY, incl_tax], money[USD, excl_tax] |
currency and tax flag are both part of the type. Any ISO 4217 code, or 円; the hundredth of a currency is its code plus c, so money[USD] counts dollars and money[USDc] counts cents. Two currencies never convert — there is no exchange rate here, and mixing them is E103 |
| rate | rate[step 1%], rate[step 0.1%], rate |
the stored integer counts steps. An input declares its step (E103 without one): what the caller passes is that integer, and its meaning cannot change when a row is added. An output travels at the step it declares, or with none declared at its rounding grid, which every answer sits on — never at whatever its rows happen to write, so no row can change what the integer counts. A rounding grid that is not a whole number of the declared step is E114. A computed rate that is not an output may leave the step out; it is held at whatever its literals need |
| number | number |
a whole number with no unit — a count of things, a number of days, a score |
| date | date |
comparison and range only. There is no date arithmetic (E048) |
| string | string |
cannot be a table column (E110). Use it for an output, or for an input that only passes through. A value that decides a branch belongs in an enum |
| optional | member_kind? |
any of the above, plus the absent value. Consumed by the cell none |
Every quantity, money, rate, number and date is an integer internally. No floating point appears anywhere in the tool or in the generated code.
Money of different currencies or different tax flags cannot be added or compared, and neither can values of different units (E103). A conversion is written as a table, never as a formula.
There are no compound dimensions. weight * length and width * depth are both E103, as amount * amount
always was: this tool does no dimensional analysis, and a dimension invented to hold a product
would be one nobody declared. Where the product itself is what a rule decides on — a floor
area, a volume of water — take it as an input, or look it up in a table. For the same reason a
divisor carrying a unit has to be written in the left side's unit: a divisor is read at the
unit it is written in and never converted, so weight / 2kg, with weight a mass[g], is E103 rather than a
division by 2000.
A value is read through its unit, wherever it is written. A range bound, a table cell, an
expected value in examples, a rounding grid, a step inside a type's brackets, an answer a
fold gives, a member of a group: each is a value of the thing it sits in, and one that is
not is E103 (E012 for a name). round up(10USDc) on a money[USD] output is refused, and
round up(1000USDc) is accepted as the ten dollars it is worth — the unit is read, not merely
recognised.
Three types are ordered but not arithmetic: date, temperature and sound. They are
written in cells, compared, and given a range, and that is all — + - × ÷ over any of them
is E048. A ℃ is a scale whose zero is displaced, so temp * 2 means nothing; a decibel is a
logarithm, so adding two of them is not two sounds' worth; a date is a calendar day, and there
is no type to hold the result of subtracting one. Where a difference is itself what the rule
decides on, compute it on the calling side and pass it in — as a duration, or a number.
Declaring an enum
A value may be marked default:
which declares "this value needs no row of its own; being caught by a - row is correct" and
silences W111 for it.
Two enums may have values of the same name — Stripe's capture_method and
confirmation_method both have automatic and manual. A value is read in the enum of the
place it is written: the column of a cell, the output of an output cell, the carried enum in
the lines under machine. A value of one enum written where another is expected is E103,
in an output cell as in any other. A value may be spelled like one of the reserved words
(§12), except the eleven its own position would read as something else.
Declaring a group
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. Its members are values of one enum (E103 when they mix two); when two enums both have every member, the group belongs to the enum of the first column it is written in, and a column of the other enum is E103.
3.1 import
Two lines start with import, and both bring in the values of an enum — nothing else
crosses a file boundary. A rule is still one file: what is imported is a set of names, not
rows, not amounts, not another rule.
| line | what it brings | who owns the set |
|---|---|---|
import std/<name> |
a built-in enum | rulec, frozen |
import proto "<file>" <Enum> -> <enum of this rule> |
the value set of an enum in a .proto |
that .proto, outside this rule |
import jsonschema "<file>" "<pointer>" -> <enum of this rule> |
the value set of an enum in a JSON Schema, OpenAPI included | that file, outside this rule |
rulec import csvandrulec import xlsxare a different thing that shares the word: a command that writes a first draft of a.rulefrom a spreadsheet, once. It leaves no line in the file and nothing is read again afterwards. These two lines are read on everyrulec check.
Built-in enums
import std/<country>/<kind> brings in the first-level divisions of a country: ISO 3166-1's two
letters in lower case, and the kind of division. The enum is named <country>_<kind, singular>.
| import | enum | values | generated type |
|---|---|---|---|
std/us/states |
us_state |
56 (the 50 states, DC, 5 territories) | UsState |
std/gb/nations |
gb_nation |
4 | GbNation |
std/cn/provinces |
cn_province |
33 (Taiwan is std/tw/divisions) |
CnProvince |
std/tw/divisions |
tw_division |
22 | TwDivision |
std/kr/provinces |
kr_province |
17 | KrProvince |
std/in/states |
in_state |
36 (28 states, 8 union territories) | InState |
std/fr/regions |
fr_region |
18 | FrRegion |
std/es/communities |
es_community |
19 (17 communities, Ceuta, Melilla) | EsCommunity |
std/it/regions |
it_region |
20 | ItRegion |
std/de/states |
de_state |
16 | DeState |
std/au/states |
au_state |
8 (6 states, 2 territories) | AuState |
std/br/states |
br_state |
27 (26 states, the Federal District) | BrState |
std/jp/prefectures |
jp_prefecture |
47 | Prefecture |
A value is the division's English name in ASCII, with _ for spaces and hyphens (California,
New_York, Bavaria, Ile_de_France, Sao_Paulo, Tokyo); that is the spelling every
output, the wire and the generated code use. Inside a rule a division may also be written in
the country's own language (Bayern, 北京, 서울특별시, Île_de_France, São_Paulo) or by
its ISO 3166-2 code without the country (CA, BY, NSW; a code that starts with a digit,
such as Japan's, Korea's and Italy's, cannot be a name). Every spelling of a division is the
same value: completeness, overlap, the vectors and the certificate see one value.
import std/都道府県 brings in the same 47 prefectures as std/jp/prefectures, as the enum
都道府県 with the values spelled in Japanese (東京都); both accept both spellings, and the
generated code is the same. One rule imports one country once (E013). A word that is no value
gets the closest spelling, or the namespace of the country that has it, in E012's note; a code
two imported countries share (WA is Washington and Western Australia) is E012 too, and is
written by its name instead. The names come from Unicode CLDR (see THIRD_PARTY_NOTICES).
Anything else after import std/ is E013.
An enum a .proto owns
When the values come from a service contract, the set is not the rule's to decide. The line
above says where it comes from, and rulec check reads that file on every run and holds the
two together. The path is followed from the directory of the .rule.
The two sides carry different things, and neither can be derived from the other. The .proto
owns which values exist; the .rule owns what they are called here and how each one is
treated (a value named in Japanese takes its name from the rule; the proto has only the ASCII one).
So what is checked is that they agree:
- the value names are matched by the ASCII alias, with the enum's own name taken off the front
(
MEMBER_TIER_GOLDisgold), which is the prefix conventionbuf lintenforces. The prefix is the name split into words the way buf splits it, soHTTPMethodasks forHTTP_METHOD_andTier2forTIER2_. It is taken off only when what is left begins with a letter:SIZE_60issize_60, since an alias cannot begin with a digit; - the zero value is proto3's "not set" when it is named
…_UNSPECIFIED, so it is not a value the table answers for — the generated code refuses it at the entry like any other non-member. A zero value named anything else is a value like any other; - a value on one side only is E032, in either direction;
- and once the sets agree, a value that no row names and no
defaultmarks is E033.
E033 is the reason this exists. Adding a value to an enum is a compatible change on the wire,
so the tools that guard the contract let it through; a table with a - row then passes the
completeness check, and the new tier quietly takes the default amount. For a value you wrote
yourself that state is a warning (W111). For a value that arrived through the contract it is an
error, because nobody has read it yet. Marking it default is how you say you did.
An enum a JSON Schema owns
import jsonschema "api/openapi.json" "#/components/schemas/MemberTier" -> tier
enum tier = basic | gold | platinum default
The same binding, for the other place a value set is declared. Everything about E032 and E033 is the same; two things differ.
How the enum is named. One document holds hundreds of enums, so one is named by a JSON
Pointer rather than by a name. The pointer may land on the schema (its enum is then read) or
on the array itself, and a leading # and a leading / are both optional. An enum written
inline in a property — the usual shape in OpenAPI — is reached the same way
(#/components/schemas/Order/properties/status). A pointer that does not resolve comes back
with the keys that were there.
How the values map. They are the aliases exactly: nothing is taken off the front and
no case is folded. A .proto earns its transformation from a convention buf lint enforces;
a schema has no such convention, and inventing one would mean a rule and a schema that look
like they agree while sending different strings. An enum of numbers or nulls is refused by
name: the values of a rule's enum are names.
YAML is not read. It is the usual spelling of an OpenAPI document, and the reason for the refusal is not that a reader would be hard to start: a reader for the subset one file happens to use is a reader that goes wrong quietly on the next one, and a value set that is quietly wrong is the one thing this must never be. Point at a JSON form of the document, which most toolchains can write.
3.2 source — the documents a rule transcribes
source stamp_act = law "342AC0000000023" asof 2026-04-01
別表第一 sha256:0ba69792e960021e
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
source japanpost = file "yupack_tariff.pdf" sha256:9e4edb5b6a1c0f42
source terms = file "tariff.md" url "https://raw.githubusercontent.com/o/r/a1b2c3d/docs/tariff.md" sha256:4f1e0a77b2c3d5e6
table1 sha256:a583ec8586bbf596
table base @stamp_act 別表第一
policy unique
| stated | amount | -> tax |
| false | - | 200JPY | @stamp_act 別表第一 # no amount stated
A source names a document, after import. A law is a law in a statute database, by the
id that database gives it, read as of a date: the API returns one fragment at a time, so each
fragment the rule cites is kept as a copy beside the rule
(sources/law/<law id>@<date>/<element>.xml) and pinned by its digest on the line under the
source.
Which database is the word after law, and there are two.
| word | the database | the id | a fragment |
|---|---|---|---|
(none), or egov |
e-Gov, the Japanese government's statute database | the law id, 342AC0000000023 |
第91条, 第20条の2第3項, 別表第一, 附則第3条 |
ecfr |
the Electronic Code of Federal Regulations: US federal regulations as in force on a date | a title and a part, 29 CFR 1910 |
a section, §1910.157 (or 1910.157) |
The word is left out for e-Gov, so a rule written before there was a choice reads the same.
What differs between the two is the shape of the id, the shape of a fragment, and where a
copy comes from — not what a copy is, nor what it is held to. 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 and cutting the copy up here would make it worse evidence than the one the
government served. A file is a document beside the rule — a tariff
sheet, a workbook, a policy in Markdown — pinned whole on its own line. A url on
it says where that copy came from, so rulec source fetch can bring it again and rulec source
outdated can ask whether the original has moved on; a document that arrived from a person has
no address and leaves it out.
A document's fragments are its tables. table1 is the first table of the document in document
order and 表1 is the same name in Japanese; for a workbook a table is a sheet. A cited table
is taken out of the document by rulec source fetch, written beside it as
<document>.fragments/table1.tsv (tariff.md.fragments/table1.tsv), and pinned under the source line exactly as a law's articles
are — so a revision of the document that moves a cited table fails the check, and one that does
not, does not. The formats read here are csv, md, xlsx and docx — a workbook's table is a sheet, a Word
document's is a w:tbl, and a merged cell leaves the column it took empty rather than being
filled in, because the copy is evidence. A PDF or a scan needs an extractor that is not this
program: rulec source fetch --via <cmd> runs one as a child process and reads the tables it
hands back (formats.md, the extraction protocol), and the name it gives itself is
kept beside the copies and shown on the page for people. A document with no extractor to hand is
cited whole.
The rows are then held to that copy, which is the one thing a completeness proof cannot do:
it says the table is consistent with itself, not that it says what the document says. An amount
a row writes that the copy does not show is E116. Where the copy has a heading that says a
word of the row's cells — 関東, or 一般 for a row the copy heads 一般の事業 — the amount is
looked for in that heading's row and column only, since the amount of the next row down is in
the copy too; and a rate the copy writes per thousand, 5/1,000 or 1,000分の5, reads as the
0.5% it is. A number the copy states as a
whole cell that no row of the citing table uses is W120, and the two together are what a
mistyped digit looks like (890円 is nowhere in the copy, and the copy's 880円 is used by
nobody). A threshold is rewritten as it is
transcribed — 1,949,000円まで becomes <=1949000円 — so its text cannot be compared, but one
thing survives the rewriting: which of the two bands the boundary value itself falls in.
The copy's 60cm以下 and 60cmを超え both put 60cm in the band below, and so do <=60cm and
>60cm; a row that puts it in the other band is E119, reported on both of the rows that
share the boundary. The word is read beside the number (60cm以下, Under 18, Not over
$11,925) or in a heading over its column (円以上 and 円未満, as a premium table writes
them). A boundary the copy words neither way — 18 to 20, 60〜80 — is left alone, because
naming the numbers that bound a band does not say which band holds them. W120 asks only about cells that are nothing but a
number, and a row that merges what the copy lists one by one (<=3kg over its 1kg, 2kg and
3kg) accounts for all of them. A table that transcribes only part of a fragment moves its
citation from the table line onto the rows that came from it: a row's citation says only where
that row came from, so the rest goes unasked while the amounts are still checked.
@<source> <fragment> at the end of a table, clause, derive or define line, or after
the last bar of a row, says which fragment the definition transcribes: 第91条, 第20条の2,
第20条第2項, 第20条第2項第3号, 別表第一, and the supplementary provisions as 附則第3条 (the law's
own) or 附則(令和七年三月三一日法律第一三号)第3条 (an amending law's, its number spelled as the law's
heading spells it); several are separated by ,. A file is cited
whole, @japanpost, or by one of its tables, @japanpost table1; a law cited with no article is E037, and so
is a document fragment named anything but 表<n> or table<n>. The citation goes before the # comment. check holds the pins to the copies and never reads the network: a cited
fragment without a pin is E037 (the fix is the pin line), a pin that differs from the copy is
E038 (naming the definitions that cite it), a fragment with no copy is E039, and a pin no
citation uses is W119. rulec source fetch brings the copies — from e-Gov for a law, from the url for a file, and
out of the document itself for a cited table —
rulec source pin writes the pins, and rulec source outdated asks whether the original has
moved on, which is the one question check cannot answer offline. For a law it asks e-Gov
whether an amendment enforced after the date changes the text of a cited fragment (a revision
that only re-marks the XML is not a change).
For a file it depends on what the url names, and the difference is worth knowing before
writing one. A URL that names a commit cannot go stale, so the question is asked of the
repository instead: on a GitHub raw URL whose revision is a commit
(raw.githubusercontent.com/<owner>/<repo>/<commit>/<path>), outdated asks what has touched
that path since, and answers with the commits, their dates and their subjects, and the URL to
pin next. A URL that names a branch, or any other URL, can only be fetched and compared with
the pin: the answer is then that the bytes differ, which for a PDF or a spreadsheet is all
anything can say — and a page that changes its footer says it too. A commit is to a file what
asof is to a law, and pinning one is what makes this question worth asking. GITHUB_TOKEN
or GH_TOKEN is passed on when it is set; without one the API allows sixty requests an hour. The
page for people quotes the fragment under the definition that cites it: an article as its text,
with the date that text came into force and the amending law; a document's table as the table
itself, beside the rows transcribed from it. Every generated file names the sources in its header
(Cites: measures_act = law 332AC0000000026 asof 2026-04-01 (第91条 sha256:…)), and rulec api lists
them under sources, a file source carrying its url in both.
3.3 shape and from — where the caller's object holds an input
An input may say where it comes from, and a shape says which contract the object it comes
from is already described by:
shape order = jsonschema "api/order.json" "#/$defs/Order"
shape order = proto "api/v1/order.proto" shop.v1.Order
inputs
dest : jp_prefecture from order.shipping.prefecture
cold : bool from any order.lines where category = "chilled"
lines : number range >=0 <=200 from count order.lines
It changes no check of the table. What comes out of a projection is a scalar input like
any other: the region analysis never learns that it was projected, and completeness, overlap,
units and overflow are decided exactly as they would be without it. What the two declarations
buy is that the glue between the caller's object and the rule's flat inputs is generated
rather than written by hand, and that a field the contract renamed is E121 rather than a
KeyError in production.
from comes last on the line and runs to its end. Four shapes, and no more:
| written | what it yields |
|---|---|
from <shape>.<field>… |
the value at the path |
from any <shape>.<collection> where <field> = <value> |
bool — some element passed |
from all <shape>.<collection> where <field> = <value> |
bool — every element did |
from count <shape>.<collection> [where …] |
number — how many passed |
One collection, and a unary test on a field of an element. A join, a nested quantifier
and a path inside a cell are all refused, for the reason §0 gives: the cell language is where
this tool's boundary is, and a path in a cell would put the caller's object model inside the
checks. The test after where takes the same forms a cell does (= a, = a, b, not: a,
<=100), and it compares the raw value the contract carries, so a literal in it carries
no unit — a contract has none, and comparing a scaled number with a raw one is refused (E120).
From a .proto, the raw value is what protojson writes: an enum is its value's name
(where temp = TEMP_FROZEN), a 64-bit integer is compared as the number it is though it
arrives as a string, and bytes or a message is nothing a where can compare (E120).
The contract is read on every check, resolved against the directory of the rule, and
carries no digest — the same footing as import proto (§3.1): what holds the two together
is the paths. A JSON Schema is read far enough to resolve a path: properties wherever an
object may have them — directly, or under allOf, anyOf, oneOf and if/then/else —
items, and a $ref that stays inside the document. The keywords written beside a $ref
count as well from JSON Schema 2019-09 on, which OpenAPI 3.1 follows, and are ignored before,
as draft-07 and OpenAPI 3.0 say. A .proto is read far enough for the same: messages and
their fields, repeated included, with map skipped rather than guessed at; the members of a
oneof are fields of the message, each with presence of its own like an optional field.
A path that cannot be resolved is E121, which says how far it got and which names were
there; a type that does not fit is E120; a shape no input projects from is W122.
The contract says which values can come, too, and that is held to the input. A path says
where a value comes from; the contract's validation says which values pass — Protovalidate's
(buf.validate.field) rules on a field of a .proto (gte, lte, in and the rest, the count
of a repeated, the listed values of a string), and a schema's minimum, maximum,
exclusiveMinimum, exclusiveMaximum, enum, minItems, maxItems and required. Each is
compared with what the input takes — its range, the values of its enum, the range of a
count — and a value that passes the contract but not the input is E122: the generated
code would refuse, at the door, something the caller's own validation let through. A proto3
number field with no rule lets 0 through, because that is what an unset field is; an input
that does not take 0 stops there. A schema that lets a value be null — "type": ["integer",
"null"], or OpenAPI 3.0's nullable — is E122 for an input that is not optional. A row whose
cell on a projected input admits nothing the contract lets through is W123. Rules this does
not read — a predefined rule, a pattern, the part of a CEL expression below — are read as not
there, which reads the contract as wider than it is: a finding it did not need to make is
possible, a missed one is not. fix.text of an E122 is the option or keywords to write in the
contract (narrow_contract); whether the contract or the rule is the side to change is a
person's decision. Still no check of the table moves: what is compared is the contract with
the input's own declaration.
Conditions across fields are read too. A contract relates fields to each other: a CEL
expression on a .proto message ((buf.validate.message).cel, cel_expression) or on a field,
a oneof or a (buf.validate.message).oneof that lets one of its fields be set, JSON Schema's
allOf, anyOf, oneOf, not and if/then/else. Of CEL, the part that is a condition
on whole numbers, strings and booleans is read: sums and differences of fields and constants,
a product with a constant, the six comparisons, in against a list of literals, size() of a
repeated field, has(), !, &&, || and ? :, and a string-valued rule that passes when it
returns "". What is not — division, %, string functions, macros such as all, a double — is
taken as true once every negation has been pushed down to the conditions it applies to, so an
unread part can only widen what the contract lets through. Three things follow. A condition
on another field that narrows this one narrows what E122 compares (this.w >= 1 && this.w <=
100 on the message is a range). A constraint between two inputs of one contract that the
contract does not keep — some request passes its validation, inside the inputs' ranges, and
breaks the constraint — is E123, with that request as the example and, for a .proto, the
(buf.validate.message).cel that would promise it as fix.text; JSON Schema has no way to
compare two fields, so there it has no fix on the contract's side. A row whose cells, each a
value the contract lets through, ask for a combination the contract's conditions never let
through — express above 5 kg where the contract says !this.express || this.weight_g <= 5000,
two members of one oneof both set — is W124.
A field the contract lets an object leave out can only be taken by an optional input (T?),
and the projection function reads a missing one — or a missing object on the way to it — as
none. In a JSON Schema that is a field not in required, and a required input read from one
is E122, since the function could not read it.
A .proto shape is read in the JSON form protojson gives it. A field is read under its
JSON name — json_name, or the lowerCamelCase of its name, so zone_code is zoneCode — or
under the name the .proto writes, which protojson's readers accept as well. A field protojson
leaves out is read as proto reads it: a number as 0, a string as "", a bool as false, a
repeated as no elements, an enum as its value numbered 0, and a message as one with every
field left out. The defaults arrive, then, and they are held to the input like any other value.
Under a message field that is not required, and in an optional field, Protovalidate
validates nothing while it is unset, so the default arrives whatever the rules on the field
say; an input that does not take it is E122, with (buf.validate.field).required = true as the
fix. An optional input (T?) reads an unset message or optional field as none instead — a
field without presence cannot be missing apart from its default. A date read from a string is
held to whether "" passes, since protojson leaves an empty string out and "" is not a date.
A contract says how a value travels, and the rule says what it means: an enum and a date arrive as strings, and money and a quantity as whole numbers in the unit the rule declares.
Five of the twelve targets generate the projection function — Python, TypeScript,
JavaScript, Ruby and PHP, where the caller's object is a plain map and needs no name. Go,
Swift, Java and Rust hold it as a type, and the only ways to name that type would be to
generate it (this tool makes no domain object model) or to follow the caller's own; SQL takes
a relation of flat columns, NumPy takes columns, and the Wasm ABI takes one JSON object of the
rule's own inputs. The path check applies to every target equally — it happens in check,
before anything is generated. rulec api lists the contracts, the path of every projected
input, and the function in each language that reads them, under projection.
4. inputs and outputs
inputs
dest : jp_prefecture
weight : mass[g] range >=1g <=40kg
total : money[JPY, incl_tax] range >=0JPY <=10_000_000JPY
member : member_kind
outputs
fee : money[JPY, incl_tax] round up(10JPY)
range — required on every numeric input and every derive
One declaration does three jobs.
- Overflow proof. The reachable interval of every intermediate value is computed from the declared ranges and steps, and must fit in int64 (E108).
- The universe of the completeness check. "Every input matches some row" means every input within these ranges.
- The entry guard of the generated code. A call outside the range returns an error instead of silently computing something.
The form is range followed by one or two bounds: range >=0JPY <=10_000_000JPY, range >=1g.
A derive whose declared range does not contain what it can actually reach is E112, and the
message states the interval to widen to. A rate input may leave range out: it is then
>=0% <=100%, and the guard enforces that, so a rate that can exceed 100% declares its range
like any other number. A table's numeric output column needs no range of its own — its cells
are its range.
contract_only marks an input that is only ever an entry check and appears in no table:
Without it, an input no table uses is W111.
range from koyomi — the days a koyomi date comes to
A date input can take its range from a date of a koyomi file instead of from bounds. koyomi computes the date on every input of its own range, so the set of days it comes to is known exactly, and the rule is checked over those days and no other:
What follows from names the date the way every language of ritsu names one: koyomi, the
file (a path from the rule's directory), date and the date's name. With payment_terms.cal
closing on the 20th and paying on the 10th of the next month, pay_day takes twelve days, the
10th of each month, and a table needs no row for the days between them:
table pick
policy unique
| pay_day | -> batch : run |
| <=2026-06-30 | first_half |
| >=2026-07-10 <=2026-12-10 | second_half |
| >=2027-01-01 | year_end |
Over every day from 2026-02-10 to 2027-01-10 this table leaves 2026-07-01 to 07-09 uncovered; over the payment days it is complete. The four jobs a range does all follow the set:
- Completeness, overlaps and unreachable rows are about the days in the set. A day of the set no row takes is E101 with that day as the example; a row that takes none of them is E102.
- The examples and the vectors use those days only. An example on another day is E019.
- The generated code refuses any other day at its door, in every backend.
- The certificate carries the days and where they come from — the koyomi file and its date
as the rule names them, and the file's SHA-256 — and both re-checkers (
tools/recheck.pyand the Lean one inproofs/) rule a box out when it holds none of the days.
The set is read through ritsu's port of dates, so the rule has to be checked with koyomi joined:
ritsu rulec check or ritsu check. The binary of rulec's own crate has no koyomi; there the
file is not checked over every day instead, and the run says so (E129, exit 2). A set that cannot be had — the file is not there, does not pass koyomi's
check, has no such date, or comes to no day — is E130, with what koyomi says. Only a date
input takes range from koyomi (E065); an output, a derive or a field of an element cannot
borrow its range from another file. The days are listed as a precondition in rulec api
("kind": "days"), and the page for people lists them beside the input.
round — required on every numeric output
Five modes, each pinned down for negative values:
| mode | direction | at grid 1 |
|---|---|---|
up |
away from zero | −4.2 → −5 |
down |
toward zero | −4.8 → −4 |
half_up |
an exact half goes away from zero | −4.5 → −5 |
half_down |
an exact half goes toward zero | 4.5 → 4, 4.6 → 5 |
half_even |
an exact half goes to the even neighbour | 2.5 → 2, 3.5 → 4 |
The value in parentheses is the grid: up(10JPY) rounds to a multiple of 10 yen. Rounding
is applied once per output, last. A missing one is E104; an output literal that is not a
multiple of the grid is E106.
5. derive
A linear combination of inputs, which can be used as a table column while still being a quantity.
The right-hand side may use inputs, +, -, and multiplication by a constant. range is
required and behaves exactly as it does for an input.
6. define
A named boolean or intermediate value. A boolean define may be used as a table column.
define bulk : bool = total >= 30_000JPY
define a_earlier : bool = a_due <= b_due
define rate_off : money[JPY, incl_tax] = list * rate
The condition of a boolean define must be one of exactly two shapes (E113):
- a unary test on one input or one derived value — that value compared with a constant;
- a comparison of two values of a type whose difference cannot be derived (two dates, for instance).
A direct comparison of two numbers is neither. Declare the difference as a derive and
compare that with a constant; the analysis is exact that way, and the message says so.
6.1 constraint
A relation between two inputs that the caller guarantees. It computes nothing; it says which combinations of inputs can happen.
The shape is constraint <input> <comparison> <input>, with one of <=, <, >=, >
(E017), an input on each side (E018), and both of a type that has an order — money, a
quantity, a rate, a number or a date. Several lines all hold at once, and A = B, when
it is ever wanted, is the two lines A <= B and A >= B.
Three things follow from one line.
- The completeness check stops demanding rows for combinations that cannot happen. A table that covers everything reachable is complete, and the gap E101 used to report — with a witness nobody could ever produce — is gone.
- A witness is one of the combinations that can happen. Every input the checks construct satisfies the constraints, so what a diagnostic hands back is a case somebody could really send.
- The generated code refuses a violating input at the door, with the constraint quoted, the way it refuses a number outside its range. The proof assumed the constraint, so the code has to insist on it.
The vectors follow the same line: rulec vectors never produces a combination a constraint
excludes, and an examples row that breaks one is an error (E019) rather than a case.
Writing - in a cell says "this column does not matter here". Before constraints it also
had to stand in for "this cannot happen", and the two read the same on the page. A constraint
is how the second one is said out loud.
6.2 elements and fold
A rule is one decision about one case. Sometimes the case carries a sequence — the rows
of a tariff sheet, the candidates a predicate left — and the answer comes from walking it.
elements declares what one element carries; 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
The fields of an element are declared exactly like inputs, and a table may use them as
columns; what differs is that the caller passes them once per element. The table's own
checks are unchanged — one element is one case, and completeness, overlap, units and
overflow are proved over it as they always were.
The arms:
| arm | what it does |
|---|---|
next |
leave this element, look at the next |
stop |
end the walk; the answer is what exhausted says |
stop with <value> |
end the walk with this answer |
take_unique <value> |
take this element's value; a second element that also takes is an error at run time |
take_first <value> |
take the first, ignore any later one |
keep_max <value> by <key> |
hold this element's value, replacing what is held when the key is larger |
empty -> <value> |
the answer when there are no elements. Required |
exhausted -> <value> |
the answer when the walk reached the end. Required; held is the value being held |
Four things are checked, and each of them is a loop somebody has written by hand and got wrong:
- the answer for an empty sequence is declared (E022);
- the answer for a walk that reached the end is declared (E023);
- every verdict the table can produce has an arm (E024), and an arm nothing can reach is named (W115);
take_uniqueortake_first— there is no baretake. Whether a second matching element is an error or is ignored is a decision, and the grammar makes it one (E021).
Why a fold does not cost the checks their decidability
The checks work because a cell narrows its own column and nothing else, so a row is a box in the input space and gaps and overlaps are arithmetic. An arbitrary loop would end that. A fold does not: the table is complete and unique, so every element lands on exactly one verdict, and the verdict's type is a finite enum. The walk is therefore a reduction of a string over a finite alphabet — a small automaton — and how many elements there are at run time does not change what can be said about it.
What a fold generates
rulec gen writes the walk in Python, TypeScript, JavaScript, Rust, Ruby, PHP, Go, Swift, Java and Wasm —
every target but SQL and NumPy, which are refused by name below.
The sequence is an argument like any other input — an array of objects on the wire (§10.2),
each element's fields integers in their canonical unit — and every field gets the same entry
guard an input gets. rulec test runs the generated walk over the vectors and holds it to the
reference evaluator, the same as for any rule.
SQL is refused by name. One query has nowhere to carry a value from row to row and stop
early. A window function or a recursive CTE can be made to look like a walk, but only by
giving up the 1:1 between a branch of the generated query and a row of the rule — which is the
reason the SQL backend exists. So rulec gen names SQL, skips it, and writes the other seven.
Writing an example of a walk
An example is a row of cells and a sequence does not fit in one, so the sequence is written once, under a name, and the cell names it:
sequence near
| row_zone | threshold | row_fee |
| kinki | 500JPY | 800JPY |
| kinki | 2000JPY | 1500JPY |
sequence no_rows
| row_zone | threshold | row_fee |
examples
| dest | total | fee_rows | -> fee |
| kinki | 5000JPY | near | 800JPY |
| kinki | 5000JPY | no_rows | 0JPY |
The columns of a sequence are the fields of elements, all of them, and every cell is a
value — a range or a - is how a table's cell is written, and this is one element as the
caller would really pass it (E026). A block with no rows is the empty sequence, which is a
case worth writing: it is the one a hand-written loop forgets.
The examples of a rule that walks a sequence must carry a column for it (E025), the cell must
name a sequence that exists (E027), and a sequence no example names is reported (W116).
Each example runs through the reference evaluator at rulec check like any other (E107), and
each one joins the generated vector suite.
An input with no answer
A sequence where take_unique matches twice is a contradiction: the reference evaluator has
no answer and the generated code raises. Such an input is still part of the suite — it goes to
vectors/<alias>.refused.jsonl, and rulec test requires every generated language to refuse
it. That is what makes the last fold transition covered rather than merely named.
6.3 count and sum
fold ends a walk with one answer. count and sum end it with a number, and the rule
goes on from there like any other.
The shape is count <name>(<alias>) over <sequence> where <column> = <value>, with range
(E028, E030). The column is one of one element — a field of elements, or a column a
per-element table produces — and its values have to be a closed set, a bool or an enum
(E029). A bool column needs no = <value>: where name_match counts the elements where it
is true.
A rule that counts runs in two phases, and which item belongs to which is derived rather than declared: an item is part of the walk exactly when it reads something that only one element has. So the table that classifies an element runs once per element, and everything that reads only the counts and the ordinary inputs runs once, after.
table row_of # the walk: it reads a field of an element
policy unique
| name_match | addr_match | -> hit : match_kind |
| true | true | same |
| true | false | diff |
| false | - | diff |
count hits over candidates where hit = same range >=0 <=100
table verdict_of # after the walk: it reads the count
policy unique
| hits | -> result : outcome |
| 0 | no_match |
| 1 | one |
| >=2 | several |
The range is required, and it says two things. It is the universe the completeness check quantifies over once the count is a column — without it the check would ask for a row covering a count of −1 — and it is the cap on the sequence: the generated code refuses a sequence longer than the smallest bound any count declares, the way it refuses a number outside its range. A count cannot leave the space the proof was made over.
sum
sum totals one column of the elements instead of counting them.
elements lines
amount : money[JPY] range >=0JPY <=100_000JPY
sum total over lines of amount range >=0JPY <=1_000_000JPY
The shape is sum <name>(<alias>) over <sequence> of <column>, with range. The column is
one of one element, the same as a count's, and it has to be a number — an amount, a
quantity, number or rate (E029). The total keeps that column's type, so total above is
money[JPY] and a table over it is written in yen.
The summed column has to be non-negative (range >=0…, E029). That is what lets the
running total move one way only: the walk refuses the moment it passes the declared maximum,
so one test at the end is a test everywhere, and the accumulator never leaves maximum plus
one element — which is what keeps E108's int64 claim true of a sequence whose length nothing
caps. To take a difference, sum two non-negative columns and subtract.
Nothing else accumulates. A fold's arms choose an element; a count adds one per element that passes a test; a sum adds one column. There is no average and no arm that carries a number forward: an average is a sum and a count divided, and the divisor is not a constant (§2.3).
A rule cannot have both a fold and a count or a sum (E031): they are two endings for
the same walk, and a fold may stop partway, which leaves the meaning of a total on that
walk undecided. Every target but SQL generates them, for the reason SQL gets no walk at all.
6.4 machine and scenario
A rule decides one call. Some rules are one step of something that goes on: an order that
is paid, shipped and delivered, an application that is filed, reviewed and decided, a
membership that moves up a tier each year. 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. machine says so:
machine order over step
carry state -> next_state
held amount_paid
initial received
final delivered, cancelled
never shipped after cancelled
once refund >0JPY
| line | what it says |
|---|---|
machine <name>(<alias>) over <table> |
the table whose rows decide the carried output: its rows are the transitions |
carry <input> -> <output> |
the output the caller passes back as that input on the next call. Both are one enum. Required |
held <input>, … |
inputs one case passes with the same value on every call, from its first to its last: the amount of an order, the class of the person who applied (E056 when one is not an input, or is the carried one) |
initial <state> |
the state a case starts in. Required |
final <state>, … |
the states a case ends in |
never <state>, … after <state>, … |
no sequence of calls reaches the first states once the case has been in one of the second |
once <output> <cell> |
in one case, at most one call answers an output the cell accepts: a refund paid, a point granted |
carry is the whole of what is new about the meaning. The generated function does not
change — it takes the state as an argument and answers the next one, and keeps nothing — so
a rule with a machine is still a pure function (DESIGN P3). What the section adds is claims
about every sequence of calls the caller can make, and rulec check proves them:
| check | what it finds | code |
|---|---|---|
| completeness of the table | a state and an event with no answer — what happens when a cancel request arrives after shipment? — including the calls that leave the state where it is | E101 |
| overlap | a state and an event with two answers | E105 |
| final states | a call that moves a case out of a final state |
E124 |
| finishing | a state a case can reach from which no final state can be reached |
E125 |
never |
a sequence of calls that reaches the first states after the second | E126 |
once |
a sequence of calls in which two calls answer what the cell accepts | E127 |
| reach | a state no sequence of calls reaches, and a row that applies only in such states | W125, W126 |
Without held, every input may take any value on every call, and a sequence that changes the
amount of an order halfway can come back as a counterexample nobody could send. With it, a
case keeps those inputs' values from its first call to its last, and the claims are about the
sequences that keep them: the check walks each world — each class the rule's own
boundaries cut the held inputs into — on its own. A row that applies only with a value a case reaching its state never has is
W126 then, with a note saying so.
A broken claim comes back with the shortest sequence of calls that breaks it, every call an
input the rule takes (witness.trace in the JSON, one line per call in the text):
error[E126]: A sequence of calls reaches shipped after cancelled
--> rules/order_lifecycle.rule:37 machine order
Calls (from received):
1. at received, event = cancel, amount_paid = 0JPY → cancelled (table step row 2)
2. at cancelled, event = pay, amount_paid = 0JPY → paid (table step row 10)
3. at paid, event = ship, amount_paid = 0JPY → shipped (table step row 4)
Why the claims stay decidable
The state is a finite enum, and every other input is cut by the rule's own boundaries into
finitely many classes — the cells rulec diff walks (§15.122). Each class is settled by an
input that realizes it, and what the rule answers there is a transition from the state the
class has to the state the rule answers. The claims are then searches over a finite graph.
The price is the lines this language does not have, and they are left out on purpose:
- no number is carried from one call to the next. A total so far — refunds paid, a balance — is kept by the caller and passed in, as it always was. Adding one up in the state would make it a counter, and whether a counter reaches a value is not decidable in general.
- one machine per rule, one carried state. Two machines running side by side is where message order and races live; that is what TLA+ and P are for.
- no calendar. "Within 14 days" is an input — the days elapsed, counted by the caller — compared with a constant, as every date comparison is.
once counts a call whose output the cell accepts. Where the output is read off an input or
a computed value, the value's own boundaries are cut at the cell's, so that one input stands
for its whole class; a claim that turns on a class no input was built for and none shown
impossible is reported as undecided (W127), never as holding. A space larger than the budget
is E128: --budget counts fifty region nodes per cell.
A held input is followed by the class its own column cuts it into. Every value of a class
allows the same calls as long as nothing else reads the input; when a computed column or a
constraint reads it too, one value may allow a call another value of its class does not. The
claims that nothing bad is reached still hold then, since the walk of a class takes in every
value's calls, but whether a case can always still reach a final state is reported as
undecided (W127), and so is a counterexample that could only be followed by changing the value
partway.
scenario
A scenario is the examples of a machine: a sequence of calls from the initial state, one
row per call, with what each call answers.
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 |
The carried input has no column: the first call starts in the initial state, and every
later one in the state the call before it answered. Every other input and every output has a
column (E055, E111). rulec check runs the calls in order through the reference evaluator; a
call that does not answer what its row says is E107, reported with the calls that led to it.
What a machine generates
The function is the one every rule gets. Beside it, each language with a module of its own gets the constants a caller needs to keep the state: where a case starts, and whether it has ended.
| language | initial | final states | has it ended |
|---|---|---|---|
| Python | INITIAL |
FINAL |
is_final(state) |
| NumPy | rule.machine["initial"] |
rule.machine["final"] |
— |
| TypeScript, JavaScript | INITIAL |
FINAL |
isFinal(state) |
| Rust | INITIAL |
FINAL |
is_final(state) |
| Ruby | INITIAL |
FINAL |
final?(state) |
| PHP | INITIAL |
FINAL_STATES |
is_final($state) |
| Go | Initial |
Final |
IsFinal(s) |
| Swift | initialState |
finalStates |
isFinal(_:) |
| Java | INITIAL |
FINAL |
isFinal(state) |
| SQL, Wasm | — | — | — |
final is a keyword in PHP whatever its case, and in Swift, hence the two other spellings.
The NumPy plan is data, so the state names are the wire form. A target with one door and no
module has no place for a constant; its caller reads the two off rulec api, which lists every
language's spelling under machine.constants.
The vector suite gets traces as well as single calls: for every transition a case can make
and every two that can follow one another, the shortest sequence of calls from the initial
state that ends with them, and every scenario. rulec test has each language's runner play
them — the state one call answers is handed to the next call as that language holds it —
and prints its constants first, so the traces hold the hand-over and the constants as well as
the answers (docs/formats.md).
7. Tables
table base
policy unique
| dest | weight | -> base : money[JPY, incl_tax] |
| remote | <=2000g | 1200JPY |
| remote | >2000g | 1800JPY |
| not: remote | <=2000g | 800JPY |
| not: remote | >2000g | 1100JPY |
The first row is the header. Left of -> are input columns, right of it output columns. A
column may name an input, a derive, a boolean or enum define, or an output of an earlier
table. An output column that introduces a new name declares its type there.
Policies
| policy | meaning |
|---|---|
unique (the default) |
no two rows may overlap. Reordering the rows cannot change the meaning |
first |
the earliest matching row wins |
There is no Any, Priority or Collect, and completeness cannot be waived: a table with a hole is E101 whichever policy it uses.
Row labels
A row may carry a label before its first bar:
| stated | amount | -> tax : money[JPY] |
exempt | true | <10_000JPY | 0JPY |
r3 | true | >=10_000JPY <=100_000JPY | 200JPY |
A label names the row wherever a name is needed — in an overrides line, in the trace a
generated function returns ({"table":"base","row":2,"label":"exempt"}), in a later version —
and it is unique within its table (E034). Rows without one are still counted by position, and
rulec fmt aligns the labels as a column of their own.
Tables that share an output
Several tables may define the same output: a main rule and its special cases, each transcribed
from its own source. Each then has exactly one output column (E045), and which takes
precedence is written on the table that wins, right after policy:
table reduced_rate
policy unique
overrides base
| reduced | stated | amount | -> tax |
| true | true | >100_000JPY <=500_000JPY | 200JPY |
overrides names tables declared above, or one labelled row of one (base:r3), and says that
every row of this table takes precedence over them. The exception is written after what it
excepts: a target that is missing or declared below is E035, one that defines a different
output is E036. The tables of one output are checked together — completeness over their
union (E101), every overlap either ordered by an overrides line or reported (E105 / W114),
and a row that the rows taking precedence over it cover entirely (E102). An overrides line
whose rows meet none of its target's is W117. The generated code tries the tables from the last
declared to the first and takes the first row that applies, and the trace names the table the
row was written in.
Clauses
A definition whose conditions do not line up as columns — a proviso, a main rule written as
one sentence — is a clause: one row, written as prose.
clause regular -> fee
when always
then base
clause free -> fee
when total >=3900JPY and member true
then 0JPY
overrides regular
The heading names the clause and the output it defines (an outputs name, an intermediate an
earlier table or clause introduced, or a new one with -> name : type). when is a list of
<column> <cell> joined by and, the cell being any of the seven kinds above, the column
anything a table's column may be; a clause with no condition writes when always (leaving the
line out is E046, for the reason a blank cell is E008). then holds what an output cell holds:
a literal or a name. overrides is the same line a table may carry. A clause is a table of one
row whose other columns are -: it is checked, evaluated and generated as one, fires in the
trace as {"table":"free","row":1}, and the page shows its condition and its value as written.
Applying another rule
A provision applied mutatis mutandis — "the rule of Article 20 applies, reading 'years of
service' as 'period in office'" — is an apply: another rule file, used once more with its
inputs bound to values of this rule.
apply retirement = "retirement_pay.rule" sha256:b58648ea2767ebbd # Source: 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 apply, the callee (a path relative to this file) and the digest of the
callee file, which rulec source pin writes and check holds the callee to (E040: a callee
that changed is looked at with rulec diff before the new digest is pasted). Under it, one
line per callee input binds it to an input, a derived value, a definition, a table or clause
output of this rule, or a literal — every input, exactly once (E041). The types agree (E042);
two enums are mapped with with, which covers every value of this rule's enum, values spelled
the same on both sides mapping by themselves. What this rule passes has to stay inside the
callee's declared ranges and satisfy its constraints (E043, proved by interval arithmetic and
never fixed by adding a row: the callee is another unit of approval). except leaves a table,
a clause or a labelled row (table:row) of the callee out; a hole that leaves in the main rule is
this rule's E101 to fill. The callee's outputs become definitions of this rule, under their
own names or renamed with ->, rounded as the callee declares and then, if one is an output
here, rounded once more as this rule declares.
The callee is expanded into this rule: its tables, clauses, derives and defines appear under
<apply>:<name> (retirement:schedule), which is how a clause of this rule takes precedence over
one of them (overrides retirement:reduction, defining retirement:allowance) and how the trace names a
row ({"table":"retirement:schedule","row":1,"label":"short"}). Rows of the callee this rule never
reaches — its ranges are usually narrower — are silent, and the page lists them under the
apply; a whole table none of whose rows is reached is W118. A callee that itself applies a
rule, walks a sequence, produces one of its own enums, or does not pass check cannot be
applied (E044). The callee's sources come along with its definitions, and the page draws its
tables from its own file, under a heading that says what was applied and how. Generated files
name the callee and its digest in their header, rulec api lists them under applies, and
rulec diff old@rev new reads the callee at the same revision as the rule.
The eight kinds of cell
| written | means |
|---|---|
- |
any value. A blank cell is a syntax error (E008): a blank cannot be told from a forgotten entry |
1200JPY 2000g true 2026-04-01 "abc" |
equality with a literal. A quantity must carry its unit |
basic, gold |
a set. Each element is a literal or a group name; on a column of numbers each is a value of its own (100, 200) |
not: basic |
the complement of a set |
<=2000g |
comparison. <=, >=, <, > |
>=1000JPY <20000JPY |
an interval — two comparisons side by side mean "and" |
starts_with "CH-" |
a prefix, on a string column. Two or more are separated by a comma |
none |
an optional that is absent |
A string column takes a prefix and nothing else (E110). Strings cannot be enumerated,
so equality and sets have no finite reading here — where the values can be listed, make it
an enum. A prefix can: the prefixes a column's cells name cut the strings into one class per
prefix, plus "under none of them", and that is all §6.2's compression asks of a column. So
completeness and overlap work on a string column exactly as they do on an enum, and the
witness for a gap is a string you can paste. The match is on the bytes: no case folding and no
Unicode normalization, so all eleven targets answer the same. (NumPy declines a table with a
string column, for the reason it declines a walk: the runtime there reads integer columns.)
A cell tests its own column only. There is no expression, no reference to another column, and no function call inside a cell; that restriction is what makes a row a box and the completeness and overlap checks exact.
.. is a syntax error (E010). 0g..1000g does not say whether 1000g is included; a
comparison operator does.
An output cell holds a literal or the name of a value declared above (an input, a derive or
a define). It never holds an expression.
8. result
Assembles the first output when it is not simply looked up from a table.
result is sugar for the first output and reaches no other. Every output — the first one
included — is otherwise taken from the binding of its own name: a define or a table output
column called fee is what the output fee returns. Naming a later output in a result is
E015; a second result line is E016.
Operators, from loosest to tightest: comparison (<= >= < > =), then + -, then * /.
Parentheses group. The functions are min(a, b), max(a, b) and allocate(t, c, s), and the
five rounding modes may also be called as functions: down(x, 1JPY), up(x, 10JPY),
half_up(x, 1JPY), half_down(x, 1JPY), half_even(x, 1JPY). There are no others, and each
takes the number of arguments written here: anything else is E118.
allocate — one line's share of an amount
constraint before <= upto
constraint upto <= base
derive to_before : money[JPY] = allocate(total_off, before, base) range >=0JPY <=1_000_000JPY
derive to_upto : money[JPY] = allocate(total_off, upto, base) range >=0JPY <=1_000_000JPY
result share = to_upto - to_before
allocate(<amount>, <running total>, <whole>) is <amount> × <running total> ÷ <whole>
rounded down to a whole unit. It is the one place a rule may divide by something that is
not a constant, and it is allowed because of what it is for: handing an amount out over a
run of lines in the ratio of their prices.
The subtraction above is the whole point. Each line is given the share up to it minus the
share up to the line before, so the remainders telescope: the parts add up to the amount
exactly, with nothing left over and nothing conjured, and the line that carries the odd yen
is the last one. proofs/ states and proves that (runTotal_exact), which is what makes it
a property of the rule rather than a thing the examples happen to show.
What it asks for, all of it E117: three names with declared ranges, an amount and a
running total that cannot be negative, a positive whole, and a constraint saying the
running total never passes the whole. The last one is not decoration — without it a share
could exceed the amount being handed out, and the interval E108 is proved against would be
the product of two ranges rather than the amount. Chains count: two constraint lines that
meet in the middle say what a single one would.
One call decides one line. The loop stays with the caller, as everything else here does.
There is no loop and no recursion.
9. 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 a row that does not hold is E107, reported with the rows that fired.
Every output must have a column (E111). With two or more outputs, writing -> before the
later output columns is optional; rulec fmt folds it to the canonical form.
A rule may have more than one examples section — the published worked examples in one,
the cases a person added in another. Each has a header of its own, and every one runs.
Its cells are held to the types of the columns they sit under, exactly as a table's are: a
heading that names nothing is E012, a value that is not one of the column's is E012, and a
literal the column cannot hold — 1lb under mass[g], a bare number where a unit is
required, an expected 800kg under a money[JPY] output — is E103. An expected value that
cannot be read would otherwise leave nothing to hold the rule to.
An example naming an enum value is not a row for it: W111 still asks which values no table names.
10. What cannot be written
- Nested objects (
order.shipping.prefecture). Flatten at the boundary and pass the scalar in. - Collections and iteration. A rule is one decision; the order and the repetition belong to the caller.
- Date arithmetic. Comparison and range only.
- State kept between calls. A
machinemakes claims about the calls a caller makes one after another, and the state stays with the caller: the function is passed it and answers the next one (§6.4).
Allowing any of the first three would make the completeness and overlap checks unable to terminate; the fourth would take the replay of past records with it.
11. The canonical form
rulec fmt is the one and only formatter and it is idempotent. It
- aligns the columns of every table by East Asian width — a CJK or fullwidth character, and ℃ and ℉, are two columns — so Japanese lines up in a terminal and in any face that draws Japanese twice as wide as Latin,
- rewrites
→ ・ 、 , ≦ ≧and fullwidth digits to their ASCII forms, - folds the
->of the second and later output columns ofexamples, - indents the lines under
machineby two spaces and lines their values up in one column, - leaves the inside of a comment alone.
rulec fmt --check names the files that are not in canonical form and exits 1, which is how
it belongs in CI.
12. Reserved words
These cannot be used as a name (E009). A declaration whose name is one of them would be read by the line-oriented parser as the start of a section and silently dropped, which is why it is caught at parse time. An ASCII alias is not read by that parser, so it may be one; W121 says when a target language takes it badly.
An enum value never starts a line, so it may be any of them but eleven: not none
true false starts_with (the words of a cell), default (the mark after a value in its
enum line), after (which divides a never line), and empty exhausted by with
(the words of a fold arm). A state may be called initial, held or final.
| line heads | rule description import enum group inputs elements outputs derive define constraint table fold count sum sequence policy overrides clause source apply result machine scenario examples |
| modifiers | range round contract_only default |
| cells | not none starts_with true false |
| rounding | up down half_up half_down half_even |
| functions | min max allocate |
| fold arms | over next stop with take_unique take_first keep_max by empty exhausted held |
| count and sum | where of (and over, above) |
| clause body | when then always |
| apply body | except (and with, above) |
| machine body | carry initial final never after once (and over and held, above) |
step (inside rate[step 1%]), unique, first, the type words (money mass length
area volume duration temperature sound rate number bool date string), the
money attributes (incl_tax excl_tax) and std are
part of the vocabulary but are told apart by position, so they are not reserved as names.
A test holds this table to src/kw.rs, which is the single place the vocabulary is defined.