total_lifting.v 3.11 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
From iris.program_logic Require Export total_weakestpre.
From iris.base_logic Require Export big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

Section lifting.
Context `{irisG Λ Σ}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.

Lemma twp_lift_step s E Φ e1 :
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
    if s is NotStuck then reducible e1 σ1 else True 
     e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
      state_interp σ2  WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.

(** Derived lifting lemmas. *)
Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
  ( σ1, reducible e1 σ1) 
  ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
  (|={E}=>  e2 efs σ, prim_step e1 σ e2 σ efs 
    WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
  { eapply reducible_not_val, (Hsafe inhabitant). }
  iIntros (σ1) "Hσ". iMod "H".
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
  iSplit; [by destruct s|]; iIntros (e2 σ2 efs ?).
  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
  iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
Qed.

(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
Lemma twp_lift_atomic_step {s E Φ} e1 :
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    if s is NotStuck then reducible e1 σ1 else True 
     e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1".
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
  iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_".
  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
  destruct (to_val e2) eqn:?; last by iExFalso.
  by iApply twp_value.
Qed.

Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
  ( σ1, reducible e1 σ1) 
  ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
  (|={E}=> WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
  { by intros; eapply Hpuredet. }
  by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet).
Qed.

Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
  PureExec φ e1 e2 
  φ 
  WP e2 @ s; E [{ Φ }]  WP e1 @ s; E [{ Φ }].
Proof.
  iIntros ([??] Hφ) "HWP".
  iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
Qed.
End lifting.