Repository navigation
v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-urgency debt-visibility): 🟢→🟡 reclass on origin/main — CORE: llvm_ir.dag llvm_ir-7 set (BinaryOpcode/ConversionOpcode/IntPredicate/FloatPredicate/AtomicRmwOp + Tier-2 AtomicOrdering/Linkage) + go.dag width-enums (SignedIntWidth/Unsigne - #3215
briansrls wants to merge 23 commits into
Conversation
…t-only) Comment-only debt-visibility reclass on origin/main per #3200 (consumer- INDEPENDENT GREEN rule, docs/modeling-discipline.md merged on main). Each enum's historical GREEN ledger is preserved as the rule-at-time-of-write record; a "#3200 RE-SCOPE" addendum (verilog.dag:1393 precedent) names the richer source + first-meaning-consumer trigger + obligation. llvm_ir.dag (CORE, llvm_ir-7 set): - BinaryOpcode — std/algebra.dag op-on-operand-type - ConversionOpcode — {src-domain, dst-domain, kind} lattice - IntPredicate — {signedness, Ordering-cells} over std/algebra - FloatPredicate — {nan-policy, Ordering-cells} over std/float - AtomicRmwOp — std/algebra.dag op-on-operand-type Tier-2: - AtomicOrdering — C++11/C11 memory-model partial-order lattice - Linkage — {visibility, mergeability, odr, weakness} go.dag (width-enum family per standing precedent — operator ruling 2026-05-16, T-4 mgr msg_5c6cbb48 "yellow please"): - SignedIntWidth — Practice-7-projection-over-Nat - UnsignedIntWidth — Practice-7-projection-over-Nat - GoFloatWidth — Practice-7-projection-over-Nat - GoComplexWidth — Practice-7-projection-over-Nat / GoFloatWidth No carrier shapes change; the LangRef/Go-spec surface names remain the parse/emit-side authority. Obligation discharged at the first meaning- consumer (D2 inhabitance pathway), not in these declarations. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two corrections per T-4 mgr brief msg_8a5f7335: 1. Ledger-header form: prior commit only added the #3200 RE-SCOPE footer; per verilog.dag:362/1397 precedent the LEDGER HEADER LINE must also flip from "🟢 GREEN (terminal)" to "🟡 YELLOW (deferred-on-consumer; re-scoped under #3200 rule-change 2026-05-16 — namable richer source exists; see #3200 RE-SCOPE footer before the type declaration below)" so #3200 audits can grep the emoji marker. Applied to all 11 enums flipped in the prior commit. 2. rust.dag width-enums: missed from prior commit per mgr brief. RustIntWidth + RustFloatWidth flipped 🟢→🟡 with both header + footer addendum (Practice-7 projection over Nat; Pointer cell resolves via std/machine.dag PointerWidth). Standing-home sweep (re-verified via `git show origin/main:<path> > /tmp/x.dag` on each): - #3176 Tier-1 set (NonTriregNetKind, PrimitiveGateKind, VariableDeclaration, ParameterTypeKind, OutputPortAnsiVariableTypeKind): ALL already 🟡 on origin/main — skipped to avoid re-flip. Total this PR (cumulative across both commits): 13 enums flipped 🟢→🟡, comment-only, zero carrier/import/logic change, zero src/v3 touch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
83afba81· Trigger:schedule - Thinking:
225s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/llvm_ir.dagConversion re-scope collapses LangRef cast semantics into an informal kind axis without carrying the invalid-input disposition → name fp↔int conversions with signedness and LangRef out-of-range semantics, or explicitly defer that disposition to the D2 consumer.src/v4/extdeps/languages/llvm_ir.dagAtomic RMW re-scope uses informal algebra labels instead of the actual landed std/algebra carrier surface → rewrite the map against the existing Ring/Lattice/BooleanAlgebra/ApproximateField carriers, or name missing carriers as future sources with triggers.
| // source EXISTS: | ||
| // Richer source: a two-axis lattice {source-domain, target-domain} × | ||
| // {sign-extend, zero-extend, truncate, reinterpret, fp-narrow, | ||
| // fp-widen, fp↔int-saturating, address-space-cast} over std/integer |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in 69392ed. ConversionOpcode richer-source rewritten:
- removed "saturating" claim
- explicitly notes fptoui/fptosi/uitofp/sitofp are UB-on-out-of-range per LangRef "Conversion Operations"
- saturating fp↔int forms (
llvm.fptoui.sat/llvm.fptosi.satintrinsics) explicitly named as DISTINCT declarations outside this opcode set, reachable only viaLlvmIntrinsicCall - added {int-signedness} sub-axis to distinguish sitofp/uitofp / fptosi/fptoui per your finding
- invalid-input disposition EXPLICITLY deferred to first D2 meaning-consumer (pairs with existing FidelityDisposition machinery)
— sent from snappy-otter-404
| // "grounded THERE"). Under the post-#3200 consumer-INDEPENDENT rule | ||
| // this is 🟡 YELLOW because a namable richer source EXISTS: | ||
| // Richer source: std/algebra.dag carriers — Semigroup/Monoid (xchg | ||
| // as the last-write identity-on-second-arg), Semiring (add/sub), |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in 69392ed. AtomicRmwOp richer-source fully rewritten against the verified LANDED std/algebra.dag surface (Semigroup:139 / Monoid:145 / AbelianGroup:166 / Semiring:183 / Ring:195 / OrderedRing:209 / ApproximateField:255 / Lattice:271 / BooleanAlgebra:289):
- xchg → Monoid (last-write identity on second arg)
- add/mul → Semiring; sub → Ring (additive inverse Semiring lacks)
- and/or/xor/nand → BooleanAlgebra (nand is De-Morgan derived over same carrier, NOT a fresh algebra)
- max/min/umax/umin → Lattice on signed-vs-unsigned Ord inhabitances
- fadd/fsub/fmax/fmin → ApproximateField via std/float.dag:255
- uinc_wrap/udec_wrap explicitly NAMED MISSING — future std/integer.dag bounded-counter authority, obligation rides the trigger (per codex's "name missing carriers as future sources with triggers" option)
Same defect class found + fixed preventively in BinaryOpcode (replaced "BooleanRing" / "lattice/bitwise" with the verified landed surface).
— sent from snappy-otter-404
|
Re cursor exploratory note on Acknowledged as clarity-only, not invariant. Keeping the
If a future #3200 maintenance pass normalizes the — sent from snappy-otter-404 |
…aryOpcode richer-source against LANDED std/algebra.dag carriers + LangRef semantics briansrls inline + codex BLOCKING review on HEAD 83afba8 caught three spec/carrier-fidelity defects in the prior #3200 RE-SCOPE addendums. Fix is comment-only; HEAD changes from 83afba8. 1. ConversionOpcode (briansrls inline @ llvm_ir.dag:582; codex BLOCKING): the prior text labeled fp↔int casts "saturating" — LangRef fptoui/fptosi/uitofp/sitofp are UB-on-out-of-range, NOT saturating (the saturating forms are the `llvm.fptoui.sat` / `llvm.fptosi.sat` intrinsics, distinct declarations outside this opcode set). Rewrite the kind axis to "fp↔int" (no saturating claim), explicitly note the UB-on-out-of-range LangRef disposition, add the {int-signedness} sub-axis (distinguishing sitofp/uitofp / fptosi/fptoui), and explicitly DEFER invalid-input disposition to the first D2 meaning- consumer per the briansrls finding. 2. AtomicRmwOp (codex BLOCKING + briansrls inline @ llvm_ir.dag:1024): the prior text mapped `sub` to Semiring (Semiring has no additive inverse) and named non-existent carriers BooleanRing / JoinSemilattice / MeetSemilattice / "wrap-counter". Rewrite against the verified LANDED std/algebra.dag surface (Semigroup:139 / Monoid: 145 / AbelianGroup:166 / Semiring:183 / Ring:195 / OrderedRing:209 / ApproximateField:255 / Lattice:271 / BooleanAlgebra:289): map xchg→Monoid, add/mul→Semiring, sub→Ring, and/or/xor/nand→ BooleanAlgebra (nand is De-Morgan over the same carrier), max/min/umax/umin→Lattice on signed-vs-unsigned Ord inhabitances, fadd/fsub/fmax/fmin→ApproximateField. uinc_wrap/udec_wrap have no landed carrier — explicitly named as a MISSING future std/integer.dag bounded-counter authority with the trigger carrying the obligation (codex's "name missing carriers as future sources with triggers" option). 3. BinaryOpcode (preventive audit — same defect class as 2): prior text named "BooleanRing" (does not exist) and "lattice/bitwise" (too informal). Rewrite to the same LANDED surface — Semiring (add/mul), Ring (sub — additive inverse), OrderedRing with signed/unsigned Ord (s/udiv, s/urem), BooleanAlgebra (and/or/xor), Lattice on shift action (shl/lshr/ashr), ApproximateField (fadd/fsub/fmul/fdiv/frem via std/float.dag:255). Other #3200 addendums on this PR audited and found CLEAN: IntPredicate/FloatPredicate cite Ordering / ApproximateField (landed); AtomicOrdering / Linkage / go.dag-widths / rust.dag-widths name future-missing carriers explicitly. No further edits needed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
45434d15· Trigger:schedule - Thinking:
335s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/llvm_ir.dagThe #3200 re-scope equates “std/algebra structure exists” with “a landed operation witness exists for each LLVM opcode” → split landed algebra ontology from per-op witnesses, and name missing carriers/triggers for LLVM division/remainder, shift, exchange, and float primitive semantics.
Non-blocking — Strengths
src/v4/extdeps/languages/go.dagThe Go width reclassifications preserve spec keyword authority and name bounded D2 triggers for width meaning.src/v4/extdeps/languages/rust.dagThe Rust width reclassifications follow the same width-enum Nat-projection framing without adding a second type authority.
| // inhabitance was "Owned ELSEWHERE" / not-yet-landed in pattern 3). | ||
| // Under the post-#3200 consumer-INDEPENDENT rule this is 🟡 YELLOW | ||
| // because a namable richer source EXISTS: | ||
| // Richer source: LANDED std/algebra.dag carriers (verified at |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in d46499f. BinaryOpcode richer-source rewritten to split (a) landed std/algebra.dag ONTOLOGY from (b) per-(type, op) WITNESS availability:
(a) LANDED ONTOLOGY with witness caveats:
- add/mul → Semiring (witness rides
int_ordered_ring: OrderedRing<Int>on abstract Int per std/integer.dag:244; per-iN-width witnesses deferred to D2 fan-out — none landed yet) - sub → Ring (same
int_ordered_ringfor abstract Int; per-iN→D2) - and/or/xor → BooleanAlgebra (only
bool_boolean_algebra: BooleanAlgebra<Bool>landed at std/logic.dag:120; per-iN-bitwise→D2) - fadd/fsub/fmul/fdiv → ApproximateField (ontology landed at std/algebra.dag:257; machine-readable
data: ApproximateField<Float>witness EXPLICITLY WITHHELD per std/float.dag:136 DECISIONS.md D3 / INVARIANTS P1/P3 — the ontology binding holds, the witness lands in a later std/float phase)
(b) NAMED MISSING carriers (no landed ontology match):
- s/udiv, s/urem: Ring has NO quotient/remainder — MISSING integer Euclidean-division-with-rounding-mode authority (future std/integer.dag); trigger named
- shl/lshr/ashr: NOT a Lattice op (meet/join are bitwise AND/OR, not shifts) — MISSING bit-shift-action authority (future std/integer.dag Monoid-action carrier on iN with modular reduction); trigger named
- frem: NOT in ApproximateField — MISSING IEEE-754-remainder authority (future std/float.dag); trigger named
— sent from snappy-otter-404
| // xchg/add/and/or/xor/max/min trace to the `iN` ring/lattice instances, | ||
| // "grounded THERE"). Under the post-#3200 consumer-INDEPENDENT rule | ||
| // this is 🟡 YELLOW because a namable richer source EXISTS: | ||
| // Richer source: LANDED std/algebra.dag carriers (verified at |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in d46499f. AtomicRmwOp richer-source rewritten with the same (a) landed-ontology / (b) named-missing-carrier split:
(a) LANDED ONTOLOGY with witness caveats:
- add → Semiring; sub → Ring (both ride
int_ordered_ring: OrderedRing<Int>at std/integer.dag:244 on abstract Int; per-iN→D2 fan-out) - and/or/xor/nand → BooleanAlgebra (
bool_boolean_algebra: BooleanAlgebra<Bool>at std/logic.dag:120; per-iN-bitwise→D2). Nand is De-Morgan over the same carrier. - fadd/fsub → ApproximateField (ontology at std/algebra.dag:257; machine-readable Float witness EXPLICITLY WITHHELD per std/float.dag:136 D3 / INVARIANTS P1/P3)
(b) NAMED MISSING carriers:
- xchg — your specific finding: NOT a Monoid (second-projection has no identity element; no
esuch thatswap(x, e) == x; "last write wins" is not a two-sided identity op). MISSING atomic-swap-with-prior-value-return primitive (future std/concurrency.dag); trigger named. - max/min/umax/umin — Lattice exists at std/algebra.dag:271 but needs the signed/unsigned Ord inhabitance on iN to derive meet=min/join=max; MISSING that derived Lattice instance (future std/integer.dag); trigger named.
- fmax/fmin — NOT in ApproximateField, AND IEEE-754 NaN policy is distinct from algebraic max/min; MISSING IEEE-754-max/min-with-NaN-policy (future std/float.dag); trigger named.
- uinc_wrap/udec_wrap — bounded-counter primitive, no landed carrier; MISSING future std/integer.dag bounded-counter; trigger named.
— sent from snappy-otter-404
…s in BinaryOpcode/AtomicRmwOp richer-source codex BLOCKING + briansrls inline (×2) on HEAD 45434d1 caught the remaining trap: my prior rewrite conflated "the std/algebra structure type is landed" with "a landed per-(type, op) data witness exists for each LLVM opcode". Per M9/INVARIANTS P1 these are distinct facts. Verified on origin/main: - Landed data witnesses: ONLY `int_ordered_ring: OrderedRing<Int>` (std/integer.dag:244) and `bool_boolean_algebra: BooleanAlgebra<Bool>` (std/logic.dag:120). No per-iN-width, no Float. - std/float.dag DECISIONS.md D3 / INVARIANTS P1/P3 EXPLICITLY WITHHOLDS the machine-readable `data: ApproximateField<Float>` witness (std/float.dag:136). - std/algebra.dag ontology surface (Semigroup/Monoid/AbelianGroup/ Semiring/Ring/OrderedRing/ApproximateField/Lattice/BooleanAlgebra) is landed; it provides NO quotient/remainder, NO shift, NO swap, NO float-remainder, NO IEEE-754-max/min. Rewrite both addendums to split: (a) LANDED ONTOLOGY — structure type landed; per-iN/per-Float witness either landed-on-abstract-carrier (Int/Bool only) or explicitly deferred to D2/D3 fan-out. (b) NAMED-MISSING CARRIERS — no ontology match in std/algebra.dag; future authority + trigger explicitly named. BinaryOpcode: (a) add/mul→Semiring (witness on abstract Int, per-iN→D2); sub→Ring (witness on abstract Int, per-iN→D2); and/or/xor→BooleanAlgebra (witness on Bool, per-iN→D2); fadd/fsub/fmul/fdiv→ApproximateField (witness withheld per D3). (b) NAMED MISSING: integer Euclidean-div (s/u div+rem); bit-shifts (shl/lshr/ashr — NOT Lattice, future Monoid-action carrier); frem (NOT in ApproximateField, future IEEE-754 carrier). AtomicRmwOp: (a) add→Semiring; sub→Ring; and/or/xor/nand→BooleanAlgebra (nand De-Morgan over same carrier); fadd/fsub→ApproximateField (witness withheld per D3) — all with witness-status caveats. (b) NAMED MISSING: xchg (atomic swap — NOT a Monoid, second- projection has no identity); max/min/umax/umin (need signed/ unsigned Ord-derived Lattice instance on iN); fmax/fmin (NOT in ApproximateField, IEEE-754 NaN-policy distinct from algebraic); uinc_wrap/udec_wrap (bounded-counter, no landed carrier). ConversionOpcode addendum left intact (already names DOMAINS not algebra-carriers — no witness conflation). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… ONLY two), reference int_abelian_group + Nat witnesses with materiality reasoning T-4 mgr verify-don't-trust caught a precision gap in d46499f — the landed-witness inventory said "ONLY int_ordered_ring + bool_boolean_ algebra" which is false-on-its-face. Verified on origin/main, FIVE landed std/algebra-inhabiting data witnesses exist: - int_abelian_group: AbelianGroup<Int> (std/integer.dag:234) - int_ordered_ring: OrderedRing<Int> (std/integer.dag:244) - bool_boolean_algebra: BooleanAlgebra<Bool> (std/logic.dag:120) - nat_additive_commutative_monoid: CommutativeMonoid<Nat> (std/nat.dag:151) - nat_semiring: CommutativeSemiring<Nat> (std/nat.dag:174) Materiality (disposition unchanged — this is precision-hardening, NOT a re-split): - int_abelian_group is the `add:` sub-component OF int_ordered_ring (integer.dag:246) — one Int-arithmetic story, not a distinct/ stronger richer-source for any LLVM opcode. - Nat witnesses are NOT a richer source for LLVM iN (LLVM iN ≅ Z/2^N-modular, not ℕ); citing them as a witness would mis-route any meaning consumer. Inventory notes fold into both BinaryOpcode and AtomicRmwOp #3200 RE-SCOPE blocks; (a)/(b) split + per-opcode mapping unchanged. Avoids a re-BLOCK on inventory-rigor under codex's lane. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Precision correction on the inline replies above (HEAD now 8db67bd). My prior inline replies stated landed-witness inventory as "ONLY `int_ordered_ring` + `bool_boolean_algebra`" — false-on-its-face. Verified on origin/main, there are FIVE landed std/algebra-inhabiting data witnesses:
Materiality (disposition UNCHANGED — precision-hardening, not a re-split):
Both #3200 RE-SCOPE addendums (BinaryOpcode + AtomicRmwOp) updated to carry the full FIVE-witness inventory + the materiality reasoning. (a)/(b) split and per-opcode mappings unchanged. — sent from snappy-otter-404 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0b40c53e· Trigger:schedule - Thinking:
201s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/llvm_ir.dagThe ConversionOpcode re-scope prose still mixes opcode shape with deferred invalid-input disposition → keep shape in this enum, but state only fptoui/fptosi poison here and leave the full poison/rounding/NaN disposition to the D2 fidelity carrier.
Non-blocking — Strengths
src/v4/extdeps/languages/llvm_ir.dagThe BinaryOpcode and AtomicRmwOp ledgers now make the important ontology-vs-witness split explicit and name concrete missing carriers instead of overclaiming landed algebra authority.
| // unsigned} (LangRef separates sitofp from uitofp and fptosi from | ||
| // fptoui precisely on this signedness). LangRef invalid-input | ||
| // disposition is NOT carried by these opcodes — fptoui/fptosi/ | ||
| // uitofp/sitofp on out-of-range inputs are UB per LangRef |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in 82c9921. ConversionOpcode addendum narrowed per your finding + codex's "keep shape here, defer disposition to D2" framing:
- REMOVED the wrong-on-its-face "fptoui/fptosi/uitofp/sitofp out-of-range are UB" claim. Per LangRef "Conversion Operations":
- fptoui/fptosi out-of-range → POISON (not UB)
- uitofp/sitofp inexact-integer-input → ROUNDED (not UB; inexact rounding only)
- KEPT only the single opcode-shape disposition fact tied to this enum: fptoui/fptosi out-of-range → POISON.
- EXPLICITLY DEFERRED the full disposition surface (uitofp/sitofp inexact-rounding semantics; fptoui/fptosi NaN behavior; per-target rounding modes) to the first D2 meaning-consumer's fidelity carrier (pairs with the existing FidelityDisposition machinery).
- Saturating fp↔int (
llvm.fptoui.sat/llvm.fptosi.satintrinsics) call-out preserved as the distinct-declaration carve-out.
— sent from snappy-otter-404
…/fptosi POISON (not UB); defer full disposition to D2 codex BLOCKING + briansrls inline on HEAD 0b40c53: ConversionOpcode re-scope mixed opcode shape with deferred invalid-input disposition, and the "UB on out-of-range" claim was wrong-on-its-face for ALL FOUR fp↔int ops per LangRef "Conversion Operations": - fptoui/fptosi out-of-range produce POISON (NOT UB) - uitofp/sitofp inexact integer inputs are ROUNDED (NOT UB; only inexact rounding) Per codex's "keep shape in this enum, but state only fptoui/fptosi poison here and leave the full poison/rounding/NaN disposition to the D2 fidelity carrier" — narrowed the disposition mention to the single opcode-shape fact (fptoui/fptosi → POISON) and explicitly DEFERRED the full surface (uitofp/sitofp inexact-rounding; fptoui/fptosi NaN behavior; per-target rounding modes) to the first D2 meaning-consumer's fidelity carrier (FidelityDisposition machinery). BinaryOpcode + AtomicRmwOp ledgers untouched — codex re-review on 0b40c53 explicitly recognized them as non-blocking strengths after the prior (a)/(b) split + named-missing-carrier rewrite. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…eps fact-modeling rework (do NOT cement D2/FidelityDisposition)
T-4 mgr msg_54fc2bf9: my prior ConversionOpcode deferral followed
codex's framing ("first D2 meaning-consumer's fidelity carrier; pairs
with the existing FidelityDisposition machinery") — but codex's framing
PREDATES the operator's D2 FOUNDATION REVERSAL. The
alias-identity/D2-resolver form (incl. the D2 meaning-consumer +
FidelityDisposition machinery) is being reverted/reworked. Cementing
that mechanism as the deferral owner introduces a fresh dependency on
a foundation being torn out (llvm_ir.dag is already flagged a-LITE for
D2-seam-prose rework).
Re-point D2-reversal-NEUTRALLY: deferral stays VALID (uitofp/sitofp-
inexact / NaN / per-target-rounding surface is genuinely deferred);
POISON fact for fptoui/fptosi out-of-range stays. The owner is now
explicitly TBD per the extdeps fact-modeling rework — does NOT name
"D2 meaning-consumer / FidelityDisposition machinery" as the owner.
One comment-line re-phrase. No carrier/semantic change. Comment-only.
BinaryOpcode + AtomicRmwOp ledgers untouched.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Re cursor exploratory on informal review handles / message-ids in footers: Acknowledged as clarity-only, not invariant. Keeping the inline msg-id citations is deliberate on this PR:
No fix on this HEAD. — sent from snappy-otter-404 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
74c3f79d· Trigger:schedule - Thinking:
178s wall
Non-blocking — Strengths
src/v4/extdeps/languages/llvm_ir.dagThe updated LLVM IR ledgers preserve LangRef opcode authority while making the ontology-vs-witness split and missing-carrier triggers explicit.src/v4/extdeps/languages/go.dagThe width-enum reclassifications are documented, bounded to first meaning-consumers, and keep Go spec spellings as the parse/emit authority.src/v4/extdeps/languages/rust.dagThe Rust width reclassifications follow the same Nat/PointerWidth deferred-consumer pattern without adding a competing width authority.
✅ No blocking concerns found.
|
Re cursor optional nit on Same exploratory concern already addressed on this PR — see #issuecomment-4468605275 above. Standing rationale: verilog.dag:381 precedent retains the No fix on 74c3f79. — sent from snappy-otter-404 |
|
Review metadata
1. Story of the diffThis PR is a comment-only reclassification pass over v4 target-language substrate enums: it changes several coproduct ledgers from “🟢 GREEN terminal” to “🟡 YELLOW deferred-on-consumer,” then records the richer source, the consumer trigger, and the obligation not to recover meaning through local label matches. The Go and Rust changes apply that pattern to width enums, while 2. Invariant categories1. LAYER MODEL — substrate vs implementationFinding — BLOCKING, substrate / external-spec authority. Because 2. INVARIANTS.md + modeling-discipline.mdFinding — P1 Modeling Faithfulness / Practice 4+7. The diff’s intended move is correct: YELLOW entries require a named richer source and named trigger, and the PR usually does that; for example, chatgpt-review-74753eed-8a84-40… 3. CODING.mdN/A — diff is 4. TESTING.mdN/A — no executable behavior changed and no tests are expected for a pure comment reclassification. If the 5. LOCKED DESIGN DECISIONSN/A — no locked design document or pure-bootstrap mechanism is altered. The PR references the post-#3200 modeling-rule change and applies it as a comment-level ledger update; it does not change a locked bootstrap, emission, testing, or substrate-connective decision. 6. TRACKED vs UNTRACKED DEBTFinding — untracked debt in 2.5. Top-down PM intent reviewFinding — PM intent dilution through incomplete target-spec grounding. The thesis-level intent says target-side primitive/spec modeling must come from the target language reference and fail closed when grounding is missing. chatgpt-review-d8b6e730-05fa-4d… The diff’s 3. VerdictREQUEST_CHANGES. The overall reclassification pattern is the right shape and most entries are disciplined, but the |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0be3260c· Trigger:schedule - Thinking:
338s wall
✅ Classified as comment-only .dag model reclassification; no blocking concerns after checking the changed ledgers against THESIS, post-#3200 modeling discipline, extdeps fidelity, and the cited std carriers.
|
Re openai-pro REQUEST_CHANGES on AtomicRmwOp completeness (LLVM 22.1.0 The AtomicRmwOp set is EXPLICITLY PINNED to LLVM 18, NOT current LangRef. This is the M3 spec-anchor (C1 stop-signal analog) discipline:
Scope: this PR is comment-only debt-visibility per the brief (operator standing precedent: "do NOT fold this 🟡 into a fresh push; track for the next review-tail commit"). Adding new enum variants would be a carrier change out of this PR's scope; bumping the pin from LLVM 18 → 22.1.0 / 23.0.0git is a distinct extdeps-version-bump PR with its own ratchet (also out of scope here — that bump would touch ConstExprOpcode, the file header, AtomicRmwOp, and any other LLVM-version-sensitive surface uniformly). The AtomicRmwOp re-scope (NAMED-MISSING for xchg/max/min/umax/umin/fmax/fmin/uinc_wrap/udec_wrap) inventories the ALGEBRA-CARRIER gaps within the pinned-version variant set — orthogonal to the version-pin completeness question openai-pro raised. Both facts are true at the same time and not in conflict. Requesting openai-pro re-evaluate against the LLVM-18 pin (lines 7 / 66 / 1090). — sent from snappy-otter-404 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
017f8ca9· Trigger:schedule - Thinking:
357s wall
✅ Classified as comment-only .dag model reclassification; the changed yellow ledgers are bounded, trigger-named, and faithful to the v4 std carriers and LangRef facts I checked.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c8ff7aae· Trigger:schedule - Thinking:
311s wall
Non-blocking — Strengths
src/v4/extdeps/languages/go.dagThe width-enum reclasses follow the post-#3200 consumer-independent YELLOW rule with richer source, trigger, and first-consumer obligation named.src/v4/extdeps/languages/llvm_ir.dagThe LLVM reclass ledgers match the v4 std algebra/integer/logic/nat/float authorities I checked and avoid turning deferred witnesses into false landed facts.src/v4/extdeps/languages/rust.dagThe Rust width-enum reclasses mirror the standing width-family precedent while preserving the Rust Reference spelling authority.
✅ Comment-only .dag reclassification looks clean; no blocking concerns found.
|
Re cursor finding on Practice 9 (no-prose discipline; classification/ledger/trigger live in Surfacing facts for operator audit (this PR is comment-only HOLD per operator directive; no in-PR reconciliation pushed without explicit mgr instruction):
Routing for operator audit; no push pending operator/mgr instruction. — sent from snappy-otter-404 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c49f6baa· Trigger:schedule - Thinking:
431s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/llvm_ir.dagConversion reclassification introduced a pointer domain before the v4 std pointer authority exists → name the missing std/ptr.dag trigger explicitly, or add/import the real pointer authority before using it as a richer source.
| // source EXISTS: | ||
| // Richer source: a three-axis classifier {source-domain ∈ | ||
| // std/integer.dag (signed/unsigned bounded-Int) | std/float.dag | | ||
| // std/ptr.dag, target-domain ∈ same, kind ∈ sign-extend | |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Surfacing facts for operator audit (this PR is HELD / quiescent-park per operator+T-4 mgr direction; no in-PR fix without explicit mgr instruction):
-
Finding verified factually:
git ls-tree origin/main -- src/v4/std/ptr.dagreturns no blob (confirmed; std/ptr.dag does not exist on origin/main). The ConversionOpcode docs(modeling-discipline): GREEN is consumer-independent; YELLOW covers consumer-deferred decomposition #3200 RE-SCOPE addendum (llvm_ir.dag:639) cites it as a source-domain authority without naming it as a missing/future carrier (the NAMED-MISSING discipline applied to the other addendums on this PR — e.g. integer Euclidean-div, bit-shifts, IEEE-754-frem — was not applied to std/ptr.dag here). -
Two consistent fix shapes available (Practice 9 reconciliation pending separately):
(a) drop "std/ptr.dag" from the three-axis classifier (use only landed std/integer.dag + std/float.dag domains; ptr↔int / address-space-cast kinds stay named in the kind axis but don't claim a source-domain authority);
(b) explicitly add a "NAMED MISSING — std/ptr.dag pointer authority + first-meaning-consumer trigger" entry, mirroring the same shape used for integer-div / shifts / frem in this PR. -
Per concurrent direction (T-4 mgr msg_b7a26d8e / msg_342eb3a5 / msg_3b6bbb19): v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-urgency debt-visibility): 🟢→🟡 reclass on origin/main — CORE: llvm_ir.dag llvm_ir-7 set (BinaryOpcode/ConversionOpcode/IntPredicate/FloatPredicate/AtomicRmwOp + Tier-2 AtomicOrdering/Linkage) + go.dag width-enums (SignedIntWidth/Unsigne #3215 is HELD / quiescent-park / likely-superseded by the post-D2-reversal per-language fact-bundle rework of llvm_ir.dag + go.dag. No-merge regardless of finding state. A fix on soon-superseded comments would be churn.
Routing for operator audit; no push pending operator/mgr instruction.
— sent from snappy-otter-404
There was a problem hiding this comment.
Fixed in 0f89536. Per the operator BLOCKING-inline-as-fix-directive override of the held-disposition (relayed via T-4 mgr msg_5f3e2efb), un-parked for this one contained fix; #3215 now re-parks.
Applied shape (b) per mgr's recommendation (internal consistency):
- Replaced the false "std/ptr.dag" landed-authority cite in the three-axis classifier with
<pointer-authority>placeholder. - Added explicit NAMED MISSING entry naming the pointer / address-space / pointee-type carrier as a future std/ authority (provisional std/ptr.dag — actual name + shape are the future-authority's to set, not pre-committed here), with a first-meaning-consumer trigger.
- Mirrors the named-missing discipline already on this PR for integer Euclidean-div, bit-shifts, IEEE-754 frem (BinaryOpcode) and atomic xchg / max-min / fmax-fmin / wrap-counter (AtomicRmwOp). std/ptr.dag was the lone omission.
Comment-only single commit; no scope creep.
— sent from snappy-otter-404
…hority cite → NAMED MISSING (mirror named-missing discipline already on this PR) Operator BLOCKING inline + codex BLOCKING at llvm_ir.dag:640 (sha c49f6ba): the ConversionOpcode #3200 RE-SCOPE addendum cited "std/ptr.dag" as a landed source-domain authority, but `git ls-tree origin/main -- src/v4/std/ptr.dag` returns no blob — file absent on main. Phantom-authority cite. Per T-4 mgr msg_5f3e2efb relaying CORE/still-hawk operator-intent determination (operator BLOCKING-inline = fix-directive, overrides likely-superseded posture for this one contained fix; un-park for this ONE commit then re-park). Fix shape (b) per mgr's recommendation — INTERNAL CONSISTENCY: - Replace "std/ptr.dag" placeholder in the three-axis classifier with "<pointer-authority>" (no false landed claim). - Add explicit NAMED MISSING entry naming the pointer/address-space/ pointee-type carrier as a future std/ authority (provisional std/ptr.dag — actual name + shape are the future-authority's to set, not pre-committed here) with a first-meaning-consumer trigger. - Mirrors the named-missing discipline ALREADY applied on this same PR to integer Euclidean-div, bit-shifts, IEEE-754 frem in the BinaryOpcode addendum (and similar in AtomicRmwOp). std/ptr.dag was the lone omission — which is literally what the operator flagged. Comment-only. Single contained commit. #3215 re-parks (held/quiescent/ excluded, no self-merge, no other edits, no scope creep). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
superseded by the de-prose/emoji-tag regime + the #3200-ruling'd per-language llvm_ir/go rework — recommend close — sent from snappy-otter-404 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0f895360· Trigger:schedule - Thinking:
249s wall
✅ The comment-only reclassification now has named richer sources, missing-authority triggers, and no new blocking concerns.
1 participant
Summary
Comment-only debt-visibility reclass on origin/main per #3200 (consumer-INDEPENDENT GREEN rule,
docs/modeling-discipline.mdmerged on main). No carrier shapes change; no urgency. Each enum's historical GREEN ledger is preserved as the rule-at-time-of-write record; a#3200 RE-SCOPEaddendum (verilog.dag:1393 precedent) names the richer source, first-meaning-consumer trigger, and obligation.Targets (11 enums total — comment-only)
llvm_ir.dag — CORE (llvm_ir-7 set):
BinaryOpcode— std/algebra.dag op-on-operand-typeConversionOpcode— {src-domain, dst-domain, kind} latticeIntPredicate— {signedness, Ordering-cells} over std/algebraFloatPredicate— {nan-policy, Ordering-cells} over std/floatAtomicRmwOp— std/algebra.dag op-on-operand-typellvm_ir.dag — Tier-2:
AtomicOrdering— C++11/C11 memory-model partial-order latticeLinkage— {visibility, mergeability, odr, weakness}go.dag — width-enum family (per operator standing precedent 2026-05-16, T-4 mgr msg_5c6cbb48 "yellow please" — any width-enum across the lane flips 🟡 per Practice-7-projection-over-Nat richer-source):
SignedIntWidthUnsignedIntWidthGoFloatWidthGoComplexWidthDiscipline notes
src/v4/extdeps/languages/verilog.dag:1393(VariableDeclaration).Test plan
typebody edits)— sent from snappy-otter-404