Fix unsound relaxation of contradictory pure range constraints

[wstran]

Fixes #3748 (reported by @N0zoM1z0).

Problem

optimize_range_constraints (autoprecompiles/src/range_constraint_optimizer.rs) removes the pure range constraints of all unconditional bus interactions and merges them per expression with RangeConstraint::conjunction. When two merged constraints are mutually exclusive — e.g. one bus interaction forces x = 1 and another forces x = 2 — conjunction cannot represent an empty range and falls back to {0} (interval_intersection(...).unwrap_or((0, 0))). The optimizer then re-emits this relaxed x = 0, turning an unsatisfiable system into a satisfiable one.

This contradicts the invariant documented on batch_make_range_constraints: "For soundness, the implementation should never relax the range constraint."

Minimal illustration of the underlying behaviour:

let a = RangeConstraint::from_value(F::from(1));
let b = RangeConstraint::from_value(F::from(2));
assert!(a.is_disjoint(&b));                          // 1 and 2 share no value
assert!(a.conjunction(&b).allows_value(F::from(0))); // yet the conjunction allows 0

Fix

While merging, detect the contradiction with RangeConstraint::is_disjoint. If any pair of pure range constraints for the same expression is disjoint, the original system is unsatisfiable, so instead of relaxing it we record an explicit unsatisfiable constraint (1 = 0) and return, keeping the system unsatisfiable. is_disjoint already distinguishes a genuine contradiction from a normal narrowing intersection, so compatible constraints are unaffected.

Tests

Two regression tests in range_constraint_optimizer:

• contradictory_pure_range_constraints_stay_unsatisfiable: two unconditional pure range constraints forcing x to be both 1 and 2 keep the system unsatisfiable instead of being relaxed to x = 0.
• compatible_pure_range_constraints_are_not_flagged: compatible constraints are not treated as a contradiction.

cargo test -p powdr-autoprecompiles (including test_apc_reth) and cargo test -p powdr-constraint-solver pass; cargo clippy --all-targets -- -D warnings and cargo fmt --check are clean.

Note on the approach

This is a minimal, self-contained fix that preserves unsatisfiability. An alternative would be to give RangeConstraint an explicit empty/unsatisfiable state and thread it through conjunction and its callers, which is a larger change; happy to go that route instead if you prefer.

[chriseth]

Thank you for your pull request! While it could be considered a bug, we are not too much concerned about turning an unsatisfiable system into a satisfiable. This is an optimizer, so it assumes the original system is satisfiable.

Furthermore, you are right with your analysis that a better fix would be to change RangeConstraint to give it an explicit "unsatisfiable" state. This is a considerable change that could have implications across the code base, so I'm not sure if this effort should be undertaken.

[wstran]

Thanks @chriseth — that lines up with what I found. To put a number on the satisfiable-input assumption: I instrumented the merge loop and ran the optimizer over the bundled APC fixtures (ecrecover, keccak, sha256, reth, etc.) — 16,562 same-expression range-constraint merges, 0 of them contradictory. So contradictions don't arise in practice, and I agree the explicit "unsatisfiable" RangeConstraint state isn't worth the cross-cutting change right now.

That makes this PR just cheap defensive hardening: one extra is_disjoint check per merge to guard a case that never fires. Happy to leave it as a small guard or close it — whichever you prefer. Thanks for taking a look!