Library mcertikos.objects.ObjThread

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalTicketLock.
Require Import ObjQLock.
Require Import ObjCV.
Require Import DeviceStateDataType.
Require Export ObjInterruptDriver.

Section OBJ_Thread.

  Context `{real_params: RealParams}.
  Context `{waittime: WaitTime}.

  Function sleeper_inc_spec (adt: RData) :=
    match (ikern adt, ihost adt) with
    | (true, true) ⇒
      let cpu := CPU_ID adt in
      let n := ZMap.get cpu (sleeper (adt)) + 1 in
      if zlt_lt 0 n num_proc then
        Some adt {sleeper: ZMap.set cpu n (sleeper (adt))}
      else
        None
    | _ ⇒ None
    end.

  Function sleeper_dec_spec (adt: RData) :=
    match (ikern adt, ihost adt) with
    | (true, true) ⇒
      let cpu := CPU_ID adt in
      let n := ZMap.get cpu (sleeper (adt)) - 1 in
      if zle_lt 0 n (num_proc - 1) then
        Some adt {sleeper: ZMap.set cpu n (sleeper (adt))}
      else None
    | _ ⇒ None
    end.

  Function sleeper_zzz_spec (adt: RData) :=
    match (ikern adt, ihost adt) with
    | (true, true) ⇒
      let cpu := CPU_ID adt in
      let n := ZMap.get cpu (sleeper (adt)) in
      if zeq n 0 then Some 1
      else Some 0
    | _ ⇒ None
    end.

  Definition kctxt_ra_spec (adt: RData) (n: Z) (b: block) (ofs: int) : option RData :=
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zlt_lt 0 n num_proc then
          let rs := (ZMap.get n (kctxt adt))#RA <- (Vptr b ofs) in
          Some adt {kctxt: ZMap.set n rs (kctxt adt)}
        else None
      | _ ⇒ None
    end.

  Definition kctxt_sp_spec (adt: RData) (n: Z) (b: block) (ofs: int) : option RData :=
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zlt_lt 0 n num_proc then
          let rs := (ZMap.get n (kctxt adt))#SP <- (Vptr b ofs) in
          Some adt {kctxt: ZMap.set n rs (kctxt adt)}
        else None
      | _ ⇒ None
    end.

  Function kctxt_switch_spec (adt: RData) (n n´: Z) (rs: KContext) : option (RData × KContext) :=
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zle_lt 0 n num_proc then
          if zle_lt 0 n´ num_proc then
            if zeq n n´ then None
            else
              Some (adt {kctxt: ZMap.set n rs (kctxt adt)}
                    , ZMap.get n´ (kctxt adt))
          else None
        else None
      | _ ⇒ None
    end.

  Definition kctxt_new_spec (adt: RData) (b: block) (b´:block) (ofs´: int) id q: option (RData × Z) :=
    let c := ZMap.get id (AC adt) in
    let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
    match (pg adt, ikern adt, ihost adt, ipt adt, cused c, cused (ZMap.get i (AC adt)), zlt_lt 0 i num_proc,
           zlt (Z_of_nat (length (cchildren c))) max_children,
           zle_le 0 q (cquota c - cusage c)) with
      | (true, true, true, true, true, false, left _, left _, left _) ⇒
        let child := mkContainer q 0 id nil true in
        let parent := (mkContainer (cquota c) (cusage c + q)
                                   (cparent c) (i :: cchildren c) (cused c)) in
        let ofs := Int.repr ((i + 1) × PgSize -4) in
        let rs := ((ZMap.get i (kctxt adt)) # SP <- (Vptr b ofs)) # RA <- (Vptr b´ ofs´) in
        Some (adt {AC: ZMap.set i child (ZMap.set id parent (AC adt))}
                  {kctxt: ZMap.set i rs (kctxt adt)}, i)
      | _ ⇒ None
    end.

  Function get_abtcb_CPU_ID_spec (n:Z) (adt: RData) : option Z :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
    | (true, true, true, true) ⇒
      if zle_lt 0 n num_proc then
        match ZMap.get n (abtcb adt) with
        | AbTCBValid _ c _ ⇒
          Some (c)
        | _ ⇒ None
        end
      else None
    | _ ⇒ None
    end.

  Function set_abtcb_CPU_ID_spec (n s: Z) (adt: RData) : option RData :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
    | (true, true, true, true) ⇒
      if zle_lt 0 n num_proc then
        if zle_le 0 s num_proc then
          match (ZMap.get n (abtcb adt)) with
          | AbTCBValid ts _ b ⇒
            Some adt {abtcb: ZMap.set n (AbTCBValid ts s b) (abtcb adt)}
          | _ ⇒ None
          end
        else None
      else None
    | _ ⇒ None
    end.

  Function get_state0_spec (n:Z) (adt: RData): option Z :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zle_lt 0 n num_proc then
          match ZMap.get n (abtcb adt) with
            | AbTCBValid s _ _ ⇒
              Some (ThreadStatetoZ s)
            | _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.

  Function set_state0_spec (n s: Z) (adt: RData): option RData :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zle_lt 0 n num_proc then
          match (ZMap.get n (abtcb adt), ZtoThreadState s) with
            | (AbTCBValid _ c b, Some i) ⇒
              Some adt {abtcb: ZMap.set n (AbTCBValid i c b) (abtcb adt)}
            | _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.

  Function set_state1_spec (n s: Z) (adt: RData) : option RData :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zle_lt 0 n num_proc then
          match ZMap.get n (abtcb adt), ZtoThreadState s with
            | AbTCBValid _ c b, Some i ⇒
              if ThreadState_dec i RUN then None
              else
                Some adt {abtcb: ZMap.set n (AbTCBValid i c b) (abtcb adt)}
            | _, _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.

  Function enqueue0_spec (n i: Z) (adt: RData): option RData :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if Queue_arg n i then
          match (ZMap.get n (abq adt), cused (ZMap.get i (AC adt))) with
            | (AbQValid l, true) ⇒
              match (ZMap.get i (abtcb adt)) with
                | AbTCBValid st c b ⇒
                  if zeq b (-1) then
                    Some adt {abtcb: ZMap.set i (AbTCBValid st c n) (abtcb adt)}
                         {abq: ZMap.set n (AbQValid (l ++ (i::nil))) (abq adt)}
                  else None
                | _ ⇒ None
              end
            | _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.

  Function enqueue_atomic_spec (n i: Z) (adt: RData): option RData :=
    match acquire_lock_ABTCB_spec n adt with
      | Some adt0 ⇒
        match enqueue0_spec n i adt0 with
          | Some adt1 ⇒
            release_lock_ABTCB_spec n adt1
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function dequeue0_spec (n: Z) (adt: RData): option (RData × Z) :=
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        if zle_lt 0 n num_chan then
          match (ZMap.get n (abq adt)) with
            | AbQValid ll ⇒
              match ll with
                | nil ⇒ Some (adt, num_proc)
                | la :: l ⇒
                  match (ZMap.get la (abtcb adt)) with
                    | AbTCBValid st c _ ⇒
                      Some (adt {abtcb: ZMap.set la (AbTCBValid st c (-1)) (abtcb adt)}
                                {abq: ZMap.set n (AbQValid l) (abq adt)}, la)
                    | _ ⇒ None
                  end
              end
            | _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.

  Function dequeue_atomic_spec (n: Z) (adt: RData) :=
    match acquire_lock_ABTCB_spec n adt with
      | Some adt0 ⇒
        match dequeue0_spec n adt0 with
          | Some (adt1, i) ⇒
            match release_lock_ABTCB_spec n adt1 with
              | Some adt´ ⇒ Some (adt´, i)
              | _ ⇒ None
            end
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function tdqueue_init0_spec (mbi_adr:Z) (adt: RData): option RData :=
    match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
      | (false, false, true, true, true, false) ⇒
        let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
        if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
          if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
            Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
                 {lapic: (mkLApicData
                            (mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
                                          (32 + 7) true true true 0 50 false 0))
                           {l1: l1 (lapic adt)}
                           {l2: l2 (lapic adt)}
                           {l3: l3 (lapic adt)}
                 } {ioapic / s / CurrentIrq: None}
                 {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
                 {AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
                 {multi_log: real_multi_log (multi_log adt)}
                 {lock: real_lock (lock adt)}
                 {idpde: real_idpde (idpde adt)}
                 {smspool: real_smspool (smspool adt)}
             {abtcb: real_abtcb (abtcb adt)}
             {abq: real_abq (abq adt)}
          else None
        else None
      | _ ⇒ None
    end.

  Definition thread_spawn_spec (adt: RData) (b: block) (b´:block) (ofs´: int) id q : option (RData× Z) :=
    let cpu := CPU_ID adt in
    let c := ZMap.get id (AC adt) in
    let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
    let cc := ZMap.get i (AC adt) in
    match (pg adt, ikern adt, ihost adt, ipt adt,cused c, cused cc, zlt_lt 0 i num_proc,
           zlt (Z_of_nat (length (cchildren c))) max_children,
           zle_le 0 q (cquota c - cusage c),
          ZMap.get i (abtcb adt)) with
      | (true, true, true, true, true, false, left _, left _, left _, AbTCBValid _ _ (-1)) ⇒
        let child := mkContainer q 0 id nil true in
        let parent := (mkContainer (cquota c) (cusage c + q)
                                   (cparent c) (i :: cchildren c) (cused c)) in
        let rdyq := rdy_q_id cpu in
        match (ZMap.get rdyq (abq adt)) with
          | AbQValid l ⇒
            let ofs := Int.repr ((i + 1) × PgSize -4) in
            let rs := ((ZMap.get i (kctxt adt))#SP <- (Vptr b ofs))#RA <- (Vptr b´ ofs´) in
            Some (adt {AC: ZMap.set i child (ZMap.set id parent (AC adt))}
                      {kctxt: ZMap.set i rs (kctxt adt)}
                      {abtcb: ZMap.set i (AbTCBValid READY cpu rdyq) (abtcb adt)}
                      {abq: ZMap.set rdyq (AbQValid (l ++ (i::nil))) (abq adt)}, i)
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function thread_wakeup_spec (cv: Z) (adt: RData) :=
    let me := CPU_ID adt in
    match (ikern adt, pg adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        let n := slp_q_id cv 0 in
        if zle_lt 0 cv num_cv then
          match dequeue_atomic_spec n adt with
            | Some (adt0, la) ⇒
              if zle_lt 0 la num_proc then
                match ZMap.get la (abtcb adt0), cused (ZMap.get la (AC adt0)) with
                  | AbTCBValid s cpu _, true ⇒
                    if zeq me cpu then
                      let rdyq := rdy_q_id cpu in
                      match ZMap.get rdyq (abq adt0) with
                        | AbQValid l´ ⇒
                          Some (adt0 {abtcb: ZMap.set la (AbTCBValid READY cpu rdyq) (abtcb adt0)}
                                     {abq: ZMap.set rdyq (AbQValid (l´ ++ (la :: nil))) (abq adt0)}, 1)
                        | _ ⇒ None
                      end
                    else if zle_lt 0 cpu TOTAL_CPU then
                      let msgq := msg_q_id cpu in
                      match enqueue_atomic_spec msgq la adt0 with
                        | Some adt´ ⇒ Some (adt´, 1)
                        | _ ⇒ None
                      end
                         else None
                  | _, _ ⇒ None
                end
              else if zle_le 0 la Int.max_unsigned then Some (adt0, 0) else None
            | _ ⇒ None
          end
        else None
      | _ ⇒ None
    end.


  Function thread_sched_spec (adt: RData) (rs: KContext) : option (RData×KContext) :=
    let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        let cpu := CPU_ID adt in
        let rdyq := rdy_q_id cpu in
        match ZMap.get rdyq (abq adt) with
          | AbQValid (la :: l) ⇒
            match ZMap.get la (abtcb adt) with
              | AbTCBValid _ cpu _ ⇒
                if zeq cpu (CPU_ID adt) then
                  match (ZMap.get curid (abtcb adt)) with
                    | AbTCBValid st _ _ ⇒
                      
                      if zeq curid la then None
                      else
                        Some (adt {kctxt: ZMap.set curid rs (kctxt adt)}
                                  {abtcb: ZMap.set la (AbTCBValid RUN cpu (-1)) (abtcb adt)}
                                  {abq: ZMap.set rdyq (AbQValid l) (abq adt)}
                                  {cid: (ZMap.set (CPU_ID adt) la (cid adt))}, ZMap.get la (kctxt adt))
                    | _ ⇒ None
                  end
                else None
              | _⇒ None
            end
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function sched_init_spec (mbi_adr:Z) (adt: RData) : option RData :=
    match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
      | (false, false, true, true, true, false) ⇒
        let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
        if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
          if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
            Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
                 {lapic: (mkLApicData
                            (mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
                                          (32 + 7) true true true 0 50 false 0))
                           {l1: l1 (lapic adt)}
                           {l2: l2 (lapic adt)}
                           {l3: l3 (lapic adt)}
                 } {ioapic / s / CurrentIrq: None}
                 {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
                 {AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
                 {multi_log: CalTicketLock.real_multi_log (multi_log adt)}
                 {lock: CalTicketLock.real_lock (lock adt)}
                 {idpde: real_idpde (idpde adt)}
                 {smspool: real_smspool (smspool adt)}
                 {abtcb: ZMap.set 0 (AbTCBValid RUN (CPU_ID adt) (-1))
                                  (real_abtcb (abtcb adt))}
                 {abq: real_abq (abq adt)}
                 
                 {syncchpool: real_syncchpool (syncchpool adt)}
                 {cid: real_cidpool (cid adt)}
          else None
        else None
      | _ ⇒ None
    end.

  Function thread_poll_pending_spec (adt: RData) :=
    let cpu := (CPU_ID adt) in
    let msgq := msg_q_id cpu in
    match dequeue_atomic_spec msgq adt with
      | Some (adt0, r) ⇒
        if zle_lt 0 r num_proc then
          let rdyq := rdy_q_id cpu in
          match ZMap.get rdyq (abq adt0) with
            | AbQValid l´ ⇒
              let n := ZMap.get cpu (sleeper (adt0)) - 1 in
              if zle_lt 0 n (num_proc - 1) then
                if cused (ZMap.get r (AC adt0)) then
                  Some (adt0 {abtcb: ZMap.set r (AbTCBValid READY cpu rdyq) (abtcb adt0)}
                             {abq: ZMap.set rdyq (AbQValid (l´ ++ (r::nil))) (abq adt0)}
                             {sleeper: ZMap.set cpu n (sleeper (adt0))})
                else None
              else None
            | _ ⇒ None
          end
        else Some adt0
      | _ ⇒ None
    end.


  Function thread_kill_spec (adt: RData) (rs: KContext) : option (RData×KContext) :=
    let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        let cpu := CPU_ID adt in
        let rdyq := rdy_q_id cpu in
        match ZMap.get rdyq (abq adt) with
          | AbQValid (la :: l) ⇒
            match ZMap.get la (abtcb adt) with
              | AbTCBValid _ cpu _ ⇒
                if zeq cpu (CPU_ID adt) then
                  match (ZMap.get curid (abtcb adt)) with
                    | AbTCBValid st cpu (-1) ⇒
                      if zeq cpu (CPU_ID adt) then
                        if zeq curid la then None
                        else
                          if zle_lt 0 la num_proc then
                            Some (adt {kctxt: ZMap.set curid rs (kctxt adt)}
                                      {abtcb: ZMap.set la (AbTCBValid RUN cpu (-1)) (ZMap.set curid (AbTCBValid DEAD cpu (-1)) (abtcb adt))}
                                      {abq: ZMap.set rdyq (AbQValid l) (abq adt)}
                                      {cid: (ZMap.set (CPU_ID adt) la (cid adt))}, ZMap.get la (kctxt adt))
                          else None
                      else None
                    | _ ⇒ None
                  end
                else None
              | _⇒ None
            end
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function thread_yield_spec (adt: RData) (rs: KContext) : option (RData × KContext) :=
    let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        let cpu := CPU_ID adt in
        match thread_poll_pending_spec adt with
          | Some adt0 ⇒
            let rdyq := rdy_q_id cpu in
            match ZMap.get rdyq (abq adt0), ZMap.get curid (abtcb adt0), cused (ZMap.get curid (AC adt0)) with
              | AbQValid (la :: l), AbTCBValid RUN cpu (-1), true ⇒
                match ZMap.get la (abtcb adt0) with
                  | AbTCBValid _ cpu2 _ ⇒
                    if zeq cpu (CPU_ID adt) then
                      if zeq cpu2 (CPU_ID adt) then
                        if zle_lt 0 la num_proc then
                          Some (adt0 {kctxt: ZMap.set curid rs (kctxt adt0)}
                                     {abtcb: ZMap.set la (AbTCBValid RUN cpu (-1))
                                                      (ZMap.set curid (AbTCBValid READY cpu rdyq) (abtcb adt0))}
                                     {abq: ZMap.set rdyq (AbQValid (l ++ (curid :: nil))) (abq adt0)}
                                     {cid: (ZMap.set (CPU_ID adt0) la (cid adt0))}
                                , ZMap.get la (kctxt adt0))
                        else
                          None
                      else
                        None
                    else
                      None
                  | _ ⇒ None
                end
              | _, _, _ ⇒ None
            end
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Function thread_sleep_spec (adt: RData) (rs: KContext) (cv: Z): option (RData × KContext) :=
    let cpu := (CPU_ID adt) in
    let curid := (ZMap.get cpu (cid adt)) in
    match (pg adt, ikern adt, ihost adt, ipt adt) with
      | (true, true, true, true) ⇒
        let cpu := CPU_ID adt in
        let n := slp_q_id cv 0 in
        let rdyq := rdy_q_id cpu in
        if zle_lt SLEEP_Q_START n TDQ_SIZE then
          if zlt_lt 0 curid num_proc then
            match enqueue_atomic_spec n curid adt with
              | Some adt1 ⇒
                match release_lock_SC_spec n adt1 with
                  | Some adt0 ⇒
                    match ZMap.get rdyq (abq adt0), ZMap.get curid (abtcb adt0) with
                      | AbQValid (next :: l´), (AbTCBValid RUN cpu _) ⇒
                        if zle_lt 0 next num_proc then
                          match ZMap.get next (abtcb adt0) with
                            | AbTCBValid _ cpu2 _ ⇒
                              let n0 := ZMap.get cpu (sleeper (adt0)) + 1 in
                              if zeq cpu (CPU_ID adt) then
                                if zeq cpu2 (CPU_ID adt) then
                                  if zlt_lt 0 n0 num_proc then
                                    Some (adt0 {kctxt: ZMap.set curid rs (kctxt adt0)}
                                               {abtcb: ZMap.set next (AbTCBValid RUN cpu (-1))
                                                                (ZMap.set curid (AbTCBValid SLEEP cpu n) (abtcb adt0))}
                                               {abq: ZMap.set rdyq (AbQValid l´) (abq adt0)}
                                               {cid: (ZMap.set (CPU_ID adt0) next (cid adt0))}
                                               {sleeper: ZMap.set cpu n0 (sleeper (adt0))}
                                          , ZMap.get next (kctxt adt0))
                                  else None
                                else None
                              else None
                            | _ ⇒ None
                          end
                        else None
                      | _, _ ⇒ None
                    end
                  | _ ⇒ None
                end
              | _ ⇒ None
            end
          else None
        else None
      | _ ⇒ None
    end.


End OBJ_Thread.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.

Local Open Scope Z_scope.

Section OBJ_SIM.

  Context `{data : CompatData RData}.
  Context `{data0 : CompatData RData}.

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.

  Notation HDATAOps := (cdata (cdata_prf := data) RData).
  Notation LDATAOps := (cdata (cdata_prf := data0) RData).

  Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
                               (stencil_ops:= stencil_ops) HDATAOps LDATAOps}.

  Context {re400: relate_impl_CPU_ID}.

  Section TDQUEUE_INIT0_SIM.

    Context `{real_params: RealParams}.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_LAT}.
    Context {re4: relate_impl_nps}.
    Context {re5: relate_impl_init}.
    Context {re6: relate_impl_PT}.
    Context {re7: relate_impl_ptpool}.
    Context {re8: relate_impl_idpde}.
    Context {re11: relate_impl_abtcb}.
    Context {re12: relate_impl_abq}.
    Context {re13: relate_impl_smspool}.
    Context {re14: relate_impl_vmxinfo}.
    Context {re15: relate_impl_AC}.

    Context {re16: relate_impl_ioapic}.
    Context {re17: relate_impl_lapic}.

    Context {mt100: match_impl_lock}.
    Context {re200: relate_impl_lock}.
    Context {re20: relate_impl_multi_log}.
    Context {re302: relate_impl_in_intr}.

    Lemma tdqueue_init0_exist:
      ∀ s habd habd´ labd f i,
        tdqueue_init0_spec i habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, tdqueue_init0_spec i labd = Some labd´ ∧
                   relate_AbData s f habd´ labd´.
    Proof.
      unfold tdqueue_init0_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_init_eq; eauto.
      exploit relate_impl_LAT_eq; eauto.
      exploit relate_impl_ptpool_eq; eauto.
      exploit relate_impl_idpde_eq; eauto.
      exploit relate_impl_CPU_ID_eq; eauto.
      exploit relate_impl_abq_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto.
      exploit relate_impl_vmxinfo_eq; eauto.
      exploit relate_impl_lock_eq; eauto.
      exploit relate_impl_smspool_eq; eauto.
      exploit relate_impl_multi_log_eq; eauto. intros.
      exploit relate_impl_ioapic_eq; eauto. intros.
      exploit relate_impl_lapic_eq; eauto. intros.
      exploit relate_impl_in_intr_eq; eauto; intros.

      revert H; subrewrite. subdestruct.
      inv HQ. refine_split´; trivial.

      apply relate_impl_abq_update.
      apply relate_impl_abtcb_update.
      apply relate_impl_smspool_update.
      apply relate_impl_idpde_update.
      apply relate_impl_lock_update.
      apply relate_impl_multi_log_update.
      apply relate_impl_ptpool_update.
      apply relate_impl_PT_update.
      apply relate_impl_init_update.
      apply relate_impl_AC_update.
      apply relate_impl_nps_update.
      apply relate_impl_LAT_update.
      apply relate_impl_pg_update.
      apply relate_impl_vmxinfo_update.
      apply relate_impl_ioapic_update.
      apply relate_impl_lapic_update.
      apply relate_impl_ioapic_update.
      assumption.
    Qed.

    Context {mt1: match_impl_iflags}.
    Context {mt2: match_impl_ipt}.
    Context {mt3: match_impl_LAT}.
    Context {mt4: match_impl_nps}.
    Context {mt5: match_impl_init}.
    Context {mt6: match_impl_PT}.
    Context {mt7: match_impl_ptpool}.
    Context {mt8: match_impl_idpde}.
    Context {mt10: match_impl_smspool}.
    Context {mt11: match_impl_abtcb}.
    Context {mt12: match_impl_abq}.
    Context {mt14: match_impl_vmxinfo}.
    Context {mt15: match_impl_AC}.
    Context {mt16: match_impl_ioapic}.
    Context {mt17: match_impl_lapic}.

    Context {mt50: match_impl_multi_log}.

    Lemma tdqueue_init0_match:
      ∀ s d d´ m i f,
        tdqueue_init0_spec i d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold tdqueue_init0_spec; intros.
      subdestruct; inv H; eauto.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update.
      eapply match_impl_smspool_update.
      eapply match_impl_idpde_update.

      eapply match_impl_lock_update.
      eapply match_impl_multi_log_update.

      eapply match_impl_ptpool_update.
      eapply match_impl_PT_update.
      eapply match_impl_init_update.
      eapply match_impl_AC_update.
      eapply match_impl_nps_update.
      eapply match_impl_LAT_update.
      eapply match_impl_pg_update.
      eapply match_impl_vmxinfo_update.
      eapply match_impl_ioapic_update.
      eapply match_impl_lapic_update.
      eapply match_impl_ioapic_update.
      assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) tdqueue_init0_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) tdqueue_init0_spec}.

    Lemma tdqueue_init0_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem tdqueue_init0_spec)
            (id ↦ gensem tdqueue_init0_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit tdqueue_init0_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply tdqueue_init0_match; eauto.
    Qed.

  End TDQUEUE_INIT0_SIM.

  Section DEQUEUE0_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_AC}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_abtcb}.

    Lemma dequeue0_exist:
      ∀ s habd habd´ labd f i z,
        dequeue0_spec i habd = Some (habd´, z)
        → relate_AbData s f habd labd
        → ∃ labd´, dequeue0_spec i labd = Some (labd´, z) ∧
                   relate_AbData s f habd´ labd´.
    Proof.
      unfold dequeue0_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto. intros.
      exploit relate_impl_abq_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto; intros.
      revert H; subrewrite.
      subdestruct; inv HQ; refine_split´; trivial.
      eapply relate_impl_abq_update; eauto.
      eapply relate_impl_abtcb_update; eauto.
    Qed.

    Context {mt1: match_impl_abtcb}.
    Context {mt2: match_impl_abq}.

    Lemma dequeue0_match:
      ∀ s d d´ m i z f,
        dequeue0_spec i d = Some (d´, z)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold dequeue0_spec; intros.
      subdestruct; inv H; eauto.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) dequeue0_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) dequeue0_spec}.

    Lemma dequeue0_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem dequeue0_spec)
            (id ↦ gensem dequeue0_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit dequeue0_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply dequeue0_match; eauto.
    Qed.

  End DEQUEUE0_SIM.

  Section DEQUEUE_ATOMIC_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_AC}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_abtcb}.
    Context {re6: relate_impl_multi_oracle}.
    Context {re7: relate_impl_multi_log}.
    Context {re8: relate_impl_CPU_ID}.
    Context {re9: relate_impl_lock}.

    Context `{waittime: WaitTime}.

    Lemma dequeue_atomic_exist:
      ∀ s habd habd´ labd i z f,
        dequeue_atomic_spec i habd = Some (habd´, z)
        → relate_AbData s f habd labd
        → ∃ labd´, dequeue_atomic_spec i labd = Some (labd´, z)
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold dequeue_atomic_spec; intros.
      revert H; subrewrite. subdestruct.
      specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
      intros [d0 [Hacq Hrel]]. rewrite Hacq.
      specialize (dequeue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
      intros [d1 [Henq Hrel1]]. rewrite Henq.
      specialize (release_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct2 Hrel1).
      intros [d2 [Hrls Hrel2]]. rewrite Hrls.
      ∃ d2. subst. inv HQ. eauto.
    Qed.

    Context {mt1: match_impl_abtcb}.
    Context {mt2: match_impl_abq}.
    Context {mt3: match_impl_multi_log}.
    Context {mt4: match_impl_lock}.

    Lemma dequeue_atomic_match:
      ∀ s d d´ m i z f,
        dequeue_atomic_spec i d = Some (d´, z)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold dequeue_atomic_spec; intros. subdestruct.
      specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
      specialize (dequeue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
      eapply release_lock_ABTCB_match; eauto. inversion H. subst. eauto.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) dequeue_atomic_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) dequeue_atomic_spec}.

    Lemma dequeue_atomic_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem dequeue_atomic_spec)
            (id ↦ gensem dequeue_atomic_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit dequeue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply dequeue_atomic_match; eauto.
    Qed.

  End DEQUEUE_ATOMIC_SIM.

  Section THREAD_pOLL_PENDING_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_AC}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_abtcb}.
    Context {re6: relate_impl_multi_oracle}.
    Context {re7: relate_impl_multi_log}.
    Context `{waittime: WaitTime}.
    Context {re8: relate_impl_CPU_ID}.
    Context {re9: relate_impl_lock}.
    Context {re10: relate_impl_sleeper}.

    Lemma thread_poll_pending_exist:
      ∀ s habd habd´ labd f,
        thread_poll_pending_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, thread_poll_pending_spec labd = Some labd´
                   ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_poll_pending_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      exploit relate_impl_sleeper_eq; eauto. intros.
      exploit relate_impl_abq_eq; eauto. intros.
      exploit relate_impl_abtcb_eq; eauto. intros.
      exploit relate_impl_AC_eq; eauto. intros.
      revert H; subrewrite. subdestruct.
      {
        specialize (dequeue_atomic_exist _ _ _ _ _ _ _ Hdestruct H0).
        intros [d0 [Hdeq Hrel]]. rewrite Hdeq.
        rewrite Hdestruct1.
        exploit relate_impl_abq_eq; eauto. intros Habq. rewrite <- Habq.
        rewrite Hdestruct4.
        exploit relate_impl_sleeper_eq; eauto. intros Hslp. rewrite <- Hslp.
        rewrite zle_lt_true; trivial.
        exploit relate_impl_AC_eq; eauto. intros HACp. rewrite <- HACp.
        rewrite Hdestruct3.
        inv HQ.
        esplit. split.
        f_equal.
        eapply relate_impl_sleeper_update; eauto.
        eapply relate_impl_abq_update; eauto.
        exploit relate_impl_abtcb_eq; eauto.
        intros Habtcb.
        rewrite <- Habtcb.
        eapply relate_impl_abtcb_update; eauto.
      }
      {
        specialize (dequeue_atomic_exist _ _ _ _ _ _ _ Hdestruct H0).
        intros [d0 [Hdeq Hrel]]. rewrite Hdeq.
        rewrite Hdestruct1.
        ∃ d0.
        split. reflexivity.
        inv HQ.
        assumption.
      }
      
    Qed.

    Context {mt1: match_impl_abtcb}.
    Context {mt2: match_impl_abq}.
    Context {mt3: match_impl_multi_log}.
    Context {mt4: match_impl_lock}.
    Context {mt5: match_impl_sleeper}.

    Lemma thread_poll_pending_match:
      ∀ s d d´ m f,
        thread_poll_pending_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_poll_pending_spec; intros. subdestruct.
      - specialize (dequeue_atomic_match _ _ _ _ _ _ _ Hdestruct H0). intros Hm1.
        inv H. eapply match_impl_sleeper_update.
        eapply match_impl_abq_update.
        eapply match_impl_abtcb_update.
        assumption.
      - specialize (dequeue_atomic_match _ _ _ _ _ _ _ Hdestruct H0). intros Hm1.
        inv H. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) thread_poll_pending_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) thread_poll_pending_spec}.

    Lemma thread_poll_pending_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem thread_poll_pending_spec)
            (id ↦ gensem thread_poll_pending_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_poll_pending_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_poll_pending_match; eauto.
    Qed.

  End THREAD_pOLL_PENDING_SIM.


  Section GET_STATE0_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_abtcb}.

    Lemma get_state0_exist:
      ∀ s habd labd i z f,
        get_state0_spec i habd = Some z
        → relate_AbData s f habd labd
        → get_state0_spec i labd = Some z.
    Proof.
      unfold get_state0_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto; intros.
      revert H; subrewrite.
    Qed.

    Lemma get_state0_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem get_state0_spec)
            (id ↦ gensem get_state0_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
      match_external_states_simpl.
      erewrite get_state0_exist; eauto. reflexivity.
    Qed.

  End GET_STATE0_SIM.

  Section SET_STAte0.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_abtcb}.

    Lemma set_state0_exist:
      ∀ s f habd habd´ labd i j,
        set_state0_spec i j habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, set_state0_spec i j labd = Some labd´ ∧
                   relate_AbData s f habd´ labd´.
    Proof.
      unfold set_state0_spec. intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto. intros.
      exploit relate_impl_abtcb_eq; eauto. intros.
      revert H. subrewrite.
      subdestruct.
      inv HQ; refine_split´; trivial.
      apply relate_impl_abtcb_update; eauto.
    Qed.

    Context {mt1: match_impl_abtcb}.

    Lemma set_state0_match:
      ∀ s d d´ m i j f,
        set_state0_spec i j d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold set_state0_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_abtcb_update. assumption.
    Qed.

    Context {inv1: PreservesInvariants (HD:= data) set_state0_spec}.
    Context {inv2: PreservesInvariants (HD:= data0) set_state0_spec}.

    Lemma set_state0_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem set_state0_spec)
            (id ↦ gensem set_state0_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit set_state0_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply set_state0_match; eauto.
    Qed.

  End SET_STAte0.

  Section SLEePER_inc.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_sleeper}.

    Lemma sleeper_inc_exist:
      ∀ s f habd habd´ labd,
        sleeper_inc_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, sleeper_inc_spec labd = Some labd´ ∧
                   relate_AbData s f habd´ labd´.
    Proof.
      unfold sleeper_inc_spec. intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_sleeper_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      revert H. subrewrite.
      subdestruct.
      inv HQ; refine_split´; trivial.
      apply relate_impl_sleeper_update; eauto.
    Qed.

    Context {mt1: match_impl_sleeper}.
    Context {mt2: match_impl_CPU_ID}.

    Lemma sleeper_inc_match:
      ∀ s d d´ m f,
        sleeper_inc_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold sleeper_inc_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_sleeper_update. assumption.
    Qed.

    Context {inv1: PreservesInvariants (HD:= data) sleeper_inc_spec}.
    Context {inv2: PreservesInvariants (HD:= data0) sleeper_inc_spec}.

    Lemma sleeper_inc_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem sleeper_inc_spec)
            (id ↦ gensem sleeper_inc_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit sleeper_inc_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply sleeper_inc_match; eauto.
    Qed.

  End SLEePER_inc.


  Section SLEePER_dec.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_sleeper}.

    Lemma sleeper_dec_exist:
      ∀ s f habd habd´ labd,
        sleeper_dec_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, sleeper_dec_spec labd = Some labd´ ∧
                   relate_AbData s f habd´ labd´.
    Proof.
      unfold sleeper_dec_spec. intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_sleeper_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      revert H. subrewrite.
      subdestruct.
      inv HQ; refine_split´; trivial.
      apply relate_impl_sleeper_update; eauto.
    Qed.

    Context {mt1: match_impl_sleeper}.
    Context {mt2: match_impl_CPU_ID}.

    Lemma sleeper_dec_match:
      ∀ s d d´ m f,
        sleeper_dec_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold sleeper_dec_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_sleeper_update. assumption.
    Qed.

    Context {inv1: PreservesInvariants (HD:= data) sleeper_dec_spec}.
    Context {inv2: PreservesInvariants (HD:= data0) sleeper_dec_spec}.

    Lemma sleeper_dec_sim:
      ∀ id,
        sim (crel RData RData) (id ↦ gensem sleeper_dec_spec)
            (id ↦ gensem sleeper_dec_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit sleeper_dec_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply sleeper_dec_match; eauto.
    Qed.

  End SLEePER_dec.

  Section SLEePER_ZzZ_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_CPU_ID}.
    Context {re3: relate_impl_sleeper}.

    Lemma sleeper_zzz_exist:
      ∀ s habd labd z f,
        sleeper_zzz_spec habd = Some z
        → relate_AbData s f habd labd
        → sleeper_zzz_spec labd = Some z.
    Proof.
      unfold sleeper_zzz_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_sleeper_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      revert H; subrewrite.
    Qed.

    Lemma sleeper_zzz_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem sleeper_zzz_spec)
            (id ↦ gensem sleeper_zzz_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
      match_external_states_simpl.
      erewrite sleeper_zzz_exist; eauto. reflexivity.
    Qed.

  End SLEePER_ZzZ_SIM.


  Section GET_ABTCB_CPU_ID_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_abtcb}.

    Lemma get_abtcb_CPU_ID_exist:
      ∀ s habd labd i z f,
        get_abtcb_CPU_ID_spec i habd = Some z
        → relate_AbData s f habd labd
        → get_abtcb_CPU_ID_spec i labd = Some z.
    Proof.
      unfold get_abtcb_CPU_ID_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto; intros.
      revert H; subrewrite.
    Qed.

    Lemma get_abtcb_CPU_ID_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem get_abtcb_CPU_ID_spec)
            (id ↦ gensem get_abtcb_CPU_ID_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
      match_external_states_simpl.
      erewrite get_abtcb_CPU_ID_exist; eauto. reflexivity.
    Qed.

  End GET_ABTCB_CPU_ID_SIM.

  Section SET_ABTCB_CPU_ID_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_abtcb}.
    Context {mt1: match_impl_abtcb}.

    Lemma set_abtcb_CPU_ID_exist:
      ∀ s habd labd n c habd´ f,
        set_abtcb_CPU_ID_spec n c habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, set_abtcb_CPU_ID_spec n c labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold set_abtcb_CPU_ID_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto; intros.
      revert H; subrewrite. subdestruct.
      inv HQ. esplit. split. trivial.
      eapply relate_impl_abtcb_update. assumption.
    Qed.

    Lemma set_abtcb_CPU_ID_match:
      ∀ s d d´ m i z f,
        set_abtcb_CPU_ID_spec i z d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold set_abtcb_CPU_ID_spec; intros. subdestruct.
      inv H. eapply match_impl_abtcb_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) set_abtcb_CPU_ID_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) set_abtcb_CPU_ID_spec}.

    Lemma set_abtcb_CPU_ID_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem set_abtcb_CPU_ID_spec)
            (id ↦ gensem set_abtcb_CPU_ID_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
      exploit set_abtcb_CPU_ID_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply set_abtcb_CPU_ID_match; eauto.
    Qed.

  End SET_ABTCB_CPU_ID_SIM.

  Section THREAD_KILL.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_kctxt}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_abtcb}.
    Context {re7: relate_impl_multi_oracle}.
    Context {re8: relate_impl_multi_log}.
    Context {re9: relate_impl_lock}.
    Context {re10: relate_impl_sleeper}.
    Context {re11: relate_impl_AC}.

    Local Opaque remove.

    Context `{high1: @high_level_invariant_impl_AbQCorrect_range data_ops}.
    Context `{high2: @high_level_invariant_impl_CPU_ID_range data_ops}.

    Lemma thread_kill_exists:
      ∀ s habd habd´ labd rs rs´ rs0 f,
        thread_kill_spec
          habd ((Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
                                     #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA)) = Some (habd´, rs´)
        → relate_AbData s f habd labd
        → @high_level_invariant _ data_ops habd
        → (∀ reg : PregEq.t,
              val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
        → ∃ labd´ rs0´ ofs,
             thread_kill_spec
               labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
                                          #EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) = Some (labd´, rs0´)
             ∧ relate_AbData s f habd´ labd´
             ∧ (∀ i r,
                   ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
             ∧ 0 ≤ ofs < num_proc
             ∧ ZMap.get ofs (kctxt labd) = rs0´.
    Proof.
      unfold thread_kill_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto.
      exploit relate_impl_cid_eq; eauto.
      exploit relate_impl_abq_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      exploit relate_impl_AC_eq; eauto. intros.
      specialize (high_level_invariant_impl_AbQCorrect_range_eq _ H1); intros Hinv1.
      specialize (high_level_invariant_impl_CPU_ID_range_eq habd H1); intros Hinv2.
      revert H. subrewrite. intros.
      subdestruct; inv HQ.
      generalize (relate_impl_kctxt_eq _ _ _ _ H0); eauto. intros.
      subrewrite´.
      assert(zrange: 0 ≤ z < num_proc).
      {
        specialize (Hinv1 pg_eq).
        unfold AbQCorrect_range in Hinv1.
        unfold rdy_q_id in Hdestruct3.
        simpl in Hdestruct3.
        rewrite <- H8 in Hdestruct3.
        assert(idrange: 0 ≤ CPU_ID habd < num_chan) by omega.
        specialize (Hinv1 (CPU_ID habd) idrange).
        unfold AbQCorrect in Hinv1.
        destruct Hinv1.
        destruct H10.
        rewrite <- H4 in Hdestruct3.
        rewrite Hdestruct3 in H10; inv H10.
        eapply H11; eauto.
        constructor.
        reflexivity.
      }

      refine_split´. reflexivity.
      - apply relate_impl_cid_update.
        apply relate_impl_abq_update.
        apply relate_impl_abtcb_update.
        apply relate_impl_kctxt_update; trivial.
        kctxt_inj_simpl.
      - intros; eapply H; eauto.
      - instantiate (1:= z); omega.
      - reflexivity.
    Qed.

    Context {mt1: match_impl_kctxt}.
    Context {mt2: match_impl_cid}.
    Context {mt3: match_impl_abq}.
    Context {mt4: match_impl_abtcb}.
    Context {mt5: match_impl_multi_log}.
    Context {mt6: match_impl_multi_oracle}.
    Context {mt7: match_impl_lock}.
    Context {mt8: match_impl_sleeper}.

    Lemma thread_kill_match:
      ∀ s d d´ m rs rs´ f,
        thread_kill_spec d rs = Some (d´, rs´)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_kill_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_cid_update.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update.
      eapply match_impl_kctxt_update; eauto.
    Qed.

    Context {inv: ThreadScheduleInvariants (data_ops:= data_ops) thread_kill_spec}.
    Context {inv0: ThreadScheduleInvariants (data_ops:= data_ops0) thread_kill_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma thread_kill_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_thread_schedule_compatsem thread_kill_spec (prim_ident:= id))
            (id ↦ primcall_thread_schedule_compatsem thread_kill_spec (prim_ident:= id)).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
      inv H. inv H0. inv match_extcall_states.
      exploit thread_kill_exists; eauto 1.
      intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
      - eapply kctxt_INJECT; try assumption.
      - eapply kctxt_INJECT; try assumption.
      - eapply thread_kill_match; eauto.
    Qed.

  End THREAD_KILL.

  Section THREAD_YIELD.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_kctxt}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_abtcb}.
    Context {re7: relate_impl_multi_oracle}.
    Context {re8: relate_impl_multi_log}.
    Context {re9: relate_impl_lock}.
    Context {re10: relate_impl_sleeper}.
    Context {re11: relate_impl_AC}.

    Local Opaque remove.

    Context `{high1: @high_level_invariant_impl_AbQCorrect_range data_ops}.
    Context `{high2: @high_level_invariant_impl_CPU_ID_range data_ops}.

    Lemma list_not_in_last:
      ∀ {A} l (a x: A),
        x ≠ a →
        In x (l ++ a :: nil) →
        In x l.
    Proof.
      intros A l a x H Hx.
      apply in_rev in Hx. rewrite rev_unit in Hx.
      Transparent In.
      simpl in Hx.
      Opaque In.
      destruct Hx as [Hx | Hx].
      - congruence.
      - apply in_rev in Hx. assumption.
    Qed.

    Lemma thread_poll_pending_preserves_kctxt:
      ∀ z d d´,
        thread_poll_pending_spec d = Some d´ →
        ZMap.get z (kctxt d) = ZMap.get z (kctxt d´).
    Proof.
      intros z d d´ Hspec.
      functional inversion Hspec; subst; simpl in ×.
      - functional inversion H0; subst; simpl in ×.
        unfold acquire_lock_ABTCB_spec in H6; subdestruct; subst; simpl in ×.
        inv H6.
        + functional inversion H8; subst n; subst; simpl in ×.
          functional inversion H7; subst l´0; subst cpu0; subst; simpl in *;
            reflexivity.
        + functional inversion H8.
          functional inversion H7; subst n;
            subst l´0; subst cpu0; subst; simpl in *; inv H6;
              reflexivity.
      - functional inversion H0; subst; simpl in ×.
        unfold acquire_lock_ABTCB_spec in H3; subdestruct; subst; simpl in ×.
        inv H3.
        + functional inversion H5; subst; simpl in ×.
          functional inversion H4; subst cpu0; subst l´; subst; simpl in *;
            reflexivity.
        + functional inversion H5.
          functional inversion H4;
            subst cpu0; subst l´; subst; simpl in *; inv H3;
              reflexivity.
    Qed.

    Lemma thread_yield_exists:
      ∀ s habd habd´ labd rs rs´ rs0 f,
        thread_yield_spec
          habd ((Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
                                     #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA)) = Some (habd´, rs´)
        → relate_AbData s f habd labd
        → @high_level_invariant _ data_ops habd
        → (∀ reg : PregEq.t,
              val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
        → ∃ labd´ rs0´ ofs,
             thread_yield_spec
               labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
                                          #EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) = Some (labd´, rs0´)
             ∧ relate_AbData s f habd´ labd´
             ∧ (∀ i r,
                   ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
             ∧ 0 ≤ ofs < num_proc
             ∧ ZMap.get ofs (kctxt labd) = rs0´.
    Proof.
      unfold thread_yield_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto.
      exploit relate_impl_cid_eq; eauto.
      exploit relate_impl_abq_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      exploit relate_impl_AC_eq; eauto. intros.
      specialize (high_level_invariant_impl_AbQCorrect_range_eq _ H1); intros Hinv1.
      specialize (high_level_invariant_impl_CPU_ID_range_eq habd H1); intros Hinv2.
      revert H. subrewrite. intros.
      subdestruct; inv HQ.
      exploit thread_poll_pending_exist; eauto; intros (labd´ & HP & HM).
      rewrite HP.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto; inversion 1.
      exploit relate_impl_abtcb_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_abq_eq; eauto; inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_AC_eq; eauto. inversion 1.
      generalize (relate_impl_kctxt_eq _ _ _ _ HM); eauto. intros.
      subrewrite´.

      refine_split´. reflexivity.
      - apply relate_impl_cid_update.
        apply relate_impl_abq_update.
        apply relate_impl_abtcb_update.
        apply relate_impl_kctxt_update; trivial.
        kctxt_inj_simpl.
      - intros; eapply H21; eauto.
      - instantiate (1:= z); omega.
      - erewrite thread_poll_pending_preserves_kctxt; eauto.
    Qed.

    Context {mt1: match_impl_kctxt}.
    Context {mt2: match_impl_cid}.
    Context {mt3: match_impl_abq}.
    Context {mt4: match_impl_abtcb}.
    Context {mt5: match_impl_multi_log}.
    Context {mt6: match_impl_multi_oracle}.
    Context {mt7: match_impl_lock}.
    Context {mt8: match_impl_sleeper}.

    Lemma thread_yield_match:
      ∀ s d d´ m rs rs´ f,
        thread_yield_spec d rs = Some (d´, rs´)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_yield_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_cid_update.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update.
      eapply match_impl_kctxt_update.
      exploit thread_poll_pending_match; eauto.
    Qed.

    Context {inv: ThreadScheduleInvariants (data_ops:= data_ops) thread_yield_spec}.
    Context {inv0: ThreadScheduleInvariants (data_ops:= data_ops0) thread_yield_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma thread_yield_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_thread_schedule_compatsem thread_yield_spec (prim_ident:= id))
            (id ↦ primcall_thread_schedule_compatsem thread_yield_spec (prim_ident:= id)).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
      inv H. inv H0. inv match_extcall_states.
      exploit thread_yield_exists; eauto 1.
      intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
      - eapply kctxt_INJECT; try assumption.
      - eapply kctxt_INJECT; try assumption.
      - eapply thread_yield_match; eauto.
    Qed.

  End THREAD_YIELD.


  Section ENQUEUE0_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_AC}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_abtcb}.

    Lemma enqueue0_exist:
      ∀ s habd habd´ labd i z f,
        enqueue0_spec i z habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, enqueue0_spec i z labd = Some labd´
                   ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold enqueue0_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_AC_eq; eauto.
      exploit relate_impl_abq_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto; intros.
      revert H; subrewrite. subdestruct.
      inv HQ. refine_split´; trivial.
      eapply relate_impl_abq_update.
      eapply relate_impl_abtcb_update. assumption.
    Qed.

    Context {mt1: match_impl_abtcb}.
    Context {mt2: match_impl_abq}.

    Lemma enqueue0_match:
      ∀ s d d´ m i z f,
        enqueue0_spec i z d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold enqueue0_spec; intros. subdestruct. inv H.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) enqueue0_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) enqueue0_spec}.

    Lemma enqueue0_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem enqueue0_spec)
            (id ↦ gensem enqueue0_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit enqueue0_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply enqueue0_match; eauto.
    Qed.

  End ENQUEUE0_SIM.

  Section ENQUEUE_ATOMIC_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_AC}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_abtcb}.
    Context {re6: relate_impl_multi_oracle}.
    Context {re7: relate_impl_multi_log}.
    Context `{waittime: WaitTime}.
    Context {re8: relate_impl_CPU_ID}.
    Context {re9: relate_impl_lock}.

    Lemma enqueue_atomic_exist:
      ∀ s habd habd´ labd i z f,
        enqueue_atomic_spec i z habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, enqueue_atomic_spec i z labd = Some labd´
                   ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold enqueue_atomic_spec; intros.
      revert H; subrewrite. subdestruct.
      specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
      intros [d0 [Hacq Hrel]]. rewrite Hacq.
      specialize (enqueue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
      intros [d1 [Henq Hrel1]]. rewrite Henq.
      eapply release_lock_ABTCB_exist; eauto.
    Qed.

    Context {mt1: match_impl_abtcb}.
    Context {mt2: match_impl_abq}.
    Context {mt3: match_impl_multi_log}.
    Context {mt4: match_impl_lock}.

    Lemma enqueue_atomic_match:
      ∀ s d d´ m i z f,
        enqueue_atomic_spec i z d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold enqueue_atomic_spec; intros. subdestruct.
      specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
      specialize (enqueue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
      eapply release_lock_ABTCB_match; eauto.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) enqueue_atomic_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) enqueue_atomic_spec}.

    Lemma enqueue_atomic_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem enqueue_atomic_spec)
            (id ↦ gensem enqueue_atomic_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit enqueue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply enqueue_atomic_match; eauto.
    Qed.

  End ENQUEUE_ATOMIC_SIM.


  Section THREAD_SLEEP.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_ipt}.
    Context {re3: relate_impl_kctxt}.
    Context {re4: relate_impl_abq}.
    Context {re5: relate_impl_cid}.
    Context {re6: relate_impl_abtcb}.
    Context {re7: relate_impl_AC}.
    Context {re8: relate_impl_multi_oracle}.
    Context {re9: relate_impl_multi_log}.
    Context {re10: relate_impl_CPU_ID}.
    Context {re11: relate_impl_lock}.
    Context {re12: relate_impl_syncchpool}.
    Context {re13: relate_impl_sleeper}.

    Context `{waittime: WaitTime}.

    Local Opaque remove.

    Context `{high: @high_level_invariant_impl_AbQCorrect_range data_ops}.
    Context `{high2: @high_level_invariant_impl_CPU_ID_range data_ops}.

    Lemma thread_sleep_exists:
      ∀ s habd habd´ labd rs rs´ rs0 n f,
        thread_sleep_spec
          habd ((Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
                                     #EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA)) n = Some (habd´, rs´)
        → relate_AbData s f habd labd
        → @high_level_invariant _ data_ops habd
        → (∀ reg : PregEq.t,
              val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
        → ∃ labd´ rs0´ ofs,
            thread_sleep_spec
              labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
                                         #EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) n = Some (labd´, rs0´)
            ∧ relate_AbData s f habd´ labd´
            ∧ (∀ i r,
                  ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
            ∧ 0 ≤ ofs < num_proc
            ∧ ZMap.get ofs (kctxt labd) = rs0´.
    Proof.
      unfold thread_sleep_spec; intros.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto.
      exploit relate_impl_abtcb_eq; eauto.
      exploit relate_impl_cid_eq; eauto.
      exploit relate_impl_abq_eq; eauto. intros.
      exploit relate_impl_CPU_ID_eq; eauto. intros.
      specialize (high_level_invariant_impl_AbQCorrect_range_eq _ H1); intros Hinv1.
      specialize (high_level_invariant_impl_CPU_ID_range_eq habd H1); intros Hinv2.
      revert H. subrewrite. intros.
      subdestruct; inv HQ.
      exploit enqueue_atomic_exist; eauto; intros (labd1 & HP1 & HM1).
      rewrite HP1.
      exploit release_lock_SC_exist; eauto; intros (labd2 & HP2 & HM2).
      rewrite HP2.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_ipt_eq; eauto; inversion 1.
      exploit relate_impl_abtcb_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      exploit relate_impl_abq_eq; eauto; inversion 1.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_sleeper_eq; eauto; inversion 1.
      generalize (relate_impl_kctxt_eq _ _ _ _ HM2); eauto. intros.
      subrewrite´.
      refine_split´. reflexivity.
      - apply relate_impl_sleeper_update.
        apply relate_impl_cid_update.
        apply relate_impl_abq_update.
        apply relate_impl_abtcb_update.
        apply relate_impl_kctxt_update; trivial.
        kctxt_inj_simpl.
      - intros; eapply H20; eauto.
      - instantiate (1:= z); omega.
      - functional inversion HP2. functional inversion HP1.
        simpl. functional inversion H30. functional inversion H32. simpl.
        unfold acquire_lock_ABTCB_spec in H31.
        subdestruct; inversion H31; simpl; reflexivity.
    Qed.

    Context {mt1: match_impl_kctxt}.
    Context {mt2: match_impl_cid}.
    Context {mt3: match_impl_abq}.
    Context {mt4: match_impl_abtcb}.
    Context {mt5: match_impl_multi_log}.
    Context {mt6: match_impl_syncchpool}.
    Context {mt7: match_impl_lock}.
    Context {mt40: match_impl_sleeper}.

    Lemma thread_sleep_match:
      ∀ s d d´ m rs rs´ n f,
        thread_sleep_spec d rs n = Some (d´, rs´)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_sleep_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_sleeper_update.
      eapply match_impl_cid_update.
      eapply match_impl_abq_update.
      eapply match_impl_abtcb_update.
      eapply match_impl_kctxt_update.
      exploit release_lock_SC_match; [eauto| |].
      exploit enqueue_atomic_match; [eauto | |].
      eassumption.
      intros Hx. eapply Hx.
      intros Hx. eapply Hx.
    Qed.

    Context {inv: ThreadTransferInvariants (data_ops:= data_ops) thread_sleep_spec}.
    Context {inv0: ThreadTransferInvariants (data_ops:= data_ops0) thread_sleep_spec}.

    Context {low1: low_level_invariant_impl}.

    Lemma thread_sleep_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ primcall_thread_transfer_compatsem thread_sleep_spec)
            (id ↦ primcall_thread_transfer_compatsem thread_sleep_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
      inv H. inv H0. inv match_extcall_states.
      exploit thread_sleep_exists; eauto 1.
      intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
      exploit low_level_invariant_impl_eq; eauto. inversion 1.
      match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
      - inv H9. inv H3. simpl in ×.
        exploit Mem.loadv_inject; try eassumption.
        val_inject_simpl. unfold Pregmap.get.
        intros (v2 & HL & Hv). inv Hv. assumption.
      - eapply kctxt_INJECT; try assumption.
      - eapply kctxt_INJECT; try assumption.
      - eapply thread_sleep_match; eauto.
    Qed.

  End THREAD_SLEEP.