wots_rhdl/verify/

top.rs

//! Three-cluster SHA-256 verifier top with global fail-closed drainage.
//!
//! One input stream is locked to a selected cluster for exactly 35 accepted
//! beats. Beat zero strictly targets the registered three-way rotating cursor;
//! a busy target causes bounded head-of-line stall even when another cluster is
//! ready. The cursor advances only after accepted beat zero. The fixed
//! accepted-beat count, never untrusted `last`, releases ownership. The selected
//! cluster, physical context, and generation form the complete internal job
//! identity.
//! The selected child sees a standard ready/valid offer independent of its
//! ready response; top and child frame state advance only on their identical
//! accepted event. Field-level stream muxes keep unrelated cluster status out
//! of that handshake's structural dependency graph. Each cluster input is also
//! a direct literal with independent one-hot stream-valid and result-ready
//! fields; no dynamic aggregate mutation joins those protocols during lowering.
//!
//! Results cross a one-entry registered fair merge. The retained payload is
//! stable under stalls except that the first global fatal edge converts a clean
//! completion to an identified transport error and suppresses its transfer.
//! Any local cluster fault latches global poison. Peer abort is driven only from
//! that registered poison bit, so a child output can never feed a combinational
//! fault-to-abort-to-fault loop.
//!
//! A current cluster fault is a containment-edge exception to ordinary
//! ready/fault intuition. It may depend on a child response observed on this
//! edge, so top admission cannot retract already-advertised credit through that
//! path. One beat may therefore transfer while `fault` rises. The selected
//! cluster receives exactly the reported accepted beat and retains its job
//! identity; registered poison removes credit on the next cycle. Result
//! transfer and capture remain suppressed on the original fault edge.
//!
//! The first broadcast-abort edge is transition-only inside each still-clean
//! peer: its output remains independent of `external_abort`, while poison,
//! frame-clear, and diagnostic D state are recorded. The poisoned top presents
//! neither a stream beat nor a child-result grant on that edge. At most one lane
//! launch, one routed return, and one internal result capture belonging to
//! already-accepted work may advance per peer. A separate registered
//! `drain_armed` phase waits for peer poison to contain those effects before the
//! top selects any poisoned child. Once armed, selection depends only on a
//! child's registered `result_valid`, never on payload data that could feed its
//! release wire. Capture defensively converts any unexpected clean payload to
//! an identified transport error and preserves every existing nonzero error.
//! Every captured child is released on the same edge, and the top's registered
//! slot may replace a transferring completion.
//!
//! This module provides source/RHDL behavioral structure only. It makes no
//! emitted-RTL, synthesis, resource, timing, route, throughput, or card claim.

use rhdl::{core::ReplicatedSynchronous, prelude::*};
use rhdl_fpga::core::dff::DFF;
use rhdl_primitives::NoResetDff;
use sha256_rhdl::lane::{ExternalFullCompressionLane, InlineCompressionLane};

use crate::{
    cluster::CompressionLaneComponent,
    verify::{
        cluster::{VerifierCluster, VerifyClusterInput, VerifyResult},
        framing::VerifyStreamBeat,
        sha::{VERIFY_ERROR_NONE, VERIFY_ERROR_TRANSPORT},
    },
};

/// Number of independent lane-local verifier clusters.
pub const VERIFY_TOP_CLUSTERS: usize = 3;
/// Number of physical verifier contexts across all clusters.
pub const VERIFY_TOP_CONTEXTS: usize = VERIFY_TOP_CLUSTERS * 4;

/// Cluster zero caused the first global poison edge.
pub const VERIFY_TOP_DIAGNOSTIC_CLUSTER_0: u128 = 1 << 0;
/// Cluster one caused the first global poison edge.
pub const VERIFY_TOP_DIAGNOSTIC_CLUSTER_1: u128 = 1 << 1;
/// Cluster two caused the first global poison edge.
pub const VERIFY_TOP_DIAGNOSTIC_CLUSTER_2: u128 = 1 << 2;
/// Registered top/child frame ownership disagreed.
pub const VERIFY_TOP_DIAGNOSTIC_OWNERSHIP: u128 = 1 << 3;
/// Admission cursor was outside `0..=2`.
pub const VERIFY_TOP_DIAGNOSTIC_ADMISSION_CURSOR: u128 = 1 << 4;
/// Result cursor was outside `0..=2`.
pub const VERIFY_TOP_DIAGNOSTIC_RESULT_CURSOR: u128 = 1 << 5;

const _: () = {
    assert!(VERIFY_TOP_CLUSTERS == 3);
    assert!(VERIFY_TOP_CONTEXTS == 12);
};

/// External verifier input and result-consumer handshake.
#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
pub struct VerifierTopInput {
    /// One 512-bit verifier input beat is present.
    pub stream_valid: bool,
    /// Signature, public-key material, message, and sideband.
    pub stream: VerifyStreamBeat,
    /// Consumer accepts the registered top result.
    pub result_ready: bool,
}

/// Three-way rotating selection result.
#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
pub struct VerifierTopSelection {
    /// At least one eligible cluster exists.
    pub valid: bool,
    /// Selected cluster `0..=2`.
    pub cluster: b2,
    /// Cursor following the selected cluster.
    pub next_cursor: b2,
}

/// Narrow resettable frame, merge, and poison state.
#[allow(clippy::struct_excessive_bools)] // Independent protocol phases.
#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
pub struct VerifierTopControl {
    /// Rotating beat-zero admission cursor.
    pub admission_cursor: b2,
    /// One cluster owns the current 35-beat input frame.
    pub frame_active: bool,
    /// Cluster owning the current frame.
    pub frame_cluster: b2,
    /// Physical context assigned on accepted beat zero.
    pub frame_context: b2,
    /// Generation assigned on accepted beat zero.
    pub frame_generation: b8,
    /// Next fixed beat index expected by the owner.
    pub frame_beat: b6,
    /// Rotating cluster-result cursor.
    pub result_cursor: b2,
    /// One registered result occupies the top slot.
    pub result_valid: bool,
    /// Source cluster of the retained result.
    pub result_cluster: b2,
    /// Sticky global poison.
    pub poison: bool,
    /// A complete registered peer-abort edge has elapsed.
    pub drain_armed: bool,
    /// Sticky first-cause top diagnostics.
    pub diagnostics: b8,
    /// Cluster-fault mask sampled before peer abort changes every child.
    pub origin_cluster_fault: b3,
    /// Per-cluster diagnostic snapshots from the first fatal edge.
    pub origin_cluster_diagnostics: [b16; VERIFY_TOP_CLUSTERS],
}

/// Global verifier status, accepted identity, and registered result.
///
/// `result` and `result_cluster` are meaningful only while `result_valid` is
/// true. They remain stable while the result is stalled, except that the first
/// fatal edge may fail-closed convert a retained clean result into an identified
/// transport error while suppressing transfer. When `result_valid` is false,
/// the stored payload fields may be stale or unspecified and must not be
/// consumed.
#[allow(clippy::struct_excessive_bools)] // Independent host and audit wires.
#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
pub struct VerifierTopOutput {
    /// The presented input beat may transfer.
    pub stream_ready: bool,
    /// One input beat transferred this cycle.
    pub stream_accepted: bool,
    /// Cluster owning or selected for the transfer.
    pub stream_cluster: b2,
    /// Physical context owning or selected for the transfer.
    pub stream_context: b2,
    /// Generation owning or selected for the transfer.
    pub stream_generation: b8,
    /// A fixed-count global input frame is active.
    pub frame_active: bool,
    /// Current global frame owner.
    pub frame_cluster: b2,
    /// Next fixed beat index for the current frame.
    pub frame_beat: b6,
    /// Beat-zero job identity retained for ownership diagnostics.
    pub frame_job_id: b32,
    /// Per-cluster input readiness before global selection.
    pub cluster_stream_ready: [bool; VERIFY_TOP_CLUSTERS],
    /// Per-cluster frame ownership state.
    pub cluster_frame_active: [bool; VERIFY_TOP_CLUSTERS],
    /// Per-cluster physical loading state.
    pub cluster_context_loading: [[bool; 4]; VERIFY_TOP_CLUSTERS],
    /// Per-cluster physical task-graph activity.
    pub cluster_context_active: [[bool; 4]; VERIFY_TOP_CLUSTERS],
    /// Per-cluster retained child results.
    pub cluster_context_result_valid: [[bool; 4]; VERIFY_TOP_CLUSTERS],
    /// Immediate or sticky per-cluster faults.
    pub cluster_fault: [bool; VERIFY_TOP_CLUSTERS],
    /// Per-cluster sticky diagnostics.
    pub cluster_diagnostics: [b16; VERIFY_TOP_CLUSTERS],
    /// One registered top result is available and its payload fields are
    /// meaningful.
    pub result_valid: bool,
    /// Registered completion.
    ///
    /// Meaningful only when `result_valid`. Stable while stalled except for the
    /// documented fail-closed conversion on the first fatal edge.
    pub result: VerifyResult,
    /// Source cluster retained beside `result`, meaningful only when
    /// `result_valid`.
    pub result_cluster: b2,
    /// The registered top result transferred this cycle.
    pub result_transfer: bool,
    /// Immediate or sticky global poison.
    pub fault: bool,
    /// A complete registered peer-abort edge has elapsed.
    pub drain_armed: bool,
    /// Sticky top-level cause mask.
    pub diagnostics: b8,
    /// First-edge cluster-fault snapshot.
    pub origin_cluster_fault: b3,
    /// First-edge per-cluster diagnostic snapshot.
    pub origin_cluster_diagnostics: [b16; VERIFY_TOP_CLUSTERS],
}

/// Select one of three eligible clusters with rotating fairness.
#[kernel]
#[allow(clippy::assign_op_pattern)] // Compound assignment is not lowered by pinned RHDL.
pub fn select_verifier_top_cluster_kernel(
    eligible: [bool; VERIFY_TOP_CLUSTERS],
    cursor: b2,
) -> VerifierTopSelection {
    let normalized_cursor = if cursor < b2(3) { cursor } else { b2(0) };
    let mut selection = VerifierTopSelection {
        next_cursor: normalized_cursor,
        ..VerifierTopSelection::default()
    };
    let mut scan = normalized_cursor;
    for _offset in 0..VERIFY_TOP_CLUSTERS {
        if !selection.valid && eligible[scan] {
            selection.valid = true;
            selection.cluster = scan;
            selection.next_cursor = if scan == b2(2) { b2(0) } else { scan + b2(1) };
        }
        scan = if scan == b2(2) { b2(0) } else { scan + b2(1) };
    }
    selection
}

/// Three replicated four-context verifier clusters and narrow global control.
#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
pub struct VerifierTop<L = InlineCompressionLane<64, 6>>
where
    L: CompressionLaneComponent,
{
    clusters: ReplicatedSynchronous<VerifierCluster<L>, VERIFY_TOP_CLUSTERS>,
    control: DFF<VerifierTopControl>,
    frame_job_id: NoResetDff<b32>,
    result: NoResetDff<VerifyResult>,
}

impl<L> Default for VerifierTop<L>
where
    L: CompressionLaneComponent + Default,
{
    fn default() -> Self {
        Self {
            clusters: ReplicatedSynchronous::new(VerifierCluster::default()),
            control: DFF::new(VerifierTopControl::default()),
            frame_job_id: NoResetDff::new(),
            result: NoResetDff::new(),
        }
    }
}

impl<L> SynchronousIO for VerifierTop<L>
where
    L: CompressionLaneComponent,
{
    type I = VerifierTopInput;
    type O = VerifierTopOutput;
    type Kernel = verifier_top_with_lane_kernel<L>;
}

/// Global frame ownership, result merge, and registered peer-abort broadcast.
#[kernel]
#[allow(clippy::assign_op_pattern, clippy::needless_range_loop)] // Pinned RHDL lowering subset.
pub fn verifier_top_with_lane_kernel<L: CompressionLaneComponent>(
    clock_reset: ClockReset,
    input: VerifierTopInput,
    q: VerifierTopQ<L>,
) -> (VerifierTopOutput, VerifierTopD<L>) {
    let resetting = clock_reset.reset.any();
    let cluster_ready = [
        q.clusters[0].stream_ready,
        q.clusters[1].stream_ready,
        q.clusters[2].stream_ready,
    ];
    let cluster_frames = [
        q.clusters[0].frame_active,
        q.clusters[1].frame_active,
        q.clusters[2].frame_active,
    ];
    let cluster_fault = [
        q.clusters[0].fault,
        q.clusters[1].fault,
        q.clusters[2].fault,
    ];
    let cluster_diagnostics = [
        q.clusters[0].diagnostics,
        q.clusters[1].diagnostics,
        q.clusters[2].diagnostics,
    ];

    let owner_consistent = match q.control.frame_cluster {
        Bits::<2>(0) => {
            cluster_frames[0]
                && !cluster_frames[1]
                && !cluster_frames[2]
                && q.clusters[0].stream_context == q.control.frame_context
                && q.clusters[0].stream_generation == q.control.frame_generation
                && q.clusters[0].frame_beat == q.control.frame_beat
                && q.clusters[0].frame_job_id == q.frame_job_id
        }
        Bits::<2>(1) => {
            !cluster_frames[0]
                && cluster_frames[1]
                && !cluster_frames[2]
                && q.clusters[1].stream_context == q.control.frame_context
                && q.clusters[1].stream_generation == q.control.frame_generation
                && q.clusters[1].frame_beat == q.control.frame_beat
                && q.clusters[1].frame_job_id == q.frame_job_id
        }
        Bits::<2>(2) => {
            !cluster_frames[0]
                && !cluster_frames[1]
                && cluster_frames[2]
                && q.clusters[2].stream_context == q.control.frame_context
                && q.clusters[2].stream_generation == q.control.frame_generation
                && q.clusters[2].frame_beat == q.control.frame_beat
                && q.clusters[2].frame_job_id == q.frame_job_id
        }
        _ => false,
    };
    let any_cluster_frame = cluster_frames[0] || cluster_frames[1] || cluster_frames[2];
    let ownership_fault = !q.control.poison
        && ((q.control.frame_active && !owner_consistent)
            || (!q.control.frame_active && any_cluster_frame));
    let admission_cursor_fault = q.control.admission_cursor >= b2(3);
    let result_cursor_fault = q.control.result_cursor >= b2(3);
    let observed_cluster_fault = cluster_fault[0] || cluster_fault[1] || cluster_fault[2];

    let mut diagnostic_now = b8(0);
    let mut origin_cluster_fault = b3(0);
    if cluster_fault[0] {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_CLUSTER_0);
        origin_cluster_fault = origin_cluster_fault | b3(1);
    }
    if cluster_fault[1] {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_CLUSTER_1);
        origin_cluster_fault = origin_cluster_fault | b3(2);
    }
    if cluster_fault[2] {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_CLUSTER_2);
        origin_cluster_fault = origin_cluster_fault | b3(4);
    }
    if ownership_fault {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_OWNERSHIP);
    }
    if admission_cursor_fault {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_ADMISSION_CURSOR);
    }
    if result_cursor_fault {
        diagnostic_now = diagnostic_now | b8(VERIFY_TOP_DIAGNOSTIC_RESULT_CURSOR);
    }
    let fatal_now = !resetting
        && !q.control.poison
        && (observed_cluster_fault
            || ownership_fault
            || admission_cursor_fault
            || result_cursor_fault);
    let fault = q.control.poison || fatal_now;
    let admission_fatal_now = !resetting
        && !q.control.poison
        && (ownership_fault || admission_cursor_fault || result_cursor_fault);

    // Beat-zero targeting is strict round-robin from registered state. Child
    // ready affects only acceptance, never which child sees valid. This permits
    // bounded head-of-line stalls but removes every ready -> selector -> valid
    // dependency from the hierarchy.
    let admission_target = if q.control.admission_cursor < b2(3) {
        q.control.admission_cursor
    } else {
        b2(0)
    };
    let selected_cluster = if q.control.frame_active {
        q.control.frame_cluster
    } else {
        admission_target
    };
    // Mux only the scalar stream fields consumed below. Selecting the complete
    // cluster aggregate would make unrelated fault/result/response fields
    // structural dependencies of stream credit during RHDL lowering.
    let selected_stream_ready = match selected_cluster {
        Bits::<2>(0) => q.clusters[0].stream_ready,
        Bits::<2>(1) => q.clusters[1].stream_ready,
        _ => q.clusters[2].stream_ready,
    };
    let selected_stream_context = match selected_cluster {
        Bits::<2>(0) => q.clusters[0].stream_context,
        Bits::<2>(1) => q.clusters[1].stream_context,
        _ => q.clusters[2].stream_context,
    };
    let selected_stream_generation = match selected_cluster {
        Bits::<2>(0) => q.clusters[0].stream_generation,
        Bits::<2>(1) => q.clusters[1].stream_generation,
        _ => q.clusters[2].stream_generation,
    };
    // A current cluster fault may depend on the response that this hierarchy is
    // simultaneously presenting. Honor the credit already visible on this
    // edge; top-local structural faults remain safe immediate admission gates.
    let stream_ready =
        !resetting && !q.control.poison && !admission_fatal_now && selected_stream_ready;
    // Present valid independently of the selected child's ready/accepted
    // response. This is the ordinary ready/valid contract and cuts the
    // child-ready -> top-accepted -> child-valid hierarchy fixed point. Beat
    // zero uses only the registered strict-round-robin target; an active frame
    // uses its registered owner. Both therefore hold their offer through child
    // stalls without observing any ready signal.
    let stream_offer =
        !resetting && !q.control.poison && !admission_fatal_now && input.stream_valid;
    let stream_accepted = stream_offer && selected_stream_ready;

    let result_transfer = !resetting && !fatal_now && q.control.result_valid && input.result_ready;
    let result_slot_available = !q.control.result_valid || result_transfer;
    let poisoned_result_eligible = q.control.poison && q.control.drain_armed;
    let result_eligible = [
        q.clusters[0].result_valid && (!q.control.poison || poisoned_result_eligible),
        q.clusters[1].result_valid && (!q.control.poison || poisoned_result_eligible),
        q.clusters[2].result_valid && (!q.control.poison || poisoned_result_eligible),
    ];
    let result_selection =
        select_verifier_top_cluster_kernel(result_eligible, q.control.result_cursor);
    let capture_result =
        !resetting && !fatal_now && result_slot_available && result_selection.valid;

    let mut control = q.control;
    let mut frame_job_id = q.frame_job_id;
    let mut result = q.result;
    let mut visible_result = q.result;
    let abort_clean_result = !resetting
        && (fatal_now || q.control.poison)
        && q.control.result_valid
        && q.result.error == b3(VERIFY_ERROR_NONE);
    if abort_clean_result {
        visible_result = VerifyResult {
            job_id: q.result.job_id,
            verified: false,
            error: b3(VERIFY_ERROR_TRANSPORT),
        };
        result = visible_result;
    }

    if result_transfer {
        control.result_valid = false;
    }
    if capture_result {
        let child = match result_selection.cluster {
            Bits::<2>(0) => q.clusters[0].result,
            Bits::<2>(1) => q.clusters[1].result,
            _ => q.clusters[2].result,
        };
        let captured_error = if q.control.poison && child.error == b3(VERIFY_ERROR_NONE) {
            b3(VERIFY_ERROR_TRANSPORT)
        } else {
            child.error
        };
        result = VerifyResult {
            job_id: child.job_id,
            verified: captured_error == b3(VERIFY_ERROR_NONE) && child.verified,
            error: captured_error,
        };
        control.result_valid = true;
        control.result_cluster = result_selection.cluster;
        control.result_cursor = result_selection.next_cursor;
    }

    if stream_accepted {
        if q.control.frame_active {
            if q.control.frame_beat == b6(34) {
                control.frame_active = false;
                control.frame_beat = b6(0);
            } else {
                control.frame_beat = q.control.frame_beat + b6(1);
            }
        } else {
            control.frame_active = true;
            control.frame_cluster = admission_target;
            control.frame_context = selected_stream_context;
            control.frame_generation = selected_stream_generation;
            control.frame_beat = b6(1);
            control.admission_cursor = if admission_target == b2(2) {
                b2(0)
            } else {
                admission_target + b2(1)
            };
            frame_job_id = input.stream.job_id;
        }
    }

    if q.control.poison && !q.control.drain_armed {
        control.drain_armed = true;
    }
    if fatal_now {
        control.poison = true;
        control.drain_armed = false;
        control.frame_active = false;
        control.frame_beat = b6(0);
        control.diagnostics = q.control.diagnostics | diagnostic_now;
        control.origin_cluster_fault = origin_cluster_fault;
        control.origin_cluster_diagnostics = cluster_diagnostics;
    }
    if resetting {
        control = VerifierTopControl::default();
    }

    // Construct every child field directly. Dynamic mutation of one field in a
    // shared aggregate makes RHDL conservatively couple sibling fields; that
    // previously let fault-dependent result grant logic contaminate stream
    // valid. These scalar one-hot expressions keep the independent protocols
    // structurally separate as well as behaviorally separate.
    let cluster_external_abort = !resetting && q.control.poison;
    let cluster_0_stream_valid = stream_offer && selected_cluster == b2(0);
    let cluster_1_stream_valid = stream_offer && selected_cluster == b2(1);
    let cluster_2_stream_valid = stream_offer && selected_cluster == b2(2);
    let cluster_0_result_ready = capture_result && result_selection.cluster == b2(0);
    let cluster_1_result_ready = capture_result && result_selection.cluster == b2(1);
    let cluster_2_result_ready = capture_result && result_selection.cluster == b2(2);
    let cluster_inputs = [
        VerifyClusterInput {
            stream_valid: cluster_0_stream_valid,
            stream: input.stream,
            result_ready: cluster_0_result_ready,
            external_abort: cluster_external_abort,
        },
        VerifyClusterInput {
            stream_valid: cluster_1_stream_valid,
            stream: input.stream,
            result_ready: cluster_1_result_ready,
            external_abort: cluster_external_abort,
        },
        VerifyClusterInput {
            stream_valid: cluster_2_stream_valid,
            stream: input.stream,
            result_ready: cluster_2_result_ready,
            external_abort: cluster_external_abort,
        },
    ];

    let output = VerifierTopOutput {
        stream_ready,
        stream_accepted,
        stream_cluster: selected_cluster,
        stream_context: selected_stream_context,
        stream_generation: selected_stream_generation,
        frame_active: !resetting && q.control.frame_active,
        frame_cluster: q.control.frame_cluster,
        frame_beat: q.control.frame_beat,
        frame_job_id: q.frame_job_id,
        cluster_stream_ready: if resetting || q.control.poison || admission_fatal_now {
            [false; VERIFY_TOP_CLUSTERS]
        } else {
            cluster_ready
        },
        cluster_frame_active: if resetting {
            [false; VERIFY_TOP_CLUSTERS]
        } else {
            cluster_frames
        },
        cluster_context_loading: if resetting {
            [[false; 4]; VERIFY_TOP_CLUSTERS]
        } else {
            [
                q.clusters[0].context_loading,
                q.clusters[1].context_loading,
                q.clusters[2].context_loading,
            ]
        },
        cluster_context_active: if resetting {
            [[false; 4]; VERIFY_TOP_CLUSTERS]
        } else {
            [
                q.clusters[0].context_active,
                q.clusters[1].context_active,
                q.clusters[2].context_active,
            ]
        },
        cluster_context_result_valid: if resetting {
            [[false; 4]; VERIFY_TOP_CLUSTERS]
        } else {
            [
                q.clusters[0].context_result_valid,
                q.clusters[1].context_result_valid,
                q.clusters[2].context_result_valid,
            ]
        },
        cluster_fault: if resetting {
            [false; VERIFY_TOP_CLUSTERS]
        } else {
            cluster_fault
        },
        cluster_diagnostics: if resetting {
            [b16(0); VERIFY_TOP_CLUSTERS]
        } else {
            cluster_diagnostics
        },
        result_valid: !resetting && q.control.result_valid,
        result: visible_result,
        result_cluster: q.control.result_cluster,
        result_transfer,
        fault: !resetting && fault,
        drain_armed: !resetting && q.control.drain_armed,
        diagnostics: if resetting {
            b8(0)
        } else if fatal_now {
            q.control.diagnostics | diagnostic_now
        } else {
            q.control.diagnostics
        },
        origin_cluster_fault: if resetting {
            b3(0)
        } else if fatal_now {
            origin_cluster_fault
        } else {
            q.control.origin_cluster_fault
        },
        origin_cluster_diagnostics: if resetting {
            [b16(0); VERIFY_TOP_CLUSTERS]
        } else if fatal_now {
            cluster_diagnostics
        } else {
            q.control.origin_cluster_diagnostics
        },
    };
    let d = VerifierTopD::<L> {
        clusters: cluster_inputs,
        control,
        frame_job_id,
        result,
    };
    (output, d)
}

