Library mcertikos.proc.BThreadGen


This file provide the contextual refinement proof between PQueueIntro layer and PQueueInit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem3.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.

Require Import LAsmModuleSemAux.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.


Require Import PBThread.
Require Import VVMXInit.
Require Export BThreadGenDef.

Definition of the refinement relation

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

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

  Notation HDATA := RData.
  Notation LDATA := RData.

  Notation HDATAOps := (cdata (cdata_ops := pbthread_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) LDATA).

  Section WITHMEM.

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


Relation between raw data at two layers
    Record relate_RData (f: meminj) (hadt: HDATA) (ladt: LDATA) :=
      mkrelate_RData {
          flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
          vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
          CR3_re: CR3 hadt = CR3 ladt;
          ikern_re: ikern hadt = ikern ladt;
          pg_re: pg hadt = pg ladt;
          ihost_re: ihost hadt = ihost ladt;
          AC_re: AC hadt = AC ladt;
          ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
          ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
          LAT_re: LAT hadt = LAT ladt;
          nps_re: nps hadt = nps ladt;
          init_re: init hadt = init ladt;

          pperm_re: pperm hadt = pperm ladt;
          PT_re: PT hadt = PT ladt;
          ptp_re: ptpool hadt = ptpool ladt;
          idpde_re: idpde hadt = idpde ladt;
          ipt_re: ipt hadt = ipt ladt;
          smspool_re: smspool hadt = smspool ladt;

          CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
          cid_re: cid hadt = cid ladt;
          multi_oracle_re: relate_big_small_oracle (big_oracle hadt) (multi_oracle ladt);
          multi_log_re: relate_big_small_log_pool (big_log hadt) (multi_log ladt);
          lock_re: lock hadt = lock ladt;

          com1_re: com1 hadt = com1 ladt;
          console_re: console hadt = console ladt;
          console_concrete_re: console_concrete hadt = console_concrete ladt;
          ioapic_re: ioapic ladt = ioapic hadt;
          lapic_re: lapic ladt = lapic hadt;
          intr_flag_re: intr_flag ladt = intr_flag hadt;
          curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
          in_intr_re: in_intr ladt = in_intr hadt;
          drv_serial_re: drv_serial hadt = drv_serial ladt;

          kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
          uctxt_re: uctxt_inj f (uctxt hadt) (uctxt ladt);

          
          syncchpool_re: syncchpool hadt = syncchpool ladt;

          
          ept_re: ept hadt = ept ladt;
          vmcs_re: VMCSPool_inj f (vmcs hadt) (vmcs ladt);
          vmx_re: VMXPool_inj f (vmx hadt) (vmx ladt)
        }.

    Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
    | MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.

    Local Hint Resolve MATCH_RDATA.

    Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
      {
        relate_AbData s f d1 d2 := relate_RData f d1 d2;
        match_AbData s d1 m f := match_RData s d1 m f;
        new_glbl := nil
      }.

Properties of relations

    Section Rel_Property.

Prove that after taking one step, the refinement relation still holds
      Lemma relate_incr:
        ∀ abd abd´ f f´,
          relate_RData f abd abd´
          → inject_incr f f´
          → relate_RData f´ abd abd´.
      Proof.
        inversion 1; subst; intros; inv H; constructor; eauto.
        - eapply kctxt_inj_incr; eauto.
        - eapply uctxt_inj_incr; eauto.
        - unfold VMCSPool_inj.
          intros.
          eapply VMCS_inj_incr; eauto.
        - unfold VMXPool_inj.
          intros.
          eapply VMX_inj_incr; eauto.
      Qed.

    End Rel_Property.

    Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
    Proof.
      constructor; intros; simpl; trivial.
      eapply relate_incr; eauto.
    Qed.

Proofs the one-step forward simulations for the low level specifications

    Section OneStep_Forward_Relation.

The low level specifications exist

      Section Exists.

        Require Import TacticsForTesting.

        Ltac cases :=
          repeat match goal with
                   | [ |- appcontext [if ?a then _ else _] ] ⇒ subdestruct_if a
                   | [ |- appcontext [match ?a with _ ⇒ _ end] ] ⇒ subdestruct_if a
                 end.

        Lemma relate_big_small_log_nil_e:
          ∀ e l id l´
                 (Hrel: relate_big_small_log l id l´)
                 (H2id: BigE2id e id = nil),
            relate_big_small_log (e::l) id l´.
        Proof.
          intros. inv Hrel.
          econstructor; eauto.
          replace bl0 with (nil ++ bl0) by eauto.
          econstructor; eauto.
        Qed.

        Lemma remove_cache_event_gso:
          ∀ l l´ cid
                 (Hgso: ∀ e cid´,
                          In (TEVENT cid´ e) l → cid´ ≠ cid),
            remove_cache_event (l ++ l´) cid
            = remove_cache_event (l´) cid.
        Proof.
          induction l; simpl; eauto; intros.
          destruct a; eauto.
          rewrite zeq_false; eauto.
        Qed.

        Lemma BigE2id_gso:
          ∀ cid cid0 e id
                 (Hneq: cid ≠ cid0),
          (∀ e0 cid´,
             In (TEVENT cid´ e0)
                (BigE2id (TBEVENT cid e) id)
             → cid´ ≠ cid0).
        Proof.
          simpl; intros.
          subdestruct; eauto;
          repeat (destruct H; try congruence).
        Qed.

        Lemma relate_big_small_log_e_gso´:
          ∀ l ml id e cid
                 (Hrel: relate_big_small_log l id ml)
                 (Hneq: cid ≠ current_CPU_ID),
            relate_big_small_log (TBEVENT cid e :: l) id ml.
        Proof.
          simpl; intros. inv Hrel. econstructor.
          - econstructor; eauto.
          - erewrite remove_cache_event_gso; eauto.
            eapply BigE2id_gso; eauto.
        Qed.

        Lemma relate_big_small_log_gso´:
          ∀ l l´ ml id
                 (Hrel: relate_big_small_log l´ id ml)
                 (Hgso: ∀ e cid,
                          In (TBEVENT cid e) l → cid ≠ current_CPU_ID),
            relate_big_small_log (l ++ l´) id ml.
        Proof.
          induction l; eauto; simpl; intros.
          destruct a.
          eapply relate_big_small_log_e_gso´; eauto.
        Qed.

        Lemma option_eq:
          ∀ {A: Type} (e: option A),
            match e with
              | Some x ⇒ Some x
              | _ ⇒ None
            end = e.
        Proof.
          intros. destruct e; trivial.
        Qed.

        Lemma CALAT_BigLog:
          ∀ bl ml
                 (Horacle0 : BigLogMap2id bl 0 ml),
            B_CalAT_log_real bl = CalAT_log_real ml.
        Proof.
          induction bl; simpl; intros.
          - inv Horacle0. trivial.
          - inv Horacle0.
            unfold B_CalAT_log_real, CalAT_log_real in ×.
            simpl in ×. destruct a.
            exploit IHbl; eauto.
            intros Heq. rewrite Heq.
            destruct e; simpl.
            + eapply option_eq.
            + destruct e; simpl; eauto; eapply option_eq.
        Qed.

        Lemma append_rewrite {A: Type}:
          ∀ (a: A) l,
            a :: l = (a::nil) ++ l.
        Proof.
          simpl. trivial.
        Qed.

        Fixpoint BigLogMap2id_fun (bl: BigLog) (id: Z) : MultiLog :=
          match bl with
            | nil ⇒ nil
            | e :: bl ⇒ BigE2id e id ++ BigLogMap2id_fun bl id
          end.

        Lemma BigLogMap2id_alt:
          ∀ bl ml id,
            BigLogMap2id bl id ml ↔ BigLogMap2id_fun bl id = ml.
        Proof.
          induction bl; simpl; intros ml id; split; intro H; subst.
          - inv H; auto.
          - constructor.
          - inv H.
            apply IHbl in Hbig; congruence.
          - constructor; auto.
            apply IHbl; auto.
        Qed.

        Lemma BigLogMap2id_fun_app:
          ∀ bl bl´ id,
            BigLogMap2id_fun (bl ++ bl´) id =
            BigLogMap2id_fun bl id ++ BigLogMap2id_fun bl´ id.
        Proof.
          induction bl; simpl; intros; auto.
          rewrite <- app_assoc, IHbl; auto.
        Qed.

        Lemma BigLogMap2id_app:
          ∀ bl ml bl´ ml´ id,
            BigLogMap2id bl id ml →
            BigLogMap2id bl´ id ml´ →
            BigLogMap2id (bl ++ bl´) id (ml ++ ml´).
        Proof.
          intros; rewrite BigLogMap2id_alt in ×.
          rewrite BigLogMap2id_fun_app; congruence.
        Qed.

        Fixpoint all_id_eq (l : MultiLog) (i : Z) :=
          match l with
            | nil ⇒ True
            | TEVENT i´ _ :: l ⇒ i´ = i ∧ all_id_eq l i
          end.

        Lemma remove_cache_event_gss:
          ∀ l l´ i,
            all_id_eq l i → l ≠ nil →
            remove_cache_event (l++l´) i = l++l´.
        Proof.
          induction l; simpl; intros; [congruence|].
          subdestruct; cases; auto; omega.
        Qed.

        Lemma relate_big_small_log_pool_gss:
          ∀ bl0 ml0 bl bl´ ml id l l´
                 (Hnil: bl0 ≠ nil)
                 (Hcur: ∀ cid´ e, In (TBEVENT cid´ e) bl0 → cid´ = current_CPU_ID)
                 (Hrel: relate_big_small_log_pool (BigDef bl) ml)
                 (Hmap1: BigLogMap2id bl0 id ml0)
                 (Hmap2: BigLogMap2id (bl´ ++ bl) id (l´ ++ l))
                 (Hneq: ∀ abid be,
                          abid ≠ id →
                          In (TBEVENT current_CPU_ID be) bl0 →
                          BigE2id (TBEVENT current_CPU_ID be) abid = nil)
                 (Heq: ∀ be,
                         In (TBEVENT current_CPU_ID be) bl0 →
                         BigE2id (TBEVENT current_CPU_ID be) id ≠ nil ∧
                         all_id_eq (BigE2id (TBEVENT current_CPU_ID be) id) current_CPU_ID)
                 (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) bl´ → cid´ ≠ current_CPU_ID),
            relate_big_small_log_pool
              (BigDef
                 (bl0 ++ bl´ ++ bl))
              (ZMap.set id
                        (MultiDef
                           (ml0 ++ l´ ++ l)) ml).
        Proof.
          induction bl0; intros; [contradiction Hnil; auto|].
          destruct a as [id´ ?].
          assert (id´ = current_CPU_ID) by (simpl in Hcur; eauto); subst.
          edestruct Heq as [Hnil´ Heq´]; simpl; eauto.
          inv Hmap1.
          constructor; intros abid Habid.
          destruct (zeq abid id); subst.
          - rewrite ZMap.gss.
            refine_split´; eauto.
            econstructor.
            + apply BigLogMap2id_alt; auto.
            + unfold BigLogMap2id_fun; fold BigLogMap2id_fun.
              rewrite remove_cache_event_gss; auto.
              rewrite BigLogMap2id_alt in *; subst; rewrite <- Hmap2.
              rewrite <- app_assoc, 3 BigLogMap2id_fun_app; auto.
          - rewrite ZMap.gso; auto.
            destruct bl0 as [|e0].
            + inv Hrel.
              destruct (Hrel_log _ Habid) as [l1 [Hget Hrel´]].
              refine_split´; eauto.
              assert (Hrel0: relate_big_small_log (bl´++bl) abid l1) by (apply relate_big_small_log_gso´; auto).
              inv Hrel0; inv Hrel´.
              econstructor.
              × apply BigLogMap2id_alt; auto.
              × unfold BigLogMap2id_fun; fold BigLogMap2id_fun.
                rewrite BigLogMap2id_alt in Hlogmap; subst.
                rewrite Hneq; simpl; auto.
            + assert (IH: relate_big_small_log_pool (BigDef ((e0 :: bl0) ++ bl´ ++ bl))
                           (ZMap.set id (MultiDef (l0 ++ l´ ++ l)) ml))
                by (apply IHbl0; simpl in *; eauto; discriminate).
              inv IH.
              destruct (Hrel_log _ Habid) as [l1 [Hget Hrel´]]; rewrite ZMap.gso in Hget; auto.
              refine_split´; eauto.
              inv Hrel´; econstructor.
              × apply BigLogMap2id_alt; auto.
              × rewrite BigLogMap2id_alt in *; subst.
                unfold BigLogMap2id_fun; fold BigLogMap2id_fun.
                rewrite Hneq; simpl; auto.
        Qed.

         Lemma relate_big_small_log_pool_e_gss:
          ∀ bl bl´ ml id be me l l´
                 (Hrel: relate_big_small_log_pool (BigDef bl) ml)
                 (Hmap: BigLogMap2id (bl´ ++ bl) id (l´ ++ l))
                 (Hneq: ∀ abid,
                          abid ≠ id →
                          BigE2id (TBEVENT current_CPU_ID be) abid = nil)
                 (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) bl´ → cid´ ≠ current_CPU_ID)
                 (He: BigE2id (TBEVENT current_CPU_ID be) id = TEVENT current_CPU_ID me :: nil),
            relate_big_small_log_pool
              (BigDef
                 (TBEVENT current_CPU_ID be :: bl´ ++ bl))
              (ZMap.set id
                        (MultiDef
                           (TEVENT current_CPU_ID me :: l´ ++ l)) ml).
        Proof.
          intros.
          rewrite (append_rewrite _ (bl´++bl)), (append_rewrite _ (l´++l)).
          apply relate_big_small_log_pool_gss; auto.
          - discriminate.
          - destruct 1 as [Hcase|Hcase]; inv Hcase; auto.
          - apply BigLogMap2id_alt.
            unfold BigLogMap2id_fun; fold BigLogMap2id_fun; rewrite He; auto.
          - destruct 2 as [Hcase|Hcase]; inv Hcase; auto.
          - destruct 1 as [Hcase|Hcase]; inv Hcase; rewrite He.
            split; [discriminate | simpl; auto].
        Qed.

        Lemma valid_big_oracle:
          ∀ habd l
                 (Hhigh: PBThread.high_level_invariant habd),
            (∀ e cid´,
               In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l) →
               cid´ ≠ current_CPU_ID).
        Proof.
          intros ? ? Hinv; apply valid_big_oracle_inv in Hinv.
          destruct Hinv as [Hinv _]; eauto.
        Qed.

        Lemma palloc_exist:
          ∀ s habd habd´ labd n i f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_palloc_spec n habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, palloc_spec n labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold palloc_spec, big_palloc_spec; intros.
          revert H. pose proof H0 as HR. inv H0.
          subrewrite.
          d5 subdestruct_one.
          destruct (big_log habd) eqn: Hbig_log; contra_inv.
          pose proof multi_log_re0 as Hrel_log´.
          inv multi_log_re0.
          exploit (Hrel_log 0); eauto.
          intros (l0 & Hget0 & Hrel0).
          rewrite Hget0.
          pose proof multi_oracle_re0 as Horacle0.
          inv Horacle0.
          exploit (Hrel 0); eauto.
          intros Horacle0. clear Hrel.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          assert (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l) →
                             cid´ ≠ current_CPU_ID) by (eapply valid_big_oracle; eauto).
          rewrite <- HCPU in ×.
          d2 subdestruct_one.
          - erewrite <- CALAT_BigLog; eauto.
            subdestruct; inv HQ.
            + refine_split´; eauto.
              econstructor; eauto; simpl.
              × congruence.
              × eapply relate_big_small_log_pool_e_gss; eauto.
                intros. simpl.
                rewrite zeq_false; eauto.
                destruct (zeq abid lock_range); trivial.
            + refine_split´; eauto.
              econstructor; eauto; simpl.
              × congruence.
              × eapply relate_big_small_log_pool_e_gss; eauto.
                intros. simpl.
                rewrite zeq_false; eauto.
                destruct (zeq abid lock_range); trivial.
          - inv HQ. refine_split´; eauto.
            econstructor; eauto; simpl.
            × congruence.
            × eapply relate_big_small_log_pool_e_gss; eauto.
              intros. simpl.
              rewrite zeq_false; eauto.
              destruct (zeq abid lock_range); trivial.
        Qed.

        Lemma ptAllocPDE0_exist:
          ∀ s habd habd´ labd i n v f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ptAllocPDE_spec n v habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_ptAllocPDE_spec, ptAllocPDE0_spec; intros.
          pose proof H0 as HR. inv H0.
          revert H. subrewrite.
          subdestruct; destruct p; inv HQ.
          - exploit palloc_exist; eauto.
            intros (? & ? & ?).
            subrewrite´. refine_split´; trivial.
          - exploit palloc_exist; eauto.
            intros (? & ? & ?).
            rewrite H. rewrite Hdestruct8.
            refine_split´; trivial.
            inv H0.
            constructor; simpl; try eassumption.
            + apply FlatMem.free_page_inj´. trivial.
            + subrewrite´.
            + subrewrite´.
        Qed.

        Lemma ptInsert0_exist:
          ∀ s habd habd´ labd i n v pa pe f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ptInsert_spec n v pa pe habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_ptInsert_spec, ptInsert0_spec; intros.
          pose proof H0 as HR. inv H0.
          revert H. subrewrite.
          subdestruct; inv HQ.
          - exploit (ptInsertPTE0_exist s); eauto.
            intros (labd´ & HptInsert0´ & Hre).
            subrewrite´.
            refine_split´; trivial.
          - exploit ptAllocPDE0_exist; eauto.
            intros (labd´ & HptInsert0´ & Hre).
            subrewrite´.
            refine_split´; trivial.
          - exploit ptAllocPDE0_exist; eauto.
            intros (labd´ & HptInsert0´ & Hre).
            subrewrite´.
            exploit (ptInsertPTE0_exist s); eauto.
            intros (labd´0 & HptInsert0´´ & Hre´).
            subrewrite´.
            refine_split´; trivial.
        Qed.

        Lemma ptResv_exist:
          ∀ s habd habd´ labd i n v p f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ptResv_spec n v p habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_ptResv_spec, ptResv_spec; intros.
          subdestruct. destruct p0.
          - exploit palloc_exist; eauto.
            intros (? & ? & ?).
            subrewrite´. inv H. refine_split´; trivial.
          - exploit palloc_exist; eauto.
            intros (? &-> & ?).
            exploit PBThread.palloc_high_level_inv; eauto. intros.
            exploit (ptInsert0_exist s); eauto.
            intros (? & → & ?).
            subrewrite´. inv H. refine_split´; trivial.
        Qed.

        Lemma ptResv2_exist:
          ∀ s habd habd´ labd i n v p n´ v´ p´ f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_ptResv2_spec, ptResv2_spec; intros.
          subdestruct; destruct p0; inv H.
          - exploit palloc_exist; eauto.
            intros (? & → & ?).
            subrewrite´. refine_split´; trivial.
          - exploit palloc_exist; eauto.
            intros (? & ? & ?).
            exploit PBThread.palloc_high_level_inv; eauto. intros.
            exploit (ptInsert0_exist s); eauto.
            intros (? & ? & ?).
            subrewrite´. inv H. refine_split´; trivial.
          - exploit palloc_exist; eauto.
            intros (? & ? & ?). revert H2.
            exploit PBThread.palloc_high_level_inv; eauto. intros.
            exploit (ptInsert0_exist s); eauto.
            intros (? & ? & ?). intros.
            exploit (PBThread.ptInsert_high_level_inv r); eauto. intros.
            exploit (ptInsert0_exist s); eauto.
            intros (? & ? & ?).
            subrewrite´. refine_split´; trivial.
        Qed.
        Ltac subdestruct_goal:=
          repeat progress (
                   match goal with
                     | [ |- context[if ?con then _ else _]] ⇒ subdestruct_if con
                     | [ |- context[match ?con with |_ ⇒ _ end]] ⇒ subdestruct_if con
                   end; simpl; trivial).

        Lemma CALTCB_BigLog´:
          ∀ bl ml
                 (Horacle0 : BigLogMap2id bl lock_range ml),
            B_CalTCB_log bl = CalTCB_log ml.
        Proof.
          induction bl; simpl; intros.
          - inv Horacle0. trivial.
          - inv Horacle0.
            exploit IHbl; eauto. intros Heq.
            set (r:= CalTCB_log l) in ×.
            unfold B_CalTCB_log, CalTCB_log in ×.
            simpl. rewrite Heq.
            destruct a; simpl.
            destruct r eqn: Hr.
            + repeat destruct p. subst r.
              destruct e; simpl.
              × rewrite Hr; trivial.
              × destruct e eqn: He; simpl; try rewrite Hr; eauto.
            + subst r.
              destruct e; simpl.
              × rewrite Hr; trivial.
              × destruct e eqn: He; simpl; try rewrite Hr; eauto.
        Qed.

        Lemma CALTCB_BigLog:
          ∀ bl ml
                 (Horacle0 : BigLogMap2id bl lock_range ml),
            B_CalTCB_log_real bl = CalTCB_log_real ml.
        Proof.
          unfold B_CalTCB_log_real, CalTCB_log_real in ×.
          intros. eapply CALTCB_BigLog´ in Horacle0; eauto.
          rewrite Horacle0. trivial.
        Qed.

        Lemma biglow_thread_yield_exist:
          ∀ habd habd´ labd rs r´ rs0 s
                 (HINV: PBThread.high_level_invariant habd) f,
            big_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´, rs0)
            → relate_AbData s f habd labd
            
            → (∀ reg : PregEq.t,
                  val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
            → ∃ labd´ r´0 ofs, biglow_thread_yield_spec
                                       labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
                                       #EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) = Some (labd´, r´0)
                                     ∧ relate_AbData s f habd´ labd´
                                     ∧ (∀ i r,
                                           ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
                                     ∧ 0 ≤ ofs < num_proc
                                     ∧ ZMap.get ofs (kctxt labd) = r´0.
        Proof.
          Opaque remove.
          unfold big_thread_yield_spec, biglow_thread_yield_spec; intros until f.
          intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          subrewrite´. intros HCPU_range Hcid Hhigh.           subdestruct; contra_inv.
          inv Hhigh.
          pose proof multi_log_re0 as Hrel_log´.
          inv multi_log_re0.
          exploit (Hrel_log lock_range); eauto.
          intros (l0 & Hget0 & Hrel0).
          rewrite Hget0.
          pose proof multi_oracle_re0 as Horacle0.
          inv Horacle0.
          exploit (Hrel lock_range); eauto.
          intros Horacle0. clear Hrel.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          assert (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l) →
                             cid´ ≠ current_CPU_ID).
          {
            
            eapply valid_big_oracle; eauto.
          }
          rewrite <- HCPU in ×.
          erewrite <- CALTCB_BigLog; eauto.
          - instantiate (1:= (TBEVENT current_CPU_ID
                                      (TBSHARED (BTDYIELD (ZMap.get current_CPU_ID (cid labd))))
                                      :: big_oracle habd current_CPU_ID l ++ l)).
            rewrite Hdestruct6.
            rewrite zle_lt_true; trivial. rewrite Hdestruct9.
            refine_split´; eauto.
            + econstructor; eauto; simpl.
              × congruence.
              × eapply relate_big_small_log_pool_e_gss; eauto.
                intros. simpl.
                destruct (zeq abid lock_AT_start); trivial.
                rewrite zeq_false; eauto.
              × kctxt_inj_simpl.
            + intros. eapply kctxt_re0; eauto.
          - apply BigLogMap2id_alt in Horacle0.
            apply BigLogMap2id_alt; simpl; rewrite Horacle0; auto.
        Qed.

        Definition head_id (l : MultiLog) (i : Z) :=
          match l with
            | TEVENT i´ _ :: _ ⇒ i´ = i
            | _ ⇒ False
          end.


        Lemma biglow_proc_create_exist:
          ∀ (s : stencil) habd habd´ (labd : RData) b b´ buc ofs´ q n
                 (HINV: PBThread.high_level_invariant habd) f,
            big_proc_create_spec habd b buc b´ ofs´ q = Some (habd´, n)
            → relate_AbData s f habd labd
            → find_symbol s STACK_LOC = Some b
            → find_symbol s START_USER_FUN_LOC = Some buc
            → (∃ id, find_symbol s id = Some b´)
            → inject_incr (Mem.flat_inj (genv_next s)) f
            → ∃ labd´, biglow_proc_create_spec labd b buc b´ ofs´ q = Some (labd´, n)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_proc_create_spec, biglow_proc_create_spec.
          Locate biglow_proc_create_spec.
          intros until f; intros HP HR Hsys Huser Hsys´ Hincr.
          pose proof HR as HR´. inv HR´. revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          subrewrite´. intros HCPU_range Hcid Hhigh.
          subrewrite´. subdestruct; contra_inv.
          inv Hhigh.
          pose proof multi_log_re0 as Hrel_log´.
          inv multi_log_re0.
          exploit (Hrel_log lock_range); eauto.
          intros (l1 & Hget0 & Hrel0).
          rewrite Hget0.
          pose proof multi_oracle_re0 as Horacle0.
          inv Horacle0.
          exploit (Hrel lock_range); eauto.
          intros Horacle0. clear Hrel.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          assert (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l0) →
                             cid´ ≠ current_CPU_ID).
          {
            
            eapply valid_big_oracle; eauto.
          }
          rewrite <- HCPU in ×.
          erewrite <- CALTCB_BigLog.
          - instantiate (1:=
                           (TBEVENT current_CPU_ID
                                    (TBSHARED
                                       (BTDSPAWN (ZMap.get current_CPU_ID (cid labd))
                                                 (ZMap.get current_CPU_ID (cid labd) × 8 + 1 +
                                                  Z.of_nat
                                                    (length
                                                       (cchildren
                                                          (ZMap.get
                                                             (ZMap.get current_CPU_ID (cid labd))
                                                             (AC labd))))) q
                                                 (Int.repr
                                                    ((ZMap.get current_CPU_ID (cid labd) × 8 + 1 +
                                                      Z.of_nat
                                                        (length
                                                           (cchildren
                                                              (ZMap.get
                                                                 (ZMap.get current_CPU_ID
                                                                           (cid labd))
                                                                 (AC labd)))) + 1) × 4096 - 4))
                                                 b´ ofs´))
                                    :: big_oracle habd current_CPU_ID l0 ++ l0)).
            rewrite Hdestruct9.
            refine_split´; eauto.
            econstructor; eauto; simpl.
            + congruence.
            + rewrite <- (app_nil_l (big_oracle habd current_CPU_ID l0)).
              rewrite <- (app_nil_l (ZMap.get lock_range (multi_oracle labd) current_CPU_ID l1)).
              rewrite (app_comm_cons _ l0), (app_comm_cons _ l1).
              rewrite 2 (app_comm_cons nil).
              rewrite <- 2 app_assoc.
              apply relate_big_small_log_pool_gss; auto.
              { discriminate. }
              { destruct 1 as [Hcase|Hcase]; inv Hcase; auto. }
              { apply BigLogMap2id_alt; auto. }
              { destruct 2 as [Hcase|Hcase]; inv Hcase; simpl; cases; auto; omega. }
              { destruct 1 as [Hcase|Hcase]; inv Hcase; simpl; split; [discriminate | auto..]. }
            + kctxt_inj_simpl.
              {
                destruct Hsys´ as [id´ Hsys´].
                eapply stencil_find_symbol_inject´; eauto.
              }
              { rewrite Int.add_zero; trivial. }
              { eapply stencil_find_symbol_inject´; eauto. }
              { rewrite Int.add_zero; trivial. }
              { eapply kctxt_re0; eauto.
                rewrite HCPU in ×.
                omega. }
            + rewrite HCPU in ×.
              clear HCPU.
              unfold uctxt_inj in uctxt_re0.
              unfold uctxt_inj.
              intros.
              case_eq (zeq i (ZMap.get (CPU_ID labd) (cid labd) × 8 + 1 +
                              Z.of_nat (length (cchildren (ZMap.get (ZMap.get (CPU_ID labd) (cid labd)) (AC labd))))));
                intros; subst.
              × rewrite ZMap.gss; auto.
                rewrite ZMap.gss; auto.
                val_inject_simpl.
                case_eq (zeq j 12); intros; subst.
                { repeat rewrite ZMap.gss.
                  destruct Hsys´ as [id´ Hsys´].
                  econstructor.
                  eapply stencil_find_symbol_inject´; eauto.
                  rewrite Int.add_zero; trivial. }
                case_eq (zeq j 14); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                case_eq (zeq j 15); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                case_eq (zeq j 16); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                case_eq (zeq j 13); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                case_eq (zeq j 9); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                case_eq (zeq j 8); intros; subst.
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gss.
                  constructor. }
                { rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto.
                  rewrite ZMap.gso; auto. }
              × rewrite ZMap.gso; auto.
                rewrite ZMap.gso; auto.
          - apply BigLogMap2id_alt in Horacle0.
            apply BigLogMap2id_alt; simpl; rewrite Horacle0; auto.
        Qed.


        Lemma biglow_thread_wakeup_exist:
          ∀ s habd habd´ labd i r
                 (HINV: PBThread.high_level_invariant habd) f,
            big_thread_wakeup_spec i habd = Some (habd´, r)
            → relate_AbData s f habd labd
            → ∃ labd´, biglow_thread_wakeup_spec i labd = Some (labd´, r)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_thread_wakeup_spec, biglow_thread_wakeup_spec.
          intros until f; intros HP HR.
          pose proof HR as HR´. inv HR´. revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          subrewrite´. intros HCPU_range Hcid Hhigh.
          subrewrite´.
          d5 subdestruct_one.
          destruct (big_log habd) eqn: Hlog; contra_inv.
          pose proof multi_log_re0 as Hrel_log´.
          inv multi_log_re0.
          exploit (Hrel_log lock_range); eauto.
          intros (l0 & Hget0 & Hrel0).
          rewrite Hget0.
          pose proof multi_oracle_re0 as Horacle0.
          inv Horacle0.
          exploit (Hrel lock_range); eauto.
          intros Horacle0. clear Hrel.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          assert (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l) →
                             cid´ ≠ current_CPU_ID) by (eapply valid_big_oracle; eauto).
          rewrite <- HCPU in ×.
          assert (Hbig: BigLogMap2id
                          (TBEVENT current_CPU_ID (TBSHARED (BTDWAKE (ZMap.get current_CPU_ID (cid labd)) i))
                                   :: big_oracle habd current_CPU_ID l ++ l) lock_range
                          (TEVENT current_CPU_ID (TSHARED (OTDWAKE i))
                                  :: ZMap.get lock_range (multi_oracle labd) current_CPU_ID l0 ++ l0)).
          {
            apply BigLogMap2id_alt in Horacle0.
            apply BigLogMap2id_alt; simpl; rewrite Horacle0; auto.
          }
          erewrite <- CALTCB_BigLog; eauto.
          subdestruct_one.
          subdestruct_one.
          subdestruct; inv Hhigh.
          - refine_split´; eauto.
            econstructor; eauto; simpl.
            + congruence.
            + eapply relate_big_small_log_pool_e_gss; eauto.
              intros. simpl.
              destruct (zeq abid lock_AT_start); trivial.
              rewrite zeq_false; eauto.
          - refine_split´; eauto.
            econstructor; eauto; simpl.
            + congruence.
            + eapply relate_big_small_log_pool_e_gss; eauto.
              intros. simpl.
              destruct (zeq abid lock_AT_start); trivial.
              rewrite zeq_false; eauto.
          - erewrite <- CALTCB_BigLog.
            instantiate (1:= (TBEVENT current_CPU_ID
                                      (TBSHARED (BTDWAKE_DIFF (ZMap.get current_CPU_ID (cid labd)) i wk_id cpu_id))
                                      :: TBEVENT current_CPU_ID (TBSHARED (BTDWAKE (ZMap.get current_CPU_ID (cid labd)) i))
                                      :: big_oracle habd current_CPU_ID l ++ l)).
            erewrite Hdestruct7.
            refine_split´; eauto.
            econstructor; eauto; simpl.
            + congruence.
            + rewrite <- (app_nil_l (big_oracle habd current_CPU_ID l)).
              rewrite <- (app_nil_l (ZMap.get lock_range (multi_oracle labd) current_CPU_ID l0)).
              rewrite (app_comm_cons _ l), (app_comm_cons _ l0).
              rewrite 2 (app_comm_cons nil).
              rewrite <- 2 app_assoc.
              rewrite (app_comm_cons _ (big_oracle habd current_CPU_ID l ++ l)).
              rewrite (app_comm_cons _ (ZMap.get lock_range (multi_oracle labd) current_CPU_ID l0 ++ l0)).
              apply relate_big_small_log_pool_gss; auto; [discriminate|..].
              { destruct 1 as [Hcase|[Hcase|Hcase]]; inv Hcase; auto. }
              { apply BigLogMap2id_alt; auto. }
              {
                intros ? ? Habid.
                destruct 1 as [Hcase|[Hcase|Hcase]]; inv Hcase; simpl.
                × rewrite (zeq_false _ _ _ _ _ Habid).
                  destruct (zeq abid lock_AT_start); auto.
                × rewrite (zeq_false _ _ _ _ _ Habid).
                  destruct (zeq abid lock_AT_start); auto.
              }
              { destruct 1 as [Hcase|[Hcase|Hcase]]; inv Hcase; simpl; split; auto; discriminate. }
            + apply BigLogMap2id_alt in Horacle0.
              apply BigLogMap2id_alt. simpl. rewrite Horacle0; auto.
        Qed.

        Ltac rewrites :=
          repeat match goal with
                   | H: ?a = _ |- context [if ?a then _ else _] ⇒ rewrite H
                   | H: _ = ?a |- context [if ?a then _ else _] ⇒ rewrite <- H
                   | H: ?a = _ |- context [match ?a with _ ⇒ _ end] ⇒ rewrite H
                   | H: _ = ?a |- context [match ?a with _ ⇒ _ end] ⇒ rewrite <- H
                 end.

        Lemma SC_range_alt:
          ∀ i,
            lock_TCB_range ≤ i < lock_TCB_range + num_chan ↔
            ∃ ofs, index2Z ID_SC ofs = Some i.
        Proof.
          unfold index2Z, index_range, index_incrange.
          intros; split; intros.
          - ∃ (i - lock_TCB_range); cases.
            f_equal; omega.
            unfold ID_SC_range in *; omega.
          - destruct H as [ofs Heq].
            destruct (zle_lt 0 ofs ID_SC_range); [|inv Heq].
            Local Opaque lock_TCB_range.
            inversion Heq; subst.
            unfold ID_SC_range in *; omega.
            Local Transparent lock_TCB_range.
        Qed.

        Lemma biglow_sched_init_exist:
          ∀ s habd habd´ labd i
                 (HINV: PBThread.high_level_invariant habd) f,
            big_sched_init_spec i habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, biglow_sched_init_spec i labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_sched_init_spec, biglow_sched_init_spec.
          intros until f; intros HP HR.
          pose proof HR as HR´. inv HR´. revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          intros HCPU_range Hcid Hhigh.
          subdestruct; inv Hhigh.
          rewrite ioapic_re0; rewrites.
          refine_split´; eauto.
          constructor; simpl; try congruence; auto.
          constructor.
          intros abid Habid; ∃ nil; split.
          - assert (0 ≤ abid < lock_range+1).
            {
              rewrite <- SC_range_alt in Habid.
              unfold lock_range, lock_AT_start, lock_SC_start, lock_TCB_range,
                     ID_AT_range, ID_TCB_range, ID_SC_range in *; omega.
            }
            unfold real_multi_log´; rewrite <- (Z2Nat.id abid); [|omega].
            apply CalTicketLock.real_multi_log_pb_in.
            split.
            + rewrite Nat2Z.inj_le.
              rewrite Z2Nat.id; simpl; omega.
            + rewrite Nat2Z.inj_lt.
              rewrite 2 Z2Nat.id; omega.
          - econstructor; [constructor|auto].
        Qed.

        Local Transparent B_CalLock.
        Local Transparent H_CalLock.

        Lemma CalLock_rel:
          ∀ bl lid v,
            lock_TCB_range ≤ lid < lock_TCB_range + num_chan →
            B_CalLock lid bl = Some v →
            H_CalLock (BigLogMap2id_fun bl lid) = Some v.
        Proof.
          induction bl; simpl; intros; auto; rename H0 into Hcal.
          destruct a as [i e].
          destruct (B_CalLock lid bl) as [[[? ?] ?]|] eqn:Heq; [|inv Hcal].
          destruct e; simpl.
          - destruct (zeq lid lock_id); subst.
            + subdestruct_one.
              destruct (zeq lock_id lock_AT_start), (zeq lock_id lock_range); subst;
                unfold lock_range, lock_AT_start, lock_TCB_range,
                       ID_AT_range, ID_TCB_range, ID_SC_range in *; try omega.
              destruct e; simpl; erewrite IHbl; eauto; simpl; subdestruct; inv Hcal; auto;
              rewrite zeq_true; auto.
            + subdestruct; inv Hcal; cases; simpl; erewrite IHbl; eauto.
          - unfold lock_range, lock_AT_start, lock_TCB_range,
                   ID_AT_range, ID_TCB_range, ID_SC_range in ×.
              rewrite zeq_false; [|omega].
              rewrite zeq_false; [|omega].
              destruct e; simpl in *; try erewrite IHbl; eauto.
            + subdestruct; inv Hcal; erewrite IHbl; eauto; simpl.
              repeat rewrite zeq_true. trivial.
            + subdestruct; inv Hcal; erewrite IHbl; eauto; simpl.
              repeat rewrite zeq_true. trivial.
        Qed.

        Definition head_wait_lock (l : MultiLog) (i : Z) :=
          match l with
            | TEVENT i1 (TSHARED OPULL) :: TEVENT i2 (TTICKET (WAIT_LOCK _)) :: _ ⇒
              i1 = i ∧ i2 = i
            | TEVENT i1 (TSHARED (OBUFFERE _)) :: _ ⇒
              i1 = i
            | _ ⇒ False
          end.

        Lemma B_CalLock_hold:
          ∀ l lid n i,
            lock_TCB_range ≤ lid < lock_TCB_range + num_chan →
            B_CalLock lid l = Some (n, LHOLD, Some i) →
            head_wait_lock (BigLogMap2id_fun l lid) i.
        Proof.
          induction l; simpl; intros lid n i Hrange Hcal; [inv Hcal|].
          assert (lid ≠ lock_AT_start)
            by (unfold lock_TCB_range, ID_AT_range, ID_TCB_range, lock_AT_start in *; omega).
          assert (lid ≠ lock_range)
            by (unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range,
                       ID_TCB_range, ID_SC_range in *; omega).
          destruct a as [i´ e]; destruct (B_CalLock lid l) as [[[? ?] ?]|] eqn:Hcal´; [|inv Hcal].
          destruct e.
          - d2 subdestruct_one; subst.
            + rewrite 2 zeq_false; auto.
              destruct e; simpl; subdestruct; inv Hcal; auto.
            + rewrite 2 zeq_false; auto; inv Hcal; simpl; eauto.
          - destruct e; simpl; try solve [inv Hcal; rewrite zeq_false; auto; cases; simpl; eauto].
            + rewrite 2 zeq_false; auto.
              subdestruct; inv Hcal; eauto.
            + rewrite 2 zeq_false; auto.
              subdestruct; inv Hcal; eauto.
        Qed.

        Lemma head_remove_cache_event:
          ∀ l i,
            head_wait_lock l i → remove_cache_event l i = l.
        Proof.
          destruct l; simpl; intros; auto.
          subdestruct; try contradiction.
          - destruct H; subst.
            subst; rewrite zeq_true; auto.
          - destruct H; subst.
            subst; rewrite zeq_true; auto.
        Qed.

        Lemma release_lock_SC_exist:
          ∀ s habd habd´ labd i
                 (HINV: PBThread.high_level_invariant habd) f,
            big_release_lock_SC_spec i habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, release_lock_SC_spec i labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_release_lock_SC_spec, release_lock_SC_spec.
          intros until f; intros HP HR.
          pose proof HR as HR´. inv HR´. revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          intros HCPU_range Hcid Hhigh.
          d4 subdestruct_one.
          rewrites.
          destruct (big_log habd) eqn:Heq; [inv Hhigh|].
          assert (Hi: (i + lock_TCB_range) = 0 ∨ (i + lock_TCB_range) = lock_range ∨
                         (∃ ofs : Z, index2Z 2 ofs = Some (i + lock_TCB_range)))
            by (right; right; apply SC_range_alt; omega).
          assert (HCPU: current_CPU_ID = CPU_ID labd)
            by (apply valid_CPU_ID_eq in HINV; congruence).
          assert (oracle_re:= multi_oracle_re0); assert (log_re:= multi_log_re0).
          inv multi_log_re0; inv multi_oracle_re0.
          destruct (Hrel_log _ Hi) as [l´ [? Hrel_log´]].
          specialize (Hrel _ _ _ Hi Hrel_log´).
          rewrite <- lock_re0; rewrites.
          destruct (ZMap.get (i + lock_TCB_range) (lock habd)) eqn:HLock; contra_inv.
          destruct b eqn:Hb; contra_inv.
          destruct (B_CalLock (i + lock_TCB_range) l) as [[[? ?] ?]|] eqn:Hcal; [|inv Hhigh].
          subdestruct_one; rewrite zeq_true in Hhigh.
          assert (Hbcal:=Hcal); apply CalLock_rel in Hcal; [|omega].
          apply BigLogMap2id_alt in Hrel.
          subdestruct; inv Hhigh.
          inv Hrel_log´.
          apply BigLogMap2id_alt in Hlogmap; subst.
          apply B_CalLock_hold in Hbcal; auto.
          rewrite CPU_ID_re0, <- HCPU in Hbcal.
          rewrite (head_remove_cache_event _ _ Hbcal) in *; rewrites.
          rewrite CPU_ID_re0, 2 zeq_true.
          refine_split´; eauto.
          constructor; simpl; auto; try congruence.
          constructor; intros abid Habid.
          destruct (zeq abid (i + lock_TCB_range)); subst.
          - rewrite ZMap.gss.
            refine_split´; eauto.
            econstructor.
            + apply BigLogMap2id_alt; simpl.
              rewrite 2 zeq_false.
              rewrite zeq_true; reflexivity.
              unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range,
                     ID_TCB_range, ID_SC_range in *; omega.
              unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range,
                     ID_TCB_range, ID_SC_range in *; omega.
            + simpl.
              rewrite HCPU, zeq_true; congruence.
          - rewrite ZMap.gso; auto.
            destruct (Hrel_log _ Habid) as [l´ [Hget Hrel´]]; ∃ l´; split; auto.
            econstructor.
            + apply BigLogMap2id_alt; simpl.
              cases; auto; omega.
            + inv Hrel´.
              apply BigLogMap2id_alt in Hlogmap; subst; auto.
        Qed.

        Lemma BigLogMap2id_fun_In:
          ∀ l cid e abid,
            In (TEVENT cid e) (BigLogMap2id_fun l abid) →
            ∃ e´, In (TBEVENT cid e´) l.
        Proof.
          induction l; simpl; intros. inv H.
          destruct a. simpl in H.
          destruct e0.
          - subdestruct; try inv H; try (exploit IHl; eauto; intros (e´ & Hin); esplit; right; eauto; fail);
            try (inv H0; esplit; left; eauto; fail).
            + inv H0.
              × inv H; esplit; left; eauto.
              × exploit IHl; eauto.
                intros (e´ & Hin). esplit; right; eauto.
            + inv H0.
              × inv H; esplit; left; eauto.
              × exploit IHl; eauto.
                intros (e´ & Hin). esplit; right; eauto.

          - subdestruct; try inv H; try (exploit IHl; eauto; intros (e´ & Hin); esplit; right; eauto; fail);
            try (inv H0; esplit; left; eauto; fail).
            inv H0.
            + inv H; esplit; left; eauto.
            + exploit IHl; eauto.
              intros (e´ & Hin). esplit; right; eauto.
        Qed.

        Lemma B_CalLock_gso:
          ∀ bl tl p n cpu id,
            B_CalLock id (bl ++ tl) = Some p →
            B_CalLock id tl = Some (n, LHOLD, Some cpu) →
            (∀ e cid´, In (TBEVENT cid´ e) bl → cid´ ≠ cpu) →
            id ≠ lock_AT_start →
            id ≠ lock_range →
            BigLogMap2id_fun bl id = nil ∧ (∃ n´, p = (n´, LHOLD, Some cpu)).
        Proof.
          induction bl; intros; trivial.
          {
            simpl in H. rewrite H in H0. inv H0. eauto.
          }
          simpl in H. destruct a.
          subdestruct_one. repeat destruct p0.
          assert (Hl: ∀ e cid´, In (TBEVENT cid´ e) bl → cid´ ≠ cpu).
          {
            intros. eapply H1. right. eauto.
          }
          repeat rewrite zeq_false; trivial.
          destruct e.
          - subdestruct; subst;
            exploit IHbl; eauto;
            intros (Hl´ & (n´ & Heq));
            inv Heq.
            + exploit H1; eauto;
              [left; trivial| intro HF; inv HF].
            + inv H; eauto.
          - subdestruct; subst;
            inv H; exploit IHbl; eauto;
            intros (Hl´ & (n´ & Heq)); inv Heq.

            + exploit H1; eauto.
              left; trivial. intro HF; inv HF.
            + exploit H1; eauto.
              left; trivial. intro HF; inv HF.
        Qed.

        Lemma biglow_thread_sleep_exist:
          ∀ habd habd´ labd rs r´ rs0 n s
                 (HINV: PBThread.high_level_invariant habd) f,
            big_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´, rs0)
            → relate_AbData s f habd labd
            
            → (∀ reg : PregEq.t,
                  val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
            → ∃ labd´ r´0 ofs, biglow_thread_sleep_spec
                                       labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
                                       #EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) n = Some (labd´, r´0)
                                     ∧ relate_AbData s f habd´ labd´
                                     ∧ (∀ i r,
                                           ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
                                     ∧ 0 ≤ ofs < num_proc
                                     ∧ ZMap.get ofs (kctxt labd) = r´0.
        Proof.
          Opaque remove.
          unfold big_thread_sleep_spec, biglow_thread_sleep_spec; intros until f.
          intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          subrewrite´. intros HCPU_range Hcid Hhigh.           subdestruct; contra_inv.
          inv Hhigh.
          pose proof multi_log_re0 as Hrel_log´.
          inv multi_log_re0.
          exploit (Hrel_log lock_range); eauto.
          intros (l0 & Hget0 & Hrel0).
          rewrite Hget0.
          pose proof multi_oracle_re0 as Horacle0.
          inv Horacle0.
          exploit (Hrel lock_range); eauto.
          intros Horacle0.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          assert (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) (big_oracle habd current_CPU_ID l) →
                             cid´ ≠ current_CPU_ID).
          {
            
            eapply valid_big_oracle; eauto.
          }
          rewrite <- HCPU in ×.
          erewrite <- CALTCB_BigLog; eauto.
          - instantiate (1:= (TBEVENT current_CPU_ID
                                      (TBSHARED
                                         (BTDSLEEP (ZMap.get current_CPU_ID (cid labd)) n
                                                   (syncchpool labd)))
                                      :: big_oracle habd current_CPU_ID l ++ l)).
            subrewrite´.
            assert (Hi: (slp_q_id n 0 + lock_TCB_range) = 0 ∨ (slp_q_id n 0 + lock_TCB_range) = lock_range ∨
                        (∃ ofs : Z, index2Z 2 ofs = Some (slp_q_id n 0 + lock_TCB_range))).
            {
              right; right. apply SC_range_alt. unfold slp_q_id. omega.
            }
            destruct (Hrel_log _ Hi) as [l´ [-> Hrel_log´´]].
            specialize (Hrel _ _ _ Hi Hrel_log´´).
            assert (Hr: lock_TCB_range ≤ slp_q_id n 0 + lock_TCB_range < lock_TCB_range + num_chan).
            {
              unfold slp_q_id; omega.
            }
            exploit B_CalLock_hold; eauto. rewrite <- HCPU in ×.
            intros Hhead.
            eapply head_remove_cache_event in Hhead.
            pose proof Hdestruct14 as HBCal.
            eapply CalLock_rel in Hdestruct14; eauto.
            inv Hrel_log´´.
            apply BigLogMap2id_alt in Hlogmap. rewrite Hlogmap in ×.
            rewrite Hhead in ×.
            rewrite Hdestruct14.
            repeat rewrite zeq_true.
            refine_split´; eauto.
            + econstructor; eauto; simpl.
              × congruence.
              × constructor.
                intros.
                assert (HIn: ∀ e cid´,
                               In (TEVENT cid´ e)
                                  (BigLogMap2id_fun (big_oracle habd current_CPU_ID l) abid) →
                               cid´ ≠ current_CPU_ID).
                {
                  intros.
                  exploit BigLogMap2id_fun_In; eauto.
                  intros (e´ & HIn).
                  eapply Horacle; eauto.
                }
                assert (Hneq1: slp_q_id n 0 + lock_TCB_range ≠ lock_AT_start).
                {
                  unfold slp_q_id, lock_TCB_range, lock_AT_start.
                  unfold ID_AT_range, ID_TCB_range, ID_SC_range.
                  omega.
                }
                assert (Hneq2: slp_q_id n 0 + lock_TCB_range ≠ lock_range).
                {
                  unfold slp_q_id, lock_TCB_range, lock_range.
                  unfold ID_AT_range, ID_TCB_range, ID_SC_range.
                  omega.
                }
                destruct (zeq abid (slp_q_id n 0 + lock_TCB_range)); subst.
                {
                  rewrite ZMap.gss.
                  refine_split´; trivial.
                  econstructor.
                  - apply BigLogMap2id_alt.
                    apply BigLogMap2id_alt in Hrel.
                    simpl. rewrite Hrel.
                    rewrite zeq_false; trivial.
                  - simpl. rewrite zeq_false; trivial. rewrite zeq_true. simpl.
                    repeat rewrite zeq_true.
                    f_equal.
                    f_equal.
                    apply BigLogMap2id_alt in Hrel.
                    rewrite BigLogMap2id_fun_app in Hrel.
                    set (tl:= BigLogMap2id_fun l (slp_q_id n 0 + lock_TCB_range)) in ×.
                    rewrite <- Hrel.
                    assert (Heq: BigLogMap2id_fun (big_oracle habd current_CPU_ID l)
                                                  (slp_q_id n 0 + lock_TCB_range) = nil).
                    {
                      exploit B_CalLock_gso; eauto.
                      intros ( → & _). trivial.
                    }
                    rewrite Heq; trivial.
                }
                {
                  rewrite ZMap.gso; eauto.
                  destruct (zeq abid lock_range); subst.
                  {
                    rewrite ZMap.gss. refine_split´; eauto.
                    econstructor; eauto.
                    apply BigLogMap2id_alt.
                    apply BigLogMap2id_alt in Horacle0.
                    simpl. rewrite Horacle0. trivial.
                    simpl. rewrite zeq_true. trivial.
                  }
                  {
                    rewrite ZMap.gso; eauto.
                    exploit Hrel_log; eauto.
                    intros (l1 & Hgetl1 & Hrel1).
                    refine_split; eauto.
                    inv Hrel1. econstructor.
                    instantiate (1:= BigLogMap2id_fun (big_oracle habd current_CPU_ID l ++ l) abid).
                    - apply BigLogMap2id_alt. simpl.
                      destruct (zeq abid lock_AT_start); subst. trivial.
                      rewrite zeq_false; trivial.
                      rewrite zeq_false; trivial.
                    - rewrite BigLogMap2id_fun_app.
                      apply BigLogMap2id_alt in Hlogmap.
                      rewrite Hlogmap.
                      erewrite remove_cache_event_gso; eauto.
                  }
                }
                
              × kctxt_inj_simpl.
            + intros. eapply kctxt_re0; eauto.
          - apply BigLogMap2id_alt in Horacle0.
            apply BigLogMap2id_alt; simpl; rewrite Horacle0; auto.
        Qed.

        Lemma GetSharedSC_rel:
          ∀ bl lid,
            lock_TCB_range ≤ lid < lock_TCB_range + num_chan →
            B_GetSharedSC lid bl = GetSharedSC (BigLogMap2id_fun bl lid).
        Proof.
          induction bl; simpl; intros; auto.
          destruct a as [i e]; rewrite IHbl; auto; destruct e; auto.
          - destruct e; simpl; try solve [cases; simpl; cases; auto].
            unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
            destruct (zeq lid 0); subst; [omega|].
            destruct (zeq lid (1 + num_chan + num_chan)); subst; [omega|].
            cases; simpl; cases; auto.
          - destruct e; simpl; try solve [cases; simpl; cases; auto].
            unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
            destruct (zeq lid 0); subst; [omega|].
            destruct (zeq lid (1 + num_chan + num_chan)); subst; [omega|].
            destruct (zeq lid (slp_q_id cv_id 0 + (1 + num_chan))); subst; auto.
        Qed.

        Lemma relate_big_small_log_pool_e_gss´:
          ∀ bl bl´ ml id be me1 me2 l l´
                 (Hrel: relate_big_small_log_pool (BigDef bl) ml)
                 (Hmap: BigLogMap2id (bl´ ++ bl) id (l´ ++ l))
                 (Hneq: ∀ abid,
                          abid ≠ id →
                          BigE2id (TBEVENT current_CPU_ID be) abid = nil)
                 (Horacle: ∀ e cid´,
                             In (TBEVENT cid´ e) bl´ → cid´ ≠ current_CPU_ID)
                 (He: BigE2id (TBEVENT current_CPU_ID be) id =
                      TEVENT current_CPU_ID me1 :: TEVENT current_CPU_ID me2 :: nil),
            relate_big_small_log_pool
              (BigDef
                 (TBEVENT current_CPU_ID be :: bl´ ++ bl))
              (ZMap.set id
                        (MultiDef
                           (TEVENT current_CPU_ID me1 ::TEVENT current_CPU_ID me2 :: l´ ++ l)) ml).
        Proof.
          intros.
          rewrite (append_rewrite _ (bl´++bl)), (append_rewrite _ (l´++l)).
          rewrite app_comm_cons.
          apply relate_big_small_log_pool_gss; auto.
          - discriminate.
          - destruct 1 as [Hcase|Hcase]; inv Hcase; auto.
          - apply BigLogMap2id_alt.
            unfold BigLogMap2id_fun; fold BigLogMap2id_fun; rewrite He; auto.
          - destruct 2 as [Hcase|Hcase]; inv Hcase; auto.
          - destruct 1 as [Hcase|Hcase]; inv Hcase; rewrite He.
            split; [discriminate | simpl; auto].
        Qed.

        Lemma acquire_lock_SC_exist:
          ∀ s habd habd´ labd i
                 (HINV: PBThread.high_level_invariant habd) f,
            big_acquire_lock_SC_spec i habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, acquire_lock_SC_spec i labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold big_acquire_lock_SC_spec, acquire_lock_SC_spec.
          intros until f; intros HP HR.
          pose proof HR as HR´. inv HR´. revert HP.
          specialize (PBThread.CPU_ID_range _ HINV).
          specialize (PBThread.valid_curid _ HINV).
          intros HCPU_range Hcid Hhigh.
          d3 subdestruct_one.
          rewrites.
          destruct (big_log habd) eqn:Heq; [inv Hhigh|].
          assert (Hi: (i + lock_TCB_range) = 0 ∨ (i + lock_TCB_range) = lock_range ∨
                         (∃ ofs : Z, index2Z 2 ofs = Some (i + lock_TCB_range)))
            by (right; right; apply SC_range_alt; omega).
          assert (HCPU: current_CPU_ID = CPU_ID labd)
            by (apply valid_CPU_ID_eq in HINV; congruence).
          assert (oracle_re:= multi_oracle_re0); assert (log_re:= multi_log_re0).
          inv multi_log_re0; inv multi_oracle_re0.
          destruct (Hrel_log _ Hi) as [l´ [? Hrel_log´]].
          specialize (Hrel _ _ _ Hi Hrel_log´).
          rewrite <- lock_re0; rewrites.
          subdestruct_one.
          destruct (B_CalLock (i + lock_TCB_range)
                       (big_oracle habd (CPU_ID habd) l ++ l)) as [[[? ?] ?]|] eqn:Hcal; [|inv Hhigh].
          subdestruct_one; rewrite zeq_true in Hhigh.
          apply CalLock_rel in Hcal; [|omega].
          apply BigLogMap2id_alt in Hrel.
          unfold MultiOracle, MultiLog in *; rewrite <- HCPU, <- Hrel.
          rewrite CPU_ID_re0, <- HCPU in Hcal; rewrite Hcal.
          rewrite <- GetSharedSC_rel; [|omega].
          rewrite CPU_ID_re0, <- HCPU in Hhigh.
          assert (Hrel_pool: relate_big_small_log_pool
                            (BigDef
                               (TBEVENT current_CPU_ID
                                        (TBLOCK (i + lock_TCB_range) (BWAIT_LOCK (ZMap.get current_CPU_ID (cid habd))
                                                                                 local_lock_bound))
                                        :: big_oracle habd current_CPU_ID l ++ l))
                            (ZMap.set (i + lock_TCB_range)
                                      (MultiDef
                                         (TEVENT current_CPU_ID (TSHARED OPULL) ::
                                           TEVENT current_CPU_ID (TTICKET (WAIT_LOCK (local_lock_bound)))
                                                 :: BigLogMap2id_fun (big_oracle habd current_CPU_ID l ++ l)
                                                 (i + lock_TCB_range))) (multi_log labd))).
          {
            rewrite BigLogMap2id_fun_app.
            eapply relate_big_small_log_pool_e_gss´; auto.
            - apply BigLogMap2id_alt; apply BigLogMap2id_fun_app.
            - simpl; intros ? Hneq; rewrite (zeq_false _ _ _ _ _ Hneq); cases; auto.
            - apply valid_big_oracle; auto.
            - simpl; rewrite zeq_true.
              unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
              cases; auto; omega.
          }
          subdestruct; inv Hhigh; repeat rewrite zeq_true; refine_split´; eauto;
          constructor; simpl; auto; try congruence.
        Qed.


        Lemma page_copy_exist:
          ∀ s habd habd´ labd index i from f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_page_copy_spec index i from habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, page_copy_spec index i from labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold page_copy_spec, big_page_copy_spec; intros.
          inversion H0.
          revert H. subrewrite.
          d3 subdestruct_one; contra_inv.
          destruct (index2Z 2 (slp_q_id index 0)) eqn:Hindex; contra_inv.
          assert (Heq: slp_q_id index 0 + lock_TCB_range = z).
          {
            functional inversion Hindex. functional inversion H2. omega.
          }
          rewrite Heq in ×.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          d3 subdestruct_one; contra_inv.
          destruct (ZMap.get (PageI from) (pperm labd)) eqn:Hperm; contra_inv.
          destruct (big_log habd) eqn:Hlog; contra_inv.
          destruct (ZMap.get z (lock labd)) eqn:Hlock; contra_inv.
          destruct b; contra_inv.
          destruct (page_copy_aux (Z.to_nat i) from (HP habd)) eqn:Hcopy; contra_inv.
          destruct (B_CalLock z l) eqn:Hcall; contra_inv.
          destruct p. destruct p.
          d1 subdestruct_one; contra_inv.
          rewrite zeq_true in HQ.
          subdestruct. inv HQ.
          pose proof multi_log_re0 as multi_log_re´.
          inv multi_log_re0. specialize (Hrel_log (slp_q_id index 0 + lock_TCB_range)).
          exploit Hrel_log. right. right. eauto.
          intros (l1 & Hmulti & Hrel). rewrite Hmulti.
          exploit page_copy_aux_exists; eauto.
          intros Hpage. rewrite Hpage.
          inv Hrel.
          assert (Hrange: lock_TCB_range ≤ slp_q_id index 0 + lock_TCB_range < lock_TCB_range + num_chan).
          {
            unfold slp_q_id.
            unfold lock_TCB_range, lock_AT_start, ID_AT_range,
            ID_TCB_range, ID_SC_range in *; omega.
          }
          exploit CalLock_rel; eauto.
          exploit B_CalLock_hold; eauto.
          intros Hhead Hcal.
          eapply head_remove_cache_event in Hhead.
          rewrite <- Hhead in Hcal.
          rewrite BigLogMap2id_alt in Hlogmap.
          rewrite Hlogmap in ×. rewrite <- HCPU in ×.
          rewrite Hcal. rewrite zeq_true.
          refine_split´; try trivial.
          constructor; simpl; auto; try congruence.
          constructor; intros abid Habid.
          destruct (zeq abid (slp_q_id index 0 + lock_TCB_range)); subst.
          - rewrite ZMap.gss.
            refine_split´; eauto.
            econstructor.
            + apply BigLogMap2id_alt; simpl.
              rewrite 2 zeq_false.
              rewrite zeq_true; reflexivity.
              × unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range,
                     ID_TCB_range, ID_SC_range in *; omega.
              × unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range,
                     ID_TCB_range, ID_SC_range in *; omega.
            + simpl.
              rewrite HCPU, zeq_true; congruence.
          - rewrite ZMap.gso; auto.
            inv multi_log_re´.
            destruct (Hrel_log0 _ Habid) as [l´ [Hget Hrel´]]; ∃ l´; split; auto.
            econstructor.
            + apply BigLogMap2id_alt; simpl.
              cases; auto; omega.
            + inv Hrel´.
              apply BigLogMap2id_alt in Hlogmap; subst; auto.
        Qed.

        Lemma ipc_send_body_exist:
          ∀ s f habd habd´ labd chid vaddr count i
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ipc_send_body_spec chid vaddr count habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ipc_send_body_spec chid vaddr count labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold ipc_send_body_spec, big_ipc_send_body_spec. intros.
          generalize H0; intro relateD.
          inv H0.
          revert H. subrewrite.
          subdestruct; inv HQ.
          exploit page_copy_exist; eauto.
          intros (labd´ & Hpage & Hrel).
          rewrite Hpage.
          refine_split´; trivial.
          inv Hrel. econstructor; eauto.
          rewrite syncchpool_re1. trivial.
        Qed.

        Lemma ipc_send_body_sim :
          ∀ id,
            sim (crel RData RData) (id ↦ gensem big_ipc_send_body_spec)
                (id ↦ gensem ipc_send_body_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit ipc_send_body_exist; eauto 1; intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

        Lemma GetSharedBuffer_rel:
          ∀ bl lid,
            lock_TCB_range ≤ lid < lock_TCB_range + num_chan →
            B_GetSharedBuffer lid bl = GetSharedBuffer (BigLogMap2id_fun bl lid).
        Proof.
          induction bl; simpl; intros; auto.
          destruct a as [i e]; rewrite IHbl; auto; destruct e; auto.
          - simpl.
            unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
            destruct (zeq lid 0); subst; [omega|].
            destruct (zeq lid (1 + num_chan + num_chan)); subst; [omega|].
            cases; simpl; cases; auto.
          - destruct e; simpl; try solve [cases; simpl; cases; auto].
            unfold lock_range, lock_TCB_range, lock_AT_start, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
            destruct (zeq lid 0); subst; [omega|].
            destruct (zeq lid (1 + num_chan + num_chan)); subst; [omega|].
            destruct (zeq lid (slp_q_id cv_id 0 + (1 + num_chan))); subst; auto.
        Qed.

        Lemma page_copy_back_exist:
          ∀ s habd habd´ labd index i to f
                 (Hhigh: PBThread.high_level_invariant habd),
            big_page_copy_back_spec index i to habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, page_copy_back_spec index i to labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold page_copy_back_spec, big_page_copy_back_spec; intros.
          inversion H0.
          revert H. subrewrite.
          subdestruct. inv HQ.
          pose proof multi_log_re0 as multi_log_re´.
          inv multi_log_re0. specialize (Hrel_log z).
          exploit Hrel_log. right. right. eauto.
          intros (l1 & Hmulti & Hrel). rewrite Hmulti.
          inv Hrel.
          assert (Hrange: lock_TCB_range ≤ z < lock_TCB_range + num_chan).
          {
            functional inversion Hdestruct5. functional inversion H2.
            unfold slp_q_id in ×. functional inversion H1. subst.
            unfold ID_SC_range in ×. omega.
          }
          exploit (GetSharedBuffer_rel l); eauto.
          exploit B_CalLock_hold; eauto.
          intros Hhead Hcal.
          eapply head_remove_cache_event in Hhead.
          rewrite <- Hhead in Hcal.
          rewrite BigLogMap2id_alt in Hlogmap.
          rewrite Hlogmap in ×.
          assert (HCPU: current_CPU_ID = (CPU_ID labd)).
          {
            exploit valid_CPU_ID_eq; eauto. intros. congruence.
          }
          rewrite <- HCPU in ×.
          rewrite <- Hcal. rewrite Hdestruct10.
          exploit page_copy_back_aux_exists; eauto.
          intros (lh´ & Hback & Hinj). rewrite Hback.
          refine_split´; try trivial.
          econstructor; simpl; eauto. congruence. congruence.
        Qed.

        Lemma ipc_receive_body_exist:
          ∀ s f habd habd´ labd fromid vaddr count i
                 (Hhigh: PBThread.high_level_invariant habd),
            big_ipc_receive_body_spec fromid vaddr count habd = Some (habd´, i)
            → relate_AbData s f habd labd
            → ∃ labd´, ipc_receive_body_spec fromid vaddr count labd = Some (labd´, i)
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold ipc_receive_body_spec, big_ipc_receive_body_spec. intros.
          generalize H0; intro relateD.
          inv H0.
          revert H. subrewrite;
                    subdestruct; inv HQ;
                    try (refine_split´; trivial; fail).
          exploit page_copy_back_exist; eauto.
          intros (labd´ & Hmemcpy2 & Hmemcpy3).
          rewrite Hmemcpy2.
          exploit relate_impl_syncchpool_eq; eauto; intros.
          refine_split´; trivial.
          rewrite H.
          exploit relate_impl_syncchpool_update; eauto.
        Qed.

        Lemma ipc_receive_body_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem big_ipc_receive_body_spec)
                (id ↦ gensem ipc_receive_body_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
          exploit ipc_receive_body_exist; eauto 1; intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

      End Exists.

      Section PASSTHROUGH_PRIM.

        Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
        Proof.
          accessor_prop_tac.
          - eapply flatmem_store_exists; eauto.
        Qed.

        Lemma passthrough_correct:
          sim (crel HDATA LDATA) pbthread_passthrough vmxinit.
        Proof.
          sim_oplus.           - apply vmxinfo_get_sim.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            exploit palloc_exist; eauto 1. intros (labd´ & HP & HM).
            match_external_states_simpl.
          - apply setPT_sim.
          - apply ptRead_sim.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
            match_external_states_simpl.
          -
            intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
            exploit biglow_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
            match_external_states_simpl.

          -
            intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
            inv H. inv H0. inv match_extcall_states.
            exploit biglow_thread_yield_exist; eauto 1.
            intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
            inv LOW_LEVEL_INVARIANT.
            match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
            + eapply kctxt_INJECT; try assumption.
            + eapply kctxt_INJECT; try assumption.

          -
            intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
            inv H. inv H0. inv match_extcall_states.
            exploit biglow_thread_sleep_exist; eauto 1.
            intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
            inv LOW_LEVEL_INVARIANT.
            match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
            + inv H9. inv H2. 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.

          -
            intros. layer_sim_simpl.
            constructor; constructor; simpl; try constructor; auto.
            intros. inv_generic_sem H0; inv H2.
            exploit biglow_sched_init_exist; eauto 1.
            intros (? & ? & ?); refine_split; auto; [|match_external_states_simpl].
            repeat constructor; eassumption.

          - apply uctx_get_sim.
          - apply uctx_set_sim.
          -
            intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
            exploit biglow_proc_create_exist; eauto 1; intros (labd´ & HP & HM).
            destruct H9 as [fun_id Hsys].
            exploit stencil_find_symbol_inject´; eauto. intros HFB.
            match_external_states_simpl.

          - apply container_get_nchildren_sim.
          - apply container_get_quota_sim.
          - apply container_get_usage_sim.
          - apply container_can_consume_sim.

          - apply get_CPU_ID_sim.
          - apply get_curid_sim.

          -
            intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
            exploit acquire_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
            match_external_states_simpl.

          -
            intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
            exploit release_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
            match_external_states_simpl.

          - apply get_sync_chan_busy_sim.
          - apply set_sync_chan_busy_sim.

          - apply ipc_send_body_sim.
          - apply ipc_receive_body_sim.

          - apply rdmsr_sim.
          - apply wrmsr_sim.
          - apply vmx_set_intercept_intwin_sim.
          - apply vmx_set_desc1_sim.
          - apply vmx_set_desc2_sim.
          - apply vmx_inject_event_sim.
          - apply vmx_set_tsc_offset_sim.
          - apply vmx_get_tsc_offset_sim.
          - apply vmx_get_exit_reason_sim.
          - apply vmx_get_exit_fault_addr_sim.
          - apply vmx_get_exit_qualification_sim.
          - apply vmx_check_pending_event_sim.
          - apply vmx_check_int_shadow_sim.
          - apply vmx_get_reg_sim.
          - apply vmx_set_reg_sim.
          - apply vmx_get_next_eip_sim.
          - apply vmx_get_io_width_sim.
          - apply vmx_get_io_write_sim.
          - apply vmx_get_exit_io_rep_sim.
          - apply vmx_get_exit_io_str_sim.
          - apply vmx_get_exit_io_port_sim.
          - apply vmx_set_mmap_sim.
          - apply vm_run_sim, VMX_INJECT.
          - apply vmx_return_from_guest_sim.
          - apply vmx_init_sim.

          - apply cli_sim.
          - apply sti_sim.
          - apply serial_intr_disable_sim.
          - apply serial_intr_enable_sim.
          - apply serial_putc_sim.
          - apply cons_buf_read_sim.

          - apply hostin_sim.
          - apply hostout_sim.
          - apply proc_create_postinit_sim.
          - apply trap_info_get_sim.
          - apply trap_info_ret_sim.
          - apply proc_start_user_sim.
            intros; inv H; auto.
          - apply proc_exit_user_sim.
          - apply proc_start_user_sim2.
            intros; inv H; auto.
          - apply proc_exit_user_sim2.
          - layer_sim_simpl.
            + eapply load_correct3.
            + eapply store_correct3.
        Qed.

      End PASSTHROUGH_PRIM.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.