Library mcertikos.trap.TTrapArgCode4

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

      Let L: compatlayer (cdata RData) :=
        vmx_get_exit_reason gensem thread_vmx_get_exit_reason_spec
                             vmx_get_exit_io_port gensem thread_vmx_get_exit_io_port_spec
                             vmx_get_io_width gensem thread_vmx_get_io_width_spec
                             vmx_get_io_write gensem thread_vmx_get_io_write_spec
                             vmx_get_exit_io_rep gensem thread_vmx_get_exit_io_rep_spec
                             vmx_get_exit_io_str gensem thread_vmx_get_exit_io_str_spec
                             vmx_get_exit_fault_addr gensem thread_vmx_get_exit_fault_addr_spec
                             vmx_get_exit_qualification gensem thread_vmx_get_exit_qualification_spec
                             uctx_set_retval1 gensem uctx_set_retval1_spec
                             uctx_set_retval2 gensem uctx_set_retval2_spec
                             uctx_set_retval3 gensem uctx_set_retval3_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 SysGetExitinfoBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

vmx_get_exit_reason
        Variable bvmx_get_exit_reason: block.
        Hypothesis hvmx_get_exit_reason1 : Genv.find_symbol ge vmx_get_exit_reason = Some bvmx_get_exit_reason.
        Hypothesis hvmx_get_exit_reason2 : Genv.find_funct_ptr ge bvmx_get_exit_reason =
                                           let arg_type := Tnil in
                                           let ret_type := tuint in
                                           let cal_conv := cc_default in
                                           let prim := vmx_get_exit_reason in
                                           Some (External (EF_external prim
                                                                       (signature_of_type arg_type ret_type cal_conv))
                                                          arg_type ret_type cal_conv).

vmx_get_exit_io_port
        Variable bvmx_get_exit_io_port: block.
        Hypothesis hvmx_get_exit_io_port1 : Genv.find_symbol ge vmx_get_exit_io_port = Some bvmx_get_exit_io_port.
        Hypothesis hvmx_get_exit_io_port2 : Genv.find_funct_ptr ge bvmx_get_exit_io_port =
                                            let arg_type := Tnil in
                                            let ret_type := tuint in
                                            let cal_conv := cc_default in
                                            let prim := vmx_get_exit_io_port in
                                            Some (External (EF_external prim
                                                                        (signature_of_type arg_type ret_type cal_conv))
                                                           arg_type ret_type cal_conv).

vmx_get_io_width
        Variable bvmx_get_io_width: block.
        Hypothesis hvmx_get_io_width1 : Genv.find_symbol ge vmx_get_io_width = Some bvmx_get_io_width.
        Hypothesis hvmx_get_io_width2 : Genv.find_funct_ptr ge bvmx_get_io_width =
                                        let arg_type := Tnil in
                                        let ret_type := tuint in
                                        let cal_conv := cc_default in
                                        let prim := vmx_get_io_width in
                                        Some (External (EF_external prim
                                                                    (signature_of_type arg_type ret_type cal_conv))
                                                       arg_type ret_type cal_conv).

vmx_get_io_write
        Variable bvmx_get_io_write: block.
        Hypothesis hvmx_get_io_write1 : Genv.find_symbol ge vmx_get_io_write = Some bvmx_get_io_write.
        Hypothesis hvmx_get_io_write2 : Genv.find_funct_ptr ge bvmx_get_io_write =
                                        let arg_type := Tnil in
                                        let ret_type := tuint in
                                        let cal_conv := cc_default in
                                        let prim := vmx_get_io_write in
                                        Some (External (EF_external prim
                                                                    (signature_of_type arg_type ret_type cal_conv))
                                                       arg_type ret_type cal_conv).

vmx_get_exit_io_rep
        Variable bvmx_get_exit_io_rep: block.
        Hypothesis hvmx_get_exit_io_rep1 : Genv.find_symbol ge vmx_get_exit_io_rep = Some bvmx_get_exit_io_rep.
        Hypothesis hvmx_get_exit_io_rep2 : Genv.find_funct_ptr ge bvmx_get_exit_io_rep =
                                           let arg_type := Tnil in
                                           let ret_type := tuint in
                                           let cal_conv := cc_default in
                                           let prim := vmx_get_exit_io_rep in
                                           Some (External (EF_external prim
                                                                       (signature_of_type arg_type ret_type cal_conv))
                                                          arg_type ret_type cal_conv).
vmx_get_exit_io_str
        Variable bvmx_get_exit_io_str: block.
        Hypothesis hvmx_get_exit_io_str1 : Genv.find_symbol ge vmx_get_exit_io_str = Some bvmx_get_exit_io_str.
        Hypothesis hvmx_get_exit_io_str2 : Genv.find_funct_ptr ge bvmx_get_exit_io_str =
                                           let arg_type := Tnil in
                                           let ret_type := tuint in
                                           let cal_conv := cc_default in
                                           let prim := vmx_get_exit_io_str in
                                           Some (External (EF_external prim
                                                                       (signature_of_type arg_type ret_type cal_conv))
                                                          arg_type ret_type cal_conv).
vmx_get_exit_fault_addr
        Variable bvmx_get_exit_fault_addr: block.
        Hypothesis hvmx_get_exit_fault_addr1 : Genv.find_symbol ge vmx_get_exit_fault_addr = Some bvmx_get_exit_fault_addr.
        Hypothesis hvmx_get_exit_fault_addr2 : Genv.find_funct_ptr ge bvmx_get_exit_fault_addr =
                                               let arg_type := Tnil in
                                               let ret_type := tuint in
                                               let cal_conv := cc_default in
                                               let prim := vmx_get_exit_fault_addr in
                                               Some (External (EF_external prim
                                                                           (signature_of_type arg_type ret_type cal_conv))
                                                              arg_type ret_type cal_conv).
vmx_get_exit_qualification
        Variable bvmx_get_exit_qualification: block.
        Hypothesis hvmx_get_exit_qualification1 : Genv.find_symbol ge vmx_get_exit_qualification = Some bvmx_get_exit_qualification.
        Hypothesis hvmx_get_exit_qualification2 : Genv.find_funct_ptr ge bvmx_get_exit_qualification =
                                               let arg_type := Tnil in
                                               let ret_type := tuint in
                                               let cal_conv := cc_default in
                                               let prim := vmx_get_exit_qualification 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_retval3
        Variable buctx_set_retval3: block.
        Hypothesis huctx_set_retval31 : Genv.find_symbol ge uctx_set_retval3 = Some buctx_set_retval3.
        Hypothesis huctx_set_retval32 : Genv.find_funct_ptr ge buctx_set_retval3 =
                                        Some (External (EF_external uctx_set_retval3
                                                                    (signature_of_type (Tcons tint Tnil) Tvoid cc_default))
                                                       (Tcons tint Tnil) Tvoid cc_default).

uctx_set_retval4
        Variable buctx_set_retval4: block.
        Hypothesis huctx_set_retval41 : Genv.find_symbol ge uctx_set_retval4 = Some buctx_set_retval4.
        Hypothesis huctx_set_retval42 : Genv.find_funct_ptr ge buctx_set_retval4 =
                                        Some (External (EF_external uctx_set_retval4
                                                                    (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_exitinfo_body_correct: m d env le,
            env = PTree.empty _
            trap_get_exitinfo_spec d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) sys_get_exitinfo_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.

          assert(0 port Int.max_unsigned).
          {
            functional inversion H2.
            functional inversion H13.
            repeat discharge_unsigned_range.
          }

          assert(0 width 3).
          {
            functional inversion H3;
            functional inversion H14;
            intomega.
          }

          assert(0 write 1).
          {
            functional inversion H4;
            functional inversion H15;
            intomega.
          }

          assert(0 rep Int.max_unsigned).
          {
            functional inversion H5; subst.
            functional inversion H16; subst.
            apply Z_land_range.
            split.
            apply Z.shiftr_nonneg.
            discharge_unsigned_range.
            rewrite Z.shiftr_div_pow2.
            change (2 ^ 5) with 32.
            generalize (Int.unsigned_range_2 v); intro.
            xomega.
            omega.
            omega.
          }
          assert(0 str Int.max_unsigned).
          {
            functional inversion H6; subst.
            functional inversion H17; subst.
            apply Z_land_range.
            split.
            apply Z.shiftr_nonneg.
            discharge_unsigned_range.
            rewrite Z.shiftr_div_pow2.
            change (2 ^ 4) with 16.
            generalize (Int.unsigned_range_2 v); intro.
            xomega.
            omega.
            omega.
          }
          assert(0 fault_addr Int.max_unsigned).
          {
            functional inversion H7; subst.
            functional inversion H18; subst.
            repeat discharge_unsigned_range.
          }
          assert(0 addr Int.max_unsigned).
          {
            functional inversion H8; subst.
            functional inversion H19; subst.
            repeat discharge_unsigned_range.
          }
          rewrite <- Int.unsigned_repr in H2 at 1; try omega.
          rewrite <- Int.unsigned_repr in H3 at 1; try omega.
          rewrite <- Int.unsigned_repr in H4 at 1; try omega.
          rewrite <- Int.unsigned_repr in H5 at 1; try omega.
          rewrite <- Int.unsigned_repr in H6 at 1; try omega.
          rewrite <- Int.unsigned_repr in H7 at 1; try omega.
          rewrite <- Int.unsigned_repr in H8 at 1; try omega.
          unfold flags in ×.
          unfold get_flags in H12.
          subdestruct; subst.
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor 0 1) with 1 in H12.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor 0 2) with 2 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor 1 2) with 3 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor 0 4) with 4 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor 1 4) with 5 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor (Z.lor 0 2) 4) with 6 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 30)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            repeat vcgen.
            ptreesolve.
            ptreesolve.
            discharge_cmp.
            discharge_cmp.
            discharge_cmp.
            change (Z.lor (Z.lor 1 2) 4) with 7 in ×.
            rewrite Int.unsigned_repr.
            assumption.
            apply Z_lor_range.
            omega.
            omega.
          }
          {
            assert(0 port Int.max_unsigned).
            {
              functional inversion H2.
              functional inversion H13.
              repeat discharge_unsigned_range.
            }

            assert(0 width 3).
            {
              functional inversion H3;
              functional inversion H14;
              intomega.
            }

            assert(0 write 1).
            {
              functional inversion H4;
              functional inversion H15;
              intomega.
            }

            assert(0 rep Int.max_unsigned).
            {
              functional inversion H5; subst.
              functional inversion H16; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 5) with 32.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 str Int.max_unsigned).
            {
              functional inversion H6; subst.
              functional inversion H17; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 4) with 16.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 fault_addr Int.max_unsigned).
            {
              functional inversion H7; subst.
              functional inversion H18; subst.
              repeat discharge_unsigned_range.
            }
            assert(0 addr Int.max_unsigned).
            {
              functional inversion H8; subst.
              functional inversion H19; subst.
              repeat discharge_unsigned_range.
            }
            rewrite <- Int.unsigned_repr in H2 at 1; try omega.
            rewrite <- Int.unsigned_repr in H3 at 1; try omega.
            rewrite <- Int.unsigned_repr in H4 at 1; try omega.
            rewrite <- Int.unsigned_repr in H5 at 1; try omega.
            rewrite <- Int.unsigned_repr in H6 at 1; try omega.
            rewrite <- Int.unsigned_repr in H7 at 1; try omega.
            rewrite <- Int.unsigned_repr in H8 at 1; try omega.
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 48)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
          }
          {
            assert(0 port Int.max_unsigned).
            {
              functional inversion H2.
              functional inversion H14.
              repeat discharge_unsigned_range.
            }

            assert(0 width 3).
            {
              functional inversion H3;
              functional inversion H15;
              intomega.
            }

            assert(0 write 1).
            {
              functional inversion H4;
              functional inversion H16;
              intomega.
            }

            assert(0 rep Int.max_unsigned).
            {
              functional inversion H5; subst.
              functional inversion H17; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 5) with 32.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 str Int.max_unsigned).
            {
              functional inversion H6; subst.
              functional inversion H18; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 4) with 16.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 fault_addr Int.max_unsigned).
            {
              functional inversion H7; subst.
              functional inversion H19; subst.
              repeat discharge_unsigned_range.
            }
            assert(0 addr Int.max_unsigned).
            {
              functional inversion H8; subst.
              functional inversion H20; subst.
              repeat discharge_unsigned_range.
            }
            rewrite <- Int.unsigned_repr in H2 at 1; try omega.
            rewrite <- Int.unsigned_repr in H3 at 1; try omega.
            rewrite <- Int.unsigned_repr in H4 at 1; try omega.
            rewrite <- Int.unsigned_repr in H5 at 1; try omega.
            rewrite <- Int.unsigned_repr in H6 at 1; try omega.
            rewrite <- Int.unsigned_repr in H7 at 1; try omega.
            rewrite <- Int.unsigned_repr in H8 at 1; try omega.
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            instantiate (1:= (Int.repr 28)).
            rewrite Int.unsigned_repr; try omega.
            reflexivity.
            repeat vcgen.
            repeat vcgen.
          }
          {
            assert(0 reason Int.max_unsigned).
            {
              functional inversion H1; subst.
              functional inversion H13; subst.
              apply Z_land_range.
              repeat discharge_unsigned_range.
              omega.
            }
            assert(0 port Int.max_unsigned).
            {
              functional inversion H2.
              functional inversion H14.
              repeat discharge_unsigned_range.
            }

            assert(0 width Int.max_unsigned).
            {
              functional inversion H3;
              functional inversion H15;
              intomega.
            }

            assert(0 write Int.max_unsigned).
            {
              functional inversion H4;
              functional inversion H16;
              intomega.
            }

            assert(0 rep Int.max_unsigned).
            {
              functional inversion H5; subst.
              functional inversion H17; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 5) with 32.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 str Int.max_unsigned).
            {
              functional inversion H6; subst.
              functional inversion H18; subst.
              apply Z_land_range.
              split.
              apply Z.shiftr_nonneg.
              discharge_unsigned_range.
              rewrite Z.shiftr_div_pow2.
              change (2 ^ 4) with 16.
              generalize (Int.unsigned_range_2 v); intro.
              xomega.
              omega.
              omega.
            }
            assert(0 fault_addr Int.max_unsigned).
            {
              functional inversion H7; subst.
              functional inversion H19; subst.
              repeat discharge_unsigned_range.
            }
            assert(0 addr Int.max_unsigned).
            {
              functional inversion H8; subst.
              functional inversion H20; subst.
              repeat discharge_unsigned_range.
            }
            rewrite <- Int.unsigned_repr in H1 at 1; try omega.
            rewrite <- Int.unsigned_repr in H2 at 1; try omega.
            rewrite <- Int.unsigned_repr in H3 at 1; try omega.
            rewrite <- Int.unsigned_repr in H4 at 1; try omega.
            rewrite <- Int.unsigned_repr in H5 at 1; try omega.
            rewrite <- Int.unsigned_repr in H6 at 1; try omega.
            rewrite <- Int.unsigned_repr in H7 at 1; try omega.
            rewrite <- Int.unsigned_repr in H8 at 1; try omega.
            unfold sys_get_exitinfo_body.
            esplit.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            d3 vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
          }
        Qed.

      End SysGetExitinfoBody.

      Theorem sys_get_exitinfo_body_code_correct:
        spec_le
          (sys_get_exitinfo trap_get_exitinfo_spec_low)
          (sys_get_exitinfo f_sys_get_exitinfo L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (sys_get_exitinfo_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             b4 Hb4fs Hb4fp
             b5 Hb5fs Hb5fp
             b6 Hb6fs Hb6fp
             b7 Hb7fs Hb7fp
             b8 Hb8fs Hb8fp
             b9 Hb9fs Hb9fp
             b10 Hb10fs Hb10fp
             b11 Hb11fs Hb11fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_sys_get_exitinfo)
                                    nil
                                    (create_undef_temps (fn_temps f_sys_get_exitinfo)))) H.
      Qed.

    End SYSGETEXITINFO.

  End WithPrimitives.

End TTRAPARGCODE.