Skip to main content

bones_core/clock/
ops.rs

1//! ITC operations: fork, join, event, peek, leq, concurrent.
2//!
3//! Implements the core Interval Tree Clock operations from:
4//! Almeida, Baquero & Fonte (2008) "Interval Tree Clocks".
5//!
6//! These operations form the public API consumed by the CRDT layer
7//! for causal comparison and LWW tie-breaking.
8
9use super::itc::{Event, Id, Stamp};
10
11// ===========================================================================
12// Id operations (split / sum)
13// ===========================================================================
14
15/// Split an ID tree into two halves. The original interval is partitioned
16/// so that left ∪ right = original and left ∩ right = ∅.
17fn split_id(id: &Id) -> (Id, Id) {
18    match id {
19        Id::Zero => (Id::zero(), Id::zero()),
20        Id::One => (
21            Id::branch(Id::one(), Id::zero()),
22            Id::branch(Id::zero(), Id::one()),
23        ),
24        Id::Branch(l, r) => {
25            if !l.is_zero() && r.is_zero() {
26                // Only left has ownership — split the left subtree
27                let (ll, lr) = split_id(l);
28                (Id::branch(ll, Id::zero()), Id::branch(lr, Id::zero()))
29            } else if l.is_zero() && !r.is_zero() {
30                // Only right has ownership — split the right subtree
31                let (rl, rr) = split_id(r);
32                (Id::branch(Id::zero(), rl), Id::branch(Id::zero(), rr))
33            } else {
34                // Both have ownership — give left to one, right to the other
35                (
36                    Id::branch((**l).clone(), Id::zero()),
37                    Id::branch(Id::zero(), (**r).clone()),
38                )
39            }
40        }
41    }
42}
43
44/// Merge two ID trees into one (the union of their intervals).
45fn sum_id(a: &Id, b: &Id) -> Id {
46    match (a, b) {
47        (Id::Zero, _) => b.clone(),
48        (_, Id::Zero) => a.clone(),
49        (Id::Branch(al, ar), Id::Branch(bl, br)) => Id::branch(sum_id(al, bl), sum_id(ar, br)),
50        // (One, anything-non-zero) or (anything-non-zero, One) — both own some
51        // part, and since ITC invariant says intervals don't overlap, this
52        // can only happen when merging complementary halves → result is One.
53        _ => Id::one(),
54    }
55}
56
57// ===========================================================================
58// Event operations (join, leq, fill, grow)
59// ===========================================================================
60
61/// Join (merge) two event trees, taking the pointwise maximum.
62fn join_event(a: &Event, b: &Event) -> Event {
63    match (a, b) {
64        (Event::Leaf(na), Event::Leaf(nb)) => Event::leaf((*na).max(*nb)),
65        (Event::Leaf(na), Event::Branch(nb, bl, br)) => {
66            if *na >= b.max_value() {
67                Event::leaf(*na)
68            } else {
69                let lifted_a_l = Event::leaf(na.saturating_sub(*nb));
70                let lifted_a_r = Event::leaf(na.saturating_sub(*nb));
71                Event::branch(
72                    *nb,
73                    join_event(&lifted_a_l, bl),
74                    join_event(&lifted_a_r, br),
75                )
76            }
77        }
78        (Event::Branch(na, al, ar), Event::Leaf(nb)) => {
79            if *nb >= a.max_value() {
80                Event::leaf(*nb)
81            } else {
82                let lifted_b_l = Event::leaf(nb.saturating_sub(*na));
83                let lifted_b_r = Event::leaf(nb.saturating_sub(*na));
84                Event::branch(
85                    *na,
86                    join_event(al, &lifted_b_l),
87                    join_event(ar, &lifted_b_r),
88                )
89            }
90        }
91        (Event::Branch(na, al, ar), Event::Branch(nb, bl, br)) => {
92            if na >= nb {
93                // a's base is higher — lift a's children by the diff,
94                // use b's base (the lower), and merge.
95                let diff = na - nb;
96                let lifted_a_left = (**al).clone().lift(diff);
97                let lifted_a_right = (**ar).clone().lift(diff);
98                Event::branch(
99                    *nb,
100                    join_event(&lifted_a_left, bl),
101                    join_event(&lifted_a_right, br),
102                )
103            } else {
104                // b's base is higher — lift b's children by the diff,
105                // use a's base (the lower), and merge.
106                let diff = nb - na;
107                let lifted_b_left = (**bl).clone().lift(diff);
108                let lifted_b_right = (**br).clone().lift(diff);
109                Event::branch(
110                    *na,
111                    join_event(al, &lifted_b_left),
112                    join_event(ar, &lifted_b_right),
113                )
114            }
115        }
116    }
117}
118
119/// Causal ordering: returns true if event tree `a` ≤ event tree `b`
120/// (every position in `a` has count ≤ the corresponding position in `b`).
121fn leq_event(a: &Event, b: &Event) -> bool {
122    match (a, b) {
123        (Event::Leaf(na), Event::Leaf(nb)) => na <= nb,
124        (Event::Leaf(na), Event::Branch(nb, bl, br)) => {
125            // a is flat at *na; b has base *nb plus children.
126            // We need na ≤ nb + bl[pos] and na ≤ nb + br[pos] for all positions.
127            // Since na is flat: if na ≤ nb, then certainly na ≤ nb + child for all children (children ≥ 0).
128            // Otherwise, we need (na - nb) ≤ every value in child.
129            if *na <= *nb {
130                true
131            } else {
132                let remainder = na - nb;
133                leq_event(&Event::leaf(remainder), bl) && leq_event(&Event::leaf(remainder), br)
134            }
135        }
136        (Event::Branch(_na, _al, _ar), Event::Leaf(nb)) => {
137            // a has structure, b is flat.
138            // Need na + al[pos] ≤ nb and na + ar[pos] ≤ nb for all positions.
139            // This means a.max_value() ≤ nb.
140            a.max_value() <= *nb
141        }
142        (Event::Branch(na, al, ar), Event::Branch(nb, bl, br)) => {
143            // We need: na + al(pos) <= nb + bl(pos) for all positions.
144            // Equivalently: al(pos) <= bl(pos) + (nb - na) when nb >= na,
145            // or: al(pos) + (na - nb) <= bl(pos) when na > nb.
146            if na <= nb {
147                let diff = nb - na;
148                // Lift b's children by diff: al <= lift(bl, diff)
149                let lifted_b_left = (**bl).clone().lift(diff);
150                let lifted_b_right = (**br).clone().lift(diff);
151                leq_event(al, &lifted_b_left) && leq_event(ar, &lifted_b_right)
152            } else {
153                let diff = na - nb;
154                // Lift a's children by diff: lift(al, diff) <= bl
155                let lifted_a_left = (**al).clone().lift(diff);
156                let lifted_a_right = (**ar).clone().lift(diff);
157                leq_event(&lifted_a_left, bl) && leq_event(&lifted_a_right, br)
158            }
159        }
160    }
161}
162
163/// Fill the event tree where the ID owns the interval, up to the
164/// maximum possible without exceeding the existing counters.
165///
166/// Returns `(filled_event, did_change)`.
167fn fill(id: &Id, event: &Event) -> (Event, bool) {
168    match (id, event) {
169        (Id::Zero, _) | (Id::One, Event::Leaf(_)) => (event.clone(), false),
170        (Id::One, Event::Branch(n, l, r)) => {
171            // Fill everything — find the max of the children and collapse
172            let max_child = l.max_value().max(r.max_value());
173            (Event::leaf(n + max_child), true)
174        }
175        (Id::Branch(il, ir), Event::Leaf(n)) => {
176            // Expand the leaf into a branch so we can fill selectively
177            let (el, changed_l) = fill(il, &Event::leaf(0));
178            let (er, changed_r) = fill(ir, &Event::leaf(0));
179            if changed_l || changed_r {
180                (Event::branch(*n, el, er), true)
181            } else {
182                (Event::Leaf(*n), false)
183            }
184        }
185        (Id::Branch(il, ir), Event::Branch(n, el, er)) => {
186            let (new_l, changed_l) = fill(il, el);
187            let (new_r, changed_r) = fill(ir, er);
188            if changed_l || changed_r {
189                (Event::branch(*n, new_l, new_r), true)
190            } else {
191                (event.clone(), false)
192            }
193        }
194    }
195}
196
197/// Grow the event tree by inflating at a position where the ID owns the interval.
198///
199/// Returns `(new_event, cost)` where cost is the increase in node count
200/// (used to pick the minimal growth). Returns `None` if growth isn't possible
201/// (e.g., anonymous ID).
202fn grow(id: &Id, event: &Event) -> Option<(Event, u32)> {
203    match (id, event) {
204        (Id::One, Event::Leaf(n)) => {
205            // Simple increment at a fully-owned leaf
206            Some((Event::leaf(n + 1), 0))
207        }
208        (Id::Zero, _) => None,
209        (Id::One, Event::Branch(n, l, r)) => {
210            // We own everything — try growing left or right, pick cheapest
211            let opt_l = grow(&Id::one(), l);
212            let opt_r = grow(&Id::one(), r);
213            match (opt_l, opt_r) {
214                (Some((new_l, cl)), Some((new_r, cr))) => {
215                    if cl <= cr {
216                        Some((Event::branch(*n, new_l, (**r).clone()), cl))
217                    } else {
218                        Some((Event::branch(*n, (**l).clone(), new_r), cr))
219                    }
220                }
221                (Some((new_l, cl)), None) => Some((Event::branch(*n, new_l, (**r).clone()), cl)),
222                (None, Some((new_r, cr))) => Some((Event::branch(*n, (**l).clone(), new_r), cr)),
223                (None, None) => None,
224            }
225        }
226        (Id::Branch(il, ir), Event::Leaf(n)) => {
227            // Event is a leaf but ID has structure — expand into branch
228            let opt_l = grow(il, &Event::leaf(0));
229            let opt_r = grow(ir, &Event::leaf(0));
230            match (opt_l, opt_r) {
231                (Some((new_l, cl)), Some((new_r, cr))) => {
232                    if cl < cr {
233                        Some((Event::branch(*n, new_l, Event::leaf(0)), cl + 1_000))
234                    } else {
235                        Some((Event::branch(*n, Event::leaf(0), new_r), cr + 1_000))
236                    }
237                }
238                (Some((new_l, cl)), None) => {
239                    Some((Event::branch(*n, new_l, Event::leaf(0)), cl + 1_000))
240                }
241                (None, Some((new_r, cr))) => {
242                    Some((Event::branch(*n, Event::leaf(0), new_r), cr + 1_000))
243                }
244                (None, None) => None,
245            }
246        }
247        (Id::Branch(il, ir), Event::Branch(n, el, er)) => {
248            let opt_l = grow(il, el);
249            let opt_r = grow(ir, er);
250            match (opt_l, opt_r) {
251                (Some((new_l, cl)), Some((new_r, cr))) => {
252                    if cl <= cr {
253                        Some((Event::branch(*n, new_l, (**er).clone()), cl))
254                    } else {
255                        Some((Event::branch(*n, (**el).clone(), new_r), cr))
256                    }
257                }
258                (Some((new_l, cl)), None) => Some((Event::branch(*n, new_l, (**er).clone()), cl)),
259                (None, Some((new_r, cr))) => Some((Event::branch(*n, (**el).clone(), new_r), cr)),
260                (None, None) => None,
261            }
262        }
263    }
264}
265
266// ===========================================================================
267// Public Stamp operations
268// ===========================================================================
269
270impl Stamp {
271    /// Split this stamp's ID interval into two halves.
272    ///
273    /// Used when a new agent forks from an existing one.
274    /// Returns `(left, right)` where `left` and `right` partition
275    /// the original interval: `left ∪ right = original`, `left ∩ right = ∅`.
276    ///
277    /// Both stamps share the same event tree (causal history at time of fork).
278    ///
279    /// # Panics
280    ///
281    /// Panics if this stamp is anonymous (owns no interval to split).
282    #[must_use]
283    pub fn fork(&self) -> (Self, Self) {
284        assert!(
285            !self.id.is_zero(),
286            "cannot fork an anonymous stamp (owns no interval)"
287        );
288        let (id_l, id_r) = split_id(&self.id);
289        (
290            Self::new(id_l, self.event.clone()).normalize(),
291            Self::new(id_r, self.event.clone()).normalize(),
292        )
293    }
294
295    /// Merge two stamps into one, combining their ID intervals and
296    /// taking the pointwise maximum of their event trees.
297    ///
298    /// Used when an agent retires and donates its interval back, or
299    /// when synchronizing causality information between agents.
300    #[must_use]
301    pub fn join(a: &Self, b: &Self) -> Self {
302        let id = sum_id(&a.id, &b.id);
303        let event = join_event(&a.event, &b.event);
304        Self::new(id, event).normalize()
305    }
306
307    /// Record a new event, inflating the event tree.
308    ///
309    /// Called on every event emission. The event counter is monotonically
310    /// increased at a position owned by this stamp's ID. Uses the
311    /// fill-then-grow strategy from the ITC paper for minimal tree growth.
312    ///
313    /// # Panics
314    ///
315    /// Panics if this stamp is anonymous (cannot record events without
316    /// owning part of the interval).
317    pub fn event(&mut self) {
318        assert!(
319            !self.id.is_zero(),
320            "cannot record event on an anonymous stamp"
321        );
322
323        // First try to fill — collapse structure where we own everything
324        let (filled, changed) = fill(&self.id, &self.event);
325        if changed {
326            self.event = filled;
327            // Normalize after fill
328            *self = self.clone().normalize();
329            return;
330        }
331
332        // Fill didn't help — grow the event tree
333        if let Some((grown, _cost)) = grow(&self.id, &self.event) {
334            self.event = grown;
335            *self = self.clone().normalize();
336        } else {
337            // This should not happen if the stamp owns an interval
338            panic!("event: could not grow event tree (internal error)");
339        }
340    }
341
342    /// Read the current event tree without incrementing.
343    #[must_use]
344    pub const fn peek(&self) -> &Event {
345        &self.event
346    }
347
348    /// Causal dominance: returns `true` if `self` happened-before-or-equal `other`.
349    ///
350    /// This means every event recorded by `self` is also recorded by `other`.
351    #[must_use]
352    pub fn leq(&self, other: &Self) -> bool {
353        leq_event(&self.event, &other.event)
354    }
355
356    /// Returns `true` if neither stamp causally dominates the other.
357    ///
358    /// Two stamps are concurrent if there exist events in each that the
359    /// other has not observed.
360    #[must_use]
361    pub fn concurrent(&self, other: &Self) -> bool {
362        !self.leq(other) && !other.leq(self)
363    }
364}
365
366// ===========================================================================
367// Tests
368// ===========================================================================
369
370#[cfg(test)]
371mod tests {
372    use super::*;
373    use proptest::prelude::*;
374
375    // === fork ===============================================================
376
377    #[test]
378    fn fork_seed_produces_two_halves() {
379        let seed = Stamp::seed();
380        let (left, right) = seed.fork();
381
382        // Each half owns part of the interval
383        assert!(!left.id.is_zero());
384        assert!(!right.id.is_zero());
385        // Neither owns the full interval
386        assert!(!left.id.is_one());
387        assert!(!right.id.is_one());
388        // Both share the same (zero) event tree
389        assert_eq!(left.event, Event::zero());
390        assert_eq!(right.event, Event::zero());
391    }
392
393    #[test]
394    fn fork_preserves_interval_coverage() {
395        let seed = Stamp::seed();
396        let (left, right) = seed.fork();
397        // Joining the IDs should recover the full interval
398        let reunited = sum_id(&left.id, &right.id);
399        assert_eq!(reunited, Id::one());
400    }
401
402    #[test]
403    fn fork_ids_are_disjoint() {
404        let seed = Stamp::seed();
405        let (left, right) = seed.fork();
406        // The expected split of seed (1) is (1,0) and (0,1)
407        assert_eq!(left.id, Id::branch(Id::one(), Id::zero()));
408        assert_eq!(right.id, Id::branch(Id::zero(), Id::one()));
409    }
410
411    #[test]
412    fn fork_of_half_further_splits() {
413        let seed = Stamp::seed();
414        let (left, _) = seed.fork();
415        let (ll, lr) = left.fork();
416        // ll and lr should subdivide the left half
417        assert!(!ll.id.is_zero());
418        assert!(!lr.id.is_zero());
419        // Reuniting them gives back the original left ID
420        let reunited = sum_id(&ll.id, &lr.id);
421        assert_eq!(reunited, Id::branch(Id::one(), Id::zero()));
422    }
423
424    #[test]
425    fn fork_preserves_event_history() {
426        let mut s = Stamp::seed();
427        s.event();
428        s.event();
429        let (left, right) = s.fork();
430        // Both children inherit the parent's event tree
431        assert_eq!(left.event, s.event);
432        assert_eq!(right.event, s.event);
433    }
434
435    #[test]
436    #[should_panic(expected = "cannot fork an anonymous stamp")]
437    fn fork_anonymous_panics() {
438        let anon = Stamp::anonymous();
439        let _ = anon.fork();
440    }
441
442    // === join ===============================================================
443
444    #[test]
445    fn join_recovers_seed_from_fork() {
446        let seed = Stamp::seed();
447        let (left, right) = seed.fork();
448        let joined = Stamp::join(&left, &right);
449        assert_eq!(joined.id, Id::one());
450        assert_eq!(joined.event, Event::zero());
451    }
452
453    #[test]
454    fn join_merges_divergent_events() {
455        let seed = Stamp::seed();
456        let (mut a, mut b) = seed.fork();
457        a.event();
458        b.event();
459        b.event();
460
461        let joined = Stamp::join(&a, &b);
462        // Joined should dominate both
463        assert!(a.leq(&joined));
464        assert!(b.leq(&joined));
465    }
466
467    #[test]
468    fn join_with_anonymous() {
469        let seed = Stamp::seed();
470        let anon = Stamp::anonymous();
471        let joined = Stamp::join(&seed, &anon);
472        assert_eq!(joined.id, Id::one());
473        assert_eq!(joined.event, Event::zero());
474    }
475
476    #[test]
477    fn join_is_commutative() {
478        let seed = Stamp::seed();
479        let (mut a, mut b) = seed.fork();
480        a.event();
481        b.event();
482        b.event();
483
484        let ab = Stamp::join(&a, &b);
485        let ba = Stamp::join(&b, &a);
486        assert_eq!(ab, ba);
487    }
488
489    // === event ==============================================================
490
491    #[test]
492    fn event_monotonically_increases() {
493        let mut s = Stamp::seed();
494        let before = s.event.max_value();
495        s.event();
496        let after = s.event.max_value();
497        assert!(after > before, "event must increase: {before} -> {after}");
498    }
499
500    #[test]
501    fn event_multiple_increments() {
502        let mut s = Stamp::seed();
503        for i in 1..=10 {
504            s.event();
505            assert!(
506                s.event.max_value() >= i,
507                "after {i} events, max_value should be >= {i}"
508            );
509        }
510    }
511
512    #[test]
513    fn event_on_forked_stamp() {
514        let seed = Stamp::seed();
515        let (mut a, _b) = seed.fork();
516        a.event();
517        assert!(a.event.max_value() >= 1);
518    }
519
520    #[test]
521    #[should_panic(expected = "cannot record event on an anonymous stamp")]
522    fn event_anonymous_panics() {
523        let mut anon = Stamp::anonymous();
524        anon.event();
525    }
526
527    // === peek ===============================================================
528
529    #[test]
530    fn peek_returns_event_ref() {
531        let s = Stamp::seed();
532        assert_eq!(s.peek(), &Event::zero());
533    }
534
535    #[test]
536    fn peek_reflects_events() {
537        let mut s = Stamp::seed();
538        s.event();
539        let peeked = s.peek();
540        assert!(peeked.max_value() >= 1);
541    }
542
543    // === leq ===============================================================
544
545    #[test]
546    fn leq_identical_stamps() {
547        let s = Stamp::seed();
548        assert!(s.leq(&s));
549    }
550
551    #[test]
552    fn leq_after_event() {
553        let mut s = Stamp::seed();
554        let before = s.clone();
555        s.event();
556        assert!(before.leq(&s), "before should be <= after event");
557        assert!(!s.leq(&before), "after event should NOT be <= before");
558    }
559
560    #[test]
561    fn leq_forked_then_diverged() {
562        let seed = Stamp::seed();
563        let (mut a, mut b) = seed.fork();
564        a.event();
565        b.event();
566        // After independent events, neither dominates
567        assert!(!a.leq(&b));
568        assert!(!b.leq(&a));
569    }
570
571    #[test]
572    fn leq_joined_dominates_parts() {
573        let seed = Stamp::seed();
574        let (mut a, mut b) = seed.fork();
575        a.event();
576        b.event();
577        let joined = Stamp::join(&a, &b);
578        assert!(a.leq(&joined));
579        assert!(b.leq(&joined));
580    }
581
582    #[test]
583    fn leq_zero_events() {
584        let a = Stamp::seed();
585        let b = Stamp::seed();
586        assert!(a.leq(&b));
587        assert!(b.leq(&a));
588    }
589
590    #[test]
591    fn leq_transitive() {
592        let mut s = Stamp::seed();
593        let s0 = s.clone();
594        s.event();
595        let s1 = s.clone();
596        s.event();
597        let s2 = s.clone();
598
599        assert!(s0.leq(&s1));
600        assert!(s1.leq(&s2));
601        assert!(s0.leq(&s2)); // transitivity
602    }
603
604    // === concurrent =========================================================
605
606    #[test]
607    fn concurrent_after_fork_and_events() {
608        let seed = Stamp::seed();
609        let (mut a, mut b) = seed.fork();
610        a.event();
611        b.event();
612        assert!(a.concurrent(&b));
613        assert!(b.concurrent(&a));
614    }
615
616    #[test]
617    fn not_concurrent_when_dominated() {
618        let mut s = Stamp::seed();
619        let before = s.clone();
620        s.event();
621        assert!(!before.concurrent(&s));
622        assert!(!s.concurrent(&before));
623    }
624
625    #[test]
626    fn not_concurrent_when_equal() {
627        let s = Stamp::seed();
628        assert!(!s.concurrent(&s));
629    }
630
631    #[test]
632    fn concurrent_is_symmetric() {
633        let seed = Stamp::seed();
634        let (mut a, mut b) = seed.fork();
635        a.event();
636        b.event();
637        assert_eq!(a.concurrent(&b), b.concurrent(&a));
638    }
639
640    // === Multi-agent scenarios ==============================================
641
642    #[test]
643    fn two_agent_fork_work_retire() {
644        let seed = Stamp::seed();
645        let (mut a, mut b) = seed.fork();
646
647        // Agent A does 3 events
648        a.event();
649        a.event();
650        a.event();
651
652        // Agent B does 2 events
653        b.event();
654        b.event();
655
656        // They're concurrent
657        assert!(a.concurrent(&b));
658
659        // Retire: join them back
660        let retired = Stamp::join(&a, &b);
661        assert!(a.leq(&retired));
662        assert!(b.leq(&retired));
663        assert_eq!(retired.id, Id::one());
664    }
665
666    #[test]
667    fn four_agent_scenario() {
668        let seed = Stamp::seed();
669        let (ab, cd) = seed.fork();
670        let (mut a, mut b) = ab.fork();
671        let (mut c, mut d) = cd.fork();
672
673        // Each agent does some work
674        a.event();
675        b.event();
676        b.event();
677        c.event();
678        c.event();
679        c.event();
680        d.event();
681
682        // All pairs are concurrent
683        assert!(a.concurrent(&b));
684        assert!(a.concurrent(&c));
685        assert!(a.concurrent(&d));
686        assert!(b.concurrent(&c));
687        assert!(b.concurrent(&d));
688        assert!(c.concurrent(&d));
689
690        // Merge a+b, c+d, then everything
691        let ab_merged = Stamp::join(&a, &b);
692        let cd_merged = Stamp::join(&c, &d);
693        assert!(a.leq(&ab_merged));
694        assert!(b.leq(&ab_merged));
695        assert!(c.leq(&cd_merged));
696        assert!(d.leq(&cd_merged));
697
698        let all = Stamp::join(&ab_merged, &cd_merged);
699        assert!(a.leq(&all));
700        assert!(b.leq(&all));
701        assert!(c.leq(&all));
702        assert!(d.leq(&all));
703        assert_eq!(all.id, Id::one());
704    }
705
706    #[test]
707    fn eight_agent_fork_work_retire_cycle() {
708        let seed = Stamp::seed();
709
710        // Fork into 8 agents
711        let (half_l, half_r) = seed.fork();
712        let (q1, q2) = half_l.fork();
713        let (q3, q4) = half_r.fork();
714        let (mut a1, mut a2) = q1.fork();
715        let (mut a3, mut a4) = q2.fork();
716        let (mut a5, mut a6) = q3.fork();
717        let (mut a7, mut a8) = q4.fork();
718
719        let mut agents = [
720            &mut a1, &mut a2, &mut a3, &mut a4, &mut a5, &mut a6, &mut a7, &mut a8,
721        ];
722
723        // Each agent does (i+1) events
724        for (i, agent) in agents.iter_mut().enumerate() {
725            for _ in 0..=(i as u32) {
726                agent.event();
727            }
728        }
729
730        // All agents should be pairwise concurrent
731        let snapshots: Vec<Stamp> = [&a1, &a2, &a3, &a4, &a5, &a6, &a7, &a8]
732            .iter()
733            .map(|s| (*s).clone())
734            .collect();
735
736        for i in 0..8 {
737            for j in (i + 1)..8 {
738                assert!(
739                    snapshots[i].concurrent(&snapshots[j]),
740                    "agents {i} and {j} should be concurrent"
741                );
742            }
743        }
744
745        // Retire all agents back into one stamp
746        let mut merged = snapshots[0].clone();
747        for s in &snapshots[1..] {
748            merged = Stamp::join(&merged, s);
749        }
750
751        // Merged dominates all
752        for (i, s) in snapshots.iter().enumerate() {
753            assert!(s.leq(&merged), "agent {i} should be <= merged");
754        }
755
756        // Merged stamp should own the full interval
757        assert_eq!(merged.id, Id::one());
758    }
759
760    #[test]
761    fn sixteen_agent_cycle() {
762        let seed = Stamp::seed();
763
764        // Fork tree to get 16 agents
765        fn fork_n(stamp: Stamp, depth: u32) -> Vec<Stamp> {
766            if depth == 0 {
767                return vec![stamp];
768            }
769            let (l, r) = stamp.fork();
770            let mut result = fork_n(l, depth - 1);
771            result.extend(fork_n(r, depth - 1));
772            result
773        }
774
775        let mut agents = fork_n(seed, 4);
776        assert_eq!(agents.len(), 16);
777
778        // Each agent does some work
779        for (i, agent) in agents.iter_mut().enumerate() {
780            for _ in 0..((i % 5) + 1) {
781                agent.event();
782            }
783        }
784
785        // Verify pairwise concurrency
786        for i in 0..16 {
787            for j in (i + 1)..16 {
788                assert!(
789                    agents[i].concurrent(&agents[j]),
790                    "agents {i} and {j} should be concurrent"
791                );
792            }
793        }
794
795        // Merge all back
796        let mut merged = agents[0].clone();
797        for a in &agents[1..] {
798            merged = Stamp::join(&merged, a);
799        }
800
801        for (i, a) in agents.iter().enumerate() {
802            assert!(a.leq(&merged), "agent {i} should be <= merged");
803        }
804        assert_eq!(merged.id, Id::one());
805    }
806
807    // === Property tests =====================================================
808
809    proptest! {
810        #[test]
811        fn prop_fork_join_roundtrip(events_before in 0u32..10) {
812            let mut s = Stamp::seed();
813            for _ in 0..events_before {
814                s.event();
815            }
816            let original_event = s.event.clone();
817
818            let (a, b) = s.fork();
819            let joined = Stamp::join(&a, &b);
820
821            // ID should be fully recovered
822            prop_assert_eq!(&joined.id, &Id::one());
823            // Event should be at least as advanced as the original
824            prop_assert!(leq_event(&original_event, &joined.event));
825        }
826
827        #[test]
828        fn prop_event_monotonic(n_events in 1u32..20) {
829            let mut s = Stamp::seed();
830            let mut prev_max = 0u32;
831            for _ in 0..n_events {
832                s.event();
833                let new_max = s.event.max_value();
834                prop_assert!(new_max > prev_max, "monotonicity violated: {} -> {}", prev_max, new_max);
835                prev_max = new_max;
836            }
837        }
838
839        #[test]
840        fn prop_leq_reflexive(n_events in 0u32..10) {
841            let mut s = Stamp::seed();
842            for _ in 0..n_events {
843                s.event();
844            }
845            prop_assert!(s.leq(&s));
846        }
847
848        #[test]
849        fn prop_leq_antisymmetric(n_a in 0u32..5, n_b in 0u32..5) {
850            let seed = Stamp::seed();
851            let (mut a, mut b) = seed.fork();
852            for _ in 0..n_a {
853                a.event();
854            }
855            for _ in 0..n_b {
856                b.event();
857            }
858            if a.leq(&b) && b.leq(&a) {
859                prop_assert_eq!(a.event, b.event);
860            }
861        }
862
863        #[test]
864        fn prop_fork_preserves_coverage(n_events in 0u32..5) {
865            let mut s = Stamp::seed();
866            for _ in 0..n_events {
867                s.event();
868            }
869            let (a, b) = s.fork();
870            let reunited = sum_id(&a.id, &b.id);
871            prop_assert_eq!(reunited, Id::one());
872        }
873
874        #[test]
875        fn prop_join_dominates_both(n_a in 1u32..5, n_b in 1u32..5) {
876            let seed = Stamp::seed();
877            let (mut a, mut b) = seed.fork();
878            for _ in 0..n_a {
879                a.event();
880            }
881            for _ in 0..n_b {
882                b.event();
883            }
884            let joined = Stamp::join(&a, &b);
885            prop_assert!(a.leq(&joined), "a should be <= join(a,b)");
886            prop_assert!(b.leq(&joined), "b should be <= join(a,b)");
887        }
888
889        #[test]
890        fn prop_concurrent_symmetric(n_a in 1u32..5, n_b in 1u32..5) {
891            let seed = Stamp::seed();
892            let (mut a, mut b) = seed.fork();
893            for _ in 0..n_a {
894                a.event();
895            }
896            for _ in 0..n_b {
897                b.event();
898            }
899            prop_assert_eq!(a.concurrent(&b), b.concurrent(&a));
900        }
901
902        #[test]
903        fn prop_leq_transitive(n1 in 0u32..4, n2 in 1u32..4, n3 in 1u32..4) {
904            let mut s = Stamp::seed();
905            for _ in 0..n1 {
906                s.event();
907            }
908            let s0 = s.clone();
909            for _ in 0..n2 {
910                s.event();
911            }
912            let s1 = s.clone();
913            for _ in 0..n3 {
914                s.event();
915            }
916            let s2 = s;
917
918            prop_assert!(s0.leq(&s1));
919            prop_assert!(s1.leq(&s2));
920            prop_assert!(s0.leq(&s2));
921        }
922    }
923}