From a3a4e215244861fbc39a4f2c90938df592199b89 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 11:40:43 +1030 Subject: [PATCH 1/5] lib/monads: move gets_the_sp to Nondet_VCG Signed-off-by: Michael McInerney --- lib/Monads/nondet/Nondet_VCG.thy | 4 ++++ proof/invariant-abstract/CSpaceInv_AI.thy | 4 ---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy index 1ebd4a18f2..210ba436d9 100644 --- a/lib/Monads/nondet/Nondet_VCG.thy +++ b/lib/Monads/nondet/Nondet_VCG.thy @@ -1019,6 +1019,10 @@ lemma gets_the_wp': (* FIXME: should prefer this one in [wp] *) unfolding gets_the_def by (wpsimp wp: bind_wp_fwd gets_wp assert_opt_wp) +lemma gets_the_sp: + "\Q\ gets_the f \\rv s. f s = Some rv \ Q s\" + by (wpsimp wp: gets_the_wp') + lemma gets_map_wp: "\\s. f s p \ None \ Q (the (f s p)) s\ gets_map f p \Q\" unfolding gets_map_def diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 1c04ad3cfe..084bce10d6 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -76,10 +76,6 @@ lemma get_bound_notification_inv[simp]: apply (wp, simp) done -lemma gets_the_sp: - "\ Q \ gets_the f \\rv s. f s = Some rv \ Q s\" - by wpsimp - lemma gets_the_get_tcb_sp: "\ Q \ gets_the (get_tcb thread) \\t. Q and ko_at (TCB t) thread\" by wpsimp From 7bad797e6729a32d0432969b392c59e9894932a4 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 12:03:46 +1030 Subject: [PATCH 2/5] lib: add corres_gets_return to Corres_UL Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index c919ae8874..3af797da51 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -104,6 +104,17 @@ lemma corres_gets[simp, corres_no_simp]: (\ s s'. P s \ P' s' \ (s, s') \ sr \ r (a s) (b s'))" by (simp add: simpler_gets_def corres_singleton) +lemma corres_gets_return: + "corres_underlying sr nf nf' r P P' (gets f) (return v) + = (\s s'. ((s, s') \ sr \ P s \ P' s') \ r (f s) v)" + by (fastforce simp: corres_underlying_def gets_def get_def return_def bind_def) + +text \A safer non-rewrite version of @{thm corres_gets_return} \ +lemma corres_gets_return_trivial: + "(\s s'. \(s, s') \ sr; P s; P' s'\ \ r (f s) v) + \ corres_underlying sr nf nf' r P P' (gets f) (return v)" + by (fastforce simp: corres_gets_return) + lemma corres_throwError[simp, corres_no_simp]: "corres_underlying sr nf nf' r P P' (throwError a) (throwError b) = ((\s s'. P s \ P' s' \ (s, s') \ sr) \ r (Inl a) (Inl b))" From 72d1fd6898c020e807c9c2ea3ea54b6ad201dc62 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 12:05:45 +1030 Subject: [PATCH 3/5] lib/monads: add ovalid_if_lift2 to Reader_Option_VCG Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 770ec119d4..46bf04201a 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -140,6 +140,13 @@ lemma ovalid_if_split: "\ P \ \Q\ f \S\; \P \ \R\ g \S\ \ \ \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\" by simp +lemma ovalid_if_lift2: + "\P\ f \\rv s. (Q rv s \ X rv s) \ (\ Q rv s \ Y rv s)\ \ + \P\ f \\rv s. if Q rv s then X rv s else Y rv s\" + "\P\ f \\rv s. (Q' rv \ X rv s) \ (\ Q' rv \ Y rv s)\ \ + \P\ f \\rv. if Q' rv then X rv else Y rv\" + by (auto simp: ovalid_def split_def) + lemma reader_case_option_wp[wp]: "\\x. \P x\ m x \Q\; \P'\ m' \Q\\ \ \\s. (x = None \ P' s) \ (\y. x = Some y \ P y s)\ case_option m' m x \Q\" From c2687a401e5015d121f10598d7484655ae3b2c3e Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 12:09:58 +1030 Subject: [PATCH 4/5] lib: add some corres_underlying rules for assert_opt This also modifies the schematics variables of corres_assert_opt_assume Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index 3af797da51..2748d2a4cc 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -905,11 +905,24 @@ qed lemma corres_inst: "corres_underlying sr nf nf' r P P' f g \ corres_underlying sr nf nf' r P P' f g" . lemma corres_assert_opt_assume: - assumes "\x. P' = Some x \ corres_underlying sr nf nf' r P Q f (g x)" - assumes "\s. Q s \ P' \ None" - shows "corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g)" using assms - by (auto simp: bind_def assert_opt_def assert_def fail_def return_def - corres_underlying_def split: option.splits) + "\\x. opt = Some x \ corres_underlying sr nf nf' r P Q f (g x); \s. Q s \ opt \ None\ + \ corres_underlying sr nf nf' r P Q f (assert_opt opt >>= g)" + by (fastforce simp: bind_def return_def corres_underlying_def) + +lemma corres_assert_opt_assume': + "(\x. opt = Some x \ corres_underlying sr nf nf' r P Q f (g x)) + \ corres_underlying sr nf nf' r P (Q and K (opt \ None)) f (assert_opt opt >>= g)" + by (fastforce intro: corres_gen_asm2 stronger_corres_guard_imp corres_assert_opt_assume) + +lemma corres_assert_opt_assume_lhs: + "\\x. opt = Some x \ corres_underlying sr nf nf' r P Q (f x) g; \s. P s \ opt \ None\ + \ corres_underlying sr nf nf' r P Q (assert_opt opt >>= f) g" + by (fastforce simp: bind_def return_def corres_underlying_def) + +lemma corres_assert_opt_assume_lhs': + "(\x. opt = Some x \ corres_underlying sr nf nf' r P Q (f x) g) + \ corres_underlying sr nf nf' r (P and K (opt \ None)) Q (assert_opt opt >>= f) g" + by (fastforce intro: corres_gen_asm stronger_corres_guard_imp corres_assert_opt_assume_lhs) lemma corres_assert_opt[corres]: "r x x' \ From 460764a088c6409c5be30db99fd41c09891f6ce0 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 25 Feb 2025 11:12:02 +1030 Subject: [PATCH 5/5] 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)