secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

clib: add ccorres_empty_handler_stackI to Corres_UL_C 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2024-07-09 11:26:48 +09:30 committed by michaelmcinerney
parent 06ef418121
commit 949512d202
2 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/clib/CCorresLemmas.thy
View File

@ -1176,7 +1176,7 @@ proof -
show ?thesis
by (fastforce dest!: helper intermediate_Normal_state spec
intro: ccorresI_empty_handler_stack cond_hoarep')
intro: ccorres_empty_handler_stackI cond_hoarep')
qed
lemmas ccorres_While' = ccorres_While[where C'=UNIV, simplified]

12
lib/clib/Corres_UL_C.thy
View File

@ -141,6 +141,18 @@ lemma ccorresI':
apply simp
done
text \<open> For proving low-level @{term ccorresG} statements where the concrete function always
returns a @{term Normal} state, and therefore, the handler stack will not be used, and can
be considered empty.\<close>
lemma ccorres_empty_handler_stackI:
assumes rl:
"\<And>s s' xstate.
\<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<Gamma> \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> xstate; \<not> snd (a s)\<rbrakk>
\<Longrightarrow> (\<exists>t'. xstate = Normal t' \<and> (\<exists>(r, t) \<in> fst (a s). (t, t') \<in> srel \<and> rrel r (xf t')))"
shows "ccorresG srel \<Gamma> rrel xf G G' [] a c"
by (fastforce dest: rl elim: exec_handlers.cases
simp: ccorres_underlying_def isNormal_def isAbr_def unif_rrel_def)
text \<open>A congruence rule for the program part of correspondence functions (prevents schematic
rewriting).\<close>
lemma ccorres_prog_only_cong: