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

crefine: resolve a small issue in design spec coming from haskell translator inflexibility 

- a case-statement in decodeARMMMUInvocation has an if-statement with a conjunction of three conditions, but they are translated in different orders between arm and arm-hyp and currently the crefine proofs depend on those orders.
- this fix is not a fundumental solution, but, given how reliable the haskell translator is, not sure how much effort we should be putting in here
This commit is contained in:
Miki Tanaka 2017-06-29 19:53:53 +10:00
parent 9f3924d1ea
commit 5a82068c34
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/crefine/ARM/Arch_C.thy
View File

@ -3984,6 +3984,7 @@ lemma Arch_decodeInvocation_ccorres:
apply (rule ccorres_Guard_Seq)+
apply (simp add: whenE_bindE_throwError_to_if if_to_top_of_bind
del: Collect_const)
apply (simp add: conj_commute[of "\<not> capIsDevice _"])
apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws[rotated -1])
apply clarsimp
apply (rule conseqPre, vcg, rule subset_refl)