Case Generation, Proof & Canon

Every other open-world detective game ships a fixed shelf of hand-authored cases. V8 (Ariadne) ships a factory — and the one promise that makes a factory of mysteries playable rather than terrifying is this: you will never be handed a case you cannot solve, and never lose one to a clue the game never showed you. Fairness in V8 is not a QA hope or a designer's gut feel. It is a property the system proves with a real constraint solver before the case is allowed to exist. That is the feature this page is about — the mint, the proof, and the canon that together keep a generated labyrinth fair, solvable, and consistent with the city the player already knows. It is the difference between "the generator usually produces good cases" and "nothing unsolvable, unfair, or canon-breaking can reach a player," which is exactly what V8's definition of done demands (V8_features.md § "Definition of done").

The mechanism is one sentence: the LLM proposes; a constraint solver disposes. A case has a symbolic skeleton — who did it, with what, and the clues that distinguish them — that must be provably correct, and an experienced surface — prose, art, voice, interrogation — that agents realize from that skeleton. Three subsystems own the skeleton, and they are where the real, deterministic, CPU-only code concentrates. Clew is the generative engine: it picks the answer first and weaves a self-consistent world backward from it. Minos is the verifier: it proves the player-visible clues admit exactly one answer and that it is the intended one. Palimpsest is the canon graph: the persistent city every case is grounded in and writes back to, so the world remembers what the player did. This page is the feature-side view; the deep internals — the SAT layer, the alibi-sign bug, the exact data contracts — live in the architecture companion. Hub: ../V8_features.md.

What ships, honestly#

The solvability proof is the strongest real thing V8 has, and it is genuinely real — not a boolean stub renamed "verifier." libs/v8/case-csp is a complete finite-domain constraint solver: backtracking search with node consistency, minimum-remaining-values ordering, and forward checking (csp-solver.ts:212). Its spec proves the canonical Zebra (Einstein) puzzle — exactly one solution, "the Norwegian drinks water, the Japanese owns the zebra" (csp-solver.spec.ts:168) — so the engine is anchored against a known-correct result it cannot fake. libs/v8/case-bundle's forge calls that proof before a single word of prose or byte of art is generated, throwing on a non-unique skeleton (case-bundle.ts:237). libs/v8/case-gates registers the seven release gates on the shared @oshun/content-release-gates platform every Oshun product uses, not a bespoke per-product checker (index.ts:99). And a second, independent solver — a real DPLL SAT engine in libs/yemaya/case-verifier (sat/dpll.ts) — decides the same uniqueness question, so the verdict is cross-checked, not asserted.

What is a seam, not a fabrication: the media a finished case needs (Stability/Flux portraits, Hunyuan3D/Meshy 3-D props, Suno music, ElevenLabs VO) arrives through injected CaseMediaGenerator boundaries. An absent provider yields a not-configured asset slot — never a fabricated asset (case-bundle.ts:262). The prose writer is required: no writer wired means a loud CaseBundleNotConfiguredError (case-bundle.ts:242), not invented flavor. The clingo ASP backend is an optional accelerator that falls back to the in-process DPLL and honestly reports which engine decided. Palimpsest's graph, hybrid retrieval, per-claim consistency check, and outcome write-back are all real and tested (@yemaya/canon-graph); its embedding signal is feature-hashing — a documented approximation, not a neural model — and durable Postgres/Neo4j persistence is the named deployment target, not something these libs pretend to be.

Clew — a case generated answer-first#

Solve-first, not author-first#

A human mystery writer invents a crime and hopes the clues add up. Clew inverts that. It picks the culprit before anything else and gives them the three things a culprit must have — means, opportunity, and no verified alibi — while handing every innocent exactly one fair, discoverable exoneration: a verified alibi, demonstrable absence, or no access to the weapon. Innocents usually keep a motive, so they still read as plausible suspects; they are the fair red herrings, each cleared by a single fact the player can actually find. The construction runs off a seeded RNG, so the same (seed, canon) reproduces the same case bit-for-bit, and a timeline conflict the true culprit could not have been present for throws rather than shipping a broken case. (Those two passes — Truth-Weaver and Clue-Smith — are detailed in the architecture companion; the feature point here is that the answer is fixed first and the world is built to fit it, which is what makes a uniqueness proof possible in the first place.)

The case as a constraint network#

Clew's decisive output is not prose — it is a constraint network, the exact object Minos solves. In the libs/v8 vertical this is a MysterySkeleton (mystery-skeleton.ts:69): a set of solution dimensions, each with a finite domain (culprit: [colonel, duchess, butler, doctor], plus weapon, location, motive); the intended ground truth, one value per dimension; and a list of clues, each either presented to the player or withheld, each carrying a logical constraint over the dimensions. The constraint vocabulary is small and honest: is / is-not pin or eliminate a value, one-of narrows a dimension, if-then is a conditional deduction, same ties two dimensions together, and allowed is the general escape hatch — an explicit set of permitted tuples rather than a hidden predicate the data can't see (mystery-skeleton.ts:33). A worked example from the spec interlocks five of these into one answer: weapon=poison (the coroner) ⇒ location=conservatory (poison was stored there) ⇒ culprit=doctor (only the doctor had conservatory access) ⇒ motive=blackmail (mystery-skeleton.spec.ts:20).

