Enable bounded cross-multiplication of inequations in DefOps

[unp1]

Intended Change

A regularly occuring problem (at least in my case) is that KeY could not close a proof on DefOps and I had to switch to Model Search which closed it.

What closed the problem at the end was the use of the cross multiplication not the systematic suts or equation saturation performed by Model Search.

An example that could not be proven w/o switching to Model Search is

public class MatrixImplem {    
    //@ public invariant x>=0 && y>=0;
    private final int x;
    private final int y;
        
    //@ public invariant matrix_implem.length == x * y; 
    private /*@spec_public @*/ int[] matrix_implem;   
        
    /*@ public normal_behavior
      @ requires i >= 0 && i < x && j >= 0 && j < y;
      @ ensures \result == matrix_implem[x * j + i];
      @ assignable \strictly_nothing;
      @*/
    public /*@ pure @*/ int get (int i, int j) {
        return matrix_implem[x * j + i];
    }   
}

The reason why cross multiplication handling was not on DefOps is that it could drown out other theories. This PR activates cross-multiplication in a restricted form for DefOps. The cross multiplication rules are restricted to cases where the product of the left-hand sides of the involved inequations occurs on some other inequation on the left side too.

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base: Only changes to the rulesets not to the soundness critical rule core

Ensuring quality

• New regression test DefOpsCrossMultiplicationTest with the pure arithmetic
  core of the matrix obligation (crossMultDefOps.key): closes with DefOps
  (new) and with Model Search (as before), stays open with Basic.
• Full runAllProofs on the branch: 674/674 proofs, 0 failures.
• Examples using Model Search verified byte-identical on an arithmetic proof corpus (identical
  node counts).
• No effect on existing proofs: every DefOps example of the runAllProofs corpus
  (189 entries) was proven with and without this change; all 180 closing proofs
  come out node-for-node identical, none changes its provable/unprovable
  outcome. Cross-multiplication fires in none of them — the exactly-bounded
  restriction admits it only where it is actually needed, so the existing proof
  search is untouched and only the previously unprovable obligations gain.
• Runtime cost of the added bounding check, measured on the ten most
  inequation-dense DefOps examples: it is skipped entirely (zero evaluations) on
  six of them, because the cheap monomial/polynomial filters reject before the
  check runs. The heaviest example in the corpus
  (standard_key/arith/gemplusDecimal/add.key) performs 0.76 evaluations per
  proof node at roughly 4 µs each, i.e. about 1% of its automode time — below
  the run-to-run spread of the unmodified prover on the same example (~10%).
• Thread-safety and determinism (the change lives in the strategy cost
  machinery, which the multi-core prover shares between goals):
  FeatureStatelessnessLintTest and SharedStateLintTest pass without
  allowlist entries; testMt2w (single-core reproducibility gate
  ScDeterminismTest + 2-worker corpus), testMt4w, and the parallel-prover
  determinism/equivalence tests all pass. No mutable state is added: the
  bounding features are stateless and their term buffers keep their values in
  the per-evaluation MutableState.

Additional information and contact(s)

The strategy-side surface of this PR (per-mode bindings in IntegerStrategy)
overlaps with the value-preserving cost refactoring in #3904; whichever lands
second needs a small mechanical rebase there.

PR created with AI tooling support.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.