What it proves

rulec check is the centre of the tool. Everything else — the code generation, the vectors, the replay — is downstream of it, and a rule that does not pass it does not generate.

$ rulec check rules/
note rules/yupack_base_fee.rule: 21 shadow pairs (21 structural, 0 equivalent, 0 needs review)
ok rules/yupack_base_fee.rule

Exit codes are 0 (notes only), 1 (errors), 2 (bad arguments or an unreadable file). Read the exit code, not whether the output looks empty.

The seven

A constraint narrows what completeness quantifies over: no row is demanded for a combination declared not to happen, and the generated code refuses one at the door instead. In a rule that walks a sequence, the same completeness check asks whether every verdict the table can produce has an arm in the fold (E024).

A derive is checked against the values it can actually come to, not against the range written on it. With amount from 1GBP to 100GBP and limit from 0GBP to 100GBP, excess = amount - limit comes to −99GBP up to 100GBP however wide its range is written. A row that asks excess only for more than 100GBP is reached by no input, and it is E102: the message marks >=-99GBP <=100GBP on the derive line, and widening the range does not make the row reachable. Completeness reads the same interval, so no row is demanded beyond it either, and deleting such a row never opens a gap. The interval takes the constraint lines in: under constraint paid <= billed, billed - paid never goes below zero. The values in it are read on the step they take, which can be finer than the whole units a cell is written in: commission = amount * 10% comes in tenths of a pound, so rows <=1GBP and >=2GBP leave 1.1GBP to no row, and completeness stops with it and with the amount that makes it, amount = 11.

A define that computes a number is read the same way. With score from 0 to 200, define share : rate = score / 200 comes to 0% up to 100%, so completeness demands no row for a share past 100%, and a row that asks only for one is E102. So is a row that asks a derive, beside the value a table above writes into another column, only for values the derive never comes to while the rows that write that value fire: when small is written only for an amount up to 50GBP, small beside an excess over the limit past 50GBP is reached by no input. The message names that row of the table above and what excess comes to there, >=-99GBP <=50GBP, and completeness asks no row for the combination either. A boolean define of one comparison is read for the truth value it takes: with made declared only up to the end of 2026, define reduced : bool = made <= 2027-03-31 is always true, so completeness asks no row for false, and a row that asks only for false is E102. The overlap checks read the same: two rows that meet only where no input reaches — the combination above, for one — are no E105, W105 or W114. The certificate gives the reason for each, and the two re-checkers work them out again rather than taking its word: the interval from the define's own expression, the truth value from its comparison, and the rows that write the value from the table above — and the values a table above writes into a column of numbers from what each of its rows writes.

A define whose expression only adds, subtracts and multiplies by constants is read as an equation as well. Each column may come to the value a row asks for while the columns never come to them together: with excess = added - limit, an excess of one or more over a limit of one or more is an added of two or more, so a row asking for that excess and that limit with an added of at most one is E102, and completeness asks no row for it. The certificate carries the equation as a fact of the define, and the two re-checkers build it again from the expression rather than taking the certificate's word for it.

In a rule that binds an enum to a .proto with import proto, completeness reaches across the contract. Every rulec check reads that file: a set that no longer agrees is E032, and once the sets agree, a value that no row names and no default marks is E033. Adding a value to an enum is a compatible change on the wire, so the tools that guard the contract let it through — this is the check that stops it from passing quietly through a table with a - row.

A rule whose inputs say where the caller's object holds them (shape and from) is held to that contract the same way. The path is resolved on every rulec check: one the contract does not have is E121, which says how far it got and which fields were there; so is one that goes on through a collection, since a path reads one value and each element has its own, and the message says how to read the collection instead (any, count, sum, or the elements as a sequence). A type that does not fit the input is E120; a contract nothing projects from is W122. None of this changes a check of the table — what comes out of a projection is a scalar input like any other — and what it stops is the glue between an application and a rule going stale in silence. How to write one is in Write a rule, and two worked rules are in Examples.

The contract also says which values can come from there, and that is held to the input. Protovalidate's rules on a .proto field and a schema's minimum, maxItems, enum and required are compared with the input's range, its enum and the range of a count: a value the contract lets through and the input refuses is E122 — a request the API itself accepted, refused at the door of the generated code. fix.text is the annotation to add to the contract. A row reached only by values the contract never lets through is W123. A proto3 number field with no rule lets 0 through, because that is what an unset field is, and that is the mismatch this finds most often. A message field that is not required may be left unset, and Protovalidate then validates nothing inside it: the value under it arrives as its default whatever its own rules say, so an input that refuses the default is E122 as well.

