Soundness bug: axioms are used wrongly during induction

[meiersi]

During polishing the section on trace induction in my thesis, I discovered a bug in the use of axioms during induction proofs. The problem is that axioms may filter the traces such that they are no longer prefix-closed. Trace induction is however only sound for prefix-closed sets of traces. Thus it is not sound to use the axioms as-is during the constraint solving, when using trace induction.

What we have to do is to extend the formula initially with all axioms in scope and then apply trace induction. This interacts however badly with the current implementation of precomputed case distinctions, which exploit all axioms in their original form.

The short-term fix is to add the axioms as additional conjuncts to the formula describing the counter-examples. Then, they will also be transformed by the application of trace induction. We can add axioms of the form All x1 ... xn. guards => no existential quantifier directly to the precomputed case distinctions, as these axioms leave the set of traces prefix-closed.

The long-term fix is to additionally refine the precomputed case distinctions with the local assumptions that are available. This requires changing the code for applying induction and inventing an additional user-interface for switching between using induction and not using it (for easy experimentation in the GUI).

[meiersi]

Tamarin's current output:

==============================================================================
summary of summaries:

analyzed: examples/loops/Axioms_and_Induction.spthy

  NoStep_with_induction (all-traces): verified (5 steps)
  NoStep_without_induction (all-traces): falsified - found trace (4 steps)

==============================================================================

[meiersi]

I implement the short-term fix with the twist that safety formulas are added directly to the precomputed case distinctions. This is OK, as safety formulas leave the set of traces prefix-close, which is the key requirement for induction.