Modes for controlling irrelevant axiom removal

[shigoel]

Description of changes:

Make the detection of relevant axioms for a given function more precise. See test in irrelevantAxiomsTestPgm2 in Strata/StrataTest/Languages/Boogie/Examples/RemoveIrrelevantAxioms.lean for details.

There are three modes to choose from for detecting and removing irrelevant axioms:

• Off: do not remove any axioms.

• Aggressive: Only the functions in the consequent Q of a goal P ==> Q will be taken into account for relevant axiom analysis. This means that axioms relevant to some function in P may be removed. This is sound, but may yield unknown results from the solver.

• Precise: Functions in both P and Q of a goal P ==> Q will be considered for relevant axiom analysis. A caveat is that only the antecedents that appear after a marker called __end_of_prelude_marker will be considered as the real assumptions here.

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

[aqjune-aws]

Hi, while reviewing this PR I became to want to assure the natures of properties Strata want to reason about.

If we want to detect malformed API calls whose inputs cannot be right, would aggressively removing axioms affect the result?
For example, let's assume that f_x_must_be_negative(x) is an API call that must have x a negative number. And if we have a code:

if x in [1, 2, 3]:
  f_x_must_be_negative(x)

If the axioms about List membership is correctly encoded, Strata will correctly indicate that f_x_must_be_negative(x) can never be right.
However, if it this membership axiom was (eagerly) eliminated for some reason, the if branch being taken won't give additional information stating that x is positive.

[shigoel]

If the axioms about List membership is correctly encoded, Strata will correctly indicate that f_x_must_be_negative(x) can never be right. However, if it this membership axiom was (eagerly) eliminated for some reason, the if branch being taken won't give additional information stating that x is positive.

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver. As you noted, at worst we may not be able to prove something we need, but then axiom removal is also optional. Indeed, there are three modes: off (which should avoid the problem you brought up), aggressive (which can eliminate necessary axioms but it'd still be sound), and precise (if the relevant axioms are properly computed, we should avoid this situation).

Does this address your concern?

[joscoh]

In principle this could be proved terminating by looking at number axioms in prog - |discoveredAxioms| but maybe that is not necessary for now.

[shigoel]

Indeed -- I shied away from that proof for now. I expect we won't be using axiom removal too much after datatypes are in. This is mostly for a rainy day.

[joscoh]

Somewhere, it should probably be documented that this must occur at the end of the prelude. And what happens if there are multiple preludes/libraries being used?

[shigoel]

Totally geared towards a single prelude for now. It's a stopgap, which I acknowledge in Strata/Languages/Boogie/Verifier.lean.

[aqjune-aws]

If the axioms about List membership is correctly encoded, Strata will correctly indicate that f_x_must_be_negative(x) can never be right. However, if it this membership axiom was (eagerly) eliminated for some reason, the if branch being taken won't give additional information stating that x is positive.

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver. As you noted, at worst we may not be able to prove something we need, but then axiom removal is also optional. Indeed, there are three modes: off (which should avoid the problem you brought up), aggressive (which can eliminate necessary axioms but it'd still be sound), and precise (if the relevant axioms are properly computed, we should avoid this situation).

Does this address your concern?

To record - we had a separate chat about this and I recommended that the codebase explicitly mentions the Aggressive mode may change unsat to sat.

[joscoh]

If the axioms about List membership is correctly encoded, Strata will correctly indicate that f_x_must_be_negative(x) can never be right. However, if it this membership axiom was (eagerly) eliminated for some reason, the if branch being taken won't give additional information stating that x is positive.

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver. As you noted, at worst we may not be able to prove something we need, but then axiom removal is also optional. Indeed, there are three modes: off (which should avoid the problem you brought up), aggressive (which can eliminate necessary axioms but it'd still be sound), and precise (if the relevant axioms are properly computed, we should avoid this situation).
Does this address your concern?

To record - we had a separate chat about this and I recommened to explicitly mention in the codebase that Aggressive mode may change unsat to sat.

If the axioms about List membership is correctly encoded, Strata will correctly indicate that f_x_must_be_negative(x) can never be right. However, if it this membership axiom was (eagerly) eliminated for some reason, the if branch being taken won't give additional information stating that x is positive.

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver. As you noted, at worst we may not be able to prove something we need, but then axiom removal is also optional. Indeed, there are three modes: off (which should avoid the problem you brought up), aggressive (which can eliminate necessary axioms but it'd still be sound), and precise (if the relevant axioms are properly computed, we should avoid this situation).
Does this address your concern?

To record - we had a separate chat about this and I recommened to explicitly mention in the codebase that Aggressive mode may change unsat to sat.

I think Precise can also change unsat to sat. E.g. if you have axiom: false and it is removed.

[aqjune-aws]

Ah, right. I was implicitly assuming that existing axioms were not false.

[jimgrundy]

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver.

Just checking. Yes, so you can do this when you are proving assertions. But not if you are checking coverage/reachability.

[shigoel]

Axiom removal is sound, as long as we're relying on an unsat result from an SMT solver.

Just checking. Yes, so you can do this when you are proving assertions. But not if you are checking coverage/reachability.

Indeed, and that was June's point too. We don't have coverage checking in Strata yet (imminent), but when we do, we won't run this axiom removal bit on it.

[shigoel]

I'll re-open this PR after #314 is merged.