Library mcertikos.objects.ObjTrap
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealProcModule.
Require Import liblayers.compat.CompatGenSem.
Require Import ObjArg.
Require Import ObjProc.
Require Import ObjSyncIPC.
Require Import ObjThread.
Require Import ObjFlatMem.
Require Import ObjBigThread.
Require Import GlobIdent.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjSerialDriver.
Require Import ObjVMX.
Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Section OBJ_Trap.
Context `{real_params: RealParams}.
Context `{multi_oralce_prop: MultiOracleProp}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Function sys_getc_spec (abd: RData) : option RData :=
match thread_serial_intr_disable_spec abd with
| Some d1 ⇒
match thread_cons_buf_read_spec d1 with
| Some (d2, x) ⇒
if zle_le 0 x 255 then
match thread_serial_intr_enable_spec d2 with
| Some d3 ⇒
match uctx_set_retval1_spec x d3 with
| Some d4 ⇒ uctx_set_errno_spec E_SUCC d4
| None ⇒ None
end
| None ⇒ None
end
else None
| None ⇒ None
end
| None ⇒ None
end.
Function sys_putc_spec (abd: RData) : option RData :=
match uctx_arg2_spec abd with
| Some c ⇒
if zle_le 0 c 255 then
match thread_serial_intr_disable_spec abd with
| Some d1 ⇒
match thread_serial_putc_spec c d1 with
| Some d2 ⇒
match thread_serial_intr_enable_spec d2 with
| Some d3 ⇒ uctx_set_errno_spec E_SUCC d3
| None ⇒ None
end
| None ⇒ None
end
| None ⇒ None
end
else None
| None ⇒ None
end.
Function trap_sendtochan_spec (abd: RData) : option RData :=
match uctx_arg2_spec abd with
| Some chid ⇒
match uctx_arg3_spec abd with
| Some vaddr ⇒
match uctx_arg4_spec abd with
| Some scount ⇒
match thread_syncsendto_chan_spec chid vaddr scount abd with
| Some (abd0, r) ⇒
match uctx_set_retval1_spec r abd0 with
| Some abd1 ⇒
uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_receivechan_spec (abd: RData) :=
match uctx_arg2_spec abd with
| Some chanid ⇒
match uctx_arg3_spec abd with
| Some vaddr ⇒
match uctx_arg4_spec abd with
| Some rcount ⇒
match thread_syncreceive_chan_spec chanid vaddr rcount abd with
| Some (abd0, r) ⇒
match uctx_set_retval1_spec r abd0 with
| Some abd1 ⇒
uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_get_quota_spec (abd: RData) :=
match thread_get_curid_spec abd with
| Some curid ⇒
match thread_container_get_quota_spec curid abd with
| Some quota ⇒
match thread_container_get_usage_spec curid abd with
| Some usage ⇒
match uctx_set_retval1_spec (quota - usage) abd with
| Some abd0 ⇒
uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_intercept_int_window_spec (abd: RData) :=
match uctx_arg2_spec abd with
| Some enable ⇒
match thread_vmx_set_intercept_intwin_spec enable abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_check_pending_event_spec (abd: RData) :=
match thread_vmx_check_pending_event_spec abd with
| Some event ⇒
match uctx_set_retval1_spec event abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_check_int_shadow_spec (abd: RData) :=
match thread_vmx_check_int_shadow_spec abd with
| Some shadow ⇒
match uctx_set_retval1_spec shadow abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_inject_event_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd, uctx_arg4_spec abd with
| Some vector, Some err, Some evmerged ⇒
match thread_vmx_inject_event_spec (evmerged / 256) vector err (evmerged mod 256) abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _,_,_ ⇒ None
end.
Function trap_get_next_eip_spec (abd: RData) :=
match thread_vmx_get_next_eip_spec abd with
| Some neip ⇒
if zle_le 0 neip Int.max_unsigned then
match uctx_set_retval1_spec neip abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function trap_set_reg_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd with
| Some r, Some v ⇒
if zle_lt C_GUEST_EAX r C_GUEST_MAX_REG then
match thread_vmx_set_reg_spec r v abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
else
uctx_set_errno_spec E_INVAL_REG abd
| _,_ ⇒ None
end.
Function trap_get_reg_spec (abd: RData) :=
match uctx_arg2_spec abd with
| Some r ⇒
if zle_lt C_GUEST_EAX r C_GUEST_MAX_REG then
match thread_vmx_get_reg_spec r abd with
| Some v ⇒
match uctx_set_retval1_spec v abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _ ⇒ None
end
else
uctx_set_errno_spec E_INVAL_REG abd
| _ ⇒ None
end.
Function trap_set_seg1_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd, uctx_arg4_spec abd with
| Some seg, Some sel, Some base ⇒
if zle_lt C_GUEST_CS seg C_GUEST_MAX_SEG_DESC then
match thread_vmx_set_desc1_spec seg sel base abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
else
uctx_set_errno_spec E_INVAL_SEG abd
| _,_,_ ⇒ None
end.
Function trap_set_seg2_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd, uctx_arg4_spec abd with
| Some seg, Some lim, Some ar ⇒
if zle_lt C_GUEST_CS seg C_GUEST_MAX_SEG_DESC then
match thread_vmx_set_desc2_spec seg lim ar abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
else
uctx_set_errno_spec E_INVAL_SEG abd
| _,_,_ ⇒ None
end.
Function trap_get_tsc_offset_spec (abd: RData) :=
match thread_vmx_get_tsc_offset_spec abd with
| Some (VZ64 ofs) ⇒
let ofs1 := ofs / (2 ^ 32) in
let ofs2 := ofs mod (2 ^ 32) in
match uctx_set_retval1_spec ofs1 abd with
| Some abd0 ⇒
match uctx_set_retval2_spec ofs2 abd0 with
| Some abd1 ⇒
uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_set_tsc_offset_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd with
| Some ofs_high, Some ofs_low ⇒
let ofs := ofs_high × (2 ^ 32) + ofs_low in
match thread_vmx_set_tsc_offset_spec (VZ64 ofs) abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _,_ ⇒ None
end.
Function trap_mmap_spec (abd: RData) :=
match uctx_arg2_spec abd, uctx_arg3_spec abd, uctx_arg4_spec abd with
| Some gpa, Some hva, Some mem_type ⇒
if andb (andb (Zdivide_dec PgSize hva HPS)
(Zdivide_dec PgSize gpa HPS))
(orb (zle_le VM_VGA_LO hva (VM_VGA_HI - PgSize))
(zle_le adr_low hva (adr_high - PgSize))) then
match thread_ptRead_spec (ZMap.get (CPU_ID abd) (cid abd)) hva abd with
| Some hpa ⇒
if zle_le 0 hpa Int.max_unsigned then
if zeq (Z.land hpa PT_PERM_P) 0 then
match big2_ptResv_spec (ZMap.get (CPU_ID abd) (cid abd)) hva PT_PERM_PTU abd with
| Some (abd0, _) ⇒
match thread_ptRead_spec (ZMap.get (CPU_ID abd) (cid abd)) hva abd0 with
| Some hpa´ ⇒
if zle_le 0 hpa´ Int.max_unsigned then
let hpa0 := (Z.land hpa´ v0xfffff000) + (hva mod PgSize) in
match thread_vmx_set_mmap_spec gpa hpa0 mem_type abd0 with
| Some (abd1, _) ⇒ uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
else
let hpa0 := (Z.land hpa v0xfffff000) + (hva mod PgSize) in
match thread_vmx_set_mmap_spec gpa hpa0 mem_type abd with
| Some (abd1, _) ⇒ uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
else None
| _ ⇒ None
end
else uctx_set_errno_spec E_INVAL_ADDR abd
| _,_,_ ⇒ None
end.
Function get_flags (width write rep str: Z) :=
let flags := 0 in
let flags0 := if zeq write 0 then flags
else Z.lor flags 1 in
let flags1 := if zeq rep 0 then flags0
else Z.lor flags0 2 in
let flags2 := if zeq str 0 then flags1
else Z.lor flags1 4 in
Z.lor flags2 (width × 8).
Function trap_get_exitinfo_spec (abd: RData) :=
match thread_vmx_get_exit_reason_spec abd, thread_vmx_get_exit_io_port_spec abd,
thread_vmx_get_io_width_spec abd, thread_vmx_get_io_write_spec abd,
thread_vmx_get_exit_io_rep_spec abd, thread_vmx_get_exit_io_str_spec abd,
thread_vmx_get_exit_fault_addr_spec abd, thread_vmx_get_exit_qualification_spec abd with
| Some reason, Some port, Some width, Some write, Some rep, Some str, Some fault_addr, Some addr ⇒
match uctx_set_retval1_spec reason abd with
| Some abd0 ⇒
if zeq reason EXIT_REASON_INOUT then
match uctx_set_retval2_spec port abd0 with
| Some abd1 ⇒
let flags := get_flags width write rep str in
match uctx_set_retval3_spec flags abd1 with
| Some abd2 ⇒ uctx_set_errno_spec E_SUCC abd2
| _ ⇒ None
end
| _ ⇒ None
end
else if zeq reason EXIT_REASON_EPT_FAULT then
match uctx_set_retval2_spec fault_addr abd0 with
| Some abd1 ⇒ uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
else if zeq reason EXIT_REASON_CR_ACCESS then
match uctx_set_retval2_spec addr abd0 with
| Some abd1 ⇒ uctx_set_errno_spec E_SUCC abd1
| _ ⇒ None
end
else
uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
| _,_,_,_,_,_,_,_ ⇒ None
end.
Function trap_handle_rdmsr_spec (abd: RData) :=
match thread_vmx_get_reg_spec C_GUEST_EAX abd with
| Some msr ⇒
match thread_rdmsr_spec msr abd with
| Some (VZ64 val) ⇒
let val_low := val mod (2 ^ 32) in
let val_high := val / (2 ^ 32) in
match thread_vmx_set_reg_spec C_GUEST_EAX val_low abd with
| Some abd0 ⇒
match thread_vmx_set_reg_spec C_GUEST_EDX val_high abd0 with
| Some abd1 ⇒
match thread_vmx_get_next_eip_spec abd1 with
| Some next_eip ⇒
if zle_le 0 next_eip Int.max_unsigned then
match thread_vmx_set_reg_spec C_GUEST_EIP next_eip abd1 with
| Some abd2 ⇒ uctx_set_errno_spec E_SUCC abd2
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_handle_wrmsr_spec (abd: RData) :=
match thread_vmx_get_reg_spec C_GUEST_ECX abd, thread_vmx_get_reg_spec C_GUEST_EAX abd,
thread_vmx_get_reg_spec C_GUEST_EDX abd with
| Some msr, Some eax, Some edx ⇒
let val := edx × 2 ^ 32 + eax in
match thread_wrmsr_spec msr (VZ64 val) abd with
| Some _ ⇒
match thread_vmx_get_next_eip_spec abd with
| Some next_eip ⇒
if zle_le 0 next_eip Int.max_unsigned then
match thread_vmx_set_reg_spec C_GUEST_EIP next_eip abd with
| Some abd0 ⇒ uctx_set_errno_spec E_SUCC abd0
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _, _, _ ⇒ None
end.
Function ptfault_resv_spec (vadr: Z) (abd: RData) :=
let cpu := (CPU_ID abd) in
let curid := (ZMap.get cpu (cid abd)) in
match big2_ptResv_spec curid vadr PT_PERM_PTU abd with
| Some (abd0, _) ⇒
Some abd0
| _ ⇒ None
end.
Section Proc_Create.
Require Import liblayers.compat.CompatLayers.
Require Import GlobIdent.
Require Import ASTExtra.
Require Import liblayers.lib.Decision.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Function ELF_ident (i: Z) : option ident :=
match i with
| 0 ⇒ Some START_USER_FUN_LOC
| _ ⇒ None
end.
Function trap_proc_create_spec (s: stencil) (m: mem) (abd: RData) :=
let cpu := (CPU_ID abd) in
let curid := (ZMap.get cpu (cid abd)) in
match uctx_arg3_spec abd with
| Some arg3 ⇒
match thread_container_can_consume_spec curid arg3 abd with
| Some 1 ⇒
match uctx_arg2_spec abd with
| Some arg1 ⇒
if zle_lt 0 arg1 num_proc then
match ELF_ident arg1 with
| Some fun_id ⇒
match find_symbol s ELF_ENTRY_LOC, find_symbol s START_USER_FUN_LOC,
find_symbol s ELF_LOC, find_symbol s STACK_LOC,
find_symbol s fun_id with
| Some bentry, Some buserstart, Some belf, Some bstack, Some busercode ⇒
match Mem.load Mint32 m bentry (arg1 × 4) with
| Some (Vptr bb bn) ⇒
if peq bb busercode then
if Int.eq bn Int.zero then
match big2_proc_create_spec abd bstack buserstart busercode Int.zero arg3 with
| Some (abd0, n) ⇒
match uctx_set_retval1_spec n abd0 with
| Some abd´ ⇒ uctx_set_errno_spec E_SUCC abd´
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end
| _,_,_,_,_ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end
| Some 0 ⇒ uctx_set_errno_spec E_MEM abd
| _ ⇒ None
end
| _ ⇒ None
end.
Inductive Syscall_Num:=
| NSYS_PUTS
| NSYS_RING0_SPAWN
| NSYS_SPAWN
| NSYS_YIELD
| NSYS_DISK_OP
| NSYS_DISK_CAP
| NSYS_GET_TSC_PER_MS
| NSYS_GET_TSC_OFFSET
| NSYS_SET_TSC_OFFSET
| NSYS_RUN_VM
| NSYS_GET_EXITINFO
| NSYS_MMAP
| NSYS_SET_REG
| NSYS_GET_REG
| NSYS_SET_SEG1
| NSYS_SET_SEG2
| NSYS_GET_NEXT_EIP
| NSYS_INJECT_EVENT
| NSYS_CHECK_PENDING_EVENT
| NSYS_CHECK_INT_SHADOW
| NSYS_INTERCEPT_INT_WINDOW
| NSYS_HANDLE_RDMSR
| NSYS_HANDLE_WRMSR
| NSYS_GET_QUOTA
| NSYS_RECV
| NSYS_SEND
| NSYS_GETC
| NSYS_PUTC
| NSYS_NR.
Definition Syscall_Z2Num (i: Z) :=
if zeq i SYS_puts then NSYS_PUTS
else if zeq i SYS_ring0_spawn then NSYS_RING0_SPAWN
else if zeq i SYS_spawn then NSYS_SPAWN
else if zeq i SYS_yield then NSYS_YIELD
else if zeq i SYS_disk_op then NSYS_DISK_OP
else if zeq i SYS_disk_cap then NSYS_DISK_CAP
else if zeq i SYS_recv then NSYS_RECV
else if zeq i SYS_send then NSYS_SEND
else if zeq i SYS_getc then NSYS_GETC
else if zeq i SYS_putc then NSYS_PUTC
else if zeq i SYS_get_tsc_per_ms then NSYS_GET_TSC_PER_MS
else if zeq i SYS_hvm_run_vm then NSYS_RUN_VM
else if zeq i SYS_hvm_get_exitinfo then NSYS_GET_EXITINFO
else if zeq i SYS_hvm_mmap then NSYS_MMAP
else if zeq i SYS_hvm_set_seg1 then NSYS_SET_SEG1
else if zeq i SYS_hvm_set_seg2 then NSYS_SET_SEG2
else if zeq i SYS_hvm_set_reg then NSYS_SET_REG
else if zeq i SYS_hvm_get_reg then NSYS_GET_REG
else if zeq i SYS_hvm_get_next_eip then NSYS_GET_NEXT_EIP
else if zeq i SYS_hvm_inject_event then NSYS_INJECT_EVENT
else if zeq i SYS_hvm_check_int_shadow then NSYS_CHECK_INT_SHADOW
else if zeq i SYS_hvm_check_pending_event then NSYS_CHECK_PENDING_EVENT
else if zeq i SYS_hvm_intercept_int_window then NSYS_INTERCEPT_INT_WINDOW
else if zeq i SYS_hvm_get_tsc_offset then NSYS_GET_TSC_OFFSET
else if zeq i SYS_hvm_set_tsc_offset then NSYS_SET_TSC_OFFSET
else if zeq i SYS_hvm_handle_rdmsr then NSYS_HANDLE_RDMSR
else if zeq i SYS_hvm_handle_wrmsr then NSYS_HANDLE_WRMSR
else if zeq i SYS_get_quota then NSYS_GET_QUOTA
else NSYS_NR.
Function sys_dispatch_c_spec (s: stencil) (m: mem) (abd: RData) :=
match uctx_arg1_spec abd with
| Some arg1 ⇒
if zle_le 0 arg1 Int.max_unsigned then
match Syscall_Z2Num arg1 with
| NSYS_SPAWN ⇒ trap_proc_create_spec s m abd
| NSYS_GET_TSC_OFFSET ⇒ trap_get_tsc_offset_spec abd
| NSYS_SET_TSC_OFFSET ⇒ trap_set_tsc_offset_spec abd
| NSYS_GET_EXITINFO ⇒ trap_get_exitinfo_spec abd
| NSYS_MMAP ⇒ trap_mmap_spec abd
| NSYS_SET_REG ⇒ trap_set_reg_spec abd
| NSYS_GET_REG ⇒ trap_get_reg_spec abd
| NSYS_SET_SEG1 ⇒ trap_set_seg1_spec abd
| NSYS_SET_SEG2 ⇒ trap_set_seg2_spec abd
| NSYS_GET_NEXT_EIP ⇒ trap_get_next_eip_spec abd
| NSYS_INJECT_EVENT ⇒ trap_inject_event_spec abd
| NSYS_CHECK_PENDING_EVENT ⇒ trap_check_pending_event_spec abd
| NSYS_CHECK_INT_SHADOW ⇒ trap_check_int_shadow_spec abd
| NSYS_INTERCEPT_INT_WINDOW ⇒ trap_intercept_int_window_spec abd
| NSYS_HANDLE_RDMSR ⇒ trap_handle_rdmsr_spec abd
| NSYS_HANDLE_WRMSR ⇒ trap_handle_wrmsr_spec abd
| NSYS_GET_QUOTA ⇒ trap_get_quota_spec abd
| NSYS_RECV ⇒ trap_receivechan_spec abd
| NSYS_SEND ⇒ trap_sendtochan_spec abd
| NSYS_YIELD ⇒ big2_thread_yield_spec abd
| NSYS_PUTC ⇒ sys_putc_spec abd
| NSYS_GETC ⇒ sys_getc_spec abd
| _ ⇒ uctx_set_errno_spec (E_INVAL_CALLNR) abd
end
else None
| _ ⇒ None
end.
End Proc_Create.
End OBJ_Trap.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{multi_oralce_prop: MultiOracleProp}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Context `{real_params: RealParams}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Lemma acquire_lock_SC_maintains_cid:
∀ habd habd´ i,
big2_acquire_lock_SC_spec i habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma release_lock_SC_maintains_cid:
∀ habd habd´ i,
big2_release_lock_SC_spec i habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_release_lock_SC_spec; intros.
unfold big_release_lock_SC_spec in *; subst.
subdestruct; inv H; reflexivity.
Qed.
Lemma palloc_maintains_cid:
∀ habd habd´ id b,
big2_palloc_spec id habd = Some (habd´, b)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; simpl; trivial.
Qed.
Lemma ptInsertPTE0_maintains_cid:
∀ habd habd´ nn vadr padr perm,
big2_ptInsertPTE0_spec nn vadr padr perm habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_ptInsertPTE0_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma ptAllocPDE0_maintains_cid:
∀ habd habd´ nn vadr i,
big2_ptAllocPDE_spec nn vadr habd = Some (habd´, i)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_ptAllocPDE_spec; intros.
subdestruct; inv H; simpl; trivial;
eapply palloc_maintains_cid; eauto.
Qed.
Lemma ptResv_maintains_cid:
∀ habd habd´ i n v p,
big2_ptResv_spec n v p habd = Some (habd´, i)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_ptResv_spec. intros.
subdestruct.
inv H.
erewrite palloc_maintains_cid; [ trivial | exact Hdestruct0 ].
erewrite palloc_maintains_cid; [| exact Hdestruct0 ].
unfold big2_ptInsert_spec in H.
subdestruct; injection H as _ <-.
- eapply ptInsertPTE0_maintains_cid; eauto.
- eapply ptAllocPDE0_maintains_cid; eauto.
- erewrite ptAllocPDE0_maintains_cid; [| exact Hdestruct11 ].
eapply ptInsertPTE0_maintains_cid; eauto.
Qed.
Lemma thread_wakeup_maintains_cid:
∀ habd habd´ a r,
big2_thread_wakeup_spec a habd = Some (habd´, r)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_thread_wakeup_spec. intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma tryreceive_chan_maintains_cid:
∀ habd habd´ chanid a b r,
thread_tryreceive_chan_spec chanid a b habd = Some (habd´, r)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_tryreceive_chan_spec, thread_ipc_receive_body_spec.
unfold ObjBigThread.big_ipc_receive_body_spec, big_page_copy_back_spec.
intros.
subdestruct; inv H; simpl; trivial.
eapply thread_wakeup_maintains_cid in Hdestruct25; simpl in *; try congruence.
eapply thread_wakeup_maintains_cid in Hdestruct25; simpl in *; try congruence.
Qed.
Lemma syncreceive_chan_maintains_cid:
∀ habd habd´ chanid a b r,
thread_syncreceive_chan_spec chanid a b habd = Some (habd´, r)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_syncreceive_chan_spec, flatmem_copy_spec.
intros.
subdestruct; inv H; trivial.
eapply release_lock_SC_maintains_cid in Hdestruct6; eauto.
eapply acquire_lock_SC_maintains_cid in Hdestruct3; eauto.
eapply tryreceive_chan_maintains_cid in Hdestruct4; eauto.
congruence.
Qed.
Lemma big2_thread_sleep_maintains_cid:
∀ habd habd´ a,
big2_thread_sleep_spec a habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_thread_sleep_spec; intros.
subdestruct; inv H; try reflexivity.
Qed.
Lemma syncsendto_chan_maintains_cid:
∀ habd habd´ a b c r,
thread_syncsendto_chan_spec a b c habd = Some (habd´, r)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_syncsendto_chan_spec, thread_ipc_send_body_spec.
unfold ObjBigThread.big_ipc_send_body_spec, big_page_copy_spec, thread_syncsendto_chan_pre_spec; intros.
subdestruct; inv H; try reflexivity.
- eapply release_lock_SC_maintains_cid in Hdestruct25; eauto.
eapply acquire_lock_SC_maintains_cid in Hdestruct8; eauto.
simpl in ×. congruence.
- eapply release_lock_SC_maintains_cid in Hdestruct27; eauto.
eapply acquire_lock_SC_maintains_cid in Hdestruct12; eauto.
eapply acquire_lock_SC_maintains_cid in Hdestruct8; eauto.
eapply big2_thread_sleep_maintains_cid in Hdestruct11; eauto.
simpl in ×. congruence.
Qed.
Lemma proc_create_maintains_cid:
∀ habd habd´ b b´ buc ofs_uc q i,
big2_proc_create_spec habd b b´ buc ofs_uc q = Some (habd´, i)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold big2_proc_create_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma thread_vmx_set_intercept_intwin_maintains_cid:
∀ habd habd´ enable,
thread_vmx_set_intercept_intwin_spec enable habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_intercept_intwin_spec.
unfold ObjVMCS.vmx_set_intercept_intwin_spec.
intros.
subdestruct; injection H as <-; reflexivity.
Qed.
Lemma thread_vmx_set_mmap_maintains_cid:
∀ habd habd´ gpa hpa mem_type i,
thread_vmx_set_mmap_spec gpa hpa mem_type habd = Some (habd´, i)
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_mmap_spec.
unfold vmx_set_mmap_spec.
unfold ObjEPT.ept_add_mapping_spec, ObjEPT.ept_invalidate_mappings_spec.
intros.
subdestruct; injection H as _ <-; reflexivity.
Qed.
Lemma thread_vmx_set_reg_maintains_cid:
∀ habd habd´ reg v,
thread_vmx_set_reg_spec reg v habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_reg_spec.
unfold vmx_set_reg_spec.
intros.
subdestruct; injection H as <-; reflexivity.
Qed.
Lemma thread_vmx_set_desc1_maintains_cid:
∀ habd habd´ seg sel base,
thread_vmx_set_desc1_spec seg sel base habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_desc1_spec.
unfold ObjVMCS.vmx_set_desc1_spec.
intros.
subdestruct; injection H as <-; reflexivity.
Qed.
Lemma thread_vmx_set_desc2_maintains_cid:
∀ habd habd´ seg lim ar,
thread_vmx_set_desc2_spec seg lim ar habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_desc2_spec.
unfold ObjVMCS.vmx_set_desc2_spec.
intros.
subdestruct; injection H as <-; reflexivity.
Qed.
Lemma thread_vmx_inject_event_maintains_cid:
∀ habd habd´ type vector errcode ev,
thread_vmx_inject_event_spec type vector errcode ev habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
Local Opaque Z.land Z.lor.
unfold thread_vmx_inject_event_spec.
unfold ObjVMCS.vmx_inject_event_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma thread_vmx_set_tsc_offset_maintains_cid:
∀ habd habd´ ofs,
thread_vmx_set_tsc_offset_spec ofs habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold thread_vmx_set_tsc_offset_spec.
unfold ObjVMCS.vmx_set_tsc_offset_spec.
intros.
subdestruct; injection H as <-; reflexivity.
Qed.
Lemma uctx_set_retval1_maintains_cid:
∀ habd habd´ n,
uctx_set_retval1_spec n habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold uctx_set_retval1_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_set_retval2_maintains_cid:
∀ habd habd´ n,
uctx_set_retval2_spec n habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold uctx_set_retval2_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_set_retval3_maintains_cid:
∀ habd habd´ n,
uctx_set_retval3_spec n habd = Some habd´
→ ZMap.get (CPU_ID habd) (cid habd) = ZMap.get (CPU_ID habd´) (cid habd´).
Proof.
unfold uctx_set_retval3_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_arg1_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd z labd f,
uctx_arg1_spec habd = Some z →
0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc →
relate_AbData s f habd labd →
uctx_arg1_spec labd = Some z.
Proof. apply uctx_argn_exist; split; [ discriminate | reflexivity ]. Qed.
Lemma uctx_arg2_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd z labd f,
uctx_arg2_spec habd = Some z →
0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc →
relate_AbData s f habd labd →
uctx_arg2_spec labd = Some z.
Proof. apply uctx_argn_exist; split; [ discriminate | reflexivity ]. Qed.
Lemma uctx_arg3_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd z labd f,
uctx_arg3_spec habd = Some z →
0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc →
relate_AbData s f habd labd →
uctx_arg3_spec labd = Some z.
Proof. apply uctx_argn_exist; split; [ discriminate | reflexivity ]. Qed.
Lemma uctx_arg4_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}: ∀ s habd z labd f,
uctx_arg4_spec habd = Some z →
0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc →
relate_AbData s f habd labd →
uctx_arg4_spec labd = Some z.
Proof. apply uctx_argn_exist; split; [ discriminate | reflexivity ]. Qed.
Lemma uctx_set_retval1_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd habd´ labd n f,
uctx_set_retval1_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, uctx_set_retval1_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof uctx_set_regk_exist U_EBX.
Lemma uctx_set_retval2_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd habd´ labd n f,
uctx_set_retval2_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, uctx_set_retval2_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof uctx_set_regk_exist U_ESI.
Lemma uctx_set_retval3_exist {re1: relate_impl_iflags} {re2: relate_impl_cid} {re3: relate_impl_uctxt}
{re4: relate_impl_init} {re5: relate_impl_CPU_ID} {re6: relate_impl_big_log}:
∀ s habd habd´ labd n f,
uctx_set_retval3_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, uctx_set_retval3_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof uctx_set_regk_exist U_EDI.
Section TRAP_GETC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_uctxt}.
Context {re3: relate_impl_console}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_cid}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_ioapic}.
Context {re8: relate_impl_com1}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_drv_serial}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_big_log}.
Require Import INVLemmaInterrupt.
Lemma sys_getc_exist:
∀ s habd habd´ labd f,
sys_getc_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, sys_getc_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold sys_getc_spec in ×. intros.
subdestruct.
assert(0 ≤ ZMap.get (CPU_ID r1) (cid r1) < num_proc).
{
functional inversion Hdestruct3.
exploit (serial_intr_enable_preserves_all); eauto; intro tmp; repeat (destruct tmp as [tmp1 tmp]; try rewrite <- tmp1 in *; clear tmp1); simpl; eauto.
clear tmp.
functional inversion Hdestruct.
exploit (serial_intr_disable_preserves_all); eauto; intro tmp; repeat (destruct tmp as [tmp1 tmp]; try rewrite tmp1 in *; clear tmp1); simpl; eauto.
functional inversion Hdestruct0.
functional inversion H8; unfold b, s0 in *; subst; eauto.
}
exploit thread_serial_intr_disable_exist; eauto; intros (? & ? & ?).
exploit thread_cons_buf_read_exist; eauto; intros (? & ? & ?).
exploit thread_serial_intr_enable_spec_exist; eauto; intros (? & ? & ?).
exploit uctx_set_retval1_exist; eauto; intros (? & ? & ?).
rewrite H3, H5, H7, Hdestruct2, H9.
eapply uctx_set_regk_exist; try eassumption.
functional inversion Hdestruct4; eauto.
Qed.
End TRAP_GETC_SIM.
Section TRAP_PUTC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_uctxt}.
Context {re3: relate_impl_console}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_cid}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_ioapic}.
Context {re8: relate_impl_com1}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_drv_serial}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_big_log}.
Lemma sys_putc_exist:
∀ s habd habd´ labd f,
sys_putc_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, sys_putc_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold sys_putc_spec in ×. intros.
subdestruct.
assert(0 ≤ ZMap.get (CPU_ID r1) (cid r1) < num_proc).
{
functional inversion Hdestruct3;
exploit (serial_intr_enable_preserves_all); eauto; intro tmp; repeat (destruct tmp as [tmp1 tmp]; try rewrite <- tmp1 in *; clear tmp1); simpl; eauto; clear tmp;
functional inversion Hdestruct2; subst;
functional inversion H5; subst;
simpl in *;
functional inversion Hdestruct1;
exploit (serial_intr_disable_preserves_all); eauto; intro tmp; repeat (destruct tmp as [tmp1 tmp]; try rewrite tmp1 in *; clear tmp1); simpl; eauto.
}
erewrite uctx_arg2_exist; eauto.
exploit thread_serial_intr_disable_exist; eauto; intros (? & ? & ?).
exploit thread_serial_putc_exist; eauto; intros (? & ? & ?).
exploit thread_serial_intr_enable_spec_exist; eauto; intros (? & ? & ?).
rewrite H3, H5, H7, Hdestruct0.
eapply uctx_set_regk_exist; try eassumption.
Qed.
End TRAP_PUTC_SIM.
Lemma big_acquire_lock_SC_preserves_cid_range:
∀ chid d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
big2_acquire_lock_SC_spec chid d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid d d´ Hinv.
unfold big2_acquire_lock_SC_spec. intros.
subdestruct; inv H; simpl; assumption.
Qed.
Lemma big2_thread_sleep_preserves_cid_range:
∀ chid d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
big2_thread_sleep_spec chid d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid d d´ Hinv.
unfold big2_thread_sleep_spec. intros.
subdestruct; inv H; simpl; assumption.
Qed.
Lemma syncsendto_chan_pre_preserves_cid_range:
∀ cv d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_syncsendto_chan_pre_spec cv d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid d d´ Hinv.
unfold thread_syncsendto_chan_pre_spec. intros.
subdestruct.
- inv H; simpl; eapply big_acquire_lock_SC_preserves_cid_range; eauto.
- eapply big_acquire_lock_SC_preserves_cid_range; [| eauto].
eapply big2_thread_sleep_preserves_cid_range; [| eauto].
eapply big_acquire_lock_SC_preserves_cid_range; [| eauto].
assumption.
Qed.
Import ObjCV.
Lemma ipc_send_body_preserves_cid_range:
∀ chid vaddr scount v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_ipc_send_body_spec chid vaddr scount d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid vaddr scount v d d´ Hinv.
unfold thread_ipc_send_body_spec.
unfold big_ipc_send_body_spec.
unfold big_page_copy_spec.
intros.
subdestruct; inv H; simpl.
assumption.
Qed.
Lemma big_release_lock_SC_preserves_cid_range:
∀ chid d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
big2_release_lock_SC_spec chid d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid d d´ Hinv.
unfold big2_release_lock_SC_spec.
unfold big_release_lock_SC_spec.
intros.
subdestruct; inv H; simpl; assumption.
Qed.
Lemma trap_sendtochan_preserves_cid_range:
∀ cv vaddr scount v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_syncsendto_chan_spec cv vaddr scount d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros cv vaddr scount v d d´ Hinv.
unfold thread_syncsendto_chan_spec. intros.
subdestruct; inv H.
exploit syncsendto_chan_pre_preserves_cid_range; eauto; intros Hinv1.
exploit ipc_send_body_preserves_cid_range; eauto; intros Hinv2.
exploit big_release_lock_SC_preserves_cid_range; eauto.
Qed.
Section TRAP_SENDTOCHAN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_syncchpool}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_uctxt}.
Context {re6: relate_impl_ptpool}.
Context {re7: relate_impl_PT}.
Context {re8: relate_impl_init}.
Context {re9: relate_impl_CPU_ID}.
Context {re11: relate_impl_lock}.
Context {re12: relate_impl_big_oracle}.
Context {re13: relate_impl_big_log}.
Context {re16: relate_impl_in_intr}.
Context {re17: relate_impl_intr_flag}.
Context {re18: relate_impl_AC}.
Context {re19: relate_impl_trapinfo}.
Context {re20: relate_impl_pperm}.
Context {re21: relate_impl_HP}.
Lemma trap_sendtochan_exist:
∀ s habd habd´ labd f,
trap_sendtochan_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_sendtochan_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_sendtochan_spec. intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
exploit thread_syncsendto_chan_exist; eauto.
intros (labd1 & → & Hr1).
exploit uctx_set_retval1_exist; eauto.
eapply trap_sendtochan_preserves_cid_range; eauto.
intros (labd2 & → & Hr2).
exploit (uctx_set_regk_exist U_EAX); eauto.
functional inversion Hdestruct4. simpl.
eapply trap_sendtochan_preserves_cid_range; eauto.
Qed.
End TRAP_SENDTOCHAN_SIM.
Lemma flatmem_copy_preserves_cid_range:
∀ v1 v2 v3 d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
flatmem_copy_spec v1 v2 v3 d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros v1 v2 v3 d d´ Hinv.
unfold flatmem_copy_spec. intros.
subdestruct; inv H; simpl; try assumption.
Qed.
Lemma page_copy_back_preserves_cid_range:
∀ v1 v2 v3 d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
big_page_copy_back_spec v1 v2 v3 d = Some d´ →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros v1 v2 v3 d d´ Hinv.
unfold big_page_copy_back_spec.
intros.
subdestruct; inv H; simpl; try assumption.
Qed.
Lemma ipc_receive_body_preserves_cid_range:
∀ cv chid vaddr v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_ipc_receive_body_spec cv chid vaddr d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chid cv vaddr v d d´ Hinv.
unfold thread_ipc_receive_body_spec.
unfold big_ipc_receive_body_spec.
intros.
subdestruct; inv H; simpl.
- eapply page_copy_back_preserves_cid_range; eauto.
Qed.
Lemma big_thread_wakeup_preserves_cid_range:
∀ id v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
big2_thread_wakeup_spec id d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros id v d d´ Hinv.
unfold big2_thread_wakeup_spec. intros.
subdestruct; inv H; simpl; assumption.
Qed.
Lemma tryreceive_chan_preserves_cid_range:
∀ chanid chid vaddr v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_tryreceive_chan_spec chanid chid vaddr d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chanid chid vaddr v d d´ Hinv.
unfold thread_tryreceive_chan_spec. intros.
subdestruct; inv H; simpl.
- assumption.
- exploit ipc_receive_body_preserves_cid_range; eauto; intros Hinv1.
exploit big_thread_wakeup_preserves_cid_range; eauto.
- exploit ipc_receive_body_preserves_cid_range; eauto; intros Hinv1.
exploit big_thread_wakeup_preserves_cid_range; eauto.
Qed.
Lemma syncreceive_chan_preserves_cid_range:
∀ chanid cv vaddr v d d´,
0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc →
thread_syncreceive_chan_spec chanid cv vaddr d = Some (d´, v) →
0 ≤ ZMap.get (CPU_ID d´) (cid d´) < num_proc.
Proof.
intros chanid cv vaddr v d d´ Hinv.
unfold thread_syncreceive_chan_spec. intros.
subdestruct; inv H.
exploit big_acquire_lock_SC_preserves_cid_range; eauto; intros Hinv1.
exploit tryreceive_chan_preserves_cid_range; eauto; intros Hinv2.
exploit big_release_lock_SC_preserves_cid_range; eauto.
Qed.
Section TRAP_RECEIVECHAN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_syncchpool}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_uctxt}.
Context {re6: relate_impl_CPU_ID}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_HP}.
Context {re11: relate_impl_init}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_PT}.
Context {re14: relate_impl_nps}.
Context {re15: relate_impl_big_oracle}.
Context {re16: relate_impl_big_log}.
Context {re17: relate_impl_lock}.
Context {re20: relate_impl_AC}.
Lemma trap_receivechan_exist:
∀ s habd habd´ labd f,
trap_receivechan_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_receivechan_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_receivechan_spec in ×. intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
exploit thread_syncreceive_chan_exist; eauto. intros (labd´ & HP & HR).
rewrite HP.
exploit uctx_set_retval1_exist; eauto.
eapply syncreceive_chan_preserves_cid_range; eauto.
intros (labd2 & → & Hr2).
exploit (uctx_set_regk_exist U_EAX); eauto.
functional inversion Hdestruct4. simpl.
eapply syncreceive_chan_preserves_cid_range; eauto.
Qed.
End TRAP_RECEIVECHAN_SIM.
Section TRAP_GET_QUOTA_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_uctxt}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_get_quota_exist:
∀ s habd habd´ labd f,
trap_get_quota_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_get_quota_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_get_quota_spec in ×. intros.
subdestruct.
erewrite thread_get_curid_exist; eauto.
erewrite thread_container_get_quota_exist; eauto.
erewrite thread_container_get_usage_exist; eauto.
exploit uctx_set_retval1_exist; eauto. intros (labd´´ & → & HR´).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_GET_QUOTA_SIM.
Section TRAP_INTERCEPT_INT_WINDOW_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_intercept_int_window_exist:
∀ s habd habd´ labd f,
trap_intercept_int_window_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_intercept_int_window_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_intercept_int_window_spec in ×. intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
exploit thread_vmx_set_intercept_intwin_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_intercept_intwin_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; try eassumption.
Qed.
End TRAP_INTERCEPT_INT_WINDOW_SIM.
Section TRAP_CHECK_PENDING_EVENT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_check_pending_event_exist:
∀ s habd habd´ labd f,
trap_check_pending_event_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_check_pending_event_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_check_pending_event_spec in ×. intros.
subdestruct.
erewrite thread_vmx_check_pending_event_exists; eauto.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_CHECK_PENDING_EVENT_SIM.
Section TRAP_CHECK_INT_SHADOW_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_check_int_shadow_exist:
∀ s habd habd´ labd f,
trap_check_int_shadow_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_check_int_shadow_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_check_int_shadow_spec in ×. intros.
subdestruct.
erewrite thread_vmx_check_int_shadow_exists; eauto.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_CHECK_INT_SHADOW_SIM.
Section TRAP_INJECT_EVENT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_inject_event_exist:
∀ s habd habd´ labd f,
trap_inject_event_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_inject_event_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_inject_event_spec in ×. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv;
destruct (uctx_arg3_spec habd) eqn:Hdestruct0; contra_inv;
destruct (uctx_arg4_spec habd) eqn:Hdestruct1; contra_inv;
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
subdestruct.
exploit thread_vmx_inject_event_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_inject_event_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_INJECT_EVENT_SIM.
Section TRAP_GET_NEXT_EIP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmx}.
Context {re5: relate_impl_vmcs}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_get_next_eip_exist:
∀ s habd habd´ labd f,
trap_get_next_eip_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_get_next_eip_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_get_next_eip_spec in ×. intros.
subdestruct.
erewrite thread_vmx_get_next_eip_exist; eauto.
rewrite Hdestruct0.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_GET_NEXT_EIP_SIM.
Section TRAP_SET_REG_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmx}.
Context {re5: relate_impl_vmcs}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_set_reg_exist:
∀ s habd habd´ labd f,
trap_set_reg_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_set_reg_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_set_reg_spec in ×. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv;
destruct (uctx_arg3_spec habd) eqn:Hdestruct0; contra_inv.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
subdestruct.
- exploit thread_vmx_set_reg_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_reg_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_SET_REG_SIM.
Section TRAP_GET_REG_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmx}.
Context {re5: relate_impl_vmcs}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_get_reg_exist:
∀ s habd habd´ labd f,
trap_get_reg_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_get_reg_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_get_reg_spec in ×. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv.
erewrite uctx_arg2_exist; eauto.
subdestruct.
- erewrite thread_vmx_get_reg_exist; eauto.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_GET_REG_SIM.
Section TRAP_SET_SEG1_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_set_seg1_exist:
∀ s habd habd´ labd f,
trap_set_seg1_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_set_seg1_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_set_seg1_spec in ×. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv;
destruct (uctx_arg3_spec habd) eqn:Hdestruct0; contra_inv;
destruct (uctx_arg4_spec habd) eqn:Hdestruct1; contra_inv;
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
subdestruct.
- exploit thread_vmx_set_desc1_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_desc1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_SET_SEG1_SIM.
Section TRAP_SET_SEG2_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_set_seg2_exist:
∀ s habd habd´ labd f,
trap_set_seg2_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_set_seg2_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_set_seg2_spec in ×. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv;
destruct (uctx_arg3_spec habd) eqn:Hdestruct0; contra_inv;
destruct (uctx_arg4_spec habd) eqn:Hdestruct1; contra_inv;
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
subdestruct.
- exploit thread_vmx_set_desc2_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_desc2_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_SET_SEG2_SIM.
Section TRAP_GET_TSC_OFFSET_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_get_tsc_offset_exist:
∀ s habd habd´ labd f,
trap_get_tsc_offset_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_get_tsc_offset_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.shiftr.
unfold trap_get_tsc_offset_spec in ×. intros.
subdestruct.
erewrite thread_vmx_get_tsc_offset_exists; eauto. simpl.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
exploit uctx_set_retval2_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval2_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_GET_TSC_OFFSET_SIM.
Section TRAP_SET_TSC_OFFSET_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_big_log}.
Lemma trap_set_tsc_offset_exist:
∀ s habd habd´ labd f,
trap_set_tsc_offset_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_set_tsc_offset_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.lor Z.shiftl.
unfold trap_set_tsc_offset_spec in ×. intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
exploit thread_vmx_set_tsc_offset_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_tsc_offset_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_SET_TSC_OFFSET_SIM.
Section TRAP_GET_EXITINFO_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmcs}.
Context {re5: relate_impl_vmx}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_get_exitinfo_exist:
∀ s habd habd´ labd f,
trap_get_exitinfo_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_get_exitinfo_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_get_exitinfo_spec in ×. intros.
repeat (
match goal with
| HT:context [match ?con with | _ ⇒ _ end] |- _ ⇒
let H := fresh "Hdestruct" in
destruct con eqn:H; contra_inv;
first [ erewrite thread_vmx_get_exit_reason_exists
| erewrite thread_vmx_get_exit_io_port_exist
| erewrite thread_vmx_get_io_width_exist
| erewrite thread_vmx_get_io_write_exist
| erewrite thread_vmx_get_exit_io_rep_exist
| erewrite thread_vmx_get_exit_io_str_exist
| erewrite thread_vmx_get_exit_fault_addr_exists
| erewrite thread_vmx_get_exit_qualification_exist ];
eauto; simpl in HT |- ×
end).
subdestruct.
- exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
exploit uctx_set_retval2_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval2_maintains_cid in H1; eauto.
exploit uctx_set_retval3_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval3_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
exploit uctx_set_retval2_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval2_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
exploit uctx_set_retval2_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval2_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
- exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_GET_EXITINFO_SIM.
Section TRAP_HANDLE_RDMSR_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmx}.
Context {re5: relate_impl_vmcs}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_handle_rdmsr_exist:
∀ s habd habd´ labd f,
trap_handle_rdmsr_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_handle_rdmsr_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.shiftr.
unfold trap_handle_rdmsr_spec, thread_rdmsr_spec.
unfold ObjVMCS.rdmsr_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite. subdestruct.
erewrite thread_vmx_get_reg_exist; eauto.
erewrite thread_vmx_set_reg_maintains_cid in H1; eauto.
exploit thread_vmx_set_reg_exist; try exact Hdestruct2; eauto. intros (? & → & ?).
erewrite thread_vmx_set_reg_maintains_cid in H1; eauto.
exploit thread_vmx_set_reg_exist; try exact Hdestruct3; eauto. intros (? & → & ?).
erewrite thread_vmx_get_next_eip_exist; eauto.
erewrite thread_vmx_set_reg_maintains_cid in H1; eauto.
rewrite Hdestruct5.
exploit thread_vmx_set_reg_exist; try exact Hdestruct5; eauto. intros (? & → & ?).
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_HANDLE_RDMSR_SIM.
Section TRAP_HANDLE_WRMSR_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_vmx}.
Context {re5: relate_impl_vmcs}.
Context {re6: relate_impl_init}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma trap_handle_wrmsr_exist:
∀ s habd habd´ labd f,
trap_handle_wrmsr_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_handle_wrmsr_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.lor Z.shiftl.
unfold trap_handle_wrmsr_spec, thread_wrmsr_spec.
unfold ObjVMCS.wrmsr_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite. subdestruct.
erewrite thread_vmx_get_reg_exist; eauto.
erewrite thread_vmx_get_reg_exist; eauto.
erewrite thread_vmx_get_reg_exist; eauto.
erewrite thread_vmx_get_next_eip_exist; eauto.
erewrite thread_vmx_set_reg_maintains_cid in H1; eauto.
exploit thread_vmx_set_reg_exist; eauto. intros (? & → & ?).
rewrite Hdestruct5.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_HANDLE_WRMSR_SIM.
Section TRAP_MMAP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_syncchpool}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_uctxt}.
Context {re6: relate_impl_ptpool}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_nps}.
Context {re9: relate_impl_pperm}.
Context {re10: relate_impl_HP}.
Context {re11: relate_impl_ept}.
Context {re12: relate_impl_AC}.
Context {re13: relate_impl_CPU_ID}.
Context {re14: relate_impl_big_oracle}.
Context {re15: relate_impl_lock}.
Context {re16: relate_impl_big_log}.
Lemma trap_mmap_exist:
∀ s habd habd´ labd f,
trap_mmap_spec habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_mmap_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.modulo Z.add Z.sub.
unfold trap_mmap_spec in ×. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
destruct (uctx_arg2_spec habd) eqn:Hdestruct; contra_inv;
destruct (uctx_arg3_spec habd) eqn:Hdestruct0; contra_inv;
destruct (uctx_arg4_spec habd) eqn:Hdestruct1; contra_inv.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
revert H. subrewrite. clear Hdestruct Hdestruct0 Hdestruct1. subdestruct.
- erewrite thread_ptRead_exist; try exact Hdestruct0; eauto.
exploit big2_ptResv_exist; eauto. intros (? & → & ?).
erewrite ptResv_maintains_cid in H1; eauto.
erewrite thread_ptRead_exist; try ∃ Hdestruct4; eauto.
exploit thread_vmx_set_mmap_exist; eauto. intros (? & → & ?).
erewrite thread_vmx_set_mmap_maintains_cid in H1; eauto.
subrewrite´.
eapply uctx_set_regk_exist; eassumption.
- erewrite thread_ptRead_exist; try exact Hdestruct0; eauto.
exploit thread_vmx_set_mmap_exist; try eauto. intros (? & → & ?).
erewrite thread_vmx_set_mmap_maintains_cid in H1; eauto.
subrewrite´.
eapply uctx_set_regk_exist; eassumption.
- eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_MMAP_SIM.
Section PTFAULT_RESV_SPEC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_nps}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_ptpool}.
Context {re7: relate_impl_HP}.
Context {re8: relate_impl_cid}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_uctxt}.
Context {re11: relate_impl_AC}.
Context {re12: relate_impl_big_oracle}.
Context {re13: relate_impl_lock}.
Context {re14: relate_impl_big_log}.
Lemma ptfault_resv_exist:
∀ s habd habd´ labd n f,
ptfault_resv_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, ptfault_resv_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptfault_resv_spec; intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
exploit big2_ptResv_exist; eauto. intros [ labd´ [ → rel´ ] ].
∃ labd´. inv HQ. refine_split; auto.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_ptpool}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_uctxt}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_big_oracle}.
Context {mt7: match_impl_lock}.
Context {mt8: match_impl_big_log}.
Lemma ptfault_resv_match:
∀ s d d´ m n f,
ptfault_resv_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptfault_resv_spec; intros.
subdestruct; inv H; trivial.
exploit big2_ptResv_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) ptfault_resv_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ptfault_resv_spec}.
Lemma ptfault_resv_sim:
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ gensem ptfault_resv_spec)
(id ↦ gensem ptfault_resv_spec).
Proof.
intros ? valid_cid. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ptfault_resv_exist; eauto; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ptfault_resv_match; eauto.
Qed.
End PTFAULT_RESV_SPEC_SIM.
Section TRAP_PROC_CREATE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_AC}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_big_log}.
Context {re8: relate_impl_lock}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_init}.
Lemma trap_proc_create_exist:
∀ s hm lm habd habd´ labd f,
trap_proc_create_spec s hm habd = Some habd´
→ relate_AbData s f habd labd
→ Mem.inject f hm lm
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, trap_proc_create_spec s lm labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold trap_proc_create_spec, ELF_ident.
unfold thread_container_can_consume_spec.
unfold ObjContainer.container_can_consume_spec.
intros.
exploit relate_impl_cid_eq; eauto; intro Hcid.
exploit relate_impl_CPU_ID_eq; eauto; intro HCPU.
exploit relate_impl_AC_eq; eauto; intro HAC.
exploit relate_impl_init_eq; eauto; intro Hinit.
exploit relate_impl_iflags_eq; eauto; intro Hflags.
exploit relate_impl_big_log_eq; eauto; intro Hbig_log.
inv Hflags.
rewrite <- HAC, <- Hcid, <- HCPU, <- Hinit, <- ikern_eq, <- ihost_eq.
destruct (uctx_arg3_spec habd) eqn:Harg3; try discriminate H.
erewrite uctx_arg3_exist; eauto.
subdestruct; subst.
rewrite <- Hbig_log.
rewrite Hdestruct6.
- assert (f b0 = Some (b0, 0)).
{ apply H2.
unfold Mem.flat_inj.
apply genv_symb_range in Hdestruct10.
destruct (plt b0 (genv_next s)); [ reflexivity | contradiction ].
}
assert (f b1 = Some (b1, 0)).
{ apply H2.
unfold Mem.flat_inj.
apply genv_symb_range in Hdestruct11.
destruct (plt b1 (genv_next s)); [ reflexivity | contradiction ].
}
erewrite uctx_arg2_exist; eauto.
simpl; subrewrite´.
exploit Mem.load_inject; eauto.
simpl. intros (? & → & ?).
inv H6. rewrite H5 in H9. injection H9 as <- <-.
inv H9.
rewrite peq_true.
rewrite Int.add_zero.
rewrite Hdestruct16.
exploit big2_proc_create_exist; eauto. intros (? & → & ?).
erewrite proc_create_maintains_cid in H3; eauto.
exploit uctx_set_retval1_exist; eauto.
intros (? & → & ?).
eapply uctx_set_retval1_maintains_cid in Hdestruct19; eauto.
simpl in Hdestruct19.
rewrite Hdestruct19 in H3.
eapply uctx_set_regk_exist; eauto.
- rewrite <- Hbig_log.
rewrite Hdestruct6.
eapply uctx_set_regk_exist; eassumption.
- rewrite <- Hbig_log.
rewrite Hdestruct8.
eapply uctx_set_regk_exist; eassumption.
- rewrite <- Hbig_log.
rewrite Hdestruct8.
eapply uctx_set_regk_exist; eassumption.
- rewrite <- Hbig_log.
rewrite Hdestruct7.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_PROC_CREATE_SIM.
Section SYS_DISPATCH_C_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_nps}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_PT}.
Context {re6: relate_impl_ptpool}.
Context {re7: relate_impl_idpde}.
Context {re8: relate_impl_cid}.
Context {re9: relate_impl_syncchpool}.
Context {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_pperm}.
Context {re12: relate_impl_HP}.
Context {re13: relate_impl_ept}.
Context {re14: relate_impl_uctxt}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_big_oracle}.
Context {re17: relate_impl_big_log}.
Context {re18: relate_impl_lock}.
Context {re19: relate_impl_CPU_ID}.
Context {re20: relate_impl_ioapic}.
Context {re21: relate_impl_com1}.
Context {re22: relate_impl_in_intr}.
Context {re23: relate_impl_drv_serial}.
Context {re24: relate_impl_console}.
Context {re25: relate_impl_intr_flag}.
Context {re26: relate_impl_vmcs}.
Context {re27: relate_impl_vmx}.
Context {re28: relate_impl_trapinfo}.
Lemma sys_dispatch_c_exist:
∀ s hm lm habd habd´ labd f,
sys_dispatch_c_spec s hm habd = Some habd´
→ relate_AbData s f habd labd
→ Mem.inject f hm lm
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´, sys_dispatch_c_spec s lm labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold sys_dispatch_c_spec. intros.
destruct (uctx_arg1_spec habd) eqn:Hdestruct; try discriminate.
erewrite uctx_arg1_exist; eauto.
case_eq (zle_le 0 z Int.max_unsigned); intros; rewrite H4 in H; try discriminate H.
destruct (Syscall_Z2Num z) eqn:Hdestruct0;
try eapply uctx_set_regk_exist; eauto.
eapply trap_proc_create_exist; eauto.
eapply big2_thread_yield_exist; eauto.
eapply trap_get_tsc_offset_exist; eauto.
eapply trap_set_tsc_offset_exist; eauto.
eapply trap_get_exitinfo_exist; eauto.
eapply trap_mmap_exist; eauto.
eapply trap_set_reg_exist; eauto.
eapply trap_get_reg_exist; eauto.
eapply trap_set_seg1_exist; eauto.
eapply trap_set_seg2_exist; eauto.
eapply trap_get_next_eip_exist; eauto.
eapply trap_inject_event_exist; eauto.
eapply trap_check_pending_event_exist; eauto.
eapply trap_check_int_shadow_exist; eauto.
eapply trap_intercept_int_window_exist; eauto.
eapply trap_handle_rdmsr_exist; eauto.
eapply trap_handle_wrmsr_exist; eauto.
eapply trap_get_quota_exist; eauto.
eapply trap_receivechan_exist; eauto.
eapply trap_sendtochan_exist; eauto.
eapply sys_getc_exist; eauto.
eapply sys_putc_exist; eauto.
Qed.
End SYS_DISPATCH_C_SIM.
End OBJ_SIM.