Wormaly Werified

A formally verified worm (snake) game in ACL2.

The game worm from bsd-games is an old snake game for the terminal. Using ACL2 (A Computational Logic for Applicative Common Lisp) a reimplementation was created. Additionaly the correctness of some properties of the implementation are proven. The output looks mostly like the original. See the screenshot:

 ACL2-Worm                      Score:   11
********************************************
*                                          *
*                                          *
*                                          *
*                                          *
*                                          *
*    o                                     *
*    ooo                                   *
*      ooooooooo@ 2                        *
*                                          *
*                                          *
*                                          *
*                                          *
*                                          *
*                                          *
********************************************

A review of the orginal game can be found at: K.Mandla. worm, worms, wtf and wump: bsd-games takes over. Inconsolation. 2014

Play

You need ACL2 8.6+ built with SBCL, make and a (POSIX) termial to run the game. The code is available at: gitlab.com/tobiasrautenkranz/acl2-worm

You can build and run it with:

make worm && ./worm

To navigate use the VI keys hjkl or the cursor keys. Press q to quit. Eat the food (numbers) to grow and increase your score and do not hit the wall or yourself.

Implementation

This verification mostly concerns the implementation details regarding correct usage of defined functions domain (guard verified, something like types) and the functions termination. The game loop should not terminate without a win or loss condition having been reached. By using a large number like (expt 10 100) for the loop count we work around this.

Terminal

Most implementation challenges solved were of a technical nature regarding the terminal input and output. Some required functions like force-output$ or read-char-no-hang$ had to be implemented first in raw Lisp (terminal/io.lisp terminal/io-raw.lsp). Some of these functions use SBCL sb-posix:termios extension and thus are not portable. Thus it will only work with SBCL. These requirements also mean, that it can not be run directly from the REPL, but a saved image must be used.

Usage of the built-in io functions like princ$ requires a channel to be passed down to the function. Thus the entry point will be:

(start-game *standard-ci* *standard-co* state)

that is passing the standard input and output channels, which are streams in raw Lisp as arguments. Reading or writing to them will always keep the channels open (unlike CL streams). But since we pass these channels as arguments, the guards require that they are open (e.g. open-output-channel-p) when passed.

(defun print-csi (channel state)
  "Prints ANSI Control Sequence Introducer (CSI) to CHANNEL"
  (declare (xargs :stobjs state
                  :guard (and (state-p state)
                              (symbolp channel)
                              (open-output-channel-p
                               channel :character state))))
  (pprogn
   (princ$ *esc* channel state)
   (princ$ "[" channel state)))

This proof step (guard-verification) required some work to get to succeed and might not be very clear or efficient. There are no bivalent channels in ACL2. Therefore both the input and output channel must be passed a argument.

A confusing problem was the -p1 variants. For the channel and state predicates like open-output-channel-p and state-p there are lower-level equivalents open-output-channel-p1 and state-p1. These are only needed to implement the raw Lisp io functions but can appear in failed proofs even though they will have nothing to do with the proof failure.¹

To simplify things and since the *standard-ci* channel does not work with some terminal io function the raw functions use the Common Lisp stream *terminal-io* and have no argument for the channel.²

Food placement

The pseudo random placement of the food (numbers) is set to avoid the worm. Thus we need to ensure that there are empty places available. This is enforced by the guard for the food placement function having (not (win-p game)).

The win condition is that there is at most one place free. The worm is implemented as list of coordinates. Finding a free place involves generating a list of all (linear) board coordinates. Then the worm coordinates are removed from this list and one of the remaining elements is randomly selected. Thus the proof involves showing that removing the elements of a list of numbers (the worm) from the elements of list of unique numbers (the board) will still contain some elements when the removed list length is smaller than the other.

Limitations & Differences

The automatic movement in the original is quite a bit slower. It was increased to make it a bit more difficult. Also manually moving the worm by pressing the direction key corresponding to its current direction is not supported.

Besides the guard verification not much is proven. Like the terminal IO or also the game logic, though the logic is quite small and probably difficult to verify. A little of the logic verification was done in theorems.lisp.

The mix of built-in IO functions with raw List ones complicates things substantially without any correctness improvements. Implementing the IO in raw Lisp would be substantially easier. One might also think about abstracting the output so that properties about it could also be proven.

The style of the code is more oriented on Common Lisp instead of ACL2. The functions and theorems could probably be cleaned up and simplified.

Keep growing!

🐛