A contract also relates fields to each other — a CEL expression on a .proto message such as this.declared_jpy <= this.cover_jpy, a oneof, JSON Schema's allOf, anyOf, oneOf, not and if/then — and those conditions are read too. A constraint between two inputs of one contract that the contract does not keep is E123: some request passes the contract's validation and breaks the constraint, and the generated code refuses it at the door. The example is that request, and for a .proto fix.text is the (buf.validate.message).cel that would promise it. A row whose cells ask for a combination the contract never lets through — express above 5 kg where the contract caps express at 5 kg — is W124. What cannot be read of a condition (a remainder, a string function) is taken as true, so neither can miss. When the contract keeps everything the rule asks of these values, rulec certificate writes down why, case by case, and both re-checkers verify it — the Lean one on the theorem included_sound (How it is checked).

A rule that declares its documents with source and cites them with @source fragment is held to its copies: every cited fragment has a copy beside the rule and its digest pinned in the rule. No pin is E037, a pin that differs from the copy is E038 (naming the tables, clauses and rows that cite it), a missing copy is E039, a pin no citation uses is W119. check never reads the network: rulec source fetch brings the copies, rulec source pin writes the pins, and, for a statute, rulec source outdated asks e-Gov, the Japanese government's statute database, whether a later amendment changes the text of a cited fragment.

What is cited from a document is a table. For a tariff sheet or a company rule, @source table1 takes that table out of the document, writes it beside it, and holds the rule to that copy ever after (a sheet in a workbook, a table in a Word file, what it looks like in Markdown and CSV; for a PDF or a scan, hand an extractor to --via). That is where one more check comes in.

• E116 — an amount a row writes is nowhere in the copy it cites. This is the error no check of the table alone can reach: 1100JPY written as 1000JPY sits on the rounding grid, leaves no gap and overlaps nothing. Where the copy has a heading that says a word of the row (関東), the amount is looked for in that heading's row and column, so the amount of the next row, which is somewhere in the copy too, is caught as well.
• W120 — a number the copy states as a whole cell is used by no row, which is what a row that was never transcribed looks like. Completeness cannot see it: the inputs of a dropped row fall into one of the rows that remain.
• E119 — a boundary falls on the other side of itself from where the copy puts it: the copy says Under 18 and the row says <=18. Nothing else can see this either. The number 18 is still used, so W120 is quiet; move both of the rows that share the boundary and the table is still complete with no overlap; and exactly one input in the whole space changes hands.

A threshold cannot be compared as text — it is rewritten as it is transcribed (1,949,000円まで becomes <=1_949_000JPY) — but one thing survives the rewriting: which of the two bands the boundary value itself falls in. 60cm以下 and 60cmを超え agree that 60cm is in the band below, and so do <=60cm and >60cm, so a rule that writes a band from either end can still be held to the copy. The word is read beside the number (60cm以下, Under 18, Not over $11,925) or in a heading over its column (円以上, 円未満 — the shape a Japanese premium table takes). A boundary the copy words neither way, 18 to 20 or 60〜80, is left alone: naming the numbers that bound a band does not say which band holds them. The page for people quotes the copy under the table and adds two lines to what was verified: every amount in this table is a value the copy shows, and its boundaries fall on the side the copy puts them on.

A rule that applies another (apply, the way a statute applies one provision to another case with its terms read differently) is pinned to the applied rule's lines with the comments left out (E040), has to substitute every input of the applied rule (E041) with agreeing types (E042), and has to keep what it passes inside the applied rule's ranges and constraints (E043, with a value outside them as the example; for an input of an ordered enum held to a range, every value the binding can pass, read through with, has to be one the range lets in). A value that may be absent passed to an input of the applied rule that is not optional is E043 as well, and with none -> basic reads the absent value as one of the applied rule's values. A rule that cannot be applied — the applies go round, through it or through others, or it fails check — is E044; a rule that applies another, walks a sequence or produces an enum of its own can be applied. The applied rule's tables and clauses are expanded into the rule and checked with it; the rows this rule never reaches stay silent, and only a whole table none of whose rows is reached is W118.

