vj-sim 0.3.0

//! The per-design, per-instance, runtime-mutable timing table every
//! SDF-annotatable value lives in (`docs/superpowers/plans/2026-10-03-sdf.md`
//! §1.1/§1.3, Task 2). Path delays, pulse limits, timing-check limits and
//! specparam values are never baked as Rust closures' captured constants or
//! LLVM constants — they are entries in [`TimingModel`], read fresh by the
//! delay-line/timing-check processes (Track A/B, `vj::specify`/
//! `vj::timingcheck`) on every firing, so a later `$sdf_annotate`
//! call (Track C) can mutate them in place mid-run with zero interaction
//! with codegen.
//!
//! Like every other `sv_lang`-touching file in this module (`dedup.rs`,
//! `elaborate.rs`, `instance.rs`, `items.rs`...), this one lives behind the
//! `frontend` feature: its key type, [`crate::symid::SymbolId`], is itself
//! `frontend`-gated, so there is no narrower cfg split available for this
//! file alone. "No `sv_lang` dependency on the mutation path"
//! (Task 2's own acceptance text) is therefore a *data*-dependency claim,
//! not a crate-dependency one: [`TimingModel::set_specparam`] — what a
//! later `$sdf_annotate` `LABEL` annotation (Task 28) calls from
//! `vj-runtime` through this crate's `frontend`-enabled build — takes
//! no `EvalSession`/live `Design`/`Symbol`, only the plain, fully-owned
//! `sv_lang::ConstantValue` (which, unlike most `sv_lang` types, carries no
//! `'d` lifetime at all — see its own doc comment) and this module's own
//! key types. Only [`TimingModel::seed_specparams`] needs a live `Design`'s
//! `Symbol`s at all.
//!
//! Task 2 is a module skeleton only: [`PathEntry`]/[`CheckEntry`] are bare
//! shells (just enough shape for [`TimingModel`]'s two `Vec`s to exist) —
//! Track A (`T3`-`T11`) and Track B (`T13`+) fill in the rest of §1.1's own
//! field list as each construct's discovery/planning lands.

use std::collections::HashMap;

use sv_lang::kinds::{ExpressionKind, SyntaxKind};
use sv_lang::nodes::{
    ConditionalPathDeclarationSyntax, IfNonePathDeclarationSyntax, PathDeclarationSyntax,
    PathSuffixSyntax,
};
use sv_lang::{
    ArgumentDirection, BinaryOp, Bit, ConstantValue, EvalSession, Expression, PulseStyleKind,
    Symbol, SyntaxTree, TimingPathPolarity, UnaryOp,
};
use sv_lang_kinds::SymbolKind;
use vj_abi::bit4::Bit4;

use super::{ElabError, InstanceId};
use crate::symid::{SymbolId, SymbolUid, is_value_name};

pub use crate::timing_types::{
    CondBinaryOp, CondUnaryOp, EdgeControl, EdgeSet, EdgeTransition, PathDelaySet, PulseStyle,
    TRANSITIONS,
};

/// A module-path terminal, resolved to its signal and (for a bit-select or
/// part-select terminal) the bit window within it: `(lo, width)`, `lo` the
/// least significant bit index and `width` the number of bits. `None` for a
/// terminal that names the whole signal.
pub type TerminalRef = (SymbolId, Option<(u32, u32)>);

/// A module path's own edge-sensitivity (LRM 1800-2023 §30.4.3, Task 7 —
/// `docs/superpowers/plans/2026-10-03-sdf.md`).
///
/// Derived from TWO sv-lang accessors together, never one alone:
/// `Symbol::timing_path_edge_identifier()` alone cannot distinguish "this is
/// a plain, non-edge-sensitive path" from "this is an edge-sensitive path
/// with no edge keyword written" — BOTH report [`sv_lang::EdgeKind::None`]
/// (verified live against sv-lang=0.1.9/slang 11.0: `(posedge clk => q) =
/// 1;` — the edge-sensitive grammar's OWN "simple destination" alternative,
/// no `(dest:data)` suffix at all — reports `PosEdge`, proving the
/// identifier is a direct field of the edge-sensitive grammar's shared
/// `[edge_identifier]` production regardless of which destination suffix
/// alternative is used; `(clock => (out:in))=10;` — LRM 30.4.3's own
/// Example 3, no edge keyword at all but WITH the `(dest:data)` suffix —
/// reports `None` for the identifier yet `Some` for
/// `timing_path_edge_source_expr()`; a PLAIN 30.4.2 simple path reports
/// `None`/`None` for both). So the discriminator for "is this path
/// edge-sensitive AT ALL" is `identifier != EdgeKind::None ||
/// edge_source_expr().is_some()`, and [`PathEdge::Any`] is exactly the
/// "edge-sensitive, but no keyword written" case LRM 30.4.3's own text
/// gives an explicit rule for: "If the edge transition is not specified,
/// the path shall be considered active on any transition at the input
/// terminal."
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum PathEdge {
    /// Not an edge-sensitive path at all (LRM 30.4.2 simple paths, 30.4.5
    /// full/parallel connection paths with no edge-sensitive suffix) — no
    /// edge gating whatsoever; `vj::specify::PathRetimer` fires on
    /// any transition of the destination's own staging cell, exactly the
    /// pre-Task-7 behavior every earlier task's fixture already exercises.
    None,
    /// An edge-sensitive path (30.4.3) with no `edge_identifier` written —
    /// gated on "any transition at the input terminal" (30.4.3's own text,
    /// quoted above), i.e. `from != to` on the member's own input, with no
    /// further direction requirement.
    Any,
    /// An edge-sensitive path with a specific `posedge`/`negedge`/`edge`
    /// identifier — never [`sv_lang::EdgeKind::None`] here (that raw value
    /// is exactly what distinguishes [`PathEdge::None`]/[`PathEdge::Any`]
    /// from this variant in the first place, so constructing `Specific`
    /// with `EdgeKind::None` would be a caller bug, not a real state; see
    /// [`PathEdge::from_accessors`]'s own body, the only constructor).
    Specific(sv_lang::EdgeKind),
}

impl PathEdge {
    /// The one, single call site for `Symbol::timing_path_edge_source_expr()`
    /// across this whole crate — returns the derived [`PathEdge`] alongside
    /// the edge-sensitive suffix's own data-source expression (LRM 30.4.3:
    /// "an arbitrary expression, which serves as a description of the flow
    /// of data to the path destination. This arbitrary data path
    /// description does not affect the actual propagation of data or
    /// events"), so a caller that also wants to store that expression for
    /// debug/VPI purposes (never for simulation effect — Task 7's own
    /// acceptance text) never needs a second call of its own.
    fn from_accessors<'d>(path: &Symbol<'d>) -> (PathEdge, Option<Expression<'d>>) {
        let identifier = path.timing_path_edge_identifier();
        let source = path.timing_path_edge_source_expr();
        let edge = if identifier != sv_lang::EdgeKind::None {
            PathEdge::Specific(identifier)
        } else if source.is_some() {
            PathEdge::Any
        } else {
            PathEdge::None
        };
        (edge, source)
    }
}

impl CondUnaryOp {
    /// `None` for any of `UnaryOp`'s other six variants (`Plus`/`Minus`/the
    /// four pre/post-increment/decrement forms) -- none of which Table
    /// 30-1 lists, so none is a legal state-dependent-path condition
    /// operator.
    fn from_sv(op: UnaryOp) -> Option<CondUnaryOp> {
        match op {
            UnaryOp::BitwiseNot => Some(CondUnaryOp::BitwiseNot),
            UnaryOp::BitwiseAnd => Some(CondUnaryOp::ReductionAnd),
            UnaryOp::BitwiseOr => Some(CondUnaryOp::ReductionOr),
            UnaryOp::BitwiseXor => Some(CondUnaryOp::ReductionXor),
            UnaryOp::BitwiseNand => Some(CondUnaryOp::ReductionNand),
            UnaryOp::BitwiseNor => Some(CondUnaryOp::ReductionNor),
            UnaryOp::BitwiseXnor => Some(CondUnaryOp::ReductionXnor),
            UnaryOp::LogicalNot => Some(CondUnaryOp::LogicalNot),
            UnaryOp::Plus
            | UnaryOp::Minus
            | UnaryOp::Preincrement
            | UnaryOp::Predecrement
            | UnaryOp::Postincrement
            | UnaryOp::Postdecrement => None,
        }
    }
}

impl CondBinaryOp {
    /// The operator set of a timing check's `&&&`/timestamp/timecheck
    /// condition (LRM 31.7, `scalar_timing_check_condition`: `==`, `===`,
    /// `!=`, `!==`, and the Table 30-1 operators slang's own parse allows):
    /// [`Self::from_sv`]'s set plus the two case-equality operators.
    fn from_sv_check(op: BinaryOp) -> Option<CondBinaryOp> {
        match op {
            BinaryOp::CaseEquality => Some(CondBinaryOp::CaseEquality),
            BinaryOp::CaseInequality => Some(CondBinaryOp::CaseInequality),
            other => CondBinaryOp::from_sv(other),
        }
    }

    /// `None` for every other `BinaryOp` variant (arithmetic, relational,
    /// shift, power, case/wildcard (in)equality, implication/equivalence)
    /// -- Table 30-1 lists none of them.
    fn from_sv(op: BinaryOp) -> Option<CondBinaryOp> {
        match op {
            BinaryOp::BinaryAnd => Some(CondBinaryOp::BitwiseAnd),
            BinaryOp::BinaryOr => Some(CondBinaryOp::BitwiseOr),
            BinaryOp::BinaryXor => Some(CondBinaryOp::BitwiseXor),
            BinaryOp::BinaryXnor => Some(CondBinaryOp::BitwiseXnor),
            BinaryOp::Equality => Some(CondBinaryOp::Equality),
            BinaryOp::Inequality => Some(CondBinaryOp::Inequality),
            BinaryOp::LogicalAnd => Some(CondBinaryOp::LogicalAnd),
            BinaryOp::LogicalOr => Some(CondBinaryOp::LogicalOr),
            BinaryOp::Add
            | BinaryOp::Subtract
            | BinaryOp::Multiply
            | BinaryOp::Divide
            | BinaryOp::Mod
            | BinaryOp::CaseEquality
            | BinaryOp::CaseInequality
            | BinaryOp::GreaterThanEqual
            | BinaryOp::GreaterThan
            | BinaryOp::LessThanEqual
            | BinaryOp::LessThan
            | BinaryOp::WildcardEquality
            | BinaryOp::WildcardInequality
            | BinaryOp::LogicalImplication
            | BinaryOp::LogicalEquivalence
            | BinaryOp::LogicalShiftLeft
            | BinaryOp::LogicalShiftRight
            | BinaryOp::ArithmeticShiftLeft
            | BinaryOp::ArithmeticShiftRight
            | BinaryOp::Power => None,
        }
    }
}

/// A state-dependent path's own `if (cond)` conditional expression (LRM
/// 30.4.4.1, Task 8), resolved to data that needs no further `sv_lang`/live
/// `Design` access to evaluate -- the same "discover the SHAPE now,
/// evaluate the VALUE later, against live simulation state" split
/// [`PathEntry::delays`]'s own doc comment already establishes, except a
/// condition's VALUE is never baked even once at plan time (unlike a
/// delay): LRM 30.4.4.1's own operand list ("module input/inout ports...
/// locally defined variables or nets... compile-time constants") means a
/// condition's truth genuinely depends on LIVE simulation state, re-read on
/// every check (`vj::specify`'s own `CondEval`, this type's
/// plan-time-`Loc`/register-time-`Place`-resolved sibling, is the runtime
/// evaluator -- this crate carries only the symbolic shape).
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum CondNode {
    /// A signal terminal (whole signal, or a constant bit-select/
    /// part-select of one) -- LRM 30.4.4.1's own "ports... variables or
    /// nets... or their bit-/part-selects".
    Signal(TerminalRef),
    /// A `Specparam` symbol -- LRM 30.4.4.1's own "compile-time constants
    /// (constant numbers and specify parameters)". Resolved against
    /// `TimingModel::specparam` at `vj::specify::plan` time (not
    /// evaluated here, and not carried as a live value past that point --
    /// see that crate's own `compile_cond_plan` doc comment for why a
    /// condition's specparam operand is, as of this task, baked once at
    /// plan time rather than re-read on every check the way a `Signal`
    /// leaf is).
    Specparam(SymbolId),
    /// A plain compile-time-constant value (LRM 30.4.4.1's own "constant
    /// numbers"), already evaluated at discovery time -- LSB-first, in
    /// [`sv_lang::SVInt::bits`]'s own bit order.
    Const(Vec<Bit4>),
    Unary(CondUnaryOp, Box<CondNode>),
    Binary(CondBinaryOp, Box<CondNode>, Box<CondNode>),
    /// `c ? t : f` -- the plain (non-pattern-matching) ternary form only;
    /// a `&&&`-chained pattern-matching conditional is rejected at
    /// [`compile_cond_expr`] (Table 30-1 does not list it).
    Ternary(Box<CondNode>, Box<CondNode>, Box<CondNode>),
    /// `{a, b, ...}`, in SOURCE order (first element MSB-most, matching
    /// `Expression::operands()`'s own documented order) -- never
    /// reordered here; `vj::specify`'s own runtime evaluator is
    /// where MSB-first source order meets this crate's own LSB-first
    /// per-bit storage convention.
    Concat(Vec<CondNode>),
    /// `{n{x}}` -- `n`, the replication count, already evaluated to a
    /// compile-time constant at discovery time (LRM 11.4.12.1's own
    /// requirement, verified live: slang already enforces this upstream).
    Replication(u32, Box<CondNode>),
}

/// A `TimingPath`'s own state-dependency (LRM 30.4.4, Task 8): which of
/// 30.4.4's three forms -- unconditional, `if (cond)`, or `ifnone` -- this
/// path was declared with. Discriminated jointly from `Symbol::
/// timing_path_is_state_dependent()` and `Symbol::
/// timing_path_condition_expr()` (see [`resolve_condition`]'s own doc
/// comment for why neither alone suffices -- this plan's own "What already
/// exists" section's decision 0).
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum PathCondition {
    /// A plain, unconditional module path (30.4.2/30.4.3/30.4.5) -- the
    /// pre-Task-8 default every earlier task's own fixture already
    /// exercises.
    Unconditional,
    /// `if (cond) ...` -- `cond`, compiled to a [`CondNode`].
    If(CondNode),
    /// `ifnone ...` -- LRM 30.4.4.4: active whenever every OTHER
    /// state-dependent declaration sharing this path's own exact source
    /// and destination is false (`vj::specify::plan`'s own
    /// `ifnone_gate` synthesizes this from its sibling `If` members'
    /// conditions; a path with no such siblings behaves as
    /// [`Self::Unconditional`], per that same subclause's own text).
    IfNone,
}

