Skip to content
Closed
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
15 changes: 4 additions & 11 deletions dsl/examples/cost_estimate/cost_estimate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,10 @@
// resolution yet. #4831 (in flight) lands it as an explicit `std.option`
// module (`Option = Absent | Present{value}`) and repoints those
// consumers to `import std.option { Option }`.
// - The real `CostEstimate.unit_price: MoneyMicros` is a `Measure<Currency,
// Micro>` value; Measure VALUE eval on v2 is blocked by G1 (identifier-
// variant type args, #4826) -- the same gap that blocks `ByteSize`/`Hertz`
// eval. So a money-carrier value cannot yet be constructed/read on v1.
//
// ⟹ INTERIM PROOF. This witness is NOT a permanent substitute for the real
// claim-run. **Real target:** a v2 claim-run over
// `product.compute_fabric.hetzner_cax41_cost_quote` (a `CostEstimate` with a
// `MoneyMicros` price), which lands once #4831 (Option-in-v2) AND #4826
// (G1 identifier-variant type args) clear. Wire this witness out / fold it
// into that real claim-run on arrival.
// - The real `CostEstimate.unit_price: MoneyMicros` consumer is now proven by
// `test.claim.hetzner_cost_quote_witness` (extdeps Hetzner CAX41 catalog row
// → `product.compute_fabric.per_second_billed_cost_quote`). This Float witness
// remains as the genuinely-real-valued fields exercise until folded.
//
// NOTE: money is fixed-point (`MoneyMicros` = `Measure<Currency, Micro>`),
// NEVER `Float` -- floating point for money is a representation defect
Expand Down
14 changes: 8 additions & 6 deletions dsl/extdeps/cloud/hetzner.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,20 +9,22 @@
module extdeps.cloud.hetzner

import std.cpu.types { CpuArchitecture }
import std.measure { MoneyMicros, money_micros }
import std.types { Int, NonEmptyStr }

type HetznerCloudServerType = Cax11 | Cax21 | Cax31 | Cax41

