Method

Two checkers, because a type cannot count.

The compiler guards the shape of a claim. It has nothing to say about whether the numbers add up — a basket can be perfectly well-typed and still be wrong by two hundred SOL. So the arithmetic is tested separately, on its own.

§1   The shape — check-sportula.mjs

6 / 6

Each cheat is written out as real TypeScript and handed to the compiler. No as and no @ts-expect-error anywhere: both suppress the exact error the case exists to provoke, which turns a proof into a decoration.

1  CLOSED cannot be written without the seal

The report is finished, so call it closed. Nothing checked that it adds up.

2  the seal cannot be forged by hand

Both halves of the arithmetic typed out — except the symbol, which no other file can name.

3  close()'s result cannot be used without deciding what it is

It returns a seal OR an objection. Dropping it straight into the basket is refused.

4  money that moved cannot be claimed without the transaction

“We distributed it.” Which transaction? This is the shape of every payout figure that is really a row.

5  a residue cannot be named and then abandoned

207.74 SOL, labelled and left. The exact hole this project exists to close.

6  CONTROL: a basket that genuinely balances does compile

The case that must PASS. Without it, a suite where everything fails looks identical to one that works.

§2   The sum — check-arithmetic.mjs

10 / 10

01exactly balanced → sealed
02one lamport short → refused, difference +1
03one lamport over → refused, difference −1
04a negative allocation → refused before anything is summed
05a blank reason → refused
06claims to have moved with no signature → refused
07no allocations at all → refused
08RESERVED is not asked for a signature
09the dissected launchpad's own figures → UNBALANCED by 207.74 SOL
10closed honestly, once the remainder is named → CLOSED

The last two matter most. They feed the dissected launchpad’s own published totals into this rule, and it returns UNBALANCED by exactly the figure their site never names. The rule reproduces the finding rather than being decorated with it.

§3   Why there is a control case

Two suites in this workspace have already been green while testing nothing. In one, every “rejection” was really a bad import path. In another, all six cases failed with empty compiler output because the runner could not spawn the compiler at all on Windows.

Five green refusals look identical whether the rule works or the compiler never started. The control is the only thing that can tell those apart — and a rejection is only counted when the error is not a module-resolution error and mentions the type the case exists to defend.

§4   What this does not claim

as unknown as Closed defeats this, as it defeats every type in TypeScript. The rule is not a sandbox and this page will not pretend otherwise.

What it closes is the accidental path, and the convenient one — the second being the one that actually happens, on the afternoon somebody needs a report to balance.