From 460764a088c6409c5be30db99fd41c09891f6ce0 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 11:12:02 +1030 Subject: [PATCH] clib: move ccorres_cond_both' to CCorresLemmas Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 23 +++++++++++++++++++++++ proof/crefine/AARCH64/SyscallArgs_C.thy | 19 ------------------- proof/crefine/ARM/SyscallArgs_C.thy | 19 ------------------- proof/crefine/ARM_HYP/SyscallArgs_C.thy | 19 ------------------- proof/crefine/RISCV64/SyscallArgs_C.thy | 19 ------------------- proof/crefine/X64/SyscallArgs_C.thy | 19 ------------------- 6 files changed, 23 insertions(+), 95 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 5f5c4af6ae..048f959038 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -990,6 +990,29 @@ lemma ccorres_cond2': apply clarsimp done +text \ + A stronger version of @{thm ccorres_cond_both}, which allows specifying a C state predicate + when showing equality of the conditionals' guards, and which supplies the relevant @{term If} + guard truth to the @{term ccorres_underlying} assumptions.\ +lemma ccorres_cond_both': + assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" + and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" + and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" + shows "ccorres_underlying sr G r xf arrel axf + (Q and (\s. P \ R s) and (\s. \ P \ U s)) + (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) + hs + (if P then a else b) (Cond P' c d)" + apply (rule ccorres_guard_imp2) + apply (rule ccorres_if_lhs) + apply (rule ccorres_cond_true) + apply (erule ac) + apply (rule ccorres_cond_false) + apply (erule bd) + apply clarsimp + apply (frule abs[rule_format, OF conjI], simp+) + done + lemmas ccorres_handlers_weaken2 = ccorres_nohs lemma ccorres_abstract_cleanup: diff --git a/proof/crefine/AARCH64/SyscallArgs_C.thy b/proof/crefine/AARCH64/SyscallArgs_C.thy index 662dab61a6..812d4ce0ca 100644 --- a/proof/crefine/AARCH64/SyscallArgs_C.thy +++ b/proof/crefine/AARCH64/SyscallArgs_C.thy @@ -707,25 +707,6 @@ lemma ccorres_case_bools: apply (auto simp: P Q) done -lemma ccorres_cond_both': - assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" - and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" - and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" - shows "ccorres_underlying sr G r xf arrel axf - (Q and (\s. P \ R s) and (\s. \ P \ U s)) - (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) - hs - (if P then a else b) (Cond P' c d)" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_if_lhs) - apply (rule ccorres_cond_true) - apply (erule ac) - apply (rule ccorres_cond_false) - apply (erule bd) - apply clarsimp - apply (frule abs[rule_format, OF conjI], simp+) - done - lemma pageBitsForSize_64 [simp]: "pageBitsForSize sz < 64" by (cases sz, auto simp: bit_simps) diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index 1aabd59eac..c0c29cae69 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -688,25 +688,6 @@ lemma ccorres_case_bools: apply (auto simp: P Q) done -lemma ccorres_cond_both': - assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" - and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" - and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" - shows "ccorres_underlying sr G r xf arrel axf - (Q and (\s. P \ R s) and (\s. \ P \ U s)) - (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) - hs - (if P then a else b) (Cond P' c d)" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_if_lhs) - apply (rule ccorres_cond_true) - apply (erule ac) - apply (rule ccorres_cond_false) - apply (erule bd) - apply clarsimp - apply (frule abs[rule_format, OF conjI], simp+) - done - lemma pageBitsForSize_32 [simp]: "pageBitsForSize sz < 32" by (cases sz, auto) diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index b1674729a1..cd1c70ac47 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -711,25 +711,6 @@ lemma ccorres_case_bools: apply (auto simp: P Q) done -lemma ccorres_cond_both': - assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" - and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" - and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" - shows "ccorres_underlying sr G r xf arrel axf - (Q and (\s. P \ R s) and (\s. \ P \ U s)) - (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) - hs - (if P then a else b) (Cond P' c d)" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_if_lhs) - apply (rule ccorres_cond_true) - apply (erule ac) - apply (rule ccorres_cond_false) - apply (erule bd) - apply clarsimp - apply (frule abs[rule_format, OF conjI], simp+) - done - lemma pageBitsForSize_32 [simp]: "pageBitsForSize sz < 32" by (cases sz, auto) diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index f75f4e9c55..b5e6fd4001 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -707,25 +707,6 @@ lemma ccorres_case_bools: apply (auto simp: P Q) done -lemma ccorres_cond_both': - assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" - and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" - and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" - shows "ccorres_underlying sr G r xf arrel axf - (Q and (\s. P \ R s) and (\s. \ P \ U s)) - (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) - hs - (if P then a else b) (Cond P' c d)" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_if_lhs) - apply (rule ccorres_cond_true) - apply (erule ac) - apply (rule ccorres_cond_false) - apply (erule bd) - apply clarsimp - apply (frule abs[rule_format, OF conjI], simp+) - done - lemma pageBitsForSize_32 [simp]: "pageBitsForSize sz < 64" by (cases sz, auto simp: bit_simps) diff --git a/proof/crefine/X64/SyscallArgs_C.thy b/proof/crefine/X64/SyscallArgs_C.thy index 808c4182c3..edac9ed997 100644 --- a/proof/crefine/X64/SyscallArgs_C.thy +++ b/proof/crefine/X64/SyscallArgs_C.thy @@ -713,25 +713,6 @@ lemma ccorres_case_bools: apply (auto simp: P Q) done -lemma ccorres_cond_both': - assumes abs: "\s s'. (s, s') \ sr \ Q s \ Q' s' \ P = (s' \ P')" - and ac: "P \ ccorres_underlying sr G r xf arrel axf R R' hs a c" - and bd: "\ P \ ccorres_underlying sr G r xf arrel axf U U' hs b d" - shows "ccorres_underlying sr G r xf arrel axf - (Q and (\s. P \ R s) and (\s. \ P \ U s)) - (Collect Q' \ {s. (s \ P' \ s \ R') \ (s \ P' \ s \ U')}) - hs - (if P then a else b) (Cond P' c d)" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_if_lhs) - apply (rule ccorres_cond_true) - apply (erule ac) - apply (rule ccorres_cond_false) - apply (erule bd) - apply clarsimp - apply (frule abs[rule_format, OF conjI], simp+) - done - lemma pageBitsForSize_32 [simp]: "pageBitsForSize sz < 64" by (cases sz, auto simp: bit_simps)