total_lifting.v 3.53 KB
Newer Older
1
From iris.program_logic Require Export total_weakestpre.
2
From iris.bi Require Export big_op.
3 4 5 6 7 8 9 10 11 12 13
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 Σ.

14 15
Hint Resolve reducible_no_obs_reducible.

16 17
Lemma twp_lift_step s E Φ e1 :
  to_val e1 = None 
18
  ( σ1 κs n, state_interp σ1 κs n ={E,}=
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
19 20
    if s is NotStuck then reducible_no_obs e1 σ1 else True 
     κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,E}=
21 22 23
      ⌜κ = [] 
      state_interp σ2 κs (length efs + n) 
      WP e2 @ s; E [{ Φ }] 
24
      [ list] ef  efs, WP ef @ s;  [{ fork_post }])
25 26 27
   WP e1 @ s; E [{ Φ }].
Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.

28 29 30
(** Derived lifting lemmas. *)
Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
  ( σ1, reducible_no_obs e1 σ1) 
31
  ( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κ = []  σ2 = σ1  efs = []) 
32 33 34 35 36 37 38 39 40 41 42 43 44
  (|={E}=>  κ e2 efs σ, prim_step e1 σ κ e2 σ efs  WP e2 @ s; E [{ Φ }])
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
  iIntros (σ1 κs n) "Hσ".
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
  { iPureIntro. destruct s; auto. }
  iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
  iMod "Hclose" as "_". iModIntro.
  iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
Qed.

45 46 47 48
(* 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 
49
  ( σ1 κs n, state_interp σ1 κs n ={E}=
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
50 51
    if s is NotStuck then reducible_no_obs e1 σ1 else True 
     κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={E}=
52 53 54
      ⌜κ = [] 
      state_interp σ2 κs (length efs + n) 
      from_option Φ False (to_val e2) 
55
      [ list] ef  efs, WP ef @ s;  [{ fork_post }])
56 57
   WP e1 @ s; E [{ Φ }].
Proof.
58 59
  iIntros (?) "H".
  iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs n) "Hσ1".
60 61
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
62 63
  iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
  iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & $ & HΦ & $)"; first by eauto.
64
  destruct (to_val e2) eqn:?; last by iExFalso.
65
  iApply twp_value; last done. by apply of_to_val.
66 67
Qed.

68 69 70
Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
  ( σ1, reducible_no_obs e1 σ1) 
  ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' 
71
    κ = []  σ2 = σ1  e2' = e2  efs' = []) 
72 73 74 75 76 77 78
  (|={E}=> WP e2 @ s; E [{ Φ }])  WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step_no_fork s E); try done.
  { naive_solver. }
  iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
Qed.

79 80
Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 
81 82 83
  φ 
  WP e2 @ s; E [{ Φ }]  WP e1 @ s; E [{ Φ }].
Proof.
84 85
  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
86 87
  iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
  iModIntro. by iApply "IH".
88 89
Qed.
End lifting.