Logically atomic stack

This relies on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/163 being merged.

added 3 commits

• 8e5226e3 - use wp_atomic_intro to get rid of the HQ everywhere
• 69e13045 - change HoCAP stack to use the style from concurrent_stacks with an invariant…
• 381ee83a - change HoCAP spec to make updates laterable, now it is really equivalent to the logatom spec

Compare with previous version

mentioned in merge request !5 (merged)

added 30 commits

• 381ee83a...b5a80fab - 21 commits from branch ci/gen_proofmode
• ecb83485 - Start with logically atomic stack: Write the code
• 5e08e49b - define the protocol and prove the constructor
• d33376ef - prove stack push
• 42c9c90b - prove stack pop; add general stack interface
• d3e97a4a - add abstract HoCAP-style spec and show that it implies the logically atomic one
• 37813ecd - show that logatom-spec implies hocap-spec EXCEPT for the Laterable restriction
• c529368f - use wp_atomic_intro to get rid of the HQ everywhere
• 204cbc28 - change HoCAP stack to use the style from concurrent_stacks with an invariant…
• 06ddf2dd - change HoCAP spec to make updates laterable, now it is really equivalent to the logatom spec

Compare with previous version

added 10 commits

• e2ed288f - 1 commit from branch ci/gen_proofmode
• 5abfb378 - Start with logically atomic stack: Write the code
• f09184d1 - define the protocol and prove the constructor
• c217df5b - prove stack push
• 3469e629 - prove stack pop; add general stack interface
• 23ce16de - add abstract HoCAP-style spec and show that it implies the logically atomic one
• 768a5c66 - show that logatom-spec implies hocap-spec EXCEPT for the Laterable restriction
• c070ea31 - use wp_atomic_intro to get rid of the HQ everywhere
• fc5cc7b1 - change HoCAP stack to use the style from concurrent_stacks with an invariant…
• 15e0affa - change HoCAP spec to make updates laterable, now it is really equivalent to the logatom spec

Compare with previous version

changed the description

added 12 commits

• 15e0affa...55a5f016 - 3 commits from branch ci/gen_proofmode
• e7af1313 - Start with logically atomic stack: Write the code
• d4e03b2f - define the protocol and prove the constructor
• 2b557384 - prove stack push
• 7fc8bf99 - prove stack pop; add general stack interface
• 9cc815ff - add abstract HoCAP-style spec and show that it implies the logically atomic one
• 429749d3 - show that logatom-spec implies hocap-spec EXCEPT for the Laterable restriction
• dff52a6d - use wp_atomic_intro to get rid of the HQ everywhere
• a7197975 - change HoCAP stack to use the style from concurrent_stacks with an invariant…
• a0ffac05 - change HoCAP spec to make updates laterable, now it is really equivalent to the logatom spec

Compare with previous version

added 9 commits

• a0ffac05...2645095c - 4 commits from branch ci/gen_proofmode
• 529e8cc5 - Start with logically atomic stack: Write the code
• cdd05583 - define the protocol and prove the constructor
• abf1398f - prove stack push
• 581d5977 - prove stack pop; add general stack interface
• 3c5dc336 - add abstract HoCAP-style spec and show that it implies the logically atomic one

Compare with previous version

added 1 commit

• 5e08dafd - add abstract HoCAP-style spec and show that it implies the logically atomic one

Compare with previous version

added 3 commits

• 9e7035a1 - prove stack push
• 011326d1 - prove stack pop; add general stack interface
• d040ec55 - add abstract HoCAP-style spec and show that it implies the logically atomic one

Compare with previous version

added 10 commits

• d040ec55...7c7bc060 - 10 commits from branch ci/gen_proofmode

Compare with previous version

changed target branch from ci/gen_proofmode to master

unmarked as a Work In Progress

mentioned in commit 65e38263

merged