aep-binding: attempted progress on Bisim, 1 sorry remains
assumptions include aep_obj aep = IdleAEP and aep_bound_tcb aep = Some x, which I guess is probably a contradiction, but I don't know how to prove that.
This commit is contained in:
parent
8467425906
commit
1ae434b9d5
|
@ -366,7 +366,7 @@ lemma decode_invocation_bisim:
|
||||||
done
|
done
|
||||||
|
|
||||||
abbreviation
|
abbreviation
|
||||||
"separate_inv c \<equiv> \<exists>ptr badge rights. c = InvokeAsyncEndpoint ptr badge rights"
|
"separate_inv c \<equiv> \<exists>ptr badge. c = InvokeAsyncEndpoint ptr badge"
|
||||||
|
|
||||||
lemma perform_invocation_bisim:
|
lemma perform_invocation_bisim:
|
||||||
"bisim (dc \<oplus> op =) \<top> (\<top> and K (separate_inv c))
|
"bisim (dc \<oplus> op =) \<top> (\<top> and K (separate_inv c))
|
||||||
|
@ -629,7 +629,7 @@ lemma handle_wait_bisim:
|
||||||
apply (case_tac rc, simp_all)[1]
|
apply (case_tac rc, simp_all)[1]
|
||||||
apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del: hoare_True_E_R)+
|
apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del: hoare_True_E_R)+
|
||||||
apply (rule handle_fault_bisim)
|
apply (rule handle_fault_bisim)
|
||||||
apply (wp | wpc | simp)+
|
apply (wp get_aep_wp | wpc | simp)+
|
||||||
apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_post_imp_R)
|
apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_post_imp_R)
|
||||||
prefer 2
|
prefer 2
|
||||||
apply simp
|
apply simp
|
||||||
|
@ -758,12 +758,16 @@ lemma set_mrs_separate_state [wp]:
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma send_async_ipc_separate_state [wp]:
|
lemma send_async_ipc_separate_state [wp]:
|
||||||
"\<lbrace>separate_state\<rbrace> send_async_ipc a b c \<lbrace>\<lambda>_. separate_state\<rbrace>"
|
"\<lbrace>separate_state\<rbrace> send_async_ipc a b \<lbrace>\<lambda>_. separate_state\<rbrace>"
|
||||||
apply (simp add: send_async_ipc_def)
|
apply (simp add: send_async_ipc_def)
|
||||||
apply (rule separate_state_pres)
|
apply (rule separate_state_pres)
|
||||||
apply (rule hoare_pre)
|
apply (rule hoare_pre)
|
||||||
apply (wp | wpc | wps | simp add: update_waiting_aep_def do_async_transfer_def | strengthen imp_consequent)+
|
apply (wp gts_wp ipc_cancel_caps_of_state get_aep_wp
|
||||||
done
|
| wpc | wps
|
||||||
|
| simp add: update_waiting_aep_def
|
||||||
|
(*| strengthen imp_consequent*))+
|
||||||
|
apply (clarsimp)
|
||||||
|
sorry
|
||||||
|
|
||||||
lemma dmo_separate_state [wp]:
|
lemma dmo_separate_state [wp]:
|
||||||
"\<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>"
|
"\<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>"
|
||||||
|
|
|
@ -158,7 +158,13 @@ definition
|
||||||
of
|
of
|
||||||
AsyncEndpointCap ref badge rights \<Rightarrow>
|
AsyncEndpointCap ref badge rights \<Rightarrow>
|
||||||
(if AllowRecv \<in> rights
|
(if AllowRecv \<in> rights
|
||||||
then liftE $ receive_async_ipc thread ep_cap
|
then doE
|
||||||
|
aep \<leftarrow> liftE $ get_async_ep ref;
|
||||||
|
boundTCB \<leftarrow> returnOk $ aep_bound_tcb aep;
|
||||||
|
if boundTCB = Some thread \<or> boundTCB = None
|
||||||
|
then liftE $ receive_async_ipc thread ep_cap
|
||||||
|
else flt
|
||||||
|
odE
|
||||||
else flt)
|
else flt)
|
||||||
| _ \<Rightarrow> flt
|
| _ \<Rightarrow> flt
|
||||||
odE)
|
odE)
|
||||||
|
|
Loading…
Reference in New Issue