Our automatic proof generator can't tell which invariants' proofs are dependent on which other invariants. So they always conservatively generate proofs that will work even if each invariant depends on each other one.
For instance, suppose we have to prove invariants I1, I2, and I3. It may be that I1 is inductive all by itself, but it could also be that it's not but I1 && I2 && I3 is inductive. We don't know which invariants together constitute an inductive invariant, so to prove that I1 is an invariant with an automatically-generated lemma, we have to emit one that proves I1 && I2 && I3 ==> I1'.
It would be useful to let the developer specify, in the recipe, that to prove a certain invariant you only need to use a certain specified set of other invariants. This would generate proofs that are faster to verify. Indeed, in some cases this feature may be necessary to prevent invariant proofs from timing out.
It might also be useful to specify that a certain invariant is not needed in any invariant proofs except its own and ones it's explicitly specified to be needed in. This way, if a certain invariant introduces too many facts (e.g., with a loosely-triggered quantifier), the developer can limit its use this way.
Our automatic proof generator can't tell which invariants' proofs are dependent on which other invariants. So they always conservatively generate proofs that will work even if each invariant depends on each other one.
For instance, suppose we have to prove invariants I1, I2, and I3. It may be that I1 is inductive all by itself, but it could also be that it's not but I1 && I2 && I3 is inductive. We don't know which invariants together constitute an inductive invariant, so to prove that I1 is an invariant with an automatically-generated lemma, we have to emit one that proves I1 && I2 && I3 ==> I1'.
It would be useful to let the developer specify, in the recipe, that to prove a certain invariant you only need to use a certain specified set of other invariants. This would generate proofs that are faster to verify. Indeed, in some cases this feature may be necessary to prevent invariant proofs from timing out.
It might also be useful to specify that a certain invariant is not needed in any invariant proofs except its own and ones it's explicitly specified to be needed in. This way, if a certain invariant introduces too many facts (e.g., with a loosely-triggered quantifier), the developer can limit its use this way.