Doc-only landing. docs/spec-methodology.md codifies the discipline arborist already practices — versioning rule, round-trip discipline, soundness/completeness honesty, default-value greenfield rule, sidecar separation — so new π*, V, and policy-field authors don't re-derive it from audit-chain failures. Three author-class sections each ship with: - Five questions the author must answer before landing. - Worked example drawn from arborist's existing surface. - One-page checklist. Worked examples cited: - π* — wikitext-base@v1 - V — paraphrase strategy - policy field — quantifier_guard_apply_caps Cross-references to bench-maxing, seven-point-program, pi-star- composition, concept-relations-design, and CLAUDE.md.
8.1 KiB
Ticket #000019 — Specification methodology for π* and V
Status: closed · landed 2026-05-07 Opened: 2026-05-07 Closed: 2026-05-07 Scope: Doc-only methodology guide for authoring canonical projections (π*) and verifier predicates (V) such that the spec-brittleness bottleneck SQD §13.3 names doesn't surface every time a new domain or corpus lands. Outcome: a checklist + worked template every new π*/V author follows. Audience: future authors of new source adapters, verifiers, distillers; future blackops shifts onboarding. Hard constraint: methodology must not assume Merkle-AGI v8 or any unbuilt substrate. Must work today against arborist v9.8 + v7 substrate as-is.
1. Problem statement
SQD §13.3 (Master Internal Whitepaper) names the real bottleneck:
Even with perfect optimization, if π* or V encodes the wrong target, you get verified nonsense. Spec writing/testing must be first-class.
arborist already lives this. Examples:
- The
wikitext-base-v1canonicalizer evolved through several iterations; each prior iteration was committed and stale records remain. No methodology document explains why v1 won over the alternatives. - The verifier's quote/span/entity/paraphrase strategy ordering
(
arborist/qa/verify.py) is the result of bench-driven iteration with no explicit "how to author a new strategy" guide. - Trailing-citation strip (
_strip_trailing_citation) is gated on citation-cue heuristics. New authors don't know whether to extend this in place or create a sibling strategy. governance_policy_hashfolds in 7+ policy fields. Adding an 8th has no guidance.
Without a methodology:
| Problem | Consequence |
|---|---|
| Each new π* re-derives the discipline | Inconsistent versioning, accidental cache invalidation. |
| V soundness/completeness not measured | Authors ship V without knowing which axis they're on. |
| New policy fields land ad-hoc | Some fold into governance_policy_hash, some don't; rule unclear. |
| Spec versioning policy unclear | When does v2 retire v1? When does v1 stay forever? |
2. What the methodology must answer
2.1 For π* authors
- Versioning rule. When does a change require a new version number vs an in-place fix? (Default: any byte-affecting change is a new version.)
- Round-trip test. Every π* must satisfy
canonicalize(canonicalize(x)) == canonicalize(x). How is this tested? - Equivalence class declaration. What strings does this π* collapse? What does it preserve? Author must declare both explicitly.
- Policy-fold rule. When does the π*'s version land in
governance_policy_hashvscanonicalization_versionvschunking_version? - Deprecation policy. v1 stays valid until when? How are v1 records re-canonicalized to v2 (if they are)?
2.2 For V authors
- Soundness statement. "V(a)=1 implies ." Must be explicit.
- Completeness statement. What does V fail to accept that should be true under the intended semantics? Honest gap declaration.
- Strategy ordering. When V has multiple internal strategies (quote, span, entity, paraphrase), why this order? What does reordering invalidate?
- Falsification surface. What signal would falsify V? (Bench-suite regression, falsified counter-examples, etc.)
- Sidecar discipline. Soft signals never enter V's hard output. Where do they go? Pre-existing rule in CLAUDE.md; methodology codifies the test.
2.3 For policy field authors
- Cache_key impact. Does this field invalidate prior cache?
(If yes, fold into
governance_policy_hash. If no, sibling field on providence record.) - Audit-event emission. When does setting this field generate an audit event?
- Default value rule. Greenfield-acceptable means default matches prior implicit value.
- Test coverage requirement. Hash-divergence test (different field values produce different governance_policy_hash) + default-stability test (default value preserves prior cache).
3. Recommendation
A single doc docs/spec-methodology.md with:
- The 5 π questions* above with worked examples drawn from
wikitext-base-v1andclaim-lattice@v1. - The 5 V questions with worked examples from
arborist/qa/verify.py. - The 4 policy-field questions with worked examples from
quantifier_guard_apply_caps,quantifier_reminder_enabled, etc. - A new-π author checklist* (one page; printable).
- A new-V author checklist (one page; printable).
- A new-policy-field checklist (one page; printable).
- Bench-discipline cross-reference to
docs/bench-maxing.md(since methodology and benching intersect).
The methodology doc lives in docs/, not docs/tickets/. It's a
reference, not a proposal. This ticket commissions writing it.
4. Implementation sketch
4.1 Doc outline
docs/spec-methodology.md
├── 0. Why this doc exists
├── 1. Authoring a new π*
│ 1.1 Versioning rule
│ 1.2 Round-trip test
│ 1.3 Equivalence class declaration
│ 1.4 Policy-fold rule
│ 1.5 Deprecation
│ 1.6 Worked example: wikitext-base-v1
│ 1.7 Checklist
├── 2. Authoring a new V (verifier strategy)
│ 2.1 Soundness statement
│ 2.2 Completeness statement
│ 2.3 Strategy ordering
│ 2.4 Falsification surface
│ 2.5 Sidecar discipline
│ 2.6 Worked example: paraphrase strategy
│ 2.7 Checklist
├── 3. Authoring a new policy field
│ 3.1 Cache_key impact
│ 3.2 Audit-event emission
│ 3.3 Default value rule
│ 3.4 Test coverage requirement
│ 3.5 Worked example: quantifier_guard_apply_caps
│ 3.6 Checklist
├── 4. Cross-references
│ 4.1 docs/bench-maxing.md (5pp signal floor)
│ 4.2 docs/seven-point-program.md (architectural directives)
│ 4.3 CLAUDE.md (hard rules — verifier stays binary, no soft signals)
└── 5. Updating this doc itself
5.1 When new π*/V/policy categories emerge, add a section.
5.2 Worked examples drift; refresh with each major version.
4.2 Tests
This is a doc, not code. Tests are:
- Lint check: every checklist item is grep-able from the respective π*/V/policy-field implementation.
- Bench reference: every "5pp signal floor" mention links to
docs/bench-maxing.md.
4.3 Companion CI hook (optional, follow-up)
A pre-commit hook that flags new π*/V/policy fields that don't have the methodology checklist filled in. Not in this ticket; future once methodology is stable.
5. Out of scope
- Tooling to auto-generate canonicalizers. Manual authoring stays.
- Cross-language methodology (e.g., for π* implemented in Rust for ZK circuits). When ticket #000016 lands, methodology gets a Rust sub-section.
- Methodology for source adapters in general. Adapters use π*'s but also have their own concerns (rate limits, caching, etc.). Source-adapter methodology is its own potential ticket.
6. Status
Closed 2026-05-07. docs/spec-methodology.md lands with:
- Section 1 — Authoring a new π* (versioning rule, round-trip,
equivalence-class declaration, policy-fold rule, deprecation,
worked example with
wikitext-base@v1, author checklist). - Section 2 — Authoring a new V (soundness/completeness statements, strategy ordering, falsification surface, sidecar discipline, worked example with paraphrase strategy, author checklist).
- Section 3 — Authoring a new policy field (cache_key impact,
audit-event emission, default-value rule, test coverage,
worked example with
quantifier_guard_apply_caps, author checklist). - Section 4 — Cross-references to bench-maxing, seven-point program, π* composition, concept-relations design, CLAUDE.md.
- Section 5 — How to update the doc itself.
Out-of-scope items deferred:
- Tooling to auto-generate canonicalizers (manual authoring stays).
- Cross-language methodology (Rust toolchain for ZK lives in sibling repo per arborist Python-only rule; methodology there is its own doc).
- Source-adapter methodology (rate limits, caching, robots.txt).