How To Evolve Reasoners
A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour, or to match additional proof rules, even after the old implementation was used to prove models. This leads to various issues, from unexpected proving failures to global prover unsoundness.
This is why successive implementations of a reasoner have to be distinguished, so that proofs using older implementations get detected by the tool as broken.
But a reasoner evolution is sometimes conservative and does not require to consider proofs broken if they use the implementation of the reasoner prior to the evolution.
In order to deal with these various cases, notions of version and level have been defined.
This page is dedicated to explaining these notions and describing exactly what to do to keep the prover sound.
What happens if I do nothing ?
The consequences of doing nothing besides functional code changes entails that proofs made using old reasoner implementation will be left unnoticed. Thus, if we clean a project in order to update proof statuses, these proofs will be considered reusable (in the sense of org.eventb.core.seqprover.ProverLib.isProofReusable() ) and their status will be left unchanged, i.e potentially discharged even if the new reasoner implementation would fail where the older succeeded. But if we make a replay on these proofs, the new reasoner implementation will be used and the correct status will be found.
So we get a difference between reusability and replayability, which makes the prover globally unstable and potentially unsound.
Versions and Levels
Roughly speaking:
| levels | 
|
backward compatible changes |
| versions |
|
non backward compatible changes |
Backward compatibility here is to be understood as: if the previous implementation can be applied to a sequent, then the new implementation can be applied seamlessly to the same sequent.
That is, given the same input, if the previous implementation succeeds and produces an output (a proof rule), then the new implementation also succeeds and produces exactly the same output (in particular the same antecedents, goal and needed hypotheses).
A new version is made through the IVersionedReasoner interface, by either starting to implement it (returning version 0) if the previous reasoner was not versioned, or incrementing the version.
A new level is created using a new reasoner, that extends the behaviour of the existing one. In practice, as is done by AutoRewrites and AutoRewritesL1, the various reasoners can use the behaviour of a third class (AutoRewriterImpl in this case), which is itself parameterized by the level. It means that the code for additional matches is conditioned by the actual level (not executed for level 0, executed for level 1 and more).
To summarize:
- Reasoner versions:
- when a bug is fixed in a reasoner, its version shall be increased so that all POs that could use the faulty version are checked again with the fixed version at the next build.
- It is OK to add more functionality to a reasoner, that is process more cases than before (e.g., accept new inputs or new sequents). There is no need to change the reasoner version in this case, as it is fully backward compatible.
- Reasoner level:
- when one wants to change the behaviour of a reasoner (for instance, the former behaviour was correct but not optimal), a new level of the reasoner shall be created. Levels are just a matter of convention, in fact each level is a reasoner by itself. However, levels share a large code basis to avoid copy-pasted code. It is very important to retain the original level, so that existing proofs do not get broken.
How to decide what to do
TODO: make a decision tree and describe precisely what to do and how to proceed
