Theory D_Seq_Invariants
section "Invariant proofs on individual processes"
theory D_Seq_Invariants
imports AWN.Invariants D_Aodv D_Aodv_Data D_Aodv_Predicates D_Fresher
begin
text ‹
The proposition numbers are taken from the December 2013 version of
the Fehnker et al technical report.
›
text ‹Proposition 7.2›
lemma sequence_number_increases:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). sn ξ ≤ sn ξ')"
by inv_cterms
lemma sequence_number_one_or_bigger:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _). 1 ≤ sn ξ)"
by (rule onll_step_to_invariantI [OF sequence_number_increases])
(auto simp: σ⇩A⇩O⇩D⇩V_def)
text ‹We can get rid of the onl/onll if desired...›
lemma sequence_number_increases':
"paodv i ⊫⇩A (λ((ξ, _), _, (ξ', _)). sn ξ ≤ sn ξ')"
by (rule step_invariant_weakenE [OF sequence_number_increases]) (auto dest!: onllD)
lemma sequence_number_one_or_bigger':
"paodv i ⊫ (λ(ξ, _). 1 ≤ sn ξ)"
by (rule invariant_weakenE [OF sequence_number_one_or_bigger]) auto
lemma sip_in_kD:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). l ∈ ({PAodv-:7} ∪ {PAodv-:5} ∪ {PRrep-:0..PRrep-:1}
∪ {PRreq-:0..PRreq-:3}) ⟶ sip ξ ∈ kD (rt ξ))"
by inv_cterms
lemma rrep_1_update_changes:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l = PRrep-:1 ⟶
rt ξ ≠ update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {})))"
by inv_cterms
lemma addpreRT_partly_welldefined:
"paodv i ⊫
onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PRreq-:18..PRreq-:20} ∪ {PRrep-:2..PRrep-:6} ⟶ dip ξ ∈ kD (rt ξ))
∧ (l ∈ {PRreq-:3..PRreq-:19} ⟶ oip ξ ∈ kD (rt ξ)))"
by inv_cterms
text ‹Proposition 7.38›
lemma includes_nhip:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). ∀dip∈kD(rt ξ). the (nhop (rt ξ) dip)∈kD(rt ξ))"
proof -
{ fix ip and ξ ξ' :: state
assume "∀dip∈kD (rt ξ). the (nhop (rt ξ) dip) ∈ kD (rt ξ)"
and "ξ' = ξ⦇rt := update (rt ξ) ip (0, unk, val, Suc 0, ip, {})⦈"
hence "∀dip∈kD (rt ξ).
the (nhop (update (rt ξ) ip (0, unk, val, Suc 0, ip, {})) dip) = ip
∨ the (nhop (update (rt ξ) ip (0, unk, val, Suc 0, ip, {})) dip) ∈ kD (rt ξ)"
by clarsimp (metis nhop_update_unk_val update_another)
} note one_hop = this
{ fix ip sip sn hops and ξ ξ' :: state
assume "∀dip∈kD (rt ξ). the (nhop (rt ξ) dip) ∈ kD (rt ξ)"
and "ξ' = ξ⦇rt := update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})⦈"
and "sip ∈ kD (rt ξ)"
hence "(the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) ip) = ip
∨ the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) ip) ∈ kD (rt ξ))
∧ (∀dip∈kD (rt ξ).
the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) dip) = ip
∨ the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) dip) ∈ kD (rt ξ))"
by (metis kD_update_unchanged nhop_update_changed update_another)
} note nhip_is_sip = this
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf sip_in_kD]
onl_invariant_sterms [OF aodv_wf addpreRT_partly_welldefined]
solve: one_hop nhip_is_sip)
qed
text ‹Proposition 7.22: needed in Proposition 7.4›
lemma addpreRT_welldefined:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PRreq-:18..PRreq-:20} ⟶ dip ξ ∈ kD (rt ξ)) ∧
(l = PRreq-:19 ⟶ oip ξ ∈ kD (rt ξ)) ∧
(l = PRrep-:5 ⟶ dip ξ ∈ kD (rt ξ)) ∧
(l = PRrep-:6 ⟶ (the (nhop (rt ξ) (dip ξ))) ∈ kD (rt ξ)))"
(is "_ ⊫ onl Γ⇩A⇩O⇩D⇩V ?P")
unfolding invariant_def
proof
fix s
assume "s ∈ reachable (paodv i) TT"
then obtain ξ p where "s = (ξ, p)"
and "(ξ, p) ∈ reachable (paodv i) TT"
by (metis prod.exhaust)
have "onl Γ⇩A⇩O⇩D⇩V ?P (ξ, p)"
proof (rule onlI)
fix l
assume "l ∈ labels Γ⇩A⇩O⇩D⇩V p"
with ‹(ξ, p) ∈ reachable (paodv i) TT›
have I1: "l ∈ {PRreq-:18..PRreq-:20} ⟶ dip ξ ∈ kD(rt ξ)"
and I2: "l = PRreq-:19 ⟶ oip ξ ∈ kD(rt ξ)"
and I3: "l ∈ {PRrep-:2..PRrep-:6} ⟶ dip ξ ∈ kD(rt ξ)"
by (auto dest!: invariantD [OF addpreRT_partly_welldefined])
moreover from ‹(ξ, p) ∈ reachable (paodv i) TT› ‹l ∈ labels Γ⇩A⇩O⇩D⇩V p› and I3
have "l = PRrep-:6 ⟶ (the (nhop (rt ξ) (dip ξ))) ∈ kD(rt ξ)"
by (auto dest!: invariantD [OF includes_nhip])
ultimately show "?P (ξ, l)"
by simp
qed
with ‹s = (ξ, p)› show "onl Γ⇩A⇩O⇩D⇩V ?P s"
by simp
qed
text ‹Proposition 7.4›
lemma known_destinations_increase:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). kD (rt ξ) ⊆ kD (rt ξ'))"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]
simp add: subset_insertI)
text ‹Proposition 7.5›
lemma rreqs_increase:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). rreqs ξ ⊆ rreqs ξ')"
by (inv_cterms simp add: subset_insertI)
lemma dests_bigger_than_sqn:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). l ∈ {PAodv-:15..PAodv-:19}
∪ {PPkt-:7..PPkt-:11}
∪ {PRreq-:11..PRreq-:15}
∪ {PRreq-:24..PRreq-:28}
∪ {PRrep-:10..PRrep-:14}
∪ {PRerr-:1..PRerr-:5}
⟶ (∀ip∈dom(dests ξ). ip∈kD(rt ξ) ∧ sqn (rt ξ) ip ≤ the (dests ξ ip)))"
proof -
have sqninv:
"⋀dests rt rsn ip.
⟦ ∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip); dests ip = Some rsn ⟧
⟹ sqn (invalidate rt dests) ip ≤ rsn"
by (rule sqn_invalidate_in_dests [THEN eq_imp_le], assumption) auto
have indests:
"⋀dests rt rsn ip.
⟦ ∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip); dests ip = Some rsn ⟧
⟹ ip∈kD(rt) ∧ sqn rt ip ≤ rsn"
by (metis domI option.sel)
show ?thesis
by inv_cterms
(clarsimp split: if_split_asm option.split_asm
elim!: sqninv indests)+
qed
text ‹Proposition 7.6›
lemma sqns_increase:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). ∀ip. sqn (rt ξ) ip ≤ sqn (rt ξ') ip)"
proof -
{ fix ξ :: state
assume *: "∀ip∈dom(dests ξ). ip ∈ kD (rt ξ) ∧ sqn (rt ξ) ip ≤ the (dests ξ ip)"
have "∀ip. sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
proof
fix ip
from * have "ip∉dom(dests ξ) ∨ sqn (rt ξ) ip ≤ the (dests ξ ip)" by simp
thus "sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
by (metis domI invalidate_sqn option.sel)
qed
} note solve_invalidate = this
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]
onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn]
simp add: solve_invalidate)
qed
text ‹Proposition 7.7›
lemma ip_constant:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _). ip ξ = i)"
by (inv_cterms simp add: σ⇩A⇩O⇩D⇩V_def)
text ‹Proposition 7.8›
lemma sender_ip_valid':
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), a, _). anycast (λm. not_Pkt m ⟶ msg_sender m = ip ξ) a)"
by inv_cterms
lemma sender_ip_valid:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), a, _). anycast (λm. not_Pkt m ⟶ msg_sender m = i) a)"
by (rule step_invariant_weaken_with_invariantE [OF ip_constant sender_ip_valid'])
(auto dest!: onlD onllD)
lemma received_msg_inv:
"paodv i ⊫ (recvmsg P →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). l ∈ {PAodv-:1} ⟶ P (msg ξ))"
by inv_cterms
text ‹Proposition 7.9›
lemma sip_not_ip':
"paodv i ⊫ (recvmsg (λm. not_Pkt m ⟶ msg_sender m ≠ i) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _). sip ξ ≠ ip ξ)"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
lemma sip_not_ip:
"paodv i ⊫ (recvmsg (λm. not_Pkt m ⟶ msg_sender m ≠ i) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _). sip ξ ≠ i)"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text ‹Neither ‹sip_not_ip'› nor ‹sip_not_ip› is needed to show loop freedom.›
text ‹Proposition 7.10›
lemma hop_count_positive:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _). ∀ip∈kD (rt ξ). the (dhops (rt ξ) ip) ≥ 1)"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]) auto
lemma rreq_dip_in_vD_dip_eq_ip:
"paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PRreq-:18..PRreq-:21} ⟶ dip ξ ∈ vD(rt ξ))
∧ (l ∈ {PRreq-:6, PRreq-:7} ⟶ dip ξ = ip ξ)
∧ (l ∈ {PRreq-:17..PRreq-:21} ⟶ dip ξ ≠ ip ξ))"
proof (inv_cterms, elim conjE)
fix l ξ pp p'
assume "(ξ, pp) ∈ reachable (paodv i) TT"
and "{PRreq-:19}⟦λξ. ξ⦇rt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))})⦈⟧ p'
∈ sterms Γ⇩A⇩O⇩D⇩V pp"
and "l = PRreq-:19"
and "dip ξ ∈ vD (rt ξ)"
from this(1-3) have "oip ξ ∈ kD (rt ξ)"
by (auto dest: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined, where l="PRreq-:19"])
with ‹dip ξ ∈ vD (rt ξ)›
show "dip ξ ∈ vD (the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}))" by simp
qed
text ‹Proposition 7.11›
lemma anycast_msg_zhops:
"⋀rreqid dip dsn dsk oip osn sip.
paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ(_, a, _). anycast msg_zhops a)"
proof (inv_cterms inv add:
onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip [THEN invariant_restrict_inD]]
onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN
invariant_restrict_inD]],
elim conjE)
fix l ξ a pp p' pp'
assume "(ξ, pp) ∈ reachable (paodv i) TT"
and "{PRreq-:20}unicast(λξ. the (nhop (rt ξ) (oip ξ)),
λξ. Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ)).
p' ▹ pp' ∈ sterms Γ⇩A⇩O⇩D⇩V pp"
and "l = PRreq-:20"
and "a = unicast (the (nhop (rt ξ) (oip ξ)))
(Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ))"
and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
and "dip ξ ∈ vD (rt ξ)"
from ‹dip ξ ∈ vD (rt ξ)› have "dip ξ ∈ kD (rt ξ)"
by (rule vD_iD_gives_kD(1))
with * have "Suc 0 ≤ the (dhops (rt ξ) (dip ξ))" ..
thus "0 < the (dhops (rt ξ) (dip ξ))" by simp
qed
lemma hop_count_zero_oip_dip_sip:
"paodv i ⊫ (recvmsg msg_zhops →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l∈{PAodv-:4..PAodv-:5} ∪ {PRreq-:n|n. True} ⟶
(hops ξ = 0 ⟶ oip ξ = sip ξ))
∧
((l∈{PAodv-:6..PAodv-:7} ∪ {PRrep-:n|n. True} ⟶
(hops ξ = 0 ⟶ dip ξ = sip ξ))))"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) auto
lemma osn_rreq:
"paodv i ⊫ (recvmsg rreq_rrep_sn →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
l ∈ {PAodv-:4, PAodv-:5} ∪ {PRreq-:n|n. True} ⟶ 1 ≤ osn ξ)"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp
lemma osn_rreq':
"paodv i ⊫ (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
l ∈ {PAodv-:4, PAodv-:5} ∪ {PRreq-:n|n. True} ⟶ 1 ≤ osn ξ)"
proof (rule invariant_weakenE [OF osn_rreq])
fix a
assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
thus "recvmsg rreq_rrep_sn a"
by (cases a) simp_all
qed
lemma dsn_rrep:
"paodv i ⊫ (recvmsg rreq_rrep_sn →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
l ∈ {PAodv-:6, PAodv-:7} ∪ {PRrep-:n|n. True} ⟶ 1 ≤ dsn ξ)"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp
lemma dsn_rrep':
"paodv i ⊫ (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
l ∈ {PAodv-:6, PAodv-:7} ∪ {PRrep-:n|n. True} ⟶ 1 ≤ dsn ξ)"
proof (rule invariant_weakenE [OF dsn_rrep])
fix a
assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
thus "recvmsg rreq_rrep_sn a"
by (cases a) simp_all
qed
lemma hop_count_zero_oip_dip_sip':
"paodv i ⊫ (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l∈{PAodv-:4..PAodv-:5} ∪ {PRreq-:n|n. True} ⟶
(hops ξ = 0 ⟶ oip ξ = sip ξ))
∧
((l∈{PAodv-:6..PAodv-:7} ∪ {PRrep-:n|n. True} ⟶
(hops ξ = 0 ⟶ dip ξ = sip ξ))))"
proof (rule invariant_weakenE [OF hop_count_zero_oip_dip_sip])
fix a
assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
thus "recvmsg msg_zhops a"
by (cases a) simp_all
qed
text ‹Proposition 7.12›
lemma zero_seq_unk_hops_one':
"paodv i ⊫ (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _).
∀dip∈kD(rt ξ). (sqn (rt ξ) dip = 0 ⟶ sqnf (rt ξ) dip = unk)
∧ (sqnf (rt ξ) dip = unk ⟶ the (dhops (rt ξ) dip) = 1)
∧ (the (dhops (rt ξ) dip) = 1 ⟶ the (nhop (rt ξ) dip) = dip))"
proof -
{ fix dip and ξ :: state and P
assume "sqn (invalidate (rt ξ) (dests ξ)) dip = 0"
and all: "∀ip. sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
and *: "sqn (rt ξ) dip = 0 ⟹ P ξ dip"
have "P ξ dip"
proof -
from all have "sqn (rt ξ) dip ≤ sqn (invalidate (rt ξ) (dests ξ)) dip" ..
with ‹sqn (invalidate (rt ξ) (dests ξ)) dip = 0› have "sqn (rt ξ) dip = 0" by simp
thus "P ξ dip" by (rule *)
qed
} note sqn_invalidate_zero [elim!] = this
{ fix dsn hops :: nat and sip oip rt and ip dip :: ip
assume "∀dip∈kD(rt).
(sqn rt dip = 0 ⟶ π⇩3(the (rt dip)) = unk) ∧
(π⇩3(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
(the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
and "hops = 0 ⟶ sip = dip"
and "Suc 0 ≤ dsn"
and "ip ≠ dip ⟶ ip∈kD(rt)"
hence "the (dhops (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = Suc 0 ⟶
the (nhop (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = ip"
by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
} note prreq_ok1 [simp] = this
{ fix ip dsn hops sip oip rt dip
assume "∀dip∈kD(rt).
(sqn rt dip = 0 ⟶ π⇩3(the (rt dip)) = unk) ∧
(π⇩3(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
(the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
and "Suc 0 ≤ dsn"
and "ip ≠ dip ⟶ ip∈kD(rt)"
hence "π⇩3(the (update rt dip (dsn, kno, val, Suc hops, sip, {}) ip)) = unk ⟶
the (dhops (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = Suc 0"
by - (rule update_cases, auto simp add: sqn_def sqnf_def dest!: bspec)
} note prreq_ok2 [simp] = this
{ fix ip dsn hops sip oip rt dip
assume "∀dip∈kD(rt).
(sqn rt dip = 0 ⟶ π⇩3(the (rt dip)) = unk) ∧
(π⇩3(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
(the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
and "Suc 0 ≤ dsn"
and "ip ≠ dip ⟶ ip∈kD(rt)"
hence "sqn (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip = 0 ⟶
π⇩3 (the (update rt dip (dsn, kno, val, Suc hops, sip, {}) ip)) = unk"
by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
} note prreq_ok3 [simp] = this
{ fix rt sip
assume "∀dip∈kD rt.
(sqn rt dip = 0 ⟶ π⇩3(the (rt dip)) = unk) ∧
(π⇩3(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
(the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
hence "∀dip∈kD rt.
(sqn (update rt sip (0, unk, val, Suc 0, sip, {})) dip = 0 ⟶
π⇩3(the (update rt sip (0, unk, val, Suc 0, sip, {}) dip)) = unk)
∧ (π⇩3(the (update rt sip (0, unk, val, Suc 0, sip, {}) dip)) = unk ⟶
the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = Suc 0)
∧ (the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = Suc 0 ⟶
the (nhop (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = dip)"
by - (rule update_cases, simp_all add: sqnf_def sqn_def)
} note prreq_ok4 [simp] = this
have prreq_ok5 [simp]: "⋀sip rt.
π⇩3(the (update rt sip (0, unk, val, Suc 0, sip, {}) sip)) = unk ⟶
the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) sip) = Suc 0"
by (rule update_cases) simp_all
have prreq_ok6 [simp]: "⋀sip rt.
sqn (update rt sip (0, unk, val, Suc 0, sip, {})) sip = 0 ⟶
π⇩3 (the (update rt sip (0, unk, val, Suc 0, sip, {}) sip)) = unk"
by (rule update_cases) simp_all
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
onl_invariant_sterms [OF aodv_wf hop_count_zero_oip_dip_sip']
seq_step_invariant_sterms_TT [OF sqns_increase aodv_wf aodv_trans]
onl_invariant_sterms [OF aodv_wf osn_rreq']
onl_invariant_sterms [OF aodv_wf dsn_rrep']) clarsimp+
qed
lemma zero_seq_unk_hops_one:
"paodv i ⊫ (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, _).
∀dip∈kD(rt ξ). (sqn (rt ξ) dip = 0 ⟶ (sqnf (rt ξ) dip = unk
∧ the (dhops (rt ξ) dip) = 1
∧ the (nhop (rt ξ) dip) = dip)))"
by (rule invariant_weakenE [OF zero_seq_unk_hops_one']) auto
lemma kD_unk_or_atleast_one:
"paodv i ⊫ (recvmsg rreq_rrep_sn →) onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
∀dip∈kD(rt ξ). π⇩3(the (rt ξ dip)) = unk ∨ 1 ≤ π⇩2(the (rt ξ dip)))"
proof -
{ fix sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2 pre1 pre2
assume "dsk1 = unk ∨ Suc 0 ≤ dsn2"
hence "π⇩3(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1, pre1) sip)) = unk
∨ Suc 0 ≤ sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2, pre2)) sip"
unfolding update_def by (cases "dsk1 =unk") (clarsimp split: option.split)+
} note fromsip [simp] = this
{ fix dip sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2 pre1 pre2
assume allkd: "∀dip∈kD(rt). π⇩3(the (rt dip)) = unk ∨ Suc 0 ≤ sqn rt dip"
and **: "dsk1 = unk ∨ Suc 0 ≤ dsn2"
have "∀dip∈kD(rt). π⇩3(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1, pre1) dip)) = unk
∨ Suc 0 ≤ sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2, pre2)) dip"
(is "∀dip∈kD(rt). ?prop dip")
proof
fix dip
assume "dip∈kD(rt)"
thus "?prop dip"
proof (cases "dip = sip")
assume "dip = sip"
with ** show ?thesis
by simp
next
assume "dip ≠ sip"
with ‹dip∈kD(rt)› allkd show ?thesis
by simp
qed
qed
} note solve_update [simp] = this
{ fix dip rt dests
assume *: "∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip)"
and **: "∀ip∈kD(rt). π⇩3(the (rt ip)) = unk ∨ Suc 0 ≤ sqn rt ip"
have "∀dip∈kD(rt). π⇩3(the (rt dip)) = unk ∨ Suc 0 ≤ sqn (invalidate rt dests) dip"
proof
fix dip
assume "dip∈kD(rt)"
with ** have "π⇩3(the (rt dip)) = unk ∨ Suc 0 ≤ sqn rt dip" ..
thus "π⇩3 (the (rt dip)) = unk ∨ Suc 0 ≤ sqn (invalidate rt dests) dip"
proof
assume "π⇩3(the (rt dip)) = unk" thus ?thesis ..
next
assume "Suc 0 ≤ sqn rt dip"
have "Suc 0 ≤ sqn (invalidate rt dests) dip"
proof (cases "dip∈dom(dests)")
assume "dip∈dom(dests)"
with * have "sqn rt dip ≤ the (dests dip)" by simp
with ‹Suc 0 ≤ sqn rt dip› have "Suc 0 ≤ the (dests dip)" by simp
with ‹dip∈dom(dests)› ‹dip∈kD(rt)› [THEN kD_Some] show ?thesis
unfolding invalidate_def sqn_def by auto
next
assume "dip∉dom(dests)"
with ‹Suc 0 ≤ sqn rt dip› ‹dip∈kD(rt)› [THEN kD_Some] show ?thesis
unfolding invalidate_def sqn_def by auto
qed
thus ?thesis by (rule disjI2)
qed
qed
} note solve_invalidate [simp] = this
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn
[THEN invariant_restrict_inD]]
onl_invariant_sterms [OF aodv_wf osn_rreq]
onl_invariant_sterms [OF aodv_wf dsn_rrep]
simp add: proj3_inv proj2_eq_sqn)
qed
text ‹Proposition 7.13›
lemma rreq_rrep_sn_any_step_invariant:
"paodv i ⊫⇩A (recvmsg rreq_rrep_sn →) onll Γ⇩A⇩O⇩D⇩V (λ(_, a, _). anycast rreq_rrep_sn a)"
proof -
have sqnf_kno: "paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l ∈ {PRreq-:18..PRreq-:20} ⟶ sqnf (rt ξ) (dip ξ) = kno))"
by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined])
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
onl_invariant_sterms [OF aodv_wf sequence_number_one_or_bigger
[THEN invariant_restrict_inD]]
onl_invariant_sterms [OF aodv_wf kD_unk_or_atleast_one]
onl_invariant_sterms_TT [OF aodv_wf sqnf_kno]
onl_invariant_sterms [OF aodv_wf osn_rreq]
onl_invariant_sterms [OF aodv_wf dsn_rrep])
(auto simp: proj2_eq_sqn)
qed
text ‹Proposition 7.14›
lemma rreq_rrep_fresh_any_step_invariant:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a)"
proof -
have rreq_oip: "paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l ∈ {PRreq-:3..PRreq-:9} ∪ {PRreq-:17, PRreq-:30, PRreq-:32}
⟶ oip ξ ∈ kD(rt ξ)
∧ (sqn (rt ξ) (oip ξ) > (osn ξ)
∨ (sqn (rt ξ) (oip ξ) = (osn ξ)
∧ the (dhops (rt ξ) (oip ξ)) ≤ Suc (hops ξ)
∧ the (flag (rt ξ) (oip ξ)) = val))))"
proof inv_cterms
fix l ξ l' pp p'
assume "(ξ, pp) ∈ reachable (paodv i) TT"
and "{PRreq-:2}⟦λξ. ξ⦇rt :=
update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})⦈⟧ p' ∈ sterms Γ⇩A⇩O⇩D⇩V pp"
and "l' = PRreq-:3"
show "osn ξ < sqn (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ)
∨ (sqn (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ) = osn ξ
∧ the (dhops (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ))
≤ Suc (hops ξ)
∧ the (flag (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ))
= val)"
unfolding update_def by (clarsimp split: option.split)
(metis linorder_neqE_nat not_less)
qed
have rrep_prrep: "paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l ∈ {PRrep-:2..PRrep-:7} ⟶ (dip ξ ∈ kD(rt ξ)
∧ sqn (rt ξ) (dip ξ) = dsn ξ
∧ the (dhops (rt ξ) (dip ξ)) = Suc (hops ξ)
∧ the (flag (rt ξ) (dip ξ)) = val
∧ the (nhop (rt ξ) (dip ξ)) ∈ kD (rt ξ))))"
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rrep_1_update_changes]
onl_invariant_sterms [OF aodv_wf sip_in_kD])
have rreq_oip_kD: "paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PRreq-:3..PRreq-:28} ⟶ oip ξ ∈ kD(rt ξ)))"
by(inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined])
have rreq_dip_kD_oip_sqn: "paodv i ⊫ onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l).
(l ∈ {PRreq-:18..PRreq-:21}
⟶ (dip ξ ∈ kD(rt ξ)
∧ (sqn (rt ξ) (oip ξ) > (osn ξ)
∨ (sqn (rt ξ) (oip ξ) = (osn ξ)
∧ the (dhops (rt ξ) (oip ξ)) ≤ Suc (hops ξ)
∧ the (flag (rt ξ) (oip ξ)) = val)))))"
by(inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rreq_oip]
onl_invariant_sterms [OF aodv_wf addpreRT_welldefined])
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rreq_oip]
onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip]
onl_invariant_sterms [OF aodv_wf rrep_prrep]
onl_invariant_sterms [OF aodv_wf rreq_oip_kD]
onl_invariant_sterms [OF aodv_wf rreq_dip_kD_oip_sqn])
qed
text ‹Proposition 7.15›
lemma rerr_invalid_any_step_invariant:
"paodv i ⊫⇩A onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a)"
proof -
have dests_inv: "paodv i ⊫
onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PAodv-:15, PPkt-:7, PRreq-:11,
PRreq-:24, PRrep-:10, PRerr-:1}
⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ)))
∧ (l ∈ {PAodv-:16..PAodv-:19}
∪ {PPkt-:8..PPkt-:11}
∪ {PRreq-:12..PRreq-:15}
∪ {PRreq-:25..PRreq-:28}
∪ {PRrep-:11..PRrep-:14}
∪ {PRerr-:2..PRerr-:5} ⟶ (∀ip∈dom(dests ξ). ip∈iD(rt ξ)
∧ the (dests ξ ip) = sqn (rt ξ) ip))
∧ (l = PPkt-:14 ⟶ dip ξ∈iD(rt ξ)))"
by inv_cterms (clarsimp split: if_split_asm option.split_asm simp: domIff)+
show ?thesis
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf dests_inv])
qed
text ‹Proposition 7.16›
text ‹
Some well-definedness obligations are irrelevant for the Isabelle development:
\begin{enumerate}
\item In each routing table there is at most one entry for each destination: guaranteed by type.
\item In each store of queued data packets there is at most one data queue for
each destination: guaranteed by structure.
\item Whenever a set of pairs @{term "(rip, rsn)"} is assigned to the variable
@{term "dests"} of type @{typ "ip ⇀ sqn"}, or to the first argument of
the function @{term "rerr"}, this set is a partial function, i.e., there
is at most one entry @{term "(rip, rsn)"} for each destination
@{term "rip"}: guaranteed by type.
\end{enumerate}
›
lemma dests_vD_inc_sqn:
"paodv i ⊫
onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l ∈ {PAodv-:15, PPkt-:7, PRreq-:11, PRreq-:24, PRrep-:10}
⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ) ∧ the (dests ξ ip) = inc (sqn (rt ξ) ip)))
∧ (l = PRerr-:1
⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ) ∧ the (dests ξ ip) > sqn (rt ξ) ip)))"
by inv_cterms (clarsimp split: if_split_asm option.split_asm)+
text ‹Proposition 7.27›
lemma route_tables_fresher:
"paodv i ⊫⇩A (recvmsg rreq_rrep_sn →) onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)).
∀dip∈kD(rt ξ). rt ξ ⊑⇘dip⇙ rt ξ')"
proof (inv_cterms inv add:
onl_invariant_sterms [OF aodv_wf dests_vD_inc_sqn [THEN invariant_restrict_inD]]
onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN invariant_restrict_inD]]
onl_invariant_sterms [OF aodv_wf osn_rreq]
onl_invariant_sterms [OF aodv_wf dsn_rrep]
onl_invariant_sterms [OF aodv_wf addpreRT_welldefined [THEN invariant_restrict_inD]])
fix ξ pp p'
assume "(ξ, pp) ∈ reachable (paodv i) (recvmsg rreq_rrep_sn)"
and "{PRreq-:2}⟦λξ. ξ⦇rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})⦈⟧
p' ∈ sterms Γ⇩A⇩O⇩D⇩V pp"
and "Suc 0 ≤ osn ξ"
and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
show "∀ip∈kD (rt ξ). rt ξ ⊑⇘ip⇙ update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
proof
fix ip
assume "ip∈kD (rt ξ)"
moreover with * have "1 ≤ the (dhops (rt ξ) ip)" by simp
moreover from ‹Suc 0 ≤ osn ξ›
have "update_arg_wf (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})" ..
ultimately show "rt ξ ⊑⇘ip⇙ update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
by (rule rt_fresher_update)
qed
next
fix ξ pp p'
assume "(ξ, pp) ∈ reachable (paodv i) (recvmsg rreq_rrep_sn)"
and "{PRrep-:1}⟦λξ. ξ⦇rt := update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})⦈⟧
p' ∈ sterms Γ⇩A⇩O⇩D⇩V pp"
and "Suc 0 ≤ dsn ξ"
and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
show "∀ip∈kD (rt ξ). rt ξ ⊑⇘ip⇙ update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
proof
fix ip
assume "ip∈kD (rt ξ)"
moreover with * have "1 ≤ the (dhops (rt ξ) ip)" by simp
moreover from ‹Suc 0 ≤ dsn ξ›
have "update_arg_wf (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})" ..
ultimately show "rt ξ ⊑⇘ip⇙ update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
by (rule rt_fresher_update)
qed
qed
end