Theory AutoCorres2.L1Valid

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)


section ‹Hoare-Triples for L1 (internal use)›


theory L1Valid
imports L1Defs
begin

definition
  validE :: "('s ⇒ bool) ⇒ ('e, 'a, 's) exn_monad ⇒
             ('a ⇒ 's ⇒ bool) ⇒
             ('e ⇒ 's ⇒ bool) ⇒ bool"
("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄)")
where
  "⦃P⦄ f ⦃Q⦄,⦃E⦄ ≡ ∀s. P s ⟶ f ∙ s ?⦃ λv s. case v of Result r ⇒ Q r s | Exn e ⇒ E e s ⦄"

lemma hoareE_TrueI: "⦃P⦄ f ⦃λ_ _. True⦄, ⦃λr _. True⦄"
  by (simp add: validE_def runs_to_partial_def_old split: xval_splits)

lemma combine_validE: "⟦ ⦃ P ⦄ x ⦃ Q ⦄,⦃ E ⦄;
         ⦃ P' ⦄ x ⦃ Q' ⦄,⦃ E' ⦄ ⟧ ⟹
         ⦃ P and P' ⦄ x ⦃ λr. (Q r) and (Q' r) ⦄,⦃λr. (E r) and (E' r) ⦄"
  by (auto simp add: validE_def runs_to_partial_def_old split: xval_splits)

(* Weakest Precondition Proofs (WP) *)

lemma L1_skip_wp: "⦃ P () ⦄ L1_skip ⦃ P ⦄, ⦃ Q ⦄"
  apply (clarsimp simp: L1_skip_def validE_def)
  done

lemma L1_modify_wp: "⦃ λs. P () (f s) ⦄ L1_modify f ⦃ P ⦄, ⦃ Q ⦄"
  apply (clarsimp simp: L1_modify_def validE_def)
  apply (runs_to_vcg)
  done

lemma L1_spec_wp: "⦃ λs. ∀t. (s, t) ∈ f ⟶ P () t ⦄ L1_spec f ⦃ P ⦄, ⦃ Q ⦄"
  apply (clarsimp simp add: L1_spec_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_assume_wp: "⦃ λs. ∀t. ((), t) ∈ f s ⟶ P () t ⦄ L1_assume f ⦃ P ⦄, ⦃ Q ⦄"
  apply (clarsimp simp add: L1_assume_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_init_wp: "⦃ λs. ∀x. P () (f (λ_. x) s) ⦄ L1_init f ⦃ P ⦄, ⦃ Q ⦄"
  apply (clarsimp simp add: L1_init_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

(* Liveness proofs. (LP) *)

lemma L1_skip_lp: "⟦ ⋀s. P s ⟹ Q () s ⟧ ⟹ ⦃P⦄ L1_skip ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_skip_def)
  apply (clarsimp simp: validE_def)
  done

lemma L1_skip_lp_same_pre_post: "⦃P⦄ L1_skip ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_skip_lp)


lemma L1_guard_lp: "⟦ ⋀s. P s ⟹ Q () s ⟧ ⟹ ⦃P⦄ L1_guard e ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_guard_def guard_def)
  apply (clarsimp simp:  validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_guard_lp_same_pre_post: "⦃P⦄ L1_guard e ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_guard_lp)

lemma L1_guarded_lp_same_pre_post: "⦃P⦄ c ⦃λ_. P⦄, ⦃λ_. P⦄ 
⟹ ⦃P⦄ L1_guarded g c ⦃λ_. P⦄, ⦃λ_. P⦄"
  unfolding L1_defs L1_guarded_def validE_def
  by (auto simp add: runs_to_partial_def_old succeeds_bind reaches_bind)

lemma L1_guarded_lp_gets: "(⋀p. ⦃P⦄ (c p) ⦃λ_. P⦄, ⦃λ_. P⦄) 
⟹ ⦃P⦄ L1_guarded g (gets dest ⤜ (λp. c p)) ⦃λ_. P⦄, ⦃λ_. P⦄"
  unfolding L1_defs L1_guarded_def validE_def
  by (auto simp add: runs_to_partial_def_old succeeds_bind reaches_bind)





lemma L1_fail_lp: "⦃P⦄ L1_fail ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_fail_def validE_def)
  done

lemma L1_fail_lp_same_pre_post: "⦃P⦄ L1_fail ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_fail_lp)


lemma L1_throw_lp: "⟦ ⋀s. P s ⟹ E () s ⟧ ⟹ ⦃P⦄ L1_throw ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_throw_def validE_def)
  done

lemma L1_throw_lp_same_pre_post: "⦃P⦄ L1_throw ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_throw_lp)

lemma L1_spec_lp: "⟦ ⋀s r. ⟦ (s, r) ∈ e; P s ⟧ ⟹ Q () r ⟧ ⟹ ⦃P⦄ L1_spec e ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_spec_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_spec_lp_same_pre_post: "⟦ ⋀s r. ⟦ (s, r) ∈ e; P s ⟧ ⟹ P r ⟧ 
 ⟹ ⦃P⦄ L1_spec e ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_spec_lp)


lemma L1_modify_lp: "⟦ ⋀s. P s ⟹ Q () (f s) ⟧ ⟹ ⦃P⦄ L1_modify f ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_modify_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_modify_lp_same_pre_post: "⟦ ⋀s. P s ⟹ P (f s) ⟧ ⟹ ⦃P⦄ L1_modify f ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_modify_lp)

lemma L1_call_lp:
  "⟦ ⋀s r. P s ⟹ Q () (return_xf r (scope_teardown s r)); 
    ⋀s r. P s ⟹ E () (result_exn (scope_teardown s r) r)⟧ ⟹
  ⦃P⦄ L1_call scope_setup dest_fn scope_teardown result_exn return_xf ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_defs L1_call_def validE_def)
  apply (runs_to_vcg)
  apply (auto simp add: runs_to_partial_def_old reaches_bind)
  done

lemma L1_call_lp_same_pre_post:
  "⟦ ⋀s r. P s ⟹ P (return_xf r (scope_teardown s r)); 
    ⋀s r. P s ⟹ P (result_exn (scope_teardown s r) r)⟧ ⟹
  ⦃P⦄ L1_call scope_setup dest_fn scope_teardown result_exn return_xf ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_call_lp)

lemma L1_seq_lp: "⟦
    ⦃P1⦄ A ⦃Q1⦄,⦃E1⦄;
    ⦃P2⦄ B ⦃Q2⦄,⦃E2⦄;
    ⋀s. P s ⟹ P1 s;
    ⋀s. Q1 () s ⟹ P2 s;
    ⋀s. Q2 () s ⟹ Q () s;
    ⋀s. E1 () s ⟹ E () s;
    ⋀s. E2 () s ⟹ E () s
    ⟧ ⟹ ⦃P⦄ L1_seq A B ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_seq_def validE_def)
  apply (runs_to_vcg)
  apply (fastforce simp add: runs_to_partial_def_old reaches_bind split: xval_splits)
  done

lemma L1_seq_lp_same_pre_post: "⟦
    ⦃P⦄ A ⦃λ_. P⦄,⦃λ_. P⦄;
    ⦃P⦄ B ⦃λ_. P⦄,⦃λ_. P⦄
    ⟧ ⟹ ⦃P⦄ L1_seq A B ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_seq_lp)

lemma L1_condition_lp: "
  ⟦ ⦃P1⦄ A ⦃Q1⦄,⦃E1⦄;
    ⦃P2⦄ B ⦃Q2⦄,⦃E2⦄;
    ⋀s. P s ⟹ P1 s;
    ⋀s. P s ⟹ P2 s;
    ⋀s. Q1 () s ⟹ Q () s;
    ⋀s. Q2 () s ⟹ Q () s;
    ⋀s. E1 () s ⟹ E () s;
    ⋀s. E2 () s ⟹ E () s ⟧ ⟹
  ⦃P⦄ L1_condition c A B ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_condition_def validE_def)
  apply (runs_to_vcg)
   apply (fastforce simp add: runs_to_partial_def_old split: xval_splits)+
  done

lemma L1_condition_lp_same_pre_post: "
  ⟦⦃P⦄ A ⦃λ_. P⦄,⦃λ_. P⦄;
   ⦃P⦄ B ⦃λ_. P⦄,⦃λ_. P⦄
  ⟧ ⟹
  ⦃P⦄ L1_condition c A B ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_condition_lp)


