Theory Aodv_Data
section "Predicates and functions used in the AODV model"
theory Aodv_Data
imports Aodv_Basic
begin
subsection "Sequence Numbers"
text ‹Sequence numbers approximate the relative freshness of routing information.›
definition inc :: "sqn ⇒ sqn"
where "inc sn ≡ if sn = 0 then sn else sn + 1"
lemma less_than_inc [simp]: "x ≤ inc x"
unfolding inc_def by simp
lemma inc_minus_suc_0 [simp]:
"inc x - Suc 0 = x"
unfolding inc_def by simp
lemma inc_never_one' [simp, intro]: "inc x ≠ Suc 0"
unfolding inc_def by simp
lemma inc_never_one [simp, intro]: "inc x ≠ 1"
by simp
subsection "Modelling Routes"
text ‹
A route is a 6-tuple, @{term "(dsn, dsk, flag, hops, nhip, pre)"} where
@{term dsn} is the `destination sequence number', @{term dsk} is the
`destination-sequence-number status', @{term flag} is the route status,
@{term hops} is the number of hops to the destination, @{term nhip} is the
next hop toward the destination, and @{term pre} is the set of `precursor nodes'--those
interested in hearing about changes to the route.
›
type_synonym r = "sqn × k × f × nat × ip × ip set"
definition proj2 :: "r ⇒ sqn" ("π⇩2")
where "π⇩2 ≡ λ(dsn, _, _, _, _, _). dsn"
definition proj3 :: "r ⇒ k" ("π⇩3")
where "π⇩3 ≡ λ(_, dsk, _, _, _, _). dsk"
definition proj4 :: "r ⇒ f" ("π⇩4")
where "π⇩4 ≡ λ(_, _, flag, _, _, _). flag"
definition proj5 :: "r ⇒ nat" ("π⇩5")
where "π⇩5 ≡ λ(_, _, _, hops, _, _). hops"
definition proj6 :: "r ⇒ ip" ("π⇩6")
where "π⇩6 ≡ λ(_, _, _, _, nhip, _). nhip"
definition proj7 :: "r ⇒ ip set" ("π⇩7")
where "π⇩7 ≡ λ(_, _, _, _, _, pre). pre"
lemma projs [simp]:
"π⇩2(dsn, dsk, flag, hops, nhip, pre) = dsn"
"π⇩3(dsn, dsk, flag, hops, nhip, pre) = dsk"
"π⇩4(dsn, dsk, flag, hops, nhip, pre) = flag"
"π⇩5(dsn, dsk, flag, hops, nhip, pre) = hops"
"π⇩6(dsn, dsk, flag, hops, nhip, pre) = nhip"
"π⇩7(dsn, dsk, flag, hops, nhip, pre) = pre"
by (clarsimp simp: proj2_def proj3_def proj4_def
proj5_def proj6_def proj7_def)+
lemma proj3_pred [intro]: "⟦ P kno; P unk ⟧ ⟹ P (π⇩3 x)"
by (rule k.induct)
lemma proj4_pred [intro]: "⟦ P val; P inv ⟧ ⟹ P (π⇩4 x)"
by (rule f.induct)
lemma proj6_pair_snd [simp]:
fixes dsn' r
shows "π⇩6 (dsn', snd (r)) = π⇩6(r)"
by (cases r) simp
subsection "Routing Tables"
text ‹Routing tables map ip addresses to route entries.›
type_synonym rt = "ip ⇀ r"
syntax
"_Sigma_route" :: "rt ⇒ ip ⇀ r" ("σ⇘route⇙'(_, _')")
translations
"σ⇘route⇙(rt, dip)" => "rt dip"
definition sqn :: "rt ⇒ ip ⇒ sqn"
where "sqn rt dip ≡ case σ⇘route⇙(rt, dip) of Some r ⇒ π⇩2(r) | None ⇒ 0"
definition sqnf :: "rt ⇒ ip ⇒ k"
where "sqnf rt dip ≡ case σ⇘route⇙(rt, dip) of Some r ⇒ π⇩3(r) | None ⇒ unk"
abbreviation flag :: "rt ⇒ ip ⇀ f"
where "flag rt dip ≡ map_option π⇩4 (σ⇘route⇙(rt, dip))"
abbreviation dhops :: "rt ⇒ ip ⇀ nat"
where "dhops rt dip ≡ map_option π⇩5 (σ⇘route⇙(rt, dip))"
abbreviation nhop :: "rt ⇒ ip ⇀ ip"
where "nhop rt dip ≡ map_option π⇩6 (σ⇘route⇙(rt, dip))"
abbreviation precs :: "rt ⇒ ip ⇀ ip set"
where "precs rt dip ≡ map_option π⇩7 (σ⇘route⇙(rt, dip))"
definition vD :: "rt ⇒ ip set"
where "vD rt ≡ {dip. flag rt dip = Some val}"
definition iD :: "rt ⇒ ip set"
where "iD rt ≡ {dip. flag rt dip = Some inv}"
definition kD :: "rt ⇒ ip set"
where "kD rt ≡ {dip. rt dip ≠ None}"
lemma kD_is_vD_and_iD: "kD rt = vD rt ∪ iD rt"
unfolding kD_def vD_def iD_def by auto
lemma vD_iD_gives_kD [simp]:
"⋀ip rt. ip ∈ vD rt ⟹ ip ∈ kD rt"
"⋀ip rt. ip ∈ iD rt ⟹ ip ∈ kD rt"
unfolding kD_is_vD_and_iD by simp_all
lemma kD_Some [dest]:
fixes dip rt
assumes "dip ∈ kD rt"
shows "∃dsn dsk flag hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, flag, hops, nhip, pre)"
using assms unfolding kD_def by simp
lemma kD_None [dest]:
fixes dip rt
assumes "dip ∉ kD rt"
shows "σ⇘route⇙(rt, dip) = None"
using assms unfolding kD_def
by (metis (mono_tags) mem_Collect_eq)
lemma vD_Some [dest]:
fixes dip rt
assumes "dip ∈ vD rt"
shows "∃dsn dsk hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, val, hops, nhip, pre)"
using assms unfolding vD_def by simp
lemma vD_empty [simp]: "vD Map.empty = {}"
unfolding vD_def by simp
lemma iD_Some [dest]:
fixes dip rt
assumes "dip ∈ iD rt"
shows "∃dsn dsk hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, inv, hops, nhip, pre)"
using assms unfolding iD_def by simp
lemma val_is_vD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "the (flag rt ip) = val"
shows "ip∈vD(rt)"
using assms unfolding vD_def by auto
lemma inv_is_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "the (flag rt ip) = inv"
shows "ip∈iD(rt)"
using assms unfolding iD_def by auto
lemma iD_flag_is_inv [elim, simp]:
fixes ip rt
assumes "ip∈iD(rt)"
shows "the (flag rt ip) = inv"
proof -
from ‹ip∈iD(rt)› have "ip∈kD(rt)" by auto
with assms show ?thesis unfolding iD_def by auto
qed
lemma kD_but_not_vD_is_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "ip∉vD(rt)"
shows "ip∈iD(rt)"
proof -
from ‹ip∈kD(rt)› obtain dsn dsk f hops nhop pre
where rtip: "rt ip = Some (dsn, dsk, f, hops, nhop, pre)"
by (metis kD_Some)
from ‹ip∉vD(rt)› have "f ≠ val"
proof (rule contrapos_nn)
assume "f = val"
with rtip have "the (flag rt ip) = val" by simp
with ‹ip∈kD(rt)› show "ip∈vD(rt)" ..
qed
with rtip have "the (flag rt ip)= inv" by simp
with ‹ip∈kD(rt)› show "ip∈iD(rt)" ..
qed
lemma vD_or_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "ip∈vD(rt) ⟹ P rt ip"
and "ip∈iD(rt) ⟹ P rt ip"
shows "P rt ip"
proof -
from ‹ip∈kD(rt)› have "ip∈vD(rt) ∪ iD(rt)"
by (simp add: kD_is_vD_and_iD)
thus ?thesis by (auto elim: assms(2-3))
qed
lemma proj5_eq_dhops: "⋀dip rt. dip∈kD(rt) ⟹ π⇩5(the (rt dip)) = the (dhops rt dip)"
unfolding sqn_def by (drule kD_Some) clarsimp
lemma proj4_eq_flag: "⋀dip rt. dip∈kD(rt) ⟹ π⇩4(the (rt dip)) = the (flag rt dip)"
unfolding sqn_def by (drule kD_Some) clarsimp
lemma proj2_eq_sqn: "⋀dip rt. dip∈kD(rt) ⟹ π⇩2(the (rt dip)) = sqn rt dip"
unfolding sqn_def by (drule kD_Some) clarsimp
lemma kD_sqnf_is_proj3 [simp]:
"⋀ip rt. ip∈kD(rt) ⟹ sqnf rt ip = π⇩3(the (rt ip))"
unfolding sqnf_def by auto
lemma vD_flag_val [simp]:
"⋀dip rt. dip ∈ vD (rt) ⟹ the (flag rt dip) = val"
unfolding vD_def by clarsimp
lemma kD_update [simp]:
"⋀rt nip v. kD (rt(nip ↦ v)) = insert nip (kD rt)"
unfolding kD_def by auto
lemma kD_empty [simp]: "kD Map.empty = {}"
unfolding kD_def by simp
lemma ip_equal_or_known [elim]:
fixes rt ip ip'
assumes "ip = ip' ∨ ip∈kD(rt)"
and "ip = ip' ⟹ P rt ip ip'"
and "⟦ ip ≠ ip'; ip∈kD(rt)⟧ ⟹ P rt ip ip'"
shows "P rt ip ip'"
using assms by auto
subsection "Updating Routing Tables"
text ‹Routing table entries are modified through explicit functions.
The properties of these functions are important in invariant proofs.›
subsubsection "Updating Precursor Lists"
definition addpre :: "r ⇒ ip set ⇒ r"
where "addpre r npre ≡ let (dsn, dsk, flag, hops, nhip, pre) = r in
(dsn, dsk, flag, hops, nhip, pre ∪ npre)"
lemma proj2_addpre:
fixes v pre
shows "π⇩2(addpre v pre) = π⇩2(v)"
unfolding addpre_def by (cases v) simp
lemma proj3_addpre:
fixes v pre
shows "π⇩3(addpre v pre) = π⇩3(v)"
unfolding addpre_def by (cases v) simp
lemma proj4_addpre:
fixes v pre
shows "π⇩4(addpre v pre) = π⇩4(v)"
unfolding addpre_def by (cases v) simp
lemma proj5_addpre:
fixes v pre
shows "π⇩5(addpre v pre) = π⇩5(v)"
unfolding addpre_def by (cases v) simp
lemma proj6_addpre:
fixes dsn dsk flag hops nhip pre npre
shows "π⇩6(addpre v npre) = π⇩6(v)"
unfolding addpre_def by (cases v) simp
lemma proj7_addpre:
fixes dsn dsk flag hops nhip pre npre
shows "π⇩7(addpre v npre) = π⇩7(v) ∪ npre"
unfolding addpre_def by (cases v) simp
lemma addpre_empty: "addpre r {} = r"
unfolding addpre_def by simp
lemma addpre_r:
"addpre (dsn, dsk, fl, hops, nhip, pre) npre = (dsn, dsk, fl, hops, nhip, pre ∪ npre)"
unfolding addpre_def by simp
lemmas addpre_simps [simp] = proj2_addpre proj3_addpre proj4_addpre proj5_addpre
proj6_addpre proj7_addpre addpre_empty addpre_r
definition addpreRT :: "rt ⇒ ip ⇒ ip set ⇀ rt"
where "addpreRT rt dip npre ≡
map_option (λs. rt (dip ↦ addpre s npre)) (σ⇘route⇙(rt, dip))"
lemma snd_addpre [simp]:
"⋀dsn dsn' v pre. (dsn, snd(addpre (dsn', v) pre)) = addpre (dsn, v) pre"
unfolding addpre_def by clarsimp
lemma proj2_addpreRT [simp]:
fixes ip rt ip' npre
assumes "ip∈kD rt"
and "ip'∈kD rt"
shows "π⇩2(the (the (addpreRT rt ip' npre) ip)) = π⇩2(the (rt ip))"
using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp
lemma proj3_addpreRT [simp]:
fixes ip rt ip' npre
assumes "ip∈kD rt"
and "ip'∈kD rt"
shows "π⇩3(the (the (addpreRT rt ip' npre) ip)) = π⇩3(the (rt ip))"
using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp
lemma proj5_addpreRT [simp]:
"⋀rt dip ip npre. dip∈kD(rt) ⟹ π⇩5(the (the (addpreRT rt dip npre) ip)) = π⇩5(the (rt ip))"
unfolding addpreRT_def by auto
lemma flag_addpreRT [simp]:
fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "flag (the (addpreRT rt dip pre)) ip = flag rt ip"
unfolding addpreRT_def
using assms [THEN kD_Some] by (clarsimp)
lemma kD_addpreRT [simp]:
fixes rt dip npre
assumes "dip ∈ kD rt"
shows "kD (the (addpreRT rt dip npre)) = kD rt"
unfolding kD_def addpreRT_def
using assms [THEN kD_Some]
by clarsimp blast
lemma vD_addpreRT [simp]:
fixes rt dip npre
assumes "dip ∈ kD rt"
shows "vD (the (addpreRT rt dip npre)) = vD rt"
unfolding vD_def addpreRT_def
using assms [THEN kD_Some] by clarsimp auto
lemma iD_addpreRT [simp]:
fixes rt dip npre
assumes "dip ∈ kD rt"
shows "iD (the (addpreRT rt dip npre)) = iD rt"
unfolding iD_def addpreRT_def
using assms [THEN kD_Some] by clarsimp auto
lemma nhop_addpreRT [simp]:
fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "nhop (the (addpreRT rt dip pre)) ip = nhop rt ip"
unfolding sqn_def addpreRT_def
using assms [THEN kD_Some] by (clarsimp)
lemma sqn_addpreRT [simp]:
fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "sqn (the (addpreRT rt dip pre)) ip = sqn rt ip"
unfolding sqn_def addpreRT_def
using assms [THEN kD_Some] by (clarsimp)
lemma dhops_addpreRT [simp]:
fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "dhops (the (addpreRT rt dip pre)) ip = dhops rt ip"
unfolding addpreRT_def
using assms [THEN kD_Some] by (clarsimp)
lemma sqnf_addpreRT [simp]:
"⋀ip dip. ip∈kD(rt ξ) ⟹ sqnf (the (addpreRT (rt ξ) ip npre)) dip = sqnf (rt ξ) dip"
unfolding sqnf_def addpreRT_def by auto
subsubsection "Updating route entries"
lemma in_kD_case [simp]:
fixes dip rt
assumes "dip ∈ kD(rt)"
shows "(case rt dip of None ⇒ en | Some r ⇒ es r) = es (the (rt dip))"
using assms [THEN kD_Some] by auto
lemma not_in_kD_case [simp]:
fixes dip rt
assumes "dip ∉ kD(rt)"
shows "(case rt dip of None ⇒ en | Some r ⇒ es r) = en"
using assms [THEN kD_None] by auto
lemma rt_Some_sqn [dest]:
fixes rt and ip dsn dsk flag hops nhip pre
assumes "rt ip = Some (dsn, dsk, flag, hops, nhip, pre)"
shows "sqn rt ip = dsn"
unfolding sqn_def using assms by simp
lemma not_kD_sqn [simp]:
fixes dip rt
assumes "dip ∉ kD(rt)"
shows "sqn rt dip = 0"
using assms unfolding sqn_def
by simp
definition update_arg_wf :: "r ⇒ bool"
where "update_arg_wf r ≡ π⇩4(r) = val ∧
(π⇩2(r) = 0) = (π⇩3(r) = unk) ∧
(π⇩3(r) = unk ⟶ π⇩5(r) = 1)"
lemma update_arg_wf_gives_cases:
"⋀r. update_arg_wf r ⟹ (π⇩2(r) = 0) = (π⇩3(r) = unk)"
unfolding update_arg_wf_def by simp
lemma update_arg_wf_tuples [simp]:
"⋀nhip pre. update_arg_wf (0, unk, val, Suc 0, nhip, pre)"
"⋀n hops nhip pre. update_arg_wf (Suc n, kno, val, hops, nhip, pre)"
unfolding update_arg_wf_def by auto
lemma update_arg_wf_tuples' [elim]:
"⋀n hops nhip pre. Suc 0 ≤ n ⟹ update_arg_wf (n, kno, val, hops, nhip, pre)"
unfolding update_arg_wf_def by auto
lemma wf_r_cases [intro]:
fixes P r
assumes "update_arg_wf r"
and c1: "⋀nhip pre. P (0, unk, val, Suc 0, nhip, pre)"
and c2: "⋀dsn hops nhip pre. dsn > 0 ⟹ P (dsn, kno, val, hops, nhip, pre)"
shows "P r"
proof -
obtain dsn dsk flag hops nhip pre
where *: "r = (dsn, dsk, flag, hops, nhip, pre)" by (cases r)
with ‹update_arg_wf r› have wf1: "flag = val"
and wf2: "(dsn = 0) = (dsk = unk)"
and wf3: "dsk = unk ⟶ (hops = 1)"
unfolding update_arg_wf_def by auto
have "P (dsn, dsk, flag, hops, nhip, pre)"
proof (cases dsk)
assume "dsk = unk"
moreover with wf2 wf3 have "dsn = 0" and "hops = Suc 0" by auto
ultimately show ?thesis using ‹flag = val› by simp (rule c1)
next
assume "dsk = kno"
moreover with wf2 have "dsn > 0" by simp
ultimately show ?thesis using ‹flag = val› by simp (rule c2)
qed
with * show "P r" by simp
qed
definition update :: "rt ⇒ ip ⇒ r ⇒ rt"
where
"update rt ip r ≡
case σ⇘route⇙(rt, ip) of
None ⇒ rt (ip ↦ r)
| Some s ⇒
if π⇩2(s) < π⇩2(r) then rt (ip ↦ addpre r (π⇩7(s)))
else if π⇩2(s) = π⇩2(r) ∧ (π⇩5(s) > π⇩5(r) ∨ π⇩4(s) = inv)
then rt (ip ↦ addpre r (π⇩7(s)))
else if π⇩3(r) = unk
then rt (ip ↦ (π⇩2(s), snd (addpre r (π⇩7(s)))))
else rt (ip ↦ addpre s (π⇩7(r)))"
lemma update_simps [simp]:
fixes r s nrt nr nr' ns rt ip
defines "s ≡ the σ⇘route⇙(rt, ip)"
and "nr ≡ addpre r (π⇩7(s))"
and "nr' ≡ (π⇩2(s), π⇩3(nr), π⇩4(nr), π⇩5(nr), π⇩6(nr), π⇩7(nr))"
and "ns ≡ addpre s (π⇩7(r))"
shows
"⟦ip ∉ kD(rt)⟧ ⟹ update rt ip r = rt (ip ↦ r)"
"⟦ip ∈ kD(rt); sqn rt ip < π⇩2(r)⟧ ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r);
the (dhops rt ip) > π⇩5(r)⟧ ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r);
flag rt ip = Some inv⟧ ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); π⇩3(r) = unk; (π⇩2(r) = 0) = (π⇩3(r) = unk)⟧ ⟹ update rt ip r = rt (ip ↦ nr')"
"⟦ip ∈ kD(rt); sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val ⟧
⟹ update rt ip r = rt (ip ↦ ns)"
proof -
assume "ip∉kD(rt)"
hence "σ⇘route⇙(rt, ip) = None" ..
thus "update rt ip r = rt (ip ↦ r)"
unfolding update_def by simp
next
assume "ip ∈ kD(rt)"
and "sqn rt ip < π⇩2(r)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip < π⇩2(r)› show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "sqn rt ip = π⇩2(r)"
and "the (dhops rt ip) > π⇩5(r)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip = π⇩2(r)› and ‹the (dhops rt ip) > π⇩5(r)›
show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "sqn rt ip = π⇩2(r)"
and "flag rt ip = Some inv"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip = π⇩2(r)› and ‹flag rt ip = Some inv›
show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "π⇩3(r) = unk"
and "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹(π⇩2(r) = 0) = (π⇩3(r) = unk)› and ‹π⇩3(r) = unk›
show "update rt ip r = rt (ip ↦ nr')"
unfolding update_def nr'_def nr_def s_def
by (cases r) simp
next
assume "ip ∈ kD(rt)"
and otherassms: "sqn rt ip ≥ π⇩2(r)"
"π⇩3(r) = kno"
"sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with otherassms show "update rt ip r = rt (ip ↦ ns)"
unfolding update_def ns_def s_def by auto
qed
lemma update_cases [elim]:
assumes "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
and c1: "⟦ip ∉ kD(rt)⟧ ⟹ P (rt (ip ↦ r))"
and c2: "⟦ip ∈ kD(rt); sqn rt ip < π⇩2(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c3: "⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r); the (dhops rt ip) > π⇩5(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c4: "⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r); the (flag rt ip) = inv⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c5: "⟦ip ∈ kD(rt); π⇩3(r) = unk⟧
⟹ P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r),
π⇩4(r), π⇩5(r), π⇩6(r), π⇩7(addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))))"
and c6: "⟦ip ∈ kD(rt); sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val⟧
⟹ P (rt (ip ↦ addpre (the σ⇘route⇙(rt, ip)) (π⇩7(r))))"
shows "(P (update rt ip r))"
proof (cases "ip ∈ kD(rt)")
assume "ip ∉ kD(rt)"
with c1 show ?thesis
by simp
next
assume "ip ∈ kD(rt)"
moreover then obtain dsn dsk fl hops nhip pre
where rteq: "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
moreover obtain dsn' dsk' fl' hops' nhip' pre'
where req: "r = (dsn', dsk', fl', hops', nhip', pre')"
by (cases r) metis
ultimately show ?thesis
using ‹(π⇩2(r) = 0) = (π⇩3(r) = unk)›
c2 [OF ‹ip∈kD(rt)›]
c3 [OF ‹ip∈kD(rt)›]
c4 [OF ‹ip∈kD(rt)›]
c5 [OF ‹ip∈kD(rt)›]
c6 [OF ‹ip∈kD(rt)›]
unfolding update_def sqn_def by auto
qed
lemma update_cases_kD:
assumes "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
and "ip ∈ kD(rt)"
and c2: "sqn rt ip < π⇩2(r) ⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c3: "⟦sqn rt ip = π⇩2(r); the (dhops rt ip) > π⇩5(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c4: "⟦sqn rt ip = π⇩2(r); the (flag rt ip) = inv⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c5: "π⇩3(r) = unk ⟹ P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r),
π⇩4(r), π⇩5(r), π⇩6(r),
π⇩7(addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))))"
and c6: "⟦sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val⟧
⟹ P (rt (ip ↦ addpre (the σ⇘route⇙(rt, ip)) (π⇩7(r))))"
shows "(P (update rt ip r))"
using assms(1) proof (rule update_cases)
assume "sqn rt ip < π⇩2(r)"
thus "P (rt(ip ↦ addpre r (π⇩7(the (rt ip)))))" by (rule c2)
next
assume "sqn rt ip = π⇩2(r)"
and "the (dhops rt ip) > π⇩5(r)"
thus "P (rt(ip ↦ addpre r (π⇩7 (the (rt ip)))))"
by (rule c3)
next
assume "sqn rt ip = π⇩2(r)"
and "the (flag rt ip) = inv"
thus "P (rt(ip ↦ addpre r (π⇩7 (the (rt ip)))))"
by (rule c4)
next
assume "π⇩3(r) = unk"
thus "P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r), π⇩4(r), π⇩5(r), π⇩6(r),
π⇩7(addpre r (π⇩7(the (rt ip)))))))"
by (rule c5)
next
assume "sqn rt ip ≥ π⇩2(r)"
and "π⇩3(r) = kno"
and "sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val"
thus "P (rt (ip ↦ addpre (the (rt ip)) (π⇩7(r))))"
by (rule c6)
qed (simp add: ‹ip ∈ kD(rt)›)
lemma in_kD_after_update [simp]:
fixes rt nip dsn dsk flag hops nhip pre
shows "kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)"
unfolding update_def
by (cases "rt nip") auto
lemma nhop_of_update [simp]:
fixes rt dip dsn dsk flag hops nhip
assumes "rt ≠ update rt dip (dsn, dsk, flag, hops, nhip, {})"
shows "the (nhop (update rt dip (dsn, dsk, flag, hops, nhip, {})) dip) = nhip"
proof -
from assms
have update_neq: "⋀v. rt dip = Some v ⟹
update rt dip (dsn, dsk, flag, hops, nhip, {})
≠ rt(dip ↦ addpre (the (rt dip)) (π⇩7 (dsn, dsk, flag, hops, nhip, {})))"
by auto
show ?thesis
proof (cases "rt dip = None")
assume "rt dip = None"
thus "?thesis" unfolding update_def by clarsimp
next
assume "rt dip ≠ None"
then obtain v where "rt dip = Some v" by (metis not_None_eq)
with update_neq [OF this] show ?thesis
unfolding update_def by auto
qed
qed
lemma sqn_if_updated:
fixes rip v rt ip
shows "sqn (λx. if x = rip then Some v else rt x) ip
= (if ip = rip then π⇩2(v) else sqn rt ip)"
unfolding sqn_def by simp
lemma update_sqn [simp]:
fixes rt dip rip dsn dsk hops nhip pre
assumes "(dsn = 0) = (dsk = unk)"
shows "sqn rt dip ≤ sqn (update rt rip (dsn, dsk, val, hops, nhip, pre)) dip"
proof (rule update_cases)
show "(π⇩2 (dsn, dsk, val, hops, nhip, pre) = 0) = (π⇩3 (dsn, dsk, val, hops, nhip, pre) = unk)"
by simp (rule assms)
qed (clarsimp simp: sqn_if_updated sqn_def)+
lemma sqn_update_bigger [simp]:
fixes rt ip ip' dsn dsk flag hops nhip pre
assumes "1 ≤ hops"
shows "sqn rt ip ≤ sqn (update rt ip' (dsn, dsk, flag, hops, nhip, pre)) ip"
using assms unfolding update_def sqn_def
by (clarsimp split: option.split) auto
lemma dhops_update [intro]:
fixes rt dsn dsk flag hops ip rip nhip pre
assumes ex: "∀ip∈kD rt. the (dhops rt ip) ≥ 1"
and ip: "(ip = rip ∧ Suc 0 ≤ hops) ∨ (ip ≠ rip ∧ ip∈kD rt)"
shows "Suc 0 ≤ the (dhops (update rt rip (dsn, dsk, flag, hops, nhip, pre)) ip)"
using ip proof
assume "ip = rip ∧ Suc 0 ≤ hops" thus ?thesis
unfolding update_def using ex
by (cases "rip ∈ kD rt") (drule(1) bspec, auto)
next
assume "ip ≠ rip ∧ ip∈kD rt" thus ?thesis
using ex unfolding update_def
by (cases "rip∈kD rt") auto
qed
lemma update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "(update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)
lemma nhop_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "nhop (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = nhop rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)
lemma dhops_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "dhops (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = dhops rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)
lemma sqn_update_same [simp]:
"⋀rt ip dsn dsk flag hops nhip pre. sqn (rt(ip ↦ v)) ip = π⇩2(v)"
unfolding sqn_def by simp
lemma dhops_update_changed [simp]:
fixes rt dip osn hops nhip
assumes "rt ≠ update rt dip (osn, kno, val, hops, nhip, {})"
shows "the (dhops (update rt dip (osn, kno, val, hops, nhip, {})) dip) = hops"
using assms unfolding update_def
by (clarsimp split: option.split_asm option.split if_split_asm) auto
lemma nhop_update_unk_val [simp]:
"⋀rt dip ip dsn hops npre.
the (nhop (update rt dip (dsn, unk, val, hops, ip, npre)) dip) = ip"
unfolding update_def by (clarsimp split: option.split)
lemma nhop_update_changed [simp]:
fixes rt dip dsn dsk flg hops sip
assumes "update rt dip (dsn, dsk, flg, hops, sip, {}) ≠ rt"
shows "the (nhop (update rt dip (dsn, dsk, flg, hops, sip, {})) dip) = sip"
using assms unfolding update_def
by (clarsimp split: option.splits if_split_asm) auto
lemma update_rt_split_asm:
"⋀rt ip dsn dsk flag hops sip.
P (update rt ip (dsn, dsk, flag, hops, sip, {}))
=
(¬(rt = update rt ip (dsn, dsk, flag, hops, sip, {}) ∧ ¬P rt
∨ rt ≠ update rt ip (dsn, dsk, flag, hops, sip, {})
∧ ¬P (update rt ip (dsn, dsk, flag, hops, sip, {}))))"
by auto
lemma sqn_update [simp]: "⋀rt dip dsn flg hops sip.
rt ≠ update rt dip (dsn, kno, flg, hops, sip, {})
⟹ sqn (update rt dip (dsn, kno, flg, hops, sip, {})) dip = dsn"
unfolding update_def by (clarsimp split: option.split if_split_asm) auto
lemma sqnf_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ sqnf (update rt dip (dsn, dsk, flg, hops, sip, {})) dip = dsk"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto
lemma update_kno_dsn_greater_zero:
"⋀rt dip ip dsn hops npre. 1 ≤ dsn ⟹ 1 ≤ (sqn (update rt dip (dsn, kno, val, hops, ip, npre)) dip)"
unfolding update_def
by (clarsimp split: option.splits)
lemma proj3_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ π⇩3(the (update rt dip (dsn, dsk, flg, hops, sip, {}) dip)) = dsk"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto
lemma nhop_update_changed_kno_val [simp]: "⋀rt ip dsn dsk hops nhip.
rt ≠ update rt ip (dsn, kno, val, hops, nhip, {})
⟹ the (nhop (update rt ip (dsn, kno, val, hops, nhip, {})) ip) = nhip"
unfolding update_def
by (clarsimp split: option.split_asm option.split if_split_asm) auto
lemma flag_update [simp]: "⋀rt dip dsn flg hops sip.
rt ≠ update rt dip (dsn, kno, flg, hops, sip, {})
⟹ the (flag (update rt dip (dsn, kno, flg, hops, sip, {})) dip) = flg"
unfolding update_def
by (clarsimp split: option.split if_split_asm) auto
lemma the_flag_Some [dest!]:
fixes ip rt
assumes "the (flag rt ip) = x"
and "ip ∈ kD rt"
shows "flag rt ip = Some x"
using assms by auto
lemma kD_update_unchanged [dest]:
fixes rt dip dsn dsk flag hops nhip pre
assumes "rt = update rt dip (dsn, dsk, flag, hops, nhip, pre)"
shows "dip∈kD(rt)"
proof -
have "dip∈kD(update rt dip (dsn, dsk, flag, hops, nhip, pre))" by simp
with assms show ?thesis by simp
qed
lemma nhop_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ the (nhop (update rt dip (dsn, dsk, flg, hops, sip, {})) dip) = sip"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto
lemma sqn_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "sqn (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = sqn rt ip"
using assms unfolding update_def sqn_def
by (clarsimp split: option.splits) auto
lemma sqnf_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "sqnf (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = sqnf rt ip"
using assms unfolding update_def sqnf_def
by (clarsimp split: option.splits) auto
lemma vD_update_val [dest]:
"⋀dip rt dip' dsn dsk hops nhip pre.
dip ∈ vD(update rt dip' (dsn, dsk, val, hops, nhip, pre)) ⟹ (dip∈vD(rt) ∨ dip=dip')"
unfolding update_def vD_def by (clarsimp split: option.split_asm if_split_asm)
subsubsection "Invalidating route entries"
definition invalidate :: "rt ⇒ (ip ⇀ sqn) ⇒ rt"
where "invalidate rt dests ≡
λip. case (rt ip, dests ip) of
(None, _) ⇒ None
| (Some s, None) ⇒ Some s
| (Some (_, dsk, _, hops, nhip, pre), Some rsn) ⇒
Some (rsn, dsk, inv, hops, nhip, pre)"
lemma proj3_invalidate [simp]:
"⋀dip. π⇩3(the ((invalidate rt dests) dip)) = π⇩3(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)
lemma proj5_invalidate [simp]:
"⋀dip. π⇩5(the ((invalidate rt dests) dip)) = π⇩5(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)
lemma proj6_invalidate [simp]:
"⋀dip. π⇩6(the ((invalidate rt dests) dip)) = π⇩6(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)
lemma proj7_invalidate [simp]:
"⋀dip. π⇩7(the ((invalidate rt dests) dip)) = π⇩7(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)
lemma invalidate_kD_inv [simp]:
"⋀rt dests. kD (invalidate rt dests) = kD rt"
unfolding invalidate_def kD_def
by (simp split: option.split)
lemma invalidate_sqn:
fixes rt dip dests
assumes "∀rsn. dests dip = Some rsn ⟶ sqn rt dip ≤ rsn"
shows "sqn rt dip ≤ sqn (invalidate rt dests) dip"
proof (cases "dip ∉ kD(rt)")
assume "¬ dip ∉ kD(rt)"
hence "dip∈kD(rt)" by simp
then obtain dsn dsk flag hops nhip pre where "rt dip = Some (dsn, dsk, flag, hops, nhip, pre)"
by (metis kD_Some)
with assms show "sqn rt dip ≤ sqn (invalidate rt dests) dip"
by (cases "dests dip") (auto simp add: invalidate_def sqn_def)
qed simp
lemma sqn_invalidate_in_dests [simp]:
fixes dests ipa rsn rt
assumes "dests ipa = Some rsn"
and "ipa∈kD(rt)"
shows "sqn (invalidate rt dests) ipa = rsn"
unfolding invalidate_def sqn_def
using assms(1) assms(2) [THEN kD_Some]
by clarsimp
lemma dhops_invalidate [simp]:
"⋀dip. the (dhops (invalidate rt dests) dip) = the (dhops rt dip)"
unfolding invalidate_def by (clarsimp split: option.split)
lemma sqnf_invalidate [simp]:
"⋀dip. sqnf (invalidate (rt ξ) (dests ξ)) dip = sqnf (rt ξ) dip"
unfolding sqnf_def invalidate_def by (clarsimp split: option.split)
lemma nhop_invalidate [simp]:
"⋀dip. the (nhop (invalidate (rt ξ) (dests ξ)) dip) = the (nhop (rt ξ) dip)"
unfolding invalidate_def by (clarsimp split: option.split)
lemma invalidate_other [simp]:
fixes rt dests dip
assumes "dip∉dom(dests)"
shows "invalidate rt dests dip = rt dip"
using assms unfolding invalidate_def
by (clarsimp split: option.split_asm)
lemma invalidate_none [simp]:
fixes rt dests dip
assumes "dip∉kD(rt)"
shows "invalidate rt dests dip = None"
using assms unfolding invalidate_def by clarsimp
lemma vD_invalidate_vD_not_dests:
"⋀dip rt dests. dip∈vD(invalidate rt dests) ⟹ dip∈vD(rt) ∧ dests dip = None"
unfolding invalidate_def vD_def
by (clarsimp split: option.split_asm)
lemma sqn_invalidate_not_in_dests [simp]:
fixes dests dip rt
assumes "dip∉dom(dests)"
shows "sqn (invalidate rt dests) dip = sqn rt dip"
using assms unfolding sqn_def by simp
lemma invalidate_changes:
fixes rt dests dip dsn dsk flag hops nhip pre
assumes "invalidate rt dests dip = Some (dsn, dsk, flag, hops, nhip, pre)"
shows " dsn = (case dests dip of None ⇒ π⇩2(the (rt dip)) | Some rsn ⇒ rsn)
∧ dsk = π⇩3(the (rt dip))
∧ flag = (if dests dip = None then π⇩4(the (rt dip)) else inv)
∧ hops = π⇩5(the (rt dip))
∧ nhip = π⇩6(the (rt dip))
∧ pre = π⇩7(the (rt dip))"
using assms unfolding invalidate_def
by (cases "rt dip", clarsimp, cases "dests dip") auto
lemma proj3_inv: "⋀dip rt dests. dip∈kD (rt)
⟹ π⇩3(the (invalidate rt dests dip)) = π⇩3(the (rt dip))"
by (clarsimp simp: invalidate_def kD_def split: option.split)
lemma dests_iD_invalidate [simp]:
assumes "dests ip = Some rsn"
and "ip∈kD(rt)"
shows "ip∈iD(invalidate rt dests)"
using assms(1) assms(2) [THEN kD_Some] unfolding invalidate_def iD_def
by (clarsimp split: option.split)
subsection "Route Requests"
text ‹Generate a fresh route request identifier.›
definition nrreqid :: "(ip × rreqid) set ⇒ ip ⇒ rreqid"
where "nrreqid rreqs ip ≡ Max ({n. (ip, n) ∈ rreqs} ∪ {0}) + 1"
subsection "Queued Packets"
text ‹Functions for sending data packets.›
type_synonym store = "ip ⇀ (p × data list)"
definition sigma_queue :: "store ⇒ ip ⇒ data list" ("σ⇘queue⇙'(_, _')")
where "σ⇘queue⇙(store, dip) ≡ case store dip of None ⇒ [] | Some (p, q) ⇒ q"
definition qD :: "store ⇒ ip set"
where "qD ≡ dom"
definition add :: "data ⇒ ip ⇒ store ⇒ store"
where "add d dip store ≡ case store dip of
None ⇒ store (dip ↦ (req, [d]))
| Some (p, q) ⇒ store (dip ↦ (p, q @ [d]))"
lemma qD_add [simp]:
fixes d dip store
shows "qD(add d dip store) = insert dip (qD store)"
unfolding add_def Let_def qD_def
by (clarsimp split: option.split)
definition drop :: "ip ⇒ store ⇀ store"
where "drop dip store ≡
map_option (λ(p, q). if tl q = [] then store (dip := None)
else store (dip ↦ (p, tl q))) (store dip)"
definition sigma_p_flag :: "store ⇒ ip ⇀ p" ("σ⇘p-flag⇙'(_, _')")
where "σ⇘p-flag⇙(store, dip) ≡ map_option fst (store dip)"
definition unsetRRF :: "store ⇒ ip ⇒ store"
where "unsetRRF store dip ≡ case store dip of
None ⇒ store
| Some (p, q) ⇒ store (dip ↦ (noreq, q))"
definition setRRF :: "store ⇒ (ip ⇀ sqn) ⇒ store"
where "setRRF store dests ≡ λdip. if dests dip = None then store dip
else map_option (λ(_, q). (req, q)) (store dip)"
subsection "Comparison with the original technical report"
text ‹
The major differences with the AODV technical report of Fehnker et al are:
\begin{enumerate}
\item @{term nhop} is partial, thus a `@{term the}' is needed, similarly for @{term dhops}
and @{term addpreRT}.
\item @{term precs} is partial.
\item @{term "σ⇘p-flag⇙(store, dip)"} is partial.
\item The routing table (@{typ rt}) is modelled as a map (@{typ "ip ⇒ r option"})
rather than a set of 7-tuples, likewise, the @{typ r} is a 6-tuple rather than
a 7-tuple, i.e., the destination ip-address (@{term "dip"}) is taken from the
argument to the function, rather than a part of the result. Well-definedness then
follows from the structure of the type and more related facts are available
automatically, rather than having to be acquired through tedious proofs.
\item Similar remarks hold for the dests mapping passed to @{term "invalidate"},
and @{term "store"}.
\end{enumerate}
›
end