add an invariant-based awp_rule for while loop

theories/c_translation/translation.v

@@ -141,6 +141,25 @@ Section proofs.
     iModIntro. by awp_lam.
   Qed.
 
+  Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
+   □ (I -∗ awp c R (λ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨
+                         (⌜v = #true⌝ ∧ (awp b R (λ _, U I))))%I) -∗
+    I -∗
+    awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
+   Proof.
+     iIntros "#Hinv Hi". iLöb as "IH".
+     iApply a_while_spec. iNext.
+     iApply a_if_spec.
+     iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv").
+     iIntros (v) "[(% & H) | (% & H)] //="; subst.
+     - iRight. iSplit; by eauto; iApply a_seq_spec.
+     - iLeft. iSplit; first eauto. awp_seq.
+       iApply a_sequence_spec. awp_seq.
+       iApply (awp_wand with "H").
+       iIntros (v) "Hi". iModIntro. awp_seq.
+       by iApply ("IH" with "Hi").
+   Qed.
+
   Lemma a_load_spec R Φ e :
     awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦U w ∗ (l ↦U w -∗ Φ w)) -∗
     awp (a_load e) R Φ.
@@ -269,3 +288,32 @@ Section proofs.
 
 
 End proofs.
+
+
+Section Derived.
+
+  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
+
+
+  Lemma a_load_ret (l: loc) (w: val) R Φ:
+    l ↦U w ∗ (l ↦U w -∗ Φ w) -∗
+    awp (a_load (a_ret (#l)%E)) R Φ.
+  Proof.
+    iIntros "H". iApply a_load_spec.
+    iApply awp_ret. wp_value_head.
+    iExists l, w. by iFrame.
+  Qed.
+
+  Lemma a_alloc_ret (w: val) R Φ:
+    (∀ (l: loc), (l ↦U w -∗ Φ #l)) -∗
+    awp (a_alloc (a_ret w)) R Φ.
+  Proof.
+    iIntros "H". iApply a_alloc_spec.
+    iApply awp_ret. by wp_value_head.
+  Qed.
+
+End Derived.
+
+  Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
+  Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
+  Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
\ No newline at end of file

theories/tests/fact.v

@@ -33,27 +33,6 @@ Section factorial_spec.
 
   Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
 
-  Lemma a_load_ret (l: loc) (w: val) R Φ:
-    l ↦U w ∗ (l ↦U w -∗ Φ w) -∗
-    awp (a_load (a_ret (#l)%E)) R Φ.
-  Proof.
-    iIntros "H". iApply a_load_spec.
-    iApply awp_ret. wp_value_head.
-    iExists l, w. by iFrame.
-  Qed.
-
-  Lemma a_alloc_ret (w: val) R Φ:
-    (∀ (l: loc), (l ↦U w -∗ Φ #l)) -∗
-    awp (a_alloc (a_ret w)) R Φ.
-  Proof.
-    iIntros "H". iApply a_alloc_spec.
-    iApply awp_ret. by wp_value_head.
-  Qed.
-
-  Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
-  Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
-  Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
-
   Lemma incr_spec (l : loc) (n : Z) R Φ :
     l ↦U #n -∗ (l ↦L #(n+1) -∗ Φ #(n+1)) -∗
     awp (incr #l) R Φ.

theories/tests/test1.v

@@ -17,9 +17,7 @@ Section test.
     iApply a_seq_spec.
     iModIntro.
     awp_lam.
-    iApply a_load_spec.
-    iApply awp_ret. iApply wp_value; eauto.
-    iExists l, #1. iFrame. eauto.
+    awp_load_ret l #1.
   Qed.
 
 
@@ -54,17 +52,13 @@ Section test.
     iIntros "Hl1 Hl2".
     do 2 awp_lam.
     iApply awp_bind.
-    iApply a_alloc_spec.
-    iApply awp_ret. iApply wp_value.
-    iIntros (r) "Hr". awp_lam.
+    awp_alloc_ret #0 r "Hr".
 
     iApply a_sequence_spec.
     iApply (a_store_spec _ _ (λ l, ⌜l = r⌝)%I
                              (λ v, ⌜v = v1⌝ ∗ l1 ↦U v1)%I with "[] [Hl1]").
-    { iApply awp_ret. iApply wp_value; eauto. }
-    { iApply a_load_spec.
-      iApply awp_ret. iApply wp_value.
-      iExists _, _; iFrame. eauto. }
+    { awp_ret_value. }
+    { awp_load_ret l1 v1. }
     iIntros (? ? ->) "[% Hl1]"; subst.
     iExists _; iFrame. iIntros "Hr". iModIntro.
     awp_seq.
@@ -72,10 +66,8 @@ Section test.
     iApply a_sequence_spec.
     iApply (a_store_spec _ _ (λ l, ⌜l = l1⌝)%I
                              (λ v, ⌜v = v2⌝ ∗ l2 ↦U v2)%I with "[] [Hl2]").
-    { iApply awp_ret. iApply wp_value; eauto. }
-    { iApply a_load_spec.
-      iApply awp_ret. iApply wp_value.
-      iExists _, _; iFrame. eauto. }
+    { awp_ret_value. }
+    { awp_load_ret l2 v2. }
     iIntros (? ? ->) "[% Hl2]"; subst.
     iExists _; iFrame. iIntros "Hl1". iModIntro.
     awp_seq.
@@ -83,10 +75,8 @@ Section test.
     iApply awp_bind.
     iApply (a_store_spec _ _ (λ l, ⌜l = l2⌝)%I
                              (λ v, ⌜v = v1⌝ ∗ r ↦U v1)%I with "[] [Hr]").
-    { iApply awp_ret. iApply wp_value; eauto. }
-    { iApply a_load_spec.
-      iApply awp_ret. iApply wp_value.
-      iExists _, _; iFrame. eauto. }
+    { awp_ret_value. }
+    { awp_load_ret r v1. }
     iIntros (? ? ->) "[% Hr]"; subst.
 
     iExists _; iFrame. iIntros "Hl2".