Theory AutoCorres2.ModifiesProofs

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

theory ModifiesProofs
imports CLanguage
begin

(* Rules for breaking down modifies goals before feeding them to the VCG.
   Helps avoid some pathological performance issues. *)

definition
  modifies_inv_refl :: "('a  'a set)  bool"
where
  "modifies_inv_refl P  x. x  P x"

definition
  modifies_inv_incl :: "('a  'a set)  bool"
where
  "modifies_inv_incl P  x y. y  P x  P y  P x"

definition
  modifies_inv_prop :: "('a  'a set)  bool"
where
  "modifies_inv_prop P  modifies_inv_refl P  modifies_inv_incl P"

lemma modifies_inv_prop:
  "modifies_inv_refl P  modifies_inv_incl P  modifies_inv_prop P"
  by (simp add: modifies_inv_prop_def)

named_theorems modifies_inv_intros

locale modifies_assertion =
  fixes P :: "'s  's set"
  assumes p: "modifies_inv_prop P"
begin

lemmas modifies_inv_prop' =
  p[unfolded modifies_inv_prop_def modifies_inv_refl_def modifies_inv_incl_def]

lemma modifies_inv_prop_lift:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F(P σ) c (P σ),(P σ)"
  using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)

lemma modifies_inv_prop_lower:
  assumes c: "σ. Γ,Θ⊢⇘/F(P σ) c (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} c (P σ),(P σ)"
  using modifies_inv_prop' by (fastforce intro: c hoarep.Conseq)

text ‹Note that the C-Parser associates sequential composition to the right. So the first statement
is typically already an 'atomic' statement (or at least no further sequential composition) 
that can be solved. We place it as the second precondition because the modifies-tactic follows the 
canonical order of tactical reasoning and solves the subgoals from the back. 
So termc1 is already solved before further decomposing termc2. This keeps
the number of subgoals (and thus the overall goal-state) small.
›
lemma modifies_inv_Seq [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c2 (P σ),(P σ)" "σ. Γ,Θ⊢⇘/F{σ} c1 (P σ),(P σ)" 
  shows "Γ,Θ⊢⇘/F{σ} c1 ;; c2 (P σ),(P σ)"
  by (intro modifies_inv_prop_lower HoarePartial.SeqSwap[OF c[THEN modifies_inv_prop_lift]])

lemma modifies_inv_Cond [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c1 (P σ),(P σ)" "σ. Γ,Θ⊢⇘/F{σ} c2 (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} Cond b c1 c2 (P σ),(P σ)"
  by (auto intro: HoarePartial.Cond c)

lemma modifies_inv_Guard_strip [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/UNIV{σ} c (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/UNIV{σ} Guard f b c (P σ),(P σ)"
  by (rule HoarePartial.GuardStrip[OF subset_refl c UNIV_I])

lemma modifies_inv_Skip [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} SKIP (P σ),(P σ)"
  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)

lemma modifies_inv_Skip' [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} SKIP (P σ)"
  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Skip)

lemma modifies_inv_whileAnno [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} whileAnno b I V c (P σ),(P σ)"
  apply (rule HoarePartial.reannotateWhileNoGuard[where I="P σ"])
  by (intro HoarePartial.While hoarep.Conseq;
      fastforce simp: modifies_inv_prop' intro: modifies_inv_prop_lift c)

lemma modifies_inv_While [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} While b c (P σ),(P σ)"
  by (intro modifies_inv_whileAnno[unfolded whileAnno_def] c)

lemma modifies_inv_Throw [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} THROW (P σ),(P σ)"
  using modifies_inv_prop' by (auto intro: modifies_inv_prop_lift HoarePartial.Throw)

lemma modifies_inv_Catch [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c1 (P σ),(P σ)"
             "σ. Γ,Θ⊢⇘/F{σ} c2 (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} TRY c1 CATCH c2 END (P σ),(P σ)"
  by (intro modifies_inv_prop_lower HoarePartial.Catch[OF c[THEN modifies_inv_prop_lift]])

lemma modifies_inv_Catch_all [modifies_inv_intros]:
  assumes 1: "σ. Γ,Θ⊢⇘/F{σ} c1 (P σ),(P σ)"
  assumes 2: "σ. Γ,Θ⊢⇘/F{σ} c2 (P σ)"
  shows "Γ,Θ⊢⇘/F{σ} TRY c1 CATCH c2 END (P σ)"
  apply (intro HoarePartial.Catch[OF 1] hoarep.Conseq, clarsimp)
  apply (metis modifies_inv_prop' 2 singletonI)
  done

lemma modifies_inv_switch_Nil [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} switch v [] (P σ),(P σ)"
  by (auto intro: modifies_inv_Skip)

lemma modifies_inv_switch_Cons [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} c (P σ),(P σ)"
             "σ. Γ,Θ⊢⇘/F{σ} switch p vcs (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} switch p ((v,c) # vcs) (P σ),(P σ)"
  by (auto intro: c modifies_inv_Cond)

end

locale modifies_state_assertion = modifies_assertion P for
  P :: "('g, 'l, 'e, 'x) state_scheme  ('g, 'l, 'e, 'x) state_scheme set" +
  assumes p: "modifies_inv_prop P"
begin

lemma modifies_inv_creturn [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} Basic (λs. xfu (λ_. v s) s) (P σ),(P σ)"
             "σ. Γ,Θ⊢⇘/F{σ} Basic (rtu (λ_. Return)) (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} creturn rtu xfu v (P σ),(P σ)"
  unfolding creturn_def by (intro p c modifies_inv_intros)

lemma modifies_inv_creturn_void [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} Basic (rtu (λ_. Return)) (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} creturn_void rtu (P σ),(P σ)"
  unfolding creturn_void_def by (intro p c modifies_inv_intros)

lemma modifies_inv_cbreak [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} Basic (rtu (λ_. Break)) (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} cbreak rtu (P σ),(P σ)"
  unfolding cbreak_def by (intro p c modifies_inv_intros)

lemma modifies_inv_ccatchbrk [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} ccatchbrk rt (P σ),(P σ)"
  unfolding ccatchbrk_def by (intro p modifies_inv_intros)

lemma modifies_inv_cgoto [modifies_inv_intros]:
  assumes c: "σ. Γ,Θ⊢⇘/F{σ} Basic (rtu (λ_. Goto l)) (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} cgoto l rtu (P σ),(P σ)"
  unfolding cgoto_def by (intro p c modifies_inv_intros)

lemma modifies_inv_ccatchgoto [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} ccatchgoto l rt (P σ),(P σ)"
  unfolding ccatchgoto_def by (intro p modifies_inv_intros)

lemma modifies_inv_ccatchreturn [modifies_inv_intros]:
  shows "Γ,Θ⊢⇘/F{σ} ccatchreturn rt (P σ),(P σ)"
  unfolding ccatchreturn_def by (intro p modifies_inv_intros)

end

lemma On_Exit_wp:
  assumes cleanup: "Γ,Θ⊢⇘/FR cleanup Q, A"
  assumes cleanup_catch: "Γ,Θ⊢⇘/FB cleanup A, A"
  assumes c: "Γ,Θ⊢⇘/FP c R, B"
  shows "Γ,Θ⊢⇘/FP On_Exit c cleanup Q, A"
  unfolding On_Exit_def
  apply (rule HoarePartial.SeqSwap [where R=R])
   apply (rule HoarePartial.conseq_no_aux)
    apply (rule cleanup)
  apply simp
  apply (rule HoarePartial.Catch)
   apply (rule c)
  apply (rule HoarePartial.SeqSwap )
   apply (rule HoarePartial.Throw)
   apply (rule subset_refl)
  apply (rule cleanup_catch)
  done


lemma DynCom_fix_pre: "s  P. Γ,Θ⊢⇘/F{s} (c s) Q,A
      
      Γ,Θ⊢⇘/FP (DynCom c) Q,A"
  by (smt (verit, best) HoarePartial.conseq_exploit_pre Int_insert_left_if1 hoarep.DynCom inf_bot_left singletonD)

lemma "Γ,Θ⊢⇘/F{s. (t. (s, t)  r  t  Q)  (t. (s, t)  r)} Spec r Q,A"
  by (rule hoarep.Spec)

lemma hoarep_Spec_fixed: "(t. (s, t)  r)  Γ,Θ⊢⇘/F{s} Spec r {t. (s, t)  r},A"
  by (simp add: HoarePartial.Spec)

context stack_heap_state
begin

lemma With_Fresh_Stack_Ptr_tight:
  assumes c: "s p d vs bs. s  P  vs  init s  length vs = n  length bs = n * size_of TYPE('a)  
    (p, d)  stack_allocs n 𝒮 TYPE('a::mem_type) (htd s)    
           Γ,Θ⊢⇘/F{hmem_upd (fold (λi. heap_update_padding (p +p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)} 
             (c p) 
           {t.  bs. length bs = n * size_of TYPE('a)  hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t)  Q}, 
           {t.  bs. length bs = n * size_of TYPE('a)  hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t)  A}"
  assumes no_overflow: "StackOverflow  F"
  shows "Γ,Θ⊢⇘/FP With_Fresh_Stack_Ptr n init c Q, A"
  unfolding With_Fresh_Stack_Ptr_def
  apply (rule hoarep.Guarantee [OF no_overflow])
   apply (rule DynCom_fix_pre)
  apply (rule ballI)
  apply clarsimp
  apply (rule HoarePartial.Seq)
   apply (rule  hoarep_Spec_fixed)
   apply clarsimp
  subgoal using Ex_list_of_length 
    by (metis equals0I old.prod.exhaust)

  apply clarsimp
  apply (rule DynCom_fix_pre)
  apply (rule ballI)
  apply clarsimp
  apply (rule On_Exit_wp)



    apply (rule HoarePartial.Spec)
    apply (rule subset_refl)
   apply (rule HoarePartial.Spec)
   apply (rule subset_refl)
  subgoal premises prems for s vs p d' vsa bs
  proof -
    have eq1: "length vs = n" using prems by simp
    have eq2:"(allocated_ptrs n 𝒮 TYPE('a) (htd s) d') = p" using prems by (simp add: stack_allocs_allocated_ptrs)
    show ?thesis
      apply (simp add: eq1 eq2 Ex_list_of_length)
      apply (rule HoarePartialDef.conseqPost [OF c [where s1=s and vs1=vsa and d1=d' and p1=p]])
      using prems
         apply auto
      done
  qed
  done


lemma With_Fresh_Stack_Ptr_tight_wp:
  assumes conseq: "s p d vs bs. s  P  vs  init s  length vs = n   length bs = n * size_of TYPE('a)   
             (p, d)  stack_allocs n 𝒮 TYPE('a::mem_type) (htd s)  
           (hmem_upd (fold (λi. heap_update_padding (p +p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s))  R s p d vs"
  assumes c: "s p d vs bs. s  P  vs  init s  length vs = n   length bs = n * size_of TYPE('a)  
            (p, d)  stack_allocs n 𝒮 TYPE('a::mem_type) (htd s)  
           (hmem_upd (fold (λi. heap_update_padding (p +p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s))  R s p d vs  
           Γ,Θ⊢⇘/F(R s p d vs) (c p) 
             {t. bs. length bs = n * size_of TYPE('a)  hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t)  Q}, 
             {t. bs. length bs = n * size_of TYPE('a)  hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases n p) t)  A}"
  assumes no_overflow: "StackOverflow  F"
  shows "Γ,Θ⊢⇘/FP With_Fresh_Stack_Ptr n init c Q, A"
  apply (rule With_Fresh_Stack_Ptr_tight [OF _ no_overflow])
  subgoal for s p d vs bs
    apply (rule HoarePartial.conseq)
     apply (rule allI)
     apply (rule c[where s1=s and vs1=vs and d1=d])
          apply assumption
         apply assumption
        apply assumption
       apply assumption
      apply assumption
     apply (rule conseq)
         apply assumption
        apply assumption
       apply assumption
      apply assumption
     apply clarsimp
    subgoal premises prems 
    proof -
      from prems have eq: "length vs = n" by simp
      show ?thesis
        apply (simp add: eq)
        apply (rule conseq)
        using prems by auto
    qed
    done
  done



text ‹Caution: this WP-setup was developed to solve the modified clauses. It might not be the
 best fit for WP-style reasoning in general. Also note that it is currently not
 invoked by the automatic modifies-proofs triggerd by the C-parser as constWith_Fresh_Stack_Ptr is
 first decomposed by the @{thm modifies_inv_intros} (see the rule below).›
declaration fn phi =>
let
  val rule = Morphism.thm phi @{thm With_Fresh_Stack_Ptr_tight}
  fun tac cont_tac ctxt mode i = 
       resolve_tac ctxt [rule] i THEN 
       SOLVED_verbose "no_overflow" ctxt (simp_tac ctxt) (i + 1) THEN 
       cont_tac true i 
in 
    Hoare.add_hoare_tacs [("With_Fresh_Stack_Ptr_tac", tac)]
end

end

locale modifies_assertion_stack_heap_state =
  modifies_assertion P + stack_heap_state htd htd_upd hmem hmem_upd 𝒮
  for P::"'s  's set" and
    htd:: "'s  heap_typ_desc" and
    htd_upd:: "(heap_typ_desc  heap_typ_desc)  's  's" and
    hmem:: "'s  heap_mem" and
    hmem_upd:: "(heap_mem  heap_mem)  's  's"   and  
    𝒮::"addr set" +
  assumes hmem_upd_inv: "σ m. hmem_upd m σ  (P σ)"
  assumes htd_upd_inv: "σ d. htd_upd d σ  (P σ)"
begin

lemma modifies_With_Fresh_Stack_Ptr [modifies_inv_intros]:
  assumes no_overflow: "StackOverflow  F"
  assumes c: "σ p. Γ,Θ⊢⇘/F{σ} (c (p::'a::mem_type ptr)) (P σ),(P σ)"
  shows "Γ,Θ⊢⇘/F{σ} With_Fresh_Stack_Ptr n init c (P σ), (P σ)"
  apply (rule With_Fresh_Stack_Ptr_tight_wp [where R = "λ s p d v. P s"])
  subgoal for s p d vs bs
  proof -
    have "(htd_upd (λ_. d) s)  P s" by (rule htd_upd_inv)
    moreover have "hmem_upd (fold (λi. heap_update_padding (p +p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)  P (htd_upd (λ_. d) s)"
      by (rule hmem_upd_inv)
    ultimately
    show "hmem_upd (fold (λi. heap_update_padding (p +p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) (htd_upd (λ_. d) s)  P s"
      using modifies_inv_prop' p by blast
  qed
  subgoal for s p d v
    apply (rule HoarePartial.conseq [where P'=P and Q'=P and A'=P])
   apply (rule allI)
    subgoal for Z
      apply (rule modifies_inv_prop_lift)
      apply (rule c)
      done
    using modifies_inv_prop' hmem_upd_inv htd_upd_inv 
    by (smt (verit, best) mem_Collect_eq singletonD subset_eq)
  apply (rule no_overflow)
  done

end



locale modifies_assertion_stack_heap_raw_state =
  modifies_assertion P + stack_heap_raw_state t_hrs t_hrs_update 𝒮
  for P::"'s  's set" and
    t_hrs:: "'s  heap_raw_state" and
    t_hrs_update:: "(heap_raw_state  heap_raw_state)  's  's" and
    𝒮::"addr set" +
  assumes hrs_upd_inv: "σ m. t_hrs_update m σ  (P σ)"
begin

sublocale modifies_assertion_stack_heap_state 
  P
  "λs. hrs_htd (t_hrs s)" "λupd. t_hrs_update (hrs_htd_update upd)" 
  "λs. hrs_mem (t_hrs s)" "λupd. t_hrs_update (hrs_mem_update upd)" 
  "𝒮"
  using hrs_upd_inv by unfold_locales auto

end

end