Library mcertikos.proc.VVMCSIntroCodeSetDesc

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.

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

Module VMCSINTROCODESETDESC.

  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.

    Section VMXSETDESC2.

      Let L: compatlayer (cdata RData) :=
        vmcs_writez gensem vmcs_writez_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 VMXSetDesc2Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmcs_writez
        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
                                   Some (External (EF_external vmcs_writez
                                                               (signature_of_type arg_type ret_type cal_conv))
                                                  arg_type ret_type cal_conv).

        Lemma vmx_set_desc2_body_correct:
           m d env le seg lim ar,
            env = PTree.empty _
            PTree.get _seg le = Some (Vint seg) →
            PTree.get _lim le = Some (Vint lim) →
            PTree.get _ar le = Some (Vint ar) →
            True
            True
            vmx_set_desc2_spec (Int.unsigned seg) (Int.unsigned lim)
                              (Int.unsigned ar) d = Some
            high_level_invariant d
            kernel_mode d
             le´,
              exec_stmt ge env le ((m, d): mem) vmx_set_desc2_body E0 le´ (m, )
                        Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.

          assert(evval: Int.unsigned seg = C_GUEST_CS
                        Int.unsigned seg = C_GUEST_DS
                        Int.unsigned seg = C_GUEST_ES
                        Int.unsigned seg = C_GUEST_FS
                        Int.unsigned seg = C_GUEST_GS
                        Int.unsigned seg = C_GUEST_SS
                        Int.unsigned seg = C_GUEST_LDTR
                        Int.unsigned seg = C_GUEST_TR
                        Int.unsigned seg = C_GUEST_GDTR
                        Int.unsigned seg = C_GUEST_IDTR
                        Int.unsigned seg > C_GUEST_IDTR).
          {
            generalize (Int.unsigned_range seg); intro.
            repeat autounfold in H.
            unfold two_power_nat in H.
            unfold shift_nat in H.
            simpl in H.
            omega.
          }

          assert (
            ihost d = true pg d = true ikern d = true
           revid, abrtid, m,
                                                  ZMap.get (CPU_ID d) (vmcs d)
                                                  = VMCSValid revid abrtid m).
          {
            functional inversion H5; subst.
            split; (assumption || split; (assumption || split; (assumption || idtac))).
             revid, abrtid, d0; assumption.
          }
          assert (CPU_range: 0 (CPU_ID d) < 8).
          { inv H6; auto. }
          assert (vmcs_double_update: vmcspool vmcspool´,
                     d {vmcs : vmcspool} {vmcs: vmcspool´} =
                     d {vmcs : vmcspool´}).
          { unfold update_vmcs.
            simpl.
            auto. }
          destruct H as [Hh [Hp [Hk Hd]]].
          destruct Hd.
          destruct H.
          destruct H.
          destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc2_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            reflexivity.

          - functional inversion H5;
            functional inversion H14;
            functional inversion H16; omega.
        Qed.

      End VMXSetDesc2Body.

      Theorem vmx_set_desc2_body__code_correct:
        spec_le
          (vmx_set_desc2 vmx_set_desc2_spec_low)
          (vmx_set_desc2 f_vmx_set_desc2 L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        Require Import TacticsForTesting.
        fbigsteptest
          (vmx_set_desc2_body_correct
             s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
             m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´
                (fn_params f_vmx_set_desc2)
                (Vint seg :: Vint lim :: Vint ar :: nil)
                (create_undef_temps (fn_temps f_vmx_set_desc2))
             )
          ) H0; try discriminate.
        intro tmpH; destruct tmpH as [le´ stmt].
        repeat fbigstep_post.
      Qed.

    End VMXSETDESC2.

    Section VMXSETDESC1.

      Let L: compatlayer (cdata RData) :=
        vmcs_writez gensem vmcs_writez_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 VMXSetDesc1Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmcs_writez
        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
                                   Some (External (EF_external vmcs_writez
                                                               (signature_of_type arg_type ret_type cal_conv))
                                                  arg_type ret_type cal_conv).

        Lemma vmx_set_desc1_body_correct:
           m d env le seg sel base,
            env = PTree.empty _
            PTree.get _seg le = Some (Vint seg) →
            PTree.get _sel le = Some (Vint sel) →
            PTree.get _base le = Some (Vint base) →
            True
            True
            vmx_set_desc1_spec (Int.unsigned seg) (Int.unsigned sel)
                              (Int.unsigned base) d = Some
            high_level_invariant d
            kernel_mode d
             le´,
              exec_stmt ge env le ((m, d): mem) vmx_set_desc1_body E0 le´ (m, )
                        Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.

          assert(evval: Int.unsigned seg = C_GUEST_CS
                        Int.unsigned seg = C_GUEST_DS
                        Int.unsigned seg = C_GUEST_ES
                        Int.unsigned seg = C_GUEST_FS
                        Int.unsigned seg = C_GUEST_GS
                        Int.unsigned seg = C_GUEST_SS
                        Int.unsigned seg = C_GUEST_LDTR
                        Int.unsigned seg = C_GUEST_TR
                        Int.unsigned seg = C_GUEST_GDTR
                        Int.unsigned seg = C_GUEST_IDTR
                        Int.unsigned seg > C_GUEST_IDTR).
          {
            generalize (Int.unsigned_range seg); intro.
            repeat autounfold in H.
            unfold two_power_nat in H.
            unfold shift_nat in H.
            simpl in H.
            omega.
          }

          assert (
            ihost d = true pg d = true ikern d = true
           revid, abrtid, m,
                                                  ZMap.get (CPU_ID d) (vmcs d)
                                                  = VMCSValid revid abrtid m).
          {
            functional inversion H5; subst.
            split; (assumption || split; (assumption || split; (assumption || idtac))).
             revid, abrtid, d0; assumption.
          }
          assert (CPU_range: 0 (CPU_ID d) < 8).
          { inv H6; auto. }
          assert (vmcs_double_update: vmcspool vmcspool´,
                     d {vmcs : vmcspool} {vmcs: vmcspool´} =
                     d {vmcs : vmcspool´}).
          { unfold update_vmcs.
            simpl.
            auto. }
          destruct H as [Hh [Hp [Hk Hd]]].
          destruct Hd.
          destruct H.
          destruct H.
          destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            reflexivity.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite ZMap.gss.
            rewrite ZMap.set2.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            rewrite vmcs_double_update.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            reflexivity.

          - esplit.
            repeat vcgen.
            unfold vmcs_writez_spec.
            simpl.
            rewrite Hk, Hp, Hh.
            rewrite zle_lt_true; try omega.
            rewrite H.
            rewrite evval in H5; simpl in H5.
            unfold vmx_set_desc1_spec in H5; simpl in H5.
            rewrite Hh, Hp, Hk in H5.
            rewrite zle_lt_true in H5; try omega.
            rewrite H in H5.
            inversion H5.
            unfold aux_zmap_4val_set, aux_zmap_2val_set.
            repeat rewrite Int.repr_unsigned.
            reflexivity.

          - functional inversion H5;
            functional inversion H14;
            functional inversion H16; omega.
        Qed.

      End VMXSetDesc1Body.

      Theorem vmx_set_desc1_body__code_correct:
        spec_le
          (vmx_set_desc1 vmx_set_desc1_spec_low)
          (vmx_set_desc1 f_vmx_set_desc1 L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        Require Import TacticsForTesting.
        fbigsteptest
          (vmx_set_desc1_body_correct
             s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
             m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´
                (fn_params f_vmx_set_desc1)
                (Vint seg :: Vint sel :: Vint base :: nil)
                (create_undef_temps (fn_temps f_vmx_set_desc1))
             )
          ) H0; try discriminate.
        intro tmpH; destruct tmpH as [le´ stmt].
        repeat fbigstep_post.
      Qed.

    End VMXSETDESC1.

  End WithPrimitives.

End VMCSINTROCODESETDESC.