scalus.compiler.sir.transform

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.

Removes the specification clauses of scalus.cardano.onchain.plutus.prelude.Spec from SIR, before it is lowered.

A clause is a call of a function of the Spec module, which the compiler plugin leaves in the SIR as it leaves any call, so that a verifier can read it there. It is not part of the script:

• Spec.expects(c) and Spec.ensures(c) are removed, with their conditions, which are not evaluated;
• body.ensuring(r => c) becomes body;
• the definitions of the Spec functions, which linking put around the code, are dropped, and so is the definition of a function that only the clauses used: a function written for the specification is no part of the script either.

The definitions that are left are nested again in the order the code alone gives. What comes out is the SIR of the same code written without the clauses, so its script has the same bytes. Code without clauses is returned as it is.

Static-argument transformation (T1 of docs/internal/CODEGEN_IMPROVEMENT_PLAN.md).

A parameter of a single-binding recursive Let is static when every self-call passes exactly that parameter's own variable in the same position. Static parameters are bound once by a wrapper lambda, and the inner recursion re-passes only the changing ones:

 let rec f = λp1...pn. body                     // some pi static in every self-call
 -->
 let f = λp1...pn.
     let rec f$sat = λq1...qk. body[ f e1...en := f$sat e_q1...e_qk ]
     in f$sat q1...qk                           // q = changing params, in source order

When the static parameters form a prefix (the common case, e.g. go f n acc with an invariant f) a leaner shape is used instead - the wrapper binds only the static prefix and returns the fixpoint itself, so the changing parameters are consumed by f$sat directly:

 let f = λp1...pj. let rec f$sat = λq1...qk. body' in f$sat

The wrapper keeps the original name, arity and type, so external uses of f (partial applications, higher-order uses, eta-lets) are unaffected. The fixpoint is built once per entry into f instead of once per iteration, and each iteration saves one Apply per lifted argument.

The transform is skipped (input returned unchanged) when it cannot be proven safe:

• multi-binding recursive Lets (mutual-recursion groups) and lazy lets;
• a rhs that is not a lambda, or has duplicate parameter names;
• any self-reference that is not the head of a self-call saturated to full arity (a bare reference or a partial application could observe the original arity);
• no static parameter at all.

If every parameter is static the last one is demoted to changing, because a nullary strict letrec would diverge.

Runs only when optimization is enabled - see scalus.compiler.sir.lowering.UplcPipeline.run, which is the single place this pass is invoked from. It runs after MutualRecursionElimination, so the peers-as-params static arguments that pass introduces (a $mutrec peer re-passing f1 .. f(i-1) unchanged on every self-call) are lifted here too.