Irrelevant Axiom Transform

[shigoel]

Summary

Reimplements the irrelevant axiom removal feature (originally drafted in PR #524) with a cleaner architecture and proven termination of helper functions.

Key changes:

• IrrelevantAxiomsMode enum (Options.lean): Replaces the old removeIrrelevantAxioms : Bool with .Off, .Aggressive, and .Precise modes, giving callers explicit control over the tradeoff between pruning aggressiveness and soundness risk.

• Caching (IrrelevantAxioms.lean): A Cache struct (function call graph + axiom map) is built once per program and reused across all per-goal queries, avoiding redundant recomputation.

• Builtin exclusion (CallGraph.lean): Builtins are excluded from the function-to-axiom map because they appear in nearly every axiom, which would otherwise collapse the relevance filter.

• Proven termination: The fixed-point computation in computeRelevantAxioms now has a Lean-verified termination proof instead of relying on a fuel counter.

• Precise mode correctness fix: Axiom-labeled path conditions are excluded from the antecedent function extraction. Without this, axiom bodies would seed the relevant set, making everything relevant and removing nothing.

• Cover obligations never prune: Removing axioms from cover VCs is unsound (it weakens path conditions), so pruning is skipped for those.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[shigoel]

@aqjune-aws @keyboardDrummer It was easier to reimplement this than deal with merge issues with the older PR. I accommodated your comments in the older PR (#524), but ideas like pruning irrelevant assumptions are left out of scope.

[keyboardDrummer]

Copying some comments from the previous PR:

---

Are triggers for quantifiers not used to enable ignoring the body? Boogie does this in its pruning algorithm. Explanation from Claude:

Consider:

axiom forall x, y :: {P(x, y), Q(y)} {R(x)} P(x, y) ==> R(x)

This axiom has two trigger groups: {P, Q} and {R}. The axiom becomes relevant if either all symbols in a trigger group are reachable, or if R alone is reachable. So trigger group {P, Q} becomes a "merge node" — both P and Q must be visited before the axiom is reachable through that path. Trigger group {R} is a simple single-symbol incoming edge.

For triggered forall in positive position (and exists in negative position), the axiom body's incoming edges are discarded — only the trigger-derived incoming edges are kept. This is sound because the solver can only instantiate those quantifiers via their triggers.

(Back to Remy) My gut feeling is that the above is both more precise and more accurate than what you're doing with the aggressive mode. I think the tracking of positivity is a generalization of your differentiation between antecedent and consequent.

Relevant previous PRs on this topic:

• Pruning axioms and functions boogie-org/boogie#427

---

Soundness documentation is included: axiom removal is sound for deductive verification

Shouldn't it be both sound and complete? If axioms that I need for a proof are deleted, what good is the feature?

Aggressive is better for finding counterexamples (fewer axioms → solver can
negate the goal more easily);

I don't understand that. By counterexample, do you mean the model given by the solver but only when it returns sat for PathCondition ^ !AssertCondition ? Are you saying fewer axioms means it's more likely to return sat ? That surprises me. I would have thought axioms make it easier to prove sat.

[keyboardDrummer]

It seems the new aggressive pruning feature is left untested and unused. My feeling is that it might be simpler to leave the aggressive pruning option out in this PR.