soundness_binary.v 14.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
Require Import Coq.Logic.Eqdep_dec.
Require Import iris.proofmode.invariants iris.proofmode.weakestpre
        iris.proofmode.tactics.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.auth iris.algebra.dec_agree iris.algebra.frac
        iris.algebra.upred_big_op.
Require Import F_mu_ref_par.lang F_mu_ref_par.typing F_mu_ref_par.rules_binary
        F_mu_ref_par.rules F_mu_ref_par.logrel_binary
        F_mu_ref_par.fundamental_binary.
Require Import iris.program_logic.adequacy.
Import uPred.

Inductive context_item : Type :=
| CTX_Lam
| CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr)
(* Products *)
| CTX_PairL (e2 : expr)
| CTX_PairR (e1 : expr)
| CTX_Fst
| CTX_Snd
(* Sums *)
| CTX_InjL
| CTX_InjR
| CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
29 30 31 32 33 34 35
(* Nat bin op *)
| CTX_NBOPL (op : NatBinOP) (e2 : expr)
| CTX_NBOPR (op : NatBinOP) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Concurrency *)
| CTX_Fork
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare and swap used for fine-grained concurrency *)
| CTX_CAS_L (e1 : expr) (e2 : expr)
| CTX_CAS_M (e0 : expr) (e2 : expr)
| CTX_CAS_R (e0 : expr) (e1 : expr).

Fixpoint fill_ctx_item (ctx : context_item) (e : expr) : expr :=
  match ctx with
  | CTX_Lam => Lam e
  | CTX_AppL e2 => App e e2
  | CTX_AppR e1 => App e1 e
  | CTX_PairL e2 => Pair e e2
  | CTX_PairR e1 => Pair e1 e
  | CTX_Fst => Fst e
  | CTX_Snd => Snd e
  | CTX_InjL => InjL e
  | CTX_InjR => InjR e
  | CTX_CaseL e1 e2 => Case e e1 e2
  | CTX_CaseM e0 e2 => Case e0 e e2
  | CTX_CaseR e0 e1 => Case e0 e1 e
68 69 70 71 72
  | CTX_NBOPL op e2 => NBOP op e e2
  | CTX_NBOPR op e1 => NBOP op e1 e
  | CTX_IfL e1 e2 => If e e1 e2
  | CTX_IfM e0 e2 => If e0 e e2
  | CTX_IfR e0 e1 => If e0 e1 e
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
  | CTX_Fold => Fold e
  | CTX_Unfold => Unfold e
  | CTX_TLam => TLam e
  | CTX_TApp => TApp e
  | CTX_Fork => Fork e
  | CTX_Alloc => Alloc e
  | CTX_Load => Load e
  | CTX_StoreL e2 => Store e e2
  | CTX_StoreR e1 => Store e1 e
  | CTX_CAS_L e1 e2 => CAS e e1 e2
  | CTX_CAS_M e0 e2 => CAS e0 e e2
  | CTX_CAS_R e0 e1 => CAS e0 e1 e
  end.

Definition context := list context_item.

Definition fill_ctx K e := foldr fill_ctx_item e K.

Local Open Scope bin_logrel_scope.

(** typed context *)
Inductive typed_context_item :
  context_item  (list type)  type  (list type)  type  Prop :=
