Library mcertikos.proc.VVMCSIntroCodeSetDefaults

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 VVMCSIntro.
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 `{multi_oracle_prop: MultiOracleProp}.


    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.

    Lemma seteq: ∀ i m1 m2 (v1 v2: Z), v1 = v2 → m1 = m2 → ZMap.set i v1 m1 = ZMap.set i v2 m2.
    Proof.
      intros.
      subst.
      reflexivity.
    Qed.

    Section VMCSSETDEFAULTS.

      Let L: compatlayer (cdata RData) :=
        get_CPU_ID ↦ gensem get_CPU_ID_spec
                   ⊕ get_curid ↦ gensem get_curid_spec
                   ⊕ 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 := 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 bget_CPU_ID: block.
        Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
        Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID =
                            let arg_type := Tnil in
                            let ret_type := tint in
                            let cal_conv := cc_default in
                            let prim := get_CPU_ID in
                            Some (External (EF_external prim
                                                        (signature_of_type arg_type ret_type cal_conv))
                                           arg_type ret_type cal_conv).

        Variable bget_curid: block.
        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.
        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid =
                            let arg_type := Tnil in
                            let ret_type := tint in
                            let cal_conv := cc_default in
                            let prim := get_curid 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
          | [ cd := _: RData,
                       H: vmxinfo _ = real_vmxinfo
                    |- _ = Int.unsigned (Int.repr ( _ ))]
            ⇒ unfold cd; simpl; rewrite H; 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 pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b,
            env = PTree.empty _ →
            high_level_invariant d →
            Genv.find_symbol ge EPT_LOC = Some pml4ept_b →
            Genv.find_symbol ge STACK_LOC = Some stack_b →
            True →
            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 pml4ept_b stack_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.
          Opaque Z.add Z.mul.
          generalize max_unsigned_val; intro muval.
          generalize tcharsize; intro tcharsize.
          generalize max_unsigned64_val; intro mu64val.
          inversion real_params.
          intros.
          unfold vmcs_set_defaults_body.

          assert(arrsize: sizeof (Tarray tuchar 4096 noattr) = 4096) by reflexivity.
          assert(arrsize2: sizeof (Tarray tuchar 8192 noattr) = 8192) by reflexivity.
          assert(maxval: Z.max 0 4096 = 4096) by reflexivity.
          assert(maxval2: Z.max 0 8192 = 8192) by reflexivity.
          assert (Hstatus: ihost d = true ∧ pg d = true ∧ ikern d = true).
          { functional inversion H8; subst.
            split; (assumption || split; (assumption || split; (assumption || idtac))). }
          destruct Hstatus as [Hh [Hp Hk]].

          assert(Hvmcs: ∃ revid abrtid data,
                    ZMap.get (CPU_ID d) (vmcs d) = VMCSValid revid abrtid data).
          { remember (ZMap.get (CPU_ID d) (vmcs d)) as vmcs´.
            destruct vmcs´.
            ∃ revid, abrtid, data; trivial. }
          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 H0.
          functional inversion H8; subst.
          assert (r_vmx_info : vmxinfo d = real_vmxinfo).
          { eapply valid_vmxinfo; auto. }

          esplit.
          unfold exec_stmt.
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            unfold get_CPU_ID_spec.
            unfold ObjMultiprocessor.get_CPU_ID_spec.
            rewrite H11, H12.
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
          }
          change E0 with (E0 ** E0).
          econstructor.
          {
            repeat vcgen.
            unfold get_curid_spec; simpl.
            unfold ObjMultiprocessor.get_curid_spec; simpl.
            rewrite H11, H12.
            rewrite Int.unsigned_repr.
            reflexivity.
            omega.
          }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("rdmsr").
            unfold rdmsr_spec; simpl.
            rewrite H11, H12.
            rewrite Int64.unsigned_repr.
            change 0 with (Int.unsigned Int.zero); reflexivity.
            - repeat vcgen.
            - SCase ("set revid").
              unfold vmcs_set_revid_spec.
              simpl.
              rewrite H11, H12, vmcsvalid.
              rewrite H14.
              rewrite zle_lt_true; auto.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range.
            - repeat discharge_unsigned_range. }
          change E0 with (E0 ** E0).
          econstructor.
          { Case ("vmptrld").
            repeat vcgen.
            { unfold vmptrld_spec.
              simpl.
              rewrite H11, H12.
              reflexivity. }
            
          }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 2").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 3").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 4").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 5").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 6").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 7").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 9").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 11").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmxinfo get 13").
            vmxinfo_proof. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_writez 16384").
            - unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_writez 16386").
            - unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_writez 16414").
            - unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_writez 16396").
            - unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_writez 16402").
            - unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 27670").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rcr0").
              unfold rcr0_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int.unsigned Int.zero);
              reflexivity.
            - Case ("vmcs_writez 27648").
              unfold vmcs_writez_spec; simpl;
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rcr0").
              unfold rcr0_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int.unsigned Int.zero);
              reflexivity.
            - Case ("vmcs_writez 27650").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rcr0").
              unfold rcr0_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int.unsigned Int.zero);
              reflexivity.
            - Case ("vmcs_writez 27652").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3072").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3074").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3076").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3078").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3080").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3082").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 3084").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 27654").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 27656").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 27658").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - rewrite maxval; omega.
            - rewrite maxval; omega.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 27660").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - rewrite maxval; omega.
            - rewrite maxval; omega.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 27662").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 372").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z 19456").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 373").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z 27664").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 374").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z 27666").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega.
            - unfold Int64.zero;
              rewrite Int64.unsigned_repr; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 911").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11268").
              unfold vmcs_writez64_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 631").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11264").
              unfold vmcs_writez64_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("rdmsr 0xc0000080").
              unfold rdmsr_spec; simpl;
              rewrite H11, H12;
              change 0 with (Int64.unsigned Int64.zero);
              reflexivity.
            - Case ("vmcs_write z64 11266").
              unfold vmcs_writez64_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26624").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26626").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26628").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26650").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z64 10244").
            unfold vmcs_writez64_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 18474").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26660").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26662").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z64 10242").
            unfold vmcs_writez64_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 8218").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - erewrite <- stencil_matches_symbols; eauto.
          }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 8219").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 0").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 8196").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 8197").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z64 10240").
            unfold vmcs_writez64_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("vmcs_write z 24576").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              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. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("vmcs_write z 24580").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("vmcs_write z 24578").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              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. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            - Case ("vmcs_write z 24582").
              unfold vmcs_writez_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - apply real_vmxinfo_range; omega.
            - apply real_vmxinfo_range; omega. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 8192").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 8193").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write ident 8194").
            - unfold vmcs_write_ident_spec; simpl.
              rewrite H11, H12, H14, zle_lt_true; try assumption.
              rewrite ZMap.gss.
              rewrite vmcs_update2_eq.
              rewrite ZMap.set2.
              reflexivity.
            - rewrite maxval2; omega.
            - rewrite maxval2; omega.
            - erewrite <- stencil_matches_symbols; eauto. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 8195").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 18470").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 18468").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          change E0 with (E0 ** E0).
          econstructor.
          { repeat vcgen.
            Case ("vmcs_write z 26658").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            rewrite ZMap.set2.
            reflexivity. }
          { repeat vcgen.
            Case ("vmcs_write z 16406").
            unfold vmcs_writez_spec; simpl.
            rewrite H11, H12, H14, zle_lt_true; try assumption.
            rewrite ZMap.gss.
            rewrite vmcs_update2_eq.
            unfold Calculate_VMCS_at_i.
            rewrite ZMap.set2.
            idtac.
            rewrite vmcsvalid.
            unfold ret; simpl.
            repeat rewrite Z.mul_1_l.
            repeat rewrite Z.add_0_l.
            rewrite maxval, maxval2.
            replace (8192 × CPU_ID d) with (CPU_ID d × 4096 × 2) by omega.
            change (Vint (Int.repr (Z.land 0 4294967295))) with Vzero.
            replace (4096 × CPU_ID d) with (CPU_ID d × 4096) by omega.
            unfold write64_block_aux; simpl.
            replace (4096 × ZMap.get (CPU_ID d) (cid d)) with (ZMap.get (CPU_ID d) (cid d) × 4096) by omega.
            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
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             b4 Hb4fs Hb4fp
             b5 Hb5fs Hb5fp
             b6 Hb6fs Hb6fp
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b7 Hb7fs Hb7fp
             b8 Hb8fs Hb8fp
             b9 Hb9fs Hb9fp
             b10 Hb10fs Hb10fp
             b11 Hb11fs Hb11fp
             b13 Hb13fs Hb13fp
             m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´
               (fn_params f_vmcs_set_defaults)
               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.