From d85ad63e011d72b0a4068007b3525fc8d1ac6538 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 24 Nov 2023 13:32:24 -0500 Subject: [PATCH 1/8] Use sum types for tictactoe example --- examples/puzzles/tictactoe/tictactoe.qnt | 72 ++++++++++++++---------- 1 file changed, 42 insertions(+), 30 deletions(-) diff --git a/examples/puzzles/tictactoe/tictactoe.qnt b/examples/puzzles/tictactoe/tictactoe.qnt index e609ec131..31aa6fdd4 100644 --- a/examples/puzzles/tictactoe/tictactoe.qnt +++ b/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 + | Occupied(_) => 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,7 +91,7 @@ module tictactoe { isEmpty(coordinate), board' = board.setBy( coordinate._1, - row => row.set(coordinate._2, player) + row => row.set(coordinate._2, Occupied(player)) ), } @@ -87,22 +99,22 @@ module tictactoe { 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)) } From f0f26b0fb17557733abd7a3250417ac56899371e Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 10:55:44 -0500 Subject: [PATCH 2/8] Update Apalache version --- quint/src/quintVerifier.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index 1f724ff16..d1e943206 100644 --- a/quint/src/quintVerifier.ts +++ b/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' From d8fdf128f1dcb81bce5203d9d42ca8449403590a Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 10:58:40 -0500 Subject: [PATCH 3/8] Update option.qnt for verification Use current conventions for operator names --- examples/language-features/option.qnt | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/examples/language-features/option.qnt b/examples/language-features/option.qnt index 1be3c5801..871eda916 100644 --- a/examples/language-features/option.qnt +++ b/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 = { From a32a6310de265924a7f827e51c69f4e2b7803517 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 11:09:02 -0500 Subject: [PATCH 4/8] Update examples script --- examples/.scripts/run-example.sh | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index 50458eeee..92dc211d8 100755 --- a/examples/.scripts/run-example.sh +++ b/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 "https://github.com/informalsystems/quint/issues/1034" - elif [[ "$file" == "language-features/option.qnt" && "$cmd" == verify ]] ; then - printf "https://github.com/informalsystems/quint/issues/1034" - elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then - printf "https://github.com/informalsystems/quint/issues/1019" + # 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 "https://github.com/informalsystems/quint/issues/1285" + elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && "$cmd" == "verify" ]] ; then + printf "https://github.com/informalsystems/quint/issues/1284" + 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}" } From f53a6c3d5bc966fc0e811dfee8285d4e813544a6 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 11:11:31 -0500 Subject: [PATCH 5/8] Update changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 197872a08..6c590d35e 100644 --- a/CHANGELOG.md +++ b/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 From be9a510723dc2121ec05786c4ce5440d623cf9ae Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 17:54:17 -0500 Subject: [PATCH 6/8] Use a default case in the tictactoe example Ensure we can handle this construct in verification, and it also clarifies the meaning of the operator tweaked. --- examples/puzzles/tictactoe/tictactoe.qnt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/puzzles/tictactoe/tictactoe.qnt b/examples/puzzles/tictactoe/tictactoe.qnt index 31aa6fdd4..4c272e087 100644 --- a/examples/puzzles/tictactoe/tictactoe.qnt +++ b/examples/puzzles/tictactoe/tictactoe.qnt @@ -53,8 +53,8 @@ module tictactoe { } def isEmpty(coordinate) = match square(coordinate) { - | Empty => true - | Occupied(_) => false + | Empty => true + | _ => false } val boardEmpty = boardCoordinates.forall(isEmpty) From f0f0c3e87482e6e76d19509fbadaa4fc83d9dd67 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 18:29:09 -0500 Subject: [PATCH 7/8] Update examples dashboard --- examples/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/README.md b/examples/README.md index 2e536ee2b..ce21160a1 100644 --- a/examples/README.md +++ b/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:https://github.com/informalsystems/quint/issues/1034 | +| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1284 | | [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:https://github.com/informalsystems/quint/issues/1034 | +| [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:https://github.com/informalsystems/quint/issues/1019 | +| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1285 | | [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] | From c53b2ca7a1d3dbc7657f0cc42be63b6c0ba5675a Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Dec 2023 18:30:49 -0500 Subject: [PATCH 8/8] Update feature table --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2deffd5cd..d163e4fd8 100644 --- a/README.md +++ b/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: |