Theory Shallow_Separation_Logic.Weakest_Precondition

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Weakest_Precondition
  imports Assertion_Language Triple Function_Contract "Shallow_Micro_Rust.Micro_Rust" Representability
begin
(*>*)

section‹A weakest precondition calculus›

(*<*)
context sepalg begin
(*>*)

text‹For solving goals related to Separation Logic triples, we introduce a Weakest Precondition (WP)
calculus: A means to convert questions about triples \<^term>‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ› into questions of
ordinary entailment \<^term>‹(⤏)›: For ∗‹fixed› \<^term>‹Γ›, \<^term>‹e›, \<^term>‹ψ› and \<^term>‹ρ›, we seek
to find an assertion ▩‹𝒲𝒫 Γ e ψ ρ› so that for any \<^term>‹φ›, \<^term>‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ› is equivalent to
 ▩‹φ ⤏ 𝒲𝒫 Γ e ψ ρ›.

First, we show that the weakest precondition exists, without explicitly computing it. This is a
consequence of basic triple properties and the abstract representability theorem proved in
🗏‹Representability.thy›.

Second, we develop rules for computing or approximating the weakest precondition for various language
constructs, proceeding on a case by case basis. Ultimately, this provides the
∗‹weakest precondition calculus› as a syntax-directed way of reasoning about triples.›

subsection‹Representability of sstriples›

text‹In this section, we show that for fixed \<^term>‹Γ›, \<^term>‹e›, \<^term>‹ψ› and \<^term>‹ρ›, the functor
 ▩‹Γ ; _ ⊢ e ⊣ ψ ⨝ ρ› is representable. The representing object is, by definition, the weakest
precondition for ▩‹Γ,e,ψ,ρ›.›

text‹First, the definition of the sstriple as a functor on assertions:›

definition sstriple_functor :: ‹('a, 'abort, 'i, 'o) striple_context ⇒
                  ('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression ⇒ ― ‹The expression to compute the WP for›
                  ('v ⇒ 'a assert) ⇒ ― ‹The success postcondition to compute the WP relative to›
                  ('r ⇒ 'a assert) ⇒ ― ‹The return postcondition to compute the WP relative to›
                  ('abort abort ⇒ 'a assert) ⇒
                  'a assert ⇒ bool› where
  ‹sstriple_functor Γ e ψ ρ θ ≡ (λφ. (Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ))›

text ‹From 🗏‹Representability.thy› we know that if the sstriple is representable, the representing
object must be given by \<^term>‹afunctor_sup›. Let's give this a name.

Note: It should not be necessary to unfold this definition! Instead, work purely with the
universal property ▩‹wp_sstriple_iff› established below to reduce properties of ▩‹𝒲𝒫›
to properties of sstriples. There are plenty of examples below.›

definition wp :: ‹('a, 'abort, 'i, 'o) striple_context ⇒
                  ('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression ⇒ ― ‹The expression to compute the WP for›
                  ('v ⇒ 'a assert) ⇒ ― ‹The success postcondition to compute the WP relative to›
                  ('r ⇒ 'a assert) ⇒ ― ‹The return postcondition to compute the WP relative to›
                  ('abort abort ⇒ 'a assert) ⇒
                  'a assert› ("𝒲𝒫") where
  ‹𝒲𝒫 Γ e ψ ρ θ ≡ afunctor_sup (sstriple_functor Γ e ψ ρ θ)›

text ‹Next, we check the representability conditions for the sstriple functor.
First, contravariance:›

lemma sstriple_contravariant:
  shows ‹is_contravariant (sstriple_functor Γ e ψ ρ θ)›
by (simp add: aentails_refl is_contravariant_def sstriple_consequence sstriple_functor_def)

text‹Second, sup-stability:›

lemma sstriple_is_sup_stable:
  shows ‹is_sup_stable (sstriple_functor Γ e ψ ρ θ)›
by (simp add: aentails_refl is_sup_stable_def sstriple_functor_def aentails_def asat_def
  sstriple_existsI')

text‹As a consequence of contravariance and sup-stability, we obtain the representability
of the sstriple functor.›

lemma sstriple_is_representable:
  shows ‹is_representable (sstriple_functor Γ e ψ ρ θ)›
using sstriple_is_sup_stable sstriple_contravariant afunctor_representability_criterion by blast

text‹Since we have already spelled out the representability candidate as ▩‹𝒲𝒫›, representability
can concretely be stated as follows:›

lemma sstriple_wp_iff:
  shows ‹(φ ⤏ 𝒲𝒫 Γ e ψ ρ θ) ⟷ (Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ)›
proof -
  from afunctor_representability_iff[OF sstriple_is_representable] have
     ‹(φ ⤏ 𝒲𝒫 Γ e ψ ρ θ) ⟷ sstriple_functor Γ e ψ ρ θ φ›
    by (force simp add: wp_def)
  from this show ?thesis
    unfolding sstriple_functor_def by simp
qed

lemma wp_sstriple_iff:
  shows ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ 𝒲𝒫 Γ e ψ ρ θ)›
proof -
  from afunctor_representability_iff[OF sstriple_is_representable] have
     ‹(φ ⤏ 𝒲𝒫 Γ e ψ ρ θ) ⟷ sstriple_functor Γ e ψ ρ θ φ›
    by (force simp add: wp_def)
  from this show ?thesis
    unfolding sstriple_functor_def by simp
qed

corollary wp_to_sstriple:
  assumes ‹φ ⤏ 𝒲𝒫 Γ e ψ ρ θ›
    shows ‹Γ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
  using assms wp_sstriple_iff by blast

corollary wp_is_precondition:
    shows ‹Γ ; 𝒲𝒫 Γ e ψ ρ θ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
  by (simp add: aentails_refl wp_to_sstriple)

corollary wp_is_weakest_precondition:
  assumes ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ e ψ ρ θ›
  using assms wp_sstriple_iff by blast

subsection‹Transporting general triple properties to WP-rules›

text ‹In this section, we demonstrate how to transport properties of sstriples to properties
of the weakest precondition. The proofs are purely formal and solely rely on the universal property
of the weakest precondition,  but not its concrete definition.›

text ‹First, the weakest precondition is always upwards closed:›
lemma ucincl_wp'I [ucincl_intros]:
  shows ‹ucincl (𝒲𝒫 Γ e φ ψ θ)›
  ―‹For sake of demonstration, we go through this proof in small steps:›
  ―‹First, we need to use a definition of \<^term>‹ucincl› which only uses ▩‹_ ⤏ φ›,
  but not ▩‹φ› itself. Luckily, ▩‹ucincl_alt'› provides such:›
  apply (simp add: ucincl_alt')
  ―‹Next, we apply the universal property of ▩‹𝒲𝒫› on both sides:›
  apply (simp add: sstriple_wp_iff)
  ―‹This has transformed the goal to an assertion about sstriples that we have proved before.›
  apply (simp flip: sstriple_upwards_closure)
  done

text ‹The weakest precondition is unchanged when passing to the upwards closure of the
post-conditions:›
lemma wp_upwards_closure:
  shows ‹(𝒲𝒫 Γ e ψ ρ θ) = 𝒲𝒫 Γ e ψ (λr. (ρ r ⋆ ⊤)) θ›
    and ‹(𝒲𝒫 Γ e ψ ρ θ) = 𝒲𝒫 Γ e (λr. (ψ r ⋆ ⊤)) ρ θ›
    and ‹(𝒲𝒫 Γ e ψ ρ θ) = 𝒲𝒫 Γ e ψ ρ (λa. θ a ⋆ ⊤)›
    and ‹(𝒲𝒫 Γ e ψ ρ θ) = 𝒲𝒫 Γ e (λr. (ψ r ⋆ ⊤)) (λr. (ρ r ⋆ ⊤)) (λa. (θ a ⋆ ⊤))›
  ―‹Here we use ▩‹aentails_yonedaI› to transform the goals into statements involving only
  ▩‹_ ⤏ 𝒲𝒫 _›. This allows us to apply the universal property ▩‹sstriple_wp_iff›, thereby
  reducing the statement to known upwards closure properties of sstriple:›
  by (auto
    intro!: aentails_yonedaI
    simp add: sstriple_wp_iff
    simp flip: sstriple_upwards_closure)

text‹The transitivity/consequence rule for triples yields a similar rule for weakest preconditions.
It allows us to strengthen preconditions and weaken postconditions:›

lemma wp_consequence:
  assumes ‹φ' ⤏ 𝒲𝒫 Γ e ψ' ρ' θ'›
      and ‹φ ⤏ φ'›
      and ‹⋀r. ψ' r ⤏ ψ r›
      and ‹⋀r. ρ' r ⤏ ρ r›
      and ‹⋀r. θ' r ⤏ θ r›
    shows ‹φ ⤏ 𝒲𝒫 Γ e ψ ρ θ›
  using assms sstriple_consequence wp_is_weakest_precondition wp_to_sstriple by metis

text‹Using \<^term>‹wp_striple_iff›, we can transport some frame rules into the weakest precondition setting:›

theorem wp_frame_ruleI:
  assumes ‹φ' ⤏ 𝒲𝒫 Γ e (λr. (φ' ↠ φ) ↠ ψ r) (λr. (φ' ↠ φ) ↠ ρ r) (λr. (φ' ↠ φ) ↠ θ r)›
      and ‹φ ⤏ φ' ⋆ (φ' ↠ φ)›
    shows ‹φ ⤏ 𝒲𝒫 Γ e ψ ρ θ›
