Skip to content

docs(modeling-discipline): GREEN is consumer-independent; YELLOW covers consumer-deferred decomposition - #3200

Merged
briansrls merged 1 commit into
mainfrom
merry-ibex-337/modeling-discipline-green
May 16, 2026
Merged

docs(modeling-discipline): GREEN is consumer-independent; YELLOW covers consumer-deferred decomposition#3200
briansrls merged 1 commit into
mainfrom
merry-ibex-337/modeling-discipline-green

Conversation

@briansrls

@briansrls briansrls commented May 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

Closes a gap in Practice 4's coproduct-classification taxonomy: there was no honest home for "the decomposition is known and substrate-ready, but correctly deferred because no consumer needs the meaning yet" (the bounded-by-consumers discipline).

YELLOW's named trigger only covered "substrate work not ready"; RED says "do it now." So a faithful enumeration whose decomposition is known but unneeded (e.g. a Verilog net-kind enum that is structurally {resolution, default, drivers}) had nowhere to go — and leaked into GREEN. That is the bug: a GREEN classification reads as "terminal, settled, route around me," which actively nudges the eventual meaning-consumer toward a local lookup (match k { Wor => OR, … } in their lens) instead of doing the structural decomposition — the exact v3 quiet-workaround failure mode.

The fix — four surgical edits to Practice 4

  • GREEN is now explicitly consumer-INDEPENDENT. "No consumer needs the decomposition yet" is not a basis for GREEN — only "no richer source exists" is. The test: if you can name the axes the variants project over, a richer source exists ⇒ not GREEN.
  • YELLOW's named trigger may be (a) substrate-not-ready OR (b) first consumer of the meaning. A consumer-triggered YELLOW must pre-assign the obligation: the first meaning-consumer owes the structural decomposition, not a lookup. Firing the trigger is the sanctioned path, not a reopening of settled work.
  • New review check — the "lookup smell": a match over a foreign-label coproduct inside a consumer (a lens/transform) to recover a structural fact is the decomposition written in the wrong place — the match arms are the axis. Same channel K-1 closes for Symbol. This review smell is the interim enforcement until a machine-checked meta-lens lands.
  • For Reviewers item 4 updated to require the consumer-independence check + the lookup-smell flag.

Why it matters

Classification (GREEN/YELLOW) tracks does a richer source exist — a fact about the spec, consumer-independent. The work is correctly consumer-bounded. Conflating them is what produced silent latent debt: GREENs that are secretly YELLOW. Expect visible YELLOW to rise — that is the intended effect (v3 died of invisible drift).

Test plan

  • Doc-only change; no code, no .dag. Renders correctly.

🤖 Generated with Claude Code

@briansrls briansrls changed the title v4 design docs(modeling-discipline): GREEN is consumer-independent; YELLOW covers consumer-deferred decomposition May 16, 2026
@briansrls
briansrls marked this pull request as ready for review May 16, 2026 19:44
@briansrls
briansrls merged commit 606034a into main May 16, 2026
14 checks passed
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4.10: flip AcSweepKind 🟢 → 🟡 per PR #3200 rule change (comment-o…
b1d2236 
…nly)

PR #3200 (merged 2026-05-16 19:53:37Z) ratified the operator-directed
modeling-discipline rule change: GREEN is consumer-INDEPENDENT — a
coproduct is GREEN ONLY IF no richer source exists. "No consumer needs
it yet" ≠ GREEN.

merry-ibex-337-led authoritative cross-PR Tier-1 audit identified
AcSweepKind as mis-GREEN: the three variants project over a namable
2D axis `(spacing-law × ratio-base)`:
  - Linear ⇒ spacing-law = arithmetic;  ratio-base = NA
  - Decade ⇒ spacing-law = logarithmic; ratio-base = base-10
  - Octave ⇒ spacing-law = logarithmic; ratio-base = base-2

