Session Routing

Theory Linorder_Helper

text_raw‹\section*{Sorting a list by two keys}›
theory Linorder_Helper
imports Main
begin

text‹Sorting is fun...›

text‹The problem is that Isabelle does not have anything like \texttt{sortBy}, only @{const sort_key}.
This means that there is no way to sort something based on two properties, with one being infinitely more important.›

text‹Enter this:›

datatype ('a,'b) linord_helper = LinordHelper 'a 'b

instantiation linord_helper :: (linorder, linorder) linorder
begin                                  
  definition "linord_helper_less_eq1 a b  (case a of LinordHelper a1 a2  case b of LinordHelper b1 b2  a1 < b1  a1 = b1  a2  b2)"
	definition "a  b  linord_helper_less_eq1 a b"
	definition "a < b  (a  b  linord_helper_less_eq1 a b)"
instance
by standard (auto simp: linord_helper_less_eq1_def less_eq_linord_helper_def less_linord_helper_def split: linord_helper.splits)
end
lemmas linord_helper_less = less_linord_helper_def linord_helper_less_eq1_def
lemmas linord_helper_le = less_eq_linord_helper_def linord_helper_less_eq1_def

text‹Now, it is possible to use @{term "sort_key f"}, 
with @{term f} constructing a @{const LinordHelper} containing the two desired properties for sorting.›

end

Theory Routing_Table

section‹Routing Table›
theory Routing_Table
imports IP_Addresses.Prefix_Match
        IP_Addresses.IPv4 IP_Addresses.IPv6
        Linorder_Helper
        IP_Addresses.Prefix_Match_toString
begin

text‹This section makes the necessary definitions to work with a routing table using longest prefix matching.›
subsection‹Definition›

record(overloaded) 'i routing_action = 
  output_iface :: string
  next_hop :: "'i word option" (* no next hop iff locally attached *)

(* Routing rule matching ip route unicast type *)
record(overloaded) 'i routing_rule =
  routing_match :: "('i::len) prefix_match" (* done on the dst *)
  metric :: nat
  routing_action :: "'i routing_action"

text‹This definition is engineered to model routing tables on packet forwarding devices.
It eludes, e.g., the source address hint, which is only relevant for packets originating from the device itself.›
(* See also: http://linux-ip.net/html/routing-saddr-selection.html *)

context
begin

definition "default_metric = 0"

type_synonym 'i prefix_routing = "('i routing_rule) list"

abbreviation "routing_oiface a  output_iface (routing_action a)" (* I needed this a lot... *)
abbreviation "routing_prefix r  pfxm_length (routing_match r)"

definition valid_prefixes where
  "valid_prefixes r = foldr conj (map (λrr. valid_prefix (routing_match rr)) r) True"
lemma valid_prefixes_split: "valid_prefixes (r#rs)  valid_prefix (routing_match r)  valid_prefixes rs"
  using valid_prefixes_def by force

lemma foldr_True_set: "foldr (λx. (∧) (f x)) l True = (x  set l. f x)"
  by (induction l) simp_all
lemma valid_prefixes_alt_def: "valid_prefixes r = (e  set r. valid_prefix (routing_match e))"
  unfolding valid_prefixes_def
  unfolding foldr_map
  unfolding comp_def
  unfolding foldr_True_set
  ..
  
fun has_default_route :: "('i::len) prefix_routing  bool" where
"has_default_route (r#rs) = (((pfxm_length (routing_match r)) = 0)  has_default_route rs)" |
"has_default_route Nil = False"

lemma has_default_route_alt: "has_default_route rt  (r  set rt. pfxm_length (routing_match r) = 0)" by(induction rt) simp_all

subsection‹Single Packet Semantics›

