use crate::proof::algebra::checker::support::{call_binary, call_unary, engine_failure_violation, violation};
use crate::spec::law::{AlgebraicLaw, LawViolation};
pub(super) fn rebuild_binary_violation(
op_id: &str,
f: fn(&[u8]) -> Vec<u8>,
law: &AlgebraicLaw,
a: u32,
b: u32,
c: u32,
) -> Result<Option<LawViolation>, LawViolation> {
match law {
AlgebraicLaw::Commutative => {
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 {
Ok(Some(violation(op_id, "commutative", a, b, 0, ab, ba)))
} else {
Ok(None)
}
}
AlgebraicLaw::Associative => {
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 {
Ok(Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)))
} else {
Ok(None)
}
}
AlgebraicLaw::Identity { element } => {
let e = *element;
for x in [a, b] {
let xe = call_binary(f, x, e).map_err(|e| engine_failure_violation(op_id, e))?;
if xe != x {
return Ok(Some(violation(op_id, "identity(right)", x, e, 0, xe, x)));
}
let ex = call_binary(f, e, x).map_err(|e| engine_failure_violation(op_id, e))?;
if ex != x {
return Ok(Some(violation(op_id, "identity(left)", e, x, 0, ex, x)));
}
}
Ok(None)
}
AlgebraicLaw::LeftIdentity { element } => {
let e = *element;
let ea = call_binary(f, e, a).map_err(|e| engine_failure_violation(op_id, e))?;
if ea != a {
Ok(Some(violation(op_id, "left-identity", e, a, 0, ea, a)))
} else {
Ok(None)
}
}
AlgebraicLaw::RightIdentity { element } => {
let e = *element;
let ae = call_binary(f, a, e).map_err(|e| engine_failure_violation(op_id, e))?;
if ae != a {
Ok(Some(violation(op_id, "right-identity", a, e, 0, ae, a)))
} else {
Ok(None)
}
}
AlgebraicLaw::SelfInverse { result } => {
let r = *result;
for x in [a, b] {
let xx = call_binary(f, x, x).map_err(|e| engine_failure_violation(op_id, e))?;
if xx != r {
return Ok(Some(violation(op_id, "self-inverse", x, x, 0, xx, r)));
}
}
Ok(None)
}
AlgebraicLaw::Idempotent => {
for x in [a, b] {
let xx = call_binary(f, x, x).map_err(|e| engine_failure_violation(op_id, e))?;
if xx != x {
return Ok(Some(violation(op_id, "idempotent", x, x, 0, xx, x)));
}
}
Ok(None)
}
AlgebraicLaw::Absorbing { element } => {
let z = *element;
for x in [a, b] {
let xz = call_binary(f, x, z).map_err(|e| engine_failure_violation(op_id, e))?;
if xz != z {
return Ok(Some(violation(op_id, "absorbing(right)", x, z, 0, xz, z)));
}
let zx = call_binary(f, z, x).map_err(|e| engine_failure_violation(op_id, e))?;
if zx != z {
return Ok(Some(violation(op_id, "absorbing(left)", z, x, 0, zx, z)));
}
}
Ok(None)
}
AlgebraicLaw::LeftAbsorbing { element } => {
let z = *element;
let za = call_binary(f, z, a).map_err(|e| engine_failure_violation(op_id, e))?;
if za != z {
Ok(Some(violation(op_id, "left-absorbing", z, a, 0, za, z)))
} else {
Ok(None)
}
}
AlgebraicLaw::RightAbsorbing { element } => {
let z = *element;
let az = call_binary(f, a, z).map_err(|e| engine_failure_violation(op_id, e))?;
if az != z {
Ok(Some(violation(op_id, "right-absorbing", a, z, 0, az, z)))
} else {
Ok(None)
}
}
AlgebraicLaw::Bounded { lo, hi } => {
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
if ab < *lo || ab > *hi {
Ok(Some(violation(op_id, "bounded", a, b, 0, ab, *lo)))
} else {
Ok(None)
}
}
AlgebraicLaw::ZeroProduct { holds: true } => {
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
if ab == 0 && a != 0 && b != 0 {
Ok(Some(violation(op_id, "zero-product(true)", a, b, 0, ab, 1)))
} else {
Ok(None)
}
}
AlgebraicLaw::ZeroProduct { holds: false } => {
let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
if ab == 0 && a != 0 && b != 0 {
Ok(Some(violation(
op_id,
"zero-product(false)",
a,
b,
0,
ab,
0,
)))
} else {
Ok(None)
}
}
AlgebraicLaw::DistributiveOver { over_op } => {
relations::rebuild_distributive(op_id, f, over_op, a, b, c)
}
AlgebraicLaw::Complement {
complement_op,
universe,
} => relations::rebuild_binary_complement(op_id, f, complement_op, *universe, a, b),
AlgebraicLaw::LatticeAbsorption { dual_op } => {
relations::rebuild_lattice_absorption(op_id, f, dual_op, a, b)
}
AlgebraicLaw::InverseOf { op } => relations::rebuild_inverse(op_id, f, op, a, b),
AlgebraicLaw::Trichotomy {
less_op,
equal_op,
greater_op,
} => relations::rebuild_trichotomy(op_id, f, less_op, equal_op, greater_op, a, b),
AlgebraicLaw::Custom { .. } => relations::rebuild_binary_custom(op_id, f, law, a, b, c),
other => Ok(Some(relations::unimplemented_rebuild(
op_id, other, a, b, c,
))),
}
}