From 53c087b7370995dbbec46be37ac8e2dcc159f0a1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 03:48:01 +0000 Subject: [PATCH 1/2] Add fromUnixSeconds: from Unix seconds back to a UTC timestamp, proved Rfc3339.fromUnixSeconds gives, for whole seconds since the epoch, the UTC timestamp with no fraction and no leap second that names them, for every second from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and none outside. Its year comes from an estimate, n * 400 / 146097, that is off by at most one and is then settled by the year's first day; its month from how many months start on or before the day. Three statements, all proved: - Spec.fromUnixSeconds_iff: the result is exactly the timestamp that is valid, in UTC, with no fraction and a second of at most 59, and whose Spec.unixSeconds is the input. So each second has one such timestamp. - Spec.fromUnixSeconds_isSome: it gives one exactly within the range. - Spec.fromUnixSeconds_vectors: the epoch, the section 5.8 example, a leap day, 2^31 - 1, -1, and the ends of the range and one past each. lake comparator --paranoid accepts all 17 theorems. The tool answers `fromunix N`, and the tests, against datetime arithmetic with year 0 moved by 400 years, run 300,000 inputs with 0 failures, 56,056 of them `fromunix`, including the first second of every year from 0000 to 9999. Seven planted bugs each make them fail; an eighth, an average year of 365.25 days in the estimate, changes nothing within the range. Plan and claim: #1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Main.lean | 21 +++- Proofs.lean | 1 + Proofs/FromUnix/Day.lean | 205 ++++++++++++++++++++++++++++++++++++++ Proofs/FromUnix/Main.lean | 133 +++++++++++++++++++++++++ README.md | 8 +- Rfc3339.lean | 1 + Rfc3339/FromUnix.lean | 45 +++++++++ SPEC.md | 16 ++- Spec.lean | 34 +++++++ bar.toml | 1 + comparator.json | 27 ++++- tests/TEST-RESULTS.md | 13 +-- tests/run_tests.py | 81 +++++++++++++++ 13 files changed, 567 insertions(+), 19 deletions(-) create mode 100644 Proofs/FromUnix/Day.lean create mode 100644 Proofs/FromUnix/Main.lean create mode 100644 Rfc3339/FromUnix.lean diff --git a/Main.lean b/Main.lean index 3767388..a376174 100644 --- a/Main.lean +++ b/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. -/ diff --git a/Proofs.lean b/Proofs.lean index a0c5328..fb97a93 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -5,3 +5,4 @@ -/ import Proofs.Main +import Proofs.FromUnix.Main diff --git a/Proofs/FromUnix/Day.lean b/Proofs/FromUnix/Day.lean new file mode 100644 index 0000000..51acbe1 --- /dev/null +++ b/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 diff --git a/Proofs/FromUnix/Main.lean b/Proofs/FromUnix/Main.lean new file mode 100644 index 0000000..39cb49d --- /dev/null +++ b/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 diff --git a/README.md b/README.md index d3ace0d..21bca35 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,7 @@ For each timestamp it prints the timestamp as written, with `T` and `Z` in upper - `Timestamp.isValid` - `Timestamp.unixSeconds` - `Timestamp.compareInstant` +- `Rfc3339.fromUnixSeconds` `SPEC.md` says what each one does. @@ -39,13 +40,16 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF | `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction, compared exactly. | `Spec.compareInstant_eq` | | The examples of section 5.8 parse to the fields the RFC gives. What the RFC says about them holds: `1996-12-19T16:39:57-08:00` is the instant `1996-12-20T00:39:57Z`, and `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. Separately, `1985-04-12T23:20:50.52Z` is 482196050 seconds after the epoch, as Python's `calendar.timegm` also gives. | `Spec.rfc3339_examples`, `Spec.rfc3339_example_instants` | | A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` | +| `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` | +| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Spec.fromUnixSeconds_isSome` | +| `fromUnixSeconds` gives the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` | | The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` | The command-line tool in `Main.lean` calls these functions directly. ## What is not proved -- Reading requests and printing answers in `Main.lean`: the hex decoding and UTF-8 check in `serve` mode, the arguments, output and exit codes of `check` mode, and the decimal printing of numbers. The differential tests cover them, with malformed requests and CR LF line endings. +- Reading requests and printing answers in `Main.lean`: the hex decoding and UTF-8 check in `serve` mode, the arguments, output and exit codes of `check` mode, and the decimal printing of numbers and reading of the numbers `fromunix` takes. The differential tests cover them, with malformed requests and CR LF line endings. - Whether a leap second was announced. Second 60 is accepted at 23:59 UTC at the end of any month, without a table of leap seconds, where section 5.7 allows it only at the end of months in which a leap second occurs. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. - Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. - Forms outside RFC 3339 are not supported, by design: @@ -95,7 +99,7 @@ The test script compares the tool with Python's `datetime` and `calendar` module ## Layout - `Rfc3339/Types.lean`: the timestamp and offset types. It is part of the specification. -- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`: the code under proof. +- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`, `Rfc3339/FromUnix.lean`: the code under proof. - `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. - `Spec/Defs.lean`: the definitions the statements use, written from the RFC, with checks against its tables and known day counts. - `Proofs.lean` and `Proofs/`: the proofs, under the same names. diff --git a/Rfc3339.lean b/Rfc3339.lean index 4945aaa..e4a567a 100644 --- a/Rfc3339.lean +++ b/Rfc3339.lean @@ -7,3 +7,4 @@ import Rfc3339.Types import Rfc3339.Calendar import Rfc3339.Format import Rfc3339.Instant +import Rfc3339.FromUnix diff --git a/Rfc3339/FromUnix.lean b/Rfc3339/FromUnix.lean new file mode 100644 index 0000000..82ff2f1 --- /dev/null +++ b/Rfc3339/FromUnix.lean @@ -0,0 +1,45 @@ +/- + From Unix seconds back to a timestamp: the UTC timestamp, with no + fraction and no leap second, that names a given second. +-/ + +import Rfc3339.Instant + +namespace Rfc3339 + +/-- The year that day `n` falls in, counting 0000-01-01 as day 0. A year + averages 146097 / 400 days, so `n * 400 / 146097` is off by at most + one; the year's first day settles it. -/ +def yearOfDay (n : Nat) : Nat := + let y := n * 400 / 146097 + if daysBeforeYear (y + 1) ≤ n then y + 1 + else if n < daysBeforeYear y then y - 1 + else y + +/-- The month that day `doy` of year `y` falls in, counting the first of + January as day 0: how many months start on or before it. -/ +def monthOfDay (y doy : Nat) : Nat := + ((List.range 12).filter fun i => daysBeforeMonth y (i + 1) ≤ doy).length + +/-- Year, month and day of day `n`, counting 0000-01-01 as day 0. -/ +def fromDayNumber (n : Nat) : Nat × Nat × Nat := + let y := yearOfDay n + let doy := n - daysBeforeYear y + let m := monthOfDay y doy + (y, m, doy - daysBeforeMonth y m + 1) + +/-- The UTC timestamp for `s` seconds since 1970-01-01T00:00:00Z, with + offset `Z`, no fraction and a second of at most 59; `none` before + 0000-01-01T00:00:00Z or after 9999-12-31T23:59:59Z. 719528 is + `dayNumber 1970 1 1`. -/ +def fromUnixSeconds (s : Int) : Option Timestamp := + let t := s + 719528 * 86400 + if 0 ≤ t ∧ t < (daysBeforeYear 10000 : Int) * 86400 then + let n := t.toNat / 86400 + let secs := t.toNat % 86400 + let (y, m, d) := fromDayNumber n + some { year := y, month := m, day := d, hour := secs / 3600, minute := secs % 3600 / 60, + second := secs % 60, fraction := [], offset := .z } + else none + +end Rfc3339 diff --git a/SPEC.md b/SPEC.md index fde8296..1bbacf9 100644 --- a/SPEC.md +++ b/SPEC.md @@ -44,9 +44,15 @@ POSIX time has no number for a leap second. As in POSIX time, second 60 is count `Timestamp.compareInstant` orders two valid timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second, 60, comes after 59, then by the fraction, compared exactly. It does not use Unix seconds, so `1990-12-31T23:59:60Z` comes before `1991-01-01T00:00:00Z`. It gives `eq` when the instants are equal, as for `2000-01-01T00:00:00.5Z` and `2000-01-01T01:00:00.500+01:00`. +## From Unix seconds + +`fromUnixSeconds` goes the other way: from whole seconds since 1970-01-01T00:00:00Z to the UTC timestamp for that second. Its result is valid, has offset `Z`, no fraction, and a second of at most 59, and names exactly the second it was given. Each second has exactly one such timestamp, and this is it. A leap second is never a result, since its number is the same as the next second's. + +It covers every second from `0000-01-01T00:00:00Z` (-62167219200) to `9999-12-31T23:59:59Z` (253402300799), the years RFC 3339 allows, and returns `none` outside them. So `fromUnixSeconds t.unixSeconds` puts any valid timestamp, whatever its offset, into UTC, dropping its fraction, unless that moves it outside those years. + ## Errors -`parse` returns `none` for any string it does not accept. No function can fail any other way. +`parse` returns `none` for any string it does not accept, and `fromUnixSeconds` for any number outside the years 0000 to 9999. No function can fail any other way. ## The command-line tool @@ -55,7 +61,7 @@ The command-line tool in `Main.lean` has two modes: - `rfc3339 check TIMESTAMP...` prints each timestamp's printed form and its Unix seconds, or `invalid`. It exits with 1 when any timestamp is invalid. - `rfc3339 serve` answers requests from the differential tests, one per line. Each string is sent as the hex digits of its UTF-8 bytes. The header comment of `Main.lean` gives the protocol. -Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds` and `Timestamp.compareInstant`. +Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds`, `Timestamp.compareInstant` and `fromUnixSeconds`. ## What must always hold @@ -77,11 +83,15 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | Days outside their month are rejected, with the leap year rule of Appendix C. | `Spec.calendar_vectors` | | Second 60 is accepted only at the end of a month in UTC. | `Spec.leap_second_vectors` | | Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Spec.syntax_vectors` | +| `fromUnixSeconds s` is `t` exactly when `t` is valid, in UTC, with no fraction and a second of at most 59, and names `s`. | `Spec.fromUnixSeconds_iff` | +| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z. | `Spec.fromUnixSeconds_isSome` | +| The epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` | Together, these fix every output for valid input. - `parse` is fixed for every string. - `print`, `unixSeconds` and `compareInstant` are fixed for every valid timestamp. The parser gives only valid timestamps. +- `fromUnixSeconds` is fixed for every number, by `Spec.fromUnixSeconds_iff` and `Spec.fromUnixSeconds_isSome`. - A parser that accepted nothing would meet `Spec.parse_valid`, but it would fail `Spec.parse_iff` and `Spec.parse_print`. - A parser that accepted too much would fail `Spec.parse_iff`. @@ -89,5 +99,5 @@ Together, these fix every output for valid input. The differential tests compare the tool with two oracles: -- Python's `datetime` and `calendar` modules: month lengths, offset arithmetic, seconds since the epoch, and `datetime.fromisoformat` on every accepted string it can hold. +- Python's `datetime` and `calendar` modules: month lengths, offset arithmetic, seconds since the epoch, `datetime.fromisoformat` on every accepted string it can hold, and the UTC timestamp for a number of seconds. `datetime` holds no year 0, so dates there are moved by 400 years, one cycle of the Gregorian calendar, for the arithmetic. - A copy of the rules above, written in Python from the RFC. diff --git a/Spec.lean b/Spec.lean index e2c8bab..2b77caa 100644 --- a/Spec.lean +++ b/Spec.lean @@ -140,3 +140,37 @@ theorem Spec.syntax_vectors : parse "1985-04-12T23:20:50" = none ∧ parse "1985-04-12T23:20:50Z " = none ∧ parse "1985-04-12T24:00:00Z" = none := sorry + +/-! ## From Unix seconds -/ + +/-- `fromUnixSeconds s` is the one timestamp that is valid, in UTC + (offset `Z`), with no fraction and no leap second, and that names + the second `s`. -/ +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 := sorry + +/-- It gives a timestamp exactly for the seconds from + 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, the years RFC 3339 + allows. -/ +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⟩ := sorry + +/-- The epoch; the example of section 5.8; a leap day; the last second a + signed 32-bit count reaches; the second before the epoch; the ends of + the range, and one second past each. -/ +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 := sorry diff --git a/bar.toml b/bar.toml index 628cd30..505ea7d 100644 --- a/bar.toml +++ b/bar.toml @@ -20,6 +20,7 @@ files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Rfc3339/Types.lean"] code = [ "Rfc3339.parse", "Rfc3339.Timestamp.print", "Rfc3339.Timestamp.isValid", "Rfc3339.Timestamp.unixSeconds", "Rfc3339.Timestamp.compareInstant", + "Rfc3339.fromUnixSeconds", ] # One entry per approval, added in a pull request the reviewer approves. diff --git a/comparator.json b/comparator.json index c9b283c..60399c4 100644 --- a/comparator.json +++ b/comparator.json @@ -2,10 +2,27 @@ "challenge_module": "Spec", "solution_module": "Proofs", "theorem_names": [ - "Spec.isValid_iff", "Spec.print_eq", "Spec.parse_iff", "Spec.parse_valid", - "Spec.parse_print", "Spec.print_parse", "Spec.unixSeconds_eq", "Spec.compareInstant_eq", - "Spec.rfc3339_examples", "Spec.rfc3339_example_instants", "Spec.leap_second_order", "Spec.calendar_vectors", - "Spec.leap_second_vectors", "Spec.syntax_vectors" + "Spec.isValid_iff", + "Spec.print_eq", + "Spec.parse_iff", + "Spec.parse_valid", + "Spec.parse_print", + "Spec.print_parse", + "Spec.unixSeconds_eq", + "Spec.compareInstant_eq", + "Spec.rfc3339_examples", + "Spec.rfc3339_example_instants", + "Spec.leap_second_order", + "Spec.calendar_vectors", + "Spec.leap_second_vectors", + "Spec.syntax_vectors", + "Spec.fromUnixSeconds_iff", + "Spec.fromUnixSeconds_isSome", + "Spec.fromUnixSeconds_vectors" ], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] } diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index cea4270..bb0dd24 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,12 +6,13 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 300000 -- Mutated: 98931 of the inputs are mutated timestamps -- By kind: compare 42725, error 18, grid 16998, mutated 98931, near miss 42347, valid 98981 -- Strings parsed: 257257, of which 118758 accepted (6407 with a leap second) and 138499 rejected -- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 110381 -- Pairs ordered: 42725 (14309 before, 12000 same instant, 14324 after, 2092 with a string rejected) -- Malformed requests answered `error`: 18 of 18 +- Mutated: 79241 of the inputs are mutated timestamps +- By kind: compare 34149, error 27, fromunix 56056, grid 16998, mutated 79241, near miss 33926, valid 79603 +- Strings parsed: 209768, of which 96503 accepted (5227 with a leap second) and 113265 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 89586 +- Pairs ordered: 34149 (11557 before, 9582 same instant, 11345 after, 1665 with a string rejected) +- Unix seconds turned back into timestamps: 56056, of which 1278 outside years 0000 to 9999 +- Malformed requests answered `error`: 27 of 27 - Requests ending in CR LF: every seventh, 42857 - Strings also given to `rfc3339 check` as arguments, in batches of 500: 20000, and once with no arguments - Last lines with no LF, sent alone, answered right: 2 of 2 diff --git a/tests/run_tests.py b/tests/run_tests.py index 21493b8..b278528 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -34,6 +34,13 @@ - pairs of timestamps to order, including pairs that name the same instant with different offsets or fractions, leap seconds next to the seconds around them, and pairs with a string that is rejected; +- Unix seconds to turn back into timestamps: the ends of the range and + one second past each, the first second of every month of years + chosen for the leap year rule and of every year from 0000 to 9999, + with the seconds either side, random + seconds in and around the range, and the seconds of valid timestamps. + `datetime` arithmetic gives the expected UTC timestamp, with year 0 + moved by 400 years as above; - malformed requests, which the tool must answer with `error`. Every seventh request ends in CR LF. The first 20,000 parsed strings @@ -79,6 +86,48 @@ CYCLE_DAYS = 146097 +# 0000-01-01T00:00:00Z and 9999-12-31T23:59:59Z in Unix seconds. +FIRST, LAST = -62167219200, 253402300799 + + +def unix_of(year, month, day, hour=0, minute=0, second=0): + """Seconds since the epoch of a UTC date and time, by `datetime`.""" + moved, days = shifted(year) + delta = datetime(moved, month, day, hour, minute, second, tzinfo=timezone.utc) - EPOCH + return (delta.days - days) * 86400 + delta.seconds + + +def from_unix(n): + """The expected answer to `fromunix n`: the UTC timestamp, by + `datetime` arithmetic, or NONE outside years 0000 to 9999.""" + if not FIRST <= n <= LAST: + return "NONE" + shift = 0 + if n < unix_of(2, 1, 1): + n, shift = n + CYCLE_DAYS * 86400, 400 + d = EPOCH + timedelta(seconds=n) + return (f"{d.year - shift:04d}-{d.month:02d}-{d.day:02d}T" + f"{d.hour:02d}:{d.minute:02d}:{d.second:02d}Z") + + +def unix_grid(): + """The ends of the range and one second past each, numbers at the + edges of 32-bit counts, and the first second of every month of years + chosen for the leap year rule, with the seconds either side.""" + yield from (FIRST - 1, FIRST, FIRST + 1, LAST - 1, LAST, LAST + 1, 0, -1, 1, + 2 ** 31 - 1, 2 ** 31, -2 ** 31, 2 ** 32, 10 ** 20, -10 ** 20) + for year in (0, 1, 3, 4, 99, 100, 101, 399, 400, 1582, 1600, 1700, 1800, 1900, 1969, + 1970, 2000, 2024, 2100, 2400, 9996, 9998, 9999): + for month in range(2, 13): + start = unix_of(year, month, 1) + yield from (start - 1, start, start + 1) + # The first second of every year, and the seconds either side: where + # a year begins against where an average year would put it. + for year in range(10000): + start = unix_of(year, 1, 1) + yield from (start - 1, start, start + 1) + + def month_length(year, month): if month == 2 and calendar.isleap(year): return 29 @@ -392,6 +441,15 @@ def same_instant_pair(rng): ("compare c0af 30", "an overlong encoding in the first string to compare"), (" parse 30", "a leading space"), ("parse 30", "two spaces"), + ("fromunix", "no number"), + ("fromunix 1 2", "two numbers"), + ("fromunix 1_000", "an underscore"), + ("fromunix +1", "a plus sign"), + ("fromunix -", "a sign alone"), + ("fromunix --1", "two signs"), + ("fromunix 1.5", "a fraction"), + ("fromunix 0x10", "hex"), + ("fromunix \u0663", "a digit that is not ASCII"), ] # A last line with no LF must still be answered. @@ -415,6 +473,8 @@ def cases(seed, count): edges = list(edge_grid()) for a, b in zip(edges, edges[1:]): fixed.append(("compare", f"compare {hexed(a)} {hexed(b)}", order(a, b), False)) + for n in unix_grid(): + fixed.append(("fromunix", f"fromunix {n}", from_unix(n), False)) for req, _ in MALFORMED: fixed.append(("error", req, "error", False)) made = 0 @@ -423,6 +483,24 @@ def cases(seed, count): made += 1 while made < count: r = rng.random() + if r < 0.1: + r = rng.random() + if r < 0.3: + n = rng.randint(FIRST - 10 ** 7, LAST + 10 ** 7) + elif r < 0.4: + # Near an end of the range, on either side. + n = rng.choice([FIRST, LAST]) + rng.randint(-10 ** 5, 10 ** 5) + elif r < 0.7: + # The second before, at or after a midnight. + n = FIRST + rng.randint(-1, (LAST - FIRST) // 86400 + 1) * 86400 + rng.choice([-1, 0, 1]) + else: + # The seconds of a valid timestamp, which name its instant. + f = reference(random_valid(rng)) + n = f["unix"] if f else rng.randint(FIRST, LAST) + yield ("fromunix", f"fromunix {n}", from_unix(n), False) + made += 1 + continue + r = rng.random() if r < 0.35: s, label, mutated = random_valid(rng), "valid", False elif r < 0.5: @@ -634,6 +712,7 @@ def main(): accepted = sum(1 for w in parsed if w.startswith("OK")) leap = sum(1 for w in parsed if w.startswith("OK") and w.split("\t")[8] == "60") orders = [want for label, _, want, _ in items if label == "compare"] + from_unix_wants = [want for label, _, want, _ in items if label == "fromunix"] mutated = sum(1 for item in items if item[3]) malformed = [got for item, got in zip(items, out) if item[0] == "error"] @@ -654,6 +733,8 @@ def main(): f"offset and seconds: {checked}", f"- Pairs ordered: {len(orders)} ({orders.count('<')} before, {orders.count('=')} same " f"instant, {orders.count('>')} after, {orders.count('REJECT')} with a string rejected)", + f"- Unix seconds turned back into timestamps: {len(from_unix_wants)}, of which " + f"{from_unix_wants.count('NONE')} outside years 0000 to 9999", f"- Malformed requests answered `error`: {malformed.count('error')} of " f"{by_label.get('error', 0)}", f"- Requests ending in CR LF: every seventh, {len(items) // 7}", From c380cc19a642478f810901468c470c51139e596a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 04:09:32 +0000 Subject: [PATCH 2/2] Say what a round trip through Unix seconds does to a leap second From an independent pre-review: SPEC.md said that fromUnixSeconds t.unixSeconds puts any valid timestamp into UTC. A leap second's Unix seconds are those of the second after it, so it comes back as that second, a different instant, and 9999-12-31T23:59:60Z gives none. The sentence now holds for seconds up to 59 and names both cases; the README says the same where it discusses Unix seconds at a leap second. SPEC.md also said each second has exactly one UTC timestamp; outside the years 0000 to 9999 none has one, so it now says at most one, as the statements give. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 4 ++-- SPEC.md | 4 ++-- Spec.lean | 7 ++++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 21bca35..ae4646f 100644 --- a/README.md +++ b/README.md @@ -40,7 +40,7 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF | `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction, compared exactly. | `Spec.compareInstant_eq` | | The examples of section 5.8 parse to the fields the RFC gives. What the RFC says about them holds: `1996-12-19T16:39:57-08:00` is the instant `1996-12-20T00:39:57Z`, and `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. Separately, `1985-04-12T23:20:50.52Z` is 482196050 seconds after the epoch, as Python's `calendar.timegm` also gives. | `Spec.rfc3339_examples`, `Spec.rfc3339_example_instants` | | A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` | -| `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` | +| `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one, at most one, that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` | | `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Spec.fromUnixSeconds_isSome` | | `fromUnixSeconds` gives the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` | | The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` | @@ -51,7 +51,7 @@ The command-line tool in `Main.lean` calls these functions directly. - Reading requests and printing answers in `Main.lean`: the hex decoding and UTF-8 check in `serve` mode, the arguments, output and exit codes of `check` mode, and the decimal printing of numbers and reading of the numbers `fromunix` takes. The differential tests cover them, with malformed requests and CR LF line endings. - Whether a leap second was announced. Second 60 is accepted at 23:59 UTC at the end of any month, without a table of leap seconds, where section 5.7 allows it only at the end of months in which a leap second occurs. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. -- Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. +- Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. `fromUnixSeconds` turns that number into the second after the leap second, so a round trip through Unix seconds loses a leap second, and `9999-12-31T23:59:60Z` gives `none`. - Forms outside RFC 3339 are not supported, by design: - a space in place of `T`, which section 5.6 lets applications choose; - other ISO 8601 forms; diff --git a/SPEC.md b/SPEC.md index 1bbacf9..187bcff 100644 --- a/SPEC.md +++ b/SPEC.md @@ -46,9 +46,9 @@ POSIX time has no number for a leap second. As in POSIX time, second 60 is count ## From Unix seconds -`fromUnixSeconds` goes the other way: from whole seconds since 1970-01-01T00:00:00Z to the UTC timestamp for that second. Its result is valid, has offset `Z`, no fraction, and a second of at most 59, and names exactly the second it was given. Each second has exactly one such timestamp, and this is it. A leap second is never a result, since its number is the same as the next second's. +`fromUnixSeconds` goes the other way: from whole seconds since 1970-01-01T00:00:00Z to the UTC timestamp for that second. Its result is valid, has offset `Z`, no fraction, and a second of at most 59, and names exactly the second it was given. Each second has at most one such timestamp, and when it has one, this is it. A leap second is never a result, since its number is the same as the next second's. -It covers every second from `0000-01-01T00:00:00Z` (-62167219200) to `9999-12-31T23:59:59Z` (253402300799), the years RFC 3339 allows, and returns `none` outside them. So `fromUnixSeconds t.unixSeconds` puts any valid timestamp, whatever its offset, into UTC, dropping its fraction, unless that moves it outside those years. +Every second from `0000-01-01T00:00:00Z` (-62167219200) to `9999-12-31T23:59:59Z` (253402300799), the years RFC 3339 allows, has one, and `fromUnixSeconds` returns `none` outside them. So for a valid timestamp `t` whose second is at most 59, `fromUnixSeconds t.unixSeconds` is `t` put into UTC with its fraction dropped, or `none` when that moves it outside those years. A leap second comes back as the second after it, a different instant, so `1990-12-31T23:59:60Z` gives `1991-01-01T00:00:00Z`, and `9999-12-31T23:59:60Z`, at any offset, gives `none`. ## Errors diff --git a/Spec.lean b/Spec.lean index 2b77caa..974a98c 100644 --- a/Spec.lean +++ b/Spec.lean @@ -143,9 +143,10 @@ theorem Spec.syntax_vectors : /-! ## From Unix seconds -/ -/-- `fromUnixSeconds s` is the one timestamp that is valid, in UTC - (offset `Z`), with no fraction and no leap second, and that names - the second `s`. -/ +/-- `fromUnixSeconds s` gives exactly the timestamp that is valid, in + UTC (offset `Z`), with no fraction and no leap second, and that + names the second `s`. There is at most one; the next statement says + for which `s` there is one. -/ theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : Rfc3339.fromUnixSeconds s = some t ↔ Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