lemma L1_catch_lp: "
  ⟦ ⦃P1⦄ A ⦃Q1⦄,⦃E1⦄;
    ⦃P2⦄ B ⦃Q2⦄,⦃E2⦄;
    ⋀s. P s ⟹ P1 s;
    ⋀s. E1 () s ⟹ P2 s;
    ⋀s. Q1 () s ⟹ Q () s;
    ⋀s. Q2 () s ⟹ Q () s;
    ⋀s. E2 () s ⟹ E () s ⟧ ⟹
  ⦃P⦄ L1_catch A B ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp: L1_catch_def validE_def)
  apply (runs_to_vcg)
  apply (fastforce simp add: runs_to_partial_def_old split: xval_splits)
  done

lemma L1_catch_lp_same_pre_post: "
  ⟦⦃P⦄ A ⦃λ_. P⦄,⦃λ_. P⦄;
   ⦃P⦄ B ⦃λ_. P⦄,⦃λ_. P⦄
  ⟧ ⟹
  ⦃P⦄ L1_catch A B ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_catch_lp)


lemma L1_init_lp: "⟦ ⋀s. P s ⟹ ∀x. Q () (f (λ_. x) s) ⟧ ⟹ ⦃P⦄ L1_init f ⦃Q⦄, ⦃E⦄"
  apply (clarsimp simp add:  L1_init_def validE_def)
  apply (runs_to_vcg)
  apply auto
  done

lemma L1_init_lp_same_pre_post: "⟦ ⋀s. P s ⟹ ∀x. P (f (λ_. x) s) ⟧ ⟹ ⦃P⦄ L1_init f ⦃λ_. P⦄, ⦃λ_. P⦄"
  by (rule L1_init_lp)


lemma validE_weaken:
  "⟦ ⦃P'⦄ A ⦃Q'⦄,⦃E'⦄; ⋀s. P s ⟹ P' s; ⋀r s. Q' r s ⟹ Q r s; ⋀r s. E' r s ⟹ E r s ⟧ ⟹ ⦃P⦄ A ⦃Q⦄,⦃E⦄"
  apply (fastforce simp add: validE_def runs_to_partial_def_old split: xval_splits)
  done

lemma L1_while_lp:
  assumes body_lp: "⦃ P' ⦄ B ⦃ Q' ⦄, ⦃ E' ⦄"
  and p_impl: "⋀s. P s ⟹ P' s"
  and q_impl: "⋀s. Q' () s ⟹ Q () s"
  and e_impl: "⋀s. E' () s ⟹ E () s"
  and inv: " ⋀s. Q' () s ⟹ P' s"
  and inv': " ⋀s. P' s ⟹ Q' () s"
