Theory AutomaticVerifiers

section ‹Fractional Predicates and Magic Wands in Automatic Separation Logic Verifiers›

text ‹This section corresponds to Section 5 of the paper~\<^cite>‹"UnboundedSL"›.›

theory AutomaticVerifiers
  imports FixedPoint WandProperties
begin

context logic
begin

subsection ‹Syntactic multiplication›

text ‹The following definition corresponds to Figure 6 of the paper~\<^cite>‹"UnboundedSL"›.›

fun syn_mult :: "'b ⇒ ('a, 'b, 'c, 'd) assertion ⇒ ('a, 'b, 'c, 'd) assertion" where
  "syn_mult π (Star A B) = Star (syn_mult π A) (syn_mult π B)"
| "syn_mult π (Wand A B) = Wand (syn_mult π A) (syn_mult π B)"
| "syn_mult π (Or A B) = Or (syn_mult π A) (syn_mult π B)"
| "syn_mult π (And A B) = And (syn_mult π A) (syn_mult π B)"
| "syn_mult π (Imp A B) = Imp (syn_mult π A) (syn_mult π B)"
| "syn_mult π (Mult α A) = syn_mult (smult α π) A"
| "syn_mult π (Exists x A) = Exists x (syn_mult π A)"
| "syn_mult π (Forall x A) = Forall x (syn_mult π A)"
| "syn_mult π (Wildcard A) = Wildcard A"
| "syn_mult π A = Mult π A"

definition div_state where
  "div_state π σ = (SOME r. σ = π ⊙ r)"

lemma div_state_ok:
  "σ = π ⊙ (div_state π σ)"
  by (metis (mono_tags) div_state_def someI_ex unique_inv)

text ‹The following theorem corresponds to Theorem 6 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem syn_sen_mult_same:
  "σ, s, Δ ⊨ syn_mult π A ⟷ σ, s, Δ ⊨ Mult π A"
proof (induct A arbitrary: σ π s)
  case (Exists x A)
  show ?case (is "?A ⟷ ?B")
  proof
    show "?B ⟹ ?A"
      using Exists.hyps by auto
    show "?A ⟹ ?B"
      using Exists.hyps by fastforce
  qed
next
  case (Forall x A)
  then show ?case
    by (metis dot_forall1 dot_forall2 entails_def sat.simps(9) syn_mult.simps(8))
next
  case (Star A B)
  show ?case (is "?P ⟷ ?Q")
  proof
    show "?P ⟹ ?Q"
    proof -
      assume ?P
      then obtain a b where "a, s, Δ ⊨ syn_mult π A" "b, s, Δ ⊨ syn_mult π B"
      "Some σ = a ⊕ b" by auto
      then obtain "a, s, Δ ⊨ Mult π A" "b, s, Δ ⊨ Mult π B"
        using Star.hyps(1) Star.hyps(2) Star.prems by blast
      then show ?Q
        by (meson ‹Some σ = a ⊕ b› dot_star2 entails_def sat.simps(2))
    qed
    assume ?Q
    then obtain a b where "a, s, Δ ⊨ Mult π A" "b, s, Δ ⊨ Mult π B" "Some σ = a ⊕ b"
      by (meson dot_star1 entails_def sat.simps(2))
    then show ?P
      using Star.hyps(1) Star.hyps(2) Star.prems by force
  qed
next
  case (Mult p A)
  show ?case (is "?P ⟷ ?Q")
  proof
    show "?P ⟹ ?Q"
    proof -
      assume ?P
      then have "σ, s, Δ ⊨ syn_mult (smult p π) A" by auto
      then have "σ, s, Δ ⊨ Mult (smult p π) A"
        using Mult.hyps by blast
      then show ?Q
        by (metis dot_mult2 logic.entails_def logic_axioms smult_comm)
    qed
    assume ?Q
    then obtain a where "a, s, Δ ⊨ A" "σ = π ⊙ (p ⊙ a)" by auto
    then show ?P
      using Mult.hyps double_mult smult_comm by auto
  qed
next
  case (Wand A B)
  show ?case (is "?P ⟷ ?Q")
  proof
    show "?P ⟹ ?Q"
    proof -
      assume "σ, s, Δ ⊨ syn_mult π (Wand A B)"
      then have "σ, s, Δ ⊨ Wand (syn_mult π A) (syn_mult π B)"
        by auto
      moreover have "div_state π σ, s, Δ ⊨ Wand A B"
      proof (rule sat_wand)
        fix a b
        assume "a, s, Δ ⊨ A ∧ Some b = div_state π σ ⊕ a"
        then have "Some (π ⊙ b) = σ ⊕ (π ⊙ a)"
          using div_state_ok plus_mult by presburger
        moreover have "π ⊙ a, s, Δ ⊨ Mult π A"
          using ‹a, s, Δ ⊨ A ∧ Some b = div_state π σ ⊕ a› by auto
        then have "π ⊙ a, s, Δ ⊨ syn_mult π A"
          using Wand.hyps(1) Wand.prems by blast
        then have "π ⊙ b, s, Δ ⊨ syn_mult π B"
          using ‹σ, s, Δ ⊨ Wand (syn_mult π A) (syn_mult π B)› calculation by auto
        ultimately show "b, s, Δ ⊨ B"
          by (metis Wand.hyps(2) Wand.prems can_divide sat.simps(1))
      qed
      then show "σ, s, Δ ⊨ Mult π (Wand A B)"
        by (metis div_state_ok sat.simps(1))
    qed
    assume "σ, s, Δ ⊨ Mult π (Wand A B)"
    then have "div_state π σ, s, Δ ⊨ Wand A B"
      by (metis div_state_ok can_divide sat.simps(1))
    have "σ, s, Δ ⊨ Wand (syn_mult π A) (syn_mult π B)"
    proof (rule sat_wand)
      fix a b assume "a, s, Δ ⊨ syn_mult π A ∧ Some b = σ ⊕ a"
      then have "Some (div_state π b) = div_state π σ ⊕ div_state π a"
        by (metis div_state_ok plus_mult unique_inv)
      then have "div_state π b, s, Δ ⊨ B"
        by (metis (no_types, lifting) Wand.hyps(1) ‹a, s, Δ ⊨ syn_mult π A ∧ Some b = σ ⊕ a› ‹div_state π σ, s, Δ ⊨ Wand A B› div_state_ok logic.can_divide logic_axioms sat.simps(1) sat.simps(3))
      then show "b, s, Δ ⊨ syn_mult π B"
        using Wand.hyps(2) div_state_ok sat.simps(1) by blast
    qed
    then show "σ, s, Δ ⊨ syn_mult π (Wand A B)"
      by simp
  qed
next
  case (And A B)
  show ?case (is "?P ⟷ ?Q")
  proof
    show "?P ⟹ ?Q"
    proof -
      assume ?P
      then obtain "σ, s, Δ ⊨ syn_mult π A" "σ, s, Δ ⊨ syn_mult π B"
        by auto
      then show ?Q
        by (meson And.hyps(1) And.hyps(2) dot_and2 logic.entails_def logic_axioms sat.simps(7))
    qed
    assume ?Q then show ?P
      using And.hyps(1) And.hyps(2) And.prems by auto
  qed
next
  case (Imp A B)
  show ?case (is "?P ⟷ ?Q")
  proof
    show "?P ⟹ ?Q"
      by (metis Imp.hyps(1) Imp.hyps(2) sat.simps(1) sat.simps(5) syn_mult.simps(5) unique_inv)
    assume ?Q then show ?P
      by (metis Imp.hyps(1) Imp.hyps(2) Imp.prems can_divide sat.simps(1) sat.simps(5) syn_mult.simps(5))
  qed
next
  case (Wildcard A)
  then show ?case
    by (metis DotWild entails_def equivalent_def syn_mult.simps(9))
qed (auto)



subsection ‹Monotonicity and fixed point›

