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

refine+crefine: arch-split Machine_R 

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2025-06-26 13:14:31 +10:00 committed by Rafal Kolanski
parent 9dabd695c2
commit 1ab65b78ed
23 changed files with 54 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/AARCH64/SyscallArgs_C.thy
View File

@ -170,7 +170,7 @@ lemma preemptionPoint_ccorres:
apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
return_def split: option.splits)
apply (clarsimp simp: cintr_def exception_defs)
apply wp+
apply wpsimp+
apply vcg
apply (unfold modifyWorkUnits_def)[1]
apply wp

2
proof/crefine/ARM/SyscallArgs_C.thy
View File

@ -169,7 +169,7 @@ lemma preemptionPoint_ccorres:
apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
return_def split: option.splits)
apply (clarsimp simp: cintr_def exception_defs)
apply wp+
apply wpsimp+
apply vcg
apply (unfold modifyWorkUnits_def)[1]
apply wp

2
proof/crefine/ARM_HYP/SyscallArgs_C.thy
View File

@ -169,7 +169,7 @@ lemma preemptionPoint_ccorres:
apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
return_def split: option.splits)
apply (clarsimp simp: cintr_def exception_defs)
apply wp+
apply wpsimp+
apply vcg
apply (unfold modifyWorkUnits_def)[1]
apply wp

2
proof/crefine/RISCV64/SyscallArgs_C.thy
View File

@ -170,7 +170,7 @@ lemma preemptionPoint_ccorres:
apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
return_def split: option.splits)
apply (clarsimp simp: cintr_def exception_defs)
apply wp+
apply wpsimp+
apply vcg
apply (unfold modifyWorkUnits_def)[1]
apply wp

2
proof/crefine/X64/SyscallArgs_C.thy
View File

@ -169,7 +169,7 @@ lemma preemptionPoint_ccorres:
apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
return_def split: option.splits)
apply (clarsimp simp: cintr_def exception_defs)
apply wp+
apply wpsimp+
apply vcg
apply (unfold modifyWorkUnits_def)[1]
apply wp

16
proof/refine/AARCH64/Machine_R.thy → proof/refine/AARCH64/ArchMachine_R.thy
View File

@ -8,21 +8,11 @@
Properties of machine operations.
*)
theory Machine_R
imports ArchBits_R
theory ArchMachine_R
imports Machine_R
begin
definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
context begin interpretation Arch . (*FIXME: arch-split*)
context Arch begin arch_global_naming
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"

5
proof/refine/AARCH64/Finalise_R.thy
View File

@ -1480,8 +1480,6 @@ lemma emptySlot_valid_irq_handlers'[wp]:
apply auto
done
declare setIRQState_irq_states' [wp]
context begin interpretation Arch .
crunch emptySlot
for irq_states'[wp]: valid_irq_states'
@ -1490,8 +1488,6 @@ crunch emptySlot
for no_0_obj'[wp]: no_0_obj'
(wp: crunch_wps)
end
lemma deletedIRQHandler_irqs_masked'[wp]:
"\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def)
@ -1499,7 +1495,6 @@ lemma deletedIRQHandler_irqs_masked'[wp]:
apply (simp add: irqs_masked'_def)
done
context begin interpretation Arch . (*FIXME: arch-split*)
crunch emptySlot
for irqs_masked'[wp]: "irqs_masked'"

2
proof/refine/AARCH64/KHeap_R.thy
View File

@ -7,7 +7,7 @@
theory KHeap_R
imports
Machine_R
ArchMachine_R
begin
lemma lookupAround2_known1:

16
proof/refine/ARM/Machine_R.thy → proof/refine/ARM/ArchMachine_R.thy
View File

@ -8,21 +8,11 @@
Properties of machine operations.
*)
theory Machine_R
imports ArchBits_R
theory ArchMachine_R
imports Machine_R
begin
definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
context begin interpretation Arch . (*FIXME: arch-split*)
context Arch begin arch_global_naming
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"

4
proof/refine/ARM/Finalise_R.thy
View File

@ -1440,8 +1440,6 @@ lemma emptySlot_valid_irq_handlers'[wp]:
apply auto
done
declare setIRQState_irq_states' [wp]
context begin interpretation Arch .
crunch emptySlot
for irq_states'[wp]: valid_irq_states'
@ -1452,7 +1450,6 @@ crunch emptySlot
crunch emptySlot
for pde_mappings'[wp]: "valid_pde_mappings'"
end
lemma deletedIRQHandler_irqs_masked'[wp]:
"\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
@ -1461,7 +1458,6 @@ lemma deletedIRQHandler_irqs_masked'[wp]:
apply (simp add: irqs_masked'_def)
done
context begin interpretation Arch . (*FIXME: arch-split*)
crunch emptySlot
for irqs_masked'[wp]: "irqs_masked'"

2
proof/refine/ARM/KHeap_R.thy
View File

@ -7,7 +7,7 @@
theory KHeap_R
imports
"AInvs.ArchDetSchedSchedule_AI"
Machine_R
ArchMachine_R
begin
lemma lookupAround2_known1:

2
proof/refine/ARM/Refine.thy
View File

@ -732,7 +732,7 @@ lemma checkActiveIRQ_valid_duplicates':
checkActiveIRQ
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add: checkActiveIRQ_def)
apply wp
apply wpsimp
done
lemma check_active_irq_corres':

16
proof/refine/ARM_HYP/Machine_R.thy → proof/refine/ARM_HYP/ArchMachine_R.thy
View File

