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"));
}