totalRecoveryCost

formal source

  47/-! ## §2. Total J-cost of n-bit key recovery -/
  48
  49/-- Total J-cost of recovering an `n`-bit key (additive over bits). -/
  50def totalRecoveryCost (n : ℕ) : ℝ := (n : ℝ) * perBitCost
  51
  52theorem totalRecoveryCost_zero : totalRecoveryCost 0 = 0 := by
  53  unfold totalRecoveryCost; simp
  54
  55theorem totalRecoveryCost_succ (n : ℕ) :
  56    totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost := by
  57  unfold totalRecoveryCost; push_cast; ring
  58
  59theorem totalRecoveryCost_pos {n : ℕ} (h : 1 ≤ n) : 0 < totalRecoveryCost n := by
  60  unfold totalRecoveryCost
  61  exact mul_pos (by exact_mod_cast (by omega : 0 < n)) perBitCost_pos
  62
  63/-- Total cost is strictly monotonic in key size. -/
  64theorem totalRecoveryCost_strict_mono {n m : ℕ} (h : n < m) :
  65    totalRecoveryCost n < totalRecoveryCost m := by
  66  unfold totalRecoveryCost
  67  have h_real : (n : ℝ) < (m : ℝ) := by exact_mod_cast h
  68  exact (mul_lt_mul_iff_of_pos_right perBitCost_pos).mpr h_real
  69
  70/-! ## §3. Doubling-key-size cost identity -/
  71
  72/-- Doubling the key size doubles the recovery cost. -/
  73theorem totalRecoveryCost_double (n : ℕ) :
  74    totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n := by
  75  unfold totalRecoveryCost
  76  push_cast
  77  ring
  78
  79/-! ## §4. Master certificate -/
  80