shows "⦃ P ⦄ L1_while c B ⦃ Q ⦄,⦃ E ⦄"
  apply (rule validE_weaken [where P'=P' and Q'=Q' and E'=E'])
     apply (clarsimp simp: L1_while_def validE_def)

     apply (rule runs_to_partial_whileLoop_exn  [where I="λr s. (case r of Exn e ⇒ E' () s | _ ⇒  P' s)"])
        apply simp
       apply (simp add: inv')
      apply (simp)
     apply simp
  subgoal using body_lp
    by ( simp add: inv validE_def runs_to_partial_def_old split: xval_splits)
    apply (simp add: p_impl)
   apply (simp add: q_impl)
  apply (simp add: e_impl)
  done

lemma L1_while_lp_same_pre_post:
  assumes body_lp: "⦃ P ⦄ B ⦃ λ_. P⦄, ⦃ λ_. P ⦄"
  shows "⦃ P ⦄ L1_while c B ⦃λ_. P ⦄,⦃ λ_. P ⦄"
  by (rule L1_while_lp [OF body_lp])

lemma on_exit_lp_same_pre_post:
  assumes cleanup: "⋀s t. (s,t) ∈ cleanup ⟹  P t = P s"
  assumes c: "⦃P⦄ c ⦃λ_. P⦄, ⦃λ_. P⦄"
  shows "⦃P⦄ on_exit c cleanup ⦃λ_. P⦄, ⦃λ_. P⦄"
  apply (clarsimp simp add: validE_def on_exit'_def on_exit_def)
  apply (runs_to_vcg)
  using cleanup c
  apply (fastforce simp add: validE_def runs_to_partial_def_old succeeds_bind   
      reaches_bind default_option_def Exn_def split: xval_splits)
  done

lemma seqE:
  assumes f_valid: "⦃A⦄ f ⦃B⦄,⦃E⦄"
  assumes g_valid: "⋀x. ⦃B x⦄ g x ⦃C⦄,⦃E⦄"
  shows "⦃A⦄ do { x ← f; g x } ⦃C⦄,⦃E⦄"
  using assms
  apply (clarsimp simp add: validE_def)
  apply (runs_to_vcg)
  apply (fastforce simp add: runs_to_partial_def_old split: xval_splits)
  done

named_theorems with_fresh_stack_ptr_lp_same_pre_post
context stack_heap_state
begin
lemma with_fresh_stack_ptr_lp_same_pre_post[with_fresh_stack_ptr_lp_same_pre_post]: 
  assumes c: "⋀p. ⦃P⦄ (c p) ⦃λ_. P⦄, ⦃λ_. P⦄"
  assumes htd_indep: "⋀s g. P (htd_upd g s) = P s"
  assumes hmem_indep: "⋀s f. P (hmem_upd f s) = P s"
shows "⦃P⦄ with_fresh_stack_ptr n g c ⦃λ_. P⦄, ⦃λ_. P⦄"
  apply (clarsimp simp add: with_fresh_stack_ptr_def)
  apply (rule seqE [where B="λ_. P"])
  subgoal
    apply (clarsimp simp add: validE_def)
    apply (runs_to_vcg)
    by (clarsimp simp add:  htd_indep hmem_indep)
  subgoal
    apply (rule on_exit_lp_same_pre_post [OF _ c])
    apply (auto simp add: htd_indep hmem_indep)
    done
  done
end

lemma validE_weaken_dependent:
  assumes dep_spec: "⋀s. P s ⟹ ⦃P' s⦄ A ⦃Q' s⦄, ⦃E' s⦄" 
  assumes weaken_pre: "⋀s. P s ⟹ P' s s"
  assumes weaken_norm: "(⋀s r t. P' s s ⟹ Q' s r t ⟹ Q r t)" 
  assumes weaken_exn: "(⋀s r t. P' s s ⟹ E' s r t ⟹ E r t)"
  shows "⦃P⦄ A ⦃Q⦄, ⦃E⦄"
  using assms
  apply (fastforce simp add: validE_def runs_to_partial_def_old split: xval_splits)
  done

lemma validE_weaken_dependent_same:
  assumes dep_spec: "⋀s. P s ⟹ ⦃P' s⦄ A ⦃λ_. P' s⦄, ⦃λ_. P' s⦄" 
  assumes weaken_post: "(⋀s t. P' s t ⟹ P t)" 
  assumes weaken_pre: "⋀s. P s ⟹ P' s s"
  shows "⦃P⦄ A ⦃λ_. P⦄, ⦃λ_. P⦄"
  using dep_spec weaken_pre weaken_post weaken_post 
  by (rule validE_weaken_dependent)

end