Library mcertikos.trap.TTrapArgCode5

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 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 TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource.
Require Import ObjTrap.
Require Import CommonTactic.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Lemma int_wrap:
  Int.repr (-1) = Int.repr (Int.max_unsigned).
Proof.
  apply Int.eqm_samerepr.
  unfold Int.eqm.
  unfold Int.eqmod.
   (-1).
  reflexivity.
Qed.

Lemma unsigned_int_range:
   x: int,
    0 Int.unsigned x Int64.max_unsigned.
Proof.
  split.
  apply Int.unsigned_range.
  apply Z.le_trans with (m:=Int.max_unsigned);
    ( apply Int.unsigned_range_2 ||
            unfold Int.max_unsigned, Int64.max_unsigned;
      simpl; omega).
Qed.

Lemma cat_unsigned64_lor_range:
   lo hi,
    0 Z.lor (Z.shiftl (Int.unsigned hi) 32) (Int.unsigned lo) Int64.max_unsigned.
Proof.
  intros lo hi.
  apply Z64_lor_range.
  apply Z_shiftl_32_range.
  apply Int.unsigned_range_2.
  apply unsigned_int_range.
Qed.

Lemma unsigned_div_2pow32_eq_0:
   x, Int.unsigned x / 2 ^ 32 = 0.
Proof.
  intro.
  generalize (Int.unsigned_range x); intro.
  repeat autounfold in H.
  unfold two_power_nat, shift_nat in H.
  simpl in H.
  change (2 ^ 32) with 4294967296.
  xomega.
Qed.

Lemma unsigned_shiftl_lor_shiftr_range:
   x y n,
    0 n
    0 Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) n) (Int.unsigned y)) n Int.max_unsigned.
Proof.
  split.
  - apply Z.shiftr_nonneg.
    apply Z_lor_range_lo.
    + apply Z.shiftl_nonneg.
      apply Int.unsigned_range.
    + apply Int.unsigned_range.
  - rewrite Z.shiftr_lor.
    rewrite Z.shiftr_shiftl_r.
    + rewrite Z.sub_diag with (n:=n).
      rewrite Z.shiftr_0_r.
      rewrite Z.shiftr_div_pow2.
      apply Z_lor_range.
      apply Int.unsigned_range_2.
      split.
      × change 0 with (0 / 2 ^ n).
        apply Z_div_le.
        apply Z.lt_gt.
        apply Z.pow_pos_nonneg; omega.
        apply Int.unsigned_range.
      × rewrite <- Z_div_mult_full with (a:=Int.max_unsigned)(b:=2^n).
        {
          apply Z_div_le.
          - apply Z.lt_gt.
            apply Z.pow_pos_nonneg; omega.
          - apply Z.le_trans with (m:=Int.max_unsigned).
            + apply Int.unsigned_range_2.
            + apply Z.le_mul_diag_r with (n:=Int.max_unsigned)(m:=2^n).
              × repeat autounfold.
                unfold two_power_nat, shift_nat.
                simpl.
                omega.
              × apply Zle_lt_or_eq in H.
                destruct H.
                {
                  generalize (Z.pow_gt_1 2 n).
                  intro Hr.
                  destruct Hr.
                  - omega.
                  - apply H0 in H.
                    omega.
                }
                rewrite <- H.
                simpl.
                omega.
        }
        apply Z.pow_nonzero.
        omega.
        assumption.
      × assumption.
    + assumption.
Qed.

Lemma unsigned_shiftl_lor_shiftr_32_range:
   x y,
    0 Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) 32) (Int.unsigned y)) 32 Int.max_unsigned.
Proof.
  intros.
  apply unsigned_shiftl_lor_shiftr_range with (n:=32).
  omega.
Qed.

Lemma Z_mod_range:
   x n,
    n > 0 →
    0 x mod n n - 1.
Proof.
  intros.
  assert(0 x mod n < n).
  apply Z_mod_lt.
  omega.
  omega.
Qed.

Ltac intomega :=
  repeat autounfold; unfold two_power_nat, shift_nat; simpl; omega.

Hint Resolve Z_lor_range_lo.
Hint Resolve Z_land_range_lo.
Hint Resolve Z_shiftl_32_range.
Hint Resolve Int.unsigned_range_2.
Hint Resolve cat_unsigned64_lor_range.
Hint Resolve Z.shiftr_nonneg.
Hint Resolve unsigned_shiftl_lor_shiftr_range.
Hint Resolve unsigned_shiftl_lor_shiftr_32_range.

Module TTRAPARGCODE.

  Section WithPrimitives.

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

    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

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

    Section SYSSETTSCOFFSET.

      Let L: compatlayer (cdata RData) :=
        vmx_set_tsc_offset gensem thread_vmx_set_tsc_offset_spec
                     uctx_arg2 gensem uctx_arg2_spec
                     uctx_arg3 gensem uctx_arg3_spec
                     uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysSetTscOffsetBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_set_tsc_offset
        Variable bvmx_set_tsc_offset: block.
        Hypothesis hvmx_set_tsc_offset1 : Genv.find_symbol ge vmx_set_tsc_offset = Some bvmx_set_tsc_offset.
        Hypothesis hvmx_set_tsc_offset2 : Genv.find_funct_ptr ge bvmx_set_tsc_offset =
                                     let arg_type := Tcons tulong Tnil in
                                     let ret_type := tvoid in
                                     let cal_conv := cc_default in
                                     let prim := vmx_set_tsc_offset in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_arg3
        Variable buctx_arg3: block.
        Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
        Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
                                 Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_set_tsc_offset_body_correct: m d env le,
            env = PTree.empty _
            trap_set_tsc_offset_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_set_tsc_offset_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          generalize max_unsigned64_val; intro muval64.

          intros; subst.
          functional inversion H0; subst.
          functional inversion H1.
          functional inversion H2.
          unfold sys_set_tsc_offset_body.
          generalize (Int.unsigned_range_2 n); intro.
          generalize (Int.unsigned_range_2 n0); intro.

          rewrite <- H4 in ×.
          rewrite <- H12 in ×.
          unfold ofs in ×.

          esplit.
          repeat vcgen.

          unfold Int64.add.
          rewrite <- H12 in H3.
          rewrite <- H4 in H3.
          assumption.
        Qed.

      End SysSetTscOffsetBody.

      Theorem sys_set_tsc_offset_body_code_correct:
        spec_le
          (sys_set_tsc_offset trap_set_tsc_offset_spec_low)
          (sys_set_tsc_offset f_sys_set_tsc_offset L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_set_tsc_offset_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_set_tsc_offset)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_set_tsc_offset)))) H.
      Qed.

    End SYSSETTSCOFFSET.

    Section SYSGETTSCOFFSET.

      Let L: compatlayer (cdata RData) :=
        vmx_get_tsc_offset gensem thread_vmx_get_tsc_offset_spec
                     uctx_set_retval1 gensem uctx_set_retval1_spec
                     uctx_set_retval2 gensem uctx_set_retval2_spec
                     uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysGetTscOffsetBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_get_tsc_offset
        Variable bvmx_get_tsc_offset: block.
        Hypothesis hvmx_get_tsc_offset1 : Genv.find_symbol ge vmx_get_tsc_offset = Some bvmx_get_tsc_offset.
        Hypothesis hvmx_get_tsc_offset2 : Genv.find_funct_ptr ge bvmx_get_tsc_offset =
                                     let arg_type := Tnil in
                                     let ret_type := tulong in
                                     let cal_conv := cc_default in
                                     let prim := vmx_get_tsc_offset in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_set_retval1
        Variable buctx_set_retval1: block.
        Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
        Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
                                        Some (External (EF_external uctx_set_retval1
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_retval2
        Variable buctx_set_retval2: block.
        Hypothesis huctx_set_retval21 : Genv.find_symbol ge uctx_set_retval2 = Some buctx_set_retval2.
        Hypothesis huctx_set_retval22 : Genv.find_funct_ptr ge buctx_set_retval2 =
                                        Some (External (EF_external uctx_set_retval2
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_get_tsc_offset_body_correct: m d env le,
            env = PTree.empty _
            trap_get_tsc_offset_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_get_tsc_offset_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          generalize max_unsigned64_val; intro muval64.

          intros; subst.
          functional inversion H0; subst.
          unfold ofs1, ofs2 in ×.
          unfold sys_get_tsc_offset_body.
          assert(ofsrange: 0 ofs Int64.max_unsigned).
          {
            functional inversion H1; subst.
            functional inversion H4; subst.
            unfold Z64Lemma.Z64ofwords.
            apply Z64_lor_range.
            apply Z_shiftl_32_range.
            apply Int.unsigned_range_2.
            split.
            discharge_unsigned_range.
            apply Z.le_trans with (m:=Int.max_unsigned).
            apply Int.unsigned_range_2.
            omega.
          }

          assert(ofsmodrange: 0 ofs mod 4294967296 Int.max_unsigned).
          {
            apply Z_mod_range.
            omega.
          }

          esplit.
          d3 vcgen.
          repeat vcgen.
          instantiate (1:= (Int64.repr ofs)).
          rewrite Int64.unsigned_repr.
          reflexivity.
          omega.
          d3 vcgen.
          repeat vcgen.
          d3 vcgen.
          repeat vcgen.
          repeat vcgen.
          repeat vcgen.
          unfold Int64.divu.
          repeat vcgen.
          xomega.
          xomega.
          xomega.
          xomega.
          xomega.
          repeat vcgen.
          unfold Int64.modu.
          repeat vcgen.
        Qed.

      End SysGetTscOffsetBody.

      Theorem sys_get_tsc_offset_body_code_correct:
        spec_le
          (sys_get_tsc_offset trap_get_tsc_offset_spec_low)
          (sys_get_tsc_offset f_sys_get_tsc_offset L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_get_tsc_offset_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_get_tsc_offset)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_get_tsc_offset)))) H.
      Qed.

    End SYSGETTSCOFFSET.

    Section SYSINJECTEVENT.

      Let L: compatlayer (cdata RData) :=
        uctx_arg2 gensem uctx_arg2_spec
         uctx_arg3 gensem uctx_arg3_spec
         uctx_arg4 gensem uctx_arg4_spec

         vmx_inject_event gensem thread_vmx_inject_event_spec
         uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysInjectEventBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_arg3
        Variable buctx_arg3: block.
        Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
        Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
                                 Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).
uctx_arg4
        Variable buctx_arg4: block.
        Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
        Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
                                 Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

vmx_inject_event
        Variable bvmx_inject_event: block.
        Hypothesis hvmx_inject_event1 : Genv.find_symbol ge vmx_inject_event = Some bvmx_inject_event.
        Hypothesis hvmx_inject_event2 : Genv.find_funct_ptr ge bvmx_inject_event =
                                     let arg_type := (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))) in
                                     let ret_type := tvoid in
                                     let cal_conv := cc_default in
                                     let prim := vmx_inject_event in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_inject_event_body_correct: m d env le,
            env = PTree.empty _
            trap_inject_event_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_inject_event_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst.
          functional inversion H2; subst.
          functional inversion H3; subst.
          unfold sys_inject_event_body.
          assert(0 Int.unsigned n1 mod 256 Int.max_unsigned).
          {
            assert (0 Int.unsigned n1 mod 256 < 256).
            {
              eapply Z_mod_lt; omega.
            }
            omega.
          }
          esplit.
          repeat vcgen.
          discharge_cmp.
          generalize (Int.unsigned_range n1); unfold Int.modulus, two_power_nat, shift_nat; simpl; intro.
          xomega.
        Qed.

      End SysInjectEventBody.

      Theorem sys_inject_event_code_correct:
        spec_le
          (sys_inject_event trap_inject_event_spec_low)
          (sys_inject_event f_sys_inject_event L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_inject_event_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             b4 Hb4fs Hb4fp

             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_inject_event)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_inject_event)))) H.
      Qed.

    End SYSINJECTEVENT.


    Section SYSSETREG.

      Let L: compatlayer (cdata RData) :=
        vmx_set_reg gensem thread_vmx_set_reg_spec
                     uctx_arg2 gensem uctx_arg2_spec
                     uctx_arg3 gensem uctx_arg3_spec
                     uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysSetRegBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_set_reg
        Variable bvmx_set_reg: block.
        Hypothesis hvmx_set_reg1 : Genv.find_symbol ge vmx_set_reg = Some bvmx_set_reg.
        Hypothesis hvmx_set_reg2 : Genv.find_funct_ptr ge bvmx_set_reg =
                                     let arg_type := Tcons tuint (Tcons tuint Tnil) in
                                     let ret_type := tvoid in
                                     let cal_conv := cc_default in
                                     let prim := vmx_set_reg in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_arg3
        Variable buctx_arg3: block.
        Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
        Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
                                 Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_set_reg_body_correct: m d env le,
            env = PTree.empty _
            trap_set_reg_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_set_reg_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst;
          functional inversion H2; subst;
          functional inversion H4; subst;
          functional inversion H5; subst;
          rewrite Int.repr_unsigned in H, H4;
          unfold sys_set_reg_body;
          esplit;
            repeat vcgen.
          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.

          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.

          functional inversion H1; subst;
          functional inversion H2; subst.

          destruct _x;
          unfold sys_set_reg_body;
          esplit;
          repeat vcgen.
          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.
        Qed.

      End SysSetRegBody.

      Theorem sys_set_reg_body_code_correct:
        spec_le
          (sys_set_reg trap_set_reg_spec_low)
          (sys_set_reg f_sys_set_reg L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_set_reg_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_set_reg)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_set_reg)))) H.
      Qed.

    End SYSSETREG.


    Section SYSGETREG.

      Let L: compatlayer (cdata RData) :=
        vmx_get_reg gensem thread_vmx_get_reg_spec
                     uctx_arg2 gensem uctx_arg2_spec
                     uctx_set_retval1 gensem uctx_set_retval1_spec
                     uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysGetRegBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_get_reg
        Variable bvmx_get_reg: block.
        Hypothesis hvmx_get_reg1 : Genv.find_symbol ge vmx_get_reg = Some bvmx_get_reg.
        Hypothesis hvmx_get_reg2 : Genv.find_funct_ptr ge bvmx_get_reg =
                                     let arg_type := Tcons tuint Tnil in
                                     let ret_type := tuint in
                                     let cal_conv := cc_default in
                                     let prim := vmx_get_reg in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_set_retval1
        Variable buctx_set_retval1: block.
        Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
        Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
                                        Some (External (EF_external uctx_set_retval1
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_get_reg_body_correct: m d env le,
            env = PTree.empty _
            trap_get_reg_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_get_reg_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst.
          functional inversion H3; subst.
          functional inversion H5; subst.
          unfold sys_get_reg_body.
          esplit;
            repeat vcgen.
          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.

          unfold sys_get_reg_body.
          esplit;
            repeat vcgen.
          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.

          unfold sys_get_reg_body.
          functional inversion H1; subst.

          destruct _x.

          esplit;
            repeat vcgen.

          esplit; repeat vcgen.
          discharge_cmp.
          econstructor.
          discharge_cmp.
          repeat vcgen.
        Qed.

      End SysGetRegBody.

      Theorem sys_get_reg_body_code_correct:
        spec_le
          (sys_get_reg trap_get_reg_spec_low)
          (sys_get_reg f_sys_get_reg L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_get_reg_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_get_reg)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_get_reg)))) H.
      Qed.

    End SYSGETREG.

    Section SYSGETNEXTEIP.

      Let L: compatlayer (cdata RData) :=
        vmx_get_next_eip gensem thread_vmx_get_next_eip_spec
                          uctx_set_retval1 gensem uctx_set_retval1_spec
                          uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysGetNextEipBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_get_next_eip
        Variable bvmx_get_next_eip: block.
        Hypothesis hvmx_get_next_eip1 : Genv.find_symbol ge vmx_get_next_eip = Some bvmx_get_next_eip.
        Hypothesis hvmx_get_next_eip2 : Genv.find_funct_ptr ge bvmx_get_next_eip =
                                     let arg_type := Tnil in
                                     let ret_type := tuint in
                                     let cal_conv := cc_default in
                                     let prim := vmx_get_next_eip in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_set_retval1
        Variable buctx_set_retval1: block.
        Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
        Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
                                        Some (External (EF_external uctx_set_retval1
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_get_next_eip_body_correct: m d env le,
            env = PTree.empty _
            trap_get_next_eip_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_get_next_eip_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst.
          functional inversion H4; subst.
          unfold sys_get_next_eip_body.
          esplit;
            repeat vcgen.
          instantiate (1:= (Int.repr (Int.unsigned v1 + Int.unsigned v2))).
          rewrite Int.unsigned_repr; try omega.
          reflexivity.
          rewrite Int.unsigned_repr; try omega.
          eassumption.
        Qed.

      End SysGetNextEipBody.

      Theorem sys_get_next_eip_code_correct:
        spec_le
          (sys_get_next_eip trap_get_next_eip_spec_low)
          (sys_get_next_eip f_sys_get_next_eip L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_get_next_eip_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_get_next_eip)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_get_next_eip)))) H.
      Qed.

    End SYSGETNEXTEIP.


    Section SYSINTERCEPTINTWINDOW.

      Let L: compatlayer (cdata RData) :=
        vmx_set_intercept_intwin gensem thread_vmx_set_intercept_intwin_spec
                                  uctx_arg2 gensem uctx_arg2_spec
                                  uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysInterceptIntWindowBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_set_intercept_intwin
        Variable bvmx_set_intercept_intwin: block.
        Hypothesis hvmx_set_intercept_intwin1 : Genv.find_symbol ge vmx_set_intercept_intwin = Some bvmx_set_intercept_intwin.
        Hypothesis hvmx_set_intercept_intwin2 : Genv.find_funct_ptr ge bvmx_set_intercept_intwin =
                                     let arg_type := Tcons tint Tnil in
                                     let ret_type := Tvoid in
                                     let cal_conv := cc_default in
                                     let prim := vmx_set_intercept_intwin in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_intercept_int_window_body_correct: m d env le,
            env = PTree.empty _
            trap_intercept_int_window_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_set_intercept_intwin_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst.
          functional inversion H2; subst;
          functional inversion H3; subst;
          unfold sys_set_intercept_intwin_body;
          esplit;
          repeat vcgen.
        Qed.

      End SysInterceptIntWindowBody.

      Theorem sys_intercept_int_window_code_correct:
        spec_le
          (sys_intercept_int_window trap_intercept_int_window_spec_low)
          (sys_intercept_int_window f_sys_set_intercept_intwin L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_intercept_int_window_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_set_intercept_intwin)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_set_intercept_intwin)))) H.
      Qed.

    End SYSINTERCEPTINTWINDOW.

    Section SYSCHECKPENDINGEVENT.

      Let L: compatlayer (cdata RData) :=
        vmx_check_pending_event gensem thread_vmx_check_pending_event_spec
                                 uctx_set_retval1 gensem uctx_set_retval1_spec
                                 uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysCheckPendingEventBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_check_int_shadow
        Variable bvmx_check_pending_event: block.
        Hypothesis hvmx_check_pending_event1 : Genv.find_symbol ge vmx_check_pending_event = Some bvmx_check_pending_event.
        Hypothesis hvmx_check_pending_event2 : Genv.find_funct_ptr ge bvmx_check_pending_event =
                                     let arg_type := Tnil in
                                     let ret_type := tuint in
                                     let cal_conv := cc_default in
                                     let prim := vmx_check_pending_event in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_set_retval1
        Variable buctx_set_retval1: block.
        Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
        Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
                                        Some (External (EF_external uctx_set_retval1
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_check_pending_event_body_correct: m d env le,
            env = PTree.empty _
            trap_check_pending_event_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_check_pending_event_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst;
          functional inversion H3; subst;
          rewrite <- Int.unsigned_repr in H1 at 1;
            try omega;
            unfold sys_check_pending_event_body;
            esplit;
            repeat vcgen.
        Qed.

      End SysCheckPendingEventBody.

      Theorem sys_check_pending_event_code_correct:
        spec_le
          (sys_check_pending_event trap_check_pending_event_spec_low)
          (sys_check_pending_event f_sys_check_pending_event L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_check_pending_event_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_check_pending_event)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_check_pending_event)))) H.
      Qed.

    End SYSCHECKPENDINGEVENT.


    Section SYSCHECKINTSHADOW.

      Let L: compatlayer (cdata RData) :=
        uctx_set_retval1 gensem uctx_set_retval1_spec
                           vmx_check_int_shadow gensem thread_vmx_check_int_shadow_spec
                           uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SysCheckIntShadowBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_check_int_shadow
        Variable bvmx_check_int_shadow: block.
        Hypothesis hvmx_check_int_shadow1 : Genv.find_symbol ge vmx_check_int_shadow = Some bvmx_check_int_shadow.
        Hypothesis hvmx_check_int_shadow2 : Genv.find_funct_ptr ge bvmx_check_int_shadow =
                                     let arg_type := Tnil in
                                     let ret_type := tuint in
                                     let cal_conv := cc_default in
                                     let prim := vmx_check_int_shadow in
                                     Some (External (EF_external
                                                       prim
                                                       (signature_of_type arg_type ret_type cal_conv))
                                                    arg_type ret_type cal_conv).

