<commit_before>theory Packet_Set
imports Fixed_Action "Output_Format/Negation_Type_Matching" Datatype_Selectors
begin

section{*Packet Set*}
(*probably everything here wants a simple ruleset*)

text{*@{const alist_and} transforms @{typ "'a negation_type list \<Rightarrow> 'a match_expr"} and uses conjunction as connective. *}

subsection{*Executable Packet Set Representation*}

(*
text{*Symbolic (executable) representation. inner is @{text \<and>}, outer is @{text \<or>}*}
datatype_new 'a packet_set = PacketSet (packet_set_repr: "('a negation_type list) list")

(*generalize remove unknown matches*)

(*irgendwie muss hier \<gamma> a rein
TODO: first remove all unknowns?
*)
definition to_packet_set :: "'a match_expr \<Rightarrow> 'a packet_set" where
 "to_packet_set m = PacketSet (map to_negation_type_nnf (normalize_match m))"

definition packet_set_to_set :: "('a, 'packet) match_tac \<Rightarrow> action \<Rightarrow> 'a packet_set \<Rightarrow> 'packet set" where
  "packet_set_to_set \<gamma> a ps \<equiv> {p. \<exists> as \<in> set (packet_set_repr ps). matches \<gamma> (alist_and as) a p}"

lemma to_packet_set_correct: "p \<in> packet_set_to_set \<gamma> a (to_packet_set m) \<longleftrightarrow> matches \<gamma> m a p"
apply(simp add: to_packet_set_def packet_set_to_set_def)
apply(rule iffI)
 apply(clarify)
 apply(induction m rule: normalize_match.induct)
       apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (smt2 alist_and_append imageE matches_simp2 matches_simp22 to_negation_type_nnf.simps(4))
apply (metis matches_DeMorgan)
apply(induction m rule: normalize_match.induct)
      apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (metis alist_and_append matches_simp1)
apply (metis Un_iff matches_DeMorgan)
done

(*'a packet_set \<Rightarrow> 'a packet_set*)
fun packet_set_filter :: "('a, 'p) match_tac \<Rightarrow> action \<Rightarrow> ('p \<Rightarrow> bool) \<Rightarrow> ('a negation_type list) list \<Rightarrow> ('a negation_type list) list" where
  "packet_set_filter _ _ _ [] = []" |
  "packet_set_filter \<gamma> a f (n#ns) = [] @ packet_set_filter \<gamma> a f ns"
*)

text{*Symbolic (executable) representation. inner is @{text \<and>}, outer is @{text \<or>}*}
(*we remember the action which might be necessary for applying \<alpha>*)
datatype_new 'a packet_set = PacketSet (packet_set_repr: "(('a negation_type \<times> action) list) list")

definition to_packet_set :: "action \<Rightarrow> 'a match_expr \<Rightarrow> 'a packet_set" where
 "to_packet_set a m = PacketSet (map (map (\<lambda>m'. (m',a)) o to_negation_type_nnf) (normalize_match m))"

definition packet_set_to_set :: "('a, 'packet) match_tac \<Rightarrow> 'a packet_set \<Rightarrow> 'packet set" where
  "packet_set_to_set \<gamma> ps \<equiv> \<Union> ms \<in> set (packet_set_repr ps).  {p. \<forall> (m, a) \<in> set ms. matches \<gamma> (negation_type_to_match_expr m) a p}"

lemma to_packet_set_correct: "p \<in> packet_set_to_set \<gamma> (to_packet_set a m) \<longleftrightarrow> matches \<gamma> m a p"
apply(simp add: to_packet_set_def packet_set_to_set_def)
apply(rule iffI)
 apply(clarify)
 apply(induction m rule: normalize_match.induct)
       apply(simp_all add: bunch_of_lemmata_about_matches)
   apply force
apply (metis matches_DeMorgan)
apply(induction m rule: normalize_match.induct)
      apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (metis Un_iff)
apply (metis Un_iff matches_DeMorgan)
done

text{*If the matching agrees for two actions, then the packet sets are also equal*}
lemma "\<forall>p. matches \<gamma> m a1 p \<longleftrightarrow> matches \<gamma> m a2 p \<Longrightarrow> packet_set_to_set \<gamma> (to_packet_set a1 m) = packet_set_to_set \<gamma> (to_packet_set a2 m)"
apply(subst(asm) to_packet_set_correct[symmetric])+
apply safe
apply simp_all
done

