Theory D_Aodv

(*  Title:       variants/d_fwdrreqs/Aodv.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
    Author:      Peter Höfner, NICTA
*)

section "The AODV protocol"

theory D_Aodv
imports D_Aodv_Data D_Aodv_Message
        AWN.AWN_SOS_Labels AWN.AWN_Invariants
begin

subsection "Data state"

record state =
  ip    :: "ip"
  sn    :: "sqn"
  rt    :: "rt" 
  rreqs :: "(ip × rreqid) set"
  store :: "store"
  (* all locals *)
  msg    :: "msg"
  data   :: "data"
  dests  :: "ip ⇀ sqn"
  pre    :: "ip set"
  rreqid :: "rreqid"
  dip    :: "ip"
  oip    :: "ip"
  hops   :: "nat"
  dsn    :: "sqn"
  dsk    :: "k"
  osn    :: "sqn"
  sip    :: "ip"
  handled:: "bool"

abbreviation aodv_init :: "ip ⇒ state"
where "aodv_init i ≡ ⦇
         ip = i,
         sn = 1,
         rt = Map.empty,
         rreqs = {},
         store = Map.empty,

         msg    = (SOME x. True),
         data   = (SOME x. True),
         dests  = (SOME x. True),
         pre    = (SOME x. True),
         rreqid = (SOME x. True),
         dip    = (SOME x. True),
         oip    = (SOME x. True),
         hops   = (SOME x. True),
         dsn    = (SOME x. True),
         dsk    = (SOME x. True),
         osn    = (SOME x. True),
         sip    = (SOME x. x ≠ i),
         handled= (SOME x. True)
       ⦈"

lemma some_neq_not_eq [simp]: "¬((SOME x :: nat. x ≠ i) = i)"
  by (subst some_eq_ex) (metis zero_neq_numeral)

definition clear_locals :: "state ⇒ state"
where "clear_locals ξ = ξ ⦇
    msg    := (SOME x. True),
    data   := (SOME x. True),
    dests  := (SOME x. True),
    pre    := (SOME x. True),
    rreqid := (SOME x. True),
    dip    := (SOME x. True),
    oip    := (SOME x. True),
    hops   := (SOME x. True),
    dsn    := (SOME x. True),
    dsk    := (SOME x. True),
    osn    := (SOME x. True),
    sip    := (SOME x. x ≠ ip ξ),
    handled:= (SOME x. True)
  ⦈"

lemma clear_locals_sip_not_ip [simp]: "¬(sip (clear_locals ξ) = ip ξ)"
  unfolding clear_locals_def by simp

lemma clear_locals_but_not_globals [simp]:
  "ip (clear_locals ξ) = ip ξ"
  "sn (clear_locals ξ) = sn ξ"
  "rt (clear_locals ξ) = rt ξ"
  "rreqs (clear_locals ξ) = rreqs ξ"
  "store (clear_locals ξ) = store ξ"
  unfolding clear_locals_def by auto

subsection "Auxilliary message handling definitions"

definition is_newpkt
where "is_newpkt ξ ≡ case msg ξ of
                       Newpkt data' dip' ⇒ { ξ⦇data := data', dip := dip'⦈ }
                     | _ ⇒ {}"

definition is_pkt
where "is_pkt ξ ≡ case msg ξ of
                    Pkt data' dip' oip' ⇒ { ξ⦇ data := data', dip := dip', oip := oip' ⦈ }
                  | _ ⇒ {}"

