fromUnixSeconds: from Unix seconds back to a UTC timestamp, proved

Main.lean

@@ -18,14 +18,19 @@
                       or REJECT
     compare HEX HEX   prints  <, = or >, or REJECT when either string
                       is not a timestamp
+    fromunix N        prints  the printed form of the UTC timestamp for N
+                      seconds since the epoch, or NONE when it falls
+                      outside the years 0000 to 9999; N is decimal, with
+                      an optional leading `-`
 
   A malformed request prints `error`: an unknown operation, hex digits
-  that are not in pairs, or bytes that are not UTF-8. A request line
+  that are not in pairs, bytes that are not UTF-8, or a number that is
+  not decimal. A request line
   may end in LF or CR LF.
 
   Every answer comes from the proved functions in `Rfc3339/`: `parse`,
-  `Timestamp.print`, `Timestamp.unixSeconds` and
-  `Timestamp.compareInstant`. The hex decoding and the request handling
+  `Timestamp.print`, `Timestamp.unixSeconds`,
+  `Timestamp.compareInstant` and `fromUnixSeconds`. The hex decoding and the request handling
   here are covered by the tests, not by a proof.
 -/
 
@@ -64,6 +69,11 @@ def showOrdering : Ordering → String
   | .eq => "="
   | .gt => ">"
 
+/-- A decimal number: an optional `-`, then one or more ASCII digits. -/
+def decimal (s : String) : Option Int :=
+  let ds := if s.startsWith "-" then s.drop 1 else s
+  if !ds.isEmpty && ds.all Char.isDigit then s.toInt? else none
+
 /-- The answer to one request line, or `none` when it is malformed. -/
 def request (line : String) : Option String :=
   match line.splitOn " " with
@@ -78,6 +88,11 @@ def request (line : String) : Option String :=
     pure <| match parse a, parse b with
       | some ta, some tb => showOrdering (ta.compareInstant tb)
       | _, _ => "REJECT"
+  | ["fromunix", n] => do
+    let s ← decimal n
+    pure <| match fromUnixSeconds s with
+      | some t => t.print
+      | none => "NONE"
   | _ => none
 
 /-- The line without its line ending: LF, or CR LF. -/

Proofs.lean

@@ -5,3 +5,4 @@
 -/
 
 import Proofs.Main
+import Proofs.FromUnix.Main

Proofs/FromUnix/Day.lean

@@ -0,0 +1,205 @@
+/-
+  From a day number back to a date: `yearOfDay`, `monthOfDay` and
+  `fromDayNumber`, and that a valid date's day number determines it.
+-/
+
+import Rfc3339
+import Spec.Defs
+import Proofs.DayNumber
+
+namespace Rfc3339.Proofs.FromUnix
+
+open Rfc3339
+
+/-! ### Years -/
+
+/-- `daysBeforeYear y` stays within a couple of days of `146097 * y / 400`. -/
+theorem dy_bound (y : Nat) :
+    146097 * y ≤ 400 * daysBeforeYear y + 396 ∧ 400 * daysBeforeYear y ≤ 146097 * y + 699 := by
+  unfold daysBeforeYear; omega
+
+/-- `daysBeforeYear` is strictly increasing. -/
+theorem dy_strict {a b : Nat} (h : a < b) : daysBeforeYear a < daysBeforeYear b := by
+  have := dy_bound a; have := dy_bound b; omega
+
+/-- `daysBeforeYear` is monotone. -/
+theorem dy_mono {a b : Nat} (h : a ≤ b) : daysBeforeYear a ≤ daysBeforeYear b := by
+  rcases Nat.eq_or_lt_of_le h with h | h
+  · subst h; exact Nat.le_refl _
+  · exact Nat.le_of_lt (dy_strict h)
+
+/-- The year `yearOfDay` gives is the one day `n` falls in. -/
+theorem yearOfDay_spec (n : Nat) :
+    daysBeforeYear (yearOfDay n) ≤ n ∧ n < daysBeforeYear (yearOfDay n + 1) := by
+  unfold yearOfDay
+  generalize he : n * 400 / 146097 = e
+  have h1 : 146097 * e ≤ 400 * n := by omega
+  have h2 : 400 * n < 146097 * (e + 1) := by omega
+  simp only
+  split
+  · have := dy_bound (e + 1 + 1)
+    omega
+  · split
+    · cases e with
+      | zero => simp [daysBeforeYear] at *
+      | succ k =>
+        have := dy_bound k
+        simp only [Nat.add_sub_cancel]
+        omega
+    · omega
+
+/-- The length of year `y`, from the code's leap year rule. -/
+theorem dy_yearLength (y : Nat) : Spec.yearLength y = if isLeapYear y then 366 else 365 := by
+  unfold Spec.yearLength; rw [DayNumber.isLeapYear_eq]
+
+/-! ### Months -/
+
+theorem dy_dbm_congr {y y' : Nat} (m : Nat) (h : isLeapYear y = isLeapYear y') :
+    daysBeforeMonth y m = daysBeforeMonth y' m := by
+  unfold daysBeforeMonth; rw [h]
+
+theorem dy_dim_congr {y y' : Nat} (m : Nat) (h : isLeapYear y = isLeapYear y') :
+    daysInMonth y m = daysInMonth y' m := by
+  simp only [daysInMonth, h]
+
+theorem dy_mod_congr {y y' : Nat} (doy : Nat) (h : isLeapYear y = isLeapYear y') :
+    monthOfDay y doy = monthOfDay y' doy := by
+  unfold monthOfDay; simp only [dy_dbm_congr _ h]
+
+/-- Year 0 is a leap year and year 1 is not; the tables below are for those two. -/
+theorem dy_table_leap : ∀ doy, doy < 366 →
+    1 ≤ monthOfDay 0 doy ∧ monthOfDay 0 doy ≤ 12 ∧
+    daysBeforeMonth 0 (monthOfDay 0 doy) ≤ doy ∧
+    doy < daysBeforeMonth 0 (monthOfDay 0 doy) + daysInMonth 0 (monthOfDay 0 doy) := by
+  decide +kernel
+
+theorem dy_table_common : ∀ doy, doy < 365 →
+    1 ≤ monthOfDay 1 doy ∧ monthOfDay 1 doy ≤ 12 ∧
+    daysBeforeMonth 1 (monthOfDay 1 doy) ≤ doy ∧
+    doy < daysBeforeMonth 1 (monthOfDay 1 doy) + daysInMonth 1 (monthOfDay 1 doy) := by
+  decide +kernel
+
+theorem dy_uniq_leap : ∀ m, m < 13 → 1 ≤ m → ∀ k, k < daysInMonth 0 m →
+    monthOfDay 0 (daysBeforeMonth 0 m + k) = m := by
+  decide +kernel
+
+theorem dy_uniq_common : ∀ m, m < 13 → 1 ≤ m → ∀ k, k < daysInMonth 1 m →
+    monthOfDay 1 (daysBeforeMonth 1 m + k) = m := by
+  decide +kernel
+
+theorem dy_end_leap : ∀ m, m < 13 → 1 ≤ m → daysBeforeMonth 0 m + daysInMonth 0 m ≤ 366 := by
+  decide +kernel
+
+theorem dy_end_common : ∀ m, m < 13 → 1 ≤ m → daysBeforeMonth 1 m + daysInMonth 1 m ≤ 365 := by
+  decide +kernel
+
+/-- `monthOfDay` gives the month that day `doy` of year `y` falls in. -/
+theorem dy_month (y doy : Nat) (h : doy < Spec.yearLength y) :
+    1 ≤ monthOfDay y doy ∧ monthOfDay y doy ≤ 12 ∧
+    daysBeforeMonth y (monthOfDay y doy) ≤ doy ∧
+    doy < daysBeforeMonth y (monthOfDay y doy) + daysInMonth y (monthOfDay y doy) := by
+  rw [dy_yearLength] at h
+  cases hl : isLeapYear y
+  · have e : isLeapYear y = isLeapYear 1 := by rw [hl]; rfl
+    rw [dy_mod_congr doy e, dy_dbm_congr _ e, dy_dim_congr _ e]
+    simp only [hl, Bool.false_eq_true, ite_false] at h
+    exact dy_table_common doy h
+  · have e : isLeapYear y = isLeapYear 0 := by rw [hl]; rfl
+    rw [dy_mod_congr doy e, dy_dbm_congr _ e, dy_dim_congr _ e]
+    simp only [hl, ite_true] at h
+    exact dy_table_leap doy h
+
+/-- A day within month `m` of year `y` falls in month `m`. -/
+theorem dy_month_uniq (y m k : Nat) (hm : 1 ≤ m ∧ m ≤ 12) (hk : k < daysInMonth y m) :
+    monthOfDay y (daysBeforeMonth y m + k) = m := by
+  cases hl : isLeapYear y
+  · have e : isLeapYear y = isLeapYear 1 := by rw [hl]; rfl
+    rw [dy_mod_congr _ e, dy_dbm_congr _ e]
+    rw [dy_dim_congr _ e] at hk
+    exact dy_uniq_common m (by omega) hm.1 k hk
+  · have e : isLeapYear y = isLeapYear 0 := by rw [hl]; rfl
+    rw [dy_mod_congr _ e, dy_dbm_congr _ e]
+    rw [dy_dim_congr _ e] at hk
+    exact dy_uniq_leap m (by omega) hm.1 k hk
+
+/-- A month ends within its year. -/
+theorem dy_month_end (y m : Nat) (hm : 1 ≤ m ∧ m ≤ 12) :
+    daysBeforeMonth y m + daysInMonth y m ≤ Spec.yearLength y := by
+  rw [dy_yearLength]
+  cases hl : isLeapYear y
+  · have e : isLeapYear y = isLeapYear 1 := by rw [hl]; rfl
+    rw [dy_dbm_congr _ e, dy_dim_congr _ e]
+    exact dy_end_common m (by omega) hm.1
+  · have e : isLeapYear y = isLeapYear 0 := by rw [hl]; rfl
+    rw [dy_dbm_congr _ e, dy_dim_congr _ e]
+    exact dy_end_leap m (by omega) hm.1
+
+/-! ### Dates -/
+
+/-- `fromDayNumber` gives a valid date with day number `n`, in a year no
+    later than 9999 when `n` is before 10000-01-01. -/
+theorem fromDayNumber_spec (n : Nat) (h : n < daysBeforeYear 10000) :
+    (fromDayNumber n).1 ≤ 9999 ∧
+    1 ≤ (fromDayNumber n).2.1 ∧ (fromDayNumber n).2.1 ≤ 12 ∧
+    1 ≤ (fromDayNumber n).2.2 ∧
+    (fromDayNumber n).2.2 ≤ Spec.daysInMonth (fromDayNumber n).1 (fromDayNumber n).2.1 ∧
+    Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 (fromDayNumber n).2.2 = n := by
+  obtain ⟨h1, h2⟩ := yearOfDay_spec n
+  have hy : yearOfDay n ≤ 9999 := by
+    apply Nat.le_of_not_lt
+    intro c
+    have := dy_mono (show 10000 ≤ yearOfDay n by omega)
+    omega
+  have hdoy : n - daysBeforeYear (yearOfDay n) < Spec.yearLength (yearOfDay n) := by
+    rw [DayNumber.daysBeforeYear_succ] at h2; omega
+  obtain ⟨hm1, hm2, hm3, hm4⟩ := dy_month _ _ hdoy
+  simp only [fromDayNumber]
+  refine ⟨hy, hm1, hm2, by omega, ?_, ?_⟩
+  · rw [← DayNumber.daysInMonth_eq]; omega
+  · rw [← DayNumber.dayNumber_eq _ _ _ hm1 hm2]; unfold dayNumber; omega
+
+/-- A valid date's day number lies in its year. -/
+theorem dy_dayNumber_bounds (y m d : Nat) (hm : 1 ≤ m ∧ m ≤ 12)
+    (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m) :
+    daysBeforeYear y ≤ Spec.dayNumber y m d ∧ Spec.dayNumber y m d < daysBeforeYear (y + 1) := by
+  rw [← DayNumber.dayNumber_eq _ _ _ hm.1 hm.2, DayNumber.daysBeforeYear_succ]
+  rw [← DayNumber.daysInMonth_eq] at hd
+  have := dy_month_end y m hm
+  unfold dayNumber
+  omega
+
+/-- Two valid dates with the same day number are the same date. -/
+theorem dayNumber_inj (y m d y' m' d' : Nat)
+    (hm : 1 ≤ m ∧ m ≤ 12) (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m)
+    (hm' : 1 ≤ m' ∧ m' ≤ 12) (hd' : 1 ≤ d' ∧ d' ≤ Spec.daysInMonth y' m')
+    (h : Spec.dayNumber y m d = Spec.dayNumber y' m' d') : y = y' ∧ m = m' ∧ d = d' := by
+  have b := dy_dayNumber_bounds y m d hm hd
+  have b' := dy_dayNumber_bounds y' m' d' hm' hd'
+  have hy : y = y' := by
+    rcases Nat.lt_trichotomy y y' with c | c | c
+    · have := dy_mono (show y + 1 ≤ y' by omega); omega
+    · exact c
+    · have := dy_mono (show y' + 1 ≤ y by omega); omega
+  subst hy
+  rw [← DayNumber.dayNumber_eq _ _ _ hm.1 hm.2, ← DayNumber.dayNumber_eq _ _ _ hm'.1 hm'.2] at h
+  unfold dayNumber at h
+  rw [← DayNumber.daysInMonth_eq] at hd hd'
+  have u := dy_month_uniq y m (d - 1) hm (by omega)
+  have u' := dy_month_uniq y m' (d' - 1) hm' (by omega)
+  have e : daysBeforeMonth y m + (d - 1) = daysBeforeMonth y m' + (d' - 1) := by omega
+  have hmm : m = m' := by
+    calc m = monthOfDay y (daysBeforeMonth y m + (d - 1)) := u.symm
+      _ = monthOfDay y (daysBeforeMonth y m' + (d' - 1)) := by rw [e]
+      _ = m' := u'
+  subst hmm
+  refine ⟨rfl, rfl, ?_⟩
+  omega
+
+/-- A valid date in a year no later than 9999 falls before 10000-01-01. -/
+theorem dayNumber_lt (y m d : Nat) (hy : y ≤ 9999) (hm : 1 ≤ m ∧ m ≤ 12)
+    (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m) : Spec.dayNumber y m d < daysBeforeYear 10000 := by
+  have b := dy_dayNumber_bounds y m d hm hd
+  have := dy_mono (show y + 1 ≤ 10000 by omega)
+  omega
+
+end Rfc3339.Proofs.FromUnix

Proofs/FromUnix/Main.lean

@@ -0,0 +1,133 @@
+/-
+  `fromUnixSeconds` against the spec, from the lemmas in `Day.lean` and
+  the first slice's proofs of `unixSeconds` and the day number.
+-/
+
+import Rfc3339
+import Spec.Defs
+import Proofs.DayNumber
+import Proofs.Instant
+import Proofs.FromUnix.Day
+
+namespace Rfc3339.Proofs.FromUnix
+
+open Rfc3339
+
+/-- `daysBeforeYear 10000`: the days before 10000-01-01. -/
+theorem fu_daysBeforeYear_10000 : daysBeforeYear 10000 = 3652425 := by decide
+
+/-- A UTC timestamp's Unix seconds, shifted to count from 0000-01-01:
+    its day number in seconds, plus the time of day. -/
+theorem fu_unixSeconds_z (t : Timestamp) (hz : t.offset = .z) :
+    Spec.unixSeconds t + 719528 * 86400 =
+      ((Spec.dayNumber t.year t.month t.day * 86400 + t.hour * 3600 + t.minute * 60 +
+        t.second : Nat) : Int) := by
+  unfold Spec.unixSeconds Spec.utcMinute
+  rw [hz, Instant.dayNumber_epoch]
+  simp only [Spec.offsetMinutes]
+  omega
+
+/-- The first second of the range. -/
+theorem fu_unixSeconds_lo : Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 := by
+  decide +kernel
+
+/-- The last second of the range. -/
+theorem fu_unixSeconds_hi :
+    Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 := by
+  decide +kernel
+
+end Rfc3339.Proofs.FromUnix
+
+open Rfc3339
+
+theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) :
+    Rfc3339.fromUnixSeconds s = some t ↔
+      Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧
+        Spec.unixSeconds t = s := by
+  have hD := Proofs.FromUnix.fu_daysBeforeYear_10000
+  constructor
+  · intro h
+    unfold Rfc3339.fromUnixSeconds at h
+    dsimp only at h
+    split at h
+    · rename_i hr
+      have hn : (s + 719528 * 86400).toNat / 86400 < daysBeforeYear 10000 := by omega
+      have hs := Proofs.FromUnix.fromDayNumber_spec _ hn
+      generalize fromDayNumber ((s + 719528 * 86400).toNat / 86400) = p at h hs
+      obtain ⟨y, m, d⟩ := p
+      simp only [Option.some.injEq] at h
+      subst h
+      obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hs
+      have hu := Proofs.FromUnix.fu_unixSeconds_z
+        ⟨y, m, d, (s + 719528 * 86400).toNat % 86400 / 3600,
+          (s + 719528 * 86400).toNat % 86400 % 3600 / 60, (s + 719528 * 86400).toNat % 86400 % 60,
+          [], .z⟩ rfl
+      simp only at h1 h2 h3 h4 h5 h6 hu
+      rw [h6] at hu
+      refine ⟨⟨h1, h2, h3, h4, h5, ?_, ?_, ?_, ?_, ?_, ?_⟩, rfl, rfl, ?_, ?_⟩
+      · show _ / 3600 ≤ 23; omega
+      · show _ % 3600 / 60 ≤ 59; omega
+      · show _ % 60 ≤ 60; omega
+      · intro h60; exfalso; change _ % 60 = 60 at h60; omega
+      · intro x hx; cases hx
+      · trivial
+      · show _ % 60 ≤ 59; omega
+      · omega
+    · contradiction
+  · rintro ⟨hv, hz, hf, hs59, hu⟩
+    obtain ⟨y, m, d, hh, mi, sec, fr, off⟩ := t
+    simp only at hz hf hs59 hu
+    subst hz hf
+    obtain ⟨hy, hm1, hm2, hd1, hd2, hh23, hmi, -, -, -, -⟩ := hv
+    have hu' := Proofs.FromUnix.fu_unixSeconds_z ⟨y, m, d, hh, mi, sec, [], .z⟩ rfl
+    simp only at hu' hy hm1 hm2 hd1 hd2 hh23 hmi
+    rw [hu] at hu'
+    have hN := Proofs.FromUnix.dayNumber_lt y m d hy ⟨hm1, hm2⟩ ⟨hd1, hd2⟩
+    unfold Rfc3339.fromUnixSeconds
+    dsimp only
+    split
+    case isFalse hr => exfalso; omega
+    have hn : (s + 719528 * 86400).toNat / 86400 = Spec.dayNumber y m d := by omega
+    have hsec : (s + 719528 * 86400).toNat % 86400 = hh * 3600 + mi * 60 + sec := by omega
+    rw [hn, hsec]
+    have hs := Proofs.FromUnix.fromDayNumber_spec _ hN
+    generalize fromDayNumber (Spec.dayNumber y m d) = p at hs ⊢
+    obtain ⟨y', m', d'⟩ := p
+    obtain ⟨-, h2, h3, h4, h5, h6⟩ := hs
+    simp only at h2 h3 h4 h5 h6
+    obtain ⟨rfl, rfl, rfl⟩ :=
+      Proofs.FromUnix.dayNumber_inj y' m' d' y m d ⟨h2, h3⟩ ⟨h4, h5⟩ ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ h6
+    simp only [Option.some.injEq, Timestamp.mk.injEq, true_and, and_true]
+    and_intros <;> omega
+
+theorem Spec.fromUnixSeconds_isSome (s : Int) :
+    (Rfc3339.fromUnixSeconds s).isSome ↔
+      Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧
+        s ≤ Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by
+  rw [Proofs.FromUnix.fu_unixSeconds_lo, Proofs.FromUnix.fu_unixSeconds_hi]
+  have hD := Proofs.FromUnix.fu_daysBeforeYear_10000
+  unfold Rfc3339.fromUnixSeconds
+  dsimp only
+  split
+  · rename_i hr
+    generalize fromDayNumber ((s + 719528 * 86400).toNat / 86400) = p
+    obtain ⟨y, m, d⟩ := p
+    simp only [Option.isSome_some, true_iff]
+    omega
+  · rename_i hr
+    simp only [Option.isSome_none, Bool.false_eq_true, false_iff]
+    omega
+
+theorem Spec.fromUnixSeconds_vectors :
+    Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds 2147483647 = some ⟨2038, 1, 19, 3, 14, 7, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds (-1) = some ⟨1969, 12, 31, 23, 59, 59, [], .z⟩ ∧
+    Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 ∧
+    Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 ∧
+    Rfc3339.fromUnixSeconds (-62167219200) = some ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds 253402300799 = some ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ ∧
+    Rfc3339.fromUnixSeconds (-62167219201) = none ∧
+    Rfc3339.fromUnixSeconds 253402300800 = none := by
+  and_intros <;> decide +kernel