Library mcertikos.multicore.Concurrent_Linking

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.

Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.

Require Import liblayers.compat.CompatGenSem.
Require Import TacticsForTesting.

Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.

Require Import HWStepSemImpl.
Require Import OracleSemImpl.
Require Import EnvSemImpl.
Require Import SingleSemImpl.
Require Import BigSemImpl.
Require Import Big2SemImpl.
Require Import SplitSemImpl.
Require Import ReorderSemImpl.
Require Import SeparateSemImpl.

Require Import AsmOracleSemtoHWStepSem.
Require Import AsmEnvSemtoOracleSem.
Require Import AsmEnvSemtoEnvSem.
Require Import AsmSingleSemtoEnvSem.
Require Import AsmBigSemtoSingleSem.
Require Import AsmBig2SemtoBigSem.
Require Import AsmSplitSemtoBig2Sem.
Require Import AsmReorderSemtoSplitSem.
Require Import AsmReorderSemtoReorderSem.
Require Import AsmSepSemtoReorderSem.
Require Import AsmLAsmtoSepSem.

Section LinkWithLAsmSim.

  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.

  Notation LDATA := RData.
  Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).

  Local Open Scope Z_scope.

  Context `{pmap: PartialMap}.
  Context `{zset_op: ZSet_operation}.

  Context `{mc_oracle_cond: MCLinkOracleCond (mem := mem) (memory_model_ops := memory_model_ops) (Hmwd := Hmwd)
                                             (Hmem := Hmem) (real_params_ops := real_params_ops)
                                             (oracle_ops0 := oracle_ops0) (oracle_ops := oracle_ops) (big_ops := big_ops)
                                             (builtin_idents_norepet_prf := builtin_idents_norepet_prf)
                                             (zset_op := zset_op) (pmap := pmap)}.

  Theorem concurrent_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
           (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (mboot ⊕ L64) = OK ph),
      backward_simulation
        (LAsm.semantics (lcfg_ops := LC (mboot ⊕ L64)) ph)
        (hwstep_semantics
           (Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
           (Genv.globalenv ph) s CTXT ph).
  Proof.
    intros.
    eapply compose_backward_simulation.
    - eapply hwstep_semantics_single_events.
    - eapply AsmLAsmtoSepSem.cl_backward_simulation.
    - eapply compose_backward_simulation.
      + eapply hwstep_semantics_single_events.
      + eapply AsmSepSemtoReorderSem.cl_backward_simulation.
      + eapply compose_backward_simulation.
        × eapply hwstep_semantics_single_events.
        × eapply AsmReorderSemtoReorderSem.cl_backward_simulation.
        × eapply compose_backward_simulation.
          { eapply hwstep_semantics_single_events. }
          { eapply AsmReorderSemtoSplitSem.cl_backward_simulation. }
          { eapply compose_backward_simulation.
            - eapply hwstep_semantics_single_events.
            - eapply AsmSplitSemtoBig2Sem.cl_backward_simulation.
            - eapply compose_backward_simulation.
              + eapply hwstep_semantics_single_events.
              + eapply AsmBig2SemtoBigSem.cl_backward_simulation.
              + eapply compose_backward_simulation.
                × eapply hwstep_semantics_single_events.
                × eapply AsmBigSemtoSingleSem.cl_backward_simulation.
                × eapply compose_backward_simulation.
                  { eapply hwstep_semantics_single_events. }
                  { eapply AsmSingleSemtoEnvSem.cl_backward_simulation. }
                  { eapply compose_backward_simulation.
                    - eapply hwstep_semantics_single_events.
                    - eapply AsmEnvSemtoEnvSem.cl_backward_simulation.
                    - eapply compose_backward_simulation.
                      + eapply hwstep_semantics_single_events.
                      + eapply AsmEnvSemtoOracleSem.cl_backward_simulation.
                      + eapply AsmOracleSemtoHWStepSem.cl_backward_simulation. } }
  Qed.

End LinkWithLAsmSim.