portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Verification: bf: use new proof features.

Browse source 
The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.
This commit is contained in:
Thomas Sewell 2016-03-14 23:56:07 +11:00
parent 9d431e293b
commit 13715658aa
1 changed files with 4 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
tools/bitfield_gen.py
View file

@ -546,25 +546,6 @@ lemmas %(name)s_ptr_guards[simp] =
%(name)s_ptr_words_aligned
%(name)s_ptr_words_ptr_safe'''
global_lemmas = \
'''lemmas guard_simps =
word_sle_def word_sless_def scast_id
lemmas mask_shift_simps =
ucast_def shift_over_ao_dists word_bw_assocs
word_size multi_shift_simps mask_def
word_ao_dist NOT_eq scast_id
word_and_max_word max_word_def
lemmas sep_heap_simps =
sep_app_def hrs_mem_update_def
hrs_htd_def split_def
lemma tag_eq_to_tag_masked_eq:
"tag == v ==> tag && m = v && m"
by simp
'''
defs_global_lemmas = '''
lemma word_sub_mask:
"\<lbrakk> w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \<rbrakk>
@ -845,8 +826,7 @@ done'''],
apply(simp add:h_t_valid_c_guard guard_simps)
(* Discharge heap-invariance conjuncts *)
apply(rule conjI[rotated])
apply(simp add:heap_update_field_hrs h_t_valid_c_guard typ_heap_simps)
apply prove_bf_clift_invariance
(* Lift field updates to bitfield struct updates *)
apply(simp add:heap_update_field_hrs h_t_valid_c_guard typ_heap_simps)
@ -1017,6 +997,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps
@ -1113,6 +1094,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps)
apply(simp add:%(name)s_%(block)s_lift_def)
@ -1134,6 +1116,7 @@ done
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
apply(frule clift_subtype, simp, simp)
apply prove_bf_clift_invariance
apply(clarsimp simp: typ_heap_simps c_guard_clift)
apply(simp add: guard_simps mask_shift_simps
@ -2784,9 +2767,6 @@ if __name__ == '__main__':
+ '"'), file=out_file)
print(file=out_file)
print(global_lemmas, file=out_file)
print(file=out_file)
for e in blocks.values() + unions.values():
e.generate_hol_proofs(options, type_map)
@ -2821,9 +2801,6 @@ if __name__ == '__main__':
file=out_file)
print(file=out_file)
print(global_lemmas, file=out_file)
print(file=out_file)
options.output = out_file
e.generate_hol_proofs(options, type_map)