BooleanOptimizer

Boolean-algebra simplification on SIR, run before lowering.

Every rule here must be semantics preserving, not just truth-table preserving: in UPLC a subterm can Error or trace, so a rule may never drop an operand that the original expression would have evaluated. And/Or/Not all lower to SIR.IfThenElse (scalus.compiler.sir.lowering.Lowering):

And(a, b) => if a then b     else false
Or(a, b)  => if a then true  else b
Not(a)    => if a then false else true

so a is always evaluated and b only conditionally. That asymmetry decides which folds are legal - see mkAnd/mkOr.

Implemented rules:

• double negation: Not(Not(a)) => a
• conditional negation: If(Not(c), t, f) => If(c, f, t) (saves one Case/ifThenElse)
• reverse De Morgan (one node fewer): Or(Not(a), Not(b)) => Not(And(a, b)) and And(Not(a), Not(b)) => Not(Or(a, b))
• constant folding of Not, and of If with a constant condition
• identity/annihilation folds that do not drop an evaluated operand

Deliberately NOT implemented, because they drop an operand the original evaluates: a && !a => false, a || !a => true, And(a, false) => false, Or(a, true) => true, If(c, t, t) => t. Idempotence (a && a => a) is out for the same reason: it evaluates a once where the original evaluates it twice, halving a duplicated trace.

The pass is a single bottom-up rebuild: children are optimized first, then the smart constructors apply the rules to already-optimized children. Rules never re-enter a full traversal, so the cost is linear in the tree size.