Add Quint Xmas logo for secret santa blogpost

docs/components/ThemedImage.tsx

@@ -0,0 +1,10 @@
+import { useTheme } from 'next-themes';
+import Image from 'next/image';
+
+export function ThemedImage({ lightSrc, darkSrc, alt, width = 500, height = 300 }) {
+  const { theme } = useTheme();
+
+  const src = theme === 'dark' ? darkSrc : lightSrc;
+
+  return <Image src={src} alt={alt} width={width} height={height} />;
+}

docs/pages/docs/blogposts/secret_santa.mdx

@@ -1,11 +1,20 @@
-# Holiday protocols: secret santa with Quint 🎅
+import { ThemedImage } from '../../../components/ThemedImage';
+
+# Holiday protocols: Secret Santa with Quint 🎅
 
 Hi everyone, and happy holiday season! I'm Gabriela, I work on
 [Quint](https://github.com/informalsystems/quint), 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
+<br />
+<ThemedImage
+  lightSrc="/quint-xmas-dark.svg"
+  darkSrc="/quint-xmas-light.svg"
+  alt="Themed Image"
+/>
+
+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
@@ -18,7 +27,7 @@ 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.
+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
@@ -30,12 +39,12 @@ material ❤️.
 
 The complete spec described here is available in the [examples folder](https://github.com/informalsystems/quint/tree/main/examples/games/secret-santa/secret_santa.qnt).
 
-## Basic secret santa
+## 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
+`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).
@@ -50,7 +59,7 @@ module secret_santa {
 
   const participants: Set[str]
 
-  /// A map from santas to their recipients. get(recipient_for_santa, S) is the recipient for secret santa S
+  /// 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
@@ -63,12 +72,12 @@ Now that we have the state variables, we need to specify their values in the ini
 ```quint
 /// The initial state
 action init = all {
-  recipient_for_santa' = Map(), // No santas or recipients
+  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.
+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.
 
 ```quint
 val santas = recipient_for_santa.keys()
@@ -102,7 +111,7 @@ action step =
 
 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
+Santa. That is, if the bowl is empty. In other words, the bowl being empty
 **implies** that all the participants will receive gifts 🎁.
 
 ```quint
@@ -141,7 +150,7 @@ 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.
+write a property stating that, for each Santa, they are not their own recipient.
 
 ```quint
 val no_person_is_self_santa = santas.forall(santa =>
@@ -162,14 +171,14 @@ 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 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:
 
@@ -221,7 +230,7 @@ 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
+## 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.
 
@@ -294,10 +303,10 @@ The property is successfully checked.
 
 ## 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.
+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.
 
 1.  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.
-2.  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!
+2.  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).
 
@@ -311,7 +320,7 @@ 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:
+This memorization is only relevant in the redraw strategy, as the reset strategy reinitializes the whole process on self-draws, 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:
 
 ```quint
 action init = all {
@@ -332,7 +341,7 @@ 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
+// 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)
 }
@@ -352,10 +361,10 @@ action step_with_redraw =
 ### 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:
+Santa:
 
 ```quint
-/// true iff Gabriela can find out who is a santa for someone.
+/// 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)) {
@@ -367,7 +376,7 @@ val gabriela_finds_out_a_santa = participants.exists(participant => {
 })
 ```
 
-Finally, the invariant we want to check is that Gabriela should NOT be able to find out a santa.
+Finally, the invariant we want to check is that Gabriela should NOT be able to find out a Santa.
 
 ```quint
 val safe_from_memorizers = not(gabriela_finds_out_a_santa)
@@ -379,7 +388,7 @@ 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 🎅
+We get a violation! After 5 steps, we get to a point where I know that Shon is my Santa 🎅
 
 ```sh
 ...
@@ -397,11 +406,10 @@ We get a violation! After 5 steps, we get to a point where I know that Shon is m
 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!
+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?
+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.
+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!
-