Theory 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