Hi all! After working on a few non-trivial medium-to-long length TLAPS proofs, as a general problem, I noticed that a number of proof obligations that went through without issues at the time of writing the proof and its initial verification, would inevitably fail to go through when the module was rerun without caches to reproduce the verification of the proof.
In my experience, the failure of these proof obligations was not deterministic, with unpredictable changes across different systems, and even on the same system across different runs without proof caches. Most of these obligations were usually deeper down in the proof (1500-2000+ lines into the proof), and their failure seems almost always easily resolvable (in my case, I have been able to resolve all such issues within minutes, some within seconds). I mainly observed three groups of failing proof obligations:
* Some failing proof obligations can be easily verified once again by running at the leaf level.
* Others can be made to go through by specifying a back-end and a timeout duration (sometimes specifying SMTT(5), which is the first back-end when no back-ends are specified, and by default is invoked with a 5 second timeout, can make a difference).
* In rarer cases, hiding facts that did not require any hiding at the time of the initial verification of the proof is required.
Regardless of how simple it is to get the stumbling proof obligations to go through once again, I ideally would like them to be verifiable on any system with an up-to-date installation of TLAPS without modifications. Are there any TLAPS practices that would help ensure such consistency? In particular, is it possible to certify that a TLAPS proof has been verified?
Ugur Y. Yavuz
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/3013f244-3482-4c43-b909-5980ad030157n%40googlegroups.com.