# TinyChess

Chess cut down until the whole of it fits inside a proof: a four by four board,
three pawns and a king a side, and one sentence the build has to keep.

    white cannot win on the first turn

That sentence is not a test. It is a law, and the compiler will not produce a
game that breaks it.

## The opening position

Black at the top, white at the bottom. Both back ranks are full and the kings
stand on different files, so neither side begins in opposition and every pawn
has somewhere to go.

|   | a | b | c | d |   | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| **4** | ♟ | ♟ | ♚ | ♟ | | 12 | 13 | 14 | 15 |
| **3** | · | · | · | · | | 8 | 9 | 10 | 11 |
| **2** | · | · | · | · | | 4 | 5 | 6 | 7 |
| **1** | ♙ | ♔ | ♙ | ♙ | | 0 | 1 | 2 | 3 |

Squares are numbers, which is what lets the counterexample search in the editor
walk them. `file` is the square mod four and `rank` is the square div four,
both written by structural recursion rather than by arithmetic, because the
checker evaluates a natural one successor at a time and these stay under
sixteen.

## The four files

**`chess.bend`** is the geometry: how a king, a pawn, a queen and a knight step
on an empty board. `king_step`, `queen_line`, `pawn_push`, `pawn_capture`,
`knight_step`, each a `Bool` over two squares. Nothing here knows what a
position is.

**`game.bend`** is the game: what stands where, what a capture is, lines of
sight, when a king is attacked, and when a side is mated or stalemated. It is
computable and has no holes, so the checker can settle a question about a
position by running it rather than by being argued with.

Sizes are the point of every loop in it. Sixteen squares and eight pieces, so a
scan is sixteen steps, an attack test is sixteen scans, and the whole "can white
win at once" question is a few tens of thousands of steps.

**`LAWS.bend`** is the laws, in three parts: movement, the rules in general,
and the one about the opening. It states them and proves nothing.

**`PROOF.bend`** imports it and fills each law with a def of the same name,
`def Laws.white_cannot_win_on_the_first_turn()` for `law
white_cannot_win_on_the_first_turn`. `bend PROOF.bend` is the gate.

## What is proved, and what is not

    bend PROOF.bend
    # Error: 7 TODOs found.
    # The code is incomplete, and not a valid proof yet.

**`white_cannot_win_on_the_first_turn` is proved.** It is not a claim about
every position, it is a claim about one, so it needs no induction. The checker
plays every first move white has and every reply black has, finds no mate, and
the proof is `{==}`. It takes about a tenth of a second.

It is stated as "the search for a mating first move comes back empty", not as a
boolean, because a boolean can only say something is wrong. A move says what.
When the law breaks the checker prints `game.Step{2n, 6n}` against the empty
move it was promised, which reads c1 to c2, and hands you the refutation.

Three more facts about the experiment are proved the same way, and together
they are the point of it: a queen for each side keeps the law, a queen for
white alone destroys it, and a knight for white alone does not.

**The seven that remain are open**, for two different reasons worth keeping
apart.

Four are about movement and quantify over every natural number, not just the
sixteen squares. The search in the editor walks all sixteen and reports that it
checked every one of them, which is evidence and not a proof: past square
fifteen they hold because nothing is on the board, and that needs an argument.

Three are about every board there is, and there are more boards than can be
walked: that you never capture your own piece, that a legal move never leaves
your own king attacked, and that mate implies check. These need induction over
the rules. They are the bounties.

## The demo

Four positions. Swap one in for `initial()` in `position()`, at the top of
`LAWS.bend`, and run `bend PROOF.bend`. The three that hold stop at the same
seven TODOs as before, since the seven open laws share the file; the fourth
stops here:

| position | what happens |
| --- | --- |
| `initial()` | the law holds |
| `initial_with_queens()` | a queen each — the law still holds |
| `initial_with_queen()` | white's queen alone — **the file stops building** |
| `initial_with_knight()` | a knight for white alone — the law holds |

    Error:
    - expected : game.Step{2n, 6n}
    - observed : game.Step{16n, 16n}
    Location: LAWS.white_cannot_win_on_the_first_turn
    16 | def Laws.white_cannot_win_on_the_first_turn():
    17>|   {==}
    18 | 

The move is **Q c1–c2**. She steps one square up the file and the black king on
c4 has nowhere: b3, c3 and d3 are all hers, b4 and d4 are black's own pawns,
nothing can take her, and nothing reaches c3 to block, because a pawn only gets
to that square by capturing.

Give black a queen too and b4 is no longer a pawn: she drops into c3 and the
check is over. Give white a knight instead and there is no first move that even
gives check. It is not the extra material that breaks the law, it is the queen,
and only when black has no answer to her.

Q c1–c3 is also check, and is not mate — the king takes her, because nothing of
white's defends c3. The file keeps that too, since it is the difference between
a check and a win.

## Two traps, already measured on this checker

**Squares must stay naturals.** The 32-bit operators, `(a + b : U32)`, wrap,
which is the wrong domain for this. A bare operator belongs to `Nat`.

**A broken law takes the game down with it.** `bend PROOF.bend -o game` refuses to
compile while any law is open, printing the same TODO count and writing
nothing, and it counts the whole import closure rather than what is reachable. That is the demo, but it also means there is no
playable board while the law is broken.

## Four things the checker insisted on

Worth knowing before filling anything in, because each one cost a rewrite.

- A `match` must scrutinise a parameter, never a computed value. Give it its
  own definition and pass the value in.
- Matches must follow binder order, and a helper must be defined above its use.
- `1n + f(x)` was a 32-bit add when this was written; since 2.0.3 a bare
  operator is `Nat`'s and the 32-bit ones need `( … : U32)`. The files still
  bind a computed natural first and write `1n+r`.
- Pattern variables and plain bindings are linear. Used twice, they must be
  rebound with `+`, and a `+` binding needs a right-hand side the checker can
  infer, so a bare constructor has to be inlined instead.