Require Export LinkSourceTemplate.
Require Export MakeProgram.

Global Opaque Structures.semof.
Global Opaque Structures.oplus.
Global Opaque Structures.emptyset.
Global Opaque LAsmModuleSem.lasm_semantics_ops.
Global Opaque LAsm.module_ops.
Global Opaque compatlayer_ops.

Section WITHCOMPCERTIKOS.
  Context `{compcertikos_prf: CompCertiKOS}.
  Context `{real_params_prf : RealParams}.

  Definition link_impl_inverted_add_cfunction (P: LAsm.module → Type) f M :=
    { Mf : LAsm.module &
      prod (CompCertiKOS.transf_module (lcf_id f ↦ lcf_fun f) = ret Mf)
           (P (Mf ⊕ M)) }.

  Fixpoint link_impl_inverted_add_gvars {D} vs (M: LAsm.module) L P0 :=
    prod
      (LayerOK (〚M〛 (link_impl_add_gvar_specs (LDATA:=D) vs L ⊕ L64) ⊕
                (link_impl_add_gvar_specs (LDATA:=D) vs L ⊕ L64)))
      (match vs with
         | nil ⇒ P0
         | v::vs ⇒
           link_impl_inverted_add_gvars vs (M ⊕ lgv_id v ↦ lgv_type v) L P0
       end).

  Definition link_impl_inverted_base {D} lm (ll: compatlayer D) M Mc :=
    link_impl_inverted_add_gvars
      (lm_gvar lm)
      (Mc ⊕ link_impl_asm lm)
      ll
      (prod
         (LayerOK (〚M〛 (ll ⊕ L64) ⊕ ll ⊕ L64))
         (M = link_impl_add_gvar_defs (lm_gvar lm) (Mc ⊕ link_impl_asm lm) ⊕ ∅)).

  Definition link_impl_inverted {D} (lm: link_module) (ll: compatlayer D) M :=
    fold_left
      (link_impl_inverted_add_cfunction)
      (lm_cfun lm)
      (link_impl_inverted_base lm ll M)
      ∅.

  Lemma link_impl_imply_add_cfunction (P: LAsm.module → Type) f M M´:
    link_add_cfunction f (ret M) = ret M´ →
    P M´ →
    link_impl_inverted_add_cfunction P f M.
  Proof.
    intros HfM HM´.
    unfold link_add_cfunction in HfM.
    inv_monad HfM.
    eexists.
    split.
    - eassumption.
    - subst.
      assumption.
  Qed.

  Lemma link_impl_imply_fold_add_cfunction P fs M M´:
    fold_right link_add_cfunction (ret M) fs = ret M´ →
    P M´ →
    fold_left link_impl_inverted_add_cfunction fs P M.
  Proof.
    revert P M M´.
    induction fs as [ | f fs IHfs].
    - simpl.
      inversion 1.
      tauto.
    - simpl.
      intros P M M´ HfM HM´.
      specialize (IHfs (link_impl_inverted_add_cfunction P f) M).
      destruct (fold_right link_add_cfunction (ret M) fs); try now inversion HfM.
      eapply IHfs.
      reflexivity.
      eapply link_impl_imply_add_cfunction; eauto.
  Qed.

  Lemma link_impl_imply_add_gvars {D} vs M L P0 M´:
    link_impl_add_gvars (LDATA:=D) vs M L = ret M´ →
    P0 →
    link_impl_inverted_add_gvars vs M L P0.
  Proof.
    revert M M´ L.
    induction vs; intros M M´ L.
    - simpl.
      intros H; inv_monad H.
      tauto.
    - simpl.
      intros H; inv_monad H.
      eauto.
  Qed.

  Lemma link_impl_imply_gvar {D} (lm: link_module) (ll: compatlayer D) M M´:
    link_impl_gvar lm ll M = ret M´ →
    M´ = link_impl_add_gvar_defs (lm_gvar lm) M.
  Proof.
    unfold link_impl_gvar.
    generalize (lm_gvar lm); clear lm.
    intros vs.
    revert M M´.
    induction vs as [ | v vs IHvs]; intros M M´.
    - simpl.
      intros H.
      inv_monad H.
      congruence.
    - simpl.
      intros H.
      inv_monad H.
      eauto.
  Qed.

  Lemma link_impl_imply {D} (lm: link_module) (ll: compatlayer D) M:
    link_impl lm ll = OK M →
    link_impl_inverted lm ll M.
  Proof.
    unfold link_impl, link_impl_c.
    intros H.
    inv_monad H; subst.
    unfold link_impl_inverted.
    eapply link_impl_imply_fold_add_cfunction; eauto.
    unfold link_impl_inverted_base.
    eapply link_impl_imply_add_gvars; eauto.
    split; eauto.
    f_equal.
    eapply link_impl_imply_gvar; eauto.
  Qed.

  Context {DL DH: Type} `{CompatData DL} `{CompatData DH}.
  Context `{!CompatRelOps (cdata DH) (cdata DL)} `{!CompatRel (cdata DH) (cdata DL)}.

  Definition init_correct_type lm LL LH :=
    ∀ M: LAsm.module,
      link_impl lm LL = OK M →
      ModuleOK M →
      cl_init_sim (cdata DH) (cdata DL) (crel DH DL) (LH ⊕ L64) M (LL ⊕ L64).

  Definition link_correct_aux_type lm LL LH :=
    ∀ M: LAsm.module,
      link_impl (LDATA := cdata DL) lm LL = OK M →
      LL ⊕ L64 ⊢ (crel DH DL, M) : LH ⊕ L64.

  Definition cl_backward_simulation_type lm LL LH :=
    fun `{!LAsm.AccessorsDefined (LL ⊕ L64)}
        `{!LAsm.AccessorsDefined (LH ⊕ L64)} ⇒
    ∀ (s: stencil) (CTXT M: LAsm.module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      link_impl lm LL = OK M →
      make_program (D := cdata DH) s CTXT (LH ⊕ L64) = OK ph →
      make_program (D := cdata DL) s (CTXT ⊕ M) (LL ⊕ L64) = OK pl →
      backward_simulation
        (LAsm.semantics (lcfg_ops := LC (LH ⊕ L64)) ph)
        (LAsm.semantics (lcfg_ops := LC (LL ⊕ L64)) pl).

  Definition make_program_exist_type lm LL LH :=
    ∀ (s: stencil) (CTXT M: LAsm.module) pl,
      link_impl lm LL = OK M →
      make_program (D := cdata DL) s (CTXT ⊕ M) (LL ⊕ L64) = OK pl →
      ∃ ph, make_program (D := cdata DH) s CTXT (LH ⊕ L64) = OK ph.

End WITHCOMPCERTIKOS.

Ltac destruct_impl_inverted H :=
  lazymatch type of H with
    | link_impl_inverted_add_cfunction _ _ _ ⇒
      let M := fresh "M" in
      let HM := fresh "H" M in
      let H´ := fresh in
      destruct H as (M & HM & H´);
      simpl in HM;
      destruct_impl_inverted H´
    | prod (LayerOK _) _ ⇒
      let Hok := fresh "Hok" in
      let H´ := fresh in
      destruct H as [Hok H´];
      destruct_impl_inverted H´
    | _ ⇒
      idtac
  end.

Ltac inv_link_impl HM :=
  apply link_impl_imply in HM;
  unfold link_impl_inverted in HM;
  unfold link_impl_inverted_base in HM;
  unfold link_impl_asm in HM;
  simpl in HM;
  destruct_impl_inverted HM.

Require Export Coqlib.
Require Export Integers.
Require Export Maps.
Require Export AST.
Require Export Globalenvs.
Require Export FlatMemory.
Require Export Decision.
Require Export LAsm.
Require Export LAsmModuleSem.
Require Export LAsmModuleSemMakeProgram.
Require Export LayerCalculusLemma.
Require Export LinkTactic.
Require Export Soundness.
Require Export CompatExternalCalls.

Section INITMEM.
  Context `{compcertikos_prf: CompCertiKOS}.
  Context `{real_params_prf : RealParams}.

  Lemma init_data_list_size_pos :
    ∀ il, Genv.init_data_list_size il ≥ 0.
  Proof.
    induction il; simpl; try omega.
    assert (H:= Genv.init_data_size_pos a); omega.
  Qed.

  Fixpoint load_init_space_zeros m b p (il: list AST.init_data): Prop :=
    match il with
      | Init_space n :: il´ ⇒
        (∀ i, 0 ≤ i < n → Mem.load Mint8unsigned m b (p + i) = Some Vzero)
        ∧ load_init_space_zeros m b (p + Zmax n 0) il´
      | _ ⇒ True
    end.

  Remark load_init_space_zeros_invariant:
    ∀ m m´ b,
      (∀ chunk ofs, Mem.load chunk m´ b ofs = Mem.load chunk m b ofs) →
      ∀ il p,
        load_init_space_zeros m b p il → load_init_space_zeros m´ b p il.
  Proof.
    induction il; intro p; simpl; auto.
    destruct a; auto.
    intro Hm; split.
    intros i Hi; rewrite H.
    apply (proj1 Hm); auto.
    apply (IHil _ (proj2 Hm)).
  Qed.

  Lemma store_zeros_charact :
    ∀ m b p n m´,
      store_zeros m b p n = Some m´ →
      ∀ i, p ≤ i < p+n → Mem.load Mint8unsigned m´ b i = Some Vzero.
  Proof.
    intros m b p n m´ Hsz i Hi.
    functional induction (store_zeros m b p n); try omega.
    assert (Hcases: i = p ∨ p+1 ≤ i < p+1+(n-1)) by omega.
    destruct Hcases as [Hi´|Hi´]; subst; auto.
    assert (Hsz´:= Genv.store_zeros_outside).
    rewrite (Hsz´ _ _ _ _ _ Hsz).
    rewrite (Mem.load_store_same _ _ _ _ _ _ e0); auto.
    right; simpl; omega.
    inv Hsz.
  Qed.

  Lemma init_space_zeros_charact {F V} :
    ∀ ge b il m p m´,
      (∀ i, p ≤ i < p + Genv.init_data_list_size il →
                 Mem.load Mint8unsigned m b i = Some Vzero) →
      Genv.store_init_data_list(F:=F)(V:=V) ge m b p il = Some m´ →
      load_init_space_zeros m´ b p il.
  Proof.
    induction il; intros m p m´ Hz Hstore; simpl; auto.
    destruct a; simpl; auto.
    simpl in Hstore; split.
    intros i Hi; assert (Hout:= Genv.store_init_data_list_outside).
    assert (Hzpos: Z.max z 0 ≥ z).
    unfold Z.max; destruct z; simpl; try omega.
    assert (Hneg:= Zlt_neg_0 p0); omega.
    rewrite (Hout _ _ _ _ _ _ _ _ Hstore).
    apply Hz; simpl.
    assert (H2:= init_data_list_size_pos il); omega.
    simpl; right; omega.
    apply (IHil m); auto.
    intros i Hi; apply Hz; simpl.
    split; try omega.
    unfold Z.max in Hi; destruct z; simpl in Hi; try omega.
    assert (Hpos:= Zle_0_pos p0); omega.
  Qed.

  Definition variables_initialized´ {F V} (ge g: Genv.t F V) (m: mem) :=
    ∀ b gv,
      Genv.find_var_info g b = Some gv →
      Mem.range_perm m b 0 (Genv.init_data_list_size gv.(gvar_init)) Cur (Genv.perm_globvar gv)
      ∧ (∀ ofs k p, Mem.perm m b ofs k p →
            0 ≤ ofs < Genv.init_data_list_size gv.(gvar_init) ∧ perm_order (Genv.perm_globvar gv) p)
      ∧ (gv.(gvar_volatile) = false → Genv.load_store_init_data ge m b 0 gv.(gvar_init) )
      ∧ (gv.(gvar_volatile) = false → load_init_space_zeros m b 0 gv.(gvar_init)).

  Lemma alloc_global_initialized´ {F V} :
    ∀ ge ge´ m id g m´,
      Genv.genv_next(F:=F)(V:=V) ge´ = Mem.nextblock m →
      Genv.alloc_global ge m (id, g) = Some m´ →
      variables_initialized´ ge ge´ m →
      Genv.functions_initialized ge´ m →
      variables_initialized´ ge (Genv.add_global ge´ (id, g)) m´
      ∧ Genv.functions_initialized (Genv.add_global ge´ (id, g)) m´
      ∧ Genv.genv_next (Genv.add_global ge´ (id, g)) = Mem.nextblock m´.
  Proof.
    intros.
    exploit Genv.alloc_global_nextblock; eauto. intros NB. split.
    destruct g as [[f|v]|].
    red; intros. unfold Genv.find_var_info in H3. simpl in H3.
    exploit H1; eauto. intros [A [B [C Hisz]]].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_vars_range; eauto. rewrite H; auto.
    split. red; intros. erewrite <- Genv.alloc_global_perm; eauto.
    split. intros. eapply B. erewrite Genv.alloc_global_perm; eauto.
    split. intros. apply Genv.load_store_init_data_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.
    intros. apply load_init_space_zeros_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.
    red; intros. unfold Genv.find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3.
    destruct (peq b (Genv.genv_next ge´)).
    inv H3. simpl in H0.
    set (init := gvar_init gv) in ×.
    set (sz := Genv.init_data_list_size init) in ×.
    destruct (Mem.alloc m 0 sz) as [m1 b´] eqn:?.
    destruct (store_zeros m1 b´ 0 sz) as [m2|] eqn:?; try discriminate.
    destruct (Genv.store_init_data_list ge m2 b´ 0 init) as [m3|] eqn:?; try discriminate.
    exploit Mem.alloc_result; eauto. intro RES.
    replace (Genv.genv_next ge´) with b´ by congruence.
    split. red; intros. eapply Mem.perm_drop_1; eauto.
    split. intros.
    assert (0 ≤ ofs < sz).
    eapply Mem.perm_alloc_3; eauto.
    erewrite Genv.store_zeros_perm; [idtac|eauto].
    erewrite Genv.store_init_data_list_perm; [idtac|eauto].
    eapply Mem.perm_drop_4; eauto.
    split. auto. eapply Mem.perm_drop_2; eauto.
    split. intros. apply Genv.load_store_init_data_invariant with m3.
    intros. eapply Mem.load_drop; eauto.
    right; right; right. unfold Genv.perm_globvar. rewrite H3.
    destruct (gvar_readonly gv); auto with mem.
    eapply Genv.store_init_data_list_charact; eauto.
    intros. apply load_init_space_zeros_invariant with m3.
    intros. eapply Mem.load_drop; eauto.
    right; right; right. unfold Genv.perm_globvar. rewrite H3.
    destruct (gvar_readonly gv); auto with mem.
    eapply init_space_zeros_charact; eauto.
    eapply store_zeros_charact; eauto.
    exploit H1; eauto. intros [A [B [C Hisz]]].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_vars_range; eauto. rewrite H; auto.
    split. red; intros. erewrite <- Genv.alloc_global_perm; eauto.
    split. intros. eapply B. erewrite Genv.alloc_global_perm; eauto.
    split. intros. apply Genv.load_store_init_data_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.
    intros. apply load_init_space_zeros_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.

    red; intros. unfold Genv.find_var_info in H3. simpl in H3.
    exploit H1; eauto. intros [A [B [C Hisz]]].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_vars_range; eauto. rewrite H; auto.
    split. red; intros. erewrite <- Genv.alloc_global_perm; eauto.
    split. intros. eapply B. erewrite Genv.alloc_global_perm; eauto.
    split. intros. apply Genv.load_store_init_data_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.
    intros. apply load_init_space_zeros_invariant with m; auto.
    intros. eapply Genv.load_alloc_global; eauto.
    split. destruct g as [[f|v]|].
    red; intros. unfold Genv.find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3.
    destruct (peq b (Genv.genv_next ge´)).
    inv H3. simpl in H0.
    destruct (Mem.alloc m 0 1) as [m1 b´] eqn:?.
    exploit Mem.alloc_result; eauto. intro RES.
    replace (Genv.genv_next ge´) with b´ by congruence.
    split. eapply Mem.perm_drop_1; eauto.
    omega.
    intros.
    assert (0 ≤ ofs < 1).
    eapply Mem.perm_alloc_3; eauto.
    eapply Mem.perm_drop_4; eauto.
    split. omega. eapply Mem.perm_drop_2; eauto.
    exploit H2; eauto. intros [A B].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_funs_range; eauto. rewrite H; auto.
    split. erewrite <- Genv.alloc_global_perm; eauto.
    intros. eapply B. erewrite Genv.alloc_global_perm; eauto.
    red; intros. unfold Genv.find_funct_ptr in H3. simpl in H3.
    exploit H2; eauto. intros [A B].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_funs_range; eauto. rewrite H; auto.
    split. erewrite <- Genv.alloc_global_perm; eauto.
    intros. eapply B. erewrite Genv.alloc_global_perm; eauto.

    red; intros. unfold Genv.find_funct_ptr in H3. simpl in H3.
    exploit H2; eauto. intros [A B].
    assert (D: Mem.valid_block m b).
    red. exploit Genv.genv_funs_range; eauto. rewrite H; auto.
    split. erewrite <- Genv.alloc_global_perm; eauto.
    intros. eapply B. erewrite Genv.alloc_global_perm; eauto.
    rewrite NB. simpl. rewrite H. auto.
  Qed.

  Lemma alloc_globals_initialized´ {F V} :
    ∀ (ge : Genv.t F V) gl ge´ m m´,
      Genv.genv_next ge´ = Mem.nextblock m →
      Genv.alloc_globals ge m gl = Some m´ →
      variables_initialized´ ge ge´ m →
      Genv.functions_initialized ge´ m →
      variables_initialized´ ge (Genv.add_globals ge´ gl) m´ ∧
      Genv.functions_initialized (Genv.add_globals ge´ gl) m´.
  Proof.
    induction gl; simpl; intros.
    inv H0; auto.
    destruct a as [id g]. destruct (Genv.alloc_global ge m (id, g)) as [m1|] eqn:?; try discriminate.
    exploit (alloc_global_initialized´(F:=F)(V:=V)); eauto. intros [P [Q R]].
    eapply IHgl; eauto.
  Qed.

  Theorem init_mem_characterization´ {F V} :
    ∀ p b gv m,
      Genv.find_var_info (Genv.globalenv(F:=F)(V:=V) p) b = Some gv →
      Genv.init_mem p = Some m →
      Mem.range_perm m b 0 (Genv.init_data_list_size gv.(gvar_init)) Cur (Genv.perm_globvar gv)
      ∧ (∀ ofs k p, Mem.perm m b ofs k p →
            0 ≤ ofs < Genv.init_data_list_size gv.(gvar_init) ∧ perm_order (Genv.perm_globvar gv) p)
      ∧ (gv.(gvar_volatile) = false → Genv.load_store_init_data (Genv.globalenv p) m b 0 gv.(gvar_init))
      ∧ (gv.(gvar_volatile) = false → load_init_space_zeros m b 0 gv.(gvar_init)).
  Proof.
    intros. eapply alloc_globals_initialized´; eauto.
    rewrite Mem.nextblock_empty. auto.
    red; intros. unfold Genv.find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
    red; intros. unfold Genv.find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
  Qed.

  Lemma zero_bytes : ∀ m b i bytes,
    Mem.loadbytes m b i 1 = Some bytes → decode_val Mint8unsigned bytes = Vzero →
    bytes = Byte Byte.zero :: nil.
  Proof.
    intros m b i bytes Hlb Hdec.
    assert (Hmax:= max_unsigned_val).
    assert (Hlength:= Mem.loadbytes_length _ _ _ _ _ Hlb).
    assert (∃ byte, bytes = byte :: nil).
    destruct bytes; inv Hlength.
    destruct bytes; inv H0.
    ∃ m0; auto.
    destruct H as [byte]; subst.
    unfold decode_val in Hdec; simpl in Hdec.
    destruct byte as [|byte|].
    inv Hdec.
    rewrite <- decode_encode_int_1 in Hdec.
    unfold decode_int, encode_int in Hdec.
    rewrite rev_if_be_involutive in Hdec.
    unfold rev_if_be in Hdec; simpl in Hdec.
    replace (if Archi.big_endian then byte::nil else byte::nil) with (byte::nil) in Hdec.
    simpl in Hdec.
    assert (Hrange:= Byte.unsigned_range byte).
    assert (Hmod: Byte.modulus = 256) by auto.
    rewrite Byte.unsigned_repr in Hdec.
    rewrite 2 Z.add_0_r in Hdec.
    rewrite Int.repr_unsigned in Hdec.
    unfold Vzero, Int.zero in Hdec.
    assert (Int.repr (Byte.unsigned byte) = Int.repr 0).
    assert (∀ i1 i2, Vint i1 = Vint i2 → i1 = i2).
    intros i1 i2 Hi; inv Hi; auto.
    apply H; auto.
    apply f_equal with (f:= Int.unsigned) in H.
    rewrite 2 Int.unsigned_repr in H; try omega.
    apply f_equal with (f:= Byte.repr) in H.
    rewrite Byte.repr_unsigned in H; subst; auto.
    rewrite Z.add_0_r; rewrite Int.unsigned_repr; try omega.
    assert (Byte.max_unsigned = 255) by auto.
    omega.
    destruct Archi.big_endian; auto.
    inv Hdec.
  Qed.

  Lemma load_four_bytes_zero : ∀ m b p, (4 | p) →
    (∀ i, 0 ≤ i < 4 → Mem.load Mint8unsigned m b (p+i) = Some Vzero) →
    Mem.load Mint32 m b p = Some Vzero.
  Proof.
    intros m b p Hdiv Hbytes.
    assert (H0: 0 ≤ 0 < 4) by omega.
    assert (H1: 0 ≤ 1 < 4) by omega.
    assert (H2: 0 ≤ 2 < 4) by omega.
    assert (H3: 0 ≤ 3 < 4) by omega.
    assert (Hl0:= Hbytes 0 H0).
    assert (Hl1:= Hbytes 1 H1).
    assert (Hl2:= Hbytes 2 H2).
    assert (Hl3:= Hbytes 3 H3).
    apply Mem.load_loadbytes in Hl0; destruct Hl0 as [bytes0 [Hlb0 Hdec0]].
    apply Mem.load_loadbytes in Hl1; destruct Hl1 as [bytes1 [Hlb1 Hdec1]].
    apply Mem.load_loadbytes in Hl2; destruct Hl2 as [bytes2 [Hlb2 Hdec2]].
    apply Mem.load_loadbytes in Hl3; destruct Hl3 as [bytes3 [Hlb3 Hdec3]].
    assert (bytes0 = Byte Byte.zero :: nil) by (apply (zero_bytes m b (p+0)); auto).
    assert (bytes1 = Byte Byte.zero :: nil) by (apply (zero_bytes m b (p+1)); auto).
    assert (bytes2 = Byte Byte.zero :: nil) by (apply (zero_bytes m b (p+2)); auto).
    assert (bytes3 = Byte Byte.zero :: nil) by (apply (zero_bytes m b (p+3)); auto).
    assert (Hchunk: size_chunk Mint8unsigned ≥ 0) by (simpl; omega).
    rewrite Z.add_0_r in Hlb0; unfold size_chunk in ×.
    assert (Hlb01:= Mem.loadbytes_concat _ _ _ _ _ _ _ Hlb0 Hlb1 Hchunk Hchunk).
    simpl in Hlb01.
    assert (Hlb012:= Mem.loadbytes_concat _ _ _ _ _ _ _ Hlb01 Hlb2 Hchunk Hchunk).
    simpl in Hlb012.
    assert (Hlb:= Mem.loadbytes_concat _ _ _ _ _ _ _ Hlb012 Hlb3 Hchunk Hchunk).
    subst; simpl in Hlb.
    replace 4 with (size_chunk Mint32) in Hlb; auto.
    apply Mem.loadbytes_load in Hlb; auto.
  Qed.
End INITMEM.

Ltac link_correct_aux_fresh :=
  lazymatch goal with
    | |- ?LL ⊢ _ : ?LH ⇒
      LinkTactic.transfer_variables;
      unfold_layer LH;
      match goal with
        | |- _ ⊢ (_, _ ⊕ ∅) : _ ⇒
          apply LayerLogicImpl.vdash_oplus_empty
        | |- _ ⇒
          hcomp_tac
      end;
      layer_link_split_tac
  end.

Ltac link_correct_aux_passthrough :=
  eapply layer_link_new_glbl_both;
  apply oplus_sim_monotonic; [ | apply L64_auto_sim].

Ltac link_correct_aux :=
  let M := fresh "M" in
  let HM := fresh "H" M in
  intros M HM;
  inv_link_impl HM; subst;
  eapply conseq_le_assoc_comm;
  hcomp_tac;
    [link_correct_aux_fresh |
     link_correct_aux_passthrough].

Ltac cl_backward_simulation init_correct lc :=
  let H := fresh in
  intros ? ? ? ? ? ? H;
  intros;
  eapply soundness;
  try eassumption;
  try decision;
  [ eapply lc; now eauto |
    eapply init_correct; [ | eapply make_program_oplus_right]; eassumption |
    inv_link_impl H; assumption ].

Ltac make_program_exists lc :=
  let H := fresh in
  let Hmkp := fresh "Hmkp" in
  intros ? ? ? ? H Hmkp;
  exploit lc; [eassumption | ];
  inv_link_impl H;
  eapply make_program_vertical´ in Hmkp; [ | eassumption];
  destruct Hmkp;
  simpl;
  intros;
  eapply make_program_sim_monotonic_exists;
  [ | eassumption | eassumption];
  reflexivity.

Ltac destruct_In H :=
  (solve [ destruct H ]) || (destruct H; [subst | destruct_In H]).

Lemma expand_not_in {A} (x x0: A) (xs: list A):
  ¬ In x (x0::xs) → x ≠ x0 ∧ ¬ In x xs.
Proof.
  simpl.
  intros Hx.
  split; eauto.
Qed.

Ltac destruct_not_In H :=
  match type of H with
    | ¬ In ?i _ ⇒
      let Hi := fresh "H" i in
      pose proof (expand_not_in _ _ _ H) as Hi;
      clear H;
      destruct Hi as [Hi H];
      destruct_not_In H
    | _ ⇒
      clear H
  end.

Lemma get_module_variable_le_ok (i: AST.ident) (τ: AST.globvar Ctypes.type) M:
  ModuleOK M →
  i ↦ τ ≤ M →
  get_module_variable i M = OK (Some τ).
Proof.
  intros HM Hi.
  apply (get_module_variable_monotonic i) in Hi.
  get_module_normalize_in Hi.
  specialize (HM i).
  destruct HM as [_ HMiOK _].
  inversion Hi; subst.
  - inversion H1.
    congruence.
  - inversion HMiOK.
    congruence.
Qed.

Ltac inv_get_module_variable H :=
  lazymatch type of H with get_module_variable ?i ?M = OK (Some ?vi) ⇒
    lazymatch M with context [i ↦ ?vi´] ⇒
      erewrite (get_module_variable_le_ok i vi´) in H; [|eassumption|le_oplus];
      inversion H; clear H; subst
    end
  end.

Ltac simpl_get_compiled_variable H :=
  lazymatch type of H with
    | get_module_variable ?i _ = _ ⇒
      transf_none i;
      get_module_normalize_in H;
      unfold module in *;
      repeat match goal with
        | Hv: get_module_variable i _ = _ |- _ ⇒
          rewrite Hv in H; clear Hv
      end
  end.

Ltac init_correct_data_list_valid :=
  lazymatch goal with
    | Hvi: get_module_variable ?i _ = OK (Some ?vi) |-
      InitMem.Genv.init_data_list_valid ?ge _ (AST.gvar_init ?vi) = true ⇒
      let H := fresh in
      destruct (decide (In i new_glbl)) as [H|H];
      [ destruct_In H;
        inv_get_module_variable Hvi;
        reflexivity
      | destruct_not_In H;
        simpl_get_compiled_variable Hvi;
        discriminate Hvi ]
  end.

Ltac init_correct_glbl_intros :=
  match goal with
    | |- In _ _ → _ ⇒
      let H := fresh in
      intros H;
      destruct_In H;
      init_correct_glbl_intros
    | |- _ ⇒
      intro;
      init_correct_glbl_intros
    | |- _ ⇒
      idtac
  end.

Lemma inv_init_mem `{CompCertiKOS} D s M L m:
  p <- make_program (D:=D) s M L; ret (Genv.init_mem p) = OK (Some m) →
  ∃ p,
    make_globalenv s M L = ret (Genv.globalenv p) ∧
    Genv.init_mem p = Some m.
Proof.
  intros Hm.
  inv_monad Hm.
  eapply make_program_make_globalenv in H1.
  eauto.
Qed.

Ltac inv_init_mem Hmpi :=
  let p := fresh "p" in
  let Hm := fresh "Hm" in
  let Hge := fresh "Hge" in
  let Hs := fresh "Hs" in
  pose proof (inv_init_mem _ _ _ _ _ Hmpi) as Hm;
  destruct Hm as (p & Hge & Hm);
  pose proof (make_globalenv_stencil_matches _ _ _ _ Hge) as Hs;
  inv_make_globalenv Hge;
  rewrite ?(stencil_matches_symbols _ _ Hs) in ×.

Ltac init_correct_sim_mem :=
  let Hmpi := fresh "Hmpi" in
  intros ? ? ? Hmpi;
  inv_init_mem Hmpi;
  constructor; econstructor;
  simpl; trivial using FlatMem.flatmem_empty_inj;
  match goal with
    | |- val_inject _ Vzero Vzero ⇒ econstructor
    | |- kctxt_inj _ _ _ _ ⇒
      repeat intro;
      unfold Pregmap.get;
      rewrite ?Maps.ZMap.gi, ?Pregmap.gi;
      constructor
    | |- uctxt_inj _ _ _ ⇒
      repeat intro;
      unfold Pregmap.get;
      rewrite ?Maps.ZMap.gi, ?Pregmap.gi;
      constructor
    | |- VMCS_inj _ _ _ ⇒
      constructor;
      repeat intro;
      unfold Pregmap.get;
      rewrite ?Maps.ZMap.gi, ?Pregmap.gi;
      constructor
    | |- VMX_inj _ _ _ ⇒
      constructor;
      repeat intro;
      unfold Pregmap.get;
      rewrite ?Maps.ZMap.gi, ?Pregmap.gi;
      constructor
    | |- find_symbol _ _ = Some _ ⇒
      eassumption
    | |- _ ⇒
      idtac
  end.

Ltac init_correct_glbl :=
  init_correct_glbl_intros;
  match goal with
    | |- InitMem.Genv.init_data_list_valid _ _ _ = true ⇒
      init_correct_data_list_valid
    | |- isOKNone _ ⇒
      reflexivity
    | |- isOKNone (get_layer_globalvar ?i _) ⇒
      revert i;
      decision
   | H: context [?i ↦ ?vi]
     |- ∃ vi, get_module_variable ?i ?M = OK (Some vi) ⇒
     ∃ vi;
     eapply (get_module_variable_le_ok i); [ assumption | le_oplus ]
    | |- _ ⇒
      idtac
  end.

Ltac init_correct :=
  let HM := fresh "HM" in
  intros ? HM ?;
  inv_link_impl HM;
  subst;
  apply cl_init_sim_intro; [ init_correct_sim_mem | init_correct_glbl .. ].