text:
(* Compatibility lemmas for logical relations.
 * Part of the CertiCoq project.
 * Author: Zoe Paraskevopoulou, 2017
 *)

From Coq Require Import NArith.BinNat Relations.Relations MSets.MSets
                        MSets.MSetRBT Lists.List omega.Omega Sets.Ensembles.
From SFS Require Import functions cps ctx cps_util identifiers ctx Ensembles_util
     List_util tactics set_util map_util.

From SFS Require Import heap heap_defs heap_equiv GC space_sem cc_log_rel closure_conversion.

From SFS Require Import Coqlib.

Import ListNotations.

Module Compat (H : Heap).

  Module LR := CC_log_rel H.

  Import H LR LR.Sem LR.Sem.GC LR.Sem.GC.Equiv LR.Sem.GC.Equiv.Defs LR.Sem.GC.Equiv.Defs.HL.

  Section CompatDefs.

    Variable (clo_tag : cTag).

    Context (IG : GInv) (* Final global *)
            (IL1 IL2: Inv) (* Final local *)
            (ILe : exp -> exp -> Inv)

            (IIG : GIInv) (* Global initial *)
            (IIL1 IIL2 : IInv) (* Local initial *)
            (IILe : exp -> exp -> IInv) (* Local initial *)

            (M : nat) (* memory cost factor *)
            (F : nat) (* time cost factor *).

    (** * Base case and timout compatibility *)

    Definition InvCostBase (e1 e2 : exp) :=
      forall (H1' H2' : heap block) (rho1' rho2' : env) (c : nat),
        IIL1 (H1', rho1', e1) (H2', rho2', e2) ->
        cost e1 <= c ->
        IL1 (H1', rho1', e1, c, reach_size H1' rho1' e1)
            (H2', rho2', e2, c, size_heap H2').

    Definition InvCostTimeOut (e1 e2 : exp) :=
      forall (H1' H2' : heap block) (rho1' rho2' : env) (c : nat),
        IIL1 (H1', rho1', e1) (H2', rho2', e2) ->
        c < cost e1 ->
        IL1 (H1', rho1', e1, c, reach_size H1' rho1' e1)
            (H2', rho2', e2, c, size_heap H2').

    Definition InvCostTimeOut' ε (e1 e2 : exp) :=
      forall (H1' H2' : heap block) (rho1' rho2' : env) (c m : nat),
        IIL1 (H1', rho1', e1) (H2', rho2', e2) ->
        c < cost e1 ->
        m <= size_heap H2' + ε ->
        IL1 (H1', rho1', e1, c, reach_size H1' rho1' e1)
            (H2', rho2', e2, c, m).

    Definition InvCostTimeOut_Funs B1 (e1 : exp) B2 e2 :=
      forall (H1' H2' : heap block) (rho1' rho2' : env) (c : nat),
        c < 1 + PS.cardinal (fundefs_fv B1) ->
        IIL1 (H1', rho1', Efun B1 e1) (H2', rho2', Efun B2 e2) ->
        IL1 (H1', rho1', Efun B1 e1, c, reach_size H1' rho1' (Efun B1 e1))
            (H2', rho2', Efun B2 e2, 0, size_heap H2').

    (* Definition InvCostTO (e1 e2 : exp) := *)
    (*   forall (H1' H2' : heap block) (rho1' rho2' : env) c,    *)
    (*     IL2 (H1', rho1', e1, 0, size_heap H1') (H2', rho2', e2, c, size_heap H2'). *)

    (** * Constructor application compatibility *)

    Definition InvCtxCompat (C1 C2 : exp_ctx) (e1 e2 : exp)  :=
      forall (H1' H2' H1'' H2'' : heap block) (rho1' rho2' rho1'' rho2'' : env) c1 c2 c1' c2' m1 m2,

        IL2 (H1'', rho1'', e1, c1, m1) (H2'', rho2'', e2, c2, m2) ->
        cost (C1 |[ e1 ]|) <= c1' ->

        ctx_to_heap_env C1 H1' rho1' H1'' rho1'' c1' ->
        ctx_to_heap_env_CC C2 H2' rho2' H2'' rho2'' c2' ->

        IL1 (H1', rho1', C1 |[ e1 ]|, c1 + c1', (max (reach_size H1' rho1' (C1 |[ e1 ]|)) m1))
            (H2', rho2', C2 |[ e2 ]|, c2 + c2', m2).

    Definition IInvCtxCompat (C1 C2 : exp_ctx) (e1 e2 : exp)  :=
      forall (H1' H2' H1'' H2'' : heap block) (rho1' rho2' rho1'' rho2'' : env) c1' c2',
        IIL1 (H1', rho1', C1 |[ e1 ]|) (H2', rho2', C2 |[ e2 ]|) ->

        ctx_to_heap_env C1 H1' rho1' H1'' rho1'' c1' ->
        ctx_to_heap_env_CC C2 H2' rho2' H2'' rho2'' c2' ->

        IIL2 (H1'', rho1'', e1) (H2'', rho2'', e2).

    Definition IInvCtxCompat_Funs (B1 B2 : fundefs) (e1 e2 : exp)  :=
      forall (H1' H2' H1'' H2'' : heap block) (rho1' rho2' rho1'' rho2'' : env) c1' c2',
        IIL1 (H1', rho1', Efun B1 e1) (H2', rho2', Efun B2 e2) ->
        binding_in_map (occurs_free_fundefs B1) rho1' ->

        ctx_to_heap_env (Efun1_c B1 Hole_c) H1' rho1' H1'' rho1'' c1' ->
        ctx_to_heap_env_CC (Efun1_c B2 Hole_c) H2' rho2' H2'' rho2'' c2' ->

        IIL2 (H1'', rho1'', e1) (H2'', rho2'', e2).

    Definition InvCtxCompat_r (C : exp_ctx) (e1 e2 : exp) :=
      forall (H1' H2' H2'' : heap block) (rho1' rho2' rho2'' : env) c' c1 c2 m1 m2,
        IL2 (H1', rho1', e1, c1, m1) (H2'', rho2'', e2, c2, m2) ->
        cost e1 <= c1 ->

        ctx_to_heap_env_CC C H2' rho2' H2'' rho2'' c' ->

        IL1 (H1', rho1', e1, c1, m1) (H2', rho2', C |[ e2 ]|, c2 + c', m2).

    Definition InvCtxCompat_r_strong (C : exp_ctx) (e1 e2 : exp) :=
      forall (H1' H2' H2'' : heap block) (rho1' rho2' rho2'' : env) c' c1 c2 m1 m2,
        IL2 (H1', rho1', e1, c1, m1) (H2'', rho2'', e2, c2, m2) ->

        ctx_to_heap_env_CC C H2' rho2' H2'' rho2'' c' ->

        IL1 (H1', rho1', e1, c1, m1) (H2', rho2', C |[ e2 ]|, c2 + c', m2).

    Definition IInvCtxCompat_r (C : exp_ctx) (e1 e2 : exp) :=
      forall (H1' H2' H2'' : heap block) (rho1' rho2' rho2'' : env) c',
        IIL1 (H1', rho1', e1) (H2', rho2', C |[ e2 ]|) ->

        ctx_to_heap_env_CC C H2' rho2' H2'' rho2'' c' ->

        IIL2 (H1', rho1', e1) (H2'', rho2'', e2).

    Definition InvCtxCompat_r_inv (C : exp_ctx) (e1 e2 : exp) :=
      forall (H1' H2' H2'' : heap block) (rho1' rho2' rho2'' : env) c' c1 c2 m1 m2,
        IL1 (H1', rho1', e1, c1, m1) (H2', rho2', C |[ e2 ]|, c2 + c', m2) ->
        cost e1 <= c1 ->

        ctx_to_heap_env_CC C H2' rho2' H2'' rho2'' c' ->

        IL2 (H1', rho1', e1, c1, m1) (H2'', rho2'', e2, c2, m2).

    Definition IInvCtxCompat_r_inv (C : exp_ctx) (e1 e2 : exp) :=
      forall (H1' H2' H2'' : heap block) (rho1' rho2' rho2'' : env) c',
        IIL2 (H1', rho1', e1) (H2'', rho2'', e2) ->

        ctx_to_heap_env_CC C H2' rho2' H2'' rho2'' c' ->

        IIL1 (H1', rho1', e1) (H2', rho2', C |[ e2 ]|).

    (** * Case compatibility *)

    Definition IInvCaseCompat x1 x2 Pats1 Pats2 :=
      forall H1' rho1' H2' rho2' c1 c2 e1 e2,
        List.In (c1, e1) Pats1 ->
        List.In (c2, e2) Pats2 ->
        IIL1 (H1', rho1', Ecase x1 Pats1) (H2', rho2', Ecase x2 Pats2) ->
        IILe e1 e2 (H1', rho1', e1) (H2', rho2', e2).

    Definition InvCaseCompat x1 x2 Pats1 Pats2 :=
      forall H1' rho1' H2' rho2' m1 m2 c1 c2 c e1 e2 tc1 tc2,
        List.In (tc1, e1) Pats1 ->
        List.In (tc2, e2) Pats2 ->
        cost (Ecase x1 Pats1) <= c ->
        ILe e1 e2 (H1', rho1', e1, c1, m1) (H2', rho2', e2, c2, m2) ->
        IL1 (H1', rho1', Ecase x1 Pats1, c1 + c, (max (reach_size H1' rho1' (Ecase x1 Pats1)) m1))
            (H2', rho2', Ecase x2 Pats2, c2 + c, m2).

    (** * App compatibility *)

    Definition IInvAppCompat (H1 H2 : heap block) (rho1 rho2 : env) f1 t xs1 f2 xs2 f2' Γ :=
      forall (i  : nat) (H1' H1'' H2' Hgc2: heap block)
        env_loc (rho_clo rho_clo1 rho_clo2 rho1' rho2' rho2'' : env) β1 β2
        (B1 : fundefs) (f1' : var) (ct1 : cTag)
        (xs1' : list var) (e1 : exp) (l1 : loc)
        (vs1 : list value)
        (B2 : fundefs) (f3 : var) (c ct2 : cTag) (xs2' : list var)
        (e2 : exp) (l2 env_loc2 : loc) (vs2 : list value) c1 c2 m1 m2 d,
        (occurs_free (Eapp f1 t xs1)) |- (H1, rho1) ⩪_(id, β1) (H1', rho1') ->
        injective_subdomain (reach' H1' (env_locs rho1' (occurs_free (Eapp f1 t xs1)))) β1 ->

        (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ)) |- (H2, rho2) ⩪_(β2, id) (H2', rho2') ->
        injective_subdomain (reach' H2 (env_locs rho2 (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ)))) β2 ->

        (* Post on the function result  *)
        IG (reach_size H1'' rho_clo2 e1) (1 + (PS.cardinal (fundefs_fv B1)))
           (H1'', rho_clo2, e1, c1, m1) (Hgc2, subst_env d rho2'', e2, c2, m2) ->
        (* Pre before APP *)
        IIL1 (H1', rho1', Eapp f1 t xs1) (H2', rho2', AppClo clo_tag f2 t xs2 f2' Γ) ->

        M.get f1 rho1' = Some (Loc l1) ->
        get l1 H1' = Some (Clos (FunPtr B1 f1') (Loc env_loc)) ->
        get env_loc H1' = Some (Env rho_clo) ->
        find_def f1' B1 = Some (ct1, xs1', e1) ->
        getlist xs1 rho1' = Some vs1 ->
        def_closures B1 B1 rho_clo H1' (Loc env_loc) = (H1'', rho_clo1) ->
        setlist xs1' vs1 rho_clo1 = Some rho_clo2 ->

        M.get f2 rho2' = Some (Loc l2) ->
        getlist xs2 rho2' = Some vs2 ->
        get l2 H2' = Some (Constr c [FunPtr B2 f3; Loc env_loc2]) ->
        Some rho2'' =
        setlist xs2' (Loc env_loc2 :: vs2) (def_funs B2 B2 (M.empty value)) ->
        find_def f3 B2 = Some (ct2, xs2', e2) ->
        live' ((env_locs rho2'') (occurs_free e2)) H2' Hgc2 d ->

        reach_size H1'' rho_clo2 e1 <= m1 ->
        (* Post on result of APP *)
        IL1 (H1', rho1', Eapp f1 t xs1, c1 + cost (Eapp f1 t xs1), max (reach_size H1' rho1' (Eapp f1 t xs1)) m1)
            (H2', rho2', AppClo clo_tag f2 t xs2 f2' Γ, c2 + 1 + 1 + cost (Eapp f2' t (Γ :: xs2)), max m2 (size_heap H2')).

  End CompatDefs.

  Section CompatLemmas.

    Variable (clo_tag : cTag).

    Context (IG : GInv) (* Final global *)
            (IL1 IL2: Inv) (* Final local *)
            (ILe : exp -> exp -> Inv)

            (IIG : GIInv) (* Global initial *)
            (IIL1 IIL2 : IInv)
            (IILe : exp -> exp -> IInv) . (* Local initial *)

    (** Application compatibility *)
    Lemma cc_approx_exp_app_compat (k j : nat) (b : Inj) (H1 H2 : heap block)
          (rho1 rho2 : env) (f1 : var) (xs1 : list var)
          (f2 f2' Γ : var) (xs2 : list var) (t : fTag) :
      IInvAppCompat clo_tag IG IL1 IIL1 H1 H2 rho1 rho2 f1 t xs1 f2 xs2 f2' Γ ->
      InvCostTimeOut IL1 IIL1 (Eapp f1 t xs1) (AppClo clo_tag f2 t xs2 f2' Γ) ->
      (* InvCostTO IL2 -> *)

      ~ Γ \in (f2 |: FromList xs2) ->
      ~ f2' \in (f2 |: FromList xs2) ->
      Γ <> f2' ->

      (forall j, cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2 f1 f2) ->
      Forall2 (fun x1 x2 =>
                 forall j, cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2 x1 x2)
              xs1 xs2 ->

      (Eapp f1 t xs1, rho1, H1) ⪯ ^ (k ; j; IIL1 ; IIG
                                     ; IL1
                                     ; IG)
      (AppClo clo_tag f2 t xs2 f2' Γ, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hiinv Hbase Hnin1 Hnin2 Hneq  Hvar Hall
             b1 b2 H1' H2' rho1' rho2' v1 c1 m1 Heq1 Hinj1 Heq2 Hinj2
             HII Hleq1 Hstep1 Hstuck1.
      eapply (cc_approx_var_env_heap_env_equiv
                _ _
                (occurs_free (Eapp f1 t xs1))
                (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ)) k j) in Hvar;
          [| eassumption | eassumption | eassumption | eassumption
           | normalize_occurs_free; now eauto with Ensembles_DB
           | unfold AppClo; normalize_occurs_free; now eauto with Ensembles_DB ].
      inv Hstep1.
      (* Timeout! *)
      - { edestruct (Hstuck1 (cost (Eapp f1 t xs1))) as [v1 [m1 Hstep1]].
          inv Hstep1; [ omega | ].
          exists OOT, c1. destruct (lt_dec c1 1).
          - eexists. eexists id. repeat split.
            now constructor; eauto.
            (* now eapply injective_subdomain_Empty_set. *)
            (* rewrite <- plus_n_O. *)
            eapply Hbase; try eassumption.
            now rewrite cc_approx_val_eq.
          - edestruct Hvar as [l2 [Hget' Hcc]]; eauto.
            simpl cc_approx_val' in Hcc. rewrite Hgetl in Hcc.
            destruct l2 as [l2 | ]; [| contradiction ].
            destruct Hcc as [Hbeq Hcc]; simpl in Hcc.
            destruct (get l2 H2') as [v |] eqn:Hget2; try contradiction.
            destruct v as [ c [| [| B2 f3 ] [| [env_loc |] [|] ] ] | | ]; try contradiction.
            destruct Hcc as [Henv Hcc].
            edestruct Hcc with (vs2 := vs)
              as (xs2' & e2 & rho2'' & Hfind' & Hset' & Hi'); try eassumption.
            reflexivity. clear. now firstorder. symmetry.
            reflexivity. clear. now firstorder.
            reflexivity.
            destruct (lt_dec (c1 - 1) 1).
            + eexists. eexists id. repeat split. unfold AppClo.
              eapply Eval_proj_per_cc; eauto.
              simpl. omega. reflexivity.
              now econstructor; simpl; eauto.
              (* rewrite <- !plus_n_O. *)
              eapply Hbase; try eassumption.
              rewrite cc_approx_val_eq. now eauto.
            + eexists. eexists id. repeat split. unfold AppClo.
              eapply Eval_proj_per_cc; eauto.
              simpl. omega. reflexivity.
              eapply Eval_proj_per_cc; eauto.
              simpl. omega.
              rewrite M.gso. eassumption.
              intros Heq; subst. now eauto with Ensembles_DB.
              reflexivity.
              econstructor; try (now simpl; eauto). simpl.
              erewrite <- Forall2_length; [| eassumption ]. simpl in *. omega.
              (* rewrite <- plus_n_O. *)
              eapply Hbase; try eassumption.
              now rewrite cc_approx_val_eq. }
      (* Termination *)
      - { simpl in Hcost.
          assert (Hall1 := Hall).
          eapply Forall2_monotonic_strong
                 with (R' := (fun x1 x2 : var =>
                                forall j : nat,
                                  cc_approx_var_env
                                    k j IIG IG (b2 ∘ b ∘ b1)
                                    H1' rho1' H2' rho2' x1 x2))
            in Hall; (* yiiiiiikes *)
            [
            | intros x1 x2 Hin1 Hin2 Hyp j';
              eapply (cc_approx_var_env_heap_env_equiv
                        _ _
                        (occurs_free (Eapp f1 t xs1))
                        (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ))) in Hyp;
              [ now eapply Hyp | eassumption | eassumption | eassumption | eassumption
                | normalize_occurs_free; now eauto with Ensembles_DB
                | unfold AppClo; repeat normalize_occurs_free; rewrite FromList_cons ];
              right; constructor;
              [ right; constructor;
                [ now eauto with Ensembles_DB
                | now intros Hc; inv Hc; eapply Hnin1; eauto ]
              | now intros Hc; inv Hc; eapply Hnin2; eauto ]
            ].
          edestruct (cc_approx_var_env_getlist IIG IG  k j rho1' rho2')
            as [vs2 [Hgetl' Hcc']];
            [ | now eauto |].
          eapply Forall2_monotonic; [| now apply Hall ].
          intros x1 x2 Hcc1. now eapply Hcc1.

          edestruct Hvar as [l2 [Hget' Hcc]]; eauto.
          simpl in Hcc. rewrite Hgetl in Hcc. destruct l2 as [l2 | ]; [| contradiction ].
          destruct Hcc as [Hbeq Hcc]. simpl in Hcc.
          destruct (get l2 H2') as [v |] eqn:Hget2; try contradiction.
          destruct v as [ ? [| [| B2 f3 ] [| [ env_loc' |] [|] ]] | | ]; try contradiction.
          edestruct Hcc
            as (Henv & xs2' & e2 & rho2'' & Hfind' & Hset' & Hi');
            try eassumption.
          reflexivity. clear; now firstorder. reflexivity. clear; now firstorder.
          eapply Forall2_length. eassumption.

          edestruct (live_exists' (env_locs rho2'' (occurs_free e2)) H2')
            as [H2'' [b' Hgc']].
          tci.
          (* edestruct (live'_live_inv (env_locs rho_clo2 (occurs_free e)) b0 H' H'') *)
          (*   as [b'' [Hgc1' [Hfe1 Hfe2]]]; try eassumption. *)
          (* assert (Hgc1 := Hgc1'); *)
          assert (Hgc2 := Hgc').
          (* destruct Hgc1' as [Hseq [Heqgc Hinjgc]].  *)
          destruct Hgc' as  [Hseq' [Heqgc' Hinjgc']].
          edestruct Hi' with (i := k - cost  (Eapp f1 t xs1))
            as [HG [r2 [c2 [m2 [b2' [Hbs2 [HIG  Hcc2]]]]]]];
            [ | | | reflexivity | | |  | |  | | | ]; try eassumption.
          + simpl. omega.
          (* + rewrite compose_id_neut_r. rewrite compose_id_neut_l. reflexivity. *)
          + intros j'. eapply Forall2_monotonic_strong; [| eassumption ].
            intros v v' Hinv1 Hinv2 Heq. rewrite cc_approx_val_eq.
            eapply cc_approx_val_monotonic with (k := k).
            assert (Hrv : val_loc v \subset env_locs rho1' (occurs_free (Eapp f1 t xs1))).
            { normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. rewrite env_locs_FromList.
              simpl. eapply In_Union_list.
              eapply in_map. eassumption. eassumption. }
            assert (Hrv' : val_loc v' \subset
                           env_locs rho2' (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ))).
            { unfold AppClo. repeat normalize_occurs_free.
              rewrite FromList_cons, !Setminus_Union_distr, !env_locs_Union.
              do 2 eapply Included_Union_preserv_r.
              eapply Included_Union_preserv_l. eapply Included_Union_preserv_r.
              rewrite !Setminus_Disjoint.
              rewrite env_locs_FromList.
              simpl. eapply In_Union_list.
              eapply in_map. eassumption. eassumption.
              now eapply Disjoint_Singleton_r; intros Hc; eapply Hnin1; eauto.
              now eapply Disjoint_Singleton_r; intros Hc; inv Hc; eapply Hnin2; eauto. }
            edestruct (cc_approx_var_env_getlist IIG IG  k j' rho1' rho2')
              as [vs2' [Hgetl'' Hcc'']];
              [ | now eauto |].
            eapply Forall2_monotonic; [| now apply Hall ].
            now intros x1 x2 Heq12; eapply Heq12.
            rewrite Hgetl' in Hgetl''. inv Hgetl''.
            edestruct (Forall2_exists _ vs vs2' v Hinv1 Hcc'')
              as [x' [Hinx2 Hr']].
            destruct v; try contradiction.
            apply cc_approx_val_loc_eq in Heq. subst.
            assert (Hr := Hr').
            eapply cc_approx_val_loc_eq in Hr. subst.
            now eauto.
            simpl. omega.

          + rewrite Combinators.compose_id_left, Combinators.compose_id_right.
            reflexivity.

          + clear; now firstorder.

          + eapply heap_env_equiv_heap_equiv_l. eassumption.

          + (* initial after GC *)
            eapply HG; eassumption.
          + simpl. omega.
          + intros i.
            edestruct (Hstuck1 (i + cost (Eapp f1 t xs1))) as [r' [m'' Hstep']].
            inv Hstep'.
            * omega.
            * rewrite Nat.add_sub in Hbs0.
              repeat subst_exp.
              do 2 eexists. eassumption.

          +  do 3 eexists. exists b2'. eexists. repeat split.
             * eapply Eval_proj_per_cc with   (c := c2 + 1 + 1 + cost (Eapp f2' t (Γ :: xs2))).
               simpl; omega.
               eassumption. eassumption. reflexivity.
               eapply Eval_proj_per_cc. simpl; omega.
               rewrite M.gso. eassumption.
               intros Hc. subst. eapply Hnin2. now left; eauto.
               eassumption. reflexivity. simpl.
               eapply Eval_app_per_cc.
               simpl. omega.
               rewrite M.gso. rewrite M.gss. reflexivity.
               now intros Hc; subst; eauto.
               eassumption.
               simpl. rewrite M.gss.
               rewrite !getlist_set_neq. now rewrite Hgetl'.
               intros Hc. eapply Hnin2. now eauto.
               intros Hc. eapply Hnin1. now eauto.
               now eauto. eassumption. reflexivity. simpl.
               replace (c2 + 1 + 1 + S (S (length xs2)) - 1 - 1 - S (S (length xs2)))  with c2.
               eassumption. omega.
             * replace c1 with (c1 - cost (Eapp f1 t xs1) + cost (Eapp f1 t xs1)) by (simpl in *; omega).
               split. eapply Hiinv; try eassumption.
               eapply big_step_reach_leq. eassumption.
               rewrite cc_approx_val_eq in *. eapply cc_approx_val_monotonic.
               eassumption. simpl. omega. }
    Qed.

    Lemma cc_approx_exp_constr_compat (k j : nat)
          (b : Inj) (H1 H2 : heap block) (rho1 rho2 : env)
          (x1 x2 : var) (t : cTag) (ys1 ys2 : list var) (e1 e2 : exp)  :
      InvCtxCompat IL1 IL2 (Econstr_c x1 t ys1 Hole_c) (Econstr_c x2 t ys2 Hole_c) e1 e2 ->
      IInvCtxCompat IIL1 IIL2 (Econstr_c x1 t ys1 Hole_c) (Econstr_c x2 t ys2 Hole_c) e1 e2 ->
      InvCostTimeOut IL1 IIL1 (Econstr x1 t ys1 e1) (Econstr x2 t ys2 e2)  ->

      well_formed (reach' H1 (env_locs rho1 (occurs_free (Econstr x1 t ys1 e1)))) H1 ->
      well_formed (reach' H2 (env_locs rho2 (occurs_free (Econstr x2 t ys2 e2)))) H2 ->
      (env_locs rho1 (occurs_free (Econstr x1 t ys1 e1))) \subset dom H1 ->
      (env_locs rho2 (occurs_free (Econstr x2 t ys2 e2))) \subset dom H2 ->

      (forall j, Forall2 (cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2) ys1 ys2) ->

      (forall vs1 vs2 l1 l2 H1' H2',
         k >= cost (Econstr x1 t ys1 e1) ->
         (* allocate a new location for the constructed value *)
         locs (Constr t vs1) \subset env_locs rho1 (FromList ys1) ->
         locs (Constr t vs2) \subset env_locs rho2 (FromList ys2) ->

         alloc (Constr t vs1) H1 = (l1, H1') ->
         alloc (Constr t vs2) H2 = (l2, H2') ->
         (* values are related *)
         (forall j, Forall2 (fun l1 l2 => (Res (l1, H1)) ≺ ^ (k - cost (Econstr x1 t ys1 e1) ; j ; IIG ; IG ; b) (Res (l2, H2))) vs1 vs2) ->
         (forall j, (e1, M.set x1 (Loc l1) rho1, H1') ⪯ ^ (k - cost (Econstr x1 t ys1 e1) ; j ; IIL2 ; IIG ; IL2 ; IG)
               (e2, M.set x2 (Loc l2) rho2, H2'))) ->

      (Econstr x1 t ys1 e1, rho1, H1) ⪯ ^ (k ; j ; IIL1; IIG ; IL1 ; IG) (Econstr x2 t ys2 e2, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hinv Hiinv Hbase Hwf1 Hwf2 Hdom1 Hdom2 Hall Hpre b1 b2 H1' H2' rho1' rho2' v1 c1 m1
             Heq1 Hinj1 Heq2 Hinj2 HII Hleq1 Hstep1 Hstuck1.
      assert (Hall' := Hall).
      inv Hstep1.
      (* Timeout! *)
      - { exists OOT, c1. eexists. exists id. repeat split.
          - econstructor. simpl. specialize (Hall 0). erewrite <- Forall2_length; [| eassumption ].
            simpl in Hcost. omega. reflexivity.
          (* - simpl. eapply injective_subdomain_Empty_set.  *)
          - eapply Hbase; try eassumption.
          - now rewrite cc_approx_val_eq. }
      (* Termination *)
      - { edestruct (cc_approx_var_env_getlist IIG IG k j rho1' rho2') as [vs2 [Hget' Hpre']];
          [| eauto |]; eauto.
          specialize (Hall j).
          eapply Forall2_monotonic_strong; [| eassumption ].
          intros x1' x2' Hin1 Hin2 Hvar.

          eapply cc_approx_var_env_heap_env_equiv; try eassumption.

          normalize_occurs_free... normalize_occurs_free...
          edestruct heap_env_equiv_env_getlist as [vs1' [Hget1' Hall1]];
            [| symmetry; now apply Heq1 | |]; try eassumption.
          normalize_occurs_free...
          edestruct heap_env_equiv_env_getlist as [vs2' [Hget2' Hall2]];
            [| symmetry; now apply Heq2 | |]; try eassumption.
          normalize_occurs_free...
          destruct (alloc (Constr t vs1') H1) as [l1 H1''] eqn:Hal1.
          destruct (alloc (Constr t vs2) H2') as [l2 H''] eqn:Hal2'.
          destruct (alloc (Constr t vs2') H2) as [l2' H2''] eqn:Hal2.
          assert (Halli := Hall). specialize (Hall j). eapply Forall2_length in Hall.
          assert (Hlen : @length M.elt ys1 = @length M.elt ys2).
          { erewrite (@getlist_length_eq value ys1 vs); [| eassumption ].
            erewrite (@getlist_length_eq value ys2 vs2); [| eassumption ].
            eapply Forall2_length. eassumption. }

          edestruct Hpre with (b1 := extend b1 l l1)
                              (b2 := extend b2 l2' l2)
            as [v2 [c2 [m2 [b' [Hstep [HS Hval]]]]]];
            [ | | | eassumption | eassumption | | | | | | | |  eassumption | | ].
          - simpl in *. omega.
          - simpl. eapply FromList_env_locs. eassumption. reflexivity.
          - simpl. eapply FromList_env_locs. eassumption. reflexivity.
          - intros j'.
            edestruct (cc_approx_var_env_getlist IIG IG k j' rho1 rho2) as [vs2'' [Hget'' Hall'']];
              [| eauto |]; eauto. subst_exp.
            eapply Forall2_monotonic; [| eassumption ]. intros ? ? H.
            eapply cc_approx_val_monotonic.
            now eapply H. omega.
          - eapply heap_env_equiv_alloc; [| | | | | | | eassumption | eassumption | | ].
            + eapply reach'_closed. eassumption. eassumption.
            + eapply reach'_closed.
              eapply well_formed_respects_heap_env_equiv.
              now apply Hwf1. eassumption.
              eapply env_locs_in_dom; eassumption.
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              eapply env_locs_monotonic. normalize_occurs_free...
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              eapply env_locs_monotonic. normalize_occurs_free...
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. simpl.
              rewrite env_locs_FromList; eauto. reflexivity.
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. simpl.
              rewrite env_locs_FromList; eauto. reflexivity.
            + eapply heap_env_equiv_antimon. eapply heap_env_equiv_rename_ext.
              eassumption.
              reflexivity.

              eapply f_eq_subdomain_extend_not_In_S_r.
              intros Hr. eapply reachable_in_dom in Hr.
              eapply alloc_fresh in Halloc. destruct Hr as [s Hgetl]. congruence.
              eapply well_formed_respects_heap_env_equiv.
              now apply Hwf1. eassumption.
              eapply env_locs_in_dom; eassumption.
              reflexivity.
              normalize_occurs_free...
            + rewrite extend_gss. reflexivity.
            + simpl. split. reflexivity.

              eapply Forall2_symm_strong; [| eassumption ].
              intros l3 l4 Hin1 Hin2 Hin. simpl in Hin. symmetry in Hin.
              eapply res_equiv_rename_ext. eassumption.
              reflexivity.

              eapply f_eq_subdomain_extend_not_In_S_r.

              intros Hr. eapply reachable_in_dom in Hr.
              eapply alloc_fresh in Halloc. destruct Hr as [s Hgetl]. congruence.

              eapply well_formed_antimon;
                [| eapply well_formed_respects_heap_env_equiv; (try now apply Hwf1); try eassumption ].
              eapply reach'_set_monotonic. simpl.
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l.

              rewrite env_locs_FromList; try eassumption.
              eapply In_Union_list. eapply in_map. eassumption.
              eapply Included_trans; [| eapply env_locs_in_dom; eassumption ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l.
              rewrite env_locs_FromList; try eassumption.
              eapply In_Union_list. eapply in_map. eassumption.

              reflexivity.
          - eapply injective_subdomain_antimon.
            eapply injective_subdomain_extend. eassumption.

            intros Hc. eapply image_monotonic in Hc; [| now eapply Setminus_Included ].
            eapply heap_env_equiv_image_reach in Hc; try eassumption.
            eapply (image_id (reach' H1 (env_locs rho1 (occurs_free (Econstr x1 t ys1 e1)))))
              in Hc.
            eapply reachable_in_dom in Hc; try eassumption. destruct Hc as [v1' Hgetv1'].
            erewrite alloc_fresh in Hgetv1'; try eassumption. congruence.

            eapply Included_trans. eapply reach'_set_monotonic. eapply env_locs_monotonic.
            eapply occurs_free_Econstr_Included.
            eapply reach'_alloc_set; [| eassumption ].
            eapply Included_trans; [| eapply reach'_extensive ].
            normalize_occurs_free. rewrite env_locs_Union.
            eapply Included_Union_preserv_l.
            rewrite env_locs_FromList; eauto. reflexivity.
          - eapply heap_env_equiv_alloc; [| | | | | | | now apply Hal2 | now apply Hal2' | | ].
            + eapply reach'_closed. eassumption. eassumption.
            + eapply reach'_closed.
              eapply well_formed_respects_heap_env_equiv.
              now apply Hwf2. eassumption.
              eapply env_locs_in_dom; eassumption.
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              eapply env_locs_monotonic. normalize_occurs_free...
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              eapply env_locs_monotonic. normalize_occurs_free...
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. simpl.
              rewrite env_locs_FromList; eauto. reflexivity.
            + eapply Included_trans; [ | now eapply reach'_extensive ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. simpl.
              rewrite env_locs_FromList; eauto. reflexivity.
            + eapply heap_env_equiv_antimon. eapply heap_env_equiv_rename_ext.
              eassumption.

              eapply f_eq_subdomain_extend_not_In_S_r.
              intros Hr. eapply reachable_in_dom in Hr.
              eapply alloc_fresh in Hal2. destruct Hr as [s Hgetl]. congruence.
              now apply Hwf2. eassumption. reflexivity. reflexivity.
              normalize_occurs_free...

            + rewrite extend_gss. reflexivity.
            + symmetry. eapply block_equiv_rename_ext.
              split; eauto. reflexivity.

              eapply f_eq_subdomain_extend_not_In_S_r.
              intros Hr. eapply reachable_in_dom in Hr.
              eapply alloc_fresh in Hal2. destruct Hr as [s Hgetl]. congruence.
              eapply well_formed_antimon; try eassumption.
              eapply reach'_set_monotonic.
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l.
              rewrite env_locs_FromList; eauto. reflexivity.

              eapply Included_trans; [| eassumption ].
              normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l.
              rewrite env_locs_FromList; eauto. reflexivity.

              reflexivity.

          - eapply injective_subdomain_antimon.
            eapply injective_subdomain_extend. eassumption.

            intros Hc. eapply image_monotonic in Hc; [| now eapply Setminus_Included ].
            eapply heap_env_equiv_image_reach in Hc; try (symmetry; eassumption).
            eapply (image_id (reach' H2' (env_locs rho2' (occurs_free (Econstr x2 t ys2 e2)))))
              in Hc.
            eapply reachable_in_dom in Hc; try eassumption. destruct Hc as [v1' Hgetv1'].
            erewrite alloc_fresh in Hgetv1'; try eassumption. congruence.

            eapply well_formed_respects_heap_env_equiv. eassumption. eassumption.

            eapply Included_trans; [| eapply env_locs_in_dom; eassumption ].
            reflexivity.

            eapply Included_trans. eapply reach'_set_monotonic. eapply env_locs_monotonic.
            eapply occurs_free_Econstr_Included.
            eapply reach'_alloc_set; [| eassumption ].
            eapply Included_trans; [| eapply reach'_extensive ].
            normalize_occurs_free. rewrite env_locs_Union.
            eapply Included_Union_preserv_l.
            rewrite env_locs_FromList; eauto. reflexivity.

          - eapply Hiinv; try eassumption.
            econstructor; eauto.
            now econstructor; eauto.
            econstructor; eauto.
            now econstructor; eauto.
          - simpl. simpl in Hcost. omega.
          - intros i. edestruct (Hstuck1 (i + cost (Econstr x1 t ys1 e1))) as [r' [m' Hstep']].
            inv Hstep'.
            * omega.
            * rewrite Nat.add_sub in Hbs0. repeat subst_exp.
              repeat eexists; eauto.
          - repeat eexists; eauto.
            + eapply Eval_constr_per_cc with (c := c2 + cost (Econstr x2 t ys2 e2))
              ; [ | | | rewrite Nat.add_sub ]; try eassumption.
              simpl. omega.
            + replace c1 with (c1 - cost (Econstr x1 t ys1 e1) + cost (Econstr x1 t ys1 e1))
                by ( simpl in *; omega).
              eapply Hinv; try eassumption. simpl in *. omega.
              replace (cost (Econstr x1 t ys1 e1))
                with (0 + cost_ctx (Econstr_c x1 t ys1 Hole_c)) by (simpl; omega).
              econstructor; eauto. now econstructor; eauto.
              replace (cost (Econstr x2 t ys2 e2)) with (0 + cost_ctx (Econstr_c x2 t ys2  Hole_c)) by (simpl; omega).
              econstructor; eauto. now econstructor; eauto.
            + rewrite cc_approx_val_eq. eapply cc_approx_val_monotonic.
              rewrite <- cc_approx_val_eq. eassumption. simpl in *. omega. }
    Qed.

    (** Projection compatibility *)
    Lemma cc_approx_exp_proj_compat (k : nat) (H1 H2 : heap block) (rho1 rho2 : env) (b : Inj)
          (x1 x2 : var) (t : cTag) (n : N) (y1 y2 : var) (e1 e2 : exp) :

      InvCtxCompat IL1 IL2 (Eproj_c x1 t n y1 Hole_c) (Eproj_c x2 t n y2 Hole_c) e1 e2 ->
      IInvCtxCompat IIL1 IIL2 (Eproj_c x1 t n y1 Hole_c) (Eproj_c x2 t n y2 Hole_c) e1 e2 ->
      InvCostTimeOut IL1 IIL1 (Eproj x1 t n y1 e1) (Eproj x2 t n y2 e2) ->

      (forall j, cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2 y1 y2) ->

      (forall v1 v2,
         k >= cost (Eproj x1 t n y1 e1) ->
         (* allocate a new location for the constructed value *)
         val_loc v1 \subset reach' H1 (env_locs rho1 [set y1]) ->
         val_loc v2 \subset reach' H2 (env_locs rho2 [set y2]) ->

         (forall j, (Res (v1, H1)) ≺ ^ (k - cost (Eproj x1 t n y1 e1) ; j ; IIG ; IG; b) (Res (v2, H2))) ->
         (forall j, (e1, M.set x1 v1 rho1, H1) ⪯ ^ (k - cost (Eproj x1 t n y1 e1) ; j ; IIL2 ; IIG ; IL2 ; IG) (e2, M.set x2 v2 rho2, H2))) ->

      (forall j, (Eproj x1 t n y1 e1, rho1, H1) ⪯ ^ (k ; j ; IIL1 ; IIG ; IL1 ; IG) (Eproj x2 t n y2 e2, rho2, H2)).
    Proof with (now eauto with Ensembles_DB).
      intros Hinv Hiinv Hbase Hall Hpre j b1 b2 H1' H2' rho1' rho2' v1 c1 m1
             Heq1' Hinj1 Heq2' Hinj2 HII Hleq1 Hstep1 Hstuck. inv Hstep1.
      (* Timeout! *)
      - { simpl in Hcost. exists OOT, c1. eexists. exists id. repeat split.
          - econstructor. simpl; omega. reflexivity.
          (* - eapply injective_subdomain_Empty_set. *)
          - eapply Hbase; eauto.
          - now rewrite cc_approx_val_eq. }
      (* Termination *)
      - { pose (cost1 := cost (Eproj x1 t n y1 e1)).
          pose (cost2 := cost (Eproj x2 t n y2 e2)).
          assert (Hall' := Hall).

          eapply (cc_approx_var_env_heap_env_equiv
                    _ _
                    (occurs_free (Eproj x1 t n y1 e1))
                    (occurs_free (Eproj x2 t n y2 e2)) _ (S j)) in Hall;
          [| eassumption | eassumption | eassumption | eassumption
           | normalize_occurs_free; now eauto with Ensembles_DB
           | normalize_occurs_free; now eauto with Ensembles_DB ].
          edestruct Hall as [l2 [Hget' Hcc']]; eauto.
          destruct l2 as [l' | l' f]; [| contradiction ].
          simpl in Hcc'. rewrite Hgetl in Hcc'.
          destruct (get l' H2') as [[ t2 vs' | | ] | ] eqn:Hgetl';
            (try destruct Hcc' as [Hteq Hcc']); try contradiction.

          edestruct heap_env_equiv_env_get as [l1 [Hgetl1 Hres1]]; [ now apply Hgety | | | ].
          symmetry. eassumption. now eauto.
          edestruct heap_env_equiv_env_get as [l2 [Hgetl2 Hres2]]; [ now apply Hget' | | | ].
          symmetry. eassumption. now eauto.

          edestruct (Hall' (S j))  as [l2' [Hgetl2'' Hcc]]; eauto. repeat subst_exp.

          assert (Hres1' := Hres1). assert (Hres2' := Hres2). rewrite res_equiv_eq in Hres1, Hres2.
          destruct l1 as [l1 |]; try contradiction.
          destruct l2' as [l2 |]; try contradiction.

          simpl in Hres1, Hres2. rewrite Hgetl in Hres1. rewrite Hgetl' in Hres2.
          destruct (get l1 H1) as [bl1 |] eqn:Hgetl1'; (try destruct Hres1 as [Hb1 Hres1]); try contradiction.
          destruct (get l2 H2) as [bl2 |] eqn:Hgetl2'; (try destruct Hres2 as [Hb2 Hres2]); try contradiction.
          destruct bl1 as [t1 vs1 | | ]; try contradiction.
          destruct bl2 as [t2' vs2 | | ]; try contradiction.
          destruct Hres1 as [Hteq Hallvs1]; subst. destruct Hres2 as [Hteq' Hallvs2]; subst.

          simpl in Hcc. rewrite Hgetl1' in Hcc. rewrite Hgetl2' in Hcc.
          destruct Hcc as [Hbeq [Henv Hcc]]. subst.

          edestruct (Forall2_nthN _ _ _ _ _ Hallvs1 Hnth) as [v1' [Hnth' Hv1]].
          edestruct (Forall2_nthN
                       (fun l1 l2 => cc_approx_val k j IIG IG b (Res (l1, H1)) (Res (l2, H2))) vs1)
            as [l3' [Hnth'' Hval']]; eauto.
          (* eapply Hcc. unfold cost1. simpl. simpl in Hcost. omega. *)

          edestruct (Forall2_nthN (fun v1 v2 : value => (v1, H2) ≈_( b2, id) (v2, H2'))) as [v2' [Hnth2' Hv2]].
          eapply Forall2_symm_strong; [| eassumption ]. intros. now symmetry; eauto. eassumption.

          edestruct Hpre with (c1 := c1 - cost1) (v1 := v1') as [v2 [c2 [m2 [b' [Hstep [HS Hres]]]]]];
            [ | | | | | | | | | | eassumption | | ].
          - simpl in *. omega.
          - intros x Hin. eapply Included_post_reach'.
            rewrite env_locs_Singleton; [| eassumption ]. simpl. rewrite post_Singleton; [| eassumption ].
            simpl. eapply In_Union_list. eapply in_map. eapply nthN_In. eassumption.
            eassumption.
          - intros x Hin. eapply Included_post_reach'.
            rewrite env_locs_Singleton; [| eassumption ]. simpl. rewrite post_Singleton; [| eassumption ].
            simpl. eapply In_Union_list. eapply in_map. eapply nthN_In. eassumption.
            eassumption.
          - intros j'.

            edestruct (Hall' (j' + 1))  as [l2'' [Hgetl2'' Hcc'']]; eauto. repeat subst_exp.
            simpl in Hcc''. rewrite Hgetl1' in Hcc''. rewrite Hgetl2' in Hcc''.
            destruct Hcc'' as [_ [Henv' Hcc'']].

            edestruct (Forall2_nthN
                         (fun l1 l2 => cc_approx_val k j' IIG IG b (Res (l1, H1)) (Res (l2, H2))) vs1)
              as [v2'' [Hnth2 Hv2']]; eauto.
            eapply Hcc''. omega.

            repeat subst_exp.
            eapply cc_approx_val_monotonic. rewrite <- cc_approx_val_eq. eassumption. omega.

          - eapply heap_env_equiv_set.
            eapply heap_env_equiv_antimon. eassumption.
            repeat subst_exp. normalize_occurs_free... symmetry. eassumption.
          - eapply injective_subdomain_antimon. eassumption.

            rewrite (reach'_idempotent H1' (env_locs rho1' (occurs_free (Eproj x1 t n y1 e1)))).
            eapply reach'_set_monotonic.
            eapply Included_trans.
            eapply env_locs_set_Inlcuded'.
            eapply Union_Included.

            eapply Included_trans; [| eapply Included_post_reach' ].
            normalize_occurs_free. rewrite env_locs_Union, post_Union. eapply Included_Union_preserv_l.
            rewrite env_locs_Singleton; eauto. simpl. erewrite post_Singleton; eauto.
            simpl. eapply In_Union_list. eapply in_map. eapply nthN_In. eassumption.

            eapply Included_trans; [| eapply reach'_extensive ].
            eapply env_locs_monotonic. normalize_occurs_free...
          - eapply heap_env_equiv_set.
            eapply heap_env_equiv_antimon. eassumption.
            normalize_occurs_free...
            repeat subst_exp. eassumption.
          - eapply injective_subdomain_antimon. eassumption.

            rewrite (reach'_idempotent H2 (env_locs rho2 (occurs_free (Eproj x2 t n y2 e2)))).
            eapply reach'_set_monotonic.
            eapply Included_trans.
            eapply env_locs_set_Inlcuded'.
            eapply Union_Included.

            eapply Included_trans; [| eapply Included_post_reach' ].
            normalize_occurs_free. rewrite env_locs_Union, post_Union. eapply Included_Union_preserv_l.
            rewrite env_locs_Singleton; eauto. simpl. erewrite post_Singleton; eauto.
            simpl. eapply In_Union_list. eapply in_map. eapply nthN_In. eassumption.

            eapply Included_trans; [| eapply reach'_extensive ].
            eapply env_locs_monotonic. normalize_occurs_free...
          - eapply Hiinv; try eassumption.
            econstructor; eauto.
            now econstructor; eauto.
            econstructor; eauto.
            now econstructor; eauto.
          - unfold cost1. simpl. omega.
          - intros i. edestruct (Hstuck (i + cost1)) as [r' [m' Hstep']].
            inv Hstep'.
            * unfold cost1 in Hcost0. omega.
            * simpl in Hbs0. rewrite Nat.add_sub in Hbs0.
              repeat subst_exp.
              do 2 eexists. eassumption.
          - repeat eexists; eauto. eapply Eval_proj_per_cc with (c := c2 + cost2); try eassumption.
            unfold cost2. simpl; omega. simpl. rewrite Nat.add_sub.
            eassumption.
            replace c1 with (c1 - cost1 + cost1) by (unfold cost1; simpl in *; omega).
            eapply Hinv; try eassumption. simpl in *. omega.
            replace cost1 with (0 + cost_ctx (Eproj_c x1 t n y1 Hole_c)) by (unfold cost1; simpl; omega).
            econstructor; eauto. now econstructor; eauto.
            replace cost2 with (0 + cost_ctx (Eproj_c x2 t n y2 Hole_c)) by (unfold cost2; simpl; omega).
            econstructor; eauto. now econstructor; eauto.
            rewrite cc_approx_val_eq in *.
            eapply cc_approx_val_monotonic. eassumption.
            unfold cost1, cost2. simpl. simpl in Hcost. omega. }
    Qed.

    (** Case compatibility *)
    Lemma cc_approx_exp_case_nil_compat (k j : nat) (H1 H2 : heap block) (rho1 rho2 : env) (x1 x2 : var) :
      InvCostTimeOut IL1 IIL1 (Ecase x1 []) (Ecase x2 []) ->
      (Ecase x1 [], rho1, H1) ⪯ ^ (k ; j ; IIL1; IIG ; IL1 ; IG) (Ecase x2 [], rho2, H2).
    Proof.
      intros Hbase b1 b2 H1' H2' rho1' rho2' v1 c1 m1 Heq1 Hinj1 Heq2 Hinj2 HII Hleq1 Hstep1 Hns. inv Hstep1.
      (* Timeout! *)
      - { simpl in Hcost. exists OOT, c1. eexists. eexists id. repeat split.
          - econstructor. simpl; omega. reflexivity.
          - eapply Hbase; eassumption.
          - now rewrite cc_approx_val_eq. }
      (* Termination *)
      - { simpl in Htag. discriminate. }
    Qed.

    Lemma Forall2_findtag {A B} c Pats1 Pats2 (e : A) (P : A -> B  -> Prop) :
      findtag Pats1 c = Some e ->
      Forall2 (fun ce1 ce2 =>
                 let '(c1, e1) := ce1 in
                 let '(c2, e2) := ce2 in
                 c1 = c2 /\ P e1 e2) Pats1 Pats2 ->
      exists e', findtag Pats2 c = Some e' /\ P e e'.
    Proof.
      intros Hf Hall. revert e Hf. induction Hall; intros e Hf.
      - inv Hf.
      - destruct x as [c1 e1]. destruct y as [c2 e2]. simpl in *.
        destruct H as [Heq1 HP]; subst.
        destruct (M.elt_eq c2 c); eauto. inv Hf.
        eexists; split; eauto.
    Qed.

    Lemma cc_approx_exp_case_compat (k j : nat) (b : Inj)
          (H1 H2 : heap block) (rho1 rho2 : env) (x1 x2 : var) (Pats1 Pats2 : list (cTag * exp)) :
      InvCostTimeOut IL1 IIL1 (Ecase x1 Pats1) (Ecase x2 Pats2) ->
      IInvCaseCompat IIL1 IILe x1 x2 Pats1 Pats2 ->
      InvCaseCompat IL1 ILe x1 x2 Pats1 Pats2 ->

      cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2 x1 x2 ->

      Forall2 (fun ce1 ce2 =>
                 let '(c1, e1) := ce1 in
                 let '(c2, e2) := ce2 in
                 c1 = c2 /\
                 (k >= cost (Ecase x1 Pats1) ->
                 (e1, rho1, H1) ⪯ ^ (k - cost (Ecase x1 Pats1); j; IILe e1 e2 ; IIG ; ILe e1 e2 ; IG)
                 (e2, rho2, H2))) Pats1 Pats2 ->

      (Ecase x1 Pats1, rho1, H1) ⪯ ^ (k ; j ; IIL1 ; IIG ; IL1 ; IG) (Ecase x2 Pats2, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hbase Hiinvh Hinvh Hvar Hall b1 b2 H1' H2' rho1' rho2'
             v1 c1 m1 Heq1 Hinj1 Heq2 Hinj2 HII Hleq1 Hstep1 Hstuck1.
      inv Hstep1.
      (* Timeout! *)
      - { simpl in Hcost. exists OOT, c1. eexists. exists id. repeat split.
          - econstructor. simpl; omega. reflexivity.
          - eapply Hbase; eassumption.
          - now rewrite cc_approx_val_eq. }
      - { pose (cost1 := cost (Ecase x1 Pats1)).
          pose (cost2 := cost (Ecase x2 Pats2)).
          eapply (cc_approx_var_env_heap_env_equiv
                    _ _
                    (occurs_free (Ecase x1 Pats1))
                    (occurs_free (Ecase x2 Pats2))) in Hvar;
          [| eassumption | eassumption | eassumption | eassumption
           | | ].
          edestruct Hvar as [l' [Hgety' Hcc]]; eauto.
          destruct l' as [l' |l' f ]; [| contradiction ].
          simpl in Hcc. rewrite Hgetl in Hcc.
          destruct (get l' H2') as [[ t' vs' | | ] |] eqn:Hgetl';
            (try destruct Hcc as [Hbeq Hcc]); try contradiction.
          destruct Hcc as [Heq Hall']; subst. simpl in Hall', Hcost.
          edestruct (@Forall2_findtag exp exp) with
          (P := fun e1 e2 => k >= cost (Ecase x1 Pats1) ->
                          (e1, rho1, H1) ⪯ ^ (k - cost (Ecase x1 Pats1); j; IILe e1 e2 ; IIG ; ILe e1 e2; IG)
                          (e2, rho2, H2)) as [e2 Hcc].
          - eassumption.
          - eapply Forall2_monotonic; [| eassumption ]. intros [c e1] [c' e2] H. eassumption.
          - destruct Hcc as [Hf2 Hcc].
            edestruct Hcc with (c1 := c1 - cost1) as [v2 [c2 [m2 [b' [Hstep [HS Hres]]]]]].
            + simpl in *. omega.
            + eapply heap_env_equiv_antimon. now eapply Heq1.
              eapply occurs_free_Ecase_Included. eapply findtag_In. eassumption.
            + eapply injective_subdomain_antimon. eassumption.
              eapply reach'_set_monotonic. eapply env_locs_monotonic.
              eapply occurs_free_Ecase_Included. eapply findtag_In. eassumption.
            + eapply heap_env_equiv_antimon. now eapply Heq2.
              eapply occurs_free_Ecase_Included. eapply findtag_In. eassumption.
            + eapply injective_subdomain_antimon. eassumption.
              eapply reach'_set_monotonic. eapply env_locs_monotonic.
              eapply occurs_free_Ecase_Included. eapply findtag_In. eassumption.
            + eapply Hiinvh. eapply findtag_In. eassumption.
              eapply findtag_In. eassumption. eassumption.
            + unfold cost1. simpl; omega.
            + eassumption.
            + intros i. edestruct (Hstuck1 (i + cost1)) as [r' [m'' Hstep']].
              inv Hstep'.
              * exists OOT. eexists. econstructor; eauto. unfold cost1 in Hcost0.
               omega.
              * repeat subst_exp.
                simpl in Hbs0. rewrite Nat.add_sub in Hbs0.
                do 2 eexists. eassumption.
            + repeat eexists; eauto.
              * eapply Eval_case_per_cc with (c := c2 + cost2)
                ; [ | | | | rewrite Nat.add_sub ]; try eassumption.
                simpl in *. omega.
              * replace c1 with (c1 - cost1 + cost1) by (unfold cost1; simpl in *; omega).
                eapply Hinvh. eapply findtag_In. eassumption.
                eapply findtag_In. eassumption. simpl in *. omega. eassumption.
              * rewrite cc_approx_val_eq. eapply cc_approx_val_monotonic.
                rewrite <- cc_approx_val_eq. eassumption. unfold cost1. simpl. omega.
          - now constructor.
          - now constructor. }
    Qed.

    (** Halt compatibility *)
    Lemma cc_approx_exp_halt_compat (k j : nat) (H1 H2 : heap block) (rho1 rho2 : env) (b : Inj)
          (x1 x2 : var) :
      InvCostTimeOut IL1 IIL1 (Ehalt x1) (Ehalt x2) ->
      InvCostBase IL1 IIL1 (Ehalt x1) (Ehalt x2) ->

      cc_approx_var_env k j IIG IG b H1 rho1 H2 rho2 x1 x2 ->

      (Ehalt x1, rho1, H1) ⪯ ^ (k ; j ; IIL1 ; IIG ; IL1; IG) (Ehalt x2, rho2, H2).
    Proof.
      intros Hoot Hbase Hvar b1 b2 H1' H2' rho1' rho2' v1 c1 m1 Heq1 Hinj1
             Heq2 Hinj2 Hleq1 HII Hstep1 Hstuck1.
      assert (Hvar' := Hvar).
      inv Hstep1.
      - (* Timeout! *)
        { simpl in Hcost. exists OOT, c1. eexists. exists id. repeat split.
          - econstructor; eauto.
          - eapply Hoot; try eassumption.
          - now rewrite cc_approx_val_eq. }
      - pose (cost1 := cost (Ehalt x1)).
        pose (cost2 := cost (Ehalt x2)).
        eapply (cc_approx_var_env_heap_env_equiv
                  _ _
                  (occurs_free (Ehalt x1))
                  (occurs_free (Ehalt x2))) in Hvar;
          [| eassumption | eassumption | eassumption | eassumption | now constructor | now constructor ].
        edestruct Hvar as [l' [Hgety' Hcc]]; eauto.
        eexists. exists c1. eexists. exists (b2 ∘ b ∘ b1). repeat eexists.
        * eapply Eval_halt_per_cc. simpl. simpl in Hcost. omega. eassumption.
          reflexivity.
        * eapply Hbase; try eassumption.
        * rewrite cc_approx_val_eq in *.
          eapply cc_approx_val_monotonic. eassumption.
          omega.
    Qed.

    (* TODO move *)

    Lemma heap_env_approx_binding_in_map S S' b1 H1 rho1 b2 H2 rho2 :
      heap_env_approx S' (b1, (H1, rho1)) (b2, (H2, rho2)) ->
      S \subset S' ->
      binding_in_map S rho1 -> binding_in_map S rho2.
    Proof.
      intros Hap Hsub Hbin x Hiny. edestruct Hbin as [v1 Hgetx]; eauto.
      edestruct Hap as [l1' [Hr2 Hres1]]; eauto.
    Qed.

  Lemma heap_env_equiv_binding_in_map S S' b1 H1 rho1 b2 H2 rho2 :
    S' |- (H1, rho1) ⩪_( b1, b2) (H2, rho2) ->
    S \subset S' ->
    binding_in_map S rho1 -> binding_in_map S rho2.
  Proof.
    intros [Henv1 Henn2] Hin Hbin; eapply heap_env_approx_binding_in_map; eauto.
  Qed.

    (** Abstraction compatibility *)
  Lemma cc_approx_exp_fun_compat (k j : nat) rho1 rho2 H1 H2 B1 e1 B2 e2 :
      InvCtxCompat IL1 IL2 (Efun1_c B1 Hole_c) (Efun1_c B2 Hole_c) e1 e2 ->
      IInvCtxCompat_Funs IIL1 IIL2 B1 B2 e1 e2 ->
      InvCostTimeOut_Funs IL1 IIL1 B1 e1 B2 e2 ->

      well_formed (reach' H1 (env_locs rho1 (occurs_free (Efun B1 e1)))) H1 ->
      (env_locs rho1 (occurs_free (Efun B1 e1))) \subset dom H1 ->

      binding_in_map (occurs_free_fundefs B1) rho1 ->

      (forall H1' H1'' rho1' rho_clo env_loc,
         k >= cost (Efun B1 e1) ->
         restrict_env (fundefs_fv B1) rho1 = rho_clo ->
         alloc (Env rho_clo) H1 = (env_loc, H1') ->

         def_closures B1 B1 rho1 H1' (Loc env_loc) = (H1'', rho1') ->

         (e1, rho1', H1'') ⪯ ^ (k - cost (Efun B1 e1) ; j ; IIL2 ; IIG ; IL2 ; IG)
         (e2, def_funs B2 B2 rho2, H2)) ->

      (Efun B1 e1, rho1, H1) ⪯ ^ (k ; j ; IIL1 ; IIG ; IL1 ; IG) (Efun B2 e2, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hinv Hiinv Hbase Hwf Hdom Hbin Hpre b1 b2 H1' H2' rho1' rho2' v1 c1
             m1 Heq1 Hinj1 Heq2 Hinj2 HII Hleq1 Hstep1 Hstuck1.
      inv Hstep1.
      (* Timeout! *)
      - { simpl in Hcost. exists OOT, 0.
          - eexists. eexists id. repeat split. econstructor. simpl.
            omega. reflexivity.
            eapply Hbase; eassumption.
            now rewrite cc_approx_val_eq. }
      (* Termination *)
      - { destruct (alloc (Env (restrict_env (fundefs_fv B1) rho1)) H1) as [env_loc H1''] eqn:Ha'.
          destruct (def_closures B1 B1 rho1 H1'' (Loc env_loc)) as [H3' rho3] eqn:Hdef3.
          assert (Hlocs : env_locs rho1' (occurs_free (Efun B1 e1)) \subset dom H1').
          { eapply env_locs_in_dom. eassumption. eassumption. }
          assert (Hwf2' : well_formed (reach' H1' (env_locs rho1' (occurs_free (Efun B1 e1)))) H1').
          { eapply well_formed_respects_heap_env_equiv. eassumption.
            eassumption. }
        edestruct heap_env_equiv_def_funs_strong
          with (H1 := H1'')
                 (H2 := H')
                 (S := occurs_free (Efun B1 e1) :|: name_in_fundefs B1) (B := B1)
                 (B0 := B1)
                 (β1 := b1 {lenv ~> env_loc})
            as [b1' Hs]; try eassumption.
          - rewrite <- well_formed_reach_alloc_same.

            eapply well_formed_alloc; try eassumption; simpl.  eapply well_formed_antimon; try eassumption.
            eapply reach'_set_monotonic. eapply env_locs_monotonic...

            eapply Included_trans. eapply Included_trans.
            eapply env_locs_monotonic with (S2 := Full_set _)...
            eapply restrict_env_env_locs. eapply restrict_env_correct.
            now eapply fundefs_fv_correct.
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic.
            normalize_occurs_free...

            eapply well_formed_antimon; try eassumption.
            eapply reach'_set_monotonic. eapply env_locs_monotonic...
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic...

            eassumption.
          - rewrite <- well_formed_reach_alloc_same.

            eapply well_formed_alloc; try eassumption; simpl.  eapply well_formed_antimon; try eassumption.
            eapply reach'_set_monotonic. eapply env_locs_monotonic...

            eapply Included_trans. eapply Included_trans.
            eapply env_locs_monotonic with (S2 := Full_set _)...
            eapply restrict_env_env_locs. eapply restrict_env_correct.
            now eapply fundefs_fv_correct.
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic.
            normalize_occurs_free...

            eapply well_formed_antimon; try eassumption.
            eapply reach'_set_monotonic. eapply env_locs_monotonic...
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic...

            eassumption.
          - rewrite HL.alloc_dom; [| eassumption ].
            eapply Included_trans; [| eapply Included_Union_preserv_r; reflexivity ].
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic...
          - rewrite HL.alloc_dom; [| eassumption ].
            eapply Included_trans; [| eapply Included_Union_preserv_r; reflexivity ].
            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic...
          - erewrite gas; eauto.
          - erewrite gas; eauto.
          - eapply Included_trans. eapply Included_trans.
            eapply env_locs_monotonic with (S2 := Full_set _)...
            eapply restrict_env_env_locs. eapply restrict_env_correct.
            now eapply fundefs_fv_correct.
            eapply Included_trans; [| now apply reach'_extensive ].
            normalize_occurs_free. eapply env_locs_monotonic.
            rewrite !Setminus_Union_distr. eapply Included_Union_preserv_l.
            eapply Included_Union_preserv_l. rewrite Setminus_Disjoint. reflexivity.
            eapply Disjoint_sym.
            eapply occurs_free_fundefs_name_in_fundefs_Disjoint.
          - eapply Included_trans. eapply Included_trans.
            eapply env_locs_monotonic with (S2 := Full_set _)...
            eapply restrict_env_env_locs. eapply restrict_env_correct.
            now eapply fundefs_fv_correct.
            eapply Included_trans; [| now apply reach'_extensive ].
            normalize_occurs_free. eapply env_locs_monotonic.
            rewrite !Setminus_Union_distr. eapply Included_Union_preserv_l.
            eapply Included_Union_preserv_l. rewrite Setminus_Disjoint. reflexivity.
            eapply Disjoint_sym.
            eapply occurs_free_fundefs_name_in_fundefs_Disjoint.
          - normalize_occurs_free. rewrite !Setminus_Union_distr.
            do 2 eapply Included_Union_preserv_l.
            rewrite Setminus_Disjoint. reflexivity. eapply Disjoint_sym.
            eapply occurs_free_fundefs_name_in_fundefs_Disjoint.
          - rewrite res_equiv_eq. simpl. split.

            rewrite extend_gss. reflexivity.

            erewrite !gas; eauto. simpl.

            eapply heap_env_equiv_antimon.
            eapply heap_env_equiv_restrict_env with (S' := occurs_free_fundefs B1).

            eapply heap_env_equiv_weaking_cor.
            eapply well_formed_respects_heap_env_equiv. eassumption.
            symmetry. eassumption.
            eassumption.

            eassumption.

            eapply env_locs_in_dom. eassumption. eassumption.

            eapply heap_env_equiv_rename_ext. eassumption. reflexivity.

            eapply f_eq_subdomain_extend_not_In_S_r.
            intros Hc. eapply reachable_in_dom in Hc. destruct Hc as [lv Heq].
            erewrite alloc_fresh in Heq; eauto. congruence.

            eassumption.
            eassumption. reflexivity.

            eapply HL.alloc_subheap. eassumption.
            eapply HL.alloc_subheap. eassumption.
            normalize_occurs_free...
            eapply restrict_env_correct. now eapply fundefs_fv_correct.
            eapply restrict_env_correct. now eapply fundefs_fv_correct.
            reflexivity.

          - rewrite <- well_formed_reach_alloc_same; [| | | eassumption ].
            eapply injective_subdomain_extend.
            eapply injective_subdomain_antimon. eassumption.
            eapply reach'_set_monotonic. eapply env_locs_monotonic...
            intros Hc.

            assert (Hinim : env_loc \in
                            reach' H1 (env_locs rho1 (occurs_free (Efun B1 e1)))).
            { erewrite <- image_id with (S := reach' H1 _).
              rewrite heap_env_equiv_image_reach; [| eassumption ].
              eapply image_monotonic; [| eassumption ].
              eapply Included_trans. eapply Setminus_Included.
              eapply reach'_set_monotonic. eapply env_locs_monotonic... }

            eapply reachable_in_dom in Hinim. destruct Hinim as [lv Hgetl].
            erewrite alloc_fresh in Hgetl; eauto. congruence. eassumption.
            eassumption.

            eapply well_formed_antimon; [| eassumption ].
            eapply reach'_set_monotonic. eapply env_locs_monotonic...

            eapply Included_trans; [| eassumption ]. eapply env_locs_monotonic...
          - eapply heap_env_equiv_antimon.
            eapply heap_env_equiv_weaking_cor.
            eapply well_formed_respects_heap_env_equiv. eassumption.
            symmetry. eassumption. eassumption.
            eassumption.

            eapply env_locs_in_dom. eassumption. eassumption.

            eapply heap_env_equiv_rename_ext. eassumption. reflexivity.

            eapply f_eq_subdomain_extend_not_In_S_r.
            intros Hc. eapply reachable_in_dom in Hc. destruct Hc as [lv Heq].
            erewrite alloc_fresh in Heq; eauto. congruence.

            eassumption.
            eassumption. reflexivity.

            eapply HL.alloc_subheap. eassumption.
            eapply HL.alloc_subheap. eassumption.
            now eauto with Ensembles_DB.
          - rewrite Hfuns, Hdef3 in Hs.
            destruct Hs as [Heq [Hfeq' [Hwf1 [Hwf2 [Henv1 [Henv2 Hinj]]]]]].
            edestruct Hpre as [v2 [c2 [m2 [b2' [Hstep [HS Hval]]]]]]
            ; [ | | | now apply Hdef3 | |
                | | | | | eassumption | | ].
            + simpl in *. omega.
            + reflexivity.
            + eassumption.
            + eapply heap_env_equiv_antimon. eassumption.
              normalize_occurs_free. rewrite <- Union_assoc. eapply Included_Union_preserv_r.
              eapply Included_Union_Setminus.
              now eauto with typeclass_instances.
            + eapply injective_subdomain_antimon. eassumption.
              eapply Included_Union_preserv_r. eapply reach'_set_monotonic.
              normalize_occurs_free. eapply env_locs_monotonic. rewrite <- Union_assoc.
              eapply Included_Union_preserv_r.
              eapply Included_Union_Setminus. now eauto with typeclass_instances.
            + eapply heap_env_equiv_def_funs'.
              eapply heap_env_equiv_antimon. eassumption. normalize_occurs_free...
            + eapply injective_subdomain_antimon. eassumption.
              eapply reach'_set_monotonic.
              eapply Included_trans. eapply def_funs_env_loc.
              eapply env_locs_monotonic. normalize_occurs_free...
            + eapply Hiinv; try eassumption. subst.
              eapply heap_env_equiv_binding_in_map. eassumption. normalize_occurs_free...
              eassumption.
              econstructor; eauto. now econstructor.
              econstructor; eauto. now econstructor.
           + simpl; omega.
           + intros i. edestruct (Hstuck1 (i + cost (Efun B1 e1))) as [r' [m' Hstep']].
             inv Hstep'.
             * omega.
             * rewrite Nat.add_sub in Hbs0. repeat subst_exp.
               repeat eexists. eassumption.
           + repeat eexists.
             * eapply Eval_fun_per_cc with (c := c2 + cost_cc (Efun B2 e2));
                 try eassumption.
               simpl. omega. reflexivity. simpl.
               rewrite Nat.add_sub. eassumption.
             * simpl.
               replace c1 with (c1 - (cost (Efun B1 e1)) + (cost (Efun B1 e1)))
                 by (simpl in *; omega).
               eapply Hinv; try eassumption.
               simpl. omega.
               replace (cost (Efun B1 e1)) with (0 + cost_ctx (Efun1_c B1 Hole_c))
                 by (simpl; omega).
               econstructor; eauto. now econstructor.
               replace 1 with (0 + cost_ctx_cc (Efun1_c B2 Hole_c)) by (simpl; omega).
               econstructor; eauto. now econstructor.
             * rewrite cc_approx_val_eq in *.
               eapply cc_approx_val_monotonic. eassumption.
               simpl. simpl in Hcost. omega. }
    Qed.

    Context (ILC : exp_ctx -> Inv).
    Context (IILC : exp_ctx -> IInv).

    Lemma cc_approx_exp_right_ctx_compat
          (k j : nat) rho1 rho2 rho2' H1 H2 H2' e1 C e2 c' :
      (* InvCostTimeOut IL1 IIL1 e1 (C |[ e2 ]|) -> *)
      InvCostTimeOut' IL1 IIL1 (cost_alloc_ctx_CC C) e1 (C |[ e2 ]|) ->
      InvCtxCompat_r IL1 IL2 C e1 e2 ->
      IInvCtxCompat_r IIL1 IIL2 C e1 e2 ->
      cost e1 <= max (cost_ctx_full_cc C) (cost_cc e2) ->

      well_formed (reach' H2 (env_locs rho2 (occurs_free (C |[ e2 ]|)))) H2 ->
      (env_locs rho2 (occurs_free (C |[ e2 ]|))) \subset dom H2 ->

      ctx_to_heap_env_CC C H2 rho2 H2' rho2' c' ->
      (e1, rho1, H1) ⪯ ^ (k; j; IIL2 ; IIG ; IL2 ; IG) (e2, rho2', H2') ->
      (e1, rho1, H1) ⪯ ^ (k; j; IIL1 ; IIG ; IL1 ; IG) (C |[ e2 ]|, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hoot Hinv Hiinv Hyp Hwf2 Henv2 Hctx Hpre.
      intros b1 b2 H1' H3 rho1' rho3 v1 k1 m1 Heq1 Hinj1 Heq2 Hinj2
             HII Hleq1 Hstep1 Hstuck1.
      edestruct ctx_to_heap_env_determistic
        as [H3' [rho3' [b' [Heq' [Hinj Heval]]]]];
        try eassumption.
      assert (Heq : c' = cost_ctx_full_cc C).
      { eapply ctx_to_heap_env_CC_cost; eauto. }

      eapply Nat_as_DT.max_le in Hyp. destruct (lt_dec k1 (cost e1)).
      - destruct (lt_dec k1 (cost_ctx_full_cc C)).
        + destruct Hstep1; try omega.
          edestruct big_step_GC_cc_OOT_leq as [m1 [Hleq Hbs']]. eassumption.
          subst. eassumption.
          eexists OOT, c. eexists. exists id.
          split.
          eassumption.
          split. eapply Hoot; eassumption.
          now rewrite cc_approx_val_eq.
        + destruct Hyp.
          * omega.
          * destruct Hstep1; try omega.
            eexists OOT, c. exists (size_heap H3'). exists id.
            split.
            replace c with (c - c' + c') by omega.
            eapply ctx_to_heap_env_big_step_compose. eassumption. subst.
            econstructor. subst. omega.
            reflexivity. split.
            erewrite ctx_to_heap_env_CC_size_heap with (H2 := H3'); [| eassumption ].
            eapply Hoot. eassumption. eassumption.
            reflexivity.
            now rewrite cc_approx_val_eq.
      - eapply Hpre in Hstep1; try eassumption.
        edestruct Hstep1 as [r1 [c3 [m2 [b'' [Hstep2 [Hinv' Hccr]]]]]];
          try eassumption.
        + eexists r1, (c3 + c'), m2, b''. split; [| split ]; try eassumption.
          * eapply ctx_to_heap_env_big_step_compose; try eassumption.
          * eapply Hinv with (c' := c'); eauto.
            omega.
        + eapply Hiinv. eassumption. eassumption.

    Qed.

    (* InvCostTimeOut IL1 IIL1 e1 (C |[ e2 ]|) -> *)
      (* InvCtxCompat_r IL1 IL2 C e1 (C' |[ e2 ]|) -> *)
      (* IInvCtxCompat_r IIL1 IIL2 C e1 (C' |[ e2 ]|) -> *)
      (* cost e1 <= max (cost_ctx_full_cc C) (cost_ctx_full_cc C' + cost_cc e2) -> *)

      (* well_formed (reach' H2 (env_locs rho2 (occurs_free (C |[ C' |[ e2 ]| ]|)))) H2 -> *)
      (* (env_locs rho2 (occurs_free (C |[ C' |[ e2 ]| ]|))) \subset dom H2 -> *)

      (* ctx_to_heap_env_CC C H2 rho2 H2' rho2' c' -> *)

      (* (e1, rho1, H1) ⪯ ^ (k; j; IIL2 ; IIG ; IL2 ; IG) (C' |[ e2 ]|, rho2', H2') -> *)
      (* (e1, rho1, H1) ⪯ ^ (k; j; IIL1 ; IIG ; IL1 ; IG) (C |[ C' |[ e2 ]| ]|, rho2, H2). *)

    (** Application compatibility *)
    Lemma cc_approx_exp_ctx_app_compat (k j : nat) (b : Inj) (H1 H2 H2' : heap block)
          (rho1 rho2 rho2' : env) (f1 : var) (xs1 : list var)
          (f2 f2' Γ : var) (xs2 : list var) (t : fTag) C c :
      InvCostTimeOut' IL1 IIL1 (cost_alloc_ctx_CC C) (Eapp f1 t xs1) (C |[ AppClo clo_tag f2 t xs2 f2' Γ ]|) ->
      IInvAppCompat clo_tag IG IL2 IIL2 H1 H2' rho1 rho2' f1 t xs1 f2 xs2 f2' Γ ->

      InvCtxCompat_r IL1 IL2 C (Eapp f1 t xs1) (AppClo clo_tag f2 t xs2 f2' Γ) ->
      IInvCtxCompat_r IIL1 IIL2 C (Eapp f1 t xs1) (AppClo clo_tag f2 t xs2 f2' Γ) ->

      well_formed (reach' H2 (env_locs rho2 (occurs_free (C |[ AppClo clo_tag f2 t xs2 f2' Γ ]|)))) H2 ->
      (env_locs rho2 (occurs_free (C |[ AppClo clo_tag f2 t xs2 f2' Γ ]|))) \subset dom H2 ->

      ~ Γ \in (f2 |: FromList xs2) ->
      ~ f2' \in (f2 |: FromList xs2) ->
      Γ <> f2' ->

      ctx_to_heap_env_CC C H2 rho2 H2' rho2' c ->

      (forall j, cc_approx_var_env k j IIG IG b H1 rho1 H2' rho2' f1 f2) ->
      Forall2 (fun x1 x2 =>
                 forall j, cc_approx_var_env k j IIG IG b H1 rho1 H2' rho2' x1 x2)
              xs1 xs2 ->

      (Eapp f1 t xs1, rho1, H1) ⪯ ^ (k ; j; IIL1 ; IIG
                                     ; IL1
                                     ; IG)
      (C |[ AppClo clo_tag f2 t xs2 f2' Γ ]|, rho2, H2).
    Proof with now eauto with Ensembles_DB.
      intros Hbase Hiinv Hictx Hiictx Hwf Hdom Hnin1 Hnin2 Hneq Hctx Hvar Hall
             b1 b2 H1' H2'' rho1' rho2'' v1 c1 m1 Heq1 Hinj1 Heq2 Hinj2
             HII Hleq1 Hstep1 Hstuck1.

      edestruct ctx_to_heap_env_determistic
        as [H3' [rho3' [b' [Heq' [Hinj Heval]]]]];
        try eassumption.
      assert (Heq : c = cost_ctx_full_cc C).
      { eapply ctx_to_heap_env_CC_cost; eauto. }

      eapply (cc_approx_var_env_heap_env_equiv
                _ _
                (occurs_free (Eapp f1 t xs1))
                (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ)) k j) in Hvar;
          [| eassumption | eassumption | eassumption | eassumption
           | normalize_occurs_free; now eauto with Ensembles_DB
           | unfold AppClo; normalize_occurs_free; now eauto with Ensembles_DB ].
      inv Hstep1.
      (* Timeout! *)
      - { edestruct (Hstuck1 (cost (Eapp f1 t xs1))) as [v1 [m1 Hstep1]].
          inv Hstep1; [ omega | ].
          exists OOT, c1. destruct (lt_dec c1 (cost_ctx_full_cc C)).
          - edestruct big_step_GC_cc_OOT_leq as [m1 [Hleq Hbs']]. eapply Heval.
            eassumption. eexists. exists id.
            split.
            eassumption.
            split. eapply Hbase; eassumption.
            now rewrite cc_approx_val_eq.
          - edestruct Hvar as [l2 [Hget' Hcc]]; eauto.
            simpl cc_approx_val' in Hcc. rewrite Hgetl in Hcc.
            destruct l2 as [l2 | ]; [| contradiction ].
            destruct Hcc as [Hbeq Hcc]; simpl in Hcc.
            destruct (get l2 H3') as [v |] eqn:Hget2; try contradiction.
            destruct v as [ c [| [| B2 f3 ] [| [env_loc |] [|] ] ] | | ]; try contradiction.
            destruct Hcc as [Henv Hcc].
            edestruct Hcc with (vs2 := vs)
              as (xs2' & e2 & rho3'' & Hfind' & Hset' & Hi'); try eassumption.
            reflexivity. clear. now firstorder. symmetry.
            reflexivity. clear. now firstorder.
            reflexivity.
            clear Henv Hcc Hi'.

            replace c1 with (c1 - cost_ctx_full_cc C +  cost_ctx_full_cc C) by omega.

            destruct (lt_dec (c1 - cost_ctx_full_cc C) 1).
            + eexists. exists id. repeat split.
              eapply ctx_to_heap_env_big_step_compose; try eassumption.
              constructor. simpl; omega.
              reflexivity.
              eapply Hbase. eassumption. simpl in *. omega.
              erewrite ctx_to_heap_env_CC_size_heap. reflexivity. eassumption.
              now rewrite cc_approx_val_eq.
            + destruct (lt_dec (c1 - cost_ctx_full_cc C - 1) 1).
              * eexists. exists id. repeat split.
                eapply ctx_to_heap_env_big_step_compose; try eassumption.
                eapply Eval_proj_per_cc. simpl. omega.
                eassumption. eassumption. reflexivity.
                econstructor. simpl in *. omega.
                reflexivity.
                eapply Hbase. eassumption. simpl in *. omega.
                erewrite ctx_to_heap_env_CC_size_heap. reflexivity. eassumption.
                now rewrite cc_approx_val_eq.
              * eexists. exists id. repeat split.
                eapply ctx_to_heap_env_big_step_compose; try eassumption.
                eapply Eval_proj_per_cc. simpl. omega.
                eassumption. eassumption. reflexivity.
                eapply Eval_proj_per_cc. simpl. omega.
                rewrite M.gso. eassumption. intros Heq; subst; eauto.
                eassumption. reflexivity.
                econstructor. simpl in *.
                erewrite <- Forall2_length; [| eassumption ]. omega.
                reflexivity.
                eapply Hbase. eassumption. simpl in *. omega.
                erewrite ctx_to_heap_env_CC_size_heap. reflexivity. eassumption.
                now rewrite cc_approx_val_eq. }

      (* Termination *)
      - { simpl in Hcost.
          assert (Hall1 := Hall).
          eapply Forall2_monotonic_strong
                 with (R' := (fun x1 x2 : var =>
                                forall j : nat,
                                  cc_approx_var_env
                                    k j IIG IG (b' ∘ b ∘ b1)
                                    H1' rho1' H3' rho3' x1 x2))
            in Hall; (* yiiiiiikes *)
            [
            | intros x1 x2 Hin1 Hin2 Hyp j';
              eapply (cc_approx_var_env_heap_env_equiv
                        _ _
                        (occurs_free (Eapp f1 t xs1))
                        (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ))) in Hyp;
              [ now eapply Hyp | eassumption | eassumption | eassumption | eassumption
                | normalize_occurs_free; now eauto with Ensembles_DB
                | unfold AppClo; repeat normalize_occurs_free; rewrite FromList_cons ];
              right; constructor;
              [ right; constructor;
                [ now eauto with Ensembles_DB
                | now intros Hc; inv Hc; eapply Hnin1; eauto ]
              | now intros Hc; inv Hc; eapply Hnin2; eauto ]
            ].
          edestruct (cc_approx_var_env_getlist IIG IG  k j rho1' rho3')
            as [vs2 [Hgetl' Hcc']];
            [ | now eauto |].
          eapply Forall2_monotonic; [| now apply Hall ].
          intros x1 x2 Hcc1. now eapply Hcc1.

          edestruct Hvar as [l2 [Hget' Hcc]]; eauto.
          simpl in Hcc. rewrite Hgetl in Hcc. destruct l2 as [l2 | ]; [| contradiction ].
          destruct Hcc as [Hbeq Hcc]. simpl in Hcc.
          destruct (get l2 H3') as [v |] eqn:Hget2; try contradiction.
          destruct v as [ ? [| [| B2 f3 ] [| [ env_loc' |] [|] ]] | | ]; try contradiction.
          edestruct Hcc
            as (Henv & xs2' & e2 & rho3'' & Hfind' & Hset' & Hi');
            try eassumption.
          reflexivity. clear; now firstorder. reflexivity. clear; now firstorder.
          eapply Forall2_length. eassumption.

          edestruct (live_exists' (env_locs rho3'' (occurs_free e2)) H3')
            as [H3'' [bg Hgc']].
          tci.
          (* edestruct (live'_live_inv (env_locs rho_clo2 (occurs_free e)) b0 H' H'') *)
          (*   as [b'' [Hgc1' [Hfe1 Hfe2]]]; try eassumption. *)
          (* assert (Hgc1 := Hgc1'); *)
          assert (Hgc2 := Hgc').
          (* destruct Hgc1' as [Hseq [Heqgc Hinjgc]].  *)
          destruct Hgc' as  [Hseq' [Heqgc' Hinjgc']].
          edestruct Hi' with (i := k - cost  (Eapp f1 t xs1))
            as [HG [r2 [c2 [m2 [b2' [Hbs2 [HIG  Hcc2]]]]]]];
            [ | | | reflexivity | | |  | |  | | | ]; try eassumption.
          + simpl. omega.
          (* + rewrite compose_id_neut_r. rewrite compose_id_neut_l. reflexivity. *)
          + intros j'. eapply Forall2_monotonic_strong; [| eassumption ].
            intros v v' Hinv1 Hinv2 Heq. rewrite cc_approx_val_eq.
            eapply cc_approx_val_monotonic with (k := k).
            assert (Hrv : val_loc v \subset env_locs rho1' (occurs_free (Eapp f1 t xs1))).
            { normalize_occurs_free. rewrite env_locs_Union.
              eapply Included_Union_preserv_l. rewrite env_locs_FromList.
              simpl. eapply In_Union_list.
              eapply in_map. eassumption. eassumption. }
            assert (Hrv' : val_loc v' \subset
                           env_locs rho3' (occurs_free (AppClo clo_tag f2 t xs2 f2' Γ))).
            { unfold AppClo. repeat normalize_occurs_free.
              rewrite FromList_cons, !Setminus_Union_distr, !env_locs_Union.
              do 2 eapply Included_Union_preserv_r.
              eapply Included_Union_preserv_l. eapply Included_Union_preserv_r.
              rewrite !Setminus_Disjoint.
              rewrite env_locs_FromList.
              simpl. eapply In_Union_list.
              eapply in_map. eassumption. eassumption.
              now eapply Disjoint_Singleton_r; intros Hc; eapply Hnin1; eauto.
              now eapply Disjoint_Singleton_r; intros Hc; inv Hc; eapply Hnin2; eauto. }
            edestruct (cc_approx_var_env_getlist IIG IG  k j' rho1' rho3')
              as [vs2' [Hgetl'' Hcc'']];
              [ | now eauto |].
            eapply Forall2_monotonic; [| now apply Hall ].
            now intros x1 x2 Heq12; eapply Heq12.
            rewrite Hgetl' in Hgetl''. inv Hgetl''.
            edestruct (Forall2_exists _ vs vs2' v Hinv1 Hcc'')
              as [x' [Hinx2 Hr']].
            destruct v; try contradiction.
            apply cc_approx_val_loc_eq in Heq. subst.
            assert (Hr := Hr').
            eapply cc_approx_val_loc_eq in Hr. subst.
            now eauto.
            simpl. omega.

          + rewrite Combinators.compose_id_left, Combinators.compose_id_right.
            reflexivity.

          + clear; now firstorder.

          + eapply heap_env_equiv_heap_equiv_l. eassumption.

          + (* initial after GC *)
            eapply HG; eassumption.
          + simpl. omega.
          + intros i.
            edestruct (Hstuck1 (i + cost (Eapp f1 t xs1))) as [r' [m'' Hstep']].
            inv Hstep'.
            * omega.
            * rewrite Nat.add_sub in Hbs0.
              repeat subst_exp.
              do 2 eexists. eassumption.

          + eexists.
            eexists (c2 + 1 + 1 + cost (Eapp f2' t (Γ :: xs2)) + cost_ctx_full_cc C).
            eexists. exists b2'. repeat split.
            * eapply ctx_to_heap_env_big_step_compose.
              eassumption.
              eapply Eval_proj_per_cc.
              simpl; omega.
              eassumption. eassumption. reflexivity.
              eapply Eval_proj_per_cc. simpl; omega.
              rewrite M.gso. eassumption.
              intros Hc. subst. eapply Hnin2. now left; eauto.
              eassumption. reflexivity. simpl.
              eapply Eval_app_per_cc.
              simpl. omega.
              rewrite M.gso. rewrite M.gss. reflexivity.
              now intros Hc; subst; eauto.
              eassumption.
              simpl. rewrite M.gss.
              rewrite !getlist_set_neq. now rewrite Hgetl'.
              intros Hc. eapply Hnin2. now eauto.
              intros Hc. eapply Hnin1. now eauto.
              now eauto. eassumption. reflexivity. simpl.
              replace (c2 + 1 + 1 + S (S (length xs2)) - 1 - 1 - S (S (length xs2)))  with c2.
              eassumption. omega.
            * replace c1 with (c1 - cost (Eapp f1 t xs1) + cost (Eapp f1 t xs1)) by (simpl in *; omega).
              eapply Hictx.
              eapply Hiinv; try eassumption.
              eapply Hiictx; try eassumption.
              eapply big_step_reach_leq. eassumption.
              simpl. omega. eassumption.
            * rewrite cc_approx_val_eq in *. eapply cc_approx_val_monotonic.
              eassumption. simpl. omega. }
    Qed.

    (* Lemma cc_approx_exp_right_ctx_compat_app *)
    (*       (k j : nat) rho1 rho2 rho2' H1 H2 H2' e1 C C' e2 c' : *)
    (*   (* InvCostTimeOut IL1 IIL1 e1 (C |[ e2 ]|) -> *) *)
    (*   InvCostTimeOut' IL1 IIL1 (cost_alloc_ctx_CC C) e1 (C |[ C' |[ e2 ]| ]|) -> *)
    (*   InvCtxCompat_r IL1 IL2 C e1 (C' |[ e2 ]|) -> *)
    (*   IInvCtxCompat_r IIL1 IIL2 C e1 (C' |[ e2 ]|) -> *)
    (*   cost e1 <= max (cost_ctx_full_cc C) (cost_ctx_full_cc C' + cost_cc e2) -> *)

    (*   well_formed (reach' H2 (env_locs rho2 (occurs_free (C |[ C' |[ e2 ]| ]|)))) H2 -> *)
    (*   (env_locs rho2 (occurs_free (C |[ C' |[ e2 ]| ]|))) \subset dom H2 -> *)

    (*   ctx_to_heap_env_CC C H2 rho2 H2' rho2' c' -> *)

    (*   (e1, rho1, H1) ⪯ ^ (k; j; IIL2 ; IIG ; IL2 ; IG) (C' |[ e2 ]|, rho2', H2') -> *)
    (*   (e1, rho1, H1) ⪯ ^ (k; j; IIL1 ; IIG ; IL1 ; IG) (C |[ C' |[ e2 ]| ]|, rho2, H2). *)
    (* Proof with now eauto with Ensembles_DB.  *)
    (*   intros Hoot Hinv' Hiinv Hyp Hwf2 Henv2 Hctx Hpre. *)
    (*   intros b1 b2 H1' H3 rho1' rho3 v1 k1 m1 Heq1 Hinj1 Heq2 Hinj2 *)
    (*          HII Hleq1 Hstep1 Hstuck1. *)
    (*   edestruct ctx_to_heap_env_determistic_strong *)
    (*     as [H3' [rho3' [b' [Heq' [Hinj [Hwf1 [Hsub1 Heval]]]]]]]; [ | | eapply Hctx | | | ]; *)
    (*     try eassumption. *)

    (*   assert (Heq : c' = cost_ctx_full_cc C). *)
    (*   { eapply ctx_to_heap_env_CC_cost; eauto. }  *)

    (*   eapply Nat_as_DT.max_le in Hyp. destruct (lt_dec k1 (cost e1)).    *)
    (*   - destruct (lt_dec k1 (cost_ctx_full_cc C)). *)
    (*     + destruct Hstep1; try omega. *)
    (*       edestruct big_step_GC_cc_OOT_leq as [m1 [Hleq Hbs']]. eapply Heval. *)
    (*       subst. eassumption.  *)
    (*       eexists OOT, c. eexists. exists id. *)
    (*       split.  *)
    (*       eassumption.  *)
    (*       split. eapply Hoot; eassumption. *)
    (*       now rewrite cc_approx_val_eq.  *)
    (*     + destruct Hyp. *)
    (*       * omega. *)
    (*       * assert (Hand : v1 = OOT).  *)
    (*         { destruct Hstep1; try omega. reflexivity. }  *)
    (*         { eapply Hpre in Hstep1; try eassumption.  *)
    (*           + edestruct Hstep1 as [r1 [c3 [m2 [b''' [Hstep2 [Hinv'' Hccr]]]]]]; *)
    (*               try eassumption. subst. *)

    (*             eexists r1, (c3 + (cost_ctx_full_cc C)), m2, b'''. *)
    (*             split; [| split ]; try eassumption. *)
    (*             * eapply ctx_to_heap_env_big_step_compose; try eassumption. *)
    (*             * eapply Hinv' with (c' := (cost_ctx_full_cc C)); eauto. *)
    (*           + eapply Hiinv. eassumption. eassumption. }  *)
    (*   - eapply Hpre in Hstep1; try eassumption. *)
    (*     edestruct Hstep1 as [r1 [c3 [m2 [b''' [Hstep2 [Hinv'' Hccr]]]]]]; *)
    (*       try eassumption.  *)
    (*     + eexists r1, (c3 + c'), m2, b'''. split; [| split ]; try eassumption. *)
    (*       * eapply ctx_to_heap_env_big_step_compose; try eassumption. *)
    (*       * eapply Hinv' with (c' := c'); eauto. *)
    (*     + eapply Hiinv. eassumption. eassumption.           *)
    (* Qed. *)

  End CompatLemmas.

End Compat.

author: zoep

repo: safe-for-space

save_path: github-repos/coq/zoep-safe-for-space


text:
(* SPDX-License-Identifier: GPL-2.0 *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import MemoryX.
Require Import Events.
Require Import EventsX.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import Locations.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import Errors.
Require Import Op.
Require Import Smallstep.
Require Import AuxLemma.
Require Import AuxStateDataType.
Require Import GenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import Clight.
Require Import CDataTypes.
Require Import CLemmas.
Require Import XOmega.
Require Import ZArith.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import Ctypes.

Require Import AbstractMachine.Spec.
Require Import PageIndex.Code.
Require Import PageIndex.Spec.
Require Import Ident.
Require Import MemRegion.Spec.
Require Import MemRegion.Layer.
Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.

Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.

Section PageIndexProofLow.

  Context `{real_params: RealParams}.
  Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
  Context `{Hmwd: UseMemWithData memb}.

  Let mem := mwd (cdata RData).

  Context `{Hstencil: Stencil}.
  Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
  Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

  Section get_s2_page_index_proof.

    Let L : compatlayer (cdata RData) :=
      get_mem_region_base ↦ gensem get_mem_region_base_spec
          ⊕ get_mem_region_index ↦ gensem get_mem_region_index_spec
          ⊕ mem_region_search ↦ gensem mem_region_search_spec.

    Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
    Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

    Section BodyProof.

      Context `{Hwb: WritableBlockOps}.
      Variable (sc: stencil).
      Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).

      Variable b_get_mem_region_base: block.
      Hypothesis h_get_mem_region_base_s : Genv.find_symbol ge get_mem_region_base = Some b_get_mem_region_base.
      Hypothesis h_get_mem_region_base_p : Genv.find_funct_ptr ge b_get_mem_region_base
                                           = Some (External (EF_external get_mem_region_base
                                                            (signature_of_type (Tcons tuint Tnil) tulong cc_default))
                                                  (Tcons tuint Tnil) tulong cc_default).
      Variable b_get_mem_region_index: block.
      Hypothesis h_get_mem_region_index_s : Genv.find_symbol ge get_mem_region_index = Some b_get_mem_region_index.
      Hypothesis h_get_mem_region_index_p : Genv.find_funct_ptr ge b_get_mem_region_index
                                            = Some (External (EF_external get_mem_region_index
                                                             (signature_of_type (Tcons tuint Tnil) tulong cc_default))
                                                   (Tcons tuint Tnil) tulong cc_default).
      Variable b_mem_region_search: block.
      Hypothesis h_mem_region_search_s : Genv.find_symbol ge mem_region_search = Some b_mem_region_search.
      Hypothesis h_mem_region_search_p : Genv.find_funct_ptr ge b_mem_region_search
                                         = Some (External (EF_external mem_region_search
                                                          (signature_of_type (Tcons tulong Tnil) tuint cc_default))
                                                (Tcons tulong Tnil) tuint cc_default).

      Lemma get_s2_page_index_body_correct:
        forall m d env le addr res
               (Henv: env = PTree.empty _)
               (HPTaddr: PTree.get _addr le = Some (Vlong addr))
               (Hinv: high_level_invariant d)
               (Hspec: get_s2_page_index_spec0 (VZ64 (Int64.unsigned addr)) d = Some (VZ64 (Int64.unsigned res))),
             exists le', (exec_stmt ge env le ((m, d): mem) get_s2_page_index_body E0 le' (m, d) (Out_return (Some (Vlong res, tulong)))).
      Proof.
        solve_code_proof Hspec get_s2_page_index_body; eexists; solve_proof_low.
      Qed.

    End BodyProof.

    Theorem get_s2_page_index_code_correct:
      spec_le (get_s2_page_index ↦ get_s2_page_index_spec_low) (〚 get_s2_page_index ↦ f_get_s2_page_index 〛 L).
    Proof.
      set (L' := L) in *.
      unfold L in *.
      fbigstep_pre L'.
      fbigstep (get_s2_page_index_body_correct s (Genv.globalenv p) makeglobalenv
               b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m'0 labd
               (PTree.empty _) (bind_parameter_temps' (fn_params f_get_s2_page_index ) (Vlong addr :: nil)
               (create_undef_temps (fn_temps f_get_s2_page_index)))) hinv.
    Qed.

  End get_s2_page_index_proof.

End PageIndexProofLow.

author: VeriGu

repo: VRM-proof

save_path: github-repos/coq/VeriGu-VRM-proof


text:
From UT Require Import Prelims Setoid Typoid TypoidFunction TypoidNT ExponentialTypoid.
Require Import Coq.Classes.CRelationClasses.
Require Import FunctionalExtensionality.
Set Universe Polymorphism.

Definition idtoeqvT: ∏ {A: Type} {x y: A} {T: Typoid A} (p: Id x y), @et A (@st A T) x y.
Proof. intros A x y T p.
        exact (transport (fun z => x ~> z) p (eqv x)).
Defined.

Definition idtoeqvTT: ∏ {A: Type} {x y: A} {T: Typoid A} {f g: x ~> y} (p: Id f g), f == g.
Proof. intros A x y T f g p.
       now induction p.
Defined.

Definition UA_defT: Type := ∏ (A: Type) (x y: A) (T: Typoid A), isequiv (@idtoeqvT A x y T).
Axiom UAT: UA_defT.

Definition UA_defTT: Type := ∏ (A: Type) (x y: A) (T: Typoid A) (f g: x ~> y), isequiv (@idtoeqvTT A x y T f g).
Axiom UATT: UA_defTT.

Definition YaOp {A: Type} (a: A) (TA: Typoid A): TypoidFunction (OppositeT TA) Uni.
Proof. unshelve econstructor.
       - intro x.
         exact (et (@st A TA) x a).
       - simpl. intros x y f.
         unshelve econstructor.
         + intro g.
           exact (f o g).
         + apply qinv_ishae.
           unshelve econstructor.
           ++ intros g.
              exact (inv f o g).
           ++ unfold homotopy, compose.
              split.
              * intros g.
                apply UATT.
                rewrite <- Typ3.
                rewrite Typ2_i.
                rewrite Typ1_i.
                unfold id.
                reflexivity.
              * intros g.
                apply UATT.
                rewrite <- Typ3.
                rewrite Typ2_ii.
                rewrite Typ1_i.
                unfold id.
                reflexivity.
       - simpl. unfold homotopy, id.
         intros x f.
         apply UATT.
         unfold Setoid.OppositeS_obligation_1.
         rewrite Typ1_i.
         reflexivity.
       - simpl. intros x y z f g.
         unfold homotopy, id, compose.
         intros h.
         apply UATT.
         unfold Setoid.OppositeS_obligation_2.
         rewrite Typ3.
         reflexivity.
       - simpl. intros x y f g H.
         unfold homotopy.
         intro h.
         apply UATT.
         rewrite H.
         reflexivity.
       - repeat intro.
         apply UATT.
         rewrite X.
         reflexivity.
Defined.

Definition PiTypoidAppOpp: forall {A: Type} (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni) (a: A),
  Typoid (fobj P a).
Proof. intros A TA P a.
       simpl.
       unshelve econstructor.
       - unshelve econstructor.
         + unfold crelation.
           intros phi Q.
(*         exact (forall x: A, (et (@st _ Uni) (phi x) (Q x))). *)
           exact (Id phi Q).
         + simpl. intros px.
           apply refl.
         + simpl. intros p q r Ha Hb.
           specialize (@concat _ p q r Ha Hb); intro C.
           exact C.
         + simpl. intros p q H.
           exact (inverse H).
       - simpl. intros p q.
         unfold crelation.
         intros Hp Hq.
         exact (Id Hp Hq).
       - simpl. intros p q H.
         apply refl.
       - simpl. intros p q Hp Hq H.
         exact (inverse H).
       - simpl. intros p q Hp Hq Hr Ha Hb.
         specialize (@concat _ Hp Hq Hr Ha Hb);
         intro C.
         exact C.
       - simpl. intros p q Hp.
         induction (Hp).
         simpl.
         apply refl.
       - simpl. intros p q Hp.
         induction (Hp).
         simpl.
         apply refl.
       - simpl. intros p q Hp.
         induction (Hp).
         simpl.
         apply refl.
       - simpl. intros p q Hp.
         induction (Hp).
         simpl.
         apply refl.
       - simpl. intros p q r s Hp Hq Hs.
         simpl in *.
         specialize (@concat_assoc _ p q r s
                                  Hp Hq Hs ); intros C.
         exact (inverse C).
       - simpl. intros p q r Hp Hq Hr Hs Ht Hi.
         induction (Ht).
         induction (Hi).
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X).
         induction (X0).
         apply refl.
       - repeat intro.
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X).
         apply refl.
Defined.

Definition PiTypoidOpp: forall {A: Type} (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni),
  Typoid (forall x: A, fobj P x).
Proof. intros A TA P.
       simpl.
       unshelve econstructor.
       - unshelve econstructor.
         + unfold crelation.
           intros phi Q.
           exact (forall x: A, (et (@st _ (PiTypoidAppOpp TA P x)) (phi x) (Q x))).
(*            exact (forall x: A, (Id (phi x) (Q x))). *)
         + simpl. intros p x.
           apply refl.
         + simpl. intros p q r Ha Hb x.
           specialize (@concat _ (p x) (q x) (r x) (Ha x) (Hb x)); intro C.
           exact C.
         + simpl. intros p q H x.
           exact (inverse (H x)).
       - simpl. intros p q.
         unfold crelation.
         intros Hp Hq.
         exact (forall x: A, Id (Hp x) (Hq x)).
       - simpl. intros p q H x.
         apply refl.
       - simpl. intros p q Hp Hq H x.
         exact (inverse (H x)).
       - simpl. intros p q Hp Hq Hr Ha Hb x.
         specialize (@concat _ (Hp x) (Hq x) (Hr x) (Ha x) (Hb x));
         intro C.
         exact C.
       - simpl. intros p q Hp x.
         induction (Hp x).
         simpl.
         apply refl.
       - simpl. intros p q Hp x.
         induction (Hp x).
         simpl.
         apply refl.
       - simpl. intros p q Hp x.
         induction (Hp x).
         simpl.
         apply refl.
       - simpl. intros p q Hp x.
         induction (Hp x).
         simpl.
         apply refl.
       - simpl. intros p q r s Hp Hq Hs x.
         simpl in *.
         specialize (@concat_assoc _ (p x) (q x) (r x) (s x)
                                  (Hp x) (Hq x) (Hs x)); intros C.
         exact (inverse C).
       - simpl. intros p q r Hp Hq Hr Hs Ht Hi x.
         induction (Ht x).
         induction (Hi x).
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X x2).
         induction (X0 x2).
         apply refl.
       - repeat intro.
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X x1).
         apply refl.
Defined.

Definition HomOp: forall {A: Type} (TA: Typoid A) (P Q: TypoidFunction (OppositeT TA) Uni),
  Typoid (∏ (x: A), ∏ (p: fobj P x), fobj Q x).
Proof. intros A TA P Q.
       unshelve econstructor.
       - unshelve econstructor.
         + unfold crelation.
           intros phi psi.
           exact (∏ (x: A) (p: fobj P x), (Id (phi x p) (psi x p))).
         + simpl. intros p x q.
           apply refl.
         + simpl. intros p q r Hp Hq x px.
           specialize (@concat _ (p x px) (q x px) (r x px) (Hp x px) (Hq x px)); intro C.
           exact C.
         + simpl. intros p q Hp x px.
           exact (inverse (Hp x px)).
       - simpl. intros p q.
         unfold crelation.
         intros Hp Hq.
         exact (forall (x: A) (p: fobj P x), Id (Hp x p) (Hq x p)).
       - simpl. intros p q H x px.
         apply refl.
       - simpl. intros p q Hp Hq H x px.
         exact (inverse (H x px)).
       - simpl. intros p q Hp Hq Hr Ha Hb x px.
         specialize (@concat _ (Hp x px) (Hq x px) (Hr x px) (Ha x px) (Hb x px));
         intro C.
         exact C.
       - simpl. intros p q Hp x px.
         induction (Hp x px).
         simpl.
         apply refl.
       - simpl. intros p q Hp x px.
         induction (Hp x px).
         simpl.
         apply refl.
       - simpl. intros p q Hp x px.
         induction (Hp x px).
         simpl.
         apply refl.
       - simpl. intros p q Hp x px.
         induction (Hp x px).
         simpl.
         apply refl.
       - simpl. intros p q r s Hp Hq Hs x px.
         simpl in *.
         specialize (@concat_assoc _ (p x px) (q x px) (r x px) (s x px)
                                  (Hp x px) (Hq x px) (Hs x px)); intros C.
         exact (inverse C).
       - simpl. intros p q r Hp Hq Hr Hs Ht Hi x px.
         induction (Ht x px).
         induction (Hi x px).
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X x2 p).
         induction (X0 x2 p).
         apply refl.
       - repeat intro.
         apply refl.
       - repeat intro.
         simpl in *.
         induction (X x1 p).
         apply refl.
Defined.

Lemma app_concat: ∏ {A B: Type} {a b c: A} (f: A -> B) (p: Id a b) (q: Id b c),
Id (ap f (concat p q)) (concat (ap f p) (ap f q)).
Proof. intros. now induction p, q. Defined.

Definition apD {A C: Type} {B: A -> Type} (f: forall a:A, B a) {x y: A} (p: Id x y):
  Id (transport _  p (f x)) (f y).
Proof. unfold transport.
       induction p.
       simpl.
       apply refl.
Defined.

(** j *)
Definition HomYaOpPNTl: forall {A: Type} (a: A) (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni),
  TypoidFunction (HomOp TA (YaOp a TA) P) (PiTypoidAppOpp TA P a).
Proof. intros A a TA P.
       unshelve econstructor.
       - simpl. intro v.
         exact (v a (eqv a)).
       - simpl. intros p q Hp.
         specialize (Hp a (eqv a)).
         exact Hp.
       - simpl. intros p.
         apply refl.
       - simpl. intros p q r Hp Hq.
         apply refl.
       - simpl. intros p q Hp Hq H.
         induction (H a (eqv a)).
         apply refl.
       - simpl. repeat intro.
         induction (X a (eqv a)).
         apply refl.
Defined.

(** i *)
Definition HomYaOpPNTr: forall {A: Type} (a: A) (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni),
  TypoidFunction (PiTypoidAppOpp TA P a) (HomOp TA (YaOp a TA) P).
Proof. intros A a TA P.
       unshelve econstructor.
       - simpl.
         intros u x f.
         exact ((pr1 (fmap P f)) u).
       - simpl. intros px py q x f.
         induction q.
         apply refl.
       - simpl. intros px x f.
         apply refl.
       - simpl. intros px py pz p q x f.
         induction p.
         induction q.
         apply refl.
       - simpl. intros px py p q r x f.
         induction p.
         induction r.
         apply refl.
       - repeat intro.
         simpl in X.
         induction X.
         apply refl.
Defined.

(** (j o i)(u) = u *)
Lemma HomYaOpPNTEql: forall {A: Type} (a: A) (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni)
                            (u: fobj P a),
  et (@st _ (PiTypoidAppOpp TA P a)) (fobj (TFCompose (HomYaOpPNTr a TA P) (HomYaOpPNTl a TA P)) u) u.
Proof. intros.
       cbn.
       unfold compose.
       simpl.
       destruct P.
       simpl in u, fmap, fmap_pid.
       unfold Setoid.OppositeS_obligation_1 in *.
       simpl.
       specialize (fmap_pid a).
       simpl in fmap_pid.
       destruct (fmap a a (@eqv A (@st A TA) a)).
       simpl in fmap_pid.
       simpl.
       unfold homotopy in fmap_pid.
       specialize (fmap_pid u).
       unfold id in *.
       exact fmap_pid.
Qed.

(** (i o j)(u) = u ??? *)
Lemma HomYaOpPNTEqr: forall {A: Type} (a: A) (TA: Typoid A) (P: TypoidFunction (OppositeT TA) Uni)
                            (sigma: ∏ x : A, ∏ e: x ~> a, fobj P x),
  et (@st _ (HomOp TA (YaOp a TA) P)) (fobj (TFCompose (HomYaOpPNTl a TA P) (HomYaOpPNTr a TA P)) sigma) sigma.
Proof. intros.
       simpl.
       intros x e.
       unfold compose.
       simpl in sigma.
       destruct P.
       simpl in sigma, fmap, e.
       destruct (fmap a x e) as (g, R).
       destruct R as (ginv, (ob1, (ob2, ob3))).
       unfold homotopy, compose, id in *.
       simpl.
Admitted.

author: ekiciburak

repo: UnivalentTypoids