| TP_CTX_Lam :  Γ τ τ',
97
    typed_context_item CTX_Lam (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
| TP_CTX_AppL (e2 : expr) :  Γ τ τ',
    typed Γ e2 τ 
    typed_context_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
| TP_CTX_AppR (e1 : expr) :  Γ τ τ',
    typed Γ e1 (TArrow τ τ') 
    typed_context_item (CTX_AppR e1) Γ τ Γ τ'
| TP_CTX_PairL (e2 : expr) :  Γ τ τ',
    typed Γ e2 τ' 
    typed_context_item (CTX_PairL e2) Γ τ Γ (TProd τ τ')
| TP_CTX_PairR (e1 : expr) :  Γ τ τ',
    typed Γ e1 τ 
    typed_context_item (CTX_PairR e1) Γ τ' Γ (TProd τ τ')
| TP_CTX_Fst :  Γ τ τ',
    typed_context_item CTX_Fst Γ (TProd τ τ') Γ τ
| TP_CTX_Snd :  Γ τ τ',
    typed_context_item CTX_Snd Γ (TProd τ τ') Γ τ'
| TP_CTX_InjL :  Γ τ τ',
    typed_context_item CTX_InjL Γ τ Γ (TSum τ τ')
| TP_CTX_InjR :  Γ τ τ',
    typed_context_item CTX_InjR Γ τ' Γ (TSum τ τ')
| TP_CTX_CaseL (e1 : expr) (e2 : expr) :  Γ τ1 τ2 τ',
    typed (τ1 :: Γ) e1 τ'  typed (τ2 :: Γ) e2 τ' 
    typed_context_item (CTX_CaseL e1 e2) Γ (TSum τ1 τ2) Γ τ'
| TP_CTX_CaseM (e0 : expr) (e2 : expr) :  Γ τ1 τ2 τ',
    typed Γ e0 (TSum τ1 τ2)  typed (τ2 :: Γ) e2 τ' 
    typed_context_item (CTX_CaseM e0 e2) (τ1 :: Γ) τ' Γ τ'
| TP_CTX_CaseR (e0 : expr) (e1 : expr) :  Γ τ1 τ2 τ',
    typed Γ e0 (TSum τ1 τ2)  typed (τ1 :: Γ) e1 τ' 
    typed_context_item (CTX_CaseR e0 e1) (τ2 :: Γ) τ' Γ τ'
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
| TP_CTX_IfL (e1 : expr) (e2 : expr) :  Γ τ,
    typed Γ e1 τ  typed Γ e2 τ 
    typed_context_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
| TP_CTX_IfM (e0 : expr) (e2 : expr) :  Γ τ,
    typed Γ e0 (TBool)  typed Γ e2 τ 
    typed_context_item (CTX_IfM e0 e2) Γ τ Γ τ
| TP_CTX_IfR (e0 : expr) (e1 : expr) :  Γ τ,
    typed Γ e0 (TBool)  typed Γ e1 τ 
    typed_context_item (CTX_IfR e0 e1) Γ τ Γ τ
| TP_CTX_NBOPL op (e2 : expr) :  Γ,
    typed Γ e2 TNat 
    typed_context_item (CTX_NBOPL op e2) Γ TNat Γ (NatBinOP_res_type op)
| TP_CTX_NBOPR op (e1 : expr) :  Γ,
    typed Γ e1 TNat 
    typed_context_item (CTX_NBOPR op e1) Γ TNat Γ (NatBinOP_res_type op)
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
| TP_CTX_Fold :  Γ τ,
    typed_context_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold :  Γ τ,
    typed_context_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam :  Γ τ,
    typed_context_item
      CTX_TLam (map (λ t : type, t.[ren (+1)]) Γ) τ Γ (TForall τ)
| TP_CTX_TApp :  Γ τ τ',
    typed_context_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
| TP_CTX_Fork :  Γ,
    typed_context_item CTX_Fork Γ TUnit Γ TUnit
| TPCTX_Alloc :  Γ τ,
    typed_context_item CTX_Alloc Γ τ Γ (Tref τ)
| TP_CTX_Load :  Γ τ,
    typed_context_item CTX_Load Γ (Tref τ) Γ τ
| TP_CTX_StoreL (e2 : expr) :  Γ τ,
    typed Γ e2 τ 
    typed_context_item (CTX_StoreL e2) Γ (Tref τ) Γ TUnit
| TP_CTX_StoreR (e1 : expr) :  Γ τ,
    typed Γ e1 (Tref τ) 
    typed_context_item (CTX_StoreR e1) Γ τ Γ TUnit
| TP_CTX_CasL (e1 : expr)  (e2 : expr) :  Γ τ,
    EqType τ  typed Γ e1 τ  typed Γ e2 τ 
165
    typed_context_item (CTX_CAS_L e1 e2) Γ (Tref τ) Γ TBool
166 167
| TP_CTX_CasM (e0 : expr) (e2 : expr) :  Γ τ,
    EqType τ  typed Γ e0 (Tref τ)  typed Γ e2 τ 
168
    typed_context_item (CTX_CAS_M e0 e2) Γ τ Γ TBool
169 170
| TP_CTX_CasR (e0 : expr) (e1 : expr) :  Γ τ,
    EqType τ  typed Γ e0 (Tref τ)  typed Γ e1 τ 
171
    typed_context_item (CTX_CAS_R e0 e1) Γ τ Γ TBool.
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327

Lemma typed_context_item_typed k Γ τ Γ' τ' e :
  typed Γ e τ  typed_context_item k Γ τ Γ' τ' 
  typed Γ' (fill_ctx_item k e) τ'.
Proof. intros H1 H2; induction H2; simpl; eauto using typed. Qed.

Inductive typed_context :
  context  (list type)  type  (list type)  type  Prop :=
| TPCTX_nil :  Γ τ, typed_context nil Γ τ Γ τ
| TPCTX_cons :  Γ1 τ1 Γ2 τ2 Γ3 τ3 k K,
    typed_context_item k Γ2 τ2 Γ3 τ3 
    typed_context K Γ1 τ1 Γ2 τ2 
    typed_context (k :: K) Γ1 τ1 Γ3 τ3.

Lemma typed_context_typed K Γ τ Γ' τ' e :
  typed Γ e τ  typed_context K Γ τ Γ' τ'  typed Γ' (fill_ctx K e) τ'.
Proof.
  intros H1 H2; induction H2; simpl; eauto using typed_context_item_typed.
Qed.

Definition context_refines Γ e e' τ (He : typed Γ e τ) (He' : typed Γ e' τ) :=
   K,
    typed_context K Γ τ [] TUnit 
     thp h v, rtc step ([fill_ctx K e], ) ((# v) :: thp, h) 
                thp' h' v',
                 rtc step ([fill_ctx K e'], ) ((# v') :: thp', h').

Section Soundness.
  Context {Σ : gFunctors}
          {iI : heapIG Σ} {iS : cfgSG Σ}
          {N : namespace}.

  Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ :=
    {| cofe_mor_car := λ x, {| cofe_mor_car := λ y, (True)%I |} |}.

  Local Notation Δφ := free_type_context.

  Global Instance free_context_interp_Persistent : context_interp_Persistent Δφ.
  Proof. intros x v; apply const_persistent. Qed.

  Lemma wp_basic_soundness e e' τ :
    @bin_log_related _ _ _ N Δφ [] e e' τ _ 
    ((heapI_ctx (N .@ 2)  Spec_ctx (N .@ 3) (to_cfg ([e'], ))  0  e')%I)
       WP e {{_,  ( thp' h v, rtc step ([e'], ) ((# v) :: thp', h))}}.
  Proof.
    intros H1.
    specialize (H1 [] Logic.eq_refl (to_cfg ([e'], )) 0 []); simpl in H1.
    rewrite ?empty_env_subst in H1.
    iIntros "[#Hheap [#Hspec Hj]]".
    iApply wp_pvs.
    iApply wp_wand_l; iSplitR; [|iApply H1; iFrame "Hheap Hspec Hj"; trivial].
    iIntros {v} "H". iDestruct "H" as {v'} "[Hj _]".
    unfold Spec_ctx, auth.auth_ctx, auth.auth_inv, Spec_inv, tpool_mapsto,
    auth.auth_own.
    iInv> (N .@ 3) as {ρ} "[Hown %]".
    iCombine "Hj" "Hown" as "Hown".
    iDestruct (own_valid _ with "Hown !") as "Hvalid".
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]";
      simpl; iClear "Hvalid".
    iDestruct "Ha'" as {ρ'} "Ha'"; iDestruct "Ha'" as %Ha'.
    rewrite ->(right_id _ _) in Ha'; setoid_subst.
    iPvsIntro; iSplitL.
    - iExists _. rewrite own_op. iDestruct "Hown" as "[Ho1 Ho2]".
      iSplitL; trivial.
    - iApply const_intro; eauto.
      rewrite from_to_cfg in H.
      destruct ρ' as [th hp]; unfold op, cmra_op in *; simpl in *.
      unfold prod_op, of_cfg in *; simpl in *.
      destruct th as [|r th]; simpl in *; eauto.
      destruct H0 as [Hx1 Hx2]. simpl in *.
      destruct r as [q r|]; simpl in *; eauto.
      inversion Hx1 as [|? ? Hx]; subst.
      apply frac_valid_inv_l in Hx. inversion Hx.
  Qed.

  Lemma of_empty_heap : of_heap  = .
  Proof. unfold of_heap; apply map_eq => i; rewrite !lookup_omap; f_equal. Qed.

  Local Arguments of_heap : simpl never.

  Lemma basic_soundness e e' τ :
    @bin_log_related _ _ _ N Δφ [] e e' τ _ 
     v thp hp,
      rtc step ([e], ) ((# v) :: thp, hp) 
      ( thp' hp' v', rtc step ([e'], ) ((# v') :: thp', hp')).
  Proof.
    rewrite -of_empty_heap.
    intros H1 v thp hp H2.
    match goal with
      |- ?A =>
      eapply (@wp_adequacy_result
                lang _  (λ _, A) e v thp (of_heap )
                (to_globalF heapI_name ( ( : heapR))
                             to_globalF cfg_name
                            ( ({[ 0 := Frac 1 (DecAgree e') ]},
                                 : heapR) 
                             ({[ 0 := Frac 1 (DecAgree e') ]},
                                 : heapR))
                ) hp); eauto
    end.
    - admit.
    - iIntros "[Hp Hg]".
      rewrite ownership.ownG_op.
      repeat
        match goal with
          |- context [ (ownership.ownG (to_globalF ?gn ?A))] =>
          change (ownership.ownG (to_globalF gn A)) with
          (ghost_ownership.own gn A)
        end.
      rewrite own_op.
      iDestruct "Hg" as "[Hg1 [Hg2 Hg3]]".
      iPvs (inv_alloc (N .@ 2) _ (auth.auth_inv heapI_name heapI_inv)
            with "[Hg1 Hp]") as "#Hheap"; auto.
      + iNext. iExists _; iFrame "Hp". unfold ghost_ownership.own; trivial.
      + rewrite of_empty_heap.
        iPvs (inv_alloc (N .@ 3) _ (auth.auth_inv cfg_name
                                                  (Spec_inv (to_cfg ([e'], ))))
            with "[Hg3]") as "#Hspec"; auto.
        * iNext. iExists _. iFrame "Hg3".
          iApply const_intro; eauto.
          rewrite from_to_cfg.
          unfold of_cfg; simpl; rewrite of_empty_heap; constructor.
        * iApply wp_basic_soundness; eauto.
          unfold heapI_ctx, Spec_ctx, auth.auth_ctx, tpool_mapsto,
          auth.auth_own. iFrame "Hheap Hspec Hg2"; trivial.
  Admitted.

  Lemma bin_log_related_under_typed_context Γ e e' τ Γ' τ' K :
    typed Γ e τ  typed Γ e' τ 
    typed_context K Γ τ Γ' τ' 
    ( Δ {HΔ : context_interp_Persistent Δ},
        @bin_log_related _ _ _ N Δ Γ e e' τ HΔ) 
     Δ {HΔ : context_interp_Persistent Δ},
      @bin_log_related _ _ _ N Δ Γ' (fill_ctx K e) (fill_ctx K e') τ' HΔ.
  Proof.
    revert Γ τ Γ' τ' e e'.
    induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl.
    - inversion_clear 1; trivial.
    - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3 Δ HΔ.
      specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3).
      inversion Hx1; subst; simpl.
      + eapply typed_binary_interp_Lam; eauto using typed_context_typed.
      + eapply typed_binary_interp_App; eauto using typed_binary_interp.
      + eapply typed_binary_interp_App; eauto using typed_binary_interp.
      + eapply typed_binary_interp_Pair; eauto using typed_binary_interp.
      + eapply typed_binary_interp_Pair; eauto using typed_binary_interp.
      + eapply typed_binary_interp_Fst; eauto.
      + eapply typed_binary_interp_Snd; eauto.
      + eapply typed_binary_interp_InjL; eauto.
      + eapply typed_binary_interp_InjR; eauto.
      + eapply typed_binary_interp_Case;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_Case;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_Case;
          eauto using typed_context_typed, typed_binary_interp.
328 329 330 331 332 333 334 335 336 337
      + eapply typed_binary_interp_If;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_If;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_If;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_nat_bin_op;
          eauto using typed_context_typed, typed_binary_interp.
      + eapply typed_binary_interp_nat_bin_op;
          eauto using typed_context_typed, typed_binary_interp.
338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
      + eapply typed_binary_interp_Fold; eauto.
      + eapply typed_binary_interp_Unfold; eauto.
      + eapply typed_binary_interp_TLam; eauto.
      + eapply typed_binary_interp_TApp; trivial.
      + eapply typed_binary_interp_Fork; trivial.
      + eapply typed_binary_interp_Alloc; trivial.
      + eapply typed_binary_interp_Load; trivial.
      + eapply typed_binary_interp_Store; eauto using typed_binary_interp.
      + eapply typed_binary_interp_Store; eauto using typed_binary_interp.
      + eapply typed_binary_interp_CAS; eauto using typed_binary_interp.
      + eapply typed_binary_interp_CAS; eauto using typed_binary_interp.
      + eapply typed_binary_interp_CAS; eauto using typed_binary_interp.
  Qed.

  Lemma Binary_Soundness Γ e e' τ
        (He : typed Γ e τ) (He' : typed Γ e' τ) :
    ( Δ {HΔ : context_interp_Persistent Δ},
        @bin_log_related _ _ _ N Δ Γ e e' τ HΔ) 
    context_refines Γ e e' τ He He'.
  Proof.
    intros H1 K HK htp hp v Hstp.
    eapply basic_soundness; eauto.
    eapply bin_log_related_under_typed_context; eauto.
  Qed.

End Soundness.