fun packet_set_and :: "'a packet_set \<Rightarrow> 'a packet_set \<Rightarrow> 'a packet_set" where
  "packet_set_and (PacketSet olist1) (PacketSet olist2) = PacketSet [andlist1 @ andlist2. andlist1 <- olist1, andlist2 <- olist2]"

value "packet_set_and (PacketSet [[a,b], [c,d]]) (PacketSet [[v,w], [x,y]])"

declare packet_set_and.simps[simp del]

lemma packet_set_and_correct: "packet_set_to_set \<gamma> (packet_set_and (to_packet_set a m1) (to_packet_set a m2)) = packet_set_to_set \<gamma> (to_packet_set a (MatchAnd m1 m2))"
 apply(simp add: to_packet_set_def packet_set_and.simps packet_set_to_set_def)
 by fast
 
lemma packet_set_and_correct': "p \<in> packet_set_to_set \<gamma> (packet_set_and (to_packet_set a m1) (to_packet_set a m2)) \<longleftrightarrow> matches \<gamma> (MatchAnd m1 m2) a p"
apply(simp add: to_packet_set_correct[symmetric])
using packet_set_and_correct by fast

fun internal_packet_set_contrain :: "action \<Rightarrow> 'a match_expr \<Rightarrow> 'a packet_set \<Rightarrow> 'a packet_set" where
  "internal_packet_set_contrain a m ns = packet_set_and ns (to_packet_set a m)"

(*TODO*)




subsection{*The set of all accepted packets*}
text{*
Collect all packets which are allowed by the firewall.
*}
fun collect_allow :: "('a, 'p) match_tac \<Rightarrow> 'a rule list \<Rightarrow> 'p set \<Rightarrow> 'p set" where
  "collect_allow _ [] P = {}" |
  "collect_allow \<gamma> ((Rule m Accept)#rs) P = {p \<in> P. matches \<gamma> m Accept p} \<union> (collect_allow \<gamma> rs {p \<in> P. \<not> matches \<gamma> m Accept p})" |
  "collect_allow \<gamma> ((Rule m Drop)#rs) P = (collect_allow \<gamma> rs {p \<in> P. \<not> matches \<gamma> m Drop p})"

lemma collect_allow_subset: "simple_ruleset rs \<Longrightarrow> collect_allow \<gamma> rs P \<subseteq> P"
apply(induction rs arbitrary: P)
 apply(simp)
apply(rename_tac r rs P)
apply(case_tac r, rename_tac m a)<commit_msg>packet set constrain<commit_after>theory Packet_Set
imports Fixed_Action "Output_Format/Negation_Type_Matching" Datatype_Selectors
begin

section{*Packet Set*}
(*probably everything here wants a simple ruleset*)

text{*@{const alist_and} transforms @{typ "'a negation_type list \<Rightarrow> 'a match_expr"} and uses conjunction as connective. *}

subsection{*Executable Packet Set Representation*}

(*
text{*Symbolic (executable) representation. inner is @{text \<and>}, outer is @{text \<or>}*}
datatype_new 'a packet_set = PacketSet (packet_set_repr: "('a negation_type list) list")

(*generalize remove unknown matches*)

(*irgendwie muss hier \<gamma> a rein
TODO: first remove all unknowns?
*)
definition to_packet_set :: "'a match_expr \<Rightarrow> 'a packet_set" where
 "to_packet_set m = PacketSet (map to_negation_type_nnf (normalize_match m))"

definition packet_set_to_set :: "('a, 'packet) match_tac \<Rightarrow> action \<Rightarrow> 'a packet_set \<Rightarrow> 'packet set" where
  "packet_set_to_set \<gamma> a ps \<equiv> {p. \<exists> as \<in> set (packet_set_repr ps). matches \<gamma> (alist_and as) a p}"

lemma to_packet_set_correct: "p \<in> packet_set_to_set \<gamma> a (to_packet_set m) \<longleftrightarrow> matches \<gamma> m a p"
apply(simp add: to_packet_set_def packet_set_to_set_def)
apply(rule iffI)
 apply(clarify)
 apply(induction m rule: normalize_match.induct)
       apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (smt2 alist_and_append imageE matches_simp2 matches_simp22 to_negation_type_nnf.simps(4))
