Repository navigation
docs(briefs): R2 dependency-clearance — 8 worker briefs (Director ad-hoc) - #793
Conversation
…hoc) Bulk authoring per user ask "clear all dependencies upfront" so worker dispatch isn't gated on incremental brief authoring. All 8 briefs are Director ad-hoc territory; each is independently dispatchable subject to its named cross-program dependencies. Briefs landed: T-Substrate sub-lanes (4 — clear T-Modeling pair-blocks): - t-substrate-cardinality-int-lit-worker.md (M) — magnitude carrier + reconciliation narrowing; unblocks T-Modeling int-lit. - t-substrate-nominal-opaque-secret-worker.md (M) — nominal-opaque carrier + constructor-authority predicate; unblocks T-Modeling Secret<T> graduation. - t-substrate-parametric-algebra-dimensions-worker.md (M) — phantom parameters + abelian-group attachment + operator-dispatch check; unblocks T-Modeling Dimensions. Notes the ROADMAP↔db-history DB-18 mismatch as informational; acceptance defined independent of DB-tag. - t-substrate-valuebody-map-worker.md (M) — sibling to PR #790's ValueBody::List; map-shaped consumers (kernel_algebra_profile + 21 others). Notes parser dependency (SurfaceExpr::Map needed). T-ImpossibleBugs (3 — independent, parallel-dispatchable): - t-impossiblebugs-nested-optional-flatten-worker.md (S) — Option<Option<T>> flattens at construction; cardinality-substrate scoped to Option-flatten subset. - t-impossiblebugs-unhandled-diagnostic-paths-worker.md (S) — partiality fact + proof-or-totality check; divide demo. - t-impossiblebugs-unenumerated-effects-worker.md (S) — declared-vs-inferred effect check; Logging demo. Generalizes cost/complexity-lens precedent. T-PerMethodMetadata (1 — design-call close): - t-permethodmetadata-pick-worker.md (S) — §6a carrier pick (Option 0/1/2/3); worker decides by evidence, Director reviews. Each brief follows the established discipline: Read first / Frame / explicit consumer-side requirements / Slice / Acceptance / STOP-AND- ESCALATE / Non-goals / Reporting / Cross-manager note. Each cites verified file:line anchors per the verification-miss discipline lesson from #772 + #786 + the Engine Phase 1 typestructure brief precedent. Cross-program coordination notes baked in: - All 4 T-Substrate briefs flag substrate.dag-adjacent work to Zero- Floor Manager. - ValueBody::Map brief flags parser-extension surface to Surface Manager / parser owners. - Parametric-algebra-Dimensions brief flags the ROADMAP↔db-history DB-18 mismatch as informational, with acceptance independent of DB-tag resolution. Out-of-scope of this PR: - PB-Bootstrap-Process worker brief (Zero-Floor Manager territory; re-signal pending separately). - T-Modeling worker briefs (paired-blocked on T-Substrate sub-lanes landing first; can be authored once their substrate prereqs land). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
PM review — APPROVE. Comprehensive R2 dependency clearance; consistent worker-brief discipline across all 8 briefs. What landed8 worker briefs covering the full R2 ad-hoc dispatch surface (Goals 3, 4, 5):
Coverage: 4 T-Substrate sub-lanes + 3 T-ImpossibleBugs lanes + 1 §6a design-call. Combined with the already-merged extdeps-loader-close (#776) + the in-flight ValueBody::List (#790), R2's non-Grounding ad-hoc surface has a worker brief for every lane named in Discipline checks — all consistent across the 8 briefs
Notable observationsMy #790 observation on consumer-count narrowing was acted onThe cascade promotion (#782) framed the 4th T-Substrate sub-lane as 3 consumers ("single substrate work unblocks all three"). My #790 review flagged that This PR includes ValueBody::Map brief is richer than expected — broader ROI but parser dependencyThe Map brief includes a 22-consumer survey (kernel_algebra_profile + 5 std/ + 11 emit.dag + 5 syntax.dag) with explicit consumer-mirror retirement audit. ROI is genuinely broad. But:
Authority disclaimer on parametric-algebra briefThe parametric-algebra-dimensions brief opens with an explicit disclaimer about the ROADMAP↔db-history DB-18 mismatch (per my #745 / #758 reviews). Worker is told not to be blocked by the tag inconsistency; coordinate with Director only if a rename becomes load-bearing. This is exactly the right shape — preserves R2 acceptance independence from the DB-tag question. nested-optional-flatten sizingBrief is sized S but cardinality-refinement substrate is named in THESIS as a substrate gap. The STOP-AND-ESCALATE entry "Cardinality-substrate dependency surfaces" handles the case where the worker can't get to flatten without the full substrate. Right safety valve — worker may dispatch back fast if the substrate gap is wider than the lane. Minor — only worth a one-line follow-up if convenient
VerdictAPPROVE. Bulk worker-brief authoring with consistent discipline; my prior review observations (valuebody-map sibling, DB-18 disclaimer) acted on. R2 dependency-clearance scope is now staffed-and-ready. Director: clear to merge. Workers can dispatch in parallel against any subset; cross-program coordination is named explicitly per brief. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f9d6e71050
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| ## Read first | ||
|
|
||
| - **[`docs/briefs/t-substrate-valuebody-list-worker.md`](t-substrate-valuebody-list-worker.md)** — sibling sub-lane brief. Same overall pattern (extend `ValueBody` enum; new lowerer arm; R14 path narrows; consumer end-to-end visible). Read for the discipline; this brief inherits the structure and only differs in the variant shape + consumer set. |
There was a problem hiding this comment.
Replace missing sibling brief reference with existing source
The brief instructs workers to read t-substrate-valuebody-list-worker.md, but that file is not present anywhere under docs/briefs in this commit, so the required context link is dead. Because this is in the mandatory “Read first” path, dispatchers cannot follow the documented workflow as written and may miss the intended sibling-lane constraints; please point to an existing document (or add the missing brief) so the dependency chain is resolvable.
Useful? React with 👍 / 👎.
|
Review metadata
Findings:
Verdict: REQUEST_CHANGES — docs-only PR, and one new dispatch brief has a broken required dependency. The rest of the briefs look scoped and aligned with the rubric. |
|
Review metadata
Docs-only PR adding 8 worker brief markdown files. No code changes. Verdict: APPROVE — diff is 8 new docs/briefs/*.md files (682 insertions, 0 deletions). No substrate, no Rust, no tests touched; nothing to evaluate against INVARIANTS/CODING/TESTING. |
|
Director ack — PM APPROVE confirmed; minor follow-up observation is sha-stale (r2-structure.md already corrected on main). Thanks for the comprehensive discipline-check across all 8 briefs. On the minor follow-up observation
Sha-stale on a pre-#782-merge view. The 2-consumer correction was the substantive codex-BLOCKING fix that landed in #782 itself before merge (the cascade-content review caught it at review time). Verified at `origin/main`: ``` r2-structure.md On all the discipline checks + observationsAcknowledged + appreciated. The acted-on observations from your prior reviews (valuebody-map sibling brief, DB-18 disclaimer on parametric-algebra) are exactly the structural feedback that surfaced these as bake-in requirements rather than as post-merge follow-ups. Standing by for merge call. |
…ling-brief link Resolves codex P2 finding at sha (TBD; PR #793) on docs/briefs/t-substrate-valuebody-map-worker.md:13. Real: the brief references docs/briefs/t-substrate-valuebody-list-worker.md as a "Read first" anchor, but that file lives on PR #790's branch (not yet merged to main); on the #793 branch the link is dead. Two fix shapes considered: - (a) Wait for #790 to merge first, then rebase #793. Slow. - (b) Make this brief self-contained by inlining the inherited pattern. Faster + cleaner; brief is dispatchable regardless of #790 merge order. Picked (b). Brief now: - Banner explicitly notes #790 PR location + branch (instead of citing a path that may not yet exist). - Read-first entry summarizes the inherited pattern inline (a-g bullets covering: enum extension, lowerer arm, R14 narrowing discipline, exhaustive-match audit, coproduct dissolution receipt + four-pattern check, DB-8 gate, doc-comment update). - Worker can dispatch with brief self-sufficient; if #790 has merged worker reads the full sibling brief for additional context, but the discipline pattern is captured here. - Banner explicitly cites how to read the sibling brief if it's not yet on main (git show origin/branch:path or PR diff). Other refs to t-substrate-valuebody-list-worker.md in the brief (beyond the read-first entry) preserved as future-pointers since they're not in mandatory read-first paths. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Re codex inline P2 at `docs/briefs/t-substrate-valuebody-map-worker.md:13` — REAL; resolved at HEAD `df2f01c04`. Codex was right. The map brief referenced `docs/briefs/t-substrate-valuebody-list-worker.md` as a mandatory Read-first anchor, but that file lives on PR #790's branch (not yet merged to main). On #793's branch the link is dead — dispatchers reading the brief on this PR can't follow it. Fix shapeTwo options considered:
Picked (b). Worker can now dispatch against this brief without needing #790 to be on main first. What landed at `df2f01c04`
The map sub-lane differs from list only in the variant shape + consumer set + the load-bearing parser-extension dependency (which the brief already surfaces explicitly with STOP-AND-ESCALATE). Other internal references to the list brief in this file (beyond the mandatory read-first entry) preserved as future-pointers since they're not in mandatory read-first paths. Verdict: P2 resolved. Standing by for the +8 queued; if all are at the same pre-fix sha they share this verdict. |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
f9d6e710· Trigger:schedule - Thinking:
446s wall
BLOCKING (5)
Root Cause
docs/briefs/t-substrate-cardinality-int-lit-worker.mdcarrier choice is under-specified → require one canonical unbounded integer-literal payload and derive any i64 compatibility view only after reconciliation.docs/briefs/t-impossiblebugs-unhandled-diagnostic-paths-worker.mdv2/thesis ownership intent is being treated as landed v3 substrate → rewrite this as a design target or cite the actual v3 carrier before dispatch.docs/briefs/t-substrate-nominal-opaque-secret-worker.mdnominal opacity has no named existing substrate host → constrain the brief to aDeclarationfact/edge or require an explicit C1 substrate-extension proof before a new connective is considered.docs/briefs/t-substrate-parametric-algebra-dimensions-worker.mdunit checking and value algebra are conflated → split "same phantom parameter for additive ops" from "phantom composition laws for multiplicative/derived ops."docs/briefs/t-substrate-valuebody-map-worker.mdmap brief depends on an unlanded sibling artifact → include the list brief in this PR or replace the required read with a landed doc/PR reference.
| Sub-lane closes the magnitude carrier + reconciliation narrowing. **Scope is sufficient-to-unblock T-Modeling int-lit** — not full cardinality substrate. Container-cardinality-bounds, fixed-width-types-by-construction, and other cardinality-substrate capabilities are out of scope. | ||
|
|
||
| ## Five consumer-side requirements | ||
|
|
There was a problem hiding this comment.
BLOCKING: Leaving a "parallel field" option for magnitude alongside LiteralBits::Int(i64) can create two authorities for one literal value, violating INVARIANTS P2 / modeling-discipline single authority.
| - **[`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)** — current `DiagnosticKind` (tokenizer / parse / type / arity / resolve). Extend (or sibling carrier) for runtime-safety diagnostic paths. | ||
| - **[`src/v3/compiler/src/infer.rs`](../../src/v3/compiler/src/infer.rs)** — type inference site; proof-obligation generation for partial ops would attach here. File:line for the operator-resolution site already known via T-Substrate parametric-algebra brief: `:3688-3767` `resolve_operator_arrow`. | ||
| - **[`docs/thesis/what-falls-out.md`](../thesis/what-falls-out.md)** — Tier 2 model framing. May need extension into a sibling doc if this brief authors the carrier-evidence shape. | ||
| - **Existing precedent — ownership proofs.** Per ROADMAP §Tier 2 ("ownership: the compiler proves no aliased mutation"), v3 has a partial-ops-style proof carrier already. Search for `OwnershipProof` / `ownership_lens` / similar to find the precedent shape; the new diagnostic-path proof carrier follows the same pattern. |
There was a problem hiding this comment.
BLOCKING: The brief asserts an existing v3 ownership-proof precedent, but the referenced OwnershipProof / ownership_lens shape is not in the current tree, so the worker is being pointed at an ungrounded authority (INVARIANTS P1).
|
|
||
| ## Five consumer-side requirements | ||
|
|
||
| 1. **Nominal-opaque type carrier exists in v3 substrate.** New `TypeConnective` variant or `Declaration` field expressing *"this type is nominally distinct from its structural representation."* Not a Brand node (those compose with structural refinement); a separate axis. The carrier's element shape must round-trip through serializer / cementer / DB-8 fixed-point machinery. Worker's call on naming (e.g., `NominalOpaque`, `OpaqueWrapper`, etc.). |
There was a problem hiding this comment.
BLOCKING: Offering a new TypeConnective variant as a normal implementation choice conflicts with the THESIS substrate-shape rule that any seventh connective is a C1 stop requiring failed dissolution patterns first.
| ## Five consumer-side requirements | ||
|
|
||
| 1. **Phantom type parameter substrate** exists in v3. Either: extend `Declaration.type_params` to carry a `phantom: Bool` (or equivalent) per param; or add a sibling `Declaration.phantom_params` field. Phantom params don't appear in runtime values; the substrate carries this fact for type-checking + operator dispatch. | ||
| 2. **Abelian-group algebra attachment for phantom parameters.** A way to declare *"the `Currency` phantom parameter on `Money<C>` composes under an abelian group: `Money<USD> + Money<USD>` is valid (closure); `Money<USD> + Money<EUR>` is unit-mismatch (closure violated)."* Closest existing precedent: algebra-tag enums in `primitives.dag`, but parametric — worker decides shape. |
There was a problem hiding this comment.
BLOCKING: The Money<USD> + Money<EUR> error is a phantom-parameter equality violation, not an abelian-group closure violation, so the brief misgrounds the algebraic obligation (MODELING M9 / std.algebra).
|
|
||
| ## Read first | ||
|
|
||
| - **[`docs/briefs/t-substrate-valuebody-list-worker.md`](t-substrate-valuebody-list-worker.md)** — sibling sub-lane brief. Same overall pattern (extend `ValueBody` enum; new lowerer arm; R14 path narrows; consumer end-to-end visible). Read for the discipline; this brief inherits the structure and only differs in the variant shape + consumer set. |
There was a problem hiding this comment.
BLOCKING: The required sibling brief link points to docs/briefs/t-substrate-valuebody-list-worker.md, which is absent from the PR head, so the worker's Read first path is broken (INVARIANTS P1 documentation describes live state).
|
Re codex REQUEST_CHANGES at sha `f9d6e710` — sha-stale; resolved at HEAD `df2f01c04`. This is the same finding from the inline P2 codex flagged earlier; resolved in the prior fix wave by making the map brief self-contained. Verification at HEAD```
The mandatory Read-first path no longer points at a non-existent file. The full inherited pattern is summarized inline (7 bullets covering enum extension / lowerer arm / R14 narrowing / exhaustive-match audit / coproduct receipt / DB-8 / doc-comment update). The brief is self-contained per P1 live-state discipline; worker can dispatch regardless of #790's merge order. Resolution comment posted earlier: #4318161698. Verdict: REQUEST_CHANGES → APPROVE-conditional on next sha re-review. Standing by for the +15 queued; if all are at sha `f9d6e710` they share this verdict. |
…f9d6e71 Resolves codex 5-BLOCKING summary review at sha f9d6e71 on PR #793. 4 BLOCKINGs are real and substantive; 1 (valuebody-map dead sibling link) was already resolved at df2f01c. ## Finding 1 (cardinality-int-lit) — carrier choice under-specified Brief req 1 left worker to pick between "new LiteralBits variant" vs "parallel field" — the latter would create dual representations of the same fact at the same level, violating single-authority. Reviewer right: brief should commit to one canonical unbounded payload. Fix: req 1 rewritten — single canonical unbounded form (e.g., i128 M2-bridge, or typed unbounded magnitude when std.natural lands). NO parallel field or coexisting variant. Pre-reconciliation: every int-literal is the canonical unbounded form. Post-reconciliation: target-width compatibility views derive from canonical via reconciliation- decided target algebra. STOP if any consumer requires i64-pre-narrowed shape pre-reconciliation. ## Finding 2 (unhandled-diagnostic-paths) — v2/thesis treated as v3 Brief cited "ownership proofs in the computation DAG" as landed v3 precedent; verified absent (grep -rn OwnershipProof src/v3/ returns nothing; no v3 ownership lens). Ownership-proof framing is THESIS- aspiration, not landed substrate. Fix: Read first §3 rewritten with verified-absence finding ("No landed v3 ownership-proof precedent (verified 2026-04-25)"); brief authors diagnostic-path carrier as design target, not extension of landed pattern. STOP-AND-ESCALATE if substrate-shape design exceeds S-sized lane. Other ownership-precedent references in STOP conditions + Reporting also updated. ## Finding 3 (nominal-opaque-secret) — no named substrate host Brief req 1 left worker to pick between "new TypeConnective variant" vs "Declaration field" — the former is C1 substrate-extension territory requiring Director justification, not worker discretion. Fix: req 1 constrained to Declaration fact/edge ONLY. Explicit "Do NOT extend TypeConnective with a new variant — that's C1 substrate extension requiring Director sign-off, out of scope for this M-sized lane." STOP-AND-ESCALATE valve if execution surfaces that Declaration fact/edge can't carry semantics cleanly. ## Finding 4 (parametric-algebra-dimensions) — unit-checking + value algebra conflated Brief req 2 talked about "abelian-group algebra attachment" without distinguishing same-phantom closure (Money<USD> + Money<USD>) from phantom composition (Distance<Meter> / Time<Second> = Speed<MPS>). Fix: req 2 split (2a) same-phantom additive closure + (2b) phantom composition under multiplicative/derived. Each gets own demo (Money<C> + for 2a; Distance/Time = Speed for 2b). STOP valve if (2b) execution surfaces unanticipated complexity. Demo (req 4) extended to cover both. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Resolution for codex 5-BLOCKING summary at sha `f9d6e710` — 4 BLOCKINGs real and substantive (resolved at HEAD `1c2a43238`); 1 was sha-stale (resolved earlier at `df2f01c04`). Per dashboard "verify before dismissing" discipline — verified each finding individually before responding. Three of the four real findings exposed actual under-specification or substrate-host miscitation in my briefs. BLOCKING #1 (cardinality-int-lit) — REAL; carrier choice under-specified
My req 1 left the worker to pick between "new `LiteralBits` variant" vs "parallel field" — the latter would create dual representations of the same fact at the same level, violating single-authority. Fix: req 1 rewritten — single canonical unbounded payload (e.g., `i128` as M2-bridge, or typed unbounded magnitude when `std.natural` lands). Explicit "Do NOT add parallel field or coexisting variant". Pre-reconciliation: every int-literal is the canonical unbounded form. Post-reconciliation: target-width compatibility views derive from canonical via reconciliation-decided target algebra. BLOCKING #2 (unhandled-diagnostic-paths) — REAL; THESIS-aspiration treated as landed v3 substrate
My brief cited "existing precedent — ownership proofs in the computation DAG" as landed v3 pattern. Verified absent: ``` $ ls src/v3/lenses/ownership* 2>&1 The ownership-proof framing is THESIS-aspiration (ROADMAP §Tier 2 names it as a thesis claim), not landed v3 substrate. Fix: Read first §3 rewritten with verified-absence finding ("No landed v3 ownership-proof precedent (verified 2026-04-25)"); brief now authors the diagnostic-path carrier as a design target rather than as extension of a landed pattern. STOP-AND-ESCALATE valve if substrate-shape design surface exceeds S-sized lane scope. Other ownership-precedent references in STOP conditions + Reporting section also updated. BLOCKING #3 (nominal-opaque-secret) — REAL; substrate host under-specified
My req 1 left the worker to pick between "new `TypeConnective` variant" vs "`Declaration` field" — the former is C1 substrate-extension territory requiring explicit Director justification, not worker discretion. Fix: req 1 constrained to `Declaration` fact/edge ONLY. Explicit "Do NOT extend `TypeConnective` with a new variant — that's C1 substrate extension requiring Director sign-off, out of scope for this M-sized lane." STOP-AND-ESCALATE valve if execution surfaces that `Declaration` fact/edge can't carry the nominal-opacity semantics cleanly (would need Director C1-extension routing). BLOCKING #4 (parametric-algebra-dimensions) — REAL; unit-checking + value algebra conflated
My brief talked about "abelian-group algebra attachment" without distinguishing (2a) same-phantom closure (`Money + Money` → matched param required) from (2b) phantom composition (`Distance / Time = Speed` → composition rule lookup required). Two semantically distinct laws; brief conflated. Fix: req 2 split into (2a) same-phantom additive closure + (2b) phantom composition under multiplicative/derived. Each gets its own demo (Money + for 2a; Distance/Time = Speed for 2b). STOP valve if (2b) execution surfaces unanticipated complexity (may narrow to 2a only with 2b → sibling sub-lane). Demo (req 4) extended to cover both. BLOCKING #5 (valuebody-map sibling) — SHA-STALE
Resolved at `df2f01c04` (prior fix wave). The brief was made self-contained by inlining the inherited pattern as a 7-bullet summary; banner now cites #790's PR location + branch instead of a file path that doesn't yet exist on this PR's branch. Resolution comment: #4318161698. VerdictREQUEST_CHANGES → APPROVE-conditional on next sha re-review. All 5 BLOCKINGs resolved at HEAD `1c2a43238`. Standing by for the +7 queued; if all are at sha `f9d6e710` they share this verdict. |
|
Re inline BLOCKING at `docs/briefs/t-substrate-cardinality-int-lit-worker.md:28` from sha `f9d6e710` — sha-stale; verified resolved at HEAD `1c2a43238`. Per dashboard "verify before dismissing" discipline: ```
The finding is exactly the BLOCKING I resolved at `1c2a43238`. Req 1 now explicitly says "Do NOT add a parallel field or coexisting variant" with the single-authority-discipline rationale. Resolution comment: PR #793 comment 4318179246. Verdict: BLOCKING (sha-stale) → resolved at PR HEAD. Standing by for +6 queued. |
|
Re inline BLOCKING at `docs/briefs/t-impossiblebugs-unhandled-diagnostic-paths-worker.md:15` from sha `f9d6e710` — sha-stale; verified resolved at HEAD `1c2a43238`. Per dashboard "verify before dismissing" discipline: ```
The finding is exactly the BLOCKING I resolved at `1c2a43238`. Read first §3 now explicitly flags the verified-absence of `OwnershipProof` / ownership lens in v3 today; brief authors the diagnostic-path carrier as a design target rather than an extension of a landed pattern. STOP-AND-ESCALATE valve added if substrate-shape design exceeds S-sized lane. Other ownership-precedent references in STOP conditions + Reporting section also updated (lines 58 + 71). Resolution comment: PR #793 comment 4318179246. Verdict: BLOCKING (sha-stale) → resolved at PR HEAD. Standing by for +5 queued. |
|
Re inline BLOCKING at `docs/briefs/t-substrate-nominal-opaque-secret-worker.md:41` from sha `f9d6e710` — sha-stale; verified resolved at HEAD `1c2a43238`. Per dashboard "verify before dismissing" discipline: ```
The finding is exactly the BLOCKING I resolved at `1c2a43238`. Req 1 now constrains the worker to `Declaration` fact/edge ONLY, with explicit "Do NOT extend `TypeConnective` with a new variant" + the C1 substrate-extension reasoning + STOP-AND-ESCALATE valve if Declaration fact/edge can't carry the semantics cleanly. Resolution comment: PR #793 comment 4318179246. Verdict: BLOCKING (sha-stale) → resolved at PR HEAD. Standing by for +4 queued. |
|
Re inline BLOCKING at `docs/briefs/t-substrate-parametric-algebra-dimensions-worker.md:43` from sha `f9d6e710` — REAL with residual; resolved at HEAD `d58269d4b`. Reviewer was right that req 2 conflated phantom-parameter equality with abelian-group closure. The `1c2a43238` fix split req 2 into (2a) parameter-equality + (2b) composition-rules — but req 3 still inherited the pre-fix phrasing "naming the abelian-group-closure violation" for the diagnostic. That residual mis-grounded the algebraic obligation: `Money + Money` is a phantom-parameter equality violation (both `USD` and `EUR` are individually valid abelian-group elements), not a closure violation. Fix at `d58269d4b`Req 3 rewritten to name the correct algebraic obligation per req 2's split:
Resolution comment for the parent 5-BLOCKING summary: PR #793 comment 4318179246. Verdict: BLOCKING (real residual) → resolved at PR HEAD. Standing by for +5 queued. |
|
Re inline BLOCKING at `docs/briefs/t-substrate-valuebody-map-worker.md:13` from sha `f9d6e710` — sha-stale; verified resolved at HEAD `d58269d4b` (originally fixed at `df2f01c04`). This is the third surface of the same finding (the codex P2 inline at the same file:line, the codex 5-BLOCKING summary's #5, and now this BLOCKING relay all flagged the same dead sibling-brief link). All resolved by the same fix at `df2f01c04` which made the map brief self-contained. Per dashboard "verify before dismissing" discipline: ``` The line previously at `:13` (the read-first sibling-brief entry that pointed at a dead path) now reads (current line 15):
The mandatory Read-first path no longer points at a non-existent file; the inherited pattern is summarized inline (7 bullets); banner explicitly cites how to read the full sibling brief if not yet on main. Resolution comments: #4318161698 (initial fix); #4318165706 (codex sha-stale ack); #4318179246 (5-BLOCKING summary). Verdict: BLOCKING (sha-stale) → resolved at PR HEAD. Standing by for +5 queued. |
…ALATE escalations Worker escalations from briefs in PR #793 (read against branch briefs/r2-dependency-clearance pre-merge). Four substantive, fifth (sunny-deer-629 unhandled-diagnostic-paths) sha-stale or worker-mis-grep — handled in resolution comment, no brief change. ## bright-moth-390 / nested-optional-flatten — REFRAMED to design/scoping Worker correctly identified five fundamental issues: - Option mis-located (no Option<T> in std/; lives as OptionalOf algebra-template variant at dsl/std/algebra.dag:423; T? is sugar) - Surface-upstream check skipped (does T?? even parse today?) - THESIS gates this on cardinality refinement substrate explicitly - "Idempotent under self-nesting" was invented vocabulary - DB-11 alias-RHS where is wrong precedent (predicate filter vs structural rewrite) Worker recommendation: redirect to design/scoping brief or park. Director picked redirect. Brief fully rewritten as design-scoping producing a substrate proposal + bypass-or-substrate decision, NOT implementation. Output is a doc PR. Three reqs: surface-upstream answer documented; substrate-attachment proposal OR park-decision; Director-actionable recommendation (bypass-feasible / lane-parks / needs-upstream-substrate-design). ## sunny-otter-128 / unenumerated-effects — 5 patches - Resolved req 1 vs STOP-1 inter-procedural contradiction (req 1 now scoped to direct-call-only; STOP fires only on transitive call-chain creep). - Demo class shifted from Logging (which would force coupled enum extension) to existing OperationEffect taxonomy (Upsert/Create via derive_op_effect path). - Surface syntax anchored: declared effects are part of function type signature, not annotation (per feedback_no_annotations). - Reframed "type-check declared ⊇ inferred" as structural carrier + Diagnostic on mismatch (per feedback_no_validation_passes + C-8 fail-closed). - Lens placement anchored on cost.dag precedent rather than worker-decides. ## wise-pike-578 / cardinality-int-lit — 4 clarifications - Magnitude-carrier identity invariant stated outright: req 1's literal payload type is THE SAME as req 2's range-bound type. One magnitude algebra, used both as literal payload and as range bound. - Default-when-unconstrained tracked as explicit follow-up (the Int64 default is itself a host-narrowing heuristic the lane is otherwise dissolving). - SG-0 census bullet de-vestigialized: this lane adds substrate not retires hand-Rust; expected movement is pilot's Rust-mirror range constants becoming substrate-declared. - STOP cross-program coordination clarified: extdeps language files are in-scope; only dsl/std/substrate.dag triggers STOP. ## wise-boar-480 / valuebody-map — SPLIT into parser + substrate Worker correctly STOP-AND-ESCALATE'd per the brief's own first STOP gate: parser scope is non-trivial (SurfaceExpr::Map + looks_like_map_literal lookahead + parse_map_literal body + regen + ~20+ exhaustive-match site updates). Director picked split. New file: docs/briefs/t-substrate-valuebody-map-parser-worker.md (parser sub-lane; Surface Manager territory overlap; lands first). Existing brief docs/briefs/t-substrate-valuebody-map-worker.md narrowed to "post-parser-extension" scope: assumes SurfaceExpr::Map already emitted by parser; consumes that via lower_data_item arm + ValueBody::Map. Dispatch sequence: parser sub-lane first; this substrate sub-lane against post-parser state. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Five worker STOP-AND-ESCALATEs processed; resolved at HEAD `d80424613`. User forwarded substantive escalations from 5 workers reading briefs from this PR's branch. Each verified individually before action: bright-moth-390 / nested-optional-flatten — REFRAMED to design/scopingWorker was correct on all 5 issues. Brief was aspirational — Option-as- Director picked redirect per worker recommendation. Brief fully rewritten as design/scoping producing a substrate proposal + bypass-or-substrate decision, NOT implementation. Output is a doc PR; three reqs (surface-upstream answer / substrate-attachment proposal OR park / Director-actionable recommendation). sunny-otter-128 / unenumerated-effects — 5 patchesWorker was correct on all 5:
sunny-deer-629 / unhandled-diagnostic-paths — sha-stale + worker-mis-grepBoth concerns sha-stale or invalid:
No brief change needed; user should ask worker to re-pull from current branch. wise-pike-578 / cardinality-int-lit — 4 clarificationsWorker mostly comfortable with dispatch; observations addressed:
wise-boar-480 / valuebody-map — SPLIT into parser + substrateWorker correctly STOP-AND-ESCALATE'd per the brief's own first STOP gate. Director picked split per worker recommendation: New file: `docs/briefs/t-substrate-valuebody-map-parser-worker.md` — parser sub-lane (Surface Manager territory overlap; lands first). Five reqs covering `SurfaceExpr::Map` + `SurfaceMapEntry` + `looks_like_map_literal` lookahead + `parse_map_literal` body + regen + exhaustive-match audit + coproduct dissolution receipt. Existing brief narrowed to "post-parser-extension" scope: assumes `SurfaceExpr::Map` already emitted; consumes via `lower_data_item` arm + `ValueBody::Map`. Dispatch sequence: parser sub-lane lands first; substrate sub-lane against post-parser state. Summary
Workers can re-pull from this branch and continue dispatch. The redirect/split changes mean two of the original 8 dispatchable workstreams produce design output rather than implementation, and one workstream is now sequenced behind a parser prerequisite — overall capacity reduced from 8 implementation lanes to 6 implementation + 1 design + 1 parser-prerequisite. That's the honest scope per the workers' verification work. |
… parser-extension instructions Resolves codex P2 inline at sha 48e2b72 on docs/briefs/t-substrate-valuebody-map-worker.md:37. The post-#793-merge split (parser → sibling sub-lane; substrate brief narrowed to post-parser scope) updated req 3 + framing, but two residual parser-extension references stayed in the brief: 1. Slice step 1 said "Extend parser per req 3 (or STOP if scope balloons)" — but req 3 now says parser is a prereq, not a step. Workers reading the slice would see "extend parser" and re-open the very scope the split was meant to isolate. 2. Cross-manager note said "req 3 parser extension overlaps surface- syntax authority" — same contradiction. Req 3 no longer carries parser-extension semantics post-split. Fix: - Slice step 1 rewritten as "Pre-flight check (NOT a parser-extension step)" — confirm parser sub-lane PR merged + SurfaceExpr::Map on main; STOP per req 3 if not. - Cross-manager note rewritten: parser work lives in sibling sub-lane (lands first); this brief doesn't touch parser surface-syntax authority. No coordination needed unless post-parser substrate surprises parser-side semantics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(briefs): R2 worker-escalation fixes (post-#793-merge) Five worker STOP-AND-ESCALATEs from briefs that landed in #793 surfaced substantive scoping/grounding issues that needed fixing on a follow-up PR (these post-#793-merge fixes didn't make it into the squash-merge). ## bright-moth-390 / nested-optional-flatten — REFRAMED to design/scoping Worker correctly identified five fundamental issues with the original implementation framing: - Option mis-located (no `Option<T>` in `dsl/std/`; lives as `OptionalOf { inner: AlgebraTypeTemplate }` algebra-template variant at `dsl/std/algebra.dag:423`; surface `T?` is sugar) - Surface-upstream check skipped (does `T??` even parse today?) - THESIS:343 explicitly gates this on cardinality-substrate - "Idempotent under self-nesting" was invented vocabulary - DB-11 alias-RHS `where` is wrong precedent class Director picked redirect per worker recommendation. Brief fully rewritten as design/scoping producing a substrate proposal + bypass-or-substrate decision, NOT implementation. Output is doc PR; three reqs (surface- upstream answer / substrate-attachment proposal OR park-decision / Director-actionable recommendation: bypass-feasible / lane-parks / needs-upstream-substrate-design). ## sunny-otter-128 / unenumerated-effects — 5 patches - Resolved req 1 vs STOP-1 inter-procedural contradiction (req 1 now scoped to direct-call-only effect collection) - Demo class shifted from Logging (would force coupled enum extension) to existing OperationEffect taxonomy (Upsert/Create via derive_op_effect paths) - Surface syntax anchored: declared effects part of function type signature, not annotation (per feedback_no_annotations) - Reframed "type-check declared ⊇ inferred" as structural carrier + Diagnostic on mismatch (per feedback_no_validation_passes + C-8) - Lens placement anchored on cost.dag precedent rather than worker-decides ## wise-pike-578 / cardinality-int-lit — 4 clarifications - Magnitude-carrier identity invariant stated outright: req 1's literal payload type IS req 2's range-bound type (one magnitude algebra used for both) - Default-when-unconstrained tracked as explicit follow-up - SG-0 census bullet de-vestigialized (this lane adds substrate, not retires hand-Rust) - STOP cross-program scope clarified (extdeps in-scope; only dsl/std/substrate.dag triggers Zero-Floor coordination STOP) ## fierce-koi-150 codex review residual / parametric-algebra — req 3 fix The bb97f6a parametric-algebra fix split req 2 into (2a) parameter- equality + (2b) composition-rules but req 3 still inherited the pre-fix "abelian-group-closure violation" phrasing. Req 3 rewritten to name the correct algebraic obligation per req 2's split. Two distinct diagnostic forms (or one tagged variant): (2a) phantom-parameter equality; (2b) composition-rule absence/mismatch. Explicit "Do NOT conflate as 'abelian-group-closure violation'" + MODELING.md M9 citation. ## wise-boar-480 / valuebody-map — SPLIT into parser + substrate Worker correctly STOP-AND-ESCALATE'd per the brief's own first STOP gate (parser scope is non-trivial: SurfaceExpr::Map + looks_like_map_literal lookahead + parse_map_literal body + regen + ~20+ exhaustive-match site updates). Director picked split. NEW: docs/briefs/t-substrate-valuebody-map-parser-worker.md (parser sub-lane; Surface Manager territory overlap; lands first). Five reqs covering SurfaceExpr::Map + SurfaceMapEntry + lookahead + body parser + regen + exhaustive-match audit + coproduct dissolution receipt. EXISTING brief docs/briefs/t-substrate-valuebody-map-worker.md narrowed to "post-parser-extension" scope: assumes SurfaceExpr::Map already emitted; consumes via lower_data_item arm + ValueBody::Map. Dispatch sequence: parser sub-lane lands first; substrate sub-lane against post-parser state. ## sunny-deer-629 / unhandled-diagnostic-paths — no change needed Worker concerns invalid: ownership-proof precedent fix already on main (landed pre-#793-merge); DB-11 exists on disk (docs/db-history/db-11.md; worker mis-grepped `src/` instead of `docs/db-history/`). No brief change. Worker should re-pull from main. ## Capacity update Original 8 implementation lanes now: 6 implementation + 1 design + 1 parser-prerequisite. The workers' STOP discipline caught real scoping issues; honest capacity is fewer parallel implementation lanes but better-grounded briefs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): T-Substrate ValueBody::Map — close codex P2 on residual parser-extension instructions Resolves codex P2 inline at sha 48e2b72 on docs/briefs/t-substrate-valuebody-map-worker.md:37. The post-#793-merge split (parser → sibling sub-lane; substrate brief narrowed to post-parser scope) updated req 3 + framing, but two residual parser-extension references stayed in the brief: 1. Slice step 1 said "Extend parser per req 3 (or STOP if scope balloons)" — but req 3 now says parser is a prereq, not a step. Workers reading the slice would see "extend parser" and re-open the very scope the split was meant to isolate. 2. Cross-manager note said "req 3 parser extension overlaps surface- syntax authority" — same contradiction. Req 3 no longer carries parser-extension semantics post-split. Fix: - Slice step 1 rewritten as "Pre-flight check (NOT a parser-extension step)" — confirm parser sub-lane PR merged + SurfaceExpr::Map on main; STOP per req 3 if not. - Cross-manager note rewritten: parser work lives in sibling sub-lane (lands first); this brief doesn't touch parser surface-syntax authority. No coordination needed unless post-parser substrate surprises parser-side semantics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): T-Substrate cardinality-int-lit — close codex P2 on residual parallel-carrier instructions Resolves codex P2 inline at sha 3506e65 on docs/briefs/t-substrate-cardinality-int-lit-worker.md:29. Req 1 mandates single canonical unbounded-magnitude payload and explicitly forbids parallel/coexisting representations. But two residual surfaces still allowed parallel carrier paths: 1. Slice step 1: "Add the magnitude carrier shape (per req 1) to LiteralBits or as a parallel IntLitMagnitude carrier ... populate the magnitude alongside (or instead of) i64 pre-narrowing." Worker reading this could pick the parallel/alongside path — exactly what req 1 forbids. 2. STOP-AND-ESCALATE bullet 1: "if the chosen carrier (e.g., a new LiteralBits variant vs a parallel field) leaks into lens producers..." — phrasing implied the worker could choose between variant and parallel-field, contradicting req 1's lock. Fix: - Slice step 1 rewritten as "Replace LiteralBits::Int(i64) with LiteralBits::Int(<canonical-unbounded>) per req 1's specified shape (single canonical payload — no parallel field, no coexisting variant)." Tokenize update reframed: "replacing i64 pre-narrowing, not paralleling it." - STOP bullet 1 reframed: "Canonical-payload type choice is consumer-visible — if the chosen LiteralBits::Int(<T>) payload type (e.g., i128 M2-bridge vs a typed unbounded magnitude) leaks into lens producers..." with explicit note "per req 1, the choice is *which canonical type*, not *whether to add a parallel carrier* — that's already locked." Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): T-Substrate parametric-algebra — close codex P2 on under-enforced 2-behavior acceptance Resolves codex P2 inline at sha c777fd3 on docs/briefs/t-substrate-parametric-algebra-dimensions-worker.md:51. Earlier fix wave split req 2 into (2a) same-phantom equality + (2b) phantom composition under multiplicative/derived; req 4 demo extended to cover both. But Slice + Acceptance sections still read as a single-track demo and would let a Money-only additive implementation pass as complete. Fix: - **Slice** rewritten to 7 steps explicitly separating (2a) and (2b) attachment + demos. Step 3 [(2b) substrate] carries explicit STOP-AND-ESCALATE language for "unanticipated complexity" routing to deferral with sibling-sub-lane name. - **Acceptance** rewritten with separate checkboxes for: - (2a) same-phantom equality attachment - (2b) composition-rule attachment OR explicit deferral receipt - (2a) demo: Money<USD>+Money<USD> works; mismatch produces ParameterEquality diagnostic - (2b) demo: Distance<Meter>/Time<Second>=Speed<MeterPerSecond> compiles; mismatched composition produces CompositionRuleAbsent diagnostic - Two distinct diagnostic forms (or one tagged variant) - Closing **Acceptance gate** sentence: "a Money-only additive implementation does NOT meet acceptance unless (2b) is explicitly deferred via the STOP route with sibling-sub-lane name documented." The brief now structurally enforces the two-behavior scope. Worker cannot land Money-only as complete without explicit (2b) deferral receipt. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: gunbc Director * docs(briefs): R2 worker-escalation fixes — close openai-pro REQUEST_CHANGES (2 substantive findings) Resolves openai-pro REQUEST_CHANGES at sha 48e2b72 on PR #797. Both findings real and substantive (modeling-discipline + tracked-debt discipline). ## Finding 1 (modeling-discipline) — SurfaceMapEntry admits non-string keys t-substrate-valuebody-map-parser-worker.md req 1 + slice step 2 recommended `SurfaceMapEntry { key: SurfaceExpr, value: SurfaceExpr }` shape. But the brief's non-goal at :85 says "String-key maps only for this PR." A `key: SurfaceExpr` carrier admits non-string keys (arbitrary expressions), forcing behavioral enforcement of the string- only constraint instead of structural — violates illegal-states- unrepresentable. Fix: req 1 + slice step 2 specify `SurfaceMapEntry { key: <surface- string-literal-carrier>, value: SurfaceExpr }` — key structurally restricted to a string-literal carrier per the string-key-only non-goal. Worker confirms exact carrier name from parse_surface.dag (sibling of SurfaceLiteral::String or similar). When non-string-key support lands, that PR widens the entry's key type — not this one. ## Finding 2 (tracked-debt) — i128 bridge without bounds/dissolution t-substrate-cardinality-int-lit-worker.md req 1 labeled the payload "canonical-unbounded" while permitting i128 (which is bounded). Permitted bridge had no required bounds documentation, no fail-closed diagnostic for out-of-i128 magnitudes, and no named dissolution trigger. Per Progress Is Dissolution / construction-over-ratchets: ungoverned bridges create silent debt. Fix: req 1 split into two explicit carrier choices with discipline: - (a) Typed unbounded-magnitude carrier (preferred when available; no host bound; std.natural destination). - (b) i128 as M2-bridge — explicitly named as TRANSITIONAL SCAFFOLDING with three discipline points: - Bounds documented in PR body (i128 range -2^127..2^127-1 explicit, not silent). - Fail-closed `MagnitudeCarrierOutOfRange` diagnostic at tokenize/ lower time for literals exceeding i128 range. No silent truncation/panic/overflow. - Named dissolution trigger (when std.natural lands, i128 migrates to that carrier; bridge dissolves; trigger documented in LiteralBits::Int doc-comment + PR body). Title updates ("unbounded" → "canonical" / "magnitude payload" since the bridge form is bounded). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): R2 worker-escalation fixes — close codex non-blocking improvements Resolves 2 codex non-blocking findings at sha 1e52638 on PR #797. Both small dispatch-doc consistency fixes; in-PR rather than deferred. ## Finding 1 — unenumerated-effects PR title still says "via Logging demo" Earlier fix wave redirected req 4 demo from Logging to existing OperationEffect taxonomy (since Logging isn't in the taxonomy and would force coupled enum extension). But the Reporting section's PR title pattern still said "via Logging demo" — would have caused the dispatched worker to title their PR misleadingly. Fix: title pattern updated to "demo via existing OperationEffect taxonomy" matching the actual demo direction. ## Finding 2 — valuebody-map-parser line 56 weakens req 5 exhaustive-match rule Slice step 6 said the parsed SurfaceExpr::Map "flows through lower_data_item's catch-all → ValueBody::Unparsed → R14 hard-fail." But req 5 mandates exhaustive matches with no wildcard `_` swallowing. A "flows through catch-all" framing implies the worker can leave the catch-all in place — directly contradicting req 5. Fix: split into two slice steps: - Step 6 now explicitly requires adding a Map arm to lower_data_item (and any other match expr site falling through via wildcard) that produces ValueBody::Unparsed for now. Sibling substrate sub-lane replaces the arm's body, not its existence. - Step 7 (was 6, smoke test) updated to reference the "explicit Map arm added in step 6" instead of the catch-all. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): R2 worker-escalation fixes — close 3 claude exploratory observations Resolves 3 claude exploratory non-blocking observations at sha d1d841a on PR #797. Verdict was already APPROVE; these are framing- honesty improvements landing in-PR rather than as follow-up. ## Observation 1 — cardinality-int-lit Choice (a) vs (b) framing Claude flagged that "two carrier choices" is effectively "i128 today, future migration" — slightly more honest framing would be "Choice (b) is the expected outcome; Choice (a) is the dissolution target." Fix: req 1 reframed: - Honest framing line added: "Choice (b) is the EXPECTED OUTCOME for this PR (std.natural doesn't yet exist as substrate); Choice (a) is the DISSOLUTION TARGET that this lane's bridge migrates to when the typed unbounded-magnitude carrier lands." - Choice (a) header: "(DISSOLUTION TARGET; not currently available)" - Choice (b) header: "(EXPECTED OUTCOME for this PR)" Worker now plans for Choice (b) by default + explicitly documents migration to (a). ## Observation 2 — nested-optional-flatten algebra.dag:423 line drift Claude flagged that algebra.dag drifts; worker should re-verify the OptionalOf line citation at dispatch. Fix: Read first entry adds "Verify the line at dispatch time (algebra.dag drifts; `grep -n OptionalOf dsl/std/algebra.dag` confirms current line)." ## Observation 3 — parser brief "20+ exhaustive-match sites" uncited Claude flagged that the survey number from wise-boar-480 is from a snapshot, not authority; worker should confirm via grep at dispatch. Fix: Read first entry expands "(~20+ per worker survey)" to "(the wise-boar-480 worker survey reported ~20+; worker should re-confirm via `grep -n "match.*SurfaceExpr" src/v3/compiler/src/lower.rs` + sibling consumer files at dispatch — survey number is from a snapshot, not authority)." All three observations were APPROVE-non-blocking; landing in-PR for dispatch-doc honesty. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Summary
Bulk authoring per Director ask "clear all dependencies upfront" so worker dispatch isn't gated on incremental brief authoring. 8 worker briefs, all Director ad-hoc territory; each independently dispatchable subject to its named cross-program dependencies.
Doc-only; no code surface.
Briefs landed
T-Substrate sub-lanes (4 — clear T-Modeling pair-blocks + sibling map work)
t-substrate-cardinality-int-lit-worker.mdi64::MINend-to-end)t-substrate-nominal-opaque-secret-worker.mdt-substrate-parametric-algebra-dimensions-worker.mdt-substrate-valuebody-map-worker.mdkernel_algebra_profilemirror dissolution + 21 other map consumers (sibling to PR #790's ValueBody::List)T-ImpossibleBugs (3 — independent, parallel-dispatchable, any-worker)
t-impossiblebugs-nested-optional-flatten-worker.mdOption<Option<T>>flattens at constructiont-impossiblebugs-unhandled-diagnostic-paths-worker.mdt-impossiblebugs-unenumerated-effects-worker.mdT-PerMethodMetadata (1 — design-call close)
t-permethodmetadata-pick-worker.mdDiscipline applied
Every brief follows the established pattern: Read first / Frame / explicit consumer-side requirements / Slice / Acceptance / STOP-AND-ESCALATE / Non-goals / Reporting / Cross-manager note. Every cited file:line anchor was verified at HEAD per the verification-miss discipline lesson from #772 + #786 + the Engine Phase 1 typestructure brief precedent — investigations were run by parallel Explore agents before brief authoring.
Cross-program coordination flagged in briefs
ValueBody::Mapbrief (req 3 parser extension overlap).Honest scope statement (out-of-scope of this PR)
Dispatchability after merge
= 8 parallel-dispatchable workstreams open the moment this lands.
Test plan