Skip to main content

max / synckit

Model the pull pipeline as four properties Phase 3 of wiki testing-posture, aimed at resolve_pull with a real Connection. The earlier attempt aimed one layer down at CleanChanges::gated_at and failed three of four properties against correct code, because that layer only ever promised committed-clock filtering. The one-entry-per-row invariant does not exist until after the collapse, so resolve_pull is the lowest layer where max-HLC-wins is an honest thing to assert. The properties: the final value of a row is the winner under the ordering rule; batch order does not change final state; replaying a batch is a no-op; committed clocks never go backwards. Two things the probes changed. The oracle first called change_order, which made it agree with a broken change_order: deleting the payload tiebreak left all four properties green. It now states the rule independently, so it fails when the rule changes. And the generator drew walls from a 100ms window, which produced roughly one exact HLC tie per run, too few to observe the tiebreak the ties exist to exercise. The clock now has almost no entropy and the payload carries the variation. committed_clocks_only_advance observes two mechanisms rather than one: the committed-HLC gate and set_committed's advance-only clause each hold it up alone, so it fails only when both go. Recorded in its doc comment, because a green run there says less than it appears to.
Co-Authored-By
Claude Opus 5 (1M context) <noreply@anthropic.com>
Author: Max Johnson <me@maxj.phd> · 2026-08-05 16:11 UTC
Signed with PGP, not checked
Commit: eafe59b857a44f3aebb6d14405dc88fa7f3c0d51
Parent: 5b1a9b3
2 files changed, +224 insertions, -0 deletions
M synckit-client/src/store/hlc.rs +213
@@ -792,6 +792,219 @@
792 792 );
793 793 }
794 794
795 + /// A model of the pull pipeline.
796 + ///
797 + /// Aimed at [`resolve_pull`] with a real `Connection`, deliberately, and not
798 + /// at the pure conflict layer one step down. The one-entry-per-row invariant
799 + /// only exists after the collapse, so `resolve_pull` is the lowest layer
800 + /// where a max-HLC-wins specification is an honest thing to assert; an
801 + /// earlier attempt at this aimed at `CleanChanges::gated_at`, which only ever
802 + /// promised committed-clock filtering, and failed three of four properties
803 + /// against correct code. See wiki `testing-posture`, Phase 3.
804 + ///
805 + /// The four properties are the ones a sync engine lives or dies on, and each
806 + /// is a different way for two devices to end up holding different bytes.
807 + mod model {
808 + use super::*;
809 + use proptest::prelude::*;
810 +
811 + /// A fixed instant, so the poisoning guard is deterministic. Generated
812 + /// walls sit near it and well inside `MAX_HLC_DRIFT_MS`; poisoning is
813 + /// covered by its own example test, and letting it fire here would mean
814 + /// the properties were quietly asserting over an empty batch.
815 + const BASE_MS: i64 = 1_700_000_000_000;
816 +
817 + fn now() -> DateTime<Utc> {
818 + DateTime::from_timestamp_millis(BASE_MS).unwrap()
819 + }
820 +
821 + /// Three rows, three devices, three wall readings, and every range here
822 + /// is narrow on purpose.
823 + ///
824 + /// The interesting case is two changes for one row at an *exact* HLC
825 + /// tie with differing payloads, because that is the only case the
826 + /// payload tiebreak in `change_order` serves. A wider generator makes it
827 + /// unreachable: a first attempt drew walls from a 100ms window and
828 + /// produced roughly one tie across a whole 256-case run, few enough that
829 + /// deleting the tiebreak outright left every property passing. Ties have
830 + /// to be common for these properties to observe anything, so the clock
831 + /// is generated with almost no entropy in it and the payload carries the
832 + /// variation instead.
833 + fn batch() -> impl Strategy<Value = Vec<PulledChange>> {
834 + let one = (0u8..3, 0u8..3, 0i64..3, 0u32..2, 0u8..4).prop_map(
835 + |(row, dev, wall_off, counter, payload)| {
836 + let node = node(u128::from(dev));
837 + PulledChange {
838 + entry: ChangeEntry {
839 + table: "note".into(),
840 + op: ChangeOp::Update,
841 + row_id: format!("r{row}"),
842 + timestamp: now(),
843 + hlc: Hlc {
844 + wall_ms: BASE_MS + wall_off,
845 + counter,
846 + node,
847 + },
848 + data: Some(serde_json::json!({
849 + "id": format!("r{row}"),
850 + "name": format!("v{payload}"),
851 + })),
852 + extra: serde_json::Map::default(),
853 + },
854 + device_id: node,
855 + seq: 0,
856 + }
857 + },
858 + );
859 + proptest::collection::vec(one, 0..6)
860 + }
861 +
862 + /// The whole observable state of a device: what each row holds, and what
863 + /// the committed ledger says about it. Both matter. A pipeline that
864 + /// wrote the right value but recorded the wrong committed clock would
865 + /// gate its own next pull incorrectly, and comparing only the rows would
866 + /// not see it.
867 + fn state(conn: &Connection) -> Vec<(String, Option<String>, Option<Hlc>)> {
868 + ["r0", "r1", "r2"]
869 + .iter()
870 + .map(|r| {
871 + (
872 + (*r).to_string(),
873 + note_name(conn, r),
874 + committed_hlc(conn, "note", r).unwrap(),
875 + )
876 + })
877 + .collect()
878 + }
879 +
880 + /// Run a batch through the real pipeline on a fresh device.
881 + fn pull(conn: &mut Connection, node: DeviceId, pulled: Vec<PulledChange>) {
882 + let s = schema();
883 + let resolved = resolve_pull(conn, &s, node, pulled, now(), "").unwrap();
884 + apply_remote_changes(conn, &s, &resolved, "").unwrap();
885 + record_committed(conn, resolved.as_slice()).unwrap();
886 + }
887 +
888 + /// The specification the pipeline is supposed to implement: per row, the
889 + /// highest wall clock wins, then the highest counter, then the highest
890 + /// device, then the highest payload bytes.
891 + ///
892 + /// Spelled out rather than delegated to `change_order`, and that is the
893 + /// whole point of it. An oracle that called `change_order` would agree
894 + /// with a broken `change_order`, which is the imitation-oracle failure
895 + /// from wiki `testing-posture` wearing a different hat: it was the first
896 + /// version of this function, and deleting the payload tiebreak left all
897 + /// four properties passing. This version fails when the rule changes,
898 + /// because it is a second statement of the rule rather than a reference
899 + /// to the first.
900 + fn expected_winner(pulled: &[PulledChange], row: &str) -> Option<String> {
901 + fn rank(e: &ChangeEntry) -> (i64, u32, Uuid, Vec<u8>) {
902 + (
903 + e.hlc.wall_ms,
904 + e.hlc.counter,
905 + e.hlc.node.as_uuid(),
906 + serde_json::to_vec(e.data.as_ref().unwrap()).unwrap(),
907 + )
908 + }
909 + pulled
910 + .iter()
911 + .map(|p| &p.entry)
912 + .filter(|e| e.row_id == row)
913 + .max_by_key(|e| rank(e))
914 + .map(|e| e.data.as_ref().unwrap()["name"].as_str().unwrap().into())
915 + }
916 +
917 + proptest! {
918 + /// **The pipeline implements max-HLC-wins.** The value each row ends
919 + /// up holding is the one from the change that wins under
920 + /// `change_order`, whatever else the batch contained.
921 + #[test]
922 + fn final_value_is_the_winner_under_change_order(pulled in batch()) {
923 + let (mut conn, n) = device(1);
924 + pull(&mut conn, n, pulled.clone());
925 + for row in ["r0", "r1", "r2"] {
926 + prop_assert_eq!(
927 + note_name(&conn, row),
928 + expected_winner(&pulled, row),
929 + "row {} does not hold the winner",
930 + row
931 + );
932 + }
933 + }
934 +
935 + /// **Batch order does not change the final state.** The server may
936 + /// deliver a batch in any order; two devices that see the same
937 + /// changes in different orders must agree afterwards. This is the
938 + /// property the whole change-ordering unification was for.
939 + #[test]
940 + fn order_within_a_batch_does_not_matter(pulled in batch()) {
941 + let (mut forwards, fnode) = device(1);
942 + pull(&mut forwards, fnode, pulled.clone());
943 +
944 + let mut reversed_batch = pulled;
945 + reversed_batch.reverse();
946 + let (mut backwards, bnode) = device(1);
947 + pull(&mut backwards, bnode, reversed_batch);
948 +
949 + prop_assert_eq!(
950 + state(&forwards),
951 + state(&backwards),
952 + "two devices diverged on batch order alone"
953 + );
954 + }
955 +
956 + /// **Replaying a batch is a no-op.** A pull that is retried, or a
957 + /// cursor that rewinds, must not change anything the first pass
958 + /// already settled. This is what the committed ledger exists for.
959 + #[test]
960 + fn replaying_a_batch_changes_nothing(pulled in batch()) {
961 + let (mut conn, n) = device(1);
962 + pull(&mut conn, n, pulled.clone());
963 + let after_first = state(&conn);
964 + pull(&mut conn, n, pulled);
965 + prop_assert_eq!(after_first, state(&conn), "a replayed batch moved the state");
966 + }
967 +
968 + /// **Committed clocks never go backwards.** The ledger is what gates
969 + /// stale re-pulls, so a regression there un-gates a change the device
970 + /// already superseded, and an old value overwrites a newer one.
971 + ///
972 + /// Two independent mechanisms hold this up, and this property
973 + /// observes the pair rather than either one: the committed-HLC gate
974 + /// drops a stale change before `set_committed` sees it, and
975 + /// `set_committed` refuses to regress even if one reaches it.
976 + /// Breaking either alone leaves this passing, which is what
977 + /// defense in depth means and is worth knowing before trusting a
978 + /// green run here; breaking both fails it. The individual clause in
979 + /// `set_committed` has its own example test,
980 + /// `committed_ledger_advances_only`.
981 + #[test]
982 + fn committed_clocks_only_advance(first in batch(), second in batch()) {
983 + let (mut conn, n) = device(1);
984 + pull(&mut conn, n, first);
985 + let before: Vec<Option<Hlc>> =
986 + state(&conn).into_iter().map(|(_, _, h)| h).collect();
987 + pull(&mut conn, n, second);
988 + let after: Vec<Option<Hlc>> =
989 + state(&conn).into_iter().map(|(_, _, h)| h).collect();
990 +
991 + for (before, after) in before.into_iter().zip(after) {
992 + match (before, after) {
993 + (Some(b), Some(a)) => prop_assert!(
994 + a >= b,
995 + "committed clock went backwards: {:?} -> {:?}",
996 + b, a
997 + ),
998 + (Some(b), None) => {
999 + prop_assert!(false, "committed clock for a row disappeared: {:?}", b);
1000 + }
1001 + _ => {}
1002 + }
1003 + }
1004 + }
1005 + }
1006 + }
1007 +
795 1008 // ── Conflict stash ──
796 1009 //
797 1010 // LWW always discards one side; these pin that the discarded bytes are kept
A synckit-client/proptest-regressions/store/hlc.txt +11
@@ -1,0 +1,11 @@
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 f316a64a84523c15582b79ba1bc8d0261f26301d5f6a29ac9721b8341d5e96ab # shrinks to pulled = [PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000026, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v0")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }, PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v1")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }]
8 + cc c2d4aa664438a38c412b938ff4a432018fc9dc6e6ab660133123ae2d04ad71b4 # shrinks to pulled = [PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v1")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }, PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v0")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }]
9 + cc c46b37be05f09c1a28abe12636d31cf4f5fb3ef15bda680dcf69e0717307a04e # shrinks to pulled = [PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r1", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r1"), "name": String("v0")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }, PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r1", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r1"), "name": String("v1")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }]
10 + cc d8ac248ba280b6786222875b5e990824e97b6de9ff67160ae191084c2c31ee5e # shrinks to pulled = [PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000002) }, data: Some(Object {"id": String("r2"), "name": String("v0")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000002), seq: 0 }, PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000002) }, data: Some(Object {"id": String("r2"), "name": String("v1")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000002), seq: 0 }]
11 + cc a6d53a57388c6cabc912f655a77cf52e2c8c449a9300a651edb0ce5c3b45a646 # shrinks to pulled = [PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000002, counter: 0, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v0")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }, PulledChange { entry: ChangeEntry { table: "note", op: Update, row_id: "r2", timestamp: 2023-11-14T22:13:20Z, hlc: Hlc { wall_ms: 1700000000000, counter: 1, node: DeviceId(00000000-0000-0000-0000-000000000000) }, data: Some(Object {"id": String("r2"), "name": String("v1")}), extra: {} }, device_id: DeviceId(00000000-0000-0000-0000-000000000000), seq: 0 }]