# Theory Common_Primitive_Matcher_Generic

```theory Common_Primitive_Matcher_Generic
imports "../Semantics_Ternary/Semantics_Ternary"
Common_Primitive_Syntax
"../Semantics_Ternary/Unknown_Match_Tacs"
begin

subsection‹A Generic primitive matcher: Agnostic of IP Addresses›

text‹Generalized Definition agnostic of IP Addresses fro IPv4 and IPv6›

(*generic assumptions for a common matcher without information about IPs.
used to add ipv6 integration without duplicating all proofs *)
locale primitive_matcher_generic =
fixes β :: "('i::len common_primitive, ('i::len, 'a) tagged_packet_scheme) exact_match_tac"
assumes IIface: "∀ p i. β (IIface i) p = bool_to_ternary (match_iface i (p_iiface p))"
and OIface: "∀ p i. β (OIface i) p = bool_to_ternary (match_iface i (p_oiface p))"
and Prot: "∀ p proto. β (Prot proto) p = bool_to_ternary (match_proto proto (p_proto p))"
and Src_Ports: "∀ p proto ps. β (Src_Ports (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ p_sport p ∈ ports_to_set ps)"
and Dst_Ports: "∀ p proto ps. β (Dst_Ports (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ p_dport p ∈ ports_to_set ps)"
― ‹-m multiport --ports matches source or destination port›
and MultiportsPorts: "∀ p proto ps. β (MultiportPorts (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ (p_sport p ∈ ports_to_set ps ∨ p_dport p ∈ ports_to_set ps))"
and L4_Flags: "∀ p flags. β (L4_Flags flags) p = bool_to_ternary (match_tcp_flags flags (p_tcp_flags p))"
and CT_State: "∀ p S. β (CT_State S) p = bool_to_ternary (match_ctstate S (p_tag_ctstate p))"
and Extra: "∀ p str. β (Extra str) p = TernaryUnknown"
begin
lemma Iface_single:
"matches (β, α) (Match (IIface X)) a p ⟷ match_iface X (p_iiface p)"
"matches (β, α) (Match (OIface X)) a p ⟷ match_iface X (p_oiface p)"
by(simp_all add: IIface OIface match_raw_ternary bool_to_ternary_simps
split: ternaryvalue.split)
text‹Since matching on the iface cannot be @{const TernaryUnknown}*, we can pull out negations.›
lemma Iface_single_not:
"matches (β, α) (MatchNot (Match (IIface X))) a p ⟷ ¬ match_iface X (p_iiface p)"
"matches (β, α) (MatchNot (Match (OIface X))) a p ⟷ ¬ match_iface X (p_oiface p)"
by(simp_all add: IIface OIface matches_case_ternaryvalue_tuple bool_to_ternary_simps
split: ternaryvalue.split)

lemma Prot_single:
"matches (β, α) (Match (Prot X)) a p ⟷ match_proto X (p_proto p)"
by(simp add: Prot match_raw_ternary bool_to_ternary_simps split: ternaryvalue.split)
lemma Prot_single_not:
"matches (β, α) (MatchNot (Match (Prot X))) a p ⟷ ¬ match_proto X (p_proto p)"
by(simp add: Prot matches_case_ternaryvalue_tuple bool_to_ternary_simps split: ternaryvalue.split)

lemma Ports_single:
"matches (β, α) (Match (Src_Ports (L4Ports proto ps))) a p ⟷ proto = p_proto p ∧ p_sport p ∈ ports_to_set ps"
"matches (β, α) (Match (Dst_Ports (L4Ports proto ps))) a p ⟷ proto = p_proto p ∧ p_dport p ∈ ports_to_set ps"
by(simp_all add: Src_Ports Dst_Ports match_raw_ternary bool_to_ternary_simps
split: ternaryvalue.split)
lemma Ports_single_not:
"matches (β, α) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p ⟷ proto ≠ p_proto p ∨ p_sport p ∉ ports_to_set ps"
"matches (β, α) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p ⟷ proto ≠ p_proto p ∨ p_dport p ∉ ports_to_set ps"
by(simp_all add: Src_Ports Dst_Ports matches_case_ternaryvalue_tuple bool_to_ternary_simps
split: ternaryvalue.split)

text‹Ports are dependent matches. They always match on the protocol too›
lemma Ports_single_rewrite_Prot:
"matches (β, α) (Match (Src_Ports (L4Ports proto ps))) a p ⟷
matches (β, α) (Match (Prot (Proto proto))) a p ∧ p_sport p ∈ ports_to_set ps"
"matches (β, α) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p ⟷
matches (β, α) (MatchNot (Match (Prot (Proto proto)))) a p ∨ p_sport p ∉ ports_to_set ps"
"matches (β, α) (Match (Dst_Ports (L4Ports proto ps))) a p ⟷
matches (β, α) (Match (Prot (Proto proto))) a p ∧ p_dport p ∈ ports_to_set ps"
"matches (β, α) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p ⟷
matches (β, α) (MatchNot (Match (Prot (Proto proto)))) a p ∨ p_dport p ∉ ports_to_set ps"
by(auto simp add: Ports_single_not Ports_single Prot_single_not Prot_single)

lemma multiports_disjuction:
"(∃rg∈set spts. matches (β, α) (Match (Src_Ports (L4Ports proto [rg]))) a p) ⟷ matches (β, α) (Match (Src_Ports (L4Ports proto spts))) a p"
"(∃rg∈set dpts. matches (β, α) (Match (Dst_Ports (L4Ports proto [rg]))) a p) ⟷ matches (β, α) (Match (Dst_Ports (L4Ports proto dpts))) a p"
by(auto simp add: Src_Ports Dst_Ports match_raw_ternary bool_to_ternary_simps ports_to_set
split: ternaryvalue.split)

lemma MultiportPorts_single_rewrite:
"matches (β, α) (Match (MultiportPorts ports)) a p ⟷
matches (β, α) (Match (Src_Ports ports)) a p ∨ matches (β, α) (Match (Dst_Ports ports)) a p"
apply(cases ports)
split: ternaryvalue.split)
lemma MultiportPorts_single_rewrite_MatchOr:
"matches (β, α) (Match (MultiportPorts ports)) a p ⟷
matches (β, α) (MatchOr (Match (Src_Ports ports)) (Match (Dst_Ports ports))) a p"
apply(cases ports)

lemma MultiportPorts_single_not_rewrite_MatchAnd:
"matches (β, α) (MatchNot (Match (MultiportPorts ports))) a p ⟷
matches (β, α) (MatchAnd (MatchNot (Match (Src_Ports ports))) (MatchNot (Match (Dst_Ports ports)))) a p"
apply(cases ports)
split: ternaryvalue.split)
lemma MultiportPorts_single_not_rewrite:
"matches (β, α) (MatchNot (Match (MultiportPorts ports))) a p ⟷
¬ matches (β, α) (Match (Src_Ports ports)) a p ∧ ¬ matches (β, α) (Match (Dst_Ports ports)) a p"
apply(cases ports)
Ports_single_not Ports_single)

lemma Extra_single:
"matches (β, α) (Match (Extra str)) a p ⟷ α a p"
lemma Extra_single_not:  ― ‹ternary logic, @{text "¬ unknown = unknown"}›
"matches (β, α) (MatchNot (Match (Extra str))) a p ⟷ α a p"
end

subsection‹Basic optimisations›

(*this is currently not used.*)
text‹Compress many @{const Extra} expressions to one expression.›
fun compress_extra :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"compress_extra (Match x) = Match x" |
"compress_extra (MatchNot (Match (Extra e))) = Match (Extra (''NOT (''@e@'')''))" |
"compress_extra (MatchNot m) = (MatchNot (compress_extra m))" |
(*"compress_extra (MatchAnd (Match (Extra e1)) (Match (Extra e2))) = compress_extra (Match (Extra (e1@'' ''@e2)))" |*)
(*"compress_extra (MatchAnd (Match (Extra e1)) MatchAny) = Match (Extra e1)" |*)
"compress_extra (MatchAnd (Match (Extra e1)) m2) = (case compress_extra m2 of Match (Extra e2) ⇒ Match (Extra (e1@'' ''@e2)) | MatchAny ⇒ Match (Extra e1) | m2' ⇒ MatchAnd (Match (Extra e1)) m2')" |
"compress_extra (MatchAnd m1 m2) = MatchAnd (compress_extra m1) (compress_extra m2)" |
(*"compress_extra (MatchAnd m1 m2) = (case (compress_extra m1, compress_extra m2) of
(Match (Extra e1), Match (Extra e2)) ⇒ Match (Extra (e1@'' ''@e2))
| (Match (Extra e1), MatchAny) ⇒ Match (Extra e1)
| (MatchAny, Match (Extra e2)) ⇒ Match (Extra e2)
| (m1', m2') ⇒ MatchAnd m1' m2')" |*)
"compress_extra MatchAny = MatchAny"

thm compress_extra.simps

value [nbe] "compress_extra (MatchAnd (Match (Extra ''foo'')) (Match (Extra ''bar'')))"
value [nbe] "compress_extra (MatchAnd (Match (Extra ''foo'')) (MatchNot (Match (Extra ''bar''))))"
value [nbe] "compress_extra (MatchAnd (Match (Extra ''-m'')) (MatchAnd (Match (Extra ''addrtype'')) (MatchAnd (Match (Extra ''--dst-type'')) (MatchAnd (Match (Extra ''BROADCAST'')) MatchAny))))"

lemma compress_extra_correct_matchexpr:
fixes β::"('i::len common_primitive, ('i::len, 'a) tagged_packet_scheme) exact_match_tac"
assumes generic: "primitive_matcher_generic β"
shows "matches (β, α) m = matches (β, α) (compress_extra m)"
proof(simp add: fun_eq_iff, clarify, rename_tac a p)
fix a and p :: "('i, 'a) tagged_packet_scheme"
from generic have "β (Extra e) p = TernaryUnknown" for e by(simp add: primitive_matcher_generic.Extra)
hence "ternary_ternary_eval (map_match_tac β p m) = ternary_ternary_eval (map_match_tac β p (compress_extra m))"
proof(induction m rule: compress_extra.induct)
case 4 thus ?case
by(simp_all split: match_expr.split match_expr.split_asm common_primitive.split)
qed (simp_all)
thus "matches (β, α) m a p = matches (β, α) (compress_extra m) a p"
by(rule matches_iff_apply_f)
qed

end
```