use std::collections::hash_map::DefaultHasher;
use std::fs;
use std::hash::{Hash, Hasher};
use std::path::PathBuf;
use std::process::Command;
use crate::backend::BackendCapabilities;
use crate::backend::hip_dense::{
hipcc_compile_executable, hipcc_compiler_fingerprint, hipcc_recheck_artifact,
};
use crate::backend::rocm::{RocmHipCapabilityReport, detect_local_rocm_hip};
use crate::domain::PadicDomain;
use crate::object::Representation;
use crate::op::{LoweringCapability, LoweringEvidenceKind, LoweringRule, OperatorRegistry};
use crate::planner::HeuristicPlanner;
use crate::theory::padic_valuation_cutoff_theory_evidence;
use crate::{Error, Result};
pub const ROCM_HIP_PADIC_VALUATION_BACKEND: &str = "rocm_hip_padic_valuation_pilot";
pub const ROCM_HIP_PADIC_VALUATION_LOWERING_ID: &str = "hip.padic_sum_products_valuation";
pub const HIP_PADIC_VALUATION_KERNEL: &str = r#"
#include <hip/hip_runtime.h>
#include <cstdint>
#include <cstdlib>
#include <iostream>
#include <string>
#include <vector>
__global__ void padic_valuation_kernel(const unsigned long long* residues, unsigned int* out, unsigned long long prime, unsigned int precision, std::size_t n) {
std::size_t idx = blockIdx.x * blockDim.x + threadIdx.x;
if (idx >= n) {
return;
}
unsigned long long value = residues[idx];
if (value == 0) {
out[idx] = precision;
return;
}
unsigned int valuation = 0;
while (valuation < precision && value % prime == 0) {
valuation += 1;
value /= prime;
}
out[idx] = valuation;
}
static void check(hipError_t status, const char* label) {
if (status != hipSuccess) {
std::cerr << "HIP_ERROR " << label << "=" << hipGetErrorString(status) << "\n";
std::exit(10);
}
}
int main(int argc, char** argv) {
if (argc < 4) {
std::cerr << "usage: rocm_padic_valuation PRIME PRECISION N RESIDUES...\n";
return 2;
}
unsigned long long prime = std::stoull(argv[1]);
unsigned int precision = static_cast<unsigned int>(std::stoul(argv[2]));
std::size_t n = static_cast<std::size_t>(std::stoul(argv[3]));
if (argc != static_cast<int>(4 + n)) {
std::cerr << "argument count does not match N\n";
return 3;
}
int device = 0;
check(hipSetDevice(device), "hipSetDevice");
std::vector<unsigned long long> residues(n);
std::vector<unsigned int> out(n);
for (std::size_t i = 0; i < n; ++i) {
residues[i] = std::stoull(argv[4 + i]);
}
unsigned long long* d_residues = nullptr;
unsigned int* d_out = nullptr;
std::size_t input_bytes = n * sizeof(unsigned long long);
std::size_t output_bytes = n * sizeof(unsigned int);
check(hipMalloc(&d_residues, input_bytes), "hipMalloc(residues)");
check(hipMalloc(&d_out, output_bytes), "hipMalloc(out)");
check(hipMemcpy(d_residues, residues.data(), input_bytes, hipMemcpyHostToDevice), "hipMemcpy(residues)");
int block = 256;
int grid = static_cast<int>((n + block - 1) / block);
hipLaunchKernelGGL(padic_valuation_kernel, dim3(grid), dim3(block), 0, 0, d_residues, d_out, prime, precision, n);
check(hipGetLastError(), "hipLaunchKernelGGL");
check(hipDeviceSynchronize(), "hipDeviceSynchronize");
check(hipMemcpy(out.data(), d_out, output_bytes, hipMemcpyDeviceToHost), "hipMemcpy(out)");
check(hipFree(d_residues), "hipFree(residues)");
check(hipFree(d_out), "hipFree(out)");
std::cout << "PRIME=" << prime << "\n";
std::cout << "PRECISION=" << precision << "\n";
std::cout << "N=" << n << "\n";
std::cout << "GRID=" << grid << "\n";
std::cout << "BLOCK=" << block << "\n";
std::cout << "VALUATIONS=";
for (std::size_t i = 0; i < out.size(); ++i) {
if (i != 0) {
std::cout << ",";
}
std::cout << out[i];
}
std::cout << "\n";
return 0;
}
"#;
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct RocmHipPadicValuationReport {
pub backend: String,
pub prime: u64,
pub precision: u32,
pub residues: Vec<u64>,
pub valuations: Vec<u32>,
pub cpu_oracle_valuations: Vec<u32>,
pub cpu_oracle_matches: bool,
pub kernel_source_fingerprint: String,
pub compiler_fingerprint: String,
pub launch_grid: u32,
pub launch_block: u32,
pub device_evidence: RocmHipCapabilityReport,
pub theorem_evidence: Vec<String>,
pub evidence: Vec<String>,
pub non_claims: Vec<String>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct RocmHipPadicValuationLoweringContract {
pub required_gfx: String,
pub device_capability_fingerprint: String,
pub kernel_source_fingerprint: String,
pub compiler_fingerprint: String,
}
impl RocmHipPadicValuationLoweringContract {
pub fn from_report(
report: &RocmHipCapabilityReport,
compiler_fingerprint: impl Into<String>,
) -> Result<Self> {
let selected = report.selected_device.as_ref().ok_or_else(|| {
Error::backend(
"ROCm/HIP p-adic valuation lowering admission requires a selected device",
)
})?;
Ok(Self {
required_gfx: selected.gfx.clone(),
device_capability_fingerprint: report.capability_fingerprint.clone(),
kernel_source_fingerprint: hip_padic_valuation_kernel_source_fingerprint(),
compiler_fingerprint: compiler_fingerprint.into(),
})
}
pub fn lowering_rule(&self) -> LoweringRule {
LoweringRule::new(
ROCM_HIP_PADIC_VALUATION_LOWERING_ID,
"padic_sum_products_valuation_skip",
ROCM_HIP_PADIC_VALUATION_BACKEND,
vec![Representation::PadicScalar.id().0],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::rocm_hip_padic_valuation(
self.required_gfx.clone(),
self.device_capability_fingerprint.clone(),
self.kernel_source_fingerprint.clone(),
self.compiler_fingerprint.clone(),
))
.with_required_evidence(
LoweringEvidenceKind::ValuationCutoff,
"HIP p-adic valuation helper computes runtime valuations against the active precision cutoff",
)
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"HIP p-adic valuation helper output must match PadicDomain::valuation_of before valuation-skip execution is admitted",
)
.with_obligation(
"all residues must be normalized modulo p^N before HIP valuation",
"the kernel computes truncated valuations for fixed-precision residues only",
)
.with_obligation(
"HIP valuation output must be copied back and checked against the CPU oracle",
"PadicDomain::valuation_of remains the semantic authority for this feature-gated lowering",
)
.with_theory_requirement(crate::theory::CertifiedTheoryRequirement::padic_valuation_skip())
}
}
impl RocmHipPadicValuationReport {
pub fn to_markdown(&self) -> String {
let mut lines = vec![
"# ROCm/HIP p-adic Valuation Pilot".to_string(),
String::new(),
format!("backend: {}", self.backend),
format!("prime: {}", self.prime),
format!("precision: {}", self.precision),
format!("len: {}", self.residues.len()),
format!("cpu_oracle_matches: {}", self.cpu_oracle_matches),
format!(
"kernel_source_fingerprint: {}",
self.kernel_source_fingerprint
),
format!("compiler_fingerprint: {}", self.compiler_fingerprint),
format!("launch_grid: {}", self.launch_grid),
format!("launch_block: {}", self.launch_block),
String::new(),
"## Theorem Evidence".to_string(),
];
for item in &self.theorem_evidence {
lines.push(format!("- {item}"));
}
lines.push(String::new());
lines.push("## Evidence".to_string());
for item in &self.evidence {
lines.push(format!("- {item}"));
}
lines.push(String::new());
lines.push("## Non-Claims".to_string());
for item in &self.non_claims {
lines.push(format!("- {item}"));
}
lines.join("\n")
}
}
pub fn run_rocm_hip_padic_valuation(
domain: &PadicDomain,
residues: &[u64],
) -> Result<RocmHipPadicValuationReport> {
if residues.is_empty() {
return Err(Error::backend(
"HIP p-adic valuation pilot requires non-empty residues",
));
}
let modulus = domain.modulus() as u64;
let normalized = residues
.iter()
.map(|value| value % modulus)
.collect::<Vec<_>>();
let cpu_oracle_valuations = normalized
.iter()
.map(|value| {
domain
.valuation_of(&domain.element(u128::from(*value)))
.map(|valuation| valuation.unwrap_or(domain.meta.precision))
})
.collect::<Result<Vec<_>>>()?;
let device_evidence = detect_local_rocm_hip();
if !device_evidence.available {
return Err(Error::backend(
"ROCm/HIP is unavailable; p-adic valuation HIP pilot remains inadmissible",
));
}
let source_fingerprint = hip_padic_valuation_kernel_source_fingerprint();
let compiler_fingerprint = hipcc_compiler_fingerprint("/opt/rocm/bin/hipcc")?;
let cache_dir = PathBuf::from("target/rocm-hip-cache");
fs::create_dir_all(&cache_dir)
.map_err(|err| Error::backend(format!("failed to create HIP cache directory: {err}")))?;
let source_path = cache_dir.join(format!("{source_fingerprint}.cpp"));
let executable_path = cache_dir.join(format!("{source_fingerprint}-padic-valuation"));
fs::write(&source_path, HIP_PADIC_VALUATION_KERNEL)
.map_err(|err| Error::backend(format!("failed to write HIP p-adic source: {err}")))?;
hipcc_compile_executable("/opt/rocm/bin/hipcc", &source_path, &executable_path, None)?;
let mut args = vec![
domain.meta.prime.to_string(),
domain.meta.precision.to_string(),
normalized.len().to_string(),
];
args.extend(normalized.iter().map(u64::to_string));
hipcc_recheck_artifact("/opt/rocm/bin/hipcc", &source_path, &executable_path, None)?;
let run = Command::new(&executable_path)
.args(args)
.output()
.map_err(|err| {
Error::backend(format!("failed to run HIP p-adic valuation pilot: {err}"))
})?;
if !run.status.success() {
return Err(Error::backend(format!(
"HIP p-adic valuation pilot failed: {}{}",
String::from_utf8_lossy(&run.stderr),
String::from_utf8_lossy(&run.stdout)
)));
}
let stdout = String::from_utf8_lossy(&run.stdout);
let valuations = parse_valuations(&stdout)?;
let launch_grid = parse_u32_line(&stdout, "GRID=").unwrap_or(0);
let launch_block = parse_u32_line(&stdout, "BLOCK=").unwrap_or(0);
let cpu_oracle_matches = valuations == cpu_oracle_valuations;
if !cpu_oracle_matches {
return Err(Error::backend(format!(
"HIP p-adic valuation pilot failed CPU oracle comparison hip={valuations:?} cpu={cpu_oracle_valuations:?}"
)));
}
let compiler_for_contract = compiler_fingerprint.clone();
let contract = RocmHipPadicValuationLoweringContract::from_report(
&device_evidence,
compiler_for_contract,
)?;
let backend_capabilities = rocm_hip_padic_valuation_backend_capabilities(&contract);
let planner = HeuristicPlanner::new(backend_capabilities);
let mut registry = OperatorRegistry::cpu_scalar_builtins()?;
register_rocm_hip_padic_valuation_lowering(&mut registry, &contract)?;
let theorem_plan =
planner.plan_padic_sum_products_skip_with_registry(domain, 0, 1, 2, ®istry);
let theorem = padic_valuation_cutoff_theory_evidence(&theorem_plan)?;
Ok(RocmHipPadicValuationReport {
backend: ROCM_HIP_PADIC_VALUATION_BACKEND.to_string(),
prime: domain.meta.prime,
precision: domain.meta.precision,
residues: normalized,
valuations,
cpu_oracle_valuations,
cpu_oracle_matches,
kernel_source_fingerprint: source_fingerprint,
compiler_fingerprint,
launch_grid,
launch_block,
device_evidence,
theorem_evidence: vec![
format!("theory={}", theorem.theory.as_str()),
format!(
"laws={}",
theorem
.law_witnesses
.iter()
.map(|witness| witness.law_id.as_str())
.collect::<Vec<_>>()
.join("|")
),
format!("theorem_bindings={}", theorem.assumption_bindings.len()),
format!("valuation_cutoff={}", domain.meta.precision),
],
evidence: vec![
"compiled p-adic valuation HIP helper with /opt/rocm/bin/hipcc".to_string(),
format!(
"planner selected lowering {} for backend {}",
ROCM_HIP_PADIC_VALUATION_LOWERING_ID, ROCM_HIP_PADIC_VALUATION_BACKEND
),
"zero residue maps to the active precision cutoff for skip decisions".to_string(),
"compared every valuation with PadicDomain::valuation_of CPU oracle".to_string(),
],
non_claims: vec![
"not full p-adic algebra".to_string(),
"not arbitrary precision p-adic fields".to_string(),
"not broad p-adic GPU acceleration".to_string(),
"not production performance evidence".to_string(),
],
})
}
pub fn hip_padic_valuation_kernel_source_fingerprint() -> String {
fingerprint("hip-padic-valuation-source", HIP_PADIC_VALUATION_KERNEL)
}
pub fn rocm_hip_padic_valuation_backend_capabilities(
contract: &RocmHipPadicValuationLoweringContract,
) -> BackendCapabilities {
BackendCapabilities {
name: ROCM_HIP_PADIC_VALUATION_BACKEND.to_string(),
exact: true,
deterministic: true,
supported_representations: vec![Representation::PadicScalar.id().0],
supported_domains: vec![
"padic:fixed_precision".to_string(),
"rocm:hip".to_string(),
format!("gfx:{}", contract.required_gfx),
format!(
"device_capability:{}",
contract.device_capability_fingerprint
),
format!("hip_kernel_source:{}", contract.kernel_source_fingerprint),
format!("hip_compiler:{}", contract.compiler_fingerprint),
"cpu_oracle:required".to_string(),
],
semantic_degradations: vec![
"feature_gated:rocm-hip".to_string(),
"scope:padic_valuation_vector".to_string(),
"transfer_obligation:host_to_device_padic_residues".to_string(),
"transfer_obligation:device_to_host_valuations".to_string(),
"unsupported:full_padic_algebra".to_string(),
"unsupported:arbitrary_precision".to_string(),
],
}
}
pub fn register_rocm_hip_padic_valuation_lowering(
registry: &mut OperatorRegistry,
contract: &RocmHipPadicValuationLoweringContract,
) -> Result<()> {
registry.register_lowering(contract.lowering_rule())
}
fn parse_valuations(stdout: &str) -> Result<Vec<u32>> {
let line = stdout
.lines()
.find_map(|line| line.strip_prefix("VALUATIONS="))
.ok_or_else(|| Error::backend("HIP p-adic valuation pilot did not print VALUATIONS"))?;
if line.trim().is_empty() {
return Ok(Vec::new());
}
line.split(',')
.map(|value| {
value.trim().parse::<u32>().map_err(|err| {
Error::backend(format!("invalid HIP p-adic valuation {value}: {err}"))
})
})
.collect()
}
fn parse_u32_line(stdout: &str, prefix: &str) -> Option<u32> {
stdout
.lines()
.find_map(|line| line.strip_prefix(prefix))
.and_then(|value| value.trim().parse::<u32>().ok())
}
fn fingerprint(label: &str, value: &str) -> String {
let mut hasher = DefaultHasher::new();
label.hash(&mut hasher);
value.hash(&mut hasher);
format!("{label}-{:016x}", hasher.finish())
}