Library mcertikos.mcslock.MMCSLockAbsIntroCodeMCSWaitLock

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
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 CommonTactic.
Require Import TacticsForTesting.

Require Import MMCSLockAbsIntroCSource.
Require Import MMCSLockAbsIntro.
Require Import MCSLockOpGenSpec.

Require Import CalMCSLock.

Require Import AbstractDataType.

Lemma multi_log_double_update:
   d ml1 ml2,
    (d {multi_log: ml1}) {multi_log: ml2} = d {multi_log: ml2}.
Proof.
  intros.
  unfold update_multi_log; simpl.
  reflexivity.
Qed.

Lemma ikern_remain :
   d ml, ikern d = ikern (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.

Lemma ihost_remain:
   d ml, ihost d = ihost (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.

Lemma oracle_remain:
   d ml,
    multi_oracle d = multi_oracle (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.

Lemma lock_AT_start_val: lock_AT_start = 0%Z.
Proof. reflexivity. Qed.

Lemma ID_AT_range_val: ID_AT_range = 1%Z.
Proof. unfold ID_AT_range; reflexivity. Qed.

Lemma lock_TCB_start_val : lock_TCB_start = 1%Z.
Proof. unfold lock_TCB_start; reflexivity. Qed.

Lemma num_chan_val: num_chan = num_chan.
Proof. reflexivity. Qed.

Lemma ID_TCB_range_val: ID_TCB_range = num_chan.
Proof. unfold ID_TCB_range; reflexivity. Qed.

Lemma lock_TCB_range_val: lock_TCB_range = (num_chan + 1)%Z.
Proof. unfold lock_TCB_range; simpl; reflexivity. Qed.

Lemma lock_SC_start_val: lock_SC_start = (num_chan + 1)%Z.
Proof. unfold lock_SC_start. rewrite lock_TCB_range_val. reflexivity. Qed.

Lemma lock_range_val: lock_range = (num_chan + num_chan + 1)%Z.
Proof.
  unfold lock_range; simpl; reflexivity.
Qed.

Lemma t_struct_mcs_lock_size:
  sizeof t_struct_mcs_lock = 576%Z.
Proof.
  simpl.
  unfold align; simpl; omega.
Qed.

Lemma t_struct_mcs_node_size:
  sizeof t_struct_mcs_node = 64%Z.
Proof.
  simpl.
  unfold align; simpl; omega.
Qed.

Module MMCSLOCKABSINTROCODEMCSWAITLOCK.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    Context `{mcs_oracle_prop: MCSOracleProp}.

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

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Local Open Scope Z_scope.

    Section MCSWAITLOCK.

      Let L: compatlayer (cdata RData) :=
        get_CPU_ID gensem get_CPU_ID_spec
                  mcs_set_next gensem mcs_set_next_spec
                  mcs_get_busy gensem mcs_get_busy_spec
                  mcs_swap_tail gensem mcs_swap_tail_spec
                  mcs_lock_get_index gensem mcs_lock_get_index_spec.

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

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

      Lemma CalMCS_AcqWait_has_prefix :
         m i l to ,
          CalMCS_AcqWait m i l to = Some
           l´´, = l´´++l.
      Proof.
        clearAll.
        induction m.
        - simpl; intros; inv H.
        - intros.
          Transparent CalMCS_AcqWait.
          simpl in H.
          subdestruct.
          + simpl in H.
            eapply IHm in H.
            destruct H.
             (x ++ TEVENT i (TTICKET (GET_BUSY true)) :: to i l).
            rewrite app_assoc_reverse; simpl.
            assumption.
          + inv H.
             (TEVENT i (TTICKET (GET_BUSY false)) :: to i l); eauto.
      Qed.

      Lemma CalMCS_AcqWait_implies_some_mcs:
         m i l to ,
          CalMCS_AcqWait m i l to = Some
           mlock, CalMCSLock = Some mlock.
      Proof.
        clearAll.
        Transparent CalMCSLock.
        induction m; simpl; intros; [ inv H | ].
        subdestruct.
        - eapply IHm in H.
          eassumption.
        - inv H.
           (MCSLOCK tail lock_array bounds); simpl.
          rewrite Hdestruct; reflexivity.
      Qed.

      Lemma CalMCSLock_prefix_has_CalMCSLock_aux:
         l a mlock,
          l = a::
          CalMCSLock l = Some mlock
           mlock´, CalMCSLock = Some mlock´.
      Proof.
        clearAll.
        intros; inv H; simpl in H0.
        subdestruct; esplit; eauto.
      Qed.

      Lemma CalMCSLock_prefix_has_CalMCSLock:
         l l´´ mlock,
          l = ++ l´´
          CalMCSLock l = Some mlock
           mlock´´, CalMCSLock l´´ = Some mlock´´.
      Proof.
        clearAll.
        induction .
        - intros; rewrite app_nil_l in H; subst.
           mlock; trivial.
        - intros.
          simpl in H.
          destruct l; try (inv H; fail).
          assert (m = a).
          { clearAllExceptOne H.
            inv H; reflexivity. }
          subst.
          edestruct CalMCSLock_prefix_has_CalMCSLock_aux
          with (2:= H0) as (mlock´, H1); eauto.
      Qed.

      Lemma CalMCSLock_fun :
         l mlock mlock´,
          CalMCSLock l = Some mlock
          CalMCSLock l = Some mlock´
          mlock = mlock´.
      Proof.
        clearAll.
        destruct l.
        - intros; simpl in ×.
          inv H; inv H0; reflexivity.
        - intros.
          simpl in H; simpl in H0; subdestruct; try (inv H; inv H0; auto; fail).
      Qed.

    Fixpoint CalMCS_AcqWaitPre (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
      match n with
        | OSome l
        | S
          let := (to i l) ++ l in
          match CalMCSLock with
            | Some (MCSLOCK _ la _) ⇒
              match ZMap.get i la with
                | (false, _)Some ((TEVENT i (TTICKET (GET_BUSY false))) :: )
                | _
                  CalMCS_AcqWaitPre i ((TEVENT i (TTICKET (GET_BUSY true))) ::) to
              end
            | _None
          end
      end.

      Lemma CalMCS_AcqWaitStops:
         m i l to ,
          CalMCS_AcqWait m i l to = Some
           k,
            (k m)%nat
            ( n,
                (0 n < k)%natCalMCS_AcqWait n i l to = None)
            CalMCS_AcqWait k i l to = Some
             j, (k j)%natCalMCS_AcqWaitPre j i l to = Some .
      Proof.
        clearAll.
        Transparent CalMCS_AcqWaitPre CalMCS_AcqWait.
        induction m; simpl; intros; [inv H | ].
        subdestruct.
        - eapply IHm in H; eauto.
          destruct H as (x & H & H0 & H1).
           (S x); split; [omega | split].
          + intros.
            assert(n0case: n = O n O) by omega.
            Caseeq n0case; intros.
            × subst; reflexivity.
            × eapply NPeano.Nat.succ_pred in H3.
              rewrite <- H3; simpl.
              rewrite Hdestruct, Hdestruct1.
              eapply H0; eauto.
              omega.
          + simpl.
            rewrite Hdestruct, Hdestruct1; split; intros.
            × apply H1.
            × assert (j O) by omega.
              eapply NPeano.Nat.succ_pred in H3.
              rewrite <- H3; simpl.
              rewrite Hdestruct, Hdestruct1.
              destruct H1.
              eapply H4; eauto; omega.
        - subst; inv H.
           1%nat.
          split; [omega | split; intros ].
          + assert(n = O) by omega; subst.
            reflexivity.
          + simpl.
            rewrite Hdestruct, Hdestruct1.
            split; [reflexivity |].
            intros.
            assert (j O) by omega.
            eapply NPeano.Nat.succ_pred in H0.
            rewrite <- H0; simpl.
            rewrite Hdestruct, Hdestruct1.
            reflexivity.
      Qed.

      Lemma CalMCS_AcqWaitToPre:
         m i l to ,
          CalMCS_AcqWait m i l to = Some
          CalMCS_AcqWaitPre m i l to = Some .
      Proof.
        clearAll.
        induction m; simpl; intros; [inv H |].
        simpl; intros.
        subdestruct.
        - apply IHm; eauto.
        - apply H.
      Qed.

      Lemma CalMCS_AcqWaitToPreCons:
         m i l to ,
          CalMCS_AcqWaitPre m i l to = Some
          ( m)%nat
           l´´,
            CalMCS_AcqWaitPre i l to = Some l´´.
      Proof.
        clearAll.
        induction m; simpl; intros.
        - assert( = O) by omega.
          subst; esplit; reflexivity.
        - simpl; intros; subdestruct.
          + assert( = O O) by omega.
            Caseeq H1; intros; subst; simpl.
            esplit; reflexivity.
            eapply NPeano.Nat.succ_pred in H1.
            rewrite <- H1; simpl.
            rewrite Hdestruct, Hdestruct1.
            eapply IHm; eauto; omega.
          + inv H.
            assert( = O O) by omega.
            Caseeq H; intros; subst; simpl.
            esplit; reflexivity.
            eapply NPeano.Nat.succ_pred in H.
            rewrite <- H; simpl.
            rewrite Hdestruct, Hdestruct1.
            esplit; reflexivity.
      Qed.

      Lemma CalMCS_AcqWaitPreInv:
         m i l to ,
          CalMCS_AcqWaitPre (S m) i l to = Some
          ( j, (j < (S m))%natCalMCS_AcqWait j i l to = None) →
           l´´,
            CalMCS_AcqWaitPre m i l to = Some l´´
            CalMCS_AcqWaitPre 1 i l´´ to = Some .
      Proof.
        clearAll.
        induction m; simpl; intros.
        - subdestruct.
          + inv H; esplit.
            split; try reflexivity.
            rewrite Hdestruct, Hdestruct1.
            reflexivity.
          + inv H; esplit.
            split; try reflexivity.
            rewrite Hdestruct, Hdestruct1.
            reflexivity.
        - simpl in *; intros; subdestruct.
          + eapply IHm.
            × rewrite Hdestruct3, Hdestruct5.
              apply H.
            × intros.
              assert ((S j < S (S m))%nat) by omega.
              eapply H0 in H2.
              simpl in H2.
              rewrite Hdestruct, Hdestruct1 in H2.
              apply H2.
          + inv H.
            eapply IHm.
            rewrite Hdestruct3, Hdestruct5.
            × reflexivity.
            × intros.
              assert ((S j < S (S m))%nat) by omega.
              eapply H0 in H1.
              simpl in H1.
              rewrite Hdestruct, Hdestruct1 in H1.
              apply H1.
          + inv H.
            assert ((1 < S (S m))%nat) by omega.
            eapply H0 in H.
            simpl in H.
            rewrite Hdestruct, Hdestruct1 in H.
            inv H.
      Qed.

      Lemma CalMCS_AcqWaitPreNeq:
         m i l to mlock mcstail mcsnp mcsbounds bs nt,
          CalMCS_AcqWait m i l to = None
          CalMCS_AcqWaitPre m i l to = Some
          (m > 0)%nat
          CalMCSLock = Some mlock
          mlock = MCSLOCK mcstail mcsnp mcsbounds
          ZMap.get i mcsnp = (bs, nt)
          bs = true.
      Proof.
        clearAll.
        induction m.
        - simpl; intros; omega.
        - simpl; intros.
          subdestruct.
          subst.
          assert (m = O (m > O)%nat) by omega.
          Caseeq H3; intros.
          × subst.
            inv H0.
            simpl in H2.
            subdestruct.
            inv H2; inv Hdestruct.
            rewrite Hdestruct1 in H4; inv H4.
            reflexivity.
          × eapply IHm; eauto.
      Qed.

      Lemma CalMCS_AcqWaitEq:
         m i l to mlock mcstail mcsnp mcsbounds bs nt,
          CalMCS_AcqWait m i l to = Some
          CalMCSLock = Some mlock
          mlock = MCSLOCK mcstail mcsnp mcsbounds
          ZMap.get i mcsnp = (bs, nt)
          bs = false.
      Proof.
        clearAll.
        induction m.
        - simpl; intros.
          inv H.
        - simpl; intros.
          subdestruct; subst.
          × eapply IHm; eauto.
          × inv H.
            simpl in H0.
            subdestruct.
            inv H0; inv Hdestruct.
            rewrite Hdestruct1 in H2; inv H2.
            reflexivity.
      Qed.


      Section MCSWAITLOCKBODY.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

get_CPU_ID
        Variable bget_CPU_ID: block.

        Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.

        Hypothesis hget_CPU_ID2 :
          Genv.find_funct_ptr ge bget_CPU_ID =
          Some (External (EF_external get_CPU_ID
                                      (signature_of_type Tnil tuint cc_default))
                         Tnil tuint cc_default).

mcs_set_next
        Variable bmcs_set_next: block.

        Hypothesis hmcs_set_next1 : Genv.find_symbol ge mcs_set_next = Some bmcs_set_next.

        Hypothesis hmcs_set_next2 :
          Genv.find_funct_ptr ge bmcs_set_next =
          Some (External (EF_external mcs_set_next
                                      (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default))
                         (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

mcs_get_busy
        Variable bmcs_get_busy: block.

        Hypothesis hmcs_get_busy1 : Genv.find_symbol ge mcs_get_busy = Some bmcs_get_busy.
        Hypothesis hmcs_get_busy2 :
          Genv.find_funct_ptr ge bmcs_get_busy =
          Some (External (EF_external mcs_get_busy
                                      (signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
                         (Tcons tint (Tcons tint Tnil)) tuint cc_default).

mcs_swap_tail
        Variable bmcs_swap_tail: block.

        Hypothesis hmcs_swap_tail1 : Genv.find_symbol ge mcs_swap_tail = Some bmcs_swap_tail.

        Hypothesis hmcs_swap_tail2 :
          Genv.find_funct_ptr ge bmcs_swap_tail =
          Some (External (EF_external mcs_swap_tail
                                      (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tuint cc_default))
                         (Tcons tint (Tcons tint (Tcons tint Tnil))) tuint cc_default).

mcs_lock_get_index
        Variable bmcs_lock_get_index: block.

        Hypothesis hmcs_lock_get_index1 : Genv.find_symbol ge mcs_lock_get_index = Some bmcs_lock_get_index.

        Hypothesis hmcs_lock_get_index2 :
            Genv.find_funct_ptr ge bmcs_lock_get_index =
            Some (External (EF_external mcs_lock_get_index
                                        (signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
                           (Tcons tint (Tcons tint Tnil)) tuint cc_default).


        Section mcs_wait_lock_loop_proof.

          Variable minit: memb.
          Variable adt: RData.
          Variable bnd : nat.           Variable K: nat.           Variable cal_time : nat.           Variable l : MultiLog.           Variable l1: MultiLog.
          Variable lock_index : Z.           Variable current_busy : Z.           Variable tail : Z.

          Hypothesis iihost: ihost adt = true.
          Hypothesis iikern: ikern adt = true.
          Hypothesis cpuid_range : 0 (CPU_ID adt) < TOTAL_CPU.
          Hypothesis lock_index_range : 0 lock_index < lock_range.

          Hypothesis Krange: (0 < K < cal_time)%nat.

          Hypothesis initlist: (ZMap.get lock_index (multi_log adt)) = MultiDef l.

          Notation pre_log := (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY true))
                                       :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
                                       (TEVENT (CPU_ID adt) (TTICKET (SET_NEXT tail))
                                               :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
                                               (TEVENT (CPU_ID adt) (TTICKET (SWAP_TAIL bnd false))
                                                       :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
                                               TEVENT (CPU_ID adt) (TTICKET (SWAP_TAIL bnd false))
                                               :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
                                       TEVENT (CPU_ID adt) (TTICKET (SET_NEXT tail))
                                       :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
                                       (TEVENT (CPU_ID adt) (TTICKET (SWAP_TAIL bnd false))
                                               :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
                                       TEVENT (CPU_ID adt) (TTICKET (SWAP_TAIL bnd false)) ::
                                       ZMap.get lock_index (multi_oracle adt)
                                       (CPU_ID adt) l ++ l).

          Definition Calculate_MCSWaitLock (i: nat) :=
            match CalMCS_AcqWaitPre i (CPU_ID adt) pre_log (ZMap.get lock_index (multi_oracle adt)) with
            | Some
              Some (adt {multi_log : ZMap.set lock_index (MultiDef ) (multi_log adt)})
            | _None
            end.

          Definition get_current_busy (d: RData) :=
            match ZMap.get lock_index (multi_log d) with
            | MultiDef l
              match CalMCSLock l with
              | Some (MCSLOCK _ cur_np _) ⇒
                match ZMap.get (CPU_ID adt) cur_np with
                  (cur_bs, cur_nt)
                  if cur_bs then Some 1 else Some 0
                end
              | _None
              end
            | _None
            end.

          Hypothesis init_current_busy:
            current_busy = 1.

          Hypothesis CalcWait:
            CalMCS_AcqWait (pred cal_time) (CPU_ID adt) pre_log
                           (ZMap.get lock_index (multi_oracle adt)) = Some l1.

          Hypothesis Kpre: n,
              (0 n < K)%nat
              CalMCS_AcqWait n (CPU_ID adt) pre_log
                             (ZMap.get lock_index (multi_oracle adt)) = None.

          Hypothesis Klast: CalMCS_AcqWait K (CPU_ID adt) pre_log
                                            (ZMap.get lock_index (multi_oracle adt)) = Some l1.

          Hypothesis Klastpre: j,
              (K j)%nat
              CalMCS_AcqWaitPre j (CPU_ID adt) pre_log
                                (ZMap.get lock_index (multi_oracle adt)) = Some l1.

          Hypothesis busy_at_while_begin:
            get_current_busy (adt {multi_log : ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}) = Some 1.

          Definition wait_lock_loop_body_P (le: temp_env) (m : mem): Prop :=
            le ! _lock_index = Some (Vint (Int.repr lock_index))
            le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt)))
            le ! _current_busy = Some (Vint (Int.repr current_busy))
            le ! _busy_var = Some (Vint (Int.repr 1))
            (get_current_busy adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)})
            = Some current_busy
            m = (minit, adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).

          Definition wait_lock_loop_body_Q (le: temp_env) (m : mem): Prop :=
             d new_busy,
              le ! _lock_index = Some (Vint (Int.repr lock_index))
              le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt)))
              le ! _current_busy = Some (Vint (Int.repr (new_busy)))
              le ! _busy_var = Some (Vint (Int.repr 1))
              (get_current_busy d) = Some new_busy
              new_busy = 0
              Calculate_MCSWaitLock (pred cal_time) = Some d
              m = (minit, d).

          Lemma wait_lock_loop_correct_aux:
            LoopProofSimpleWhile.t
              f_mcs_wait_lock_while_condition
              f_mcs_wait_lock_while_body
              ge (PTree.empty _)
              wait_lock_loop_body_P
              wait_lock_loop_body_Q.
          Proof.
            generalize max_unsigned_val; intro muval.
            apply LoopProofSimpleWhile.make with
            (W := Z)
              (lt := fun z1 z2 ⇒ (0 z2 z1 < z2)%Z)
              (I := fun le m w
                       i new_busy ,
                        le ! _lock_index = Some (Vint (Int.repr lock_index))
                        le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt)))
                        le ! _current_busy = Some (Vint (Int.repr (new_busy)))
                        le ! _busy_var = Some (Vint (Int.repr 1))
                        get_current_busy = Some new_busy
                        (( i = O new_busy = 1
                            = adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)})
                         (((0 < i < K)%nat new_busy = 1 i = K new_busy = 0)
                          Calculate_MCSWaitLock i = Some ))
                        w = Z.of_nat K - Z.of_nat i
                        m = (minit, )
              ).
            - apply Zwf_well_founded.

            - intros le m Hp.
              destruct Hp as (Hle1 & Hle2 & Hle3 & Hle4 & Hc_busy & Hm).
               (Z.of_nat K), O, 1.
               (adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
              rewrite init_current_busy in Hle3.
              repeat vcgen.
              + rewrite <- Nat2Z.inj_sub.
                rewrite NPeano.Nat.sub_0_r.
                reflexivity.
                omega.

            - intros le m n Hp.
              destruct Hp as (cur_index & new_busy & new_d &
                              Hle1 & Hle2 & Hle3 & Hle4 & Hc_busy & Hcond & Hw & Hm).

              Caseeq Hcond.
              +
                intros (ival & new & nd); subst.
                unfold get_current_busy in Hc_busy; simpl in Hc_busy.
                subdestruct.
                inversion Hc_busy; subst.
                esplit; esplit.
                repeat vcgen; try (subst; repeat vcgen; fail); subst.
                assert (tmp: bs_flag, mcs,
                           CalMCSLock
                             (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY bs_flag))
                                     :: ZMap.get lock_index (multi_oracle adt)
                                     (CPU_ID adt) pre_log ++ pre_log) = Some mcs).
                { assert (kneq0: K O) by omega.
                  apply NPeano.Nat.succ_pred in kneq0.
                  rewrite <- kneq0 in Klast.
                  simpl in Klast.
                  intros.
                  case_eq bs_flag; intros;
                  subdestruct; esplit; rewrite Hdestruct1; reflexivity. }
                
                destruct tmp with (bs_flag := true) as (mcs_t´, tmp_t).
                destruct tmp with (bs_flag := false) as (mcs_f´, tmp_f).
                assert (mcs_t´ = mcs_f´).
                { simpl in tmp_t.
                  simpl in tmp_f.
                  subdestruct.
                  inv tmp_t; inv tmp_f; reflexivity. }
                subst.
                rename mcs_f´ into mcs´.
                assert (tmp´: CalMCSLock
                                (ZMap.get lock_index (multi_oracle adt)
                                          (CPU_ID adt) pre_log ++ pre_log) = Some mcs´).
                { simpl in tmp_f; subdestruct; try (inv tmp_f; fail).
                  assumption. }
                destruct mcs´.
                assert (tmp_val: tmp_busy tmp_next, ZMap.get (CPU_ID adt) lock_array0 = (tmp_busy, tmp_next)).
                { set (cur_flags:= ZMap.get (CPU_ID adt) lock_array0).
                  destruct cur_flags.
                   b, z0; reflexivity. }
                destruct tmp_val as (tmp_busy, (tmp_next, tmp_val)).
                destruct tmp_busy.
                {
                  esplit; esplit; repeat vcgen.
                  { unfold mcs_get_busy_spec; subst.
                    rewrite <- ikern_remain.
                    rewrite <- ihost_remain.
                    rewrite iikern, iihost.
                    rewrite zle_lt_true; try eauto.
                    rewrite zle_lt_true; try eauto.
                    simpl; rewrite ZMap.gss.
                    rewrite tmp´.
                    instantiate (1:= (Int.repr (BooltoZ true))).
                    rewrite Int.unsigned_repr; [ | unfold BooltoZ; simpl; omega ].
                    rewrite tmp_val.
                    unfold BooltoZ; simpl.
                    reflexivity. }
                  { rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega. }
                  {
                     (Z.of_nat K - 1).
                    repeat vcgen.
                     1%nat.
                    esplit.
                    rewrite multi_log_double_update.
                     (adt {multi_log
                                 : ZMap.set lock_index
                                            (MultiDef
                                               (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY true))
                                                       :: ZMap.get lock_index (multi_oracle adt)
                                                       (CPU_ID adt) pre_log ++ pre_log))
                                            (ZMap.set lock_index (MultiDef pre_log) (multi_log adt))}).
                    repeat vcgen.
                    - unfold get_current_busy.
                      simpl.
                      rewrite ZMap.gss.
                      simpl.
                      rewrite tmp´.
                      rewrite tmp_val.
                      auto.
                    - right.
                      assert (Kcase: (1 = K 1 < K)%nat) by omega.
                      Caseeq Kcase; intros.
                      +
                        rewrite <- H0.
                        rewrite <- H0 in Klast.
                        simpl in Klast.
                        rewrite tmp´ in Klast.
                        rewrite tmp_val in Klast.
                        inv Klast.
                      +
                        split.
                        × left.
                          split; try omega.
                          unfold BooltoZ; auto.
                        × unfold Calculate_MCSWaitLock; simpl.
                          rewrite tmp´.
                          rewrite tmp_val.
                          rewrite ZMap.set2.
                          reflexivity. } }
                {
                  esplit; esplit; repeat vcgen.
                  { unfold mcs_get_busy_spec; subst.
                    rewrite <- ikern_remain.
                    rewrite <- ihost_remain.
                    rewrite iikern, iihost.
                    rewrite zle_lt_true; try eauto.
                    rewrite zle_lt_true; try eauto.
                    simpl; rewrite ZMap.gss.
                    rewrite tmp´.
                    instantiate (1:= (Int.repr (BooltoZ false))).
                    rewrite Int.unsigned_repr; [ | unfold BooltoZ; simpl; omega ].
                    rewrite tmp_val.
                    unfold BooltoZ; simpl.
                    reflexivity. }
                  { rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega. }
                  {
                     (Z.of_nat K - 1).
                    repeat vcgen.
                     1%nat.
                    esplit.
                    rewrite multi_log_double_update.
                     (adt {multi_log
                                 : ZMap.set lock_index
                                            (MultiDef
                                               (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY false))
                                                       :: ZMap.get lock_index (multi_oracle adt)
                                                       (CPU_ID adt) pre_log ++ pre_log))
                                            (ZMap.set lock_index (MultiDef pre_log) (multi_log adt))}).
                    repeat vcgen.
                    - unfold get_current_busy.
                      simpl.
                      rewrite ZMap.gss.
                      simpl.
                      rewrite tmp´.
                      rewrite tmp_val.
                      auto.
                    - right.
                      assert (Kcase: (1 = K 1 < K)%nat) by omega.
                      Caseeq Kcase; intros.
                      +
                        split.
                        × right.
                          auto.
                        × unfold Calculate_MCSWaitLock; simpl.
                          rewrite tmp´.
                          rewrite tmp_val.
                          rewrite ZMap.set2.
                          reflexivity.
                      +
                        assert ((0 1 < K)%nat) by omega.
                        apply Kpre in H1.
                        simpl in H1.
                        rewrite tmp´ in H1.
                        rewrite tmp_val in H1.
                        inv H1. } }

              + intro tmp; destruct tmp as [icond Hcalc].
                Caseeq icond.

                ×
                  intros (irange & neq).
                  unfold Calculate_MCSWaitLock in Hcalc.
                  subdestruct.
                  inv Hcalc.

                  assert (tmp: bs_flag, mlock,
                               CalMCSLock
                                 (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY bs_flag))::
                                         (ZMap.get lock_index (multi_oracle adt))
                                         (CPU_ID adt) m0 ++ m0) = Some mlock).
                  { eapply CalMCS_AcqWaitToPre in Klast.
                    assert ((S cur_index K)%nat) by omega.
                    eapply CalMCS_AcqWaitToPreCons in Klast; eauto.
                    destruct Klast.
                    eapply CalMCS_AcqWaitPreInv in H0; eauto.
                    intros.
                    - destruct H0.
                      destruct H0.
                      rewrite Hdestruct in H0.
                      inv H0.
                      simpl in H1.
                      subdestruct; rewrite Hdestruct0; esplit; reflexivity.
                    - intros.
                      eapply Kpre; eauto.
                      omega. }

                  destruct tmp with (bs_flag := true) as (mcs_t´, tmp_t).
                  destruct tmp with (bs_flag := false) as (mcs_f´, tmp_f).
                  assert (mcs_t´ = mcs_f´).
                  { simpl in tmp_t.
                    simpl in tmp_f.
                    subdestruct.
                    inv tmp_t; inv tmp_f; reflexivity. }
                  subst.
                  rename mcs_f´ into mcs´.
                  assert (tmp´: CalMCSLock
                                  (ZMap.get lock_index (multi_oracle adt)
                                            (CPU_ID adt) m0 ++ m0) = Some mcs´).
                  { simpl in tmp_f; subdestruct; try (inv tmp_f; fail).
                    assumption. }
                  destruct mcs´.
                  assert (tmp_val: tmp_busy tmp_next, ZMap.get (CPU_ID adt) lock_array = (tmp_busy, tmp_next)).
                  { set (cur_flags:= ZMap.get (CPU_ID adt) lock_array).
                    destruct cur_flags.
                     b, z; reflexivity. }
                  destruct tmp_val as (tmp_busy, (tmp_next, tmp_val)).
                  destruct tmp_busy.
                  {
                    esplit; esplit; repeat vcgen.
                    { esplit; esplit.
                      repeat vcgen.
                      - unfold mcs_get_busy_spec.
                        rewrite <- ikern_remain.
                        rewrite <- ihost_remain.
                        rewrite iikern, iihost.
                        rewrite zle_lt_true; try omega.
                        rewrite zle_lt_true; try omega.
                        simpl; rewrite ZMap.gss.
                        rewrite tmp´.
                        instantiate (1:= (Int.repr 1)).
                        rewrite tmp_val.
                        rewrite multi_log_double_update.
                        rewrite Int.unsigned_repr; try omega.
                        reflexivity.
                      - rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega.
                      -
                         (Z.of_nat K - Z.of_nat cur_index - 1).
                        repeat vcgen.
                        esplit; esplit;
                         (adt {multi_log
                                     : ZMap.set lock_index
                                                (MultiDef
                                                   (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY true))
                                                           :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) m0 ++
                                                           m0)) (multi_log adt)});
                        repeat vcgen.
                        + unfold get_current_busy.
                          simpl.
                          rewrite ZMap.gss.
                          rewrite tmp_t.
                          rewrite tmp_val.
                          auto.
                        + instantiate (1:= (S cur_index)).
                          right.
                          split.
                          × assert (icase: (S cur_index = K S cur_index < K)%nat) by omega.
                            Caseeq icase; intros.
                            { right; split; auto.
                              assert((K K)%nat) by omega.
                              eapply Klastpre in H1.
                              rewrite <- H0 in H1.
                              assert (CalMCSLock l1 = Some (MCSLOCK tail0 lock_array bounds)).
                              { eapply CalMCS_AcqWaitPreInv in H1; eauto.
                                - destruct H1.
                                  destruct H1.
                                  rewrite Hdestruct in H1.
                                  inv H1.
                                  simpl in H2.
                                  subdestruct.
                                  + inv H2.
                                    simpl.
                                    rewrite Hdestruct0.
                                    eauto.
                                  + inv H2.
                                    simpl.
                                    rewrite Hdestruct0.
                                    eauto.
                                - intros.
                                  eapply Kpre; eauto.
                                  omega. }
                              eapply CalMCS_AcqWaitEq in Klast; eauto.
                              inv Klast. }
                            { left.
                              split; try omega. }
                          × unfold Calculate_MCSWaitLock.
                            eapply CalMCS_AcqWaitToPre in Klast; eauto.
                            assert ((S cur_index K)%nat) by omega.
                            eapply CalMCS_AcqWaitToPreCons in Klast; eauto.
                            destruct Klast.
                            rewrite H1.
                            eapply CalMCS_AcqWaitPreInv in H1; eauto.
                            { destruct H1; destruct H1.
                              rewrite Hdestruct in H1.
                              inv H1.
                              simpl in H2.
                              subdestruct.
                              - inv H2.
                                reflexivity.
                              - inv tmp´.
                                rewrite tmp_val in Hdestruct2.
                                inv Hdestruct2. }
                            { intros.
                              eapply Kpre; eauto.
                              omega. }
                        + rewrite Nat2Z.inj_succ.
                          unfold Z.succ.
                          omega.
                        + rewrite ZMap.set2.
                          reflexivity. } }
                  {
                    esplit; esplit; repeat vcgen.
                    { esplit; esplit.
                      repeat vcgen.
                      - unfold mcs_get_busy_spec.
                        rewrite <- ikern_remain.
                        rewrite <- ihost_remain.
                        rewrite iikern, iihost.
                        rewrite zle_lt_true; try omega.
                        rewrite zle_lt_true; try omega.
                        simpl; rewrite ZMap.gss.
                        rewrite tmp´.
                        instantiate (1:= (Int.repr 0)).
                        rewrite tmp_val.
                        rewrite multi_log_double_update.
                        rewrite Int.unsigned_repr; try omega.
                        reflexivity.
                      - rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega.
                      -
                         (Z.of_nat K - Z.of_nat cur_index - 1).
                        repeat vcgen.
                        esplit; esplit;
                         (adt {multi_log
                                     : ZMap.set lock_index
                                                (MultiDef
                                                   (TEVENT (CPU_ID adt) (TTICKET (GET_BUSY false))
                                                           :: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) m0 ++
                                                           m0)) (multi_log adt)});
                        repeat vcgen.
                        + unfold get_current_busy.
                          simpl.
                          rewrite ZMap.gss.
                          rewrite tmp_f.
                          rewrite tmp_val.
                          auto.
                        + instantiate (1:= (S cur_index)).
                          right.
                          split.
                          × assert (icase: (S cur_index = K S cur_index < K)%nat) by omega.
                            Caseeq icase; intros.
                            { right; split; auto. }
                            { left.
                              split; try omega.
                              assert ((0 S cur_index < K)%nat) by omega.
                              eapply Kpre in H1.
                              eapply CalMCS_AcqWaitToPre in Klast; eauto.
                              assert ((S cur_index K)%nat) by omega.
                              eapply CalMCS_AcqWaitToPreCons in Klast; eauto.
                              destruct Klast.
                              assert (CalMCSLock x = Some (MCSLOCK tail0 lock_array bounds)).
                              { eapply CalMCS_AcqWaitPreInv in H3; eauto.
                                - destruct H3.
                                  destruct H3.
                                  rewrite Hdestruct in H3.
                                  inv H3.
                                  simpl in H4.
                                  subdestruct.
                                  + inv H4.
                                    simpl.
                                    rewrite Hdestruct0.
                                    eauto.
                                  + inv H4.
                                    simpl.
                                    rewrite Hdestruct0.
                                    eauto.
                                - intros.
                                  eapply Kpre; eauto.
                                  omega. }
                              eapply CalMCS_AcqWaitPreNeq in H1; try eauto.
                              - inv H1.
                              - omega. }
                          × unfold Calculate_MCSWaitLock.
                            eapply CalMCS_AcqWaitToPre in Klast; eauto.
                            assert ((S cur_index K)%nat) by omega.
                            eapply CalMCS_AcqWaitToPreCons in Klast; eauto.
                            destruct Klast.
                            rewrite H1.
                            eapply CalMCS_AcqWaitPreInv in H1; eauto.
                            { destruct H1; destruct H1.
                              rewrite Hdestruct in H1.
                              inv H1.
                              simpl in H2.
                              subdestruct.
                              - inv tmp´.
                                rewrite tmp_val in Hdestruct2.
                                inv Hdestruct2.
                              - inv H2.
                                reflexivity. }
                            { intros.
                              eapply Kpre; eauto.
                              omega. }
                        + rewrite Nat2Z.inj_succ.
                          unfold Z.succ.
                          omega.
                        + rewrite ZMap.set2.
                          reflexivity. } }
                ×
                  intros.
                  destruct H as (ci_val & cn_val).
                  esplit; esplit; repeat vcgen.
                  { unfold wait_lock_loop_body_Q.
                     new_d.
                    esplit.
                    repeat vcgen.
                    assert ((S K cal_time)%nat) by omega.
                    assert ((K (pred cal_time))%nat) by omega.
                    unfold Calculate_MCSWaitLock in ×.
                    assert ((K K)%nat) by omega.
                    erewrite Klastpre in Hcalc; eauto; try omega.
                    erewrite Klastpre; eauto. }
          Qed.

        End mcs_wait_lock_loop_proof.

        Lemma mcs_wait_lock_body_correct:
           m d env le bound index ofs,
            env = PTree.empty _
            PTree.get _bound le = Some (Vint bound) →
            PTree.get _lock_id le = Some (Vint index) →
            PTree.get _offset le = Some (Vint ofs) →
            kernel_mode d
            high_level_invariant d
            mcs_wait_lock_spec (Int.unsigned bound) (Int.unsigned index) (Int.unsigned ofs) d = Some
             le´,
              exec_stmt ge env le ((m, d): mem) f_mcs_wait_lock_body E0 le´ (m, ) (Out_return None).
        Proof.
          intros.
          generalize max_unsigned_val; intros muval.
          generalize lock_AT_start_val; intros lat_val.
          generalize ID_AT_range_val; intros iar_val.
          generalize lock_TCB_start_val; intros lts_val.
          generalize ID_TCB_range_val; intros itr_val.
          generalize num_chan_val; intros nc_val.
          generalize lock_TCB_range_val; intros ltr_val.
          generalize lock_SC_start_val; intros lss_val.
          generalize lock_range_val; intros lr_val.

          generalize t_struct_mcs_lock_size; intros t_st_ml_size.
          generalize t_struct_mcs_node_size; intros t_st_mn_size.

          unfold f_mcs_wait_lock_body; subst.

          unfold mcs_wait_lock_spec in H5.
          destruct H3 as (H3a & H3b).
          rewrite H3a, H3b in H5.
          remember (index2Z (Int.unsigned index) (Int.unsigned ofs)) as lock_index.
          destruct lock_index; try (inv H5; fail).

          Opaque Z.add Z.mul.
          assert (lock_index_range: 0 z < lock_range).
          { clearAllExceptTwo Heqlock_index lock_range_val.
            assert (lock_id_val: (Int.unsigned index) = ID_AT
                                 (Int.unsigned index) = ID_TCB
                                 (Int.unsigned index) = ID_SC).
            { unfold index2Z in Heqlock_index.
              unfold index_range in ×.
              destruct (Int.unsigned index); try tauto; try (inversion Heqlock_index; fail).
              destruct p; try tauto; try (inversion Heqlock_index; fail).
              destruct p; try tauto; try (inversion Heqlock_index). }
            destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]];
              rewrite lock_id_val in Heqlock_index; unfold index2Z in Heqlock_index; simpl in *; subdestruct;
              inv Heqlock_index; rewrite lock_range_val.
            - unfold ID_AT_range in *; omega.
            - unfold ID_TCB_range, ID_AT_range in *; omega.
            - unfold lock_TCB_range, ID_SC_range, ID_AT_range, ID_TCB_range in *; omega. }
          symmetry in Heqlock_index.

          assert (cid_range: 0 (CPU_ID d) < TOTAL_CPU).
          { inv H4; omega. }

          Transparent Z.add Z.mul.
          Opaque CalMCSLock CalMCS_RelWait CalWaitLockTime.

          subdestruct.

          -
            esplit; repeat vcgen.
            {
              unfold mcs_lock_get_index_spec.
              instantiate (1:= Int.repr z).
              rewrite Int.unsigned_repr; try omega.
              rewrite H3a, H3b, Heqlock_index.
              reflexivity. }
            {
              unfold get_CPU_ID_spec.
              instantiate (1:= Int.repr (CPU_ID d)).
              rewrite Int.unsigned_repr; try omega.
              rewrite H3a, H3b.
              reflexivity. }
            {
              unfold mcs_swap_tail_spec.
              rewrite H3a, H3b.
              rewrite Int.unsigned_repr; try omega.
              rewrite zle_lt_true; try omega.
              rewrite Int.unsigned_repr; try omega.
              rewrite zle_lt_true; try omega.
              rewrite Hdestruct.
              rewrite Hdestruct0.
              instantiate (1:= NULL).
              rewrite e; unfold NULL.
              rewrite Int.unsigned_repr; try omega.
              reflexivity. }
            { unfold NULL; simpl; repeat vcgen. }
            { unfold NULL; omega. }
            { unfold NULL; rewrite muval; omega. }
            { simpl.
              instantiate
                (1:= (PTree.set _prev_id (Vint (Int.repr NULL))
                                (PTree.set _cpuid
                                           (Vint (Int.repr (CPU_ID d)))
                                           (PTree.set _lock_index (Vint (Int.repr z))
                                                      le)))).
              inv H5.
              repeat vcgen. }

          -
            assert ((CalWaitLockTime bounds > 0)%nat).
            { assert ((CalWaitLockTime bounds 0)%nat).
              { intro.
                Transparent CalWaitLockTime.
                unfold CalWaitLockTime in H.
                inv H. }
              omega. }
            Opaque CalWaitLockTime.
            rewrite <- NPeano.Nat.succ_pred_pos with (n:= CalWaitLockTime bounds) in Hdestruct3 by omega.
            simpl in Hdestruct3.
            subdestruct; subst.

            +

              
              Transparent CalMCSLock.
              simpl in Hdestruct3.
              generalize Hdestruct3; intro HcalcWait.
              generalize HcalcWait; intro Hcalctmp.
              eapply CalMCS_AcqWaitToPre in HcalcWait; eauto.
              eapply CalMCS_AcqWaitStops in Hdestruct3; eauto.

              inv H5.

              destruct Hdestruct3 as [K [Krange [KPre [KPost KPostPre]]]].
              assert (Kgt0: (0 < K)%nat).
              { assert (K = OFalse).
                intro.
                subst.
                inv KPost.
                omega. }
              
              assert (Krangelt: (0 < K < CalWaitLockTime bounds)%nat) by omega.
              remember 1 as current_busy.

              assert (gc_busy :
                        get_current_busy
                          d z d
                          {multi_log
                           : ZMap.set
                               z (MultiDef
                                    (TEVENT (CPU_ID d) (TTICKET (GET_BUSY true))
                                            :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                            (TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
                                                    :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                                    (TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                            :: ZMap.get z (multi_oracle d)
                                                            (CPU_ID d) l ++ l) ++
                                                    TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                    :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
                                            TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
                                            :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                            (TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                    :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
                                            TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                            :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
                               (multi_log d)} = Some 1).
              { unfold get_current_busy.
                Transparent CalMCSLock.
                simpl.
                rewrite ZMap.gss.
                simpl.
                rewrite Hdestruct4.
                rewrite Hdestruct6.
                reflexivity. }
              Opaque CalMCSLock.

              generalize (wait_lock_loop_correct_aux m _ (nat_of_Z (Int.unsigned bound))
                                                     K (CalWaitLockTime bounds) _ _ z current_busy tail
                                                     H3b H3a
                                                     cid_range
                                                     lock_index_range
                                                     Krangelt Heqcurrent_busy
                                                     Hcalctmp KPre KPost KPostPre gc_busy).
              intros LP.
              eapply LoopProofSimpleWhile.termination
              with (condition := f_mcs_wait_lock_while_condition)
                     (body := f_mcs_wait_lock_while_body)
                     (P := wait_lock_loop_body_P m d (nat_of_Z (Int.unsigned bound)) l z current_busy tail)
                     (Q := wait_lock_loop_body_Q m d (nat_of_Z (Int.unsigned bound)) (CalWaitLockTime bounds) l z tail)
                     (le0 := (PTree.set _current_busy (Vint (Int.repr 1))
                                        (PTree.set _busy_var (Vint (Int.repr 1))
                                                   (PTree.set
                                                      _prev_id (Vint (Int.repr tail))
                                                      (PTree.set _cpuid
                                                                 (Vint (Int.repr (CPU_ID d)))
                                                                 (PTree.set _lock_index (Vint (Int.repr z)) le))))))
                     (m0 :=
                        (m, d {multi_log :
                                 ZMap.set
                                   z (MultiDef
                                        (TEVENT (CPU_ID d) (TTICKET (GET_BUSY true))
                                                :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                                (TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
                                                        :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                                        (TEVENT (CPU_ID d)
                                                                (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                                :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
                                                        TEVENT (CPU_ID d)
                                                        (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                        :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
                                                TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
                                                :: ZMap.get z (multi_oracle d) (CPU_ID d)
                                                (TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                        :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
                                                TEVENT (CPU_ID d) (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned bound)) false))
                                                :: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
                                   (multi_log d)})) in LP.
              destruct LP as (while_le´, (while_m´, (LP1 & LP2))).
              unfold wait_lock_loop_body_Q in LP2.
              destruct LP2 as (while_d´, (while_new´, LP2)).
              ×
                esplit; repeat vcgen.
                {
                  unfold mcs_lock_get_index_spec.
                  instantiate (1:= Int.repr z).
                  rewrite Int.unsigned_repr; try omega.
                  rewrite H3a, H3b, Heqlock_index.
                  reflexivity. }
                {
                  unfold get_CPU_ID_spec.
                  instantiate (1:= Int.repr (CPU_ID d)).
                  rewrite Int.unsigned_repr; try omega.
                  rewrite H3a, H3b.
                  reflexivity. }
                {
                  unfold mcs_swap_tail_spec.
                  rewrite H3a, H3b.
                  rewrite Int.unsigned_repr; try omega.
                  rewrite zle_lt_true; try omega.
                  rewrite Int.unsigned_repr; try omega.
                  rewrite zle_lt_true; try omega.
                  rewrite Hdestruct.
                  rewrite Hdestruct0.
                  assert (0 tail < TOTAL_CPU).
                  { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                    clearAll; intros.
                    inv H4.
                    unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                    eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                    unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                    unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                    eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                    unfold valid_MCS_log in Hdestruct.
                    unfold MCSCorrect_range in Hdestruct.
                    eapply Hdestruct in Hdestruct0; eauto.
                    destruct Hdestruct0.
                    unfold NULL in n.
                    omega. }
                  rewrite zle_le_true; try omega.
                  rewrite zeq_false; try omega.
                  instantiate (1:= tail).
                  rewrite Int.unsigned_repr; try omega.
                  reflexivity. }
                { unfold NULL in *; simpl.
                  rewrite Hdestruct2; repeat vcgen. }
                { assert (0 tail < TOTAL_CPU).
                  { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                    clearAll; intros.
                    inv H4.
                    unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                    eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                    unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                    unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                    eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                    unfold valid_MCS_log in Hdestruct.
                    unfold MCSCorrect_range in Hdestruct.
                    eapply Hdestruct in Hdestruct0; eauto.
                    destruct Hdestruct0.
                    unfold NULL in n.
                    omega. }
                  omega. }
                { assert (0 tail < TOTAL_CPU).
                  { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                    clearAll; intros.
                    inv H4.
                    unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                    eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                    unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                    unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                    eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                    unfold valid_MCS_log in Hdestruct.
                    unfold MCSCorrect_range in Hdestruct.
                    eapply Hdestruct in Hdestruct0; eauto.
                    destruct Hdestruct0.
                    unfold NULL in n.
                    omega. }
                  omega. }
                { simpl.
                  change E0 with (E0 ** E0).
                  assert (0 tail < TOTAL_CPU).
                  { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                    clearAll; intros.
                    inv H4.
                    unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                    eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                    unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                    unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                    eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                    unfold valid_MCS_log in Hdestruct.
                    unfold MCSCorrect_range in Hdestruct.
                    eapply Hdestruct in Hdestruct0; eauto.
                    destruct Hdestruct0.
                    unfold NULL in n.
                    omega. }
                  econstructor; [repeat vcgen | ].
                  change E0 with (E0 ** E0).
                  econstructor.
                  -
                    repeat vcgen.
                    unfold mcs_set_next_spec.
                    rewrite <- ikern_remain.
                    rewrite <- ihost_remain.
                    rewrite H3a, H3b.
                    rewrite zle_lt_true; try omega.
                    rewrite zle_lt_true; try omega.
                    rewrite zle_lt_true; try omega.
                    simpl.
                    eapply CalMCSLock_prefix_has_CalMCSLock in Hdestruct4; eauto.
                    destruct Hdestruct4.
                    eapply CalMCSLock_prefix_has_CalMCSLock_aux in H5; eauto.
                    destruct H5.
                    rewrite ZMap.gss.
                    rewrite H5.
                    rewrite multi_log_double_update.
                    simpl; reflexivity.
                  - change E0 with (E0 ** E0).
                    econstructor.
                    +
                      repeat vcgen.
                      unfold mcs_get_busy_spec.
                      rewrite <- ikern_remain.
                      rewrite <- ihost_remain.
                      rewrite H3a, H3b.
                      rewrite zle_lt_true; try omega.
                      rewrite zle_lt_true; try omega.
                      simpl.
                      rewrite ZMap.gss.
                      rewrite multi_log_double_update.
                      rewrite ZMap.set2.
                      rewrite ZMap.set2.
                      Transparent CalMCSLock.
                      simpl in Hdestruct4.
                      rewrite Hdestruct4.
                      rewrite Hdestruct6.
                      instantiate (1:= Int.repr 1).
                      rewrite Int.unsigned_repr; try omega.
                      repeat vcgen.
                    + change E0 with (E0 ** E0).
                      econstructor; [ | repeat vcgen].
                      destruct LP2 as (LP21 & LP22 & LP23 & LP24 & LP25 & LP26 & LP27 & LP28).
                      inv LP28.
                      unfold Calculate_MCSWaitLock in LP27.
                      subdestruct; try (inv LP27; fail).
                      inv LP27.
                      instantiate (1:= while_le´).
                      unfold exec_stmt in LP1.
                      inv HcalcWait.
                      exact LP1. }
              × unfold wait_lock_loop_body_P; subst.
                split; [repeat vcgen | ].
                split; [repeat vcgen | ].
                split; [repeat vcgen | ].
                split; [repeat vcgen | ].
                split; auto.

            +
              simpl; subst.
              inv Hdestruct3; inv H5; subst.
              esplit; repeat vcgen.
              {
                unfold mcs_lock_get_index_spec.
                instantiate (1:= Int.repr z).
                rewrite Int.unsigned_repr; try omega.
                rewrite H3a, H3b, Heqlock_index.
                reflexivity. }
              {
                unfold get_CPU_ID_spec.
                instantiate (1:= Int.repr (CPU_ID d)).
                rewrite Int.unsigned_repr; try omega.
                rewrite H3a, H3b.
                reflexivity. }
              {
                unfold mcs_swap_tail_spec.
                rewrite H3a, H3b.
                rewrite Int.unsigned_repr; try omega.
                rewrite zle_lt_true; try omega.
                rewrite Int.unsigned_repr; try omega.
                rewrite zle_lt_true; try omega.
                rewrite Hdestruct.
                rewrite Hdestruct0.
                assert (0 tail < TOTAL_CPU).
                { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                  clearAll; intros.
                  inv H4.
                  unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                  eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                  unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                  unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                  eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                  unfold valid_MCS_log in Hdestruct.
                  unfold MCSCorrect_range in Hdestruct.
                  eapply Hdestruct in Hdestruct0; eauto.
                  destruct Hdestruct0.
                  unfold NULL in n.
                  omega. }
                rewrite zle_le_true; try omega.
                rewrite zeq_false; try omega.
                instantiate (1:= tail).
                rewrite Int.unsigned_repr; try omega.
                reflexivity. }
              { unfold NULL in *; simpl.
                rewrite Hdestruct2; repeat vcgen. }
              { assert (0 tail < TOTAL_CPU).
                { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                  clearAll; intros.
                  inv H4.
                  unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                  eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                  unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                  unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                  eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                  unfold valid_MCS_log in Hdestruct.
                  unfold MCSCorrect_range in Hdestruct.
                  eapply Hdestruct in Hdestruct0; eauto.
                  destruct Hdestruct0.
                  unfold NULL in n.
                  omega. }
                omega. }
              { assert (0 tail < TOTAL_CPU).
                { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                  clearAll; intros.
                  inv H4.
                  unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                  eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                  unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                  unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                  eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                  unfold valid_MCS_log in Hdestruct.
                  unfold MCSCorrect_range in Hdestruct.
                  eapply Hdestruct in Hdestruct0; eauto.
                  destruct Hdestruct0.
                  unfold NULL in n.
                  omega. }
                omega. }
              { simpl.
                change E0 with (E0 ** E0).
                assert (0 tail < TOTAL_CPU).
                { generalize Hdestruct Hdestruct0 n H4 lock_index_range.
                  clearAll; intros.
                  inv H4.
                  unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
                  eapply valid_multi_log_pool_mcs_inv in Hdestruct; eauto.
                  unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
                  unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
                  eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in Hdestruct; eauto.
                  unfold valid_MCS_log in Hdestruct.
                  unfold MCSCorrect_range in Hdestruct.
                  eapply Hdestruct in Hdestruct0; eauto.
                  destruct Hdestruct0.
                  unfold NULL in n.
                  omega. }
                econstructor; [repeat vcgen | ].
                change E0 with (E0 ** E0).
                econstructor.
                -
                  repeat vcgen.
                  unfold mcs_set_next_spec.
                  rewrite <- ikern_remain.
                  rewrite <- ihost_remain.
                  rewrite H3a, H3b.
                  rewrite zle_lt_true; try omega.
                  rewrite zle_lt_true; try omega.
                  rewrite zle_lt_true; try omega.
                  simpl.
                  rewrite ZMap.gss.
                  eapply CalMCSLock_prefix_has_CalMCSLock in Hdestruct4; eauto.
                  destruct Hdestruct4.
                  eapply CalMCSLock_prefix_has_CalMCSLock_aux in H5; eauto.
                  destruct H5.
                  rewrite H5.
                  rewrite multi_log_double_update.
                  simpl; reflexivity.
                - change E0 with (E0 ** E0).
                  econstructor.
                  +
                    repeat vcgen.
                    unfold mcs_get_busy_spec.
                    rewrite <- ikern_remain.
                    rewrite <- ihost_remain.
                    rewrite H3a, H3b.
                    rewrite zle_lt_true; try omega.
                    rewrite zle_lt_true; try omega.
                    simpl.
                    rewrite ZMap.gss.
                    rewrite Hdestruct4.
                    rewrite Hdestruct6.
                    rewrite multi_log_double_update.
                    rewrite ZMap.set2.
                    rewrite ZMap.set2.
                    instantiate (1:= Int.repr 0).
                    rewrite Int.unsigned_repr; try omega.
                    reflexivity.
                  + change E0 with (E0 ** E0).
                    econstructor; [ | repeat vcgen].
                    unfold set_opttemp.
                    unfold f_mcs_wait_lock_while_condition, f_mcs_wait_lock_while_body.
                    instantiate (1:= (PTree.set _current_busy (Vint (Int.repr 0))
                                                (PTree.set _busy_var (Vint (Int.repr 1))
                                                           (PTree.set
                                                              _prev_id (Vint (Int.repr tail))
                                                              (PTree.set _cpuid
                                                                         (Vint (Int.repr (CPU_ID d)))
                                                                         (PTree.set _lock_index (Vint (Int.repr z)) le)))))).
                    eapply ClightBigstep.exec_Sloop_stop1.
                    eapply exec_Sseq_2.
                    repeat vcgen.
                    { intros contra.
                      inv contra. }
                    { econstructor. } }
        Qed.

      End MCSWAITLOCKBODY.

      Theorem mcs_wait_lock_code_correct:
        spec_le (wait_lock mcs_wait_lock_spec_low) (wait_lock f_mcs_wait_lock L).
      Proof.
        set ( := L) in ×.
        unfold L in ×.
        fbigstep_pre .
        fbigstep (mcs_wait_lock_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_mcs_wait_lock)
                                                                    (Vint bound::Vint i::Vint ofs::nil)
                                                                    (create_undef_temps (fn_temps f_mcs_wait_lock)))) muval.
      Qed.

    End MCSWAITLOCK.

  End WithPrimitives.

End MMCSLOCKABSINTROCODEMCSWAITLOCK.