Theory UnboundedLogic

section ‹Unbounded Separation Logic›

theory UnboundedLogic
  imports Main
begin

subsection ‹Assertions and state model›

text ‹We define our assertion language as described in Section 2.3 of the paper~cite‹"UnboundedSL"›.›

datatype ('a, 'b, 'c, 'd) assertion =
  Sem "('d ⇒ 'c) ⇒ 'a ⇒ bool"
  | Mult 'b "('a, 'b, 'c, 'd) assertion"
  | Star "('a, 'b, 'c, 'd) assertion" "('a, 'b, 'c, 'd) assertion"
  | Wand "('a, 'b, 'c, 'd) assertion" "('a, 'b, 'c, 'd) assertion"
  | Or "('a, 'b, 'c, 'd) assertion" "('a, 'b, 'c, 'd) assertion"
  | And "('a, 'b, 'c, 'd) assertion" "('a, 'b, 'c, 'd) assertion"
  | Imp "('a, 'b, 'c, 'd) assertion" "('a, 'b, 'c, 'd) assertion"
  | Exists 'd "('a, 'b, 'c, 'd) assertion"
  | Forall 'd "('a, 'b, 'c, 'd) assertion"
  | Pred
  | Bounded "('a, 'b, 'c, 'd) assertion"
  | Wildcard "('a, 'b, 'c, 'd) assertion"

type_synonym 'a command = "('a × 'a option) set"

locale pre_logic =
    fixes plus :: "'a ⇒ 'a ⇒ 'a option" (infixl ‹⊕› 63)

begin