A rule in which two or more tables define the same output — a main rule and the special case that says overrides over it, a clause written as one line of prose among them — runs the first three checks over those tables as one set. Completeness is judged over their union. An overlap passes when a precedence is written and stops as E105 when none is. A row the rows taking precedence cover entirely is E102, and an overrides line whose rows meet none of its target's is W117. The page for people says in one sentence which table is the exception to which.

A rule that is one step of a state machine (machine) is checked for what every sequence of calls can do as well. A call that moves a case out of a final state is E124; a state a case can reach and never finish from is E125; a sequence that reaches a never state after its after state is E126; two calls in one case that answer what a once cell accepts is E127. The case each of them carries is a sequence of calls from the initial state — the shortest that breaks the claim, each call an input the rule takes. A state no sequence reaches is W125, and a row that applies only in such states W126. A scenario, an example several calls long, runs as the examples do.

A machine can carry more than its state: a number with both ends of its range, a truth value or another enum, each with the value it starts at (initial days_left 0). The claims are then about the state together with those values, and two more are checked. A call that answers a carried number outside its range is E134; a sequence of calls that breaks an always line — always days_left >=1 <=7 when in_grace — is E135. While every value fits the budget one by one the walk is exact; past it, the numbers are cut into intervals, a sequence that breaks a claim there is looked for again among calls that really happen, and one that cannot be made again is W127, never a pass. The certificate lays these claims on the places a case can be, and the Lean re-checker proves that places closed under every call the rows allow hold every case, whether the walk took the values one by one or cut them into intervals. Where it took them one by one, the certificate also gives a path of calls that really happen from every place to a final state, and the Lean re-checker proves from it that every case can still finish.

Some values of an enum can be had only after others — a course after the courses it requires, a certification after the one below it. A prerequisites block says which, once for every value: start for the ones that need nothing, one <value> requires … line for each of the rest (, all, or any one), requires nothing "<reason>" for one no case can take, and ordered by <table> for a table whose answer — the year a course is taught in — never goes below a prerequisite's. The graph is finite, so the check walks it whole: a cycle is E136, a value that cannot be reached from start is E137, a value whose year comes before a prerequisite's is E138, and a prerequisite another one already needs is W130. The generated code answers what a value needs and whether it can be taken with what is held, in every language with a module. The certificate writes the block out as it is, both re-checkers check it again, and the Lean one proves the three claims: no cycle, every value but those no case can take reached from start, and the table's order kept along every edge.

An input can be drawn rather than chosen: random at the end of its line says that the caller draws it uniformly from its range, and a chances table claims how likely each answer is — for a store's lottery out of a campaign, | false | third | 5% |. The rows of a table are regions, so the check counts the points of each region exactly, however wide the range, and a claim the table does not keep is E133, with the combination and the chance it comes to: "With campaign = false, the chance of prize = third is 1/20 (5.0%)." A claim the count cannot settle within the budget is W129, never a pass. A fold can pick one element by weight with a drawn value (take_weighted <value> by <weight>), and what it picks is claimed and counted the same way. The generated code gives the chances as a function beside the rule's, in every target but SQL and Wasm; the certificate writes the counts out, both re-checkers count them again — working out from the rows what each region answers, and running a pick by weight at every draw — and the Lean one proves the claims hold; one the check left undecided (W129) is named rather than proved.

A rule can leave places for other files to add to: a value its terms put together (open stackable : money[USD] combine sum range >=0USD <=100USD), an enum, a table or a clause. A contribution file adds to them, and pins the shape of what it relies on (E040 says what moved). The rule is checked over the whole range it declares for an open value, so its own check holds whatever is added; a contribution whose terms take the value out of that range is E131, with the term and an input that does it, and a term that cannot move the value at all is W132. The certificate names each contribution with the digest of its file, and both re-checkers hold the range to what the terms come to together; the Lean one proves it. A value a contribution adds to an enum is asked for a row by every table that reads the enum (E101), and one that a table that is not open would decide in silence, by its - row or a comparing cell, is E033. The rule is checked alone and merged: its claims of chances hold whatever is added, and a contribution that moves a claimed chance is E133, naming the contribution's rows.

Every diagnostic writes its first line in the words of the business, always carries a concrete case, and states the fix down to the rewritten form.

Proved is not type-checked

Type checking says a value has the right shape: a member of the enum, an integer, the unit it claims. APIs and models that return typed values are common now, which makes the two easy to run together. A right shape says nothing about a right answer.

What rulec check proves is not a shape but a property of the table: every input in the declared range matches some row; no input matches two; every row can be reached; units never mix; every intermediate fits in int64. Those five are shown exhaustively — not sampled.

Why it can be exhaustive at all. A cell only ever tests its own column (<=2000g is the weight column, remote the destination column), so a row is the product of its columns' conditions — one box of the input space — and a numeric column only has to be cut where the table itself cuts it. The declared range therefore falls into a finite number of boxes, and looking at all of them terminates. The cell language is kept narrow to keep that true. Nothing is waved through when it does not terminate either: over the budget, E109 stops.

Four things it does not prove, and they are kept beside the word:

1. That the table matches reality. What is proved is what can be said about the table as written. Cite the document a table was transcribed from (@source table1) and an amount that disagrees with the copy does fail (E116, W120) — but even then what is shown is agreement with the copy, not with the world. With no citation, transcribe the tariff wrong and everything stays green
2. That the generated code answers like the table. That is a test: cases built from the boundaries run through the reference evaluator and every generated language, compared byte for byte. Strong evidence, not an equivalence proof
3. The row pairs W114 could not settle. Those move to a guard at run time — so "the rows do not overlap" is not always provable, and the pairs where it was not are always named
4. That the checker itself is right. The five above come out of rulec's own implementation, and that implementation has not been proved correct. The evidence is 216 deliberately broken rules (tests/mutants/) each producing the diagnostic it should, the corpus rules — the transcriptions of published terms and statutes among them — passing on every commit, and the reference evaluator agreeing with twelve languages. Evidence, not proof

For the Rust, a second tool reads what was generated: gen writes proof harnesses for Kani, and over every input in the declared domain they hold that no table falls through, that the guard of (3) never fires, that nothing overflows an i64, and that the rows of each unique table cover the domain exactly once. It shares no code with the checker above, so agreement is two unrelated tools saying the same thing, and disagreement comes back with the input that shows it (generate).

The evidence can be handed over, and the checks behind it are proved. rulec certificate writes out what the five proofs rest on — the tree that tiles the input space, the axis each pair of rows of a unique table parts on, a point that reaches every row with the values behind it, and the interval and the type of every computed value — together with where each cell stands in your file, down to the byte, and what stands there. Two programs re-check it: tools/recheck.py, one dependency-free file, and the program proofs/ builds, a Lean 4 development in which the meaning of a table, the checks, and the theorems that each check settles its claim are all written down and machine-checked. That moves what (4) asks you to take on trust from 42,000 lines of Rust to a few hundred lines of checking whose soundness is proved — plus the reading of the document itself, which is not. It does not remove (4): whether the tool produces a right certificate is still evidence, the declared ranges and types and constraints in it are its own word, and some things are named in a run rather than proved — a pair of rows the axes do not part, and a claim of chances the check left undecided, among them. Both programs end by saying which. See formats for the document, its limits, and both re-checkers.

Reading a diagnostic

error[E101]: Completeness gap: some input matches no row
  --> rules/parcel_rate.rule:30 table base_rate
   |
30 | table base_rate
   |       ^^^^^^^^^ the input space is not fully covered
   |
 An input that matches no row: dest = overseas, size = small, weight = 1lb
 An input producing this example: dest = overseas, girth = 23, signature = true, weight = 1
 hint: add a row that matches this input.
 The shape of the row to add: `| overseas | small | 1lb | 6USD |`. Its output values are copied
 from the first row to give a shape that parses; they are not the right amounts. …

The witness is the part to reason about. dest = overseas, size = small, weight = 1lb is not an illustration — it is an input the checker constructed, and it is the sentence you hand to whoever knows the answer. size is a value the rule works out from the girth, so the line under it gives the values a caller sends to get there.

--terse, when there are many

$ rulec check rules/ --terse
error[E101]: Completeness gap: some input matches no row
  --> rules/parcel_rate.rule:30 table base_rate
  witness: dest = overseas, size = small, weight = 1
note rules/parcel_rate.rule: 3 shadow pairs (3 structural, 0 equivalent, 0 needs review)
details: rulec explain <code>

Heading, position, witness. The pointer to the rest is printed once, at the end of the run.

