perf(viewer): deduce spaces lazily instead of the full database in SSR

packages/viewer/src/debug.ts

@@ -47,10 +47,24 @@ export type ServerEvent =
       // deduction work, since the eager run finishes after the SSR response is
       // sent, so a completion-time count is dropped. `reset` marks a full re-run
       // (e.g. from a refresh) vs an incremental top-up.
+      //
+      // Client-only after the lazy-deduction change: the full run no longer
+      // fires during SSR, so this should disappear from runtime logs entirely
+      // (see `deduce_space`).
       evt: 'deduce_run'
       planned: number
       reset: boolean
     }
+  | {
+      // One per space deduced on demand. SSR now proves only the single space a
+      // page needs, so a page render should emit exactly one of these instead of
+      // a `deduce_run` over the whole database. `derived` is the trait count
+      // proved (0 on a `contradiction`).
+      evt: 'deduce_space'
+      space: number
+      derived: number
+      contradiction: boolean
+    }
 
 // Emit one structured Workers Logs event. We log the *object* (not a JSON
 // string) so Workers Logs indexes each field as a queryable key, the same way

packages/viewer/src/stores/deduction.test.ts

@@ -97,18 +97,15 @@ describe(Deduction.create, () => {
 
     await store.run()
 
-    // FIXME: this documents the current behavior, but it's surprising that we're
-    // getting duplicated entries.
+    // Each space is deduced exactly once: the store advances to "checking" the
+    // space, then records it as checked, with no duplicate passes.
     expect(stores.map(({ checking, checked }) => [checking, checked])).toEqual([
       [undefined, new Set()],
       [undefined, new Set()],
       ['Space 1', new Set()],
       ['Space 1', new Set([1])],
-      ['Space 1', new Set([1])],
       ['Space 2', new Set([1])],
       ['Space 2', new Set([1, 2])],
-      ['Space 2', new Set([1, 2])],
-      ['Space 2', new Set([1, 2])],
     ])
 
     expect(
@@ -118,8 +115,6 @@ describe(Deduction.create, () => {
       [1, 3, true],
       [2, 2, false],
       [2, 1, false],
-      [2, 2, false],
-      [2, 1, false],
     ])
   })
 

packages/viewer/src/stores/deduction.ts

@@ -1,3 +1,4 @@
+import { browser } from '$app/environment'
 import { type Readable, writable } from 'svelte/store'
 import {
   ImplicationIndex,
@@ -85,10 +86,68 @@ export function create(
   theorems.subscribe($theorems => {
     implications = indexTheorems($theorems)
 
-    // Ensure that the trait store is updated before deductions run
-    setTimeout(run, 0)
+    // The eager full-database prover only makes sense for the interactive
+    // client. During SSR it re-derives every space on each request and dominates
+    // Worker CPU, so we deduce individual spaces lazily via `checked` instead.
+    if (browser) {
+      // Ensure that the trait store is updated before deductions run
+      setTimeout(run, 0)
+    }
   })
 
+  // Deduce a single space, deriving its traits from the asserted ones (or
+  // recording a contradiction). Idempotent: already-checked spaces are skipped.
+  function deduceSpace(space: Space): void {
+    const state = read(store)
+    if (state.contradiction || state.checked.has(space.id)) {
+      return
+    }
+
+    store.update(s => ({ ...s, checking: space.name }))
+
+    const map = new Map(
+      read(traits)
+        .forSpace(space)
+        .map(([p, t]) => [p.id, t.value]),
+    )
+    const result = deduceTraits(implications, map)
+
+    if (result.kind === 'contradiction') {
+      store.update(s => ({ ...s, contradiction: result.contradiction }))
+      serverLog({
+        evt: 'deduce_space',
+        space: space.id,
+        derived: 0,
+        contradiction: true,
+      })
+      return
+    }
+
+    const newTraits: DeducedTrait[] = result.derivations
+      .all()
+      .map(({ property, value, proof }) => ({
+        asserted: false,
+        space: space.id,
+        property,
+        value,
+        proof,
+      }))
+
+    addTraits(newTraits)
+
+    store.update(s => ({
+      ...s,
+      checked: new Set([...s.checked, space.id]),
+    }))
+
+    serverLog({
+      evt: 'deduce_space',
+      space: space.id,
+      derived: newTraits.length,
+      contradiction: false,
+    })
+  }
+
   function run(reset = false): Promise<void> {
     if (reset) {
       store.set(initialize(read(spaces)))
@@ -102,13 +161,7 @@ export function create(
     }))
 
     const checked = read(store).checked
-
-    const unchecked: Space[] = []
-    allSpaces.forEach(s => {
-      if (!checked.has(s.id)) {
-        unchecked.push(s)
-      }
-    })
+    const unchecked = allSpaces.filter(s => !checked.has(s.id))
 
     // Log the planned work *synchronously*, before the async loop. On the eager
     // SSR model the loop finishes after the response is sent (the page resolves
@@ -118,44 +171,23 @@ export function create(
     serverLog({ evt: 'deduce_run', planned: unchecked.length, reset })
 
     return eachTick(unchecked, (s: Space, halt: () => void) => {
-      store.update(state => ({ ...state, checking: s.name }))
-
-      const map = new Map(
-        read(traits)
-          .forSpace(s)
-          .map(([p, t]) => [p.id, t.value]),
-      )
-      const result = deduceTraits(implications, map)
-
-      if (result.kind === 'contradiction') {
-        store.update(s => ({ ...s, contradiction: result.contradiction }))
+      deduceSpace(s)
+      if (read(store).contradiction) {
         halt()
-        return
       }
-
-      const newTraits: DeducedTrait[] = result.derivations
-        .all()
-        .map(({ property, value, proof }) => ({
-          asserted: false,
-          space: s.id,
-          property,
-          value,
-          proof,
-        }))
-
-      addTraits(newTraits)
-
-      store.update(state => ({
-        ...state,
-        checked: new Set([...state.checked, s.id]),
-      }))
     })
   }
 
   return {
     subscribe: store.subscribe,
     run,
     checked(spaceId: number) {
+      // Deduce on demand so a single SSR page render only proves the space it
+      // needs, rather than blocking on a full-database background run.
+      const space = read(spaces).find(spaceId)
+      if (space) {
+        deduceSpace(space)
+      }
       return subscribeUntil(
         store,
         state => state.checked.has(spaceId) || !!state.contradiction,

packages/viewer/src/stores/index.ts

@@ -1,3 +1,4 @@
+import { browser } from '$app/environment'
 import { type SerializedTheorem } from '@pi-base/core'
 import type * as Gateway from '@/gateway'
 import {
@@ -81,7 +82,11 @@ export function create(pre: Prestore, gateway: Gateway.Sync): Store {
     if (result) {
       set(result.properties, result.spaces, result.theorems, result.traits)
 
-      deduction.run(true)
+      // Eager full-database deduction is client-only; during SSR individual
+      // spaces are deduced lazily on demand (see stores/deduction.ts).
+      if (browser) {
+        deduction.run(true)
+      }
 
       return {
         etag: result.etag,