Theory Output_Interface_Replace
theory Output_Interface_Replace
imports
Ipassmt
Routing_IpAssmt
Common_Primitive_toString
begin
section‹Replacing output interfaces by their IP ranges according to Routing›
text‹Copy of @{file ‹Interface_Replace.thy›}›
definition ipassmt_iface_replace_dstip_mexpr
:: "'i::len ipassignment ⇒ iface ⇒ 'i common_primitive match_expr" where
"ipassmt_iface_replace_dstip_mexpr ipassmt ifce ≡ case ipassmt ifce of
None ⇒ Match (OIface ifce)
| Some ips ⇒ (match_list_to_match_expr (map (Match ∘ Dst) (map (uncurry IpAddrNetmask) ips)))"
lemma matches_ipassmt_iface_replace_dstip_mexpr:
"matches (common_matcher, α) (ipassmt_iface_replace_dstip_mexpr ipassmt ifce) a p ⟷ (case ipassmt ifce of
None ⇒ match_iface ifce (p_oiface p)
| Some ips ⇒ p_dst p ∈ ipcidr_union_set (set ips)
)"
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: ipassmt_iface_replace_dstip_mexpr_def primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
next
case (Some ips)
have "matches (common_matcher, α) (match_list_to_match_expr (map (Match ∘ Dst ∘ (uncurry IpAddrNetmask)) ips)) a p ⟷
(∃m∈set ips. p_dst p ∈ (uncurry ipset_from_cidr m))"
by(simp add: match_list_to_match_expr_disjunction[symmetric]
match_list_matches match_simplematcher_SrcDst ipt_iprange_to_set_uncurry_IpAddrNetmask)
with Some show ?thesis
by(simp add: ipassmt_iface_replace_dstip_mexpr_def bunch_of_lemmata_about_matches ipcidr_union_set_uncurry)
qed
fun oiface_rewrite
:: "'i::len ipassignment ⇒ 'i common_primitive match_expr ⇒ 'i common_primitive match_expr"
where
"oiface_rewrite _ MatchAny = MatchAny" |
"oiface_rewrite ipassmt (Match (OIface ifce)) = ipassmt_iface_replace_dstip_mexpr ipassmt ifce" |
"oiface_rewrite _ (Match a) = Match a" |
"oiface_rewrite ipassmt (MatchNot m) = MatchNot (oiface_rewrite ipassmt m)" |
"oiface_rewrite ipassmt (MatchAnd m1 m2) = MatchAnd (oiface_rewrite ipassmt m1) (oiface_rewrite ipassmt m2)"
context
begin
private lemma oiface_rewrite_matches_Primitive:
"matches (common_matcher, α) (MatchNot (oiface_rewrite ipassmt (Match x))) a p = matches (common_matcher, α) (MatchNot (Match x)) a p ⟷
matches (common_matcher, α) (oiface_rewrite ipassmt (Match x)) a p = matches (common_matcher, α) (Match x) a p"
proof(cases x)
case (OIface ifce)
have "(matches (common_matcher, α) (MatchNot (ipassmt_iface_replace_dstip_mexpr ipassmt ifce)) a p = (¬ match_iface ifce (p_oiface p))) ⟷
(matches (common_matcher, α) (ipassmt_iface_replace_dstip_mexpr ipassmt ifce) a p = match_iface ifce (p_oiface p))"
proof(cases "ipassmt ifce")
case None thus ?thesis
apply(simp add: matches_ipassmt_iface_replace_dstip_mexpr)
apply(simp add: ipassmt_iface_replace_dstip_mexpr_def primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
done
next
case (Some ips)
{ fix ips
have "matches (common_matcher, α)
(MatchNot (match_list_to_match_expr (map (Match ∘ Dst ∘ (uncurry IpAddrNetmask)) ips))) a p ⟷
(p_dst p ∉ ipcidr_union_set (set ips))"
apply(induction ips)
apply(simp add: bunch_of_lemmata_about_matches ipcidr_union_set_uncurry)
apply(simp add: MatchOr_MatchNot)
apply(simp add: ipcidr_union_set_uncurry)
apply(simp add: match_simplematcher_SrcDst_not)
apply(thin_tac _)
apply(simp add: ipt_iprange_to_set_uncurry_IpAddrNetmask)
done
} note helper=this
from Some show ?thesis
apply(simp add: matches_ipassmt_iface_replace_dstip_mexpr)
apply(simp add: ipassmt_iface_replace_dstip_mexpr_def)
apply(simp add: helper)
done
qed
with OIface show ?thesis
by(simp add: primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed(simp_all)
lemma ipassmt_disjoint_matcheq_iifce_dstip:
assumes ipassmt_nowild: "ipassmt_sanity_nowildcards ipassmt"
and ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
and ifce: "ipassmt ifce = Some i_ips"
and p_ifce: "ipassmt (Iface (p_oiface p)) = Some p_ips ∧ p_dst p ∈ ipcidr_union_set (set p_ips)"
shows "match_iface ifce (p_oiface p) ⟷ p_dst p ∈ ipcidr_union_set (set i_ips)"
proof
assume "match_iface ifce (p_oiface p)"
thus "p_dst p ∈ ipcidr_union_set (set i_ips)"
apply(cases "ifce = Iface (p_oiface p)")
using ifce p_ifce apply force
by (metis domI iface.sel iface_is_wildcard_def ifce ipassmt_nowild ipassmt_sanity_nowildcards_def match_iface.elims(2) match_iface_case_nowildcard)
next
assume a: "p_dst p ∈ ipcidr_union_set (set i_ips)"
from ipassmt_disjoint_nonempty_inj[OF ipassmt_disjoint ifce] a have ipassmt_inj: "∀k. ipassmt k = Some i_ips ⟶ k = ifce" by blast
from ipassmt_disjoint_inj_k[OF ipassmt_disjoint ifce _ a] have ipassmt_inj_k:
"⋀k ips'. ipassmt k = Some ips' ⟹ p_dst p ∈ ipcidr_union_set (set ips') ⟹ k = ifce" by simp
have ipassmt_inj_p: "∀ips'. p_dst p ∈ ipcidr_union_set (set ips') ∧ (∃k. ipassmt k = Some ips') ⟶ ips' = i_ips"
proof(intro allI impI; elim conjE exE)
fix ips' k
assume as: "p_dst p ∈ ipcidr_union_set (set ips')" "ipassmt k = Some ips'"
hence "k = ifce" using ipassmt_inj_k by simp
thus "ips' = i_ips" using ifce as by simp
qed
from p_ifce have "(Iface (p_oiface p)) = ifce" using ipassmt_inj_p ipassmt_inj by blast
thus "match_iface ifce (p_oiface p)" using match_iface_refl by blast
qed
private lemma matches_ipassmt_iface_replace_dstip_mexpr_case_Iface:
fixes ifce::iface
assumes "ipassmt_sanity_nowildcards ipassmt"
and "ipassmt_sanity_disjoint ipassmt"
and "ipassmt (Iface (p_oiface p)) = Some p_ips ∧ p_dst p ∈ ipcidr_union_set (set p_ips)"
shows "matches (common_matcher, α) (ipassmt_iface_replace_dstip_mexpr ipassmt ifce) a p ⟷
matches (common_matcher, α) (Match (OIface ifce)) a p"
proof -
have "matches (common_matcher, α) (ipassmt_iface_replace_dstip_mexpr ipassmt ifce) a p = match_iface ifce (p_oiface p)"
proof -
show ?thesis
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: matches_ipassmt_iface_replace_dstip_mexpr)
next
case (Some y) with assms(2) have "p_dst p ∈ ipcidr_union_set (set y) = match_iface ifce (p_oiface p)"
using assms(1) assms(3) ipassmt_disjoint_matcheq_iifce_dstip by blast
with Some show ?thesis by(simp add: matches_ipassmt_iface_replace_dstip_mexpr)
qed
qed
thus ?thesis by(simp add: primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed
lemma matches_oiface_rewrite_ipassmt:
"normalized_nnf_match m ⟹ ipassmt_sanity_nowildcards ipassmt ⟹ ipassmt_sanity_disjoint ipassmt ⟹
(∃p_ips. ipassmt (Iface (p_oiface p)) = Some p_ips ∧ p_dst p ∈ ipcidr_union_set (set p_ips)) ⟹
matches (common_matcher, α) (oiface_rewrite ipassmt m) a p ⟷ matches (common_matcher, α) m a p"
proof(induction m)
case MatchAny thus ?case by simp
next
case (MatchNot m)
hence IH: "normalized_nnf_match m ⟹
matches (common_matcher, α) (oiface_rewrite ipassmt m) a p =matches (common_matcher, α) m a p" by blast
with MatchNot.prems IH show ?case by(induction m) (simp_all add: oiface_rewrite_matches_Primitive)
next
case(Match x) thus ?case
proof(cases x)
case (OIface ifce) with Match show ?thesis
apply(cases "ipassmt (Iface (p_oiface p))")
prefer 2
apply(simp add: matches_ipassmt_iface_replace_dstip_mexpr_case_Iface; fail)
by auto
qed(simp_all)
next
case (MatchAnd m1 m2) thus ?case by(simp add: bunch_of_lemmata_about_matches)
qed
lemma matches_oiface_rewrite:
"normalized_nnf_match m ⟹ ipassmt_sanity_nowildcards ipassmt ⟹
correct_routing rt ⟹
ipassmt = map_of (routing_ipassmt rt) ⟹
output_iface (routing_table_semantics rt (p_dst p)) = p_oiface p ⟹
matches (common_matcher, α) (oiface_rewrite ipassmt m) a p ⟷ matches (common_matcher, α) m a p"
apply(rule matches_oiface_rewrite_ipassmt; assumption?)
apply(simp add: correct_routing_def routing_ipassmt_ipassmt_sanity_disjoint; fail)
apply(simp)
apply(rule routing_ipassmt; assumption?)
apply(simp add: correct_routing_def; fail)
done
end
lemma oiface_rewrite_preserves_nodisc:
"∀a. ¬ disc (Dst a) ⟹ ¬ has_disc disc m ⟹ ¬ has_disc disc (oiface_rewrite ipassmt m)"
proof(induction ipassmt m rule: oiface_rewrite.induct)
case 2
have "∀a. ¬ disc (Dst a) ⟹ ¬ disc (OIface ifce) ⟹ ¬ has_disc disc (ipassmt_iface_replace_dstip_mexpr ipassmt ifce)"
for ifce ipassmt
apply(simp add: ipassmt_iface_replace_dstip_mexpr_def split: option.split)
apply(intro allI impI, rename_tac ips)
apply(drule_tac X=Dst and ls="map (uncurry IpAddrNetmask) ips" in match_list_to_match_expr_not_has_disc)
apply(simp)
done
with 2 show ?case by simp
qed(simp_all)
end