infoflow: weakened assumptions for c refinement of infoflow adts
The fact that the C infoflow adt refines the abstract infoflow adt now only requires that given user operation is nonempty and not sane (nonempty and doesn't return an interrupt). Also added some more general lemmas about fw_sim and refinement to lib/Simulation.thy.
This commit is contained in:
parent
6c915fa629
commit
6df2eb6cf9
|
@ -275,6 +275,9 @@ lemma L_invariantI:
|
|||
by (simp add: fw_simulates_def, rule_tac x="r \<inter> I\<^sub>a \<times> I\<^sub>c" in exI,
|
||||
simp add: LI_fw_sim)
|
||||
|
||||
lemma refinement_refl[simp]:
|
||||
"A \<sqsubseteq> A"
|
||||
by (simp add: refines_def)
|
||||
|
||||
lemma refinement_trans [trans]:
|
||||
"\<lbrakk>C \<sqsubseteq> B; B \<sqsubseteq> A\<rbrakk> \<Longrightarrow> C \<sqsubseteq> A"
|
||||
|
@ -300,5 +303,44 @@ lemma fw_inv_transport:
|
|||
apply blast
|
||||
done
|
||||
|
||||
lemma fw_sim_refl:
|
||||
"fw_sim Id A A"
|
||||
apply (simp add: fw_sim_def rel_semi_def)
|
||||
done
|
||||
|
||||
lemma fw_simulates_refl[simp]:
|
||||
"A \<sqsubseteq>\<^sub>F A"
|
||||
apply (simp add: fw_simulates_def fw_sim_refl exI[where x="Id"])
|
||||
done
|
||||
|
||||
lemma fw_sim_trans:
|
||||
"\<lbrakk>fw_sim Q C B; fw_sim R B A\<rbrakk> \<Longrightarrow> fw_sim (R O Q) C A"
|
||||
apply (clarsimp simp: fw_sim_def)
|
||||
apply (intro conjI)
|
||||
apply clarsimp
|
||||
apply (rename_tac s x)
|
||||
apply (erule_tac x="s" in allE)
|
||||
apply (drule set_mp)
|
||||
apply assumption
|
||||
apply clarsimp
|
||||
apply (erule_tac x="s" in allE)
|
||||
apply (drule set_mp)
|
||||
apply assumption
|
||||
apply blast
|
||||
apply (clarsimp simp: rel_semi_def)
|
||||
apply (rename_tac j z' x y z)
|
||||
apply (erule_tac x="j" in allE)+
|
||||
apply (drule_tac x="(y, z')" in set_mp)
|
||||
apply blast
|
||||
apply clarsimp
|
||||
apply (rename_tac j x z x' y' z')
|
||||
apply (drule_tac x="(x, y')" in set_mp)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma fw_simulates_trans:
|
||||
"\<lbrakk>C \<sqsubseteq>\<^sub>F B; B \<sqsubseteq>\<^sub>F A\<rbrakk> \<Longrightarrow> C \<sqsubseteq>\<^sub>F A"
|
||||
apply (auto simp: fw_simulates_def dest: fw_sim_trans)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
|
@ -3739,4 +3739,20 @@ lemma refines_refines':
|
|||
apply(auto simp: refines_def refines'_def)
|
||||
done
|
||||
|
||||
text {* Two validity requires on the user operation (uop) of the infoflow adt.
|
||||
These definitions are mostly only needed in ADT_A_if_Refine. *}
|
||||
|
||||
text {* uop_nonempty is required to prove corres between do_user_op_if and doUserOp_if *}
|
||||
definition
|
||||
uop_nonempty :: "user_transition_if \<Rightarrow> bool"
|
||||
where
|
||||
"uop_nonempty uop \<equiv> \<forall>t pl pr pxn tc um es. uop t pl pr pxn (tc, um, es) \<noteq> {}"
|
||||
|
||||
text {* uop_sane is required to prove that the infoflow adt describes an enabled system *}
|
||||
definition
|
||||
uop_sane :: "user_transition_if \<Rightarrow> bool"
|
||||
where
|
||||
"uop_sane f \<equiv> \<forall>t pl pr pxn tcu. (f t pl pr pxn tcu) \<noteq> {} \<and>
|
||||
(\<forall>tc um es. (Some Interrupt, tc, um, es) \<notin> (f t pl pr pxn tcu))"
|
||||
|
||||
end (* a comment *)
|
||||
|
|
|
@ -1031,11 +1031,7 @@ definition ADT_H_if where
|
|||
kernelCall_H_if handlePreemption_H_if
|
||||
schedule'_H_if kernelExit_H_if)\<rparr>"
|
||||
|
||||
definition uop_sane where
|
||||
"uop_sane f \<equiv> \<forall>t pl pr pxn tcu. (f t pl pr pxn tcu) \<noteq> {} \<and>
|
||||
(\<forall>tc um es. (Some Interrupt,tc,um, es) \<notin> (f t pl pr pxn tcu))"
|
||||
|
||||
lemma haskell_invs: "uop_sane uop \<Longrightarrow> global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop)
|
||||
lemma haskell_invs: "global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop)
|
||||
kernelCall_H_if handlePreemption_H_if
|
||||
schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV"
|
||||
apply (unfold_locales)
|
||||
|
@ -1044,11 +1040,11 @@ lemma haskell_invs: "uop_sane uop \<Longrightarrow> global_automaton_invs checkA
|
|||
apply (simp_all add: checkActiveIRQ_H_if_def doUserOp_H_if_def
|
||||
kernelCall_H_if_def handlePreemption_H_if_def
|
||||
schedule'_H_if_def kernelExit_H_if_def split del: split_if)[12]
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def uop_sane_def)+
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def)+
|
||||
apply (wp_once hoare_disjI1)
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def uop_sane_def)+
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def)+
|
||||
apply (wp_once hoare_disjI2)
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def uop_sane_def)+
|
||||
apply (rule preserves_lifts | wp | simp add: full_invs_if'_def)+
|
||||
apply (rule hoare_pre)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule hoare_drop_imps)
|
||||
|
@ -1171,14 +1167,17 @@ lemma extras_inter'[dest!]: "(t,mode) \<in> has_srel_state (lift_fst_rel srel) i
|
|||
apply (fastforce intro!: srel_Fin simp: lift_fst_rel_def)
|
||||
done
|
||||
|
||||
lemma refinement: "ADT_conc \<sqsubseteq> ADT_abs"
|
||||
apply (rule sim_imp_refines)
|
||||
lemma fw_simulates: "ADT_conc \<sqsubseteq>\<^sub>F ADT_abs"
|
||||
apply (rule L_invariantI)
|
||||
apply (rule abs.ADT_invs)
|
||||
apply (rule conc.ADT_invs)
|
||||
apply (rule fw_sim_abs_conc)
|
||||
done
|
||||
|
||||
lemma refinement: "ADT_conc \<sqsubseteq> ADT_abs"
|
||||
apply (rule sim_imp_refines[OF fw_simulates])
|
||||
done
|
||||
|
||||
lemma conc_serial:
|
||||
assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow>
|
||||
e \<noteq> Some Interrupt"
|
||||
|
@ -1399,7 +1398,7 @@ lemma ct_idle'_related: "\<lbrakk>(a, c) \<in> state_relation; invs' c; ct_idle
|
|||
apply (case_tac st, simp_all)[1]
|
||||
done
|
||||
|
||||
lemma haskell_to_abs: "uop_sane uop \<Longrightarrow> global_automata_refine
|
||||
lemma haskell_to_abs: "uop_nonempty uop \<Longrightarrow> global_automata_refine
|
||||
check_active_irq_A_if (do_user_op_A_if uop)
|
||||
kernel_call_A_if kernel_handle_preemption_if
|
||||
kernel_schedule_if kernel_exit_A_if
|
||||
|
@ -1411,7 +1410,7 @@ lemma haskell_to_abs: "uop_sane uop \<Longrightarrow> global_automata_refine
|
|||
apply (simp add: global_automata_refine_def)
|
||||
apply (intro conjI)
|
||||
apply (rule abstract_invs)
|
||||
apply (erule haskell_invs)
|
||||
apply (rule haskell_invs)
|
||||
apply (unfold_locales)
|
||||
apply (simp add: step_restrict_def)
|
||||
apply (simp add: ADT_H_if_def ADT_A_if_def)
|
||||
|
@ -1443,8 +1442,8 @@ lemma haskell_to_abs: "uop_sane uop \<Longrightarrow> global_automata_refine
|
|||
apply (rule step_corres_lifts)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule do_user_op_if_corres)
|
||||
apply (fastforce simp: full_invs_if_def uop_sane_def)
|
||||
apply (simp add: full_invs_if'_def uop_sane_def)
|
||||
apply (fastforce simp: full_invs_if_def uop_nonempty_def)
|
||||
apply (simp add: full_invs_if'_def uop_nonempty_def)
|
||||
apply (rule doUserOp_if_empty_fail)
|
||||
apply (simp add: kernelCall_H_if_def kernel_call_A_if_def)
|
||||
apply (rule step_corres_lifts)
|
||||
|
@ -1490,13 +1489,12 @@ lemma doUserOp_if_no_interrupt: "\<lbrace>K(uop_sane uop)\<rbrace> doUserOp_if u
|
|||
apply (clarsimp simp: uop_sane_def simp del: split_paired_All)
|
||||
done
|
||||
|
||||
|
||||
lemma ADT_A_if_Init_Fin_serial: "uop_sane uop \<Longrightarrow>
|
||||
Init_Fin_serial (ADT_A_if uop) s0 (full_invs_if \<inter> {s. step_restrict s})"
|
||||
apply (simp add: Init_Fin_serial_def)
|
||||
apply (rule conjI)
|
||||
apply (rule global_automata_refine.abs_serial[OF haskell_to_abs])
|
||||
apply simp
|
||||
apply (simp add: uop_sane_def uop_nonempty_def)
|
||||
apply (fastforce simp: step_restrict_def has_srel_state_def)
|
||||
apply (clarsimp simp add: doUserOp_H_if_def)
|
||||
apply (frule use_valid[OF _ doUserOp_if_no_interrupt])
|
||||
|
@ -1505,7 +1503,6 @@ lemma ADT_A_if_Init_Fin_serial: "uop_sane uop \<Longrightarrow>
|
|||
apply (clarsimp simp: ADT_A_if_def)+
|
||||
done
|
||||
|
||||
|
||||
lemma ADT_A_if_enabled:
|
||||
"uop_sane uop \<Longrightarrow> enabled_system (ADT_A_if uop) s0"
|
||||
apply (rule Init_Fin_serial.enabled)
|
||||
|
@ -1513,12 +1510,14 @@ lemma ADT_A_if_enabled:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma (in valid_initial_state_noenabled) uop_nonempty:
|
||||
"uop_nonempty utf"
|
||||
apply (simp add: uop_nonempty_def utf_non_empty)
|
||||
done
|
||||
|
||||
lemma (in valid_initial_state_noenabled) uop_sane:
|
||||
"uop_sane utf"
|
||||
apply (simp add: uop_sane_def)
|
||||
apply (intro allI conjI)
|
||||
apply (cut_tac utf_non_empty)
|
||||
apply blast
|
||||
apply (simp add: uop_sane_def utf_non_empty)
|
||||
apply (cut_tac utf_non_interrupt)
|
||||
apply blast
|
||||
done
|
||||
|
|
|
@ -434,10 +434,10 @@ lemma dmo_getExMonitor_C_wp[wp]:
|
|||
|
||||
lemma do_user_op_if_C_corres:
|
||||
"corres_underlying rf_sr True op =
|
||||
(invs' and ex_abs einvs and (\<lambda>_. uop_sane f)) \<top>
|
||||
(invs' and ex_abs einvs and (\<lambda>_. uop_nonempty f)) \<top>
|
||||
(doUserOp_if f tc) (doUserOp_C_if f tc)"
|
||||
apply (rule corres_gen_asm)
|
||||
apply (simp add: doUserOp_if_def doUserOp_C_if_def uop_sane_def del: split_paired_All)
|
||||
apply (simp add: doUserOp_if_def doUserOp_C_if_def uop_nonempty_def del: split_paired_All)
|
||||
apply (thin_tac "?P")
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule_tac r'="op=" and P'=\<top> and P="invs' and ex_abs (einvs)" in corres_split)
|
||||
|
@ -730,13 +730,13 @@ lemma full_invs_all_invs[simp]: "((tc,s),KernelEntry e) \<in> full_invs_if' \<Lo
|
|||
apply (fastforce simp: ct_running_related schedaction_related)
|
||||
done
|
||||
|
||||
lemma c_to_haskell: "uop_sane uop \<Longrightarrow> global_automata_refine checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if
|
||||
lemma c_to_haskell: "uop_nonempty uop \<Longrightarrow> global_automata_refine checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if
|
||||
handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV
|
||||
check_active_irq_C_if (do_user_op_C_if uop) (kernel_call_C_if fp) handle_preemption_C_if schedule_C_if
|
||||
kernel_exit_C_if UNIV (ADT_C_if fp uop) (lift_snd_rel rf_sr) False"
|
||||
apply (simp add: global_automata_refine_def)
|
||||
apply (intro conjI)
|
||||
apply (erule haskell_invs)
|
||||
apply (rule haskell_invs)
|
||||
apply (unfold_locales)
|
||||
apply (simp add: ADT_C_if_def)
|
||||
apply blast
|
||||
|
@ -783,17 +783,25 @@ lemma c_to_haskell: "uop_sane uop \<Longrightarrow> global_automata_refine check
|
|||
apply (clarsimp simp: full_invs_if'_def)
|
||||
done
|
||||
|
||||
theorem infoflow_refinement_H: "uop_sane uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_H_if uop"
|
||||
apply (erule global_automata_refine.refinement[OF c_to_haskell])
|
||||
(*fw_sim lemmas as theorems and refinement as corollaries with sim_imp_refines?*)
|
||||
lemma infoflow_fw_sim_H: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_H_if uop"
|
||||
apply (erule global_automata_refine.fw_simulates[OF c_to_haskell])
|
||||
done
|
||||
|
||||
theorem infoflow_refinement_A: "uop_sane uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_A_if uop"
|
||||
apply (rule refinement_trans)
|
||||
apply (rule infoflow_refinement_H)
|
||||
lemma infoflow_fw_sim_A: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_A_if uop"
|
||||
apply (rule fw_simulates_trans)
|
||||
apply (rule infoflow_fw_sim_H)
|
||||
apply simp+
|
||||
apply (erule global_automata_refine.refinement[OF haskell_to_abs])
|
||||
apply (erule global_automata_refine.fw_simulates[OF haskell_to_abs])
|
||||
done
|
||||
|
||||
theorem infoflow_refinement_H: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_H_if uop"
|
||||
apply (erule sim_imp_refines[OF infoflow_fw_sim_H])
|
||||
done
|
||||
|
||||
theorem infoflow_refinement_A: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_A_if uop"
|
||||
apply (erule sim_imp_refines[OF infoflow_fw_sim_A])
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
|
|
|
@ -50,22 +50,16 @@ context kernel_m begin
|
|||
definition big_step_ADT_C_if where
|
||||
"big_step_ADT_C_if utf \<equiv> big_step_adt (ADT_C_if fp utf) (internal_R (ADT_C_if fp utf) big_step_R) big_step_evmap"
|
||||
|
||||
(*Note: Might be able to generalise big_step_adt_refines for fw_sim*)
|
||||
lemma big_step_ADT_C_if_big_step_ADT_A_if_refines:
|
||||
"uop_sane utf \<Longrightarrow> refines (big_step_ADT_C_if utf) (big_step_ADT_A_if utf) "
|
||||
"uop_nonempty utf \<Longrightarrow> refines (big_step_ADT_C_if utf) (big_step_ADT_A_if utf) "
|
||||
apply (simp add: big_step_ADT_A_if_def big_step_ADT_C_if_def)
|
||||
apply (rule big_step_adt_refines[where A="ADT_A_if utf", simplified internal_R_ADT_A_if])
|
||||
apply (rule LI_trans)
|
||||
apply (rule global_automata_refine.fw_sim_abs_conc)
|
||||
apply (rule haskell_to_abs)
|
||||
apply simp
|
||||
apply (rule global_automata_refine.fw_sim_abs_conc)
|
||||
apply (rule c_to_haskell)
|
||||
apply simp
|
||||
apply (rule global_automaton_invs.ADT_invs)
|
||||
apply (rule haskell_invs)
|
||||
apply simp
|
||||
apply (rule global_automaton_invs.ADT_invs)
|
||||
apply (rule abstract_invs)
|
||||
apply (erule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs])
|
||||
apply (erule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell])
|
||||
apply (rule global_automaton_invs.ADT_invs[OF haskell_invs])
|
||||
apply (rule global_automaton_invs.ADT_invs[OF abstract_invs])
|
||||
apply simp
|
||||
done
|
||||
|
||||
|
@ -227,11 +221,10 @@ lemma LI_abs_to_c:
|
|||
(full_invs_if \<times> UNIV)"
|
||||
apply (rule LI_trans)
|
||||
apply (rule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs])
|
||||
apply (rule uop_sane)
|
||||
apply (rule uop_nonempty)
|
||||
apply (rule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell])
|
||||
apply (rule uop_sane)
|
||||
apply (rule uop_nonempty)
|
||||
apply (rule global_automaton_invs.ADT_invs[OF haskell_invs])
|
||||
apply (rule uop_sane)
|
||||
done
|
||||
|
||||
lemma ADT_C_if_Init_Fin_serial:
|
||||
|
@ -242,11 +235,10 @@ lemma ADT_C_if_Init_Fin_serial:
|
|||
apply (rule fw_inv_transport)
|
||||
apply (rule global_automaton_invs.ADT_invs)
|
||||
apply (rule haskell_invs)
|
||||
apply (rule uop_sane)
|
||||
apply (rule invariant_T)
|
||||
apply (rule global_automata_refine.fw_sim_abs_conc)
|
||||
apply (rule c_to_haskell)
|
||||
apply (rule uop_sane)
|
||||
apply (rule uop_nonempty)
|
||||
apply simp
|
||||
apply (rule ADT_C_if_serial[rule_format])
|
||||
apply simp
|
||||
|
@ -320,9 +312,9 @@ lemma ADT_C_if_Init_transport:
|
|||
(\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and>
|
||||
invs_if as)}"
|
||||
apply clarsimp
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_sane]]])
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]])
|
||||
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_sane]]])
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]])
|
||||
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
||||
apply (rule_tac x=bb in exI)
|
||||
apply simp
|
||||
|
@ -356,9 +348,9 @@ lemma ADT_C_if_big_step_R_terminate:
|
|||
apply assumption
|
||||
apply simp
|
||||
apply (clarsimp simp: invs_if_full_invs_if extras_s0)
|
||||
apply (drule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_sane]]])
|
||||
apply (drule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]])
|
||||
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_sane]]])
|
||||
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]])
|
||||
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
||||
apply (rule_tac x="((aa, bc), bd)" in bexI)
|
||||
apply (rule_tac b="((aa, bb), bd)" in relcompI)
|
||||
|
@ -403,7 +395,7 @@ sublocale valid_initial_state_C \<subseteq>
|
|||
apply(insert big_step_ADT_C_if_enabled_system)[1]
|
||||
apply(fastforce simp: enabled_system_def)
|
||||
apply(rule big_step_ADT_C_if_big_step_ADT_A_if_refines)
|
||||
apply (rule uop_sane)
|
||||
apply (rule uop_nonempty)
|
||||
done
|
||||
|
||||
context valid_initial_state_C begin
|
||||
|
|
Loading…
Reference in New Issue