docs: land ticket #000019 (spec methodology for π*, V, policy fields)
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.
This commit is contained in:
parent
40d106fb2f
commit
5cbcda41b9
3 changed files with 356 additions and 8 deletions
|
|
@ -60,7 +60,7 @@ Newest first. Update on every open/close.
|
|||
| #000022 | Adapter LossReport (PRD I9 analogue) | open · awaiting go/no-go | 2026-05-07 | — |
|
||||
| #000021 | 5S/5T/5R benchmark fixtures + harness | open · awaiting go/no-go | 2026-05-07 | — |
|
||||
| #000020 | Capital-cost ledger (8-capital queues) | closed · landed 2026-05-07 | 2026-05-07 | — |
|
||||
| #000019 | Specification methodology for π* and V | open · awaiting go/no-go | 2026-05-07 | — |
|
||||
| #000019 | Specification methodology for π* and V | closed · landed 2026-05-07 | 2026-05-07 | — |
|
||||
| #000018 | Adversarial soft-hash covert-channel analysis | open · awaiting go/no-go | 2026-05-07 | — |
|
||||
| #000017 | Memory-root: lifelong learning audit chain | closed · landed 2026-05-07 | 2026-05-07 | — |
|
||||
| #000016 | ZK Phase-2 frontier proof (concretize) | open · awaiting go/no-go | 2026-05-07 | — |
|
||||
|
|
|
|||
331
docs/spec-methodology.md
Normal file
331
docs/spec-methodology.md
Normal file
|
|
@ -0,0 +1,331 @@
|
|||
# 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 <stated semantic property> 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.
|
||||
|
|
@ -1,7 +1,8 @@
|
|||
# Ticket #000019 — Specification methodology for π* and V
|
||||
|
||||
**Status:** open · awaiting go/no-go
|
||||
**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
|
||||
|
|
@ -190,10 +191,26 @@ once methodology is stable.
|
|||
|
||||
## 6. Status
|
||||
|
||||
**Open · awaiting go/no-go.** Pure doc work. Could land
|
||||
opportunistically alongside any new π*/V landing — a "if you're
|
||||
adding one, also document why" companion.
|
||||
**Closed 2026-05-07.** `docs/spec-methodology.md` lands with:
|
||||
|
||||
Closure criterion: `docs/spec-methodology.md` lands with worked
|
||||
examples for all three author classes (π*, V, policy field) and
|
||||
checklists pinned.
|
||||
- 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).
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue