adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

infoflow: 2015 update for infoflow C refinement

This commit is contained in:
Gerwin Klein 2015-05-20 21:10:59 +10:00
parent d4be402559
commit c6564cb4cb
2 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
proof/infoflow/ADT_IF_Refine_C.thy
View File

@ -444,7 +444,7 @@ lemma do_user_op_if_C_corres:
(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_nonempty_def del: split_paired_All)
apply (thin_tac "?P")
apply (thin_tac "P" for P)
apply (rule corres_guard_imp)
apply (rule_tac r'="op=" and P'=\<top> and P="invs' and ex_abs (einvs)" in corres_split)
prefer 2
@ -504,7 +504,6 @@ lemma do_user_op_if_C_corres:
apply (wp | simp)+
apply (clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def ex_abs_def)
apply (thin_tac "(?a,?b) : f ?c ?d ?e ?f ?g")
apply (clarsimp simp: user_mem'_def ex_abs_def restrict_map_def invs_def
ptable_lift_s'_def
split: if_splits)

4
proof/infoflow/Noninterference_Refinement.thy
View File

@ -230,7 +230,7 @@ lemma LI_abs_to_c:
lemma ADT_C_if_Init_Fin_serial:
"Init_Fin_serial (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}"
apply (unfold_locales)
apply (subgoal_tac "ADT_C_if fp utf \<Turnstile> ?P")
apply (subgoal_tac "ADT_C_if fp utf \<Turnstile> P" for P)
prefer 2
apply (rule fw_inv_transport)
apply (rule global_automaton_invs.ADT_invs)
@ -408,4 +408,4 @@ lemma xnonleakage_C:
end
end (* a comment *)
end