Library mcertikos.trap.SysCallGenAsmData
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
Require Import Conventions.
Require Import TDispatch.
Require Import SysCallGenAsmSource.
Require Import AbstractDataType.
Require Import IntelPrimSemantics.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Opaque full_thread_list.
Section ASM_DATA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Lemma thread_proc_start_generate:
∀ abd1 abd´ rs´ m,
thread_proc_start_user_spec abd1 = Some (abd´, rs´) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros.
unfold thread_proc_start_user_spec in ×.
unfold ObjProc.proc_start_user_spec in ×.
subdestruct. subst v.
inv H. eauto.
Qed.
Lemma thread_proc_start_ueip_value:
∀ abd1 abd´ rs´,
thread_proc_start_user_spec abd1 = Some (abd´, rs´) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)) =
ZMap.get U_EIP rs´.
Proof.
intros.
unfold thread_proc_start_user_spec in ×.
unfold ObjProc.proc_start_user_spec in ×.
subdestruct.
inv H. eauto.
Qed.
Lemma set_errno_generate:
∀ abd0 abd1 m n,
uctx_set_errno_spec n abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx´ uctx.
destruct (zeq i 7).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_errno_ueip_value:
∀ abd0 abd1 n,
uctx_set_errno_spec n abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
unfold uctx´, uctx, curid.
rewrite ZMap.gss.
rewrite ZMap.gso; [ | intro contra; inv contra].
reflexivity.
Qed.
Lemma set_retval1_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval1_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx´ uctx.
destruct (zeq i 4).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval1_ueip_value:
∀ abd0 abd1 shadow,
uctx_set_retval1_spec shadow abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
unfold uctx´, uctx, curid.
rewrite ZMap.gss.
rewrite ZMap.gso; [ | intro contra; inv contra].
reflexivity.
Qed.
Lemma set_retval2_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval2_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx´ uctx.
destruct (zeq i 1).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval2_ueip_value:
∀ abd0 abd1 shadow,
uctx_set_retval2_spec shadow abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
unfold uctx´, uctx, curid.
rewrite ZMap.gss.
rewrite ZMap.gso; [ | intro contra; inv contra].
reflexivity.
Qed.
Lemma set_retval3_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval3_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx´ uctx.
destruct (zeq i 0).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval3_ueip_value:
∀ abd0 abd1 shadow,
uctx_set_retval3_spec shadow abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
unfold uctx´, uctx, curid.
rewrite ZMap.gss.
rewrite ZMap.gso; [ | intro contra; inv contra].
reflexivity.
Qed.
Lemma thread_proc_exit_generate:
∀ m abd abd1 uctx,
thread_proc_exit_user_spec abd uctx = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
unfold thread_proc_exit_user_spec in ×.
unfold ObjProc.proc_exit_user_spec in ×.
subdestruct; inv H; simpl in ×.
repeat rewrite ZMap.gss. auto.
Qed.
Lemma thread_proc_exit_ueip_value:
∀ abd abd1 uctx,
thread_proc_exit_user_spec abd uctx = Some abd1 →
ZMap.get U_EIP uctx =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
unfold thread_proc_exit_user_spec in ×.
unfold ObjProc.proc_exit_user_spec in ×.
subdestruct; inv H; simpl in ×.
repeat rewrite ZMap.gss. auto.
Qed.
Lemma thread_vmx_set_mmap_generate:
∀ abd0 abd1 m v1 v2 v3 z,
thread_vmx_set_mmap_spec v1 v2 v3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
functional inversion H2; simpl; subst.
functional inversion H7; simpl; eauto.
functional inversion H7; simpl; eauto.
Qed.
Lemma thread_vmx_set_mmap_ueip_value:
∀ abd0 abd1 v1 v2 v3 z,
thread_vmx_set_mmap_spec v1 v2 v3 abd0 = Some (abd1, z) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
functional inversion H0; simpl; subst.
functional inversion H5; simpl; eauto.
functional inversion H5; simpl; eauto.
Qed.
Lemma thread_vmx_set_reg_generate:
∀ abd0 abd1 m v1 v2,
thread_vmx_set_reg_spec v1 v2 abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
functional inversion H2; simpl; eauto.
Qed.
Lemma thread_vmx_set_reg_ueip_value:
∀ abd0 abd1 v1 v2,
thread_vmx_set_reg_spec v1 v2 abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
functional inversion H0; simpl; eauto.
Qed.
Lemma sys_get_generate:
∀ m shadow labd abd abd´ abd0 abd1 rs´ uctx n,
thread_proc_exit_user_spec labd uctx = Some abd →
uctx_set_retval1_spec shadow abd = Some abd0 →
uctx_set_errno_spec n abd0 = Some abd1 →
thread_proc_start_user_spec abd1 = Some (abd´, rs´) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros.
eapply thread_proc_start_generate; eauto.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply thread_proc_exit_generate; eauto.
Qed.
Lemma sys_get_ueip_value:
∀ shadow labd abd abd´ abd0 abd1 rs´ uctx n,
thread_proc_exit_user_spec labd uctx = Some abd →
uctx_set_retval1_spec shadow abd = Some abd0 →
uctx_set_errno_spec n abd0 = Some abd1 →
thread_proc_start_user_spec abd1 = Some (abd´, rs´) →
ZMap.get U_EIP uctx = ZMap.get U_EIP rs´.
Proof.
intros.
eapply thread_proc_start_ueip_value in H2.
eapply set_errno_ueip_value in H1.
eapply set_retval1_ueip_value in H0.
eapply thread_proc_exit_ueip_value in H; auto.
congruence.
Qed.
Lemma ptInsertPTE0_generate:
∀ abd0 abd1 m n vadr v1 v2,
big2_ptInsertPTE0_spec n vadr v1 v2 abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl; eauto.
Qed.
Lemma ptInsertPTE0_ueip_value:
∀ abd0 abd1 n vadr v1 v2,
big2_ptInsertPTE0_spec n vadr v1 v2 abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl; eauto.
Qed.
Lemma palloc_generate:
∀ abd0 abd1 m v1 z,
big2_palloc_spec v1 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
unfold big2_palloc_spec in H; subdestruct; inv H; simpl in *; eauto.
Qed.
Lemma palloc_ueip_value:
∀ abd0 abd1 v1 z,
big2_palloc_spec v1 abd0 = Some (abd1, z) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
unfold big2_palloc_spec in H; subdestruct; inv H; simpl in *; eauto.
Qed.
Lemma ptAllocPDE0_generate:
∀ abd0 abd1 m n vadr z,
big2_ptAllocPDE_spec n vadr abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl; subst; eauto.
eapply palloc_generate; eauto.
eapply palloc_generate; eauto.
Qed.
Lemma ptAllocPDE0_ueip_value:
∀ abd0 abd1 n vadr z,
big2_ptAllocPDE_spec n vadr abd0 = Some (abd1, z) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl; subst; eauto.
eapply palloc_ueip_value; eauto.
eapply palloc_ueip_value; eauto.
Qed.
Lemma ptInsert_generate:
∀ abd0 abd1 m n vadr v1 v2 z,
big2_ptInsert_spec n vadr v1 v2 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
- eapply ptInsertPTE0_generate; eauto.
- eapply ptAllocPDE0_generate; eauto.
- eapply ptInsertPTE0_generate; eauto.
eapply ptAllocPDE0_generate; eauto.
Qed.
Lemma ptInsert_ueip_value:
∀ abd0 abd1 n vadr v1 v2 z,
big2_ptInsert_spec n vadr v1 v2 abd0 = Some (abd1, z) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; simpl.
- eapply ptInsertPTE0_ueip_value; eauto.
- eapply ptAllocPDE0_ueip_value; eauto.
- eapply ptInsertPTE0_ueip_value in H12; eauto.
eapply ptAllocPDE0_ueip_value in H10; eauto.
rewrite H10, H12; reflexivity.
Qed.
Lemma ptResv_generate:
∀ abd0 abd1 m v1 v2 v3 z,
big2_ptResv_spec v1 v2 v3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
- eapply palloc_generate; eauto.
- eapply ptInsert_generate; eauto.
eapply palloc_generate; eauto.
Qed.
Lemma ptResv_ueip_value:
∀ abd0 abd1 v1 v2 v3 z,
big2_ptResv_spec v1 v2 v3 abd0 = Some (abd1, z) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; subst; simpl; eauto.
- eapply palloc_ueip_value; eauto.
- eapply ptInsert_ueip_value in H0; eauto.
eapply palloc_ueip_value in H2; eauto.
rewrite H2, H0; reflexivity.
Qed.
Lemma pgf_handler_generate:
∀ m labd abd abd´ abd0 rs´ uctx vadr,
thread_proc_exit_user_spec labd uctx = Some abd →
ptfault_resv_spec vadr abd = Some abd0 →
thread_proc_start_user_spec abd0 = Some (abd´, rs´) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
ikern abd = true
∧ ihost abd = true
∧ (∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros.
functional inversion H; subst; simpl in ×.
functional inversion H0; subst; simpl in ×.
functional inversion H3; substx; simpl in ×.
refine_split´; trivial.
eapply thread_proc_start_generate; eauto.
eapply ptResv_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit thread_proc_exit_generate; eauto.
Qed.
Lemma pgf_handler_ueip_value_aux:
∀ abd abd0 vadr,
ptfault_resv_spec vadr abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H; subst; simpl in ×.
eapply ptResv_ueip_value in H1; eauto.
Qed.
Lemma pgf_handler_ueip_value:
∀ labd abd abd´ abd0 rs´ uctx vadr,
thread_proc_exit_user_spec labd uctx = Some abd →
ptfault_resv_spec vadr abd = Some abd0 →
thread_proc_start_user_spec abd0 = Some (abd´, rs´) →
ZMap.get U_EIP uctx = ZMap.get U_EIP rs´.
Proof.
intros.
eapply thread_proc_exit_ueip_value in H; auto.
eapply thread_proc_start_ueip_value in H1; auto.
eapply pgf_handler_ueip_value_aux in H0; auto.
congruence.
Qed.
Lemma sys_run_vm_generate:
∀ m labd abd abd0 rs´ uctx rs0,
thread_proc_exit_user_spec labd uctx = Some abd →
thread_vm_run_spec rs0 abd = Some (abd0, rs´) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
(∀ r, Val.has_type (rs´#r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)).
Proof.
intros. functional inversion H; subst.
functional inversion H3; subst.
unfold thread_vm_run_spec in H0; simpl in H0.
subdestruct.
unfold ObjVMX.vm_run_spec in H0; simpl in H0.
subdestruct. inv H0.
inv H2.
unfold VMXPool_inject_neutral in VMX_INJECT.
generalize a; intros VMX_INJECT_WID.
eapply VMX_INJECT in VMX_INJECT_WID; auto.
inv VMX_INJECT_WID.
destruct r as [| [] | [] | | [] |]; try (split; constructor); try eapply H0.
Qed.
Lemma sys_run_vm_ueip_value:
∀ labd abd abd0 rs´ uctx rs0,
thread_proc_exit_user_spec labd uctx = Some abd →
thread_vm_run_spec rs0 abd = Some (abd0, rs´) →
ZMap.get U_EIP uctx =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros. functional inversion H; subst.
functional inversion H1; subst.
unfold thread_vm_run_spec in H0; simpl in H0.
subdestruct.
unfold ObjVMX.vm_run_spec in H0; simpl in H0.
subdestruct. inv H0.
inv H2.
simpl.
unfold curid0.
rewrite ZMap.gss.
reflexivity.
Qed.
Lemma trap_proc_create_generate:
∀ abd0 abd1 m s,
trap_proc_create_spec s m abd0 = Some abd1 →
(genv_next s ≤ Mem.nextblock m)%positive →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
rename H into Hspec; unfold trap_proc_create_spec in Hspec.
destruct (uctx_arg3_spec abd0); try discriminate Hspec.
unfold thread_container_can_consume_spec.
unfold ObjContainer.container_can_consume_spec.
subdestruct; subst.
- eapply set_errno_generate; eauto.
- eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
unfold big2_proc_create_spec in ×. subdestruct; subst.
inv Hdestruct14; simpl in ×.
functional inversion Hdestruct16; subst; simpl in ×.
clear Hspec Hdestruct16.
intros. specialize (H1 i3 H).
destruct H1.
eauto.
- eapply set_errno_generate; eauto.
- eapply set_errno_generate; eauto.
- eapply set_errno_generate; eauto.
Qed.
Lemma trap_proc_create_ueip_value:
∀ abd0 abd1 m s,
trap_proc_create_spec s m abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
rename H into Hspec; unfold trap_proc_create_spec in Hspec.
destruct (uctx_arg3_spec abd0); try discriminate Hspec.
unfold thread_container_can_consume_spec.
unfold ObjContainer.container_can_consume_spec.
subdestruct; subst.
- eapply set_errno_ueip_value; eauto.
- eapply set_errno_ueip_value in Hspec; eauto.
eapply set_retval1_ueip_value in Hdestruct16; eauto.
unfold big2_proc_create_spec in ×.
subdestruct; subst.
inv Hdestruct14; simpl in ×.
rewrite Hdestruct16, Hspec.
reflexivity.
- eapply set_errno_ueip_value; eauto.
- eapply set_errno_ueip_value; eauto.
- eapply set_errno_ueip_value; eauto.
Qed.
Lemma big_acquire_lock_SC_generate:
∀ abd0 abd v1 m,
big2_acquire_lock_SC_spec v1 abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
unfold big2_acquire_lock_SC_spec in H; subdestruct; inv H; subst; simpl in *; eauto.
Qed.
Lemma big_acquire_lock_SC_ueip_value:
∀ abd0 abd v1,
big2_acquire_lock_SC_spec v1 abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
unfold big2_acquire_lock_SC_spec in H; subdestruct; inv H; subst; simpl in *; eauto.
Qed.
Lemma big_release_lock_SC_generate:
∀ abd0 abd v1 m,
big2_release_lock_SC_spec v1 abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl in *; eauto.
functional inversion H2; subst; simpl in *; eauto.
Qed.
Lemma big_release_lock_SC_ueip_value:
∀ abd0 abd v1,
big2_release_lock_SC_spec v1 abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H; subst; simpl in *; eauto.
functional inversion H0; subst; simpl in *; eauto.
Qed.
Lemma syncreceive_chan_generate:
∀ abd0 abd v0 v1 v2 r m,
thread_syncreceive_chan_spec v0 v1 v2 abd = Some (abd0, r) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl in *; eauto.
eapply big_release_lock_SC_generate; eauto.
functional inversion H9; unfold chid0, cpu0 in *; subst; simpl; eauto.
- eapply big_acquire_lock_SC_generate; eauto.
- functional inversion H20; subst; eauto; simpl in ×.
functional inversion H2; subst; eauto; simpl in ×.
functional inversion H21; unfold me, l´, l1, me, to in *; subst; eauto; simpl in ×.
functional inversion H33; substx; eauto; simpl in ×.
eapply big_acquire_lock_SC_generate; eauto.
- functional inversion H20.
functional inversion H2; subst.
functional inversion H21; unfold me, l´, l1, me, to in *; subst; eauto; simpl in ×.
functional inversion H33; eauto; simpl in *;
try eapply big_acquire_lock_SC_generate; eauto.
functional inversion H33; eauto; simpl in *;
try eapply big_acquire_lock_SC_generate; eauto.
functional inversion H33; eauto; simpl in *;
try eapply big_acquire_lock_SC_generate; eauto.
Qed.
Lemma syncreceive_chan_ueip_value:
∀ abd0 abd v0 v1 v2 r,
thread_syncreceive_chan_spec v0 v1 v2 abd = Some (abd0, r) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H; subst; simpl in *; eauto.
eapply big_release_lock_SC_ueip_value in H8; eauto.
functional inversion H7; unfold chid0, cpu0 in *; subst; simpl; eauto.
- eapply big_acquire_lock_SC_ueip_value in H6.
congruence.
- functional inversion H18; subst; eauto; simpl in ×.
functional inversion H0; subst; eauto; simpl in ×.
functional inversion H19; unfold me, l´, l1, me, to in *; subst; eauto; simpl in ×.
functional inversion H31; substx; eauto; simpl in ×.
eapply big_acquire_lock_SC_ueip_value in H6; eauto.
congruence.
- functional inversion H18; subst; eauto; simpl in ×.
functional inversion H0; subst; eauto; simpl in ×.
functional inversion H19; unfold me, l´, l1, me, to in *; subst; eauto; simpl in ×.
functional inversion H31; substx; eauto; simpl in ×.
eapply big_acquire_lock_SC_ueip_value in H6; eauto.
congruence.
functional inversion H31; substx; eauto; simpl in ×.
eapply big_acquire_lock_SC_ueip_value in H6; eauto.
congruence.
functional inversion H31; substx; eauto; simpl in ×.
eapply big_acquire_lock_SC_ueip_value in H6; eauto.
congruence.
Qed.
Lemma trap_receivechan_generate:
∀ abd0 abd m,
trap_receivechan_spec abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply syncreceive_chan_generate; eauto.
Qed.
Lemma trap_receivechan_ueip_value:
∀ abd0 abd,
trap_receivechan_spec abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H5; eauto.
eapply syncreceive_chan_ueip_value in H4.
congruence.
Qed.
Lemma syncsendto_chan_generate:
∀ abd0 abd v1 v2 v3 r m,
thread_syncsendto_chan_spec v1 v2 v3 abd = Some (abd0, r) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl in *; eauto.
eapply big_release_lock_SC_generate; eauto.
functional inversion H4; subst; simpl in *; eauto.
functional inversion H5; subst; simpl in *; eauto.
functional inversion H2; subst; simpl in *; eauto.
- functional inversion H24; subst; simpl in *; eauto.
eapply big_acquire_lock_SC_generate; eauto.
- functional inversion H5; simpl; eauto.
functional inversion H15; simpl; eauto.
functional inversion H26; simpl; eauto.
functional inversion H14; simpl; substx;
eapply big_acquire_lock_SC_generate; eauto; simpl.
+ eapply big_acquire_lock_SC_generate; eauto.
+ eapply big_acquire_lock_SC_generate; eauto.
Qed.
Lemma syncsendto_chan_ueip_value:
∀ abd0 abd v1 v2 v3 r,
thread_syncsendto_chan_spec v1 v2 v3 abd = Some (abd0, r) →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H; subst; simpl in *; eauto.
eapply big_release_lock_SC_ueip_value in H4; eauto.
functional inversion H2; subst; simpl in *; eauto.
functional inversion H3; subst; simpl in *; eauto.
functional inversion H0; subst; simpl in *; eauto.
functional inversion H22; subst; simpl in *; eauto.
- eapply big_acquire_lock_SC_ueip_value in H9; eauto.
rewrite H9; rewrite H4; reflexivity.
- functional inversion H3; simpl; eauto.
functional inversion H13; simpl; eauto.
functional inversion H24; simpl; eauto.
functional inversion H12; simpl; substx; eauto;
eapply big_acquire_lock_SC_ueip_value in H9; simpl in ×.
+ eapply big_acquire_lock_SC_ueip_value in H0; simpl in H0; congruence.
+ eapply big_acquire_lock_SC_ueip_value in H0; simpl in H0; congruence.
Qed.
Lemma trap_sendtochan_generate:
∀ abd0 abd m,
trap_sendtochan_spec abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply syncsendto_chan_generate; eauto.
Qed.
Lemma trap_sendtochan_ueip_value:
∀ abd0 abd,
trap_sendtochan_spec abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H5; eauto.
eapply syncsendto_chan_ueip_value in H4; eauto.
congruence.
Qed.
Lemma sys_yield_generate:
∀ abd0 abd m,
big2_thread_yield_spec abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get ((ZMap.get (CPU_ID abd) (cid abd)))
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl.
eauto.
eauto.
Qed.
Lemma sys_yield_ueip_value:
∀ abd0 abd,
big2_thread_yield_spec abd = Some abd0 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd) (cid abd)) (uctxt abd)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)).
Proof.
intros.
functional inversion H; subst; simpl.
eauto.
eauto.
Qed.
Lemma serial_intr_enable_aux_generate:
∀ abd0 abd1 m n,
ObjInterruptManagement.serial_intr_enable_aux n abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
generalize dependent abd0.
generalize dependent abd1.
generalize dependent i.
induction n.
{
simpl.
intros.
inv H; auto.
}
{
simpl.
intros.
subdestruct.
eapply IHn in H; eauto.
intros.
unfold v.
functional inversion Hdestruct0; subst; simpl in *; eauto.
inv H; auto.
}
Qed.
Lemma serial_intr_enable_aux_ueip_value:
∀ abd0 abd1 n,
ObjInterruptManagement.serial_intr_enable_aux n abd0 = Some abd1→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
generalize dependent abd0.
generalize dependent abd1.
induction n.
{
simpl.
intros.
inv H; auto.
}
{
simpl.
intros.
subdestruct.
eapply IHn in H; eauto.
intros.
functional inversion Hdestruct0; subst; simpl in *; eauto.
inv H; auto.
}
Qed.
Lemma serial_intr_enable_generate:
∀ abd0 abd1 m,
thread_serial_intr_enable_spec abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
functional inversion H2; subst; simpl; eauto.
eapply serial_intr_enable_aux_generate; eauto.
Qed.
Lemma serial_intr_enable_ueip_value:
∀ abd0 abd1,
thread_serial_intr_enable_spec abd0 = Some abd1→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; subst; simpl; eauto.
functional inversion H0; subst; simpl; eauto.
eapply serial_intr_enable_aux_ueip_value in H11.
simpl in ×.
rewrite H11.
auto.
Qed.
Lemma serial_intr_disable_aux_generate:
∀ abd0 abd1 m n masked,
ObjInterruptManagement.serial_intr_disable_aux n masked abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
generalize dependent abd0.
generalize dependent abd1.
generalize dependent i.
induction n.
{
simpl.
intros.
inv H; auto.
}
{
simpl.
intros.
subdestruct.
eapply IHn in H; eauto.
eapply IHn in H; eauto.
intros.
unfold v.
functional inversion Hdestruct1; subst; simpl in *; eauto.
inv H; auto.
}
Qed.
Lemma serial_intr_disable_aux_ueip_value:
∀ abd0 abd1 n masked,
ObjInterruptManagement.serial_intr_disable_aux n masked abd0 = Some abd1→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
generalize dependent abd0.
generalize dependent abd1.
induction n.
{
simpl.
intros.
inv H; auto.
}
{
simpl.
intros.
subdestruct.
eapply IHn in H; eauto.
eapply IHn in H; eauto.
intros.
functional inversion Hdestruct1; subst; simpl in *; eauto.
inv H; auto.
}
Qed.
Lemma serial_intr_disable_generate:
∀ abd0 abd1 m,
thread_serial_intr_disable_spec abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
functional inversion H2; subst; simpl; eauto;
eapply serial_intr_disable_aux_generate; eauto.
Qed.
Lemma serial_intr_disable_ueip_value:
∀ abd0 abd1,
thread_serial_intr_disable_spec abd0 = Some abd1→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; subst; simpl; eauto.
functional inversion H0; subst; simpl; eauto.
eapply serial_intr_disable_aux_ueip_value in H12; simpl in *; auto.
eapply serial_intr_disable_aux_ueip_value in H12; simpl in *; auto.
eapply serial_intr_disable_aux_ueip_value in H12; simpl in *; auto.
eapply serial_intr_disable_aux_ueip_value in H10; simpl in *; auto.
Qed.
Lemma serial_putc_generate:
∀ abd0 abd1 m c,
thread_serial_putc_spec c abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
functional inversion H2; subst; simpl; eauto.
Qed.
Lemma serial_putc_ueip_value:
∀ abd0 abd1 c,
thread_serial_putc_spec c abd0 = Some abd1→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; subst; simpl; eauto.
functional inversion H0; subst; simpl; eauto.
Qed.
Require Import FutureTactic.
Lemma cons_buf_read_generate:
∀ abd0 abd1 m c,
thread_cons_buf_read_spec abd0 = Some (abd1, c)→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; functional inversion H2; substx; simpl; eauto.
Qed.
Lemma cons_buf_read_ueip_value:
∀ abd0 abd1 c,
thread_cons_buf_read_spec abd0 = Some (abd1, c)→
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
functional inversion H; subst; simpl; eauto.
functional inversion H0; substx; simpl; eauto.
Qed.
Lemma sys_dispatch_c_generate:
∀ abd0 abd1 m s,
sys_dispatch_c_spec s m abd0 = Some abd1 →
∀ (Hgenv: (genv_next s ≤ Mem.nextblock m)%positive),
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0))
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1))
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
unfold sys_dispatch_c_spec in ×.
subdestruct;
try (eapply set_errno_generate; eauto; fail).
-
eapply trap_proc_create_generate; eauto.
-
eapply sys_yield_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval2_generate; eauto.
eapply set_retval1_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
functional inversion H5; simpl; try subst; eauto.
functional inversion H6; simpl; try subst; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply set_retval3_generate; eauto.
eapply set_retval2_generate; eauto.
eapply set_retval1_generate; eauto.
+ eapply set_errno_generate; eauto.
eapply set_retval2_generate; eauto.
eapply set_retval1_generate; eauto.
+ eapply set_errno_generate; eauto.
eapply set_retval2_generate; eauto.
eapply set_retval1_generate; eauto.
+ eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply thread_vmx_set_mmap_generate; eauto.
eapply ptResv_generate; eauto.
+ eapply set_errno_generate; eauto.
eapply thread_vmx_set_mmap_generate; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply thread_vmx_set_reg_generate; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
functional inversion H7; simpl; subst; eauto.
functional inversion H8; simpl; subst; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
functional inversion H7; simpl; subst; eauto.
functional inversion H8; simpl; subst; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
functional inversion H6; simpl; subst; eauto.
functional inversion H7; simpl; subst; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
functional inversion H4; simpl; subst; eauto.
functional inversion H5; simpl; subst; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply thread_vmx_set_reg_generate; eauto.
eapply thread_vmx_set_reg_generate; eauto.
eapply thread_vmx_set_reg_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply thread_vmx_set_reg_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
- eapply trap_receivechan_generate; eauto.
- eapply trap_sendtochan_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply serial_intr_enable_generate; eauto.
eapply cons_buf_read_generate; eauto.
eapply serial_intr_disable_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply serial_intr_enable_generate; eauto.
eapply serial_putc_generate; eauto.
eapply serial_intr_disable_generate; eauto.
Qed.
Lemma sys_dispatch_c_ueip_value:
∀ abd0 abd1 m s,
sys_dispatch_c_spec s m abd0 = Some abd1 →
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd0) (cid abd0)) (uctxt abd0)) =
ZMap.get U_EIP (ZMap.get (ZMap.get (CPU_ID abd1) (cid abd1)) (uctxt abd1)).
Proof.
intros.
unfold sys_dispatch_c_spec in ×.
subdestruct;
try (eapply set_errno_ueip_value in H; simpl; eauto; congruence; fail).
-
eapply trap_proc_create_ueip_value in H; eauto.
-
eapply sys_yield_ueip_value in H; eauto.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval2_ueip_value in H3; eauto.
eapply set_retval1_ueip_value in H2; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
functional inversion H3; simpl; try subst; eauto.
functional inversion H4; simpl; try subst; eauto.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
eapply set_retval3_ueip_value in H12; eauto.
eapply set_retval2_ueip_value in H11; eauto.
eapply set_retval1_ueip_value in H9; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
eapply set_retval2_ueip_value in H12; eauto.
eapply set_retval1_ueip_value in H9; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
eapply set_retval2_ueip_value in H13; eauto.
eapply set_retval1_ueip_value in H9; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H9; eauto.
congruence.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
eapply thread_vmx_set_mmap_ueip_value in H11; eauto.
eapply ptResv_ueip_value in H8; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
eapply thread_vmx_set_mmap_ueip_value in H8; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
eapply thread_vmx_set_reg_ueip_value in H4; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H4; eauto.
congruence.
+ eapply set_errno_ueip_value in H0; eauto.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
functional inversion H5; simpl; subst; eauto.
functional inversion H6; simpl; subst; eauto.
+ eapply set_errno_ueip_value in H0; eauto.
-
functional inversion H.
+ eapply set_errno_ueip_value in H0; eauto.
functional inversion H5; simpl; subst; eauto.
functional inversion H6; simpl; subst; eauto.
+ eapply set_errno_ueip_value in H0; eauto.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H3; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
functional inversion H4; simpl; subst; eauto.
functional inversion H5; simpl; subst; eauto.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H2; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H2; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
functional inversion H2; simpl; subst; eauto.
functional inversion H3; simpl; subst; eauto.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply thread_vmx_set_reg_ueip_value in H3; eauto.
eapply thread_vmx_set_reg_ueip_value in H4; eauto.
eapply thread_vmx_set_reg_ueip_value in H7; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply thread_vmx_set_reg_ueip_value in H7; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H4; eauto.
congruence.
- eapply trap_receivechan_ueip_value; eauto.
- eapply trap_sendtochan_ueip_value; eauto.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply set_retval1_ueip_value in H5; eauto.
eapply serial_intr_enable_ueip_value in H4; eauto.
eapply cons_buf_read_ueip_value in H2; eauto.
eapply serial_intr_disable_ueip_value in H1; eauto.
congruence.
-
functional inversion H.
eapply set_errno_ueip_value in H0; eauto.
eapply serial_intr_enable_ueip_value in H5; eauto.
eapply serial_putc_ueip_value in H4; eauto.
eapply serial_intr_disable_ueip_value in H3; eauto.
congruence.
Qed.
Lemma sys_dispatch_generate:
∀ m labd abd abd´ abd0 rs´ uctx s,
thread_proc_exit_user_spec labd uctx = Some abd →
sys_dispatch_c_spec s m abd = Some abd0 →
thread_proc_start_user_spec abd0 = Some (abd´, rs´) →
(genv_next s ≤ Mem.nextblock m)%positive →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
eapply thread_proc_start_generate; eauto.
eapply sys_dispatch_c_generate; eauto.
eapply thread_proc_exit_generate; eauto.
Qed.
Lemma sys_dispatch_ueip_value:
∀ m labd abd abd´ abd0 rs´ uctx s,
thread_proc_exit_user_spec labd uctx = Some abd →
sys_dispatch_c_spec s m abd = Some abd0 →
thread_proc_start_user_spec abd0 = Some (abd´, rs´) →
ZMap.get U_EIP uctx = ZMap.get U_EIP rs´.
Proof.
intros.
eapply thread_proc_start_ueip_value in H1; eauto.
eapply sys_dispatch_c_ueip_value in H0; eauto.
eapply thread_proc_exit_ueip_value in H; eauto.
congruence.
Qed.
Lemma Hrun_vm:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge vmx_run_vm = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external vmx_run_vm null_signature)))
∧ get_layer_primitive vmx_run_vm tdispatch =
OK (Some (primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm)).
Proof.
intros.
assert (Hprim: get_layer_primitive vmx_run_vm tdispatch =
OK (Some (primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_get = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_get trap_get_sig)))
∧ get_layer_primitive trap_get tdispatch =
OK (Some (primcall_trap_info_get_compatsem thread_trap_info_get_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_get tdispatch =
OK (Some (primcall_trap_info_get_compatsem thread_trap_info_get_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hpgfr:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge ptfault_resv = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external ptfault_resv ptfault_resv_sig)))
∧ get_layer_primitive ptfault_resv tdispatch =
OK (Some (gensem ptfault_resv_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive ptfault_resv tdispatch =
OK (Some (gensem ptfault_resv_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hstart:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_start_user = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_start_user proc_start_user_sig)))
∧ get_layer_primitive proc_start_user tdispatch =
OK (Some (primcall_start_user_tm_compatsem thread_proc_start_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_start_user tdispatch =
OK (Some (primcall_start_user_tm_compatsem thread_proc_start_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hexit:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_exit_user = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_exit_user proc_exit_user_sig)))
∧ get_layer_primitive proc_exit_user tdispatch =
OK (Some (primcall_exit_user_tm_compatsem thread_proc_exit_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_exit_user tdispatch =
OK (Some (primcall_exit_user_tm_compatsem thread_proc_exit_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hstart2:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_start_user2 = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_start_user2 proc_start_user_sig)))
∧ get_layer_primitive proc_start_user2 tdispatch =
OK (Some (primcall_start_user_tm_compatsem2 thread_proc_start_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_start_user2 tdispatch =
OK (Some (primcall_start_user_tm_compatsem2 thread_proc_start_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hexit2:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_exit_user2 = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_exit_user2 proc_exit_user_sig)))
∧ get_layer_primitive proc_exit_user2 tdispatch =
OK (Some (primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_exit_user2 tdispatch =
OK (Some (primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hdispatch_c:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge syscall_dispatch_C = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external syscall_dispatch_C syscall_c_dispatch_sig)))
∧ get_layer_primitive syscall_dispatch_C tdispatch =
OK (Some (trap_proccreate_compatsem sys_dispatch_c_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive syscall_dispatch_C tdispatch =
OK (Some (trap_proccreate_compatsem sys_dispatch_c_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsys_dispatch_c:
∀ ge s b,
make_globalenv s (syscall_dispatch ↦ sys_dispatch_function) tdispatch = ret ge →
find_symbol s syscall_dispatch = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_dispatch_function).
Proof.
intros.
assert (Hmodule: get_module_function syscall_dispatch (syscall_dispatch ↦ sys_dispatch_function)
= OK (Some sys_dispatch_function)) by
reflexivity.
assert (HInternal: make_internal sys_dispatch_function = OK (AST.Internal sys_dispatch_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hsys_run_vm:
∀ ge s b,
make_globalenv s (sys_run_vm ↦ sys_run_vm_function) tdispatch = ret ge →
find_symbol s sys_run_vm = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_run_vm_function).
Proof.
intros.
assert (Hmodule: get_module_function sys_run_vm (sys_run_vm ↦ sys_run_vm_function)
= OK (Some sys_run_vm_function)) by
reflexivity.
assert (HInternal: make_internal sys_run_vm_function = OK (AST.Internal sys_run_vm_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hpgf_handler:
∀ ge s b,
make_globalenv s (pgf_handler ↦ pgf_handler_function) tdispatch = ret ge →
find_symbol s pgf_handler = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal pgf_handler_function).
Proof.
intros.
assert (Hmodule: get_module_function pgf_handler (pgf_handler ↦ pgf_handler_function)
= OK (Some pgf_handler_function)) by
reflexivity.
assert (HInternal: make_internal pgf_handler_function = OK (AST.Internal pgf_handler_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
End WITHMEM.
End ASM_DATA.