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

TL;DR

This paper addresses the challenge of formally verifying a self-hosting circuit within Conway's Game of Life (GOL) that simulates GOL itself. The authors formalize GOL rules and IO semantics, develop a modular GOL-IO framework, and implement gates based on Carlini's designs, culminating in a verified 21×21 mega-cell tiling that computes the GOL step across an infinite grid under a clocked LWSS signal. They prove key floodfill lemmas to guarantee non-interference between tiles and use symbolic evaluation and kernel automation in HOL4 to verify gate specifications and their composition into a complete GOL-in-GOL compiler. The result is a formally verified pipeline that, given an initial GOL state $S$, outputs a tiling of logic gates implementing the GOL step on the mega-cell lattice, with potential applicability to other cellular automata and hardware verification tasks involving wire delays. This work demonstrates that rigorous formal methods can underpin complex CA-based hardware-like architectures and sets the stage for broader verification of CA-based computation and self-replicating constructs.

Abstract

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.

Figures (5)

• Figure 1: Evolution of the glider (red, left) and the lightweight spaceship (LWSS) (blue, right).
• Figure 2: Collision between a glider and an LWSS which destroys the glider but leaves the LWSS intact.
• Figure 3: Illustration of some gates and their data flow behavior. Color key: ${\color{red}a}, {\color{blue}b}, {\color{yellow}\neg b}, {\color{purple}a\wedge b}$.
• Figure 4: A high-level circuit diagram representation of the mega-cell in our construction. There are AND (&), OR ($\vee$) and NOT ($\rhd\!\circ$) gates, half-adders (H-A), and all of it is acyclic except for the latch, highlighted in yellow, and the clock, which is a wire cycle forming the outer border of the cell. The clock uses slow wires (visualized as switchbacks) in order to ensure that the main logic can complete in time for the next clock cycle.
• Figure 5: Composition of an AND gate and a wire. In step $(a)\to(b)$ we merge the gate areas, resulting in an assembly with an internal input port overlapping an output, highlighted in yellow. In step $(b)\to(c)$ the matching pair is canceled.