vj-sim 0.1.0

Netlist, scheduler and process model of the vj SystemVerilog simulator.
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
//! Task 16 — Undo-log rollback and the one generic coarse snapshot/restore
//! primitive (ledger ST-032, ST-036, ST-098).
//!
//! Two independent primitives, both documented in ARCHITECTURE §6.2/§7 item 5
//! as STATE's checkpoint machinery:
//! - [`UndoLog`] (ST-036): a per-thread-owned reverse log implementing Task
//!   8's [`super::PreWriteHook`], giving that hook its first real body.
//!   `O(1)`-amortized append via `before_write`, `O(distance)` undo via
//!   [`UndoLog::rollback_to`] — the checkpoint cost model ST-032 asks be
//!   "referenced by the accessor-ABI calling convention" (Task 8's
//!   `commit_write(&mut self, cell, new, hook: &mut dyn PreWriteHook)`,
//!   frozen since that task).
//! - [`StateEngine::snapshot`]/[`StateEngine::restore`]/
//!   [`StateEngine::reset_to_initial`] (ST-098): the one generic
//!   slice-granular checkpoint/restore primitive — an optional
//!   `(SlotClass, start_word, word_count)` range, `None` meaning "the whole
//!   arena" — WOCB's inner-window rollback, a top-level `$save`/`$restart`,
//!   and VPI/debugger state snapshotting all call this *same* function with
//!   different `range` arguments, never three separate serialization
//!   implementations.
//!
//! **Deviations from the plan's literal text** (documented once here,
//! applying to everything below — the first four are related: each exists
//! because the plan's own pinned signatures, taken literally, are either
//! under-specified or structurally unimplementable as written; the fifth is
//! a review fix, not a plan-signature gap):
//!
//! 1. **`checkpoint_marker`/`rollback_to`/`fossil_collect` live on
//!    [`UndoLog`], not on `StateEngine`.** The plan's prose puts them in
//!    `impl StateEngine`, but `StateEngine` cannot *also* own the log as a
//!    field and have `commit_write`'s existing, frozen
//!    `hook: &mut dyn PreWriteHook` parameter be `&mut self.undo_log` at the
//!    one call site that matters — `engine.commit_write(cell, new, &mut
//!    engine.undo_log)` is two overlapping mutable borrows of `self` through
//!    one method call, which Rust refuses. Keeping [`UndoLog`] a plain,
//!    caller-owned value — exactly mirroring `()`'s existing role as the
//!    no-op hook — sidesteps that conflict entirely and needs no new
//!    `StateEngine` field: a caller passes `&mut log` to `commit_write`
//!    exactly like `&mut ()`, and later calls `log.rollback_to(&mut engine,
//!    mark)` (which *does* need `&mut StateEngine`, to replay into it — its
//!    only extra parameter versus the plan's pinned prose) or
//!    `log.fossil_collect(gvt)`/`log.checkpoint_marker()` (which don't).
//! 2. **`rollback_to` returns `Result<(), sched::RewindError>`, not `()`**
//!    (binding per this task's own unresolved-review-findings list, findings
//!    3/4): the plan's own `fossil_collect` test requires that a
//!    `rollback_to` call targeting a marker before the fossil-collected
//!    horizon "returns a documented `RewindError`-shaped failure rather than
//!    silently under-rolling-back," which a unit-returning function
//!    structurally cannot do. `sched::RewindError` (the crate's own
//!    contract stub, `crate::sched::mod.rs`) already declares exactly the
//!    two variants this module needs — `PastFossilHorizon` (reused here, per
//!    the plan's own test prose) and `LayoutMismatch` (reused by
//!    [`StateEngine::restore`] below, for the identical reason: no new local
//!    error type duplicates what the scheduler contract already names).
//! 3. **`PreWriteHook::before_write` gained a `SimTime` parameter**
//!    (`state::write`, this module's one caller of the trait): `fossil_collect
//!    (gvt)`'s "trims entries provably before `gvt`" is only meaningful if
//!    [`UndoLog`]'s entries carry a real timestamp to compare, and nothing
//!    else in the calling convention threads one to the hook — see
//!    `state::write`'s own doc comment on this second, smaller deviation.
//! 4. **[`ArenaSnapshot`] carries a fifth field, `range`,** beyond the plan's
//!    literal `{layout_hash, inline, wide_aval, wide_bval}` list: `restore`'s
//!    own pinned signature (`&mut self, snap: &ArenaSnapshot`) takes no
//!    `range` parameter of its own, so a snapshot that only stored the four
//!    plan-listed fields would have no way to tell `restore` *where* a
//!    partial-range snapshot's data belongs — seeing this field is the
//!    minimal addition that makes the plan's own pinned `restore` signature
//!    actually implementable for the partial-range case its own test
//!    requires.
//! 5. **`ArenaSnapshot` carries two further fields, `build_mode` and a
//!    2-state pair (`inline_2s`, `wide_2s`), and `snapshot`/`restore`/
//!    `reset_to_initial` are all build-mode-aware** (Task 16 r1, blocking
//!    review finding 1): the plan's own prose pins `reset_to_initial`'s
//!    contract as "uninitialized 4-state variables ... to all-X ..., 2-state
//!    to 0" — i.e. this primitive is specified to handle a
//!    `BuildMode::TwoState` engine, not just the default `BuildMode::FourState`
//!    one this module's first revision exclusively handled. Task 13's own
//!    `alloc_inline_words`/`alloc_wide_words` grow the 4-state and 2-state
//!    plane-pairs in lockstep at identical word offsets (`state::arena`'s own
//!    module doc comment), so a `TwoState` engine's real live data lives in
//!    `inline_2s`/`wide_2s` at the exact same offsets this module's
//!    4-state-only primitives were reading/writing instead — silently
//!    touching only the inert, always-zero 4-state planes and leaving the
//!    real data completely untouched, with no panic or error of any kind.
//!    `snapshot` now branches on `self.build_mode()` once per call and
//!    captures whichever plane-pair is actually live for that range (never
//!    both — the other pair's fields stay empty `Vec`s), and stamps the
//!    captured `BuildMode` onto the snapshot; `restore` rejects
//!    (`Err(RewindError::LayoutMismatch)`) a snapshot whose stored
//!    `build_mode` doesn't match `self`'s own, before touching any plane —
//!    the same "no ArenaSnapshot with a ForceWide range can exist to reach
//!    that arm" style of making a cross-mode restore structurally impossible
//!    to mis-apply, rather than merely undocumented. This does not conflict
//!    with `state::write`'s own "never a runtime branch inside either
//!    [4-state/2-state] family" design principle: that principle is about
//!    per-write dispatch inside a compiled kernel's hot path, never applying
//!    to this module's coarse, call-once-per-checkpoint administrative bulk
//!    operations, which already branch once per call on `SlotClass` in
//!    exactly this same way.

use sv_sim_abi::SimTime;

use super::arena::{Arena, BuildMode};
use super::instance::StateEngine;
use super::write::{PreWriteHook, SlotLocation, write_inline_2s, write_slot, write_wide_2s};
use super::{FourStateValue, SlotClass, StateCellId};
use crate::sched::RewindError;

