Spec: first-class claim + authority model (#113)

[ahoward]

Closes the spec side of #113. Umbrella: #112. Vision: dna/product/vision-spec-machine.md (v4.0), principles 1–2.

Spec only — no implementation. Human checkpoint #1: review and salt to taste.

What it specifies

A first-class claim: an assertion about a concept or edge, made under a registered authority tier, from a source. Competing claims coexist; resolution is a read-time projection, never a write-time deletion.

The refund scenario from the vision doc is the acceptance test: product=30d, legal=14d, implementation=45d → three claims, one conflict group, legal as the resolution, all three still present afterward.

Design decisions worth arguing about

• Strict authority, loose vocabulary (principle 1) is enforced literally: authority tiers are a registered, ranked, closed set; predicate and assertion are free-form and never validated.
• Authority rank is looked up at read time, not copied into the claim row — so re-ranking a tier changes resolution without rewriting history.
• Ties do not resolve. Equal top rank → resolution: null, unresolved: true. No tiebreak by recency or ID.
• Claims are immutable. Correction = delete + re-assert. In-place update would erase the contradiction record the feature exists to keep.
• Conflict is exact-assertion mismatch, not semantic. "30 days" vs "one month" is two claims, not a detected conflict. Called out as a known limitation.
• Built-in contradictions rule wires claims into the existing Datalog validator arm so verify/pr-verify can fail on unresolved contradiction.

Deliberately out of scope (kept foundational per constitution VI)

• Binding/constraining claims + the promotion gate → spec-machine gap #2: observation → requirement promotion gate #114
• Retraction with audit, demotion → spec-machine gap #2: observation → requirement promotion gate #114
• Regeneration from the graph → spec-machine gap #3 (keystone): regeneration → test → feedback prototype #115
• Production signals as claims → spec-machine gap #4: production-as-teacher ingestion #116
• Claim-to-claim supports/contradicts edges

Also in this PR

ROADMAP gains a Spec Machine section tracking #113–#116 as 067–070.

Next in the flow

Human approval → /speckit.plan → /speckit.tasks → Gemini antagonist review of the tc tests → implement.

Note: the gemini CLI is not installed on this machine; the antagonist review will need it available (or a human stand-in) before implementation starts.

🤖 Generated with Claude Code

[ahoward]

Plan + tasks pushed. PR now carries the full pre-implementation package.

Added

• plan.md — constitution check, structure, risks, one justified complexity (the authorities registry vs a hardcoded tier constant)
• research.md — 10 decisions, including the three the spec deferred: conflict comparison is trim-then-exact case-sensitive (D3), rank is joined at read time and never stored on the claim (D2), idempotency by pre-insert 5-tuple lookup (D4)
• data-model.md — claims (8 cols, Int PK) + authorities (String PK, rank/description), derived conflict-group shape, cascade rules, schema v1.12.0 → v1.13.0
• contracts/claims.md + contracts/authorities.md — all 8 sys.call paths
• quickstart.md — the refund 30/14/45 walkthrough end to end, including re-ranking and the tie case
• tasks.md — 42 tasks in 7 phases, tc tests authored before implementation per constitution IV

De-risked before writing code: the built-in contradictions Datalog rule and the read-time rank join were executed against an in-memory CozoDB with the exact relation shapes. The rule returned only the contradicting concept and correctly omitted a concept whose claims agreed; the rank join ordered legal(40) > product(30) > implementation(20).

Docs updated: CLAUDE.md gains a Spec Machine section with the #113–#116 table and the two governing principles; README links the vision doc; ai/MEMORY.md records the invariants later features must not break (notably the 8-column arity coupling #114 will hit); ROADMAP reflects status.

Blocked at T023: the gemini CLI is not installed on this machine. Implementation cannot start until the antagonist review of the tc tests happens — install it or substitute a human antagonist.

[ahoward]

Self-review pass (Fable, adversarial) — findings applied

Ran an independent adversarial review of the whole package against the codebase. It found real problems. Verified each against the tree before acting; all confirmed. Fixes pushed.

Blockers (fixed)

B1 — SC-005 was unachievable and the task list dead-ended. A third built-in rule and a schema bump break locked fixtures that pin exact values: tests/mind/verify (rules_passed: 2, enumerated cycles+orphans), tests/mind/rules/list (counts 2 and 3), tests/mind/init (schema_version: 1.12.0), and the concept-delete cascade shape. No task covered them, and constitution IV forbids quietly editing tests. Now an explicit human-approved task (T003) with the fixtures enumerated, and SC-005 reworded to distinguish a mechanical fixture update from a test rewrite that hides failures.

B2 — concept deletion would orphan edge-claims. concepts/delete.ts cascades edges with a direct :rm edges. A cascade that only removed subject_type = "concept" claims leaves claims on those removed edges dangling — violating the spec's own edge case. Concept deletion now cascades claims on the edge IDs it already collects.

Should-fix (all applied)

• Dangling claims after prune and re-extraction. Both delete concepts/edges directly, bypassing the handlers (verified: prune.ts:148-175, extract.ts:330-365). Annotations already dangle there. Rather than copy that bug into a feature about integrity, cascade logic is now one cascade_claims() lib function called from all four sites.
• The two read paths disagreed about what a contradiction is. Conflicts compared trimmed assertions; the Datalog rule compared raw (a1 != a2), so "30 days" vs "30 days " was agreement to one arm and a violation to the other — SC-004 fails. Fixed at the boundary: trim on write, store trimmed, exact-compare everywhere (new FR-016b).
• US6 overclaimed. The rule flags all contradictions, including rank-resolved ones. Spec text said "unresolved". Aligned to the shipped behavior, which is the right one — the rule reports that the graph disagrees with itself; rank filtering is what conflicts is for. Also corrected a research.md line that wrongly said the built-in rule joins authorities.
• A stated mitigation was false. Built-in rules are seeded by raw :put and are not syntax-validated — validate_rule_syntax only runs in rules/create. An arity break would surface quietly as a caught per-rule error. Corrected, and the real safety net (spec-machine gap #2: observation → requirement promotion gate #114 depends on it) is now a tc case asserting contradictions runs with error: null.
• claims has no declared primary key. No =>, so all 8 columns are the composite key — repo convention. id uniqueness is allocator-enforced, :rm needs the full row, and delete is read-then-remove like annotations/delete.ts. Documented; the earlier "surrogate PK" wording was wrong.
• Tasks violated constitution IV. Schema, migration, and the entire lib layer — including group_conflicts, the heart of the feature — sat before test authoring and the Gemini lock. Reordered: tests first, lock, then implementation.
• Migration test had no way to get a v1.12.0 db. Mechanism now specified (init fresh → downgrade in place → reopen via open_mind, since /mind/init does not migrate).
• Cascade result shape decided: claims_removed on both delete handlers.

Nits (fixed)

--rules → --rule in quickstart; authority upsert preserves description when omitted (quickstart step 8 blanked its own); contradictory subject_id filter wording; a note that "authority" now means three unrelated things in mind.db; single-subject claims stated in Out of Scope against #113's plural phrasing.

Verdict

Reviewer's call: sound core (schema fits repo precedent, rule matches the [id, name] contract, migration matches the v1.10→v1.11 pattern, Out of Scope is genuinely YAGNI-clean), but not implementable as written. That is now addressed. Still blocked at T009 on the Gemini antagonist review before any code.

[ahoward]

Antagonist review done (Fable, two rounds) — tests LOCKED

Constitution amended to 1.1.0 first: the antagonist is now Fable, run as a subagent, not the Gemini CLI. Principle IV is unchanged in substance. Swapped across constitution, development-loop.md, CLAUDE.md, ROADMAP.md, and ai/MEMORY.md (including how to invoke it and a note to verify its findings against the tree — it is a reviewer, not an oracle).

Round 1 — 3 blockers, 11 should-fixes

• pr-verify fixtures were missed. tests/calabi/pr-verify/data/{00,01,02} pin rules_passed and enumerate exactly cycles+orphans. pr-verify runs every rule through the same path as verify, so the new builtin lands there too. My D11 sweep covered verify and missed its sibling.
• edges/delete fixture pins {"deleted": true} alone — so claims_removed either fails the locked fixture or gets quietly dropped to stay green.
• The prune cascade case could never pass. prune only removes concepts whose provenance is entirely stale; the setup created no provenance at all, so nothing was ever pruned. A false red that would have read as an implementation bug during the green loop.

Should-fixes were the holes a wrong implementation slides through: resolve-tie (an implementation breaking ties by lowest id passed everything), resolve treated as a global max instead of per-group, agreement silently deduplicated, source dropped from the identity tuple, missing conflict filters and unpinned group ordering, the new builtin not registered as protected, edge subjects validated against the concepts relation, trim running after the empty check, and every cascade count matched by <number> so a hardcoded 0 passed.

Round 2 — one blocker survived

The prune fix was still wrong: /mind/provenance/create validates the file against body.db, so create_provenance on a nonexistent URL returns not_found, and with set -e the case emitted nothing at all. Now uses the add-then-delete pattern tests/mind/prune/run already had.

Round 2 otherwise verified every new case: pinned ids match the setup order, orderings match the newly pinned contract rules, key sets satisfy deep_match's exact-key requirement, boundary cases are at the real boundaries (257/1025/65), and a full grep across every suite found no remaining stale pins of the schema version, builtin count, or cascade shape.

State

82 tc cases across claims (52), authorities (15), migration (8), rules (5), verify (2) — red until Phase 2, as intended. Contract now pins conflict group ordering (subject_type, subject_id, predicate ascending) and the resolve-tie list shape. T009 is done; the tests are locked — changing them now takes a human checkpoint.

Needs your approval

The locked-fixture updates (research D11): verify, pr-verify, rules/list, init, concepts/delete, edges/delete. These are mechanical consequences of a third builtin rule and a schema bump, not edits to make a failing implementation pass — but constitution IV says you sign off, so flagging rather than assuming.

Next: Phase 2 (schema + migration) → Phase 3 (lib) → handlers → CLI → green.

[ahoward]

Implemented. 432/432 tests pass.

Phases 2–8 complete against the locked suite. No test was changed after the lock.

Schema v1.13.0 — claims (8 columns, all-key) and authorities (name => rank, description), five seeded tiers, and the contradictions built-in rule. Relation definitions and the rule body live in src/lib/claims.ts and are imported by both init.ts and migrate.ts, so a fresh v1.13.0 db and a migrated one cannot drift.

Eight paths: /mind/claims/{create,get,list,delete,conflicts}, /mind/authorities/{create,list,delete}. CLI: brane claim and brane authority, wired under admin plus the backward-compat top level.

cascade_claims() is the single deletion seam — called from concepts/delete (including the edges that deletion cascades), edges/delete, prune, and re-extraction. That last pair matters: both delete concepts directly without going through the handlers, which is exactly how annotations already dangle today.

One bug found on the way, fixed

src/handlers/mind/rules/create.ts escaped single quotes SQL-style (''). CozoDB uses backslash escapes, so 'it''s' is a parse error — meaning any rule body containing an apostrophe silently failed to save, and had since the handler was written. My own escaper had copied the same mistake. Both now use esc_cozo() in src/lib/mind.ts. Verified against Cozo directly before fixing.

This surfaced because a locked test asserted a user-defined rule joining *claims and *authorities — the one case whose body needed quoted literals. The antagonist's insistence on that case is what caught it.

Verified live, not just green

The full quickstart round-trips: 30/14/45 written → all three listed → one conflict group with legal resolving → --resolve returns 14 days → the losers are still stored → verify --rule contradictions fails with RefundWindow. Then registering security at rank 45 moves the resolution with no claim rewritten, a second tier at the same rank makes it unresolved: true with resolution: null, a rank-only upsert preserves the description, and it's fine round-trips through the escaper.

Docs

CLAUDE.md gains a Claims section with the invariants and the Cozo gotcha; ROADMAP marks 067 complete; ai/MEMORY.md records four findings worth keeping (the arity coupling, the escaping rule, provenance validation in tests, and prune's all-stale requirement).

#114, #115, #116 are unblocked.