# Theory Aodv_Loop_Freedom

```(*  Title:       Aodv_Loop_Freedom.thy
Author:      Timothy Bourke, Inria
*)

section "Lift and transfer invariants to show loop freedom"

theory Aodv_Loop_Freedom
imports AWN.OClosed_Transfer AWN.Qmsg_Lifting Global_Invariants Loop_Freedom
begin

subsection ‹Lift to parallel processes with queues›

fixes σ s a σ' s'
assumes "((σ, s), a, (σ', s')) ∈ oparp_sos i (oseqp_sos Γ⇩A⇩O⇩D⇩V i) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
and "a ≠ τ"
shows "σ' i = σ i"

lemma par_nhop_quality_increases:
shows "opaodv i ⟨⟨⇘i⇙ qmsg ⊨ (otherwith ((=)) {i} (orecvmsg (λσ m.
msg_fresh σ m ∧ msg_zhops m)),
other quality_increases {i} →)
global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
proof (rule lift_into_qmsg [OF seq_nhop_quality_increases])
show "opaodv i ⊨⇩A (otherwith ((=)) {i}
(orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
other quality_increases {i} →)
globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
proof (rule ostep_invariant_weakenE [OF oquality_increases], simp_all)
fix t :: "(((nat ⇒ state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
assume "onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), _, (σ', _)). ∀j. quality_increases (σ j) (σ' j)) t"
thus "quality_increases (fst (fst t) i) (fst (snd (snd t)) i)"
by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
next
fix σ σ' a
assume "otherwith ((=)) {i}
(orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)) σ σ' a"
thus "otherwith quality_increases {i} (orecvmsg (λ_. rreq_rrep_sn)) σ σ' a"
by - (erule weaken_otherwith, auto)
qed
qed auto

lemma par_rreq_rrep_sn_quality_increases:
"opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
proof -
have "opaodv i ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
by (rule ostep_invariant_weakenE [OF olocal_quality_increases])
(auto dest!: onllD seqllD elim!: aodv_ex_labelE)
hence "opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
by (rule lift_step_into_qmsg_statelessassm) simp_all
thus ?thesis by rule auto
qed

lemma par_rreq_rrep_nsqn_fresh_any_step:
shows "opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ,
other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
proof -
have "opaodv i ⊨⇩A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
proof (rule ostep_invariant_weakenE [OF rreq_rrep_nsqn_fresh_any_step_invariant])
fix t
assume "onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), a, _). anycast (msg_fresh σ) a) t"
thus "globala (λ(σ, a, σ'). anycast (msg_fresh σ) a) t"
by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
qed auto
hence "opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
by (rule lift_step_into_qmsg_statelessassm) simp_all
thus ?thesis by rule auto
qed

lemma par_anycast_msg_zhops:
shows "opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(_, a, _). anycast msg_zhops a)"
proof -
from anycast_msg_zhops initiali_aodv oaodv_trans aodv_trans
have "opaodv i ⊨⇩A (act TT, other (λ_ _. True) {i} →)
seqll i (onll Γ⇩A⇩O⇩D⇩V (λ(_, a, _). anycast msg_zhops a))"
by (rule open_seq_step_invariant)
hence "opaodv i ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(_, a, _). anycast msg_zhops a)"
proof (rule ostep_invariant_weakenE)
fix t :: "(((nat ⇒ state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
assume "seqll i (onll Γ⇩A⇩O⇩D⇩V (λ(_, a, _). anycast msg_zhops a)) t"
thus "globala (λ(_, a, _). anycast msg_zhops a) t"
by (cases t) (clarsimp dest!: seqllD onllD, metis aodv_ex_label)
qed simp_all
hence "opaodv i ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(_, a, _). anycast msg_zhops a)"
by (rule lift_step_into_qmsg_statelessassm) simp_all
thus ?thesis by rule auto
qed

subsection ‹Lift to nodes›

assumes "((σ, NodeS i P R), a, (σ', NodeS i' P' R')) ∈ onode_sos
(oparp_sos i (oseqp_sos Γ⇩A⇩O⇩D⇩V i) (seqp_sos Γ⇩Q⇩M⇩S⇩G))"
and "a ≠ τ"
shows "σ' i = σ i"
using assms
by (cases a) (auto elim!: par_step_no_change_on_send_or_receive)

lemma node_nhop_quality_increases:
shows "⟨ i : opaodv i ⟨⟨⇘i⇙ qmsg : R ⟩⇩o ⊨
(otherwith ((=)) {i}
(oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
other quality_increases {i}
→) global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
by (rule node_lift [OF par_nhop_quality_increases]) auto

lemma node_quality_increases:
"⟨ i : opaodv i ⟨⟨⇘i⇙ qmsg : R ⟩⇩o ⊨⇩A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
by (rule node_lift_step_statelessassm [OF par_rreq_rrep_sn_quality_increases]) simp

lemma node_rreq_rrep_nsqn_fresh_any_step:
shows "⟨ i : opaodv i ⟨⟨⇘i⇙ qmsg : R ⟩⇩o ⊨⇩A
(λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). castmsg (msg_fresh σ) a)"
by (rule node_lift_anycast_statelessassm [OF par_rreq_rrep_nsqn_fresh_any_step])

lemma node_anycast_msg_zhops:
shows "⟨ i : opaodv i ⟨⟨⇘i⇙ qmsg : R ⟩⇩o ⊨⇩A
(λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
globala (λ(_, a, _). castmsg msg_zhops a)"
by (rule node_lift_anycast_statelessassm [OF par_anycast_msg_zhops])

lemma node_silent_change_only:
shows "⟨ i : opaodv i ⟨⟨⇘i⇙ qmsg : R⇩i ⟩⇩o ⊨⇩A (λσ _. oarrivemsg (λ_ _. True) σ,
other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). a ≠ τ ⟶ σ' i = σ i)"
proof (rule ostep_invariantI, simp (no_asm), rule impI)
fix σ ζ a σ' ζ'
assume or: "(σ, ζ) ∈ oreachable (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o)
(λσ _. oarrivemsg (λ_ _. True) σ)
(other (λ_ _. True) {i})"
and tr: "((σ, ζ), a, (σ', ζ')) ∈ trans (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o)"
and "a ≠ τ⇩n"
from or obtain p R where "ζ = NodeS i p R"
by - (drule node_net_state, metis)
with tr have "((σ, NodeS i p R), a, (σ', ζ'))
∈ onode_sos (oparp_sos i (trans (opaodv i)) (trans qmsg))"
by simp
thus "σ' i = σ i" using ‹a ≠ τ⇩n›
by (cases rule: onode_sos.cases)
qed

subsection ‹Lift to partial networks›

lemma arrive_rreq_rrep_nsqn_fresh_inc_sn [simp]:
assumes "oarrivemsg (λσ m. msg_fresh σ m ∧ P σ m) σ m"
shows "oarrivemsg (λ_. rreq_rrep_sn) σ m"
using assms by (cases m) auto

lemma opnet_nhop_quality_increases:
shows "opnet (λi. opaodv i ⟨⟨⇘i⇙ qmsg) p ⊨
(otherwith ((=)) (net_tree_ips p)
(oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
other quality_increases (net_tree_ips p) →)
global (λσ. ∀i∈net_tree_ips p. ∀dip.
let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
proof (rule pnet_lift [OF node_nhop_quality_increases])
fix i R
have "⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
other (λ_ _. True) {i} →) globala (λ(σ, a, σ').
castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a)"
proof (rule ostep_invariantI, simp (no_asm))
fix σ s a σ' s'
assume or: "(σ, s) ∈ oreachable (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o)
(λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ)
(other (λ_ _. True) {i})"
and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o)"
and am: "oarrivemsg (λ_. rreq_rrep_sn) σ a"
from or tr am have "castmsg (msg_fresh σ) a"
by (auto dest!: ostep_invariantD [OF node_rreq_rrep_nsqn_fresh_any_step])
moreover from or tr am have "castmsg (msg_zhops) a"
by (auto dest!: ostep_invariantD [OF node_anycast_msg_zhops])
ultimately show "castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a"
by (case_tac a) auto
qed
thus "⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩A
(λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
other quality_increases {i} →) globala (λ(σ, a, _).
castmsg (λm. msg_fresh σ m ∧ msg_zhops m) a)"
by rule auto
next
fix i R
show "⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩A
(λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
other quality_increases {i} →) globala (λ(σ, a, σ').
a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ σ i = σ' i)"
by (rule ostep_invariant_weakenE [OF node_silent_change_only]) auto
next
fix i R
show "⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩A
(λσ _. oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ,
other quality_increases {i} →) globala (λ(σ, a, σ').
a = τ ∨ (∃d. a = i:deliver(d)) ⟶ quality_increases (σ i) (σ' i))"
by (rule ostep_invariant_weakenE [OF node_quality_increases]) auto
qed simp_all

subsection ‹Lift to closed networks›

lemma onet_nhop_quality_increases:
shows "oclosed (opnet (λi. opaodv i ⟨⟨⇘i⇙ qmsg) p)
⊨ (λ_ _ _. True, other quality_increases (net_tree_ips p) →)
global (λσ. ∀i∈net_tree_ips p. ∀dip.
let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
(is "_ ⊨ (_, ?U →) ?inv")
proof (rule inclosed_closed)
from opnet_nhop_quality_increases
show "opnet (λi. opaodv i ⟨⟨⇘i⇙ qmsg) p
⊨ (otherwith ((=)) (net_tree_ips p) inoclosed, ?U →) ?inv"
proof (rule oinvariant_weakenE)
fix σ σ' :: "ip ⇒ state" and a :: "msg node_action"
assume "otherwith ((=)) (net_tree_ips p) inoclosed σ σ' a"
thus "otherwith ((=)) (net_tree_ips p)
(oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)) σ σ' a"
proof (rule otherwithEI)
fix σ :: "ip ⇒ state" and a :: "msg node_action"
assume "inoclosed σ a"
thus "oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m) σ a"
proof (cases a)
fix ii ni ms
assume "a = ii¬ni:arrive(ms)"
moreover with ‹inoclosed σ a› obtain d di where "ms = newpkt(d, di)"
by (cases ms) auto
ultimately show ?thesis by simp
qed simp_all
qed
qed
qed

subsection ‹Transfer into the standard model›

interpretation aodv_openproc: openproc paodv opaodv id
rewrites "aodv_openproc.initmissing = initmissing"
proof -
show "openproc paodv opaodv id"
proof unfold_locales
fix i :: ip
have "{(σ, ζ). (σ i, ζ) ∈ σ⇩A⇩O⇩D⇩V i ∧ (∀j. j ≠ i ⟶ σ j ∈ fst ` σ⇩A⇩O⇩D⇩V j)} ⊆ σ⇩A⇩O⇩D⇩V'"
unfolding σ⇩A⇩O⇩D⇩V_def σ⇩A⇩O⇩D⇩V'_def
proof (rule equalityD1)
show "⋀f p. {(σ, ζ). (σ i, ζ) ∈ {(f i, p)} ∧ (∀j. j ≠ i
⟶ σ j ∈ fst ` {(f j, p)})} = {(f, p)}"
by (rule set_eqI) auto
qed
thus "{ (σ, ζ) |σ ζ s. s ∈ init (paodv i)
∧ (σ i, ζ) = id s
∧ (∀j. j≠i ⟶ σ j ∈ (fst o id) ` init (paodv j)) } ⊆ init (opaodv i)"
by simp
next
show "∀j. init (paodv j) ≠ {}"
unfolding σ⇩A⇩O⇩D⇩V_def by simp
next
fix i s a s' σ σ'
assume "σ i = fst (id s)"
and "σ' i = fst (id s')"
and "(s, a, s') ∈ trans (paodv i)"
then obtain q q' where "s = (σ i, q)"
and "s' = (σ' i, q')"
and "((σ i, q), a, (σ' i, q')) ∈ trans (paodv i)"
by (cases s, cases s') auto
from this(3) have "((σ, q), a, (σ', q')) ∈ trans (opaodv i)"
by simp (rule open_seqp_action [OF aodv_wf])

with ‹s = (σ i, q)› and ‹s' = (σ' i, q')›
show "((σ, snd (id s)), a, (σ', snd (id s'))) ∈ trans (opaodv i)"
by simp
qed
then interpret opn: openproc paodv opaodv id .
have [simp]: "⋀i. (SOME x. x ∈ (fst o id) ` init (paodv i)) = aodv_init i"
unfolding σ⇩A⇩O⇩D⇩V_def by simp
hence "⋀i. openproc.initmissing paodv id i = initmissing i"
unfolding opn.initmissing_def opn.someinit_def initmissing_def
by (auto split: option.split)
thus "openproc.initmissing paodv id = initmissing" ..
qed

interpretation aodv_openproc_par_qmsg: openproc_parq paodv opaodv id qmsg
rewrites "aodv_openproc_par_qmsg.netglobal = netglobal"
and "aodv_openproc_par_qmsg.initmissing = initmissing"
proof -
show "openproc_parq paodv opaodv id qmsg"
by (unfold_locales) simp
then interpret opq: openproc_parq paodv opaodv id qmsg .

have im: "⋀σ. openproc.initmissing (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) σ
= initmissing σ"
unfolding opq.initmissing_def opq.someinit_def initmissing_def
unfolding σ⇩A⇩O⇩D⇩V_def σ⇩Q⇩M⇩S⇩G_def by (clarsimp cong: option.case_cong)
thus "openproc.initmissing (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) = initmissing"
by (rule ext)
have "⋀P σ. openproc.netglobal (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) P σ
= netglobal P σ"
unfolding opq.netglobal_def netglobal_def opq.initmissing_def initmissing_def opq.someinit_def
unfolding σ⇩A⇩O⇩D⇩V_def σ⇩Q⇩M⇩S⇩G_def
by (clarsimp cong: option.case_cong
simp del: One_nat_def
[symmetric, unfolded initmissing_def])
thus "openproc.netglobal (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) = netglobal"
by auto
qed

lemma net_nhop_quality_increases:
assumes "wf_net_tree n"
shows "closed (pnet (λi. paodv i ⟨⟨ qmsg) n) ⊫ netglobal
(λσ. ∀i dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
(is "_ ⊫ netglobal (λσ. ∀i. ?inv σ i)")
proof -
from ‹wf_net_tree n›
have proto: "closed (pnet (λi. paodv i ⟨⟨ qmsg) n) ⊫ netglobal (λσ. ∀i∈net_tree_ips n. ∀dip.
let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
by (rule aodv_openproc_par_qmsg.close_opnet [OF _ onet_nhop_quality_increases])
show ?thesis
unfolding invariant_def opnet_sos.opnet_tau1
proof (rule, simp only: aodv_openproc_par_qmsg.netglobalsimp
fst_initmissing_netgmap_pair_fst, rule allI)
fix σ i
assume sr: "σ ∈ reachable (closed (pnet (λi. paodv i ⟨⟨ qmsg) n)) TT"
hence "∀i∈net_tree_ips n. ?inv (fst (initmissing (netgmap fst σ))) i"
by - (drule invariantD [OF proto],
simp only: aodv_openproc_par_qmsg.netglobalsimp
fst_initmissing_netgmap_pair_fst)
thus "?inv (fst (initmissing (netgmap fst σ))) i"
proof (cases "i∈net_tree_ips n")
assume "i∉net_tree_ips n"
from sr have "σ ∈ reachable (pnet (λi. paodv i ⟨⟨ qmsg) n) TT" ..
hence "net_ips σ = net_tree_ips n" ..
with ‹i∉net_tree_ips n› have "i∉net_ips σ" by simp
hence "(fst (initmissing (netgmap fst σ))) i = aodv_init i"
by simp
thus ?thesis by simp
qed metis
qed
qed

subsection ‹Loop freedom of AODV›

theorem aodv_loop_freedom:
assumes "wf_net_tree n"
shows "closed (pnet (λi. paodv i ⟨⟨ qmsg) n) ⊫ netglobal (λσ. ∀dip. irrefl ((rt_graph σ dip)⇧+))"
using assms by (rule aodv_openproc_par_qmsg.netglobal_weakenE
[OF net_nhop_quality_increases inv_to_loop_freedom])

end
```