rel_tactics.v 16.9 KB
Newer Older
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics sel_patterns.
From iris.proofmode Require Export tactics.
4
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary hax.
5 6
From iris_logrel.F_mu_ref_conc Require Export lang logrel_binary relational_properties.
From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics classes.
7 8 9
Set Default Proof Using "Type".
Import lang.

Dan Frumin's avatar
Dan Frumin committed
10
(** General tactics *)
11 12
Ltac rel_reshape_cont_r tac :=
  lazymatch goal with
13
  | |- _  bin_log_related _ _ _ _ _ (fill ?K ?e) _ =>
14 15
    reshape_expr e ltac:(fun K' e' =>
      tac (K' ++ K) e')
16
  | |- _  bin_log_related _ _ _ _ _ ?e _ =>
17 18 19
    reshape_expr e ltac:(fun K' e' => tac K' e')
  end.

20 21
Ltac rel_reshape_cont_l tac :=
  lazymatch goal with
22
  | |- _  bin_log_related _ _ _ _ (fill ?K ?e) _ _ =>
23 24
    reshape_expr e ltac:(fun K' e' =>
      tac (K' ++ K) e')
25
  | |- _  bin_log_related _ _ _ _ ?e _ _ =>
26 27 28
    reshape_expr e ltac:(fun K' e' => tac K' e')
  end.

Dan Frumin's avatar
Dan Frumin committed
29 30 31 32 33 34 35 36 37 38
Ltac rel_bind_ctx_l K :=
  eapply (tac_rel_bind_l _ K);
  [reflexivity || tac_bind_helper
  |].

Ltac rel_bind_ctx_r K :=
  eapply (tac_rel_bind_r _ K);
  [reflexivity || tac_bind_helper
  |].

39
Tactic Notation "rel_vals" :=
Dan Frumin's avatar
Dan Frumin committed
40
  iStartProof;
Dan Frumin's avatar
Dan Frumin committed
41 42 43 44
  iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | simpl ].


Tactic Notation "rel_apply_l" open_constr(lem) :=
Dan Frumin's avatar
Dan Frumin committed
45 46 47 48 49 50 51 52
  (iPoseProofCore lem as false true (fun H =>
    rel_reshape_cont_l ltac:(fun K e =>
      rel_bind_ctx_l K;
      iApplyHyp H;
      try iNext; simpl_subst/=)
    || lazymatch iTypeOf H with
      | Some (_,?P) => fail "rel_apply_l: Cannot apply" P
      end)); tac_rel_done.
Dan Frumin's avatar
Dan Frumin committed
53 54

Tactic Notation "rel_apply_r" open_constr(lem) :=
Dan Frumin's avatar
Dan Frumin committed
55 56 57 58 59 60 61 62
  (iPoseProofCore lem as false true (fun H =>
    rel_reshape_cont_r ltac:(fun K e =>
      rel_bind_ctx_r K;
      iApplyHyp H;
      try iNext; simpl_subst/=)
    || lazymatch iTypeOf H with
      | Some (_,?P) => fail "rel_apply_r: Cannot apply" P
      end)); tac_rel_done.
Dan Frumin's avatar
Dan Frumin committed
63

64
(** Pure reductions *)
Dan Frumin's avatar
Dan Frumin committed
65

Dan Frumin's avatar
Dan Frumin committed
66
Lemma tac_rel_pure_l `{logrelG Σ} K e1  E1 E2 Δ Γ e e2 eres ϕ t τ (b : bool) :
67 68 69 70
  e = fill K e1 
  PureExec ϕ e1 e2 
  ϕ 
  ((b = true  E1 = E2)  b = false) 
Dan Frumin's avatar
Dan Frumin committed
71 72 73
  eres = fill K e2 
  (  ?b bin_log_related E1 E2 Δ Γ eres t τ) 
  (  bin_log_related E1 E2 Δ Γ e t τ).
Dan Frumin's avatar
Dan Frumin committed
74
Proof.
75
  intros Hfill Hpure Hϕ Hb ? Hp. subst.
76 77 78 79 80 81 82 83 84 85
  destruct b.
  - destruct Hb as [[_ ?] | Hb']; last by inversion Hb'. subst.    
    rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ).
    { exact Hp. }
    { apply pure_exec_safe. exact Hϕ. }
    { apply pure_exec_puredet. exact Hϕ. }
  - rewrite -(bin_log_pure_masked_l Δ Γ E1 E2 K e1 e2 t τ).
    { exact Hp. }
    { apply pure_exec_safe. exact Hϕ. }
    { apply pure_exec_puredet. exact Hϕ. }
Dan Frumin's avatar
Dan Frumin committed
86 87
Qed.

88
Tactic Notation "rel_pure_l" open_constr(ef) :=
Dan Frumin's avatar
Dan Frumin committed
89
  iStartProof;
90 91 92 93 94 95 96
  rel_reshape_cont_l ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_l K e');
      [tac_bind_helper             (* e = fill K e1' *)
      |apply _                     (* PureExec ϕ e1 e2 *)
      |try (exact I || reflexivity || tac_rel_done)
      |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
Dan Frumin's avatar
Dan Frumin committed
97
      |simpl; reflexivity       (* eres = fill K e2 *)
98 99 100
      |try iNext; simpl_subst/= (* new goal *)])
  || fail "rel_pure_l: cannot find the reduct".

101
Tactic Notation "rel_rec_l" := rel_pure_l (App (Rec _ _ _) _) || rel_pure_l (App _ _).
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
Tactic Notation "rel_seq_l" := rel_rec_l.
Tactic Notation "rel_let_l" := rel_rec_l.
Tactic Notation "rel_fst_l" := rel_pure_l (Fst (Pair _ _)).
Tactic Notation "rel_snd_l" := rel_pure_l (Snd (Pair _ _)).
Tactic Notation "rel_proj_l" := rel_pure_l (_ (Pair _ _)).
Tactic Notation "rel_unfold_l" := rel_pure_l (Unfold (Fold _)).
Tactic Notation "rel_fold_l" := rel_unfold_l.
Tactic Notation "rel_if_l" := rel_pure_l (If _ _ _).
Tactic Notation "rel_if_true_l" := rel_pure_l (If true _ _).
Tactic Notation "rel_if_false_l" := rel_pure_l (If false _ _).
Tactic Notation "rel_case_inl_l" := rel_pure_l (Case (InjL _) _ _).
Tactic Notation "rel_case_inr_l" := rel_pure_l (Case (InjL _) _ _).
Tactic Notation "rel_case_l" := rel_pure_l (Case _ _ _).
Tactic Notation "rel_op_l" := rel_pure_l (BinOp _ _ _).

Dan Frumin's avatar
Dan Frumin committed
117
Lemma tac_rel_pure_r `{logrelG Σ} K e1  E1 E2 Δ Γ e e2 eres ϕ t τ :
118 119 120 121
  e = fill K e1 
  PureExec ϕ e1 e2 
  ϕ 
  nclose specN  E1 
Dan Frumin's avatar
Dan Frumin committed
122 123 124
  eres = fill K e2 
  (  bin_log_related E1 E2 Δ Γ t (fill K e2) τ) 
  (  bin_log_related E1 E2 Δ Γ t e τ).
125
Proof.
126
  intros Hfill Hpure Hϕ ?? Hp. subst.
127 128
  rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
  { exact Hp. }
Dan Frumin's avatar
Dan Frumin committed
129
  { assumption. }
130 131
  { intros σ.
    destruct Hpure as [Hsafe Hstep].
Dan Frumin's avatar
Dan Frumin committed
132
    destruct (Hsafe Hϕ σ) as [e2' [σ2' [? Hstep']]].
133 134
    destruct (Hstep Hϕ _ _ _ _ Hstep') as (? & ? & ?); subst.
    done. }
135 136
Qed.

137
Tactic Notation "rel_pure_r" open_constr(ef) :=
138
  iStartProof;
139 140 141
  rel_reshape_cont_r ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_r K e');
Dan Frumin's avatar
Dan Frumin committed
142
      [tac_bind_helper             (* e = fill K e1 *)
143
      |apply _                     (* PureExec ϕ e1 e2 *)
Dan Frumin's avatar
Dan Frumin committed
144
      |try (exact I || reflexivity || tac_rel_done)  (* φ *)
145
      |solve_ndisj                 (* specN  E1 *)
Dan Frumin's avatar
Dan Frumin committed
146
      |simpl; reflexivity          (* eres = fill K e2 *)
147
      |simpl_subst/=               (* new goal *)])
148 149
  || fail "rel_pure_r: cannot find the reduct".

150
Tactic Notation "rel_rec_r" := rel_pure_r (App (Rec _ _ _) _) || rel_pure_r (App _ _).
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
Tactic Notation "rel_seq_r" := rel_rec_r.
Tactic Notation "rel_ret_r" := rel_rec_r.
Tactic Notation "rel_fst_r" := rel_pure_r (Fst (Pair _ _)).
Tactic Notation "rel_snd_r" := rel_pure_r (Snd (Pair _ _)).
Tactic Notation "rel_proj_r" := rel_pure_r (_ (Pair _ _)).
Tactic Notation "rel_unfold_r" := rel_pure_r (Unfold (Fold _)).
Tactic Notation "rel_fold_r" := rel_unfold_r.
Tactic Notation "rel_if_r" := rel_pure_r (If _ _ _).
Tactic Notation "rel_if_true_r" := rel_pure_r (If true _ _).
Tactic Notation "rel_if_false_r" := rel_pure_r (If false _ _).
Tactic Notation "rel_case_inl_r" := rel_pure_r (Case (InjL _) _ _).
Tactic Notation "rel_case_inr_r" := rel_pure_r (Case (InjL _) _ _).
Tactic Notation "rel_case_r" := rel_pure_r (Case _ _ _).
Tactic Notation "rel_op_r" := rel_pure_r (BinOp _ _ _).

(** Stateful reductions *)
167

Dan Frumin's avatar
Dan Frumin committed
168 169 170
(* Fork *)
Lemma tac_rel_fork_l `{logrelG Σ}  Δ E1 E2 e' K eres Γ e t τ :
  e = fill K (Fork e') 
171
  Closed  e' 
Dan Frumin's avatar
Dan Frumin committed
172 173 174
  eres = fill K (Lit Unit) 
  (  |={E1,E2}=>  WP e' {{ _ , True }}  bin_log_related E2 E1 Δ Γ eres t τ) 
  (  bin_log_related E1 E1 Δ Γ e t τ).
175
Proof.
Dan Frumin's avatar
Dan Frumin committed
176 177 178
  intros ????.
  subst e eres.
  rewrite -(bin_log_related_fork_l Δ Γ E1 E2); eassumption.
179 180 181 182 183 184
Qed.

Tactic Notation "rel_fork_l" :=
  iStartProof;
  eapply (tac_rel_fork_l);
    [tac_bind_helper || fail "rel_fork_l: cannot find 'fork'"
Dan Frumin's avatar
Dan Frumin committed
185 186
    |solve_closed       (* Closed  e' *)
    |simpl; reflexivity (* eres = fill K () *)
187 188
    |simpl (* new goal *) ].

Dan Frumin's avatar
Dan Frumin committed
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
Lemma tac_rel_fork_r `{logrelG Σ}  Δ E1 E2 e' K Γ e t eres τ :
  nclose specN  E1 
  e = fill K (Fork e') 
  Closed  e' 
  eres = fill K (Lit Unit) 
  (   i, i  e' - bin_log_related E1 E2 Δ Γ t eres τ) 
  (  bin_log_related E1 E2 Δ Γ t e τ).
Proof.
  intros ?????.
  subst e eres.
  rewrite -(bin_log_related_fork_r Δ Γ E1 E2); eassumption.
Qed.

Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
  iStartProof;
  eapply (tac_rel_fork_r);
    [solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_fork_r: cannot find 'fork'"
    |solve_closed         (* Closed  e' *)
    |simpl; reflexivity   (* eres = fill K () *)
    |simpl; iIntros (i) H (* new goal *)].

(* Alloc *)
Dan Frumin's avatar
Dan Frumin committed
212
Tactic Notation "rel_alloc_l_atomic" := rel_apply_l bin_log_related_alloc_l.
213

Dan Frumin's avatar
Dan Frumin committed
214 215 216
Lemma tac_rel_alloc_l_simp `{logrelG Σ} 1 2 E1 Δ Γ e t e' v' K τ :
  e = fill K (Alloc e') 
  IntoLaterNEnvs 1 1 2 
217
  to_val e' = Some v' 
Dan Frumin's avatar
Dan Frumin committed
218 219 220
  (2   l,
     (l ↦ᵢ v' - bin_log_related E1 E1 Δ Γ (fill K (Loc l)) t τ)) 
  (1  bin_log_related E1 E1 Δ Γ e t τ).
221 222 223
Proof.
  intros ???.
  subst e.
Dan Frumin's avatar
Dan Frumin committed
224
  rewrite into_laterN_env_sound /=.
Dan Frumin's avatar
Dan Frumin committed
225
  rewrite -(bin_log_related_alloc_l' Δ Γ E1); eauto.
Dan Frumin's avatar
Dan Frumin committed
226
  apply uPred.later_mono.
227 228 229 230
Qed.

Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
  iStartProof;
Dan Frumin's avatar
Dan Frumin committed
231 232 233 234 235
  eapply tac_rel_alloc_l_simp;
    [tac_bind_helper       (* e = fill K' .. *)
    |apply _               (* IntoLaterNEnvs _ _ _ *)
    |solve_to_val          (* to_val e' = Some v *)
    |iIntros (l) H         (* new goal *)].
236

Dan Frumin's avatar
Dan Frumin committed
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
Lemma tac_rel_alloc_r `{logrelG Σ}  E1 E2 Δ Γ t' v' K' e t τ :
  nclose specN  E1 
  t = fill K' (Alloc t') 
  to_val t' = Some v' 
  (   l, l ↦ₛ v' - bin_log_related E1 E2 Δ Γ e (fill K' (Loc l)) τ) 
  (  bin_log_related E1 E2 Δ Γ e t τ).
Proof.
  intros ????.
  subst t.
  rewrite -(bin_log_related_alloc_r Δ Γ E1 E2); eassumption.
Qed.

Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
  iStartProof;
  eapply (tac_rel_alloc_r);
    [solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
    |solve_to_val (* to_val t' = Some v' *)
    |simpl; iIntros (l) H (* new goal *)].

Tactic Notation "rel_alloc_r" :=
  let l := fresh in
  let H := iFresh "H" in
  rel_alloc_r as l H.

(* Load *)
Dan Frumin's avatar
Dan Frumin committed
263
Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
264

Dan Frumin's avatar
Dan Frumin committed
265 266 267 268 269 270 271
Lemma tac_rel_load_l_simp `{logrelG Σ} 1 2 i1 E1 Δ Γ l v K e t eres τ :
  e = fill K (Load (Loc l)) 
  IntoLaterNEnvs 1 1 2 
  envs_lookup i1 2 = Some (false, l ↦ᵢ v)%I 
  eres = fill K (of_val v) 
  (2  bin_log_related E1 E1 Δ Γ eres t τ) 
  (1  bin_log_related E1 E1 Δ Γ e t τ).
Dan Frumin's avatar
Dan Frumin committed
272
Proof.
Dan Frumin's avatar
Dan Frumin committed
273 274
  intros ???? HΔ2.
  subst e eres.
Dan Frumin's avatar
Dan Frumin committed
275 276 277 278
  rewrite into_laterN_env_sound envs_lookup_split //; simpl.
  rewrite uPred.later_sep.
  rewrite HΔ2.
  apply uPred.wand_elim_l'.
Dan Frumin's avatar
Dan Frumin committed
279
  by rewrite -(bin_log_related_load_l' Δ Γ E1).
Dan Frumin's avatar
Dan Frumin committed
280 281 282 283
Qed.

Tactic Notation "rel_load_l" :=
  iStartProof;
Dan Frumin's avatar
Dan Frumin committed
284
  eapply (tac_rel_load_l_simp);
Dan Frumin's avatar
Dan Frumin committed
285
    [tac_bind_helper (* e = fill K' .. *)
Dan Frumin's avatar
Dan Frumin committed
286 287
    |apply _  (* IntoLaterNenvs _ Δ1 Δ2 *)
    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
Dan Frumin's avatar
Dan Frumin committed
288
    |simpl; reflexivity  (* eres = fill K (of_val v) *)
Dan Frumin's avatar
Dan Frumin committed
289 290
    | (* new goal *)].

Dan Frumin's avatar
Dan Frumin committed
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
Lemma tac_rel_load_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t tres τ v :
  nclose specN  E1 
  t = fill K (Load (Loc l)) 
  envs_lookup i1 1 = Some (false, l ↦ₛ v)%I 
  envs_simple_replace i1 false
    (Esnoc Enil i1 (l ↦ₛ v)%I) 1 = Some 2 
  tres = fill K (of_val v) 
  (2  bin_log_related E1 E2 Δ Γ e tres τ) 
  (1  bin_log_related E1 E2 Δ Γ e t τ).
Proof.
  intros ????? Hg.
  rewrite (envs_simple_replace_sound 1 2 i1) //; simpl.
  rewrite right_id.
  subst t tres.
  rewrite {1}(bin_log_related_load_r Δ Γ E1 E2); [ | eassumption ].
  rewrite Hg.
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_load_r" :=
  iStartProof;
  eapply (tac_rel_load_r);
    [solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper (* e = fill K (Store (Loc l) e') *)
    |iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?"
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
    |simpl; reflexivity  (* tres = fill K (of_val v) *)
    |simpl (* new goal *)].

(* Store *)
Dan Frumin's avatar
Dan Frumin committed
321
Tactic Notation "rel_store_l_atomic" := rel_apply_l bin_log_related_store_l.
322

Dan Frumin's avatar
Dan Frumin committed
323 324
Lemma tac_rel_store_l_simp `{logrelG Σ} 1 2 3 i1 E1 Δ Γ K l v e' v' e t eres τ :
  e = fill K (Store (Loc l) e') 
325
  to_val e' = Some v' 
Dan Frumin's avatar
Dan Frumin committed
326 327 328 329 330 331
  IntoLaterNEnvs 1 1 2 
  envs_lookup i1 2 = Some (false, l ↦ᵢ v)%I 
  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) 2 = Some 3 
  eres = fill K (Lit Unit) 
  (3  bin_log_related E1 E1 Δ Γ eres t τ) 
  (1  bin_log_related E1 E1 Δ Γ e t τ).
332
Proof.
Dan Frumin's avatar
Dan Frumin committed
333 334 335 336
  intros ?????? Hg.
  subst e eres.
  rewrite into_laterN_env_sound envs_simple_replace_sound //; simpl.
  rewrite uPred.later_sep.
337
  rewrite right_id.
Dan Frumin's avatar
Dan Frumin committed
338 339
  rewrite (bin_log_related_store_l' Δ Γ E1). 2: eassumption.
  rewrite Hg.
340 341 342 343 344 345 346
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_store_l" :=
  iStartProof;
  eapply (tac_rel_store_l_simp);
    [tac_bind_helper (* e = fill K' .. *)    
347
    |solve_to_val (* to_val e' = Some v' *)
Dan Frumin's avatar
Dan Frumin committed
348
    |apply _      (* IntoLaterNEnvs *)
349 350
    |iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
Dan Frumin's avatar
Dan Frumin committed
351 352
    |simpl; reflexivity  (* eres = fill K () *)
    |(* new goal *)].
353

Dan Frumin's avatar
Dan Frumin committed
354
Lemma tac_rel_store_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l t' v' e t tres τ v :
355
  nclose specN  E1 
Dan Frumin's avatar
Dan Frumin committed
356
  t = fill K (Store (Loc l) t') 
357
  to_val t' = Some v' 
Dan Frumin's avatar
Dan Frumin committed
358 359 360 361 362
  envs_lookup i1 1 = Some (false, l ↦ₛ v)%I 
  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) 1 = Some 2 
  tres = fill K (Lit Unit) 
  (2  bin_log_related E1 E2 Δ Γ e tres τ) 
  (1  bin_log_related E1 E2 Δ Γ e t τ).
363
Proof.
Dan Frumin's avatar
Dan Frumin committed
364
  intros ?????? Hg.
365 366
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id.
Dan Frumin's avatar
Dan Frumin committed
367 368 369
  subst t tres.
  rewrite (bin_log_related_store_r Δ Γ E1 E2); [ | eassumption..].
  rewrite Hg.
370 371 372 373 374 375 376 377
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_store_r" :=
  iStartProof;
  eapply (tac_rel_store_r);
    [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
378
    |solve_to_val (* to_val e' = Some v *)
Dan Frumin's avatar
Dan Frumin committed
379
    |iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?"
380
    |env_cbv; reflexivity || fail "rel_store_r: this should not happen"
Dan Frumin's avatar
Dan Frumin committed
381
    |simpl; reflexivity  (* tres = fill K () *)
382 383
    |(* new goal *)].

Dan Frumin's avatar
Dan Frumin committed
384 385
(* CAS *)
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
386

Dan Frumin's avatar
Dan Frumin committed
387
Lemma tac_rel_cas_fail_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t e1 e2 v1 v2 tres τ v :
388
  nclose specN  E1 
Dan Frumin's avatar
Dan Frumin committed
389
  t = fill K (CAS (Loc l) e1 e2) 
390 391
  to_val e1 = Some v1 
  to_val e2 = Some v2 
Dan Frumin's avatar
Dan Frumin committed
392
  envs_lookup i1 1 = Some (false, l ↦ₛ v)%I 
393 394
  v  v1 
  envs_simple_replace i1 false 
Dan Frumin's avatar
Dan Frumin committed
395 396 397 398
    (Esnoc Enil i1 (l ↦ₛ v)%I) 1 = Some 2 
  tres = fill K (# false) 
  (2  bin_log_related E1 E2 Δ Γ e tres τ) 
  (1  bin_log_related E1 E2 Δ Γ e t τ).
399
Proof.
Dan Frumin's avatar
Dan Frumin committed
400 401
  intros ???????? Hg.
  rewrite (envs_simple_replace_sound 1 2 i1) //; simpl. 
402
  rewrite right_id.
Dan Frumin's avatar
Dan Frumin committed
403 404 405
  subst t tres.
  rewrite {1}(bin_log_related_cas_fail_r Δ Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
  rewrite Hg.
406 407 408 409 410 411 412 413
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_cas_fail_r" :=
  iStartProof;
  eapply (tac_rel_cas_fail_r);
    [solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_cas_fail_r: cannot find 'CAS ..'"
414 415
    |solve_to_val
    |solve_to_val
416 417 418
    |iAssumptionCore || fail "rel_cas_fail_l: cannot find ? ↦ₛ ?" 
    |try fast_done (* v  v1 *)
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
Dan Frumin's avatar
Dan Frumin committed
419
    |simpl; reflexivity  (* tres = fill K false *)
420 421 422
    |(* new goal *)].


Dan Frumin's avatar
Dan Frumin committed
423
Lemma tac_rel_cas_suc_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t e1 e2 v1 v2 tres τ v :
424
  nclose specN  E1 
Dan Frumin's avatar
Dan Frumin committed
425
  t = fill K (CAS (Loc l) e1 e2) 
426 427
  to_val e1 = Some v1 
  to_val e2 = Some v2 
Dan Frumin's avatar
Dan Frumin committed
428
  envs_lookup i1 1 = Some (false, l ↦ₛ v)%I 
429 430
  v = v1 
  envs_simple_replace i1 false 
Dan Frumin's avatar
Dan Frumin committed
431 432 433 434
    (Esnoc Enil i1 (l ↦ₛ v2)%I) 1 = Some 2 
  tres = fill K (# true) 
  (2  bin_log_related E1 E2 Δ Γ e tres τ) 
  (1  bin_log_related E1 E2 Δ Γ e t τ).
435
Proof.
Dan Frumin's avatar
Dan Frumin committed
436 437
  intros ???????? Hg.
  rewrite (envs_simple_replace_sound 1 2 i1) //; simpl.
438
  rewrite right_id.
Dan Frumin's avatar
Dan Frumin committed
439 440 441
  subst t tres.
  rewrite {1}(bin_log_related_cas_suc_r Δ Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
  rewrite Hg.
442 443 444 445 446 447 448 449
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_cas_suc_r" :=
  iStartProof;
  eapply (tac_rel_cas_suc_r);
    [solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_cas_suc_r: cannot find 'CAS ..'"
450 451
    |solve_to_val
    |solve_to_val
452 453 454
    |iAssumptionCore || fail "rel_cas_suc_l: cannot find ? ↦ₛ ?" 
    |try fast_done (* v = v1 *)
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
Dan Frumin's avatar
Dan Frumin committed
455
    |simpl; reflexivity  (* tres = fill K true *)
456 457
    |(* new goal *)].

458
Section test.
459
  From iris_logrel.F_mu_ref_conc Require Import reflection.
460
  Context `{logrelG Σ}.
461
  
462 463 464 465 466 467 468
  Definition choiceN : namespace := nroot .@ "choice".

  Definition choice_inv y y' : iProp Σ :=
    ( f, y ↦ᵢ (#v f)  y' ↦ₛ (#v f))%I.

  Definition storeFalse : val := λ: "y", "y" <- # false.

Dan Frumin's avatar
Dan Frumin committed
469
  Lemma test_store Γ Δ y y':
470
    inv choiceN (choice_inv y y')
Dan Frumin's avatar
Dan Frumin committed
471
    - {,;Δ;Γ}  (storeFalse (Fst (#y, 3))) log (storeFalse #y') : TUnit.
472 473 474
  Proof.
    iIntros "#Hinv".
    unfold storeFalse. unlock.
475
    rel_fst_l.
476 477 478
    rel_rec_l.
    rel_rec_r.

Dan Frumin's avatar
Dan Frumin committed
479 480 481 482 483
    rel_apply_l bin_log_related_store_l.
    iInv choiceN as (f) ">[Hy Hy']" "Hcl".
    iExists _. iFrame "Hy".
    iModIntro. iNext. iIntros "Hy".
    rel_store_r. simpl.
484 485 486 487

    iMod ("Hcl" with "[Hy Hy']").
    { iNext. iExists _. iFrame. }

Dan Frumin's avatar
Dan Frumin committed
488 489

    rel_vals; eauto.
490 491 492
  Qed.

End test.