Logically atomic triples: Notation, tactics, small example

This implements a proper infrastructure for logically atomic triples.

TODO:

• Get !161 (merged) merged.
• Get !167 (merged) merged and fix conflicts.
• CHANGELOG

mentioned in issue #29

marked as a Work In Progress

Note that this blocks https://gitlab.mpi-sws.org/FP/iris-examples/merge_requests/9 and FP/iris-atomic!7 (merged). Moreover, Marianna's work on prophecy variables is also going to be based on top of this.

added 1 commit

• 7c068703 - the rewrite problem now has an issue number

Compare with previous version

added 31 commits

• 7c068703...ffd67c09 - 17 commits from branch gen_proofmode
• f4eeb4c6 - make pm_maybe_wand a BI connective; reduce BI connectives and option combinators…
• cfbf220f - add general telescopes and telescopic BI binders and proofmode support
• 016ab04d - fix nits
• f6204b4c - Use telescopes for atomic accessors, updates and triples; improve mask handling;…
• 2b48b668 - make atomic_heap a typeclass and add some notation for it
• 62aeb889 - Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
• 0a3c0a8e - Prove that atomic triples imply "normal" triples
• 8085fcde - add a weak increment operation that knows it does not race
• 12fe0f0e - enable iMod to run an atomic update
• eb337f79 - add a tactic for the final introduction of an atomic accessor
• f2f74664 - Sequential triples with a persistent precondition and no initial quantifier are atomic
• 47536e8c - add lemma to prove atomic WP without seeing a Q
• 49a7af9a - define a general make_laterable construct and use it for atomic updates
• a9fb91bb - the rewrite problem now has an issue number

Compare with previous version

added 22 commits

• a9fb91bb...29c965ba - 8 commits from branch gen_proofmode
• a83fcb9e - make pm_maybe_wand a BI connective; reduce BI connectives and option combinators…
• d6fa3215 - add general telescopes and telescopic BI binders and proofmode support
• 162474a5 - fix nits
• 649dbeaf - Use telescopes for atomic accessors, updates and triples; improve mask handling;…
• 662ae77e - make atomic_heap a typeclass and add some notation for it
• d56701ef - Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
• a4a12fef - Prove that atomic triples imply "normal" triples
• 13700515 - add a weak increment operation that knows it does not race
• dd82455e - enable iMod to run an atomic update
• 9c3b1a36 - add a tactic for the final introduction of an atomic accessor
• 687769a5 - Sequential triples with a persistent precondition and no initial quantifier are atomic
• 4b0036f6 - add lemma to prove atomic WP without seeing a Q
• 7879979a - define a general make_laterable construct and use it for atomic updates
• f8b9b6c5 - the rewrite problem now has an issue number

Compare with previous version

changed the description

added 21 commits

• f8b9b6c5...f5defba3 - 5 commits from branch gen_proofmode
• 0c16dccd - make pm_maybe_wand a BI connective; reduce BI connectives and option combinators…
• 6d15cf39 - add general telescopes and telescopic BI binders and proofmode support
• 191a6f43 - fix nits
• 0157c46f - test and fix more telescope normalization
• 79ea27b3 - proofmode: normalize big_opL
• 310e7929 - Use telescopes for atomic accessors, updates and triples; improve mask handling;…
• da87e9c1 - make atomic_heap a typeclass and add some notation for it
• 6cda562b - Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
• 29f0dbff - Prove that atomic triples imply "normal" triples
• 501ee5be - add a weak increment operation that knows it does not race
• c0bfed5d - enable iMod to run an atomic update
• 9797d9e7 - add a tactic for the final introduction of an atomic accessor
• b1984057 - Sequential triples with a persistent precondition and no initial quantifier are atomic
• 398e8b6e - add lemma to prove atomic WP without seeing a Q
• c995c337 - define a general make_laterable construct and use it for atomic updates
• e3b00876 - the rewrite problem now has an issue number

Compare with previous version

added 10 commits

• 5c4c3a3f - make atomic_heap a typeclass and add some notation for it
• 5f09759c - Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
• 3107b7d5 - Prove that atomic triples imply "normal" triples
• f6793a03 - add a weak increment operation that knows it does not race
• 34a57694 - enable iMod to run an atomic update
• 2a969a41 - add a tactic for the final introduction of an atomic accessor
• 59fe3cea - Sequential triples with a persistent precondition and no initial quantifier are atomic
• 2e3832f7 - add lemma to prove atomic WP without seeing a Q
• 979a68a4 - define a general make_laterable construct and use it for atomic updates
• 77324782 - the rewrite problem now has an issue number

Compare with previous version

marked the checklist item Get !167 (merged) merged and fix conflicts. as completed

marked the checklist item Get !161 (merged) merged. as completed

added 16 commits

• 77324782...24656b41 - 5 commits from branch gen_proofmode
• bde1f23d - Use telescopes for atomic accessors, updates and triples; improve mask handling;…
• 43827681 - make atomic_heap a typeclass and add some notation for it
• f9877483 - Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
• 89a95ff7 - Prove that atomic triples imply "normal" triples
• e4ac4683 - add a weak increment operation that knows it does not race
• c88ed1d5 - enable iMod to run an atomic update
• 16326478 - add a tactic for the final introduction of an atomic accessor
• 2e089d80 - Sequential triples with a persistent precondition and no initial quantifier are atomic
• 0bed201a - add lemma to prove atomic WP without seeing a Q
• ecb29abc - define a general make_laterable construct and use it for atomic updates
• ab624a48 - the rewrite problem now has an issue number

Compare with previous version

unmarked as a Work In Progress

added 1 commit

• e788c208 - changelog

Compare with previous version

marked the checklist item CHANGELOG as completed

All right, this is now ready to be merged. It does not touch any files except for those that are entirely about logical atomicity, and laterable assertions (a new class of assertions I introduced for the purpose of logical atomicity).

added 33 commits

• e788c208...9a672643 - 33 commits from branch gen_proofmode

Compare with previous version

changed the description

changed target branch from gen_proofmode to master

enabled an automatic merge when the pipeline for 9a672643 succeeds

canceled the automatic merge

mentioned in commit af5611c8

merged

mentioned in issue #92 (closed)