SSL IpRoute_Parser.thy

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