Repository navigation
Lens registry completeness: enroll unenrolled lenses at handler-grain (W3.3) - #6739
Conversation
…ral dot-depth check lens_registry_completeness_nested_module_prefix_roster was a hardcoded list of known submodule prefixes that missed several real nested modules under src/v2/lens (cost., idempotency., parallelism., ownership., structural_resolution., application., etc.), causing lens_registry_completeness_holds_live to false-positive as an enrollment gap. Live census confirms every real module under src/v2/lens is either depth-1 (v2.lens.<name>, a genuine top-level lens) or depth-2 (v2.lens.<parent>.<child>, always an internal file of an already-enrolled parent) — no depth-3 modules exist. Replaced the roster with a structural split-on-"." length check (>3 segments after "v2.lens." = nested submodule), a single-authority rule that needs no further hand-maintenance as new submodules are added. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
Re review 38857: agreed the per-variant — sent from still-raven-540 |
|
CI failure ( — sent from still-raven-540 |
Worker attestation
claim_batchscoped runs (below); result: PASS.Summary
Enrolls the previously-unenrolled real lenses into
LensIdV0at handler grain (mandate W3.3), so every real invariant-handler lens is nameable by a contract and gateable — prerequisite for the Question-0 self-enforcement wall.Census (step 1 — ground the roster in what EXISTS)
Live census of
src/v2/lens/**/*.dag(excluding*_test.dag):v2.lens.prefix (v2.lens.<name>) — each either a genuine distinct top-level lens, or already-known infra (registry,module_graph,affected_set,affected_set_examples,application,application_serializer,edit_locus,reference_deps,testgen).v2.lens.<parent>.<child>) — confirmed every one is an internal implementation file of an already-enrolled depth-1 parent (e.g.cost.,idempotency.,parallelism.,ownership.,structural_resolution.,application.,enforcement.,common., …).LensIdV0grew from 10 → 53 variants;lens_registry_v0/lens_registry_v0_required_idsextended to match,lens_id_v0_eqgiven self-matching arms for all 43 new variants (it is a total match).Grain (step 2 — one id per distinct invariant-handler)
Grain = one
LensIdV0per distinct verdict+remedy, not per module. Three modules were deliberately not given their own id because they consolidate onto an already-enrolled invariant (kept inlens_registry_completeness_consolidated_roster_noteinsrc/v2/lens/registry/completeness.dag):v2.lens.wiring_liveness_preflight→ sharesWiringLiveness'sgraph_invariantreachability handler (only the corpus entry point differs).v2.lens.identity_captured_navigation→ projects findings intoDependencyFidelity'sUnderClaimedEdgeverdict rather than a bespoke verdict type.v2.lens.grounding_ledger→ vocabulary/support types consumed byGrounding(GroundingVerdict,LedgerEntry), not a second checked invariant.Two modules that look like a fork candidate were kept as two distinct ids on purpose:
v2.lens.structural_similarityandv2.lens.simulated_relationshipboth call the sharedchain_generalization.chain_collapseskernel with different parameters, and each self-declaresdissolves_to: SingleAuthorityas a pending future-wave dedup — but today they are two distinct call sites with no single module to bind one id to, so both are enrolled (StructuralSimilarity,SimulatedRelationship) rather than force-merged or dropped.Enrollment (step 3)
LensIdV0variant +LensRegistryEntryV0+ append tolens_registry_v0andlens_registry_v0_required_idsfor each of the 43 newly-enrolled lenses;lens_id_v0_eqextended with matching arms (still total).Frontier (step 4 — receipt half out of scope, counted not faked)
41 of the 43 newly-enrolled lenses land as
LensContractrows with noCoverageReceiptyet (gated onfn_body_reflection_blocker— the receipt mechanism needs fn-body reflection that doesn't exist yet). These are tracked as a counted, typed, dissolve-on frontier list —lens_contracts_pending_fn_body_reflectioninsrc/v2/lens/enforcement/contract.dag(lens_contracts_pending_fn_body_reflection_count() == 41) — never a silent gap or a fabricated green receipt.gate.dag's existingfind_receipt→ReceiptAbsent→ typedLegFailsmechanism was reused as-is (generalized via this list, not forked).Completeness mechanism (this PR's fix)
src/v2/lens/registry/completeness.dagwalks the live tree (module_declaration_facts_live) and flags any realv2.lens.*module that is a genuine top-level candidate and unbound inlens_registry_v0. Its nested-submodule exclusion previously relied on a hand-maintained prefix roster that was missing several real submodule directories (cost.,idempotency.,parallelism.,ownership.,structural_resolution.,application., …), which madelens_registry_completeness_holds_livea false-positive gap. Replaced with a structural, single-authority rule: split the module name on.and treat >3 segments after thev2.lens.prefix as a nested submodule — this matches the confirmed corpus fact (depth 1 or 2 only, never 3+) and needs no further hand-maintenance as new submodules are added.RED control (step 6)
lens_registry_completeness_red_control_catches_missing_lens(fixture-based) proves the completeness mechanism catches a genuinely-missing real lens — a deliberately-unenrolled fixture module is flagged as an unenrolled candidate.Test plan
Scoped
claim_batchruns (source rootssrc/v2,dag):src/v2/lens/registry/completeness_test.dag:lens_registry_completeness_holds_live,lens_registry_completeness_red_control_catches_missing_lens,lens_registry_completeness_clean_when_fully_bound— PASS (all 3).src/v2/lens/registry/sg_claims_test.dag:lens_registry_required_ids_resolve_holds,lens_registry_singleton_row_counts_holds— PASS (both).src/v2/lens/enforcement/gate_test.dag: all 11 tests — PASS.Confirmed no sibling-lane drift:
lens_id_v0_eqis the only exhaustive match overLensIdV0in the corpus (checkedstanding_intent.dag,gate.dag,dag/gunbc/plans/self_applying_lenses.dag— none match exhaustively onLensIdV0itself).git diff --name-only origin/main...HEADconfirms only this PR's 5 files changed.Final confidence via CI (this PR), not local-only, per mandate step 6.