definition is_rreq
where "is_rreq ξ ≡ case msg ξ of
                     Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled' ⇒
                       { ξ⦇ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                            dsk := dsk', oip := oip', osn := osn', sip := sip', 
                            handled := handled' ⦈ }
                   | _ ⇒ {}"

lemma is_rreq_asm [dest!]:
  assumes "ξ' ∈ is_rreq ξ"
    shows "(∃hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled'.
               msg ξ = Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled' ∧
               ξ' = ξ⦇ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                       dsk := dsk', oip := oip', osn := osn', sip := sip', 
                       handled := handled' ⦈)"
  using assms unfolding is_rreq_def
  by (cases "msg ξ") simp_all

definition is_rrep
where "is_rrep ξ ≡ case msg ξ of
                     Rrep hops' dip' dsn' oip' sip' ⇒
                       { ξ⦇ hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ⦈ }
                   | _ ⇒ {}"

lemma is_rrep_asm [dest!]:
  assumes "ξ' ∈ is_rrep ξ"
    shows "(∃hops' dip' dsn' oip' sip'.
               msg ξ = Rrep hops' dip' dsn' oip' sip' ∧
               ξ' = ξ⦇ hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ⦈)"
  using assms unfolding is_rrep_def
  by (cases "msg ξ") simp_all

definition is_rerr
where "is_rerr ξ ≡ case msg ξ of
                     Rerr dests' sip' ⇒ { ξ⦇ dests := dests', sip := sip' ⦈ }
                   | _ ⇒ {}"

lemma is_rerr_asm [dest!]:
  assumes "ξ' ∈ is_rerr ξ"
    shows "(∃dests' sip'.
               msg ξ = Rerr dests' sip' ∧
               ξ' = ξ⦇ dests := dests', sip := sip' ⦈)"
  using assms unfolding is_rerr_def
  by (cases "msg ξ") simp_all

lemmas is_msg_defs =
  is_rerr_def is_rrep_def is_rreq_def is_pkt_def is_newpkt_def

lemma is_msg_inv_ip [simp]:
  "ξ' ∈ is_rerr ξ   ⟹ ip ξ' = ip ξ"
  "ξ' ∈ is_rrep ξ   ⟹ ip ξ' = ip ξ"
  "ξ' ∈ is_rreq ξ   ⟹ ip ξ' = ip ξ"
  "ξ' ∈ is_pkt ξ    ⟹ ip ξ' = ip ξ"
  "ξ' ∈ is_newpkt ξ ⟹ ip ξ' = ip ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sn [simp]:
  "ξ' ∈ is_rerr ξ   ⟹ sn ξ' = sn ξ"
  "ξ' ∈ is_rrep ξ   ⟹ sn ξ' = sn ξ"
  "ξ' ∈ is_rreq ξ   ⟹ sn ξ' = sn ξ"
  "ξ' ∈ is_pkt ξ    ⟹ sn ξ' = sn ξ"
  "ξ' ∈ is_newpkt ξ ⟹ sn ξ' = sn ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rt [simp]:
  "ξ' ∈ is_rerr ξ   ⟹ rt ξ' = rt ξ"
  "ξ' ∈ is_rrep ξ   ⟹ rt ξ' = rt ξ"
  "ξ' ∈ is_rreq ξ   ⟹ rt ξ' = rt ξ"
  "ξ' ∈ is_pkt ξ    ⟹ rt ξ' = rt ξ"
  "ξ' ∈ is_newpkt ξ ⟹ rt ξ' = rt ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rreqs [simp]:
  "ξ' ∈ is_rerr ξ   ⟹ rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_rrep ξ   ⟹ rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_rreq ξ   ⟹ rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_pkt ξ    ⟹ rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_newpkt ξ ⟹ rreqs ξ' = rreqs ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_store [simp]:
  "ξ' ∈ is_rerr ξ   ⟹ store ξ' = store ξ"
  "ξ' ∈ is_rrep ξ   ⟹ store ξ' = store ξ"
  "ξ' ∈ is_rreq ξ   ⟹ store ξ' = store ξ"
  "ξ' ∈ is_pkt ξ    ⟹ store ξ' = store ξ"
  "ξ' ∈ is_newpkt ξ ⟹ store ξ' = store ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sip [simp]:
  "ξ' ∈ is_pkt ξ    ⟹ sip ξ' = sip ξ"
  "ξ' ∈ is_newpkt ξ ⟹ sip ξ' = sip ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

subsection "The protocol process"

datatype pseqp =
    PAodv
  | PNewPkt
  | PPkt
  | PRreq
  | PRrep
  | PRerr

fun nat_of_seqp :: "pseqp ⇒ nat"
where
  "nat_of_seqp PAodv  = 1"
| "nat_of_seqp PPkt   = 2"
| "nat_of_seqp PNewPkt   = 3"
| "nat_of_seqp PRreq  = 4"
| "nat_of_seqp PRrep  = 5"
| "nat_of_seqp PRerr  = 6"

instantiation "pseqp" :: ord
begin
definition less_eq_seqp [iff]: "l1 ≤ l2 = (nat_of_seqp l1 ≤ nat_of_seqp l2)"
definition less_seqp [iff]:    "l1 < l2 = (nat_of_seqp l1 < nat_of_seqp l2)"
instance ..
end

abbreviation AODV
where
  "AODV ≡ λ_. ⟦clear_locals⟧ call(PAodv)"

abbreviation PKT
where
  "PKT args ≡

     ⟦ξ. let (data, dip, oip) = args ξ in
         (clear_locals ξ) ⦇ data := data, dip := dip, oip := oip ⦈⟧
     call(PPkt)"
abbreviation NEWPKT
where
  "NEWPKT args ≡
     ⟦ξ. let (data, dip) = args ξ in
         (clear_locals ξ) ⦇ data := data, dip := dip ⦈⟧
     call(PNewPkt)"

abbreviation RREQ
where
  "RREQ args ≡
     ⟦ξ. let (hops, rreqid, dip, dsn, dsk, oip, osn, sip, handled) = args ξ in
         (clear_locals ξ) ⦇ hops := hops, rreqid := rreqid, dip := dip,
                            dsn := dsn, dsk := dsk, oip := oip,
                            osn := osn, sip := sip, handled := handled ⦈⟧
     call(PRreq)"

abbreviation RREP
where
  "RREP args ≡
     ⟦ξ. let (hops, dip, dsn, oip, sip) = args ξ in
         (clear_locals ξ) ⦇ hops := hops, dip := dip, dsn := dsn,
                            oip := oip, sip := sip ⦈⟧
     call(PRrep)"

abbreviation RERR
where
  "RERR args ≡
     ⟦ξ. let (dests, sip) = args ξ in
         (clear_locals ξ) ⦇ dests := dests, sip := sip ⦈⟧
     call(PRerr)"

fun Γ⇩A⇩O⇩D⇩V :: "(state, msg, pseqp, pseqp label) seqp_env"
where
  "Γ⇩A⇩O⇩D⇩V PAodv = labelled PAodv (
     receive(λmsg' ξ. ξ ⦇ msg := msg' ⦈).
     (    ⟨is_newpkt⟩ NEWPKT(λξ. (data ξ, ip ξ))
       ⊕ ⟨is_pkt⟩ PKT(λξ. (data ξ, dip ξ, oip ξ))
       ⊕ ⟨is_rreq⟩
            ⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
            RREQ(λξ. (hops ξ, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, sip ξ, handled ξ))
       ⊕ ⟨is_rrep⟩
            ⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
            RREP(λξ. (hops ξ, dip ξ, dsn ξ, oip ξ, sip ξ))
       ⊕ ⟨is_rerr⟩
            ⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
            RERR(λξ. (dests ξ, sip ξ))
     )
     ⊕ ⟨λξ. { ξ⦇ dip := dip ⦈ | dip. dip ∈ qD(store ξ) ∩ vD(rt ξ) }⟩
          ⟦ξ. ξ ⦇ data := hd(σ⇘queue⇙(store ξ, dip ξ)) ⦈⟧
          unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, ip ξ)).
            ⟦ξ. ξ ⦇ store := the (drop (dip ξ) (store ξ)) ⦈⟧
            AODV()
          ▹ ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
             ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
             ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
             ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
             ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) ⦈⟧
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV()
     ⊕ ⟨λξ. { ξ⦇ dip := dip ⦈
             | dip. dip ∈ qD(store ξ) - vD(rt ξ) ∧ the (σ⇘p-flag⇙(store ξ, dip)) = req }⟩
         ⟦ξ. ξ ⦇ store := unsetRRF (store ξ) (dip ξ) ⦈⟧
         ⟦ξ. ξ ⦇ sn := inc (sn ξ) ⦈⟧
         ⟦ξ. ξ ⦇ rreqid := nrreqid (rreqs ξ) (ip ξ) ⦈⟧
         ⟦ξ. ξ ⦇ rreqs := rreqs ξ ∪ {(ip ξ, rreqid ξ)} ⦈⟧
         broadcast(λξ. rreq(0, rreqid ξ, dip ξ, sqn (rt ξ) (dip ξ), sqnf (rt ξ) (dip ξ), ip ξ, sn ξ,
                            ip ξ, False)). AODV())"

