Theory Routing_IpAssmt

section‹Routing and IP Assignments›
theory Routing_IpAssmt
imports Ipassmt
        Routing.Routing_Table
begin
context
begin

subsection‹Routing IP Assignment›
text‹Up to now, the definitions were all still on word intervals because those are much more convenient to work with.›

definition routing_ipassmt :: "'i::len routing_rule list ⇒ (iface × ('i word × nat) list) list"
  where
  "routing_ipassmt rt ≡ map (apfst Iface ∘ apsnd cidr_split) (routing_ipassmt_wi rt)"

private lemma ipcidr_union_cidr_split[simp]: "ipcidr_union_set (set (cidr_split x)) = wordinterval_to_set x" 
  apply(subst cidr_split_prefix[symmetric])
  apply(fact ipcidr_union_set_uncurry)
done

private lemma map_of_map_Iface: "map_of (map (λx. (Iface (fst x), f (snd x))) xs) (Iface ifce) = 
        map_option f ((map_of xs) ifce)"
  by (induct xs) (auto)

lemma "routing_ipassmt_wi ([]::32 prefix_routing) = [(output_iface (routing_action (undefined :: 32 routing_rule)), WordInterval 0 0xFFFFFFFF)]"
  by code_simp


lemma routing_ipassmt: "
    valid_prefixes rt ⟹
    output_iface (routing_table_semantics rt (p_dst p)) = p_oiface p ⟹
    ∃p_ips. map_of (routing_ipassmt rt) (Iface (p_oiface p)) = Some p_ips ∧ p_dst p ∈ ipcidr_union_set (set p_ips)"
  apply(simp add: routing_ipassmt_def)
  apply(drule routing_ipassmt_wi[where output_port="p_oiface p" and k="p_dst p"])
  apply(simp)
  apply(elim exE, rename_tac ip_range)
  apply(rule_tac x="cidr_split ip_range" in exI)
  apply(simp)
  apply(simp add: comp_def)
  apply(simp add: map_of_map_Iface)
  apply(rule_tac x="ip_range" in exI)
  apply(simp)
  by (simp add: routing_ipassmt_wi_distinct)

lemma routing_ipassmt_ipassmt_sanity_disjoint: "valid_prefixes (rt::('i::len) prefix_routing) ⟹
    ipassmt_sanity_disjoint (map_of (routing_ipassmt rt))"
unfolding ipassmt_sanity_disjoint_def routing_ipassmt_def comp_def
  apply(clarsimp)
  apply(drule map_of_SomeD)+
  apply(clarsimp split: iface.splits)
using routing_ipassmt_wi_disjoint[where 'i = 'i] by meson

lemma routing_ipassmt_distinct: "distinct (map fst (routing_ipassmt rtbl))"
  using routing_ipassmt_wi_distinct[of rtbl]
  unfolding routing_ipassmt_def
  apply(simp add: comp_def)
  apply(subst distinct_map[where f = Iface and xs = "map fst (routing_ipassmt_wi rtbl)", simplified, unfolded comp_def])
  apply(auto intro: inj_onI)
done
  
end

end