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

arm-hyp ainvs: fix proofs broken by spec update

This commit is contained in:
Matthew Brecknell 2017-04-30 10:06:18 +10:00 committed by Alejandro Gomez-Londono
parent 3757e605d4
commit ec0c106c49
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy
View File

@ -446,8 +446,8 @@ lemma vgic_maintenance_irq_valid_sched[wp]:
unfolding vgic_maintenance_def
get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_eisr1_def get_gic_vcpu_ctrl_eisr0_def
apply (wpsimp wp: handle_fault_valid_sched thread_get_wp'
simp: do_machine_op_bind valid_fault_def
| rule conjI | strengthen conj_imp_strg)+
simp: do_machine_op_bind valid_fault_def submonad_do_machine_op.gets
| intro conjI impI)+
apply (clarsimp simp: st_tcb_at_def obj_at_def runnable_eq)
done

6
proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy
View File

@ -212,11 +212,11 @@ lemma vgic_maintenance_invs[wp]:
"\<lbrace>invs\<rbrace> vgic_maintenance \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding vgic_maintenance_def get_gic_vcpu_ctrl_misr_def
get_gic_vcpu_ctrl_eisr1_def get_gic_vcpu_ctrl_eisr0_def
apply (wpsimp simp: valid_fault_def do_machine_op_bind ct_in_state_def
apply (wpsimp simp: do_machine_op_bind submonad_do_machine_op.gets valid_fault_def
wp: thread_get_wp'
| strengthen conj_imp_strg)+
| intro conjI impI)+
apply (fastforce intro!: st_tcb_ex_cap[where P=active]
simp: st_tcb_at_def obj_at_def runnable_eq halted_eq)
simp: st_tcb_at_def obj_at_def runnable_eq halted_eq)+
done
lemma handle_reserved_irq_invs[wp]: