secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

arm+arm-hyp crefine: update for platform constant changes 

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski 2020-11-14 18:21:08 +11:00 committed by Rafal Kolanski
parent 6a587f7c20
commit 7d998ac2ba
4 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/crefine/ARM/Arch_C.thy
View File

@ -2191,7 +2191,7 @@ lemma decodeARMFrameInvocation_ccorres:
is_aligned_neg_mask_eq[simp del]
is_aligned_neg_mask_weaken[simp del]
defines "does_not_throw args extraCaps pg_sz mapdata \<equiv>
(mapdata = None \<longrightarrow> \<not> (ARM_H.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata = None \<longrightarrow> \<not> (ARM.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata \<noteq> None \<longrightarrow> (fst (the mapdata) = (the (capPDMappedASID (capCap (fst (extraCaps ! 0)))))
\<and> snd (the mapdata) = hd args))"
shows
@ -2484,7 +2484,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply clarsimp
apply ccorres_rewrite
apply csymbr
apply (simp add: ARM_H.pptrBase_def ARM.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: ARM.pptrBase_def ARM.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply ccorres_rewrite
apply (rule syscall_error_throwError_ccorres_n[unfolded id_def dc_def])
apply (simp add: syscall_error_to_H_cases)
@ -2510,7 +2510,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (csymbr, clarsimp, ccorres_rewrite)
apply (csymbr,
simp add: ARM_H.pptrBase_def ARM.pptrBase_def
simp add: ARM.pptrBase_def ARM.pptrBase_def
hd_conv_nth length_ineq_not_Nil,
ccorres_rewrite)
apply (fold dc_def)

4
proof/crefine/ARM/Finalise_C.thy
View File

@ -1414,7 +1414,7 @@ lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capab
apply (frule (1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
ARM_H.pptrBase_def
ARM.pptrBase_def
framesize_to_H_def valid_cap'_def
elim!: ccap_relationE simp del: Collect_const)
apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage")
@ -1726,7 +1726,7 @@ lemma Arch_finaliseCap_ccorres:
apply (subgoal_tac "capVPMappedAddress cp \<noteq> None")
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
Kernel_C.ARMSmallPage_def ARM_H.pptrBase_def
Kernel_C.ARMSmallPage_def ARM.pptrBase_def
if_split
elim!: ccap_relationE simp del: Collect_const)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def

8
proof/crefine/ARM_HYP/Arch_C.thy
View File

@ -2568,7 +2568,7 @@ lemma throwError_invocationCatch:
lemma decodeARMFrameInvocation_ccorres:
notes if_cong[cong] tl_drop_1[simp]
defines "does_not_throw args extraCaps pg_sz mapdata \<equiv>
(mapdata = None \<longrightarrow> \<not> (ARM_HYP_H.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata = None \<longrightarrow> \<not> (ARM_HYP.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata \<noteq> None \<longrightarrow> (fst (the mapdata) = (the (capPDMappedASID (capCap (fst (extraCaps ! 0)))))
\<and> snd (the mapdata) = hd args))"
shows
@ -2879,7 +2879,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply clarsimp
apply ccorres_rewrite
apply csymbr
apply (simp add: ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: ARM_HYP.pptrBase_def ARM_HYP.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply ccorres_rewrite
apply (rule syscall_error_throwError_ccorres_n[unfolded id_def dc_def])
apply (simp add: syscall_error_to_H_cases)
@ -2904,7 +2904,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (csymbr, clarsimp, ccorres_rewrite)
apply (csymbr,
simp add: ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def
simp add: ARM_HYP.pptrBase_def ARM_HYP.pptrBase_def
hd_conv_nth length_ineq_not_Nil,
ccorres_rewrite)
apply (fold dc_def)
@ -3073,7 +3073,7 @@ lemma decodeARMFrameInvocation_ccorres:
framesize_from_H_eq_eqs of_bool_nth[simplified of_bool_from_bool]
vm_page_size_defs neq_Nil_conv excaps_in_mem_def hd_conv_nth
length_ineq_not_Nil numeral_2_eq_2 does_not_throw_def
ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def)
ARM_HYP.pptrBase_def ARM_HYP.pptrBase_def)
apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
apply (frule(1) slotcap_in_mem_PageDirectory)
apply (clarsimp simp: mask_def[where n=4] typ_heap_simps' isCap_simps)

4
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -2258,7 +2258,7 @@ lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capab
apply (frule (1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
ARM_HYP_H.pptrBase_def
ARM_HYP.pptrBase_def
framesize_to_H_def valid_cap'_def
elim!: ccap_relationE simp del: Collect_const)
apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage")
@ -2583,7 +2583,7 @@ lemma Arch_finaliseCap_ccorres:
apply (subgoal_tac "capVPMappedAddress cp \<noteq> None")
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
Kernel_C.ARMSmallPage_def ARM_HYP_H.pptrBase_def
Kernel_C.ARMSmallPage_def ARM_HYP.pptrBase_def
if_split
elim!: ccap_relationE simp del: Collect_const)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def