-
Notifications
You must be signed in to change notification settings - Fork 1
feat(core/units): F# UoM declarations for Zeta domain (Aaron 2026-05-05) #1590
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
AceHack
merged 7 commits into
main
from
feat/core-units-uom-zeta-bug-class-prevention-aaron-2026-05-05
May 5, 2026
Merged
Changes from all commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
08a7faf
feat(core/units): F# UoM declarations for Zeta domain (weight/cardina…
AceHack 43b964f
fix(core/units): per_tick/per_sec as derived measures + role-ref disc…
AceHack 745ff3d
fix(core/units): clarify DST acronym + document wallToLogical truncat…
AceHack 406e19b
fix(core/units): reuse existing namespace-scope tick/ms from Window.f…
AceHack e0885cb
fix(core/units): zero-rate guard + cardinality unsignedness clarifica…
AceHack ae549e2
fix(core/units): msToNs overflow guard + 3 overflow tests (#1590 revi…
AceHack 3c98c42
fix(core/units): applyDelta+logicalToWall checked/guarded + 3 new tes…
AceHack File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. | ||
| [<Measure>] | ||
| 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). | ||
| [<Measure>] | ||
| type cardinality | ||
|
|
||
| /// Signed change between two states (`State_t - State_{t-1}`). Distinct | ||
| /// from `weight` because deltas compose differently than raw multiplicities. | ||
| [<Measure>] | ||
| 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. | ||
| [<Measure>] | ||
| type ns | ||
|
|
||
|
|
||
| // ============================================================================ | ||
| // Bayesian: probability in [0,1] vs percentage in [0,100]. | ||
| // ============================================================================ | ||
|
|
||
| /// Probability in [0, 1]. Bayesian inference outputs. | ||
| [<Measure>] | ||
| type prob | ||
|
|
||
| /// Percentage in [0, 100]. User-facing display only; not for | ||
| /// Bayesian computation. | ||
| [<Measure>] | ||
| type pct | ||
|
|
||
|
|
||
| // ============================================================================ | ||
| // Rates: explicit per-time domain (DERIVED measures so the algebra cancels). | ||
| // ============================================================================ | ||
|
|
||
| /// Wall-clock second. Base measure for per-second rates. | ||
| [<Measure>] | ||
| type s | ||
|
|
||
| /// Rate per logical tick (e.g. arrivals per circuit step). Defined as | ||
| /// reciprocal of `tick` so the algebra cancels: `<per_tick> * <tick>` | ||
| /// produces `<1>` (dimensionless) without unit-erasure casts. | ||
| [<Measure>] | ||
| type per_tick = /tick | ||
|
|
||
| /// Rate per wall-clock second. Defined as reciprocal of `s`. | ||
| [<Measure>] | ||
| 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<prob>) : float<pct> = | ||
| LanguagePrimitives.FloatWithMeasure<pct> (float p * 100.0) | ||
|
|
||
| /// Convert percentage (0..100) back to probability (0..1). | ||
| let pctToProb (p: float<pct>) : float<prob> = | ||
| LanguagePrimitives.FloatWithMeasure<prob> (float p / 100.0) | ||
|
|
||
| /// Convert ticks to wall-clock milliseconds given an explicit tick rate. | ||
| /// The `rate: float<ms/tick>` 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<ms/tick>) (t: int64<tick>) : float<ms> = | ||
| if float rate <= 0.0 then | ||
| invalidArg "rate" $"rate must be positive (got %f{float rate})" | ||
| LanguagePrimitives.FloatWithMeasure<tick> (float t) * rate | ||
|
AceHack marked this conversation as resolved.
|
||
|
|
||
| /// 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<ms/tick>) (d: float<ms>) : int64<tick> = | ||
| if float rate <= 0.0 then | ||
| invalidArg "rate" $"rate must be positive (got %f{float rate})" | ||
| LanguagePrimitives.Int64WithMeasure<tick> (int64 (d / rate)) | ||
|
AceHack marked this conversation as resolved.
AceHack marked this conversation as resolved.
AceHack marked this conversation as resolved.
|
||
|
|
||
| /// 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<ms/tick>) (d: float<ms>) : int64<tick> = | ||
| if float rate <= 0.0 then | ||
| invalidArg "rate" $"rate must be positive (got %f{float rate})" | ||
| LanguagePrimitives.Int64WithMeasure<tick> (int64 (System.Math.Floor (float (d / rate)))) | ||
|
|
||
| /// Same as `wallToLogical` but with explicit ceiling rounding (always | ||
| /// rounds toward positive infinity). | ||
| let wallToLogicalCeil (rate: float<ms/tick>) (d: float<ms>) : int64<tick> = | ||
| if float rate <= 0.0 then | ||
| invalidArg "rate" $"rate must be positive (got %f{float rate})" | ||
| LanguagePrimitives.Int64WithMeasure<tick> (int64 (System.Math.Ceiling (float (d / rate)))) | ||
|
AceHack marked this conversation as resolved.
|
||
|
|
||
| /// 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. | ||
|
AceHack marked this conversation as resolved.
|
||
| let msToNs (d: int64<ms>) : int64<ns> = | ||
| let raw = Checked.(*) (int64 d) 1000000L | ||
| LanguagePrimitives.Int64WithMeasure<ns> 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<delta>`). | ||
| let applyDelta (state: int64<weight>) (d: int64<delta>) : int64<weight> = | ||
| let raw = Checked.(+) (int64 state) (int64 d) | ||
| LanguagePrimitives.Int64WithMeasure<weight> raw | ||
|
|
||
| /// Compute expected count over a window given a per-tick arrival rate. | ||
| /// The unit algebra cancels naturally: `per_tick = /tick`, so | ||
| /// `<per_tick> * <tick> = <1>` (dimensionless, no cast needed). | ||
| let expectedArrivals (rate: float<per_tick>) (window: int64<tick>) : float = | ||
| let windowFloat = LanguagePrimitives.FloatWithMeasure<tick> (float window) | ||
|
AceHack marked this conversation as resolved.
|
||
| rate * windowFloat | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogical truncates toward zero (positive duration)`` () = | ||
| let rate = 10.0<ms/tick> // 10 ms per tick | ||
| let d = 25.0<ms> // 2.5 ticks worth | ||
| let result = wallToLogical rate d | ||
| Assert.Equal(2L<tick>, result) // truncated, not rounded | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogical truncates toward zero (negative duration)`` () = | ||
| let rate = 10.0<ms/tick> | ||
| let d = -25.0<ms> // -2.5 ticks | ||
| let result = wallToLogical rate d | ||
| Assert.Equal(-2L<tick>, result) // truncates toward 0, not toward -inf | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogicalFloor rounds toward negative infinity`` () = | ||
| let rate = 10.0<ms/tick> | ||
|
|
||
| // Positive: same as truncation | ||
| Assert.Equal(2L<tick>, wallToLogicalFloor rate 25.0<ms>) | ||
|
|
||
| // Negative: differs from truncation -- rounds AWAY from zero | ||
| Assert.Equal(-3L<tick>, wallToLogicalFloor rate -25.0<ms>) | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogicalCeil rounds toward positive infinity`` () = | ||
| let rate = 10.0<ms/tick> | ||
|
|
||
| // Positive: rounds AWAY from zero | ||
| Assert.Equal(3L<tick>, wallToLogicalCeil rate 25.0<ms>) | ||
|
|
||
| // Negative: same as truncation (rounds toward 0) | ||
| Assert.Equal(-2L<tick>, wallToLogicalCeil rate -25.0<ms>) | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogical exact tick boundary returns exact tick count`` () = | ||
| let rate = 10.0<ms/tick> | ||
| let d = 30.0<ms> // exactly 3 ticks | ||
| Assert.Equal(3L<tick>, wallToLogical rate d) | ||
| Assert.Equal(3L<tick>, wallToLogicalFloor rate d) | ||
| Assert.Equal(3L<tick>, wallToLogicalCeil rate d) | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogical rejects zero rate`` () = | ||
| let rate = 0.0<ms/tick> | ||
| let d = 25.0<ms> | ||
| Assert.Throws<System.ArgumentException>(fun () -> wallToLogical rate d |> ignore) | ||
| |> ignore | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogical rejects negative rate`` () = | ||
| let rate = -1.0<ms/tick> | ||
| let d = 25.0<ms> | ||
| Assert.Throws<System.ArgumentException>(fun () -> wallToLogical rate d |> ignore) | ||
| |> ignore | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogicalFloor rejects zero/negative rate`` () = | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| wallToLogicalFloor 0.0<ms/tick> 25.0<ms> |> ignore) | ||
| |> ignore | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| wallToLogicalFloor -1.0<ms/tick> 25.0<ms> |> ignore) | ||
| |> ignore | ||
|
|
||
| [<Fact>] | ||
| let ``wallToLogicalCeil rejects zero/negative rate`` () = | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| wallToLogicalCeil 0.0<ms/tick> 25.0<ms> |> ignore) | ||
| |> ignore | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| wallToLogicalCeil -1.0<ms/tick> 25.0<ms> |> ignore) | ||
| |> ignore | ||
|
|
||
| // ============================================================================ | ||
| // Conversion round-trips: probToPct / pctToProb. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``probToPct then pctToProb is identity (within float tolerance)`` () = | ||
| let original = 0.95<prob> | ||
| let roundTrip = original |> probToPct |> pctToProb | ||
| Assert.Equal(float original, float roundTrip, 10) | ||
|
|
||
| [<Fact>] | ||
| let ``probToPct produces 100 for prob 1`` () = | ||
| Assert.Equal(100.0<pct>, probToPct 1.0<prob>) | ||
|
|
||
| [<Fact>] | ||
| let ``pctToProb produces 0 for pct 0`` () = | ||
| Assert.Equal(0.0<prob>, pctToProb 0.0<pct>) | ||
|
|
||
| // ============================================================================ | ||
| // Algebra cancellation: per_tick * tick is dimensionless. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``expectedArrivals algebra cancels per_tick * tick`` () = | ||
| let rate = 0.05<per_tick> | ||
| let window = 100L<tick> | ||
| // 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. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``applyDelta accumulates positive delta`` () = | ||
| let state = 10L<weight> | ||
| let d = 3L<delta> | ||
| Assert.Equal(13L<weight>, applyDelta state d) | ||
|
|
||
| [<Fact>] | ||
| let ``applyDelta accumulates negative delta (retraction)`` () = | ||
| let state = 10L<weight> | ||
| let d = -3L<delta> | ||
| Assert.Equal(7L<weight>, applyDelta state d) | ||
|
|
||
| [<Fact>] | ||
| let ``applyDelta below zero is allowed (signed weight)`` () = | ||
| let state = 1L<weight> | ||
| let d = -5L<delta> | ||
| Assert.Equal(-4L<weight>, applyDelta state d) | ||
|
|
||
| // ============================================================================ | ||
| // msToNs overflow guard: input above ~9.22e12 ms throws OverflowException. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``msToNs converts small values correctly`` () = | ||
| Assert.Equal(1_000_000L<ns>, msToNs 1L<ms>) | ||
| Assert.Equal(1_500_000_000L<ns>, msToNs 1500L<ms>) | ||
|
|
||
| [<Fact>] | ||
| let ``msToNs throws OverflowException on values that would overflow int64`` () = | ||
| let overflowing = 9_223_372_036_855L<ms> | ||
| Assert.Throws<System.OverflowException>(fun () -> msToNs overflowing |> ignore) | ||
| |> ignore | ||
|
|
||
| [<Fact>] | ||
| let ``msToNs throws OverflowException on negative values that would overflow`` () = | ||
| let overflowing = -9_223_372_036_855L<ms> | ||
| Assert.Throws<System.OverflowException>(fun () -> msToNs overflowing |> ignore) | ||
| |> ignore | ||
|
|
||
| // ============================================================================ | ||
| // applyDelta overflow guard: Int64.MaxValue + positive delta throws. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``applyDelta throws OverflowException on int64 overflow`` () = | ||
| let state = LanguagePrimitives.Int64WithMeasure<weight> System.Int64.MaxValue | ||
| let d = 1L<delta> | ||
| Assert.Throws<System.OverflowException>(fun () -> applyDelta state d |> ignore) | ||
| |> ignore | ||
|
|
||
| [<Fact>] | ||
| let ``applyDelta throws OverflowException on int64 underflow`` () = | ||
| let state = LanguagePrimitives.Int64WithMeasure<weight> System.Int64.MinValue | ||
| let d = -1L<delta> | ||
| Assert.Throws<System.OverflowException>(fun () -> applyDelta state d |> ignore) | ||
| |> ignore | ||
|
|
||
| // ============================================================================ | ||
| // logicalToWall positive-rate guard. | ||
| // ============================================================================ | ||
|
|
||
| [<Fact>] | ||
| let ``logicalToWall rejects zero/negative rate`` () = | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| logicalToWall 0.0<ms/tick> 100L<tick> |> ignore) | ||
| |> ignore | ||
| Assert.Throws<System.ArgumentException>(fun () -> | ||
| logicalToWall -1.0<ms/tick> 100L<tick> |> ignore) | ||
| |> ignore |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.