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

abstract Haskell init parameters into constants

This commit is contained in:
Gerwin Klein 2014-11-05 15:29:00 +11:00
parent 35f237f266
commit dfa9c09892
6 changed files with 36 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/Init_C.thy
View File

@ -19,6 +19,6 @@ text {*
*}
axiomatization where init_refinement_C:
"Init_C s \<subseteq> lift_state_relation rf_sr `` Init_H a b c d e f"
"Init_C s \<subseteq> lift_state_relation rf_sr `` Init_H"
end

12
proof/crefine/Refine_C.thy
View File

@ -684,7 +684,7 @@ lemma ct_running'_C:
done
lemma full_invs_both:
"ADT_H a b c d e f uop \<Turnstile>
"ADT_H uop \<Turnstile>
{s'. \<exists>s. (s,s') \<in> lift_state_relation state_relation \<and>
s \<in> full_invs \<and> s' \<in> full_invs'}"
apply (rule fw_inv_transport)
@ -862,7 +862,7 @@ lemma check_active_irq_corres_C:
lemma refinement2_both:
"\<lparr> Init = Init_C, Fin = Fin_C,
Step = (\<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)) \<rparr>
\<sqsubseteq> ADT_H a b c d e f uop"
\<sqsubseteq> ADT_H uop"
apply (rule sim_imp_refines)
apply (rule L_invariantI [where I\<^sub>c=UNIV and r="lift_state_relation rf_sr"])
apply (rule full_invs_both)
@ -917,12 +917,12 @@ lemma refinement2_both:
done
theorem refinement2:
"ADT_C uop \<sqsubseteq> ADT_H a b c d e f uop"
"ADT_C uop \<sqsubseteq> ADT_H uop"
unfolding ADT_C_def
by (rule refinement2_both)
theorem fp_refinement:
"ADT_FP_C uop \<sqsubseteq> ADT_H a b c d e f uop"
"ADT_FP_C uop \<sqsubseteq> ADT_H uop"
unfolding ADT_FP_C_def
by (rule refinement2_both)
@ -1030,7 +1030,7 @@ lemma kernel_all_subset_kernel:
theorem true_refinement:
"kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop
\<sqsubseteq> ADT_H a b c d e f uop"
\<sqsubseteq> ADT_H uop"
apply (rule refinement_trans[OF _ refinement2])
apply (simp add: kernel_global.ADT_C_def ADT_C_def)
apply (rule sim_imp_refines)
@ -1042,7 +1042,7 @@ theorem true_refinement:
theorem true_fp_refinement:
"kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop
\<sqsubseteq> ADT_H a b c d e f uop"
\<sqsubseteq> ADT_H uop"
apply (rule refinement_trans[OF _ fp_refinement])
apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def)
apply (rule sim_imp_refines)

8
proof/crefine/Refine_nondet_C.thy
View File

