Simulation.v 19.6 KB
Newer Older
1
From iris_time.heap_lang Require Import notation proofmode.
2
From iris.program_logic Require Import adequacy.
3

4 5
From iris_time Require Import Misc Reduction Tactics.
From iris_time Require Export Translation.
6 7 8 9 10 11 12 13

Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type  : loc.
Implicit Type m n : nat.
Glen Mével's avatar
Glen Mével committed
14
Implicit Type φ : val  Prop.
15 16 17



Glen Mével's avatar
Glen Mével committed
18 19
(* Our definition of tick will depend on a location. This is made a typeclass
 * so as to be inferred automatically. *)
20 21 22 23
Class TickCounter := { tick_counter : loc }.
Notation "S« σ , n »" := (<[tick_counter := LitV (LitInt n%nat)]> (translationS σ%V)).
(* Notation "« σ , n »" := (<[ := LitV (LitInt n%nat)]> (translationS σ%V)) (only printing). *)
Local Notation  := tick_counter.
24 25


Glen Mével's avatar
Glen Mével committed
26 27
(* This whole file is parameterized by a runtime_error value: *)
Section Simulation.
28 29 30 31 32 33 34 35
Context (runtime_error : val).



(*
 * Definition of tick
 *)

36 37
Local Instance generic_tick {Hloc : TickCounter} : Tick :=
 (rec: "tick" "x" :=
38 39 40 41 42 43
    let: "k" := ! # in
    if: "k"  #0 then
      runtime_error #()
    else if: CAS # "k" ("k" - #1) then
      "x"
    else
44
      "tick" "x")%V.
45 46 47 48 49 50 51 52 53


(*
 * Operational behavior of tick
 *)

Section Tick_exec.

  Context {Hloc : TickCounter}.
54 55 56 57

  Lemma exec_tick_success n v σ :
    prim_exec  (tick v) (<[ := #(S n)]> σ)  v (<[ := #n]> σ)  [].
  Proof.
58
    remember (Z.of_nat (S n)) as Sn.
59
    unlock tick generic_tick.
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
    eapply prim_exec_cons_nofork. (* Initial β-redex *)
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork. (* Load of  *)
    { prim_step; apply lookup_insert. }
    simpl. eapply prim_exec_cons_nofork. (* First redex of let *)
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork. (* Second redex of let *)
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork. (* Comparison ["k"  #0] *)
    { by prim_step. }
    rewrite /= bool_decide_false; [|lia].
    eapply prim_exec_cons_nofork.        (* If *)
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork. (* Decrementing "k" *)
    { by prim_step. }
                                         (* CAS *)
    simpl. eapply (prim_exec_cons_nofork _ _ _ (if: #true then _ else _)).
    { prim_step; [apply lookup_insert|by left]. }
    eapply prim_exec_cons_nofork.        (* If *)
    { by prim_step. }
    replace (Sn - 1) with (Z.of_nat n) by lia.
81 82 83 84
    rewrite insert_insert.
    apply prim_exec_nil.
  Qed.

Glen Mével's avatar
Glen Mével committed
85
  Lemma exec_tick_case_branch e1 v2 σ :
86
    prim_exec  (tick_case_branch (λ: <>, e1) v2)%E  σ ((tick e1) v2) σ  [].
87
  Proof.
Glen Mével's avatar
Glen Mével committed
88
    unfold tick_case_branch ; unlock.
89
    eapply prim_exec_cons_nofork.
90 91 92 93 94 95 96 97 98 99
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork.
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork.
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork.
    { by prim_step. }
    simpl. eapply prim_exec_cons_nofork.
    { by prim_step. }
    apply prim_exec_nil.
100
  Qed.
101 102

End Tick_exec.
103 104 105 106



(*
107
 * Simulation lemma
108 109
 *)

110
Section SimulationLemma.
111

112
  Context {Hloc : TickCounter}.
113 114 115 116

  Local Ltac exec_tick_success :=
    lazymatch goal with
    | |- prim_exec ?e _ _ _ _ =>
117
        reshape_expr false e ltac:(fun K e' =>
118
          eapply prim_exec_fill' with K e' _ ; [ done | done | ] ;
119
          eapply exec_tick_success
120 121
        )
    end ;
122
    done.
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
  (* in this tactic, the parameter afterwards allows to unify the expression
   * resulting from the step before running the tactic prim_step;
   * this matters when the reduction rule to apply is directed by the syntax of
   * the result (more specifically, CasFailS would be picked instead of
   * CasSucS if we did not unify the result with #true beforehand). *)
  Local Ltac tick_then_step_then afterwards :=
    eapply prim_exec_transitive_nofork ; first (
      exec_tick_success
    ) ;
    eapply prim_exec_cons_nofork, afterwards ; first (
      prim_step
    ).
  Local Ltac tick_then_step_then_stop :=
    tick_then_step_then prim_exec_nil.

138
  Lemma simulation_head_step_success n e1 σ1 κ e2 σ2 efs :
139
    σ2 !!  = None 
140
    head_step e1 σ1 κ e2 σ2 efs 
141 142
    prim_exec «e1» S«σ1, S n» «e2» S«σ2, n» T«efs».
  Proof.
143
    intros H Hstep.
144
    destruct Hstep as
145 146 147 148 149 150 151
      [ (* RecS *) f x e σ
      | (* PairS *) v1 v2 σ
      | (* InjLS *) v σ
      | (* InjRS *) v σ
      | (* BetaS *) f x e1 v2 e' σ  ->
      | (* UnOpS *) op v v' σ  Hopeval
      | (* BinOpS *) op v1 v2 v' σ  Hopeval
152 153
      | (* IfTrueS  *) e1 e2 σ
      | (* IfFalseS *) e1 e2 σ
154 155 156 157
      | (* FstS *) v1 v2 σ
      | (* SndS *) v1 v2 σ
      | (* CaseLS *) v0 e1 e2 σ
      | (* CaseRS *) v0 e1 e2 σ
158
      | (* ForkS *) e σ
159
      | (* AllocS *) v σ l  Hfree_l
160
      | (* LoadS *) l v σ  Hbound_l
161 162 163 164 165 166
      | (* StoreS *) l v σ  Hisbound_l
      | (* CasFailS *) l v1 v2 vl σ  Hbound_l Hneq_vl_v1
      | (* CasSucS *) l v1 v2 σ  Hbound_l
      | (* FaaS *) l i1 i2 σ  Hbound_l
      ];
    simpl_trans;
167 168 169 170
    (try (
      assert (  l) as I by (by apply lookup_insert_None in H as [ _ I ]) ;
      rewrite translationS_insert insert_commute ; last exact I
    )).
171 172 173 174 175 176 177 178 179 180 181 182 183 184
    (* RecS f x e σ : *)
    - eapply (prim_exec_cons _ _ _ _ _ [] _ _ []).
      + prim_step.
      + exec_tick_success.
    (* PairS *)
    - tick_then_step_then_stop.
    (* InjLS *)
    - tick_then_step_then_stop.
    (* InjRS *)
    - tick_then_step_then_stop.
    (* BetaS f x e1 v2 e' σ : *)
    - rewrite 2! translation_subst'.
      by tick_then_step_then_stop.
    (* UnOpS op v v' σ : *)
185 186
    - tick_then_step_then_stop.
      by apply un_op_eval_translation.
187
    (* BinOpS op v1 v2 v' σ : *)
188 189 190 191 192 193
    - tick_then_step_then_stop.
      by apply bin_op_eval_translation.
    (* IfTrueS e1 e2 σ : *)
    - tick_then_step_then_stop.
    (* IfFalseS e1 e2 σ : *)
    - tick_then_step_then_stop.
194
    (* FstS v1 v2 σ : *)
195
    - tick_then_step_then_stop.
196
    (* SndS v1 v2 σ : *)
197
    - tick_then_step_then_stop.
198
    (* CaseLS v0 e1 e2 σ : *)
Glen Mével's avatar
Glen Mével committed
199
    - tick_then_step_then exec_tick_case_branch.
200
    (* CaseRS v0 e1 e2 σ : *)
Glen Mével's avatar
Glen Mével committed
201
    - tick_then_step_then exec_tick_case_branch.
202
    (* ForkS e σ : *)
203
    - replace T« [e] » with ([« e »] ++ []) by apply app_nil_r.
204 205 206
      eapply prim_exec_cons.
      + prim_step.
      + exec_tick_success.
207
    (* AllocS v σ l : *)
208 209 210 211 212 213 214
    - tick_then_step_then_stop.
      apply lookup_insert_None ; auto using lookup_translationS_None.
    (* LoadS l v σ : *)
    - tick_then_step_then_stop.
      assert (  l) as I by (intros <- ; rewrite -> H in * ; discriminate).
      rewrite lookup_insert_ne ; last exact I.
      by apply lookup_translationS_Some.
215
    (* StoreS l v σ : *)
216 217 218
    - tick_then_step_then_stop.
      rewrite lookup_insert_ne ; last exact I.
      by apply lookup_translationS_is_Some.
219
    (* CasFailS l v1 v2 vl σ : *)
220 221 222 223 224
    - tick_then_step_then_stop.
      + assert (  l) as I by (intros <- ; rewrite -> H in * ; discriminate).
        rewrite lookup_insert_ne ; last done.
        by apply lookup_translationS_Some.
      + eauto using translationV_injective.
225
      + by apply vals_cas_compare_safe_translationV.
226
    (* CasSucS l v1 v2 σ : *)
227
    - tick_then_step_then_stop.
228 229 230
      + rewrite lookup_insert_ne ; last exact I.
        by apply lookup_translationS_Some.
      + by apply vals_cas_compare_safe_translationV.
231
    (* FaaS l i1 i2 σ : *)
232 233 234 235 236 237
    - tick_then_step_then_stop.
      rewrite lookup_insert_ne ; last exact I.
      change (#i1)%V with V« #i1 ».
      by apply lookup_translationS_Some.
  Qed.

238
  Lemma simulation_prim_step_success n e1 σ1 κ e2 σ2 efs :
239
    σ2 !!  = None 
240
    prim_step e1 σ1 κ e2 σ2 efs 
241 242
    prim_exec «e1» S«σ1, S n» «e2» S«σ2, n» T«efs».
  Proof.
243
    intros H [ K e1' e2' -> -> H ].
244 245 246 247
    rewrite 2! translation_fill.
    by eapply prim_exec_fill, simulation_head_step_success.
  Qed.

248
  Lemma simulation_step_success n t1 σ1 κ t2 σ2 :
249
    σ2 !!  = None 
250 251
    step (t1, σ1) κ (t2, σ2) 
    rtc erased_step (T«t1», S«σ1, S n») (T«t2», S«σ2, n»).
252
  Proof.
253
    intros H Hstep.
254 255 256 257
    destruct Hstep as [ e1 σ1_ e2 σ2_ efs t t' E1 E2 Hprimstep ] ;
    injection E1 as -> <- ;
    injection E2 as -> <-.
    repeat rewrite ? fmap_app ? fmap_cons.
258 259
    by eapply exec_frame_singleton_thread_pool, prim_exec_exec,
       simulation_prim_step_success.
260 261 262 263
  Qed.

  Lemma simulation_exec_success m n t1 σ1 t2 σ2 :
    σ2 !!  = None 
264 265
    nsteps erased_step m (t1, σ1) (t2, σ2) 
    rtc erased_step (T«t1», S«σ1, m+n») (T«t2», S«σ2, n»).
266 267 268
  Proof.
    make_eq (t1, σ1) as config1 E1.
    make_eq (t2, σ2) as config2 E2.
269 270 271 272
    intros H Hnsteps.
    revert t1 σ1 E1 ;
    induction Hnsteps as [ config | m' config1 (t3, σ3) config2 [κ Hstep] Hsteps IHnsteps ] ;
    intros t1 σ1 E1.
273 274 275 276 277 278
    - destruct E2 ; injection E1 as -> ->.
      apply rtc_refl.
    - destruct E2, E1.
      specialize (IHnsteps eq_refl t3 σ3 eq_refl).
      assert (σ3 !!  = None) as H3 by (eapply loc_fresh_in_dom_nsteps ; cycle 1 ; eassumption).
      eapply rtc_transitive.
279
      + eapply simulation_step_success ; cycle -1 ; eassumption.
280 281 282 283 284 285
      + apply IHnsteps.
  Qed.

  Lemma simulation_exec_success' m n t1 σ1 t2 σ2 :
    σ2 !!  = None 
    (m  n)%nat 
286 287
    nsteps erased_step m (t1, σ1) (t2, σ2) 
    rtc erased_step (T«t1», S«σ1, n») (T«t2», S«σ2, n-m»).
288
  Proof.
289
    intros H I.
290 291 292 293 294 295 296
    replace #n with #(m + (n-m))%nat ; last (repeat f_equal ; lia).
    by apply simulation_exec_success.
  Qed.

  (* from a reduction of the translated expression,
   * deduce a reduction of the source expression. *)

297
  (* note: this does not depend on the operational behavior of `tick`. *)
298 299

  Local Ltac exhibit_prim_step e2 :=
300
    eexists _, e2, _, _ ; simpl ; prim_step.
301 302

  Local Ltac eexhibit_prim_step :=
303
    eexists _, _, _, _ ; simpl ; prim_step.
304 305 306 307 308 309 310

  Lemma active_item_translation_reducible ki v σ m :
    ectx_item_is_active ki 
    loc_fresh_in_expr  (fill_item ki v) 
    reducible (fill_item Ki«ki» V«v») S«σ, m» 
    reducible (fill_item ki v) σ.
  Proof.
311 312
    intros Hactive Hfresh (e2' & σ2' & efs &
                           [κ Hheadstep % active_item_prim_step_is_head_step]) ;
313 314 315
      last by apply is_active_translationKi.
    make_eq (fill_item Ki«ki» V«v») as e1' Ee1' ; rewrite Ee1' in Hheadstep.
    make_eq (S«σ, m») as σ1' Eσ1' ; rewrite Eσ1' in Hheadstep.
316 317 318 319 320 321 322 323
    destruct Hheadstep  as
      [ (* RecS *) f x e σ1
      | (* PairS *) v1 v2 σ1
      | (* InjLS *) v1 σ1
      | (* InjRS *) v1 σ1
      | (* BetaS *) f x e1 v2 e' σ1  ->
      | (* UnOpS *) op v1 v' σ1  Hopeval
      | (* BinOpS *) op v1 v2 v' σ1  Hopeval
324 325
      | (* IfTrueS  *) e1 e2 σ1
      | (* IfFalseS *) e1 e2 σ1
326 327 328 329
      | (* FstS *) v1 v2 σ1
      | (* SndS *) v1 v2 σ1
      | (* CaseLS *) v0 e1 e2 σ1
      | (* CaseRS *) v0 e1 e2 σ1
330
      | (* ForkS *) e σ1
331
      | (* AllocS *) v1 σ1 l  Hfree_l
332
      | (* LoadS *) l v1 σ1  Hbound_l
333 334 335 336 337
      | (* StoreS *) l v1 σ1  Hisbound_l
      | (* CasFailS *) l v1 v2 vl σ1  Hbound_l Hneq_vl_v1
      | (* CasSucS *) l v1 v2 σ1  Hbound_l
      | (* FaaS *) l i1 i2 σ1  Hbound_l
      ];
338 339
    destruct ki ; try contradiction Hactive ; try discriminate Ee1' ;
    injection Ee1' ; clear Ee1' ;
340 341
    repeat (intros -> || intros <- || intros -> % translationV_lit_inv || intros E) ;
    destruct Eσ1'.
342 343 344 345 346 347 348
    (* replacing the state S«σ, m» with S«σ»: *)
    all: first [
        apply lookup_insert_None in Hfree_l as [Hfree_l _]
      | apply lookup_insert_Some in Hbound_l as [ [<- _] | [_ Hbound_l] ] ; first naive_solver
      | apply lookup_insert_is_Some in Hisbound_l as [ <- | [_ Hisbound_l] ] ; first naive_solver
      | idtac
    ].
349 350 351 352 353 354
    (* PairS *)
    - eexhibit_prim_step.
    (* InjLS *)
    - eexhibit_prim_step.
    (* InjRS *)
    - eexhibit_prim_step.
355
    (* BetaS *)
356
    - destruct v ; try discriminate E.
357
      by eexhibit_prim_step.
358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
    (* UnOpS *)
    - eexhibit_prim_step.
      by eapply un_op_eval_translation_inv.
    (* BinOpS *)
    - eexhibit_prim_step.
      by eapply bin_op_eval_translation_inv.
    (* IfTrueS *)
    - eexhibit_prim_step.
    (* IfFalseS *)
    - eexhibit_prim_step.
    (* FstS *)
    - destruct v ; try discriminate E.
      eexhibit_prim_step.
    (* SndS *)
    - destruct v ; try discriminate E.
      eexhibit_prim_step.
    (* CaseLS *)
    - destruct v ; try discriminate E.
      eexhibit_prim_step.
    (* CaseRS *)
    - destruct v ; try discriminate E.
      eexhibit_prim_step.
    (* AllocS *)
    - eexhibit_prim_step.
      by eapply lookup_translationS_None_inv.
    (* LoadS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & _).
385
      by eexhibit_prim_step.
386 387 388 389 390
    (* StoreS *)
    - eexhibit_prim_step.
      by eapply lookup_translationS_is_Some_inv.
    (* CasFailS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & ->).
391 392
      exhibit_prim_step (Val #false).
      + done.
393 394
      + intros ? % (f_equal translationV). contradiction.
      + by apply vals_cas_compare_safe_translationV_inv.
395 396
    (* CasSucS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % translationV_injective).
397 398
      exhibit_prim_step (Val #true)%E.
      done. by apply vals_cas_compare_safe_translationV_inv.
399 400
    (* FaaS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % eq_sym % translationV_lit_inv).
401
      by eexhibit_prim_step.
402 403 404
  Qed.

  (* assuming the safety of the translated expression,
405
   * a proof that the original expression is m-safe. *)
406

Glen Mével's avatar
Glen Mével committed
407
  Lemma safe_translation__nsafe_here m e σ :
408 409 410 411 412
    loc_fresh_in_expr  e 
    (m > 0)%nat 
    safe «e» S«σ, m» 
    is_Some (to_val e)  reducible e σ.
  Proof.
413
    intros Hfresh Im Hsafe.
414 415 416 417 418 419 420
    (* case analysis on whether e is a value *)
    destruct (to_val e) as [ v | ] eqn:Hnotval.
    (*  if e is a value, then we get the result immediately: *)
    - left. eauto.
    (*  if e is not a value, then we show that it is reducible: *)
    - right.
      (* we decompose e into a maximal evaluation context K and a head-redex: *)
421 422 423 424 425 426 427 428 429 430 431 432 433 434
      pose proof (not_val_fill_active_item _ Hnotval) as He ; clear Hnotval.
      destruct He as [ (K & x & ->) |
                     [ (K & e1 & ->) |
                     [ (K & f & x & e1 & ->) |
                       (K & ki & v & -> & Hactive) ] ]].
      (*  either e = K[Var x]: *)
      + (* then [«fill K x»] is stuck: *)
        exfalso. clear -Hsafe. rewrite translation_fill in Hsafe.
        apply safe_fill_inv in Hsafe. destruct Hsafe as [_ Hsafe].
        destruct (Hsafe _ _ x eq_refl (rtc_refl _ _)) as
            [[? [=]]|(?&?&?&?&[K' ?? Hx ? Hred])]; first set_solver+; simpl in *.
        destruct (decide (K' = [])) as [->|(K''&Ki&->)%exists_last]; last first.
        { rewrite !fill_app in Hx. by destruct Ki. }
        simpl in Hx. subst e1'. inversion Hred.
435 436
      (*  either e = K[Fork e1]: *)
      + (* then we easily derive a reduction from e: *)
437 438 439 440
        eexists _, _, _, _. apply Ectx_step', ForkS.
      (*  either e = K[Rec f x e1]: *)
      + (* then we easily derive a reduction from e: *)
        eexists _, _, _, _. apply Ectx_step', RecS.
441 442 443 444 445 446 447 448 449 450 451
      (*  or e = K[ki[v]] where ki is an active item: *)
      + (* it is enough to show that ki[v] is reducible: *)
        apply loc_fresh_in_expr_fill_inv in Hfresh ;
        rewrite -> translation_fill in Hsafe ; apply safe_fill_inv in Hsafe ;
        apply reducible_fill ;
        clear K.
        (* we deduce the reducibility of ki[v] from that of «ki»[«v»]: *)
        eapply active_item_translation_reducible ; [ done | done | ].
        (* remind that « ki[v] » = «ki»[tick «v»]: *)
        rewrite -> translation_fill_item_active in Hsafe ; last done.
        (* we have that «ki»[tick «v»] reduces to «ki»[«v»]
452
         * (m  1 so tick can be run): *)
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
        assert (
          prim_exec (fill_item Ki«ki» (tick V«v»)) S«σ, m»
                    (fill_item Ki«ki» V«v»)        S«σ, m-1» []
        ) as Hsteps % prim_exec_exec.
        {
          assert (fill [Ki«ki»] = fill_item Ki«ki») as E by reflexivity ; destruct E.
          apply prim_exec_fill. apply safe_fill_inv in Hsafe.
          rewrite {+1} (_ : m = S (m-1)) ; last lia.
          apply exec_tick_success.
        }
        (* using the safety of «ki»[tick «v»], we proceed by case analysis *)
        eapply Hsafe in Hsteps as [ Hisval | Hred ] ; auto using elem_of_list_here.
        (*  either «ki»[«v»] is a value: this is not possible because ki is active. *)
        * simpl in Hisval. rewrite active_item_not_val in Hisval ;
          [ by apply is_Some_None in Hisval | by apply is_active_translationKi ].
        (*  or «ki»[«v»] reduces to something: this is precisely what we need. *)
        * exact Hred.
  Qed.
Glen Mével's avatar
Glen Mével committed
471
  Lemma safe_translation__nsafe m n e σ t2 σ2 e2 :
472 473 474
    loc_fresh_in_expr  e2 
    σ2 !!  = None 
    safe «e» S«σ, m» 
475
    nsteps erased_step n ([e], σ) (t2, σ2) 
476 477 478 479
    (n < m)%nat 
    e2  t2 
    is_Some (to_val e2)  reducible e2 σ2.
  Proof.
480
    intros He Hℓσ Hsafe Hnsteps Inm He2.
481 482 483 484 485
    assert (safe «e2» S«σ2, m-n») as Hsafe2.
    {
      eapply safe_exec.
      - eapply elem_of_list_fmap_1. eassumption.
      - eassumption.
486
      - change [«e»] with T«[e]». apply simulation_exec_success' ; [ assumption | lia | assumption ].
487 488
    }
    assert (m - n > 0)%nat by lia.
Glen Mével's avatar
Glen Mével committed
489
    by eapply safe_translation__nsafe_here.
490 491 492
  Qed.

  (* assuming the adequacy of the translated expression,
493
   * a proof that the original expression has m-adequate results. *)
494

495 496
  (* FIXME : this is a weaker result than the adequacy result of Iris,
     where the predicate can also speak about the final state. *)
Glen Mével's avatar
Glen Mével committed
497
  Lemma adequate_translation__nadequate_result m n φ e σ t2 σ2 v2 :
498
    σ2 !!  = None 
499
    adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)) 
500
    nsteps erased_step n ([e], σ) (Val v2 :: t2, σ2) 
501 502 503
    (n  m)%nat 
    φ v2.
  Proof.
504
    intros Hfresh Hadq Hnsteps Inm.
505
    assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
506
    replace (φ v2) with ((φ  invtranslationV) (translationV v2))
507
      by (simpl ; by rewrite invtranslationV_translationV).
508
    eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))); first done.
509 510
    simpl. change [«e»%E] with T«[e]».
    replace (Val «v2» :: _) with (T«Val v2 :: t2») by done.
511 512 513
    eapply simulation_exec_success' ; eauto.
  Qed.

514
End SimulationLemma. (* we close the section here as we now want to quantify over all locations *)
515

516
(* now lets combine the two results. *)
517

Glen Mével's avatar
Glen Mével committed
518
Lemma adequate_translation__nadequate m φ e σ :
519
  ( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) 
Glen Mével's avatar
Glen Mével committed
520
  nadequate NotStuck m e σ φ.
521
Proof.
522
  intros Hadq.
523 524 525 526 527 528 529
  split.
  (* (1) adequate result: *)
  - intros n t2 σ2 v2 Hnsteps Inm.
    (* build a location  which is not in the domain of σ2: *)
    pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
    assert (σ2 !!  = None)
      by (simpl ; eapply not_elem_of_dom, is_fresh).
Glen Mével's avatar
Glen Mével committed
530
    by eapply adequate_translation__nadequate_result.
531 532 533 534 535 536 537 538 539
  (* (2) safety: *)
  - intros n t2 σ2 e2 _ Hnsteps Inm He2.
    (* build a location  which is fresh in e2 and in the domain of σ2: *)
    pose (set1 := loc_set_of_expr e2 : gset loc).
    pose (set2 := dom (gset loc) σ2 : gset loc).
    pose (Hloc := Build_TickCounter (fresh (set1  set2)) : TickCounter).
    eassert (  set1  set2) as [H1 H2] % not_elem_of_union
      by (unfold  ; apply is_fresh).
    assert (loc_fresh_in_expr  e2)
540
      by by apply loc_not_in_set_is_fresh_in_expr.
541 542 543
    assert (σ2 !!  = None)
      by by (simpl ; eapply not_elem_of_dom).
    specialize (Hadq Hloc) as Hsafe % safe_adequate.
Glen Mével's avatar
Glen Mével committed
544
    by eapply safe_translation__nsafe.
545 546
Qed.

547
End Simulation.