tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
use tokitai_operator::domain::{DynamicPadicDomain, PadicDomain};
use tokitai_operator::object::sheaf::{Cover, FiniteSite, Inclusion, OpenId};
use tokitai_operator::planner::ExecutionPlan;
use tokitai_operator::verify::{
    PadicSampleGenerator, audit_report_with_properties, check_padic_contract_properties,
    check_padic_contract_properties_with_samples, check_sheaf_contract_properties,
    ensure_all_properties_pass, verify_padic_contracts, verify_sheaf_contracts,
};

fn open(id: &str) -> OpenId {
    OpenId(id.to_string())
}

#[test]
fn p_adic_contract_properties_pass_for_deterministic_samples() {
    let q5 = PadicDomain::new(5, 4).unwrap();
    let reports = check_padic_contract_properties(&q5).unwrap();

    assert_eq!(reports.len(), 6);
    assert_eq!(reports[0].samples_checked, 10);
    assert_eq!(reports[1].samples_checked, 16);
    assert!(reports.iter().any(|report| {
        report.property == "p-adic additive and multiplicative identities"
            && report.samples_checked == 16
    }));
    assert!(reports.iter().any(|report| {
        report.property == "p-adic multiplication distributes over addition"
            && report.samples_checked == 16
    }));
    assert!(reports.iter().any(|report| {
        report.property == "p-adic vector operation oracle laws" && report.samples_checked == 4
    }));
    assert!(reports.iter().all(|report| report.passed));
    ensure_all_properties_pass(&reports).unwrap();
}

#[test]
fn p_adic_sample_generator_produces_valuation_stratified_pairs() {
    let q5 = PadicDomain::new(5, 4).unwrap();
    let samples = PadicSampleGenerator::valuation_stratified()
        .binary_samples(&q5)
        .unwrap();

    assert_eq!(samples.len(), 16);
    assert!(samples.source.contains("valuation-stratified"));
    assert!(
        samples
            .pairs
            .iter()
            .any(|(lhs, rhs)| q5.valuation_of(lhs).unwrap() == Some(3)
                && q5.valuation_of(rhs).unwrap() == Some(3))
    );
}

#[test]
fn dynamic_p_adic_samples_preserve_valuation_identities() {
    let q5 = DynamicPadicDomain::new(5, 72).unwrap();
    let lhs = q5.from_digits(&[0, 0, 2, 4, 1]).unwrap();
    let rhs = q5.from_digits(&[0, 3, 1]).unwrap();
    let product = q5.mul(&lhs, &rhs).unwrap();
    let sum = q5.add(&lhs, &rhs).unwrap();

    assert_eq!(q5.valuation_of(&lhs).unwrap(), Some(2));
    assert_eq!(q5.valuation_of(&rhs).unwrap(), Some(1));
    assert_eq!(q5.valuation_of(&product).unwrap(), Some(3));
    assert!(q5.valuation_of(&sum).unwrap().unwrap() >= 1);
}

#[test]
fn p_adic_property_checker_accepts_custom_sample_sets() {
    let q5 = PadicDomain::new(5, 4).unwrap();
    let samples = PadicSampleGenerator::contract_smoke()
        .binary_samples(&q5)
        .unwrap();
    let reports = check_padic_contract_properties_with_samples(&q5, &samples).unwrap();

    assert_eq!(samples.len(), 3);
    assert_eq!(reports[0].samples_checked, 3);
    assert_eq!(reports.len(), 6);
    assert!(reports.iter().all(|report| report.passed));
}

#[test]
fn p_adic_contract_verification_returns_aggregate_report() {
    let q5 = PadicDomain::new(5, 4).unwrap();
    let report = verify_padic_contracts(&q5).unwrap();

    assert!(report.execution.is_none());
    assert_eq!(report.properties.len(), 6);
    assert!(report.property_failures().is_empty());
    report.ensure_passed().unwrap();
}

#[test]
fn sheaf_contract_properties_pass_for_valid_finite_site() {
    let site = FiniteSite::new(
        vec![open("U"), open("A"), open("B"), open("A_cap_B")],
        vec![
            Inclusion::new("A", "U"),
            Inclusion::new("B", "U"),
            Inclusion::new("A_cap_B", "A"),
            Inclusion::new("A_cap_B", "B"),
            Inclusion::new("A_cap_B", "U"),
        ],
    );
    let cover = Cover::new("U", ["A", "B"]);
    let reports =
        check_sheaf_contract_properties(&site, &cover, (&open("A_cap_B"), &open("A"), &open("U")))
            .unwrap();

    assert_eq!(reports.len(), 2);
    assert!(reports.iter().all(|report| report.passed));
}

#[test]
fn sheaf_contract_properties_report_invalid_composition() {
    let site = FiniteSite::new(
        vec![open("U"), open("A"), open("B"), open("A_cap_B")],
        vec![
            Inclusion::new("A", "U"),
            Inclusion::new("B", "U"),
            Inclusion::new("A_cap_B", "A"),
            Inclusion::new("A_cap_B", "B"),
        ],
    );
    let cover = Cover::new("U", ["A", "B"]);
    let reports =
        check_sheaf_contract_properties(&site, &cover, (&open("A_cap_B"), &open("A"), &open("U")))
            .unwrap();

    assert_eq!(reports.len(), 2);
    assert!(reports[0].passed);
    assert!(!reports[1].passed);
    assert!(ensure_all_properties_pass(&reports).is_err());
}

#[test]
fn sheaf_contract_verification_propagates_property_failures() {
    let site = FiniteSite::new(
        vec![open("U"), open("A"), open("B"), open("A_cap_B")],
        vec![
            Inclusion::new("A", "U"),
            Inclusion::new("B", "U"),
            Inclusion::new("A_cap_B", "A"),
            Inclusion::new("A_cap_B", "B"),
        ],
    );
    let cover = Cover::new("U", ["A", "B"]);

    assert!(
        verify_sheaf_contracts(&site, &cover, (&open("A_cap_B"), &open("A"), &open("U"))).is_err()
    );
}

#[test]
fn audit_report_can_include_property_checks() {
    let q5 = PadicDomain::new(5, 4).unwrap();
    let properties = check_padic_contract_properties(&q5).unwrap();
    let audit =
        audit_report_with_properties(&ExecutionPlan::new("cpu.scalar".to_string()), &properties);

    assert!(audit.contains("property checks: 6"));
    assert!(audit.contains("p-adic valuation multiplication identity"));
    assert!(audit.contains("p-adic vector operation oracle laws"));
    assert!(audit.contains("passed=true"));
}