The load-bearing detail is the presented / withheld tag on every clue, because only the clues the player can reach count toward solvability. A true but withheld "confession" is excluded from the proof entirely (mystery-skeleton.spec.ts:76). That single distinction is the whole game: a case is fair only if it can be solved from what the player is actually shown — not from facts the system happens to know.

The solvability proof — why a V8 case is provably fair#

This is the strongest real feature in V8, so it earns the most space.

Three verdicts, one question#

Minos's headline obligation is uniqueness: with only the player-reachable clues, is the culprit the only satisfying answer? Exactly three verdicts matter. Zero satisfying solutions means the case is unsolvable (over-constrained — the visible clues contradict each other). Two or more means it is ambiguous (under-determined — the player could rightly accuse more than one suspect). Exactly one means unique — the answer is entailed by the visible clues, and that is the only verdict that ships. A boolean "does this look fair?" check cannot tell these three apart. Counting models can, which is precisely why V8 spends real solver code here instead of a heuristic.

A real solver, anchored against the Zebra puzzle#

solveCsp (csp-solver.ts:212) is a textbook-complete backtracking search. It seeds node consistency from the unary constraints (pruning impossible values up front), then searches with minimum-remaining-values ordering — always branching on the most-constrained variable, breaking early on a singleton (selectVar, :260) — and forward checking, which after each assignment prunes from each unassigned neighbour any value a shared constraint would now definitely violate, recording every removal so it can be undone on backtrack (forwardCheck, :278). The soundness hinge is constraintViolated (:120): it returns true only when a constraint can no longer be satisfied, leaving undetermined constraints alone, so the search is both sound and complete. A degenerate constraint that touches no assigned variable — a 0-ary relation the incremental checks would never see — is still enforced by a full constraint sweep at each leaf (:314), pinned by a dedicated soundness-guard test (csp-solver.spec.ts:68).

The proof that this is a genuine engine and not a renamed boolean is the Zebra puzzle: the solver returns the canonical answer — Norwegian in the first house, the Norwegian drinks water, the Japanese owns the zebra — and exactly one solution (csp-solver.spec.ts:168). A solver that produces that specific answer across fourteen interlocking constraints is doing real search. The same domain-agnostic engine that solves the Zebra puzzle solves a murder. proveUniqueSolution (:356) drives the uniqueness test efficiently: it asks the search for up to two solutions — none ⇒ unsatisfiable, one ⇒ unique (with the witness assignment), two ⇒ under-determined — stopping the moment a second model appears, because one counterexample is all uniqueness needs.

Solvable and correct: the two-part fairness check#

proveCaseUniqueness (mystery-skeleton.ts:239) is where the fairness guarantee is actually enforced, and it checks two things, not one. First it compiles only the presented clues into a CSP (compileMysteryToCsp, :136) — the model the player can solve from — and demands a unique solution. Second, it demands that the unique solution equals the intended ground truth. A case is rejected if it is under-determined, if it is unsatisfiable, or if the visible clues prove a perfectly unique culprit who simply is not the one Clew intended — a real generation bug the prover surfaces with a one-line, honest reason (:251) rather than asserting away.

The spec pins every one of these failure modes. A case whose visible clues prove the doctor while the author's ground truth says "butler" is caught: uniqueSolutionProven is false, and groundTruthSatisfiesAllClues (mystery-skeleton.ts:180) confirms the shipped clues contradict the shipped answer (mystery-skeleton.spec.ts:154). And the most important one for fairness: moving the two deducing clues from presented to withheld flips a uniquely-solvable case to under-determined for the player, even though the full clue set still solves uniquely — proving the case isn't broken, it's just unfair as presented (mystery-skeleton.spec.ts:178). This is the whole reason the compiler defaults to presented-only: solvability is judged from what the player can actually reach.

Two solvers, one verdict#

The CSP is not alone. The architecture names a second, independent route: a propositional DPLL SAT solver (libs/yemaya/case-verifier/sat/dpll.ts) — the real 1962 algorithm with unit propagation and pure-literal elimination (solveFrom, :98) — that treats the case as a Boolean CNF over (suspect, attribute) atoms and tests each suspect by assumption: suspect s is a viable culprit iff CNF ∧ culpritIs(s) is satisfiable (isSat, :129; proveUniqueness, uniqueness.ts:47). Count the survivors — 0 unsolvable, 1 unique, ≥2 ambiguous — and return every offender for the repair loop. Two engines reducing the same question to model-counting is itself a cross-check, and it earned its keep: this DPLL layer caught a real alibi-rule sign error during development that a boolean "looks fair" stub would have sailed straight past (the mechanism is dissected in the companion). The verifyCase orchestrator (minos.ts:25) runs this G1 uniqueness proof alongside deductive-completeness and the existing Knox/Van-Dine fair-play checker; the clingo ASP sidecar can offload the proof to a container and falls back to the in-process DPLL when no binary is present, reporting backend: 'dpll' honestly rather than fabricating a verdict.

Prove first, generate never-if-unsolvable#

The discipline becomes executable in the forge. forgeCaseBundle (case-bundle.ts:236) calls proveCaseUniqueness as its very first act and throws CaseNotSolvableError on a non-unique skeleton before any prose or media is generated (:237). The spec proves a watchful prose writer is never even invoked for an unsolvable case (case-bundle.spec.ts:169), which means fairness discipline and cost discipline are the same act: you never pay to generate art for a case that can't be solved. Only a proven case proceeds to realization, and each produced asset is then C2PA-stamped — its bytes hashed and a canonical manifest Ed25519-signed (stampAsset, :184) — so that verifyCaseAssetManifest (:215) flips to false if any signed field is later tampered (case-bundle.spec.ts:147).

The seven gates#

Solvability gates generation; a wider suite gates release. buildV8CaseGates (case-gates/src/index.ts:99) registers seven gates — G1 fair-play, G2 solvability, G3 clue-grounding, G4 suspect voice, G5 misdirection, G6 prose, G7 safety — on the shared @oshun/content-release-gates service, composed from the platform's gate builders rather than forked. The crucial wiring is that G2 consumes the very uniqueSolutionProven flag the CSP produced (index.ts:124), so the symbolic proof is literally what the release gate stands on. The suite is real: its spec asserts each distinct fault blocks its own gate — solving on a withheld clue trips G1, a non-unique case trips G2, a solution citing an invented clue trips G3, and a maze of too many red herrings trips G5 (case-gates.spec.ts:30). A case clears only when all seven required gates pass (evaluateV8Case, :183).

Canon consistency — cases that fit the world and remember#

Grounded in a persistent city#

A generated case is not a disconnected vignette. Palimpsest (@yemaya/canon-graph) is the persistent world every case is grounded in — a typed property graph of characters, locations, factions, timeline events, prior-case outcomes, and open threads. Generation never sees the whole graph; a bounded CanonContext is retrieved per case (retrieval.ts), ranked by a genuine hybrid of lexical tf-idf and a feature-hashing embedding cosine, with the required cast and locations force-included so a hard continuity constraint is never pruned by the top-K cut. Prior-case outcomes are first-class retrievable nodes carrying their current dynamic state, so a new case reuses the city's actual history rather than re-inventing it.

The continuity gate, and a world that remembers#

Two real mechanisms turn canon-consistency from a wish into a feature. First, the consistency check (consistency.ts) is real per-claim contradiction logic judged against the exact canon snapshot a draft was grounded on: re-parenting a known location, negating a recorded character fact, or flipping a recorded case outcome is a HARD violation, while a plausible new fact is SOFT and surfaced for review rather than silently rejected. Second, write-back (writeback.ts) makes a played case durable world history — convicted suspects become convicted, and the signature continuity move is the wrongly-accused suspect, whose state becomes freed-vengeful and who opens a vengeance thread the director can weave into a future case. Accuse the wrong man in case #7 and he can resurface — freed and vengeful — in case #19. Every commit materializes a content-hashed snapshot (snapshot.ts): a SHA-256 over a canonicalized serialization that flips on any node, edge, or state change, which together with the seed and model versions forms the (seed, model-versions, canon-hash) key that makes a generated case deterministically replayable. (Palimpsest's retrieval ranking, the full consistency taxonomy, and the snapshot canonicalization are detailed in the companion; the feature point is that the world has a memory the player can feel.)

The mint, end to end#

The fairness guarantee is a pipeline, not a single check — generate, prove, gate, ship, and write back, with the proof standing between generation and any spend on realization.

The arrows that make it a proof rather than a hope are the two pointing back to REJECT: an unsolvable skeleton never reaches the forge, and a gate failure never reaches the player. Everything downstream — the writers' room, the asset fabric, the living suspects — only ever sees a skeleton Minos has already certified.

Related#

• ./overview-and-player-promise.md — the V8 product, the endless case board, and the player promise this page makes good on.
• ./realization-and-living-suspects.md — how the verified skeleton becomes prose, art, voice, and live interrogation: the experienced surface built on top of the proven core.
• ../architecture/clew-minos-palimpsest-symbolic-core.md — the deep architecture companion: Truth-Weaver / Clue-Smith internals, the DPLL/ASP layer, the alibi-rule sign bug, the seven-gate orchestrator, and the exact data contracts.
• Hub: ../V8_features.md