Cryptol is a language tailored for cryptographic algorithms. Sudoku is a popular puzzle the reader is no-doubt already familiar with. We will offer no deep reason why anyone should try to solve Sudoku in Cryptol; other than the very fact that it'd be a shame if we couldn't!Needless to say, Cryptol has not been designed for encoding search algorithms. Nonetheless, some of the features of Cryptol and its associated toolset make it extremely suitable for expressing certain constraint satisfaction problems very concisely; and Sudoku very nicely falls into this category.
Representing the boardA Sudoku board can be represented in a variety of ways. We will pick the simplest: A sequence of 9 rows, each of which has 9 elements storing the digits. Each digit will require 4 bits; since they range from 1 to 9. So, a good Cryptol type for a board is:
In Cryptol-speak, this type simply represents a sequence of precisely 9 elements, each of which is a sequence of 9 elements themselves, each of which are 4-bit words. (Technically, the type  also represents a sequence of precisely 4 elements, each of which are bits. But it's easier to read that as 4-bit words. The type  and Bit are synonymous in Cryptol, and can be used interchangeably in all contexts.)