type HetznerCloudServerCatalogRow {
server_type: HetznerCloudServerType
// P-CF-BYTESIZE: shared raw-Int stopgap (operator_fleet + Hetzner) — NOT a parallel
// representation. Dissolves when Measure value-typing lands (ByteSize, currency, thread
// count); converts BOTH operator_fleet and Hetzner catalog rows.
// representation. Dissolves when Measure value-typing lands (ByteSize, thread count);
// converts BOTH operator_fleet and Hetzner catalog rows. Money fields migrated to
// `MoneyMicros` (Measure<Currency, Micro>) — the Hetzner source quotes micro-EUR.
vcpus: Int
memory_bytes: Int
disk_bytes: Int
hourly_eur_micros: Int
monthly_cap_eur_micros: Int
hourly_eur: MoneyMicros
monthly_cap_eur: MoneyMicros
pricing_citation: NonEmptyStr
cpu_architecture: CpuArchitecture
}
Expand All @@ -34,8 +36,8 @@ data cax41_catalog: HetznerCloudServerCatalogRow = HetznerCloudServerCatalogRow
vcpus: 16,
memory_bytes: 34359738368,
disk_bytes: 343597383680,
hourly_eur_micros: 50500,
monthly_cap_eur_micros: 31490000,
hourly_eur: money_micros(count: 50500),
monthly_cap_eur: money_micros(count: 31490000),
pricing_citation: "docs.hetzner.com/general/infrastructure-and-availability/price-adjustment/ GE-D9256 CAX41 Germany/Finland €0.0505/hr €31.49/mo ex-VAT effective 2026-04-01",
cpu_architecture: Aarch64,
}
21 changes: 21 additions & 0 deletions dsl/product/compute_fabric.dag
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ import std.measure {
One,
ByteSize,
MoneyMicros,
money_micros_count,
NanosecondDuration,
nanosecond_duration,
nanosecond_duration_count,
Expand Down Expand Up @@ -269,6 +270,26 @@ type AvailabilityWindow { open: LogicalTime, close: LogicalTime? }
// `NonEmptyStr`.
type CostEstimate { model: CostModel, unit_price: MoneyMicros, currency: CurrencyCode }

// Per-second billed cloud quote — the product-side $/billing axis consumer for a
// vendor hourly rate carried as `MoneyMicros` (Measure<Currency, Micro>). The vendor
// catalog (extdeps.cloud.hetzner) owns the cited micro-EUR rows; this function is
// vendor-agnostic — it projects any hourly `MoneyMicros` + ISO currency into the
// `CostEstimate` shape the placement/isolation lattice reads via `ComputeOffer.cost_quote`.
fn per_second_billed_cost_quote(unit_price: MoneyMicros, currency: CurrencyCode) -> CostEstimate {
CostEstimate {
model: CostModel {
cost_class: PerSecondBilled,
rates: ProviderCostModel { placeholder: true },
},
unit_price: unit_price,
currency: currency,
}
}

fn cost_estimate_unit_price_micros(quote: CostEstimate) -> Nat {
money_micros_count(m: quote.unit_price)
}

type ComputeOffer {
provider: ProviderIdentity
supply: ComputeSupplyFacts
Expand Down
55 changes: 55 additions & 0 deletions dsl/test/claim/hetzner_cost_quote_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
// test/claim/hetzner_cost_quote_witness_test.dag — by-execution witness for the
// MoneyMicros product consumer on the $/billing axis (DESIGN §5).
//
// Proves the extdeps Hetzner catalog row (cited micro-EUR hourly rate) projects
// through product.compute_fabric.per_second_billed_cost_quote into a `CostEstimate`
// whose fixed-point unit price round-trips the catalog magnitude — the real target
// named in examples/cost_estimate/cost_estimate.dag (replacing the interim Float witness).
//
// Run:
// gunbc run --source-root dsl --entry dsl/test/claim/hetzner_cost_quote_witness_test.dag \
// --function hetzner_cost_quote_witness_holds --claim-run

module test.claim.hetzner_cost_quote_witness

import std.logic { Bool }
import std.nat { Nat }
import std.currency { Eur }
import extdeps.cloud.hetzner { cax41_catalog }
import product.compute_fabric {
per_second_billed_cost_quote,
cost_estimate_unit_price_micros,
PerSecondBilled,
}

fn hetzner_cax41_hourly_micros() -> Nat {
cost_estimate_unit_price_micros(
quote: per_second_billed_cost_quote(
unit_price: cax41_catalog.hourly_eur,
currency: Eur,
),
)
}

fn hetzner_cax41_cost_class_is_per_second_billed() -> Bool {
let quote = per_second_billed_cost_quote(
unit_price: cax41_catalog.hourly_eur,
currency: Eur,
)
match quote.model.cost_class {
PerSecondBilled => true
OwnedMarginalZero => false
Metered => false
DeveloperAttention => false
}
}

// CAX41 Germany/Finland 2026-04-01: €0.0505/hr = 50500 micro-EUR (extdeps cited row).
fn hetzner_cax41_unit_price_matches_catalog() -> Bool {
hetzner_cax41_hourly_micros() == 50500
}

test fn hetzner_cost_quote_witness_holds() -> Bool {
hetzner_cax41_cost_class_is_per_second_billed()
&& hetzner_cax41_unit_price_matches_catalog()
}
6 changes: 3 additions & 3 deletions src/v2/lens/unit_modeling.dag
Original file line number Diff line number Diff line change
Expand Up @@ -114,9 +114,9 @@ data unit_field_rows: List<UnitFieldRow> = [
UnitFieldRow { field: ^ram_cap_bytes, carrier: ^ByteSize },
UnitFieldRow { field: ^memory_bytes, carrier: ^ByteSize },
UnitFieldRow { field: ^disk_bytes, carrier: ^ByteSize },
// Currency (MoneyMicros = MoneyAmount<Micro>, measure.dag:225)
UnitFieldRow { field: ^hourly_eur_micros, carrier: ^MoneyMicros },
UnitFieldRow { field: ^monthly_cap_eur_micros, carrier: ^MoneyMicros },
// Currency (MoneyMicros = MoneyAmount<Micro>, measure.dag:225) — hourly_eur /
// monthly_cap_eur migrated on extdeps.cloud.hetzner; rows for the old bare-Int
// field names dissolved.
// Time. Carrier is compute_fabric.Duration = Measure<Time, One>
// (compute_fabric.dag:76) — NOT the legacy types.dag:321 `Duration = Int`
// brand. That brand is itself a violator of the scale+quantity-conflated
Expand Down
Loading