Library mcertikos.invariants.INVLemmaInterrupt

Require Import Coqlib.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import AuxLemma.
Require Import DeviceStateDataType.
Require Import AbstractDataType.

Require Import Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import AST.
Require Import AuxStateDataType.
Require Import ObjInterruptManagement.
Require Import Omega.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import GlobalOracleProp.
Require Import INVLemmaMemory.
Require Import RealParams.

Section INTERRUPT_INV.

  Section INTR_DISABLE.

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

    Lemma serial_intr_disable_aux_preserves_all:
      ∀ n masked d d´,
        serial_intr_disable_aux n masked d = ret d´ →
        CPU_ID d = CPU_ID d´ ∧
        cid d = cid d´ ∧
        multi_oracle d = multi_oracle d´ ∧
        multi_log d = multi_log d´ ∧
        ti d = ti d´ ∧
        kctxt d = kctxt d´ ∧
        uctxt d = uctxt d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        AC d = AC d´ ∧
        init d = init d´ ∧
        ikern d = ikern d´ ∧
        ihost d = ihost d´ ∧
        pg d = pg d´ ∧
        MM d = MM d´ ∧
        MMSize d = MMSize d´ ∧
        CR3 d = CR3 d´ ∧
        nps d = nps d´ ∧
        AT d = AT d´ ∧
        ATC d = ATC d´ ∧
        pperm d = pperm d´ ∧
        ipt d = ipt d´ ∧
        PT d = PT d´ ∧
        ptpool d = ptpool d´ ∧
        HP d = HP d´ ∧
        LAT d = LAT d´ ∧
        idpde d = idpde d´ ∧
        abtcb d = abtcb d´ ∧
        abq d = abq d´ ∧
        cid d = cid d´ ∧
        tcb d = tcb d´ ∧
        tdq d = tdq d´ ∧
        syncchpool d = syncchpool d´ ∧
        uctxt d = uctxt d´ ∧
        ept d = ept d´ ∧
        tf d = tf d´ ∧
        big_oracle d = big_oracle d´ ∧
        big_log d = big_log d´ ∧
        sleeper d = sleeper d´ ∧
        lock d = lock d´ ∧
        smspool d = smspool d´ ∧
        big_log d = big_log d´ ∧
        big_oracle d = big_oracle d´ ∧
        ept d = ept d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        vmxinfo d = vmxinfo d´.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        repeat (split; [reflexivity|]); try reflexivity.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H.
          simpl in H.
          apply H.
        }
        {
          eapply IHn in H.
          functional inversion Hdestruct1; subst;
          simpl in *; eauto.
        }
        {
          inv H.
          repeat (split; [reflexivity|]); try reflexivity.
        }
      }
    Qed.

    Lemma serial_intr_disable_preserves_all:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        CPU_ID d = CPU_ID d´ ∧
        cid d = cid d´ ∧
        multi_oracle d = multi_oracle d´ ∧
        multi_log d = multi_log d´ ∧
        ti d = ti d´ ∧
        kctxt d = kctxt d´ ∧
        uctxt d = uctxt d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        AC d = AC d´ ∧
        init d = init d´ ∧
        ikern d = ikern d´ ∧
        ihost d = ihost d´ ∧
        pg d = pg d´ ∧
        MM d = MM d´ ∧
        MMSize d = MMSize d´ ∧
        CR3 d = CR3 d´ ∧
        nps d = nps d´ ∧
        AT d = AT d´ ∧
        ATC d = ATC d´ ∧
        pperm d = pperm d´ ∧
        ipt d = ipt d´ ∧
        PT d = PT d´ ∧
        ptpool d = ptpool d´ ∧
        HP d = HP d´ ∧
        LAT d = LAT d´ ∧
        idpde d = idpde d´ ∧
        abtcb d = abtcb d´ ∧
        abq d = abq d´ ∧
        cid d = cid d´ ∧
        tcb d = tcb d´ ∧
        tdq d = tdq d´ ∧
        syncchpool d = syncchpool d´ ∧
        uctxt d = uctxt d´ ∧
        ept d = ept d´ ∧
        tf d = tf d´ ∧
        big_oracle d = big_oracle d´ ∧
        big_log d = big_log d´ ∧
        sleeper d = sleeper d´ ∧
        lock d = lock d´ ∧
        smspool d = smspool d´ ∧
        big_log d = big_log d´ ∧
        big_oracle d = big_oracle d´ ∧
        ept d = ept d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        vmxinfo d = vmxinfo d´.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_disable_aux_preserves_all INTR_DISABLE_REC_MAX masked (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_disable_aux_rpos_within_range:
      ∀ n masked d d´,
        serial_intr_disable_aux n masked d = ret d´ →
        0 ≤ rpos (console d) < 512 →
        0 ≤ rpos (console d´) < 512.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        eauto.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H.
          eassumption.
          simpl in ×.
          assumption.
        }
        {
          eapply IHn in H; simpl in *; try assumption.
          functional inversion Hdestruct1; subst; simpl in *; eauto.
          apply Z.mod_bound_pos.
          omega.
          omega.
        }
        {
          inv H.
          eauto.
        }
      }
    Qed.

    Open Scope Z_scope.
    Lemma serial_intr_disable_rpos_within_range:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        0 ≤ rpos (console d) < 512 →
        0 ≤ rpos (console d´) < 512.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_disable_aux_rpos_within_range INTR_DISABLE_REC_MAX masked (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_disable_aux_cons_buf_length_within_range:
      ∀ n masked d d´,
        serial_intr_disable_aux n masked d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        0 ≤ Zlength (cons_buf (console d´)) < 512.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        eauto.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H; simpl in *; eassumption.
        }
        {
          eapply IHn in H; simpl in *; try eassumption.
          functional inversion Hdestruct1; simpl in *; eauto.
          split. apply Zlength_ge_0. omega.
          split. apply Zlength_ge_0. repeat solve_list. repeat toZ.
          omega.
          generalize _x10. repeat solve_list. intros. omega. omega.
          generalize _x10. repeat solve_list. intros. omega.
        }
        {
          inv H; eauto.
        }
      }
    Qed.

    Lemma serial_intr_disable_cons_buf_length_within_range:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        0 ≤ Zlength (cons_buf (console d´)) < 512.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_disable_aux_cons_buf_length_within_range INTR_DISABLE_REC_MAX masked (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_disable_aux_cons_buf_tl_length_within_range:
      ∀ n masked d d´ x tl,
        serial_intr_disable_aux n masked d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        cons_buf (console d´) = x :: tl →
        0 ≤ Zlength tl < 512.
    Proof.
      intros.
      generalize (serial_intr_disable_aux_cons_buf_length_within_range n masked d d´ H H0).
      rewrite H1. generalize H0. solve_list.
      intros. split. apply Zlength_ge_0. omega.
    Qed.

    Require Import FutureTactic.
    Lemma serial_intr_disable_cr2_injection:
      ∀ d d´ m,
        serial_intr_disable_spec d = ret d´ →
        val_inject (Mem.flat_inj m) (snd (ti d)) (snd (ti d)) →
        val_inject (Mem.flat_inj m) (snd (ti d´)) (snd (ti d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_cr2_type:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        Val.has_type (snd (ti d)) Tint →
        Val.has_type (snd (ti d´)) Tint.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_kctxt_INJECT:
      ∀ d d´ m,
        serial_intr_disable_spec d = ret d´ →
        kctxt_inject_neutral (kctxt d) m →
        kctxt_inject_neutral (kctxt d´) m.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_uctxt_INJECT:
      ∀ d d´ m,
        serial_intr_disable_spec d = ret d´ →
        uctxt_inject_neutral (uctxt d) m →
        uctxt_inject_neutral (uctxt d´) m.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_VMCS_inject_neutral:
      ∀ d d´ m,
        serial_intr_disable_spec d = ret d´ →
        VMCSPool_inject_neutral (vmcs d) m →
        VMCSPool_inject_neutral (vmcs d´) m.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_VMX_inject_neutral:
      ∀ d d´ m,
        serial_intr_disable_spec d = ret d´ →
        VMXPool_inject_neutral (vmx d) m →
        VMXPool_inject_neutral (vmx d´) m.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_Container_valid:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        Container_valid (AC d) →
        Container_valid (AC d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_disable_valid_preinit_container:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = false →
         ∀ x : Z, 0 ≤ x < num_proc → cused (ZMap.get x (AC d)) ≠ true) →
        (init d´ = false →
         ∀ x : Z, 0 ≤ x < num_proc → cused (ZMap.get x (AC d´)) ≠ true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_preserves_ikernhost:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        ikern d = true ∧ ihost d = true →
        ikern d´ = true ∧ ihost d´ = true.
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_kern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ikern d = false → pg d = true ∧ init d = true) →
        (ikern d´ = false → pg d´ = true ∧ init d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_mm:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → MM_valid (MM d) (MMSize d)) →
        (init d´ = true → MM_valid (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_correct_mm:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → MM_correct (MM d) (MMSize d)) →
        (init d´ = true → MM_correct (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_mm_kern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → MM_kern (MM d) (MMSize d)) →
        (init d´ = true → MM_kern (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_mm_size:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → 0 < MMSize d ≤ Int.max_unsigned) →
        (init d´ = true → 0 < MMSize d´ ≤ Int.max_unsigned).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_CR4:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → CR3_valid (CR3 d)) →
        (pg d´ = true → CR3_valid (CR3 d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_nps:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → 262144 ≤ nps d ≤ 1048576) →
        (init d´ = true → 262144 ≤ nps d´ ≤ 1048576).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_AT_kern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → AT_kern (AT d) (nps d)) →
        (init d´ = true → AT_kern (AT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_AT_usr:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = true → AT_usr (AT d) (nps d)) →
        (init d´ = true → AT_usr (AT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pperm:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (consistent_ppage (AT d) (pperm d) (nps d)) →
        (consistent_ppage (AT d´) (pperm d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_init_pperm:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = false → pperm d = ZMap.init PGUndef) →
        (init d´ = false → pperm d´ = ZMap.init PGUndef).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_kern_pt:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ipt d = false → pg d = true ∧ init d = true) →
        (ipt d´ = false → pg d´ = true ∧ init d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_iptt:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ipt d = true → ikern d = true) →
        (ipt d´ = true → ikern d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_iptf:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ikern d = false → ipt d = false) →
        (ikern d´ = false → ipt d´ = false).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_PMap:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → PMap_valid (ZMap.get (PT d) (ptpool d))) →
        (pg d´ = true → PMap_valid (ZMap.get (PT d´) (ptpool d´))).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_PMap_kern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → ipt d = true → PMap_kern (ZMap.get (PT d) (ptpool d))) →
        (pg d´ = true → ipt d´ = true → PMap_kern (ZMap.get (PT d´) (ptpool d´))).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_PT:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → 0 ≤ PT d < num_proc) →
        (pg d´ = true → 0 ≤ PT d´ < num_proc).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_dirty:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (dirty_ppage (pperm d) (HP d)) →
        (dirty_ppage (pperm d´) (HP d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_uninitialized:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = false → (∀ n i pi pte, ZMap.get i (ZMap.get n (ptpool d)) ≠ PDEValid pi pte)) →
        (init d´ = false → (∀ n i pi pte, ZMap.get i (ZMap.get n (ptpool d´)) ≠ PDEValid pi pte)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_ihost:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ihost d = false → pg d = true ∧ init d = true ∧ ikern d = true) →
        (ihost d´ = false → pg d´ = true ∧ init d´ = true ∧ ikern d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_preserves_tf:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        tf d = tf d´.
    Proof.
      intros.
      generalize (serial_intr_disable_preserves_all d d´ H); intro.
      destruct H0 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]; try assumption).
    Qed.

    Lemma serial_intr_disable_CPU_ID_within_range:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        0 ≤ CPU_ID d < 8 →
        0 ≤ CPU_ID d´ < 8.
    Proof.
      intros.
      generalize (serial_intr_disable_preserves_all d d´ H); intros.
      destruct H1 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]); try omega.
    Qed.

    Lemma serial_intr_disable_cid_within_range:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
        0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
    Proof.
      intros.
      generalize (serial_intr_disable_preserves_all d d´ H); intros.
      destruct H1 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]).
      rewrite <- H1; rewrite <- H2; auto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_multi_oracle_pool:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        valid_multi_oracle_pool (multi_oracle d) →
        valid_multi_oracle_pool (multi_oracle d´).
    Proof.
      intros.
      generalize (serial_intr_disable_preserves_all d d´ H); intro.
      destruct H1 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]).
      rewrite <- H3; auto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_multi_oracle_pool_H:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        valid_multi_oracle_pool_H (multi_oracle d) →
        valid_multi_oracle_pool_H (multi_oracle d´).
    Proof.
      intros.
      generalize (serial_intr_disable_preserves_all d d´ H); intro.
      destruct H1 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]).
      rewrite <- H3; auto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_qlock_pool:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        (init d = true → valid_qlock_pool (multi_log d)) →
        (init d´ = true → valid_qlock_pool (multi_log d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_hlock_pool:
      ∀ d d´,
        serial_intr_disable_spec d = Some d´ →
        (valid_hlock_pool (multi_log d)) →
        (valid_hlock_pool (multi_log d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_AT_oracle_pool:
      ∀ d d´, serial_intr_disable_spec d = Some d´ →
                   valid_AT_oracle_pool (multi_oracle d) →
                   valid_AT_oracle_pool (multi_oracle d´).
    Proof.
      intros; generalize (serial_intr_disable_preserves_all d d´ H); intro.
      destruct H1 as [? Htmp].
      repeat (destruct Htmp as [? Htmp]).
      rewrite <- H3; auto.
    Qed.

    Lemma serial_intr_disable_preserves_valid_AT_log_pool:
      ∀ d d´, serial_intr_disable_spec d = Some d´ →
                   (init d = true → valid_AT_log_pool (multi_log d) (nps d)) →
                   (init d´ = true → valid_AT_log_pool (multi_log d´) (nps d´)).
    Proof.
      intros; generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_nps2:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → 262144 ≤ nps d ≤ 1048576) →
        (pg d´ = true → 262144 ≤ nps d´ ≤ 1048576).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.


    Lemma serial_intr_disable_valid_ipt_pg:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ipt d = false → pg d = true) →
        (ipt d´ = false → pg d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_ihost_pg_ikern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (ihost d = false → pg d = true ∧ ikern d = true) →
        (ihost d´ = false → pg d´ = true ∧ ikern d´ = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.


    Lemma serial_intr_disable_valid_pg_pperm:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = false → pperm d = ZMap.init PGUndef) →
        (pg d´ = false → pperm d´ = ZMap.init PGUndef).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_PMap_valid:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true →
         ∀ i : Z, 0 ≤ i < num_proc → PMap_valid (ZMap.get i (ptpool d))) →
        (pg d´ = true →
         ∀ i : Z, 0 ≤ i < num_proc → PMap_valid (ZMap.get i (ptpool d´))).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_ipt_PT:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → ipt d = true → PT d = 0) →
        (pg d´ = true → ipt d´ = true → PT d´ = 0).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_PMap_kern:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → PMap_kern (ZMap.get 0 (ptpool d))) →
        (pg d´ = true → PMap_kern (ZMap.get 0 (ptpool d´))).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_IDPDE_init:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → IDPDE_init (idpde d)) →
        (pg d´ = true → IDPDE_init (idpde d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_consistent_pmap2:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (consistent_pmap (ptpool d) (pperm d) (AT d) (LAT d) (nps d)) →
        (consistent_pmap (ptpool d´) (pperm d´) (AT d´) (LAT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_consistent_pmap_domain2:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (consistent_pmap_domain (ptpool d) (pperm d) (LAT d) (nps d)) →
        (consistent_pmap_domain (ptpool d´) (pperm d´) (LAT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_consistent_lat_domain:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (consistent_lat_domain (ptpool d) (LAT d) (nps d)) →
        (consistent_lat_domain (ptpool d´) (LAT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_LATable_nil:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (LATCTable_nil (LAT d) (AT d)) →
        (LATCTable_nil (LAT d´) (AT d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_init:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = init d) →
        (pg d´ = init d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_cused:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → cused (ZMap.get 0 (AC d)) = true) →
        (pg d´ = true → cused (ZMap.get 0 (AC d´)) = true).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_AbTCBCorrect_range:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → AbTCBCorrect_range (abtcb d)) →
        (pg d´ = true → AbTCBCorrect_range (abtcb d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_AbQCorrect_range:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → AbQCorrect_range (abq d)) →
        (pg d´ = true → AbQCorrect_range (abq d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_NotInQ:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → NotInQ (AC d) (abtcb d)) →
        (pg d´ = true → NotInQ (AC d´) (abtcb d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_QCount:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → QCount (abtcb d) (abq d)) →
        (pg d´ = true → QCount (abtcb d´) (abq d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_pg_InQ:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (pg d = true → InQ (abtcb d) (abq d)) →
        (pg d´ = true → InQ (abtcb d´) (abq d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_consistent_ppage_log:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        consistent_ppage_log (multi_log d) (pperm d) (nps d) →
        consistent_ppage_log (multi_log d´) (pperm d´) (nps d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Definition PMap_uninitialized (ptp: PMapPool) :=
      ∀ n i pi pte,
        ZMap.get i (ZMap.get n ptp) ≠ PDEValid pi pte.

    Lemma PMap_uninitialized_undef:
      PMap_uninitialized (ZMap.init (ZMap.init PDEUndef)).
    Proof.
      intros n. intros.
      repeat rewrite ZMap.gi. congruence.
    Qed.

    Lemma serial_intr_disable_valid_init_PMap_uninitialized:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        (init d = false → PMap_uninitialized (ptpool d)) →
        (init d´ = false → PMap_uninitialized (ptpool d´)).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_multi_oracle_pool_H1:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_multi_oracle_pool_H1 (multi_oracle d) →
        valid_multi_oracle_pool_H1 (multi_oracle d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_hlock_pool1:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_hlock_pool1 (multi_log d) →
        valid_hlock_pool1 (multi_log d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_AT_oracle_pool_H:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_AT_oracle_pool_H (multi_oracle d) →
        valid_AT_oracle_pool_H (multi_oracle d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_AT_log_pool_H:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_AT_log_pool_H (multi_log d) →
        valid_AT_log_pool_H (multi_log d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Context`{oracle_ops: MultiOracleOps}.

    Lemma serial_intr_disable_valid_valid_big_oracle:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_big_oracle (big_oracle d) →
        valid_big_oracle (big_oracle d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_big_log:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_big_log (big_log d) (CPU_ID d) →
        valid_big_log (big_log d´) (CPU_ID d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_disable_valid_valid_lock_pool:
      ∀ d d´,
        serial_intr_disable_spec d = ret d´ →
        valid_lock_pool_B (big_log d) →
        valid_lock_pool_B (big_log d´).
    Proof.
      intros. generalize (serial_intr_disable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

  End INTR_DISABLE.

  Section INTR_ENABLE.

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

    Lemma serial_intr_enable_aux_preserves_all:
      ∀ n d d´,
        serial_intr_enable_aux n d = ret d´ →
        CPU_ID d = CPU_ID d´ ∧
        cid d = cid d´ ∧
        multi_oracle d = multi_oracle d´ ∧
        multi_log d = multi_log d´ ∧
        ti d = ti d´ ∧
        kctxt d = kctxt d´ ∧
        uctxt d = uctxt d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        AC d = AC d´ ∧
        init d = init d´ ∧
        ikern d = ikern d´ ∧
        ihost d = ihost d´ ∧
        pg d = pg d´ ∧
        MM d = MM d´ ∧
        MMSize d = MMSize d´ ∧
        CR3 d = CR3 d´ ∧
        nps d = nps d´ ∧
        AT d = AT d´ ∧
        ATC d = ATC d´ ∧
        pperm d = pperm d´ ∧
        ipt d = ipt d´ ∧
        PT d = PT d´ ∧
        ptpool d = ptpool d´ ∧
        HP d = HP d´ ∧
        LAT d = LAT d´ ∧
        idpde d = idpde d´ ∧
        abtcb d = abtcb d´ ∧
        abq d = abq d´ ∧
        cid d = cid d´ ∧
        tcb d = tcb d´ ∧
        tdq d = tdq d´ ∧
        syncchpool d = syncchpool d´ ∧
        uctxt d = uctxt d´ ∧
        ept d = ept d´ ∧
        tf d = tf d´ ∧
        sleeper d = sleeper d´ ∧
        lock d = lock d´ ∧
        smspool d = smspool d´ ∧
        big_log d = big_log d´ ∧
        big_oracle d = big_oracle d´ ∧
        ept d = ept d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        vmxinfo d = vmxinfo d´.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        repeat (split; [reflexivity|]); try reflexivity.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H.
          functional inversion Hdestruct0; subst;
          simpl in *; eauto.
        }
        {
          inv H.
          repeat (split; [reflexivity|]); try reflexivity.
        }
      }
    Qed.

    Lemma serial_intr_enable_preserves_all:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        CPU_ID d = CPU_ID d´ ∧
        cid d = cid d´ ∧
        multi_oracle d = multi_oracle d´ ∧
        multi_log d = multi_log d´ ∧
        ti d = ti d´ ∧
        kctxt d = kctxt d´ ∧
        uctxt d = uctxt d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        AC d = AC d´ ∧
        init d = init d´ ∧
        ikern d = ikern d´ ∧
        ihost d = ihost d´ ∧
        pg d = pg d´ ∧
        MM d = MM d´ ∧
        MMSize d = MMSize d´ ∧
        CR3 d = CR3 d´ ∧
        nps d = nps d´ ∧
        AT d = AT d´ ∧
        ATC d = ATC d´ ∧
        pperm d = pperm d´ ∧
        ipt d = ipt d´ ∧
        PT d = PT d´ ∧
        ptpool d = ptpool d´ ∧
        HP d = HP d´ ∧
        LAT d = LAT d´ ∧
        idpde d = idpde d´ ∧
        abtcb d = abtcb d´ ∧
        abq d = abq d´ ∧
        cid d = cid d´ ∧
        tcb d = tcb d´ ∧
        tdq d = tdq d´ ∧
        syncchpool d = syncchpool d´ ∧
        uctxt d = uctxt d´ ∧
        ept d = ept d´ ∧
        tf d = tf d´ ∧
        sleeper d = sleeper d´ ∧
        lock d = lock d´ ∧
        smspool d = smspool d´ ∧
        big_log d = big_log d´ ∧
        big_oracle d = big_oracle d´ ∧
        ept d = ept d´ ∧
        vmcs d = vmcs d´ ∧
        vmx d = vmx d´ ∧
        vmxinfo d = vmxinfo d´.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_enable_aux_preserves_all INTR_ENABLE_REC_MAX (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_enable_aux_rpos_within_range:
      ∀ n d d´,
        serial_intr_enable_aux n d = ret d´ →
        0 ≤ rpos (console d) < 512 →
        0 ≤ rpos (console d´) < 512.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        eauto.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H; simpl in *; try assumption.
          functional inversion Hdestruct0; subst; simpl in *; eauto.
          apply Z.mod_bound_pos.
          omega.
          omega.
        }
        {
          inv H.
          eauto.
        }
      }
    Qed.

    Open Scope Z_scope.
    Lemma serial_intr_enable_rpos_within_range:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        0 ≤ rpos (console d) < 512 →
        0 ≤ rpos (console d´) < 512.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_enable_aux_rpos_within_range INTR_ENABLE_REC_MAX (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_enable_aux_cons_buf_length_within_range:
      ∀ n d d´,
        serial_intr_enable_aux n d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        0 ≤ Zlength (cons_buf (console d´)) < 512.
    Proof.
      intros until n.
      induction n.
      {
        simpl.
        intros.
        inv H.
        eauto.
      }
      {
        simpl.
        intros.
        subdestruct.
        {
          eapply IHn in H; simpl in *; try eassumption.
          functional inversion Hdestruct0; simpl in *; eauto.
          split. apply Zlength_ge_0. omega.
          split. apply Zlength_ge_0. repeat solve_list. repeat toZ.
          omega.
          generalize _x10. repeat solve_list. intros. omega. omega.
          generalize _x10. repeat solve_list. intros. omega.
        }
        {
          inv H; eauto.
        }
      }
    Qed.

    Lemma serial_intr_enable_cons_buf_length_within_range:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        0 ≤ Zlength (cons_buf (console d´)) < 512.
    Proof.
      intros.
      functional inversion H; simpl;
      apply (serial_intr_enable_aux_cons_buf_length_within_range INTR_ENABLE_REC_MAX (d { in_intr : true}) d0); assumption.
    Qed.

    Lemma serial_intr_enable_aux_cons_buf_tl_length_within_range:
      ∀ n d d´ x tl,
        serial_intr_enable_aux n d = ret d´ →
        0 ≤ Zlength (cons_buf (console d)) < 512 →
        cons_buf (console d´) = x :: tl →
        0 ≤ Zlength tl < 512.
    Proof.
      intros.
      generalize (serial_intr_enable_aux_cons_buf_length_within_range n d d´ H H0).
      rewrite H1. generalize H0. solve_list.
      intros. split. apply Zlength_ge_0. omega.
    Qed.

    Require Import FutureTactic.
    Lemma serial_intr_enable_cr2_injection:
      ∀ d d´ m,
        serial_intr_enable_spec d = ret d´ →
        val_inject (Mem.flat_inj m) (snd (ti d)) (snd (ti d)) →
        val_inject (Mem.flat_inj m) (snd (ti d´)) (snd (ti d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_cr2_type:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        Val.has_type (snd (ti d)) Tint →
        Val.has_type (snd (ti d´)) Tint.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_kctxt_INJECT:
      ∀ d d´ m,
        serial_intr_enable_spec d = ret d´ →
        kctxt_inject_neutral (kctxt d) m →
        kctxt_inject_neutral (kctxt d´) m.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_uctxt_INJECT:
      ∀ d d´ m,
        serial_intr_enable_spec d = ret d´ →
        uctxt_inject_neutral (uctxt d) m →
        uctxt_inject_neutral (uctxt d´) m.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_VMCS_inject_neutral:
      ∀ d d´ m,
        serial_intr_enable_spec d = ret d´ →
        VMCSPool_inject_neutral (vmcs d) m →
        VMCSPool_inject_neutral (vmcs d´) m.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_VMX_inject_neutral:
      ∀ d d´ m,
        serial_intr_enable_spec d = ret d´ →
        VMXPool_inject_neutral (vmx d) m →
        VMXPool_inject_neutral (vmx d´) m.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_Container_valid:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        Container_valid (AC d) →
        Container_valid (AC d´).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. assumption.
    Qed.

    Lemma serial_intr_enable_valid_preinit_container:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = false →
         ∀ x : Z, 0 ≤ x < num_proc → cused (ZMap.get x (AC d)) ≠ true) →
        (init d´ = false →
         ∀ x : Z, 0 ≤ x < num_proc → cused (ZMap.get x (AC d´)) ≠ true).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_preserves_ikernhost:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        ikern d = true ∧ ihost d = true →
        ikern d´ = true ∧ ihost d´ = true.
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_kern:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (ikern d = false → pg d = true ∧ init d = true) →
        (ikern d´ = false → pg d´ = true ∧ init d´ = true).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_mm:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → MM_valid (MM d) (MMSize d)) →
        (init d´ = true → MM_valid (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_correct_mm:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → MM_correct (MM d) (MMSize d)) →
        (init d´ = true → MM_correct (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_mm_kern:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → MM_kern (MM d) (MMSize d)) →
        (init d´ = true → MM_kern (MM d´) (MMSize d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_mm_size:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → 0 < MMSize d ≤ Int.max_unsigned) →
        (init d´ = true → 0 < MMSize d´ ≤ Int.max_unsigned).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_CR4:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (pg d = true → CR3_valid (CR3 d)) →
        (pg d´ = true → CR3_valid (CR3 d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_nps:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → 262144 ≤ nps d ≤ 1048576) →
        (init d´ = true → 262144 ≤ nps d´ ≤ 1048576).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_AT_kern:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → AT_kern (AT d) (nps d)) →
        (init d´ = true → AT_kern (AT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_AT_usr:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = true → AT_usr (AT d) (nps d)) →
        (init d´ = true → AT_usr (AT d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_valid_pperm:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (consistent_ppage (AT d) (pperm d) (nps d)) →
        (consistent_ppage (AT d´) (pperm d´) (nps d´)).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.

    Lemma serial_intr_enable_init_pperm:
      ∀ d d´,
        serial_intr_enable_spec d = ret d´ →
        (init d = false → pperm d = ZMap.init PGUndef) →
        (init d´ = false → pperm d´ = ZMap.init PGUndef).
    Proof.
      intros. generalize (serial_intr_enable_preserves_all d d´ H).
      intros Hpre. blast Hpre. eauto.
    Qed.