cspec/crefine: make ctcb_offset available to AUXUPD
This commit is contained in:
parent
0f38e20094
commit
62bee91f12
|
@ -116,18 +116,6 @@ definition
|
||||||
where
|
where
|
||||||
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_size_bits :: nat
|
|
||||||
where
|
|
||||||
"ctcb_size_bits \<equiv> 8"
|
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_offset :: word32
|
|
||||||
where
|
|
||||||
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
|
||||||
|
|
||||||
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
|
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
|
||||||
where
|
where
|
||||||
|
|
|
@ -131,18 +131,6 @@ definition
|
||||||
where
|
where
|
||||||
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_size_bits :: nat
|
|
||||||
where
|
|
||||||
"ctcb_size_bits \<equiv> 8"
|
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_offset :: word32
|
|
||||||
where
|
|
||||||
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
|
||||||
|
|
||||||
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
|
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
|
||||||
where
|
where
|
||||||
|
|
|
@ -122,18 +122,6 @@ definition
|
||||||
where
|
where
|
||||||
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
"cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_size_bits :: nat
|
|
||||||
where
|
|
||||||
"ctcb_size_bits \<equiv> 10"
|
|
||||||
|
|
||||||
definition
|
|
||||||
ctcb_offset :: machine_word
|
|
||||||
where
|
|
||||||
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
|
||||||
|
|
||||||
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word64"
|
ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word64"
|
||||||
where
|
where
|
||||||
|
|
|
@ -77,6 +77,18 @@ requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_size_bits :: nat
|
||||||
|
where
|
||||||
|
"ctcb_size_bits \<equiv> 8"
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_offset :: "32 word"
|
||||||
|
where
|
||||||
|
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
||||||
|
|
||||||
|
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
||||||
|
|
||||||
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
||||||
[machinety=machine_state, ghostty=cghost_state]
|
[machinety=machine_state, ghostty=cghost_state]
|
||||||
|
|
||||||
|
|
|
@ -77,6 +77,18 @@ requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_size_bits :: nat
|
||||||
|
where
|
||||||
|
"ctcb_size_bits \<equiv> 8"
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_offset :: "32 word"
|
||||||
|
where
|
||||||
|
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
||||||
|
|
||||||
|
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
||||||
|
|
||||||
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
||||||
[machinety=machine_state, ghostty=cghost_state]
|
[machinety=machine_state, ghostty=cghost_state]
|
||||||
|
|
||||||
|
|
|
@ -75,6 +75,18 @@ context begin interpretation Arch . global_naming vmpage_size
|
||||||
requalify_consts X64SmallPage X64LargePage X64HugePage
|
requalify_consts X64SmallPage X64LargePage X64HugePage
|
||||||
end
|
end
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_size_bits :: nat
|
||||||
|
where
|
||||||
|
"ctcb_size_bits \<equiv> 10"
|
||||||
|
|
||||||
|
definition
|
||||||
|
ctcb_offset :: "64 word"
|
||||||
|
where
|
||||||
|
"ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
|
||||||
|
|
||||||
|
lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
|
||||||
|
|
||||||
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
|
||||||
[machinety=machine_state, ghostty=cghost_state]
|
[machinety=machine_state, ghostty=cghost_state]
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue