Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.

Require Import AbstractDataType.
Require Import MMCSLockAbsIntro.
Require Import MCSLockAbsIntroGenSpec.
Require Import DeviceStateDataType.

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.
  Context `{mcs_oracle_prop: MCSOracleProp}.

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

  Notation HDATAOps := (cdata (cdata_ops := mmcslockabsintro_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := mcurid_data_ops) LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
      mkrelate_RData {
          flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
          MM_re: MM hadt = MM ladt;
          MMSize_re: MMSize hadt = MMSize ladt;
          vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
          CR3_re: CR3 hadt = CR3 ladt;
          ikern_re: ikern hadt = ikern ladt;
          pg_re: pg hadt = pg ladt;
          ihost_re: ihost hadt = ihost ladt;
          ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
          ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
          init_re: init hadt = init ladt;

          CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
          cid_re: cid hadt = cid ladt;
          multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
          multi_log_re: multi_log hadt = multi_log ladt;
          com1_re: com1 ladt = com1 hadt;
          ioapic_re: ioapic ladt = ioapic hadt;
          lapic_re: lapic ladt = lapic hadt;
          intr_flag_re: intr_flag ladt = intr_flag hadt;
          saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
          curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
          in_intr_re: in_intr hadt = in_intr ladt;
          tf_re: tfs_inj f (tf hadt) (tf ladt)

        }.

    Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
    | MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.

    Local Hint Resolve MATCH_RDATA.

    Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
      {
        relate_AbData s f d1 d2 := relate_RData f d1 d2;
        match_AbData s d1 m f := match_RData s d1 m f;
        new_glbl := nil
      }.

    Section Rel_Property.

      Lemma relate_incr:
        ∀ abd abd´ f f´,
          relate_RData f abd abd´
          → inject_incr f f´
          → relate_RData f´ abd abd´.
      Proof.
        inversion 1; subst; intros; inv H; constructor; eauto.
        eapply tfs_inj_incr; eauto.
      Qed.

      Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
      Proof.
        constructor; intros; simpl; trivial.
        eapply relate_incr; eauto.
      Qed.

    End Rel_Property.

    Section OneStep_Forward_Relation.

      Section FRESH_PRIM.

        Lemma ticket_lock_init_kern_mode:
          ∀ i d d´,
            ticket_lock_init_spec i d = Some d´
            → kernel_mode d.
        Proof.
          unfold ticket_lock_init_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma ticket_lock_init_exist:
          ∀ habd habd´ labd lock_index f,
            ticket_lock_init_spec lock_index habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, ticket_lock_init_spec lock_index labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold ticket_lock_init_spec; intros until f; exist_simpl.
        Qed.

        Lemma ticket_lock_init_spec_ref:
          compatsim (crel HDATA LDATA) (gensem ticket_lock_init_spec) mcs_lock_init_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit ticket_lock_init_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply ticket_lock_init_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_get_next_kern_mode:
          ∀ lock_index curid d d´ n,
            mcs_get_next_spec lock_index curid d = Some (d´, n)
            → kernel_mode d.
        Proof.
          unfold mcs_get_next_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_get_next_exist:
          ∀ habd habd´ labd lock_index curid n f,
            mcs_get_next_spec lock_index curid habd = Some (habd´, n)
            → relate_RData f habd labd
            → ∃ labd´, mcs_get_next_spec lock_index curid labd = Some (labd´, n) ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_get_next_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_get_next_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_get_next_spec) mcs_get_next_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_get_next_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_get_next_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_set_next_kern_mode:
          ∀ lock_index curid next d d´,
            mcs_set_next_spec lock_index curid next d = Some d´
            → kernel_mode d.
        Proof.
          unfold mcs_set_next_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_set_next_exist:
          ∀ habd habd´ labd lock_index curid next f,
            mcs_set_next_spec lock_index curid next habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, mcs_set_next_spec lock_index curid next labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_set_next_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_set_next_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_set_next_spec) mcs_set_next_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_set_next_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_set_next_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_get_busy_kern_mode:
          ∀ lock_index curid d d´ n,
            mcs_get_busy_spec lock_index curid d = Some (d´, n)
            → kernel_mode d.
        Proof.
          unfold mcs_get_busy_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_get_busy_exist:
          ∀ habd habd´ labd lock_index curid n f,
            mcs_get_busy_spec lock_index curid habd = Some (habd´, n)
            → relate_RData f habd labd
            → ∃ labd´, mcs_get_busy_spec lock_index curid labd = Some (labd´, n) ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_get_busy_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_get_busy_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_get_busy_spec) mcs_get_busy_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_get_busy_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_get_busy_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_set_busy_kern_mode:
          ∀ lock_index curid d d´,
            mcs_set_busy_spec lock_index curid d = Some d´
            → kernel_mode d.
        Proof.
          unfold mcs_set_busy_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_set_busy_exist:
          ∀ habd habd´ labd lock_index curid f,
            mcs_set_busy_spec lock_index curid habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, mcs_set_busy_spec lock_index curid labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_set_busy_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_set_busy_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_set_busy_spec) mcs_set_busy_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_set_busy_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_set_busy_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_swap_tail_kern_mode:
          ∀ bound lock_index curid d d´ n,
            mcs_swap_tail_spec bound lock_index curid d = Some (d´, n)
            → kernel_mode d.
        Proof.
          unfold mcs_swap_tail_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_swap_tail_exist:
          ∀ habd habd´ labd bound lock_index curid n f,
            mcs_swap_tail_spec bound lock_index curid habd = Some (habd´, n)
            → relate_RData f habd labd
            → ∃ labd´, mcs_swap_tail_spec bound lock_index curid labd = Some (labd´, n) ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_swap_tail_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_swap_tail_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_swap_tail_spec) mcs_swap_tail_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_swap_tail_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_swap_tail_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_cas_tail_kern_mode:
          ∀ lock_index curid d d´ n,
            mcs_cas_tail_spec lock_index curid d = Some (d´, n)
            → kernel_mode d.
        Proof.
          unfold mcs_cas_tail_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_cas_tail_exist:
          ∀ habd habd´ labd lock_index curid n f,
            mcs_cas_tail_spec lock_index curid habd = Some (habd´, n)
            → relate_RData f habd labd
            → ∃ labd´, mcs_cas_tail_spec lock_index curid labd = Some (labd´, n) ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_cas_tail_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_cas_tail_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_cas_tail_spec) mcs_cas_tail_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_cas_tail_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_cas_tail_kern_mode; eauto.
          - constructor.
        Qed.

        Lemma mcs_lock_get_index_kern_mode:
          ∀ lock_id offset d d´ n,
            mcs_lock_get_index_spec lock_id offset d = Some (d´, n)
            → kernel_mode d.
        Proof.
          unfold mcs_lock_get_index_spec; simpl; intros.
          subdestruct; auto.
        Qed.

        Lemma mcs_lock_get_index_exist:
          ∀ habd habd´ labd lock_id offset n f,
            mcs_lock_get_index_spec lock_id offset habd = Some (habd´, n)
            → relate_RData f habd labd
            → ∃ labd´, mcs_lock_get_index_spec lock_id offset labd = Some (labd´, n) ∧ relate_RData f habd´ labd´.
        Proof.
          unfold mcs_lock_get_index_spec; intros until f; exist_simpl.
        Qed.

        Lemma mcs_lock_get_index_spec_ref:
          compatsim (crel HDATA LDATA) (gensem mcs_lock_get_index_spec) mcs_lock_get_index_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit mcs_lock_get_index_exist; eauto 1.
          intros [labd´ [HP HM]].
          refine_split; try econstructor; eauto.
          - eapply mcs_lock_get_index_kern_mode; eauto.
          - constructor.
        Qed.

      End FRESH_PRIM.

      Section PASSTHROUGH_RPIM.

        Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
        Proof.
          accessor_prop_tac.
          - eapply flatmem_store´_exists; eauto.
        Qed.

        Lemma passthrough_correct:
          sim (crel HDATA LDATA) mmcslockabsintro_passthrough mmcslockintro.
        Proof.
          sim_oplus.
          - apply fload´_sim.
          - apply fstore´_sim.
          - apply page_copy´´´_sim.
          - apply page_copy_back´_sim.
          - apply vmxinfo_get_sim.
          - apply setPG_sim.
          - apply setCR3_sim.
          - apply get_size_sim.
          - apply is_mm_usable_sim.
          - apply get_mm_s_sim.
          - apply get_mm_l_sim.
          - apply get_CPU_ID_sim.
          - apply release_shared0_sim.
          - apply (acquire_shared0_mcs_sim (valid_id_args:= Shared2ID_valid0)).
            intros. inv H.
          - apply get_curid_sim.
          - apply set_curid_sim.
          - apply set_curid_init_sim.
          - apply trapin_sim.
          - apply trapout´_sim.
          - apply hostin_sim.
          - apply hostout´_sim.
          - apply proc_create_postinit_sim.
          - apply trap_info_get_sim.
          - apply trap_info_ret_sim.
          - apply serial_irq_check_sim.
          - apply iret_sim.
          - apply cli_sim.
          - apply sti_sim.
          - apply serial_irq_current_sim.
          - apply ic_intr_sim.
          - apply save_context_sim.
          - apply restore_context_sim.
          - apply local_irq_save_sim.
          - apply local_irq_restore_sim.
          - apply serial_in_sim.
          - apply serial_out_sim.
          - apply serial_hw_intr_sim.
          - apply ioapic_read_sim.
          - apply ioapic_write_sim.
          - apply lapic_read_sim.
          - apply lapic_write_sim.
          - layer_sim_simpl.
            + eapply load_correct1.
            + eapply store_correct1.
        Qed.

      End PASSTHROUGH_RPIM.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.