Theory C_Aodv

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

section "The AODV protocol"

theory C_Aodv
imports C_Aodv_Data C_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"
  rreqid :: "rreqid"
  dip    :: "ip"
  oip    :: "ip"
  hops   :: "nat"
  dsn    :: "sqn"
  dsk    :: "k"
  osn    :: "sqn"
  sip    :: "ip"

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),
         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)
       "

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),
    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 ξ)
  "

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' 
                       { ξ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                            dsk := dsk', oip := oip', osn := osn', sip := sip'  }
                   | _  {}"

lemma is_rreq_asm [dest!]:
  assumes "ξ'  is_rreq ξ"
    shows "(hops' rreqid' dip' dsn' dsk' oip' osn' sip'.
               msg ξ = Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' 
               ξ' = ξ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                       dsk := dsk', oip := oip', osn := osn', sip := sip' )"
  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) = args ξ in
         (clear_locals ξ)  hops := hops, rreqid := rreqid, dip := dip,
                            dsn := dsn, dsk := dsk, oip := oip,
                            osn := osn, sip := sip 
     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 ΓAODV :: "(state, msg, pseqp, pseqp label) seqp_env"
where
  "ΓAODV 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 ξ))
        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 ξ)
             broadcast(λξ. 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 ξ)). AODV())"

|  "ΓAODV PNewPkt = labelled PNewPkt (
     ξ. dip ξ = ip ξ
        deliver(λξ. data ξ).AODV()
      ξ. dip ξ  ip ξ
        ξ. ξ  store := add (data ξ) (dip ξ) (store ξ) 
        AODV())"

| "ΓAODV 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 ξ)
           broadcast(λξ. rerr(dests ξ, ip ξ)).AODV()
        ξ. dip ξ  vD (rt ξ)
       (
           ξ. dip ξ  iD (rt ξ)
             broadcast(λξ. rerr([dip ξ  sqn (rt ξ) (dip ξ)], ip ξ)). AODV()
            ξ. dip ξ  iD (rt ξ)
              AODV()
       )
     ))"

| "ΓAODV PRreq = labelled PRreq (
     ξ. (oip ξ, rreqid ξ)  rreqs ξ
       AODV()
      ξ. (oip ξ, rreqid ξ)  rreqs ξ
       ξ. ξ  rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, hops ξ + 1, sip ξ) 
       ξ. ξ  rreqs := rreqs ξ  {(oip ξ, rreqid ξ)} 
       (
         ξ. dip ξ = ip ξ
           ξ. ξ  sn := max (sn ξ) (dsn ξ) 
           unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(0, dip ξ, sn ξ, 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 ξ)
             broadcast(λξ. rerr(dests ξ, ip ξ)).AODV()
          ξ. dip ξ  ip ξ
         (
           ξ. dip ξ  vD (rt ξ)  dsn ξ  sqn (rt ξ) (dip ξ)  sqnf (rt ξ) (dip ξ) = kno
             unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(the (dhops (rt ξ) (dip ξ)), dip ξ,
                                                             sqn (rt ξ) (dip ξ), 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 ξ)
             broadcast(λξ. 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 ξ)).
             AODV()
         )
       ))"

| "ΓAODV 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 ξ)
             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 ξ)
             broadcast(λξ. rerr(dests ξ, ip ξ)).AODV()
            ξ. oip ξ  vD (rt ξ)
             AODV()
         )
       )
     )
      ξ. rt ξ = update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ) 
         AODV()
     )"

| "ΓAODV 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 ξ)
     (
        ξ. dests ξ  Map.empty
          broadcast(λξ. rerr(dests ξ, ip ξ)). AODV()
         ξ. dests ξ = Map.empty 
          AODV()
     ))"



declare ΓAODV.simps [simp del, code del]
lemmas ΓAODV_simps [simp, code] = ΓAODV.simps [simplified]

fun ΓAODV_skeleton
where
    "ΓAODV_skeleton PAodv   = seqp_skeleton (ΓAODV PAodv)"
  | "ΓAODV_skeleton PNewPkt = seqp_skeleton (ΓAODV PNewPkt)"
  | "ΓAODV_skeleton PPkt    = seqp_skeleton (ΓAODV PPkt)"
  | "ΓAODV_skeleton PRreq   = seqp_skeleton (ΓAODV PRreq)"
  | "ΓAODV_skeleton PRrep   = seqp_skeleton (ΓAODV PRrep)"
  | "ΓAODV_skeleton PRerr   = seqp_skeleton (ΓAODV PRerr)"

lemma ΓAODV_skeleton_wf [simp]:
  "wellformed ΓAODV_skeleton"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn')  stermsl (ΓAODV_skeleton pn)"
      by (cases pn) simp_all
  qed

declare ΓAODV_skeleton.simps [simp del, code del]
lemmas ΓAODV_skeleton_simps [simp, code]
           = ΓAODV_skeleton.simps [simplified ΓAODV_simps seqp_skeleton.simps]

lemma aodv_proc_cases [dest]:
  fixes p pn
  shows "p  ctermsl (ΓAODV pn) 
                                (p  ctermsl (ΓAODV PAodv)  
                                 p  ctermsl (ΓAODV PNewPkt)  
                                 p  ctermsl (ΓAODV PPkt)  
                                 p  ctermsl (ΓAODV PRreq) 
                                 p  ctermsl (ΓAODV PRrep) 
                                 p  ctermsl (ΓAODV PRerr))"
  by (cases pn) simp_all

definition σAODV :: "ip  (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σAODV i  {(aodv_init i, ΓAODV PAodv)}"

abbreviation paodv
  :: "ip  (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "paodv i   init = σAODV i, trans = seqp_sos ΓAODV "

lemma aodv_trans: "trans (paodv i) = seqp_sos ΓAODV"
  by simp

lemma aodv_control_within [simp]: "control_within ΓAODV (init (paodv i))"
  unfolding σAODV_def by (rule control_withinI) (auto simp del: ΓAODV_simps)

lemma aodv_wf [simp]:
  "wellformed ΓAODV"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn')  stermsl (ΓAODV 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. llabels ΓAODV p"
  by (metis aodv_labels_not_empty all_not_in_conv)

lemma aodv_ex_labelE [elim]:
  assumes "llabels ΓAODV 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 ΓAODV"
  proof
    fix pn p
    assume "psubterms(ΓAODV pn)"
    thus "∃!l. labels ΓAODV p = {l}"
    by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
  qed

lemma σAODV_labels [simp]: "(ξ, p)  σAODV i   labels ΓAODV p = {PAodv-:0}"
  unfolding σAODV_def by simp

lemma aodv_init_kD_empty [simp]:
  "(ξ, p)  σAODV i  kD (rt ξ) = {}"
  unfolding σAODV_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)  σAODV i"
    shows "sip ξ  ip ξ"
  using assms unfolding σAODV_def by simp

lemma aodv_init_sip_not_i [simp]:
  assumes "(ξ, p)  σAODV i"
    shows "sip ξ  i"
  using assms unfolding σAODV_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
  ΓAODV_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