Library mcertikos.proc.VMXInitGenAsm

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

Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.

Require Import VVMXIntro.
Require Import VMXInitGenSpec.
Require Import VMXInitGenAsmSource.
Require Import VMXInitGenAsmData.

Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.

Section ASM_VERIFICATION.

  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 LDATA := RData.
  Notation LDATAOps := (cdata LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
    Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

  Lemma vmx_return_from_guest_proof:
    ∀ ge (s: stencil) (rs: regset) b m0 labd labd´,
      find_symbol s vmx_return_from_guest = Some b →
      make_globalenv s (vmx_return_from_guest ↦ vmx_return_from_guest_function) vmxintro = ret ge →
      rs PC = Vptr b Int.zero →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      vmx_return_from_guest_spec labd = Some labd´ →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      low_level_invariant (Mem.nextblock m0) labd →
      high_level_invariant labd →
      let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      ∃ r_: regset,
        lasm_step (vmx_return_from_guest ↦ vmx_return_from_guest_function)
                  (vmxintro (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_return_from_guest s rs (m0, labd) r_ (m0, labd´)
        ∧ (∀ l,
              Val.lessdef (Pregmap.get l (rs0#PC <- (Vptr b (Int.repr 3))))
                          (Pregmap.get l r_)).
  Proof.
    intros.

    exploit Hvmx_exit_post; eauto.
    intros [[Hvmx_exit_post [HHvmx_exit_post HHvmx_exit_post_fun]] prim_Hvmx_exit_post].
    exploit Hhost_in; eauto.
    intros [[b_host_in [Hhost_in Hhost_in_fun]] prim_host_in].

    exploit vmx_return_from_guest_generate; eauto.
    intros (labd0 & Hhostin & Hpost).
    exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
    intros Hstencil_matches.
    exploit Hvmx_return_from_guest; eauto 2. intros Hfunct.

    rewrite (Lregset_rewrite rs).
    refine_split´; try eassumption.
    - rewrite H1.
      econstructor; eauto.

      one_step_forward´.
      unfold symbol_offset. unfold fundef.
      rewrite Hhost_in.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_prim_call _ b_host_in); eauto 1.
      econstructor; eauto 1.
      instantiate (4:= host_in).
      change positive with ident in ×.
      rewrite prim_host_in.
      refine_split´; try reflexivity.
      econstructor; eauto. simpl.
      econstructor; eauto.

      Lregset_simpl_tac.

      one_step_forward´.
      unfold symbol_offset. unfold fundef.
      rewrite HHvmx_exit_post.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_external _ Hvmx_exit_post); eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      change positive with ident in ×.
      rewrite prim_Hvmx_exit_post.
      refine_split´; try reflexivity.
      econstructor; eauto.
      refine_split´; try reflexivity; try eassumption.
      simpl. econstructor.
      constructor_gen_sem_intro.
      Lregset_simpl_tac.
      erewrite <- stencil_matches_genv_next in H3; eauto.
      discriminate.
      Lregset_simpl_tac.

      one_step_forward´.
      Lregset_simpl_tac.

      econstructor.
      reflexivity.
    - Lregset_simpl_tac.
      simpl; Lregset_simpl_tac.
      unfold Lregset_fold; simpl.
      intros reg.
      repeat (rewrite Pregmap.gsspec).
      subst rs0.
      simpl_destruct_reg.
      exploit reg_false; try eassumption.
      intros HF. inv HF.
  Qed.

  Lemma vmx_return_from_guest_code_correct:
    asm_spec_le (vmx_return_from_guest ↦ vmx_return_from_guest_spec_low)
                (〚 vmx_return_from_guest ↦ vmx_return_from_guest_function 〛 vmxintro).
  Proof.
    eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
    intros. inv H.
    eapply make_program_make_globalenv in H0.
    exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
    intros Hstencil_matches.
    assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
                 Some (Internal vmx_return_from_guest_function)).
    {
      assert (Hmodule:
                get_module_function vmx_return_from_guest (vmx_return_from_guest ↦ vmx_return_from_guest_function)
                = OK (Some vmx_return_from_guest_function)) by reflexivity.
      assert (HInternal:
                make_internal vmx_return_from_guest_function
                = OK (AST.Internal vmx_return_from_guest_function)) by reflexivity.
      eapply make_globalenv_get_module_function in H0; eauto.
      destruct H0 as [?[Hsymbol ?]].
      inv Hstencil_matches.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H1 in Hsymbol. inv Hsymbol.
      assumption.
    }

    exploit vmx_return_from_guest_proof; eauto 2.
    intros (r_ & Hstep & Hless).

    refine_split´; try eassumption; try reflexivity.
    inv H6. inv inv_inject_neutral.
    eapply Mem.neutral_inject in inv_mem_inject_neutral.
    lift_unfold. split; eauto.
    eapply inv_mem_inject_neutral.
  Qed.

    Lemma vm_run_proof:
      ∀ ge (s: stencil) (rs rs´: regset) b m0 labd labd´,
        find_symbol s vmx_run_vm = Some b →
        make_globalenv s (vmx_run_vm ↦ vm_run_function) vmxintro = ret ge →
        rs PC = Vptr b Int.zero →
        let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
        vm_run_spec rs01 labd = Some (labd´, rs´) →
        asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
        low_level_invariant (Mem.nextblock m0) labd →
        high_level_invariant labd →
        rs ESP ≠ Vundef →
        (∀ b1 o,
           rs ESP = Vptr b1 o →
           Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m0)) →
        let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
                              (undef_regs (List.map preg_of destroyed_at_call) rs)) in
        ∃ r_: regset,
          lasm_step (vmx_run_vm ↦ vm_run_function)
                    (vmxintro (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_run_vm s rs (m0, labd) r_ (m0, labd´)
          ∧ (∀ l,
                Val.lessdef (Pregmap.get l (rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
                                               #ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
                                               #PC <- (rs´#RA)))
                            (Pregmap.get l r_)).
  Proof.
    intros.
    exploit Hvmptrld; eauto.
    intros [[Hvmptrld [HHvmptrld HHvmptrld_fun]] prim_Hvmptrld].
    exploit Hvmx_enter_pre; eauto.
    intros [[Hvmx_enter_pre [HHvmx_enter_pre HHvmx_enter_pre_fun]] prim_Hvmx_enter_pre].
    exploit Hvmx_enter; eauto.
    intros [[Hvmx_enter [HHvmx_enter HHvmx_enter_fun]] prim_Hvmx_enter].

    exploit vm_run_generate; eauto.
    intros (labd0 & Hld & Hpre & Henter & Hr1 & Hr2).
    exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
    intros Hstencil_matches.
    exploit Hvm_run; eauto 2. intros Hfunct.

    rewrite (Lregset_rewrite rs).
    refine_split´; try eassumption.
    - rewrite H1.
      econstructor; eauto.

      one_step_forward´.
      Lregset_simpl_tac.

      unfold symbol_offset. unfold fundef.
      rewrite HHvmptrld.
      econstructor; eauto.
      eapply (LAsm.exec_step_external _ Hvmptrld); eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      change positive with ident in ×.
      rewrite prim_Hvmptrld.
      refine_split´; try reflexivity.
      econstructor; eauto.
      refine_split´; try reflexivity; try eassumption.
      simpl. econstructor.
      constructor_gen_sem_intro.
      discriminate.
      Lregset_simpl_tac.

      one_step_forward´.
      unfold symbol_offset. unfold fundef.
      rewrite HHvmx_enter_pre.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_external _ Hvmx_enter_pre); eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      econstructor; eauto 1.
      change positive with ident in ×.
      rewrite prim_Hvmx_enter_pre.
      refine_split´; try reflexivity.
      econstructor; eauto.
      refine_split´; try reflexivity; try eassumption.
      simpl. econstructor.
      constructor_gen_sem_intro.
      discriminate.
      Lregset_simpl_tac.

      one_step_forward´.
      unfold symbol_offset. unfold fundef.
      rewrite HHvmx_enter.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_prim_call _ Hvmx_enter); eauto 1.
      econstructor; eauto 1.
      instantiate (4:= vmx_enter).
      change positive with ident in ×.
      rewrite prim_Hvmx_enter.
      refine_split´; try reflexivity.
      econstructor; eauto. simpl.
      econstructor; eauto.
      inv Hstencil_matches.
      erewrite <- stencil_matches_symbols; eauto.
      reflexivity.

      inv Hstencil_matches.
      rewrite <- stencil_matches_genv_next.
      eassumption.

      econstructor.
      reflexivity.
    - Lregset_simpl_tac.
      simpl; Lregset_simpl_tac.
      unfold Lregset_fold; simpl.
      intros reg.
      repeat (rewrite Pregmap.gsspec).
      simpl_destruct_reg.
      exploit reg_false; try eassumption.
      intros HF. inv HF.
  Qed.

  Lemma vmx_run_vm_code_correct:
    asm_spec_le (vmx_run_vm ↦ vmx_run_vm_spec_low)
                (〚 vmx_run_vm ↦ vm_run_function 〛 vmxintro).
  Proof.
    eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
    intros. inv H.
    eapply make_program_make_globalenv in H0.
    exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
    intros Hstencil_matches.
    rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches) in H8.
    assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
                 Some (Internal vm_run_function)).
    {
      assert (Hmodule:
                get_module_function vmx_run_vm (vmx_run_vm ↦ vm_run_function)
                = OK (Some vm_run_function)) by reflexivity.
      assert (HInternal:
                make_internal vm_run_function
                = OK (AST.Internal vm_run_function)) by reflexivity.
      eapply make_globalenv_get_module_function in H0; eauto.
      destruct H0 as [?[Hsymbol ?]].
      inv Hstencil_matches.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H1 in Hsymbol. inv Hsymbol.
      assumption.
    }

    exploit vm_run_proof; eauto 2.
    intros (r_ & Hstep & Hless).

    refine_split´; try eassumption; try reflexivity.
    inv H4. inv inv_inject_neutral.
    eapply Mem.neutral_inject in inv_mem_inject_neutral.
    lift_unfold. split; eauto.
    eapply inv_mem_inject_neutral.
  Qed.

  End WITHMEM.

End ASM_VERIFICATION.