tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
//! Audit-report section that lists every registered lowering rule (P356).
//!
//! The base `audit_report` only lists the lowering rules that were
//! actually exercised in a plan. This module adds a complementary
//! "registry summary" that lists every rule registered in
//! `OperatorRegistry::cpu_scalar_builtins`, so the audit text can
//! answer "what rules COULD this plan have used?" not just "what
//! rules did it use?".
//!
//! P356 keeps the new section additive: it is appended to the
//! existing audit text. The existing "lowering evidence" and
//! "math-bound lowering_rule_ids" lines are unchanged.

use crate::op::registry::LoweringRule;

/// Format a "registered lowering rules" section that lists every
/// rule in the slice, sorted by `(backend, op_name, id)`. Each
/// rule gets one line:
///
/// ```text
/// registered lowering rule: id=..., op=..., backend=..., evidence=N, obligations=M
/// ```
///
/// The function does not fail: if a rule has no required-evidence
/// or no obligations, the corresponding fields are `0`.
pub fn registered_lowering_rules_section(rules: &[LoweringRule]) -> String {
    let mut sorted: Vec<&LoweringRule> = rules.iter().collect();
    sorted.sort_by(|a, b| {
        (a.backend.as_str(), a.op_name.as_str(), a.id.0.as_str()).cmp(&(
            b.backend.as_str(),
            b.op_name.as_str(),
            b.id.0.as_str(),
        ))
    });
    let mut lines: Vec<String> = Vec::new();
    lines.push(format!("registered_lowering_rules: count={}", sorted.len()));
    for rule in sorted {
        lines.push(format!(
            "registered_lowering_rule: id={}, op={}, backend={}, evidence={}, obligations={}",
            rule.id.0,
            rule.op_name,
            rule.backend,
            rule.required_evidence.len(),
            rule.obligations.len(),
        ));
    }
    lines.join("\n")
}

/// Wrap the standard `audit_report(plan)` text with a "registered
/// lowering rules" section. The base report already lists the rules
/// the plan actually exercised; this wrapper appends the rules that
/// the registry makes available, so the audit text can answer
/// "what lowering rules COULD this plan have used?" as well as
/// "what rules did it use?".
///
/// The wrapper is additive: it never trims or rewrites the base
/// report's lines. The "registered lowering rules" section is
/// appended after a blank line.
pub fn audit_report_with_registry(
    plan: &crate::planner::ExecutionPlan,
    registry: &crate::op::registry::OperatorRegistry,
) -> String {
    let base = crate::verify::audit_report(plan);
    let section = registered_lowering_rules_section(registry.lowering_registry().rules());
    format!("{base}\n{section}")
}