Theory Shallow_Separation_Logic.Triple

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

(*<*)
theory Triple
  imports Assertion_Language Shallow_Micro_Rust.Shallow_Micro_Rust Precision Weak_Triple
begin
(*>*)

section‹Triples›

subsection‹Evaluation predicates›

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

abbreviation urust_is_local where
  ‹urust_is_local Γ e φ ≡
     is_local (λσ (v, σ'). σ ↝⇩v⟨Γ,e⟩ (v,σ')) φ ∧
     is_local (λσ (r, σ'). σ ↝⇩r⟨Γ,e⟩ (r,σ')) φ ∧
     is_local (λσ (a, σ'). σ ↝⇩a⟨Γ,e⟩ (a,σ')) φ›

lemma urust_is_local_weaken:
  assumes ‹φ' ⤏ φ›
      and ‹urust_is_local Γ e φ›
    shows ‹urust_is_local Γ e φ'›
  using assms by (clarsimp simp add: is_local_weaken)

lemma urust_is_local_Union:
  assumes ‹⋀x. urust_is_local Γ e (φ x)›
    shows ‹urust_is_local Γ e (⋃x. φ x)›
  using assms by (simp add: is_local_Union)

definition sstriple ::
     ‹('a, 'abort, 'i, 'o) striple_context ⇒ ― ‹Fixed context for this verification›
      'a assert ⇒ ― ‹The property of the pre-state›
      ('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression ⇒ ― ‹Expanded out our expression type›
      ('v ⇒ 'a assert) ⇒ ― ‹The property of the post-state after successful execution›
      ('r ⇒ 'a assert) ⇒ ― ‹The property of the post-state after successful early return›
      ('abort abort ⇒ 'a assert) ⇒
      bool› ("(_) ; (_) /⊢/ (_) /⊣/ (_) /⨝/ (_) /⨝/ (_)" [50,50,50,50,50,50]50) where
  ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ ≡ (
     φ ⊢ eval_value (yh Γ) e ⊣⇩R ψ ∧
     φ ⊢ eval_return (yh Γ) e ⊣⇩R ξ ∧
     φ ⊢ eval_abort (yh Γ) e ⊣⇩R θ)›

lemma sstripleI:
  assumes ‹φ ⊢ eval_value (yh Γ) e ⊣⇩R ψ›
      and ‹φ ⊢ eval_return (yh Γ) e ⊣⇩R ξ›
      and ‹φ ⊢ eval_abort (yh Γ) e ⊣⇩R θ›
    shows ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
using assms sstriple_def by blast

lemma sstriple_upwards_closure:
  shows ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷ (Γ ; φ ⋆ ⊤ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ)›
    and ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷ (Γ ; φ ⊢ e ⊣ (λr. ψ r ⋆ ⊤) ⨝ ξ ⨝ θ)›
    and ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷ (Γ ; φ ⊢ e ⊣ ψ ⨝ (λr. ξ r ⋆ ⊤) ⨝ θ)›
    and ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷ (Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ (λa. θ a ⋆ ⊤))›
    and ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷ (Γ ; φ ⊢ e ⊣ (λr. ψ r ⋆ ⊤) ⨝ (λr. ξ r ⋆ ⊤) ⨝ (λa. θ a ⋆ ⊤))›
  by (auto simp add: sstriple_def atriple_rel_upwards_closure' asepconj_simp)

lemma sstriple_striple:
  fixes Γ :: ‹('a, 'abort, 'i, 'o) striple_context›
    and φ :: ‹'a assert›
    and e :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression›
    and ψ :: ‹'v ⇒ 'a assert›
    and ξ :: ‹'r ⇒ 'a assert›
    and θ :: ‹'abort abort ⇒ 'a assert›
  shows ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷
           (Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ ∧ is_local (eval_value (yh Γ) e) φ
                                        ∧ is_local (eval_return (yh Γ) e) φ
                                        ∧ is_local (eval_abort (yh Γ) e) φ)›
   (is ‹?a ⟷ ?b›)
proof -
  { assume SS: ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
    then have ‹Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ›
      by (intro striple_localI'; auto simp add: sstriple_def atriple_rel_def
        eval_value_def eval_return_def eval_abort_def asepconj_weakenI)
    moreover from SS have ‹is_local (eval_value (yh Γ) e) φ›
                      and ‹is_local (eval_return (yh Γ) e) φ›
                      and ‹is_local (eval_abort (yh Γ) e) φ›
      by (auto simp add: atriple_rel_def sstriple_def)
    ultimately have ‹(Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ ∧ is_local (eval_value (yh Γ) e) φ
                                                  ∧ is_local (eval_return (yh Γ) e) φ
                                                  ∧ is_local (eval_abort (yh Γ) e) φ)›
      by auto }
  moreover {
    assume S: ‹Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ›
      and ‹is_local (eval_value (yh Γ) e) φ›
      and ‹is_local (eval_return (yh Γ) e) φ›
      and ‹is_local (eval_abort (yh Γ) e) φ›
    then have ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
      by (intro sstripleI; clarsimp simp add: atriple_rel_def eval_value_def eval_return_def
        eval_abort_def striple_def atriple_def urust_eval_action_via_predicate ucincl_UNIV
        asepconj_weakenI)
  }
  ultimately show ?thesis
    by auto
qed

lemma sstriple_implies_is_local:
  assumes ‹Γ; φ ⊢ e ⊣ α ⨝ β ⨝ γ›
  shows ‹urust_is_local (yh Γ) e φ›
  using assms by (simp add: sstriple_striple eval_abort_def eval_return_def eval_value_def)

lemma sstriple_striple':
  fixes Γ :: ‹('a, 'abort, 'i, 'o) striple_context›
    and φ :: ‹'a assert›
    and e :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression›
    and ψ :: ‹'v ⇒ 'a assert›
    and ξ :: ‹'r ⇒ 'a assert›
    and θ :: ‹'abort abort ⇒ 'a assert›
  shows ‹(Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ) ⟷
           (Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ ∧ urust_is_local (yh Γ) e φ)›
  by (clarsimp simp add: sstriple_striple eval_value_def eval_abort_def eval_return_def)

lemma sstriple_from_stripleI:
  assumes ‹Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ›
      and ‹is_local (eval_value (yh Γ) e) φ›
      and ‹is_local (eval_return (yh Γ) e) φ›
      and ‹is_local (eval_abort (yh Γ) e) φ›
    shows ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
  using assms sstriple_striple by blast

lemma striple_from_sstripleI:
  assumes ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
    shows ‹Γ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ θ›
  using assms sstriple_striple by blast

lemma sstriple_satisfiable:
  assumes ‹striple_context_no_yield ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ θ›
      and ‹is_sat φ›
      and ‹⋀v. ucincl (ψ v)›
      and ‹⋀r. ucincl (ξ r)›
      and ‹⋀a. ucincl (θ a)›
    shows ‹(∃v. is_sat (ψ v)) ∨ (∃r. is_sat (ξ r)) ∨ (∃a. is_sat (θ a))›
  using assms striple_satisfiable striple_from_sstripleI by blast

subsection ‹Basic properties of \<^term>‹sstriple››

text‹When proving a triple, one can without loss of generality assume that the spatial
precondition of the triple is satisfiable.›
lemma sstriple_assume_is_sat:
  assumes ‹is_sat φ ⟹ Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    shows ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
  using assms
  by (meson aentails_is_sat is_local_empty is_local_weaken striple_assume_is_sat sstriple_striple)

lemma sstriple_existsI:
  assumes ‹(⋀x. Γ ; φ x ⊢ e ⊣ ξ ⨝ ρ ⨝ θ)›
    shows ‹Γ ; (⋃x. φ x) ⊢ e ⊣ ξ ⨝ ρ ⨝ θ›
  using assms
  by (simp add: local.is_local_bUnion local.striple_bexistsI sstriple_striple)

lemma sstriple_existsI':
  assumes ‹(⋀φ. φ ∈ Φ ⟹ Γ ; φ ⊢ e ⊣ ξ ⨝ ρ ⨝ θ)›
    shows ‹Γ ; (⋃Φ) ⊢ e ⊣ ξ ⨝ ρ ⨝ θ›
  using assms
  by (simp add: local.is_local_Union' local.striple_existsI' sstriple_striple)

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_bexistsI:
  assumes ‹(⋀x. x∈S ⟹ Γ ; φ x ⊢ e ⊣ ξ ⨝ ρ ⨝ θ)›
    shows ‹Γ ; (⋃x∈S. φ x) ⊢ e ⊣ ξ ⨝ ρ ⨝ θ›
  using assms
  by (metis (mono_tags, lifting) imageE sstriple_existsI')

subsection‹Structural rules›

text‹This is the rule of consequence, which allows you to strengthen the preconditions of an
expression's execution and strengthen the postcondition:›
lemma sstriple_consequence:
  assumes ‹Γ ; φ' ⊢ e ⊣ ψ' ⨝ ρ' ⨝ θ'›
      and ‹φ ⤏ φ'›
      and ‹⋀r. ψ' r ⤏ ψ r›
      and ‹⋀r. ρ' r ⤏ ρ r›
      and ‹⋀a. θ' a ⤏ θ a›
    shows ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
using assms is_local_weaken by (intro sstriple_from_stripleI; clarsimp simp add: sstriple_striple
  striple_consequence)

text‹NB: this is expressed in a non-standard form as it's used to derive other results below by
unifying against the premiss of another theorem.›
lemma sstriple_consequence_wrap:
  shows ‹∀φ ψ ρ θ ψ' ρ' θ' φ' e Γ.
     sstriple Γ φ' e ψ' ρ' θ'
      ⟶ φ ⤏ φ'
      ⟶ (∀r. ψ' r ⤏ ψ r)
      ⟶ (∀r. ρ' r ⤏ ρ r)
      ⟶ (∀a. θ' a ⤏ θ a)
      ⟶ sstriple Γ φ e ψ ρ θ›
using sstriple_consequence by blast

theorem sstriple_frame_rule:
  assumes ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
    shows ‹Γ ; φ ⋆ ξ ⊢ e ⊣ (λr. ψ r ⋆ ξ) ⨝ (λr. ρ r ⋆ ξ)⨝ (λa. θ a ⋆ ξ)›
  using assms by (intro sstriple_from_stripleI; clarsimp simp add: sstriple_striple
      striple_frame_rule is_local_frame)

text‹NB: this is expressed in a non-standard form as it's used to derive other results below by
unifying against the premiss of another theorem.›
theorem sstriple_frame_rule_wrap:
  shows ‹∀φ ψ ρ θ ξ Γ e. sstriple Γ φ e ψ ρ θ
     ⟶ sstriple Γ (φ ⋆ ξ) e (λv. ψ v ⋆ ξ) (λr. ρ r ⋆ ξ) (λa. θ a ⋆ ξ)›
  by (simp add: sstriple_frame_rule)

lemmas sstriple_frame_rule' = triple_frame_rule'
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_ruleI = triple_frame_ruleI
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_ruleI' = triple_frame_ruleI'
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_rule_asepconj_multi_singleI' =
  triple_frame_rule_asepconj_multi_singleI'
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_rule_asepconj_multi =
  triple_frame_rule_asepconj_multi_singleI'
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_rule_asepconj_multi_single =
  triple_frame_rule_asepconj_multi_single
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_rule_no_value =
  triple_frame_rule_no_value
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]
lemmas sstriple_frame_rule_no_return =
  triple_frame_rule_no_return
  [OF sstriple_consequence_wrap, OF sstriple_frame_rule_wrap]

subsection‹Local axioms for Micro Rust expressions in SSA form:›

text‹This is the ``fundamental result'' here, as most other Micro Rust constructs are defined in
terms of the monadic bind.  Note that this is the rule for ▩‹let› in disguise.›
lemma sstriple_bindI:
  assumes ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
      and ‹⋀x. Γ ; ψ x ⊢ f x ⊣ ξ ⨝ ρ ⨝ θ›   ― ‹Case of continuation into \<^term>‹f››
    shows ‹Γ ; φ ⊢ Core_Expression.bind e f ⊣ ξ ⨝ ρ ⨝ θ›
  using assms by (clarsimp simp add: sstriple_def urust_eval_predicate_simps
    atriple_rel_bind atriple_rel_disj)

text‹This is basically the ▩‹sstriple_bindI› theorem in a (thin) disguise:›
corollary sstriple_sequenceI:
  assumes ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ρ ⨝ θ›
      and ‹Γ ; ψ () ⊢ f ⊣ ξ ⨝ ρ ⨝ θ›
      and ‹⋀r. ρ r = ξ r›
    shows ‹Γ ; φ ⊢ sequence e f ⊣ ξ ⨝ ρ ⨝ θ›
  using assms unfolding sequence_def by (auto intro: sstriple_bindI)

text‹The ▩‹skip› command does not modify the state in any way, and always succeeds:›
―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_skipI:
  shows ‹Γ ; ψ ⊢ skip ⊣ (λ_. ψ) ⨝ ρ ⨝ θ›
  by (auto intro!: sstriple_from_stripleI striple_skipI
      simp add: eval_value_def eval_return_def eval_abort_def urust_eval_predicate_skip is_local_def)

text‹Executing a literal does not modify the state in anyway way, but does return the literal value.
It also always succeeds:›
lemma sstriple_literalI:
  shows ‹Γ ; ⊤ ⊢ ↑v ⊣ (λrv. ⟨rv = v⟩) ⨝ ρ ⨝ θ›
  by (auto intro: sstriple_from_stripleI striple_literalI 
      simp add: urust_eval_predicate_literal is_local_def eval_value_def eval_return_def eval_abort_def)

lemma sstriple_literal:
  shows ‹(Γ ; φ ⊢ ↑v ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ ψ v ⋆ ⊤)›
proof (intro iffI)
  show ‹Γ ; φ ⊢ ↑v ⊣ ψ ⨝ ρ ⨝ θ ⟹ φ ⤏ ψ v ⋆ UNIV›
    by (simp add: local.striple_literal sstriple_striple')
  show ‹φ ⤏ ψ v ⋆ UNIV ⟹ Γ ; φ ⊢ ↑v ⊣ ψ ⨝ ρ ⨝ θ›
  by (meson aentails_true is_local_weaken striple_literal sstriple_literalI sstriple_striple)
qed

lemma sstriple_assert_val:
  shows ‹(Γ ; φ ⊢ assert_val v ⊣ ψ ⨝ ρ ⨝ θ) ⟷
     ((v ⟶ φ ⤏ ⊤ ⋆ ψ ()) ∧ (¬v ⟶ φ ⤏ ⊤ ⋆ θ AssertionFailed))›
  by (auto simp add: sstriple_striple striple_assert_val eval_value_def
    eval_abort_def eval_return_def urust_eval_predicate_simps is_local_def)

lemma sstriple_assert:
  shows ‹(Γ ; φ ⊢ ⟦assert!(v)⟧ ⊣ ψ ⨝ ρ ⨝ θ) ⟷
            (v ⟶ φ ⤏ ⊤ ⋆ ψ ()) ∧ (¬v ⟶ φ ⤏ ⊤ ⋆ θ AssertionFailed)›
  by (simp add: assert_def micro_rust_simps sstriple_assert_val)

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_assert_eq:
  shows ‹(Γ ; φ ⊢ ⟦assert_eq!(v,w)⟧ ⊣ ψ ⨝ ρ ⨝ θ) ⟷
      (v=w ⟶ φ ⤏ ⊤ ⋆ ψ ()) ∧ (v ≠ w ⟶ φ ⤏ ⊤ ⋆ θ AssertionFailed)›
  by (simp add: assert_eq_def assert_eq_val_def sstriple_assert_val micro_rust_simps)

text‹The ▩‹return_func› command always succeeds and returns the given value:›
―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_return_valI:
  shows ‹Γ ; ⊤ ⊢ return_val v ⊣ ψ ⨝ (λrv. ⟨rv = v⟩) ⨝ θ›
  by (auto intro!: sstriple_from_stripleI striple_return_valI
      simp add: urust_eval_predicate_return is_local_def eval_value_def eval_return_def eval_abort_def)

lemma sstriple_return_val:
  shows ‹(Γ ; φ ⊢ return_val v ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ ρ v ⋆ ⊤)›
proof
  show ‹Γ ; φ ⊢ return_val v ⊣ ψ ⨝ ρ ⨝ θ ⟹ φ ⤏ ρ v ⋆ UNIV›
    by (simp add: striple_return_val sstriple_striple)
  show ‹φ ⤏ ρ v ⋆ UNIV ⟹ Γ ; φ ⊢ return_val v ⊣ ψ ⨝ ρ ⨝ θ›
    by (meson aentails_true is_local_weaken striple_return_val sstriple_return_valI sstriple_striple)
qed

text‹The ▩‹return_func› command always succeeds and returns the given value:›
―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_returnI:
  shows ‹Γ ; ⊤ ⊢ return_func (↑v) ⊣ ψ ⨝ (λrv. ⟨rv = v⟩) ⨝ θ›
  by (simp add: bind_literal_unit return_func_def sstriple_return_valI)

lemma sstriple_return:
  shows ‹(Γ ; φ ⊢ return_func (↑v) ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ ρ v ⋆ ⊤)›
  by (simp add: bind_literal_unit return_func_def sstriple_return_val)

corollary sstriple_noneI:
  shows ‹Γ ; ⊤ ⊢ `None ⊣ (λrv. ⟨rv = None⟩) ⨝ ρ ⨝ θ›
  unfolding none_def by (rule sstriple_literalI)

corollary sstriple_trueI:
  shows ‹Γ ; ⊤ ⊢ `True ⊣ (λrv. ⟨rv = True⟩) ⨝ ρ ⨝ θ›
  unfolding true_def by (rule sstriple_literalI)

corollary sstriple_falseI:
  shows ‹Γ ; ⊤ ⊢ `False ⊣ (λrv. ⟨rv = False⟩) ⨝ ρ ⨝ θ›
  unfolding false_def by (rule sstriple_literalI)

corollary sstriple_someI:
  notes asepconj_simp [simp]
  shows ‹Γ ; ⊤ ⊢ `Some (↑x) ⊣ (λrv. ⟨rv = Some x⟩) ⨝ ρ ⨝ θ›
  apply (intro sstriple_from_stripleI striple_someI)
  apply (auto simp add: return_func_def urust_eval_predicate_literal urust_eval_predicate_return
    micro_rust_simps some_def is_local_def eval_value_def eval_return_def eval_abort_def)
  done

text‹Abort and panic terminate execution of the program:›
lemma sstriple_abort:
  shows ‹(Γ ; φ ⊢ abort m ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ θ m ⋆ ⊤)›
  by (fastforce simp add: sstriple_striple striple_abort is_local_def eval_value_def
    eval_return_def eval_abort_def urust_eval_predicate_simps)

text‹Panic terminates execution of the program:›
―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_panic:
  shows ‹(Γ ; φ ⊢ panic m ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ θ (Panic m) ⋆ ⊤)›
  by (simp add: sstriple_abort)

text‹Pause / Breakpoint›

lemma sstriple_pause:
  assumes ‹⋀r. ucincl (ψ r)›
    shows ‹(Γ ; ⊤ ⊢ ⟦ 𝗒𝗂𝖾𝗅𝖽 ⟧ ⊣ ⊤ ⨝ ρ ⨝ θ)›
  using assms
  by (auto intro!: sstriple_from_stripleI striple_pause
      simp add: is_local_def eval_return_def eval_value_def eval_abort_def urust_eval_predicate_simps
      is_valid_striple_context_def)

lemma sstriple_pause':
  assumes ‹⋀r. ucincl (ψ r)›
  shows ‹(Γ ; φ ⊢ ⟦ 𝗒𝗂𝖾𝗅𝖽 ⟧ ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ ψ ())›
proof
  show ‹Γ ; φ ⊢ pause ⊣ ψ ⨝ ρ ⨝ θ ⟹ φ ⤏ ψ ()›
    using assms by (simp add: striple_pause' sstriple_striple')
  show ‹φ ⤏ ψ () ⟹ Γ ; φ ⊢ pause ⊣ ψ ⨝ ρ ⨝ θ›
    using assms 
    by (auto simp: sstriple_striple striple_pause' is_local_def 
        eval_return_def eval_value_def eval_abort_def urust_eval_predicate_simps)
qed

text‹Log›

lemma sstriple_log:
  shows ‹Γ ; ⊤ ⊢ ⟦ 𝗅𝗈𝗀 ⟪p⟫ ⟪l⟫ ⟧ ⊣ ⊤ ⨝ ρ ⨝ θ›
  by (auto intro!: sstriple_from_stripleI striple_log simp add: is_local_def eval_return_def eval_value_def urust_eval_predicate_simps
    is_valid_striple_context_def eval_abort_def)

lemma sstriple_log':
  assumes  ‹⋀r. ucincl (ψ r)›
  shows ‹(Γ ; φ ⊢ ⟦ 𝗅𝗈𝗀 ⟪p⟫ ⟪l⟫ ⟧ ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (φ ⤏ ψ ())›
proof
  show ‹Γ ; φ ⊢ log p l ⊣ ψ ⨝ ρ ⨝ θ ⟹ φ ⤏ ψ ()›
    using assms by (simp add: local.striple_log' sstriple_striple')
  show ‹φ ⤏ ψ () ⟹ Γ ; φ ⊢ log p l ⊣ ψ ⨝ ρ ⨝ θ›
    using assms by (meson aentails_true is_local_weaken striple_log' sstriple_log sstriple_striple)
qed

text‹Fatal errors›

lemma sstriple_fatal:
  assumes ‹is_aborting_striple_context Γ›
      and ‹⋀r. ucincl (ψ r)›
    shows ‹(Γ ; φ ⊢ ⟦ fatal!(msg) ⟧ ⊣ ψ ⨝ ρ ⨝ θ)›
  using assms
  by (auto intro!: sstriple_from_stripleI 
      simp add: is_local_def eval_return_def eval_value_def urust_eval_predicate_simps
      is_aborting_striple_context_def eval_abort_def striple_fatal)

text‹Generic yield›

lemma sstriple_yield:
  shows ‹(Γ; φ ⊢ yield ω ⊣ ψ ⨝ ρ ⨝ θ) ⟷ (
               is_local (λσ (v, σ'). YieldContinue (v, σ') ∈ yh Γ ω σ) φ ∧
               is_local (λσ (a, σ'). YieldAbort a σ' ∈ yh Γ ω σ) φ ∧
               (∀σ σ' v. YieldContinue (v, σ') ∈ yh Γ ω σ ⟶ σ ⊨ φ ⟶ σ' ⊨ ψ v ⋆ UNIV) ∧
               (∀σ σ' a. YieldAbort a σ' ∈ yh Γ ω σ ⟶ σ ⊨ φ ⟶ σ' ⊨ θ a ⋆ UNIV))›
  by (auto simp add: sstriple_def eval_abort_def eval_value_def eval_return_def is_local_False
    urust_eval_predicate_simps urust_eval_action_via_predicate striple_yield atriple_rel_def)

text‹Conditionals›

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma sstriple_two_armed_conditionalI:
  assumes ‹x ⟹ Γ ; φ ⊢ e ⊣ ξ ⨝ ρ ⨝ θ›
      and ‹¬ x ⟹ Γ ; φ ⊢ f ⊣ ξ ⨝ ρ ⨝ θ›
    shows ‹Γ ; φ ⊢ two_armed_conditional (↑x) e f ⊣ ξ ⨝ ρ ⨝ θ›
  by (metis (full_types) assms two_armed_conditional_true_false_collapse)

text‹Note that, in contrast to the weak striple, this lemma cannot be strengthened into
an equivalence, as ▩‹call f› can be local without ▩‹f› being local.›
lemma sstriple_callI:
  assumes ‹Γ ; φ ⊢ f ⊣ ψ ⨝ ψ ⨝ θ›
    shows ‹Γ ; φ ⊢ call (FunctionBody f) ⊣ ψ ⨝ ρ ⨝ θ›
using assms by (auto simp: sstriple_def atriple_rel_def urust_eval_predicate_call
  urust_eval_predicate_call_rel is_local_disj) (subst is_local_def; clarsimp)

lemma sstriple_call_funliteral:
  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) ⋆ ⊤)›
  by (fastforce simp: sstriple_striple striple_call_funliteral micro_rust_simps striple_literal
    eval_value_def eval_return_def eval_abort_def is_local_def urust_eval_predicate_simps)+

lemma sstriple_getI:
  assumes ‹ucincl (has f v)›
    shows ‹Γ; has f v ⊢ get f ⊣ (λx. ⟨x = v⟩ ⋆ has f v) ⨝ ρ ⨝ θ›
proof -
  from ‹ucincl (has f v)› have ‹⋀x y. x ♯ y ⟹ x ⊨ has f v ⟹ (x + y) ⊨ has f v›
    by (simp add: local.asat_weaken)
  with assms show ?thesis
    apply (intro sstriple_from_stripleI striple_getI)
    apply (auto simp: is_local_def urust_eval_predicate_simps eval_value_def
        eval_return_def eval_abort_def asat_def has_def)
    done
qed

lemma sstriple_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›
    shows ‹Γ; has f v ⊢ put g ⊣ (λ_. has f v') ⨝ ρ ⨝ θ›
  using assms
  by (auto intro!: sstriple_from_stripleI striple_putI simp add: is_local_def urust_eval_predicate_simps eval_value_def
      eval_return_def eval_abort_def)


subsection‹Defining triples for numeric and bitwise operators›

lemma sstriple_word_add_no_wrapI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⟨unat x + unat y < 2^(LENGTH('l))⟩ ⊢ ⟦ x + y ⟧ ⊣ (λr. ⟨r = x + y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_add_no_wrapI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_mul_no_wrapI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⟨unat x * unat y < 2^(LENGTH('l))⟩ ⊢ ⟦ x * y ⟧ ⊣ (λr. ⟨r = x * y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_mul_no_wrapI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_sub_no_wrapI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⟨y ≤ x⟩ ⊢ ⟦ x - y ⟧ ⊣ (λr. ⟨r = x - y⟩) ⨝ ρ ⨝ θ›
  by (auto intro!: sstriple_from_stripleI striple_word_sub_no_wrapI simp add: eval_value_def
    eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_udivI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⟨y ≠ 0⟩ ⊢ ⟦ x / y ⟧ ⊣ (λr. ⟨r = x div y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_udivI simp add: eval_value_def eval_return_def
  urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_umodI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⟨y ≠ 0⟩ ⊢ ⟦ x % y ⟧ ⊣ (λr. ⟨r = x mod y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_umodI simp add: eval_value_def eval_return_def
  urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_shift_leftI:
  fixes x :: ‹'l0::{len} word›
    and y :: ‹64 word›
  shows ‹Γ ; ⟨unat y < LENGTH('l0)⟩ ⊢ ⟦ x << y ⟧ ⊣ (λr. ⟨r = push_bit (unat y) x⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_shift_leftI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_word_shift_rightI:
  fixes x :: ‹'l0::{len} word›
    and y :: ‹64 word›
  shows ‹Γ ; ⟨unat y < LENGTH('l0)⟩ ⊢ ⟦ x >> y ⟧ ⊣ (λr. ⟨r = drop_bit (unat y) x⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_word_shift_rightI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_bitwise_orI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⊤ ⊢ ⟦ x | y ⟧ ⊣ (λr. ⟨r = x OR y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_bitwise_orI simp add: eval_value_def eval_return_def
  urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_bitwise_andI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⊤ ⊢ ⟦ x & y ⟧ ⊣ (λr. ⟨r = x AND y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_bitwise_andI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_bitwise_xorI:
  fixes x y :: ‹'l::{len} word›
  shows ‹Γ ; ⊤ ⊢ ⟦ x ^ y ⟧ ⊣ (λr. ⟨r = x XOR y⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_bitwise_xorI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

lemma sstriple_bitwise_notI:
  fixes x :: ‹'l::{len} word›
  shows ‹Γ ; ⊤ ⊢ ⟦ !x ⟧ ⊣ (λr. ⟨r = NOT x⟩) ⨝ ρ ⨝ θ›
by (auto intro!: sstriple_from_stripleI striple_bitwise_notI simp add: eval_value_def
  eval_return_def urust_eval_predicate_simps is_local_def eval_abort_def)

subsection‹Loops›

lemma sstriple_raw_for_loop:
    fixes I :: ‹'t list ⇒ 't list ⇒ 'a assert›
  assumes ‹⋀past cur todo. Γ ; I past (cur # todo) ⊢ f cur ⊣ (λ_. I (past @ [cur]) todo) ⨝ ρ ⨝ θ›
    shows ‹Γ ; I [] xs ⊢ raw_for_loop xs f ⊣ (λ_. I xs []) ⨝ ρ ⨝ θ›
  using assms 
proof (induction xs arbitrary: I)
  case Nil
  then show ?case
    by (simp add: raw_for_loop_nil sstriple_skipI)
next
  case (Cons x xs)
  then have ‹Γ ; I [] (x # xs) ⊢ f x ⊣ (λ_. I [x] xs) ⨝ ρ ⨝ θ›
    by (metis append_Nil)
  moreover have ‹Γ ; I [x] xs ⊢ raw_for_loop xs f ⊣ (λ_. I (x # xs) []) ⨝ ρ ⨝ θ›
    using Cons.prems Cons.IH[where I=‹λpast todo. I (x # past) todo›] by (metis append_Cons)
  ultimately have ‹Γ ; I [] (x # xs) ⊢ (bind (f x) (λ_. raw_for_loop xs f)) ⊣ (λ_. I (x # xs) []) ⨝ ρ ⨝ θ›
    using sstriple_bindI by fastforce
  then show ‹Γ ; I [] (x # xs) ⊢ raw_for_loop (x # xs) f ⊣ (λ_. I (x # xs) []) ⨝ ρ ⨝ θ›
    by (clarsimp simp add: micro_rust_simps sequence_def)
qed

lemma sstriple_raw_for_loop_framed:
    notes aentails_intro [intro]
    fixes INV :: ‹'t list ⇒ 't list ⇒ 'a assert›
  assumes ‹⋀p t. ucincl (INV p t)›
      and ‹⋀past cur todo. Γ ;  INV past (cur # todo) ⊢ f cur ⊣ (λ_. INV (past @ [cur]) todo) ⨝ τ ⨝ θ›
    shows ‹Γ ; INV [] xs ⋆ ((INV xs [] ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r)) ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
proof -
  let ?pc = ‹(INV xs [] ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r)›
  {
    fix past cur todo
    have ‹Γ ; INV past (cur # todo) ⊢ f cur ⊣ (λ_. INV (past @ [cur]) todo) ⨝ τ ⨝ θ›
      using assms by auto
    moreover have ‹Γ ; INV past (cur # todo) ⋆ ?pc ⊢ f cur ⊣
        (λ_. INV (past @ [cur]) todo ⋆ ?pc) ⨝ (λr. τ r ⋆ ?pc) ⨝ (λa. θ a ⋆ ?pc)›
      using assms by (intro sstriple_frame_rule; clarsimp)
    moreover have ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
    proof -
      have ‹⋀r. τ r ⋆ (⨅r. τ r ↠ ρ r) ⤏ ρ r›
        by (meson aentails_refl aentails_trans aforall_entailsL asepconj_mono3 awand_counit)
      from this show ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
        by (meson aentails_fold_def aentails_inter_weaken aentails_inter_weaken2 asepconj_mono awand_adjointI)
    qed
    moreover have ‹⋀a. θ a ⋆ ?pc ⤏ χ a›
      by (meson aentails_refl aentails_trans' aentails_inter_weaken aforall_entailsL asepconj_mono awand_counit)
    ultimately have ‹Γ ; INV past (cur # todo) ⋆?pc ⊢ f cur ⊣
          (λ_. INV (past @ [cur]) todo ⋆ ?pc) ⨝ ρ ⨝ χ›
      using assms
      by (meson aentails_refl sstriple_consequence)
  }
  then have ‹Γ ; INV [] xs ⋆ ?pc ⊢ raw_for_loop xs f ⊣ (λ_. INV xs [] ⋆ ?pc) ⨝ ρ ⨝ χ›
    using assms sstriple_raw_for_loop[where I=‹λp t. INV p t ⋆ ?pc›]
      by blast
  moreover have ‹INV xs [] ⋆ ?pc ⤏ ψ ()›
    by (metis (no_types, lifting) aentails_refl local.asepconj_comm local.aentails_int local.awand_adjoint)
  ultimately have ‹Γ ; INV [] xs ⋆ ?pc ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
    using local.sstriple_consequence by (fastforce simp add: aentails_refl)
  then show ?thesis
    using aentails_refl local.asepconj_comm local.awand_mp local.sstriple_consequence by fastforce
qed

lemma sstriple_raw_for_loop':
    fixes I :: ‹'t list ⇒ nat ⇒ 'a assert›
  assumes ‹⋀i. i < length xs ⟹ (Γ ; I xs i ⊢ f (xs ! i) ⊣ (λ_. I xs (i+1)) ⨝ ρ ⨝ θ)›
    shows ‹Γ ; I xs 0 ⊢ raw_for_loop xs f ⊣ (λ_. I xs (length xs)) ⨝ ρ ⨝ θ›
  using assms 
proof (induction xs arbitrary: I)
  case Nil
  then show ?case
    by (simp add: raw_for_loop_nil sstriple_skipI)
next
  case (Cons x xs)
  then have ‹Γ ; I (x # xs) 0 ⊢ f x ⊣ (λ_. I (x # xs) 1) ⨝ ρ ⨝ θ›
    by fastforce
  moreover have ‹⋀i. i < length xs ⟹ Γ ; I (x # xs) (Suc i) ⊢ f (xs ! i) ⊣ (λ_. I (x # xs) (Suc (Suc i))) ⨝ ρ ⨝ θ›
    by (metis Cons.prems Suc_eq_plus1 Suc_mono length_Cons nth_Cons_Suc)
  then have ‹Γ ; I (x # xs) 1 ⊢ raw_for_loop xs f ⊣ (λ_. I (x # xs) (Suc (length xs))) ⨝ ρ ⨝ θ›
    using  Cons.IH[where I=‹λ_ i. I (x # xs) (i+1)›] by force
  ultimately have ‹Γ ; I (x # xs) 0 ⊢ (bind (f x) (λ_. raw_for_loop xs f)) ⊣ (λ_. I (x # xs) (Suc (length xs))) ⨝ ρ ⨝ θ›
    by (auto intro: sstriple_bindI[where ψ=‹λ _. I (x # xs) 1›])
  then show ?case
    by (auto simp add: micro_rust_simps sequence_def)
qed

lemma sstriple_raw_for_loop_framed':
    notes aentails_intro [intro]
    fixes INV :: ‹'t list ⇒ nat ⇒ 'a assert›
  assumes ‹⋀i. (i < length xs) ⟹ (Γ ; INV xs i ⊢ f (xs ! i) ⊣ (λ_. INV xs (i+1)) ⨝ τ ⨝ θ)›
    shows ‹Γ ; INV xs 0 ⋆ (INV xs (length xs) ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r) ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
proof -
  let ?pc = ‹(INV xs (length xs) ↠ ψ ()) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r)›
  {
    fix i
    assume ‹i < length xs›
    from this have ‹Γ ; INV xs i ⊢ f (xs ! i) ⊣ (λ_. INV xs (i+1)) ⨝ τ ⨝ θ›
      using assms by auto
    moreover have ‹Γ ; INV xs i ⋆ ?pc ⊢ f (xs ! i) ⊣
        (λ_. INV xs (i+1) ⋆ ?pc) ⨝ (λr. τ r ⋆ ?pc) ⨝ (λa. θ a ⋆ ?pc)›
      using calculation assms by (intro sstriple_frame_rule)
        (auto intro!: ucincl_Int ucincl_awand ucincl_inter)
    moreover have ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
    proof -
      have ‹⋀r. τ r ⋆ (⨅r. τ r ↠ ρ r) ⤏ ρ r›
        by (meson aentails_refl aentails_trans aforall_entailsL asepconj_mono3 awand_counit)
      from this show ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
        by (meson aentails_fold_def aentails_inter_weaken aentails_inter_weaken2 asepconj_mono awand_adjointI)
    qed
    moreover have ‹⋀a. θ a ⋆ ?pc ⤏ χ a›
      by (meson aentails_refl_eq aentails_trans' aentails_inter_weaken aforall_entailsL asepconj_mono3
          awand_counit)
    ultimately have ‹Γ ; INV xs i ⋆ ?pc ⊢ f (xs ! i) ⊣ (λ_. INV xs (i+1) ⋆ ?pc) ⨝ ρ ⨝ χ›
      by (meson aentails_refl sstriple_consequence)
  }
  from this have ‹Γ ; INV xs 0 ⋆ ?pc
                            ⊢ raw_for_loop xs f ⊣ (λ_. INV xs (length xs) ⋆ ?pc) ⨝ ρ ⨝ χ›
    using assms sstriple_raw_for_loop'[where I=‹λxs' i'. INV xs' i' ⋆ ?pc›] by blast
  moreover have ‹INV xs (length xs) ⋆ ?pc ⤏ ψ ()›
    by (metis (no_types, lifting) aentails_refl local.asepconj_comm local.aentails_int local.awand_adjoint)
  moreover have ‹Γ ; INV xs 0 ⋆ ?pc ⊢ raw_for_loop xs f ⊣ ψ ⨝ ρ ⨝ χ›
    using calculation local.sstriple_consequence by (fastforce simp add: aentails_refl)
  from this show ?thesis
    using aentails_refl local.asepconj_comm local.awand_mp local.sstriple_consequence by fastforce
qed

lemma sstriple_gather_spec':
    notes asepconj_simp [simp]
      and aentails_intro [intro]
    fixes INV :: ‹nat ⇒ 'v list ⇒ 'a assert›
      and thunks :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression list›
  assumes ‹⋀i ls. i < length thunks ⟹ length ls = i ⟹ (Γ ; INV i ls ⊢ thunks ! i ⊣ (λv. INV (i+1) (ls @ [v])) ⨝ ρ ⨝ θ)›
    shows ‹Γ ; INV 0 [] ⊢ gather' thunks acc ⊣ (λrs. ⨆rs'. ⟨rs = acc @ rs'⟩ ⋆ INV (length thunks) rs') ⨝ ρ ⨝ θ›
  using assms 
proof (induction thunks arbitrary: INV acc)
  case Nil
  then show ?case
    by (auto simp: gather'_nil apure_def urust_eval_predicate_literal
       eval_value_def eval_abort_def eval_return_def sstriple_def atriple_rel_def is_local_def
      local.asepconj_comm local.asepconj_weaken2I)
next
  case (Cons t thunks)
  then have  first: ‹Γ ; INV 0 [] ⊢ t ⊣ (λv. INV 1 [v]) ⨝ ρ ⨝ θ›
    by fastforce
  have ‹Γ ; INV 1 [r0] ⊢ gather' thunks (acc @ [r0]) ⊣
        (λrs. ⨆rs'. ⟨rs = (acc @ rs')⟩ ⋆ INV (length (t # thunks)) rs') ⨝ ρ ⨝ θ› for r0
  proof -
    have ‹Γ ; INV (i+1) (r0 # ls) ⊢ thunks ! i ⊣ (λv. INV ((i+1)+1) ((r0 # ls) @ [v])) ⨝ ρ ⨝ θ›
      if  ‹i < length thunks› and ‹length ls = i› for i and ls :: ‹'v list›
      using that Cons.prems[where i=‹i+1› and ls=‹r0 # ls›] by fastforce
    with Cons.IH[where INV=‹λi ls. INV (i+1) (r0 # ls)› and acc=‹acc @ [r0]›] 
    have ‹Γ ; INV 1 [r0] ⊢ gather' thunks (acc @ [r0]) ⊣
          (λrs. ⨆rs'. ⟨rs = (acc @ (r0 # rs'))⟩ ⋆ INV (length (t # thunks)) (r0 # rs')) ⨝ ρ ⨝ θ›
      by simp
    moreover 
    have ‹⋀rs. (⨆rs'. ⟨rs = (acc @ (r0 # rs'))⟩ ⋆ INV (Suc (length thunks)) (r0 # rs')) ⤏
          (⨆rs'. ⟨rs = (acc @ rs')⟩ ⋆ INV (Suc (length thunks)) rs')›
      by blast
    ultimately show ?thesis
      by (meson aentails_refl local.aexists_entailsL local.aexists_entailsR local.sstriple_consequence)
  qed
  then show ?case
    by (metis (no_types, lifting) first gather'_cons sstriple_bindI)
qed

lemma sstriple_gather_spec:
    notes aentails_intro [intro]
    fixes INV :: ‹nat ⇒ 'v list ⇒ 'a assert›
      and thunks :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression list›
  assumes ‹⋀i ls. ucincl (INV i ls)›
      and ‹⋀i ls. i < length thunks ⟹ length ls = i ⟹
            Γ ; INV i ls ⊢ thunks ! i ⊣ (λv. INV (i+1) (ls @ [v])) ⨝ ρ ⨝ θ›
    shows ‹Γ ; INV 0 [] ⊢ gather thunks ⊣ (λrs. INV (length thunks) rs) ⨝ ρ ⨝ θ›
proof -
  from assms and gather_spec'[where INV=INV and thunks=thunks] have
        ‹Γ ; INV 0 [] ⊢ gather thunks ⊣ (λrs. ⨆rs'. ⟨rs = [] @ rs'⟩ ⋆ INV (length thunks) rs') ⨝ ρ ⨝ θ›
    unfolding gather_def using sstriple_gather_spec' by blast
  from this have ‹Γ ; INV 0 [] ⊢ gather thunks ⊣ (λrs. ⨆rs'. ⟨rs = rs'⟩ ⋆ INV (length thunks) rs') ⨝ ρ ⨝ θ›
    by fastforce
  moreover have ‹⋀rs. (⨆rs'. ⟨rs = rs'⟩ ⋆ INV (length thunks) rs') ⤏ INV (length thunks) rs›
    using assms by (simp add: asat_simp aentails_def)
  ultimately show ?thesis
    using sstriple_consequence by blast
qed

lemma sstriple_gather_framed:
    notes aentails_intro [intro]
    fixes thunks :: ‹('a, 'v, 'r, 'abort, 'i prompt, 'o prompt_output) expression list›
  assumes ‹⋀p r. ucincl (INV p r)›
      and ‹⋀i res. i < length thunks ⟹ length res = i ⟹ Γ ; INV i res ⊢ thunks ! i ⊣ (λv. INV (i+1) (res @ [v])) ⨝ τ ⨝ θ›
  shows ‹Γ ; INV 0 [] ⋆ ((⨅r. (INV (length thunks) r ↠ ψ r)) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r)) ⊢ gather thunks ⊣ ψ ⨝ ρ ⨝ χ›
proof -
  let ?pc = ‹((⨅r. (INV (length thunks) r ↠ ψ r)) ⊓ (⨅r. τ r ↠ ρ r) ⊓ (⨅r. θ r ↠ χ r))›
  {
    fix i and res :: ‹'v list›
    assume ‹i < length thunks›
       and ‹length res = i›
    from this have ‹Γ ; INV i res ⊢ thunks ! i ⊣ (λr. INV (i+1) (res @ [r])) ⨝ τ ⨝ θ›
      using assms ‹i < length thunks› by auto
    moreover have ‹Γ ; INV i res ⋆ ?pc ⊢
          (thunks ! i) ⊣ (λr. INV (i+1) (res @ [r]) ⋆ ?pc) ⨝ (λr. τ r ⋆ ?pc) ⨝ (λr. θ r ⋆ ?pc)›
      using assms calculation by (intro sstriple_frame_rule, force)
    moreover have ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
    proof -
      have ‹⋀r. τ r ⋆ (⨅r. τ r ↠ ρ r) ⤏ ρ r›
        by (meson aentails_refl aentails_trans aforall_entailsL asepconj_mono3 awand_counit)
      from this show ‹⋀r. τ r ⋆ ?pc ⤏ ρ r›
        by (meson aentails_fold_def aentails_inter_weaken aentails_inter_weaken2 asepconj_mono awand_adjointI)
    qed
    moreover have ‹⋀a. θ a ⋆ ?pc ⤏ χ a›
    proof -
      have ‹⋀a. θ a ⋆ (⨅a. θ a ↠ χ a) ⤏ χ a›
        by (meson aentails_refl aentails_trans aforall_entailsL asepconj_mono3 awand_counit)
      from this show ‹⋀a. θ a ⋆ ?pc ⤏ χ a›
        by (meson aentails_fold_def aentails_inter_weaken aentails_inter_weaken2 asepconj_mono awand_adjointI)
    qed
    ultimately have ‹Γ ; INV i res ⋆ ?pc ⊢ thunks ! i ⊣ (λr. INV (i+1) (res @ [r]) ⋆ ?pc) ⨝ ρ ⨝ χ›
      by - (rule sstriple_consequence, assumption, rule aentails_refl, rule aentails_refl, force)
  }
  from this have ‹Γ ; INV 0 [] ⋆ ?pc ⊢
        gather thunks ⊣ (λr. INV (length thunks) r ⋆ ?pc) ⨝ ρ ⨝ χ›
    using assms by (auto intro!: ucincl_intros sstriple_gather_spec[where INV=‹λi' res'. INV i' res' ⋆ ?pc› and thunks=thunks])
  moreover have ‹⋀r. INV (length thunks) r ⋆?pc
                 ⤏ INV (length thunks) r ⋆ (⨅r. (INV (length thunks) r ↠ ψ r))›
    by (meson aentails_refl local.aentails_int local.asepconj_mono)
  moreover have ‹⋀r. INV (length thunks) r ⋆ (⨅r. (INV (length thunks) r ↠ ψ r))  ⤏ ψ r›
    by (metis (no_types, lifting) aentails_refl local.aforall_entailsL local.asepconj_AC(1) local.awand_adjoint)
  ultimately have ‹Γ ; INV 0 [] ⋆ ?pc ⊢ gather thunks ⊣ ψ ⨝ ρ ⨝ χ›
    by (meson aentails_refl aentails_trans sstriple_consequence)
  then show ?thesis
    using aentails_refl local.asepconj_comm local.awand_mp local.sstriple_consequence by fastforce
qed

lemma is_local_eqI:
  assumes ‹⋀σ σ'. σ ⊨ φ ⋆ ⊤ ⟹ R σ σ' = S σ σ'›
  shows ‹is_local R φ = is_local S φ›
proof -
  from assms have ‹⋀σ σ'. σ ⊨ φ ⟹ R σ σ' = S σ σ'›
    by (simp add: asepconj_weakenI)
  from this and assms show ?thesis
    by (clarsimp simp add: is_local_def asepconjI)
qed

lemma sstriple_yield_handler_refine:
  assumes ‹Θ ≲ Γ›
      and ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ ⊥›
    shows ‹Θ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ ⊥›
proof -
  from assms have ref: ‹yield_handler_nondet_basic_refines (yh Θ) (yh Γ)›
    by simp
  { fix σ assume ‹σ ⊨ φ ⋆ ⊤›
    from this and assms have ‹⋀a σ'. σ ↝⇩a⟨yh Γ, e⟩ (a, σ') ⟷ False›
      by (metis asat_connectives_characterisation(2) bot_apply asepconj_ident2
        atripleE stripleE_abort ucincl_UNIV ucincl_empty striple_from_sstripleI)
    from this have no_abort: ‹(yh Γ, e) ⋄⇩a σ = {}›
      by (simp add: abort_evaluations_def)
    from ‹⋀a σ'. σ ↝⇩a⟨yh Γ, e⟩ (a, σ') ⟷ False› urust_eval_predicate_refine[OF ref no_abort] have
          eq_abort: ‹⋀a σ'. σ ↝⇩a⟨yh Θ, e⟩ (a, σ') ⟷ σ ↝⇩a⟨yh Γ, e⟩ (a, σ')› and
          eq_val: ‹⋀v σ'. σ ↝⇩v⟨yh Θ, e⟩ (v, σ') ⟷ σ ↝⇩v⟨yh Γ, e⟩ (v, σ')› and
          eq_res: ‹⋀r σ'. σ ↝⇩r⟨yh Θ, e⟩ (r, σ') ⟷ σ ↝⇩r⟨yh Γ, e⟩ (r, σ')› by simp+
  }
  note X = this
  from X have
    ‹is_local (eval_return (yh Θ) e) φ ⟷ is_local (eval_return (yh Γ) e) φ› and
    ‹is_local (eval_value (yh Θ) e) φ ⟷ is_local (eval_value (yh Γ) e) φ› and
    ‹is_local (eval_abort (yh Θ) e) φ ⟷ is_local (eval_abort (yh Γ) e) φ›
    by (intro is_local_eqI; clarsimp simp add: eval_value_def eval_abort_def eval_return_def)+
  moreover from assms have ‹Θ ; φ ⊢ e ⊣⇩w⇩e⇩a⇩k ψ ⨝ ξ ⨝ ⊥›
    using assms by (simp add: striple_yield_handler_refine striple_from_sstripleI)
  ultimately show ?thesis
    using assms by (clarsimp simp add: sstriple_striple)
qed

corollary sstriple_yield_handler_no_yield_implies_all:
  assumes ‹striple_context_no_yield ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ ⊥›
    shows ‹Γ ; φ ⊢ e ⊣ ψ ⨝ ξ ⨝ ⊥›
  using assms striple_context_refines_top sstriple_yield_handler_refine by blast

(*<*)
end

end
(*>*)