(*
 * 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 "validE P f Q E ≡ ∀s. P s ⟶ f ∙ s ?{ λv s. case v of Result r → Q r s | Exn e → E e s }"

open_bundle validE_syntax
begin
notation validE (‹(‹open_block notation=‹mixfix L1 Hoare triple››{_}/ _ /({_},/ {_}))›)
end

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}
\<Longrightarrow> {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})
\<Longrightarrow> {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