examples merge requestshttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests2024-02-16T12:29:02Zhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/65Fix broken proofs for improved iFrame ∃2024-02-16T12:29:02ZIke MulderFix broken proofs for improved iFrame ∃https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/64logrel: Change nat to int2024-02-15T20:24:10ZAmin Timanylogrel: Change nat to intThis MR changes logical relations. It changes the type nat in F_mu_ref_conc to int. It also adds a few missing cases in the definition of well-typed contexts.This MR changes logical relations. It changes the type nat in F_mu_ref_conc to int. It also adds a few missing cases in the definition of well-typed contexts.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/63update dependencies2023-10-30T09:26:53ZPierre Rouxupdate dependencies@jung sorry to bother you again but we need that for Coq CI@jung sorry to bother you again but we need that for Coq CIhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/62Attempt to fix Coq CI2023-03-16T10:54:43ZPierre RouxAttempt to fix Coq CICoq CI is broken since a few days because it compiles the wrong version of iris, obtained from the OPAM file here in iris-example. Merging this should fix it.Coq CI is broken since a few days because it compiles the wrong version of iris, obtained from the OPAM file here in iris-example. Merging this should fix it.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/61Attempt to fix Coq CI2023-03-12T17:51:35ZPierre RouxAttempt to fix Coq CII don't know if that's the correct way to do it, but this would fix Coq CI which is currently broken because iris-example requires a version of iris that no longer compiles with Coq master.I don't know if that's the correct way to do it, but this would fix Coq CI which is currently broken because iris-example requires a version of iris that no longer compiles with Coq master.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/60Explicitly disable native compile2022-12-05T16:53:52ZGaëtan GilbertExplicitly disable native compileOtherwise coq fails when compiled with native on because iris is compiled with native offOtherwise coq fails when compiled with native on because iris is compiled with native offhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/59Add Chase-Lev deque2023-09-24T05:15:25ZJaemin ChoiAdd Chase-Lev dequeThis MR adds logically atomic specifications and proof of Chase-Lev work-stealing deque.
Note: the proof uses a strong variant of `mono_nat_own_alloc` and a variant of LATs having extra non-atomic postconditions, so `mono_nat.v` and `at...This MR adds logically atomic specifications and proof of Chase-Lev work-stealing deque.
Note: the proof uses a strong variant of `mono_nat_own_alloc` and a variant of LATs having extra non-atomic postconditions, so `mono_nat.v` and `atomic.v` were taken from the Iris repository and edited.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/58Add parallel add example2022-11-01T18:51:27ZJonas KastbergAdd parallel add exampleAn example based on a generalization of parallel_incr, that has also
been covered in the Iris Lecture NotesAn example based on a generalization of parallel_incr, that has also
been covered in the Iris Lecture Noteshttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/57cleanup logrel2022-08-26T19:00:21ZAmin Timanycleanup logrelThis MR just cleans up the logical relations examples a bit.This MR just cleans up the logical relations examples a bit.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/56add counter with backup case study2023-07-14T04:05:59ZRalf Jungjung@mpi-sws.orgadd counter with backup case studyRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/55do not rely on make_laterable in logatom triples any more2022-08-10T19:12:59ZRalf Jungjung@mpi-sws.orgdo not rely on make_laterable in logatom triples any morePrepares for https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/835Prepares for https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/835Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/51Bump Iris2022-07-20T13:18:32ZLennard Gähergaeher@mpi-sws.orgBump Irishttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/49Added petersons algorithm as an example of sequential consistency2022-02-07T09:29:40ZJonas KastbergAdded petersons algorithm as an example of sequential consistencyA port of [Peterson's algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm)--A CAS-free lock for a fixed number of participants (here 2), that relies on sequential consistency--to HeapLang.
This is a direct port of the impleme...A port of [Peterson's algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm)--A CAS-free lock for a fixed number of participants (here 2), that relies on sequential consistency--to HeapLang.
This is a direct port of the implementation and proof presented in the [Cosmo'ICFP20](https://iris-project.org/pdfs/2020-icfp-cosmo-final.pdf) paper, available [online](https://gitlab.inria.fr/gmevel/cosmo/-/blob/master/theories/examples/peterson.v), and all credit goes to the authors (Glen Mével, Jacques-Henri Jourdan, François Pottier) for the original implementation, as the port was very straightforward.
I thought that the lock was quite cute (being CAS-free), and thus could make sense to include in the library of HeapLang (for one as evidence of how its sequentially consistent nature can be used for reasoning), although it is of course up for debate.
I am willing to improve the structure/proof if need be.
NB: Moved from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/775 per requesthttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/48Bump iris2022-01-14T14:54:50ZMatthieu SozeauBump irishttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/47Bump iris2022-01-13T17:18:51ZMatthieu SozeauBump irishttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/46Draft: Adapt to iris!750: Flip quantifiers for atomic updates2022-05-24T21:29:40ZPaolo G. GiarrussoDraft: Adapt to iris!750: Flip quantifiers for atomic updatesThis MR adapts to iris!750, so it doesn't build yet. (I've built it locally with `dune`).This MR adapts to iris!750, so it doesn't build yet. (I've built it locally with `dune`).https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/45fix names2021-07-23T16:29:41ZAmin Timanyfix namesThis MR fixes the problem with names raised in #13.This MR fixes the problem with names raised in #13.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/44Embedding of classical logic in Coq + proof mode support.2021-05-14T08:02:50ZRobbert KrebbersEmbedding of classical logic in Coq + proof mode support.This MR defines a new logic `clProp` that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of `clProp` are defined as the subset of `Prop` propositions that are stable under double n...This MR defines a new logic `clProp` that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of `clProp` are defined as the subset of `Prop` propositions that are stable under double negation, and the pure, ∨, ∃ connectives of `clProp` are defined using a double negation.
The logic `clProp` is a BI, so this MR allows one to use the proof mode to carry out proofs in classical logic, without axioms! For example:
```coq
Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
Proof.
iApply clProp.dn; iIntros "#H". iApply "H".
iRight. iIntros "HP". iApply "H". auto.
Qed.
Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
Proof.
iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
Qed.
```https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/43avoid using Hoare triples2021-02-03T16:32:50ZRalf Jungjung@mpi-sws.orgavoid using Hoare triples@robbertkrebbers some of these make me wonder if deprecating Hoare triples is really the right call... Texan triples aren't always better, in particular for higher-order specs in negative position.@robbertkrebbers some of these make me wonder if deprecating Hoare triples is really the right call... Texan triples aren't always better, in particular for higher-order specs in negative position.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/42remove logreal/heaplang in favor of POPL20 tutorial2020-10-01T12:21:48ZRalf Jungjung@mpi-sws.orgremove logreal/heaplang in favor of POPL20 tutorialFixes https://gitlab.mpi-sws.org/iris/examples/-/issues/9Fixes https://gitlab.mpi-sws.org/iris/examples/-/issues/9