adequacy.v 6.24 KB
Newer Older
1 2
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 100 (_  _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Local Hint Extern 10 ({_} _) =>
6 7 8
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10

Section adequacy.
11
Context {Λ : language} {Σ : iFunctor}.
12
Implicit Types e : expr Λ.
13 14 15
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ  iProp Λ Σ.
Implicit Types Φs : list (val Λ  iProp Λ Σ).
16
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18 19 20
Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp  e Φ) n r)).
Lemma wptp_le Φs es rs n n' :
  {n'} (big_op rs)  wptp n es Φs rs  n'  n  wptp n' es Φs rs.
21
Proof. induction 2; constructor; eauto using uPred_closed. Qed.
22
Lemma nsteps_wptp Φs k n tσ1 tσ2 rs1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  nsteps step k tσ1 tσ2 
24
  1 < n  wptp (k + n) (tσ1.1) Φs rs1 
25
  wsat (k + n)  (tσ1.2) (big_op rs1) 
26
   rs2 Φs', wptp n (tσ2.1) (Φs ++ Φs') rs2  wsat n  (tσ2.2) (big_op rs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof.
28
  intros Hsteps Hn; revert Φs rs1.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
30
    simplify_eq/=; intros Φs rs.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  { by intros; exists rs, []; rewrite right_id_L. }
32 33
  intros (Φs1&?&rs1&?&->&->&?&
    (Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
Ralf Jung's avatar
Ralf Jung committed
34
  rewrite wp_eq in Hwp.
35
  destruct (wp_step_inv   Φ e1 (k + n) (S (k + n)) σ1 r
36
    (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using val_stuck.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39 40
  { by rewrite right_id_L -big_op_cons Permutation_middle. }
  destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
  revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
  destruct ef as [e'|].
41 42
  - destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, True%I])
      (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Φs'&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    { apply Forall3_app, Forall3_cons,
Ralf Jung's avatar
Ralf Jung committed
44 45
        Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le; [|];
      rewrite wp_eq; eauto. }
46 47
    { by rewrite -Permutation_middle /= (assoc (++))
        (comm (++)) /= assoc big_op_app. }
48 49 50
    exists rs', ([λ _, True%I] ++ Φs'); split; auto.
    by rewrite (assoc _ _ _ Φs') -(assoc _ Φs1).
  - apply (IH (Φs1 ++ Φ :: Φs2) (rs1 ++ r2  r2' :: rs2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
    { rewrite /option_list right_id_L.
      apply Forall3_app, Forall3_cons; eauto using wptp_le.
Ralf Jung's avatar
Ralf Jung committed
53
      rewrite wp_eq.
54
      apply uPred_closed with (k + n);
55
        first apply uPred_mono with r2; eauto using cmra_includedN_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
    by rewrite -Permutation_middle /= big_op_app.
Qed.
Ralf Jung's avatar
Ralf Jung committed
58
Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
59
  P  WP e1 {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  nsteps step k ([e1],σ1) (t2,σ2) 
61
  1 < n  wsat (k + n)  σ1 r1 
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  P (k + n) r1 
63
   rs2 Φs', wptp n t2 (Φ :: Φs') rs2  wsat n  σ2 (big_op rs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof.
65
  intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
66
    rewrite /big_op ?right_id; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  constructor; last constructor.
Ralf Jung's avatar
Ralf Jung committed
68
  apply Hht; by eauto using cmra_included_core.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
Ralf Jung's avatar
Ralf Jung committed
70 71

Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
72
   m 
73
  (ownP σ1  ownG m)  WP e1 {{ Φ }} 
74
  rtc step ([e1],σ1) (t2,σ2) 
75
   rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2  wsat 2  σ2 (big_op rs2).
76
Proof.
77
  intros Hv ? [k ?]%rtc_nsteps.
78
  eapply wp_adequacy_steps with (r1 := (Res  (Excl σ1) m)); eauto; [|].
79
  { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
80
  uPred.unseal; exists (Res  (Excl σ1) ), (Res   m); split_and?.
81
  - by rewrite Res_op ?left_id ?right_id.
82
  - rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
83
  - by apply ownG_spec.
84
Qed.
Ralf Jung's avatar
Ralf Jung committed
85 86

Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
87
   m 
88
  (ownP σ1  ownG m)  WP e @ E {{ v',  φ v' }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91
  rtc step ([e], σ1) (of_val v :: t2, σ2) 
  φ v.
Proof.
92
  intros Hv ? Hs.
Ralf Jung's avatar
Ralf Jung committed
93
  destruct (wp_adequacy_own (λ v',  φ v')%I e (of_val v :: t2) σ1 m σ2)
94
             as (rs2&Qs&Hwptp&?); auto.
Ralf Jung's avatar
Ralf Jung committed
95
  { by rewrite -(wp_mask_weaken E ). }
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
Ralf Jung's avatar
Ralf Jung committed
97 98
  move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp.
  rewrite pvs_eq in Hwp.
99
  destruct (Hwp (big_op rs) 2  σ2) as [r' []]; rewrite ?right_id_L; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Qed.
Ralf Jung's avatar
Ralf Jung committed
101 102

Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 :
103
   m 
104
  {{ ownP σ1  ownG m }} e @ E {{ v',  φ v' }} 
Ralf Jung's avatar
Ralf Jung committed
105 106 107 108 109 110 111 112 113
  rtc step ([e], σ1) (of_val v :: t2, σ2) 
  φ v.
Proof.
  intros ? Hht. eapply wp_adequacy_result with (E:=E); first done.
  move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
Qed.

Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
   m 
114
  (ownP σ1  ownG m)  WP e1 @ E {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  rtc step ([e1], σ1) (t2, σ2) 
Ralf Jung's avatar
Ralf Jung committed
116
  e2  t2  (is_Some (to_val e2)  reducible e2 σ2).
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof.
Ralf Jung's avatar
Ralf Jung committed
118
  intros Hv ? Hs [i ?]%elem_of_list_lookup.
Ralf Jung's avatar
Ralf Jung committed
119 120
  destruct (wp_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
  { by rewrite -(wp_mask_weaken E ). }
121 122
  destruct (Forall3_lookup_l (λ e Φ r, wp  e Φ 2 r) t2
    (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
Ralf Jung's avatar
Ralf Jung committed
123
  case He:(to_val e2)=>[v2|]; first by eauto. right.
124
  destruct (wp_step_inv   Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    rewrite ?right_id_L ?big_op_delete; auto.
Ralf Jung's avatar
Ralf Jung committed
126
  by rewrite -wp_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Qed.
Ralf Jung's avatar
Ralf Jung committed
128

Ralf Jung's avatar
Ralf Jung committed
129
(* Connect this up to the threadpool-semantics. *)
Ralf Jung's avatar
Ralf Jung committed
130
Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
131
   m 
132
  (ownP σ1  ownG m)  WP e1 @ E {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135 136 137 138
  rtc step ([e1], σ1) (t2, σ2) 
  Forall (λ e, is_Some (to_val e)) t2   t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
  intros.
  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
Ralf Jung's avatar
Ralf Jung committed
139
  destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as [?|(e3&σ3&ef&?)];
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    rewrite ?eq_None_not_Some; auto.
Ralf Jung's avatar
Ralf Jung committed
141
  { exfalso. eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
145 146 147 148 149 150 151 152 153 154

Lemma ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
   m 
  {{ ownP σ1  ownG m }} e1 @ E {{ Φ }} 
  rtc step ([e1], σ1) (t2, σ2) 
  Forall (λ e, is_Some (to_val e)) t2   t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
  intros ? Hht. eapply wp_adequacy_safe with (E:=E) (Φ:=Φ); first done.
  move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
End adequacy.