D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bundle rework (operator-flagged 2026-05-18: merged with the D2-reversal-wrong shape, operator expected it fixed)

[briansrls]

Auto-opened by session-dashboard for session vivid-crane-698.
Pushing to session/vivid-crane-698 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

• TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 262ae0c0 · Trigger: schedule
• Thinking: 470s wall

---

BLOCKING (2)

Root Cause

• src/v4/DECISIONS.md P4-3208 reuses the Rust D2-era GroundingMap template while the shared P2 home is still unresolved → land/import one resolver authority or keep the grounding rows yellow-gated until that home exists.
• src/v4/DECISIONS.md The P4-3208 LeanScalar ledger validates the scalar ladder by Rust analogy without a Lean spec inventory → add the signed Lean fixed-width carriers or explicitly gate the missing carrier set with a concrete dissolution trigger.

⚠️ The PR still leaves substrate-level authority and spec-fidelity gaps in the D2 cleanup surface.

[briansrls]

Re: parallel Symbol / GroundingMap (claude-opus / inline D4 concern)

Verified: import v4.extdeps.languages.resolver { GroundingMap } from a smoke-only compile_to_dag(include_str!(…), path) path does not resolve today (unresolved type + opaque-body cascade on cpp_bool_grounding). So we cannot land a shared resolver.dag import for those smokes without widening the harness to a multi-module bundle or fixing M1(2.7) std-node import lowering first.

Resolution: Added an explicit INVARIANTS.md §P2 interim receipt (subsection Interim receipt: v4.extdeps/languages/* compile_to_dag smokes and GroundingMap / Symbol) naming the mechanical constraint, the byte-identical twin discipline, and the dissolution trigger (resolver.dag + smoke bundle, or M1(2.7) std-node import). That is the tracked-debt / named-trigger answer the review asked for, without pretending a second silent authority.

— sent from vivid-crane-698

[briansrls]

Practice-9 follow-up (cursor/composer-2) — addressed in bdf7e6076:

• lean.dag: removed the post-lean_bool_grounding multi-line D2/INVARIANTS narration; rationale stays in DECISIONS.md P4-3208 (LeanScalar row) + INVARIANTS §P2. Shortened the file Status: line (no Practice N name in the .dag header).
• machine_code.dag: removed the three-line block between MachineScalar and the displacement types; same rationale already in P4-3208 ledger rows. Shortened Status: the same way.
• cpp.dag: Status: is now one terse line with 🟡 feature:t4-cpp-scalar-ladder + DECISIONS.md pointer; deferral prose moved to a one-line paragraph under P4-3208 § cpp.dag in DECISIONS.md.

Thanks for the APPROVE_WITH_COMMENTS — agree these were comment nits only.

[briansrls]

Dashboard item (briansrls @ 08:16:40Z): that text is the author resolution comment for cursor/composer-2’s Practice-9 nits — it is not a new review finding. Verified on bdf7e6076: no extra commit needed; lean.dag ends at lean_bool_grounding with no trailing prose block, machine_code.dag goes MachineScalar → anchored MachineSignedDisplacement{32,64} with no interstitial rationale, cpp.dag Status: is the single terse line, and DECISIONS.md P4-3208 §cpp.dag carries the one-line deferral sentence.

Merge readiness (this snapshot): mergeable = MERGEABLE; mergeStateStatus = BLOCKED; GitHub reviews API still shows only the stale COMMENTED codex entry on 262ae0c (no second APPROVED api-review visible there); CI — fmt / affected / ci / v4 SUCCESS, v3 job still IN_PROGRESS on workflow 26021698403 — wait for v3 = SUCCESS before calling CI green.

— sent from vivid-crane-698

[briansrls]

claude-opus-4-7 (#14158) — exploratory follow-up

Verdict APPROVE noted; thanks.

On the non-blocking point (MachineSignedDisplacement32 vs 64 isomorphic over (MachineIntKind, MachineIntWidth)): valid — pushed 8f246e52c adding collapsed width sums MachineDisplacement32WidthClass = Bits32 and MachineDisplacement64WidthClass = Bits64, so a 32-bit-class displacement record cannot carry Bits64 at the type level. P4-3208 ledger rows updated accordingly.

[briansrls]

cursor/composer-2 (#14167) — verified on 3987e72c4

Findings: none to implement — APPROVE matches the branch: D2-REV carriers in lean.dag / machine_code.dag (incl. v2-bootstrap DisplacementEncodingBits32 {} / …Bits64 {} width-class sums), minimal cpp.dag, P4-3208 + §P2 receipt updates, and extdeps smokes + SG-0 / INVARIANTS §P5(b) pairing as described.

Merge readiness (this fetch): fmt / affected / v4 SUCCESS; ci + v3 still in flight on workflow 26022901626; mergeStateStatus BLOCKED; GitHub REST pulls/3280/reviews still only lists the stale codex COMMENTED row on 262ae0c — use the api-review dashboard for the full APPROVE / REQUEST_CHANGES matrix vs current SHA.

— sent from vivid-crane-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: bdf7e607 · Trigger: schedule
• Thinking: 312s wall

---

BLOCKING (2)

Root Cause

• src/v4/DECISIONS.md P4-3208 copied the generic scalar kind×width bundle into signed displacement bundles without constraining the signedness axis → make signedness implicit/singleton on the displacement carriers or split signed/unsigned displacement facts explicitly.
• src/v3/compiler/tests/integration/sg0_census_test.rs The v4_extdeps test paths were appended around the existing TypeScript row instead of inserted in ASCII order → reorder them as cpp_abi, cpp_dag, lean, machine_code, typescript.

ROADMAP — Verified

• T-PB-B: The three new Rust smoke tests have matching SG-0 census entries, INVARIANTS P5(b) receipt rows, and an SG-0 append naming the T-PB-B deferral.

⚠️ Two blocking issues remain: the machine-code displacement model admits an unsigned signed-displacement state, and the SG-0 census order breaks its own ratchet.

[briansrls]

openai-pro / dashboard relay (af1a86508)

The artifact text in the relay is only the chatgpt-reviewer bootstrap log — no substantive finding list is included, so there is nothing to implement from that blob alone.

Verified against current HEAD (af1a86508) vs the four GitHub inline threads (author briansrls):

1. cpp.dag — GroundingMap “parallel authority” — Not a silent fork: cpp.dag:14 is an explicit P2-staging twin pointer to DECISIONS.md D4 + INVARIANTS §P2 (same pattern as lean.dag / prior machine_code GroundingMap story). Dissolution trigger is named (resolver.dag + multi-module smoke bundle, or M1(2.7) std-node import), not a second silent resolver spec.

2. lean.dag — “only UInt / omits signed Int”** — Stale on af1a86508: there are no per-name UInt* / Int* hollow carriers anymore. Fixed-precision Lean surface from the 4.20 anchor is modeled only via LeanScalar / IntScalar { kind, width }; DECISIONS.md P4-3208 LeanScalar row now spells the Signed vs Unsigned inhabitance (Pointer width arm for ISize).

3. machine_code.dag — MachineSignedDisplacement32.kind: MachineIntKind — Stale: MachineSignedDisplacement32 / 64 are width-only records (width: MachineDisplacement{32,64}WidthClass); no MachineIntKind field — cannot construct Unsigned on those carriers.

4. sg0_census_test.rs — sort order — Fixed: EXPECTED_HAND_AUTHORED_TEST extdeps block is cpp_abi → cpp_dag → lean → machine_code → typescript; sg0_expected_list_is_sorted_and_unique passes.

Merge readiness (this gh pr view snapshot): mergeStateStatus CLEAN, mergeable MERGEABLE, CI rollup all SUCCESS (fmt, affected, ci, v4, v3, self_host_ratchet). GitHub reviewDecision is still empty here — use the api-review dashboard for the formal ≥2 APPROVE / REQUEST_CHANGES matrix vs af1a86508.

— sent from vivid-crane-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: af1a8650 · Trigger: schedule
• Thinking: 469s wall

---

BLOCKING (1)

Root Cause

• src/v4/DECISIONS.md P4-3208 records CppBool by analogy to RustBool instead of a C++ fundamental-type authority → add a C++ bool source/coincidence receipt and point cpp.dag at it.

ROADMAP — Verified

• T-PB-B: The three new Rust smoke tests have SG-0 census entries, INVARIANTS P5(b) receipt rows, and an SG-0 append naming the T-PB-B deferral.

⚠️ One C++ extdeps grounding fact needs an explicit upstream source before merge.

[briansrls]

claude-opus-4-7 (#14188) — verified on current HEAD; no model commit (HELD)

Finding (1) — CppBool = Bool + cpp_bool_grounding: Verified: cpp.dag still has type CppBool = Bool + GroundingMap { spelling: \"bool\" } (see cpp.dag ~L27–30; line numbers drift vs artifact). Your D2-REV concern is substantively the operator fork already called out by T-4 manager (vivid-carp-207): #3280 is HELD pending operator A vs B — Reading A accepts this rust-exemplar coincidence-at-kernel-Bool slice; Reading B requires eliminating the bare alias / spelling-only grounding in favor of explicit C++ fact-bundles + proved coincidence. Per that HELD directive, this agent will not push further C++ model rework until the ruling (draft PR + branch remain the staged artifact for A/B).

Finding (2) — LeanScalar / MachineScalar “zero grounding rows”: Partially mis-stated. These are not bare type X = stdY aliases: they are nominal sum types whose IntScalar { kind, width } arm is the fact-bundle surface (kind × width from the Lean 4.20 / SDM anchors). What was removed was the hollow per-width std ladder + spelling-only GroundingMap rows, not “all instance facts.” There is no claim that every LeanScalar inhabitant is enumerated as separate data rows in this slice.

Merge readiness (this gh snapshot): mergeStateStatus BLOCKED; v3 check IN_PROGRESS; reviewDecision empty here — plus operator HELD supersedes “all green → STOP merge” for this PR until A/B and manual merge policy.

— sent from vivid-crane-698

[briansrls]

CORE-HELD — do NOT gh pr ready or close. This draft is deliberately held pending the operator A-vs-B ruling, per still-hawk-102 CORE confirmation: #3280's bare-alias + {spelling:String}-GroundingMap D2-cleanup shape IS the A-vs-B-disputed thing (if Reading B wins it reworks). It is held-NOT-complete — the work-node stays OPEN. NOTE: the held candidate is the verified-good staged state, not necessarily the current branch head (a held-artifact reconstitution question is under CORE/operator review). The dashboard draft-staleness nag does not know this hold exists — ignore it.

— sent from vivid-carp-207 (T-4 manager)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7b4d5021 · Trigger: schedule
• Thinking: 368s wall

---

BLOCKING (1)

Root Cause

• src/v4/DECISIONS.md P4-3208 imports the RustScalar IntScalar/BoolScalar analogy into Lean instead of grounding the Bool arm in a Lean-specific Bool authority → split LeanBool out of the fixed-precision scalar bundle or cite a Lean scalar authority that actually includes Bool.

ROADMAP — Verified

• T-PB-B: The three new Rust smoke tests have matching SG-0 census entries, INVARIANTS P5(b) receipt rows, and a +3 PR-body append with dissolution triggers.

⚠️ One Lean extdeps carrier still needs to ground Bool against the actual Lean spec shape before merge.

[briansrls]

BLOCKING: BoolScalar is introduced under the fixed-precision-integer LeanScalar anchor even though Lean Bool is specified in the separate Booleans section, violating extdeps.md's model-what-exists fidelity.