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

bitfield_gen: merge clarsimp/simp in generated proofs

Browse source 
The old generated proofs would fail if a simp set change made
`clarsimp` discharge what `simp` simplified.
This commit is contained in:
Edward Pierzchalski 2018-07-19 12:31:42 +10:00
parent 8cf34ab395
commit 1283345bfd
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tools/bitfield_gen.py
View file

@ -952,8 +952,7 @@ done'''],
%(name)s_get_tag \<acute>ret__struct_%(name)s_C = ''' \
'''scast %(name)s_%(block)s\<rbrace>"''',
''' apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: guard_simps o_def)
apply (simp add: mask_def shift_over_ao_dists)
apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists)
apply (rule context_conjI[THEN iffD1[OF conj_commute]],
fastforce simp: %(name)s_get_tag_eq_x %(name)s_%(block)s_def
mask_def shift_over_ao_dists word_bw_assocs word_ao_dist)