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

riscv+x64 crefine: remove unused lemma 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-03-10 10:59:03 +11:00 committed by Corey Lewis
parent 1d2e75fd81
commit ba241aac64
2 changed files with 0 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
proof/crefine/RISCV64/Finalise_C.thy
View File

@ -1734,22 +1734,6 @@ lemma cnotification_relation_udpate_arch:
apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case)
done
lemma sanitiseSetRegister_ccorres:
"\<lbrakk> val = val'; reg' = register_from_H reg\<rbrakk> \<Longrightarrow>
ccorres dc xfdc (tcb_at' tptr)
UNIV
hs
(asUser tptr (setRegister reg (local.sanitiseRegister False reg val)))
(\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(reg',val',0);;
CALL setRegister(tcb_ptr_to_ctcb_ptr tptr,reg',\<acute>unsigned_long_eret_2))"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_r)
apply (ctac add: setRegister_ccorres)
apply (vcg)
apply (rule conseqPre, vcg)
apply (fastforce simp: sanitiseRegister_def split: register.splits)
by (auto simp: sanitiseRegister_def from_bool_def simp del: Collect_const split: register.splits bool.splits)
lemma case_option_both[simp]:
"(case f of None \<Rightarrow> P | _ \<Rightarrow> P) = P"
by (auto split: option.splits)

16
proof/crefine/X64/Finalise_C.thy
View File

@ -1810,22 +1810,6 @@ lemma cnotification_relation_udpate_arch:
apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case)
done
lemma sanitiseSetRegister_ccorres:
"\<lbrakk> val = val'; reg' = register_from_H reg\<rbrakk> \<Longrightarrow>
ccorres dc xfdc (tcb_at' tptr)
UNIV
hs
(asUser tptr (setRegister reg (local.sanitiseRegister False reg val)))
(\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(reg',val',0);;
CALL setRegister(tcb_ptr_to_ctcb_ptr tptr,reg',\<acute>unsigned_long_eret_2))"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_r)
apply (ctac add: setRegister_ccorres)
apply (vcg)
apply (rule conseqPre, vcg)
apply (fastforce simp: sanitiseRegister_def split: register.splits)
by (auto simp: sanitiseRegister_def from_bool_def simp del: Collect_const split: register.splits bool.splits)
lemma case_option_both[simp]:
"(case f of None \<Rightarrow> P | _ \<Rightarrow> P) = P"
by (auto split: option.splits)