Library mcertikos.virt.intel.VVMCSIntroCodeSetDesc

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

Require Import Coqlib.
Require Import 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.

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.

Module VMCSINTROCODESETDESC.

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

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

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        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_desc_body_correct:
          ∀ m d d´ env le seg sel base lim ar,
            env = PTree.empty _ →
            PTree.get tseg le = Some (Vint seg) →
            PTree.get tsel le = Some (Vint sel) →
            PTree.get tbase le = Some (Vint base) →
            PTree.get tlim le = Some (Vint lim) →
            PTree.get tar le = Some (Vint ar) →
            vmx_set_desc_spec (Int.unsigned seg) (Int.unsigned sel)
                              (Int.unsigned base) (Int.unsigned lim)
                              (Int.unsigned ar) d
            = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) vmx_set_desc_body E0 le´ (m, d´)
                        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, vmcs d = VMCSValid revid abrtid m).
          {
            functional inversion H5; subst.
            split; (assumption || split; (assumption || split; (assumption || idtac))).
            ∃ revid, abrtid, d0; assumption.
          }
          destruct H as [Hh [Hp [Hk Hd]]].
          destruct Hd.
          destruct H.
          destruct H.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          reflexivity.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          rewrite H in H5.
          inversion H5.
          unfold aux_zmap_4val_set, aux_zmap_2val_set.
          repeat rewrite Int.repr_unsigned.
          reflexivity.

          Caseeq evval; intro evval.
          esplit.
          repeat vcgen.
          unfold vmcs_writez_spec.
          simpl.
          rewrite Hk, Hp, Hh.
          rewrite evval in H5; simpl in H5.
          unfold vmx_set_desc_spec in H5; simpl in H5.
          rewrite Hh, Hp, Hk in H5.
          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 H11;
          functional inversion H13; omega.

        Qed.

      End VMXSetDescBody.

      Theorem vmx_set_desc_body__code_correct:
        spec_le
          (vmx_set_desc ↦ vmx_set_desc_spec_low)
          (〚vmx_set_desc ↦ f_vmx_set_desc 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        Require Import TacticsForTesting.
        fbigsteptest
          (vmx_set_desc_body_correct
             s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
             m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´
                (fn_params f_vmx_set_desc)
                (Vint seg :: Vint sel :: Vint base :: Vint lim :: Vint ar :: nil)
                (create_undef_temps (fn_temps f_vmx_set_desc))
             )
          ) H0; try discriminate.
        intro tmpH; destruct tmpH as [le´ stmt].
        repeat fbigstep_post.
      Qed.

    End VMXSETDESC.

  End WithPrimitives.

End VMCSINTROCODESETDESC.