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

Section adequacy.
10 11 12 13
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types Q : val Λ  iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Transparent uPred_holds.

Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
Lemma wptp_le Qs es rs n n' :
  {n'} (big_op rs)  wptp n es Qs rs  n'  n  wptp n' es Qs rs.
Proof. induction 2; constructor; eauto using uPred_weaken. Qed.
Lemma nsteps_wptp Qs k n tσ1 tσ2 rs1 :
  nsteps step k tσ1 tσ2 
  1 < n  wptp (k + n) (tσ1.1) Qs rs1 
  wsat (k + n) coPset_all (tσ1.2) (big_op rs1) 
   rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2 
             wsat n coPset_all (tσ2.2) (big_op rs2).
Proof.
  intros Hsteps Hn; revert Qs rs1.
  induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
    simplify_equality'; intros Qs rs.
  { by intros; exists rs, []; rewrite right_id_L. }
  intros (Qs1&?&rs1&?&->&->&?&
    (Q&Qs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
  destruct (wp_step_inv coPset_all  Q e1 (k + n) (S (k + n)) σ1 r
    (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'|].
  * destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I])
      (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?).
    { apply Forall3_app, Forall3_cons,
        Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. }
    { by rewrite -Permutation_middle /= (associative (++))
        (commutative (++)) /= associative big_op_app. }
    exists rs', ([λ _, True%I] ++ Qs'); split; auto.
    by rewrite (associative _ _ _ Qs') -(associative _ Qs1).
  * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2  r2' :: rs2)).
    { rewrite /option_list right_id_L.
      apply Forall3_app, Forall3_cons; eauto using wptp_le.
50
      apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56 57
    by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
  {{ P }} e1 @ coPset_all {{ Q }} 
  nsteps step k ([e1],σ1) (t2,σ2) 
  1 < n  wsat (k + n) coPset_all σ1 r1 
  P (k + n) r1 
58
   rs2 Qs', wptp n t2 (Q :: Qs') rs2  wsat n coPset_all σ2 (big_op rs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof.
60 61
  intros Hht ????; apply (nsteps_wptp [Q] k n ([e1],σ1) (t2,σ2) [r1]);
    rewrite /big_op ?right_id; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  constructor; last constructor.
63
  apply Hht with r1 (k + n); eauto using cmra_included_unit.
64
  eapply uPred.const_intro; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Qed.
66 67 68 69
Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
  m 
  {{ ownP σ1  ownG m }} e1 @ coPset_all {{ Q }} 
  rtc step ([e1],σ1) (t2,σ2) 
70
   rs2 Qs', wptp 3 t2 (Q :: Qs') rs2  wsat 3 coPset_all σ2 (big_op rs2).
71
Proof.
72
  intros Hv ? [k ?]%rtc_nsteps.
73
  eapply ht_adequacy_steps with (r1 := (Res  (Excl σ1) (Some m))); eauto; [|].
74
  { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
75
  exists (Res  (Excl σ1) ), (Res   (Some m)); split_ands.
76 77 78
  * by rewrite Res_op ?left_id ?right_id.
  * by rewrite /uPred_holds /=.
  * by apply ownG_spec.
79 80
Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
81
   m 
82
  {{ ownP σ1  ownG m }} e @ E {{ λ v',  φ v' }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85
  rtc step ([e], σ1) (of_val v :: t2, σ2) 
  φ v.
Proof.
86 87 88
  intros Hv ? Hs.
  destruct (ht_adequacy_own (λ v',  φ v')%I e (of_val v :: t2) σ1 m σ2)
             as (rs2&Qs&Hwptp&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90
  { by rewrite -(ht_mask_weaken E coPset_all). }
  inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
91
  apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 3  σ2) as [r' []]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
  by rewrite right_id_L.
Qed.
94
Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
95
   m 
96
  {{ ownP σ1  ownG m }} e1 @ E {{ Q }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99
  rtc step ([e1], σ1) (t2, σ2) 
  e2  t2  to_val e2 = None  reducible e2 σ2.
Proof.
100 101
  intros Hv ? Hs [i ?]%elem_of_list_lookup He.
  destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103
  { by rewrite -(ht_mask_weaken E coPset_all). }
  destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2
104
    (Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107
  destruct (wp_step_inv coPset_all  Q' e2 2 3 σ2 r2 (big_op (delete i rs2)));
    rewrite ?right_id_L ?big_op_delete; auto.
Qed.
108
Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
109
   m 
110
  {{ ownP σ1  ownG m }} e1 @ E {{ Q }} 
Robbert Krebbers's avatar
Robbert Krebbers committed
111 112 113 114 115 116
  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).
117
  destruct (ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119 120 121 122
    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.