use crate::proof::algebra::checker::support::{
boundary_grid_u32, call_binary, engine_failure_violation, simple_rng, violation,
ZERO_PRODUCT_COUNTEREXAMPLES,
};
use crate::spec::law::{AlgebraicLaw, LawViolation};
use super::witnessed::*;
#[inline]
pub(crate) fn check_witnessed_u32(
op_id: &str,
f: fn(&[u8]) -> Vec<u8>,
law: &AlgebraicLaw,
count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
let mut rng = simple_rng(op_id, law.name());
let grid = boundary_grid_u32();
match law {
AlgebraicLaw::Commutative => {
for &a in &grid {
for &b in &grid {
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
let ba = call_binary(f, b, a).map_err(|e| engine_failure_violation(op_id, e))?;
if ab != ba {
return Ok((1, Some(violation(op_id, "commutative", a, b, 0, ab, ba))));
}
}
}
for i in 0..count {
let a = rng.next_u32();
let b = rng.next_u32();
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
let ba = call_binary(f, b, a).map_err(|e| engine_failure_violation(op_id, e))?;
if ab != ba {
return Ok((i + 1, Some(violation(op_id, "commutative", a, b, 0, ab, ba))));
}
}
Ok((count, None))
}
AlgebraicLaw::Associative => {
for &a in &grid {
for &b in &grid {
for &c in &grid {
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
if ab_c != a_bc {
return Ok((
1,
Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
));
}
}
}
}
for i in 0..count {
let a = rng.next_u32();
let b = rng.next_u32();
let c = rng.next_u32();
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
if ab_c != a_bc {
return Ok((
i + 1,
Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
));
}
}
Ok((count, None))
}
AlgebraicLaw::Identity { element } => {
check_identity_witnessed(op_id, f, *element, count, &grid)
}
AlgebraicLaw::LeftIdentity { element } => {
crate::proof::algebra::laws::one_sided::check_identity_witnessed_u32(
op_id,
f,
crate::proof::algebra::laws::one_sided::Side::Left,
*element,
count,
)
}
AlgebraicLaw::RightIdentity { element } => {
crate::proof::algebra::laws::one_sided::check_identity_witnessed_u32(
op_id,
f,
crate::proof::algebra::laws::one_sided::Side::Right,
*element,
count,
)
}
AlgebraicLaw::SelfInverse { result } => {
check_self_inverse_witnessed(op_id, f, *result, count)
}
AlgebraicLaw::Idempotent => check_idempotent_witnessed(op_id, f, count),
AlgebraicLaw::Absorbing { element } => check_absorbing_witnessed(op_id, f, *element, count),
AlgebraicLaw::LeftAbsorbing { element } => {
crate::proof::algebra::laws::one_sided::check_absorbing_witnessed_u32(
op_id,
f,
crate::proof::algebra::laws::one_sided::Side::Left,
*element,
count,
)
}
AlgebraicLaw::RightAbsorbing { element } => {
crate::proof::algebra::laws::one_sided::check_absorbing_witnessed_u32(
op_id,
f,
crate::proof::algebra::laws::one_sided::Side::Right,
*element,
count,
)
}
AlgebraicLaw::Bounded { lo, hi } => check_bounded_witnessed(op_id, f, *lo, *hi, count),
AlgebraicLaw::ZeroProduct { holds } => check_zero_product_witnessed(op_id, f, *holds, count),
AlgebraicLaw::DistributiveOver { over_op } => {
crate::proof::algebra::laws::distributive::check_witnessed_u32(op_id, f, over_op, count)
}
AlgebraicLaw::Complement {
complement_op,
universe,
} => crate::proof::algebra::laws::complement::check_binary_witnessed_u32(
op_id,
f,
complement_op,
*universe,
count,
),
AlgebraicLaw::LatticeAbsorption { dual_op } => {
Ok(crate::proof::algebra::laws::lattice::check_witnessed_u32(op_id, f, dual_op, count))
}
AlgebraicLaw::InverseOf { op } => {
crate::proof::algebra::laws::inverse::check_witnessed_u32(op_id, f, op, count)
}
AlgebraicLaw::Trichotomy {
less_op,
equal_op,
greater_op,
} => crate::proof::algebra::laws::trichotomy::check_witnessed_u32(
op_id, f, less_op, equal_op, greater_op, count,
),
AlgebraicLaw::Custom {
name, arity, check, ..
} => Ok(crate::proof::algebra::laws::custom::check_witnessed_u32(
op_id, f, name, *arity, *check, count,
)),
other => Ok((0, Some(LawViolation {
law: format!("{:?}", other),
op_id: op_id.to_string(),
message: format!("unimplemented binary witnessed law checker for {:?}. Fix: add a real checker or remove the declared law.", other),
a: 0, b: 0, c: 0, lhs: 0, rhs: 0,
}))),
}
}