Library mcertikos.multithread.highrefins.PHThread2TGenLemmaPTRESV
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem3high.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmPHThread2T.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import PHThread2TComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import ObjBigThread.
Require Import BigLogThreadConfigFunction.
Require Import StencilImpl.
Require Import PHThread2TGenDef.
Opaque full_thread_list.
Section PHTHREAD2TGENLEMMAPTRESVFILE.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := s_oracle_prf.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Lemma ptResv_related_t:
∀ kctxt a a´ n vadr perm res l pd,
relate_RData kctxt a l pd →
big2_ptResv_spec (Int.unsigned n) (Int.unsigned vadr) (Int.unsigned perm) a = Some (a´, res) →
∃ l´ pd´ res´,
single_big_ptResv_spec (Int.unsigned n) (Int.unsigned vadr) (Int.unsigned perm)
(uRData l, pd) = Some ((uRData l´, pd´), res´) ∧
relate_RData kctxt a´ l´ pd´ ∧
proc_id (uRData l) = proc_id (uRData l´) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint n::Lint vadr::Lint perm::nil)
(choice_check pt_resv (Lint n::Lint vadr::Lint perm::nil) (uRData l) pd)
(snap_func pd))::l) ∧
res = res´.
Proof.
generalize int_max; intros max_val; intros.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
assert (prim_num: prim_id_num pt_resv = 2).
{ unfold prim_id_num; simpl; auto. }
functional inversion H0; subst.
-
unfold big2_palloc_spec in H4; subdestruct; substx; simpl in *; inv H4; try omega.
+ case_eq (first_free a0 (AbstractDataType.nps a)); intros; rewrite H1 in Hdestruct11; [inv Hdestruct11 | ].
unfold single_big_ptResv_spec; simpl.
inv H; rewritesb; rewrite zeq_true.
unfold single_big_palloc_spec; simpl in ×.
rewritesb.
rewrite zeq_true.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7, Hdestruct8.
rewrite e; simpl.
rewrite Hdestruct9, Hdestruct5.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true.
rewrite zeq_true.
∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 1 (snap_func pd))::l)).
refine_split´; eauto.
× simpl; rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; reflexivity.
× simpl; constructor; auto;
try (simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl;
rewritesb; rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1; rewrite zeq_true; auto; fail).
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl.
rewrite <- pg_re; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl.
rewrite <- init_re; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl.
rewrite e; simpl.
rewrite cid_eq; rewrite <- CPU_ID_re; reflexivity. }
{ rewrite e; reflexivity. }
{ inv inv_re; constructor; simpl.
- rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl; auto.
- rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl; auto. }
× simpl; rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, H1.
rewrite zeq_true; simpl.
rewrite e.
rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
× simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7, Hdestruct8.
rewrite e; simpl.
rewrite Hdestruct9.
unfold single_big_palloc_spec; simpl in ×.
unfold single_big_palloc_spec_share; simpl in ×.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7, Hdestruct8.
rewrite e; simpl.
rewrite Hdestruct9.
rewrite zeq_true.
rewrite Hdestruct0, Hdestruct3, Hdestruct5, Hdestruct6, Hdestruct10, H1; subst.
rewrite zeq_true; rewrite zeq_true.
rewrite <- e.
rewrite Int.repr_unsigned; auto.
+ unfold single_big_ptResv_spec; simpl.
inv H; rewritesb; rewrite zeq_true.
unfold single_big_palloc_spec; simpl in ×.
rewritesb.
rewrite zeq_true.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7, Hdestruct8.
rewrite e; simpl.
rewrite Hdestruct9, Hdestruct5.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true.
∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 0 (snap_func pd))::l)).
refine_split´; eauto.
× simpl; rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; reflexivity.
× simpl; constructor; auto;
try (simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl;
rewritesb; rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8; rewrite zeq_true; auto; fail).
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl.
rewrite <- pg_re; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl.
rewrite <- init_re; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl.
rewrite e; rewrite <- CPU_ID_re; rewrite cid_eq; auto. }
{ simpl; rewrite <- e; auto. }
{ inv inv_re; constructor; simpl.
- rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl; auto.
- rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl; auto. }
×simpl; rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_true; simpl.
rewrite e.
rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
× simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7, Hdestruct8.
rewrite e; simpl.
rewrite Hdestruct9.
rewrite <- e.
rewrite Int.repr_unsigned; auto.
-
subst.
unfold big2_palloc_spec in H3; subdestruct; inv H3; substx; simpl in *; try (omega; fail).
functional inversion H1; subst; simpl in ×.
×
functional inversion H14; subst; simpl in ×.
unfold single_big_ptResv_spec.
simpl in ×.
unfold single_big_palloc_spec; simpl in ×.
inv H; simpl.
rewrite e.
rewrite <- cid_re, <- CPU_ID_re.
rewrite zeq_true; auto; rewrite zeq_true; auto.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- _x.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; simpl in ×.
unfold B_inLock; simpl.
rewrite Hdestruct8, Hdestruct9, Hdestruct5.
unfold single_big_palloc_spec_share.
rewrite <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true.
rewrite zeq_false; auto.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite <- _x.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, H6, H12.
fold pdi pt; rewrite H13.
unfold single_ptInsertPTE0_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, H6.
fold pdi pt; rewrite H13.
rewrite <- pperm_re; rewrite H20.
assert (Htemp: pti0 = pti) by (substx; auto).
substx.
rewrite H21 in H13; inv H13; substx.
destruct (ZMap.get (PTX (Int.unsigned vadr)) pdt); try inv H23.
{ ∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 2 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; auto.
- simpl; constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re;
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11; rewrite zeq_true; rewrite zeq_false; simpl; auto; fail).
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- pg_re; auto.
+ rewrite <- _x.
rewrite ZMap.gss; auto.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- init_re; auto.
+ rewrite <- _x; auto.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- cid_eq.
rewrite <- e.
reflexivity.
+ inv inv_re; constructor; simpl.
× rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_false; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_false; auto.
- simpl; auto.
rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite _x.
rewrite <- CPU_ID_re; rewrite cid_eq; auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- _x.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; simpl in ×.
rewrite Hdestruct8; simpl.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct9.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite zeq_true.
rewrite <- _x.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; simpl in ×.
rewrite Hdestruct8; simpl.
rewrite Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct5, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; auto.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4.
rewrite <- _x.
rewrite H6, H12, H21.
rewrite Int.repr_unsigned.
reflexivity. }
{ ∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 2 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; auto.
- simpl; constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re;
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11; rewrite zeq_true; rewrite zeq_false; simpl; auto; fail).
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- pg_re; auto.
+ rewrite <- _x.
rewrite ZMap.gss; auto.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- init_re; auto.
+ rewrite <- _x; auto.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite <- cid_eq.
rewrite <- e.
reflexivity.
+ inv inv_re; constructor; simpl.
× rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_false; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_false; auto.
- simpl; auto.
rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; simpl; auto.
rewrite _x.
rewrite <- CPU_ID_re; rewrite cid_eq; auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- _x.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; simpl in ×.
rewrite Hdestruct8; simpl.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct9.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite zeq_true.
rewrite <- _x.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; simpl in ×.
rewrite Hdestruct8; simpl.
rewrite Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct0, Hdestruct3, Hdestruct5, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, zeq_true.
rewrite zeq_false; auto.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4.
rewrite <- _x.
rewrite H6, H12, H21.
rewrite Int.repr_unsigned.
reflexivity. }
×
functional inversion H14; subst; simpl in *; try omega.
unfold big2_palloc_spec in H23; subdestruct; inv H23; substx; simpl in *; try omega.
{
clear Hdestruct0 Hdestruct1 Hdestruct2 Hdestruct3 Hdestruct4 Hdestruct6.
clear H7 H8 H9 H10 H11 H17 H18 H19 H20 H21 H15 H24 _x1.
rewrite ZMap.gss in *; simpl in ×.
unfold single_big_ptResv_spec.
simpl in ×.
unfold single_big_palloc_spec; simpl in ×.
inv H; simpl.
rewrite _x.
rewrite <- cid_re, <- CPU_ID_re.
rewrite zeq_true; auto; rewrite zeq_true; auto.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- _x.
rewrite e.
rewrite Hdestruct14, Hdestruct15, Hdestruct8, Hdestruct9, Hdestruct17.
rewrite <- e.
simpl.
rewrite Hdestruct7, Hdestruct5.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct8, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, H4, H4.
unfold single_big_ptInsert_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite <- _x.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12, H13.
unfold single_big_ptAllocPDE_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H16.
rewrite <- ptp_re; rewrite H13.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re.
rewrite _x.
rewrite zeq_true, Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- _x.
rewrite zeq_true.
rewrite _x.
rewrite Hdestruct20.
unfold single_big_palloc_spec_share; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite _x in Hdestruct21.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct21, Hdestruct22, Hdestruct23.
rewrite zeq_true.
rewrite zeq_true.
rewrite zeq_true.
∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 4 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23.
rewrite cid_re.
rewrite CPU_ID_re.
reflexivity.
- simpl; constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl;
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl; auto; fail).
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- pg_re; auto.
× rewrite ZMap.gss.
rewrite <- cid_re; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- init_re; auto.
× rewrite pperm_re; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite cid_re, CPU_ID_re.
reflexivity.
× inv inv_re; constructor; simpl; auto.
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
- simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- big_log_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct8, Hdestruct9, Hdestruct17.
rewrite <- e.
simpl.
rewrite <- AC_re.
rewrite e in Hdestruct7.
rewrite Hdestruct7.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite e.
rewrite zeq_true.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- _x.
simpl.
unfold B_inLock; rewrite Hdestruct8, Hdestruct5.
rewrite <- _x in Hdestruct7, Hdestruct9.
rewrite Hdestruct7, Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12, H13.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- cid_re, <- CPU_ID_re.
rewrite e.
rewrite Hdestruct20.
rewrite Hdestruct21.
simpl.
rewrite <- e.
rewrite Int.repr_unsigned.
reflexivity. }
{
clear Hdestruct0 Hdestruct1 Hdestruct2 Hdestruct3 Hdestruct4 Hdestruct6.
clear H7 H8 H9 H10 H11 H17 H18 H19 H20 H21 H15 H24 _x1.
rewrite ZMap.gss in *; simpl in ×.
unfold single_big_ptResv_spec.
simpl in ×.
unfold single_big_palloc_spec; simpl in ×.
inv H; simpl.
rewrite _x.
rewrite <- cid_re, <- CPU_ID_re.
rewrite zeq_true; auto; rewrite zeq_true; auto.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- _x.
rewrite e.
rewrite Hdestruct14, Hdestruct15, Hdestruct8, Hdestruct9, Hdestruct17.
rewrite <- e.
simpl.
rewrite Hdestruct7, Hdestruct5.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct8, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, H4, H4.
unfold single_big_ptInsert_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite <- _x.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12, H13.
unfold single_big_ptAllocPDE_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H16.
rewrite <- ptp_re; rewrite H13.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re.
rewrite _x.
rewrite zeq_true, Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- _x.
rewrite zeq_true.
rewrite _x.
rewrite Hdestruct20.
unfold single_big_palloc_spec_share; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite _x in Hdestruct21.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct21.
rewrite zeq_true.
rewrite zeq_true.
∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 3 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19.
rewrite cid_re.
rewrite CPU_ID_re.
reflexivity.
- simpl; constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl;
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re;
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl; auto; fail).
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
rewrite <- pg_re; auto.
× rewrite ZMap.gss.
rewrite <- cid_re; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
rewrite <- init_re; auto.
× rewrite pperm_re; auto.
× rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
rewrite cid_re, CPU_ID_re.
reflexivity.
× inv inv_re; constructor; simpl; auto.
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
auto. }
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
auto. }
- simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19; simpl.
auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- big_log_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct8, Hdestruct9, Hdestruct17.
rewrite <- e.
simpl.
rewrite <- AC_re.
rewrite e in Hdestruct7.
rewrite Hdestruct7.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite e.
rewrite zeq_true.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- _x.
simpl.
unfold B_inLock; rewrite Hdestruct8, Hdestruct5.
rewrite <- _x in Hdestruct7, Hdestruct9.
rewrite Hdestruct7, Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12, H13.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- cid_re, <- CPU_ID_re.
rewrite e.
rewrite Hdestruct20.
rewrite Hdestruct21.
simpl.
rewrite <- e.
rewrite Int.repr_unsigned.
reflexivity. }
×
functional inversion H14; subst; simpl in *; try omega.
unfold big2_palloc_spec in H24; subdestruct; inv H24; substx; simpl in *; try omega.
functional inversion H16; subst; simpl in *; try omega.
rewrite ZMap.gss in *; rewrite ZMap.set2 in ×.
unfold single_big_ptResv_spec.
simpl in ×.
clear Hdestruct0 Hdestruct1 Hdestruct2 Hdestruct3 Hdestruct4 Hdestruct6.
clear H7 H8 H9 H10 H11 H18 H19 H20 H21 H22 H15 H2 _x _x1.
unfold single_big_palloc_spec; simpl in ×.
inv H; simpl.
rewrite e.
rewrite <- cid_re, <- CPU_ID_re.
rewrite zeq_true; auto; rewrite zeq_true; auto.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- e.
rewrite e.
rewrite Hdestruct14, Hdestruct15, Hdestruct8, Hdestruct9, Hdestruct17.
rewrite <- e.
simpl.
rewrite Hdestruct7, Hdestruct5.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct8, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, H4, H4.
unfold single_big_ptInsert_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite <- e.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12, H13.
unfold single_big_ptAllocPDE_spec; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H17.
rewrite <- ptp_re; rewrite H13.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re.
rewrite e.
rewrite zeq_true, Hdestruct14, Hdestruct15, Hdestruct17.
rewrite <- e.
rewrite zeq_true.
rewrite e.
rewrite Hdestruct20.
unfold single_big_palloc_spec_share; simpl.
rewrite <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite e in Hdestruct21.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct21, Hdestruct22, Hdestruct23.
rewrite zeq_false; auto.
rewrite zeq_false; try assumption.
rewrite zeq_false; try assumption.
unfold single_ptInsertPTE0_spec; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- ipt_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17.
rewrite e in H6.
rewrite H6.
rewrite ZMap.gss.
rewrite ZMap.gss.
rewrite <- pperm_re.
rewrite ZMap.set2.
fold pti.
unfold pt, pdi, pti, pdt´, pt´ in *; auto; substx.
rewrite e in H30.
rewrite H30.
rewrite ZMap.gss in ×.
rewrite ZMap.gss in H31.
inv H31.
destruct (ZMap.get (PTX (Int.unsigned vadr)) CalRealInitPTE.real_init_PTE); try inv H33.
{ ∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 4 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23.
rewrite cid_re.
rewrite CPU_ID_re.
reflexivity.
- repeat rewrite ZMap.set2.
repeat rewrite ZMap.gss.
set (pgval:= (PGHide (PGPMap (ZMap.get (AbstractDataType.CPU_ID a)(AbstractDataType.cid a)) (PDX (Int.unsigned vadr))))).
set (ac_val := (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a)) (AbstractDataType.AC a))).
constructor; simpl; try assumption;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto;
simpl;
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl; auto; fail).
+ rewrite flatmem_re; reflexivity.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- pg_re; auto.
+ rewrite <- e; rewrite ZMap.gss; unfold ac_val.
rewrite cid_re.
reflexivity.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- init_re; auto.
+ rewrite <- cid_re.
fold pgval.
reflexivity.
+ rewrite <- ptp_re.
rewrite <- cid_re.
auto.
rewrite e.
auto.
+ reflexivity.
+ inv inv_re; constructor; simpl; auto.
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
- simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- e.
rewrite Hdestruct14, Hdestruct15, Hdestruct17, Hdestruct8.
rewrite e; simpl in ×.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct9.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite zeq_true.
rewrite <- e.
rewrite Hdestruct14, Hdestruct15, Hdestruct17, Hdestruct8.
rewrite e; simpl in ×.
rewrite Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false;
auto.
rewrite e in Hdestruct7; rewrite Hdestruct7.
rewrite Hdestruct5.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12;
rewrite e in H13; rewrite H13.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite CPU_ID_re.
rewrite <- cid_re, <- CPU_ID_re.
rewrite Hdestruct20.
rewrite Hdestruct21.
simpl.
rewrite <- e.
rewrite Int.repr_unsigned.
reflexivity. }
{ ∃ ((LEvent (proc_id (uRData l)) (LogPrim pt_resv (Lint (Int.repr (proc_id (uRData l)))::Lint vadr::Lint perm::nil) 4 (snap_func pd))::l)).
refine_split´; eauto.
- simpl; rewrite prim_num.
unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23.
rewrite cid_re.
rewrite CPU_ID_re.
reflexivity.
- repeat rewrite ZMap.set2.
repeat rewrite ZMap.gss.
set (pgval:= (PGHide (PGPMap (ZMap.get (AbstractDataType.CPU_ID a)(AbstractDataType.cid a)) (PDX (Int.unsigned vadr))))).
set (ac_val := (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a)) (AbstractDataType.AC a))).
constructor; simpl; try assumption;
try (rewrite prim_num; unfold single_big_palloc_spec_share;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto;
simpl;
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re;
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl; auto; fail).
+ rewrite flatmem_re; reflexivity.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- pg_re; auto.
+ rewrite <- e; rewrite ZMap.gss; unfold ac_val.
rewrite cid_re.
reflexivity.
+ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
rewrite <- init_re; auto.
+ rewrite <- cid_re.
fold pgval.
reflexivity.
+ rewrite <- ptp_re.
rewrite <- cid_re.
auto.
rewrite e.
auto.
+ reflexivity.
+ inv inv_re; constructor; simpl; auto.
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
{ rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto. }
- simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false; auto.
simpl.
rewrite <- cid_re, <- pg_re, <- lock_re, <- big_oracle_re, <- CPU_ID_re, <- nps_re, <- init_re.
rewrite Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct22, Hdestruct23; simpl.
auto.
- simpl; unfold choice_check; rewrite prim_num.
unfold single_big_ptResv_spec_test; simpl.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite <- e.
rewrite Hdestruct14, Hdestruct15, Hdestruct17, Hdestruct8.
rewrite e; simpl in ×.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct9.
unfold single_big_palloc_spec; simpl.
rewrite <- cid_re, <- CPU_ID_re, <- ikern_re, <- ihost_re, <- ipt_re, <- AC_re, <- big_log_re.
rewrite zeq_true.
rewrite <- e.
rewrite Hdestruct14, Hdestruct15, Hdestruct17, Hdestruct8.
rewrite e; simpl in ×.
rewrite Hdestruct9.
unfold single_big_palloc_spec_share.
rewrite <-pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <-big_oracle_re, <-nps_re, <-init_re.
rewrite Hdestruct8, Hdestruct13, Hdestruct16, Hdestruct19, Hdestruct10, Hdestruct11, zeq_true, zeq_false;
auto.
rewrite e in Hdestruct7; rewrite Hdestruct7.
rewrite Hdestruct5.
rewrite zeq_false; auto.
unfold single_big_ptInsert_spec_test; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- nps_re, <- ptp_re, <- init_re.
rewrite Hdestruct13, Hdestruct14, Hdestruct15, Hdestruct16, Hdestruct17, H6, H12;
rewrite e in H13; rewrite H13.
unfold single_big_palloc_spec_test; simpl.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite Hdestruct14, Hdestruct15, Hdestruct17.
rewrite CPU_ID_re.
rewrite <- cid_re, <- CPU_ID_re.
rewrite Hdestruct20.
rewrite Hdestruct21.
simpl.
rewrite <- e.
rewrite Int.repr_unsigned.
reflexivity. }
Qed.
End PHTHREAD2TGENLEMMAPTRESVFILE.