Holiday protocols: secret santa with Quint 🎅

Hi everyone, and happy holiday season! I'm Gabriela, I work on Quint (opens in a new tab), and today I'll walk you through my end-of-the-year holiday experiment: writing a specification for the secret santa game 🎅.

Secret santa is a game for trading presents between participants. We write down the participants' names on individual pieces of paper, fold them, and put them in a bowl. The bowl is passed around to the participants, with each of them taking one piece of paper from the bowl, deciding the person the picker should gift a present to. This goes on until the bowl is empty, and everyone has someone to gift 🎁.

I played this game at least once a year since I was a little kid, and well, different groups have different standards for the drawing process. I'm always one of the (potentially annoying) people who will make everyone play by the safest rules (well, that applies to many other scenarios, and I guess that's how I ended up working on Quint 😬). So welcome aboard if you are one of these people too, and if you are not, this blogpost might introduce some complications for your next secret santa game.

Disclaimer: This is not a super didactic tutorial, but rather a fun example of how I personally appreciate Quint (or formal specification in general). If you are looking for tutorials, we have some better introductory material here, and more documentation here. In any way, I still recommend skimming through this as a potential motivational material ❤️.

The complete spec described here is available in the examples folder (opens in a new tab).

Basic secret santa

Let's start with the basics: we have a bowl of recipient names. As each participant draws its recipient, we record the drawn name in a map called recipient_for_santa. The keys of the map are the santas giving gifts, and the values are the gift-receivers for each santa. Those will be our two state variables, meaning we'll be changing their values as the game progresses. The set of participants in the game is a constant, which can be seen as a module parameter (more on that later).

We also import a library with some utility functions. The import statement should point to the basicSpells.qnt (opens in a new tab) file, from the quint repo, on your local file system.

module secret_santa {
  import basicSpells.* from "../../spells/basicSpells"
 
  const participants: Set[str]
 
  /// A map from santas to their recipients. get(recipient_for_santa, S) is the recipient for secret santa S
  var recipient_for_santa: str -> str
 
  /// The bowl of participants, containing a paper piece for each participant's name
  var bowl: Set[str]
}

Now that we have the state variables, we need to specify their values in the initial state:

/// The initial state
action init = all {
  recipient_for_santa' = Map(), // No santas or recipients
  bowl' = participants,         // Every participant's name in the bowl
}

The following definitions are helpers: the set of santas are the keys of the recipent_for_santa map, while the recipients are the values of that map. These values are not fixed. Rather, they work as projections, or views, on the current state. When the values for the recipient_for_santa state variable change, the values for these helpers will change as well.

val santas = recipient_for_santa.keys()
val recipients = recipient_for_santa.values()

Finally, we define the system's transitions, which is just the drawing process. At each step, we non-deterministically pick the participant who is going to draw, and then, non-deterministically, draw one of the names from the bowl. We register that on our recipient_for_santa map and remove the drawn name from the bowl. When the bowl gets empty, we still need to define what happens. In this case, the drawing is over, and all state variables will stay the same - at least until the next holidays :christmas_tree:. When no variables change, we call that a stutter step.

action draw_recipient(santa: str): bool = {
  nondet recipient = oneOf(bowl)
  all {
    recipient_for_santa' = put(recipient_for_santa, santa, recipient),
    bowl' = bowl.setRemove(recipient),
  }
}
 
action stutter = all {
  recipient_for_santa' = recipient_for_santa,
  bowl' = bowl,
}
 
action step =
  if (empty(bowl)) {
    stutter
  } else {
    nondet next_santa = participants.exclude(santas).oneOf()
    draw_recipient(next_santa)
  }

This is a very basic protocol, but already ensures one of the properties I'm interested in: no sad kids with no presents at the revelation - everyone gets a santa. That is, if the bowl is empty. In other words, the bowl being empty implies that all the participants will receive gifts 🎁.

val everyone_gets_a_santa = empty(bowl) implies (participants == recipients)

Before we can check that our spec satisfies this property, we need to define a value for our module's constant. Constants are parameters to a module, so we need to instantiate that module and specify the participants. Let's use the Quint developer team as an example!

module secret_santa {
  // ... all the code from before
}
 
module quint_team_secret_santa {
  import secret_santa(participants = Set("Gabriela", "Igor", "Jure", "Shon", "Thomas")).*
}

Now we can use Quint's verify command to check that all possible executions (up to a certain length -- 10 steps, by default) satisfy this property for the quint_team_secret_santa module.

quint verify secret_santa.qnt --main=quint_team_secret_santa --invariant=everyone_gets_a_santa

We get a successful result - the property holds!

[ok] No violation found (2119ms).
You may increase --max-steps.

Let's try a different property! People don't really want to buy themselves presents. Well, perhaps except for that teenage cousin who would rather not be playing, but their mom forced them to. But let's not consider that. So let's write a property stating that, for each santa, they are not their own recipient.

val no_person_is_self_santa = santas.forall(santa =>
  get(recipient_for_santa, santa) != santa
)

