adequacy.v 5.46 KB
Newer Older
1 2
From program_logic Require Export hoare.
From program_logic Require Import wsat ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
4
Local Hint Extern 100 (@eq coPset _ _) => eassumption || 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 12
Context {Λ : language} {Σ : iFunctor}.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Proof. induction 2; constructor; eauto using uPred_weaken. 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
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40
    (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
  { 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
      apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
    by rewrite -Permutation_middle /= big_op_app.
Qed.
57
Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
58
  {{ P }} e1 {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  nsteps step k ([e1],σ1) (t2,σ2) 
60
  1 < n  wsat (k + n)  σ1 r1 
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  P (k + n) r1 
62
   rs2 Φs', wptp n t2 (Φ :: Φs') rs2  wsat n  σ2 (big_op rs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
64
  intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
65
    rewrite /big_op ?right_id; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  constructor; last constructor.
67 68
  move: Hht; rewrite /ht; uPred.unseal=> Hht.
  apply Hht with (k + n) r1; by eauto using cmra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70
Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
71 72
   m 
  {{ ownP σ1  ownG m }} e1 {{ Φ }} 
73
  rtc step ([e1],σ1) (t2,σ2) 
74
   rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2  wsat 2  σ2 (big_op rs2).
75
Proof.
76
  intros Hv ? [k ?]%rtc_nsteps.
77
  eapply ht_adequacy_steps with (r1 := (Res  (Excl σ1) (Some m))); eauto; [|].
78
  { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
79
  uPred.unseal; exists (Res  (Excl σ1) ), (Res   (Some m)); split_and?.
80
  - by rewrite Res_op ?left_id ?right_id.
81
  - rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
82
  - by apply ownG_spec.
83 84
Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
85
   m 
86
  {{ ownP σ1  ownG m }} e @ E {{ λ v',  φ v' }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89
  rtc step ([e], σ1) (of_val v :: t2, σ2) 
  φ v.
Proof.
90 91 92
  intros Hv ? Hs.
  destruct (ht_adequacy_own (λ v',  φ v')%I e (of_val v :: t2) σ1 m σ2)
             as (rs2&Qs&Hwptp&?); auto.
93
  { by rewrite -(ht_mask_weaken E ). }
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
Ralf Jung's avatar
Ralf Jung committed
95 96
  move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp.
  rewrite pvs_eq in Hwp.
97
  destruct (Hwp (big_op rs) 2  σ2) as [r' []]; rewrite ?right_id_L; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
99
Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
100
   m 
101
  {{ ownP σ1  ownG m }} e1 @ E {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104
  rtc step ([e1], σ1) (t2, σ2) 
  e2  t2  to_val e2 = None  reducible e2 σ2.
Proof.
105
  intros Hv ? Hs [i ?]%elem_of_list_lookup He.
106
  destruct (ht_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
107
  { by rewrite -(ht_mask_weaken E ). }
108 109 110
  destruct (Forall3_lookup_l (λ e Φ r, wp  e Φ 2 r) t2
    (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
  destruct (wp_step_inv   Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    rewrite ?right_id_L ?big_op_delete; auto.
Ralf Jung's avatar
Ralf Jung committed
112
  by rewrite -wp_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Qed.
114
Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
115
   m 
116
  {{ ownP σ1  ownG m }} e1 @ E {{ Φ }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118 119 120 121 122
  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).
123
  destruct (ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
Robbert Krebbers's avatar
Robbert Krebbers committed
124 125 126 127 128
    rewrite ?eq_None_not_Some; auto.
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed.
End adequacy.