Module check 

The soundness checker: evidence that every rule is a valid rewrite, and the proof ledger.

Obligation. For every width assignment satisfying the rule’s constraints at which the pattern can match, and every value of the parameters: if the guard holds, the pattern and the template evaluate to the same value. Guards may only talk about facts through positive proof predicates (proves, zero_bits, one_bits, nonzero, disjoint), which are monotone in fact precision; so evaluating them on the concrete values (the most precise facts possible) proves the rule sound for every sound fact engine.

Evidence is derived, never declared: exhaustive enumeration over every width assignment up to max_exhaustive_width whose parameter space fits in max_exhaustive_bits, plus boundary-biased random sampling at wide widths, half of it steered toward values that satisfy the guard.

This is testing, not proof: above the exhaustive widths a rule is only sampled. A verdict of Verdict::Sound therefore requires the guard to have held in both tiers (unless every width at which the rule applies was covered exhaustively), so a rule whose guard only holds at unsampled values cannot pass. Proof at wide widths is the SMT export’s job.

Structs

CheckConfig

How thoroughly to check.

Counterexample

Inputs on which the two sides of a rule differ.

Evidence

What the checker established about one rule.

RuleCheck

The result of checking one rule.

Enums

ExampleFailure

An #[example("input" => "output")] that does not hold.

Verdict

The verdict for one rule.

Functions

check_examples

Applies rule once, at the root, to each of its #[example] inputs and compares the result with the expected output, both parsed with a default width of 8 bits (ascribe widths, as in p:32, for others). Guards are answered by the facts of the example’s own input. The failures, in example order.

check_program

Checks every rule of a program, in parallel across threads.

check_rule

Checks one rule.