ticket #000031 Phase 3: warrant-chain render tail + theorem-name resolver
Two improvements that together make the warrant chain visible at
Q&A time. Phase 3 (verifier wiring) lights up the chain-of-custody
on rendered audit lines; the resolver fix makes the underlying
proofs actually point at meaningful per-axiom chunks.
Phase 3 — warrant-chain render tail
====================================
arborist/cli.py:_render_warrant_chain_tail — when a Q&A answer
cites a claim-pack record that has a `warrant-resolver-v1`
derivations row binding it to a primary-source surface chunk,
the rendered audit line gets a positive-signal tail:
STRICT · via quote · warrant: 1 proven 1/1 0.9s (cached)
Render-only — no schema change, no audit_mode change, no
governance_policy_hash change. The verifier produces the same
audit_mode + violations as before; this layer just SURFACES the
chain-of-custody when one exists. Silent in absence of data
(no chains → no tail).
Threading: shards_dir is stashed on result["_shards_dir"] in
_cmd_query before render, stripped before JSON output. Render
function signature stays (result, question) — pure function of
the result dict.
Resolver fix — theorem-name discriminating tokens
=================================================
arborist/qa/warrant_resolver.py:_build_fts_query — switched from
OR-union to AND-required on discriminating tokens. The previous
strategy had all 18 Hilbert axioms binding to the SAME chunk
because they all share "axiom" + "Hilbert"; the new strategy
extracts the discriminating token from each theorem name
("Pasch's Axiom" → "Pasch"; "Axiom of Betweenness" → "Betweenness")
and AND's them together. Each axiom now points at its own chunk.
Re-running the resolver on a clean shard:
Pasch's Axiom → chunk_idx=1 (early Group II chapter)
Axiom of Betweenness → chunk_idx=2
Axiom of Angle Cong. → chunk_idx=8 (congruence chapter)
Pythagorean Theorem → chunk_idx=26 (similitude chapter)
Sum of Angles in Tri → chunk_idx=57 (angle-related chapter)
...
11 records now resolve (down from 18) — the drop is honest:
records whose theorem name's discriminating token doesn't appear
verbatim in the cited textbook (e.g., "Vacuous Quantification"
in a propositional-logic axiom) correctly produce no match.
9 distinct chunks across the 11 records — meaningful per-axiom
binding.
A new generic-terms filter list (_GENERIC_THEOREM_TERMS) drops
"axiom"/"theorem"/"principle"/etc from the discriminating set,
so they don't pollute the AND-query.
End-to-end verification
=======================
$ arborist --shards-dir ~/.arborist/shards query \\
"What is Pasch's axiom?" --top-k 3
What is Pasch's axiom?
STRICT · via quote · warrant: 1 proven 1/1 0.9s (cached)
...
vs. a query whose cited records have no warrant chain:
$ arborist --shards-dir ~/.arborist/shards query \\
"What is Bayes theorem?" --top-k 3
What is Bayes theorem?
HYBRID · via paraphrase 9/11 5.8s (fresh)
The Bayes case stays silent because Kolmogorov isn't surface-
ingested. The Pasch case lights up because Hilbert IS, and the
warrant resolver bound this specific record to Hilbert chunk 1.
Test suite stays at 1588 passed / 28 skipped — render-only +
read-only changes outside the verifier path.
Phase 3 complete; Phase 4 (Mendelson + Enderton license decision
+ ingest) remains the natural follow-up to widen warrant
coverage from 11/92 records to a larger fraction.
This commit is contained in:
parent
f0e6baf907
commit
69e0a957ad
2 changed files with 187 additions and 13 deletions
|
|
@ -531,8 +531,19 @@ def _cmd_query(args: argparse.Namespace) -> int:
|
|||
except Exception: # pragma: no cover — best-effort journaling
|
||||
pass
|
||||
|
||||
# Ticket #000031 Phase 3 — stash shards_dir on the result dict
|
||||
# so the render-layer warrant-chain tail can look up
|
||||
# warrant-resolver derivations without needing args. Stripped
|
||||
# before JSON output to keep the json shape stable.
|
||||
_shards_dir = args.global_shards_dir or args.shards_dir
|
||||
if _shards_dir:
|
||||
result["_shards_dir"] = str(_shards_dir)
|
||||
|
||||
if args.json:
|
||||
print(json.dumps(result, indent=2, ensure_ascii=False))
|
||||
# Don't leak the internal-only `_shards_dir` field into JSON
|
||||
# output — strip it before serialize.
|
||||
json_result = {k: v for k, v in result.items() if not k.startswith("_")}
|
||||
print(json.dumps(json_result, indent=2, ensure_ascii=False))
|
||||
else:
|
||||
print(_render_query_human(result, args.question))
|
||||
return (
|
||||
|
|
@ -986,11 +997,19 @@ def _render_query_human(result: dict, question: str) -> str:
|
|||
# Schema column stays unchanged; pure display.
|
||||
display_label = _render_audit_label(audit, method, result.get("violations"))
|
||||
warrant_tail = _render_warrant_tail(result)
|
||||
# Ticket #000031 Phase 3 — when a cited source has a warrant-
|
||||
# resolver derivation row tying it to a primary-source surface
|
||||
# chunk, surface a `· warrant: N proven` tail so the user sees
|
||||
# the chain-of-custody. Pure render layer; cache_key /
|
||||
# audit_mode / governance_policy_hash all unchanged. The
|
||||
# _shards_dir is stashed on the result dict by `_cmd_query`
|
||||
# before render time (the CLI has it; the renderer doesn't).
|
||||
warrant_chain_tail = _render_warrant_chain_tail(result)
|
||||
|
||||
lines: list[str] = []
|
||||
lines.append(question)
|
||||
lines.append(
|
||||
f" {display_label}{warrant_tail} {n_verified}/{n_quotes} "
|
||||
f" {display_label}{warrant_tail}{warrant_chain_tail} {n_verified}/{n_quotes} "
|
||||
f"{elapsed} ({cache_status})"
|
||||
)
|
||||
lines.append("")
|
||||
|
|
@ -3332,6 +3351,46 @@ def _cmd_selfmodel_list(args: argparse.Namespace) -> int:
|
|||
return 0
|
||||
|
||||
|
||||
def _render_warrant_chain_tail(result: dict) -> str:
|
||||
"""Compute a render-layer tail showing how many cited sources
|
||||
have a `warrant-resolver-v1` derivations chain back to a primary-
|
||||
source surface (ticket #000031 Phase 3).
|
||||
|
||||
Returns ``""`` when no shards_dir is on the result dict, no
|
||||
chains exist, or the lookup fails — keeps the render path silent
|
||||
in absence of data.
|
||||
Returns ``" · warrant: 1 proven"`` (or higher count) when cited
|
||||
sources have Merkle-bound bindings to textbook surface chunks.
|
||||
|
||||
The actual ladder upgrade — POINTER-LINKED → ANCHOR-WARRANTED →
|
||||
EVIDENCE-WARRANTED based on warrant chains — is intentionally
|
||||
NOT done here. This is a positive-signal render addition; the
|
||||
underlying audit_mode + violations stay as the verifier
|
||||
produced them.
|
||||
|
||||
Reads ``result["_shards_dir"]`` (stashed by ``_cmd_query`` before
|
||||
render time). The render function takes only ``(result, question)``
|
||||
so the shards_dir threads through the result dict.
|
||||
"""
|
||||
shards_dir = result.get("_shards_dir")
|
||||
if not shards_dir:
|
||||
return ""
|
||||
sources = result.get("sources") or []
|
||||
if not sources:
|
||||
return ""
|
||||
try:
|
||||
from arborist.qa.warrant_resolver import warrant_chains_for_sources
|
||||
|
||||
chains = warrant_chains_for_sources(sources, shards_dir)
|
||||
except Exception:
|
||||
return ""
|
||||
if not chains:
|
||||
return ""
|
||||
n = len(chains)
|
||||
label = "warrant" if n == 1 else "warrants"
|
||||
return f" · {label}: {n} proven"
|
||||
|
||||
|
||||
def _cmd_warrant_status(args: argparse.Namespace) -> int:
|
||||
"""Read-only — show what surface chunks the citation resolver
|
||||
finds for each claim-pack record. JSON output. No DB writes.
|
||||
|
|
|
|||
|
|
@ -344,27 +344,73 @@ def _fts5_search(
|
|||
|
||||
_FTS_STOPWORDS = {"of", "the", "a", "an", "and", "or", "to", "in", "on", "is", "by"}
|
||||
|
||||
# Categorical terms that classify a record but don't discriminate
|
||||
# between records ("Axiom of X", "Theorem of Y" — both share "Axiom"
|
||||
# / "Theorem"). Drop these from the discriminating-token set so the
|
||||
# resolver can find DIFFERENT chunks per axiom in the same textbook.
|
||||
# Without this filter, "Pasch's Axiom" and "Axiom of Betweenness"
|
||||
# both rank for "axiom" and end up pointing at the same chunk.
|
||||
_GENERIC_THEOREM_TERMS = {
|
||||
"axiom", "axioms", "theorem", "theorems", "lemma", "lemmas",
|
||||
"principle", "principles", "rule", "rules", "law", "laws",
|
||||
"identity", "identities", "definition", "definitions",
|
||||
"property", "properties", "schema",
|
||||
}
|
||||
|
||||
|
||||
def _discriminating_tokens(theorem_name: str) -> list[str]:
|
||||
"""Pull the tokens from a theorem name that distinguish it from
|
||||
sibling theorems in the same textbook. Drops categorical terms
|
||||
like "Axiom" / "Theorem" / "Principle"; keeps proper-noun-ish or
|
||||
domain-specific words.
|
||||
|
||||
"Pasch's Axiom" → ["Pasch"]
|
||||
"Axiom of Betweenness" → ["Betweenness"]
|
||||
"Law of Excluded Middle" → ["Excluded", "Middle"]
|
||||
"Newton's First Law" → ["Newton", "First"]
|
||||
"""
|
||||
if not theorem_name:
|
||||
return []
|
||||
out = []
|
||||
for t in re.findall(r"[A-Za-z]{3,}", theorem_name):
|
||||
low = t.lower()
|
||||
if low in _FTS_STOPWORDS or low in _GENERIC_THEOREM_TERMS:
|
||||
continue
|
||||
out.append(t)
|
||||
return out
|
||||
|
||||
|
||||
def _build_fts_query(citation: Citation, theorem_name: str = "") -> str:
|
||||
"""Compose an FTS5 MATCH query from a citation + theorem name.
|
||||
|
||||
Strategy: union of significant tokens from the theorem name plus
|
||||
author last name. FTS5's default tokenizer indexes lowercase ASCII
|
||||
words.
|
||||
Strategy: discriminating tokens from the theorem name (proper
|
||||
nouns / domain terms, NOT categorical "Axiom"/"Theorem")
|
||||
AND'd together — FTS5 will only return chunks that contain ALL
|
||||
of them. Falls back to author + title tokens when no
|
||||
discriminating signal is available.
|
||||
|
||||
The shift from OR to AND on the discriminating tokens is the
|
||||
key fix: per-axiom queries now point at per-axiom chunks
|
||||
(Pasch's Axiom → chunk mentioning "Pasch"; Axiom of Betweenness
|
||||
→ chunk mentioning "Betweenness"), not at one shared chunk
|
||||
that mentions "axiom" everywhere.
|
||||
"""
|
||||
discriminating = _discriminating_tokens(theorem_name)
|
||||
if discriminating:
|
||||
# AND-join on discriminating tokens (FTS5 default operator
|
||||
# IS AND — but explicit for readability + safety against
|
||||
# quoting weirdness on multi-token records).
|
||||
return " AND ".join(t.lower() for t in discriminating)
|
||||
# Fall back: author last name + title tokens, OR'd.
|
||||
parts: list[str] = []
|
||||
if theorem_name:
|
||||
toks = [
|
||||
t for t in re.findall(r"[A-Za-z]{3,}", theorem_name)
|
||||
if t.lower() not in _FTS_STOPWORDS
|
||||
]
|
||||
parts.extend(toks)
|
||||
for a in citation.authors:
|
||||
last = a.split()[-1] if a else ""
|
||||
if last and len(last) >= 4 and last not in parts:
|
||||
parts.append(last)
|
||||
if not parts and citation.title:
|
||||
parts = [t for t in re.findall(r"[A-Za-z]{4,}", citation.title)][:4]
|
||||
if citation.title:
|
||||
for t in re.findall(r"[A-Za-z]{4,}", citation.title)[:4]:
|
||||
if t.lower() not in _GENERIC_THEOREM_TERMS:
|
||||
parts.append(t)
|
||||
return " OR ".join(p.lower() for p in parts) if parts else ""
|
||||
|
||||
|
||||
|
|
@ -645,6 +691,75 @@ def _has_derivation(db_path: str, record_root: str) -> bool:
|
|||
conn.close()
|
||||
|
||||
|
||||
def warrant_chains_for_sources(
|
||||
sources: list[dict],
|
||||
shards_dir: Path | str,
|
||||
) -> list[dict]:
|
||||
"""Given a list of cited source dicts (each with ``document_root``),
|
||||
return entries for those whose document_root has a warrant-resolver
|
||||
derivation row.
|
||||
|
||||
Used at Q&A render time to flip the four-rung-ladder display label
|
||||
from ANCHOR-WARRANTED toward EVIDENCE-WARRANTED when the cited
|
||||
record has a Merkle-proven binding to a primary-source surface.
|
||||
|
||||
Each returned entry: ``{record_root, surface_root, surface_title,
|
||||
surface_uri, chunk_idx, host_shard}``.
|
||||
"""
|
||||
if not sources:
|
||||
return []
|
||||
shards_dir = Path(shards_dir).expanduser()
|
||||
|
||||
# Walk every shard once to collect the warrant-resolver derivations.
|
||||
# The cost is bounded by total number of derivation rows across all
|
||||
# shards in the cluster — small relative to a Q&A render.
|
||||
chains: list[dict] = []
|
||||
for db in sorted(shards_dir.glob("*.db")):
|
||||
if db.name.startswith(("qa.", "snapshots.")):
|
||||
continue
|
||||
try:
|
||||
conn = sqlite3.connect(f"file:{db}?mode=ro", uri=True)
|
||||
except sqlite3.OperationalError:
|
||||
continue
|
||||
try:
|
||||
for row in conn.execute(
|
||||
"SELECT dr.core_root, dr.src_root, dr.proof_blob "
|
||||
"FROM derivations dr "
|
||||
"WHERE dr.process_id = ?",
|
||||
(WARRANT_PROCESS_ID,),
|
||||
):
|
||||
core, src, blob = row
|
||||
# Match this derivation to one of the answer's cited
|
||||
# source document_roots.
|
||||
for s in sources:
|
||||
if s.get("document_root") == core:
|
||||
try:
|
||||
pb = json.loads(blob)
|
||||
chunk_idx = pb.get("chunk_idx")
|
||||
except (TypeError, ValueError):
|
||||
chunk_idx = None
|
||||
chains.append({
|
||||
"record_root": core,
|
||||
"surface_root": src,
|
||||
"chunk_idx": chunk_idx,
|
||||
"host_shard": str(db),
|
||||
})
|
||||
break
|
||||
finally:
|
||||
conn.close()
|
||||
# De-duplicate by (record_root, surface_root) — same chain may
|
||||
# show up if the same record is cited multiple times.
|
||||
seen: set[tuple[str, str]] = set()
|
||||
unique: list[dict] = []
|
||||
for c in chains:
|
||||
k = (c["record_root"], c["surface_root"])
|
||||
if k in seen:
|
||||
continue
|
||||
seen.add(k)
|
||||
unique.append(c)
|
||||
return unique
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# High-level orchestration
|
||||
# ---------------------------------------------------------------------------
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue