Library mcertikos.conlib.conmtlib.EAsmComposeRefinement

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
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 CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.

Require Import LAsm.
Require Import EAsmCommon.
Require Import EAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleConfiguration.
Require Import EAsmCompose.
Require Import EAsmPropLib.

Section Refinement.

  Context `{s_link_config : SingleLinkConfiguration}.
  Context `{Hmwd: UseMemWithData mem}.

  Context `{data_prf : CompatData PData}.
  Context `{Hstencil: Stencil}.

  Context `{L: compatlayer (cdata PData)}.

  Context `{ass_def: !AccessorsDefined L}.
  Context `{lasmops: !LAsmAbsDataProp}.

  Local Instance : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.

  Local Instance : LayerConfigurationOps := compatlayer_configuration_ops L.

  Opaque Z.to_nat.

  Notation mestate := (estate (mem:= mem)).

  Class Compose_Reinfment_Prop :=
    {
      compose_relation: mestate → mestate → mestate → Prop;
      compose_lemma: ∀ ge st1 st1´ st2 st2´ st
                            (Hstar1: star estep ge st1 E0 st1´)
                            (Hstar2: star estep ge st2 E0 st2´)
                            (Hcompose: compose_relation st st1 st2),
                     ∃ st´, star estep ge st E0 st´
                                 ∧ compose_relation st´ st1´ st2´;
      refinement_relation: mestate → mestate → Prop;
      refinement: ∀ ge st1 st1´ st2
                         (Hstar: star estep ge st1 E0 st1´)
                         (Hrel: refinement_relation st1 st2),
                  ∃ st2´, star estep ge st2 E0 st2´
                               ∧ refinement_relation st1´ st2´
    }.

  Section WITH_PROP.

    Context `{crprop: Compose_Reinfment_Prop}.

    Theorem star_step_EAsm_compose_refinement:
      ∀ ge st1 st1´ st2 st2´ st10 st20 st
             (Hstar1: star estep ge st1 E0 st1´)
             (Hstar2: star estep ge st2 E0 st2´)
             (Hrel1: refinement_relation st1 st10)
             (Hrel2: refinement_relation st2 st20)
             (Hcompose: compose_relation st st10 st20),
        ∃ st´ st10´ st20´,
          star estep ge st E0 st´
          ∧ refinement_relation st1´ st10´
          ∧ refinement_relation st2´ st20´
          ∧ compose_relation st´ st10´ st20´.
    Proof.
      intros.
      eapply refinement in Hstar1; eauto.
      destruct Hstar1 as (st10´ & Hstar1 & Hrel1´).
      eapply refinement in Hstar2; eauto.
      destruct Hstar2 as (st20´ & Hstar2 & Hrel2´).
      exploit compose_lemma; try eapply Hcompose; eauto.
      intros (st´ & Hstar & Hcom).
      refine_split´; eauto.
    Qed.

  End WITH_PROP.

  Section WITH_PROP2.

    Context `{crprop: Compose_Reinfment_Prop}.

    Class Compose_Reinfment_Prop2 :=
      {
        decompose_lemma: ∀ ge st1 st2 st st´
                                (Hstar: star estep ge st E0 st´)
                                (Hcompose: compose_relation st st1 st2),
                         ∃ st1´ st2´, star estep ge st1 E0 st1´
                                           ∧ star estep ge st2 E0 st2´
                                           ∧ compose_relation st´ st1´ st2´
      }.

    Context `{crprop2: Compose_Reinfment_Prop2}.

    Theorem star_step_EAsm_compose_soundness´:
      ∀ ge st1 st2 st10 st20 st st´ st0
             (Hstar: star estep ge st E0 st´)
             (Hrel1: refinement_relation st1 st10)
             (Hrel2: refinement_relation st2 st20)
             (Hcompose: compose_relation st st1 st2)
             (Hcompose0: compose_relation st0 st10 st20),
      ∃ st1´ st2´ st0´ st10´ st20´,
        star estep ge st0 E0 st0´
        ∧ refinement_relation st1´ st10´
        ∧ refinement_relation st2´ st20´
        ∧ compose_relation st´ st1´ st2´
        ∧ compose_relation st0´ st10´ st20´.
    Proof.
      intros.
      eapply decompose_lemma in Hstar; eauto.
      destruct Hstar as (st1´ & st2´ & Hstar1 & Hstar2 & Hcompose´).
      exploit star_step_EAsm_compose_refinement;
        try eapply Hcompose0; try eapply Hrel1; try eapply Hrel2; eauto.
      intros (st´0 & st10´ & st20´ & Hstar0 & Hrel10 & Hrel20 & Hcompose0´).
      refine_split´.
      - eauto.
      - eapply Hrel10.
      - eapply Hrel20.
      - trivial.
      - trivial.
    Qed.

    Inductive new_relation: mestate → mestate → Prop :=
    | NEW_RELATION_INTRO:
        ∀ st st0 st1 st2 st10 st20
             (Hrel1: refinement_relation st1 st10)
             (Hrel2: refinement_relation st2 st20)
             (Hcompose: compose_relation st st1 st2)
             (Hcompose0: compose_relation st0 st10 st20),
          new_relation st st0.

    Theorem star_step_EAsm_compose_soundness:
      ∀ ge st st´ st0
             (Hstar: star estep ge st E0 st´)
             (Hrel: new_relation st st0),
      ∃ st0´,
        star estep ge st0 E0 st0´
        ∧ new_relation st´ st0´.
    Proof.
      intros. inv Hrel.
      exploit star_step_EAsm_compose_soundness´.
      { eapply Hstar. }
      { eapply Hrel1. }
      { eapply Hrel2. }
      { eauto. }
      { eauto. }
      intros (st1´ & st2´ & st0´ & st10´ & st20´ & Hstar0 & Hrel10 & Hrel20 & Hcompose0´ & Hcompose0´´).
      refine_split´; eauto.
      econstructor.
      - eapply Hrel10.
      - eapply Hrel20.
      - trivial.
      - trivial.
    Qed.

  End WITH_PROP2.

End Refinement.