use crate::Result;
use crate::backend::BackendCapabilities;
use crate::backend::conformance::BackendConformanceRunner;
use crate::backend::gpu::GpuScaffoldBackend;
use crate::facade::Tokitai;
use crate::object::sheaf::{Cover, FiniteSite, Inclusion, OpenId, SectionTable};
use crate::op::OperatorRegistry;
use crate::planner::HeuristicPlanner;
use crate::theory::{
TheoryId, categorical_law_theory_evidence, finite_sheaf_compatibility_theory_evidence,
padic_valuation_cutoff_theory_evidence, validate_theory_evidence,
};
use crate::verify::{
PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID, PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID,
PropertyCheckReport, SemanticConformanceReport, SupportStatus, TheoremBindingRegistry,
TheorySupportMatrix, check_padic_contract_properties, check_sheaf_contract_properties,
generated_theory_support_matrix, semantic_conformance_report,
};
pub const THEORY_ENGINEERING_RELEASE_GATE_ARTIFACT: &str =
"tokitai-theory-engineering-release-gate";
pub const THEORY_ENGINEERING_RELEASE_GATE_VERSION: u32 = 1;
const PADIC_THEOREM_CHECKER_SCRIPT: &str =
include_str!("../../scripts/check_padic_valuation_skip_theorem.sh");
const FINITE_SHEAF_THEOREM_CHECKER_SCRIPT: &str =
include_str!("../../scripts/check_finite_sheaf_gluing_theorem.sh");
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ReleaseGateCheck {
pub name: String,
pub passed: bool,
pub evidence: Vec<String>,
pub blockers: Vec<String>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoryEngineeringReleaseGateReport {
pub artifact: String,
pub version: u32,
pub checks: Vec<ReleaseGateCheck>,
pub required_commands: Vec<String>,
pub deferred_work: Vec<String>,
pub known_limits: Vec<String>,
}
impl TheoryEngineeringReleaseGateReport {
pub fn passed(&self) -> bool {
self.checks.iter().all(|check| check.passed)
}
pub fn blockers(&self) -> Vec<String> {
self.checks
.iter()
.flat_map(|check| check.blockers.iter().cloned())
.collect()
}
pub fn to_markdown(&self) -> String {
let mut lines = vec![
"# Theory-Engineering Release Gate".to_string(),
String::new(),
format!("artifact: {}", self.artifact),
format!("version: {}", self.version),
format!("passed: {}", self.passed()),
String::new(),
"| Check | Passed | Evidence | Blockers |".to_string(),
"| --- | --- | --- | --- |".to_string(),
];
for check in &self.checks {
lines.push(format!(
"| {} | {} | {} | {} |",
md(&check.name),
check.passed,
md(&check.evidence.join("<br>")),
md(&check.blockers.join("<br>"))
));
}
lines.push(String::new());
lines.push("## Required Commands".to_string());
for command in &self.required_commands {
lines.push(format!("- `{command}`"));
}
lines.push(String::new());
lines.push("## Deferred Work".to_string());
for item in &self.deferred_work {
lines.push(format!("- {item}"));
}
lines.push(String::new());
lines.push("## Known Limits".to_string());
for item in &self.known_limits {
lines.push(format!("- {item}"));
}
lines.join("\n")
}
pub fn to_json(&self) -> String {
let checks = self
.checks
.iter()
.map(ReleaseGateCheck::to_json)
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":{},\"version\":{},\"passed\":{},\"checks\":[{}],\"required_commands\":{},\"deferred_work\":{},\"known_limits\":{}}}",
json_string(&self.artifact),
self.version,
self.passed(),
checks,
json_array(&self.required_commands),
json_array(&self.deferred_work),
json_array(&self.known_limits)
)
}
}
impl ReleaseGateCheck {
fn passed(name: impl Into<String>, evidence: Vec<String>) -> Self {
Self {
name: name.into(),
passed: true,
evidence,
blockers: Vec::new(),
}
}
fn failed(name: impl Into<String>, blockers: Vec<String>, evidence: Vec<String>) -> Self {
Self {
name: name.into(),
passed: false,
evidence,
blockers,
}
}
fn to_json(&self) -> String {
format!(
"{{\"name\":{},\"passed\":{},\"evidence\":{},\"blockers\":{}}}",
json_string(&self.name),
self.passed,
json_array(&self.evidence),
json_array(&self.blockers)
)
}
}
pub fn run_theory_engineering_release_gate() -> Result<TheoryEngineeringReleaseGateReport> {
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let theorem_registry = TheoremBindingRegistry::tokitai_default()?;
let q5 = crate::domain::PadicDomain::new(5, 3)?;
let planner = HeuristicPlanner::new(BackendCapabilities::cpu_scalar());
let padic_plan = planner.plan_padic_sum_products_skip_with_registry(&q5, 0, 1, 2, ®istry);
let padic_evidence = padic_valuation_cutoff_theory_evidence(&padic_plan)?;
let (site, cover) = release_sheaf_fixture();
let sheaf_plan = planner.plan_cover_glue_check_with_registry(&cover, ®istry);
let mut sections = SectionTable::new();
sections.insert(open("A"), 5);
sections.insert(open("B"), 5);
sections.insert(open("A_cap_B"), 5);
let compatibility = sections.compatibility_report(&site, &cover);
let sheaf_evidence = finite_sheaf_compatibility_theory_evidence(&sheaf_plan, &compatibility)?;
let categorical_evidence = categorical_law_theory_evidence(true, true)?;
let mut properties = check_padic_contract_properties(&q5)?;
properties.extend(check_sheaf_contract_properties(
&site,
&cover,
(&open("A_cap_B"), &open("A"), &open("U")),
)?);
properties.extend([
PropertyCheckReport::passed("categorical identity witness", 1),
PropertyCheckReport::passed("categorical associative composition witness", 1),
]);
let gpu_conformance = BackendConformanceRunner::new().run_gpu_scaffold(&GpuScaffoldBackend)?;
let semantic_report = semantic_conformance_report(
&[&padic_plan, &sheaf_plan],
&[padic_evidence, sheaf_evidence, categorical_evidence],
&properties,
Some(&gpu_conformance),
)?;
let support_matrix = generated_theory_support_matrix()?;
let facade_evidence = facade_gate_evidence(&q5, &cover)?;
let report = theory_engineering_release_gate_from_parts(
&semantic_report,
&support_matrix,
&theorem_registry,
&facade_evidence,
)?;
#[cfg(feature = "rocm-hip")]
{
let mut report = report;
append_rocm_hip_feature_checks(&mut report)?;
return Ok(report);
}
#[cfg(not(feature = "rocm-hip"))]
{
Ok(report)
}
}
pub fn theory_engineering_release_gate_from_parts(
semantic_report: &SemanticConformanceReport,
support_matrix: &TheorySupportMatrix,
theorem_registry: &TheoremBindingRegistry,
facade_evidence: &[String],
) -> Result<TheoryEngineeringReleaseGateReport> {
theorem_registry.validate()?;
let mut checks = Vec::new();
checks.push(check_theory_contracts(semantic_report));
checks.push(check_theorem_bindings(theorem_registry));
checks.push(check_semantic_conformance(semantic_report));
checks.push(check_support_matrix(support_matrix));
checks.push(check_certified_padic_gemm_claim_gate(
support_matrix,
theorem_registry,
));
checks.push(check_optional_theorem_checker_timeout_policy());
checks.push(check_mandatory_proof_assistant_profile());
checks.push(check_facade_examples(facade_evidence));
checks.push(check_known_limit_coverage(support_matrix));
Ok(TheoryEngineeringReleaseGateReport {
artifact: THEORY_ENGINEERING_RELEASE_GATE_ARTIFACT.to_string(),
version: THEORY_ENGINEERING_RELEASE_GATE_VERSION,
checks,
required_commands: vec![
"cargo fmt --check".to_string(),
"python -m json.tool todo.json >/dev/null".to_string(),
"cargo test --offline".to_string(),
"cargo test --offline --features rocm-hip".to_string(),
"cargo test --offline --features rocm-hip --test rocm_audit_traces".to_string(),
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks"
.to_string(),
"cargo run --quiet --offline --example paper_benchmarks".to_string(),
"cargo run --quiet --offline --features rocm-hip --example rocm_benchmarks"
.to_string(),
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks"
.to_string(),
"sh scripts/check_padic_valuation_skip_theorem.sh".to_string(),
"sh scripts/check_finite_sheaf_gluing_theorem.sh".to_string(),
"TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_padic_valuation_skip_theorem.sh".to_string(),
"TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_finite_sheaf_gluing_theorem.sh".to_string(),
],
deferred_work: vec![
"full p-adic algebra and arbitrary precision p-adic fields".to_string(),
"general sheaf theory, sheaf cohomology, and global repair synthesis".to_string(),
"full category-theory framework beyond law witnesses".to_string(),
"nonstandard-domain GPU acceleration beyond CPU fallback evidence".to_string(),
"production performance claims and broad tensor compiler maturity".to_string(),
],
known_limits: vec![
"CPU reference remains the semantic oracle".to_string(),
"Lean theorem packages cover minimized theorem boundaries, not the Rust runtime".to_string(),
"P263 mandatory proof-assistant profile applies only to the selected p-adic valuation and finite-sheaf theorem files when strict mode is requested".to_string(),
"Optional Lean execution is bounded by TOKITAI_LEAN_TIMEOUT_SECONDS; default timeout evidence is non-blocking, success transcripts are captured when Lean runs, while TOKITAI_REQUIRE_LEAN=1 fails closed".to_string(),
"ROCm/HIP pilots are feature-gated local evidence and remain CPU-oracle checked"
.to_string(),
"ROCm/HIP hardware contract records local device evidence only; it does not execute kernels"
.to_string(),
"HIP audit traces bind provenance and guardrails; they do not verify generated machine code"
.to_string(),
"paper benchmark rows are deterministic evidence and CI checks, not production speed claims"
.to_string(),
"certified valuation-sparse p-adic GEMM is scoped to fixed precision and does not claim full p-adic algebra"
.to_string(),
],
})
}
fn check_optional_theorem_checker_timeout_policy() -> ReleaseGateCheck {
let scripts = [
(
"p-adic valuation theorem checker",
PADIC_THEOREM_CHECKER_SCRIPT,
),
(
"finite-sheaf gluing theorem checker",
FINITE_SHEAF_THEOREM_CHECKER_SCRIPT,
),
];
let mut blockers = Vec::new();
let mut evidence = Vec::new();
for (name, script) in scripts {
let required_tokens = [
"TOKITAI_LEAN_TIMEOUT_SECONDS",
"timeout -k 2s",
"lean_status=\"timeout\"",
"lean_status=$lean_status",
"required=$require_lean",
"status=accepted",
"success_transcript=captured",
"artifact_sha256=",
"stdout_file=",
"stderr_file=",
"if [ \"$require_lean\" = \"1\" ] || [ \"$lean_status\" != \"timeout\" ]; then",
"exit 0",
];
let missing = required_tokens
.iter()
.filter(|token| !script.contains(**token))
.copied()
.collect::<Vec<_>>();
if missing.is_empty() {
evidence.push(format!(
"{name}: bounded optional Lean timeout policy and success transcript capture present"
));
} else {
blockers.push(format!(
"{name}: missing timeout policy token(s): {}",
missing.join(", ")
));
}
}
if blockers.is_empty() {
ReleaseGateCheck::passed("optional Lean timeout policy", evidence)
} else {
ReleaseGateCheck::failed("optional Lean timeout policy", blockers, evidence)
}
}
fn check_mandatory_proof_assistant_profile() -> ReleaseGateCheck {
let scripts: [(&str, &str, &[&str]); 2] = [
(
"p-adic valuation theorem checker",
PADIC_THEOREM_CHECKER_SCRIPT,
&[
"tokitai_padic_valuation_skip_sound_mod_pk",
"tokitai_padic_valuation_skip_dot_product_sound_mod_pk",
"tokitai_padic_valuation_skip_matrix_output_sound_mod_pk",
],
),
(
"finite-sheaf gluing theorem checker",
FINITE_SHEAF_THEOREM_CHECKER_SCRIPT,
&[
"tokitai_finite_sheaf_gluing_sound",
"tokitai_finite_sheaf_incompatible_overlap_blocks_gluing",
],
),
];
let mut blockers = Vec::new();
let mut evidence = Vec::new();
for (name, script, selected_theorems) in scripts {
for token in [
"evidence_profile=selected-theorem-strict-capable",
"selected_theorems=",
"TOKITAI_REQUIRE_LEAN",
"required=$require_lean",
"success_transcript=captured",
"structural_validation=passed",
] {
if !script.contains(token) {
blockers.push(format!("{name}: missing strict-profile token {token}"));
}
}
for theorem in selected_theorems {
if !script.contains(theorem) {
blockers.push(format!("{name}: missing selected theorem {theorem}"));
}
}
evidence.push(format!(
"{name}: selected_theorems={} strict_mode=TOKITAI_REQUIRE_LEAN=1",
selected_theorems.join(",")
));
}
if blockers.is_empty() {
ReleaseGateCheck::passed("mandatory proof-assistant evidence profile", evidence)
} else {
ReleaseGateCheck::failed(
"mandatory proof-assistant evidence profile",
blockers,
evidence,
)
}
}
#[cfg(feature = "rocm-hip")]
fn append_rocm_hip_feature_checks(report: &mut TheoryEngineeringReleaseGateReport) -> Result<()> {
let benchmark_report = crate::verify::generate_rocm_benchmark_report()?;
report
.checks
.push(check_rocm_hip_benchmark_report(&benchmark_report));
let audit_report = crate::verify::hip_audit_report_from_rocm_benchmarks(&benchmark_report)?;
report.checks.push(check_hip_audit_report(&audit_report));
let padic_benchmark_report =
crate::backend::hip_padic_benchmarks::generate_padic_stratified_benchmark_report()?;
report.checks.push(check_padic_stratified_benchmark_report(
&padic_benchmark_report,
));
let padic_audit_report =
crate::verify::hip_audit_report_from_padic_stratified_benchmarks(&padic_benchmark_report)?;
let mut padic_audit_check = check_hip_audit_report(&padic_audit_report);
padic_audit_check.name = "Certified p-adic GEMM HIP audit traces".to_string();
report.checks.push(padic_audit_check);
Ok(())
}
#[cfg(feature = "rocm-hip")]
fn check_rocm_hip_benchmark_report(
report: &crate::verify::RocmBenchmarkReport,
) -> ReleaseGateCheck {
let mut blockers = Vec::new();
if report.rows.is_empty() {
blockers.push("ROCm/HIP benchmark report has no rows".to_string());
}
if !report
.non_claims
.iter()
.any(|claim| claim.contains("not production speedup claims"))
{
blockers.push("ROCm/HIP benchmark report lacks speedup non-claim".to_string());
}
let has_executed = report.rows.iter().any(|row| row.status == "passed");
if has_executed {
for workload in [
"dense_i32_add_smoke",
"dense_i32_add_scale_1024",
"padic_valuation_fixed_precision",
"sheaf_overlap_compatible",
"sheaf_overlap_incompatible",
] {
if !report.rows.iter().any(|row| {
row.workload == workload && row.status == "passed" && row.cpu_oracle_matches
}) {
blockers.push(format!(
"ROCm/HIP benchmark report lacks CPU-oracle checked workload {workload}"
));
}
}
} else if !report.rows.iter().all(|row| row.status == "unavailable") {
blockers.push(
"ROCm/HIP benchmark report must contain passed rows or all-unavailable rows"
.to_string(),
);
}
if !report
.rows
.iter()
.any(|row| row.status == "fallback_captured" || row.status == "unavailable")
{
blockers
.push("ROCm/HIP benchmark report lacks fallback or unavailable evidence".to_string());
}
if blockers.is_empty() {
ReleaseGateCheck::passed(
"ROCm/HIP semantic conformance benchmarks",
vec![
format!("rows={}", report.rows.len()),
format!(
"executed_rows={}",
report
.rows
.iter()
.filter(|row| row.status == "passed")
.count()
),
format!(
"fallback_or_unavailable_rows={}",
report
.rows
.iter()
.filter(
|row| row.status == "fallback_captured" || row.status == "unavailable"
)
.count()
),
],
)
} else {
ReleaseGateCheck::failed(
"ROCm/HIP semantic conformance benchmarks",
blockers,
vec![report.to_markdown()],
)
}
}
fn check_theory_contracts(report: &SemanticConformanceReport) -> ReleaseGateCheck {
let mut blockers = Vec::new();
for theory in [
TheoryId::PadicValuation,
TheoryId::FiniteSheaf,
TheoryId::CategoricalLaw,
] {
if !report
.theory_statuses
.iter()
.any(|status| status.theory == theory && status.missing_evidence.is_empty())
{
blockers.push(format!(
"missing complete theory evidence for {}",
theory.as_str()
));
}
}
if blockers.is_empty() {
ReleaseGateCheck::passed(
"theory contracts",
report
.theory_statuses
.iter()
.map(|status| {
format!(
"{} status={} constraints={}",
status.theory.as_str(),
status.status.as_str(),
status.constraints.join("|")
)
})
.collect(),
)
} else {
ReleaseGateCheck::failed("theory contracts", blockers, Vec::new())
}
}
fn check_theorem_bindings(registry: &TheoremBindingRegistry) -> ReleaseGateCheck {
let descriptors = registry.descriptors();
if descriptors.len() >= 3 {
ReleaseGateCheck::passed(
"theorem bindings",
descriptors
.iter()
.map(|descriptor| {
format!(
"{} transcript={} checker={}",
descriptor.theorem_id,
descriptor.transcript.captured_status.as_str(),
descriptor.checker_command
)
})
.collect(),
)
} else {
ReleaseGateCheck::failed(
"theorem bindings",
vec![
"expected p-adic, finite-sheaf gluing, and finite-sheaf obstruction descriptors"
.to_string(),
],
Vec::new(),
)
}
}
fn check_semantic_conformance(report: &SemanticConformanceReport) -> ReleaseGateCheck {
if report.passed() {
ReleaseGateCheck::passed(
"semantic conformance report",
vec![
format!("cpu_oracle_fixtures={}", report.cpu_oracle.fixtures.len()),
format!("theory_statuses={}", report.theory_statuses.len()),
format!("audit_traces={}", report.audit_traces.len()),
],
)
} else {
ReleaseGateCheck::failed(
"semantic conformance report",
vec!["semantic conformance report did not pass".to_string()],
vec![report.to_text()],
)
}
}
fn check_support_matrix(matrix: &TheorySupportMatrix) -> ReleaseGateCheck {
let required = [
(
"cpu_scalar",
"padic_sum_products_valuation_skip",
SupportStatus::Supported,
),
("cpu_scalar", "matmul", SupportStatus::Supported),
("cpu_scalar", "cover_glue_check", SupportStatus::Supported),
(
"gpu_scaffold",
"padic_sum_products_valuation_skip",
SupportStatus::FallbackOnly,
),
(
"gpu_dense_i64_pilot",
"add",
SupportStatus::FeatureGatedPilot,
),
(
"rocm_hip_hardware_contract",
"hardware_contract",
SupportStatus::LocalHardwareEvidence,
),
(
"rocm_hip_dense_i32_pilot",
"add",
SupportStatus::FeatureGatedPilot,
),
(
"rocm_hip_dense_i32_pilot",
"add",
SupportStatus::Unavailable,
),
(
"rocm_hip_padic_valuation_pilot",
"valuation",
SupportStatus::FeatureGatedPilot,
),
(
"rocm_hip_padic_stratified_matmul_pilot",
"matmul",
SupportStatus::FeatureGatedPilot,
),
(
"rocm_hip_padic_stratified_benchmark_suite",
"matmul_benchmark_matrix",
SupportStatus::FeatureGatedPilot,
),
(
"rocm_hip_sheaf_locality_pilot",
"overlap_compatibility",
SupportStatus::FeatureGatedPilot,
),
];
let mut blockers = Vec::new();
for (backend, operator, status) in required {
if !matrix.rows.iter().any(|row| {
row.backend == backend && row.operator == operator && row.support_status == status
}) {
blockers.push(format!(
"missing support matrix row backend={backend} operator={operator} status={}",
status.as_str()
));
}
}
for row in matrix
.rows
.iter()
.filter(|row| row.backend.starts_with("rocm_hip"))
{
if row.tests.is_empty() {
blockers.push(format!(
"HIP support matrix row backend={} operator={} lacks tests",
row.backend, row.operator
));
}
if row.non_claims.is_empty() {
blockers.push(format!(
"HIP support matrix row backend={} operator={} lacks non-claims",
row.backend, row.operator
));
}
}
if blockers.is_empty() {
ReleaseGateCheck::passed(
"theory-aware support matrix",
vec![format!("rows={}", matrix.rows.len())],
)
} else {
ReleaseGateCheck::failed("theory-aware support matrix", blockers, Vec::new())
}
}
pub fn check_certified_padic_gemm_claim_gate(
matrix: &TheorySupportMatrix,
theorem_registry: &TheoremBindingRegistry,
) -> ReleaseGateCheck {
let mut blockers = Vec::new();
for theorem_id in [
PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID,
PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID,
] {
if theorem_registry.lookup(theorem_id).is_err() {
blockers.push(format!(
"certified p-adic GEMM claim missing theorem binding {theorem_id}"
));
}
}
let Some(matmul_row) = matrix.rows.iter().find(|row| {
row.backend == "rocm_hip_padic_stratified_matmul_pilot"
&& row.operator == "matmul"
&& row.support_status == SupportStatus::FeatureGatedPilot
}) else {
blockers
.push("certified p-adic GEMM claim missing ROCm/HIP matmul support row".to_string());
return ReleaseGateCheck::failed("certified p-adic GEMM claim gate", blockers, Vec::new());
};
for required in [
"dense_cpu_oracle_required",
"certified_sparse_cpu_oracle_required",
"per_output_certificate_required",
] {
if !matmul_row
.theory_constraints
.iter()
.any(|constraint| constraint == required)
{
blockers.push(format!(
"certified p-adic GEMM support row missing constraint {required}"
));
}
}
for required in [
"tests/rocm_padic_stratified_matmul.rs --features rocm-hip",
"tests/rocm_padic_stratified_benchmarks.rs --features rocm-hip",
"tests/padic_valuation_skip_theorem.rs",
] {
if !matmul_row.tests.iter().any(|test| test == required) {
blockers.push(format!(
"certified p-adic GEMM support row missing test {required}"
));
}
}
let Some(benchmark_row) = matrix.rows.iter().find(|row| {
row.backend == "rocm_hip_padic_stratified_benchmark_suite"
&& row.operator == "matmul_benchmark_matrix"
&& row.support_status == SupportStatus::FeatureGatedPilot
}) else {
blockers
.push("certified p-adic GEMM claim missing benchmark support matrix row".to_string());
return ReleaseGateCheck::failed("certified p-adic GEMM claim gate", blockers, Vec::new());
};
for required in [
"benchmark_distribution_coverage_required",
"hip_or_fallback_row_required",
"speed_claim_guard_required",
] {
if !benchmark_row
.theory_constraints
.iter()
.any(|constraint| constraint == required)
{
blockers.push(format!(
"certified p-adic GEMM benchmark row missing constraint {required}"
));
}
}
for non_claim in [
"not full p-adic algebra",
"not arbitrary precision p-adic fields",
"not portable AMD GPU support",
"not verified HIP machine code",
"not production speedup evidence",
] {
if !benchmark_row
.non_claims
.iter()
.any(|claim| claim == non_claim)
{
blockers.push(format!(
"certified p-adic GEMM benchmark row missing non-claim {non_claim}"
));
}
}
if blockers.is_empty() {
ReleaseGateCheck::passed(
"certified p-adic GEMM claim gate",
vec![
format!(
"theorems={}|{}",
PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID,
PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID
),
"dense_cpu_oracle_required".to_string(),
"certified_sparse_cpu_oracle_required".to_string(),
"per_output_certificate_required".to_string(),
"benchmark_distribution_coverage_required".to_string(),
],
)
} else {
ReleaseGateCheck::failed("certified p-adic GEMM claim gate", blockers, Vec::new())
}
}
#[cfg(feature = "rocm-hip")]
pub fn check_hip_audit_report(report: &crate::verify::HipAuditReport) -> ReleaseGateCheck {
match crate::verify::validate_hip_audit_report(report) {
Ok(()) => ReleaseGateCheck::passed(
"HIP proof and audit traces",
vec![
format!("traces={}", report.traces.len()),
"kernel_source compiler device transfer fallback cpu_oracle theory_constraints"
.to_string(),
],
),
Err(err) => ReleaseGateCheck::failed(
"HIP proof and audit traces",
vec![format!("{err}")],
vec![report.to_markdown()],
),
}
}
#[cfg(feature = "rocm-hip")]
pub fn check_padic_stratified_benchmark_report(
report: &crate::backend::hip_padic_benchmarks::PadicStratifiedBenchmarkReport,
) -> ReleaseGateCheck {
let mut blockers = Vec::new();
let required_distributions = [
"unit_heavy",
"sparse_high_valuation",
"mixed",
"adversarial_boundary",
"mixed_prime_variant",
"larger_precision_shape",
];
for distribution in required_distributions {
if !report
.fixtures
.iter()
.any(|fixture| fixture.distribution == distribution)
{
blockers.push(format!(
"p-adic stratified benchmark missing distribution {distribution}"
));
}
}
for fixture in &report.fixtures {
if !fixture
.lhs_bucket_fingerprint
.starts_with("padic-bucket-fnv64:")
|| !fixture
.rhs_bucket_fingerprint
.starts_with("padic-bucket-fnv64:")
{
blockers.push(format!(
"p-adic stratified benchmark fixture {} has stale bucket fingerprint",
fixture.name
));
}
let rows = report
.rows
.iter()
.filter(|row| row.fixture == fixture.name)
.collect::<Vec<_>>();
if !rows.iter().any(|row| {
row.backend == "dense_cpu_padic_matmul"
&& row.status == "passed"
&& row.dense_cpu_oracle_matches
}) {
blockers.push(format!(
"p-adic stratified benchmark fixture {} lacks dense CPU oracle row",
fixture.name
));
}
if !rows.iter().any(|row| {
row.backend == "certified_sparse_cpu_padic_matmul"
&& row.status == "passed"
&& row.sparse_cpu_oracle_matches
&& row.certificate_coverage
}) {
blockers.push(format!(
"p-adic stratified benchmark fixture {} lacks certified sparse CPU oracle row",
fixture.name
));
}
if !rows.iter().any(|row| {
row.backend == "rocm_hip_padic_stratified_matmul_pilot"
&& ((row.status == "passed"
&& row.dense_cpu_oracle_matches
&& row.sparse_cpu_oracle_matches
&& row.certificate_coverage
&& row.transfer_time_ns > 0
&& row.kernel_time_ns > 0)
|| (row.status == "fallback_captured"
&& row.fallback_reason.contains("unsupported")
&& row.certificate_coverage))
}) {
blockers.push(format!(
"p-adic stratified benchmark fixture {} lacks HIP oracle or closed fallback row",
fixture.name
));
}
}
if !report
.non_claims
.iter()
.any(|claim| claim.contains("work reduction is reported separately"))
{
blockers.push("p-adic stratified benchmark report lacks speed non-claim".to_string());
}
if let Err(err) =
crate::backend::hip_padic_benchmarks::validate_padic_stratified_speed_claims(report)
{
blockers.push(format!("{err}"));
}
if blockers.is_empty() {
ReleaseGateCheck::passed(
"Certified p-adic GEMM benchmark matrix",
vec![
format!("fixtures={}", report.fixtures.len()),
format!("rows={}", report.rows.len()),
format!(
"hip_passed_rows={}",
report
.rows
.iter()
.filter(|row| {
row.backend == "rocm_hip_padic_stratified_matmul_pilot"
&& row.status == "passed"
})
.count()
),
format!(
"fallback_rows={}",
report
.rows
.iter()
.filter(|row| row.status == "fallback_captured")
.count()
),
],
)
} else {
ReleaseGateCheck::failed(
"Certified p-adic GEMM benchmark matrix",
blockers,
vec![report.to_markdown()],
)
}
}
fn check_facade_examples(evidence: &[String]) -> ReleaseGateCheck {
let required = [
"facade p-adic CPU plan",
"facade p-adic GPU fallback",
"facade strict GPU rejection",
"facade sheaf CPU plan",
];
let blockers = required
.iter()
.filter(|required| !evidence.iter().any(|entry| entry.contains(*required)))
.map(|missing| format!("missing {missing}"))
.collect::<Vec<_>>();
if blockers.is_empty() {
ReleaseGateCheck::passed("facade examples", evidence.to_vec())
} else {
ReleaseGateCheck::failed("facade examples", blockers, evidence.to_vec())
}
}
fn check_known_limit_coverage(matrix: &TheorySupportMatrix) -> ReleaseGateCheck {
let matrix_text = matrix.to_markdown();
let required = [
"not full p-adic algebra",
"not general sheaf theory",
"not p-adic or finite-site sheaf acceleration",
"not production performance evidence",
"not portable AMD GPU support",
];
let blockers = required
.iter()
.filter(|required| !matrix_text.contains(*required))
.map(|missing| format!("support matrix missing non-claim: {missing}"))
.collect::<Vec<_>>();
if blockers.is_empty() {
ReleaseGateCheck::passed(
"known limits and non-claims",
required.map(str::to_string).to_vec(),
)
} else {
ReleaseGateCheck::failed("known limits and non-claims", blockers, Vec::new())
}
}
fn facade_gate_evidence(q5: &crate::domain::PadicDomain, cover: &Cover) -> Result<Vec<String>> {
let cpu = Tokitai::cpu_only();
let padic_cpu = cpu.plan_padic_sum_products(q5, 0, 1, 2)?;
validate_theory_evidence(
&padic_valuation_cutoff_theory_evidence(&padic_cpu.plan)?,
&["valuation_skip_sound_mod_pk"],
&["PadicPlanningResource"],
)?;
let prefer_gpu = Tokitai::prefer_gpu_with_cpu_fallback();
let padic_fallback = prefer_gpu.plan_padic_sum_products(q5, 0, 1, 2)?;
let strict_rejection = Tokitai::strict_gpu()
.plan_padic_sum_products(q5, 0, 1, 2)
.unwrap_err()
.to_string();
let sheaf_cpu = cpu.plan_sheaf_glue_check(cover)?;
Ok(vec![
format!(
"facade p-adic CPU plan selected={:?}",
padic_cpu.selected_target.kind
),
format!(
"facade p-adic GPU fallback selected={:?} reason={}",
padic_fallback.selected_target.kind,
padic_fallback.fallback_reason.as_deref().unwrap_or("none")
),
format!("facade strict GPU rejection: {strict_rejection}"),
format!(
"facade sheaf CPU plan selected={:?} steps={}",
sheaf_cpu.selected_target.kind,
sheaf_cpu.plan.steps.len()
),
])
}
fn release_sheaf_fixture() -> (FiniteSite, Cover) {
let site = FiniteSite::new(
vec![open("U"), open("A"), open("B"), open("A_cap_B")],
vec![
Inclusion::new("A", "U"),
Inclusion::new("B", "U"),
Inclusion::new("A_cap_B", "A"),
Inclusion::new("A_cap_B", "B"),
Inclusion::new("A_cap_B", "U"),
],
)
.with_intersection(open("A"), open("B"), open("A_cap_B"));
(site, Cover::new("U", ["A", "B"]))
}
fn open(id: &str) -> OpenId {
OpenId(id.to_string())
}
fn md(value: &str) -> String {
value.replace('|', "\\|")
}
fn json_array(values: &[String]) -> String {
format!(
"[{}]",
values
.iter()
.map(|value| json_string(value))
.collect::<Vec<_>>()
.join(",")
)
}
fn json_string(value: &str) -> String {
let mut escaped = String::from("\"");
for ch in value.chars() {
match ch {
'"' => escaped.push_str("\\\""),
'\\' => escaped.push_str("\\\\"),
'\n' => escaped.push_str("\\n"),
'\r' => escaped.push_str("\\r"),
'\t' => escaped.push_str("\\t"),
ch if ch.is_control() => escaped.push_str(&format!("\\u{:04x}", ch as u32)),
ch => escaped.push(ch),
}
}
escaped.push('"');
escaped
}