chess.bend checks
raw source on the hub · import 0x6d15da24c6555ddee2181d043774a796/chess.bend as Chess
# TinyChess — the board and the way the pieces move. # # Four files by four ranks, kings and pawns and a queen. Everything in # this file is COMPUTABLE and has no holes: squares are numbers, the # step rules are Bools, and the checker can simply run them. That is # deliberate, because it is what lets the counterexample search in the # editor walk a claim and hand you the two squares that break it. # # What is NOT here is the game: occupancy, captures against a real # position, check, and mate. Those live in game.bend; the laws about them # are stated in LAWS.bend and proved, where they are proved, in PROOF.bend. # # Squares are 0..15, counting along the files first: # # a b c d # 4 12 13 14 15 rank 4, black's back rank # 3 8 9 10 11 # 2 4 5 6 7 # 1 0 1 2 3 rank 1, white's back rank # # so file = s mod 4 and rank = s div 4, and both are written out by # structural recursion rather than by arithmetic, because the checker # evaluates a Nat one successor at a time and these stay under sixteen.
1 import
import Base
Definitions
def nat_eq source · line 29 · raw
@a:Nat -> @b:Nat -> Bool
def nat_lt source · line 44 · raw
@a:Nat -> @b:Nat -> Bool
def gap source · line 60 · raw
@a:Nat -> @b:Nat -> Nat
the distance between two numbers, whichever way round they are
def file source · line 74 · raw
@s:Nat -> Nat
which file a square is on: 0 is the a-file, 3 is the d-file
def rank source · line 94 · raw
@s:Nat -> Nat
which rank a square is on: 0 is white's back rank, 3 is black's
def on_board source · line 115 · raw
@s:Nat -> Bool
a square is on the board when it is one of the sixteen
def king_step source · line 122 · raw
@+a:Nat -> @+b:Nat -> Bool
A king steps to a touching square: at most one file across, at most one rank up or down, and never onto the square it is already on.
def queen_line source · line 133 · raw
@+a:Nat -> @+b:Nat -> Bool
A queen steps along a rank, a file or a diagonal. The path being clear is a question about a position, not about geometry, so it is not asked here — it is one of the open claims.
def ahead source · line 144 · raw
@+white:Bool -> @+a:Nat -> @+b:Nat -> Bool
White pawns walk up the board, black pawns walk down. up says whether
b is exactly one rank ahead of a for the side given.
def pawn_push source · line 155 · raw
@+white:Bool -> @+a:Nat -> @+b:Nat -> Bool
A pawn's quiet move: one rank forward, same file. There is no double step on a board this short, and nowhere to promote to.
def pawn_capture source · line 162 · raw
@+white:Bool -> @+a:Nat -> @+b:Nat -> Bool
A pawn's capture: one rank forward, one file sideways. A pawn can only take this way, and can never take the piece directly in front of it.
def pawn_step source · line 168 · raw
@+white:Bool -> @+a:Nat -> @+b:Nat -> Bool
every way a pawn may move, capture or not
def knight_step source · line 173 · raw
@+a:Nat -> @+b:Nat -> Bool
A knight's leap: two squares one way and one the other, which is the only move on the board that does not care what stands between.