Library mcertikos.multithread.SingleProcessor_Refinement

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.

Require Import liblayers.compat.CompatGenSem.
Require Import LAsmModuleSemEvent.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.

Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.
Require Import AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleOracle.
Require Import AbstractDataType.
Require Export ObjMultiprocessor.

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

Require Import HAsm.
Require Import TAsm.
Require Import EAsm.
Require Import IIEAsm.
Require Import LAsm.

Require Import AsmPHThread2T.
Require Import AsmT2IIE.
Require Import AsmIIE2IIE.
Require Import AsmIIE2E.
Require Import AsmE2L.

Require Import GlobalOracleProp.
Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.

Require Import PHThread.
Require Import PHBThread.
Require Import PBThread.

Require Import PHThread2TGenDef.
Require Import PHThread2TGen.

Require Import E2PBThreadGenDef.
Require Import E2PBThreadGen.

Section SingleProcessorRefinementTheorem.

  Context `{multi_oracle_prop : MultiOracleProp}.
  Context `{s_oracle_ops : SingleOracleOps}.
  Context `{s_threads_ops: ThreadsConfigurationOps}.
  Context `{real_params : RealParams}.

  Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
  Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
                                      (s_threads_ops := s_threads_ops)}.
  Context `{Hmem: Mem.MemoryModelX}.

  Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.

  Existing Instance SingleOracleImpl.s_oracle_prf.
  Existing Instance SingleOracleImpl.s_oracle_prop_prf.
  Existing Instance SingleOracleImpl.s_config.

  Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
                                           (s_threads_ops := s_threads_ops)}.

  Existing Instance SingleOracleImpl.s_link_config.

  Context `{Hmwd: UseMemWithData mem}.
  Context `{acc_def: !AccessorsDefined (stencil := stencil) (phbthread ⊕ L64)}.

  Context `{extcallsx: !ExternalCallsXDefined (phbthread ⊕ L64)}.

  Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData))
    := CompatExternalCalls.compatlayer_extcall_ops (phbthread ⊕ L64).

  Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops (phbthread ⊕ L64).

  Context `{tasm_primcall_props: !PrimcallProperties TAsm.sprimitive_call}.
  Context `{ieasm_primcall_props: !PrimcallProperties IIEAsm.sprimitive_call}.
  Context `{easm_primcall_props: !PrimcallProperties EAsm.sprimitive_call}.

  Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.

  Existing Instance PHThread2TGen.abs_relT.

  Theorem HThread2T_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
      (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (HAsm.semantics (phthread ⊕ L64) ph)
        (TAsm.tsemantics ph).
  Proof.
    intros.
    apply @AsmPHThread2T.cl_backward_simulation with (s:= s) (CTXT := CTXT); try auto.
    eapply PHThread2TGen.abs_relT.
  Qed.

  Theorem T2IIE_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
      (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (TAsm.tsemantics ph)
        (IIEAsm.iesemantics (current_thread::nil) ph).
  Proof.
    intros.
    apply @AsmT2IIE.cl_backward_simulation with (s := s) (CTXT := CTXT); try auto.
    typeclasses eauto.
  Qed.

  Existing Instance algebraicmem.
  Context `{ie2ie_rel: !IE2IERel}.

  Theorem IIE2IIE_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
      (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (IIEAsm.iesemantics (current_thread::nil) ph)
        (IIEAsm.iesemantics (full_thread_list) ph).
  Proof.
    intros.
    apply @AsmIIE2IIE.cl_backward_simulation with (s := s) (CTXT := CTXT); try auto.
    typeclasses eauto.
  Qed.

  Context `{lasm_abs_data: !LAsmAbsDataProp}.

  Theorem IIE2E_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
      (Hs: genv_next s = init_nb)
      (Hph: noglobvar ph)
      (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (IIEAsm.iesemantics (full_thread_list) ph)
        (EAsm.esemantics (full_thread_list) ph).
  Proof.
    intros.
    apply @AsmIIE2E.cl_backward_simulation with (s := s) (CTXT := CTXT); try auto.
    typeclasses eauto.
  Qed.

  Context `{e2pbthread_gen_prop: !E2PBThreadGenProp s_oracle_prf}.

  Existing Instance E2PBThreadGen.abs_rel.
  Existing Instance LAsm.asm_init_default.

  Theorem E2BThread_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
           (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (EAsm.esemantics full_thread_list ph)
        (LAsm.semantics (lcfg_ops := LC (pbthread ⊕ L64)) ph).
  Proof.
    intros.
    eapply @AsmE2L.cl_backward_simulation with (s := s) (multi_oracle_prop := multi_oracle_prop) (CTXT := CTXT) (ph := ph).
    auto.
    auto.
    apply E2PBThreadGen.abs_rel.
    auto.
  Qed.

  Theorem SingleCore_backward_simulation:
    ∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
           (Hs: genv_next s = init_nb)
           (Hph: noglobvar ph)
           (Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (phbthread ⊕ L64) = OK ph),
      backward_simulation
        (HAsm.semantics (phthread ⊕ L64) ph)
        (LAsm.semantics (lcfg_ops := LC (pbthread ⊕ L64)) ph).
  Proof.
    intros.
    eapply compose_backward_simulation.
    - apply LAsmModuleSemEvent.LAsm_single_events;
        [ Decision.decision | assumption ].
    - eapply HThread2T_backward_simulation; eauto.
    - eapply compose_backward_simulation.
      + apply LAsmModuleSemEvent.LAsm_single_events;
          [ Decision.decision | assumption ].
      + eapply T2IIE_backward_simulation; eauto.
      + eapply compose_backward_simulation.
        × apply LAsmModuleSemEvent.LAsm_single_events;
            [ Decision.decision | assumption ].
        × eapply IIE2IIE_backward_simulation; eauto.
        × eapply compose_backward_simulation.
          { apply LAsmModuleSemEvent.LAsm_single_events;
              [ Decision.decision | assumption ]. }
          { eapply IIE2E_backward_simulation; eauto. }
          { eapply E2BThread_backward_simulation; eauto. }
  Qed.

End SingleProcessorRefinementTheorem.