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

arch_split: CRefine: use requalify instead of shadow

This commit is contained in:
Matthew Brecknell 2016-05-06 08:59:33 +10:00
parent 9ceed1eb12
commit 56b226a608
19 changed files with 116 additions and 143 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
proof/crefine/Arch_C.thy
View File

@ -977,7 +977,7 @@ lemma cpde_relation_pde_case:
then R else S)"
by (clarsimp simp: cpde_relation_def Let_def pde_get_tag_alt
pde_tag_defs pde_pde_section_lift_def
split: Hardware_H.pde.split_asm)
split: ARM_H.pde.split_asm)
lemma pde_pde_section_size_0_1:
"pde_get_tag pde = scast pde_pde_section
@ -1098,7 +1098,7 @@ lemma createSafeMappingEntries_PDE_ccorres:
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: isPageTablePDE_def isSectionPDE_def
fst_throwError_returnOk
split: Hardware_H.pde.split)
split: ARM_H.pde.split)
apply (auto simp: exception_defs syscall_error_rel_def
syscall_error_to_H_cases)[1]
apply wp
@ -1157,7 +1157,7 @@ lemma createSafeMappingEntries_PDE_ccorres:
lemma pte_case_isLargePagePTE:
"(case pte of LargePagePTE _ _ _ _ _ \<Rightarrow> P | _ \<Rightarrow> Q)
= (if isLargePagePTE pte then P else Q)"
by (simp add: isLargePagePTE_def split: Hardware_H.pte.split)
by (simp add: isLargePagePTE_def split: ARM_H.pte.split)
lemma ccorres_pre_getObject_pte:
"(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
@ -1258,7 +1258,7 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply (clarsimp simp: typ_heap_simps cpte_relation_def Let_def)
apply (simp add: isLargePagePTE_def pte_pte_large_lift_def pte_lift_def Let_def
pte_tag_defs pte_pte_invalid_def
split: Hardware_H.pte.split_asm split_if_asm)
split: ARM_H.pte.split_asm split_if_asm)
apply ceqv
apply (simp add: pte_case_isLargePagePTE if_to_top_of_bindE del: Collect_const)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
@ -1439,7 +1439,7 @@ lemma valid_pde_slots_lift2:
done
lemma obj_at_pte_aligned:
"obj_at' (\<lambda>a::Hardware_H.pte. True) ptr s ==> is_aligned ptr 2"
"obj_at' (\<lambda>a::ARM_H.pte. True) ptr s ==> is_aligned ptr 2"
apply (drule obj_at_ko_at')
apply (clarsimp dest!:ko_at_is_aligned'
simp:objBits_simps archObjSize_def)

14
proof/crefine/Fastpath_C.thy
View File

@ -986,11 +986,11 @@ lemma pointerInUserData_h_t_valid2:
done
lemma dmo_clearExMonitor_setCurThread_swap:
"(do _ \<leftarrow> doMachineOp MachineOps.clearExMonitor;
"(do _ \<leftarrow> doMachineOp ARM.clearExMonitor;
setCurThread thread
od)
= (do _ \<leftarrow> setCurThread thread;
doMachineOp MachineOps.clearExMonitor od)"
doMachineOp ARM.clearExMonitor od)"
apply (simp add: setCurThread_def doMachineOp_def split_def)
apply (rule oblivious_modify_swap[symmetric])
apply (intro oblivious_bind,
@ -4930,7 +4930,7 @@ lemma setCurThread_isolatable:
end
crunch tcb2[wp]: "Arch.switchToThread" "tcb_at' t"
(ignore: MachineOps.clearExMonitor)
(ignore: ARM.clearExMonitor)
context kernel_m begin
@ -5339,8 +5339,8 @@ lemma fastpath_callKernel_SysCall_corres:
apply (clarsimp split: split_if)
apply (rule ext)
apply (simp add: badgeRegister_def msgInfoRegister_def
MachineTypes.badgeRegister_def
MachineTypes.msgInfoRegister_def
ARM.badgeRegister_def
ARM.msgInfoRegister_def
split: split_if)
apply simp
apply (wp | simp cong: if_cong bool.case_cong
@ -6269,8 +6269,8 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply (clarsimp split: split_if)
apply (rule ext)
apply (simp add: badgeRegister_def msgInfoRegister_def
MachineTypes.msgInfoRegister_def
MachineTypes.badgeRegister_def
ARM.msgInfoRegister_def
ARM.badgeRegister_def
split: split_if)
apply simp
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps

64
proof/crefine/Ipc_C.thy
View File

@ -403,7 +403,7 @@ lemma asUser_storeWordUser_comm:
lemma length_syscallMessage:
"length ARM_H.syscallMessage = unat n_syscallMessage"
apply (simp add: syscallMessage_def MachineTypes.syscallMessage_def
apply (simp add: syscallMessage_def ARM.syscallMessage_def
msgRegisters_unfold n_syscallMessage_def)
apply (simp add: upto_enum_def)
apply (simp add: fromEnum_def enum_register)
@ -424,7 +424,7 @@ lemma syscallMessage_ccorres:
\<Longrightarrow> register_from_H (ARM_H.syscallMessage ! n)
= index syscallMessageC n"
apply (simp add: ARM_H.syscallMessage_def syscallMessageC_def
MachineTypes.syscallMessage_def
ARM.syscallMessage_def
n_syscallMessage_def msgRegisters_unfold)
apply (simp add: upto_enum_def fromEnum_def enum_register)
apply (simp add: toEnum_def enum_register)
@ -533,7 +533,7 @@ lemma stateAssert_mapM_loadWordUser_comm:
lemmas syscallMessage_unfold
= ARM_H.syscallMessage_def
MachineTypes.syscallMessage_def
ARM.syscallMessage_def
[unfolded upto_enum_def, simplified,
unfolded fromEnum_def enum_register, simplified,
unfolded toEnum_def enum_register, simplified]
@ -559,7 +559,7 @@ lemma handleFaultReply':
apply (case_tac f)
apply (clarsimp simp: handleFaultReply_def zipWithM_x_mapM_x
zip_Cons ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def
ARM.exceptionMessage_def
mapM_x_Cons mapM_x_Nil)
apply (rule bind_apply_cong [OF refl], rename_tac sb s'')
apply (case_tac sb)
@ -570,7 +570,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
n_msgRegisters_def
dest: word_less_cases)
apply (clarsimp simp: bind_assoc asUser_bind_distrib
@ -579,7 +579,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
word_less_nat_alt ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
n_msgRegisters_def)
apply (case_tac "msgLength tag < scast n_msgRegisters")
apply (fastforce simp: asUser_bind_distrib
@ -588,7 +588,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
bind_assoc ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
bind_comm_mapM_comm [OF asUser_loadWordUser_comm]
word_size stateAssert_mapM_loadWordUser_comm
n_msgRegisters_def
@ -599,7 +599,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
bind_assoc ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
bind_comm_mapM_comm [OF asUser_loadWordUser_comm]
word_size stateAssert_mapM_loadWordUser_comm
word_less_nat_alt n_msgRegisters_def)
@ -626,7 +626,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
n_msgRegisters_def
dest: word_less_cases)
apply (clarsimp simp: bind_assoc asUser_bind_distrib
@ -635,7 +635,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
word_less_nat_alt ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def take_Cons
ARM.sanitiseRegister_def take_Cons
split: nat.split)
apply (case_tac "msgLength tag < scast n_msgRegisters")
apply (fastforce simp: asUser_bind_distrib zipWithM_x_mapM_x
@ -644,7 +644,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert asUser_return
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
bind_assoc ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
bind_comm_mapM_comm [OF asUser_loadWordUser_comm]
word_size stateAssert_mapM_loadWordUser_comm
n_msgRegisters_def
@ -664,7 +664,7 @@ lemma handleFaultReply':
submonad_asUser.fn_stateAssert
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
word_less_nat_alt ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def
ARM.sanitiseRegister_def
split_def n_msgRegisters_def msgMaxLength_def
word_size msgLengthBits_def n_syscallMessage_def
split del: split_if cong: if_weak_cong)
@ -846,7 +846,7 @@ lemma getMessageInfo_ccorres:
apply wp
apply vcg
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def MachineTypes.msgInfoRegister_def
apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def dest!: c_guard_clift)
done
@ -863,7 +863,7 @@ lemma getMessageInfo_ccorres':
apply wp
apply vcg
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def MachineTypes.msgInfoRegister_def
apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def dest!: c_guard_clift)
done
@ -885,9 +885,9 @@ lemma replyFromKernel_success_empty_ccorres [corres]:
apply wp
apply vcg
apply wp
apply (simp add: ARM_H.msgInfoRegister_def MachineTypes.msgInfoRegister_def
apply (simp add: ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def
ARM_H.badgeRegister_def MachineTypes.badgeRegister_def
ARM_H.badgeRegister_def ARM.badgeRegister_def
Kernel_C.badgeRegister_def Kernel_C.R0_def
message_info_to_H_def)
done
@ -1197,9 +1197,9 @@ lemma replyFromKernel_error_ccorres [corres]:
apply (wp lookupIPCBuffer_aligned_option_to_0)
apply (simp del: Collect_const)
apply (vcg exspec=lookupIPCBuffer_modifies)
apply (simp add: ARM_H.msgInfoRegister_def MachineTypes.msgInfoRegister_def
apply (simp add: ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def
ARM_H.badgeRegister_def MachineTypes.badgeRegister_def
ARM_H.badgeRegister_def ARM.badgeRegister_def
Kernel_C.badgeRegister_def Kernel_C.R0_def
message_info_to_H_def valid_pspace_valid_objs')
apply (clarsimp simp: msgLengthBits_def msgFromSyscallError_def
@ -1460,7 +1460,7 @@ lemma exceptionMessage_ccorres:
\<Longrightarrow> register_from_H (ARM_H.exceptionMessage ! n)
= index exceptionMessageC n"
apply (simp add: exceptionMessageC_def ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def)
ARM.exceptionMessage_def)
apply (simp add: Arrays.update_def n_exceptionMessage_def fcp_beta nth_Cons'
fupdate_def
split: split_if)
@ -1848,7 +1848,7 @@ proof -
apply (rule guard_is_UNIVI, clarsimp simp: option_to_ptr_def)
apply (clarsimp simp: msgMaxLength_unfold length_syscallMessage
ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def
ARM.exceptionMessage_def
n_exceptionMessage_def)
apply (drule(1) obj_at_cslift_tcb[where thread=sender])
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
@ -1906,7 +1906,7 @@ lemma doFaultTransfer_ccorres [corres]:
apply (ctac (no_vcg, c_lines 2) add: setMessageInfo_ccorres)
apply (ctac add: setRegister_ccorres[unfolded dc_def])
apply wp
apply (simp add: badgeRegister_def MachineTypes.badgeRegister_def
apply (simp add: badgeRegister_def ARM.badgeRegister_def
Kernel_C.badgeRegister_def "StrictC'_register_defs")
apply (clarsimp simp: message_info_to_H_def guard_is_UNIVI
mask_def msgLengthBits_def
@ -3317,7 +3317,7 @@ proof -
apply ctac
apply wp
apply (clarsimp simp: Kernel_C.badgeRegister_def ARM_H.badgeRegister_def
MachineTypes.badgeRegister_def Kernel_C.R0_def)
ARM.badgeRegister_def Kernel_C.R0_def)
apply wp
apply simp
apply (wp hoare_case_option_wp getMessageInfo_le3
@ -3585,7 +3585,7 @@ lemma fault_case_absorb_bind:
lemma length_exceptionMessage:
"length ARM_H.exceptionMessage = unat n_exceptionMessage"
by (simp add: ARM_H.exceptionMessage_def MachineTypes.exceptionMessage_def n_exceptionMessage_def)
by (simp add: ARM_H.exceptionMessage_def ARM.exceptionMessage_def n_exceptionMessage_def)
lemma handleFaultReply_ccorres [corres]:
"ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
@ -3655,7 +3655,7 @@ lemma handleFaultReply_ccorres [corres]:
apply vcg
apply vcg
apply (rule conjI, simp add: ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def word_of_nat_less)
ARM.exceptionMessage_def word_of_nat_less)
apply (thin_tac "n < unat n'" for n')
apply (simp add: msgRegisters_ccorres n_msgRegisters_def length_msgRegisters
unat_of_nat exceptionMessage_ccorres[symmetric]
@ -3663,10 +3663,10 @@ lemma handleFaultReply_ccorres [corres]:
apply (simp add: word_less_nat_alt unat_of_nat)
apply (rule conseqPre, vcg)
apply (clarsimp simp: word_of_nat_less ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def)
ARM.exceptionMessage_def)
apply (clarsimp simp: min_def n_exceptionMessage_def
ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def
ARM.exceptionMessage_def
length_msgRegisters n_msgRegisters_def
message_info_to_H_def
split: split_if)
@ -3676,7 +3676,7 @@ lemma handleFaultReply_ccorres [corres]:
apply wp
apply simp
apply (clarsimp simp: ARM_H.exceptionMessage_def
MachineTypes.exceptionMessage_def
ARM.exceptionMessage_def
word_bits_def)
apply unat_arith
apply ceqv
@ -5485,7 +5485,7 @@ lemma completeSignal_ccorres:
apply assumption
apply wp
apply (clarsimp simp: guard_is_UNIV_def ARM_H.badgeRegister_def
MachineTypes.badgeRegister_def Kernel_C.badgeRegister_def
ARM.badgeRegister_def Kernel_C.badgeRegister_def
Kernel_C.R0_def)
-- "WaitingNtfn case"
apply (clarsimp simp: NtfnState_Active_def NtfnState_Waiting_def)
@ -5505,7 +5505,7 @@ lemma doNBRecvFailedTransfer_ccorres[corres]:
apply (cinit lift: thread_')
apply (ctac add: setRegister_ccorres)
by (clarsimp simp: Kernel_C.badgeRegister_def ARM_H.badgeRegister_def
MachineTypes.badgeRegister_def Kernel_C.R0_def)
ARM.badgeRegister_def Kernel_C.R0_def)
lemma receiveIPC_ccorres [corres]:
notes option.case_cong_weak [cong]
@ -6092,7 +6092,7 @@ lemma sendSignal_ccorres [corres]:
apply (ctac add: ntfn_set_active_ccorres[unfolded dc_def])
apply (clarsimp simp: guard_is_UNIV_def option_to_ctcb_ptr_def
ARM_H.badgeRegister_def Kernel_C.badgeRegister_def
MachineTypes.badgeRegister_def Kernel_C.R0_def
ARM.badgeRegister_def Kernel_C.R0_def
"StrictC'_thread_state_defs"less_mask_eq
Collect_const_mem)
apply (case_tac ts, simp_all add: receiveBlocked_def typ_heap_simps
@ -6155,7 +6155,7 @@ lemma sendSignal_ccorres [corres]:
apply (wp setThreadState_st_tcb set_ntfn_valid_objs' | clarsimp)+
apply (clarsimp simp: guard_is_UNIV_def ThreadState_Running_def mask_def
badgeRegister_def Kernel_C.badgeRegister_def
MachineTypes.badgeRegister_def Kernel_C.R0_def)
ARM.badgeRegister_def Kernel_C.R0_def)
apply (clarsimp simp: guard_is_UNIV_def NtfnState_Idle_def
NtfnState_Active_def NtfnState_Waiting_def)
apply clarsimp
@ -6503,7 +6503,7 @@ lemma receiveSignal_ccorres [corres]:
apply assumption
apply wp
apply (clarsimp simp: guard_is_UNIV_def)
apply (clarsimp simp: MachineTypes.badgeRegister_def Kernel_C.R0_def)
apply (clarsimp simp: ARM.badgeRegister_def Kernel_C.R0_def)
-- "WaitingNtfn case"
apply (rename_tac list)
apply (rule ccorres_cond_true)

4
proof/crefine/Machine_C.thy
View File

@ -126,7 +126,7 @@ assumes cleanL2Range_ccorres:
assumes clearExMonitor_ccorres:
"ccorres dc xfdc \<top> UNIV []
(doMachineOp MachineOps.clearExMonitor)
(doMachineOp ARM.clearExMonitor)
(Call clearExMonitor_'proc)"
assumes getIFSR_ccorres:
@ -181,7 +181,7 @@ assumes cleanCacheRange_PoU_spec:
(* clearExMonitor_fp is an inline-friendly version of clearExMonitor *)
assumes clearExMonitor_fp_ccorres:
"ccorres dc xfdc (\<lambda>_. True) UNIV [] (doMachineOp MachineOps.clearExMonitor)
"ccorres dc xfdc (\<lambda>_. True) UNIV [] (doMachineOp ARM.clearExMonitor)
(Call clearExMonitor_fp_'proc)"
(*

2
proof/crefine/Refine_C.thy
View File

@ -572,7 +572,7 @@ lemma ccorres_get_registers:
apply (drule(1) obj_at_cslift_tcb, clarsimp simp: obj_at'_def projectKOs)
apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
ARM_H.msgInfoRegister_def ARM_H.capRegister_def
MachineTypes.msgInfoRegister_def MachineTypes.capRegister_def
ARM.msgInfoRegister_def ARM.capRegister_def
"StrictC'_register_defs")
done

25
proof/crefine/Retype_C.thy
View File

@ -4792,19 +4792,11 @@ definition "placeNewObject_with_memset regionBase us \<equiv>
doMachineOp (mapM_x (\<lambda>p::word32. storeWord p (0::word32))
[regionBase , regionBase + (4::word32) .e. regionBase + (2::word32) ^ (pageBits + us) - (1::word32)])
od)"
end
context Arch begin global_naming ARM_H
lemmas createObject_def = ARM_H.createObject_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
crunch gsMaxObjectSize[wp]: placeNewObject_with_memset, createObject "\<lambda>s. P (gsMaxObjectSize s)"
(wp: crunch_wps simp: unless_def)
end
shadow_facts (in Arch) createObject_def
context kernel_m begin
lemma placeNewObject_user_data:
@ -7135,22 +7127,12 @@ lemma APIType_capBits_min:
end
(*FIXME: arch_split crunch bug *)
context Arch begin global_naming ARM_H'
lemmas createObject_def = ARM_H.createObject_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
crunch gsCNodes[wp]: insertNewCap, Arch_createNewCaps, threadSet,
"Arch.createObject" "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def ignore: getObject setObject)
end
(*FIXME: arch_split crunch bug *)
shadow_facts (in Arch) createObject_def
context begin interpretation Arch . (*FIXME: arch_split*)
lemma createNewCaps_1_gsCNodes_p:
"\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>"
@ -7174,9 +7156,10 @@ lemma createObject_cnodes_have_size:
apply (simp add: createObject_def)
apply (rule hoare_pre)
apply (wp mapM_x_wp' | wpc | simp add: createObjects_def)+
apply (cases newType, simp_all add: toAPIType_def ARM_H.toAPIType_def)
apply (cases newType, simp_all add: ARM_H.toAPIType_def)
apply (clarsimp simp: APIType_capBits_def objBits_simps
cnodes_retype_have_size_def cte_level_bits_def)
cnodes_retype_have_size_def cte_level_bits_def
split: split_if_asm)
done
lemma range_cover_not_in_neqD:

10
proof/crefine/Schedule_C.thy
View File

@ -106,7 +106,7 @@ lemma setVMRoot_valid_queues':
(* FIXME move to REFINE *)
crunch valid_queues'[wp]: "Arch.switchToThread" valid_queues'
(ignore: MachineOps.clearExMonitor)
(ignore: clearExMonitor)
crunch ksCurDomain[wp]: switchToIdleThread "\<lambda>s. P (ksCurDomain s)"
crunch valid_pspace'[wp]: switchToIdleThread, switchToThread valid_pspace'
(simp: whenE_def)
@ -116,9 +116,11 @@ end
(*FIXME: arch_split: move up?*)
context Arch begin
shadow_facts
switchToIdleThread_def
switchToThread_def
context begin global_naming global
requalify_facts
Thread_H.switchToIdleThread_def
Thread_H.switchToThread_def
end
end
context kernel_m begin

36
proof/crefine/StateRelation_C.thy
View File

@ -205,24 +205,24 @@ definition
fun
register_from_H :: "register \<Rightarrow> word32"
where
"register_from_H MachineTypes.R0 = scast Kernel_C.R0"
| "register_from_H MachineTypes.R1 = scast Kernel_C.R1"
| "register_from_H MachineTypes.R2 = scast Kernel_C.R2"
| "register_from_H MachineTypes.R3 = scast Kernel_C.R3"
| "register_from_H MachineTypes.R4 = scast Kernel_C.R4"
| "register_from_H MachineTypes.R5 = scast Kernel_C.R5"
| "register_from_H MachineTypes.R6 = scast Kernel_C.R6"
| "register_from_H MachineTypes.R7 = scast Kernel_C.R7"
| "register_from_H MachineTypes.R8 = scast Kernel_C.R8"
| "register_from_H MachineTypes.R9 = scast Kernel_C.R9"
| "register_from_H MachineTypes.SL = scast Kernel_C.R10"
| "register_from_H MachineTypes.FP = scast Kernel_C.R11"
| "register_from_H MachineTypes.IP = scast Kernel_C.R12"
| "register_from_H MachineTypes.SP = scast Kernel_C.SP"
| "register_from_H MachineTypes.LR = scast Kernel_C.LR"
| "register_from_H MachineTypes.LR_svc = scast Kernel_C.LR_svc"
| "register_from_H MachineTypes.CPSR = scast Kernel_C.CPSR"
| "register_from_H MachineTypes.FaultInstruction = scast Kernel_C.FaultInstruction"
"register_from_H ARM.R0 = scast Kernel_C.R0"
| "register_from_H ARM.R1 = scast Kernel_C.R1"
| "register_from_H ARM.R2 = scast Kernel_C.R2"
| "register_from_H ARM.R3 = scast Kernel_C.R3"
| "register_from_H ARM.R4 = scast Kernel_C.R4"
| "register_from_H ARM.R5 = scast Kernel_C.R5"
| "register_from_H ARM.R6 = scast Kernel_C.R6"
| "register_from_H ARM.R7 = scast Kernel_C.R7"
| "register_from_H ARM.R8 = scast Kernel_C.R8"
| "register_from_H ARM.R9 = scast Kernel_C.R9"
| "register_from_H ARM.SL = scast Kernel_C.R10"
| "register_from_H ARM.FP = scast Kernel_C.R11"
| "register_from_H ARM.IP = scast Kernel_C.R12"
| "register_from_H ARM.SP = scast Kernel_C.SP"
| "register_from_H ARM.LR = scast Kernel_C.LR"
| "register_from_H ARM.LR_svc = scast Kernel_C.LR_svc"
| "register_from_H ARM.CPSR = scast Kernel_C.CPSR"
| "register_from_H ARM.FaultInstruction = scast Kernel_C.FaultInstruction"
definition
ccontext_relation :: "(MachineTypes.register \<Rightarrow> word32) \<Rightarrow> user_context_C \<Rightarrow> bool"

6
proof/crefine/Syscall_C.thy
View File

@ -1016,9 +1016,9 @@ lemma handleInvocation_ccorres:
apply wp
apply (clarsimp simp: Collect_const_mem)
apply (simp add: Kernel_C.msgInfoRegister_def ARM_H.msgInfoRegister_def
MachineTypes.msgInfoRegister_def Kernel_C.R1_def
ARM.msgInfoRegister_def Kernel_C.R1_def
Kernel_C.capRegister_def ARM_H.capRegister_def
MachineTypes.capRegister_def Kernel_C.R0_def)
ARM.capRegister_def Kernel_C.R0_def)
apply (clarsimp simp: cfault_rel_def option_to_ptr_def)
apply (simp add: fault_cap_fault_lift is_cap_fault_def)
apply (frule lookup_failure_rel_fault_lift, assumption)
@ -1486,7 +1486,7 @@ lemma handleRecv_ccorres:
apply (clarsimp simp add: sch_act_sane_def)
apply (simp add: cap_get_tag_isCap[symmetric] del: rf_sr_upd_safe)
apply (simp add: Kernel_C.capRegister_def ARM_H.capRegister_def ct_in_state'_def
MachineTypes.capRegister_def Kernel_C.R0_def
ARM.capRegister_def Kernel_C.R0_def
tcb_at_invs')
apply (frule invs_valid_objs')
apply (frule tcb_aligned'[OF tcb_at_invs'])

2
proof/crefine/TcbAcc_C.thy
View File

@ -213,7 +213,7 @@ lemma sanitiseRegister_spec:
\<lbrace>\<acute>ret__unsigned_long = sanitiseRegister r v\<rbrace>"
apply vcg
apply (auto simp: C_register_defs ARM_H.sanitiseRegister_def
MachineTypes.sanitiseRegister_def word_0_sle_from_less
ARM.sanitiseRegister_def word_0_sle_from_less
split: register.split)
done

12
proof/crefine/Tcb_C.thy
View File

@ -1009,8 +1009,8 @@ lemma frame_gp_registers_convs:
"n < length ARM_H.gpRegisters \<Longrightarrow>
index gpRegistersC n = register_from_H (ARM_H.gpRegisters ! n)"
apply (simp_all add: ARM_H.gpRegisters_def ARM_H.frameRegisters_def
MachineTypes.gpRegisters_def n_gpRegisters_def
MachineTypes.frameRegisters_def n_frameRegisters_def
ARM.gpRegisters_def n_gpRegisters_def
ARM.frameRegisters_def n_frameRegisters_def
frameRegistersC_def gpRegistersC_def msgRegisters_unfold
fupdate_def Arrays.update_def toEnum_def
upto_enum_def fromEnum_def enum_register)
@ -1463,7 +1463,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
n_frameRegisters_def)
apply arith
apply (simp add: ARM_H.gpRegisters_def word_bits_def
MachineTypes.gpRegisters_def)
ARM.gpRegisters_def)
apply simp
apply (rule ceqv_refl)
apply (ctac(no_vcg) add: getRestartPC_ccorres)
@ -1558,7 +1558,7 @@ lemma msg_registers_convs:
"n < length ARM_H.msgRegisters \<Longrightarrow>
index msgRegistersC n = register_from_H (ARM_H.msgRegisters ! n)"
apply (simp_all add: msgRegisters_unfold
MachineTypes.msgRegisters_def n_msgRegisters_def
ARM.msgRegisters_def n_msgRegisters_def
msgRegistersC_def fupdate_def Arrays.update_def)
apply (auto simp: less_Suc_eq fcp_beta)
done
@ -1971,7 +1971,7 @@ shows
apply simp
apply (wp lookupIPCBuffer_Some_0 | wp_once hoare_drop_imps)+
apply (simp add: Collect_const_mem ARM_H.badgeRegister_def
MachineTypes.badgeRegister_def
ARM.badgeRegister_def
"StrictC'_register_defs")
apply (vcg exspec=lookupIPCBuffer_modifies)
apply (simp add: false_def)
@ -2404,7 +2404,7 @@ lemma ccap_relation_gen_framesize_to_H:
\<Longrightarrow> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap'))
= capVPSize (capCap cap)"
apply (clarsimp simp: isCap_simps)
apply (case_tac "sz = MachineTypes.ARMSmallPage")
apply (case_tac "sz = ARM.ARMSmallPage")
apply (frule cap_get_tag_PageCap_small_frame)
apply (simp add: cap_get_tag_isCap isCap_simps
pageSize_def cap_lift_small_frame_cap

20
proof/crefine/VSpace_C.thy
View File

@ -353,7 +353,7 @@ lemma storeHWASID_ccorres:
apply (simp split: split_if_asm)
apply (clarsimp simp: cpde_relation_def Let_def
pde_lift_pde_invalid
cong: Hardware_H.pde.case_cong)
cong: ARM_H.pde.case_cong)
apply (erule array_relation_update)
subgoal by simp
subgoal by (simp add: option_to_0_def)
@ -449,7 +449,7 @@ lemma invalidateASID_ccorres:
apply (simp split: split_if_asm)
apply (clarsimp simp: cpde_relation_def Let_def
pde_lift_pde_invalid
cong: Hardware_H.pde.case_cong)
cong: ARM_H.pde.case_cong)
apply (subst asid_map_pd_to_hwasids_clear, assumption)
subgoal by clarsimp
apply (rule ext, simp add: pd_pointer_to_asid_slot_def map_comp_def split: split_if)
@ -871,7 +871,7 @@ lemma lookupPTSlot_ccorres:
apply (simp add: pageBits_def)
apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def
pde_pde_coarse_lift Let_def isPageTablePDE_def
split: Hardware_H.pde.split_asm)
split: ARM_H.pde.split_asm)
done
lemma cap_case_isPageDirectoryCap:
@ -1654,10 +1654,10 @@ lemma setVMRootForFlush_ccorres:
(* FIXME: move to StateRelation_C *)
definition
"framesize_from_H sz \<equiv> case sz of
MachineTypes.ARMSmallPage \<Rightarrow> (scast Kernel_C.ARMSmallPage :: word32)
| MachineTypes.ARMLargePage \<Rightarrow> scast Kernel_C.ARMLargePage
| MachineTypes.ARMSection \<Rightarrow> scast Kernel_C.ARMSection
| MachineTypes.ARMSuperSection \<Rightarrow> scast Kernel_C.ARMSuperSection"
ARM.ARMSmallPage \<Rightarrow> (scast Kernel_C.ARMSmallPage :: word32)
| ARM.ARMLargePage \<Rightarrow> scast Kernel_C.ARMLargePage
| ARM.ARMSection \<Rightarrow> scast Kernel_C.ARMSection
| ARM.ARMSuperSection \<Rightarrow> scast Kernel_C.ARMSuperSection"
lemma framesize_from_to_H:
"gen_framesize_to_H (framesize_from_H sz) = sz"
@ -1901,7 +1901,7 @@ lemma setMessageInfo_ccorres:
apply (ctac add: setRegister_ccorres)
apply wp
apply vcg
apply (simp add: ARM_H.msgInfoRegister_def MachineTypes.msgInfoRegister_def
apply (simp add: ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def)
done
@ -1936,8 +1936,8 @@ lemma performPageGetAddress_ccorres:
apply (simp add: guard_is_UNIV_def)
apply wp
apply vcg
by (auto simp: Hardware_H.fromPAddr_def message_info_to_H_def mask_def ARM_H.msgInfoRegister_def
MachineTypes.msgInfoRegister_def Kernel_C.msgInfoRegister_def Kernel_C.R1_def
by (auto simp: ARM_H.fromPAddr_def message_info_to_H_def mask_def ARM_H.msgInfoRegister_def
ARM.msgInfoRegister_def Kernel_C.msgInfoRegister_def Kernel_C.R1_def
word_sle_def word_sless_def Kernel_C.R2_def
kernel_all_global_addresses.msgRegisters_def fupdate_def Arrays.update_def
fcp_beta)

8
proof/crefine/Wellformed_C.thy
View File

@ -203,16 +203,16 @@ vmrights_to_H :: "word32 \<Rightarrow> vmrights" where
(* Force clarity over name collisions *)
abbreviation
ARMSmallPage :: "vmpage_size" where
"ARMSmallPage == MachineTypes.ARMSmallPage"
"ARMSmallPage == ARM.ARMSmallPage"
abbreviation
ARMLargePage :: "vmpage_size" where
"ARMLargePage == MachineTypes.ARMLargePage"
"ARMLargePage == ARM.ARMLargePage"
abbreviation
ARMSection :: "vmpage_size" where
"ARMSection == MachineTypes.ARMSection"
"ARMSection == ARM.ARMSection"
abbreviation
ARMSuperSection :: "vmpage_size" where
"ARMSuperSection == MachineTypes.ARMSuperSection"
"ARMSuperSection == ARM.ARMSuperSection"
-- "ARMSmallFrame is treated in a separate cap in C,
so needs special treatment in ccap_relation"

2
proof/refine/Retype_R.thy
View File

@ -113,7 +113,7 @@ definition
makeObjectKO :: "(kernel_object + ARM_H.object_type) \<rightharpoonup> kernel_object"
where
"makeObjectKO ty \<equiv> case ty of
Inl KOUserData \<Rightarrow> Some KOUserData
Inl KOUserData \<Rightarrow> Some KOUserData
| Inl (KOArch (KOASIDPool _)) \<Rightarrow> Some (KOArch (KOASIDPool makeObject))
| Inr (APIObjectType ArchTypes_H.TCBObject) \<Rightarrow> Some (KOTCB makeObject)
| Inr (APIObjectType ArchTypes_H.EndpointObject) \<Rightarrow> Some (KOEndpoint makeObject)

9
spec/design/KernelStateData_H.thy
View File

@ -22,7 +22,6 @@ imports
"./$L4V_ARCH/ArchStateData_H"
begin
context begin interpretation Arch .
requalify_types
@ -30,7 +29,7 @@ requalify_types
end
requalify_types (in Arch)
requalify_types (in Arch)
kernel_state
subsection "The Kernel State"
@ -64,6 +63,12 @@ record kernel_state =
ksArchState :: Arch.kernel_state
ksMachineState :: machine_state
context Arch begin
context begin global_naming global
requalify_types KernelStateData_H.kernel_state
end
end
type_synonym 'a kernel = "(kernel_state, 'a) nondet_monad"
translations

11
spec/design/Kernel_H.thy
View File

@ -17,15 +17,4 @@ imports
FaultHandler_H
CSpace_H
begin
context Arch begin
requalify_types
kernel_state
requalify_types
KernelStateData_H.kernel_state
end
end

9
spec/design/skel/KernelStateData_H.thy
View File

@ -22,7 +22,6 @@ imports
"./$L4V_ARCH/ArchStateData_H"
begin
context begin interpretation Arch .
requalify_types
@ -30,7 +29,7 @@ requalify_types
end
requalify_types (in Arch)
requalify_types (in Arch)
kernel_state
subsection "The Kernel State"
@ -64,6 +63,12 @@ record kernel_state =
ksArchState :: Arch.kernel_state
ksMachineState :: machine_state
context Arch begin
context begin global_naming global
requalify_types KernelStateData_H.kernel_state
end
end
type_synonym 'a kernel = "(kernel_state, 'a) nondet_monad"
translations

11
spec/design/skel/Kernel_H.thy
View File

@ -17,15 +17,4 @@ imports
FaultHandler_H
CSpace_H
begin
context Arch begin
requalify_types
kernel_state
requalify_types
KernelStateData_H.kernel_state
end
end

4
spec/design/version
View File

@ -1,5 +1,5 @@
Built from git repo at /Users/dmatichuk/verification-archsplit/seL4/haskell by dmatichuk
Built from git repo at /home/matthewb/verification/arch_split/seL4/haskell by matthewb
Generated from changeset:
fd5246f Use constant to specify first dynamic cptr in doc
35add5e Updated bootinfo doc for userImagePaging field