Commit 18fe6f53 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Refactor shared lemmas into common module

parent 467e6866
......@@ -62,9 +62,12 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/common.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_alt.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel/heaplang/ltyping.v
......@@ -93,7 +96,6 @@ theories/logatom/flat_combiner/peritem.v
theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
......
From Coq.Lists Require Import List.
From iris.algebra Require Import csum excl auth list gmap.
From iris.program_logic Require Import adequacy ectxi_language.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris.proofmode Require Import tactics.
(* Repeadedly introduce existential variables. *)
Ltac iExistsN := repeat iExists _.
(* Solve a goal that consists of introducing existentials, framing, and picking branches. *)
Ltac iExistsFrame :=
(repeat iExistsN || iFrame);
(done || (iLeft; iExistsFrame) || (iRight; iExistsFrame) || fail "Could not solve goal").
Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
Notation "◔ v" := ((1/4)%Qp, to_agree v) (at level 20).
Section common.
Definition locO := leibnizO loc.
Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1) - own γ (q2, to_agree v2) - v1 = v2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
Qed.
Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1)
- own γ (q2, to_agree v2)
- own γ ((q1 + q2)%Qp, to_agree v2) v1 = v2.
Proof.
iIntros "Hl1 Hl2".
iDestruct (fracAgree_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
iDestruct (own_valid with "Hl") as %Hv%pair_valid.
eauto with iFrame.
Qed.
Lemma fracAgree_update γ v w u :
own γ ( v) - own γ ( w) == own γ (1%Qp, to_agree u).
Proof.
iIntros "Hb1 Hb2".
iDestruct (fracAgree_combine with "Hb1 Hb2") as "[tok <-]".
rewrite Qp_half_half.
iApply (own_update with "tok").
by apply cmra_update_exclusive.
Qed.
Lemma fracAgree_update_one γ v u :
own γ (1%Qp, to_agree v) == own γ (1%Qp, to_agree u).
Proof.
iIntros. iApply (own_update with "[$]"). by apply cmra_update_exclusive.
Qed.
(* Maybe commit this upstream. *)
Lemma mapsto_exclusive l v1 v2 q : l ↦ᵢ v1 - l ↦ᵢ{q} v2 - False.
iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1.
Qed.
End common.
\ No newline at end of file
......@@ -5,15 +5,12 @@ From iris.program_logic Require Import adequacy ectxi_language.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
CG_queue MS_queue.
common CG_queue MS_queue.
From iris.proofmode Require Import tactics.
Definition locO := leibnizO loc.
Definition queueN : namespace := nroot .@ "queue".
Definition nodesN : namespace := nroot .@ "nodes".
Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
Definition exlTokR : cmraT := exclR (unitR).
Definition nodeStateR : cmraT := authUR mnatUR.
......@@ -32,19 +29,6 @@ Section Queue_refinement.
Notation D := (prodO valO valO -n> iPropO Σ).
(* Maybe commit this upstream. *)
Lemma mapsto_exclusive l v1 v2 q : l ↦ᵢ v1 - l ↦ᵢ{q} v2 - False.
iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1.
Qed.
(* Repeadetly introduce existential variables. *)
Ltac iExistsN := repeat iExists _.
(* Solve a goal that consists of introducing existentials, framing, and picking branches. *)
Ltac iExistsFrame :=
(repeat iExistsN || iFrame);
(done || (iLeft; iExistsFrame) || (iRight; iExistsFrame) || fail "Could not solve goal").
(* gname naming conventions:
- γ for the fractional agreement used at the tail.
- κ for the authorative finite map used in nodesInv.
......@@ -54,36 +38,6 @@ Section Queue_refinement.
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Local Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1) - own γ (q2, to_agree v2) - v1 = v2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
Qed.
Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1)
- own γ (q2, to_agree v2)
- own γ ((q1 + q2)%Qp, to_agree v2) v1 = v2.
Proof.
iIntros "Hl1 Hl2".
iDestruct (fracAgree_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
iDestruct (own_valid with "Hl") as %Hv%pair_valid.
eauto with iFrame.
Qed.
Lemma fracAgree_update γ v w u :
own γ ( v) - own γ ( w) == own γ (1%Qp, to_agree u).
Proof.
iIntros "Hb1 Hb2".
iDestruct (fracAgree_combine with "Hb1 Hb2") as "[tok <-]".
rewrite Qp_half_half.
iApply (own_update with "tok").
by apply cmra_update_exclusive.
Qed.
Lemma node_update ι (x y : mnat) : x y own ι ( x) == own ι ( y).
Proof.
iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
......
......@@ -5,11 +5,9 @@ From iris.program_logic Require Import adequacy ectxi_language.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
CG_queue MS_queue_alt.
common CG_queue MS_queue_alt.
From iris.proofmode Require Import tactics.
Definition locO := leibnizO loc.
Definition queueN : namespace := nroot .@ "queue".
Definition tailN : namespace := nroot .@ "tail".
Definition nodesN : namespace := nroot .@ "nodes".
......@@ -29,22 +27,6 @@ Definition tailsUR : ucmraT := authUR (gsetUR loc).
Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))).
Definition nodeUR : ucmraT := authUR (gmapUR loc (agreeR (leibnizO (gname * loc)))).
Section my_map.
Context `{Monoid M o}.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Context {PROP : bi}.
Implicit Types Φ : K A PROP.
Infix "`o`" := o (at level 50, left associativity).
(* This lemma is committed upstream and should be available from Iris at
some point (when?) *)
Lemma big_sepM_insert_delete Φ m i x :
(([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky (delete i m), Φ k y)%I.
Proof. Admitted.
End my_map.
Section my_set.
Context {PROP : bi}.
Context `{Countable A}.
......@@ -62,11 +44,6 @@ Section Queue_refinement.
Notation D := (prodO valO valO -n> iPropO Σ).
(* Maybe commit this upstream. *)
Lemma mapsto_exclusive l v1 v2 q : l ↦ᵢ v1 - l ↦ᵢ{q} v2 - False.
iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1.
Qed.
(* gname naming conventions:
- γ for the fractional agreement used at the tail.
- κ for the authorative finite map used in nodesInv.
......@@ -77,43 +54,6 @@ Section Queue_refinement.
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Local Notation "◔ v" := ((1/4)%Qp, to_agree v) (at level 20).
Local Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1) - own γ (q2, to_agree v2) - v1 = v2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
Qed.
Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1)
- own γ (q2, to_agree v2)
- own γ ((q1 + q2)%Qp, to_agree v2) v1 = v2.
Proof.
iIntros "Hl1 Hl2".
iDestruct (fracAgree_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
iDestruct (own_valid with "Hl") as %Hv%pair_valid.
eauto with iFrame.
Qed.
Lemma fracAgree_update γ v w u :
own γ ( v) - own γ ( w) == own γ (1%Qp, to_agree u).
Proof.
iIntros "Hb1 Hb2".
iDestruct (fracAgree_combine with "Hb1 Hb2") as "[tok <-]".
rewrite Qp_half_half.
iApply (own_update with "tok").
by apply cmra_update_exclusive.
Qed.
Lemma fracAgree_update_one γ v u :
own γ (1%Qp, to_agree v) == own γ (1%Qp, to_agree u).
Proof.
iIntros. iApply (own_update with "[$]"). by apply cmra_update_exclusive.
Qed.
Lemma node_update ι (x y : mnat) : x y own ι ( x) == own ι ( y).
Proof.
iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
......@@ -324,7 +264,7 @@ Section Queue_refinement.
iDestruct (own_valid_2 with "a b") as %Hv.
rewrite -auth_frag_op in Hv.
apply (auth_frag_valid (_ _)) in Hv. (* Why is this necessary? *)
rewrite op_singleton in Hv.
rewrite singleton_op in Hv.
apply singleton_valid, agree_op_invL' in Hv.
inversion Hv.
done.
......@@ -473,10 +413,10 @@ Section Queue_refinement.
iExists ι'. iFrame. iExists _, _, _, _. iFrame.
Qed. *)
(* This lemma has been commited upstream to Iris and will be available in the future. *)
Lemma auth_update_core_id_frac {A : ucmraT} (a b : A) `{!CoreId b} q :
b a {q} a ~~> {q} a b.
Proof.
Admitted.
Proof. Admitted.
Lemma MS_CG_counter_refinement :
[] MS_queue log CG_queue :
......
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