Simulation.v 21.7 KB
Newer Older
1
From iris.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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
Context (runtime_error : val).



(*
 * Definition of tick
 *)

Definition tick {Hloc : TickCounter} : val :=
  rec: "tick" "x" :=
    let: "k" := ! # in
    if: "k"  #0 then
      runtime_error #()
    else if: CAS # "k" ("k" - #1) then
      "x"
    else
      "tick" "x".

Local Instance Tick_tick (Hloc: TickCounter) : Tick :=
  {| Translation.tick := tick |}.



(*
 * Operational behavior of tick
 *)

Section Tick_exec.

  Context {Hloc : TickCounter}.
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73

  Lemma exec_tick_success n v σ :
    prim_exec  (tick v) (<[ := #(S n)]> σ)  v (<[ := #n]> σ)  [].
  Proof.
    unlock tick.
    apply prim_exec_cons_nofork
    with (
      let: "k" := ! # in
      if: "k"  #0 then
        runtime_error #()
      else if: CAS # "k" ("k" - #1) then
        v
      else
        tick v
    )%E  (<[ := #(S n)]> σ).
    {
74 75
      prim_step ; first exact _. simpl_subst. repeat f_equal.
      unfold tick. by unlock. }
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
    apply prim_exec_cons_nofork
    with (
      let: "k" := #(S n) in
      if: "k"  #0 then
        runtime_error #()
      else if: CAS # "k" ("k" - #1) then
        v
      else
        tick v
    )%E  (<[ := #(S n)]> σ).
    {
      prim_step.
      apply lookup_insert.
    }
    apply prim_exec_cons_nofork
    with (
      if: #(S n)  #0 then
        runtime_error #()
      else if: CAS # #(S n) (#(S n) - #1) then
        v
      else
        tick v
    )%E  (<[ := #(S n)]> σ).
    {
100
      prim_step ; first exact _. by simpl_subst.
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
    }
    apply prim_exec_cons_nofork
    with (
      if: #false then
        runtime_error #()
      else if: CAS # #(S n) (#(S n) - #1) then
        v
      else
        tick v
    )%E  (<[ := #(S n)]> σ).
    {
      prim_step.
    }
    apply prim_exec_cons_nofork
    with  (if: CAS # #(S n) (#(S n) - #1) then v else tick v)%E  (<[ := #(S n)]> σ).
    {
      prim_step.
    }
    apply prim_exec_cons_nofork
    with  (if: CAS # #(S n) (#(S n - 1)) then v else tick v)%E  (<[ := #(S n)]> σ).
    {
      prim_step.
    }
    apply prim_exec_cons_nofork
    with  (if: #true then v else tick v)%E  (<[ := #(S n - 1)]> (<[ := #(S n)]> σ)).
    {
127
      prim_step; [apply lookup_insert|auto].
128 129 130 131 132 133 134 135 136 137 138
    }
    replace (S n - 1) with (Z.of_nat n) by lia.
    rewrite insert_insert.
    apply prim_exec_cons_nofork
    with  v  (<[ := #n]> σ).
    {
      prim_step.
    }
    apply prim_exec_nil.
  Qed.

Glen Mével's avatar
Glen Mével committed
139
  Lemma exec_tick_case_branch e1 v2 σ :
140
    is_closed [] e1 
141
    prim_exec  (tick_case_branch (λ: <>, e1) v2)%E  σ ((tick e1) v2) σ  [].
142 143
  Proof.
    intros ; assert (Closed [] e1) by exact.
Glen Mével's avatar
Glen Mével committed
144
    unfold tick_case_branch ; unlock.
145 146 147 148 149 150
    eapply prim_exec_cons_nofork.
    {
      prim_step.
      - rewrite /= decide_left //.
      - exact _.
    }
151
    simpl_subst.
152 153
    eapply prim_exec_cons_nofork.
    {
154
      prim_step. exact _.
155
    }
156 157
    simpl_subst.
    eapply prim_exec_cons_nofork, prim_exec_nil.
158
    {
159
      prim_step.
160 161
    }
  Qed.
162 163

End Tick_exec.
164 165 166 167



(*
168
 * Simulation lemma
169 170
 *)

171
Section SimulationLemma.
172

173
  Context {Hloc : TickCounter}.
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

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

  Lemma exec_tick_success' n e v σ :
    to_val e = Some v 
    prim_exec  (tick e) (<[ := #(S n)]> σ)  e (<[ := #n]> σ)  [].
  Proof.
    intros <- % of_to_val. eapply exec_tick_success.
  Qed.

  Local Ltac exec_tick_success :=
    lazymatch goal with
    | |- prim_exec ?e _ _ _ _ =>
        reshape_expr e ltac:(fun K e' =>
          eapply prim_exec_fill' with K e' _ ; [ done | done | ] ;
          eapply exec_tick_success'
        )
    end ;
    by simpl_to_of_val.
  (* 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.

  Lemma simulation_head_step_success n e1 σ1 e2 σ2 efs :
    σ2 !!  = None 
    is_closed [] e1 
    head_step e1 σ1 e2 σ2 efs 
    prim_exec «e1» S«σ1, S n» «e2» S«σ2, n» T«efs».
  Proof.
    intros H Hclosed Hstep.
    destruct Hstep as
      [ (* BetaS *) f x e1 e2 v2 e' σ  Hval_e2 Hclosed_e1 ->
      | (* UnOpS *) op e v v' σ  Hval_e Hopeval
      | (* BinOpS *) op e1 e2 v1 v2 v' σ  Hval_e1 Hval_e2 Hopeval
      | (* IfTrueS  *) e1 e2 σ
      | (* IfFalseS *) e1 e2 σ
      | (* FstS *) e1 v1 e2 v2 σ  Hval_e1 Hval_e2
      | (* SndS *) e1 v1 e2 v2 σ  Hval_e1 Hval_e2
      | (* CaseLS *) e0 v0 e1 e2 σ  Hval_e0
      | (* CaseRS *) e0 v0 e1 e2 σ  Hval_e0
      | (* ForkS *) e σ
      | (* AllocS *) e v σ l  Hval_e Hfree_l
      | (* LoadS *) l v σ  Hbound_l
      | (* StoreS *) l e v σ  Hval_e Hisbound_l
      | (* CasFailS *) l e1 v1 e2 v2 vl σ  Hval_e1 Hval_e2 Hbound_l Hneq_vl_v1
      | (* CasSucS *) l e1 v1 e2 v2 σ  Hval_e1 Hval_e2 Hbound_l
      | (* FaaS *) l i1 e2 i2 σ  Hval_e2 Hbound_l
      ] ;
    cbn [translation fmap list_fmap] ;
    rewrite_into_values ; rewrite ? translation_of_val ;
    (try (
      assert (  l) as I by (by apply lookup_insert_None in H as [ _ I ]) ;
      rewrite translationS_insert insert_commute ; last exact I
    )).
    (* BetaS f x e1 e2 v2 e' σ : *)
    - assert (Closed (f :b: x :b: []) « e1 ») by by apply is_closed_translation.
      rewrite 2! translation_subst' translation_of_val.
243 244 245 246 247 248
      replace (rec: f x := « e1 »)%E with (of_val (rec: f x := « e1 »)%V)
        by by unlock.
      (* FIXME : tick_then_step_then_stop does not work here. *)
      eapply prim_exec_transitive_nofork. exec_tick_success.
      eapply prim_exec_cons_nofork, prim_exec_nil.
      simpl. unlock. prim_step.
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
    (* UnOpS op e v v' σ : *)
    - tick_then_step_then_stop.
      by apply un_op_eval_translation.
    (* BinOpS op e1 e2 v1 v2 v' σ : *)
    - 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.
    (* FstS e1 v1 e2 v2 σ : *)
    - tick_then_step_then_stop.
    (* SndS e1 v1 e2 v2 σ : *)
    - tick_then_step_then_stop.
    (* CaseLS e0 v0 e1 e2 σ : *)
Glen Mével's avatar
Glen Mével committed
264
    - tick_then_step_then exec_tick_case_branch.
265 266 267 268 269
      (* this is the only place where we need the term to be closed (because
       * the reduction rules for Case are adhoc somehow: *)
      simpl in Hclosed ; repeat (apply andb_True in Hclosed as [ Hclosed ? ]).
      by apply is_closed_translation.
    (* CaseRS e0 v0 e1 e2 σ : *)
Glen Mével's avatar
Glen Mével committed
270
    - tick_then_step_then exec_tick_case_branch.
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
      (* this is the only place where we need the term to be closed (because
       * the reduction rules for Case are adhoc somehow: *)
      simpl in Hclosed ; repeat (apply andb_True in Hclosed as [ Hclosed ? ]).
      by apply is_closed_translation.
    (* ForkS e σ : *)
    - replace [« e »] with ([« e »] ++ []) by apply app_nil_r.
      eapply prim_exec_cons.
      + prim_step.
      + exec_tick_success.
    (* AllocS e v σ l : *)
    - 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.
    (* StoreS l e v σ : *)
    - tick_then_step_then_stop.
      rewrite lookup_insert_ne ; last exact I.
      by apply lookup_translationS_is_Some.
    (* CasFailS l e1 v1 e2 v2 vl σ : *)
    - 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.
298
      + by apply vals_cas_compare_safe_translationV.
299 300
    (* CasSucS l e1 v1 e2 v2 σ : *)
    - tick_then_step_then_stop.
301 302 303
      + rewrite lookup_insert_ne ; last exact I.
        by apply lookup_translationS_Some.
      + by apply vals_cas_compare_safe_translationV.
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 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 367 368 369 370 371 372 373 374 375 376
    (* FaaS l i1 e2 i2 σ : *)
    - tick_then_step_then_stop.
      rewrite lookup_insert_ne ; last exact I.
      change (#i1)%V with V« #i1 ».
      by apply lookup_translationS_Some.
  Qed.

  Lemma simulation_prim_step_success n e1 σ1 e2 σ2 efs :
    σ2 !!  = None 
    is_closed [] e1 
    prim_step e1 σ1 e2 σ2 efs 
    prim_exec «e1» S«σ1, S n» «e2» S«σ2, n» T«efs».
  Proof.
    intros H Hclosed [ K e1' e2' -> -> H ].
    rewrite 2! translation_fill.
    apply is_closed_fill_inv in Hclosed.
    by eapply prim_exec_fill, simulation_head_step_success.
  Qed.

  Lemma simulation_step_success n t1 σ1 t2 σ2 :
    σ2 !!  = None 
    Forall (is_closed []) t1 
    step (t1, σ1) (t2, σ2) 
    rtc step (T«t1», S«σ1, S n») (T«t2», S«σ2, n»).
  Proof.
    intros H Hclosed Hstep.
    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.
    apply Forall_app, proj2, Forall_cons, proj1 in Hclosed.
    by apply exec_frame_singleton_thread_pool, prim_exec_exec, simulation_prim_step_success.
  Qed.

  Lemma simulation_exec_success m n t1 σ1 t2 σ2 :
    σ2 !!  = None 
    Forall (is_closed []) t1 
    nsteps step m (t1, σ1) (t2, σ2) 
    rtc step (T«t1», S«σ1, m+n») (T«t2», S«σ2, n»).
  Proof.
    make_eq (t1, σ1) as config1 E1.
    make_eq (t2, σ2) as config2 E2.
    intros H Hclosed Hnsteps.
    revert t1 σ1 E1 Hclosed ;
    induction Hnsteps as [ config | m' config1 (t3, σ3) config2 Hstep Hsteps IHnsteps ] ;
    intros t1 σ1 E1 Hclosed.
    - 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).
      assert (Forall (is_closed []) t3) as Hclosed3 by by eapply is_closed_step.
      specialize (IHnsteps Hclosed3).
      eapply rtc_transitive.
      + apply simulation_step_success ; cycle -1 ; eassumption.
      + apply IHnsteps.
  Qed.

  Lemma simulation_exec_success' m n t1 σ1 t2 σ2 :
    σ2 !!  = None 
    Forall (is_closed []) t1 
    (m  n)%nat 
    nsteps step m (t1, σ1) (t2, σ2) 
    rtc step (T«t1», S«σ1, n») (T«t2», S«σ2, n-m»).
  Proof.
    intros H Hclosed I.
    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. *)

377
  (* note: this does not depend on the operational behavior of `tick`. *)
378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427

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

  Local Ltac eexhibit_prim_step :=
    eexists _, _, _ ; simpl ; prim_step.

  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.
    intros Hactive Hfresh (e2' & σ2' & efs & Hheadstep % active_item_prim_step_is_head_step) ;
      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.
    destruct Hheadstep as
      [ (* BetaS *) f x e1 e2 v2 e' σ1  Hval_e2 Hclosed_e1 E'
      | (* UnOpS *) op e1 v1 v' σ1  Hval_e1 Hopeval
      | (* BinOpS *) op e1 e2 v1 v2 v' σ1  Hval_e1 Hval_e2 Hopeval
      | (* IfTrueS  *) e1 e2 σ1
      | (* IfFalseS *) e1 e2 σ1
      | (* FstS *) e1 v1 e2 v2 σ1  Hval_e1 Hval_e2
      | (* SndS *) e1 v1 e2 v2 σ1  Hval_e1 Hval_e2
      | (* CaseLS *) e0 v0 e1 e2 σ1  Hval_e0
      | (* CaseRS *) e0 v0 e1 e2 σ1  Hval_e0
      | (* ForkS *) e σ1
      | (* AllocS *) e1 v1 σ1 l  Hval_e1 Hfree_l
      | (* LoadS *) l v1 σ1  Hbound_l
      | (* StoreS *) l e1 v1 σ1  Hval_e1 Hisbound_l
      | (* CasFailS *) l e1 v1 e2 v2 vl σ1  Hval_e1 Hval_e2 Hbound_l Hneq_vl_v1
      | (* CasSucS *) l e1 v1 e2 v2 σ1  Hval_e1 Hval_e2 Hbound_l
      | (* FaaS *) l i1 e2 i2 σ1  Hval_e2 Hbound_l
      ] ;
    destruct ki ; try contradiction Hactive ; try discriminate Ee1' ;
    injection Ee1' ; clear Ee1' ;
    repeat (intros -> || intros <- || intros -> % translationV_lit_inv_expr || intros E) ;
    destruct Eσ1' ;
    repeat lazymatch goal with H : to_val (of_val «_»%V) = Some _ |- _ =>
      rewrite to_of_val in H ; injection H as <-
    end .
    (* 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
    ].
    (* BetaS *)
428
    - destruct v ; try discriminate E.
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
      eexhibit_prim_step.
    (* 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 (? & ? & _).
      eexhibit_prim_step.
    (* StoreS *)
    - eexhibit_prim_step.
      by eapply lookup_translationS_is_Some_inv.
    (* CasFailS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & ->).
      exhibit_prim_step (#false)%E.
464 465
      + intros ? % (f_equal translationV). contradiction.
      + by apply vals_cas_compare_safe_translationV_inv.
466 467 468
    (* CasSucS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % translationV_injective).
      exhibit_prim_step (#true)%E.
469
      by apply vals_cas_compare_safe_translationV_inv.
470 471 472 473 474 475 476
    (* FaaS *)
    - apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % eq_sym % translationV_lit_inv).
      rewrite to_of_val in Hval_e2 ; injection Hval_e2 as -> % translationV_lit_inv.
      eexhibit_prim_step.
  Qed.

  (* assuming the safety of the translated expression,
477
   * a proof that the original expression is m-safe. *)
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509

  Lemma safe_translation__safe_here m e σ :
    is_closed [] e 
    loc_fresh_in_expr  e 
    (m > 0)%nat 
    safe «e» S«σ, m» 
    is_Some (to_val e)  reducible e σ.
  Proof.
    intros Hclosed Hfresh Im Hsafe.
    (* 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: *)
      pose proof (not_val_fill_active_item _ Hclosed Hnotval) as He ; clear Hclosed Hnotval.
      destruct He as [ (K & e1 & ->) | (K & ki & v & -> & Hactive) ].
      (*  either e = K[Fork e1]: *)
      + (* then we easily derive a reduction from e: *)
        eexists _, _, _. apply Ectx_step', ForkS.
      (*  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»]
510
         * (m  1 so tick can be run): *)
511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557
        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.
  Lemma safe_translation__safe m n e σ t2 σ2 e2 :
    is_closed [] e 
    loc_fresh_in_expr  e2 
    σ2 !!  = None 
    safe «e» S«σ, m» 
    nsteps step n ([e], σ) (t2, σ2) 
    (n < m)%nat 
    e2  t2 
    is_Some (to_val e2)  reducible e2 σ2.
  Proof.
    intros Hclosed He Hℓσ Hsafe Hnsteps Inm He2.
    assert (safe «e2» S«σ2, m-n») as Hsafe2.
    {
      eapply safe_exec.
      - eapply elem_of_list_fmap_1. eassumption.
      - eassumption.
      - change [«e»] with T«[e]». apply simulation_exec_success' ; [ assumption | auto | lia | assumption ].
    }
    assert (is_closed [] e2) as Hclosede2.
    {
      assert (Forall (is_closed []) t2) as Hclosedt2
        by eauto using nsteps_rtc, is_closed_exec.
      by eapply Forall_forall in Hclosedt2 ; last exact He2.
    }
    assert (m - n > 0)%nat by lia.
    by eapply safe_translation__safe_here.
  Qed.

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

560 561
  (* 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
562
  Lemma adequate_translation__adequate_result m n φ e σ t2 σ2 v2 :
563 564
    is_closed [] e 
    σ2 !!  = None 
565
    adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)) 
566 567 568 569 570 571
    nsteps step n ([e], σ) (of_val v2 :: t2, σ2) 
    (n  m)%nat 
    φ v2.
  Proof.
    intros Hclosed Hfresh Hadq Hnsteps Inm.
    assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
572
    replace (φ v2) with ((φ  invtranslationV) (translationV v2))
573
      by (simpl ; by rewrite invtranslationV_translationV).
574
    eapply (adequate_result _ _ _ (λ v σ, φ (invtranslationV v))); first done.
575 576 577 578 579
    change [«e»%E] with T«[e]».
    replace (of_val «v2» :: _) with (T«of_val v2 :: t2») by by rewrite - translation_of_val.
    eapply simulation_exec_success' ; eauto.
  Qed.

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

582
(* now lets combine the two results. *)
583

Glen Mével's avatar
Glen Mével committed
584
Lemma adequate_translation__adequate m φ e σ :
585
  is_closed [] e 
586
  ( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) 
Glen Mével's avatar
Glen Mével committed
587
  nadequate NotStuck m e σ φ.
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614
Proof.
  intros Hclosed Hadq.
  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).
    by eapply adequate_translation__adequate_result.
  (* (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)
      by by apply loc_not_in_set_is_fresh.
    assert (σ2 !!  = None)
      by by (simpl ; eapply not_elem_of_dom).
    specialize (Hadq Hloc) as Hsafe % safe_adequate.
    by eapply safe_translation__safe.
Qed.

End Simulation.