Commit 453d2b16 by Ralf Jung

### heap: start to use proof mode

parent 04e8c944
 ... @@ -2,6 +2,7 @@ From iris.heap_lang Require Export lifting. ... @@ -2,6 +2,7 @@ From iris.heap_lang Require Export lifting. From iris.algebra Require Import upred_big_op frac dec_agree. From iris.algebra Require Import upred_big_op frac dec_agree. From iris.program_logic Require Export invariants ghost_ownership. From iris.program_logic Require Export invariants ghost_ownership. From iris.program_logic Require Import ownership auth. From iris.program_logic Require Import ownership auth. From iris.proofmode Require Import weakestpre. Import uPred. Import uPred. (* TODO: The entire construction could be generalized to arbitrary languages that have (* TODO: The entire construction could be generalized to arbitrary languages that have a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary ... @@ -140,29 +141,25 @@ Section heap. ... @@ -140,29 +141,25 @@ Section heap. (** Weakest precondition *) (** Weakest precondition *) Lemma wp_alloc N E e v P Φ : Lemma wp_alloc N E e v P Φ : to_val e = Some v → to_val e = Some v → nclose N ⊆ E → P ⊢ heap_ctx N → nclose N ⊆ E → (heap_ctx N ★ ▷ ∀ l, l ↦ v -★ Φ (LitV \$ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}. P ⊢ (▷ ∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) → P ⊢ WP Alloc e @ E {{ Φ }}. Proof. Proof. rewrite /heap_ctx /heap_inv=> ??? HP. iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx. trans (|={E}=> auth_own heap_name ∅ ★ P)%I. iPvs (auth_empty heap_name) as "Hheap". { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } (* TODO: use an iTactic *) apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) apply (auth_fsa heap_inv (wp_fsa (Alloc e))) with N heap_name ∅; simpl; eauto with I. with N heap_name ∅; simpl; eauto with I. rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l. iFrame "Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id. rewrite -assoc left_id; apply const_elim_sep_l=> ?. iIntros "[% Hheap]". rewrite /heap_inv. rewrite -(wp_alloc_pst _ (of_heap h)) //. iApply wp_alloc_pst; first done. iFrame "Hheap". iNext. apply sep_mono_r; rewrite HP; apply later_mono. iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _. apply forall_mono=> l; apply wand_intro_l. rewrite [{[ _ := _ ]} ⋅ ∅]right_id. rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?. rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None. rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})). iFrame "Hheap". iSplit. repeat erewrite <-exist_intro by apply _; simpl. { (* FIXME iTactic for introduction of constant assertions? *) rewrite -of_heap_insert left_id right_id. rewrite const_equiv; first done. split; first done. rewrite /heap_mapsto. ecancel [_ -★ Φ _]%I. by apply (insert_valid h). } rewrite -(insert_singleton_op h); last by apply of_heap_None. iIntros "Hheap". iApply "HΦ". rewrite /heap_mapsto. done. rewrite const_equiv; last by apply (insert_valid h). by rewrite left_id -later_intro. Qed. Qed. Lemma wp_load N E l q v P Φ : Lemma wp_load N E l q v P Φ : ... ...
 ... @@ -25,7 +25,8 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ : ... @@ -25,7 +25,8 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ : Δ'' ⊢ Φ (LitV (LitLoc l))) → Δ'' ⊢ Φ (LitV (LitLoc l))) → Δ ⊢ WP Alloc e @ E {{ Φ }}. Δ ⊢ WP Alloc e @ E {{ Φ }}. Proof. Proof. intros ???? HΔ; eapply wp_alloc; eauto. intros ???? HΔ. etrans; last apply: wp_alloc; eauto. rewrite -always_and_sep_l. iSplit; first done. rewrite strip_later_env_sound; apply later_mono, forall_intro=> l. rewrite strip_later_env_sound; apply later_mono, forall_intro=> l. destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl. destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'. by rewrite right_id HΔ'. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!