Library mcertikos.objects.BigLogThreadConfigFunctionProp
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Export GlobalOracle.
Require Import Integers.
Require Import BigStepGlobalOracle.
Require Import CalRealProcModule.
Require Import BigStepLogReplay.
Require Import AbstractDataType.
Require Import BigLogThreadConfigFunction.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import SingleOracle.
Require Import GlobalOracleProp.
Require Import RealParams.
Opaque full_thread_list.
Section BLThreadConfFuncProp.
Definition diff_owner (ev: BigOracleEvent) (cpuid : Z) :=
match ev with
| TBEVENT cpuid´ _ ⇒ cpuid´ ≠ cpuid
end.
Section THREADLINKINGMACHINES.
Require Import AuxSingleAbstractDataType.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadVMM.
Require Import ObjPHBThreadSCHED.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{threads_conf_ops : ThreadsConfigurationOps}.
Lemma single_big_oracle_query_preserves_B_inLock_aux´:
∀ l´ cpu l,
(∀ ev, In ev l´ → diff_owner ev cpu) →
B_inLock_aux cpu l = B_inLock_aux cpu (l´++ l).
Proof.
induction l´; intros.
- simpl; auto.
- assert (∀ ev : BigOracleEvent, In ev l´ → diff_owner ev cpu).
{ intros; eapply H; simpl; auto. }
assert (diff_owner a cpu).
{ eapply H; simpl; auto. }
eapply IHl´ with (cpu := cpu) (l := l) in H0.
simpl.
destruct a; simpl.
destruct e; simpl.
+ unfold diff_owner in H1.
destruct e; simpl; rewrite zeq_false; auto.
+ unfold diff_owner in H1.
destruct e; simpl; rewrite zeq_false; auto.
Qed.
Lemma single_big_oracle_query_preserves_B_inLock_aux:
∀ adt l cpuid,
valid_big_oracle (big_oracle adt) →
B_inLock_aux cpuid l = B_inLock_aux cpuid ((big_oracle adt) cpuid l ++ l).
Proof.
intros.
assert (∀ ev, In ev ((big_oracle adt) cpuid l) → diff_owner ev cpuid).
{ intros.
inv H.
clear H2.
unfold valid_big_oracle_domain in H1.
unfold diff_owner.
destruct ev.
eapply H1.
eauto. }
apply single_big_oracle_query_preserves_B_inLock_aux´; auto.
Qed.
Lemma single_big_oracle_query_preserves_cused_aux:
∀ l´ tid cpu l,
(∀ ev, In ev l´ → diff_owner ev cpu) →
B_GetContainerUsed tid cpu l = B_GetContainerUsed tid cpu (l´++ l).
Proof.
induction l´; intros.
- simpl; reflexivity.
- assert (∀ ev : BigOracleEvent, In ev l´ → diff_owner ev cpu).
{ intros; eapply H; simpl; auto. }
assert (diff_owner a cpu).
{ eapply H; simpl; auto. }
eapply IHl´ with (tid := tid) (cpu := cpu) (l := l) in H0.
unfold B_GetContainerUsed in ×.
simpl.
destruct (zeq tid (cpu + 1)); auto.
destruct (zle_le 0 tid 8); auto.
destruct a; auto.
destruct e; auto.
destruct e; auto.
unfold diff_owner in ×.
rewrite zeq_false; auto.
Qed.
Lemma single_big_oracle_query_preserves_cused:
∀ tid adt l cpuid,
valid_big_oracle (big_oracle adt) →
B_GetContainerUsed tid cpuid l = B_GetContainerUsed tid cpuid ((big_oracle adt) cpuid l ++ l).
Proof.
intros.
assert (∀ ev, In ev ((big_oracle adt) cpuid l) → diff_owner ev cpuid).
{ intros.
inv H.
clear H2.
unfold valid_big_oracle_domain in H1.
unfold diff_owner.
destruct ev.
eapply H1.
eauto. }
apply single_big_oracle_query_preserves_cused_aux; auto.
Qed.
Lemma single_big_palloc_share_preserves_cused:
∀ tid adt adt´ l l´ n choice res,
valid_big_oracle (big_oracle adt) →
single_big_palloc_spec_share n choice adt = Some (adt´, res) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetContainerUsed tid (CPU_ID adt) l = B_GetContainerUsed tid (CPU_ID adt) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID adt) l =
B_GetContainerUsed tid (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
unfold single_big_palloc_spec_share in H0; subdestruct; inv H0; subst.
- inv H1; simpl in H2; inv H2; eauto.
- inv H1; simpl in H2; inv H2; eauto.
- inv H1; simpl in H2; inv H2; eauto.
Qed.
Lemma single_big_palloc_preserves_cused:
∀ tid adt adt´ l l´ n res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_palloc_spec n adt = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed tid (CPU_ID (fst adt)) l = B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID (fst adt)) l =
B_GetContainerUsed tid (CPU_ID (fst adt)) (big_oracle (fst adt) (CPU_ID (fst adt)) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
unfold single_big_palloc_spec in H0; subdestruct.
- destruct adt; inv Hdestruct7.
inv H0; simpl in ×.
exploit single_big_palloc_share_preserves_cused; eauto.
- destruct adt; inv Hdestruct7; inv H0.
simpl in ×.
rewrite H1 in Hdestruct5; inv Hdestruct5.
exploit single_big_palloc_share_preserves_cused; eauto.
- destruct adt; inv Hdestruct7; inv H0.
simpl in ×.
rewrite H1 in Hdestruct5; inv Hdestruct5.
exploit single_big_palloc_share_preserves_cused; eauto.
Qed.
Lemma single_big_palloc_share_preserves_CPU_ID:
∀ adt adt´ n choice res,
single_big_palloc_spec_share n choice adt = Some (adt´, res) →
CPU_ID adt = CPU_ID adt´.
Proof.
intros.
unfold single_big_palloc_spec_share in H; subdestruct; inv H; subst; simpl; auto.
Qed.
Lemma single_big_palloc_share_preserves_big_oracle:
∀ adt adt´ n choice res,
single_big_palloc_spec_share n choice adt = Some (adt´, res) →
big_oracle adt = big_oracle adt´.
Proof.
intros.
unfold single_big_palloc_spec_share in H; subdestruct; inv H; subst; simpl; auto.
Qed.
Lemma single_big_palloc_preserves_CPU_ID:
∀ adt adt´ n res,
single_big_palloc_spec n adt = Some (adt´, res) →
CPU_ID (fst adt) = CPU_ID (fst adt´).
Proof.
intros.
unfold single_big_palloc_spec in H; subdestruct.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_CPU_ID.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_CPU_ID.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_CPU_ID.
Qed.
Lemma single_big_palloc_preserves_big_oracle:
∀ adt adt´ n res,
single_big_palloc_spec n adt = Some (adt´, res) →
big_oracle (fst adt) = big_oracle (fst adt´).
Proof.
intros.
unfold single_big_palloc_spec in H; subdestruct.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_big_oracle.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_big_oracle.
- inv H; destruct adt; simpl in ×.
eauto using single_big_palloc_share_preserves_big_oracle.
Qed.
Lemma single_big_ptResv_preserves_cused:
∀ tid adt adt´ l l´ n vadr perm res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_ptResv_spec n vadr perm adt = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed tid (CPU_ID (fst adt)) l = B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_ptResv_spec in H0; subdestruct.
- inv H0.
eauto using single_big_palloc_preserves_cused.
- destruct adt.
destruct adt´.
simpl in ×.
inv Hdestruct1.
destruct p0.
assert (valid_big_oracle (big_oracle d2)).
{ eapply single_big_palloc_preserves_big_oracle in Hdestruct0; simpl in ×.
rewrite Hdestruct0 in H; auto. }
assert (CPU_ID s = CPU_ID d2).
{ eapply single_big_palloc_preserves_CPU_ID in Hdestruct0; simpl in ×.
auto. }
assert (∃ l´´, big_log d2 = BigDef l´´).
{ unfold single_big_palloc_spec in Hdestruct0.
unfold single_big_palloc_spec_share in Hdestruct0.
subdestruct; inv Hdestruct0; esplit; simpl; eauto. }
destruct H5 as (l´´ & H5).
assert (B_GetContainerUsed tid (CPU_ID s) l = B_GetContainerUsed tid (CPU_ID s) l´´).
{ eapply single_big_palloc_preserves_cused in Hdestruct0; eauto. }
clear H H1 Hdestruct0 Hdestruct.
rewrite H4 in ×.
rewrite H6.
clear H6.
clear H4.
unfold single_big_ptInsert_spec in H0.
unfold single_ptInsertPTE0_spec in H0.
unfold single_big_ptAllocPDE_spec in H0.
subdestruct; inv H0; try (rewrite H5 in H2; inv H2; reflexivity).
eapply single_big_palloc_preserves_cused in Hdestruct9; [ eauto | simpl; auto | simpl; auto | simpl; auto].
eapply single_big_palloc_preserves_cused in Hdestruct9; [ eauto | simpl; auto | simpl; auto | simpl; auto].
eapply single_big_palloc_preserves_cused in Hdestruct9; [ eauto | simpl; auto | simpl; auto | simpl; auto].
Qed.
Lemma single_big_acquire_lock_SC_share_preserves_cused:
∀ tid lock_id adt adt´ l l´ sync,
valid_big_oracle (big_oracle adt) →
single_big_acquire_lock_SC_spec_share lock_id adt = Some (adt´, sync) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetContainerUsed tid (CPU_ID adt) l = B_GetContainerUsed tid (CPU_ID adt) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID adt) l =
B_GetContainerUsed tid (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
unfold single_big_acquire_lock_SC_spec_share in H0; subdestruct;
simpl in *; inv H0; inv H2; inv H1; auto.
Qed.
Lemma single_big_acquire_lock_SC_preserves_cused:
∀ tid lock_id adt adt´ l l´,
valid_big_oracle (big_oracle (fst adt)) →
single_big_acquire_lock_SC_spec lock_id adt = Some adt´ →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed tid (CPU_ID (fst adt)) l = B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_acquire_lock_SC_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
eauto using single_big_acquire_lock_SC_share_preserves_cused.
Qed.
Lemma single_big_release_lock_SC_share_preserves_cused:
∀ tid lock_id adt adt´ l l´ syncch,
valid_big_oracle (big_oracle adt) →
single_big_release_lock_SC_spec_share lock_id syncch adt = Some adt´→
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetContainerUsed tid (CPU_ID adt) l = B_GetContainerUsed tid (CPU_ID adt) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID adt) l =
B_GetContainerUsed tid (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
unfold single_big_release_lock_SC_spec_share in H0; subdestruct;
simpl in *; inv H0; inv H2; inv H1; auto.
Qed.
Lemma single_big_release_lock_SC_preserves_cused:
∀ tid lock_id adt adt´ l l´,
valid_big_oracle (big_oracle (fst adt)) →
single_big_release_lock_SC_spec lock_id adt = Some adt´ →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed tid (CPU_ID (fst adt)) l = B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_release_lock_SC_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
eauto using single_big_release_lock_SC_share_preserves_cused.
Qed.
Lemma single_big_thread_wakeup_share_preserves_cused:
∀ tid sc adt adt´ l l´ res,
valid_big_oracle (big_oracle adt) →
single_big_thread_wakeup_spec_share sc adt = Some (adt´, res) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetContainerUsed tid (CPU_ID adt) l = B_GetContainerUsed tid (CPU_ID adt) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID adt) l =
B_GetContainerUsed tid (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
intros.
unfold single_big_thread_wakeup_spec_share in H0; subdestruct.
- inv H0; inv H2; inv H1.
eauto.
- inv H0; inv H2; inv H1.
eauto.
- inv H0; inv H2; inv H1.
eauto.
Qed.
Lemma single_big_thread_wakeup_preserves_cused:
∀ tid sc adt adt´ l l´ res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_thread_wakeup_spec sc adt = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed tid (CPU_ID (fst adt)) l = B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_thread_wakeup_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
eauto using single_big_thread_wakeup_share_preserves_cused.
Qed.
Lemma single_big_proc_create_share_preserves_cused:
∀ tid adt adt´ l l´ buc ofs_uc q child_id res,
valid_big_oracle (big_oracle adt) →
single_big_proc_create_spec_share adt buc ofs_uc q child_id = Some (adt´, res) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
tid ≠ child_id →
B_GetContainerUsed tid (CPU_ID adt) l = B_GetContainerUsed tid (CPU_ID adt) l´.
Proof.
intros.
assert (B_GetContainerUsed tid (CPU_ID adt) l =
B_GetContainerUsed tid (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_cused; auto. }
intros.
unfold single_big_proc_create_spec_share in H0; subdestruct.
inv H0.
inv H2.
inv H1.
rewrite H4.
unfold B_GetContainerUsed; simpl.
destruct (zeq tid (CPU_ID adt + 1)); auto.
destruct (zle_le 0 tid 8); auto.
rewrite zeq_true.
rewrite zeq_false; auto.
Qed.
Lemma single_big_proc_create_preserves_cused:
∀ adt adt´ l l´ b b´ buc ofs_uc q res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetContainerUsed (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) (CPU_ID (fst adt)) l =
B_GetContainerUsed (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_proc_create_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
rewrite H1 in Hdestruct6; inv Hdestruct6.
assert (ZMap.get (CPU_ID s0) (cid s0) ≠
(ZMap.get (CPU_ID s0) (cid s0) × 8 + 1 +
Z.of_nat (length (cchildren (AC d))))) by omega.
eauto using single_big_proc_create_share_preserves_cused.
Qed.
Lemma single_big_proc_create_preserves_cused_snd:
∀ tid adt adt´ l l´ b b´ buc ofs_uc q res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
tid ≠ res →
B_GetContainerUsed tid (CPU_ID (fst adt)) l =
B_GetContainerUsed tid (CPU_ID (fst adt)) l´.
Proof.
intros.
unfold single_big_proc_create_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
rewrite H1 in Hdestruct6; inv Hdestruct6.
eauto using single_big_proc_create_share_preserves_cused.
Qed.
Lemma single_big_oracle_query_preserves_B_GetlastPush_aux´:
∀ l´ cpu l,
(∀ ev, In ev l´ → diff_owner ev cpu) →
B_GetlastPush_aux cpu l = B_GetlastPush_aux cpu (l´++l).
Proof.
induction l´; intros.
- simpl; reflexivity.
- assert (∀ ev : BigOracleEvent, In ev l´ → diff_owner ev cpu).
{ intros; eapply H; simpl; auto. }
assert (diff_owner a cpu).
{ eapply H; simpl; auto. }
eapply IHl´ with (cpu := cpu) (l := l) in H0.
unfold B_GetContainerUsed in ×.
simpl.
destruct a; auto.
destruct e; auto.
+ destruct e; auto.
unfold diff_owner in ×.
rewrite zeq_false; auto.
+ destruct e; auto.
unfold diff_owner in ×.
rewrite zeq_false; auto.
Qed.
Lemma single_big_oracle_query_preserves_B_GetlastPush_aux:
∀ l adt cpuid,
valid_big_oracle (big_oracle adt) →
B_GetlastPush_aux cpuid l = B_GetlastPush_aux cpuid ((big_oracle adt) cpuid l ++ l).
Proof.
intros.
inv H.
clear H1.
unfold valid_big_oracle_domain in H0.
eapply single_big_oracle_query_preserves_B_GetlastPush_aux´; eauto.
intros.
destruct ev.
eapply H0 in H.
unfold diff_owner; auto.
Qed.
Lemma single_big_palloc_share_preserves_B_GetlastPush_aux:
∀ adt adt´ l l´ n choice res,
valid_big_oracle (big_oracle adt) →
single_big_palloc_spec_share n choice adt = Some (adt´, res) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetlastPush_aux (CPU_ID adt) l = B_GetlastPush_aux (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l).
Proof.
intros.
assert (B_GetlastPush_aux (CPU_ID adt) l =
B_GetlastPush_aux (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_B_GetlastPush_aux; auto. }
unfold single_big_palloc_spec_share in H0; subdestruct; inv H0; subst.
- inv H1; simpl in H2; inv H2; eauto.
- inv H1; simpl in H2; inv H2; eauto.
- inv H1; simpl in H2; inv H2; eauto.
Qed.
Lemma single_big_palloc_preserves_B_GetlastPush_aux:
∀ adt adt´ l l´ n res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_palloc_spec n adt = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetlastPush_aux (CPU_ID (fst adt)) l = B_GetlastPush_aux (CPU_ID (fst adt))
((big_oracle (fst adt)) (CPU_ID (fst adt)) l ++ l).
Proof.
intros.
assert (B_GetlastPush_aux (CPU_ID (fst adt)) l =
B_GetlastPush_aux (CPU_ID (fst adt)) ((big_oracle (fst adt)) (CPU_ID (fst adt)) l ++ l)).
{ eapply single_big_oracle_query_preserves_B_GetlastPush_aux; auto. }
unfold single_big_palloc_spec in H0; subdestruct.
- destruct adt; inv Hdestruct7.
inv H0; simpl in ×.
exploit single_big_palloc_share_preserves_B_GetlastPush_aux; eauto.
- destruct adt; inv Hdestruct7; inv H0.
simpl in ×.
rewrite H1 in Hdestruct5; inv Hdestruct5.
exploit single_big_palloc_share_preserves_B_GetlastPush_aux; eauto.
- destruct adt; inv Hdestruct7; inv H0.
simpl in ×.
rewrite H1 in Hdestruct5; inv Hdestruct5.
exploit single_big_palloc_share_preserves_B_GetlastPush_aux; eauto.
Qed.
Lemma single_big_ptResv_preserves_B_GetlastPush_aux:
∀ adt adt´ l l´ n vadr perm res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_ptResv_spec n vadr perm adt = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetlastPush_aux (CPU_ID (fst adt)) l = B_GetlastPush_aux (CPU_ID (fst adt))
((big_oracle (fst adt)) (CPU_ID (fst adt)) l ++ l).
Proof.
intros.
unfold single_big_ptResv_spec in H0; subdestruct.
- inv H0.
eauto using single_big_palloc_preserves_B_GetlastPush_aux.
- destruct adt.
destruct adt´.
simpl in ×.
inv Hdestruct1.
destruct p0.
assert (valid_big_oracle (big_oracle d2)).
{ eapply single_big_palloc_preserves_big_oracle in Hdestruct0; simpl in ×.
rewrite Hdestruct0 in H; auto. }
assert (CPU_ID s = CPU_ID d2).
{ eapply single_big_palloc_preserves_CPU_ID in Hdestruct0; simpl in ×.
auto. }
assert (∃ l´´, big_log d2 = BigDef l´´).
{ unfold single_big_palloc_spec in Hdestruct0.
unfold single_big_palloc_spec_share in Hdestruct0.
subdestruct; inv Hdestruct0; esplit; simpl; eauto. }
destruct H5 as (l´´ & H5).
assert (B_GetlastPush_aux (CPU_ID s) l = B_GetlastPush_aux (CPU_ID s) (big_oracle s (CPU_ID s) l ++ l)).
{ eapply single_big_palloc_preserves_B_GetlastPush_aux in Hdestruct0; eauto. }
clear H H1 Hdestruct0 Hdestruct.
rewrite H4 in ×.
rewrite H6.
clear H6.
clear H4.
unfold single_big_ptInsert_spec in H0.
unfold single_ptInsertPTE0_spec in H0.
unfold single_big_ptAllocPDE_spec in H0.
subdestruct; inv H0; try (rewrite H5 in H2; inv H2; reflexivity); auto.
Qed.
Lemma single_big_proc_create_share_preserves_B_GetlastPush:
∀ adt adt´ l l´ buc ofs_uc q child_id res,
valid_big_oracle (big_oracle adt) →
single_big_proc_create_spec_share adt buc ofs_uc q child_id = Some (adt´, res) →
big_log adt = BigDef l →
big_log adt´ = BigDef l´ →
B_GetlastPush_aux (CPU_ID adt) l = B_GetlastPush_aux (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l).
Proof.
intros.
assert (B_GetlastPush_aux (CPU_ID adt) l =
B_GetlastPush_aux (CPU_ID adt) ((big_oracle adt) (CPU_ID adt) l ++ l)).
{ eapply single_big_oracle_query_preserves_B_GetlastPush_aux; auto. }
intros.
unfold single_big_proc_create_spec_share in H0; subdestruct.
inv H0.
inv H2.
inv H1.
rewrite H3.
reflexivity.
Qed.
Lemma single_big_proc_create_preserves_B_GetlastPush:
∀ adt adt´ l l´ b b´ buc ofs_uc q res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
big_log (fst adt) = BigDef l →
big_log (fst adt´) = BigDef l´ →
B_GetlastPush_aux (CPU_ID (fst adt)) l = B_GetlastPush_aux (CPU_ID (fst adt))
((big_oracle (fst adt)) (CPU_ID (fst adt)) l ++ l).
Proof.
intros.
unfold single_big_proc_create_spec in H0; subdestruct.
inv H0.
inv H2.
destruct adt; simpl in ×.
rewrite H1 in Hdestruct6; inv Hdestruct6.
eauto using single_big_proc_create_share_preserves_B_GetlastPush.
Qed.
End THREADLINKINGMACHINES.
End BLThreadConfFuncProp.