/// An opaque log-length marker (ST-036) — see [`UndoLog::checkpoint_marker`].
/// The wrapped index is absolute over the log's *entire* lifetime (it
/// includes entries [`UndoLog::fossil_collect`] has already trimmed), never
/// merely an index into the log's *currently retained* `Vec` — see
/// [`UndoLog::rollback_to`]'s own doc comment for why that distinction is
/// what makes the fossil-horizon check correct.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct RollbackMark(usize);

/// Task 16 (ST-098): per-cell reset behavior [`StateEngine::reset_to_initial`]
/// consults, populated in lockstep with `StateEngine.cells` — see
/// `state::instance`'s `StateEngine.cell_reset` field doc comment for how
/// each cell gets its real entry.
#[derive(Debug)]
pub(crate) enum CellReset {
    /// An uninitialized non-net variable/port: 4-state all-X (`val=0,
    /// mask=all-1`), sized from the cell's own `SlotLocation` — the
    /// conservative default `write::StateEngine::alloc_cell` pushes for
    /// *every* cell (including force_driver's synthetic contribution cells
    /// and this crate's own test helpers), never overwritten for those.
    AllX,
    /// A variable/port with a declared initializer (Task 6): the exact
    /// `FourStateValue` to re-blit, already converted from the slot's
    /// `sv_lang::OwnedSVInt` at `allocate_instance` time.
    Initial(FourStateValue),
    /// A net-backed cell (`SlotDescriptor.net_info.is_some()`): never
    /// touched by `reset_to_initial` — its reset state is the emergent `Z`
    /// `driver::resolve_net_step` folds to over zero active drivers (Task
    /// 14), not a stored arena default.
    Net,
    /// **Review fix (Task 16 r1, blocking finding 2):** one of
    /// `driver::force_driver`'s synthetic, caller-invisible contribution
    /// cells (both its `SlotClass::Inline` arm, which shares the ordinary
    /// inline plane with real variables and is otherwise indistinguishable
    /// from one once `alloc_cell` has run, and its `SlotClass::ForceWide`
    /// arm) — never touched by `reset_to_initial`, for the identical reason
    /// [`StateEngine::snapshot`] already refuses a `SlotClass::ForceWide`
    /// range outright: these cells are never part of a real elaborated
    /// signal's storage, so blitting all-X (or any reset value) over one
    /// would silently corrupt a live `force` contribution with no error,
    /// exactly the "silent corruption" class `snapshot`'s own `ForceWide`
    /// panic exists to prevent for the snapshot/restore half of this same
    /// primitive family. `force_driver` (`state::driver`) sets this on its
    /// synthetic cell immediately after `StateEngine::alloc_cell`, the same
    /// way `allocate_instance` overwrites `alloc_cell`'s conservative
    /// default for its own real slots.
    ForceContribution,
}

/// ST-036: the per-thread undo/reverse log — see this module's top doc
/// comment for why it is a plain, caller-owned value (like `()`) rather than
/// a `StateEngine`-owned field. Implements [`PreWriteHook`]: every
/// `commit_write(cell, new, &mut log)` call appends `(cell, old, at)` here
/// *before* the store happens (Task 8/ST-091's own ordering guarantee),
/// giving that hook its first real body.
#[derive(Default)]
pub struct UndoLog {
    entries: Vec<(StateCellId, FourStateValue, SimTime)>,
    /// The absolute count of entries [`Self::fossil_collect`] has ever
    /// trimmed from the front over this log's lifetime — see
    /// [`RollbackMark`]'s own doc comment for why marks are absolute indices
    /// over this running total, not indices into `entries` alone.
    collected: usize,
}

impl UndoLog {
    pub fn new() -> Self {
        UndoLog::default()
    }

    /// ST-036: an opaque marker for the log's current length — "current"
    /// meaning the absolute count of entries ever appended so far (already
    /// including any [`Self::fossil_collect`] has trimmed), so a mark taken
    /// before a trim and a mark taken after it are still comparable on the
    /// same absolute scale.
    pub fn checkpoint_marker(&self) -> RollbackMark {
        RollbackMark(self.collected + self.entries.len())
    }

    /// ST-036: pops entries back to `mark`, replaying each popped entry's
    /// `old` value into `engine` via [`StateEngine::commit_write_no_hook`]
    /// (a *second*, hook-free write primitive, so unwinding the log never
    /// re-appends to the very log it's unwinding) in reverse order — `Vec::
    /// pop` naturally visits the most-recently-appended entry first, which
    /// is what makes a cell written twice since `mark` end up back at its
    /// original (not its intermediate) value.
    ///
    /// `Err(RewindError::PastFossilHorizon)` — never a silent
    /// under-rollback — when `mark` refers to a position at or before
    /// entries [`Self::fossil_collect`] has already, irreversibly discarded;
    /// the log is left completely untouched in that case (checked before any
    /// entry is popped).
    pub fn rollback_to(
        &mut self,
        engine: &mut StateEngine,
        mark: RollbackMark,
    ) -> Result<(), RewindError> {
        if mark.0 < self.collected {
            return Err(RewindError::PastFossilHorizon);
        }
        let target_local = mark.0 - self.collected;
        while self.entries.len() > target_local {
            let (cell, old, _at) = self
                .entries
                .pop()
                .expect("entries.len() > target_local, checked by the loop condition, guarantees pop succeeds");
            engine.commit_write_no_hook(cell, old);
        }
        Ok(())
    }

    /// Trims every entry with `at <= gvt` from the *front* of the log
    /// (append-only, so the front holds the oldest entries) — "at or before
    /// `gvt`, never past it": the scan stops at the first entry whose `at`
    /// is strictly after `gvt`, so nothing newer is ever removed even if a
    /// later entry happened to compare `<=` some other way.
    pub fn fossil_collect(&mut self, gvt: SimTime) {
        let mut cut = 0;
        while cut < self.entries.len() && super::write::sim_time_le(self.entries[cut].2, gvt) {
            cut += 1;
        }
        if cut > 0 {
            self.entries.drain(0..cut);
            self.collected += cut;
        }
    }

    /// Test-only peek at how many entries are currently retained (distinct
    /// from `checkpoint_marker`'s absolute, ever-appended count) — lets a
    /// test assert `fossil_collect` actually removed entries without
    /// depending on `rollback_to`'s own (separately tested) replay behavior.
    #[cfg(test)]
    fn retained_len(&self) -> usize {
        self.entries.len()
    }
}

impl PreWriteHook for UndoLog {
    fn before_write(
        &mut self,
        cell: StateCellId,
        _loc: SlotLocation,
        old: &FourStateValue,
        _new_incoming: &FourStateValue,
        at: SimTime,
    ) {
        self.entries.push((cell, old.clone(), at));
    }
}

/// ST-098: the one generic slice-granular checkpoint/restore primitive's
/// data — see this module's top doc comment, deviation 4, for why `range` is
/// a fifth field beyond the plan's literal list, and deviation 5 for why
/// `build_mode`/`inline_2s`/`wide_2s` exist beyond that (only one of
/// `{inline, wide_aval, wide_bval}`/`{inline_2s, wide_2s}` is ever populated
/// for a given snapshot — whichever plane-pair `build_mode` says is actually
/// live — the other stays empty `Vec`s).
pub struct ArenaSnapshot {
    layout_hash: u64,
    range: Option<(SlotClass, u32, u32)>,
    build_mode: BuildMode,
    inline: Vec<u128>,
    wide_aval: Vec<u64>,
    wide_bval: Vec<u64>,
    inline_2s: Vec<u64>,
    wide_2s: Vec<u64>,
}

