# Theory Protocols_Normalize

```theory Protocols_Normalize
imports Common_Primitive_Lemmas
"../Common/Word_Upto"
begin

section‹Optimizing Protocols›

section‹Optimizing protocols in match expressions›

fun compress_pos_protocols :: "protocol list ⇒ protocol option" where
"compress_pos_protocols [] = Some ProtoAny" |
"compress_pos_protocols [p] = Some p" |
"compress_pos_protocols (p1#p2#ps) = (case simple_proto_conjunct p1 p2 of None ⇒ None | Some p ⇒ compress_pos_protocols (p#ps))"

lemma compress_pos_protocols_Some: "compress_pos_protocols ps = Some proto ⟹
match_proto proto p_prot ⟷ (∀ p ∈ set ps. match_proto p p_prot)"
proof(induction ps rule: compress_pos_protocols.induct)
case (3 p1 p2 pps) thus ?case
apply(cases "simple_proto_conjunct p1 p2")
apply(simp; fail)
using simple_proto_conjunct_Some by(simp)
qed(simp)+

lemma compress_pos_protocols_None: "compress_pos_protocols ps = None ⟹
¬ (∀ proto ∈ set ps. match_proto proto p_prot)"
proof(induction ps rule: compress_pos_protocols.induct)
case (3 i1 i2 iis) thus ?case
apply(cases "simple_proto_conjunct i1 i2")
apply(simp_all)
using simple_proto_conjunct_None apply blast
using simple_proto_conjunct_Some by blast
qed(simp)+

(*the intuition behind the compress_protocols*)
lemma "simple_proto_conjunct (Proto p1) (Proto p2) ≠ None ⟹ ∀pkt. match_proto (Proto p1) pkt ⟷ match_proto (Proto p2) pkt"
apply(subgoal_tac "p1 = p2")
apply(simp)
apply(simp split: if_split_asm)
done
lemma "simple_proto_conjunct p1 (Proto p2) ≠ None ⟹ ∀pkt. match_proto (Proto p2) pkt ⟶ match_proto p1 pkt"
apply(cases p1)
apply(simp)
apply(simp split: if_split_asm)
done

definition compress_protocols :: "protocol negation_type list ⇒ (protocol list × protocol list) option" where
"compress_protocols ps ≡ case (compress_pos_protocols (getPos ps))
of None ⇒ None
|  Some proto ⇒ if ProtoAny ∈ set (getNeg ps) ∨ (∀p ∈ {0..- 1}. Proto p ∈ set (getNeg ps)) then
None
else if proto = ProtoAny then
Some ([], getNeg ps)
else if (∃p ∈ set (getNeg ps). simple_proto_conjunct proto p ≠ None) then
None
else
― ‹‹proto› is a ‹primitive_protocol› here. This is strict equality match, e.g.›
― ‹protocol must be TCP. Thus, we can remove all negative matches!›
Some ([proto], [])"

(* It is kind of messy to find a definition that checks whether a match is the exhaustive list
and is executable *)
lemma all_proto_hlp2: "ProtoAny ∈ a ∨ (∀p ∈ {0..- 1}. Proto p ∈ a) ⟷
ProtoAny ∈ a ∨ a = {p. p ≠ ProtoAny}"
proof -
have all_proto_hlp: "ProtoAny ∉ a ⟹ (∀p ∈ {0..- 1}. Proto p ∈ a) ⟷ a = {p. p ≠ ProtoAny}"
by(auto intro: protocol.exhaust)
thus ?thesis by blast
qed

lemma set_word8_word_upto: "{0..(- 1 :: 8 word)} = set (word_upto 0 255)"
proof -
have ‹0xFF = (- 1 :: 8 word)›
by simp
then show ?thesis
by (simp only:) (auto simp add: word_upto_set_eq)
qed
lemma "(∀p ∈ {0..- 1}. Proto p ∈ set (getNeg ps)) ⟷
((∀p ∈ set (word_upto 0 255). Proto p ∈ set (getNeg ps)))"

lemma compress_protocols_code[code]:
"compress_protocols ps = (case (compress_pos_protocols (getPos ps))
of None ⇒ None
|  Some proto ⇒ if ProtoAny ∈ set (getNeg ps) ∨ (∀p ∈ set (word_upto 0 255). Proto p ∈ set (getNeg ps)) then
None
else if proto = ProtoAny then
Some ([], getNeg ps)
else if (∃p ∈ set (getNeg ps). simple_proto_conjunct proto p ≠ None) then
None
else
Some ([proto], [])
)"
unfolding compress_protocols_def
using set_word8_word_upto by presburger

(*fully optimized, i.e. we cannot compress it better*)
lemma "compress_protocols ps = Some (ps_pos, ps_neg) ⟹
∃ p. ((∀m∈set ps_pos. match_proto m p) ∧ (∀m∈set ps_neg. ¬ match_proto m p))"
apply(simp add: compress_protocols_def all_proto_hlp2 split: option.split_asm if_split_asm)
apply(subgoal_tac "∃p. (Proto p) ∉ set ps_neg")
apply(elim exE)
apply(rename_tac x2 p)
apply(rule_tac x=p in exI)
apply(blast elim: match_proto.elims)
apply(auto intro: protocol.exhaust)
done

definition compress_normalize_protocols_step :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr option" where
"compress_normalize_protocols_step m ≡ compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m"

lemma (in primitive_matcher_generic) compress_normalize_protocols_step_Some:
assumes "normalized_nnf_match m" and "compress_normalize_protocols_step m = Some m'"
shows "matches (β, α) m' a p ⟷ matches (β, α) m a p"
proof(rule compress_normalize_primitive_Some[OF assms(1) wf_disc_sel_common_primitive(7), of compress_protocols])
show "compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'"
next
fix ps ps_pos ps_neg
show "compress_protocols ps = Some (ps_pos, ps_neg) ⟹
matches (β, α) (alist_and (NegPos_map Prot ((map Pos ps_pos)@(map Neg ps_neg)))) a p ⟷
matches (β, α) (alist_and (NegPos_map Prot ps)) a p"
apply(case_tac "compress_pos_protocols (getPos ps)")
apply(simp_all)
apply(drule_tac p_prot="p_proto p" in compress_pos_protocols_Some)
apply(simp split:if_split_asm)
using simple_proto_conjunct_None by auto
qed

lemma (in primitive_matcher_generic) compress_normalize_protocols_step_None:
assumes "normalized_nnf_match m" and "compress_normalize_protocols_step m = None"
shows "¬ matches (β, α) m a p"
proof(rule compress_normalize_primitive_None[OF assms(1) wf_disc_sel_common_primitive(7), of "compress_protocols"])
show "compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = None"
next
fix ps
have if_option_Some:
"((if P then None else Some x) = Some y) = (¬P ∧ x = y)"
for P and x::protocol and y by simp
show "compress_protocols ps = None ⟹ ¬ matches (β, α) (alist_and (NegPos_map Prot ps)) a p"
apply(cases "compress_pos_protocols (getPos ps)")
apply(simp_all)
apply(drule_tac p_prot="p_proto p" in compress_pos_protocols_None)
apply(simp; fail)
apply(drule_tac p_prot="p_proto p" in compress_pos_protocols_Some)
apply(simp split:if_split_asm)
apply fastforce
apply(elim bexE exE)
apply(simp)
apply(elim simple_proto_conjunct.elims)
apply(simp; fail)
apply(simp; fail)
using if_option_Some by metis
qed

lemma compress_normalize_protocols_step_nnf:
"normalized_nnf_match m ⟹ compress_normalize_protocols_step m = Some m' ⟹
normalized_nnf_match m'"
unfolding compress_normalize_protocols_step_def
using compress_normalize_primitive_nnf[OF wf_disc_sel_common_primitive(7)] by blast

(*not needed, I want it to introduce prot when I import from L4Ports!*)
lemma compress_normalize_protocols_step_not_introduces_Prot:
"¬ has_disc is_Prot m ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols_step m = Some m' ⟹
¬ has_disc is_Prot m'"
apply(drule compress_normalize_primitive_not_introduces_C[where m=m and C'=Prot])
done

lemma compress_normalize_protocols_step_not_introduces_Prot_negated:
assumes notdisc: "¬ has_disc_negated is_Prot False m"
and nm: "normalized_nnf_match m"
and some: "compress_normalize_protocols_step m = Some m'"
shows "¬ has_disc_negated is_Prot False m'"
apply(rule compress_normalize_primitive_not_introduces_C_negated[OF notdisc wf_disc_sel_common_primitive(7) nm])
by(simp add: compress_protocols_def split: option.split_asm if_split_asm)

lemma compress_normalize_protocols_step_hasdisc:
"¬ has_disc disc m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols_step m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc disc m'"
unfolding compress_normalize_protocols_step_def
using compress_normalize_primitive_hasdisc[OF _ wf_disc_sel_common_primitive(7)] by blast

lemma compress_normalize_protocols_step_hasdisc_negated:
"¬ has_disc_negated disc neg m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols_step m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc_negated disc neg m'"
unfolding compress_normalize_protocols_step_def
using compress_normalize_primitive_hasdisc_negated[OF _ wf_disc_sel_common_primitive(7)] by blast

lemma compress_normalize_protocols_step_preserves_normalized_n_primitive:
"normalized_n_primitive (disc, sel) P m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols_step m = Some m' ⟹
normalized_nnf_match m' ∧ normalized_n_primitive (disc, sel) P m'"
unfolding compress_normalize_protocols_step_def
using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(7)] by blast

lemma "case compress_normalize_protocols_step
(MatchAnd (MatchAnd (MatchAnd (Match ((Prot (Proto TCP)):: 32 common_primitive)) (MatchNot (Match (Prot (Proto UDP))))) (Match (IIface (Iface ''eth1''))))
(Match (Prot (Proto TCP)))) of Some ps ⇒ opt_MatchAny_match_expr ps
= MatchAnd (Match (Prot (Proto 6))) (Match (IIface (Iface ''eth1'')))" by eval

value[code] "compress_normalize_protocols_step (MatchAny:: 32 common_primitive match_expr)"

subsection‹Importing the matches on @{typ primitive_protocol} from @{const L4Ports}›

(* add protocols from positive L4 ports into optimization. *)
definition import_protocols_from_ports
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"import_protocols_from_ports m ≡
(case primitive_extractor (is_Src_Ports, src_ports_sel) m of (srcpts, rst1) ⇒
case primitive_extractor (is_Dst_Ports, dst_ports_sel) rst1 of (dstpts, rst2) ⇒
MatchAnd
(MatchAnd
(MatchAnd
(andfold_MatchExp (map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) (getPos srcpts)))
(andfold_MatchExp (map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) (getPos dstpts)))
)
(alist_and' (NegPos_map Src_Ports srcpts @ NegPos_map Dst_Ports dstpts))
)
rst2
)"

text‹The @{const Proto} and @{const L4Ports} match make the following match impossible:›
lemma "compress_normalize_protocols_step (import_protocols_from_ports
(MatchAnd (MatchAnd (Match (Prot (Proto TCP):: 32 common_primitive))
(Match (Src_Ports (L4Ports UDP [(22,22)])))) (Match (IIface (Iface ''eth1''))))) = None"
by eval

(*unfolding the whole primitive_extractor*)
lemma import_protocols_from_ports_erule: "normalized_nnf_match m ⟹ P m ⟹
(⋀srcpts rst1 dstpts rst2.
normalized_nnf_match m ⟹
― ‹‹P m ⟹› erule consumes only first argument›
primitive_extractor (is_Src_Ports, src_ports_sel) m = (srcpts, rst1) ⟹
primitive_extractor (is_Dst_Ports, dst_ports_sel) rst1 = (dstpts, rst2) ⟹
normalized_nnf_match rst1 ⟹
normalized_nnf_match rst2 ⟹
P (MatchAnd
(MatchAnd
(MatchAnd
(andfold_MatchExp
(map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) (getPos srcpts)))
(andfold_MatchExp
(map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) (getPos dstpts))))
(alist_and' (NegPos_map Src_Ports srcpts @ NegPos_map Dst_Ports dstpts)))
rst2)) ⟹
P (import_protocols_from_ports m)"
apply(case_tac "primitive_extractor (is_Src_Ports, src_ports_sel) m", rename_tac srcpts rst1)
apply(simp)
apply(case_tac "primitive_extractor (is_Dst_Ports, dst_ports_sel) rst1", rename_tac dstpts rst2)
apply(simp)
apply(frule(1) primitive_extractor_correct(2)[OF _ wf_disc_sel_common_primitive(1)])
apply(frule(1) primitive_extractor_correct(2)[OF _ wf_disc_sel_common_primitive(2)])
apply simp
done

lemma (in primitive_matcher_generic) import_protocols_from_ports:
assumes normalized: "normalized_nnf_match m"
shows "matches (β, α) (import_protocols_from_ports m) a p ⟷ matches (β, α) m a p"
proof-
"matches (β, α)
(andfold_MatchExp (map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) (getPos as))) a p ∧
matches (β, α) (alist_and (NegPos_map C as)) a p
⟷
matches (β, α) (alist_and (NegPos_map C as)) a p"
if C: "C = Src_Ports ∨ C = Dst_Ports" for C as
proof(induction as)
case Nil thus ?case by(simp)
next
case (Cons x xs)
show ?case
proof(cases x)
case Neg with Cons.IH show ?thesis
by blast
next
case (Pos portmatch)
with Cons.IH show ?thesis
apply(cases portmatch)
using Ports_single_rewrite_Prot C by blast
qed
qed
from normalized show ?thesis
apply -
apply(erule import_protocols_from_ports_erule)
apply(simp; fail)
apply(subst primitive_extractor_correct(1)[OF normalized wf_disc_sel_common_primitive(1),
where γ="(β,α)" and a=a and p=p, symmetric])
apply(simp; fail)
apply(drule(1) primitive_extractor_correct(1)[OF _ wf_disc_sel_common_primitive(2),
where γ="(β,α)" and a=a and p=p])
qed

lemma import_protocols_from_ports_nnf:
"normalized_nnf_match m ⟹ normalized_nnf_match (import_protocols_from_ports m)"
proof -
have hlp: "∀m∈set (map (Match ∘ (Prot ∘ (case_ipt_l4_ports (λproto x. Proto proto)))) ls).
normalized_nnf_match m" for ls
apply(induction ls)
apply(simp)
apply(rename_tac l ls, case_tac l)
by(simp)
show "normalized_nnf_match m ⟹ normalized_nnf_match (import_protocols_from_ports m)"
apply(rule import_protocols_from_ports_erule)
apply(simp_all)
apply(safe)
done
qed

lemma import_protocols_from_ports_not_introduces_Prot_negated:
"normalized_nnf_match m ⟹ ¬ has_disc_negated is_Prot False m ⟹
¬ has_disc_negated is_Prot False (import_protocols_from_ports m)"
apply(erule(1) import_protocols_from_ports_erule)
apply(simp)
apply(intro conjI)
using andfold_MatchExp_not_disc_negated_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
using andfold_MatchExp_not_disc_negated_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
using not_has_disc_negated_NegPos_map[where disc=is_Prot and C=Src_Ports, simplified]
not_has_disc_negated_NegPos_map[where disc=is_Prot and C=Dst_Ports, simplified] apply blast
apply(drule(1) primitive_extractor_correct(6)[OF _ wf_disc_sel_common_primitive(1), where neg=False])
apply(drule(1) primitive_extractor_correct(6)[OF _ wf_disc_sel_common_primitive(2), where neg=False])
by blast

lemma import_protocols_from_ports_hasdisc:
"normalized_nnf_match m ⟹ ¬ has_disc disc m ⟹ (∀a. ¬ disc (Prot a)) ⟹
normalized_nnf_match (import_protocols_from_ports m) ∧ ¬ has_disc disc (import_protocols_from_ports m)"
apply(intro conjI)
using import_protocols_from_ports_nnf apply blast
apply(erule(1) import_protocols_from_ports_erule)
apply(simp)
apply(intro conjI)
using andfold_MatchExp_not_disc_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
using andfold_MatchExp_not_disc_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
subgoal for srcpts rst1 dstpts rst2
apply(frule(2) primitive_extractor_reassemble_not_has_disc[OF wf_disc_sel_common_primitive(1)])
apply(subgoal_tac "¬ has_disc disc rst1")
prefer 2
apply(drule(1) primitive_extractor_correct(4)[OF _ wf_disc_sel_common_primitive(1)])
apply blast
apply(drule(2) primitive_extractor_reassemble_not_has_disc[OF wf_disc_sel_common_primitive(2)])
using has_disc_alist_and'_append by blast
apply(drule(1) primitive_extractor_correct(4)[OF _ wf_disc_sel_common_primitive(1)])
apply(drule(1) primitive_extractor_correct(4)[OF _ wf_disc_sel_common_primitive(2)])
apply blast
done

lemma import_protocols_from_ports_hasdisc_negated:
"¬ has_disc_negated disc False m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹
normalized_nnf_match (import_protocols_from_ports m) ∧
¬ has_disc_negated disc False (import_protocols_from_ports m)"
apply(intro conjI)
using import_protocols_from_ports_nnf apply blast
apply(erule(1) import_protocols_from_ports_erule)
apply(simp)
apply(intro conjI)
using andfold_MatchExp_not_disc_negated_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
using andfold_MatchExp_not_disc_negated_mapMatch[
where C="Prot ∘ case_ipt_l4_ports (λproto x. Proto proto)", simplified] apply blast
subgoal for srcpts rst1 dstpts rst2
apply(frule(2) primitive_extractor_reassemble_not_has_disc_negated[OF wf_disc_sel_common_primitive(1)])
apply(subgoal_tac "¬ has_disc_negated disc False rst1")
prefer 2
apply(drule(1) primitive_extractor_correct(6)[OF _ wf_disc_sel_common_primitive(1)])
apply blast
apply(drule(2) primitive_extractor_reassemble_not_has_disc_negated[OF wf_disc_sel_common_primitive(2)])
using has_disc_negated_alist_and'_append by blast
apply(drule(1) primitive_extractor_correct(6)[OF _ wf_disc_sel_common_primitive(1)])
apply(drule(1) primitive_extractor_correct(6)[OF _ wf_disc_sel_common_primitive(2)])
apply blast
done

lemma import_protocols_from_ports_preserves_normalized_n_primitive:
"normalized_n_primitive (disc, sel) f m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹
normalized_nnf_match (import_protocols_from_ports m) ∧ normalized_n_primitive (disc, sel) f (import_protocols_from_ports m)"
apply(intro conjI)
using import_protocols_from_ports_nnf apply blast
apply(erule(1) import_protocols_from_ports_erule)
apply(simp)
apply(intro conjI)
subgoal for srcpts rst1 dstpts rst2
apply(rule andfold_MatchExp_normalized_n_primitive)
using normalized_n_primitive_impossible_map by blast
subgoal for srcpts rst1 dstpts rst2
apply(rule andfold_MatchExp_normalized_n_primitive)
using normalized_n_primitive_impossible_map by blast
subgoal for srcpts rst1 dstpts rst2
apply(frule(2) primitive_extractor_reassemble_normalized_n_primitive[OF wf_disc_sel_common_primitive(1)])
apply(subgoal_tac "normalized_n_primitive (disc, sel) f rst1")
prefer 2
apply(drule(1) primitive_extractor_correct(5)[OF _ wf_disc_sel_common_primitive(1)])
apply blast
apply(drule(2) primitive_extractor_reassemble_normalized_n_primitive[OF wf_disc_sel_common_primitive(2)])
using normalized_n_primitive_alist_and'_append by blast
apply(drule(1) primitive_extractor_correct(5)[OF _ wf_disc_sel_common_primitive(1)])
apply(drule(1) primitive_extractor_correct(5)[OF _ wf_disc_sel_common_primitive(2)])
apply blast
done

subsection‹Putting things together›

definition compress_normalize_protocols
:: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr option" where
"compress_normalize_protocols m ≡ compress_normalize_protocols_step (import_protocols_from_ports m)"

lemma (in primitive_matcher_generic) compress_normalize_protocols_Some:
assumes "normalized_nnf_match m" and "compress_normalize_protocols m = Some m'"
shows "matches (β, α) m' a p ⟷ matches (β, α) m a p"
by (metis import_protocols_from_ports import_protocols_from_ports_nnf
compress_normalize_protocols_step_Some)

lemma (in primitive_matcher_generic) compress_normalize_protocols_None:
assumes "normalized_nnf_match m" and "compress_normalize_protocols m = None"
shows "¬ matches (β, α) m a p"
by (metis import_protocols_from_ports import_protocols_from_ports_nnf
compress_normalize_protocols_step_None)

lemma compress_normalize_protocols_nnf:
"normalized_nnf_match m ⟹ compress_normalize_protocols m = Some m' ⟹
normalized_nnf_match m'"
by (metis import_protocols_from_ports_nnf compress_normalize_protocols_step_nnf)

lemma compress_normalize_protocols_not_introduces_Prot_negated:
assumes notdisc: "¬ has_disc_negated is_Prot False m"
and nm: "normalized_nnf_match m"
and some: "compress_normalize_protocols m = Some m'"
shows "¬ has_disc_negated is_Prot False m'"
using import_protocols_from_ports_nnf
import_protocols_from_ports_not_introduces_Prot_negated
compress_normalize_protocols_step_not_introduces_Prot_negated by auto

lemma compress_normalize_protocols_hasdisc:
"¬ has_disc disc m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc disc m'"
using import_protocols_from_ports_hasdisc
compress_normalize_protocols_step_hasdisc by blast

lemma compress_normalize_protocols_hasdisc_negated:
"¬ has_disc_negated disc False m ⟹ (∀a. ¬ disc (Prot a)) ⟹
normalized_nnf_match m ⟹ compress_normalize_protocols m = Some m' ⟹
normalized_nnf_match m' ∧ ¬ has_disc_negated disc False m'" (*original lemma allowed arbitrary neg*)
apply(frule(2) import_protocols_from_ports_hasdisc_negated)
using compress_normalize_protocols_step_hasdisc_negated by blast

lemma compress_normalize_protocols_preserves_normalized_n_primitive:
"normalized_n_primitive (disc, sel) P m ⟹ (∀a. ¬ disc (Prot a)) ⟹ normalized_nnf_match m ⟹ compress_normalize_protocols m = Some m' ⟹
normalized_nnf_match m' ∧ normalized_n_primitive (disc, sel) P m'"
using import_protocols_from_ports_preserves_normalized_n_primitive
compress_normalize_protocols_step_preserves_normalized_n_primitive by blast

lemma "case compress_normalize_protocols
(MatchAnd (MatchAnd (MatchAnd (Match ((Prot (Proto TCP)):: 32 common_primitive)) (MatchNot (Match (Prot (Proto UDP))))) (Match (IIface (Iface ''eth1''))))
(Match (Prot (Proto TCP)))) of Some ps ⇒ opt_MatchAny_match_expr ps
=
MatchAnd (Match (Prot (Proto 6))) (Match (IIface (Iface ''eth1'')))" by eval

(*too many MatchAny!*)
value[code] "compress_normalize_protocols (MatchAny:: 32 common_primitive match_expr)"

end
```