diff --git a/src/Core/Core.fsproj b/src/Core/Core.fsproj index bbc5c96cf..d8f162688 100644 --- a/src/Core/Core.fsproj +++ b/src/Core/Core.fsproj @@ -46,6 +46,7 @@ + diff --git a/src/Core/Units.fs b/src/Core/Units.fs new file mode 100644 index 000000000..a74dd7b80 --- /dev/null +++ b/src/Core/Units.fs @@ -0,0 +1,182 @@ +namespace Zeta.Core + +/// Units of Measure for Zeta domain quantities. +/// +/// Pick units where confusion of like-shaped numbers is a real bug +/// class, not just "a number with a name." The four highest-pay +/// declarations: +/// +/// - Z-set semantic safety (weight / cardinality / delta) -- prevents +/// adding signed weights to unsigned counts on retraction +/// - Logical-vs-wall-clock time (tick / ms / ns / s) -- prevents +/// passing a duration where a tick count is expected (off-by-1000x +/// bugs that survive unit tests because both numbers look plausible) +/// - Bayesian probability vs percentage (prob / pct) -- prevents +/// 0.95-vs-95 confusion in Bayesian-output handlers +/// - Rate domain (per_tick / per_sec) -- defined as reciprocal of +/// tick / s respectively, so unit algebra cancels naturally +/// +/// UoM is erased at runtime (numeric-only, compile-time-only). The +/// safety is at the F# type-checker layer; runtime numeric ops are +/// identical to plain `int64` / `float`. This is additive: existing +/// code without UoM annotations stays untouched; consumers opt in by +/// annotating their own variables. +/// +/// Lineage: see the maintainer-forwarded Claude.ai conversation +/// preservation under `docs/research/` (knights-knaves-round-table- +/// harmonious-division-bootstrap-razor preservation, 2026-05-05) for +/// the original UoM-examples discussion + the "code tests the formal +/// verifications" framing. +module Units = + + // ============================================================================ + // Z-set semantic safety: signed weight, unsigned cardinality, signed delta. + // ============================================================================ + + /// Signed Z-set multiplicity. Negative weight means retraction. + /// Don't add weights to unsigned counts -- the type checker won't let you. + [] + type weight + + /// Count of distinct elements -- expected to be >= 0 by discipline, + /// not by UoM enforcement. UoM tags the *kind* (cardinality vs + /// weight); the underlying numeric type (typically `int` or `int64`) + /// is what carries signedness. A `cardinality`-tagged value being + /// non-negative is a contract callers maintain, not a property the + /// type system can prove. Combining with `weight` requires explicit + /// conversion at the call site (which is the point: you have to + /// think about retraction semantics). + [] + type cardinality + + /// Signed change between two states (`State_t - State_{t-1}`). Distinct + /// from `weight` because deltas compose differently than raw multiplicities. + [] + type delta + + + // ============================================================================ + // Time: logical ticks vs wall-clock milliseconds vs nanoseconds. + // ============================================================================ + + // `tick` and `ms` are NOT redeclared here -- they already exist as + // namespace-scope measures in `Window.fs:13-14`. This module compiles + // AFTER Window.fs so it sees those declarations and reuses them. The + // alternative (redeclaring inside Units) would create + // `Zeta.Core.Units.tick` distinct from `Zeta.Core.tick` -- non- + // interoperable, undermining the additive-safety goal. Reuse > redeclare. + + /// Wall-clock nanosecond. For high-precision deterministic- + /// simulation-testing (DST in the Otto-272 sense -- distinct from + /// daylight-saving-time) where `ms` is too coarse-grained to drive + /// deterministic scheduling. + [] + type ns + + + // ============================================================================ + // Bayesian: probability in [0,1] vs percentage in [0,100]. + // ============================================================================ + + /// Probability in [0, 1]. Bayesian inference outputs. + [] + type prob + + /// Percentage in [0, 100]. User-facing display only; not for + /// Bayesian computation. + [] + type pct + + + // ============================================================================ + // Rates: explicit per-time domain (DERIVED measures so the algebra cancels). + // ============================================================================ + + /// Wall-clock second. Base measure for per-second rates. + [] + type s + + /// Rate per logical tick (e.g. arrivals per circuit step). Defined as + /// reciprocal of `tick` so the algebra cancels: ` * ` + /// produces `<1>` (dimensionless) without unit-erasure casts. + [] + type per_tick = /tick + + /// Rate per wall-clock second. Defined as reciprocal of `s`. + [] + type per_sec = /s + + + // ============================================================================ + // Conversion helpers (explicit by design — conversion IS the safety boundary). + // ============================================================================ + + /// Convert probability (0..1) to percentage (0..100). Explicit so the + /// boundary between Bayesian-internal and user-facing is visible. + let probToPct (p: float) : float = + LanguagePrimitives.FloatWithMeasure (float p * 100.0) + + /// Convert percentage (0..100) back to probability (0..1). + let pctToProb (p: float) : float = + LanguagePrimitives.FloatWithMeasure (float p / 100.0) + + /// Convert ticks to wall-clock milliseconds given an explicit tick rate. + /// The `rate: float` parameter forces the caller to declare + /// the conversion factor at the call site (which is the point). + /// Validates `rate > 0` for symmetry with the wallToLogical* family. + let logicalToWall (rate: float) (t: int64) : float = + if float rate <= 0.0 then + invalidArg "rate" $"rate must be positive (got %f{float rate})" + LanguagePrimitives.FloatWithMeasure (float t) * rate + + /// Convert wall-clock milliseconds to ticks given an explicit tick rate. + /// **Rounding semantics**: truncates toward zero (`int64 (...)` cast). + /// Callers needing floor / ceiling / nearest semantics at tick boundaries + /// should compute the float result themselves and apply the rounding + /// they want. Truncation was chosen as the default because tick-time + /// is monotonically increasing in the scheduler and "ticks elapsed so + /// far" is the dominant query shape; truncation gives the conservative + /// answer. + let wallToLogical (rate: float) (d: float) : int64 = + if float rate <= 0.0 then + invalidArg "rate" $"rate must be positive (got %f{float rate})" + LanguagePrimitives.Int64WithMeasure (int64 (d / rate)) + + /// Same as `wallToLogical` but with explicit floor rounding (always + /// rounds toward negative infinity; matches truncation for non-negative + /// inputs but differs for negative durations). + let wallToLogicalFloor (rate: float) (d: float) : int64 = + if float rate <= 0.0 then + invalidArg "rate" $"rate must be positive (got %f{float rate})" + LanguagePrimitives.Int64WithMeasure (int64 (System.Math.Floor (float (d / rate)))) + + /// Same as `wallToLogical` but with explicit ceiling rounding (always + /// rounds toward positive infinity). + let wallToLogicalCeil (rate: float) (d: float) : int64 = + if float rate <= 0.0 then + invalidArg "rate" $"rate must be positive (got %f{float rate})" + LanguagePrimitives.Int64WithMeasure (int64 (System.Math.Ceiling (float (d / rate)))) + + /// Convert milliseconds to nanoseconds. Multiplies by 1_000_000; + /// `int64` overflows for `|d|` above roughly 9_223_372_036_854 ms + /// (~292 years). Guarded with `Checked.( * )` so overflow throws + /// `OverflowException` rather than silently wrapping. + let msToNs (d: int64) : int64 = + let raw = Checked.(*) (int64 d) 1000000L + LanguagePrimitives.Int64WithMeasure raw + + /// Apply a signed delta to a weight, producing a new weight. + /// Both arguments are signed; result is signed. The function exists + /// to make the semantic (state += delta) explicit at call sites. + /// Uses `Checked.(+)` so overflow throws `OverflowException` rather + /// than silently wrapping (e.g., `Int64.MaxValue + 1L`). + let applyDelta (state: int64) (d: int64) : int64 = + let raw = Checked.(+) (int64 state) (int64 d) + LanguagePrimitives.Int64WithMeasure raw + + /// Compute expected count over a window given a per-tick arrival rate. + /// The unit algebra cancels naturally: `per_tick = /tick`, so + /// ` * = <1>` (dimensionless, no cast needed). + let expectedArrivals (rate: float) (window: int64) : float = + let windowFloat = LanguagePrimitives.FloatWithMeasure (float window) + rate * windowFloat diff --git a/tests/Tests.FSharp/Algebra/Units.Tests.fs b/tests/Tests.FSharp/Algebra/Units.Tests.fs new file mode 100644 index 000000000..080ab38a1 --- /dev/null +++ b/tests/Tests.FSharp/Algebra/Units.Tests.fs @@ -0,0 +1,188 @@ +module Zeta.Tests.Algebra.UnitsTests + +open Xunit +open Zeta.Core +open Zeta.Core.Units + +// ============================================================================ +// Rounding semantics for wallToLogical / wallToLogicalFloor / wallToLogicalCeil. +// Pin the contract -- these are easy to silently change later, and the +// difference matters at tick boundaries. +// ============================================================================ + +[] +let ``wallToLogical truncates toward zero (positive duration)`` () = + let rate = 10.0 // 10 ms per tick + let d = 25.0 // 2.5 ticks worth + let result = wallToLogical rate d + Assert.Equal(2L, result) // truncated, not rounded + +[] +let ``wallToLogical truncates toward zero (negative duration)`` () = + let rate = 10.0 + let d = -25.0 // -2.5 ticks + let result = wallToLogical rate d + Assert.Equal(-2L, result) // truncates toward 0, not toward -inf + +[] +let ``wallToLogicalFloor rounds toward negative infinity`` () = + let rate = 10.0 + + // Positive: same as truncation + Assert.Equal(2L, wallToLogicalFloor rate 25.0) + + // Negative: differs from truncation -- rounds AWAY from zero + Assert.Equal(-3L, wallToLogicalFloor rate -25.0) + +[] +let ``wallToLogicalCeil rounds toward positive infinity`` () = + let rate = 10.0 + + // Positive: rounds AWAY from zero + Assert.Equal(3L, wallToLogicalCeil rate 25.0) + + // Negative: same as truncation (rounds toward 0) + Assert.Equal(-2L, wallToLogicalCeil rate -25.0) + +[] +let ``wallToLogical exact tick boundary returns exact tick count`` () = + let rate = 10.0 + let d = 30.0 // exactly 3 ticks + Assert.Equal(3L, wallToLogical rate d) + Assert.Equal(3L, wallToLogicalFloor rate d) + Assert.Equal(3L, wallToLogicalCeil rate d) + +[] +let ``wallToLogical rejects zero rate`` () = + let rate = 0.0 + let d = 25.0 + Assert.Throws(fun () -> wallToLogical rate d |> ignore) + |> ignore + +[] +let ``wallToLogical rejects negative rate`` () = + let rate = -1.0 + let d = 25.0 + Assert.Throws(fun () -> wallToLogical rate d |> ignore) + |> ignore + +[] +let ``wallToLogicalFloor rejects zero/negative rate`` () = + Assert.Throws(fun () -> + wallToLogicalFloor 0.0 25.0 |> ignore) + |> ignore + Assert.Throws(fun () -> + wallToLogicalFloor -1.0 25.0 |> ignore) + |> ignore + +[] +let ``wallToLogicalCeil rejects zero/negative rate`` () = + Assert.Throws(fun () -> + wallToLogicalCeil 0.0 25.0 |> ignore) + |> ignore + Assert.Throws(fun () -> + wallToLogicalCeil -1.0 25.0 |> ignore) + |> ignore + +// ============================================================================ +// Conversion round-trips: probToPct / pctToProb. +// ============================================================================ + +[] +let ``probToPct then pctToProb is identity (within float tolerance)`` () = + let original = 0.95 + let roundTrip = original |> probToPct |> pctToProb + Assert.Equal(float original, float roundTrip, 10) + +[] +let ``probToPct produces 100 for prob 1`` () = + Assert.Equal(100.0, probToPct 1.0) + +[] +let ``pctToProb produces 0 for pct 0`` () = + Assert.Equal(0.0, pctToProb 0.0) + +// ============================================================================ +// Algebra cancellation: per_tick * tick is dimensionless. +// ============================================================================ + +[] +let ``expectedArrivals algebra cancels per_tick * tick`` () = + let rate = 0.05 + let window = 100L + // 0.05 per tick * 100 ticks = 5.0 dimensionless + Assert.Equal(5.0, expectedArrivals rate window, 10) + +// ============================================================================ +// applyDelta: signed weight + signed delta produces signed weight. +// ============================================================================ + +[] +let ``applyDelta accumulates positive delta`` () = + let state = 10L + let d = 3L + Assert.Equal(13L, applyDelta state d) + +[] +let ``applyDelta accumulates negative delta (retraction)`` () = + let state = 10L + let d = -3L + Assert.Equal(7L, applyDelta state d) + +[] +let ``applyDelta below zero is allowed (signed weight)`` () = + let state = 1L + let d = -5L + Assert.Equal(-4L, applyDelta state d) + +// ============================================================================ +// msToNs overflow guard: input above ~9.22e12 ms throws OverflowException. +// ============================================================================ + +[] +let ``msToNs converts small values correctly`` () = + Assert.Equal(1_000_000L, msToNs 1L) + Assert.Equal(1_500_000_000L, msToNs 1500L) + +[] +let ``msToNs throws OverflowException on values that would overflow int64`` () = + let overflowing = 9_223_372_036_855L + Assert.Throws(fun () -> msToNs overflowing |> ignore) + |> ignore + +[] +let ``msToNs throws OverflowException on negative values that would overflow`` () = + let overflowing = -9_223_372_036_855L + Assert.Throws(fun () -> msToNs overflowing |> ignore) + |> ignore + +// ============================================================================ +// applyDelta overflow guard: Int64.MaxValue + positive delta throws. +// ============================================================================ + +[] +let ``applyDelta throws OverflowException on int64 overflow`` () = + let state = LanguagePrimitives.Int64WithMeasure System.Int64.MaxValue + let d = 1L + Assert.Throws(fun () -> applyDelta state d |> ignore) + |> ignore + +[] +let ``applyDelta throws OverflowException on int64 underflow`` () = + let state = LanguagePrimitives.Int64WithMeasure System.Int64.MinValue + let d = -1L + Assert.Throws(fun () -> applyDelta state d |> ignore) + |> ignore + +// ============================================================================ +// logicalToWall positive-rate guard. +// ============================================================================ + +[] +let ``logicalToWall rejects zero/negative rate`` () = + Assert.Throws(fun () -> + logicalToWall 0.0 100L |> ignore) + |> ignore + Assert.Throws(fun () -> + logicalToWall -1.0 100L |> ignore) + |> ignore diff --git a/tests/Tests.FSharp/Tests.FSharp.fsproj b/tests/Tests.FSharp/Tests.FSharp.fsproj index 9f0d47f17..4d197f22a 100644 --- a/tests/Tests.FSharp/Tests.FSharp.fsproj +++ b/tests/Tests.FSharp/Tests.FSharp.fsproj @@ -15,6 +15,7 @@ +