exhaustive-testing

A formally-verified Conway's Game of Life engine in which geometry may render the automaton's history but never author it. Exhaustive gates (512/512 local rules; 65,536/65,536 worlds vs an independent oracle) plus a machine-checked Idris2 constitution. A proven foundation — not yet a playable game.

A poor-man's prolog, in rust, for doing exhaustive testing. It lets you write singlethreaded code with calls to choose(n) that return a value in 0..n-1, and executes that code in all possible ways for all possible combinations of values for the chooses.

The NEC uPD77C25 as Nintendo shipped it across four microcodes. The DSP-2 is modelled with its commands proved rather than sampled: the tile conversion exhaustively over all 256 bits, the merge over every input it accepts, and the whole chip differentially against a reference validated on 71,970,987 recorded bytes.