It occurs to me that I do not have a signature  online game. You might point
out that  it has been a decade  since I last played a game.  An author named
Frank  Sargeson observed  that you had to be removed from a topic  to see it
clearly...  Anyway, I do not view my complete unfamiliarity with games as an
obstruction  to me making a good one.
I  figure   a  game needs  to have state,  controls,  media,  a  clock   and
networking.  Since acl2 is my jam now, it should also be formally correct.
State is normally avoided in ACL2; being more simulation than an applicative
model  [in fact, state transition  is the opposite  to  being  applicative].
Having a model having state transitions  satisfies my ego.
Von Neumann bottlenecks are stobjs (single threaded objects) in acl2. Trendy
Haskell marketing calls them monads. 

(defstobj game-state (sparse-objects :type t :initially nil)
 (subject-cursor :type integer :initially 0)
 (object-cursor :type integer :initially 0) (chars-in :type t :initially nil))

(defun add-player (game-state name row col)
  (declare (xargs :stobjs (game-state)))
  (let ((new-sparse-objects
         (append (list (list name (cons 'row row) (cons 'col col)))
                 (sparse-objects game-state))))
    (update-sparse-objects new-sparse-objects game-state)))

Pretty much finished  amirite?  Lists of sparse (game) objects and character
inputs  for controls.  I also decided to have cursors to acheive  a for-each
for-each be part of the game state since they are basically about performing
state transitions  sequentially.   Viz for-each-for-each...   Coming up with
particular   theories  of less than the implied  O(nn) complexity  is a side
goal. 
My first hack at stateful input (without- lots of things) then. When you are
hell-bent   on introducing  stateful  input to acl2, it has a special  stobj
named state. I guess like Haskell's io monad.

(defun catch-char (state)
  (declare (xargs :stobjs (state) :verify-guards nil))
  (mv-let (ch state) (read-char$ *standard-ci* state) (mv ch state)))

(defun catch2global (state)
  (declare (xargs :stobjs (state) :verify-guards nil))
  (mv-let (ch state) (catch-char state) (f-put-global 'global-char ch state)))

(defun global2game (game-state state)
  (declare (xargs :stobjs (game-state state) :verify-guards nil))
  (let ((my-char (f-get-global 'global-char state)))
    (update-chars-in (list my-char) game-state)))

(defun getch (game-state state)
  (declare (xargs :stobjs (game-state state) :verify-guards nil))
  (pprogn (catch2global state)
   (let ((game-state (global2game game-state state)))
     (mv state game-state))))

Basically  in :program  (not :logic)  mode also with no "soft error"(-tuple)
handling, but I get a character into the st ate stobj and from state into my
game-state stobj.  Even without guard verification  it is a little  dance to
comply  with the special von Neumann  bottleneck  handling  (and the special
state stobj has more requirements  still).
---
I  saw  jns  has  a  game  engine in his history somwhere. Inb4 I plagiarize
-Capability machine architectures
-Text justification
-Game engine
-???
Hopefully I add a something!