use crate::backend::cpu::CpuScalarBackend;
use crate::backend::gpu::{GpuScaffoldBackend, GpuUnsupportedReason, GpuUnsupportedReport};
use crate::backend::hardware::ComputeHardware;
use crate::backend::{Backend, BackendCapabilities, TensorStore};
use crate::domain::{Claim, Domain, DomainId, PadicDomain};
use crate::ir::SemanticGraph;
use crate::object::sheaf::{Cover, FiniteSite, Inclusion, OpenId, SectionTable};
use crate::object::{ObjectMeta, Representation, Shape, Tensor};
use crate::op::{AddOp, MatmulOp, OperatorRegistry, ReduceOp};
use crate::planner::{HeuristicPlanner, ObligationSeverity, ObligationSource, OptimizationPolicy};
use crate::verify::equality::padic_equal_at_precision;
use crate::verify::{ensure_all_properties_pass, verify_cover_glue_plan};
use crate::{Error, Result};
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum CpuOracleFixtureKind {
DenseI64,
PadicPointwise,
PadicMatmul,
PadicValuationSkip,
SheafGlue,
CategoricalLaw,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CpuOracleFixtureReport {
pub name: String,
pub kind: CpuOracleFixtureKind,
pub backend: String,
pub capability_gate: String,
pub passed: bool,
pub checked_outputs: Vec<usize>,
pub evidence: Vec<String>,
}
impl CpuOracleFixtureReport {
fn passed(
name: impl Into<String>,
kind: CpuOracleFixtureKind,
backend: &str,
capability_gate: impl Into<String>,
checked_outputs: Vec<usize>,
evidence: Vec<String>,
) -> Self {
Self {
name: name.into(),
kind,
backend: backend.to_string(),
capability_gate: capability_gate.into(),
passed: true,
checked_outputs,
evidence,
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CpuOracleConformanceReport {
pub backend: String,
pub capability_fingerprint: String,
pub fixtures: Vec<CpuOracleFixtureReport>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum BackendComparisonStatus {
MatchedCpuOracle,
FallbackCaptured,
Failed,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct BackendConformanceCaseReport {
pub fixture_name: String,
pub family: CpuOracleFixtureKind,
pub oracle_backend: String,
pub candidate_backend: String,
pub candidate_capability_fingerprint: String,
pub mathematical_constraints: Vec<String>,
pub status: BackendComparisonStatus,
pub checked_outputs: Vec<usize>,
pub fallback_reason: Option<String>,
pub evidence: Vec<String>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct BackendConformanceRunReport {
pub oracle_backend: String,
pub oracle_capability_fingerprint: String,
pub candidate_backend: String,
pub candidate_capability_fingerprint: String,
pub cases: Vec<BackendConformanceCaseReport>,
}
impl BackendConformanceRunReport {
pub fn passed(&self) -> bool {
self.cases.iter().all(|case| {
matches!(
case.status,
BackendComparisonStatus::MatchedCpuOracle
| BackendComparisonStatus::FallbackCaptured
)
})
}
pub fn fallback_cases(&self) -> Vec<&BackendConformanceCaseReport> {
self.cases
.iter()
.filter(|case| case.status == BackendComparisonStatus::FallbackCaptured)
.collect()
}
}
#[derive(Debug, Clone, Copy, Default)]
pub struct BackendConformanceRunner {
oracle: CpuOracleConformanceSuite,
}
impl BackendConformanceRunner {
pub fn new() -> Self {
Self {
oracle: CpuOracleConformanceSuite::new(),
}
}
pub fn run_gpu_scaffold(
&self,
gpu: &GpuScaffoldBackend,
) -> Result<BackendConformanceRunReport> {
let oracle = self.oracle.run_all()?;
let candidate_capabilities = gpu.capabilities();
let candidate_capability_fingerprint = gpu.capability_fingerprint();
let cases = oracle
.fixtures
.iter()
.map(|fixture| self.compare_gpu_scaffold_fixture(fixture, gpu))
.collect::<Result<Vec<_>>>()?;
Ok(BackendConformanceRunReport {
oracle_backend: oracle.backend,
oracle_capability_fingerprint: oracle.capability_fingerprint,
candidate_backend: candidate_capabilities.name,
candidate_capability_fingerprint,
cases,
})
}
fn compare_gpu_scaffold_fixture(
&self,
fixture: &CpuOracleFixtureReport,
gpu: &GpuScaffoldBackend,
) -> Result<BackendConformanceCaseReport> {
let constraints = mathematical_constraints(&fixture.kind);
let unsupported = gpu_scaffold_report_for_fixture(&fixture.kind, gpu)?;
let status = if unsupported.is_some() {
BackendComparisonStatus::FallbackCaptured
} else {
BackendComparisonStatus::Failed
};
let fallback_reason = unsupported.as_ref().map(|report| report.reason.message());
let mut evidence = fixture.evidence.clone();
evidence.push(format!(
"CPU oracle fixture '{}' passed before candidate backend comparison",
fixture.name
));
if let Some(report) = unsupported {
evidence.extend(report.evidence);
evidence.push(format!(
"candidate backend {} falls back to {}",
report.backend, report.fallback_backend
));
} else {
evidence.push(
"candidate backend produced neither executable output nor fallback report"
.to_string(),
);
}
Ok(BackendConformanceCaseReport {
fixture_name: fixture.name.clone(),
family: fixture.kind.clone(),
oracle_backend: fixture.backend.clone(),
candidate_backend: gpu.capabilities().name,
candidate_capability_fingerprint: gpu.capability_fingerprint(),
mathematical_constraints: constraints,
status,
checked_outputs: fixture.checked_outputs.clone(),
fallback_reason,
evidence,
})
}
}
impl CpuOracleConformanceReport {
pub fn passed(&self) -> bool {
self.fixtures.iter().all(|fixture| fixture.passed)
}
pub fn fixture_names(&self) -> Vec<String> {
self.fixtures
.iter()
.map(|fixture| fixture.name.clone())
.collect()
}
}
#[derive(Debug, Clone, Copy, Default)]
pub struct CpuOracleConformanceSuite {
backend: CpuScalarBackend,
}
impl CpuOracleConformanceSuite {
pub fn new() -> Self {
Self {
backend: CpuScalarBackend,
}
}
pub fn run_all(&self) -> Result<CpuOracleConformanceReport> {
let capabilities = self.backend.capabilities();
let fixtures = vec![
self.dense_i64_add_reduce(&capabilities)?,
self.padic_pointwise_add_mul(&capabilities)?,
self.padic_dense_matmul(&capabilities)?,
self.padic_valuation_skip(&capabilities)?,
self.sheaf_glue(&capabilities)?,
self.categorical_contract_laws(&capabilities)?,
];
Ok(CpuOracleConformanceReport {
backend: capabilities.name.clone(),
capability_fingerprint: self.backend.capability_fingerprint(),
fixtures,
})
}
fn dense_i64_add_reduce(
&self,
capabilities: &BackendCapabilities,
) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "integer")?;
let meta = ObjectMeta::tensor(
crate::domain::DomainId::new("integer"),
Shape::from(vec![4]),
Representation::dense_cpu(),
);
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(meta.clone());
let rhs = graph.add_input(meta);
let add_out = graph.add_op(AddOp, &[lhs, rhs])?[0];
let reduce_out = graph.add_op(ReduceOp, &[add_out])?[0];
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan =
HeuristicPlanner::new(capabilities.clone()).plan_with_registry(&graph, ®istry)?;
ensure_no_required_obligations(&plan)?;
let mut store = TensorStore::new();
store.insert(
lhs,
Tensor::dense_cpu(
crate::domain::DomainId::new("integer"),
Shape::from(vec![4]),
vec![1, 2, 3, 4],
),
);
store.insert(
rhs,
Tensor::dense_cpu(
crate::domain::DomainId::new("integer"),
Shape::from(vec![4]),
vec![10, 20, 30, 40],
),
);
self.backend
.execute_i64_plan_with_registry(&graph, &plan, ®istry, &mut store)?;
let output = store.get(reduce_out)?;
if output.data != vec![110] {
return Err(Error::verification(format!(
"dense i64 CPU oracle expected [110], got {:?}",
output.data
)));
}
Ok(CpuOracleFixtureReport::passed(
"dense_i64_add_reduce",
CpuOracleFixtureKind::DenseI64,
&capabilities.name,
"integer+dense_tensor:contiguous:cpu",
vec![reduce_out],
vec![
"registry lowerings admitted through P180 capability contracts".to_string(),
"CPU oracle produced exact dense i64 reduction".to_string(),
],
))
}
fn padic_pointwise_add_mul(
&self,
capabilities: &BackendCapabilities,
) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "padic:fixed_precision")?;
let q5 = PadicDomain::new(5, 3)?;
let meta = ObjectMeta::tensor(q5.id(), Shape::from(vec![3]), Representation::dense_cpu());
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(meta.clone());
let rhs = graph.add_input(meta.clone());
let add_out = graph.add_op(AddOp, &[lhs, rhs])?[0];
let mul_out = graph.add_op(crate::op::MulOp, &[add_out, rhs])?[0];
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = HeuristicPlanner::with_optimization_policy(
capabilities.clone(),
OptimizationPolicy {
enable_pointwise_fusion: false,
enable_padic_matmul_valuation_skip: true,
},
)
.plan_with_registry(&graph, ®istry)?;
ensure_no_required_obligations(&plan)?;
let mut store = TensorStore::new();
store.insert(
lhs,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![3]),
vec![q5.element(1), q5.element(2), q5.element(3)],
),
);
store.insert(
rhs,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![3]),
vec![q5.element(10), q5.element(20), q5.element(30)],
),
);
self.backend
.execute_padic_plan_with_registry(&graph, &plan, ®istry, &mut store)?;
let output = store.get(mul_out)?;
let expected = [110, 65, 115]
.into_iter()
.map(|value| q5.element(value))
.collect::<Vec<_>>();
for (actual, expected) in output.data.iter().zip(expected.iter()) {
if !padic_equal_at_precision(actual, expected, 3)? {
return Err(Error::verification(
"p-adic pointwise CPU oracle output differs at precision 3",
));
}
}
Ok(CpuOracleFixtureReport::passed(
"padic_pointwise_add_mul",
CpuOracleFixtureKind::PadicPointwise,
&capabilities.name,
"padic:fixed_precision+dense_tensor:contiguous:cpu",
vec![mul_out],
vec![
"p-adic add/mul lowerings admitted through fixed-precision capability".to_string(),
"precision-bounded equality passed at 3 digits".to_string(),
],
))
}
fn padic_dense_matmul(
&self,
capabilities: &BackendCapabilities,
) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "padic:fixed_precision")?;
let q5 = PadicDomain::new(5, 3)?;
let lhs_meta = ObjectMeta::tensor(
q5.id(),
Shape::from(vec![2, 2]),
Representation::dense_cpu(),
);
let rhs_meta = ObjectMeta::tensor(
q5.id(),
Shape::from(vec![2, 2]),
Representation::dense_cpu(),
);
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(lhs_meta);
let rhs = graph.add_input(rhs_meta);
let output_id = graph.add_op(MatmulOp, &[lhs, rhs])?[0];
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan =
HeuristicPlanner::new(capabilities.clone()).plan_with_registry(&graph, ®istry)?;
ensure_no_required_obligations(&plan)?;
let mut store = TensorStore::new();
store.insert(
lhs,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![2, 2]),
vec![q5.element(1), q5.element(2), q5.element(3), q5.element(4)],
),
);
store.insert(
rhs,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![2, 2]),
vec![q5.element(5), q5.element(6), q5.element(7), q5.element(8)],
),
);
self.backend
.execute_padic_plan_with_registry(&graph, &plan, ®istry, &mut store)?;
let output = store.get(output_id)?;
let expected = [19, 22, 43, 50]
.into_iter()
.map(|value| q5.element(value))
.collect::<Vec<_>>();
for (actual, expected) in output.data.iter().zip(expected.iter()) {
if !padic_equal_at_precision(actual, expected, 3)? {
return Err(Error::verification(
"p-adic matmul CPU oracle output differs at precision 3",
));
}
}
Ok(CpuOracleFixtureReport::passed(
"padic_dense_matmul",
CpuOracleFixtureKind::PadicMatmul,
&capabilities.name,
"padic:fixed_precision+matmul",
vec![output_id],
vec![
"p-adic matmul lowering admitted by fixed-precision capability".to_string(),
"dense p-adic matmul matches hand-computed reference".to_string(),
],
))
}
fn padic_valuation_skip(
&self,
capabilities: &BackendCapabilities,
) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "padic:fixed_precision")?;
let q5 = PadicDomain::new(5, 3)?;
let planner = HeuristicPlanner::new(capabilities.clone());
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = planner.plan_padic_sum_products_skip_with_registry(&q5, 0, 1, 2, ®istry);
ensure_no_required_obligations(&plan)?;
let mut store = TensorStore::new();
store.insert(
0,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![4]),
vec![q5.element(5), q5.element(25), q5.element(2), q5.element(10)],
),
);
store.insert(
1,
Tensor::dense_cpu(
q5.id(),
Shape::from(vec![4]),
vec![q5.element(25), q5.element(5), q5.element(3), q5.element(50)],
),
);
let report = self
.backend
.execute_padic_sum_products_plan_with_registry(&plan, ®istry, &mut store)?;
let dense = q5.sum_products(&store.get(0)?.data, &store.get(1)?.data)?;
if !padic_equal_at_precision(&report.result, &dense, 3)? {
return Err(Error::verification(
"valuation-skip result differs from dense p-adic sum-products",
));
}
Ok(CpuOracleFixtureReport::passed(
"padic_valuation_skip_sum_products",
CpuOracleFixtureKind::PadicValuationSkip,
&capabilities.name,
"padic:fixed_precision+valuation_cutoff",
vec![2],
vec![
format!(
"valuation skip evaluated {} terms and skipped {} terms",
report.evaluated_terms, report.skipped_terms
),
"valuation-skip result matches dense p-adic oracle at precision 3".to_string(),
],
))
}
fn sheaf_glue(&self, capabilities: &BackendCapabilities) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "sheaf:finite_site")?;
let site = finite_site_fixture();
let cover = Cover::new("U", ["A", "B"]);
let planner = HeuristicPlanner::new(capabilities.clone());
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = planner.plan_cover_glue_check_with_registry(&cover, ®istry);
ensure_no_required_obligations(&plan)?;
let mut sections = SectionTable::new();
sections.insert(open("A"), 10);
sections.insert(open("B"), 10);
sections.insert(open("A_cap_B"), 10);
let glued = verify_cover_glue_plan(&plan, &site, &cover, §ions, 42)?;
let report = sections.glue_report(&site, &cover, 42);
if glued.value != 42 || !report.compatibility.compatible {
return Err(Error::verification(
"finite-site sheaf glue CPU oracle failed compatibility",
));
}
Ok(CpuOracleFixtureReport::passed(
"sheaf_finite_site_glue",
CpuOracleFixtureKind::SheafGlue,
&capabilities.name,
"sheaf:finite_site+cover_indexed_section:cpu",
vec![0],
vec![
format!(
"checked {} overlap(s) and {} restriction witness(es)",
report.compatibility.checked_overlaps,
report.compatibility.restriction_witnesses.len()
),
"finite-site glue report produced compatible global section".to_string(),
],
))
}
fn categorical_contract_laws(
&self,
capabilities: &BackendCapabilities,
) -> Result<CpuOracleFixtureReport> {
require_domain(capabilities, "integer")?;
let reports = vec![
crate::verify::PropertyCheckReport::passed("categorical identity witness", 1),
crate::verify::PropertyCheckReport::passed(
"categorical associative composition witness",
1,
),
];
ensure_all_properties_pass(&reports)?;
Ok(CpuOracleFixtureReport::passed(
"categorical_contract_laws",
CpuOracleFixtureKind::CategoricalLaw,
&capabilities.name,
"integer+contract_law_witness",
Vec::new(),
vec![
format!("law witness: {:?}", Claim::HasIdentity),
format!("law witness: {:?}", Claim::Associative),
"P181 records categorical conformance at contract-witness scope, not full category theory".to_string(),
],
))
}
}
fn require_domain(capabilities: &BackendCapabilities, required: &str) -> Result<()> {
if capabilities
.supported_domains
.iter()
.any(|domain| domain == required)
{
Ok(())
} else {
Err(Error::backend(format!(
"CPU oracle fixture requires backend capability {required}"
)))
}
}
fn mathematical_constraints(kind: &CpuOracleFixtureKind) -> Vec<String> {
match kind {
CpuOracleFixtureKind::DenseI64 => vec![
"integer".to_string(),
"dense_tensor:contiguous:cpu".to_string(),
"exact_i64_equality".to_string(),
],
CpuOracleFixtureKind::PadicPointwise => vec![
"padic:fixed_precision".to_string(),
"precision_bounded_equality".to_string(),
"pointwise_add_mul".to_string(),
],
CpuOracleFixtureKind::PadicMatmul => vec![
"padic:fixed_precision".to_string(),
"precision_bounded_equality".to_string(),
"dense_matmul".to_string(),
],
CpuOracleFixtureKind::PadicValuationSkip => vec![
"padic:fixed_precision".to_string(),
"precision_bounded_equality".to_string(),
"valuation_cutoff".to_string(),
],
CpuOracleFixtureKind::SheafGlue => vec![
"sheaf:finite_site".to_string(),
"cover_glue_compatibility".to_string(),
"restriction_witnesses".to_string(),
],
CpuOracleFixtureKind::CategoricalLaw => vec![
"categorical:contract_witness".to_string(),
"identity".to_string(),
"associativity".to_string(),
],
}
}
fn gpu_scaffold_report_for_fixture(
kind: &CpuOracleFixtureKind,
gpu: &GpuScaffoldBackend,
) -> Result<Option<GpuUnsupportedReport>> {
match kind {
CpuOracleFixtureKind::DenseI64 => dense_gpu_unsupported_report(gpu),
CpuOracleFixtureKind::PadicPointwise => padic_pointwise_gpu_unsupported_report(gpu),
CpuOracleFixtureKind::PadicMatmul => padic_matmul_gpu_unsupported_report(gpu),
CpuOracleFixtureKind::PadicValuationSkip => padic_valuation_gpu_unsupported_report(gpu),
CpuOracleFixtureKind::SheafGlue => sheaf_gpu_unsupported_report(gpu),
CpuOracleFixtureKind::CategoricalLaw => Ok(Some(GpuUnsupportedReport {
backend: "gpu_scaffold".to_string(),
reason: GpuUnsupportedReason::NoKernel {
op_name: "categorical_contract_laws".to_string(),
},
transfer_reason: None,
fallback_backend: "cpu_scalar".to_string(),
evidence: vec![
"P183 GPU support is scaffold/fallback only; no optimized kernels are claimed"
.to_string(),
GpuUnsupportedReason::NoKernel {
op_name: "categorical_contract_laws".to_string(),
}
.message(),
],
})),
}
}
fn dense_gpu_unsupported_report(gpu: &GpuScaffoldBackend) -> Result<Option<GpuUnsupportedReport>> {
let meta = ObjectMeta::tensor(
DomainId::new("integer"),
Shape::from(vec![4]),
Representation::dense_cpu(),
);
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(meta.clone());
let rhs = graph.add_input(meta);
let add_out = graph.add_op(AddOp, &[lhs, rhs])?[0];
graph.add_op(ReduceOp, &[add_out])?;
let plan = HeuristicPlanner::new(gpu.capabilities()).plan(&graph)?;
Ok(gpu.unsupported_plan_report(&plan))
}
fn padic_pointwise_gpu_unsupported_report(
gpu: &GpuScaffoldBackend,
) -> Result<Option<GpuUnsupportedReport>> {
let q5 = PadicDomain::new(5, 3)?;
let meta = ObjectMeta::tensor(q5.id(), Shape::from(vec![3]), Representation::dense_cpu());
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(meta.clone());
let rhs = graph.add_input(meta);
let add_out = graph.add_op(AddOp, &[lhs, rhs])?[0];
graph.add_op(crate::op::MulOp, &[add_out, rhs])?;
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = HeuristicPlanner::new(gpu.capabilities()).plan_with_registry(&graph, ®istry)?;
Ok(gpu.unsupported_plan_report(&plan))
}
fn padic_matmul_gpu_unsupported_report(
gpu: &GpuScaffoldBackend,
) -> Result<Option<GpuUnsupportedReport>> {
let q5 = PadicDomain::new(5, 3)?;
let meta = ObjectMeta::tensor(
q5.id(),
Shape::from(vec![2, 2]),
Representation::dense_cpu(),
);
let mut graph = SemanticGraph::new();
let lhs = graph.add_input(meta.clone());
let rhs = graph.add_input(meta);
graph.add_op(MatmulOp, &[lhs, rhs])?;
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = HeuristicPlanner::new(gpu.capabilities()).plan_with_registry(&graph, ®istry)?;
Ok(gpu.unsupported_plan_report(&plan))
}
fn padic_valuation_gpu_unsupported_report(
gpu: &GpuScaffoldBackend,
) -> Result<Option<GpuUnsupportedReport>> {
let q5 = PadicDomain::new(5, 3)?;
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = HeuristicPlanner::new(gpu.capabilities())
.plan_padic_sum_products_skip_with_registry(&q5, 0, 1, 2, ®istry);
Ok(gpu.unsupported_plan_report(&plan))
}
fn sheaf_gpu_unsupported_report(gpu: &GpuScaffoldBackend) -> Result<Option<GpuUnsupportedReport>> {
let cover = Cover::new("U", ["A", "B"]);
let registry = OperatorRegistry::cpu_scalar_builtins()?;
let plan = HeuristicPlanner::new(gpu.capabilities())
.plan_cover_glue_check_with_registry(&cover, ®istry);
Ok(gpu.unsupported_plan_report(&plan))
}
fn ensure_no_required_obligations(plan: &crate::planner::ExecutionPlan) -> Result<()> {
if let Some(obligation) = plan.obligations.iter().find(|obligation| {
obligation.severity == ObligationSeverity::Required
&& matches!(obligation.source, ObligationSource::Backend(_))
}) {
Err(Error::verification(format!(
"CPU oracle conformance plan has unresolved backend admission obligation: {}",
obligation.condition
)))
} else {
Ok(())
}
}
fn open(id: &str) -> OpenId {
OpenId(id.to_string())
}
fn finite_site_fixture() -> FiniteSite {
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"))
}