Library mcertikos.virt.intel.VVMCSIntroCodeSetDefaults

***********************************************************************
*                                                                     *
*            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 TacticsForTesting.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VMCSInitGenSpec.
Require Import ObjVMCS.
Require Import VVMCSIntroCSource.
Require Import IntelPrimSemantics.
Require Import ObjCPU.
Require Import ObjEPT.

Hint Resolve Int.unsigned_range_2.
Hint Resolve CLemmas.Z_lor_range_lo.
Hint Resolve Z_lor_range.

Function unsigned64 (x : int64) : Z64 :=
  VZ64 (Int64.unsigned x).

Function unpack64 (x: Z64): Z :=
  match x with
  | VZ64 z ⇒ z
  end.

Function repr64 (x : Z64) : int64 :=
  Int64.repr (unpack64 x).

Lemma unsigned64_repr: ∀ x: Z64,
    0 ≤ unpack64(x) ≤ Int64.max_unsigned →
    unsigned64 (repr64 x) = x.
Proof.
  unfold repr64, unpack64, unsigned64.
  intros. destruct x. rewrite Int64.unsigned_repr; auto.
Qed.

Print Int64.repr_unsigned.

Lemma repr64_unsigned: ∀ x: int64,
    repr64 (unsigned64 x) = x.
Proof.
  unfold repr64, unpack64, unsigned64.
  apply Int64.repr_unsigned.
Qed.

Lemma Z64_eq: ∀ x y: Z,
    0 ≤ x ≤ Int64.max_unsigned →
    0 ≤ y ≤ Int64.max_unsigned →
    x = y →
    VZ64 x = VZ64 y.
Proof.
  intros x y Hx Hy Heq; rewrite Heq; reflexivity.
Qed.

Lemma Z64_elim: ∀ x y: Z,
    VZ64 x = VZ64 y →
    x = y.
Proof.
  intros x y Heq.
  inversion Heq.
  reflexivity.
Qed.

Lemma unsigned_repr_eq:
  ∀ (x: int) (y: Z),
    y = Int.unsigned x →
    Int.repr y = x.
Proof.
  intros x y. intros Heq.
  rewrite Heq; rewrite Int.repr_unsigned; reflexivity.
Qed.

Lemma repr_unsigned_eq:
  ∀ (x: int) (y: Z),
    Int.repr y = x →
    0 ≤ y ≤ Int.max_unsigned →
    y = Int.unsigned x.
Proof.
  intros x y Heq Hrg.
  rewrite <- Heq; rewrite Int.unsigned_repr;
  (reflexivity || assumption).
Qed.

Module VMCSINTROCODE.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Local Open Scope Z_scope.

    Section VMCSSETDEFAULTS.

      Let L: compatlayer (cdata RData) :=
        vmcs_set_revid ↦ gensem vmcs_set_revid_spec
                       ⊕ ept_init ↦ gensem ept_init_spec
                       ⊕ vmcs_writez ↦ gensem vmcs_writez_spec
                       ⊕ vmcs_writez64 ↦ gensem vmcs_writez64_spec
                       ⊕ vmcs_write_ident ↦ vmcs_writeb_compatsem vmcs_write_ident_spec
                       ⊕ rcr0 ↦ gensem rcr0_spec
                       ⊕ rcr3 ↦ gensem rcr3_spec
                       ⊕ rcr4 ↦ gensem rcr4_spec
                       ⊕ rdmsr ↦ gensem rdmsr_spec
                       ⊕ vmptrld ↦ gensem vmptrld_spec
                       ⊕ vmx_enable ↦ gensem vmx_enable_spec
                       ⊕ vmxinfo_get ↦ gensem vmxinfo_get_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Local Open Scope Z_scope.

      Section VMCSSetDefaultsBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable bvmcs_set_revid: block.
        Hypothesis hvmcs_set_revid1 : Genv.find_symbol ge vmcs_set_revid = Some bvmcs_set_revid.
        Hypothesis hvmcs_set_revid2 : Genv.find_funct_ptr ge bvmcs_set_revid =
                                      let arg_type := (Tcons tint Tnil) in
                                      let ret_type := tvoid in
                                      let cal_conv := cc_default in
                                      let prim := vmcs_set_revid in
                                      Some (External (EF_external prim
                                                                  (signature_of_type arg_type ret_type cal_conv))
                                                     arg_type ret_type cal_conv).

        Variable bept_init: block.
        Hypothesis hept_init1 : Genv.find_symbol ge ept_init = Some bept_init.
        Hypothesis hept_init2 : Genv.find_funct_ptr ge bept_init =
                                let arg_type := (Tcons tint Tnil) in
                                let ret_type := tvoid in
                                let cal_conv := cc_default in
                                let prim := ept_init in
                                Some (External (EF_external prim
                                                            (signature_of_type arg_type ret_type cal_conv))
                                               arg_type ret_type cal_conv).

        Variable bvmcs_writez: block.
        Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
        Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
                                   let arg_type := (Tcons tint (Tcons tint Tnil)) in
                                   let ret_type := tvoid in
                                   let cal_conv := cc_default in
                                   let prim := vmcs_writez in
                                   Some (External (EF_external prim
                                                               (signature_of_type arg_type ret_type cal_conv))
                                                  arg_type ret_type cal_conv).

        Variable bvmcs_writez64: block.
        Hypothesis hvmcs_writez641 : Genv.find_symbol ge vmcs_writez64 = Some bvmcs_writez64.
        Hypothesis hvmcs_writez642 : Genv.find_funct_ptr ge bvmcs_writez64 =
                                     let arg_type := (Tcons tuint (Tcons tulong Tnil)) in
                                     let ret_type := tvoid in
                                     let cal_conv := cc_default in
                                     let prim := vmcs_writez64 in
                                     Some (External (EF_external prim
                                                                 (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

        Variable bvmcs_write_ident: block.
        Hypothesis hvmcs_write_ident1 : Genv.find_symbol ge vmcs_write_ident = Some bvmcs_write_ident.
        Hypothesis hvmcs_write_ident2 : Genv.find_funct_ptr ge bvmcs_write_ident =
                                        let arg_type := (Tcons tint (Tcons (tptr tvoid) Tnil)) in
                                        let ret_type := tvoid in
                                        let cal_conv := cc_default in
                                        let prim := vmcs_write_ident in
                                        Some (External (EF_external prim
                                                                    (signature_of_type arg_type ret_type cal_conv))
                                                       arg_type ret_type cal_conv).

        Variable brcr0: block.
        Hypothesis hrcr01 : Genv.find_symbol ge rcr0 = Some brcr0.
        Hypothesis hrcr02 : Genv.find_funct_ptr ge brcr0 =
                            let arg_type := Tnil in
                            let ret_type := tint in
                            let cal_conv := cc_default in
                            let prim := rcr0 in
                            Some (External (EF_external prim
                                                        (signature_of_type arg_type ret_type cal_conv))
                                           arg_type ret_type cal_conv).

        Variable brcr3: block.
        Hypothesis hrcr31 : Genv.find_symbol ge rcr3 = Some brcr3.
        Hypothesis hrcr32 : Genv.find_funct_ptr ge brcr3 =
                            let arg_type := Tnil in
                            let ret_type := tint in
                            let cal_conv := cc_default in
                            let prim := rcr3 in
                            Some (External (EF_external prim
                                                        (signature_of_type arg_type ret_type cal_conv))
                                           arg_type ret_type cal_conv).

        Variable brcr4: block.
        Hypothesis hrcr41 : Genv.find_symbol ge rcr4 = Some brcr4.
        Hypothesis hrcr42 : Genv.find_funct_ptr ge brcr4 =
                            let arg_type := Tnil in
                            let ret_type := tint in
                            let cal_conv := cc_default in
                            let prim := rcr4 in
                            Some (External (EF_external prim
                                                        (signature_of_type arg_type ret_type cal_conv))
                                           arg_type ret_type cal_conv).

        Variable brdmsr: block.
        Hypothesis hrdmsr1 : Genv.find_symbol ge rdmsr = Some brdmsr.
        Hypothesis hrdmsr2 : Genv.find_funct_ptr ge brdmsr =
                             let arg_type := (Tcons tint Tnil) in
                             let ret_type := tulong in
                             let cal_conv := cc_default in
                             let prim := rdmsr in
                             Some (External (EF_external prim
                                                         (signature_of_type arg_type ret_type cal_conv))
                                            arg_type ret_type cal_conv).

        Variable bvmptrld: block.
        Hypothesis hvmptrld1 : Genv.find_symbol ge vmptrld = Some bvmptrld.
        Hypothesis hvmptrld2 : Genv.find_funct_ptr ge bvmptrld =
                               let arg_type := Tnil in
                               let ret_type := tvoid in
                               let cal_conv := cc_default in
                               let prim := vmptrld in
                               Some (External (EF_external prim
                                                           (signature_of_type arg_type ret_type cal_conv))
                                              arg_type ret_type cal_conv).

        Variable bvmx_enable: block.
        Hypothesis hvmx_enable1 : Genv.find_symbol ge vmx_enable = Some bvmx_enable.
        Hypothesis hvmx_enable2 : Genv.find_funct_ptr ge bvmx_enable =
                               let arg_type := Tnil in
                               let ret_type := tvoid in
                               let cal_conv := cc_default in
                               let prim := vmx_enable in
                               Some (External (EF_external prim
                                                           (signature_of_type arg_type ret_type cal_conv))
                                              arg_type ret_type cal_conv).

        Variable bvmxinfo_get: block.
        Hypothesis hvmxinfo_get1 : Genv.find_symbol ge vmxinfo_get = Some bvmxinfo_get.
        Hypothesis hvmxinfo_get2 : Genv.find_funct_ptr ge bvmxinfo_get =
                                   let arg_type := (Tcons tint Tnil) in
                                   let ret_type := tint in
                                   let cal_conv := cc_default in
                                   let prim := vmxinfo_get in
                                   Some (External (EF_external prim
                                                               (signature_of_type arg_type ret_type cal_conv))
                                                  arg_type ret_type cal_conv).

        Ltac find_d :=
          match goal with
          | |- context[ret(?current_d,_)] ⇒
            let H := fresh "cd" in
            pose current_d as H
          end.

        Ltac vmxinfo_range :=
          match goal with
          | [real_params: RealParams |- _] ⇒
            destruct real_params; apply real_vmxinfo_range; omega
          end.

        Ltac vmxinfo_get :=
          match goal with
          | [ |- _ = Int.unsigned (Int.repr ( _ ))]
            ⇒ rewrite Int.unsigned_repr;
              ( reflexivity || vmxinfo_range )
          end.

        Ltac vmxinfo_match :=
          match goal with
          | [cd := _: RData,
                      Hvmxinfo:
                     ∀ (i : Z) (v : int) (d0 : RData),
                       _ →
                       _ →
                       _ →
                       _ →
                       ZMap.get i (vmxinfo d0) = Int.unsigned v →
                       vmxinfo_get_spec i d0 = Some (Int.unsigned v)
                       |-
                       match vmxinfo_get_spec ?i _ with
                       | Some _ ⇒ _
                       | None ⇒ _
                       end = _
            ]
            ⇒ exploit (Hvmxinfo i (Int.repr (ZMap.get i real_vmxinfo)) cd); eauto;
               ( omega || vmxinfo_get || unfold cd; intro Hdes; rewrite Hdes; reflexivity)
          end.

        Ltac vmxinfo_proof :=
          match goal with
          | [ Hvmxinfo:
                ∀ (i : Z) (v : int) (d0 : RData),
                  _ →
                  _ →
                  _ →
                  _ →
                  ZMap.get i (vmxinfo d0) = Int.unsigned v →
                  vmxinfo_get_spec i d0 = Some (Int.unsigned v)
                  |-
                  match vmxinfo_get_spec ?i _ with
                  | Some _ ⇒ _
                  | None ⇒ _
                  end = _
            ]
            ⇒
            find_d; vmxinfo_match
          end.

        Lemma vmcs_update2_eq:
          ∀ d v1 v2,
            d {vmcs: v1} {vmcs:v2} = d {vmcs:v2}.
        Proof.
          reflexivity.
        Qed.

        Lemma vmcs_set_defaults_body_correct:
          ∀ m d d´ env le mbi_adr pml4ept_b tss_b gdt_b idt_b msr_bitmap_b io_bitmap_b host_rip_b,
            env = PTree.empty _ →
            PTree.get _mbi_adr le = Some (Vint mbi_adr) →
            high_level_invariant d →
            Genv.find_symbol ge EPT_LOC = Some pml4ept_b →
            Genv.find_symbol ge tss_LOC = Some tss_b →
            Genv.find_symbol ge gdt_LOC = Some gdt_b →
            Genv.find_symbol ge idt_LOC = Some idt_b →
            Genv.find_symbol ge msr_bitmap_LOC = Some msr_bitmap_b →
            Genv.find_symbol ge io_bitmap_LOC = Some io_bitmap_b →
            Genv.find_symbol ge vmx_return_from_guest = Some host_rip_b →
            vmcs_set_defaults_spec (Int.unsigned mbi_adr) pml4ept_b tss_b gdt_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) vmcs_set_defaults_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          generalize max_unsigned64_val; intro mu64val.
          inversion real_params.
          intros.
          unfold vmcs_set_defaults_body.

          assert (Hstatus: ihost d = true ∧ pg d = false ∧ ikern d = true).
          {
            functional inversion H9; subst.
            split; (assumption || split; (assumption || split; (assumption || idtac))).
          }
          destruct Hstatus as [Hh [Hp Hk]].

          assert(Hvmcs: ∃ revid abrtid data, vmcs d = VMCSValid revid abrtid data).
          {
            destruct (vmcs d).
            esplit. esplit. esplit.
            reflexivity.
          }
          destruct Hvmcs as [revid Hvmcs].
          destruct Hvmcs as [abrtid Hvmcs].
          destruct Hvmcs as [data vmcsvalid].

          assert ( Hvmxinfo:
              ∀ i v d,
                1 ≤ i ≤ 14 →
                ihost d = true →
                ikern d = true →
                vmxinfo d = real_vmxinfo →
                ZMap.get i (vmxinfo d) = Int.unsigned v →
                vmxinfo_get_spec i d = Some (Int.unsigned v)).
          {
            intros i v cd Har Hih Hik Hvd Heq.
            unfold vmxinfo_get_spec.
            rewrite Hik, Hih.
            rewrite <- Heq.
            rewrite Hvd.
            reflexivity.
          }
          
          inversion H1.
          functional inversion H9; subst.

          esplit.
          d3 vcgen.
          {
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            vcgen.
            unfold ept_init_spec.
            rewrite H11, H12, H13, H14, H15, H16, H17, H18.
            reflexivity.
          }
          d3 vcgen.
          { repeat vcgen.
            Case ("rdmsr").
            unfold rdmsr_spec; simpl.
            rewrite H12, H13.
            rewrite Int64.unsigned_repr.
            change 0 with (Int.unsigned Int.zero);
              reflexivity.
            - repeat vcgen.
            - SCase ("set revid").
              unfold vmcs_set_revid_spec.
              simpl. rewrite H12, H13, vmcsvalid.
              reflexivity.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
          }

          d3 vcgen.
          { Case ("vmptrld").
            repeat vcgen.
            {
              unfold vmptrld_spec.
              simpl. rewrite H12, H13.
              reflexivity.
            }
            {
              unfold vmptrld_spec.
              simpl. rewrite H12, H13.
              reflexivity.
            }
          }

          d3 vcgen.
          { Case ("vmxinfo get 2").
            repeat vcgen.
            vmxinfo_proof.
          }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmxinfo get 3").
            vmxinfo_proof.
          }
          d3 vcgen.
          {
            repeat vcgen.
            Case ("vmxinfo get 4").
            vmxinfo_proof.
          }
          d3 vcgen.
          {
            repeat vcgen.
            Case ("vmxinfo get 5").
            vmxinfo_proof.
          }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmxinfo get 6").
            vmxinfo_proof.
          }
          d3 vcgen.
          { repeat vcgen.
            Case ("vmxinfo get 7").
            vmxinfo_proof.
          }
          d3 vcgen.
          { repeat vcgen.
            Case ("vmxinfo get 9").
            vmxinfo_proof.
          }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmxinfo get 11").
            vmxinfo_proof.
          }
          d3 vcgen.
          { repeat vcgen.
            Case ("vmxinfo get 13").
            vmxinfo_proof.
          }
          d3 vcgen.
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_writez 16384").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          { repeat vcgen.
            Case ("vmcs_writez 16386").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_writez 16414").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_writez 16396").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          { repeat vcgen.
            Case ("vmcs_writez 16402").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { eassumption. }
          { reflexivity. }
          { repeat vcgen.
            Case ("vmcs_write ident 27670").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen.
            Case ("rcr0").
            unfold rcr0_spec; simpl;
            rewrite Hk, Hh;
            change 0 with (Int.unsigned Int.zero);
            reflexivity.
          }
          { repeat vcgen.
            Case ("vmcs_writez 27648").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            Case ("rcr0").
            unfold rcr0_spec; simpl;
            rewrite Hk, Hh;
            change 0 with (Int.unsigned Int.zero);
            reflexivity.
            - Case ("vmcs_writez 27650").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen.
            Case ("rcr0").
            unfold rcr0_spec; simpl;
            rewrite Hk, Hh;
            change 0 with (Int.unsigned Int.zero);
            reflexivity.
            - Case ("vmcs_writez 27652").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen.
            Case ("vmcs_write z 3072").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { reflexivity. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 3074").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 3076").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            Case ("vmcs_write z 3078").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 3080").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 3082").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            Case ("vmcs_write z 3084").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 27654").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 27656").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            Case ("vmcs_write ident 27658").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { reflexivity. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 27660").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 27662").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { reflexivity. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("rdmsr 372").
            unfold rdmsr_spec; simpl;
            rewrite Hk, Hh;
            change 0 with (Int64.unsigned Int64.zero);
            reflexivity.
          }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write z 19456").
            - unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("rdmsr 373").
              unfold rdmsr_spec; simpl;
              rewrite Hk, Hh;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z 27664").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("rdmsr 374").
              unfold rdmsr_spec; simpl;
              rewrite Hk, Hh;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z 27666").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("rdmsr 911").
              unfold rdmsr_spec; simpl;
              rewrite Hk, Hh;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11268").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("rdmsr 631").
              unfold rdmsr_spec; simpl;
              rewrite Hk, Hh;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11264").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("rdmsr 0xc0000080").
              unfold rdmsr_spec; simpl;
              rewrite Hk, Hh;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11266").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { reflexivity. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26624").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26626").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            - Case ("vmcs_write z 26628").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26650").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z64 10244").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 18474").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26660").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26662").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            - Case ("vmcs_write z64 10242").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 8218").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 8219").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            - Case ("vmcs_write z 0").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 8196").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 8197").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            - Case ("vmcs_write z64 10240").
              unfold vmcs_writez64_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 24576").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply Z_lor_range_lo;
              apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 24580").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          { repeat vcgen.
            - Case ("vmcs_write z 24578").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply Z_lor_range_lo;
              apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 24582").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 8192").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          { repeat vcgen.
            - Case ("vmcs_write z 8193").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            Case ("vmcs_write ident 8194").
            - unfold vmcs_write_ident_spec; simpl;
              rewrite Hk, Hh; reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
            - unfold sizeof; omega.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 8195").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen.
            - Case ("vmcs_write z 18470").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 18468").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen.
            - Case ("vmcs_write z 26658").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh; reflexivity.
          }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          { repeat vcgen. }
          rewrite vmcs_update2_eq.
          d3 vcgen.           { repeat vcgen.
            - Case ("vmcs_write z 16406").
              unfold vmcs_writez_spec; simpl;
              rewrite Hk, Hh.
              rewrite vmcs_update2_eq.
              unfold CalRealIntelModule.real_vmcs.
              rewrite vmcsvalid.
              change (Z.land 0 4294967295) with 0.
              unfold CalRealIntelModule.write64_block_aux.
              change (Vint (Int.repr 1)) with Vone.
              change (Vint (Int.repr 0)) with Vzero.
              simpl.
              reflexivity.
          }
          Qed.

      End VMCSSetDefaultsBody.

      Theorem vmcs_set_defaults__code_correct:
        spec_le
          (vmcs_set_defaults ↦ vmcs_set_defaults_spec_low)
          (〚vmcs_set_defaults ↦ f_vmcs_set_defaults 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigsteptest
          (vmcs_set_defaults_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             b4 Hb4fs Hb4fp
             b5 Hb5fs Hb5fp
             b6 Hb6fs Hb6fp
             b7 Hb7fs Hb7fp
             b8 Hb8fs Hb8fp
             b9 Hb9fs Hb9fp
             b10 Hb10fs Hb10fp
             b11 Hb11fs Hb11fp
             m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´
               (fn_params f_vmcs_set_defaults)
                 (Vint mbi_adr :: nil)
                 (create_undef_temps (fn_temps f_vmcs_set_defaults))
             )
          ) H; try discriminate.
          intro tmpH; destruct tmpH as [le´ stmt].
          repeat fbigstep_post.
      Qed.
    End VMCSSETDEFAULTS.
  End WithPrimitives.
End VMCSINTROCODE.