Commit b45d539b authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Interp extract preserves steps.

parent 690ccd6d
......@@ -10,7 +10,17 @@ Definition ownl `{inG Λ Σ (mapR gname A)} (γ : gname) (a : A) : ilPropG Λ Σ
ownGl (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
Typeclasses Opaque to_globalF own.
Instance: Params (@ownl) 5.
Typeclasses Opaque to_globalF own ownl.
Definition owne `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownG (to_globalFe a).
Definition ownle `{inG Λ Σ A} (a : A) : ilPropG Λ Σ :=
ownGl (to_globalFe a).
Instance: Params (@to_globalFe) 4.
Instance: Params (@own) 4.
Instance: Params (@ownle) 4.
Typeclasses Opaque to_globalFe owne ownle.
Section empty.
Context `{i : inG Λ Σ A} `{CMRAUnit A}.
......@@ -31,6 +41,15 @@ Proof.
- intros; by rewrite left_id.
- intros. destruct inG_prf. by rewrite left_id.
Qed.
Lemma inG_empty_back_sym:
cmra_transport (Init.Logic.eq_sym inG_prf) .
Proof.
eapply cmra_unit_unique.
- intros; by rewrite left_id.
- intros. rewrite inG_empty_back.
rewrite cmra_transport_sym_inv. by rewrite left_id.
Qed.
End empty.
(** Properties about ghost ownership *)
......@@ -119,3 +138,69 @@ Proof.
- naive_solver.
Qed.
End global.
(* There is obviously some redundancy *)
(** Properties about ghost ownership in the nameless case *)
Section globale.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
(** * Properties of own *)
Global Instance owne_ne n : Proper (dist n ==> dist n) (owne).
Proof. solve_proper. Qed.
Global Instance owne_proper : Proper (() ==> (⊣⊢)) (owne) := ne_proper _.
Lemma owne_op a1 a2 : owne (a1 a2) ⊣⊢ (owne a1 owne a2).
Proof. by rewrite /owne -ownG_op to_globalFe_op. Qed.
Global Instance owne_mono : Proper (flip () ==> ()) (owne).
Proof. move=>a b [c H]. rewrite H owne_op. eauto with I. Qed.
Lemma owne_valid a : owne a a.
Proof.
rewrite /owne ownG_valid /to_globalFe.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
trans ( cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma owne_valid_r a : owne a (owne a a).
Proof. apply: uPred.always_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a ( a owne a).
Proof. by rewrite comm -owne_valid_r. Qed.
Global Instance owne_timeless a : Timeless a TimelessP (owne a).
Proof. rewrite /owne; apply _. Qed.
Global Instance owne_core_persistent a : Persistent a PersistentP (owne a).
Proof. rewrite /owne; apply _. Qed.
(* TODO: This also holds if we just have a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma owne_updateP P a E :
a ~~>: P owne a (|={E}=> a', P a' owne a').
Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalFe a' P a') ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (apply cmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
Lemma owne_update a a' E : a ~~> a' owne a (|={E}=> owne a').
Proof.
intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
Qed.
Lemma owne_empty `{Empty A, !CMRAUnit A} E :
True (|={E}=> owne ).
Proof.
rewrite ownG_empty /owne. apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty inG_id
(λ y, iprod_singleton inG_id y = to_globalFe )).
- rewrite inG_empty_back.
eapply cmra_transport_updateP;
first eapply cmra_update_updateP, cmra_update_unit.
naive_solver.
- naive_solver.
Qed.
End globale.
\ No newline at end of file
......@@ -32,6 +32,9 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
Definition to_globalF `{inG Λ Σ (mapR gname A)} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id (cmra_transport inG_prf ({[ γ := a ]})).
Definition to_globalFe `{inG Λ Σ A} (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id (cmra_transport inG_prf a).
(** * Properties of to_globalC *)
Section to_globalF.
Context `{i : inG Λ Σ (mapR gname A)}.
......@@ -51,6 +54,25 @@ Global Instance to_globalF_persistent γ m :
Proof. rewrite /to_globalF; apply _. Qed.
End to_globalF.
(** * Properties of to_globalC *)
Section to_globalFe.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
Global Instance to_globalFe_ne n : Proper (dist n ==> dist n) (to_globalFe).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalFe_op a1 a2 :
to_globalFe (a1 a2) to_globalFe a1 to_globalFe a2.
Proof.
by rewrite /to_globalFe iprod_op_singleton -cmra_transport_op.
Qed.
Global Instance to_globalFe_timeless m: Timeless m Timeless (to_globalFe m).
Proof. rewrite /to_globalFe; apply _. Qed.
Global Instance to_globalFe_persistent m :
Persistent m Persistent (to_globalFe m).
Proof. rewrite /to_globalFe; apply _. Qed.
End to_globalFe.
(** When instantiating the logic, we want to just plug together the
requirements exported by the modules we use. To this end, we construct
the "gFunctors" from a "list gFunctor", and have some typeclass magic
......
......@@ -1014,7 +1014,7 @@ Definition refine v ts cs ixs : refine_cmra sΛ :=
Section definitions.
From iris.program_logic Require Import ownership adequacy adequacy_inf.
Context `{refineG Λ Σ F} (γ: gname).
Context `{refineG Λ Σ F}.
Definition trivial_step (A: cmraT) :=
(a a': A) n, a _(n) a'.
......@@ -1023,18 +1023,18 @@ From iris.program_logic Require Import ownership adequacy adequacy_inf.
A = projT2 Σ gid' (iPreProp Λ (globalF Σ))
trivial_step A).
Definition master_own (c: cfg sΛ) :=
( cfg0 idx0, own γ (refine master (cfg0 ++ [c]) idx0))%I.
( cfg0 idx0, owne (refine master (cfg0 ++ [c]) idx0))%I.
Definition master_own_exact (cs: list (cfg sΛ)) idxs :=
own γ (refine master cs idxs)%I.
owne (refine master cs idxs)%I.
From iris.algebra Require Import lupred upred.
Definition snapshot_ownl tids (c: cfg sΛ) :=
( cfg0 idx0, ownl γ (refine snapshot tids (cfg0 ++ [c]) idx0))%L.
( cfg0 idx0, ownle (refine snapshot tids (cfg0 ++ [c]) idx0))%L.
Definition snapshot_ownl_exact tids cs idxs :=
ownl γ (refine snapshot tids cs idxs)%L.
ownle (refine snapshot tids cs idxs)%L.
Definition interp_extract (r: iRes Λ (globalF Σ)) : refine_cmra sΛ :=
default (((gst r) inG_id) !! γ) (cmra_transport (eq_sym inG_prf)).
cmra_transport (eq_sym inG_prf) ((gst r) inG_id).
Instance default_proper `{Equiv A} `{Equiv B}:
Proper (() ==> () ==> (() ==> ()) ==> ()) (@default A B).
......@@ -1060,12 +1060,9 @@ From iris.program_logic Require Import ownership adequacy adequacy_inf.
Instance interp_extract_proper:
Proper (() ==> ()) interp_extract.
Proof.
unfold interp_extract. intros x y Heq.
eapply default_proper; eauto.
- inversion Heq as [? ? Heqg].
eapply lookup_proper.
eapply Heqg.
- intros f f' Heqf. destruct (eq_sym inG_prf). auto.
rewrite /interp_extract. intros x y Heq.
inversion Heq as [_ _ Heq'].
rewrite (Heq' inG_id) //.
Qed.
......@@ -1243,15 +1240,17 @@ have non empty cfgs in second part, we can use that to get the desired cfg of s
interp_extract (r r') interp_extract r interp_extract r'.
Proof.
unfold interp_extract.
rewrite lookup_op default_id_op //=.
rewrite cmra_transport_op //=.
Qed.
Lemma interp_extract_bigop rs:
interp_extract (big_op rs) big_op (map interp_extract rs).
Proof.
induction rs; auto.
simpl. rewrite interp_extract_op.
rewrite IHrs. eauto.
induction rs.
- rewrite /interp_extract //= iprod_lookup_empty.
symmetry. eapply inG_empty_back_sym.
- rewrite interp_extract_op.
rewrite IHrs. eauto.
Qed.
Existing Instances refine_op refine_equiv.
......@@ -1281,10 +1280,7 @@ have non empty cfgs in second part, we can use that to get the desired cfg of s
unfold interp_extract.
destruct 1 as (?&?&Hv).
specialize (Hv inG_id).
specialize (map_lookup_valid (gst r inG_id) γ); intros Hmv; auto.
destruct lookup; simpl; auto.
- eapply cmra_transport_valid; eauto.
- eapply cmra_unit_valid.
eapply cmra_transport_valid; eauto.
Qed.
Lemma interp_extract_validN r n:
......@@ -1293,19 +1289,9 @@ have non empty cfgs in second part, we can use that to get the desired cfg of s
intros (?&?&Hv). cut ({S n} (interp_extract r)); auto.
unfold interp_extract.
specialize (Hv inG_id).
specialize (map_lookup_validN (S n) (gst r inG_id) γ); intros Hmv; auto.
destruct lookup; simpl; auto.
- eapply cmra_transport_validN; eauto.
- eapply cmra_unit_valid.
eapply cmra_transport_validN; eauto.
Qed.
(* TODO: move to cmra *)
Lemma cmra_transport_sym_inv {A B: cmraT} (Pf: A = B) (x: A):
cmra_transport (eq_sym Pf) (cmra_transport Pf (x)) = x.
Proof.
destruct Pf. auto.
Qed.
Lemma force_some_interp n σ robs r rw iname:
wsat' (S n) σ
(big_op robs r
......@@ -1369,15 +1355,14 @@ have non empty cfgs in second part, we can use that to get the desired cfg of s
assert (interp_extract rP
(refine master (cs ++ [c]) idxs)
(default (rext inG_id !! γ) (cmra_transport (eq_sym inG_prf)))) as H_interp_rP.
(cmra_transport (eq_sym inG_prf) (rext inG_id))) as H_interp_rP.
{
unfold interp_extract.
rewrite (Heq inG_id).
rewrite lookup_op.
rewrite default_id_op.
unfold to_globalF.
rewrite iprod_lookup_op.
rewrite cmra_transport_op.
unfold to_globalFe.
rewrite iprod_lookup_singleton.
rewrite lookup_singleton. simpl.
rewrite cmra_transport_sym_inv. auto.
}
......@@ -1509,21 +1494,115 @@ have non empty cfgs in second part, we can use that to get the desired cfg of s
simpl; split_and!.
**
Check interp_extract.
Lemma option_stepN_some {A: cmraT} (ma mb: option A) n:
ma _(n) mb a b, ma = Some a mb = Some b a _(n) b.
Lemma stepN_interp_extract n r r':
r _(n) r' (interp_extract r) _(n) (interp_extract r').
Proof.
destruct ma as [a|]; destruct mb as [b|]; eauto;
rewrite /cmra_stepN /option_stepN //=.
rewrite /interp_extract; split; intros Hs.
- eapply cmra_transport_stepN; eauto.
- rewrite /stepN /cmra_stepN //=.
intros id.
case (decide (id = inG_id)).
* intros ->. eapply cmra_transport_stepN; eauto.
* intros Hne. eapply AltTriv. eauto.
Qed.
Lemma tepN_interp_extract n r r':
r _(n) r' (interp_extract r) _(n) (interp_extract r').
Lemma idx_stepN_interp_extract n i rs rs':
idx_stepN n i rs rs' idx_stepN n i (map interp_extract rs) (map interp_extract rs').
Proof.
intros Hs. unfold interp_extract.
rewrite ?idx_stepN_equiv.
induction 1.
* simpl. econstructor; first eapply stepN_interp_extract; auto.
setoid_subst. auto.
* simpl. rewrite map_app. simpl.
eapply (idx_stepN_alt_hd_fork);
first (rewrite -interp_extract_op; eapply stepN_interp_extract; auto).
setoid_subst. auto.
* simpl. econstructor; setoid_subst; eauto.
Qed.
eapply idx_stepN_interp_extract; eauto.
eapply idx_stepN_le; last eauto.
omega.
**
(* TODO: it seems like the "rest" data is not actually needed,
and then stepping just ought to be whether the istep vector steps, and again
when you flatten you just take last elt in product.
I think I wanted the rest data to constrain evolution to make it bounded non-det? But that could be done
with another side condition: every token has to be owned by somebody in the vector -- this ensures each thread in the vector can only do its own steps and that's enough
Actually, no, the rest appears to be because otherwise the invariant can't guarantee that the interp is non-empty. but actually, the fact that some elt of vector took step guarantees that one of them i snon empty -- so I guess we could use that instead in force interp
*)
- rewrite ?idx_stepN_equiv.
remember (map interp_extract rs) as rsi eqn:Heq.
remember (map interp_extract rs') as rsi' eqn:Heq'.
intros Hsi. revert Heq Heq'.
induction Hsi; intros; subst.
* destruct rs as [|r rs_tl]; simpl in *; first congruence.
destruct rs' as [|r' rs'_tl]; simpl in *; first congruence.
econstructor; setoid_subst.
eapply stepN_interp_extract; auto.
eauto.
simpl.
*
* simpl in *. inversion 1.
* simpl in *. inversion 1.
induction rs' as [|a']; simpl in *; first congruence.
subst.
econstructor. eapply stepN_interp_extract.
setoid_subst. auto.
setoid_subst. auto.
eauto. eapply equivalence_refl. eauto.
assert (interp_extract a' = r2).
congruence. subst. eauto.
eauto.
subst. econstructor.
intros His. inversion His.
subst.
SearchAbout map app.
* intros.
SearchAbout map.
induction 1.
econstructor. first eapply interp_extract; eauto.
eapply interp_
rewrite H1.
rewrite /interp_extract; split; intros Hs.
- eapply cmra_transport_stepN; eauto.
- rewrite /stepN /cmra_stepN //=.
intros id.
case (decide (id = inG_id)).
* intros ->. eapply cmra_transport_stepN; eauto.
* intros Hne. eapply AltTriv. eauto.
Qed.
idtac.
subst.
econstructor.
simpl. econstructor. eapply cmra_transport_stepN; eauto.
- eapply cmra_transport_stepN in Hs.
rewrite cmra_transport_sym_inv.
; eauto.
specialize (Hs inG_id).
specialize (Hs γ).
rewrite eq_
destruct ((gst r) inG_id).
eapply option_stepN_some in Hs as (c&c'&Heq&Heq'&hs).
rewrite Heq.
assert ( c, gst r inG_id !! γ = Some c).
......
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