kripke: add daily and random challenges

apps/web/package.json

@@ -13,6 +13,7 @@
     "fix": "biome check --fix"
   },
   "devDependencies": {
+    "@biomejs/biome": "1.9.4",
     "@poppanator/sveltekit-svg": "5.0.0",
     "@sveltejs/adapter-auto": "3.3.1",
     "@sveltejs/enhanced-img": "0.4.4",

apps/web/src/routes/kripke/+page.svelte

@@ -1,66 +1,95 @@
 <script lang="ts">
-import { type Formula, getId, isomorphic, validWorlds } from "@cannorin/kripke";
+import { Button } from "$lib/components/ui/button";
-import LuHeart from "lucide-svelte/icons/heart";
+import * as Dialog from "$lib/components/ui/dialog";
-import Game from "./game.svelte";
+import { type Formula, isomorphic, validWorlds } from "@cannorin/kripke";
-import { getDailyFrame } from "./system";
+import LuX from "lucide-svelte/icons/x";
+import { onMount } from "svelte";
 
-const dailyFrame = getDailyFrame();
+import FrameInput from "./frame-input.svelte";
-const dailyFrameId = isomorphic[getId(dailyFrame)];
+import Game, { type GameStatus, type Move } from "./game.svelte";
-const relationSize = dailyFrame.relations.size;
+import Rules from "./rules.svelte";
-const guess = (frameId: number) => isomorphic[frameId] === dailyFrameId;
+
-const check = (formula: Formula) => validWorlds(dailyFrame, formula).length;
+import { daily } from "./store";
-const getAnswer = () => dailyFrameId;
+import { getDailyFrame, getTimeUntilNextGame } from "./system";
+
+const { id, frame } = getDailyFrame();
+const guess = (frameId: number) => isomorphic[frameId] === id;
+const check = (formula: Formula) => validWorlds(frame, formula).length;
+const getAnswer = () => id;
+const relationSize = frame.relations.size;
+
+let status: GameStatus = $state("playing");
+let dialogOpen = $state(false);
+$effect(() => {
+  if (status !== "playing") dialogOpen = true;
+});
+
+let timeUntilNextGame = $state(getTimeUntilNextGame());
+onMount(() => {
+  const interval = setInterval(() => {
+    timeUntilNextGame = getTimeUntilNextGame();
+  }, 1000);
+  return () => {
+    clearInterval(interval);
+  };
+});
 </script>
 
 <main class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8">
   <h1 class="font-display text-6xl">KRiPkE</h1>
 
   <div class="flex flex-col md:flex-row-reverse gap-x-20 gap-y-8">
-    <Game relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} />
+    <section class="flex flex-col gap-2">
+      <h2 class="text-sm">
+        <span class="font-bold">Daily Challenge: </span>
+        {timeUntilNextGame.hours}:{timeUntilNextGame.minutes}:{timeUntilNextGame.seconds} until the next game.
+      </h2>
+      <Game bind:moves={$daily.moves} bind:status relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} />
+    </section>
 
-    <div class="w-[300px] prose prose-sm">
+    <section class="w-[300px] prose prose-sm">
-      <h2>Rules</h2>
+      <h2>Daily Challenge!</h2>
       <ul>
-        <li>
+        <li>The answer of the game changes every day.</li>
-          A Kripke frame with 4 worlds is generated.
+        <li>The progress of the game persists until the next day ({timeUntilNextGame.hours}:{timeUntilNextGame.minutes}:{timeUntilNextGame.seconds} from now).</li>
-        </li>
+        <li>You can also play <a href="/kripke/random">Random Challenge</a>.</li>
-        <li>
-          The game tells you how many accessibility relations are in the frame, but not the exact shape of it.
-        </li>
-        <li>
-          You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
-          In each move you can do one of the following:
-          <ul>
-            <li>
-              Enter a modal formula.
-              The game tells you in how many worlds the formula is valid (for every valuation).
-            </li>
-            <li>
-              Guess the Kripke frame.
-              If your frame is equal or isomorphic to the secret frame, you win.
-            </li>
-          </ul>
-        </li>
-        <li>
-          You lose when you run out of moves.
-        </li>
       </ul>
 
-      <h2>Syntax</h2>
+      <Rules />
-      <p>You may use the following symbols:</p>
+    </section>
-      <ul>
-        <li>propositional variables: <code>p</code>, <code>q</code>, <code>r</code>, <code>s</code></li>
-        <li>verum: <code>⊤</code>, <code>T</code>, <code>1</code>, <code>\top</code></li>
-        <li>falsum: <code>⊥</code>, <code>F</code>, <code>0</code>, <code>\bot</code></li>
-        <li>negation: <code>¬</code>, <code>~</code>, <code>\neg</code>, <code>\lnot</code></li>
-        <li>box modality: <code>□</code>, <code>[]</code>, <code>!</code>, <code>L</code>, <code>\Box</code></li>
-        <li>diamond modality: <code>⋄</code>, <code>&lt;&gt;</code>, <code>?</code>, <code>M</code>, <code>\Diamond</code></li>
-        <li>conjunction: <code>∧</code>, <code>^</code>, <code>&amp;</code>,  <code>\wedge</code>, <code>\land</code></li>
-        <li>disjunction: <code>∨</code>, <code>v</code>, <code>|</code>, <code>\vee</code>, <code>\lor</code></li>
-        <li>implication: <code>→</code>, <code>-&gt;</code>, <code>&gt;</code>, <code>\rightarrow</code>, <code>\to</code></li>
-        <li>equivalence: <code>↔</code>,  <code>&lt;-&gt;</code>, <code>=</code>, <code>\leftrightarrow</code>, <code>\equiv</code></li>
-        <li>parentheses: <code>(</code>, <code>)</code></li>
-      </ul>
-    </div>
   </div>
 </main>
