From 89e4796cfc8e6a6b0015379e9c8205ce362730d3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 15:44:23 +0000 Subject: [PATCH 1/4] WIP: STD_LEAK slice (NanosecondDuration decomposition): std must be perfectly --- dsl/test/claim/scale_probe_test.dag | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 dsl/test/claim/scale_probe_test.dag diff --git a/dsl/test/claim/scale_probe_test.dag b/dsl/test/claim/scale_probe_test.dag new file mode 100644 index 00000000000..23059aca6d7 --- /dev/null +++ b/dsl/test/claim/scale_probe_test.dag @@ -0,0 +1,25 @@ +module test.claim.scale_probe + +import std.types { Bool } +import std.nat { Nat, nat_max } +import std.measure { Measure, Time, Nano, Micro, measure_count } + +fn time_make(count: Nat) -> Measure { + Measure { count: count } +} + +fn time_seq(a: Measure, b: Measure) -> Measure { + time_make(count: measure_count(m: a) + measure_count(m: b)) +} + +fn time_par(a: Measure, b: Measure) -> Measure { + time_make(count: nat_max(a: measure_count(m: a), b: measure_count(m: b))) +} + +test fn scale_probe_witnesses() -> Bool { + let a: Measure = time_make(count: 3) + let b: Measure = time_make(count: 4) + let s = time_seq(a: a, b: b) + let p = time_par(a: a, b: b) + (measure_count(m: s) == 7) && (measure_count(m: p) == 4) +} From 1ff2cf0756a825449a8d40c859a1daf9281bce78 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 15:55:13 +0000 Subject: [PATCH 2/4] WIP: STD_LEAK slice (NanosecondDuration decomposition): std must be perfectly --- dsl/product/compute_fabric.dag | 11 +++- dsl/std/cache_interface.dag | 10 ++-- dsl/std/measure.dag | 26 ++++++++- dsl/std/realization.dag | 16 ++--- dsl/std/realization_measurement.dag | 91 ++++++++++++++++------------- dsl/std/realization_schedule.dag | 36 +++++++----- dsl/test/claim/scale_probe_test.dag | 25 -------- 7 files changed, 119 insertions(+), 96 deletions(-) delete mode 100644 dsl/test/claim/scale_probe_test.dag diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 0cbc35e623a..7a721c409ee 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -31,6 +31,7 @@ import std.measure { Currency, Micro, One, + Nano, ByteSize, MoneyAmount, NanosecondDuration, @@ -658,6 +659,12 @@ type MeasurementConfidence type PerformanceReceipt { provider: ProviderIdentity work_shape: WorkUnitId + // NANOSECOND scale CHOICE (relocated here per DESIGN §3): the realization / + // measurement framework (std.realization_measurement / std.realization_schedule) is + // scale-AGNOSTIC; this consumer — the host wall-clock observation boundary — OWNS the + // decision to denominate measured cost in nanoseconds, because that is the resolution + // the host clock observes elapsed wall time at. The framework rolls up whatever scale + // arrives; nanosecond is named here, once, where it is measured. wall_duration: NanosecondDuration cpu_seconds: Float? sample_count: Int @@ -678,7 +685,9 @@ fn performance_receipts_total_time(receipts: List) -> Nanose // Pure roll-up lens (std.realization_measurement): PerformanceReceipt observations // → CostAccount.time with Measured basis. Handler emits receipts; this folds them. -fn cost_account_from_performance_receipts(receipts: List) -> CostAccount { +// The scale-agnostic roll-up is instantiated at `CostAccount` HERE (this consumer's +// owned ns choice), inferred from the NanosecondDuration wall_duration. +fn cost_account_from_performance_receipts(receipts: List) -> CostAccount { cost_account_measured_from_time(time: performance_receipts_total_time(receipts: receipts)) } diff --git a/dsl/std/cache_interface.dag b/dsl/std/cache_interface.dag index ade9d2a6edf..db291f8bd00 100644 --- a/dsl/std/cache_interface.dag +++ b/dsl/std/cache_interface.dag @@ -9,7 +9,7 @@ module std.cache_interface import std.types { NonEmptyStr, ContentHash, Bool, Int, LogicalTime } -import std.measure { ByteSize, NanosecondDuration, nanosecond_duration, nanosecond_duration_count } +import std.measure { Nano, ByteSize, NanosecondDuration, nanosecond_duration, nanosecond_duration_count } import std.pareto { AxisComparison, DominanceVerdict, @@ -295,7 +295,7 @@ fn cache_reach_candidate_recompute() -> CacheReachCandidate { fn cache_reach_candidate_probe( id: CacheInterfaceId, catalog: List, - recompute: CostAccount, + recompute: CostAccount, ) -> CacheReachCandidate { let facts = cache_facts_for_id(id: id, catalog: catalog) let fetch = read_latency_cost(facts: facts) @@ -336,7 +336,7 @@ fn cache_reach_dominates(a: CacheReachCandidate, b: CacheReachCandidate) -> Domi fn cache_layer_cost_justified( id: CacheInterfaceId, catalog: List, - recompute: CostAccount, + recompute: CostAccount, ) -> Bool { nanosecond_duration_count(d: recompute.time) >= nanosecond_duration_count(d: read_latency_cost(facts: cache_facts_for_id(id: id, catalog: catalog))) } @@ -344,7 +344,7 @@ fn cache_layer_cost_justified( fn cache_layer_beats_recompute_path( id: CacheInterfaceId, catalog: List, - recompute: CostAccount, + recompute: CostAccount, ) -> Bool { let probe = cache_reach_candidate_probe(id: id, catalog: catalog, recompute: recompute) match cache_reach_dominates( @@ -377,7 +377,7 @@ fn cache_layer_plan_contains_id(plan: CacheLayerPlan, id: CacheInterfaceId) -> B fn plan_cache_layers( deployment: CacheDeploymentBackends, - recompute: CostAccount, + recompute: CostAccount, catalog: List, default_order: List, ) -> CacheLayerPlan { diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag index 4a1ae430721..40eb95c608f 100644 --- a/dsl/std/measure.dag +++ b/dsl/std/measure.dag @@ -237,6 +237,23 @@ fn measure_count(m: Measure) -> M { m.count } +// Generic time-measure constructor: a `Time` magnitude at ANY scale ``, magnitude +// fixed at the concrete `Nat` node. This is the scale-AGNOSTIC surface the realization / +// measurement framework (std.realization_measurement) builds its roll-up algebra on — +// it names no particular scale, so the framework carries no scale CHOICE (DESIGN §3: the +// agnostic shape stays central, the scale CHOICE sits peripheral at the consumer). A +// consumer pins `` (e.g. `Nano` for measured wall-clock) at its own boundary. +// +// `` is fixed at `Nat` here, NOT generic: a magnitude-generic roll-up would need `+`/ +// `max` over ``, and algebra-inhabitance resolves only on concrete numeric nodes — +// the same where-clause substrate gap `GroupCompletion` and the `Measure` +// constrained-inhabitance note above already carry. **Dissolution trigger:** when +// parametric where-clause syntax lands, widen to ` where M : CommutativeMonoid` and +// the roll-up algebra generalizes with it. +fn time_measure(count: Nat) -> Measure { + Measure { count: count } +} + // Memory magnitude at unit scale (Q-Unit composition; P2 single authority). type ByteSize = Measure @@ -255,8 +272,13 @@ type Hertz = Measure // Schedulable hardware thread count (std.cpu catalog/deployment authority). type HardwareThreadCount = Measure -// Time magnitude at nanosecond scale — realization `CostAccount.time` consumer -// (Q-Unit-5 minted-with-consumer; aligns with comment reserve for Duration/Milliseconds). +// Time magnitude at nanosecond scale — a neutral dimensional alias (parallel to `Hertz` +// / `Watt` / `ByteSize`), NOT a framework-level scale choice. The realization / +// measurement framework (std.realization_measurement, std.realization_schedule) is now +// scale-AGNOSTIC over `time_measure` and `Measure` / `CostAccount`; +// the CHOICE to denominate measured realization cost in nanoseconds + its reason live at +// the CONSUMER boundary that observes wall-clock (product.compute_fabric.PerformanceReceipt +// / `CostAccount` instantiation), not here and not in the framework (DESIGN §3). type NanosecondDuration = Measure fn nanosecond_duration(count: Nat) -> NanosecondDuration { diff --git a/dsl/std/realization.dag b/dsl/std/realization.dag index 6f680c03ef9..237ce792dcb 100644 --- a/dsl/std/realization.dag +++ b/dsl/std/realization.dag @@ -36,7 +36,7 @@ import std.realization_schedule { CostAccount, cost_account_measured, cost_account_predicted_zero, - cost_account_time_nanos, + cost_account_time_count, schedule_lens_verdict_for_ci_floor, schedule_generates_same_batch_count, schedule_generates_identical_schedule, @@ -51,7 +51,7 @@ import std.realization_measurement { cost_account_measured_from_schedule_critical_path, schedule_critical_path_time, schedule_batch_critical_path, - nanosecond_duration_list_total, + time_measure_list_total, } // --- Independence classifier (fail-closed) ------------------------------------ @@ -103,16 +103,18 @@ type Placement = LocalInProcess | LocalFilesystem | RemoteNetwork type Materialization = Recompute | Memoize | Share -type RealizedStep { +// `` is the consumer-pinned time scale of the carried cost ledger (CostAccount); +// reconcile never inspects the scale — it only threads it (DESIGN §3: framework agnostic). +type RealizedStep { shape: EffectShape placement: Placement materialization: Materialization - cost: CostAccount + cost: CostAccount } // Mark every accumulator step whose effect is the same-KeySource create-if-absent // twin of `s` as Share (s collapses INTO the shared materialization; not appended). -fn mark_collapsible_share(acc: List, s: RealizedStep) -> List { +fn mark_collapsible_share(acc: List>, s: RealizedStep) -> List> { acc |> map(e => if create_double_init_collapsible(a: e.shape, b: s.shape) { RealizedStep { @@ -128,7 +130,7 @@ fn mark_collapsible_share(acc: List, s: RealizedStep) -> List, s: RealizedStep) -> Bool { +fn has_collapsible_peer(acc: List>, s: RealizedStep) -> Bool { let peers = acc |> filter(e => create_double_init_collapsible(a: e.shape, b: s.shape)) !((peers |> length) == 0) } @@ -138,7 +140,7 @@ fn has_collapsible_peer(acc: List, s: RealizedStep) -> Bool { // materialization is Share; distinct identities (or non-create effects) stay separate. // The collapse decision is create_double_init_collapsible (std.effects, KeySource-keyed) — // reconcile only consumes it, never re-derives KeySource equality (§3 single authority). -fn reconcile(steps: List) -> List { +fn reconcile(steps: List>) -> List> { steps |> fold(init: [], f: (acc, s) => if has_collapsible_peer(acc: acc, s: s) { mark_collapsible_share(acc: acc, s: s) diff --git a/dsl/std/realization_measurement.dag b/dsl/std/realization_measurement.dag index 25fcb7b99d2..cb739193cc0 100644 --- a/dsl/std/realization_measurement.dag +++ b/dsl/std/realization_measurement.dag @@ -13,19 +13,19 @@ module std.realization_measurement import std.types { ContentHash, Bool, String, List } -import std.nat { Nat } +import std.nat { Nat, nat_max } import std.measure { - NanosecondDuration, - nanosecond_duration, - nanosecond_duration_count, - nanosecond_duration_max, + Measure, + Time, + time_measure, + measure_count, } import std.realization_schedule { CostAccount, CostBasis, cost_account_measured, cost_account_predicted_zero, - cost_account_time_nanos, + cost_account_time_count, } // Host-effect shape: observe elapsed wall time at a cache-subject boundary. @@ -38,14 +38,20 @@ type RealizationMeasureEffect } // --- Pure roll-up lens: observations → CostAccount.time -------------------- +// +// Scale-AGNOSTIC over ``: the algebra below is pure add / max over a `Time` magnitude +// at ANY scale (DESIGN §3 — the framework carries no scale CHOICE). A consumer pins `` +// (e.g. `Nano`) at its own boundary; nothing here names a particular scale. `` is fixed +// at `Nat` (magnitude-genericity needs `+`/`max` over ``, the documented where-clause +// substrate gap — see `std.measure.time_measure`). -fn cost_account_measured_from_time(time: NanosecondDuration) -> CostAccount { +fn cost_account_measured_from_time(time: Measure) -> CostAccount { cost_account_measured(time: time) } -fn nanosecond_duration_list_total(times: List) -> NanosecondDuration { - nanosecond_duration( - count: fold(times, init: 0, f: (acc, t) => acc + nanosecond_duration_count(d: t)) +fn time_measure_list_total(times: List>) -> Measure { + time_measure( + count: fold(times, init: 0, f: (acc, t) => acc + measure_count(m: t)) ) } @@ -56,78 +62,81 @@ fn nanosecond_duration_list_total(times: List) -> Nanosecond // CostMax) at complexity.dag:3754-3771. Do NOT fork a second span semantics here; // these are the concrete NanosecondDuration realizations of that proof vocabulary. -fn nanosecond_duration_is_zero(d: NanosecondDuration) -> Bool { - nanosecond_duration_count(d: d) == 0 +fn time_measure_is_zero(d: Measure) -> Bool { + measure_count(m: d) == 0 } -fn nanosecond_duration_seq(a: NanosecondDuration, b: NanosecondDuration) -> NanosecondDuration { - if nanosecond_duration_is_zero(d: a) { +fn time_measure_seq(a: Measure, b: Measure) -> Measure { + if time_measure_is_zero(d: a) { b - } else if nanosecond_duration_is_zero(d: b) { + } else if time_measure_is_zero(d: b) { a } else { - nanosecond_duration( - count: nanosecond_duration_count(d: a) + nanosecond_duration_count(d: b) + time_measure( + count: measure_count(m: a) + measure_count(m: b) ) } } -fn nanosecond_duration_par(a: NanosecondDuration, b: NanosecondDuration) -> NanosecondDuration { - if nanosecond_duration_is_zero(d: a) { +fn time_measure_par(a: Measure, b: Measure) -> Measure { + if time_measure_is_zero(d: a) { b - } else if nanosecond_duration_is_zero(d: b) { + } else if time_measure_is_zero(d: b) { a } else { - nanosecond_duration_max(a: a, b: b) + time_measure( + count: nat_max(a: measure_count(m: a), b: measure_count(m: b)) + ) } } -fn nanosecond_duration_list_par(times: List) -> NanosecondDuration { +fn time_measure_list_par(times: List>) -> Measure { fold( times, - init: nanosecond_duration(count: 0), - f: (acc, t) => nanosecond_duration_par(a: acc, b: t) + init: time_measure(count: 0), + f: (acc, t) => time_measure_par(a: acc, b: t) ) } // One schedule batch (parallel runnables) → max wall time; zero identity matches cost_par. -fn schedule_batch_critical_path(batch_times: List) -> NanosecondDuration { - nanosecond_duration_list_par(times: batch_times) +fn schedule_batch_critical_path(batch_times: List>) -> Measure { + time_measure_list_par(times: batch_times) } // Schedule topology `List>`: sequential across batches, parallel within batch. -fn schedule_critical_path_time(batch_times: List>) -> NanosecondDuration { +fn schedule_critical_path_time(batch_times: List>>) -> Measure { fold( batch_times, - init: nanosecond_duration(count: 0), - f: (acc, batch) => nanosecond_duration_seq( + init: time_measure(count: 0), + f: (acc, batch) => time_measure_seq( a: acc, b: schedule_batch_critical_path(batch_times: batch) ) ) } -fn cost_account_measured_from_schedule_critical_path( - batch_times: List> -) -> CostAccount { +fn cost_account_measured_from_schedule_critical_path( + batch_times: List>> +) -> CostAccount { cost_account_measured_from_time(time: schedule_critical_path_time(batch_times: batch_times)) } -fn cost_account_measured_from_time_list(times: List) -> CostAccount { - cost_account_measured_from_time(time: nanosecond_duration_list_total(times: times)) +fn cost_account_measured_from_time_list(times: List>) -> CostAccount { + cost_account_measured_from_time(time: time_measure_list_total(times: times)) } // Discriminating lens: non-zero measured roll-up must differ from predicted_zero -// and preserve nanosecond count (§5 — goes red if roll-up aliases or drops time). -fn witness_measured_rollup_differs_from_predicted_zero(wall_time: NanosecondDuration) -> Bool { - if nanosecond_duration_count(d: wall_time) == 0 { +// and preserve the magnitude count (§5 — goes red if roll-up aliases or drops time). +// Scale-agnostic: holds at whatever scale `` the consumer supplies. +fn witness_measured_rollup_differs_from_predicted_zero(wall_time: Measure) -> Bool { + if measure_count(m: wall_time) == 0 { false } else { - let measured_nanos = cost_account_time_nanos( + let measured_count = cost_account_time_count( account: cost_account_measured_from_time(time: wall_time) ) - let predicted_nanos = cost_account_time_nanos(account: cost_account_predicted_zero()) - measured_nanos != predicted_nanos - && measured_nanos == nanosecond_duration_count(d: wall_time) + let predicted_count = cost_account_time_count(account: cost_account_predicted_zero()) + measured_count != predicted_count + && measured_count == measure_count(m: wall_time) } } diff --git a/dsl/std/realization_schedule.dag b/dsl/std/realization_schedule.dag index 49d0791b58c..749d6ea35ad 100644 --- a/dsl/std/realization_schedule.dag +++ b/dsl/std/realization_schedule.dag @@ -10,8 +10,8 @@ module std.realization_schedule import std.types { ContentHash, Bool, String, List, Int } import std.nat { Nat } import std.measure { - ByteSize, Watt, NanosecondDuration, - byte_size, watt, nanosecond_duration + Measure, Time, ByteSize, Watt, + byte_size, watt, time_measure, measure_count } import std.pareto { AxisGoal } import std.lens_verdict { @@ -28,23 +28,27 @@ type CostBasis = Predicted | Measured -type CostAccount { - time: NanosecondDuration +// Scale-AGNOSTIC cost ledger: `time` is a `Time` magnitude at ANY scale `` (DESIGN §3 +// — the framework names no scale; a consumer pins ``, e.g. `CostAccount` for +// measured wall-clock, at its own boundary). `space`/`power` keep their own dimensional +// scales (`Memory@One` / `Power@One`); only the time axis is the relocated scale choice. +type CostAccount { + time: Measure space: ByteSize power: Watt basis: CostBasis } -fn cost_account_predicted_zero() -> CostAccount { +fn cost_account_predicted_zero() -> CostAccount { CostAccount { - time: nanosecond_duration(count: 0) + time: time_measure(count: 0) space: byte_size(count: 0) power: watt(count: 0) basis: Predicted } } -fn cost_account_measured(time: NanosecondDuration) -> CostAccount { +fn cost_account_measured(time: Measure) -> CostAccount { CostAccount { time: time space: byte_size(count: 0) @@ -53,8 +57,9 @@ fn cost_account_measured(time: NanosecondDuration) -> CostAccount { } } -fn cost_account_time_nanos(account: CostAccount) -> Nat { - nanosecond_duration_count(d: account.time) +// Magnitude projection at the ledger's declared scale (count, not scale-named "nanos"). +fn cost_account_time_count(account: CostAccount) -> Nat { + measure_count(m: account.time) } type RealizationObjective { @@ -76,14 +81,15 @@ type Runnable type Schedule = List> -type RealizationPlan { +type RealizationPlan { target: ContentHash objective: RealizationObjective schedule: Schedule // Measured roll-up along schedule critical path (seq across batches, max within batch); // authority v1.compiler.complexity span / cost_seq / cost_par — see - // std.realization_measurement.schedule_critical_path_time. - total: CostAccount + // std.realization_measurement.schedule_critical_path_time. `` is the consumer-pinned + // time scale of the ledger (e.g. `RealizationPlan`); the plan itself is agnostic. + total: CostAccount } fn runnable_step_label(r: Runnable) -> String { @@ -127,7 +133,7 @@ fn schedule_lens_violation_diagnostic( } } -fn schedule_lens_verdict_for_ci_floor(plan: RealizationPlan, compile_gate_fn: String) -> LensVerdict { +fn schedule_lens_verdict_for_ci_floor(plan: RealizationPlan, compile_gate_fn: String) -> LensVerdict { if plan.schedule.length() == 0 { Violation { diagnostic: schedule_lens_violation_diagnostic( @@ -181,7 +187,7 @@ fn schedule_lens_verdict_for_ci_floor(plan: RealizationPlan, compile_gate_fn: St } } -fn schedule_generates_same_batch_count(left: RealizationPlan, right: RealizationPlan) -> Bool { +fn schedule_generates_same_batch_count(left: RealizationPlan, right: RealizationPlan) -> Bool { left.schedule.length() == right.schedule.length() } @@ -253,6 +259,6 @@ fn schedule_eq(left: Schedule, right: Schedule) -> Bool { } } -fn schedule_generates_identical_schedule(plan: RealizationPlan, schedule: Schedule) -> Bool { +fn schedule_generates_identical_schedule(plan: RealizationPlan, schedule: Schedule) -> Bool { schedule_eq(left: plan.schedule, right: schedule) } diff --git a/dsl/test/claim/scale_probe_test.dag b/dsl/test/claim/scale_probe_test.dag deleted file mode 100644 index 23059aca6d7..00000000000 --- a/dsl/test/claim/scale_probe_test.dag +++ /dev/null @@ -1,25 +0,0 @@ -module test.claim.scale_probe - -import std.types { Bool } -import std.nat { Nat, nat_max } -import std.measure { Measure, Time, Nano, Micro, measure_count } - -fn time_make(count: Nat) -> Measure { - Measure { count: count } -} - -fn time_seq(a: Measure, b: Measure) -> Measure { - time_make(count: measure_count(m: a) + measure_count(m: b)) -} - -fn time_par(a: Measure, b: Measure) -> Measure { - time_make(count: nat_max(a: measure_count(m: a), b: measure_count(m: b))) -} - -test fn scale_probe_witnesses() -> Bool { - let a: Measure = time_make(count: 3) - let b: Measure = time_make(count: 4) - let s = time_seq(a: a, b: b) - let p = time_par(a: a, b: b) - (measure_count(m: s) == 7) && (measure_count(m: p) == 4) -} From c62e25e2f6a665cf85648c12e75a86f841404c7f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 16:00:38 +0000 Subject: [PATCH 3/4] STD_LEAK: scale-agnostic realization framework + relocate ns choice to verification Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/test_node_wall_clock_ratchet.dag | 2 +- dsl/product/compute_fabric.dag | 5 +- dsl/std/cache_interface.dag | 5 +- dsl/std/measure.dag | 52 +++------------- dsl/std/realization_measurement.dag | 3 +- dsl/std/verification.dag | 32 +++++++++- dsl/test/claim/cache_layer_planner_test.dag | 2 +- .../realization_measurement_keystone_test.dag | 6 +- .../claim/realization_scale_agnostic_test.dag | 62 +++++++++++++++++++ ...ealization_schedule_critical_path_test.dag | 10 +-- 10 files changed, 118 insertions(+), 61 deletions(-) create mode 100644 dsl/test/claim/realization_scale_agnostic_test.dag diff --git a/dsl/gunbc/test_node_wall_clock_ratchet.dag b/dsl/gunbc/test_node_wall_clock_ratchet.dag index dce0a5e38f4..fb8e36a0213 100644 --- a/dsl/gunbc/test_node_wall_clock_ratchet.dag +++ b/dsl/gunbc/test_node_wall_clock_ratchet.dag @@ -8,7 +8,7 @@ // the retired hand-only manifest). Single edit surface: add/remove rows here. // // Phase-0 convergence: `TestNodeCostDimension.budget_time` / `measured_time` use -// `NanosecondDuration` (std.measure); this table names libtest tokens until every +// `NanosecondDuration` (std.verification, its timing-authority home); this table names libtest tokens until every // slow test is either sped up or modeled with explicit budget/measured facts. module gunbc.test_node_wall_clock_ratchet diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 7a721c409ee..e6f0b26b982 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -34,9 +34,6 @@ import std.measure { Nano, ByteSize, MoneyAmount, - NanosecondDuration, - nanosecond_duration, - nanosecond_duration_count, HardwareThreadCount, byte_size, byte_size_count, @@ -45,6 +42,8 @@ import std.measure { hertz, } import std.currency { CurrencyCode } +// Nanosecond timing CHOICE from its single authority (std.verification), not std.measure. +import std.verification { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } import std.realization_schedule { CostAccount } import std.realization_measurement { cost_account_measured_from_time } import std.content_hash { diff --git a/dsl/std/cache_interface.dag b/dsl/std/cache_interface.dag index db291f8bd00..6444bdcd44e 100644 --- a/dsl/std/cache_interface.dag +++ b/dsl/std/cache_interface.dag @@ -9,7 +9,10 @@ module std.cache_interface import std.types { NonEmptyStr, ContentHash, Bool, Int, LogicalTime } -import std.measure { Nano, ByteSize, NanosecondDuration, nanosecond_duration, nanosecond_duration_count } +import std.measure { Nano, ByteSize } +// NanosecondDuration scale CHOICE imported from its timing-authority home (std.verification, +// DESIGN §3), not re-coined here: cache read-latency costs are the consumer's nanosecond facts. +import std.verification { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } import std.pareto { AxisComparison, DominanceVerdict, diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag index 40eb95c608f..bcce4fc5962 100644 --- a/dsl/std/measure.dag +++ b/dsl/std/measure.dag @@ -51,9 +51,8 @@ module std.measure -import std.nat { Nat, nat_compare, nat_max, nat_min } +import std.nat { Nat } import std.types { Int } -import std.algebra { Ordering } // --- Quantity: what is being measured ------------------------------------- // @@ -272,47 +271,14 @@ type Hertz = Measure // Schedulable hardware thread count (std.cpu catalog/deployment authority). type HardwareThreadCount = Measure -// Time magnitude at nanosecond scale — a neutral dimensional alias (parallel to `Hertz` -// / `Watt` / `ByteSize`), NOT a framework-level scale choice. The realization / -// measurement framework (std.realization_measurement, std.realization_schedule) is now -// scale-AGNOSTIC over `time_measure` and `Measure` / `CostAccount`; -// the CHOICE to denominate measured realization cost in nanoseconds + its reason live at -// the CONSUMER boundary that observes wall-clock (product.compute_fabric.PerformanceReceipt -// / `CostAccount` instantiation), not here and not in the framework (DESIGN §3). -type NanosecondDuration = Measure - -fn nanosecond_duration(count: Nat) -> NanosecondDuration { - NanosecondDuration { count: count } -} - -fn nanosecond_duration_count(d: NanosecondDuration) -> Nat { - d.count -} - -fn nanosecond_duration_compare(a: NanosecondDuration, b: NanosecondDuration) -> Ordering { - nat_compare( - a: nanosecond_duration_count(d: a), - b: nanosecond_duration_count(d: b) - ) -} - -fn nanosecond_duration_max(a: NanosecondDuration, b: NanosecondDuration) -> NanosecondDuration { - nanosecond_duration( - count: nat_max( - a: nanosecond_duration_count(d: a), - b: nanosecond_duration_count(d: b) - ) - ) -} - -fn nanosecond_duration_min(a: NanosecondDuration, b: NanosecondDuration) -> NanosecondDuration { - nanosecond_duration( - count: nat_min( - a: nanosecond_duration_count(d: a), - b: nanosecond_duration_count(d: b) - ) - ) -} +// NOTE: the scale-FIXED nanosecond time alias `NanosecondDuration = Measure` is deliberately NOT defined here. A scale-fixed alias is a CHOICE, not generic +// dimensional vocabulary — it is parallel to `Milliwatt` (`Measure`, +// homed at its product consumer in #5235), not to the base SI units `Watt` / `Hertz` +// that stay below. std.measure keeps only the generic `Measure` carrier + +// `time_measure`; the nanosecond CHOICE + its reason live at the timing-authority +// CONSUMER (std.verification), per DESIGN §3 (the agnostic shape stays central; the +// scale that selects a realization sits peripheral). // Power magnitude at unit scale — the plain watt (SI derived: W = J/s). The dimension // TDP specs, PSU ratings, and live draw are all quoted in. A power rating carries the diff --git a/dsl/std/realization_measurement.dag b/dsl/std/realization_measurement.dag index cb739193cc0..8204bc971db 100644 --- a/dsl/std/realization_measurement.dag +++ b/dsl/std/realization_measurement.dag @@ -60,7 +60,8 @@ fn time_measure_list_total(times: List>) -> Measure` realizations of that +// proof vocabulary (a consumer pins ``, e.g. `Nano`; the algebra names no scale). fn time_measure_is_zero(d: Measure) -> Bool { measure_count(m: d) == 0 diff --git a/dsl/std/verification.dag b/dsl/std/verification.dag index 21900689e1a..007d77d1bc2 100644 --- a/dsl/std/verification.dag +++ b/dsl/std/verification.dag @@ -22,7 +22,33 @@ module std.verification import std.nat { Nat } -import std.measure { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } +import std.measure { Measure, Time, Nano, measure_count } + +// --- Timing authority: the NANOSECOND scale CHOICE ------------------------- +// +// std.verification is the single timing-authority CONSUMER (Phase-0 convergence, +// header below). The scale-FIXED nanosecond time alias is homed HERE, not in the +// generic std.measure carrier and not in the scale-AGNOSTIC realization framework +// (std.realization_measurement / std.realization_schedule operate over `Measure` / `CostAccount` and name no scale). The nanosecond decision EMERGES at +// this consumer because the timing authority is verification's: budget/measured facts +// are nanosecond thresholds (DESIGN §3 — the scale that selects a realization sits +// peripheral, never in the agnostic shape). Parallel to `Milliwatt` homed at its +// product consumer (#5235), not to base SI units `Watt`/`Hertz` that stay in measure. +// Other consumers (std.cache_interface, product.compute_fabric) import this alias FROM +// here, the single authority — never re-coining the Nano choice. +// +// `` is fixed at `Nat`; magnitude-genericity is the documented where-clause substrate +// gap (see std.measure.time_measure). +type NanosecondDuration = Measure + +fn nanosecond_duration(count: Nat) -> NanosecondDuration { + NanosecondDuration { count: count } +} + +fn nanosecond_duration_count(d: NanosecondDuration) -> Nat { + measure_count(m: d) +} // The predicate form of an assertion. // Each variant corresponds to a standard verification predicate @@ -53,8 +79,8 @@ type TestClaim { // warn-name list. **Follow-on:** attach explicit `TimingBudget` / `TimingMeasurement` // rows per test where paydown replaces warn-only policy. // -// Phase-0 convergence: `NanosecondDuration` (std.measure) is the timing authority; -// budget/measured facts are nanosecond thresholds, not parallel Milliseconds fields. +// Phase-0 convergence: `NanosecondDuration` (homed in this module, above) is the timing +// authority; budget/measured facts are nanosecond thresholds, not parallel Milliseconds. // A named test case — a conjunction of claims. // All claims must hold for the test to pass. diff --git a/dsl/test/claim/cache_layer_planner_test.dag b/dsl/test/claim/cache_layer_planner_test.dag index bf7612e2192..29ba0e63a78 100644 --- a/dsl/test/claim/cache_layer_planner_test.dag +++ b/dsl/test/claim/cache_layer_planner_test.dag @@ -7,7 +7,7 @@ module test.claim.cache_layer_planner import std.types { Bool } -import std.measure { nanosecond_duration } +import std.verification { nanosecond_duration } import std.realization_schedule { CostAccount, cost_account_measured } import std.cache_interface { CacheDeploymentBackends, diff --git a/dsl/test/claim/realization_measurement_keystone_test.dag b/dsl/test/claim/realization_measurement_keystone_test.dag index 8ea4285b21c..9254fd6ae40 100644 --- a/dsl/test/claim/realization_measurement_keystone_test.dag +++ b/dsl/test/claim/realization_measurement_keystone_test.dag @@ -12,7 +12,7 @@ import std.realization_schedule { CostAccount, CostBasis, cost_account_predicted_zero, - cost_account_time_nanos, + cost_account_time_count, } import std.realization_measurement { RealizationMeasureEffect, @@ -25,7 +25,7 @@ import product.compute_fabric { cost_account_from_performance_receipts, performance_receipts_total_time, } -import std.measure { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } +import std.verification { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } data sample_subject: ContentHash = "witness-subject-realization-measurement-keystone" data sample_work_shape: WorkUnitId = "witness:realization_measurement_keystone" @@ -49,7 +49,7 @@ fn witness_measured_receipt_rollup_uses_lens() -> Bool { wall_time: sample_wall_time, ) let total = cost_account_from_performance_receipts(receipts: [receipt]) - let rolled = cost_account_time_nanos(account: total) + let rolled = cost_account_time_count(account: total) let observed = nanosecond_duration_count( d: performance_receipts_total_time(receipts: [receipt]) ) diff --git a/dsl/test/claim/realization_scale_agnostic_test.dag b/dsl/test/claim/realization_scale_agnostic_test.dag new file mode 100644 index 00000000000..d95b5631131 --- /dev/null +++ b/dsl/test/claim/realization_scale_agnostic_test.dag @@ -0,0 +1,62 @@ +// dsl/test/claim/realization_scale_agnostic_test.dag +// +// §5 discriminating witness: the realization measurement framework +// (std.realization_measurement / std.realization_schedule) is scale-AGNOSTIC. It is +// exercised here at the MILLI scale — a scale the framework never names. If any roll-up +// fn or CostAccount field had stayed hardcoded to NanosecondDuration (Measure), +// these Milli-scale instantiations would fail to resolve / type-check. Green here means +// the scale CHOICE genuinely lives at the consumer, not in the framework. +// +// Run: gunbc run --source-root dsl --entry --function realization_scale_agnostic_witnesses --claim-run + +module test.claim.realization_scale_agnostic + +import std.types { Bool, List } +import std.nat { Nat } +import std.measure { Measure, Time, Milli, time_measure, measure_count } +import std.realization_schedule { CostAccount, cost_account_time_count } +import std.realization_measurement { + time_measure_seq, + time_measure_par, + schedule_critical_path_time, + cost_account_measured_from_schedule_critical_path, + witness_measured_rollup_differs_from_predicted_zero, +} + +// Consumer-pinned scale anchor: MILLI (NOT nanosecond). Proves the framework names no scale. +fn milli(count: Nat) -> Measure { + time_measure(count: count) +} + +// seq = add, par = max — at Milli scale. +fn witness_milli_seq_and_par() -> Bool { + let a = milli(count: 30) + let b = milli(count: 12) + (measure_count(m: time_measure_seq(a: a, b: b)) == 42) + && (measure_count(m: time_measure_par(a: a, b: b)) == 30) +} + +// critical path (seq across batches, max within batch) at Milli scale: max(10,40) + max(5) = 45. +fn witness_milli_critical_path() -> Bool { + let batches = [[milli(count: 10), milli(count: 40)], [milli(count: 5)]] + measure_count(m: schedule_critical_path_time(batch_times: batches)) == 45 +} + +// CostAccount bridges through the roll-up; ledger preserves the Milli count. +fn witness_milli_cost_account() -> Bool { + let batches = [[milli(count: 7)], [milli(count: 8)]] + let account = cost_account_measured_from_schedule_critical_path(batch_times: batches) + cost_account_time_count(account: account) == 15 +} + +// The discriminating roll-up lens holds at Milli too (scale-parametric witness). +fn witness_milli_rollup_discriminates() -> Bool { + witness_measured_rollup_differs_from_predicted_zero(wall_time: milli(count: 99)) +} + +test fn realization_scale_agnostic_witnesses() -> Bool { + witness_milli_seq_and_par() + && witness_milli_critical_path() + && witness_milli_cost_account() + && witness_milli_rollup_discriminates() +} diff --git a/dsl/test/claim/realization_schedule_critical_path_test.dag b/dsl/test/claim/realization_schedule_critical_path_test.dag index d65503a11d6..5e1e70bbd81 100644 --- a/dsl/test/claim/realization_schedule_critical_path_test.dag +++ b/dsl/test/claim/realization_schedule_critical_path_test.dag @@ -8,14 +8,14 @@ module test.claim.realization_schedule_critical_path -import std.measure { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } +import std.verification { NanosecondDuration, nanosecond_duration, nanosecond_duration_count } import std.realization_measurement { schedule_batch_critical_path, schedule_critical_path_time, cost_account_measured_from_schedule_critical_path, - nanosecond_duration_list_total, + time_measure_list_total, } -import std.realization_schedule { CostBasis, cost_account_time_nanos } +import std.realization_schedule { CostBasis, cost_account_time_count } import std.nat { nat_compare, nat_max } import std.algebra { Greater, Equal } @@ -25,7 +25,7 @@ fn witness_parallel_batch_takes_max_not_sum() -> Bool { nanosecond_duration(count: 5), ] let critical = schedule_batch_critical_path(batch_times: batch) - let summed = nanosecond_duration_list_total(times: batch) + let summed = time_measure_list_total(times: batch) nanosecond_duration_count(d: critical) == 100 && nanosecond_duration_count(d: summed) == 105 && nanosecond_duration_count(d: critical) != nanosecond_duration_count(d: summed) @@ -52,7 +52,7 @@ fn witness_measured_total_uses_critical_path_basis() -> Bool { let account = cost_account_measured_from_schedule_critical_path(batch_times: batches) match account.basis { Measured => - cost_account_time_nanos(account: account) == 200 + cost_account_time_count(account: account) == 200 Predicted => false } } From f5ca18b8f8077e1b015bf6c77af62a5d91b9ce0c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 16:14:10 +0000 Subject: [PATCH 4/4] =?UTF-8?q?=C2=A75=20honesty:=20reword=20scale-agnosti?= =?UTF-8?q?c=20witness=20=E2=80=94=20=20is=20phantom/erased,=20claim=20?= =?UTF-8?q?only=20the=20arithmetic=20teeth?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The witness header claimed Milli-scale instantiations would fail to resolve/type-check if a roll-up fn stayed Nano-hardcoded. Execution-falsified by parent (smart-eagle-107): the scale tag is a phantom type the substrate erases — re-hardcoding to Measure leaves the witness green with 0 dag-compile diagnostics (same no-where-clause substrate gap already cited for ). Reworded to assert only what bites (roll-up arithmetic composes off-Nano; perturbing it goes red) and to name the genuine guard as structural (a no-concrete-scale-literal lens), a documented follow-up. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../claim/realization_scale_agnostic_test.dag | 22 ++++++++++++++----- 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/dsl/test/claim/realization_scale_agnostic_test.dag b/dsl/test/claim/realization_scale_agnostic_test.dag index d95b5631131..2e085193c32 100644 --- a/dsl/test/claim/realization_scale_agnostic_test.dag +++ b/dsl/test/claim/realization_scale_agnostic_test.dag @@ -1,11 +1,21 @@ // dsl/test/claim/realization_scale_agnostic_test.dag // -// §5 discriminating witness: the realization measurement framework -// (std.realization_measurement / std.realization_schedule) is scale-AGNOSTIC. It is -// exercised here at the MILLI scale — a scale the framework never names. If any roll-up -// fn or CostAccount field had stayed hardcoded to NanosecondDuration (Measure), -// these Milli-scale instantiations would fail to resolve / type-check. Green here means -// the scale CHOICE genuinely lives at the consumer, not in the framework. +// §5 witness: the realization measurement framework (std.realization_measurement / +// std.realization_schedule) is exercised at the MILLI scale — a scale the framework +// never names — and its roll-up ARITHMETIC composes correctly there (seq = add, par = +// max, critical-path = seq-of-batch-max, and the CostAccount bridge preserves the +// count). That is what these witnesses actually bite on: perturbing the arithmetic (e.g. +// dropping an addend in time_measure_seq) turns them FALSE. +// +// HONEST SCOPE (what this does NOT prove): scale-agnosticism is NOT enforced by execution +// or type-checking. The `` scale tag is a PHANTOM type the substrate erases — neither +// the interpreter nor the dag compiler checks it (re-hardcoding a roll-up fn to +// Measure leaves these Milli witnesses GREEN and emits 0 diagnostics). +// This is the same no-where-clause / constrained-inhabitance substrate gap already cited +// for `` (std.measure.time_measure). So no runtime witness can carry anti-regression +// teeth for the scale-agnosticism claim. The genuine guard is STRUCTURAL — a lens +// asserting the framework modules contain no concrete scale literal — tracked as the +// honest follow-up, not delivered here. // // Run: gunbc run --source-root dsl --entry --function realization_scale_agnostic_witnesses --claim-run