Library mcertikos.invariants.INVLemmaInterrupt
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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.
Section INTERRUPT_INV.
Section INTR_DISABLE.
Lemma serial_intr_disable_aux_preserves_all:
∀ n masked d d´,
serial_intr_disable_aux n masked d = ret 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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
VMCS_inject_neutral (vmcs d) m →
VMCS_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´ →
VMX_inject_neutral (vmx d) m →
VMX_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 < 64 → cused (ZMap.get x (AC d)) ≠ true) →
(init d´ = false →
∀ x : Z, 0 ≤ x < 64 → 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.
for MPT
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 < 64) →
(pg d´ = true → 0 ≤ PT d´ < 64).
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.
End INTR_DISABLE.
Section INTR_ENABLE.
Lemma serial_intr_enable_aux_preserves_all:
∀ n d d´,
serial_intr_enable_aux n d = ret 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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
VMCS_inject_neutral (vmcs d) m →
VMCS_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´ →
VMX_inject_neutral (vmx d) m →
VMX_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 < 64 → cused (ZMap.get x (AC d)) ≠ true) →
(init d´ = false →
∀ x : Z, 0 ≤ x < 64 → 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.
∀ 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 < 64) →
(pg d´ = true → 0 ≤ PT d´ < 64).
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.
End INTR_DISABLE.
Section INTR_ENABLE.
Lemma serial_intr_enable_aux_preserves_all:
∀ n d d´,
serial_intr_enable_aux n d = ret 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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
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´ ∧
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´ ∧
pb d = pb 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´.
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´ →
VMCS_inject_neutral (vmcs d) m →
VMCS_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´ →
VMX_inject_neutral (vmx d) m →
VMX_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 < 64 → cused (ZMap.get x (AC d)) ≠ true) →
(init d´ = false →
∀ x : Z, 0 ≤ x < 64 → 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.
for MPT
Lemma serial_intr_enable_valid_kern_pt:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_iptt:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(ipt d = true → ikern d = true) →
(ipt d´ = true → ikern d´ = true).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_iptf:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(ikern d = false → ipt d = false) →
(ikern d´ = false → ipt d´ = false).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PMap:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PMap_kern:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PT:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(pg d = true → 0 ≤ PT d < 64) →
(pg d´ = true → 0 ≤ PT d´ < 64).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_dirty:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(dirty_ppage (pperm d) (HP d)) →
(dirty_ppage (pperm d´) (HP d´)).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_uninitialized:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_ihost:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_preserves_tf:
∀ d d´,
serial_intr_enable_spec d = Some d´ →
tf d = tf d´.
Proof.
intros.
generalize (serial_intr_enable_preserves_all d d´ H); intro.
destruct H0 as [? Htmp].
repeat (destruct Htmp as [? Htmp]; try assumption).
Qed.
End INTR_ENABLE.
End INTERRUPT_INV.
Create HintDb serial_intr_disable_invariantdb discriminated.
Hint Resolve serial_intr_disable_cr2_injection: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_cr2_type: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_kctxt_INJECT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_uctxt_INJECT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_VMCS_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_VMX_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_Container_valid: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_preinit_container: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_rpos_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_cons_buf_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_preserves_ikernhost: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_correct_mm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm_size: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_CR4: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_ihost: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_nps: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_AT_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_AT_usr: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_pperm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_init_pperm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_kern_pt: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_iptt: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_iptf: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PMap: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PMap_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_dirty: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_uninitialized: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_preserves_all: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_rpos_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_cons_buf_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_cons_buf_tl_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_preserves_tf: serial_intr_disable_invariantdb.
Create HintDb serial_intr_enable_invariantdb discriminated.
Hint Resolve serial_intr_enable_cr2_injection: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_cr2_type: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_kctxt_INJECT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_uctxt_INJECT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_VMCS_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_VMX_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_Container_valid: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_preinit_container: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_rpos_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_cons_buf_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_preserves_ikernhost: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_correct_mm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm_size: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_CR4: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_ihost: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_nps: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_AT_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_AT_usr: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_pperm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_init_pperm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_kern_pt: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_iptt: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_iptf: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PMap: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PMap_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_dirty: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_uninitialized: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_preserves_all: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_rpos_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_cons_buf_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_cons_buf_tl_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_preserves_tf: serial_intr_enable_invariantdb.
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_iptt:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(ipt d = true → ikern d = true) →
(ipt d´ = true → ikern d´ = true).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_iptf:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(ikern d = false → ipt d = false) →
(ikern d´ = false → ipt d´ = false).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PMap:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PMap_kern:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_PT:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(pg d = true → 0 ≤ PT d < 64) →
(pg d´ = true → 0 ≤ PT d´ < 64).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_dirty:
∀ d d´,
serial_intr_enable_spec d = ret d´ →
(dirty_ppage (pperm d) (HP d)) →
(dirty_ppage (pperm d´) (HP d´)).
Proof.
intros. generalize (serial_intr_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_uninitialized:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_valid_ihost:
∀ d d´,
serial_intr_enable_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_enable_preserves_all d d´ H).
intros Hpre. blast Hpre. eauto.
Qed.
Lemma serial_intr_enable_preserves_tf:
∀ d d´,
serial_intr_enable_spec d = Some d´ →
tf d = tf d´.
Proof.
intros.
generalize (serial_intr_enable_preserves_all d d´ H); intro.
destruct H0 as [? Htmp].
repeat (destruct Htmp as [? Htmp]; try assumption).
Qed.
End INTR_ENABLE.
End INTERRUPT_INV.
Create HintDb serial_intr_disable_invariantdb discriminated.
Hint Resolve serial_intr_disable_cr2_injection: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_cr2_type: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_kctxt_INJECT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_uctxt_INJECT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_VMCS_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_VMX_inject_neutral: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_Container_valid: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_preinit_container: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_rpos_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_cons_buf_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_preserves_ikernhost: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_correct_mm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_mm_size: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_CR4: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_ihost: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_nps: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_AT_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_AT_usr: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_pperm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_init_pperm: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_kern_pt: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_iptt: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_iptf: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PMap: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PMap_kern: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_PT: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_dirty: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_valid_uninitialized: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_preserves_all: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_rpos_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_cons_buf_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_aux_cons_buf_tl_length_within_range: serial_intr_disable_invariantdb.
Hint Resolve serial_intr_disable_preserves_tf: serial_intr_disable_invariantdb.
Create HintDb serial_intr_enable_invariantdb discriminated.
Hint Resolve serial_intr_enable_cr2_injection: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_cr2_type: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_kctxt_INJECT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_uctxt_INJECT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_VMCS_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_VMX_inject_neutral: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_Container_valid: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_preinit_container: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_rpos_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_cons_buf_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_preserves_ikernhost: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_correct_mm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_mm_size: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_CR4: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_ihost: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_nps: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_AT_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_AT_usr: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_pperm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_init_pperm: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_kern_pt: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_iptt: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_iptf: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PMap: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PMap_kern: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_PT: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_dirty: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_valid_uninitialized: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_preserves_all: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_rpos_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_cons_buf_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_aux_cons_buf_tl_length_within_range: serial_intr_enable_invariantdb.
Hint Resolve serial_intr_enable_preserves_tf: serial_intr_enable_invariantdb.