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
3 changes: 0 additions & 3 deletions dsl/gunbc/compiler.dag
Original file line number Diff line number Diff line change
Expand Up @@ -74,16 +74,13 @@ data stage0: GeneratedCrate = {
source_dir: "src/v3/compiler/src",
hand_maintained_src: [
"bootstrap.rs",
"cost_basis_declaration.rs",
"dag.rs",
"diagnostics.rs",
"dimension.rs",
"emit.rs",
"emit_go.rs",
"emit_python.rs",
"emit_rust.rs",
// PB-1 Item 5: hand-authored `main.rs` shell formatter (not emitted into src/).
"emit_rust_bin_shim.rs",
"python_target.rs",
"rust_target.rs",
"infer.rs",
Expand Down
109 changes: 107 additions & 2 deletions src/v3/compiler/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -436,6 +436,97 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) {
/// **Hygiene:** `repeat_string` exists in the bootstrap bundle only via this excerpt — no
/// hand-maintained duplicate of `render.dag` (INVARIANTS P2). Edit the marked region in
/// `render.dag` only; this output is overwritten on `cargo build -p v3-compiler`.
/// Emit PB-0 cycle-4 host authority modules (former `EXPECTED_HAND_AUTHORED_NON_TEST` paths) from
/// checked-in templates so `REGEN_OUTPUTS` / `GENERATED_FILES` stay the sole SG-0 partition
/// authority (`sg0_v3_hand_authored_census`).
///
/// **Templates** live under `tools/pb0_cycle4_emit_templates/*.rs.in` (workspace root — not under
/// `src/v3/compiler/`, so they are outside the SG-0 `.rs` walk and not misread as hand-authored
/// compiler sources). **Full substrate dissolution** (`.dag` / lens-producer authority replacing
/// this body) is the separate T-LP-Retirement program; this path is the bounded PB-0 census
/// partition receipt per `docs/briefs/r3-pb0-non-test-retirement-worker.md`.
///
/// **Checked-in outputs:** the emitted `*_generated.rs` paths are tracked in git like other
/// `REGEN_OUTPUTS` modules (not gitignored). `cargo build` / `cargo check` runs this `build.rs`
/// hook before `rustc` sees `lib.rs`, and `cargo:rerun-if-changed` on the template directory
/// forces a rebuild when `.rs.in` edits land — refresh committed `*_generated.rs` in the same PR
/// as template edits (CI exercises the full path).
///
/// Do not hand-edit `*_generated.rs`; edit the `.rs.in` templates and rebuild.
fn emit_pb0_cycle4_host_authority_modules(repo_root: &Path) {
const HEADER: &str = concat!(
"// AUTO-GENERATED by src/v3/compiler/build.rs (`emit_pb0_cycle4_host_authority_modules`).\n",
"//\n",
"// Template: `tools/pb0_cycle4_emit_templates/<stem>.rs.in` (workspace root).\n",
"// Dissolution receipt: PB-0 NON_TEST partition — `REGEN_OUTPUTS` producer; full `.dag` emit T-LP track.\n",
"//\n",
"\n",
);
let tmpl_dir = repo_root.join("tools/pb0_cycle4_emit_templates");
let specs: &[(&str, &str)] = &[
(
"complexity_lattice.rs.in",
"src/v3/compiler/src/complexity_lattice_generated.rs",
),
(
"cost_basis_declaration.rs.in",
"src/v3/compiler/src/cost_basis_declaration_generated.rs",
),
(
"emit_collection_ops_method_contract.rs.in",
"src/v3/compiler/src/emit/collection_ops_method_contract_generated.rs",
),
(
"emit_rust_bin_shim.rs.in",
"src/v3/compiler/src/emit_rust_bin_shim_generated.rs",
),
(
"enforced_lens_application.rs.in",
"src/v3/compiler/src/enforced_lens_application_generated.rs",
),
(
"int_literal_ranges.rs.in",
"src/v3/compiler/src/int_literal_ranges_generated.rs",
),
(
"pb_method_template_projection.rs.in",
"src/v3/compiler/src/pb_method_template_projection_generated.rs",
),
];
for (tmpl_name, rel_out) in specs {
let src_path = tmpl_dir.join(tmpl_name);
println!("cargo:rerun-if-changed={}", src_path.display());
let body = fs::read_to_string(&src_path).unwrap_or_else(|e| {
panic!(
"emit_pb0_cycle4_host_authority_modules: read template {}: {e}",
src_path.display()
)
});
let out_path = repo_root.join(rel_out);
if let Some(parent) = out_path.parent() {
fs::create_dir_all(parent).unwrap_or_else(|e| {
panic!(
"emit_pb0_cycle4_host_authority_modules: mkdir {}: {e}",
parent.display()
)
});
}
let generated = format!("{HEADER}{body}");
let needs_write = match fs::read_to_string(&out_path) {
Ok(existing) => existing != generated,
Err(_) => true,
};
if needs_write {
fs::write(&out_path, generated).unwrap_or_else(|e| {
panic!(
"emit_pb0_cycle4_host_authority_modules: write {}: {e}",
out_path.display()
)
});
}
}
}

fn emit_render_repeat_string_bootstrap(repo_root: &Path) {
const BEGIN: &str = "// GUNBC_BOOTSTRAP_EMIT_BEGIN\n";
const END: &str = "// GUNBC_BOOTSTRAP_EMIT_END";
Expand Down Expand Up @@ -529,6 +620,7 @@ fn main() {
let src_dir = v3_dir.parent().expect("v3 dir has parent");
let repo_root = src_dir.parent().expect("src dir has parent");
emit_render_repeat_string_bootstrap(repo_root);
emit_pb0_cycle4_host_authority_modules(repo_root);
let std_dir = v3_dir.join("std");
let spec_dir = v3_dir.join("spec");
let compiler_dir = manifest_path.clone();
Expand All @@ -545,6 +637,10 @@ fn main() {
println!("cargo:rerun-if-changed={}", extdeps_dir.display());
println!("cargo:rerun-if-changed={}", gunbc_dir.display());
println!("cargo:rerun-if-changed={}", dsl_std_dir.display());
println!(
"cargo:rerun-if-changed={}",
repo_root.join("tools/pb0_cycle4_emit_templates").display()
);

// Structural-recursion termination analysis walks a recursing
// argument back to its declared Disj connective (see
Expand Down Expand Up @@ -658,6 +754,9 @@ fn main() {
"src/v3/compiler/src/bootstrap_generated.rs",
"src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs",
"src/v3/compiler/src/bootstrap_std_generated.rs",
// PB-0 cycle-4: former hand `EXPECTED_HAND_AUTHORED_NON_TEST` modules — templates under
// `tools/pb0_cycle4_emit_templates/*.rs.in`, emitted by `emit_pb0_cycle4_host_authority_modules`.
"src/v3/compiler/src/complexity_lattice_generated.rs",
// SG-5 substrate / runtime-mirror projections, generated from
// `src/v3/std/substrate.dag` + `src/v3/std/parse_surface.dag`
// and consumed by hand-authored Rust via `include!(...)`.
Expand All @@ -666,15 +765,20 @@ fn main() {
// outputs, so the content header alone never masquerades as
// generated (SG-0's `sg0_generated_partition_is_producer_owned`
// invariant).
"src/v3/compiler/src/complexity_lens_generated.rs",
"src/v3/compiler/src/cost_basis_declaration_generated.rs",
"src/v3/compiler/src/dag_branch_generated.rs",
"src/v3/compiler/src/dag_cluster_generated.rs",
"src/v3/compiler/src/dag_lookup_generated.rs",
"src/v3/compiler/src/dag_cost_generated.rs",
"src/v3/compiler/src/dag_lookup_generated.rs",
"src/v3/compiler/src/dag_scalar_generated.rs",
"src/v3/compiler/src/dag_value_body_generated.rs",
"src/v3/compiler/src/diagnostics_generated.rs",
"src/v3/compiler/src/emit/collection_ops_method_contract_generated.rs",
"src/v3/compiler/src/emit_rust_bin_shim_generated.rs",
"src/v3/compiler/src/enforced_lens_application_generated.rs",
"src/v3/compiler/src/infer_helpers_generated.rs",
"src/v3/compiler/src/complexity_lens_generated.rs",
"src/v3/compiler/src/int_literal_ranges_generated.rs",
"src/v3/compiler/src/lens_cost_symbolic_generated.rs",
"src/v3/compiler/src/lens_cost_target_realization_generated.rs",
"src/v3/compiler/src/lens_effect_enumeration_generated.rs",
Expand All @@ -684,6 +788,7 @@ fn main() {
"src/v3/compiler/src/lens_unused_parameters_generated.rs",
"src/v3/compiler/src/lower_helpers_generated.rs",
"src/v3/compiler/src/operators_generated.rs",
"src/v3/compiler/src/pb_method_template_projection_generated.rs",
"src/v3/compiler/src/parse_generated.rs",
"src/v3/compiler/src/parse_surface_generated.rs",
"src/v3/compiler/src/parse_tables_generated.rs",
Expand Down
115 changes: 115 additions & 0 deletions src/v3/compiler/src/complexity_lattice_generated.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,115 @@
// AUTO-GENERATED by src/v3/compiler/build.rs (`emit_pb0_cycle4_host_authority_modules`).
//
// Template: `tools/pb0_cycle4_emit_templates/<stem>.rs.in` (workspace root).
// Dissolution receipt: PB-0 NON_TEST partition — `REGEN_OUTPUTS` producer; full `.dag` emit T-LP track.
//

//! **`complexity_enforcement_budget_dominates`** — executable **T-LAS enforcement**
//! ordering on `AsymptoticClass` for `complexity_enforcement_violates` /
//! `EnforcedApplication` (gate #92). It matches `v3.std.algebra::asymptotic_dominates`
//! on every arm including `ClassPolynomial×ClassPolynomial` (Peano `degree` compare).
//!
//! **`asymptotic_dominates`** is a backward-compatible alias for tests and older
//! call sites; new enforcement code should call [`complexity_enforcement_budget_dominates`].
//!
//! Stay aligned with `complexity.dag` + `complexity_enforcement_violates` comments.

use crate::dag::{positive_descent_count, AsymptoticClass};

pub fn complexity_enforcement_budget_dominates(a: &AsymptoticClass, b: &AsymptoticClass) -> bool {
use AsymptoticClass::*;
match a {
ClassUnknown => true,
ClassExponential => match b {
ClassUnknown => false,
ClassExponential
| ClassPolynomial { .. } // Any `ClassPolynomial` tier is below exponential.
| ClassQuadratic
| ClassLinearithmic
| ClassLinear
| ClassLog
| ClassConstant => true,
},
ClassPolynomial { degree: da } => match b {
ClassUnknown | ClassExponential => false,
ClassPolynomial { degree: db } => {
positive_descent_count(da) >= positive_descent_count(db)
}
ClassQuadratic | ClassLinearithmic | ClassLinear | ClassLog | ClassConstant => true,
},
ClassQuadratic => match b {
ClassConstant | ClassLog | ClassLinear | ClassLinearithmic | ClassQuadratic => true,
ClassPolynomial { .. } | ClassExponential | ClassUnknown => false,
},
ClassLinearithmic => match b {
ClassConstant | ClassLog | ClassLinear | ClassLinearithmic => true,
ClassQuadratic | ClassPolynomial { .. } | ClassExponential | ClassUnknown => false,
},
ClassLinear => match b {
ClassConstant | ClassLog | ClassLinear => true,
ClassLinearithmic
| ClassQuadratic
| ClassPolynomial { .. }
| ClassExponential
| ClassUnknown => false,
},
ClassLog => match b {
ClassConstant | ClassLog => true,
ClassLinear
| ClassLinearithmic
| ClassQuadratic
| ClassPolynomial { .. }
| ClassExponential
| ClassUnknown => false,
},
ClassConstant => match b {
ClassConstant => true,
ClassLog
| ClassLinear
| ClassLinearithmic
| ClassQuadratic
| ClassPolynomial { .. }
| ClassExponential
| ClassUnknown => false,
},
}
}

/// Alias of [`complexity_enforcement_budget_dominates`]. Prefer the named helper for
/// new call sites so enforcement-grade poly refinement is not confused with substrate
/// `algebra.dag::asymptotic_dominates` at the documentation layer.
#[inline]
pub fn asymptotic_dominates(a: &AsymptoticClass, b: &AsymptoticClass) -> bool {
complexity_enforcement_budget_dominates(a, b)
}

#[cfg(test)]
mod asymptotic_dominates_tests {
use super::{asymptotic_dominates, complexity_enforcement_budget_dominates};
use crate::dag::{positive_amount_from_i64, AsymptoticClass};

fn poly(k: i64) -> AsymptoticClass {
AsymptoticClass::ClassPolynomial {
degree: positive_amount_from_i64(k).expect("test degree in range"),
}
}

#[test]
fn polynomial_degree_orders_within_class_polynomial() {
let p5 = poly(5);
let p3 = poly(3);
assert!(complexity_enforcement_budget_dominates(&p5, &p3));
assert!(!complexity_enforcement_budget_dominates(&p3, &p5));
assert!(complexity_enforcement_budget_dominates(&p3, &p3));
}

#[test]
fn alias_matches_budget_dominates() {
let p3 = poly(3);
let p5 = poly(5);
assert_eq!(
asymptotic_dominates(&p5, &p3),
complexity_enforcement_budget_dominates(&p5, &p3)
);
}
}
Loading
Loading