And then check that property:

quint verify secret_santa.qnt --main=quint_team_secret_santa --invariant=no_person_is_self_santa

This time, we find out that the property does not hold! Quint provides us with a minimal counterexample.

An example execution:
 
[State 0] { quint_team_secret_santa::secret_santa::bowl: Set("Gabriela", "Igor", "Jure", "Shon", "Thomas"), quint_team_secret_santa::secret_santa::recipient_for_santa: Map() }
 
[State 1] { quint_team_secret_santa::secret_santa::bowl: Set("Igor", "Jure", "Shon", "Thomas"), quint_team_secret_santa::secret_santa::recipient_for_santa: Map("Gabriela" -> "Gabriela") }
    
[violation] Found an issue (2068ms).
error: found a counterexample

In this example, Gabriela (that's me) got themself in the very first draw and would have to buy their own present. Not great!

A better secret santa game has an additional, currently unspecified, step: after a person draws a name from the bowl, they should confirm that they didn't get themself before the drawing can continue. If someone draws themself, one of two strategies can take place:

They immediately put their name back and draw again.
The whole game gets reset: everyone who has already drawn a paper puts it back, and it all starts again.

I want to try both strategies in Quint, and then show how (2) is better than (1). Usually, people don't want to reset the whole thing and get tempted to do (1), and that's when I say "no no no no no". Well, now I can show them the Quint spec and counterexamples, and they won't have any arguments! But first, let's add the confirmation step to our existing spec, which will be used by both strategies.

First, we add a variable and change our init definition to include an initialization for it. We should also make sure it also stutters in our stutter helper definition.

/// Information about the last draw
type LastDraw =
  | Self(str) // The name of someone who drew themself
  | Ok        // The draw was Ok
 
var last_draw: LastDraw
 
action init = all {
  // ...
  last_draw' = Ok // if no one has drawn yet, no one has drawn themself
}
 
action stutter = all {
  // ...
  last_draw' = last_draw,
}

Then, we update the draw_recipent action to include the confirmation, that is, last_draw should be updated to the participant who drew, and its confirmed value should be true if and only if the participant got someone other than themself.

action draw_recipient(santa: str): bool = {
nondet recipient = oneOf(bowl)
all {
  // ...
  last_draw' = if (santa == recipient) Self(santa) else Ok
}

With this variable in place, we can now write a new invariant stating that our predicate no_person_is_self_santa should be satisfied if the last draw was ok. That is, the condition implies the predicate.

val inv = (last_draw == Ok) implies no_person_is_self_santa

Defining the variable on its own doesn't help us with satisfying that property, tho. We need to define a strategy to deal with scenarios where the last draw didn't turn out right.

Secret santa with the redraw strategy

In this strategy, when a participant draws themself, they should pick another name. They can either first put their name back in the bowl, and then redraw; or first redraw and then put their name back, ensuring they won't get themself again. Both of them should work the same in the end, since we are not considering efficiency here. But let's define the latter.

action redraw(participant: str): bool = {
  // Draw from the current bowl, without having first put paper back
  nondet new_recipient = oneOf(bowl)
  all {
    new_recipient != participant, // The action requires this precondition
    // Remove the new paper from the bowl, and then put the old one back in
    bowl' = bowl.exclude(Set(new_recipient)).union(Set(participant)),
    recipient_for_santa' = recipient_for_santa.put(participant, new_recipient),
    last_draw' = Ok // We know this is OK due to the precondition
  }
}

We should call the redraw action whenever we find a self-draw. It is important to ensure that the bowl is not empty when we call that action since we need at least one name in the bowl to be drawn.

action step_with_redraw =
  match last_draw {
    | Ok =>
        step // All good, continue as usual
    | Self(participant) => all {
        not(empty(bowl)),
        redraw(participant),
      }
  }

Let's check if our new invariant inv (defined as (last_draw == Ok) implies no_person_is_self_santa is satisfied with our new step definition. We now have to specify our step definition with --step=step_with_redraw, otherwise, Quint will use the default name step.

quint verify secret_santa.qnt --main=quint_team_secret_santa --invariant=inv --step=step_with_redraw

The property is successfully checked.

[ok] No violation found (4360ms).

Secret santa with the reset strategy

In the reset strategy, we restart the whole game when some confirmation is negative. The definition looks quite nice! We could define this in a different module and plug everything together with import statements - but let's keep things simpler here and define yet another step action called step_with_reset.

action step_with_reset =
  if (last_draw == Ok) {
    step
  } else {
    init
  }

Now, let's check the property.

quint verify secret_santa.qnt --main=quint_team_secret_santa --invariant=inv --step=step_with_reset

The property is successfully checked.

[ok] No violation found (2492ms).

Redrawing is not good enough!

Although both strategies can guarantee that, if the last draw was confirmed, then no person is their own santa, I still see two scenarios where the redraw strategy might have problems, while the reset strategy does not.

If the player who draws themself is the last player, and the bowl gets empty, there is nothing to be done to solve the issue.
If some of the players have a good memory and pay attention, they will have information about who may and may not be someone's santa, and even potentially find out who is a santa of someone, or their own santa! We need to preserve the "secret" part of this game!

To show how (1) can happen, we should use temporal properties. However, since that requires a deeper explanation, and the tooling for it is not the most stable at the moment, I'll leave this one for next year. Instead, let's play around with (2).

(2) does not need all the players to have a great memory, so let's say only I (Gabriela) am actually paying attention and memorizing some stuff. For that, let's introduce my memory as a state variable.

/// Who had already drawn a paper when someone got themself. This way, I know
/// that none of those people can be the santa of the person who is drawing.
var gabrielas_memory: str -> Set[str]

This is what I will be memorizing during the game: for each person that gets themself, who has already drawn by the time they got themself. Let's think of an example, using the Quint team as the set of participants (that is Set("Gabriela", "Igor", "Jure", "Shon", "Thomas")): Let's say Shon draws and confirms, then Igor draws and confirms, then Thomas draws and makes a negative confirmation. At that point, I know that neither Shon nor Igor had drawn Thomas, otherwise, the paper with Thomas' name wouldn't be in the bowl when he drew. So my memory map becomes Map("Thomas" -> Set("Shon", "Igor", "Thomas")), which tells me that neither Shon nor Igor is Thomas' santa. Thomas themself is also part of the set because that makes things easier to represent, but we could also choose to remove the participant themself from the set.

This memorization is only relevant in the redraw strategy, as the reset strategy reinitializes the whole process on self-sdraws, making any memorization useless from that point on. Therefore, let's only play with memorization in the redraw version. For that let's define how the memory variable is initialized and updated:

action init = all {
  // ...
  gabrielas_memory' = Map(),
}
 
action draw_recipient(santa: str): bool = {
  // ...
  all {
    // ...,
    gabrielas_memory' = gabrielas_memory, // Nothing to memorize, so the memory stays the same
  }
}
 
action stutter = all {
  // ...
  gabrielas_memory' = gabrielas_memory,
}
 
// Store current santas (people who have already drawn) on a participant's key, meaning that they can't be that participant's santa
action memorize(participant) = {
  gabrielas_memory' = put(gabrielas_memory, participant, santas)
}
 
action step_with_redraw =
  match last_draw {
    | Ok =>
        step // All good, continue as usual
    | Self(participant) => all {
        // ...,
        memorize(participant),
      }
  }

Is there a scenario where I find out who is someone's santa?

Now let's define a property that is true when I am able to deduce someone's santa:

/// true iff Gabriela can find out who is a santa for someone.
/// That is, if exists a participant where find_out_a_santa_for participant is Some()
val gabriela_finds_out_a_santa = participants.exists(participant => {
  if (gabrielas_memory.has(participant)) {
    val possible_santas = participants.exclude(gabrielas_memory.get(participant))
    possible_santas.size() == 1
  } else {
    false
  }
})

Finally, the invariant we want to check is that Gabriela should NOT be able to find out a santa.

val safe_from_memorizers = not(gabriela_finds_out_a_santa)

Let's verify it, with the redraw version of step_for_confirmation

quint verify secret_santa.qnt --main=quint_team_secret_santa --invariant=safe_from_memorizers --step=step_with_redraw

We get a violation! After 5 steps, we get to a point where I know that Shon is my santa 🎅

...
[State 5]
{
  quint_team_secret_santa::secret_santa::bowl: Set("Gabriela"),
  quint_team_secret_santa::secret_santa::gabrielas_memory:
    Map("Gabriela" -> Set("Gabriela", "Igor", "Jure", "Thomas")),
  quint_team_secret_santa::secret_santa::last_draw: Ok,
  quint_team_secret_santa::secret_santa::recipient_for_santa:
    Map("Jure" -> "Igor", "Igor" -> "Thomas", "Gabriela" -> "Jure", "Thomas" -> "Shon")
}
 
[violation] Found an issue (2628ms).
error: found a counterexample

On state 5, my memory is Map("Gabriela" -> Set("Gabriela", "Igor", "Jure", "Thomas")), so only Shon can possibly be my (non-secret) santa!

Here, we only checked for the presence of the worst scenario: finding out someone's santa. This only happens if the second to last person redraws, and therefore their name is the only one in the bowl when the last person (in this case, Shon) draws. However, memorizers can also find partial information that can also ruin the game a bit, i.e. knowing for sure that a person who always gives the best gifts couldn't possibly have drawn me - that's a bummer, right?

Well, what actually bothers me is having possible flaws in the drawing protocol like this, and that's why every year I insist on the reset strategy. There are some other interesting properties of secret santa that I'd like to explore, especially in the revelation procedure. But it's almost Christmas already, which means it's time for me to get ready for some beach time: I'm in Brazil, and we get Christmas during summer, and that's my favorite time of the year ☀️. So let's talk about secret santa Quint specs again next year.

Wish you all a happy holiday season and a lovely new year!

Sets Literate Specifications