Skip to main content

max / synckit

State the clock, resolver and crypto contracts as properties HLC ordering, conflict resolution and encryption are universally quantified: an order is an order for every pair, a round-trip round-trips for every input. All 133 tests over them were examples, which pin the cases someone thought of. Nine properties, in-crate because `PulledChange` is non-exhaustive and a consumer has no business constructing one. The clock: tick strictly follows its predecessor, observe overtakes both inputs, and a repeated observe never goes backwards, each exempting the representable ceiling where the documented behaviour is to clamp. The resolver: convergence (two devices given the same pair with the roles reversed keep the same payload), determinism, and that an honest clock beats a poisoned one from either side. Crypto: round-trip, wrong-key failure, and that sealing twice does not repeat ciphertext. Convergence needed a second pass to be worth anything. Written against two independently drawn clocks it passed even with `resolve_tie`'s payload tiebreak removed, because independent draws essentially never collide and the exact tie is the whole point of that tiebreak. Generating the pair with ties weighted in fixes it: the same deletion now fails with identical HLCs, A keeping 0 and B keeping 1, which is the divergence the comment on `resolve_tie` describes. That seed is the committed regression. Phase 2 of wiki `testing-posture`.
Co-Authored-By
Claude Opus 5 (1M context) <noreply@anthropic.com>
Author: Max Johnson <me@maxj.phd> · 2026-08-05 15:10 UTC
Signed with PGP, not checked
Commit: 914ca41cfd7dda43e939982b7fb536f8740a9421
Parent: 559c9d0
5 files changed, +363 insertions, -0 deletions
M synckit-client/Cargo.toml +5
@@ -106,6 +106,11 @@
106 106 path = "tests/integration/main.rs"
107 107
108 108 [dev-dependencies]
109 + # The contracts in `types::Hlc`, `conflict`, and `crypto` are universally
110 + # quantified (an order is an order for every pair, a round-trip round-trips for
111 + # every input), while their tests were all examples. `proptest-regressions/` is
112 + # committed so a shrunk counterexample becomes a permanent case.
113 + proptest = "1"
109 114 wiremock = "0.6"
110 115 # reqwest is built `rustls-no-provider`, so real consumers install a rustls crypto
111 116 # provider at startup (audiofiles installs ring). The test suite has no such app, so
M synckit-client/src/conflict.rs +168
@@ -524,6 +524,174 @@
524 524 use crate::types::{ChangeOp, Hlc};
525 525 use serde_json::json;
526 526
527 + /// Properties of the resolver.
528 + ///
529 + /// The contract here is convergence, which is a statement about every pair
530 + /// of changes rather than about the pairs someone wrote down. The 43 tests
531 + /// below are examples; these state the rule. See wiki `testing-posture`,
532 + /// Phase 2.
533 + mod properties {
534 + use super::*;
535 + use proptest::prelude::*;
536 +
537 + /// Small device pool: node is the final tiebreak, so collisions are the
538 + /// interesting case and random UUIDs would never produce them.
539 + fn device_id() -> impl Strategy<Value = DeviceId> {
540 + (0u8..3).prop_map(|n| {
541 + let mut bytes = [0u8; 16];
542 + bytes[15] = n;
543 + DeviceId::new(Uuid::from_bytes(bytes))
544 + })
545 + }
546 +
547 + /// Walls clustered tightly so ties and near-ties are common, plus a
548 + /// far-future band that trips the clock-poisoning guard.
549 + fn any_hlc() -> impl Strategy<Value = Hlc> {
550 + let wall = prop_oneof![
551 + 6 => 1_700_000_000_000i64..1_700_000_000_010,
552 + 2 => 0i64..2_000_000_000_000,
553 + 2 => 4_000_000_000_000i64..8_000_000_000_000,
554 + ];
555 + (wall, 0u32..4, device_id()).prop_map(|(wall_ms, counter, node)| Hlc {
556 + wall_ms,
557 + counter,
558 + node,
559 + })
560 + }
561 +
562 + /// Pairs of clocks, weighted so exact ties are common.
563 + ///
564 + /// Two independent draws almost never collide, and the tie is exactly
565 + /// where convergence is hardest: it is the case the payload tiebreak in
566 + /// `resolve_tie` exists for. Generating the pair rather than two
567 + /// independent clocks is what gives this property teeth, verified by
568 + /// removing that tiebreak and watching the convergence test fail.
569 + fn hlc_pair() -> impl Strategy<Value = (Hlc, Hlc)> {
570 + prop_oneof![
571 + 3 => (any_hlc(), any_hlc()),
572 + 3 => any_hlc().prop_map(|h| (h, h)),
573 + 2 => (any_hlc(), 0u32..4).prop_map(|(h, counter)| (h, Hlc { counter, ..h })),
574 + ]
575 + }
576 +
577 + fn entry_with(hlc: Hlc, payload: u8) -> ChangeEntry {
578 + let mut e = make_entry("tasks", "row-1", ChangeOp::Update, Utc::now());
579 + e.hlc = hlc;
580 + e.data = Some(json!({ "v": payload }));
581 + e
582 + }
583 +
584 + fn pulled_with(hlc: Hlc, payload: u8) -> PulledChange {
585 + let mut p = make_pulled(
586 + "tasks",
587 + "row-1",
588 + ChangeOp::Update,
589 + Utc::now(),
590 + hlc.node.as_uuid(),
591 + 1,
592 + );
593 + p.entry.hlc = hlc;
594 + p.entry.data = Some(json!({ "v": payload }));
595 + p
596 + }
597 +
598 + proptest! {
599 + /// **Convergence.** Two devices hold the same pair with the roles
600 + /// reversed: what is local on A is remote on B. If the answer
601 + /// depended on which side the resolver was handed, the two devices
602 + /// would keep different rows and never reconcile. No example test
603 + /// notices unless it happens to pick that pair.
604 + ///
605 + /// Stated over the surviving payload rather than the `Resolution`
606 + /// variant: at an exact tie both sides keep local, which converges
607 + /// precisely because the two changes are then byte-identical.
608 + #[test]
609 + fn lww_picks_the_same_winner_from_either_side(
610 + (a_hlc, b_hlc) in hlc_pair(),
611 + a_payload in any::<u8>(),
612 + b_payload in any::<u8>(),
613 + ) {
614 + let now = Utc::now();
615 + let on_a = match resolve_lww_at(
616 + &entry_with(a_hlc, a_payload),
617 + &pulled_with(b_hlc, b_payload),
618 + now,
619 + ) {
620 + Resolution::KeepLocal => a_payload,
621 + Resolution::KeepRemote => b_payload,
622 + other => return Err(TestCaseError::fail(format!("unexpected {other:?}"))),
623 + };
624 + let on_b = match resolve_lww_at(
625 + &entry_with(b_hlc, b_payload),
626 + &pulled_with(a_hlc, a_payload),
627 + now,
628 + ) {
629 + Resolution::KeepLocal => b_payload,
630 + Resolution::KeepRemote => a_payload,
631 + other => return Err(TestCaseError::fail(format!("unexpected {other:?}"))),
632 + };
633 +
634 + prop_assert_eq!(
635 + on_a, on_b,
636 + "the two devices kept different payloads and will never converge: \
637 + A kept {}, B kept {} (a={:?}, b={:?})",
638 + on_a, on_b, a_hlc, b_hlc
639 + );
640 + }
641 +
642 + /// Resolution is a function of its inputs. Cheap to state, and it is
643 + /// what lets the resolver be re-run from a retry without
644 + /// re-deriving the world.
645 + #[test]
646 + fn lww_is_deterministic(
647 + (a_hlc, b_hlc) in hlc_pair(),
648 + a_payload in any::<u8>(),
649 + b_payload in any::<u8>(),
650 + ) {
651 + let now = Utc::now();
652 + let local = entry_with(a_hlc, a_payload);
653 + let first = resolve_lww_at(&local, &pulled_with(b_hlc, b_payload), now);
654 + let second = resolve_lww_at(&local, &pulled_with(b_hlc, b_payload), now);
655 + prop_assert_eq!(format!("{first:?}"), format!("{second:?}"));
656 + }
657 +
658 + /// A poisoned clock must never beat an honest one. This is the
659 + /// guard's whole purpose: an unbounded future timestamp would
660 + /// otherwise win every conflict for years.
661 + #[test]
662 + fn an_honest_clock_beats_a_poisoned_one(
663 + honest_wall in 1_700_000_000_000i64..1_700_000_100_000,
664 + poison_offset in (MAX_HLC_DRIFT_MS + 1)..10_000_000_000i64,
665 + node_a in device_id(),
666 + node_b in device_id(),
667 + ) {
668 + let now = Utc::now();
669 + let honest = Hlc { wall_ms: honest_wall, counter: 0, node: node_a };
670 + let poisoned = Hlc {
671 + wall_ms: now.timestamp_millis().saturating_add(poison_offset),
672 + counter: 0,
673 + node: node_b,
674 + };
675 + prop_assume!(!is_clock_poisoned(&honest, now));
676 +
677 + prop_assert!(
678 + matches!(
679 + resolve_lww_at(&entry_with(honest, 1), &pulled_with(poisoned, 2), now),
680 + Resolution::KeepLocal
681 + ),
682 + "a poisoned remote won against an honest local"
683 + );
684 + prop_assert!(
685 + matches!(
686 + resolve_lww_at(&entry_with(poisoned, 2), &pulled_with(honest, 1), now),
687 + Resolution::KeepRemote
688 + ),
689 + "a poisoned local won against an honest remote"
690 + );
691 + }
692 + }
693 + }
694 +
527 695 /// Fixed node for locally-minted test entries, distinct from any random
528 696 /// `other_device`, so HLC tiebreaks are deterministic.
529 697 fn local_node() -> DeviceId {
M synckit-client/src/crypto.rs +54
@@ -878,6 +878,60 @@
878 878 mod tests {
879 879 use super::*;
880 880
881 + /// Properties of the sealing layer.
882 + ///
883 + /// Encryption is a round-trip for every input, not for the handful of
884 + /// payload shapes the examples below happen to use. See wiki
885 + /// `testing-posture`, Phase 2.
886 + mod properties {
887 + use super::*;
888 + use proptest::prelude::*;
889 +
890 + proptest! {
891 + /// `decrypt(encrypt(m, k), k) == m`, including for the empty
892 + /// message and for inputs that straddle the chunking boundary.
893 + #[test]
894 + fn encryption_round_trips(
895 + plaintext in prop::collection::vec(any::<u8>(), 0..4096),
896 + ) {
897 + let key = generate_master_key();
898 + let sealed = encrypt_bytes(&plaintext, &key).expect("encrypt");
899 + let opened = decrypt_bytes(&sealed, &key).expect("decrypt");
900 + prop_assert_eq!(opened, plaintext);
901 + }
902 +
903 + /// A wrong key must be an error rather than garbage plaintext,
904 + /// which is what makes the AEAD tag load-bearing instead of
905 + /// decorative.
906 + #[test]
907 + fn decryption_under_the_wrong_key_fails(
908 + plaintext in prop::collection::vec(any::<u8>(), 0..1024),
909 + ) {
910 + let key = generate_master_key();
911 + let other = generate_master_key();
912 + prop_assume!(key != other);
913 + let sealed = encrypt_bytes(&plaintext, &key).expect("encrypt");
914 + prop_assert!(
915 + decrypt_bytes(&sealed, &other).is_err(),
916 + "a wrong key produced a result instead of an error"
917 + );
918 + }
919 +
920 + /// Sealing the same bytes twice under one key must not repeat the
921 + /// ciphertext. A reused nonce is the classic AEAD break, and
922 + /// nothing asserted the nonce actually varies.
923 + #[test]
924 + fn sealing_twice_does_not_repeat_ciphertext(
925 + plaintext in prop::collection::vec(any::<u8>(), 1..512),
926 + ) {
927 + let key = generate_master_key();
928 + let a = encrypt_bytes(&plaintext, &key).expect("encrypt");
929 + let b = encrypt_bytes(&plaintext, &key).expect("encrypt");
930 + prop_assert_ne!(a, b, "the same plaintext sealed to identical bytes twice");
931 + }
932 + }
933 + }
934 +
881 935 #[test]
882 936 fn master_key_generation_is_random() {
883 937 let k1 = generate_master_key();
M synckit-client/src/types.rs +129
@@ -725,6 +725,135 @@
725 725 use super::*;
726 726 use serde_json::json;
727 727
728 + /// Properties of the clock.
729 + ///
730 + /// The HLC contracts are universally quantified, an order is an order for
731 + /// every pair, while the tests below are examples. Examples pin the cases
732 + /// someone thought of; these state the rule. Shrinking is the part that
733 + /// pays: a counterexample you can read beats a hundred passing examples.
734 + /// See wiki `testing-posture`, Phase 2.
735 + mod properties {
736 + use super::*;
737 + use proptest::prelude::*;
738 +
739 + /// A small device pool on purpose. With random UUIDs a node collision
740 + /// is vanishingly rare, and the node tiebreak is what needs exercising.
741 + fn device_id() -> impl Strategy<Value = DeviceId> {
742 + (0u8..4).prop_map(|n| {
743 + let mut bytes = [0u8; 16];
744 + bytes[15] = n;
745 + DeviceId::new(Uuid::from_bytes(bytes))
746 + })
747 + }
748 +
749 + /// Ordinary clocks plus the i64 ceiling, where `bump_counter`'s overflow
750 + /// ladder lives.
751 + fn wall_ms() -> impl Strategy<Value = i64> {
752 + prop_oneof![
753 + 5 => 0i64..2_000_000_000_000,
754 + 1 => (i64::MAX - 4)..=i64::MAX,
755 + ]
756 + }
757 +
758 + fn counter() -> impl Strategy<Value = u32> {
759 + prop_oneof![
760 + 5 => 0u32..1000,
761 + 1 => (u32::MAX - 2)..=u32::MAX,
762 + ]
763 + }
764 +
765 + fn any_hlc() -> impl Strategy<Value = Hlc> {
766 + (wall_ms(), counter(), device_id()).prop_map(|(wall_ms, counter, node)| Hlc {
767 + wall_ms,
768 + counter,
769 + node,
770 + })
771 + }
772 +
773 + /// The parts that encode causality. The derived `Ord` also breaks ties
774 + /// on `node`, which is a convergence device rather than a clock reading,
775 + /// so a monotonicity claim is about this pair.
776 + fn reading(h: &Hlc) -> (i64, u32) {
777 + (h.wall_ms, h.counter)
778 + }
779 +
780 + /// At `{i64::MAX, u32::MAX}` no greater HLC is representable and the
781 + /// documented behaviour is to clamp rather than wrap backwards. A
782 + /// monotonicity property has to exempt that point or it asserts
783 + /// something the type cannot provide.
784 + fn at_ceiling(h: &Hlc) -> bool {
785 + h.wall_ms == i64::MAX && h.counter == u32::MAX
786 + }
787 +
788 + proptest! {
789 + /// A local event always produces a clock strictly later than the one
790 + /// it advanced from. Two local writes comparing equal would leave
791 + /// LWW unable to order a device against itself.
792 + #[test]
793 + fn tick_is_strictly_increasing(
794 + prev in any_hlc(),
795 + now_ms in wall_ms(),
796 + node in device_id(),
797 + ) {
798 + let next = Hlc::tick(prev, now_ms, node);
799 + if at_ceiling(&prev) {
800 + prop_assert_eq!(reading(&next), reading(&prev), "the ceiling clamps");
801 + } else {
802 + prop_assert!(
803 + reading(&next) > reading(&prev),
804 + "tick({:?}, {}) gave {:?}, which does not follow it",
805 + prev, now_ms, next
806 + );
807 + }
808 + }
809 +
810 + /// Receiving leaves the clock ahead of everything seen: later than
811 + /// the previous local reading and past the remote one. A subsequent
812 + /// local write then causally follows the remote change, which is the
813 + /// entire point of the receive rule.
814 + #[test]
815 + fn observe_overtakes_both_inputs(
816 + prev in any_hlc(),
817 + remote in any_hlc(),
818 + now_ms in wall_ms(),
819 + node in device_id(),
820 + ) {
821 + prop_assume!(!at_ceiling(&prev) && !at_ceiling(&remote));
822 + let next = Hlc::observe(prev, remote, now_ms, node);
823 + prop_assert!(
824 + reading(&next) > reading(&prev),
825 + "observe left the clock at or behind its previous reading: {:?} -> {:?}",
826 + prev, next
827 + );
828 + prop_assert!(
829 + reading(&next) > reading(&remote),
830 + "observe did not overtake the remote clock: remote {:?}, got {:?}",
831 + remote, next
832 + );
833 + }
834 +
835 + /// Observing the same remote twice must not move the clock
836 + /// backwards. Retries and duplicate deliveries make this a real
837 + /// sequence rather than a hypothetical one.
838 + #[test]
839 + fn observe_is_monotone_under_repetition(
840 + prev in any_hlc(),
841 + remote in any_hlc(),
842 + now_ms in wall_ms(),
843 + node in device_id(),
844 + ) {
845 + prop_assume!(!at_ceiling(&prev) && !at_ceiling(&remote));
846 + let once = Hlc::observe(prev, remote, now_ms, node);
847 + let twice = Hlc::observe(once, remote, now_ms, node);
848 + prop_assert!(
849 + reading(&twice) >= reading(&once),
850 + "a repeated observe went backwards: {:?} -> {:?}",
851 + once, twice
852 + );
853 + }
854 + }
855 + }
856 +
728 857 #[test]
729 858 fn change_op_serde_roundtrip() {
730 859 for (variant, expected_str) in [
A synckit-client/proptest-regressions/conflict.txt +7
@@ -1,0 +1,7 @@
1 + # Seeds for failure cases proptest has generated in the past. It is
2 + # automatically read and these particular cases re-run before any
3 + # novel cases are generated.
4 + #
5 + # It is recommended to check this file in to source control so that
6 + # everyone who runs the test benefits from these saved cases.
7 + cc 9d9f0ab1b1f55d7fe578e6c112c886bca450128961e27b0531affe544f42a200 # shrinks to (a_hlc, b_hlc) = (Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }), a_payload = 0, b_payload = 1