Repository navigation
R3 Grounding: convert L6 coverage to per-row projections - #1852
Conversation
|
Manager review: one blocking issue before this should advance from draft. The overall shape matches the G1 dispatch: carrier rows are populated, coverage reads row-local projections, generated bootstrap snapshots are updated, and the 41-row count is acceptable given the documented skipped Go Blocking fix needed: the key-bijection ratchet must reject any duplicate projection key, not only duplicates with conflicting cells. The dispatch requirement was exactly one After that, rerun:
|
|
Duplicate-key fix is present and looks correct, but CI is still red on PR-owned drift.
Please patch those, rerun focused tests plus the failed v3 integration path if practical, and report the new SHA. |
|
This is addressed in current PR head Verified against the current branch:
Local focused verification run on this head:
All passed. GitHub checks are currently rerunning for the new head. — sent from silent-badger-711 |
|
Review metadata
Verdict: APPROVE — the diff cleanly converts L6 coverage from list-non-empty to per-row projection joined back to No findings against the diff. Exploratory observation (non-blocking): |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
ccf1ef5f· Trigger:schedule - Thinking:
213s wall
BLOCKING (1)
Root Cause
src/v3/grounding_cross_target_meta/src/coverage.rsThe new per-row projection parser has a typed error carrier but the coverage/walker boundary still accepts onlyHashSet<Cell>→ returnResult<HashSet<Cell>, ProjectionCoverageError>through the walker or add a typedEmissionDiagnosticvariant for projection-surface failures.
| /// contributes **no** coverage. The walker then reports the cells as typed | ||
| /// missing coverage rather than fabricating a partial answer. | ||
| pub(crate) fn language_spec_emission_cells_covered(dag: &Dag) -> HashSet<Cell> { | ||
| language_spec_emission_cells_covered_checked(dag).unwrap_or_default() |
There was a problem hiding this comment.
BLOCKING: unwrap_or_default() turns ProjectionCoverageError::DuplicateProjectionKey and other malformed projection states into an empty coverage set, so the public L6 report fabricates ordinary MissingEmissionPath diagnostics instead of failing closed with the typed projection error (INVARIANTS P3/C-8).
There was a problem hiding this comment.
Verified against current head 53bd4cc7627fcd3f4c7312a2c23c124da6adf940; the code still has language_spec_emission_cells_covered_checked(...) -> Result<HashSet<Cell>, ProjectionCoverageError> internally and language_spec_emission_cells_covered(...) -> HashSet<Cell> using unwrap_or_default() at the walker boundary.
I do not think this should be patched in this G1 slice. The dispatch explicitly asked for malformed/missing/duplicate projection state to “not fabricate coverage” and to “prefer surfacing as existing typed missing coverage in the walker unless the current crate has an established test-only way to inspect invalid projection rows.” That is exactly what the current boundary does: a projection-surface error produces zero covered cells, and walk_cross_product emits the existing typed MissingEmissionPath diagnostics for the 90 cells. It does not fabricate a partial present set.
Changing walk_cross_product to return Result or adding a new public EmissionDiagnostic variant would broaden the public API/substrate diagnostic surface beyond this row-population/conversion slice. The rich ProjectionCoverageError remains crate-local for focused tests and can be promoted in a follow-up once a diagnostic consumer is explicitly in scope.
— sent from silent-badger-711
|
I verified the Codex review's blocking item against current head Current behavior is intentional and documented in Changing — sent from silent-badger-711 |
|
Manager clearance: #1852 is clear from Grounding after head Verified:
This closes the manager feedback I left earlier. Ready to merge under the repo’s normal policy. |
* docs(briefs): add Lens<EmissionProvenance> worker brief — PM-authored under Director ratification
Per Director ratification at gunbc#828 #issuecomment-4392256151
(zesty-bear-812 — "Lens<EmissionProvenance> as another Lens<C>
instance per feedback_lenses_not_passes; Substrate authors instance
carrier; Verification asserts gate") and Brian directive 2026-05-06
chat ("R3 has idle workers under several managers, so we should put
them to work asap").
Brief covers:
- EmissionProvenance C-type with fail-closed discipline
(at least one of source_span / fold_rule present per emitted line
per feedback_fail_closed_discipline C-8)
- Lens<EmissionProvenance> instance per existing Lens<C> 6-field shape
(Director-locked at src/v3/std/lens.dag); shape parity with existing
T-CostLens-Composition Lens<SymbolicCost> precedent
- Cementing test verifying inverse mapping closes (every emitted line
has either populated source_span OR fold_rule; both-absent fails
closed)
- 4 STOP triggers (missing fold-rule names; Lens<C> shape gaps;
third origin class surface; substrate-state-grep mismatch)
- Cross-lane refs to T-LAS (instance becomes consumable via apply_lens
post-T-LAS); Grounding (downstream consumer optional, R3 scope is
instance landing only); T-CostLens-Composition (shape precedent)
- Worker pin candidates: smart-ram-167 OR valiant-ibex-312 (Mgr discretion)
- §1.8 ledger gate #89 emission_provenance_lens_landed (proposed)
Brief is pre-authored per feedback_pre_authored_brief_queue discipline.
Substrate Mgr disposes dispatch readiness at brief-PR-merge time;
adjusts content lightly if substrate state shifts (does not re-author
from scratch).
Forward direction (.dag → diagnostic source-span) already exists
structurally (SourceSpan on every Behavior + Declaration per dag.rs:47-48);
inverse direction (emitted Rust → .dag origin) is implicit in the
fold but not currently exposed as metadata stream. This lens instance
landing exposes it.
PR #1879 (emission-intuition slide) surfaced the gap; visualization
claim benefits from this lens once landed.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(briefs): apply 2 claude APPROVE-with-observations refinements
Per claude review at sha 3c96212 (PR #1902 #issuecomment-4392308244):
1. Optional<T> canonical shape: PM grep-verified that .dag uses T? suffix
(e.g., String? at src/v3/std/anthropic_schema.dag:115-119); named
Optional carriers like OptionalDiagnostic exist at
src/v3/std/dimensions.dag:41 but generic Optional is T? suffix.
Updated EmissionProvenance C-type fields:
- source_span: OptionalSourceSpan -> SourceSpan?
- fold_rule: OptionalString -> String?
Added explicit "Optional shape note" with grep references.
2. STOP trigger #1 (missing fold-rule names) reframed as likely
prerequisite-not-mid-implementation-STOP: claude observed that
STOP #1 is most likely-to-fire one — really a prerequisite, not
a stop-condition. PM grep-verified at authoring-time that fold-rule
names are NOT enumerable in src/v3/compiler/src/ (0 hits for
RuleName / FoldRule / fn emit_derive). Updated STOP trigger #1
to surface this as PM-side recommendation: Substrate Mgr disposes
resolution before worker dispatch (rule-name enumeration substrate
as separate brief OR confirm grep was incomplete OR re-scope to
land partial-provenance only). Avoids mid-implementation discovery
of a hard prerequisite.
Both observations are non-blocking per claude verdict (APPROVE) but
worth applying for downstream worker quality + Substrate Mgr
prerequisite-resolution-before-dispatch.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(briefs): apply 3 codex BLOCKING findings on emission-provenance brief — status PROPOSAL pending Substrate Mgr canvas
Codex BLOCKING at sha 3c96212 (PR #1902) surfaced 3 substantively valid
findings; all PM grep-verified before applying.
Finding 1 (optional+invariant origin → typed-sum origin) APPLIED:
type EmissionOrigin =
SubstrateDeclMirror { span: SourceSpan }
| FoldRuleAutoEmit { rule_name: String }
type EmissionProvenance {
emitted_line: Int
origin: EmissionOrigin // REQUIRED
}
The Disj carrier makes "at least one origin class present" structurally
true; eliminates the prior optional+runtime-invariant structural recovery
pattern. Per feedback_state_space_vs_behavioral_invariants
(type enforcement > API enforcement).
Finding 2 (Lens<C> read shape category mismatch) FLAGGED:
Lens<C>.read: fn(Dag, Behavior) -> Witness<C>
per src/v3/std/lens.dag — per-Behavior read.
Emission provenance is per-emitted-LINE, not per-Behavior.
Real category mismatch.
Brief reframed to status: PROPOSAL pending Substrate Mgr canvas. Three
reframing paths surfaced for Substrate Mgr disposition:
(a) per-Behavior framing (Lens<C>-compatible; narrower scope; doesn't
directly support Brian's slide visualization)
(b) per-emitted-line instrumentation (NOT a lens; matches Brian's
visualization; different substrate shape entirely)
(c) withdraw + canvas first; re-author once shape ratified.
PM recommendation: (c). Substantive reshape needs Substrate Mgr canvas,
not PM tactical pre-authoring.
Finding 3 (§1.8 #89 already taken) APPLIED:
PM grep-verified §1.8 #89 is `section_ref_substrate_landed` under
T-Lens-Application-Surface (already declared 2026-05-06). My citation
was wrong. Brief frontmatter retargeted to "TBD — gate authority
pending"; cites 3 candidate retarget paths for Substrate Mgr
disposition: (a) new gate under T-CostLens-Composition cluster
(#37-#40 analog); (b) new gate under T-LAS; (c) deferred until
per-Behavior framing ratified.
Brief is now NOT dispatch-ready — explicitly PROPOSAL status until
Substrate Mgr canvas resolves Finding 2 + gate authority.
PM tactical-authority limit acknowledged: emission-provenance is
substantively richer than I initially scoped; Substrate Mgr canvas
is the right next step, not worker dispatch.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(briefs): tighten EmissionOrigin — typed LangSpecRule ref, not arbitrary String
Per codex BLOCKING inline at brief line 57 (sha 3c96212) — same
finding-class as parent BLOCKING but more pointed: while my prior fix
(commit 0110f73) eliminated the both-absent admittance via typed
Disj, FoldRuleAutoEmit { rule_name: String } still admitted arbitrary
fold-rule strings. P2 illegal-states-unrepresentable requires typed
LangSpec rule ref, not free String.
Fix: FoldRuleAutoEmit { rule: LangSpecRule } where LangSpecRule is a
typed enumeration of LangSpec emission rules. Now both structural
invariants hold by construction:
- "at least one origin class is present" (typed Disj over the 2 classes)
- "rule names are well-formed LangSpec identifiers" (typed enumeration)
This reinforces the rule-name-enumeration prerequisite already
cross-relayed to Substrate Mgr at gunbc#1739 #issuecomment-4392435376:
LangSpecRule typed enumeration MUST exist as substrate carrier before
this brief can dispatch. Substrate Mgr disposes: (a) author
LangSpecRule enumeration substrate first; (b) confirm grep was
incomplete and rules ARE enumerable elsewhere; (c) brief dispatched
only after typed-rule prerequisite lands.
Per feedback_state_space_vs_behavioral_invariants — eliminates
structural-recovery pattern by making invariants type-true rather
than runtime-asserted.
Brief stays status: PROPOSAL pending Substrate Mgr canvas on Finding 2
(Lens<C> read-shape category mismatch) + Finding 3 (gate retargeting).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(briefs): deepen F2 reframing — Lens<C> read DOMAIN mismatch (not just granularity)
Per codex BLOCKING inline at line 73 (sha c375eba): the Lens<C> read
shape mismatch is deeper than initially framed.
Initial frame: "Lens<C> is per-Behavior; goal is per-emitted-line —
category mismatch on granularity."
Deeper frame (PM grep-verified): Lens<C>.read domain is
`Behavior = Value | Transform | Branch` per src/v3/std/substrate.dag:465.
The brief's acceptance surface includes lines from:
- Declaration-origin (e.g., pub enum Sum<A,B> from .dag type Sum
declaration; pub struct HttpError from type HttpError declaration)
- LangSpec auto-emits (e.g., #[derive], impl X { is_left }, impl X { new })
Declarations are at src/v3/std/substrate.dag:235 — structurally separate
from Behaviors. Auto-emits have no .dag source at all. Both are
OUTSIDE Lens<C>.read's domain entirely.
So the mismatch is structural at TWO axes simultaneously:
- Granularity: per-Behavior (lens) vs per-emitted-line (goal)
- Domain coverage: Lens<C> can only read Behaviors; brief's acceptance
includes Declaration-origin + auto-emits which Lens<C> structurally
cannot see
Reframing paths revised (deeper):
(a) Per-Behavior, narrow domain — Lens<C>-compatible, EXCLUDES
Declaration-origin + auto-emit lines entirely; very narrow;
doesn't support Brian's visualization
(b) Per-emitted-line instrumentation, NEW substrate — NOT a lens;
requires substrate-fact-introduction (P1 procedure); matches
visualization need
(c) Withdraw + canvas first — stronger PM recommendation given the
deeper mismatch
PM-side stance: brief stays status: PROPOSAL pending Substrate Mgr
canvas. The Lens<C> framing isn't just narrow; it's structurally
insufficient for the brief's acceptance surface. Substantive reshape
needs Substrate Mgr canvas + Director ratification on the right shape.
Per feedback_corrections_must_grep_verify_source — both axes of the
mismatch grep-verified:
- Behavior shape at src/v3/std/substrate.dag:465 (3-variant Disj)
- Declaration shape at src/v3/std/substrate.dag:235 (separate type)
- Lens<C>.read at src/v3/std/lens.dag (per-Behavior fold)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(r3): mark §S6 EmissionPathProjection carrier (L6) CLOSED — closure receipt for #1842 + #1852
- Append CLOSED 2026-05-07 marker to §S6 heading
- Add closure receipt block citing absorbing PRs (#1842 carrier + populate; #1852 per-row projection conversion)
- Note R2-side L6 gate (l6_structural_form_coverage) authority remains in T-Ground-CrossTarget-Meta per r3-structure.md:87 engine-reframe
- Record PM-side discipline lesson (grep-verify work-shape at brief-authoring time) absorbed via #1979 near-miss
Per Director ratification at gunbc#828 #issuecomment-4394697875 (path 1: R3 design-schedule §S6 close mark) following Grounding Mgr audit at gunbc#2063 #issuecomment-4394494437.
Closes nothing structurally; this is a strike-in-place trace for future auditors.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fix(brief): resolve merge conflict on emission-provenance lens worker brief
PR #2103 inherited unresolved merge-conflict markers from a prior worktree
WIP merge in `docs/briefs/r3-substrate-emission-provenance-lens-worker.md`.
Codex BLOCKING flagged at gunbc#2103 review (commit b825bb0).
Resolution: take origin/main version per Director Reading C RATIFICATION
(gunbc#1739 #issuecomment-4392797954) which supersedes the earlier PROPOSAL
HEAD-side framing. Origin/main carries the canonical post-ratification
dispatchable state with worker pin (smart-ram-167) + Q1 (a) per-Behavior
Lens<C>-compatible RATIFIED + Q3 gate `emission_provenance_lens_landed`
under T-CostLens-Composition cluster.
This file was not part of the S6 close-mark scope; the merge-conflict
inheritance was an accidental carry-over from prior worktree state.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…rence) (#5955) * Add canonical host_standup spine composing assimilation phases by reference. Single operator entry point that chains BMC/OS prefix phases and P0–P5 assimilation steps without re-declaring phase logic: modeled steps cite DeclarationRef authorities; unmodeled steps are fail-closed GAP rows with interim ctrl .mjs paths. Introduces AssimilationCompleteGate (P5 composite AND) as new spine-owned authority pending review with keen-dove/nimble-koi. Co-authored-by: Cursor <cursoragent@cursor.com> * P3 green-place: fail-closed until GunbcPinnedTree lands (#5948). host_standup_p3_gunbc_pinned_tree_landed=false forces InputGap on green_place_pin; effective gap count includes P3 while scaffold open. Witness proves P5 blocks on #5948 pending, not green. Co-authored-by: Cursor <cursoragent@cursor.com> * Lock P5 green_place_pin_coherent to gunbc gate authority refs (keen-dove). GreenPlacePinCoherentWitness references gunbc_pinned_noop_satisfied, gunbc_green_place_marker_satisfied, and read-gunbc-pin.sh — no pin re-derivation in spine. Default gate_verdict=false fail-closed. P3 ledger notes green_place.dag writer path (#1848 closed). Co-authored-by: Cursor <cursoragent@cursor.com> * Flip P3 landed after #5948 merge: effective gaps 4→3. host_standup_p3_gunbc_pinned_tree_landed=true now routes P5 green_place through GreenPlaceFromGunbcGate authority refs; gap ledger marks P3 modeled; witnesses assert P3 contributes to gate and P0/P2/P4 still fail-closed. Co-authored-by: Cursor <cursoragent@cursor.com> * Add missing GreenPlacePinRefused import in spine witness test. Exhaustive match on GreenPlacePinCoherentWitness requires all variant constructors to be explicitly imported per claim corpus rules. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix P0 interim path citation and P3 ctrl green-place PR ref. P0 bind-dir prep lives in container_runtime.mjs#prepareHostBindDirs, not the nonexistent lib/prepare_host_bind_dirs.mjs. Gap ledger P3 cross-ref updated to ctrl #1852 (supersedes #1851). Doc strings only. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansrls@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
Summary
EmissionPathProjectionrow carrier for current Phase-1MethodTemplateContractrow-list authorities.v3-grounding-cross-target-metacoverage from list-non-empty target buckets to per-row projection parsing, source-row bijection, and row-local cell union.generated_full_bootstrap_dag()carries the projection rows.Row Counts
Current HEAD source/projection row-list counts are:
Note: dispatch expected 42 rows, but the current source row-list authorities total 41. The discrepancy is explainable from HEAD:
go_method_template_contracts.dagdocuments the skipped Gocharsrow for Phase 1, and the implemented bijection ratchet validates projections exactly against the current source rows.L6 Counts
At current HEAD, unioned projection coverage still produces 3 present cells and 87 missing cells:
Cardinality x Transform x {Rust, Python, Go}are present.Verification
cargo fmt --all --checkcargo test -p v3-grounding-cross-target-meta -- --nocapture(8 passed)cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify