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 CalRealSMSPool.
Require Import CalRealProcModule.
Require Import liblayers.compat.CompatGenSem.
Require Import ObjArg.
Require Import ObjProc.
Require Import ObjLMM.
Require Import ObjVMM.
Require Import ObjSyncIPC.
Require Import ObjThread.
Require Import ObjContainer.
Require Import ObjFlatMem.
Section OBJ_Trap.
Function trap_sendtochan_pre_spec (abd: RData) : option (RData × Z) :=
match uctx_arg2_spec abd with
| Some chid ⇒
match uctx_arg3_spec abd with
| Some vaddr ⇒
match uctx_arg4_spec abd with
| Some scount ⇒
syncsendto_chan_pre_spec chid vaddr scount abd
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function trap_sendtochan_post_spec (abd: RData) :=
match syncsendto_chan_post_spec 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.
Function trap_receivechan_spec (abd: RData) :=
match uctx_arg2_spec abd with
| Some fromid ⇒
match uctx_arg3_spec abd with
| Some vaddr ⇒
match uctx_arg4_spec abd with
| Some rcount ⇒
match syncreceive_chan_spec fromid 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 get_curid_spec abd with
| Some curid ⇒
match container_get_quota_spec curid abd with
| Some quota ⇒
match 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 ptfault_resv_spec (vadr: Z) (abd: RData) :=
match ikern abd, ihost abd, pg abd with
| true, true, true ⇒
if zle_lt adr_low vadr adr_high then
match ptResv_spec (cid abd) vadr PT_PERM_PTU abd with
| Some (abd0, _) ⇒
Some abd0
| _ ⇒ None
end
else Some abd
| _, _, _ ⇒ None
end.
Require Import ObjShareMem.
Function trap_offer_shared_mem_spec (abd: RData) :=
match (uctx_arg2_spec abd, cid abd) with
| (Some vadr, n) ⇒
if zeq n 1 then
match offer_shared_mem_spec 1 2 vadr abd with
| Some (abd', res) ⇒
match uctx_set_retval1_spec res abd' with
| Some abd'' ⇒ uctx_set_errno_spec E_SUCC abd''
| _ ⇒ None
end
| _ ⇒ None
end
else uctx_set_errno_spec E_SUCC abd
| _ ⇒ None
end.
Function print_spec (adt: RData) :=
match uctx_arg2_spec adt with
| Some content ⇒
uctx_set_errno_spec E_SUCC
(adt {devout: DeviceOutput_update (devout adt) (cid adt) (cid adt) (OUT content)})
| _ ⇒ 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.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Function ELF_ident (i: Z) : option ident :=
match i with
| 0 ⇒ Some proc_start_user
| _ ⇒ None
end.
Function trap_proc_create_spec (s: stencil) (m: mem) (abd: RData) :=
match uctx_arg3_spec abd with
| Some arg3 ⇒
if zle_le 0 arg3 (cquota (ZMap.get (cid abd) (AC abd)) - cusage (ZMap.get (cid abd) (AC abd))) then
if zle_le 0 (cid abd × max_children + 1 + max_children) num_id then
if zlt (Z_of_nat (length (cchildren (ZMap.get (cid abd) (AC abd))))) max_children then
match uctx_arg2_spec abd with
| Some arg1 ⇒
if zle_lt 0 arg1 num_id then
match ELF_ident arg1 with
| Some fun_id ⇒
match find_symbol s ELF_ENTRY_LOC, find_symbol s proc_start_user,
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 proc_create_spec abd bstack buserstart busercode Int.zero arg3 with
| Some (abd', n) ⇒
match uctx_set_retval1_spec n abd' 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
else uctx_set_errno_spec E_MEM abd
else uctx_set_errno_spec E_MEM abd
else uctx_set_errno_spec E_MEM abd
| _ ⇒ None
end.
Inductive Syscall_Num:=
| NSYS_PUTS
| NSYS_RING0_SPAWN
| NSYS_SPAWN
| NSYS_YIELD
| NSYS_DISK_OP
| NSYS_DISK_CAP
| NSYS_GET_QUOTA
| NSYS_RECV
| NSYS_SHARE
| NSYS_PRINT
| NSYS_NR.
Notation SYS_share := 27.
Notation SYS_print := 28.
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_get_quota then NSYS_GET_QUOTA
else if zeq i SYS_share then NSYS_SHARE
else if zeq i SYS_print then NSYS_PRINT
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_QUOTA ⇒ trap_get_quota_spec abd
| NSYS_SHARE ⇒ trap_offer_shared_mem_spec abd
| NSYS_PRINT ⇒ print_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.
Require Import Observation.
Section OBJ_SIM.
Context `{Hobs: Observation}.
Context `{data : CompatData(Obs:=Obs) RData}.
Context `{data0 : CompatData(Obs:=Obs) RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (Obs:=Obs) (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Lemma alloc_maintains_cid:
∀ habd habd' id b,
alloc_spec id habd = Some (habd', b)
→ cid habd = cid habd'.
Proof.
unfold alloc_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma ptInsertPTE0_maintains_cid:
∀ habd habd' nn vadr padr perm,
ptInsertPTE0_spec nn vadr padr perm habd = Some habd'
→ cid habd = cid habd'.
Proof.
unfold ptInsertPTE0_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma ptAllocPDE0_maintains_cid:
∀ habd habd' nn vadr i,
ptAllocPDE0_spec nn vadr habd = Some (habd', i)
→ cid habd = cid habd'.
Proof.
unfold ptAllocPDE0_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma ptInsert0_maintains_cid:
∀ habd habd' nn vadr padr perm z,
ptInsert0_spec nn vadr padr perm habd = Some (habd', z)
→ cid habd = cid habd'.
Proof.
intros. functional inversion H; subst; auto.
- eapply ptInsertPTE0_maintains_cid; eauto.
- eapply ptAllocPDE0_maintains_cid; eauto.
- erewrite ptAllocPDE0_maintains_cid; [| eassumption ].
eapply ptInsertPTE0_maintains_cid; eauto.
Qed.
Lemma ptResv_maintains_cid:
∀ habd habd' i n v p,
ptResv_spec n v p habd = Some (habd', i)
→ cid habd = cid habd'.
Proof.
unfold ptResv_spec. intros.
subdestruct; [ injection H as _ <-; reflexivity |].
erewrite alloc_maintains_cid; [| exact Hdestruct ].
eapply ptInsert0_maintains_cid; eauto.
Qed.
Lemma ptResv2_maintains_cid:
∀ habd habd' i n v p n' v' p',
ptResv2_spec n v p n' v' p' habd = Some (habd', i)
→ cid habd = cid habd'.
Proof.
intros. functional inversion H; subst; auto; clear H.
- erewrite alloc_maintains_cid; [| eassumption ].
eapply ptInsert0_maintains_cid; eauto.
- erewrite alloc_maintains_cid; [| eassumption ].
erewrite ptInsert0_maintains_cid; [|eassumption].
eapply ptInsert0_maintains_cid; eauto.
Qed.
Lemma offer_shared_mem_maintains_cid:
∀ i1 i2 i3 d d' z,
offer_shared_mem_spec i1 i2 i3 d = Some (d', z)
→ cid d = cid d'.
Proof.
intros. functional inversion H; subst; auto; simpl; clear H.
- eapply ptResv2_maintains_cid; eauto.
- eapply ptResv2_maintains_cid; eauto.
Qed.
Lemma thread_wakeup_maintains_cid:
∀ habd habd' a,
ObjThread.thread_wakeup_spec a habd = Some habd'
→ cid habd = cid habd'.
Proof.
unfold ObjThread.thread_wakeup_spec. intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma syncreceive_chan_maintains_cid:
∀ habd habd' a b c r,
syncreceive_chan_spec a b c habd = Some (habd', r)
→ cid habd = cid habd'.
Proof.
unfold syncreceive_chan_spec, flatmem_copy_spec.
intros.
subdestruct; inv H; trivial.
eapply thread_wakeup_maintains_cid in Hdestruct17; eauto.
Qed.
Lemma syncsendto_chan_post_maintains_cid:
∀ habd habd' r,
syncsendto_chan_post_spec habd = Some (habd', r)
→ cid habd = cid habd'.
Proof.
unfold syncsendto_chan_post_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma proc_create_maintains_cid:
∀ habd habd' b b' buc ofs_uc q i,
proc_create_spec habd b b' buc ofs_uc q = Some (habd', i)
→ cid habd = cid habd'.
Proof.
unfold proc_create_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_set_retval1_maintains_cid:
∀ habd habd' n,
uctx_set_retval1_spec n habd = Some habd'
→ cid 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'
→ cid 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'
→ cid habd = cid habd'.
Proof.
unfold uctx_set_retval3_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_set_retval4_maintains_cid:
∀ habd habd' n,
uctx_set_retval4_spec n habd = Some habd'
→ cid habd = cid habd'.
Proof.
unfold uctx_set_retval4_spec; intros.
subdestruct; inv H; reflexivity.
Qed.
Lemma uctx_arg1_exist {re1: relate_impl_iflags}
{re2: relate_impl_cid} {re3: relate_impl_uctxt}:
∀ s habd z labd f,
uctx_arg1_spec habd = Some z →
0 ≤ 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}:
∀ s habd z labd f,
uctx_arg2_spec habd = Some z →
0 ≤ 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}:
∀ s habd z labd f,
uctx_arg3_spec habd = Some z →
0 ≤ 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}:
∀ s habd z labd f,
uctx_arg4_spec habd = Some z →
0 ≤ 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_arg5_exist {re1: relate_impl_iflags}
{re2: relate_impl_cid} {re3: relate_impl_uctxt}:
∀ s habd z labd f,
uctx_arg5_spec habd = Some z →
0 ≤ cid habd < num_proc →
relate_AbData s f habd labd →
uctx_arg5_spec labd = Some z.
Proof. apply uctx_argn_exist; split; [ discriminate | reflexivity ]. Qed.
Lemma uctx_arg6_exist {re1: relate_impl_iflags}
{re2: relate_impl_cid} {re3: relate_impl_uctxt}:
∀ s habd z labd f,
uctx_arg6_spec habd = Some z →
0 ≤ cid habd < num_proc →
relate_AbData s f habd labd →
uctx_arg6_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}:
∀ s habd habd' labd n f,
uctx_set_retval1_spec n habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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}:
∀ s habd habd' labd n f,
uctx_set_retval2_spec n habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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_ECX.
Lemma uctx_set_retval3_exist {re1: relate_impl_iflags}
{re2: relate_impl_cid} {re3: relate_impl_uctxt}:
∀ s habd habd' labd n f,
uctx_set_retval3_spec n habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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_EDX.
Lemma uctx_set_retval4_exist {re1: relate_impl_iflags}
{re2: relate_impl_cid} {re3: relate_impl_uctxt}:
∀ s habd habd' labd n f,
uctx_set_retval4_spec n habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd', uctx_set_retval4_spec n labd = Some labd'
∧ relate_AbData s f habd' labd'.
Proof uctx_set_regk_exist U_ESI.
Section TRAP_SENDTOCHAN_PRE_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_abq}.
Context {re10: relate_impl_abtcb}.
Lemma trap_sendtochan_pre_exist:
∀ s habd habd' labd r f,
trap_sendtochan_pre_spec habd = Some (habd', r)
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd', trap_sendtochan_pre_spec labd = Some (labd', r)
∧ relate_AbData s f habd' labd'.
Proof.
unfold trap_sendtochan_pre_spec in ×. intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
erewrite uctx_arg3_exist; eauto.
erewrite uctx_arg4_exist; eauto.
exploit syncsendto_chan_pre_exist; eauto.
Qed.
End TRAP_SENDTOCHAN_PRE_SIM.
Section TRAP_SENDTOCHAN_POST_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_abq}.
Context {re10: relate_impl_abtcb}.
Lemma trap_sendtochan_post_exist:
∀ s habd habd' labd f,
trap_sendtochan_post_spec habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd', trap_sendtochan_post_spec labd = Some labd'
∧ relate_AbData s f habd' labd'.
Proof.
unfold trap_sendtochan_post_spec in ×. intros.
subdestruct.
exploit syncsendto_chan_post_exist; eauto.
intros (labd' & HP & HR).
rewrite HP.
erewrite syncsendto_chan_post_maintains_cid in H1; eauto.
exploit uctx_set_retval1_exist; eauto. intros (labd'' & HP' & HR').
rewrite HP'.
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
Qed.
End TRAP_SENDTOCHAN_POST_SIM.
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_abq}.
Context {re7: relate_impl_abtcb}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_HP}.
Context {re10: relate_impl_init}.
Context {re11: relate_impl_ptpool}.
Context {re12: relate_impl_PT}.
Context {re13: relate_impl_nps}.
Lemma trap_receivechan_exist:
∀ s habd habd' labd f,
trap_receivechan_spec habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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 syncreceive_chan_exist; eauto. intros (labd' & HP & HR).
rewrite HP.
erewrite syncreceive_chan_maintains_cid in H1; eauto.
exploit uctx_set_retval1_exist; eauto. intros (labd'' & HP' & HR').
rewrite HP'.
erewrite uctx_set_retval1_maintains_cid in H1; eauto.
eapply uctx_set_regk_exist; eassumption.
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}.
Lemma trap_get_quota_exist:
∀ s habd habd' labd f,
trap_get_quota_spec habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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 get_curid_exist; eauto.
erewrite container_get_quota_exist; eauto.
erewrite 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 DEVOUT_SIM.
Context {re1: relate_impl_devout}.
Context {re2: relate_impl_cid}.
Context {re4: relate_impl_iflags}.
Context {re5: relate_impl_uctxt}.
Lemma print_exist:
∀ s habd habd' labd f,
print_spec habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd', print_spec labd = Some labd' ∧
relate_AbData s f habd' labd'.
Proof.
unfold print_spec; intros.
subdestruct.
erewrite uctx_arg2_exist; eauto.
exploit relate_impl_devout_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H; subrewrite.
eapply uctx_set_regk_exist; eauto.
eapply relate_impl_devout_update. assumption.
Qed.
End DEVOUT_SIM.
Section TRAP_OFFER_SHARED_MEM_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_HP}.
Context {re9: relate_impl_smspool}.
Context {re10: relate_impl_AC}.
Context {re11: relate_impl_cid}.
Context {re12: relate_impl_uctxt}.
Lemma trap_offer_shared_mem_exist:
∀ s habd habd' labd f,
trap_offer_shared_mem_spec habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd', trap_offer_shared_mem_spec labd = Some labd'
∧ relate_AbData s f habd' labd'.
Proof.
unfold trap_offer_shared_mem_spec in ×. intros.
exploit relate_impl_cid_eq; eauto. intros.
subdestruct.
- erewrite uctx_arg2_exist; eauto.
rewrite <- H2. rewrite e. simpl.
exploit offer_shared_mem_exists; eauto.
intros (labd' & → & Hr).
assert (Hrange: 0 ≤ cid r < num_proc) by
(erewrite <- offer_shared_mem_maintains_cid; eauto).
exploit uctx_set_retval1_exist; eauto.
intros (labd'' & → & HR').
eapply uctx_set_regk_exist; eauto.
erewrite <- uctx_set_retval1_maintains_cid; eauto.
- erewrite uctx_arg2_exist; eauto.
rewrite <- H2. rewrite zeq_false; trivial.
eapply uctx_set_regk_exist; eauto.
Qed.
End TRAP_OFFER_SHARED_MEM_SIM.
Section PTFAULT_RESV_SPEC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_HP}.
Context {re9: relate_impl_cid}.
Context {re10: relate_impl_uctxt}.
Context {re11: relate_impl_AC}.
Lemma ptfault_resv_exist:
∀ s habd habd' labd n f,
ptfault_resv_spec n habd = Some habd'
→ relate_AbData s f habd labd
→ 0 ≤ 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_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
revert H. subrewrite. subdestruct.
- exploit ptResv_exist; eauto. intros [ labd' [ → rel' ] ].
inv HQ; refine_split'; trivial.
- inv HQ; refine_split'; trivial.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_LAT}.
Context {mt3: match_impl_ptpool}.
Context {mt4: match_impl_HP}.
Context {mt5: match_impl_uctxt}.
Context {mt6: match_impl_AC}.
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.
eapply 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 ≤ 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_kctxt}.
Context {re4: relate_impl_abtcb}.
Context {re5: relate_impl_abq}.
Context {re6: relate_impl_uctxt}.
Context {re7: relate_impl_cid}.
Context {re8: relate_impl_AC}.
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 ≤ 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. intros.
exploit relate_impl_AC_eq; eauto; intro HAC.
exploit relate_impl_cid_eq; eauto; intro Hcid.
rewrite <- HAC; rewrite <- Hcid.
destruct (uctx_arg3_spec habd) eqn:Harg3; try discriminate H.
erewrite uctx_arg3_exist; eauto.
subdestruct; try solve [eapply uctx_set_regk_exist; eassumption].
assert (f b0 = Some (b0, 0)).
{ apply H2.
unfold Mem.flat_inj.
apply genv_symb_range in Hdestruct6.
destruct (plt b0 (genv_next s)); [ reflexivity | contradiction ].
}
assert (f b3 = Some (b3, 0)).
{ apply H2.
unfold Mem.flat_inj.
rewrite <- e in Hdestruct7.
apply genv_symb_range in Hdestruct7.
destruct (plt b3 (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 <- <-.
rewrite Hdestruct11, Int.add_zero, Hdestruct12.
exploit proc_create_exist; eauto. intros (? & → & ?).
erewrite proc_create_maintains_cid in H3; eauto.
exploit uctx_set_retval1_exist; eauto. intros (? & → & ?).
erewrite uctx_set_retval1_maintains_cid in H3; eauto.
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_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re9: relate_impl_smspool}.
Context {re10: relate_impl_abtcb}.
Context {re11: relate_impl_abq}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_syncchpool}.
Context {re14: relate_impl_vmxinfo}.
Context {re15: relate_impl_pperm}.
Context {re16: relate_impl_HP}.
Context {re17: relate_impl_ept}.
Context {re18: relate_impl_kctxt}.
Context {re19: relate_impl_uctxt}.
Context {re22: relate_impl_AC}.
Context {re23: relate_impl_devout}.
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 ≤ 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 trap_get_quota_exist; eauto.
eapply trap_offer_shared_mem_exist; eauto.
eapply print_exist; eauto.
Qed.
End SYS_DISPATCH_C_SIM.
End OBJ_SIM.