(formal) game logic

(let ((my-game-state (list 'any 'modifiable 'sequence 'type))
  (loop :repeat 1000 :do
    (let* ((my-series (scan my-game-state))
       (choice (choose #Z(t t t) my-series))
       (update (#Mmy-formal-update-function choice)))
      (alter choice update))
    :finally (return list)))

acl2 < my-formal-update-function.lisp | grep Failure

(search
 "Failure"
 (uiop:run-program
  "acl2"
  :input #p"my-formal-update-function.lisp"
  :output :string))

(defun relu (x)
  "relu (x)
returns NIL if x is not a number,
0 if the x was negative,
and x otherwise."
  (and (acl2-numberp x)
       (if (minusp x) 0 x)))

If our input is not a number, we propagate NIL as is conventional instead.

ACL2 actually extends its subset of lisp with its own "recognizers" like acl2-numberp as well as thm, implies and things. At the moment, only for common lisp I am providing fake acl2 recognizer support like

(defun acl2-numberp (x) (numberp x))

the distinction is that while in practice we can pretend irrational numbers like π, e and √2 never happen, a logic has to be very careful of what it thinks it can do.

Let us put our definition in a file:

(with-open-file (out #p"relu.lisp" :direction :output
                   :if-exists :supersede)
  (print
   '(defun relu (x)
     "relu (x)
returns NIL if x is not a number,
0 if the x was negative,
and x otherwise."
     (and (acl2-numberp x)
      (if (minusp x) 0 x)))
   out))

following the convention of NIL for arguments outside its domain. acl2 functions must be total.

and feed it to acl2:

(uiop:run-program "acl2"
          :input #p"relu.lisp"
          :output :string)

we do have to constrain ourselves to acl2's extended subset of common lisp i.e. mostly no side effects. So our side effects will live in methods and commands, but our defuns can be pure. They can actually contain side effects using single threaded objects, but that is a kettle of fish for another day.

Let us try writing a theory to a file

(with-open-file (out #p"relu-thm.lisp"
             :direction :output :if-exists :supersede)
  (print
   '(thm
     (implies
      (and (equal x (1- y))
       (< c 0)
       (zerop (relu y))
       (not (zerop (relu (+ y c)))))
      (equal y 0)))
   out))

and throw both of those into ACL2:

(with-open-file (in-relu #p"relu.lisp")
  (with-open-file (in-thm #p"relu-thm.lisp")
    (uiop:run-program "acl2"
              :input (make-concatenated-stream
                  in-relu
                  in-thm)
              :output :string)))

GCL (GNU Common Lisp)  2.6.14 Fri Jan 13 10:47:56 AM EST 2023  ANSI    git: Version_2_6_14
Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl)
Binary License:  GPL due to GPL'ed components: (XGCL UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
Temporary directory for compiler files set to /tmp/
; Hons-Note: grew SBITS to 9648622; 0.19 seconds, [unknown] bytes.
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 + ACL2 Version 8.5                                                     +
 +   built January 16, 2023  08:05:44.                                  +
 + Copyright (C) 2022, Regents of the University of Texas.              +
 + ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and   +
 + you are welcome to redistribute it under certain conditions.  For    +
 + details, see the LICENSE file distributed with ACL2.                 +
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
System books directory "/usr/share/acl2-8.5dfsg/books/".
Type :help for help.
Type (quit) to quit completely out of ACL2.
ACL2 !>
Since RELU is non-recursive, its admission is trivial.  We observe
that the type of RELU is described by the theorem 
(OR (AND (RATIONALP (RELU X))
         (<= 0 (RELU X)))
    (COMPLEX-RATIONALP (RELU X))
    (EQUAL (RELU X) NIL)).
Summary
Form:  ( DEFUN RELU ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 RELU
ACL2 !>Goal'
Goal''
Q.E.D.
Summary
Form:  ( THM ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION RELU)
        (:DEFINITION ZEROP)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  189
Proof succeeded.
ACL2 !>Bye.

Ah, confusingly acl2 does not output the input it received. Well, it seems to work.

What if we make a mistake in our theorem? (Though it could also be that the theory is provable and acl2 just does not see how to do it.)

(with-open-file (out #p"bad-relu-thm.lisp"
             :direction :output :if-exists :supersede)
  (print
   '(thm
     (implies
      (and (equal x (1- y))
       ;;(< c 0)
       (zerop (relu y))
       (not (zerop (relu (+ y c)))))
      (equal y 0)))
   out))

and run that

(with-open-file (in-relu #p"relu.lisp")
  (with-open-file (in-thm #p"bad-relu-thm.lisp")
    (uiop:run-program "acl2"
              :input (make-concatenated-stream
                  in-relu
                  in-thm)
              :output :string)))

GCL (GNU Common Lisp)  2.6.14 Fri Jan 13 10:47:56 AM EST 2023  ANSI    git: Version_2_6_14
Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl)
Binary License:  GPL due to GPL'ed components: (XGCL UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
Temporary directory for compiler files set to /tmp/
; Hons-Note: grew SBITS to 9648622; 0.21 seconds, [unknown] bytes.
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 + ACL2 Version 8.5                                                     +
 +   built January 16, 2023  08:05:44.                                  +
 + Copyright (C) 2022, Regents of the University of Texas.              +
 + ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and   +
 + you are welcome to redistribute it under certain conditions.  For    +
 + details, see the LICENSE file distributed with ACL2.                 +
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
System books directory "/usr/share/acl2-8.5dfsg/books/".
Type :help for help.
Type (quit) to quit completely out of ACL2.
ACL2 !>
Since RELU is non-recursive, its admission is trivial.  We observe
that the type of RELU is described by the theorem 
(OR (AND (RATIONALP (RELU X))
         (<= 0 (RELU X)))
    (COMPLEX-RATIONALP (RELU X))
    (EQUAL (RELU X) NIL)).
Summary
Form:  ( DEFUN RELU ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 RELU
ACL2 !>Goal'
Goal''
([ A key checkpoint:
Goal''
(IMPLIES (AND (ACL2-NUMBERP Y)
              (< Y 0)
              (<= 0 (+ C Y)))
         (EQUAL (+ C Y) 0))
*1 (Goal'') is pushed for proof by induction.
])
No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.
Summary
Form:  ( THM ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION RELU)
        (:DEFINITION ZEROP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  239
---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal''
(IMPLIES (AND (ACL2-NUMBERP Y)
              (< Y 0)
              (<= 0 (+ C Y)))
         (EQUAL (+ C Y) 0))
ACL2 Error [Failure] in ( THM ...):  See :DOC failure.
******** FAILED ********
ACL2 !>Bye.

we can see failed theorems (like failed defuns) include "Failure" in their result.