Prepare to release sum type support in verify

CHANGELOG.md

@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 
 - When an input file only one module, it will be inferred as the main module  (#1260)
+- Sum types are now supported when running `verify` (#1034)
 
 ### Changed
 ### Deprecated

README.md

@@ -166,7 +166,7 @@ completely implementing every pass.
 | [Lists][]                         | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Records][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Tuples][]                        | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [Sum types][]                     | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [1034][]       | :x:                |
+| [Sum types][]                     | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Imports][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module definitions][]            | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module instances][]              | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |

examples/.scripts/run-example.sh

@@ -40,20 +40,24 @@ result () {
 
     # Run the command and record success / failure
     local quint_cmd="quint $cmd $args $file"
+    local succeeded=false
     if ($quint_cmd &> /dev/null)
     then
         printf ":white_check_mark:"
+        succeeded=true
     else
         printf ":x:"
+        succeeded=false
     fi
 
-    # Print additional explanations
-    if [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" &&  "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/1034</sup>"
-    elif [[ "$file" == "language-features/option.qnt" && "$cmd" == verify ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/1034</sup>"
-    elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/issues/1019</sup>"
+    # We only want to print additional info to annotate failing results
+    if [[ $succeeded == false ]]; then
+      # Print additional explanations
+      if [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
+        printf "<sup>https://github.com/informalsystems/quint/issues/1285</sup>"
+      elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && "$cmd" == "verify" ]] ; then
+        printf "<sup>https://github.com/informalsystems/quint/issues/1284</sup>"
+      fi
     fi
 }
 
@@ -118,6 +122,8 @@ get_verify_args () {
     args="--init=n4_f1::Init --step=n4_f1::Next --invariant=n4_f1::Agreement"
   elif [[ "$file" == "cosmos/ics23/ics23.qnt" ]] ; then
     args="--init=Init --step=Next"
+  elif [[ "$file" == "puzzles/tictactoe/tictactoe.qnt" ]] ; then
+    args="--max-steps=1" # pretty slow, and we just want to check that verification can run
   fi
   echo "${args}"
 }

examples/README.md

@@ -51,7 +51,7 @@ listed without any additional command line arguments.
 | [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1034</sup> |
+| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -80,7 +80,7 @@ listed without any additional command line arguments.
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1034</sup> |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -90,7 +90,7 @@ listed without any additional command line arguments.
 | [solidity/Coin/coin.qnt](./solidity/Coin/coin.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1019</sup> |
+| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1285</sup> |
 | [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |

examples/language-features/option.qnt

@@ -2,41 +2,40 @@ module option {
   // A demonstration of sum types, specifying an option type.
 
   // An option type for int values.
-  // Polymorphic sum types are not yet supported: https://github.com/informalsystems/quint/issues/1073
-  type Vote_option =
+  type VoteOption =
     | None
     | Some(int)
 
-  var votes: List[Vote_option]
+  var votes: List[VoteOption]
   var outcome: int
 
-  action Init = all {
+  action init = all {
     votes' = [],
     outcome' = 0
   }
 
-  action Vote(v) = {
+  action vote(v) = {
     votes' = votes.append(Some(v))
   }
 
-  action Unvote(i) = all {
+  action unvote(i) = all {
     votes[i] != None,
     votes' = votes.replaceAt(i, None),
   }
 
-  val SumVotes =
-    votes.foldl(0, (sum, vote) => match vote {
-        | Some(v) => sum + v
+  val sumVotes =
+    votes.foldl(0, (sum, v) => match v {
+        | Some(n) => sum + n
         | None    => sum
       }
     )
 
-  action Next = all {
+  action step = all {
     any {
-      nondet v = oneOf(Int); Vote(v),
-      nondet i = oneOf(votes.indices()); Unvote(i),
+      nondet v = oneOf(Int); vote(v),
+      nondet i = oneOf(votes.indices()); unvote(i),
     },
-    outcome' = SumVotes
+    outcome' = sumVotes
   }
 
   run matchWithDefaultTest = {

examples/puzzles/tictactoe/tictactoe.qnt

@@ -12,10 +12,14 @@
  * Gabriela Moreira, Informal Systems, 2022-2023
  */
 module tictactoe {
+  type Player = X | O
+  type Square = Occupied(Player) | Empty
+
   /// A 3x3 tic-tac-toe board
-  var board: int -> (int -> str)
+  var board: int -> (int -> Square)
+
   /// Who goes next
-  var nextTurn: str
+  var nextTurn: Player
 
   pure val boardCoordinates = tuples(1.to(3), 1.to(3))
 
@@ -40,33 +44,41 @@ module tictactoe {
     (3,3)
   )
 
-  def hasValue(coordinate, player) =
-    board.get(coordinate._1).get(coordinate._2) == player
+  def square(coordinate: (int, int)): Square =
+    board.get(coordinate._1).get(coordinate._2)
 
-  def isEmpty(coordinate) = hasValue(coordinate, "_")
+  def hasPlayer(coordinate, player) = match square(coordinate) {
+    | Empty   => false
+    | Occupied(p) => player == p
+  }
+
+  def isEmpty(coordinate) = match square(coordinate) {
+    | Empty  => true
+    | _      => false
+  }
 
   val boardEmpty = boardCoordinates.forall(isEmpty)
 
   def won(player) = winningPatterns.exists(pattern =>
-    pattern.forall(coordinate => hasValue(coordinate, player))
+    pattern.forall(coordinate => hasPlayer(coordinate, player))
   )
 
   val boardFull = not(boardCoordinates.exists(isEmpty))
-  val stalemate = boardFull and not(won("X")) and not(won("O"))
-  val gameOver = won("X") or won("O") or boardFull
+  val stalemate = boardFull and not(won(X)) and not(won(O))
+  val gameOver = won(X) or won(O) or boardFull
 
   def canWinWithPattern(pattern) = and {
-    pattern.filter(coordinate => coordinate.hasValue("X")).size() == 2,
+    pattern.filter(coordinate => coordinate.hasPlayer(X)).size() == 2,
     pattern.filter(coordinate => coordinate.isEmpty()).size() == 1,
   }
 
   def canBlockWithPattern(pattern) = and {
-    pattern.filter(coordinate => coordinate.hasValue("O")).size() == 2,
+    pattern.filter(coordinate => coordinate.hasPlayer(O)).size() == 2,
     pattern.filter(coordinate => coordinate.isEmpty()).size() == 1,
   }
 
   def canSetupWinWithPattern(pattern) = and {
-    pattern.filter(coordinate => coordinate.hasValue("X")).size() == 1,
+    pattern.filter(coordinate => coordinate.hasPlayer(X)).size() == 1,
     pattern.filter(coordinate => coordinate.isEmpty()).size() == 2,
   }
 
@@ -79,30 +91,30 @@ module tictactoe {
     isEmpty(coordinate),
     board' = board.setBy(
       coordinate._1,
-      row => row.set(coordinate._2, player)
+      row => row.set(coordinate._2, Occupied(player))
     ),
   }
 
   action Win = all {
     canWin,
     nondet pattern = winningPatterns.filter(canWinWithPattern).oneOf()
     nondet coordinate = pattern.filter(isEmpty).oneOf()
-    Move("X", coordinate),
+    Move(X, coordinate),
   }
 
   action Block = all {
     canBlock,
     nondet pattern = winningPatterns.filter(canBlockWithPattern).oneOf()
     nondet coordinate = pattern.filter(isEmpty).oneOf()
-    Move("X", coordinate),
+    Move(X, coordinate),
   }
 
-  action TakeCenter = Move("X", (2, 2))
+  action TakeCenter = Move(X, (2, 2))
 
   action SetupWin = all {
     nondet pattern = winningPatterns.filter(canSetupWinWithPattern).oneOf()
     nondet coordinate = pattern.filter(isEmpty).oneOf()
-    Move("X", coordinate),
+    Move(X, coordinate),
   }
 
   action MoveToEmpty(player) =
@@ -111,32 +123,32 @@ module tictactoe {
 
   action StartInCorner =
     nondet corner = oneOf(corners)
-    Move("X", corner)
+    Move(X, corner)
 
   action MoveX = all {
-    nextTurn == "X",
-    not(won("O")),
+    nextTurn == X,
+    not(won(O)),
     if (boardEmpty) StartInCorner else
     if (canWin) Win else
     if (canBlock) Block else
     if (canTakeCenter) TakeCenter else
     if (canSetupWin) SetupWin else
-    MoveToEmpty("X"),
-    nextTurn' = "O",
+    MoveToEmpty(X),
+    nextTurn' = O,
   }
 
   action MoveO = all {
-    nextTurn == "O",
-    not(won("X")),
-    MoveToEmpty("O"),
-    nextTurn' = "X",
+    nextTurn == O,
+    not(won(X)),
+    MoveToEmpty(O),
+    nextTurn' = X,
   }
 
   action init = all {
     // X always goes first
-    nextTurn' = "X",
+    nextTurn' = X,
     // Every space in the board starts blank
-    board' = 1.to(3).mapBy(_ => 1.to(3).mapBy(_ => "_")),
+    board' = 1.to(3).mapBy(_ => 1.to(3).mapBy(_ => Empty)),
   }
 
   /// Either X or O will make a move, depending on the value of `nextTurn`
@@ -150,10 +162,10 @@ module tictactoe {
   /* Invariants */
 
   /// X has not won. This does not hold, as X wins most of the times.
-  val XHasNotWon = not(won("X"))
+  val XHasNotWon = not(won(X))
 
   /// O has not won. This should hold, as O can only achieve a draw.
-  val OHasNotWon = not(won("O"))
+  val OHasNotWon = not(won(O))
 
   /// It's not a stalemate if one player has won or the board is not filled
   /// Check with `quint run --invariant=NotStalemate tictactoe.qnt`
@@ -166,5 +178,5 @@ module tictactoe {
 
   /// This is not always true, as if O picks the right moves, the game will
   /// result in a stalemate.
-  temporal XMustEventuallyWin = eventually(won("X"))
+  temporal XMustEventuallyWin = eventually(won(X))
 }

quint/src/quintVerifier.ts

@@ -39,7 +39,7 @@ import type { Buffer } from 'buffer'
 import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
 
 const APALACHE_SERVER_URI = 'localhost:8822'
-const APALACHE_VERSION_TAG = '0.42.0'
+const APALACHE_VERSION_TAG = '0.44.2'
 // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
 // const APALACHE_TGZ = 'apalache.tgz'