Commit f06aa0e0 authored by Ralf Jung's avatar Ralf Jung

port to gen_proofmode

parent deacc8fc
Pipeline #10042 passed with stage
in 13 minutes and 23 seconds
......@@ -26,20 +26,20 @@ variables:
## Build jobs
build-coq.8.7.1:
build-coq.8.8.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1 coq-mathcomp-ssreflect version 1.6.4"
OPAM_PINS: "coq version 8.8.0"
build-coq.8.6.1:
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
OPAM_PINS: "coq version 8.7.1"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1 coq-mathcomp-ssreflect version 1.6.4 coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
OPAM_PINS: "coq version 8.7.1 coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
except:
only:
- triggers
......
......@@ -6,8 +6,7 @@ Atomicity related verification based on Iris logic.
This version is known to compile with:
- Coq 8.6.1 / 8.7.1
- Ssreflect 1.6.4
- Coq 8.7.1 / 8.8.0
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
## Building from source
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.2018-02-21.1") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-05.5.4946e270") | (= "dev") }
]
......@@ -67,14 +67,14 @@ Section atomic_sync.
(* we should view shift at this point *)
iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. subst.
iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
{ iApply "Hseq". iFrame. done. }
iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
rewrite Qp_div_2.
iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I
with "[Hg]" as ">[Hg1 Hg2]".
......
......@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import auth frac agree excl agree gset gmap.
From iris.base_logic Require Import big_op saved_prop.
From iris.base_logic Require Import saved_prop.
From iris_atomic Require Import misc peritem sync.
Definition doOp : val :=
......@@ -162,10 +162,10 @@ Section proof.
* iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
* iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
wp_store. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
{ iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
iRight. iExists _, v. iFrame. iExists Q. iFrame. }
iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
......
......@@ -3,7 +3,8 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.base_logic Require Import big_op auth fractional.
From iris.bi Require Import fractional.
From iris.base_logic Require Import auth.
Import uPred.
......@@ -63,9 +64,9 @@ Section pair.
Context {A : ofeT} `{EqDecision A, !OfeDiscrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) own γm (q2, to_agree a2) a1 = a2.
own γm (q1, to_agree a1) - own γm (q2, to_agree a2) - a1 = a2.
Proof.
iIntros "[Ho Ho']".
iIntros "Ho Ho'".
destruct (decide (a1 = a2)) as [->|Hneq]=>//.
iCombine "Ho" "Ho'" as "Ho".
iDestruct (own_valid with "Ho") as %Hvalid.
......@@ -75,11 +76,11 @@ Section pair.
Qed.
Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) own γm (q2, to_agree a2)
own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
own γm (q1, to_agree a1) - own γm (q2, to_agree a2)
- own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
Proof.
iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
iIntros "Ho Ho'".
iDestruct (m_frag_agree with "Ho Ho'") as %Heq.
subst. iCombine "Ho" "Ho'" as "Ho".
by iFrame.
Qed.
......
......@@ -3,7 +3,6 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op.
From iris_atomic Require Export treiber misc.
From iris.base_logic.lib Require Import invariants.
......
......@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op.
From iris_atomic Require Import atomic misc.
Definition new_stack: val := λ: <>, ref (ref NONE).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment