Skip to main content

vj_sim/sched/
subscribe.rs

1//! SCHED::SUBSCRIBE — the `WaitSpec` engine registration surface and the
2//! NBA/Inactive drain destination (scheduler.md; process.md §2/§4; ledger
3//! SC-085, SC-086; `docs/superpowers/plans/2026-09-23-wave-A-sched.md` Task
4//! 13).
5//!
6//! [`register_wait`] is the SC-085 "engine registration call every `WaitSpec`
7//! variant triggers": an exhaustive `match` over `WaitSpec`'s 4 variants
8//! (`Delay`/`Edge`/`EdgeList`/`ImplicitComb`), each dispatched to the one
9//! engine primitive that owns that variant's registration (the time wheel for
10//! `Delay`, [`SensitivityTable::install_dynamic`] for `Edge`/`EdgeList`,
11//! [`SensitivityTable::install_static`] for `ImplicitComb`). No wildcard arm
12//! — a 5th `WaitSpec` variant added later fails this match to compile.
13//!
14//! [`nba_drain_destination`] is the SC-086 "the engine's NBA-region drain
15//! must be the destination `nba_enqueue` targets, and the engine owns
16//! draining/applying" — made concrete as one function that stages `updates`
17//! into a temporary [`NbaLog`] and delegates to Task 7's already-existing
18//! [`commit_nba`], never reimplementing its write+diff algorithm a second
19//! time (see this module's own commit message / the plan's Task 13 "review
20//! fix, sixth review pass" note for why: two physical implementations of one
21//! pure write+diff algorithm is exactly the failure class this codebase has
22//! hit before).
23//!
24//! **Deviation from the plan's literal signatures** (both functions), recorded
25//! here and in `docs/CONTRACTS.md`'s Deviations section: the plan names a
26//! `gate: &QueuedGate` parameter on both `register_wait` and
27//! `nba_drain_destination`, and a `queues: &mut RegionQueues` parameter on
28//! `nba_drain_destination`. `QueuedGate` is Task 10's own type
29//! (`docs/superpowers/plans/2026-09-23-wave-A-sched.md` Task 10, ledger
30//! SC-055/SC-056) and — exactly as Task 11's `process_table.rs::form_ready_set`
31//! doc comment already records for the same reason — does not exist in this
32//! tree: Task 10 has not been implemented yet, and SC-055/SC-056 are not in
33//! this task's assigned ledger scope (`["SC-085","SC-086"]`). Per Task 11's
34//! own precedent ("Task 10, when it lands, is expected to extend this
35//! function's signature... which this task deliberately leaves untouched
36//! rather than inventing Task 10's own type ahead of its task"), this module
37//! does the same: `register_wait` never needed `gate` for any of its 4 match
38//! arms' described behavior (registration, not dedup-at-notify-time) so it is
39//! dropped entirely; `nba_drain_destination`'s wakeup sink calls Task 9's
40//! already-existing [`SensitivityTable::matches`] directly instead of Task
41//! 10's not-yet-existing `dedup::sensitivity_match_to_enqueue` wrapper — this
42//! is still exactly one canonical matching implementation (Task 9's), not a
43//! second one, so SC-042's "no duplicate implementation" concern this
44//! delegation exists to satisfy is unaffected. Neither of Task 13's own
45//! specified tests exercises the case dedup would change (a single process
46//! sensitive to two different cells that both change in the same
47//! `nba_drain_destination` call), so no acceptance behavior in this task's
48//! ledger scope is weakened by the omission. `nba_drain_destination`'s
49//! `queues: &mut RegionQueues` parameter is dropped for the same reason: the
50//! plan's own prose for this function never describes pushing anything onto
51//! `queues` — it only describes building and returning
52//! `Vec<PendingActivation>` ("This is what's returned") — so the parameter
53//! was unused by the function's own specified algorithm.
54//!
55//! Also not in the plan's literal signature: `register_wait`'s `WaitSpec::
56//! ImplicitComb` arm needs the "caller-supplied `SubscriptionSetId ->
57//! StaticSensitivity` lookup" the plan's own prose names but omits from the
58//! parameter list — added here as `static_sensitivity_by_set`, exactly the
59//! `HashMap` parameter the plan's prose says this function gains.
60//! `register_wait` returns `Result<(), RegisterWaitError>` rather than the
61//! plan's literal `-> ()`: an unresolvable `SubscriptionSetId` (the fake
62//! test-only lookup missing an entry) is a real, catchable condition, not a
63//! programmer error safe to `.expect()` away, and this workspace's
64//! correctness posture forbids a silent no-op or a panic for a condition a
65//! caller can legitimately hit.
66
67use std::collections::HashMap;
68
69use vj_abi::{Region, SimTime};
70
71use crate::process::{SubscriptionSetId, WaitSpec};
72use crate::sched::{
73    ActivationId, EventTerm, EventWaitSet, NbaLog, NbaUpdate, PendingActivation, ProcessId,
74    RegionQueues, ResumeArg, SchedTime, SensitivityTable, StaticSensitivity, TimeWheel, commit_nba,
75};
76use crate::state::{EdgeKind, SignalAccess, StateCellId, ValueChangeSink};
77
78/// `register_wait`'s one failure mode. See this module's doc comment for why
79/// this exists instead of the plan's literal `-> ()`.
80#[derive(Clone, Copy, PartialEq, Eq, Debug)]
81pub enum RegisterWaitError {
82    /// `WaitSpec::ImplicitComb`'s `SubscriptionSetId` had no entry in the
83    /// caller-supplied lookup (codegen's real static-sensitivity table does
84    /// not exist yet in this wave — the plan's own text names this as an
85    /// in-crate test fixture stand-in).
86    UnknownSubscriptionSet(SubscriptionSetId),
87    /// [`TimeWheel::arm_delay`] is documented to return only
88    /// `Region::Active` or `Region::Inactive`. This variant exists purely so
89    /// this function's own dispatch on that return value stays an
90    /// exhaustive match over the full 7-variant `Region` type with no
91    /// wildcard arm (this workspace's "loud typed error, never a silent
92    /// no-op" posture), catching a future change to `arm_delay`'s contract
93    /// at this call site instead of silently mishandling it. sva T1 (§1.4,
94    /// review fix, blocking finding 2) folded `Region::Preponed` into this
95    /// same defensive arm alongside `Nba`/`Reactive`/`Postponed`; sva T2
96    /// (review fix, blocking finding 2), Observed's half, folds
97    /// `Region::Observed` into it too, for the identical reason.
98    UnexpectedWheelRegion(Region),
99}
100
101impl std::fmt::Display for RegisterWaitError {
102    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
103        match self {
104            RegisterWaitError::UnknownSubscriptionSet(id) => {
105                write!(f, "no StaticSensitivity registered for {id:?}")
106            }
107            RegisterWaitError::UnexpectedWheelRegion(r) => {
108                write!(f, "TimeWheel::arm_delay returned unexpected region {r:?}")
109            }
110        }
111    }
112}
113
114impl std::error::Error for RegisterWaitError {}
115
116/// Converts a `WaitSpec::Delay`'s `SimTime` *duration* into wheel-facing
117/// ticks. `WaitSpec::Delay` names a duration (an `#N` delay statement), not
118/// an absolute time, so only `sim_units` (the minimum-time-precision tick
119/// count) is meaningful here — `delta` (the delta-cycle/region-iteration
120/// counter, per `vj_abi::SimTime`'s own doc comment) has no meaning for a
121/// duration. Saturates at zero rather than reinterpreting a negative
122/// `sim_units` as a huge `u64` via a raw `as` cast, which would silently
123/// arm a near-infinite delay instead of surfacing the codegen/elaboration
124/// bug a negative delay duration would represent.
125fn ticks_from(t: SimTime) -> u64 {
126    t.sim_units.max(0) as u64
127}
128
129/// The SC-085 engine registration call every `WaitSpec` variant triggers, on
130/// `proc`'s behalf, at `now`. See this module's doc comment for the
131/// deviations from the plan's literal signature.
132pub fn register_wait(
133    table: &mut SensitivityTable,
134    wheel: &mut TimeWheel,
135    queues: &mut RegionQueues,
136    proc: ProcessId,
137    spec: &WaitSpec,
138    now: SchedTime,
139    static_sensitivity_by_set: &HashMap<SubscriptionSetId, StaticSensitivity>,
140) -> Result<(), RegisterWaitError> {
141    match spec {
142        WaitSpec::Delay(t) => {
143            let delay_ticks = ticks_from(*t);
144            let act = PendingActivation {
145                id: proc as ActivationId,
146                proc,
147                arg: ResumeArg::TimeElapsed,
148                reconv_iter: 0,
149                logical_order: (
150                    SchedTime {
151                        ticks: now.ticks + delay_ticks,
152                    },
153                    Region::Active,
154                    0,
155                ),
156            };
157            match wheel.arm_delay(now.ticks, delay_ticks, act) {
158                Region::Inactive => {
159                    // `delay_ticks == 0`: `arm_delay` deliberately never
160                    // touches the wheel for this case (SC-029) — the caller
161                    // (here) must land `act` directly in `Region::Inactive`.
162                    // `RegionQueues::push` only ever rejects `Region::Nba`
163                    // (Task 4), so pushing to `Inactive` cannot fail.
164                    //
165                    // `act` was built above with `logical_order.1` set to
166                    // `Region::Active` (the common case, where `arm_delay`
167                    // arms the wheel instead). That tag must agree with the
168                    // queue the activation actually lands in — `order.rs`'s
169                    // `canonical_key_of`/`sort_ready_set` read
170                    // `logical_order.1` directly to build the canonical key
171                    // (SC-010/DT-005/DT-010), and `RegionQueues::push`'s own
172                    // contract is to route `act` to *its region's* queue —
173                    // so re-tag it to `Region::Inactive` before pushing.
174                    let act = PendingActivation {
175                        logical_order: (act.logical_order.0, Region::Inactive, act.logical_order.2),
176                        ..act
177                    };
178                    queues
179                        .push(Region::Inactive, act)
180                        .expect("Region::Inactive is always accepted by RegionQueues::push");
181                }
182                Region::Active => {
183                    // Armed onto the wheel by `arm_delay` itself (nonzero
184                    // delay) — nothing further to do here.
185                }
186                // sva T1 (§1.4, review fix, blocking finding 2): `Region::
187                // Preponed` joins this defensive arm for the identical
188                // reason `Nba`/`Reactive`/`Postponed` are already here --
189                // `TimeWheel::arm_delay` can no more legitimately return
190                // `Preponed` than any of those three (it is a pure
191                // snapshot-push point, never a wheel-armed delay target).
192                // sva T2 (review fix, blocking finding 2), Observed's half:
193                // `Region::Observed` joins it too -- a process's delay/edge
194                // wait can no more land in Observed than in Preponed (it is
195                // reached only through the region-callback mechanism, never
196                // a wheel-armed delay target).
197                other @ (Region::Nba
198                | Region::Reactive
199                | Region::Postponed
200                | Region::Preponed
201                | Region::Observed) => {
202                    return Err(RegisterWaitError::UnexpectedWheelRegion(other));
203                }
204            }
205        }
206        WaitSpec::Edge { edge, signal, iff } => {
207            let wait = EventWaitSet {
208                terms: vec![EventTerm::Edge {
209                    cell: *signal,
210                    edge: *edge,
211                    iff: *iff,
212                }],
213                ..Default::default()
214            };
215            table.install_dynamic(&wait, proc);
216        }
217        WaitSpec::EdgeList(terms) => {
218            let wait = EventWaitSet {
219                terms: terms
220                    .iter()
221                    .map(|(edge, signal, iff)| EventTerm::Edge {
222                        cell: *signal,
223                        edge: *edge,
224                        iff: *iff,
225                    })
226                    .collect(),
227                ..Default::default()
228            };
229            table.install_dynamic(&wait, proc);
230        }
231        WaitSpec::ImplicitComb(set_id) => {
232            let sensitivity = static_sensitivity_by_set
233                .get(set_id)
234                .ok_or(RegisterWaitError::UnknownSubscriptionSet(*set_id))?;
235            table.install_static(sensitivity, proc);
236        }
237    }
238    Ok(())
239}
240
241/// The [`ValueChangeSink`] [`nba_drain_destination`] hands to Task 7's
242/// [`commit_nba`] instead of calling the sink method directly (or any other
243/// fan-out) itself. Its own `notify_change` body routes straight through
244/// Task 9's already-existing [`SensitivityTable::matches`] — no new matching
245/// logic, no second implementation of the sensitivity lookup Task 18's
246/// `EngineNotifySink` also reuses (see this module's doc comment for why
247/// this is `matches` directly rather than Task 10's not-yet-existing
248/// `dedup::sensitivity_match_to_enqueue` wrapper).
249struct NbaWakeupSink<'a> {
250    sensitivity: &'a SensitivityTable,
251    /// Always `Region::Active` for every activation this sink produces
252    /// (SC-086 — NBA-triggered wakeups land in Active, scheduler.md §1 step
253    /// 3), regardless of the `region` `commit_nba` itself reports on each
254    /// `notify_change` call (`Region::Nba`, the region the *write* committed
255    /// in — not the region the *woken process* must next run in).
256    region: Region,
257    /// The scheduler time `nba_drain_destination` was called at (its own
258    /// `at: SchedTime` parameter), threaded through so every
259    /// `PendingActivation` this sink produces carries the *real* vtime as
260    /// `logical_order.0` — the primary field `order.rs`'s
261    /// `canonical_key_of`/`sort_ready_set` sort by (SC-010/DT-005/DT-010) —
262    /// instead of an unconditional `SchedTime { ticks: 0 }`.
263    /// `commit_nba`'s own `notify_change` callback receives `_at: SimTime`
264    /// (the write's timestamp, which is `at` reinterpreted, per this
265    /// module's existing convention of discarding it here — see below) but
266    /// that value is per-write and always equal to this sink's own `now`
267    /// for every call `commit_nba` makes within one `nba_drain_destination`
268    /// invocation, so capturing it once at construction is equivalent and
269    /// avoids re-deriving `SchedTime` from `SimTime` per call.
270    now: SchedTime,
271    out: &'a mut Vec<PendingActivation>,
272}
273
274impl ValueChangeSink for NbaWakeupSink<'_> {
275    fn notify_change(&mut self, cell: StateCellId, edge: EdgeKind, _at: SimTime, _region: Region) {
276        // Task 3 widened `matches`'s item type to `(ProcessId, usize,
277        // Option<u64>)`, and Task 5 (SC-068) widened it again to add a 4th
278        // `Option<PredicateFn>` element; this sink has no repeat-counting or
279        // `iff`-evaluation role (see this module's own doc comment for why
280        // it calls `matches` directly rather than
281        // `dedup::sensitivity_match_to_enqueue`) and only ever needed the
282        // `ProcessId`.
283        for (proc, _, _, _) in self.sensitivity.matches(cell, edge) {
284            // Placeholder `id`/tiebreak values (this task's own scope is
285            // SC-085/SC-086, which name nothing about global `ActivationId`
286            // assignment or a real per-process `registration_order`; both
287            // remain Task 21 outer-driver concerns, matching the existing
288            // precedent of `notify.rs`'s `NBA_COMMIT_KEY_PROCESS_ID`/
289            // `reconv_iter: 0` placeholders for the same not-yet-wired
290            // concern). `self.out.len()` at push time is nonetheless a
291            // real, strictly increasing counter that exactly matches
292            // `commit_nba`'s own deterministic (canonical, cell-id-ordered)
293            // `notify_change` call order — not a caller-`stage()`-order
294            // artifact — which is what SC-086's canonical-order tests need.
295            let seq = self.out.len() as u64;
296            self.out.push(PendingActivation {
297                id: seq,
298                proc,
299                // `SensitivityTable::matches` (Task 9) returns only
300                // `ProcessId`, not the originating `Dynamic` entry's
301                // `term_index` — that information is discarded by `matches`
302                // itself and is not recoverable here without changing Task
303                // 9's own contract, which this task does not own. `0` is a
304                // placeholder, matching this module's established pattern
305                // for information not yet threaded end-to-end.
306                arg: ResumeArg::EventFired { term_index: 0 },
307                reconv_iter: 0,
308                logical_order: (self.now, self.region, seq),
309            });
310        }
311    }
312}
313
314/// The SC-086 NBA/Inactive-region drain destination: stages `updates` into a
315/// temporary [`NbaLog`] (preserving their original `order`, since `updates`
316/// is itself [`NbaLog::take`]'s output and `stage` assigns `order` from push
317/// position — Task 6's own contract), then delegates to Task 7's
318/// [`commit_nba`] rather than reimplementing its write+diff algorithm.
319/// Returns one [`PendingActivation`] per process woken by an actually-changed
320/// cell, each landing in `Region::Active` (SC-086).
321pub fn nba_drain_destination(
322    updates: Vec<NbaUpdate>,
323    arena: &mut dyn SignalAccess,
324    sensitivity: &SensitivityTable,
325    at: SchedTime,
326) -> Vec<PendingActivation> {
327    let mut temp_log = NbaLog::new();
328    for u in updates {
329        temp_log.stage(u.cell, u.value, u.source);
330    }
331
332    let mut out: Vec<PendingActivation> = Vec::new();
333    {
334        let mut sink = NbaWakeupSink {
335            sensitivity,
336            region: Region::Active,
337            now: at,
338            out: &mut out,
339        };
340        commit_nba(&mut temp_log, arena, at, &mut sink);
341    }
342    out
343}
344
345#[cfg(test)]
346mod tests {
347    use super::*;
348    use crate::sched::{ProcessId as SchedProcessId, StaticSensitivity, sort_ready_set};
349    use crate::state::{FourStateValue, ListenerRole};
350    use std::collections::HashMap;
351
352    // --- register_wait / SC-085 ---
353
354    fn four_state_eq(a: &FourStateValue, b: &FourStateValue) -> bool {
355        match (a, b) {
356            (FourStateValue::Narrow(x), FourStateValue::Narrow(y)) => x == y,
357            (
358                FourStateValue::Wide { aval: a1, bval: b1 },
359                FourStateValue::Wide { aval: a2, bval: b2 },
360            ) => a1 == a2 && b1 == b2,
361            _ => false,
362        }
363    }
364
365    struct FakeArena {
366        cells: HashMap<StateCellId, FourStateValue>,
367    }
368
369    impl FakeArena {
370        fn new() -> Self {
371            Self {
372                cells: HashMap::new(),
373            }
374        }
375
376        fn seed(&mut self, cell: StateCellId, value: FourStateValue) {
377            self.cells.insert(cell, value);
378        }
379    }
380
381    impl SignalAccess for FakeArena {
382        fn read(&self, cell: StateCellId) -> FourStateValue {
383            self.cells
384                .get(&cell)
385                .cloned()
386                .unwrap_or(FourStateValue::Narrow(0))
387        }
388
389        fn write(&mut self, cell: StateCellId, value: FourStateValue) -> bool {
390            let changed = match self.cells.get(&cell) {
391                Some(existing) => !four_state_eq(existing, &value),
392                None => true,
393            };
394            self.cells.insert(cell, value);
395            changed
396        }
397
398        fn subscribe(
399            &mut self,
400            _cell: StateCellId,
401            _role: ListenerRole,
402            _sink: Box<dyn ValueChangeSink + Send>,
403        ) {
404            // Not exercised by this task's tests.
405        }
406    }
407
408    #[test]
409    fn every_wait_spec_variant_has_a_registration_arm() {
410        let empty_lookup: HashMap<SubscriptionSetId, StaticSensitivity> = HashMap::new();
411
412        // --- Delay ---
413        {
414            let mut table = SensitivityTable::new();
415            let mut wheel = TimeWheel::new();
416            let mut queues = RegionQueues::new();
417            let proc: SchedProcessId = 1;
418            let spec = WaitSpec::Delay(SimTime {
419                sim_units: 5,
420                delta: 0,
421            });
422            register_wait(
423                &mut table,
424                &mut wheel,
425                &mut queues,
426                proc,
427                &spec,
428                SchedTime { ticks: 10 },
429                &empty_lookup,
430            )
431            .expect("Delay registration must succeed");
432            assert_eq!(
433                wheel.next_tick(),
434                Some(15),
435                "Delay(5) registered at tick 10 must arm the wheel to fire at tick 15"
436            );
437        }
438
439        // --- Edge ---
440        {
441            let mut table = SensitivityTable::new();
442            let mut wheel = TimeWheel::new();
443            let mut queues = RegionQueues::new();
444            let proc: SchedProcessId = 2;
445            let cell = StateCellId(100);
446            let spec = WaitSpec::Edge {
447                edge: EdgeKind::Posedge,
448                signal: cell,
449                iff: None,
450            };
451            register_wait(
452                &mut table,
453                &mut wheel,
454                &mut queues,
455                proc,
456                &spec,
457                SchedTime { ticks: 0 },
458                &empty_lookup,
459            )
460            .expect("Edge registration must succeed");
461            assert_eq!(
462                table
463                    .matches(cell, EdgeKind::Posedge)
464                    .map(|(p, _, _, _)| p)
465                    .collect::<Vec<_>>(),
466                vec![proc],
467                "Edge registration must install a dynamic entry the table finds"
468            );
469        }
470
471        // --- EdgeList ---
472        {
473            let mut table = SensitivityTable::new();
474            let mut wheel = TimeWheel::new();
475            let mut queues = RegionQueues::new();
476            let proc: SchedProcessId = 3;
477            let cell_a = StateCellId(101);
478            let cell_b = StateCellId(102);
479            let spec = WaitSpec::EdgeList(vec![
480                (EdgeKind::Posedge, cell_a, None),
481                (EdgeKind::Negedge, cell_b, None),
482            ]);
483            register_wait(
484                &mut table,
485                &mut wheel,
486                &mut queues,
487                proc,
488                &spec,
489                SchedTime { ticks: 0 },
490                &empty_lookup,
491            )
492            .expect("EdgeList registration must succeed");
493            assert_eq!(
494                table
495                    .matches(cell_a, EdgeKind::Posedge)
496                    .map(|(p, _, _, _)| p)
497                    .collect::<Vec<_>>(),
498                vec![proc],
499                "EdgeList must install a dynamic entry per (edge, signal) pair (first pair)"
500            );
501            assert_eq!(
502                table
503                    .matches(cell_b, EdgeKind::Negedge)
504                    .map(|(p, _, _, _)| p)
505                    .collect::<Vec<_>>(),
506                vec![proc],
507                "EdgeList must install a dynamic entry per (edge, signal) pair (second pair)"
508            );
509        }
510
511        // --- ImplicitComb ---
512        {
513            let mut table = SensitivityTable::new();
514            let mut wheel = TimeWheel::new();
515            let mut queues = RegionQueues::new();
516            let proc: SchedProcessId = 4;
517            let cell = StateCellId(103);
518            let set_id = SubscriptionSetId(7);
519            let mut lookup: HashMap<SubscriptionSetId, StaticSensitivity> = HashMap::new();
520            lookup.insert(
521                set_id,
522                StaticSensitivity {
523                    edges: vec![(cell, None)],
524                },
525            );
526            let spec = WaitSpec::ImplicitComb(set_id);
527            register_wait(
528                &mut table,
529                &mut wheel,
530                &mut queues,
531                proc,
532                &spec,
533                SchedTime { ticks: 0 },
534                &lookup,
535            )
536            .expect("ImplicitComb registration must succeed via the fake lookup");
537            assert_eq!(
538                table
539                    .matches(cell, EdgeKind::Negedge)
540                    .map(|(p, _, _, _)| p)
541                    .collect::<Vec<_>>(),
542                vec![proc],
543                "ImplicitComb must install a static any-change entry via the lookup"
544            );
545        }
546    }
547
548    #[test]
549    fn delay_zero_lands_directly_in_inactive_not_the_wheel() {
550        let mut table = SensitivityTable::new();
551        let mut wheel = TimeWheel::new();
552        let mut queues = RegionQueues::new();
553        let empty_lookup: HashMap<SubscriptionSetId, StaticSensitivity> = HashMap::new();
554        let proc: SchedProcessId = 9;
555        let spec = WaitSpec::Delay(SimTime {
556            sim_units: 0,
557            delta: 0,
558        });
559
560        register_wait(
561            &mut table,
562            &mut wheel,
563            &mut queues,
564            proc,
565            &spec,
566            SchedTime { ticks: 3 },
567            &empty_lookup,
568        )
569        .expect("Delay(0) registration must succeed");
570
571        assert_eq!(
572            wheel.next_tick(),
573            None,
574            "Delay(0) must never touch the wheel"
575        );
576        let drained = queues.drain_inactive();
577        assert_eq!(drained.len(), 1);
578        assert_eq!(drained[0].proc, proc);
579        assert_eq!(
580            drained[0].logical_order.1,
581            Region::Inactive,
582            "an activation landed in the Inactive queue must carry Region::Inactive as its \
583             own logical_order.1 tag, agreeing with the queue it actually lives in — \
584             canonical_key_of/sort_ready_set (order.rs) read logical_order.1 directly to \
585             build the canonical key that SC-010/DT-005/DT-010 depend on"
586        );
587    }
588
589    /// sva T1 (§1.4, review fix, blocking finding 2): `register_wait`'s
590    /// `match wheel.arm_delay(..)` defensive arm must still compile
591    /// exhaustively over `Region`'s new 6th variant, with `Preponed` folded
592    /// into the SAME `other @ (Nba | Reactive | Postponed | Preponed)` arm
593    /// as the pre-existing three (not a fresh wildcard, which this
594    /// workspace's "loud typed error" posture forbids). `arm_delay` itself
595    /// is documented to return only `Active`/`Inactive`, so this arm is
596    /// never reachable through the real code path above (there is no mock
597    /// `TimeWheel` seam this function could inject one through) -- this
598    /// test instead proves, by direct construction, that
599    /// `RegisterWaitError::UnexpectedWheelRegion` can represent
600    /// `Region::Preponed` and names it correctly in its `Display` text, the
601    /// same proof-by-construction this type's own doc comment already
602    /// relies on for `Nba`/`Reactive`/`Postponed`.
603    #[test]
604    fn register_wait_defensive_arm_still_exhaustive_with_preponed() {
605        let err = RegisterWaitError::UnexpectedWheelRegion(Region::Preponed);
606        assert_eq!(
607            err,
608            RegisterWaitError::UnexpectedWheelRegion(Region::Preponed)
609        );
610        assert!(
611            err.to_string().contains("Preponed"),
612            "the Display text must name the offending region: {err}"
613        );
614    }
615
616    /// sva T2 (review fix, blocking finding 2), Observed's half: the
617    /// identical proof-by-construction as
618    /// `register_wait_defensive_arm_still_exhaustive_with_preponed`, now for
619    /// `Region::Observed`.
620    #[test]
621    fn register_wait_defensive_arm_still_exhaustive_with_observed() {
622        let err = RegisterWaitError::UnexpectedWheelRegion(Region::Observed);
623        assert_eq!(
624            err,
625            RegisterWaitError::UnexpectedWheelRegion(Region::Observed)
626        );
627        assert!(
628            err.to_string().contains("Observed"),
629            "the Display text must name the offending region: {err}"
630        );
631    }
632
633    #[test]
634    fn implicit_comb_with_an_unresolvable_set_id_is_a_typed_error_not_a_panic() {
635        let mut table = SensitivityTable::new();
636        let mut wheel = TimeWheel::new();
637        let mut queues = RegionQueues::new();
638        let empty_lookup: HashMap<SubscriptionSetId, StaticSensitivity> = HashMap::new();
639        let spec = WaitSpec::ImplicitComb(SubscriptionSetId(999));
640
641        let result = register_wait(
642            &mut table,
643            &mut wheel,
644            &mut queues,
645            1,
646            &spec,
647            SchedTime { ticks: 0 },
648            &empty_lookup,
649        );
650
651        assert_eq!(
652            result,
653            Err(RegisterWaitError::UnknownSubscriptionSet(
654                SubscriptionSetId(999)
655            ))
656        );
657    }
658
659    // --- nba_drain_destination / SC-086 ---
660
661    #[test]
662    fn nba_drain_produces_activations_only_for_changed_cells_in_canonical_form() {
663        let cell_changed = StateCellId(200);
664        let cell_unchanged = StateCellId(201);
665        let proc_changed: SchedProcessId = 10;
666        let proc_unchanged: SchedProcessId = 20;
667
668        let mut arena = FakeArena::new();
669        arena.seed(cell_changed, FourStateValue::Narrow(0));
670        arena.seed(cell_unchanged, FourStateValue::Narrow(7));
671
672        let mut sensitivity = SensitivityTable::new();
673        sensitivity.install_static(
674            &StaticSensitivity {
675                edges: vec![(cell_changed, None)],
676            },
677            proc_changed,
678        );
679        sensitivity.install_static(
680            &StaticSensitivity {
681                edges: vec![(cell_unchanged, None)],
682            },
683            proc_unchanged,
684        );
685
686        let updates = vec![
687            NbaUpdate {
688                cell: cell_changed,
689                value: FourStateValue::Narrow(1),
690                source: 1,
691                order: 0,
692            },
693            NbaUpdate {
694                cell: cell_unchanged,
695                value: FourStateValue::Narrow(7),
696                source: 1,
697                order: 1,
698            },
699        ];
700
701        let activations =
702            nba_drain_destination(updates, &mut arena, &sensitivity, SchedTime { ticks: 5 });
703
704        assert_eq!(
705            activations.len(),
706            1,
707            "only the process sensitive to the genuinely-changed cell may be activated"
708        );
709        assert_eq!(activations[0].proc, proc_changed);
710        assert_eq!(
711            activations[0].logical_order.1,
712            Region::Active,
713            "NBA-triggered wakeups must land in Region::Active"
714        );
715        assert_eq!(
716            activations[0].logical_order.0,
717            SchedTime { ticks: 5 },
718            "an NBA-triggered wakeup's logical_order.0 must be the `at` scheduler time \
719             nba_drain_destination was called with, not a hardcoded tick"
720        );
721    }
722
723    #[test]
724    fn nba_drain_at_nonzero_time_stamps_activations_with_that_time_not_zero() {
725        // SC-010/DT-005/DT-010 regression: `NbaWakeupSink` used to hardcode
726        // `logical_order.0` to `SchedTime { ticks: 0 }` for every activation
727        // it produced, regardless of `nba_drain_destination`'s own `at`
728        // parameter. A call at a nonzero time must stamp its activations
729        // with that time.
730        let cell = StateCellId(230);
731        let proc: SchedProcessId = 40;
732
733        let mut arena = FakeArena::new();
734        arena.seed(cell, FourStateValue::Narrow(0));
735
736        let mut sensitivity = SensitivityTable::new();
737        sensitivity.install_static(
738            &StaticSensitivity {
739                edges: vec![(cell, None)],
740            },
741            proc,
742        );
743
744        let updates = vec![NbaUpdate {
745            cell,
746            value: FourStateValue::Narrow(1),
747            source: 1,
748            order: 0,
749        }];
750
751        let at = SchedTime { ticks: 7 };
752        let activations = nba_drain_destination(updates, &mut arena, &sensitivity, at);
753
754        assert_eq!(activations.len(), 1);
755        assert_eq!(
756            activations[0].logical_order.0, at,
757            "logical_order.0 must equal the `at` time nba_drain_destination was called \
758             with, not SchedTime {{ ticks: 0 }}"
759        );
760    }
761
762    #[test]
763    fn nba_drain_applies_exactly_the_queued_tuples_in_canonical_order() {
764        let cell_a = StateCellId(210);
765        let cell_b = StateCellId(211);
766        let cell_c = StateCellId(212);
767        let proc_a: SchedProcessId = 30;
768        let proc_b: SchedProcessId = 31;
769        let proc_c: SchedProcessId = 32;
770
771        let mut sensitivity = SensitivityTable::new();
772        sensitivity.install_static(
773            &StaticSensitivity {
774                edges: vec![(cell_a, None)],
775            },
776            proc_a,
777        );
778        sensitivity.install_static(
779            &StaticSensitivity {
780                edges: vec![(cell_b, None)],
781            },
782            proc_b,
783        );
784        sensitivity.install_static(
785            &StaticSensitivity {
786                edges: vec![(cell_c, None)],
787            },
788            proc_c,
789        );
790
791        // Out-of-order relative to the cells' own ordering.
792        let updates = vec![
793            NbaUpdate {
794                cell: cell_c,
795                value: FourStateValue::Narrow(1),
796                source: 1,
797                order: 0,
798            },
799            NbaUpdate {
800                cell: cell_a,
801                value: FourStateValue::Narrow(1),
802                source: 1,
803                order: 1,
804            },
805            NbaUpdate {
806                cell: cell_b,
807                value: FourStateValue::Narrow(1),
808                source: 1,
809                order: 2,
810            },
811        ];
812
813        let mut arena1 = FakeArena::new();
814        let acts1 = nba_drain_destination(
815            updates.clone(),
816            &mut arena1,
817            &sensitivity,
818            SchedTime { ticks: 7 },
819        );
820
821        // A second run with a different stage/arrival order for the same
822        // logical set of updates (only the arena is fresh; the sensitivity
823        // table and target cells are identical).
824        let updates2 = vec![updates[1].clone(), updates[2].clone(), updates[0].clone()];
825        let mut arena2 = FakeArena::new();
826        let acts2 =
827            nba_drain_destination(updates2, &mut arena2, &sensitivity, SchedTime { ticks: 7 });
828
829        let mut sorted1 = acts1;
830        let mut sorted2 = acts2;
831        sort_ready_set(&mut sorted1);
832        sort_ready_set(&mut sorted2);
833
834        let procs1: Vec<SchedProcessId> = sorted1.iter().map(|a| a.proc).collect();
835        let procs2: Vec<SchedProcessId> = sorted2.iter().map(|a| a.proc).collect();
836        assert_eq!(
837            procs1, procs2,
838            "canonical order must not depend on the original stage/arrival order"
839        );
840        assert_eq!(procs1.len(), 3);
841    }
842
843    #[test]
844    fn nba_drain_destination_delegates_to_commit_nba_not_a_second_diff_implementation() {
845        let cell = StateCellId(220);
846        let mut arena = FakeArena::new();
847        arena.seed(cell, FourStateValue::Narrow(5));
848
849        let sensitivity = SensitivityTable::new();
850
851        let updates = vec![NbaUpdate {
852            cell,
853            value: FourStateValue::Narrow(5),
854            source: 1,
855            order: 0,
856        }];
857
858        let activations =
859            nba_drain_destination(updates, &mut arena, &sensitivity, SchedTime { ticks: 0 });
860
861        assert!(
862            activations.is_empty(),
863            "an NBA write equal to the current value must produce no activation — a \
864             reimplementation that diffs against a stale/default value instead of \
865             genuinely calling commit_nba's arena-compare would produce a spurious one here"
866        );
867
868        // Source-text companion check (same technique as process_table.rs's
869        // slotmap scan / determinism's DT-006 scan): production code (test
870        // bodies stripped) must call `commit_nba(` and must never call
871        // `.notify_change(` itself.
872        let src = std::fs::read_to_string(concat!(
873            env!("CARGO_MANIFEST_DIR"),
874            "/src/sched/subscribe.rs"
875        ))
876        .expect("must be able to read subscribe.rs's own source");
877        let production_only = crate::determinism::scan_support::strip_cfg_test_blocks(&src);
878        assert!(
879            production_only.contains("commit_nba("),
880            "nba_drain_destination must call Task 7's commit_nba"
881        );
882        assert!(
883            !production_only.contains(".notify_change("),
884            "subscribe.rs must not call .notify_change( itself — it must delegate to \
885             commit_nba, not reimplement NBA commit semantics"
886        );
887    }
888}