total_adequacy.v 5.58 KB
Newer Older
1
From iris.program_logic Require Export total_weakestpre adequacy.
2 3
From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.bi Require Import big_op fixpoint.
4 5 6 7 8 9 10 11 12 13
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.

Section adequacy.
Context `{irisG Λ Σ}.
Implicit Types e : expr Λ.

Definition twptp_pre (twptp : list (expr Λ)  iProp Σ)
    (t1 : list (expr Λ)) : iProp Σ :=
14 15
  ( t2 σ1 κ κs σ2 n, step (t1,σ1) κ (t2,σ2) -
    state_interp σ1 κs n ={}=  n', ⌜κ = []  state_interp σ2 κs n'  twptp t2)%I.
16 17

Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ)  iProp Σ) :
18
  (<pers> ( t, twptp1 t - twptp2 t) 
19 20 21
   t, twptp_pre twptp1 t - twptp_pre twptp2 t)%I.
Proof.
  iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
22 23 24
  iIntros (t2 σ1 κ κs σ2 n1) "Hstep Hσ".
  iMod ("Hwp" with "[$] [$]") as (n2) "($ & Hσ & ?)".
  iModIntro. iExists n2. iFrame "Hσ". by iApply "H".
25 26
Qed.

27
Local Instance twptp_pre_mono' : BiMonoPred twptp_pre.
28 29 30 31 32 33
Proof.
  constructor; first apply twptp_pre_mono.
  intros wp Hwp n t1 t2 ?%(discrete_iff _ _)%leibniz_equiv; solve_proper.
Qed.

Definition twptp (t : list (expr Λ)) : iProp Σ :=
34
  bi_least_fixpoint twptp_pre t.
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52

Lemma twptp_unfold t : twptp t  twptp_pre twptp t.
Proof. by rewrite /twptp least_fixpoint_unfold. Qed.

Lemma twptp_ind Ψ :
  ((  t, twptp_pre (λ t, Ψ t  twptp t) t - Ψ t)   t, twptp t - Ψ t)%I.
Proof.
  iIntros "#IH" (t) "H".
  assert (NonExpansive Ψ).
  { by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
  iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
  iIntros "!#" (t') "H". by iApply "IH".
Qed.

Instance twptp_Permutation : Proper (() ==> ()) twptp.
Proof.
  iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
  iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
53
  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
54
  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
55 56
  iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
  iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
57 58 59 60 61 62 63 64
Qed.

Lemma twptp_app t1 t2 : twptp t1 - twptp t2 - twptp (t1 ++ t2).
Proof.
  iIntros "H1". iRevert (t2). iRevert (t1) "H1".
  iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
  iRevert (t1) "IH1"; iRevert (t2) "H2".
  iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
65
  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1".
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67
  destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=.
  apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
68
  - destruct t as [|e1' ?]; simplify_eq/=.
69
    + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
70
      { by eapply step_atomic with (t1:=[]). }
71 72
      iModIntro. iExists n2. iFrame "Hσ".
      rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
73
      by setoid_rewrite (right_id_L [] (++)).
74
    + iMod ("IH1" with "[%] Hσ1") as (n2) "($ & Hσ & IH1 & _)"; first by econstructor.
75 76 77
      iAssert (twptp t2) with "[IH2]" as "Ht2".
      { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
        iIntros "!# * [_ ?] //". }
78 79 80 81
      iModIntro. iExists n2. iFrame "Hσ".
      rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L. by iApply "IH1".
  - iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)"; first by econstructor.
    iModIntro. iExists n2. iFrame "Hσ". rewrite -assoc_L. by iApply "IH2".
82 83 84 85 86 87 88
Qed.

Lemma twp_twptp s Φ e : WP e @ s;  [{ Φ }] - twptp [e].
Proof.
  iIntros "He". remember ( : coPset) as E eqn:HE.
  iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
  iIntros "!#" (e E Φ); iIntros "IH" (->).
89
  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ2' n Hstep) "Hσ1".
90
  destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
91 92 93 94
    simplify_eq/=; try discriminate_list.
  destruct (to_val e1) as [v|] eqn:He1.
  { apply val_stuck in Hstep; naive_solver. }
  iMod ("IH" with "Hσ1") as "[_ IH]".
95 96
  iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
  iModIntro. iExists (length efs + n). iFrame "Hσ".
97 98
  iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
  clear. iInduction efs as [|e efs] "IH"; simpl.
99
  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n1 Hstep).
100 101
    destruct Hstep; simplify_eq/=; discriminate_list. }
  iDestruct "IHfork" as "[[IH' _] IHfork]".
102
  iApply (twptp_app [_] with "[IH']"). by iApply "IH'". by iApply "IH".
103 104
Qed.

105 106
Lemma twptp_total n σ t :
  state_interp σ [] n - twptp t ={}=  sn erased_step (t, σ).
107
Proof.
108 109
  iIntros "Hσ Ht". iRevert (σ n) "Hσ". iRevert (t) "Ht".
  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ n) "Hσ".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
110
  iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
111 112
  rewrite /twptp_pre.
  iMod ("IH" with "[% //] Hσ") as (n' ->) "[Hσ [H _]]".
113
  by iApply "H".
114 115 116
Qed.
End adequacy.

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
117
Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
118
  ( `{Hinv : invG Σ},
119 120
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
121
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
122
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
123
       stateI σ [] 0  WP e @ s;  [{ Φ }])%I) 
124
  sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
125
Proof.
126 127
  intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
  apply (fupd_plain_soundness  _)=> Hinv.
128
  iMod (Hwp) as (stateI fork_post) "[Hσ H]".
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
  iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)).
131
Qed.