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

crefine: update for PR seL4/seL4#321 

The aim of the PR was readability, but it actually also brings the
C more in line with the spec.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-12-06 12:18:38 +11:00 committed by Gerwin Klein
parent 614e24ee10
commit 46a1d2509a
4 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/crefine/ARM/CSpace_RAB_C.thy
View File

@ -324,8 +324,8 @@ next
unat guardBits = capCNodeGuardSize cap;
\<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
\<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
by clarsimp unat_arith
have cond4:
"\<And>rva nodeCapb ret__unsigned_long.

4
proof/crefine/ARM_HYP/CSpace_RAB_C.thy
View File

@ -360,8 +360,8 @@ next
unat guardBits = capCNodeGuardSize cap;
\<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
\<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
by clarsimp unat_arith
have cond4:
"\<And>rva nodeCapb ret__unsigned_long.

4
proof/crefine/RISCV64/CSpace_RAB_C.thy
View File

@ -362,8 +362,8 @@ next
unat guardBits = capCNodeGuardSize cap;
\<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
\<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
by clarsimp unat_arith
have cond4:
"\<And>rva nodeCapb ret__unsigned_long.

4
proof/crefine/X64/CSpace_RAB_C.thy
View File

@ -362,8 +362,8 @@ next
unat guardBits = capCNodeGuardSize cap;
\<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
\<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
(guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
by clarsimp unat_arith
have cond4:
"\<And>rva nodeCapb ret__unsigned_long.