Commit 1797c461 authored by Hai Dang's avatar Hai Dang
Browse files

fix cmra

parent f734ecf1
......@@ -7,17 +7,17 @@ Set Default Proof Using "Type".
Inductive tag_kind := tkUnique | tkPub.
(* Ex() + Ag() *)
Definition tagKindR := csumR (exclR unitO) (agreeR unitO).
Definition tagKindR := csumR (exclR unitO) unitR.
Definition to_tagKindR (tk: tag_kind) : tagKindR :=
match tk with tkUnique => Cinl (Excl ()) | tkPub => Cinr (to_agree ()) end.
match tk with tkUnique => Cinl (Excl ()) | tkPub => Cinr () end.
Inductive call_state := csOwned (T: gset ptr_id) | csPub.
(* Ex(ptr_id) + Ag() *)
Definition callStateR := csumR (exclR (gsetO ptr_id)) (agreeR unitO).
Definition callStateR := csumR (exclR (gsetO ptr_id)) unitR.
Definition to_callStateR (cs: call_state) : callStateR :=
match cs with csOwned T => Cinl (Excl T) | csPub => Cinr (to_agree ()) end.
match cs with csOwned T => Cinl (Excl T) | csPub => Cinr () end.
Definition cmap := gmap call_id call_state.
(* call_id CallState *)
......@@ -35,7 +35,7 @@ Definition to_tmapUR (pm: tmap) : tmapUR :=
fmap (λ tm, (to_tagKindR tm.1, to_heapletR tm.2)) pm.
Definition lmap := gmap loc (scalar * stack).
Definition lmapUR := gmapUR loc (csumR (exclR (leibnizO (scalar * stack))) (agreeR unitO)).
Definition lmapUR := gmapUR loc (csumR (exclR (leibnizO (scalar * stack))) unitR).
Definition res := (tmap * cmap * lmap)%type.
Definition resUR := prodUR (prodUR tmapUR cmapUR) lmapUR.
......@@ -55,11 +55,9 @@ Qed.
Lemma tag_kind_incl_eq (k1 k2: tagKindR):
k2 k1 k2 k1 k2.
Proof.
move => VAL /csum_included [? |[[? [? [? [? Eq]]]]|[? [? [? [? LE]]]]]];
subst; [done|..].
- exfalso. eapply exclusive_included; [..|apply Eq|apply VAL]. apply _.
- apply Cinr_equiv, agree_op_inv. apply agree_included in LE.
rewrite -LE. apply VAL.
move => VAL /csum_included [? |[[? [? [? [? Eq]]]]|[[] [[] [? [? LE]]]]]];
subst; [done|..|done].
exfalso. eapply exclusive_included; [..|apply Eq|apply VAL]. apply _.
Qed.
Lemma tagKindR_exclusive (h0 h: heapletR) mb :
......@@ -89,11 +87,11 @@ Proof.
Qed.
Lemma tagKindR_valid (k: tagKindR) :
valid k k', k to_tagKindR k'.
valid k k', k = to_tagKindR k'.
Proof.
destruct k as [[[]|]|a |]; [|done|..|done]; intros VAL.
destruct k as [[[]|]|[]|]; [|done|..|done]; intros VAL.
- by exists tkUnique.
- exists tkPub. by apply to_agree_uninj in VAL as [[] <-].
- by exists tkPub.
Qed.
(** cmap properties *)
......@@ -143,8 +141,7 @@ Proof.
intros HL. move : (VALID c). rewrite lookup_op HL.
destruct (cm2 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
rewrite -Some_op Some_valid.
destruct cs' as [[]|c2|]; auto; try inversion 1.
rewrite /= Cinr_op. intros Eq2%agree_op_inv. by rewrite -Eq2 agree_idemp.
destruct cs' as [[]|c2|]; auto; inversion 1.
Qed.
Lemma cmap_insert_op_r (cm1 cm2: cmapUR) c T cs (VALID: (cm1 cm2)):
......
......@@ -170,8 +170,7 @@ Proof.
{ apply (pair_valid tk2 h2). rewrite -pair_valid.
apply (lookup_valid_Some r2.(rtm) t2); [apply VAL|]. by rewrite Eq1. }
destruct Eq as [|[|Eq]]; [by subst|naive_solver|].
destruct Eq as [?[ag[? [? ?]]]]. simplify_eq.
apply to_agree_uninj in VL2 as [[] Eq]. rewrite -Eq.
destruct Eq as [?[[][? [? ?]]]]. simplify_eq.
apply csum_included. naive_solver.
Qed.
......
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