Library mcertikos.layerlib.Constant

Require Import Coqlib.
Require Import Integers.
Require Import Values.

Notation num_proc:= 1024.

Notation TOTAL_CPU := 8.
Notation NUM_VMS := TOTAL_CPU.
Notation max_children := TOTAL_CPU.
Notation READ_Q_START := 0.
Notation MSG_Q_START := (READ_Q_START + TOTAL_CPU).
Notation SLEEP_Q_START := (MSG_Q_START + TOTAL_CPU).
Notation num_cv := num_proc.
Notation TDQ_SIZE := (SLEEP_Q_START + num_proc).
Notation num_chan:= TDQ_SIZE.
Notation max_resource_size := 1.

Notation kern_low:= 262144.
Notation kern_high:= 983040.
Notation PgSize:= 4096.
Notation maxpage:= 1048576.
Notation one_k := 1024.
Notation adr_max := 4294967296.
Notation adr_low := 1073741824.
Notation adr_high := 4026531840.
Notation MagicNumber := (maxpage + 1).

Notation root_quota := 720896.

Notation PT_PERM_UP := 0.
Notation PT_PERM_P := 1. Notation PT_PERM_PTKF := 3. Notation PT_PERM_PTKT := 259. Notation PT_PERM_PTU := 7.
Notation TSTATE_READY := 0.
Notation TSTATE_RUN := 1.
Notation TSTATE_SLEEP := 2.
Notation TSTATE_DEAD := 3.
Notation NPTEPERM := 7.
Notation NPDEPERM := 39.
Notation EPTEPERM := 7.
Notation EPDTEPERM := 39.
Notation VMCB_V_SIZE := 16.
Notation VMCB_Z_SIZE := 1008.
Notation XVMST_SIZE := 6.

Notation U_EDI := 0.
Notation U_ESI := 1.
Notation U_EBP := 2.
Notation U_OESP := 3.
Notation U_EBX := 4.
Notation U_EDX := 5.
Notation U_ECX := 6.
Notation U_EAX := 7.
Notation U_ES := 8.
Notation U_DS := 9.
Notation U_TRAPNO := 10.
Notation U_ERR := 11.
Notation U_EIP := 12.
Notation U_CS := 13.
Notation U_EFLAGS := 14.
Notation U_ESP := 15.
Notation U_SS := 16.

Notation UCTXT_SIZE := 17.
Notation STACK_TOP:= (Int.repr (kern_high × PgSize)).
Notation CPU_GDT_UDATA := (Vint (Int.repr 35)).
Notation CPU_GDT_UCODE := (Vint (Int.repr 27)).
Notation FL_IF := (Vint (Int.repr 512)).

Notation VMCB_Z_INTCEPT_LO_OFFSET := 3.
Notation VMCB_Z_INTCEPT_HI_OFFSET := 4.
Notation VMCB_Z_GASID_OFFSET := 22.
Notation VMCB_Z_INT_CTL_OFFSET := 24.
Notation VMCB_Z_INT_STATE_OFFSET := 26.
Notation VMCB_Z_EXITCODE_LO_OFFSET := 28.
Notation VMCB_Z_EXITINFO1_LO_OFFSET := 30.
Notation VMCB_Z_EXITINFO2_LO_OFFSET := 32.
Notation VMCB_Z_EXITINTINFO_LO_OFFSET := 34.
Notation VMCB_Z_EXITINTINFO_HI_OFFSET := 35.
Notation VMCB_Z_NESTED_CTL_OFFSET := 36.
Notation VMCB_Z_EVENTINJ_LO_OFFSET := 42.
Notation VMCB_Z_EVENTINJ_HI_OFFSET := 43.
Notation VMCB_Z_NEXT_RIP_LO_OFFSET := 50.

Notation VMCB_Z_ES_OFFSET := 256.
Notation VMCB_Z_CS_OFFSET := 260.
Notation VMCB_Z_SS_OFFSET := 264.
Notation VMCB_Z_DS_OFFSET := 268.
Notation VMCB_Z_FS_OFFSET := 272.
Notation VMCB_Z_GS_OFFSET := 276.
Notation VMCB_Z_GDTR_OFFSET := 280.
Notation VMCB_Z_LDTR_OFFSET := 284.
Notation VMCB_Z_IDTR_OFFSET := 288.
Notation VMCB_Z_TR_OFFSET := 292.

Notation VMCB_Z_EFER_LO_OFFSET := 308.
Notation VMCB_Z_DR7_LO_OFFSET := 344.
Notation VMCB_Z_DR6_LO_OFFSET := 346.
Notation VMCB_Z_GPAT_LO_OFFSET := 410.
Notation VMCB_Z_GPAT_HI_OFFSET := 411.

Notation VMCB_V_CR4_LO_OFFSET := 338.
Notation VMCB_V_CR3_LO_OFFSET := 340.
Notation VMCB_V_CR0_LO_OFFSET := 342.
Notation VMCB_V_RFLAGS_LO_OFFSET := 348.
Notation VMCB_V_RIP_LO_OFFSET := 350.
Notation VMCB_V_RSP_LO_OFFSET := 374.
Notation VMCB_V_RAX_LO_OFFSET := 382.
Notation VMCB_V_CR2_LO_OFFSET := 400.

Notation VMEXIT_VINTR := 96.
Notation VMEXIT_IOIO := 123.
Notation VMEXIT_NPF := 1024.

Notation VMCB_INTCEPT_VINT_SHIFT := 4.

Notation VMCB_INT_CTL_VIRQ_SHIFT := 8.
Notation VMCB_INT_CTL_IGN_TPR_SHIFT := 20.

Notation VMCB_EVENTINJ_VALID_SHIFT := 31.
Notation VMCB_EVENTINJ_EV_SHIFT := 11.
Notation VMCB_EVENTINJ_TYPE_SHIFT := 8.
Notation VMCB_EVENTINJ_TYPE_INTR := 0.
Notation VMCB_EVENTINJ_TYPE_EXCPT := 3.

Notation VMCB_SEG_ATTR_SHIFT := 2.
Notation VMCB_SEG_LIM_SHIFT := 4.
Notation VMCB_SEG_BASE_SHIFT := 8.

Notation EXIT_INTINFO_VALID_SHIFT := 31.
Notation EXIT_INTINFO_TYPE_SHIFT := 8.
Notation EXIT_INTINFO_TYPE_MASK := (Z.shiftl 7 EXIT_INTINFO_TYPE_SHIFT).
Notation EXIT_INTINFO_TYPE_INTR := 0.
Notation EXIT_INTINFO_VECTOR_MASK := 255.

Notation XVMST_EBX_OFFSET := 0.
Notation XVMST_ECX_OFFSET := 1.
Notation XVMST_EDX_OFFSET := 2.
Notation XVMST_ESI_OFFSET := 3.
Notation XVMST_EDI_OFFSET := 4.
Notation XVMST_EBP_OFFSET := 5.

Notation G_CS := 0.
Notation G_DS := 1.
Notation G_ES := 2.
Notation G_FS := 3.
Notation G_GS := 4.
Notation G_SS := 5.
Notation G_LDTR := 6.
Notation G_TR := 7.
Notation G_GDTR := 8.
Notation G_IDTR := 9.
Notation MAX_SEG := 10.

Notation G_EAX := 0.
Notation G_EBX := 1.
Notation G_ECX := 2.
Notation G_EDX := 3.
Notation G_ESI := 4.
Notation G_EDI := 5.
Notation G_EBP := 6.
Notation G_ESP := 7.
Notation G_EIP := 8.
Notation G_EFLAGS := 9.
Notation G_CR0 := 10.
Notation G_CR2 := 11.
Notation G_CR3 := 12.
Notation G_CR4 := 13.

Definition sz32_mask := Z.shiftl 1 6.
Definition sz16_mask := Z.shiftl 1 5.
Definition sz8_mask := Z.shiftl 1 4.
Definition rep_mask := Z.shiftl 1 3.
Definition str_mask := Z.shiftl 1 2.

Notation in_mask := 1.
Notation SZ8 := 0.
Notation SZ16 := 1.
Notation SZ32 := 2.

Notation SHARED_MEM_READY := 0.
Notation SHARED_MEM_PEND := 1.
Notation SHARED_MEM_DEAD := 2.


Notation EPT_SIZE:= 8413184.
Notation GDT_OFFSET:= 0.
Notation TSS_OFFSET:= 48.

Notation five_one_two := 512.
Notation C_VMCS_VPID := 0 .
Notation C_VMCS_GUEST_ES_SELECTOR := 2048 .
Notation C_VMCS_GUEST_CS_SELECTOR := 2050 .
Notation C_VMCS_GUEST_SS_SELECTOR := 2052 .
Notation C_VMCS_GUEST_DS_SELECTOR := 2054 .
Notation C_VMCS_GUEST_FS_SELECTOR := 2056 .
Notation C_VMCS_GUEST_GS_SELECTOR := 2058 .
Notation C_VMCS_GUEST_LDTR_SELECTOR := 2060 .
Notation C_VMCS_GUEST_TR_SELECTOR := 2062 .
Notation C_VMCS_HOST_ES_SELECTOR := 3072 .
Notation C_VMCS_HOST_CS_SELECTOR := 3074 .
Notation C_VMCS_HOST_SS_SELECTOR := 3076 .
Notation C_VMCS_HOST_DS_SELECTOR := 3078 .
Notation C_VMCS_HOST_FS_SELECTOR := 3080 .
Notation C_VMCS_HOST_GS_SELECTOR := 3082 .
Notation C_VMCS_HOST_TR_SELECTOR := 3084 .
Notation C_VMCS_IO_BITMAP_A := 8192 .
Notation C_VMCS_IO_BITMAP_A_HI := 8193 .
Notation C_VMCS_IO_BITMAP_B := 8194 .
Notation C_VMCS_IO_BITMAP_B_HI := 8195 .
Notation C_VMCS_MSR_BITMAP := 8196 .
Notation C_VMCS_MSR_BITMAP_HI := 8197 .
Notation C_VMCS_EXIT_MSR_STORE := 8198 .
Notation C_VMCS_EXIT_MSR_LOAD := 8200 .
Notation C_VMCS_ENTRY_MSR_LOAD := 8202 .
Notation C_VMCS_EXECUTIVE_VMCS := 8204 .
Notation C_VMCS_TSC_OFFSET := 8208 .
Notation C_VMCS_VIRTUAL_APIC := 8210 .
Notation C_VMCS_APIC_ACCESS := 8212 .
Notation C_VMCS_EPTP := 8218 .
Notation C_VMCS_EPTP_HI := 8219 .
Notation C_VMCS_GUEST_PHYSICAL_ADDRESS := 9216 .
Notation C_VMCS_LINK_POINTER := 10240 .
Notation C_VMCS_GUEST_IA32_DEBUGCTL := 10242 .
Notation C_VMCS_GUEST_IA32_PAT := 10244 .
Notation C_VMCS_GUEST_IA32_EFER := 10246 .
Notation C_VMCS_GUEST_IA32_PERF_GLOBAL_CTRL := 10248 .
Notation C_VMCS_GUEST_PDPTE0 := 10250 .
Notation C_VMCS_GUEST_PDPTE1 := 10252 .
Notation C_VMCS_GUEST_PDPTE2 := 10254 .
Notation C_VMCS_GUEST_PDPTE3 := 10256 .
Notation C_VMCS_HOST_IA32_PAT := 11264 .
Notation C_VMCS_HOST_IA32_EFER := 11266 .
Notation C_VMCS_HOST_IA32_PERF_GLOBAL_CTRL := 11268 .
Notation C_VMCS_PIN_BASED_CTLS := 16384 .
Notation C_VMCS_PRI_PROC_BASED_CTLS := 16386 .
Notation C_VMCS_EXCEPTION_BITMAP := 16388 .
Notation C_VMCS_PF_ERROR_MASK := 16390 .
Notation C_VMCS_PF_ERROR_MATCH := 16392 .
Notation C_VMCS_CR3_TARGET_COUNT := 16394 .
Notation C_VMCS_EXIT_CTLS := 16396 .
Notation C_VMCS_EXIT_MSR_STORE_COUNT := 16398 .
Notation C_VMCS_EXIT_MSR_LOAD_COUNT := 16400 .
Notation C_VMCS_ENTRY_CTLS := 16402 .
Notation C_VMCS_ENTRY_MSR_LOAD_COUNT := 16404 .
Notation C_VMCS_ENTRY_INTR_INFO := 16406 .
Notation C_VMCS_ENTRY_EXCEPTION_ERROR := 16408 .
Notation C_VMCS_ENTRY_INST_LENGTH := 16410 .
Notation C_VMCS_TPR_THRESHOLD := 16412 .
Notation C_VMCS_SEC_PROC_BASED_CTLS := 16414 .
Notation C_VMCS_PLE_GAP := 16416 .
Notation C_VMCS_PLE_WINDOW := 16418 .
Notation C_VMCS_INSTRUCTION_ERROR := 17408 .
Notation C_VMCS_EXIT_REASON := 17410 .
Notation C_VMCS_EXIT_INTERRUPTION_INFO := 17412 .
Notation C_VMCS_EXIT_INTERRUPTION_ERROR := 17414 .
Notation C_VMCS_IDT_VECTORING_INFO := 17416 .
Notation C_VMCS_IDT_VECTORING_ERROR := 17418 .
Notation C_VMCS_EXIT_INSTRUCTION_LENGTH := 17420 .
Notation C_VMCS_EXIT_INSTRUCTION_INFO := 17422 .
Notation C_VMCS_GUEST_ES_LIMIT := 18432 .
Notation C_VMCS_GUEST_CS_LIMIT := 18434 .
Notation C_VMCS_GUEST_SS_LIMIT := 18436 .
Notation C_VMCS_GUEST_DS_LIMIT := 18438 .
Notation C_VMCS_GUEST_FS_LIMIT := 18440 .
Notation C_VMCS_GUEST_GS_LIMIT := 18442 .
Notation C_VMCS_GUEST_LDTR_LIMIT := 18444 .
Notation C_VMCS_GUEST_TR_LIMIT := 18446 .
Notation C_VMCS_GUEST_GDTR_LIMIT := 18448 .
Notation C_VMCS_GUEST_IDTR_LIMIT := 18450 .
Notation C_VMCS_GUEST_ES_ACCESS_RIGHTS := 18452 .
Notation C_VMCS_GUEST_CS_ACCESS_RIGHTS := 18454 .
Notation C_VMCS_GUEST_SS_ACCESS_RIGHTS := 18456 .
Notation C_VMCS_GUEST_DS_ACCESS_RIGHTS := 18458 .
Notation C_VMCS_GUEST_FS_ACCESS_RIGHTS := 18460 .
Notation C_VMCS_GUEST_GS_ACCESS_RIGHTS := 18462 .
Notation C_VMCS_GUEST_LDTR_ACCESS_RIGHTS := 18464 .
Notation C_VMCS_GUEST_TR_ACCESS_RIGHTS := 18466 .
Notation C_VMCS_GUEST_INTERRUPTIBILITY := 18468 .
Notation C_VMCS_GUEST_ACTIVITY := 18470 .
Notation C_VMCS_GUEST_SMBASE := 18472 .
Notation C_VMCS_GUEST_IA32_SYSENTER_CS := 18474 .
Notation C_VMCS_PREEMPTION_TIMER_VALUE := 18478 .
Notation C_VMCS_HOST_IA32_SYSENTER_CS := 19456 .
Notation C_VMCS_CR0_MASK := 24576 .
Notation C_VMCS_CR4_MASK := 24578 .
Notation C_VMCS_CR0_SHADOW := 24580 .
Notation C_VMCS_CR4_SHADOW := 24582 .
Notation C_VMCS_CR3_TARGET0 := 24584 .
Notation C_VMCS_CR3_TARGET1 := 24586 .
Notation C_VMCS_CR3_TARGET2 := 24588 .
Notation C_VMCS_CR3_TARGET3 := 24590 .
Notation C_VMCS_EXIT_QUALIFICATION := 25600 .
Notation C_VMCS_IO_RCX := 25602 .
Notation C_VMCS_IO_RSI := 25604 .
Notation C_VMCS_IO_RDI := 25606 .
Notation C_VMCS_IO_RIP := 25608 .
Notation C_VMCS_GUEST_LINEAR_ADDRESS := 25610 .
Notation C_VMCS_GUEST_CR0 := 26624 .
Notation C_VMCS_GUEST_CR3 := 26626 .
Notation C_VMCS_GUEST_CR4 := 26628 .
Notation C_VMCS_GUEST_ES_BASE := 26630 .
Notation C_VMCS_GUEST_CS_BASE := 26632 .
Notation C_VMCS_GUEST_SS_BASE := 26634 .
Notation C_VMCS_GUEST_DS_BASE := 26636 .
Notation C_VMCS_GUEST_FS_BASE := 26638 .
Notation C_VMCS_GUEST_GS_BASE := 26640 .
Notation C_VMCS_GUEST_LDTR_BASE := 26642 .
Notation C_VMCS_GUEST_TR_BASE := 26644 .
Notation C_VMCS_GUEST_GDTR_BASE := 26646 .
Notation C_VMCS_GUEST_IDTR_BASE := 26648 .
Notation C_VMCS_GUEST_DR7 := 26650 .
Notation C_VMCS_GUEST_RSP := 26652 .
Notation C_VMCS_GUEST_RIP := 26654 .
Notation C_VMCS_GUEST_RFLAGS := 26656 .
Notation C_VMCS_GUEST_PENDING_DBG_EXCEPTIONS := 26658 .
Notation C_VMCS_GUEST_IA32_SYSENTER_ESP := 26660 .
Notation C_VMCS_GUEST_IA32_SYSENTER_EIP := 26662 .
Notation C_VMCS_HOST_CR0 := 27648 .
Notation C_VMCS_HOST_CR3 := 27650 .
Notation C_VMCS_HOST_CR4 := 27652 .
Notation C_VMCS_HOST_FS_BASE := 27654 .
Notation C_VMCS_HOST_GS_BASE := 27656 .
Notation C_VMCS_HOST_TR_BASE := 27658 .
Notation C_VMCS_HOST_GDTR_BASE := 27660 .
Notation C_VMCS_HOST_IDTR_BASE := 27662 .
Notation C_VMCS_HOST_IA32_SYSENTER_ESP := 27664 .
Notation C_VMCS_HOST_IA32_SYSENTER_EIP := 27666 .
Notation C_VMCS_HOST_RSP := 27668 .
Notation C_VMCS_HOST_RIP := 27670 .
Notation MAX_INT_16 := 65535.
Notation MAX_INT_32 := 4294967296.
Notation MAX_INT_64 := 18446744073709551616.


Notation VMX_G_RAX := 0.
Notation VMX_G_RBX := 8.
Notation VMX_G_RCX := 16.
Notation VMX_G_RDX := 24.
Notation VMX_G_RSI := 32.
Notation VMX_G_RDI := 40.
Notation VMX_G_RBP := 48.
Notation VMX_G_RIP := 56.
Notation VMX_G_CR2 := 64.
Notation VMX_G_DR0 := 68.
Notation VMX_G_DR1 := 72.
Notation VMX_G_DR2 := 76.
Notation VMX_G_DR3 := 80.
Notation VMX_G_DR6 := 84.
Notation VMX_ENTER_TSC0 := 88.
Notation VMX_ENTER_TSC1 := 92.
Notation VMX_EXIT_TSC0 := 96.
Notation VMX_EXIT_TSC1 := 100.
Notation VMX_VPID := 104.
Notation VMX_EXIT_REASON := 108.
Notation VMX_EXIT_QUALIFICATION := 112.
Notation VMX_PENDING_INTR := 120.
Notation VMX_LAUNCHED := 124.
Notation VMX_FAILED := 128.
Notation VMX_HOST_EBP := 132.
Notation VMX_HOST_EDI := 136.
Notation VMX_HOST_EIP := 140.
Notation VMX_STOPPED := 144.
Notation VMX_VDISK_IDX := 148.
Notation VMX_Size := 152.

Notation VMX_G_RAX´ := 0.
Notation VMX_G_RBX´ := 2.
Notation VMX_G_RCX´ := 4.
Notation VMX_G_RDX´ := 6.
Notation VMX_G_RSI´ := 8.
Notation VMX_G_RDI´ := 10.
Notation VMX_G_RBP´ := 12.
Notation VMX_G_RIP´ := 14.
Notation VMX_G_CR2´ := 16.
Notation VMX_G_DR0´ := 17.
Notation VMX_G_DR1´ := 18.
Notation VMX_G_DR2´ := 19.
Notation VMX_G_DR3´ := 20.
Notation VMX_G_DR6´ := 21.
Notation VMX_ENTER_TSC0´ := 22.
Notation VMX_ENTER_TSC1´ := 23.
Notation VMX_EXIT_TSC0´ := 24.
Notation VMX_EXIT_TSC1´ := 25.
Notation VMX_VPID´ := 26.
Notation VMX_EXIT_REASON´ := 27.
Notation VMX_EXIT_QUALIFICATION´ := 28.
Notation VMX_PENDING_INTR´ := 30.
Notation VMX_LAUNCHED´ := 31.
Notation VMX_FAILED´ := 32.
Notation VMX_HOST_EBP´ := 33.
Notation VMX_HOST_EDI´ := 34.
Notation VMX_HOST_EIP´ := 35.
Notation VMX_STOPPED´ := 36.
Notation VMX_VDISK_IDX´ := 37.
Notation VMX_Size´ := 38.

Notation C_GUEST_EAX := 0.
Notation C_GUEST_EBX := 1.
Notation C_GUEST_ECX := 2.
Notation C_GUEST_EDX := 3.
Notation C_GUEST_ESI := 4.
Notation C_GUEST_EDI := 5.
Notation C_GUEST_EBP := 6.
Notation C_GUEST_ESP := 7.
Notation C_GUEST_EIP := 8.
Notation C_GUEST_EFLAGS := 9.
Notation C_GUEST_CR0 := 10.
Notation C_GUEST_CR2 := 11.
Notation C_GUEST_CR3 := 12.
Notation C_GUEST_CR4 := 13.
Notation C_GUEST_MAX_REG := 14.

Notation C_GUEST_CS := 0.
Notation C_GUEST_DS := 1.
Notation C_GUEST_ES := 2.
Notation C_GUEST_FS := 3.
Notation C_GUEST_GS := 4.
Notation C_GUEST_SS := 5.
Notation C_GUEST_LDTR := 6.
Notation C_GUEST_TR := 7.
Notation C_GUEST_GDTR := 8.
Notation C_GUEST_IDTR := 9.
Notation C_GUEST_MAX_SEG_DESC := 10.

Notation MSR_VMX_BASIC := 1152.
Notation VM_VGA_LO := 655360.
Notation VM_VGA_HI := 1703936.

Notation EXIT_QUAL_IO_ONE_BYTE := 0.
Notation EXIT_QUAL_IO_TWO_BYTE := 1.
Notation EXIT_QUAL_IO_FOUR_BYTE := 4.
Notation EXIT_QUAL_IO_SIZE := 7.

Notation EXIT_QUAL_IO_OUT := 0.
Notation EXIT_QUAL_IO_IN := 1.
Notation EXIT_QUAL_IO_DIR := 3.

Notation EXIT_REASON_MASK := 65535.
Notation PROCBASED_INT_WINDOW_EXITING := 4.

Notation VMCS_INTERRUPTION_INFO_VALID := 2147483648. Notation VMCS_INTERRUPTION_INFO_EV := 2048.
Notation VMCS_INTERRUPTIBILITY_STI_BLOCKING := 1.
Notation VMCS_INTERRUPTIBILITY_MOVSS_BLOCKING := 2.
Notation VMCS_INTERRUPTIBILITY_STI_or_MOVSS_BLOCKING := 3.

Notation CPU_GDT_KDATA := 16. Notation CPU_GDT_KCODE := 8. Notation CPU_GDT_TSS := 40.
Notation MSR_IA32_SYSENTER_CS := 372. Notation MSR_IA32_SYSENTER_ESP := 373. Notation MSR_IA32_SYSENTER_EIP := 374. Notation MSR_PAT := 631. Notation MSR_IA32_PERF_GLOBAL_CTRL := 911. Notation MSR_EFER := 3221225600.
Notation CR0_PE := 1. Notation CR0_MP := 2. Notation CR0_EM := 4. Notation CR0_TS := 8. Notation CR0_NE := 32. Notation CR0_WP := 65536. Notation CR0_AM := 262144. Notation CR0_PG := 2147483648.
Notation v0x60000010 := 1610612752. Notation CR4_VMXE := 8192. Notation v0x00000400 := 1024. Notation v0x7040600070406 := 1974748653749254. Notation v0xffffffffffffffff := 18446744073709551615.

Notation EXIT_QUAL_IO_REP := 5.
Notation EXIT_QUAL_IO_STR := 4.
Notation EXIT_REASON_ENTRY_FAIL := 2147483648. Notation C_EXIT_QUAL_IO_PORT := 65536.
Notation v0xffffffff := 4294967295.
Notation v0xfff0 := 65520.
Notation v0xffff0ff0 := 4294905840.


Notation EPT_NO_PERM:= 4294967288. Notation EPT_ADDR_OFFSET_MASK := 4095.

Notation EPT_PG_IGNORE_PAT_or_PERM:= 71.
Notation EPT_ADDR_MASK := 4294963200. Notation EPT_PG_MEMORY_TYPE := 3.

Notation EPTP_pml4 := 30.
Notation T_MCHK_SHIFT := 262144.

Notation VMX_INFO_VMX_ENABLED := 1.
Notation VMX_INFO_PINBASED_CTLS := 2.
Notation VMX_INFO_PROCBASED_CTLS := 3.
Notation VMX_INFO_PROCBASED_CTLS2 := 4.
Notation VMX_INFO_EXIT_CTLS := 5.
Notation VMX_INFO_ENTRY_CTLS := 6.
Notation VMX_INFO_CR0_ONES_MASK := 7.
Notation VMX_INFO_CR0_ZEROS_MASK := 8.
Notation VMX_INFO_CR4_ONES_MASK := 9.
Notation VMX_INFO_CR4_ZEROS_MASK := 10.
Notation VMX_INFO_VMX_REGION := 11.

Notation E_SUCC := 0. Notation E_MEM := 1. Notation E_IPC := 2.
Notation E_INVAL_CALLNR := 3. Notation E_INVAL_ADDR := 4. Notation E_INVAL_PID := 5. Notation E_INVAL_REG := 6.
Notation E_INVAL_SEG := 7.
Notation E_INVAL_EVENT := 8.
Notation E_INVAL_PORT := 9.
Notation E_INVAL_HVM := 10.
Notation E_INVAL_CHID := 11.
Notation E_DISK_OP := 12. Notation E_HVM_VMRUN := 13.
Notation E_HVM_MMAP := 14.
Notation E_HVM_REG := 15.
Notation E_HVM_SEG := 16.
Notation E_HVM_NEIP := 17.
Notation E_HVM_INJECT := 18.
Notation E_HVM_IOPORT := 19.
Notation E_HVM_MSR := 20.
Notation E_HVM_INTRWIN := 21.
Notation MAX_ERROR_NR := 22.

Notation v0xfffff000 := 4294963200.

Notation EXIT_REASON_CR_ACCESS := 28.
Notation EXIT_REASON_INOUT:= 30.
Notation EXIT_REASON_EPT_FAULT:= 48.

Notation SYS_puts := 0. Notation SYS_ring0_spawn := 1. Notation SYS_spawn := 2. Notation SYS_yield := 3. Notation SYS_sleep := 4.
Notation SYS_disk_op := 5. Notation SYS_disk_cap := 6. Notation SYS_is_chan_ready := 7.
Notation SYS_send := 8.
Notation SYS_recv := 9.
Notation SYS_get_tsc_per_ms := 10.
Notation SYS_hvm_run_vm := 11.
Notation SYS_hvm_get_exitinfo := 12.
Notation SYS_hvm_mmap := 13.
Notation SYS_hvm_set_seg := 14.
Notation SYS_hvm_set_reg := 15.
Notation SYS_hvm_get_reg := 16.
Notation SYS_hvm_get_next_eip := 17.
Notation SYS_hvm_inject_event := 18.
Notation SYS_hvm_check_int_shadow := 19.
Notation SYS_hvm_check_pending_event := 20.
Notation SYS_hvm_intercept_int_window := 21.
Notation SYS_hvm_get_tsc_offset := 22.
Notation SYS_hvm_set_tsc_offset := 23.
Notation SYS_hvm_handle_rdmsr := 24.
Notation SYS_hvm_handle_wrmsr := 25.
Notation SYS_get_quota := 26.
Notation SYS_getc := 27.
Notation SYS_putc := 28.
Notation SYS_hvm_hypervisor_mode := 29.
Notation SYS_getkey := 30.
Notation SYS_vputc := 31.
Notation SYS_cpuidx := 32.
Notation SYS_get_pid := 33.
Notation SYS_get_cpu_nums := 34.
Notation SYS_hvm_get_cur_vconsole := 35.
Notation SYS_hvm_set_cur_vconsole := 36.
Notation SYS_save_vga_buffer := 37.
Notation SYS_restore_vga_buffer := 38.
Notation SYS_hvm_stop_vm := 39.
Notation SYS_hvm_set_seg1 := 40.
Notation SYS_hvm_set_seg2 := 41.
Notation MAX_SYSCALL_NR := 42.

Notation PortCom1Base := 1016.
Notation PortCom2Base := 760.
Notation PortCom3Base := 998.
Notation PortCom4Base := 744.

Notation PortComRx := 0.
Notation PortComTx := 0.
Notation PortComDll := 0.
Notation PortComDlm := 1.
Notation PortComIER := 1.
Notation PortComIIR := 2.
Notation PortComFCR := 2.
Notation PortComLCR := 3.
Notation PortComMCR := 4.
Notation PortComLSR := 5.

Notation COM_LCR_DLAB := 128. Notation COM_DEFAULT_BAUDRATE := 115200.

Notation CONSOLE_BUFFER_SIZE := 512.

Notation KEYBOARD_HW_BUF_SIZE := 6%nat.
Notation KEYBOARD_SW_BUF_SIZE := 512%Z.
Notation KEY_ESC := 0%Z.
Notation KEY_F12 := 87%Z.
Notation KEY_PAD := 88%Z.
Notation KEY_APP := 93%Z.
Notation KEY_PRINT_SCREEN := 98%Z.
Notation KEY_PAUSE := 99%Z.
Notation SCODE_DAUL_KEY:= 224%Z.

Notation IRQ0 := 32%Z.

Notation IOAPIC_ID := 0.
Notation IOAPIC_VER := 1.
Notation IOAPIC_TABLE_BASE := 16.

Notation LAPIC_IDX_TPR := 32.
Notation LAPIC_IDX_EOI := 44.
Notation LAPIC_IDX_SVR := 60.
Notation LAPIC_IDX_DFR := 56.
Notation LAPIC_IDX_LDR := 52.
Notation LAPIC_IDX_ESR := 160.
Notation LAPIC_IDX_LVT_PMC := 208.
Notation LAPIC_IDX_LVT_LINT0 := 212.
Notation LAPIC_IDX_LVT_LINT1 := 216.
Notation LAPIC_IDX_ERROR := 220.

Notation INTR_DISABLE_REC_MAX := 100%nat.
Notation INTR_ENABLE_REC_MAX := 100%nat.

Notation TRAPNO_EXCEPTIONS_BEGIN := 0.
Notation TRAPNO_EXCEPTIONS_END := 30.
Notation TRAPNO_IOAPIC_BEGIN := 32.
Notation TRAPNO_IOAPIC_END := 55.
Notation TRAPNO_SYSCALL := 56.
Notation TRAPNO_CMCI := 57.
Notation TRAPNO_MSI_BEGIN := 72.
Notation TRAPNO_PASSTHROUGH := 112.
Notation TRAPNO_DEFAULT := 254.
Notation TRAPNO_MAX := 256.

Notation MAX_IRQ_NUM := 257%nat.