[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Fri, 3 Feb 2023 18:34:19 -0800 (PST)*References*: <3013f244-3482-4c43-b909-5980ad030157n@googlegroups.com>

Nothing to contribute here other than I saw that repo in my github feed the other day and it looks great! Hope you'll decide to contribute it to the TLA+ examples repo.

Andrew

On Friday, February 3, 2023 at 5:10:07 PM UTC-5 uguryag...@xxxxxxxxx wrote:

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?The proofs I refer to can all be found in this GitHub repository.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/71da8af1-5463-4a0f-bb8c-1b45f4f7b55an%40googlegroups.com.

**References**:**[tlaplus] Good TLAPS practices for reproducible verification of proofs***From:*Ugur Yagmur Yavuz

- Prev by Date:
**[tlaplus] Good TLAPS practices for reproducible verification of proofs** - Next by Date:
**Re: [tlaplus] Good TLAPS practices for reproducible verification of proofs** - Previous by thread:
**[tlaplus] Good TLAPS practices for reproducible verification of proofs** - Next by thread:
**Re: [tlaplus] Good TLAPS practices for reproducible verification of proofs** - Index(es):