arborist/docs/spec-methodology.md

Spec methodology — authoring π*, V, and policy fields

Reference doc commissioned by ticket #000019. The SQD whitepaper identifies spec brittleness as the real bottleneck: with perfect optimization, a wrong π* or V produces verified nonsense. This doc codifies the discipline arborist already practices, so new authors don't re-derive it from the codebase every time.

This is a checklist, not a rulebook. Where it conflicts with something concrete in CLAUDE.md, CLAUDE.md wins.

0. Why this doc exists

arborist has, over its history, evolved:

• One canonical text projection (wikitext-base@v1).
• One claim-lattice projection (claim-lattice@v1).
• A four-strategy verifier (quote / span / entity / paraphrase) with layered fallback (arborist/qa/verify.py).
• Seven-plus policy fields folded into governance_policy_hash.

Every one of those landed through bench-driven iteration with no authoritative "how to author the next one" guide. New authors either:

• Replicate prior work by mimicry (good but loses the why).
• Re-derive the discipline from the audit-chain failures (slow).
• Skip steps and ship something that breaks (bad).

This doc closes the gap. It's the source of truth for the questions every new π*, V, or policy field author should answer before landing.

1. Authoring a new π* (canonical projection)

A π* takes raw bytes and returns canonical bytes — collapsing "different surface forms with same meaning" into a single representative. New π*'s register through arborist.pi_star.register (ticket #000015).

1.1 Versioning rule

Any byte-affecting change requires a new version number. Never mutate wikitext-base@v1 in place; land wikitext-base@v2 and ship both for the deprecation window.

