Lang lemmas

CHANGELOG.md

@@ -11,6 +11,12 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   splitting and other forms of weakening.
 * Updated the strong variant of the opening lemma for cancellable invariants
   to match that of regular invariants, where you can pick the mask at a later time.
+  
+**Changes in program logic:**
+
+* In the axiomatization of ectx languages we replace the axiom of positivity of
+  context composition with an axiom that says if `fill K e` takes a head step,
+  then either `K` is the empty evaluation context or `e` is a value.
 
 **Changes in Coq:**
 

theories/heap_lang/lang.v

@@ -722,7 +722,7 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
 
-(* The following lemma is not provable using the axioms of [ectxi_language].
+(** The following lemma is not provable using the axioms of [ectxi_language].
 The proof requires a case analysis over context items ([destruct i] on the
 last line), which in all cases yields a non-value. To prove this lemma for
 [ectxi_language] in general, we would require that a term of the form
@@ -747,6 +747,13 @@ Proof.
   apply to_val_fill_some in H3 as [-> ->]. subst e. done.
 Qed.
 
+(** If [e1] makes a head step to a value under some state [σ1] then any head
+ step from [e1] under any other state [σ1'] must necessarily be to a value. *)
+Lemma head_step_to_val e1 σ1 κ e2 σ2 efs σ1' κ' e2' σ2' efs' :
+  head_step e1 σ1 κ e2 σ2 efs →
+  head_step e1 σ1' κ' e2' σ2' efs' → is_Some (to_val e2) → is_Some (to_val e2').
+Proof. destruct 1; inversion 1; naive_solver. Qed.
+
 Lemma irreducible_resolve e v1 v2 σ :
   irreducible e σ → irreducible (Resolve e (Val v1) (Val v2)) σ.
 Proof.

theories/program_logic/adequacy.v

@@ -67,11 +67,10 @@ Proof.
   by iApply (IH with "Hσ He Ht").
 Qed.
 
-Lemma wp_safe κs m e σ Φ :
-  state_interp σ κs m -∗
-  WP e {{ Φ }} ={⊤}=∗ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+Lemma wp_not_stuck κs m e σ Φ :
+  state_interp σ κs m -∗ WP e {{ Φ }} ={⊤}=∗ ⌜not_stuck e σ⌝.
 Proof.
-  rewrite wp_unfold /wp_pre. iIntros "Hσ H".
+  rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?; first by eauto.
   iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
   iMod (fupd_plain_mask with "H") as %?; eauto.
@@ -98,8 +97,8 @@ Proof.
     with "[$Hσ $Hwp $Ht]") as "(Hsafe&Hσ&Hwp&Hvs)".
   { iIntros "(Hσ & Hwp & Ht)" (e' -> He').
     apply elem_of_cons in He' as [<-|(t1''&t2''&->)%elem_of_list_split].
-    - iMod (wp_safe with "Hσ Hwp") as "$"; auto.
-    - iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_safe with "Hσ He'"). }
+    - iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto.
+    - iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_not_stuck with "Hσ He'"). }
   iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
   iExists _, _. iSplitL ""; first done. iFrame "Hsafe Hσ".
   iSplitL "Hwp".
@@ -166,14 +165,14 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
   adequate_not_stuck t2 σ2 e2 :
    s = NotStuck →
    rtc erased_step ([e1], σ1) (t2, σ2) →
-   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
+   e2 ∈ t2 → not_stuck e2 σ2
 }.
 
 Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ → state Λ → Prop) :
   adequate s e1 σ1 φ ↔ ∀ t2 σ2,
     rtc erased_step ([e1], σ1) (t2, σ2) →
       (∀ v2 t2', t2 = of_val v2 :: t2' → φ v2 σ2) ∧
-      (∀ e2, s = NotStuck → e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)).
+      (∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2).
 Proof. split. intros []; naive_solver. constructor; naive_solver. Qed.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :

theories/program_logic/ectx_language.v

@@ -29,17 +29,17 @@ Section ectx_language_mixin.
     mixin_fill_inj K : Inj (=) (=) (fill K);
     mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);
 