/// A `TimingPath` (LRM §30.4), post multi-path desugaring (30.4.6): one
/// [`PathEntry`] per individual module path assignment, after a multi-input/
/// multi-output full-connection declaration (`(a, b, c *> q1, q2) = 10;`)
/// has been expanded into its six (here: `inputs.len() * outputs.len()`)
/// one-to-one assignments per 30.4.6's own worked example. `inputs`/
/// `outputs` therefore always have exactly one element each as of this task
/// (Task 3) — kept as `Vec` (matching the plan's own §1.1 pseudocode)
/// because a later task's vector-terminal handling reads them the same way
/// regardless of how many elements they end up holding.
///
/// Bare shell beyond this — Track A (Task 4a onward) fills in the rest of
/// §1.1's own field list (`polarity`/`edge`/`condition`/`delays`/
/// `reject_limit`/`error_limit`/`pulse_style`/`showcancelled`).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct PathEntry {
    /// The instance the path's declaration lives in.
    pub instance: InstanceId,
    /// This path's one resolved source terminal (LRM 30.4.1: always a net).
    pub inputs: Vec<TerminalRef>,
    /// This path's one resolved destination terminal (LRM 30.4.1: a net or
    /// a variable).
    pub outputs: Vec<TerminalRef>,
    /// `*>` (`Full`) or `=>` (`Parallel`) — metadata only at this task; T4a
    /// is where it starts to matter (full connection's fan-in/fan-out vs.
    /// parallel's bit-paired semantics).
    pub connection: sv_lang::TimingPathConnectionKind,
    /// This path's own overall polarity (LRM §30.4.7: the `+`/`-` on the
    /// path operator itself, e.g. the `+` of `(a +*> b) = 1;` — `path.
    /// timing_path_polarity()`, NOT `timing_path_edge_polarity()`, which is
    /// an edge-sensitive path's own, separate destination-suffix polarity
    /// and T7's scope, not this one). Per §30.4.7.1/.2/.3's own text — "does
    /// not affect the actual propagation of data" — this is metadata ONLY:
    /// stored here so a debug/VPI-facing accessor ([`PathEntry::polarity`])
    /// can read it back, and never consulted by any delay/timing
    /// computation. `vj::specify::PathRetimer` — the only runtime
    /// reader of a [`PathEntry`]'s timing data — never reads this field (its
    /// own fields are `src`/`delays`/`prev`/`shared`/`kick`, and `plan`
    /// never copies `polarity` into `RetimerPlan`); see that crate's own
    /// `path_retimer_never_reads_polarity_in_its_delay_computation` test for
    /// the behavioral proof.
    pub polarity: TimingPathPolarity,
    /// The ORIGINAL (pre-desugaring) `TimingPath` symbol's own identity
    /// (LRM 30.4.6): several desugared [`PathEntry`]s share one `path_uid`
    /// when they came from one multi-terminal declaration, since they also
    /// share its one delay list. `vj`'s own plan-time delay
    /// evaluation (Task 4a) uses it to re-locate that original symbol --
    /// see [`PathEntry::delays`]'s own doc comment for why evaluation
    /// cannot happen inside this crate.
    pub path_uid: SymbolId,
    /// This path's own 12-entry transition-delay table (LRM Table 30-2/
    /// 30-3), in scheduler ticks. [`PathDelaySet::default()`] (all zero)
    /// until `vj`'s own plan-time pass attaches the real,
    /// timescale-converted value via [`TimingModel::set_path_delays`] --
    /// evaluating a `path_delay_value` expression needs both
    /// `sv_lang::EvalSession` (constant-folding) and `vj-codegen::
    /// timescale` (unit/precision conversion); this crate's own `frontend`
    /// feature carries the former but can never depend on the latter
    /// (`vj-codegen` depends on `vj-sim`, never the reverse), so
    /// the two-step "discover the SHAPE, then attach the VALUE" split this
    /// field forces mirrors [`TimingModel::set_specparam`]'s own,
    /// already-established precedent exactly. Never read before that
    /// attach call runs (`crate::specify::discover`'s own call order,
    /// `vj`'s `run.rs` wiring) -- the module-path retimer process
    /// is the only runtime reader, and it is planned strictly after this
    /// field is set.
    pub delays: PathDelaySet,
    /// This path's own edge-sensitivity (LRM 30.4.3, Task 7) — see
    /// [`PathEdge`]'s own doc comment. [`vj::specify::PathRetimer`]
    /// is the only runtime reader, and reads it to GATE which of this
    /// destination's candidate module paths are "active" for a given
    /// transition (LRM 30.4.3's own text: "which only occur when a
    /// specified edge occurs at the source signal"), never to decide the
    /// destination's VALUE (still never this module's job — decision 3,
    /// unchanged by this task).
    pub edge: PathEdge,
    /// The edge-sensitive suffix's own data-source expression (LRM 30.4.3:
    /// "the `d` of `(posedge clk => (q +: d))`"), reduced to its referenced
    /// symbol's own name for debug/VPI purposes — `None` both for a
    /// non-edge-sensitive path and for an edge-sensitive one whose data
    /// source is not a plain named reference (an arbitrary expression per
    /// the LRM's own text; losing fidelity for a complex expression is
    /// harmless, since this field is documented, by both the LRM ("does not
    /// affect the actual propagation of data or events") and this crate's
    /// own [`Self::debug_edge_source_expr_name`] accessor, as read ONCE
    /// here (via [`PathEdge::from_accessors`], [`Self::edge`]'s own sibling
    /// value from the SAME call) and never again — see
    /// `vj::specify`'s own
    /// `edge_source_expr_text_never_affects_scheduled_timing` test for the
    /// behavioral proof.
    pub edge_data_source_name: Option<String>,
    /// This path's own state-dependency (LRM 30.4.4, Task 8) -- see
    /// [`PathCondition`]'s own doc comment. `vj::specify::
    /// PathRetimer::select_delay` reads it (through `vj`'s own
    /// plan-time `CondPlan`/register-time `CondEval` compilation of the
    /// `CondNode` it carries) to gate this entry's own eligibility
    /// alongside [`Self::edge`]'s existing edge gate -- both decision 3's
    /// "only when a specify path is actually active for it."
    pub condition: PathCondition,
    /// This path's own per-transition REJECT limit (LRM 30.7, Task 10), in
    /// scheduler ticks: an output pulse narrower than the limit of the
    /// delay that forms its TRAILING edge is cancelled outright. Defaults
    /// (LRM 30.7: "if no limits are specified, they default to the path
    /// delay") to [`Self::delays`] itself -- every transition's own delay --
    /// which is exactly full inertial delay; [`TimingModel::set_path_delays`]
    /// re-establishes that default every time a path's delays are (re)set,
    /// and [`TimingModel::set_path_pulse_limits`] (a `PATHPULSE$`) overrides
    /// it afterwards.
    pub reject_limit: PathDelaySet,
    /// This path's own per-transition ERROR limit (LRM 30.7, Task 10): an
    /// output pulse at least as wide as the reject limit but narrower than
    /// this one is filtered to `x`; one at least this wide passes. Same
    /// default and override rules as [`Self::reject_limit`]. Never smaller
    /// than it (see [`TimingModel::set_path_pulse_limits`]).
    pub error_limit: PathDelaySet,
    /// This path's own output's pulse style (LRM 30.7.4.1, Task 11): whether
    /// the `x` that marks a filtered pulse (or, with [`Self::showcancelled`],
    /// a negative pulse) starts at the leading edge's scheduled time or at the
    /// moment the pulse is detected. [`PulseStyle::OnEvent`] unless a
    /// `pulsestyle_ondetect` declaration names an output window overlapping
    /// this path's own ([`TimingModel::discover`] applies the declarations).
    pub pulse_style: PulseStyle,
    /// Whether this path's own output shows a negative pulse (LRM 30.7.4.2,
    /// Task 11) as `x` rather than cancelling it: `false` (`noshowcancelled`,
    /// the LRM's own default) unless a `showcancelled` declaration names an
    /// overlapping output window. Same application rule as
    /// [`Self::pulse_style`]; the two settings are independent.
    pub showcancelled: bool,
}

impl PathEntry {
    /// This path's own overall polarity (see [`Self::polarity`]'s own field
    /// doc) — the debug/VPI-facing accessor the plan's own Task 4a
    /// acceptance text asks for. Metadata only: never called by
    /// `vj::specify::PathRetimer`'s delay computation, only by a
    /// debugger/VPI host wanting to report a path's declared polarity back
    /// to the user.
    pub fn debug_polarity(&self) -> TimingPathPolarity {
        self.polarity
    }

    /// This path's own edge-sensitive data-source expression, reduced to a
    /// debug name (see [`Self::edge_data_source_name`]'s own field doc) —
    /// the Task 7 sibling of [`Self::debug_polarity`]: metadata only, never
    /// called by `vj::specify::PathRetimer`'s delay computation.
    pub fn debug_edge_source_expr_name(&self) -> Option<&str> {
        self.edge_data_source_name.as_deref()
    }
}

impl EdgeControl {
    /// The control of "the reference event signal with opposite edge" (LRM
    /// 31.4.4, `$width`'s derived data event; `$nochange`'s trailing edge is the
    /// same derivation): every transition reversed. `None` for
    /// [`EdgeControl::AnyChange`], which has no direction to oppose -- a check
    /// that needs this has an edge-specified reference (T13 enforces it), so a
    /// caller meeting `None` reports it by name rather than guessing.
    pub fn opposite(self) -> Option<EdgeControl> {
        match self {
            EdgeControl::AnyChange => None,
            EdgeControl::Edges(set) => Some(EdgeControl::Edges(set.reversed())),
        }
    }

    /// Resolves the parsed `edge` / `edge_descriptors` pair of a
    /// `SystemTimingCheckArg` (sv-lang keeps the descriptors as written).
    ///
    /// * `posedge`/`negedge` are the lists LRM 31.5 states they abbreviate;
    /// * `edge [d, ...]` is the union of its descriptors;
    /// * a bare `edge` (no list) is NOT defined by 31.5's text. It is taken as
    ///   all six transitions -- "any edge", as 9.4.2's `@(edge e)` -- chosen
    ///   once here.
    ///
    /// A descriptor that is not one of the six, or a descriptor list on
    /// anything but `edge`, is a named `Err` (slang rejects the former at
    /// parse time; this is the backstop for an sv-lang that stops doing so).
    pub fn from_syntax(edge: sv_lang::EdgeKind, descriptors: &[String]) -> Result<Self, String> {
        use sv_lang::EdgeKind as K;
        match (edge, descriptors.is_empty()) {
            (K::None, true) => Ok(EdgeControl::AnyChange),
            (K::PosEdge, true) => Ok(EdgeControl::Edges(EdgeSet::POSEDGE)),
            (K::NegEdge, true) => Ok(EdgeControl::Edges(EdgeSet::NEGEDGE)),
            (K::BothEdges, true) => Ok(EdgeControl::Edges(EdgeSet::ALL)),
            (K::BothEdges, false) => {
                let mut set = EdgeSet::EMPTY;
                for d in descriptors {
                    let t = EdgeTransition::of_descriptor(d).ok_or_else(|| {
                        format!(
                            "edge descriptor `{d}` is not one of 01, 10, 0x, x0, 1x, x1 (z \
                             allowed for x, LRM 31.5)"
                        )
                    })?;
                    set = set.with(t);
                }
                Ok(EdgeControl::Edges(set))
            }
            (K::None | K::PosEdge | K::NegEdge, false) => Err(format!(
                "an edge descriptor list {descriptors:?} is only allowed on `edge [...]`, not \
                 on {edge:?} (LRM 31.5)"
            )),
        }
    }
}

/// One `timing_check_event` argument (LRM 31.3): a terminal, its optional
/// edge control, and its optional `&&& condition` (LRM 31.5/31.7).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CheckEvent {
    /// The signal (and bit window) the event watches.
    pub terminal: TerminalRef,
    /// `posedge`/`negedge` (`EdgeKind::PosEdge`/`NegEdge`), a bare `edge` or
    /// `edge [descriptors]` (`EdgeKind::BothEdges`), or [`EdgeKind::None`]
    /// for an event with no edge control (any value change).
    pub edge: sv_lang::EdgeKind,
    /// The `edge [01, 1x]` descriptor list as written (LRM Table 31-14),
    /// empty for every other form. Kept for diagnostics; the check process
    /// reads [`Self::edge_control`], which is this resolved.
    pub edge_descriptors: Vec<String>,
    /// [`Self::edge`] and [`Self::edge_descriptors`] resolved to the
    /// transitions that are this event (LRM 31.5), validated at discovery.
    pub edge_control: EdgeControl,
    /// The `&&&` qualifying condition (LRM 31.5/31.7), if any.
    pub condition: Option<CondNode>,
}

/// A timing check limit / threshold / offset argument. Discovery records only
/// WHERE it is (`arg_index`, the position in the check's own argument list);
/// its VALUE needs `sv_lang::EvalSession` plus the timescale, neither
/// reachable from this crate, so `vj::specify::discover` evaluates it
/// and attaches [`Self::ticks`] -- the SAME "discover the SHAPE, attach the
/// VALUE" split [`PathEntry::delays`] documents. `$sdf_annotate` (Track C)
/// overwrites `ticks` in place afterwards. Signed: LRM 31.9 allows negative
/// `$setuphold`/`$recrem` limits (and `$nochange` offsets).
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub struct CheckLimit {
    /// The argument's position in the check's own argument list (LRM Tables
    /// 31-1..31-12 numbering, zero-based).
    pub arg_index: u32,
    /// The limit in scheduler ticks; `0` until `vj` attaches it.
    pub ticks: i64,
}

/// The arguments shared by the five checks that take two events, one limit
/// and an optional notifier -- `$setup` (LRM 31.3.1), `$hold` (31.3.2),
/// `$recovery`, `$removal` (31.4), `$skew` (31.4.1). `$setup` alone lists its
/// DATA event first; the others list the reference event first. Decoding
/// puts each event in its own named field either way.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct EventPairArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    pub limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
}

/// `$setuphold` (LRM 31.3.3, Syntax 31-5): all nine positions.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SetupHoldArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    pub setup_limit: CheckLimit,
    pub hold_limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
    /// `timestamp_condition` (position 5), if given.
    pub timestamp_cond: Option<CondNode>,
    /// `timecheck_condition` (position 6), if given.
    pub timecheck_cond: Option<CondNode>,
    /// `delayed_reference` (position 7), if given.
    pub delayed_reference: Option<TerminalRef>,
    /// `delayed_data` (position 8), if given.
    pub delayed_data: Option<TerminalRef>,
}

/// `$recrem` (LRM 31.4.3, Syntax 31-8): the nine positions of
/// [`SetupHoldArgs`], with the limits named for their meaning (position 2 is
/// the RECOVERY limit, position 3 the REMOVAL limit).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct RecRemArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    pub recovery_limit: CheckLimit,
    pub removal_limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
    pub timestamp_cond: Option<CondNode>,
    pub timecheck_cond: Option<CondNode>,
    pub delayed_reference: Option<TerminalRef>,
    pub delayed_data: Option<TerminalRef>,
}

/// `$timeskew` (LRM 31.4.2, Syntax 31-10). A flag is `None` when elided, so
/// the LRM default is applied in exactly one place (the check's behavior).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct TimeSkewArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    pub limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
    pub event_based: Option<bool>,
    pub remain_active: Option<bool>,
}

/// `$fullskew` (LRM 31.4.3, Syntax 31-11).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct FullSkewArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    /// `timing_check_limit` (position 2): "the maximum time by which the
    /// data event should FOLLOW the reference event" -- i.e. the limit that
    /// applies when the reference event comes first.
    pub reference_first_limit: CheckLimit,
    /// The second limit (position 3): "the maximum time by which the
    /// reference event should follow the data event" -- applies when the
    /// data event comes first.
    pub data_first_limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
    pub event_based: Option<bool>,
    pub remain_active: Option<bool>,
}

/// `$period` (LRM 31.4.5, Syntax 31-13).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct PeriodArgs {
    pub reference: CheckEvent,
    pub limit: CheckLimit,
    pub notifier: Option<TerminalRef>,
}

/// `$width` (LRM 31.4.4, Syntax 31-12). `threshold` is `None` when elided
/// (LRM: "the default value for the threshold [is] zero").
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct WidthArgs {
    pub reference: CheckEvent,
    pub limit: CheckLimit,
    pub threshold: Option<CheckLimit>,
    pub notifier: Option<TerminalRef>,
}

/// `$nochange` (LRM 31.4.6, Syntax 31-14).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct NoChangeArgs {
    pub reference: CheckEvent,
    pub data: CheckEvent,
    pub start_edge_offset: CheckLimit,
    pub end_edge_offset: CheckLimit,
    pub notifier: Option<TerminalRef>,
}

/// A system timing check's arguments, decoded by the positional layout of
/// LRM 1800-2023 Tables 31-1..31-12 -- one variant per check kind.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum CheckArgs {
    Setup(EventPairArgs),
    Hold(EventPairArgs),
    SetupHold(SetupHoldArgs),
    Recovery(EventPairArgs),
    Removal(EventPairArgs),
    RecRem(RecRemArgs),
    Skew(EventPairArgs),
    TimeSkew(TimeSkewArgs),
    FullSkew(FullSkewArgs),
    Period(PeriodArgs),
    Width(WidthArgs),
    NoChange(NoChangeArgs),
}

impl CheckArgs {
    /// Every limit / threshold / offset this check carries, in argument
    /// order -- the slots `vj` attaches tick values to and
    /// `$sdf_annotate` (Track C) overwrites.
    pub fn limits_mut(&mut self) -> Vec<&mut CheckLimit> {
        match self {
            CheckArgs::Setup(a)
            | CheckArgs::Hold(a)
            | CheckArgs::Recovery(a)
            | CheckArgs::Removal(a)
            | CheckArgs::Skew(a) => vec![&mut a.limit],
            CheckArgs::SetupHold(a) => vec![&mut a.setup_limit, &mut a.hold_limit],
            CheckArgs::RecRem(a) => vec![&mut a.recovery_limit, &mut a.removal_limit],
            CheckArgs::TimeSkew(a) => vec![&mut a.limit],
            CheckArgs::FullSkew(a) => {
                vec![&mut a.reference_first_limit, &mut a.data_first_limit]
            }
            CheckArgs::Period(a) => vec![&mut a.limit],
            CheckArgs::Width(a) => {
                let mut v = vec![&mut a.limit];
                v.extend(a.threshold.as_mut());
                v
            }
            CheckArgs::NoChange(a) => vec![&mut a.start_edge_offset, &mut a.end_edge_offset],
        }
    }
}

/// A `SystemTimingCheck` (LRM §31.2), decoded.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CheckEntry {
    /// The instance the check's declaration lives in.
    pub instance: InstanceId,
    /// The `SystemTimingCheck` symbol's own identity, so `vj` can
    /// re-locate the symbol to evaluate [`CheckLimit`] values (see its doc).
    pub check_uid: SymbolId,
    pub kind: sv_lang::SystemTimingCheckKind,
    pub args: CheckArgs,
}

/// The per-design, runtime-mutable timing-annotation table (§1.1).
#[derive(Default)]
pub struct TimingModel {
    specparams: HashMap<(InstanceId, SymbolId), ConstantValue>,
    /// One per desugared [`PathEntry`] (Track A).
    pub paths: Vec<PathEntry>,
    /// One per [`CheckEntry`] (Track B).
    pub timing_checks: Vec<CheckEntry>,
    /// The pulse style invocation option (LRM 30.7.4.1: "The pulse style invocation options take
    /// precedence over pulse style specify block declarations"): `Some` overrides every
    /// `pulsestyle_*` declaration, `None` (no option given) leaves the declarations in force.
    pulse_style_option: Option<PulseStyle>,
    /// The `showcancelled` invocation option, the same way (LRM 30.7.4.2: "The showcancelled
    /// invocation options take precedence over the showcancelled specify block declarations").
    showcancelled_option: Option<bool>,
}

impl TimingModel {
    /// An empty table (no design has been seeded into it yet).
    pub fn new() -> TimingModel {
        TimingModel::default()
    }

    /// Seeds the specparam table from every `Specparam` member of each
    /// `(instance, body)` pair in `infos` — the SAME per-instance
    /// `(InstanceId, Symbol)` shape `vj::primitives::plan`'s own
    /// `bodies` parameter already uses — via [`super::module_items`] (the
    /// same discovery surface `primitives.rs` already walks). `Specparam`
    /// is a direct module member, legal both inside and outside a `specify`
    /// block (LRM 30.3). Stores each one's frozen `constant_value()` — the
    /// pre-SDF baseline a later `$sdf_annotate` `LABEL` annotation
    /// (Task 28) overwrites in place through [`Self::set_specparam`].
    ///
    /// A `specparam` declared INSIDE a `specify ... endspecify` block (LRM
    /// 30.3's own `specify_item` production lists `specparam_declaration`;
    /// 30.7.1's `PATHPULSE$` is only ever legal there) is not a direct
    /// `Specparam` member of `body` the way a module-scope one is:
    /// `module_items` deliberately leaves `SpecifyBlock` opaque (it only
    /// recurses into `GenerateBlock`/`GenerateBlockArray`, per that
    /// function's own doc comment — dedup.rs/elaborate.rs/instance.rs/
    /// primitives.rs all rely on that), so a `specify`-block specparam's
    /// real `Specparam` symbol is a child of the `SpecifyBlock` member
    /// itself, never surfaced by the `module_items` walk above. This loop
    /// therefore also looks inside every `SpecifyBlock` member it finds and
    /// seeds any `Specparam` declared directly in it, one level deep (a
    /// `specify` block cannot nest another one — 30.3 gives it no such
    /// production — so one level is exhaustive).
    ///
    /// Deviation from the plan's own pseudocode signature: no `&EvalSession`
    /// parameter. `Symbol::constant_value()` is documented as "a pure read
    /// on a frozen design... never evaluates" (sv-lang's own doc comment),
    /// so no session is needed here — the plan carried one for symmetry
    /// with `specify_eval::eval_specparam_aware`'s (which genuinely needs
    /// one, for its general-constant-folding fallback), not because seeding
    /// itself requires one.
    pub fn seed_specparams(&mut self, infos: &[(InstanceId, Symbol<'_>)]) {
        for &(id, body) in infos {
            for m in super::module_items(&body) {
                if m.kind() == SymbolKind::Specparam {
                    if let Some(v) = m.constant_value() {
                        self.specparams.insert((id, m.uid()), v);
                    }
                    continue;
                }
                if m.kind() != SymbolKind::SpecifyBlock {
                    continue;
                }
                for inner in m.members() {
                    if inner.kind() != SymbolKind::Specparam {
                        continue;
                    }
                    if let Some(v) = inner.constant_value() {
                        self.specparams.insert((id, inner.uid()), v);
                    }
                }
            }
        }
    }

    /// The specparam identified by `(instance, uid)`'s current value: the
    /// pre-SDF baseline [`seed_specparams`](Self::seed_specparams) stored,
    /// or whatever a later direct mutation ([`set_specparam`]
    /// (Self::set_specparam) — `$sdf_annotate`, Task 28) has since
    /// overwritten it with. A plain table lookup, needing no
    /// `EvalSession`/live `Design`.
    pub fn specparam(&self, instance: InstanceId, uid: &SymbolId) -> Option<&ConstantValue> {
        self.specparams.get(&(instance, uid.clone()))
    }

    /// Overwrites (or inserts) a specparam's value directly — what Task 28's
    /// real SDF `LABEL` annotation calls, and what this task's own unit
    /// tests use to simulate it ahead of time. This task's "mutation path"
    /// acceptance criterion: no `EvalSession`/`Design`/`Symbol` anywhere in
    /// this signature, only `InstanceId`/`SymbolId`/the plain, fully-owned
    /// `ConstantValue`.
    pub fn set_specparam(&mut self, instance: InstanceId, uid: SymbolId, value: ConstantValue) {
        self.specparams.insert((instance, uid), value);
    }

    /// Attaches `delays` to every desugared [`PathEntry`] that came from
    /// the one `TimingPath` symbol identified by `(instance, path_uid)`
    /// (LRM 30.4.6: several entries share one declaration, and all share
    /// its one delay list) -- `vj`'s own plan-time pass
    /// (`crate::specify::discover`, right after calling [`Self::discover`])
    /// is the only caller; see [`PathEntry::delays`]'s own doc comment for
    /// why evaluation lives there, not here. A no-op, never an error, if
    /// nothing matches -- [`Self::discover`]'s own loop already guarantees
    /// that a `path_uid` it produced has at least one entry, so a caller
    /// passing a `path_uid` it did not itself get from THIS SAME
    /// `TimingModel`'s own [`Self::paths`] is a caller bug, not a runtime
    /// condition this method needs to report.
    pub fn set_path_delays(
        &mut self,
        instance: InstanceId,
        path_uid: &SymbolId,
        delays: PathDelaySet,
    ) {
        for p in &mut self.paths {
            if p.instance == instance && &p.path_uid == path_uid {
                p.delays = delays;
                // LRM 30.7: absent a `PATHPULSE$`, both limits default to
                // each transition's own delay. Resetting them HERE (rather
                // than leaving them a separately-stored default) is what
                // makes a path whose delays are re-annotated keep
                // following its delay; a `PATHPULSE$` must therefore be
                // applied AFTER the delays (`set_path_pulse_limits`).
                p.reject_limit = delays;
                p.error_limit = delays;
            }
        }
    }

    /// Attaches a `PATHPULSE$` (LRM 30.7.1) -- `reject` and `error`, already
    /// evaluated and tick-converted by the caller exactly like
    /// [`Self::set_path_delays`]'s own delays (see that method for why
    /// evaluation lives in `vj`) -- to every desugared [`PathEntry`]
    /// of the one `TimingPath` symbol `(instance, path_uid)`; every
    /// transition of each gets the same two values.
    ///
    /// **Implementation-defined choice**: LRM 30.7.1 requires the error limit
    /// to be at least the reject limit but does not say what a source that
    /// writes `(6, 2)` means. Rather than reject a design over it, the error
    /// limit is raised to the reject limit (`error = max(error, reject)`),
    /// which makes the region between the two empty: a pulse is then either
    /// cancelled or passed, never filtered to `x`.
    ///
    /// Like [`Self::set_path_delays`], a no-op if nothing matches.
    pub fn set_path_pulse_limits(
        &mut self,
        instance: InstanceId,
        path_uid: &SymbolId,
        reject: u64,
        error: u64,
    ) {
        let error = error.max(reject);
        for p in &mut self.paths {
            if p.instance == instance && &p.path_uid == path_uid {
                p.reject_limit = PathDelaySet::uniform(reject);
                p.error_limit = PathDelaySet::uniform(error);
            }
        }
    }

    /// Sets every path's reject and error limit to `reject_pct` / `error_pct` percent of each
    /// transition's OWN delay (LRM 30.7.2, 32.7: the global invocation options), rounded to the
    /// nearest tick, an error limit below the reject limit raised to it (the same
    /// implementation-defined repair as [`Self::set_path_pulse_limits`]). `100.0` is exact (the
    /// LRM default, limits equal to the delays). A `PATHPULSE$` is more specific than this
    /// option and must be applied AFTER it ([`Self::set_path_pulse_limits`]); like
    /// [`Self::set_path_delays`], which re-establishes the default this replaces, it must come
    /// after the delays.
    pub fn apply_pulse_percent(&mut self, reject_pct: f64, error_pct: f64) {
        let scale = |v: u64, pct: f64| -> u64 {
            if pct == 100.0 {
                v
            } else {
                // A saturating float-to-int cast: a tick count beyond 2^53 loses low bits first,
                // an absurd delay for a pulse limit.
                (v as f64 * pct / 100.0).round() as u64
            }
        };
        for p in &mut self.paths {
            let delays = p.delays.transitions();
            let reject = delays.map(|d| scale(d, reject_pct));
            let error: [u64; 12] =
                std::array::from_fn(|i| scale(delays[i], error_pct).max(reject[i]));
            p.reject_limit = PathDelaySet::from_transitions(reject);
            p.error_limit = PathDelaySet::from_transitions(error);
        }
    }

    /// Sets the pulse style and `showcancelled` invocation options (LRM 30.7.4.1/30.7.4.2). An
    /// option that is `Some` takes precedence over every specify block declaration of its axis
    /// (the LRM's own wording), so [`Self::discover`] applies it AFTER the declarations; one that
    /// is `None` was not given and the declarations (then the built-in on-event /
    /// `noshowcancelled`) decide. Must be called BEFORE [`Self::discover`].
    pub fn set_pulse_options(&mut self, style: Option<PulseStyle>, showcancelled: Option<bool>) {
        self.pulse_style_option = style;
        self.showcancelled_option = showcancelled;
    }

    /// Walks every `(instance, body)` pair's `SpecifyBlock` members
    /// (Task 3, `docs/superpowers/plans/2026-10-03-sdf.md`), appending one
    /// [`PathEntry`] per desugared module path to [`Self::paths`] and one
    /// [`CheckEntry`] per `SystemTimingCheck` to [`Self::timing_checks`]
    /// ([`discover_check`] decodes its arguments by kind and enforces the
    /// clause's compile-time restrictions as named errors, Task 13).
    ///
    /// `SpecifyBlock`'s own member-kind match is exhaustive over LRM 30.3's
    /// `specify_item` production (`specparam_declaration` |
    /// `path_declaration` | `system_timing_check` |
    /// `pulsestyle_declaration`/`showcancelled_declaration`, i.e.
    /// `SymbolKind::{Specparam,TimingPath,SystemTimingCheck,PulseStyle}`):
    /// any other member kind is a named [`ElabError::UnsupportedConstruct`],
    /// never a silent skip, matching this crate's own top-of-file
    /// discipline. `Specparam` members are skipped here (already seeded by
    /// [`Self::seed_specparams`]); `PulseStyle` members (Task 11:
    /// `pulsestyle_onevent`/`_ondetect`/`showcancelled`/`noshowcancelled`) are
    /// validated against LRM 30.7.4.1/30.7.4.2's declaration-order rule as
    /// they are met, then applied to the `PathEntry`s whose outputs they name
    /// once the module's whole specify content has been walked
    /// ([`discover_pulse_style`], [`apply_pulse_style_declarations`]).
    ///
    /// A `TimingPath` whose desugaring would need [`EvalSession::
    /// eval_constant`] (a bit-select/part-select terminal whose index is
    /// not already folded) is why this method takes `eval`, unlike
    /// [`Self::seed_specparams`] — mirrors `specify_eval::
    /// eval_specparam_aware`'s own reason for carrying one.
    pub fn discover<'d>(
        &mut self,
        eval: &EvalSession<'d>,
        infos: &[(InstanceId, Symbol<'d>)],
    ) -> Result<(), ElabError> {
        // Needed only by `syntax_terminal_counts` (the sibling-terminal-drop
        // check `discover_path` runs after sv-lang's own per-terminal LRM
        // 30.4.1 filtering) -- computed once here, mirroring `run.rs`'s own
        // single `eval.design().syntax_trees()` call reused across every
        // instance, rather than once per path.
        let trees = eval.design().syntax_trees();
        for &(id, body) in infos {
            let ports = port_directions(&body);
            // Task 11: every pulse style / showcancelled declaration of this
            // instance, in source order across all its specify blocks; applied
            // to the paths once the whole module has been walked.
            let mut declarations: Vec<(TerminalRef, PulseStyleKind)> = Vec::new();
            for m in super::module_items(&body) {
                if m.kind() != SymbolKind::SpecifyBlock {
                    continue;
                }
                for inner in m.members() {
                    match inner.kind() {
                        SymbolKind::Specparam => {}
                        SymbolKind::TimingPath => {
                            self.paths
                                .extend(discover_path(eval, id, &inner, &ports, &trees)?);
                        }
                        SymbolKind::PulseStyle => {
                            declarations.extend(discover_pulse_style(
                                eval,
                                id,
                                &inner,
                                &ports,
                                &self.paths,
                            )?);
                        }
                        SymbolKind::SystemTimingCheck => {
                            self.timing_checks.push(discover_check(eval, id, &inner)?);
                        }
                        other => {
                            return Err(ElabError::UnsupportedConstruct {
                                hier_path: inner.hierarchical_path(),
                                detail: format!(
                                    "specify block member of kind `{other:?}` (LRM 30.3's own \
                                     specify_item production only allows specparam_declaration, \
                                     path_declaration, system_timing_check and \
                                     pulsestyle_declaration/showcancelled_declaration — this is \
                                     an unexpected AST shape, not a construct this task has \
                                     chosen to defer)"
                                ),
                            });
                        }
                    }
                }
            }
            // Task 8: LRM 30.4.4.3's "same destination reference shape"
            // and 30.4.4.4's "ifnone + unconditional for the same path"
            // validations, run once every one of `id`'s own specify
            // blocks has contributed its `PathEntry`s (several specify
            // blocks per module are legal, so this runs after the whole
            // `module_items` loop above, not per `SpecifyBlock` member).
            validate_state_dependent_groups(id, &self.paths)?;
            apply_pulse_style_declarations(id, &mut self.paths, &declarations);
            // LRM 30.7.4.1/30.7.4.2: the invocation options beat the declarations.
            for p in self.paths.iter_mut().filter(|p| p.instance == id) {
                if let Some(style) = self.pulse_style_option {
                    p.pulse_style = style;
                }
                if let Some(show) = self.showcancelled_option {
                    p.showcancelled = show;
                }
            }
        }
        Ok(())
    }
}

/// Strips the wrappers slang puts around a timing check's signal arguments:
/// an implicit `Conversion`, and the `Assignment` slang builds for an
/// output-direction formal (the notifier and the two delayed signals are bound
/// as output arguments), whose `left()` is the actual the user wrote.
fn strip_arg_wrappers<'d>(mut e: Expression<'d>) -> Expression<'d> {
    // Equality tests rather than a `match`: this is not a dispatch over the
    // kind enum (every other kind is "not a wrapper", by design), and the
    // kind guard forbids a silent wildcard arm over one.
    loop {
        let k = e.kind();
        let next = if k == ExpressionKind::Conversion {
            e.operand()
        } else if k == ExpressionKind::Assignment {
            e.left()
        } else {
            None
        };
        match next {
            Some(n) => e = n,
            None => return e,
        }
    }
}

/// A timing check's argument list, with the per-position accessors
/// [`discover_check`] decodes through. Positions are zero-based and match LRM
/// Tables 31-1..31-12's argument order; an elided or never-written trailing
/// argument reads as absent either way.
struct CheckArgsView<'a, 'd> {
    eval: &'a EvalSession<'d>,
    check: &'a Symbol<'d>,
    name: &'static str,
    args: Vec<sv_lang::SystemTimingCheckArg<'d>>,
}

impl<'a, 'd> CheckArgsView<'a, 'd> {
    fn err(&self, detail: String) -> ElabError {
        unsupported(self.check, format!("`{}` {detail}", self.name))
    }

    fn arg(&self, i: usize) -> Option<&sv_lang::SystemTimingCheckArg<'d>> {
        self.args.get(i).filter(|a| a.expr.is_some())
    }

    fn require(
        &self,
        i: usize,
        what: &str,
    ) -> Result<&sv_lang::SystemTimingCheckArg<'d>, ElabError> {
        self.arg(i).ok_or_else(|| {
            self.err(format!(
                "is missing its required {what} (argument {}; an empty argument is not allowed \
                 there)",
                i + 1
            ))
        })
    }

    /// A signal-valued argument (an event terminal, a notifier, a delayed
    /// signal): a net or variable, whole or a constant bit/part window.
    fn signal_of(&self, e: Expression<'d>, what: &str) -> Result<TerminalRef, ElabError> {
        let e = strip_arg_wrappers(e);
        let (sym, bits) = resolve_cond_signal_ref(self.eval, self.check, e)?;
        // LRM 25.6: a signal of an interface port (`ch.d`) is a terminal.
        let modport_signal = sym.kind() == SymbolKind::ModportPort
            && sym.modport_port_explicit_connection().is_none()
            && sym
                .modport_port_internal_symbol()
                .is_some_and(|s| matches!(s.kind(), SymbolKind::Net | SymbolKind::Variable));
        if !modport_signal && !matches!(sym.kind(), SymbolKind::Net | SymbolKind::Variable) {
            return Err(self.err(format!(
                "{what} `{}` is a {:?}, not a net or variable",
                sym.name(),
                sym.kind()
            )));
        }
        Ok((sym.uid(), bits))
    }

    fn event(&self, i: usize, what: &str) -> Result<CheckEvent, ElabError> {
        let a = self.require(i, what)?;
        let expr = a
            .expr
            .expect("require() only returns arguments with an expr");
        let condition = a
            .condition
            .map(|c| compile_cond_expr_in(self.eval, self.check, c, CondDialect::TimingCheck))
            .transpose()?;
        let edge_control = EdgeControl::from_syntax(a.edge, &a.edge_descriptors)
            .map_err(|e| self.err(format!("{what}: {e}")))?;
        Ok(CheckEvent {
            terminal: self.signal_of(expr, what)?,
            edge: a.edge,
            edge_descriptors: a.edge_descriptors.clone(),
            edge_control,
            condition,
        })
    }

    fn limit(&self, i: usize, what: &str) -> Result<CheckLimit, ElabError> {
        self.require(i, what)?;
        Ok(CheckLimit {
            arg_index: i as u32,
            ticks: 0,
        })
    }

    fn opt_limit(&self, i: usize) -> Option<CheckLimit> {
        self.arg(i).map(|_| CheckLimit {
            arg_index: i as u32,
            ticks: 0,
        })
    }

    fn opt_signal(&self, i: usize, what: &str) -> Result<Option<TerminalRef>, ElabError> {
        self.arg(i)
            .map(|a| self.signal_of(a.expr.expect("arg() filters on expr"), what))
            .transpose()
    }

    fn opt_cond(&self, i: usize) -> Result<Option<CondNode>, ElabError> {
        self.arg(i)
            .map(|a| {
                compile_cond_expr_in(
                    self.eval,
                    self.check,
                    a.expr.expect("arg() filters on expr"),
                    CondDialect::TimingCheck,
                )
            })
            .transpose()
    }

    fn opt_flag(&self, i: usize, what: &str) -> Result<Option<bool>, ElabError> {
        self.arg(i)
            .map(|a| {
                const_i64(self.eval, a.expr.expect("arg() filters on expr"))
                    .map(|v| v != 0)
                    .ok_or_else(|| self.err(format!("{what} must be a constant expression")))
            })
            .transpose()
    }

    fn pair(&self, data_first: bool) -> Result<EventPairArgs, ElabError> {
        let (r, d) = if data_first { (1, 0) } else { (0, 1) };
        Ok(EventPairArgs {
            reference: self.event(r, "reference event")?,
            data: self.event(d, "data event")?,
            limit: self.limit(2, "limit")?,
            notifier: self.opt_signal(3, "notifier")?,
        })
    }
}

/// Decodes one `SystemTimingCheck` symbol (LRM 31.2-31.6) into a typed
/// [`CheckEntry`], by the hard-coded positional layout of Tables 31-1..31-12
/// (`$setup` alone lists its data event first; `$setuphold`/`$recrem` carry
/// nine positions; `$skew` family flags and `$width`'s threshold are
/// optional). slang already diagnoses most malformed calls, but the CLI's
/// "the design has errors" abort is the only thing between a violation and
/// this function, so the clause's compile-time restrictions are re-raised here
/// as named errors: `$width`/`$period` need an edge specification (31.4.4,
/// 31.4.5), `$nochange`'s reference event must be `posedge`/`negedge` (31.4.6),
/// and `$width`'s notifier needs a non-null, constant threshold (31.4.4).
fn discover_check<'d>(
    eval: &EvalSession<'d>,
    instance: InstanceId,
    check: &Symbol<'d>,
) -> Result<CheckEntry, ElabError> {
    use sv_lang::SystemTimingCheckKind as K;
    let kind = check.system_timing_check_kind();
    let name = match kind {
        K::Setup => "$setup",
        K::Hold => "$hold",
        K::SetupHold => "$setuphold",
        K::Recovery => "$recovery",
        K::Removal => "$removal",
        K::RecRem => "$recrem",
        K::Skew => "$skew",
        K::TimeSkew => "$timeskew",
        K::FullSkew => "$fullskew",
        K::Period => "$period",
        K::Width => "$width",
        K::NoChange => "$nochange",
        K::Unknown => {
            return Err(unsupported(
                check,
                "system timing check of an unrecognized kind (unexpected AST shape)".to_string(),
            ));
        }
    };
    let v = CheckArgsView {
        eval,
        check,
        name,
        args: check.system_timing_check_arguments().collect(),
    };
    let args = match kind {
        // Already rejected by the name table above.
        K::Unknown => {
            return Err(unsupported(
                check,
                "system timing check of an unrecognized kind (unexpected AST shape)".to_string(),
            ));
        }
        K::Setup => CheckArgs::Setup(v.pair(true)?),
        K::Hold => CheckArgs::Hold(v.pair(false)?),
        K::Recovery => CheckArgs::Recovery(v.pair(false)?),
        K::Removal => CheckArgs::Removal(v.pair(false)?),
        K::Skew => CheckArgs::Skew(v.pair(false)?),
        K::SetupHold => CheckArgs::SetupHold(SetupHoldArgs {
            reference: v.event(0, "reference event")?,
            data: v.event(1, "data event")?,
            setup_limit: v.limit(2, "setup limit")?,
            hold_limit: v.limit(3, "hold limit")?,
            notifier: v.opt_signal(4, "notifier")?,
            timestamp_cond: v.opt_cond(5)?,
            timecheck_cond: v.opt_cond(6)?,
            delayed_reference: v.opt_signal(7, "delayed reference")?,
            delayed_data: v.opt_signal(8, "delayed data")?,
        }),
        K::RecRem => CheckArgs::RecRem(RecRemArgs {
            reference: v.event(0, "reference event")?,
            data: v.event(1, "data event")?,
            recovery_limit: v.limit(2, "recovery limit")?,
            removal_limit: v.limit(3, "removal limit")?,
            notifier: v.opt_signal(4, "notifier")?,
            timestamp_cond: v.opt_cond(5)?,
            timecheck_cond: v.opt_cond(6)?,
            delayed_reference: v.opt_signal(7, "delayed reference")?,
            delayed_data: v.opt_signal(8, "delayed data")?,
        }),
        K::TimeSkew => CheckArgs::TimeSkew(TimeSkewArgs {
            reference: v.event(0, "reference event")?,
            data: v.event(1, "data event")?,
            limit: v.limit(2, "limit")?,
            notifier: v.opt_signal(3, "notifier")?,
            event_based: v.opt_flag(4, "event_based_flag")?,
            remain_active: v.opt_flag(5, "remain_active_flag")?,
        }),
        K::FullSkew => CheckArgs::FullSkew(FullSkewArgs {
            reference: v.event(0, "reference event")?,
            data: v.event(1, "data event")?,
            reference_first_limit: v.limit(2, "first limit")?,
            data_first_limit: v.limit(3, "second limit")?,
            notifier: v.opt_signal(4, "notifier")?,
            event_based: v.opt_flag(5, "event_based_flag")?,
            remain_active: v.opt_flag(6, "remain_active_flag")?,
        }),
        K::Period => {
            let reference = v.event(0, "reference event")?;
            if reference.edge == sv_lang::EdgeKind::None {
                return Err(v.err(
                    "reference event must be an edge specification (`posedge`, `negedge` or \
                     `edge`) -- LRM 31.4.5: the period is measured between successive \
                     occurrences of that edge"
                        .to_string(),
                ));
            }
            CheckArgs::Period(PeriodArgs {
                reference,
                limit: v.limit(1, "limit")?,
                notifier: v.opt_signal(2, "notifier")?,
            })
        }
        K::Width => {
            let reference = v.event(0, "reference event")?;
            if reference.edge == sv_lang::EdgeKind::None {
                return Err(v.err(
                    "reference event must be an edge specification (`posedge`, `negedge` or \
                     `edge`) -- LRM 31.4.4: the width is measured from that edge to the opposite \
                     one"
                    .to_string(),
                ));
            }
            if v.arg(3).is_some() && v.arg(2).is_none() {
                return Err(v.err(
                    "has a notifier but a null threshold: LRM 31.4.4 allows the notifier only \
                     when the threshold argument is also given (write `0` for no threshold)"
                        .to_string(),
                ));
            }
            if let Some(t) = v.arg(2) {
                let te = t.expr.expect("arg() filters on expr");
                if te
                    .constant_value()
                    .or_else(|| eval.eval_constant(te))
                    .is_none()
                {
                    return Err(v.err(
                        "threshold must be a constant expression (LRM 31.4.4) -- a notifier in \
                         the third position is the classic mistake; the notifier is the fourth \
                         argument"
                            .to_string(),
                    ));
                }
            }
            CheckArgs::Width(WidthArgs {
                reference,
                limit: v.limit(1, "limit")?,
                threshold: v.opt_limit(2),
                notifier: v.opt_signal(3, "notifier")?,
            })
        }
        K::NoChange => {
            let reference = v.event(0, "reference event")?;
            let plain_edge = matches!(
                reference.edge,
                sv_lang::EdgeKind::PosEdge | sv_lang::EdgeKind::NegEdge
            ) && reference.edge_descriptors.is_empty();
            if !plain_edge {
                return Err(v.err(
                    "reference event must be `posedge` or `negedge` (LRM 31.4.6); an `edge` \
                     control specifier (with or without a descriptor list) or a bare signal is \
                     not allowed"
                        .to_string(),
                ));
            }
            CheckArgs::NoChange(NoChangeArgs {
                reference,
                data: v.event(1, "data event")?,
                start_edge_offset: v.limit(2, "start edge offset")?,
                end_edge_offset: v.limit(3, "end edge offset")?,
                notifier: v.opt_signal(4, "notifier")?,
            })
        }
    };
    Ok(CheckEntry {
        instance,
        check_uid: check.uid(),
        kind,
        args,
    })
}

/// Whether two output terminals of one instance share at least one bit
/// (`None` is the whole signal, `Some((lo, width))` a bit/part-select window).
fn terminals_overlap(a: &TerminalRef, b: &TerminalRef) -> bool {
    if a.0 != b.0 {
        return false;
    }
    match (a.1, b.1) {
        (Some((alo, aw)), Some((blo, bw))) => alo < blo + bw && blo < alo + aw,
        _ => true,
    }
}

/// One `PulseStyle` symbol (LRM 30.7.4: `pulsestyle_onevent`/
/// `pulsestyle_ondetect`/`showcancelled`/`noshowcancelled` followed by a
/// `list_of_path_outputs`): its outputs paired with the declaration kind, after
/// the 30.7.4.1/30.7.4.2 ordering rule — "it is an error if a module path
/// output appears in a [pulse style / showcancelled] declaration after it has
/// already appeared in a module path declaration" — has been checked against
/// `paths`, the path entries of every module path declared BEFORE this
/// declaration (discovery walks a module's specify blocks in source order, so
/// that is exactly `instance`'s entries so far). slang itself only warns
/// (`InvalidPulseStyle`) about a violation, so this is the hard error.
///
/// "Appeared" is overlap of the output's bit window: a declaration for `y[0]`
/// after a path to `y[1]` names a different output bit and is legal.
fn discover_pulse_style<'d>(
    eval: &EvalSession<'d>,
    instance: InstanceId,
    decl: &Symbol<'d>,
    ports: &HashMap<SymbolId, ArgumentDirection>,
    paths: &[PathEntry],
) -> Result<Vec<(TerminalRef, PulseStyleKind)>, ElabError> {
    let kind = decl.pulse_style_kind();
    let (keyword, clause) = match kind {
        PulseStyleKind::OnEvent => ("pulsestyle_onevent", "30.7.4.1"),
        PulseStyleKind::OnDetect => ("pulsestyle_ondetect", "30.7.4.1"),
        PulseStyleKind::ShowCancelled => ("showcancelled", "30.7.4.2"),
        PulseStyleKind::NoShowCancelled => ("noshowcancelled", "30.7.4.2"),
    };
    let mut out = Vec::new();
    for e in decl.pulse_style_terminals() {
        // Same resolution (and 30.4.1 output-direction check) as a module path
        // destination: a pulse style names module path outputs.
        let terminal = resolve_terminal(eval, decl, ports, e, false)?;
        let already_used = paths.iter().any(|p| {
            p.instance == instance && p.outputs.iter().any(|o| terminals_overlap(o, &terminal))
        });
        if already_used {
            let full = terminal.0.to_string();
            let name = full.rsplit('.').next().unwrap_or(&full);
            return Err(unsupported(
                decl,
                format!(
                    "`{keyword} {name}` follows a module path declaration that already names \
                     output `{name}` (LRM {clause}: it is an error for a module path output to \
                     appear in this declaration after it has already appeared in a module path \
                     declaration — the output would have contradictory pulse behavior for the \
                     earlier path)"
                ),
            ));
        }
        out.push((terminal, kind));
    }
    Ok(out)
}

/// Applies `declarations` (source order) to `instance`'s `paths`: a declaration
/// reaches every path whose output window overlaps its terminal. The two
/// settings are independent axes — `pulsestyle_*` sets
/// [`PathEntry::pulse_style`], `showcancelled`/`noshowcancelled` sets
/// [`PathEntry::showcancelled`] — and **implementation-defined**: when one
/// output is declared twice on the same axis (legal, since both precede its
/// paths), the later declaration wins; the LRM only forbids the contradictory
/// order relative to a path.
fn apply_pulse_style_declarations(
    instance: InstanceId,
    paths: &mut [PathEntry],
    declarations: &[(TerminalRef, PulseStyleKind)],
) {
    for (terminal, kind) in declarations {
        for p in paths.iter_mut().filter(|p| {
            p.instance == instance && p.outputs.iter().any(|o| terminals_overlap(o, terminal))
        }) {
            match kind {
                PulseStyleKind::OnEvent => p.pulse_style = PulseStyle::OnEvent,
                PulseStyleKind::OnDetect => p.pulse_style = PulseStyle::OnDetect,
                PulseStyleKind::ShowCancelled => p.showcancelled = true,
                PulseStyleKind::NoShowCancelled => p.showcancelled = false,
            }
        }
    }
}

/// `body`'s module ports, keyed by each port's internal net/variable's
/// [`SymbolUid::uid`] (the SAME `port_internal_symbol().unwrap_or(port)`
/// pattern `nets.rs`/`run.rs`/`primitives.rs` already use to relate a
/// port to the signal it connects to inside the module) — the table
/// [`validate_direction`] checks a specify-path terminal's own symbol
/// against for LRM 30.4.1's restriction.
fn port_directions<'d>(body: &Symbol<'d>) -> HashMap<SymbolId, ArgumentDirection> {
    let mut map = HashMap::new();
    for m in body.members() {
        if m.kind() != SymbolKind::Port {
            continue;
        }
        let internal = m.port_internal_symbol().unwrap_or(m);
        map.insert(internal.uid(), m.port_direction());
    }
    map
}

/// `ElabError::UnsupportedConstruct` at `sym`'s own hierarchical path —
/// every named error this module raises goes through this one call site.
fn unsupported(sym: &Symbol<'_>, detail: String) -> ElabError {
    ElabError::UnsupportedConstruct {
        hier_path: sym.hierarchical_path(),
        detail,
    }
}

/// `e`'s value as a compile-time constant `i64`, folding what slang left
/// unfolded (mirrors `vj::primitives::constant_of`/`vj::
/// specify_eval::constant_of` — a third, small copy for the same reason
/// `specify_eval.rs`'s own doc comment gives: the existing ones are
/// private `fn`s in sibling/downstream crates this crate cannot reach into
/// or be reached from).
fn const_i64<'d>(eval: &EvalSession<'d>, e: Expression<'d>) -> Option<i64> {
    e.constant_value()
        .or_else(|| eval.eval_constant(e))
        .and_then(|v| v.as_i64())
}

/// LRM 30.4.1: a module path source must be a net connected to an
/// input/inout port; a destination must be a net or variable connected to
/// an output/inout port. Verified live against sv-lang=0.1.9/slang 11.0:
/// slang already enforces exactly this (its own diagnostic text literally
/// reads "specify path source/destination must be an 'input'/'output' or
/// 'inout' ...", `SpecifyBlockSymbol::checkPathTerminal`) and already drops
/// a violating terminal from `timing_path_inputs()`/`_outputs()` — but it
/// does so ONE TERMINAL AT A TIME, in `bindTerminal`, before this crate
/// ever sees the symbol: `path.timing_path_inputs()`/`_outputs()` (what
/// `discover_path` iterates to build `raw_inputs`/`raw_outputs`, and the
/// only source this function's own `sym` argument ever comes from) has
/// *already* had every terminal failing this exact check removed. So this
/// function's own checks below are, today, unreachable dead code against
/// sv-lang 0.1.9 — verified live, not a theoretical claim: every `sym` this
/// function is ever called with has already passed
/// `checkPathTerminal`'s identical net-kind/port-direction test. It is kept
/// anyway as defense-in-depth against a future sv-lang version relaxing
/// that filter, or an AST shape this module's own enumeration above has not
/// considered — never as this module's real guarantee against a dropped
/// sibling terminal in an otherwise-valid multi-terminal declaration. THAT
/// guarantee — a multi-terminal `path_declaration` with one invalid
/// sibling among otherwise-valid terminals is a `LoweringError`, never a
/// silently-accepted partial `PathEntry` — is [`discover_path`]'s own
/// syntax-vs-resolved terminal COUNT check (via
/// [`syntax_terminal_counts`]), not this function: this function only ever
/// sees the terminals sv-lang's per-terminal filtering already decided to
/// keep, so it cannot by construction "catch a violation regardless of how
/// many sibling terminals are otherwise valid" the way an earlier revision
/// of this comment claimed.
fn validate_direction<'d>(
    path: &Symbol<'d>,
    ports: &HashMap<SymbolId, ArgumentDirection>,
    sym: Symbol<'d>,
    want_input: bool,
) -> Result<(), ElabError> {
    if sym.kind() == SymbolKind::ModportPort {
        // LRM 25.6: every signal of an interface port is a terminal, with the
        // direction the modport gives it (an interface port without a modport
        // never reaches here: it names the interface's own signal). The
        // signal lives in the interface instance; the module's own signal
        // table carries it under the port's uid (run.rs foreign slots).
        // A `ref` port cannot be a terminal; an expression-bound port
        // (`.x(r[3:0])`) is not a plain signal.
        let internal = sym.modport_port_internal_symbol();
        if sym.modport_port_explicit_connection().is_some()
            || !internal.is_some_and(|s| matches!(s.kind(), SymbolKind::Net | SymbolKind::Variable))
        {
            return Err(unsupported(
                path,
                format!(
                    "specify terminal `{}` is an interface-port signal bound to an expression \
                     or a non-signal (LRM 25.6): not lowered",
                    sym.name()
                ),
            ));
        }
        let dir = sym.modport_port_direction();
        let ok = if want_input {
            matches!(dir, ArgumentDirection::In | ArgumentDirection::InOut)
        } else {
            matches!(dir, ArgumentDirection::Out | ArgumentDirection::InOut)
        };
        if !ok {
            return Err(unsupported(
                path,
                format!(
                    "specify path {} `{}` is a modport port with direction {:?}, not {} (LRM \
                     25.6, 30.4.1)",
                    if want_input { "source" } else { "destination" },
                    sym.name(),
                    dir,
                    if want_input {
                        "input or inout"
                    } else {
                        "output or inout"
                    }
                ),
            ));
        }
        return Ok(());
    }
    if want_input && sym.kind() != SymbolKind::Net {
        return Err(unsupported(
            path,
            format!(
                "specify path source `{}` is a {:?}, not a net (LRM 30.4.1: \"the module path \
                 source shall be a net\")",
                sym.name(),
                sym.kind()
            ),
        ));
    }
    if !want_input && !matches!(sym.kind(), SymbolKind::Net | SymbolKind::Variable) {
        return Err(unsupported(
            path,
            format!(
                "specify path destination `{}` is a {:?}, not a net or variable (LRM 30.4.1: \
                 \"the module path destination shall be a net or variable\")",
                sym.name(),
                sym.kind()
            ),
        ));
    }
    let dir = ports.get(&sym.uid()).ok_or_else(|| {
        unsupported(
            path,
            format!(
                "specify path terminal `{}` is not connected to any module port (LRM 30.4.1 \
                 requires the source to be connected to an input/inout port, and the \
                 destination to an output/inout port)",
                sym.name()
            ),
        )
    })?;
    let ok = if want_input {
        matches!(dir, ArgumentDirection::In | ArgumentDirection::InOut)
    } else {
        matches!(dir, ArgumentDirection::Out | ArgumentDirection::InOut)
    };
    if !ok {
        return Err(unsupported(
            path,
            format!(
                "specify path {} `{}` is connected to a {:?} port, not {} (LRM 30.4.1)",
                if want_input { "source" } else { "destination" },
                sym.name(),
                dir,
                if want_input {
                    "an input or inout port"
                } else {
                    "an output or inout port"
                }
            ),
        ));
    }
    Ok(())
}