--format json, when a program is reading

The same finding as data. The prose is still there, but nothing downstream has to take a sentence apart:

$ rulec check rules/parcel_rate.rule --format json | jq -c 'select(.code=="E101") | {table:.where.table, witness:.witness.inputs, fix:.fix}'
{"table":"base_rate","witness":{"dest":"overseas","size":"small","weight":1},"fix":{"kind":"add_row","text":"| overseas | small | 1lb | 6USD |"}}

where says which table and row, witness is an assignment of values in the canonical unit, rows names every row that takes part, and fix carries the rewritten form ready to paste. witness and fix do not change with --lang — only fields whose names say prose do. The full shape is in Formats.

Looking a code up

Every code has an entry: when it appears, how to fix it down to the rewritten form, the smallest .rule that reproduces it, and the codes next to it.

$ rulec explain E101
error[E101]: Completeness gap: some input matches no row

When
  The union of the rows does not cover the declared input space. …

Fix
  Add a row that matches the witness. If a new enum value caused it, …

Smallest reproduction
  rule t(t) v1

  enum k(k) = a(a) | b(b) | c(c)
  …

Related codes: E102 E105 W111

rulec explain --all --format markdown prints every one of them — and is exactly what Diagnostics on this site is built from. Every reproduction in it is run by the test suite, so an example cannot rot into something that reads well and is no longer true.

Only what is new

$ rulec check rules/ --diff-base origin/main

Findings that were already present at that revision are hidden, and the count of what was hidden is printed. Pairs are matched on the canonical form of their cells rather than on line numbers, so inserting one row does not make everything look new.

That is what makes warnings usable in CI: a table can carry an intended policy first shadowing for years without drowning the one overlap this change introduced.

When it cannot prove something

It says so. It does not approximate and pass.

• E109 — the check ran out of its node budget, so completeness was not proved. Split the table or raise --budget (rulec check and ritsu check both take it); nothing is assumed.
• W114 — two rows of a unique table might overlap, and the checker could neither construct an input that proves it nor prove that none exists. It warns, and the generated code carries a guard that returns an error rather than silently picking the earlier row. If that guard ever fires, the overlap was real. Two derived values that share an input, and the thresholds inside a boolean definition, no longer land here: those are decided by eliminating one variable at a time. What is left is what that cannot decide because it works over the rationals — a pair kept apart only by the values being whole.
• W128 — a row asks a computed column (a derive, a define) for values, and no input was found that reaches it, nor was it shown that none does. It warns rather than passing the row as reached: ok would otherwise read as "every row is reached". An example that reaches the row decides it, and the warning goes. If no input does, delete the row — unless completeness then asks for it back, which means the combination cannot be shown impossible either, and the row can stay.

Over the days a koyomi date comes to

A date input can take its range from a date of a koyomi file: pay_day : date range from koyomi "payment_terms.cal" date payment. koyomi computes the date on every input of its own range, so the days it comes to are known exactly, and the seven checks run over those days and no other: a table needs no row for the days between two payment days, a payment day no row takes is E101 with that day as the example, and a row that takes none of them is E102. The generated code refuses any other day at its door, and the certificate carries the days with the koyomi file's SHA-256. The days are read through ritsu, with koyomi joined (ritsu rulec check, ritsu check); a rulec with no koyomi does not check the rule over every day instead, and says so (E129). See the reference.

An input that may be missing

An optional input (T?) takes one value more than the type it wraps: none at all, which the cell none tests. Completeness asks for a row for it and for the whole declared range beside it. A date declared as due : date? range >=2026-01-01 <=2026-12-31, with the one row <2026-07-01, stops with due = none, and once a none row is written, with due = 2026-07-01. A comparison, a literal and a set of values match only a value that is there, while - and not: take the absent value too, so a none row meets either of them (E105). The generated code checks a value that is there against the range and the step of the type it wraps, and lets the absent value through to its row. See the reference.

An answer that may be missing

An output may be optional too. A row that answers no value writes none, and every other row a value of the type the output wraps, read in that type: 439USDc under money[USDc]?, rounded as any amount is (round down(1USDc); E104 without it). none under an output that is not optional is E103. A table that reads an optional column is asked for a row for none wherever a table above can write it or pass on an input that has none (E101). The generated code answers no value the way its language writes one: None, null, nil, NULL.

