Pluscal algorithm to validate that the well-known Nim strategy is optimal

Nim.tla

--------------------------- MODULE Nim ---------------------------
EXTENDS TLC, Sequences, Integers, FiniteSets

CONSTANTS INITIAL_PILES, HUMAN_STARTS

(*
--algorithm Nim

\* An n-pile version of Nim with the rules:
\* * Take as much as you want, but only from one pile
\* * Player who takes the last stone on the board *loses*

\* See also https://en.wikipedia.org/wiki/Nim

\* This is set up as two players, "Human" and "Computer".
\* "Human" moves non-deterministically, trying all possible moves.
\* "Computer" moves according to an optimal strategy.

\* The model used with this should have ValidGame as an invariant,
\* and both OnlyValidChanges and ComputerWinsEventually as temporal
\* properties to check.

\* Suggested starting values:
\* INITIAL_PILES <- <<1, 3, 5, 7>>
\* HUMAN_STARTS <- TRUE

\* With those values, the computer always wins. Switch HUMAN_STARTS
\* to see how the human can beat the computer if the computer starts
\* from the 1,3,5,7 position.

variables
  piles = INITIAL_PILES;
  humanTurn = HUMAN_STARTS

define
  GameOver == \A p \in DOMAIN piles : piles[p] = 0
  \* player who took the last stone lost, so these next two are flipped when
  \* compared to other similar models
  HumanWins == GameOver /\ humanTurn
  ComputerWins == GameOver /\ ~humanTurn
  ComputerWinsEventually == []<>ComputerWins

  \* Validity checks to keep us honest
  ValidGame == \A p \in DOMAIN piles : piles[p] >= 0
  ValidChange ==
      /\ (humanTurn' /= humanTurn)
      /\ (\E p \in DOMAIN piles : \A q \in DOMAIN piles :
          IF q = p THEN piles'[q] < piles[q] ELSE piles'[q] = piles[q])
  OnlyValidChanges == [][ValidChange]_<<piles, humanTurn>>

  \* From here on are operators used in the computer strategy
  MaxPileLoc == CHOOSE p \in DOMAIN piles:
                \A q \in DOMAIN piles: piles[p] >= piles[q]

  RECURSIVE FoldL(_, _, _)
  FoldL(init, op(_,_), target) == 
      IF target = <<>> THEN init
      ELSE FoldL(op(init, Head(target)), op, Tail(target))

  \* Adapted from https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla
  RECURSIVE XorImpl(_,_,_,_)
  XorImpl(x,y,n,m) == LET exp == 2^n
                       IN IF m = 0 
                          THEN 0
                          ELSE exp * (((x \div exp) + (y \div exp)) % 2) 
                                   + XorImpl(x, y, n+1, m \div 2)
  Xor(x, y) == IF x >= y THEN XorImpl(x, y, 0, x) ELSE XorImpl(y, x, 0, y)
end define;

fair process human = "Human"
begin
A:
  while ~GameOver do
    await humanTurn \/ GameOver;
    if ~GameOver then
      with p \in DOMAIN piles do
        with takeAmt \in 1..piles[p] do
          piles[p] := piles[p] - takeAmt
        end with
      end with;
      humanTurn := FALSE
    end if
  end while
end process;

fair process computer = "Computer"
begin
A:
  while ~GameOver do
    await (~humanTurn) \/ GameOver;
    if ~GameOver then
      if Cardinality({q \in DOMAIN piles : piles[q] > 1}) > 1 then
        \* we have at least two piles larger than 1, so are not in the endgame
        \* yet. Strategy is to move so that the human gets piles such that the
        \* Xor of all piles is 0.
        with allxor = FoldL(0, Xor, piles) do
          if allxor = 0 then
            \* Uh-oh. Human is winning. Do something, because we have to.
            with p = MaxPileLoc do
              piles[p] := piles[p] - 1
            end with
          else
            with p = CHOOSE q \in DOMAIN piles : Xor(allxor, piles[q]) < piles[q] do
              \* Note that after this move, Xor of everything is 0
              piles[p] := Xor(allxor, piles[p])
            end with
          end if
        end with
      else
        \* Now we only have "1" piles left, except maybe for the largest pile,
        \* so we're in the endgame.
        \* Endgame strategy is to leave human with an odd number of "1"s
        with p = MaxPileLoc do
          with nOnes = Cardinality({q \in DOMAIN piles : piles[q] = 1}) do
            if nOnes % 2 = 1 then
              \* Either piles[p] > 1, and this move leaves human with just an
              \* odd number of "1"s, or human is winning and we need to do
              \* something so we might as well do this
              piles[p] := 0
            elsif piles[p] > 1 then
              \* Doing this increases the number of "1" piles by one, leaving
              \* human with an odd number of "1" piles.
              piles[p] := 1
            else
              \* piles[p] = 1, so this decreases the number of "1" piles by 1
              piles[p] := 0
            end if
          end with
        end with
      end if;
      humanTurn := TRUE
    end if
  end while
end process

end algorithm
*)

=============================================================================