Library mcertikos.mm.PTOpGenLink

Require Import MPTIntro.
Require Import MPTOp.
Require Import MPTIntroCode.
Require Import PTOpGen.
Require Import PTOpGenSpec.
Require Import MPTIntroCSource.
Require Import LinkTemplate.
Require Import LinkTactic.
Require Import PTOpGenLinkSource.

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


  Notation HDATA := AbstractDataType.RData.
  Notation LDATA := AbstractDataType.RData.

  Notation HDATAOps := (cdata HDATA).
  Notation LDATAOps := (cdata LDATA).

  Require Import Coqlib.
  Require Import FlatMemory.
  Require Import Decision.
  Require Import LAsmModuleSem.
  Require Import Soundness.
  Require Import CompatExternalCalls.

  Lemma init_correct:
    ∀ M, MPTOp_impl = OK M →
              ModuleOK M →
              cl_init_sim HDATAOps LDATAOps (crel HDATA LDATA) (mptop ⊕ L64) M (mptintro ⊕ L64).
  Proof.
    intros.
    pose proof (fun i ⇒ module_ok_variable M i (H0 i)) as MOK; clear H0.
    apply cl_init_sim_intro.
    - constructor; simpl; trivial.
      constructor; simpl; trivial. apply FlatMem.flatmem_empty_inj.
      + econstructor.
      + constructor.
    - intros; inv H0.
    - intros; inv H0.
    - intros; inv H0.
    - intros.
      inv_link_impl H; subst.
      transf_none i. specialize (MOK i).
      assert (get_module_variable i (((M6 ⊕ M5 ⊕ M4 ⊕ M3 ⊕ M2 ⊕ M1 ⊕ M0 ⊕ ∅) ⊕ ∅) ⊕ ∅) = OK None).
      {
        get_module_variable_relfexivity.
      }
      congruence.
    - decision.
  Qed.

  Lemma link_correct_aux:
    ∀ M, MPTOp_impl = OK M →
              mptintro ⊕ L64
                    ⊢ (path_inj (crel _ _), M)
              : mptop ⊕ L64.
  Proof.
    link_correct_aux.
    - link_cfunction ptRead_spec_ref MPTINTROCODE.pt_read_code_correct.
    - link_cfunction ptReadPDE_spec_ref MPTINTROCODE.pt_read_pde_code_correct.
    - link_cfunction ptInsertAux_spec_ref MPTINTROCODE.pt_insert_aux_code_correct.
    - link_cfunction ptInsertPDE_spec_ref MPTINTROCODE.pt_insert_pde_code_correct.
    - link_cfunction ptRmvAux_spec_ref MPTINTROCODE.pt_rmv_aux_code_correct.
    - link_cfunction ptRmvPDE_spec_ref MPTINTROCODE.pt_rmv_pde_code_correct.
    - link_cfunction idpde_init_spec_ref MPTINTROCODE.idpde_init_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    ∀ (s: stencil) (CTXT M: module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      MPTOp_impl = OK M →
      make_program s CTXT (mptop ⊕ L64) = OK ph →
      make_program s (CTXT ⊕ M) (mptintro ⊕ L64) = OK pl →
      backward_simulation
        (LAsm.semantics (lcfg_ops := LC (mptop ⊕ L64)) ph)
        (LAsm.semantics (lcfg_ops := LC (mptintro ⊕ L64)) pl).
  Proof.
    intros.
    eapply (soundness (crel HDATA LDATA)); try eassumption; try decision.

    eapply link_correct_aux; eauto.
    eapply init_correct; eauto.
    eapply make_program_oplus_right; eassumption.

    inv_link_impl H; subst.
    assumption.
  Qed.

  Require Import LAsmModuleSemMakeProgram.

  Theorem make_program_exists:
    ∀ (s: stencil) (CTXT M: module) pl,
      MPTOp_impl = OK M →
      make_program s (CTXT ⊕ M) (mptintro ⊕ L64) = OK pl →
      ∃ ph, make_program s CTXT (mptop ⊕ L64) = OK ph.
  Proof.
    intros.
    exploit link_correct_aux; eauto.
    eapply make_program_vertical´ in H0.
    destruct H0 as [p´ Hmake].
    intros Hle.
    eapply make_program_sim_monotonic_exists.
    2: eapply Hle.
    reflexivity.
    eassumption.

    inv_link_impl H; subst.
    assumption.
  Qed.

End WITHCOMPCERTIKOS.