/// Resolves one `timing_path_inputs()`/`timing_path_outputs()` item to the
/// `TerminalRef` a [`PathEntry`] stores, validating [`validate_direction`]
/// along the way. Handles a plain signal reference, a constant bit-select
/// (`a[3]`) and a constant SIMPLE part-select (`a[7:4]`) — mirrors
/// `vj::primitives::signal_bit`'s own `Conversion`-unwrap/
/// `ElementSelect` handling, generalized with a part-select case
/// `primitives.rs`'s own scalar-terminal callers never needed.
///
/// An INDEXED part-select (`a[base +: w]`/`a[base -: w]`) with constant
/// operands resolves to the same bit window as the equivalent simple
/// part-select (LRM 11.5.1; bounds zero-based like the simple form).
fn resolve_terminal<'d>(
    eval: &EvalSession<'d>,
    path: &Symbol<'d>,
    ports: &HashMap<SymbolId, ArgumentDirection>,
    e: Expression<'d>,
    want_input: bool,
) -> Result<TerminalRef, ElabError> {
    let e = if e.kind() == ExpressionKind::Conversion {
        e.operand().unwrap_or(e)
    } else {
        e
    };
    let (sym, bits) = if is_value_name(e.kind()) {
        let sym = e.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "specify path terminal has no referenced symbol (unexpected AST shape)".to_string(),
            )
        })?;
        (sym, None)
    } else if e.kind() == ExpressionKind::ElementSelect {
        let base = e.select_value().ok_or_else(|| {
            unsupported(
                path,
                "bit-select specify path terminal missing its own base expression".to_string(),
            )
        })?;
        if !is_value_name(base.kind()) {
            return Err(unsupported(
                path,
                "bit-select specify path terminal's base is not a plain signal reference \
                 (unexpected AST shape)"
                    .to_string(),
            ));
        }
        let sym = base.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "bit-select specify path terminal's base has no referenced symbol (unexpected \
                 AST shape)"
                    .to_string(),
            )
        })?;
        let idx_expr = e.selector().ok_or_else(|| {
            unsupported(
                path,
                "bit-select specify path terminal missing its own index".to_string(),
            )
        })?;
        let idx = const_i64(eval, idx_expr).ok_or_else(|| {
            unsupported(
                path,
                "bit-select specify path terminal index must be a compile-time constant"
                    .to_string(),
            )
        })?;
        if idx < 0 {
            return Err(unsupported(
                path,
                "bit-select specify path terminal index is negative".to_string(),
            ));
        }
        (sym, Some((idx as u32, 1)))
    } else if e.kind() == ExpressionKind::RangeSelect {
        let base = e.select_value().ok_or_else(|| {
            unsupported(
                path,
                "part-select specify path terminal missing its own base expression".to_string(),
            )
        })?;
        if !is_value_name(base.kind()) {
            return Err(unsupported(
                path,
                "part-select specify path terminal's base is not a plain signal reference \
                 (unexpected AST shape)"
                    .to_string(),
            ));
        }
        let sym = base.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "part-select specify path terminal's base has no referenced symbol (unexpected \
                 AST shape)"
                    .to_string(),
            )
        })?;
        let kind = e.range_selection_kind().ok_or_else(|| {
            unsupported(
                path,
                "part-select specify path terminal missing its own range_selection_kind"
                    .to_string(),
            )
        })?;
        let l_expr = e.range_left().ok_or_else(|| {
            unsupported(
                path,
                "simple part-select specify path terminal missing its left bound".to_string(),
            )
        })?;
        let r_expr = e.range_right().ok_or_else(|| {
            unsupported(
                path,
                "simple part-select specify path terminal missing its right bound".to_string(),
            )
        })?;
        let l = const_i64(eval, l_expr).ok_or_else(|| {
            unsupported(
                path,
                "simple part-select specify path terminal's left bound must be a compile-time \
                 constant"
                    .to_string(),
            )
        })?;
        let r = const_i64(eval, r_expr).ok_or_else(|| {
            unsupported(
                path,
                "simple part-select specify path terminal's right bound must be a \
                 compile-time constant"
                    .to_string(),
            )
        })?;
        // LRM 11.5.1 / 30.3: `[l +: r]` is bits `l .. l+r-1`, `[l -: r]` is
        // `l-r+1 .. l` (kind 1 = up, 2 = down; 0 = simple `[l:r]`). Like the
        // simple form the bounds are taken as zero-based offsets.
        let (lo, hi) = match kind {
            0 => (l.min(r), l.max(r)),
            1 => (l, l + r - 1),
            _ => (l - r + 1, l),
        };
        if lo < 0 || hi < lo {
            return Err(unsupported(
                path,
                "part-select specify path terminal has a negative or empty bit window".to_string(),
            ));
        }
        (sym, Some((lo as u32, (hi - lo + 1) as u32)))
    } else {
        return Err(unsupported(
            path,
            format!(
                "specify path terminal expression kind `{:?}` (unexpected AST shape)",
                e.kind()
            ),
        ));
    };
    validate_direction(path, ports, sym, want_input)?;
    Ok((sym.uid(), bits))
}

/// `b`'s value as [`Bit4`] -- the one place `sv_lang::Bit`'s discriminant
/// order is asserted to equal [`Bit4`]'s in THIS crate's `netlist` module
/// (mirrors `state::value::bit_to_bit4`'s own identical, independently-
/// written copy; a third small duplicate for the same reason `vj::
/// specify_eval`'s own `constant_of` doc comment gives for its own
/// duplicate of `primitives::constant_of` -- `state::value`'s copy is a
/// private `fn` of a sibling module this one cannot reach into).
fn bit4_of(b: Bit) -> Bit4 {
    match b {
        Bit::Zero => Bit4::Zero,
        Bit::One => Bit4::One,
        Bit::X => Bit4::X,
        Bit::Z => Bit4::Z,
    }
}

/// Resolves a condition operand that is a plain signal/specparam reference,
/// a constant bit-select, or a constant SIMPLE part-select -- the
/// condition-expression analogue of [`resolve_terminal`] (same AST shapes,
/// same `ElementSelect`/`RangeSelect` handling), but WITHOUT
/// [`validate_direction`]'s port-direction check: LRM 30.4.4.1's own
/// operand list ("module input/inout ports... OR locally defined variables
/// or nets") is strictly WIDER than a module-path terminal's own 30.4.1
/// restriction (a plain internal variable/net, not connected to any port at
/// all, is a legal condition operand but never a legal path terminal), so
/// this function resolves the symbol and its bit window only, leaving any
/// further legality check to the caller (today: none -- see
/// [`compile_cond_expr`]'s own doc comment for why this task does not add
/// one).
fn resolve_cond_signal_ref<'d>(
    eval: &EvalSession<'d>,
    path: &Symbol<'d>,
    e: Expression<'d>,
) -> Result<(Symbol<'d>, Option<(u32, u32)>), ElabError> {
    if is_value_name(e.kind()) {
        let sym = e.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "state-dependent path condition operand has no referenced symbol (unexpected \
                 AST shape)"
                    .to_string(),
            )
        })?;
        return Ok((sym, None));
    }
    if e.kind() == ExpressionKind::ElementSelect {
        let base = e.select_value().ok_or_else(|| {
            unsupported(
                path,
                "bit-select condition operand missing its own base expression".to_string(),
            )
        })?;
        if !is_value_name(base.kind()) {
            return Err(unsupported(
                path,
                "bit-select condition operand's base is not a plain signal reference \
                 (unexpected AST shape)"
                    .to_string(),
            ));
        }
        let sym = base.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "bit-select condition operand's base has no referenced symbol (unexpected AST \
                 shape)"
                    .to_string(),
            )
        })?;
        let idx_expr = e.selector().ok_or_else(|| {
            unsupported(
                path,
                "bit-select condition operand missing its own index".to_string(),
            )
        })?;
        let idx = const_i64(eval, idx_expr).ok_or_else(|| {
            unsupported(
                path,
                "bit-select condition operand index must be a compile-time constant".to_string(),
            )
        })?;
        if idx < 0 {
            return Err(unsupported(
                path,
                "bit-select condition operand index is negative".to_string(),
            ));
        }
        return Ok((sym, Some((idx as u32, 1))));
    }
    if e.kind() == ExpressionKind::RangeSelect {
        let base = e.select_value().ok_or_else(|| {
            unsupported(
                path,
                "part-select condition operand missing its own base expression".to_string(),
            )
        })?;
        if !is_value_name(base.kind()) {
            return Err(unsupported(
                path,
                "part-select condition operand's base is not a plain signal reference \
                 (unexpected AST shape)"
                    .to_string(),
            ));
        }
        let sym = base.referenced_symbol().ok_or_else(|| {
            unsupported(
                path,
                "part-select condition operand's base has no referenced symbol (unexpected AST \
                 shape)"
                    .to_string(),
            )
        })?;
        let kind = e.range_selection_kind().ok_or_else(|| {
            unsupported(
                path,
                "part-select condition operand missing its own range_selection_kind".to_string(),
            )
        })?;
        let l_expr = e.range_left().ok_or_else(|| {
            unsupported(
                path,
                "simple part-select condition operand missing its left bound".to_string(),
            )
        })?;
        let r_expr = e.range_right().ok_or_else(|| {
            unsupported(
                path,
                "simple part-select condition operand missing its right bound".to_string(),
            )
        })?;
        let l = const_i64(eval, l_expr).ok_or_else(|| {
            unsupported(
                path,
                "simple part-select condition operand's left bound must be a compile-time \
                 constant"
                    .to_string(),
            )
        })?;
        let r = const_i64(eval, r_expr).ok_or_else(|| {
            unsupported(
                path,
                "simple part-select condition operand's right bound must be a compile-time \
                 constant"
                    .to_string(),
            )
        })?;
        // LRM 11.5.1 / 30.4.4.1: an indexed part-select with constant
        // operands. `l` is the base, `r` the width: `[l +: r]` is bits
        // `l .. l+r-1`, `[l -: r]` is `l-r+1 .. l` (kind 1 = up, 2 = down;
        // 0 = simple `[l:r]`). Like the simple form this takes the bounds as
        // zero-based offsets (a `[N:0]` declaration).
        let (lo, hi) = match kind {
            0 => (l.min(r), l.max(r)),
            1 => (l, l + r - 1),
            _ => (l - r + 1, l),
        };
        if lo < 0 || hi < lo {
            return Err(unsupported(
                path,
                "part-select condition operand has a negative or empty bit window".to_string(),
            ));
        }
        return Ok((sym, Some((lo as u32, (hi - lo + 1) as u32))));
    }
    Err(unsupported(
        path,
        format!(
            "state-dependent path condition operand expression kind `{:?}` is neither a \
             signal/specparam reference nor a bit-/part-select of one (unexpected AST shape)",
            e.kind()
        ),
    ))
}

/// Compiles a state-dependent path's own `if (cond)` conditional expression
/// (LRM 30.4.4.1) into a [`CondNode`] -- see that type's own doc comment
/// for why this produces symbolic data rather than a value. Table 30-1's
/// own closed operator list is enforced via [`CondUnaryOp::from_sv`]/
/// [`CondBinaryOp::from_sv`]; any operator, or any operand AST shape, Table
/// 30-1/30.4.4.1 do not cover is a named [`ElabError::UnsupportedConstruct`],
/// never a silent acceptance.
///
/// This task does not re-enforce 30.4.4.1's own operand-KIND restriction
/// (ports/variables/nets only, never e.g. a class property or a function
/// call) beyond what [`resolve_cond_signal_ref`]'s own AST-shape dispatch
/// already excludes by construction (a function call, for instance, is
/// none of `NamedValue`/`ElementSelect`/`RangeSelect`/a foldable constant,
/// so it already falls through to this function's own trailing `Err`) --
/// mirrors [`validate_direction`]'s own documented reasoning that slang's
/// own elaboration-time checks make a second, redundant kind check
/// pure defense-in-depth rather than this function's real guarantee.
fn compile_cond_expr<'d>(
    eval: &EvalSession<'d>,
    path: &Symbol<'d>,
    e: Expression<'d>,
) -> Result<CondNode, ElabError> {
    compile_cond_expr_in(eval, path, e, CondDialect::ModulePath)
}

/// Which clause's operator set a condition expression is compiled under.
#[derive(Clone, Copy, PartialEq, Eq)]
enum CondDialect {
    /// A state-dependent module path's `if (cond)` (LRM 30.4.4.1, Table 30-1).
    ModulePath,
    /// A system timing check's `&&&`/timestamp/timecheck condition (LRM 31.7):
    /// Table 30-1 plus `===`/`!==`.
    TimingCheck,
}

fn compile_cond_expr_in<'d>(
    eval: &EvalSession<'d>,
    path: &Symbol<'d>,
    e: Expression<'d>,
    dialect: CondDialect,
) -> Result<CondNode, ElabError> {
    let e = if e.kind() == ExpressionKind::Conversion {
        e.operand().unwrap_or(e)
    } else {
        e
    };
    match e.kind() {
        ExpressionKind::UnaryOp => {
            let uop = e.unary_op().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's unary expression is missing its own \
                     operator (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            let cop = CondUnaryOp::from_sv(uop).ok_or_else(|| {
                unsupported(
                    path,
                    format!(
                        "state-dependent path condition uses unary operator `{uop:?}`, which is \
                         not one of LRM Table 30-1's own eight valid conditional-expression \
                         operators"
                    ),
                )
            })?;
            let operand = e.operand().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's unary expression is missing its own \
                     operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            Ok(CondNode::Unary(
                cop,
                Box::new(compile_cond_expr_in(eval, path, operand, dialect)?),
            ))
        }
        ExpressionKind::BinaryOp => {
            let bop = e.binary_op().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's binary expression is missing its own \
                     operator (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            let mapped = match dialect {
                CondDialect::ModulePath => CondBinaryOp::from_sv(bop),
                CondDialect::TimingCheck => CondBinaryOp::from_sv_check(bop),
            };
            let cop = mapped.ok_or_else(|| {
                unsupported(
                    path,
                    format!(
                        "state-dependent path condition uses binary operator `{bop:?}`, which \
                         is not one of LRM Table 30-1's own eight valid conditional-expression \
                         operators"
                    ),
                )
            })?;
            let l = e.left().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's binary expression is missing its own \
                     left operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            let r = e.right().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's binary expression is missing its own \
                     right operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            Ok(CondNode::Binary(
                cop,
                Box::new(compile_cond_expr_in(eval, path, l, dialect)?),
                Box::new(compile_cond_expr_in(eval, path, r, dialect)?),
            ))
        }
        ExpressionKind::ConditionalOp => {
            let conds = e.conditions();
            if conds.len() != 1 || conds[0].pattern().is_some() {
                return Err(unsupported(
                    path,
                    "state-dependent path condition uses a pattern-matching conditional \
                     operator (`&&&`-chained or `matches`), which LRM Table 30-1 does not list"
                        .to_string(),
                ));
            }
            let c = compile_cond_expr_in(eval, path, conds[0].expr(), dialect)?;
            let t = e.true_value().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's conditional operator is missing its own \
                     true-value operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            let f = e.false_value().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's conditional operator is missing its own \
                     false-value operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            Ok(CondNode::Ternary(
                Box::new(c),
                Box::new(compile_cond_expr_in(eval, path, t, dialect)?),
                Box::new(compile_cond_expr_in(eval, path, f, dialect)?),
            ))
        }
        ExpressionKind::Concatenation => {
            let operands = e.operands();
            if operands.is_empty() {
                return Err(unsupported(
                    path,
                    "state-dependent path condition's concatenation has no operands \
                     (unexpected AST shape)"
                        .to_string(),
                ));
            }
            let mut out = Vec::with_capacity(operands.len());
            for o in operands {
                out.push(compile_cond_expr_in(eval, path, o, dialect)?);
            }
            Ok(CondNode::Concat(out))
        }
        ExpressionKind::Replication => {
            let count_expr = e.replication_count().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's replication is missing its own count \
                     (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            let count = const_i64(eval, count_expr).ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's replication count must be a compile-time \
                     constant"
                        .to_string(),
                )
            })?;
            if count < 0 {
                return Err(unsupported(
                    path,
                    "state-dependent path condition's replication count is negative".to_string(),
                ));
            }
            let unit = e.replication_concat().ok_or_else(|| {
                unsupported(
                    path,
                    "state-dependent path condition's replication is missing its own repeated \
                     operand (unexpected AST shape)"
                        .to_string(),
                )
            })?;
            Ok(CondNode::Replication(
                count as u32,
                Box::new(compile_cond_expr_in(eval, path, unit, dialect)?),
            ))
        }
        ExpressionKind::NamedValue
        | ExpressionKind::HierarchicalValue
        | ExpressionKind::ElementSelect
        | ExpressionKind::RangeSelect => {
            let (sym, bits) = resolve_cond_signal_ref(eval, path, e)?;
            if sym.kind() == SymbolKind::Specparam {
                Ok(CondNode::Specparam(sym.uid()))
            } else {
                Ok(CondNode::Signal((sym.uid(), bits)))
            }
        }
        // LRM 30.4.4.1's own third operand kind, "compile-time constants
        // (constant numbers...)" -- a plain NUMBER LITERAL, the only shape
        // this clause's own text means by it (an arithmetic/relational
        // constant EXPRESSION built from these, e.g. `(2+3)`, is already
        // illegal regardless of foldability, since `+`/`<` etc. are not
        // among Table 30-1's own eight operators -- rejected by the
        // `UnaryOp`/`BinaryOp` arms above via `CondUnaryOp`/`CondBinaryOp::
        // from_sv`, never reaching here). Named explicitly, one arm per
        // literal `ExpressionKind` (not a catch-all): `cargo xtask
        // lint-unimplemented`'s own static walk singles out a WILDCARD arm
        // for this match for extra scrutiny (it must be unconditionally
        // loud, since the lint cannot otherwise tell which kinds a
        // "try to fold it, fail loudly if that fails too" catch-all
        // silently accepts) -- enumerating the literal kinds here keeps the
        // trailing `_` arm honestly, unconditionally loud instead.
        ExpressionKind::IntegerLiteral | ExpressionKind::UnbasedUnsizedIntegerLiteral => {
            let c = match e.constant_value().or_else(|| eval.eval_constant(e)) {
                Some(c) => c,
                None => {
                    return Err(unsupported(
                        path,
                        "state-dependent path condition's integer literal operand did not fold \
                         to a constant (unexpected AST shape)"
                            .to_string(),
                    ));
                }
            };
            let int = match c.as_integer() {
                Some(int) => int,
                None => {
                    return Err(unsupported(
                        path,
                        "state-dependent path condition's integer literal operand did not fold \
                         to an integer constant (unexpected AST shape)"
                            .to_string(),
                    ));
                }
            };
            let bits = int.bits();
            if bits.is_empty() && int.bit_width() > 0 {
                return Err(unsupported(
                    path,
                    "state-dependent path condition's integer literal operand is too wide to \
                     expand bit-by-bit"
                        .to_string(),
                ));
            }
            Ok(CondNode::Const(bits.iter().map(|&b| bit4_of(b)).collect()))
        }
        ExpressionKind::RealLiteral
        | ExpressionKind::TimeLiteral
        | ExpressionKind::NullLiteral
        | ExpressionKind::UnboundedLiteral
        | ExpressionKind::StringLiteral => Err(unsupported(
            path,
            format!(
                "state-dependent path condition operand of kind `{:?}` is not an integer \
                 constant number -- LRM 30.4.4.1's own \"compile-time constants\" operand kind \
                 means a constant NUMBER, never a real/time/null/unbounded/string literal",
                e.kind()
            ),
        )),
        _ => Err(unsupported(
            path,
            format!(
                "state-dependent path condition operand expression kind `{:?}` is none of LRM \
                 30.4.4.1's own operand kinds (a module input/inout port, a locally defined \
                 variable or net, their bit-/part-selects, or a compile-time constant number) \
                 and is not one of the operator shapes this function otherwise handles \
                 (unexpected AST shape)",
                e.kind()
            ),
        )),
    }
}

/// `TimingPath::timing_path_is_state_dependent()`/`_condition_expr()`'s own
/// joint discriminant (this plan's own "What already exists" section's
/// decision 0): neither accessor alone distinguishes all three of
/// [`PathCondition`]'s own cases -- `is_state_dependent() == false` is
/// always [`PathCondition::Unconditional`]; `is_state_dependent() == true`
/// with `condition_expr().is_some()` is [`PathCondition::If`] (the
/// expression compiled via [`compile_cond_expr`]); `is_state_dependent() ==
/// true` with `condition_expr().is_none()` is [`PathCondition::IfNone`] (an
/// `ifnone` path has no condition expression of its own at all).
fn resolve_condition<'d>(
    eval: &EvalSession<'d>,
    path: &Symbol<'d>,
) -> Result<PathCondition, ElabError> {
    if !path.timing_path_is_state_dependent() {
        return Ok(PathCondition::Unconditional);
    }
    match path.timing_path_condition_expr() {
        Some(cond) => Ok(PathCondition::If(compile_cond_expr(eval, path, cond)?)),
        None => Ok(PathCondition::IfNone),
    }
}

/// A module-path terminal's own "reference shape" -- LRM 30.4.4.3's own
/// "the port is referenced in the same way in all path declarations
/// (entire port, bit-select, or part-select)" -- the SHAPE category only
/// (never the specific indices: Example 4's own `q[3:0]` vs `q[0]` is
/// illegal because one is a part-select and the other a bit-select, not
/// because their indices differ).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum TerminalShape {
    Whole,
    BitSelect,
    PartSelect,
}

impl TerminalShape {
    fn of(bits: &Option<(u32, u32)>) -> TerminalShape {
        match bits {
            None => TerminalShape::Whole,
            Some((_, 1)) => TerminalShape::BitSelect,
            Some((_, _)) => TerminalShape::PartSelect,
        }
    }
}

/// LRM 30.4.4.3's "same port reference shape" requirement and 30.4.4.4's
/// "ifnone + unconditional for the same path is illegal" rule -- Task 8's
/// own two discovery-time validations (its own text: "both `LoweringError`s,
/// not silent acceptance"), run once `instance`'s every desugared
/// [`PathEntry`] has been discovered. Both group entries by `(input
/// terminal symbol, output terminal symbol)` -- "the same module path" per
/// 30.4.4.4's own text, and what this plan's own T8 section calls "what
/// full-path grouping identifies as 'the same path'" for 30.4.4.3.
///
/// Scope note (task's own documented choice): 30.4.4.3's subclause title is
/// "Edge-sensitive state-dependent paths," but its own criteria are framed
/// generically over "the same path," and the plan's own T8 text does not
/// limit the shape check to edge-sensitive declarations specifically -- so
/// this validates the destination's own shape agreement across every
/// state-dependent (`If`/`IfNone`) entry of a group, edge-sensitive or not.
/// Only the DESTINATION's shape is compared (30.4.4.4's own Example 4 only
/// ever illustrates a destination mismatch); a source-shape mismatch is not
/// validated here.
fn validate_state_dependent_groups(
    instance: InstanceId,
    paths: &[PathEntry],
) -> Result<(), ElabError> {
    let mut groups: HashMap<(SymbolId, SymbolId), Vec<&PathEntry>> = HashMap::new();
    for p in paths.iter().filter(|p| p.instance == instance) {
        let key = (p.inputs[0].0.clone(), p.outputs[0].0.clone());
        groups.entry(key).or_default().push(p);
    }
    for ((in_uid, out_uid), group) in &groups {
        let has_ifnone = group
            .iter()
            .any(|p| matches!(p.condition, PathCondition::IfNone));
        let has_unconditional = group
            .iter()
            .any(|p| matches!(p.condition, PathCondition::Unconditional));
        if has_ifnone && has_unconditional {
            return Err(ElabError::UnsupportedConstruct {
                hier_path: format!("{in_uid} -> {out_uid}"),
                detail: "an `ifnone` condition and an unconditional module path both declared \
                         for the same module path source/destination pair (LRM 30.4.4.4: \"It \
                         is illegal to specify both an ifnone condition for a module path and \
                         an unconditional simple module path for the same module path.\")"
                    .to_string(),
            });
        }
        let mut shape: Option<TerminalShape> = None;
        for p in group
            .iter()
            .filter(|p| !matches!(p.condition, PathCondition::Unconditional))
        {
            let s = TerminalShape::of(&p.outputs[0].1);
            match shape {
                None => shape = Some(s),
                Some(prev) if prev == s => {}
                Some(_) => {
                    return Err(ElabError::UnsupportedConstruct {
                        hier_path: format!("{in_uid} -> {out_uid}"),
                        detail: "state-dependent module path declarations for the same path \
                                 reference their destination port in different ways (whole \
                                 port vs. bit-select vs. part-select) -- LRM 30.4.4.3: \"The \
                                 port is referenced in the same way in all path declarations \
                                 (entire port, bit-select, or part-select).\""
                            .to_string(),
                    });
                }
            }
        }
    }
    Ok(())
}

/// Desugars one `TimingPath` symbol into its [`PathEntry`]s (LRM 30.4.6):
/// a `Full` (`*>`) connection with `n` inputs and `m` outputs becomes `n *
/// m` entries, one per (output, input) pair, in the SAME order the LRM's
/// own worked example lists them (outer loop over outputs, inner loop over
/// inputs — "(a*>q1);(b*>q1);(c*>q1);(a*>q2);(b*>q2);(c*>q2);" for
/// `(a,b,c*>q1,q2)`). A `Parallel` (`=>`) connection's own grammar
/// (`parallel_path_description`, LRM Annex A.7.2) only ever has a single
/// terminal on each side, so it is never desugared — a `Parallel`
/// `TimingPath` with more than one resolved input or output is an
/// unexpected AST shape, not a shape this function silently handles by
/// picking the first one.
///
/// A `TimingPath` whose `timing_path_inputs()`/`_outputs()` resolves to
/// ZERO terminals (LRM 30.4.1's restriction already rejected the only one
/// declared, slang's own diagnostic naming it — or, per
/// `resolve_terminal`'s own doc comment, an unsupported terminal form such
/// as `interface_identifier.port_identifier`: verified live, slang 11.0
/// rejects that form outright with "specify path must be a simple
/// reference to a module port signal") is a named error here, never a
/// silently-empty `Vec<PathEntry>` — the "never silently accepted" guarantee
/// this plan's own "What already exists" section commits to for Clause 30.
///
/// Review fix (r1): the zero-terminal checks above are not a COMPLETE
/// restriction check on their own. sv-lang's own per-terminal filtering
/// (`SpecifyBlockSymbol::checkPathTerminal`, consulted one
/// `specify_input_terminal_descriptor`/`specify_output_terminal_descriptor`
/// at a time) drops only the terminal(s) that actually violate 30.4.1,
/// keeping every sibling that does not — so a multi-terminal declaration
/// with one bad terminal among several good ones (e.g. `(a, r, c *> q1)`
/// where `r` is a `reg`) never hits the `is_empty()` guards above at all:
/// `raw_inputs`/`raw_outputs` end up non-empty, just SHORTER than what the
/// source actually wrote, and the bad sibling is silently dropped with zero
/// error — verified live (`crates/vj-sim/tests/specify_discovery.rs`'s
/// `a_bad_sibling_input_terminal_in_an_otherwise_valid_multi_terminal_\
/// path_is_a_named_error`/`..._output_terminal_..._` tests). The count
/// check right after this function's own
/// `raw_inputs`/`raw_outputs` collection closes that gap directly, by
/// comparing against [`syntax_terminal_counts`]'s own syntax-level count
/// (from `list_of_path_inputs`/`list_of_path_outputs` itself, upstream of
/// any AST-level filtering) — independent of `validate_direction`, whose
/// own doc comment explains why it cannot do this.
fn discover_path<'d>(
    eval: &EvalSession<'d>,
    instance: InstanceId,
    path: &Symbol<'d>,
    ports: &HashMap<SymbolId, ArgumentDirection>,
    trees: &[SyntaxTree],
) -> Result<Vec<PathEntry>, ElabError> {
    let raw_inputs: Vec<_> = path.timing_path_inputs().collect();
    let raw_outputs: Vec<_> = path.timing_path_outputs().collect();
    if raw_inputs.is_empty() {
        return Err(unsupported(
            path,
            "specify path has no input terminal sv-lang could resolve (LRM 30.4.1's source \
             restriction already rejected it upstream, or it uses a terminal form this \
             workspace does not resolve, e.g. `interface_identifier.port_identifier`)"
                .to_string(),
        ));
    }
    if raw_outputs.is_empty() {
        return Err(unsupported(
            path,
            "specify path has no output terminal sv-lang could resolve (LRM 30.4.1's \
             destination restriction already rejected it upstream, or it uses a terminal form \
             this workspace does not resolve)"
                .to_string(),
        ));
    }
    // Non-empty is not the same as "nothing was dropped": compare against
    // the syntax-level terminal count (see `syntax_terminal_counts`'s own
    // doc comment) to catch a sibling terminal sv-lang's own per-terminal
    // filtering silently removed from an otherwise multi-terminal
    // declaration -- the gap the `is_empty()` guards above cannot see.
    let (syntax_input_count, syntax_output_count) = syntax_terminal_counts(path, trees)?;
    if raw_inputs.len() != syntax_input_count {
        return Err(unsupported(
            path,
            format!(
                "specify path's `list_of_path_inputs` names {syntax_input_count} terminal(s) in \
                 the source, but only {} resolved (LRM 30.4.1: \"the module path source shall be \
                 a net ... connected to an input or inout port\") -- at least one sibling input \
                 terminal violates this restriction and was silently dropped by sv-lang's own \
                 per-terminal filtering rather than failing the whole declaration",
                raw_inputs.len()
            ),
        ));
    }
    if raw_outputs.len() != syntax_output_count {
        return Err(unsupported(
            path,
            format!(
                "specify path's output terminal list names {syntax_output_count} terminal(s) in \
                 the source, but only {} resolved (LRM 30.4.1: \"the module path destination \
                 shall be a net or variable ... connected to an output or inout port\") -- at \
                 least one sibling output/destination terminal violates this restriction and \
                 was silently dropped by sv-lang's own per-terminal filtering rather than \
                 failing the whole declaration",
                raw_outputs.len()
            ),
        ));
    }
    let inputs = raw_inputs
        .into_iter()
        .map(|e| resolve_terminal(eval, path, ports, e, true))
        .collect::<Result<Vec<_>, _>>()?;
    let outputs = raw_outputs
        .into_iter()
        .map(|e| resolve_terminal(eval, path, ports, e, false))
        .collect::<Result<Vec<_>, _>>()?;
    let connection = path.timing_path_connection_kind();
    // LRM §30.4.7: the path operator's own overall polarity (`+*>`/`-*>`/
    // `+=>`/`-=>`, or none) -- metadata only, see [`PathEntry::polarity`]'s
    // own doc comment. Read once here: every desugared entry sharing this
    // one `path_declaration` (30.4.6) shares its one polarity too, exactly
    // like they already share one `path_uid`/delay list.
    let polarity = path.timing_path_polarity();
    let path_uid = path.uid();
    // LRM §30.4.3 (Task 7): this path's own edge-sensitivity, plus the
    // edge-sensitive suffix's data-source expression (reduced to a debug
    // name) -- the ONE call to `PathEdge::from_accessors` (hence to
    // `Symbol::timing_path_edge_source_expr()`) every desugared entry
    // sharing this one `path_declaration` reuses, exactly like
    // `polarity`/`path_uid`/the (not-yet-evaluated) delay list above.
    let (edge, edge_source) = PathEdge::from_accessors(path);
    let edge_data_source_name = edge_source
        .and_then(|e| e.referenced_symbol())
        .map(|s| s.name().to_string());
    // LRM §30.4.4 (Task 8): this path's own state-dependency, shared by
    // every desugared entry exactly like `polarity`/`edge`/`path_uid`
    // above (30.4.6: several entries sharing one declaration share its one
    // `if`/`ifnone` too).
    let condition = resolve_condition(eval, path)?;
    let mut out = Vec::new();
    match connection {
        sv_lang::TimingPathConnectionKind::Full => {
            for o in &outputs {
                for i in &inputs {
                    out.push(PathEntry {
                        instance,
                        inputs: vec![i.clone()],
                        outputs: vec![o.clone()],
                        connection,
                        path_uid: path_uid.clone(),
                        delays: PathDelaySet::default(),
                        polarity,
                        edge,
                        edge_data_source_name: edge_data_source_name.clone(),
                        condition: condition.clone(),
                        reject_limit: PathDelaySet::default(),
                        error_limit: PathDelaySet::default(),
                        pulse_style: PulseStyle::default(),
                        showcancelled: false,
                    });
                }
            }
        }
        sv_lang::TimingPathConnectionKind::Parallel => {
            if inputs.len() != 1 || outputs.len() != 1 {
                return Err(unsupported(
                    path,
                    format!(
                        "parallel (`=>`) module path with {} input(s) and {} output(s) \
                         (unexpected AST shape — LRM Annex A.7.2's `parallel_path_description` \
                         grammar only allows a single terminal on each side)",
                        inputs.len(),
                        outputs.len()
                    ),
                ));
            }
            out.push(PathEntry {
                instance,
                inputs,
                outputs,
                connection,
                path_uid,
                delays: PathDelaySet::default(),
                polarity,
                edge,
                edge_data_source_name,
                condition,
                reject_limit: PathDelaySet::default(),
                error_limit: PathDelaySet::default(),
                pulse_style: PulseStyle::default(),
                showcancelled: false,
            });
        }
    }
    Ok(out)
}