+
+{#if status !== "playing"}
+  {#await getAnswer() then answerId}
+    <Dialog.Root bind:open={dialogOpen}>
+      <Dialog.Content class="animate-fade-in">
+        <Dialog.Header>
+          <Dialog.Title>
+            {#if status === "win"}
+              YOU WIN!
+            {:else if status === "lose"}
+              YOU LOSE!
+            {/if}
+          </Dialog.Title>
+          <Dialog.Description>
+            The answer was:
+          </Dialog.Description>
+        </Dialog.Header>
+
+        <div class="flex flex-col items-center w-fit rounded bg-background mx-auto">
+          <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
+          <FrameInput class="pb-6" disabled width={250} height={250} frame={frame} />
+        </div>
+
+        <Dialog.Footer class="gap-x-1 gap-y-2">
+          <Button
+            variant="outline"
+            onclick={() => (dialogOpen = false)}>
+            <LuX class="w-4 h-4 mt-[2px]" /> Close
+          </Button>
+        </Dialog.Footer>
+      </Dialog.Content>
+    </Dialog.Root>
+  {/await}
+{/if}

apps/web/src/routes/kripke/game.svelte

@@ -1,7 +1,6 @@
 <script lang="ts">
 import Katex from "$lib/components/katex.svelte";
-import { Button } from "$lib/components/ui/button";
+
-import * as Dialog from "$lib/components/ui/dialog";
 import { cn } from "$lib/utils";
 import {
   type Formula,
@@ -44,28 +43,21 @@ let {
 }: Props = $props();
 
 let formula: Formula | undefined = $state(undefined);
+let formulaStr = $derived(
+  formula ? prettyPrint(formula, { symbols: latexSymbols }) : "",
+);
 let frame: Frame = $state(getFrame(0));
 let frameId = $derived(getId(frame));
-let math = $derived.by(() => {
-  if (formula) return prettyPrint(formula, { symbols: latexSymbols });
-  return "\\phantom{p}";
-});
 
 let remainingRelations = $derived(relationSize - frame.relations.size);
 
 let life = $derived(10 - moves.length);
-let dialogOpen = $state(false);
 
 $effect(() => {
-  if (life <= 0) {
-    status = "lose";
-    dialogOpen = true;
-    return;
-  }
   if (moves.some((move) => move.type === "guess" && move.correct)) {
     status = "win";
-    dialogOpen = true;
+  } else if (life <= 0) {
-    return;
+    status = "lose";
   }
 });
 
@@ -87,7 +79,6 @@ async function guess() {
 
 let canCheck = $derived.by(() => {
   if (status !== "playing" || life === 1 || !formula) return false;
-  const formulaStr = prettyPrint(formula);
   return !moves.some(
     (move) => move.type === "check" && move.formulaStr === formulaStr,
   );
@@ -96,7 +87,6 @@ let canCheck = $derived.by(() => {
 async function check() {
   if (!canCheck || !formula) return;
   const valid = await checkImpl(formula);
-  const formulaStr = prettyPrint(formula, { symbols: latexSymbols });
   moves.push({ type: "check", formulaStr, valid });
   moves = [...moves];
   formula = undefined;
@@ -162,8 +152,6 @@ const colors: Record<number, string> = {
     </button>
   </div>
 
-  <div class="flex flex-col items-center gap-2">
-    <Katex math={math} />
   <form
     class="flex flex-col items-center gap-2"
     onsubmit={(e) => { e.preventDefault(); check(); }}>
@@ -182,10 +170,9 @@ const colors: Record<number, string> = {
       {/if}
     </button>
   </form>
-  </div>
 
   <div>
-    <ul class="flex flex-col gap-2">
+    <ul class="flex flex-col-reverse gap-2">
       {#each moves as move}
         {#if move.type === "guess"}
           <li class="flex justify-between items-center animate-fade-in">
@@ -206,13 +193,21 @@ const colors: Record<number, string> = {
           </li>
         {/if}
       {/each}
+      {#if formulaStr}
+        <li class="flex justify-between items-center animate-fade-in">
+          <Katex math={formulaStr} />
+          <span class={["rounded w-6 h-6 min-w-6 min-h-6 max-w-6 max-h-6 text-background font-bold flex items-center justify-center pb-[2px] bg-muted"]}>?</span>
+        </li>
+      {/if}
       {#if status === "win"}
-        <li class="flex flex-col items-center gap-5 rounded bg-primary text-background p-5 animate-fade-in">
+        <li class="flex flex-col items-center gap-2 rounded bg-primary text-background p-5 animate-fade-in">
           <p class="text-xl font-bold">YOU WIN!</p>
+
+          <p class="text-sm">Play <a class="underline font-medium" href="/kripke/random">random challenge</a>?</p>
         </li>
       {:else if status === "lose"}
         {#await getAnswer() then answerId}
-          <li class="flex flex-col gap-5 rounded bg-primary text-background p-5 animate-fade-in">
+          <li class="flex flex-col gap-2 rounded bg-foreground text-background p-5 animate-fade-in">
             <div>
               <p class="text-xl font-bold">YOU LOSE!</p>
               <p class="text-sm">The answer was:</p>
@@ -221,6 +216,7 @@ const colors: Record<number, string> = {
               <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
               <FrameInput class="pb-6" disabled width={250} height={250} frame={getFrame(answerId)} />
             </div>
+            <p class="text-sm self-end">Play <a class="underline font-medium" href="/kripke/random">random challenge</a>?</p>
           </li>
         {/await}
       {/if}
@@ -228,36 +224,3 @@ const colors: Record<number, string> = {
   </div>
 </div>
 
-{#if status !== "playing"}
-  {#await getAnswer() then answerId}
-    <Dialog.Root bind:open={dialogOpen}>
-      <Dialog.Content class="animate-fade-in">
-        <Dialog.Header>
-          <Dialog.Title>
-            {#if status === "win"}
-              YOU WIN!
-            {:else if status === "lose"}
-              YOU LOSE!
-            {/if}
-          </Dialog.Title>
-          <Dialog.Description>
-            The answer was:
-          </Dialog.Description>
-        </Dialog.Header>
-
-        <div class="flex flex-col items-center w-fit rounded bg-background mx-auto">
-          <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
-          <FrameInput class="pb-6" disabled width={250} height={250} frame={getFrame(answerId)} />
-        </div>
-
-        <Dialog.Footer class="gap-x-1 gap-y-2">
-          <Button
-            variant="outline"
-            onclick={() => (dialogOpen = false)}>
-            <LuX class="w-4 h-4 mt-[2px]" /> Close
-          </Button>
-        </Dialog.Footer>
-      </Dialog.Content>
-    </Dialog.Root>
-  {/await}
-{/if}

apps/web/src/routes/kripke/random/+page.server.ts

@@ -0,0 +1,18 @@
+import type { SeoProps } from "$components/seo";
+
+export async function load() {
+  return {
+    seo: {
+      title: "KRIPKE (random challenge) - cannorin.net",
+      description: "KRIPKE - WORDLE, but for Kripke frames!",
+      openGraph: {
+        title: "KRIPKE (random challenge) - cannorin.net",
+        description: "KRIPKE - WORDLE, but for Kripke frames!",
+      },
+      twitter: {
+        title: "KRIPKE (random challenge) - cannorin.net",
+        description: "KRIPKE - WORDLE, but for Kripke frames!",
+      },
+    } as SeoProps,
+  };
+}

apps/web/src/routes/kripke/random/+page.svelte

@@ -0,0 +1,99 @@
+<script lang="ts">
+import { page } from "$app/state";
+import { Button } from "$lib/components/ui/button";
+import * as Dialog from "$lib/components/ui/dialog";
+import { type Formula, isomorphic, validWorlds } from "@cannorin/kripke";
+import LuX from "lucide-svelte/icons/x";
+
+import FrameInput from "../frame-input.svelte";
+import Game, { type GameStatus, type Move } from "../game.svelte";
+import Rules from "../rules.svelte";
+import { getRandomFrame, randomSeed } from "../system";
+
+const seed = (() => {
+  const seedStr = page.url.searchParams.get("seed");
+  if (seedStr) {
+    const seed = Math.floor(Number.parseInt(seedStr));
+    return seed;
+  }
+  return randomSeed();
+})();
+
+const { id, frame } = getRandomFrame(seed);
+const guess = (frameId: number) => isomorphic[frameId] === id;
+const check = (formula: Formula) => validWorlds(frame, formula).length;
+const getAnswer = () => id;
+const relationSize = frame.relations.size;
+
+let moves: Move[] = $state([]);
+let status: GameStatus = $state("playing");
+
+let dialogOpen = $state(false);
+$effect(() => {
+  if (status !== "playing") dialogOpen = true;
+});
+</script>
+
+{#snippet seedNumber()}
+  <a class="text-primary font-medium underline" href={`/kripke/random?seed=${seed}`}>{seed}</a>
+{/snippet}
+
+<main class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8">
+  <h1 class="font-display text-6xl">KRiPkE</h1>
+
+  <div class="flex flex-col md:flex-row-reverse gap-x-20 gap-y-8">
+    <section class="flex flex-col gap-2">
+      <h2 class="text-sm">
+        <span class="font-bold">Random Challenge</span>
+        <span>(seed: {@render seedNumber()})</span>
+      </h2>
+      <Game bind:moves bind:status relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} />
+    </section>
+
+    <section class="w-[300px] prose prose-sm">
+      <h2>Random Challenge!</h2>
+      <ul>
+        <li>The answer of the game is determined by a seed number {@render seedNumber()}, which changes on every reload.</li>
+        <li>You can right-click on the seed number to obtain a permalink to this exact game.</li>
+        <li>Unlike Daily Challenge, the progress of the game does not persist.</li>
+        <li>You can also play <a href="/kripke">Daily Challenge</a>, if you have not yet.</li>
+      </ul>
+
+      <Rules />
+    </section>
+  </div>
+</main>
+
+{#if status !== "playing"}
+  {#await getAnswer() then answerId}
+    <Dialog.Root bind:open={dialogOpen}>
+      <Dialog.Content class="animate-fade-in">
+        <Dialog.Header>
+          <Dialog.Title>
+            {#if status === "win"}
+              YOU WIN!
+            {:else if status === "lose"}
+              YOU LOSE!
+            {/if}
+          </Dialog.Title>
+          <Dialog.Description>
+            The answer was:
+          </Dialog.Description>
+        </Dialog.Header>
+
+        <div class="flex flex-col items-center w-fit rounded bg-background mx-auto">
+          <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
+          <FrameInput class="pb-6" disabled width={250} height={250} frame={frame} />
+        </div>
+
+        <Dialog.Footer class="gap-x-1 gap-y-2">
+          <Button
+            variant="outline"
+            onclick={() => (dialogOpen = false)}>
+            <LuX class="w-4 h-4 mt-[2px]" /> Close
+          </Button>
+        </Dialog.Footer>
+      </Dialog.Content>
+    </Dialog.Root>
+  {/await}
+{/if}

apps/web/src/routes/kripke/rules.svelte

@@ -0,0 +1,46 @@
+<script lang="ts">
+import LuHeart from "lucide-svelte/icons/heart";
+</script>
+
+<h2>Rules</h2>
+<ul>
+  <li>
+    A Kripke frame with 4 worlds is generated.
+  </li>
+  <li>
+    The game tells you how many accessibility relations are in the frame, but not the exact shape of it.
+  </li>
+  <li>
+    You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
+    In each move you can do one of the following:
+    <ul>
+      <li>
+        Enter a modal formula.
+        The game tells you in how many worlds the formula is valid (for every valuation).
+      </li>
+      <li>
+        Guess the Kripke frame.
+        If your frame is equal or isomorphic to the secret frame, you win.
+      </li>
+    </ul>
+  </li>
+  <li>
+    You lose when you run out of moves.
+  </li>
+</ul>
+
+<h2>Syntax</h2>
+<p>You may use the following symbols:</p>
+<ul>
+  <li>propositional variables: <code>p</code>, <code>q</code>, <code>r</code>, <code>s</code></li>
+  <li>verum: <code>⊤</code>, <code>T</code>, <code>1</code>, <code>\top</code></li>
+  <li>falsum: <code>⊥</code>, <code>F</code>, <code>0</code>, <code>\bot</code></li>
+  <li>negation: <code>¬</code>, <code>~</code>, <code>\neg</code>, <code>\lnot</code></li>
+  <li>box modality: <code>□</code>, <code>[]</code>, <code>!</code>, <code>L</code>, <code>\Box</code></li>
+  <li>diamond modality: <code>⋄</code>, <code>&lt;&gt;</code>, <code>?</code>, <code>M</code>, <code>\Diamond</code></li>
+  <li>conjunction: <code>∧</code>, <code>^</code>, <code>&amp;</code>,  <code>\wedge</code>, <code>\land</code></li>
+  <li>disjunction: <code>∨</code>, <code>v</code>, <code>|</code>, <code>\vee</code>, <code>\lor</code></li>
+  <li>implication: <code>→</code>, <code>-&gt;</code>, <code>&gt;</code>, <code>\rightarrow</code>, <code>\to</code></li>
+  <li>equivalence: <code>↔</code>,  <code>&lt;-&gt;</code>, <code>=</code>, <code>\leftrightarrow</code>, <code>\equiv</code></li>
+  <li>parentheses: <code>(</code>, <code>)</code></li>
+</ul>

apps/web/src/routes/kripke/store.ts

@@ -0,0 +1,24 @@
+import { persisted } from "svelte-persisted-store";
+import type { Move } from "./game.svelte";
+import { date } from "./system";
+
+export type Daily = {
+  date: string;
+  moves: Move[];
+};
+
+export const daily = persisted<Daily>(
+  "daily",
+  {
+    date: date(),
+    moves: [],
+  },
+  {
+    syncTabs: true,
+    storage: "local",
+    beforeRead: (value) => {
+      if (value.date !== date()) return { date: date(), moves: [] };
+      return value;
+    },
+  },
+);

apps/web/src/routes/kripke/system.ts

@@ -18,10 +18,43 @@ function cyrb53(str: string, seed = 0): number {
   return 4294967296 * (2097151 & h2) + (h1 >>> 0);
 }
 
+export const date = () => new Date().toISOString().split("T")[0];
+
 export function getDailyFrame() {
   // Use UTC ISO string so it's consistent across time zones
-  const dateStr = new Date().toISOString().split("T")[0];
+  const dateStr = date();
   const hash = cyrb53(dateStr);
   const index = hash % nontrivials.length;
-  return getFrame(nontrivials[index]);
+  return {
+    date: dateStr,
+    id: nontrivials[index],
+    frame: getFrame(nontrivials[index]),
+  };
+}
+
+export const randomSeed = () => Math.floor(Math.random() * 0x100000000);
+
+export function getRandomFrame(seed?: number) {
+  const actualSeed = seed ?? randomSeed();
+  const hash = cyrb53("random", seed);
+  const index = hash % nontrivials.length;
+  return {
+    seed: actualSeed,
+    id: nontrivials[index],
+    frame: getFrame(nontrivials[index]),
+  };
+}
+
+export function getTimeUntilNextGame() {
+  const now = new Date();
+  const nextDayUTC = new Date(
+    Date.UTC(now.getUTCFullYear(), now.getUTCMonth(), now.getUTCDate() + 1),
+  );
+  const deltaSeconds = (nextDayUTC.getTime() - now.getTime()) / 1000;
+  const pad = (num: number) => `0${num}`.slice(-2);
+  return {
+    hours: pad(Math.floor(deltaSeconds / 3600)),
+    minutes: pad(Math.floor((deltaSeconds % 3600) / 60)),
+    seconds: pad(Math.floor(deltaSeconds % 60)),
+  };
 }

yarn.lock

@@ -3948,6 +3948,7 @@ __metadata:
   version: 0.0.0-use.local
   resolution: "web@workspace:apps/web"
   dependencies:
+    "@biomejs/biome": "npm:1.9.4"
     "@cannorin/kripke": "workspace:*"
     "@fontsource/poiret-one": "npm:5.1.1"
     "@fontsource/zen-kaku-gothic-new": "npm:5.1.1"