Library mcertikos.multicore.refins.AsmSepSemtoReorderSem

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 SeparateSemImpl.
Require Import ReorderSemImpl.

Section LinkwithLAsm.

  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}.

  Existing Instance hdseting.
  Existing Instance op_sep.

  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)}.

  Section WITH_GE.

    Variables (ge: genv) (sten: stencil) (M: module).
    Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
                                       sten M (mboot ⊕ L64) = ret ge}.

    Definition single_reorder_step_aux_ge´ :=
      @single_reorder_step_aux_ge mem memory_model_ops Hmem Hmwd
                                  real_params_ops oracle_ops0 oracle_ops big_ops
                                  builtin_idents_norepet_prf zset_op
                                  ge sten M Hmakege reorder_oracle_red.

    Definition single_separate_step_aux_ge´ :=
      @single_separate_step_aux_ge mem memory_model_ops Hmem Hmwd
                                   real_params_ops oracle_ops0 oracle_ops big_ops
                                   builtin_idents_norepet_prf zset_op mc_oracle
                                   ge sten M Hmakege.

    Lemma single_reorder_step_aux_eq :
      ∀ (ge:genv) sten M
             (Hmakege: make_globalenv sten M (mboot ⊕ L64) = ret ge)
             s t s´ o,
        single_reorder_step_aux_ge ge sten M (Hmakege:=Hmakege) o ge s t s´ ↔
        single_reorder_step_aux ge sten M (Hmakege:=Hmakege) o s t s´.
    Proof.
      intros; split; intros.
      inversion H; auto.
      constructor; auto.
    Qed.

    Lemma single_separate_step_aux_eq :
      ∀ s t s´,
        single_separate_step_aux_ge ge sten M
                                    (Hmakege:=Hmakege) ge s t s´ ↔
        single_separate_step_aux ge sten M (Hmakege:=Hmakege) s t s´.
    Proof.
      intros; split; intros.
      inversion H; auto.
      constructor; auto.
    Qed.

    Definition match_spstate_link := match_spstate (hdset := hdseting) current_CPU_ID.

    Hint Unfold match_spstate_link.

    Existing Instance op_reorder.
    Existing Instance op_sep.

    Lemma one_step_reorder_refines_separate_concrete:
      ∀ s s0 s´ t
             (Hone: single_separate_step_aux_ge´ ge s t s´)
             (Hmatch: match_spstate_link s s0)
           ,
      ∃ s0´,
        single_reorder_step_aux_ge´ ge s0 t s0´
        ∧ match_spstate_link s´ s0´.
    Proof.
      simpl in ×.
      unfold single_separate_step_aux_ge´.
      unfold single_reorder_step_aux_ge´.
      intros.
      rewrite single_separate_step_aux_eq in Hone.
      unfold single_reorder_step_aux in Hone; simpl in ×.
      unfold match_spstate_link in Hmatch.
      eapply one_step_reorder_refines_separate in Hone; eauto; [ | inv mc_oracle_cond; eauto | inv mc_oracle_cond; eauto].
      destruct Hone as (s0´ & Hone1 & Hone2).
      ∃ s0´.
      split; auto.
      rewrite single_reorder_step_aux_eq.
      unfold single_reorder_step_aux; simpl; eauto. About valid_oracle´.
    Qed.

  End WITH_GE.

End LinkwithLAsm.

Section LinkSim.

  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 cl_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
        (single_separate_semantics
           (Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
           (Genv.globalenv ph) s CTXT ph)
        (single_reorder_semantics
           (Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
           (Genv.globalenv ph) s CTXT reorder_oracle_red ph).
  Proof.
    intros. apply forward_to_backward_simulation; eauto.
    - eapply forward_simulation_plus with
          (match_states:= match_spstate_link); intros; eauto; simpl in *; unfold match_spstate_link in *;
        simpl in ×.
      + inv H.
        ∃ (RState (hdset := hdseting) (Asm.State rs0 m0) nil).
        split.
        × constructor; eauto.
        × constructor; eauto.
          { unfold valid_log´; simpl; auto. }
          { constructor.
            intros.
            rewrite ZMap.gi in H; subst.
            simpl; auto. }
      + generalize one_step_reorder_refines_separate_concrete; simpl.
        unfold single_separate_step_aux_ge´.
        unfold single_reorder_step_aux_ge´.
        unfold match_spstate_link.
        intros Hstep.
        exploit Hstep; eauto.
        intros.
        destruct H1 as (s0´ & H1 & H2).
        ∃ s0´.
        split; auto.
        apply plus_one; auto.
    -
      eapply single_separate_semantics_receptive.
    -
      eapply single_reorder_semantics_determinate; eauto.
  Qed.

End LinkSim.