Theory IpRoute_Parser

section Parser
theory IpRoute_Parser
imports Routing_Table 
  IP_Addresses.IP_Address_Parser
keywords "parse_ip_route" "parse_ip_6_route" :: thy_decl
begin
text‹This helps to read the output of the \texttt{ip route} command into a @{typ "32 routing_rule list"}.›

definition empty_rr_hlp :: "('a::len) prefix_match ⇒ 'a routing_rule" where
  "empty_rr_hlp pm = routing_rule.make pm default_metric (routing_action.make '''' None)"

lemma empty_rr_hlp_alt:
  "empty_rr_hlp pm = ⦇ routing_match = pm, metric = 0, routing_action = ⦇output_iface = [], next_hop = None⦈⦈"
  unfolding empty_rr_hlp_def routing_rule.defs default_metric_def routing_action.defs ..

definition routing_action_next_hop_update :: "'a word ⇒ 'a routing_rule ⇒ ('a::len) routing_rule"
  where
  "routing_action_next_hop_update h pk = pk⦇ routing_action := (routing_action pk)⦇ next_hop := Some h⦈ ⦈"
lemma "routing_action_next_hop_update h pk = routing_action_update (next_hop_update (λ_. (Some h))) (pk::32 routing_rule)"
  by(simp add: routing_action_next_hop_update_def)

definition routing_action_oiface_update :: "string ⇒ 'a routing_rule ⇒ ('a::len) routing_rule"
  where
  "routing_action_oiface_update h pk = routing_action_update (output_iface_update (λ_. h)) (pk::'a routing_rule)"
lemma "routing_action_oiface_update h pk = pk⦇ routing_action := (routing_action pk)⦇ output_iface :=  h⦈ ⦈"
  by(simp add: routing_action_oiface_update_def)

(* Could be moved to Bitmagic *)
definition "default_prefix = PrefixMatch 0 0"
lemma default_prefix_matchall: "prefix_match_semantics default_prefix ip"
  unfolding default_prefix_def by (simp add: valid_prefix_00 zero_prefix_match_all)

definition "sanity_ip_route (r::('a::len) prefix_routing) ≡ correct_routing r ∧ unambiguous_routing r ∧ list_all ((≠) '''' ∘ routing_oiface) r"
text‹The parser ensures that @{const sanity_ip_route} holds for any ruleset that is imported.›

(* Hide all the ugly ml in a file with the right extension *)
(*Depends on the function parser_ipv4 from IP_Address_Parser*)
ML_file ‹IpRoute_Parser.ML›
                  
ML‹
  Outer_Syntax.local_theory @{command_keyword parse_ip_route}
  "Load a file generated by ip route and make the routing table definition available as isabelle term"
  (Parse.binding --| @{keyword "="} -- Parse.string >> register_ip_route 32)
›

ML‹
  Outer_Syntax.local_theory @{command_keyword parse_ip_6_route}
  "Load a file generated by ip -6 route and make the routing table definition available as isabelle term"
  (Parse.binding --| @{keyword "="} -- Parse.string >> register_ip_route 128)
›

parse_ip_route "rtbl_parser_test1" = "ip-route-ex"
lemma  "sanity_ip_route rtbl_parser_test1" by eval (* checked by parse_ip_route alread *)

lemma "rtbl_parser_test1 =
  [⦇routing_match = PrefixMatch 0xFFFFFF00 32, metric = 0, routing_action = ⦇output_iface = ''tun0'', next_hop = None⦈⦈,
  ⦇routing_match = PrefixMatch 0xA0D2AA0 28, metric = 303, routing_action = ⦇output_iface = ''ewlan'', next_hop = None⦈⦈,
  ⦇routing_match = PrefixMatch 0xA0D2500 24, metric = 0, routing_action = ⦇output_iface = ''tun0'', next_hop = Some 0xFFFFFF00⦈⦈,
  ⦇routing_match = PrefixMatch 0xA0D2C00 24, metric = 0, routing_action = ⦇output_iface = ''tun0'', next_hop = Some 0xFFFFFF00⦈⦈,
  ⦇routing_match = PrefixMatch 0 0, metric = 303, routing_action = ⦇output_iface = ''ewlan'', next_hop = Some 0xA0D2AA1⦈⦈]"
by eval

parse_ip_6_route "rtbl_parser_test2" = "ip-6-route-ex"
value[code] rtbl_parser_test2
lemma  "sanity_ip_route rtbl_parser_test2" by eval

end