Library mcertikos.devdrivers.AbsConsoleBuffIntroGen


This file provide the contextual refinement proof between MPTInit layer and MPTBit 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 LoadStoreSem2.
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 AbstractDataType.
Require Import DeviceStateDataType.
Require Import CLemmas.
Require Import ListLemma.

Require Import AbsConsoleBuffIntroGenSpec.
Require Import DAbsConsoleBuffIntro.
Require Import LayerCalculusLemma.

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 `{oracle_prop: MultiOracleProp}.

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

  Notation HDATAOps := (cdata (cdata_ops := dabsconsolebuffintro_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) LDATA).

  Section WITHMEM.

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

Definition the refinement relation: relate_RData + match_RData

    Section REFINEMENT_REL.

Relation between the new raw data at the higher layer with the mememory at lower layer
        Inductive match_RData: stencilHDATAmemmeminjProp :=
        | MATCH_RDATA:
             hadt m f s,
              match_RData s hadt m f.


        Fixpoint match_buffer_list (buffer: list Z) (buffmap: ZMap.t ConsoleBufVal) (rpos wpos: Z) : Prop :=
          Z.of_nat (length buffer) < CONS_BUFFER_SIZE
          match buffer with
           | nilrpos = wpos
           | cons bv buffer´
               ZMap.get rpos buffmap = BufVal bv
               match_buffer_list buffer´ buffmap ((rpos + 1) mod CONS_BUFFER_SIZE) wpos
          end
        .

        Inductive match_Console: ConsoleDriverConcreteConsoleDriverProp :=
        | MATCH_CONSOLE:
             cdc cd,
              rpos_concrete cdc = rpos cd
              wpos_concrete cdc = (rpos cd + (Z.of_nat (length (cons_buf cd)))) mod CONS_BUFFER_SIZE
              match_buffer_list (cons_buf cd) (cons_buf_concrete cdc) (rpos_concrete cdc) (wpos_concrete cdc) →
              match_Console cdc cd.

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;
              MM_re: MM hadt = MM ladt;
              MMSize_re: MMSize hadt = MMSize ladt;
              CR3_re: CR3 hadt = CR3 ladt;
              ikern_re: ikern ladt = ikern hadt;
              pg_re: pg ladt = pg hadt;
              ihost_re: ihost ladt = ihost hadt;
              AC_re: AC ladt = AC hadt;
              ti_fst_re: (fst (ti ladt)) = (fst (ti hadt));
              ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
              LAT_re: LAT ladt = LAT hadt;
              nps_re: nps ladt = nps hadt;
              ipt_re: ipt ladt = ipt hadt;
              init_re: init ladt = init hadt;

              buffer_re: buffer hadt = buffer ladt;

              com1_re: com1 ladt = com1 hadt;
              ioapic_re: ioapic ladt = ioapic hadt;
              lapic_re: lapic ladt = lapic hadt;
              intr_flag_re: intr_flag ladt = intr_flag hadt;
              saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
              curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
              console_re: match_Console (console_concrete ladt) (console hadt);
              in_intr_re: in_intr hadt = in_intr ladt;
              tf_re: tfs_inj f (tf hadt) (tf ladt);

              CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
              cid_re: cid hadt = cid ladt;
              multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
              multi_log_re: multi_log hadt = multi_log ladt;
              lock_re: lock hadt = lock ladt
            }.

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

    End REFINEMENT_REL.

Properties of relations

    Section Rel_Property.

Prove that after taking one step, the refinement relation still holds
      Lemma relate_incr:
         abd abd´ f ,
          relate_RData f abd abd´
          → inject_incr f
          → relate_RData abd abd´.
      Proof.
        inversion 1; subst; intros; inv H; constructor; eauto.
        eapply tfs_inj_incr; eauto.
      Qed.

    End Rel_Property.

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

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

    Section OneStep_Forward_Relation.

      Section FRESH_PRIM.

        Lemma cons_buf_init_spec_kernel_mode:
           d ,
            cons_buf_init_spec d = Some
            kernel_mode d.
        Proof.
          intros. simpl; functional inversion H; eauto.
        Qed.

        Global Instance cons_buf_init_concrete_spec_inv:
          PreservesInvariants cons_buf_init_concrete_spec.
        Proof.
          preserves_invariants_simpl low_level_invariant high_level_invariant; eauto.
        Qed.

        Global Instance cons_buf_write_concrete_spec_inv:
          PreservesInvariants cons_buf_write_concrete_spec.
        Proof.
          preserves_invariants_simpl low_level_invariant high_level_invariant; eauto.
        Qed.

        Global Instance cons_buf_read_concrete_spec_inv:
          PreservesInvariants cons_buf_read_concrete_spec.
        Proof.
          preserves_invariants_simpl low_level_invariant high_level_invariant; eauto;
          inversion H0;
          try functional inversion H2; unfold rpos, wpos, s in *; subst;
          constructor;
          eauto 2.
        Qed.

        Global Instance cons_buf_wpos_concrete_spec_inv:
          PreservesInvariants cons_buf_wpos_concrete_spec.
        Proof.
          preserves_invariants_simpl low_level_invariant high_level_invariant; eauto.
        Qed.

        Lemma cons_buf_init_spec_ref:
          compatsim (crel HDATA LDATA) (gensem cons_buf_init_spec) (gensem cons_buf_init_concrete_spec).
        Proof.
          compatsim_simpl (@match_AbData).
          functional inversion H1; subst.
          refine_split; try econstructor; eauto.
          - econstructor.
            unfold cons_buf_init_concrete_spec.
            exploit relate_impl_iflags_eq; eauto; inversion 1.
            exploit relate_impl_init_eq; eauto; inversion 1.
            rewrite <- ikern_eq, <- ihost_eq, H0, H2, H3.
            reflexivity.
          - inv match_related.
            repeat econstructor; simpl; eauto.
          - econstructor.
        Qed.

        Lemma cons_buf_wpos_spec_kernel_mode:
           d wpos,
            cons_buf_wpos_spec d = Some wpos
            kernel_mode d.
        Proof.
          intros. simpl; functional inversion H; eauto.
        Qed.

        Lemma cons_buf_wpos_spec_ref:
          compatsim (crel HDATA LDATA) (gensem cons_buf_wpos_spec) cons_buf_wpos_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          functional inversion H2; subst.
          refine_split; try econstructor; eauto.
          - unfold cons_buf_wpos_concrete_spec.
            exploit relate_impl_iflags_eq; eauto; inversion 1.
            exploit relate_impl_init_eq; eauto; inversion 1.
            rewrite <- ikern_eq, <- ihost_eq, H0, H1, H3.
            inv match_related.
            inv console_re0.
            rewrite H8.
            unfold b, r, s0 in ×.
            rewrite H.
            reflexivity.
          - exploit relate_impl_iflags_eq; eauto. inversion 1.
            econstructor; eauto.
        Qed.

        Lemma cons_buf_read_spec_kernel_mode:
           d z,
            cons_buf_read_spec d = Some (, z)
            kernel_mode d.
        Proof.
          intros. simpl; functional inversion H; eauto.
        Qed.

        Lemma cons_buf_read_spec_ref:
          compatsim (crel HDATA LDATA) (gensem cons_buf_read_spec) cons_buf_read_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          functional inversion H1.
          {
            unfold b, r, s1, s0 in ×.
            subst.
            refine_split; try econstructor; eauto.
            - unfold cons_buf_read_concrete_spec.
              exploit relate_impl_iflags_eq; eauto; inversion 1.
              exploit relate_impl_init_eq; eauto; inversion 1.
              rewrite <- ikern_eq, <- ihost_eq, H2, H4, H3.
              inv match_related.
              inv console_re0.
              rewrite H5 in ×.
              simpl in ×.
              rewrite Z.add_0_r in H9.
              destruct (zeq (rpos_concrete (console_concrete d2))
                            (wpos_concrete (console_concrete d2))); try omega.
              rewrite H0.
              reflexivity.
            - exploit relate_impl_iflags_eq; eauto. inversion 1.
              econstructor; eauto.
          }
          {
            unfold r, b, s0 in ×.
            subst.
            refine_split; try econstructor; eauto.
            - unfold cons_buf_read_concrete_spec.
              exploit relate_impl_iflags_eq; eauto. inversion 1.
              exploit relate_impl_init_eq; eauto; inversion 1.
              rewrite <- ikern_eq, <- ihost_eq, H2, H4, H3.
              inv match_related.
              inv console_re0.
              rewrite H5 in ×.
              Opaque Z.of_nat.
              simpl in ×.
              destruct H9.
              destruct H10.
              rewrite H10.
              rewrite H8, H6.
              assert (rpos (console d1) (rpos (console d1) + Z.of_nat (S (length tl))) mod 512).
              {
                intro.
                xomega.
              }
              destruct (zeq (rpos (console d1))
                            ((rpos (console d1) + Z.of_nat (S (length tl))) mod 512)); try omega.
              reflexivity.
            - exploit relate_impl_iflags_eq; eauto. inversion 1.
              econstructor; eauto.
            - inv match_related.
              inv console_re0.
              econstructor; eauto.
              econstructor; eauto; simpl.
              rewrite H0.
              rewrite H5.
              simpl.
              rewrite Nat2Z.inj_succ.
              unfold Z.succ.
              repeat match goal with
                | [H: _ |- _] ⇒ clear H
              end.
              xomega.
              rewrite H5 in ×.
              simpl in ×.
              destruct H6.
              rewrite H in H7.
              destruct H7.
              assumption.
            - econstructor.
          }
        Qed.

        Lemma cons_buf_write_spec_kernel_mode:
           d c,
            cons_buf_write_spec c d = Some
            kernel_mode d.
        Proof.
          intros. simpl; functional inversion H; eauto.
        Qed.

        Ltac clearAll :=
          repeat match goal with
                   | [H: _ |- _] ⇒ clear H
                 end.


        Lemma eq1: rpos n, (rpos mod 512 + (n + 1)) mod 512 = ((rpos + 1) mod 512 + n) mod 512.
        Proof.
          intros.
          xomega.
        Qed.

        Lemma eqtmp: rpos, (rpos mod 512 + 1) mod 512 = (rpos + 1) mod 512.
        Proof.
          intros.
          xomega.
        Qed.

        Lemma eq2: rpos, (((rpos mod 512 + 1) mod 512 + 1) mod 512 + 1) mod 512 = (((rpos + 1) mod 512 + 1) mod 512 + 1) mod 512.
        Proof.
          intros.
          rewrite eqtmp.
          rewrite eqtmp.
          rewrite eqtmp.
          reflexivity.
        Qed.

        Lemma eq3: rpos n, ((rpos mod 512 + (n + 1)) mod 512 + 1) mod 512 = (((rpos + 1) mod 512 + n) mod 512 + 1) mod 512.
        Proof.
          intros.
          rewrite eq1.
          reflexivity.
        Qed.

        Lemma cons_buf_write_spec_ref:
          compatsim (crel HDATA LDATA) (gensem cons_buf_write_spec) cons_buf_write_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          functional inversion H1; subst.
          unfold handle_cons_buf_write in H1.
          destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)).
          {
            refine_split; try econstructor; eauto.
            - unfold cons_buf_write_concrete_spec.
              exploit relate_impl_iflags_eq; eauto. inversion 1.
              exploit relate_impl_init_eq; eauto; inversion 1.
              rewrite <- ikern_eq, <- ihost_eq, H2, H0, H3.
              inv match_related.
              inv console_re0.
              rewrite H5, H7.
              destruct (zeq
                          (((rpos (console d1) + Z.of_nat (length (cons_buf (console d1))))
                              mod 512 + 1) mod 512) (rpos (console d1))).
              exfalso.
              generalize e, l.
              repeat match goal with
                       | [H: _ |- _] ⇒ clear H
                     end.
              intros.
              rewrite <- length_to_zlength in l.
              xomega.
              reflexivity.
            - exploit relate_impl_iflags_eq; eauto. inversion 1.
              econstructor; eauto.
            - inv match_related.
              inv console_re0.
              econstructor; eauto.
              econstructor; eauto; simpl.
              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              rewrite H.
              reflexivity.
              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              simpl.
              assert(Z.of_nat (length (cons_buf (console d1) ++ Int.unsigned i :: nil)) = Z.of_nat (length (cons_buf (console d1))) + 1).
              {
                rewrite app_length.
                simpl.
                change 1 with (Z.of_nat 1).
                rewrite <- Nat2Z.inj_add.
                reflexivity.
              }
              rewrite H6.
              generalize l.
              repeat match goal with
                       | [H: _ |- _] ⇒ clear H
                     end.
              intro.
              xomega.
              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              rewrite H, H3 in ×.
              simpl in ×.

              assert(ind: n, length (cons_buf (console d1)) = n) by (esplit; eauto).
              destruct ind as [n ind].
              revert ind l.
              remember (cons_buf (console d1)) as L.
              revert HeqL.
              assert(0 rpos (console d1) < CONS_BUFFER_SIZE).
              {
                destruct Hhigh´.
                assumption.
              }
              clear H H3 H1 H0 H2 H4 flatmem_re0 vmxinfo_re0 ikern_re0 pg_re0 ihost_re0 AC_re0 ti_fst_re0 ti_snd_re0 LAT_re0 nps_re0 ipt_re0 init_re0 Hhigh´ Hmatch_ext match_match.
              generalize dependent L.
              remember (rpos (console d1)) as rpos.
              replace rpos with (rpos mod 512) by xomega.
              clear H6.
              generalize dependent d1.
              generalize dependent rpos.

              induction n.
              {
                intros.
                destruct L.
                simpl.
                change (Z.of_nat 0) with 0.
                split.
                change (Z.of_nat 1) with 1.
                omega.
                split.
                rewrite Z.add_0_r.
                rewrite Z.mod_mod by omega.
                rewrite ZMap.gss.
                reflexivity.
                split.
                omega.
                rewrite Z.add_0_r.
                rewrite Z.mod_mod by omega.
                reflexivity.
                inv ind.
              }
              {
                intros.
                destruct L.
                inv ind.
                rewrite <- length_to_zlength in l.
                econstructor.
                simpl in ×.
                rewrite app_length.
                simpl.
                rewrite Nat2Z.inj_succ in ×.
                unfold Z.succ in ×.
                rewrite Nat2Z.inj_add.
                change (Z.of_nat 1) with 1.
                omega.
                split.
                inv H5.
                rewrite ZMap.gso.
                destruct H0.
                assumption.
                generalize l.
                repeat match goal with
                         | [H: _ |- _] ⇒ clear H
                       end.
                intros.
                intro.
                simpl in ×.
                rewrite Nat2Z.inj_succ in ×.
                unfold Z.succ in ×.
                assert(Z.of_nat (length L) + 1 > 0) by xomega.
                assert( q, (rpos (console d1) mod 512 + (Z.of_nat (length L) + 1)) = 512 × q + (rpos (console d1) mod 512 + (Z.of_nat (length L) + 1)) mod 512).
                {
                   ((rpos (console d1) mod 512 + (Z.of_nat (length L) + 1)) / 512).
                  xomega.
                }
                destruct H1.
                assert ((rpos (console d1) mod 512 + (Z.of_nat (length L) + 1)) mod 512 = rpos (console d1) mod 512 + (Z.of_nat (length L) + 1) - 512 × x) by omega.
                rewrite H2 in H.
                assert((Z.of_nat (length L) + 1) - 512 × x > 0 (Z.of_nat (length L) + 1) - 512 × x < 0) by omega.
                Caseeq H3; intro.
                assert( x y, y > 0 → x = x + yFalse).
                {
                  intros.
                  omega.
                }
                apply (H4 (rpos (console d1) mod 512) ((Z.of_nat (length L) + 1) - 512 × x)).
                assumption.
                rewrite H at 1.
                omega.
                assert( x y, y < 0 → x = x + yFalse).
                {
                  intros.
                  omega.
                }
                apply (H4 (rpos (console d1) mod 512) ((Z.of_nat (length L) + 1) - 512 × x)).
                assumption.
                rewrite H at 1.
                omega.
                simpl.
                rewrite Nat2Z.inj_succ.
                unfold Z.succ.
                replace (rpos mod 512 + (Z.of_nat (length L) + 1)) with (rpos mod 512 + 1 + (Z.of_nat (length L))) by omega.
                assert (tmprw: (rpos mod 512 + 1 + Z.of_nat (length L)) mod 512 = ((rpos mod 512 + 1) mod 512 + Z.of_nat (length L)) mod 512).
                {
                  rewrite Z.add_mod by omega.
                  assert(0 Z.of_nat (length L) < 512).
                  {
                    split.
                    omega.
                    simpl in l.
                    rewrite Nat2Z.inj_succ in l.
                    unfold Z.succ in l.
                    omega.
                  }
                  assert(Z.of_nat (length L) mod 512 = Z.of_nat (length L)) by (generalize H; clearAll; intro; xomega).
                  rewrite H0.
                  reflexivity.
                }
                rewrite tmprw.
                eapply (IHn (rpos mod 512 + 1) (d1 {console: (console d1) {cons_buf: L} {rpos: rpos mod 512 + 1}})); eauto.
                simpl in l.
                rewrite Nat2Z.inj_succ in l.
                unfold Z.succ in l.
                generalize H5.
                clearAll.
                intro.
                simpl in H5.
                rewrite Nat2Z.inj_succ in H5.
                unfold Z.succ in H5.
                destruct H5.
                destruct H0.
                remember (rpos mod 512) as tmpz.
                remember (Z.of_nat (length L)) as tmpz´.
                clear Heqtmpz Heqtmpz´ H0.
                replace (((tmpz + 1) mod 512 + tmpz´) mod 512) with ((tmpz + (tmpz´ + 1)) mod 512) by xomega.
                apply H1.
                simpl in l.
                rewrite Nat2Z.inj_succ in l.
                unfold Z.succ in l.
                rewrite <- length_to_zlength.
                omega.
                simpl in l.
                rewrite Nat2Z.inj_succ in l.
                unfold Z.succ in l.
                rewrite <- length_to_zlength.
                omega.
              }
            - econstructor.
          }
          {
            assert(llength: Z.of_nat (length (cons_buf (console d1))) = 511).
            {
              destruct Hhigh´.
              rewrite <- length_to_zlength in g, valid_cons_buf_length.
              omega.
            }
            refine_split; try econstructor; eauto.
            - unfold cons_buf_write_concrete_spec.
              exploit relate_impl_iflags_eq; eauto; inversion 1.
              exploit relate_impl_init_eq; eauto; inversion 1.
              rewrite <- ikern_eq, <-ihost_eq, H0, H2, H3.
              inv match_related.
              inv console_re0.
              rewrite H5, H7.
              destruct (zeq
                          (((rpos (console d1) + Z.of_nat (length (cons_buf (console d1))))
                              mod 512 + 1) mod 512) (rpos (console d1))).
              reflexivity.
              exfalso.
              rewrite llength in n.
              destruct Hhigh´.
              generalize n valid_cons_buf_rpos.
              clearAll.
              intros.
              xomega.
            - exploit relate_impl_iflags_eq; eauto. inversion 1.
              econstructor; eauto.
            - inv match_related.
              inv console_re0.
              econstructor; eauto.
              econstructor; eauto; simpl.
              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              reflexivity.
              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              simpl.
              case_eq (cons_buf (console d1) ++ Int.unsigned i :: nil); intro.
              eapply app_eq_nil in H6.
              destruct H6.
              inv H7.
              intros.
              assert(Z.of_nat(length(cons_buf (console d1) ++ Int.unsigned i :: nil)) = Z.of_nat(length(z :: l))).
              {
                rewrite H6; reflexivity.
              }
              rewrite app_length in H7.
              simpl in H7.
              rewrite Nat2Z.inj_succ in H7.
              unfold Z.succ in H7.
              rewrite Nat2Z.inj_add in H7.
              change (Z.of_nat 1) with 1 in H7.
              assert(llength´: Z.of_nat (length l) = 511).
              {
                rewrite llength in H7.
                omega.
              }
              rewrite llength´.
              destruct Hhigh´.
              rewrite llength.
              generalize valid_cons_buf_rpos; clearAll; intros.
              change 1 with (1 mod 512).
              change 511 with (511 mod 512).
              rewrite <- Z.add_mod.
              rewrite <- Z.add_mod.
              change (1 mod 512) with 1.
              change (511 mod 512) with 511.
              xomega.
              omega.
              omega.

              unfold handle_cons_buf_write.
              destruct (zlt (Zlength (cons_buf (console d1))) (512 - 1)); try omega.
              simpl in ×.
              case_eq (cons_buf (console d1) ++ Int.unsigned i :: nil); intro.
              eapply app_eq_nil in H6.
              destruct H6.
              inv H7.
              intros.
              assert(ind: n, length l = n) by (esplit; eauto).
              destruct ind as [n ind].
              revert ind.
              assert(0 rpos (console d1) < CONS_BUFFER_SIZE).
              {
                destruct Hhigh´.
                assumption.
              }
              assert(lengthl: Z.of_nat (length l) < 512).
              {
                simpl in ×.
                assert(Z.of_nat(length(cons_buf (console d1) ++ Int.unsigned i :: nil)) = Z.of_nat(length(z :: l))).
                {
                  rewrite H6; reflexivity.
                }
                rewrite app_length in H8.
                simpl in H8.
                rewrite Nat2Z.inj_succ in H8.
                unfold Z.succ in H8.
                rewrite Nat2Z.inj_add in H8.
                change (Z.of_nat 1) with 1 in H8.
                rewrite llength in H8.
                omega.
              }
              assert(((rpos (console d1) + Z.of_nat (length (cons_buf (console d1))))
                              mod 512 + 1) mod 512 = rpos (console d1)).
              {
                rewrite llength.
                destruct Hhigh´.
                generalize n valid_cons_buf_rpos.
                clearAll.
                intros.
                xomega.
              }
              rewrite H, H4 in ×.
              assert(Z.of_nat (length (cons_buf (console d1))) = Z.of_nat (length l)).
              {
                simpl in ×.
                assert(Z.of_nat(length(cons_buf (console d1) ++ Int.unsigned i :: nil)) = Z.of_nat(length(z :: l))).
                {
                  rewrite H6; reflexivity.
                }
                rewrite app_length in H9.
                simpl in H9.
                rewrite Nat2Z.inj_succ in H9.
                unfold Z.succ in H9.
                rewrite Nat2Z.inj_add in H9.
                change (Z.of_nat 1) with 1 in H9.
                rewrite llength in H9.
                omega.
              }
              rewrite H9 in ×.

              clear H H3 H1 H0 H2 H4 flatmem_re0 vmxinfo_re0 ikern_re0 pg_re0 ihost_re0 AC_re0 ti_fst_re0 ti_snd_re0 LAT_re0 nps_re0 ipt_re0 init_re0 Hhigh´ Hmatch_ext match_match g llength H8 H9 g0.
              generalize dependent l.
              remember (rpos (console d1)) as rpos.
              replace rpos with (rpos mod 512) by xomega.
              clear H7.
              generalize dependent d1.
              generalize dependent rpos.
              generalize dependent z.

              induction n.
              {
                intros.
                destruct l.
                simpl.
                change (Z.of_nat 1) with 1.
                split.
                omega.
                change (Z.of_nat 0) with 0.
                rewrite Z.add_0_r.
                rewrite Z.mod_mod by omega.
                reflexivity.
                inv ind.
              }
              {
                intros.
                destruct l.
                inv ind.
                econstructor.
                assumption.
                split.
                simpl.
                rewrite Nat2Z.inj_succ.
                unfold Z.succ.
                destruct (cons_buf (console d1)).
                inv H6.
                inv H5.
                destruct H0.
                destruct l0.
                inv H6.
                simpl.
                change (Z.of_nat 0) with 0.
                replace (0 + 1) with 1 by omega.
                rewrite ZMap.gss.
                reflexivity.
                rewrite ZMap.gso.
                inv H1.
                destruct H3.
                inv H6.
                assumption.
                inv H6.

                assert(0 < (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) < 512).
                {
                  rewrite app_length.
                  simpl in ×.
                  rewrite Nat2Z.inj_succ in H.
                  rewrite Nat2Z.inj_succ in H.
                  unfold Z.succ in H.
                  rewrite Nat2Z.inj_add.
                  change (Z.of_nat 1) with 1.
                  omega.
                }
                generalize H2.
                clearAll.
                intros.
                intro.
                change 1 with (1 mod 512) in H at 1.
                replace (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) with ((Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) mod 512) in H by (generalize H2; clearAll; intro; xomega).
                rewrite <- Z.add_mod in H by omega.
                rewrite <- Z.add_mod in H by omega.
                assert( q, (rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1)) = 512 × q + (rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1)) mod 512).
                {
                   ((rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1)) / 512).
                  xomega.
                }
                destruct H0.
                assert ((rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1)) mod 512 = rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) - 512 × x) by omega.
                rewrite H1 in H.
                assert( , (rpos (console d1) + 1) = 512 × + (rpos (console d1) + 1) mod 512).
                {
                   ((rpos (console d1) + 1) / 512).
                  xomega.
                }
                destruct H3.
                assert ((rpos (console d1) + 1) mod 512 = rpos (console d1) + 1 - 512 × x0) by omega.
                rewrite H4 in H.
                assert (512 × x0 + Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) - 512 × x = 0).
                {
                  generalize H; clearAll; intros.
                  assert(rpos (console d1) + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) - 512 × x = rpos (console d1) + 1 + (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) - 512 × x)) by omega.
                  rewrite H0 in H.
                  clear H0.
                  assert( a b c, a - b = a + cb + c = 0).
                  {
                    intros.
                    omega.
                  }
                  eapply (H0 (rpos (console d1) + 1)) in H.
                  omega.
                }
                generalize H2 H5; clearAll; intros.
                assert(0 < Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) < 512).
                {
                  split.
                  rewrite app_length.
                  simpl.
                  rewrite Nat2Z.inj_add.
                  change (Z.of_nat 1) with 1.
                  generalize (Nat2Z.is_nonneg (length l0)); intro.
                  omega.
                  omega.
                }
                remember (Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) as n.
                clear Heqn.
                omega.

                simpl.
                rewrite Nat2Z.inj_succ.
                unfold Z.succ.
                rewrite (eq1 rpos (Z.of_nat (length l))).
                rewrite (eqtmp rpos).
                destruct (cons_buf (console d1)).
                inv H6.
                destruct l0.
                inv H6.
                simpl.
                change (Z.of_nat 0) with 0.
                rewrite Z.add_0_r.
                rewrite Z.mod_mod by omega.
                split.
                omega.
                reflexivity.
                inv H6.
                inv H5.
                destruct H0.
                eapply (IHn z0 (rpos (console d1) + 1) (d1 {console: (console d1) {cons_buf: z0 :: l0} {rpos: (rpos (console d1)) + 1}})); eauto.
                simpl.
                simpl in H.
                rewrite Nat2Z.inj_succ in H.
                rewrite Nat2Z.inj_succ in H.
                unfold Z.succ in H.
                inv H1.
                destruct H3.
                split.
                rewrite Nat2Z.inj_succ.
                unfold Z.succ.
                omega.
                split.
                rewrite <- (eqtmp (rpos (console d1))).
                assumption.
                simpl in H3.
                rewrite Nat2Z.inj_succ in H3.
                unfold Z.succ in H3.
                assert(tmprw: ((rpos (console d1) + 1) mod 512 +
       Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) mod 512 = (rpos (console d1) mod 512 +
                                 (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1)) mod 512).
                {
                  assert(Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1 < 512).
                  {
                    rewrite app_length.
                    simpl.
                    rewrite Nat2Z.inj_add.
                    change (Z.of_nat 1) with 1.
                    omega.
                  }
                  replace (Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) with ((Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) + 1) mod 512) by (generalize H4; clearAll; intro; xomega).
                  rewrite <- Z.add_mod by omega.
                  assert(Z.of_nat (length (l0 ++ Int.unsigned i :: nil)) < 512) by omega.
                  replace (Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) with ((Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) mod 512) by (generalize H5; clearAll; intro; xomega).
                  rewrite <- Z.add_mod by omega.
                  assert(mod_eq: a b c, a = ba mod c = b mod c).
                  {
                    intros.
                    rewrite H6.
                    reflexivity.
                  }
                  replace ((Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) mod 512) with (Z.of_nat (length (l0 ++ Int.unsigned i :: nil))) by (generalize H5; clearAll; intro; xomega).
                  eapply mod_eq; try omega.
                }
                rewrite tmprw.
                rewrite <- (eqtmp (rpos (console d1))).
                assumption.

                rewrite app_length.
                simpl.
                rewrite Nat2Z.inj_add.
                change (Z.of_nat 1) with 1.
                simpl in H.
                rewrite Nat2Z.inj_succ in H.
                rewrite Nat2Z.inj_succ in H.
                unfold Z.succ in H.
                omega.
              }
            - econstructor.
          }
        Qed.

      End FRESH_PRIM.


      Section PASSTHROUGH_PRIM.

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

        Require Import LoadStoreSem1.

        Lemma passthrough_correct:
          sim (crel HDATA LDATA) dabsconsolebuffintro_passthrough dconsolebuffintro.
        Proof.
          sim_oplus.
          - apply fload´_sim.
          - apply fstore´_sim.
          - apply page_copy´_sim.
          - apply page_copy_back´_sim.

          - apply vmxinfo_get_sim.
          - apply setPG_sim.
          - apply setCR3_sim.
          - apply get_size_sim.
          - apply is_mm_usable_sim.
          - apply get_mm_s_sim.
          - apply get_mm_l_sim.
          - apply get_CPU_ID_sim.
          - apply get_curid_sim.
          - apply set_curid_sim.
          - apply set_curid_init_sim.
          - apply (release_lock_sim (valid_arg_imply:= Shared2ID0_imply)).
          -
            eapply acquire_lock_sim0; eauto.
            intros. inv H; trivial; try inv H0.
          - apply ticket_lock_init0_sim.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            generalize (cons_buf_init_spec_ref); intro.
            inv H.
            inv H3.
            simpl in ×.
            eapply sextcall_sim_step; eauto.
            econstructor.
            econstructor.
            assumption.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            generalize (cons_buf_write_spec_ref); intro.
            inv H.
            inv H3.
            simpl in ×.
            exploit sextcall_sim_step; eauto.
            econstructor.
            econstructor.
            econstructor.
            eassumption.
            intro.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H0.
            destruct H2.
            esplit. esplit. esplit. esplit.
            split; try eassumption.
            inv H.
            Focus 2.
            split; try eassumption.
            split; try eassumption.
            econstructor.
            econstructor.
            econstructor.
            eassumption.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            generalize (cons_buf_read_spec_ref); intro.
            inv H.
            inv H3.
            simpl in ×.
            exploit sextcall_sim_step; eauto.
            econstructor.
            econstructor.
            eassumption.
            intro.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H0.
            destruct H2.
            esplit. esplit. esplit. esplit.
            split; try eassumption.
            inv H.
            Focus 2.
            split; try eassumption.
            split; try eassumption.
            econstructor.
            econstructor.
            eassumption.
          -
            layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
            generalize (cons_buf_wpos_spec_ref); intro.
            inv H.
            inv H3.
            simpl in ×.
            exploit sextcall_sim_step; eauto.
            econstructor.
            econstructor.
            rewrite H2.
            reflexivity.
            intro.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H.
            destruct H0.
            destruct H1.
            esplit. esplit. esplit. esplit.
            split; try eassumption.
            inv H.
            Focus 2.
            split; try eassumption.
            split.
            eapply Hmatch_ext.
            unfold inject_incr.
            intros.
            assumption.
            econstructor.
            econstructor.
            rewrite H12.
            reflexivity.
          - apply serial_irq_check_sim.
          - apply iret_sim.
          - apply cli_sim.
          - apply sti_sim.
          - apply serial_irq_current_sim.
          - apply ic_intr_sim.
          - apply save_context_sim.
          - apply restore_context_sim.
          - apply local_irq_save_sim.
          - apply local_irq_restore_sim.
          - apply serial_in_sim.
          - apply serial_out_sim.
          - apply serial_hw_intr_sim.
          - apply ioapic_read_sim.
          - apply ioapic_write_sim.
          - apply lapic_read_sim.
          - apply lapic_write_sim.
          - apply trapin_sim.
          - apply trapout´_sim.
          - apply hostin_sim.
          - apply hostout´_sim.
          - apply proc_create_postinit_sim.
          - apply trap_info_get_sim.
          - apply trap_info_ret_sim.
          - layer_sim_simpl.
            + eapply load_correct1.
            + eapply store_correct1.
        Qed.

      End PASSTHROUGH_PRIM.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.