Library mcertikos.trap.SysCallGenAsmData
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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 liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import TDispatch.
Require Import SysCallGenAsmSource.
Require Import AbstractDataType.
Section ASM_DATA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
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 proc_start_generate:
∀ abd1 abd´ rs´ m,
proc_start_user_spec abd1 = Some (abd´, rs´) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 proc_start_user_spec in ×.
subdestruct. subst v.
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 (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 (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_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 (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 (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_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 (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 (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 6).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
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 (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 (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 5).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval4_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval4_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 proc_exit_generate:
∀ m abd abd1 uctx,
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 (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. auto.
Qed.
Lemma vmx_set_mmap_generate:
∀ abd0 abd1 m v1 v2 v3 z,
vmx_set_mmap_spec v1 v2 v3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 H4; simpl; eauto.
Qed.
Lemma vmx_set_reg_generate:
∀ abd0 abd1 m v1 v2,
vmx_set_reg_spec v1 v2 abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 sys_get_generate:
∀ m shadow labd abd abd´ abd0 abd1 rs´ uctx n,
proc_exit_user_spec labd uctx = Some abd →
uctx_set_retval1_spec shadow abd = Some abd0 →
uctx_set_errno_spec n abd0 = Some abd1 →
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 proc_start_generate; eauto.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply proc_exit_generate; eauto.
Qed.
Lemma sys_yield_generate:
∀ m labd abd abd0 rs´ uctx rs1,
proc_exit_user_spec labd uctx = Some abd →
thread_yield_spec abd rs´ = Some (abd0, rs1) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
(∀ v r, ZtoPreg v = Some r →
Val.has_type (rs1 r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m))
(rs1 r) (rs1 r)).
Proof.
intros.
functional inversion H; subst.
Opaque remove.
unfold thread_yield_spec in H0; simpl in H0.
rewrite H5, H6 in H0; simpl in H0. subdestruct. inv H0. inv H1.
assert(HIn: In (last l num_proc) l).
{
apply last_correct; auto.
}
assert (HOS: 0≤ num_proc ≤ num_proc) by omega.
unfold AbQCorrect in ×.
specialize (valid_TDQ H6 _ HOS).
destruct valid_TDQ as [lt[HM HP]].
rewrite Hdestruct in HM. inv HM.
inv H2.
eapply kctxt_INJECT.
apply HP; trivial.
eassumption.
Qed.
Lemma ptInsertPTE0_generate:
∀ abd0 abd1 m n vadr v1 v2,
ptInsertPTE0_spec n vadr v1 v2 abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 ptAllocPDE0_generate:
∀ abd0 abd1 m n vadr z,
ptAllocPDE0_spec n vadr abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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.
Qed.
Lemma ptInsert0_generate:
∀ abd0 abd1 m n vadr v1 v2 z,
ptInsert0_spec n vadr v1 v2 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 pgf_handler_generate:
∀ m labd abd abd´ abd0 rs´ uctx vadr,
proc_exit_user_spec labd uctx = Some abd →
ptfault_resv_spec vadr abd = Some abd0 →
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 ×.
unfold ptfault_resv_spec in *; simpl in ×.
unfold ptResv_spec in ×.
unfold palloc_spec in *; simpl in ×.
subdestruct;
refine_split´; trivial.
- eapply proc_start_generate; eauto.
inv H0. simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
inv H0. eapply ptInsert0_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
inv H0. simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
inv H0. simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
Qed.
Lemma sys_run_vm_generate:
∀ m labd abd abd0 rs´ uctx rs0,
proc_exit_user_spec labd uctx = Some abd →
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.
unfold vm_run_spec in H0; simpl in H0.
subdestruct. inv H0.
inv H2. inv VMX_INJECT.
destruct r as [| [] | [] | | [] |]; try (split; constructor); try eapply H0.
Qed.
Lemma sys_sendtochan_pre_generate:
∀ m labd abd abd0 abd1 rs´ uctx chanid rs_yield,
proc_exit_user_spec labd uctx = Some abd →
trap_sendtochan_pre_spec abd = Some (abd0, Int.unsigned chanid) →
thread_sleep_spec abd0 rs_yield (Int.unsigned chanid) = Some (abd1, rs´) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
(∀ v r, ZtoPreg v = Some 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.
unfold thread_sleep_spec in H1.
unfold proc_exit_user_spec in H.
unfold trap_sendtochan_pre_spec in H0.
subdestruct; inv H1. inv H. inv H0.
assert(HIn: In (last l num_proc) l).
{
apply last_correct; auto.
}
assert (HOS: 0≤ num_proc ≤ num_proc) by omega.
unfold AbQCorrect_range, AbQCorrect in ×.
inv H2.
specialize (valid_TDQ Hdestruct0 _ HOS).
destruct valid_TDQ as [lt[HM HP]].
functional inversion H1; simpl in ×.
- inv H; simpl in *; rewrite Hdestruct10 in HM. inv HM.
eapply kctxt_INJECT; eauto.
- inv H. inv H17. simpl in ×.
rewrite Hdestruct10 in HM. inv HM.
eapply kctxt_INJECT; eauto.
Qed.
Lemma trap_sendtochan_post_generate:
∀ abd0 abd m,
trap_sendtochan_post_spec abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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.
functional inversion H3;
subst; simpl; auto.
Qed.
Lemma sys_sendtochan_post_generate:
∀ m abd abd´ abd0 rs´,
trap_sendtochan_post_spec abd = Some abd0 →
proc_start_user_spec abd0 = Some (abd´, rs´) →
high_level_invariant abd →
low_level_invariant (Mem.nextblock m) abd →
(∀ 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 proc_start_generate; eauto.
eapply trap_sendtochan_post_generate; eauto.
inv H1. unfold uctxt_inject_neutral in ×.
intros; eapply uctxt_INJECT; eauto.
Qed.
Lemma ptResv_generate:
∀ abd0 abd1 m v1 v2 v3 z,
ptResv_spec v1 v2 v3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 ptInsert0_generate; eauto.
functional inversion H3; subst; eauto.
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 (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 (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.
destruct (zle_le 0 z
(cquota (ZMap.get (cid abd0) (AC abd0)) -
cusage (ZMap.get (cid abd0) (AC abd0)))) eqn:Hquota; subdestruct; subst.
- eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
unfold proc_create_spec in ×. subdestruct; subst.
inv Hdestruct17; simpl in ×.
intros; inv_proc; try (split; constructor; fail).
split. constructor.
econstructor.
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr. assumption.
rewrite Int.add_zero. reflexivity.
- eapply set_errno_generate; eauto.
Qed.
Lemma serial_intr_enable_aux_generate:
∀ abd0 abd1 m n,
serial_intr_enable_aux n abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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_generate:
∀ abd0 abd1 m,
serial_intr_enable_spec abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 serial_intr_enable_aux_generate; eauto.
Qed.
Lemma serial_intr_disable_aux_generate:
∀ abd0 abd1 m n masked,
serial_intr_disable_aux n masked abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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_generate:
∀ abd0 abd1 m,
serial_intr_disable_spec abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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 serial_intr_disable_aux_generate; eauto.
Qed.
Lemma serial_putc_generate:
∀ abd0 abd1 m c,
serial_putc_spec c abd0 = Some abd1→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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.
Qed.
Lemma cons_buf_read_generate:
∀ abd0 abd1 m c,
cons_buf_read_spec abd0 = Some (abd1, c)→
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (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 (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; clear H7; unfold s, b in *; subst; 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 (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 (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.
-
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 H.
+ eapply set_errno_generate; eauto.
eapply set_retval4_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_retval1_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply vmx_set_mmap_generate; eauto.
eapply ptResv_generate; eauto.
+ eapply set_errno_generate; eauto.
eapply vmx_set_mmap_generate; eauto.
+ eapply set_errno_generate; eauto.
-
functional inversion H.
+ eapply set_errno_generate; eauto.
eapply 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 H9; 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 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 H.
eapply set_errno_generate; eauto.
eapply vmx_set_reg_generate; eauto.
eapply vmx_set_reg_generate; eauto.
eapply vmx_set_reg_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply vmx_set_reg_generate; 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 H6; simpl; subst; eauto.
functional inversion H21; simpl; eauto;
functional inversion H20; simpl; eauto.
Require Import INVLemmaInterrupt.
-
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.
-
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.
Qed.
Lemma sys_dispatch_generate:
∀ m labd abd abd´ abd0 rs´ uctx s,
proc_exit_user_spec labd uctx = Some abd →
sys_dispatch_c_spec s m abd = Some abd0 →
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 proc_start_generate; eauto.
eapply sys_dispatch_c_generate; eauto.
eapply proc_exit_generate; 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_compatsem proc_start_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_start_user tdispatch =
OK (Some (primcall_start_user_compatsem 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_compatsem proc_exit_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_exit_user tdispatch =
OK (Some (primcall_exit_user_compatsem proc_exit_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hyield:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge thread_yield = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external thread_yield thread_yield_sig)))
∧ get_layer_primitive thread_yield tdispatch =
OK (Some (primcall_thread_schedule_compatsem
thread_yield_spec (prim_ident:= thread_yield))).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_yield tdispatch =
OK (Some (primcall_thread_schedule_compatsem
thread_yield_spec (prim_ident:= thread_yield))))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsleep:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge thread_sleep = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external thread_sleep thread_sleep_sig)))
∧ get_layer_primitive thread_sleep tdispatch =
OK (Some (primcall_thread_transfer_compatsem thread_sleep_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_sleep tdispatch =
OK (Some (primcall_thread_transfer_compatsem thread_sleep_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
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 vm_run_spec vmx_run_vm)).
Proof.
intros.
assert (Hprim: get_layer_primitive vmx_run_vm tdispatch =
OK (Some (primcall_vmx_enter_compatsem 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 trap_info_get_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_get tdispatch =
OK (Some (primcall_trap_info_get_compatsem 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 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 Hsendpre:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_sendtochan_pre = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_sendtochan_pre trap_sendtochan_pre_sig)))
∧ get_layer_primitive trap_sendtochan_pre tdispatch =
OK (Some (gensem trap_sendtochan_pre_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_sendtochan_pre tdispatch =
OK (Some (gensem trap_sendtochan_pre_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsendpost:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_sendtochan_post = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_sendtochan_post null_signature)))
∧ get_layer_primitive trap_sendtochan_post tdispatch =
OK (Some (gensem trap_sendtochan_post_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_sendtochan_post tdispatch =
OK (Some (gensem trap_sendtochan_post_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsys_yield:
∀ ge s b,
make_globalenv s (sys_yield ↦ sys_yield_function) tdispatch = ret ge →
find_symbol s sys_yield = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_yield_function).
Proof.
intros.
assert (Hmodule: get_module_function sys_yield (sys_yield ↦ sys_yield_function)
= OK (Some sys_yield_function)) by
reflexivity.
assert (HInternal: make_internal sys_yield_function = OK (AST.Internal sys_yield_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_sendtochan_pre:
∀ ge s b,
make_globalenv s (sys_sendtochan_pre ↦ sys_sendtochan_pre_function) tdispatch = ret ge →
find_symbol s sys_sendtochan_pre = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_sendtochan_pre_function).
Proof.
intros.
assert (Hmodule: get_module_function sys_sendtochan_pre (sys_sendtochan_pre ↦ sys_sendtochan_pre_function)
= OK (Some sys_sendtochan_pre_function)) by
reflexivity.
assert (HInternal: make_internal sys_sendtochan_pre_function =
OK (AST.Internal sys_sendtochan_pre_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_sendtochan_post:
∀ ge s b,
make_globalenv s (sys_sendtochan_post ↦ sys_sendtochan_post_function) tdispatch = ret ge →
find_symbol s sys_sendtochan_post = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_sendtochan_post_function).
Proof.
intros.
assert (Hmodule: get_module_function sys_sendtochan_post (sys_sendtochan_post ↦ sys_sendtochan_post_function)
= OK (Some sys_sendtochan_post_function)) by
reflexivity.
assert (HInternal: make_internal sys_sendtochan_post_function =
OK (AST.Internal sys_sendtochan_post_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.