@ -8,21 +8,11 @@
Properties of machine operations.
*)
theory Machine_R
imports ArchBits_R
theory ArchMachine_R
imports Machine_R
begin
definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
context begin interpretation Arch . (*FIXME: arch-split*)
context Arch begin arch_global_naming
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"

4
proof/refine/ARM_HYP/Finalise_R.thy
View File

@ -1454,8 +1454,6 @@ lemma emptySlot_valid_irq_handlers'[wp]:
apply auto
done
declare setIRQState_irq_states' [wp]
context begin interpretation Arch .
crunch emptySlot
for irq_states'[wp]: valid_irq_states'
@ -1466,7 +1464,6 @@ crunch emptySlot
crunch emptySlot
for pde_mappings'[wp]: "valid_pde_mappings'"
end
lemma deletedIRQHandler_irqs_masked'[wp]:
"\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
@ -1475,7 +1472,6 @@ lemma deletedIRQHandler_irqs_masked'[wp]:
apply (simp add: irqs_masked'_def)
done
context begin interpretation Arch . (*FIXME: arch-split*)
crunch emptySlot
for irqs_masked'[wp]: "irqs_masked'"

2
proof/refine/ARM_HYP/KHeap_R.thy
View File

@ -7,7 +7,7 @@
theory KHeap_R
imports
"AInvs.ArchDetSchedSchedule_AI"
Machine_R
ArchMachine_R
begin
lemma lookupAround2_known1:

2
proof/refine/ARM_HYP/Refine.thy
View File

@ -741,7 +741,7 @@ lemma checkActiveIRQ_valid_duplicates':
checkActiveIRQ
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add: checkActiveIRQ_def)
apply wp
apply wpsimp
done
lemma check_active_irq_corres':

27
proof/refine/Machine_R.thy Normal file
View File

@ -0,0 +1,27 @@
(*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
Properties of machine operations - generic interface.
*)
theory Machine_R
imports ArchBits_R
begin
definition irq_state_independent_H :: "(kernel_state \<Rightarrow> bool) \<Rightarrow> bool" where
"irq_state_independent_H P \<equiv>
\<forall>f s. P s \<longrightarrow> P (s\<lparr>ksMachineState :=
ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState :=
ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
end

16
proof/refine/RISCV64/Machine_R.thy → proof/refine/RISCV64/ArchMachine_R.thy
View File

@ -8,21 +8,11 @@
Properties of machine operations.
*)
theory Machine_R
imports ArchBits_R
theory ArchMachine_R
imports Machine_R
begin
definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
context begin interpretation Arch . (*FIXME: arch-split*)
context Arch begin arch_global_naming
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"

5
proof/refine/RISCV64/Finalise_R.thy
View File

@ -1405,8 +1405,6 @@ lemma emptySlot_valid_irq_handlers'[wp]:
apply auto
done
declare setIRQState_irq_states' [wp]
context begin interpretation Arch .
crunch emptySlot
for irq_states'[wp]: valid_irq_states'
@ -1415,8 +1413,6 @@ crunch emptySlot
for no_0_obj'[wp]: no_0_obj'
(wp: crunch_wps)
end
lemma deletedIRQHandler_irqs_masked'[wp]:
"\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def)
@ -1424,7 +1420,6 @@ lemma deletedIRQHandler_irqs_masked'[wp]:
apply (simp add: irqs_masked'_def)
done
context begin interpretation Arch . (*FIXME: arch-split*)
crunch emptySlot
for irqs_masked'[wp]: "irqs_masked'"

2
proof/refine/RISCV64/KHeap_R.thy
View File

@ -6,7 +6,7 @@
theory KHeap_R
imports
Machine_R
ArchMachine_R
begin
lemma lookupAround2_known1:

16
proof/refine/X64/Machine_R.thy → proof/refine/X64/ArchMachine_R.thy
View File

@ -8,21 +8,11 @@
Properties of machine operations.
*)
theory Machine_R
imports ArchBits_R
theory ArchMachine_R
imports Machine_R
begin
definition "irq_state_independent_H (P :: kernel_state \<Rightarrow> bool)\<equiv>
\<forall>(f :: nat \<Rightarrow> nat) (s :: kernel_state). P s \<longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)"
lemma irq_state_independent_HI[intro!, simp]:
"\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
\<Longrightarrow> irq_state_independent_H P"
by (simp add: irq_state_independent_H_def)
context begin interpretation Arch . (*FIXME: arch-split*)
context Arch begin arch_global_naming
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"

5
proof/refine/X64/Finalise_R.thy
View File

@ -1407,8 +1407,6 @@ lemma emptySlot_valid_irq_handlers'[wp]:
apply auto
done
declare setIRQState_irq_states' [wp]
context begin interpretation Arch .
crunch emptySlot
for irq_states'[wp]: valid_irq_states'
@ -1417,8 +1415,6 @@ crunch emptySlot
for no_0_obj'[wp]: no_0_obj'
(wp: crunch_wps)
end
lemma deletedIRQHandler_irqs_masked'[wp]:
"\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>"
apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def)
@ -1426,7 +1422,6 @@ lemma deletedIRQHandler_irqs_masked'[wp]:
apply (simp add: irqs_masked'_def)
done
context begin interpretation Arch . (*FIXME: arch-split*)
crunch emptySlot
for irqs_masked'[wp]: "irqs_masked'"

2
proof/refine/X64/KHeap_R.thy
View File

@ -7,7 +7,7 @@
theory KHeap_R
imports
"AInvs.ArchDetSchedSchedule_AI"
Machine_R
ArchMachine_R
begin
lemma lookupAround2_known1: