vj-codegen 0.1.0

//! T4 (`docs/superpowers/plans/2026-10-03-sva.md`): mirroring
//! `UnaryAssertionOperator`/`BinaryAssertionOperator` as typed Rust enums,
//! and recovering `Abort`/`Clocking`/`Case`'s positional children.
//!
//! ## The operator mirror
//!
//! `sv_lang::AssertionExpr::op()` hands back only the raw C++ enum
//! discriminant (`Option<i32>`, `None` for any `AssertionExprKind` other
//! than [`Unary`](AssertionExprKind::Unary)/[`Binary`](AssertionExprKind::Binary)
//! -- see its own doc comment) because `sv-lang` 0.1.9 has not yet minted a
//! typed Rust enum for either `UnaryAssertionOperator` or
//! `BinaryAssertionOperator` (plan §1.1). Both are plain, zero-based,
//! declaration-order C++ enums (`SLANG_ENUM`, `include/slang/util/Enum.h`
//! -- no explicit initializers anywhere in either `#define OP(x) ...`
//! block, `include/slang/ast/expressions/AssertionExpr.h` lines 37-61), so
//! their pinned values are exactly their declaration position:
//!
//! ```text
//! UnaryAssertionOperator: Not=0 NextTime=1 SNextTime=2 Always=3 SAlways=4
//!                          Eventually=5 SEventually=6                (7)
//! BinaryAssertionOperator: And=0 Or=1 Intersect=2 Throughout=3 Within=4
//!                           Iff=5 Until=6 SUntil=7 UntilWith=8
//!                           SUntilWith=9 Implies=10
//!                           OverlappedImplication=11
//!                           NonOverlappedImplication=12
//!                           OverlappedFollowedBy=13
//!                           NonOverlappedFollowedBy=14               (15)
//! ```
//!
//! [`AssertionUnaryOp`] and [`AssertionBinaryOp`] mirror these (named with
//! an `Assertion` prefix, not the plan prose's bare `UnaryOp`/`BinaryOp`,
//! because `sv_lang::{UnaryOp, BinaryOp}` already exist at the crate root
//! for ordinary `Expression` operators -- an unqualified `use` of both
//! would collide, and callers of this module and `module.rs`'s existing
//! `sv_lang::UnaryOp` import are the same leaf-compilation code, so the
//! names must coexist in one `use` block). [`Op`] is the plan's
//! `sv_sim_codegen::sva::Op`: a thin sum of the two, built by [`Op::of`],
//! which is also the single place the `AssertionExprKind::{Unary,Binary}`
//! disambiguation plan §1.1 describes happens -- `op()` is `None`/invalid
//! for every other kind, and `Op::of` rejects that loudly rather than
//! guessing which operator family a raw discriminant belongs to.
//!
//! Each mirror's `TryFrom<i32>` is exhaustive over the full `i32` domain
//! (every arm not in the pinned 0..=N-1 range falls through to a named
//! [`LoweringError`]) -- never a panic, per this workspace's "every kind
//! match shouts, never guesses" rule (ARCHITECTURE §7 item 9). The plan
//! prose describes this as a `From<i32>` that "panics"; `TryFrom` returning
//! `Result` is the actually-non-panicking shape that rule requires, so that
//! wording is implemented as `TryFrom`, not literal `From` + `panic!`.
//!
//! ## Positional children
//!
//! `AssertionExpr::children()` walks every `AssertionExprKind`'s "immediate
//! semantic children" generically as `SemNode`s, but a `SemNode` carries no
//! label -- for `Abort`/`Clocking`/`Case` specifically, which child is
//! "the condition" vs "the body" (or, for `Case`, which children are labels
//! vs a branch body vs the optional default) is only recoverable by
//! position, read off the C++ class layouts themselves
//! (`include/slang/ast/expressions/AssertionExpr.h`'s `visitExprs` for each):
//!
//! - `AbortAssertionExpr::visitExprs`: `condition.visit(); expr.visit();`
//!   -- children are `[condition, body]`, always exactly 2.
//! - `ClockingAssertionExpr::visitExprs`: `clocking.visit(); expr.visit();`
//!   -- children are `[event, body]`, always exactly 2 (the class's
//!   `clocking`/`expr` members are both plain references, never optional,
//!   so a `Clocking` node always carries both).
//! - `CaseAssertionExpr::visitExprs`: `expr.visit();` then, for each
//!   *non-default* `ItemGroup` in source order, each of its label
//!   `expressions` followed by its `body`; then, only if present,
//!   `defaultCase.visit()` last. The label *count* per item is
//!   data-dependent (16.12.16's `property_expr { , property_expr } :
//!   property_expr ;` allows any number of labels per item) and isn't
//!   recoverable from the flattened `children()` list alone -- [`case_children`]
//!   recovers it the same way [`super::ranges`] recovers delay/repetition
//!   bounds: from the *syntax* tree's typed accessor
//!   (`CasePropertyExprSyntax::items()`, each `StandardPropertyCaseItemSyntax::
//!   expressions()`), which preserves the per-item grouping the semantic
//!   children list flattens away, then partitions the flat `children()`
//!   list using those counts. This is a full, N-items/M-labels-each decoder,
//!   not a decoder narrowed to one hardcoded shape.
//!
//! Each decoder below has its own unit test compiling a live `Design` and
//! asserting the exact shape, so a future `sv-lang` upgrade that reorders
//! any of these children fails that test loudly instead of silently
//! mis-binding (plan §1.1's closing paragraph).
//!
//! This workaround lives entirely in `sv-sim-codegen`, like [`super::ranges`];
//! it adds no file to `sv-lang`, `sv-lang-sys`, or `sv-lang-kinds`.
#![allow(dead_code)]