definition compatible :: "'a ⇒ 'a ⇒ bool" (infixl ‹##› 60) where
  "a ## b ⟷ a ⊕ b ≠ None"

definition larger :: "'a ⇒ 'a ⇒ bool" (infixl ‹≽› 55) where
  "a ≽ b ⟷ (∃c. Some a = b ⊕ c)"

end

type_synonym ('a, 'b, 'c) interp = "('a ⇒ 'b) ⇒ 'c set"

text ‹The following locale captures the state model described in Section 2.2 of the paper~cite‹"UnboundedSL"›.›

locale logic = pre_logic +

  fixes mult :: "'b ⇒ 'a ⇒ 'a" (infixl ‹⊙› 64)

  fixes smult :: "'b ⇒ 'b ⇒ 'b"
  fixes sadd :: "'b ⇒ 'b ⇒ 'b"
  fixes sinv :: "'b ⇒ 'b"

  fixes one :: 'b

  fixes valid :: "'a ⇒ bool"


  assumes commutative: "a ⊕ b = b ⊕ a"
      and asso1: "a ⊕ b = Some ab ∧ b ⊕ c = Some bc ⟹ ab ⊕ c = a ⊕ bc"
      and asso2: "a ⊕ b = Some ab ∧ ¬ b ## c ⟹ ¬ ab ## c"

      and sinv_inverse: "smult p (sinv p) = one"
      and sone_neutral: "smult one p = p"
      and sadd_comm: "sadd p q = sadd q p"
      and smult_comm: "smult p q = smult q p"
      and smult_distrib: "smult p (sadd q r) = sadd (smult p q) (smult p r)"
      and smult_asso: "smult (smult p q) r = smult p (smult q r)"

      and double_mult: "p ⊙ (q ⊙ a) = (smult p q) ⊙ a"
      and plus_mult: "Some a = b ⊕ c ⟹ Some (p ⊙ a) = (p ⊙ b) ⊕ (p ⊙ c)"
      and distrib_mult: "Some ((sadd p q) ⊙ x) = p ⊙ x ⊕ q ⊙ x"
      and one_neutral: "one ⊙ a = a"

      and valid_mono: "valid a ∧ a ≽ b ⟹ valid b"

begin

text ‹The validity of assertions corresponds to Figure 3 of the paper~cite‹"UnboundedSL"›.›

fun sat :: "'a ⇒ ('d ⇒ 'c) ⇒ ('d, 'c, 'a) interp ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" (‹_, _, _ ⊨ _› [51, 65, 68, 66] 50) where
  "σ, s, Δ ⊨ Mult p A ⟷ (∃a. σ = p ⊙ a ∧ a, s, Δ ⊨ A)"
| "σ, s, Δ ⊨ Star A B ⟷ (∃a b. Some σ = a ⊕ b ∧ a, s, Δ ⊨ A ∧ b, s, Δ ⊨ B)"
| "σ, s, Δ ⊨ Wand A B ⟷ (∀a σ'. a, s, Δ ⊨ A ∧ Some σ' = σ ⊕ a ⟶ σ', s, Δ ⊨ B)"

| "σ, s, Δ ⊨ Sem b ⟷ b s σ"
| "σ, s, Δ ⊨ Imp A B ⟷ (σ, s, Δ ⊨ A ⟶ σ, s, Δ ⊨ B)"
| "σ, s, Δ ⊨ Or A B ⟷ (σ, s, Δ ⊨ A ∨ σ, s, Δ ⊨ B)"
| "σ, s, Δ ⊨ And A B ⟷ (σ, s, Δ ⊨ A ∧ σ, s, Δ ⊨ B)"

| "σ, s, Δ ⊨ Exists x A ⟷ (∃v. σ, s(x := v), Δ ⊨ A)"
| "σ, s, Δ ⊨ Forall x A ⟷ (∀v. σ, s(x := v), Δ ⊨ A)"

| "σ, s, Δ ⊨ Pred ⟷ (σ ∈ Δ s)"
| "σ, s, Δ ⊨ Bounded A ⟷ (valid σ ⟶ σ, s, Δ ⊨ A)"
| "σ, s, Δ ⊨ Wildcard A ⟷ (∃a p. σ = p ⊙ a ∧ a, s, Δ ⊨ A)"

definition intuitionistic :: "('d ⇒ 'c) ⇒ ('d, 'c, 'a) interp ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" where
  "intuitionistic s Δ A ⟷ (∀a b. a ≽ b ∧ b, s, Δ ⊨ A ⟶ a, s, Δ ⊨ A)"

definition entails :: "('a, 'b, 'c, 'd) assertion ⇒ ('d, 'c, 'a) interp ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" (‹_, _ ⊢ _› [63, 66, 68] 52) where
  "A, Δ ⊢ B ⟷ (∀σ s. σ, s, Δ ⊨ A ⟶ σ, s, Δ ⊨ B)"

definition equivalent :: "('a, 'b, 'c, 'd) assertion ⇒ ('d, 'c, 'a) interp ⇒ ('a, 'b, 'c, 'd) assertion ⇒ bool" (‹_, _ ≡ _› [63, 66, 68] 52) where
  "A, Δ ≡ B ⟷ (A, Δ ⊢ B ∧ B, Δ ⊢ A)"

definition pure :: "('a, 'b, 'c, 'd) assertion ⇒ bool" where
  "pure A ⟷ (∀σ σ' s Δ Δ'. σ, s, Δ ⊨ A ⟷ σ', s, Δ' ⊨ A)"


subsection ‹Useful lemmas›

lemma sat_forall:
  assumes "⋀v. σ, s(x := v), Δ ⊨ A"
  shows "σ, s, Δ ⊨ Forall x A"
  by (simp add: assms)

lemma intuitionisticI:
  assumes "⋀a b. a ≽ b ∧ b, s, Δ ⊨ A ⟹ a, s, Δ ⊨ A"
  shows "intuitionistic s Δ A"
  by (meson assms intuitionistic_def)

lemma can_divide:
  assumes "p ⊙ a = p ⊙ b"
  shows "a = b"
  by (metis assms double_mult logic.one_neutral logic_axioms sinv_inverse smult_comm)

lemma unique_inv:
  "a = p ⊙ b ⟷ b = (sinv p) ⊙ a"
  by (metis double_mult logic.can_divide logic_axioms sinv_inverse sone_neutral)

lemma entailsI:
  assumes "⋀σ s. σ, s, Δ ⊨ A ⟹ σ, s, Δ ⊨ B"
  shows "A, Δ ⊢ B"
  by (simp add: assms entails_def)

lemma equivalentI:
  assumes "⋀σ s. σ, s, Δ ⊨ A ⟹ σ, s, Δ ⊨ B"
      and "⋀σ s. σ, s, Δ ⊨ B ⟹ σ, s, Δ ⊨ A"
    shows "A, Δ ≡ B"
  by (simp add: assms(1) assms(2) entailsI equivalent_def)

lemma compatible_imp:
  assumes "a ## b"
  shows "(p ⊙ a) ## (p ⊙ b)"
  by (metis assms compatible_def option.distinct(1) option.exhaust plus_mult)

lemma compatible_iff:
  "a ## b ⟷ (p ⊙ a) ## (p ⊙ b)"
  by (metis compatible_imp unique_inv)

lemma sat_wand:
  assumes "⋀a σ'. a, s, Δ ⊨ A ∧ Some σ' = σ ⊕ a ⟹ σ', s, Δ ⊨ B"
  shows "σ, s, Δ ⊨ Wand A B"
  using assms by auto

lemma sat_imp:
  assumes "σ, s, Δ ⊨ A ⟹ σ, s, Δ ⊨ B"
  shows "σ, s, Δ ⊨ Imp A B"
  using assms by auto

lemma sat_mult:
  assumes "⋀a. σ = p ⊙ a ⟹ a, s, Δ ⊨ A"
  shows "σ, s, Δ ⊨ Mult p A"
  by (metis assms logic.sat.simps(1) logic_axioms unique_inv)

lemma larger_same:
  "a ≽ b ⟷ p ⊙ a ≽ p ⊙ b"
proof -
  have "⋀a b p. a ≽ b ⟹ p ⊙ a ≽ p ⊙ b"
    by (meson larger_def plus_mult)
  then show ?thesis
    by (metis unique_inv)
qed

lemma asso3:
  assumes "¬ a ## b"
      and "b ⊕ c = Some bc"
    shows "¬ a ## bc"
  by (metis (full_types) assms(1) assms(2) asso2 commutative compatible_def)

lemma compatible_smaller:
  assumes "a ≽ b"
      and "x ## a"
    shows "x ## b"
  by (metis assms(1) assms(2) asso3 larger_def)

lemma compatible_multiples:
  assumes "p ⊙ a ## q ⊙ b"
  shows "a ## b"
  by (metis (no_types, opaque_lifting) assms commutative compatible_def compatible_iff compatible_smaller distrib_mult larger_def one_neutral)

lemma move_sum:
  assumes "Some a = a1 ⊕ a2"
      and "Some b = b1 ⊕ b2"
      and "Some x = a ⊕ b"
      and "Some x1 = a1 ⊕ b1"
      and "Some x2 = a2 ⊕ b2"
    shows "Some x = x1 ⊕ x2"
proof -
  obtain ab1 where "Some ab1 = a ⊕ b1"
    by (metis assms(2) assms(3) asso3 compatible_def not_Some_eq)
  then have "Some ab1 = x1 ⊕ a2"
    by (metis assms(1) assms(4) asso1 commutative)
  then show ?thesis
    by (metis ‹Some ab1 = a ⊕ b1› assms(2) assms(3) assms(5) asso1)
qed

lemma sum_both_larger:
  assumes "Some x' = a' ⊕ b'"
      and "Some x = a ⊕ b"
      and "a' ≽ a"
      and "b' ≽ b"
    shows "x' ≽ x"
proof -
  obtain ra rb where "Some a' = a ⊕ ra" "Some b' = b ⊕ rb"
    using assms(3) assms(4) larger_def by auto
  then obtain r where "Some r = ra ⊕ rb"
    by (metis assms(1) asso3 commutative compatible_def option.collapse)
  then have "Some x' = x ⊕ r"
    by (meson ‹Some a' = a ⊕ ra› ‹Some b' = b ⊕ rb› assms(1) assms(2) move_sum)
  then show ?thesis
    using larger_def by blast
qed

lemma larger_first_sum:
  assumes "Some y = a ⊕ b"
      and "x ≽ y"
    shows "∃a'. Some x = a' ⊕ b ∧ a' ≽ a"
proof -
  obtain r where "Some x = y ⊕ r"
    using assms(2) larger_def by auto
  then obtain a' where "Some a' = a ⊕ r"
    by (metis assms(1) asso2 commutative compatible_def option.collapse)
  then show ?thesis
    by (metis ‹Some x = y ⊕ r› assms(1) asso1 commutative larger_def)
qed

lemma larger_implies_compatible:
  assumes "x ≽ y"
  shows "x ## y"
  by (metis assms compatible_def compatible_smaller distrib_mult one_neutral option.distinct(1))







section ‹Frame rule›

text ‹This section corresponds to Section 2.5 of the paper~cite‹"UnboundedSL"›.›

definition safe :: "('a × ('d ⇒ 'c)) command ⇒ ('a × ('d ⇒ 'c)) ⇒ bool" where
  "safe c σ ⟷ (σ, None) ∉ c"

definition safety_monotonicity :: "('a × ('d ⇒ 'c)) command ⇒ bool" where
  "safety_monotonicity c ⟷ (∀σ σ' s. valid σ' ∧ σ' ≽ σ ∧ safe c (σ, s) ⟶ safe c (σ', s))"

definition frame_property :: "('a × ('d ⇒ 'c)) command ⇒ bool" where
  "frame_property c ⟷ (∀σ σ0 r σ' s s'. valid σ ∧ valid σ' ∧ safe c (σ0, s) ∧ Some σ = σ0 ⊕ r ∧ ((σ, s), Some (σ', s')) ∈ c
  ⟶ (∃σ0'. Some σ' = σ0' ⊕ r ∧ ((σ0, s), Some (σ0', s')) ∈ c))"

definition valid_hoare_triple :: "('a, 'b, 'c, 'd) assertion ⇒ ('a × ('d ⇒ 'c)) command ⇒ ('a, 'b, 'c, 'd) assertion ⇒ ('d, 'c, 'a) interp ⇒ bool" where
  "valid_hoare_triple P c Q Δ ⟷ (∀σ s. valid σ ∧ σ, s, Δ ⊨ P ⟶ safe c (σ, s) ∧ (∀σ' s'. ((σ, s), Some (σ', s')) ∈ c ⟶ σ', s', Δ ⊨ Q))"

lemma valid_hoare_tripleI:
  assumes "⋀σ s. valid σ ∧ σ, s, Δ ⊨ P ⟹ safe c (σ, s)"
      and "⋀σ s σ' s'. valid σ ∧ σ, s, Δ ⊨ P ⟹ ((σ, s), Some (σ', s')) ∈ c ⟹ σ', s', Δ ⊨ Q"
    shows "valid_hoare_triple P c Q Δ"
  using assms(1) assms(2) valid_hoare_triple_def by blast

definition valid_command :: "('a × ('d ⇒ 'c)) command ⇒ bool" where
  "valid_command c ⟷ (∀a b sa sb. ((a, sa), Some (b, sb)) ∈ c ∧ valid a ⟶ valid b)"

definition modified :: "('a × ('d ⇒ 'c)) command ⇒ 'd set" where
  "modified c = { x |x. ∃σ s σ' s'. ((σ, s), Some (σ', s')) ∈ c ∧ s x ≠ s' x }"

definition equal_outside :: "('d ⇒ 'c) ⇒ ('d ⇒ 'c) ⇒ 'd set ⇒ bool" where
  "equal_outside s s' S ⟷ (∀x. x ∉ S ⟶ s x = s' x)"



definition not_in_fv :: "('a, 'b, 'c, 'd) assertion ⇒ 'd set ⇒ bool" where
  "not_in_fv A S ⟷ (∀σ s Δ s'. equal_outside s s' S ⟶ (σ, s, Δ ⊨ A ⟷ σ, s', Δ ⊨ A))"



lemma not_in_fv_mod:
  assumes "not_in_fv A (modified c)"
  and "((σ, s), Some (σ', s')) ∈ c"
  shows "x, s, Δ ⊨ A ⟷ x, s', Δ ⊨ A"
proof -
  have "⋀x. x ∉ (modified c) ⟹ s x = s' x"
  proof -
    fix x assume "x ∉ (modified c)"
    then show "s x = s' x"
      by (metis (mono_tags, lifting) CollectI assms(2) modified_def)
  qed
  then have "equal_outside s s' (modified c)"
    by (simp add: equal_outside_def)
  then show ?thesis
    using assms(1) not_in_fv_def by blast
qed


text ‹This theorem corresponds to Theorem 2 of the paper~cite‹"UnboundedSL"›.›

theorem frame_rule:
  assumes "valid_command c"
      and "safety_monotonicity c"
      and "frame_property c"
      and "valid_hoare_triple P c Q Δ"
      and "not_in_fv R (modified c)"
    shows "valid_hoare_triple (Star P R) c (Star Q R) Δ"
proof (rule valid_hoare_tripleI)
  fix σ s assume asm0: "valid σ ∧ σ, s, Δ ⊨ Star P R"
  then obtain p r where "Some σ = p ⊕ r" "p, s, Δ ⊨ P" "r, s, Δ ⊨ R"
    by auto
  then have "safe c (p, s)"
    by (metis asm0 assms(4) larger_def logic.valid_mono logic_axioms valid_hoare_triple_def)
  then show "safe c (σ, s)"
    using ‹Some σ = p ⊕ r› assms(2) larger_def safety_monotonicity_def asm0 by blast
  fix σ' s' assume asm1: "((σ, s), Some (σ', s')) ∈ c"
  then obtain q where "Some σ' = q ⊕ r" "((p, s), Some (q, s')) ∈ c"
    using ‹Some σ = p ⊕ r› ‹safe c (p, s)› asm0 assms(1) assms(3) frame_property_def valid_command_def by blast
  moreover have "r, s', Δ ⊨ R"
    by (meson ‹r, s, Δ ⊨ R› assms(5) calculation(2) logic.not_in_fv_mod logic_axioms)
  ultimately show "σ', s', Δ ⊨ Star Q R"
    by (meson ‹Some σ = p ⊕ r› ‹p, s, Δ ⊨ P› ‹r, s, Δ ⊨ R› asm0 assms(4) larger_def sat.simps(2) valid_hoare_triple_def valid_mono)
qed


lemma hoare_triple_input:
  "valid_hoare_triple P c Q Δ ⟷ valid_hoare_triple (Bounded P) c Q Δ"
  using sat.simps(11) valid_hoare_triple_def by blast


lemma hoare_triple_output:
  assumes "valid_command c"
  shows "valid_hoare_triple P c Q Δ ⟷ valid_hoare_triple P c (Bounded Q) Δ"
  using assms valid_command_def valid_hoare_triple_def by fastforce



end

end