wots_rhdl/verify/
transport.rs

1//! Fail-closed transport for four verifier contexts sharing one SHA-256 lane.
2//!
3//! Context requests first enter a speculative one-entry launch register. A
4//! request is acknowledged only on the following edge, when the unchanged,
5//! still-canonical payload is actually launched into the compression lane. The
6//! launch edge also writes its exact tag into a 64-entry synchronous expected-
7//! return memory. A due bitmap and circular pointer advance across both tokens
8//! and bubbles, aligning that tag with the lane's exact 64-cycle response.
9//!
10//! Returned tags are compared with the delayed expected tag before routing.
11//! This detects loss, extras, mistiming, malformed ownership, and a perfect swap
12//! of two otherwise canonical in-flight tags. Any outbound rejection or return
13//! integrity failure suppresses launch, capture, and routing in that cycle. The
14//! enclosing cluster registers the failure as reset-only poison and asserts
15//! `transport_abort` to every context on the following cycle.
16//!
17//! This is source and behavioral-simulation architecture. It is not generated-
18//! RTL, synthesis, resource, timing, route, or hardware evidence.
19
20use rhdl::prelude::*;
21use rhdl_fpga::core::{
22    dff::DFF,
23    ram::synchronous::{In as SyncBramIn, SyncBRAM, Write as SyncBramWrite},
24};
25use rhdl_primitives::NoResetDff;
26use sha256_rhdl::lane::{CompressionInput, CompressionOutput};
27
28use crate::{tag::decode_tag_kernel, verify::tasks::verification_tag_is_well_formed_kernel};
29
30/// Number of contexts sharing one verifier lane.
31pub const VERIFY_CLUSTER_CONTEXTS: usize = 4;
32/// Exact tag-memory address width for the 64-cycle lane.
33pub const VERIFY_EXPECTED_TAG_ADDRESS_BITS: usize = 6;
34
35/// At least one presented context request was noncanonical or changed while held.
36pub const VERIFY_DIAGNOSTIC_ISSUE_REJECT: u128 = 1 << 0;
37/// Lane-valid did not match the token/bubble due in this cycle.
38pub const VERIFY_DIAGNOSTIC_RETURN_TIMING: u128 = 1 << 1;
39/// Returned tag was not bit-for-bit equal to the delayed expected tag.
40pub const VERIFY_DIAGNOSTIC_RETURN_TAG: u128 = 1 << 2;
41/// Returned tag was outside the canonical verifier task subset.
42pub const VERIFY_DIAGNOSTIC_RETURN_FORMAT: u128 = 1 << 3;
43/// Returned tag named a physical context outside this four-context cluster.
44pub const VERIFY_DIAGNOSTIC_RETURN_OWNER: u128 = 1 << 4;
45
46const VERIFY_EXPECTED_DUE_INSERT: u128 = 1_u128 << 63;
47
48const _: () = {
49    assert!(VERIFY_CLUSTER_CONTEXTS == 4);
50    assert!(VERIFY_EXPECTED_TAG_ADDRESS_BITS == 6);
51};
52
53/// Narrow resettable control for [`VerifyTransport`].
54#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
55pub struct VerifyTransportControl {
56    /// Rotating speculative-capture cursor.
57    pub issue_cursor: b2,
58    /// A request payload is held for validation and launch.
59    pub launch_valid: bool,
60    /// Physical owner of the held launch payload.
61    pub launch_owner: b2,
62    /// Tokens due to return in exactly one through sixty-four cycles.
63    pub response_due: b64,
64    /// Circular time-slot address for the current launch or bubble.
65    pub pointer: b6,
66}
67
68/// Inputs to the four-context expected-tag transport.
69#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
70pub struct VerifyTransportInput {
71    /// Stable context-owned compression requests.
72    pub requests: [CompressionInput; VERIFY_CLUSTER_CONTEXTS],
73    /// Generation currently assigned to each physical context.
74    pub assigned_generations: [b8; VERIFY_CLUSTER_CONTEXTS],
75    /// Combinational output of the shared exact-64-cycle lane.
76    pub lane_response: CompressionOutput,
77    /// Registered cluster poison; flushes launches and ignores residual returns.
78    pub abort: bool,
79}
80
81/// Observable launch, route, and integrity signals.
82#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
83pub struct VerifyTransportOutput {
84    /// Token or bubble presented directly to the shared compression lane.
85    pub lane_request: CompressionInput,
86    /// One-hot handshakes asserted only on an actual lane launch.
87    pub request_accepted: [bool; VERIFY_CLUSTER_CONTEXTS],
88    /// One-hot noncanonical or changed held requests.
89    pub request_rejected: [bool; VERIFY_CLUSTER_CONTEXTS],
90    /// Exact-match response routed by delayed expected owner.
91    pub responses: [CompressionOutput; VERIFY_CLUSTER_CONTEXTS],
92    /// One-hot response-route pulse.
93    pub response_routed: [bool; VERIFY_CLUSTER_CONTEXTS],
94    /// A launch payload is waiting in the speculative register.
95    pub launch_pending: bool,
96    /// A token is due from the lane in this cycle.
97    pub expected_valid: bool,
98    /// Synchronous expected tag aligned with the current lane output.
99    pub expected_tag: b32,
100    /// Immediate fail-closed integrity indication.
101    pub fatal: bool,
102    /// Diagnostic causes for `fatal` in this cycle.
103    pub diagnostics: b16,
104}
105
106/// Fair speculative-capture decision.
107#[derive(Clone, Copy, Debug, Default, Digital, Eq, PartialEq)]
108pub struct VerifyTransportSelection {
109    /// At least one eligible request was selected.
110    pub valid: bool,
111    /// Selected physical context.
112    pub owner: b2,
113    /// Cursor following the selected owner.
114    pub next_cursor: b2,
115}
116
117/// Compare complete compression payloads without relying on aggregate lowering.
118#[kernel]
119#[allow(clippy::assign_op_pattern)] // Compound assignment is not lowered by pinned RHDL.
120pub fn compression_input_equal_kernel(left: CompressionInput, right: CompressionInput) -> bool {
121    let mut equal = left.valid == right.valid && left.tag == right.tag;
122    for word in 0..8 {
123        equal = equal && left.chaining[word] == right.chaining[word];
124    }
125    for word in 0..16 {
126        equal = equal && left.block[word] == right.block[word];
127    }
128    equal
129}
130
131/// Validate a request against the verifier subset and its physical assignment.
132#[kernel]
133pub fn verify_transport_request_is_canonical_kernel(
134    request: CompressionInput,
135    physical_owner: b2,
136    assigned_generation: b8,
137) -> bool {
138    let fields = decode_tag_kernel(request.tag);
139    let physical_owner_wide: b4 = physical_owner.resize();
140    request.valid
141        && verification_tag_is_well_formed_kernel(request.tag)
142        && fields.context == physical_owner_wide
143        && fields.generation == assigned_generation
144}
145
146/// Select one eligible request, optionally excluding the request being launched.
147#[kernel]
148#[allow(clippy::assign_op_pattern)] // Compound assignment is not lowered by pinned RHDL.
149pub fn select_verify_transport_request_kernel(
150    eligible: [bool; VERIFY_CLUSTER_CONTEXTS],
151    cursor: b2,
152    exclude_valid: bool,
153    excluded_owner: b2,
154) -> VerifyTransportSelection {
155    let mut selection = VerifyTransportSelection {
156        next_cursor: cursor,
157        ..VerifyTransportSelection::default()
158    };
159    let mut scan = cursor;
160    for _offset in 0..VERIFY_CLUSTER_CONTEXTS {
161        if !selection.valid && eligible[scan] && (!exclude_valid || scan != excluded_owner) {
162            selection.valid = true;
163            selection.owner = scan;
164            selection.next_cursor = scan + b2(1);
165        }
166        scan = scan + b2(1);
167    }
168    selection
169}
170
171/// Expected-tag transport controller with one speculative launch register.
172#[derive(Clone, Debug, Synchronous, SynchronousDQ)]
173#[rhdl(dq_no_prefix)]
174pub struct VerifyTransport {
175    control: DFF<VerifyTransportControl>,
176    launch: NoResetDff<CompressionInput>,
177    expected_tags: SyncBRAM<b32, VERIFY_EXPECTED_TAG_ADDRESS_BITS>,
178}
179
180impl Default for VerifyTransport {
181    fn default() -> Self {
182        Self {
183            control: DFF::new(VerifyTransportControl::default()),
184            launch: NoResetDff::new(),
185            expected_tags: SyncBRAM::default(),
186        }
187    }
188}
189
190impl SynchronousIO for VerifyTransport {
191    type I = VerifyTransportInput;
192    type O = VerifyTransportOutput;
193    type Kernel = verify_transport_kernel;
194}
195
196/// Launch-register, expected-tag, and exact-response routing transition.
197#[kernel]
198#[allow(clippy::assign_op_pattern, clippy::needless_range_loop)] // Iterators/compound assignments are not lowered by pinned RHDL.
199pub fn verify_transport_kernel(
200    clock_reset: ClockReset,
201    input: VerifyTransportInput,
202    q: Q,
203) -> (VerifyTransportOutput, D) {
204    let resetting = clock_reset.reset.any();
205    let mut control = q.control;
206    let mut launch = q.launch;
207    let mut request_accepted = [false; VERIFY_CLUSTER_CONTEXTS];
208    let mut request_rejected = [false; VERIFY_CLUSTER_CONTEXTS];
209    let mut responses = [CompressionOutput::default(); VERIFY_CLUSTER_CONTEXTS];
210    let mut response_routed = [false; VERIFY_CLUSTER_CONTEXTS];
211    let mut lane_request = CompressionInput::default();
212    let mut diagnostics = b16(0);
213
214    let canonical = [
215        verify_transport_request_is_canonical_kernel(
216            input.requests[0],
217            b2(0),
218            input.assigned_generations[0],
219        ),
220        verify_transport_request_is_canonical_kernel(
221            input.requests[1],
222            b2(1),
223            input.assigned_generations[1],
224        ),
225        verify_transport_request_is_canonical_kernel(
226            input.requests[2],
227            b2(2),
228            input.assigned_generations[2],
229        ),
230        verify_transport_request_is_canonical_kernel(
231            input.requests[3],
232            b2(3),
233            input.assigned_generations[3],
234        ),
235    ];
236    for context in 0..VERIFY_CLUSTER_CONTEXTS {
237        request_rejected[context] = input.requests[context].valid && !canonical[context];
238    }
239
240    let held_request = match q.control.launch_owner {
241        Bits::<2>(0) => input.requests[0],
242        Bits::<2>(1) => input.requests[1],
243        Bits::<2>(2) => input.requests[2],
244        _ => input.requests[3],
245    };
246    let held_generation = match q.control.launch_owner {
247        Bits::<2>(0) => input.assigned_generations[0],
248        Bits::<2>(1) => input.assigned_generations[1],
249        Bits::<2>(2) => input.assigned_generations[2],
250        _ => input.assigned_generations[3],
251    };
252    let held_canonical = verify_transport_request_is_canonical_kernel(
253        held_request,
254        q.control.launch_owner,
255        held_generation,
256    );
257    let held_unchanged = compression_input_equal_kernel(q.launch, held_request);
258    let held_failure = q.control.launch_valid && (!held_canonical || !held_unchanged);
259    if held_failure {
260        request_rejected[q.control.launch_owner] = true;
261    }
262    let issue_failure =
263        request_rejected[0] || request_rejected[1] || request_rejected[2] || request_rejected[3];
264    if issue_failure {
265        diagnostics = diagnostics | b16(VERIFY_DIAGNOSTIC_ISSUE_REJECT);
266    }
267
268    let expected_valid = q.control.response_due & b64(1) != b64(0);
269    let response_fields = decode_tag_kernel(input.lane_response.tag);
270    let response_timing_failure = expected_valid != input.lane_response.valid;
271    let response_tag_failure =
272        expected_valid && input.lane_response.valid && input.lane_response.tag != q.expected_tags;
273    let response_format_failure = input.lane_response.valid
274        && !verification_tag_is_well_formed_kernel(input.lane_response.tag);
275    let response_owner_failure = input.lane_response.valid && response_fields.context >= b4(4);
276    if response_timing_failure {
277        diagnostics = diagnostics | b16(VERIFY_DIAGNOSTIC_RETURN_TIMING);
278    }
279    if response_tag_failure {
280        diagnostics = diagnostics | b16(VERIFY_DIAGNOSTIC_RETURN_TAG);
281    }
282    if response_format_failure {
283        diagnostics = diagnostics | b16(VERIFY_DIAGNOSTIC_RETURN_FORMAT);
284    }
285    if response_owner_failure {
286        diagnostics = diagnostics | b16(VERIFY_DIAGNOSTIC_RETURN_OWNER);
287    }
288    let return_failure = response_timing_failure
289        || response_tag_failure
290        || response_format_failure
291        || response_owner_failure;
292    let fatal = !resetting && !input.abort && (issue_failure || return_failure);
293
294    let exact_return = expected_valid
295        && input.lane_response.valid
296        && input.lane_response.tag == q.expected_tags
297        && !response_format_failure
298        && !response_owner_failure;
299    if !resetting && !input.abort && !fatal && exact_return {
300        let expected_fields = decode_tag_kernel(q.expected_tags);
301        let expected_owner: b2 = expected_fields.context.resize();
302        responses[expected_owner] = input.lane_response;
303        response_routed[expected_owner] = true;
304    }
305
306    let mut expected_write = SyncBramWrite::<b32, VERIFY_EXPECTED_TAG_ADDRESS_BITS> {
307        addr: q.control.pointer,
308        value: b32(0),
309        enable: false,
310    };
311    if !resetting && !input.abort && !fatal {
312        control.response_due = q.control.response_due >> 1;
313        control.pointer = q.control.pointer + b6(1);
314
315        if q.control.launch_valid {
316            lane_request = q.launch;
317            lane_request.valid = true;
318            request_accepted[q.control.launch_owner] = true;
319            control.response_due = control.response_due | b64(VERIFY_EXPECTED_DUE_INSERT);
320            expected_write = SyncBramWrite::<b32, VERIFY_EXPECTED_TAG_ADDRESS_BITS> {
321                addr: q.control.pointer,
322                value: q.launch.tag,
323                enable: true,
324            };
325        }
326
327        let capture = select_verify_transport_request_kernel(
328            canonical,
329            q.control.issue_cursor,
330            q.control.launch_valid,
331            q.control.launch_owner,
332        );
333        control.launch_valid = capture.valid;
334        if capture.valid {
335            control.launch_owner = capture.owner;
336            control.issue_cursor = capture.next_cursor;
337            launch = match capture.owner {
338                Bits::<2>(0) => input.requests[0],
339                Bits::<2>(1) => input.requests[1],
340                Bits::<2>(2) => input.requests[2],
341                _ => input.requests[3],
342            };
343        }
344    } else {
345        control.launch_valid = false;
346        control.response_due = b64(0);
347        lane_request.valid = false;
348    }
349
350    if resetting {
351        control = VerifyTransportControl::default();
352        expected_write.enable = false;
353    }
354
355    let output = VerifyTransportOutput {
356        lane_request,
357        request_accepted,
358        request_rejected,
359        responses,
360        response_routed,
361        launch_pending: !resetting && q.control.launch_valid,
362        expected_valid: !resetting && !input.abort && expected_valid,
363        expected_tag: q.expected_tags,
364        fatal,
365        diagnostics: if resetting || input.abort {
366            b16(0)
367        } else {
368            diagnostics
369        },
370    };
371    let d = D {
372        control,
373        launch,
374        expected_tags: SyncBramIn::<b32, VERIFY_EXPECTED_TAG_ADDRESS_BITS> {
375            // At time slot p+63, pre-read slot p so the synchronous output is
376            // aligned with the lane token visible in slot p+64.
377            read_addr: q.control.pointer + b6(1),
378            write: expected_write,
379        },
380    };
381    (output, d)
382}
wots_rhdl/verify/transport.rs

wots_rhdl/verify/
transport.rs