|  "Γ⇩A⇩O⇩D⇩V PNewPkt = labelled PNewPkt (
     ⟨ξ. dip ξ = ip ξ⟩
        deliver(λξ. data ξ).AODV()
     ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
        ⟦ξ. ξ ⦇ store := add (data ξ) (dip ξ) (store ξ) ⦈⟧
        AODV())"

| "Γ⇩A⇩O⇩D⇩V PPkt = labelled PPkt (
     ⟨ξ. dip ξ = ip ξ⟩
        deliver(λξ. data ξ).AODV()
     ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
     (
       ⟨ξ. dip ξ ∈ vD (rt ξ)⟩
         unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, oip ξ)).AODV()
         ▹
           ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
                                   then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
           ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
           ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
           ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
           ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                   then (dests ξ) rip else None) ⦈⟧
           groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
       ⊕ ⟨ξ. dip ξ ∉ vD (rt ξ)⟩
       (
           ⟨ξ. dip ξ ∈ iD (rt ξ)⟩
             groupcast(λξ. the (precs (rt ξ) (dip ξ)), λξ. rerr([dip ξ ↦ sqn (rt ξ) (dip ξ)],
                                                                ip ξ)).AODV()
           ⊕ ⟨ξ. dip ξ ∉ iD (rt ξ)⟩
              AODV()
       )
     ))"