uctx_set_retval1
        Variable buctx_set_retval1: block.
        Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
        Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
                                        Some (External (EF_external uctx_set_retval1
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_errno
        Variable buctx_set_errno: block.
        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
                                      Some (External (EF_external uctx_set_errno
                                                                  (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                     (Tcons tint Tnil) Tvoid cc_default).

        Lemma sys_check_int_shadow_body_correct: m d env le,
            env = PTree.empty _
            trap_check_int_shadow_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_check_int_shadow_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; subst;
          functional inversion H3; subst;
          rewrite <- Int.unsigned_repr in H1 at 1;
            try omega;
            unfold sys_check_int_shadow_body;
            esplit;
            repeat vcgen.
        Qed.

      End SysCheckIntShadowBody.

      Theorem sys_check_int_shadow_code_correct:
        spec_le
          (sys_check_int_shadow trap_check_int_shadow_spec_low)
          (sys_check_int_shadow f_sys_check_int_shadow L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_check_int_shadow_body_correct
             s (Genv.globalenv p) makeglobalenv
             b1 Hb1fs Hb1fp
             b0 Hb0fs Hb0fp
             b2 Hb2fs Hb2fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_check_int_shadow)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_check_int_shadow)))) H.
      Qed.

    End SYSCHECKINTSHADOW.




  End WithPrimitives.

End TTRAPARGCODE.