(******************************************************************************
 * Clean
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

theory Clean_Symbex
  imports Clean
begin


section‹Clean Symbolic Execution Rules ›


subsection‹Basic NOP - Symbolic Execution Rules. ›

text‹ As they are equalities, they can also
  used as program optimization rules. ›

lemma non_exec_assign  : 
assumes "▹ σ"
shows "(σ ⊨ ( _ ← assign f; M)) = ((f σ) ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success)

lemma non_exec_assign'  : 
assumes "▹ σ"
shows "(σ ⊨ (assign f;- M)) = ((f σ) ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)

lemma exec_assign  : 
assumes "exec_stop σ"
shows "(σ ⊨ ( _ ← assign f; M)) = (σ ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success)     

lemma exec_assign'  : 
assumes "exec_stop σ"
shows "(σ ⊨ (assign f;- M)) = (σ ⊨ M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)     

subsection‹Assign Execution Rules. ›

lemma non_exec_assign_global  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← assign_global upd rhs; M)) = ((upd (λ_. rhs σ) σ) ⊨ M)"
by(simp add: assign_global_def non_exec_assign assms)

lemma non_exec_assign_global'  : 
assumes "▹ σ"
shows   "(σ ⊨ (assign_global upd rhs;- M)) = ((upd (λ_. rhs σ) σ) ⊨ M)"
  by (metis (full_types) assms bind_SE'_def non_exec_assign_global)


lemma exec_assign_global  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← assign_global upd rhs; M)) = ( σ ⊨ M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success)

lemma exec_assign_global'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (assign_global upd rhs;- M)) = ( σ ⊨ M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success bind_SE'_def)

lemma non_exec_assign_local  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← assign_local upd rhs; M)) = ((upd (upd_hd (λ_. rhs σ)) σ) ⊨ M)"
  by(simp add: assign_local_def non_exec_assign assms)

lemma non_exec_assign_local'  : 
assumes "▹ σ"
shows   "(σ ⊨ (assign_local upd rhs;- M)) = ((upd (upd_hd (λ_. rhs σ)) σ) ⊨ M)"
  by (metis assms bind_SE'_def non_exec_assign_local)

lemmas non_exec_assign_localD'= non_exec_assign[THEN iffD1]

lemma exec_assign_local  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← assign_local upd rhs; M)) = ( σ ⊨ M)"
  by (simp add: assign_local_def assign_def assms exec_bind_SE_success)

lemma exec_assign_local'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( assign_local upd rhs;- M)) = ( σ ⊨ M)" 
  unfolding assign_local_def assign_def 
  by (simp add: assms exec_bind_SE_success2)

lemmas exec_assignD = exec_assign[THEN iffD1]
thm exec_assignD

lemmas exec_assignD' = exec_assign'[THEN iffD1]
thm exec_assignD'

lemmas exec_assign_globalD =  exec_assign_global[THEN iffD1]

lemmas exec_assign_globalD' =  exec_assign_global'[THEN iffD1]

lemmas exec_assign_localD = exec_assign_local[THEN iffD1]
thm exec_assign_localD

lemmas exec_assign_localD' = exec_assign_local'[THEN iffD1]



subsection‹Basic Call Symbolic Execution Rules. ›



lemma exec_call_0  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← call_0_C M; M')) = (σ ⊨ M')"
  by (simp add: assms call_0_{C_def} exec_bind_SE_success)