use sv_lang::kinds::AssertionExprKind;
use sv_lang::nodes::{
    CasePropertyExprSyntax, ParenthesizedPropertyExprSyntax, PropertyCaseItemSyntax,
    PropertySpecSyntax,
};
use sv_lang::{AssertionExpr, AstNode, Node, SemNode, Symbol};

use super::trees::Trees;

use crate::error::LoweringError;

/// `node` with the syntax parentheses and a bare `property_spec` wrapper taken
/// off: the node that names the operator. slang hangs a property's syntax off
/// its outermost wrapper, so a property that is the whole body of a named
/// declaration (`property p; case (..) ... endcase endproperty`) or is written in
/// parentheses has the wrapper, not the operator, as its syntax node.
pub(crate) fn peel_property_parens(mut node: Node<'_>) -> Node<'_> {
    loop {
        if let Some(p) = ParenthesizedPropertyExprSyntax::cast(node) {
            node = p.expr().syntax();
        } else if let Some(s) = PropertySpecSyntax::cast(node)
            && s.clocking().is_none()
            && s.disable().is_none()
        {
            node = s.expr().syntax();
        } else {
            return node;
        }
    }
}

/// Mirrors slang's `UnaryAssertionOperator` (16.12.3, 16.12.10, 16.12.11,
/// 16.12.13 -- `not`, `nexttime`/`s_nexttime`, `always`/`s_always`,
/// `eventually`/`s_eventually`). Discriminants are pinned to the C++ enum's
/// declaration order (module doc comment above).
#[repr(i32)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AssertionUnaryOp {
    Not = 0,
    NextTime = 1,
    SNextTime = 2,
    Always = 3,
    SAlways = 4,
    Eventually = 5,
    SEventually = 6,
}

impl AssertionUnaryOp {
    /// The number of variants (7) -- the same "arity" guard this
    /// workspace's exhaustive kind enums already carry (e.g.
    /// `sv_sim_abi::Region::ALL`'s own arity tests).
    pub const COUNT: i32 = 7;
    /// Every variant, in pinned-discriminant order.
    pub const ALL: [AssertionUnaryOp; Self::COUNT as usize] = [
        AssertionUnaryOp::Not,
        AssertionUnaryOp::NextTime,
        AssertionUnaryOp::SNextTime,
        AssertionUnaryOp::Always,
        AssertionUnaryOp::SAlways,
        AssertionUnaryOp::Eventually,
        AssertionUnaryOp::SEventually,
    ];
}

impl TryFrom<i32> for AssertionUnaryOp {
    type Error = LoweringError;

    fn try_from(raw: i32) -> Result<Self, Self::Error> {
        match raw {
            0 => Ok(AssertionUnaryOp::Not),
            1 => Ok(AssertionUnaryOp::NextTime),
            2 => Ok(AssertionUnaryOp::SNextTime),
            3 => Ok(AssertionUnaryOp::Always),
            4 => Ok(AssertionUnaryOp::SAlways),
            5 => Ok(AssertionUnaryOp::Eventually),
            6 => Ok(AssertionUnaryOp::SEventually),
            other => Err(LoweringError::unsupported(
                &format!(
                    "UnaryAssertionOperator raw value {other} is out of the pinned 0..=6 range \
                     (Not..SEventually) -- either a malformed raw discriminant or a slang \
                     upgrade that added a variant this mirror does not yet know about"
                ),
                "sva::op::AssertionUnaryOp::try_from",
            )),
        }
    }
}

