Library mcertikos.proc.PQueueIntroCode

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 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 TacticsForTesting.
Require Import CommonTactic.

Require Import CalRealProcModule.

Require Import AbstractDataType.

Require Import PQueueIntro.
Require Import PQueueIntroCSource.
Require Import QueueInitGenSpec.

Module PQUEUEINTROCODE.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.
    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 ENQUEUE.

      Let L: compatlayer (cdata RData) := set_prev gensem set_prev_spec
            set_next gensem set_next_spec
            get_tail gensem get_tail_spec
            set_head gensem set_head_spec
            set_tail gensem set_tail_spec.

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

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

      Section EnqueueBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

set_prev

        Variable bset_prev: block.

        Hypothesis hset_prev1 : Genv.find_symbol ge set_prev = Some bset_prev.

        Hypothesis hset_prev2 : Genv.find_funct_ptr ge bset_prev
                                = Some (External (EF_external set_prev
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

set_next

        Variable bset_next: block.

        Hypothesis hset_next1 : Genv.find_symbol ge set_next = Some bset_next.

        Hypothesis hset_next2 : Genv.find_funct_ptr ge bset_next
                                = Some (External (EF_external set_next
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

get_tail

        Variable bget_tail: block.

        Hypothesis hget_tail1 : Genv.find_symbol ge get_tail = Some bget_tail.

        Hypothesis hget_tail2 : Genv.find_funct_ptr ge bget_tail
                                = Some (External (EF_external get_tail
                                                              (signature_of_type (Tcons tint Tnil) tint cc_default))
                                                 (Tcons tint Tnil) tint cc_default).

set_head

        Variable bset_head: block.

        Hypothesis hset_head1 : Genv.find_symbol ge set_head = Some bset_head.

        Hypothesis hset_head2 : Genv.find_funct_ptr ge bset_head
                                = Some (External (EF_external set_head
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

set_tail

        Variable bset_tail: block.

        Hypothesis hset_tail1 : Genv.find_symbol ge set_tail = Some bset_tail.

        Hypothesis hset_tail2 : Genv.find_funct_ptr ge bset_tail
                                = Some (External (EF_external set_tail
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

        Lemma enqueue_body_correct: m d env le chan_index proc_index,
                                      env = PTree.empty _
                                      PTree.get tchan_index le = Some (Vint chan_index) →
                                      PTree.get tproc_index le = Some (Vint proc_index) →
                                      PTree.get ttail le = Some Vundef
                                      enqueue_spec (Int.unsigned chan_index) (Int.unsigned proc_index) d = Some
                                       le´,
                                        exec_stmt ge env le ((m, d): mem) enqueue_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold enqueue_spec in H3.
          case_eq (ikern d); intros iikern; rewrite iikern in H3; try (inv H3; fail).
          case_eq (pg d); intros ipg; rewrite ipg in H3; try (inv H3; fail).
          case_eq (ihost d); intros iihost; rewrite iihost in H3; try (inv H3; fail).
          case_eq (ipt d); intros iipt; rewrite iipt in H3; try (inv H3; fail).
          case_eq (Queue_arg (Int.unsigned chan_index) (Int.unsigned proc_index));
            intros qargs; rewrite qargs in H3; try (inv H3; fail).
          unfold Queue_arg in qargs.
          destruct (zle_le 0 (Int.unsigned chan_index) num_chan) in qargs; try (inv qargs; auto; fail).
          destruct (zle_lt 0 (Int.unsigned proc_index) num_proc) in qargs; try (inv qargs; auto; fail).
          unfold enqueue_body; subst.
          subdestruct; subst.
          -
            esplit; repeat vcgen.
            + unfold get_tail_spec.
              rewrite iikern, iihost, ipg, iipt, Hdestruct0.
              rewrite zle_lt_true.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + repeat vcgen.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold set_prev_spec; simpl.
                rewrite iikern, iihost, ipg, iipt.
                rewrite zle_lt_true.
                rewrite Hdestruct2.
                reflexivity.
                omega.
              × unfold set_next_spec; simpl.
                rewrite iikern, iihost, ipg, iipt.
                rewrite zle_lt_true.
                rewrite ZMap.gss.
                reflexivity.
                omega.
              × unfold set_head_spec; simpl.
                rewrite iikern, iihost, ipg, iipt, Hdestruct0.
                rewrite zle_lt_true.
                reflexivity.
                omega.
              × unfold set_tail_spec; simpl.
                rewrite iikern, iihost, ipg, iipt.
                rewrite zle_lt_true.
                rewrite ZMap.gss.
                repeat rewrite ZMap.set2.
                repeat zdestruct.
                omega.
          -
            assert(tcase: Int.unsigned proc_index = tail Int.unsigned proc_index tail)
              by omega.
            Caseeq tcase.
            +
              intro tmp; rewrite tmp in ×.
              esplit; repeat vcgen.
              × unfold get_tail_spec.
                rewrite iikern, iihost, ipg, iipt.
                rewrite zle_lt_true.
                rewrite Int.unsigned_repr.
                rewrite Hdestruct0.
                reflexivity.
                omega.
                omega.
              × repeat vcgen.
              × omega.
              × omega.
              × repeat vcgen.
                { unfold set_next_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true by omega.
                  rewrite zle_le_true by omega.
                  rewrite Hdestruct3.
                  reflexivity. }
                { unfold set_prev_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true by omega.
                  rewrite zle_le_true by omega.
                  rewrite tmp.
                  rewrite ZMap.gss.
                  reflexivity. }
                { unfold set_next_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true by omega.
                  rewrite tmp.
                  rewrite ZMap.set2.
                  rewrite ZMap.gss.
                  reflexivity. }
                { unfold set_tail_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true.
                  rewrite Hdestruct0.
                  repeat rewrite ZMap.set2.
                  rewrite tmp.
                  rewrite Hdestruct4 in Hdestruct3.
                  injection Hdestruct3.
                  intros; subst.
                  rewrite ZMap.set2 in H3.
                  repeat zdestruct.
                  omega. }
            +
              intro.
              esplit; repeat vcgen.
              × unfold get_tail_spec; simpl.
                rewrite iikern, iihost, ipg, iipt.
                rewrite zle_lt_true.
                rewrite Hdestruct0.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
              × repeat vcgen.
              × omega.
              × omega.
              × repeat vcgen.
                { unfold set_next_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true.
                  rewrite zle_le_true.
                  rewrite Hdestruct4.
                  reflexivity.
                  omega.
                  omega. }
                { unfold set_prev_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true.
                  rewrite zle_le_true.
                  rewrite ZMap.gso.
                  rewrite Hdestruct3.
                  reflexivity.
                  assumption.
                  omega.
                  omega. }
                { unfold set_next_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true.
                  rewrite ZMap.gss.
                  reflexivity.
                  omega. }
                { unfold set_tail_spec; simpl.
                  rewrite iikern, iihost, ipg, iipt.
                  rewrite zle_lt_true.
                  rewrite Hdestruct0.
                  simpl.
                  rewrite ZMap.set2.
                  repeat zdestruct.
                  omega. }
          - subdestruct.
          - subdestruct.
            omega.
            omega.
        Qed.

      End EnqueueBody.

      Theorem enqueue_code_correct:
        spec_le (enqueue enqueue_spec_low) (enqueue f_enqueue L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep (enqueue_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 labd´ (PTree.empty _)
                                       (bind_parameter_temps´ (fn_params f_enqueue)
                                                              (Vint n::Vint i::nil)
                                                              (create_undef_temps (fn_temps f_enqueue)))) H0.
      Qed.

    End ENQUEUE.


    Section DEQUEUE.

      Let L: compatlayer (cdata RData) := set_prev gensem set_prev_spec
            get_head gensem get_head_spec
            get_next gensem get_next_spec
            set_head gensem set_head_spec
            set_tail gensem set_tail_spec.

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

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

      Section DequeueBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

set_prev

        Variable bset_prev: block.

        Hypothesis hset_prev1 : Genv.find_symbol ge set_prev = Some bset_prev.

        Hypothesis hset_prev2 : Genv.find_funct_ptr ge bset_prev
                                = Some (External (EF_external set_prev
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

get_head

        Variable bget_head: block.

        Hypothesis hget_head1 : Genv.find_symbol ge get_head = Some bget_head.

        Hypothesis hget_head2 : Genv.find_funct_ptr ge bget_head
                                = Some (External (EF_external get_head
                                                              (signature_of_type (Tcons tint Tnil)
                                                                                 tint cc_default))
                                                 (Tcons tint Tnil) tint cc_default).

get_next

        Variable bget_next: block.

        Hypothesis hget_next1 : Genv.find_symbol ge get_next = Some bget_next.

        Hypothesis hget_next2 : Genv.find_funct_ptr ge bget_next
                                = Some (External (EF_external get_next
                                                              (signature_of_type (Tcons tint Tnil)
                                                                                 tint cc_default))
                                                 (Tcons tint Tnil) tint cc_default).

set_head

        Variable bset_head: block.

        Hypothesis hset_head1 : Genv.find_symbol ge set_head = Some bset_head.

        Hypothesis hset_head2 : Genv.find_funct_ptr ge bset_head
                                = Some (External (EF_external set_head
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

set_tail

        Variable bset_tail: block.

        Hypothesis hset_tail1 : Genv.find_symbol ge set_tail = Some bset_tail.

        Hypothesis hset_tail2 : Genv.find_funct_ptr ge bset_tail
                                = Some (External (EF_external set_tail
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

        Lemma dequeue_body_correct:
           m d env le chan_index proc_index,
            env = PTree.empty _
            PTree.get tchan_index le = Some (Vint chan_index) →
            dequeue_spec (Int.unsigned chan_index) d = Some (, (Int.unsigned proc_index))
            high_level_invariant d
             le´,
              exec_stmt ge env le ((m, d): mem) dequeue_body E0 le´ (m, ) (Out_return (Some (Vint proc_index, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold dequeue_body.
          functional inversion H1; subst.
          -
            
            destruct H2.
            simpl in ×.
            esplit.
            repeat vcgen.
            + unfold get_head_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
            + simpl.
              ptreesolve.
              rewrite H3.
              rewrite Int.repr_unsigned.
              reflexivity.
          -
            esplit.
            repeat vcgen.
            + unfold get_head_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold get_next_spec; simpl.
                rewrite H4, H5, H6, H7, H12.
                rewrite zle_lt_true.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
              × discharge_cmp.
              × omega.
              × omega.
              × repeat vcgen.
                unfold set_tail_spec; simpl.
                rewrite H4, H5, H6, H7.
                rewrite zle_lt_true.
                rewrite ZMap.gss.
                repeat rewrite ZMap.set2.
                repeat zdestruct.
                omega.
            + repeat vcgen.
          -
            assert(nextrange: 0 next num_proc).
            { repeat vcgen. }
            esplit.
            repeat vcgen.
            + unfold get_head_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold get_next_spec; simpl.
                rewrite H4, H5, H6, H7, H12.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                rewrite zle_lt_true.
                reflexivity.
                omega.
                omega.
              × discharge_cmp.
              × omega.
              × omega.
              × repeat vcgen.
                unfold set_head_spec; simpl.
                rewrite H4, H5, H6, H7, H9.
                rewrite zle_lt_true.
                repeat zdestruct.
                omega.
            + repeat vcgen.
        Qed.

      End DequeueBody.

      Theorem dequeue_code_correct:
        spec_le (dequeue dequeue_spec_low) (dequeue f_dequeue L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep (dequeue_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 labd´ (PTree.empty _)
                                       (bind_parameter_temps´ (fn_params f_dequeue)
                                                              (Vint n::nil)
                                                              (create_undef_temps (fn_temps f_dequeue)))) H0.
      Qed.

    End DEQUEUE.


    Section QUEUERMV.

      Let L: compatlayer (cdata RData) := set_prev gensem set_prev_spec
            set_next gensem set_next_spec
            get_prev gensem get_prev_spec
            get_next gensem get_next_spec
            set_head gensem set_head_spec
            set_tail gensem set_tail_spec.

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

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

      Section QueueRmvBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

set_prev

        Variable bset_prev: block.

        Hypothesis hset_prev1 : Genv.find_symbol ge set_prev = Some bset_prev.

        Hypothesis hset_prev2 : Genv.find_funct_ptr ge bset_prev
                                = Some (External (EF_external set_prev
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

set_next

        Variable bset_next: block.

        Hypothesis hset_next1 : Genv.find_symbol ge set_next = Some bset_next.

        Hypothesis hset_next2 : Genv.find_funct_ptr ge bset_next
                                = Some (External (EF_external set_next
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

get_prev

        Variable bget_prev: block.

        Hypothesis hget_prev1 : Genv.find_symbol ge get_prev = Some bget_prev.

        Hypothesis hget_prev2 : Genv.find_funct_ptr ge bget_prev
                                = Some (External (EF_external get_prev
                                                              (signature_of_type (Tcons tint Tnil) tint cc_default))
                                                 (Tcons tint Tnil) tint cc_default).

get_next

        Variable bget_next: block.

        Hypothesis hget_next1 : Genv.find_symbol ge get_next = Some bget_next.

        Hypothesis hget_next2 : Genv.find_funct_ptr ge bget_next
                                = Some (External (EF_external get_next
                                                              (signature_of_type (Tcons tint Tnil) tint cc_default))
                                                 (Tcons tint Tnil) tint cc_default).

set_head

        Variable bset_head: block.

        Hypothesis hset_head1 : Genv.find_symbol ge set_head = Some bset_head.

        Hypothesis hset_head2 : Genv.find_funct_ptr ge bset_head
                                = Some (External (EF_external set_head
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

set_tail

        Variable bset_tail: block.

        Hypothesis hset_tail1 : Genv.find_symbol ge set_tail = Some bset_tail.

        Hypothesis hset_tail2 : Genv.find_funct_ptr ge bset_tail
                                = Some (External (EF_external set_tail
                                                              (signature_of_type (Tcons tint (Tcons tint Tnil))
                                                                                 Tvoid cc_default))
                                                 (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).

        Lemma queue_rmv_body_correct: m d env le chan_index proc_index,
            env = PTree.empty _
            high_level_invariant d
            PTree.get tchan_index le = Some (Vint chan_index) →
            PTree.get tproc_index le = Some (Vint proc_index) →
            queue_rmv_spec (Int.unsigned chan_index) (Int.unsigned proc_index) d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) queue_rmv_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold queue_rmv_body.
          functional inversion H3; functional inversion H8; subst.
          -
            esplit.
            repeat vcgen.
            + unfold get_prev_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + unfold get_next_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold set_tail_spec; simpl.
                rewrite ZMap.gss.
                rewrite ZMap.set2.
                rewrite H4, H5, H6, H7.
                rewrite zle_lt_true.
                repeat zdestruct.
                omega.

          -
            assert(nextrange: 0 next num_proc).
            { omega. }
            esplit.
            repeat vcgen.
            + unfold get_prev_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + unfold get_next_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold set_head_spec; simpl.
                rewrite H4, H5, H6, H7, H10.
                rewrite zle_lt_true.
                repeat zdestruct.
                omega.
          -
            assert(nextrange: 0 prev num_proc) by omega.
            esplit.
            repeat vcgen.
            + unfold get_prev_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + unfold get_next_spec; simpl.
              rewrite H4, H5, H6, H7, H9.
              rewrite zle_lt_true.
              repeat zdestruct.
              rewrite Int.unsigned_repr.
              reflexivity.
              omega.
              omega.
            + discharge_cmp.
            + omega.
            + omega.
            + repeat vcgen.
              × unfold set_tail_spec; simpl.
                rewrite H4, H5, H6, H7, H10.
                rewrite zle_lt_true.
                repeat zdestruct.
                omega.
          -
            assert(prevrange: 0 prev num_proc) by omega.
            assert(nextrange: 0 next num_proc) by omega.
            assert(prevnext: prev = next prev next) by omega.
            Caseeq prevnext.
            +
              intro.
              esplit.
              repeat vcgen.
              × unfold get_prev_spec; simpl.
                rewrite H4, H5, H6, H7, H9.
                rewrite zle_lt_true.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
              × unfold get_next_spec; simpl.
                rewrite H4, H5, H6, H7, H9.
                rewrite zle_lt_true.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
                × discharge_cmp.
                × omega.
                × omega.
                × repeat vcgen.
                  unfold set_prev_spec; simpl.
                  rewrite H4, H5, H6, H7.
                  rewrite zle_lt_true.
                  rewrite zle_le_true.
                  rewrite H16.
                  rewrite H.
                  rewrite ZMap.set2.
                  repeat zdestruct.
                  omega.
                  omega.
            +
              intro.
              esplit.
              repeat vcgen.
              × unfold get_prev_spec; simpl.
                rewrite H4, H5, H6, H7, H9.
                rewrite zle_lt_true.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
              × unfold get_next_spec; simpl.
                rewrite H4, H5, H6, H7, H9.
                rewrite zle_lt_true.
                repeat zdestruct.
                rewrite Int.unsigned_repr.
                reflexivity.
                omega.
                omega.
              × discharge_cmp.
              × omega.
              × omega.
              × repeat vcgen.
                { unfold set_next_spec; simpl.
                   rewrite H4, H5, H6, H7.
                   rewrite H13.
                   rewrite zle_lt_true.
                   rewrite zle_le_true.
                   repeat zdestruct.
                   omega.
                   omega. }
                { unfold set_prev_spec; simpl.
                  rewrite ZMap.gso.
                  rewrite H4, H5, H6, H7.
                  rewrite zle_lt_true.
                  rewrite zle_le_true.
                  rewrite H16.
                  repeat zdestruct.
                  omega.
                  omega.
                  unfold not; intros.
                  elim H; congruence. }
        Qed.

      End QueueRmvBody.

      Theorem queue_rmv_code_correct:
        spec_le (queue_rmv queue_rmv_spec_low) (queue_rmv f_queue_rmv L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep (queue_rmv_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 m´0 labd labd´ (PTree.empty _)
                                         (bind_parameter_temps´ (fn_params f_queue_rmv)
                                                                (Vint n::Vint i::nil)
                                                                (create_undef_temps (fn_temps f_queue_rmv)))) H0.
      Qed.

    End QUEUERMV.

  End WithPrimitives.

End PQUEUEINTROCODE.