Comment-only flip (no carrier/code/import/diag change):
- Classification 🟢 GREEN → 🟡 YELLOW (deferred-on-consumer)
- Added rule-change attribution (PR #3200) + axes
- Pattern-4 and Pattern-5 ledger entries updated:
  - Pattern 4: FAILS-AT-THIS-LAYER, but the 2D axis is the richer
    source the YELLOW dissolution targets at the meaning-consumer
  - Pattern 5: SUCCEEDS at the meaning-consumer per #3200's
    parameterized-family pattern; stays coproduct at this file's
    surface because the decomposition is the consumer's obligation
- Named trigger: first consumer of frequency-stepping semantics —
  the AC-analysis sweep-point generator (walks fstart → fstop
  emitting per-step frequencies for `.AC` simulation)
- Pre-assigned obligation: that consumer DERIVES the step law from
  the (spacing-law, ratio-base) axes — NOT a match over the
  {Linear | Decade | Octave} coproduct labels. A typed (spacing-law,
  ratio-base) carrier (or equivalent decomposition) is the
  structural form the consumer owes

This is part of the cross-PR-uniform Tier-1 audit dispatched by
merry-ibex-337 following #3200's merge. SubcircuitStatement and
DeckStatement stay-GREEN (authoritative audit confirmed-clean as
spec's-own-irreducible-partitions).

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics. No structural change; ledger-prose only.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4.9 verilog: re-scope 5 Tier-1 Practice-4 ledgers 🟢 GREEN → 🟡 YE…
20deaa4 
…LLOW per #3200 rule-change

#3200 (docs/modeling-discipline.md rule-change MERGED on origin/main
2026-05-16 19:53:37Z): GREEN is now consumer-INDEPENDENT. A
coproduct is GREEN only if NO richer source EXISTS; "no consumer
needs the decomposition yet" is no longer GREEN — it is 🟡 YELLOW
deferred-on-consumer with a named first-meaning-consumer trigger
and a pre-assigned obligation on that consumer.

Per merry-ibex-337's authoritative cross-PR audit, #3176's Tier-1
mis-GREEN list under #3200 is exactly FIVE:

1. NonTriregNetKind — axes: {resolution_function,
   default_when_undriven, driver_arity, designer_intent_marker};
   trigger: first consumer of net-resolution semantics; obligation:
   {resolution, default, arity} record at consumer.

2. VariableDeclaration — axes: {storage-class, width, signedness,
   algebra-grounding}; trigger: first consumer of variable-storage /
   algebra semantics (D2 inhabitance pathway); obligation:
   structural decomposition into the storage-class matrix at
   consumer.

3. OutputPortAnsiVariableTypeKind — same storage-class family as
   VariableDeclaration (output-admissible subset; real/realtime
   excluded per §12.3.3); same D2 trigger + obligation.

4. ParameterTypeKind — same storage-class family as
   VariableDeclaration (compile-time-constant variant at parameter
   position); same D2 trigger + obligation.

5. PrimitiveGateKind — axes: {gate-family, logic-function,
   inversion, polarity, controllable-enable, resistive,
   transmission}; trigger: first consumer of gate-class semantics
   (elaboration / simulation dispatch); obligation: gate-family
   matrix at consumer.

Comment-only edit: 5 Practice-4 ledger headers flipped 🟢 GREEN →
🟡 YELLOW + 5 "#3200 RE-SCOPE" footers added before each type's
declaration with axes + trigger + obligation. NO carrier shape /
field-type / code / import changes — purely the Practice-4
classification labels updated. The 14 over-flagged in the worker's
duplicate sweep (PortDirection, EdgeTrigger, ProceduralAssignKind,
Signedness, VectorednessClause, NonAnsiPort, AnsiPortDeclaration,
AlwaysBlockSensitivity, PortConnections, ParameterOverrides,
LifetimeClause, AnsiModuleItem, ModuleKeyword, VerilogModule) STAND
DOWN — clean per merry-ibex-337's authoritative cross-PR list (small
binary present/absent partitions and presence-form Disjs are
terminal under #3200's namable-richer-source test).

Rule-change-attributed: each footer explicitly notes "correct under
pre-#3200 consumer-DEPENDENT rule, re-scoped under post-#3200
consumer-INDEPENDENT rule." Not a prior error; a rule re-scope.

grep -c '🟢 GREEN' = 36 (was 41); grep -c '🟡 YELLOW
(deferred-on-consumer; re-scoped under #3200' = 5; grep -c
'^// #3200 RE-SCOPE (rule-change' = 5. Invariants intact.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4.10: model extdeps/formats/spice.dag — Shape-B netlist (B2-OMNI…
ef189a2 
… probe ✓) (#3168)

* WIP: T-4.10 spice

* v4 T-4.10: review fixes — Mosfet `source_terminal`→`source` + Parameter prose

Addresses cursor/composer-2 APPROVE_WITH_COMMENTS on PR #3168:

1. Mosfet field name vs Practice-4 ledger drift (spice.dag:251-252 vs :288):
   ledger described terminals as `drain`/`gate`/`source`/`body` but the
   field was `source_terminal`. Renamed the field to `source` — matches
   the SPICE3 MOS convention (Quarles 1993), matches the ledger text,
   and is legal (the same field name is used by `Directive.Dc` and by
   `algebra.dag`'s `Homomorphism`).

2. Parameter prose vs types (spice.dag:216-220 vs :286): the Parameter
   doc-comment claimed `Diode`'s optional `AREA` as a use site, but the
   `Diode` variant in this initial cut is `{ identity, anode, cathode,
   model }` with no parameter slot. Narrowed the prose to name only the
   variants that DO carry `parameters` today (`Mosfet`, `SubcircuitCall`)
   and explicitly flagged `Diode`/`Bjt` instance parameters as part of
   the same follow-up that enumerates E/F/G/H/J/T/S/W — the carrier is
   ready for them; the variants are not.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
indexed 63 modules, resolved 63 sources, 0 diagnostics.

The "merge hygiene — squash the WIP commit" exploratory note is moot
under squash-merge: the squash commit picks up the PR title/body, not
individual commit messages.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: address 3 BLOCKING codex findings — .End structural, ModelKind/Component → 🟡 YELLOW

PR #3168 codex review (sha 2c666933, 242s) raised three substrate-shape
gaps; all three are valid + addressed structurally rather than glossed.

1. `.END` is the SPICE3 file TERMINATOR, not a repeatable Directive
   (Quarles 1993 §2.4): exactly one, always last, never repeatable. The
   prior `End` Directive variant + `directives: List<Directive>` admitted
   illegal states (zero / multiple / mid-position `.End`) — INVARIANTS P2
   violation. Removed `End` from the `Directive` coproduct entirely.
   `.End` is now owned by the parse/emit DISCIPLINE: parse success
   structurally requires exactly one trailing `.END` (absence /
   duplication / mid-position = Diagnostic); emit always appends `.END`
   after the last directive. Added header notes to both `Directive` and
   `SpiceNetlist` documenting why `.End` has no data shape it could
   correctly take here. There is nothing in the data model that
   `.End`'s removal silently loses — the terminator obligation moves
   from "a variant in a list" to "a structural property of valid
   parse/emit output", which is exactly where the spec puts it.

2. `ModelKind` was claimed 🟢 GREEN with 5 variants (Diode/BjtN|P/
   MosfetN|P), but the SPICE3 `.MODEL` authority is 15 kinds (R, C, URC,
   LTRA, SW, CSW, D, NPN, PNP, NJF, PJF, NMOS, PMOS, NMF, PMF — Quarles
   1993 §6). The 🟢 claim was dishonest about the closure: claiming a
   subset is terminal masks a real coverage gap. Reclassified 🟡 YELLOW
   with named trigger: dissolves to 🟢 when the full SPICE3 .MODEL set
   is enumerated (tied to Component's 🟡 trigger — same authority).

3. `Component` was claimed 🟢 GREEN with 10 variants (R/C/L/V/I/D/Q/M/K/X)
   but TWO distinct coverage gaps were unhonored:
   (a) 7 SPICE3 elements not yet enumerated (E/F/G/H/J/T/S/W).
   (b) Each enumerated variant carries MANDATORY-positional facts only,
       not the full SPICE3 §11 statement grammar — Resistor missing
       TC/TEMP/optional .MODEL ref, Diode missing AREA/OFF/IC, Bjt
       missing optional substrate-terminal + AREA/OFF/IC, V/I-sources
       missing transient source specs (DC/AC magnitude+phase + PULSE/
       SIN/EXP/PWL/SFFM). Each enumerated variant is itself a partial-
       grammar scaffold. Reclassified 🟡 YELLOW with a compound named
       trigger (both gaps named explicitly); the per-variant grammar
       gap is enumerated in the modeling-note "HONESTY NOTE" so the
       missing facts are tracked, not vaporized.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
indexed 63 modules, resolved 63 sources, 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: Consumes-strike pending-ratification note (T-4 mgr ruling)

Per T-4 mgr vivid-carp-207 ruling (msg_0909f4b5) on PR #3168: my
Consumes-line correction (dropped stale primitive.dag + node.dag/
collection.dag) is correctly surfaced — not a silent rewrite — but
the scaffold-contract change itself is operator-ratification tier
per memory `project_v4_scaffold_header_substrate_drift_pattern`; the
verifier/mgr never blesses or blocks per-file Consumes strikes. The
operator ratifies the systemic scaffold-Consumes reconciliation
uniformly across spice + ptx (#3170) + verilog. Added one inline
line to the Consumes block declaring the change as pending that
ratification.

Do NOT revert the correction itself: reverting re-introduces the
PR #3152-deleted `primitive.dag` citation, a fact-of-record stale.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: address 4th BLOCKING — Bjt substrate-spec + instance parameters

PR #3168 codex inline BLOCKING (sha 2c666933) at spice.dag:293:
"Bjt fixes Q-card shape to collector/base/emitter/model and drops the
optional substrate node plus instance payloads, so valid SPICE3 BJT
statements cannot be represented (P1/P2)."

Finding valid. SPICE3 §11.4 BJT cards admit two syntactic-surface forms
(3-terminal `Q1 c b e m` vs 4-terminal `Q1 c b e s m`) and a set of
instance modifiers (`AREA`, `OFF`, `IC=Vbe,Vce`). The prior shape
`{ identity, collector, base, emitter, model }` could not round-trip
either fact.

Structural fix:

1. New `SubstrateSpec` typed sum (closed binary, 🟢 GREEN with the
   full 5-pattern Practice-4 ledger):
     SubstrateSpec = SubstrateImplicit | SubstrateExplicit { node: NodeRef }
   `Option<NodeRef>` was explicitly rejected per std/diagnostic.dag
   header discipline (`Correction = Suggested(Node) | Unavailable(...)`
   over `Option<Node>`); the closed two-variant typed sum is the
   P2-faithful encoding of the optional-substrate choice. The two
   variants are syntactically distinct at the deck surface (parse∘emit
   preserves the choice) even though they reduce to the same circuit
   topology when SUBSTRATE=node 0.

2. `Bjt` variant becomes:
     Bjt { identity, collector, base, emitter, substrate: SubstrateSpec,
           model: Symbol, parameters: List<Parameter> }
   `parameters: List<Parameter>` is the lexical-surface scaffold for
   instance modifiers (AREA, OFF, IC=Vbe,Vce), exactly matching the
   `Mosfet` variant's slot. Flag-form modifiers like bare `OFF` are
   encoded as `Parameter { name = OFF, value = SpiceValue { lexeme = "" } }`
   — an admissible workaround at the lexeme layer, surfaced honestly
   in the `Parameter` declaration's "FLAG-FORM INSTANCE MODIFIERS" note.

3. Updated the `Component` HONESTY NOTE: marked the `Bjt` per-variant
   grammar gap as ADDRESSED (substrate-spec + instance-params); the
   remaining gaps (Diode AREA/OFF/IC, Resistor/Capacitor/Inductor
   TC/TEMP/optional .MODEL ref, V/I-source transient specs PULSE/SIN/
   EXP/PWL/SFFM) stay 🟡-tracked under the same named trigger.

4. Updated `Parameter` doc-block: lists Bjt among the variants carrying
   `parameters: List<Parameter>` today, lists Diode/V/I/passives as the
   remaining instance-modifier follow-up, and adds the parameter-name
   schema + flag-form modifier notes that justify `List<Parameter>` as
   the intermediate scaffold (a typed sub-coproduct per element is the
   eventual 🟢 destination, tied to `Component`'s 🟡 trigger).

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
indexed 63 modules, resolved 63 sources, 0 diagnostics.

Per the codex review's pattern, future inline BLOCKINGs on Diode /
V/I / passives are predictable and have the same fix shape — per-
variant structural completion is now the established discipline.
The 🟡 trigger lists every remaining gap explicitly so future fixes
are mechanical, not new modeling.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: rephrase SpiceNetlist emptiness comment (cursor exploratory)

PR #3168 cursor/composer-2 exploratory: the prior "Lists are non-empty
by no structural constraint" phrasing was ambiguous — readable as
either "lists are required to be non-empty (no constraint allows them
empty)" or "no constraint requires non-emptiness, so they may be empty."
Rephrased to unambiguous active voice: "Emptiness ... is NOT structurally
ruled out at this layer ... The lists may therefore be empty as a matter
of type." Added a concrete example of the semantic-non-emptiness check
the simulator-driver layer would do (a deck with nothing to simulate).

No structural change; doc-comment only.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: flip cross-ref directions for ModelKind ↔ Component (cursor exploratory)

PR #3168 cursor/composer-2 exploratory: Component is declared before
ModelKind in this file, so Component's trigger comment saying
"ModelKind's 🟡 trigger above" reads backwards (it's below); same
inverse in ModelKind's trigger saying "see Component below" (it's
above). Both flipped to read literally.

Doc-comment only. Verified: 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: Directive 🟡 trigger — add .PZ/.WIDTH + per-variant grammar gaps

PR #3168 codex inline BLOCKING (line 552): "Directive's yellow trigger
tracks only missing directive names and omits valid `.PZ` plus optional
grammar on modeled directives such as `.TRAN TSTART/TMAX/UIC` and two-
source `.DC`, leaving the scaffold unbounded against the SPICE3
authority (P1/P2/P5)."

Finding valid. Restructured Directive's HONESTY NOTE to mirror
Component's structure, with the same two-gap discipline + the explicit
synchronization-discipline note:

1. DIRECTIVE-KIND COVERAGE (gap a) — added missing kinds to the list:
   `.PZ` (pole-zero analysis — flagged by the review) and `.WIDTH`
   (also missing per Quarles 1993 §11.5). Combined with the existing
   `.NOISE`/`.TF`/`.SENS`/`.DISTO`/`.FOUR`/`.PRINT`/`.PLOT`/`.SAVE`/
   `.LIB`. Same synchronization-discipline language as Component's
   list — a missing directive name lets the 🟡 trigger false-fire
   green (M3 / P1 failure mode the review surfaced).

2. PER-VARIANT GRAMMAR COVERAGE (gap b) — new section parallel to
   Component's per-variant grammar list. Enumerates the optional
   facts on already-modeled directives that the current variants
   don't carry:
   - Tran: missing `TSTART` (default 0), `TMAX` (default
     (TSTOP-TSTART)/50), flag `UIC`. Current shape is `{ tstep,
     tstop }` only.
   - Dc: missing optional second-source nested sweep `[SRC2 VSTART2
     VSTOP2 VINCR2]`. Current shape is single-source only.
   - Ac / Op / InitialCondition / NodeSet / Options / Include: noted
     as complete-for-mandatory-grammar at this layer; surfacing
     honestly so a future spec re-read can flag a miss.

3. Trigger updated to require BOTH gaps closed before reclassifying
   🟢 (with shape hints: the optional 2nd-source sweep can be modeled
   as Implicit/Explicit typed sum like `SubstrateSpec`, or as a
   nested-sweep variant; the choice is part of the dissolution work).

The Component synchronization-discipline pattern (added in the prior
commit for Z/O/U) is now also applied to Directive — same lesson,
same scope.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: drop directives field from SubcircuitDefinition (P2 type-enforcement)

PR #3168 codex inline BLOCKING (line 616): "SubcircuitDefinition stores
`directives: List<Directive>`, making `.OP`/`.TRAN`/`.AC` and other
control cards representable inside `.SUBCKT` even though SPICE3 forbids
control lines there (P2/API-level enforcement)."

Finding valid. SPICE3F5 §3.4 permits ONLY component instances and
`.MODEL` cards inside a `.SUBCKT/.ENDS` pair; analysis/control cards
are top-level only. The prior shape carried `directives:
List<Directive>` and tracked the prohibition as a "consumer-side well-
formedness check" — but INVARIANTS P2 / modeling-discipline.md
Practice 2/6 require illegal states UNREPRESENTABLE, not merely
checked. The reviewer's call is exact and the fix is structural:

  - Removed `directives: List<Directive>` from `SubcircuitDefinition`.
  - An `.OP` (or any other Directive variant) inside a `.SUBCKT` is
    now STRUCTURALLY UNREPRESENTABLE in a `SubcircuitDefinition`
    value — the type system rejects it; no checker required.
  - Updated the header note: previous "consumer-side check" language
    is gone; the prohibition is now type-enforced, in the same
    discipline as `Component`'s closed-set + per-variant terminal
    slots.

The `SubcircuitCall` Component variant (top-level subcircuit
invocation) is unchanged; subcircuit-INVOCATIONS still appear in the
top-level `components: List<Component>` list, where they belong.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: preserve SUBCKT lexical scope via parent_scope: List<Symbol>

PR #3168 codex inline BLOCKING (line 608): "Resolving nested subcircuit
calls against a top-level flat list erases SPICE3's local nested-
subcircuit scope, so same-named local definitions in different parents
become ambiguous competing authorities (P1/P2)."

Finding valid. SPICE3F5 §3.4 lexically scopes `.SUBCKT` names to their
enclosing subcircuit — two `.SUBCKT FOO`s in different parents are
distinct definitions, but the prior flat-list shape with bare Symbol
keys made them collide.

Design forks:
  (i)  Recursive `SubcircuitDefinition` (self-referential type) — A1
       reserves recursion-via-type-self-reference for the substrate
       root; adding a domain-carrier recursive type is a substrate-
       design call that exceeds worker authority.
  (ii) Flat lift + bare Symbol — the prior shape; loses scope (this
       BLOCKING).

Fix (does not introduce a recursive type):
- Added `parent_scope: List<Symbol>` to `SubcircuitDefinition`,
  outermost-first; `[]` = top-level, `[BAR]` = inside `.SUBCKT BAR`,
  `[BAZ, BAR]` = inside `.SUBCKT BAR` inside `.SUBCKT BAZ`. List-depth
  tracks nesting-depth structurally. Two same-named SUBCKTs in
  different parents now have DISTINCT `(name, parent_scope)` identities
  — they are no longer competing authorities.
- `SubcircuitCall.subcircuit` resolution: positional (the call's
  containing `components` list determines its enclosing scope) +
  walks up the scope chain per SPICE3 §3.4 shadowing rules
  (innermost first, then outward, then top-level). This is consumer-
  side logic; the data model preserves the facts the consumer needs.
- Updated the top-of-file "SUBCIRCUIT NESTING + LEXICAL SCOPING"
  modeling note + the `SubcircuitDefinition` declaration's header to
  document both design forks and why `List<Symbol>` (kernel-ambient,
  flat) is the safer call versus a recursive carrier (which would
  parallel A1's sole-recursive-type discipline for a non-substrate
  domain concern).

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: sync Component 🟡 trigger text with missing-list (O/U/Z)

PR #3168 codex BLOCKING (REQUEST_CHANGES on sha 32ea6919): "missing-
element list 'MUST stay synchronized' or the 🟡 trigger can 'false-fire
green' ... But the actual reclassification trigger only requires
adding (E/F/G/H/J/T/S/W), omitting O/U/Z."

Finding exact + load-bearing. My commit `9fad7b3f0` added Z/O/U to the
missing-list at line 318 (with explicit synchronization-discipline
language) but did NOT update the trigger TEXT at line 378, which still
named only the original `(E/F/G/H/J/T/S/W)` set. The contradiction is
exactly the failure mode the synchronization note warns about — a
green trigger that fires while a documented-as-missing element remains
unmodeled.

Fix (two textual occurrences):
- Trigger at line 378: now reads "all SPICE3F5 elements named in the
  missing-list above (E, F, G, H, J, O, S, T, U, W, Z)" — names every
  element in the missing-list explicitly so future drift between the
  two texts is immediately visible.
- `Parameter` doc-block at line 239 (the related cross-ref): same
  update — now reads "enumerates the missing-list (E, F, G, H, J, O,
  S, T, U, W, Z)" rather than the obsolete short form.

The Component HONESTY NOTE missing-list (line 318) is unchanged — it
was already correct after `9fad7b3f0`; this commit just makes the
trigger and cross-reference match it.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: reconcile authority claim with coverage state (FIDELITY SCOPE)

PR #3168 codex BLOCKING (REQUEST_CHANGES on sha 32ea6919 / 2026-05-16
02:07): "Marking the missing SPICE3 directive/model coverage as a
tolerated yellow subset means valid SPICE3 decks using omitted cards
cannot be represented by this authority, which is a concrete Modeling
Faithfulness miss rather than just implementation debt ... the diff
still blesses a partial SPICE3 authority as if it satisfied the named
format-model target. That needs explicit reconciliation or a scope
change before approval."

Finding valid + load-bearing. The file's stated authority ("SPICE
netlist model") conflicted with three sites that acknowledged partial
coverage as "deliberate non-exhaustive scoping the probe permits" /
"SUBSET of the SPICE3 .MODEL authority" / "tracked by the YELLOW
classification". The reviewer asked for either full coverage or an
explicit scope reconciliation; full SPICE3 spec coverage is substrate-
design-tier modeling work, so this commit does the scope
reconciliation (worker-tier).

Added a new "FIDELITY SCOPE" section to the top-of-file modeling
notes that EXPLICITLY DISTINGUISHES two deliverables:

  (1) SHAPE DELIVERABLE — substrate-design decisions the T-4.10 probe
      tests (closed coproducts, per-variant terminal slots, typed
      sums for optional fields, lexical-scope-preserving SUBCKT lift,
      .END as parse/emit discipline, subcircuit-body type-enforcement,
      well-formed-by-construction at the shape layer). COMPLETE for
      the T-4.10 scope. The B2-OMNI O(N+M) substrate-validation claim
      rests on the SHAPE, not on coverage exhaustiveness.

  (2) SPEC-EXHAUSTIVE COVERAGE — full enumeration of every SPICE3F5
      element / .MODEL / directive kind + per-variant grammar facts.
      PARTIAL. The YELLOW classifications + named triggers on
      Component/ModelKind/Directive track the gap; each missing-list
      is synchronization-disciplined against the SPICE3F5 anchor.

What the file CLAIMS authority for: (1). What it DOES NOT yet claim:
(2). A valid SPICE3 deck using an omitted kind cannot be represented
in the current state — bounded, documented, and the YELLOW triggers
name the work that closes the gap. The "probe permits non-exhaustive
coverage" framing means the SHAPE deliverable did not require
concurrent spec-exhaustive coverage — it does NOT mean the fidelity
gap is excusable; the YELLOW triggers track that gap as load-bearing
follow-up, not as discretion to leave unfilled.

Additional fixes:
- CLOSED-SET COVERAGE passage (line 156 → was missing the O/U/Z
  expansion + still used "probe permits" framing) now references the
  FIDELITY SCOPE explicitly and lists all 11 unenumerated kinds.
- ModelKind HONESTY NOTE now cross-refs FIDELITY SCOPE deliverable
  (2) gap.
- Directive HONESTY NOTE now cross-refs FIDELITY SCOPE deliverable
  (2) gap.
- Component HONESTY NOTE now cross-refs FIDELITY SCOPE deliverable
  (2) gap.

The three sites the reviewer specifically flagged (lines 156, 443,
560) are now consistent with the file's authority claim — the
authority is the SHAPE; the coverage is documented load-bearing
follow-up.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: .IC/.NODESET variadic via NodeVoltageBinding list (openai-pro BLOCKING)

PR #3168 openai-pro/gpt-5-5-pro REQUEST_CHANGES: ".IC and .NODESET are
documented as complete, but their variants only carry one node/value
pair even though the SPICE3 card grammar is variadic ... `.NODESET
V(NODNUM)=VAL V(NODNUM)=VAL ...` and `.IC V(NODNUM)=VAL V(NODNUM)=VAL
...` — so this model either cannot represent a valid single card
faithfully or silently normalizes one card into multiple directive
facts without declaring that normalization."

Finding valid (P1 modeling-faithfulness / P2 boundary-discipline).
Single-binding variants forced silent one-card-to-many-directive
normalization, breaking parse∘emit round-trip identity.

Structural fix:

1. New `NodeVoltageBinding` record: { node: NodeRef, value: SpiceValue }.
   Modeling note explicitly cites the round-trip concern and the
   silent-normalization anti-pattern it prevents.

2. `InitialCondition` and `NodeSet` variants now carry
   `assignments: List<NodeVoltageBinding>` instead of bare
   `{ node, value }`. One SPICE3 `.IC` or `.NODESET` card with N
   bindings maps to ONE `Directive` value with N assignments — no
   silent normalization.

3. Updated the Directive HONESTY NOTE per-variant grammar list:
   - Removed the false "complete-for-mandatory-grammar" claim on
     InitialCondition / NodeSet.
   - Added an explicit ADDRESSED entry for IC/NodeSet documenting the
     fix and crediting the review.
   - Left Ac / Op / Options / Include as complete-for-mandatory-
     grammar with the per-directive grammar shape spelled out so any
     spec re-read can flag a miss (Ac has 4 mandatory positional
     fields; Op nullary; Options variadic-via-parameters; Include
     one-filename).

Tran's optional TSTART/TMAX/UIC and Dc's optional 2nd-source sweep
remain YELLOW-tracked under the existing trigger — those are genuinely
optional in the spec, distinct from the variadic-cardinality issue
this commit addresses.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: enforce non-empty subcircuit ports via SubcircuitPorts (openai-pro BLOCKING)

PR #3168 openai-pro inline BLOCKING (spice.dag:762): "SPICE3 §2.4
requires `.SUBCKT` external nodes to be present and nonzero, but
`terminals: List<NodeRef>` admits an empty port list and the same
ground-capable `NodeRef` used by component terminals (P1/P2)."

Two parts. (1) Ground-capable port was already addressed in commit
`443c56da4` (terminals is `List<Symbol>`, ground excluded by element
type). (2) Empty-port list was still admitted by the bare `List<
Symbol>` shape — I had previously deferred this as YELLOW debt citing
"std/-substrate non-empty-list refinement", but it can be modeled
inline without a substrate addition.

Fix:

New `SubcircuitPorts` record:

    type SubcircuitPorts {
      first: Symbol
      rest: List<Symbol>
    }

`SubcircuitDefinition.terminals: List<Symbol>` is replaced by
`ports: SubcircuitPorts`. A zero-port `SubcircuitPorts` value is
unconstructible (the `first` field is mandatory) — STRUCTURALLY
UNREPRESENTABLE, P2 illegal-states-unrepresentable. Ground exclusion
is preserved by the `Symbol` element type.

Why a head+tail record instead of a typed sum
(`OnePort | MultiPort | ...`): the record is the canonical std/
non-empty-list shape, adds no per-arity enumeration overhead, and uses
only the kernel-ambient `List` carrier. A generic `NonEmptyList<T>`
refinement is the eventual std/-substrate dissolution; the inlined
head+tail record is the worker-tier scaffold that doesn't require it.

Updated the SubcircuitDefinition modeling note to consolidate both
constraints (NO GROUND + NON-EMPTY) into a single "PORTS EXCLUDE
GROUND AND ARE NON-EMPTY" section; the prior YELLOW-debt note about
non-emptiness is removed because the debt is now closed.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: NodeVoltageBindings non-empty + DeckStatement top-level order (codex BLOCKING ×2)

PR #3168 codex BLOCKING (REQUEST_CHANGES on sha bab3956f):
1. ".IC and .NODESET are modeled as `assignments: List<
   NodeVoltageBinding>`, which admits an empty card even though the
   card syntax requires at least one binding."
2. "`Directive.Include` is modeled as a top-level directive, but
   `SpiceNetlist` still splits the deck into separate components/
   models/subcircuits/directives lists. That loses top-level statement
   order, so a deck that interleaves `.INCLUDE` with models or
   component instances cannot be represented without reordering."

Both findings valid. Two structural fixes, both extending disciplines
already established for sibling carriers:

1. **NodeVoltageBindings non-empty.** New head+tail record matching the
   `SubcircuitPorts` discipline:

       type NodeVoltageBindings {
         first: NodeVoltageBinding
         rest: List<NodeVoltageBinding>
       }

   `Directive.InitialCondition.assignments` and
   `Directive.NodeSet.assignments` are now `NodeVoltageBindings` (not
   `List<NodeVoltageBinding>`). A zero-binding card is now
   STRUCTURALLY UNREPRESENTABLE — INVARIANTS P2.

2. **DeckStatement coproduct for top-level ordering.** Mirrors the
   `SubcircuitStatement` discipline at the deck layer:

       type DeckStatement
         = DeckComponent { component: Component }
         | DeckModelCard { model: ModelCard }
         | DeckSubcircuit { definition: SubcircuitDefinition }
         | DeckDirective { directive: Directive }

   `SpiceNetlist` is now `{ title: String, body: List<DeckStatement> }`
   (the prior four parallel lists `components`/`models`/`subcircuits`/
   `directives` are removed). The deck body now preserves source-order
   interleaving of all four statement kinds through `parse ∘ emit`.
   Full 5-pattern Practice-4 🟢 GREEN ledger added.

Secondary fidelity concession documented honestly in the SpiceNetlist
header: lifted nested `.SUBCKT` definitions appear in the top-level
body at canonical post-lifting positions (not their original within-
parent positions). Their `parent_scope` chain preserves parent
identity; emit re-nests them inside the parent's body. The exact
within-parent position is NOT preserved by this shape (a YELLOW debt
documented in the modeling notes — closing it would require either
position metadata on SubcircuitDefinition or admitting nested
SubcircuitDefinitions as SubcircuitStatement variants, both of which
have substrate-shape implications). The current shape favors top-
level interleave fidelity (the reviewer's flagged concern) over
within-parent nesting position.

Updated the SUBCIRCUIT NESTING + LEXICAL SCOPING modeling note
cross-ref to point at the new `body`/`DeckComponent` structure.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: NamedNode standalone carrier + header Owns sync (codex BLOCKING + nit)

PR #3168 codex BLOCKING (sha c436bbfc): "Subcircuit port identity is
modeled as an unrefined Symbol instead of a non-ground named-node
carrier — split NodeRef into Ground plus a reusable named-node
carrier and use that carrier inside SubcircuitPorts."

Plus non-blocking improvement: "The header Owns line still names the
old bucketed SpiceNetlist fields even though the landed type uses
`body: List<DeckStatement>`."

Both addressed:

**1. `NamedNode` standalone carrier** (BLOCKING fix). Extracted the
`NamedNode` content from the `NodeRef.Named` variant as a reusable
standalone record:

    type NamedNode {
      name: Symbol
    }

    type NodeRef
      = Ground
      | Named { node: NamedNode }

`SubcircuitPorts` element type is now `NamedNode` (not `Symbol`).
Prior shape achieved ground-exclusion only by being LESS PERMISSIVE
than `NodeRef` (a `Symbol` can't carry the `Ground` variant) — a fact
by absence, not a positive type guarantee. `NamedNode` makes
"port-element-is-a-named-node-not-ground" a STRUCTURAL type fact: a
value of `NamedNode` is, by construction, not the ground variant of
`NodeRef`. Same Symbol payload at the bottom; the type-level signal
now carries the engineering invariant directly.

Updated:
- `NodeRef` variant `Named` wraps a `NamedNode` (was inline `{ name:
  Symbol }`).
- `SubcircuitPorts.{first, rest}` are `NamedNode` (were `Symbol`).
- NodeRef 5-pattern ledger updated to reflect the new variant shape.
- SubcircuitDefinition "PORTS EXCLUDE GROUND" modeling note rewritten
  to explain the positive-type-fact-vs-absence-by-permissiveness
  distinction the reviewer surfaced.

**2. Header `Owns:` SpiceNetlist line synced** (nit fix). Updated from
the obsolete `{ title, components, models, subcircuits, directives }`
shape to the current `{ title: String, body: List<DeckStatement> }`,
with a note explaining the source-order-preserving body and the
variadic-card `NodeVoltageBindings` for `.IC` / `.NODESET`.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: rename "Practice 5" → "Practice-4 pattern 5" (cursor exploratory)

PR #3168 cursor/composer-2 exploratory: at spice.dag:191-192 the text
"(Practice 5 fails by inspection of the payloads)" cross-references the
wrong authority. Practice 5 in modeling-discipline.md is single-
authority metadata; what this prose means is **pattern 5 of Practice 4
(parameterized-family)**. Renamed to "Practice-4 parameterized-family
pattern — pattern 5" to disambiguate. No behavioral change; doc-comment
precision.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: tighten LIFTED-NESTED-SUBCKT YELLOW with crisp named trigger

PR #3168 cursor/composer-2 exploratory: the "within-parent nested
SUBCKT position" YELLOW concession at spice.dag:1054-1072 was called
YELLOW in prose but lacked a one-line "Named trigger: when ..."
consumer condition matching the Component/Directive YELLOW style.

Tightened with an explicit named trigger ("when a consumer requires
byte-exact `parse ∘ emit` round-trip of decks where a nested `.SUBCKT`
is interleaved between sibling statements of its parent body") and
enumerated three dissolution paths:
  (a) parallel ordering authority on SubcircuitDefinition (position_
      in_parent metadata)
  (b) admit SubcircuitDefinition as a SubcircuitStatement variant
      (introduces a recursive carrier — std/-substrate-tier per A1)
  (c) accept the concession permanently and emit lossless-but-not-
      byte-identical canonicalization
Explicit 🟡 emoji prefix matches sibling YELLOW carriers.

No behavioral change; doc-comment precision.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: tighten Owns round-trip contract to match nested-SUBCKT concession (codex BLOCKING)

PR #3168 codex BLOCKING (sha 543a47b8c, 2026-05-16 05:08): the Owns
contract said the ordered DeckStatement body means source-order
interleaving "round-trips through `parse ∘ emit`", but the same diff
documents (in the LIFTED NESTED `.SUBCKT` POSITION YELLOW note) that
lifted nested `.SUBCKT` definitions do NOT preserve their within-
parent position — only parent identity. That makes the header promise
materially broader than what the modeled shape actually guarantees,
which is exactly the kind of semantic overclaim the fidelity/authority
rules are trying to prevent (P1 modeling-faithfulness).

Tightened the Owns contract to scope the round-trip claim explicitly:

  Round-trip scope (PR #3168 codex review): TOP-LEVEL source-order
  interleaving of these four statement kinds round-trips through
  `parse ∘ emit`. LIFTED nested `.SUBCKT` definitions preserve their
  parent identity (via `parent_scope`) but NOT their original within-
  parent positional offset — a documented secondary fidelity
  concession tracked as 🟡 YELLOW debt with a named consumer trigger
  (see the LIFTED NESTED `.SUBCKT` POSITION YELLOW note in the
  SpiceNetlist declaration's header). The contract promised here is
  therefore "top-level interleave round-trip" + "nested-SUBCKT
  parent-identity preservation", not "byte-exact deck round-trip".

The header authority now matches what the type can actually deliver;
the YELLOW concession in the SpiceNetlist declaration body remains
the load-bearing dissolution path with its named trigger and three
fix paths.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: drop unused Diagnostic import to match sibling format-scaffold style (cursor exploratory)

PR #3168 cursor/composer-2 exploratory: this file imported
`Diagnostic` while every other mention is in comments (parse/emit
signatures conceptual-only at this layer); sibling format scaffolds
(`json.dag`, `csv.dag`, etc.) cite `Diagnostic` in prose only without
an import. The forward-looking import would become a stranded
unused-import warning if/when the v4 toolchain enforces import-must-
be-used.

Match the sibling style: dropped the `import v4.std.diagnostic
{ Diagnostic }` line. Updated the Consumes block to note explicitly
that the actual import lands when parse/emit fn bodies do (T-6/T-7),
which mirrors how json/csv/yaml/etc. handle the same dependency.

No behavioral change. `v2-compiler compile --source-root src/v4
--target dag` → 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: fix broken Symbol resolution + sync Consumes (post cursor exploratory)

The previous commit `61401f484` dropped the `Diagnostic` import per
cursor's exploratory observation (match sibling format-scaffold
style) — but doing so transitively broke `Symbol` resolution: the v2
bridge parser requires an explicit import path into std/ to bring
`Symbol` into scope, and removing the Diagnostic import severed the
only such path (Symbol is conceptually substrate-ambient per node.dag
K-1, but v2's parser does not auto-resolve it without a module link).

Fix: added `import v4.std.node { Symbol }` to bring Symbol into scope
directly. The Diagnostic citation stays in prose only (matching
sibling format scaffolds — json/csv/yaml/etc. — exactly as cursor's
exploratory note recommended); the import for Diagnostic will land
when the parse/emit fn bodies do (pipeline-stage work, T-6/T-7).

Also updated the Consumes block to reflect:
- std/node.dag is now an explicit Consumes entry (Symbol bring-in),
  with the K-1-vs-v2-bridge distinction documented (Symbol is
  conceptually substrate-ambient but the v2 parser needs the import).
- std/diagnostic.dag stays as prose-only with an explicit note that
  the actual import lands with the parse/emit bodies.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics on new HEAD.

The interim state after `61401f484` (22 errors on src/v4) was a
genuine breakage I missed by not re-running v2-compiler after the
import deletion; this commit restores green and documents the
underlying constraint so the lesson doesn't repeat.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: SubcircuitConnections non-empty at the X-element call site (codex BLOCKING)

PR #3168 codex BLOCKING (sha d7cd8539): "The non-empty carrier
discipline added for `.SUBCKT` formal ports was not mirrored at the
call-site boundary — add a non-empty `SubcircuitConnections
{ first: NodeRef, rest: List<NodeRef> }` carrier and use it for
`SubcircuitCall.terminals`."

Finding valid. SPICE3F5 §3.4's `X NAME N1 N2 ... SUBCKTNAME [PARAMS]`
form requires at least one connection node (matching the callee
subcircuit's non-empty port arity). The prior `terminals: List<
NodeRef>` admitted an empty-connection X-element value, which the
type system should reject — INVARIANTS P2.

Fix:
- New `SubcircuitConnections { first: NodeRef, rest: List<NodeRef> }`
  record — same head+tail discipline as `SubcircuitPorts` /
  `NodeVoltageBindings`. Element type is `NodeRef` (not `NamedNode`)
  because the call site CAN connect a callee port to global ground
  (`X1 in 0 out my_amp` is legal — the middle port connects to
  ground at the call site). The callee's ports themselves cannot BE
  ground; that's `SubcircuitPorts`'s `NamedNode` discipline at the
  SubcircuitDefinition side.
- `Component.SubcircuitCall.terminals: List<NodeRef>` is replaced by
  `connections: SubcircuitConnections`. (Renamed from `terminals` to
  `connections` to disambiguate from the callee's port `terminals` —
  caller side is "connections to the callee's ports", callee side is
  "port declarations".)
- Updated the SubcircuitCall per-variant-grammar HONESTY-NOTE line
  to reference the new shape.

Arity-match between caller `connections` and callee `ports` remains a
consumer-side check (it requires resolving `subcircuit: Symbol`
against the SubcircuitDefinition table to know the callee's port
count); non-emptiness is type-enforced here.

Same eventual dissolution as `SubcircuitPorts` / `NodeVoltageBindings`:
a generic `NonEmptyList<T>` in std/ would absorb all three.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 T-4.10: Component name = post-prefix portion (kind/name single-authority; codex BLOCKING)

PR #3168 codex inline BLOCKING (sha b471e9cc, spice.dag:550): "SPICE
element kind is encoded by the element-name prefix, but each Component
variant stores kind as the variant and name as an independent opaque
`identity: Symbol`, so a mismatched or prefix-erased element token is
representable unless parse/emit enforce a second authority (M3/P2)."

Finding valid. The prior `identity: Symbol` field stored the FULL
element name including the kind prefix; the variant ALSO encoded the
kind; the two were independent, so `Capacitor { identity: Symbol("R1"),
... }` was representable — a kind/name mismatch that required parse/
emit as a second authority to reject.

Fix (structural single-authority):

1. The `name: Symbol` field (renamed from `identity` for sibling
   consistency with NamedNode/SubcircuitDefinition/ModelCard/Parameter)
   now carries the POST-PREFIX portion of the SPICE3 instance name.
   The kind prefix is IMPLICIT in the variant.

   `R1`        ⇒ `Resistor { name = Symbol("1"), ... }`
   `R_LOAD`    ⇒ `Resistor { name = Symbol("_LOAD"), ... }`
   `M3_high`   ⇒ `Mosfet { name = Symbol("3_high"), ... }`
   `X1`        ⇒ `SubcircuitCall { name = Symbol("1"), ... }`

2. Emit prepends the variant's kind letter; parse strips it. ZERO
   secondary authority needed; the variant IS the kind, the `name`
   field IS the post-prefix suffix, and the two cannot contradict
   because the prefix is no longer in `name` at all.

3. Added a "NAME / KIND SINGLE-AUTHORITY" section to the Component
   modeling note documenting the discipline + examples.

The `Symbol` payload remains K-1-opaque; the kernel never observes
the suffix's spelling. The mismatch failure mode the reviewer
surfaced is now structurally unrepresentable rather than convention-
enforced (M3 modeling-faithfulness / P2 illegal-states-unrepresentable
satisfied at the type layer).

Sibling renames: every Component variant's first field is now `name:
Symbol` (was `identity: Symbol`) — matches the `name` convention
already used across NamedNode/SubcircuitDefinition/ModelCard/Parameter.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* WIP: T-4.10 spice

* v4 T-4.10: NamedNode honesty + typed Modifier sum for instance-modifiers (codex BLOCKING ×2)

PR #3168 codex BLOCKING (sha 9a477536, 242s): two substrate-level
representation holes:

1. "Non-ground node identity is modeled as a nominal wrapper over
   opaque Symbol — make the non-ground lexical carrier/refinement
   itself exclude the ground token, or keep `0` rejection as an
   explicit unresolved scaffold instead of claiming structural
   enforcement."

2. "Instance modifiers are forced through the name/value Parameter
   carrier — split modifiers into a typed `Flag | KeyValue` shape
   now, or stop claiming `OFF=` is an equivalent SPICE spelling."

Both findings valid (earlier overclaims).

Fix 1: HONEST framing of NamedNode's true guarantee:

- `NamedNode` STRUCTURALLY excludes the `NodeRef.Ground` VARIANT
  (a `NamedNode` value is, by type, not the Ground variant).
- `NamedNode` DOES NOT, at the type layer, exclude a Symbol whose
  parser-translation is the SPICE3-ground literal "0" — Symbol
  content is K-1 opaque; that's PARSER DISCIPLINE (the parser maps
  "0" to `NodeRef.Ground`, never through `NodeRef.Named`).
- Documented this distinction with a YELLOW debt note: dissolves
  when std/ provides a Symbol refinement substrate (NonZeroSymbol
  or similar). That's std/-substrate-tier, not in T-4.10's scope.
- Updated NamedNode declaration prose + SubcircuitDefinition
  "NO GROUND VARIANT" sub-note to be precise about variant-vs-token
  exclusion.

Fix 2: New typed `Modifier` sum for instance modifiers:

    type Modifier
      = Flag { name: Symbol }
      | KeyValue { name: Symbol, value: SpiceValue }

- `Component.Mosfet.parameters: List<Parameter>` → `modifiers: List<
  Modifier>`
- `Component.Bjt.parameters: List<Parameter>` → `modifiers: List<
  Modifier>`
- `Parameter` retained for contexts that admit ONLY name=value: .MODEL
  cards, .OPTIONS directive, HSPICE-extension X-element params
  (`SubcircuitCall.parameters: List<Parameter>` unchanged).
- Bare-flag `OFF` is now `Flag { name = OFF }`; parameter `AREA=2` is
  `KeyValue { name = AREA, value = ... }`. The two surface forms are
  STRUCTURALLY DISTINCT — no conflation, no "equivalent SPICE3
  spellings" overclaim.
- Full 5-pattern Practice-4 🟢 GREEN ledger added for `Modifier`.

Header `Owns:` round-trip-scope updated: the prior "instance-modifier
semantic-equivalent round-trip (modulo bare-flag vs name= form)"
framing is RETRACTED. The contract is now "instance-modifier
byte-exact round-trip (Flag vs KeyValue distinguished structurally)".

Updated all prose references: Parameter declaration's role narrowed to
the name=value-only contexts; Bjt/Mosfet HONESTY-NOTE entries updated
to reference `modifiers: List<Modifier>` not `parameters: List<
Parameter>`; the prior FLAG-FORM INSTANCE MODIFIERS workaround note
on Parameter is deleted (the workaround is no longer needed — the
typed sum makes it unnecessary).

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: .OPTIONS uses Modifier sum (admits bare flags + name=value; openai-pro BLOCKING)

PR #3168 openai-pro REQUEST_CHANGES on sha d84d5ef5: ".OPTIONS
currently cannot represent legal bare option tokens, and the gap is
incorrectly outside the YELLOW debt list."

Finding valid + spec-anchored (ngspice §Simulator Variables shows
both `.OPTIONS ACCT NOPAGE` bare-flag and `.OPTIONS METHOD=GEAR
ABSTOL=1e-12` key-value forms; SPICE3F5 admits both in the same
card). The prior `Options { parameters: List<Parameter> }` excluded
bare options because `Parameter` is name=value-only.

Fix:
- `Directive.Options.parameters: List<Parameter>` →
  `modifiers: List<Modifier>`. Same `Modifier = Flag | KeyValue`
  carrier already used for `Mosfet`/`Bjt` instance modifiers; bare
  options are `Flag`, name=value options are `KeyValue`. Bare-option
  cards are now representable, and the flag-vs-key-value distinction
  is byte-exact preserved through parse∘emit.
- Updated the Directive HONESTY-NOTE per-variant entry for `.OPTIONS`
  — now classified ADDRESSED (not "complete-for-mandatory-grammar")
  with the bare-flag + key-value mixed grammar documented and the
  ngspice anchor cited. The `Ac` / `Op` / `Include` entries remain
  complete-for-mandatory-grammar.
- Updated `Parameter`'s doc-block: dropped the stale `.OPTIONS`
  reference (which used to claim Parameter; now `.OPTIONS` is
  Modifier). Parameter is now scoped to .MODEL parameter sets +
  HSPICE-extension X-element params — the genuine name=value-only
  contexts.

The YELLOW debt for .OPTIONS is closed by this commit; the typed sum
makes the failure mode unrepresentable. The completeness claim is
now spec-faithful.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: typed cross-element refs — SweepSourceRef, InductorRef (codex BLOCKING)

PR #3168 codex inline BLOCKING (spice.dag:960): "After `Component.name`
strips the element prefix, `.DC source: Symbol` cannot preserve
whether a swept source was `V1` or `I1`, so valid SPICE source
references can alias and violate P1/P2 single-authority."

Finding valid + surfaces a structural tension introduced by the
earlier kind/name single-authority commit (post-prefix Component.name).
Cross-element references that previously carried the FULL element
name (prefix + suffix) now lose the kind disambiguation when typed
as bare `Symbol`. Two sites affected:
  - `Directive.Dc.source: Symbol` — V1 and I1 both reduce to
    Symbol("1") post-stripping; the V-vs-I sweep distinction
    aliases. (The reviewer's flagged site.)
  - `Component.MutualInductance.l1: Symbol` / `l2: Symbol` —
    references to inductor elements; same prefix-loss concern.
    Same fix shape, applied for consistency.

Fix: typed cross-element reference carriers at each site:

  type SweepSourceRef
    = VoltageSweepSource { name: Symbol }
    | CurrentSweepSource { name: Symbol }

  type InductorRef {
    name: Symbol
  }

  Directive.Dc.source: SweepSourceRef
  Component.MutualInductance.l1: InductorRef
  Component.MutualInductance.l2: InductorRef

Kind is carried structurally at the reference site (matching the
target Component variant); suffix matches the corresponding
`Component.{variant}.name`. The reference type constrains which
Component variants can satisfy it, so cross-kind aliasing is
structurally unrepresentable — INVARIANTS P1/P2 single-authority
restored at reference sites.

Full 5-pattern Practice-4 🟢 GREEN ledger added for `SweepSourceRef`.
`InductorRef` is a single-variant record (SPICE3 `K` references only
inductors) — modeling note explains why a typed sum would add no
information.

A generic `ComponentRef` typed-sum mirroring every Component variant
was considered and rejected — it would parallel-represent the
Component variant set (Practice-7 parameterized-family smell); the
narrowly-typed reference carriers at each site are the worker-tier
scaffold. A `ComponentRef` generalization is the std/-substrate-tier
dissolution path.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* WIP: T-4.10 spice

* v4 T-4.10: add B (non-linear dependent source) to Component 🟡 trigger missing-list

PR #3168 openai-pro REQUEST_CHANGES on sha e85920c2: "the `Component`
YELLOW scaffold is missing a real SPICE3 element (`B` non-linear
dependent source) from its bounds. Because the file's own trigger
relies on that missing-list to decide when the scaffold can become
green, this should be fixed before landing."

Finding valid + spec-anchored. SPICE3 `B` element (per the archived
SPICE 3 manual / ngspice carry-forward) is the non-linear dependent
source: `BXXXXXXX N+ N- <I=EXPR> <V=EXPR>`. It is a real SPICE3
element kind and the prior missing-list (E, F, G, H, J, O, S, T, U,
W, Z) omitted it — exactly the false-fire-green failure mode the
synchronization-discipline note warns about.

Fix: added `B (non-linear dependent source — SPICE3 `B N+ N- <I=expr>
<V=expr>`)` to the missing-list at three textual sites:
1. Component HONESTY NOTE element-kind list (line 664-678)
2. Component 🟡 trigger reclassification condition (line 727-728)
3. Parameter doc-block cross-reference (line 409-410)

Per the synchronization discipline established for the prior Z/O/U
addition: the missing-list must stay synchronized with the SPICE3F5
anchor's element table. The discipline-note now cites the openai-pro
B omission as a precedent for the same failure mode.

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-4.10 spice

* v4 T-4.10: flip AcSweepKind 🟢 → 🟡 per PR #3200 rule change (comment-only)

PR #3200 (merged 2026-05-16 19:53:37Z) ratified the operator-directed
modeling-discipline rule change: GREEN is consumer-INDEPENDENT — a
coproduct is GREEN ONLY IF no richer source exists. "No consumer needs
it yet" ≠ GREEN.

merry-ibex-337-led authoritative cross-PR Tier-1 audit identified
AcSweepKind as mis-GREEN: the three variants project over a namable
2D axis `(spacing-law × ratio-base)`:
  - Linear ⇒ spacing-law = arithmetic;  ratio-base = NA
  - Decade ⇒ spacing-law = logarithmic; ratio-base = base-10
  - Octave ⇒ spacing-law = logarithmic; ratio-base = base-2

Comment-only flip (no carrier/code/import/diag change):
- Classification 🟢 GREEN → 🟡 YELLOW (deferred-on-consumer)
- Added rule-change attribution (PR #3200) + axes
- Pattern-4 and Pattern-5 ledger entries updated:
  - Pattern 4: FAILS-AT-THIS-LAYER, but the 2D axis is the richer
    source the YELLOW dissolution targets at the meaning-consumer
  - Pattern 5: SUCCEEDS at the meaning-consumer per #3200's
    parameterized-family pattern; stays coproduct at this file's
    surface because the decomposition is the consumer's obligation
- Named trigger: first consumer of frequency-stepping semantics —
  the AC-analysis sweep-point generator (walks fstart → fstop
  emitting per-step frequencies for `.AC` simulation)
- Pre-assigned obligation: that consumer DERIVES the step law from
  the (spacing-law, ratio-base) axes — NOT a match over the
  {Linear | Decade | Octave} coproduct labels. A typed (spacing-law,
  ratio-base) carrier (or equivalent decomposition) is the
  structural form the consumer owes

This is part of the cross-PR-uniform Tier-1 audit dispatched by
merry-ibex-337 following #3200's merge. SubcircuitStatement and
DeckStatement stay-GREEN (authoritative audit confirmed-clean as
spec's-own-irreducible-partitions).

Verified: `v2-compiler compile --source-root src/v4 --target dag` →
0 diagnostics. No structural change; ledger-prose only.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4 #3174: reshape OverflowDisposition to 2-variant nullary Disj
c9ba92d 
Per BLOCKING reviewer 2026-05-16T20:33:06Z @ rust.dag:1799:

  "OverflowDisposition makes Rust's required debug-assertion overflow
   action a variable OverflowAction, so TwoComplementWrap remains
   constructible for a fact the Rust Reference fixes to panic,
   violating INVARIANTS P2/extdeps fidelity."

Verified: the prior shape OverflowDisposition<IRCarrier> {
debug_assert_required_action: OverflowAction } let any OverflowAction
value sit in that field, including TwoComplementWrap — but the
Rust Reference (behavior-not-considered-unsafe.html#integer-overflow)
fixes that fact: "implementations MUST insert dynamic checks that
panic on overflow." Variable field type = illegal-state-constructible
= INVARIANTS P2 illegal-states-unrepresentable violation.

Fix: reshape OverflowDisposition to a closed two-variant Disj with
nullary variants, structurally pinning both Reference facts:

  type OverflowDisposition<IRCarrier>
    = MustPanicOnOverflow
    | MayPanicOrTwoComplementWrap

  - MustPanicOnOverflow: the deterministic Reference fact for debug_assert
    builds. Nullary variant — no payload can carry an alternative action.
  - MayPanicOrTwoComplementWrap: the Reference fact for other builds
    (impl-defined choice between the permitted actions, commonly driven
    by -C overflow-checks). Wrap convention (two's-complement per
    Reference) structurally encoded in variant name; no ArbitraryWrap
    sibling exists.

This matches openai-pro's earlier REQUEST_CHANGES suggested faithful
shape ("a disposition such as MustPanic | MayPanicOrWrap { wrap_convention:
TwoComplement }") with the wrap-convention encoded in variant naming
rather than as a payload.

Practice-4 ledger updated: 5 patterns FAIL (closed two-element Reference-
defined per-build-mode classification; nullary variants are the faithful
form per pattern-2; the action-as-payload form is exactly what the
BLOCKING rejected). Terminal 🟢 GREEN under #3200 (Bool-shaped on the
debug_assert-enabled axis; no namable richer std/ source).

Deferred-instructions block for per-integer rust_<x>_overflow rows
updated: two D2a(3) data rows per integer type capturing the per-build-
mode dispositions; both are TOP-LEVEL SUM-VARIANT bodies (= MustPanicOnOverflow
etc.) → DOUBLE-deferred under (a) std/integer.dag ladder + (b)
Class-5-Gap-3 (top-level ValueBody::Unparsed) per ROADMAP.md:418.
Type shape canonical regardless of instance-row landing.

Owns: D2-resolver-shape bullet updated.

v2-compiler: 0 diagnostics (full lower-and-emit, 68 files).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4 #3200 reclass: llvm_ir.dag (7) + go.dag (4) widths 🟢→🟡 (commen…
ee9a051 
…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>
@briansrls briansrls mentioned this pull request May 16, 2026
Closed
2 tasks
briansrls added a commit that referenced this pull request May 16, 2026
@briansrls @claude
v4 T-4 #3200 reclass: add ledger-header flip + rust.dag widths
83afba8 
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 added a commit that referenced this pull request May 17, 2026
@briansrls
WIP: v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-u…
9531d4e 
…rgency d
briansrls added a commit that referenced this pull request May 17, 2026
@briansrls @claude
v4 T-4 #3215 fix: BLOCKING — rewrite ConversionOpcode/AtomicRmwOp/Bin…
69392ed 
…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 added a commit that referenced this pull request May 17, 2026
@briansrls
WIP: v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-u…
18d0b80 
…rgency d
briansrls added a commit that referenced this pull request May 17, 2026
@briansrls @claude
v4 T-4 #3215 precision: tighten landed-witness inventory to FIVE (was…
8db67bd 
… 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>
briansrls added a commit that referenced this pull request May 17, 2026
@briansrls @claude
v4 T-4 #3215 fix: BLOCKING — ConversionOpcode std/ptr.dag phantom-aut…
0f89536 
…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>
briansrls added a commit that referenced this pull request May 17, 2026
@briansrls @cursoragent
fix(scripts): canonicalize Verilog coproduct tags vs DECISIONS (#3229)
3d59bb7 
`inject_coproduct_tags` now replaces any shaped coproduct line whose slug
differs from the merge-base manifest so stale pointers cannot satisfy
`--check`. `verilog_yellow_ref` treats `#3200` markers after `// Terminal:`
as D3200 carriers. Regenerated allowlisted `.dag` files; add
`scripts/test_strict_deprose_dag.py` for the stale-slug case.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls briansrls mentioned this pull request May 17, 2026
Merged
briansrls added a commit that referenced this pull request May 17, 2026
@briansrls @cursoragent
D2-impact de-prose: verilog/llvm_ir/ptx + std integer/float — terse h…
75f98aa 
…eaders, archive, strict_deprose_dag.py (#3229)

* WIP: D2-impact non-per-language rework — strip D2-reversed-model prose from f

* fix: finish D2-prose strip in llvm_ir/ptx .dag comments

Reword PTX RegisterScalar seam to scalar-inhabitance framing; restore
llvm_ir comment line wrap after prior edit.

Co-authored-by: Cursor <cursoragent@cursor.com>

* chore: reflow llvm_ir.dag ledger comments (review nit)

Join split mid-sentence lines in LlvmConstant and BinaryOpcode Practice-4
ledgers so phrases are not orphaned across comment boundaries.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: D2-impact non-per-language rework — strip D2-reversed-model prose from f

* WIP: D2-impact non-per-language rework — strip D2-reversed-model prose from f

* WIP: D2-impact non-per-language rework — strip D2-reversed-model prose from f

* fix: include `data` carriers in strict-deprose Owns list

Owns must name substrate carriers; integer/float add Tier-2 Symbol rows.
Re-run scripts/strict_deprose_dag.py — comment% still <20% (integer 14.7%, float 6.2%).

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: D2-impact non-per-language rework — strip D2-reversed-model prose from f

* docs: drop de-prose process meta from v4-dag-rationale

Per operator feedback: keep architectural relocated commentary; remove
strip/receipt narration and line-number census from headings.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(ptx): cite PTX ISA 8.5 PDF as primary spec anchor

extdeps fidelity invariant (dsl/extdeps/extdeps.md): header must link the
upstream specification; add normative PDF URL with HTML TOC on same line.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs: mark v4-dag-rationale non-authoritative; purge stale D2 archive

Codex blocking: doc must not conflate relocated commentary with canonical
authority. Replace intro with explicit non-authoritative banner; replace
integer/float fenced blocks with neutral archive summaries (no D2 tokens).

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(scripts): correct strict_deprose_dag specs tuple arity in type hint

Composer exploratory: each spec row is (rel, scope, anchor, consumes, status)
— five strings, not four.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(scripts): warn strict_deprose_dag strips all post-module body comments

Claude-opus non-blocking: script is a sharp edge for any future in-body `//`
authorship; document that in the module docstring.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(v4): drop deleted std/primitive.dag from verilog/llvm Consumes headers

Composer REQUEST_CHANGES / INVARIANTS P1: `std/primitive.dag` was removed
(PR #3152); substrate headers must not cite missing paths. Align Consumes
with the sole live import (`v4.std.node` / std/node.dag) and sync the
strict_deprose_dag allowlist so regeneration cannot reintroduce the stale
names.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(v4): align verilog/llvm Consumes with PTX Int kernel-ambient wording

Composer optional: LLVM IR (and Verilog) use ambient Int like PTX while only
importing Symbol from std/node; spell that in // Consumes so headers match
across the three extdeps language carriers.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(v4): point verilog.dag Anchor at IEEE 1364-2005 catalog, not wrong Xplore id

9576818 is not IEEE 1364-2005; extdeps fidelity expects the standards.ieee.org
upstream anchor for the cited revision.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(v4): relocate Practice-4 ledgers + scaffolds to DECISIONS Part 6 (#3229)

Operator directive: authoritative coproduct classifications and tracked-
scaffold records (with dissolution triggers) removed by strict de-prose
must live in DECISIONS.md, not the non-authoritative archive.

- Append Part 6 with verbatim SL-3229-* scaffold blocks (merge-base
  92cb264) for llvm_ir (width + ops), ptx Dim3, verilog non-empty list
  deferral, float nominal-width notes; CP-3229-GREEN-TERMINAL inventory +
  git recovery commands; CP-3229-VERIFY integer.dag (no Practice-4 blocks).
- strict_deprose_dag.py: emit `// Ledger: DECISIONS.md Part 6 (PR #3229).`
  in regenerated headers; re-run on allowlist.
- docs/v4-dag-rationale.md: point Practice-4 authority at DECISIONS Part 6.

Supersedes prior PR #3229 thread rebuttal — openai-pro REQUEST_CHANGES
addressed in-tree.

Co-authored-by: Cursor <cursoragent@cursor.com>

* feat(v4): coproduct 🟢/🟡/🔴 one-liners + DECISIONS Part 6 cite (#3229)

Operator directive: each N>=2 sum coproduct in the five allowlisted v4
.dag files carries a single Practice-4 emoji line on the type, citing
DECISIONS.md Part 6 (SL-3229-* / CP-3229-GREEN-TERMINAL); merge-base
92cb264 drives 🟢 vs 🟡 (llvm LlvmType -> SL-3229-LLVM-WIDTH; verilog
🟡 YELLOW families -> SL-3229-VERILOG-NONEMPTY). strict_deprose_dag.py
preserves those tags through the body strip; compresses // Owns to one
comma-separated line to keep comment% <20%. DECISIONS Part 6 intro notes
PR #3234 alignment.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(v4): Part 6 VerilogCost/PTX cost rows + red coproduct slug (#3229)

Practice 9: relocate merge-base VerilogCost and PtxCost Int-axis scaffold
receipts into DECISIONS Part 6; add missing verilog D3200 / VectorRange
rows so strict_deprose inventory matches authority. Map 🔴 coproducts to
CP-3229-RED-PRACTICE4 instead of CP-3229-GREEN-TERMINAL. Regenerate allowlist
headers via strict_deprose_dag.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(scripts): Owns manifest includes fn + strict_deprose --check (#3229)

Restore complete top-level symbol inventory (type, data, fn) for
regenerated .dag headers; document the contract in the script docstring.
Add `--check` to fail on drift without rewriting. Regenerate allowlisted
substrates (llvm_ir gains helper fn names in Owns).

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(scripts): canonicalize Verilog coproduct tags vs DECISIONS (#3229)

`inject_coproduct_tags` now replaces any shaped coproduct line whose slug
differs from the merge-base manifest so stale pointers cannot satisfy
`--check`. `verilog_yellow_ref` treats `#3200` markers after `// Terminal:`
as D3200 carriers. Regenerated allowlisted `.dag` files; add
`scripts/test_strict_deprose_dag.py` for the stale-slug case.

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(scripts): live-derived Ledger + fail-closed unknown coproducts (#3229)

Build `// Ledger:` from current sum types in each allowlisted file (Part-6
refs from the merge-base tag map) plus `EXTRA_PART6_SLUGS_BY_REL` scaffolds;
restore `SL-3229-VERILOG-NONEMPTY` on the Verilog inventory. `inject_coproduct_tags`
and `required_ledger_slugs` exit non-zero if a live coproduct is absent from the
pinned merge-base manifest. Tests stay in-process (no `git show`); note merge-base
object availability beside `MERGE_BASE`.

Co-authored-by: Cursor <cursoragent@cursor.com>

* ci: run strict_deprose_dag self-test and --check on every PR

Wire the v4 de-prose ratchet into the main `ci` job (full-history checkout
already satisfies `git show` for the pinned merge-base). Addresses review
feedback to catch stale coproduct slugs / Ledger drift before the allowlist grows.

Co-authored-by: Cursor <cursoragent@cursor.com>

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls briansrls mentioned this pull request May 18, 2026
Closed
6 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@briansrls