Add awp tactics

_CoqProject

@@ -6,4 +6,5 @@ theories/lib/flock.v
 theories/lib/locking_heap.v
 theories/c_translation/monad.v
 theories/c_translation/lifting.v
+theories/c_translation/proofmode.v
 theories/c_translation/translation.v

theories/c_translation/proofmode.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac auth.
+From iris.base_logic.lib Require Import fractional.
+From iris_c.lib Require Import locking_heap mset flock.
+From iris_c.c_translation Require Export monad lifting.
+From iris.proofmode Require Import coq_tactics.
+
+Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ R Φ :
+  e = fill K e1 →
+  PureExec φ e1 e2 →
+  φ →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_entails Δ' (awp (fill K e2) R Φ) →
+  envs_entails Δ (awp e R Φ).
+Proof.
+  rewrite /envs_entails=> -> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite HΔ' -awp_pure //.
+Qed.
+
+Tactic Notation "tac_bind_helper" :=
+  lazymatch goal with
+  | |- fill ?K ?e = fill _ ?efoc =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       let K'' := eval cbn[app] in (K' ++ K) in
+       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
+  | |- ?e = fill _ ?efoc =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       replace e with (fill K' e') by (by rewrite ?fill_app))
+  end; reflexivity.
+
+Tactic Notation "awp_pure" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (awp ?e ?R ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_awp_pure _ _ _ _ _ (fill K e'));
+      [tac_bind_helper                (* e = fill K e' *)
+      |apply _                        (* PureExec *)
+      |try fast_done                  (* The pure condition for PureExec *)
+      |apply _                        (* IntoLaters *)
+      |simpl_subst
+      ])
+    || fail "awp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
+  | _ => fail "awp_pure: not an 'awp'"
+  end.
+
+Tactic Notation "awp_if" := awp_pure (If _ _ _).
+Tactic Notation "awp_if_true" := awp_pure (If (Lit (LitBool true)) _ _).
+Tactic Notation "awp_if_false" := awp_pure (If (Lit (LitBool false)) _ _).
+Tactic Notation "awp_unop" := awp_pure (UnOp _ _).
+Tactic Notation "awp_binop" := awp_pure (BinOp _ _ _).
+Tactic Notation "awp_op" := awp_unop || awp_binop.
+Tactic Notation "awp_rec" := awp_pure (App _ _).
+Tactic Notation "awp_lam" := awp_rec.
+Tactic Notation "awp_let" := awp_lam.
+Tactic Notation "awp_seq" := awp_lam.
+Tactic Notation "awp_proj" := awp_pure (Fst _) || awp_pure (Snd _).
+Tactic Notation "awp_case" := awp_pure (Case _ _ _).
+Tactic Notation "awp_match" := awp_case; awp_let.

theories/c_translation/translation.v

@@ -3,7 +3,7 @@ From iris.heap_lang Require Import spin_lock assert par.
 From iris.algebra Require Import frac auth.
 From iris.base_logic.lib Require Import fractional.
 From iris_c.lib Require Import locking_heap mset flock.
-From iris_c.c_translation Require Import monad lifting.
+From iris_c.c_translation Require Import monad lifting proofmode.
 
 Definition a_alloc : val := λ: "x",
   a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
@@ -49,11 +49,10 @@ Section proofs.
   Proof.
     unfold a_load. iIntros "Hv HΦ".
     rewrite /a_ret.
-    iApply (awp_pure [AppRCtx _]); first done. iNext. simpl_subst.
-    iApply (awp_pure []); first done. iNext. simpl_subst.
+    do 2 awp_lam.
     iApply awp_bind.
     iApply awp_value.
-    iApply (awp_pure []); first done. iNext. simpl_subst.
+    awp_let.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
@@ -79,17 +78,17 @@ Section proofs.
     (∀ l, l ↦U v -∗ Φ #l) -∗
     awp (a_alloc (a_ret v)) R Φ.
   Proof.
-    unfold a_alloc. iIntros "HΦ".    
-    rewrite /awp.
-    iIntros (γ π env lk) "#Hfl Hunfl".
-    Opaque acquire release.
-    repeat wp_rec.
-    wp_apply (acquire_cancel_spec with "[$]").
-    iIntros "(Hlkd & Henv & HR)".
-    wp_seq.
+    unfold a_alloc. iIntros "HΦ".
+    rewrite /a_ret.
+    do 2 awp_lam.
+    iApply awp_bind. iApply awp_value.
+    awp_let.
+    iApply awp_atomic_env.
+    iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
     iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks.
-    wp_let. wp_alloc l as "Hl". wp_let.
+    iApply wp_fupd.
+    wp_let. wp_alloc l as "Hl".
     iAssert (⌜σ !! l = None⌝)%I with "[Hl Hls]" as %Hl.
     { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
       iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
@@ -97,12 +96,11 @@ Section proofs.
       by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
     iDestruct "Hl" as "[Hl Hl']".
     iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
-    wp_apply (release_cancel_spec with "[$Hfl $Hlkd $HR Hσ Hls Hl HX]").
-    { iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
-      - rewrite big_sepM_insert; eauto. iFrame. eauto.
-      - iPureIntro. by rewrite locked_locs_alloc_unlocked.
-    }
-    iIntros "Hunfl". wp_seq. iFrame. by iApply "HΦ".
+    iModIntro. iFrame "HR". iSplitR "HΦ Hl'".
+    - iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+      + rewrite big_sepM_insert; eauto. iFrame. eauto.
+      + iPureIntro. by rewrite locked_locs_alloc_unlocked.
+    - by iApply "HΦ".
   Qed.
-        
+
 End proofs.