GOL in GOL in HOL: Verified Circuits in Conway's Game of Life

Conway's Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete, and people have been building increasingly sophisticated constructions within GOL, such as 8-bit displays, Turing machines, and even an implementation of GOL itself. In this paper, we report on a project to build an implementation of GOL within GOL, via logic circuits, fully formally verified within the HOL4 theorem prover. This required a combination of interactive tactic proving, symbolic simulation, and semi-automated forward proof to assemble the components into an infinite circuit which can calculate the next step of the simulation while respecting signal propagation delays. The result is a verified "GOL in GOL compiler" which takes an initial GOL state and returns a mega-cell version of it that can be passed to off-the-shelf GOL simulators, such as Golly. We believe these techniques are also applicable to other cellular automata, as well as for hardware verification which takes into account both the physical configuration of components and wire delays.