using assms sstriple_frame_ruleI' wp_sstriple_iff by blast

theorem wp_frame_rule_asepconj_multi_singleI:
  assumes ‹ξ (lst ! i) ⋆ φ ⤏
              𝒲𝒫 Γ e (λr. ⋆⋆{# ξ ∷ drop_nth i lst #} ↠ ψ r)
                      (λr. ⋆⋆{# ξ ∷ drop_nth i lst #} ↠ ρ r)
                      (λr. ⋆⋆{# ξ ∷ drop_nth i lst #} ↠ θ r)›
      and ‹ucincl φ›
      and ‹i < length lst›
    shows ‹⋆⋆{# ξ ∷ lst #} ⋆ φ ⤏ 𝒲𝒫 Γ e ψ ρ θ›
using assms sstriple_frame_rule_asepconj_multi_singleI' wp_sstriple_iff by blast

lemma sstriple_pure_to_wp':
    notes asat_simp [simp]
      and asepconj_simp [simp]
  assumes ‹ucincl (ψ x)›
      and ‹Γ; ⊤ ⊢ e ⊣ (λv. ⟨v = x⟩) ⨝ ⊥ ⨝ ⊥›
    shows ‹ψ x ⤏ 𝒲𝒫 Γ e ψ ρ θ›
proof -
  from assms have ‹Γ; ⊤ ⋆ ψ x ⊢ e ⊣ (λv. ⟨v = x⟩ ⋆ ψ x) ⨝ (λ_. ⊥ ⋆ ψ x) ⨝ (λ_. ⊥ ⋆ ψ x)›
    by (intro sstriple_frame_rule, auto simp add: bot_fun_def)
  from assms and this show ‹ψ x ⤏ 𝒲𝒫 Γ e ψ ρ θ›
    by (intro wp_is_weakest_precondition; clarsimp)
      (rule sstriple_consequence, auto simp add: aentails_def)
qed

text ‹This is a useful lemma for transporting Hoare triple facts of straight-line code (guaranteed
not to return) directly into WP facts using a standard pattern.›
lemma sstriple_straightline_to_wp:
  notes asepconj_simp [simp]
  assumes ‹Γ; pre ⊢ e ⊣ post ⨝ ⊥ ⨝ ⊥›
  shows ‹pre ⋆ (⨅v. post v ↠ ψ v) ⤏ 𝒲𝒫 Γ e ψ ρ θ›
proof -
  from assms have ‹Γ; pre ⋆ (⨅v. post v ↠ ψ v) ⊢ e ⊣
                          (λv. post v ⋆ (⨅v'. post v' ↠ ψ v'))
                       ⨝ (λ_. ⊥ ⋆ (⨅v'. post v' ↠ ψ v'))
                       ⨝ (λ_. ⊥ ⋆ (⨅v'. post v' ↠ ψ v'))›
    by (intro sstriple_frame_rule; clarsimp simp add: bot_fun_def ucincl_intros intro!:ucincl_Int)
  moreover have ‹⋀r. post r ⋆ (⋂v'. post v' ↠ ψ v') ⤏ ψ r›
    by (metis (no_types, lifting) aentails_refl aforall_entailsL asepconj_comm awand_adjoint)
  ultimately have ‹Γ; pre ⋆ (⨅v. post v ↠ ψ v) ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    by (simp add: aentails_refl local.bot_aentails_all local.sstriple_consequence)
  from this and assms show ‹pre ⋆ (⨅v. post v ↠ ψ v) ⤏ 𝒲𝒫 Γ e ψ ρ θ›
    using wp_sstriple_iff by blast
qed

lemma sstriple_straightline_to_wp_with_abort:
    notes asepconj_simp [simp]
  assumes ‹Γ; pre ⊢ e ⊣ post ⨝ ⊥ ⨝ ab›
    shows ‹pre ⋆ ((⨅v. post v ↠ ψ v)⊓(⨅v. ab v ↠ θ v)) ⤏ 𝒲𝒫 Γ e ψ ρ θ›
proof -
  let ?frame = ‹((⨅v. post v ↠ ψ v)⊓(⨅v. ab v ↠ θ v))›
  from assms have A: ‹Γ; pre ⋆ ?frame ⊢ e ⊣
                          (λv. post v ⋆ ?frame)
                       ⨝ (λ_. ⊥ ⋆ ?frame)
                       ⨝ (λr. ab r ⋆ ?frame)›
    by (intro sstriple_frame_rule; clarsimp simp add: bot_fun_def ucincl_intros intro!:ucincl_Int)
  moreover have B: ‹⋀r. ab r ⋆ ?frame ⤏ θ r›
    by (metis (no_types, lifting) aentails_refl_eq inf_commute aentails_fold_def
      aentails_inter_weaken2 aforall_entailsL asepconj_mono3)
  moreover have C: ‹⋀r. post r ⋆ ?frame ⤏ ψ r›
    by (metis (no_types, lifting) aentails_refl_eq aentails_fold_def
      aentails_inter_weaken2 aforall_entailsL asepconj_mono3)
  have ‹Γ; pre ⋆ ?frame ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    using sstriple_consequence [OF A]
    by (simp add: B C aentails_refl local.bot_aentails_all)
  from this and assms show ‹pre ⋆ ?frame ⤏ 𝒲𝒫 Γ e ψ ρ θ›
    using wp_sstriple_iff by blast
qed

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_to_wp_frame:
  assumes ‹Γ; pre ⊢ e ⊣ post
                        ⨝ (λr. (⨅v'. post v' ↠ ψ v') ↠ ρ r)
                        ⨝ (λr. (⨅v'. post v' ↠ ψ v') ↠ θ r)›
    shows ‹pre ⋆ (⨅v. post v ↠ ψ v) ⤏ 𝒲𝒫 Γ e ψ ρ θ›
proof -
  from assms have ‹Γ; pre ⋆ (⨅v. post v ↠ ψ v) ⊢ e ⊣ (λv. post v ⋆ (⨅v'. post v' ↠ ψ v')) ⨝
                        (λr. ((⨅v'. post v' ↠ ψ v') ↠ ρ r) ⋆ (⨅v'. post v' ↠ ψ v')) ⨝
                        (λr. ((⨅v'. post v' ↠ ψ v') ↠ θ r) ⋆ (⨅v'. post v' ↠ ψ v'))›
    by (intro sstriple_frame_rule; clarsimp simp add: ucincl_intros intro!: ucincl_Int)
  moreover have ‹pre ⋆ (⋂v. post v ↠ ψ v) ⤏ pre ⋆ (⋂v. post v ↠ ψ v)›
    by (intro aentails_refl)
  moreover have ‹⋀r. post r ⋆ (⋂v'. post v' ↠ ψ v') ⤏ ψ r›
    by (meson aentails_refl local.aentails_forward local.aforall_entailsL local.asepconj_mono)
  moreover have ‹⋀r. (⋂v'. post v' ↠ ψ v') ↠ ρ r ⋆ (⋂v'. post v' ↠ ψ v') ⤏ ρ r›
    by (blast intro: awand_mp)
  moreover have ‹⋀r. (⋂v'. post v' ↠ ψ v') ↠ θ r ⋆ (⋂v'. post v' ↠ ψ v') ⤏ θ r›
    by (blast intro: awand_mp)
  ultimately have ‹Γ; pre ⋆ (⨅v. post v ↠ ψ v) ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    by (rule sstriple_consequence)
  then show ‹pre ⋆ (⨅v. post v ↠ ψ v) ⤏ 𝒲𝒫 Γ e ψ ρ θ›
    using assms by (auto intro!: wp_is_weakest_precondition ucincl_asepconj ucincl_Int ucincl_awand)
qed

subsection‹Local axioms for Micro Rust expressions›

text‹In this section, we reason on a case-by-case basis, computing the Weakest Precondition for the
expressions of Core Micro Rust.  Note that, as many expressions are defined as abbreviations,
written in terms of a small set of core expressions that others elaborate into, we need only
consider this core set here.

First, we introduce some named collections of theorem that will be useful later, when defining
automation tactics.  We have theorem collections relating to simplification and introduction rules
for the Weakest Precondition calculus:›

named_theorems micro_rust_wp_simps
named_theorems micro_rust_wp_elims
named_theorems micro_rust_wp_intros
named_theorems micro_rust_wp_case_splits

text‹Introduction rules introducing schematic variables. Those should be attempted after
destructing quantified assumptions, as only then the schematic may depend on the quantifiers
in the assumptions:›
named_theorems micro_rust_wp_ex_intros

lemma wp_pause:
    notes asepconj_simp [simp]
  assumes ‹⋀r. ucincl (ψ r)›
    shows ‹𝒲𝒫 Γ ⟦ 𝗒𝗂𝖾𝗅𝖽 ⟧ ψ ρ θ = ψ ()›
  using assms by (auto intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_pause')

text‹The following is deliberately not marked as ▩‹micro_rust_wp_intros› so automation does not
silently go over it.›
―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma wp_pauseI:
  assumes ‹⋀r. ucincl (ψ r)›
      and ‹φ ⤏ ψ ()›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ 𝗒𝗂𝖾𝗅𝖽 ⟧ ψ ρ θ›
using assms by (simp add: wp_pause)

lemma wp_log:
    notes asepconj_simp [simp]
  assumes ‹⋀r. ucincl (ψ r)›
    shows ‹𝒲𝒫 Γ ⟦ 𝗅𝗈𝗀 ⟪p⟫ ⟪l⟫ ⟧ ψ ρ θ = ψ ()›
using assms by (auto intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_log')

lemma wp_logI [micro_rust_wp_intros]:
  assumes ‹⋀r. ucincl (ψ r)›
      and ‹φ ⤏ ψ ()›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ 𝗅𝗈𝗀 ⟪p⟫ ⟪l⟫ ⟧ ψ ρ θ›
using assms by (simp add: wp_log)

lemma wp_fatalI [micro_rust_wp_intros]:
    notes asepconj_simp [simp]
  assumes ‹is_aborting_striple_context Γ›
      and ‹⋀r. ucincl (ψ r)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ fatal!(msg) ⟧ ψ ρ θ›
  using assms by (auto intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_fatal)

lemma wp_literal [micro_rust_wp_simps]:
    notes asepconj_simp [simp]
  assumes ‹⋀r. ucincl (ψ r)›
    shows ‹𝒲𝒫 Γ (↑v) ψ ρ  θ = ψ v›
  using assms by (auto intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_literal)

lemma wp_literal_coreI:
  assumes ‹⋀r. ucincl (ψ r)›
      and ‹φ ⤏ ψ v›
    shows ‹φ ⤏ 𝒲𝒫 Γ (↑v) ψ ρ θ›
using assms by (subst wp_literal)

lemma wp_literalI[micro_rust_wp_intros]:
  assumes ‹φ ⤏ ψ v ⋆ ⊤›
    shows ‹φ ⤏ 𝒲𝒫 Γ (↑v) ψ ρ θ›
  by (simp add: assms local.sstriple_literal local.sstriple_wp_iff)

text‹As immediate corollaries of the result above we have analogous results for all of our literal
values for Core Micro Rust:›
corollary wp_core_rust_literals [micro_rust_wp_simps]:
  shows ‹⋀ψ. (⋀r. ucincl (ρ r)) ⟹ (⋀s. ucincl (ψ s)) ⟹ 𝒲𝒫 Γ `True ψ ρ  θ= ψ True›
    and ‹⋀ψ. (⋀r. ucincl (ρ r)) ⟹ (⋀s. ucincl (ψ s)) ⟹ 𝒲𝒫 Γ `False ψ ρ  θ= ψ False›
    and ‹⋀ψ. (⋀r. ucincl (ρ r)) ⟹ (⋀s. ucincl (ψ s)) ⟹ 𝒲𝒫 Γ `None ψ ρ  θ= ψ None›
    and ‹⋀x ψ. (⋀r. ucincl (ρ r)) ⟹ (⋀s. ucincl (ψ s)) ⟹ 𝒲𝒫 Γ (`Some (↑x)) ψ ρ  θ= ψ (Some x)›
by (auto simp add: true_def false_def none_def some_def wp_literal micro_rust_simps)

lemma wp_abort [micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ (abort a) ψ ρ θ = θ a ⋆ UNIV›
  by (clarsimp intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_abort)

corollary wp_panic [micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ panic!(m) ⟧ ψ ρ θ = θ (Panic m) ⋆ UNIV›
  by (intro wp_abort)

lemma wp_abortI [micro_rust_wp_intros]:
  assumes ‹φ ⤏ θ a ⋆ UNIV›
    shows ‹φ ⤏ 𝒲𝒫 Γ (abort a) ψ ρ θ›
using assms by (subst wp_abort)

lemma wp_panicI [micro_rust_wp_intros]:
  assumes ‹φ ⤏ θ (Panic m) ⋆ UNIV›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ panic!(m) ⟧ ψ ρ θ›
using assms by (subst wp_panic)

lemma wp_return [micro_rust_wp_simps]:
    shows ‹𝒲𝒫 Γ ⟦ return v; ⟧ ψ ρ θ = ρ v ⋆ ⊤›
by (auto intro!: aentails_yonedaI simp add: sstriple_wp_iff sstriple_return)

lemma wp_returnI [micro_rust_wp_intros]:
  assumes ‹φ ⤏ ρ v ⋆ ⊤›
  shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ return v; ⟧ ψ ρ θ›
using assms by (simp add: wp_return)

lemma wp_assert [micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ assert!(x) ⟧ ψ ρ θ = (⟨x⟩ ↠ (UNIV ⋆ ψ ())) ⊓ (⟨¬x⟩ ↠ (UNIV ⋆ θ AssertionFailed))›
  apply (intro aentails_yonedaI)
  apply (clarsimp simp add: sstriple_wp_iff aentails_simp sstriple_assert apure_def asepconj_simp
    bot_aentails_all)
  apply (meson aentails_refl_eq aentails_trans aentails_top_R' aentails_uc'
    ucincl_UNIV ucincl_asepconjL)
  done

lemma wp_assert_eq [micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ assert_eq!(x, y) ⟧ ψ ρ θ =
     (⟨x=y⟩ ↠ (UNIV ⋆ ψ ())) ⊓ (⟨x≠y⟩ ↠ (UNIV ⋆ θ AssertionFailed))›
  by (clarsimp simp add: wp_assert[simplified assert_def micro_rust_simps]
    assert_eq_def assert_eq_val_def micro_rust_simps)

thm aentails_frulify_pure

lemma wp_assertI[micro_rust_wp_intros]:
    notes aentails_intro [intro]
  assumes ‹φ ⤏ (⟨x⟩ ⋆ ψ ())›
  shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ assert!(x) ⟧ ψ ρ θ›
proof -
  have ‹⟨x⟩ ⋆ ψ () ⋆ ⟨x⟩ ⤏ UNIV ⋆ ψ ()›
    by (simp add: aentails_refl apure_entailsL' asepconj_comm asepconj_pure2)
  moreover
  have ‹⟨x⟩ ⋆ ψ () ⋆ ⟨¬ x⟩ ⤏ UNIV ⋆ θ AssertionFailed›
    by (metis local.aentails_is_sat local.is_sat_pure local.is_sat_splitE)
  ultimately show ?thesis
    using aentails_trans[OF assms]
    by (simp add: wp_assert aentails_intI asepconj_assoc awand_adjoint)
qed

lemma wp_assert_eqI[micro_rust_wp_intros]:
    notes aentails_intro[intro]
  assumes ‹φ ⤏ (⟨x=y⟩ ⋆ ψ ())›
  shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ assert_eq!(x,y) ⟧ ψ ρ θ›
  using assms by (clarsimp intro!: wp_assertI[simplified assert_def micro_rust_simps]
     simp add: assert_eq_def assert_eq_val_def micro_rust_simps)

lemma wp_assert_neI[micro_rust_wp_intros]:
    notes aentails_intro[intro]
  assumes ‹φ ⤏ (⟨x≠y⟩ ⋆ ψ ())›
  shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ assert_ne!(x,y) ⟧ ψ ρ θ›
  using assms by (clarsimp intro!: wp_assertI[simplified assert_def micro_rust_simps]
     simp add: assert_ne_def assert_ne_val_def micro_rust_simps)

lemma wp_bind_core:
  shows ‹𝒲𝒫 Γ e (λr. 𝒲𝒫 Γ (f r) ξ ρ θ) ρ θ ⤏ 𝒲𝒫 Γ ⟦ let v = ε‹e›; ε‹f v› ⟧ ξ ρ θ›
  by (meson sstriple_bindI wp_is_precondition wp_sstriple_iff)

lemma aentails_cong_only_rhs:
  assumes ‹ψ = ψ'›
    shows ‹(φ ⤏ ψ) ⟷ (φ ⤏ ψ')›
using assms by auto

lemma wp_bindI [micro_rust_wp_intros]:
    notes aentails_intro [intro]
    fixes e :: ‹('a, 'b, 'c, 'abort, 'i prompt, 'o prompt_output) expression›
  assumes ‹φ ⤏ 𝒲𝒫 Γ e (λr. 𝒲𝒫 Γ (f r) ξ ρ θ) ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ let v = ε‹e›; ε‹f v› ⟧  ξ ρ θ›
using assms by (blast intro: wp_bind_core)

corollary wp_sequence_core:
  shows ‹𝒲𝒫 Γ e (λx. 𝒲𝒫 Γ f ξ ρ θ) ρ θ ⤏ 𝒲𝒫 Γ (sequence e f) ξ ρ θ›
by (auto simp add: sequence_def intro!: wp_bind_core)

lemma wp_sequenceI [micro_rust_wp_intros]:
    notes aentails_intro[intro]
  assumes ‹φ ⤏ 𝒲𝒫 Γ e (λx. 𝒲𝒫 Γ f ξ ρ θ) ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (sequence e f) ξ ρ θ›
using assms wp_sequence_core by blast

lemma wp_two_armed_conditional:
  shows ‹𝒲𝒫 Γ ⟦ if x { ε‹t› } else { ε‹f› } ⟧ ψ ρ θ
     = (if x then 𝒲𝒫 Γ t ψ ρ θ else 𝒲𝒫 Γ f ψ ρ θ)›
by (cases x) (auto simp add: micro_rust_simps)

lemma wp_two_armed_conditionalI[micro_rust_wp_case_splits]:
  assumes ‹x ⟹ φ ⤏ 𝒲𝒫 Γ t ψ ρ θ›
      and ‹¬x ⟹ φ ⤏ 𝒲𝒫 Γ f ψ ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ if x { ε‹t› } else { ε‹f› }⟧ ψ ρ θ›
by (simp add: assms wp_two_armed_conditional)

corollary wp_one_armed_conditional:
  assumes ‹⋀s. ucincl (ψ s)›
  shows ‹𝒲𝒫 Γ ⟦ if x { ε‹t› } ⟧ ψ ρ θ = (if x then 𝒲𝒫 Γ t ψ ρ θ else ψ ())›
using assms by (simp add: micro_rust_wp_simps wp_two_armed_conditional)

lemma wp_one_armed_conditionalI[micro_rust_wp_case_splits]:
  assumes ‹x ⟹ φ ⤏ 𝒲𝒫 Γ t ψ ρ θ›
      and ‹¬x ⟹ φ ⤏ ψ () ⋆ ⊤›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ if x { ε‹t› } ⟧ ψ ρ θ›
  using assms by (simp add: wp_literalI wp_two_armed_conditional)

lemma wp_two_armed_conditional_thenI:
  assumes ‹x›
      and ‹φ ⤏ 𝒲𝒫 Γ t ψ ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ if x { ε‹t› } else { ε‹f› }⟧ ψ ρ θ›
  by (simp add: assms wp_two_armed_conditional)

lemma wp_two_armed_conditional_elseI:
  assumes ‹¬x›
      and ‹φ ⤏ 𝒲𝒫 Γ f ψ ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ if x { ε‹t› } else { ε‹f› }⟧ ψ ρ θ›
  by (simp add: assms wp_two_armed_conditional)

―‹TODO: This is not uniform with the treatment of conditionals
which are discharged using ▩‹micro_rust_wp_intros› rather than
▩‹micro_rust_wp_simps›.›
lemma wp_option_cases: (* [micro_rust_wp_simps]: *)
  shows ‹𝒲𝒫 Γ ⟦ match x { None ⇒ ε‹nn›, Some(s) ⇒ ε‹sm s› } ⟧ ψ ρ θ =
          (case x of
             None   ⇒ 𝒲𝒫 Γ nn ψ ρ θ
           | Some s ⇒ 𝒲𝒫 Γ (sm s) ψ ρ θ)›
by (rule asat_semequivI; cases ‹x›) (auto simp add: micro_rust_simps)

lemma wp_option_cases_none[micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ match None { Some(s) ⇒ ε‹sm s›, None ⇒ ε‹nn› } ⟧ ψ ρ θ = 𝒲𝒫 Γ nn ψ ρ θ›
  by (simp add: wp_option_cases)

lemma wp_option_cases_some[micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ match ⟪Some s⟫ { Some(s) ⇒ ε‹sm s›, None ⇒ ε‹nn› } ⟧ ψ ρ θ = 𝒲𝒫 Γ (sm s) ψ ρ θ›
  by (simp add: wp_option_cases)

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma wp_option_casesI:
  assumes ‹x = None ⟹ φ ⤏ 𝒲𝒫 Γ nn ψ ρ θ›
     and ‹⋀s. x = Some s ⟹ φ ⤏ 𝒲𝒫 Γ (sm s) ψ ρ θ›
   shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ match x { None ⇒ ε‹nn›, Some(s) ⇒ ε‹sm s› } ⟧ ψ ρ θ›
  using assms by (clarsimp simp add: wp_option_cases split!: option.splits)

lemma wp_result_cases: (* [micro_rust_wp_simps]: *)
  shows ‹𝒲𝒫 Γ ⟦ match x { Ok(k) ⇒ ε‹ok k›, Err(e) ⇒ ε‹err e› } ⟧ ψ ρ θ =
           (case x of
              Ok k  ⇒ 𝒲𝒫 Γ (ok k) ψ ρ θ
            | Err e ⇒ 𝒲𝒫 Γ (err e) ψ ρ θ)›
by (rule asat_semequivI; cases ‹x›) (auto simp add:micro_rust_simps)

lemma wp_result_cases_ok[micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ match ⟪Ok k⟫ { Ok(k) ⇒ ε‹ok k›, Err(e) ⇒ ε‹err e› } ⟧ ψ ρ θ = 𝒲𝒫 Γ (ok k) ψ ρ θ›
  by (simp add: wp_result_cases)

lemma wp_result_cases_err[micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ ⟦ match ⟪Err e⟫ { Ok(k) ⇒ ε‹ok k›, Err(e) ⇒ ε‹err e› } ⟧ ψ ρ θ = 𝒲𝒫 Γ (err e) ψ ρ θ›
  by (simp add: wp_result_cases)

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma wp_result_casesI:
  assumes ‹⋀k. x = Ok k ⟹ φ ⤏ 𝒲𝒫 Γ (ok k) ψ ρ θ›
     and ‹⋀e. x = Err e ⟹ φ ⤏ 𝒲𝒫 Γ (err e) ψ ρ θ›
   shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ match x { Ok(k) ⇒ ε‹ok k›, Err(e) ⇒ ε‹err e› } ⟧ ψ ρ θ›
  using assms by (clarsimp simp add: wp_result_cases split!: result.splits)

lemma wp_get:
    notes asat_simp [simp]
  assumes ‹ucincl (has f v)›
      and ‹⋀x. ucincl (ψ x)›
    shows ‹has f v ⋆ (has f v ↠ ψ v) ⤏ 𝒲𝒫 Γ (get f) ψ ρ θ›
proof -
  have ‹has f v ⋆ (⨅x. (⟨x=v⟩ ⋆ has f v) ↠ ψ x) ⤏ 𝒲𝒫 Γ (get f) ψ ρ θ›
    using assms by (auto intro!: sstriple_straightline_to_wp sstriple_getI)
  moreover from assms have ‹has f v ⋆ (has f v ↠ ψ v) ⤏ has f v ⋆ (⨅x. (⟨x=v⟩ ⋆ has f v) ↠ ψ x)›
    by (clarsimp simp add: aentails_def elim!: awandE asepconjE) (force intro: asepconjI awandI)
  ultimately show ?thesis
    using aentails_trans by force
qed

lemma wp_put:
  assumes ‹⋀x. x ⊨ has f v ⟹ g x ⊨ has f v'›
      and ‹⋀x y. x♯y ⟹ x ⊨ has f v ⟹ g (x+y) = g x + y ∧ g x ♯ y›
      and ‹ucincl (has f v)›
      and ‹⋀x. ucincl (ψ x)›
    shows ‹has f v ⋆ (has f v' ↠ ψ ()) ⤏ 𝒲𝒫 Γ (put g) ψ ρ θ›
proof -
  from assms have ‹has f v ⋆ (⨅u. has f v' ↠ ψ u) ⤏ 𝒲𝒫 Γ (put g) ψ ρ θ›
    by (auto intro!: sstriple_straightline_to_wp sstriple_putI)
  moreover from assms have ‹has f v ⋆ (has f v' ↠ ψ ()) ⤏ has f v ⋆ (⨅u. has f v' ↠ ψ u)›
    by (auto simp add: aentails_def elim!: asepconjE awandE intro!: asepconjI awandI)
  ultimately show ?thesis
    using aentails_trans by force
qed

lemma wp_getI [micro_rust_wp_intros]:
  assumes ‹ucincl (has f v)›
      and ‹⋀x. ucincl (ψ x)›
      and  ‹φ ⤏ has f v ⋆ (has f v ↠ ψ v)›
    shows ‹φ ⤏ 𝒲𝒫 Γ (get f) ψ ρ θ›
using assms by (force intro: aentails_trans' wp_get)

lemma wp_putI:
  assumes ‹⋀x. x ⊨ has f v ⟹ g x ⊨ has f v'›
      and ‹⋀x y. x♯y ⟹ x ⊨ has f v ⟹ g (x+y) = g x + y ∧ g x ♯ y›
      and ‹ucincl (has f v)›
      and ‹⋀x. ucincl (ψ x)›
      and ‹φ ⤏ has f v ⋆ (has f v' ↠ ψ ())›
    shows ‹φ ⤏ 𝒲𝒫 Γ (put g) ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_put, auto)

lemma wp_fun [micro_rust_wp_simps]:
  shows ‹𝒲𝒫 Γ (f⟨⟩) φ ρ θ = 𝒲𝒫 Γ (call f) φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f1(a0) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f1 a0› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f2(a0, a1) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f2 a0 a1› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f3(a0, a1, a2) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f3 a0 a1 a2› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f4(a0, a1, a2, a3) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f4 a0 a1 a2 a3› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f5(a0, a1, a2, a3, a4) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f5 a0 a1 a2 a3 a4› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f6(a0, a1, a2, a3, a4, a5) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f6 a0 a1 a2 a3 a4 a5› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f7(a0, a1, a2, a3, a4, a5, a6) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f7 a0 a1 a2 a3 a4 a5 a6› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f8(a0, a1, a2, a3, a4, a5, a6, a7) ⟧ φ ρ θ = 𝒲𝒫 Γ ⟦ ε‹f8 a0 a1 a2 a3 a4 a5 a6 a7› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f9(a0, a1, a2, a3, a4, a5, a6, a7, a8) ⟧ φ ρ θ =
           𝒲𝒫 Γ ⟦ ε‹f9 a0 a1 a2 a3 a4 a5 a6 a7 a8› () ⟧ φ ρ θ›
    and ‹𝒲𝒫 Γ ⟦ f10(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9) ⟧ φ ρ θ =
           𝒲𝒫 Γ ⟦ ε‹f10 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9› () ⟧ φ ρ θ›
by (simp only:micro_rust_simps)+

text‹This rule is useful for unfolding the definition of a called function and reasoning about it
directly.›
lemma wp_call_function_body:
  shows ‹𝒲𝒫 Γ f ψ ψ θ ⤏ 𝒲𝒫 Γ (call (FunctionBody f)) ψ ρ θ›
  by (clarsimp intro!: aentails_yonedaI sstriple_callI simp add: sstriple_wp_iff
    wp_is_precondition)

― ‹NB We don't mark this as an introduction rule because for some functions
we want to invoke a function contract rather than unfolding their definition.›
corollary wp_call_function_bodyI:
    notes aentails_intro [intro]
  assumes ‹φ ⤏ 𝒲𝒫 Γ (function_body f) ψ ψ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  using assms wp_call_function_body by (cases f; clarsimp) blast

―‹The following formulation is useful in the presence of a list of definitions for functions
to be inlined, one of which will discharge the first generated assumption.›
corollary wp_call_inlineI:
  assumes ‹f ≡ FunctionBody b›
      and ‹φ ⤏ 𝒲𝒫 Γ b ψ ψ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  using assms by (clarsimp intro!: wp_call_function_bodyI)

corollary wp_call_inline'I:
  assumes ‹f ≡ g›
      and ‹φ ⤏ 𝒲𝒫 Γ (call g) ψ ρ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  using assms by clarsimp

corollary wp_call_function_bodyI2 [micro_rust_wp_intros]:
    notes aentails_intro [intro]
  assumes ‹φ ⤏ 𝒲𝒫 Γ f ψ ψ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call (FunctionBody f)) ψ ρ θ›
using assms wp_call_function_body by (cases f; clarsimp) blast

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma wp_satisfies_function_contract_direct:
    notes asat_simp [simp]
  assumes ‹Γ; f ⊨⇩F 𝒞›
      and pre: ‹φ ⤏ function_contract_pre 𝒞›
      and post: ‹⋀r. function_contract_post 𝒞 r ⤏ ψ r›
      and abort: ‹⋀r. function_contract_abort 𝒞 r ⤏ θ r›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
proof -
  from assms have ‹Γ; function_contract_pre 𝒞 ⊢ call f ⊣ function_contract_post 𝒞 ⨝ ρ ⨝ function_contract_abort 𝒞›
    by (auto elim!: satisfies_function_contractE)
  note X = this
  have ‹Γ; φ ⊢ call f ⊣ ψ ⨝ ρ ⨝ θ›
    using sstriple_consequence[OF X pre post aentails_refl abort] by simp
  from this show ?thesis
    by (simp add: wp_sstriple_iff)
qed

lemma wp_satisfies_function_contract:
  assumes ‹Γ; f ⊨⇩F 𝒞›
  shows ‹function_contract_pre 𝒞 ⋆ ((⨅r. function_contract_post 𝒞 r ↠ ψ r)
                                   ⊓(⨅r. function_contract_abort 𝒞 r ↠ θ r))
           ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  using assms by (elim satisfies_function_contractE,
   intro sstriple_straightline_to_wp_with_abort, auto)

lemma wp_call_with_abortI:
  assumes A: ‹Γ; f ⊨⇩F 𝒞›
      and B: ‹φ ⤏ function_contract_pre 𝒞 ⋆
           ((⨅r. function_contract_post 𝒞 r ↠ ψ r)
           ⊓(⨅r. function_contract_abort 𝒞 r ↠ θ r))›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  by (intro aentails_trans[OF _ wp_satisfies_function_contract[OF A]], simp add: B)

lemma wp_callI:
  assumes ‹Γ; f ⊨⇩F 𝒞›
      and ‹function_contract_abort 𝒞 = ⊥›
      and ‹φ ⤏ function_contract_pre 𝒞 ⋆ (⨅r. function_contract_post 𝒞 r ↠ ψ r)›
    shows ‹φ ⤏ 𝒲𝒫 Γ (call f) ψ ρ θ›
  using assms by - (intro wp_call_with_abortI, assumption, simp add: awand_bot)

lemma wp_funliteral:
  assumes ‹⋀r. ucincl (ψ r)›
    shows ‹𝒲𝒫 Γ ⟦ ⟪f1⟫⇩1 (v0) ⟧ ψ ρ θ = ψ (f1 v0)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f2⟫⇩2 (v0, v1) ⟧ ψ ρ θ = ψ (f2 v0 v1)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f3⟫⇩3 (v0, v1, v2) ⟧ ψ ρ θ = ψ (f3 v0 v1 v2)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f4⟫⇩4 (v0, v1, v2, v3) ⟧ ψ ρ θ = ψ (f4 v0 v1 v2 v3)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f5⟫⇩5 (v0, v1, v2, v3, v4) ⟧ ψ ρ θ = ψ (f5 v0 v1 v2 v3 v4)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f6⟫⇩6 (v0, v1, v2, v3, v4, v5) ⟧ ψ ρ θ = ψ (f6 v0 v1 v2 v3 v4 v5)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f7⟫⇩7 (v0, v1, v2, v3, v4, v5, v6) ⟧ ψ ρ θ = ψ (f7 v0 v1 v2 v3 v4 v5 v6)›
      and ‹𝒲𝒫 Γ ⟦ ⟪f8⟫⇩8 (v0, v1, v2, v3, v4, v5, v6, v7) ⟧ ψ ρ θ = ψ (f8 v0 v1 v2 v3 v4 v5 v6 v7)›
  using assms by (clarsimp intro!: aentails_yonedaI simp add: sstriple_wp_iff
    sstriple_call_funliteral asepconj_simp)+

lemma wp_range_new [micro_rust_wp_simps]:
  assumes ‹⋀r. ucincl (φ r)›
    shows ‹𝒲𝒫 Γ (⟨↑b…↑e⟩) φ ρ θ = φ (make_range b e)›
using assms by (clarsimp simp add: range_new_def wp_funliteral)

lemma wp_op_eq [micro_rust_wp_simps]:
  assumes ‹⋀r. ucincl (ψ r)›
      and ‹⋀r. ucincl (ρ r)›
    shows ‹𝒲𝒫 Γ ⟦ ⟪λa b. a=b⟫⇩2(e,f) ⟧ ψ ρ θ = ψ (e = f)›
using assms by (clarsimp simp add: wp_funliteral)

lemma wp_op_eqs [micro_rust_wp_simps]:
  assumes ‹⋀r. ucincl (ψ r)›
      and ‹⋀r. ucincl (ρ r)›
    shows ‹𝒲𝒫 Γ ⟦ e == f ⟧ ψ ρ θ = ψ (e = f)›
using assms by (clarsimp simp add: urust_eq_def micro_rust_wp_simps micro_rust_simps)

lemma wp_word_add_no_wrap [micro_rust_wp_intros]:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x+y))›
    shows ‹⟨unat x + unat y < 2^LENGTH('l)⟩ ⋆ ψ (x + y) ⤏ 𝒲𝒫 Γ ⟦ x + y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨(unat x) + (unat y) < 2^(LENGTH('l))⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have I: ‹Γ ; ?asm ⊢ ⟦ x + y ⟧ ⊣ (λr. ⟨r = x + y⟩ ⋆ ψ (x+y)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return; simp add: sstriple_word_add_no_wrapI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x + y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_add_no_wrapI [micro_rust_wp_intros]:
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x + y))›
      and ‹φ ⤏ ⟨unat x + unat y < 2^LENGTH('l)⟩ ⋆ ψ (x + y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x + y ⟧ ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_word_add_no_wrap, auto)

lemma wp_word_mul_no_wrap [micro_rust_wp_intros]:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x*y))›
    shows ‹⟨unat x * unat y < 2^LENGTH('l)⟩ ⋆ ψ (x * y) ⤏ 𝒲𝒫 Γ ⟦ x * y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨(unat x) * (unat y) < 2^(LENGTH('l))⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have I: ‹Γ ; ?asm ⊢ ⟦ x * y ⟧ ⊣ (λr. ⟨r = x * y⟩ ⋆ ψ (x*y)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_mul_no_wrapI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x * y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]; auto)
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_mul_no_wrapI [micro_rust_wp_intros]:
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x * y))›
      and ‹φ ⤏ ⟨unat x * unat y < 2^LENGTH('l)⟩ ⋆ ψ (x * y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x * y ⟧ ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_word_mul_no_wrap, auto)

lemma wp_word_sub_no_wrap:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x - y))›
    shows ‹⟨y ≤ x⟩ ⋆ ψ (x - y) ⤏ 𝒲𝒫 Γ ⟦ x - y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨y ≤ x⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have I: ‹Γ ; ?asm ⊢ ⟦ x - y ⟧ ⊣ (λr. ⟨r = x - y⟩ ⋆ ψ (x - y)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_sub_no_wrapI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x - y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_sub_no_wrapI [micro_rust_wp_intros]:
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x - y))›
      and ‹φ ⤏ ⟨y ≤ x⟩ ⋆ ψ (x - y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x - y ⟧ ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_word_sub_no_wrap, auto)

lemma wp_word_udiv:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x div y))›
  shows ‹⟨y ≠ 0⟩ ⋆ ψ (x div y) ⤏ 𝒲𝒫 Γ ⟦ x / y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨y ≠ 0⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have I: ‹Γ ; ?asm ⊢ ⟦ x / y ⟧ ⊣ (λr. ⟨r = x div y⟩ ⋆ ψ (x div y)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_udivI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x / y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_udivI [micro_rust_wp_intros]:
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x div y))›
      and ‹φ ⤏ ⟨y ≠ 0⟩ ⋆ ψ (x div y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x / y ⟧ ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_word_udiv, auto)

lemma wp_word_umod:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x mod y))›
    shows ‹⟨y ≠ 0⟩ ⋆ ψ (x mod y) ⤏ 𝒲𝒫 Γ ⟦ x % y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨y ≠ 0⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have I: ‹Γ ; ?asm ⊢ ⟦ x % y ⟧ ⊣ (λr. ⟨r = x mod y⟩ ⋆ ψ (x mod y)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_umodI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x % y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_umodI [micro_rust_wp_intros]:
    fixes x y :: ‹'l::{len} word›
  assumes ‹ucincl (ψ (x mod y))›
      and ‹φ ⤏ ⟨y ≠ 0⟩ ⋆ ψ (x mod y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x % y ⟧ ψ ρ θ›
using assms by - (rule aentails_trans', rule wp_word_umod, auto)

lemma wp_bitwise_or:
  assumes ‹⋀v. ucincl (ψ v)›
    shows ‹ψ (x OR y) ⤏ 𝒲𝒫 Γ ⟦ x | y ⟧ ψ ρ θ›
using assms by (intro sstriple_pure_to_wp') (auto intro: sstriple_bitwise_orI)

lemma wp_bitwise_and:
  assumes ‹⋀v. ucincl (ψ v)›
    shows ‹ψ (x AND y) ⤏ 𝒲𝒫 Γ ⟦ x & y ⟧ ψ ρ θ›
using assms by (intro sstriple_pure_to_wp') (auto intro: sstriple_bitwise_andI)

lemma wp_bitwise_xor:
  assumes ‹⋀v. ucincl (ψ v)›
    shows ‹ψ (x XOR y) ⤏ 𝒲𝒫 Γ ⟦ x ^ y ⟧ ψ ρ θ›
using assms by (intro sstriple_pure_to_wp') (auto intro: sstriple_bitwise_xorI)

lemma wp_bitwise_not:
  assumes ‹⋀v. ucincl (ψ v)›
    shows ‹ψ (NOT x) ⤏ 𝒲𝒫 Γ ⟦ !x ⟧ ψ ρ θ›
using assms by (intro sstriple_pure_to_wp') (auto intro: sstriple_bitwise_notI)

lemma wp_bitwise_orI [micro_rust_wp_intros]:
  assumes ‹⋀v. ucincl (ψ v)›
      and ‹φ ⤏ ψ (x OR y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x | y ⟧ ψ ρ θ›
using assms wp_bitwise_or aentails_trans' by blast

lemma wp_bitwise_andI [micro_rust_wp_intros]:
  assumes ‹⋀v. ucincl (ψ v)›
      and ‹φ ⤏ ψ (x AND y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x & y ⟧ ψ ρ θ›
using assms wp_bitwise_and aentails_trans' by blast

lemma wp_bitwise_xorI [micro_rust_wp_intros]:
  assumes ‹⋀v. ucincl (ψ v)›
      and ‹φ ⤏ ψ (x XOR y)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x ^ y ⟧ ψ ρ θ›
using assms wp_bitwise_xor aentails_trans' by blast

lemma wp_bitwise_notI [micro_rust_wp_intros]:
  assumes ‹⋀v. ucincl (ψ v)›
      and ‹φ ⤏ ψ (NOT x)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ !x ⟧ ψ ρ θ›
using assms wp_bitwise_not aentails_trans' by blast

lemma wp_word_shift_left:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp[simp]
    fixes x :: ‹'l0::{len} word›
      and y :: ‹64 word›
  assumes ‹ucincl (ψ (push_bit (unat y) x))›
    shows ‹⟨unat y < LENGTH('l0)⟩ ⋆ ψ (push_bit (unat y) x) ⤏ 𝒲𝒫 Γ ⟦ x << y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨unat y < LENGTH('l0)⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have
         I: ‹Γ ; ?asm ⊢ ⟦ x << y ⟧ ⊣ (λr. ⟨r = push_bit (unat y) x⟩ ⋆ ψ (push_bit (unat y) x)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_shift_leftI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x << y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_shift_leftI [micro_rust_wp_intros]:
    fixes x :: ‹'l0::{len} word›
      and y :: ‹64 word›
  assumes ‹ucincl (ψ (push_bit (unat y) x))›
      and ‹φ ⤏ ⟨unat y < LENGTH('l0)⟩ ⋆ ψ (push_bit (unat y) x)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x << y ⟧ ψ ρ θ›
using assms wp_word_shift_left aentails_trans' by blast

lemma wp_word_shift_right:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
    fixes x :: ‹'l0::{len} word›
      and y :: ‹64 word›
  assumes ‹ucincl (ψ (drop_bit (unat y) x))›
    shows ‹⟨unat y < LENGTH('l0)⟩ ⋆ ψ (drop_bit (unat y) x) ⤏ 𝒲𝒫 Γ ⟦ x >> y ⟧ ψ ρ θ› (is ‹?asm ⤏ ?GOAL›)
proof -
  have ‹ucincl (⟨unat y < LENGTH('l0)⟩)›
    by (simp add: ucincl_apure)
  moreover from this have ‹ucincl ?asm›
    by (simp add: assms ucincl_apure ucincl_asepconj)
  moreover from calculation and assms have
         I: ‹Γ ; ?asm ⊢ ⟦ x >> y ⟧ ⊣ (λr. ⟨r = drop_bit (unat y) x⟩ ⋆ ψ (drop_bit (unat y) x)) ⨝ ρ ⨝ θ›
    by (intro sstriple_frame_rule_no_return) (auto simp add: sstriple_word_shift_rightI)
  moreover from assms have ‹Γ ; ?asm ⊢ ⟦ x >> y ⟧ ⊣ ψ ⨝ ρ ⨝ θ›
    by (intro sstriple_consequence[OF I]) auto
  ultimately show ‹?asm ⤏ ?GOAL›
    by (intro wp_is_weakest_precondition)
qed

lemma wp_word_shift_rightI [micro_rust_wp_intros]:
    fixes x :: ‹'l0::{len} word›
      and y :: ‹64 word›
  assumes ‹ucincl (ψ (drop_bit (unat y) x))›
      and ‹φ ⤏ ⟨unat y < LENGTH('l0)⟩ ⋆ ψ (drop_bit (unat y) x)›
    shows ‹φ ⤏ 𝒲𝒫 Γ ⟦ x >> y ⟧ ψ ρ θ›
using assms wp_word_shift_right aentails_trans' by blast

declare aexists_entailsL aexists_entailsR aforall_entailsL aforall_entailsR apure_entails_iff
  apure_entailsR [micro_rust_wp_intros]

subsection‹Loops›

text‹Note that this is not added to ▩‹micro_rust_wp_intros›. The invariant pretty much always needs
to be provided, so there is not much point.›
lemma wp_raw_for_loopI:
    notes aentails_intro [intro]
      and aentails_simp [simp]
      and asepconj_simp [simp]
  assumes ‹⋀past todo. ucincl (INV past todo)›
      and ‹⋀r. ucincl (ρ r)›
      and ‹φ ⤏ INV [] xs›
      and ‹⋀past cur todo. xs = past@(cur#todo) ⟹ INV past (cur#todo) ⤏ 𝒲𝒫 Γ (f cur) (λ_. INV (past@[cur]) todo) ρ θ›
      and ‹INV xs [] ⤏ ψ ()›
    shows ‹φ ⤏ 𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ θ›
proof -
  from assms have H: ‹Γ ; ⟨xs = []@xs⟩ ⋆ INV [] xs ⊢ raw_for_loop xs f ⊣ (λ_. ⟨xs = xs@[]⟩ ⋆ INV xs []) ⨝ ρ ⨝ θ›
    by (intro sstriple_raw_for_loop) (force intro: ucincl_intros wp_to_sstriple)
  from assms have ‹INV [] xs ⤏  𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ θ›
    by (intro wp_is_weakest_precondition; clarsimp intro: ucincl_intros)
      (rule sstriple_consequence[OF H]; clarsimp simp add: aentails_refl)
  from this and assms show ?thesis
    by blast
qed

text‹The following is a framed version of \<^text>‹wp_raw_for_loopI› recovering the latter if
\<^term>‹ξ = UNIV›.›
lemma wp_raw_for_loop_framedI:
  assumes ‹⋀past todo. ucincl (INV past todo)›
      and ‹⋀r. ucincl (ρ r)›
      and ‹ucincl (ψ ())›
      and ‹⋀r. ucincl (τ r)›
      and ‹φ ⤏ INV [] xs ⋆ ((INV xs [] ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
      and ‹⋀past cur todo. INV past (cur#todo) ⤏ 𝒲𝒫 Γ (f cur) (λ_. INV (past@[cur]) todo) τ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ χ›
proof -
  let ?pc = ‹((INV xs [] ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
  from assms have ‹Γ ; INV [] xs ⋆ ?pc ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
    by (intro sstriple_raw_for_loop_framed) (auto simp add: local.wp_to_sstriple ucincl_intros)
  from this and assms have ‹INV [] xs ⋆ ?pc ⤏ 𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ χ›
    using local.ucincl_asepconj wp_is_weakest_precondition by (metis (mono_tags, lifting)
      ucincl_Int local.ucincl_IntE local.ucincl_awand local.ucincl_inter)
  from this and assms show ?thesis
    by (meson assms ucincl_asepconj ucincl_awand aentails_trans')
qed

text‹Alternative loop rule which might be easier to use in some situations. Passing the list to the
invariant may seem redundant because it's part of the context, but we don't always know what the
list will be named in the current proof state.›
lemma wp_raw_for_loop_framedI':
    fixes xs :: ‹'e list›
      and INV :: ‹'e list ⇒ nat ⇒ 'a assert›
  assumes ‹⋀ls i. ucincl (INV ls i)›
      and ‹⋀r. ucincl (ρ r)›
      and ‹ucincl (ψ ())›
      and ‹⋀r. ucincl (τ r)›
      and ‹φ ⤏ INV xs 0 ⋆ ((INV xs (length xs) ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
      and ‹⋀i. i < length xs ⟹ INV xs i ⤏ 𝒲𝒫 Γ (f (xs ! i)) (λ_. INV xs (i+1)) τ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ χ›
proof -
  let ?pc = ‹((INV xs (length xs) ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
  from assms have ‹Γ ; INV xs 0 ⋆ ?pc ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
    by (intro sstriple_raw_for_loop_framed') (auto simp add: local.wp_to_sstriple ucincl_intros)
  from this and assms have ‹INV xs 0 ⋆ ?pc ⤏ 𝒲𝒫 Γ (raw_for_loop xs f) ψ ρ χ›
    by (intro wp_is_weakest_precondition) (auto intro!: ucincl_Int ucincl_awand ucincl_inter
      ucincl_asepconj)
  from this and assms show ?thesis
    by (meson assms ucincl_asepconj ucincl_awand aentails_trans')
qed

lemma wp_gather_framedI:
    fixes INV :: ‹nat ⇒ 'v list ⇒ 'a assert›
      and ξ :: ‹nat ⇒ 'v ⇒ bool›
      and thunks :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression list›
  assumes ‹⋀r. ucincl (ρ r)›
      and ‹⋀r. ucincl (ψ r)›
      and ‹⋀r. ucincl (τ r)›
      and ‹⋀ls i. ucincl (INV i ls)›
      and ‹φ ⤏ INV 0 [] ⋆ ((⨅r. (INV (length thunks) r ↠ ψ r)) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
      and ‹⋀i res. i < length thunks ⟹ length res = i ⟹
              Γ ; INV i res ⊢ thunks ! i ⊣ (λv. INV (i+1) (res @ [v])) ⨝ τ ⨝ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (gather thunks) ψ ρ χ›
proof -
  let ?pc = ‹((⨅r. (INV (length thunks) r ↠ ψ r)) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
  from assms have ‹Γ ; INV 0 [] ⋆ ?pc ⊢ gather thunks ⊣ ψ ⨝ ρ ⨝ χ›
    by (intro sstriple_gather_framed; simp add: local.wp_to_sstriple ucincl_intros)
  from this and assms have ‹INV 0 [] ⋆ ?pc ⤏ 𝒲𝒫 Γ (gather thunks) ψ ρ χ›
    by (intro wp_is_weakest_precondition) (auto intro!: ucincl_asepconj ucincl_inter ucincl_Int
      ucincl_awand)
  from this and assms show ?thesis
    by (meson assms ucincl_asepconj ucincl_awand aentails_trans')
qed

lemma wp_gather_framedI':
    fixes INV :: ‹nat ⇒ 'v list ⇒ 'a assert›
      and ξ :: ‹nat ⇒ 'v ⇒ bool›
      and thunks :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression list›
  assumes ‹⋀r. ucincl (ρ r)›
      and ‹⋀r. ucincl (ψ r)›
      and ‹⋀r. ucincl (τ r)›
      and ‹⋀ls i. ucincl (INV i ls)›
      and ‹φ ⤏ INV 0 [] ⋆ ((⨅r. (INV (length thunks) r ↠ ψ r)) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
      and ‹⋀i res. i < length thunks ⟹ length res = i ⟹
              INV i res ⤏ 𝒲𝒫 Γ (thunks ! i) (λv. INV (i+1) (res @ [v])) τ θ›
    shows ‹φ ⤏ 𝒲𝒫 Γ (gather thunks) ψ ρ χ›
  using assms by (blast intro: wp_gather_framedI wp_to_sstriple)

(*<*)
end
(*>*)

(*<*)
end
(*>*)