vj-sim 0.3.0

//! Task 14 — Multi-driver resolution: strength lattice, K+1 slots,
//! force/release (ledger ST-034, ST-055, ST-146).
//!
//! **Scope note (from the plan):** `DriverSet`/`combine_bit`/
//! `resolve_net_step` are exercised exclusively against hand-built
//! `DriverSet` fixtures — wiring a `DriverSet` to a *real* elaborated net's
//! actual driver count/`NetKind` needs an `sv_lang` accessor the pinned
//! `sv-lang=0.1.9` C API does not expose (see `state::mod`'s `NetLayout` doc
//! comment); that connection is deferred, not this task's job. What this
//! task delivers, and what ST-034/ST-055/ST-146's literal acceptance text
//! asks for: the resolution logic itself lives in this crate (ST-034),
//! `force`/`release` are real (ST-055), and the `AliasedSingleDriver`
//! -materialization decision is made and documented (ST-146).
//!
//! **Deviations from the plan's literal text (documented once here, applying
//! to everything below — all binding per this task's own unresolved-review-
//! findings list):**
//!
//! 1. **`force_driver`/`release_driver` both take an added `set: &mut
//!    DriverSet` parameter**, not in the plan's literal signatures. The
//!    plan's own test for these two functions
//!    (`force_overrides_a_strong_wire_driver_release_restores_prior_value`)
//!    requires a subsequent `resolve_net_step(engine, &set, ..)` call, on
//!    the *same, caller-held* `DriverSet`, to observe the forced entry's
//!    presence/absence — structurally impossible if `force_driver`/
//!    `release_driver` cannot reach the caller's `DriverSet` at all (no
//!    `StateCellId -> DriverSet` registry exists anywhere in this plan; the
//!    Scope note above is explicit that `DriverSet` is exclusively
//!    caller-owned/hand-built this wave). `resolve_net_step` itself keeps
//!    its plan-pinned `set: &DriverSet` (it never mutates the driver list,
//!    only reads it and writes `set.resolved`'s own cell).
//! 2. **`ST-146`'s documented decision below is phrased as STATE's own
//!    proposed default, not a bilaterally closed joint decision.** ST-146's
//!    literal acceptance text requires "a written decision... agreed by both
//!    STATE and CODEGEN owners" before CODEGEN's kernel-net-read lowering is
//!    implemented; no CODEGEN track exists this wave to actually agree, so a
//!    unilateral STATE decision cannot fully satisfy that acceptance text by
//!    itself. This task still makes the decision (materialize always,
//!    matching state.md's already-designed default) and documents it in
//!    full, exactly as the plan describes — but frames it explicitly as a
//!    proposal pending CODEGEN concurrence, the same posture ST-028 and the
//!    `NetKind` gap above are already given, rather than asserting the
//!    joint-decision row is fully closed by one side alone.
//! 3. **`combine_bit` receives contributions as already Z-filtered-eligible
//!    `(Bit4, DriveStrength)` pairs** (the per-contributor
//!    `DriveStrengthPair -> DriveStrength` reduction the plan's prose
//!    describes as part of `combine_bit`'s own algorithm is actually
//!    performed by `resolve_net_step`, which is the only place that has
//!    both a contributor's pair *and* its currently-driven bit in scope at
//!    once); `combine_bit` itself still does the Z-drop, matching its own
//!    pinned signature `&[(Bit4, DriveStrength)]` (not `&[(Bit4,
//!    DriveStrengthPair)]`) literally.
//! 4. **A local `pack_bits4` helper, not `state::value::bits_to_four_state`.**
//!    `bits_to_four_state` packs `&[sv_lang::Bit]`; `combine_bit`'s own
//!    output is already `Bit4` (the ABI-level type, not `sv_lang::Bit`, and
//!    this file does not otherwise need an `sv_lang` dependency). `pack_bits4`
//!    below still goes through `Bit4::to_val_unk`/`to_aval_bval` exactly as
//!    `bits_to_four_state` does (ST-148's "one table" discipline) — it only
//!    skips the unnecessary `sv_lang::Bit` round-trip.
//! 5. **`state::value::four_state_bit_at` widened to `pub(crate)`** (edit to
//!    `value.rs`, not in this task's Files list): the same ST-148 "reuse the
//!    one table" discipline applied to the read direction — this file's
//!    per-bit extraction reuses that exact function rather than a second,
//!    parallel copy of its `Bit4::from_val_unk`/`from_aval_bval` logic.
//! 6. **`StateEngine` gains a `trireg_charge: HashMap<StateCellId,
//!    TriregCharge>` field** (edit to `instance.rs`, not in this task's
//!    Files list): the plan's own prose places `TriregCharge` "in
//!    `StateEngine`'s own `HashMap<StateCellId, TriregCharge>` side table" —
//!    a direct field is the only place for that table to live, per ST-152's
//!    "every resource STATE owns is a direct field" discipline this crate
//!    already applies to every other field of `StateEngine`.
//! 7. **(r2, blocking review finding 3) `wand`/`triand`/`wor`/`trior`
//!    resolution ignores drive strength entirely** (r1's own fix, made
//!    explicit and reconciled with state.md §4 step 3 here — the doc file
//!    itself is updated to match): matches real LRM/iverilog behavior for the
//!    ordinary multi-driver case, but it means a `force`d entry can no longer
//!    rely on its `Supply` strength alone to win outright on these four net
//!    kinds (a `Supply`-strength contributor is just one more live driver in
//!    the wired-AND/OR fold, and can be outvoted). `DriverEntry` therefore
//!    gains an explicit `forced: bool` tag, and `resolve_net_step`
//!    short-circuits to a forced entry's own value before running
//!    `combine_bit`'s fold at all, on every net kind — see `DriverEntry`'s
//!    and `resolve_net_step`'s own doc comments.
//! 8. **(r2, blocking review finding 1) `Tri0`/`Tri1`'s implicit resistive
//!    pull, previously entirely omitted:** `combine_bit` now injects it as a
//!    `Pull`-strength live contributor whenever `net_kind` is `Tri0`/`Tri1` —
//!    see `combine_bit`'s own doc comment for the full LRM/iverilog argument.
//! 9. **(r2, blocking review finding 2) `force_driver`'s Wide/Memory-class
//!    contribution cell no longer grows the ordinary wide plane
//!    (`Arena::alloc_wide_words`), which panics once `sv_get_wide` has sealed
//!    it:** it now grows a separate, never-sealed force-only plane pair
//!    (`Arena::alloc_force_wide_words`, `SlotClass::ForceWide`) that no
//!    accessor-ABI function ever exposes a raw pointer into, so it can never
//!    dangle an already-issued `WideView` regardless of seal state — see
//!    `SlotClass::ForceWide`'s and `Arena::alloc_force_wide_words`'s own doc
//!    comments. `mod.rs`, `arena.rs`, `write.rs`, `dedup.rs`, `instance.rs`,
//!    and `accessor_impl.rs` all needed a mechanical new match arm for the
//!    added `SlotClass` variant (none of them in this task's Files list).
//! 10. **(Task 15 retrofit, binding per Task 15's own unresolved-review-
//!     findings list) `force_driver`/`release_driver` each call
//!     `StateEngine::notify_force_observed`** after doing their own work —
//!     `force_driver` with `net` (already asserted `== set.resolved`),
//!     `release_driver` with `set.resolved` (read after the entry is removed
//!     and the net re-resolved, since `release_driver`'s own `forced`
//!     parameter names the *driver contribution* cell being removed, not the
//!     net). This file's own Files list (this task's header) names only
//!     `state/driver.rs` (new) and `state/mod.rs`; Task 15's plan text
//!     describes this exact retrofit ("`driver::force_driver`/`release_driver`
//!     (Task 14) each call every registered `ForceObserved` listener") without
//!     listing `driver.rs` under its own Files section — documented here, on
//!     the retrofitted side, per that task's own binding review finding.

use std::cmp::Ordering;

use vj_abi::{Bit4, SimTime};

use super::four_state_bit_at;
use super::instance::StateEngine;
use super::write::{ChangeResult, PreWriteHook, SlotLocation};
use super::{FourStateValue, NetKind, SignalAccess, SlotClass, StateCellId};

/// The 4-level drive-strength lattice (state.md §4 simplifies the LRM's
/// 8-level charge/drive split to these 4 for resolution purposes).
/// `Ord`/`PartialOrd` are hand-written, not derived: the plan pins
/// `Supply > Strong > Pull > Weak`, the *reverse* of this enum's own
/// declaration order (declaration order is what `#[derive(Ord)]` would use).
#[derive(Clone, Copy, PartialEq, Eq, Debug, serde::Serialize, serde::Deserialize)]
pub enum DriveStrength {
    Supply,
    Strong,
    Pull,
    Weak,
    /// `highz0`/`highz1` (LRM 28.3): the driver drives nothing for that
    /// value (it contributes `z`), the bottom of the lattice.
    HighZ,
}

impl DriveStrength {
    /// Higher rank == wins resolution. The one place this lattice's total
    /// order is defined; `Ord`/`PartialOrd` below and every comparison
    /// elsewhere in this file goes through this, never a second hand-rolled
    /// ordering.
    fn rank(self) -> u8 {
        match self {
            DriveStrength::HighZ => 0,
            DriveStrength::Weak => 1,
            DriveStrength::Pull => 2,
            DriveStrength::Strong => 3,
            DriveStrength::Supply => 4,
        }
    }
}

impl PartialOrd for DriveStrength {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        Some(self.cmp(other))
    }
}

impl Ord for DriveStrength {
    fn cmp(&self, other: &Self) -> Ordering {
        self.rank().cmp(&other.rank())
    }
}

/// A driver's own strength for each value it might drive (state.md §4):
/// `s0` applies when this driver is driving `0`, `s1` when driving `1`;
/// driving `X` reduces to `min(s0, s1)` (see [`effective_strength`]).
#[derive(Clone, Copy, PartialEq, Eq, Debug, serde::Serialize, serde::Deserialize)]
pub struct DriveStrengthPair {
    pub s0: DriveStrength,
    pub s1: DriveStrength,
}

impl DriveStrengthPair {
    /// The default drive strength: `(strong0, strong1)` (LRM 28.11).
    pub const STRONG: DriveStrengthPair = DriveStrengthPair {
        s0: DriveStrength::Strong,
        s1: DriveStrength::Strong,
    };
}

/// One driver's own private contribution slot plus its strength (ST-034):
/// `source` is a [`StateCellId`] this driver alone writes to (never shared
/// read-modify-write storage with any other driver or with `resolved`).
///
/// **Review fix (Task 14 r2, blocking finding 3) adds `forced`.** Before this
/// fix, [`force_driver`] modeled `force` purely via `Supply`/`Supply`
/// strength, relying on strength-grouping (the "every other kind" branch of
/// [`combine_bit`]) to make it win outright by being the sole top-strength
/// member. That assumption broke the moment r1 changed `wand`/`triand`/
/// `wor`/`trior` resolution to skip strength-grouping entirely (matching real
/// LRM/iverilog behavior for the *ordinary* multi-driver case) — on those net
/// kinds a `Supply`-strength forced entry is just one more live contributor
/// in the wired-AND/OR fold and can be outvoted. `forced` is an explicit,
/// net-kind-independent tag: [`resolve_net_step`] short-circuits to a forced
/// entry's own value directly (see its doc comment), the way `force`/
/// `release` (ST-055) are specified to override *every* other driver outright
/// regardless of net kind or strength. Ordinary drivers always set this
/// `false`; only [`force_driver`]'s own synthetic entry ever sets it `true`.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct DriverEntry {
    pub source: StateCellId,
    pub strength: DriveStrengthPair,
    pub forced: bool,
}

/// The **K+1 slots** design (ST-034): `resolved` is one more [`StateCellId`]
/// (`StateEngine::alloc_cell`) than the `K` entries in `drivers` — never a
/// single shared slot every driver writes through. Hand-built by every test
/// in this task (see this module's own top doc comment, Scope note).
#[derive(Clone, Debug)]
pub struct DriverSet {
    pub resolved: StateCellId,
    pub drivers: Vec<DriverEntry>,
    pub net_kind: NetKind,
}

/// The loud, typed rejection [`combine_bit`]/[`resolve_net_step`] return
/// instead of panicking or silently guessing a winner for a net kind this
/// fold cannot resolve (ARCHITECTURE §6.5's "hard-error, not silently
/// wrong" for `nettype...with`, applied to this crate's own `NetKind` enum
/// per ARCHITECTURE §7 item 9).
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DriverError {
    UnresolvableUserDefinedNetType,
}

/// `trireg`'s own charge-decay state (state.md §4/§6): stored in
/// `StateEngine`'s own side table (`instance.rs`'s `trireg_charge` field),
/// never as a normal [`DriverEntry`] — `trireg` decay *timing* itself is a
/// TIMING-subsystem hook this task only stores state for, not implemented
/// here.
#[derive(Clone, Debug)]
pub struct TriregCharge {
    pub last_value: FourStateValue,
    pub strength: ChargeStrength,
    pub last_drive_time: SimTime,
}

/// `trireg`'s charge-strength lattice — kept separate from [`DriveStrength`]
/// (state.md §4: `trireg` charge decay is not part of the ordinary K+1
/// drive-strength fold `combine_bit` performs).
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum ChargeStrength {
    Small,
    Medium,
    Large,
}

impl StateEngine {
    /// Task 14 (ST-034): read-only lookup into this engine's own
    /// `trireg_charge` side table.
    pub fn trireg_charge(&self, cell: StateCellId) -> Option<&TriregCharge> {
        self.trireg_charge.get(&cell)
    }

    /// Task 14 (ST-034): records/replaces `cell`'s stored charge state. No
    /// decay-timing behavior happens here or anywhere in this crate this
    /// wave — see [`TriregCharge`]'s own doc comment.
    pub fn set_trireg_charge(&mut self, cell: StateCellId, charge: TriregCharge) {
        self.trireg_charge.insert(cell, charge);
    }
}

/// Reduces one driver's [`DriveStrengthPair`] plus its currently-driven bit
/// to a single effective [`DriveStrength`] (state.md §4): driving `0` picks
/// `s0`, driving `1` picks `s1`, driving `X` picks `min(s0, s1)` (this task's
/// own pinned resolution of state.md's previously-open "driver outputting X"
/// question — a v1 default, not re-opened here). A `Z`-driving contributor's
/// strength is never actually consulted (`combine_bit` drops every `Z`
/// contributor before grouping by strength) — this arm exists only so the
/// function is total; its value is irrelevant by construction.
fn effective_strength(bit: Bit4, pair: DriveStrengthPair) -> DriveStrength {
    match bit {
        Bit4::Zero => pair.s0,
        Bit4::One => pair.s1,
        // An `x` from a `highz` side still drives at the other side's level.
        Bit4::X => match pair.s0.min(pair.s1) {
            DriveStrength::HighZ => pair.s0.max(pair.s1),
            weaker => weaker,
        },
        Bit4::Z => pair.s0,
    }
}

