use std::collections::BTreeMap;
use crate::domain::ContractSet;
use crate::object::Representation;
use crate::op::reductions::ReductionKind;
use crate::op::{LayerBehavior, OpInput, OpOutput, OpSignature};
use crate::theory::CertifiedTheoryRequirement;
use crate::{Error, Result};
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct LoweringRuleId(pub String);
impl LoweringRuleId {
pub fn new(id: impl Into<String>) -> Self {
Self(id.into())
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct OperatorEntry {
pub name: String,
pub signature: OpSignature,
pub required_contracts: ContractSet,
pub provided_contracts: ContractSet,
pub layer_behavior: Vec<LayerBehavior>,
}
impl OperatorEntry {
pub fn new(
name: impl Into<String>,
signature: OpSignature,
required_contracts: ContractSet,
provided_contracts: ContractSet,
layer_behavior: Vec<LayerBehavior>,
) -> Self {
Self {
name: name.into(),
signature,
required_contracts,
provided_contracts,
layer_behavior,
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LoweringRule {
pub id: LoweringRuleId,
pub op_name: String,
pub backend: String,
pub supported_representations: Vec<String>,
pub supported_domains: Vec<String>,
pub capabilities: Vec<LoweringCapability>,
pub required_evidence: Vec<LoweringEvidence>,
pub obligations: Vec<LoweringObligation>,
pub theory_requirements: Vec<CertifiedTheoryRequirement>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LoweringCapability {
pub domain: LoweringDomainRequirement,
pub precision: PrecisionRequirement,
pub valuation: ValuationRequirement,
pub locality: LocalityRequirement,
pub layout: LayoutRequirement,
pub device: DeviceRequirement,
pub proof_obligations: Vec<String>,
}
impl LoweringCapability {
pub fn dense_integer() -> Self {
Self {
domain: LoweringDomainRequirement::BackendDomain("integer".to_string()),
precision: PrecisionRequirement::Exact,
valuation: ValuationRequirement::None,
locality: LocalityRequirement::Global,
layout: LayoutRequirement::Representation(Representation::dense_cpu().id().0),
device: DeviceRequirement::Any,
proof_obligations: Vec::new(),
}
}
pub fn rocm_hip_dense_i32(
required_gfx: impl Into<String>,
device_capability_fingerprint: impl Into<String>,
kernel_source_fingerprint: impl Into<String>,
compiler_fingerprint: impl Into<String>,
) -> Self {
Self {
domain: LoweringDomainRequirement::BackendDomain("integer".to_string()),
precision: PrecisionRequirement::Exact,
valuation: ValuationRequirement::None,
locality: LocalityRequirement::Global,
layout: LayoutRequirement::Representation(Representation::dense_cpu().id().0),
device: DeviceRequirement::RocmHip {
required_gfx: required_gfx.into(),
device_capability_fingerprint: device_capability_fingerprint.into(),
kernel_source_fingerprint: kernel_source_fingerprint.into(),
compiler_fingerprint: compiler_fingerprint.into(),
cpu_oracle_required: true,
transfer_obligations: vec![
"host_to_device_lhs".to_string(),
"host_to_device_rhs".to_string(),
"device_to_host_output".to_string(),
],
},
proof_obligations: vec![
"ROCm/HIP device capability fingerprint must match the admitted lowering"
.to_string(),
"kernel source and hipcc compiler fingerprints must match the cache key"
.to_string(),
"HIP dense output must be compared elementwise with the CPU oracle".to_string(),
],
}
}
pub fn rocm_hip_padic_valuation(
required_gfx: impl Into<String>,
device_capability_fingerprint: impl Into<String>,
kernel_source_fingerprint: impl Into<String>,
compiler_fingerprint: impl Into<String>,
) -> Self {
Self {
domain: LoweringDomainRequirement::BackendDomain("padic:fixed_precision".to_string()),
precision: PrecisionRequirement::PadicFixedPrecision {
min_digits: 1,
equality_digits_match_precision: true,
},
valuation: ValuationRequirement::PadicCutoffAtPrecision,
locality: LocalityRequirement::Global,
layout: LayoutRequirement::Representation(Representation::PadicScalar.id().0),
device: DeviceRequirement::RocmHip {
required_gfx: required_gfx.into(),
device_capability_fingerprint: device_capability_fingerprint.into(),
kernel_source_fingerprint: kernel_source_fingerprint.into(),
compiler_fingerprint: compiler_fingerprint.into(),
cpu_oracle_required: true,
transfer_obligations: vec![
"host_to_device_padic_residues".to_string(),
"device_to_host_valuations".to_string(),
],
},
proof_obligations: vec![
"ROCm/HIP p-adic valuation helper must use the active precision cutoff"
.to_string(),
"HIP valuation output must be compared elementwise with PadicDomain::valuation_of"
.to_string(),
"planner cache identity must bind device, kernel source, compiler, and p-adic cutoff"
.to_string(),
],
}
}
pub fn fixed_precision_padic() -> Self {
Self {
domain: LoweringDomainRequirement::BackendDomain("padic:fixed_precision".to_string()),
precision: PrecisionRequirement::PadicFixedPrecision {
min_digits: 1,
equality_digits_match_precision: true,
},
valuation: ValuationRequirement::PadicCutoffAtPrecision,
locality: LocalityRequirement::Global,
layout: LayoutRequirement::Any,
device: DeviceRequirement::Any,
proof_obligations: vec![
"p-adic prime and precision must be known before lowering".to_string(),
],
}
}
pub fn finite_site_sheaf() -> Self {
Self {
domain: LoweringDomainRequirement::BackendDomain("sheaf:finite_site".to_string()),
precision: PrecisionRequirement::Exact,
valuation: ValuationRequirement::None,
locality: LocalityRequirement::FiniteSite {
requires_restriction_witnesses: true,
requires_gluing_report: true,
},
layout: LayoutRequirement::Representation(
Representation::CoverIndexedSection {
device: crate::object::DeviceId::cpu(),
}
.id()
.0,
),
device: DeviceRequirement::Any,
proof_obligations: vec![
"cover must be valid in the finite site".to_string(),
"sections must agree on declared overlaps before gluing".to_string(),
],
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum LoweringDomainRequirement {
Any,
BackendDomain(String),
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PrecisionRequirement {
Any,
Exact,
PadicFixedPrecision {
min_digits: u32,
equality_digits_match_precision: bool,
},
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ValuationRequirement {
None,
PadicCutoffAtPrecision,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum LocalityRequirement {
Global,
FiniteSite {
requires_restriction_witnesses: bool,
requires_gluing_report: bool,
},
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum LayoutRequirement {
Any,
Representation(String),
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum DeviceRequirement {
Any,
RocmHip {
required_gfx: String,
device_capability_fingerprint: String,
kernel_source_fingerprint: String,
compiler_fingerprint: String,
cpu_oracle_required: bool,
transfer_obligations: Vec<String>,
},
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum UnsupportedBackendReason {
MissingBackendDomain {
required: String,
backend: String,
},
UnsupportedRepresentation {
required: String,
actual: String,
},
PadicDomainParseFailed {
domain: String,
},
PadicPrecisionTooLow {
required_min_digits: u32,
actual_digits: u32,
},
MissingPadicResource,
MissingPadicValuationCutoff {
expected_cutoff: u32,
actual_cutoff: u32,
},
MissingSheafFiniteSiteCapability {
backend: String,
},
MissingRocmHipCapability {
required: String,
backend: String,
},
}
impl UnsupportedBackendReason {
pub fn message(&self) -> String {
match self {
Self::MissingBackendDomain { required, backend } => {
format!(
"backend {backend} does not advertise required domain capability {required}"
)
}
Self::UnsupportedRepresentation { required, actual } => {
format!("representation {actual} does not satisfy required layout {required}")
}
Self::PadicDomainParseFailed { domain } => {
format!("domain {domain} is not a fixed-precision p-adic domain id")
}
Self::PadicPrecisionTooLow {
required_min_digits,
actual_digits,
} => format!(
"p-adic precision {actual_digits} is below required minimum {required_min_digits}"
),
Self::MissingPadicResource => {
"p-adic lowering requires a planner-visible PadicPlanningResource".to_string()
}
Self::MissingPadicValuationCutoff {
expected_cutoff,
actual_cutoff,
} => format!(
"p-adic valuation cutoff {actual_cutoff} does not match active precision {expected_cutoff}"
),
Self::MissingSheafFiniteSiteCapability { backend } => {
format!("backend {backend} does not advertise sheaf:finite_site capability")
}
Self::MissingRocmHipCapability { required, backend } => {
format!(
"backend {backend} does not satisfy ROCm/HIP lowering requirement {required}"
)
}
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LoweringEvidence {
pub kind: LoweringEvidenceKind,
pub description: String,
}
impl LoweringEvidence {
pub fn new(kind: LoweringEvidenceKind, description: impl Into<String>) -> Self {
Self {
kind,
description: description.into(),
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum LoweringEvidenceKind {
ExactnessPreserved,
MetadataPreserved,
FusionPreserved,
ValuationCutoff,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LoweringObligation {
pub condition: String,
pub rationale: String,
}
impl LoweringObligation {
pub fn new(condition: impl Into<String>, rationale: impl Into<String>) -> Self {
Self {
condition: condition.into(),
rationale: rationale.into(),
}
}
}
impl LoweringRule {
pub fn new(
id: impl Into<String>,
op_name: impl Into<String>,
backend: impl Into<String>,
supported_representations: Vec<String>,
) -> Self {
Self {
id: LoweringRuleId::new(id),
op_name: op_name.into(),
backend: backend.into(),
supported_representations,
supported_domains: Vec::new(),
capabilities: Vec::new(),
required_evidence: Vec::new(),
obligations: Vec::new(),
theory_requirements: Vec::new(),
}
}
pub fn supports_representation(&self, representation: &str) -> bool {
self.supported_representations.is_empty()
|| self
.supported_representations
.iter()
.any(|supported| supported == representation)
}
pub fn supports_domain(&self, domain: &str) -> bool {
self.supported_domains.is_empty()
|| self.supported_domains.iter().any(|supported| {
supported == domain
|| supported
.strip_suffix('*')
.is_some_and(|prefix| domain.starts_with(prefix))
})
}
pub fn with_supported_domain(mut self, domain: impl Into<String>) -> Self {
self.supported_domains.push(domain.into());
self
}
pub fn with_capability(mut self, capability: LoweringCapability) -> Self {
self.capabilities.push(capability);
self
}
pub fn with_required_evidence(
mut self,
kind: LoweringEvidenceKind,
description: impl Into<String>,
) -> Self {
self.required_evidence
.push(LoweringEvidence::new(kind, description));
self
}
pub fn with_obligation(
mut self,
condition: impl Into<String>,
rationale: impl Into<String>,
) -> Self {
self.obligations
.push(LoweringObligation::new(condition, rationale));
self
}
pub fn with_theory_requirement(mut self, requirement: CertifiedTheoryRequirement) -> Self {
self.theory_requirements.push(requirement);
self
}
pub fn cache_fingerprint_material(&self) -> Vec<String> {
let mut parts = vec![
format!("id={}", self.id.0),
format!("op={}", self.op_name),
format!("backend={}", self.backend),
];
parts.extend(
self.supported_representations
.iter()
.map(|item| format!("repr={item}")),
);
parts.extend(
self.supported_domains
.iter()
.map(|item| format!("domain={item}")),
);
parts.extend(
self.capabilities
.iter()
.map(|capability| format!("capability={capability:?}")),
);
parts.extend(
self.required_evidence
.iter()
.map(|evidence| format!("evidence={:?}:{}", evidence.kind, evidence.description)),
);
parts.extend(self.obligations.iter().map(|obligation| {
format!(
"obligation={}:{}",
obligation.condition, obligation.rationale
)
}));
parts.extend(self.theory_requirements.iter().map(|requirement| {
format!(
"theory={}:{}:{}:{}",
requirement.theory.as_str(),
requirement.law_id,
requirement.theorem_id.as_deref().unwrap_or("none"),
requirement.required_evidence.join("|")
)
}));
parts.sort();
parts
}
pub fn cache_fingerprint(&self) -> String {
stable_fingerprint(&self.cache_fingerprint_material())
}
}
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct BackendLoweringRegistry {
lowerings: Vec<LoweringRule>,
}
impl BackendLoweringRegistry {
pub fn new() -> Self {
Self::default()
}
pub fn register_lowering_unchecked(&mut self, rule: LoweringRule) -> Result<()> {
if self.lowering_by_id(&rule.id.0).is_some() {
return Err(Error::operator(format!(
"lowering {} is already registered",
rule.id.0
)));
}
self.lowerings.push(rule);
Ok(())
}
pub fn lowering_for(
&self,
op_name: &str,
backend: &str,
representation: &str,
) -> Option<&LoweringRule> {
self.lowerings.iter().find(|rule| {
rule.op_name == op_name
&& rule.backend == backend
&& rule.supports_representation(representation)
})
}
pub fn lowering_for_domain(
&self,
op_name: &str,
backend: &str,
representation: &str,
domain: &str,
) -> Option<&LoweringRule> {
self.lowerings.iter().find(|rule| {
rule.op_name == op_name
&& rule.backend == backend
&& rule.supports_representation(representation)
&& rule.supports_domain(domain)
})
}
pub fn lowering_by_id(&self, id: &str) -> Option<&LoweringRule> {
self.lowerings.iter().find(|rule| rule.id.0 == id)
}
pub fn rules(&self) -> &[LoweringRule] {
&self.lowerings
}
}
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct OperatorRegistry {
operators: BTreeMap<String, OperatorEntry>,
lowerings: BackendLoweringRegistry,
}
impl OperatorRegistry {
pub fn new() -> Self {
Self::default()
}
pub fn from_parts(
operators: BTreeMap<String, OperatorEntry>,
lowerings: BackendLoweringRegistry,
) -> Result<Self> {
for rule in lowerings.rules() {
if !operators.contains_key(&rule.op_name) {
return Err(Error::operator(format!(
"cannot attach lowering {} for unknown operator {}",
rule.id.0, rule.op_name
)));
}
}
Ok(Self {
operators,
lowerings,
})
}
pub fn register_operator(&mut self, entry: OperatorEntry) -> Result<()> {
if self.operators.contains_key(&entry.name) {
return Err(Error::operator(format!(
"operator {} is already registered",
entry.name
)));
}
self.operators.insert(entry.name.clone(), entry);
Ok(())
}
pub fn register_lowering(&mut self, rule: LoweringRule) -> Result<()> {
if !self.operators.contains_key(&rule.op_name) {
return Err(Error::operator(format!(
"cannot register lowering {} for unknown operator {}",
rule.id.0, rule.op_name
)));
}
self.lowerings.register_lowering_unchecked(rule)
}
pub fn operator(&self, name: &str) -> Option<&OperatorEntry> {
self.operators.get(name)
}
pub fn lowering_registry(&self) -> &BackendLoweringRegistry {
&self.lowerings
}
pub fn lowering_for(
&self,
op_name: &str,
backend: &str,
representation: &str,
) -> Option<&LoweringRule> {
self.lowerings
.lowering_for(op_name, backend, representation)
}
pub fn lowering_for_domain(
&self,
op_name: &str,
backend: &str,
representation: &str,
domain: &str,
) -> Option<&LoweringRule> {
self.lowerings
.lowering_for_domain(op_name, backend, representation, domain)
}
pub fn lowering_by_id(&self, id: &str) -> Option<&LoweringRule> {
self.lowerings.lowering_by_id(id)
}
pub fn cpu_scalar_builtins() -> Result<Self> {
let mut registry = Self::new();
let dense_cpu = Representation::dense_cpu().id().0;
let padic_scalar = Representation::PadicScalar.id().0;
registry.register_operator(binary_pointwise_entry("add"))?;
registry.register_operator(binary_pointwise_entry("mul"))?;
registry.register_operator(matmul_entry())?;
registry.register_operator(ternary_pointwise_entry("fma"))?;
registry.register_operator(p_pad_fma_entry())?;
registry.register_operator(p_dot_entry())?;
registry.register_operator(clamp_entry())?;
registry.register_operator(neg_entry())?;
registry.register_operator(abs_entry())?;
registry.register_operator(square_entry())?;
registry.register_operator(mul_by_two_entry())?;
registry.register_operator(binary_pointwise_entry("sub"))?;
registry.register_operator(binary_pointwise_entry("div"))?;
registry.register_operator(scalar_binary_entry("scalar_add"))?;
registry.register_operator(scalar_binary_entry("scalar_mul"))?;
registry.register_operator(scalar_binary_entry("pow"))?;
registry.register_operator(unary_pointwise_entry("sqrt"))?;
registry.register_operator(unary_pointwise_entry("exp2"))?;
registry.register_operator(unary_pointwise_entry("log2"))?;
registry.register_operator(reshape_entry())?;
registry.register_operator(transpose_entry())?;
registry.register_operator(permute_entry())?;
registry.register_operator(slice_entry())?;
registry.register_operator(concat_entry())?;
registry.register_operator(broadcast_entry())?;
registry.register_operator(unary_pointwise_entry("flatten"))?;
registry.register_operator(squeeze_entry())?;
registry.register_operator(unsqueeze_entry())?;
registry.register_operator(unary_pointwise_entry("relu"))?;
registry.register_operator(nn_approximate_entry("sigmoid"))?;
registry.register_operator(nn_approximate_entry("tanh"))?;
registry.register_operator(nn_approximate_entry("gelu"))?;
registry.register_operator(nn_softmax_entry())?;
registry.register_operator(nn_layer_norm_entry())?;
registry.register_operator(gather_entry())?;
registry.register_operator(scatter_entry())?;
registry.register_operator(index_select_entry())?;
registry.register_operator(index_add_entry())?;
registry.register_operator(nonzero_entry())?;
registry.register_operator(reduction_entry("sum", ReductionKind::Sum))?;
registry.register_operator(reduction_entry("mean", ReductionKind::Mean))?;
registry.register_operator(reduction_entry("max", ReductionKind::Max))?;
registry.register_operator(reduction_entry("min", ReductionKind::Min))?;
registry.register_operator(reduction_entry("argmax", ReductionKind::ArgMax))?;
registry.register_operator(reduction_entry("argmin", ReductionKind::ArgMin))?;
registry.register_operator(reduction_entry("prod", ReductionKind::Prod))?;
registry.register_operator(reduction_entry("any", ReductionKind::Any))?;
registry.register_operator(reduction_entry("all", ReductionKind::All))?;
registry.register_operator(unary_pointwise_entry("map"))?;
registry.register_operator(global_reduce_entry())?;
registry.register_operator(binary_pointwise_entry("fused:add+map"))?;
registry.register_operator(OperatorEntry::new(
"cover_glue_check",
OpSignature {
inputs: Vec::new(),
outputs: vec![OpOutput {
name: "glued".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::CoverLocal],
))?;
registry.register_operator(OperatorEntry::new(
"padic_sum_products_valuation_skip",
binary_signature(),
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::ValuationFiltered],
))?;
for lowering in [
LoweringRule::new(
"cpu.add.dense",
"add",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve exact integer addition",
)
.with_obligation(
"input domains and shapes must match before dense add lowering",
"add lowering assumes semantic inference already discharged domain and shape equality",
),
LoweringRule::new(
"cpu.add.padic_dense",
"add",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve fixed-precision p-adic addition modulo p^N",
)
.with_obligation(
"all p-adic add operands must share prime and precision",
"p-adic addition lowering assumes semantic inference preserved a single p-adic domain",
),
LoweringRule::new(
"cpu.mul.dense",
"mul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve exact integer multiplication",
)
.with_obligation(
"input domains and shapes must match before dense mul lowering",
"mul lowering assumes semantic inference already discharged domain and shape equality",
),
LoweringRule::new(
"cpu.mul.padic_dense",
"mul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve fixed-precision p-adic multiplication modulo p^N",
)
.with_obligation(
"all p-adic mul operands must share prime and precision",
"p-adic multiplication lowering assumes semantic inference preserved a single p-adic domain",
),
LoweringRule::new(
"cpu.fma.dense",
"fma",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve exact integer fused multiply-add in a single deterministic pass",
)
.with_obligation(
"all fma operands must share domain and shape before dense fma lowering",
"fma lowering assumes semantic inference discharged domain and shape equality for a, b, c",
),
LoweringRule::new(
"cpu.fma.padic_dense",
"fma",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tensors preserve fixed-precision p-adic fused multiply-add modulo p^N",
)
.with_obligation(
"all p-adic fma operands must share prime and precision",
"p-adic fma lowering assumes semantic inference preserved a single p-adic domain",
),
LoweringRule::new(
"cpu.p_pad_fma.dense",
"p_pad_fma",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU p-adic tensors preserve fixed-precision matmul-fma modulo p^N in a single deterministic pass",
)
.with_obligation(
"p_pad_fma expects rank-2 a, b, c with matching inner dim and bias shape equal to output (M, N)",
"p-adic matmul-fma lowering assumes semantic inference discharged the rank-2 shape constraints",
),
LoweringRule::new(
"cpu.p_dot.dense",
"p_dot",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU p-adic vectors preserve fixed-precision dot product modulo p^N in a single deterministic pass",
)
.with_obligation(
"p_dot expects rank-1 vectors of equal length on a single p-adic domain",
"p-adic dot lowering assumes semantic inference discharged the rank-1 length and domain equality",
),
LoweringRule::new(
"cpu.clamp.dense",
"clamp",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer clamp into a closed interval from scalar lo/hi inputs",
)
.with_obligation(
"clamp expects (data, lo, hi) where lo and hi are scalar i64 tensors and data shape is preserved",
"clamp lowering assumes semantic inference discharged the 3-input shape constraints",
),
LoweringRule::new(
"cpu.neg.dense",
"neg",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer negation in a single deterministic pass",
)
.with_obligation(
"neg expects a single dense i64 tensor input with shape preserved",
"neg lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.abs.dense",
"abs",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer absolute value with saturating i64::MIN handling",
)
.with_obligation(
"abs expects a single dense i64 tensor input with shape preserved",
"abs lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.square.dense",
"square",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer square via wrapping multiplication in one pass",
)
.with_obligation(
"square expects a single dense i64 tensor input with shape preserved",
"square lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.mul_by_two.dense",
"mul_by_two",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer doubling via wrapping multiplication in one pass",
)
.with_obligation(
"mul_by_two expects a single dense i64 tensor input with shape preserved",
"mul_by_two lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.sub.dense",
"sub",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer subtraction via wrapping in one pass",
)
.with_obligation(
"sub expects two dense i64 tensor inputs with matching shape and domain",
"sub lowering assumes semantic inference discharged domain and shape equality",
),
LoweringRule::new(
"cpu.div.dense",
"div",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer division in one pass; divisor zero rejected",
)
.with_obligation(
"div expects two dense i64 tensor inputs with matching shape and nonzero divisor",
"div lowering assumes semantic inference discharged domain and shape equality and divisor nonzero",
),
LoweringRule::new(
"cpu.scalar_add.dense",
"scalar_add",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer tensor+scalar broadcast addition in one pass",
)
.with_obligation(
"scalar_add expects (tensor, scalar) with matching domain and a 1-element scalar tensor",
"scalar_add lowering assumes semantic inference discharged domain equality and scalar 1-element shape",
),
LoweringRule::new(
"cpu.scalar_mul.dense",
"scalar_mul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer tensor*scalar broadcast multiplication in one pass",
)
.with_obligation(
"scalar_mul expects (tensor, scalar) with matching domain and a 1-element scalar tensor",
"scalar_mul lowering assumes semantic inference discharged domain equality and scalar 1-element shape",
),
LoweringRule::new(
"cpu.pow.dense",
"pow",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer tensor^non-negative-scalar exponentiation in one pass",
)
.with_obligation(
"pow expects (tensor, exp) with matching domain, a 1-element exp tensor, and a non-negative exponent",
"pow lowering assumes semantic inference discharged domain equality and the non-negative exponent precondition",
),
LoweringRule::new(
"cpu.sqrt.dense",
"sqrt",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer floor square root in one pass; negative input rejected",
)
.with_obligation(
"sqrt expects a single dense i64 tensor input with all values non-negative",
"sqrt lowering assumes semantic inference discharged the non-negative-input precondition",
),
LoweringRule::new(
"cpu.exp2.dense",
"exp2",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer 2^x with saturating overflow to i64::MAX",
)
.with_obligation(
"exp2 expects a single dense i64 tensor input with all values non-negative",
"exp2 lowering assumes semantic inference discharged the non-negative-input precondition",
),
LoweringRule::new(
"cpu.log2.dense",
"log2",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU i64 tensors preserve exact integer floor log2 with values <= 1 mapped to 0",
)
.with_obligation(
"log2 expects a single dense i64 tensor input",
"log2 lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.reshape.dense",
"reshape",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU reshape copies data into a new buffer with the target shape, preserving element order",
)
.with_obligation(
"reshape expects (data, target_shape) where target_shape is a 1-D i64 tensor and the dim product matches data length",
"reshape lowering copies the input buffer so downstream ops cannot alias the original",
),
LoweringRule::new(
"cpu.transpose.dense",
"transpose",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU transpose swaps two axes of an all-static input tensor, preserving element values",
)
.with_obligation(
"transpose expects (input, axes) where axes is a 2-element i32 tensor and input dims are all static",
"transpose lowering assumes semantic inference discharged the all-static input constraint",
),
LoweringRule::new(
"cpu.permute.dense",
"permute",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU permute reorders axes of an all-static input tensor by a permutation vector",
)
.with_obligation(
"permute expects (input, permutation) where permutation is a valid 1-D permutation vector of length rank",
"permute lowering assumes semantic inference discharged the all-static input and permutation constraints",
),
LoweringRule::new(
"cpu.slice.dense",
"slice",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU slice copies a half-open [start, end) range of an axis into a new buffer",
)
.with_obligation(
"slice expects (input, bounds) where bounds is a 3-element [axis, start, end] i32 tensor with 0 <= start <= end <= dim_size",
"slice lowering assumes semantic inference discharged the bounds-in-range precondition",
),
LoweringRule::new(
"cpu.concat.dense",
"concat",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU concat stacks 2+ tensors along a single axis into a new buffer",
)
.with_obligation(
"concat expects N input tensors plus a final 1-element axis tensor; all inputs must share rank and matching non-concat dim sizes",
"concat lowering assumes semantic inference discharged the rank and non-concat-dim constraints",
),
LoweringRule::new(
"cpu.broadcast.dense",
"broadcast",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU broadcast expands an input tensor to a target shape by repeating size-1 axes (numpy-style right-align)",
)
.with_obligation(
"broadcast expects (input, target_shape) where input rank <= target rank and each aligned dim is either 1 or equal to the target",
"broadcast lowering assumes semantic inference discharged the broadcasting compatibility precondition",
),
LoweringRule::new(
"cpu.flatten.dense",
"flatten",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU flatten collapses every dim into a single 1-D dim; rank-0 input becomes a [1] tensor",
)
.with_obligation(
"flatten expects a single dense i64 tensor input",
"flatten lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.squeeze.dense",
"squeeze",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU squeeze drops every size-1 dim from an all-static input tensor",
)
.with_obligation(
"squeeze expects a single dense i64 tensor input with all dims static",
"squeeze lowering assumes semantic inference discharged the all-static input constraint",
),
LoweringRule::new(
"cpu.unsqueeze.dense",
"unsqueeze",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU unsqueeze inserts a single size-1 dim at the given axis (resolving negative indices)",
)
.with_obligation(
"unsqueeze expects (input, axis) where axis is a 1-element i32 tensor with -rank-1 <= axis <= rank",
"unsqueeze lowering assumes semantic inference discharged the axis-in-range precondition",
),
LoweringRule::new(
"cpu.relu.dense",
"relu",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU relu clamps every element to max(0, x), preserving i64 values exactly",
)
.with_obligation(
"relu expects a single dense i64 tensor input",
"relu lowering assumes semantic inference discharged the single-input shape constraint",
),
LoweringRule::new(
"cpu.sigmoid.dense",
"sigmoid",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU sigmoid returns a fixed-point approximation of 1 / (1 + exp(-x)) scaled by 1_000_000",
)
.with_obligation(
"sigmoid expects a single dense i64 tensor input",
"sigmoid lowering emits a 1_000_000-scaled fixed-point value; consumers that need floating-point fidelity must divide by 1_000_000",
),
LoweringRule::new(
"cpu.tanh.dense",
"tanh",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU tanh returns a fixed-point Pade-approximant of tanh(x) scaled by 1_000_000, saturating to +/-1_000_000 for |x| >= 8",
)
.with_obligation(
"tanh expects a single dense i64 tensor input",
"tanh lowering emits a 1_000_000-scaled fixed-point value; consumers that need floating-point fidelity must divide by 1_000_000",
),
LoweringRule::new(
"cpu.gelu.dense",
"gelu",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU gelu returns 0.5 * x * (1 + tanh(sqrt(2/pi) * (x + 0.044715 * x^3))) computed in fixed-point and scaled by 1_000_000",
)
.with_obligation(
"gelu expects a single dense i64 tensor input",
"gelu lowering emits a 1_000_000-scaled fixed-point value; consumers that need floating-point fidelity must divide by 1_000_000",
),
LoweringRule::new(
"cpu.softmax.dense",
"softmax",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU softmax normalizes over the last axis; output is scaled by 1_000_000 and the row sum equals 1_000_000 (modulo floor-rounding)",
)
.with_obligation(
"softmax expects a single dense i64 tensor input with a static last dim",
"softmax lowering assumes semantic inference discharged the static-last-dim precondition",
),
LoweringRule::new(
"cpu.layer_norm.dense",
"layer_norm",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU layer_norm normalizes over the last axis using floor-division mean and integer-sqrt stddev; gamma and beta are 1-D tensors of size last_dim",
)
.with_obligation(
"layer_norm expects (input, gamma, beta) where gamma and beta are 1-D dense i64 tensors of size last_dim",
"layer_norm lowering assumes semantic inference discharged the (input, gamma, beta) rank-and-shape preconditions",
),
LoweringRule::new(
"cpu.gather.dense",
"gather",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU gather copies input values to output positions selected by indices along a runtime axis, preserving i64 values exactly",
)
.with_obligation(
"gather expects (input, indices, axis) where indices is a dense i64 tensor and axis is a 1-element i32 tensor",
"gather lowering assumes semantic inference discharged the (input, indices, axis) rank preconditions and rejects out-of-range indices at execution time",
),
LoweringRule::new(
"cpu.scatter.dense",
"scatter",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU scatter writes input values into output positions named by indices along a runtime axis, leaving unwritten positions at 0",
)
.with_obligation(
"scatter expects (input, indices, axis) where indices has the same data length as input",
"scatter lowering assumes semantic inference discharged the (input, indices, axis) rank and length-match preconditions",
),
LoweringRule::new(
"cpu.index_select.dense",
"index_select",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU index_select selects elements along a runtime axis by integer indices, replacing the indexed dim with indices.len()",
)
.with_obligation(
"index_select expects (input, indices, axis) where indices is a 1-D dense i64 tensor",
"index_select lowering assumes semantic inference discharged the (input, indices, axis) rank preconditions",
),
LoweringRule::new(
"cpu.index_add.dense",
"index_add",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU index_add adds source values into input at positions named by indices along a runtime axis, using wrapping i64 addition",
)
.with_obligation(
"index_add expects (input, indices, source, axis) where indices and source have the same length and axis is a 1-element i32 tensor",
"index_add lowering assumes semantic inference discharged the (input, indices, source, axis) rank and length-match preconditions",
),
LoweringRule::new(
"cpu.nonzero.dense",
"nonzero",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU nonzero returns the row-major coordinates of every nonzero element as a 2-D i64 tensor [N, rank]",
)
.with_obligation(
"nonzero expects a single dense i64 tensor input with all dims static",
"nonzero lowering assumes semantic inference discharged the all-static-dim precondition",
),
LoweringRule::new(
"cpu.sum.dense",
"sum",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU sum reduces along the named axis using i64 saturating addition; output shape is the input shape with the axis dim removed",
)
.with_obligation(
"sum expects (input, axis) where axis is a 1-element i32 tensor",
"sum lowering assumes semantic inference discharged the (input, axis) rank precondition",
),
LoweringRule::new(
"cpu.mean.dense",
"mean",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU mean reduces by i64 floor division of the sum by axis_size",
)
.with_obligation(
"mean expects (input, axis) where axis is a 1-element i32 tensor and the named axis has positive size",
"mean lowering assumes semantic inference discharged the (input, axis) rank precondition; the result is integer floor-divided",
),
LoweringRule::new(
"cpu.max.dense",
"max",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU max returns the largest element along the named axis",
)
.with_obligation(
"max expects (input, axis) where axis is a 1-element i32 tensor and the named axis has positive size",
"max lowering assumes semantic inference discharged the (input, axis) rank precondition",
),
LoweringRule::new(
"cpu.min.dense",
"min",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU min returns the smallest element along the named axis",
)
.with_obligation(
"min expects (input, axis) where axis is a 1-element i32 tensor and the named axis has positive size",
"min lowering assumes semantic inference discharged the (input, axis) rank precondition",
),
LoweringRule::new(
"cpu.argmax.dense",
"argmax",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU argmax returns the index of the first occurrence of the largest element along the named axis",
)
.with_obligation(
"argmax expects (input, axis) where axis is a 1-element i32 tensor and the named axis has positive size",
"argmax lowering assumes semantic inference discharged the (input, axis) rank precondition; ties are broken by lowest index",
),
LoweringRule::new(
"cpu.argmin.dense",
"argmin",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU argmin returns the index of the first occurrence of the smallest element along the named axis",
)
.with_obligation(
"argmin expects (input, axis) where axis is a 1-element i32 tensor and the named axis has positive size",
"argmin lowering assumes semantic inference discharged the (input, axis) rank precondition; ties are broken by lowest index",
),
LoweringRule::new(
"cpu.prod.dense",
"prod",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU prod reduces along the named axis using wrapping i64 multiplication",
)
.with_obligation(
"prod expects (input, axis) where axis is a 1-element i32 tensor",
"prod lowering assumes semantic inference discharged the (input, axis) rank precondition; large products will wrap modulo 2^64",
),
LoweringRule::new(
"cpu.any.dense",
"any",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU any returns 1 if any element along the named axis is nonzero, else 0",
)
.with_obligation(
"any expects (input, axis) where axis is a 1-element i32 tensor",
"any lowering assumes semantic inference discharged the (input, axis) rank precondition",
),
LoweringRule::new(
"cpu.all.dense",
"all",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU all returns 1 if every element along the named axis is nonzero, else 0",
)
.with_obligation(
"all expects (input, axis) where axis is a 1-element i32 tensor",
"all lowering assumes semantic inference discharged the (input, axis) rank precondition",
),
LoweringRule::new(
"cpu.matmul.dense",
"matmul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU matmul preserves exact integer matrix multiplication for static rank-2 tensors",
)
.with_obligation(
"matmul inputs must be rank-2 tensors with matching inner dimensions",
"matrix multiplication lowering relies on semantic shape inference and backend static-dimension validation",
),
LoweringRule::new(
"cpu.matmul.padic_dense",
"matmul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU matmul preserves fixed-precision p-adic matrix multiplication modulo p^N",
)
.with_obligation(
"all p-adic matmul operands must share prime, precision, and compatible rank-2 matrix dimensions",
"p-adic matmul lowering assumes semantic inference preserved a single p-adic domain and matrix shape compatibility",
),
LoweringRule::new(
"cpu.matmul.padic_valuation_skip",
"matmul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ValuationCutoff,
"p-adic matmul skips products whose operand valuation sum reaches the precision cutoff",
)
.with_obligation(
"valuation-skip matmul must preserve precision-bounded equality with dense p-adic matmul",
"skipped products vanish modulo p^N under the active non-Archimedean precision model",
)
.with_theory_requirement(CertifiedTheoryRequirement::padic_valuation_skip()),
LoweringRule::new(
"cpu.matmul.padic_valuation_stratified",
"matmul",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("Q_*")
.with_capability(LoweringCapability::fixed_precision_padic())
.with_required_evidence(
LoweringEvidenceKind::ValuationCutoff,
"certificate-aware p-adic matmul skips only products whose operand valuation lower bound reaches the precision cutoff",
)
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"certified sparse p-adic matmul must match the dense CPU oracle modulo p^N",
)
.with_obligation(
"valuation-stratified matmul requires deterministic lhs/rhs valuation bucket fingerprints in plan identity",
"bucket fingerprints bind runtime valuation metadata to the admitted certificate policy",
)
.with_obligation(
"valuation-stratified matmul requires per-output skip certificates before optimized execution is claimed",
"certificates record skipped/evaluated counts, minimum skipped valuation, precision cutoff, and safety margin",
)
.with_theory_requirement(CertifiedTheoryRequirement::padic_valuation_skip()),
LoweringRule::new(
"cpu.map.dense",
"map",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::MetadataPreserved,
"dense CPU map preserves tensor metadata",
),
LoweringRule::new(
"cpu.reduce.dense",
"reduce",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::ExactnessPreserved,
"dense CPU reduce preserves exact integer summation semantics",
)
.with_obligation(
"reduction operator must have an associative accumulator",
"scalar reduction lowering relies on associativity for deterministic accumulation",
)
.with_theory_requirement(CertifiedTheoryRequirement::categorical_associativity()),
LoweringRule::new(
"cpu.fused_add_map.dense",
"fused:add+map",
"cpu_scalar",
vec![dense_cpu.clone()],
)
.with_supported_domain("integer")
.with_capability(LoweringCapability::dense_integer())
.with_required_evidence(
LoweringEvidenceKind::FusionPreserved,
"pointwise fusion preserves dense tensor metadata",
)
.with_obligation(
"fused pointwise chain must be single-consumer and metadata-preserving",
"fusion lowering relies on use-def safety and matching output metadata",
),
LoweringRule::new(
"cpu.padic_sum_products_valuation_skip",
"padic_sum_products_valuation_skip",
"cpu_scalar",
vec![padic_scalar],
)
.with_required_evidence(
LoweringEvidenceKind::ValuationCutoff,
"terms with valuation >= precision vanish modulo p^N",
)
.with_capability(LoweringCapability::fixed_precision_padic())
.with_obligation(
"all operands must share the same p-adic domain and precision",
"valuation skip correctness requires a single non-Archimedean precision model",
)
.with_theory_requirement(CertifiedTheoryRequirement::padic_valuation_skip()),
LoweringRule::new(
"cpu.cover_glue_check.finite_site",
"cover_glue_check",
"cpu_scalar",
vec![
Representation::CoverIndexedSection {
device: crate::object::DeviceId::cpu(),
}
.id()
.0,
],
)
.with_supported_domain("cover:*")
.with_capability(LoweringCapability::finite_site_sheaf())
.with_required_evidence(
LoweringEvidenceKind::MetadataPreserved,
"finite-site cover glue lowering preserves restriction witnesses and gluing reports",
)
.with_obligation(
"cover glue lowering requires a valid finite-site cover and compatible local sections",
"sheaf lowering is admitted only when local-to-global compatibility evidence can be produced",
)
.with_theory_requirement(CertifiedTheoryRequirement::finite_sheaf_gluing()),
] {
registry.register_lowering(lowering)?;
}
Ok(registry)
}
}
fn binary_pointwise_entry(name: &str) -> OperatorEntry {
OperatorEntry::new(
name,
binary_signature(),
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise],
)
}
fn scalar_binary_entry(name: &str) -> OperatorEntry {
OperatorEntry::new(
name,
OpSignature {
inputs: vec![
OpInput {
name: "tensor".to_string(),
},
OpInput {
name: "scalar".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::CoverLocal],
)
}
fn reshape_entry() -> OperatorEntry {
OperatorEntry::new(
"reshape",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "target_shape".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn transpose_entry() -> OperatorEntry {
OperatorEntry::new(
"transpose",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "axes".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn permute_entry() -> OperatorEntry {
OperatorEntry::new(
"permute",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "permutation".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn slice_entry() -> OperatorEntry {
OperatorEntry::new(
"slice",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "bounds".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn concat_entry() -> OperatorEntry {
OperatorEntry::new(
"concat",
OpSignature {
inputs: vec![OpInput {
name: "first".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn broadcast_entry() -> OperatorEntry {
OperatorEntry::new(
"broadcast",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "target_shape".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn squeeze_entry() -> OperatorEntry {
OperatorEntry::new(
"squeeze",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn nn_approximate_entry(name: &str) -> OperatorEntry {
OperatorEntry::new(
name,
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise],
)
}
fn nn_softmax_entry() -> OperatorEntry {
OperatorEntry::new(
"softmax",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn gather_entry() -> OperatorEntry {
OperatorEntry::new(
"gather",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "indices".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn scatter_entry() -> OperatorEntry {
OperatorEntry::new(
"scatter",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "indices".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn index_select_entry() -> OperatorEntry {
OperatorEntry::new(
"index_select",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "indices".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn index_add_entry() -> OperatorEntry {
OperatorEntry::new(
"index_add",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "indices".to_string(),
},
OpInput {
name: "source".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn reduction_entry(name: &str, _kind: ReductionKind) -> OperatorEntry {
OperatorEntry::new(
name,
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn nonzero_entry() -> OperatorEntry {
OperatorEntry::new(
"nonzero",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn nn_layer_norm_entry() -> OperatorEntry {
OperatorEntry::new(
"layer_norm",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "gamma".to_string(),
},
OpInput {
name: "beta".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn unsqueeze_entry() -> OperatorEntry {
OperatorEntry::new(
"unsqueeze",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "axis".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::Global],
)
}
fn mul_by_two_entry() -> OperatorEntry {
OperatorEntry::new(
"mul_by_two",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::CoverLocal],
)
}
fn square_entry() -> OperatorEntry {
OperatorEntry::new(
"square",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::CoverLocal],
)
}
fn abs_entry() -> OperatorEntry {
OperatorEntry::new(
"abs",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::CoverLocal],
)
}
fn neg_entry() -> OperatorEntry {
OperatorEntry::new(
"neg",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise, LayerBehavior::CoverLocal],
)
}
fn clamp_entry() -> OperatorEntry {
OperatorEntry::new(
"clamp",
OpSignature {
inputs: vec![
OpInput {
name: "input".to_string(),
},
OpInput {
name: "lo".to_string(),
},
OpInput {
name: "hi".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise],
)
}
fn p_dot_entry() -> OperatorEntry {
OperatorEntry::new(
"p_dot",
OpSignature {
inputs: vec![
OpInput {
name: "a".to_string(),
},
OpInput {
name: "b".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Global, LayerBehavior::PrecisionLayered],
)
}
fn p_pad_fma_entry() -> OperatorEntry {
OperatorEntry::new(
"p_pad_fma",
OpSignature {
inputs: vec![
OpInput {
name: "a".to_string(),
},
OpInput {
name: "b".to_string(),
},
OpInput {
name: "c".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Global, LayerBehavior::PrecisionLayered],
)
}
fn ternary_pointwise_entry(name: &str) -> OperatorEntry {
OperatorEntry::new(
name,
OpSignature {
inputs: vec![
OpInput {
name: "a".to_string(),
},
OpInput {
name: "b".to_string(),
},
OpInput {
name: "c".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise],
)
}
fn unary_pointwise_entry(name: &str) -> OperatorEntry {
OperatorEntry::new(
name,
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Pointwise],
)
}
fn matmul_entry() -> OperatorEntry {
OperatorEntry::new(
"matmul",
binary_signature(),
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Global, LayerBehavior::PrecisionLayered],
)
}
fn global_reduce_entry() -> OperatorEntry {
OperatorEntry::new(
"reduce",
OpSignature {
inputs: vec![OpInput {
name: "input".to_string(),
}],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
},
ContractSet::new(),
ContractSet::new(),
vec![LayerBehavior::Global],
)
}
fn binary_signature() -> OpSignature {
OpSignature {
inputs: vec![
OpInput {
name: "lhs".to_string(),
},
OpInput {
name: "rhs".to_string(),
},
],
outputs: vec![OpOutput {
name: "out".to_string(),
}],
}
}
fn stable_fingerprint(parts: &[String]) -> String {
let mut hash = 0xcbf29ce484222325u64;
for part in parts {
for byte in part.as_bytes() {
hash ^= u64::from(*byte);
hash = hash.wrapping_mul(0x100000001b3);
}
hash ^= 0xff;
hash = hash.wrapping_mul(0x100000001b3);
}
format!("loweringfp-{hash:016x}")
}