(* Bool means positive *)
fun pos_neg_rec_call :: "bool ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" where
  "pos_neg_rec_call b Pred ⟷ b"
| "pos_neg_rec_call b (Mult _ A) ⟷ pos_neg_rec_call b A"
| "pos_neg_rec_call b (Exists _ A) ⟷ pos_neg_rec_call b A"
| "pos_neg_rec_call b (Forall _ A) ⟷ pos_neg_rec_call b A"
| "pos_neg_rec_call b (Star A B) ⟷ pos_neg_rec_call b A ∧ pos_neg_rec_call b B"
| "pos_neg_rec_call b (Or A B) ⟷ pos_neg_rec_call b A ∧ pos_neg_rec_call b B"
| "pos_neg_rec_call b (And A B) ⟷ pos_neg_rec_call b A ∧ pos_neg_rec_call b B"
| "pos_neg_rec_call b (Wand A B) ⟷ pos_neg_rec_call (¬ b) A ∧ pos_neg_rec_call b B"
| "pos_neg_rec_call b (Imp A B) ⟷ pos_neg_rec_call (¬ b) A ∧ pos_neg_rec_call b B"
| "pos_neg_rec_call _ (Sem _) ⟷ True"
| "pos_neg_rec_call b (Bounded A) ⟷ pos_neg_rec_call b A"
| "pos_neg_rec_call b (Wildcard A) ⟷ pos_neg_rec_call b A"


lemma pos_neg_rec_call_mono:
  assumes "pos_neg_rec_call b A"
  shows "(b ⟶ monotonic (applies_eq A)) ∧ (¬ b ⟶ non_increasing (applies_eq A))"
  using assms
proof (induct A arbitrary: b)
  case (Exists x A)
  then show ?case
    by (meson mono_exists non_increasing_exists pos_neg_rec_call.simps(3))
next
  case (Forall x A)
  then show ?case
    by (meson mono_forall non_increasing_forall pos_neg_rec_call.simps(4))
next
  case (Sem x)
  then show ?case
    by (metis applies_eq.simps mem_Collect_eq mono_sem non_increasingI sat.simps(4) smaller_interp_def subsetI)
next
  case (Mult x1a A)
  then show ?case
    using mono_mult non_increasing_mult pos_neg_rec_call.simps(2) by blast
next
  case (Star A1 A2)
  then show ?case
    by (metis mono_star non_inc_star pos_neg_rec_call.simps(5))
next
  case (Wand A1 A2)
  then show ?case
    by (metis mono_wand non_increasing_wand pos_neg_rec_call.simps(8))
next
  case (Or A1 A2)
  then show ?case
    by (metis mono_or non_increasing_or pos_neg_rec_call.simps(6))
next
  case (And A1 A2)
  then show ?case
    by (metis mono_and non_increasing_and pos_neg_rec_call.simps(7))
next
  case (Imp A1 A2)
  then show ?case
    by (metis mono_imp non_increasing_imp pos_neg_rec_call.simps(9))
next
  case Pred
  then show ?case
    using mono_interp pos_neg_rec_call.simps(1) by blast
next
  case (Bounded A)
  then show ?case
    using mono_bounded non_increasing_bounded pos_neg_rec_call.simps(11) by blast
next
  case (Wildcard A)
  then show ?case
    using mono_wild non_increasing_wild pos_neg_rec_call.simps(12) by blast
qed


text ‹The following theorem corresponds to Theorem 7 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem exists_lfp_gfp:
  assumes "pos_neg_rec_call True A"
  shows "σ, s, LFP (applies_eq A) ⊨ A ⟷ σ ∈ LFP (applies_eq A) s"
    and "σ, s, GFP (applies_eq A) ⊨ A ⟷ σ ∈ GFP (applies_eq A) s"
   apply (metis LFP_is_FP applies_eq.simps assms mem_Collect_eq pos_neg_rec_call_mono)
  by (metis GFP_is_FP applies_eq.simps assms mem_Collect_eq pos_neg_rec_call_mono)





subsection ‹Combinability›

definition combinable_sem :: "(('d ⇒ 'c) ⇒ 'a ⇒ bool) ⇒ bool" where
  "combinable_sem B ⟷ (∀a b x s α β. B s a ∧ B s b ∧ sadd α β = one ∧ Some x = α ⊙ a ⊕ β ⊙ b  ⟶ B s x)"

fun wf_assertion :: "('a, 'b, 'c, 'd) assertion ⇒ bool" where
  "wf_assertion Pred ⟷ True"
| "wf_assertion (Sem B) ⟷ combinable_sem B"
| "wf_assertion (Mult _ A) ⟷ wf_assertion A"
| "wf_assertion (Forall _ A) ⟷ wf_assertion A"
| "wf_assertion (Exists x A) ⟷ wf_assertion A ∧ (∀Δ. unambiguous Δ A x)"
| "wf_assertion (Star A B) ⟷ wf_assertion A ∧ wf_assertion B"
| "wf_assertion (And A B) ⟷ wf_assertion A ∧ wf_assertion B"
| "wf_assertion (Wand A B) ⟷ wf_assertion B"
| "wf_assertion (Imp A B) ⟷ pure A ∧ wf_assertion B"
| "wf_assertion (Wildcard A) ⟷ wf_assertion A"
| "wf_assertion _ ⟷ False"



lemma wf_implies_combinable:
  assumes "wf_assertion A"
      and "sem_combinable Δ"
  shows "combinable Δ A"
  using assms
proof (induct A)
  case (Exists x A)
  then show ?case
    by (meson combinable_exists wf_assertion.simps(5))
next
  case (Forall x A)
  then show ?case
    by (meson combinable_forall wf_assertion.simps(4))
next
  case (Sem B)
  show ?case
  proof (rule combinableI)
    fix a b p q x σ s
    assume "a, s, Δ ⊨ Sem B ∧ b, s, Δ ⊨ Sem B ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
    then show "x, s, Δ ⊨ Sem B"
      by (metis Sem.prems(1) combinable_sem_def sat.simps(4) wf_assertion.simps(2))
  qed
next
  case (Mult x1a A)
  then show ?case
    using combinable_mult wf_assertion.simps(3) by blast
next
  case (Star A1 A2)
  then show ?case
    using combinable_star wf_assertion.simps(6) by blast
next
  case (Wand A1 A2)
  then show ?case
    using combinable_wand wf_assertion.simps(8) by blast
next
  case (And A1 A2)
  then show ?case
    using combinable_and by auto
next
  case (Imp A1 A2)
  then show ?case
    using combinable_imp by auto
next
  case Pred
  show ?case
  proof (rule combinableI)
    fix a b p q x σ s
    assume "a, s, Δ ⊨ Pred ∧ b, s, Δ ⊨ Pred ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
    then show "x, s, Δ ⊨ Pred"
      using assms(2) sat.simps(10) sem_combinableE by metis
  qed
next
  case (Wildcard A)
  then show ?case
    using combinable_wildcard wf_assertion.simps(10) by blast
qed (auto)





subsection ‹Theorems›

text ‹The following two theorems correspond to the rules shown in Section 5.1 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem apply_wand:
  "Star (syn_mult π A) (Mult π (Wand A B)), Δ ⊢ syn_mult π B"
proof (rule entailsI)
  fix σ s
  assume asm: "σ, s, Δ ⊨ Star (syn_mult π A) (Mult π (Wand A B))"
  then obtain x y where "Some σ = x ⊕ y" "x, s, Δ ⊨ syn_mult π A" "y, s, Δ ⊨ Mult π (Wand A B)"
    by auto
  then have "y, s, Δ ⊨ Wand (syn_mult π A) (syn_mult π B)"
    by (metis syn_mult.simps(2) syn_sen_mult_same)
  then show "σ, s, Δ ⊨ syn_mult π B"
    using ‹Some σ = x ⊕ y› ‹x, s, Δ ⊨ syn_mult π A› ‹y, s, Δ ⊨ Wand (syn_mult π A) (syn_mult π B)› commutative by auto
