Theory Zeroconf_Analysis

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

section ‹Formalizing the IPv4-address allocation in ZeroConf›

theory Zeroconf_Analysis
  imports "../Discrete_Time_Markov_Chain"
begin

declare UNIV_bool[simp]

subsection ‹Definition of a ZeroConf allocation run›

datatype zc_state = start
                  | probe nat
                  | ok
                  | error

lemma inj_probe: "inj_on probe X"
  by (auto simp: inj_on_def)

text ‹Countability of @{typ zc_state} simplifies measurability of functions on @{typ zc_state}.›

instance zc_state :: countable
proof
  have "countable ({start, ok, error} ∪ probe`UNIV)"
    by auto
  also have "{start, ok, error} ∪ probe`UNIV = UNIV"
    using zc_state.nchotomy by auto
  finally show "∃f::zc_state ⇒ nat. inj f"
    using inj_on_to_nat_on[of "UNIV :: zc_state set"] by auto
qed

locale Zeroconf_Analysis =
  fixes N :: nat and p q r e :: real
  assumes p: "0 < p" "p < 1" and q: "0 < q" "q < 1"
  assumes r[simp]: "0 ≤ r" and e[simp]: "0 ≤ e"
begin

lemma p_bounds[simp]: "0 ≤ p" "p ≤ 1"
  using p by auto

lemma q_bounds[simp]: "0 ≤ q" "q ≤ 1"
  using q by auto

abbreviation states where
  "states ≡ probe ` {.. N} ∪ {start, ok, error}"

primrec τ :: "zc_state ⇒ zc_state pmf" where
  "τ start     = map_pmf (λTrue ⇒ probe 0 | False ⇒ ok) (bernoulli_pmf q)"
| "τ (probe n) = map_pmf (λTrue ⇒ (if n < N then probe (Suc n) else error) | False ⇒ start) (bernoulli_pmf p)"
| "τ ok        = return_pmf ok"
| "τ error     = return_pmf error"

primrec ρ :: "zc_state ⇒ zc_state ⇒ real" where
  "ρ start     = (λ_. 0) (probe 0 := r, ok := r * (N + 1))"
| "ρ (probe n) = (if n < N then (λ_. 0) (probe (Suc n) := r) else (λ_. 0) (error := e))"
| "ρ ok        = (λ_. 0) (ok := 0)"
| "ρ error     = (λ_. 0) (error := 0)"

lemma ρ_nonneg'[simp]: "0 ≤ ρ s t"
  using r e by (cases s) auto

sublocale MC_with_rewards τ ρ "λs. 0"
  proof qed (simp_all add: pair_measure_countable)

subsection ‹The allocation run is a rewarded DTMC›

abbreviation "E s ≡ set_pmf (τ s)"

lemma enabled_ok: "enabled ok ω ⟷ ω = sconst ok"
  by (simp add: enabled_iff_sconst)

lemma finite_E[intro, simp]: "finite (E s)"
  by (cases s) auto

lemma E_closed: "s ∈ states ⟹ E s ⊆ states"
  using p q by (cases s) (auto split: bool.splits)

lemma enabled_error: "enabled error ω ⟷ ω = sconst error"
  by (simp add: enabled_iff_sconst)

lemma pos_neg_q_pn: "0 < 1 - q * (1 - p^Suc N)"
proof -
  have "p ^ Suc N ≤ 1 ^ Suc N"
    using p by (intro power_mono) auto
  with p q have "q * (1 - p^Suc N) < 1 * 1"
    by (intro mult_strict_mono) (auto simp: field_simps simp del: power_Suc)
  then show ?thesis by simp
qed

lemma to_error: assumes "n ≤ N" shows "(probe n, error) ∈ acc"
  using ‹n ≤ N›