apply (metis matches_DeMorgan)
apply(induction m rule: normalize_match.induct)
      apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (metis alist_and_append matches_simp1)
apply (metis Un_iff matches_DeMorgan)
done

(*'a packet_set \<Rightarrow> 'a packet_set*)
fun packet_set_filter :: "('a, 'p) match_tac \<Rightarrow> action \<Rightarrow> ('p \<Rightarrow> bool) \<Rightarrow> ('a negation_type list) list \<Rightarrow> ('a negation_type list) list" where
  "packet_set_filter _ _ _ [] = []" |
  "packet_set_filter \<gamma> a f (n#ns) = [] @ packet_set_filter \<gamma> a f ns"
*)

text{*Symbolic (executable) representation. inner is @{text \<and>}, outer is @{text \<or>}*}
(*we remember the action which might be necessary for applying \<alpha>*)
datatype_new 'a packet_set = PacketSet (packet_set_repr: "(('a negation_type \<times> action) list) list")

definition to_packet_set :: "action \<Rightarrow> 'a match_expr \<Rightarrow> 'a packet_set" where
 "to_packet_set a m = PacketSet (map (map (\<lambda>m'. (m',a)) o to_negation_type_nnf) (normalize_match m))"

definition packet_set_to_set :: "('a, 'packet) match_tac \<Rightarrow> 'a packet_set \<Rightarrow> 'packet set" where
  "packet_set_to_set \<gamma> ps \<equiv> \<Union> ms \<in> set (packet_set_repr ps).  {p. \<forall> (m, a) \<in> set ms. matches \<gamma> (negation_type_to_match_expr m) a p}"

lemma to_packet_set_correct: "p \<in> packet_set_to_set \<gamma> (to_packet_set a m) \<longleftrightarrow> matches \<gamma> m a p"
apply(simp add: to_packet_set_def packet_set_to_set_def)
apply(rule iffI)
 apply(clarify)
 apply(induction m rule: normalize_match.induct)
       apply(simp_all add: bunch_of_lemmata_about_matches)
   apply force
apply (metis matches_DeMorgan)
apply(induction m rule: normalize_match.induct)
      apply(simp_all add: bunch_of_lemmata_about_matches)
 apply (metis Un_iff)
apply (metis Un_iff matches_DeMorgan)
done

lemma to_packet_set_set: "packet_set_to_set \<gamma> (to_packet_set a m) = {p. matches \<gamma> m a p}"
using to_packet_set_correct by fast


text{*If the matching agrees for two actions, then the packet sets are also equal*}
lemma "\<forall>p. matches \<gamma> m a1 p \<longleftrightarrow> matches \<gamma> m a2 p \<Longrightarrow> packet_set_to_set \<gamma> (to_packet_set a1 m) = packet_set_to_set \<gamma> (to_packet_set a2 m)"
apply(subst(asm) to_packet_set_correct[symmetric])+
apply safe
apply simp_all
done

fun packet_set_and :: "'a packet_set \<Rightarrow> 'a packet_set \<Rightarrow> 'a packet_set" where
  "packet_set_and (PacketSet olist1) (PacketSet olist2) = PacketSet [andlist1 @ andlist2. andlist1 <- olist1, andlist2 <- olist2]"

value "packet_set_and (PacketSet [[a,b], [c,d]]) (PacketSet [[v,w], [x,y]])"

declare packet_set_and.simps[simp del]

lemma packet_set_and_correct: "packet_set_to_set \<gamma> (packet_set_and (to_packet_set a m1) (to_packet_set a m2)) = packet_set_to_set \<gamma> (to_packet_set a (MatchAnd m1 m2))"
 apply(simp add: to_packet_set_def packet_set_and.simps packet_set_to_set_def)
 by fast
 
lemma packet_set_and_correct': "p \<in> packet_set_to_set \<gamma> (packet_set_and (to_packet_set a m1) (to_packet_set a m2)) \<longleftrightarrow> matches \<gamma> (MatchAnd m1 m2) a p"
apply(simp add: to_packet_set_correct[symmetric])
using packet_set_and_correct by fast

