Theory B_Aodv_Predicates

(*  Title:       variants/b_fwdrreps/Aodv_Predicates.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
*)

section "Invariant assumptions and properties"

theory B_Aodv_Predicates
imports B_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