soundness_binary.v 8.45 KB
Newer Older
1 2 3 4 5 6
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.
7
From iris_logrel.F_mu_ref_par Require Import lang typing rules_binary
8
        rules logrel_binary fundamental_binary context_refinement.
9 10 11 12 13 14 15 16
Require Import iris.program_logic.adequacy.
Import uPred.

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

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 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  Lemma bin_log_related_under_typed_context Γ e e' τ Γ' τ' K :
    ( f, e.[iter (List.length Γ) up f] = e) 
    ( f, e'.[iter (List.length Γ) up f] = 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;
          match goal with
            H : _ |- _ => eapply (typed_context_n_closed _ _ _ _ _ _ _ H)
          end.
      + 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.
      + match goal with
          H : typed_context_item _ _ _ _ _ |- _ => inversion H; subst
        end.
        eapply typed_binary_interp_Case;
          eauto using typed_binary_interp;
          match goal with
            H : _ |- _ => eapply (typed_n_closed _ _ _ H)
          end.
      + match goal with
          H : typed_context_item _ _ _ _ _ |- _ => inversion H; subst
        end.
        eapply typed_binary_interp_Case;
          eauto using typed_binary_interp;
          try match goal with
                H : _ |- _ => eapply (typed_n_closed _ _ _ H)
              end;
          match goal with
            H : _ |- _ => eapply (typed_context_n_closed _ _ _ _ _ _ _ H)
          end.
      + match goal with
          H : typed_context_item _ _ _ _ _ |- _ => inversion H; subst
        end.
        eapply typed_binary_interp_Case;
          eauto using typed_binary_interp;
          try match goal with
                H : _ |- _ => eapply (typed_n_closed _ _ _ H)
              end;
          match goal with
            H : _ |- _ => eapply (typed_context_n_closed _ _ _ _ _ _ _ H)
          end.
      + 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.
      + 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.
        Unshelve. all: trivial.
  Qed.

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 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
  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.

  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.

191 192 193
  Lemma Binary_Soundness Γ e e' τ :
    ( f, e.[iter (List.length Γ) up f] = e) 
    ( f, e'.[iter (List.length Γ) up f] = e') 
194 195
    ( Δ {HΔ : context_interp_Persistent Δ},
        @bin_log_related _ _ _ N Δ Γ e e' τ HΔ) 
196
    context_refines Γ e e' τ.
197
  Proof.
198
    intros H1 K HK htp hp v Hstp Hc Hc'.
199 200 201 202 203
    eapply basic_soundness; eauto.
    eapply bin_log_related_under_typed_context; eauto.
  Qed.

End Soundness.