The range an answer stays in

An output may write a range after its rounding: share : money[JPY] round down(1JPY) range >=0JPY <=1_000_000JPY. The checker holds it to what the output can come to: the cells of the rows that decide it, or what its result reaches over the inputs' ranges and the constraint lines. A range that leaves out an answer the rule can give is E140, and the message gives the range to widen it to. A range on an output that reads an input with no range cannot be checked, and is E140 too. A share taken as the difference of two allocate calls, at running totals the constraints put in order, is read as never below zero and never above the amount handed out (the example). The range is then the answer's wherever an input's range is said: the certificate, rulec schema and rulec api, the page for people, and ritsu's port, through which the other languages read the answer. With none written, the output still has one range, and every one of them but the page says it: what decides the output, put out to the grid it rounds to. The certificate's two re-checkers hold the range, written or not, to what the output answers once rounded, and rulec diff lists a range that moved among the declarations that changed. See the reference.

Showing it to people

$ rulec doc rules/yupack_base_fee.rule > fees.md

A .rule is already almost markdown, so transcribing its syntax is worth nothing. What doc adds is the facts the checker knows that the text does not show: that a group of six values and its complement of 41 really do cover all 47, which rows shadow which, where a rounding was assumed rather than sourced.

This is what rulec doc writes (excerpt; --lang ja asks for Japanese).

## Groups

A group is a named subset of an enum. One word written in a table cell stands for all the values below.

- **kinki** (6 values) — Shiga, Kyoto, Osaka, Hyogo, Nara, Wakayama
- **cs** (9 values) — Tottori, Shimane, Okayama, Hiroshima, Yamaguchi, Tokushima, Kagawa, Ehime, Kochi
- **okinawa** (1 value) — Okinawa
…

These 6 groups partition the 47 values of jp_prefecture exactly (counted from the declarations by this rendering).

## Table fee_table (policy unique)

Source: Japan Post, base fee table (Tokyo)

| Column | Source |
|---|---|
| dest | Input |
| size | Output of table size_of |
| → fee | Output of this rule |
…

Write # Source: Japan Post, base fee table (Tokyo) at the end of a row or of the table line, and those words appear in the document too. The reader's job turns from "read the whole table again" into "compare this row with that cell".

A page a reader can try a case on

$ rulec doc rules/parcel_rate.rule --format html > parcel_rate.html

--format html renders the same document as one HTML page, laid out as a board. The form is on the left; the middle holds one card per decider — one table, one derive, one define — with that table itself inside the card. A reader types a case: the row that fired lights up inside the card it belongs to, the card says which row that was, the answer appears on the card that produced it, and the line the generated code would write to a log is shown as it is. The example buttons fill in the rule's own verified examples. An input that may have no value takes none from the top of its list, or an empty field, and an answer with no value reads none. The page is drawn light or dark, as the reader's browser is set.

Selecting a card opens a dock below it: where that table's columns come from, and what rulec check verified about it. Only the selected card carries colour, so which one you are reading is never in doubt.

What runs in the page is the generated JavaScript itself, so the page says nothing the code does not. The case and the card both stay in the page's address (?weight=5&girth=40&dest=canada&…#t-base_rate), so "look at this table on this case" is a link.

There is one prohibition. It writes no sentence that is not in the checker's output — every line traces back to the source or to a check result, and the two are named apart ("rulec check confirmed" versus "this rendering counted it from the declarations"). It is never committed: CI renders it and pastes it into the PR, because a stale rendering that still looks authoritative is the danger it was designed against.

All the diagnostic codes Generate and call

Showing it to the customer

$ rulec doc rules/yupack_base_fee.rule --audience customer > fee-guide.md

The same rule as the article a help centre publishes. Aliases, declared ranges and diagnostic codes are left out; what is added is the case on either side of every threshold, taken from the boundary-pair vectors, so a reader — or a model reading a retrieved page — is never left to decide what <=60cm means for 61cm.

## At the thresholds

How the answer changes on either side of a threshold.

- girth 60cm → fee 1410JPY; 61cm → fee 1710JPY (dest Hokkaido, weight 1g)
- girth 80cm → fee 1710JPY; 81cm → fee 2020JPY (dest Hokkaido, weight 1g)
…

This page is one layer. How it is checked is the map of all of them — what each one reaches, and where each one stops.