kripke: create PoC

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

@@ -3,24 +3,90 @@ import Katex from "$lib/components/katex.svelte";
 import {
   type Formula,
   type Frame,
+  getFrame,
+  getId,
+  isomorphic,
   latexSymbols,
   prettyPrint,
+  validWorlds,
 } from "@cannorin/kripke";
 import LuHeart from "lucide-svelte/icons/heart";
 import LuHeartCrack from "lucide-svelte/icons/heart-crack";
 import FormulaInput from "./formula-input.svelte";
 import FrameInput from "./frame-input.svelte";
+import { getDailyFrame } from "./system";
 
 let formula: Formula | undefined = $state(undefined);
-let frame: Frame = $state({ relations: new Set() });
+let frame: Frame = $state(getFrame(0));
 let math = $derived.by(() => {
   if (formula) return prettyPrint(formula, { symbols: latexSymbols });
   return "\\phantom{p}";
 });
 
-const life = 6;
+const dailyFrame = getDailyFrame();
+const dailyFrameId = isomorphic[getId(dailyFrame)];
+let remainingRelations = $derived(
+  dailyFrame.relations.size - frame.relations.size,
+);
+
+type Move =
+  | { type: "guess"; frameId: number; correct: boolean }
+  | { type: "check"; formulaStr: string; valid: number };
+
+let moves: Move[] = $state([]);
+let life = $derived(10 - moves.length);
+
+let canGuess = $derived.by(() => {
+  if (remainingRelations !== 0) return false;
+  const frameId = isomorphic[getId(frame)];
+  return !moves.some(
+    (move) => move.type === "guess" && move.frameId === frameId,
+  );
+});
+function guess() {
+  if (!canGuess) return;
+  const frameId = isomorphic[getId(frame)];
+  moves.push({ type: "guess", frameId, correct: frameId === dailyFrameId });
+  moves = [...moves];
+}
+
+let canCheck = $derived.by(() => {
+  if (!formula) return false;
+  const formulaStr = prettyPrint(formula);
+  return !moves.some(
+    (move) => move.type === "check" && move.formulaStr === formulaStr,
+  );
+});
+function check() {
+  if (!canCheck || !formula) return;
+  const formulaStr = prettyPrint(formula);
+  const valid = validWorlds(dailyFrame, formula).length;
+  moves.push({ type: "check", formulaStr, valid });
+  moves = [...moves];
+  formula = undefined;
+}
 </script>
 
