Library mcertikos.multithread.phbthread.AuxSingleAbstractDataType
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem2.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import INVLemmaContainer.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import GlobalOracleProp.
Require Import BigStepGlobalOracle.
Require Import DeviceStateDataType.
Require Import SingleAbstractDataType.
Require Import SingleOracle.
Require Import I64Layer.
Section SINGLEDATAINSTANCE.
Record sharedData :=
mk_sharedData {
CPU_ID: Z;
MM: MMTable;
MMSize: Z;
vmxinfo: VMXInfo;
CR3: globalpointer;
pg: bool;
cid: ZMap.t Z;
lock: Lock;
nps: Z;
init: bool;
idpde: IDPDE;
big_log: BigLogType;
big_oracle: BigOracle
}.
Definition sh_update_CPU_ID (a: sharedData) b :=
mk_sharedData b (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_MM (a: sharedData) b :=
mk_sharedData (CPU_ID a) b (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_MMSize (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) b (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_vmxinfo (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) b (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_CR3 (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) b (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_pg (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) b (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_cid (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) b
(lock a) (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_lock (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
b (nps a) (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_nps (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) b (init a) (idpde a) (big_log a) (big_oracle a).
Definition sh_update_init (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) b (idpde a) (big_log a) (big_oracle a).
Definition sh_update_idpde (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) b (big_log a) (big_oracle a).
Definition sh_update_big_log (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) b (big_oracle a).
Definition sh_update_big_oracle (a: sharedData) b :=
mk_sharedData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (pg a) (cid a)
(lock a) (nps a) (init a) (idpde a) (big_log a) b.
Record privData :=
mk_privData {
ti: trapinfo;
ikern: bool;
ihost: bool;
HP: flatmem;
AC : Container;
uctxt : UContext;
pperm: PPermT;
PT: Z;
ptpool: PMapPool;
ipt: bool;
syncchpool : SyncChanPool;
buffer: PageBufferPool;
ept: EPT;
vmcs: VMCS;
vmx: VMX;
com1: SerialData;
drv_serial: SerialDriver;
console_concrete: ConsoleDriverConcrete;
console: ConsoleDriver;
ioapic: IoApicData;
lapic: LApicData;
tf: TrapFrames;
tf_reg: val;
temporary place to save an intermediate tf regiter
curr_intr_num: Z;
intr_flag: bool;
saved_intr_flags: list bool;
in_intr: bool;
i_dev_serial: bool
}.
Definition pv_update_ti (a: privData) b :=
mk_privData b (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ikern (a: privData) b :=
mk_privData (ti a) b (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ihost (a: privData) b :=
mk_privData (ti a) (ikern a) b (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_HP (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) b (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_AC (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) b (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_uctxt (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) b (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_pperm (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) b (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_PT (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) b (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ptpool (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) b (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ipt (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) b
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_syncchpool (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
b (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_buffer (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) b (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ept (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) b (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_vmcs (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) b (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_vmx (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) b (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_com1 (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) b (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_drv_serial (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) b (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_console_concrete (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) b (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_console (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) b
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ioapic (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
b (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_lapic (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) b (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_tf (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) b (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_tf_reg (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) b (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_curr_intr_num (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) b (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_intr_flag (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) b (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_saved_intr_flags (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) b (in_intr a)
(i_dev_serial a).
Definition pv_update_in_intr (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) b
(i_dev_serial a).
Definition pv_update_i_dev_serial (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
b.
End SINGLEDATAINSTANCE.
Notation "a ´{´ ´sh_CPU_ID´ : x }" := (sh_update_CPU_ID a x) (at level 1).
Notation "a ´{´ ´sh_MM´ : x }" := (sh_update_MM a x) (at level 1).
Notation "a ´{´ ´sh_MSize´ : x }" := (sh_update_MMSize a x) (at level 1).
Notation "a ´{´ ´sh_vmxinfo´ : x }" := (sh_update_vmxinfo a x) (at level 1).
Notation "a ´{´ ´sh_CR3´ : x }" := (sh_update_CR3 a x) (at level 1).
Notation "a ´{´ ´sh_pg´ : x }" := (sh_update_pg a x) (at level 1).
Notation "a ´{´ ´sh_cid´ : x }" := (sh_update_cid a x) (at level 1).
Notation "a ´{´ ´sh_lock´ : x }" := (sh_update_lock a x) (at level 1).
Notation "a ´{´ ´sh_nps´ : x }" := (sh_update_nps a x) (at level 1).
Notation "a ´{´ ´sh_init´ : x }" := (sh_update_init a x) (at level 1).
Notation "a ´{´ ´sh_idpde´ : x }" := (sh_update_idpde a x) (at level 1).
Notation "a ´{´ ´sh_big_log´ : x }" := (sh_update_big_log a x) (at level 1).
Notation "a ´{´ ´sh_big_oracle´ : x }" := (sh_update_big_oracle a x) (at level 1).
Notation "a ´{´ ´pv_ti´ : x }" := (pv_update_ti a x) (at level 1).
Notation "a ´{´ ´pv_ikern´ : x }" := (pv_update_ikern a x) (at level 1).
Notation "a ´{´ ´pv_ihost´ : x }" := (pv_update_ihost a x) (at level 1).
Notation "a ´{´ ´pv_HP´ : x }" := (pv_update_HP a x) (at level 1).
Notation "a ´{´ ´pv_AC´ : x }" := (pv_update_AC a x) (at level 1).
Notation "a ´{´ ´pv_uctxt´ : x }" := (pv_update_uctxt a x) (at level 1).
Notation "a ´{´ ´pv_pperm´ : x }" := (pv_update_pperm a x) (at level 1).
Notation "a ´{´ ´pv_PT´ : x }" := (pv_update_PT a x) (at level 1).
Notation "a ´{´ ´pv_ptpool´ : x }" := (pv_update_ptpool a x) (at level 1).
Notation "a ´{´ ´pv_ipt´ : x }" := (pv_update_ipt a x) (at level 1).
Notation "a ´{´ ´pv_syncchpool´ : x }" := (pv_update_syncchpool a x) (at level 1).
Notation "a ´{´ ´pv_buffer´ : x }" := (pv_update_buffer a x) (at level 1).
Notation "a ´{´ ´pv_ept´ : x }" := (pv_update_ept a x) (at level 1).
Notation "a ´{´ ´pv_vmcs´ : x }" := (pv_update_vmcs a x) (at level 1).
Notation "a ´{´ ´pv_vmx´ : x }" := (pv_update_vmx a x) (at level 1).
Notation "a ´{´ ´pv_com1´ : x }" := (pv_update_com1 a x) (at level 1).
Notation "a ´{´ ´pv_drv_serial´ : x }" := (pv_update_drv_serial a x) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ : x }" := (pv_update_console_concrete a x) (at level 1).
Notation "a ´{´ ´pv_console´ : x }" := (pv_update_console a x) (at level 1).
Notation "a ´{´ ´pv_ioapic´ : x }" := (pv_update_ioapic a x) (at level 1).
Notation "a ´{´ ´pv_lapic´ : x }" := (pv_update_lapic a x) (at level 1).
Notation "a ´{´ ´pv_tf´ : x }" := (pv_update_tf a x) (at level 1).
Notation "a ´{´ ´pv_tf_reg´ : x }" := (pv_update_tf_reg a x) (at level 1).
Notation "a ´{´ ´pv_curr_intr_num´ : x }" := (pv_update_curr_intr_num a x) (at level 1).
Notation "a ´{´ ´pv_intr_flag´ : x }" := (pv_update_intr_flag a x) (at level 1).
Notation "a ´{´ ´pv_saved_intr_flags´ : x }" := (pv_update_saved_intr_flags a x) (at level 1).
Notation "a ´{´ ´pv_in_intr´ : x }" := (pv_update_in_intr a x) (at level 1).
Notation "a ´{´ ´pv_i_dev_serial´ : x }" := (pv_update_i_dev_serial a x) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Base´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Base (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´SerialOn´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_SerialOn (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´SerialIrq´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_SerialIrq (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´RxIntEnable´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_RxIntEnable (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´TxBuf´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_TxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´RxBuf´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_RxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´DLAB´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_DLAB (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Baudrate´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Baudrate (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Databits´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Databits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Stopbits´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Stopbits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Parity´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Parity (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Fifo´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Fifo (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Modem´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Modem (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ : x }" := (pv_update_com1 a (update_s (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l1´ : x }" := (pv_update_com1 a (update_l1 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l2´ : x }" := (pv_update_com1 a (update_l2 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l3´ : x }" := (pv_update_com1 a (update_l3 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_drv_serial´ ´/´ ´serial_exists´ : x }"
:= (pv_update_drv_serial a (update_serial_exists (drv_serial (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´cons_buf_concrete´ : x }"
:= (pv_update_console_concrete a (update_cons_buf_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´rpos_concrete´ : x }"
:= (pv_update_console_concrete a (update_rpos_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´wpos_concrete´ : x }"
:= (pv_update_console_concrete a (update_wpos_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console´ ´/´ ´cons_buf´ : x }" := (pv_update_console a (update_cons_buf (console (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console´ ´/´ ´rpos´ : x }" := (pv_update_console a (update_rpos (console (a)) x)) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) x)) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicInit´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicInit (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´CurrentIrq´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_CurrentIrq (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicBase´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicBase (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicId´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicId (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicMaxIntr´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicMaxIntr (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicIrqs (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ ´[´ n ´]´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a))
(update_IoApicIrqs (s ((ioapic (a))))
(replace x n (IoApicIrqs (s (ioapic a))))))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicEnables (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ ´[´ n ´]´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a))
(update_IoApicEnables (s ((ioapic (a))))
(replace x n (IoApicEnables (s (ioapic a))))))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ : x }" := (pv_update_lapic a (update_s (lapic (a)) x)) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEsr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEsr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEoi´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEoi (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicMaxLvt´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicMaxLvt (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEnable´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEnable (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicSpurious´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicSpurious (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLint0Mask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLint0Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLint1Mask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLint1Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicPcIntMask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicPcIntMask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLdr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLdr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicErrorIrq´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicErrorIrq (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEsrClrPen´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEsrClrPen (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicTpr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicTpr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_regs´ : x }"
:= (pv_update_tf a (replace (update_tf_regs (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_trapno´ : x }"
:= (pv_update_tf a (replace (update_tf_trapno (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_err´ : x }"
:= (pv_update_tf a (replace (update_tf_err (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_esp´ : x }"
:= (pv_update_tf a (replace (update_tf_esp (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Ltac unfold_PData :=
try unfold sh_update_CPU_ID; simpl;
try unfold sh_update_MM; simpl;
try unfold sh_update_MMSize; simpl;
try unfold sh_update_vmxinfo; simpl;
try unfold sh_update_CR3; simpl;
try unfold sh_update_pg; simpl;
try unfold sh_update_lock; simpl;
try unfold sh_update_cid; simpl;
try unfold sh_update_nps; simpl;
try unfold sh_update_init; simpl;
try unfold sh_update_idpde; simpl;
try unfold sh_update_big_log; simpl;
try unfold sh_update_big_oracle; simpl;
try unfold pv_update_ti; simpl;
try unfold pv_update_ikern; simpl;
try unfold pv_update_ihost; simpl;
try unfold pv_update_HP; simpl;
try unfold pv_update_AC; simpl;
try unfold pv_update_uctxt; simpl;
try unfold pv_update_pperm; simpl;
try unfold pv_update_PT; simpl;
try unfold pv_update_ptpool; simpl;
try unfold pv_update_ipt; simpl;
try unfold pv_update_syncchpool; simpl;
try unfold pv_update_buffer; simpl;
try unfold pv_update_ept; simpl;
try unfold pv_update_vmcs; simpl;
try unfold pv_update_vmx; simpl;
try unfold pv_update_com1; simpl;
try unfold pv_update_drv_serial; simpl;
try unfold pv_update_console_concrete; simpl;
try unfold pv_update_console; simpl;
try unfold pv_update_ioapic; simpl;
try unfold pv_update_lapic; simpl;
try unfold pv_update_tf; simpl;
try unfold pv_update_tf_reg; simpl;
try unfold pv_update_curr_intr_num; simpl;
try unfold pv_update_intr_flag; simpl;
try unfold pv_update_saved_intr_flags; simpl;
try unfold pv_update_in_intr; simpl;
try unfold pv_update_i_dev_serial; simpl.
Tactic Notation "unfold_PData_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold sh_update_CPU_ID in T; simpl in T;
try unfold sh_update_MM in T; simpl in T;
try unfold sh_update_MMSize in T; simpl in T;
try unfold sh_update_vmxinfo in T; simpl in T;
try unfold sh_update_CR3 in T; simpl in T;
try unfold sh_update_pg in T; simpl in T;
try unfold sh_update_lock in T; simpl in T;
try unfold sh_update_cid in T; simpl in T;
try unfold sh_update_nps in T; simpl in T;
try unfold sh_update_init in T; simpl in T;
try unfold sh_update_idpde in T; simpl in T;
try unfold sh_update_big_log in T; simpl in T;
try unfold sh_update_big_oracle in T; simpl in T;
try unfold pv_update_ti in T; simpl in T;
try unfold pv_update_ikern in T; simpl in T;
try unfold pv_update_ihost in T; simpl in T;
try unfold pv_update_HP in T; simpl in T;
try unfold pv_update_AC in T; simpl in T;
try unfold pv_update_uctxt in T; simpl in T;
try unfold pv_update_pperm in T; simpl in T;
try unfold pv_update_PT in T; simpl in T;
try unfold pv_update_ptpool in T; simpl in T;
try unfold pv_update_ipt in T; simpl in T;
try unfold pv_update_syncchpool in T; simpl in T;
try unfold pv_update_buffer in T; simpl in T;
try unfold pv_update_ept in T; simpl in T;
try unfold pv_update_vmcs in T; simpl in T;
try unfold pv_update_vmx in T; simpl in T;
try unfold pv_update_com1 in T; simpl in T;
try unfold pv_update_drv_serial in T; simpl in T;
try unfold pv_update_console_concrete in T; simpl in T;
try unfold pv_update_console in T; simpl in T;
try unfold pv_update_ioapic in T; simpl in T;
try unfold pv_update_lapic in T; simpl in T;
try unfold pv_update_tf in T; simpl in T;
try unfold pv_update_tf_reg in T; simpl in T;
try unfold pv_update_curr_intr_num in T; simpl in T;
try unfold pv_update_intr_flag in T; simpl in T;
try unfold pv_update_saved_intr_flags in T; simpl in T;
try unfold pv_update_in_intr in T; simpl in T;
try unfold pv_update_i_dev_serial in T; simpl in T
end.
Section WITH_SINGLE_DATA.
Local Open Scope Z_scope.
Context `{multi_oracle_prop: MultiOracleProp}.
Fixpoint init_cal_cidpool (i: nat) (cidpool: ZMap.t Z) : ZMap.t Z :=
match i with
| O ⇒ ZMap.set 0 1 cidpool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Z.of_nat (S k) + 1) (init_cal_cidpool k cidpool)
end.
Definition init_real_cidpool (cidpool: ZMap.t Z) : ZMap.t Z :=
init_cal_cidpool (Z.to_nat (TOTAL_CPU - 1)) cidpool.
Definition init_shared_adt :=
mk_sharedData GlobalOracle.current_CPU_ID (ZMap.init MMUndef) 0 (ZMap.init 0) GLOBUndef false
(init_real_cidpool (ZMap.init 0))
init_lock 0 false (ZMap.init (ZMap.init IDPTEUndef)) BigUndef big_oracle0.
Definition main_init_priv_adt :=
mk_privData init_trap_info true true FlatMem.empty_flatmem Container_unused
(ZMap.init Vundef) (ZMap.init PGUndef) (-1)
(ZMap.init (ZMap.init PDEUndef)) true (ZMap.init SyncChanUndef)
page_buffer_init
(ZMap.init EPML4EUndef)
(VMCSValid Vzero Vzero (ZMap.init Vundef))
(ZMap.init Vundef)
com1_init serial_drv_init
console_init_concrete console_init_d ioapic_init_d lapic_init_d nil
(Vint Int.zero) 256 true nil false false.
Definition nomain_init_priv_adt :=
mk_privData init_trap_info true true FlatMem.empty_flatmem Container_unused
(ZMap.init Vundef) (ZMap.init PGUndef) 0
(CalRealPT.real_pt (ZMap.init (ZMap.init PDEUndef))) true
(CalRealProcModule.real_syncchpool (ZMap.init SyncChanUndef))
page_buffer_init
(ZMap.init EPML4EUndef)
(VMCSValid Vzero Vzero (ZMap.init Vundef))
(ZMap.init Vundef)
com1_init serial_drv_init
console_init_concrete console_init_d ioapic_init_d lapic_init_d nil
(Vint Int.zero) 256 true nil false false.
Global Instance single_data : SingleData :=
{
dshare := sharedData;
init_dshare := init_shared_adt;
proc_id s := ZMap.get (CPU_ID s) (cid s);
processor_id s := CPU_ID s;
dproc := privData;
main_init_dproc:= main_init_priv_adt;
nomain_init_dproc:= nomain_init_priv_adt
}.
Section LOW_INV.
Definition priv_uctxt_inject_neutral (up: UContext) (n: block) :=
∀ ii,
0≤ ii < UCTXT_SIZE →
let v:= (ZMap.get ii up) in
Val.has_type v AST.Tint
∧ val_inject (Mem.flat_inj n) v v.
Record low_level_invariant (n: block) (adt: PData) :=
mkLowInv {
CR2_INJECT: val_inject (Mem.flat_inj n) (snd (ti (snd adt))) (snd (ti (snd adt)));
CR2_Type: Val.has_type (snd (ti (snd adt))) AST.Tint;
uctxt_INJECT: priv_uctxt_inject_neutral (uctxt (snd adt)) n;
VMCS_INJECT: VMCS_inject_neutral (vmcs (snd adt)) n;
VMX_INJECT: VMX_inject_neutral (vmx (snd adt)) n;
tf_INJECT: tfs_inject_neutral (tf (snd adt)) n
}.
Lemma low_level_invariant_incr:
∀ (n n´: positive) a,
(n ≤ n´)%positive →
low_level_invariant n a →
low_level_invariant n´ a.
Proof.
inversion 2; subst.
intros; constructor; trivial.
- eapply val_inject_incr; [|eauto].
apply flat_inj_inject_incr; trivial.
- unfold priv_uctxt_inject_neutral.
intros; exploit uctxt_INJECT0; eauto.
intros [? ?].
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- inv VMCS_INJECT0.
destruct a; simpl in ×.
Print VMCS_inject_neutral.
rewrite <- H1.
constructor; intros.
destruct (H2 ofs) as (? & ?).
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- inv VMX_INJECT0. constructor; intros.
destruct (H1 ofs) as (? & ?).
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- unfold tfs_inject_neutral in ×.
destruct a; simpl in ×.
induction (tf d0).
constructor.
inv tf_INJECT0.
constructor.
unfold tf_inject_neutral in ×.
intros.
specialize (H3 r).
destruct H3.
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
eapply IHt; auto.
Qed.
Lemma empty_data_low_level_invariant:
∀ n, low_level_invariant n (init_shared_adt, main_init_priv_adt).
Proof.
constructor; simpl; auto.
- econstructor.
- repeat constructor.
+ rewrite ZMap.gi.
econstructor.
+ rewrite ZMap.gi.
econstructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor.
Qed.
Lemma empty_data_low_level_invariant_nomain:
∀ n, low_level_invariant n (init_shared_adt, nomain_init_priv_adt).
Proof.
constructor; simpl; auto.
- econstructor.
- repeat constructor.
+ rewrite ZMap.gi.
econstructor.
+ rewrite ZMap.gi.
econstructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor.
Qed.
End LOW_INV.
End WITH_SINGLE_DATA.
intr_flag: bool;
saved_intr_flags: list bool;
in_intr: bool;
i_dev_serial: bool
}.
Definition pv_update_ti (a: privData) b :=
mk_privData b (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ikern (a: privData) b :=
mk_privData (ti a) b (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ihost (a: privData) b :=
mk_privData (ti a) (ikern a) b (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_HP (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) b (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_AC (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) b (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_uctxt (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) b (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_pperm (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) b (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_PT (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) b (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ptpool (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) b (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ipt (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) b
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_syncchpool (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
b (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_buffer (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) b (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ept (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) b (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_vmcs (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) b (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_vmx (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) b (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_com1 (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) b (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_drv_serial (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) b (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_console_concrete (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) b (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_console (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) b
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_ioapic (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
b (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_lapic (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) b (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_tf (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) b (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_tf_reg (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) b (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_curr_intr_num (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) b (intr_flag a) (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_intr_flag (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) b (saved_intr_flags a) (in_intr a)
(i_dev_serial a).
Definition pv_update_saved_intr_flags (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) b (in_intr a)
(i_dev_serial a).
Definition pv_update_in_intr (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) b
(i_dev_serial a).
Definition pv_update_i_dev_serial (a: privData) b :=
mk_privData (ti a) (ikern a) (ihost a) (HP a) (AC a) (uctxt a) (pperm a) (PT a) (ptpool a) (ipt a)
(syncchpool a) (buffer a) (ept a) (vmcs a) (vmx a) (com1 a) (drv_serial a) (console_concrete a) (console a)
(ioapic a) (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a)
b.
End SINGLEDATAINSTANCE.
Notation "a ´{´ ´sh_CPU_ID´ : x }" := (sh_update_CPU_ID a x) (at level 1).
Notation "a ´{´ ´sh_MM´ : x }" := (sh_update_MM a x) (at level 1).
Notation "a ´{´ ´sh_MSize´ : x }" := (sh_update_MMSize a x) (at level 1).
Notation "a ´{´ ´sh_vmxinfo´ : x }" := (sh_update_vmxinfo a x) (at level 1).
Notation "a ´{´ ´sh_CR3´ : x }" := (sh_update_CR3 a x) (at level 1).
Notation "a ´{´ ´sh_pg´ : x }" := (sh_update_pg a x) (at level 1).
Notation "a ´{´ ´sh_cid´ : x }" := (sh_update_cid a x) (at level 1).
Notation "a ´{´ ´sh_lock´ : x }" := (sh_update_lock a x) (at level 1).
Notation "a ´{´ ´sh_nps´ : x }" := (sh_update_nps a x) (at level 1).
Notation "a ´{´ ´sh_init´ : x }" := (sh_update_init a x) (at level 1).
Notation "a ´{´ ´sh_idpde´ : x }" := (sh_update_idpde a x) (at level 1).
Notation "a ´{´ ´sh_big_log´ : x }" := (sh_update_big_log a x) (at level 1).
Notation "a ´{´ ´sh_big_oracle´ : x }" := (sh_update_big_oracle a x) (at level 1).
Notation "a ´{´ ´pv_ti´ : x }" := (pv_update_ti a x) (at level 1).
Notation "a ´{´ ´pv_ikern´ : x }" := (pv_update_ikern a x) (at level 1).
Notation "a ´{´ ´pv_ihost´ : x }" := (pv_update_ihost a x) (at level 1).
Notation "a ´{´ ´pv_HP´ : x }" := (pv_update_HP a x) (at level 1).
Notation "a ´{´ ´pv_AC´ : x }" := (pv_update_AC a x) (at level 1).
Notation "a ´{´ ´pv_uctxt´ : x }" := (pv_update_uctxt a x) (at level 1).
Notation "a ´{´ ´pv_pperm´ : x }" := (pv_update_pperm a x) (at level 1).
Notation "a ´{´ ´pv_PT´ : x }" := (pv_update_PT a x) (at level 1).
Notation "a ´{´ ´pv_ptpool´ : x }" := (pv_update_ptpool a x) (at level 1).
Notation "a ´{´ ´pv_ipt´ : x }" := (pv_update_ipt a x) (at level 1).
Notation "a ´{´ ´pv_syncchpool´ : x }" := (pv_update_syncchpool a x) (at level 1).
Notation "a ´{´ ´pv_buffer´ : x }" := (pv_update_buffer a x) (at level 1).
Notation "a ´{´ ´pv_ept´ : x }" := (pv_update_ept a x) (at level 1).
Notation "a ´{´ ´pv_vmcs´ : x }" := (pv_update_vmcs a x) (at level 1).
Notation "a ´{´ ´pv_vmx´ : x }" := (pv_update_vmx a x) (at level 1).
Notation "a ´{´ ´pv_com1´ : x }" := (pv_update_com1 a x) (at level 1).
Notation "a ´{´ ´pv_drv_serial´ : x }" := (pv_update_drv_serial a x) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ : x }" := (pv_update_console_concrete a x) (at level 1).
Notation "a ´{´ ´pv_console´ : x }" := (pv_update_console a x) (at level 1).
Notation "a ´{´ ´pv_ioapic´ : x }" := (pv_update_ioapic a x) (at level 1).
Notation "a ´{´ ´pv_lapic´ : x }" := (pv_update_lapic a x) (at level 1).
Notation "a ´{´ ´pv_tf´ : x }" := (pv_update_tf a x) (at level 1).
Notation "a ´{´ ´pv_tf_reg´ : x }" := (pv_update_tf_reg a x) (at level 1).
Notation "a ´{´ ´pv_curr_intr_num´ : x }" := (pv_update_curr_intr_num a x) (at level 1).
Notation "a ´{´ ´pv_intr_flag´ : x }" := (pv_update_intr_flag a x) (at level 1).
Notation "a ´{´ ´pv_saved_intr_flags´ : x }" := (pv_update_saved_intr_flags a x) (at level 1).
Notation "a ´{´ ´pv_in_intr´ : x }" := (pv_update_in_intr a x) (at level 1).
Notation "a ´{´ ´pv_i_dev_serial´ : x }" := (pv_update_i_dev_serial a x) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Base´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Base (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´SerialOn´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_SerialOn (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´SerialIrq´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_SerialIrq (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´RxIntEnable´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_RxIntEnable (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´TxBuf´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_TxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´RxBuf´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_RxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´DLAB´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_DLAB (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Baudrate´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Baudrate (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Databits´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Databits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Stopbits´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Stopbits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Parity´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Parity (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Fifo´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Fifo (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ ´/´ ´Modem´ : x }"
:= (pv_update_com1 a (update_s (com1 (a)) (update_Modem (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´s´ : x }" := (pv_update_com1 a (update_s (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l1´ : x }" := (pv_update_com1 a (update_l1 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l2´ : x }" := (pv_update_com1 a (update_l2 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_com1´ ´/´ ´l3´ : x }" := (pv_update_com1 a (update_l3 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´pv_drv_serial´ ´/´ ´serial_exists´ : x }"
:= (pv_update_drv_serial a (update_serial_exists (drv_serial (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´cons_buf_concrete´ : x }"
:= (pv_update_console_concrete a (update_cons_buf_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´rpos_concrete´ : x }"
:= (pv_update_console_concrete a (update_rpos_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console_concrete´ ´/´ ´wpos_concrete´ : x }"
:= (pv_update_console_concrete a (update_wpos_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console´ ´/´ ´cons_buf´ : x }" := (pv_update_console a (update_cons_buf (console (a)) x)) (at level 1).
Notation "a ´{´ ´pv_console´ ´/´ ´rpos´ : x }" := (pv_update_console a (update_rpos (console (a)) x)) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) x)) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicInit´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicInit (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´CurrentIrq´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_CurrentIrq (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicBase´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicBase (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicId´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicId (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicMaxIntr´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicMaxIntr (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicIrqs (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ ´[´ n ´]´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a))
(update_IoApicIrqs (s ((ioapic (a))))
(replace x n (IoApicIrqs (s (ioapic a))))))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a)) (update_IoApicEnables (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ ´[´ n ´]´ : x }"
:= (pv_update_ioapic a (update_s (ioapic (a))
(update_IoApicEnables (s ((ioapic (a))))
(replace x n (IoApicEnables (s (ioapic a))))))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ : x }" := (pv_update_lapic a (update_s (lapic (a)) x)) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEsr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEsr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEoi´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEoi (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicMaxLvt´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicMaxLvt (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEnable´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEnable (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicSpurious´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicSpurious (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLint0Mask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLint0Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLint1Mask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLint1Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicPcIntMask´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicPcIntMask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicLdr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicLdr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicErrorIrq´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicErrorIrq (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicEsrClrPen´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicEsrClrPen (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_lapic´ ´/´ ´s´ ´/´ ´LapicTpr´ : x }"
:= (pv_update_lapic a (update_s (lapic (a)) (update_LapicTpr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_regs´ : x }"
:= (pv_update_tf a (replace (update_tf_regs (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_trapno´ : x }"
:= (pv_update_tf a (replace (update_tf_trapno (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_err´ : x }"
:= (pv_update_tf a (replace (update_tf_err (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´pv_tf´ ´[´ n ´]´ ´/´ ´tf_esp´ : x }"
:= (pv_update_tf a (replace (update_tf_esp (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Ltac unfold_PData :=
try unfold sh_update_CPU_ID; simpl;
try unfold sh_update_MM; simpl;
try unfold sh_update_MMSize; simpl;
try unfold sh_update_vmxinfo; simpl;
try unfold sh_update_CR3; simpl;
try unfold sh_update_pg; simpl;
try unfold sh_update_lock; simpl;
try unfold sh_update_cid; simpl;
try unfold sh_update_nps; simpl;
try unfold sh_update_init; simpl;
try unfold sh_update_idpde; simpl;
try unfold sh_update_big_log; simpl;
try unfold sh_update_big_oracle; simpl;
try unfold pv_update_ti; simpl;
try unfold pv_update_ikern; simpl;
try unfold pv_update_ihost; simpl;
try unfold pv_update_HP; simpl;
try unfold pv_update_AC; simpl;
try unfold pv_update_uctxt; simpl;
try unfold pv_update_pperm; simpl;
try unfold pv_update_PT; simpl;
try unfold pv_update_ptpool; simpl;
try unfold pv_update_ipt; simpl;
try unfold pv_update_syncchpool; simpl;
try unfold pv_update_buffer; simpl;
try unfold pv_update_ept; simpl;
try unfold pv_update_vmcs; simpl;
try unfold pv_update_vmx; simpl;
try unfold pv_update_com1; simpl;
try unfold pv_update_drv_serial; simpl;
try unfold pv_update_console_concrete; simpl;
try unfold pv_update_console; simpl;
try unfold pv_update_ioapic; simpl;
try unfold pv_update_lapic; simpl;
try unfold pv_update_tf; simpl;
try unfold pv_update_tf_reg; simpl;
try unfold pv_update_curr_intr_num; simpl;
try unfold pv_update_intr_flag; simpl;
try unfold pv_update_saved_intr_flags; simpl;
try unfold pv_update_in_intr; simpl;
try unfold pv_update_i_dev_serial; simpl.
Tactic Notation "unfold_PData_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold sh_update_CPU_ID in T; simpl in T;
try unfold sh_update_MM in T; simpl in T;
try unfold sh_update_MMSize in T; simpl in T;
try unfold sh_update_vmxinfo in T; simpl in T;
try unfold sh_update_CR3 in T; simpl in T;
try unfold sh_update_pg in T; simpl in T;
try unfold sh_update_lock in T; simpl in T;
try unfold sh_update_cid in T; simpl in T;
try unfold sh_update_nps in T; simpl in T;
try unfold sh_update_init in T; simpl in T;
try unfold sh_update_idpde in T; simpl in T;
try unfold sh_update_big_log in T; simpl in T;
try unfold sh_update_big_oracle in T; simpl in T;
try unfold pv_update_ti in T; simpl in T;
try unfold pv_update_ikern in T; simpl in T;
try unfold pv_update_ihost in T; simpl in T;
try unfold pv_update_HP in T; simpl in T;
try unfold pv_update_AC in T; simpl in T;
try unfold pv_update_uctxt in T; simpl in T;
try unfold pv_update_pperm in T; simpl in T;
try unfold pv_update_PT in T; simpl in T;
try unfold pv_update_ptpool in T; simpl in T;
try unfold pv_update_ipt in T; simpl in T;
try unfold pv_update_syncchpool in T; simpl in T;
try unfold pv_update_buffer in T; simpl in T;
try unfold pv_update_ept in T; simpl in T;
try unfold pv_update_vmcs in T; simpl in T;
try unfold pv_update_vmx in T; simpl in T;
try unfold pv_update_com1 in T; simpl in T;
try unfold pv_update_drv_serial in T; simpl in T;
try unfold pv_update_console_concrete in T; simpl in T;
try unfold pv_update_console in T; simpl in T;
try unfold pv_update_ioapic in T; simpl in T;
try unfold pv_update_lapic in T; simpl in T;
try unfold pv_update_tf in T; simpl in T;
try unfold pv_update_tf_reg in T; simpl in T;
try unfold pv_update_curr_intr_num in T; simpl in T;
try unfold pv_update_intr_flag in T; simpl in T;
try unfold pv_update_saved_intr_flags in T; simpl in T;
try unfold pv_update_in_intr in T; simpl in T;
try unfold pv_update_i_dev_serial in T; simpl in T
end.
Section WITH_SINGLE_DATA.
Local Open Scope Z_scope.
Context `{multi_oracle_prop: MultiOracleProp}.
Fixpoint init_cal_cidpool (i: nat) (cidpool: ZMap.t Z) : ZMap.t Z :=
match i with
| O ⇒ ZMap.set 0 1 cidpool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Z.of_nat (S k) + 1) (init_cal_cidpool k cidpool)
end.
Definition init_real_cidpool (cidpool: ZMap.t Z) : ZMap.t Z :=
init_cal_cidpool (Z.to_nat (TOTAL_CPU - 1)) cidpool.
Definition init_shared_adt :=
mk_sharedData GlobalOracle.current_CPU_ID (ZMap.init MMUndef) 0 (ZMap.init 0) GLOBUndef false
(init_real_cidpool (ZMap.init 0))
init_lock 0 false (ZMap.init (ZMap.init IDPTEUndef)) BigUndef big_oracle0.
Definition main_init_priv_adt :=
mk_privData init_trap_info true true FlatMem.empty_flatmem Container_unused
(ZMap.init Vundef) (ZMap.init PGUndef) (-1)
(ZMap.init (ZMap.init PDEUndef)) true (ZMap.init SyncChanUndef)
page_buffer_init
(ZMap.init EPML4EUndef)
(VMCSValid Vzero Vzero (ZMap.init Vundef))
(ZMap.init Vundef)
com1_init serial_drv_init
console_init_concrete console_init_d ioapic_init_d lapic_init_d nil
(Vint Int.zero) 256 true nil false false.
Definition nomain_init_priv_adt :=
mk_privData init_trap_info true true FlatMem.empty_flatmem Container_unused
(ZMap.init Vundef) (ZMap.init PGUndef) 0
(CalRealPT.real_pt (ZMap.init (ZMap.init PDEUndef))) true
(CalRealProcModule.real_syncchpool (ZMap.init SyncChanUndef))
page_buffer_init
(ZMap.init EPML4EUndef)
(VMCSValid Vzero Vzero (ZMap.init Vundef))
(ZMap.init Vundef)
com1_init serial_drv_init
console_init_concrete console_init_d ioapic_init_d lapic_init_d nil
(Vint Int.zero) 256 true nil false false.
Global Instance single_data : SingleData :=
{
dshare := sharedData;
init_dshare := init_shared_adt;
proc_id s := ZMap.get (CPU_ID s) (cid s);
processor_id s := CPU_ID s;
dproc := privData;
main_init_dproc:= main_init_priv_adt;
nomain_init_dproc:= nomain_init_priv_adt
}.
Section LOW_INV.
Definition priv_uctxt_inject_neutral (up: UContext) (n: block) :=
∀ ii,
0≤ ii < UCTXT_SIZE →
let v:= (ZMap.get ii up) in
Val.has_type v AST.Tint
∧ val_inject (Mem.flat_inj n) v v.
Record low_level_invariant (n: block) (adt: PData) :=
mkLowInv {
CR2_INJECT: val_inject (Mem.flat_inj n) (snd (ti (snd adt))) (snd (ti (snd adt)));
CR2_Type: Val.has_type (snd (ti (snd adt))) AST.Tint;
uctxt_INJECT: priv_uctxt_inject_neutral (uctxt (snd adt)) n;
VMCS_INJECT: VMCS_inject_neutral (vmcs (snd adt)) n;
VMX_INJECT: VMX_inject_neutral (vmx (snd adt)) n;
tf_INJECT: tfs_inject_neutral (tf (snd adt)) n
}.
Lemma low_level_invariant_incr:
∀ (n n´: positive) a,
(n ≤ n´)%positive →
low_level_invariant n a →
low_level_invariant n´ a.
Proof.
inversion 2; subst.
intros; constructor; trivial.
- eapply val_inject_incr; [|eauto].
apply flat_inj_inject_incr; trivial.
- unfold priv_uctxt_inject_neutral.
intros; exploit uctxt_INJECT0; eauto.
intros [? ?].
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- inv VMCS_INJECT0.
destruct a; simpl in ×.
Print VMCS_inject_neutral.
rewrite <- H1.
constructor; intros.
destruct (H2 ofs) as (? & ?).
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- inv VMX_INJECT0. constructor; intros.
destruct (H1 ofs) as (? & ?).
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
- unfold tfs_inject_neutral in ×.
destruct a; simpl in ×.
induction (tf d0).
constructor.
inv tf_INJECT0.
constructor.
unfold tf_inject_neutral in ×.
intros.
specialize (H3 r).
destruct H3.
split; try assumption.
eapply val_inject_incr; try eassumption.
apply flat_inj_inject_incr; trivial.
eapply IHt; auto.
Qed.
Lemma empty_data_low_level_invariant:
∀ n, low_level_invariant n (init_shared_adt, main_init_priv_adt).
Proof.
constructor; simpl; auto.
- econstructor.
- repeat constructor.
+ rewrite ZMap.gi.
econstructor.
+ rewrite ZMap.gi.
econstructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor.
Qed.
Lemma empty_data_low_level_invariant_nomain:
∀ n, low_level_invariant n (init_shared_adt, nomain_init_priv_adt).
Proof.
constructor; simpl; auto.
- econstructor.
- repeat constructor.
+ rewrite ZMap.gi.
econstructor.
+ rewrite ZMap.gi.
econstructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor. intros. subst v. repeat rewrite ZMap.gi.
split; constructor.
- constructor.
Qed.
End LOW_INV.
End WITH_SINGLE_DATA.