Theory Compositional_Reasoning

(*<*)
theory Compositional_Reasoning
imports BD_Security_Unwinding
begin
(*>*)

section ‹Compositional Reasoning›

text ‹This section formalizes the compositional unwinding method discussed in
\<^cite>‹‹Section 5.2› in "cocon-CAV2014"››

context BD_Security_IO begin


subsection‹Preliminaries›

definition "disjAll Δs s vl s1 vl1 ≡ (∃Δ ∈ Δs. Δ s vl s1 vl1)"

lemma disjAll_simps[simp]:
  "disjAll {} ≡ λ_ _ _ _. False"
  "disjAll (insert Δ Δs) ≡ λs vl s1 vl1. Δ s vl s1 vl1 ∨ disjAll Δs s vl s1 vl1"
  unfolding disjAll_def[abs_def] by auto

lemma disjAll_mono:
assumes "disjAll Δs s vl s1 vl1"
and "Δs ⊆ Δs'"
shows "disjAll Δs' s vl s1 vl1"
using assms unfolding disjAll_def by auto

lemma iaction_mono:
assumes 1: "iaction Δ s vl s1 vl1" and 2: "⋀ s vl s1 vl1. Δ s vl s1 vl1 ⟹ Δ' s vl s1 vl1"
shows "iaction Δ' s vl s1 vl1"
using assms unfolding iaction_def by fastforce

lemma match_mono:
assumes 1: "match Δ s s1 vl1 a ou s' vl'" and 2: "⋀ s vl s1 vl1. Δ s vl s1 vl1 ⟹ Δ' s vl s1 vl1"
shows "match Δ' s s1 vl1 a ou s' vl'"
using assms unfolding match_def by fastforce

lemma ignore_mono:
assumes 1: "ignore Δ s s1 vl1 a ou s' vl'" and 2: "⋀ s vl s1 vl1. Δ s vl s1 vl1 ⟹ Δ' s vl s1 vl1"
shows "ignore Δ' s s1 vl1 a ou s' vl'"
using assms unfolding ignore_def by auto

lemma reaction_mono:
assumes 1: "reaction Δ s vl s1 vl1" and 2: "⋀ s vl s1 vl1. Δ s vl s1 vl1 ⟹ Δ' s vl s1 vl1"
shows "reaction Δ' s vl s1 vl1"
proof
  fix a ou s' vl'
  assume "step s a = (ou, s')" and "¬ T (Trans s a ou s')" and "consume (Trans s a ou s') vl vl'"
  hence "match Δ s s1 vl1 a ou s' vl' ∨ ignore Δ s s1 vl1 a ou s' vl'" (is "?m ∨ ?i")
  using 1 unfolding reaction_def by auto
  thus "match Δ' s s1 vl1 a ou s' vl' ∨ ignore Δ' s s1 vl1 a ou s' vl'" (is "?m' ∨ ?i'")
  proof
    assume ?m from match_mono[OF this 2] show ?thesis by simp
  next
    assume ?i from ignore_mono[OF this 2] show ?thesis by simp
  qed
qed


subsection‹Decomposition into an arbitrary network of components›

(* Unwind not to itself, but to a disjunction of other relations: *)
definition unwind_to where
"unwind_to Δ Δs ≡
 ∀ s vl s1 vl1.
   reachNT s ∧ reach s1 ∧ Δ s vl s1 vl1
   ⟶
   vl ≠ [] ∧ exit s (hd vl)
   ∨
   iaction (disjAll Δs) s vl s1 vl1
   ∨
   (vl ≠ [] ∨ vl1 = []) ∧ reaction (disjAll Δs) s vl s1 vl1"

lemma unwind_toI[intro?]:
assumes
"⋀ s vl s1 vl1.
   ⟦reachNT s; reach s1; Δ s vl s1 vl1⟧
   ⟹
   vl ≠ [] ∧ exit s (hd vl)
   ∨
   iaction (disjAll Δs) s vl s1 vl1
   ∨
   (vl ≠ [] ∨ vl1 = []) ∧ reaction (disjAll Δs) s vl s1 vl1"
shows "unwind_to Δ Δs"
using assms unfolding unwind_to_def by auto

(* Decomposition: *)
lemma unwind_dec:
assumes ne: "⋀ Δ. Δ ∈ Δs ⟹ next Δ ⊆ Δs ∧ unwind_to Δ (next Δ)"
shows "unwind (disjAll Δs)" (is "unwind ?Δ")
proof
  fix s s1 :: 'state and vl vl1 :: "'value list"
  assume r: "reachNT s" "reach s1" and Δ: "?Δ s vl s1 vl1"
  then obtain Δ where Δ: "Δ ∈ Δs" and 2: "Δ s vl s1 vl1" unfolding disjAll_def by auto
  let ?Δs' = "next Δ"  let ?Δ' = "disjAll ?Δs'"
  have "(vl ≠ [] ∧ exit s (hd vl)) ∨
        iaction ?Δ' s vl s1 vl1 ∨
        ((vl ≠ [] ∨ vl1 = []) ∧ reaction ?Δ' s vl s1 vl1)"
  using 2 Δ ne r unfolding unwind_to_def by auto
  moreover have "⋀ s vl s1 vl1. ?Δ' s vl s1 vl1 ⟹ ?Δ s vl s1 vl1"
  using ne[OF Δ] unfolding disjAll_def by auto
  ultimately show
       "(vl ≠ [] ∧ exit s (hd vl)) ∨
        iaction ?Δ s vl s1 vl1 ∨
        ((vl ≠ [] ∨ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)"
  using iaction_mono[of ?Δ' _ _ _ _ ?Δ] reaction_mono[of ?Δ' _ _ _ _ ?Δ] by blast
qed

lemma init_dec:
assumes Δ0: "Δ0 ∈ Δs"
and i: "⋀ vl vl1. B vl vl1 ⟹ Δ0 istate vl istate vl1"
shows "∀ vl vl1. B vl vl1 ⟶ disjAll Δs istate vl istate vl1"
using assms unfolding disjAll_def by auto

theorem unwind_dec_secure:
assumes Δ0: "Δ0 ∈ Δs"
and i: "⋀ vl vl1. B vl vl1 ⟹ Δ0 istate vl istate vl1"
and ne: "⋀ Δ. Δ ∈ Δs ⟹ next Δ ⊆ Δs ∧ unwind_to Δ (next Δ)"
shows secure
using init_dec[OF Δ0 i] unwind_dec[OF ne] unwind_secure by metis


subsection‹A customization for linear modular reasoning›

(* The customization assumes that each component unwinds only into itself,
its successor or an exit component.  *)

definition unwind_cont where
"unwind_cont Δ Δs ≡
 ∀ s vl s1 vl1.
   reachNT s ∧ reach s1 ∧ Δ s vl s1 vl1
   ⟶
   iaction (disjAll Δs) s vl s1 vl1
   ∨
   ((vl ≠ [] ∨ vl1 = []) ∧ reaction (disjAll Δs) s vl s1 vl1)"

lemma unwind_contI[intro?]:
assumes
"⋀ s vl s1 vl1.
   ⟦reachNT s; reach s1; Δ s vl s1 vl1⟧
   ⟹
   iaction (disjAll Δs) s vl s1 vl1
   ∨
   ((vl ≠ [] ∨ vl1 = []) ∧ reaction (disjAll Δs) s vl s1 vl1)"
shows "unwind_cont Δ Δs"
using assms unfolding unwind_cont_def by auto

definition unwind_exit where
"unwind_exit Δe ≡
 ∀ s vl s1 vl1.
   reachNT s ∧ reach s1 ∧ Δe s vl s1 vl1
   ⟶
   vl ≠ [] ∧ exit s (hd vl)"

lemma unwind_exitI[intro?]:
assumes
"⋀ s vl s1 vl1.
   ⟦reachNT s; reach s1; Δe s vl s1 vl1⟧
   ⟹
   vl ≠ [] ∧ exit s (hd vl)"
shows "unwind_exit Δe"
using assms unfolding unwind_exit_def by auto

lemma unwind_cont_mono:
assumes Δs: "unwind_cont Δ Δs"
and Δs': "Δs ⊆ Δs'"
shows "unwind_cont Δ Δs'"
using Δs disjAll_mono[OF _ Δs'] unfolding unwind_cont_def
by (auto intro!: iaction_mono[where Δ = "disjAll Δs" and Δ' = "disjAll Δs'"]
                 reaction_mono[where Δ = "disjAll Δs" and Δ' = "disjAll Δs'"])

fun allConsec :: "'a list ⇒ ('a * 'a) set" where
  "allConsec [] = {}"
| "allConsec [a] = {}"
| "allConsec (a # b # as) = insert (a,b) (allConsec (b#as))"


lemma set_allConsec:
assumes "Δ ∈ set Δs'" and "Δs = Δs' ## Δ1"
shows "∃ Δ2. (Δ,Δ2) ∈ allConsec Δs"
using assms proof (induction Δs' arbitrary: Δs)
  case Nil thus ?case by auto
next
  case (Cons Δ3 Δs' Δs)
  show ?case proof(cases "Δ = Δ3")
    case True
    show ?thesis proof(cases Δs')
      case Nil
      show ?thesis unfolding ‹Δs = (Δ3 # Δs') ## Δ1› Nil True by (rule exI[of _ Δ1]) simp
    next
      case (Cons Δ4 Δs'')
      show ?thesis unfolding ‹Δs = (Δ3 # Δs') ## Δ1› Cons True by (rule exI[of _ Δ4]) simp
    qed
  next
    case False hence "Δ ∈ set Δs'" using Cons by auto
    then obtain Δ2 where "(Δ, Δ2) ∈ allConsec (Δs' ## Δ1)" using Cons by auto
    thus ?thesis unfolding ‹Δs = (Δ3 # Δs') ## Δ1› by (intro exI[of _ Δ2]) (cases Δs', auto)
  qed
qed

lemma allConsec_set:
assumes "(Δ1,Δ2) ∈ allConsec Δs"
shows "Δ1 ∈ set Δs ∧ Δ2 ∈ set Δs"
using assms by (induct Δs rule: allConsec.induct) auto

(* Liniar decomposition: *)
theorem unwind_decomp_secure:
assumes n: "Δs ≠ []"
and i: "⋀ vl vl1. B vl vl1 ⟹ hd Δs istate vl istate vl1"
and c: "⋀ Δ1 Δ2. (Δ1,Δ2) ∈ allConsec Δs ⟹ unwind_cont Δ1 {Δ1, Δ2, Δe}"
and l: "unwind_cont (last Δs) {last Δs, Δe}"
and e: "unwind_exit Δe"
shows secure
proof-
  let ?Δ0 = "hd Δs"  let ?Δs = "insert Δe (set Δs)"
  define "next" where "next Δ1 =
    (if Δ1 = Δe then {}
     else if Δ1 = last Δs then {Δ1,Δe}
     else {Δ1,SOME Δ2. (Δ1,Δ2) ∈ allConsec Δs,Δe})" for Δ1
  show ?thesis
  proof(rule unwind_dec_secure)
    show "?Δ0 ∈ ?Δs" using n by auto
  next
    fix vl vl1 assume "B vl vl1"
    thus "?Δ0 istate vl istate vl1" by fact
  next
    fix Δ
    assume 1: "Δ ∈ ?Δs" show "next Δ ⊆ ?Δs ∧ unwind_to Δ (next Δ)"
    proof-
      {assume "Δ = Δe"
       hence ?thesis using e unfolding next_def unwind_exit_def unwind_to_def by auto
      }
      moreover
      {assume "Δ = last Δs" and "Δ ≠ Δe"
       hence ?thesis using n l unfolding next_def unwind_cont_def unwind_to_def by simp
      }
      moreover
      {assume 1: "Δ ∈ set Δs" and 2: "Δ ≠ last Δs" "Δ ≠ Δe"
       then obtain Δ' Δs' where Δs: "Δs = Δs' ## Δ'" and Δ: "Δ ∈ set Δs'"
       by (metis (no_types) append_Cons append_assoc in_set_conv_decomp last_snoc rev_exhaust)
       have "∃ Δ2. (Δ, Δ2) ∈ allConsec Δs" using set_allConsec[OF Δ Δs] .
       hence "(Δ, SOME Δ2. (Δ, Δ2) ∈ allConsec Δs) ∈ allConsec Δs" by (metis (lifting) someI_ex)
       hence ?thesis using 1 2 c unfolding next_def unwind_cont_def unwind_to_def
       by simp (metis (no_types) allConsec_set)
      }
      ultimately show ?thesis using 1 by blast
    qed
  qed
qed

subsection‹Instances›

corollary unwind_decomp3_secure:
assumes
i: "⋀ vl vl1. B vl vl1 ⟹ Δ1 istate vl istate vl1"
and c1: "unwind_cont Δ1 {Δ1, Δ2, Δe}"
and c2: "unwind_cont Δ2 {Δ2, Δ3, Δe}"
and l: "unwind_cont Δ3 {Δ3, Δe}"
and e: "unwind_exit Δe"
shows secure
apply(rule unwind_decomp_secure[of "[Δ1, Δ2, Δ3]" Δe])
using assms by auto

corollary unwind_decomp4_secure:
assumes
i: "⋀ vl vl1. B vl vl1 ⟹ Δ1 istate vl istate vl1"
and c1: "unwind_cont Δ1 {Δ1, Δ2, Δe}"
and c2: "unwind_cont Δ2 {Δ2, Δ3, Δe}"
and c3: "unwind_cont Δ3 {Δ3, Δ4, Δe}"
and l: "unwind_cont Δ4 {Δ4, Δe}"
and e: "unwind_exit Δe"
shows secure
apply(rule unwind_decomp_secure[of "[Δ1, Δ2, Δ3, Δ4]" Δe])
using assms by auto

corollary unwind_decomp5_secure:
assumes
i: "⋀ vl vl1. B vl vl1 ⟹ Δ1 istate vl istate vl1"
and c1: "unwind_cont Δ1 {Δ1, Δ2, Δe}"
and c2: "unwind_cont Δ2 {Δ2, Δ3, Δe}"
and c3: "unwind_cont Δ3 {Δ3, Δ4, Δe}"
and c4: "unwind_cont Δ4 {Δ4, Δ5, Δe}"
and l: "unwind_cont Δ5 {Δ5, Δe}"
and e: "unwind_exit Δe"
shows secure
apply(rule unwind_decomp_secure[of "[Δ1, Δ2, Δ3, Δ4, Δ5]" Δe])
using assms by auto



subsection ‹A graph alternative presentation›

(* This is more flexible for instantiation. *)

theorem unwind_decomp_secure_graph:
  assumes n: "∀ Δ ∈ Domain Gr. ∃ Δs. Δs ⊆ Domain Gr ∧ (Δ,Δs) ∈ Gr"
  and i: "Δ0 ∈ Domain Gr" "⋀ vl vl1. B vl vl1 ⟹ Δ0 istate vl istate vl1"
  and c: "⋀ Δ. unwind_exit Δ ∨ (∀ Δs. (Δ,Δs) ∈ Gr ⟶ unwind_cont Δ Δs)"
  shows secure
proof -
  let ?pr = "λ Δ Δs. Δs ⊆ Domain Gr ∧ (Δ,Δs) ∈ Gr"
  define "next" where "next Δ = (SOME Δs. ?pr Δ Δs)" for Δ
  let ?Δs = "Domain Gr"
  show ?thesis
  proof(rule unwind_dec_secure)
    show "Δ0 ∈ ?Δs" using i by auto
    fix vl vl1 assume "B vl vl1"
    thus "Δ0 istate vl istate vl1" by fact
  next
    fix Δ
    assume "Δ ∈ ?Δs"
    hence "?pr Δ (next Δ)" using n someI_ex[of "?pr Δ"] unfolding next_def by auto
    hence "next Δ ⊆ ?Δs ∧ (unwind_cont Δ (next Δ) ∨ unwind_exit Δ)" using c by auto
    thus "next Δ ⊆ ?Δs ∧ unwind_to Δ (next Δ)"
      unfolding unwind_to_def unwind_exit_def unwind_cont_def
      by blast
  qed
qed

(*<*)

end (* context BD_Security_IO_Aut *)

end

(*>*)