| "Γ⇩A⇩O⇩D⇩V PRreq = labelled PRreq (
     ⟨ξ. (oip ξ, rreqid ξ) ∈ rreqs ξ⟩
       AODV()
     ⊕ ⟨ξ. (oip ξ, rreqid ξ) ∉ rreqs ξ⟩
       ⟦ξ. ξ ⦇ rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⦈⟧
       ⟦ξ. ξ ⦇ rreqs := rreqs ξ ∪ {(oip ξ, rreqid ξ)} ⦈⟧
       (
         ⟨ξ. handled ξ = False⟩
         (
           ⟨ξ. dip ξ = ip ξ⟩
             ⟦ξ. ξ ⦇ sn := max (sn ξ) (dsn ξ) ⦈⟧
             unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(0, dip ξ, sn ξ, oip ξ, ip ξ)).
               broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, ip ξ, True)).
               AODV()
             ▹
               ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                       then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
               ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
               ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
               ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
               ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                       then (dests ξ) rip else None) ⦈⟧
               groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
           ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
           (
             ⟨ξ. dip ξ ∈ vD (rt ξ) ∧ dsn ξ ≤ sqn (rt ξ) (dip ξ) ∧ sqnf (rt ξ) (dip ξ) = kno⟩
               ⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (dip ξ) {sip ξ}) ⦈⟧
               ⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}) ⦈⟧ 
               unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(the (dhops (rt ξ) (dip ξ)), dip ξ,
               sqn (rt ξ) (dip ξ), oip ξ, ip ξ)).
                 broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ,
                                dsk ξ, oip ξ, osn ξ, ip ξ, True)).
                 AODV()
             ▹
               ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                       then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
               ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
               ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
               ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
               ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                       then (dests ξ) rip else None) ⦈⟧
               groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
             ⊕ ⟨ξ. dip ξ ∉ vD (rt ξ) ∨ sqn (rt ξ) (dip ξ) < dsn ξ ∨ sqnf (rt ξ) (dip ξ) = unk⟩
               broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, max (sqn (rt ξ) (dip ξ)) (dsn ξ),
                                  dsk ξ, oip ξ, osn ξ, ip ξ, False)).
               AODV()
           )
         )
         ⊕ ⟨ξ. handled ξ = True⟩
           broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, ip ξ, True)).
           AODV()
       ))"

