fix: exactly_one/1 produces wrong results for N > 2 variables

[matt-beanland]

Summary

Expression.exactly_one/1 uses a binary fold with nand/2 that incorrectly treats the accumulated compound expression as a single variable at each step. For N > 2 variables this produces logically wrong results: assignments that should be rejected are accepted, and vice versa.

The fix uses the standard encoding: at_least_one (OR of all variables) combined with at_most_one/1 (pairwise negation). This is semantically correct for any N.

Impact

• Crux.exactly_one/1 is the recommended replacement for the deprecated AshPolicy.Expr.mutually_exclusive_and_collectively_exhaustive/1. Any Ash policy using N > 2 mutually exclusive predicates via Crux.exactly_one/1 will produce incorrect access control decisions.
• The bug also causes unnecessary expression expansion for large N, contributing to performance issues in Formula.from_expression/1.

Changes

• Fix exactly_one/1 to use at_most_one/1 combined with an OR of all variables
• Update doctest to reflect the corrected output
• Add tests for N=3 and N=4 covering all cases: each singleton valid, all pairs invalid, all-true invalid, none-true invalid, SAT solver round-trip

Test plan

• mix test test/crux/expression_test.exs — all 90 tests + 48 doctests pass
• Verify N=2 behaviour is unchanged
• Verify N=3: exactly one of three valid, all pairs rejected
• Verify N=4 via SAT solver: two-true is unsatisfiable, one-true is satisfiable