-    (* There are a whole lot of sensible axioms (like associativity, and left and
-    right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
-    positivity suffices. *)
-    mixin_ectx_positive K1 K2 :
-      comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
-
     mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
       fill K e1 = fill K' e1' →
       to_val e1 = None →
       head_step e1' σ1 κ e2 σ2 efs →
       ∃ K'', K' = comp_ectx K K'';
+
+    (* If [fill K e] takes a head step, then either [e] is a value or [K] is
+       the empty evaluation context. In other words, if [e] is not a value then
+       there cannot be another redex position elsewhere in [fill K e]. *)
+    mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
+      head_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx;
   }.
 End ectx_language_mixin.
 
@@ -87,15 +87,15 @@ Section ectx_language.
   Proof. apply ectx_language_mixin. Qed.
   Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
   Proof. apply ectx_language_mixin. Qed.
-  Lemma ectx_positive K1 K2 :
-    comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx.
-  Proof. apply ectx_language_mixin. Qed.
   Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
     fill K e1 = fill K' e1' →
     to_val e1 = None →
     head_step e1' σ1 κ e2 σ2 efs →
     ∃ K'', K' = comp_ectx K K''.
   Proof. apply ectx_language_mixin. Qed.
+  Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs :
+    head_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx.
+  Proof. apply ectx_language_mixin. Qed.
 
   Definition head_reducible (e : expr Λ) (σ : state Λ) :=
     ∃ κ e' σ' efs, head_step e σ κ e' σ' efs.
@@ -151,6 +151,8 @@ Section ectx_language.
   Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ.
   Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
 
+  Lemma head_step_not_stuck e σ κ e' σ' efs : head_step e σ κ e' σ' efs → not_stuck e σ.
+  Proof. rewrite /not_stuck /reducible /=. eauto 10 using head_prim_step. Qed.
 
   Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
     prim_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
