Modeling Snakes and Ladders: The Board | John Senneker's blog<br>In the last post, we introduced Verus and used it to create an abstract formal model of Snakes and Ladders. The model knows that the board has some number of squares, that players take turns moving around the board, and if someone lands on the final square the game is over, but the board itself was abstracted away completely. Here, we model the board.<br>Recall that a Snakes and Ladders board is a sequence of squares. On some squares there is the base of a ladder. Players on that square can climb the ladder to go further along the board. Other squares have the head of a snake on them; when a player lands on one of those, they slide down the snake&rsquo;s back to an earlier square.<br>A Snakes and Ladders board<br>muffinn from Worcester, UK, CC BY 2.0 https://creativecommons.org/licenses/by/2.0, via Wikimedia Commons<br>We model the board as a sequence of integers, where each integer represents the number of squares forward or backward a player must move after landing on that square:<br>pub struct Board {<br>// `Seq` is a Verus built-in type that represents an abstract sequence<br>pub squares: Seqint>,

A square that sits at the base of a ladder will have a positive value; one that sits at the head of a snake will have a negative value. Zero-valued squares are neutral.<br>For example, the board [0, 0, 0] has no snakes or ladders. The board [0, 1, 0] has a ladder in the second square, so if you land on it you immediately move forward to the final square and win the game. Conversely, the board [0, -1, 0] has a snake in the second square; if you land on it you get sent back one square to the start.<br>A few helpers will make properties easier to state. Note that DiceRoll is an enum with a case for each face on a six-sided die.<br>impl Board {<br>/// Get the total number of squares on the board.<br>pub open spec fn len(self) -> nat {<br>self.squares.len()

/// Determine if the given square is on the board.<br>pub open spec fn in_bounds(self, square: int) -> bool {<br>0 square self.len()

/// Determine if the given square is the winning square.<br>pub open spec fn is_winner(self, square: int) -> bool {<br>square == self.len() - 1

/// Compute the resting square of a player currently at the given square<br>/// after they roll the given value from the die.<br>pub open spec fn roll(self, square: int, roll: DiceRoll) -> int {<br>self.follow(square + roll.value())

/// Compute the resting square of a player who landed on the given square<br>/// after following any snakes or ladders on that square.<br>pub open spec fn follow(self, roll_square: int) -> int {<br>if roll_square >= self.len() {<br>self.len() - 1<br>} else {<br>roll_square + self.squares[roll_square]

/// Determine whether a player can come to rest at the given square.<br>/// Returns false if the given square is at the head of a snake or the<br>/// bottom of a ladder.<br>pub open spec fn is_at_rest(self, square: int) -> bool {<br>self.squares[square] == 0

/// Determine whether there is some dice roll that makes forward progress<br>/// from a given square.<br>pub open spec fn has_forward_progress(self, square: int) -> bool {<br>||| self.roll(square, DiceRoll::One) > square<br>||| self.roll(square, DiceRoll::Two) > square<br>||| self.roll(square, DiceRoll::Three) > square<br>||| self.roll(square, DiceRoll::Four) > square<br>||| self.roll(square, DiceRoll::Five) > square<br>||| self.roll(square, DiceRoll::Six) > square

Board Invariants<br>As in the abstract model, a board must have at least 2 squares, otherwise everyone would win immediately:<br>Invariant: a board must have at least 2 squares

This condition can be expressed on our Board type as:<br>self.len() > 1

The board [0, 2, 0] is invalid: the second square asks you to move forward 2 spaces, but there is only one square beyond it on the board. This suggests an invariant:<br>Invariant: snakes and ladders cannot send a player off the board<br>forall |square: int|<br>self.in_bounds(square) ==> self.in_bounds(self.follow(square))

In words, for every position on the board, adding the value of the square at that position can&rsquo;t send you before the first square or after the last. Note that forall is a spec-mode operator in Verus that represents the universal quantifier \(\forall\).<br>Another invalid board is [2, 0, 0], in which the starting square has a ladder to the final square. This board is unplayable: everyone would win before the game even began! Similarly, the board [0, 0, -1] is unplayable, because every time you land on the final square you are immediately kicked back, so the game cannot be won. We need another invariant to rule these cases out:<br>Invariant: a board cannot have a snake or ladder on the first or last square<br>self.squares[0] == 0 && self.squares[self.len() - 1] == 0

Now consider the board [0, -1, -2, -3, -4, -5, -6, 0]. This board has 6 snakes in a row. No matter what you roll on your first turn, you are sent back to the starting square. There is therefore no traversable path from start to finish, and the game is again unwinnable. We can define...