(*TODO move*)
lemma packet_set_to_set_alt:  "packet_set_to_set \<gamma> ps = (\<Union> ms \<in> set (packet_set_repr ps).  {p. \<forall> m a. (m, a) \<in> set ms \<longrightarrow> matches \<gamma> (negation_type_to_match_expr m) a p})"
unfolding packet_set_to_set_def
by fast

lemma packet_set_and_union: "packet_set_to_set \<gamma> (packet_set_and P1 P2) = packet_set_to_set \<gamma> P1 \<inter> packet_set_to_set \<gamma> P2"
unfolding packet_set_to_set_alt
 apply(cases P1)
 apply(cases P2)
 apply(simp)
 apply(simp add: packet_set_and.simps)
 apply blast
done



definition packet_set_constrain :: "action \<Rightarrow> 'a match_expr \<Rightarrow> 'a packet_set \<Rightarrow> 'a packet_set" where
  "packet_set_constrain a m ns = packet_set_and ns (to_packet_set a m)"


lemma packet_set_constrain_correct: "packet_set_to_set \<gamma> (packet_set_constrain a m P) = {p \<in> packet_set_to_set \<gamma> P. matches \<gamma> m a p}"
unfolding packet_set_constrain_def
unfolding packet_set_and_union
unfolding to_packet_set_set
by blast

(*
(*scratch*)
lemma "(\<not> ((a1 \<and> a2) \<or> b \<or> c)) = ((\<not>a1 \<and> \<not> b \<and> \<not> c) \<or> (\<not>a2 \<and> \<not> b \<and> \<not> c))" by blast
(*TODO: how?*)

fun listprepend :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
  "listprepend [] ns = []" |
  "listprepend (a#as) ns = (a#ns) # (listprepend as ns)"

lemma "listprepend [a,b,c] ns = [a#ns, b#ns, c#ns]" by simp


fun packet_set_not_internal :: " ('a negation_type \<times> action) list list \<Rightarrow>  ('a negation_type \<times> action) list list" where
  "packet_set_not_internal [] = []" |
  "packet_set_not_internal (ns#nss) = listprepend (map (\<lambda>(n,a). (invert n,a)) ns) (packet_set_not_internal nss)"

fun packet_set_not :: "'a packet_set \<Rightarrow> 'a packet_set" where
  "packet_set_not (PacketSet ps) = PacketSet [map (\<lambda>(n,a). (invert n,a)) ns. ns <- ps]"

declare packet_set_not.simps[simp del]

lemma "packet_set_to_set \<gamma> (packet_set_not P) = - packet_set_to_set \<gamma> P"
apply(cases P)
apply(simp)
apply(simp add: packet_set_not.simps)
apply(simp add: packet_set_to_set_alt)
apply(safe)
oops
(*end scratch*)
*)




subsection{*The set of all accepted packets*}
text{*
Collect all packets which are allowed by the firewall.
*}
fun collect_allow :: "('a, 'p) match_tac \<Rightarrow> 'a rule list \<Rightarrow> 'p set \<Rightarrow> 'p set" where
  "collect_allow _ [] P = {}" |
  "collect_allow \<gamma> ((Rule m Accept)#rs) P = {p \<in> P. matches \<gamma> m Accept p} \<union> (collect_allow \<gamma> rs {p \<in> P. \<not> matches \<gamma> m Accept p})" |
  "collect_allow \<gamma> ((Rule m Drop)#rs) P = (collect_allow \<gamma> rs {p \<in> P. \<not> matches \<gamma> m Drop p})"

lemma collect_allow_subset: "simple_ruleset rs \<Longrightarrow> collect_allow \<gamma> rs P \<subseteq> P"
apply(induction rs arbitrary: P)
 apply(simp)
apply(rename_tac r rs P)
apply(case_tac r, rename_tac m a)
{'fraction_non_alphanumeric': 0.13217799970627112, 'fraction_numerical': 0.004552797767660449, 'mean_word_length': 5.692383292383292, 'pattern_counts': {'":': 0, '<': 214, '<?xml version=': 0, '>': 209, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6835666', 'n_tokens_mistral': 5210, 'n_tokens_neox': 4857, 'n_words': 1448}