/// Builds the all-X [`FourStateValue`] for an uninitialized cell's own
/// `SlotLocation` shape — reuses [`bits_to_four_state`] for the `Inline`
/// case (always `<= 64` bits by construction, so it always yields `Narrow`,
/// never ambiguous) rather than hand-deriving the val/unk bit pattern; the
/// `Wide`/`Memory`/`ForceWide` case constructs the per-word all-ones
/// `aval`/`bval` planes directly from the already-established
/// `Bit4::to_aval_bval(X) == (true, true)` table (`state::value`'s own test,
/// `bits_to_four_state_wide_uses_bit4_aval_bval_table`, is what pins that
/// exact constant) rather than through `bits_to_four_state` itself, because
/// a `Wide`-class cell can legitimately be exactly 64 bits (one word) —
/// `bits_to_four_state`'s own `<= 64` branch would then return `Narrow`, a
/// shape `write_slot`'s `Wide`/`Memory` match arm rejects outright.
fn all_x_value_for(loc: SlotLocation) -> FourStateValue {
    match loc.class {
        SlotClass::Inline => {
            // Narrow lanes are `2*unk+val` with val in the low 64 bits and
            // unk in the high 64; X is (val 0, unk 1) per
            // `Bit4::to_val_unk`, so all-X is the width mask in the unk
            // plane. (Built directly, not through the frontend-only
            // `bits_to_four_state`, so this module builds without the
            // `frontend` feature -- CONTRACTS D4.)
            let (x_val, x_unk) = sv_sim_abi::Bit4::X.to_val_unk();
            let mask: u64 = if loc.bit_width >= 64 {
                u64::MAX
            } else {
                (1u64 << loc.bit_width) - 1
            };
            let val = if x_val { mask } else { 0 };
            let unk = if x_unk { mask } else { 0 };
            FourStateValue::Narrow((val as u128) | ((unk as u128) << 64))
        }
        SlotClass::Wide | SlotClass::Memory | SlotClass::ForceWide => {
            let n = loc.elem_word_count as usize;
            FourStateValue::Wide {
                aval: vec![u64::MAX; n],
                bval: vec![u64::MAX; n],
            }
        }
    }
}

/// **Review fix (Task 16 r1, blocking finding 1):** the `BuildMode::TwoState`
/// counterpart of [`all_x_value_for`] — an uninitialized 2-state cell resets
/// to plain `0` (the plan's own `reset_to_initial` contract: "... 2-state to
/// `0`"), never all-ones, since there is no mask/unknown half in the 2-state
/// plane to set at all.
///
/// # Panics
/// If `loc.class` is `SlotClass::ForceWide` — unreachable in practice, since
/// [`StateEngine::reset_to_initial`] filters out every
/// [`CellReset::ForceContribution`] cell (which is what every `ForceWide`
/// cell's own `CellReset` entry is tagged as, per that variant's own doc
/// comment) before this helper is ever called.
fn reset_2s_cell_to_zero(arena: &Arena, loc: SlotLocation) {
    match loc.class {
        SlotClass::Inline => {
            write_inline_2s(arena, loc.word_offset, 0);
        }
        SlotClass::Wide | SlotClass::Memory => {
            let zeros = vec![0u64; loc.elem_word_count as usize];
            write_wide_2s(arena, loc.word_offset, &zeros);
        }
        SlotClass::ForceWide => unreachable!(
            "reset_2s_cell_to_zero: force_driver's contribution cells are tagged \
             CellReset::ForceContribution and are filtered out by reset_to_initial \
             before this helper is ever reached for one"
        ),
    }
}

/// **Review fix (Task 16 r1, blocking finding 1):** the `BuildMode::TwoState`
/// counterpart of re-blitting a [`CellReset::Initial`] value — projects the
/// 4-state [`FourStateValue`] a declared initializer was already converted
/// to (Task 6, `value::owned_svint_to_four_state`) down to just its known
/// "value" half (`val` for `Narrow`, `aval` for `Wide` — `state::value`'s own
/// val/unk and aval/bval encoding, where the first half is always the plain
/// value bits and the second is the unknown-ness mask), since the 2-state
/// plane has no mask half to store an unknown bit in at all.
///
/// # Panics
/// If `loc`'s `SlotClass` doesn't match `fv`'s own `FourStateValue` shape
/// (`Inline`/`Narrow` or `Wide|Memory`/`Wide`) — the same class of
/// caller-contract violation `write_slot`'s own shape-mismatch arm already
/// panics on elsewhere in this crate; every real `CellReset::Initial` this
/// crate ever constructs (`allocate_instance`, the one call site) is built
/// from the same slot's own `SlotLocation`, so reaching this arm indicates a
/// lockstep-invariant violation elsewhere, never a normal case to tolerate
/// silently.
fn write_2s_cell_from_initial(arena: &Arena, loc: SlotLocation, fv: &FourStateValue) {
    match (loc.class, fv) {
        (SlotClass::Inline, FourStateValue::Narrow(word)) => {
            write_inline_2s(arena, loc.word_offset, *word as u64);
        }
        (SlotClass::Wide | SlotClass::Memory, FourStateValue::Wide { aval, .. }) => {
            write_wide_2s(arena, loc.word_offset, aval);
        }
        (class, value) => panic!(
            "write_2s_cell_from_initial: SlotClass {class:?} does not match the \
             FourStateValue shape of this cell's own CellReset::Initial ({value:?}) -- \
             a CellReset::Initial is only ever built by allocate_instance from the same \
             slot's own SlotLocation, so this indicates a lockstep-invariant violation \
             elsewhere in this crate, not a normal case this helper tolerates silently"
        ),
    }
}

impl StateEngine {
    /// ST-036: writes `value` at `cell`'s already-allocated `SlotLocation`
    /// with no [`PreWriteHook`] call and no `VcRecord` append — used
    /// exclusively by [`UndoLog::rollback_to`]'s own reverse replay, so
    /// unwinding the log never re-appends to the very log it is unwinding,
    /// and a rollback (reverting to a value the log already knows was live)
    /// is never itself treated as a fresh, dispatch-notified "change."
    pub(crate) fn commit_write_no_hook(&mut self, cell: StateCellId, value: FourStateValue) {
        let loc = self.cells[cell.0 as usize];
        write_slot(&self.arena, loc, &value);
    }