qed

theorem package_wand:
  assumes "Star F (syn_mult π A), Δ ⊢ syn_mult π B"
  shows "F, Δ ⊢ Mult π (Wand A B)"
  by (metis adjunct2 assms entails_def syn_mult.simps(2) syn_sen_mult_same)

text ‹The following four theorems correspond to the rules shown in Section 5.2 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem fold_lfp:
  assumes "pos_neg_rec_call True A"
    shows "syn_mult π A, LFP (applies_eq A) ⊢ Mult π Pred"
  by (simp add: assms entails_def exists_lfp_gfp(1) syn_sen_mult_same)

theorem unfold_lfp:
  assumes "pos_neg_rec_call True A"
    shows "Mult π Pred, LFP (applies_eq A) ⊢ syn_mult π A"
  by (simp add: assms entails_def exists_lfp_gfp(1) syn_sen_mult_same)

theorem fold_gfp:
  assumes "pos_neg_rec_call True A"
    shows "syn_mult π A, GFP (applies_eq A) ⊢ Mult π Pred"
  by (simp add: assms entails_def exists_lfp_gfp(2) syn_sen_mult_same)

theorem unfold_gfp:
  assumes "pos_neg_rec_call True A"
    shows "Mult π Pred, GFP (applies_eq A) ⊢ syn_mult π A"
  by (simp add: assms entails_def exists_lfp_gfp(2) syn_sen_mult_same)

text ‹The following theorems correspond to the rule shown in Section 5.3 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem wf_assertion_combinable_lfp:
  assumes "wf_assertion A"
      and "pos_neg_rec_call True A"
    shows "sem_combinable (LFP (applies_eq A))"
proof -
  let ?f = "λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b}"
  have "set_closure_property ?f (LFP (applies_eq A))"
  proof (rule FP_preserves_set_closure_property(2))
    show "monotonic (applies_eq A)"
      using assms(2) pos_neg_rec_call_mono by blast
    fix Δ :: "('d, 'c, 'a) interp" assume asm0: "set_closure_property ?f Δ"
    then have "sem_combinable Δ"
      by (metis combinable_set_closure)
    then show "set_closure_property ?f (applies_eq A Δ)"
      by (metis assms(1) combinable_set_closure sem_combinable_equiv wf_implies_combinable)
  qed
  then show ?thesis using combinable_set_closure by metis
qed


theorem wf_assertion_combinable_gfp:
  assumes "wf_assertion A"
      and "pos_neg_rec_call True A"
    shows "sem_combinable (GFP (applies_eq A))"
proof -
  let ?f = "λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b}"
  have "set_closure_property ?f (GFP (applies_eq A))"
  proof (rule FP_preserves_set_closure_property(1))
    show "monotonic (applies_eq A)"
      using assms(2) pos_neg_rec_call_mono by blast
    fix Δ :: "('d, 'c, 'a) interp" assume asm0: "set_closure_property ?f Δ"
    then have "sem_combinable Δ"
      by (metis combinable_set_closure)
    then show "set_closure_property ?f (applies_eq A Δ)"
      by (metis assms(1) combinable_set_closure sem_combinable_equiv wf_implies_combinable)
  qed
  then show ?thesis using combinable_set_closure by metis
qed

theorem wf_combine:
  assumes "wf_assertion A"
      and "pos_neg_rec_call True A"
    shows "Star (Mult α Pred) (Mult β Pred), LFP (applies_eq A) ⊢ Mult (sadd α β) Pred"
    and "Star (Mult α Pred) (Mult β Pred), GFP (applies_eq A) ⊢ Mult (sadd α β) Pred"
  apply (metis assms(1) assms(2) logic.combinable_def logic.wf_implies_combinable logic_axioms wf_assertion.simps(1) wf_assertion_combinable_lfp)
  by (metis assms(1) assms(2) logic.combinable_def logic.wf_implies_combinable logic_axioms wf_assertion.simps(1) wf_assertion_combinable_gfp)

end

end