/// Production three-cluster verifier with three inline full SHA-256 lanes.
pub type Sha256VerifierTop = VerifierTop<InlineCompressionLane<64, 6>>;

/// Production verifier skeleton linked with one separately generated lane type.
///
/// Only the complete ordinary [`VerifierCluster`] is replicated. Its direct
/// external lane child remains unresolved until the separately generated RHDL
/// lane artifact is supplied to an external parser.
pub type ModularSha256VerifierTop = VerifierTop<ExternalFullCompressionLane>;

/// Native-lane wrapper retained as a stable free-kernel entry point.
#[kernel]
pub fn sha256_verifier_top_kernel(
    clock_reset: ClockReset,
    input: VerifierTopInput,
    q: VerifierTopQ<InlineCompressionLane<64, 6>>,
) -> (
    VerifierTopOutput,
    VerifierTopD<InlineCompressionLane<64, 6>>,
) {
    verifier_top_with_lane_kernel::<InlineCompressionLane<64, 6>>(clock_reset, input, q)
}

impl<L> VerifierTop<L>
where
    L: CompressionLaneComponent,
{
    /// Reads per-context launch handshakes from software-simulation state.
    ///
    /// This host-only helper is not part of [`VerifierTopInput`],
    /// [`VerifierTopOutput`], or the generated hardware interface.
    #[doc(hidden)]
    #[must_use]
    pub fn simulation_request_accepted(
        state: &<Self as Synchronous>::S,
    ) -> [[bool; 4]; VERIFY_TOP_CLUSTERS] {
        [
            state.0.clusters[0].request_accepted,
            state.0.clusters[1].request_accepted,
            state.0.clusters[2].request_accepted,
        ]
    }

    /// Reads per-context accepted-return pulses from software-simulation state.
    ///
    /// This host-only helper exists for exact finite source-equivalence gates;
    /// it adds no production datapath or hardware port.
    #[doc(hidden)]
    #[must_use]
    pub fn simulation_response_routed(
        state: &<Self as Synchronous>::S,
    ) -> [[bool; 4]; VERIFY_TOP_CLUSTERS] {
        [
            state.0.clusters[0].response_routed,
            state.0.clusters[1].response_routed,
            state.0.clusters[2].response_routed,
        ]
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::verify::{cluster::VerifyClusterOutput, sha::VERIFY_ERROR_FRAME};

    type NativeLane = InlineCompressionLane<64, 6>;

    fn fatal_collision_q(result: VerifyResult) -> VerifierTopQ<NativeLane> {
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[0].fault = true;
        clusters[0].diagnostics = b16(0x0004);
        clusters[1].result_valid = true;
        clusters[1].result = VerifyResult {
            job_id: b32(0x2222_0002),
            verified: true,
            error: b3(VERIFY_ERROR_NONE),
        };
        VerifierTopQ::<NativeLane> {
            clusters,
            control: VerifierTopControl {
                result_valid: true,
                result_cluster: b2(2),
                ..VerifierTopControl::default()
            },
            frame_job_id: b32(0),
            result,
        }
    }

    #[test]
    fn fatal_edge_converts_clean_top_slot_and_suppresses_transfer_and_child_capture() {
        let retained = VerifyResult {
            job_id: b32(0x1111_0001),
            verified: true,
            error: b3(VERIFY_ERROR_NONE),
        };
        let (output, d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            VerifierTopInput {
                result_ready: true,
                ..VerifierTopInput::default()
            },
            fatal_collision_q(retained),
        );

        assert!(output.fault);
        assert!(output.result_valid);
        assert!(!output.result_transfer);
        assert_eq!(output.result.job_id, retained.job_id);
        assert!(!output.result.verified);
        assert_eq!(output.result.error, b3(VERIFY_ERROR_TRANSPORT));
        assert_eq!(output.result_cluster, b2(2));
        assert!(d.control.result_valid);
        assert_eq!(d.result, output.result);
        assert!(!d.clusters[0].result_ready);
        assert!(!d.clusters[1].result_ready);
        assert!(!d.clusters[2].result_ready);
    }

    #[test]
    fn fatal_edge_preserves_retained_nonzero_error() {
        let retained = VerifyResult {
            job_id: b32(0x3333_0003),
            verified: false,
            error: b3(VERIFY_ERROR_FRAME),
        };
        let (output, d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            VerifierTopInput {
                result_ready: true,
                ..VerifierTopInput::default()
            },
            fatal_collision_q(retained),
        );

        assert!(output.fault);
        assert!(output.result_valid);
        assert!(!output.result_transfer);
        assert_eq!(output.result, retained);
        assert_eq!(d.result, retained);
        assert!(d.control.result_valid);
        assert!(!d.clusters[1].result_ready);
    }

    #[test]
    fn beat_zero_offer_targets_registered_cursor_even_when_another_cluster_is_ready() {
        let stream = VerifyStreamBeat {
            job_id: b32(0x3030_0003),
            ..VerifyStreamBeat::default()
        };
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[0].stream_ready = true;
        clusters[1].stream_context = b2(3);
        clusters[1].stream_generation = b8(9);
        clusters[2].stream_ready = true;
        let q = VerifierTopQ::<NativeLane> {
            clusters,
            control: VerifierTopControl {
                admission_cursor: b2(1),
                ..VerifierTopControl::default()
            },
            frame_job_id: b32(0),
            result: VerifyResult::default(),
        };
        let input = VerifierTopInput {
            stream_valid: true,
            stream,
            result_ready: false,
        };

        let (stalled, stalled_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            q,
        );
        assert_eq!(stalled.stream_cluster, b2(1));
        assert!(!stalled.stream_ready);
        assert!(!stalled.stream_accepted);
        assert!(stalled_d.clusters[1].stream_valid);
        assert_eq!(stalled_d.clusters[1].stream, stream);
        assert!(!stalled_d.clusters[0].stream_valid);
        assert!(!stalled_d.clusters[2].stream_valid);
        assert!(!stalled_d.control.frame_active);
        assert_eq!(stalled_d.control.admission_cursor, b2(1));

        let mut ready_q = q;
        ready_q.clusters[1].stream_ready = true;
        let (accepted, accepted_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            ready_q,
        );
        assert_eq!(accepted.stream_cluster, b2(1));
        assert!(accepted.stream_ready);
        assert!(accepted.stream_accepted);
        assert!(accepted_d.clusters[1].stream_valid);
        assert_eq!(accepted_d.clusters[1].stream, stream);
        assert!(accepted_d.control.frame_active);
        assert_eq!(accepted_d.control.frame_cluster, b2(1));
        assert_eq!(accepted_d.control.frame_context, b2(3));
        assert_eq!(accepted_d.control.frame_generation, b8(9));
        assert_eq!(accepted_d.control.frame_beat, b6(1));
        assert_eq!(accepted_d.control.admission_cursor, b2(2));
        assert_eq!(accepted_d.frame_job_id, stream.job_id);
    }

    #[test]
    fn selected_child_offer_is_ready_independent_and_acceptance_matches() {
        let stream = VerifyStreamBeat {
            job_id: b32(0x4040_0004),
            ..VerifyStreamBeat::default()
        };
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[1].frame_active = true;
        clusters[1].frame_beat = b6(5);
        clusters[1].frame_job_id = stream.job_id;
        clusters[1].stream_context = b2(2);
        clusters[1].stream_generation = b8(7);
        let q = VerifierTopQ::<NativeLane> {
            clusters,
            control: VerifierTopControl {
                frame_active: true,
                frame_cluster: b2(1),
                frame_context: b2(2),
                frame_generation: b8(7),
                frame_beat: b6(5),
                ..VerifierTopControl::default()
            },
            frame_job_id: stream.job_id,
            result: VerifyResult::default(),
        };
        let input = VerifierTopInput {
            stream_valid: true,
            stream,
            result_ready: false,
        };

        let (stalled, stalled_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            q,
        );
        assert!(!stalled.stream_ready);
        assert!(!stalled.stream_accepted);
        assert_eq!(stalled.stream_cluster, b2(1));
        assert_eq!(stalled.stream_context, b2(2));
        assert_eq!(stalled.stream_generation, b8(7));
        assert!(stalled_d.clusters[1].stream_valid);
        assert_eq!(stalled_d.clusters[1].stream, stream);
        assert!(!stalled_d.clusters[0].stream_valid);
        assert!(!stalled_d.clusters[2].stream_valid);
        assert_eq!(
            stalled.stream_accepted,
            q.clusters[1].stream_ready && stalled_d.clusters[1].stream_valid
        );
        assert_eq!(stalled_d.control.frame_beat, b6(5));

        let mut ready_q = q;
        ready_q.clusters[1].stream_ready = true;
        let (accepted, accepted_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            ready_q,
        );
        assert!(accepted.stream_ready);
        assert!(accepted.stream_accepted);
        assert!(accepted_d.clusters[1].stream_valid);
        assert_eq!(accepted_d.clusters[1].stream, stream);
        assert_eq!(
            accepted.stream_accepted,
            ready_q.clusters[1].stream_ready && accepted_d.clusters[1].stream_valid
        );
        assert_eq!(accepted_d.control.frame_beat, b6(6));
    }

    #[test]
    fn stream_offer_and_result_capture_coexist_on_independent_one_hot_fields() {
        let stream = VerifyStreamBeat {
            job_id: b32(0x4141_0004),
            ..VerifyStreamBeat::default()
        };
        let captured = VerifyResult {
            job_id: b32(0x4242_0004),
            verified: true,
            error: b3(VERIFY_ERROR_NONE),
        };
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[0].stream_ready = true;
        clusters[0].stream_context = b2(1);
        clusters[0].stream_generation = b8(5);
        clusters[2].result_valid = true;
        clusters[2].result = captured;
        let (output, d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            VerifierTopInput {
                stream_valid: true,
                stream,
                result_ready: false,
            },
            VerifierTopQ::<NativeLane> {
                clusters,
                control: VerifierTopControl {
                    admission_cursor: b2(0),
                    result_cursor: b2(2),
                    ..VerifierTopControl::default()
                },
                frame_job_id: b32(0),
                result: VerifyResult::default(),
            },
        );

        assert!(output.stream_accepted);
        assert!(d.clusters[0].stream_valid);
        assert!(!d.clusters[1].stream_valid);
        assert!(!d.clusters[2].stream_valid);
        assert!(!d.clusters[0].result_ready);
        assert!(!d.clusters[1].result_ready);
        assert!(d.clusters[2].result_ready);
        for cluster in d.clusters {
            assert_eq!(cluster.stream, stream);
        }
        assert!(d.control.result_valid);
        assert_eq!(d.control.result_cluster, b2(2));
        assert_eq!(d.result, captured);
    }

    #[test]
    #[allow(clippy::too_many_lines)] // Clean/fault/registered containment timeline.
    fn cluster_fault_containment_edge_accepts_beat_zero_exactly_once_then_broadcasts_abort() {
        let stream = VerifyStreamBeat {
            job_id: b32(0x4444_0004),
            ..VerifyStreamBeat::default()
        };
        let retained = VerifyResult {
            job_id: b32(0x5555_0005),
            verified: true,
            error: b3(VERIFY_ERROR_NONE),
        };
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[0].fault = true;
        clusters[0].diagnostics = b16(0x0020);
        clusters[1].stream_ready = true;
        clusters[1].stream_context = b2(2);
        clusters[1].stream_generation = b8(7);
        clusters[2].result_valid = true;
        clusters[2].result = VerifyResult {
            job_id: b32(0x5656_0005),
            verified: true,
            error: b3(VERIFY_ERROR_NONE),
        };
        let q = VerifierTopQ::<NativeLane> {
            clusters,
            control: VerifierTopControl {
                admission_cursor: b2(1),
                result_cursor: b2(2),
                result_valid: true,
                result_cluster: b2(2),
                ..VerifierTopControl::default()
            },
            frame_job_id: b32(0),
            result: retained,
        };
        let input = VerifierTopInput {
            stream_valid: true,
            stream,
            result_ready: true,
        };
        let mut clean_q = q;
        clean_q.clusters[0].fault = false;
        clean_q.clusters[0].diagnostics = b16(0);
        let (_, clean_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            clean_q,
        );
        let (containment, d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            input,
            q,
        );

        assert!(containment.fault);
        assert!(containment.stream_ready);
        assert!(containment.stream_accepted);
        assert_eq!(containment.stream_cluster, b2(1));
        assert_eq!(containment.stream_context, b2(2));
        assert_eq!(containment.stream_generation, b8(7));
        assert!(!containment.result_transfer);
        assert_eq!(containment.result.job_id, retained.job_id);
        assert_eq!(containment.result.error, b3(VERIFY_ERROR_TRANSPORT));
        assert!(d.clusters[1].stream_valid);
        assert_eq!(d.clusters[1].stream, stream);
        assert!(!d.clusters[0].stream_valid);
        assert!(!d.clusters[2].stream_valid);
        for (cluster, (faulted, clean)) in
            d.clusters.iter().zip(clean_d.clusters.iter()).enumerate()
        {
            assert_eq!(
                faulted.stream_valid, clean.stream_valid,
                "current fault contaminated cluster {cluster} stream offer"
            );
            assert_eq!(faulted.stream, stream);
        }
        assert!(clean_d.clusters[2].result_ready);
        for faulted in d.clusters {
            assert!(!faulted.result_ready);
        }
        assert!(d.control.poison);
        assert!(!d.control.frame_active);
        assert_eq!(d.frame_job_id, stream.job_id);

        let mut next_clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        for cluster in &mut next_clusters {
            cluster.stream_ready = true;
        }
        let (poisoned, poisoned_d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            VerifierTopInput {
                stream_valid: true,
                stream,
                result_ready: false,
            },
            VerifierTopQ::<NativeLane> {
                clusters: next_clusters,
                control: d.control,
                frame_job_id: d.frame_job_id,
                result: d.result,
            },
        );
        assert!(poisoned.fault);
        assert!(!poisoned.stream_ready);
        assert!(!poisoned.stream_accepted);
        for cluster in 0..VERIFY_TOP_CLUSTERS {
            assert!(poisoned_d.clusters[cluster].external_abort);
            assert!(!poisoned_d.clusters[cluster].stream_valid);
            assert!(!poisoned_d.clusters[cluster].result_ready);
        }
    }

    fn poisoned_drain_capture(
        error: b3,
        verified: bool,
    ) -> (VerifyResult, VerifierTopD<NativeLane>) {
        let mut clusters = [VerifyClusterOutput::default(); VERIFY_TOP_CLUSTERS];
        clusters[1].result_valid = true;
        clusters[1].result = VerifyResult {
            job_id: b32(0x6666_0006),
            verified,
            error,
        };
        let (output, d) = verifier_top_with_lane_kernel::<NativeLane>(
            clock_reset(clock(false), reset(false)),
            VerifierTopInput::default(),
            VerifierTopQ::<NativeLane> {
                clusters,
                control: VerifierTopControl {
                    result_cursor: b2(1),
                    poison: true,
                    drain_armed: true,
                    ..VerifierTopControl::default()
                },
                frame_job_id: b32(0),
                result: VerifyResult::default(),
            },
        );
        assert!(output.fault);
        assert!(!output.result_valid);
        assert!(d.control.result_valid);
        assert_eq!(d.control.result_cluster, b2(1));
        assert!(d.clusters[1].result_ready);
        assert!(!d.clusters[0].result_ready);
        assert!(!d.clusters[2].result_ready);
        (d.result, d)
    }

    #[test]
    fn poisoned_drain_grant_is_payload_independent_and_capture_fails_closed() {
        let (clean, _) = poisoned_drain_capture(b3(VERIFY_ERROR_NONE), true);
        assert_eq!(clean.job_id, b32(0x6666_0006));
        assert!(!clean.verified);
        assert_eq!(clean.error, b3(VERIFY_ERROR_TRANSPORT));

        let (frame, _) = poisoned_drain_capture(b3(VERIFY_ERROR_FRAME), false);
        assert_eq!(frame.job_id, b32(0x6666_0006));
        assert!(!frame.verified);
        assert_eq!(frame.error, b3(VERIFY_ERROR_FRAME));
    }
}