Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions dsl/std/compute_fabric.dag
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,8 @@ type CostClass = OwnedMarginalZero | PerSecondBilled | Metered | DeveloperAttent
// Lens: tiered-access cost — owned marginal vs metered vs attention-priced axes.
type OomSignalClass = KillProcess | Throttle | ReportOnly

type Bandwidth = Measure<DataRate, One>
type Duration = Measure<Time, One>
type Bandwidth = Measure<DataRate, One, Nat>
type Duration = Measure<Time, One, Nat>
type ProviderIdentity = NonEmptyStr where brand("ProviderIdentity")

type ComputeArtifactLocality
Expand Down
73 changes: 52 additions & 21 deletions dsl/std/measure.dag
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,17 @@ type Quantity =
| Frequency
| Count
| Currency
// Electrical dimensions (Q-Unit-5 inhabitant: std.spice R/L/C passive map/fold,
// gunbc#4895/#4913). These five are consumed by EVERY form of the passive fold
// (v and i are always derived), so they are form-independent. ElectricCharge +
// MagneticFlux are pre-approved (carrier authority) to land WITH the fold that
// reads them (#4913 Form B: Q+=i*dt → v=Q/C; Φ+=v*dt → i=Φ/L) — minted with their
// inhabitant per Q-Unit-5, not speculatively here.
| ElectricPotential
| ElectricCurrent
| Resistance
| Capacitance
| Inductance

