Theory Conntrack_State

theory Conntrack_State
imports "../Common/Negation_Type" Simple_Firewall.Lib_Enum_toString
begin


datatype ctstate = CT_New | CT_Established | CT_Related | CT_Untracked | CT_Invalid

text‹The state associated with a packet can be added as a tag to the packet.
      See @{file ‹../Semantics_Stateful.thy›}.›

fun match_ctstate :: "ctstate set ⇒ ctstate ⇒ bool" where
"match_ctstate S s_tag ⟷ s_tag ∈ S"

fun ctstate_conjunct :: "ctstate set ⇒ ctstate set ⇒ ctstate set option" where
  "ctstate_conjunct S1 S2 = (if S1 ∩ S2 = {} then None else Some (S1 ∩ S2))"

value[code] "ctstate_conjunct {CT_Established, CT_New} {CT_New}"

lemma ctstate_conjunct_correct: "match_ctstate S1 pkt ∧ match_ctstate S2 pkt ⟷ 
  (case ctstate_conjunct S1 S2 of None ⇒ False | Some S' ⇒ match_ctstate S' pkt)"
  apply simp
  by blast

lemma UNIV_ctstate: "UNIV = {CT_New, CT_Established, CT_Related, CT_Untracked, CT_Invalid}" using ctstate.exhaust by auto 

(*
function ctstate_set_toString_list :: "ctstate set ⇒ string list" where
  "ctstate_set_toString_list S = (if S = {} then [] else
    if CT_New ∈ S then ''NEW''#ctstate_set_toString_list (S - {CT_New}) else
    if CT_Established ∈ S then ''ESTABLISHED''#ctstate_set_toString_list (S - {CT_Established}) else
    if CT_Related ∈ S then ''RELATED''#ctstate_set_toString_list (S - {CT_Related}) else
    if CT_Untracked ∈ S then ''UNTRACKED''#ctstate_set_toString_list (S - {CT_Untracked}) else [''ERROR-unkown-ctstate''])"
by(pat_completeness) auto

termination ctstate_set_toString_list
  apply(relation "measure (λ(S). card S)")
  apply(simp_all add: card_gt_0_iff)
  done

*)
instance ctstate :: finite
proof
  from UNIV_ctstate show "finite (UNIV:: ctstate set)" using finite.simps by auto 
qed

  
lemma "finite (S :: ctstate set)" by simp


instantiation "ctstate" :: enum
begin
  definition "enum_ctstate = [CT_New, CT_Established, CT_Related, CT_Untracked, CT_Invalid]"

  definition "enum_all_ctstate P ⟷ P CT_New ∧ P CT_Established ∧ P CT_Related ∧ P CT_Untracked ∧ P CT_Invalid"
  
  definition "enum_ex_ctstate P ⟷ P CT_New ∨ P CT_Established ∨ P CT_Related ∨ P CT_Untracked ∨ P CT_Invalid"
instance proof
  show "UNIV = set (enum_class.enum :: ctstate list)"
    by(simp add: UNIV_ctstate enum_ctstate_def)
  next
  show "distinct (enum_class.enum :: ctstate list)"
    by(simp add: enum_ctstate_def)
  next
  show "⋀P. (enum_class.enum_all :: (ctstate ⇒ bool) ⇒ bool) P = Ball UNIV P"
    by(simp add: UNIV_ctstate enum_all_ctstate_def)
  next
  show "⋀P. (enum_class.enum_ex :: (ctstate ⇒ bool) ⇒ bool) P = Bex UNIV P"
    by(simp add: UNIV_ctstate enum_ex_ctstate_def)
qed
end

definition ctstate_is_UNIV :: "ctstate set ⇒ bool" where
  "ctstate_is_UNIV c ≡ CT_New ∈ c ∧ CT_Established ∈ c ∧ CT_Related ∈ c ∧ CT_Untracked ∈ c ∧ CT_Invalid ∈ c"

lemma ctstate_is_UNIV: "ctstate_is_UNIV c ⟷ c = UNIV"
  unfolding ctstate_is_UNIV_def
  apply(simp add: UNIV_ctstate)
  apply(rule iffI)
  apply(clarify)
   using UNIV_ctstate apply fastforce
   apply(simp)
  done


value[code] "ctstate_is_UNIV {CT_Established}"



fun ctstate_toString :: "ctstate ⇒ string" where
  "ctstate_toString CT_New = ''NEW''" |
  "ctstate_toString CT_Established = ''ESTABLISHED''" |
  "ctstate_toString CT_Related = ''RELATED''" |
  "ctstate_toString CT_Untracked = ''UNTRACKED''" |
  "ctstate_toString CT_Invalid = ''INVALID''"


definition ctstate_set_toString :: "ctstate set ⇒ string" where
  "ctstate_set_toString S = list_separated_toString '','' ctstate_toString (enum_set_to_list S)"

lemma "ctstate_set_toString {CT_New, CT_New, CT_Established} = ''NEW,ESTABLISHED''" by eval


end