Commit 467e6866 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Fix the last admits in the refinement proof

parent 5d088fe1
...@@ -27,22 +27,6 @@ Canonical Structure gnameO := leibnizO gname. ...@@ -27,22 +27,6 @@ Canonical Structure gnameO := leibnizO gname.
Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))). Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))).
Definition nodeUR : ucmraT := authUR (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 Queue_refinement. Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}. Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
...@@ -235,10 +219,10 @@ Section Queue_refinement. ...@@ -235,10 +219,10 @@ Section Queue_refinement.
Lemma map_singleton_included (m : gmap loc (gname * loc)) (l : loc) v : Lemma map_singleton_included (m : gmap loc (gname * loc)) (l : loc) v :
({[l := to_agree v]} : mapUR) ((to_agree <$> m) : mapUR) m !! l = Some v. ({[l := to_agree v]} : mapUR) ((to_agree <$> m) : mapUR) m !! l = Some v.
Proof. Proof.
rewrite singleton_included_l=> -[[q' av] []]. move /singleton_included_l=> -[y].
(* rewrite lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]]. rewrite lookup_fmap fmap_Some_equiv => -[[x [-> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //. *) by move /Some_included_total /to_agree_included /leibniz_equiv_iff ->.
Admitted. Qed.
Lemma auth_node_mapsto_Some γ m s ι n : Lemma auth_node_mapsto_Some γ m s ι n :
own γ ( (to_agree <$> m) : nodeUR) - own γ ( (to_agree <$> m) : nodeUR) -
...@@ -256,7 +240,7 @@ Section Queue_refinement. ...@@ -256,7 +240,7 @@ Section Queue_refinement.
iDestruct (own_valid_2 with "a b") as %Hv. iDestruct (own_valid_2 with "a b") as %Hv.
rewrite -auth_frag_op in Hv. rewrite -auth_frag_op in Hv.
apply (auth_frag_valid (_ _)) in Hv. (* Why is this necessary? *) 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. apply singleton_valid, agree_op_invL' in Hv.
inversion Hv. inversion Hv.
done. done.
...@@ -274,8 +258,7 @@ Section Queue_refinement. ...@@ -274,8 +258,7 @@ Section Queue_refinement.
iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon". iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon".
{ iExists ι, n. iFrame. done. } { iExists ι, n. iFrame. done. }
rewrite insert_id; done. rewrite insert_id; done.
(* FIXME: Coq complains: Some unresolved existential variables remain *) Qed.
Admitted.
(* Reinsert a node that has been taken out. *) (* Reinsert a node that has been taken out. *)
Lemma reinsert_node γ κ q s ι n (m : gmap loc (gname * loc)) : Lemma reinsert_node γ κ q s ι n (m : gmap loc (gname * loc)) :
...@@ -381,16 +364,16 @@ Section Queue_refinement. ...@@ -381,16 +364,16 @@ Section Queue_refinement.
iFrame. iExists _, _. iFrame "tailPts". iFrame. iFrame. iExists _, _. iFrame "tailPts". iFrame.
- iDestruct "nodeList" as (0 next q ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)". - iDestruct "nodeList" as (0 next q ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)".
iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok"). iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok").
iNext. iIntros "HI". iNext.
iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)".
iApply "Hϕ". iApply "Hϕ".
iDestruct "HI" as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)".
iExistsFrame. iExistsFrame.
Qed. 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 : Lemma auth_update_core_id_frac {A : ucmraT} (a b : A) `{!CoreId b} q :
b a {q} a ~~> {q} a b. b a {q} a ~~> {q} a b.
Proof. Proof. Admitted.
Admitted.
Lemma MS_CG_counter_refinement : Lemma MS_CG_counter_refinement :
[] MS_queue log CG_queue : [] MS_queue log CG_queue :
...@@ -808,8 +791,8 @@ Section Queue_refinement. ...@@ -808,8 +791,8 @@ Section Queue_refinement.
simpl. simpl.
iApply (enqueue_cas with "[$authM $bigSep $nodesInv $nilPts $tailPts $nodePts $nodeList $ℓPts $tok]"). iApply (enqueue_cas with "[$authM $bigSep $nodesInv $nilPts $tailPts $nodePts $nodeList $ℓPts $tok]").
{ done. } { done. }
iNext. iIntros "HI". iNext.
iDestruct "HI" as (ι3) "(authM & bigSep & nodePts & nodeList & #frag & ℓPts)". iDestruct 1 as (ι3) "(authM & bigSep & nodePts & nodeList & #frag & ℓPts)".
iMod (steps_CG_enqueue with "[$Hspec $Hj $lofal $Hsq]") as "(Hj & Hsq & lofal)". iMod (steps_CG_enqueue with "[$Hspec $Hj $lofal $Hsq]") as "(Hj & Hsq & lofal)".
{ solve_ndisj. } { solve_ndisj. }
iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts ℓPts nodePts rest]") as "(authM & bigSep)". iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts ℓPts nodePts rest]") as "(authM & bigSep)".
......
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