Skip to content
Closed
9 changes: 7 additions & 2 deletions dsl/extdeps/rust/cargo.dag
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

module extdeps.cargo

import extdeps.cargo_version { CargoPackageVersion, CargoVersionRequirement }
import std.types { FilePathParts }

// -- Edition -------------------------------------------------------
Expand All @@ -35,11 +36,15 @@ fn rust_edition_str(edition: RustEdition) -> String {

data default_rust_edition: RustEdition = Edition2021

// Minimum cargo for edition 2021 (Cargo Reference: "The edition field").
// Pinned toolchain stays rust-toolchain.toml — this is the honest floor.
data min_cargo_version: CargoVersionRequirement = ">= 1.56"

// -- Package model -------------------------------------------------

type CargoPackage {
name: String
version: String
version: CargoPackageVersion
edition: RustEdition
path: String
}
Expand All @@ -51,7 +56,7 @@ type CargoPackage {
// version (with optional features); a path dependency points at a local
// crate directory. (Git/other sources extend this coproduct when needed.)
type CargoDepSource
= RegistryDep { version: String, features: List<String> }
= RegistryDep { version: CargoVersionRequirement, features: List<String> }
| LocalPathDep { path: String }

type CargoDependency {
Expand Down
44 changes: 44 additions & 0 deletions dsl/extdeps/rust/version.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
// extdeps/rust/version.dag — Cargo version carriers (SemVer scheme + requirements).
//
// Fidelity — extdeps invariant (cite source; DESIGN.md §3):
// Spec: https://doc.rust-lang.org/cargo/reference/manifest.html
// Package version field: SemVer 2.0.0 (manifest.md#the-version-field).
// Dependency version field: semver version requirement
// (specifying-dependencies.md#specifying-dependencies) — caret/tilde/comparator
// syntax, not a bare published version.
//
// Authority: extdeps.version.semver (semver.org), not std.types.SemVer.
//
// Consumers:
// extdeps/rust/cargo.dag — `CargoPackage`, `RegistryDep`

module extdeps.cargo_version

import extdeps.version.semver { SemVerIdentity, SemVerConstraint }

// Published crate version in `[package].version` (crates.io / workspace manifests).
type CargoPackageVersion = SemVerIdentity

// Dependency version requirement in `[dependencies].crate = "…"`.
type CargoVersionRequirement = SemVerConstraint

// Single authority for the stage0/bootstrap crate package version token.
data default_stage0_package_version: CargoPackageVersion = "0.1.0"

// Render helpers exercised by witnesses (manifest emission reuses these tokens).
fn render_cargo_package_version_field(version: CargoPackageVersion) -> String {
concat("version = \"", version, "\"")
}

fn render_cargo_version_requirement_toml(req: CargoVersionRequirement) -> String {
concat("\"", req, "\"")
}

// `[package]` header through default_stage0_package_version — shared by
// `stage0_crates.emit_stage0_crate_manifest` and `emit_rust.emit_cargo_toml`.
fn render_cargo_package_header_prefix(name: String) -> String {
concat(
"[package]\nname = \"", name, "\"\n",
render_cargo_package_version_field(version: default_stage0_package_version)
)
}
30 changes: 30 additions & 0 deletions dsl/extdeps/version/semver.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
// extdeps/version/semver.dag — Semantic Versioning scheme (slice 2).
//
// Spec: https://semver.org/
//
// Inhabits extdeps.version carriers — not std.types.SemVer (String alias; OCI migration
// is a separate escalation-gated PR). Ecosystem consumers (Cargo package version, etc.)
// import SemVerIdentity / SemVerConstraint from here.
//
// Structured MAJOR.MINOR.PATCH decomposition and semver-aware ordering land in slice-2b;
// semver_scheme below uses wire-label equality until then (dissolve-on).

module extdeps.version.semver

import extdeps.version { VersionIdentity, VersionScheme, VersionConstraint }
import std.algebra { Ordering, Less, Equal, Greater }

// Published semver version label (MAJOR.MINOR.PATCH wire form).
type SemVerIdentity = VersionIdentity

// Semver version requirement / comparator wire text — not a published identity.
type SemVerConstraint = VersionConstraint

// Interim compare: equality on wire labels only (slice-2b adds semver-aware ordering).
fn semver_identity_compare(a: VersionIdentity, b: VersionIdentity) -> Ordering {
if a == b { Equal } else { if a < b { Less } else { Greater } }
}

data semver_scheme: VersionScheme = {
compare: semver_identity_compare
}
19 changes: 11 additions & 8 deletions dsl/std/realization_width.dag
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,12 @@ module std.realization_width
import std.types { Int, List }
import std.measure {
HardwareThreadCount,
NanosecondDuration,
hardware_thread_count,
hardware_thread_count_value,
Nano,
}
import std.verification {
NanosecondDuration,
nanosecond_duration,
}
import std.pareto { AxisGoal, LowerIsBetter }
Expand All @@ -38,7 +41,7 @@ import std.realization_schedule {
schedule_eq,
cost_account_measured,
cost_account_predicted_zero,
cost_account_time_nanos,
cost_account_time_count,
}

fn int_min(a: Int, b: Int) -> Int {
Expand Down Expand Up @@ -72,13 +75,13 @@ fn width_fold_objective_goals() -> List<AxisGoal> {
}

type WidthBoundedRealization {
plan: RealizationPlan
plan: RealizationPlan<Nano>
spawn_width: HardwareThreadCount
}

// Width is peripheral: the schedule topology is unchanged (§3 invariant).
fn width_bounded_realization(
plan: RealizationPlan,
plan: RealizationPlan<Nano>,
shard_count: Int,
hardware_threads: HardwareThreadCount
) -> WidthBoundedRealization {
Expand All @@ -89,7 +92,7 @@ fn width_bounded_realization(
}

fn witness_width_fold_preserves_schedule_topology(
plan: RealizationPlan,
plan: RealizationPlan<Nano>,
shard_count: Int,
hardware_threads: HardwareThreadCount
) -> Bool {
Expand Down Expand Up @@ -123,10 +126,10 @@ fn witness_budget_ignoring_fold_fails(
}

// Measured shard-balance scaffold: assignment must read CostAccount.basis=Measured.
fn shard_balance_slot_for_cost(cost: CostAccount, baseline: CostAccount) -> Int {
fn shard_balance_slot_for_cost(cost: CostAccount<Nano>, baseline: CostAccount<Nano>) -> Int {
match cost.basis {
Measured => cost_account_time_nanos(account: cost)
Predicted => cost_account_time_nanos(account: baseline)
Measured => cost_account_time_count(account: cost)
Predicted => cost_account_time_count(account: baseline)
}
}

Expand Down
76 changes: 76 additions & 0 deletions dsl/test/claim/cargo_version_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
// test/claim/cargo_version_witness_test.dag — by-execution witness for Cargo SemVer carriers.
//
// DESIGN §5 green-by-execution: `CargoPackageVersion` and `CargoVersionRequirement`
// are not spec-without-execution — this witness folds render helpers and the stage0
// default over discriminating inputs. Reverting either field to bare `String` or
// dropping the branded requirement carrier breaks the typed data rows below.

module test.claim.cargo_version

import extdeps.cargo {
CargoPackage,
CargoDependency,
RegistryDep,
Edition2021,
min_cargo_version,
}
import extdeps.cargo_version {
default_stage0_package_version,
render_cargo_package_version_field,
render_cargo_package_header_prefix,
render_cargo_version_requirement_toml,
}

fn w_stage0_default_package_version() -> Bool {
default_stage0_package_version == "0.1.0"
&& render_cargo_package_version_field(version: default_stage0_package_version) == "version = \"0.1.0\""
}

fn w_package_version_field_renders() -> Bool {
let pkg = CargoPackage {
name: "demo",
version: "2.4.6",
edition: Edition2021,
path: "."
}
render_cargo_package_version_field(version: pkg.version) == "version = \"2.4.6\""
}

fn w_registry_dep_version_requirements() -> Bool {
let serde = CargoDependency {
name: "serde",
source: RegistryDep { version: "1", features: ["derive", "rc"] }
}
let stacker = CargoDependency {
name: "stacker",
source: RegistryDep { version: "0.1", features: [] }
}
match serde.source {
RegistryDep { version: v, features: f } =>
render_cargo_version_requirement_toml(req: v) == "\"1\""
&& (f |> count) == 2
LocalPathDep { path: _ } => false
}
&& match stacker.source {
RegistryDep { version: v, features: f } =>
render_cargo_version_requirement_toml(req: v) == "\"0.1\""
&& (f |> count) == 0
LocalPathDep { path: _ } => false
}
}

fn w_requirement_distinct_from_package_version() -> Bool {
render_cargo_version_requirement_toml(req: "1") != render_cargo_package_version_field(version: "1.0.0")
}

fn w_emitter_header_prefix_uses_default() -> Bool {
render_cargo_package_header_prefix(name: "demo-crate") == "[package]\nname = \"demo-crate\"\nversion = \"0.1.0\""
}

test fn cargo_version_witnesses() -> Bool {
w_stage0_default_package_version()
&& w_package_version_field_renders()
&& w_registry_dep_version_requirements()
&& w_requirement_distinct_from_package_version()
&& w_emitter_header_prefix_uses_default()
}
38 changes: 38 additions & 0 deletions dsl/test/claim/extdeps_version_semver_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// By-execution witnesses for extdeps.version.semver (slice 2).
//
// Run via:
// gunbc run --source-root dsl --entry dsl/test/claim/extdeps_version_semver_witness_test.dag \
// --function extdeps_version_semver_witnesses --claim-run

module test.claim.extdeps_version_semver

import extdeps.version.semver { SemVerIdentity, SemVerConstraint, semver_scheme }
import std.algebra { Equal }

fn semver_identity_1_2_3() -> SemVerIdentity { "1.2.3" }
fn semver_constraint_caret() -> SemVerConstraint { "^1.2" }
fn semver_identity_1_0_0() -> SemVerIdentity { "1.0.0" }
fn semver_constraint_one() -> SemVerConstraint { "1" }

fn w_semver_identity_inhabits_version_identity() -> Bool {
semver_identity_1_2_3() == "1.2.3"
}

fn w_semver_constraint_inhabits_version_constraint() -> Bool {
semver_constraint_caret() == "^1.2"
}

fn w_identity_distinct_from_constraint() -> Bool {
semver_identity_1_0_0() != semver_constraint_one()
}

fn w_semver_scheme_equality_compare() -> Bool {
semver_scheme.compare("1.0.0", "1.0.0") == Equal
}

test fn extdeps_version_semver_witnesses() -> Bool {
w_semver_identity_inhabits_version_identity()
&& w_semver_constraint_inhabits_version_constraint()
&& w_identity_distinct_from_constraint()
&& w_semver_scheme_equality_compare()
}
2 changes: 1 addition & 1 deletion dsl/test/claim/realization_width_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ fn witness_threads_4() -> HardwareThreadCount {
hardware_thread_count(4)
}

fn synthetic_plan() -> RealizationPlan {
fn synthetic_plan() -> RealizationPlan<Nano> {
RealizationPlan {
target: "width-witness-target"
objective: RealizationObjective { goals: [] }
Expand Down
3 changes: 2 additions & 1 deletion src/v1/05_emit_rust.dag
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ import extdeps.languages.rust.emit {
rust_serde_rename_all_snake_case, rust_serde_rename_all_screaming_snake_case,
HigherOrderMethodSpec, rust_higher_order_methods
}
import extdeps.cargo_version { render_cargo_package_header_prefix }
import v1.compiler.languages {
scaffold_for_target, serialization_for_target,
TestConventions, ItemKeywords,
Expand Down Expand Up @@ -7511,7 +7512,7 @@ fn emit_cargo_dep(name: String, version: String, features: List<String>) -> Stri
}

fn emit_cargo_toml(crate_name: String, has_services: Bool) -> TextFile {
let header = concat("[package]\nname = \"", crate_name, "\"\nversion = \"0.1.0\"\nedition = \"2021\"\n")
let header = concat(render_cargo_package_header_prefix(name: crate_name), "\nedition = \"2021\"\n")
let workspace = "\n[workspace]\n"
let base_deps = [
emit_cargo_dep(name: "serde", version: "1", features: ["derive", "rc"]),
Expand Down
4 changes: 3 additions & 1 deletion src/v1/stage0_crates.dag
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ module v1.compiler.stage0_crates
import v1.std.core { TextFile }
import v1.compiler.emit_rust { emit_non_empty_wrappers, emit_cargo_dep }
import extdeps.cargo { CargoDependency, CargoFeature, RegistryDep, LocalPathDep }
import extdeps.cargo_version { render_cargo_package_header_prefix }

// =========================================================================
// Crate-boundary model
Expand Down Expand Up @@ -155,7 +156,8 @@ fn render_stage0_crate_features_section(features: List<CargoFeature>) -> String
fn emit_stage0_crate_manifest(spec: Stage0CrateSpec) -> TextFile {
let deps = spec.dependencies |> map(render_stage0_crate_dep) |> join(separator: "")
let content = concat(
"[package]\nname = \"", spec.package_name, "\"\nversion = \"0.1.0\"\nedition = \"2021\"",
render_cargo_package_header_prefix(name: spec.package_name),
"\nedition = \"2021\"",
render_stage0_crate_features_section(features: spec.features),
"\n\n[dependencies]\n",
deps
Expand Down