Add high-value property tests for HLC and vector clocks

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

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