Library mcertikos.virt.intel.VMXInitGenAsm

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 

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

  Notation LDATA := RData.
  Notation LDATAOps := (cdata LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModel}.
    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 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.

  Lemma vmx_return_from_guest_proof:
    ∀ ge (s: stencil) (rs: regset) rs´ 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 →
      let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
                                        #EDX <- (rs EDX) #EDI <- (rs EDI)
                                        #ESI <- (rs ESI) #EBP <- (rs EBP) in
      vmx_return_from_guest_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 :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs))
                            # EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
                            # EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
                            # EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
                            # ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
                            # PC <- (ZMap.get U_EIP 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)
                          (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 Hvmx_exit; eauto.
    intros [[Hvmx_exit [HHvmx_exit HHvmx_exit_fun]] prim_Hvmx_exit].
    exploit Hhost_in; eauto.
    intros [[b_host_in [Hhost_in Hhost_in_fun]] prim_host_in].
    exploit Hproc_start_user; eauto.
    intros [[b_proc_start_user [Hproc_start_user Hproc_start_user_fun]] prim_proc_start_user].

    exploit vmx_return_from_guest_generate; eauto.
    intros (labd0 & Hhostin & labd1 & rs_exit & Hexit & HR1´ & HR2´ & labd2 & Hpost & Hstart & HR1 & HR2).
    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.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_prim_call _ Hvmx_exit); eauto 1.
      econstructor; eauto 1.
      instantiate (4:= vmx_exit).
      change positive with ident in ×.
      rewrite prim_Hvmx_exit.
      refine_split´; try reflexivity.
      econstructor; eauto. simpl.
      econstructor; eauto.
      inv Hstencil_matches.
      erewrite <- stencil_matches_symbols; eauto.
      reflexivity.
      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.
      discriminate.
      Lregset_simpl_tac.

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

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

      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_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.
    rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches) in H8.
    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 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.