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

aarch64 refine: first pass through Interrupt_R 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-05-19 19:08:30 +10:00
parent 865facfde9
commit 835d82c253
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
2 changed files with 1172 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -44,7 +44,7 @@ lemma setIRQState_corres:
lemma setIRQState_invs[wp]:
"\<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and>
(state \<noteq> IRQInactive \<longrightarrow> irq \<le> maxIRQ \<and> irq \<noteq> irqInvalid)\<rbrace>
(state \<noteq> IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace>
setIRQState state irq
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def)

1171
proof/refine/AARCH64/Interrupt_R.thy Normal file
View File

File diff suppressed because it is too large Load Diff