/// Mirrors slang's `BinaryAssertionOperator` (16.9.5-16.9.10's sequence
/// operators plus 16.12.4-16.12.9/16.12.12's property operators --
/// `and`/`or`/`intersect`/`throughout`/`within`, `iff`, `until`/`s_until`/
/// `until_with`/`s_until_with`, `|->`/`|=>`, `#-#`/`#=#`). Discriminants
/// are pinned to the C++ enum's declaration order (module doc comment
/// above).
#[repr(i32)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AssertionBinaryOp {
    And = 0,
    Or = 1,
    Intersect = 2,
    Throughout = 3,
    Within = 4,
    Iff = 5,
    Until = 6,
    SUntil = 7,
    UntilWith = 8,
    SUntilWith = 9,
    Implies = 10,
    OverlappedImplication = 11,
    NonOverlappedImplication = 12,
    OverlappedFollowedBy = 13,
    NonOverlappedFollowedBy = 14,
}

impl AssertionBinaryOp {
    /// The number of variants (15).
    pub const COUNT: i32 = 15;
    /// Every variant, in pinned-discriminant order.
    pub const ALL: [AssertionBinaryOp; Self::COUNT as usize] = [
        AssertionBinaryOp::And,
        AssertionBinaryOp::Or,
        AssertionBinaryOp::Intersect,
        AssertionBinaryOp::Throughout,
        AssertionBinaryOp::Within,
        AssertionBinaryOp::Iff,
        AssertionBinaryOp::Until,
        AssertionBinaryOp::SUntil,
        AssertionBinaryOp::UntilWith,
        AssertionBinaryOp::SUntilWith,
        AssertionBinaryOp::Implies,
        AssertionBinaryOp::OverlappedImplication,
        AssertionBinaryOp::NonOverlappedImplication,
        AssertionBinaryOp::OverlappedFollowedBy,
        AssertionBinaryOp::NonOverlappedFollowedBy,
    ];
}

impl TryFrom<i32> for AssertionBinaryOp {
    type Error = LoweringError;

    fn try_from(raw: i32) -> Result<Self, Self::Error> {
        match raw {
            0 => Ok(AssertionBinaryOp::And),
            1 => Ok(AssertionBinaryOp::Or),
            2 => Ok(AssertionBinaryOp::Intersect),
            3 => Ok(AssertionBinaryOp::Throughout),
            4 => Ok(AssertionBinaryOp::Within),
            5 => Ok(AssertionBinaryOp::Iff),
            6 => Ok(AssertionBinaryOp::Until),
            7 => Ok(AssertionBinaryOp::SUntil),
            8 => Ok(AssertionBinaryOp::UntilWith),
            9 => Ok(AssertionBinaryOp::SUntilWith),
            10 => Ok(AssertionBinaryOp::Implies),
            11 => Ok(AssertionBinaryOp::OverlappedImplication),
            12 => Ok(AssertionBinaryOp::NonOverlappedImplication),
            13 => Ok(AssertionBinaryOp::OverlappedFollowedBy),
            14 => Ok(AssertionBinaryOp::NonOverlappedFollowedBy),
            other => Err(LoweringError::unsupported(
                &format!(
                    "BinaryAssertionOperator raw value {other} is out of the pinned 0..=14 \
                     range (And..NonOverlappedFollowedBy) -- either a malformed raw \
                     discriminant or a slang upgrade that added a variant this mirror does not \
                     yet know about"
                ),
                "sva::op::AssertionBinaryOp::try_from",
            )),
        }
    }
}

/// The operator of one [`AssertionExprKind::Unary`]/`Binary` node, resolved
/// from `AssertionExpr::op()`'s raw discriminant against the node's own
/// `kind()` -- the disambiguation plan §1.1 calls for ("disambiguated here
/// by `AssertionExprKind` since Unary/Binary are the only kinds `op()` is
/// valid for").
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Op {
    Unary(AssertionUnaryOp),
    Binary(AssertionBinaryOp),
}

