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

riscv ainvs: cleanup tweak for store_pte_invs

This commit is contained in:
Gerwin Klein 2019-05-07 14:52:34 +10:00 committed by Rafal Kolanski
parent af6e0765c5
commit 4a73ad6ef1
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/RISCV64/ArchAcc_AI.thy
View File

@ -2880,7 +2880,7 @@ lemma store_pte_valid_arch_caps:
by (wpsimp wp: store_pte_valid_vs_lookup store_pte_valid_table_caps)
lemma store_pte_invs:
"\<lbrace> invs and P
"\<lbrace> invs
and (\<lambda>s. table_base p \<notin> global_refs s)
and K (wellformed_pte pte)
and (\<lambda>s. \<forall>level. \<exists>\<rhd> (level, table_base p) s