/// `path`'s own `(input_count, output_count)` as actually WRITTEN in its
/// `path_declaration` syntax (Annex A.7.2's `list_of_path_inputs`/
/// `list_of_path_outputs`) — upstream of sv-lang's own per-terminal LRM
/// 30.4.1 filtering (`SpecifyBlockSymbol::checkPathTerminal`, consulted one
/// terminal at a time by `bindTerminal`), which is why `timing_path_
/// inputs()`/`_outputs()` (what `raw_inputs`/`raw_outputs` hold) cannot be
/// compared against each other to detect a dropped sibling: both sides of
/// that comparison would already be post-filtering. This function walks
/// `trees` for the one `path.syntax(tree)` resolves against — the SAME
/// `Symbol::syntax(&SyntaxTree)` pattern `vj::nets::net_kind_of`
/// already uses to recover a symbol's own declaration syntax — then
/// unwraps a `ConditionalPathDeclaration`/`IfNonePathDeclaration` wrapper
/// down to the underlying `PathDeclaration` the same way slang's own
/// `TimingPathSymbol::resolve()` does (`if (a) (b=>q)=1;` / `(b=>q)=1 \
/// else 1;` both still describe exactly one `list_of_path_inputs`/
/// `list_of_path_outputs` pair). `PathDescriptionSyntax::inputs()` is the
/// one input list shared by every path shape (simple AND edge-sensitive);
/// the output list lives on whichever `PathSuffixSyntax` variant the
/// declaration uses (`SimplePathSuffix` for `*>`/`=>`, `EdgeSensitivePathSuffix`
/// for `posedge clk => (q +: d)`-shaped paths), so both are matched
/// explicitly rather than assuming one shape.
fn syntax_terminal_counts<'d>(
    path: &Symbol<'d>,
    trees: &[SyntaxTree],
) -> Result<(usize, usize), ElabError> {
    let node = trees
        .iter()
        .find_map(|tree| path.syntax(tree))
        .ok_or_else(|| {
            unsupported(
                path,
                "specify path declaration has no syntax node in any of the design's syntax \
                 trees (unexpected AST shape)"
                    .to_string(),
            )
        })?;
    let decl = match node.kind() {
        SyntaxKind::PathDeclaration => <PathDeclarationSyntax as sv_lang::AstNode>::cast(node),
        SyntaxKind::ConditionalPathDeclaration => {
            <ConditionalPathDeclarationSyntax as sv_lang::AstNode>::cast(node).map(|n| n.path())
        }
        SyntaxKind::IfNonePathDeclaration => {
            <IfNonePathDeclarationSyntax as sv_lang::AstNode>::cast(node).map(|n| n.path())
        }
        other => {
            return Err(unsupported(
                path,
                format!(
                    "specify path declaration's own syntax node is of kind `{other:?}` \
                     (expected PathDeclaration, ConditionalPathDeclaration or \
                     IfNonePathDeclaration -- unexpected AST shape)"
                ),
            ));
        }
    }
    .ok_or_else(|| {
        unsupported(
            path,
            "specify path declaration's own syntax node failed to cast to its expected shape \
             (unexpected AST shape)"
                .to_string(),
        )
    })?;
    let desc = decl.desc();
    let input_count = desc.inputs().iter().count();
    let output_count = match desc.suffix() {
        PathSuffixSyntax::SimplePathSuffix(s) => s.outputs().iter().count(),
        PathSuffixSyntax::EdgeSensitivePathSuffix(s) => s.outputs().iter().count(),
    };
    Ok((input_count, output_count))
}

#[cfg(test)]
mod tests {
    use sv_lang::{Compilation, ConstantValue, Design, Session, Symbol};
    use sv_lang_kinds::SymbolKind;
    use vj_abi::bit4::Bit4;

    use super::{PathDelaySet, PathEdge, PulseStyle, TimingModel};
    use crate::netlist::InstanceId;
    use crate::symid::SymbolUid;

    fn compile(src: &str) -> Design {
        let session = Session::new();
        let mut comp = Compilation::new(&session).expect("compilation created");
        comp.add_source(src).expect("source added");
        comp.compile().expect("design compiled")
    }

    fn top_body(design: &Design) -> Symbol<'_> {
        design
            .top_instances()
            .next()
            .expect("one top instance")
            .instance_body()
            .expect("top instance has a body")
    }

    /// SDF's Table 32-4 expansion builds a table twelve values at a time; the array form
    /// round-trips in [`TRANSITIONS`] order, which is the order `of` indexes by.
    #[test]
    fn transitions_array_round_trips_in_the_documented_order() {
        let t = [10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21];
        let set = PathDelaySet::from_transitions(t);
        assert_eq!(set.transitions(), t);
        for (i, &(from, to)) in super::TRANSITIONS.iter().enumerate() {
            assert_eq!(set.of(from, to), t[i], "{from:?}->{to:?}");
        }
        // The 12-value `from_list` form copies in the same order.
        assert_eq!(PathDelaySet::from_list(&t).unwrap(), set);
    }

    /// LRM 31.9.1: a path floor raises the transitions below it and leaves the rest alone,
    /// transition by transition (a 6-value list keeps its larger delays).
    #[test]
    fn at_least_raises_only_the_delays_below_the_floor() {
        let set = PathDelaySet::from_list(&[2, 9, 4, 3, 12, 1]).expect("six values");
        let raised = set.at_least(5);
        for (from, to) in [
            (Bit4::Zero, Bit4::One),
            (Bit4::One, Bit4::Zero),
            (Bit4::Zero, Bit4::Z),
            (Bit4::Z, Bit4::One),
            (Bit4::One, Bit4::Z),
            (Bit4::Z, Bit4::Zero),
            (Bit4::X, Bit4::One),
            (Bit4::One, Bit4::X),
        ] {
            assert_eq!(
                raised.of(from, to),
                set.of(from, to).max(5),
                "{from:?}->{to:?}"
            );
        }
        assert_eq!(raised.of(Bit4::One, Bit4::Zero), 9);
        assert_eq!(raised.of(Bit4::Zero, Bit4::One), 5);
        assert_eq!(raised.min_all(), 5);
        // A floor of 0 changes nothing.
        assert_eq!(set.at_least(0), set);
    }

    #[test]
    fn seed_specparams_round_trips_constant_value() {
        let design =
            compile("module m;\n  specparam tRise = 10;\n  specparam tFall = 7;\nendmodule\n");
        let body = top_body(&design);
        let mut model = TimingModel::new();
        model.seed_specparams(&[(InstanceId(0), body)]);

        let rise_uid = body
            .members()
            .find(|s| s.name() == "tRise")
            .expect("tRise member")
            .uid();
        let fall_uid = body
            .members()
            .find(|s| s.name() == "tFall")
            .expect("tFall member")
            .uid();

        assert_eq!(
            model
                .specparam(InstanceId(0), &rise_uid)
                .and_then(ConstantValue::as_i64),
            Some(10)
        );
        assert_eq!(
            model
                .specparam(InstanceId(0), &fall_uid)
                .and_then(ConstantValue::as_i64),
            Some(7)
        );
        // No specparam was seeded under a different instance id.
        assert!(model.specparam(InstanceId(1), &rise_uid).is_none());
    }

    #[test]
    fn set_specparam_overwrites_the_seeded_value() {
        // Simulates what Task 28's real `$sdf_annotate` LABEL annotation
        // will do: mutate an already-seeded table in place, through an API
        // that needs no live `EvalSession`/`Design` of its own.
        // `tFall`'s own frozen value stands in for the new, SDF-supplied
        // value Task 28 would compute from a real `.sdf` file -- this task
        // only needs SOME concrete, non-seeded `ConstantValue` to move the
        // table to, not a hand-built one (`sv_lang::SVInt` has no public
        // "build an owned integer of value N" constructor outside the
        // frozen-design read path this file already uses for seeding).
        let design =
            compile("module m;\n  specparam tRise = 10;\n  specparam tFall = 22;\nendmodule\n");
        let body = top_body(&design);
        let mut model = TimingModel::new();
        model.seed_specparams(&[(InstanceId(0), body)]);
        let uid = body
            .members()
            .find(|s| s.name() == "tRise")
            .expect("tRise member")
            .uid();
        assert_eq!(
            model
                .specparam(InstanceId(0), &uid)
                .and_then(ConstantValue::as_i64),
            Some(10)
        );

        let new_value = body
            .members()
            .find(|s| s.name() == "tFall")
            .expect("tFall member")
            .constant_value()
            .expect("tFall has a constant value");
        model.set_specparam(InstanceId(0), uid.clone(), new_value);

        assert_eq!(
            model
                .specparam(InstanceId(0), &uid)
                .and_then(ConstantValue::as_i64),
            Some(22)
        );
    }

    #[test]
    fn seed_specparams_finds_specparams_declared_inside_a_specify_block() {
        // Review fix (r1): a `specparam` declared INSIDE `specify ...
        // endspecify` (LRM 30.3's own `specify_item` production lists
        // `specparam_declaration`) is legal, and is the ONLY legal location
        // for a `PATHPULSE$` specparam (30.7.1). Its real `Specparam`
        // symbol is a child of the `SpecifyBlock` member, never a direct
        // `Specparam` member of the module body the way a module-scope one
        // is -- `seed_specparams` must still find it.
        let design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a => q) = tRise;\n   \
             specparam tRise = 10;\n    specparam PATHPULSE$ = 3;\n  endspecify\nendmodule\n",
        );
        let body = top_body(&design);
        let mut model = TimingModel::new();
        model.seed_specparams(&[(InstanceId(0), body)]);

        let specify = body
            .members()
            .find(|s| s.kind() == SymbolKind::SpecifyBlock)
            .expect("specify block member");
        let rise_uid = specify
            .members()
            .find(|s| s.kind() == SymbolKind::Specparam && s.name() == "tRise")
            .expect("tRise member inside the specify block")
            .uid();
        let pulse_uid = specify
            .members()
            .find(|s| s.kind() == SymbolKind::Specparam && s.name() == "PATHPULSE$")
            .expect("PATHPULSE$ member inside the specify block")
            .uid();

        assert_eq!(
            model
                .specparam(InstanceId(0), &rise_uid)
                .and_then(ConstantValue::as_i64),
            Some(10),
            "a plain specparam declared inside the specify block must be seeded"
        );
        assert_eq!(
            model
                .specparam(InstanceId(0), &pulse_uid)
                .and_then(ConstantValue::as_i64),
            Some(3),
            "a PATHPULSE$ specparam -- legal only inside a specify block (30.7.1) -- must be \
             seeded too"
        );
    }

    // Task 4a: `PathDelaySet::from_list`'s 1/2/3-value forms (LRM Table
    // 30-2) and Table 30-3's own x-transition default algorithm. T5 adds
    // the 6/12-value worked examples below; these pin the basic shape
    // T4a's own `PathRetimer` actually reads.

    #[test]
    fn from_list_one_value_gives_every_known_transition_the_same_delay() {
        let d = PathDelaySet::from_list(&[10]).expect("a 1-value list is supported");
        for (from, to) in [
            (Bit4::Zero, Bit4::One),
            (Bit4::One, Bit4::Zero),
            (Bit4::Zero, Bit4::Z),
            (Bit4::Z, Bit4::One),
            (Bit4::One, Bit4::Z),
            (Bit4::Z, Bit4::Zero),
        ] {
            assert_eq!(d.of(from, to), 10, "{from:?} -> {to:?}");
        }
    }

    #[test]
    fn from_list_two_values_split_rise_and_fall_and_z_follows_the_matching_side() {
        let d = PathDelaySet::from_list(&[3, 5]).expect("a 2-value list is supported");
        assert_eq!(d.of(Bit4::Zero, Bit4::One), 3, "0->1 is trise");
        assert_eq!(d.of(Bit4::Z, Bit4::One), 3, "z->1 is trise");
        assert_eq!(d.of(Bit4::One, Bit4::Zero), 5, "1->0 is tfall");
        assert_eq!(d.of(Bit4::Z, Bit4::Zero), 5, "z->0 is tfall");
        assert_eq!(d.of(Bit4::Zero, Bit4::Z), 3, "0->z is trise");
        assert_eq!(d.of(Bit4::One, Bit4::Z), 5, "1->z is tfall");
    }

    #[test]
    fn from_list_three_values_give_z_its_own_delay_distinct_from_rise_and_fall() {
        let d = PathDelaySet::from_list(&[3, 5, 7]).expect("a 3-value list is supported");
        assert_eq!(d.of(Bit4::Zero, Bit4::One), 3);
        assert_eq!(d.of(Bit4::One, Bit4::Zero), 5);
        assert_eq!(d.of(Bit4::Zero, Bit4::Z), 7, "0->z is tz, not trise");
        assert_eq!(d.of(Bit4::One, Bit4::Z), 7, "1->z is tz, not tfall");
        // z->1/z->0 still follow rise/fall, per Table 30-2's own 3-value
        // column (only 0->z/1->z use the third value).
        assert_eq!(d.of(Bit4::Z, Bit4::One), 3);
        assert_eq!(d.of(Bit4::Z, Bit4::Zero), 5);
    }

    #[test]
    fn from_list_derives_x_transitions_via_table_30_3s_general_algorithm() {
        // Table 30-3's own general algorithm (`s->x` = min of the two
        // delays INTO x from a known state; `x->s` = max of the two delays
        // OUT of x into a known state), exercised over a 3-value list's own
        // six known transitions (r01=5, r10=12, r0z=17, rz1=r01=5,
        // r1z=r0z=17, rz0=r10=12 -- Table 30-2's own 3-value column).
        // `from_list_six_value_reproduces_the_lrm_worked_example_exactly`
        // below reproduces the LRM's own literal 6-value worked example
        // (30.5.2) through the SAME algorithm; this pins it against the
        // 3-value shape T4a actually built it for.
        let d = PathDelaySet::from_list(&[5, 12, 17]).expect("a 3-value list is supported");
        // r01=5, r10=12, r0z=17, rz1=5 (=r01), r1z=17 (=r0z), rz0=12 (=r10).
        assert_eq!(
            d.of(Bit4::Zero, Bit4::X),
            5,
            "0->x = min(0->z=17, 0->1=5) = 5"
        );
        assert_eq!(
            d.of(Bit4::One, Bit4::X),
            12,
            "1->x = min(1->z=17, 1->0=12) = 12"
        );
        assert_eq!(d.of(Bit4::Z, Bit4::X), 5, "z->x = min(z->1=5, z->0=12) = 5");
        assert_eq!(
            d.of(Bit4::X, Bit4::Zero),
            12,
            "x->0 = max(z->0=12, 1->0=12) = 12"
        );
        assert_eq!(
            d.of(Bit4::X, Bit4::One),
            5,
            "x->1 = max(z->1=5, 0->1=5) = 5"
        );
        assert_eq!(
            d.of(Bit4::X, Bit4::Z),
            17,
            "x->z = max(1->z=17, 0->z=17) = 17"
        );
    }

    // Task 5: `PathDelaySet::from_list`'s 6- and 12-value forms (LRM Table
    // 30-2) and the x-transition default algorithm (Table 30-3) applied to
    // them.

    #[test]
    fn from_list_one_value_gives_all_twelve_entries_the_same_delay() {
        // The 1-value test above only pins the six "known" transitions;
        // this one pins Table 30-3's algorithm degenerating correctly too
        // (s->x = min(s->s, s->s) = s; x->s = max(s->s, s->s) = s), so
        // EVERY one of the 12 entries -- not just the six Table 30-2 names
        // directly -- is the single given value.
        let d = PathDelaySet::from_list(&[10]).expect("a 1-value list is supported");
        for (from, to) in [
            (Bit4::Zero, Bit4::One),
            (Bit4::One, Bit4::Zero),
            (Bit4::Zero, Bit4::Z),
            (Bit4::Z, Bit4::One),
            (Bit4::One, Bit4::Z),
            (Bit4::Z, Bit4::Zero),
            (Bit4::Zero, Bit4::X),
            (Bit4::X, Bit4::One),
            (Bit4::One, Bit4::X),
            (Bit4::X, Bit4::Zero),
            (Bit4::X, Bit4::Z),
            (Bit4::Z, Bit4::X),
        ] {
            assert_eq!(d.of(from, to), 10, "{from:?} -> {to:?}");
        }
    }

    #[test]
    fn from_list_six_value_list_takes_each_known_transition_directly_no_grouping() {
        // Six DISTINCT values, so a wrong implementation that reused the
        // 1/2/3-value forms' rise/fall/z grouping (forcing tz1==t01,
        // t1z==t0z, tz0==t10) would fail this test, unlike the LRM's own
        // worked example below where that grouping happens to coincide by
        // construction for some of the pairs.
        let d = PathDelaySet::from_list(&[1, 2, 3, 4, 5, 6]).expect("a 6-value list is supported");
        assert_eq!(d.of(Bit4::Zero, Bit4::One), 1, "t01");
        assert_eq!(d.of(Bit4::One, Bit4::Zero), 2, "t10");
        assert_eq!(d.of(Bit4::Zero, Bit4::Z), 3, "t0z");
        assert_eq!(d.of(Bit4::Z, Bit4::One), 4, "tz1 -- independent of t01");
        assert_eq!(d.of(Bit4::One, Bit4::Z), 5, "t1z -- independent of t0z");
        assert_eq!(d.of(Bit4::Z, Bit4::Zero), 6, "tz0 -- independent of t10");
    }

    #[test]
    fn from_list_six_value_reproduces_the_lrm_worked_example_exactly() {
        // LRM 1800-2023 30.5.2's own literal worked example: `(C => Q) =
        // (5, 12, 17, 10, 6, 22);` -> `0->x=5, 1->x=6, z->x=10, x->0=22,
        // x->1=10, x->z=17` (verified directly against the LRM text,
        // Table 30-3's own "Usage" rows).
        let d =
            PathDelaySet::from_list(&[5, 12, 17, 10, 6, 22]).expect("a 6-value list is supported");
        // The six given transitions themselves (Table 30-2's 6-value
        // column: t01, t10, t0z, tz1, t1z, tz0, in that order).
        assert_eq!(d.of(Bit4::Zero, Bit4::One), 5, "t01");
        assert_eq!(d.of(Bit4::One, Bit4::Zero), 12, "t10");
        assert_eq!(d.of(Bit4::Zero, Bit4::Z), 17, "t0z");
        assert_eq!(d.of(Bit4::Z, Bit4::One), 10, "tz1");
        assert_eq!(d.of(Bit4::One, Bit4::Z), 6, "t1z");
        assert_eq!(d.of(Bit4::Z, Bit4::Zero), 22, "tz0");
        // The six derived x-transitions, matching the LRM's own stated
        // numbers exactly.
        assert_eq!(d.of(Bit4::Zero, Bit4::X), 5, "0->x = min(17, 5) = 5");
        assert_eq!(d.of(Bit4::One, Bit4::X), 6, "1->x = min(6, 12) = 6");
        assert_eq!(d.of(Bit4::Z, Bit4::X), 10, "z->x = min(10, 22) = 10");
        assert_eq!(d.of(Bit4::X, Bit4::Zero), 22, "x->0 = max(22, 12) = 22");
        assert_eq!(d.of(Bit4::X, Bit4::One), 10, "x->1 = max(10, 5) = 10");
        assert_eq!(d.of(Bit4::X, Bit4::Z), 17, "x->z = max(6, 17) = 17");
    }

    #[test]
    fn from_list_twelve_value_list_is_all_explicit_no_derivation() {
        // Twelve DISTINCT values, in Table 30-2's own 12-value column order
        // (t01,t10,t0z,tz1,t1z,tz0,t0x,tx1,t1x,tx0,txz,tzx). If the
        // x-involving entries were (wrongly) derived via Table 30-3's
        // algorithm instead of copied straight through, e.g. `0->x` would
        // come out `min(t0z=3, t01=1) = 1`, not the `7` actually given --
        // this test fails loudly on that mistake instead of silently
        // tolerating it.
        let d = PathDelaySet::from_list(&[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])
            .expect("a 12-value list is supported");
        assert_eq!(d.of(Bit4::Zero, Bit4::One), 1, "t01");
        assert_eq!(d.of(Bit4::One, Bit4::Zero), 2, "t10");
        assert_eq!(d.of(Bit4::Zero, Bit4::Z), 3, "t0z");
        assert_eq!(d.of(Bit4::Z, Bit4::One), 4, "tz1");
        assert_eq!(d.of(Bit4::One, Bit4::Z), 5, "t1z");
        assert_eq!(d.of(Bit4::Z, Bit4::Zero), 6, "tz0");
        assert_eq!(
            d.of(Bit4::Zero, Bit4::X),
            7,
            "t0x -- given directly, not derived"
        );
        assert_eq!(
            d.of(Bit4::X, Bit4::One),
            8,
            "tx1 -- given directly, not derived"
        );
        assert_eq!(
            d.of(Bit4::One, Bit4::X),
            9,
            "t1x -- given directly, not derived"
        );
        assert_eq!(
            d.of(Bit4::X, Bit4::Zero),
            10,
            "tx0 -- given directly, not derived"
        );
        assert_eq!(
            d.of(Bit4::X, Bit4::Z),
            11,
            "txz -- given directly, not derived"
        );
        assert_eq!(
            d.of(Bit4::Z, Bit4::X),
            12,
            "tzx -- given directly, not derived"
        );
    }

    #[test]
    fn from_list_rejects_any_length_other_than_1_2_3_6_or_12() {
        for len in [4, 5, 7, 8, 9, 10, 11, 13] {
            let d = vec![1u64; len];
            let err = PathDelaySet::from_list(&d).unwrap_err();
            assert!(
                err.contains(&len.to_string()),
                "the error must name the bad length, not just say \"unsupported\": {err}"
            );
        }
    }

    #[test]
    fn set_path_delays_attaches_to_every_desugared_entry_sharing_one_path_uid() {
        // `(a, b *> q) = 10;` desugars into two `PathEntry`s (30.4.6)
        // sharing one `path_uid`; `set_path_delays` must reach both.
        let mut design = compile(
            "module m(input a, input b, output q);\n  assign q = a | b;\n  specify\n    (a, b \
             *> q) = 10;\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 2);
        let path_uid = model.paths[0].path_uid.clone();
        assert_eq!(
            model.paths[1].path_uid, path_uid,
            "both entries share one path_uid"
        );

        let delays = PathDelaySet::from_list(&[3, 5]).expect("a 2-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, delays);
        assert_eq!(model.paths[0].delays, delays);
        assert_eq!(model.paths[1].delays, delays);
    }

    const ALL_TRANSITIONS: [(Bit4, Bit4); 12] = [
        (Bit4::Zero, Bit4::One),
        (Bit4::One, Bit4::Zero),
        (Bit4::Zero, Bit4::Z),
        (Bit4::Z, Bit4::One),
        (Bit4::One, Bit4::Z),
        (Bit4::Z, Bit4::Zero),
        (Bit4::Zero, Bit4::X),
        (Bit4::X, Bit4::One),
        (Bit4::One, Bit4::X),
        (Bit4::X, Bit4::Zero),
        (Bit4::X, Bit4::Z),
        (Bit4::Z, Bit4::X),
    ];

    /// sdf T10 (LRM 30.7): with no `PATHPULSE$`, every transition's reject
    /// AND error limit is that transition's OWN delay (here a 12-value list
    /// with twelve distinct values, so a limit that merely copied one
    /// transition's delay everywhere would be caught).
    #[test]
    fn pulse_limits_default_to_each_transitions_own_delay() {
        let mut design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a => q) = 10;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        let path_uid = model.paths[0].path_uid.clone();
        let delays = PathDelaySet::from_list(&[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])
            .expect("a 12-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, delays);
        for (from, to) in ALL_TRANSITIONS {
            let d = delays.of(from, to);
            assert_eq!(
                model.paths[0].reject_limit.of(from, to),
                d,
                "{from:?}->{to:?}"
            );
            assert_eq!(
                model.paths[0].error_limit.of(from, to),
                d,
                "{from:?}->{to:?}"
            );
        }
        assert_eq!(
            model.paths[0].reject_limit.of(Bit4::Zero, Bit4::One),
            1,
            "twelve DISTINCT limits, not one copied value"
        );
        assert_eq!(model.paths[0].reject_limit.of(Bit4::Z, Bit4::X), 12);
    }

    /// sdf T10: `set_path_pulse_limits` reaches every desugared entry of one
    /// declaration, sets all twelve transitions, leaves the delays alone,
    /// and raises an error limit below the reject limit up to it (the
    /// documented implementation-defined choice).
    #[test]
    fn set_path_pulse_limits_reaches_every_entry_and_clamps_error_to_reject() {
        let mut design = compile(
            "module m(input a, input b, output q);\n  assign q = a | b;\n  specify\n    (a, b \
             *> q) = 10;\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        let path_uid = model.paths[0].path_uid.clone();
        let delays = PathDelaySet::from_list(&[10]).expect("a 1-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, delays);

        model.set_path_pulse_limits(InstanceId(0), &path_uid, 2, 6);
        for p in &model.paths {
            for (from, to) in ALL_TRANSITIONS {
                assert_eq!(p.reject_limit.of(from, to), 2);
                assert_eq!(p.error_limit.of(from, to), 6);
            }
            assert_eq!(p.delays, delays, "pulse limits never touch the delays");
        }

        model.set_path_pulse_limits(InstanceId(0), &path_uid, 6, 2);
        for p in &model.paths {
            assert_eq!(p.reject_limit.of(Bit4::Zero, Bit4::One), 6);
            assert_eq!(
                p.error_limit.of(Bit4::Zero, Bit4::One),
                6,
                "error < reject is raised to the reject limit"
            );
        }

        // Re-annotating the delays re-establishes the delay-following default.
        let longer = PathDelaySet::from_list(&[20]).expect("a 1-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, longer);
        assert_eq!(model.paths[0].reject_limit, longer);
        assert_eq!(model.paths[1].error_limit, longer);
    }

    /// sdf T31 (LRM 30.7.2, 32.7): the global percentage options set every transition's limit to
    /// that percentage of ITS OWN delay, and an error limit below the reject limit is raised to it.
    #[test]
    fn apply_pulse_percent_scales_each_transitions_own_delay() {
        let mut design = compile(
            "module m(input a, input b, output q);\n  assign q = a | b;\n  specify\n    (a, b \
             *> q) = 10;\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        let path_uid = model.paths[0].path_uid.clone();
        let delays = PathDelaySet::from_list(&[10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120])
            .expect("a 12-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, delays);

        model.apply_pulse_percent(50.0, 25.0);
        for p in &model.paths {
            assert_eq!(p.delays, delays, "limits never touch the delays");
            for (from, to) in ALL_TRANSITIONS {
                let d = delays.of(from, to);
                assert_eq!(
                    p.reject_limit.of(from, to),
                    d / 2,
                    "reject {from:?}->{to:?}"
                );
                assert_eq!(
                    p.error_limit.of(from, to),
                    d / 2,
                    "error 25% < reject 50% is raised to the reject limit"
                );
            }
        }

        model.apply_pulse_percent(20.0, 90.0);
        for p in &model.paths {
            for (from, to) in ALL_TRANSITIONS {
                let d = delays.of(from, to);
                assert_eq!(p.reject_limit.of(from, to), d / 5);
                assert_eq!(p.error_limit.of(from, to), d * 9 / 10);
            }
        }

        // 100/100 is the LRM default: limits equal the delays, exactly.
        model.apply_pulse_percent(100.0, 100.0);
        assert_eq!(model.paths[0].reject_limit, delays);
        assert_eq!(model.paths[1].error_limit, delays);

        // Rounds to the nearest tick (3 * 50% = 1.5 -> 2).
        let odd = PathDelaySet::from_list(&[3]).expect("a 1-value list is supported");
        model.set_path_delays(InstanceId(0), &path_uid, odd);
        model.apply_pulse_percent(50.0, 100.0);
        assert_eq!(model.paths[0].reject_limit.of(Bit4::Zero, Bit4::One), 2);
        assert_eq!(model.paths[0].error_limit.of(Bit4::Zero, Bit4::One), 3);
    }

    /// sdf T31 (LRM 30.7.4.1/30.7.4.2): "The pulse style invocation options take precedence over
    /// pulse style specify block declarations" and the same for showcancelled; an axis whose
    /// option was not given keeps the declarations, each axis on its own.
    #[test]
    fn pulse_options_override_declarations_and_an_absent_option_leaves_them() {
        let mut design = compile(
            "module m(input a, output q, output r, output s);\n  assign q = a;\n  assign r = a;\n  \
             assign s = a;\n  specify\n    pulsestyle_ondetect q;\n    showcancelled q;\n    \
             noshowcancelled r;\n    (a => q) = 1;\n    (a => r) = 1;\n    (a => s) = 1;\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let settings = |model: &TimingModel| -> Vec<(PulseStyle, bool)> {
            ["q", "r", "s"]
                .iter()
                .map(|out| {
                    let p = model
                        .paths
                        .iter()
                        .find(|p| p.outputs[0].0.path().rsplit('.').next() == Some(*out))
                        .unwrap_or_else(|| panic!("no path to {out}"));
                    (p.pulse_style, p.showcancelled)
                })
                .collect()
        };

        let mut plain = TimingModel::new();
        plain
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(
            settings(&plain),
            vec![
                // q: declared on-detect and showcancelled; r: declared off; s: built-in default.
                (PulseStyle::OnDetect, true),
                (PulseStyle::OnEvent, false),
                (PulseStyle::OnEvent, false)
            ],
            "declarations, then the built-in default: on-event, noshowcancelled"
        );

        let discovered = |style: Option<PulseStyle>, show: Option<bool>| {
            let mut model = TimingModel::new();
            model.set_pulse_options(style, show);
            model
                .discover(&eval, &[(InstanceId(0), body)])
                .unwrap_or_else(|e| panic!("discover failed: {e}"));
            settings(&model)
        };
        use PulseStyle::{OnDetect, OnEvent};
        // Both options: they beat q's `pulsestyle_onevent` and r's `noshowcancelled`.
        assert_eq!(
            discovered(Some(OnDetect), Some(true)),
            vec![(OnDetect, true), (OnDetect, true), (OnDetect, true)]
        );
        // Style option only: showcancelled keeps the declarations (q on, r off, s default).
        assert_eq!(
            discovered(Some(OnEvent), None),
            vec![(OnEvent, true), (OnEvent, false), (OnEvent, false)]
        );
        // `--noshowcancelled` forces off what q's declaration turned on, and the style axis keeps
        // q's declaration.
        assert_eq!(
            discovered(None, Some(false)),
            vec![(OnDetect, false), (OnEvent, false), (OnEvent, false)]
        );
        // `--showcancelled` forces on what r's `noshowcancelled` declared off.
        assert_eq!(
            discovered(None, Some(true)),
            vec![(OnDetect, true), (OnEvent, true), (OnEvent, true)]
        );
    }

    // Task 4a review fix (r1): LRM §30.4.7's own polarity -- the path
    // operator's `+`/`-` -- round-trips into `PathEntry::polarity`, readable
    // via the debug/VPI-facing `PathEntry::debug_polarity` accessor.
    // `vj::specify`'s own
    // `path_retimer_never_reads_polarity_in_its_delay_computation` test
    // proves the OTHER half of this task's acceptance text: that nothing in
    // the retiming math ever consults it.

    #[test]
    fn discover_resolves_positive_polarity_on_a_full_connection_path() {
        use sv_lang::TimingPathPolarity;

        let mut design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a +*> q) = 1;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(
            model.paths[0].debug_polarity(),
            TimingPathPolarity::Positive
        );
    }

    #[test]
    fn discover_resolves_negative_polarity_on_a_parallel_connection_path() {
        use sv_lang::TimingPathPolarity;

        let mut design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a -=> q) = 1;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(
            model.paths[0].debug_polarity(),
            TimingPathPolarity::Negative
        );
    }

    #[test]
    fn discover_resolves_unknown_polarity_when_no_polarity_operator_is_written() {
        use sv_lang::TimingPathPolarity;

        let mut design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a => q) = 1;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].debug_polarity(), TimingPathPolarity::Unknown);
    }

    // Task 7 (LRM 30.4.3, edge-sensitive paths): `PathEdge` derivation --
    // verified LIVE (not assumed) against sv-lang=0.1.9/slang 11.0 that
    // `timing_path_edge_identifier()` ALONE cannot tell a plain path apart
    // from an edge-sensitive one with no edge keyword (both report
    // `EdgeKind::None`), and that the identifier is populated even for the
    // edge-sensitive grammar's "simple destination" alternative (no
    // `(dest:data)` suffix at all) -- see `PathEdge`'s own doc comment for
    // the full four-case matrix this pins.

    #[test]
    fn discover_resolves_specific_posedge_on_an_edge_sensitive_path() {
        use sv_lang::EdgeKind;

        let mut design = compile(
            "module m(input clock, in, output out);\n  specify\n    (posedge clock => (out +: \
             in)) = (10, 8);\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].edge, PathEdge::Specific(EdgeKind::PosEdge));
        assert_eq!(
            model.paths[0].debug_edge_source_expr_name(),
            Some("in"),
            "the `: in` data-source expression's referenced symbol name must round-trip"
        );
    }

    #[test]
    fn discover_resolves_specific_negedge_on_an_edge_sensitive_path() {
        use sv_lang::EdgeKind;

        let mut design = compile(
            "module m(input clock, in, output out);\n  specify\n    (negedge clock => (out -: \
             in)) = (10, 8);\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].edge, PathEdge::Specific(EdgeKind::NegEdge));
    }

    #[test]
    fn discover_resolves_edge_sensitive_any_transition_when_no_edge_identifier_is_written() {
        // LRM 30.4.3's own Example 3: `(clock => (out : in)) = (10, 8);` --
        // no edge keyword at all, but the `(dest:data)` destination suffix
        // marks this as edge-sensitive (`PathEdge::Any`), not a plain
        // `PathEdge::None` simple path -- `timing_path_edge_identifier()`
        // alone reports `EdgeKind::None` for BOTH, which is exactly why
        // `PathEdge::from_accessors` also consults
        // `timing_path_edge_source_expr()`.
        let mut design = compile(
            "module m(input clock, in, output out);\n  specify\n    (clock => (out : in)) = \
             (10, 8);\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].edge, PathEdge::Any);
    }

    #[test]
    fn discover_resolves_no_edge_sensitivity_on_a_plain_simple_path() {
        // The negative case: a plain 30.4.2 simple path (no edge-sensitive
        // suffix at all) must resolve `PathEdge::None`, not `PathEdge::Any`
        // -- `edge_source_expr().is_some()` must be `false` here, the
        // discriminator `PathEdge::from_accessors` relies on.
        let mut design = compile(
            "module m(input a, output q);\n  assign q = a;\n  specify\n    (a => q) = 1;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].edge, PathEdge::None);
        assert_eq!(model.paths[0].debug_edge_source_expr_name(), None);
    }

    #[test]
    fn discover_resolves_specific_posedge_even_with_the_simple_destination_suffix() {
        // `(posedge clk => q) = 1;` -- edge keyword given, but NO
        // `(dest:data)` suffix at all (`edge_source_expr()` is `None` here):
        // `timing_path_edge_identifier()` is still populated, proving the
        // identifier is a field of the shared `[edge_identifier]`
        // production, independent of which destination-suffix alternative
        // is used -- `PathEdge::from_accessors` must still resolve
        // `Specific(PosEdge)`, not fall through to `None`.
        use sv_lang::EdgeKind;

        let mut design = compile(
            "module m(input clk, output q);\n  specify\n    (posedge clk => q) = 1;\n  \
             endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(model.paths.len(), 1);
        assert_eq!(model.paths[0].edge, PathEdge::Specific(EdgeKind::PosEdge));
        assert_eq!(model.paths[0].debug_edge_source_expr_name(), None);
    }

    #[test]
    fn discover_shares_one_edge_spec_across_every_desugared_entry_of_a_full_connection() {
        // LRM 30.4.6's own desugaring: a multi-terminal FULL (`*>`)
        // edge-sensitive declaration shares its one `edge`/data-source name
        // across every desugared `PathEntry`, exactly like it already
        // shares one `path_uid`/`polarity`/delay list.
        let mut design = compile(
            "module m(input clock, input a, input b, output q1, output q2);\n  specify\n    \
             (posedge clock *> (q1, q2 : a)) = (10, 8);\n  endspecify\nendmodule\n",
        );
        let eval = design.eval_session();
        let body = top_body(eval.design());
        let mut model = TimingModel::new();
        model
            .discover(&eval, &[(InstanceId(0), body)])
            .unwrap_or_else(|e| panic!("discover failed: {e}"));
        assert_eq!(
            model.paths.len(),
            2,
            "two desugared (clock*>q1), (clock*>q2) entries"
        );
        for p in &model.paths {
            assert_eq!(p.edge, PathEdge::Specific(sv_lang::EdgeKind::PosEdge));
            assert_eq!(p.debug_edge_source_expr_name(), Some("a"));
        }
    }
}