Library iris.heap_lang.refine
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Import lang tactics.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership refine_ectx_delay
refine_raw_adequacy nat_delayed_language.
From iris.program_logic Require Import ownership auth refine_raw ectx_lifting.
From iris.proofmode Require Import weakestpre.
Import uPred.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Section refine.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types ef : option expr.
Local Open Scope nat_scope.
From iris.heap_lang Require Import lang tactics.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership refine_ectx_delay
refine_raw_adequacy nat_delayed_language.
From iris.program_logic Require Import ownership auth refine_raw ectx_lifting.
From iris.proofmode Require Import weakestpre.
Import uPred.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Section refine.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types ef : option expr.
Local Open Scope nat_scope.
Base axioms for core primitives of the language: Stateful reductions.
Lemma refine_alloc_pst' E σ K d d' e v i:
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v →
(ownT i (Alloc e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitLoc (fresh (dom _ σ)))) K d' ★ ownSP (<[fresh (dom _ σ):=v]>σ) .
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_load_pst E σ K d d' l v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some v →
(ownT i (Load (Lit (LitLoc l))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (of_val v) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_store_pst E σ K d d' l e v v' i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some v' →
(ownT i (Store (Lit (LitLoc l)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit LitUnit) K d' ★ ownSP (<[l:=v]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
econstructor. eauto.
Qed.
Lemma refine_cas_fail_pst E σ K d d' l e1 v1 e2 v2 v' i:
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
(ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitBool false)) K d' ★ ownSP σ.
Proof.
iIntros (??????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_cas_suc_pst E σ K d d' l e1 v1 e2 v2 i:
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
(ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitBool true)) K d' ★ ownSP (<[l:=v2]>σ).
Proof.
iIntros (?????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_swap_pst E σ K d d' l v e v' i:
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v' → σ !! l = Some v →
(ownT i (Swap (Lit (LitLoc l)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (of_val v) K d' ★ ownSP (<[l:=v']>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_fai_pst E σ K d d' l k i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (LitV $ LitInt k) →
(ownT i (FAI (Lit (LitLoc l))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitInt k) K d' ★ ownSP (<[l:=LitV $ LitInt (k+1)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v →
(ownT i (Alloc e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitLoc (fresh (dom _ σ)))) K d' ★ ownSP (<[fresh (dom _ σ):=v]>σ) .
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_load_pst E σ K d d' l v i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some v →
(ownT i (Load (Lit (LitLoc l))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (of_val v) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
Qed.
Lemma refine_store_pst E σ K d d' l e v v' i :
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v → σ !! l = Some v' →
(ownT i (Store (Lit (LitLoc l)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit LitUnit) K d' ★ ownSP (<[l:=v]>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; auto.
econstructor. eauto.
Qed.
Lemma refine_cas_fail_pst E σ K d d' l e1 v1 e2 v2 v' i:
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
(ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitBool false)) K d' ★ ownSP σ.
Proof.
iIntros (??????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_cas_suc_pst E σ K d d' l e1 v1 e2 v2 i:
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
(ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit (LitBool true)) K d' ★ ownSP (<[l:=v2]>σ).
Proof.
iIntros (?????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_swap_pst E σ K d d' l v e v' i:
d ≤ Kd →
d' ≤ Kd →
to_val e = Some v' → σ !! l = Some v →
(ownT i (Swap (Lit (LitLoc l)) e) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (of_val v) K d' ★ ownSP (<[l:=v']>σ).
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_fai_pst E σ K d d' l k i:
d ≤ Kd →
d' ≤ Kd →
σ !! l = Some (LitV $ LitInt k) →
(ownT i (FAI (Lit (LitLoc l))) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit $ LitInt k) K d' ★ ownSP (<[l:=LitV $ LitInt (k+1)]>σ).
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Base axioms for core primitives of the language: Stateless reductions.
Unfortunately, whereas the wp rules do not require physical state ownership,
the refinement monoid construction does require ownSP. Hence, we suffice them by pst
as in the above rules. Later, when we develop the heap monoid for the source language,
we prove versions without this ownership requirement.
Lemma refine_fork_pst E σ K d d' e i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (Fork e) K d ★ ownSP σ) ⊢
|={E}=>> ∃ i', ownT i (Lit LitUnit) K d' ★ ownT i' e [] (fresh_delay heap_lang Fd e)
★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_fork; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_rec_pst E σ K d d' f x erec e1 e2 i :
d ≤ Kd →
d' ≤ Kd →
e1 = Rec f x erec →
is_Some (to_val e2) →
Closed (f :b: x :b: []) erec →
(ownT i (App e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (subst' x e2 (subst' f e1 erec)) K d' ★ ownSP σ.
Proof.
intros ?? → [v2 ?] ?.
iIntros "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto; rewrite //= ?right_id.
eapply head_prim_step.
inv_head_step; eauto.
econstructor; eauto using to_of_val.
Qed.
Lemma refine_un_op_pst E op σ K d d' l l' i:
d ≤ Kd →
d' ≤ Kd →
un_op_eval op l = Some l' →
(ownT i (UnOp op (Lit l)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit l') K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_bin_op_pst E op σ K d d' l1 l2 l' i:
d ≤ Kd →
d' ≤ Kd →
bin_op_eval op l1 l2 = Some l' →
(ownT i (BinOp op (Lit l1) (Lit l2)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (Lit l') K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_if_true_pst E σ K d d' e1 e2 i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (If (Lit (LitBool true)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e1 K d' ★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_if_false_pst E σ K d d' e1 e2 i :
d ≤ Kd →
d' ≤ Kd →
(ownT i (If (Lit (LitBool false)) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e2 K d' ★ ownSP σ.
Proof.
iIntros (??) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_fst_pst E σ K d d' e1 v1 e2 v2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 →
(ownT i (Fst (Pair e1 e2)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e1 K d' ★ ownSP σ.
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_snd_pst E σ K d d' e1 v1 e2 v2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e1 = Some v1 → to_val e2 = Some v2 →
(ownT i (Snd (Pair e1 e2)) K d ★ ownSP σ) ⊢
|={E}=>> ownT i e2 K d' ★ ownSP σ.
Proof.
iIntros (????) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_case_inl_pst E σ K d d' e0 v0 e1 e2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e0 = Some v0 →
(ownT i (Case (InjL e0) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e1 e0) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
Lemma refine_case_inr_pst E σ K d d' e0 v0 e1 e2 i :
d ≤ Kd →
d' ≤ Kd →
to_val e0 = Some v0 →
(ownT i (Case (InjR e0) e1 e2) K d ★ ownSP σ) ⊢
|={E}=>> ownT i (App e2 e0) K d' ★ ownSP σ.
Proof.
iIntros (???) "Hown".
iApply ownT_ownSP_step_nofork_ctx1; last done; eauto.
eapply head_prim_step. econstructor; eauto.
Qed.
End refine.