impl Op {
    /// Resolves `expr.op()` against `expr.kind()`. `scope` is only used to
    /// name the error's location (16.12/16.9's own worked sites all have a
    /// containing symbol in hand already, same as every other decoder in
    /// this file).
    pub fn of(expr: AssertionExpr, scope: &Symbol) -> Result<Op, LoweringError> {
        match expr.kind() {
            AssertionExprKind::Unary => {
                let raw = expr.op().ok_or_else(|| {
                    LoweringError::unsupported_at(
                        "AssertionExprKind::Unary node has no operator (`AssertionExpr::op()` \
                         returned None) -- this is a slang invariant violation, not a legal \
                         shape",
                        scope,
                    )
                })?;
                AssertionUnaryOp::try_from(raw).map(Op::Unary)
            }
            AssertionExprKind::Binary => {
                let raw = expr.op().ok_or_else(|| {
                    LoweringError::unsupported_at(
                        "AssertionExprKind::Binary node has no operator (`AssertionExpr::op()` \
                         returned None) -- this is a slang invariant violation, not a legal \
                         shape",
                        scope,
                    )
                })?;
                AssertionBinaryOp::try_from(raw).map(Op::Binary)
            }
            other => Err(LoweringError::unsupported_at(
                &format!(
                    "AssertionExprKind::{other:?} never carries an operator -- \
                     `AssertionExpr::op()` is only valid for Unary/Binary (see its own doc \
                     comment)"
                ),
                scope,
            )),
        }
    }
}

/// [`abort_children`]'s result: `AbortAssertionExpr`'s `[condition, body]`
/// (16.12.14's `accept_on`/`reject_on`/`sync_accept_on`/`sync_reject_on`).
/// `condition` is kept as a generic [`SemNode`] (it is a plain Boolean
/// `Expression` per the C++ class, but this module's job is only to label
/// positions, not to narrow types the caller -- T5's leaf compiler, T25's
/// abort lowering -- will cast as needed).
#[derive(Debug, Clone, Copy)]
pub struct AbortChildren<'d> {
    pub condition: SemNode<'d>,
    pub body: AssertionExpr<'d>,
}

/// Recovers `expr`'s `[condition, body]` children (`AssertionExprKind::Abort`
/// only). A named [`LoweringError`], never a panic, if `expr` is not an
/// `Abort` node, or if its child shape ever stops being exactly 2 (a future
/// slang reorder).
pub fn abort_children<'d>(
    expr: AssertionExpr<'d>,
    scope: &Symbol,
) -> Result<AbortChildren<'d>, LoweringError> {
    if expr.kind() != AssertionExprKind::Abort {
        return Err(LoweringError::unsupported_at(
            &format!(
                "abort_children: expected AssertionExprKind::Abort, found {:?}",
                expr.kind()
            ),
            scope,
        ));
    }
    let kids = expr.children();
    let [condition, body] = kids.as_slice() else {
        return Err(LoweringError::unsupported_at(
            &format!(
                "abort_children: expected exactly 2 children [condition, body], found {}",
                kids.len()
            ),
            scope,
        ));
    };
    let body = body.as_assertion_expr().ok_or_else(|| {
        LoweringError::unsupported_at(
            "abort_children: second child (body) is not an AssertionExpr",
            scope,
        )
    })?;
    Ok(AbortChildren {
        condition: *condition,
        body,
    })
}

/// Recovers a `disable iff (condition) body` node's `[condition, body]`
/// children (`AssertionExprKind::DisableIff` only; 16.12's top-level reset).
/// Same shape as [`AbortChildren`], and the same named [`LoweringError`]s.
pub fn disable_iff_children<'d>(
    expr: AssertionExpr<'d>,
    scope: &Symbol,
) -> Result<AbortChildren<'d>, LoweringError> {
    if expr.kind() != AssertionExprKind::DisableIff {
        return Err(LoweringError::unsupported_at(
            &format!(
                "disable_iff_children: expected AssertionExprKind::DisableIff, found {:?}",
                expr.kind()
            ),
            scope,
        ));
    }
    let kids = expr.children();
    let [condition, body] = kids.as_slice() else {
        return Err(LoweringError::unsupported_at(
            &format!(
                "disable_iff_children: expected exactly 2 children [condition, body], found {}",
                kids.len()
            ),
            scope,
        ));
    };
    let body = body.as_assertion_expr().ok_or_else(|| {
        LoweringError::unsupported_at(
            "disable_iff_children: second child (body) is not an AssertionExpr",
            scope,
        )
    })?;
    Ok(AbortChildren {
        condition: *condition,
        body,
    })
}

/// [`clocking_children`]'s result: `ClockingAssertionExpr`'s `[event, body]`
/// (16.5.2/16.13's `@(...)`-prefixed sequence/property). `event` is kept as
/// a generic [`SemNode`] (it is a `TimingControl` per the C++ class, not an
/// `AssertionExpr`; T7's clock-flow layer is the one that interprets it).
#[derive(Debug, Clone, Copy)]
pub struct ClockingChildren<'d> {
    pub event: SemNode<'d>,
    pub body: AssertionExpr<'d>,
}

/// Recovers `expr`'s `[event, body]` children (`AssertionExprKind::Clocking`
/// only). A named [`LoweringError`], never a panic, if `expr` is not a
/// `Clocking` node, or if its child shape ever stops being exactly 2.
pub fn clocking_children<'d>(
    expr: AssertionExpr<'d>,
    scope: &Symbol,
) -> Result<ClockingChildren<'d>, LoweringError> {
    if expr.kind() != AssertionExprKind::Clocking {
        return Err(LoweringError::unsupported_at(
            &format!(
                "clocking_children: expected AssertionExprKind::Clocking, found {:?}",
                expr.kind()
            ),
            scope,
        ));
    }
    let kids = expr.children();
    let [event, body] = kids.as_slice() else {
        return Err(LoweringError::unsupported_at(
            &format!(
                "clocking_children: expected exactly 2 children [event, body], found {}",
                kids.len()
            ),
            scope,
        ));
    };
    let body = body.as_assertion_expr().ok_or_else(|| {
        LoweringError::unsupported_at(
            "clocking_children: second child (body) is not an AssertionExpr",
            scope,
        )
    })?;
    Ok(ClockingChildren {
        event: *event,
        body,
    })
}

/// One non-default `case`/`endcase` item (16.12.16, Syntax 16-17): the
/// comma-separated label expressions that select it, and the property
/// expression that applies when one matches.
#[derive(Debug, Clone)]
pub struct CaseItemChildren<'d> {
    pub labels: Vec<SemNode<'d>>,
    pub body: AssertionExpr<'d>,
}

/// [`case_children`]'s result: the controlling `selector`, every non-default
/// item in source order, and the optional `default` body.
#[derive(Debug, Clone)]
pub struct CaseChildren<'d> {
    pub selector: SemNode<'d>,
    pub items: Vec<CaseItemChildren<'d>>,
    pub default: Option<AssertionExpr<'d>>,
}

/// Takes the next element of `kids` at `*idx`, advancing it -- the shared
/// bounds-checked cursor [`case_children`]'s selector/label/body/default
/// decoding steps all go through, so a too-short children list (a future
/// slang reorder) is always a named [`LoweringError`], never an out-of-
/// bounds panic.
fn next_child<'d>(
    kids: &[SemNode<'d>],
    idx: &mut usize,
    scope: &Symbol,
) -> Result<SemNode<'d>, LoweringError> {
    let node = kids.get(*idx).copied().ok_or_else(|| {
        LoweringError::unsupported_at(
            &format!(
                "case_children: ran out of semantic children at index {idx} (only {} present)",
                kids.len()
            ),
            scope,
        )
    })?;
    *idx += 1;
    Ok(node)
}

/// Recovers `expr`'s selector/items/default (`AssertionExprKind::Case`
/// only), per the module doc comment's `CaseAssertionExpr::visitExprs`
/// transcription: `[selector, item_0.labels..., item_0.body, ...,
/// default_body?]`. Each item's label count is read from the *syntax* tree
/// (`CasePropertyExprSyntax::items()`), not assumed, so this decodes any
/// number of items with any number of labels each -- not a decoder
/// hardcoded to one shape. A named [`LoweringError`], never a panic, for
/// any mismatch between the syntax-derived item/label counts and the
/// flattened semantic children list (a future slang reorder).
pub fn case_children<'d>(
    expr: AssertionExpr<'d>,
    tree: Trees<'_>,
    scope: &Symbol,
) -> Result<CaseChildren<'d>, LoweringError> {
    if expr.kind() != AssertionExprKind::Case {
        return Err(LoweringError::unsupported_at(
            &format!(
                "case_children: expected AssertionExprKind::Case, found {:?}",
                expr.kind()
            ),
            scope,
        ));
    }
    let syn = tree.syntax(&expr).ok_or_else(|| {
        LoweringError::unsupported_at(
            "case_children: Case assertion expression has no syntax node in the given tree",
            scope,
        )
    })?;
    let syn = peel_property_parens(syn);
    let case_syn = CasePropertyExprSyntax::cast(syn).ok_or_else(|| {
        LoweringError::unsupported_at(
            &format!(
                "case_children: expected CasePropertyExprSyntax syntax, found {:?}",
                syn.kind()
            ),
            scope,
        )
    })?;

    // Per-item label counts, and whether a default item is present, read
    // from the syntax tree's own grouping (the semantic `children()` list
    // below has no grouping at all -- it is one flat `Vec<SemNode>`).
    let mut label_counts = Vec::new();
    let mut has_default = false;
    for item in case_syn.items() {
        match item {
            PropertyCaseItemSyntax::StandardPropertyCaseItem(s) => {
                label_counts.push(s.expressions().iter().count());
            }
            PropertyCaseItemSyntax::DefaultPropertyCaseItem(_) => {
                has_default = true;
            }
        }
    }

    let kids = expr.children();
    let mut idx = 0usize;

    let selector = next_child(&kids, &mut idx, scope)?;

    let mut items = Vec::with_capacity(label_counts.len());
    for count in &label_counts {
        let mut labels = Vec::with_capacity(*count);
        for _ in 0..*count {
            labels.push(next_child(&kids, &mut idx, scope)?);
        }
        let body_node = next_child(&kids, &mut idx, scope)?;
        let body = body_node.as_assertion_expr().ok_or_else(|| {
            LoweringError::unsupported_at(
                "case_children: an item body child is not an AssertionExpr",
                scope,
            )
        })?;
        items.push(CaseItemChildren { labels, body });
    }

    let default = if has_default {
        let body_node = next_child(&kids, &mut idx, scope)?;
        let body = body_node.as_assertion_expr().ok_or_else(|| {
            LoweringError::unsupported_at(
                "case_children: the default item's body child is not an AssertionExpr",
                scope,
            )
        })?;
        Some(body)
    } else {
        None
    };

    if idx != kids.len() {
        return Err(LoweringError::unsupported_at(
            &format!(
                "case_children: {} semantic children left over after decoding selector + {} \
                 item(s) + default ({}); expected exactly {idx}, found {}",
                kids.len() - idx,
                label_counts.len(),
                has_default,
                kids.len()
            ),
            scope,
        ));
    }

    Ok(CaseChildren {
        selector,
        items,
        default,
    })
}

#[cfg(test)]
mod tests {
    use super::*;
    use sv_lang::{AnalysisFlags, Compilation, Session, SyntaxTree};

    /// Compiles `property_body` as a clocked `assert property` inside an
    /// `always_ff`, same shape as [`super::super::ranges::tests::compiled_root_body`]
    /// (that module's own test scaffolding), returning the full `(design,
    /// src)` so callers can pull whatever assertion-tree node they need.
    fn compiled(extra_decls: &str, property_body: &str) -> (sv_lang::Design, String) {
        let src = format!(
            "module m;\n\
             {extra_decls}\n\
             logic clk, a, b, c, rst;\n\
             always_ff @(posedge clk) begin\n\
               assert property (@(posedge clk) {property_body});\n\
             end\n\
             endmodule\n"
        );
        let session = Session::new();
        let mut comp = Compilation::new(&session).unwrap();
        comp.add_source(&src).unwrap();
        let design = comp.compile().unwrap();
        assert!(
            !design.has_fatal_errors(),
            "fixture failed to compile: {src}"
        );
        (design, src)
    }

    /// Compiles `property_body`, finds its one concurrent assertion, and
    /// hands the `Clocking` node itself (not yet stripped -- some tests
    /// need the wrapper, `clocking_children_are_event_then_body` chief among
    /// them) and the containing scope `Symbol` to `f`, all while the
    /// `Analysis` they borrow from is still alive.
    ///
    /// `f`'s own return type (`R`) is required (by this signature's
    /// implicit higher-ranked lifetime on the `Fn` bound's `AssertionExpr<'_>`/
    /// `Symbol<'_>` parameters) to not itself borrow from that `Analysis` --
    /// every test below returns only owned `bool`/`()` conclusions already
    /// checked inside the closure, never the borrowed node itself, which is
    /// exactly the discipline [`super::super::ranges::tests::ranges_of_property`]
    /// (this same crate's T3 test scaffolding) independently arrived at for
    /// the identical reason: `AnalyzedAssertion`'s lifetime parameter is
    /// tied to the `Analysis` borrow, not to `Design`, so it cannot outlive
    /// a helper function that builds and drops its own local `Analysis`.
    fn with_clocking_root<R>(
        extra_decls: &str,
        property_body: &str,
        f: impl FnOnce(AssertionExpr<'_>, Symbol<'_>) -> R,
    ) -> R {
        let (design, _src) = compiled(extra_decls, property_body);
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
        let proc = analysis.procedures(body).next().unwrap();
        let assertion = analysis.assertions(proc.symbol()).next().unwrap();
        let root = assertion.root().as_assertion_expr().unwrap();
        assert_eq!(root.kind(), AssertionExprKind::Clocking);
        f(root, body)
    }

    /// Like [`with_clocking_root`], but also strips the `Clocking` wrapper
    /// down to its `[1]` (body) child -- the actual operator under test for
    /// every fixture that isn't itself testing [`clocking_children`].
    fn with_property_root<R>(
        extra_decls: &str,
        property_body: &str,
        f: impl FnOnce(AssertionExpr<'_>, Symbol<'_>) -> R,
    ) -> R {
        with_clocking_root(extra_decls, property_body, |clocking, body| {
            let root = clocking.children()[1].as_assertion_expr().unwrap();
            f(root, body)
        })
    }

    /// Like [`with_property_root`], but also hands in the fixture's one
    /// [`SyntaxTree`] -- needed only by [`case_children`] (and this file's
    /// tests of it), since it is the one decoder here that falls back to
    /// syntax (module doc comment).
    fn with_property_root_and_tree<R>(
        extra_decls: &str,
        property_body: &str,
        f: impl FnOnce(AssertionExpr<'_>, &SyntaxTree, Symbol<'_>) -> R,
    ) -> R {
        let (design, _src) = compiled(extra_decls, property_body);
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
        let proc = analysis.procedures(body).next().unwrap();
        let assertion = analysis.assertions(proc.symbol()).next().unwrap();
        let clocking = assertion.root().as_assertion_expr().unwrap();
        assert_eq!(clocking.kind(), AssertionExprKind::Clocking);
        let root = clocking.children()[1].as_assertion_expr().unwrap();
        let tree = design.syntax_trees().into_iter().next().unwrap();
        f(root, &tree, body)
    }

    #[test]
    fn op_try_from_matches_every_pinned_cpp_value() {
        let expected_unary = [
            (0, AssertionUnaryOp::Not),
            (1, AssertionUnaryOp::NextTime),
            (2, AssertionUnaryOp::SNextTime),
            (3, AssertionUnaryOp::Always),
            (4, AssertionUnaryOp::SAlways),
            (5, AssertionUnaryOp::Eventually),
            (6, AssertionUnaryOp::SEventually),
        ];
        assert_eq!(expected_unary.len(), AssertionUnaryOp::COUNT as usize);
        for (raw, want) in expected_unary {
            assert_eq!(AssertionUnaryOp::try_from(raw).unwrap(), want);
        }
        assert_eq!(
            AssertionUnaryOp::ALL.to_vec(),
            expected_unary.iter().map(|(_, v)| *v).collect::<Vec<_>>()
        );

        let expected_binary = [
            (0, AssertionBinaryOp::And),
            (1, AssertionBinaryOp::Or),
            (2, AssertionBinaryOp::Intersect),
            (3, AssertionBinaryOp::Throughout),
            (4, AssertionBinaryOp::Within),
            (5, AssertionBinaryOp::Iff),
            (6, AssertionBinaryOp::Until),
            (7, AssertionBinaryOp::SUntil),
            (8, AssertionBinaryOp::UntilWith),
            (9, AssertionBinaryOp::SUntilWith),
            (10, AssertionBinaryOp::Implies),
            (11, AssertionBinaryOp::OverlappedImplication),
            (12, AssertionBinaryOp::NonOverlappedImplication),
            (13, AssertionBinaryOp::OverlappedFollowedBy),
            (14, AssertionBinaryOp::NonOverlappedFollowedBy),
        ];
        assert_eq!(expected_binary.len(), AssertionBinaryOp::COUNT as usize);
        for (raw, want) in expected_binary {
            assert_eq!(AssertionBinaryOp::try_from(raw).unwrap(), want);
        }
        assert_eq!(
            AssertionBinaryOp::ALL.to_vec(),
            expected_binary.iter().map(|(_, v)| *v).collect::<Vec<_>>()
        );

        // 7 + 15 = 22, per the plan's own count.
        assert_eq!(
            AssertionUnaryOp::COUNT + AssertionBinaryOp::COUNT,
            22,
            "plan §1.1 pins this at 22 variants total"
        );
    }

    #[test]
    fn op_try_from_rejects_out_of_range() {
        for raw in [-1, i32::MIN, 7, 100] {
            assert!(
                AssertionUnaryOp::try_from(raw).is_err(),
                "raw {raw} must be rejected, not panic or silently coerce"
            );
        }
        for raw in [-1, i32::MIN, 15, 100] {
            assert!(
                AssertionBinaryOp::try_from(raw).is_err(),
                "raw {raw} must be rejected, not panic or silently coerce"
            );
        }
    }

    #[test]
    fn op_of_resolves_unary_and_binary_and_rejects_other_kinds() {
        with_property_root("", "not a", |root, body| {
            assert_eq!(root.kind(), AssertionExprKind::Unary);
            assert_eq!(
                Op::of(root, &body).unwrap(),
                Op::Unary(AssertionUnaryOp::Not)
            );
        });

        with_property_root("", "a and b", |root, body| {
            assert_eq!(root.kind(), AssertionExprKind::Binary);
            assert_eq!(
                Op::of(root, &body).unwrap(),
                Op::Binary(AssertionBinaryOp::And)
            );
        });

        // `Simple` never carries an operator -- Op::of must reject it, not
        // panic trying to unwrap a `None` from `expr.op()`.
        with_property_root("", "a", |root, body| {
            assert_eq!(root.kind(), AssertionExprKind::Simple);
            let err = Op::of(root, &body).expect_err("Simple has no operator");
            assert!(err.message.contains("Simple"), "error was: {err}");
        });
    }

    #[test]
    fn abort_children_are_condition_then_body() {
        with_property_root("", "accept_on (rst) a", |root, body| {
            assert_eq!(root.kind(), AssertionExprKind::Abort);
            let decoded = abort_children(root, &body).unwrap();
            assert_eq!(decoded.body.kind(), AssertionExprKind::Simple);
        });
    }

    #[test]
    fn abort_children_rejects_non_abort_kind() {
        with_property_root("", "a", |root, body| {
            let err = abort_children(root, &body).expect_err("Simple is not Abort");
            assert!(err.message.contains("Abort"), "error was: {err}");
        });
    }

    #[test]
    fn clocking_children_are_event_then_body() {
        with_clocking_root("", "a", |clocking, body| {
            let decoded = clocking_children(clocking, &body).unwrap();
            assert_eq!(decoded.body.kind(), AssertionExprKind::Simple);
        });
    }

    #[test]
    fn clocking_children_rejects_non_clocking_kind() {
        with_property_root("", "a", |root, body| {
            let err = clocking_children(root, &body).expect_err("Simple is not Clocking");
            assert!(err.message.contains("Clocking"), "error was: {err}");
        });
    }

    #[test]
    fn case_children_decode_selector_items_default() {
        // Two items (the first with 2 labels, proving label counts are read
        // per item, not hardcoded to 1) plus a default.
        with_property_root_and_tree(
            "parameter int sel = 0;",
            "case (sel) 0, 1 : a; 2 : b; default : c; endcase",
            |root, tree, body| {
                assert_eq!(root.kind(), AssertionExprKind::Case);
                let decoded = case_children(root, tree.into(), &body).unwrap();
                assert_eq!(decoded.items.len(), 2, "two non-default items");
                assert_eq!(decoded.items[0].labels.len(), 2, "first item has 2 labels");
                assert_eq!(decoded.items[1].labels.len(), 1, "second item has 1 label");
                assert_eq!(decoded.items[0].body.kind(), AssertionExprKind::Simple);
                assert_eq!(decoded.items[1].body.kind(), AssertionExprKind::Simple);
                assert!(decoded.default.is_some(), "default item recovered");
                assert_eq!(decoded.default.unwrap().kind(), AssertionExprKind::Simple);
            },
        );
    }

    #[test]
    fn case_children_decode_with_no_default() {
        with_property_root_and_tree(
            "parameter int sel = 0;",
            "case (sel) 0 : a; 1 : b; endcase",
            |root, tree, body| {
                let decoded = case_children(root, tree.into(), &body).unwrap();
                assert_eq!(decoded.items.len(), 2);
                assert!(decoded.default.is_none(), "no default item in this fixture");
            },
        );
    }

    #[test]
    fn case_children_rejects_non_case_kind() {
        with_property_root_and_tree("", "a", |root, tree, body| {
            let err = case_children(root, tree.into(), &body).expect_err("Simple is not Case");
            assert!(err.message.contains("Case"), "error was: {err}");
        });
    }
}