fun routing_table_semantics :: "('i::len) prefix_routing  'i word  'i routing_action" where
"routing_table_semantics [] _ = routing_action (undefined::'i routing_rule)" | 
"routing_table_semantics (r#rs) p = (if prefix_match_semantics (routing_match r) p then routing_action r else routing_table_semantics rs p)"
lemma routing_table_semantics_ports_from_table: "valid_prefixes rtbl  has_default_route rtbl  
  routing_table_semantics rtbl packet = r  r  routing_action ` set rtbl"
proof(induction rtbl)
  case (Cons r rs)
  note v_pfxs = valid_prefixes_split[OF Cons.prems(1)]
  show ?case
  proof(cases "pfxm_length (routing_match r) = 0")
    case True                                                 
    note zero_prefix_match_all[OF conjunct1[OF v_pfxs] True] Cons.prems(3)
    then show ?thesis by simp
  next
    case False
    hence "has_default_route rs" using Cons.prems(2) by simp
    from Cons.IH[OF conjunct2[OF v_pfxs] this] Cons.prems(3) show ?thesis by force
  qed
qed simp

subsection‹Longest Prefix Match›

text‹We can abuse @{const LinordHelper} to sort.›
definition "routing_rule_sort_key  λr. LinordHelper (0 - (of_nat :: nat  int) (pfxm_length (routing_match r))) (metric r)"
text‹There is actually a slight design choice here. We can choose to sort based on @{thm less_eq_prefix_match_def} (thus including the address) or only the prefix length (excluding it).
  Which is taken does not matter gravely, since the bits of the prefix can't matter. They're either eqal or the rules don't overlap and the metric decides. (It does matter for the resulting list though.)
  Ignoring the prefix and taking only its length is slightly easier.›

(*example: get longest prefix match by sorting by pfxm_length*)
definition "rr_ctor m l a nh me   routing_match = PrefixMatch (ipv4addr_of_dotdecimal m) l, metric = me, routing_action =output_iface = a, next_hop = (map_option ipv4addr_of_dotdecimal nh) "
value "sort_key routing_rule_sort_key [
  rr_ctor (0,0,0,1) 3 '''' None 0,
  rr_ctor (0,0,0,2) 8 [] None 0,
  rr_ctor (0,0,0,3) 4 [] None 13,
  rr_ctor (0,0,0,3) 4 [] None 42]"

definition "is_longest_prefix_routing  sorted  map routing_rule_sort_key"

definition correct_routing :: "('i::len) prefix_routing  bool" where 
  "correct_routing r  is_longest_prefix_routing r  valid_prefixes r"
text‹Many proofs and functions around routing require at least parts of @{const correct_routing} as an assumption.
Obviously, @{const correct_routing} is not given for arbitrary routing tables. Therefore,
@{const correct_routing} is made to be executable and should be checked for any routing table after parsing.
Note: @{const correct_routing} used to also require @{const has_default_route},
but none of the proofs require it anymore and it is not given for any routing table.›

lemma is_longest_prefix_routing_rule_exclusion:
  assumes "is_longest_prefix_routing (r1 # rn # rss)"
  shows "is_longest_prefix_routing (r1 # rss)"
using assms by(case_tac rss) (auto simp add: is_longest_prefix_routing_def)

lemma int_of_nat_less: "int_of_nat a < int_of_nat b  a < b" by (simp add: int_of_nat_def)

lemma is_longest_prefix_routing_sorted_by_length:
  assumes "is_longest_prefix_routing r"
     and "r = r1 # rs @ r2 # rss"
  shows "(pfxm_length (routing_match r1)  pfxm_length (routing_match r2))"
using assms
proof(induction rs arbitrary: r)
  case (Cons rn rs)
  let ?ro = "r1 # rs @ r2 # rss"
  have "is_longest_prefix_routing ?ro" using Cons.prems is_longest_prefix_routing_rule_exclusion[of r1 rn "rs @ r2 # rss"] by simp
  from Cons.IH[OF this] show ?case by simp
next
  case Nil thus ?case by(auto simp add: is_longest_prefix_routing_def routing_rule_sort_key_def linord_helper_less_eq1_def less_eq_linord_helper_def int_of_nat_def)    
qed

definition "sort_rtbl :: ('i::len) routing_rule list  'i routing_rule list  sort_key routing_rule_sort_key"

lemma is_longest_prefix_routing_sort: "is_longest_prefix_routing (sort_rtbl r)" unfolding sort_rtbl_def is_longest_prefix_routing_def by simp

definition "unambiguous_routing rtbl  (rt1 rt2 rr ra. rtbl = rt1 @ rr # rt2  ra  set (rt1 @ rt2)  routing_match rr = routing_match ra  routing_rule_sort_key rr  routing_rule_sort_key ra)"
lemma unambiguous_routing_Cons: "unambiguous_routing (r # rtbl)  unambiguous_routing rtbl"
  unfolding unambiguous_routing_def by(clarsimp) (metis append_Cons in_set_conv_decomp)
lemma "unambiguous_routing (rr # rtbl)  is_longest_prefix_routing (rr # rtbl)  ra  set rtbl  routing_match rr = routing_match ra  routing_rule_sort_key rr < routing_rule_sort_key ra"
  unfolding is_longest_prefix_routing_def unambiguous_routing_def by(fastforce)
primrec unambiguous_routing_code where
"unambiguous_routing_code [] = True" |
"unambiguous_routing_code (rr#rtbl) = (list_all (λra. routing_match rr  routing_match ra  routing_rule_sort_key rr  routing_rule_sort_key ra) rtbl  unambiguous_routing_code rtbl)"
lemma unambiguous_routing_code[code_unfold]: "unambiguous_routing rtbl  unambiguous_routing_code rtbl"
proof(induction rtbl)
  case (Cons rr rtbl) show ?case (is "?l  ?r") proof
    assume l: ?l
    with unambiguous_routing_Cons Cons.IH have "unambiguous_routing_code rtbl" by blast
    moreover have "list_all (λra. routing_match rr  routing_match ra  routing_rule_sort_key rr  routing_rule_sort_key ra) rtbl"
      using l unfolding unambiguous_routing_def by(fastforce simp add: list_all_iff)
    ultimately show ?r by simp
  next
    assume r: ?r
    with Cons.IH have "unambiguous_routing rtbl" by simp
    from r have *: "list_all (λra. routing_match rr  routing_match ra   routing_rule_sort_key rr  routing_rule_sort_key ra) rtbl" by simp
    have False if "rr # rtbl = rt1 @ rra # rt2" "ra  set (rt1 @ rt2)" "routing_rule_sort_key rra = routing_rule_sort_key ra  routing_match rra = routing_match ra" for rt1 rt2 rra ra
    proof(cases "rt1 = []")
      case True thus ?thesis using that * by(fastforce simp add: list_all_iff)
    next
      case False
      with that(1) have rtbl: "rtbl = tl rt1 @ rra # rt2" by (metis list.sel(3) tl_append2)
      show ?thesis proof(cases "ra = hd rt1") (* meh case split… *)
        case False hence "ra  set (tl rt1 @ rt2)" using that by(cases rt1; simp)
        with ‹unambiguous_routing rtbl show ?thesis  using that(3) rtbl unfolding unambiguous_routing_def by fast
      next
        case True hence "rr = ra" using that rt1  [] by(cases rt1; simp) 
        thus ?thesis using that * unfolding rtbl by(fastforce simp add: list_all_iff)
      qed
    qed
    thus ?l unfolding unambiguous_routing_def by blast 
  qed
qed(simp add: unambiguous_routing_def)

lemma unambigous_prefix_routing_weak_mono:
  assumes lpfx: "is_longest_prefix_routing (rr#rtbl)"
  assumes e:"rr'  set rtbl"
  shows "routing_rule_sort_key rr'  routing_rule_sort_key rr"
using assms  by(simp add: is_longest_prefix_routing_def)
lemma unambigous_prefix_routing_strong_mono:
  assumes lpfx: "is_longest_prefix_routing (rr#rtbl)" 
  assumes uam: "unambiguous_routing (rr#rtbl)" 
  assumes e:"rr'  set rtbl"
  assumes ne: "routing_match rr' = routing_match rr"
  shows "routing_rule_sort_key rr' > routing_rule_sort_key rr" 
proof -
  from uam e ne have "routing_rule_sort_key rr  routing_rule_sort_key rr'" by(fastforce simp add: unambiguous_routing_def)
  moreover from unambigous_prefix_routing_weak_mono lpfx e have "routing_rule_sort_key rr  routing_rule_sort_key rr'" .
  ultimately show ?thesis by simp
qed

lemma "routing_rule_sort_key (rr_ctor (0,0,0,0) 8 [] None 0) > routing_rule_sort_key (rr_ctor (0,0,0,0) 24 [] None 0)" by eval
(* get the inequality right… bigger means lower priority *)
text‹In case you don't like that formulation of @{const is_longest_prefix_routing} over sorting, this is your lemma.›
theorem existential_routing: "valid_prefixes rtbl  is_longest_prefix_routing rtbl  has_default_route rtbl  unambiguous_routing rtbl 
routing_table_semantics rtbl addr = act  (rr  set rtbl. prefix_match_semantics (routing_match rr) addr  routing_action rr = act 
  (ra  set rtbl. routing_rule_sort_key ra < routing_rule_sort_key rr  ¬prefix_match_semantics (routing_match ra) addr))"
proof(induction rtbl)
  case Nil thus ?case by simp
next
  case (Cons rr rtbl)
  show ?case proof(cases "prefix_match_semantics (routing_match rr) addr")
    case False
    hence [simp]: "routing_table_semantics (rr # rtbl) addr = routing_table_semantics (rr # rtbl) addr" by simp
    show ?thesis proof(cases "routing_prefix rr = 0")
      case True text‹Need special treatment, rtbl won't have a default route, so the IH is not usable.›
      have "valid_prefix (routing_match rr)" using Cons.prems valid_prefixes_split by blast
      with True False have False using zero_prefix_match_all by blast
      thus ?thesis ..
    next
      case False
      with Cons.prems have mprems: "valid_prefixes rtbl" "is_longest_prefix_routing rtbl" "has_default_route rtbl" "unambiguous_routing rtbl" 
        by(simp_all add: valid_prefixes_split unambiguous_routing_Cons is_longest_prefix_routing_def)
      show ?thesis using Cons.IH[OF mprems] False ¬ prefix_match_semantics (routing_match rr) addr by simp
    qed
  next
    case True
    from True have [simp]: "routing_table_semantics (rr # rtbl) addr = routing_action rr" by simp
    show ?thesis (is "?l  ?r") proof
      assume ?l
      hence [simp]: "act = routing_action rr" by(simp add: True)
      have *: "(raset (rr # rtbl). routing_rule_sort_key rr  routing_rule_sort_key ra)"
        using ‹is_longest_prefix_routing (rr # rtbl)  by(clarsimp simp: is_longest_prefix_routing_def)
      thus ?r by(fastforce simp add: True)
    next
      assume ?r
      then guess rr' .. note rr' = this
      have "rr' = rr" proof(rule ccontr)
        assume C: "rr'  rr"
        from C have e: "rr'  set rtbl" using rr' by simp
        show False proof cases
          assume eq: "routing_match rr' = routing_match rr"
          with e have "routing_rule_sort_key rr < routing_rule_sort_key rr'" using unambigous_prefix_routing_strong_mono[OF Cons.prems(2,4) _ eq] by simp
          with True rr' show False by simp
        next
          assume ne: "routing_match rr'  routing_match rr"
          from rr' Cons.prems have "valid_prefix (routing_match rr)" "valid_prefix (routing_match rr')" "prefix_match_semantics (routing_match rr') addr" by(auto simp add: valid_prefixes_alt_def)
          note same_length_prefixes_distinct[OF this(1,2) ne[symmetric] _ True this(3)]
          moreover have "routing_prefix rr = routing_prefix rr'" (is ?pe) proof -
            have "routing_rule_sort_key rr < routing_rule_sort_key rr'  ¬ prefix_match_semantics (routing_match rr) addr" using rr' by simp
            with unambigous_prefix_routing_weak_mono[OF Cons.prems(2) e] True have "routing_rule_sort_key rr = routing_rule_sort_key rr'" by simp
            thus ?pe by(simp add: routing_rule_sort_key_def int_of_nat_def)
          qed
          ultimately show False .
        qed
      qed
      thus ?l using rr' by simp
    qed
  qed
qed
    


subsection‹Printing›

definition "routing_rule_32_toString (rr::32 routing_rule)  
  prefix_match_32_toString (routing_match rr) 
@ (case next_hop (routing_action rr) of Some nh  '' via '' @ ipv4addr_toString nh | _  [])
@ '' dev '' @ routing_oiface rr 
@ '' metric '' @ string_of_nat (metric rr)"

definition "routing_rule_128_toString (rr::128 routing_rule)  
  prefix_match_128_toString (routing_match rr) 
@ (case next_hop (routing_action rr) of Some nh  '' via '' @ ipv6addr_toString nh | _  [])
@ '' dev '' @ routing_oiface rr 
@ '' metric '' @ string_of_nat (metric rr)"

lemma "map routing_rule_32_toString 
[rr_ctor (42,0,0,0) 7 ''eth0'' None 808, 
 rr_ctor (0,0,0,0) 0 ''eth1'' (Some (222,173,190,239)) 707] =
[''42.0.0.0/7 dev eth0 metric 808'',
 ''0.0.0.0/0 via 222.173.190.239 dev eth1 metric 707'']" by eval

section‹Routing table to Relation›

text‹Walking through a routing table splits the (remaining) IP space when traversing a routing table into a pair of sets:
 the pair contains the IPs concerned by the current rule and those left alone.›
private definition ipset_prefix_match where 
  "ipset_prefix_match pfx rg = (let pfxrg = prefix_to_wordset pfx in (rg  pfxrg, rg - pfxrg))"
private lemma ipset_prefix_match_m[simp]:  "fst (ipset_prefix_match pfx rg) = rg  (prefix_to_wordset pfx)" by(simp only: Let_def ipset_prefix_match_def, simp)
private lemma ipset_prefix_match_nm[simp]: "snd (ipset_prefix_match pfx rg) = rg - (prefix_to_wordset pfx)" by(simp only: Let_def ipset_prefix_match_def, simp)
private lemma ipset_prefix_match_distinct: "rpm = ipset_prefix_match pfx rg  
  (fst rpm)  (snd rpm) = {}" by force
private lemma ipset_prefix_match_complete: "rpm = ipset_prefix_match pfx rg  
  (fst rpm)  (snd rpm) = rg" by force
private lemma rpm_m_dup_simp: "rg  fst (ipset_prefix_match (routing_match r) rg) = fst (ipset_prefix_match (routing_match r) rg)"
  by simp
private definition range_prefix_match :: "'i::len prefix_match  'i wordinterval  'i wordinterval × 'i wordinterval" where
  "range_prefix_match pfx rg  (let pfxrg = prefix_to_wordinterval pfx in 
  (wordinterval_intersection rg pfxrg, wordinterval_setminus rg pfxrg))"
private lemma range_prefix_match_set_eq:
  "(λ(r1,r2). (wordinterval_to_set r1, wordinterval_to_set r2)) (range_prefix_match pfx rg) =
    ipset_prefix_match pfx (wordinterval_to_set rg)"
  unfolding range_prefix_match_def ipset_prefix_match_def Let_def 
  using wordinterval_intersection_set_eq wordinterval_setminus_set_eq prefix_to_wordinterval_set_eq  by auto
private lemma range_prefix_match_sm[simp]:  "wordinterval_to_set (fst (range_prefix_match pfx rg)) = 
    fst (ipset_prefix_match pfx (wordinterval_to_set rg))"
  by (metis fst_conv ipset_prefix_match_m  wordinterval_intersection_set_eq prefix_to_wordinterval_set_eq range_prefix_match_def)
private lemma range_prefix_match_snm[simp]: "wordinterval_to_set (snd (range_prefix_match pfx rg)) =
    snd (ipset_prefix_match pfx (wordinterval_to_set rg))"
  by (metis snd_conv ipset_prefix_match_nm wordinterval_setminus_set_eq prefix_to_wordinterval_set_eq range_prefix_match_def)

subsection‹Wordintervals for Ports by Routing›
text‹This split, although rather trivial, 
can be used to construct the sets (or rather: the intervals) 
of IPs that are actually matched by an entry in a routing table.›

private fun routing_port_ranges :: "'i prefix_routing  'i wordinterval  (string × ('i::len) wordinterval) list" where
"routing_port_ranges [] lo = (if wordinterval_empty lo then [] else [(routing_oiface (undefined::'i routing_rule),lo)])" | (* insert default route to nirvana. has to match what routing_table_semantics does. *)
"routing_port_ranges (a#as) lo = (
	let rpm = range_prefix_match (routing_match a) lo; m = fst rpm; nm = snd rpm in (
	(routing_oiface a,m) # routing_port_ranges as nm))"

private lemma routing_port_ranges_subsets:
"(a1, b1)  set (routing_port_ranges tbl s)  wordinterval_to_set b1  wordinterval_to_set s"
  by(induction tbl arbitrary: s; fastforce simp add: Let_def split: if_splits)

private lemma routing_port_ranges_sound: "e  set (routing_port_ranges tbl s)  k  wordinterval_to_set (snd e)  valid_prefixes tbl 
	fst e = output_iface (routing_table_semantics tbl k)"
proof(induction tbl arbitrary: s)
	case (Cons a as)
	note s = Cons.prems(1)[unfolded routing_port_ranges.simps Let_def list.set]
	note vpfx = valid_prefixes_split[OF Cons.prems(3)] 
	show ?case (is ?kees) proof(cases "e = (routing_oiface a, fst (range_prefix_match (routing_match a) s))")
		case False
		hence es: "e  set (routing_port_ranges as (snd (range_prefix_match (routing_match a) s)))" using s by blast
		note eq = Cons.IH[OF this Cons.prems(2) conjunct2[OF vpfx]]
		have "¬prefix_match_semantics (routing_match a) k" (is ?nom)
		proof -
		  from routing_port_ranges_subsets[of "fst e" "snd e", unfolded prod.collapse, OF es]
		  have *: "wordinterval_to_set (snd e)  wordinterval_to_set (snd (range_prefix_match (routing_match a) s))" .
			show ?nom unfolding prefix_match_semantics_wordset[OF conjunct1[OF vpfx]]
			  using * Cons.prems(2)	unfolding wordinterval_subset_set_eq
				by(auto simp add: range_prefix_match_def Let_def)
		qed
		thus ?kees using eq by simp
	next
		case True
		hence fe: "fst e = routing_oiface a" by simp
		from True have "k  wordinterval_to_set (fst (range_prefix_match (routing_match a) s))"
			using Cons.prems(2) by(simp)
		hence "prefix_match_semantics (routing_match a) k" 
			unfolding prefix_match_semantics_wordset[OF conjunct1, OF vpfx]
			unfolding range_prefix_match_def Let_def
			by simp
		thus ?kees by(simp add: fe)
	qed
qed (simp split: if_splits)

private lemma routing_port_ranges_disjoined:
assumes vpfx: "valid_prefixes tbl"
  and ins:  "(a1, b1)  set (routing_port_ranges tbl s)" "(a2, b2)  set (routing_port_ranges tbl s)"
  and nemp: "wordinterval_to_set b1  {}"
shows "b1  b2  wordinterval_to_set b1  wordinterval_to_set b2 = {}"
using assms
proof(induction tbl arbitrary: s)
  case (Cons r rs)
  have vpfx: "valid_prefix (routing_match r)" "valid_prefixes rs" using Cons.prems(1) using valid_prefixes_split by blast+
  { (* In case that one of b1 b2 stems from r and one does not, we assume it is b1 WLOG. *)
    fix a1 b1 a2 b2
    assume one: "b1 = fst (range_prefix_match (routing_match r) s)"
    assume two: "(a2, b2)  set (routing_port_ranges rs (snd (range_prefix_match (routing_match r) s)))"
    have dc: "wordinterval_to_set (snd (range_prefix_match (routing_match r) s)) 
          wordinterval_to_set (fst (range_prefix_match (routing_match r) s)) = {}" by force
    hence "wordinterval_to_set b1  wordinterval_to_set b2 = {}"
    unfolding one using two[THEN routing_port_ranges_subsets] by fast
  } note * = this
  show ?case
  using (a1, b1)  set (routing_port_ranges (r # rs) s) (a2, b2)  set (routing_port_ranges (r # rs) s) nemp
    Cons.IH[OF vpfx(2)] * 
    by(fastforce simp add: Let_def)    
qed (simp split: if_splits)

private lemma routing_port_rangesI:
"valid_prefixes tbl 
 output_iface (routing_table_semantics tbl k) = output_port 
 k  wordinterval_to_set wi 
 (ip_range. (output_port, ip_range)  set (routing_port_ranges tbl wi)  k  wordinterval_to_set ip_range)"
proof(induction tbl arbitrary: wi)
  case Nil thus ?case by simp blast
next
  case (Cons r rs)
  from Cons.prems(1) have vpfx: "valid_prefix (routing_match r)" and vpfxs: "valid_prefixes rs" 
    by(simp_all add: valid_prefixes_split)
  show ?case
  proof(cases "prefix_match_semantics (routing_match r) k")
    case True
    thus ?thesis 
      using Cons.prems(2) using vpfx k  wordinterval_to_set wi
      by (intro exI[where x =  "fst (range_prefix_match (routing_match r) wi)"]) 
         (simp add: prefix_match_semantics_wordset Let_def)
  next
    case False
    with k  wordinterval_to_set wi have ksnd: "k  wordinterval_to_set (snd (range_prefix_match (routing_match r) wi))"
      by (simp add: prefix_match_semantics_wordset vpfx)
    have mpr: "output_iface (routing_table_semantics rs k) = output_port" using Cons.prems False by simp
    note Cons.IH[OF vpfxs mpr ksnd]
    thus ?thesis by(fastforce simp: Let_def)
  qed
qed

subsection‹Reduction›
text‹So far, one entry in the list would be generated for each routing table entry. 
This next step reduces it to one for each port. 
The resulting list will represent a function from port to IP wordinterval.
(It can also be understood as a function from IP (interval) to port (where the intervals don't overlap).›

definition "reduce_range_destination l 
let ps = remdups (map fst l) in
let c = λs. (wordinterval_Union  map snd  filter (((=) s)  fst)) l in
[(p, c p). p  ps]
"

definition "routing_ipassmt_wi tbl  reduce_range_destination (routing_port_ranges tbl wordinterval_UNIV)"

lemma routing_ipassmt_wi_distinct: "distinct (map fst (routing_ipassmt_wi tbl))"
  unfolding routing_ipassmt_wi_def reduce_range_destination_def
  by(simp add: comp_def)

private lemma routing_port_ranges_superseted:
"(a1,b1)  set (routing_port_ranges tbl wordinterval_UNIV)  
  b2. (a1,b2)  set (routing_ipassmt_wi tbl)  wordinterval_to_set b1  wordinterval_to_set b2"
  unfolding routing_ipassmt_wi_def reduce_range_destination_def
  by(force simp add: Set.image_iff wordinterval_Union)

private lemma routing_ipassmt_wi_subsetted:
"(a1,b1)  set (routing_ipassmt_wi tbl)  
 (a1,b2)  set (routing_port_ranges tbl wordinterval_UNIV)   wordinterval_to_set b2  wordinterval_to_set b1"
  unfolding routing_ipassmt_wi_def reduce_range_destination_def
  by(fastforce simp add: Set.image_iff wordinterval_Union comp_def)

text‹This lemma should hold without the @{const valid_prefixes} assumption, but that would break the semantic argument and make the proof a lot harder.›
lemma routing_ipassmt_wi_disjoint:
assumes vpfx: "valid_prefixes (tbl::('i::len) prefix_routing)"
  and dif: "a1  a2"
  and ins:  "(a1, b1)  set (routing_ipassmt_wi tbl)" "(a2, b2)  set (routing_ipassmt_wi tbl)"
shows "wordinterval_to_set b1  wordinterval_to_set b2 = {}"
proof(rule ccontr)
  note iuf = ins[unfolded routing_ipassmt_wi_def reduce_range_destination_def Let_def, simplified, unfolded Set.image_iff comp_def, simplified]
  assume "(wordinterval_to_set b1  wordinterval_to_set b2  {})"
  hence "wordinterval_to_set b1  wordinterval_to_set b2  {}" by simp
  text‹If the intervals are not disjoint, there exists a witness of that.›
  then obtain x where x[simp]: "x  wordinterval_to_set b1" "x  wordinterval_to_set b2" by blast
  text‹This witness has to have come from some entry in the result of @{const routing_port_ranges}, for both of @{term b1} and @{term b2}.›
  hence "b1g. x  wordinterval_to_set b1g  wordinterval_to_set b1g  wordinterval_to_set b1  (a1, b1g)  set (routing_port_ranges tbl wordinterval_UNIV)"
    using iuf(1) by(fastforce simp add: wordinterval_Union) (* strangely, this doesn't work with obtain *)
  then obtain b1g where b1g: "x  wordinterval_to_set b1g" "wordinterval_to_set b1g  wordinterval_to_set b1" "(a1, b1g)  set (routing_port_ranges tbl wordinterval_UNIV)" by clarsimp
  from x have "b2g. x  wordinterval_to_set b2g  wordinterval_to_set b2g  wordinterval_to_set b2  (a2, b2g)  set (routing_port_ranges tbl wordinterval_UNIV)"
    using iuf(2) by(fastforce simp add: wordinterval_Union)
  then obtain b2g where b2g: "x  wordinterval_to_set b2g" "wordinterval_to_set b2g  wordinterval_to_set b2" "(a2, b2g)  set (routing_port_ranges tbl wordinterval_UNIV)" by clarsimp
  text‹Soudness tells us that the both @{term a1} and @{term a2} have to be the result of routing @{term x}.›
  note routing_port_ranges_sound[OF b1g(3), unfolded fst_conv snd_conv, OF b1g(1) vpfx] routing_port_ranges_sound[OF b2g(3), unfolded fst_conv snd_conv, OF b2g(1) vpfx]
  text‹A contradiction follows from @{thm dif}.›
  with dif show False by simp
qed

lemma routing_ipassmt_wi_sound:
  assumes vpfx: "valid_prefixes tbl"
  and ins: "(ea,eb)  set (routing_ipassmt_wi tbl)"
  and x: "k  wordinterval_to_set eb"
  shows "ea = output_iface (routing_table_semantics tbl k)"
proof -
  note iuf = ins[unfolded routing_ipassmt_wi_def reduce_range_destination_def Let_def, simplified, unfolded Set.image_iff comp_def, simplified]
  from x have "b1g. k  wordinterval_to_set b1g  wordinterval_to_set b1g  wordinterval_to_set eb  (ea, b1g)  set (routing_port_ranges tbl wordinterval_UNIV)"
    using iuf(1) by(fastforce simp add: wordinterval_Union)
  then obtain b1g where b1g: "k  wordinterval_to_set b1g" "wordinterval_to_set b1g  wordinterval_to_set eb" "(ea, b1g)  set (routing_port_ranges tbl wordinterval_UNIV)" by clarsimp
  note routing_port_ranges_sound[OF b1g(3), unfolded fst_conv snd_conv, OF b1g(1) vpfx]
  thus ?thesis .
qed

theorem routing_ipassmt_wi:
assumes vpfx: "valid_prefixes tbl"
  shows 
  "output_iface (routing_table_semantics tbl k) = output_port 
    (ip_range. k  wordinterval_to_set ip_range  (output_port, ip_range)  set (routing_ipassmt_wi tbl))"
proof (intro iffI, goal_cases)
  case 2 with vpfx routing_ipassmt_wi_sound show ?case by blast
next
  case 1
  then obtain ip_range where "(output_port, ip_range)  set (routing_port_ranges tbl wordinterval_UNIV)  k  wordinterval_to_set ip_range"
    using routing_port_rangesI[where wi = wordinterval_UNIV, OF vpfx] by auto
  thus ?case
    unfolding routing_ipassmt_wi_def reduce_range_destination_def
    unfolding Let_def comp_def
    by(force simp add: Set.image_iff wordinterval_Union)
qed

(* this was not given for the old reduced_range_destination *)
lemma routing_ipassmt_wi_has_all_interfaces:
  assumes in_tbl: "r  set tbl"
  shows "s. (routing_oiface r,s)  set (routing_ipassmt_wi tbl)"
proof -
  from in_tbl have "s. (routing_oiface r,s)  set (routing_port_ranges tbl S)" for S
  proof(induction tbl arbitrary: S)
    case (Cons l ls)
    show ?case
    proof(cases "r = l")
      case True thus ?thesis using Cons.prems by(auto simp: Let_def)
    next
      case False with Cons.prems have "r  set ls" by simp
      from Cons.IH[OF this] show ?thesis by(simp add: Let_def) blast
    qed
  qed simp
  thus ?thesis
    unfolding routing_ipassmt_wi_def reduce_range_destination_def
    by(force simp add: Set.image_iff)
qed

end

end

Theory Linux_Router

section "Linux Router"
theory Linux_Router
imports 
	Routing_Table
	Simple_Firewall.SimpleFw_Semantics
	Simple_Firewall.Simple_Packet
	"HOL-Library.Monad_Syntax"
begin

definition "fromMaybe a m = (case m of Some a  a | None  a)" (* mehr Haskell wagen *)

text‹Here, we present a heavily simplified model of a linux router. 
(i.e., a linux-based device with \texttt{net.ipv4.ip\_forward})
It covers the following steps in packet processing:
\begin{itemize}
 \item Packet arrives (destination port is empty, destination mac address is own address).
 \item Destination address is extracted and used for a routing table lookup.
 \item Packet is updated with output interface of routing decision.
 \item The FORWARD chain of iptables is considered.
 \item Next hop is extracted from the routing decision, fallback to destination address if directly attached.
 \item MAC address of next hop is looked up (using the mac lookup function mlf)
 \item L2 destination address of packet is updated.
\end{itemize}
This is stripped down to model only the most important and widely used aspects of packet processing.
Here are a few examples of what was abstracted away:
\begin{itemize}
 \item No local traffic.
 \item Only the \texttt{filter} table of iptables is considered, \texttt{raw} and \texttt{nat} are not.
 \item Only one routing table is considered. (Linux can have other tables than the \texttt{default} one.)
 \item No source MAC modification.
 \item \ldots
\end{itemize}
›

record interface =
	iface_name :: string
	iface_mac :: "48 word"
	(*iface_ips :: "(ipv4addr × 32 prefix_match) set" (* there is a set of IP addresses and the reachable subnets for them *), but we don't use that right now, so it is commented out. 
	Also, part of that information is already in the routing table, so careful here... *)

definition iface_packet_check ::  "interface list ('i::len,'b) simple_packet_ext_scheme  interface option"
where "iface_packet_check ifs p  find (λi. iface_name i = p_iiface p  iface_mac i = p_l2dst p) ifs" 
term simple_fw
definition simple_linux_router ::
  "'i routing_rule list  'i simple_rule list  (('i::len) word  48 word option)  
         interface list  'i simple_packet_ext  'i simple_packet_ext option" where
"simple_linux_router rt fw mlf ifl p  do {
	_  iface_packet_check ifl p;
	let rd ― ‹(routing decision)› = routing_table_semantics rt (p_dst p);
	let p = pp_oiface := output_iface rd;
	let fd ― ‹(firewall decision)› = simple_fw fw p;
	_  (case fd of Decision FinalAllow  Some () | Decision FinalDeny  None);
	let nh = fromMaybe (p_dst p) (next_hop rd);
	ma  mlf nh;
	Some (pp_l2dst := ma)
}"
(* Can I find something that looks a bit more semantic. Maybe the option monad can reduce a bit of the foo? *)
(* TODO: What happens in linux, if I send a packet to an interface with the mac of another interface? Hopefully, that is going to be dropped? *) 

text‹However, the above model is still too powerful for some use-cases.
Especially, the next hop look-up cannot be done without either a pre-distributed table of all MAC addresses,
or the usual mechanic of sending out an ARP request and caching the answer.
Doing ARP requests in the restricted environment of, e.g., an OpenFlow ruleset seems impossible.
Therefore, we present this model:›
definition simple_linux_router_nol12 ::
    "'i routing_rule list  'i simple_rule list  ('i,'a) simple_packet_scheme  ('i::len,'a) simple_packet_scheme option" where
"simple_linux_router_nol12 rt fw p  do {
	let rd = routing_table_semantics rt (p_dst p);
	let p = pp_oiface := output_iface rd;
	let fd = simple_fw fw p;
	_  (case fd of Decision FinalAllow  Some () | Decision FinalDeny  None);
	Some p
}"
text‹The differences to @{const simple_linux_router} are illustrated by the lemmata below.›
(* an alternative formulation would maybe be "if the routing decision for the source is the same as for the destination, don't forward it." 
   This might be advantageous in $cases, however, this formulation is clearly easier to translate to openflow. *)

lemma rtr_nomac_e1:
  fixes pi
	assumes "simple_linux_router rt fw mlf ifl pi = Some po"
	assumes "simple_linux_router_nol12 rt fw pi = Some po'"
	shows "x. po = po'p_l2dst := x"
using assms
unfolding simple_linux_router_nol12_def simple_linux_router_def
by(simp add: Let_def split: option.splits state.splits final_decision.splits Option.bind_splits if_splits) blast+

lemma rtr_nomac_e2:
  fixes pi
	assumes "simple_linux_router rt fw mlf ifl pi = Some po"
	shows "po'. simple_linux_router_nol12 rt fw pi = Some po'"
using assms
unfolding simple_linux_router_nol12_def simple_linux_router_def
by(clarsimp simp add: Let_def split: option.splits state.splits final_decision.splits Option.bind_splits if_splits)

lemma rtr_nomac_e3:
  fixes pi
	assumes "simple_linux_router_nol12 rt fw pi = Some po"
	assumes "iface_packet_check ifl pi = Some i ― ‹don't care›"
	assumes "mlf (fromMaybe (p_dst pi) (next_hop (routing_table_semantics rt (p_dst pi)))) = Some i2"
	shows "po'. simple_linux_router rt fw mlf ifl pi = Some po'"
using assms
unfolding simple_linux_router_nol12_def simple_linux_router_def
by(clarsimp simp add: Let_def split: option.splits state.splits final_decision.splits Option.bind_splits if_splits)

lemma rtr_nomac_eq:
  fixes pi
	assumes "iface_packet_check ifl pi  None"
	assumes "mlf (fromMaybe (p_dst pi) (next_hop (routing_table_semantics rt (p_dst pi))))  None"
	shows "x. map_option (λp. pp_l2dst := x) (simple_linux_router_nol12 rt fw pi) = simple_linux_router rt fw mlf ifl pi"
proof(cases "simple_linux_router_nol12 rt fw pi"; cases "simple_linux_router rt fw mlf ifl pi")
	fix a b
	assume as: "simple_linux_router rt fw mlf ifl pi = Some b" "simple_linux_router_nol12 rt fw pi = Some a"
	note rtr_nomac_e1[OF this]
	with as show ?thesis by auto 
next
	fix a assume as: "simple_linux_router_nol12 rt fw pi = None" "simple_linux_router rt fw mlf ifl pi = Some a"
	note rtr_nomac_e2[OF as(2)]
	with as(1) have False by simp
	thus ?thesis ..
next
	fix a assume as: "simple_linux_router_nol12 rt fw pi = Some a" "simple_linux_router rt fw mlf ifl pi = None"
	from ‹iface_packet_check ifl pi  None› obtain i3 where "iface_packet_check ifl pi = Some i3" by blast
	note rtr_nomac_e3[OF as(1) this] assms(2)
	with as(2) have False by force
	thus ?thesis ..
qed simp

end

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›
                  
MLOuter_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)

MLOuter_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

File ‹IpRoute_Parser.ml›

fun register_ip_route bitness (name,path) (lthy: local_theory) =
	let
	val _ = case bitness of
	    32  => writeln "Using IPv4 parser"
    | 128 => writeln "Using IPv6 parser"
    | _   => raise Fail("Unable to decide on IPv4 or IPv6")

	(* Bitness dependent stuff *)
  val v4 = (bitness = 32)
  val parser_ip = if v4 then (parser_ipv4 >> (fn ip => mk_ipv4addr ip)) else (parser_ipv6 >> (fn ip => mk_ipv6addr ip))
  val next_hop_update = if v4 then @{const routing_action_next_hop_update (32)} else @{const routing_action_next_hop_update (128)}
  val construct_prefix = if v4 then @{term "PrefixMatch :: 32 word  nat  32 prefix_match"} else @{term "PrefixMatch :: 128 word  nat  128 prefix_match"}
  val default_prefix = if v4 then @{const default_prefix (32)} else @{const default_prefix (128)}
  val oiface_update = if v4 then @{term "routing_action_oiface_update :: string  32 routing_rule  32 routing_rule"} else @{term "routing_action_oiface_update :: string  128 routing_rule  128 routing_rule"}
  val metric_update = if v4 then @{term "metric_update :: (nat  nat)  32 routing_rule  32 routing_rule"} else @{term "metric_update :: (nat  nat)  128 routing_rule  128 routing_rule"}
  val empty_rr = if v4 then @{const empty_rr_hlp (32)} else @{const empty_rr_hlp (128)}
  fun to_rtbl r = if v4 then @{const sort_rtbl (32)} $ (HOLogic.mk_list @{typ "32 routing_rule"} r) else @{const sort_rtbl (128)} $ (HOLogic.mk_list @{typ "128 routing_rule"} r)
  fun sanity_check r = if v4 then @{const sanity_ip_route (32)} $ r else @{const sanity_ip_route (128)} $ r

  (* the parser *)
  fun define_const (t: term) (name: binding) (lthy: local_theory) : local_theory = let
        val _ = writeln ("Defining constant `"^Binding.name_of name^"' ("^Binding.name_of name^"_def')...");
        val ((_, (_, thm)), lthy) = Local_Theory.define ((name, NoSyn), ((Binding.empty, []), t)) lthy;
        val (_, lthy) = Local_Theory.note ((Binding.suffix_name "_def" name, @{attributes [code]}), [thm]) lthy;
       in
         lthy
  end
  fun load_file (thy: theory) (path: string list) =
      let val p =  File.full_path (Resources.master_directory thy) (Path.make path); in
      let val _ = "Loading file "^File.platform_path p |> writeln; in
        if not (File.exists p) orelse (File.is_dir p) then raise Fail "File not found" else File.read_lines p
   end end;

  (* and now, some code duplication with the IPtables parser… *)
  fun extract_int ss = case ss |> implode |> Int.fromString of SOME i => i
                                                             | NONE => raise Fail "unparsable int";

  fun is_iface_char x = Symbol.is_ascii x andalso
      (Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "+" orelse x = "*" orelse x = "." orelse x = "-")
  fun mk_nat maxval i = if i < 0 orelse i > maxval
            then
              raise Fail("nat ("^Int.toString i^") must be between 0 and "^Int.toString maxval)
            else (HOLogic.mk_number HOLogic.natT i);

  fun ipprefix_to_hol (ip,len) = construct_prefix $ ip $ mk_nat bitness len;
  
  val parser_ip_cidr = parser_ip --| ($$ "/") -- (Scan.many1 Symbol.is_ascii_digit >> extract_int) >> ipprefix_to_hol;
  
  val parser_interface = Scan.many1 is_iface_char >> (implode #> (fn x => HOLogic.mk_string x));
  (* end dup *)
  
  val parser_subnet =  (Scan.this_string "default" >> K default_prefix) ||
    parser_ip_cidr ||
    (parser_ip >> (fn ip => ipprefix_to_hol (ip,bitness)))
  val isSpace = (fn x => x = " " orelse  x = "\t")
  val parser_whitespace = Scan.many1 isSpace;
  val eater_whitespace = Scan.many isSpace; (* I refuse to have this eat \r to make the parser work with windows newlines. *)

  val parser_via = (Scan.this_string "via" -- parser_whitespace |-- parser_ip)
    >> (fn ip => fn pk => next_hop_update $ ip $ pk)
  val parser_dev = (Scan.this_string "dev" -- parser_whitespace |-- parser_interface)
    >> (fn dev => fn pk => oiface_update $ dev $ pk)
  val parser_metric = (Scan.this_string "metric" -- parser_whitespace |-- Scan.many1 Symbol.is_ascii_digit)
    >> (fn metric => fn pk => metric_update $ (@{term "(λ x _. x) :: nat  nat  nat"} $ (mk_nat 65535 (extract_int metric))) $ pk)

  (* the following values are going to be ignored since they can't be represented in the model, but I want to make sure they are parsed correctly *)
  val parser_scope = (Scan.this_string "scope" -- parser_whitespace |-- (
    Scan.this_string "host" || Scan.this_string "link" || Scan.this_string "global" || (Scan.many1 Symbol.is_ascii_digit >> implode)))
    >> K I (* K I -> constant ignore: this value indicates the scope of validity of the rule *)
  val parser_proto = (Scan.this_string "proto" -- parser_whitespace |-- (
    Scan.this_string "kernel" || Scan.this_string "boot" || Scan.this_string "static" || Scan.this_string "dhcp" || (Scan.many1 Symbol.is_ascii_digit >> implode)))
    >> K I (* ignore: this value indicates how the rt-entry came to existence *)
  val parser_src = (Scan.this_string "src" -- parser_whitespace |-- parser_ipv4) 
    >> K I (* ignore: this value is used if an application (on the same device as the routing table) is sending an IP packet and has not bound to a specific address *)

  (* TODO (for IPv6) there might be some more options to ignore… "pref medium"? *)

  fun parser_end p i = let
    val (r,es) = Scan.finite Symbol.stopper (p --| eater_whitespace) i
  in
    if es = [] then r else let val _ = writeln ("'" ^ (implode es) ^ "'") in K r (* cause error - TODO: How do I do that properly? *) 
    (($$ "x") (Symbol.explode ""))
  end end

  val parser =
    (parser_end ((parser_subnet >> (fn x => empty_rr $ x))
        -- Scan.repeat (parser_whitespace |-- (parser_via || parser_dev || parser_metric || parser_scope || parser_proto || parser_src)))) 
    #> swap #> (uncurry (fold (fn a => fn b => a b)))

  fun sanity_check_ip_route (ctx: Proof.context) t = let
    val _ = writeln "Checking sanity..."
    val check = Code_Evaluation.dynamic_value_strict ctx (sanity_check t)
  in
    if check <> @{term "True"} then raise ERROR "sanity_wf_ruleset failed" else t
  end;
	  val fcontent = load_file (Proof_Context.theory_of lthy) [path]
	  (*val _ = map (Pretty.writeln o Syntax.pretty_term @{context} o parser o Symbol.explode) fcontent (* keep this one, lets you see on which line it fails *)*)
	  val r = map (parser o Symbol.explode) fcontent
	  val c = to_rtbl r
	  val s = sanity_check_ip_route lthy c
	  val d = define_const s name lthy
	  val _ = writeln "Done."
	in
	  d
end