    /// ST-098: takes a snapshot of `range` (`None` = the whole arena) —
    /// `layout_hash` is `self.templates.signature_hash()` at the moment of
    /// the call, guarding a later [`Self::restore`] against an incompatible
    /// `StateEngine`. **Review fix (Task 16 r1, blocking finding 1):**
    /// build-mode-aware — branches once on `self.build_mode()` and captures
    /// whichever plane-pair (`{inline, wide_aval, wide_bval}` for
    /// `FourState`, `{inline_2s, wide_2s}` for `TwoState`) is actually the
    /// engine's live data at `range`'s word offsets (Task 13's
    /// `alloc_inline_words`/`alloc_wide_words` grow both plane-pairs in
    /// lockstep at identical offsets, `state::arena`'s own module doc
    /// comment, so the offsets are shared — only which plane-pair holds the
    /// real values differs); the other plane-pair's fields stay empty
    /// `Vec`s. The captured `build_mode` is stamped onto the returned
    /// snapshot so [`Self::restore`] can refuse a cross-mode restore.
    ///
    /// # Panics
    /// If `range`'s `SlotClass` is `ForceWide` — `force_driver`'s synthetic,
    /// caller-invisible contribution cells (see `SlotClass::ForceWide`'s own
    /// doc comment) are never part of a real elaborated signal's storage and
    /// are not an intended target of this API (WOCB rollback, `$save`/
    /// `$restart`, and VPI/debugger snapshotting all operate over ordinary
    /// `Inline`/`Wide`/`Memory` signals); a caller reaching this is a
    /// programming error at the call site, the same class of failure
    /// `write_slot`'s own shape-mismatch panic already documents elsewhere
    /// in this crate, not a normal case this primitive tolerates silently.
    pub fn snapshot(&self, range: Option<(SlotClass, u32, u32)>) -> ArenaSnapshot {
        let layout_hash = self.templates.signature_hash();
        let build_mode = self.build_mode();
        let (inline, wide_aval, wide_bval, inline_2s, wide_2s) = match (build_mode, range) {
            (BuildMode::FourState, None) => (
                self.arena.inline().to_vec(),
                self.arena.wide_aval().to_vec(),
                self.arena.wide_bval().to_vec(),
                Vec::new(),
                Vec::new(),
            ),
            (BuildMode::FourState, Some((SlotClass::Inline, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                (
                    self.arena.inline()[s..e].to_vec(),
                    Vec::new(),
                    Vec::new(),
                    Vec::new(),
                    Vec::new(),
                )
            }
            (BuildMode::FourState, Some((SlotClass::Wide | SlotClass::Memory, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                (
                    Vec::new(),
                    self.arena.wide_aval()[s..e].to_vec(),
                    self.arena.wide_bval()[s..e].to_vec(),
                    Vec::new(),
                    Vec::new(),
                )
            }
            (BuildMode::TwoState, None) => (
                Vec::new(),
                Vec::new(),
                Vec::new(),
                self.arena.inline_2s().to_vec(),
                self.arena.wide_2s().to_vec(),
            ),
            (BuildMode::TwoState, Some((SlotClass::Inline, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                (
                    Vec::new(),
                    Vec::new(),
                    Vec::new(),
                    self.arena.inline_2s()[s..e].to_vec(),
                    Vec::new(),
                )
            }
            (BuildMode::TwoState, Some((SlotClass::Wide | SlotClass::Memory, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                (
                    Vec::new(),
                    Vec::new(),
                    Vec::new(),
                    Vec::new(),
                    self.arena.wide_2s()[s..e].to_vec(),
                )
            }
            (_, Some((SlotClass::ForceWide, _, _))) => panic!(
                "StateEngine::snapshot: SlotClass::ForceWide is never a valid snapshot/restore \
                 range -- force_driver's synthetic contribution cells are never part of a real \
                 elaborated signal's storage and are not observable through this API"
            ),
        };
        ArenaSnapshot {
            layout_hash,
            range,
            build_mode,
            inline,
            wide_aval,
            wide_bval,
            inline_2s,
            wide_2s,
        }
    }

    /// ST-098: restores `snap`'s data back into `self`'s arena at `snap`'s
    /// own recorded range (or the whole arena, for `None`) — a slice
    /// operation for `Some(range)`: words outside that range are left
    /// completely untouched. `Err(RewindError::LayoutMismatch)` — checked
    /// *before* any write — when `self`'s currently-registered template
    /// set doesn't hash the same as the one `snap` was taken from, when
    /// `self`'s `build_mode` doesn't match `snap`'s own (**review fix, Task
    /// 16 r1, blocking finding 1** — restoring a `FourState` snapshot into a
    /// `TwoState` engine, or vice versa, would otherwise silently target the
    /// wrong plane-pair entirely, the identical hazard this fix closes for
    /// `snapshot`/`reset_to_initial`), and when the target range's own word
    /// count doesn't match what `snap` actually holds (a
    /// same-hash-different-instance-count edge case the plan's own
    /// four-field `ArenaSnapshot` shape doesn't separately name, but which
    /// this same typed error class covers rather than panicking on a
    /// length-mismatched `copy_from_slice`); on any mismatch, `self`'s
    /// arena contents are provably unchanged — no partial corruption on the
    /// rejected path.
    pub fn restore(&mut self, snap: &ArenaSnapshot) -> Result<(), RewindError> {
        if self.templates.signature_hash() != snap.layout_hash {
            return Err(RewindError::LayoutMismatch);
        }
        if self.build_mode() != snap.build_mode {
            return Err(RewindError::LayoutMismatch);
        }
        // The planes are about to be rewritten behind every huge-signal
        // mirror (`state::huge_mirror`).
        self.arena.huge.invalidate_all();
        match (snap.build_mode, snap.range) {
            (BuildMode::FourState, None) => {
                if snap.inline.len() != self.arena.inline().len()
                    || snap.wide_aval.len() != self.arena.wide_aval().len()
                    || snap.wide_bval.len() != self.arena.wide_bval().len()
                {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: `&mut self` guarantees no other live borrow of any
                // Arena plane is held across this call (Arena's own
                // single-logical-writer discipline, `state::arena`'s module
                // doc comment); this `StateEngine` is the sole owner
                // reaching this `Arena` at this moment, and the length
                // checks above already proved every slice below is in
                // bounds.
                unsafe {
                    self.arena.inline_mut()[..snap.inline.len()].copy_from_slice(&snap.inline);
                    self.arena.wide_aval_mut()[..snap.wide_aval.len()]
                        .copy_from_slice(&snap.wide_aval);
                    self.arena.wide_bval_mut()[..snap.wide_bval.len()]
                        .copy_from_slice(&snap.wide_bval);
                }
            }
            (BuildMode::FourState, Some((SlotClass::Inline, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                if e > self.arena.inline().len() || snap.inline.len() != count as usize {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: same argument as the `None` arm above, restricted
                // to the `[s, e)` sub-slice the bounds check just proved is
                // in range.
                unsafe {
                    self.arena.inline_mut()[s..e].copy_from_slice(&snap.inline);
                }
            }
            (BuildMode::FourState, Some((SlotClass::Wide | SlotClass::Memory, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                if e > self.arena.wide_aval().len()
                    || e > self.arena.wide_bval().len()
                    || snap.wide_aval.len() != count as usize
                    || snap.wide_bval.len() != count as usize
                {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: same argument as the `None` arm above, restricted
                // to the `[s, e)` sub-slice the bounds check just proved is
                // in range, applied to both wide planes.
                unsafe {
                    self.arena.wide_aval_mut()[s..e].copy_from_slice(&snap.wide_aval);
                    self.arena.wide_bval_mut()[s..e].copy_from_slice(&snap.wide_bval);
                }
            }
            (BuildMode::TwoState, None) => {
                if snap.inline_2s.len() != self.arena.inline_2s().len()
                    || snap.wide_2s.len() != self.arena.wide_2s().len()
                {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: same argument as the `FourState`/`None` arm above,
                // applied to the 2-state planes.
                unsafe {
                    self.arena.inline_2s_mut()[..snap.inline_2s.len()]
                        .copy_from_slice(&snap.inline_2s);
                    self.arena.wide_2s_mut()[..snap.wide_2s.len()].copy_from_slice(&snap.wide_2s);
                }
            }
            (BuildMode::TwoState, Some((SlotClass::Inline, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                if e > self.arena.inline_2s().len() || snap.inline_2s.len() != count as usize {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: same argument as the `FourState`/`Inline` arm
                // above, restricted to the `[s, e)` sub-slice the bounds
                // check just proved is in range, applied to the 2-state
                // inline plane.
                unsafe {
                    self.arena.inline_2s_mut()[s..e].copy_from_slice(&snap.inline_2s);
                }
            }
            (BuildMode::TwoState, Some((SlotClass::Wide | SlotClass::Memory, start, count))) => {
                let (s, e) = (start as usize, start as usize + count as usize);
                if e > self.arena.wide_2s().len() || snap.wide_2s.len() != count as usize {
                    return Err(RewindError::LayoutMismatch);
                }
                // SAFETY: same argument as the `FourState`/`Wide|Memory` arm
                // above, restricted to the `[s, e)` sub-slice the bounds
                // check just proved is in range, applied to the 2-state
                // wide plane.
                unsafe {
                    self.arena.wide_2s_mut()[s..e].copy_from_slice(&snap.wide_2s);
                }
            }
            (_, Some((SlotClass::ForceWide, _, _))) => unreachable!(
                "StateEngine::restore: an ArenaSnapshot's own `range` is only ever set by \
                 Self::snapshot, which already rejects SlotClass::ForceWide before constructing \
                 one -- no ArenaSnapshot with a ForceWide range can exist to reach this arm"
            ),
        }
        Ok(())
    }

    /// ST-098 (documented alongside `snapshot`/`restore` as this same
    /// primitive family's third bulk operation, per the plan's own prose):
    /// re-blits every cell's [`CellReset`] (`state::instance`'s
    /// `cell_reset`, populated by `allocate_instance`) over the arena — a
    /// declared initializer's exact value for a slot that has one, all-X (4-
    /// state) or `0` (2-state) for an uninitialized non-net, non-force slot,
    /// and nothing at all for a net-backed slot (its reset state is the
    /// emergent `Z` `driver::resolve_net_step` folds to over zero active
    /// drivers, never a stored arena default) or a `force_driver` contribution
    /// cell (**review fix, Task 16 r1, blocking finding 2** — never a real
    /// elaborated signal's storage; see [`CellReset::ForceContribution`]'s
    /// own doc comment for why blitting over one would silently corrupt a
    /// live `force`). Bypasses `commit_write`/`PreWriteHook`/`VcRecord`
    /// entirely (a direct [`write_slot`]/[`write_inline_2s`]/[`write_wide_2s`]
    /// poke, the same tier of primitive `Self::restore` uses) — this
    /// establishes the simulation's actual starting state before any process
    /// runs, not an ordinary mid-run write a scheduler/waveform/VPI listener
    /// should observe as a "change." **Review fix (Task 16 r1, blocking
    /// finding 1):** build-mode-aware — branches once on `self.build_mode()`
    /// and re-blits whichever plane-pair is this engine's actual live data
    /// (see this module's top doc comment, deviation 5).
    pub fn reset_to_initial(&mut self) {
        self.reset_to_initial_with(false);
    }

    /// [`Self::reset_to_initial`], optionally starting every uninitialized
    /// 4-state variable and memory row at 0 instead of X (`x_as_zero`): the
    /// non-LRM `--x-initial zero` run option, for benches written against a
    /// 2-state simulator (Verilator's `--x-initial 0`, VCS's `+vcs+initreg+0`).
    /// Nets keep their LRM starting values.
    pub fn reset_to_initial_with(&mut self, x_as_zero: bool) {
        let build_mode = self.build_mode();
        for idx in 0..self.cell_reset.len() {
            let loc = self.cells[idx];
            match &self.cell_reset[idx] {
                CellReset::Net => {}
                CellReset::ForceContribution => {}
                // A memory is ONE cell whose `loc` addresses row 0; every row
                // must be reset (an unwritten `mem[k]` reads X, LRM §6.8 --
                // iverilog-verified), not just the first.
                CellReset::AllX => {
                    let rows = if loc.class == SlotClass::Memory {
                        loc.num_rows as u64
                    } else {
                        1
                    };
                    for row in 0..rows {
                        let row_loc = if loc.class == SlotClass::Memory {
                            super::write::resolve_mem_row(loc, row)
                        } else {
                            loc
                        };
                        match build_mode {
                            BuildMode::FourState => {
                                let value = if x_as_zero {
                                    match row_loc.class {
                                        SlotClass::Inline => FourStateValue::Narrow(0),
                                        _ => FourStateValue::Wide {
                                            aval: vec![0; row_loc.elem_word_count as usize],
                                            bval: vec![0; row_loc.elem_word_count as usize],
                                        },
                                    }
                                } else {
                                    all_x_value_for(row_loc)
                                };
                                write_slot(&self.arena, row_loc, &value);
                            }
                            BuildMode::TwoState => reset_2s_cell_to_zero(&self.arena, row_loc),
                        }
                    }
                }
                // A memory's `initial` (layout): `Narrow(0)` for a 2-state
                // memory with no initializer (`int m[4]`, `real r[2]`) --
                // every row 0 -- or `Wide` holding every row's
                // `elem_word_count`-word value in row order (a declared
                // initializer, `int m[2] = '{1, 2}`).
                CellReset::Initial(fv) if loc.class == SlotClass::Memory => {
                    let words = loc.elem_word_count as usize;
                    for row in 0..loc.num_rows as usize {
                        let row_loc = super::write::resolve_mem_row(loc, row as u64);
                        let (aval, bval) = match fv {
                            FourStateValue::Wide { aval, bval } => (
                                aval[row * words..(row + 1) * words].to_vec(),
                                bval[row * words..(row + 1) * words].to_vec(),
                            ),
                            FourStateValue::Narrow(_) => (vec![0; words], vec![0; words]),
                        };
                        match build_mode {
                            BuildMode::FourState => write_slot(
                                &self.arena,
                                row_loc,
                                &FourStateValue::Wide { aval, bval },
                            ),
                            BuildMode::TwoState => {
                                write_wide_2s(&self.arena, row_loc.word_offset, &aval);
                            }
                        }
                    }
                }
                CellReset::Initial(fv) => match build_mode {
                    BuildMode::FourState => {
                        let value = fv.clone();
                        write_slot(&self.arena, loc, &value);
                    }
                    BuildMode::TwoState => write_2s_cell_from_initial(&self.arena, loc, fv),
                },
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use super::super::write::{read_inline_2s, read_wide_2s};
    use super::*;
    use crate::netlist::{SymbolKey, TemplateKey};
    use crate::state::instance::TemplateRegistry;
    use crate::state::write::SlotLocation;
    use crate::state::{SignalAccess, SlotDescriptor, SlotOffset, StateLayout};

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

    /// Allocates one inline cell (mirrors `write::tests::inline_cell`,
    /// duplicated locally per this crate's existing per-task-module test
    /// helper convention).
    fn inline_cell(engine: &mut StateEngine) -> StateCellId {
        // SAFETY: local, single-owned engine; no other live borrow of the
        // inline plane, and every test below performs no concurrent
        // allocation on the same engine.
        let word_offset = unsafe { engine.arena.alloc_inline_word() };
        let loc = SlotLocation {
            class: SlotClass::Inline,
            word_offset,
            bit_width: 8,
            elem_word_count: 1,
            row_stride_words: 0,
            num_rows: 0,
        };
        engine.alloc_cell(loc)
    }

    fn narrow_word(val: u64, unk: u64) -> u128 {
        (val as u128) | ((unk as u128) << 64)
    }

    fn narrow_at(engine: &StateEngine, cell: StateCellId) -> u128 {
        match engine.read(cell) {
            FourStateValue::Narrow(w) => w,
            FourStateValue::Wide { .. } => panic!("expected Narrow"),
        }
    }

    fn t(units: i64) -> SimTime {
        SimTime {
            sim_units: units,
            delta: 0,
        }
    }

    /// ST-036: 3 sequential `commit_write`s to 3 *different* cells through an
    /// `UndoLog`-backed `StateEngine` (`checkpoint_marker()` taken before all
    /// 3); `rollback_to` the marker; all 3 cells must read back their
    /// pre-write (uninitialized, all-zero-word) values — not just the last
    /// one, proving multi-entry replay.
    #[test]
    fn rollback_to_a_marker_undoes_writes_in_reverse_order() {
        let mut engine = fresh_engine();
        let cell_a = inline_cell(&mut engine);
        let cell_b = inline_cell(&mut engine);
        let cell_c = inline_cell(&mut engine);
        let mut log = UndoLog::new();

        let mark = log.checkpoint_marker();
        engine.commit_write(cell_a, FourStateValue::Narrow(narrow_word(1, 0)), &mut log);
        engine.commit_write(cell_b, FourStateValue::Narrow(narrow_word(2, 0)), &mut log);
        engine.commit_write(cell_c, FourStateValue::Narrow(narrow_word(3, 0)), &mut log);

        log.rollback_to(&mut engine, mark)
            .expect("mark is well within the retained log");

        for cell in [cell_a, cell_b, cell_c] {
            assert_eq!(
                narrow_at(&engine, cell),
                narrow_word(0, 0),
                "every cell written since `mark` must be back to its pre-write value"
            );
        }
    }

    /// ST-036: write A, take `mark`, write B and C, `rollback_to(mark)`; A's
    /// write must survive (still the post-write value) while B and C are
    /// undone. Fails if `rollback_to` always rewinds the whole log
    /// regardless of the marker.
    #[test]
    fn rollback_partial_marker_only_undoes_writes_after_it() {
        let mut engine = fresh_engine();
        let cell_a = inline_cell(&mut engine);
        let cell_b = inline_cell(&mut engine);
        let cell_c = inline_cell(&mut engine);
        let mut log = UndoLog::new();

        engine.commit_write(cell_a, FourStateValue::Narrow(narrow_word(1, 0)), &mut log);
        let mark = log.checkpoint_marker();
        engine.commit_write(cell_b, FourStateValue::Narrow(narrow_word(2, 0)), &mut log);
        engine.commit_write(cell_c, FourStateValue::Narrow(narrow_word(3, 0)), &mut log);

        log.rollback_to(&mut engine, mark)
            .expect("mark is well within the retained log");

        assert_eq!(
            narrow_at(&engine, cell_a),
            narrow_word(1, 0),
            "A's write predates `mark` and must survive"
        );
        assert_eq!(
            narrow_at(&engine, cell_b),
            narrow_word(0, 0),
            "B's write postdates `mark` and must be undone"
        );
        assert_eq!(
            narrow_at(&engine, cell_c),
            narrow_word(0, 0),
            "C's write postdates `mark` and must be undone"
        );
    }

    /// Append entries (via real `commit_write` calls, each stamped with a
    /// distinct `SimTime` via `set_current_time`) at times 1, 2, 3;
    /// `fossil_collect(SimTime{sim_units: 2,..})`; the log's remaining
    /// length must reflect only the `t=3` entry — and, critically, a
    /// subsequent `rollback_to` targeting a marker *before* the
    /// fossil-collected entries must now return
    /// `Err(RewindError::PastFossilHorizon)` rather than silently
    /// under-rolling-back.
    #[test]
    fn fossil_collect_trims_entries_at_or_before_gvt_never_past_it() {
        let mut engine = fresh_engine();
        let cell_a = inline_cell(&mut engine);
        let cell_b = inline_cell(&mut engine);
        let cell_c = inline_cell(&mut engine);
        let mut log = UndoLog::new();

        let mark_before_any = log.checkpoint_marker();

        engine.set_current_time(t(1));
        engine.commit_write(cell_a, FourStateValue::Narrow(narrow_word(1, 0)), &mut log);
        engine.set_current_time(t(2));
        engine.commit_write(cell_b, FourStateValue::Narrow(narrow_word(2, 0)), &mut log);
        engine.set_current_time(t(3));
        engine.commit_write(cell_c, FourStateValue::Narrow(narrow_word(3, 0)), &mut log);

        log.fossil_collect(t(2));
        assert_eq!(
            log.retained_len(),
            1,
            "only the t=3 entry (strictly after gvt=2) must remain"
        );

        let result = log.rollback_to(&mut engine, mark_before_any);
        assert_eq!(
            result,
            Err(RewindError::PastFossilHorizon),
            "a marker before the fossil-collected horizon must fail loudly, never silently under-roll-back"
        );
    }

    /// Write distinct values to 4 inline words; `snapshot(Some((Inline, 1,
    /// 2)))` (only words 1-2); mutate word 1 to something else; `restore`
    /// the partial snapshot; word 1 must be back to its snapshotted value
    /// *and* words 0/3 (outside the snapshotted range) must be unaffected —
    /// proving it's genuinely a slice operation, not silently promoted to a
    /// full-arena restore.
    #[test]
    fn snapshot_restore_round_trips_a_partial_range_not_just_the_whole_arena() {
        let mut engine = fresh_engine();
        let cells: Vec<StateCellId> = (0..4).map(|_| inline_cell(&mut engine)).collect();
        for (i, &cell) in cells.iter().enumerate() {
            engine.commit_write(
                cell,
                FourStateValue::Narrow(narrow_word(i as u64 + 1, 0)),
                &mut (),
            );
        }

        let snap = engine.snapshot(Some((SlotClass::Inline, 1, 2)));

        engine.commit_write(
            cells[1],
            FourStateValue::Narrow(narrow_word(99, 0)),
            &mut (),
        );

        engine
            .restore(&snap)
            .expect("same engine, same layout hash, in-bounds range");

        assert_eq!(
            narrow_at(&engine, cells[1]),
            narrow_word(2, 0),
            "word 1 must be back to its snapshotted value"
        );
        assert_eq!(
            narrow_at(&engine, cells[0]),
            narrow_word(1, 0),
            "word 0 is outside the snapshotted range and must be unaffected"
        );
        assert_eq!(
            narrow_at(&engine, cells[3]),
            narrow_word(4, 0),
            "word 3 is outside the snapshotted range and must be unaffected"
        );
    }

    /// Snapshot a `StateEngine` built from template set A; construct a
    /// *different* `StateEngine` from template set B (different
    /// `layout_hash`); `restore` A's snapshot into B; must return
    /// `Err(LayoutMismatch)`, and B's arena contents must be byte-identical
    /// to before the attempted restore — no partial corruption on the
    /// rejected path.
    #[test]
    fn restore_with_a_layout_hash_mismatch_is_a_typed_error_never_silent_corruption() {
        let templates_a = TemplateRegistry::new();
        let tmpl_a = TemplateKey {
            definition: 100,
            params_hash: 0,
        };
        // SAFETY: `templates_a` is a local, single-owned value with no other
        // live borrow and no concurrent caller.
        unsafe {
            templates_a.register(
                tmpl_a,
                StateLayout {
                    slots: vec![],
                    inline_words: 1,
                    wide_words: 0,
                },
            );
        }
        let mut engine_a = StateEngine::new(templates_a);
        let handle_a = engine_a
            .allocate_instance(tmpl_a)
            .expect("tmpl_a is registered");
        drop(handle_a);
        let snap_a = engine_a.snapshot(None);

        let templates_b = TemplateRegistry::new();
        let tmpl_b = TemplateKey {
            definition: 200,
            params_hash: 0,
        };
        // SAFETY: same reasoning as `templates_a` above.
        unsafe {
            templates_b.register(
                tmpl_b,
                StateLayout {
                    slots: vec![],
                    inline_words: 1,
                    wide_words: 0,
                },
            );
        }
        let mut engine_b = StateEngine::new(templates_b);
        let handle_b = engine_b
            .allocate_instance(tmpl_b)
            .expect("tmpl_b is registered");
        let cell_b = engine_b.alloc_cell(SlotLocation {
            class: SlotClass::Inline,
            word_offset: handle_b.base.inline_base,
            bit_width: 8,
            elem_word_count: 1,
            row_stride_words: 0,
            num_rows: 0,
        });
        engine_b.commit_write(
            cell_b,
            FourStateValue::Narrow(narrow_word(0x2A, 0)),
            &mut (),
        );
        drop(handle_b);

        let before: Vec<u128> = engine_b.arena.inline().to_vec();

        let result = engine_b.restore(&snap_a);
        assert_eq!(
            result,
            Err(RewindError::LayoutMismatch),
            "restoring across two different template sets must be rejected"
        );

        assert_eq!(
            engine_b.arena.inline().to_vec(),
            before,
            "a rejected restore must never partially corrupt the target arena"
        );
    }

    /// A template with one slot initialized to `8'hAA` and one uninitialized
    /// `logic [7:0]`; mutate both away from their reset state;
    /// `reset_to_initial`; the first must read back `0xAA` known, the second
    /// must read back all-X (`val=0, mask=0xFF`).
    #[test]
    fn reset_to_initial_reblits_declared_initializers_and_x_fills_the_rest() {
        let templates = TemplateRegistry::new();
        let tmpl = TemplateKey {
            definition: 42,
            params_hash: 0,
        };
        let initial_value = FourStateValue::Narrow(0xAA);
        // SAFETY: `templates` is a local, single-owned value with no other
        // live borrow and no concurrent caller.
        unsafe {
            templates.register(
                tmpl,
                StateLayout {
                    slots: vec![
                        SlotDescriptor {
                            key: SymbolKey(0),
                            offset: SlotOffset {
                                class: SlotClass::Inline,
                                word_offset: 0,
                                bit_width: 8,
                                elem_word_count: 1,
                                row_stride_words: 0,
                                num_rows: 0,
                            },
                            initial: Some(initial_value),
                            net_info: None,
                        },
                        SlotDescriptor {
                            key: SymbolKey(1),
                            offset: SlotOffset {
                                class: SlotClass::Inline,
                                word_offset: 1,
                                bit_width: 8,
                                elem_word_count: 1,
                                row_stride_words: 0,
                                num_rows: 0,
                            },
                            initial: None,
                            net_info: None,
                        },
                    ],
                    inline_words: 2,
                    wide_words: 0,
                },
            );
        }
        let mut engine = StateEngine::new(templates);
        let handle = engine.allocate_instance(tmpl).expect("tmpl is registered");
        let cell_initialized = handle.cell_for_slot(0);
        let cell_uninitialized = handle.cell_for_slot(1);
        drop(handle);

        // Mutate both away from their reset state.
        engine.commit_write(
            cell_initialized,
            FourStateValue::Narrow(narrow_word(0x11, 0)),
            &mut (),
        );
        engine.commit_write(
            cell_uninitialized,
            FourStateValue::Narrow(narrow_word(0x22, 0)),
            &mut (),
        );

        engine.reset_to_initial();

        let initialized = narrow_at(&engine, cell_initialized);
        assert_eq!(
            initialized as u64 & 0xFF,
            0xAA,
            "the declared initializer must be re-blitted exactly"
        );
        assert_eq!(
            (initialized >> 64) as u64 & 0xFF,
            0,
            "a fully-known initializer has no unknown bits"
        );

        let uninitialized = narrow_at(&engine, cell_uninitialized);
        assert_eq!(
            uninitialized as u64 & 0xFF,
            0,
            "an uninitialized slot's value half must reset to 0"
        );
        assert_eq!(
            (uninitialized >> 64) as u64 & 0xFF,
            0xFF,
            "an uninitialized slot must reset to all-X (mask=all-1) within its width"
        );
    }

    /// **Review fix (Task 16 r1, blocking finding 1).** A `BuildMode::TwoState`
    /// engine's declared-initializer and uninitialized inline slots, mutated
    /// through the *actual live* 2-state plane (`write_inline_2s`, Task 13 —
    /// `write_slot`/`commit_write` only ever touch the inert, always-zero
    /// 4-state planes in a `TwoState` build); `reset_to_initial()` must
    /// observe and affect that same live plane. Before this fix,
    /// `reset_to_initial` unconditionally called `write_slot` (4-state-only),
    /// so it silently did nothing to either cell's real data.
    #[test]
    fn reset_to_initial_is_build_mode_aware_for_two_state_engines() {
        let mut engine = StateEngine::new_with_mode(TemplateRegistry::new(), BuildMode::TwoState);
        assert_eq!(engine.build_mode(), BuildMode::TwoState);

        let cell_initialized = inline_cell(&mut engine);
        let cell_uninitialized = inline_cell(&mut engine);
        // `cell_reset` is `pub(crate)`, directly pokeable from within this
        // crate — the same shortcut `write::StateEngine::alloc_cell` and
        // `instance::StateEngine::allocate_instance` themselves use, standing
        // in here for a full `allocate_instance`/`TemplateRegistry` round
        // trip this test doesn't otherwise need.
        engine.cell_reset[cell_initialized.0 as usize] =
            CellReset::Initial(FourStateValue::Narrow(0xAA));
        // `cell_uninitialized` keeps `alloc_cell`'s own conservative
        // `CellReset::AllX` default.

        let loc_initialized = engine.cells[cell_initialized.0 as usize];
        let loc_uninitialized = engine.cells[cell_uninitialized.0 as usize];

        write_inline_2s(&engine.arena, loc_initialized.word_offset, 0x11);
        write_inline_2s(&engine.arena, loc_uninitialized.word_offset, 0x22);

        engine.reset_to_initial();

        assert_eq!(
            read_inline_2s(&engine.arena, loc_initialized.word_offset),
            0xAA,
            "a declared initializer must be re-blitted into the live 2-state plane"
        );
        assert_eq!(
            read_inline_2s(&engine.arena, loc_uninitialized.word_offset),
            0,
            "an uninitialized 2-state slot must reset to 0, not all-X (there is no mask half in this plane)"
        );
    }

    /// **Review fix (Task 16 r1, blocking finding 1), the `Wide`-class half:**
    /// same shape as
    /// `reset_to_initial_is_build_mode_aware_for_two_state_engines` above, but
    /// for a wide (`elem_word_count > 1`) 2-state slot — proving the fix
    /// covers the `wide_2s` plane, not just `inline_2s`.
    #[test]
    fn reset_to_initial_two_state_wide_all_x_resets_every_word_to_zero() {
        let mut engine = StateEngine::new_with_mode(TemplateRegistry::new(), BuildMode::TwoState);
        // SAFETY: local, single-owned engine; no other live borrow of the
        // wide plane, and this test performs no concurrent allocation.
        let word_offset = unsafe { engine.arena.alloc_wide_words(2) };
        let loc = SlotLocation {
            class: SlotClass::Wide,
            word_offset,
            bit_width: 128,
            elem_word_count: 2,
            row_stride_words: 0,
            num_rows: 0,
        };
        engine.alloc_cell(loc); // keeps `alloc_cell`'s own `CellReset::AllX` default

        write_wide_2s(&engine.arena, word_offset, &[0x1111_1111, 0x2222_2222]);
        assert_eq!(
            read_wide_2s(&engine.arena, word_offset, 2),
            &[0x1111_1111, 0x2222_2222]
        );

        engine.reset_to_initial();

        assert_eq!(
            read_wide_2s(&engine.arena, word_offset, 2),
            &[0, 0],
            "an uninitialized wide 2-state slot must reset to all-zero words"
        );
    }

    /// **Review fix (Task 16 r1, blocking finding 1).** `snapshot`/`restore`'s
    /// partial-range slice semantics (already proven for `FourState` by
    /// `snapshot_restore_round_trips_a_partial_range_not_just_the_whole_arena`
    /// above), re-proven against a `BuildMode::TwoState` engine's *live*
    /// `inline_2s` plane. Before this fix, `snapshot`/`restore` unconditionally
    /// captured/restored the inert 4-state planes, so this would have silently
    /// left `word 1`'s real (2-state) value at its mutated `99`, not its
    /// snapshotted `2`.
    #[test]
    fn snapshot_restore_two_state_round_trips_the_live_plane_not_the_inert_four_state_one() {
        let mut engine = StateEngine::new_with_mode(TemplateRegistry::new(), BuildMode::TwoState);
        let cells: Vec<StateCellId> = (0..4).map(|_| inline_cell(&mut engine)).collect();
        let offsets: Vec<u32> = cells
            .iter()
            .map(|&c| engine.cells[c.0 as usize].word_offset)
            .collect();
        for (i, &off) in offsets.iter().enumerate() {
            write_inline_2s(&engine.arena, off, i as u64 + 1);
        }

        let snap = engine.snapshot(Some((SlotClass::Inline, offsets[1], 2)));

        write_inline_2s(&engine.arena, offsets[1], 99);

        engine
            .restore(&snap)
            .expect("same engine, same layout hash, same build mode, in-bounds range");

        assert_eq!(
            read_inline_2s(&engine.arena, offsets[1]),
            2,
            "word 1 must be back to its snapshotted 2-state value"
        );
        assert_eq!(
            read_inline_2s(&engine.arena, offsets[0]),
            1,
            "word 0 is outside the snapshotted range and must be unaffected"
        );
        assert_eq!(
            read_inline_2s(&engine.arena, offsets[3]),
            4,
            "word 3 is outside the snapshotted range and must be unaffected"
        );
    }

    /// **Review fix (Task 16 r1, blocking finding 1), the cross-mode-rejection
    /// half:** a snapshot taken from a `FourState` engine, `restore`d against a
    /// `TwoState` engine with the *same* (empty) template set — so
    /// `layout_hash` alone would not catch the mismatch — must be rejected
    /// with `Err(LayoutMismatch)` before touching any plane, never silently
    /// interpreted as 4-state data landing in the 2-state target's arena.
    #[test]
    fn restore_rejects_a_build_mode_mismatch_even_when_layout_hash_matches() {
        let mut four_state_engine =
            StateEngine::new_with_mode(TemplateRegistry::new(), BuildMode::FourState);
        let cell = inline_cell(&mut four_state_engine);
        four_state_engine.commit_write(cell, FourStateValue::Narrow(narrow_word(0x2A, 0)), &mut ());
        let snap = four_state_engine.snapshot(None);

        let mut two_state_engine =
            StateEngine::new_with_mode(TemplateRegistry::new(), BuildMode::TwoState);
        let two_cell = inline_cell(&mut two_state_engine);
        let loc = two_state_engine.cells[two_cell.0 as usize];
        write_inline_2s(&two_state_engine.arena, loc.word_offset, 0x77);
        let before = two_state_engine.arena.inline_2s().to_vec();

        let result = two_state_engine.restore(&snap);
        assert_eq!(
            result,
            Err(RewindError::LayoutMismatch),
            "restoring a FourState snapshot into a TwoState engine must be rejected"
        );
        assert_eq!(
            two_state_engine.arena.inline_2s().to_vec(),
            before,
            "a rejected cross-build-mode restore must never partially corrupt the target arena"
        );
    }

    /// **Review fix (Task 16 r1, blocking finding 2).** Reproduces the exact
    /// scenario the finding reported: force a net (via `driver::force_driver`,
    /// a live SV `force` statement), confirm the returned contribution cell
    /// reads back the forced value, then `reset_to_initial()`. Before this
    /// fix, `reset_to_initial` iterated every `CellReset::AllX` entry
    /// unconditionally — including `force_driver`'s synthetic contribution
    /// cells, which share the ordinary inline plane and are indistinguishable
    /// from a real variable once `alloc_cell` has run — and blitted all-X
    /// over the live forced value with no error of any kind.
    #[test]
    fn reset_to_initial_never_corrupts_a_live_force_contribution_cell() {
        let mut engine = fresh_engine();
        let net_cell = inline_cell(&mut engine);
        let mut set = crate::state::driver::DriverSet {
            resolved: net_cell,
            drivers: Vec::new(),
            net_kind: crate::state::NetKind::Wire,
        };

        let forced_cell = crate::state::driver::force_driver(
            &mut engine,
            &mut set,
            net_cell,
            FourStateValue::Narrow(narrow_word(0x2A, 0)),
        );
        assert_eq!(
            narrow_at(&engine, forced_cell),
            narrow_word(0x2A, 0),
            "force_driver must seed its own contribution cell with the forced value"
        );

        engine.reset_to_initial();

        assert_eq!(
            narrow_at(&engine, forced_cell),
            narrow_word(0x2A, 0),
            "reset_to_initial must never blit a reset value over a live force_driver contribution cell"
        );
    }
}