logrel_binary.v 16.4 KB
Newer Older
1 2
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
3
From iris.base_logic Require Export big_op invariants.
4
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
5
From iris.algebra Require Import list.
6
From stdpp Require Import tactics.
7 8
Import uPred.

9
(* HACK: move somewhere else *)
10
Ltac auto_equiv :=
11 12 13 14 15 16 17 18 19 20
  (* Deal with "pointwise_relation" *)
  repeat lazymatch goal with
  | |- pointwise_relation _ _ _ _ => intros ?
  end;
  (* Normalize away equalities. *)
  repeat match goal with
  | H : _ {_} _ |-  _ => apply (timeless_iff _ _) in H
  | _ => progress simplify_eq
  end;
  (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
21
  try (f_equiv; fast_done || auto_equiv).
22

23 24 25 26 27 28 29 30 31 32 33 34 35
(* TODO: modify this in coq-stdpp or something *)
(* this is /almost/ [solve_proper_core ltac:(fun _ => auto_equiv)] *)
(* but we do an additional simpl auto [simplify_eq] *)
Ltac solve_proper ::=
  intros;
  repeat lazymatch goal with
  | |- Proper _ _ => intros ???
  | |- (_ ==> _)%signature _ _ => intros ???
  | |- pointwise_relation _ _ _ _ => intros ?
  | |- ?R ?f _ => try let f' := constr:(λ x, f x) in intros ?
  end; simplify_eq/=;
  (solve_proper_unfold + idtac);
  solve [repeat first [eassumption | auto_equiv] ].
36

37 38
Definition logN : namespace := nroot .@ "logN".

39 40
(** interp : is a unary logical relation. *)
Section logrel.
41
  Context `{logrelG Σ}.
42
  Notation D := (prodC valC valC -n> iProp Σ).
43 44 45 46
  Implicit Types τi : D.
  Implicit Types Δ : listC D.
  Implicit Types interp : listC D  D.

47
  Definition interp_expr (E1 E2 : coPset) (τi : listC D -n> D) (Δ : listC D)
48
      (ee : expr * expr) : iProp Σ := ( j K,
49
    j  fill K (ee.2) -
50
    |={E1,E2}=> WP ee.1 {{ v,  v', j  fill K (of_val v')  τi Δ (v, v') }})%I.
51 52 53
  Global Instance interp_expr_ne n E1 E2:
    Proper (dist n ==> dist n ==> (=) ==> dist n) (interp_expr E1 E2).
  Proof. solve_proper. Qed.       
54

55 56
  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ ww,
    ( from_option id (cconst True)%I (Δ !! x) ww)%I.
57
  Solve Obligations with solve_proper.
58 59

  Program Definition interp_unit : listC D -n> D := λne Δ ww,
60
    (ww.1 = UnitV  ww.2 = UnitV)%I.
61
  Solve Obligations with solve_proper_alt.
62

63
  Program Definition interp_nat : listC D -n> D := λne Δ ww,
64 65 66
    ( n : nat, ww.1 = #nv n  ww.2 = #nv n)%I.
  Solve Obligations with solve_proper. 

67
  Program Definition interp_bool : listC D -n> D := λne Δ ww,
68 69
    ( b : bool, ww.1 = #v b  ww.2 = #v b)%I.
  Solve Obligations with solve_proper. 
70 71 72

  Program Definition interp_prod
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
73
    ( vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) 
74
                interp1 Δ vv1  interp2 Δ vv2)%I.
75
  Solve Obligations with solve_proper. 
76 77 78

  Program Definition interp_sum
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
79 80 81
    (( vv, ww = (InjLV (vv.1), InjLV (vv.2))  interp1 Δ vv) 
     ( vv, ww = (InjRV (vv.1), InjRV (vv.2))  interp2 Δ vv))%I.
  Solve Obligations with solve_proper. 
82

83
  Program Definition interp_arrow (E1 E2 : coPset)
84 85 86
          (interp1 interp2 : listC D -n> D) : listC D -n> D :=
    λne Δ ww,
    (  vv, interp1 Δ vv 
87
             interp_expr E1 E2 
88 89
               interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
                          App (of_val (ww.2)) (of_val (vv.2))))%I.
90
  Solve Obligations with solve_proper. 
91

92
  Program Definition interp_forall (E1 E2 : coPset)
93
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
94
    (  τi,
95
          ⌜∀ ww, PersistentP (τi ww) 
96
          interp_expr E1 E2
97
            interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
98 99
  Solve Obligations with solve_proper.

100 101 102 103 104 105
  Program Definition interp_exists
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
    ( vv, ww = (PackV (vv.1), PackV (vv.2)) 
        τi : D, ⌜∀ ww, PersistentP (τi ww)  interp (τi :: Δ) vv)%I.
  Solve Obligations with solve_proper.

106 107
  Program Definition interp_rec1
      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
108
    ( vv, ww = (FoldV (vv.1), FoldV (vv.2))   interp (τi :: Δ) vv)%I.
109 110 111 112
  Solve Obligations with solve_proper.

  Global Instance interp_rec1_contractive
    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
113
  Proof. solve_contractive. Qed.
114

115 116
  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
    fixpoint (interp_rec1 interp Δ).
117
  Next Obligation.
118 119 120
    intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
  Qed.

121
  Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi,
122
    ( vv, ll.1 ↦ᵢ vv.1  ll.2 ↦ₛ vv.2  τi vv)%I.
123 124 125 126
  Solve Obligations with solve_proper.

  Program Definition interp_ref
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
127
    ( ll, ww = (LocV (ll.1), LocV (ll.2)) 
128
           inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
129 130
  Solve Obligations with solve_proper.

131 132 133 134 135 136 137 138 139 140 141 142
  Program Definition interp_singleton (v v' : val) : listC D -n> D :=
    λne Δ ww, ww = (v,v')%I.
  Solve Obligations with solve_proper.       

  Program Definition interp_iref
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
    ( (ll : loc * loc), 
       interp_ref (interp_singleton (LocV (ll.1)) (LocV (ll.2))) Δ ww 
       inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
  Solve Obligations with solve_proper.

  Fixpoint interp (E1 E2 : coPset) (τ : type) : listC D -n> D :=
143 144 145 146
    match τ return _ with
    | TUnit => interp_unit
    | TNat => interp_nat
    | TBool => interp_bool
147 148 149 150
    | TProd τ1 τ2 => interp_prod (interp E1 E2 τ1) (interp E1 E2 τ2)
    | TSum τ1 τ2 => interp_sum (interp E1 E2 τ1) (interp E1 E2 τ2)
    | TArrow τ1 τ2 =>
      interp_arrow   (interp E1 E2 τ1) (interp   τ2)
151
    | TVar x => ctx_lookup x
152 153 154 155
    | TForall τ' => interp_forall   (interp E1 E2 τ')
    | TExists τ' => interp_exists (interp E1 E2 τ')
    | TRec τ' => interp_rec (interp E1 E2 τ')
    | Tref τ' => interp_ref (interp E1 E2 τ')
156
    end.
157
  Notation "⟦ τ ⟧" := (interp   τ).
158

159 160 161 162 163
  Definition interp_env (Γ : stringmap type) (E1 E2 : coPset)
      (Δ : listC D) (vvs : stringmap (val * val)) : iProp Σ :=
    (dom _ Γ = dom _ vvs 
     [ map] x  τvv  (map_zip Γ vvs), interp E1 E2 (fst τvv) Δ (snd τvv))%I.
  Notation "⟦ Γ ⟧*" := (interp_env Γ  ).
164

165 166
  Global Instance interp_persistent τ E1 E2 Δ vv :
    PersistentP (interp E1 E2 τ Δ vv).
167
  Proof.
168
    revert vv Δ; induction τ=> vv Δ; simpl; try apply _.
169
    rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=. eauto.
170
  Qed.
171 172
  Global Instance interp_env_persistent Γ E1 E2 Δ vvs :
    PersistentP (interp_env Γ E1 E2 Δ vvs) := _.
173

174 175 176 177
  (* DF: automate this proof some more *)
  Lemma interp_weaken Δ1 Π Δ2 E1 E2 τ :
    interp E1 E2 (τ.[upn (length Δ1) (ren (+ length Π))]) (Δ1 ++ Π ++ Δ2)
     interp E1 E2 τ (Δ1 ++ Δ2).
178
  Proof.
179
    revert Δ1 Π Δ2 E1 E2. induction τ=> Δ1 Π Δ2 E1 E2; simpl; auto.
180 181
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
182 183
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
184 185
    - apply fixpoint_proper=> τi ww /=.
      properness; auto. apply (IHτ (_ :: _)).
186 187
    - intros ww; simpl; properness; auto.
      rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
188
      { by rewrite !lookup_app_l. }
189
      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia. 
190 191
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
192
    - intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
193 194 195 196
    - intros ww; simpl; properness; auto. by apply IHτ.
  Qed.

  Lemma interp_subst_up Δ1 Δ2 τ τ' :
197 198
    interp   τ (Δ1 ++ interp   τ' Δ2 :: Δ2)
     interp   (τ.[upn (length Δ1) (τ' .: ids)]) (Δ1 ++ Δ2).
199
  Proof.
200 201 202
    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
203 204
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
205 206
    - apply fixpoint_proper=> τi ww /=.
      properness; auto. apply (IHτ (_ :: _)).
207 208
    - intros ww; simpl.
      rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
209 210 211
      { by rewrite !lookup_app_l. }
      rewrite !lookup_app_r; [|lia ..].
      destruct (x - length Δ1) as [|n] eqn:?; simpl.
212
      { symmetry. rewrite always_always. asimpl. apply (interp_weaken [] Δ1 Δ2 _ _ τ'). }
213
      rewrite !lookup_app_r; [|lia ..]. do 4 f_equiv. lia. 
214 215
    - unfold interp_expr.
      intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
216
    - intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
217 218 219
    - intros ww; simpl; properness; auto. by apply IHτ.
  Qed.

220 221
  Lemma interp_subst Δ2 τ τ' :
    interp   τ ((interp   τ' Δ2) :: Δ2)  interp   (τ.[τ'/]) Δ2.
222 223
  Proof. apply (interp_subst_up []). Qed.

224
  Lemma interp_env_dom Δ Γ E1 E2 vvs : interp_env Γ E1 E2 Δ vvs  dom _ Γ = dom _ vvs.
225 226
  Proof. by iIntros "[% ?]". Qed.

227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
  Lemma interp_env_Some_l Δ Γ E1 E2 vvs x τ :
    Γ !! x = Some τ  interp_env Γ E1 E2 Δ vvs   vv, vvs !! x = Some vv  interp E1 E2 τ Δ vv.
  Proof.
    iIntros (Hτ) "[Hdom HΓ]"; iDestruct "Hdom" as %Hdom.
    destruct (elem_of_dom vvs x) as [[v Hv] ].
    { rewrite -Hdom. apply elem_of_dom. by exists τ. }
    assert (map_zip Γ vvs !! x = Some (τ, v)) as Hτv.
    { rewrite map_lookup_zip_with.
      by rewrite Hτ /= Hv /=. }    
    iExists v; iSplit. done.    
    iApply (big_sepM_lookup _ _ _ _ Hτv with "HΓ").
  Qed.

  Lemma interp_env_nil Δ E1 E2 : True  interp_env  E1 E2 Δ .
  Proof.
    iIntros ""; iSplit. 
    - iPureIntro. unfold_leibniz. by rewrite ?dom_empty.
    - rewrite map_zip_with_empty. auto.
  Qed.

  Lemma interp_env_cons (Δ : list D) (Γ : stringmap type)
     (vvs : stringmap (val * val)) E1 E2 (τ : type) (vv : val * val) (x : string) :
    interp E1 E2 τ Δ vv  interp_env Γ E1 E2 Δ vvs 
     interp_env (<[x:=τ]> Γ) E1 E2 Δ (<[x:=vv]> vvs).
251
  Proof.
252 253 254 255 256 257 258 259 260
    iIntros "[Hτ [Hdom HΓ]]". iDestruct "Hdom" as %Hdom. iSplit.
    - iPureIntro. by rewrite !dom_insert_L Hdom. (* TODO: RK: look at why this is so slow *)
    - rewrite -(map_insert_zip_with pair Γ vvs x (τ,vv)); auto.
      rewrite -insert_delete.
      rewrite big_sepM_insert; last by rewrite lookup_delete.
      iFrame "Hτ".
      iApply (big_sepM_mono _ _ (map_zip Γ vvs) with "HΓ").
      { apply delete_subseteq. }
      done.
261 262
  Qed.

263 264 265 266
  Lemma interp_env_cons_bi (Δ : list D) (Γ : stringmap type) (vvs : stringmap (val * val)) E1 E2 (τ : type) (vv : val * val) (x : string) :
    x  dom (gset string) Γ 
    x  dom (gset string) vvs 
    interp_env (<[x:=τ]> Γ) E1 E2 Δ (<[x:=vv]> vvs) ⊣⊢ interp E1 E2 τ Δ vv  interp_env Γ E1 E2 Δ vvs.
267
  Proof.
268
    intros Hx1 Hx2.
269
    rewrite /interp_env /= (assoc _ ( _  _ _)) -(comm _ (_ = _)%I) -assoc.
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
    apply sep_proper; [apply pure_proper|].
    - unfold_leibniz. rewrite ?dom_insert.
      split. 
      + intros Hd y. destruct (Hd y) as [Hd1 Hd2].
        split; intro Hy.
        * destruct (elem_of_union {[x]} (dom (gset string) Γ) y) as [Hy1 Hy2].
          pose (Hy2':=Hd1 (Hy2 (or_intror Hy))).
          destruct (decide (x = y)) as [?|neq]; subst.
          { exfalso. by apply Hx1. }
          apply elem_of_union in Hy2'.
          destruct Hy2' as [F | ?]; auto.
          exfalso. apply neq. symmetry.
          (* what the hell am i even doing here TODO *)
          apply (and_rec (fun x1 _ => x1 F) (elem_of_singleton y x)).
        * destruct (elem_of_union {[x]} (dom (gset string) vvs) y) as [Hy1 Hy2 ].
          pose (Hy2':=Hd2 (Hy2 (or_intror Hy))).
          destruct (decide (x = y)) as [?|neq]; subst.
          { exfalso. by apply Hx2. }
          apply elem_of_union in Hy2'.
          destruct Hy2' as [F | ?]; auto.
          exfalso. apply neq. symmetry.
          apply (and_rec (fun x1 _ => x1 F) (elem_of_singleton y x)).
      + intros Heq. fold_leibniz. by f_equal.
    - rewrite -(map_insert_zip_with _ _ _ _ (τ, vv)); auto.
      rewrite big_sepM_insert /=; auto.
      apply not_elem_of_dom in Hx1.
      apply not_elem_of_dom in Hx2.
      unfold map_zip. erewrite lookup_merge.
      by rewrite Hx1 /=. 
      by compute.
300 301
  Qed.

302 303 304 305
  Lemma interp_env_ren Δ (Γ : stringmap type) E1 E2 (vvs : stringmap (val * val)) (τi : D) :
    interp_env (subst (ren (+1)) <$> Γ) E1 E2 (τi :: Δ) vvs
               ⊣⊢
    interp_env Γ E1 E2 Δ vvs.
306
  Proof.
307 308 309 310 311 312 313 314 315 316 317 318 319
    apply sep_proper; [apply pure_proper|].
    - unfold_leibniz. by rewrite dom_fmap. 
    - rewrite map_zip_with_fmap_1. 
      rewrite map_zip_with_map_zip.
      generalize (map_zip Γ vvs).
      apply map_ind. 
      + rewrite fmap_empty. done.
      + intros i [σ ww] m Hm IH.
        rewrite fmap_insert.
        rewrite ?big_sepM_insert /=; auto; last first.
        { rewrite lookup_fmap. rewrite Hm. done. }
        rewrite IH. apply sep_proper; auto.
        apply (interp_weaken [] [τi] Δ).
320 321
  Qed.

322 323
  Lemma interp_EqType_agree τ v v' E1 E2 Δ :
    EqType τ  interp E1 E2 τ Δ (v, v')  v = v'⌝.
324
  Proof.
325
    intros Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
326
    - by iDestruct "H1" as "[% %]"; subst.
327 328 329
    - by iDestruct "H1" as (n) "[% %]"; subst.
    - by iDestruct "H1" as (b) "[% %]"; subst.
    - iDestruct "H1" as ([??] [??]) "[% [H1 H2]]"; simplify_eq/=.
330
      rewrite IHHτ1 IHHτ2.
331
      by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
332
    - iDestruct "H1" as "[H1|H1]".
333
      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
334
        rewrite IHHτ1. by iDestruct "H1" as "%"; subst.
335
      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
336
        rewrite IHHτ2. by iDestruct "H1" as "%"; subst.
337
  Qed.
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 364 365 366

  (* Observable types are, at the moment, exactly the types which support equality. *)
  Definition ObsType : type  Prop := EqType.

  (* TODO: derive this from [interp_EqType_agree] *)
  (* This formulation is more suitable for proving soundness of the logical relation in [soundness_binary.v] *)
  Lemma interp_ObsType_agree τ :  (v v' : val),
     τ  [] (v, v')  ObsType τ  v = v'⌝.
  Proof.
    induction τ; iIntros (v v') "HI"; simpl; eauto;
      try by (iPureIntro; inversion 1).
    - iDestruct "HI" as "[% %]"; subst; eauto.
    - iDestruct "HI" as (n) "[% %]"; subst; eauto.
    - iDestruct "HI" as (b) "[% %]"; subst; eauto.
    - iDestruct "HI" as ([v1 v1'] [v2 v2']) "/= [% [H1 H2]]".
      simplify_eq/=.
      iDestruct (IHτ1 with "H1") as %IH1.
      iDestruct (IHτ2 with "H2") as %IH2.
      iPureIntro. inversion 1; simplify_eq.
      rewrite IH1; auto.
      by rewrite IH2.
    - iDestruct "HI" as "[HI | HI]";
        iDestruct "HI" as ([w w']) "[% HI]"; simplify_eq/=.
      + iDestruct (IHτ1 with "HI") as %IH1. iPureIntro.
        inversion 1. by rewrite IH1.
      + iDestruct (IHτ2 with "HI") as %IH2. iPureIntro.
       inversion 1. by rewrite IH2.
  Qed.

367
End logrel.
368 369

Typeclasses Opaque interp_env.
370 371
Notation "⟦ τ ⟧" := (interp   τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr    τ ).
372
Notation "⟦ Γ ⟧*" := (interp_env Γ).
373 374

Section bin_log_def.
375
  Context `{logrelG Σ}.
376 377
  Notation D := (prodC valC valC -n> iProp Σ).

378
  Definition bin_log_related_def (E1 E2 : coPset) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := ( Δ (vvs : stringmap (val * val)) ρ,  
379 380 381 382
    spec_ctx ρ -
     interp_env Γ   Δ vvs 
    - interp_expr E1 E2 (interp   τ) Δ
             (env_subst (fst <$> vvs) e, env_subst (snd <$> vvs) e'))%I.
383 384 385 386
  Definition bin_log_related_aux : seal bin_log_related_def. Proof. by eexists. Qed.
  Definition bin_log_related := unseal bin_log_related_aux.
  Definition bin_log_related_eq : bin_log_related = bin_log_related_def :=
    seal_eq bin_log_related_aux.
387 388 389 390 391 392
End bin_log_def.

Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
  (bin_log_related E1 E2 Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level).
Notation "Γ ⊨ e '≤log≤' e' : τ" :=
  (bin_log_related   Γ e e' τ) (at level 74, e, e', τ at next level).