lemma exec_call_0'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_0_C M;- M')) = (σ ⊨ M')"
  by (simp add: assms bind_SE'_def exec_call_0)



lemma exec_call_1  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( x ← call_1_C M A₁; M' x)) = (σ ⊨ M' undefined)"
  by (simp add: assms call_1_{C_def} call_{C_def} exec_bind_SE_success)

lemma exec_call_1'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_1_C M A₁;- M')) = (σ ⊨ M')"
  by (simp add: assms bind_SE'_def exec_call_1)

lemma exec_call  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( x ← call_C M A₁; M' x)) = (σ ⊨ M' undefined)"
  by (simp add: assms call_{C_def} call_1_{C_def} exec_bind_SE_success)

lemma exec_call'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_C M A₁;- M')) = (σ ⊨ M')"
  by (metis assms call_1_{C_def} exec_call_1')

lemma exec_call_2  : 
assumes "exec_stop σ"
shows   "(σ ⊨ ( _ ← call_2_C M A₁ A₂; M')) = (σ ⊨ M')"
  by (simp add: assms call_2_{C_def} exec_bind_SE_success)

lemma exec_call_2'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (call_2_C M A₁ A₂;- M')) = (σ ⊨ M')"
  by (simp add: assms bind_SE'_def exec_call_2)

subsection‹Basic Call Symbolic Execution Rules. ›

lemma non_exec_call_0  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← call_0_C M; M')) = (σ ⊨ M;- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_0_{C_def} valid_SE_def)

lemma non_exec_call_0'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_0_C M;- M') = (σ ⊨ M;- M')"
  by (simp add: assms bind_SE'_def non_exec_call_0)

lemma non_exec_call_1  : 
assumes "▹ σ"
shows   "(σ ⊨ ( x ← (call_1_C M (A₁)); M' x)) = (σ ⊨ (x ← M (A₁ σ); M' x))"
  by (simp add: assms bind_SE'_def call_{C_def} bind_SE_def call_1_{C_def} valid_SE_def)

lemma non_exec_call_1'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_1_C M (A₁);- M') = (σ ⊨ M (A₁ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_1)

(* general case *)
lemma non_exec_call  : 
assumes "▹ σ"
shows   "(σ ⊨ ( x ← (call_C M (A₁)); M' x)) = (σ ⊨ (x ← M (A₁ σ); M' x))"
  by (simp add: assms call_{C_def} bind_SE'_def bind_SE_def call_1_{C_def} valid_SE_def)

lemma non_exec_call'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_C M (A₁);- M') = (σ ⊨ M (A₁ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call)


lemma non_exec_call_2  : 
assumes "▹ σ"
shows   "(σ ⊨ ( _ ← (call_2_C M (A₁) (A₂)); M')) = (σ ⊨ M (A₁ σ) (A₂ σ);- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_2_{C_def} valid_SE_def)

lemma non_exec_call_2'  : 
assumes "▹ σ"
shows   "(σ ⊨ call_2_C M (A₁) (A₂);- M') = (σ ⊨ M (A₁ σ) (A₂ σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_2)


subsection‹Conditional. ›

lemma exec_If_{C_IfSE}  : 
assumes "▹ σ"
shows   "((if_C P then B₁ else B₂ fi))σ = ((if_SE P then B₁ else B₂ fi)) σ "
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def
  by (simp add: assms bind_SE_def if_C_def)
    
    
lemma valid_exec_If_C  : 
assumes "▹ σ"
shows   "(σ ⊨ (if_C P then B₁ else B₂ fi);-M) = (σ ⊨ (if_SE P then B₁ else B₂ fi);-M)"
  by (meson assms exec_If_{C_IfSE} valid_bind'_cong)


      
lemma exec_If_C'  : 
assumes "exec_stop σ"
shows   "(σ ⊨ (if_C P then B₁ else B₂ fi);-M) = (σ ⊨ M)"    
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
    by (simp add: assms if_C_def)
    
lemma exec_While_C'  : 
assumes "exec_stop σ"
shows  "(σ ⊨ (while_C P do B₁ od);-M) = (σ ⊨ M)"    
  unfolding while_C_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
  apply simp using assms by blast    


    
    
lemma if_{C_cond_cong} : "f σ = g σ ==> (if_C f then c else d fi) σ =
                                     (if_C g then c else d fi) σ"
  unfolding if_C_def
   by simp 
   
 
subsection‹Break - Rules. ›

lemma break_assign_skip [simp]: "(break ;- assign f) = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def bind_SE'_def   bind_SE_def
  by auto



lemma break_if_skip [simp]: "(break ;- if_C b then c else d fi) = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def if_C_def bind_SE'_def   bind_SE_def
  by auto
    
                       
lemma break_while_skip [simp]: "(break ;- while_C b do c od) = break"
  apply(rule ext)
  unfolding while_C_def skip_{SE_def} unit_SE_def bind_SE'_def bind_SE_def break_def exec_stop_def
  by simp

    
lemma unset_break_idem [simp] : 
 "(unset_break_status ;- unset_break_status ;- M) = (unset_break_status ;- M)"
  apply(rule ext)  unfolding unset_break_status_def bind_SE'_def bind_SE_def by auto

lemma return_cancel1_idem [simp] : 
 "(return(E) ;- X :==_G E' ;- M) = ( return_C X E ;- M)"
  apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def return_{C_def} return_{C0_def} assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
  apply auto
  by (simp add: exec_stop_def set_return_status_def)
    
lemma return_cancel2_idem [simp] : 
 "( return(E) ;- X :==_L E' ;- M) = ( return_C X E ;- M)"
    apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def return_{C_def} return_{C0_def} assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
   apply auto
  by (simp add: exec_stop_def set_return_status_def)


subsection‹While. ›     

lemma while_{C_skip} [simp]: "(while_C (λ x. False) do c od) = skip_SE"
  apply(rule ext)
  unfolding while_C_def skip_{SE_def} unit_SE_def
  apply auto
  unfolding exec_stop_def skip_{SE_def} unset_break_status_def bind_SE'_def unit_SE_def bind_SE_def
  by simp
 

txt‹ Various tactics for various coverage criteria ›

definition while_k :: "nat → (('σ_ext) control_state_ext → bool)
                        → (unit, ('σ_ext) control_state_ext)MON_SE
                        → (unit, ('σ_ext) control_state_ext)MON_SE"
where     "while_k _ ≡ while_C"


text‹Somewhat amazingly, this unfolding lemma crucial for symbolic execution still holds ...
 Even in the presence of break or return...›
lemma exec_while_C : 
"(σ ⊨ ((while_C b do c od) ;- M)) =
 (σ ⊨ ((if_C b then c ;- ((while_C b do c od) ;- unset_break_status) else skip_SE fi) ;- M))"
proof (cases "exec_stop σ")
  case True
  then show ?thesis 
    by (simp add: True exec_If_C' exec_While_C')
next
  case False
  then show ?thesis
    proof (cases "¬ b σ")
      case True
      then show ?thesis
        apply(subst valid_bind'_cong)
        using ‹¬ exec_stop σ› apply simp_all
        apply (auto simp: skip_{SE_def} unit_SE_def)
          apply(subst while_C_def, simp)
         apply(subst bind'_cong)
         apply(subst MonadSE.while_SE_unfold)
          apply(subst if_{SE_cond_cong} [of _ _ "λ_. False"])
          apply simp_all
        apply(subst if_{C_cond_cong} [of _ _ "λ_. False"], simp add: )
        apply(subst exec_If_{C_IfSE},simp_all)
        by (simp add: exec_stop_def unset_break_status_def)
    next
      case False
      have * : "b σ"  using False by auto
      then show ?thesis
           unfolding while_k_def 
           apply(subst  while_C_def)
           apply(subst  if_C_def)
           apply(subst  valid_bind'_cong)
            apply (simp add: ‹¬ exec_stop σ›)
           apply(subst  (2) valid_bind'_cong)
            apply (simp add: ‹¬ exec_stop σ›)
            apply(subst MonadSE.while_SE_unfold)
            apply(subst valid_bind'_cong)
            apply(subst bind'_cong)
             apply(subst if_{SE_cond_cong} [of _ _ "λ_. True"])
              apply(simp_all add:   ‹¬ exec_stop σ› )
            apply(subst bind_assoc', subst bind_assoc')
            proof(cases "c σ")
              case None
              then show "(σ ⊨ c;-((while_SE (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M) =
                         (σ ⊨ c;-(while_C b do c od) ;- unset_break_status ;- M)"
                by (simp add: bind_SE'_def exec_bind_SE_failure)
            next
              case (Some a)
              then show "(σ ⊨ c ;- ((while_SE (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M) =
                         (σ ⊨ c ;- (while_C b do c od) ;- unset_break_status ;- M)"
                apply(insert ‹c σ = Some a›, subst (asm) surjective_pairing[of a])
                apply(subst exec_bind_SE_success2, assumption)
                apply(subst exec_bind_SE_success2, assumption)
                proof(cases "exec_stop (snd a)")
                  case True
                  then show "(snd a ⊨((while_SE (λσ. ¬ exec_stop σ ∧ b σ) do c od);-unset_break_status);-M)=
                             (snd a ⊨ (while_C b do c od) ;- unset_break_status ;- M)"
                       by (metis (no_types, lifting) bind_assoc' exec_While_C' exec_skip if_SE_D2' 
                                                  skip_{SE_def} while_SE_unfold)
                next
                  case False
                  then show "(snd a ⊨ ((while_SE(λσ. ¬exec_stop σ ∧ b σ) do c od);-unset_break_status);-M)=
                             (snd a ⊨ (while_C b do c od) ;- unset_break_status ;- M)"
                          unfolding  while_C_def
                          by(subst (2) valid_bind'_cong,simp)(simp)
                qed       
            qed  
    qed
qed
(* ... although it is, oh my god, amazingly complex to prove. *)


lemma while_k_SE : "while_C = while_k k"
by (simp only: while_k_def)


corollary exec_while_k : 
"(σ ⊨ ((while_k (Suc n) b c) ;- M)) =
 (σ ⊨ ((if_C b then c ;- (while_k n b c) ;- unset_break_status else skip_SE fi) ;- M))"
  by (metis exec_while_C while_k_def)
    

txt‹ Necessary prerequisite: turning ematch and dmatch into a proper Isar Method. ›
(* TODO : this code shoud go to TestGen Method setups *)
ML‹
 
  method_setup b tac =
 Method.setup b
 (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o K (tac ctxt rules))))
 
  _ =
 Theory.setup ( method_setup @{binding ematch} ematch_tac "fast elimination matching"
 #> method_setup @{binding dmatch} dmatch_tac "fast destruction matching"
 #> method_setup @{binding match} match_tac "resolution based on fast matching")
 
 ›

lemmas exec_while_kD = exec_while_k[THEN iffD1]

end