wots_rhdl/verify/
cluster.rs

1//! Four-context SHA-256 verifier cluster with fail-closed lane ownership.
2//!
3//! [`VerifyClusterCore`] keeps the compression lane injectable: it exposes one
4//! prepared lane request and consumes one exact-latency lane response. This is
5//! the focused behavioral-test boundary. [`VerifierCluster`] closes that
6//! boundary around one lane implementing the shared
7//! [`CompressionLaneComponent`] contract; nested `SynchronousDQ` connectivity
8//! adds no protocol register.
9//!
10//! Beat zero is fairly allocated from registered idle state and locks one
11//! physical context for exactly 35 accepted beats. Keep, last, and job-ID
12//! defects remain per-job framing errors inside that context; they never poison
13//! the cluster. Generations have separate assigned and next values so beat zero
14//! increments the reuse counter immediately while every beat and task of the
15//! accepted job continues to use its original assignment.
16//!
17//! Results cross a one-entry registered elastic slot. Capturing a child result
18//! releases that child before external delivery, and a transferring slot may be
19//! replaced on the same edge. The first fatal edge suppresses transfer and turns
20//! an already-retained clean slot into an identified transport error before that
21//! slot can transfer. Transport, child audit, or ownership failures set
22//! reset-only cluster poison. The registered poison aborts every live context on
23//! the following cycle and prevents all later frame admission, lane launch, and
24//! response routing until shared reset. Already-retained error completions may
25//! still drain so software is not left waiting without an identity.
26//!
27//! A child response rejection is a containment-edge exception to ordinary
28//! ready/fault intuition. Its exact response must first be physically presented,
29//! so same-cycle stream credit cannot depend on the rejection without forming a
30//! hierarchy loop. One already-advertised beat may therefore transfer while
31//! `fault` rises. That beat is reported accepted, delivered to the selected
32//! child, and retains its job identity; registered poison aborts it on the next
33//! cycle. Result transfer and capture are still suppressed immediately.
34//! Context stream, response, result-grant, generation, and abort fields are
35//! constructed as four direct child literals. No dynamically mutated aggregate
36//! can couple one protocol's fault dependency into another protocol field.
37//!
38//! `external_abort` is a registered-parent transition command. On its command
39//! edge it changes only cluster D state: poison and its diagnostic are latched,
40//! and any frame lock is cleared. It deliberately has no combinational effect
41//! on stream, lane, response, result, fault, or diagnostic outputs. The parent
42//! must therefore issue it only after withdrawing this cluster's stream valid
43//! and result ready. Registered local poison provides complete containment on
44//! the following cycle; at most one lane launch and one routed return per peer
45//! may advance on the transition edge, and one internal result capture may also
46//! occur. All belong to already-accepted jobs.
47//!
48//! The implementation has source and behavioral-simulation evidence only. It
49//! makes no emitted-RTL, synthesis, resource, timing, route, or hardware claim.
50
51use rhdl::{core::ReplicatedSynchronous, prelude::*};
52use rhdl_fpga::core::dff::DFF;
53use rhdl_primitives::NoResetDff;
54use sha256_rhdl::lane::{
55    CompressionInput, CompressionOutput, ExternalFullCompressionLane, InlineCompressionLane,
56};
57
58use crate::{
59    cluster::CompressionLaneComponent,
60    verify::{
61        framing::VerifyStreamBeat,
62        sha::{
63            VERIFY_ERROR_NONE, VERIFY_ERROR_TRANSPORT, VerifyContextInput, VerifySingleContextSha,
64        },
65        transport::{
66            VERIFY_CLUSTER_CONTEXTS, VerifyTransport, VerifyTransportInput, VerifyTransportOutput,
67        },
68    },
69};
70
71/// A child rejected a response that passed the cluster's expected-tag gate.
72pub const VERIFY_DIAGNOSTIC_CHILD_RESPONSE_REJECT: u128 = 1 << 5;
73/// A child latched a transport or final-accounting fault.
74pub const VERIFY_DIAGNOSTIC_CHILD_FAULT: u128 = 1 << 6;
75/// Registered frame ownership disagreed with child loading state.
76pub const VERIFY_DIAGNOSTIC_OWNERSHIP: u128 = 1 << 7;
77/// A registered parent requested cluster-wide transport abort.
78pub const VERIFY_DIAGNOSTIC_EXTERNAL_ABORT: u128 = 1 << 8;
79
80const _: () = {
81    assert!(VERIFY_CLUSTER_CONTEXTS == 4);
82};
83
84/// One registered verifier result.
85#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
86pub struct VerifyResult {
87    /// Opaque job identity captured from input beat zero.
88    pub job_id: b32,
89    /// Cryptographic decision; false for every nonzero error.
90    pub verified: bool,
91    /// Context-defined three-bit completion code.
92    pub error: b3,
93}
94
95/// External streaming interface for the production verifier cluster.
96#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
97pub struct VerifyClusterInput {
98    /// One 512-bit verifier input beat is present.
99    pub stream_valid: bool,
100    /// Signature, public-key, and message bytes plus sideband.
101    pub stream: VerifyStreamBeat,
102    /// Consumer accepts the registered result slot.
103    pub result_ready: bool,
104    /// Registered-parent poison transition that aborts every accepted job.
105    ///
106    /// This signal must come from parent state, never from a combinational
107    /// union of sibling outputs. That restriction prevents a peer-fault
108    /// broadcast from forming a hierarchy-wide fixed point. The parent must
109    /// also withdraw `stream_valid` and `result_ready` before asserting it;
110    /// command-edge output behavior intentionally remains independent of this
111    /// input, and registered local poison contains the cluster one cycle later.
112    pub external_abort: bool,
113}
114
115/// Injectable-core input, adding the shared lane's combinational output.
116#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
117pub struct VerifyClusterCoreInput {
118    /// One 512-bit verifier input beat is present.
119    pub stream_valid: bool,
120    /// Signature, public-key, and message bytes plus sideband.
121    pub stream: VerifyStreamBeat,
122    /// Consumer accepts the registered result slot.
123    pub result_ready: bool,
124    /// Response from an exact-64-cycle tag-preserving compression lane.
125    pub lane_response: CompressionOutput,
126    /// Registered parent poison, with the same contract as
127    /// [`VerifyClusterInput::external_abort`].
128    pub external_abort: bool,
129}
130
131/// Cluster status, diagnostics, injectable lane request, and registered result.
132#[allow(clippy::struct_excessive_bools)] // Independent protocol and audit wires.
133#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
134pub struct VerifyClusterOutput {
135    /// The presented input beat may transfer.
136    pub stream_ready: bool,
137    /// One input beat transferred in this cycle.
138    pub stream_accepted: bool,
139    /// Physical context owning or selected for this transfer.
140    pub stream_context: b2,
141    /// Generation assigned to the owning job.
142    pub stream_generation: b8,
143    /// A 35-beat frame currently owns one physical context.
144    pub frame_active: bool,
145    /// Next fixed beat index for the owning frame.
146    pub frame_beat: b6,
147    /// Beat-zero identity retained for ownership diagnostics.
148    pub frame_job_id: b32,
149    /// Prepared token or bubble for the injectable/shared lane.
150    pub lane_request: CompressionInput,
151    /// Per-context actual lane-launch handshakes.
152    pub request_accepted: [bool; VERIFY_CLUSTER_CONTEXTS],
153    /// Per-context noncanonical or changed held requests.
154    pub request_rejected: [bool; VERIFY_CLUSTER_CONTEXTS],
155    /// Per-context accepted-route diagnostics.
156    ///
157    /// This reports the transport's exact tag route. A child may still reject
158    /// that physically presented candidate; inspect
159    /// [`VerifyClusterOutput::context_response_rejected`] separately.
160    pub response_routed: [bool; VERIFY_CLUSTER_CONTEXTS],
161    /// Child response-acceptance pulses after local dependency validation.
162    pub context_response_ready: [bool; VERIFY_CLUSTER_CONTEXTS],
163    /// Child local response-rejection pulses.
164    pub context_response_rejected: [bool; VERIFY_CLUSTER_CONTEXTS],
165    /// Child frame loaders currently active.
166    pub context_loading: [bool; VERIFY_CLUSTER_CONTEXTS],
167    /// Child cryptographic task graphs currently active.
168    pub context_active: [bool; VERIFY_CLUSTER_CONTEXTS],
169    /// Child retained results awaiting cluster capture.
170    pub context_result_valid: [bool; VERIFY_CLUSTER_CONTEXTS],
171    /// Child reset-only transport/audit faults.
172    pub context_fault: [bool; VERIFY_CLUSTER_CONTEXTS],
173    /// Child accepted-request counts for transport diagnostics.
174    pub context_total_issued: [b11; VERIFY_CLUSTER_CONTEXTS],
175    /// Child accepted-response counts for transport diagnostics.
176    pub context_total_retired: [b11; VERIFY_CLUSTER_CONTEXTS],
177    /// One registered result is available.
178    pub result_valid: bool,
179    /// Registered result, stable while stalled except for fail-closed conversion
180    /// of a clean completion on the first fatal edge.
181    pub result: VerifyResult,
182    /// The registered result transferred in this cycle; always false on the
183    /// first fatal edge.
184    pub result_transfer: bool,
185    /// Immediate local fatal or registered cluster poison.
186    ///
187    /// A parent `external_abort` command is not echoed combinationally through
188    /// this field; it becomes visible from registered local poison on the next
189    /// cycle. Command-edge datapath and result outputs are likewise unchanged.
190    pub fault: bool,
191    /// Sticky diagnostic cause mask, cleared only by shared reset.
192    pub diagnostics: b16,
193}
194
195/// Narrow resettable ownership, result, and poison state.
196#[allow(clippy::struct_excessive_bools)] // Each bit has an independent protocol role.
197#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
198pub struct VerifyClusterControl {
199    /// Rotating beat-zero allocation cursor.
200    pub allocation_cursor: b2,
201    /// One context owns the current 35-beat frame.
202    pub frame_active: bool,
203    /// Physical owner of the current frame.
204    pub frame_owner: b2,
205    /// Next beat index expected for the current frame.
206    pub frame_beat: b6,
207    /// Rotating retained-result capture cursor.
208    pub result_cursor: b2,
209    /// One registered result occupies the external elastic slot.
210    pub result_valid: bool,
211    /// Sticky cluster-wide transport poison.
212    pub poison: bool,
213    /// Sticky diagnostic causes corresponding to `poison`.
214    pub diagnostics: b16,
215}
216
217/// Fair four-way context selection.
218#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
219pub struct VerifyClusterSelection {
220    /// At least one eligible context was found.
221    pub valid: bool,
222    /// Selected physical context.
223    pub context: b2,
224    /// Cursor following the selected context.
225    pub next_cursor: b2,
226}
227
228/// Inputs to the independent-fatal transport gate.
229#[allow(clippy::struct_excessive_bools)] // Independent reset and fatal causes.
230#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
231pub struct VerifyClusterTransportGateInput {
232    /// Current transport launch and response decision.
233    pub transport: VerifyTransportOutput,
234    /// Shared reset is asserted.
235    pub resetting: bool,
236    /// Registered cluster poison is already active.
237    pub poisoned: bool,
238    /// Transport, ownership, or registered-child fault independent of response delivery.
239    pub independent_fatal: bool,
240}
241
242/// Actual launch, acknowledgement, and response signals after fatal gating.
243#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
244pub struct VerifyClusterTransportGateOutput {
245    /// Token or bubble actually delivered to the lane.
246    pub lane_request: CompressionInput,
247    /// Actual per-context launch acknowledgements.
248    pub request_accepted: [bool; VERIFY_CLUSTER_CONTEXTS],
249    /// Candidate responses physically presented to contexts.
250    pub responses: [CompressionOutput; VERIFY_CLUSTER_CONTEXTS],
251    /// Transport-approved route diagnostics.
252    pub response_routed: [bool; VERIFY_CLUSTER_CONTEXTS],
253}
254
255/// Gate transport effects for causes independent of a child's current response.
256///
257/// Current child rejection is intentionally absent from this input. It depends
258/// on the physically presented response and therefore cannot be allowed to
259/// retract that response or the same-cycle lane decision.
260#[kernel]
261pub fn verify_cluster_transport_gate_kernel(
262    input: VerifyClusterTransportGateInput,
263) -> VerifyClusterTransportGateOutput {
264    let response_delivery_enabled = !input.resetting && !input.poisoned && !input.independent_fatal;
265    VerifyClusterTransportGateOutput {
266        lane_request: if response_delivery_enabled {
267            input.transport.lane_request
268        } else {
269            CompressionInput::default()
270        },
271        request_accepted: if response_delivery_enabled {
272            input.transport.request_accepted
273        } else {
274            [false; VERIFY_CLUSTER_CONTEXTS]
275        },
276        responses: if response_delivery_enabled {
277            input.transport.responses
278        } else {
279            [CompressionOutput::default(); VERIFY_CLUSTER_CONTEXTS]
280        },
281        response_routed: if response_delivery_enabled {
282            input.transport.response_routed
283        } else {
284            [false; VERIFY_CLUSTER_CONTEXTS]
285        },
286    }
287}
288
289/// Select one of four eligible contexts with rotating fairness.
290#[kernel]
291#[allow(clippy::assign_op_pattern)] // Compound assignment is not lowered by pinned RHDL.
292pub fn select_verify_cluster_context_kernel(
293    eligible: [bool; VERIFY_CLUSTER_CONTEXTS],
294    cursor: b2,
295) -> VerifyClusterSelection {
296    let mut selection = VerifyClusterSelection {
297        next_cursor: cursor,
298        ..VerifyClusterSelection::default()
299    };
300    let mut scan = cursor;
301    for _offset in 0..VERIFY_CLUSTER_CONTEXTS {
302        if !selection.valid && eligible[scan] {
303            selection.valid = true;
304            selection.context = scan;
305            selection.next_cursor = scan + b2(1);
306        }
307        scan = scan + b2(1);
308    }
309    selection
310}
311
312/// Four verifier contexts plus transport, with the compression lane injectable.
313#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
314pub struct VerifyClusterCore {
315    contexts: ReplicatedSynchronous<VerifySingleContextSha, VERIFY_CLUSTER_CONTEXTS>,
316    transport: VerifyTransport,
317    control: DFF<VerifyClusterControl>,
318    assigned_generations: DFF<[b8; VERIFY_CLUSTER_CONTEXTS]>,
319    next_generations: DFF<[b8; VERIFY_CLUSTER_CONTEXTS]>,
320    frame_job_id: NoResetDff<b32>,
321    result: NoResetDff<VerifyResult>,
322}
323
324impl Default for VerifyClusterCore {
325    fn default() -> Self {
326        Self {
327            contexts: ReplicatedSynchronous::new(VerifySingleContextSha::default()),
328            transport: VerifyTransport::default(),
329            control: DFF::new(VerifyClusterControl::default()),
330            assigned_generations: DFF::new([b8(0); VERIFY_CLUSTER_CONTEXTS]),
331            next_generations: DFF::new([b8(0); VERIFY_CLUSTER_CONTEXTS]),
332            frame_job_id: NoResetDff::new(),
333            result: NoResetDff::new(),
334        }
335    }
336}
337
338impl SynchronousIO for VerifyClusterCore {
339    type I = VerifyClusterCoreInput;
340    type O = VerifyClusterOutput;
341    type Kernel = verify_cluster_core_kernel;
342}
343
344/// Frame ownership, poison, result elasticity, and child/transport connectivity.
345#[kernel]
346#[allow(clippy::assign_op_pattern, clippy::needless_range_loop)] // Iterators/compound assignments are not lowered by pinned RHDL.
347pub fn verify_cluster_core_kernel(
348    clock_reset: ClockReset,
349    input: VerifyClusterCoreInput,
350    q: VerifyClusterCoreQ,
351) -> (VerifyClusterOutput, VerifyClusterCoreD) {
352    let resetting = clock_reset.reset.any();
353    let loading = [
354        q.contexts[0].loading,
355        q.contexts[1].loading,
356        q.contexts[2].loading,
357        q.contexts[3].loading,
358    ];
359    let active = [
360        q.contexts[0].active,
361        q.contexts[1].active,
362        q.contexts[2].active,
363        q.contexts[3].active,
364    ];
365    let child_results = [
366        q.contexts[0].result_valid,
367        q.contexts[1].result_valid,
368        q.contexts[2].result_valid,
369        q.contexts[3].result_valid,
370    ];
371    let child_faults = [
372        q.contexts[0].fault,
373        q.contexts[1].fault,
374        q.contexts[2].fault,
375        q.contexts[3].fault,
376    ];
377    let child_latched_faults = [
378        q.contexts[0].fault_latched,
379        q.contexts[1].fault_latched,
380        q.contexts[2].fault_latched,
381        q.contexts[3].fault_latched,
382    ];
383    let child_response_rejected = q.contexts[0].response_rejected
384        || q.contexts[1].response_rejected
385        || q.contexts[2].response_rejected
386        || q.contexts[3].response_rejected;
387    let child_fault = child_latched_faults[0]
388        || child_latched_faults[1]
389        || child_latched_faults[2]
390        || child_latched_faults[3];
391
392    let owner_loading = match q.control.frame_owner {
393        Bits::<2>(0) => loading[0] && !loading[1] && !loading[2] && !loading[3],
394        Bits::<2>(1) => !loading[0] && loading[1] && !loading[2] && !loading[3],
395        Bits::<2>(2) => !loading[0] && !loading[1] && loading[2] && !loading[3],
396        _ => !loading[0] && !loading[1] && !loading[2] && loading[3],
397    };
398    let any_loading = loading[0] || loading[1] || loading[2] || loading[3];
399    let ownership_fault = !q.control.poison
400        && ((q.control.frame_active && !owner_loading) || (!q.control.frame_active && any_loading));
401
402    let mut local_diagnostic_now = q.transport.diagnostics;
403    if child_response_rejected {
404        local_diagnostic_now = local_diagnostic_now | b16(VERIFY_DIAGNOSTIC_CHILD_RESPONSE_REJECT);
405    }
406    if child_fault {
407        local_diagnostic_now = local_diagnostic_now | b16(VERIFY_DIAGNOSTIC_CHILD_FAULT);
408    }
409    if ownership_fault {
410        local_diagnostic_now = local_diagnostic_now | b16(VERIFY_DIAGNOSTIC_OWNERSHIP);
411    }
412    let external_abort_transition = !resetting && !q.control.poison && input.external_abort;
413    let mut transition_diagnostic_now = local_diagnostic_now;
414    if external_abort_transition {
415        transition_diagnostic_now =
416            transition_diagnostic_now | b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT);
417    }
418    let local_independent_fatal_now =
419        !resetting && !q.control.poison && (q.transport.fatal || child_fault || ownership_fault);
420    let local_fatal_now = local_independent_fatal_now || (!resetting && child_response_rejected);
421    let poison_transition_now = local_fatal_now || external_abort_transition;
422    // A child rejection depends on seeing the exact transport-approved
423    // response. Keep response presentation and the current lane decision
424    // independent of that observation so neither signal feeds its own
425    // rejection predicate. The child terminal path suppresses all writes.
426    // Immediate result effects still use `local_fatal_now`; registered poison
427    // invalidates transport ownership and ignores any bounded later return from
428    // an unrelated token accepted on this containment edge.
429    let transport_gate = verify_cluster_transport_gate_kernel(VerifyClusterTransportGateInput {
430        transport: q.transport,
431        resetting,
432        poisoned: q.control.poison,
433        independent_fatal: local_independent_fatal_now,
434    });
435
436    // Allocation eligibility must use registered child fault state. A child's
437    // public `fault` deliberately has an immediate local-transport
438    // view; using it here would feed registered cluster poison back through
439    // `transport_abort -> child fault -> idle -> stream` during hierarchy
440    // lowering. Independent fatal causes still block same-cycle admission;
441    // registered `fault_latched` prevents reuse on every later edge.
442    let idle = [
443        !loading[0] && !active[0] && !child_results[0] && !child_latched_faults[0],
444        !loading[1] && !active[1] && !child_results[1] && !child_latched_faults[1],
445        !loading[2] && !active[2] && !child_results[2] && !child_latched_faults[2],
446        !loading[3] && !active[3] && !child_results[3] && !child_latched_faults[3],
447    ];
448    let allocation = select_verify_cluster_context_kernel(idle, q.control.allocation_cursor);
449    let selected_context = if q.control.frame_active {
450        q.control.frame_owner
451    } else {
452        allocation.context
453    };
454    let selected_generation = if q.control.frame_active {
455        match q.control.frame_owner {
456            Bits::<2>(0) => q.assigned_generations[0],
457            Bits::<2>(1) => q.assigned_generations[1],
458            Bits::<2>(2) => q.assigned_generations[2],
459            _ => q.assigned_generations[3],
460        }
461    } else {
462        match allocation.context {
463            Bits::<2>(0) => q.next_generations[0],
464            Bits::<2>(1) => q.next_generations[1],
465            Bits::<2>(2) => q.next_generations[2],
466            _ => q.next_generations[3],
467        }
468    };
469    let frame_ready = if q.control.frame_active {
470        owner_loading
471    } else {
472        allocation.valid
473    };
474    // Do not retract already-advertised credit from the combinational child
475    // rejection that observing this edge's response may itself produce. The
476    // accepted beat is delivered below and becomes part of the identified job;
477    // registered poison removes credit and aborts the job on the next cycle.
478    let stream_ready =
479        !resetting && !q.control.poison && !local_independent_fatal_now && frame_ready;
480    let stream_accepted = stream_ready && input.stream_valid;
481
482    let result_transfer =
483        !resetting && !local_fatal_now && q.control.result_valid && input.result_ready;
484    let result_slot_available = !q.control.result_valid || result_transfer;
485    let child_errors = [
486        q.contexts[0].error,
487        q.contexts[1].error,
488        q.contexts[2].error,
489        q.contexts[3].error,
490    ];
491    // On the first registered-poison cycle, a clean retained child exposes a
492    // combinational TRANSPORT view but terminal precedence prevents it from
493    // honoring result_ready. Wait until fault_latched proves the conversion is
494    // registered. Organic transport failures obey the same acknowledgement
495    // rule; FRAME remains eligible because it is not transport poison.
496    let child_result_committed = [
497        child_errors[0] != b3(VERIFY_ERROR_TRANSPORT) || child_latched_faults[0],
498        child_errors[1] != b3(VERIFY_ERROR_TRANSPORT) || child_latched_faults[1],
499        child_errors[2] != b3(VERIFY_ERROR_TRANSPORT) || child_latched_faults[2],
500        child_errors[3] != b3(VERIFY_ERROR_TRANSPORT) || child_latched_faults[3],
501    ];
502    let result_eligible = [
503        child_results[0]
504            && (!q.control.poison || child_errors[0] != b3(VERIFY_ERROR_NONE))
505            && child_result_committed[0],
506        child_results[1]
507            && (!q.control.poison || child_errors[1] != b3(VERIFY_ERROR_NONE))
508            && child_result_committed[1],
509        child_results[2]
510            && (!q.control.poison || child_errors[2] != b3(VERIFY_ERROR_NONE))
511            && child_result_committed[2],
512        child_results[3]
513            && (!q.control.poison || child_errors[3] != b3(VERIFY_ERROR_NONE))
514            && child_result_committed[3],
515    ];
516    let result_selection =
517        select_verify_cluster_context_kernel(result_eligible, q.control.result_cursor);
518    let capture_result =
519        !resetting && !local_fatal_now && result_slot_available && result_selection.valid;
520    let selected_result_job_id = match result_selection.context {
521        Bits::<2>(0) => q.contexts[0].result_job_id,
522        Bits::<2>(1) => q.contexts[1].result_job_id,
523        Bits::<2>(2) => q.contexts[2].result_job_id,
524        _ => q.contexts[3].result_job_id,
525    };
526    let selected_result_verified = match result_selection.context {
527        Bits::<2>(0) => q.contexts[0].verified,
528        Bits::<2>(1) => q.contexts[1].verified,
529        Bits::<2>(2) => q.contexts[2].verified,
530        _ => q.contexts[3].verified,
531    };
532    let selected_result_error = match result_selection.context {
533        Bits::<2>(0) => q.contexts[0].error,
534        Bits::<2>(1) => q.contexts[1].error,
535        Bits::<2>(2) => q.contexts[2].error,
536        _ => q.contexts[3].error,
537    };
538    let context_0_result_ready = capture_result && result_selection.context == b2(0);
539    let context_1_result_ready = capture_result && result_selection.context == b2(1);
540    let context_2_result_ready = capture_result && result_selection.context == b2(2);
541    let context_3_result_ready = capture_result && result_selection.context == b2(3);
542
543    let mut control = q.control;
544    let mut assigned_generations = q.assigned_generations;
545    let mut next_generations = q.next_generations;
546    let mut frame_job_id = q.frame_job_id;
547    let mut result = q.result;
548    let abort_clean_result = !resetting
549        && (local_fatal_now || q.control.poison)
550        && q.control.result_valid
551        && q.result.error == b3(VERIFY_ERROR_NONE);
552    let mut visible_result = q.result;
553
554    if abort_clean_result {
555        visible_result = VerifyResult {
556            job_id: q.result.job_id,
557            verified: false,
558            error: b3(VERIFY_ERROR_TRANSPORT),
559        };
560        result = visible_result;
561    }
562
563    if result_transfer {
564        control.result_valid = false;
565    }
566    if capture_result {
567        result = VerifyResult {
568            job_id: selected_result_job_id,
569            verified: selected_result_error == b3(VERIFY_ERROR_NONE) && selected_result_verified,
570            error: selected_result_error,
571        };
572        control.result_valid = true;
573        control.result_cursor = result_selection.next_cursor;
574    }
575
576    if stream_accepted {
577        if q.control.frame_active {
578            if q.control.frame_beat == b6(34) {
579                control.frame_active = false;
580                control.frame_beat = b6(0);
581            } else {
582                control.frame_beat = q.control.frame_beat + b6(1);
583            }
584        } else {
585            control.frame_active = true;
586            control.frame_owner = allocation.context;
587            control.frame_beat = b6(1);
588            control.allocation_cursor = allocation.next_cursor;
589            assigned_generations[allocation.context] = q.next_generations[allocation.context];
590            next_generations[allocation.context] = q.next_generations[allocation.context] + b8(1);
591            frame_job_id = input.stream.job_id;
592        }
593    }
594
595    if poison_transition_now {
596        control.poison = true;
597        control.frame_active = false;
598        control.frame_beat = b6(0);
599        control.diagnostics = q.control.diagnostics | transition_diagnostic_now;
600    }
601    if resetting {
602        control = VerifyClusterControl::default();
603        assigned_generations = [b8(0); VERIFY_CLUSTER_CONTEXTS];
604        next_generations = [b8(0); VERIFY_CLUSTER_CONTEXTS];
605    }
606
607    // As at the three-cluster boundary, every child protocol field is built
608    // directly. Dynamic mutation of one context aggregate would conservatively
609    // couple fault-dependent result grants to response and stream fields during
610    // RHDL lowering.
611    let context_0_stream_valid = stream_accepted && selected_context == b2(0);
612    let context_1_stream_valid = stream_accepted && selected_context == b2(1);
613    let context_2_stream_valid = stream_accepted && selected_context == b2(2);
614    let context_3_stream_valid = stream_accepted && selected_context == b2(3);
615    let context_0_generation = if context_0_stream_valid {
616        selected_generation
617    } else {
618        q.assigned_generations[0]
619    };
620    let context_1_generation = if context_1_stream_valid {
621        selected_generation
622    } else {
623        q.assigned_generations[1]
624    };
625    let context_2_generation = if context_2_stream_valid {
626        selected_generation
627    } else {
628        q.assigned_generations[2]
629    };
630    let context_3_generation = if context_3_stream_valid {
631        selected_generation
632    } else {
633        q.assigned_generations[3]
634    };
635    // A parent abort first latches `control.poison`; only that registered state
636    // reaches child contexts. Feeding `input.external_abort` here would create a
637    // parent-abort -> child-fault -> parent-fault hierarchy loop even though the
638    // behavioral intent is edge ordered.
639    let context_transport_abort = !resetting && q.control.poison;
640    let context_inputs = [
641        VerifyContextInput {
642            stream_valid: context_0_stream_valid,
643            stream: input.stream,
644            context: b4(0),
645            context_enabled: true,
646            generation: context_0_generation,
647            request_ready: transport_gate.request_accepted[0],
648            response: transport_gate.responses[0],
649            result_ready: context_0_result_ready,
650            transport_abort: context_transport_abort,
651        },
652        VerifyContextInput {
653            stream_valid: context_1_stream_valid,
654            stream: input.stream,
655            context: b4(1),
656            context_enabled: true,
657            generation: context_1_generation,
658            request_ready: transport_gate.request_accepted[1],
659            response: transport_gate.responses[1],
660            result_ready: context_1_result_ready,
661            transport_abort: context_transport_abort,
662        },
663        VerifyContextInput {
664            stream_valid: context_2_stream_valid,
665            stream: input.stream,
666            context: b4(2),
667            context_enabled: true,
668            generation: context_2_generation,
669            request_ready: transport_gate.request_accepted[2],
670            response: transport_gate.responses[2],
671            result_ready: context_2_result_ready,
672            transport_abort: context_transport_abort,
673        },
674        VerifyContextInput {
675            stream_valid: context_3_stream_valid,
676            stream: input.stream,
677            context: b4(3),
678            context_enabled: true,
679            generation: context_3_generation,
680            request_ready: transport_gate.request_accepted[3],
681            response: transport_gate.responses[3],
682            result_ready: context_3_result_ready,
683            transport_abort: context_transport_abort,
684        },
685    ];
686
687    let output = VerifyClusterOutput {
688        stream_ready,
689        stream_accepted,
690        stream_context: selected_context,
691        stream_generation: selected_generation,
692        frame_active: !resetting && q.control.frame_active,
693        frame_beat: q.control.frame_beat,
694        frame_job_id: q.frame_job_id,
695        lane_request: transport_gate.lane_request,
696        request_accepted: transport_gate.request_accepted,
697        request_rejected: if resetting || q.control.poison {
698            [false; VERIFY_CLUSTER_CONTEXTS]
699        } else {
700            q.transport.request_rejected
701        },
702        response_routed: transport_gate.response_routed,
703        context_response_ready: if resetting {
704            [false; VERIFY_CLUSTER_CONTEXTS]
705        } else {
706            [
707                q.contexts[0].response_ready,
708                q.contexts[1].response_ready,
709                q.contexts[2].response_ready,
710                q.contexts[3].response_ready,
711            ]
712        },
713        context_response_rejected: if resetting {
714            [false; VERIFY_CLUSTER_CONTEXTS]
715        } else {
716            [
717                q.contexts[0].response_rejected,
718                q.contexts[1].response_rejected,
719                q.contexts[2].response_rejected,
720                q.contexts[3].response_rejected,
721            ]
722        },
723        context_loading: if resetting {
724            [false; VERIFY_CLUSTER_CONTEXTS]
725        } else {
726            loading
727        },
728        context_active: if resetting {
729            [false; VERIFY_CLUSTER_CONTEXTS]
730        } else {
731            active
732        },
733        context_result_valid: if resetting {
734            [false; VERIFY_CLUSTER_CONTEXTS]
735        } else {
736            child_results
737        },
738        context_fault: if resetting {
739            [false; VERIFY_CLUSTER_CONTEXTS]
740        } else {
741            child_faults
742        },
743        context_total_issued: if resetting {
744            [b11(0); VERIFY_CLUSTER_CONTEXTS]
745        } else {
746            [
747                q.contexts[0].total_issued,
748                q.contexts[1].total_issued,
749                q.contexts[2].total_issued,
750                q.contexts[3].total_issued,
751            ]
752        },
753        context_total_retired: if resetting {
754            [b11(0); VERIFY_CLUSTER_CONTEXTS]
755        } else {
756            [
757                q.contexts[0].total_retired,
758                q.contexts[1].total_retired,
759                q.contexts[2].total_retired,
760                q.contexts[3].total_retired,
761            ]
762        },
763        result_valid: !resetting && q.control.result_valid,
764        result: visible_result,
765        result_transfer,
766        fault: !resetting && (q.control.poison || local_fatal_now),
767        diagnostics: if resetting {
768            b16(0)
769        } else {
770            q.control.diagnostics | local_diagnostic_now
771        },
772    };
773    let d = VerifyClusterCoreD {
774        contexts: context_inputs,
775        transport: VerifyTransportInput {
776            requests: [
777                q.contexts[0].transport_request,
778                q.contexts[1].transport_request,
779                q.contexts[2].transport_request,
780                q.contexts[3].transport_request,
781            ],
782            assigned_generations: q.assigned_generations,
783            lane_response: input.lane_response,
784            // As with the contexts, the transport observes only registered
785            // local poison. The external input is a transition cause, not a
786            // combinational fanout into child status.
787            abort: !resetting && q.control.poison,
788        },
789        control,
790        assigned_generations,
791        next_generations,
792        frame_job_id,
793        result,
794    };
795    (output, d)
796}
797
798/// Four verifier contexts behind one injected exact-64-cycle compression lane.
799///
800/// The lane remains a direct child of this ordinary derived parent. That
801/// hierarchy is required by the typed external-netlist path: a top may
802/// replicate this complete cluster, but must never replicate an unresolved
803/// external leaf directly.
804#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
805pub struct VerifierCluster<L = InlineCompressionLane<64, 6>>
806where
807    L: CompressionLaneComponent,
808{
809    core: VerifyClusterCore,
810    lane: L,
811}
812
813impl<L> Default for VerifierCluster<L>
814where
815    L: CompressionLaneComponent + Default,
816{
817    fn default() -> Self {
818        Self {
819            core: VerifyClusterCore::default(),
820            lane: L::default(),
821        }
822    }
823}
824
825impl<L> SynchronousIO for VerifierCluster<L>
826where
827    L: CompressionLaneComponent,
828{
829    type I = VerifyClusterInput;
830    type O = VerifyClusterOutput;
831    type Kernel = verifier_cluster_with_lane_kernel<L>;
832}
833
834/// Close the injectable core around one exact-64-cycle compression lane.
835#[kernel]
836pub fn verifier_cluster_with_lane_kernel<L: CompressionLaneComponent>(
837    clock_reset: ClockReset,
838    input: VerifyClusterInput,
839    q: VerifierClusterQ<L>,
840) -> (VerifyClusterOutput, VerifierClusterD<L>) {
841    let _ = clock_reset;
842    let d = VerifierClusterD::<L> {
843        core: VerifyClusterCoreInput {
844            stream_valid: input.stream_valid,
845            stream: input.stream,
846            result_ready: input.result_ready,
847            lane_response: q.lane,
848            external_abort: input.external_abort,
849        },
850        lane: q.core.lane_request,
851    };
852    (q.core, d)
853}
854
855/// Production four-context verifier cluster with one inline full SHA-256 lane.
856pub type Sha256VerifierCluster = VerifierCluster<InlineCompressionLane<64, 6>>;
857
858/// Production verifier cluster linked to a separately generated full SHA lane.
859///
860/// Behavioral simulation remains identical to [`Sha256VerifierCluster`]. The
861/// emitted hierarchy intentionally leaves `sha256_compression_lane` unresolved
862/// until the separately generated RHDL lane artifact is supplied.
863pub type ModularSha256VerifierCluster = VerifierCluster<ExternalFullCompressionLane>;
864
865/// Native-lane wrapper retained for callers of the original free kernel API.
866#[kernel]
867pub fn sha256_verifier_cluster_kernel(
868    clock_reset: ClockReset,
869    input: VerifyClusterInput,
870    q: VerifierClusterQ<InlineCompressionLane<64, 6>>,
871) -> (
872    VerifyClusterOutput,
873    VerifierClusterD<InlineCompressionLane<64, 6>>,
874) {
875    verifier_cluster_with_lane_kernel::<InlineCompressionLane<64, 6>>(clock_reset, input, q)
876}
877
878#[cfg(test)]
879mod tests {
880    use super::*;
881    use crate::verify::sha::VerifyContextOutput;
882
883    fn rejection_q(frame_active: bool) -> VerifyClusterCoreQ {
884        let mut contexts = [VerifyContextOutput::default(); VERIFY_CLUSTER_CONTEXTS];
885        contexts[3].response_rejected = true;
886        contexts[3].fault = true;
887        if frame_active {
888            contexts[1].loading = true;
889        }
890        VerifyClusterCoreQ {
891            contexts,
892            transport: VerifyTransportOutput {
893                lane_request: CompressionInput {
894                    tag: b32(0x1234_5678),
895                    valid: true,
896                    ..CompressionInput::default()
897                },
898                request_accepted: [true, false, false, false],
899                response_routed: [false, false, false, true],
900                ..VerifyTransportOutput::default()
901            },
902            control: VerifyClusterControl {
903                frame_active,
904                frame_owner: b2(1),
905                frame_beat: if frame_active { b6(7) } else { b6(0) },
906                result_valid: true,
907                ..VerifyClusterControl::default()
908            },
909            assigned_generations: [b8(0), b8(5), b8(0), b8(0)],
910            next_generations: [b8(0); VERIFY_CLUSTER_CONTEXTS],
911            frame_job_id: b32(0x6000_0001),
912            result: VerifyResult {
913                job_id: b32(0x5fff_0001),
914                verified: true,
915                error: b3(VERIFY_ERROR_NONE),
916            },
917        }
918    }
919
920    #[test]
921    #[allow(clippy::too_many_lines)] // Three-protocol collision plus independent toggles.
922    fn stream_result_and_response_fields_remain_independent_on_one_edge() {
923        let stream = VerifyStreamBeat {
924            job_id: b32(0x5757_0005),
925            ..VerifyStreamBeat::default()
926        };
927        let routed_response = CompressionOutput {
928            tag: b32(0x5858_0005),
929            valid: true,
930            ..CompressionOutput::default()
931        };
932        let mut contexts = [VerifyContextOutput::default(); VERIFY_CLUSTER_CONTEXTS];
933        contexts[1].loading = true;
934        contexts[2].result_valid = true;
935        contexts[2].result_job_id = b32(0x5959_0005);
936        contexts[2].verified = true;
937        contexts[2].error = b3(VERIFY_ERROR_NONE);
938        let q = VerifyClusterCoreQ {
939            contexts,
940            transport: VerifyTransportOutput {
941                responses: [
942                    CompressionOutput::default(),
943                    CompressionOutput::default(),
944                    CompressionOutput::default(),
945                    routed_response,
946                ],
947                response_routed: [false, false, false, true],
948                ..VerifyTransportOutput::default()
949            },
950            control: VerifyClusterControl {
951                frame_active: true,
952                frame_owner: b2(1),
953                frame_beat: b6(7),
954                result_cursor: b2(2),
955                ..VerifyClusterControl::default()
956            },
957            assigned_generations: [b8(1), b8(5), b8(9), b8(11)],
958            next_generations: [b8(2), b8(6), b8(10), b8(12)],
959            frame_job_id: stream.job_id,
960            result: VerifyResult::default(),
961        };
962        let input = VerifyClusterCoreInput {
963            stream_valid: true,
964            stream,
965            result_ready: false,
966            ..VerifyClusterCoreInput::default()
967        };
968
969        let (output, d) =
970            verify_cluster_core_kernel(clock_reset(clock(false), reset(false)), input, q);
971        assert!(output.stream_accepted);
972        assert_eq!(output.stream_context, b2(1));
973        assert!(d.contexts[1].stream_valid);
974        assert_eq!(d.contexts[1].stream, stream);
975        assert_eq!(d.contexts[1].generation, b8(5));
976        assert!(!d.contexts[0].stream_valid);
977        assert!(!d.contexts[2].stream_valid);
978        assert!(!d.contexts[3].stream_valid);
979        assert!(d.contexts[2].result_ready);
980        assert!(!d.contexts[0].result_ready);
981        assert!(!d.contexts[1].result_ready);
982        assert!(!d.contexts[3].result_ready);
983        assert_eq!(d.contexts[3].response, routed_response);
984        assert!(d.control.result_valid);
985        assert_eq!(d.result.job_id, b32(0x5959_0005));
986        assert!(d.result.verified);
987        assert_eq!(d.result.error, b3(VERIFY_ERROR_NONE));
988
989        let (_, no_stream_d) = verify_cluster_core_kernel(
990            clock_reset(clock(false), reset(false)),
991            VerifyClusterCoreInput {
992                stream_valid: false,
993                ..input
994            },
995            q,
996        );
997        for context in no_stream_d.contexts {
998            assert!(!context.stream_valid);
999        }
1000        assert!(no_stream_d.contexts[2].result_ready);
1001        assert_eq!(no_stream_d.contexts[3].response, routed_response);
1002
1003        let mut rejection_q = q;
1004        rejection_q.contexts[3].response_rejected = true;
1005        rejection_q.contexts[3].fault = true;
1006        let (faulted, faulted_d) =
1007            verify_cluster_core_kernel(clock_reset(clock(false), reset(false)), input, rejection_q);
1008        assert!(faulted.fault);
1009        assert!(faulted.stream_accepted);
1010        for (faulted_context, clean_context) in faulted_d.contexts.iter().zip(d.contexts.iter()) {
1011            assert_eq!(faulted_context.stream_valid, clean_context.stream_valid);
1012            assert_eq!(faulted_context.stream, stream);
1013            assert!(!faulted_context.result_ready);
1014        }
1015        assert_eq!(faulted_d.contexts[3].response, routed_response);
1016    }
1017
1018    fn assert_containment_edge(frame_active: bool, expected_context: b2) -> VerifyClusterCoreD {
1019        let stream = VerifyStreamBeat {
1020            job_id: if frame_active {
1021                b32(0x6000_0001)
1022            } else {
1023                b32(0x6000_0002)
1024            },
1025            ..VerifyStreamBeat::default()
1026        };
1027        let (output, d) = verify_cluster_core_kernel(
1028            clock_reset(clock(false), reset(false)),
1029            VerifyClusterCoreInput {
1030                stream_valid: true,
1031                stream,
1032                result_ready: true,
1033                ..VerifyClusterCoreInput::default()
1034            },
1035            rejection_q(frame_active),
1036        );
1037
1038        // The rejection is immediately fatal for results and diagnostics, but
1039        // cannot retract credit that was derived before observing the response.
1040        assert!(output.fault);
1041        assert!(output.stream_ready);
1042        assert!(output.stream_accepted);
1043        assert_eq!(output.stream_context, expected_context);
1044        assert!(!output.result_transfer);
1045        assert!(output.result_valid);
1046        assert_eq!(output.result.job_id, b32(0x5fff_0001));
1047        assert!(!output.result.verified);
1048        assert_eq!(output.result.error, b3(VERIFY_ERROR_TRANSPORT));
1049        assert_ne!(
1050            output.diagnostics & b16(VERIFY_DIAGNOSTIC_CHILD_RESPONSE_REJECT),
1051            b16(0)
1052        );
1053
1054        // The exact reported transfer is the exact physical child transfer.
1055        assert!(d.contexts[expected_context].stream_valid);
1056        assert_eq!(d.contexts[expected_context].stream, stream);
1057        for context in 0..VERIFY_CLUSTER_CONTEXTS {
1058            if b2(context as u128) != expected_context {
1059                assert!(!d.contexts[context].stream_valid);
1060            }
1061        }
1062        assert!(d.control.poison);
1063        assert!(!d.control.frame_active);
1064        assert_eq!(d.control.frame_beat, b6(0));
1065        assert_eq!(d.frame_job_id, stream.job_id);
1066
1067        // Current lane effects are independent of the response observation;
1068        // registered poison invalidates ownership and ignores the bounded later
1069        // return on the following cycle.
1070        assert!(output.lane_request.valid);
1071        assert_eq!(output.request_accepted, [true, false, false, false]);
1072        d
1073    }
1074
1075    #[test]
1076    fn child_rejection_containment_edge_accepts_beat_zero_and_midframe_then_poison_blocks() {
1077        let beat_zero_d = assert_containment_edge(false, b2(0));
1078        assert_eq!(beat_zero_d.assigned_generations[0], b8(0));
1079        assert_eq!(beat_zero_d.next_generations[0], b8(1));
1080
1081        let midframe_d = assert_containment_edge(true, b2(1));
1082        assert_eq!(midframe_d.frame_job_id, b32(0x6000_0001));
1083
1084        let (poisoned, poisoned_d) = verify_cluster_core_kernel(
1085            clock_reset(clock(false), reset(false)),
1086            VerifyClusterCoreInput {
1087                stream_valid: true,
1088                stream: VerifyStreamBeat {
1089                    job_id: b32(0x6000_0002),
1090                    ..VerifyStreamBeat::default()
1091                },
1092                ..VerifyClusterCoreInput::default()
1093            },
1094            VerifyClusterCoreQ {
1095                contexts: [VerifyContextOutput::default(); VERIFY_CLUSTER_CONTEXTS],
1096                transport: VerifyTransportOutput {
1097                    lane_request: CompressionInput {
1098                        valid: true,
1099                        ..CompressionInput::default()
1100                    },
1101                    request_accepted: [true, false, false, false],
1102                    ..VerifyTransportOutput::default()
1103                },
1104                control: beat_zero_d.control,
1105                assigned_generations: beat_zero_d.assigned_generations,
1106                next_generations: beat_zero_d.next_generations,
1107                frame_job_id: beat_zero_d.frame_job_id,
1108                result: beat_zero_d.result,
1109            },
1110        );
1111        assert!(poisoned.fault);
1112        assert!(!poisoned.stream_ready);
1113        assert!(!poisoned.stream_accepted);
1114        assert!(!poisoned.lane_request.valid);
1115        assert_eq!(poisoned.request_accepted, [false; VERIFY_CLUSTER_CONTEXTS]);
1116        for context in 0..VERIFY_CLUSTER_CONTEXTS {
1117            assert!(poisoned_d.contexts[context].transport_abort);
1118            assert!(!poisoned_d.contexts[context].stream_valid);
1119        }
1120    }
1121
1122    #[test]
1123    #[allow(clippy::too_many_lines)] // One complete command/registered/local-fatal timeline.
1124    fn external_abort_is_transition_only_until_registered_poison_contains() {
1125        let clean = VerifyResult {
1126            job_id: b32(0x7000_0007),
1127            verified: true,
1128            error: b3(VERIFY_ERROR_NONE),
1129        };
1130        let q = VerifyClusterCoreQ {
1131            contexts: [VerifyContextOutput::default(); VERIFY_CLUSTER_CONTEXTS],
1132            transport: VerifyTransportOutput {
1133                lane_request: CompressionInput {
1134                    valid: true,
1135                    ..CompressionInput::default()
1136                },
1137                request_accepted: [true, false, false, false],
1138                response_routed: [false, true, false, false],
1139                responses: [
1140                    CompressionOutput::default(),
1141                    CompressionOutput {
1142                        valid: true,
1143                        ..CompressionOutput::default()
1144                    },
1145                    CompressionOutput::default(),
1146                    CompressionOutput::default(),
1147                ],
1148                ..VerifyTransportOutput::default()
1149            },
1150            control: VerifyClusterControl {
1151                result_valid: true,
1152                ..VerifyClusterControl::default()
1153            },
1154            assigned_generations: [b8(0); VERIFY_CLUSTER_CONTEXTS],
1155            next_generations: [b8(0); VERIFY_CLUSTER_CONTEXTS],
1156            frame_job_id: b32(0),
1157            result: clean,
1158        };
1159        let parent_quiescent = VerifyClusterCoreInput {
1160            stream_valid: false,
1161            result_ready: false,
1162            ..VerifyClusterCoreInput::default()
1163        };
1164        let (baseline, _) = verify_cluster_core_kernel(
1165            clock_reset(clock(false), reset(false)),
1166            parent_quiescent,
1167            q,
1168        );
1169        let (command_edge, d) = verify_cluster_core_kernel(
1170            clock_reset(clock(false), reset(false)),
1171            VerifyClusterCoreInput {
1172                external_abort: true,
1173                ..parent_quiescent
1174            },
1175            q,
1176        );
1177
1178        // Parent abort is a transition command. The poisoned parent has already
1179        // withdrawn stream valid and result ready; every cluster output remains
1180        // bit-for-bit independent of the command on this edge.
1181        assert_eq!(command_edge, baseline);
1182        assert!(!command_edge.fault);
1183        assert!(command_edge.stream_ready);
1184        assert!(!command_edge.stream_accepted);
1185        assert!(command_edge.lane_request.valid);
1186        assert_eq!(command_edge.request_accepted, [true, false, false, false]);
1187        assert!(!command_edge.result_transfer);
1188        assert!(command_edge.result_valid);
1189        assert_eq!(command_edge.result.job_id, clean.job_id);
1190        assert!(command_edge.result.verified);
1191        assert_eq!(command_edge.result.error, b3(VERIFY_ERROR_NONE));
1192        assert_eq!(
1193            command_edge.diagnostics & b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT),
1194            b16(0)
1195        );
1196        assert!(d.control.poison);
1197        assert_ne!(
1198            d.control.diagnostics & b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT),
1199            b16(0)
1200        );
1201        assert_eq!(d.result, clean);
1202
1203        let (registered, registered_d) = verify_cluster_core_kernel(
1204            clock_reset(clock(false), reset(false)),
1205            VerifyClusterCoreInput {
1206                stream_valid: true,
1207                result_ready: false,
1208                external_abort: true,
1209                ..VerifyClusterCoreInput::default()
1210            },
1211            VerifyClusterCoreQ {
1212                contexts: [VerifyContextOutput::default(); VERIFY_CLUSTER_CONTEXTS],
1213                transport: q.transport,
1214                control: d.control,
1215                assigned_generations: d.assigned_generations,
1216                next_generations: d.next_generations,
1217                frame_job_id: d.frame_job_id,
1218                result: d.result,
1219            },
1220        );
1221        assert!(registered.fault);
1222        assert!(!registered.stream_ready);
1223        assert!(!registered.stream_accepted);
1224        assert!(!registered.lane_request.valid);
1225        assert_eq!(
1226            registered.request_accepted,
1227            [false; VERIFY_CLUSTER_CONTEXTS]
1228        );
1229        assert_eq!(registered.response_routed, [false; VERIFY_CLUSTER_CONTEXTS]);
1230        assert!(registered.result_valid);
1231        assert!(!registered.result_transfer);
1232        assert_eq!(registered.result.job_id, clean.job_id);
1233        assert!(!registered.result.verified);
1234        assert_eq!(registered.result.error, b3(VERIFY_ERROR_TRANSPORT));
1235        assert_ne!(
1236            registered.diagnostics & b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT),
1237            b16(0)
1238        );
1239        for context in registered_d.contexts {
1240            assert!(context.transport_abort);
1241            assert!(!context.stream_valid);
1242            assert!(!context.response.valid);
1243        }
1244        assert!(registered_d.transport.abort);
1245
1246        // A genuine local cause remains an immediate public fault even when the
1247        // parent command arrives on the same edge. The external diagnostic is
1248        // still visible only from the registered transition state.
1249        let mut simultaneous_q = q;
1250        simultaneous_q.transport.fatal = true;
1251        let (simultaneous, simultaneous_d) = verify_cluster_core_kernel(
1252            clock_reset(clock(false), reset(false)),
1253            VerifyClusterCoreInput {
1254                external_abort: true,
1255                ..VerifyClusterCoreInput::default()
1256            },
1257            simultaneous_q,
1258        );
1259        assert!(simultaneous.fault);
1260        assert_eq!(simultaneous.result.error, b3(VERIFY_ERROR_TRANSPORT));
1261        assert_eq!(
1262            simultaneous.diagnostics & b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT),
1263            b16(0)
1264        );
1265        assert_ne!(
1266            simultaneous_d.control.diagnostics & b16(VERIFY_DIAGNOSTIC_EXTERNAL_ABORT),
1267            b16(0)
1268        );
1269    }
1270}
wots_rhdl/verify/cluster.rs

wots_rhdl/verify/
cluster.rs
