diff --git a/src/v4/extdeps/languages/verilog.dag b/src/v4/extdeps/languages/verilog.dag index 9ebf5f7720d..94f064907b5 100644 --- a/src/v4/extdeps/languages/verilog.dag +++ b/src/v4/extdeps/languages/verilog.dag @@ -29,9 +29,4418 @@ // - std/node.dag, std/algebra.dag, std/primitive.dag // - extdeps/coordination.dag (concurrency via effect-typed Bind — IN-B) // -// Status: scaffold — fill per TASKS.md T-4.9 -// Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable -// contract for the worker. Splitting this file requires explicit operator -// ratification (substrate extension = stop signal). +// Status: T-4.9 modeled 2026-05-16 (bright-crane-527). IN-B probe RESULT: +// PASS — Verilog hardware concurrency models cleanly under the existing +// five L1 behaviors with NO 6th `Concurrent` behavior and NO core/ +// pipeline change (see modeling notes "IN-B PROBE FINDING"). The probe +// surfaces the structurally-correct intra-vs-cross-program partition: +// hardware concurrency (parallel `always`-blocks / continuous assigns +// within ONE module) is the Conj-of-parallel-siblings + Bind-chain +// shape, with per-language effect-typing intrinsic to the wire/reg/ +// vector signal type — exactly the THESIS:401 IN-B disposition. +// The scaffold-header `Consumes` line is preserved verbatim and carries +// two known stale citations: (1) `std/primitive.dag` was deleted by +// PR #3152 (STRUCTURE.md §"Scalar/numeric concept decomposition"); the +// six concept-anchored scalar files are the replacement, and `Symbol` +// is now substrate-ambient at std/node.dag (K-1). (2) `extdeps/ +// coordination.dag` is an unfilled scaffold (T-4.8) and its modeled +// scope is CROSS-PROGRAM coordination (Endpoint / DeploymentUnit / +// sync-async-stream-pubsub semantics, v4-close-interrogation.md §16) — +// a different concern from intra-program hardware concurrency, which +// this file demonstrates needs no cross-program coordination carrier +// at all. Both stale citations are surfaced, not edited: the contract +// lines are immutable, and the per-file Consumes correction is +// pending the systemic operator scaffold-Consumes reconciliation +// (T-4 mgr synthesis msg_1fddb75c) — uniform with ptx #3170, spice +// #3168, and llvm_ir #3171. The body's `import` reflects what this +// file actually uses. Splitting this file requires explicit operator +// ratification (substrate extension = stop signal). + module v4.extdeps.languages.verilog + + +// std/node.dag is imported: it makes the K-1 opaque `Symbol` (the +// name-reference identity used pervasively in the Verilog grammar — +// module names, port names, signal names, instance names) resolvable +// through this file's import closure. std/algebra.dag is NOT imported: +// this file's scaffold-declared `Inhabitance: bit-vectors per +// std/algebra.dag` is DEFERRED to the operator-pending D2 STOP (see the +// Inhabitance section in modeling notes); declaring per-target +// OrderedRing/Semiring instance-values now would be the per-file +// `` improvisation D2 forbids (#3171 worker +// vivid-crab-154 / snappy-badger-570 held precedent). std/diagnostic.dag +// is NOT imported: this declarative LanguageModel declares no +// parse/emit body — those ride the operator-pending D1 Outcome +// carrier (`Produced{value:T} | Rejected{diagnostic:Diagnostic}`) when +// ratified in std/diagnostic.dag; improvising a per-file Result shape +// now is exactly the v4 value-or-Diagnostic STOP first surfaced by +// T-4.6 (keen-wren-419). `Int`, `Bool`, `String`, `List` are +// kernel-ambient per STRUCTURE.md §"Kernel-ambient types" — no import. +import v4.std.node { Symbol } + + +// ───────────────────────────────────────────────────────────────────── +// Modeling notes (read before validating against the anchor) +// +// SPEC, NOT LIBRARY (M3 / L-2). The anchor is IEEE 1364-2005 — the +// language specification. The set of synthesizable subsets used by any +// particular tool (Xilinx XST, Synopsys Design Compiler, Yosys), the +// vendor-specific timing libraries, and the simulation-only constructs +// (`$display`, `$monitor`, file I/O system tasks) are NOT modeled: an +// invocation of `$display` is just a system-task call (a Symbol-named +// call site); modeling the system-task universe is infinite and the +// wrong layer. SystemVerilog (IEEE 1800) extensions (interfaces, +// always_comb / always_ff / always_latch sugar, packed structs, classes) +// are scope-negative for this file — they are a later language model. +// The 1364-2005 surface is the closed L-2 fidelity authority. +// +// DECLARATIVE MODEL, NOT A RECOGNIZER (T-4 authoring contract). This +// file is the grammar/type/semantics-skeleton as DATA. It declares no +// `parse`/`emit` procedure: those are the GENERIC walker (compiler +// 01_tokenize / 02_parse / 05_emit, B2-OMNI) reading this model. The +// expression sub-grammar (operators, function calls, concatenation, +// system functions) is owned by the bidirectional `LanguageModel` +// substrate that the T-4 bundle introduces — when that shape lands, +// the Verilog statement/expression productions slot into the Verilog +// `LanguageModel` instance; the closed classifiers + Conj records +// declared here are the irreducible structural carrier that does not +// prejudge that shape. Lexical-surface bodies of always-blocks, +// continuous-assign right-hand sides, and control-flow conditions are +// carried as verbatim `String` lexemes at this phase (the spice.dag +// `SpiceValue.lexeme` precedent — `parse ∘ emit` is identity on the +// textual surface; the sub-grammar interprets the lexeme when the +// expression model lands). +// +// IN-B PROBE FINDING (the deliverable — the STOP discipline is the +// product). Verilog HW concurrency models as a plain `LanguageModel` +// over the closed 5 L1 behaviors with NO 6th `Concurrent` / `Parallel` +// behavior and NO core/pipeline change. The probe's stress axis — the +// concurrent semantics of `always` / continuous-assign / module +// instantiation — resolves into ORDINARY Node structure, surfacing +// the right intra-vs-cross-program partition along the way. The +// mapping, member-by-member: +// +// - MODULE BODY ↦ Conj of parallel siblings. +// A Verilog `module` body is a flat list of items +// (`ModuleItem` — continuous-assigns, always-blocks, instances, +// declarations). Concurrent execution across those siblings is +// STRUCTURAL: each item is a child of the module-body Conj, and +// concurrent semantics is the SAME shape as a Conj of submodule +// instantiations (which every C / Rust / Python module already +// models as Conj children). The simulator/synthesizer schedule +// (event-driven evaluation) is the mechanical realization of the +// dependency graph (THESIS:18 "parallelism is the default — +// independence is visible in the structure"); it is NOT a +// separate behavior. Tempting alternative: a `Concurrent` behavior +// wrapping each module item. REJECTED — it would parallel- +// represent what the Conj's children already say +// (feedback_no_annotations: a property structurally visible is +// never duplicated as a marker). This is precisely the IN-B win. +// +// - CONTINUOUS ASSIGN (`assign net = expr;`) ↦ Transform. +// A continuous assignment is a function from the right-hand-side +// expression's input signals to the left-hand-side net — exactly +// the Transform behavior (function application, node.dag:209 +// "Transform=application"). The "continuous" aspect — re-evaluate +// whenever an input changes — is the SCHEDULE of the surrounding +// dataflow graph, not a property of the Transform itself. +// +// - ALWAYS BLOCK ↦ Loop (one step) + boundary-driven iteration. +// Per node.dag A2 footnote (genuine unboundedness — "servers / +// streams / REPLs is a TERMINATING step iterated by the +// coordination-boundary driver — never an unbounded `.dag` loop"), +// each `always @(...)` block's ONE TRIGGER is a BOUNDED step +// (one event-fire: read inputs, sequence the statements, write +// outputs). The eternal-iteration ("forever, every clock edge") +// lives at the simulator/synthesizer's coordination boundary; the +// `.dag` model carries the BOUNDED step, not the unbounded +// iteration. The trigger-event-list (`SensitivityItem`s) is the +// bound that gates the next iteration. Tempting alternative: an +// unbounded `Eternal` / `Concurrent` behavior. REJECTED — the A2 +// bounded-Loop discipline is the existing surface for this exact +// pattern. +// +// - PROCEDURAL STATEMENT SEQUENCE (within `begin ... end`) ↦ Bind. +// The statements inside an always-block (or initial-block) form +// a sequential composition — exactly the Bind behavior +// (node.dag:209 "Bind=let"). Blocking (`=`) vs non-blocking +// (`<=`) assignment is a SCHEDULING discriminator on the Bind's +// write semantics (blocking commits before the next statement; +// non-blocking schedules the write for the end of the time-step), +// not a new behavior. The `ProceduralAssignKind` enum below +// carries that discriminator as data on the assignment statement. +// +// - IF / CASE ↦ Branch. +// Verilog `if ... else` and `case ... endcase` are guarded sums +// over a discriminator — exactly the Branch behavior +// (node.dag:209 "Branch=sums"). The case-item ordering and the +// full-case / parallel-case synthesis directives are emission- +// time properties (the synthesizer's concern); the structural +// surface is the Branch. +// +// - SIGNAL DECLARATION (Wire / Reg / Vector) ↦ effect-typed value. +// A Verilog `wire`, `reg`, or `wire [7:0]` is a TYPED signal +// carrier; the type IS the effect-typing locus per the +// v4-close-interrogation §16 IN-B disposition ("effects intrinsic +// to the type signature, NOT an annotation layer"). A continuous- +// assign Transform's domain/codomain types name Wire/Reg with +// packing, and the typing is what constrains valid composition +// (a `reg`-typed driver can drive an `output reg` port; a +// procedural assignment is only legal to a `reg`-typed +// destination; etc.). This file's `NetDeclaration` / +// `VariableDeclaration` / `PortDeclaration` records are the +// effect-typed carriers; there is no separate Verilog-effect- +// annotation layer. +// +// - MODULE INSTANCE ↦ structural Conj child. +// `ModuleName instance_name (.port(signal), ...);` is a child +// Node in the parent module-body Conj — the same shape as a +// submodule reference in any other LanguageModel. Concurrent +// execution of the instance alongside its sibling items is the +// same Conj-of-parallel-siblings shape as multiple always-blocks +// (above); no new behavior. +// +// INTRA-PROGRAM vs CROSS-PROGRAM EFFECT-TYPING (the partition the +// probe surfaces). The scaffold-header `Consumes` line citing +// `extdeps/coordination.dag` for "concurrency via effect-typed Bind +// — IN-B" was a SCAFFOLD-AUTHOR ANTICIPATION that lumped all +// concurrency under one carrier. The probe surfaces the structurally +// correct partition: (a) INTRA-program concurrency (multiple +// `always`-blocks within one Verilog module sharing signal nets) is +// what this file models — the effect-typing carriers are the +// signal-type declarations (`NetType` / `VariableDeclaration` variants / +// `PackingShape`) +// declared HERE, in this language file; (b) CROSS-program coordination +// (one program's output deployed to host A, another to host B, +// communicating via Endpoint / DeploymentUnit / sync-async-stream- +// pubsub) is what `extdeps/coordination.dag` (T-4.8) models — a +// distinct concern with a distinct anchor (Wikipedia Distributed +// computing + Messaging pattern). The IN-B principle "effect-typed +// Bind composition, no 6th behavior" holds in BOTH partitions, with +// the effect-typing carriers in their respective per-language / +// per-coordination home files (P2 single-authority). This is the +// per-language effect-typing finding the probe was authored to +// surface — and it surfaces here on the SUCCESS side, not the STOP +// side. +// +// INHABITANCE (DEFERRED to D2). The scaffold-declared "Inhabitance: +// bit-vectors (wire/reg [N:0]) per std/algebra.dag" is DEFERRED to +// the operator-pending D2 STOP. Conceptually, an N-bit unsigned +// signal grounds in `Semiring>` (or `OrderedRing>` +// for signed-as-twos-complement reg/integer arithmetic) — but +// declaring a `data verilog_wire_n_semiring: Semiring> = …` +// instance-value at this layer would be the per-file +// `` improvisation D2 was authored to hold +// (PR #3171's hold precedent). The instance-value form lands when +// std/integer.dag / std/logic.dag inhabitance walks land plus the +// ratified D2 instance-value shape; the algebra import + the +// instance-value declarations are added in ONE pass, not improvised +// per language. +// +// PROBE LIMITS (honest framing — what this file does NOT validate). +// The IN-B finding covers the STRUCTURAL fit of Verilog HW concurrency +// to the 5 L1 behaviors. It does NOT validate: +// - that a synthesizer actually produces gates from `emit`'s output +// (the "clear win" in the header — that requires invoking a +// synthesizer process, an `extdeps/process.dag` consumer +// boundary, not modeled here). +// - the expression sub-grammar of `assign net = expr;` right-hand +// sides and procedural statement bodies (verbatim lexemes at +// this phase; the T-4 LanguageModel bundle owns the recursive +// expression productions when it lands). +// - SystemVerilog (IEEE 1800) extensions (`always_comb` / +// `always_ff` / `always_latch` sugar, interfaces, classes, +// packed structs) — a later language-version model edits this +// file (under the L-2 pin discipline) when it lands. +// - Simulator-only / testbench constructs (`initial` with +// `$display`, `$finish`, file I/O system tasks, `force` / +// `release`, fork-join, `wait`) — `initial` is admitted as a +// `ModuleItem` variant for the once-only-driven case; the +// `$task` universe is the system-task call site, not the +// concurrency primitive. +// - Timing-checks (`$setup`, `$hold`, `specify` blocks) — a +// separate timing-annotation layer (SDF — Standard Delay +// Format), out of scope for this language model. +// +// PRACTICE-4 LEDGER DISCIPLINE. Every closed-Disj coproduct below +// carries the full 🟢/🟡/🔴 classification + all FIVE patterns +// attempted (Fact-placement / Variant-is-data / Algebraic-form / +// Dimensional / Parameterized-family-Practice-7) per modeling- +// discipline.md §4 (operator-ratified binding 2026-05-15, gate (b); +// PR #3163 made the 4-pattern miss the proof case — do not omit +// Practice-7). Conj records carry no ledger (only coproducts +// dissolve); scaffold-residual fields (VectorRange's lexeme-pair +// bridge to the constant_expression sub-grammar, VerilogCost's +// raw-Int axes) carry a 🟡 bridge note mirroring the std/ +// diagnostic.dag / ptx Dim3 precedent. + + +// ───────────────────────────────────────────────────────────────────── +// PortDirection — the closed Verilog port-direction classifier +// (IEEE 1364-2005 §12.3.2). A module's port is exactly one of three +// directions. +// +// - Input — `input` driven by the instantiating context, read +// inside this module +// - Output — `output` driven inside this module, read by the +// instantiating context +// - Inout — `inout` bidirectional (tri-state nets only) +// +// CLOSED (C1 stop-signal). A fourth direction is an edit to THIS +// declaration under the L-2 pin discipline (IEEE 1364-2005 has fixed +// three directions; SystemVerilog adds `ref` — a future language- +// version model would EDIT this enum explicitly). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every port consumer (instantiation +// legality, emission of the `input`/`output`/`inout` keyword, +// reverse-flow check) reads the direction tag uniformly; +// shared classifier, not a per-consumer scattered fact. +// 2. Variant-is-data — FAILS: a `{ name: Symbol }` proxy reopens +// the readable-string heuristic surface K-1 forecloses (a +// `match name { "input" => … }` smell). The enum IS the +// faithful form (algebra.dag:332 `Ordering` precedent). +// 3. Algebraic form — N/A by construction: the three port +// directions are the Verilog spec's primitive port-flow +// taxonomy; they do not trace to a richer std/ algebraic +// structure (no `BoundedLattice` with Inout = top — +// that would be a parallel representation of "Inout admits +// both directions", a property derived FROM the three tags). +// 4. Dimensional — FAILS: a port has EXACTLY ONE direction; +// `input output foo` is a syntax error in Verilog itself. +// Mutually-exclusive alternatives, not simultaneous coordinates. +// 5. Parameterized family — FAILS: the three are structurally +// distinct flow-roles (consumer / producer / bidirectional) — +// NOT one generic `F` / projection over a separately- +// declared source set (Practice 7). They are the IEEE 1364-2005 +// spec's irreducible port-flow partition. +// Terminal: the closed three-way port-flow classifier of the +// IEEE 1364-2005 spec; a fourth direction is the C1 stop-signal. +type PortDirection + = Input + | Output + | Inout + + +// ───────────────────────────────────────────────────────────────────── +// NonTriregNetKind — the closed Verilog net-type-keyword classifier +// over the eleven non-`trireg` net types (IEEE 1364-2005 §3.7.1, §5.6). +// `trireg` is partitioned OFF this Disj because it is the only spec +// net-type that (a) carries storage (capacitive last-driven-value +// semantics, §3.10 / §7.10) and (b) admits `charge_strength` in +// net_declaration position while FORBIDDING `drive_strength` on the +// identifier-only form (§A.2.1.3 grammar's third/fourth alternatives). +// Treating that partition as STRUCTURAL — variant-of-`NetType` not +// admit-then-check on a free field — is the dissolution of the +// net_declaration illegal-states-representable concern openai-pro +// REQUEST_CHANGES flagged on PR #3176 2026-05-16. +// +// - Wire — `wire` standard net; resolves to X if multiply +// driven with conflicting values +// - Tri — `tri` identical to `wire` semantically; +// designer-intent marker for tri-state nets +// - Wand — `wand` wired-AND resolution +// - TriAnd — `triand` identical to `wand` semantically; +// designer-intent marker pairing with `tri` +// - Wor — `wor` wired-OR resolution +// - TriOr — `trior` identical to `wor` semantically; +// designer-intent marker pairing with `tri` +// - Tri0 — `tri0` pull-down (resolves to 0 if undriven) +// - Tri1 — `tri1` pull-up (resolves to 1 if undriven) +// - Supply0 — `supply0` constant 0 power-rail net +// - Supply1 — `supply1` constant 1 power-rail net +// - Uwire — `uwire` unresolved wire — exactly one driver +// required (IEEE 1364-2005 §5.6.6) +// +// CLOSED (C1 stop-signal). The eleven non-trireg keywords of the +// IEEE 1364-2005 §3.7.1 table; `trireg` is the twelfth, and lives +// as a distinct top-level NetType variant rather than here. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟡 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). Ledger — five patterns +// attempted: +// 1. Fact placement — FAILS: every net-declaration emitter + +// every driver-resolution consumer reads the net-type tag +// uniformly; shared classifier. +// 2. Variant-is-data — FAILS: a `{ keyword: Symbol }` proxy +// reopens the K-1-forbidden readable-string heuristic; a +// `{ resolution_kind: Int }` proxy replaces a closed +// exhaustive sum with an unbounded Int (algebra.dag:332 +// `Ordering` precedent). +// 3. Algebraic form — N/A by construction: spec primitives. +// 4. Dimensional — FAILS: exactly one keyword per net declaration. +// 5. Parameterized family — FAILS: eleven structurally distinct +// resolution / pull / supply / unresolved variants (Practice 7). +// The Wire/Tri, Wand/TriAnd, Wor/TriOr designer-intent pairs +// MUST stay distinct at the syntactic surface (parse ∘ emit +// preserves writer intent). +// Terminal: the closed eleven-way non-trireg net-type-keyword +// classifier of the IEEE 1364-2005 spec. +// +// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md +// merged on origin/main): under the pre-#3200 consumer-DEPENDENT +// GREEN rule this Disj was correctly GREEN (no consumer needed the +// decomposition yet, so structural extraction was deferred). Under +// the post-#3200 consumer-INDEPENDENT rule this is 🟡 YELLOW +// because a namable richer source EXISTS: +// Axes: {resolution_function, default_when_undriven, driver_arity, +// designer_intent_marker} +// Resolution: Wire/Tri=X-on-conflict; Wand/TriAnd=AND; +// Wor/TriOr=OR; Tri0=pull0; Tri1=pull1; Supply0=const0; +// Supply1=const1; Uwire=single-driver-required +// Default-when-undriven: Wire/Tri/Wand/Wor=X; Tri0=0; Tri1=1; +// Supply0=0; Supply1=1; Uwire=N/A +// Driver-arity: multi-driver-resolution (Wire/Wand/Wor/Tri*); +// power-rail (Supply0/1); exactly-one (Uwire) +// Designer-intent marker: Tri/TriAnd/TriOr (semantically- +// equivalent partner variants kept distinct for parse∘emit +// writer-intent preservation) +// Trigger: first consumer of net-resolution semantics (synthesizer +// dispatch / driver-resolution walker). +// Obligation: the first meaning-consumer owes structural +// decomposition into a {resolution, default, arity} record AT +// the consumer site — NOT a local match-over-keyword lookup in +// this carrier. +type NonTriregNetKind + = Wire + | Tri + | Wand + | TriAnd + | Wor + | TriOr + | Tri0 + | Tri1 + | Supply0 + | Supply1 + | Uwire + + +// ───────────────────────────────────────────────────────────────────── +// NetType — the Verilog net-type classifier as the {storage-vs-non- +// storage} structural partition over the IEEE 1364-2005 §3.7.1 table. +// The partition is structural per spec §A.2.1.3 net_declaration +// grammar: `trireg` admits `charge_strength` and a different declarator +// alternative set than the other eleven net types. Modeling the +// partition at NetType (rather than a flat twelve-way Disj) makes the +// {trireg?} fact STRUCTURAL — consumers that need to discriminate +// `trireg` from the others (NetDeclaration variants, future port- +// position §12.3.3 carriers) get the partition from the type itself, +// no admit-then-check (codex / openai-pro REQUEST_CHANGES discipline +// on PR #3176 2026-05-16). +// +// - NonTriregNet { kind: NonTriregNetKind } +// — one of the eleven non-`trireg` net-type keywords (see +// NonTriregNetKind above). +// - TriregNet +// — `trireg`; the storage net type. Nullary variant because +// there is only one trireg keyword (no sub-discrimination). +// +// CLOSED (C1 stop-signal). Two-way storage-vs-non-storage partition; +// a new net-type with `trireg`-like behavior is an edit to TriregNet +// (sub-Disj-with-payload, identical to NonTriregNet's shape if it +// ever needs sub-discrimination); a new non-storage net-type extends +// NonTriregNetKind. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: shared classifier across all net +// declarations + ANSI port-net carriers + driver-resolution +// consumers; the {trireg?} fact must be uniformly available. +// 2. Variant-is-data — FAILS: a `{ is_trireg: Bool, keyword: ... }` +// proxy reintroduces the admit-then-check shape the structural +// partition exists to dissolve. The 2-way Disj IS the dissolution. +// 3. Algebraic form — N/A by construction: the {storage-vs-non- +// storage} partition is the spec's irreducible §3.10 / §A.2.1.3 +// structural axis, not a richer std/ algebraic source. +// 4. Dimensional — FAILS: one net-type per declaration; mutually +// exclusive alternatives. +// 5. Parameterized family — FAILS: the two variants are structurally +// heterogeneous (NonTriregNet carries a `kind` payload, TriregNet +// is nullary). The trireg keyword is the SOLE storage net-type +// per spec — no generic `F` projection over a richer source. +// Terminal: the closed two-way Verilog net-type {storage-vs-non- +// storage} partition. +type NetType + = NonTriregNet { kind: NonTriregNetKind } + | TriregNet + + +// (VariableType has been dissolved into VariableDeclaration's +// Disj-with-named-payloads below — the spec couples kind × packing +// admissibility (only `reg` accepts a `[msb:lsb]` packing per IEEE +// 1364-2005 §5.7), and modeling kind and packing as independent +// coordinates ratified the illegal state "Integer with Packed +// range" — the INVARIANTS P2 illegal-states-unrepresentable anti- +// pattern (codex BLOCKING review on PR #3176). The 5-pattern ledger +// for the dissolved partition lives on VariableDeclaration; the +// reasoning is identical except that "Variant-is-data" now FAILS +// for the additional reason that uniform `{ kind, packing }` ratifies +// the illegal state. + + +// ───────────────────────────────────────────────────────────────────── +// EdgeTrigger — the closed Verilog sensitivity-event classifier +// (IEEE 1364-2005 §9.7.2). The trigger condition under which an +// always-block's body re-executes when an event-control signal +// transitions. +// +// - PosEdge — `posedge` rising edge: 0→1 transition (also +// X→1, Z→1; the spec defines edge events +// on the implicit ordering 0 < X = Z < 1) +// - NegEdge — `negedge` falling edge: 1→0 transition +// - AnyChange — bare signal name in the event-list (no edge +// keyword): re-executes on ANY signal +// transition (level-sensitive) +// +// CLOSED (C1 stop-signal). A fourth edge type is an edit to THIS +// declaration under the L-2 pin discipline (the IEEE 1364-2005 §9.7.2 +// edge-event set is the authority). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every always-block's sensitivity- +// list consumer reads the trigger tag per item (a clock-edge +// always synthesizes to a flip-flop, a level-sensitive always +// to combinational or a latch); shared classifier, not +// scattered. +// 2. Variant-is-data — FAILS: a `{ direction: Int }` (+1/-1/0) +// proxy replaces a closed 3-valued exhaustive sum with an +// unbounded Int — violates P2 + M4 (algebra.dag:332 `Ordering` +// precedent, which uses the SAME shape). +// 3. Algebraic form — N/A by construction: the three triggers +// are the IEEE 1364-2005 spec's primitive event-control +// vocabulary; they do not trace to a richer std/ algebraic +// structure. +// 4. Dimensional — FAILS: a sensitivity-list item carries +// EXACTLY ONE trigger; `posedge negedge clk` is a syntax +// error. Mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the three are structurally +// distinct event-control shapes (rising-edge / falling-edge / +// level-sensitive) — NOT one generic `F` / projection over +// a separately-declared source set (Practice 7). +// Terminal: the closed three-way sensitivity-trigger classifier of +// the IEEE 1364-2005 spec. +type EdgeTrigger + = PosEdge + | NegEdge + | AnyChange + + +// ───────────────────────────────────────────────────────────────────── +// ProceduralAssignKind — the closed Verilog procedural-assignment +// scheduling discriminator (IEEE 1364-2005 §9.2). Inside an always- +// or initial-block, an assignment to a `reg`-typed destination is +// either BLOCKING or NON-BLOCKING; the discriminator selects when the +// write commits within the simulation time step. +// +// - Blocking — `=` commits BEFORE the next statement in the +// Bind chain (sequential-by-construction; +// the destination's new value is visible to +// the next statement) +// - NonBlocking — `<=` SCHEDULES the write for the end of the +// time step (the destination's old value is +// visible to every subsequent statement in +// the same time step; all non-blocking +// writes commit at once) +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 admits exactly these two +// assignment-scheduling shapes; SystemVerilog's continuous-assign +// inside procedural blocks is a separate construct, not a third +// scheduling shape. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every procedural-assignment emitter +// AND the synthesis-time race-check ("non-blocking required +// for flip-flop inference") read the kind uniformly; shared +// classifier, not scattered. +// 2. Variant-is-data — FAILS: a `{ deferred: Bool }` proxy is a +// faithful 2-valued representation, but the LEXICAL SURFACE +// (`=` vs `<=`) is a closed two-keyword pair the parser / +// emitter must dispatch on; the named-enum is the M4-faithful +// form (closed sets are enums, not Bool proxies — the +// `Ordering`-as-Int rejection generalizes). +// 3. Algebraic form — N/A by construction: the two are the IEEE +// 1364-2005 spec's primitive scheduling-discriminator pair; +// they do not trace to a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a procedural assignment carries +// EXACTLY ONE kind; `x = <= y` is a syntax error. +// Mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the two are structurally +// distinct scheduling shapes (immediate / deferred) — NOT one +// generic `F` / projection over a separately-declared +// source set (Practice 7). +// Terminal: the closed two-way procedural-assignment scheduling +// classifier of the IEEE 1364-2005 spec. +type ProceduralAssignKind + = Blocking + | NonBlocking + + +// ───────────────────────────────────────────────────────────────────── +// VectorRange — a packed bit-vector index range `[msb:lsb]` +// (IEEE 1364-2005 §3.10 / §A.8.3). Conj record (no Practice-4 ledger — +// only coproducts dissolve). +// +// Per spec §A.8.3 grammar: +// +// range ::= [ constant_expression : constant_expression ] +// +// where `constant_expression` admits integer literals, constant- +// identifier references (e.g. `WIDTH`, parameter names), arithmetic +// (`WIDTH-1`, `1<` / projection over a +// separately-declared source set (Practice 7). It IS the +// irreducible two-way packing partition. +// Terminal: the closed two-way packing classifier; multi-dimensional +// unpacked arrays would be an EDIT to this declaration under the +// L-2 pin discipline (a third variant). +type PackingShape + = Scalar + | Packed { range: VectorRange } + + +// ───────────────────────────────────────────────────────────────────── +// NetVectoredPacking — the net-declaration-specific packing-shape +// classifier, coupling `vectoredness` (vectored/scalared) to range- +// presence per IEEE 1364-2005 §3.7.1 + §A.2.1.3. Per spec §3.7.1: +// "The vectored keyword can be used only with a vector declaration." +// — vectoredness is meaningful ONLY when the net is ranged; `wire +// vectored a;` (unranged) is a syntax-error / semantic-violation +// (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 at line 1050). +// The structural coupling makes the spec-illegal "unranged-with- +// vectoredness" combination unrepresentable. +// +// This Disj is SCOPED TO NET DECLARATIONS: variable declarations +// (reg/integer/real/time/realtime) do NOT carry vectoredness per +// spec, and port declarations consume the more general PackingShape +// directly. Sibling carrier of PackingShape — different state-space +// (PackingShape lacks vectoredness; NetVectoredPacking gates it on +// the ranged variant), so no representation-duality at any carrier +// site (PackingShape never appears in NetDeclaration positions and +// NetVectoredPacking never appears in VariableDeclaration / ANSI +// port positions). +// +// - NetUnranged +// — `wire a;` form: no `[msb:lsb]` range; vectoredness is not +// carried because the spec forbids the keyword in this form. +// - NetRanged { vectoredness: VectorednessClause, range: VectorRange } +// — `wire [7:0] a;` / `wire vectored [7:0] a;` / `wire scalared +// [7:0] a;` forms: the range is present and vectoredness IS +// carried (with the NoVectoredness | VectoredNet | ScalaredNet +// three-way partition admitting the §3.7.1 spec choices). +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.2.1.3 admits these two +// net-packing forms (range-absent vs range-present); a third form +// would be an EDIT to this declaration under the L-2 pin discipline. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every net-declaration emitter and +// every signal-width / synthesizer-hint consumer reads the +// net-packing-shape tag uniformly; shared classifier. +// 2. Variant-is-data — FAILS: collapsing to a uniform +// `{ packing: PackingShape, vectoredness: VectorednessClause }` +// ratifies the spec-forbidden "unranged-with-vectoredness" +// state — exactly the §3.7.1 illegal state this Disj exists +// to dissolve. The Disj-with-payload-on-ranged-variant-only +// is the dissolved form. +// 3. Algebraic form — N/A by construction: the range-presence +// axis IS the spec's §A.2.1.3 partition; not a richer std/ +// algebraic source. +// 4. Dimensional — FAILS: a single net_declaration has EXACTLY +// ONE packing form (ranged or unranged); mutually exclusive. +// 5. Parameterized family — FAILS: NetUnranged is nullary; +// NetRanged carries a {vectoredness, range} payload — +// structurally heterogeneous (Practice 7); the partition's +// defining structural fact is the vectoredness-gated-on-range +// coupling itself. +// Terminal: the closed two-way net-declaration packing classifier +// of the IEEE 1364-2005 §A.2.1.3 spec. +type NetVectoredPacking + = NetUnranged + | NetRanged { vectoredness: VectorednessClause, range: VectorRange } + + +// ───────────────────────────────────────────────────────────────────── +// Signedness — the closed Verilog net/reg signedness classifier +// (IEEE 1364-2005 §5.6 "Signed types"). The `signed` keyword on a net +// or `reg` declaration selects two's-complement signed interpretation +// of the bit-vector; the default (no keyword) is unsigned. The +// signedness fact governs sign-extension on assignment, comparison +// semantics, and arithmetic operator dispatch — a fact every emission +// / arithmetic consumer must preserve per INVARIANTS P2 (codex +// BLOCKING review on PR #3176 2026-05-16 surfaced this gap; the +// prior NetDeclaration / RegVariable collapsed signed and unsigned +// packed forms, losing a spec-mandated boundary fact). +// +// - Signed — `signed` modifier present; two's-complement +// signed interpretation; sign-extension on +// assignment; signed-arithmetic operator dispatch +// - Unsigned — no `signed` modifier; unsigned modular +// interpretation; zero-extension on assignment; +// unsigned-arithmetic operator dispatch (the spec's +// default) +// +// CLOSED (C1 stop-signal). The signedness axis is BINARY per the +// IEEE 1364-2005 spec; a third interpretation is an edit to THIS +// declaration under the L-2 pin discipline. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every arithmetic-emission consumer +// and every assignment-extension consumer reads the signedness +// tag uniformly to dispatch (signed vs unsigned operator +// lowering; sign- vs zero-extension); shared classifier, not +// scattered. +// 2. Variant-is-data — FAILS: a `{ signed: Bool }` proxy is a +// faithful 2-valued representation, but the LEXICAL SURFACE +// (`signed` keyword present / absent) is a closed pair the +// parser/emitter dispatch on; the named-enum is the M4-faithful +// form (closed sets are enums, not Bool proxies — same +// argument as ProceduralAssignKind's ledger). +// 3. Algebraic form — PARTIAL: each variant grounds in a different +// std/algebra structure (Signed → OrderedRing on the underlying +// bit-vector width; Unsigned → Semiring). That grounding is +// the inhabitance walk DEFERRED to D2 per the file's "Owned +// ELSEWHERE" framing; the signedness enum itself stays a closed +// classifier. +// 4. Dimensional — FAILS: a net/reg declaration is EXACTLY ONE +// signedness; `wire signed signed x;` is a syntax error. +// Mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the two are structurally +// distinct arithmetic-interpretation primitives — NOT one +// generic `F` / projection over a separately-declared +// source set (Practice 7). They are the spec's irreducible +// signedness partition. +// Terminal: the closed two-way Verilog signedness classifier of the +// IEEE 1364-2005 spec. +type Signedness + = Signed + | Unsigned + + +// ───────────────────────────────────────────────────────────────────── +// DriveStrengthClause — the closed Verilog drive-strength clause +// classifier on a net_declaration (IEEE 1364-2005 §A.2.1.3 / §7.10). +// The clause is OPTIONAL per spec — present-or-absent partition +// modeled as a closed Disj rather than an empty-string sentinel on +// a `String` field (openai-pro REQUEST_CHANGES on PR #3176; same +// pattern as PortConnectionActual's BlankConnection — closed sum, +// not sentinel). `drive_strength` admits the §7.10 `(strength0, +// strength1)` keyword set; `charge_strength` (for `trireg`) is a +// DISTINCT spec set (§A.5.1 `small | medium | large`) and lives in +// its own sibling Disj `ChargeStrengthClause` below — the two are +// not interchangeable on the spec surface. +// +// - NoDriveStrength +// — no `(strong0, weak1)` clause on the declaration. +// - DriveStrengthLexeme { lexeme: String } +// — the clause as a verbatim lexeme (sub-grammar deferred to +// T-4 LanguageModel — the spec's closed strength-keyword set +// lives there). +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 admits the present/absent +// partition; per-strength-keyword closure is owned by the bundled +// LanguageModel. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every net-declaration emitter + +// every drive-resolution consumer reads the clause uniformly; +// shared classifier. +// 2. Variant-is-data — FAILS: collapsing to `{ lexeme: String }` +// with "" = absent reintroduces the empty-string sentinel +// anti-pattern this Disj exists to dissolve (PortConnection +// Actual's BlankConnection precedent rejected the same shape). +// 3. Algebraic form — N/A by construction: the present/absent +// partition is the spec's clause-presence axis; not a richer +// std/ algebraic structure. +// 4. Dimensional — FAILS: a net_declaration has EXACTLY ONE +// drive-strength clause state; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: NoDriveStrength is nullary; +// DriveStrengthLexeme carries a `lexeme: String` payload — +// structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog drive-strength clause- +// presence classifier. +type DriveStrengthClause + = NoDriveStrength + | DriveStrengthLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// ChargeStrengthClause — the closed Verilog charge-strength clause +// classifier on a `trireg` net_declaration (IEEE 1364-2005 §A.2.1.3 / +// §A.5.1 / §7.10). The clause is OPTIONAL per spec and applies ONLY +// to the identifier-only `trireg` net_declaration form (§A.2.1.3 +// third alternative); on the `trireg` assignment form `drive_strength` +// applies instead. Sibling Disj of DriveStrengthClause — kept distinct +// because the spec keyword sets are disjoint: drive_strength = (§7.10 +// strength0, strength1 pairs), charge_strength = §A.5.1 small | +// medium | large. +// +// - NoChargeStrength +// — no `(small)` / `(medium)` / `(large)` clause on the +// trireg declaration. +// - ChargeStrengthLexeme { lexeme: String } +// — the clause as a verbatim lexeme; sub-grammar (the +// small/medium/large keyword closure) deferred to the bundled +// T-4 LanguageModel. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as DriveStrengthClause; abbreviated for brevity (each pattern's +// argument is identical modulo "drive" vs "charge"). +// 1. Fact placement — FAILS: shared classifier across trireg-form +// emitters / simulation-init consumers. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected +// (same BlankConnection precedent argument). +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one charge-strength state per trireg +// declaration. +// 5. Parameterized family — FAILS: NoChargeStrength is nullary; +// ChargeStrengthLexeme carries a `lexeme: String` payload — +// structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog charge-strength clause- +// presence classifier. Added 2026-05-16 per openai-pro REQUEST_ +// CHANGES on PR #3176 — net_declaration §A.2.1.3 grammar requires +// charge_strength to be available on the identifier-only `trireg` +// form distinct from `drive_strength`. +type ChargeStrengthClause + = NoChargeStrength + | ChargeStrengthLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// DelayClause — the closed Verilog delay3 clause classifier on a +// net_declaration (IEEE 1364-2005 §A.2.1.3 / §7.14). The clause is +// OPTIONAL per spec — present-or-absent partition as a closed Disj +// (same pattern as DriveStrengthClause). +// +// - NoDelay +// — no `#5` / `#(2:3:4)` clause on the declaration. +// - DelayLexeme { lexeme: String } +// — the delay clause as a verbatim lexeme; sub-grammar deferred +// to T-4 LanguageModel. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every net-declaration emitter and +// every timing-aware consumer reads the clause uniformly. +// 2. Variant-is-data — FAILS: empty-string sentinel rejection +// same argument as DriveStrengthClause. +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: exactly one delay-clause state per +// declaration. +// 5. Parameterized family — FAILS: heterogeneous payloads +// (Practice 7). +// Terminal: the closed two-way Verilog delay-clause-presence +// classifier. +type DelayClause + = NoDelay + | DelayLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// AttributeInstanceClause — the closed Verilog attribute_instance- +// list-presence classifier (IEEE 1364-2005 §A.9.1 / §A.1.4). Most +// syntactic constructs in §A.1.4 (module_items, generate_items, +// statements, declarations, port_declarations, expression operators) +// admit an OPTIONAL list of attribute_instance prefixes: +// +// attribute_instance ::= (* attr_spec { , attr_spec } *) +// attr_spec ::= attr_name [ = constant_expression ] +// +// Examples: `(* keep *) assign x = y;`, `(* synthesis_full_case *) +// always @(...) ...`, `(* dont_touch *) Adder a1 (...)`. The prior +// shape made attribute_instances unrepresentable on structured +// module_item carriers — they could only leak into unrelated lexeme +// payloads (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 at +// line 2884). The fix carries this Disj per-variant on +// AnsiModuleItem / NonAnsiModuleItem. +// +// - NoAttributeInstances +// — no `(* … *)` prefix on the item. +// - AttributeInstanceLexeme { lexeme: String } +// — one or more `(* attr_spec, … *)` prefixes as a verbatim +// lexeme; sub-grammar (the attr_name + constant_expression +// internal structure of each attribute_instance) deferred to +// the bundled T-4 LanguageModel via the established body_lexeme +// precedent. Multiple `(* a *)(* b *)` prefixes per spec are +// carried as one concatenated lexeme — the parser splits. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as DriveStrengthClause / DelayClause; abbreviated for brevity. +// 1. Fact placement — FAILS: shared across every module-item / +// generate-item / statement / declaration carrier; not +// scattered. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected +// (same BlankConnection precedent argument). +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one attribute-instance-list state per +// item; mutually exclusive (present vs absent at the boundary). +// 5. Parameterized family — FAILS: NoAttributeInstances is +// nullary; AttributeInstanceLexeme carries a `lexeme: String` +// payload — structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog attribute_instance-list +// classifier of the IEEE 1364-2005 §A.9.1 spec. +type AttributeInstanceClause + = NoAttributeInstances + | AttributeInstanceLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// VectorednessClause — the closed Verilog vectored/scalared +// declaration-boundary classifier on a net_declaration (IEEE +// 1364-2005 §A.2.1.3 / §3.7.1). The clause is OPTIONAL per spec and +// is DISTINCT from drive_strength: it carries a synthesizer hint +// about whether the net is to be treated as a single addressable +// unit (`vectored`) or as bit-addressable (`scalared`). +// +// - NoVectoredness +// — neither `vectored` nor `scalared` keyword on the +// declaration (the spec default). +// - VectoredNet +// — `vectored` modifier; synthesizer treats the net as a +// single addressable unit (bit/part-select access constrained). +// - ScalaredNet +// — `scalared` modifier; synthesizer treats the net as +// bit-addressable. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 admits exactly the +// three-way present/absent + which-keyword partition (vectored +// and scalared are mutually exclusive per spec — both modifiers +// in one declaration is a syntax error). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every net-declaration emitter + +// every synthesizer-hint consumer reads the clause uniformly; +// shared classifier. +// 2. Variant-is-data — FAILS: a `{ kind: Symbol }` proxy reopens +// the readable-string heuristic surface K-1 forecloses; a +// `{ vectored: Bool, scalared: Bool }` proxy ratifies the +// spec-forbidden "both keywords" state. The 3-variant Disj +// IS the dissolved form. +// 3. Algebraic form — N/A by construction: synthesizer-hint +// partition, not a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single net_declaration has EXACTLY +// ONE vectoredness state; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the three variants are +// structurally distinct (none-vs-vectored-vs-scalared +// semantically heterogeneous) — NOT one generic `F` +// projection (Practice 7). +// Terminal: the closed three-way Verilog vectored/scalared clause +// classifier. Added per codex BLOCKING on PR #3176 2026-05-16 — +// the vectored/scalared clause is a §A.2.1.3 declaration-boundary +// fact distinct from drive_strength; the prior commentary "collapsed +// into the strength lexeme position" overloaded the two clauses. +type VectorednessClause + = NoVectoredness + | VectoredNet + | ScalaredNet + + +// ───────────────────────────────────────────────────────────────────── +// (NetInitializerClause was DISSOLVED on PR #3176 2026-05-16 per +// openai-pro REQUEST_CHANGES. The optional-initializer state is +// dissolved structurally by NetDeclaration's per-form Disj split: +// the §A.2.1.3 assignment form's declarators ALWAYS carry an +// initializer (NetAssignmentDeclarator.rhs_lexeme), the identifier- +// only form's declarators NEVER do (NetIdentifierDeclarator carries +// only `name: Symbol`). The "no initializer on an assignment-form +// declarator" and "initializer on an identifier-only declarator" +// states are structurally unrepresentable, so a present/absent +// initializer-presence Disj on a single declarator type became dead +// weight. The deletion is the dissolution.) + + +// ───────────────────────────────────────────────────────────────────── +// UnpackedDimensionsClause — the closed Verilog +// unpacked-array-dimensions-presence classifier on a variable +// declarator (IEEE 1364-2005 §7.4 / §A.2.4). Optional per spec — +// present-or-absent partition. +// +// - NoUnpackedDimensions +// — `reg a;` form: scalar (no unpacked array). +// - UnpackedDimensionsLexeme { lexeme: String } +// — `reg mem[0:1023];` form: unpacked-array dimensions as a +// verbatim lexeme. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every variable-declaration consumer +// reads the clause uniformly to size the unpacked array vs +// scalar. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected. +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one unpacked-dimensions state per +// declarator. +// 5. Parameterized family — FAILS: heterogeneous payloads. +// Terminal: the closed two-way Verilog unpacked-dimensions-presence +// classifier. +type UnpackedDimensionsClause + = NoUnpackedDimensions + | UnpackedDimensionsLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// VariableInitializerClause — the closed Verilog variable-declarator +// initializer-presence classifier (IEEE 1364-2005 §A.2.4). Optional +// per spec — present-or-absent partition. +// +// - NoVariableInitializer +// — `reg a;` form: no initializer. +// - VariableInitializerLexeme { lexeme: String } +// — `reg a = 8'h00;` form: initializer as a verbatim lexeme. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as UnpackedDimensionsClause; abbreviated for brevity (each pattern's +// argument is identical modulo "unpacked-dimensions" vs "variable- +// initializer"). The pre-#3176-openai-pro shape pointed at +// NetInitializerClause, which has since been dissolved structurally +// by NetDeclaration's per-form Disj split. +// 1. Fact placement — FAILS: shared classifier across emitters / +// simulation-init / elaboration consumers. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected. +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one initializer state per declarator. +// 5. Parameterized family — FAILS: heterogeneous payloads. +// Terminal: the closed two-way Verilog variable-initializer- +// presence classifier. +type VariableInitializerClause + = NoVariableInitializer + | VariableInitializerLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// NetDeclaration — a Verilog net declaration (`wire foo;`, +// `wire [7:0] bus;`, `wire signed [15:0] s;`, `wand x;`, +// `wire (strong0, weak1) #5 a = expr_a, b = expr_b;`, `trireg +// (small) [3:0] cap_bus;`, `trireg (weak0, weak1) #2 stor = expr_s;`). +// IEEE 1364-2005 §3.10 / §A.2.1.3. +// +// Per spec §A.2.1.3 net_declaration is a FOUR-WAY closed alternative +// set, NOT a free product of {net_type, strength, form, declarators}: +// +// net_declaration ::= +// net_type [drive_strength] [vectored|scalared] [signed] [range] +// [delay3] list_of_net_decl_assignments ; +// | net_type [vectored|scalared] [signed] [range] [delay3] +// list_of_net_identifiers ; +// | trireg [charge_strength] [vectored|scalared] [signed] [range] +// [delay3] list_of_net_identifiers ; +// | trireg [drive_strength] [vectored|scalared] [signed] [range] +// [delay3] list_of_net_decl_assignments ; +// +// where `net_type` (per §3.7.1) is one of the eleven non-`trireg` +// keywords; `trireg` is the fourth-row net-type with distinct +// strength-and-form admissibility. +// +// Modeling the four spec alternatives as STRUCTURAL variants makes +// these illegal states unrepresentable (openai-pro REQUEST_CHANGES +// on PR #3176 2026-05-16; same INVARIANTS P2 / Practice-2 discipline +// as VariableDeclaration's kind×packing structural split below): +// +// - drive_strength on the identifier-only form (forbidden by spec) +// - charge_strength on a non-trireg net_type (forbidden by spec) +// - mixed init/non-init declarator lists (forbidden by spec) +// - identifier-only declarators with initializers (forbidden by spec) +// - assignment-form declarators without initializers (forbidden) +// +// The discriminating axes are STRUCTURAL per variant: {trireg?} × +// {form: identifier-only vs assignment}. The non-trireg-net-type +// keyword set (`wire / tri / wand / triand / wor / trior / tri0 / +// tri1 / supply0 / supply1 / uwire`) rides as a `NonTriregNetKind` +// field on the two non-trireg variants; the trireg variants do NOT +// carry a `net_type` field — the variant identity IS the net_type +// fact. `drive_strength` and `charge_strength` PRESENCE remain inside +// their respective Clause Disjs (DriveStrengthClause / +// ChargeStrengthClause), not as a top-level variant axis — strength +// is optional per spec brackets, and the existing Clause Disjs +// already structurally encode present-vs-absent. +// +// - NonTriregIdentifierForm — `wire [7:0] a, b, c;` (no drive_ +// strength permitted on this spec +// alternative; declarators are +// name-only). +// - NonTriregAssignForm — `wire (strong0, weak1) [7:0] a = +// e1, b = e2;` (optional drive_ +// strength; declarators carry +// required initializers). +// - TriregIdentifierForm — `trireg (small) [3:0] cap_bus;` +// (optional charge_strength; +// declarators are name-only). +// - TriregAssignForm — `trireg (weak0, weak1) #2 stor = +// e_s;` (optional drive_strength; +// declarators carry required +// initializers). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every net-declaration emitter + +// every elaboration / well-formedness consumer reads the +// net_declaration uniformly; not a scattered fact. +// 2. Variant-is-data — FAILS: collapsing into `{ is_trireg: Bool, +// has_assignments: Bool, drive_strength, charge_strength, … }` +// reintroduces the admit-then-check shape this Disj exists to +// dissolve (non-trireg + charge_strength becomes representable; +// identifier-form + drive_strength becomes representable). +// Structural Disj forecloses. +// 3. Algebraic form — N/A by construction: the {trireg?} × {form} +// partition is the spec's §A.2.1.3 irreducible structural axis, +// not a richer std/ algebraic source. +// 4. Dimensional — FAILS: a net_declaration is EXACTLY ONE of +// the four spec forms; mutually exclusive alternatives. +// 5. Parameterized family — FAILS: the four variants are +// structurally heterogeneous (kind-vs-no-kind, drive-vs-charge- +// vs-neither strength, assignment-vs-identifier declarators) — +// no generic `F` projection over a richer source set +// (Practice 7). +// Terminal: the closed four-way IEEE 1364-2005 §A.2.1.3 +// net_declaration alternative set. +// +// Prior shape (single Conj-record with free {net_type, drive_strength, +// declarators: List}) was the codex BLOCKING-fix shape +// on PR #3176 2026-05-16; openai-pro REQUEST_CHANGES at sha 6f587e6c +// correctly flagged that it admitted the five spec-illegal states +// above as a free product. This four-variant structural split is +// the dissolution. +type NetDeclaration + = NonTriregIdentifierForm { + kind: NonTriregNetKind + net_packing: NetVectoredPacking + signedness: Signedness + delay: DelayClause + // 🟡 spec-non-empty (§A.2.1.3 list_of_net_identifiers) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + identifiers: List + } + | NonTriregAssignForm { + kind: NonTriregNetKind + drive_strength: DriveStrengthClause + net_packing: NetVectoredPacking + signedness: Signedness + delay: DelayClause + // 🟡 spec-non-empty (§A.2.1.3 list_of_net_decl_assignments) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List + } + | TriregIdentifierForm { + charge_strength: ChargeStrengthClause + net_packing: NetVectoredPacking + signedness: Signedness + delay: DelayClause + // 🟡 spec-non-empty (§A.2.1.3 list_of_net_identifiers) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + identifiers: List + } + | TriregAssignForm { + drive_strength: DriveStrengthClause + net_packing: NetVectoredPacking + signedness: Signedness + delay: DelayClause + // 🟡 spec-non-empty (§A.2.1.3 list_of_net_decl_assignments) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List + } + + +// ───────────────────────────────────────────────────────────────────── +// NetAssignmentDeclarator — one (net_identifier, initializer- +// expression) pair in a net_declaration's list_of_net_decl_assignments +// (IEEE 1364-2005 §A.2.4: `net_decl_assignment ::= net_identifier = +// expression`). A single `wire [7:0] a = e_a, b = e_b;` carries TWO +// NetAssignmentDeclarators. The initializer is REQUIRED on every +// element of the assignment-form (no `[]` brackets in the spec +// production) — it is structurally non-optional here, dissolving the +// prior optional-initializer Disj on a unified NetDeclarator type +// (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16). Conj record +// (no Practice-4 ledger). +// +// - name the declared net identifier (K-1-opaque +// Symbol). +// - rhs_lexeme the initializer expression as a verbatim +// lexeme. Sub-grammar deferred to the bundled +// T-4 LanguageModel via the established +// body_lexeme precedent. +type NetAssignmentDeclarator { + name: Symbol + rhs_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// NetIdentifierDeclarator — one element of a net_declaration's +// list_of_net_identifiers (IEEE 1364-2005 §A.2.3 / §A.2.1.3 +// identifier-only form). Carries the net identifier and optional +// unpacked-array dimensions: the identifier-only spec form forbids +// initializers structurally (openai-pro REQUEST_CHANGES on PR #3176 +// 2026-05-16 — making "identifier-only-with-initializer" +// unrepresentable rather than a runtime check). Per §A.2.3: +// `net_identifier [ dimension { dimension } ]` — each identifier +// admits an OPTIONAL unpacked-array dimension suffix +// (openai-pro REQUEST_CHANGES on PR #3176 sha 4ccc6267 added this +// field; the prior shape dropped the per-identifier dimensions fact). +// A single `wire [7:0] a, b[0:1023], c;` carries THREE +// NetIdentifierDeclarators (the second with unpacked dimensions). +// Conj record (no Practice-4 ledger). +// +// - name the declared net identifier (K-1-opaque +// Symbol). +// - unpacked_dimensions optional unpacked-array dimensions per +// §A.2.3 (reuses UnpackedDimensionsClause). +type NetIdentifierDeclarator { + name: Symbol + unpacked_dimensions: UnpackedDimensionsClause +} + + +// ───────────────────────────────────────────────────────────────────── +// VariableDeclaration — a Verilog variable (`reg foo;`, `reg [31:0] +// counter;`, `reg signed [15:0] s;`, `integer i;`, `real x;`, +// `time t;`, `realtime rt;`). IEEE 1364-2005 §3.7.2, §5.7 partitions +// variable declarations into five kinds, where ONLY `reg` admits a +// `[msb:lsb]` packing — the other four (`integer` / `real` / `time` +// / `realtime`) have spec-fixed widths and forbid a vector range +// (`[N:M] integer i;` is a syntax error per §5.7). The kind × packing +// admissibility is modeled STRUCTURALLY: only `RegVariable` carries +// a `packing` payload, so "Integer with Packed range" is +// unrepresentable — not "rejected by a check" — the INVARIANTS P2 +// illegal-states-unrepresentable shape (same design choice as +// node.dag's EdgeLabel, rust.dag's RustScalar Disj-with-named- +// payloads, and go.dag's GoScalar). The prior `{ var_type: +// VariableType, packing: PackingShape }` Conj-record-with- +// independent-coordinates form was the codex BLOCKING-review anti- +// pattern on PR #3176; this Disj-with-payloads form is the +// dissolution. +// +// The kind × signedness admissibility is also modeled STRUCTURALLY +// per IEEE 1364-2005 §5.6: `reg` admits `signed` (`reg signed [N:0]` +// is two's-complement signed bit-vector); `integer` is ALWAYS signed +// by spec (§3.7.2: "32-bit signed"); `time` is ALWAYS unsigned (the +// 64-bit simulation-time carrier); `real` and `realtime` are IEEE-754 +// floating-point and carry NO signedness keyword (the floating-point +// sign is internal to the IEEE-754 representation, not a separate +// declaration modifier). Only `RegVariable` carries the +// `signedness: Signedness` payload — "RealVariable signedness=Signed" +// is unrepresentable, just like the kind × packing partition (codex +// BLOCKING fix 2026-05-16 on PR #3176; the spec-fixed-signedness +// kinds DO NOT need the carrier because the fact is non-variant per +// spec). +// +// - RegVariable — `reg [msb:lsb] name;` / `reg signed [msb: +// lsb] name;` / `reg name;` general-purpose +// variable; the procedural-assignment +// destination; THE ONLY variable-kind that +// admits packing AND signedness modifiers +// - IntegerVariable — `integer name;` 32-bit signed (spec-fixed +// signed); no packing, no signedness payload +// - RealVariable — `real name;` double-precision IEEE-754 +// floating-point; no packing, no signedness +// payload (sign is internal to the IEEE-754 +// representation, not a declaration modifier) +// - TimeVariable — `time name;` 64-bit unsigned simulation- +// time carrier (spec-fixed unsigned); no +// packing, no signedness payload +// - RealTimeVariable — `realtime name;` aliased to `real` per +// §3.7.2; no packing, no signedness payload +// +// CLOSED (C1 stop-signal). A new variable-kind is an edit to THIS +// declaration under the L-2 pin discipline (SystemVerilog adds +// `logic` / `bit` / typed enums — a future language-version model +// would EDIT this Disj explicitly). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟡 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). Ledger — five patterns +// attempted: +// 1. Fact placement — FAILS: every variable-declaration emitter, +// every procedural-assignment legality check (only RegVariable +// is a legal procedural-assignment destination), every signed- +// vs-unsigned arithmetic dispatch, and the per-kind algebra +// inhabitance walk all read the variant tag uniformly; shared +// classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to `{ kind: VariableType, +// packing: PackingShape, signedness: Signedness }` ratifies +// multiple illegal states the spec forbids — "Integer with +// Packed range" (§5.7) AND "Real with signedness=Signed" (§5.6 +// — real is floating-point, no signedness modifier), AND +// "Time with signedness=Signed" (spec-fixed unsigned). The +// Disj-with-heterogeneous-payloads dissolves all of these: +// only RegVariable carries packing AND signedness; the spec- +// fixed-attribute kinds carry only `name`. Same dissolution +// shape as rust.dag's RustScalar and go.dag's GoScalar. +// 3. Algebraic form — PARTIAL: each variant grounds in a std/ +// algebra structure (RegVariable → `Semiring>` or +// `OrderedRing>` per declared packing × signedness; +// IntegerVariable → `OrderedRing>`; RealVariable / +// RealTimeVariable → `ApproximateField`; TimeVariable +// → `Semiring>`). That grounding is INHABITANCE — +// owned by the inhabiting carrier file (std/integer.dag, +// std/float.dag) per P2, and DEFERRED to the operator-pending +// D2 STOP. The variant set itself stays a closed classifier. +// 4. Dimensional — FAILS: a single variable declaration IS +// EXACTLY ONE variant; mutually-exclusive alternatives. The +// shapes differ across variants (RegVariable carries packing +// AND signedness; the rest carry neither) — they cannot be +// coordinates of a single record without the illegal-state +// smell. +// 5. Parameterized family — FAILS: the five are structurally +// heterogeneous (RegVariable carries packing + signedness; the +// rest carry neither; the algebraic groundings are five +// distinct std/algebra structures — Semiring or OrderedRing +// depending on packing×signedness / OrderedRing> / +// ApproximateField / Semiring> / aliased +// ApproximateField) — NOT one generic `F` / projection +// over a separately-declared source set (Practice 7). +// Terminal: the closed five-variant Verilog variable-declaration +// classifier; illegal kind×packing AND kind×signedness combinations +// are unrepresentable by construction. +// +// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md +// merged on origin/main): under the pre-#3200 consumer-DEPENDENT +// GREEN rule this Disj was correctly GREEN (D2 inhabitance not yet +// landed). Under the post-#3200 consumer-INDEPENDENT rule this is +// 🟡 YELLOW because a namable richer source EXISTS: +// Axes: {storage-class, width, signedness, algebra-grounding} +// RegVariable: storage=mutable-bit-vector; width=packing-payload; +// signedness=signedness-payload; algebra=Semiring/OrderedRing +// per packing×signedness +// IntegerVariable: storage=fixed-int; width=32; signedness= +// signed-fixed; algebra=OrderedRing> +// RealVariable: storage=ieee754-double; width=64; signedness= +// ieee754-internal; algebra=ApproximateField +// TimeVariable: storage=sim-time-counter; width=64; signedness= +// unsigned-fixed; algebra=Semiring> +// RealTimeVariable: aliased to RealVariable per spec §3.7.2 +// (parse∘emit preserves the keyword); same algebra-grounding +// as RealVariable +// Trigger: first consumer of variable-storage / algebra semantics +// (algebra inhabitance lens — D2 pathway). +// Obligation: the first meaning-consumer (D2 inhabitance work) owes +// structural decomposition into a {storage-class, width, +// signedness, algebra} record AT that consumer — NOT a local +// match-over-kind lookup in this carrier. +type VariableDeclaration + // declarators: 🟡 spec-non-empty (§A.2.4 / §7.4) — deferred to + // std/collection.dag Wave-A2 `List where non_empty` refinement; + // see shared TRACKED-SCAFFOLD note above. + = RegVariable { packing: PackingShape, signedness: Signedness, declarators: List } + | IntegerVariable { declarators: List } + | RealVariable { declarators: List } + | TimeVariable { declarators: List } + | RealTimeVariable { declarators: List } + + +// ───────────────────────────────────────────────────────────────────── +// VariableDeclarator — one entry in a variable declaration's +// list_of_variable_decl_assignments (IEEE 1364-2005 §A.2.4 / §3.10). +// Per spec grammar `variable_type` is either `variable_identifier +// { dimension }` (named-with-optional-unpacked-dimensions) OR +// `variable_identifier = constant_expression` (initialized) — +// MUTUALLY EXCLUSIVE alternatives, not independent coordinates. The +// prior {name, unpacked_dimensions, initializer} product shape +// admitted the spec-illegal `reg mem[0:1023] = 8'h00` combined +// dimensions+initializer state (openai-pro REQUEST_CHANGES on +// PR #3176 sha 4ccc6267 — VariableDeclarator product-shape admits +// illegal states). Split into a closed Disj over the two §A.2.4 +// alternatives makes the spec-illegal combined state structurally +// unrepresentable (INVARIANTS P2). +// +// A single declaration like `reg [7:0] a, mem[0:1023], c = 4'hF;` +// carries THREE VariableDeclarators (one NamedVariable per the first +// two names; one InitializedVariable for the last). The §7.4 PACKED +// dimensions stay on RegVariable's shared `packing` field at the +// outer level — those are TYPE-level, not declarator-level. +// +// - NamedVariable +// — `reg a;` / `reg mem[0:1023];` form: identifier with +// OPTIONAL unpacked-array dimensions; NO initializer. +// - InitializedVariable +// — `reg c = 4'hF;` form: identifier with REQUIRED initializer +// expression; NO unpacked-array dimensions. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.2.4 admits exactly the +// two variable_type alternatives. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every variable-declaration emitter +// and elaboration consumer reads the per-declarator form +// uniformly; shared classifier. +// 2. Variant-is-data — FAILS: a `{ unpacked_dimensions, +// initializer }` product (prior shape) admits the §A.2.4 +// spec-illegal combined dimensions+initializer state — exactly +// the P2 illegal-states-representable concern this Disj +// dissolves. +// 3. Algebraic form — N/A by construction: the two alternatives +// are the spec's §A.2.4 irreducible partition. +// 4. Dimensional — FAILS: a single variable_decl_assignment is +// EXACTLY ONE form; mutually exclusive alternatives. +// 5. Parameterized family — FAILS: NamedVariable carries +// `unpacked_dimensions: UnpackedDimensionsClause`; +// InitializedVariable carries `initializer: +// VariableInitializerClause` — structurally heterogeneous +// (Practice 7). +// Terminal: the closed two-way Verilog variable_decl_assignment +// alternative classifier of the IEEE 1364-2005 §A.2.4 spec. +type VariableDeclarator + = NamedVariable { + name: Symbol + unpacked_dimensions: UnpackedDimensionsClause + } + | InitializedVariable { + name: Symbol + initializer_lexeme: String + } + + +// (PortDeclarationStyle has been dissolved into ModulePortsList's +// Disj-with-named-payloads at the MODULE level — IEEE 1364-2005 +// §12.3.4 forbids mixing ANSI and non-ANSI styles within ONE module, +// so the style-choice belongs on the module's port-list as a whole, +// not as a per-port field. The prior per-port `style: PortDeclaration +// Style` admitted the spec-forbidden mixed-style state (codex BLOCKING +// review on PR #3176 surfaced this — the per-port encoding was a +// product-axis miscarve relative to the spec's module-header +// partition). See ModulePortsList below.) + + +// ───────────────────────────────────────────────────────────────────── +// (PortAnsiTypeKind was DELETED on PR #3176 2026-05-16 per codex +// non-blocking improvement. The earlier generic-set carrier became +// orphaned once AnsiPortDeclaration adopted direction-specific +// payload types — input/inout use AnsiNetPortType, output uses +// OutputPortAnsiTypeKind. Keeping the unused 6-way generic carrier +// risked a parallel-authority drift between two carriers modeling +// the same ANSI-port type/kind space. The direction-specific +// classifiers below are the SOLE authority; future ANSI-port +// type/kind extensions (SystemVerilog `logic`, etc.) edit the +// direction-specific classifiers directly.) + + +// ───────────────────────────────────────────────────────────────────── +// OutputPortAnsiTypeKind — the closed Verilog ANSI-OUTPUT-port +// type/kind classifier. IEEE 1364-2005 §12.3.3: "An output port can +// be of any net or variable type EXCEPT a real type" — floating- +// point types are not admitted as output ports because they have no +// well-defined inter-module wire representation. The output-specific +// admissible four-way partition is modeled here; the spec-illegal +// real / realtime output variants are unrepresentable by construction +// (codex BLOCKING fix on PR #3176 2026-05-16 — the prior shape +// reused a generic-output-port carrier admitting `output real` / +// `output realtime` which the spec forbids). +// +// - OutputAnsiNetType { net_type: NetType, packing: PackingShape, +// signedness: Signedness } +// — `output wire [7:0] data`; net family. +// - OutputAnsiRegType { packing: PackingShape, signedness: Signedness } +// — `output reg [7:0] count`; reg-typed (procedural-assignable +// output, the most common parameterized output form). +// - OutputAnsiIntegerType +// — `output integer counter`; 32-bit signed. +// - OutputAnsiTimeType +// — `output time t`; 64-bit unsigned simulation-time. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.3.3 admits exactly +// this four-way output-type partition; SystemVerilog adds further +// types — future language-version model EDITS this Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every output-port consumer reads the +// kind to dispatch emission / type-check legality; shared +// classifier, not scattered. +// 2. Variant-is-data — FAILS: reusing a generic 6-variant output- +// port carrier (the prior shape, predecessor to the direction- +// specific split) admits `output real` / `output realtime` — +// exactly the §12.3.3 illegal state this Disj dissolves. P2 +// illegal-states-unrepresentable. +// 3. Algebraic form — PARTIAL: each variant grounds in a std/ +// algebra structure (OutputAnsiNetType / OutputAnsiRegType → +// Semiring or OrderedRing per packing × signedness; +// OutputAnsiIntegerType → OrderedRing>; +// OutputAnsiTimeType → Semiring>). D2-deferred per +// "Owned ELSEWHERE". +// 4. Dimensional — FAILS: an ANSI output port has EXACTLY ONE +// type/kind; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the four variants are +// structurally heterogeneous (OutputAnsiNetType carries net_type +// + packing + signedness; OutputAnsiRegType carries packing + +// signedness; OutputAnsiIntegerType + OutputAnsiTimeType are +// nullary). NOT one generic `F` projection over a richer +// source set (Practice 7); the real/realtime exclusion is the +// §12.3.3 spec's output-port-admissibility partition, not a +// derived projection. +// Terminal: the closed five-way Verilog ANSI-output-port type/kind +// classifier (the no-net-no-reg variant added at sha 7b7dd0b54+ +// per codex L1600 BLOCKING on PR #3176 — §A.1.3 output_declaration +// admits `output [net_type] [signed] [range]` AND `output [reg] +// [signed] [range]` where both `net_type` and `reg` are +// syntactically OPTIONAL; "output [signed] [range] name;" with +// neither keyword is a legal spec form that resolves to a net via +// §12.3.3 separate-declaration inheritance OR defaults to wire); +// real/realtime outputs unrepresentable by construction per IEEE +// 1364-2005 §12.3.3. +// (DELETED 2026-05-16 per openai-pro REQUEST_CHANGES on PR #3176 +// sha 98953d5f: this single 5-way Disj conflated two §A.1.3 spec- +// alternatives — net-form outputs (list_of_port_identifiers, no +// initializers) and variable-form outputs (list_of_variable_port_ +// identifiers, with initializers). Replaced with two sibling Disjs +// OutputPortAnsiNetTypeKind + OutputPortAnsiVariableTypeKind below, +// consumed by separate AnsiOutputNetPort / AnsiOutputVariablePort +// variants of AnsiPortDeclaration, structurally forbidding `output +// wire y = 1'b0` while admitting all spec-legal output forms.) + + +// ───────────────────────────────────────────────────────────────────── +// OutputPortAnsiNetTypeKind — the closed Verilog ANSI-output-port +// type/kind classifier for the NET form: `output [net_type] [signed] +// [range] list_of_port_identifiers` (IEEE 1364-2005 §A.1.3, first +// output_declaration alternative). The list of identifiers uses +// `list_of_port_identifiers` — plain port_identifier elements with +// NO per-port initializers. Per port_declaration spec the net_type +// keyword (when present) excludes `trireg` — this carrier therefore +// uses NonTriregNetKind directly, not the broader NetType. Real/ +// realtime are not net types and are not admitted here. +// +// - OutputAnsiNetType { kind: NonTriregNetKind, packing, signedness } +// — `output wire [7:0] y`, `output wand a`, etc.; explicit +// non-trireg net-type keyword. +// - OutputAnsiNoNetType { packing, signedness } +// — `output [7:0] y` (no net_type keyword); spec §A.1.3 makes +// net_type bracketed/optional. Resolves to default wire OR +// inherits from a separate later declaration per §12.3.3. +// +// CLOSED (C1 stop-signal). Two-way net-form output partition; a +// third would be an L-2 pin edit. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Five-pattern ledger abbreviated (same shape +// arguments as the prior OutputPortAnsiTypeKind ledger): +// 1. Fact placement — FAILS: shared classifier across output-port +// emitters/recognizers. +// 2. Variant-is-data — FAILS: collapsing to `{kind: +// Option, packing, signedness}` re-admits the +// illegal "trireg-output" + the "net-form-with-initializer" +// states this Disj exists to dissolve. +// 3. Algebraic form — N/A by construction: spec's §A.1.3 +// net-output partition. +// 4. Dimensional — FAILS: exactly one form per output port; mutually +// exclusive. +// 5. Parameterized family — FAILS: heterogeneous payloads +// (OutputAnsiNetType carries `kind`; OutputAnsiNoNetType does +// not). Practice 7. +// Terminal: the closed two-way Verilog ANSI-output-port NET-form +// type/kind classifier. +type OutputPortAnsiNetTypeKind + = OutputAnsiNetType { kind: NonTriregNetKind, packing: PackingShape, signedness: Signedness } + | OutputAnsiNoNetType { packing: PackingShape, signedness: Signedness } + + +// ───────────────────────────────────────────────────────────────────── +// OutputPortAnsiVariableTypeKind — the closed Verilog ANSI-output- +// port type/kind classifier for the VARIABLE form: `output [reg] +// [signed] [range] list_of_variable_port_identifiers` / +// `output output_variable_type list_of_variable_port_identifiers` +// (IEEE 1364-2005 §A.1.3, second + third output_declaration +// alternatives). The list of identifiers uses +// `list_of_variable_port_identifiers` — each port_identifier admits +// an OPTIONAL initializer expression. Real/realtime are excluded +// per §12.3.3 ("An output port can be of any net or variable type +// EXCEPT a real type"). +// +// - OutputAnsiRegType { packing, signedness } +// — `output reg [7:0] count`; spec-form 2. +// - OutputAnsiIntegerType +// — `output integer counter`; 32-bit signed (spec-form 3). +// - OutputAnsiTimeType +// — `output time t`; 64-bit unsigned simulation-time +// (spec-form 3). +// +// CLOSED (C1 stop-signal). Three-way variable-form output partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟡 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). Five-pattern ledger +// abbreviated: +// 1. Fact placement — FAILS: shared output-port classifier. +// 2. Variant-is-data — FAILS: collapsing to `{kind, packing?, +// signedness?}` admits the §12.3.3 illegal `output real` / +// `output realtime` + reg-fixed-width violations the per-variant +// payload-presence rule dissolves. +// 3. Algebraic form — PARTIAL: each variant grounds in std/ +// algebra (Reg→Semiring/OrderedRing per packing×signedness; +// Integer→OrderedRing>; Time→Semiring>); +// D2-deferred per Owned ELSEWHERE. +// 4. Dimensional — FAILS: exactly one form per output port. +// 5. Parameterized family — FAILS: structurally heterogeneous +// payloads + algebraic groundings (Practice 7). +// Terminal: the closed three-way Verilog ANSI-output-port VARIABLE- +// form type/kind classifier; real/realtime outputs unrepresentable +// by construction per §12.3.3. +// +// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md +// merged on origin/main): under the pre-#3200 consumer-DEPENDENT +// GREEN rule this Disj was correctly GREEN. Under the post-#3200 +// consumer-INDEPENDENT rule this is 🟡 YELLOW because a namable +// richer source EXISTS — same {storage-class, width, signedness, +// algebra-grounding} matrix as VariableDeclaration (output-admissible +// subset: real/realtime structurally excluded per §12.3.3): +// OutputAnsiRegType: same as RegVariable +// OutputAnsiIntegerType: same as IntegerVariable +// OutputAnsiTimeType: same as TimeVariable +// Trigger: first consumer of variable-storage / algebra semantics +// (D2 inhabitance pathway — shared with VariableDeclaration +// consumer). +// Obligation: the first meaning-consumer owes structural +// decomposition into the same {storage-class, width, signedness, +// algebra} record consumed for VariableDeclaration — single- +// authority across the storage-kind family. +type OutputPortAnsiVariableTypeKind + = OutputAnsiRegType { packing: PackingShape, signedness: Signedness } + | OutputAnsiIntegerType + | OutputAnsiTimeType + + +// ───────────────────────────────────────────────────────────────────── +// NonAnsiPort — one entry in a non-ANSI-style Verilog module-HEADER +// port list (`module M (a, b, c);` / `module M (.ext(internal));` / +// `module M (a, , c);`). IEEE 1364-2005 §12.3.2 / §A.1.3: +// +// port ::= [port_expression] +// | .port_identifier ( [port_expression] ) +// +// The spec admits TWO port forms (regular-position vs external-named- +// binding), each with an OPTIONAL inner port_expression (the brackets +// in both alternatives) — yielding FOUR closed alternatives. The +// prior single-String shape collapsed all four into one mandatory +// lexeme, losing the blank-port + external-named-binding spec forms +// and forcing empty-string sentinel for blanks (openai-pro +// REQUEST_CHANGES on PR #3176 sha f9159ce8b at line 1654). +// +// Per §12.3.2 the non-ANSI header carries port-EXPRESSIONS only — +// port direction (input/output/inout) and any inline +// type/packing/signedness facts live in BODY `port_declaration` items +// (see PortDeclaration below + the PortDeclarationItem ModuleItem +// variant). The prior `PortDeclaration { direction, name }` on the +// header port-list collapsed this spec-boundary; corrected per codex +// BLOCKING on PR #3176 2026-05-16. The 4-way alternative split per +// §A.1.3 is the structural completion of that prior correction. +// +// - BlankNonAnsiPort +// — `module M (a, , c);` — the empty header position +// (port_expression absent on the regular form). +// - ExpressionNonAnsiPort { expression_lexeme: String } +// — `module M (a);` — port_expression present on the regular +// form (bare identifier, bit/part-select, or concatenation; +// sub-grammar deferred via the body_lexeme precedent). +// - ExternalNamedBlankPort { external_name: Symbol } +// — `module M (.ext());` — external-named-binding form with +// blank inner port_expression. +// - ExternalNamedExpressionPort { external_name: Symbol, expression_lexeme: String } +// — `module M (.ext(internal));` — external-named-binding form +// with port_expression present. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.1.3 admits exactly these +// four port-list-entry alternatives. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every header-port-list emitter + +// port-binding resolver branches on the form (blank / regular / +// external-named-blank / external-named-expr) uniformly; shared +// classifier at the port-list-entry boundary. +// 2. Variant-is-data — FAILS: collapsing to one mandatory lexeme +// reintroduces the empty-string sentinel for blank ports AND +// drops the spec's external-named-binding form as a distinct +// structural fact — exactly the §A.1.3 illegal-collapse +// INVARIANTS P2 concern this Disj exists to dissolve. +// 3. Algebraic form — N/A by construction: the four alternatives +// are the §A.1.3 spec's irreducible port-form partition. +// 4. Dimensional — FAILS: a single port-list entry is EXACTLY ONE +// form; mutually exclusive alternatives. +// 5. Parameterized family — FAILS: the four variants carry +// heterogeneous payloads — BlankNonAnsiPort is nullary; +// ExpressionNonAnsiPort carries `{ expression_lexeme }`; +// ExternalNamedBlankPort carries `{ external_name }`; +// ExternalNamedExpressionPort carries +// `{ external_name, expression_lexeme }`. Practice 7. +// Terminal: the closed four-way Verilog non-ANSI port-list-entry +// classifier of the IEEE 1364-2005 §A.1.3 spec. +type NonAnsiPort + = BlankNonAnsiPort + | ExpressionNonAnsiPort { expression_lexeme: String } + | ExternalNamedBlankPort { external_name: Symbol } + | ExternalNamedExpressionPort { external_name: Symbol, expression_lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// (PortDeclaration was DISSOLVED on PR #3176 sha cb028c7d+ per +// openai-pro REQUEST_CHANGES. Per spec §A.2.1.2: +// +// input_declaration ::= input [net_type] [signed] [range] list_of_port_identifiers +// output_declaration ::= output ... (multiple forms) +// inout_declaration ::= inout [net_type] [signed] [range] list_of_port_identifiers +// +// the SAME spec production covers BOTH the bare form (`input a;`) +// AND the with-modifiers form (`input [7:0] a;`) AND the with-type +// form (`input wire [7:0] a;`) — net_type / signed / range are all +// independently optional. The prior partition (PortDeclaration = +// direction+names only, AnsiPortDeclaration reused for with-type +// forms via NonAnsiBodyPortDeclarationItem) collapsed the +// with-modifiers-without-type form (`output [7:0] y;` followed by +// separate `reg [7:0] y;`) — PortDeclaration path lost range/signed, +// AnsiPortDeclaration path made the carrier "falsely complete" +// (openai-pro REQUEST_CHANGES on PR #3176 sha cb028c7d at line 1710). +// +// Resolution: AnsiPortDeclaration's existing no-net-type variants +// (AnsiInputInoutNoNetType for input/inout, OutputAnsiNoNetType for +// output) ALREADY cover the direction+modifiers-without-type form +// with the full {packing, signedness} payload — the bare-form +// `input a;` is the same carrier with packing=Scalar + +// signedness=Unsigned. PortDeclaration's direction+names shape is +// thus a strict subset (the {packing=Scalar, signedness=Unsigned} +// projection) of AnsiPortDeclaration's no-net-type variants. +// Keeping PortDeclaration as a separate carrier was +// representation-duality and a partition gap; dissolving it +// collapses both NonAnsiPortDeclarationItem + +// NonAnsiBodyPortDeclarationItem in NonAnsiModuleItem into one +// variant using AnsiPortDeclaration uniformly. Single carrier, +// single authority, full §A.2.1.2 spec form coverage.) + + +// ───────────────────────────────────────────────────────────────────── +// AnsiNetPortType — the closed type/payload variants admitted for an +// ANSI port that ONLY accepts net types (input + inout ports per IEEE +// 1364-2005 §12.3.3). Input and inout ports cannot be reg-typed +// (procedural assignment requires reg, which only output can carry), +// and cannot be the spec-fixed-width variable kinds (integer / real / +// time / realtime are output-only per spec). This carrier is the +// closed type-payload set for input / inout — strictly the net family. +// +// - AnsiInputInoutNet { kind: NonTriregNetKind, packing: PackingShape, +// signedness: Signedness } +// — any non-trireg net-type variant (wire/wand/wor/tri/etc.) +// with optional packing + signedness per spec §5.6. Per +// port_declaration §A.1.3 grammar, `trireg` is excluded at +// port positions (it is a net-declaration-only form); +// NonTriregNetKind enforces this structurally (openai-pro +// REQUEST_CHANGES on PR #3176 sha 98953d5f — the prior `NetType` +// field admitted spec-illegal `input trireg p` / `output trireg p`). +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.3.3 admits exactly net +// types for input/inout ANSI ports; SystemVerilog `logic` would EDIT +// this Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Single-variant Disj (currently exactly one +// type-shape — net with payload — admitted; future spec extensions +// would add variants). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every input/inout-ANSI consumer reads +// the type uniformly to dispatch emission / drive net-resolution; +// shared classifier. +// 2. Variant-is-data — FAILS: the single variant carries a +// structured payload (net_type + packing + signedness); a +// uniform record would collapse the future-extension axis a +// Disj preserves. +// 3. Algebraic form — N/A by construction: net types are the spec's +// primitive resolution-function set per §3.7.1; D2-deferred per +// "Owned ELSEWHERE". +// 4. Dimensional — FAILS: an input/inout ANSI port has EXACTLY ONE +// net-type payload; the variant is the dispatcher. +// 5. Parameterized family — FAILS: the single variant's payload is +// a structured record (NetType × PackingShape × Signedness), +// not one generic `F` projection (Practice 7). +// Terminal: the closed two-way net-type-presence-aware type-payload +// classifier for input / inout ANSI ports (the no-net-type variant +// added at sha 7b7dd0b54+ per codex L1600 BLOCKING on PR #3176 — +// §A.1.3 `input [net_type] [signed] [range]` makes net_type +// SYNTACTICALLY OPTIONAL; the prior single-variant shape forced +// every input/inout port to claim a net_type, dropping the spec's +// "port_declaration without type, type provided by a separate +// later net/reg declaration" §12.3.3 form). +type AnsiNetPortType + = AnsiInputInoutNet { kind: NonTriregNetKind, packing: PackingShape, signedness: Signedness } + | AnsiInputInoutNoNetType { packing: PackingShape, signedness: Signedness } + + +// ───────────────────────────────────────────────────────────────────── +// AnsiPortDeclaration — an ANSI-style Verilog module port (`module M +// (input wire [7:0] a, output reg b, output reg signed [3:0] count, +// inout tri bus, …);`). The header carries direction, name, AND a +// direction-specific type payload. Per IEEE 1364-2005 §12.3.3 the +// port declaration is "completely declared" by this single carrier; +// a body redeclaration is a SYNTAX ERROR. +// +// Direction × type-kind admissibility is modeled STRUCTURALLY via +// Disj-with-named-payloads per direction (codex BLOCKING fix on +// PR #3176 2026-05-16: the prior uniform `{ direction, name, type_ +// kind }` Conj record admitted spec-forbidden combinations like +// `input reg [N:0]` and `inout integer` — INVARIANTS P2 illegal- +// states-unrepresentable violation. Per spec §12.3.3 input/inout +// ports MUST be net-typed; only output ports admit reg/integer/real/ +// time/realtime variable kinds. The per-direction split makes those +// illegal combinations structurally unrepresentable, mirroring the +// VariableDeclaration kind×packing×signedness dissolution). +// +// - AnsiInputPort { net: AnsiNetPortType, names: List } +// — input ports are net-typed only (the spec forbids +// `input reg`); names form a §A.1.3 list_of_port_identifiers. +// - AnsiOutputNetPort { type_kind: OutputPortAnsiNetTypeKind, +// names: List } +// — output net-form (§A.1.3 output_declaration alternative 1: +// `output [net_type] [signed] [range] list_of_port_identifiers`). +// The 2-way OutputPortAnsiNetTypeKind partition (explicit +// non-trireg net-type / no-net-type) covers the spec alternatives; +// names use plain port_identifiers — NO per-port initializers +// structurally representable. +// - AnsiOutputVariablePort { type_kind: OutputPortAnsiVariableTypeKind, +// names: List } +// — output variable-form (§A.1.3 output_declaration alternatives +// 2+3: `output [reg] [signed] [range]` / +// `output output_variable_type` followed by +// list_of_variable_port_identifiers). The 3-way +// OutputPortAnsiVariableTypeKind partition (reg / integer / time) +// covers spec-admissible variable kinds; names use +// list_of_variable_port_identifiers with optional per-port +// initializers via AnsiOutputPortDeclarator. Real/realtime +// outputs excluded per §12.3.3. The net-vs-variable AnsiOutputPort +// split corrected the prior unified-declarator shape per openai-pro +// REQUEST_CHANGES on PR #3176 sha 98953d5f — the prior shape +// admitted spec-illegal `output wire y = 1'b0` net-output-with- +// initializer states. +// - AnsiInoutPort { net: AnsiNetPortType, names: List } +// — inout ports are net-typed only (bidirectional requires +// nets; `inout reg` is a spec violation); names form a +// §A.1.3 list_of_port_identifiers. +// +// All three variants gained an `attributes: AttributeInstanceClause` +// prefix and a non-empty `names` list at sha 4ccc6267 per openai-pro +// REQUEST_CHANGES (Layer-Model BLOCKING) — the prior single-name-no- +// attributes shape dropped §A.1.3 attribute-instance and +// list_of_port_identifiers declaration-boundary facts. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.3.3 admits exactly +// these three direction-bearing ANSI-port forms; SystemVerilog +// `ref` ports would EDIT this Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every ANSI-port consumer branches on +// direction × type-kind to dispatch emission / type-check +// legality / drive net-vs-reg-assignment-legality; shared +// classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to a uniform +// `{ direction: PortDirection, name: Symbol, type_payload: +// }` ratifies spec-forbidden +// combinations (Input + reg-typed payload, Inout + integer- +// typed payload, etc.) — the product-axis admits illegal states +// this per-direction Disj dissolves. INVARIANTS P2 illegal- +// states-unrepresentable. +// 3. Algebraic form — N/A by construction: the three direction- +// bearing ANSI forms are the spec's primitive direction × type +// admissibility table — not a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single ANSI port is EXACTLY ONE +// direction variant; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: AnsiInputPort and AnsiInoutPort +// carry `net: AnsiNetPortType` (net-only, 2-variant: explicit +// non-trireg-kind + no-net-type); AnsiOutputNetPort carries +// `type_kind: OutputPortAnsiNetTypeKind` (2-variant net forms) +// + `names: List`; AnsiOutputVariablePort carries +// `type_kind: OutputPortAnsiVariableTypeKind` (3-variant +// variable forms: reg/integer/time) + `names: List< +// AnsiOutputPortDeclarator>` (with optional initializers). The +// payload types differ structurally — NOT one generic +// `F` projection over a single source set +// (Practice 7). +// Terminal: the closed four-way Verilog ANSI-port direction-kind +// classifier; illegal direction × type-kind combinations are +// unrepresentable by construction. +// As of sha 7b7dd0b54+ (codex L3563 BLOCKING on PR #3176): the +// `attributes: AttributeInstanceClause` field has been STRIPPED from +// all three variants below — AnsiPortDeclaration is now the +// attribute-FREE per-spec port declaration payload, reusable at: +// - ANSI header position via AnsiHeaderPort wrapper (carries the +// §A.1.3 outer `{attribute_instance}` prefix) +// - non-ANSI body position via NonAnsiBodyPortDeclarationItem +// (whose outer `attributes` field is the single authority) +// This dissolves the §A.1.3 double-authority that arose when both +// the outer wrapper AND the inner AnsiPortDeclaration carried +// attribute slots for one syntactic site (same shape as the +// OrderedPortConnection / NamedPortConnection split that resolved +// the analogous PortConnectionActual double-authority). +type AnsiPortDeclaration + = AnsiInputPort { + net: AnsiNetPortType + // 🟡 spec-non-empty (§A.1.3 list_of_port_identifiers) — deferred + // to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note below. + names: List + } + | AnsiOutputNetPort { + // Spec §A.1.3 output_declaration form 1: `output [net_type] + // [signed] [range] list_of_port_identifiers`. Net-form outputs + // use plain port_identifiers — NO per-port initializers + // structurally representable (openai-pro REQUEST_CHANGES on + // PR #3176 sha 98953d5f: prior unified AnsiOutputPort admitted + // `output wire y = 1'b0` which the spec forbids). + type_kind: OutputPortAnsiNetTypeKind + // 🟡 spec-non-empty (§A.1.3 list_of_port_identifiers) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note below. + names: List + } + | AnsiOutputVariablePort { + // Spec §A.1.3 output_declaration forms 2+3: `output [reg] + // [signed] [range] list_of_variable_port_identifiers` / + // `output output_variable_type list_of_variable_port_ + // identifiers`. Variable-form outputs use + // list_of_variable_port_identifiers — each port_identifier + // admits an OPTIONAL initializer expression. Real/realtime + // excluded per §12.3.3. + type_kind: OutputPortAnsiVariableTypeKind + // 🟡 spec-non-empty (§A.1.3 list_of_variable_port_identifiers) + // — deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note below. + names: List + } + | AnsiInoutPort { + net: AnsiNetPortType + // 🟡 spec-non-empty (§A.1.3 list_of_port_identifiers) — deferred + // to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note below. + names: List + } + + +// ───────────────────────────────────────────────────────────────────── +// AnsiHeaderPort — one ANSI-style module-header port entry (IEEE +// 1364-2005 §12.3.3 / §A.1.3). Conj wrapper providing the §A.1.3 +// `{attribute_instance}` outer prefix around the attribute-free +// AnsiPortDeclaration payload. Sibling pattern of +// OrderedPortConnection / NamedPortConnection — outer-attribute +// placement matching the spec grammar's prefix position. +// +// Per §A.1.3 grammar: +// +// port_declaration ::= {attribute_instance} +// (input_declaration | output_declaration +// | inout_declaration) +// +// the attributes live at the port_declaration level, ABOVE the +// direction-specific declaration sub-form. This wrapper provides +// that level for ANSI header use; the same AnsiPortDeclaration +// payload is reused at non-ANSI body position via +// NonAnsiBodyPortDeclarationItem (whose outer `attributes` field +// is the single authority for that position). Conj record (no +// Practice-4 ledger). +// +// - attributes the optional {attribute_instance} prefix per +// §A.1.3 (reuses AttributeInstanceClause). +// - decl the direction-bearing port declaration payload +// (AnsiPortDeclaration). Attribute-free. +type AnsiHeaderPort { + attributes: AttributeInstanceClause + decl: AnsiPortDeclaration +} + + +// ───────────────────────────────────────────────────────────────────── +// AnsiOutputPortDeclarator — one (name, optional-initializer) entry +// in an ANSI output port's list_of_variable_port_identifiers (IEEE +// 1364-2005 §A.1.3 / §A.2.3). Per spec list_of_variable_port_ +// identifiers ::= port_identifier [ = constant_expression ] { , +// port_identifier [ = constant_expression ] } — each output-port +// identifier admits an OPTIONAL initializer. Only ANSI output ports +// reach this carrier; input/inout ports use plain `List` +// because the spec form list_of_port_identifiers does NOT admit +// per-port initializers. Conj record (no Practice-4 ledger). +// +// - name the declared port identifier (K-1-opaque +// Symbol). +// - initializer the optional initializer clause (reuses +// VariableInitializerClause); structurally +// optional per the §A.2.3 brackets. +type AnsiOutputPortDeclarator { + name: Symbol + initializer: VariableInitializerClause +} + + +// (The standalone ModulePortsList Disj has been dissolved into +// VerilogModule's own per-style Disj — VerilogModule is now +// NonAnsiVerilogModule | AnsiVerilogModule, each variant carrying its +// own header-port list type AND its own admissible body-items list +// type. This lifts the port-style choice from the port-list carrier +// to the module-as-a-whole carrier, making "ANSI port-list module +// with body PortDeclarationItem" structurally unrepresentable — +// INVARIANTS P2 illegal-states-unrepresentable fix per codex BLOCKING +// on PR #3176 2026-05-16. The §12.3.4 module-style partition is now +// the dimensional axis of VerilogModule itself; the rationale +// formerly housed here is folded into VerilogModule's ledger below.) + + +// ───────────────────────────────────────────────────────────────────── +// ParameterTypeKind — the closed Verilog parameter-type classifier +// (IEEE 1364-2005 §A.2.1.1). A parameter declaration's type is +// either UNTYPED (inferring from the default-value's type per §3.10) +// OR an explicit parameter_type (integer / real / realtime / time). +// The explicit-type form FORBIDS [signed]/[range] modifiers per +// spec — those apply only to the untyped form. +// +// - UntypedParameter { packing: PackingShape, signedness: Signedness } +// — `parameter WIDTH = 8;`, `parameter signed [3:0] X = 4'sb1100;` +// The packing + signedness modifiers apply ONLY to this form. +// - IntegerParameter — `parameter integer N = 4;` +// - RealParameter — `parameter real PI = 3.14;` +// - TimeParameter — `parameter time T = 10;` +// - RealTimeParameter — `parameter realtime RT = 1.5;` +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.2.1.1 admits exactly +// this five-way parameter-type partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟡 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). Ledger — five patterns +// attempted: +// 1. Fact placement — FAILS: every parameter consumer (override- +// conversion per §12.1.3, type-check legality, emission) +// reads the type kind uniformly; shared classifier. +// 2. Variant-is-data — FAILS: collapsing to a uniform `{ kind: +// Symbol, packing?: PackingShape, signedness?: Signedness }` +// ratifies spec-forbidden states like "IntegerParameter with +// signed [3:0]" (per spec the explicit-type forms forbid +// range/signedness modifiers). Disj-with-heterogeneous- +// payloads makes the per-kind admissibility structural. +// 3. Algebraic form — PARTIAL: each variant grounds in a std/ +// algebra structure (UntypedParameter → polymorphic per the +// default-value's inferred type; IntegerParameter → +// OrderedRing>; RealParameter / RealTimeParameter → +// ApproximateField; TimeParameter → Semiring>). +// D2-deferred per "Owned ELSEWHERE". +// 4. Dimensional — FAILS: a single parameter has EXACTLY ONE +// type kind; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: heterogeneous payload-presence +// (UntypedParameter carries packing+signedness; the typed +// kinds carry neither) — NOT one generic `F` / projection +// over a single source set (Practice 7). Mirror of body-side +// VariableDeclaration's kind × packing × signedness +// dissolution. +// Terminal: the closed five-way Verilog parameter-type classifier. +// +// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md +// merged on origin/main): under the pre-#3200 consumer-DEPENDENT +// GREEN rule this Disj was correctly GREEN. Under the post-#3200 +// consumer-INDEPENDENT rule this is 🟡 YELLOW because a namable +// richer source EXISTS — same {storage-class, width, signedness, +// algebra-grounding} matrix as VariableDeclaration / OutputPortAnsi +// VariableTypeKind (compile-time-constant variant at parameter +// position): +// UntypedParameter: packing-payload + signedness-payload +// (inferred from default-value expression) +// IntegerParameter: same as IntegerVariable +// RealParameter: same as RealVariable +// TimeParameter: same as TimeVariable +// RealTimeParameter: same as RealTimeVariable (aliased to Real) +// Trigger: first consumer of parameter-storage / algebra semantics +// (D2 inhabitance pathway — shared with the +// VariableDeclaration / OutputPortAnsiVariableTypeKind family). +// Obligation: the first meaning-consumer owes structural +// decomposition into the same storage-class matrix used for +// VariableDeclaration — single-authority across the family. +type ParameterTypeKind + = UntypedParameter { packing: PackingShape, signedness: Signedness } + | IntegerParameter + | RealParameter + | TimeParameter + | RealTimeParameter + + +// ───────────────────────────────────────────────────────────────────── +// 🟡 TRACKED-SCAFFOLD: spec-non-empty list fields (relayed +// disposition from T-4 mgr vivid-carp-207 msg_30a7ec7c, 2026-05-16). +// +// Twenty-six sites in this file carry `List` payloads where IEEE +// 1364-2005 requires AT LEAST ONE entry — the spec-illegal empty +// state is structurally representable, the same INVARIANTS P2 +// illegal-states-unrepresentable concern codex / openai-pro +// correctly flagged. The MOTIVATION is real and spec-grounded. The +// CANONICAL FIX is NOT a worker-minted `NonEmptyList` generic +// carrier: +// +// - `docs/coercion-design.md` RQ-3 (ratified): "refinements of +// base containers, NOT separate inhabitant families. +// `NonEmptyList = List where non_empty`. Separate +// inhabitants would grow the authority surface." A hand-rolled +// `NonEmptyList { head: T, tail: List }` IS a separate +// inhabitant family and breaks the ratified Vec coercion. +// - `std/collection.dag` (merged on main) DEFERS its entire +// finite-cardinality / refinement layer to "Wave-A2 — TRACKED +// SCAFFOLD (🟡)". The `List where non_empty` refinement IS +// that deferred layer. +// - This file's frozen scaffold header neither Owns nor Consumes +// `std/collection.dag`. Minting a parallel non-empty carrier in +// a leaf language probe would be a 5-language parallel- +// declaration precedent — the v3 cross-layer spine-drift this +// T-4 directive exists to prevent. +// +// SANCTIONED DEFERRAL (the deferral middle-path, mirroring +// collection.dag's own Wave-A2 scaffold + the ptx #3170 / spice #3168 +// inhabitance-deferral pattern): +// - Each of the twenty-six spec-non-empty sites keeps `List` for now. +// - Each site carries a back-pointer comment to THIS shared note. +// - The empty-list illegal state is a PRODUCER-SIDE invariant +// pending the refinement substrate landing. +// - DISSOLUTION TRIGGER: when `std/collection.dag` Wave-A2 lands the +// non-empty refinement, the twenty-four sites adopt +// `List where non_empty` uniformly in one sweep — single- +// authority preserved. +// +// The twenty-six spec-non-empty sites (back-pointers to this note): +// (sites 25-26 below — VerilogModule per-style header_ports) +// 1. NetDeclaration.NonTriregIdentifierForm.identifiers (§A.2.1.3) +// 2. NetDeclaration.NonTriregAssignForm.assignments (§A.2.1.3) +// 3. NetDeclaration.TriregIdentifierForm.identifiers (§A.2.1.3) +// 4. NetDeclaration.TriregAssignForm.assignments (§A.2.1.3) +// 5. VariableDeclaration.{Reg,Integer,Real,Time,RealTime}Variable.declarators +// (§A.2.4 / §7.4) +// 6. ParameterDeclaration.assignments (§A.2.1.1) +// 7. LocalParameterDeclaration.assignments (§A.2.1.1) +// 8. SpecparamDeclaration.assignments (§A.2.1.1) +// 9. ModuleParameters.parameters (§12.1) +// 10. AlwaysBlockSensitivity.ExplicitEventList.items (§9.7.2) +// 11. ParameterOverrides.OrderedParameterOverrides.actuals (§12.1.3) +// 12. ParameterOverrides.NamedParameterOverrides.overrides (§12.1.3) +// 13. ContinuousAssign.assignments (§6.1) +// 14. ModuleInstantiation.instances (§A.4.1.1) +// 15. PortConnections.PositionalConnections.actuals (§A.4.1.1) +// 16. PortConnections.NamedConnections.connections (§A.4.1.1) +// 17. DefparamDeclaration.assignments (§A.2.5) +// 18. EventDeclaration.event_names (§A.2.1.4) +// 19. GenvarDeclaration.genvar_names (§A.2.1.1) +// 20. UdpInstantiation.instances (§A.5.2) +// (Former site 21 PortDeclaration.names was DISSOLVED at sha +// cb028c7d+ — PortDeclaration itself dissolved into AnsiPortDeclaration +// per openai-pro REQUEST_CHANGES; the §A.2.1.2 list_of_port_identifiers +// fact is now uniformly carried by AnsiPortDeclaration's per-direction +// variants at sites 21-24 below.) +// 21. AnsiPortDeclaration.AnsiInputPort.names (§A.1.3) +// 22. AnsiPortDeclaration.AnsiOutputNetPort.names (§A.1.3) +// 23. AnsiPortDeclaration.AnsiOutputVariablePort.names (§A.1.3) +// 24. AnsiPortDeclaration.AnsiInoutPort.names (§A.1.3) +// 25. VerilogModule.NonAnsiVerilogModule.header_ports (§12.3.4) +// 26. VerilogModule.AnsiVerilogModule.header_ports (§12.3.4) +// +// Sites previously numbered 7-9 added 2026-05-16 per codex +// REQUEST_CHANGES on PR #3176 at sha f87fdf189; site previously 10 +// added 2026-05-16 per codex BLOCKING on PR #3176 at sha bcc6b5f89 +// (ContinuousAssign restructured to carry drive_strength + delay + +// list_of_net_assignments per §6.1, with the non-empty assignments +// list deferred under the same RQ-3 disposition); site previously 11 +// added 2026-05-16 per codex BLOCKING on PR #3176 at sha 2bf0024ba +// (ModuleInstantiation restructured to carry shared module_name + +// parameter_overrides + non-empty instances per §A.4.1.1 multi- +// instance form). Sites 1-4 (formerly the single site +// `NetDeclaration.declarators`) added 2026-05-16 per openai-pro +// REQUEST_CHANGES on PR #3176 at sha 6f587e6c — NetDeclaration +// dissolved into the IEEE 1364-2005 §A.2.1.3 four-way +// {trireg?}×{form} structural Disj making spec-impossible states +// (drive_strength on the identifier-only form, charge_strength on +// a non-trireg form, mixed init/non-init declarator lists, +// identifier-only-with-initializer, assignment-form-without- +// initializer) unrepresentable; the four per-variant +// list_of_net_decl_assignments / list_of_net_identifiers fields +// inherit the §A.2.1.3 spec-non-empty constraint and ride the same +// RQ-3 deferral. Sites 15-20 added 2026-05-16 per openai-pro +// REQUEST_CHANGES on PR #3176 at sha 1eb241a2 (inline BLOCKING +// findings at lines 2156 / 2315 / 2604): PortConnections gained the +// NoPortConnections nullary variant — the §A.4.1.1 empty `()` +// connection-list form is now structurally distinct from non-empty +// ordered/named lists (P2 representation-duality dissolution); the +// two non-empty inner lists ride the same RQ-3 deferral. +// DefparamDeclaration / EventDeclaration / GenvarDeclaration each +// gained a non-empty list of per-entry sub-records (new +// DefparamAssignment Conj for §A.2.5 list_of_defparam_assignments; +// `event_declarators: List` for §A.2.1.4 +// list_of_event_identifiers (later sha 4ccc6267 added per-identifier +// dimensions via EventDeclarator); `genvar_names: List` for +// §A.2.1.1 list_of_genvar_identifiers) — restoring the spec +// statement-boundary lost by the prior singular-entry shape. UdpInstantiation refactored to the +// same shared-header + non-empty-instance-list pattern as +// ModuleInstantiation, per §A.5.2 `udp_identifier [drive_strength] +// [delay2] udp_instance { , udp_instance } ;` — shared +// (udp_name, drive_strength, delay) clause + per-instance +// (instance_name, body_lexeme) UdpInstance entries. Codex's / +// openai-pro's motivation is spec-correct in each case; the FORM +// is the deferred refinement, not a verilog-local mint. Site 21 +// added 2026-05-16 per openai-pro REQUEST_CHANGES on PR #3176 at +// sha cba903a3e (inline BLOCKING at line 1429): PortDeclaration +// reshape from singular-name to list-form mirrors the Defparam/ +// Event/Genvar list-form precedent under §A.2.1.2 list_of_port_ +// identifiers; the non-empty list rides the same RQ-3 deferral. +// Sites 22-24 added 2026-05-16 per openai-pro REQUEST_CHANGES on +// PR #3176 at sha 4ccc6267 (Layer-Model BLOCKING on +// AnsiPortDeclaration per-single-name carrier): the three ANSI port +// direction variants reshape from `name: Symbol` singletons to +// non-empty name-lists (AnsiInputPort/AnsiInoutPort use +// `List` per §A.1.3 list_of_port_identifiers; AnsiOutputPort +// uses `List` per §A.1.3 +// list_of_variable_port_identifiers — output variable-ports admit +// per-port initializers via the existing VariableInitializerClause +// Disj). All three new non-empty lists ride the same RQ-3 / +// std/collection.dag Wave-A2 deferral; no verilog-local +// NonEmptyList mint. Sites 25-26 added 2026-05-16 per openai-pro +// REQUEST_CHANGES on PR #3176 at sha 7709c9968 (inline BLOCKING at +// line 3525 — VerilogModule header_ports List representation- +// duality): the no-ports module form (`module M; ... endmodule`) +// was representable as either NonAnsi{header_ports=[]} or +// Ansi{header_ports=[]} (P2 representation-duality), AND empty +// non-ANSI header with body port_declaration items admitted a spec- +// illegal §12.3.4 state (body port_declarations reference header +// port names; no header ports → no body port_declarations). +// Resolution: VerilogModule gained a NoPortsModule style-neutral +// variant (3-way Disj) with `items: List` (no body +// port_declaration variants representable). The remaining +// NonAnsiVerilogModule + AnsiVerilogModule variants now have +// spec-non-empty header_ports — sites 25-26 — riding the same +// RQ-3 deferral. + + +// ───────────────────────────────────────────────────────────────────── +// ParameterAssignment — one (name, default-value) pair in a +// parameter_declaration's list_of_param_assignments (IEEE 1364-2005 +// §A.2.4 / §3.10). A single declaration like `parameter WIDTH = 8, +// DEPTH = 16;` carries TWO ParameterAssignments. Conj record (no +// Practice-4 ledger). +// +// - name the parameter identifier (K-1-opaque Symbol) +// - default_lexeme the default value as a verbatim expression +// lexeme; per spec every parameter declaration +// requires a default value (unlike net/variable +// decls), so this field is non-empty in a +// well-formed declaration. Sub-grammar deferred +// to T-4 LanguageModel. +type ParameterAssignment { + name: Symbol + default_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// ParameterDeclaration — a Verilog compile-time constant declaration +// (`parameter WIDTH = 8;`, `parameter signed [3:0] X = 4'sb1100;`, +// `parameter integer N = 4;`, `parameter WIDTH = 8, DEPTH = 16;`). +// IEEE 1364-2005 §3.10 / §A.2.1.1. Conj record (no Practice-4 +// ledger). +// +// - type_kind which parameter-type form (ParameterTypeKind +// Disj — UntypedParameter carries packing + +// signedness; the typed forms IntegerParameter +// / RealParameter / TimeParameter / +// RealTimeParameter carry neither per spec +// §A.2.1.1). +// - assignments the list_of_param_assignments — each +// ParameterAssignment carries name + +// default_lexeme. Per spec a parameter +// declaration must have at least one assignment. +// +// Multi-assignment + type_kind added per codex BLOCKING on PR #3176 +// 2026-05-16 — the prior {name, default_lexeme} shape collapsed the +// spec's type/range/signedness facts that govern §12.1.3 override +// conversion (when an instantiation #(...) overrides a parameter, +// the spec defines conversion semantics based on the declared type; +// without these facts the conversion is unspecified). +type ParameterDeclaration { + type_kind: ParameterTypeKind + // 🟡 spec-non-empty (§A.2.1.1) — deferred to std/collection.dag + // Wave-A2 refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List +} + + +// ───────────────────────────────────────────────────────────────────── +// SensitivityItem — one entry in an always-block's event-control list +// (`posedge clk`, `negedge rst`, `posedge (a & b)`, bare expression). +// IEEE 1364-2005 §9.7.2. Conj record (no Practice-4 ledger). +// +// - trigger which edge / level-sensitivity +// - event_expression_lexeme the expression the trigger watches +// as a verbatim lexeme. Per spec +// §9.7.2 the event_expression can be +// ANY expression (identifier, bit- +// select, arithmetic combination), not +// just a bare identifier — corrected +// 2026-05-16 per codex BLOCKING on +// PR #3176 (the prior `signal: Symbol` +// narrowed event expressions to +// identifier references, excluding +// valid syntax). Sub-grammar deferred +// to the T-4 LanguageModel via the +// established body_lexeme precedent. +type SensitivityItem { + trigger: EdgeTrigger + event_expression_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// NetAssignment — one (net_lvalue, expression) pair in a +// continuous_assign's list_of_net_assignments (IEEE 1364-2005 §6.1 + +// §A.6.1). A single `assign net1 = expr1, net2 = expr2;` carries TWO +// NetAssignments. Conj record (no Practice-4 ledger). +// +// - lhs_lexeme the destination net_lvalue as a verbatim +// lexeme (identifier ref, bit/part-select, or +// concatenation/replication of net_lvalues per +// §6.1). Sub-grammar deferred to T-4 +// LanguageModel. +// - rhs_lexeme the right-hand-side expression as a verbatim +// lexeme. +type NetAssignment { + lhs_lexeme: String + rhs_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// ContinuousAssign — a Verilog continuous-assignment statement +// (`assign net = expr;`, `assign (strong0, weak1) #5 a = e1, b = e2;`). +// IEEE 1364-2005 §6.1 + §A.6.1. Conj record (no Practice-4 ledger). +// +// Per spec §6.1 a continuous_assign carries an optional drive_strength, +// an optional delay3, and a non-empty list_of_net_assignments — +// declaration-boundary facts the prior single-(lhs,rhs)-pair shape +// collapsed (codex BLOCKING on PR #3176 2026-05-16). +// +// - drive_strength optional drive_strength clause (`(strong0, +// weak1)`); reuses the DriveStrengthClause Disj +// shared with NetDeclaration. +// - delay optional delay3 clause (`#5`, `#(2:3:4)`); +// reuses the DelayClause Disj shared with +// NetDeclaration. +// - assignments the list_of_net_assignments per spec §A.6.1 +// — each NetAssignment carries a net_lvalue +// lexeme + expression lexeme. +type ContinuousAssign { + drive_strength: DriveStrengthClause + delay: DelayClause + // ContinuousAssign.assignments: 🟡 spec-non-empty (§6.1) — + // deferred to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List +} + + +// ───────────────────────────────────────────────────────────────────── +// AlwaysBlock — a Verilog `always @(...)` block (IEEE 1364-2005 §9.9). +// Conj record (no Practice-4 ledger). +// +// - sensitivity the event-control specification (closed Disj +// over the three IEEE 1364-2005 §9.7.2 forms: +// no event control / implicit `@*` / explicit +// event list) +// - body_lexeme the procedural body (begin…end or single +// statement) as a verbatim lexeme (sub-grammar +// deferred to the T-4 LanguageModel expression / +// statement productions; `parse ∘ emit` is +// identity on the textual surface) +// +// Per the IN-B PROBE FINDING above, this carrier IS the Loop-step + +// Bind-chain unit: the always-block's ONE TRIGGER is a bounded step +// (A2 footnote); the iteration across triggers is the simulator/ +// synthesizer's coordination boundary; the sequential composition of +// statements inside the body is the Bind chain. +type AlwaysBlock { + sensitivity: AlwaysBlockSensitivity + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// AlwaysBlockSensitivity — the closed Verilog event-control +// classifier for an `always` block (IEEE 1364-2005 §9.7.2). The spec +// admits exactly THREE event-control forms; modeling sensitivity as +// `List` collapsed the implicit `@*` form with both +// "no event control" (empty list) and "explicit event list" (non- +// empty) — the codex BLOCKING review on PR #3176 surfaced the gap. +// This Disj-with-named-payloads makes each form structurally distinct +// per INVARIANTS P1 modeling-faithfulness + P2 single-authority. +// +// - NoEventControl — bare `always begin ... end` with no +// `@(...)` — the body uses internal +// delay control (`#10 ...`) for timing. +// Rare in practice; legal per spec. +// - ImplicitAtStar — `always @*` or `always @(*)` — +// implicit sensitivity list covering +// ALL signals read in the body (the +// §9.7.2 implicit-event-control form; +// recommended for combinational logic +// to avoid manual list errors). The +// implicit set is COMPUTED FROM THE +// BODY at synthesis / simulation time; +// this variant carries no payload — +// the body itself is the authority for +// which signals trigger the always. +// - ExplicitEventList — `always @(event_expression)` — +// explicit list of edge-triggered or +// level-sensitive entries (`posedge +// clk, negedge rst, data`). The +// `items` payload is the list of +// `SensitivityItem` entries. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §9.7.2 admits exactly +// these three event-control forms; a fourth would be a future +// language-version change requiring edit under the L-2 pin +// discipline. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every always-block consumer (the +// synthesis dispatch for flip-flop vs latch vs combinational +// inference, the implicit-set-from-body extraction, the +// explicit-list emission) branches on the form uniformly; +// shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to +// `{ items: List }` (the prior model) +// conflates NoEventControl (empty list) with ExplicitEventList +// (empty list is technically possible) AND has NO +// representation for ImplicitAtStar — exactly the codex +// BLOCKING finding. The Disj-with-heterogeneous-payloads is +// the dissolution: each variant carries exactly the structural +// data its form admits. +// 3. Algebraic form — N/A by construction: the three forms are +// the IEEE 1364-2005 spec's primitive event-control partition; +// they do not trace to a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single `always` block has EXACTLY +// ONE event-control form; mutually-exclusive alternatives +// (per spec: a single `always` cannot have both an implicit +// and explicit list). +// 5. Parameterized family — FAILS: the three variants carry +// structurally heterogeneous payloads (NoEventControl is +// nullary; ImplicitAtStar is a nullary marker — the implicit +// set is computed from the body, not stored; ExplicitEventList +// carries a `List`) — NOT one generic `F` +// / projection over a separately-declared source set +// (Practice 7). +// Terminal: the closed three-way Verilog always-block event-control +// classifier of the IEEE 1364-2005 spec. +type AlwaysBlockSensitivity + = NoEventControl + | ImplicitAtStar + // ExplicitEventList.items: 🟡 spec-non-empty (§9.7.2) — deferred to + // std/collection.dag Wave-A2 refinement; see shared TRACKED-SCAFFOLD + // note above. (NoEventControl already covers the no-`@(...)` form.) + | ExplicitEventList { items: List } + + +// ───────────────────────────────────────────────────────────────────── +// InitialBlock — a Verilog `initial` block (IEEE 1364-2005 §9.9). +// Executes its body ONCE at simulation time 0. Conj record (no +// Practice-4 ledger). +// +// - body_lexeme the procedural body as a verbatim lexeme (sub- +// grammar deferred — same shape as `AlwaysBlock. +// body_lexeme`) +// +// `initial` is admitted here for the simulation-time-zero +// initialization case (the synthesizable-subset uses register-reset +// in `always @(posedge clk)` blocks instead); per the PROBE LIMITS +// header note the testbench-only `$display` / `$finish` system tasks +// inside `initial` are out of scope. +type InitialBlock { + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// PortConnectionActual — the closed Verilog port-connection-actual +// classifier (IEEE 1364-2005 §12.1.2). The spec admits a port- +// connection's actual to be any of three forms: a full expression +// (including identifier references, literals, bit-selects, arithmetic +// — `.en(1'b1)`, `.data(bus[3:0])`, `.sum(a + b)`), or BLANK (an +// explicitly unconnected port — `.unused()`). Modeling the actual as +// a bare `Symbol` (the prior form) narrowed it to identifier +// references only, excluding valid IEEE 1364-2005 syntax — openai-pro +// REQUEST_CHANGES on PR #3176 surfaced this gap. INVARIANTS P1 +// modeling-faithfulness violation (the spec's port-connection-actual +// partition is wider than just identifiers). +// +// - ExpressionConnection { expression_lexeme: String } +// — the connection-actual is a Verilog expression carried as +// a verbatim lexeme (sub-grammar deferred to the T-4 +// LanguageModel grammar productions; the spice.dag +// `SpiceValue.lexeme` precedent — `parse ∘ emit` is identity +// on the textual surface; the expression-typed-fact lands +// when the bundled expression productions land). Covers +// identifier references (`.en(clk)`), literals (`.en(1'b1)`), +// bit-selects (`.data(bus[3:0])`), and arithmetic +// (`.sum(a + b)`). +// - BlankConnection +// — `.port_name()` — an explicitly unconnected port (spec +// §12.1.2 admits this form for documenting that a named port +// is intentionally left unconnected); nullary marker. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.1.2 admits these two +// actual-forms; a third would be an edit to THIS declaration under +// the L-2 pin discipline. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every port-connection emitter and +// every dependency-graph walker reads the actual form +// uniformly (a blank connection contributes no dependency; a +// non-blank actual contributes the expression's signal +// references); shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to `{ expression_lexeme: +// String }` where blank = empty-string conflates "intentionally +// blank" with "expression is empty string" (the lexeme `""` is +// not a valid Verilog expression); the Disj-with-named-payloads +// makes blank vs expression structurally distinct. +// 3. Algebraic form — N/A by construction: the two actual-forms +// are the IEEE 1364-2005 spec's port-connection-actual partition; +// they do not trace to a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single port-connection actual is +// EXACTLY ONE form; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: ExpressionConnection carries a +// lexeme payload; BlankConnection is nullary — structurally +// heterogeneous, NOT one generic `F` / projection over a +// separately-declared source set (Practice 7). The expression +// sub-grammar is owned by the bundled T-4 LanguageModel; this +// vocabulary slice declares the actual-form partition only. +// Terminal: the closed two-way Verilog port-connection-actual +// classifier; the expression sub-grammar is deferred to T-4 +// LanguageModel. +type PortConnectionActual + = ExpressionConnection { expression_lexeme: String } + | BlankConnection + + +// ───────────────────────────────────────────────────────────────────── +// OrderedPortConnection — one element of a positional port-binding +// list (IEEE 1364-2005 §A.4.1.1): +// +// ordered_port_connection ::= { attribute_instance } [ expression ] +// +// The §A.4.1.1 grammar places the attribute_instance prefix at the +// ordered_port_connection element level — the same level where +// named_port_connection carries its attribute prefix. The earlier +// shape (sha cba903a3e) put attributes ON each PortConnectionActual +// variant, which then double-authoritied named connections +// (NamedPortConnection.attributes + actual.attributes both present +// for one syntactic binding) — openai-pro REQUEST_CHANGES on +// PR #3176 sha 4ccc6267 flagged the double-authority. Resolution: +// strip attributes from PortConnectionActual (the inner blank-vs- +// expression Disj is shared between ordered and named forms; +// attributes live at the OUTER wrapping level) and wrap the +// positional case in this OrderedPortConnection Conj that mirrors +// NamedPortConnection's outer-attribute placement. +// Conj record (no Practice-4 ledger). +// +// - attributes the optional attribute_instance prefix per +// §A.4.1.1 (reuses AttributeInstanceClause). +// - actual the connection's expression-or-blank inner form +// (PortConnectionActual). +type OrderedPortConnection { + attributes: AttributeInstanceClause + actual: PortConnectionActual +} + + +// ───────────────────────────────────────────────────────────────────── +// NamedPortConnection — one named connection in a module-instance's +// port-binding list (IEEE 1364-2005 §12.1.2, named form). Conj record +// (no Practice-4 ledger). +// +// - port the formal port name on the instantiated module +// (K-1-opaque Symbol; resolved through the namespace +// to the matching `PortDeclaration` on the target +// module) +// - actual the connection's actual value — an expression +// (carried as a verbatim lexeme per the closed +// PortConnectionActual classifier above) or a blank +// `.port_name()` marker. The prior `signal: Symbol` +// narrowed this to identifier references only — +// corrected per openai-pro REQUEST_CHANGES on +// PR #3176 to admit the full spec-mandated set of +// expression actuals + blank. +type NamedPortConnection { + attributes: AttributeInstanceClause + port: Symbol + actual: PortConnectionActual +} + + +// ───────────────────────────────────────────────────────────────────── +// PortConnections — the closed Verilog port-binding-list form +// classifier (IEEE 1364-2005 §12.1.2 / §A.4.1.1). The spec admits +// THREE forms per the §A.4.1.1 grammar: +// +// module_instance ::= name_of_instance ( [list_of_port_connections] ) ; +// list_of_port_connections ::= +// ordered_port_connection { , ordered_port_connection } +// | named_port_connection { , named_port_connection } +// +// where the `[list_of_port_connections]` brackets make the entire +// connection list OPTIONAL (`Adder a1 ();` — empty parens — is legal +// spec syntax), and when present the inner list is a NON-EMPTY list +// of ordered_port_connection OR a NON-EMPTY list of named_port_ +// connection — mixing the two is forbidden (`Adder a1 (x, .b(y))` +// is a syntax error). +// +// The empty `()` form is modeled as a STRUCTURAL `NoPortConnections` +// variant rather than as an `[]` empty list inside either of the +// other two variants — otherwise the empty connection-list state is +// representable TWO ways (positional-empty vs named-empty) and +// violates INVARIANTS P2 representation-duality (openai-pro +// REQUEST_CHANGES on PR #3176 2026-05-16 at line 2156). Sibling +// non-empty lists ride the established RQ-3 / std/collection.dag +// Wave-A2 `List where non_empty` deferral (see shared TRACKED- +// SCAFFOLD note above). +// +// - NoPortConnections — `Adder a1 ();` — empty parens; the +// spec's "[list_of_port_connections]" +// bracket-absent form. +// - PositionalConnections — `Adder a1 (sig1, sig2, sig3)` — +// actuals listed in declaration-order +// position; the i-th signal binds to +// the i-th port. Spec §12.1.2 +// "Ordered port connections". The +// `actuals` list is spec-non-empty. +// - NamedConnections — `Adder a1 (.a(x), .b(y), .sum(z))` +// — actuals explicitly bound to +// formals by name. Spec §12.1.2 +// "Named port connections". The +// `connections` list is spec-non-empty. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.4.1.1 admits exactly +// these three forms; a fourth would be an edit to THIS declaration +// under the L-2 pin discipline (SystemVerilog adds `.port` shorthand +// for `.port(port)` and `.*` for "connect all matching names" — a +// future language-version model would EDIT this Disj explicitly). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every instance-emission consumer and +// every port-binding resolver reads the connection form +// uniformly to know whether to emit `()`, align by position, +// or align by name; shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing the variants to a uniform +// `List` where each entry has `kind: Form` +// ratifies the illegal state "mixed positional+named within +// one instance" — exactly the spec-forbidden form. Replacing +// `NoPortConnections` with empty inner lists ratifies the +// double-spelling of `()`. Disj-with-heterogeneous-payloads- +// plus-nullary-empty-variant makes both partitions structural. +// 3. Algebraic form — N/A by construction: the three forms are +// the IEEE 1364-2005 §A.4.1.1 spec's primitive port-connection +// partition; they do not trace to a richer std/ algebraic +// structure. +// 4. Dimensional — FAILS: a single module instance is EXACTLY +// ONE form; mutually-exclusive alternatives. (Mixed-form and +// multi-form-per-instance are syntax errors per spec.) +// 5. Parameterized family — FAILS: the three variants carry +// structurally heterogeneous payloads (NoPortConnections is +// nullary; PositionalConnections carries +// `List`; NamedConnections carries +// `List`) — NOT one generic `F` +// projection over a separately-declared source set +// (Practice 7). +// Terminal: the closed three-way Verilog port-connection-form +// classifier of the IEEE 1364-2005 §A.4.1.1 spec. +type PortConnections + = NoPortConnections + | PositionalConnections { + // 🟡 spec-non-empty (§A.4.1.1 ordered_port_connection list) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + actuals: List + } + | NamedConnections { + // 🟡 spec-non-empty (§A.4.1.1 named_port_connection list) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + connections: List + } + + +// ───────────────────────────────────────────────────────────────────── +// ParameterOverrideActual — the closed Verilog named-parameter- +// override actual classifier (IEEE 1364-2005 §A.4.1 named_parameter_ +// assignment). Per spec grammar: +// +// named_parameter_assignment ::= . parameter_identifier +// ( [ mintypmax_expression ] ) +// +// the `[ mintypmax_expression ]` brackets make the actual OPTIONAL — +// `.PARAM()` (blank parens) is legal spec syntax that documents the +// override list while retaining the parameter's declared default +// value. Modeling the actual as a mandatory String collapsed the +// spec's blank-actual form, making `.WIDTH()` unrepresentable +// (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 at line 2161). +// Sibling Disj of PortConnectionActual.BlankConnection — same shape +// for the same "optional sub-expression in a named binding" axis. +// +// - BlankParameterOverride +// — `.PARAM()` form: blank parens; retains the declared +// default. +// - ParameterOverrideExpression { lexeme: String } +// — `.PARAM(expr)` form: the override value as a verbatim +// mintypmax_expression lexeme; sub-grammar deferred to the +// bundled T-4 LanguageModel. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as PortConnectionActual.BlankConnection; abbreviated for brevity +// (each pattern's argument is identical modulo "named-parameter" +// vs "ordered port-connection"). +// 1. Fact placement — FAILS: shared across instance-emission + +// parameter-resolution consumers. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected +// (same BlankConnection precedent argument). +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one actual state per binding. +// 5. Parameterized family — FAILS: BlankParameterOverride is +// nullary; ParameterOverrideExpression carries a `lexeme: +// String` payload — structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog named-parameter-override- +// actual classifier. +type ParameterOverrideActual + = BlankParameterOverride + | ParameterOverrideExpression { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// NamedParameterOverride — one named parameter override on a module +// instantiation (`.WIDTH(8)`, `.PARAM()`). IEEE 1364-2005 §12.1.3 / +// §A.4.1. Conj record (no Practice-4 ledger). +// +// - parameter the formal parameter name on the instantiated +// module (K-1-opaque Symbol; resolves to a matching +// ParameterDeclaration on the target module). +// - actual the override value as a closed Disj over the +// blank-vs-lexeme spec choice (ParameterOverrideActual +// above). Replaces the prior mandatory-String shape +// that collapsed the `.PARAM()` blank-actual form +// per openai-pro REQUEST_CHANGES on PR #3176 +// 2026-05-16. +type NamedParameterOverride { + parameter: Symbol + actual: ParameterOverrideActual +} + + +// ───────────────────────────────────────────────────────────────────── +// ParameterOverrides — the closed Verilog module-instance parameter- +// override classifier (IEEE 1364-2005 §12.1.3). A module +// instantiation can override the instantiated module's parameter +// declarations via the `#(...)` syntax (`Adder #(.WIDTH(8)) a1 +// (.a(x), .b(y))` named form, or `Adder #(8) a1 (x, y)` ordered +// form), or omit overrides entirely. The spec admits three mutually- +// exclusive forms; modeling parameter-overrides as omitted (the prior +// ModuleInstance shape) excluded valid Verilog syntax that +// parameterized instantiations depend on (codex BLOCKING review on +// PR #3176). INVARIANTS P1 modeling-faithfulness violation. +// +// - NoParameterOverrides +// — `Adder a1 (.a(x), .b(y))` — no `#(...)` clause; the +// instantiated module uses its declared default-parameter +// values. +// - OrderedParameterOverrides { actuals: List } +// — `Adder #(8, 16) a1 (...)` — overrides listed in +// declaration-order position; the i-th actual overrides the +// i-th parameter of the instantiated module. Each actual is a +// verbatim expression lexeme. +// - NamedParameterOverrides { overrides: List } +// — `Adder #(.WIDTH(8), .DEPTH(16)) a1 (...)` — overrides +// explicitly bound to formals by name. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.1.3 admits exactly +// these three parameter-override forms; mixing ordered and named +// within one `#(...)` clause is a syntax error per spec — the Disj- +// with-named-payloads makes that uniform-form choice structural +// (same shape as PortConnections). +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every instance-emission consumer and +// every parameter-resolution walker reads the override form +// uniformly; shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing the three forms to a +// uniform `{ named?: List<...>, ordered?: List<...> }` ratifies +// "both named and ordered in one clause" — exactly the spec- +// forbidden mixed form. The Disj makes per-instance uniformity +// structural. +// 3. Algebraic form — N/A by construction: the three forms are +// the IEEE 1364-2005 spec's parameter-override partition; they +// do not trace to a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single module instance has EXACTLY +// ONE parameter-override form; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: NoParameterOverrides is +// nullary; OrderedParameterOverrides carries +// `List` (verbatim expression lexemes by position); +// NamedParameterOverrides carries `List` +// (each with formal + actual) — structurally heterogeneous, +// NOT one generic `F` / projection over a single source set +// (Practice 7). +// Terminal: the closed three-way Verilog module-instance parameter- +// override classifier of the IEEE 1364-2005 spec. +type ParameterOverrides + = NoParameterOverrides + // OrderedParameterOverrides.actuals: 🟡 spec-non-empty (§12.1.3) — + // deferred to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note above. + // (NoParameterOverrides covers the omitted-clause form, so an + // empty present-clause is structurally redundant AND spec-illegal.) + | OrderedParameterOverrides { actuals: List } + // NamedParameterOverrides.overrides: 🟡 spec-non-empty (§12.1.3) — + // deferred to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note above. + | NamedParameterOverrides { overrides: List } + + +// ───────────────────────────────────────────────────────────────────── +// InstanceRangeClause — the closed Verilog instance-array range +// classifier on a module / UDP instance (IEEE 1364-2005 §A.4.1.1 / +// §A.5.2): a single instance identifier may optionally carry a +// `[msb:lsb]` range to declare an ARRAY of instances (`Adder a[7:0] +// (...)`), elaborated to multiple bit-replicated instances at compile +// time. Sibling Disj of DriveStrengthClause / DelayClause / etc. — +// optional-clause present/absent partition. +// +// - NoInstanceRange +// — `Adder a1 (...)` form: single-instance declaration. +// - InstanceRange { range: VectorRange } +// — `Adder a[7:0] (...)` form: instance-array; the range +// drives elaboration-time instance replication. Reuses the +// VectorRange carrier (constant_expression-pair via lexeme). +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as DriveStrengthClause / DelayClause; abbreviated for brevity. +// 1. Fact placement — FAILS: shared classifier across module- +// instance / UDP-instance emitters + elaboration-time +// replication consumers. +// 2. Variant-is-data — FAILS: empty-VectorRange sentinel +// reintroduces the spec-illegal "zero-width array" state and +// mixes the no-range form with a degenerate range form. +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one instance-range state per instance +// name; mutually exclusive. +// 5. Parameterized family — FAILS: NoInstanceRange is nullary; +// InstanceRange carries a `range: VectorRange` payload — +// structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog instance-array-range-presence +// classifier. Added 2026-05-16 per openai-pro REQUEST_CHANGES on +// PR #3176 — the prior shape dropped the optional range, making +// instance arrays unrepresentable. +type InstanceRangeClause + = NoInstanceRange + | InstanceRange { range: VectorRange } + + +// ───────────────────────────────────────────────────────────────────── +// ModuleInstance — one instance within a module_instantiation +// statement (`a1 (.a(x), .b(y), .sum(z))`, `a[7:0] (...)`). IEEE +// 1364-2005 §12.1 + §A.4.1.1. A single module_instantiation can +// declare MULTIPLE instances sharing a common (module_name, +// parameter_overrides); each instance carries its own (instance_name, +// optional instance-array range, port_connections). Per spec +// §A.4.1.1 `name_of_module_instance ::= module_instance_identifier +// [range]` — the prior shape dropped the optional range, making +// spec-legal `Adder a[7:0] (...)` instance arrays unrepresentable +// (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 at line 2247). +// Conj record (no Practice-4 ledger). +// +// - instance_name this instance's local name (K-1-opaque Symbol) +// - instance_range optional instance-array range +// (NoInstanceRange | InstanceRange{range}) +// - connections the port-binding list per spec §12.1.2 +// (PositionalConnections OR NamedConnections; +// uniform per instance). +type ModuleInstance { + instance_name: Symbol + instance_range: InstanceRangeClause + connections: PortConnections +} + + +// ───────────────────────────────────────────────────────────────────── +// ModuleInstantiation — a Verilog module_instantiation statement +// (`Adder #(.WIDTH(8)) a1 (.a(x1), .b(y1)), a2 (.a(x2), .b(y2));`). +// IEEE 1364-2005 §12.1 + §A.4.1.1. Per spec grammar +// module_instantiation is ONE shared (module_identifier + +// parameter_value_assignment) clause followed by a NON-EMPTY LIST of +// module_instance entries — multi-instance declarations share the +// statement's module-name and parameter-override authority across +// all listed instances. The prior shape modeled ONE instance per +// ModuleInstance carrier and lost the §12.1 statement-boundary +// (shared module + shared overrides) for multi-instance forms +// (codex BLOCKING on PR #3176 2026-05-16). INVARIANTS P1/P2. +// +// - module_name the instantiated module's name (K-1- +// opaque Symbol; resolved through the +// namespace to the matching top-level +// `VerilogModule`). Shared across all +// instances in this statement. +// - parameter_overrides the `#(...)` parameter-override clause +// per spec §12.1.3. Shared across all +// instances; the same overrides bind to +// every instance in the multi-instance +// form. +// - instances the per-instance entries — each carries +// its own (instance_name, connections). +// Conj record (no Practice-4 ledger). +type ModuleInstantiation { + module_name: Symbol + parameter_overrides: ParameterOverrides + // ModuleInstantiation.instances: 🟡 spec-non-empty (§A.4.1.1) — + // deferred to std/collection.dag Wave-A2 `List where non_empty` + // refinement; see shared TRACKED-SCAFFOLD note above. + instances: List +} + + +// ───────────────────────────────────────────────────────────────────── +// DefparamAssignment — one (target_path, value) pair in a `defparam` +// statement's defparam_assignment list (IEEE 1364-2005 §A.2.5: +// `defparam_assignment ::= hierarchical_parameter_identifier = +// mintypmax_expression`). Conj record (no Practice-4 ledger). +// +// - target_path the hierarchical target-parameter path as a +// verbatim lexeme (sub-grammar deferred to the +// T-4 LanguageModel — hierarchical identifier +// resolution is its concern). +// - value_lexeme the override value as a verbatim expression +// lexeme. +type DefparamAssignment { + target_path: String + value_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// DefparamDeclaration — a Verilog `defparam` statement +// (`defparam top.sub.WIDTH = 8, top.sub.DEPTH = 16;`). IEEE 1364-2005 +// §12.2 + §A.2.5 (deprecated per spec but admitted). Per spec a +// single `defparam` statement carries a NON-EMPTY list of +// defparam_assignment entries: +// +// defparam_assignment_list ::= defparam_assignment +// { , defparam_assignment } ; +// +// The prior singular-entry shape lost the §12.2 statement-boundary +// (shared `defparam` keyword across multi-assignment forms) and made +// repeated DefparamDeclaration items in a module's ModuleItems +// ambiguous about whether two adjacent defparams came from one +// statement or two (openai-pro REQUEST_CHANGES on PR #3176 +// 2026-05-16 at line 2315). Conj record (no Practice-4 ledger). +// +// - assignments the non-empty list of defparam assignments +// declared under this single `defparam` +// statement. +type DefparamDeclaration { + // 🟡 spec-non-empty (§A.2.5 defparam_assignment list) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List +} + + +// ───────────────────────────────────────────────────────────────────── +// GenerateRegion — a Verilog `generate ... endgenerate` block +// (IEEE 1364-2005 §12.4, §12.1.3.3). Generate regions admit +// `generate-for`, `generate-if`, and `generate-case` constructs that +// are ELABORATED at compile time to produce additional module items. +// Conj record (no Practice-4 ledger). +// +// - body_lexeme the entire `generate ... endgenerate` body as +// a verbatim lexeme (sub-grammar deferred to the +// T-4 LanguageModel — the elaboration rules for +// generate-for / generate-if / generate-case + +// the elaboration-time iteration are owned by +// the bundled LanguageModel productions when +// they land) +type GenerateRegion { + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// LoopGenerateConstruct — a Verilog `for ( genvar = init ; cond ; +// next ) generate_block` construct (IEEE 1364-2005 §12.4 + +// §A.1.4 / §A.4.2 loop_generate_construct). Per spec grammar +// loop_generate_construct is a module_or_generate_item DIRECTLY +// (not nested inside `generate ... endgenerate`); a bare +// `for (genvar i = 0; i < 8; i = i + 1) … endgenerate` is a legal +// module-body item per Annex A.1.4. Conj record (no Practice-4 +// ledger). +// +// - body_lexeme the entire generate-for construct (genvar +// init/cond/iteration + generate_block body) +// as a verbatim lexeme; sub-grammar deferred to +// T-4 LanguageModel (the elaboration-time +// iteration semantics live there). +// +// Added per openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 — +// the prior GenerateRegion variant only covered the `generate ... +// endgenerate` form, omitting the bare loop_generate_construct +// admitted directly at module-item level per spec Annex A.1.4. +type LoopGenerateConstruct { + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// ConditionalGenerateConstruct — a Verilog `if (cond) generate_block +// [else generate_block]` or `case (cond) ... endcase` conditional +// generate construct (IEEE 1364-2005 §A.1.4 / §A.4.2 +// conditional_generate_construct = if_generate_construct | +// case_generate_construct). Like LoopGenerateConstruct, this is +// admitted directly at module-item level per spec Annex A.1.4 +// (not nested inside `generate ... endgenerate`). Conj record (no +// Practice-4 ledger). +// +// - body_lexeme the entire conditional-generate construct +// (if/case head + generate_block body) as a +// verbatim lexeme; sub-grammar deferred to +// T-4 LanguageModel. +// +// Added per openai-pro REQUEST_CHANGES on PR #3176 2026-05-16. +type ConditionalGenerateConstruct { + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// SpecifyBlock — a Verilog `specify ... endspecify` block +// (IEEE 1364-2005 §14, §12.2). Specify blocks declare module path +// delays + timing checks (`$setup`, `$hold`, `$width`, etc.). Conj +// record (no Practice-4 ledger). +// +// - body_lexeme the entire `specify ... endspecify` body as a +// verbatim lexeme (sub-grammar deferred — the +// SDF-class timing-check vocabulary is owned by +// the bundled T-4 LanguageModel productions when +// they land; per the header PROBE LIMITS, +// timing-checks are a separate layer) +type SpecifyBlock { + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// LifetimeClause — the closed Verilog task/function lifetime +// classifier (IEEE 1364-2005 §10.2 / §10.3 / §A.2.6): tasks and +// functions admit an OPTIONAL `automatic` keyword: +// +// task_declaration ::= task [automatic] task_identifier ; ... endtask +// function_declaration ::= function [automatic] +// [function_range_or_type] +// function_identifier ; ... endfunction +// +// `automatic` declares per-call storage (recursive-safe); the +// default is `static` (single shared storage, default keyword +// absent). Modeled as a closed Disj rather than a Bool to avoid +// the K-1 Bool-as-keyword anti-pattern. Field added at sha +// cb028c7d+ per openai-pro REQUEST_CHANGES — TaskDeclaration / +// FunctionDeclaration previously collapsed this into body_lexeme, +// losing the §10.2/§10.3 declaration-boundary fact. +// +// - StaticLifetime +// — `task t;` / `function f;` (default; `automatic` keyword +// absent). +// - AutomaticLifetime +// — `task automatic t;` / `function automatic f;` (per-call +// storage; spec keyword present). +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Five-pattern ledger abbreviated. +// 1. Fact placement — FAILS: shared classifier across task / +// function emitters + elaboration consumers. +// 2. Variant-is-data — FAILS: collapsing to `is_automatic: Bool` +// reintroduces the K-1-forbidden Bool-as-keyword anti-pattern; +// string sentinel ditto. +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one lifetime per declaration; mutually +// exclusive. +// 5. Parameterized family — FAILS: both variants are nullary — +// spec-distinct keyword identities (Practice 7). +// Terminal: the closed two-way Verilog task/function lifetime +// classifier. +type LifetimeClause + = StaticLifetime + | AutomaticLifetime + + +// ───────────────────────────────────────────────────────────────────── +// FunctionReturnTypeClause — the closed Verilog function return- +// type-or-range classifier (IEEE 1364-2005 §10.3 / §A.2.6): function +// declarations admit an OPTIONAL `function_range_or_type` between +// `[automatic]` and the function name: +// +// function_range_or_type ::= [ signed ] [ range ] +// | integer | real | realtime | time +// +// The clause is OPTIONAL per spec; when absent, the function returns +// a single-bit (default) result. When present, the spec form is +// either a signed/range pair (returning a bit-vector) or one of the +// spec-fixed-width variable types. Field added at sha cb028c7d+ per +// openai-pro REQUEST_CHANGES — FunctionDeclaration previously +// collapsed this declaration-boundary fact into body_lexeme. The +// sub-grammar (signed/range distinction + variable-type keyword +// closure) is deferred to the bundled T-4 LanguageModel via the +// established body_lexeme precedent. +// +// - NoFunctionReturnType +// — `function f;` form: default single-bit return. +// - FunctionReturnTypeLexeme { lexeme: String } +// — `function [7:0] f;` / `function signed [7:0] f;` / +// `function integer f;` / etc.; the function_range_or_type as +// a verbatim lexeme. Sub-grammar deferred. +// +// CLOSED (C1 stop-signal). Two-way present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Five-pattern ledger abbreviated. +// 1. Fact placement — FAILS: shared function-emitter / return- +// type-resolution consumers. +// 2. Variant-is-data — FAILS: empty-string sentinel rejected +// (BlankConnection precedent). +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one return-type-or-range state per +// function declaration. +// 5. Parameterized family — FAILS: NoFunctionReturnType is +// nullary; FunctionReturnTypeLexeme carries `lexeme: String` +// — structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog function-return-type-clause +// classifier. +type FunctionReturnTypeClause + = NoFunctionReturnType + | FunctionReturnTypeLexeme { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// TaskDeclaration — a Verilog `task ... endtask` declaration +// (IEEE 1364-2005 §10.2, §12.2 / §A.2.6). A task is a procedural +// sub-routine callable from procedural code; it can carry +// input/output/inout arguments and contain delay/event controls +// (unlike `function`). Conj record (no Practice-4 ledger). +// +// - lifetime the optional `automatic` keyword +// (LifetimeClause); per §10.2 task admits +// `[automatic]` as a declaration-boundary +// modifier (added at sha cb028c7d+ per openai-pro +// REQUEST_CHANGES; prior shape collapsed this +// into body_lexeme). +// - name the task identifier (K-1-opaque Symbol) +// - body_lexeme the procedural body (port list + statements +// between `task [automatic] name;` and `endtask`) +// as a verbatim lexeme (sub-grammar deferred to +// the T-4 LanguageModel) +type TaskDeclaration { + lifetime: LifetimeClause + name: Symbol + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// FunctionDeclaration — a Verilog `function ... endfunction` +// declaration (IEEE 1364-2005 §10.3, §12.2 / §A.2.6). A function is +// a pure (synthesizable) sub-routine that returns a value; the spec +// forbids delay/event controls inside the body (distinguishing +// functions from tasks). Conj record (no Practice-4 ledger). +// +// - lifetime the optional `automatic` keyword +// (LifetimeClause); per §10.3 function admits +// `[automatic]` (added at sha cb028c7d+ per +// openai-pro REQUEST_CHANGES). +// - return_type the optional function_range_or_type clause +// (FunctionReturnTypeClause); per §10.3 function +// admits `[function_range_or_type]` between +// `[automatic]` and the function name (added at +// sha cb028c7d+ per openai-pro REQUEST_CHANGES; +// prior shape collapsed this into body_lexeme). +// - name the function identifier (K-1-opaque Symbol) +// - body_lexeme the function body (arguments + statements +// between the declaration header and +// `endfunction`) as a verbatim lexeme (sub- +// grammar deferred to the T-4 LanguageModel — +// the pure-body constraint enforcement lives +// there) +type FunctionDeclaration { + lifetime: LifetimeClause + return_type: FunctionReturnTypeClause + name: Symbol + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// EventDeclarator — one (name, optional-unpacked-dimensions) entry +// in an event_declaration's list_of_event_identifiers (IEEE 1364-2005 +// §A.2.1.4 / §A.2.3). Per spec: +// +// list_of_event_identifiers ::= event_identifier [ dimension +// { dimension } ] +// { , event_identifier [ dimension +// { dimension } ] } +// +// each event identifier admits an OPTIONAL unpacked-array dimension +// suffix (openai-pro REQUEST_CHANGES on PR #3176 sha 4ccc6267 — the +// prior Symbol-only shape dropped the per-identifier dimensions +// fact). Conj record (no Practice-4 ledger). +// +// - name the event identifier (K-1-opaque Symbol). +// - unpacked_dimensions optional unpacked-array dimensions per +// §A.2.3 (reuses UnpackedDimensionsClause). +type EventDeclarator { + name: Symbol + unpacked_dimensions: UnpackedDimensionsClause +} + + +// ───────────────────────────────────────────────────────────────────── +// EventDeclaration — a Verilog named-event declaration (`event ev1, +// ev2, ev3;` / `event log[0:255];`). IEEE 1364-2005 §9.7.3 / §10.3 / +// §A.2.1.4. Named events are explicitly-triggered control-flow +// primitives (`-> ev;` triggers, `@ev` waits). Per spec §A.2.1.4 +// grammar: +// +// event_declaration ::= event list_of_event_identifiers ; +// list_of_event_identifiers ::= event_identifier [ dimension +// { dimension } ] +// { , event_identifier [ dimension +// { dimension } ] } +// +// a single `event` statement declares a NON-EMPTY list of +// (name, optional-dimensions) entries under a shared `event` keyword +// (sha 4ccc6267 openai-pro REQUEST_CHANGES — per-identifier +// dimensions added via EventDeclarator). The prior singular-name +// shape lost the §A.2.1.4 statement-boundary; the prior +// Symbol-only-list shape dropped the per-identifier dimensions. +// Conj record (no Practice-4 ledger). +// +// - event_declarators the non-empty list of EventDeclarator +// entries declared under this single +// `event` statement. +type EventDeclaration { + // 🟡 spec-non-empty (§A.2.1.4 list_of_event_identifiers) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + event_declarators: List +} + + +// ───────────────────────────────────────────────────────────────────── +// GenvarDeclaration — a Verilog `genvar` declaration (`genvar i, j, +// k;`). IEEE 1364-2005 §12.4.2 / §A.2.1.1. Generate variables drive +// elaboration-time loop iteration in `generate-for` constructs. Per +// spec §A.2.1.1 grammar: +// +// genvar_declaration ::= genvar list_of_genvar_identifiers ; +// list_of_genvar_identifiers ::= genvar_identifier +// { , genvar_identifier } +// +// a single `genvar` statement declares a NON-EMPTY list of genvar +// identifiers under a shared `genvar` keyword. The prior singular- +// name shape lost the §A.2.1.1 statement-boundary — openai-pro +// REQUEST_CHANGES on PR #3176 2026-05-16 at line 2315 (grouped with +// DefparamDeclaration / EventDeclaration). Conj record (no Practice-4 +// ledger). +// +// - genvar_names the non-empty list of genvar identifiers (K-1- +// opaque Symbols) declared under this single +// `genvar` statement. +type GenvarDeclaration { + // 🟡 spec-non-empty (§A.2.1.1 list_of_genvar_identifiers) — + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + genvar_names: List +} + + +// ───────────────────────────────────────────────────────────────────── +// LocalParameterDeclaration — a Verilog `localparam` declaration +// (`localparam W = 8;`). IEEE 1364-2005 §3.10, §12.2. Local parameters +// differ from ordinary parameters in that they CANNOT be overridden +// by `defparam` or by parameter overrides on a module instantiation +// (the spec's distinct binding rule). Conj record (no Practice-4 +// ledger). +// +// - type_kind which parameter-type form (ParameterTypeKind +// Disj — same per-kind admissibility as +// ParameterDeclaration). Mirrors ParameterDeclaration's +// type-fact preservation per IEEE 1364-2005 §A.2.1.1. +// - assignments the list_of_param_assignments per spec — each +// ParameterAssignment carries name + default_lexeme. +type LocalParameterDeclaration { + type_kind: ParameterTypeKind + // 🟡 spec-non-empty (§A.2.1.1) — deferred to std/collection.dag + // Wave-A2 refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List +} + + +// ───────────────────────────────────────────────────────────────────── +// PrimitiveGateKind — the closed Verilog built-in primitive-gate +// kind classifier (IEEE 1364-2005 §7.2). The spec admits exactly 26 +// primitive gate types partitioned into six families per §7. Modeling +// the keyword as a free `String` admits spec-illegal keywords — +// corrected per codex BLOCKING on PR #3176 (M4 closed-sets-are-enums +// + INVARIANTS P2 illegal-states-unrepresentable). The keyword IS the +// closed kind discriminator and lives on this enum. +// +// N-input gates (§7.2): +// - GateAnd, GateNand, GateOr, GateNor, GateXor, GateXnor +// N-output gates (§7.2): +// - GateBuf, GateNot +// Three-state gates (§7.2): +// - GateBufif0, GateBufif1, GateNotif0, GateNotif1 +// MOS switches (§7.5): +// - GateNmos, GatePmos, GateCmos, GateRnmos, GateRpmos, GateRcmos +// Bidirectional pass switches (§7.6): +// - GateTran, GateRtran, GateTranif0, GateTranif1, GateRtranif0, +// GateRtranif1 +// Pull gates (§7.7): +// - GatePulldown, GatePullup +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §7 admits this 26-way +// primitive-gate partition; SystemVerilog adds no new primitives. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟡 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). Ledger — five patterns +// attempted: +// 1. Fact placement — FAILS: every gate-emission consumer + every +// per-gate terminal-arity check + every per-gate drive-strength +// legality check reads the kind tag uniformly; shared +// classifier, not scattered. +// 2. Variant-is-data — FAILS: a `{ keyword: String }` proxy admits +// spec-illegal keywords (M4 closed-sets-are-enums-not-strings; +// the K-1 readable-string heuristic surface this Disj forecloses). +// A `{ id: Int }` proxy admits unbounded Int — same anti-pattern. +// The enum IS the M4-faithful form. +// 3. Algebraic form — N/A by construction: the 26 gates are the +// spec's primitive electrical-primitive taxonomy; the per-family +// sub-partitions (n-input / n-output / three-state / MOS / pass / +// pull) are observable derivations, not richer std/ algebra. +// 4. Dimensional — FAILS: a single gate instantiation has EXACTLY +// ONE kind; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: the 26 are structurally +// heterogeneous per family (varying terminal-arity admissibility +// per gate, varying drive-strength admissibility, varying +// bidirectionality) — NOT one generic `F` / projection over +// a separately-declared source set (Practice 7). The spec's +// partition is irreducible. +// Terminal: the closed twenty-six-way Verilog primitive-gate-kind +// classifier of the IEEE 1364-2005 §7 spec. +// +// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md +// merged on origin/main): under the pre-#3200 consumer-DEPENDENT +// GREEN rule this Disj was correctly GREEN. Under the post-#3200 +// consumer-INDEPENDENT rule this is 🟡 YELLOW because a namable +// richer source EXISTS: +// Axes: {gate-family, logic-function, inversion, polarity, +// controllable-enable, resistive, transmission} +// Logic-family + inversion: and/or/not/buf/nand/nor/xor/xnor +// Controllable-enable + polarity: bufif0/bufif1/notif0/notif1 +// CMOS-switch + resistive + polarity: cmos/rcmos/nmos/rnmos/ +// pmos/rpmos +// Transmission-gate + resistive + controllable + polarity: +// tran/rtran/tranif0/tranif1/rtranif0/rtranif1 +// Pull-resistor + polarity: pulldown/pullup +// Trigger: first consumer of gate-class semantics (elaboration / +// simulation dispatch — the per-gate-class admissibility table +// for drive_strength / delay / terminal-arity). +// Obligation: the first meaning-consumer owes structural +// decomposition into the gate-family matrix AT that consumer — +// NOT a local match-over-keyword lookup in this carrier. +type PrimitiveGateKind + = GateAnd + | GateNand + | GateOr + | GateNor + | GateXor + | GateXnor + | GateBuf + | GateNot + | GateBufif0 + | GateBufif1 + | GateNotif0 + | GateNotif1 + | GateNmos + | GatePmos + | GateCmos + | GateRnmos + | GateRpmos + | GateRcmos + | GateTran + | GateRtran + | GateTranif0 + | GateTranif1 + | GateRtranif0 + | GateRtranif1 + | GatePulldown + | GatePullup + + +// ───────────────────────────────────────────────────────────────────── +// GateInstantiation — a Verilog built-in primitive instantiation +// (`and g1(out, a, b);` / `not n1(o, i);` / `bufif1 b1(out, in, en);`, +// etc.). IEEE 1364-2005 §7 / §A.5.4. Conj record (no Practice-4 ledger). +// +// - gate_kind which built-in primitive gate (PrimitiveGateKind +// closed Disj; replaces the prior free-String +// gate_keyword that admitted spec-illegal +// keywords — M4 / INVARIANTS P2 fix per codex +// BLOCKING on PR #3176). +// - body_lexeme THE ENTIRE statement body after the gate- +// keyword (per-gate-class drive_strength / +// delay clauses + non-empty list of +// gate_instance entries, where each +// gate_instance carries an optional +// name_of_gate_instance (`identifier [range]`) +// plus its per-instance terminal list) as a +// verbatim lexeme. Sub-grammar deferred to the +// bundled T-4 LanguageModel — the per-gate- +// class admissibility table (cmos_switch_type +// forbids drive_strength but allows delay3; +// enable_gatetype allows both; pass_switchtype +// forbids both; n_input_gatetype admits delay2 +// not delay3; etc., per §A.5.4) is exactly the +// class-specific grammar productions that owner +// models. The per-instance name_of_gate_ +// instance + range structural extraction +// (codex non-blocking flag re: "name_of_instance +// carrier reuse at gate boundaries") rides this +// SAME sub-grammar deferral — the per-gate- +// class shape matrix forbids a uniform +// structural carrier at the GateInstantiation +// level (it would re-introduce admit-then-check +// on the gate-kind × clause admissibility +// product), so the per-instance facts live +// inside body_lexeme until the LanguageModel +// productions structurally encode each +// gate-class's instance shape. Same body_lexeme +// precedent as UdpDefinition.body_lexeme + +// AlwaysBlock.body_lexeme — sub-grammar +// defer-via-lexeme is the established pattern +// for spec sub-productions owned by the +// bundled LanguageModel. +type GateInstantiation { + gate_kind: PrimitiveGateKind + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// UdpInstanceName — the closed Verilog UDP-instance name-of-instance +// classifier (IEEE 1364-2005 §A.5.2): +// +// udp_instance ::= [ name_of_udp_instance ] ( output_terminal , +// input_terminal +// { , input_terminal } ) +// name_of_udp_instance ::= udp_instance_identifier [ range ] +// +// the brackets around `name_of_udp_instance` make the entire name +// clause OPTIONAL — unnamed UDP instances are legal spec syntax +// (`xor ( o, a, b )` without an instance name). When present, the +// name itself may carry an optional instance-array range. The prior +// shape required `instance_name: Symbol` and dropped the range, +// making both spec-legal forms unrepresentable (openai-pro +// REQUEST_CHANGES on PR #3176 2026-05-16 at line 2648). +// +// - NoUdpInstanceName +// — `xor ( o, a, b )` form: no instance name; the spec's +// bracket-absent form. +// - NamedUdpInstance { name: Symbol, instance_range: InstanceRangeClause } +// — `xor x1 ( o, a, b )` / `xor x[7:0] ( o, a, b )` form: +// instance name present, optionally with an array range +// (reuses the shared InstanceRangeClause Disj). +// +// CLOSED (C1 stop-signal). Two-way name-present/absent partition. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: same shape +// as the optional-clause Disj family. +// 1. Fact placement — FAILS: shared across UDP-emitter + +// elaboration consumers reading the optional name. +// 2. Variant-is-data — FAILS: empty-Symbol sentinel rejected +// (same K-1 readable-string heuristic surface concern). +// 3. Algebraic form — N/A by construction. +// 4. Dimensional — FAILS: one name-of-udp-instance state per +// udp_instance; mutually exclusive. +// 5. Parameterized family — FAILS: NoUdpInstanceName is nullary; +// NamedUdpInstance carries `{ name, instance_range }` payload — +// structurally heterogeneous (Practice 7). +// Terminal: the closed two-way Verilog UDP-instance name-of-instance +// classifier of the IEEE 1364-2005 §A.5.2 spec. +type UdpInstanceName + = NoUdpInstanceName + | NamedUdpInstance { name: Symbol, instance_range: InstanceRangeClause } + + +// ───────────────────────────────────────────────────────────────────── +// UdpInstance — one (optional-instance-name, port-list body) entry +// in a UDP instantiation's udp_instance list (IEEE 1364-2005 §A.5.2: +// `udp_instance ::= [name_of_udp_instance] ( output_terminal , +// input_terminal { , input_terminal } )`). The optional name (with +// optional array range when present) is carried via the +// UdpInstanceName Disj above. Conj record (no Practice-4 ledger). +// +// - instance_name optional name-of-udp-instance per §A.5.2 +// (NoUdpInstanceName | NamedUdpInstance{name, +// instance_range}). +// - body_lexeme the per-instance terminal list (`( out , in1, +// in2, ... )`) as a verbatim lexeme; sub-grammar +// (output_terminal + input_terminal_list per +// §A.5.4) deferred to the bundled T-4 +// LanguageModel. +type UdpInstance { + instance_name: UdpInstanceName + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// UdpInstantiation — a Verilog user-defined-primitive instantiation +// (a UDP defined via `primitive ... endprimitive` at the file level +// per IEEE 1364-2005 §8 is instantiated like a gate at the module- +// body level). Per spec §A.5.2 grammar: +// +// udp_instantiation ::= udp_identifier [drive_strength] [delay2] +// udp_instance { , udp_instance } ; +// +// the spec form is ONE shared (udp_identifier + drive_strength + +// delay) clause followed by a NON-EMPTY list of udp_instance entries +// — multi-instance UDP statements share the statement's udp-name and +// strength/delay authority across all listed instances. The prior +// singular-instance shape lost the §A.5.2 statement-boundary (shared +// udp_identifier + shared strength/delay) for multi-instance forms +// (openai-pro REQUEST_CHANGES on PR #3176 2026-05-16 at line 2604; +// same shape as the ModuleInstantiation refactor above per +// §A.4.1.1). Conj record (no Practice-4 ledger). +// +// - udp_name the UDP identifier (K-1-opaque Symbol; +// resolves through the namespace to the +// matching file-level UdpDefinition — see +// below; the UDP and Module sibling design- +// elements share the same name-space). Shared +// across all instances in this statement. +// - drive_strength optional drive_strength clause; reuses the +// DriveStrengthClause Disj shared with +// NetDeclaration / ContinuousAssign. Shared +// across all instances. +// - delay optional delay clause; reuses the DelayClause +// Disj. Per spec §A.5.2 this is `delay2` (rise/ +// fall) where net_declaration uses `delay3` +// (rise/fall/turn-off); the delay2-vs-delay3 +// sub-grammar distinction lives in the bundled +// T-4 LanguageModel productions. Shared across +// all instances. +// - instances the per-instance entries — each carries its +// own (instance_name, body_lexeme). +type UdpInstantiation { + udp_name: Symbol + drive_strength: DriveStrengthClause + delay: DelayClause + // 🟡 spec-non-empty (§A.5.2 udp_instance list) — deferred to + // std/collection.dag Wave-A2 `List where non_empty` refinement; + // see shared TRACKED-SCAFFOLD note above. + instances: List +} + + +// ───────────────────────────────────────────────────────────────────── +// UdpDefinition — a Verilog user-defined-primitive definition +// (`primitive XorPrim (out, a, b); output out; input a, b; table … endtable +// endprimitive`). IEEE 1364-2005 §8 + §A.5. UDP definitions are +// FILE-LEVEL design elements (sibling of `module`/`macromodule`/ +// `config`), NOT module-body items — codex BLOCKING on PR #3176 +// 2026-05-16 surfaced the gap that the prior model referenced UDP +// definitions from UdpInstantiation but did not declare a carrier +// for them. +// +// Conj record (no Practice-4 ledger). +// +// - name the UDP identifier (K-1-opaque Symbol; +// cross-referenced by UdpInstantiation.udp_name) +// - body_lexeme the entire `primitive ... endprimitive` body +// (port list + port declarations + state table +// for sequential UDPs or output assignments for +// combinational UDPs) as a verbatim lexeme; sub- +// grammar deferred to the T-4 LanguageModel — +// the UDP state-table sub-grammar (§8.2) is its +// own recursive sub-language, owned by the +// bundled productions when they land. +// +// FILE-LEVEL DESIGN-ELEMENT NOTE. UdpDefinition is declared at the +// same scope as VerilogModule (top-level type, sibling of the +// module-style Disj). The IEEE 1364-2005 source_text grammar (§A.1.1) +// admits a list of file-level design elements +// `module_declaration | udp_declaration | config_declaration`. +// +// verilog.dag does NOT mint the design-element Disj LOCALLY. Per +// TASKS.md:504 (verbatim, dispositive): "A local Byte/Word copy or +// private language-model schema is invalid." The source_text +// design-element classifier IS the canonical T-4 LanguageModel +// contract spine (top-level compilation-unit composition) — owned +// by the bundled LanguageModel grammar-productions work per the +// canonical-LanguageModel-first directive (TASKS.md 457/473/504), +// + P2 single-authority. Per-language minting would be the v3 +// cross-layer spine-drift the canonical-first directive exists to +// kill (5-language parallel-declaration precedent: every language +// file otherwise hits "source_text needs a design-element +// classifier" and would mint locally; codex top-level review will +// push each language file to do so, exactly what TASKS.md:504 +// forbids). +// +// Dissolution trigger: when the canonical T-4 LanguageModel +// grammar-productions work lands, that owner aggregates +// VerilogModule + UdpDefinition (+ config_declaration when its +// sub-language lands) into the source_text design-element Disj. +// `config_declaration` is scope-negative here per the header +// PROBE LIMITS framing (configuration is a separate elaboration- +// time concern outside the IN-B probe). +// +// At this vocabulary-slice phase UdpDefinition exists as a +// sibling-typed carrier consumed by UdpInstantiation (the +// name-reference resolution target). This NOTE is the single +// source-of-truth deferral marker for the missing aggregator. +type UdpDefinition { + // Per IEEE 1364-2005 Syntax 3-9, udp_declaration carries + // a top-level `{ attribute_instance }` prefix: `(* attr *) primitive + // ... endprimitive` is legal spec form. Field added at sha 7b7dd0b54+ + // per openai-pro REQUEST_CHANGES on PR #3176 sha f9159ce8b (Layer- + // Model BLOCKING: top-level UDP attributes had no typed home; reuses + // the existing AttributeInstanceClause Disj). No double-authority + // concern by grammar-level distinction (not by deferral-timing): + // the §A.1.2 / Syntax 3-9 attribute_instance prefix is INTRINSIC + // to the udp_declaration production, attaching at the declaration + // boundary itself. The source_text design-element classifier (when + // the bundled T-4 LanguageModel lands it) is the description-level + // {module | udp | config} KIND-SELECTOR — a different grammar level + // that structurally NEVER carries attribute_instance. So there is + // no double-authority NOW NOR AFTER the wrapper lands: by spec + // grammar levels, the attribute_instance lives ON the declaration + // (here) and not on the kind-selector. + attributes: AttributeInstanceClause + name: Symbol + body_lexeme: String +} + + +// ───────────────────────────────────────────────────────────────────── +// SpecparamAssignment — one element of a specparam declaration's +// list_of_specparam_assignments (IEEE 1364-2005 §A.2.4): +// +// specparam_assignment ::= +// specparam_identifier = constant_mintypmax_expression +// | pulse_control_specparam +// pulse_control_specparam ::= +// PATHPULSE$ = ( reject_limit_value [ , error_limit_value ] ) ; +// | PATHPULSE$specify_input_terminal_descriptor +// $specify_output_terminal_descriptor +// = ( reject_limit_value [ , error_limit_value ] ) ; +// +// The two alternatives have distinct spec syntax — pulse_control_ +// specparam is NOT a `name = expr` form; it's the special +// `PATHPULSE$...` family. The prior shape reused ParameterAssignment +// `{ name: Symbol, default_lexeme: String }`, forcing every specparam +// to claim a name+value shape — which made pulse_control_specparam +// unrepresentable as a structural variant (openai-pro REQUEST_CHANGES +// on PR #3176 sha 4ccc6267). Split into a specparam-specific Disj +// over the two §A.2.4 spec alternatives. +// +// - NamedSpecparamAssignment +// — `specparam T_rise = 1.0;` form: identifier + constant +// mintypmax-expression lexeme. +// - PulseControlSpecparam +// — `PATHPULSE$ = (1.5, 2.0);` / `PATHPULSE$in$out = +// (1.5);` form: the entire PATHPULSE$... directive as a +// verbatim lexeme (sub-grammar — terminal descriptors + +// reject/error limit values — deferred to the bundled T-4 +// LanguageModel via the established body_lexeme precedent). +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.2.4 admits exactly the +// two specparam_assignment alternatives. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every specparam-emission consumer +// branches on the form (named-value vs pulse-control); shared +// classifier. +// 2. Variant-is-data — FAILS: reusing ParameterAssignment (prior +// shape) forced pulse_control_specparam to claim a `name + +// value_lexeme` shape it doesn't have, losing the PATHPULSE$ +// form as a structural variant. +// 3. Algebraic form — N/A by construction: the two alternatives +// are the §A.2.4 spec's irreducible partition. +// 4. Dimensional — FAILS: a single specparam_assignment is +// EXACTLY ONE form; mutually exclusive alternatives. +// 5. Parameterized family — FAILS: NamedSpecparamAssignment +// carries `{ name: Symbol, value_lexeme: String }`; +// PulseControlSpecparam carries `{ lexeme: String }` (no name +// field — the PATHPULSE$... directive has its own internal +// identifier structure) — structurally heterogeneous +// (Practice 7). +// Terminal: the closed two-way Verilog specparam_assignment +// classifier of the IEEE 1364-2005 §A.2.4 spec. +type SpecparamAssignment + = NamedSpecparamAssignment { name: Symbol, value_lexeme: String } + | PulseControlSpecparam { lexeme: String } + + +// ───────────────────────────────────────────────────────────────────── +// SpecparamDeclaration — a Verilog `specparam` declaration. IEEE +// 1364-2005 §14.3.1 + §12.2 + §A.2.1.1. Specify parameters are +// distinct from ordinary parameters: they are intended for timing- +// check values (rise/fall/hi-Z transitions, pulse-control limits) +// and CANNOT be used as bit-vector widths or array indices per spec. +// Per spec grammar specparam admits an optional range and a list of +// specparam_assignments (sha 4ccc6267 openai-pro REQUEST_CHANGES — +// specparam_assignment carrier split via SpecparamAssignment Disj +// above to admit both NamedSpecparamAssignment + PulseControlSpecparam +// alternatives per §A.2.4). Conj record (no Practice-4 ledger). +// +// - packing optional range (`specparam [9:0]`); applies to +// all assignments in this declaration. +// - assignments the list_of_specparam_assignments per §A.2.4; +// each entry is one of the two SpecparamAssignment +// variants (named-value or pulse-control). +type SpecparamDeclaration { + packing: PackingShape + // 🟡 spec-non-empty (§A.2.1.1) — deferred to std/collection.dag + // Wave-A2 refinement; see shared TRACKED-SCAFFOLD note above. + assignments: List +} + + +// ───────────────────────────────────────────────────────────────────── +// ModuleItem — the closed Verilog module-body item classifier. The +// items inside a `module ... endmodule` body are a flat list of +// concurrently-executing siblings (IEEE 1364-2005 §12.2); ModuleItem +// is the closed variant set of what each sibling can be. +// +// Per the IN-B PROBE FINDING above, this coproduct IS the parallel- +// composition surface: the module-body's `List` is the +// Conj children whose concurrent execution is the IN-B claim's +// structural representation — no 6th `Concurrent` behavior; the +// parallelism is the Conj-of-siblings shape, exactly as a Conj of +// submodule instantiations. +// +// - ContinuousAssignItem `assign net = expr;` +// - AlwaysBlockItem `always @(...) begin … end` +// - InitialBlockItem `initial begin … end` +// - NetDeclarationItem `wire`, `wand`, … declarations +// - VariableDeclarationItem `reg`, `integer`, … declarations +// - ParameterDeclarationItem `parameter NAME = expr;` +// - LocalParameterDeclarationItem `localparam NAME = expr;` (§3.10) +// - ModuleInstantiationItem nested `ModuleName inst (...);` (or +// multi-instance form `Name a1(...), a2(...)`) +// - DefparamDeclarationItem `defparam top.sub.PARAM = value;` (§4.10.2.1) +// - GenerateRegionItem `generate ... endgenerate` (§12.4) +// - SpecifyBlockItem `specify ... endspecify` (§14) +// - TaskDeclarationItem `task name; … endtask` (§10.2) +// - FunctionDeclarationItem `function name; … endfunction` (§10.3) +// - EventDeclarationItem `event ev;` (§9.7.3) +// - GenvarDeclarationItem `genvar i;` (§12.4.2) +// - GateInstantiationItem `and g1(out, a, b);` (§7) +// - UdpInstantiationItem UDP instantiation (§8) +// - SpecparamDeclarationItem `specparam ...;` (§14.3.1) +// +// CLOSED-SET COVERAGE — the variants enumerated below cover the full +// IEEE 1364-2005 §12.2 module_or_generate_item + specparam_declaration +// grammar partition per Annex A.1.4. The prior 12-variant cut missed +// `event_declaration`, `genvar_declaration`, `local_parameter_ +// declaration`, `gate_instantiation`, `udp_instantiation`, and +// `specparam_declaration` (codex BLOCKING on PR #3176, codex/codex- +// default 2026-05-16 — the strict spec-fidelity bar surfaced these +// gaps). Each new variant is a Conj record + body_lexeme deferral +// per the established AlwaysBlock body_lexeme precedent — the sub- +// language structures (gate-primitive terminal lists, UDP definition +// tables, generate-for elaboration, specify timing checks) are owned +// by the bundled T-4 LanguageModel productions when they land, but +// the variant + payload-skeleton lives here so the closed-Disj +// honestly covers §12.2 + §14.3.1. A NEW item kind (one the spec +// does not list) is the C1 stop-signal edit. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every module-body consumer (emission, +// port-binding resolution, sensitivity-list signal lookup, +// synthesis dispatch, generate-elaboration, specify-timing- +// check, task/function inlining, gate-primitive emission, UDP +// resolution, genvar elaboration) branches on the item kind; +// shared classifier, not scattered. +// 2. Variant-is-data — FAILS: each variant carries a payload of +// a DIFFERENT type (the 18 distinct payload records). Collapsing +// to a uniform `{ kind: ItemKind, … }` shape requires Option- +// typed payload fields, which makes mismatched-kind+payload +// combinations representable — the inverse of P2. +// 3. Algebraic form — N/A by construction: the module-body items +// are the IEEE 1364-2005 spec's primitive item taxonomy; they +// do not trace to a richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single item is EXACTLY ONE kind; +// mutually-exclusive alternatives. (The module body as a +// WHOLE is `List` — multiple items co-exist as +// siblings, but each item is one kind. The Conj-of-siblings +// IS the dimensional model the IN-B finding consumes; that +// lives on `VerilogModule.items`, not on this enum.) +// 5. Parameterized family — FAILS: the variants are structurally +// heterogeneous (different payload types; the declaration +// variants carry storage-shape facts while the action variants +// carry computation-shape facts; gate / udp / specify / task / +// function / generate each carry their own sub-language body) +// — NOT one generic `F` / projection over a separately- +// declared source set (Practice 7). The IEEE 1364-2005 module- +// body item set is the irreducible partition. +// Terminal: the closed twenty-way module-body-item classifier of +// the IEEE 1364-2005 §12.2 + §14.3.1 spec (corrected per codex +// BLOCKING on PR #3176 2026-05-16 — added PortDeclarationItem +// (direction-only body port_declaration) and BodyPortDeclarationItem +// (body port_declaration with inline type, reusing the +// AnsiPortDeclaration carrier; the body-form combined declaration +// is structurally equivalent to ANSI per §12.3.4). The body port_ +// declaration is itself a §12.2 module_item the spec lists; the +// prior 18-way cut missed both body forms. +// AnsiModuleItem — the closed Verilog module-body item classifier +// for ANSI-style modules (IEEE 1364-2005 §12.2 — the 18 items spec- +// admitted in any module body, EXCLUDING body port_declarations). +// ANSI ports are "completely declared" per §12.3.3, so body port_ +// declarations (`PortDeclarationItem` / `BodyPortDeclarationItem`) +// are a SYNTAX ERROR in ANSI-style modules — they are admitted only +// in the NonAnsiModuleItem set below. +// +// Per spec §A.1.4 / §A.6.1 most module_or_generate_items admit an +// `{ attribute_instance }` prefix (`(* keep *) assign net = expr;`, +// `(* synthesis_full_case *) always @(...) ...`, `(* dont_touch *) +// Adder a1 (...);`). The prior shape collapsed this fact — +// attribute_instances were unrepresentable except by leaking into +// unrelated lexeme payloads (openai-pro REQUEST_CHANGES on PR #3176 +// 2026-05-16 at line 2884). The fix: each variant carries an +// `attributes: AttributeInstanceClause` first field (closed Disj +// over the §A.9.1 attribute_instance-list-present/absent partition). +// Carried per-variant (rather than as a wrapping Conj outside the +// Disj) keeps the structural per-variant payload-heterogeneity that +// the Practice-4 ledger relies on, and mirrors the established +// per-variant clause-field convention (drive_strength, delay, +// etc.). +type AnsiModuleItem + = ContinuousAssignItem { attributes: AttributeInstanceClause, assign: ContinuousAssign } + | AlwaysBlockItem { attributes: AttributeInstanceClause, always_block: AlwaysBlock } + | InitialBlockItem { attributes: AttributeInstanceClause, initial_block: InitialBlock } + | NetDeclarationItem { attributes: AttributeInstanceClause, net: NetDeclaration } + | VariableDeclarationItem { attributes: AttributeInstanceClause, variable: VariableDeclaration } + | ParameterDeclarationItem { attributes: AttributeInstanceClause, parameter: ParameterDeclaration } + | LocalParameterDeclarationItem { attributes: AttributeInstanceClause, local_parameter: LocalParameterDeclaration } + | ModuleInstantiationItem { attributes: AttributeInstanceClause, instantiation: ModuleInstantiation } + | DefparamDeclarationItem { attributes: AttributeInstanceClause, defparam: DefparamDeclaration } + // GenerateRegionItem carries NO attributes field — per §A.1.4 + // generate_region is one of the module_items without an + // {attribute_instance} prefix in the spec grammar (openai-pro + // REQUEST_CHANGES on PR #3176 sha f9159ce8b — the 4ccc62675 + // uniform-application over-admitted attributes on this variant). + | GenerateRegionItem { generate_region: GenerateRegion } + | LoopGenerateConstructItem { attributes: AttributeInstanceClause, loop_generate: LoopGenerateConstruct } + | ConditionalGenerateConstructItem { attributes: AttributeInstanceClause, conditional_generate: ConditionalGenerateConstruct } + // SpecifyBlockItem carries NO attributes field — per §A.1.4 + // specify_block is one of the module_items without an + // {attribute_instance} prefix in the spec grammar (openai-pro + // REQUEST_CHANGES on PR #3176 sha f9159ce8b — same over-application + // correction as GenerateRegionItem above). + | SpecifyBlockItem { specify_block: SpecifyBlock } + | TaskDeclarationItem { attributes: AttributeInstanceClause, task: TaskDeclaration } + | FunctionDeclarationItem { attributes: AttributeInstanceClause, function_decl: FunctionDeclaration } + | EventDeclarationItem { attributes: AttributeInstanceClause, event_decl: EventDeclaration } + | GenvarDeclarationItem { attributes: AttributeInstanceClause, genvar_decl: GenvarDeclaration } + | GateInstantiationItem { attributes: AttributeInstanceClause, gate: GateInstantiation } + | UdpInstantiationItem { attributes: AttributeInstanceClause, udp_instance: UdpInstantiation } + | SpecparamDeclarationItem { attributes: AttributeInstanceClause, specparam: SpecparamDeclaration } + + +// ───────────────────────────────────────────────────────────────────── +// NonAnsiModuleItem — the closed Verilog module-body item classifier +// for non-ANSI-style modules. Non-ANSI bodies admit ALL AnsiModuleItem +// variants PLUS body port_declarations (PortDeclarationItem + +// BodyPortDeclarationItem) per IEEE 1364-2005 §12.3.4 — port direction +// + (optional) type live in body items in the non-ANSI form. The +// Disj-with-named-payloads makes "ANSI port-list module with body +// PortDeclarationItem" structurally unrepresentable (codex BLOCKING +// fix on PR #3176 2026-05-16: items list was previously +// `List` regardless of port style, admitting the §12.3.3 +// "ANSI ports are completely declared" violation). +// +// - NonAnsiAnsiCompatItem — wraps any AnsiModuleItem +// variant (the 18-way common +// item set admitted in any +// module body). +// - NonAnsiPortDeclarationItem — body port_declaration in +// direction-only form (`input +// a;`); spec §12.3.4 non-ANSI +// style only. +// - NonAnsiBodyPortDeclarationItem +// — body port_declaration in +// direction-plus-type combined +// form (`input wire [7:0] a;`); +// reuses the AnsiPortDeclaration +// carrier per the body-form-is- +// shape-equivalent-to-ANSI +// framing of §12.3.4. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.3.4 admits this +// three-way non-ANSI module-item partition (the common-items +// wrapper + the two body port_declaration forms); SystemVerilog +// adds further forms — future language-version model EDITS this +// Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every non-ANSI module-body consumer +// branches on the variant to dispatch — common items go to +// the AnsiModuleItem walker (via the wrapped item), body +// port_declarations go to the §12.3.4 port-binding-resolution +// walker. Shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to a uniform `{ kind: +// ItemKind, … }` shape reintroduces the §12.3.3 illegal state +// this Disj-split exists to dissolve at the VerilogModule +// level (NonAnsiModuleItem variants belong ONLY to non-ANSI +// modules per VerilogModule's Disj; admitting them on ANSI +// modules would re-open the §12.3.3 "ANSI ports are completely +// declared" violation). The structural-membership constraint +// lives at the VerilogModule-Disj level; this Disj enumerates +// the per-style admissible items. +// 3. Algebraic form — N/A by construction: the three variants +// are the §12.3.4 non-ANSI item-set partition (common-items +// wrapper + two body-port forms); they do not trace to a +// richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single non-ANSI module-body item is +// EXACTLY ONE variant; mutually-exclusive alternatives. (A +// module body's `items` is `List` — +// multiple items co-exist as siblings, but each item is one +// variant.) +// 5. Parameterized family — FAILS: the three variants carry +// structurally heterogeneous payloads (NonAnsiAnsiCompatItem +// wraps an AnsiModuleItem; NonAnsiPortDeclarationItem carries +// a PortDeclaration direction-only record; +// NonAnsiBodyPortDeclarationItem carries an +// AnsiPortDeclaration per-direction Disj) — NOT one generic +// `F` / projection over a single source set (Practice 7). +// Terminal: the closed three-way Verilog non-ANSI module-body-item +// classifier of the IEEE 1364-2005 §12.3.4 spec; ledger added per +// codex BLOCKING on PR #3176 2026-05-16. +type NonAnsiModuleItem + = NonAnsiAnsiCompatItem { item: AnsiModuleItem } + | NonAnsiPortDeclarationItem { + // PortDeclaration was dissolved at sha cb028c7d+ per openai-pro + // REQUEST_CHANGES — AnsiPortDeclaration's no-net-type variants + // cover the §A.2.1.2 input/output/inout [net_type] [signed] + // [range] list_of_port_identifiers production uniformly (bare + // / with-modifiers / with-type-and-modifiers), making the prior + // 2-variant split (PortDeclaration direction-only vs + // AnsiPortDeclaration with-type) a partition gap that lost + // range/signed on `output [7:0] y;` forms. Single AnsiPort + // Declaration carrier here = single authority for non-ANSI + // body port_declarations under §12.3.4. + attributes: AttributeInstanceClause, + port_decl: AnsiPortDeclaration + } + + +// ───────────────────────────────────────────────────────────────────── +// ModuleParameterPortList — the closed Verilog module-header +// parameter-port-list classifier (IEEE 1364-2005 §12.1). A module +// declaration may carry an OPTIONAL `#(parameter W = 8, parameter +// D = 16)` clause between the module name and the port list. Per +// spec grammar the clause is module_parameter_port_list and admits +// parameter_declarations only (not localparam — localparams must +// live in the body). The optional-presence is structural and +// modeled via a closed Disj rather than a nullable field. +// +// - NoModuleParameterPortList +// — `module M (a, b);` — no `#(...)` clause; the module's +// OVERRIDEABLE-PARAMETER SURFACE is the ordered list of body +// `ParameterDeclarationItem` declarations per spec §12.1 +// conditional rule (when no header parameter port list is +// given, body `parameter` declarations are the overrideable +// parameters). Instantiation `ParameterOverrides` actuals +// bind to THAT body-derived list. +// - ModuleParameters { parameters: List } +// — `module M #(parameter W = 8, parameter D = 16) (a, b);` +// — the header carries an explicit `#(...)` parameter port +// list. THESE header parameters are the overrideable surface; +// any body `ParameterDeclarationItem` becomes LOCAL (not +// overrideable) per the spec §12.1 conditional rule. Instantiation +// `ParameterOverrides` actuals bind positionally or by name +// to the header parameters only. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.1 admits exactly the +// present-or-absent partition; SystemVerilog adds type parameters +// and parameterized class declarations — a future language-version +// model would EDIT this Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every module-instantiation / +// parameter-resolution consumer reads the header parameter +// port list to know which parameters are externally +// overridable; shared classifier, not scattered. +// 2. Variant-is-data — FAILS: collapsing to a uniform `{ +// parameters: List }` where empty-list +// = "no clause" conflates "explicitly `#()` empty" (a syntax +// no Verilog admits) with "no `#(...)` clause at all" — the +// Disj makes the present-vs-absent partition structural. +// 3. Algebraic form — N/A by construction: the two variants are +// the spec's primitive clause-presence partition; not a +// richer std/ algebraic structure. +// 4. Dimensional — FAILS: a single module declaration has +// EXACTLY ONE parameter-port-list-presence state; mutually- +// exclusive alternatives. +// 5. Parameterized family — FAILS: NoModuleParameterPortList is +// nullary; ModuleParameters carries +// `List` — structurally heterogeneous, +// NOT one generic `F` / projection over a single source +// set (Practice 7). +// Terminal: the closed two-way Verilog module-header parameter- +// port-list classifier of the IEEE 1364-2005 spec §12.1. +type ModuleParameterPortList + = NoModuleParameterPortList + // ModuleParameters.parameters: 🟡 spec-non-empty (§12.1) — deferred + // to std/collection.dag Wave-A2 refinement; see shared TRACKED- + // SCAFFOLD note above. + | ModuleParameters { parameters: List } + + +// ───────────────────────────────────────────────────────────────────── +// ModuleKeyword — the closed Verilog module-declaration-keyword +// classifier (IEEE 1364-2005 §A.1.2): a module declaration begins +// with either `module` or `macromodule`. The two keywords select +// distinct simulator-elaboration semantics — `macromodule` requests +// the implementation to "treat the module as a macromodule" (a +// hint that the simulator MAY flatten the module's hierarchy for +// performance) while `module` is the standard hierarchical form. +// The two are syntactically distinct on the spec surface and +// `parse ∘ emit` must preserve which keyword the writer used +// (otherwise a `macromodule` declaration emitted as `module` +// silently loses a simulator hint — openai-pro REQUEST_CHANGES on +// PR #3176 2026-05-16 at line 3046). +// +// - ModuleKw — `module` — the standard module-declaration +// keyword. +// - MacromoduleKw — `macromodule` — the macromodule-declaration +// keyword. +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §A.1.2 admits exactly the +// two keywords. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every module-emission consumer reads +// the keyword tag to choose `module` vs `macromodule`; shared +// classifier at the module-declaration boundary. +// 2. Variant-is-data — FAILS: a `{ is_macromodule: Bool }` proxy +// ratifies the K-1-forbidden Bool-as-keyword anti-pattern; a +// `{ keyword: Symbol }` proxy reopens the readable-string +// heuristic surface K-1 forecloses. The 2-variant Disj IS the +// dissolved form. +// 3. Algebraic form — N/A by construction: the two keywords are +// the IEEE 1364-2005 spec's irreducible module-keyword +// partition. +// 4. Dimensional — FAILS: a single module declaration uses +// EXACTLY ONE keyword; mutually-exclusive alternatives. +// 5. Parameterized family — FAILS: both variants are nullary; +// they are spec-distinct keyword identities, not a generic +// `F` projection over a richer source set (Practice 7). +// Terminal: the closed two-way Verilog module-declaration-keyword +// classifier of the IEEE 1364-2005 §A.1.2 spec. +type ModuleKeyword + = ModuleKw + | MacromoduleKw + + +// ───────────────────────────────────────────────────────────────────── +// VerilogModule — a top-level Verilog module (`module Name +// #(parameters) (ports); items endmodule`, or `macromodule Name …`, +// or `module Name; items endmodule` with no port list at all). +// IEEE 1364-2005 §12.1 / §12.3.4 / §A.1.2. +// Three-way Disj — the §12.3.4 module-style partition is the +// dimensional axis of VerilogModule, with a style-neutral +// NoPortsModule variant for the no-port-list form. Each style +// variant carries its own header-port-list type AND its own +// admissible body-items list type. Three illegal states are +// structurally unrepresentable: +// (1) "ANSI port-list module with body PortDeclarationItem" +// (the original 2-way split) +// (2) "No-port-list module with body port_declarations" +// (NoPortsModule items: List — no body +// port_declaration variants representable since body +// port_declarations would reference non-existent header +// port names per §12.3.4) +// (3) "No-port-list represented two ways" +// (P2 representation-duality between NonAnsi{header_ports=[]} +// and Ansi{header_ports=[]} — the NoPortsModule variant is +// the single representation of the no-ports state; the per- +// style variants now have spec-non-empty header_ports) +// +// - NoPortListModule +// — `module M; ... endmodule` form: §A.1.2 port-list brackets +// entirely absent (no parens). Style-neutral. +// - EmptyPortListModule +// — `module M (); ... endmodule` form: §A.1.2 port-list +// brackets PRESENT but inner list EMPTY. Distinct spec +// surface from NoPortListModule per §A.1.2 (split at sha +// cb028c7d+ per openai-pro REQUEST_CHANGES — prior single +// NoPortsModule variant conflated the two distinct spec +// forms, losing surface fidelity for parse/emit). Style- +// neutral; items use the AnsiModuleItem set (excludes body +// port_declarations). +// - NonAnsiVerilogModule +// — non-ANSI style: header carries port-EXPRESSIONS only +// (List); body carries the full NonAnsiModuleItem +// set including body PortDeclarationItem + +// BodyPortDeclarationItem per §12.3.4. +// - AnsiVerilogModule +// — ANSI style: header carries fully-declared ports +// (List, where AnsiHeaderPort wraps an +// attribute-free AnsiPortDeclaration payload with the §A.1.3 +// outer attribute_instance prefix); body carries AnsiModuleItem +// only (the 18 items spec-admitted in any module body +// EXCLUDING port_declarations — per §12.3.3 ANSI ports are +// "completely declared" and body redeclarations are a syntax +// error). +// +// Both variants carry name + parameter_port_list. The module's +// OVERRIDEABLE-PARAMETER SURFACE is determined by IEEE 1364-2005 +// §12.1's CONDITIONAL rule (clarified per openai-pro REQUEST_CHANGES +// on PR #3176 2026-05-16 — the prior framing was internally +// inconsistent on this rule): +// +// - WHEN `parameter_port_list` is `ModuleParameters { ... }` (i.e. +// the module has an explicit `#(...)` header clause), THOSE +// header parameters ARE the overrideable parameter surface; any +// body `ParameterDeclarationItem` is LOCAL (not overrideable — +// even though it uses the `parameter` keyword). +// - WHEN `parameter_port_list` is `NoModuleParameterPortList` (no +// header `#(...)`), the OVERRIDEABLE parameter surface is the +// ORDERED LIST of body `ParameterDeclarationItem` declarations +// in source-appearance order. +// - `LocalParameterDeclarationItem` is NEVER part of the +// overrideable surface regardless of header presence (per §3.10 +// `localparam` is local-only by spec). +// +// Instantiation `#(parameter overrides)` clauses bind by position or +// by name to whichever set IS the overrideable surface per the +// conditional rule above. Downstream override-resolution consumers +// read the per-variant `parameter_port_list` to determine which set +// to walk. +// +// Per the IN-B PROBE FINDING: the `items` field IS the parallel- +// Conj surface; the structural concurrency of multiple always-blocks +// / continuous-assigns / instances is precisely "these are siblings +// in the items list". There is no `concurrent: Bool` flag; the +// parallelism is read FROM the list-of-siblings shape +// (feedback_no_annotations). +// +// CLOSED (C1 stop-signal). IEEE 1364-2005 §12.3.4 admits exactly the +// two module-style forms; SystemVerilog adds further declaration +// forms — future language-version model EDITS this Disj explicitly. +// +// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) — +// 🟢 GREEN (terminal). Ledger — five patterns attempted: +// 1. Fact placement — FAILS: every module-level consumer +// (emission, port-binding resolution, body item-set +// admissibility check, synthesis dispatch) branches on the +// style uniformly; shared classifier at the module-as-a-whole +// level, not scattered. +// 2. Variant-is-data — FAILS: collapsing to a uniform Conj +// record `{ name, parameter_port_list, ports: ModulePortsList, +// items: List }` ratifies the §12.3.3 +// illegal state "ANSI ports + body port_declaration" — the +// prior shape this VerilogModule Disj was introduced to +// dissolve. The per-style payloads make admissibility +// structural. +// 3. Algebraic form — N/A by construction: the two module styles +// are the IEEE 1364-2005 spec's primitive module-style +// partition; they do not trace to a richer std/ algebraic +// structure. +// 4. Dimensional — FAILS: a single module declaration is EXACTLY +// ONE style; mutually-exclusive alternatives per §12.3.4. +// 5. Parameterized family — FAILS: the variants carry +// structurally heterogeneous payloads (NonAnsi.header_ports: +// List + items: List vs Ansi. +// header_ports: List + items: +// List; NoPortsModule has no header_ports at +// all + items: List) — the header port-list +// type AND the body item-set type both differ per variant. +// NOT one generic `F` / projection over a single source set +// (Practice 7). The compound payload-type difference IS the +// partition's defining structural fact. +// Terminal: the closed four-way Verilog module-declaration-style +// classifier of the IEEE 1364-2005 §A.1.2 / §12.3.4 spec +// (NoPortListModule + EmptyPortListModule + per-style variants); +// the NoPortListModule/EmptyPortListModule split (sha cb028c7d+, +// openai-pro REQUEST_CHANGES) distinguishes parens-absent from +// parens-present-empty per §A.1.2. Original ledger added per codex +// BLOCKING on PR #3176 2026-05-16, NoPortsModule variant added at +// sha 7709c9968 per +// openai-pro REQUEST_CHANGES (line 3525 — no-port-list +// representation-duality + non-ANSI body port_declarations with +// empty header). +// All 4 variants carry `attributes: AttributeInstanceClause` per +// IEEE 1364-2005 Syntax 3-4: `module_declaration ::= { attribute_ +// instance } module_keyword ... endmodule` — `(* optimize_power *) +// module M ... endmodule` is legal spec form. Field added at sha +// 7b7dd0b54+ per openai-pro REQUEST_CHANGES on PR #3176 sha +// f9159ce8b (Layer-Model BLOCKING: top-level module attributes had +// no typed home; reuses the existing AttributeInstanceClause Disj). +// No double-authority concern by grammar-level distinction (not by +// deferral-timing): the §A.1.2 / Syntax 3-4 attribute_instance +// prefix is INTRINSIC to the module_declaration production, +// attaching at the declaration boundary itself. The source_text +// design-element classifier (when the bundled T-4 LanguageModel +// lands it) is the description-level {module | udp | config} +// KIND-SELECTOR — a different grammar level that structurally +// NEVER carries attribute_instance. So there is no double-authority +// NOW NOR AFTER the wrapper lands: by spec grammar levels, the +// attribute_instance lives ON the declaration (here) and not on +// the kind-selector. +type VerilogModule + = NoPortListModule { + // `module M; ... endmodule` — the §A.1.2 `[list_of_ports]` / + // `[list_of_port_declarations]` brackets are ENTIRELY absent + // (no parens around the port-list position in the spec form). + // Style-neutral: with no header port-list, the §12.3.4 + // ANSI-vs-non-ANSI distinction loses meaning. Distinct from + // EmptyPortListModule below per §A.1.2 surface fact (parens- + // absent vs parens-present-empty) — openai-pro REQUEST_CHANGES + // on PR #3176 sha cb028c7d at line 4021: prior NoPortsModule + // conflated these two distinct spec forms, losing a §A.1.2 + // surface fact the language model otherwise preserves for + // parse/emit fidelity. Items use the AnsiModuleItem set + // (excludes body port_declaration variants — body + // port_declarations would reference non-existent header port + // names per §12.3.4). + attributes: AttributeInstanceClause, + module_keyword: ModuleKeyword, + name: Symbol, + parameter_port_list: ModuleParameterPortList, + items: List + } + | EmptyPortListModule { + // `module M (); ... endmodule` — the §A.1.2 port-list brackets + // are PRESENT but the inner list is EMPTY. Distinct spec + // surface from NoPortListModule above (parens-present-empty + // vs parens-absent). Same style-neutrality and item-set + // reasoning as NoPortListModule (no header ports → no body + // port_declarations admissible). Variant added at sha + // cb028c7d+ per openai-pro REQUEST_CHANGES (line 4021). + attributes: AttributeInstanceClause, + module_keyword: ModuleKeyword, + name: Symbol, + parameter_port_list: ModuleParameterPortList, + items: List + } + | NonAnsiVerilogModule { + attributes: AttributeInstanceClause, + module_keyword: ModuleKeyword, + name: Symbol, + parameter_port_list: ModuleParameterPortList, + // 🟡 spec-non-empty (§12.3.4 non-ANSI module-header port list) — + // non-ANSI modules WITH a header port-list have at least one + // port (the no-ports case routes to NoPortsModule above); + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + header_ports: List, + items: List + } + | AnsiVerilogModule { + attributes: AttributeInstanceClause, + module_keyword: ModuleKeyword, + name: Symbol, + parameter_port_list: ModuleParameterPortList, + // 🟡 spec-non-empty (§12.3.4 ANSI module-header port list) — + // ANSI modules WITH a header port-list have at least one + // port (the no-ports case routes to NoPortsModule above); + // deferred to std/collection.dag Wave-A2 `List where + // non_empty` refinement; see shared TRACKED-SCAFFOLD note above. + header_ports: List, + items: List + } + + +// ───────────────────────────────────────────────────────────────────── +// (The file-level §A.1.1 source_text design-element Disj +// aggregating VerilogModule + UdpDefinition is DELIBERATELY NOT +// declared in this file — relayed disposition from T-4 mgr +// vivid-carp-207 msg_f2a511b6, 2026-05-16; same shape as the +// NonEmptyList → std/collection.dag Wave-A2 deferral. +// +// Three anchors: +// 1. TASKS.md:504 (verbatim, dispositive): "A local Byte/Word +// copy or private language-model schema is invalid." The +// source_text design-element classifier IS the canonical +// LanguageModel contract spine (top-level compilation-unit +// composition), not verilog-private grammar; minting it +// locally is the v3 cross-layer spine-drift this directive +// exists to prevent (every language file otherwise hits +// "source_text needs a design-element classifier" → 5-language +// parallel-declaration precedent). +// 2. P2 single-authority + canonical-LanguageModel-first +// directive (TASKS.md 457/473/504): the design-element +// aggregator is owned by the canonical T-4 LanguageModel +// grammar-productions work — already the named owner in +// UdpDefinition's FILE-LEVEL DESIGN-ELEMENT NOTE. +// 3. Codex's gap finding is spec-right (the §A.1.1 partition +// should exist somewhere), but the FORM is the deferred +// canonical-LanguageModel obligation, not a verilog-local +// mint. Same pattern the NonEmptyList HOLD established. +// +// In-scope vocabulary carriers at file scope: VerilogModule (the +// per-style Disj declared above) + UdpDefinition (the Conj +// declared earlier alongside UdpInstantiation). The bundled +// T-4 LanguageModel grammar productions, when they land, aggregate +// these two file-level carriers into the canonical source_text +// design-element classifier — `config_declaration` is admitted by +// that canonical Disj when its sub-language lands (scope-negative +// here per the header PROBE LIMITS framing). The FILE-LEVEL +// DESIGN-ELEMENT NOTE in UdpDefinition's commentary is the single +// source-of-truth deferral marker; verilog.dag does NOT mint the +// design-element Disj locally.) + + +// ───────────────────────────────────────────────────────────────────── +// VerilogCost — the per-target cost-realization carrier shape for the +// Verilog `LanguageModel`. Conj record (no Practice-4 ledger). +// +// This declares the SHAPE the U1 spine reads when computing Verilog- +// target realization cost — the scaffold header's "Cost realization: +// per-construct cost on a Verilog target" claim: +// +// - gate_cost per-construct gate-count cost (an XOR, AND, OR +// primitive's gate equivalent; the U1 per-target- +// op cost projection — the `map` side of +// `Homomorphism<…, …, VerilogBits>` carries this; +// cost is read FROM the map's structure, never +// stored as a parallel field per algebra.dag's U1 +// no-engine discipline) +// - area_cost per-construct area cost (in technology-dependent +// units — gate equivalents in a generic process, +// LUT count on FPGA, transistor count on ASIC; +// the technology-specific cost table sits in the +// inhabitance walk that the T-4 LanguageModel +// shape parameterizes when it lands, not in this +// carrier itself) +// +// Both Int carriers are 🟡 scaffold (same bridge as VectorRange and +// ptx Dim3): cost is a non-negative quantity, but without +// std/cardinality.dag refinement the negative-cost state is +// structurally representable. Producer-side invariant pending the +// cardinality substrate landing. +type VerilogCost { + gate_cost: Int + area_cost: Int +}