Library mcertikos.proc.AbQueueGenLink

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import VCGen.
Require Import RealParams.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import I64Layer.
Require Import CompCertiKOSproof.
Require Import LinkTactic.
Require Import LayerCalculusLemma.
Require Import PQueueInit.
Require Import PAbQueue.
Require Import AbQueueGen.

Section WITHCOMPCERTIKOS.

  Context `{compcertikos_prf: CompCertiKOS}.

  Context `{real_params_prf : RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{multi_oracle_link: !MultiOracleLink}.

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

  Notation HDATAOps := (cdata (cdata_ops := pabqueue_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := pqueueinit_data_ops) LDATA).

  Lemma link_correct_aux:
              pqueueinit ⊕ L64
                    ⊢ (path_inj (crel HDATA LDATA), ∅)
              : pabqueue ⊕ L64.
  Proof.
    eapply layer_link_new_glbl_both.
    apply oplus_sim_monotonic.
    apply passthrough_correct.
    apply L64_auto_sim.
  Qed.

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

  Lemma init_correct:
    cl_init_sim (mops := module_ops)
                HDATAOps LDATAOps (crel HDATA LDATA)
                (pabqueue ⊕ L64) ∅ (pqueueinit ⊕ L64).
  Proof.
    apply cl_init_sim_intro.
    - constructor; simpl; trivial.
      constructor; simpl; trivial. apply FlatMem.flatmem_empty_inj.
      constructor.
      + apply kctxt_inj_empty.
      +
        constructor.
        ×
          intros qi l qi_range.
          rewrite ZMap.gi.
          discriminate.
        ×
          intros i tds inq i_range.
          rewrite ZMap.gi.
          discriminate.
      + eapply relateabtcb.       + constructor.
        × reflexivity.
        × intros i Hi.
          rewrite !ZMap.gi.
          constructor.
      + constructor.
    - intros _ [].
    - intros _ [].
    - intros _ [].
    - intros.
      assert (get_module_variable (ModuleOps := module_ops) i ∅ = OK None)
        by get_module_variable_relfexivity.
      congruence.
    - decision.
  Qed.

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

    eapply link_correct_aux; eauto.
    eapply init_correct; eauto.
  Qed.

  Require Import LAsmModuleSemMakeProgram.

  Theorem make_program_exists:
    ∀ (s: stencil) (CTXT : module) pl,
      make_program s (CTXT ⊕ ∅) (pqueueinit ⊕ L64) = OK pl →
      ∃ ph, make_program s CTXT (pabqueue ⊕ L64) = OK ph.
  Proof.
    intros.
    eapply make_program_vertical´ in H.
    destruct H as [p´ Hmake].
    assert (Hle := link_correct_aux).
    eapply make_program_sim_monotonic_exists.
    2: eapply Hle.
    reflexivity.
    eassumption.

    decision.
  Qed.

End WITHCOMPCERTIKOS.