proof (induction rule: inc_induct)
  case (step n') with p show ?case
    by (intro rtrancl_trans[OF r_into_rtrancl step.IH]) auto
qed (insert p, auto)

subsection ‹Probability of a erroneous allocation›

definition "P_err s = 𝒫(ω in T s. ev (HLD {error}) (s ## ω))"

lemma P_err:
  defines "p_start == (q * p ^ Suc N) / (1 - q * (1 - p ^ Suc N))"
  defines "p_probe == (λn. p ^ Suc (N - n) + (1 - p^Suc (N - n)) * p_start)"
  assumes s: "s ∈ states - {ok, error}"
  shows "P_err s = (case s of ok ⇒ 0 | error ⇒ 1 | probe n ⇒ p_probe n | start ⇒ p_start)"
    (is "… = ?E s")
  using s
proof (rule unique_les)
  have [arith]: "0 ≤ p * (q * p ^ N)"
    using p q by simp
  have p_eq: "p_start = p_probe 0 * q"
    "⋀n. n < N ⟹ p_probe n = p_probe (Suc n) * p + p_start * (1 - p)"
    "p_probe N = p + p_start * (1 - p)"
    using p q
    by (auto simp: p_probe_def p_start_def power_Suc[symmetric] Suc_diff_Suc divide_simps
             simp del: power_Suc)
       (auto simp: field_simps)
  fix s assume s: "s ∈ states - {ok, error}"
  then show "?E s = (∫t. ?E t ∂τ s) + 0"
    using p q by (auto intro: p_eq)
  show "∃t∈{ok, error}. (s, t) ∈ acc"
    using s q to_error by auto
  from s show "P_err s = integral⇧L (measure_pmf (τ s)) P_err + 0"
    unfolding P_err_def[abs_def] by (subst prob_T) (auto simp: ev_Stream simp del: UNIV_bool)
next
  fix s assume "s ∈ {ok, error}" then show "P_err s = ?E s"
    by (auto intro!: T.prob_eq_0_AE T.prob_Collect_eq_1[THEN iffD2]
             simp: P_err_def AE_sconst ev_sconst HLD_iff ev_Stream T.prob_space
             simp del: space_T sets_T )
qed (insert p q, auto intro!: integrable_measure_pmf_finite split: if_split_asm)

lemma P_err_start: "P_err start = (q * p ^ Suc N) / (1 - q * (1 - p ^ Suc N))"
  by (simp add: P_err)

subsection ‹An allocation run terminates almost surely›

lemma states_closed:
  assumes "s ∈ states"
  assumes "(s, t) ∈ acc_on (- {error, ok})"
  shows "t ∈ states"
  using assms(2,1) p q by induction (auto split: if_split_asm)

lemma finite_reached:
  assumes s: "s ∈ states" shows "finite (acc_on (- {error, ok}) `` {s})"
  using states_closed[OF s]
  by (rule_tac finite_subset[of _ states]) auto

lemma AE_reaches_error_or_ok:
  assumes s: "s ∈ states"
  shows "AE ω in T s. ev (HLD {error, ok}) ω"
proof (rule AE_T_ev_HLD)
  { fix t assume t: "(s, t) ∈ acc_on (- {error, ok})"
    with states_closed[OF s t] to_error p q show "∃t'∈{error, ok}. (t, t') ∈ acc"
      by auto }
qed (rule finite_reached[OF s])

subsection ‹Expected runtime of an allocation run›

definition "R s = (∫⇧+ ω. reward_until {error, ok} s ω ∂T s)"

definition "R' s = enn2real (R s)"

lemma R_iter: "s ≠ error ⟹ s ≠ ok ⟹ R s = (∫⇧+t. ennreal (ρ s t) + R t ∂τ s)"
  unfolding R_def using T.emeasure_space_1
  by (subst nn_integral_T)
     (auto simp del: τ.simps ρ.simps simp add: AE_measure_pmf_iff nn_integral_add
           intro!: nn_integral_cong_AE)

lemma R_finite:
  assumes s: "s ∈ states"
  shows "R s ≠ ∞"
  unfolding R_def
proof (rule nn_integral_reward_until_finite)
  { fix t assume "(s, t) ∈ acc" from this s p q have "t ∈ states"
      by induction (auto split: if_split_asm) }
  then have "acc `` {s} ⊆ states"
    by auto
  then show "finite (acc `` {s})"
    by (auto dest: finite_subset)
qed (auto simp: AE_reaches_error_or_ok[OF s])

lemma R_less_top: "s ∈ states ⟹ R s < top"
  using R_finite[of s] by (subst less_top[symmetric]) simp

lemma R'_iter: assumes s: "s ∈ states" "s ≠ error" "s ≠ ok" shows "R' s = (∫t. ρ s t + R' t ∂τ s)"
  unfolding R'_def R_iter[OF s(2,3)]
proof (rule enn2real_nn_integral_eq_integral)
  have "t ∈ E s ⟹ R t < top" for t
    using ‹s∈states› E_closed[of s] by (intro R_less_top) auto
  then show "AE t in τ s. ennreal (ρ s t) + R t = ennreal (ρ s t + enn2real (R t))"
    by (auto simp: AE_measure_pmf_iff intro!: ennreal_enn2real[symmetric])
qed auto

lemma cost_from_start:
  "R' start =
    (q * (r + p^Suc N * e + r * p * (1 - p^N) / (1 - p)) + (1 - q) * (r * Suc N)) /
    (1 - q + q * p^Suc N)"
proof -
  have ok_error: "R' ok = 0 ∧ R' error = 0"
    unfolding R'_def R_def by (subst (1 2) reward_until_unfold[abs_def]) simp

  then have R_start: "R' start = q * (r + R' (probe 0)) + (1 - q) * (r * (N + 1))"
    using q r by (subst R'_iter) (simp_all add: field_simps)

  have R_probe: "⋀n. n < N ⟹ R' (probe n) = p * R' (probe (Suc n)) + p * r + (1 - p) * R' start"
    using p r by (subst R'_iter) (simp_all add: field_simps distrib_right)

  have R_N: "R' (probe N) = p * e + (1 - p) * R' start"
    using p e ok_error by (subst R'_iter) (auto simp: mult.commute )

  { fix n
    assume "n ≤ N"
    then have "R' (probe (N - n)) =
      p ^ Suc n * e + (1 - p^n) * r * p / (1 - p) + (1 - p^Suc n) * R' start"
    proof (induct n)
      case 0 with R_N show ?case by simp
    next
      case (Suc n)
      moreover then have "Suc (N - Suc n) = N - n" by simp
      ultimately show ?case
        using R_probe[of "N - Suc n"] p by (simp_all add: field_simps Suc)
    qed }
  from this[of N]
  have [simp]: "R' (probe 0) = p ^ Suc N * e + (1 - p^N) * r * p / (1 - p) + (1 - p^Suc N) * R' start"
    by simp
  have "R' start - q * (1 - p^Suc N) * R' start =
    q * (r + p^Suc N * e + (1 - p^N) * r * p / (1 - p)) + (1 - q) * (r * (N + 1))"
    by (subst R_start) (simp_all add: field_simps)
  then have "R' start = (q * (r + p^Suc N * e + (1 - p^N) * r * p / (1 - p)) + (1 - q) * (r * Suc N)) /
    (1 - q * (1 - p^Suc N))"
    using pos_neg_q_pn by (simp_all add: field_simps)
  then show ?thesis
    by (simp add: field_simps)
qed

end

interpretation ZC: Zeroconf_Analysis 2 "16 / 65024 :: real" "0.01" "0.002" "3600"
  by standard auto

lemma "ZC.P_err start ≤ 1 / 10^12"
  unfolding ZC.P_err_start by (simp add: power_divide power_one_over[symmetric])

lemma "ZC.R' start ≤ 0.007"
  unfolding ZC.cost_from_start by (simp add: power_divide power_one_over[symmetric])

end