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>
4.8 KiB
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_assistwithshadow. - 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
- 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.
- 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.
- 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.