Commit 3be6384b by Dan Frumin

```- Add awp_pure to lifting.v
- Prove a_load without unfolding awp
- Use IntoVal in some rules in monad.v```
parent ee9db80d
 ... ... @@ -5,4 +5,5 @@ theories/lib/mset.v theories/lib/flock.v theories/lib/locking_heap.v theories/c_translation/monad.v theories/c_translation/lifting.v theories/c_translation/translation.v
 From iris.heap_lang Require Export proofmode notation. From iris.algebra Require Import frac auth. From iris.base_logic.lib Require Import fractional. From iris_c.lib Require Export locking_heap mset flock. From iris_c.c_translation Require Export monad. Notation "l ↦[ x ] v" := (mapsto l x v) (at level 20, x at level 50, format "l ↦[ x ] v") : uPred_scope. Notation "l ↦L v" := (l ↦[LLvl] v)%I (at level 20, format "l ↦L v") : uPred_scope. Notation "l ↦U v" := (l ↦[ULvl] v)%I (at level 20, format "l ↦U v") : uPred_scope. Notation "l ↦L -" := (∃ v, l ↦L v)%I (at level 20, format "l ↦L -") : uPred_scope. Notation "l ↦U -" := (∃ v, l ↦U v)%I (at level 20, format "l ↦U -") : uPred_scope. Section lifting. Context `{locking_heapG Σ, heapG Σ, flockG Σ}. Lemma awp_value (ve : expr) (v : val) R Φ : IntoVal ve v → Φ v -∗ awp (λ: <> <>, ve) R Φ. Proof. intros ?. rewrite -(of_to_val ve v); last done. iIntros "HΦ". rewrite /awp. iIntros (γ π env lk) "Hfl Hunfl". do 2 wp_rec. by iFrame. Qed. Lemma awp_pure K φ e1 e2 R Φ : PureExec φ e1 e2 → φ → ▷ awp (fill K e2) R Φ -∗ awp (fill K e1) R Φ. Proof. iIntros (? Hφ) "Hawp". rewrite /awp. iIntros (γ π env l) "#Hflock Hunfl". replace ((fill K e1) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e1); last first. { by rewrite fill_app. } iApply (wp_bind (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))). wp_pure e1. iSpecialize ("Hawp" with "Hflock Hunfl"). replace ((fill K e2) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e2); last first. { by rewrite fill_app. } rewrite (wp_bind_inv (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))). by iApply "Hawp". Qed. End lifting.
 ... ... @@ -74,10 +74,14 @@ Section a_wp. Qed. (* Use [IntoVal] everywhere *) Lemma awp_bind (f v : val) R Φ : awp v R (λ w, awp (f w) R Φ) -∗ awp (a_bind f v) R Φ. Lemma awp_bind (fe ve : expr) (f v : val) R Φ : IntoVal fe f → IntoVal ve v → awp ve R (λ w, awp (fe w) R Φ) -∗ awp (a_bind fe ve) R Φ. Proof. iIntros "Hwp" (γ π env l) "#Hlock Hunfl". iIntros (? ?) "Hwp". iIntros (γ π env l) "#Hlock Hunfl". rewrite -(of_to_val fe f); last done. rewrite -(of_to_val ve v); last done. rewrite /a_bind /=. do 4 wp_lam. wp_bind (v env l). iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". ... ... @@ -103,11 +107,13 @@ Section a_wp. iIntros "Hunfl1". wp_seq. iFrame. Qed. Lemma awp_atomic_env (v : val) R Φ `{Timeless _ R} : Lemma awp_atomic_env (ve : expr) (v : val) R Φ `{Timeless _ R} : IntoVal ve v → (∀ env, env_inv env -∗ R -∗ WP v env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗ awp (a_atomic_env v) R Φ. WP ve env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗ awp (a_atomic_env ve) R Φ. Proof. intros ?. rewrite -(of_to_val ve v); last done. iIntros "Hwp" (γ π env l) "#Hlock Hunfl". rewrite /a_atomic_env /=. do 3 wp_lam. wp_apply (acquire_cancel_spec with "[\$]"). ... ...
 ... ... @@ -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. From iris_c.c_translation Require Import monad lifting. Definition a_alloc : val := λ: "x", a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x". ... ... @@ -39,18 +39,6 @@ Definition a_seq : val := λ: "env", a_atomic_env (λ: "env", mset_clear "env") "env". Notation "l ↦[ x ] v" := (mapsto l x v) (at level 20, x at level 50, format "l ↦[ x ] v") : uPred_scope. Notation "l ↦L v" := (l ↦[LLvl] v)%I (at level 20, format "l ↦L v") : uPred_scope. Notation "l ↦U v" := (l ↦[ULvl] v)%I (at level 20, format "l ↦U v") : uPred_scope. Notation "l ↦L -" := (∃ v, l ↦L v)%I (at level 20, format "l ↦L -") : uPred_scope. Notation "l ↦U -" := (∃ v, l ↦U v)%I (at level 20, format "l ↦U -") : uPred_scope. Section proofs. Context `{locking_heapG Σ, heapG Σ, flockG Σ}. ... ... @@ -60,13 +48,14 @@ Section proofs. awp (a_load (a_ret #l)) R Φ. Proof. unfold a_load. iIntros "Hv HΦ". rewrite /awp /a_ret. iIntros (γ π env lk) "#Hfl Hunfl". Opaque acquire release. repeat wp_rec. wp_apply (acquire_cancel_spec with "[\$]"). iIntros "(Hlkd & Henv & HR)". wp_seq. rewrite /a_ret. iApply (awp_pure [AppRCtx _]); first done. iNext. simpl_subst. iApply (awp_pure []); first done. iNext. simpl_subst. iApply awp_bind. iApply awp_value. iApply (awp_pure []); first done. iNext. simpl_subst. iApply awp_atomic_env. iIntros (env) "Henv HR". rewrite {2}/env_inv. iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks. ... ... @@ -80,11 +69,10 @@ Section proofs. iIntros "Henv /=". case_decide; first by exfalso. simpl. wp_op. iSplit; eauto. iNext. wp_seq. rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load. iCombine "Hv Hl" as "Hv". wp_seq. wp_apply (release_cancel_spec with "[\$Hfl \$Hlkd \$HR Hσ Hls Henv]"). { iExists X,σ. by iFrame. } iIntros "Hunfl". wp_seq. iFrame. by iApply "HΦ". iCombine "Hv Hl" as "Hv". iFrame "HR". iSplitR "HΦ Hv". - iExists X,σ. by iFrame. - by iApply "HΦ". Qed. Lemma a_alloc_spec R `{Timeless _ R} (v : val) Φ : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!