+{#snippet sampleArrow()}
+  <svg width="50" height="10" class="mt-[1px]">
+    <defs>
+      <marker
+        id="arrowhead"
+        viewBox="0 0 10 10"
+        refX="8"
+        refY="5"
+        markerWidth="6"
+        markerHeight="6"
+        orient="auto"
+        markerUnits="strokeWidth"
+      >
+        <path d="M0,0 L0,10 L10,5 z" fill="rgb(var(--foreground))" />
+      </marker>
+    </defs>
+    <path d="M 5 5 L 45 5" stroke="rgb(var(--foreground))" stroke-width="1" marker-end="url(#arrowhead)" />
+  </svg>
+{/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>
@@ -38,24 +104,98 @@ const life = 6;
       </div>
 
       <div class="flex flex-col items-center gap-2">
-        <FrameInput bind:frame />
+        <div class="w-[300px] h-[300px] flex flex-col items-center justify-betwenn border rounded border-border">
+          <span class="text-xs text-muted self-start px-2 py-1">id: {isomorphic[getId(frame)]}</span>
+          <FrameInput bind:frame />
+          <span class="text-sm px-2 py-1 self-end flex items-center">
+            {@render sampleArrow()} × {remainingRelations}
+          </span>
+        </div>
 
-        <button class="rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2">
-          Guess! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1"/>1)</span>
+        <button
+          onclick={guess}
+          disabled={!canGuess}
+          class={[
+            "rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2",
+            !canGuess && "bg-muted cursor-not-allowed"
+          ]}>
+          Guess! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
         </button>
       </div>
 
       <div class="flex flex-col items-center gap-2">
         <Katex math={math} />
         <FormulaInput bind:formula />
-        <button class="rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2">
-          Check! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1"/>1)</span>
+        <button
+          onclick={check}
+          disabled={!canCheck}
+          class={[
+            "rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2",
+            !canCheck && "bg-muted cursor-not-allowed"
+          ]}>
+          Check! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
         </button>
       </div>
+
+      <div>
+        <ul class="flex flex-col gap-2">
+          {#each moves as move}
+            <li>
+              {#if move.type === "guess"}
+                Guess({move.frameId}) = {move.correct}
+              {/if}
+              {#if move.type === "check"}
+                Valid({move.formulaStr}) = {move.valid}
+              {/if}
+            </li>
+          {/each}
+        </ul>
+      </div>
     </div>
 
-    <div class="w-[300px] flex flex-col gap-4">
-      Foo
+    <div class="w-[300px] prose prose-sm">
+      <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>T</code>, <code>⊤</code>, <code>1</code>, <code>\top</code></li>
+        <li>falsum: <code>F</code>, <code>⊥</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>L</code>, <code>\Box</code></li>
+        <li>diamond modality: <code>&lt;&gt;</code>, <code>⋄</code>, <code>M</code>, <code>\Diamond</code></li>
+        <li>conjunction: <code>&amp;</code>, <code>^</code>, <code>∧</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>-&gt;</code>, <code>→</code>, <code>\rightarrow</code>, <code>\to</code>, <code>\implies</code></li>
+        <li>equivalence: <code>&lt;-&gt;</code>, <code>↔</code>, <code>\leftrightarrow</code>, <code>\iff</code></li>
+        <li>parentheses: <code>(</code>, <code>)</code></li>
+      </ul>
     </div>
   </div>
 </main>

apps/web/src/routes/kripke/formula-input.svelte

@@ -1,5 +1,5 @@
 <script lang="ts">
-import { type Formula, tryParse } from "@cannorin/kripke";
+import { type Formula, prettyPrint, tryParse } from "@cannorin/kripke";
 
 let {
   formula = $bindable<Formula | undefined>(undefined),
@@ -7,7 +7,7 @@ let {
   formula?: Formula | undefined;
 } = $props();
 
-let input = $state("");
+let input = $state(formula ? prettyPrint(formula) : "");
 let error = $state(false);
 
 $effect(() => {
@@ -15,7 +15,10 @@ $effect(() => {
   if (fml) {
     formula = fml;
     error = false;
-  } else if (input !== null && input.length > 0) error = true;
+  } else {
+    formula = undefined;
+    error = input !== null && input.length > 0;
+  }
 });
 </script>
 

apps/web/src/routes/kripke/frame-input.svelte

@@ -3,6 +3,7 @@ import {
   type Frame,
   type Relation,
   type World,
+  getFrame,
   left,
   reverse,
   right,
@@ -11,27 +12,21 @@ import {
 import { type Vector, add, degree, rotate, sub, theta } from "./vector";
 
 let {
-  frame = $bindable<Frame>({ relations: new Set() }),
+  frame = $bindable<Frame>(getFrame(0)),
 }: {
   frame?: Frame | undefined;
 } = $props();
 
-let relations = $state(new Set<Relation>());
-
-$effect(() => {
-  frame = { relations };
-});
-
 let selected: World | null = $state(null);
 
 function toggle(rel: Relation) {
-  if (relations.has(rel)) {
-    relations.delete(rel);
+  if (frame.relations.has(rel)) {
+    frame.relations.delete(rel);
   } else {
-    relations.add(rel);
+    frame.relations.add(rel);
   }
   // Reassign to trigger reactivity
-  relations = new Set(relations);
+  frame = { relations: new Set(frame.relations) };
 }
 
 function handleNodeClick(node: World, event: MouseEvent) {
@@ -59,24 +54,24 @@ function handleSvgClick() {
 
 const positions: Record<World, Vector> = {
   a: {
-    x: 75,
-    y: 75,
+    x: 50,
+    y: 50,
   },
   b: {
-    x: 225,
-    y: 75,
+    x: 200,
+    y: 50,
   },
   c: {
-    x: 225,
-    y: 225,
+    x: 200,
+    y: 200,
   },
   d: {
-    x: 75,
-    y: 225,
+    x: 50,
+    y: 200,
   },
 };
 
-const center: Vector = { x: 150, y: 150 };
+const center: Vector = { x: 125, y: 125 };
 
 const radius: Vector = { x: 20, y: 0 };
 
@@ -100,14 +95,14 @@ function getPath(rel: Relation) {
 
   const angle = theta(sub(positions[r], positions[l]));
 
-  const offset = relations.has(reverse(rel)) ? degree(10) : 0;
+  const offset = frame.relations.has(reverse(rel)) ? degree(10) : 0;
 
   const dl = rotate(radius, angle + offset);
   const dr = rotate(radius, angle + Math.PI - offset);
   const from = add(positions[l], dl);
   const to = add(positions[r], dr);
 
-  if (!relations.has(reverse(rel)))
+  if (!frame.relations.has(reverse(rel)))
     return `M ${from.x} ${from.y} L ${to.x} ${to.y}`;
 
   return `M ${from.x} ${from.y} C ${from.x + dl.x * 2} ${from.y + dl.y * 2}, ${to.x + dr.x * 2} ${to.y + dr.y * 2}, ${to.x} ${to.y}`;
@@ -136,7 +131,7 @@ function getPath(rel: Relation) {
 
 <!-- svelte-ignore a11y_click_events_have_key_events -->
 <!-- svelte-ignore a11y_no_static_element_interactions -->
-<svg class="border border-foreground rounded" width="300" height="300" onclick={handleSvgClick}>
+<svg width="250" height="250" onclick={handleSvgClick}>
   <defs>
     <marker
       id="arrowhead"
@@ -148,11 +143,11 @@ function getPath(rel: Relation) {
       orient="auto"
       markerUnits="strokeWidth"
     >
-      <path d="M0,0 L0,10 L10,5 z" fill="#333" />
+      <path d="M0,0 L0,10 L10,5 z" fill="rgb(var(--foreground))" />
     </marker>
   </defs>
 
-  {#each Array.from(relations) as rel}
+  {#each Array.from(frame.relations) as rel}
     {#key rel}
       <path
         d={getPath(rel)}

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

@@ -0,0 +1,27 @@
+import { getFrame, nontrivials } from "@cannorin/kripke";
+
+function cyrb53(str: string, seed = 0): number {
+  let h1 = 0xdeadbeef ^ seed;
+  let h2 = 0x41c6ce57 ^ seed;
+  for (let i = 0; i < str.length; i++) {
+    const ch = str.charCodeAt(i);
+    h1 = Math.imul(h1 ^ ch, 2654435761);
+    h2 = Math.imul(h2 ^ ch, 1597334677);
+  }
+  h1 =
+    Math.imul(h1 ^ (h1 >>> 16), 2246822507) ^
+    Math.imul(h2 ^ (h2 >>> 13), 3266489909);
+  h2 =
+    Math.imul(h2 ^ (h2 >>> 16), 2246822507) ^
+    Math.imul(h1 ^ (h1 >>> 13), 3266489909);
+  // Combine the two 32-bit hashes into a single 53-bit integer
+  return 4294967296 * (2097151 & h2) + (h1 >>> 0);
+}
+
+export function getDailyFrame() {
+  // Use UTC ISO string so it's consistent across time zones
+  const dateStr = new Date().toISOString().split("T")[0];
+  const hash = cyrb53(dateStr);
+  const index = hash % nontrivials.length;
+  return getFrame(nontrivials[index]);
+}

packages/kripke/semantics.ts

@@ -124,6 +124,7 @@ function applyPermutation<T extends Frame>(
 
 export function generateAllFrames() {
   const canonicals: number[] = [];
+  const nontrivials: number[] = [];
   const map = new Map<number, number>();
 
   const total = 2 ** relation.length;
@@ -131,6 +132,7 @@ export function generateAllFrames() {
     if (map.has(id)) continue;
 
     const relations = decode(relation, id);
+
     const frame = { relations };
     const equivalentIds: number[] = [];
 
@@ -148,6 +150,11 @@ export function generateAllFrames() {
     for (const equivalentId of equivalentIds) {
       map.set(equivalentId, canonicalId);
     }
+
+    // Exclude the sizes with less than 10 frames (= can be bruteforced)
+    if (relations.size >= 3 && relations.size <= 13) {
+      nontrivials.push(canonicalId);
+    }
   }
 
   const isomorphic: Uint16Array = new Uint16Array(total);
@@ -157,8 +164,18 @@ export function generateAllFrames() {
     isomorphic[id] = value;
   }
 
-  return { canonicals, isomorphic };
+  return { canonicals, isomorphic, nontrivials };
 }
 
-const { canonicals, isomorphic } = generateAllFrames();
-export { canonicals, isomorphic };
+const allFrames = generateAllFrames();
+
+/** canonical frames among all the isomorphic ones */
+const canonicals = allFrames.canonicals;
+
+/** mapping to get the canonical frame */
+const isomorphic = allFrames.isomorphic;
+
+/** frames that are suitable for the puzzle */
+const nontrivials = allFrames.nontrivials;
+
+export { canonicals, isomorphic, nontrivials };