6b5b6647bd* chore(repo): land the retrieval contract and drop root cruft Lands work that had been sitting uncommitted in the working tree: - docs/architecture/retrieval_contracts.md plus its executable form, tests/benchmarks/retrieval_contract.py and test_retrieval_contract.py, now registered in meson as retrieval_contract_unit (suite: policy). .gitignore keeps them tracked beneath the tests/benchmarks/*.py ignore. - AGENTS.md: the Development Memory section, and the product default recorded as hybrid_assist + shadow with topology-off as the control, which is what search_topology_stage already does. docs/benchmarks/index.md gains the matching search_shadow_cost plan. - .gitleaks.toml, and a Secret scan workflow that actually runs it on push and pull requests (nothing in .github invoked gitleaks before). Deletes three root files with zero references anywhere in the tree: bench_profile.json (ad-hoc profiling leftover), CppProperties.json (Visual Studio config; the repo standardises on Meson), and spdlog.pc (a hand-copied spdlog 1.12 pkg-config with prefix=/usr/local that would mislead any PKG_CONFIG_PATH lookup; spdlog comes from Conan). docs/plans/ (two p2p designs already shipped in5a53cdfaandd012d95b) was ingested into YAMS with task=desloppification source=plan, hydrated via yams cat and byte-compared before removal, per the new AGENTS.md rule; tests/scripts/analyze_simeon_adaptivity.py no longer points at a plans directory. Also reflows two stale line anchors in raw_environment_allowlist.txt for tools/yams-cli/main.cpp (shifted by11c39157) so the policy suite passes again; no new environment writes. Not included: the external/yams-repo submodule pointer in the working tree was a stale local clone two commits behind, not an intended bump. Signed-off-by: trvon <me@trevon.dev> * test(policy): make the configuration-authority ratchet bidirectional check_configuration_authority.py only reported keys and TOML readers present in code but missing from the allowlists, so the reviewed YAMS_* surface could grow but never shrink: production_environment_keys.txt even said removals "may remain grandfathered". An allowlist that only accretes stops describing the code. The policy now also fails on allowlist entries with no remaining occurrence in src/, include/, or tools/, naming the lines to delete. Key removals in later commits therefore have to update the allowlist in the same change, and the count in the success banner becomes a real measure of the environment surface (432 today). stale_entries() exposes the two stale sets for tooling; three unit tests cover stale key, stale reader, and the returned names. Signed-off-by: trvon <me@trevon.dev> * tools(policy): report where every configuration key is referenced Adds tests/scripts/report_config_key_usage.py: for each YAMS_* key in production_environment_keys.txt and each dotted TOML key literally resolved in ConfigResolver.cpp, count whole-token references per tree bucket (src, test, bench, docs, plugin; build output and the allowlists themselves excluded) and assign a verdict: KEEP when anything outside product code exercises or documents the key, CANDIDATE when only product code mentions it, NOT_IN_SRC when the allowlist is stale. The report is evidence, not a decision. From here on a key deletion must paste its CANDIDATE rows into the change description; the first audit pass hand-listed keys that turned out to have bench and test consumers, which is exactly the mistake a mechanical inventory avoids. Today: 432 env keys (215 CANDIDATE, 217 KEEP), 117 TOML keys (103 CANDIDATE, 14 KEEP). Registered as config_key_usage_report_unit. The report counts only files git tracks (git ls-files) when the root is a work tree, so an ignored local bench harness cannot turn a CANDIDATE into a KEEP on one machine and not another; outside a work tree it falls back to scanning the directory, which is what the synthetic-tree test exercises. Signed-off-by: trvon <me@trevon.dev> --------- Signed-off-by: trvon <me@trevon.dev>
78 lines
4.8 KiB
Markdown
78 lines
4.8 KiB
Markdown
# Retrieval contracts and measurement boundaries
|
|
|
|
The Lean provenance model and the bounded C++ retriever have different proof
|
|
obligations. `formal/topology/Yams/Topology/AllowedSetRetrieval.lean` models the
|
|
allowed-set operator used by fast narrowing. Its protected-document preservation
|
|
theorem explicitly requires scorer completeness after each route's quota. Neither
|
|
cover membership nor zero misses on held-out queries proves this condition for
|
|
every future query. The earlier filter-based model remains a specification of
|
|
post-filtering an existing global list.
|
|
|
|
Construction identity describes topology membership and structural inputs.
|
|
Calibration identity must additionally describe the representatives and effective
|
|
routing policy that selected the measured allowed sets. Publication timestamps
|
|
are not calibration inputs. A missing or mismatching policy identity leaves
|
|
calibration unavailable, including for legacy configs containing only a
|
|
construction fingerprint. Held-out observation counts are empirical evidence;
|
|
the identity of their dataset/split must accompany them.
|
|
|
|
Document result limits and vector-row budgets are separate quantities. Bounded
|
|
chunk retrieval can omit documents when one document contributes many high-scoring
|
|
chunks. Weighted top-k aggregation over retrieved chunks is not an exhaustive
|
|
document score. Refill can improve unique-document coverage, but bounded refill
|
|
does not establish exact ranking or completeness. Exact document-complete scoring
|
|
is the comparison oracle; it must not silently become the product latency baseline.
|
|
|
|
Simeon lexical work should be shared within one request and one selected scoring
|
|
recipe. A request-local result must not leak across queries, recipes, backend
|
|
instances, or corpus rebuilds. Benchmark the routed APIs used by the engine;
|
|
`score()`'s optional hot-query cache is a separate API and experiment.
|
|
|
|
## Benchmark controls
|
|
|
|
- Current product behavior is `hybrid_assist` with `shadow`.
|
|
- Topology disabled is the no-topology control.
|
|
- Traced shadow can run an additional exact document-complete search. Its timing
|
|
is diagnostic; compare product latency using untraced requests.
|
|
- A PHSS candidate count is a rerank pool size, not HNSW traversal work. It is
|
|
clamped to at least the raw vector-row request size. Record effective values.
|
|
- An experiment requiring narrowing must show that narrowing actually executed,
|
|
that its calibration matches the current construction and policy, and that work
|
|
counters are observed. A successful fallback is not evidence for narrowing.
|
|
|
|
The optional local xplan harness calls the tracked
|
|
`tests/benchmarks/retrieval_contract.py` preflight. Its historical
|
|
`topology_routing_budget_ablation` plan currently fails that contract: nominal
|
|
16/64 PHSS pools alias under default chunk overfetching, and its Vec0/stale
|
|
calibration setup does not validate fast certified narrowing. Do not use historical
|
|
reports from that plan to promote defaults. `search_shadow_cost` separates the
|
|
three baseline modes above. Certified narrowing plans remain parked until a
|
|
held-out calibration generator and worker artifact loader exist; an artifact
|
|
filename alone is not evidence. Replace the historical routing gate with a PQ
|
|
comparison only after verifying calibration identity and actual narrow actions
|
|
for every arm.
|
|
|
|
For promotion, use frozen binaries and immutable shared corpus state, at least
|
|
three repetitions on SciFact and NF-Corpus and a mixed index, and report quality
|
|
alongside latency, unique-document fill, route action rates, and actual work.
|
|
|
|
## Remaining foundational work
|
|
|
|
1. Define a versioned calibration artifact containing immutable construction,
|
|
routing policy, embedding-space and held-out dataset/query-split identities,
|
|
protected-document definitions, observed misses, and scorer/budget settings.
|
|
Generate observations against the document-complete oracle on a calibration
|
|
split that is disjoint from the evaluation queries. Test drift and malformed
|
|
artifacts before adding the worker loader; never synthesize successful counts.
|
|
2. Require observed narrow actions and complete work counters in each PQ arm,
|
|
then run the existing multi-corpus evaluation loop. Revalidate calibration
|
|
when scorer, aggregation, or quota policy changes. The current route identity
|
|
does not prove bounded scorer completeness.
|
|
3. Characterize a document-candidate batch seam with explicit completeness and
|
|
work status using high chunk-skew fixtures. Compare the bounded refill to
|
|
document-complete retrieval before deciding whether incremental backend
|
|
selection is worth implementing. Measure single-batch lexical requests as
|
|
well as expanded/direct-rescue requests as corpus size grows.
|
|
|
|
These are prerequisites for stronger completeness or default-promotion claims,
|
|
not properties established by the current provenance proofs or microbenchmarks.
|