Theory Conntrack_State_Transform

theory Conntrack_State_Transform
imports Common_Primitive_Matcher
        "../Semantics_Ternary/Semantics_Ternary"
begin


text‹The following function assumes that the packet is in a certain state.›

fun ctstate_assume_state :: "ctstate ⇒ 'i::len  common_primitive match_expr ⇒ 'i common_primitive match_expr" where
  "ctstate_assume_state s (Match (CT_State x)) = (if s ∈ x then MatchAny else MatchNot MatchAny)" |
  "ctstate_assume_state s (Match m) = Match m" |
  "ctstate_assume_state s (MatchNot m) = MatchNot (ctstate_assume_state s m)" |
  "ctstate_assume_state _ MatchAny = MatchAny" |
  "ctstate_assume_state s (MatchAnd m1 m2) = MatchAnd (ctstate_assume_state s m1) (ctstate_assume_state s m2)"

lemma ctstate_assume_state: "p_tag_ctstate p = s ⟹
    matches (common_matcher, α) (ctstate_assume_state s m) a p ⟷ matches (common_matcher, α) m a p"
apply(rule matches_iff_apply_f)
by(induction m rule: ctstate_assume_state.induct) (simp_all)


definition ctstate_assume_new :: "'i::len  common_primitive rule list ⇒ 'i common_primitive rule list" where
  "ctstate_assume_new ≡ optimize_matches (ctstate_assume_state CT_New)"

lemma ctstate_assume_new_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (ctstate_assume_new rs)"
  by (simp add: ctstate_assume_new_def optimize_matches_simple_ruleset)

text‹Usually, the interesting part of a firewall is only about the rules for setting up connections.
      That means, we mostly only care about packets in state @{const CT_New}.
      Use the function @{const ctstate_assume_new} to remove all state matching and just care about
      the connection setup.
›
corollary ctstate_assume_new: "p_tag_ctstate p = CT_New ⟹ 
  approximating_bigstep_fun (common_matcher, α) p (ctstate_assume_new rs) s = approximating_bigstep_fun (common_matcher, α) p rs s"
unfolding ctstate_assume_new_def
apply(rule optimize_matches)
apply(simp add: ctstate_assume_state)
done

text‹If we assume the CT State is @{const CT_New}, we can also assume that the TCP SYN flag (@{const ipt_tcp_syn}) is set.›

fun ipt_tcp_flags_assume_flag :: "ipt_tcp_flags ⇒ 'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
  "ipt_tcp_flags_assume_flag flg (Match (L4_Flags x)) = (if ipt_tcp_flags_equal x flg then MatchAny else (case match_tcp_flags_conjunct_option x flg of None ⇒ MatchNot MatchAny | Some f3 ⇒ Match (L4_Flags f3)))" |
  "ipt_tcp_flags_assume_flag flg (Match m) = Match m" |
  "ipt_tcp_flags_assume_flag flg (MatchNot m) = MatchNot (ipt_tcp_flags_assume_flag flg m)" |
  "ipt_tcp_flags_assume_flag _ MatchAny = MatchAny" |
  "ipt_tcp_flags_assume_flag flg (MatchAnd m1 m2) = MatchAnd (ipt_tcp_flags_assume_flag flg m1) (ipt_tcp_flags_assume_flag flg m2)"

lemma ipt_tcp_flags_assume_flag: assumes "match_tcp_flags flg (p_tcp_flags p)"
    shows "matches (common_matcher, α) (ipt_tcp_flags_assume_flag flg m) a p ⟷ matches (common_matcher, α) m a p"
proof(rule matches_iff_apply_f)
show "ternary_ternary_eval (map_match_tac common_matcher p (ipt_tcp_flags_assume_flag flg m)) = ternary_ternary_eval (map_match_tac common_matcher p m)"
  using assms proof(induction m rule: ipt_tcp_flags_assume_flag.induct)
  case (1 flg x)
    thus ?case
    apply(simp add: ipt_tcp_flags_equal del: match_tcp_flags.simps)
    apply(cases "match_tcp_flags_conjunct_option x flg")
     apply(simp)
     using match_tcp_flags_conjunct_option_None bool_to_ternary_simps(2) apply metis
    apply(simp)
    apply(drule_tac pkt="(p_tcp_flags p)" in match_tcp_flags_conjunct_option_Some)
    by simp
  qed(simp_all del: match_tcp_flags.simps)
qed

definition ipt_tcp_flags_assume_syn :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where
  "ipt_tcp_flags_assume_syn ≡ optimize_matches (ipt_tcp_flags_assume_flag ipt_tcp_syn)"

lemma ipt_tcp_flags_assume_syn_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (ipt_tcp_flags_assume_syn rs)"
  by (simp add: ipt_tcp_flags_assume_syn_def optimize_matches_simple_ruleset)

corollary ipt_tcp_flags_assume_syn: "match_tcp_flags ipt_tcp_syn (p_tcp_flags p) ⟹
  approximating_bigstep_fun (common_matcher, α) p (ipt_tcp_flags_assume_syn rs) s = approximating_bigstep_fun (common_matcher, α) p rs s"
unfolding ipt_tcp_flags_assume_syn_def
apply(rule optimize_matches)
apply(simp add: ipt_tcp_flags_assume_flag)
done





definition packet_assume_new :: "'i::len common_primitive rule list ⇒ 'i common_primitive rule list" where
  "packet_assume_new ≡ ctstate_assume_new ∘ ipt_tcp_flags_assume_syn"

lemma packet_assume_new_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (packet_assume_new rs)"
  by (simp add: packet_assume_new_def ipt_tcp_flags_assume_syn_simple_ruleset ctstate_assume_new_simple_ruleset)

corollary packet_assume_new: "match_tcp_flags ipt_tcp_syn (p_tcp_flags p) ⟹ p_tag_ctstate p = CT_New ⟹ 
  approximating_bigstep_fun (common_matcher, α) p (packet_assume_new rs) s = approximating_bigstep_fun (common_matcher, α) p rs s"
unfolding packet_assume_new_def
by (simp add: ctstate_assume_new ipt_tcp_flags_assume_syn)

  



end