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

riscv crefine: add valid_untyped' to ArchMove_C 

Opted to use old form of statement and adjust proof, as CRefine proofs
are not aware of mask_range and a cleanup of that sort would take too
long at this time.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski 2020-04-10 15:56:18 +10:00 committed by Gerwin Klein
parent 533dd333ac
commit 9a86c195ed
1 changed files with 48 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
proof/crefine/RISCV64/ArchMove_C.thy
View File

@ -98,6 +98,54 @@ lemma sign_extend_canonical_address:
"(x = sign_extend 38 x) = canonical_address x"
by (fastforce simp: sign_extended_iff_sign_extend canonical_address_sign_extended canonical_bit_def)
lemma ptr_range_mask_range:
"{ptr..ptr + 2 ^ bits - 1} = mask_range ptr bits"
unfolding mask_def
by simp
lemma valid_untyped':
notes usableUntypedRange.simps[simp del]
assumes pspace_distinct': "pspace_distinct' s" and
pspace_aligned': "pspace_aligned' s" and
al: "is_aligned ptr bits"
shows "valid_untyped' d ptr bits idx s =
(\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow>
obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow>
obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and>
obj_range' p ko \<inter>
usableUntypedRange (UntypedCap d ptr bits idx) = {})"
apply (simp add: valid_untyped'_def)
apply (simp add: ko_wp_at'_def)
apply (rule arg_cong[where f=All])
apply (rule ext)
apply (rule arg_cong[where f=All])
apply (rule ext)
apply (case_tac "ksPSpace s ptr' = Some ko", simp_all)
apply (frule pspace_alignedD'[OF _ pspace_aligned'])
apply (frule pspace_distinctD'[OF _ pspace_distinct'])
apply (simp add: ptr_range_mask_range)
apply (frule aligned_ranges_subset_or_disjoint[OF al])
apply (simp only: ptr_range_mask_range)
apply (fold obj_range'_def)
apply (rule iffI)
apply auto[1]
apply (rule conjI)
apply (rule ccontr, simp)
apply (simp add: Set.psubset_eq)
apply (erule conjE)
apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp)
apply (cut_tac is_aligned_no_overflow[OF al])
apply (clarsimp simp add: obj_range'_def mask_def add_diff_eq)
subgoal by auto
apply (clarsimp simp add: usableUntypedRange.simps Int_commute)
apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp+)
apply (cut_tac is_aligned_no_overflow[OF al])
apply (clarsimp simp add: obj_range'_def mask_def add_diff_eq)
apply (frule is_aligned_no_overflow)
by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1
nat_le_linear power_overflow sub_wrap add_0
add_0_right word_add_increasing word_less_1 word_less_sub_1)
lemma more_pageBits_inner_beauty:
fixes x :: "9 word"
fixes p :: machine_word