Heading toward an improved robust_safety.

Simplified adv, defining it with ownL.

Proof of concept for a friendly interface that (if it works) lets the user
set up an invariant and prove view shifts and atomic triples for primitive
reductions, rather than work in the model. (It should work, but I have to
merge my two proofs to make sure.)

iris_unsafe.v

@@ -15,6 +15,25 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
   Local Open Scope lang_scope.
   Local Open Scope iris_scope.
 
+  (* PDS: Why isn't this inferred automatically? If necessary, move this to ris_core.v *)
+  Global Program Instance res_preorder : PreOrder (pcm_ord res) := @preoPO res (PCM_preo res).
+
+  (* PDS: Move to iris_core.v *)
+  Lemma ownL_timeless {r : option RL.res} :
+    valid(timeless(ownL r)).
+  Proof. intros w n _ w' k r' HSW HLE; now destruct r. Qed.
+
+  (* PDS: Hoist, somewhere. *)
+  Program Definition restrictV (Q : expr -n> Props) : vPred :=
+    n[(fun v => Q (` v))].
+  Solve Obligations using resp_set.
+  Next Obligation.
+    move=> v v' Hv w k r; move: Hv.
+    case: n=>[_ Hk | n].
+    - by absurd (k < 0); omega.
+    by move=> /= ->.
+  Qed.
+
   Implicit Types (P Q R : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (φ : value -n> Props) (r : res) (w : Wld).
 
   (* PDS: Move to iris_wp.v *)
@@ -167,30 +186,13 @@ But I can hack around it...
     Qed.
 
     (*
-     * The predicate adv e internalizes ɑ e ⊑ -.
+     * adv e: own ghost prim_of e.
      *)
 
-    Definition advP e r := ɑ e ⊑ r.
-
     Program Definition adv : expr -n> Props :=
-      n[(fun e => m[(fun w => mkUPred (fun n r => advP e r) _)])].
-    Next Obligation.
-      move=> n k r r' HLe [α Hr'] [β Hr]; rewrite/advP.
-      move: Hr'; move: Hr<-;
-      rewrite	(* α · (β · e) *)
-      	[Some β · _]pcm_op_comm	(* α · (e · β) *)
-      	pcm_op_assoc	(* (α · e) · β *)
-      	[Some α · _]pcm_op_comm	(* (e · α) · β *)
-      	-pcm_op_assoc	(* e · (α · β) *)
-      	pcm_op_comm	(* (α · β) · e *)
-      => Hr'.
-      move: Hr'; case Hαβ: (Some α · _) => [αβ |] Hr'; last done.
-      by exists αβ.
-    Qed.
-    Next Obligation. done. Qed.
-    Next Obligation. by move=> w w' HSw. Qed.
-    Next Obligation. (* use the def of discrete e = n = e' *)
-      move=> e e' HEq w k r HLt; rewrite/=/advP.
+      n[(fun e => ownL(Some(prim_of e)))].
+    Next Obligation. (* Poper (dist n ==> dist n) (fun e => ownRL (prim_of e)) *)
+      move=> e e' HEq w k r HLt /=.
       move: HEq HLt; case: n=>[| n'] /= HEq HLt.
       - by absurd(k < 0); omega.
       by rewrite HEq.
@@ -232,7 +234,7 @@ But I can hack around it...
         move: HW'; case Hr': (Some _ · Some _) => [r'' |] HW'; last first.
         + by rewrite pcm_op_zero in HW'; exfalso; exact: (wsat_nz HW').
         exists w'' r''; split; [done | split; [| by rewrite mask_full_union] ].
-        apply: (IH _ HLt _ _); rewrite/=/advP/=/pcm_ord; exists r'.
+        apply: (IH _ HLt _ _); rewrite/=/pcm_ord; exists r'.
         by rewrite pcm_op_comm -Hr'; reflexivity.
 
       (* e forks *)
@@ -247,7 +249,7 @@ But I can hack around it...
       case Hrret: (_ · Some r') => [rret |] He; last done.
       exists w' (ɑ e') rret; split; first by reflexivity.
       have {IH} IH: forall e r, ɑ e ⊑ r -> (wp false mask_full e (umconst top)) w' k r.
-      + by move=> e0 r0 He0; apply: (IH _ HLt); rewrite/=/advP.
+      + by move=> e0 r0 He0; apply: (IH _ HLt).
       split; [| split ].
       + by apply IH; rewrite/=; exists r'; rewrite pcm_op_comm Hrret.
       + by apply IH; reflexivity.
@@ -255,17 +257,17 @@ But I can hack around it...
     Qed.
 
     (*
-     * Facts about adv.
+     * Boring facts about adv.
      *)
 
     Lemma adv_timeless {e} :
       valid(timeless(adv e)).
-    Proof. by move=> w n _ w' k r HSW HLe; rewrite/=/advP. Qed.
+    Proof. exact: ownL_timeless. Qed.
 
     Lemma adv_dup {e} :
       valid(adv e → adv e * adv e).
     Proof.
-      move=> _ _ _ w' _ k r' _ _ [β Hβ]; rewrite/=/advP.
+      move=> _ _ _ w' _ k r' _ _ [β Hβ].
       have Hdup: Some(ɑ e) == Some(ɑ e)· Some(ɑ e).
       - rewrite/pcm_op/res_op/pcm_op_prod pcm_op_unit.
         by move/prim_res_eq_hack: (prim_dup e) => <-.
@@ -275,24 +277,24 @@ But I can hack around it...
       exists βe (ɑ e); split; [| split].
       - by move: Hβee Hβ; rewrite /= => -> ->.
       - by rewrite/=; exists β; move: Hβe; rewrite /= => ->.
-      by reflexivity.
+      by rewrite/=; reflexivity.
     Qed.
 
     Lemma adv_fork {e} :
       valid(adv (fork e) ↔ adv e).
-    Proof. by move=> w n r; rewrite/=/advP prim_of_fork; tauto. Qed.
+    Proof. by move=> w n r /=; rewrite prim_of_fork; tauto. Qed.
 
     Lemma adv_fork_ret :
       valid(adv fork_ret).
     Proof.
-      move=> w n r; rewrite/=/advP prim_of_fork_ret /=.
+      move=> w n r /=; rewrite prim_of_fork_ret /=.
       by exists r; rewrite pcm_op_comm pcm_op_unit.
     Qed.
 
     Lemma adv_split {K e} :
       valid(adv (K [[e]]) ↔ adv e * adv (K [[fork_ret]])).
     Proof.
-      move=> w n r; rewrite/=/advP; split; move=> {w n r} _ _ _ r _ _.
+      move=> w n r /=; split; move=> {w n r} _ _ _ r _ _.
       - move=> [β].
         rewrite	(* β · K[e] *)
         	res_of_split	(* β · (e · K) *)
@@ -314,6 +316,108 @@ But I can hack around it...
       by exists αβ.
     Qed.
 
+    (*
+     * More assumptions about primitive reduction.
+     *
+     * I suspect we need these to prove the lifting lemmas. If so,
+     * they should be in core_lang.v.
+     *)
+    Hypothesis atomic_dec : forall e, atomic e + ~atomic e.
+    
+    Hypothesis pure_step : forall e σ e' σ',
+      ~ atomic e ->
+      prim_step (e, σ) (e', σ') ->
+      σ = σ'.
+
+    (*
+     * Proof of concept: Improving the user-interface.
+     *
+     * We can implement adv_step assuming
+     *
+     * • view shifts adv(e) ==>>_⊤ adv(e') for each pure reduction e →
+     * e' and
+     *
+     * • triples {adv(e)} e {v. adv(v)} for each atomic reduction ς; e
+     * → ς'; e'.
+     *
+     * These view shifts and atomic reductions need only be valid
+     * after some w₀ with user-supplied invariants.
+     *)
+
+    Variable w₀ : Wld.
+    
+    Definition valid₀ P := forall {w n r} (HSw₀ : w₀ ⊑ w), P w n r.
+
+    Hypothesis adv_step_pure : forall {e σ e'}
+        (HStep : prim_step (e,σ) (e',σ)),
+      valid₀ (vs mask_full mask_full (adv e) (adv e')).
+    
+    Hypothesis adv_step_atomic : forall {e σ e' σ'}
+        (HStep : prim_step (e,σ) (e',σ'))
+        (HV : is_value e'),
+      valid₀ (ht false mask_full (adv e) e (restrictV adv)).
+    
+    (* This is not precisely what we assumed earlier. The extra factor
+    * r' shouldn't matter once we merge the proofs.
+     *)
+    Lemma adv_step₀ {e σ e' σ' rf w k}
+        (HSw₀ : w₀ ⊑ w)
+        (HStep : prim_step (e,σ) (e',σ'))
+        (HW : wsat σ mask_full (Some (ɑ e) · rf) w @ S k) :
+      exists w' (r' : option res), w ⊑ w' /\
+        wsat σ' mask_full (Some (ɑ e') · r' · rf) w' @ k.
+    Proof.
+      (* common setup. *)
+      case Hα: (Some (ɑ e) · rf) => [α |]; last first.
+      - by exfalso; rewrite Hα in HW; exact: (wsat_nz HW).
+      have HSw : w ⊑ w by reflexivity.
+      have HLe : S k <= S k by omega.
+      have H1e : pcm_unit res ⊑%pcm ɑ e by exact: unit_min.
+      have Hee : ɑ e ⊑%pcm ɑ e by reflexivity.
+      have HLt : k < S k by omega.
+      move: (mask_full_union mask_emp) => Hrew.
+      move: HW; rewrite -{1}Hrew => HW {Hrew}.
+      case: (atomic_dec e) => HA.
+      - (* atomic reduction *)
+        move: (atomic_step _ _ _ _ HA HStep) => HV {HA}.
+        move: (adv_step_atomic _ _ _ _ HStep HV) => He.
+        move: {He Hα HSw₀} (He w (S k) α HSw₀) => He.
+        move: {He HLe H1e Hee α} (He _ HSw _ _ HLe H1e Hee) => He.
+        move: He; rewrite unfold_wp => He.
+        move: (mask_emp_disjoint mask_full) => HD.
+        move: {He HSw HLt HW} (He _ _ _ _ _ HSw HLt HD HW) => [_ [HS _] ].
+        have Hεe: e = ε[[e]] by move: (fill_empty e)->.
+        move: {HS Hεe HStep} (HS _ _ _ _ Hεe HStep) => [w' [r [HSw' [He' HW] ] ] ].
+        (* unroll wp a second time. *)
+        move: He'; rewrite unfold_wp => He'.
+        case Hk': k => [| k']; first by exists w' rf; split.	(* vacuous *)
+        have HSw: w' ⊑ w' by reflexivity.
+        have HLt: k' < k by omega.
+        move: HW; rewrite Hk' => HW.
+        move: {He' HSw HLt HD HW} (He' _ _ _ _ _ HSw HLt HD HW) => [Hv _].
+        move: HV; rewrite -(fill_empty e') => HV.
+        move: {Hv} (Hv HV) => [w'' [r' [HSw'' [ [α Hα] HW] ] ] ].
+        move: Hα.
+        have ->: (Some (ɑ ` (exist is_value (ε [[e']]) HV))) = Some (ɑ ε [[e']]) by done.
+        rewrite pcm_op_comm.
+        case Hαe: (_ · _) => [αe |] => Hα; last done.
+        move: HW; rewrite -Hα -Hαe mask_full_union => HW.
+        by exists w'' (Some α); split; first by transitivity w'.
+      (* pure reduction *)
+      move: (pure_step _ _ _ _ HA HStep) => {HA} Hσ.
+      rewrite Hσ in HStep HW => {Hσ}.
+      move: (adv_step_pure _ _ _ HStep) => {HStep} He.
+      move: {He Hα HSw₀} (He w (S k) α HSw₀) => He.
+      move: {He HLe H1e Hee α} (He _ HSw _ _ HLe H1e Hee) => He.
+      move: (mask_emp_disjoint (mask_full ∪ mask_full)) => HD.
+      move: {He HSw HLt HW} (He _ _ _ _ _ HSw HLt HD HW) => [w' [r' [HSw [ [α Hα] HW] ] ] ].
+      move: HW; rewrite mask_full_union	(* r' · rf *)
+      	-Hα	(* (α · e') · rf) *)
+      	-[Some α · _]pcm_op_comm	(* (e' · α) · rf *)
+      => HW {Hα}.
+      by exists w' (Some α); split; [done | by wsatM HW].
+    Qed.
+        
   End RobustSafety.
 
 End Unsafety.