diff --git a/theories/c_translation/derived.v b/theories/c_translation/derived.v index d5d5b9cfc8f579ff21740da607f00b054e7240d3..988f429c73ac7b17c0dc427d279121be3403a112 100644 --- a/theories/c_translation/derived.v +++ b/theories/c_translation/derived.v @@ -8,7 +8,6 @@ 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 Φ. @@ -18,11 +17,12 @@ Section Derived. 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 Φ. + Lemma a_alloc_ret (e: expr) (ev: val) R Φ: + IntoVal e ev → + (∀ (l: loc), (l ↦U ev -∗ Φ #l)) -∗ + awp (a_alloc (a_ret e)) R Φ. Proof. - iIntros "H". iApply a_alloc_spec. + iIntros (<-%of_to_val) "H". iApply a_alloc_spec. iApply awp_ret. by wp_value_head. Qed. diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v index 101b0ff584686176b9d8d1adbabbde344a563c13..67c5689f8d7eaf1f84189926c9d14e9ded3155ab 100644 --- a/theories/c_translation/monad.v +++ b/theories/c_translation/monad.v @@ -113,7 +113,6 @@ Section a_wp_rules. iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. iFrame. Qed. - (* Use [IntoVal] everywhere *) Lemma awp_bind (f e : expr) R Φ : AsVal f → awp e R (λ ev, awp (f ev) R Φ) -∗ @@ -127,7 +126,7 @@ Section a_wp_rules. iIntros (v) "H". by iApply ("H" with "[\$]"). Qed. - Lemma awp_atomic e (ev : val) R Φ : + Lemma awp_atomic (e : expr) (ev : val) R Φ : IntoVal e ev → (R -∗ ∃ R', R' ∗ awp (ev #()) R' (λ w, R' -∗ R ∗ Φ w)) -∗ awp (a_atomic e) R Φ. @@ -148,7 +147,7 @@ Section a_wp_rules. iIntros "Hunfl1". wp_seq. iFrame. Qed. - Lemma awp_atomic_env e (ev : val) R Φ : + Lemma awp_atomic_env (e : expr) (ev : val) R Φ : IntoVal e ev → (∀ env, env_inv env -∗ R -∗ WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗ @@ -191,11 +190,12 @@ End a_wp_rules. Section a_wp_run. Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}. - Lemma awp_run (v : val) R Φ : - R -∗ (∀ `{locking_heapG Σ}, awp v R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗ - WP a_run v {{ Φ }}. + Lemma awp_run (e : expr) R Φ : + AsVal e → + R -∗ (∀ `{locking_heapG Σ}, awp e R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗ + WP a_run e {{ Φ }}. Proof. - iIntros "HR Hwp". rewrite /awp /a_run /=. wp_let. + iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let. wp_bind (mset_create #()). iApply mset_create_spec; first done. iNext. iIntros (env) "Henv". wp_let. iMod (locking_heap_init ∅) as (?) "Hσ". diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index dab73ecc01c321de36d8249a2463c1838965281d..66eef0b87fd515b23ad237e4b8fa7f13c722074f 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -79,7 +79,7 @@ Section proofs. iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if. Qed. - Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ : + Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : awp e1 R Φ -∗ awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ. Proof. iIntros "HΦ". @@ -88,7 +88,7 @@ Section proofs. iLeft. iSplit; eauto. by awp_seq. Qed. - Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ : + Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : awp e2 R Φ -∗ awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ. Proof. iIntros "HΦ".