From e6942fce09c8c8a2b3e8f5a27ad8c4e699f57863 Mon Sep 17 00:00:00 2001
From: Dexter Ajoku <dex@dexcompiler.com>
Date: Sun, 8 Feb 2026 14:27:47 +0100
Subject: [PATCH 1/2] Add high-value property tests for HLC and vector clocks

---
 property-tests/HlcTimestampProperties.fs | 60 ++++++++++++++++++++++++
 property-tests/VectorClockProperties.fs  | 25 ++++++++++
 2 files changed, 85 insertions(+)

diff --git a/property-tests/HlcTimestampProperties.fs b/property-tests/HlcTimestampProperties.fs
index b0ef16c..6dc9b7b 100644
--- a/property-tests/HlcTimestampProperties.fs
+++ b/property-tests/HlcTimestampProperties.fs
@@ -6,6 +6,15 @@ open FsCheck.FSharp
 open FsCheck.Xunit
 open Clockworks.Distributed
 
+let private compareBytesLex (a: byte[]) (b: byte[]) =
+    let len = min a.Length b.Length
+    let mutable i = 0
+    let mutable cmp = 0
+    while i < len && cmp = 0 do
+        cmp <- compare a[i] b[i]
+        i <- i + 1
+    if cmp <> 0 then cmp else compare a.Length b.Length
+
 type HlcTimestampArb =
     static member HlcTimestamp() : FsCheck.Arbitrary<HlcTimestamp> =
         let maxWallTime = (1L <<< 48) - 1L
@@ -102,3 +111,54 @@ let ``WriteTo and ReadFrom form a round-trip`` (wallTimeMs: int64) (counter: uin
     let unpacked = HlcTimestamp.ReadFrom(System.ReadOnlySpan<byte>(buffer))
     
     unpacked = original
+
+/// Property: Packing masks counter/nodeId to their bit-widths (12-bit counter, 4-bit node)
+[<Property>]
+let ``ToPackedInt64 truncates counter and node id`` (wallTimeMs: int64) (counter: uint16) (nodeId: uint16) =
+    let safeWallTimeMs = abs wallTimeMs % (1L <<< 47) // avoid sign-bit issues when casting packed to long
+    let original = HlcTimestamp(safeWallTimeMs, counter, nodeId)
+    let unpacked = HlcTimestamp.FromPackedInt64(original.ToPackedInt64())
+
+    unpacked.WallTimeMs = safeWallTimeMs
+    && unpacked.Counter = (counter &&& 0x0FFFus)
+    && unpacked.NodeId = (nodeId &&& 0x000Fus)
+
+/// Property: String representation round-trips through Parse
+[<Property(Arbitrary = [| typeof<HlcTimestampArb> |])>]
+let ``ToString and Parse round-trip`` (ts: HlcTimestamp) =
+    HlcTimestamp.Parse(ts.ToString()) = ts
+
+/// Property: String representation round-trips through TryParse
+[<Property(Arbitrary = [| typeof<HlcTimestampArb> |])>]
+let ``ToString and TryParse round-trip`` (ts: HlcTimestamp) =
+    let ok, parsed = HlcTimestamp.TryParse(ts.ToString().AsSpan())
+    ok && parsed = ts
+
+/// Property: TryParse never throws and only returns true when output is stable
+[<Property>]
+let ``TryParse is non-throwing`` (s: string) =
+    try
+        let ok, parsed = HlcTimestamp.TryParse(s.AsSpan())
+        (not ok) || (parsed.ToString() = s)
+    with
+    | _ -> false
+
+/// Property: Operators are consistent with CompareTo
+[<Property(Arbitrary = [| typeof<HlcTimestampArb> |])>]
+let ``Operators are consistent with CompareTo`` (a: HlcTimestamp) (b: HlcTimestamp) =
+    (a < b) = (a.CompareTo(b) < 0)
+    && (a > b) = (a.CompareTo(b) > 0)
+    && (a <= b) = (a.CompareTo(b) <= 0)
+    && (a >= b) = (a.CompareTo(b) >= 0)
+
+/// Property: Big-endian encoding preserves ordering under lexicographic byte comparison
+[<Property(Arbitrary = [| typeof<HlcTimestampArb> |])>]
+let ``WriteTo encoding preserves lexicographic ordering`` (a: HlcTimestamp) (b: HlcTimestamp) =
+    let bufferA = Array.zeroCreate<byte> 10
+    let bufferB = Array.zeroCreate<byte> 10
+    a.WriteTo(Span<byte>(bufferA))
+    b.WriteTo(Span<byte>(bufferB))
+
+    let cmpTs = a.CompareTo(b)
+    let cmpBytes = compareBytesLex bufferA bufferB
+    sign cmpTs = sign cmpBytes
diff --git a/property-tests/VectorClockProperties.fs b/property-tests/VectorClockProperties.fs
index 2158d94..05fec15 100644
--- a/property-tests/VectorClockProperties.fs
+++ b/property-tests/VectorClockProperties.fs
@@ -69,3 +69,28 @@ let ``WriteTo and ReadFrom round-trip`` (clock: VectorClock) =
 let ``Increment moves clock forward`` (clock: VectorClock) (nodeId: uint16) =
     let incremented = clock.Increment(nodeId)
     incremented.Compare(clock) = VectorClockOrder.After
+
+/// Property: If a is before-or-equal b, Merge(a,b) = b (b is an upper bound)
+[<Property(Arbitrary = [| typeof<VectorClockArb> |])>]
+let ``Merge returns the upper bound when one input dominates`` (a: VectorClock) (b: VectorClock) =
+    match a.Compare(b) with
+    | VectorClockOrder.Before
+    | VectorClockOrder.Equal -> a.Merge(b) = b
+    | VectorClockOrder.After -> a.Merge(b) = a
+    | VectorClockOrder.Concurrent -> true
+    | _ -> true
+
+/// Property: Merge is monotone: merged clock is never before either input
+[<Property(Arbitrary = [| typeof<VectorClockArb> |])>]
+let ``Merge is monotone with respect to inputs`` (a: VectorClock) (b: VectorClock) =
+    let m = a.Merge(b)
+    let ra = m.Compare(a)
+    let rb = m.Compare(b)
+    (ra = VectorClockOrder.After || ra = VectorClockOrder.Equal)
+    && (rb = VectorClockOrder.After || rb = VectorClockOrder.Equal)
+
+/// Property: Increment only advances the chosen node; merging original with incremented equals incremented
+[<Property(Arbitrary = [| typeof<VectorClockArb> |])>]
+let ``Increment is stable under merge with original`` (clock: VectorClock) (nodeId: uint16) =
+    let inc = clock.Increment(nodeId)
+    clock.Merge(inc) = inc && inc.Merge(clock) = inc

From 7d8c4d3cc52973e32f0d1e4860f519309e8e07d7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 8 Feb 2026 13:35:16 +0000
Subject: [PATCH 2/2] Initial plan