// --- Scale: SI decimal scale exponent -------------------------------------
//
Expand Down Expand Up @@ -139,8 +150,10 @@ fn scale_exponent(s: Scale) -> Int {
//
// PRACTICE 4 CHECKPOINT: 🟢 PRIMITIVE
// Parametric dimensional carrier: phantom `<Q>` / `<S>` tag semantics;
// `count` holds magnitude at the declared scale. Widening adds Quantity /
// Scale values, not new Measure variants.
// non-phantom `<M>` carries the magnitude type (see the MAGNITUDE
// GENERALIZATION note at the type decl below). `count` holds the magnitude
// at the declared scale. Widening adds Quantity / Scale values (or a new `<M>`
// instantiation), not new Measure variants.
// Per-target representation (Rust `std::time::Duration`, Python
// `datetime.timedelta`, Go `time.Duration`, etc.) is Grounding's job
// per Q-Unit-4 RATIFIED.
Expand Down Expand Up @@ -171,16 +184,33 @@ fn scale_exponent(s: Scale) -> Int {
// - No `Refined<Measure<…>, predicate>` at this layer per option (c).
// - No mechanical Measure-witness derivation declared here -- same
// substrate gap as `GroupCompletion<M>`; inhabitance lens follow-up.
// - v2 claim-run: phantom type-arg resolution (G1) and single-hop alias
// field access (G2) now resolve on the v2 interpreter; parametric record
// literals (G3) and multi-hop alias field-access chains remain gated.
// Consumers use the constructor/projection fns below until G3 lands.
type Measure<Q, S> {
count: Nat
// - v2 claim-run: phantom type-arg resolution (G1), single-hop alias field
// access (G2), parametric record literals (G3), and multi-hop alias
// field-access chains all now resolve on the v2 interpreter (G3 + multi-hop
// landed in gunbc#4885, alias-chain peel / fail-closed). The carrier
// witnesses in dsl/test/claim/measure_magnitude_carrier.dag exercise each
// path by execution; the constructor/projection fns below remain the
// ergonomic surface, no longer a pre-flip workaround.
// MAGNITUDE GENERALIZATION (`<M>`): the `count` field now carries its magnitude at
// type `<M>` rather than a hardwired `Nat`. `<M>` ranges over the std numeric tower
// (`Nat` / `Int` / `Rational` / `Real`) so a single carrier spans the magnitude
// migration frame: GATE0 (non-negative integer magnitudes) instantiates `<M> = Nat`
// (every existing alias below); GATE1 (signed or fractional magnitudes — e.g. SPICE
// electrical potentials/currents, which are signed) instantiates `<M> = Int` (or
// `Rational`/`Real` for fractional consumers, a later consumer-specific rung). `<M>`
// is a NON-phantom parameter: unlike `<Q>`/`<S>` it appears in the `count` field. The
// param-dependent field through the alias chains below (`ByteSize.count : Nat`,
// `Measure<ElectricPotential, Micro, Int>.count : Int`) resolves + evaluates on the v2
// interpreter today (verified by execution post-#4885 G3 + multi-hop): M=Nat via the
// single-hop alias projection, signed M=Int via a direct record literal, and a two-hop
// alias chain (`MoneyMicros.count`) all round-trip — each backed by an enrolled witness
// in dsl/test/claim/measure_magnitude_carrier.dag.
type Measure<Q, S, M> {
count: M
}

// Memory magnitude at unit scale (Q-Unit composition; P2 single authority).
type ByteSize = Measure<Memory, One>
type ByteSize = Measure<Memory, One, Nat>

// PRACTICE 4 CHECKPOINT: 🟢 PRIMITIVE (parametric alias of the 🟢 `Measure`
// carrier; Information's FIRST inhabitant — sets precedent: Information = digital
Expand All @@ -189,13 +219,13 @@ type ByteSize = Measure<Memory, One>
// consumer needing Memory <-> Information (byte <-> bit x8). x8 is non-decimal so
// it will NOT be an SI Scale; lands as a separate sub-unit authority (same pattern
// as currency ISO minor-unit at lines 205-209). Dissolve-on: first consumer.
type BitWidth = Measure<Information, One>
type BitWidth = Measure<Information, One, Nat>

// Dimensional alias for sustained per-thread clock rate (SI hertz).
type Hertz = Measure<Frequency, One>
type Hertz = Measure<Frequency, One, Nat>

// Schedulable hardware thread count (std.cpu catalog/deployment authority).
type HardwareThreadCount = Measure<Count, One>
type HardwareThreadCount = Measure<Count, One, Nat>

// --- MoneyAmount<S>: price magnitude carrier ------------------------------
//
Expand All @@ -221,11 +251,12 @@ type HardwareThreadCount = Measure<Count, One>
// e.g. `std.compute_fabric.CostEstimate { unit_price, currency }`.
//
// `MoneyAmount` is a MULTI-HOP alias (MoneyMicros = MoneyAmount<Micro> =
// Measure<Currency, Micro>); its phantom type args resolve on v2 (G1 landed),
// but reading its `.count` is the multi-hop alias field-access case that the
// single-hop G2 does not yet cover -- the money VALUE on v2 lands with the G3
// follow-up. `std.currency` (a plain enum) evaluates on v2 today.
type MoneyAmount<S> = Measure<Currency, S>
// Measure<Currency, Micro, Nat>); reading its `.count` is the multi-hop alias
// field-access case, which now resolves + evaluates on v2 (G3 + multi-hop landed
// in gunbc#4885, alias-chain peel) -- verified by execution, see
// measure_two_hop_alias_count_roundtrip_holds. `std.currency` (a plain enum)
// evaluates on v2 today.
type MoneyAmount<S> = Measure<Currency, S, Nat>

// Micro-denominated money (storage scale = `Micro`, 10^-6 major units).
// Demanded by Hetzner cost quotes, whose source data is `*_eur_micros`
Expand All @@ -237,10 +268,10 @@ fn money_micros(count: Nat) -> MoneyMicros {
MoneyMicros { count: count }
}

// 🟡 consumer:G3-multi-hop-alias-field-access — bind gunbc#4885 (G3 flip lane).
// Inline `Measure<Currency, Micro>` dodges v2 multi-hop `.count` on `MoneyMicros` pre-flip.
// Dissolve-on: #4885 merge — repoint param to `MoneyMicros`; coordinate with snappy-stag-903.
fn money_micros_count(m: Measure<Currency, Micro>) -> Nat {
// Dissolved gunbc#4885 (G3 + multi-hop alias field-access landed, alias-chain peel):
// the param is the `MoneyMicros` alias directly; v2 resolves the two-hop `.count`
// (verified by execution — see measure_two_hop_alias_count_roundtrip_holds).
fn money_micros_count(m: MoneyMicros) -> Nat {
m.count
}

Expand Down
49 changes: 49 additions & 0 deletions dsl/test/claim/measure_magnitude_carrier.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
// Carrier witnesses for the Measure<Q, S, M> magnitude generalization (GATE0 Nat +
// GATE1 signed Int). Proves by execution that the 3-param carrier round-trips its
// param-dependent `count` field for BOTH magnitude rungs — through the single-hop
// alias projection (ByteSize), a direct record literal (signed electrical Int), and
// a two-hop alias chain (MoneyMicros -> MoneyAmount<Micro> -> Measure) — and that a
// signed electrical magnitude (negative count) is representable, the whole reason the
// magnitude axis was generalized off the hardwired `Nat`.
module test.claim.measure_magnitude_carrier

import std.measure {
Measure,
ByteSize,
byte_size,
byte_size_count,
ElectricPotential,
Micro,
money_micros,
money_micros_count
}
import std.types { Int }
import std.logic { Bool }

// GATE0 — M=Nat through the ByteSize alias (Measure<Memory, One, Nat>).
fn measure_nat_magnitude_roundtrip_holds() -> Bool {
byte_size_count(byte_size(42)) == 42
}

// GATE1 — M=Int (signed) over an electrical Quantity. Microvolts are signed:
// a negative potential must round-trip through the param-dependent count field.
fn signed_microvolts(n: Int) -> Measure<ElectricPotential, Micro, Int> {
Measure { count: n }
}

fn signed_microvolts_count(v: Measure<ElectricPotential, Micro, Int>) -> Int {
v.count
}

fn measure_signed_magnitude_roundtrip_holds() -> Bool {
signed_microvolts_count(signed_microvolts(-5)) == -5
}

// Two-hop alias chain — the `<M>`-carrying `count` field read multi-hop through
// MoneyMicros (= MoneyAmount<Micro> = Measure<Currency, Micro, Nat>). Substantiates
// the "two-hop alias chains round-trip" claim in measure.dag (G3 + multi-hop landed
// gunbc#4885): both `money_micros` (multi-hop record literal) and `money_micros_count`
// (multi-hop `.count`) resolve + evaluate on the v2 interpreter.
fn measure_two_hop_alias_count_roundtrip_holds() -> Bool {
money_micros_count(money_micros(99)) == 99
}
38 changes: 34 additions & 4 deletions src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag
Original file line number Diff line number Diff line change
Expand Up @@ -315,6 +315,30 @@ data corpus_ci_gate_row_probe_selector_cf_import_resolves: ClaimWitnessCorpusCla
expected: ExpectPass
}

// Measure<Q,S,M> magnitude-carrier witnesses (dsl-rooted, shard b) — the CI consumer
// that breaks on regression of the magnitude generalization (gunbc#4929): GATE0 M=Nat,
// GATE1 signed M=Int, and the two-hop alias-chain `.count` round-trip (G3 + multi-hop).
data corpus_ci_gate_row_measure_nat_magnitude_roundtrip: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
label: "measure carrier M=Nat magnitude round-trip",
entry: "dsl/test/claim/measure_magnitude_carrier.dag",
function: "measure_nat_magnitude_roundtrip_holds",
expected: ExpectPass
}

data corpus_ci_gate_row_measure_signed_magnitude_roundtrip: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
label: "measure carrier signed M=Int magnitude round-trip",
entry: "dsl/test/claim/measure_magnitude_carrier.dag",
function: "measure_signed_magnitude_roundtrip_holds",
expected: ExpectPass
}

data corpus_ci_gate_row_measure_two_hop_alias_count_roundtrip: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
label: "measure carrier two-hop alias .count round-trip",
entry: "dsl/test/claim/measure_magnitude_carrier.dag",
function: "measure_two_hop_alias_count_roundtrip_holds",
expected: ExpectPass
}

data claim_witness_corpus_claim_run_rows: List<ClaimWitnessCorpusClaimRunRow> = [
corpus_ci_gate_row_mvp1_emit_matches_serialize,
corpus_ci_gate_row_mvp1_emit_ingest_round_trip,
Expand Down Expand Up @@ -353,10 +377,13 @@ data claim_witness_corpus_claim_run_rows: List<ClaimWitnessCorpusClaimRunRow> =
corpus_ci_gate_row_effect_io_eval_roundtrip,
corpus_ci_gate_row_effect_io_eval_unbound_fail_closed,
corpus_ci_gate_row_dsl_root_probe,
corpus_ci_gate_row_probe_selector_cf_import_resolves
corpus_ci_gate_row_probe_selector_cf_import_resolves,
corpus_ci_gate_row_measure_nat_magnitude_roundtrip,
corpus_ci_gate_row_measure_signed_magnitude_roundtrip,
corpus_ci_gate_row_measure_two_hop_alias_count_roundtrip
]

data claim_witness_corpus_claim_run_row_count: String = "38"
data claim_witness_corpus_claim_run_row_count: String = "41"

// Sharded enrollment: two parallel CI jobs (~12–13 rows each). Wave A partition rows
// co-locate with COMPREP emit shard-a (shared entry fixture cost); closure witnesses on shard-b.
Expand Down Expand Up @@ -403,7 +430,10 @@ data claim_witness_corpus_shard_b_rows: List<ClaimWitnessCorpusClaimRunRow> = [
corpus_ci_gate_row_effect_io_eval_roundtrip,
corpus_ci_gate_row_effect_io_eval_unbound_fail_closed,
corpus_ci_gate_row_dsl_root_probe,
corpus_ci_gate_row_probe_selector_cf_import_resolves
corpus_ci_gate_row_probe_selector_cf_import_resolves,
corpus_ci_gate_row_measure_nat_magnitude_roundtrip,
corpus_ci_gate_row_measure_signed_magnitude_roundtrip,
corpus_ci_gate_row_measure_two_hop_alias_count_roundtrip
]

data claim_witness_corpus_shard_b_row_count: String = "20"
data claim_witness_corpus_shard_b_row_count: String = "23"
Loading