/// The per-bit combinator (state.md §4). `net_kind == NetKind::UserDefined`
/// returns `Err` immediately, regardless of `contributions` (even an empty
/// slice) — v1 has no `nettype...with` resolution-function plugin, so this
/// net kind can never be folded, not even trivially. Every other kind first
/// drops `Z`-valued contributors, then — **`Tri0`/`Tri1` only** (review fix,
/// Task 14 r2, blocking finding 1) — adds one *implicit* live contributor of
/// its own: the LRM-mandated resistive pull-to-0 (`tri0`) / pull-to-1
/// (`tri1`) at [`DriveStrength::Pull`], which always participates in
/// strength-grouping below alongside any real contributions, even when there
/// are none. This is what makes an undriven `tri0`/`tri1` net read `0`/`1`
/// (not `Z`, unlike every other net kind) and what makes an explicit `Weak`
/// driver lose to the implicit pull rather than winning outright — verified
/// empirically against iverilog 12 (`tri0 w;` alone reads `0`; `tri0 w;
/// assign (weak0,weak1) w=1;` still reads `0`). Zero remaining contributors
/// after that (every other kind, all-`Z`/`K==0`) ⇒ `Z` — an emergent fold
/// result, never a special case. From there two genuinely different
/// algorithms apply, per IEEE 1800 Table 28-8:
///
/// - **`wand`/`triand`/`wor`/`trior`** (wired-logic net types): drive
///   strength plays **no role** in resolution — every live (non-Z)
///   contributor, at *any* strength, participates directly in the
///   wired-AND/OR fold (`wand`/`triand`: `0` dominates, else `X` if any `X`,
///   else `1`; `wor`/`trior`: `1` dominates, else `X` if any `X`, else `0`).
///   Strength is never consulted for these four kinds, not even to pick a
///   subset of participants. (`Tri0`/`Tri1`'s implicit pull, above, never
///   applies here — it is not one of these four kinds.)
/// - **every other kind** (`wire`/`tri`-family — including `Tri0`/`Tri1`'s
///   own implicit-pull contributor above — `supply0`/`supply1`, `uwire`):
///   group live contributors by (already-reduced, see
///   [`effective_strength`]) strength, highest group wins; single winner or
///   multiple agreeing in that group ⇒ its value; multiple disagreeing ⇒
///   `X`.
///
/// Exhaustive over `NetKind`'s 13 variants, no wildcard arm (ARCHITECTURE §7
/// item 9) — enforced by
/// `combine_bit_and_resolve_net_step_reject_userdefined_net_kind_with_a_typed_error`
/// below, not only by this doc comment.
fn combine_bit(
    contributions: &[(Bit4, DriveStrength)],
    net_kind: NetKind,
) -> Result<Bit4, DriverError> {
    combine_bit_strength(contributions, net_kind).map(|(bit, _)| bit)
}

/// [`combine_bit`] plus the strength the result is driven at (LRM 28.12: the
/// strength of the winning group; `None` for a `z`). A resolution that ends
/// in `x` from disagreeing drivers keeps the strength of the group that
/// disagreed. The single fold both the value and the `%v` strength view use.
fn combine_bit_strength(
    contributions: &[(Bit4, DriveStrength)],
    net_kind: NetKind,
) -> Result<(Bit4, Option<DriveStrength>), DriverError> {
    if let NetKind::UserDefined = net_kind {
        return Err(DriverError::UnresolvableUserDefinedNetType);
    }

    let mut live: Vec<(Bit4, DriveStrength)> = contributions
        .iter()
        .copied()
        .filter(|(bit, s)| *bit != Bit4::Z && *s != DriveStrength::HighZ)
        .collect();

    // Review fix (Task 14 r2, blocking finding 1): Tri0/Tri1's implicit
    // resistive pull is injected here, unconditionally, *before* the
    // live-emptiness check below -- so it alone keeps an otherwise-undriven
    // tri0/tri1 net out of the `Z` fold result, and so it genuinely competes
    // in strength-grouping against any real (even Weak) contributors rather
    // than only being consulted when nothing else drives the net.
    match net_kind {
        NetKind::Tri0 => live.push((Bit4::Zero, DriveStrength::Pull)),
        NetKind::Tri1 => live.push((Bit4::One, DriveStrength::Pull)),
        _ => {}
    }

    if live.is_empty() {
        return Ok((Bit4::Z, None));
    }

    // Wired-logic net types: strength plays no role at all (IEEE 1800 Table
    // 28-8) — every live driver folds through the wired-AND/OR truth table
    // directly, never gated by a strength-grouping step first. This is a
    // *different* algorithm from the strength-gated fold below, not that
    // same fold merely restricted to a strength-selected subset.
    if matches!(
        net_kind,
        NetKind::WAnd | NetKind::TriAnd | NetKind::WOr | NetKind::TriOr
    ) {
        let is_and = matches!(net_kind, NetKind::WAnd | NetKind::TriAnd);
        let dominant = if is_and { Bit4::Zero } else { Bit4::One };
        let recessive = if is_and { Bit4::One } else { Bit4::Zero };
        let top = live.iter().map(|(_, s)| *s).max();
        return Ok((
            if live.iter().any(|(bit, _)| *bit == dominant) {
                dominant
            } else if live.iter().any(|(bit, _)| *bit == Bit4::X) {
                Bit4::X
            } else {
                recessive
            },
            top,
        ));
    }

    let max_strength = live
        .iter()
        .map(|(_, strength)| *strength)
        .max()
        .expect("live is non-empty, checked above");
    let winners: Vec<Bit4> = live
        .iter()
        .filter(|(_, strength)| *strength == max_strength)
        .map(|(bit, _)| *bit)
        .collect();

    let first = winners[0];
    if winners.iter().all(|bit| *bit == first) {
        return Ok((first, Some(max_strength)));
    }

    let x = match net_kind {
        NetKind::Wire
        | NetKind::Tri
        | NetKind::Tri0
        | NetKind::Tri1
        | NetKind::TriReg
        | NetKind::Supply0
        | NetKind::Supply1
        | NetKind::UWire => Bit4::X,
        NetKind::WAnd | NetKind::TriAnd | NetKind::WOr | NetKind::TriOr => {
            unreachable!("handled above, before strength grouping")
        }
        NetKind::UserDefined => unreachable!("returned Err above"),
    };
    Ok((x, Some(max_strength)))
}

/// Per-bit resolution of `values` like [`resolve_values`], keeping each
/// bit's strength (LRM 28.12; `None` for `z`) for `%v` (LRM 21.2.1.5).
/// Index 0 is bit 0. `supply0`/`supply1` nets are `Supply`.
pub fn resolve_strengths(
    values: &[(FourStateValue, DriveStrengthPair)],
    width: u32,
    net_kind: NetKind,
) -> Result<Vec<(Bit4, Option<DriveStrength>)>, DriverError> {
    (0..width)
        .map(|i| match net_kind {
            NetKind::Supply0 => Ok((Bit4::Zero, Some(DriveStrength::Supply))),
            NetKind::Supply1 => Ok((Bit4::One, Some(DriveStrength::Supply))),
            _ => {
                let contributions: Vec<(Bit4, DriveStrength)> = values
                    .iter()
                    .map(|(v, strength)| {
                        let bit = four_state_bit_at(v, i);
                        (bit, effective_strength(bit, *strength))
                    })
                    .collect();
                combine_bit_strength(&contributions, net_kind)
            }
        })
        .collect()
}

/// Packs already-resolved [`Bit4`]s into a [`FourStateValue`] shaped for
/// `class` (see this module's top doc comment, deviation 4, for why this is
/// a local helper rather than `state::value::bits_to_four_state`) — goes
/// through the exact same [`Bit4::to_val_unk`]/[`Bit4::to_aval_bval`] tables
/// that function uses, never a hand-rolled polarity (ST-148).
fn pack_bits4(class: SlotClass, elem_word_count: u32, bits: &[Bit4]) -> FourStateValue {
    match class {
        SlotClass::Inline => {
            let mut val: u64 = 0;
            let mut unk: u64 = 0;
            for (i, bit) in bits.iter().enumerate() {
                let (v, u) = bit.to_val_unk();
                if v {
                    val |= 1u64 << i;
                }
                if u {
                    unk |= 1u64 << i;
                }
            }
            FourStateValue::Narrow((val as u128) | ((unk as u128) << 64))
        }
        SlotClass::Wide | SlotClass::Memory => {
            let words = elem_word_count as usize;
            let mut aval = vec![0u64; words];
            let mut bval = vec![0u64; words];
            for (i, bit) in bits.iter().enumerate() {
                let (a, b) = bit.to_aval_bval();
                let word = i / 64;
                let lane = i % 64;
                if a {
                    aval[word] |= 1u64 << lane;
                }
                if b {
                    bval[word] |= 1u64 << lane;
                }
            }
            FourStateValue::Wide { aval, bval }
        }
        // `class` here is always `set.resolved`'s own class (this function's
        // only caller, `resolve_net_step`, passes `resolved_loc.class`); a
        // `resolved` cell is never itself `SlotClass::ForceWide` -- see
        // `force_driver`'s identically-justified `unreachable!` arm and
        // `SlotClass::ForceWide`'s own doc comment.
        SlotClass::ForceWide => {
            unreachable!("pack_bits4: set.resolved is never itself SlotClass::ForceWide")
        }
    }
}

/// Resolves one `width`-bit net of `net_kind` from its drivers' current
/// values and strengths (each full-width; a bit a driver does not drive is
/// `z`), per bit through [`combine_bit`]. A `supply0`/`supply1` net is its
/// constant unless a supply-strength driver disagrees (`x`). The result is shaped Narrow (up to 64 bits) or Wide.
pub fn resolve_values(
    values: &[(FourStateValue, DriveStrengthPair)],
    width: u32,
    net_kind: NetKind,
) -> Result<FourStateValue, DriverError> {
    let (class, words) = if width <= 64 {
        (SlotClass::Inline, 1)
    } else {
        (SlotClass::Wide, width.div_ceil(64))
    };
    let mut bits = Vec::with_capacity(width as usize);
    for i in 0..width {
        let mut contributions: Vec<(Bit4, DriveStrength)> = values
            .iter()
            .map(|(v, strength)| {
                let bit = four_state_bit_at(v, i);
                (bit, effective_strength(bit, *strength))
            })
            .collect();
        // A `supply0`/`supply1` net carries an implicit supply-strength
        // driver of its constant (LRM 6.6.1), so it is that constant unless
        // another driver is *also* supply-strength with the other value
        // (Table 28-9: the conflict resolves to `x`).
        if net_kind == NetKind::Supply0 {
            contributions.push((Bit4::Zero, DriveStrength::Supply));
        } else if net_kind == NetKind::Supply1 {
            contributions.push((Bit4::One, DriveStrength::Supply));
        }
        let bit = combine_bit(&contributions, net_kind)?;
        bits.push(bit);
    }
    Ok(pack_bits4(class, words, &bits))
}

/// Reads all `K` contribution cells via [`SignalAccess::read`], folds them
/// bit-by-bit through [`combine_bit`] (propagating the first `Err` out via
/// `?`, never partially committing some bits and rejecting others), and
/// `commit_write`s the result into `set.resolved` only on a fully-resolved
/// `Ok` — schedulable exactly like any other write (ARCHITECTURE §6.2: this
/// function is the pure function ENGINE later wraps as a synthetic
/// sensitivity-driven process, not the scheduling itself).
///
/// **Documented decision (ST-146, see this module's top doc comment,
/// deviation 2, for the joint-sign-off caveat):** always materializes the
/// resolved value into `set.resolved`, including for the trivial
/// single-driver (`K==1`) case — the simpler, already-designed default from
/// state.md, chosen over CODEGEN inlining a reader-side shortcut. This is
/// STATE's own proposed default for this wave, not yet bilaterally agreed
/// with CODEGEN (no CODEGEN track exists this wave to agree) — CODEGEN's own
/// kernel-net-read wave may revisit it.
///
/// **Review fix (Task 14 r2, blocking finding 3):** before running
/// [`combine_bit`]'s per-net-kind fold at all, checks whether any
/// [`DriverEntry`] in `set.drivers` is [`DriverEntry::forced`] and, if so,
/// short-circuits straight to that entry's own current value, verbatim —
/// `force`/`release` (ST-055) override *every* other driver outright on
/// *every* net kind, which the ordinary per-bit fold can no longer be relied
/// on to produce merely by giving the forced entry `Supply` strength (see
/// this module's top doc comment, deviation 7, and [`DriverEntry`]'s own doc
/// comment, for why that stopped being sufficient once `wand`/`wor` stopped
/// consulting strength at all). `NetKind::UserDefined` is still rejected
/// first, even when forced — `force`/`release` are only ever exercised on
/// ordinary, non-`UserDefined` nets in v1 (this module's top doc comment,
/// Scope note), so this ordering makes no observable difference for any
/// real caller, but keeps `resolve_net_step`'s `UnresolvableUserDefinedNetType`
/// guarantee unconditional rather than force-dependent. At most one forced
/// entry is expected at a time in v1 (`force_driver`'s own doc comment); if
/// more than one were ever present, the first in `set.drivers` order wins,
/// deterministically.
pub fn resolve_net_step(
    engine: &mut StateEngine,
    set: &DriverSet,
    hook: &mut dyn PreWriteHook,
) -> Result<ChangeResult, DriverError> {
    if let NetKind::UserDefined = set.net_kind {
        return Err(DriverError::UnresolvableUserDefinedNetType);
    }

    if let Some(forced_entry) = set.drivers.iter().find(|entry| entry.forced) {
        let forced_value = engine.read(forced_entry.source);
        return Ok(engine.commit_write(set.resolved, forced_value, hook));
    }

    let resolved_loc: SlotLocation = engine.cells[set.resolved.0 as usize];
    let width = resolved_loc.bit_width;

    let mut resolved_bits: Vec<Bit4> = Vec::with_capacity(width as usize);
    for i in 0..width {
        let contributions: Vec<(Bit4, DriveStrength)> = set
            .drivers
            .iter()
            .map(|entry| {
                let value = engine.read(entry.source);
                let bit = four_state_bit_at(&value, i);
                (bit, effective_strength(bit, entry.strength))
            })
            .collect();
        resolved_bits.push(combine_bit(&contributions, set.net_kind)?);
    }

    let new_value = pack_bits4(
        resolved_loc.class,
        resolved_loc.elem_word_count,
        &resolved_bits,
    );
    Ok(engine.commit_write(set.resolved, new_value, hook))
}

/// `force`/`release`/`deassign` (ST-055), modeled as a synthetic,
/// singleton-partition dynamic driver: allocates one more [`DriverEntry`]
/// (`Supply`-strength, so it always wins outright per the lattice above,
/// matching `force`'s LRM override semantics), seeds its private contribution
/// cell with `value`, pushes it onto `set.drivers`, and returns its
/// [`StateCellId`] so the caller can later [`release_driver`] it.
///
/// `net` must be `set`'s own `resolved` cell (this module's top doc comment,
/// deviation 1, explains why `set` itself must also be passed — `net` alone,
/// as the plan's literal signature had it, gives this function no way to
/// reach the caller's `DriverSet` at all). Checked with a real `assert_eq!`
/// (not `debug_assert_eq!`): this is a caller-contract precondition, not a
/// debug-only sanity check, and `net` would otherwise never be read by this
/// function's body at all.
pub fn force_driver(
    engine: &mut StateEngine,
    set: &mut DriverSet,
    net: StateCellId,
    value: FourStateValue,
) -> StateCellId {
    assert_eq!(
        net, set.resolved,
        "force_driver: `net` must be this DriverSet's own resolved cell"
    );

    let resolved_loc: SlotLocation = engine.cells[set.resolved.0 as usize];
    let source = match resolved_loc.class {
        SlotClass::Inline => {
            // SAFETY: `engine` is exclusively borrowed (`&mut StateEngine`)
            // for the duration of this call; no other live borrow of the
            // inline plane is held across this allocation, matching every
            // other caller of `Arena::alloc_inline_word` in this crate.
            let word_offset = unsafe { engine.arena.alloc_inline_word() };
            SlotLocation {
                class: SlotClass::Inline,
                word_offset,
                bit_width: resolved_loc.bit_width,
                elem_word_count: 1,
                row_stride_words: 0,
                num_rows: 0,
            }
        }
        SlotClass::Wide | SlotClass::Memory => {
            // Review fix (Task 14 r2, blocking finding 2): allocate from
            // `Arena`'s separate, never-sealed `force_wide_aval`/
            // `force_wide_bval` planes (`SlotClass::ForceWide`), not the
            // ordinary wide planes `alloc_wide_words` refuses to grow once
            // `sv_get_wide` has sealed them. `force`/`release` (ST-055) must
            // stay real, always-available runtime operations regardless of
            // whether any wide signal has already been read through the
            // accessor ABI — see `Arena::alloc_force_wide_words`'s doc
            // comment for the full argument.
            //
            // SAFETY: same single-logical-writer/single-borrow argument as
            // the `Inline` arm above, applied to the force-only wide planes.
            let word_offset = unsafe {
                engine
                    .arena
                    .alloc_force_wide_words(resolved_loc.elem_word_count)
            };
            SlotLocation {
                class: SlotClass::ForceWide,
                word_offset,
                bit_width: resolved_loc.bit_width,
                elem_word_count: resolved_loc.elem_word_count,
                row_stride_words: 0,
                num_rows: 0,
            }
        }
        // `set.resolved` is always a real net's resolved cell (this
        // function's own `assert_eq!` above); `SlotClass::ForceWide` is
        // minted only by this same match's `Wide | Memory` arm, for a
        // *contribution* cell, never for a `resolved` cell — see
        // `SlotClass::ForceWide`'s own doc comment.
        SlotClass::ForceWide => {
            unreachable!("force_driver: set.resolved is never itself SlotClass::ForceWide")
        }
    };
    let source = engine.alloc_cell(source);
    // Review fix (Task 16 r1, blocking finding 2): overwrite `alloc_cell`'s
    // conservative `CellReset::AllX` default for this synthetic contribution
    // cell -- mirroring `allocate_instance`'s own overwrite for its real
    // slots (`state::instance`) -- so `StateEngine::reset_to_initial` never
    // blits a reset value over a live `force` contribution. See
    // `CellReset::ForceContribution`'s own doc comment (`state::rollback`)
    // for the silent-corruption hazard this closes.
    engine.cell_reset[source.0 as usize] = super::rollback::CellReset::ForceContribution;
    engine.commit_write(source, value, &mut ());

    // Review fix (Task 14 r2, blocking finding 3): tag this synthetic entry
    // as `forced` (not merely `Supply`-strength) — see `DriverEntry::forced`'s
    // own doc comment and `resolve_net_step`'s doc comment for why the
    // strength alone is no longer sufficient to guarantee force wins
    // outright on every net kind.
    set.drivers.push(DriverEntry {
        source,
        strength: DriveStrengthPair {
            s0: DriveStrength::Supply,
            s1: DriveStrength::Supply,
        },
        forced: true,
    });

    // Task 15 retrofit (ST-122's external-write half, see this module's top
    // doc comment, deviation 10): `net` was already asserted `== set.resolved`
    // above, so this names exactly the net a future partitioning pass would
    // otherwise (wrongly) assume no external writer ever touches.
    engine.notify_force_observed(net);

    source
}

