diff --git a/Directory.Packages.props b/Directory.Packages.props
index 549b010..fba8223 100644
--- a/Directory.Packages.props
+++ b/Directory.Packages.props
@@ -17,6 +17,7 @@
+
diff --git a/src/SIL.Harmony.Tests/PropertyBased/ChangeSpecs.cs b/src/SIL.Harmony.Tests/PropertyBased/ChangeSpecs.cs
new file mode 100644
index 0000000..144bd31
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/ChangeSpecs.cs
@@ -0,0 +1,90 @@
+using System.Globalization;
+using SIL.Harmony.Changes;
+using SIL.Harmony.Sample.Changes;
+using SIL.Harmony.Sample.Models;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// An immutable, deterministic description of a single change, mintable into a real
+/// . Kept as data (not a live ) so a schedule can be
+/// replayed and fed to many engines reproducibly. mints the runtime change;
+/// renders the C# that reconstructs this spec, so a failing property can emit
+/// a ready-to-run reproduction (see ).
+///
+public abstract record ChangeSpec(Guid EntityId)
+{
+ public abstract IChange ToChange();
+
+ /// Renders a C# expression that reconstructs this spec, e.g. new SetWordTextSpec(Guid.Parse("..."), "t3").
+ public abstract string ToCode();
+}
+
+public sealed record SetWordTextSpec(Guid EntityId, string Text) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new SetWordTextChange(EntityId, Text);
+ public override string ToCode() => $"new {nameof(SetWordTextSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Str(Text)})";
+}
+
+public sealed record NewWordSpec(Guid EntityId, string Text) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new NewWordChange(EntityId, Text);
+ public override string ToCode() => $"new {nameof(NewWordSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Str(Text)})";
+}
+
+public sealed record SetWordNoteSpec(Guid EntityId, string Note) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new SetWordNoteChange(EntityId, Note);
+ public override string ToCode() => $"new {nameof(SetWordNoteSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Str(Note)})";
+}
+
+public sealed record DeleteWordSpec(Guid EntityId) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new DeleteChange(EntityId);
+ public override string ToCode() => $"new {nameof(DeleteWordSpec)}({ReproCode.Guid(EntityId)})";
+}
+
+public sealed record SetAntonymSpec(Guid EntityId, Guid AntonymId) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new SetAntonymReferenceChange(EntityId, AntonymId);
+ public override string ToCode() => $"new {nameof(SetAntonymSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Guid(AntonymId)})";
+}
+
+public sealed record NewDefinitionSpec(Guid EntityId, Guid WordId, string Text, string PartOfSpeech, double Order)
+ : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new NewDefinitionChange(EntityId)
+ {
+ WordId = WordId,
+ Text = Text,
+ PartOfSpeech = PartOfSpeech,
+ Order = Order,
+ };
+
+ public override string ToCode() =>
+ $"new {nameof(NewDefinitionSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Guid(WordId)}, {ReproCode.Str(Text)}, {ReproCode.Str(PartOfSpeech)}, {ReproCode.Dbl(Order)})";
+}
+
+public sealed record SetDefinitionPartOfSpeechSpec(Guid EntityId, string PartOfSpeech) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new SetDefinitionPartOfSpeechChange(EntityId, PartOfSpeech);
+ public override string ToCode() => $"new {nameof(SetDefinitionPartOfSpeechSpec)}({ReproCode.Guid(EntityId)}, {ReproCode.Str(PartOfSpeech)})";
+}
+
+public sealed record DeleteDefinitionSpec(Guid EntityId) : ChangeSpec(EntityId)
+{
+ public override IChange ToChange() => new DeleteChange(EntityId);
+ public override string ToCode() => $"new {nameof(DeleteDefinitionSpec)}({ReproCode.Guid(EntityId)})";
+}
+
+/// Type-specific projected-content signatures, used to compare entities across engines.
+public static class EntitySignature
+{
+ public static string Of(object dbObject) => dbObject switch
+ {
+ Word w => $"W:{w.Text}|{w.Note}|{w.AntonymId}|{w.ImageResourceId}",
+ Definition d =>
+ $"D:{d.Text}|{d.PartOfSpeech}|{d.Order.ToString(CultureInfo.InvariantCulture)}|{d.OneWordDefinition}|{d.WordId}",
+ _ => dbObject.ToString() ?? "",
+ };
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/GeneratorMetaTests.cs b/src/SIL.Harmony.Tests/PropertyBased/GeneratorMetaTests.cs
new file mode 100644
index 0000000..52373a5
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/GeneratorMetaTests.cs
@@ -0,0 +1,51 @@
+using CsCheck;
+using FluentAssertions.Execution;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// Meta-tests over the generators themselves (no engine involved). They prove the generated
+/// schedules actually contain author-time ties, stragglers, cascades, duplicates, and
+/// genesis-depth rollbacks. If any of these stopped appearing, the property suite would still
+/// go green while testing nothing — these tests fail loudly instead.
+///
+public class GeneratorMetaTests
+{
+ // Fixed, generous sample budget so every (even rare) axis appears with overwhelming
+ // probability. Independent of CsCheck_Iter so CI tuning of the real properties doesn't
+ // make this meta-check flaky.
+ private const int Iterations = 5000;
+
+ [Fact]
+ public void Tier1_Generator_Produces_AllRollbackPhenomena() => AssertProducesAllPhenomena(Generators.Tier1);
+
+ [Fact]
+ public void Tier2_Generator_Produces_AllRollbackPhenomena() => AssertProducesAllPhenomena(Generators.Tier2);
+
+ private static void AssertProducesAllPhenomena(Gen schedules)
+ {
+ var sawTie = false;
+ var sawStraggler = false;
+ var sawCascade = false;
+ var sawDuplicate = false;
+ var sawGenesisRebuild = false;
+
+ schedules.Sample(schedule =>
+ {
+ sawTie |= ScheduleAnalysis.HasAuthorTimeTie(schedule);
+ sawStraggler |= ScheduleAnalysis.StragglerCount(schedule.ArrivalsA) > 0;
+ sawCascade |= ScheduleAnalysis.MaxCascade(schedule.ArrivalsA) >= 2;
+ sawDuplicate |= ScheduleAnalysis.HasDuplicates(schedule.ArrivalsA)
+ || ScheduleAnalysis.HasDuplicates(schedule.ArrivalsB);
+ sawGenesisRebuild |= ScheduleAnalysis.ForcesGenesisRebuild(schedule, schedule.ArrivalsA);
+ return true;
+ }, iter: Iterations);
+
+ using var _ = new AssertionScope();
+ sawTie.Should().BeTrue("the small author-time range must produce commits with equal author times (tiebreak path)");
+ sawStraggler.Should().BeTrue("arrival order independent of author time must produce stragglers (rollback path)");
+ sawCascade.Should().BeTrue("batches must sometimes contain multiple stragglers (cascading rollback)");
+ sawDuplicate.Should().BeTrue("the generator must re-send some commits (idempotency/dedup path)");
+ sawGenesisRebuild.Should().BeTrue("some straggler must arrive earlier than everything already folded (genesis-depth rollback)");
+ }
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/Generators.cs b/src/SIL.Harmony.Tests/PropertyBased/Generators.cs
new file mode 100644
index 0000000..be55087
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/Generators.cs
@@ -0,0 +1,288 @@
+using CsCheck;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// CsCheck generators that force the rollback bug surface: stragglers, ties, cascades,
+/// duplicates, and batching. Adapted from the handoff doc's §7 recipe to Harmony's commit
+/// model. Author time is drawn from a SMALL range and is INDEPENDENT of arrival order (so
+/// stragglers are the norm and rollback is exercised); entities come from a SMALL pool (so
+/// commits contend and canonical order decides the value); duplicates and random batching are
+/// always present. Commit ids and times are deterministic functions of the generated integers,
+/// so a failing case reproduces exactly.
+///
+/// Tier 1 uses only SetWordTextChange (create-or-edit), so every schedule
+/// is valid in any order. Tier 2 adds creates, deletes, notes, definitions,
+/// antonym/word→definition reference cascades, and fractional ordering; it keeps schedules
+/// valid by time-banding (word creates < definition creates < all edits), so every
+/// entity is canonically created before it is edited or deleted (an edit/delete of a
+/// not-yet-created entity throws by design — see SnapshotWorker.ApplyCommitChanges).
+///
+internal static class Generators
+{
+ private static readonly DateTimeOffset BaseDate = new(2020, 1, 1, 0, 0, 0, TimeSpan.Zero);
+
+ private static HybridDateTime Time(int hour) => new(BaseDate.AddHours(hour), 0);
+
+ /// Deterministic Guid from a tag + index, so the same schedule reproduces identical ids.
+ private static Guid Det(byte tag, int i)
+ {
+ Span b = stackalloc byte[16];
+ b[0] = tag;
+ BitConverter.TryWriteBytes(b[1..], i);
+ return new Guid(b);
+ }
+
+ private static Guid WordId(int i) => Det(0x02, i);
+ private static Guid DefId(int i) => Det(0x03, i);
+ private static Guid CommitId(int i) => Det(0x01, i);
+
+ // ---- Tier 1: create-or-edit text only ------------------------------------------------
+
+ public static readonly Gen Tier1 =
+ from n in Gen.Int[1, 30]
+ from hours in Gen.Int[0, 8].Array[n] // small range => ties + varied-depth stragglers
+ from deep in Gen.Int[0, 9].Array[n] // ~10% chance a commit is a deep straggler
+ from entityIdx in Gen.Int[0, 3].Array[n] // small entity pool => contention
+ from textIdx in Gen.Int[0, 5].Array[n]
+ let specs = BuildTier1Specs(n, hours, deep, entityIdx, textIdx)
+ let deps = NoDependencies(specs.Length)
+ from arrivalsA in ArrivalPlan(specs, deps)
+ from arrivalsB in ArrivalPlan(specs, deps)
+ select new Schedule(specs, arrivalsA, arrivalsB);
+
+ private static CommitSpec[] BuildTier1Specs(int n, int[] hours, int[] deep, int[] entityIdx, int[] textIdx)
+ {
+ var specs = new CommitSpec[n];
+ for (var i = 0; i < n; i++)
+ {
+ var hour = deep[i] == 0 ? -5 : hours[i];
+ ChangeSpec change = new SetWordTextSpec(WordId(entityIdx[i]), "t" + textIdx[i]);
+ specs[i] = new CommitSpec(CommitId(i), Time(hour), new[] { change });
+ }
+ return specs;
+ }
+
+ // ---- Tier 2: creates, deletes, notes, definitions, references, ordering --------------
+
+ // Time bands guarantee canonical validity regardless of arrival order:
+ // word creates in [0,3] < definition creates in [4,7] < all edits/deletes in [8,14].
+ private const int EditLow = 8, EditHigh = 14;
+
+ public static readonly Gen Tier2 =
+ from wCount in Gen.Int[1, 3]
+ from dCount in Gen.Int[0, 3]
+ from wCreateHour in Gen.Int[0, 3].Array[wCount]
+ from dCreateHour in Gen.Int[4, 7].Array[Math.Max(dCount, 1)]
+ from dWord in Gen.Int[0, 999].Array[Math.Max(dCount, 1)]
+ from editCount in Gen.Int[0, 12]
+ from editKind in Gen.Int[0, 1].Array[Math.Max(editCount, 1)] // 0 = word edit, 1 = definition edit
+ from editTarget in Gen.Int[0, 999].Array[Math.Max(editCount, 1)]
+ from editOp in Gen.Int[0, 2].Array[Math.Max(editCount, 1)]
+ from editHour in Gen.Int[EditLow, EditHigh].Array[Math.Max(editCount, 1)]
+ from editVal in Gen.Int[0, 4].Array[Math.Max(editCount, 1)]
+ from antCount in Gen.Int[0, 2]
+ from antFrom in Gen.Int[0, 999].Array[Math.Max(antCount, 1)]
+ from antTo in Gen.Int[0, 999].Array[Math.Max(antCount, 1)]
+ from antHour in Gen.Int[EditLow, EditHigh].Array[Math.Max(antCount, 1)]
+ let specSet = BuildTier2Specs(wCount, dCount, wCreateHour, dCreateHour, dWord,
+ editCount, editKind, editTarget, editOp, editHour, editVal,
+ antCount, antFrom, antTo, antHour)
+ from arrivalsA in ArrivalPlan(specSet.Specs, specSet.Deps)
+ from arrivalsB in ArrivalPlan(specSet.Specs, specSet.Deps)
+ select new Schedule(specSet.Specs, arrivalsA, arrivalsB);
+
+ /// Generated commits plus, for each commit, the indices of commits that must ARRIVE before it.
+ private sealed record SpecSet(CommitSpec[] Specs, int[][] Deps);
+
+ private static SpecSet BuildTier2Specs(
+ int wCount, int dCount, int[] wCreateHour, int[] dCreateHour, int[] dWord,
+ int editCount, int[] editKind, int[] editTarget, int[] editOp, int[] editHour, int[] editVal,
+ int antCount, int[] antFrom, int[] antTo, int[] antHour)
+ {
+ var specs = new List();
+ // For each commit, the single create it depends on arriving first (-1 = no dependency).
+ var depDependsOnEntity = new List();
+ var createIndexByEntity = new Dictionary();
+ var commitIndex = 0;
+
+ // A create registers its entity's create index; an edit records the entity it needs present.
+ void Add(int hour, ChangeSpec change, Guid? createdEntity, Guid? dependsOnEntity)
+ {
+ if (createdEntity is { } created) createIndexByEntity[created] = commitIndex;
+ specs.Add(new CommitSpec(CommitId(commitIndex), Time(hour), new[] { change }));
+ depDependsOnEntity.Add(dependsOnEntity);
+ commitIndex++;
+ }
+
+ // Word creates (band [0,3]) — depend on nothing.
+ for (var w = 0; w < wCount; w++)
+ Add(wCreateHour[w], new NewWordSpec(WordId(w), "w" + w), createdEntity: WordId(w), dependsOnEntity: null);
+
+ // Definition creates (band [4,7]) — need their word to have arrived (projected-table FK).
+ for (var d = 0; d < dCount; d++)
+ {
+ var word = dWord[d] % wCount;
+ Add(dCreateHour[d], new NewDefinitionSpec(DefId(d), WordId(word), "d" + d, "pos" + d, d),
+ createdEntity: DefId(d), dependsOnEntity: WordId(word));
+ }
+
+ // Edits / deletes (band [8,14]) — need their subject entity to have arrived.
+ for (var e = 0; e < editCount; e++)
+ {
+ var editsDefinition = dCount > 0 && editKind[e] == 1;
+ if (!editsDefinition)
+ {
+ var w = editTarget[e] % wCount;
+ ChangeSpec change = (editOp[e] % 3) switch
+ {
+ 0 => new SetWordTextSpec(WordId(w), "wt" + editVal[e]),
+ 1 => new SetWordNoteSpec(WordId(w), "nn" + editVal[e]),
+ _ => new DeleteWordSpec(WordId(w)),
+ };
+ Add(editHour[e], change, createdEntity: null, dependsOnEntity: WordId(w));
+ }
+ else
+ {
+ var d = editTarget[e] % dCount;
+ ChangeSpec change = (editOp[e] % 2) == 0
+ ? new SetDefinitionPartOfSpeechSpec(DefId(d), "pp" + editVal[e])
+ : new DeleteDefinitionSpec(DefId(d));
+ Add(editHour[e], change, createdEntity: null, dependsOnEntity: DefId(d));
+ }
+ }
+
+ // Antonym references between distinct words (band [8,14]) — need the SUBJECT word present.
+ // The target word need not have arrived: SetAntonymReferenceChange no-ops on a missing target.
+ if (wCount >= 2)
+ {
+ for (var a = 0; a < antCount; a++)
+ {
+ var from = antFrom[a] % wCount;
+ var to = antTo[a] % wCount;
+ if (from == to) continue;
+ Add(antHour[a], new SetAntonymSpec(WordId(from), WordId(to)), createdEntity: null, dependsOnEntity: WordId(from));
+ }
+ }
+
+ // Resolve each dependency-entity to the index of that entity's create commit.
+ var deps = new int[specs.Count][];
+ for (var i = 0; i < specs.Count; i++)
+ {
+ deps[i] = depDependsOnEntity[i] is { } entity && createIndexByEntity.TryGetValue(entity, out var createIdx)
+ ? new[] { createIdx }
+ : Array.Empty();
+ }
+
+ return new SpecSet(specs.ToArray(), deps);
+ }
+
+ private static int[][] NoDependencies(int count)
+ {
+ var deps = new int[count][];
+ for (var i = 0; i < count; i++) deps[i] = Array.Empty();
+ return deps;
+ }
+
+ // ---- Shared arrival planning ---------------------------------------------------------
+
+ ///
+ /// A delivery plan: the full commit set delivered in a random order that RESPECTS
+ /// dependencies (each commit arrives no earlier than the commits in ),
+ /// split into consecutive batches, followed by duplicate re-send batches. Arrival order is
+ /// otherwise independent of author time, so stragglers, cascades and genesis-depth rollbacks
+ /// abound — a low-keyed create arriving after other entities' high-keyed edits is still a
+ /// straggler. Respecting dependencies mirrors real Harmony sync, which never delivers an
+ /// edit before the create it needs. Duplicates always land in their own batches (a re-send of
+ /// already-present commits), keeping each batch free of within-batch id collisions.
+ ///
+ private static Gen> ArrivalPlan(CommitSpec[] specs, int[][] deps) =>
+ from order in RandomLinearExtension(specs, deps)
+ from originalBatches in SplitIntoBatches(order)
+ from dupCount in Gen.Int[0, specs.Length / 3]
+ from dupPick in Gen.Shuffle(specs)
+ let dups = dupPick.Take(dupCount).ToArray()
+ from dupBatches in dupCount == 0
+ ? Gen.Const(Array.Empty())
+ : SplitIntoBatches(dups)
+ select (IReadOnlyList)originalBatches
+ .Concat(dupBatches)
+ .Select(b => new Arrival(b))
+ .ToList();
+
+ ///
+ /// A uniformly-random-ish topological order (linear extension of the dependency DAG). Kahn's
+ /// algorithm, breaking ties among ready commits by a generated priority — so different
+ /// priority draws yield different valid arrival orders, while a dependency never precedes the
+ /// commit that requires it.
+ ///
+ private static Gen RandomLinearExtension(CommitSpec[] specs, int[][] deps)
+ {
+ var n = specs.Length;
+ if (n <= 1) return Gen.Const(specs);
+ return Gen.Int[0, int.MaxValue].Array[n].Select(priorities =>
+ {
+ var indegree = new int[n];
+ var dependents = new List[n];
+ for (var i = 0; i < n; i++) dependents[i] = new List();
+ for (var i = 0; i < n; i++)
+ {
+ foreach (var dep in deps[i])
+ {
+ indegree[i]++;
+ dependents[dep].Add(i);
+ }
+ }
+
+ // Ready set, always popping the smallest (priority, index) — a deterministic linear extension.
+ var ready = new List();
+ for (var i = 0; i < n; i++)
+ if (indegree[i] == 0) ready.Add(i);
+
+ var order = new CommitSpec[n];
+ var emitted = 0;
+ while (ready.Count > 0)
+ {
+ var bestPos = 0;
+ for (var k = 1; k < ready.Count; k++)
+ {
+ var a = ready[k];
+ var b = ready[bestPos];
+ if (priorities[a] < priorities[b] || (priorities[a] == priorities[b] && a < b)) bestPos = k;
+ }
+ var next = ready[bestPos];
+ ready.RemoveAt(bestPos);
+ order[emitted++] = specs[next];
+ foreach (var dependent in dependents[next])
+ if (--indegree[dependent] == 0) ready.Add(dependent);
+ }
+
+ // Cycles are impossible by construction; guard anyway so a bug surfaces loudly.
+ if (emitted != n) throw new InvalidOperationException("dependency cycle in generated schedule");
+ return order;
+ });
+ }
+
+ private static Gen SplitIntoBatches(CommitSpec[] stream)
+ {
+ if (stream.Length <= 1) return Gen.Const(new[] { stream });
+ return Gen.Bool.Array[stream.Length - 1].Select(cuts => PartitionByCuts(stream, cuts));
+ }
+
+ private static CommitSpec[][] PartitionByCuts(CommitSpec[] stream, bool[] cuts)
+ {
+ var batches = new List();
+ var current = new List { stream[0] };
+ for (var i = 1; i < stream.Length; i++)
+ {
+ if (cuts[i - 1])
+ {
+ batches.Add(current.ToArray());
+ current = new List();
+ }
+ current.Add(stream[i]);
+ }
+ batches.Add(current.ToArray());
+ return batches.ToArray();
+ }
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/HarmonyEngineHarness.cs b/src/SIL.Harmony.Tests/PropertyBased/HarmonyEngineHarness.cs
new file mode 100644
index 0000000..92b0ae9
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/HarmonyEngineHarness.cs
@@ -0,0 +1,89 @@
+using SIL.Harmony.Changes;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// The projected value we compare across engines/replays. Deterministic across runs and
+/// across models: per-entity content signature (including deleted flag) plus the canonical
+/// commit-hash chain. Deliberately excludes ObjectSnapshot.Id, which is
+/// Guid.NewGuid() per run and would otherwise make identical projections compare unequal.
+///
+public sealed record Projection(IReadOnlyDictionary Entities, string? LastCommitHash);
+
+///
+/// Bridges generated s to a real Harmony .
+/// Each helper builds fresh in-memory engines (via , which
+/// wires an in-memory SQLite SampleDbContext, a deterministic MockTimeProvider,
+/// and AlwaysValidateCommits = true so the hash-chain check runs for free after every
+/// ingest) and disposes them. Commits are minted fresh per feed so no engine ever mutates a
+/// commit another engine also holds.
+///
+internal static class HarmonyEngineHarness
+{
+ private static readonly Guid ClientId = new("00000000-0000-0000-0000-0000000000AA");
+
+ /// Mint a fresh from an immutable spec. Fresh per call because the engine mutates commit hashes during ingest.
+ public static Commit ToCommit(CommitSpec spec)
+ {
+ var commit = new Commit(spec.Id)
+ {
+ ClientId = ClientId,
+ HybridDateTime = spec.Time,
+ };
+ for (var i = 0; i < spec.Changes.Count; i++)
+ {
+ var change = spec.Changes[i];
+ commit.ChangeEntities.Add(new ChangeEntity
+ {
+ Change = change.ToChange(),
+ Index = i,
+ CommitId = spec.Id,
+ EntityId = change.EntityId,
+ });
+ }
+ return commit;
+ }
+
+ /// Ingest each arrival batch in order via the sync path (the straggler/rollback entry point).
+ public static async Task Feed(DataModel model, IEnumerable arrivals)
+ {
+ foreach (var arrival in arrivals)
+ {
+ var batch = arrival.Batch.Select(ToCommit).ToArray();
+ await ((ISyncable)model).AddRangeFromSync(batch);
+ }
+ }
+
+ /// Ingest a flat set of commits as a single batch.
+ public static async Task Feed(DataModel model, IEnumerable specs)
+ {
+ var batch = specs.Select(ToCommit).ToArray();
+ await ((ISyncable)model).AddRangeFromSync(batch);
+ }
+
+ ///
+ /// Read the projected state as a comparable value. Iterates the current snapshot of every
+ /// entity (words and definitions, including deleted ones), capturing a deleted flag and a
+ /// type-specific content signature, plus the canonical commit-hash chain.
+ ///
+ public static async Task Read(DataModel model)
+ {
+ var entities = new Dictionary();
+ await foreach (var snapshot in model.GetLatestSnapshots())
+ {
+ var marker = snapshot.EntityIsDeleted ? "X:" : "-:";
+ entities[snapshot.EntityId] = marker + EntitySignature.Of(snapshot.Entity.DbObject);
+ }
+
+ var projectSnapshot = await model.GetProjectSnapshot();
+ return new Projection(entities, projectSnapshot.LastCommitHash);
+ }
+
+ /// Build a fresh in-memory engine. Caller must dispose the returned harness.
+ public static async Task NewEngine()
+ {
+ var engine = new DataModelTestBase();
+ await engine.InitializeAsync();
+ return engine;
+ }
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/ProjectionProperties.cs b/src/SIL.Harmony.Tests/PropertyBased/ProjectionProperties.cs
new file mode 100644
index 0000000..eeeb9fd
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/ProjectionProperties.cs
@@ -0,0 +1,152 @@
+using CsCheck;
+using static SIL.Harmony.Tests.PropertyBased.HarmonyEngineHarness;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// Property-based tests for Harmony's incremental rollback-and-replay projection engine.
+/// Each property drives real instances over generated schedules that
+/// inject stragglers, ties, cascades, duplicates and batching (see ).
+/// Every property runs against two generators: Tier 1 (create-or-edit text only) and
+/// Tier 2 (creates, deletes, notes, definitions, reference cascades, and ordering).
+///
+/// Oracles (see PropertyBased/README.md for the full rationale):
+/// - Replica convergence (primary, fully independent): the same commit set delivered
+/// in two independent arrival orders must project identically.
+/// - Incremental == from-scratch (secondary): the incrementally-rolled-back projection
+/// must equal RegenerateSnapshots(), which bypasses the rollback-specific machinery.
+///
+/// A failure that shrinks to a genuine engine defect is a real finding — capture the CsCheck
+/// seed it prints and the minimized schedule; do not weaken the property to make it pass.
+/// Raise CsCheck_Iter / CsCheck_Time in CI; failures replay via CsCheck_Seed=<seed>.
+///
+public class ProjectionProperties
+{
+ private static void AssertSameProjection(Projection a, Projection b, string because)
+ {
+ a.Entities.Should().BeEquivalentTo(b.Entities, because);
+ a.LastCommitHash.Should().Be(b.LastCommitHash, because);
+ }
+
+ // ---- Oracle bodies, parameterized by generator ---------------------------------------
+
+ ///
+ /// P-converge (doc P1 / P-master): the projection is a pure function of the change SET.
+ /// Two fresh replicas fed the same commits in independently shuffled/batched orders must
+ /// converge to identical entity content and the same canonical commit-hash chain. Primary,
+ /// order-independent oracle: any order-dependent rollback or tiebreak bug diverges here.
+ ///
+ private static Task ConvergesAcrossArrivalOrders(Gen schedules)
+ {
+ var output = TestContext.Current.TestOutputHelper;
+ return schedules.SampleAsync(async schedule =>
+ {
+ await using var replicaA = await NewEngine();
+ await using var replicaB = await NewEngine();
+
+ await Feed(replicaA.DataModel, schedule.ArrivalsA);
+ await Feed(replicaB.DataModel, schedule.ArrivalsB);
+
+ AssertSameProjection(
+ await Read(replicaA.DataModel),
+ await Read(replicaB.DataModel),
+ "two replicas receiving the same commit set in different arrival orders must converge");
+ }, print: s => ReproCode.Emit(output, s, ReproTemplate.Converge));
+ }
+
+ ///
+ /// P-regenerate (doc P-master, secondary oracle): the state built incrementally by the
+ /// rollback engine must equal a full from-scratch replay via RegenerateSnapshots(),
+ /// which rebuilds without any rollback machinery.
+ ///
+ private static Task IncrementalEqualsFromScratch(Gen schedules)
+ {
+ var output = TestContext.Current.TestOutputHelper;
+ return schedules.SampleAsync(async schedule =>
+ {
+ await using var engine = await NewEngine();
+
+ await Feed(engine.DataModel, schedule.ArrivalsA);
+ var incremental = await Read(engine.DataModel);
+
+ await engine.DataModel.RegenerateSnapshots();
+ var fromScratch = await Read(engine.DataModel);
+
+ AssertSameProjection(
+ incremental,
+ fromScratch,
+ "the incrementally rolled-back projection must equal a from-scratch replay of the same commits");
+ }, print: s => ReproCode.Emit(output, s, ReproTemplate.IncrementalVsFromScratch));
+ }
+
+ ///
+ /// P-dup (doc §5.4): re-ingesting commits already in the log is idempotent. Re-sending the
+ /// entire commit set as one batch must not change the projection or the commit-hash chain.
+ ///
+ private static Task ReingestIsIdempotent(Gen schedules)
+ {
+ var output = TestContext.Current.TestOutputHelper;
+ return schedules.SampleAsync(async schedule =>
+ {
+ await using var engine = await NewEngine();
+
+ await Feed(engine.DataModel, schedule.ArrivalsA);
+ var before = await Read(engine.DataModel);
+
+ await Feed(engine.DataModel, schedule.Commits);
+ var after = await Read(engine.DataModel);
+
+ AssertSameProjection(before, after, "re-ingesting already-present commits must leave the projection unchanged");
+ }, print: s => ReproCode.Emit(output, s, ReproTemplate.ReingestIdempotent));
+ }
+
+ ///
+ /// R-determinism (doc §5.6): replay is reproducible. Feeding the identical schedule to two
+ /// fresh engines yields identical projected content and commit-hash chains.
+ ///
+ private static Task ReplayIsDeterministic(Gen schedules)
+ {
+ var output = TestContext.Current.TestOutputHelper;
+ return schedules.SampleAsync(async schedule =>
+ {
+ await using var first = await NewEngine();
+ await using var second = await NewEngine();
+
+ await Feed(first.DataModel, schedule.ArrivalsA);
+ await Feed(second.DataModel, schedule.ArrivalsA);
+
+ AssertSameProjection(
+ await Read(first.DataModel),
+ await Read(second.DataModel),
+ "feeding the identical schedule twice must produce identical projections");
+ }, print: s => ReproCode.Emit(output, s, ReproTemplate.ReplayDeterministic));
+ }
+
+ // ---- Tier 1: create-or-edit text only ------------------------------------------------
+
+ [Fact]
+ public Task Tier1_Projection_IsIndependentOfArrivalOrder() => ConvergesAcrossArrivalOrders(Generators.Tier1);
+
+ [Fact]
+ public Task Tier1_IncrementalProjection_EqualsFromScratchReplay() => IncrementalEqualsFromScratch(Generators.Tier1);
+
+ [Fact]
+ public Task Tier1_ReingestingExistingCommits_IsIdempotent() => ReingestIsIdempotent(Generators.Tier1);
+
+ [Fact]
+ public Task Tier1_Replay_IsDeterministic() => ReplayIsDeterministic(Generators.Tier1);
+
+ // ---- Tier 2: creates, deletes, definitions, references, ordering ---------------------
+
+ [Fact]
+ public Task Tier2_Projection_IsIndependentOfArrivalOrder() => ConvergesAcrossArrivalOrders(Generators.Tier2);
+
+ [Fact]
+ public Task Tier2_IncrementalProjection_EqualsFromScratchReplay() => IncrementalEqualsFromScratch(Generators.Tier2);
+
+ [Fact]
+ public Task Tier2_ReingestingExistingCommits_IsIdempotent() => ReingestIsIdempotent(Generators.Tier2);
+
+ [Fact]
+ public Task Tier2_Replay_IsDeterministic() => ReplayIsDeterministic(Generators.Tier2);
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/README.md b/src/SIL.Harmony.Tests/PropertyBased/README.md
new file mode 100644
index 0000000..7f8a71a
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/README.md
@@ -0,0 +1,181 @@
+# Property-based tests for the rollback-and-replay engine
+
+> ## ⚠️ These tests currently fail on `main` — by design
+>
+> The **Tier 2** properties have found a **real bug in Harmony's incremental rollback
+> engine** and are intentionally left red as a living reproduction (no engine fix and no
+> test weakening). Tier 1 and the generator meta-tests pass.
+>
+> **Symptom:** a `SetDefinitionPartOfSpeechChange` on a `Definition` is *dropped* by the
+> incremental rollback/resume when a straggler commit arrives, while a full from-scratch
+> replay applies it. Reproduced two independent ways:
+> - **Replica convergence** (`Tier2_Projection_IsIndependentOfArrivalOrder`): the same
+> commit set in two arrival orders projects to different `Definition.PartOfSpeech`.
+> - **Incremental ≠ from-scratch** (`Tier2_IncrementalProjection_EqualsFromScratchReplay`):
+> feeding a schedule then calling `RegenerateSnapshots()` (the trusted oracle) on the
+> *same* engine yields different projected state. Since from-scratch replay of the
+> persisted commit log is ground truth, the incremental path is the wrong one.
+>
+> **Minimized shape (~15 commits):** create word + definition on it, `SetDefinitionPartOfSpeech`
+> on the definition, then `DeleteDefinition` + `DeleteWord` (reference cascade) + a second
+> `DeleteDefinition`, with the part-of-speech edit arriving as a straggler after later
+> commits are already folded. This is the doc's "stale-snapshot / wrong rollback target"
+> class; the suspected code is the resume-from-surviving-intermediate-snapshot path in
+> `SnapshotWorker` interacting with `CrdtRepository.DeleteStaleSnapshots`.
+>
+> **Deterministic replay** (CsCheck reproduces the shrunk counterexample from a seed):
+> ```bash
+> CsCheck_Seed=0WhakBBZlgK1 dotnet test src/SIL.Harmony.Tests \
+> --filter-method "*Tier2_IncrementalProjection_EqualsFromScratchReplay*"
+> ```
+> (Seeds are tied to this CsCheck version/generator; re-run the property to mint a fresh
+> one if they drift.)
+
+
+These [CsCheck](https://github.com/AnthonyLloyd/CsCheck) property tests exercise
+Harmony's incremental projection engine: the machinery that, when a commit arrives
+with an author time *earlier* than commits already folded into the projection, rolls
+back to earlier state and replays forward with the straggler slotted into canonical
+order (`DataModel.AddRangeFromSync` → `CrdtRepository.AddNewCommits` /
+`DeleteStaleSnapshots` → `SnapshotWorker`). This is the code most prone to off-by-one
+rollback targets, tie mishandling, stale-snapshot invalidation, and snapshot aliasing,
+and it was previously covered only by example-based tests.
+
+The suite is inspired by a generic "rollback-and-replay projection engine" testing
+handoff, adapted to Harmony's real types. The mapping:
+
+| Generic concept | Harmony |
+|---|---|
+| A change event | A `Commit` (`HybridDateTime`, `ClientId`, `Id`, ordered `ChangeEntities`) |
+| Canonical total order | `CommitBase.CompareKey = (HybridDateTime.DateTime, Counter, Id)` |
+| Ingest a (possibly late/duplicate) batch | `((ISyncable)DataModel).AddRangeFromSync(commits)` |
+| Rollback to checkpoint + replay | `DeleteStaleSnapshots` + `SnapshotWorker` |
+| From-scratch replay | `DataModel.RegenerateSnapshots()` |
+| Content-addressed dedup | Commit-`Id` dedup in `FilterExistingCommits` |
+
+## Oracles
+
+Harmony's projection logic (create/edit/delete/reference-cascade) is non-trivial, so a
+"dead-simple sorted-fold oracle" would just duplicate `SnapshotWorker`. Instead the
+suite leans on two oracles that are strong together:
+
+1. **Replica convergence** (primary, fully independent) — the same commit *set*
+ delivered to two fresh engines in two independent arrival orders / batchings must
+ project identically. This is genuinely independent of any single code path
+ (replica-vs-replica), and different arrival orders create different straggler and
+ rollback patterns, so any order-dependent rollback or tiebreak bug shows up as a
+ divergence. Implemented by `Projection_IsIndependentOfArrivalOrder`.
+
+2. **Incremental == from-scratch** (secondary) — the state built incrementally by the
+ rollback engine must equal `RegenerateSnapshots()`, which deletes all snapshots and
+ projected tables and rebuilds without any rollback machinery
+ (`DeleteStaleSnapshots`, surviving-snapshot resumption, `AddNewCommits`
+ hash-rechaining, the every-other-commit retention optimization are all bypassed).
+ So a bug in that machinery surfaces as incremental ≠ regenerate. This is *not* a
+ fully independent oracle (it shares the leaf projection code); oracle #1 covers the
+ gap. Implemented by `IncrementalProjection_EqualsFromScratchReplay`.
+
+### Compared value
+
+Projections are compared by **entity content** (`QueryLatest()` → id⇒text) plus
+the **canonical commit-hash chain** (`GetProjectSnapshot().LastCommitHash`). We
+deliberately exclude `ObjectSnapshot.Id`, which is `Guid.NewGuid()` per run and would
+make identical projections compare unequal.
+
+## Properties
+
+| Test | Role |
+|---|---|
+| `Projection_IsIndependentOfArrivalOrder` | Replica convergence (P1 / P-master) — primary. |
+| `IncrementalProjection_EqualsFromScratchReplay` | Incremental == from-scratch (P-master) — secondary oracle. |
+| `ReingestingExistingCommits_IsIdempotent` | Duplicate re-send changes nothing (P-dup). |
+| `Replay_IsDeterministic` | Same schedule twice ⇒ identical projection (R-determinism). |
+| `GeneratorMetaTests.Generator_Produces_AllRollbackPhenomena` | Proves the generator actually emits ties, stragglers, cascades, duplicates, and genesis-depth rollbacks. |
+
+## Generators (`Generators.cs`)
+
+Author time is drawn from a **small** range and is **independent of arrival order**, so
+stragglers are the norm; entities come from a **small pool** so commits contend and
+order decides the value; ~10% of commits are **deep stragglers** (well before the rest)
+to force rollback toward genesis; **duplicates** and random **batching** are always
+present. Commit ids and times are deterministic functions of the generated integers, so
+a failing case reproduces exactly.
+
+Tier 1 (current) uses only `SetWordTextChange`, which supports **both** create and edit,
+so every schedule is valid regardless of order. (A delete or edit of a not-yet-created
+entity throws *by design* — see `SnapshotWorker.ApplyCommitChanges` — so those changes
+require a "create is canonically first" guarantee, added in Tier 2.)
+
+## Running
+
+Default (local, low iteration count baked into CsCheck):
+
+```bash
+dotnet test src/SIL.Harmony.Tests --filter-class "*ProjectionProperties*"
+```
+
+Each iteration spins up in-memory SQLite engines, so iterations are not free. Tune the
+budget with CsCheck environment variables:
+
+```bash
+# Run each property for 60 seconds instead of the default iteration count
+CsCheck_Iter=1000000 CsCheck_Time=60 dotnet test src/SIL.Harmony.Tests --filter-class "*ProjectionProperties*"
+
+# Or a fixed iteration count
+CsCheck_Iter=1000 dotnet test src/SIL.Harmony.Tests --filter-class "*ProjectionProperties*"
+```
+
+CI should raise `CsCheck_Iter` (or set `CsCheck_Time`) well above the local default.
+
+### Reproducing a failure
+
+On failure CsCheck prints the shrunk counterexample and a **seed**. Replay it with:
+
+```bash
+CsCheck_Seed= dotnet test src/SIL.Harmony.Tests --filter-class "*ProjectionProperties*"
+```
+
+**A failure that shrinks to a genuine engine defect is a real finding, not a test bug.**
+Capture the seed and the minimized schedule and report it — do not loosen the property
+or special-case the oracle to make it pass. Only relax a property if it is genuinely
+wrong about Harmony's intended semantics (and say so explicitly).
+
+### Ready-to-run reproduction in the test output
+
+On failure each property emits **the full C# source of a self-contained `[Fact]`** with
+the shrunk counterexample hard-coded — no CsCheck, no seed, no shrinking needed to re-run
+it. Copy the emitted `Repro_*` method into a class that has
+`using static SIL.Harmony.Tests.PropertyBased.HarmonyEngineHarness;` (e.g.
+`ProjectionProperties`) and run it directly to debug or attach to the bug report. There
+is one body template per property type (`ReproTemplate`); each `ChangeSpec` renders itself
+via `ToCode()`. Keep the templates in `ReproCode.Body` in sync with the property bodies.
+
+The method is written to the **test output** (`ITestOutputHelper`), which shows in full in
+CI logs, because CsCheck hard-caps the value it embeds in the exception *message* at 5000
+characters — larger reproductions would be clipped there. The exception message therefore
+carries only the compact schedule summary and a pointer to the test output. `ReproCode.Emit`
+(passed as CsCheck's `print:`) does this; it is invoked once, on the final shrunk case.
+
+## Proving the suite bites
+
+The strongest evidence is empirical: **the suite already caught a real, pre-existing bug
+in the shipping engine** (see the banner at the top) — not an injected one. The generator
+meta-tests are the committed, standing proof that the axes (ties, stragglers, cascades,
+duplicates, genesis-depth rollbacks) are actually exercised.
+
+For additional bug-injection evidence, temporarily break real engine code, run the suite,
+confirm the named property fails and shrinks small, capture the seed + minimized schedule,
+then revert (no broken code is committed). Suggested injections and the property each
+should trip:
+
+- **Weak tiebreak** — drop `Id` from `CommitBase.CompareKey` (author time + counter
+ only) ⇒ `Projection_IsIndependentOfArrivalOrder` fails, shrinking to two equal-keyed
+ commits differing only by id.
+- **Wrong stale-snapshot boundary** — perturb the `DeleteStaleSnapshots` / `WhereAfter`
+ boundary by one ⇒ `IncrementalProjection_EqualsFromScratchReplay` (and convergence)
+ fail on a straggler landing just before a retained snapshot.
+- **Aliasing** (Tier 2, once mutable multi-field entities are generated) — remove a
+ `Copy()` in `SnapshotWorker`/`CrdtRepository` so a checkpoint aliases live state ⇒
+ convergence / snapshot-consistency fail after a rollback.
+
+Record the observed counterexamples and seeds in the PR description.
diff --git a/src/SIL.Harmony.Tests/PropertyBased/ReproCode.cs b/src/SIL.Harmony.Tests/PropertyBased/ReproCode.cs
new file mode 100644
index 0000000..8b8b782
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/ReproCode.cs
@@ -0,0 +1,153 @@
+using System.Globalization;
+using System.Text;
+using Xunit;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+/// Which property body to emit in a hard-coded reproduction.
+public enum ReproTemplate
+{
+ Converge,
+ IncrementalVsFromScratch,
+ ReingestIdempotent,
+ ReplayDeterministic,
+}
+
+///
+/// Renders a failing as the C# source of a self-contained, ready-to-run
+/// xUnit test method with every generated value hard-coded — so a shrunk CsCheck counterexample
+/// can be pasted straight into the test project and debugged without CsCheck or a seed. Passed as
+/// the print: argument to CsCheck's SampleAsync, so it appears in the failure
+/// message. One body template per property type ().
+///
+/// The emitted method assumes it is pasted into a class with
+/// using static SIL.Harmony.Tests.PropertyBased.HarmonyEngineHarness; (e.g.
+/// ); it relies only on the harness statics and FluentAssertions.
+/// Keep the bodies here in sync with the property bodies in .
+///
+public static class ReproCode
+{
+ public static string Guid(Guid value) => $"System.Guid.Parse(\"{value:D}\")";
+
+ public static string Str(string? value) =>
+ value is null ? "null" : "\"" + value.Replace("\\", "\\\\").Replace("\"", "\\\"") + "\"";
+
+ public static string Dbl(double value) => value.ToString("R", CultureInfo.InvariantCulture);
+
+ private static string Time(HybridDateTime time) =>
+ $"new HybridDateTime(System.DateTimeOffset.Parse(\"{time.DateTime:O}\"), {time.Counter}L)";
+
+ ///
+ /// Writes the full ready-to-run reproduction to the test output (untruncated in CI logs) and
+ /// returns a compact summary for CsCheck's failure message, which CsCheck hard-caps at 5000
+ /// chars. Call this from a property's print: argument; CsCheck invokes it exactly once,
+ /// on the final shrunk counterexample. Pass the captured at the
+ /// start of the test (so it is available regardless of which thread CsCheck calls back on).
+ ///
+ public static string Emit(ITestOutputHelper? output, Schedule schedule, ReproTemplate template)
+ {
+ var code = Render(schedule, template);
+ if (output is not null) output.WriteLine(code);
+ else Console.WriteLine(code);
+ // Keep this short: CsCheck hard-caps the embedded message at 5000 chars. The full,
+ // untruncated method is in the test output above; the assertion diff follows below.
+ return $"Full ready-to-run reproduction ({schedule.Commits.Count} commits) written to the test output above — copy the Repro_{template} method to re-run without CsCheck.";
+ }
+
+ public static string Render(Schedule schedule, ReproTemplate template)
+ {
+ var indexById = new Dictionary();
+ for (var i = 0; i < schedule.Commits.Count; i++) indexById[schedule.Commits[i].Id] = i;
+
+ var sb = new StringBuilder();
+
+ sb.AppendLine("// ---- Ready-to-run reproduction (hard-coded CsCheck counterexample) ----");
+ sb.AppendLine("// Paste into a class with: using static SIL.Harmony.Tests.PropertyBased.HarmonyEngineHarness;");
+ sb.AppendLine("[Fact]");
+ sb.AppendLine($"public async Task {MethodName(template)}()");
+ sb.AppendLine("{");
+
+ // commits
+ sb.AppendLine(" var commits = new CommitSpec[]");
+ sb.AppendLine(" {");
+ foreach (var commit in schedule.Commits)
+ {
+ var changes = string.Join(", ", commit.Changes.Select(c => c.ToCode()));
+ sb.AppendLine($" new({Guid(commit.Id)}, {Time(commit.Time)}, new ChangeSpec[] {{ {changes} }}),");
+ }
+ sb.AppendLine(" };");
+ sb.AppendLine();
+
+ // arrivals
+ AppendArrivals(sb, "arrivalsA", schedule.ArrivalsA, indexById);
+ AppendArrivals(sb, "arrivalsB", schedule.ArrivalsB, indexById);
+ sb.AppendLine(" var schedule = new Schedule(commits, arrivalsA, arrivalsB);");
+ sb.AppendLine();
+
+ foreach (var line in Body(template)) sb.Append(" ").AppendLine(line);
+
+ sb.AppendLine("}");
+ return sb.ToString();
+ }
+
+ private static void AppendArrivals(StringBuilder sb, string name, IReadOnlyList arrivals, IReadOnlyDictionary indexById)
+ {
+ sb.AppendLine($" var {name} = new Arrival[]");
+ sb.AppendLine(" {");
+ foreach (var arrival in arrivals)
+ {
+ var refs = string.Join(", ", arrival.Batch.Select(c => $"commits[{indexById[c.Id]}]"));
+ sb.AppendLine($" new(new[] {{ {refs} }}),");
+ }
+ sb.AppendLine(" };");
+ }
+
+ private static string MethodName(ReproTemplate template) => "Repro_" + template;
+
+ private static IEnumerable Body(ReproTemplate template) => template switch
+ {
+ ReproTemplate.Converge =>
+ [
+ "await using var replicaA = await NewEngine();",
+ "await using var replicaB = await NewEngine();",
+ "await Feed(replicaA.DataModel, schedule.ArrivalsA);",
+ "await Feed(replicaB.DataModel, schedule.ArrivalsB);",
+ "var a = await Read(replicaA.DataModel);",
+ "var b = await Read(replicaB.DataModel);",
+ "a.Entities.Should().BeEquivalentTo(b.Entities, \"two replicas receiving the same commit set in different arrival orders must converge\");",
+ "a.LastCommitHash.Should().Be(b.LastCommitHash);",
+ ],
+ ReproTemplate.IncrementalVsFromScratch =>
+ [
+ "await using var engine = await NewEngine();",
+ "await Feed(engine.DataModel, schedule.ArrivalsA);",
+ "var incremental = await Read(engine.DataModel);",
+ "await engine.DataModel.RegenerateSnapshots();",
+ "var fromScratch = await Read(engine.DataModel);",
+ "incremental.Entities.Should().BeEquivalentTo(fromScratch.Entities, \"the incrementally rolled-back projection must equal a from-scratch replay of the same commits\");",
+ "incremental.LastCommitHash.Should().Be(fromScratch.LastCommitHash);",
+ ],
+ ReproTemplate.ReingestIdempotent =>
+ [
+ "await using var engine = await NewEngine();",
+ "await Feed(engine.DataModel, schedule.ArrivalsA);",
+ "var before = await Read(engine.DataModel);",
+ "await Feed(engine.DataModel, schedule.Commits);",
+ "var after = await Read(engine.DataModel);",
+ "before.Entities.Should().BeEquivalentTo(after.Entities, \"re-ingesting already-present commits must leave the projection unchanged\");",
+ "before.LastCommitHash.Should().Be(after.LastCommitHash);",
+ ],
+ ReproTemplate.ReplayDeterministic =>
+ [
+ "await using var first = await NewEngine();",
+ "await using var second = await NewEngine();",
+ "await Feed(first.DataModel, schedule.ArrivalsA);",
+ "await Feed(second.DataModel, schedule.ArrivalsA);",
+ "var a = await Read(first.DataModel);",
+ "var b = await Read(second.DataModel);",
+ "a.Entities.Should().BeEquivalentTo(b.Entities, \"feeding the identical schedule twice must produce identical projections\");",
+ "a.LastCommitHash.Should().Be(b.LastCommitHash);",
+ ],
+ _ => throw new ArgumentOutOfRangeException(nameof(template)),
+ };
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/Schedule.cs b/src/SIL.Harmony.Tests/PropertyBased/Schedule.cs
new file mode 100644
index 0000000..08576f5
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/Schedule.cs
@@ -0,0 +1,62 @@
+using System.Text;
+
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// An immutable description of a single commit to be minted at feed time.
+/// We store specs rather than instances because the engine
+/// mutates a commit's Hash/ParentHash (and attaches Snapshots) while ingesting it,
+/// so a single instance cannot be safely fed to two engines or
+/// replayed. Minting a fresh from a spec keeps the logical
+/// identity () stable so dedup and canonical ordering are reproducible.
+///
+/// Stable, deterministic commit id — the final canonical-order tiebreaker and the dedup key.
+/// The hybrid logical clock stamp used for canonical ordering.
+/// The change(s) this commit carries, applied in list order (ChangeEntity.Index).
+public sealed record CommitSpec(Guid Id, HybridDateTime Time, IReadOnlyList Changes)
+{
+ ///
+ /// The canonical total order key, matching CommitBase.CompareKey
+ /// (DateTime, then Counter, then Id). Used by the generator meta-tests to reason
+ /// about ties and stragglers without touching the engine.
+ ///
+ public (DateTimeOffset, long, Guid) CompareKey => (Time.DateTime, Time.Counter, Id);
+}
+
+/// One ingest batch: the commits that arrive together in a single sync call.
+public sealed record Arrival(IReadOnlyList Batch);
+
+///
+/// A generated test schedule: one canonical commit set, delivered two independent ways.
+/// and each deliver the full
+/// set (plus possible duplicate re-sends) in an independently
+/// shuffled and batched order, so a single set can be cross-checked for
+/// arrival-order independence (replica convergence).
+///
+public sealed record Schedule(
+ IReadOnlyList Commits,
+ IReadOnlyList ArrivalsA,
+ IReadOnlyList ArrivalsB)
+{
+ public override string ToString()
+ {
+ var sb = new StringBuilder();
+ sb.AppendLine($"Schedule: {Commits.Count} commits, {ArrivalsA.Count} arrivals A, {ArrivalsB.Count} arrivals B");
+ sb.AppendLine("Commits:");
+ foreach (var commit in Commits.OrderBy(c => c.CompareKey))
+ {
+ sb.AppendLine($" {commit.Id} @ {commit.Time} ({commit.Changes.Count} changes), [{string.Join(", ", commit.Changes.Select(c => $"EntityId: {c.EntityId}, Type: {c.GetType().Name}"))}]");
+ }
+ sb.AppendLine("Arrivals A:");
+ foreach (var arrival in ArrivalsA)
+ {
+ sb.AppendLine($" Batch of {arrival.Batch.Count} commits [{string.Join(", ", arrival.Batch.Select(c => c.Id))}]");
+ }
+ sb.AppendLine("Arrivals B:");
+ foreach (var arrival in ArrivalsB)
+ {
+ sb.AppendLine($" Batch of {arrival.Batch.Count} commits [{string.Join(", ", arrival.Batch.Select(c => c.Id))}]");
+ }
+ return sb.ToString();
+ }
+}
diff --git a/src/SIL.Harmony.Tests/PropertyBased/ScheduleAnalysis.cs b/src/SIL.Harmony.Tests/PropertyBased/ScheduleAnalysis.cs
new file mode 100644
index 0000000..3171efa
--- /dev/null
+++ b/src/SIL.Harmony.Tests/PropertyBased/ScheduleAnalysis.cs
@@ -0,0 +1,85 @@
+namespace SIL.Harmony.Tests.PropertyBased;
+
+///
+/// Pure (engine-free) analyses of a generated . Used by the generator
+/// meta-tests to prove the generator actually produces the phenomena the properties exist to
+/// stress. Per the handoff doc §7: "if the generator doesn't produce these, the suite is
+/// testing nothing." Ordering here mirrors CommitBase.CompareKey exactly.
+///
+internal static class ScheduleAnalysis
+{
+ private static readonly IComparer<(DateTimeOffset, long, Guid)> KeyComparer =
+ Comparer<(DateTimeOffset, long, Guid)>.Default;
+
+ private static int CompareKeys(CommitSpec a, CommitSpec b) => KeyComparer.Compare(a.CompareKey, b.CompareKey);
+
+ /// True if two commits share an author time (same DateTime + Counter) — the tiebreak path.
+ public static bool HasAuthorTimeTie(Schedule schedule) =>
+ schedule.Commits
+ .GroupBy(c => (c.Time.DateTime, c.Time.Counter))
+ .Any(g => g.Count() > 1);
+
+ ///
+ /// A "straggler" is a commit that arrives with a canonical key EARLIER than the maximum
+ /// key already delivered — i.e. it must be slotted into the past, forcing a rollback.
+ /// Returns the total number of stragglers across the whole delivery plan.
+ ///
+ public static int StragglerCount(IReadOnlyList arrivals)
+ {
+ var count = 0;
+ CommitSpec? maxSeen = null;
+ foreach (var commit in arrivals.SelectMany(a => a.Batch))
+ {
+ if (maxSeen is not null && CompareKeys(commit, maxSeen) < 0) count++;
+ if (maxSeen is null || CompareKeys(commit, maxSeen) > 0) maxSeen = commit;
+ }
+ return count;
+ }
+
+ ///
+ /// The largest number of stragglers contained in a single batch, measured against the state
+ /// BEFORE that batch. A value ≥ 2 is a "cascade": one ingest that must roll back for several
+ /// stragglers at once (and, correctly, to the earliest of them — not process each alone).
+ ///
+ public static int MaxCascade(IReadOnlyList arrivals)
+ {
+ var maxCascade = 0;
+ CommitSpec? maxSeen = null;
+ foreach (var arrival in arrivals)
+ {
+ var stragglersThisBatch = 0;
+ CommitSpec? maxInBatch = null;
+ foreach (var commit in arrival.Batch)
+ {
+ if (maxSeen is not null && CompareKeys(commit, maxSeen) < 0) stragglersThisBatch++;
+ if (maxInBatch is null || CompareKeys(commit, maxInBatch) > 0) maxInBatch = commit;
+ }
+ maxCascade = Math.Max(maxCascade, stragglersThisBatch);
+ if (maxInBatch is not null && (maxSeen is null || CompareKeys(maxInBatch, maxSeen) > 0)) maxSeen = maxInBatch;
+ }
+ return maxCascade;
+ }
+
+ /// True if any commit id is delivered in more than one batch (a duplicate re-send).
+ public static bool HasDuplicates(IReadOnlyList arrivals)
+ {
+ var total = arrivals.Sum(a => a.Batch.Count);
+ var distinct = arrivals.SelectMany(a => a.Batch).Select(c => c.Id).Distinct().Count();
+ return total > distinct;
+ }
+
+ ///
+ /// True if the globally-earliest commit (the new canonical genesis) is delivered after the
+ /// very first batch — arriving as a straggler earlier than everything already folded, which
+ /// forces a rollback all the way toward genesis.
+ ///
+ public static bool ForcesGenesisRebuild(Schedule schedule, IReadOnlyList arrivals)
+ {
+ if (arrivals.Count == 0) return false;
+ var globalMin = schedule.Commits.Aggregate((a, b) => CompareKeys(a, b) <= 0 ? a : b);
+ var firstBatchIds = arrivals[0].Batch.Select(c => c.Id).ToHashSet();
+ if (firstBatchIds.Contains(globalMin.Id)) return false;
+ // It forces a genesis rebuild only if something with a larger key was already folded first.
+ return arrivals[0].Batch.Any(c => CompareKeys(c, globalMin) > 0);
+ }
+}
diff --git a/src/SIL.Harmony.Tests/SIL.Harmony.Tests.csproj b/src/SIL.Harmony.Tests/SIL.Harmony.Tests.csproj
index 575f837..0ae7cb3 100644
--- a/src/SIL.Harmony.Tests/SIL.Harmony.Tests.csproj
+++ b/src/SIL.Harmony.Tests/SIL.Harmony.Tests.csproj
@@ -10,6 +10,7 @@
+