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

riscv refine: simplify assumptions in CSpace_R

This commit is contained in:
Gerwin Klein 2019-07-07 21:05:03 +10:00
parent b1157aef9e
commit 42bd55ea3b
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
proof/refine/RISCV64/CSpace_R.thy
View File

@ -3270,8 +3270,7 @@ lemma cteInsert_invs:
"\<lbrace>invs' and cte_wp_at' (\<lambda>c. cteCap c=NullCap) dest and valid_cap' cap and
(\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)
and cte_wp_at' (untyped_derived_eq cap o cteCap) src
and ex_cte_cap_to' dest and (\<lambda>s. \<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)
and safe_ioport_insert' cap NullCap\<rbrace>
and ex_cte_cap_to' dest and (\<lambda>s. \<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
cteInsert cap src dest
\<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: invs'_def valid_state'_def valid_pspace'_def)