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

Isabelle2016: infoflow update (partial)

This commit is contained in:
Matthew Brecknell 2016-01-28 18:02:11 +11:00
parent b287127924
commit 5228a0ec78
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/infoflow/ADT_IF.thy
View File

@ -1799,7 +1799,7 @@ lemma handle_preemption_globals_equiv[wp]: "\<lbrace>globals_equiv st and invs\<
apply (wp handle_interrupt_globals_equiv dmo_getActiveIRQ_globals_equiv crunch_wps | simp add: crunch_simps)+
done
lemmas handle_preemption_idle_equiv[wp] = idle_globals_lift[OF handle_preemption_globals_equiv invs_pd_not_idle_thread,simplified, OF TrueI]
lemmas handle_preemption_idle_equiv[wp] = idle_globals_lift[OF handle_preemption_globals_equiv invs_pd_not_idle_thread,simplified]
lemma schedule_if_globals_equiv_scheduler[wp]: "\<lbrace>globals_equiv_scheduler st and invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>"
apply (simp add: schedule_if_def)
@ -1809,7 +1809,7 @@ lemma schedule_if_globals_equiv_scheduler[wp]: "\<lbrace>globals_equiv_scheduler
apply (wp | simp)+
done
lemmas schedule_if_idle_equiv[wp] = idle_globals_lift_scheduler[OF schedule_if_globals_equiv_scheduler invs_pd_not_idle_thread,simplified, OF TrueI]
lemmas schedule_if_idle_equiv[wp] = idle_globals_lift_scheduler[OF schedule_if_globals_equiv_scheduler invs_pd_not_idle_thread,simplified]
lemma not_in_global_refs_vs_lookup:
"\<lbrakk>(\<exists>\<unrhd>p) s; valid_vs_lookup s; valid_global_refs s;

4
proof/infoflow/Noninterference_Base_Refinement.thy
View File

@ -15,8 +15,8 @@ begin
(* we assume the same initial state for both systems *)
locale noninterference_refinement =
abs: complete_unwinding_system A s0 dom uwr policy out schedDomain +
conc: noninterference_system C s0 dom uwr policy out schedDomain
abs?: complete_unwinding_system A s0 dom uwr policy out schedDomain +
conc?: noninterference_system C s0 dom uwr policy out schedDomain
for A :: "('a,'s,'e) data_type"
and s0 :: "'s"
and dom :: "'e \<Rightarrow> 's \<Rightarrow> 'd"