Commit f2534449 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Cleaned up deprecated code

parent 1e938dbf
Pipeline #9884 failed with stages
in 0 seconds
......@@ -530,7 +530,7 @@ Implicit Types p i : K.
Implicit Types x y : gmap K A.
Implicit Types v : A.
Definition insert2 m p i v :=
Definition insert2 `{Countable K} {A : Type} (p i:K) (m: gmap K (gmap K A)) (v: A) :=
match m !! p with
| None => <[p := {[ i := v ]}]>m
| Some(m') => <[p:= <[ i := v ]>m']>m
......@@ -542,7 +542,7 @@ Definition delete2 `{Countable K} {A : Type} (p i:K) (m: gmap K (gmap K A)) :=
| Some(m') => <[p := delete i m']>m
end.
Lemma delete_something_update m1 m2 p i x y :
Lemma dealloc2_local_update m1 m2 p i x y :
m1 !! p = Some x
m2 !! p = Some y
(x, y) ~l~> (delete i x, )
......@@ -554,61 +554,7 @@ Proof.
apply insert_local_update with x y => //.
Qed.
(* Lemma delete_something_update m1 m2 p i v : *)
(* m2 !! p = Some {[ i := v ]} → *)
(* (m1, m2) ~l~> (delete2 p i m1, <[ p := ∅ ]>m2 ). *)
(* Proof. *)
(* intros. *)
(* apply local_update_unital=> n mf Hmv Hm. *)
(* assert (m1 !! p ≡{n}≡ Some {[ i := v ]} ) by admit. *)
(* split. *)
(* - admit. *)
(* - unfold delete2. *)
(* destruct (m1 !! p). *)
(* inversion H1. *)
(* rewrite H4. *)
(* rewrite delete_insert. *)
(* rewrite Hm. *)
(* SearchAbout op. *)
(* rewrite -insert_opN. *)
(* rewrite -(insert_idN). *)
(* eapply insert_local_update. *)
(* Lemma delete_something_update m1 m2 p i x y: *)
(* m1 !! p = Some x → *)
(* m2 !! p = Some y → *)
(* (x, y) ~l~> (delete i x, ∅) → *)
(* (m1, m2) ~l~> (delete2 p i m1, <[ p := ∅ ]>m2 ). *)
(* Proof. *)
(* intros. *)
(* apply local_update_unital=> n mf Hmv Hm. *)
(* assert (m !! p ≡{n}≡ Some {[ i := x ]} ) by admit. *)
(* split. *)
(* - unfold delete2. *)
(* destruct (m !! p). inversion H0. rewrite H3. apply insert_validN =>//. rewrite delete_insert => //. apply Hmv. *)
(* - rewrite left_id. *)
(* assert (m !! p ≡{n}≡ Some {[ i := x ]} ) by admit. *)
(* assert (mf !! p ≡{n}≡ None \/ (∃ mf', mf !! p ≡{n}≡ Some (mf') /\ mf !! i ≡{n}≡ None)) by admit. *)
(* split. *)
(* - unfold delete2. *)
(* destruct (m !! p). inversion H0. rewrite H4. apply insert_validN =>//. rewrite delete_insert => //. apply Hmv. *)
(* - unfold delete2. *)
(* destruct (m !! p). *)
(* inversion H0. *)
(* rewrite H4. *)
(* rewrite left_id. *)
(* rewrite Hm. *)
(* destruct H1. *)
(* + subst. rewrite -insert_singleton_op => //. *)
(* apply delete_notin. *)
(* rewrite -insert_opN. *)
(* Admitted. *)
End nested_gmap_properties.
Print delete_something_update.
(** Functor *)
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A B) n :
......
......@@ -6,21 +6,15 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Definition to_auth {A} (a : A) : auth A :=
{| authoritative := Excl' a; auth_own := a |}.
Definition to_excl {A} (a : A) : excl A := Excl a.
(* Process state *)
Definition gen_procUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (gen_heapUR L V).
Definition to_gen_proc {L V} `{Countable L} (σ : (gmap L (gmap L V))) : gen_procUR L V :=
fmap (λ h, to_gen_heap h) σ.
(* fmap (λ h, (fmap (λ v, (1%Qp, to_agree (v : leibnizC V))) h)) σ. *)
(** The CMRA we need. *)
Class gen_procG (L V : Type) (Σ :gFunctors) `{Countable L} := GenProcG {
gen_proc_inG :> inG Σ (authR (gen_procUR L V)); (* Why authR? *)
gen_proc_inG :> inG Σ (authR (gen_procUR L V));
gen_proc_name : gname
}.
Arguments gen_proc_name {_ _ _ _ _} _ : assert.
......@@ -39,28 +33,13 @@ Section proc_definitions.
Context `{pG : gen_procG L V Σ}.
Definition gen_proc_ctx (σ : gmap L (gmap L V)) : iProp Σ :=
own (gen_proc_name pG) ( (to_gen_proc σ)) (* ∗ gen_heap_ctx (snd σ) *).
(* Lemma unit_def : ((◯ (∅)):(auth (gen_procUR L V))) = (ε:(auth (gen_procUR L V))) . *)
(* eauto. *)
(* Qed. *)
(* Lemma derive_empty_heap (p : L) (σ : gmap L (gmap L V)) : *)
(* (* (gen_proc_ctx σ) ==∗ (gen_proc_ctx σ) ∗ (own (gen_proc_name pG) (ε)). *) *)
(* (gen_proc_ctx σ) ==∗ (gen_proc_ctx σ) ∗ (own (gen_proc_name pG) (◯ (∅))). *)
(* Proof. *)
(* iIntros "H". *)
(* rewrite unit_def. *)
(* iFrame. *)
(* iApply own_unit. *)
(* Qed. *)
own (gen_proc_name pG) ( (to_gen_proc σ)).
Inductive proc_mapping : Type :=
| pinit : L -> proc_mapping
| pmap : L -> L -> Qp -> V -> proc_mapping
.
Definition proc_match (pm : proc_mapping) :
gen_procUR L V :=
match pm with
......@@ -70,10 +49,6 @@ Section proc_definitions.
Definition mapsto_def (pm : proc_mapping) : iProp Σ :=
own (gen_proc_name pG) ( (proc_match pm) ).
(* Definition proc_mapsto_def (p : L) (l : L) (q:Qp) (v : V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ p := {[ l := (q, to_agree (v : leibnizC V)) ]} ]}). *)
(* Definition proc_mapsto_def (pid : L) (h : gmap L V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ pid := to_gen_heap h ]}). *)
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
......@@ -118,19 +93,6 @@ Section to_gen_proc.
- revert H2. apply gen_heap_singleton_included.
Qed.
(* Lemma gen_proc_singleton_included σ (p:L) (l:L) (q:Qp) (v:V): *)
(* {[p := {[l := (q, to_agree v)]}]} ≼ (to_gen_proc σ) → match (σ !! p) with None => None | Some(h) => h !! l end = Some v. *)
(* Proof. *)
(* rewrite singleton_included=> -[ah]. *)
(* rewrite /to_gen_proc lookup_fmap fmap_Some_equiv => -[h']. *)
(* move=> /Some_included_total. destruct h'. destruct H0. rewrite H1. *)
(* intro. *)
(* rewrite H0. *)
(* revert H2. *)
(* apply gen_heap_singleton_included. *)
(* Qed. *)
Lemma to_gen_proc_insert (p:L) (σ : gmap L (gmap L V)) (σ' : gmap L V) :
to_gen_proc (<[p:=σ']> σ) = <[p:=to_gen_heap σ']> (to_gen_proc σ).
Proof. by rewrite /to_gen_proc fmap_insert. Qed.
......@@ -145,32 +107,10 @@ Section to_gen_proc.
- rewrite /to_gen_proc fmap_insert.
assert ((to_gen_heap ((<[l := v]>):(gmap L V))) = ((<[l := (1%Qp, to_agree v)]>(to_gen_heap )):(gen_heapUR L V))). by rewrite /to_gen_heap fmap_insert. rewrite H0. reflexivity. Qed.
(* Definition delete2 `{Countable K} {A : Type} (p l:K) (σ:gmap K (gmap K A)) := *)
(* match (σ !! p) with *)
(* | None => σ *)
(* | Some(σ') => <[p := delete l σ']>σ *)
(* end. *)
(* Definition delete2 `{Countable K} {A : Type} (p i:K) (m: gmap K (gmap K A)) := *)
(* match (m !! p) with *)
(* | None => m *)
(* | Some(m') => <[p := delete i m']>m *)
(* end. *)
(* Lemma delete_something_update `{Countable K} {A : cmraT} (m:gmap K (gmap K A)) (p i: K) (x : A) : *)
(* (* m !! i = Some x → *) *)
(* (m, {[ p := {[ i := x ]} ]}) ~l~> (delete2 p i m, ∅). *)
(* Proof. *)
(* assert (m !! p = Some {[ i := x]}) by admit. *)
(* unfold delete2. *)
(* rewrite H1. *)
(* Admitted. *)
Lemma to_gen_proc_delete p σ :
to_gen_proc (delete p σ) = delete p (to_gen_proc σ).
Proof. by rewrite /to_gen_proc fmap_delete. Qed.
(* Lemma to_gen_proc_delete_val (p l : L) (σ : gmap L (gmap L V)) : *)
Lemma to_gen_proc_delete_val p l σ :
to_gen_proc (delete2 p l σ) = delete2 p l (to_gen_proc σ).
Proof.
......@@ -189,14 +129,6 @@ Section to_gen_proc.
rewrite to_gen_proc_insert. by rewrite to_gen_heap_delete.
Qed.
(* Lemma to_gen_proc_delete_val p l σ : *)
(* to_gen_proc (match σ !! p with None => σ | Some(h) => <[p := delete l h]>σ end) = *)
(* match σ !! p with None => (to_gen_proc σ) | Some(h) => <[p := delete l (to_gen_heap h)]>(to_gen_proc σ) end. *)
(* Proof. *)
(* destruct (σ !! p); try eauto. *)
(* - rewrite /to_gen_proc fmap_insert. *)
(* assert (to_gen_heap (delete l g) = delete l (to_gen_heap g)). apply to_gen_heap_delete. rewrite H0. reflexivity. *)
(* Qed. *)
End to_gen_proc.
Lemma gen_proc_init `{gen_procPreG L V Σ} σ :
......@@ -228,8 +160,6 @@ Section gen_proc.
Global Instance mapsto_as_fractional p l q v :
AsFractional (l p{p}{q} v) (λ q, l p{p}{q} v)%I q.
Proof. split. done. apply _. Qed.
Print discreteC.
Lemma mapsto_agree p l q1 q2 v1 v2 : l p{p}{q1} v1 - l p{p}{q2} v2 - v1 = v2.
Proof.
......@@ -239,51 +169,6 @@ Section gen_proc.
by intros [_ ?%agree_op_invL'].
Qed.
(* Lemma mapsto_contains (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) (n:nat) : *)
(* gen_proc_ctx σ -∗ l p↦{p} v -∗ ⌜(∃ (σ' : gmap L V), ((to_gen_proc σ) !! p ≡{n}≡ Some (to_gen_heap σ') /\ (to_gen_heap σ') !! l ≡{n}≡ Some ((1%Qp, to_agree (v : leibnizC V)))))⌝. *)
(* Proof. *)
(* apply wand_intro_r. *)
(* rewrite mapsto_eq. *)
(* rewrite -own_op. *)
(* rewrite own_valid. *)
(* rewrite discrete_valid. *)
(* f_equiv => /=. *)
(* intros H1. *)
(* inversion H1. *)
(* simpl in H2. *)
(* specialize (H2 n). *)
(* revert H2. rewrite left_id. intros. *)
(* apply gen_proc_singleton_included in H2. *)
(* inversion H2. *)
(* exists {[ l := v ]}. *)
(* split. *)
(* - revert H2. rewrite left_id. intros. apply gen_proc_singleton_included in H2. rewrite singleton_includedN. intros. inversion H2. inversion H5. rewrite H6. revert H7. SearchAbout (≼). rewrite Some_included_totalN. rewrite singleton_includedN. inversion H7. rewrite H8. *)
(* rewrite H4. rewrite left_id. rewrite lookup_op. rewrite lookup_insert. admit. *)
(* - unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. by rewrite lookup_insert. *)
(* rewrite singleton_includedN in H2. *)
(* rewrite cmra_discrete_included_iff in H1. *)
(* rewrite singleton_included in H1. *)
(* rewrite singleton_included in H1. *)
(* assert ( ✓ (● to_gen_proc σ ⋅ ◯ proc_match (pmap p l 1 v)) = ✓{n} (● to_gen_proc σ ⋅ ◯ proc_match (pmap p l 1 v))) by admit. *)
(* rewrite H1 in a. *)
(* apply auth_validN_2 in a. *)
(* f_equiv => /auth_own_valid /=. *)
(* rewrite auth_own_valid. *)
(* auth_own_valid. *)
(* iIntros "H1". *)
(* iApply auth_validN_2 with "H1". *)
(* rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. *)
(* f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid op_singleton singleton_valid pair_op. *)
(* by intros [_ ?%agree_op_invL']. *)
(* iIntros. *)
(* Admitted. *)
Global Instance ex_mapsto_fractional p l : Fractional (λ q, l p{p}{q} -)%I.
Proof.
intros p' q'. iSplit.
......@@ -318,16 +203,9 @@ Section gen_proc.
iModIntro. simpl. rewrite to_gen_proc_insert. unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. rewrite insert_empty. iFrame.
Qed.
Definition insert2 σ p l v :=
match σ !! p with
| None => <[p := {[ l := v ]}]>σ
| Some(σ') => <[p:= <[ l := v ]>σ']>σ
end.
Lemma gen_proc_alloc_val (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) (σ':gmap L V) :
σ !! p = Some σ' σ' !! l = None
(* gen_proc_ctx σ ==∗ gen_proc_ctx (<[p:=(<[l:=v]>σ')]>σ) ∗ l p↦{p} v. *)
gen_proc_ctx σ == gen_proc_ctx (insert2 σ p l v) l p{p} v.
gen_proc_ctx σ == gen_proc_ctx (insert2 p l σ v) l p{p} v.
Proof.
iIntros (? ?) "Hσ".
unfold insert2. rewrite H1.
......@@ -357,7 +235,7 @@ Section gen_proc.
destruct H1.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update. unfold proc_match.
eapply (delete_something_update (to_gen_proc σ) ({[p := {[l := (1%Qp, to_agree v)]}]}) (p) (l) (to_gen_heap x) ({[l := (1%Qp, to_agree v)]})) => //.
eapply (dealloc2_local_update (to_gen_proc σ) ({[p := {[l := (1%Qp, to_agree v)]}]}) (p) (l) (to_gen_heap x) ({[l := (1%Qp, to_agree v)]})) => //.
by apply lookup_to_gen_proc_Some.
by rewrite lookup_insert.
eapply (delete_singleton_local_update (to_gen_heap x) (l) ((1%Qp, to_agree v))).
......@@ -374,7 +252,7 @@ Section gen_proc.
Qed.
Lemma gen_proc_update σ p l v1 v2 :
gen_proc_ctx σ - l p{p} v1 == gen_proc_ctx (insert2 σ p l v2) l p{p} v2.
gen_proc_ctx σ - l p{p} v1 == gen_proc_ctx (insert2 p l σ v2) l p{p} v2.
Proof.
iIntros "Hσ Hl". rewrite /gen_proc_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
......@@ -384,7 +262,6 @@ Section gen_proc.
{ eapply auth_update.
eapply singleton_local_update.
by apply lookup_to_gen_proc_Some.
Print exclusive_local_update.
eapply singleton_local_update.
by apply lookup_to_gen_heap_Some.
eapply (exclusive_local_update _ ((1%Qp, to_agree (v2:leibnizC _))))=> //.
......
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