Module xor 

A checked specialist for affine systems of EVM word XOR equalities.

Gaussian elimination proposes either a model or a set of source equations whose XOR is contradictory. Neither answer is trusted: models are evaluated against the entire original query, and the certificate checker cancels terms in the original source equations without consulting the elimination rows. Unsupported queries and exhausted work budgets fall through.

Re-exports

use super::*; 🔒

Structs

Relation 🔒

Row 🔒

Enums

CheckedXorResult 🔒

Constants

MAX_XOR_ATOMS 🔒

MAX_XOR_ROWS 🔒

MAX_XOR_VISITS 🔒

Functions

affine_terms 🔒

Recovers equalities compiled as ISZERO(ADD(word, constant)) or ISZERO(SUB(a, b)). Only the equality boundary admits these rewrites: addition inside an XOR remains opaque because carries are not linear over GF(2). Every constant operation wraps at EVM word width.

asserted_relations 🔒

Collects asserted equalities and disequalities. Negated conjunctions cannot supply relations.

check_certificate 🔒

Checks a contradiction certificate by XORing selected source equalities directly. All opaque terms must cancel, leaving 0 = nonzero, or 0 != 0 for a disequality certificate. This is a necessary contradiction even when atoms are related (e.g. x and x & mask); no independence assumption is used to establish UNSAT.

checked_xor_result 🔒

Returns only independently checked answers, using the original, unnormalized constraints.

is_affine_op 🔒