| "Γ⇩A⇩O⇩D⇩V PRrep = labelled PRrep (
     ⟨ξ. rt ξ ≠ update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
     (
       ⟦ξ. ξ ⦇ rt := update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⦈ ⟧
       (
         ⟨ξ. oip ξ = ip ξ ⟩
            AODV()
         ⊕ ⟨ξ. oip ξ ≠ ip ξ ⟩
         (
           ⟨ξ. oip ξ ∈ vD (rt ξ)⟩
             ⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (dip ξ) {the (nhop (rt ξ) (oip ξ))}) ⦈⟧
             ⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (the (nhop (rt ξ) (dip ξ)))
                                               {the (nhop (rt ξ) (oip ξ))}) ⦈⟧ 
             unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(hops ξ + 1, dip ξ, dsn ξ, oip ξ, ip ξ)).
             AODV()
           ▹
             ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
             ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
             ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
             ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
             ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) ⦈⟧
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
           ⊕ ⟨ξ. oip ξ ∉ vD (rt ξ)⟩
             AODV()
         )
       )
     )
     ⊕ ⟨ξ. rt ξ = update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
         AODV()
     )"

| "Γ⇩A⇩O⇩D⇩V PRerr = labelled PRerr (
     ⟦ξ. ξ ⦇ dests := (λrip. case (dests ξ) rip of None ⇒ None
                       | Some rsn ⇒ if rip ∈ vD (rt ξ) ∧ the (nhop (rt ξ) rip) = sip ξ
                                       ∧ sqn (rt ξ) rip < rsn then Some rsn else None) ⦈⟧
     ⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
     ⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
     ⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
     ⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                             then (dests ξ) rip else None) ⦈⟧
     groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV())"

declare Γ⇩A⇩O⇩D⇩V.simps [simp del, code del]
lemmas Γ⇩A⇩O⇩D⇩V_simps [simp, code] = Γ⇩A⇩O⇩D⇩V.simps [simplified]

fun Γ⇩A⇩O⇩D⇩V_skeleton
where
    "Γ⇩A⇩O⇩D⇩V_skeleton PAodv   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PAodv)"
  | "Γ⇩A⇩O⇩D⇩V_skeleton PNewPkt = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PNewPkt)"
  | "Γ⇩A⇩O⇩D⇩V_skeleton PPkt    = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PPkt)"
  | "Γ⇩A⇩O⇩D⇩V_skeleton PRreq   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRreq)"
  | "Γ⇩A⇩O⇩D⇩V_skeleton PRrep   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRrep)"
  | "Γ⇩A⇩O⇩D⇩V_skeleton PRerr   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRerr)"

lemma Γ⇩A⇩O⇩D⇩V_skeleton_wf [simp]:
  "wellformed Γ⇩A⇩O⇩D⇩V_skeleton"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ⇩A⇩O⇩D⇩V_skeleton pn)"
      by (cases pn) simp_all
  qed

declare Γ⇩A⇩O⇩D⇩V_skeleton.simps [simp del, code del]
lemmas Γ⇩A⇩O⇩D⇩V_skeleton_simps [simp, code]
           = Γ⇩A⇩O⇩D⇩V_skeleton.simps [simplified Γ⇩A⇩O⇩D⇩V_simps seqp_skeleton.simps]

lemma aodv_proc_cases [dest]:
  fixes p pn
  shows "p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V pn) ⟹
                                (p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PAodv) ∨ 
                                 p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PNewPkt)  ∨
                                 p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PPkt)  ∨
                                 p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRreq) ∨
                                 p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRrep) ∨
                                 p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRerr))"
  by (cases pn) simp_all

definition σ⇩A⇩O⇩D⇩V :: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σ⇩A⇩O⇩D⇩V i ≡ {(aodv_init i, Γ⇩A⇩O⇩D⇩V PAodv)}"

abbreviation paodv
  :: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "paodv i ≡ ⦇ init = σ⇩A⇩O⇩D⇩V i, trans = seqp_sos Γ⇩A⇩O⇩D⇩V ⦈"

lemma aodv_trans: "trans (paodv i) = seqp_sos Γ⇩A⇩O⇩D⇩V"
  by simp

lemma aodv_control_within [simp]: "control_within Γ⇩A⇩O⇩D⇩V (init (paodv i))"
  unfolding σ⇩A⇩O⇩D⇩V_def by (rule control_withinI) (auto simp del: Γ⇩A⇩O⇩D⇩V_simps)

lemma aodv_wf [simp]:
  "wellformed Γ⇩A⇩O⇩D⇩V"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ⇩A⇩O⇩D⇩V pn)"
      by (cases pn) simp_all
  qed

lemmas aodv_labels_not_empty [simp] = labels_not_empty [OF aodv_wf]

lemma aodv_ex_label [intro]: "∃l. l∈labels Γ⇩A⇩O⇩D⇩V p"
  by (metis aodv_labels_not_empty all_not_in_conv)

lemma aodv_ex_labelE [elim]:
  assumes "∀l∈labels Γ⇩A⇩O⇩D⇩V p. P l p"
      and "∃p l. P l p ⟹ Q"
    shows "Q"
  using assms by (metis aodv_ex_label)

lemma aodv_simple_labels [simp]: "simple_labels Γ⇩A⇩O⇩D⇩V"
  proof
    fix pn p
    assume "p∈subterms(Γ⇩A⇩O⇩D⇩V pn)"
    thus "∃!l. labels Γ⇩A⇩O⇩D⇩V p = {l}"
    by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
  qed

lemma σ⇩A⇩O⇩D⇩V_labels [simp]: "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i ⟹  labels Γ⇩A⇩O⇩D⇩V p = {PAodv-:0}"
  unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma aodv_init_kD_empty [simp]:
  "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i ⟹ kD (rt ξ) = {}"
  unfolding σ⇩A⇩O⇩D⇩V_def kD_def by simp

lemma aodv_init_sip_not_ip [simp]: "¬(sip (aodv_init i) = i)" by simp

lemma aodv_init_sip_not_ip' [simp]:
  assumes "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i"
    shows "sip ξ ≠ ip ξ"
  using assms unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma aodv_init_sip_not_i [simp]:
  assumes "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i"
    shows "sip ξ ≠ i"
  using assms unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma clear_locals_sip_not_ip':
  assumes "ip ξ = i"
    shows "¬(sip (clear_locals ξ) = i)"
  using assms by auto

text ‹Stop the simplifier from descending into process terms.›
declare seqp_congs [cong]

text ‹Configure the main invariant tactic for AODV.›

declare
  Γ⇩A⇩O⇩D⇩V_simps [cterms_env]
  aodv_proc_cases [ctermsl_cases]
  seq_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
                            cterms_intros]
  seq_step_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
                                 cterms_intros]

end