@@ -211,16 +213,30 @@ Section ectx_language.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
+  Lemma head_reducible_prim_step_ctx K e1 σ1 κ e2 σ2 efs :
+    head_reducible e1 σ1 →
+    prim_step (fill K e1) σ1 κ e2 σ2 efs →
+    ∃ e2', e2 = fill K e2' ∧ head_step e1 σ1 κ e2' σ2 efs.
+  Proof.
+    intros (κ'&e2''&σ2''&efs''&?HhstepK) [K' e1' e2' HKe1 -> Hstep].
+    edestruct (step_by_val K) as [K'' ?];
+      eauto using val_head_stuck; simplify_eq/=.
+    rewrite -fill_comp in HKe1; simplify_eq.
+    exists (fill K'' e2'). rewrite fill_comp; split; first done.
+    apply head_ctx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
+    { apply val_head_stuck in Hstep; simplify_eq. }
+    by rewrite !fill_empty.
+  Qed.
+
   Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs :
     head_reducible e1 σ1 →
     prim_step e1 σ1 κ e2 σ2 efs →
     head_step e1 σ1 κ e2 σ2 efs.
   Proof.
-    intros (κ'&e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
-    destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 κ' e2'' σ2'' efs'')
-      as [K' [-> _]%symmetry%ectx_positive];
-      eauto using fill_empty, fill_not_val, val_head_stuck.
-    by rewrite !fill_empty.
+    intros.
+    edestruct (head_reducible_prim_step_ctx empty_ectx) as (?&?&?);
+      rewrite ?fill_empty; eauto.
+    by simplify_eq; rewrite fill_empty.
   Qed.
 
   (* Every evaluation context is a context. *)

theories/program_logic/ectxi_language.v

@@ -109,7 +109,6 @@ Section ectxi_language.
     - intros K1 K2 e. by rewrite /fill /= foldl_app.
     - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
     - done.
-    - by intros [] [].
     - intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
       induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
       destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
@@ -121,6 +120,10 @@ Section ectxi_language.
         apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
       simplify_eq. destruct (IH K') as [K'' ->]; auto.
       exists K''. by rewrite assoc.
+    - intros K e1 σ1 κ e2 σ2 efs.
+      destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
+      rewrite fill_app /=.
+      intros ?%head_ctx_step_val; eauto using fill_val.
   Qed.
 
   Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.

theories/program_logic/language.v

@@ -80,6 +80,8 @@ Section language.
     ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
     to_val e = None ∧ irreducible e σ.
+  Definition not_stuck (e : expr Λ) (σ : state Λ) :=
+    is_Some (to_val e) ∨ reducible e σ.
 
   (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
      invariants when WP ensures safety, i.e., programs never can get stuck.  We
@@ -140,6 +142,11 @@ Section language.
   Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+  Lemma not_not_stuck e σ : ¬not_stuck e σ ↔ stuck e σ.
+  Proof.
+    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
+    destruct (decide (to_val e = None)); naive_solver.
+  Qed.
 
   Lemma strongly_atomic_atomic e a :
     Atomic StronglyAtomic e → Atomic a e.
@@ -175,6 +182,18 @@ Section language.
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.
 
+  Lemma step_insert i t2 σ2 e κ e' σ3 efs :
+    t2 !! i = Some e →
+    prim_step e σ2 κ e' σ3 efs →
+    step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
+  Proof.
+    intros.
+    edestruct (elem_of_list_split_length t2) as (t21&t22&?&?);
+      first (by eauto using elem_of_list_lookup_2); simplify_eq.
+    econstructor; eauto.
+    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
+  Qed.
+
   Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
     t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2).
   Proof.
@@ -188,6 +207,8 @@ Section language.
       prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []
   }.
 
+  Notation pure_steps_tp := (Forall2 (rtc pure_step)).
+
   (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
   succeeding when it did not actually do anything. *)
   Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
@@ -208,7 +229,21 @@ Section language.
   Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
     relations.nsteps pure_step n e1 e2 →
     relations.nsteps pure_step n (K e1) (K e2).
-  Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
+  Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.
+
+  Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
+    rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2).
+  Proof. eauto using rtc_congruence, pure_step_ctx. Qed.
+
+  Lemma not_stuck_under_ectx K `{!@LanguageCtx Λ K} e σ :
+    not_stuck (K e) σ → not_stuck e σ.
+  Proof.
+    rewrite /not_stuck /reducible /=.
+    intros [[? HK]|(?&?&?&?&Hstp)]; simpl in *.
+    - left. apply not_eq_None_Some; intros ?%fill_not_val; simplify_eq.
+    - destruct (to_val e) eqn:?; first by left; eauto.
+      apply fill_step_inv in Hstp; naive_solver.
+  Qed.
 
   (* We do not make this an instance because it is awfully general. *)
   Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
@@ -228,7 +263,58 @@ Section language.
     apply TCForall_Forall, Forall_fmap, Forall_true=> v.
     rewrite /AsVal /=; eauto.
   Qed.
+
   Lemma as_val_is_Some e :
     (∃ v, of_val v = e) → is_Some (to_val e).
   Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
+
+  Lemma prim_step_not_stuck e σ κ e' σ' efs :
+    prim_step e σ κ e' σ' efs → not_stuck e σ.
+  Proof. rewrite /not_stuck /reducible. eauto 10. Qed.
+
+  Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e :
+    rtc pure_step (of_val v) e → to_val e = Some v.
+  Proof.
+    intros ?; rewrite <- to_of_val.
+    f_equal; symmetry; eapply rtc_nf; first done.
+    intros [e' [Hstep _]].
+    destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
+    by rewrite to_of_val in Hval.
+  Qed.
+
+  (** Let thread pools [t1] and [t3] be such that each thread in [t1] makes
+   (zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
+   let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
+   step to thread pool [t2] and state [σ2]. In this situation, either the step
+   from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
+   or, there is an [i] such that [i]th thread does not participate in the
+   pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
+   the [i]th thread starting from [t1]. *)
+  Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 :
+    erased_step (t1, σ1) (t2, σ2) →
+    pure_steps_tp t1 t3 →
+    (σ1 = σ2 ∧ pure_steps_tp t2 t3) ∨
+    (∃ i e efs e' κ,
+      t1 !! i = Some e ∧ t3 !! i = Some e ∧
+      t2 = <[i:=e']>t1 ++ efs ∧
+      prim_step e σ1 κ e' σ2 efs).
+  Proof.
+    intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
+    apply Forall2_app_inv_l in Hps
+      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
+    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
+    - right.
+      exists (length t11), e, efs, e', κ; split_and!; last done.
+      + by rewrite lookup_app_r // Nat.sub_diag.
+      + apply Forall2_length in Hpsteps.
+        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
+      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
+    - edestruct Hprs as (?&?&?&?); first done; simplify_eq.
+      left; split; first done.
+      rewrite right_id_L.
+      eauto using Forall2_app.
+  Qed.
+
 End language.
+
+Notation pure_steps_tp := (Forall2 (rtc pure_step)).