Library mcertikos.virt.intel.VMXInitGenAsmData

***********************************************************************
*                                                                     *
*            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 VMXInitGenAsmSource.
Require Import AbstractDataType.

Section ASM_DATA.

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

    Section ExitGUEST.

      Lemma vmx_return_from_guest_generate:
        ∀ labd labd´ rs rs´ n,
          vmx_return_from_guest_spec rs labd = Some (labd´, rs´) →
          low_level_invariant n labd →
          high_level_invariant labd →
          ∃ labd0,
            hostin_spec labd = Some labd0
            ∧ ∃ labd1 rs´´,
                 vmx_exit_spec rs labd0 = Some (labd1, rs´´)
                 ∧ (∀ r, Val.has_type (rs´´ r) Tint)
                 ∧ (∀ r,
                       val_inject (Mem.flat_inj n) (rs´´ r) (rs´´ r))
                 ∧ ∃ labd2, vmx_exit_post_spec labd1 = Some labd2
                                  ∧ proc_start_user_spec labd2 = Some (labd´, rs´)
                                  ∧ (∀ i,
                                        0 ≤ i < UCTXT_SIZE →
                                        let v:= (ZMap.get i rs´) in
                                        Val.has_type v Tint)
                                  ∧ (∀ i,
                                        0 ≤ i < UCTXT_SIZE →
                                        let v:= (ZMap.get i rs´) in
                                        val_inject (Mem.flat_inj n) v v).
      Proof.
        unfold vmx_return_from_guest_spec.
        intros. unfold hostin_spec.
        subdestruct. inv H.
        esplit; split.
        reflexivity.
        unfold vmx_exit_spec; simpl.
        subrewrite´. esplit; esplit; split.
        reflexivity.
        inv H0. inv VMX_INJECT.
        split.
        intros.
        destruct r as [| [] | [] | | [] |]; try constructor; eapply H.
        split.
        intros.
        destruct r as [| [] | [] | | [] |]; try constructor; eapply H.
        unfold vmx_exit_post_spec; simpl.
        subrewrite´.
        esplit; split; trivial.
        unfold proc_start_user_spec; simpl.
        subrewrite´.
        split; trivial.
        split; intros;
        eapply uctxt_INJECT; eauto;
        apply valid_curid; eauto.
      Qed.

    End ExitGUEST.

    Section StartGuest.

      Lemma vm_run_generate:
        ∀ labd labd´ rs rs´ n,
          vm_run_spec rs labd = Some (labd´, rs´) →
          low_level_invariant n labd →
          ∃ labd0,
            vmptrld_spec labd = Some labd
            ∧ vmx_enter_pre_spec labd = Some labd0
            ∧ vmx_enter_spec rs labd0 = Some (labd´, rs´)
            ∧ (∀ r, Val.has_type (rs´ r) Tint)
            ∧ (∀ r,
                  val_inject (Mem.flat_inj n) (rs´ r) (rs´ r)).
      Proof.
        unfold vm_run_spec. intros.
        subdestruct.
        unfold vmptrld_spec, vmx_enter_pre_spec. inv H.
        subrewrite´.
        esplit.
        split; trivial.
        split; trivial.
        unfold vmx_enter_spec; simpl.
        subrewrite´.
        split; trivial.
        inv H0.
        inv VMX_INJECT.
        split; intros r;
        destruct r as [| [] | [] | | [] |]; try constructor;
        eapply H.
      Qed.

    End StartGuest.

    Lemma Hvmx_enter:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_vmx_enter, Genv.find_symbol ge vmx_enter = Some b_vmx_enter
                             ∧ Genv.find_funct_ptr ge b_vmx_enter =
                                Some (External (EF_external vmx_enter null_signature)))
        ∧ get_layer_primitive vmx_enter vmxintro = OK (Some (primcall_vmx_enter_compatsem vmx_enter_spec vmx_enter)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive vmx_enter vmxintro
                     = OK (Some (primcall_vmx_enter_compatsem vmx_enter_spec vmx_enter)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hvmx_enter_pre:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_vmx_enter_pre, Genv.find_symbol ge vmx_enter_pre = Some b_vmx_enter_pre
                             ∧ Genv.find_funct_ptr ge b_vmx_enter_pre =
                                Some (External (EF_external vmx_enter_pre null_signature)))
        ∧ get_layer_primitive vmx_enter_pre vmxintro = OK (Some (gensem vmx_enter_pre_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive vmx_enter_pre vmxintro = OK (Some (gensem vmx_enter_pre_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hvmptrld:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_vmptrld, Genv.find_symbol ge vmptrld = Some b_vmptrld
                             ∧ Genv.find_funct_ptr ge b_vmptrld =
                                Some (External (EF_external vmptrld null_signature)))
        ∧ get_layer_primitive vmptrld vmxintro = OK (Some (gensem vmptrld_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive vmptrld vmxintro = OK (Some (gensem vmptrld_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hvmx_exit_post:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_vmx_exit_post, Genv.find_symbol ge vmx_exit_post = Some b_vmx_exit_post
                             ∧ Genv.find_funct_ptr ge b_vmx_exit_post =
                                Some (External (EF_external vmx_exit_post null_signature)))
        ∧ get_layer_primitive vmx_exit_post vmxintro = OK (Some (gensem vmx_exit_post_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive vmx_exit_post vmxintro = OK (Some (gensem vmx_exit_post_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hvmx_exit:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_vmx_exit, Genv.find_symbol ge vmx_exit = Some b_vmx_exit
                             ∧ Genv.find_funct_ptr ge b_vmx_exit =
                                Some (External (EF_external vmx_exit null_signature)))
        ∧ get_layer_primitive vmx_exit vmxintro = OK (Some (primcall_vmx_exit_compatsem vmx_exit_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive vmx_exit vmxintro
                     = OK (Some (primcall_vmx_exit_compatsem vmx_exit_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hhost_in:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_host_in, Genv.find_symbol ge host_in = Some b_host_in
                             ∧ Genv.find_funct_ptr ge b_host_in =
                                Some (External (EF_external host_in null_signature)))
        ∧ get_layer_primitive host_in vmxintro = OK (Some (primcall_general_compatsem hostin_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive host_in vmxintro = OK (Some (primcall_general_compatsem hostin_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hproc_start_user:
      ∀ MCode_Asm s ge,
        make_globalenv s MCode_Asm vmxintro = ret ge →
        (∃ b_proc_start_user, Genv.find_symbol ge proc_start_user = Some b_proc_start_user
                                   ∧ Genv.find_funct_ptr ge b_proc_start_user =
                                      Some (External (EF_external proc_start_user null_signature)))
        ∧ get_layer_primitive proc_start_user vmxintro = OK (Some (primcall_start_user_compatsem proc_start_user_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive proc_start_user vmxintro = OK (Some (primcall_start_user_compatsem proc_start_user_spec)))
        by reflexivity.
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hvm_run:
      ∀ ge s b,
        make_globalenv s (vmx_run_vm ↦ vm_run_function) vmxintro = ret ge →
        find_symbol s vmx_run_vm = Some b →
        stencil_matches s ge →
        Genv.find_funct_ptr ge b = Some (Internal vm_run_function).
    Proof.
      intros.
      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 H; eauto.
      destruct H as [?[Hsymbol ?]].
      inv H1.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H0 in Hsymbol. inv Hsymbol.
      assumption.
    Qed.

    Lemma Hvmx_return_from_guest:
      ∀ ge s b,
        make_globalenv s (vmx_return_from_guest ↦ vmx_return_from_guest_function) vmxintro = ret ge →
        find_symbol s vmx_return_from_guest = Some b →
        stencil_matches s ge →
        Genv.find_funct_ptr ge b = Some (Internal vmx_return_from_guest_function).
    Proof.
      intros.
      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 H; eauto.
      destruct H as [?[Hsymbol ?]].
      inv H1.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H0 in Hsymbol. inv Hsymbol.
      assumption.
    Qed.

  End WITHMEM.

End ASM_DATA.