/// The other half of [`force_driver`]: removes `forced`'s one `DriverEntry`
/// from `set.drivers` and re-runs [`resolve_net_step`], unwrapping its `Ok`
/// — `force`/`release` are only ever exercised on ordinary, non-`UserDefined`
/// nets in v1 (this module's top doc comment, Scope note), so the `Err` arm
/// is unreachable from this function and it never wraps it further.
pub fn release_driver(engine: &mut StateEngine, set: &mut DriverSet, forced: StateCellId) {
    let before = set.drivers.len();
    set.drivers.retain(|entry| entry.source != forced);
    assert_eq!(
        set.drivers.len(),
        before - 1,
        "release_driver: `forced` must be the `StateCellId` of a `DriverEntry` \
         currently present in `set.drivers` (from a prior `force_driver` call on this same set)"
    );

    resolve_net_step(engine, set, &mut ()).expect(
        "release_driver: force/release only ever targets a non-UserDefined net in v1, \
         so resolve_net_step's Err arm is unreachable here",
    );

    // Task 15 retrofit (ST-122's external-write half, see this module's top
    // doc comment, deviation 10): `forced` above names the removed *driver
    // contribution* cell, not the net -- `set.resolved` is the actual net a
    // future partitioning pass would otherwise (wrongly) assume no external
    // writer ever touches.
    engine.notify_force_observed(set.resolved);
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::state::instance::TemplateRegistry;

    fn fresh_engine() -> StateEngine {
        StateEngine::new(TemplateRegistry::new())
    }

    /// Allocates a fresh, zero-initialized 1-bit inline cell — every driver
    /// contribution and every `resolved` cell in this task's tests is a
    /// scalar net.
    fn scalar_cell(engine: &mut StateEngine) -> StateCellId {
        // SAFETY: `engine` is a local, single-owned value with no other live
        // borrow of the inline plane, and every test here is single-threaded
        // with no concurrent allocation.
        let word_offset = unsafe { engine.arena.alloc_inline_word() };
        let loc = SlotLocation {
            class: SlotClass::Inline,
            word_offset,
            bit_width: 1,
            elem_word_count: 1,
            row_stride_words: 0,
            num_rows: 0,
        };
        engine.alloc_cell(loc)
    }

    /// A scalar cell pre-seeded (via a real `commit_write`) to drive `bit`.
    fn seeded_scalar_cell(engine: &mut StateEngine, bit: Bit4) -> StateCellId {
        let cell = scalar_cell(engine);
        let (v, u) = bit.to_val_unk();
        let word = (v as u128) | ((u as u128) << 64);
        engine.commit_write(cell, FourStateValue::Narrow(word), &mut ());
        cell
    }

    /// Reads bit 0 of `cell`'s currently-stored value back out as a `Bit4`.
    fn read_bit(engine: &StateEngine, cell: StateCellId) -> Bit4 {
        four_state_bit_at(&engine.read(cell), 0)
    }

    fn strong_pair() -> DriveStrengthPair {
        DriveStrengthPair {
            s0: DriveStrength::Strong,
            s1: DriveStrength::Strong,
        }
    }

    /// Allocates a fresh, zero-initialized 128-bit `SlotClass::Wide` cell
    /// (`bit_width > 64`, `elem_word_count == 2`) — the storage shape
    /// `force_driver`'s Wide/Memory branch (Task 14 r2, blocking review
    /// finding 2) exercises.
    fn wide_cell(engine: &mut StateEngine) -> StateCellId {
        // SAFETY: `engine` is a local, single-owned value with no other live
        // borrow of the wide plane, and every test here is single-threaded
        // with no concurrent allocation.
        let word_offset = unsafe { engine.arena.alloc_wide_words(2) };
        let loc = SlotLocation {
            class: SlotClass::Wide,
            word_offset,
            bit_width: 128,
            elem_word_count: 2,
            row_stride_words: 0,
            num_rows: 0,
        };
        engine.alloc_cell(loc)
    }

    /// A 128-bit `SlotClass::Wide` cell pre-seeded (via a real
    /// `commit_write`) with `aval0` as its low word's known-value bits (no
    /// unknown bits, high word zero).
    fn seeded_wide_cell(engine: &mut StateEngine, aval0: u64) -> StateCellId {
        let cell = wide_cell(engine);
        engine.commit_write(
            cell,
            FourStateValue::Wide {
                aval: vec![aval0, 0],
                bval: vec![0, 0],
            },
            &mut (),
        );
        cell
    }

    /// Reads a `SlotClass::Wide` cell's low `aval` word back out.
    fn read_wide_aval0(engine: &StateEngine, cell: StateCellId) -> u64 {
        match engine.read(cell) {
            FourStateValue::Wide { aval, .. } => aval[0],
            FourStateValue::Narrow(_) => panic!("expected a Wide value"),
        }
    }

    /// ST-034: the concrete structural proof of "K+1, never a single shared
    /// slot" — a `DriverSet` with 3 `DriverEntry`s has `drivers.len() == 3`
    /// and `resolved` is a *4th*, distinct `StateCellId`.
    #[test]
    fn k_plus_1_slots_means_k_contribution_cells_plus_one_resolved_cell() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let d0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
        let d1 = seeded_scalar_cell(&mut engine, Bit4::One);
        let d2 = seeded_scalar_cell(&mut engine, Bit4::X);
        let set = DriverSet {
            resolved,
            drivers: vec![
                DriverEntry {
                    source: d0,
                    strength: strong_pair(),
                    forced: false,
                },
                DriverEntry {
                    source: d1,
                    strength: strong_pair(),
                    forced: false,
                },
                DriverEntry {
                    source: d2,
                    strength: strong_pair(),
                    forced: false,
                },
            ],
            net_kind: NetKind::Wire,
        };

        assert_eq!(set.drivers.len(), 3);
        assert_ne!(set.resolved, d0);
        assert_ne!(set.resolved, d1);
        assert_ne!(set.resolved, d2);
    }

    /// state.md §4 step 3: two `Strong` drivers agreeing on `One` resolve to
    /// `One` on an ordinary `Wire`.
    #[test]
    fn two_strong_drivers_agreeing_resolve_to_that_value_wire() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let d0 = seeded_scalar_cell(&mut engine, Bit4::One);
        let d1 = seeded_scalar_cell(&mut engine, Bit4::One);
        let set = DriverSet {
            resolved,
            drivers: vec![
                DriverEntry {
                    source: d0,
                    strength: strong_pair(),
                    forced: false,
                },
                DriverEntry {
                    source: d1,
                    strength: strong_pair(),
                    forced: false,
                },
            ],
            net_kind: NetKind::Wire,
        };

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(read_bit(&engine, resolved), Bit4::One);
    }

    /// state.md §4 step 3: a `Strong`-driving-`0` beats a `Weak`-driving-`1`
    /// on a `Wire` regardless of which order the two entries are registered
    /// in `DriverSet.drivers` — proves the fold is order-independent, not
    /// accidentally favoring registration order over strength.
    #[test]
    fn strong_beats_weak_on_a_wire_regardless_of_registration_order() {
        for reversed in [false, true] {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let strong0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
            let weak1 = seeded_scalar_cell(&mut engine, Bit4::One);
            let mut drivers = vec![
                DriverEntry {
                    source: strong0,
                    strength: strong_pair(),
                    forced: false,
                },
                DriverEntry {
                    source: weak1,
                    strength: DriveStrengthPair {
                        s0: DriveStrength::Weak,
                        s1: DriveStrength::Weak,
                    },
                    forced: false,
                },
            ];
            if reversed {
                drivers.reverse();
            }
            let set = DriverSet {
                resolved,
                drivers,
                net_kind: NetKind::Wire,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                Bit4::Zero,
                "reversed={reversed}: strong driver must win regardless of registration order"
            );
        }
    }

    /// Mutation regression (survived the mutation-testing pass): a
    /// contributor driving `X` reduces its two-sided `DriveStrengthPair` to
    /// a single [`DriveStrength`] via `effective_strength`, which
    /// `combine_bit`'s own doc comment pins as `min(s0, s1)` (state.md §4's
    /// "driver outputting X" resolution), never `max(s0, s1)`. Built so the
    /// two reductions disagree observably: the `X`-driver's pair is
    /// `{s0: Weak, s1: Strong}` (`min` = `Weak`, `max` = `Strong`) alongside
    /// a `Zero`-driver at `Strong`/`Strong`. Under the correct `min`
    /// reduction the `X`-driver's effective strength is `Weak`, strictly
    /// below the `Zero`-driver's `Strong`, so `Zero` wins outright. Under a
    /// `max` reduction the `X`-driver's effective strength would tie the
    /// `Zero`-driver's at `Strong`, and two disagreeing winners in the same
    /// strength group fold to `X` on an ordinary `Wire` (per
    /// `two_strong_disagreeing_drivers_resolve_per_net_kind` above) — an
    /// observably different, wrong result this test would catch.
    #[test]
    fn effective_strength_reduces_an_x_driving_contributor_by_the_weaker_of_its_two_strengths() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let x_driver = seeded_scalar_cell(&mut engine, Bit4::X);
        let zero_driver = seeded_scalar_cell(&mut engine, Bit4::Zero);
        let set = DriverSet {
            resolved,
            drivers: vec![
                DriverEntry {
                    source: x_driver,
                    strength: DriveStrengthPair {
                        s0: DriveStrength::Weak,
                        s1: DriveStrength::Strong,
                    },
                    forced: false,
                },
                DriverEntry {
                    source: zero_driver,
                    strength: strong_pair(),
                    forced: false,
                },
            ],
            net_kind: NetKind::Wire,
        };

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::Zero,
            "an X-driving contributor's effective strength must be min(s0,s1) = Weak here, \
             losing outright to the Strong zero driver -- not max(s0,s1) = Strong, which \
             would tie and fold to X"
        );
    }

    /// Table-driven: two equal-strength, disagreeing (`0` vs `1`) drivers
    /// resolve per `net_kind`'s own family — `Wire` -> `X`, `WAnd` -> `0`,
    /// `WOr` -> `1`. Each sub-case is a concrete regression for a specific
    /// net-kind branch in `combine_bit`.
    #[test]
    fn two_strong_disagreeing_drivers_resolve_per_net_kind() {
        for (net_kind, expected) in [
            (NetKind::Wire, Bit4::X),
            (NetKind::WAnd, Bit4::Zero),
            (NetKind::WOr, Bit4::One),
        ] {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let d0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
            let d1 = seeded_scalar_cell(&mut engine, Bit4::One);
            let set = DriverSet {
                resolved,
                drivers: vec![
                    DriverEntry {
                        source: d0,
                        strength: strong_pair(),
                        forced: false,
                    },
                    DriverEntry {
                        source: d1,
                        strength: strong_pair(),
                        forced: false,
                    },
                ],
                net_kind,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                expected,
                "net_kind={net_kind:?}"
            );
        }
    }

    /// state.md §4 step 1 / "undriven net" emergent property: two `Z`-valued
    /// drivers never participate in the fold at all — `resolved` reads `Z`
    /// as a genuine fold result of zero remaining (post-Z-filter)
    /// contributors, not a hand-coded special case.
    #[test]
    fn z_valued_drivers_never_participate_undriven_net_reads_as_z() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let d0 = seeded_scalar_cell(&mut engine, Bit4::Z);
        let d1 = seeded_scalar_cell(&mut engine, Bit4::Z);
        let set = DriverSet {
            resolved,
            drivers: vec![
                DriverEntry {
                    source: d0,
                    strength: strong_pair(),
                    forced: false,
                },
                DriverEntry {
                    source: d1,
                    strength: strong_pair(),
                    forced: false,
                },
            ],
            net_kind: NetKind::Wire,
        };

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(read_bit(&engine, resolved), Bit4::Z);
    }

    /// Regression for the review finding that `combine_bit`'s wand/wor fold
    /// dropped lower-strength drivers entirely (grouping by strength *before*
    /// applying the AND/OR fold, instead of folding every live driver
    /// regardless of strength, per IEEE 1800 Table 28-8). Mirrors an iverilog
    /// 12 repro exactly: on a `wand`, `strong1,strong0` driving `1` combined
    /// with `weak1,weak0` driving `0` must resolve to `0` (iverilog:
    /// `w=0`) — the pre-fix algorithm grouped by strength first, discarded
    /// the weak `0` before any AND happened, and left only the strong `1`
    /// group, producing `1`. Symmetric `wor` case: `strong` driving `0`
    /// combined with `weak` driving `1` must resolve to `1` (iverilog:
    /// `w=1`), not `0`.
    #[test]
    fn heterogeneous_strength_drivers_still_all_participate_in_wand_wor_fold() {
        let weak_pair = DriveStrengthPair {
            s0: DriveStrength::Weak,
            s1: DriveStrength::Weak,
        };

        // wand: assign (strong1,strong0) w=1; assign (weak1,weak0) w=0;
        {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let strong1 = seeded_scalar_cell(&mut engine, Bit4::One);
            let weak0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
            let set = DriverSet {
                resolved,
                drivers: vec![
                    DriverEntry {
                        source: strong1,
                        strength: strong_pair(),
                        forced: false,
                    },
                    DriverEntry {
                        source: weak0,
                        strength: weak_pair,
                        forced: false,
                    },
                ],
                net_kind: NetKind::WAnd,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                Bit4::Zero,
                "wand must AND-fold every live driver regardless of strength \
                 (matches iverilog 12: w=0), not drop the weak 0 via strength-grouping"
            );
        }

        // wor: assign (strong1,strong0) w=0; assign (weak1,weak0) w=1;
        {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let strong0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
            let weak1 = seeded_scalar_cell(&mut engine, Bit4::One);
            let set = DriverSet {
                resolved,
                drivers: vec![
                    DriverEntry {
                        source: strong0,
                        strength: strong_pair(),
                        forced: false,
                    },
                    DriverEntry {
                        source: weak1,
                        strength: weak_pair,
                        forced: false,
                    },
                ],
                net_kind: NetKind::WOr,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                Bit4::One,
                "wor must OR-fold every live driver regardless of strength \
                 (matches iverilog 12: w=1), not drop the weak 1 via strength-grouping"
            );
        }
    }

    /// ST-055: `force_driver` on a `Strong`-driving-`0` wire overrides it
    /// outright (force wins regardless of the ordinary driver's own
    /// strength); `release_driver` removes the forced entry and reverts to
    /// the still-present strong driver's value. Fails if `force`/`release`
    /// were the archived hard-error stubs instead of a real synthetic
    /// driver.
    #[test]
    fn force_overrides_a_strong_wire_driver_release_restores_prior_value() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let strong0 = seeded_scalar_cell(&mut engine, Bit4::Zero);
        let mut set = DriverSet {
            resolved,
            drivers: vec![DriverEntry {
                source: strong0,
                strength: strong_pair(),
                forced: false,
            }],
            net_kind: NetKind::Wire,
        };

        let (v, u) = Bit4::One.to_val_unk();
        let one = FourStateValue::Narrow((v as u128) | ((u as u128) << 64));
        let forced = force_driver(&mut engine, &mut set, resolved, one);

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::One,
            "force must win outright over the ordinary strong driver"
        );

        release_driver(&mut engine, &mut set, forced);
        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::Zero,
            "release must restore the still-present strong driver's value"
        );
    }

    /// Mutation regression (survived the mutation-testing pass):
    /// `release_driver` must remove exactly the one `DriverEntry` named by
    /// its `forced: StateCellId` parameter, never every `forced`-tagged
    /// entry in `set.drivers` -- a `retain` keyed on `!entry.forced` instead
    /// of `entry.source != forced` happens to produce the same observable
    /// result while at most one forced entry is ever live (this crate's own
    /// v1 usage pattern), but is a different, wrong function the moment two
    /// are: two consecutive `force_driver` calls on the same `set` (with no
    /// `release_driver` between them, exactly the "if more than one were
    /// ever present, the first ... wins" case `resolve_net_step`'s own doc
    /// comment already accounts for) leave two `forced` entries; releasing
    /// the first-pushed one must leave the second-pushed one fully live.
    #[test]
    fn release_driver_removes_only_the_named_forced_entry_not_every_forced_entry() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let ordinary = seeded_scalar_cell(&mut engine, Bit4::One);
        let mut set = DriverSet {
            resolved,
            drivers: vec![DriverEntry {
                source: ordinary,
                strength: strong_pair(),
                forced: false,
            }],
            net_kind: NetKind::Wire,
        };

        let (v, u) = Bit4::Zero.to_val_unk();
        let zero = FourStateValue::Narrow((v as u128) | ((u as u128) << 64));
        let forced_a = force_driver(&mut engine, &mut set, resolved, zero);

        let (v, u) = Bit4::X.to_val_unk();
        let x = FourStateValue::Narrow((v as u128) | ((u as u128) << 64));
        let _forced_b = force_driver(&mut engine, &mut set, resolved, x);

        release_driver(&mut engine, &mut set, forced_a);
        assert_eq!(
            set.drivers.len(),
            2,
            "releasing forced_a must remove exactly that one entry, leaving the ordinary \
             driver and the still-live forced_b entry"
        );
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::X,
            "forced_b, pushed after forced_a and never released, must still be the entry \
             resolve_net_step's forced short-circuit picks -- not silently removed alongside \
             forced_a"
        );
    }

    /// ST-146-adjacent: closes the `combine_bit`/`resolve_net_step`
    /// loud-error requirement in two sub-cases. (1) `combine_bit(&[],
    /// NetKind::UserDefined)` rejects even with zero contributions -- the
    /// rejection isn't conditioned on there being any drivers to fold. (2) A
    /// `DriverSet` with `net_kind: NetKind::UserDefined` and one real,
    /// otherwise-trivially-resolvable `DriverEntry` is rejected the same
    /// way, and `set.resolved`'s cell is left at its pre-call value -- no
    /// partial/guessed commit on the rejected path. Fails if the
    /// `UserDefined` arm panicked, silently fell through to another net
    /// kind's fold logic, or resolved to an arbitrary winner instead of
    /// returning the typed `Err`.
    #[test]
    fn combine_bit_and_resolve_net_step_reject_userdefined_net_kind_with_a_typed_error() {
        assert_eq!(
            combine_bit(&[], NetKind::UserDefined),
            Err(DriverError::UnresolvableUserDefinedNetType)
        );

        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let d0 = seeded_scalar_cell(&mut engine, Bit4::One);
        let set = DriverSet {
            resolved,
            drivers: vec![DriverEntry {
                source: d0,
                strength: strong_pair(),
                forced: false,
            }],
            net_kind: NetKind::UserDefined,
        };

        let before = read_bit(&engine, resolved);
        let result = resolve_net_step(&mut engine, &set, &mut ());
        assert_eq!(
            result.err(),
            Some(DriverError::UnresolvableUserDefinedNetType)
        );
        assert_eq!(
            read_bit(&engine, resolved),
            before,
            "no partial/guessed commit on the rejected path"
        );
    }

    /// Regression for review finding 1 (blocking): `combine_bit` previously
    /// resolved `NetKind::Tri0`/`Tri1` identically to `Wire`/`Tri`, entirely
    /// omitting the LRM-mandated implicit resistive pull (tri0 pulls weakly
    /// to 0, tri1 to 1, whenever nothing stronger drives the net). Verified
    /// empirically against iverilog 12: an undriven `tri0 w;` reads `0`, an
    /// undriven `tri1 w;` reads `1` -- not `Z`, unlike every other net kind
    /// with zero live drivers.
    #[test]
    fn undriven_tri0_reads_zero_and_undriven_tri1_reads_one_via_implicit_pull() {
        for (net_kind, expected) in [(NetKind::Tri0, Bit4::Zero), (NetKind::Tri1, Bit4::One)] {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let set = DriverSet {
                resolved,
                drivers: vec![],
                net_kind,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                expected,
                "net_kind={net_kind:?}: undriven tri0/tri1 must read its implicit pull, not Z"
            );
        }
    }

    /// Regression for review finding 1 (blocking): the implicit pull is at
    /// `Pull` strength, which must beat an explicit `Weak` driver rather than
    /// losing to it outright. Verified empirically against iverilog 12:
    /// `tri0 w; assign (weak0,weak1) w=1;` still reads `0`.
    #[test]
    fn tri0_tri1_implicit_pull_beats_an_explicit_weak_driver() {
        let weak_pair = DriveStrengthPair {
            s0: DriveStrength::Weak,
            s1: DriveStrength::Weak,
        };
        for (net_kind, weak_drives, expected) in [
            (NetKind::Tri0, Bit4::One, Bit4::Zero),
            (NetKind::Tri1, Bit4::Zero, Bit4::One),
        ] {
            let mut engine = fresh_engine();
            let resolved = scalar_cell(&mut engine);
            let weak_driver = seeded_scalar_cell(&mut engine, weak_drives);
            let set = DriverSet {
                resolved,
                drivers: vec![DriverEntry {
                    source: weak_driver,
                    strength: weak_pair,
                    forced: false,
                }],
                net_kind,
            };

            resolve_net_step(&mut engine, &set, &mut ()).unwrap();
            assert_eq!(
                read_bit(&engine, resolved),
                expected,
                "net_kind={net_kind:?}: the implicit Pull-strength pull must beat an \
                 explicit Weak driver, matching iverilog 12"
            );
        }
    }

    /// Regression for review finding 2 (blocking): `force_driver` used to
    /// panic for any `SlotClass::Wide`/`Memory` net (`bit_width > 64`) once
    /// `Arena::seal_wide_plane` had fired -- its Wide branch called
    /// `Arena::alloc_wide_words` unconditionally for its own contribution
    /// cell, which refuses any further growth once sealed (Task 9 r3's own
    /// review fix). `seal_wide_plane` is called for real the instant any wide
    /// signal is read through the compiled-kernel FFI accessor
    /// (`accessor_impl.rs::sv_get_wide`) -- the very ABI this crate exists to
    /// serve -- so any realistic simulation with a >64-bit signal would hit
    /// this before any `force` statement ever ran. This proves `force`/
    /// `release` keep working after the seal by growing the separate,
    /// never-sealed `SlotClass::ForceWide` plane instead.
    #[test]
    fn force_and_release_still_work_on_a_wide_net_after_the_wide_plane_is_sealed() {
        let mut engine = fresh_engine();
        let resolved = wide_cell(&mut engine);
        let strong_driver = seeded_wide_cell(&mut engine, 0xAAAA_AAAA);
        let mut set = DriverSet {
            resolved,
            drivers: vec![DriverEntry {
                source: strong_driver,
                strength: strong_pair(),
                forced: false,
            }],
            net_kind: NetKind::Wire,
        };
        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(read_wide_aval0(&engine, resolved), 0xAAAA_AAAA);

        // Simulate a prior `sv_get_wide` call elsewhere in the same
        // simulation, exactly as the review finding's own repro did.
        engine.arena.seal_wide_plane();
        assert!(engine.arena.is_wide_plane_sealed());

        let forced_value = FourStateValue::Wide {
            aval: vec![0xFFFF_FFFF, 0],
            bval: vec![0, 0],
        };
        // Must not panic even though the ordinary wide plane is sealed.
        let forced = force_driver(&mut engine, &mut set, resolved, forced_value);

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_wide_aval0(&engine, resolved),
            0xFFFF_FFFF,
            "force must win outright over the ordinary strong driver on a Wide net"
        );

        release_driver(&mut engine, &mut set, forced);
        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_wide_aval0(&engine, resolved),
            0xAAAA_AAAA,
            "release must restore the still-present strong driver's value"
        );
    }

    /// Regression for review finding 3 (blocking): r1's fix made
    /// `wand`/`triand`/`wor`/`trior` resolution ignore drive strength
    /// entirely (matching real LRM/iverilog behavior for the ordinary
    /// multi-driver case), which silently broke `force`'s override guarantee
    /// on those net kinds -- a merely `Supply`-strength forced entry became
    /// just one more live contributor in the wired-AND/OR fold and could be
    /// outvoted by an ordinary driver of any strength. `force` must still win
    /// outright, independent of net kind.
    #[test]
    fn force_overrides_an_ordinary_driver_on_a_wand_net() {
        let mut engine = fresh_engine();
        let resolved = scalar_cell(&mut engine);
        let ordinary = seeded_scalar_cell(&mut engine, Bit4::Zero);
        let mut set = DriverSet {
            resolved,
            drivers: vec![DriverEntry {
                source: ordinary,
                strength: strong_pair(),
                forced: false,
            }],
            net_kind: NetKind::WAnd,
        };

        let (v, u) = Bit4::One.to_val_unk();
        let one = FourStateValue::Narrow((v as u128) | ((u as u128) << 64));
        let forced = force_driver(&mut engine, &mut set, resolved, one);

        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::One,
            "force must win outright on a wand net even though the wired-AND fold of \
             the ordinary driver's 0 and the forced 1 would otherwise resolve to 0"
        );

        release_driver(&mut engine, &mut set, forced);
        resolve_net_step(&mut engine, &set, &mut ()).unwrap();
        assert_eq!(
            read_bit(&engine, resolved),
            Bit4::Zero,
            "release must restore the still-present ordinary driver's value"
        );
    }
}