# Theory Aodv_Predicates

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

section "Invariant assumptions and properties"

theory Aodv_Predicates
imports Aodv
begin

text ‹Definitions for expression assumptions on incoming messages and properties of
outgoing messages.›

abbreviation not_Pkt :: "msg ⇒ bool"
where "not_Pkt m ≡ case m of Pkt _ _ _ ⇒ False | _ ⇒ True"

definition msg_sender :: "msg ⇒ ip"
where "msg_sender m ≡ case m of Rreq _ _ _ _ _ _ _ ipc ⇒ ipc
| Rrep _ _ _ _ ipc ⇒ ipc
| Rerr _ ipc ⇒ ipc
| Pkt _ _ ipc ⇒ ipc"

lemma msg_sender_simps [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip.
msg_sender (Rreq hops rreqid dip dsn dsk oip osn sip) = sip"
"⋀hops dip dsn oip sip. msg_sender (Rrep hops dip dsn oip sip) = sip"
"⋀dests sip.            msg_sender (Rerr dests sip) = sip"
"⋀d dip sip.            msg_sender (Pkt d dip sip) = sip"
unfolding msg_sender_def by simp_all

definition msg_zhops :: "msg ⇒ bool"
where "msg_zhops m ≡ case m of
Rreq hopsc _ dipc _ _ oipc _ sipc ⇒ hopsc = 0 ⟶ oipc = sipc
| Rrep hopsc dipc _ _ sipc ⇒ hopsc = 0 ⟶ dipc = sipc
| _ ⇒ True"

lemma msg_zhops_simps [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip.
msg_zhops (Rreq hops rreqid dip dsn dsk oip osn sip) = (hops = 0 ⟶ oip = sip)"
"⋀hops dip dsn oip sip. msg_zhops (Rrep hops dip dsn oip sip) = (hops = 0 ⟶ dip = sip)"
"⋀dests sip.            msg_zhops (Rerr dests sip)        = True"
"⋀d dip.                msg_zhops (Newpkt d dip)          = True"
"⋀d dip sip.            msg_zhops (Pkt d dip sip)         = True"
unfolding msg_zhops_def by simp_all

definition rreq_rrep_sn :: "msg ⇒ bool"
where "rreq_rrep_sn m ≡ case m of Rreq _ _ _ _ _ _ osnc _ ⇒ osnc ≥ 1
| Rrep _ _ dsnc _ _ ⇒ dsnc ≥ 1
| _ ⇒ True"

lemma rreq_rrep_sn_simps [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip.
rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip) = (osn ≥ 1)"
"⋀hops dip dsn oip sip. rreq_rrep_sn (Rrep hops dip dsn oip sip) = (dsn ≥ 1)"
"⋀dests sip.            rreq_rrep_sn (Rerr dests sip) = True"
"⋀d dip.                rreq_rrep_sn (Newpkt d dip)   = True"
"⋀d dip sip.            rreq_rrep_sn (Pkt d dip sip)  = True"
unfolding rreq_rrep_sn_def by simp_all

definition rreq_rrep_fresh :: "rt ⇒ msg ⇒ bool"
where "rreq_rrep_fresh crt m ≡ case m of Rreq hopsc _ _ _ _ oipc osnc ipcc ⇒ (ipcc ≠ oipc ⟶
oipc∈kD(crt) ∧ (sqn crt oipc > osnc
∨ (sqn crt oipc = osnc
∧ the (dhops crt oipc) ≤ hopsc
∧ the (flag crt oipc) = val)))
| Rrep hopsc dipc dsnc _ ipcc ⇒ (ipcc ≠ dipc ⟶
dipc∈kD(crt)
∧ sqn crt dipc = dsnc
∧ the (dhops crt dipc) = hopsc
∧ the (flag crt dipc) = val)
| _ ⇒ True"

lemma rreq_rrep_fresh [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip.
rreq_rrep_fresh crt (Rreq hops rreqid dip dsn dsk oip osn sip) =
(sip ≠ oip ⟶ oip∈kD(crt)
∧ (sqn crt oip > osn
∨ (sqn crt oip = osn
∧ the (dhops crt oip) ≤ hops
∧ the (flag crt oip) = val)))"
"⋀hops dip dsn oip sip. rreq_rrep_fresh crt (Rrep hops dip dsn oip sip) =
(sip ≠ dip ⟶ dip∈kD(crt)
∧ sqn crt dip = dsn
∧ the (dhops crt dip) = hops
∧ the (flag crt dip) = val)"
"⋀dests sip.            rreq_rrep_fresh crt (Rerr dests sip) = True"
"⋀d dip.                rreq_rrep_fresh crt (Newpkt d dip)   = True"
"⋀d dip sip.            rreq_rrep_fresh crt (Pkt d dip sip)  = True"
unfolding rreq_rrep_fresh_def by simp_all

definition rerr_invalid :: "rt ⇒ msg ⇒ bool"
where "rerr_invalid crt m ≡ case m of Rerr destsc _ ⇒ (∀ripc∈dom(destsc).
(ripc∈iD(crt) ∧ the (destsc ripc) = sqn crt ripc))
| _ ⇒ True"

lemma rerr_invalid [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip.
rerr_invalid crt (Rreq hops rreqid dip dsn dsk oip osn sip) = True"
"⋀hops dip dsn oip sip. rerr_invalid crt (Rrep hops dip dsn oip sip) = True"
"⋀dests sip.            rerr_invalid crt (Rerr dests sip) = (∀rip∈dom(dests).
rip∈iD(crt) ∧ the (dests rip) = sqn crt rip)"
"⋀d dip.                rerr_invalid crt (Newpkt d dip)   = True"
"⋀d dip sip.            rerr_invalid crt (Pkt d dip sip)  = True"
unfolding rerr_invalid_def by simp_all

definition
initmissing :: "(nat ⇒ state option) × 'a ⇒ (nat ⇒ state) × 'a"
where
"initmissing σ = (λi. case (fst σ) i of None ⇒ aodv_init i | Some s ⇒ s, snd σ)"

lemma not_in_net_ips_fst_init_missing [simp]:
assumes "i ∉ net_ips σ"
shows "fst (initmissing (netgmap fst σ)) i = aodv_init i"
using assms unfolding initmissing_def by simp

lemma fst_initmissing_netgmap_pair_fst [simp]:
"fst (initmissing (netgmap (λ(p, q). (fst (id p), snd (id p), q)) s))
= fst (initmissing (netgmap fst s))"
unfolding initmissing_def by auto

text ‹We introduce a streamlined alternative to @{term initmissing} with @{term netgmap}
to simplify invariant statements and thus facilitate their comprehension and
presentation.›

lemma fst_initmissing_netgmap_default_aodv_init_netlift:
"fst (initmissing (netgmap fst s)) = default aodv_init (netlift fst s)"
unfolding initmissing_def default_def
by (simp add: fst_netgmap_netlift del: One_nat_def)

definition
netglobal :: "((nat ⇒ state) ⇒ bool) ⇒ ((state × 'b) × 'c) net_state ⇒ bool"
where
"netglobal P ≡ (λs. P (default aodv_init (netlift fst s)))"

end
```