get rid of erasures, use exclusive state ownership instead

core_lang.v

 Require Import RecDom.PCM.
 
-Module Type CORE_LANG (Res : PCM_T).
-  Import Res.
-
+Module Type CORE_LANG.
   Delimit Scope lang_scope with lang.
   Local Open Scope lang_scope.
 
@@ -98,53 +96,4 @@ Module Type CORE_LANG (Res : PCM_T).
                         prim_step (e, σ) (e', σ') ->
                         K = ε /\ is_value e'.
 
-
-  (******************************************************************)
-  (** ** Erasures **)
-  (******************************************************************)
-
-  (** Erasure of a resource to the set of states it describes **)
-  Parameter erase_state : option res -> state -> Prop.
-
-  Axiom erase_state_nonzero :
-    forall σ, ~ erase_state 0%pcm σ.
-
-  Axiom erase_state_emp :
-    forall σ, erase_state 1%pcm σ.
-
-  (** Erasure of a resource to the set of expressions it describes **)
-  (* Not needed for now *)
-  Parameter erase_exp : option res -> expr -> Prop.
-
-  Axiom erase_exp_mono :
-    forall r r' e,
-      erase_exp r e ->
-      erase_exp (r · r')%pcm e.
-
-  Axiom erase_fork_ret :
-    forall r, erase_exp r fork_ret.
-
-  Axiom erase_fork :
-    forall r e,
-      erase_exp r (fork e) ->
-      erase_exp r e.
-
-  Axiom erase_exp_idemp :
-    forall r e, erase_exp r e ->
-      exists r', r = (r · r')%pcm /\ r' = (r' · r')%pcm /\ erase_exp r' e.
-
-  Axiom erase_exp_split :
-    forall r K e,
-      erase_exp r (fill K e) ->
-      exists r_K r_e,
-        r = (r_K · r_e)%pcm /\
-        erase_exp r_K (fill K fork_ret) /\
-        erase_exp r_e e.
-
-  Axiom erase_exp_combine :
-    forall r_K r_e e K,
-      erase_exp r_K (fill K fork_ret) ->
-      erase_exp r_e e ->
-      erase_exp (r_K · r_e)%pcm (fill K e).
-
 End CORE_LANG.

iris.v

 Require Import world_prop core_lang lang masks.
 Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
 
-Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
+Module Iris (RL : PCM_T) (C : CORE_LANG).
 
-  Module Import L  := Lang RP RL C.
+  Module Import L  := Lang C.
   Module Import R <: PCM_T.
-    Definition res := (RP.res * RL.res)%type.
+    Definition res := (pcm_res_ex state * RL.res)%type.
     Instance res_op   : PCM_op res := _.
     Instance res_unit : PCM_unit res := _.
     Instance res_pcm  : PCM res := _.
@@ -142,13 +142,29 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     pcmconst (up_cr (pord r)).
 
   (** Physical part **)
-  Definition ownRP (r : RP.res) : Props :=
+  Definition ownRP (r : pcm_res_ex state) : Props :=
     ownR (r, pcm_unit _).
 
   (** Logical part **)
   Definition ownRL (r : RL.res) : Props :=
     ownR (pcm_unit _, r).
 
+  (** Proper physical state: ownership of the machine state **)
+  Instance state_type : Setoid state := discreteType.
+  Instance state_metr : metric state := discreteMetric.
+  Instance state_cmetr : cmetric state := discreteCMetric.
+
+  Program Definition ownS : state -n> Props :=
+    n[(fun s => ownRP (ex_own _ s))].
+  Next Obligation.
+    intros r1 r2 EQr. hnf in EQr. now rewrite EQr.
+  Qed.
+  Next Obligation.
+    intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
+    simpl in EQr. subst; reflexivity.
+  Qed.
+
+  (** Proper ghost state: ownership of logical w/ possibility of undefined **)
   Lemma ores_equiv_eq T `{pcmT : PCM T} (r1 r2 : option T) (HEq : r1 == r2) : r1 = r2.
   Proof.
     destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
@@ -158,7 +174,6 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
   Instance logR_metr : metric RL.res := discreteMetric.
   Instance logR_cmetr : cmetric RL.res := discreteCMetric.
 
-  (** Proper ghost state: ownership of logical w/ possibility of undefined **)
   Program Definition ownL : (option RL.res) -n> Props :=
     n[(fun r => match r with
                   | Some r => ownRL r
@@ -172,6 +187,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction; simpl in EQr; subst; reflexivity.
   Qed.
 
+
   (** Lemmas about box **)
   Lemma box_intro p q (Hpq : □ p ⊑ q) :
     □ p ⊑ □ q.
@@ -202,7 +218,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       destruct u as [u |]; [| now erewrite pcm_op_zero in EQut by apply _].
       assert (HT := comm (Some u) t); rewrite EQut in HT.
       destruct t as [t |]; [| now erewrite pcm_op_zero in HT by apply _]; clear HT.
-      exists (pcm_unit RP.res, u) (pcm_unit RP.res, t).
+      exists (pcm_unit (pcm_res_ex state), u) (pcm_unit (pcm_res_ex state), t).
       split; [unfold pcm_op, res_op, pcm_op_prod | split; do 15 red; reflexivity].
       now erewrite pcm_op_unit, EQut by apply _.
     - destruct u as [u |]; [| contradiction]; destruct t as [t |]; [| contradiction].
@@ -216,6 +232,8 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       destruct (Some rt · Some ru)%pcm as [rut |];
         [| now erewrite pcm_op_zero in EQr by apply _].
       exists rut; assumption.
+
+      (* TODO: own 0 = False, own 1 = True *)
   Qed.
 
   Section Erasure.
@@ -268,11 +286,16 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
         rewrite !assoc, (comm (Some r2)); reflexivity.
     Qed.
 
+    Definition erase_state (r: option res) σ: Prop := match r with
+    | Some (ex_own s, _) => s = σ
+    | _ => False
+    end.
+
     Global Instance preo_unit : preoType () := disc_preo ().
 
     Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
       ▹ (mkUPred (fun n _ =>
-                    erase_state (option_map fst (r · s)) σ
+                    erase_state (r · s) σ
                     /\ exists rs : nat -f> res,
                          erase rs == s /\
                          forall i (Hm : m i),
@@ -321,7 +344,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       ~ erasure σ m r s w (S k) tt.
     Proof.
       intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
-      now apply erase_state_nonzero in HD.
+      exact HD.
     Qed.
 
   End Erasure.

lang.v

@@ -3,13 +3,12 @@ Require Import RecDom.PCM.
 Require Import core_lang.
 
 (******************************************************************)
-(** * Derived language with physical and logical resources **)
+(** * Derived language with threadpool steps **)
 (******************************************************************)
 
-Module Lang (RP: PCM_T) (RL: PCM_T) (C : CORE_LANG RP).
+Module Lang (C : CORE_LANG).
 
   Export C.
-  Export RP RL.
 
   Local Open Scope lang_scope.
 
@@ -107,86 +106,4 @@ Module Lang (RP: PCM_T) (RL: PCM_T) (C : CORE_LANG RP).
     tauto.
   Qed.
 
-  (* Derived facts about expression erasure *)
-  (* I don't think we need these for now — F. *)
-  (*
-  Lemma erase_exp_zero r e :
-    erase_exp r e ->
-    erase_exp RP.res_zero e.
-  Proof.
-    move=>r e H.
-    rewrite -(RP.res_timesZ r) RP.res_timesC.
-      by eapply C.erase_exp_mono.
-  Qed.
-
-  Lemma erase_exp_mono: forall r r' e,
-                          erase_exp (resP r) e ->
-                          erase_exp (resP (r ** r')) e.
-  Proof.
-    move=>r r' e H.
-    case EQ_m:(RL.res_times (resL r) (resL r'))=>[m|].
-    - erewrite resP_comm.
-    - by apply C.erase_exp_mono.
-    - by rewrite EQ_m.
-    - move:(resL_zero _ _ EQ_m)=>->/=.
-                               eapply erase_exp_zero; eassumption.
-  Qed.
-
-  Lemma erase_exp_idemp: forall r e,
-                           erase_exp (resP r) e ->
-                           exists r',
-                             r = r ** r' /\
-                             r' = r' ** r' /\
-                             erase_exp (resP r') e.
-  Proof.
-    move=>[[rP rL]|] /= e H_erase; last first.
-    - exists None.
-             split; first done.
-             split; first done.
-             done.
-             move:(C.erase_exp_idemp _ _ H_erase)=>{H_erase}[r'] [H_EQ1 [H_EQ2 H_erase]].
-             exists (resFP r').
-             split; last split.
-             - case:r' H_EQ1 {H_EQ2 H_erase}=>[r'|]/=H_EQ1.
-             - by rewrite -H_EQ1 RL.res_timesC RL.res_timesI /=.
-                  - by rewrite RP.res_timesC RP.res_timesZ in H_EQ1.
-             - by rewrite -resFP_comm -H_EQ2.
-             - by rewrite resP_FP.
-  Qed.
-
-  Lemma erase_exp_split: forall r K e, 
-                           erase_exp (resP r) (fill K e) ->
-                           exists r_K r_e,
-                             r = r_K ** r_e /\
-                             erase_exp (resP r_K) (fill K fork_ret) /\
-                             erase_exp (resP r_e) e.
-  Proof.
-    move=>r K e H_erase.
-    move:(C.erase_exp_split _ _ _ H_erase)=>{H_erase}[r_K [r_e [H_EQ [H_erase1 H_erase2]]]].
-    exists (resFP r_K ** resFL (resL r)). exists (resFP r_e).
-    split; last split.
-    - rewrite -{1}(res_eta r).
-      rewrite res_timesA [_  ** resFP _]res_timesC -res_timesA.
-      f_equal.
-        by rewrite -resFP_comm H_EQ.
-    - eapply erase_exp_mono.
-        by rewrite resP_FP.
-    - by rewrite resP_FP.
-  Qed.
-
-  Lemma erase_exp_combine: forall r_K r_e e K,
-                             erase_exp (resP r_K) (fill K fork_ret) ->
-                             erase_exp (resP r_e) e ->
-                             erase_exp (resP (r_K ** r_e)) (fill K e).
-  Proof.
-    move=>r_k r_e e K H_K H_e.
-    case EQ_m:(RL.res_times (resL r_k) (resL r_e))=>[m|]; last first.
-    - apply resL_zero in EQ_m.
-      rewrite EQ_m.
-      eapply erase_exp_zero, erase_exp_combine; eassumption.
-      rewrite resP_comm; last first.
-    - by rewrite EQ_m.
-      eapply erase_exp_combine; eassumption.
-  Qed.*)
-
 End Lang.