@ -44,8 +44,8 @@ where
lemma refinement2_both_nondet:
"\<lparr> Init = Init_C', Fin = Fin_CN,
Step = global_automaton do_user_op_C (kernel_call_C fp) \<rparr>
\<sqsubseteq> ADT_H' a b c d e f"
apply (cut_tac a=a and b=b and c=c and d=d and e=e and f=f in refinement2_both)
\<sqsubseteq> ADT_H'"
apply (cut_tac refinement2_both)
apply (clarsimp simp add: refines_def execution_def ADT_H'_def ADT_H_def)
apply (clarsimp simp add: Fin_CN_def cstate_to_AN_def Fin_C_def cstate_to_A_def Init_C_def)
apply (rename_tac js aa ba aaa baa ad bd ae be)
@ -59,12 +59,12 @@ lemma refinement2_both_nondet:
done
theorem refinement2_nondet:
"ADT_C' \<sqsubseteq> ADT_H' a b c d e f"
"ADT_C' \<sqsubseteq> ADT_H'"
unfolding ADT_C'_def
by (rule refinement2_both_nondet)
theorem fp_refinement_nondet:
"ADT_FP_C' \<sqsubseteq> ADT_H' a b c d e f"
"ADT_FP_C' \<sqsubseteq> ADT_H'"
unfolding ADT_FP_C'_def
by (rule refinement2_both_nondet)

26
proof/refine/ADT_H.thy
View File

@ -24,19 +24,27 @@ text {*
to base the refinement's observable state on the abstract state.
*}
consts
initEntry :: word32
initFrames :: "word32 list"
initOffset :: word32
initKernelFrames :: "word32 list"
initBootFrames :: "word32 list"
initDataStart :: word32
text {*
The construction of the abstract data type
for the executable specification largely follows
the one for the abstract specification.
*}
definition
Init_H :: "word32 \<Rightarrow> word32 list \<Rightarrow> word32 \<Rightarrow> word32 list \<Rightarrow> asid list \<Rightarrow> word32 \<Rightarrow> kernel_state global_state set"
Init_H :: "kernel_state global_state set"
where
"Init_H entry initFrames initOffset kernelFrames bootFrames data_start \<equiv>
"Init_H \<equiv>
({empty_context} \<times> snd `
fst (initKernel (VPtr entry) (map PPtr initFrames) (PPtr initOffset)
(map PPtr kernelFrames) bootFrames
(newKernelState data_start))) \<times>
fst (initKernel (VPtr initEntry) (map PPtr initFrames) (PPtr initOffset)
(map PPtr initKernelFrames) initBootFrames
(newKernelState initDataStart))) \<times>
{UserMode} \<times> {None}"
definition
@ -1929,14 +1937,12 @@ definition
m = (if ct_running' (snd s') then UserMode else IdleMode)}"
definition
ADT_H :: "word32 \<Rightarrow> word32 list \<Rightarrow> word32 \<Rightarrow> word32 list \<Rightarrow> asid list \<Rightarrow> asid \<Rightarrow>
user_transition \<Rightarrow>
ADT_H :: "user_transition \<Rightarrow>
(kernel_state global_state, det_ext observable, unit) data_type"
where
"ADT_H entry initFrames initOffset kernelFrames bootFrames data_start uop \<equiv>
\<lparr>Init = \<lambda>s. Init_H entry initFrames initOffset kernelFrames bootFrames
data_start,
"ADT_H uop \<equiv>
\<lparr>Init = \<lambda>s. Init_H,
Fin = \<lambda>((tc,s),m,e). ((tc, absKState s),m,e),
Step = (\<lambda>u. global_automaton check_active_irq_H (do_user_op_H uop) kernel_call_H)\<rparr>"

10
proof/refine/KernelInit_R.thy
View File

@ -20,22 +20,22 @@ begin
(* Axiomatisation of the rest of the initialisation code *)
axiomatization where
init_refinement:
"Init_H a b c d e f \<subseteq> lift_state_relation state_relation `` Init_A"
"Init_H \<subseteq> lift_state_relation state_relation `` Init_A"
axiomatization where
ckernel_init_valid_duplicates':
"\<forall>((tc,s),x) \<in> (Init_H a b c d e f). vs_valid_duplicates' (ksPSpace s)"
"\<forall>((tc,s),x) \<in> Init_H. vs_valid_duplicates' (ksPSpace s)"
axiomatization where
ckernel_init_invs:
"\<forall>((tc,s),x) \<in> (Init_H a b c d e f). invs' s"
"\<forall>((tc,s),x) \<in> Init_H. invs' s"
axiomatization where
ckernel_init_sch_norm:
"((tc,s),x) \<in> Init_H a b c d e f \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread"
"((tc,s),x) \<in> Init_H \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread"
axiomatization where
ckernel_init_ctr:
"((tc,s),x) \<in> Init_H a b c d e f \<Longrightarrow> ct_running' s"
"((tc,s),x) \<in> Init_H \<Longrightarrow> ct_running' s"
end

8
proof/refine/Refine.thy
View File

@ -637,7 +637,7 @@ lemma sched_act_rct_related:
by (case_tac "scheduler_action a", simp_all add: state_relation_def)
lemma ckernel_invariant:
"ADT_H a b c d e f uop \<Turnstile> full_invs'"
"ADT_H uop \<Turnstile> full_invs'"
unfolding full_invs'_def
apply (rule invariantI)
apply (clarsimp simp add: ADT_H_def)
@ -650,7 +650,7 @@ lemma ckernel_invariant:
apply (frule akernel_init_invs[THEN bspec])
apply (rule_tac x = s in exI)
apply (clarsimp simp: Init_A_def)
apply (insert ckernel_init_invs[of a b c d e f])[1]
apply (insert ckernel_init_invs)[1]
apply clarsimp
apply (frule ckernel_init_sch_norm)
apply (frule ckernel_init_ctr)
@ -726,7 +726,7 @@ text {* The top-level theorem *}
lemma fw_sim_A_H:
"LI (ADT_A uop)
(ADT_H a b c d e f uop)
(ADT_H uop)
(lift_state_relation state_relation)
(full_invs \<times> full_invs')"
apply (unfold LI_def full_invs_def full_invs'_def)
@ -798,7 +798,7 @@ lemma fw_sim_A_H:
done
theorem refinement:
"ADT_H a b c d e f uop \<sqsubseteq> ADT_A uop"
"ADT_H uop \<sqsubseteq> ADT_A uop"
apply (rule sim_imp_refines)
apply (rule L_invariantI)
apply (rule akernel_invariant)