The registry key is name@version. It enters canonicalization_version (per-π* slot in v9.8 cache_key) and/or governance_policy_hash (where multiple π*'s combine). Changing the key value invalidates every cache record that hashed it.

This is the right behavior — the alternative is silent drift where two records claim the same canonicalization but produce different bytes.

1.2 Round-trip test

Every π* MUST satisfy canonicalize(canonicalize(x)) == canonicalize(x) on inputs in its declared domain. The assert_round_trip helper in arborist.pi_star.protocol exercises this. If the π* is not idempotent (e.g., claim-lattice@v1 projects text → JSON; running it on its JSON output produces different bytes), document the projective nature explicitly in the module docstring and skip the round-trip assertion in tests.

1.3 Equivalence class declaration

State, in the module docstring, what the projection collapses and what it preserves. Examples:

• wikitext-base@v1 collapses MediaWiki templates, citations, link markup, and HTML entities → preserves the prose token sequence.
• claim-lattice@v1 collapses text claim-line phrasing → preserves parsed claim text + pointer IDs + parse status.

Authors that don't write this section invariably under-specify and ship surprises.

1.4 Policy-fold rule

Pick exactly one of:

• canonicalization_version (per-shard, single-π* records like text ingestion). Bumping invalidates ingest-time canonicalization.
• chunking_version (per-shard, single-π* records like chunker output). Same semantics.
• governance_policy_hash (multi-π* policy bundles, runtime decisions). Bumping invalidates everything within governance scope.
• Sibling field on a non-cache-keyed table (e.g., selfmodel_records, memory_records). Doesn't invalidate cache.

The default for a new π*: declare it in governance_policy_hash unless it slots clearly into one of the dedicated version fields.

1.5 Deprecation policy (current)

v1 of any π* stays valid until explicit retirement. Retirement is its own ticket and includes:

• Re-canonicalization tooling for v1 records (so they can move forward to v2).
• A grace window during which both versions are queryable.
• Audit-chain entries for every record migrated.

There is no automatic deprecation; old keys live forever in the registry unless explicitly removed (and removal requires its own ticket).

1.6 Worked example: wikitext-base@v1

See arborist/pi_star/text.py and arborist/wikitext.py.

• Domain: text-or-wikitext. Input is UTF-8 bytes; output is UTF-8 prose bytes.
• Equivalence class: collapses MediaWiki markup and templates; preserves token sequence.
• Round-trip: idempotent (prose canonicalized again is the same prose).
• Policy fold: lands in governance_policy_hash via policy["base_version"] per the QA runner.
• Lineage: BASE_VERSION = "wikitext-base-v1" in arborist/wikitext.py. Bump = new version key + new module registration.

1.7 New-π* author checklist

• Module docstring states domain, equivalence class collapsed, what's preserved.
• name, version, domain declared as class attributes.
• Registers via arborist.pi_star.register at module-import time.
• Round-trip test (or explicit projective declaration with reason).
• Determinism test: same input + same registry → byte-identical output across runs.
• Policy-fold rule chosen and documented.
• If composition with existing π*'s is intended: composition manifest + fingerprint test.
• Spec-methodology checklist (this section) referenced in the ticket that lands the new π*.

2. Authoring a new V (verifier strategy)

A verifier strategy V is one of the layered checks in arborist/qa/verify.py. New strategies land as new branches in the strategy chain, NOT mutations of existing ones.

2.1 Soundness statement

State precisely: "V(a)=1 implies holds on a." For the existing strategies:

• quote: V=1 ⇒ the quoted span verbatim appears in the cited evidence.
• span: V=1 ⇒ the answer's full evidence-anchored span is a verbatim line in cited evidence.
• entity: V=1 ⇒ the proper-noun entities cited in the answer cluster within proximity in evidence (under stated entity_policy).
• paraphrase: V=1 ⇒ the answer's prose has token-coverage above threshold against cited evidence.

Soundness statements anchor claim audits — when an auditor sees audit_mode=STRICT and the verifier_method is one of these, they know exactly what was checked.

2.2 Completeness statement

State the honest gap: what does V fail to accept that should be true under the intended semantics? Examples:

• quote: fails when paraphrased correctly.
• paraphrase: fails when the answer is correct but uses near-zero shared tokens with evidence.

A verifier with no completeness gap is suspect — usually means the gap wasn't measured.

2.3 Strategy ordering

Layered verifiers try strategies in fixed order. New strategies must declare their position and the consequence of reordering. The existing chain is quote → span → entity → paraphrase; the ordering matters because each strategy can either succeed (lock the verdict) or fall through.

A new strategy author must answer: "If I run BEFORE the existing chain, what false-positives does my strategy introduce? If I run AFTER, do I still get any traction?" The answer goes in the strategy's module docstring.

2.4 Falsification surface

What signal would falsify V's soundness claim? Concretely:

• Bench-suite regression below 5pp signal floor (per docs/bench-maxing.md).
• A counter-example fixture where V=1 but the semantic property doesn't hold.
• Audit-chain disagreement against another sound verifier on the same input.

Strategy authors include a falsifier set in the strategy's tests.

2.5 Sidecar discipline (CLAUDE.md hard rule)

Soft signals never enter V's hard output. The arborist.qa.inspect.diagnose_* family produces sidecar classifications (deflection, title-relevance, etc.) that are read-only — they cannot write to providence_cache or audit_events.

When tempted to add a "soft signal" to V, ask: "Does this surface a probabilistic / heuristic judgment?" If yes, it goes in a sidecar. If V starts emitting "MAYBE" alongside "VERIFIED", the binary discipline is broken.

2.6 Worked example: paraphrase strategy

See verifier_method='paraphrase' in arborist/qa/verify.py.

• Soundness: V=1 ⇒ token-coverage of answer against cited evidence exceeds policy threshold (default 0.6).
• Completeness gap: rejects correct answers that paraphrase using novel vocabulary.
• Position: last in the chain (after quote/span/entity). Reordering earlier introduces false positives because token-coverage is cheap to satisfy.
• Falsification: bench-fixture regression below 5pp.
• Sidecar relationship: diagnose_deflection runs alongside; never feeds into V.

2.7 New-V author checklist

• Soundness statement explicit in module docstring.
• Completeness gap acknowledged with example.
• Strategy ordering position declared with rationale.
• Falsifier set covered by tests.
• Hard verifier output remains binary (no soft signals).
• Sidecar(s) for soft signals exist if relevant.
• Bench fixtures added to capture the strategy's behavior.

3. Authoring a new policy field

Policy fields fold into governance_policy_hash (or sibling fields). New fields must answer four questions before landing.

3.1 Cache_key impact

Two options:

• Folds into governance_policy_hash. Field changes invalidate prior cache. Choose this when the field actually changes the answer's audit identity (e.g., quantifier_guard_apply_caps — applying claim caps changes which answers verify).
• Sibling field on providence record. Cache hits across field changes. Choose this when the field is operator-metadata that shouldn't reframe what counts as the same answer (e.g., retrieval_keywords per ticket #000001).

3.2 Audit-event emission

Does setting the field generate an audit event? If yes, declare the event_type and body shape. If no, document why (typically: the field is read-only / lookup-time-only).

3.3 Default value rule

Greenfield-acceptable means the default value matches prior implicit behavior. Adding a field with a default that changes answers is a bug — every existing record becomes incorrect under the new default.

Rule: default = "what the system did before this field existed."

3.4 Test coverage requirement

Two tests at minimum:

• Hash-divergence test. Different field values produce different governance_policy_hash. Confirms the field actually enters the hash.
• Default-stability test. Default value preserves prior cache. Confirms greenfield landing.

3.5 Worked example: quantifier_guard_apply_caps

See ticket #000008 §12.

• Cache_key impact: folds into governance_policy_hash. Different cap values = different cache_keys.
• Audit event: emitted as part of the run-DAG retrieval stage.
• Default: False (greenfield-acceptable; pre-#000008 behavior was no caps).
• Tests: tests/test_quantifier.py covers both hash divergence and default stability.

3.6 New-policy-field author checklist

• Cache_key impact decision documented.
• Default value matches prior implicit behavior (greenfield).
• Audit event declaration if relevant.
• Hash-divergence test.
• Default-stability test.
• Spec-methodology checklist (this section) referenced in the ticket that lands the field.

4. Cross-references

• docs/bench-maxing.md — 5pp signal-floor discipline; "old maps vs runtime maps"; n≥3 measurement.
• docs/seven-point-program.md — architectural directives every ticket walks past.
• docs/pi-star-composition.md — composition algebra (ticket #000015).
• docs/concept-relations-design.md — concept-relations storage rationale (worked example of "policy-touching but not cache-keying" decision).
• CLAUDE.md — hard rules: verifier stays binary, no soft signals in hard chain, soft hash never in hard preimage, Python-only, etc.

5. Updating this doc

When new categories emerge (e.g., a new class of verifier-related artifact, or a new authoritative table), add a section. Worked examples drift; refresh them with each major version of arborist or whenever a referenced module changes shape materially.

This doc is reference, not ticket. Edits land in normal commits with a brief message about the new category or refresh.