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 LoadStoreSem2.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.

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 LAsmModuleSemAux.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.

Require Import PThreadSched.
Require Import PThread.
Require Import ThreadGenSpec.

Section Refinement.

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

  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

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

  Notation HDATAOps := (cdata (cdata_ops := pthread_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := pthreadsched_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);
          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;
          AC_re: AC hadt = AC ladt;
          ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
          ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
          LAT_re: LAT hadt = LAT ladt;
          nps_re: nps hadt = nps ladt;
          init_re: init hadt = init ladt;

          pperm_re: pperm hadt = pperm ladt;
          PT_re: PT hadt = PT ladt;
          ptp_re: ptpool hadt = ptpool ladt;
          idpde_re: idpde hadt = idpde ladt;
          ipt_re: ipt hadt = ipt ladt;
          smspool_re: smspool hadt = smspool 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;
          lock_re: lock hadt = lock ladt;

          com1_re: com1 hadt = com1 ladt;
          console_re: console hadt = console ladt;
          console_concrete_re: console_concrete hadt = console_concrete ladt;
          ioapic_re: ioapic ladt = ioapic hadt;
          lapic_re: lapic ladt = lapic hadt;
          intr_flag_re: intr_flag ladt = intr_flag hadt;
          curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
          in_intr_re: in_intr ladt = in_intr hadt;
          drv_serial_re: drv_serial hadt = drv_serial ladt;

          kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
          abtcb_re: abtcb hadt = abtcb ladt;
          abq_re: abq hadt = abq ladt;
          
          syncchpool_re: syncchpool hadt = syncchpool ladt;

          sleeper_re: sleeper hadt = sleeper 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 kctxt_inj_incr; eauto.
      Qed.

    End Rel_Property.

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

    Section OneStep_Forward_Relation.

      Section Exists.

        Lemma dequeue0_exist:
          ∀ s habd habd´ labd f i z,
            dequeue0_spec i habd = Some (habd´, z)
            → relate_AbData s f habd labd
            → ∃ labd´, dequeue0_spec i labd = Some (labd´, z) ∧
                       relate_AbData s f habd´ labd´.
        Proof.
          unfold dequeue0_spec; intros.
          exploit relate_impl_iflags_eq; eauto. inversion 1.
          exploit relate_impl_ipt_eq; eauto. intros.
          exploit relate_impl_abq_eq; eauto.
          exploit relate_impl_abtcb_eq; eauto; intros.
          revert H; subrewrite.
          subdestruct; inv HQ; refine_split´; trivial.
          generalize relate_impl_abq_update; intro tmp; simpl in tmp; eapply tmp; eauto; clear tmp.
          generalize relate_impl_abtcb_update; intro tmp; simpl in tmp; eapply tmp; eauto; clear tmp.
        Qed.


        Lemma dequeue_atomic_exist:
          ∀ s habd habd´ labd f i z,
            dequeue_atomic_spec i habd = Some (habd´, z)
            → relate_AbData s f habd labd
            → ∃ labd´, dequeue_atomic_spec i labd = Some (labd´, z) ∧
                       relate_AbData s f habd´ labd´.
        Proof.
          unfold dequeue_atomic_spec; intros.
          revert H; subrewrite. subdestruct.
          specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
          intros [d0 [Hacq Hrel]]. rewrite Hacq.
          specialize (dequeue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
          intros [d1 [Hdeq Hrel1]]. rewrite Hdeq.
          specialize (release_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct2 Hrel1).
          intros [d2 [Hrls Hrel2]]. rewrite Hrls.
          ∃ d2. subst. inv HQ. eauto.
        Qed.

        Require Import FutureTactic.

        Lemma thread_poll_pending_exist:
          ∀ s habd habd´ labd f,
            thread_poll_pending_spec habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, thread_poll_pending_spec labd = Some labd´
                       ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold thread_poll_pending_spec; intros.
          revert H; subrewrite. inversion H0.
          subdestruct; inv HQ.
          {
            specialize (dequeue_atomic_exist _ _ _ _ _ _ _ Hdestruct H0).
            intros [d0 [Hdeq Hrel]]. rewrite CPU_ID_re0 in Hdeq. rewrite Hdeq.
            if_true.
            inversion Hrel.
            rewrite <- abq_re1. rewrite <- CPU_ID_re0. rewrite Hdestruct4.
            remember (((d0 {abtcb : ZMap.set z (AbTCBValid READY (CPU_ID habd)
                                                           (rdy_q_id (CPU_ID habd))) (abtcb d0)})
                         {abq: ZMap.set (rdy_q_id (CPU_ID habd)) (AbQValid (l ++ z :: nil)) (abq r)})
                        {sleeper: ZMap.set (CPU_ID habd) (ZMap.get (CPU_ID habd) (sleeper d0) - 1) (sleeper d0)}) as dx.
            rewrite <- sleeper_re1.
            rewrite zle_lt_true; trivial.
            rewrite <- AC_re1.
            subrewrite´.
            ∃ dx.
            split.
            subst.
            rewrite <- abq_re1.
            rewrite CPU_ID_re0.
            reflexivity.
            rewrite Heqdx.
            rewrite <- abtcb_re1.
            rewrite <- sleeper_re1.
            rewrite CPU_ID_re0.
            rewrite <- abq_re1.
            econstructor; eauto; simpl.
          }
          {
            specialize (dequeue_atomic_exist _ _ _ _ _ _ _ Hdestruct H0).
            intros [d0 [Hdeq Hrel]]. rewrite CPU_ID_re0 in Hdeq. rewrite Hdeq.
            if_false.
            ∃ d0.
            split. reflexivity.
            assumption.
          }
        Qed.

        Lemma dequeue0_pg:
          ∀ i d d´ z,
            dequeue0_spec i d = Some (d´, z) →
            pg d = pg d´.
        Proof.
            unfold dequeue0_spec in *; intros.
            subdestruct; inv H; simpl; auto.
        Qed.

        Lemma thread_poll_pending_pg:
          ∀ d d´,
            thread_poll_pending_spec d = Some d´ →
            pg d = pg d´.
        Proof.
          unfold thread_poll_pending_spec, dequeue_atomic_spec, acquire_lock_ABTCB_spec.
          intros. subdestruct.
          - inv H; simpl. unfold release_lock_ABTCB_spec in ×.
            subdestruct. inv Hdestruct10; simpl.
            eapply dequeue0_pg in Hdestruct8.
            simpl in Hdestruct8. congruence.
          - inv H; simpl. unfold release_lock_ABTCB_spec in ×.
            subdestruct. inv Hdestruct10; simpl.
            eapply dequeue0_pg in Hdestruct8.
            simpl in Hdestruct8. congruence.
          - inv H; simpl. unfold release_lock_ABTCB_spec in ×.
            subdestruct. inv Hdestruct9; simpl.
            eapply dequeue0_pg in Hdestruct7.
            simpl in Hdestruct7. congruence.
          - inv H; simpl. unfold release_lock_ABTCB_spec in ×.
            subdestruct. inv Hdestruct9; simpl.
            eapply dequeue0_pg in Hdestruct7.
            simpl in Hdestruct7. congruence.
        Qed.

        Lemma thread_kill_exist:
          ∀ habd habd´ labd rs r´ rs0 s f,
            ObjThread.thread_kill_spec
              habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
              #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) = Some (habd´, rs0)
            → relate_AbData s f habd labd
            → high_level_invariant habd
            → (∀ reg : PregEq.t,
                  val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
            → ∃ labd´ r´0, thread_kill_spec
                                   labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
                                   #EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) = Some (labd´, r´0)
                                 ∧ relate_AbData s f habd´ labd´
                                 ∧ (∀ i r,
                                       ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r)).
        Proof.
          Opaque remove.
          unfold ObjThread.thread_kill_spec, thread_kill_spec; intros until f.
          intros HP HR HINV HVL; pose proof HR as HR´; inv HR; revert HP.
          specialize (CPU_ID_range _ HINV).
          specialize (valid_TDQ _ HINV).
          specialize (valid_TCB _ HINV). unfold AbQCorrect_range, AbQCorrect.
          simpl; subrewrite´; intros HT HQ HC Hhigh.
          assert (HOS: 0≤ rdy_q_id (CPU_ID labd) < num_chan).
          {
            unfold rdy_q_id. omega.
          }
          subdestruct; contra_inv.
          inv Hhigh.
          refine_split´; eauto 1.
          - econstructor; simpl; try eassumption; try congruence.
            kctxt_inj_simpl.
          - intros; eapply kctxt_re; eauto.
        Qed.

        Lemma thread_yield_exist:
          ∀ habd habd´ labd rs r´ rs0 s f,
            ObjThread.thread_yield_spec
              habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
              #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) = Some (habd´, rs0)
            → relate_AbData s f habd labd
            → high_level_invariant habd
            → (∀ reg : PregEq.t,
                  val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
            → ∃ labd´ r´0, thread_yield_spec
                                   labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
                                   #EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) = Some (labd´, r´0)
                                 ∧ relate_AbData s f habd´ labd´
                                 ∧ (∀ i r,
                                       ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r)).
        Proof.
          Opaque remove.
          unfold ObjThread.thread_yield_spec, thread_yield_spec; intros until f.
          intros HP HR HINV HVL; pose proof HR as HR´; inv HR; revert HP.
          specialize (CPU_ID_range _ HINV).
          specialize (valid_TDQ _ HINV).
          specialize (valid_TCB _ HINV). unfold AbQCorrect_range, AbQCorrect.
          simpl; subrewrite´; intros HT HQ HC Hhigh.
          destruct (pg labd); contra_inv.
          assert (HOS: 0≤ rdy_q_id (CPU_ID labd) < num_chan).
          {
            unfold rdy_q_id. omega.
          }
          specialize (HQ refl_equal _ HOS).
          specialize (HT refl_equal).
          subdestruct; contra_inv.
          inv HQ.
          exploit thread_poll_pending_high_level_inv; eauto. intros HINV´.
          specialize (valid_TDQ _ HINV´).
          erewrite thread_poll_pending_pg in pg_re0; eauto.
          rewrite pg_re0.
          unfold AbQCorrect_range, AbQCorrect.
          intros HP.
          specialize (HP refl_equal _ HOS).
          rewrite Hdestruct4 in HP.
          destruct HP as (l & Heq & Hin). inv Heq.
          specialize (thread_poll_pending_exist s _ _ _ _ Hdestruct2 HR´).
          intros [d0 [Hacq Hrel]]. rewrite Hacq.
          inversion Hrel.
          rewrite <- abq_re1, <- abtcb_re1, <- AC_re1.
          subrewrite´.
          inv Hhigh.
          refine_split´; eauto 1.
          - econstructor; simpl; try eassumption; try congruence.
            kctxt_inj_simpl.
          - intros; eapply kctxt_re1; eauto.
        Qed.

        Lemma relate_R_Ab_Data:
          ∀ s f h l,
            relate_AbData s f h l →
            relate_RData f h l.
        Proof.
          intros. simpl in H. assumption.
        Qed.

        Lemma thread_sleep_exist:
          ∀ habd habd´ labd rs r´ rs0 n s f,
            ObjThread.thread_sleep_spec
              habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
              #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) n = Some (habd´, rs0)
            → relate_AbData s f habd labd
            → high_level_invariant habd
            → (∀ reg : PregEq.t,
                  val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
            → ∃ labd´ r´0, thread_sleep_spec
                                   labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
                                   #EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) n = Some (labd´, r´0)
                                 ∧ relate_AbData s f habd´ labd´
                                 ∧ (∀ i r,
                                       ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r)).
        Proof.
          Opaque remove.
          unfold ObjThread.thread_sleep_spec, thread_sleep_spec; intros until f.
          intros HP HR HINV HVL; pose proof HR as HR´; inv HR; revert HP.
          specialize (CPU_ID_range _ HINV).
          specialize (valid_TDQ _ HINV).
          specialize (valid_TCB _ HINV). unfold AbQCorrect_range, AbQCorrect.
          subrewrite´; intros HT HQ HC Hhigh.
          assert (Hpg: pg labd = true).
          {
            destruct (pg labd); contra_inv.
            reflexivity.
          }
          assert (HOS: 0≤ rdy_q_id (CPU_ID labd) < num_chan).
          {
            unfold rdy_q_id. omega.
          }
          specialize (HQ Hpg _ HOS).
          specialize (HT Hpg).
          subdestruct; contra_inv.
          assert (Hpgr0: pg r0 = true).
          {
            functional inversion Hdestruct6. simpl.
            functional inversion Hdestruct5.
            functional inversion H7. simpl.
            functional inversion H9. simpl.
            unfold acquire_lock_ABTCB_spec in H8.
            subdestruct. inversion H8. simpl. auto.
            inversion H8. simpl. auto.
          }
          inv HQ.
          generalize (enqueue_atomic_exist s _ _ _ _ _ _ Hdestruct5 HR´). intros [ld0 [Hspec0 Hrel0]].
          rewrite Hspec0.
          exploit (release_lock_SC_exist); eauto. intros [ld1 [Hspec1 Hrel1]].
          rewrite Hspec1.
          inv Hrel1.
          rewrite <- abq_re1, <- abtcb_re1, <- sleeper_re1.
          subrewrite´.
          refine_split´. reflexivity.
          {
            inv Hhigh. subrewrite´. econstructor; simpl; eauto.
            kctxt_inj_simpl.
          }
          {
            inv Hhigh.
            intros.
            eapply kctxt_re1; eauto.
          }
        Qed.

      End Exists.

      Section FRESH_PRIM.

        Lemma thread_kill_spec_ref:
          compatsim (crel HDATA LDATA)
                    (primcall_thread_schedule_compatsem ObjThread.thread_kill_spec (prim_ident:= thread_kill))
                    thread_kill_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          inv match_extcall_states.
          exploit thread_kill_exist; eauto 1.
          intros [labd´ [r´0[HP [HM HReg]]]].
          refine_split; try econstructor; eauto.
          eapply reg_symbol_inject; eassumption.
          econstructor; eauto. constructor.
          subst rs3.
          val_inject_simpl; eapply HReg;
          apply PregToZ_correct; reflexivity.
        Qed.

        Lemma thread_yield_spec_ref:
          compatsim (crel HDATA LDATA)
                    (primcall_thread_schedule_compatsem ObjThread.thread_yield_spec (prim_ident:= thread_yield))
                    thread_yield_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          inv match_extcall_states.
          exploit thread_yield_exist; eauto 1.
          intros [labd´ [r´0[HP [HM HReg]]]].
          refine_split; try econstructor; eauto.
          eapply reg_symbol_inject; eassumption.
          econstructor; eauto. constructor.
          subst rs3.
          val_inject_simpl; eapply HReg;
          apply PregToZ_correct; reflexivity.
        Qed.

        Lemma thread_sleep_spec_ref:
          compatsim (crel HDATA LDATA)
                    (primcall_thread_transfer_compatsem ObjThread.thread_sleep_spec)
                    thread_sleep_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          inv match_extcall_states.
          exploit thread_sleep_exist; eauto 1.
          intros [labd´ [r´0[HP [HM HReg]]]].
          refine_split; try econstructor; eauto.
          - eapply reg_symbol_inject; eassumption.
          - exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
            instantiate (3:= d1´).
            apply extcall_args_with_data; eauto.
            instantiate (1:= d2).
            intros [?[? Hinv]]. inv_val_inject.
            apply extcall_args_without_data in H; eauto.
          - econstructor; eauto. constructor.
          - subst rs3.
            val_inject_simpl;
              eapply HReg; apply PregToZ_correct; reflexivity.
        Qed.

      End FRESH_PRIM.

      Section PASSTHROUGH_PRIM.

        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) pthread_passthrough pthreadsched.
        Proof.
          sim_oplus.
          - apply fload_sim.
          - apply fstore_sim.
          - apply vmxinfo_get_sim.
          - apply palloc_sim.
          - apply setPT_sim.
          - apply ptRead_sim.
          - apply ptResv_sim.
          - apply shared_mem_status_sim.
          - apply offer_shared_mem_sim.
          - apply thread_spawn_sim.
          - apply thread_wakeup_sim.
          - apply sched_init_sim.
          - apply ptin_sim.
          - apply ptout_sim.
          - apply container_get_nchildren_sim.
          - apply container_get_quota_sim.
          - apply container_get_usage_sim.
          - apply container_can_consume_sim.

          - apply get_CPU_ID_sim.
          - apply get_curid_sim.
          - apply acquire_lock_SC_sim.
          - apply release_lock_SC_sim.
          - apply get_sync_chan_busy_sim.
          - apply set_sync_chan_busy_sim.

          - apply ipc_send_body_sim.
          - apply ipc_receive_body_sim.
          - apply cli_sim.
          - apply sti_sim.
          - apply serial_intr_disable_sim.
          - apply serial_intr_enable_sim.
          - apply serial_putc_sim.
          - apply cons_buf_read_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.
          - layer_sim_simpl.
            + eapply load_correct2.
            + eapply store_correct2.
        Qed.

      End PASSTHROUGH_PRIM.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.