diff --git a/Main.lean b/Main.lean index a376174..1b56fcd 100644 --- a/Main.lean +++ b/Main.lean @@ -22,6 +22,16 @@ seconds since the epoch, or NONE when it falls outside the years 0000 to 9999; N is decimal, with an optional leading `-` + known HEX prints OK, then tab-separated: SI seconds since + 1972-01-01T00:00:00Z (before 1972, Unix seconds + less 63072000) and TAI - UTC (`-` before + 1972, when TAI - UTC was not a whole number of + seconds); NOLEAP when the timestamp is valid but + its second 60 is not a leap second of the table; + or REJECT + fromsi N prints the printed form of the UTC timestamp N SI + seconds after 1972-01-01T00:00:00Z, with second 60 + at a leap second, or NONE outside 1972 to 9999 A malformed request prints `error`: an unknown operation, hex digits that are not in pairs, bytes that are not UTF-8, or a number that is @@ -30,7 +40,9 @@ Every answer comes from the proved functions in `Rfc3339/`: `parse`, `Timestamp.print`, `Timestamp.unixSeconds`, - `Timestamp.compareInstant` and `fromUnixSeconds`. The hex decoding and the request handling + `Timestamp.compareInstant`, `fromUnixSeconds`, + `Timestamp.isValidKnown`, `Timestamp.siSeconds`, + `Timestamp.taiMinusUtc` and `fromSiSeconds`. The hex decoding and the request handling here are covered by the tests, not by a proof. -/ @@ -93,6 +105,20 @@ def request (line : String) : Option String := pure <| match fromUnixSeconds s with | some t => t.print | none => "NONE" + | ["known", h] => do + let s ← fromHex h + pure <| match parse s with + | some t => + if t.isValidKnown then + let tai := if 63072000 ≤ t.unixSeconds then toString t.taiMinusUtc else "-" + s!"OK\t{t.siSeconds}\t{tai}" + else "NOLEAP" + | none => "REJECT" + | ["fromsi", n] => do + let s ← decimal n + pure <| match fromSiSeconds 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 fb97a93..80f7eb1 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -6,3 +6,4 @@ import Proofs.Main import Proofs.FromUnix.Main +import Proofs.Leap.Main diff --git a/Proofs/Leap/FromSi.lean b/Proofs/Leap/FromSi.lean new file mode 100644 index 0000000..6d33141 --- /dev/null +++ b/Proofs/Leap/FromSi.lean @@ -0,0 +1,401 @@ +/- + From SI seconds back to a timestamp. +-/ + +import Proofs.Leap.Si +import Proofs.Leap.Order +import Proofs.FromUnix.Main + +open Rfc3339 + +namespace Rfc3339.Proofs.Leap + +/-! ## Counting a prefix -/ + +/-- A predicate closed downward on `0, …, N - 1` holds exactly below + the number of indices it holds for. -/ +theorem fs_count_prefix (p : Nat → Bool) : ∀ N : Nat, + (∀ i j, i ≤ j → j < N → p j = true → p i = true) → + ((List.range N).filter p).length ≤ N ∧ + ∀ i, i < N → (p i = true ↔ i < ((List.range N).filter p).length) + | 0, _ => by simp + | N + 1, hm => by + have ih := fs_count_prefix p N (fun i j hij hj hp => hm i j hij (by omega) hp) + rw [List.range_succ, List.filter_append, List.length_append] + cases hpN : p N with + | true => + have hall : ∀ i, i < N + 1 → p i = true := fun i hi => hm i N (by omega) (by omega) hpN + have hk : ((List.range N).filter p).length = N := by + rcases Nat.eq_zero_or_pos N with h0 | hpos + · subst h0; simp + · have := (ih.2 (N - 1) (by omega)).mp (hall _ (by omega)); omega + simp only [List.filter_cons, hpN, List.filter_nil, ite_true, List.length_singleton, hk] + refine ⟨by omega, fun i hi => ?_⟩ + simp only [hall i hi, true_iff]; omega + | false => + simp only [List.filter_cons, hpN, List.filter_nil, Bool.false_eq_true, ite_false, + List.length_nil, Nat.add_zero] + refine ⟨by omega, fun i hi => ?_⟩ + rcases Nat.lt_or_ge i N with h | h + · exact ih.2 i h + · have : i = N := by omega + subst this + simp only [hpN, Bool.false_eq_true, false_iff] + omega + +/-- The number of indices below `N` that satisfy `p`, when `p` holds + exactly below `k`. -/ +theorem fs_count_lt (p : Nat → Bool) (N k : Nat) (hk : k ≤ N) + (h : ∀ i, i < N → (p i = true ↔ i < k)) : ((List.range N).filter p).length = k := by + have hc := fs_count_prefix p N (fun i j hij hj hp => (h i (by omega)).mpr + (by have := (h j hj).mp hp; omega)) + rcases Nat.lt_trichotomy ((List.range N).filter p).length k with c | c | c + · exfalso + have h1 := (h _ (by omega)).mpr c + have h2 := (hc.2 _ (by omega)).mp h1 + omega + · exact c + · exfalso + have h1 := (hc.2 k (by omega)).mpr c + have h2 := (h k (by omega)).mp h1 + omega + +/-! ## The list, by index -/ + +/-- The `i`-th month of the list. -/ +def fs_ym (i : Nat) : Nat × Nat := leapMonths.getD i (0, 0) + +/-- The Unix seconds of the instant just after the `i`-th leap second, + less those of 1972-01-01T00:00:00Z. -/ +def fs_V (i : Nat) : Int := (leapKey (fs_ym i) + 1) / 61 * 60 - 719528 * 86400 - 63072000 + +theorem fs_leapMonths_eq : leapMonths = (List.range 27).map fs_ym := by decide +kernel + +theorem fs_leapSiSeconds_eq : leapSiSeconds = (List.range 27).map (fun i => fs_V i + i) := by + decide +kernel + +theorem fs_V_mono_dec : ∀ j, j < 27 → ∀ i, i < j → fs_V i < fs_V j := by decide +kernel + +theorem fs_V_mono (i j : Nat) (hij : i ≤ j) (hj : j < 27) : fs_V i ≤ fs_V j := by + rcases Nat.lt_or_ge i j with h | h + · exact Int.le_of_lt (fs_V_mono_dec j hj i h) + · have : i = j := by omega + subst this; exact Int.le_refl _ + +theorem fs_key_mod : ∀ i, i < 27 → (leapKey (fs_ym i) + 1) % 87840 = 0 := by decide +kernel + +theorem fs_V_zero : fs_V 0 = 15724800 := by decide +kernel + +theorem fs_V_last : fs_V 26 = 1420156800 := by decide +kernel + +theorem fs_mem_leapSiSeconds (n : Int) : n ∈ leapSiSeconds ↔ ∃ i, i < 27 ∧ fs_V i + i = n := by + rw [fs_leapSiSeconds_eq, List.mem_map] + simp only [List.mem_range] + +/-- The count `fromSiSeconds` makes. -/ +theorem fs_k_eq (n : Int) : (leapSiSeconds.filter (· < n)).length = + ((List.range 27).filter (fun i => decide (fs_V i + i < n))).length := by + rw [fs_leapSiSeconds_eq, List.filter_map, List.length_map] + rfl + +theorem fs_k_char (n : Int) : + (leapSiSeconds.filter (· < n)).length ≤ 27 ∧ + ∀ i, i < 27 → (fs_V i + i < n ↔ i < (leapSiSeconds.filter (· < n)).length) := by + rw [fs_k_eq] + have hc := fs_count_prefix (fun i => decide (fs_V i + i < n)) 27 (by + intro i j hij hj hp + simp only [decide_eq_true_eq] at hp ⊢ + have := fs_V_mono i j hij hj + omega) + refine ⟨hc.1, fun i hi => ?_⟩ + have := hc.2 i hi + simp only [decide_eq_true_eq] at this + exact this + +/-- Off the leap seconds, the `i`-th leap second comes before `n - k` + Unix seconds after 1972 exactly when it is one of the `k` below `n`. -/ +theorem fs_V_le_iff (n : Int) (hn : n ∉ leapSiSeconds) (i : Nat) (hi : i < 27) : + fs_V i ≤ n - (leapSiSeconds.filter (· < n)).length ↔ + i < (leapSiSeconds.filter (· < n)).length := by + obtain ⟨hk, hc⟩ := fs_k_char n + have hne : ∀ j, j < 27 → fs_V j + j ≠ n := fun j hj e => + hn ((fs_mem_leapSiSeconds n).mpr ⟨j, hj, e⟩) + generalize (leapSiSeconds.filter (· < n)).length = k at hk hc ⊢ + constructor + · intro h + apply Nat.lt_of_not_le + intro hik + have hk27 : k < 27 := by omega + have h1 : ¬ fs_V k + k < n := fun c => by have := (hc k hk27).mp c; omega + have h2 := hne k hk27 + have h3 := fs_V_mono k i hik hi + omega + · intro h + have h1 := (hc (k - 1) (by omega)).mpr (by omega) + have h2 := fs_V_mono i (k - 1) (by omega) (by omega) + omega + +/-! ## Leap seconds before a second other than 60 -/ + +theorem fs_unix_utc (t : Timestamp) : + t.unixSeconds = (t.utcMinute - 719528 * 1440) * 60 + t.second := by + unfold Timestamp.unixSeconds Timestamp.utcMinute + omega + +theorem fs_lt_key_iff (t : Timestamp) (h59 : t.second ≤ 59) (i : Nat) (hi : i < 27) : + leapKey (fs_ym i) < t.utcMinute * 61 + t.second ↔ fs_V i + 63072000 ≤ t.unixSeconds := by + have := fs_key_mod i hi + rw [fs_unix_utc] + unfold fs_V + omega + +theorem fs_leapsBefore_of_le59 (t : Timestamp) (h59 : t.second ≤ 59) : + t.leapsBefore = + ((List.range 27).filter (fun i => decide (fs_V i + 63072000 ≤ t.unixSeconds))).length := by + unfold Timestamp.leapsBefore + rw [fs_leapMonths_eq, List.filter_map, List.length_map] + congr 1 + apply List.filter_congr + intro i hi + rw [List.mem_range] at hi + exact decide_eq_decide.mpr (fs_lt_key_iff t h59 i hi) + + +/-! ## The leap seconds themselves -/ + +/-- What `fromSiSeconds n` gives, checked: a UTC timestamp with no + fraction, known valid, from 1972 on, with SI seconds `n`. -/ +def fs_check (n : Int) : Bool := + match fromSiSeconds n with + | some t => decide (t.offset = .z) && decide (t.fraction = []) && t.isValidKnown && + decide (1972 ≤ t.year) && decide (t.siSeconds = n) + | none => false + +theorem fs_check_leap : ∀ n ∈ leapSiSeconds, fs_check n = true := by decide +kernel + +/-! ## Bounds -/ + +theorem fs_unix_1972 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by + decide +kernel + +theorem fs_dby_1972 : daysBeforeYear 1972 = 720258 := by decide + +theorem fs_si_max : Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253339228826 := by + decide +kernel + +/-- A valid UTC second other than 60, at or after 1972-01-01T00:00:00Z, + is in 1972 or later. -/ +theorem fs_year_of_unix (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) + (h59 : t.second ≤ 59) (hu : 63072000 ≤ Spec.unixSeconds t) : 1972 ≤ t.year := by + apply Nat.le_of_not_lt + intro hy + obtain ⟨_, hm1, hm2, hd1, hd2, hh, hmi, _⟩ := hv + have e := FromUnix.fu_unixSeconds_z t hz + have b := FromUnix.dy_dayNumber_bounds t.year t.month t.day ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ + have m := FromUnix.dy_mono (show t.year + 1 ≤ 1972 by omega) + rw [fs_dby_1972] at m + omega + +/-- A valid UTC timestamp in 1972 or later is at or after + 1972-01-01T00:00:00Z. -/ +theorem fs_unix_of_year (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) + (hy : 1972 ≤ t.year) : 63072000 ≤ Spec.unixSeconds t := by + obtain ⟨_, hm1, hm2, hd1, hd2, _⟩ := hv + have e := FromUnix.fu_unixSeconds_z t hz + have b := FromUnix.dy_dayNumber_bounds t.year t.month t.day ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ + have m := FromUnix.dy_mono hy + rw [fs_dby_1972] at m + omega + +theorem fs_si_nonneg (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) + (hy : 1972 ≤ t.year) : 0 ≤ Spec.siSeconds t := by + unfold Spec.siSeconds + rw [fs_unix_1972] + have := fs_unix_of_year t hv hz hy + omega + +theorem fs_Tmax_known : Spec.ValidKnown ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := + (isValidKnown_iff _).mp (by decide +kernel) + +theorem fs_Tmax_utcMinute : + Timestamp.utcMinute ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 5259491999 := by decide +kernel + +theorem fs_leapKey_lt_max : ∀ ym ∈ leapMonths, leapKey ym < 5259491999 * 61 + 59 := by + decide +kernel + +theorem fs_key_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = .z) : + t.utcMinute * 61 + t.second ≤ 5259491999 * 61 + 59 := by + obtain ⟨hy, hm1, hm2, hd1, hd2, hh, hmi, hs, _⟩ := hk.1 + by_cases h60 : t.second = 60 + · obtain ⟨ym, hym, e⟩ := leapKey_of_known t hk h60 + have := fs_leapKey_lt_max ym hym + omega + · have hN := FromUnix.dayNumber_lt t.year t.month t.day hy ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ + rw [FromUnix.fu_daysBeforeYear_10000, ← DayNumber.dayNumber_eq _ _ _ hm1 hm2] at hN + unfold Timestamp.utcMinute + rw [hz] + simp only [offsetMinutes] + omega + +/-- A known-valid UTC whole second is no later than + 9999-12-31T23:59:59Z, in SI seconds. -/ +theorem fs_si_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = .z) + (hf : t.fraction = []) : + Spec.siSeconds t ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by + have ho := siSeconds_order t _ hk fs_Tmax_known hf rfl + rw [siSeconds_eq t hk.1, siSeconds_eq _ fs_Tmax_known.1] at ho + have hkey : t.utcMinute * 61 + (t.second : Int) ≤ + Timestamp.utcMinute ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ * 61 + + ((Timestamp.second ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ : Nat) : Int) := by + rw [fs_Tmax_utcMinute] + exact fs_key_le_max t hk hz + apply Int.not_lt.mp + intro c + rw [Int.compare_eq_gt.mpr c] at ho + unfold Timestamp.compareInstant at ho + rcases Int.lt_or_eq_of_le hkey with h | h + · rw [Int.compare_eq_lt.mpr h] at ho + cases ho + · rw [Int.compare_eq_eq.mpr h, hf] at ho + simp [compareFraction] at ho + +/-! ## Uniqueness -/ + +theorem fs_eq_of_key (t t' : Timestamp) (hv : Spec.Valid t) (hv' : Spec.Valid t') + (hz : t.offset = .z) (hz' : t'.offset = .z) (hf : t.fraction = []) (hf' : t'.fraction = []) + (h : t.utcMinute * 61 + t.second = t'.utcMinute * 61 + t'.second) : t = t' := by + obtain ⟨y, m, d, hh, mi, s, fr, off⟩ := t + obtain ⟨y', m', d', hh', mi', s', fr', off'⟩ := t' + simp only at hz hz' hf hf' + subst hz hz' hf hf' + obtain ⟨_, hm1, hm2, hd1, hd2, hh23, hmi, hs, _⟩ := hv + obtain ⟨_, hm1', hm2', hd1', hd2', hh23', hmi', hs', _⟩ := hv' + simp only at hm1 hm2 hd1 hd2 hh23 hmi hs hm1' hm2' hd1' hd2' hh23' hmi' hs' + unfold Timestamp.utcMinute at h + simp only [offsetMinutes] at h + rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.dayNumber_eq _ _ _ hm1' hm2'] at h + have hdn : Spec.dayNumber y m d = Spec.dayNumber y' m' d' := by omega + obtain ⟨rfl, rfl, rfl⟩ := FromUnix.dayNumber_inj y m d y' m' d' ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ + ⟨hm1', hm2'⟩ ⟨hd1', hd2'⟩ hdn + have : hh = hh' ∧ mi = mi' ∧ s = s' := by omega + obtain ⟨rfl, rfl, rfl⟩ := this + rfl + +theorem fs_eq_of_si (t t' : Timestamp) (hk : Spec.ValidKnown t) (hk' : Spec.ValidKnown t') + (hz : t.offset = .z) (hz' : t'.offset = .z) (hf : t.fraction = []) (hf' : t'.fraction = []) + (h : Spec.siSeconds t = Spec.siSeconds t') : t = t' := by + have ho := siSeconds_order t t' hk hk' hf hf' + rw [siSeconds_eq t hk.1, siSeconds_eq t' hk'.1, h, Int.compare_eq_eq.mpr rfl] at ho + apply fs_eq_of_key t t' hk.1 hk'.1 hz hz' hf hf' + unfold Timestamp.compareInstant at ho + rw [hf, hf'] at ho + rcases Int.lt_trichotomy (t.utcMinute * 61 + t.second) (t'.utcMinute * 61 + t'.second) + with c | c | c + · rw [Int.compare_eq_lt.mpr c] at ho; cases ho + · exact c + · rw [Int.compare_eq_gt.mpr c] at ho; cases ho + +/-! ## The two directions -/ + +theorem fs_forward (n : Int) (t : Timestamp) (h : fromSiSeconds n = some t) : + t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Spec.siSeconds t = n := by + by_cases hl : n ∈ leapSiSeconds + · have hc := fs_check_leap n hl + unfold fs_check at hc + rw [h] at hc + simp only [Bool.and_eq_true, decide_eq_true_eq] at hc + obtain ⟨⟨⟨⟨hz, hf⟩, hk⟩, hy⟩, hs⟩ := hc + have hk' := (isValidKnown_iff t).mp hk + exact ⟨hz, hf, hk', hy, by rw [← siSeconds_eq t hk'.1]; exact hs⟩ + · have hcont : leapSiSeconds.contains n = false := by + cases e : leapSiSeconds.contains n + · rfl + · exact absurd (List.contains_iff_mem.mp e) hl + unfold fromSiSeconds at h + split at h + · contradiction + rename_i hn0 + simp only [hcont, Bool.false_eq_true, ite_false] at h + obtain ⟨hv, hz, hf, h59, hu⟩ := (Spec.fromUnixSeconds_iff _ _).mp h + have hU : t.unixSeconds = n + 63072000 - (leapSiSeconds.filter (· < n)).length := by + rw [Instant.unixSeconds_eq t hv]; exact hu + obtain ⟨hk27, hc⟩ := fs_k_char n + have hlb : t.leapsBefore = (leapSiSeconds.filter (· < n)).length := by + rw [fs_leapsBefore_of_le59 t h59] + apply fs_count_lt _ 27 _ hk27 + intro i hi + rw [decide_eq_true_iff, hU] + have := fs_V_le_iff n hl i hi + constructor + · intro a; exact this.mp (by omega) + · intro a; have := this.mpr a; omega + have hnk : ((leapSiSeconds.filter (· < n)).length : Int) ≤ n := by + have key : ∀ k : Nat, k ≤ 27 → (∀ i, i < 27 → (fs_V i + i < n ↔ i < k)) → + (k : Int) ≤ n := by + intro k hk hc + rcases Nat.eq_zero_or_pos k with e | e + · subst e; omega + · have h1 := (hc (k - 1) (by omega)).mpr (by omega) + have h2 := fs_V_mono 0 (k - 1) (Nat.zero_le _) (by omega) + rw [fs_V_zero] at h2 + omega + exact key _ hk27 hc + have hs : Spec.siSeconds t = n := by + rw [← siSeconds_eq t hv] + unfold Timestamp.siSeconds + rw [hU, hlb] + omega + refine ⟨hz, hf, ⟨hv, fun h60 => absurd h60 (by omega)⟩, + fs_year_of_unix t hv hz h59 (by omega), hs⟩ + +theorem fs_isSome_of_bounds (n : Int) (h0 : 0 ≤ n) (h1 : n ≤ 253339228826) : + (fromSiSeconds n).isSome := by + obtain ⟨hk27, hc⟩ := fs_k_char n + have h26 := hc 26 (by omega) + rw [fs_V_last] at h26 + have hb : n + 63072000 - (leapSiSeconds.filter (· < n)).length ≤ 253402300799 := by + by_cases c : (1420156800 : Int) + ((26 : Nat) : Int) < n + · have := h26.mp c; omega + · omega + unfold fromSiSeconds + split + · exact absurd ‹n < 0› (by omega) + dsimp only + split + · rw [Option.isSome_map] + apply (Spec.fromUnixSeconds_isSome _).mpr + rw [FromUnix.fu_unixSeconds_lo, FromUnix.fu_unixSeconds_hi] + omega + · apply (Spec.fromUnixSeconds_isSome _).mpr + rw [FromUnix.fu_unixSeconds_lo, FromUnix.fu_unixSeconds_hi] + omega + +theorem fromSiSeconds_iff (n : Int) (t : Timestamp) : + fromSiSeconds n = some t ↔ + t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Spec.siSeconds t = n := by + constructor + · exact fs_forward n t + · rintro ⟨hz, hf, hk, hy, hs⟩ + have h0 : 0 ≤ n := hs ▸ fs_si_nonneg t hk.1 hz hy + have h1 : n ≤ 253339228826 := by rw [← hs, ← fs_si_max]; exact fs_si_le_max t hk hz hf + obtain ⟨t', ht'⟩ := Option.isSome_iff_exists.mp (fs_isSome_of_bounds n h0 h1) + obtain ⟨hz', hf', hk', -, hs'⟩ := fs_forward n t' ht' + rw [ht'] + congr 1 + exact (fs_eq_of_si t t' hk hk' hz hz' hf hf' (by rw [hs, hs'])).symm + +theorem fromSiSeconds_isSome (n : Int) : + (fromSiSeconds n).isSome ↔ + 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by + constructor + · intro h + obtain ⟨t, ht⟩ := Option.isSome_iff_exists.mp h + obtain ⟨hz, hf, hk, hy, hs⟩ := fs_forward n t ht + exact ⟨hs ▸ fs_si_nonneg t hk.1 hz hy, hs ▸ fs_si_le_max t hk hz hf⟩ + · rintro ⟨h0, h1⟩ + rw [fs_si_max] at h1 + exact fs_isSome_of_bounds n h0 h1 + +end Rfc3339.Proofs.Leap diff --git a/Proofs/Leap/Main.lean b/Proofs/Leap/Main.lean new file mode 100644 index 0000000..c9540f6 --- /dev/null +++ b/Proofs/Leap/Main.lean @@ -0,0 +1,76 @@ +/- + The leap second statements of `Spec.lean`, under the same names, from + the lemmas in the other files of `Proofs/Leap/`. The test vectors are + checked by evaluation. +-/ + +import Proofs.Leap.Table +import Proofs.Leap.Si +import Proofs.Leap.Order +import Proofs.Leap.FromSi + +open Rfc3339 + +theorem Spec.isValidKnown_iff (t : Timestamp) : + t.isValidKnown = true ↔ Spec.ValidKnown t := + Rfc3339.Proofs.Leap.isValidKnown_iff t + +theorem Spec.siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : + t.siSeconds = Spec.siSeconds t := + Rfc3339.Proofs.Leap.siSeconds_eq t h + +theorem Spec.siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) + (fa : a.fraction = []) (fb : b.fraction = []) : + compare a.siSeconds b.siSeconds = a.compareInstant b := + Rfc3339.Proofs.Leap.siSeconds_order a b ha hb fa fb + +theorem Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : + fromSiSeconds n = some t ↔ + t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Spec.siSeconds t = n := + Rfc3339.Proofs.Leap.fromSiSeconds_iff n t + +theorem Spec.fromSiSeconds_isSome (n : Int) : + (fromSiSeconds n).isSome ↔ + 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := + Rfc3339.Proofs.Leap.fromSiSeconds_isSome n + +theorem Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Spec.Valid t) : + t.taiMinusUtc = 10 + Spec.leapsBefore t := by + unfold Timestamp.taiMinusUtc + rw [Rfc3339.Proofs.Leap.leapsBefore_eq t h] + +theorem Spec.taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : + t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := + Rfc3339.Proofs.Leap.taiMinusUtc_eq t h h60 h72 + +theorem Spec.leap_table_vectors : + Timestamp.isValidKnown ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = true ∧ + Timestamp.isValidKnown ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨2017, 1, 1, 0, 59, 60, [], .plus 1 0⟩ = true ∧ + Timestamp.isValidKnown ⟨2015, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.isValidKnown ⟨1971, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.isValidKnown ⟨2026, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.siSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 0 ∧ + Timestamp.siSeconds ⟨1972, 6, 30, 23, 59, 59, [], .z⟩ = 15724799 ∧ + Timestamp.siSeconds ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = 15724800 ∧ + Timestamp.siSeconds ⟨1972, 7, 1, 0, 0, 0, [], .z⟩ = 15724801 ∧ + Timestamp.siSeconds ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ = 1420156827 ∧ + Timestamp.siSeconds ⟨2016, 12, 31, 23, 59, 59, [], .z⟩ = 1420156825 ∧ + Timestamp.siSeconds ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = 1420156826 ∧ + Timestamp.taiMinusUtc ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 6, 30, 23, 59, 59, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 7, 1, 0, 0, 0, [], .z⟩ = 11 ∧ + Timestamp.taiMinusUtc ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = 36 ∧ + Timestamp.taiMinusUtc ⟨2016, 12, 31, 23, 59, 59, [], .z⟩ = 36 ∧ + Timestamp.taiMinusUtc ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ = 37 ∧ + fromSiSeconds 15724800 = some ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ ∧ + fromSiSeconds 1420156826 = some ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ ∧ + fromSiSeconds 1420156827 = some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ ∧ + fromUnixSeconds (Timestamp.unixSeconds ⟨2016, 12, 31, 23, 59, 60, [], .z⟩) = + some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ := by + and_intros <;> decide +kernel diff --git a/Proofs/Leap/Order.lean b/Proofs/Leap/Order.lean new file mode 100644 index 0000000..9d1d136 --- /dev/null +++ b/Proofs/Leap/Order.lean @@ -0,0 +1,98 @@ +/- + SI seconds order known-valid whole seconds as their instants. +-/ + +import Proofs.Leap.Table + +open Rfc3339 + +namespace Rfc3339.Proofs.Leap + +/-- Counting the entries below a threshold is monotone in the threshold. -/ +private theorem or_filter_mono {α : Type} (l : List α) (f : α → Int) (x y : Int) (h : x ≤ y) : + (l.filter fun a => decide (f a < x)).length ≤ + (l.filter fun a => decide (f a < y)).length := by + induction l with + | nil => simp + | cons a l ih => + simp only [List.filter_cons] + by_cases h1 : f a < x + · have h2 : f a < y := by omega + simp [h1, h2] <;> omega + · by_cases h2 : f a < y + · simp [h1, h2] <;> omega + · simp [h1, h2] <;> omega + +/-- And strictly so when an entry lies between the two thresholds. -/ +private theorem or_filter_strict {α : Type} (l : List α) (f : α → Int) (x y : Int) (h : x ≤ y) + (z : α) (hz : z ∈ l) (hz1 : x ≤ f z) (hz2 : f z < y) : + (l.filter fun a => decide (f a < x)).length + 1 ≤ + (l.filter fun a => decide (f a < y)).length := by + induction l with + | nil => simp at hz + | cons a l ih => + have hm := or_filter_mono l f x y h + simp only [List.filter_cons] + rcases List.mem_cons.mp hz with he | hz' + · rw [he] at hz1 hz2 + have h1 : ¬ f a < x := by omega + simp [h1, hz2] <;> omega + · have ih' := ih hz' + by_cases h1 : f a < x + · have h2 : f a < y := by omega + simp [h1, h2] <;> omega + · by_cases h2 : f a < y + · simp [h1, h2] <;> omega + · simp [h1, h2] <;> omega + +private theorem or_unix (t : Timestamp) : + t.unixSeconds = (t.utcMinute - 719528 * 1440) * 60 + t.second := by + unfold Timestamp.unixSeconds Timestamp.utcMinute + omega + +private theorem or_si (t : Timestamp) : + t.siSeconds = (t.utcMinute - 719528 * 1440) * 60 + t.second - 63072000 + t.leapsBefore := by + unfold Timestamp.siSeconds + rw [or_unix] + +private theorem or_lt (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) + (h : a.utcMinute * 61 + a.second < b.utcMinute * 61 + b.second) : + a.siSeconds < b.siSeconds := by + obtain ⟨_, _, _, _, _, _, _, hsa, _⟩ := ha.1 + obtain ⟨_, _, _, _, _, _, _, hsb, _⟩ := hb.1 + have hm : a.leapsBefore ≤ b.leapsBefore := by + unfold Timestamp.leapsBefore + exact or_filter_mono leapMonths leapKey _ _ (by omega) + rw [or_si, or_si] + by_cases h60 : a.second = 60 + · obtain ⟨ym, hym, hk⟩ := leapKey_of_known a ha h60 + have hs : a.leapsBefore + 1 ≤ b.leapsBefore := by + unfold Timestamp.leapsBefore + exact or_filter_strict leapMonths leapKey _ _ (by omega) ym hym (by omega) (by omega) + omega + · omega + +private theorem or_eq (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) + (h : a.utcMinute * 61 + a.second = b.utcMinute * 61 + b.second) : + a.siSeconds = b.siSeconds := by + obtain ⟨_, _, _, _, _, _, _, hsa, _⟩ := ha.1 + obtain ⟨_, _, _, _, _, _, _, hsb, _⟩ := hb.1 + have hL : a.leapsBefore = b.leapsBefore := by + unfold Timestamp.leapsBefore + rw [h] + rw [or_si, or_si, hL] + omega + +theorem siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) + (fa : a.fraction = []) (fb : b.fraction = []) : + compare a.siSeconds b.siSeconds = a.compareInstant b := by + unfold Timestamp.compareInstant + rw [fa, fb] + rcases Int.lt_trichotomy (a.utcMinute * 61 + a.second) (b.utcMinute * 61 + b.second) + with h | h | h + · rw [Int.compare_eq_lt.mpr h, Int.compare_eq_lt.mpr (or_lt a b ha hb h)] + · rw [Int.compare_eq_eq.mpr h, Int.compare_eq_eq.mpr (or_eq a b ha hb h)] + simp [compareFraction] + · rw [Int.compare_eq_gt.mpr h, Int.compare_eq_gt.mpr (or_lt b a hb ha h)] + +end Rfc3339.Proofs.Leap diff --git a/Proofs/Leap/Si.lean b/Proofs/Leap/Si.lean new file mode 100644 index 0000000..a298d9a --- /dev/null +++ b/Proofs/Leap/Si.lean @@ -0,0 +1,115 @@ +/- + SI seconds and TAI − UTC against the spec. +-/ + +import Proofs.Leap.Table + +open Rfc3339 + +namespace Rfc3339.Proofs.Leap + +/-- Filtering a mapped list counts what filtering by the composite + predicate counts. -/ +theorem si_length_filter_map {α β : Type} (l : List α) (f : α → β) (p : β → Bool) : + ((l.map f).filter p).length = (l.filter fun a => p (f a)).length := by + rw [List.filter_map, List.length_map] + rfl + +theorem leapsBefore_eq (t : Timestamp) (h : Spec.Valid t) : + t.leapsBefore = Spec.leapsBefore t := by + unfold Timestamp.leapsBefore Spec.leapsBefore + rw [Instant.utcMinute_eq t h] + have h1 := si_length_filter_map leapMonths leapKey + (fun k => decide (k < Spec.utcMinute t * 61 + (t.second : Int))) + have h2 := si_length_filter_map Spec.leapTable.tail (fun e => Spec.leapSecondKey e.1) + (fun k => decide (k < Spec.utcMinute t * 61 + (t.second : Int))) + rw [leapKey_table] at h1 + rw [← h1, h2] + rfl + +theorem si_unix1972 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by + decide +kernel + +theorem siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : t.siSeconds = Spec.siSeconds t := by + unfold Timestamp.siSeconds Spec.siSeconds + rw [Instant.unixSeconds_eq t h, si_unix1972, leapsBefore_eq t h] + +/-- The shape of the table after its first line: NTP times strictly + increasing from `n`, offsets one more each line from `c`. -/ +def si_shape : Nat → Nat → List (Nat × Nat) → Bool + | _, _, [] => true + | n, c, (n', c') :: rest => decide (n < n') && c' == c + 1 && si_shape n' c' rest + +theorem si_shape_lower (l : List (Nat × Nat)) : + ∀ n c, si_shape n c l = true → ∀ e ∈ l, n < e.1 := by + induction l with + | nil => intro n c _ e he; cases he + | cons hd rest ih => + intro n c hs e he + obtain ⟨n', c'⟩ := hd + simp only [si_shape, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] at hs + obtain ⟨⟨hn, _⟩, hr⟩ := hs + rcases List.mem_cons.mp he with he | he + · subst he; exact hn + · have := ih n' c' hr e he + omega + +theorem si_lastLine (l : List (Nat × Nat)) : + ∀ (n c : Nat) (x : Int), si_shape n c l = true → (n : Int) ≤ x → + ((((n, c) :: l).filter fun e => decide ((e.1 : Int) ≤ x)).getLast?.map (·.2)).getD 0 = + c + (l.filter fun e => decide ((e.1 : Int) ≤ x)).length := by + induction l with + | nil => + intro n c x _ hx + simp [hx] + | cons hd rest ih => + intro n c x hs hx + obtain ⟨n', c'⟩ := hd + have hs' := hs + simp only [si_shape, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] at hs' + obtain ⟨⟨hn, hc⟩, hr⟩ := hs' + by_cases hx' : (n' : Int) ≤ x + · have ih' := ih n' c' x hr hx' + simp only [List.filter_cons, hx, hx', decide_true, ite_true] at ih' ⊢ + rw [List.getLast?_cons_cons, ih', List.length_cons] + omega + · have hnil : (rest.filter fun e => decide ((e.1 : Int) ≤ x)) = [] := by + rw [List.filter_eq_nil_iff] + intro e he + have := si_shape_lower rest n' c' hr e he + simp only [decide_eq_true_eq] + omega + simp [hx, hx', hnil] + +theorem si_table_shape : si_shape 2272060800 10 Spec.leapTable.tail = true := by + decide +kernel + +theorem si_table_mod : ∀ e ∈ Spec.leapTable.tail, e.1 % 60 = 0 := by + decide +kernel + +theorem si_taiMinusUtcAt (x : Int) (hx : 2272060800 ≤ x) : + Spec.taiMinusUtcAt x = 10 + (Spec.leapTable.tail.filter fun e => decide ((e.1 : Int) ≤ x)).length := by + unfold Spec.taiMinusUtcAt + have hl : Spec.leapTable = (2272060800, 10) :: Spec.leapTable.tail := rfl + rw [hl] + exact si_lastLine Spec.leapTable.tail 2272060800 10 x si_table_shape (by omega) + +theorem taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : + t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := by + have hs : t.second ≤ 60 := h.2.2.2.2.2.2.2.1 + rw [si_unix1972] at h72 + unfold Timestamp.taiMinusUtc + rw [leapsBefore_eq t h, si_taiMinusUtcAt _ (by unfold Spec.ntpOfUnix; omega)] + congr 1 + unfold Spec.leapsBefore + congr 1 + apply List.filter_congr + intro e he + have hm := si_table_mod e he + unfold Spec.leapSecondKey Spec.secondKey Spec.ntpOfUnix Spec.unixSeconds + rw [Instant.dayNumber_epoch] + simp only [decide_eq_decide] + omega + +end Rfc3339.Proofs.Leap diff --git a/Proofs/Leap/Table.lean b/Proofs/Leap/Table.lean new file mode 100644 index 0000000..22a091a --- /dev/null +++ b/Proofs/Leap/Table.lean @@ -0,0 +1,157 @@ +/- + The leap second table: the code's (year, month) list against the + spec's NTP times, and `isValidKnown` against `Spec.ValidKnown`. +-/ + +import Rfc3339 +import Spec.Leap +import Proofs.Valid +import Proofs.Instant +import Proofs.FromUnix.Day + +open Rfc3339 + +namespace Rfc3339.Proofs.Leap + +/-- The leap seconds of the code's list, in order, are those of the + table's lines after the first. -/ +theorem leapKey_table : + leapMonths.map leapKey = Spec.leapTable.tail.map (fun e => Spec.leapSecondKey e.1) := by + decide +kernel + +/-- The day number of the first day of the month after `ym`, as + `leapKey` computes it. -/ +def tb_next (ym : Nat × Nat) : Nat := + if ym.2 = 12 then dayNumber (ym.1 + 1) 1 1 else dayNumber ym.1 (ym.2 + 1) 1 + +theorem tb_leapKey_eq (ym : Nat × Nat) : + leapKey ym = (((tb_next ym * 1440 : Nat) : Int) - 1) * 61 + 60 := rfl + +/-- Each NTP time of the table after the first line is a whole number + of minutes after the Unix epoch. -/ +theorem tb_table_div : ∀ e ∈ Spec.leapTable.tail, ((e.1 : Int) - Spec.ntpOfUnix 0) % 60 = 0 := by + decide +kernel + +/-- Facts about each month of the code's list: its range, and that the + day before the next month starts falls in it. -/ +theorem tb_months : ∀ ym ∈ leapMonths, 1972 ≤ ym.1 ∧ ym.1 ≤ 2016 ∧ 1 ≤ ym.2 ∧ ym.2 ≤ 12 ∧ + 1 ≤ tb_next ym ∧ + (fromDayNumber (tb_next ym - 1)).1 = ym.1 ∧ (fromDayNumber (tb_next ym - 1)).2.1 = ym.2 := by + decide +kernel + +/-- The month after `(y, m)` starts `daysInMonth y m` days after it. -/ +theorem tb_next_eq (y m : Nat) (hm1 : 1 ≤ m) (hm2 : m ≤ 12) : + tb_next (y, m) = Spec.dayNumber y m 1 + Spec.daysInMonth y m := by + unfold tb_next + simp only + split + · rename_i h12 + subst h12 + rw [DayNumber.dayNumber_eq _ _ _ (by decide) (by decide), ← Valid.next_year y] + simp [Spec.daysInMonth] + · rw [DayNumber.dayNumber_eq _ _ _ (by omega) (by omega), Valid.next_month y m hm1] + +theorem tb_utcMonth_eq (t : Timestamp) : + t.utcMonth = ((fromDayNumber (t.utcMinute / 1440).toNat).1, + (fromDayNumber (t.utcMinute / 1440).toNat).2.1) := rfl + +/-- At second 60, a leap second of the code's list is one of the table's. -/ +theorem tb_key_iff_table (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) : + (∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second) ↔ Spec.TableLeapSecond t := by + have e1 : (∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second) ↔ + ∃ e ∈ Spec.leapTable.tail, Spec.leapSecondKey e.1 = t.utcMinute * 61 + t.second := by + have := congrArg (fun l => t.utcMinute * 61 + t.second ∈ l) leapKey_table + simp only [List.mem_map] at this + exact Iff.of_eq this + rw [e1, Instant.utcMinute_eq t h] + unfold Spec.TableLeapSecond + simp only [h60, true_and] + constructor + · rintro ⟨e, he, hk⟩ + refine ⟨e, he, ?_⟩ + have hd := tb_table_div e he + unfold Spec.leapSecondKey at hk + unfold Spec.unixSeconds + rw [Instant.dayNumber_epoch] at hk ⊢ + simp only [Spec.ntpOfUnix] at hk hd ⊢ + omega + · rintro ⟨e, he, hk⟩ + refine ⟨e, he, ?_⟩ + unfold Spec.leapSecondKey + unfold Spec.unixSeconds at hk + rw [Instant.dayNumber_epoch] at hk ⊢ + simp only [Spec.ntpOfUnix] at hk ⊢ + omega + +/-- At a valid second 60, the code's month test is the leap second key test. -/ +theorem tb_contains_iff (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) : + leapMonths.contains t.utcMonth = true ↔ + ∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second := by + obtain ⟨y, m, hm1, hm2, hD⟩ := h.2.2.2.2.2.2.2.2.1 h60 + rw [← Instant.utcMinute_eq t h] at hD + have hkey : ∀ ym, leapKey ym = t.utcMinute * 61 + t.second ↔ + tb_next ym = Spec.dayNumber y m 1 := by + intro ym + rw [tb_leapKey_eq, h60] + omega + simp only [hkey, List.contains_iff_mem] + rw [tb_utcMonth_eq] + constructor + · intro hmem + have hp := tb_months _ hmem + generalize hn : (t.utcMinute / 1440).toNat = n at hmem hp + have hy := FromUnix.yearOfDay_spec n + have hy1 : (fromDayNumber n).1 = yearOfDay n := rfl + obtain ⟨hp1, hp2, -, -, -, -, -⟩ := hp + simp only at hp1 hp2 + rw [hy1] at hp1 hp2 + have h10 : n < daysBeforeYear 10000 := by + have := FromUnix.dy_mono (show yearOfDay n + 1 ≤ 10000 by omega) + omega + have h72 : daysBeforeYear 1972 ≤ n := by + have := FromUnix.dy_mono hp1 + omega + have h72' : 0 < daysBeforeYear 1972 := by decide + have hnD : n + 1 = Spec.dayNumber y m 1 := by omega + obtain ⟨-, hm1', hm2', hd1', hd2', hdn⟩ := FromUnix.fromDayNumber_spec n h10 + refine ⟨_, hmem, ?_⟩ + rw [tb_next_eq _ _ hm1' hm2'] + have hday := Valid.dayNumber_day (fromDayNumber n).1 (fromDayNumber n).2.1 + (fromDayNumber n).2.2 + have hsp := Valid.month_start_spaced hm1' hm2' hm1 hm2 (show + Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 1 < Spec.dayNumber y m 1 by omega) + omega + · rintro ⟨ym, hmem, hk⟩ + obtain ⟨-, -, -, -, hn1, hy, hm⟩ := tb_months ym hmem + have hn : (t.utcMinute / 1440).toNat = tb_next ym - 1 := by omega + rw [hn, hy, hm] + exact hmem + +theorem isValidKnown_iff (t : Timestamp) : t.isValidKnown = true ↔ Spec.ValidKnown t := by + unfold Timestamp.isValidKnown Spec.ValidKnown + simp only [Bool.and_eq_true, Bool.or_eq_true, bne_iff_ne, ne_eq, Valid.isValid_iff] + constructor + · rintro ⟨hv, hl⟩ + refine ⟨hv, fun h60 => ?_⟩ + rcases hl with hl | hl + · exact absurd h60 hl + · exact (tb_key_iff_table t hv h60).1 ((tb_contains_iff t hv h60).1 hl) + · rintro ⟨hv, hl⟩ + refine ⟨hv, ?_⟩ + by_cases h60 : t.second = 60 + · exact Or.inr ((tb_contains_iff t hv h60).2 ((tb_key_iff_table t hv h60).2 (hl h60))) + · exact Or.inl h60 + +/-- A known-valid second 60 sits at one of the list's leap seconds. -/ +theorem leapKey_of_known (t : Timestamp) (h : Spec.ValidKnown t) (h60 : t.second = 60) : + ∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second := + (tb_key_iff_table t h.1 h60).2 (h.2 h60) + +/-- And a valid second 60 at one of the list's leap seconds is known + valid. -/ +theorem known_of_leapKey (t : Timestamp) (h : Spec.Valid t) (ym : Nat × Nat) + (hym : ym ∈ leapMonths) (hk : leapKey ym = t.utcMinute * 61 + t.second) : + Spec.ValidKnown t := + ⟨h, fun h60 => (tb_key_iff_table t h h60).1 ⟨ym, hym, hk⟩⟩ + +end Rfc3339.Proofs.Leap diff --git a/README.md b/README.md index ae4646f..484b59a 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # rfc: RFC 3339 timestamps, proved -This library reads, checks and writes RFC 3339 timestamps, such as `1985-04-12T23:20:50.52Z`, in Lean. Machine-checked proofs show that it accepts exactly the strings that the RFC's grammar and calendar rules allow, including the day ranges and leap years of the calendar. There is one relaxation: it accepts a leap second at the end of any month, because it keeps no table of the months that had one. The proofs also cover the round trip from text to value and back, the count of seconds since the Unix epoch, and the order of two timestamps by the instant they name. The library is tested against Python's date and time code; `tests/TEST-RESULTS.md` has the record. +This library reads, checks and writes RFC 3339 timestamps, such as `1985-04-12T23:20:50.52Z`, in Lean. Machine-checked proofs show that it accepts exactly the strings that the RFC's grammar and calendar rules allow, including the day ranges and leap years of the calendar. `isValid` has one relaxation: it accepts a leap second at the end of any month. `isValidKnown` is exact: it checks second 60 against the table of the 27 leap seconds there have been, as tzdata publishes it. The proofs also cover the round trip from text to value and back, the count of seconds since the Unix epoch, and the order of two timestamps by the instant they name. A count of SI seconds since 1972 gives each leap second its own number, so a round trip through it keeps a leap second, as one through Unix seconds cannot. TAI − UTC is also given, as 10 plus the leap seconds before the timestamp, and proved to agree with the table's own TAI − UTC column at every second from 1972 on but a leap second. The library is tested against Python's date and time code; `tests/TEST-RESULTS.md` has the record. It is a project of [Proven Commons](https://github.com/Proven-Commons/mission), built to the verified bar published there. @@ -21,16 +21,20 @@ For each timestamp it prints the timestamp as written, with `T` and `Z` in upper - `Timestamp.unixSeconds` - `Timestamp.compareInstant` - `Rfc3339.fromUnixSeconds` +- `Timestamp.isValidKnown` +- `Timestamp.siSeconds` +- `Timestamp.taiMinusUtc` +- `Rfc3339.fromSiSeconds` `SPEC.md` says what each one does. ## What is proved -The statements are in `Spec.lean`. The definitions they use, written from the RFC, are in `Spec/Defs.lean`, and the types are in `Rfc3339/Types.lean`. The proofs are in `Proofs/`. +The statements are in `Spec.lean`. The definitions they use, written from the RFC, are in `Spec/Defs.lean`; those for the leap second table, with the table itself, are in `Spec/Leap.lean`; and the types are in `Rfc3339/Types.lean`. The proofs are in `Proofs/`. | Claim | Theorem | |-------|---------| -| `isValid` decides the rules of RFC 3339, sections 5.6 and 5.7. Every field is in its range. The day exists in its month, with the leap years of Appendix C. Second 60 falls only at 23:59 UTC on the last day of a month. Section 5.7 allows it only in months that had a leap second; with no table of them, any month is accepted. | `Spec.isValid_iff` | +| `isValid` decides the rules of RFC 3339, sections 5.6 and 5.7. Every field is in its range. The day exists in its month, with the leap years of Appendix C. Second 60 falls only at 23:59 UTC on the last day of a month. Section 5.7 allows it only in months that had a leap second; `isValid` uses no table of them, so any month is accepted. | `Spec.isValid_iff` | | A valid timestamp prints as the grammar of section 5.6 writes it, with `T` and `Z` in upper case. | `Spec.print_eq` | | `parse` returns a timestamp exactly when the timestamp is valid and the string is how it prints, with `T` and `Z` in either case. So `parse` accepts nothing outside the grammar and those rules, rejects nothing inside them, and returns the fields as written. | `Spec.parse_iff` | | What `parse` returns is valid; for example, 30 February never passes. | `Spec.parse_valid` | @@ -44,13 +48,23 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF | `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` | +| `isValidKnown` decides section 5.7 with the table of leap seconds. It allows second 60 only at one of the table's leap seconds, at the same instant whatever the offset. The table is the one in `Spec/Leap.lean`. The code keeps its own list of months, and the proof shows the two agree. | `Spec.isValidKnown_iff` | +| `siSeconds` is the Unix seconds since 1972-01-01T00:00:00Z, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds; so a leap second, the second before it and the second after it get three numbers in a row. Before 1972 the number is Unix seconds, 86400 to a day. | `Spec.siSeconds_eq` | +| On whole seconds valid by the table, `siSeconds` orders timestamps exactly as `compareInstant` does. So no two instants share a number, a leap second and the second after it included. | `Spec.siSeconds_order` | +| `fromSiSeconds` turns SI seconds back into the one UTC timestamp from 1972 on, valid by the table, that has them, a leap second included. It gives a timestamp for every second from 1972-01-01T00:00:00Z to 9999-12-31T23:59:59Z and `none` outside. | `Spec.fromSiSeconds_iff`, `Spec.fromSiSeconds_isSome` | +| `taiMinusUtc` is 10, and one more for each leap second of the table before the timestamp, so during a leap second it is still the value from before it. | `Spec.taiMinusUtc_leapsBefore` | +| TAI − UTC at each second from 1972 on, other than a leap second, is the value in the table's second column, 10 to 37. The code never reads that column; it counts leap seconds. | `Spec.taiMinusUtc_eq` | +| Section 5.8's leap seconds, the table's first and last, one seen from another offset, and second 60 in months that had none. SI seconds and TAI − UTC around the first and the last leap second. And the round trip that Unix seconds lose and SI seconds keep. | `Spec.leap_table_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 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. +- 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, the decimal printing of numbers and reading of the numbers `fromunix` and `fromsi` take, and the layout of the `known` answer, with `-` for TAI − UTC before 1972. The differential tests cover them, with malformed requests and CR LF line endings. +- Whether a leap second was announced, in `isValid` and `parse`. They accept second 60 at 23:59 UTC at the end of any month, where section 5.7 allows it only at the end of months in which a leap second occurs; `isValidKnown` checks that against the table. 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. +- The table after its expiry date, 28 June 2027. `isValidKnown` refuses second 60 at any month end the table does not list, and `siSeconds` and `taiMinusUtc` count no leap second after 2016. If one is ever announced, the table in the spec and the code's list must change together, and the spec approved again. The table is what tzdata publishes from IERS Bulletin C; that it matches the IERS record is trusted, not proved. +- SI seconds and TAI − UTC before 1972. UTC then ran on seconds of varying length, with TAI − UTC not a whole number of seconds. Before 1972, `Spec.siSeconds_eq` makes `siSeconds` Unix seconds less 63072000, 86400 to a day, which are not SI seconds there, and `taiMinusUtc` gives 10, which means nothing there; the tool's `known` request prints `-` for TAI − UTC. +- The table itself. `Spec/Leap.lean` copies tzdata's `leap-seconds.list` (tzdata 2026e, updated through IERS Bulletin C, expiring 28 June 2027) line for line. That copy is part of the specification: the reviewer checks it against the file, and the differential tests check the code against the copy of the file on the test machine, but no proof does. - 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; @@ -67,7 +81,7 @@ The command-line tool in `Main.lean` calls these functions directly. - The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. - Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as the arithmetic on natural numbers and integers and the conversion between strings and lists of characters. - The operating system and hardware it runs on. -- Python's `datetime` and `calendar` modules, as an oracle in the differential tests. The record names the Python version. +- Python's `datetime` and `calendar` modules, and for leap seconds the copy of tzdata's `leap-seconds.list` on the test machine, as oracles in the differential tests. The record names the Python version and the file. This project has no dependencies beyond Lean itself. @@ -82,9 +96,11 @@ This project has no dependencies beyond Lean itself. - Go accepts a comma before the fraction. - `rfc3339-validator` accepts a timestamp followed by a line break. +For leap seconds, it compares `siSeconds`, `taiMinusUtc` and `fromSiSeconds` with ERFA, a BSD-licensed C library derived from the IAU's SOFA, through pyerfa, which keeps its own leap second table. `tests/CROSS-CHECK.md` gives the counts. + ## Re-check it -Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), and Python 3.11 or later. +Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), Python 3.11 or later, and tzdata, for `/usr/share/zoneinfo/leap-seconds.list`. ``` lake build @@ -94,14 +110,15 @@ python3 tests/run_tests.py `lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. -The test script compares the tool with Python's `datetime` and `calendar` modules, and with the RFC's rules copied into the script, on inputs from a recorded seed. It then rewrites `tests/TEST-RESULTS.md`. +The test script compares the tool with Python's `datetime` and `calendar` modules, with the RFC's rules copied into the script, and with tzdata's `leap-seconds.list`, which the script reads itself, on inputs from a recorded seed. It then rewrites `tests/TEST-RESULTS.md`. ## Layout - `Rfc3339/Types.lean`: the timestamp and offset types. It is part of the specification. -- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`, `Rfc3339/FromUnix.lean`: the code under proof. +- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`, `Rfc3339/FromUnix.lean`, `Rfc3339/Leap.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. +- `Spec/Leap.lean`: the leap second table, line for line from tzdata's `leap-seconds.list`, and the definitions the leap second statements use. - `Proofs.lean` and `Proofs/`: the proofs, under the same names. - `Main.lean`: the command-line tool. - `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else. @@ -109,4 +126,4 @@ The test script compares the tool with Python's `datetime` and `calendar` module - `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. -- `tests/cross_check.py` and `tests/cross_check/main.go`: the one-off comparison with other parsers. +- `tests/cross_check.py` and `tests/cross_check/main.go`: the one-off comparison with other parsers, and with ERFA for leap seconds. diff --git a/Rfc3339.lean b/Rfc3339.lean index e4a567a..70cee98 100644 --- a/Rfc3339.lean +++ b/Rfc3339.lean @@ -8,3 +8,4 @@ import Rfc3339.Calendar import Rfc3339.Format import Rfc3339.Instant import Rfc3339.FromUnix +import Rfc3339.Leap diff --git a/Rfc3339/Leap.lean b/Rfc3339/Leap.lean new file mode 100644 index 0000000..641fba1 --- /dev/null +++ b/Rfc3339/Leap.lean @@ -0,0 +1,71 @@ +/- + Leap seconds: the table of the months that ended in one, validity by + that table as section 5.7 asks, SI seconds since 1972 that give each + leap second a number of its own, and TAI − UTC. +-/ + +import Rfc3339.FromUnix + +namespace Rfc3339 + +/-- The months, as (year, month), whose last second in UTC was a leap + second, 23:59:60: the 27 of IERS Bulletin C, as tzdata's + `leap-seconds.list` gives them. That file expires on 28 June 2027: + no leap second comes before then that is not in it. -/ +def leapMonths : List (Nat × Nat) := + [(1972, 6), (1972, 12), (1973, 12), (1974, 12), (1975, 12), (1976, 12), (1977, 12), + (1978, 12), (1979, 12), (1981, 6), (1982, 6), (1983, 6), (1985, 6), (1987, 12), + (1989, 12), (1990, 12), (1992, 6), (1993, 6), (1994, 6), (1995, 12), (1997, 6), + (1998, 12), (2005, 12), (2008, 12), (2012, 6), (2015, 6), (2016, 12)] + +/-- The year and month, in UTC, of the minute the timestamp falls in. -/ +def Timestamp.utcMonth (t : Timestamp) : Nat × Nat := + let (y, m, _) := fromDayNumber (t.utcMinute / 1440).toNat + (y, m) + +/-- Whether `t` is valid and, if its second is 60, one of the leap + seconds of the table: section 5.7 allows second 60 only "at the end + of months in which a leap second occurs". -/ +def Timestamp.isValidKnown (t : Timestamp) : Bool := + t.isValid && (t.second != 60 || leapMonths.contains t.utcMonth) + +/-- The place of the leap second at the end of month `ym` in the order + `utcMinute * 61 + second`: second 60 of the last minute before the + next month. -/ +def leapKey (ym : Nat × Nat) : Int := + let next := if ym.2 = 12 then dayNumber (ym.1 + 1) 1 1 else dayNumber ym.1 (ym.2 + 1) 1 + (((next * 1440 : Nat) : Int) - 1) * 61 + 60 + +/-- How many leap seconds of the table come before the second the + timestamp falls in. -/ +def Timestamp.leapsBefore (t : Timestamp) : Nat := + (leapMonths.filter fun ym => leapKey ym < t.utcMinute * 61 + t.second).length + +/-- SI seconds from 1972-01-01T00:00:00Z to the timestamp, leaving out + the fraction: Unix seconds, which give each day 86400, and one more + for each leap second of the table before it. 63072000 is the Unix + seconds of 1972-01-01T00:00:00Z. -/ +def Timestamp.siSeconds (t : Timestamp) : Int := + t.unixSeconds - 63072000 + t.leapsBefore + +/-- TAI − UTC at the timestamp, in seconds: 10 from the start of 1972, + and one more after each leap second. -/ +def Timestamp.taiMinusUtc (t : Timestamp) : Nat := + 10 + t.leapsBefore + +/-- The SI seconds of each leap second of the table. -/ +def leapSiSeconds : List Int := + (leapMonths.zipIdx).map fun (ym, i) => (leapKey ym + 1) / 61 * 60 - 719528 * 86400 - 63072000 + i + +/-- The UTC timestamp `n` SI seconds after 1972-01-01T00:00:00Z, with + second 60 at each leap second of the table, no fraction, and offset + `Z`; `none` below 0 or after 9999-12-31T23:59:59Z. -/ +def fromSiSeconds (n : Int) : Option Timestamp := + if n < 0 then none + else + let k := (leapSiSeconds.filter (· < n)).length + if leapSiSeconds.contains n then + (fromUnixSeconds (n + 63072000 - k - 1)).map fun t => { t with second := 60 } + else fromUnixSeconds (n + 63072000 - k) + +end Rfc3339 diff --git a/SPEC.md b/SPEC.md index 187bcff..08736c3 100644 --- a/SPEC.md +++ b/SPEC.md @@ -18,7 +18,7 @@ time-offset = "Z" / ("+" / "-") time-hour ":" time-minute - Every field has exactly the number of digits the grammar gives. A digit is an ASCII digit, `0` to `9`. The parser rejects digits from other scripts, such as `٣` and `０`. - The year runs from 0000 to 9999 and the month from 01 to 12. The day runs from 01 to the length of its month, as in the table of section 5.7. February has 29 days in a leap year and 28 otherwise. A leap year is one divisible by 4, unless it is divisible by 100 and not by 400 (Appendix C). - The hour runs from 00 to 23 and the minute from 00 to 59. The second runs from 00 to 59. It may be 60 only for a leap second, which section 5.7 places at the end of a month in UTC. With the offset applied, the time must be 23:59 UTC on the last day of a month. Because the leap second is shifted by the offset, `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. -- Section 5.7 allows second 60 only at the end of months in which a leap second occurs. This library keeps no table of them, so it allows second 60 at the end of every month, which is more than section 5.7 allows. It also allows second 59 everywhere, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. `Spec.Valid` states the rule as this library applies it. +- Section 5.7 allows second 60 only at the end of months in which a leap second occurs. `isValid` and `parse` use no table of them, so they allow second 60 at the end of every month, which is more than section 5.7 allows; `isValidKnown`, below, checks it against the table. It also allows second 59 everywhere, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. `Spec.Valid` states the rule as this library applies it. - The fraction is optional. When present it is a point and at least one digit, with no upper limit on the digits. The parser keeps every digit as written. - The offset is `Z`, `+hh:mm` or `-hh:mm`, with hours from 00 to 23 and minutes from 00 to 59. Section 4.3 gives `-00:00` its own meaning, an unknown local offset. It is therefore kept apart from `+00:00` and from `Z`, although all three name the same instant. - The note under the grammar lets `T` and `Z` be written in lower case. The parser accepts `t` and `z`, and printing writes upper case. @@ -50,9 +50,20 @@ POSIX time has no number for a leap second. As in POSIX time, second 60 is count 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`. +## Leap seconds, with the table + +Section 5.7 allows second 60 only "at the end of months in which a leap second occurs". `isValid` cannot know those months; `isValidKnown` uses a table of them. The table is tzdata's `leap-seconds.list`, which publishes IERS Bulletin C. `Spec/Leap.lean` copies it line for line: 28 NTP times, from 1 January 1972 to 1 January 2017, each with TAI − UTC from that time on, 10 to 37 seconds. Each line after the first follows a leap second, the second `23:59:60` UTC just before it, so there have been 27. The file expires on 28 June 2027: until then, no leap second comes that it does not list. + +- `isValidKnown` is `isValid`, with second 60 allowed only at one of the table's leap seconds. The instant is what counts, whatever the offset: `1990-12-31T15:59:60-08:00` is the leap second at the end of 1990, and `2017-01-01T00:59:60+01:00` the one at the end of 2016. `2015-12-31T23:59:60Z` is refused, since that leap second came at the end of June 2015. +- `siSeconds` gives the Unix seconds from `1972-01-01T00:00:00Z`, ignoring the fraction, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds between them. So `2016-12-31T23:59:59Z`, `2016-12-31T23:59:60Z` and `2017-01-01T00:00:00Z` get three numbers in a row, where Unix seconds give the last two the same one. On whole seconds valid by the table, these numbers are in the order of the instants, as `compareInstant` gives it. +- `fromSiSeconds` goes back: from SI seconds to the UTC timestamp, a leap second as second 60. It gives one for every number from 0, `1972-01-01T00:00:00Z`, to that of `9999-12-31T23:59:59Z`, and `none` outside. +- `taiMinusUtc` gives TAI − UTC: 10, and one more for each leap second before the timestamp. At every second from 1972 on, a leap second aside, it is the table's second column. During a leap second it is still the value from before it. + +Before 1972, UTC ran on seconds of varying length, with TAI − UTC not a whole number of seconds. There `siSeconds` is Unix seconds less 63072000, 86400 to a day, as `Spec.siSeconds_eq` says, which are not SI seconds, and `taiMinusUtc` gives 10, which means nothing. A leap second announced after the table's date would need a new table, in the spec and in the code, and a new approval. + ## Errors -`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. +`parse` returns `none` for any string it does not accept, `fromUnixSeconds` for any number outside the years 0000 to 9999, and `fromSiSeconds` for any number outside 1972 to 9999. No function can fail any other way. ## The command-line tool @@ -61,11 +72,11 @@ 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`, `Timestamp.compareInstant` and `fromUnixSeconds`. +Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds`, `Timestamp.compareInstant`, `fromUnixSeconds`, `Timestamp.isValidKnown`, `Timestamp.siSeconds`, `Timestamp.taiMinusUtc` and `fromSiSeconds`. The `known` request prints `-` for TAI − UTC before 1972. ## What must always hold -Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the RFC and checked against its tables and against known day counts. +Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean` and, for the leap second table, `Spec/Leap.lean`. They are written from the RFC and checked against its tables and against known day counts. | Property | Theorem | |----------|---------| @@ -86,12 +97,20 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | `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` | +| `isValidKnown` decides `Spec.ValidKnown`: `Spec.Valid`, with second 60 only at a leap second of the table. | `Spec.isValidKnown_iff` | +| `siSeconds` is Unix seconds since 1972 and one more for each leap second of the table before the timestamp. | `Spec.siSeconds_eq` | +| On whole seconds valid by the table, `siSeconds` gives the order of the instants. | `Spec.siSeconds_order` | +| `fromSiSeconds n` is `t` exactly when `t` is in UTC, with no fraction, valid by the table, from 1972 on, and has SI seconds `n`; it gives one for every second from 1972 to 9999. | `Spec.fromSiSeconds_iff`, `Spec.fromSiSeconds_isSome` | +| `taiMinusUtc` is 10 and one more for each leap second of the table before the timestamp. | `Spec.taiMinusUtc_leapsBefore` | +| TAI − UTC from 1972 on, at each second but a leap second, is the table's value. | `Spec.taiMinusUtc_eq` | +| Leap seconds of the table and months without one; SI seconds and TAI − UTC around the first and the last; the round trip Unix seconds lose. | `Spec.leap_table_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`. +- `fromUnixSeconds` is fixed for every number, by `Spec.fromUnixSeconds_iff` and `Spec.fromUnixSeconds_isSome`, and `fromSiSeconds` likewise by its two statements. +- `isValidKnown` is fixed for every timestamp, and `siSeconds` for every valid one. `taiMinusUtc` is fixed for every valid timestamp, by `Spec.taiMinusUtc_leapsBefore`, and agrees with the table's column from 1972 on but at a leap second. - 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`. @@ -101,3 +120,4 @@ The differential tests compare the tool with two oracles: - 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. +- For leap seconds, tzdata's `leap-seconds.list` on the test machine, read by the test script itself, with the SI seconds and TAI − UTC worked out from it in Python. diff --git a/Spec.lean b/Spec.lean index 974a98c..bb85987 100644 --- a/Spec.lean +++ b/Spec.lean @@ -14,6 +14,7 @@ import Rfc3339 import Spec.Defs +import Spec.Leap open Rfc3339 @@ -175,3 +176,88 @@ theorem Spec.fromUnixSeconds_vectors : Rfc3339.fromUnixSeconds 253402300799 = some ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ ∧ Rfc3339.fromUnixSeconds (-62167219201) = none ∧ Rfc3339.fromUnixSeconds 253402300800 = none := sorry + +/-! ## Leap seconds, with the table -/ + +/-- `isValidKnown` decides section 5.7 with the table of leap seconds: + as `isValid`, but second 60 only at one of the table's leap seconds, + at the same instant whatever the offset. -/ +theorem Spec.isValidKnown_iff (t : Timestamp) : + t.isValidKnown = true ↔ Spec.ValidKnown t := sorry + +/-- `siSeconds` is the Unix seconds from 1972-01-01T00:00:00Z to the + timestamp, leaving out the fraction, and one more for each leap + second of the table before it. From 1972 on, those are the SI + seconds between them; before 1972 there are no leap seconds, and the + number is Unix seconds, 86400 to a day, not SI seconds. -/ +theorem Spec.siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : + t.siSeconds = Spec.siSeconds t := sorry + +/-- On whole seconds, valid by the table, `siSeconds` orders timestamps + exactly as the instants they name. So no two instants share a + number, a leap second and the second after it included. -/ +theorem Spec.siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) + (fa : a.fraction = []) (fb : b.fraction = []) : + compare a.siSeconds b.siSeconds = a.compareInstant b := sorry + +/-- `fromSiSeconds` turns SI seconds since 1972-01-01T00:00:00Z back into + a timestamp: the one, at most one, in UTC, with no fraction, valid by + the table and from 1972 on, that has those SI seconds. A leap second + comes back as second 60. -/ +theorem Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : + fromSiSeconds n = some t ↔ + t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Spec.siSeconds t = n := sorry + +/-- `fromSiSeconds` gives a timestamp exactly for the seconds from + 1972-01-01T00:00:00Z to 9999-12-31T23:59:59Z. -/ +theorem Spec.fromSiSeconds_isSome (n : Int) : + (fromSiSeconds n).isSome ↔ + 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry + +/-- `taiMinusUtc` is 10, and one more for each leap second of the table + before the timestamp. So during a leap second it is still the value + from before it. (Before 1972, UTC was not a whole number of seconds + from TAI, and the 10 there means nothing.) -/ +theorem Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Spec.Valid t) : + t.taiMinusUtc = 10 + Spec.leapsBefore t := sorry + +/-- TAI − UTC at each second from 1972 on, other than a leap second, is + the value the table's second column gives for it. The code never + reads that column: it counts leap seconds. -/ +theorem Spec.taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : + t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := sorry + +/-- The leap seconds of section 5.8, the first and the last of the + table, one seen from another offset, and second 60 in months that + had none; SI seconds and TAI − UTC around the first and the last; + and the round trip that Unix seconds lose and SI seconds keep. -/ +theorem Spec.leap_table_vectors : + Timestamp.isValidKnown ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = true ∧ + Timestamp.isValidKnown ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ + Timestamp.isValidKnown ⟨2017, 1, 1, 0, 59, 60, [], .plus 1 0⟩ = true ∧ + Timestamp.isValidKnown ⟨2015, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.isValidKnown ⟨1971, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.isValidKnown ⟨2026, 12, 31, 23, 59, 60, [], .z⟩ = false ∧ + Timestamp.siSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 0 ∧ + Timestamp.siSeconds ⟨1972, 6, 30, 23, 59, 59, [], .z⟩ = 15724799 ∧ + Timestamp.siSeconds ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = 15724800 ∧ + Timestamp.siSeconds ⟨1972, 7, 1, 0, 0, 0, [], .z⟩ = 15724801 ∧ + Timestamp.siSeconds ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ = 1420156827 ∧ + Timestamp.siSeconds ⟨2016, 12, 31, 23, 59, 59, [], .z⟩ = 1420156825 ∧ + Timestamp.siSeconds ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = 1420156826 ∧ + Timestamp.taiMinusUtc ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 6, 30, 23, 59, 59, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = 10 ∧ + Timestamp.taiMinusUtc ⟨1972, 7, 1, 0, 0, 0, [], .z⟩ = 11 ∧ + Timestamp.taiMinusUtc ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ = 36 ∧ + Timestamp.taiMinusUtc ⟨2016, 12, 31, 23, 59, 59, [], .z⟩ = 36 ∧ + Timestamp.taiMinusUtc ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ = 37 ∧ + fromSiSeconds 15724800 = some ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ ∧ + fromSiSeconds 1420156826 = some ⟨2016, 12, 31, 23, 59, 60, [], .z⟩ ∧ + fromSiSeconds 1420156827 = some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ ∧ + fromUnixSeconds (Timestamp.unixSeconds ⟨2016, 12, 31, 23, 59, 60, [], .z⟩) = + some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ := sorry diff --git a/Spec/Leap.lean b/Spec/Leap.lean new file mode 100644 index 0000000..85698c8 --- /dev/null +++ b/Spec/Leap.lean @@ -0,0 +1,129 @@ +/- + The definitions the leap second statements use: the table of leap + seconds and TAI − UTC as tzdata's `leap-seconds.list` publishes it, + from IERS Bulletin C, and section 5.7 of RFC 3339 with that table. + Part of the approved specification, with `Spec.lean` and + `Spec/Defs.lean`, and written independently of the code in + `Rfc3339/`. +-/ + +import Spec.Defs + +open Rfc3339 + +/-! ## The table + +`leap-seconds.list`, as tzdata 2026e ships it in +`/usr/share/zoneinfo/leap-seconds.list`, is "Updated through IERS +Bulletin C", its last update at NTP time 3992312697 (its `#$` line), and +its own hash line reads `#h a9bad145 84c31c70 758402aa b37bfd54 +5923836a`. It defines its columns so: "NTP timestamp (X parameter) is +the number of seconds since 1900.0", and "DTAI: The difference DTAI= +TAI-UTC in units of seconds. It is the quantity to add to UTC to get the +time in TAI". NTP time counts 86400 seconds to every day. Each data line +is an NTP time and the DTAI from then on: + +``` +2272060800 10 # 1 Jan 1972 +2287785600 11 # 1 Jul 1972 +2303683200 12 # 1 Jan 1973 +2335219200 13 # 1 Jan 1974 +2366755200 14 # 1 Jan 1975 +2398291200 15 # 1 Jan 1976 +2429913600 16 # 1 Jan 1977 +2461449600 17 # 1 Jan 1978 +2492985600 18 # 1 Jan 1979 +2524521600 19 # 1 Jan 1980 +2571782400 20 # 1 Jul 1981 +2603318400 21 # 1 Jul 1982 +2634854400 22 # 1 Jul 1983 +2698012800 23 # 1 Jul 1985 +2776982400 24 # 1 Jan 1988 +2840140800 25 # 1 Jan 1990 +2871676800 26 # 1 Jan 1991 +2918937600 27 # 1 Jul 1992 +2950473600 28 # 1 Jul 1993 +2982009600 29 # 1 Jul 1994 +3029443200 30 # 1 Jan 1996 +3076704000 31 # 1 Jul 1997 +3124137600 32 # 1 Jan 1999 +3345062400 33 # 1 Jan 2006 +3439756800 34 # 1 Jan 2009 +3550089600 35 # 1 Jul 2012 +3644697600 36 # 1 Jul 2015 +3692217600 37 # 1 Jan 2017 +``` + +"File expires on 28 June 2027": the table holds until then. The first +line is the start of UTC as it is now, with TAI − UTC 10; each later +line follows a leap second, the second 23:59:60 UTC just before it. The +file adds that "so far, all leap seconds have been positive (a second has +been added to UTC)". +-/ + +/-- The table, line for line: NTP time, and TAI − UTC from then on. -/ +def Spec.leapTable : List (Nat × Nat) := + [(2272060800, 10), (2287785600, 11), (2303683200, 12), (2335219200, 13), + (2366755200, 14), (2398291200, 15), (2429913600, 16), (2461449600, 17), + (2492985600, 18), (2524521600, 19), (2571782400, 20), (2603318400, 21), + (2634854400, 22), (2698012800, 23), (2776982400, 24), (2840140800, 25), + (2871676800, 26), (2918937600, 27), (2950473600, 28), (2982009600, 29), + (3029443200, 30), (3076704000, 31), (3124137600, 32), (3345062400, 33), + (3439756800, 34), (3550089600, 35), (3644697600, 36), (3692217600, 37)] + +/-- NTP time from Unix seconds: NTP counts from 1900-01-01T00:00:00Z, + 70 years of 86400-second days, 17 of them leap years, before the + Unix epoch. -/ +def Spec.ntpOfUnix (u : Int) : Int := u + (70 * 365 + 17) * 86400 + +example : Spec.ntpOfUnix 0 = 2208988800 := by decide + +/-! ## Section 5.7, with the table + +"the leap second point is shifted by the zone offset (so it happens at +the same instant around the globe)": a timestamp with second 60 is a +leap second of the table when its Unix seconds, which count second 60 +as the start of the next minute, are those of a line after the first. +-/ + +/-- `t` names one of the table's leap seconds: its second is 60, and the + time just after it, in NTP time, is that of a line of the table + after the first. -/ +def Spec.TableLeapSecond (t : Timestamp) : Prop := + t.second = 60 ∧ ∃ e ∈ Spec.leapTable.tail, Spec.ntpOfUnix (Spec.unixSeconds t) = e.1 + +/-- Valid, by section 5.7 with the table: as `Spec.Valid`, and second 60 + only at a leap second of the table. -/ +def Spec.ValidKnown (t : Timestamp) : Prop := + Spec.Valid t ∧ (t.second = 60 → Spec.TableLeapSecond t) + +/-! ## SI seconds and TAI − UTC -/ + +/-- The place of a timestamp's whole second in UTC order: its UTC minute + and its second, with 61 places to a minute, as `Spec.instantKey` + with no fraction. -/ +def Spec.secondKey (t : Timestamp) : Int := Spec.utcMinute t * 61 + t.second + +/-- The same place for the leap second just before NTP time `ntp`: + second 60 of the minute before it. -/ +def Spec.leapSecondKey (ntp : Nat) : Int := + (((ntp : Int) - Spec.ntpOfUnix 0) / 60 + ((Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int) - 1) * 61 + 60 + +/-- How many leap seconds of the table come before the second `t` falls + in. -/ +def Spec.leapsBefore (t : Timestamp) : Nat := + (Spec.leapTable.tail.filter fun e => Spec.leapSecondKey e.1 < Spec.secondKey t).length + +/-- SI seconds from 1972-01-01T00:00:00Z to `t`, without its fraction: + the Unix seconds between them, which count 86400 to every day, and + one more for each leap second of the table between them. -/ +def Spec.siSeconds (t : Timestamp) : Int := + Spec.unixSeconds t - Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ + Spec.leapsBefore t + +/-- TAI − UTC at NTP time `ntp`: the value on the table's last line at + or before it. -/ +def Spec.taiMinusUtcAt (ntp : Int) : Nat := + ((Spec.leapTable.filter fun e => (e.1 : Int) ≤ ntp).getLast?.map (·.2)).getD 0 + +example : Spec.taiMinusUtcAt 2272060800 = 10 ∧ Spec.taiMinusUtcAt 3692217599 = 36 ∧ + Spec.taiMinusUtcAt 3692217600 = 37 := by decide diff --git a/bar.toml b/bar.toml index 505ea7d..7baee02 100644 --- a/bar.toml +++ b/bar.toml @@ -15,12 +15,13 @@ entry_points = ["Main.lean"] [spec] # Rfc3339/Types.lean holds the types every statement is about, so it is # part of the specification. -files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Rfc3339/Types.lean"] +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Spec/Leap.lean", "Rfc3339/Types.lean"] # The code under proof: the functions the statements are about. code = [ "Rfc3339.parse", "Rfc3339.Timestamp.print", "Rfc3339.Timestamp.isValid", "Rfc3339.Timestamp.unixSeconds", "Rfc3339.Timestamp.compareInstant", - "Rfc3339.fromUnixSeconds", + "Rfc3339.fromUnixSeconds", "Rfc3339.Timestamp.isValidKnown", "Rfc3339.Timestamp.siSeconds", + "Rfc3339.Timestamp.taiMinusUtc", "Rfc3339.fromSiSeconds", ] # One entry per approval, added in a pull request the reviewer approves. diff --git a/comparator.json b/comparator.json index 60399c4..2924454 100644 --- a/comparator.json +++ b/comparator.json @@ -18,7 +18,15 @@ "Spec.syntax_vectors", "Spec.fromUnixSeconds_iff", "Spec.fromUnixSeconds_isSome", - "Spec.fromUnixSeconds_vectors" + "Spec.fromUnixSeconds_vectors", + "Spec.isValidKnown_iff", + "Spec.siSeconds_eq", + "Spec.siSeconds_order", + "Spec.fromSiSeconds_iff", + "Spec.fromSiSeconds_isSome", + "Spec.taiMinusUtc_leapsBefore", + "Spec.taiMinusUtc_eq", + "Spec.leap_table_vectors" ], "permitted_axioms": [ "propext", diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 4cbdf35..2eb1491 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -6,20 +6,27 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified - Go: `time.Parse(time.RFC3339Nano, s)`, go version go1.24.7 linux/amd64 - rfc3339-validator 0.1.4 (Python 3.13.17), called on the string as given. `jsonschema` calls it for its `date-time` check on the upper-cased string, so the lower case rows below do not apply to `jsonschema`. - Seed: 20261025 -- Strings: 256755 +- Strings: 182166 - Strings both this project and Go accept, read to a different instant: 0 Where each parser differs from this one, by the first category that fits the string: | Parser | Differs by | Category | Strings | Example | | --- | --- | --- | --- | --- | -| Go | rejects | lower case t or z | 28347 | `'1985-04-12t23:20:50.52z'`, `'3864-12-02t01:14:12.577732z'` | -| Go | rejects | second 60 | 4691 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| Go | accepts | offset hour above 23 or minute above 59 | 3033 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | -| Go | accepts | a field with one digit | 702 | `'5585-08-01T5:46:19.534-17:35'`, `'2098-08-07T1:15:55-19:39'` | -| Go | accepts | comma before the fraction | 5 | `'2000-01-01T00:00:00,5Z'`, `'3237-07-31T04:42:37,135148-08:01'` | -| rfc3339-validator | rejects | lower case t or z | 28347 | `'1985-04-12t23:20:50.52z'`, `'3864-12-02t01:14:12.577732z'` | -| rfc3339-validator | rejects | second 60 | 4691 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| rfc3339-validator | rejects | year 0000 | 1583 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | -| rfc3339-validator | accepts | line break at the end | 1330 | `'2513-04-29T17:09:04.19696594243724-20:08\n'`, `'8984-09-01T04:21:23+15:45\n'` | +| Go | rejects | lower case t or z | 18971 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| Go | rejects | second 60 | 3784 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| Go | accepts | offset hour above 23 or minute above 59 | 1978 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | +| Go | accepts | a field with one digit | 448 | `'0099-09-29T8:05:14.9-13:23'`, `'0508-04-01T2:41:06.3-08:38'` | +| Go | accepts | comma before the fraction | 4 | `'2000-01-01T00:00:00,5Z'`, `'1900-01-02T22:19:55,9-00:00'` | +| rfc3339-validator | rejects | lower case t or z | 18971 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| rfc3339-validator | rejects | second 60 | 3784 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| rfc3339-validator | rejects | year 0000 | 1248 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | +| rfc3339-validator | accepts | line break at the end | 891 | `'4244-06-01T08:05:55.054876690884+00:00\n'`, `'8593-06-30T13:42:25+05:44\n'` | + + +## Leap seconds + +- ERFA, through pyerfa 2.0.1.5, with its own leap second table +- Timestamps known valid by the table, from 1972 on, given to ERFA: 22611. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 2949. +- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8666. Different: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index bb0dd24..103614d 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,17 +2,20 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `datetime` and `calendar`, and the RFC 3339 rules copied into this script +- Oracle: Python 3.13.17 `datetime` and `calendar`, the RFC 3339 rules copied into this script, and for leap seconds tzdata's `/usr/share/zoneinfo/leap-seconds.list`, read by this script - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 300000 -- 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 +- Mutated: 67878 of the inputs are mutated timestamps +- By kind: compare 29413, error 44, fromsi 9360, fromunix 44543, grid 16998, known 34497, mutated 67878, near miss 29254, valid 68013 +- Strings parsed: 182143, of which 83519 accepted (4666 with a leap second) and 98624 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77331 +- Pairs ordered: 29413 (9874 before, 8322 same instant, 9754 after, 1463 with a string rejected) +- Unix seconds turned back into timestamps: 44543, of which 679 outside years 0000 to 9999 +- Leap second table: /usr/share/zoneinfo/leap-seconds.list, 28 lines, 27 leap seconds, expires 2027-06-28, last updated at NTP time 3992312697, hash line `a9bad145 84c31c70 758402aa b37bfd54 5923836a` +- Timestamps checked against the table (`known`): 34497, of which 267 leap seconds of the table, 6367 with a second 60 it does not list, and 2570 rejected +- SI seconds turned back into timestamps (`fromsi`): 9360, of which 27 leap seconds and 695 outside 1972 to 9999 +- Malformed requests answered `error`: 44 of 44 - 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/cross_check.py b/tests/cross_check.py index 6cfd605..f2182b4 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -16,8 +16,18 @@ `rfc3339_validator.validate_rfc3339`. Where a parser accepts what this one rejects, or the reverse, the string is put in the first category below that fits it. Where Go and this tool both accept a string, the -instants must match to the nanosecond. The counts go to -tests/CROSS-CHECK.md. +instants must match to the nanosecond. + +For the leap second table, the timestamps tests/run_tests.py sends as +`known` requests, and the SI seconds it sends as `fromsi`, go to ERFA, +a BSD-licensed C library derived from the IAU's SOFA, through pyerfa, which keeps its +own leap second table: `dat` gives TAI - UTC, and `dtf2d` with `utctai` +the TAI time, from which the SI seconds since 1972-01-01T00:00:00Z +follow. It needs pyerfa: + + pip install --target .lake/oracle-packages pyerfa==2.0.1.5 + +The counts go to tests/CROSS-CHECK.md. """ import argparse @@ -92,6 +102,85 @@ def go_version(): return out.stdout.strip() +def erfa_elapsed(erfa, y, mo, d, h, mi, sec, base): + """SI seconds from `base`, a TAI two-part Julian date, to the UTC time, + by ERFA.""" + u1, u2 = erfa.dtf2d("UTC", y, mo, d, h, mi, float(sec)) + t1, t2 = erfa.utctai(u1, u2) + return round(((t1 - base[0]) + (t2 - base[1])) * 86400) + + +def leap_section(args): + sys.path.insert(0, str(ROOT / ".lake" / "oracle-packages")) + try: + import erfa + except ImportError: + sys.exit("needs pyerfa: pip install --target .lake/oracle-packages pyerfa==2.0.1.5") + import warnings + from importlib.metadata import version + # ERFA warns of a "dubious year" after its table's last entry; its + # answers still assume no later leap second, as the table here does. + warnings.simplefilter("ignore") + items = list(run_tests.cases(args.seed, args.count)) + knowns = [bytes.fromhex(req.split(" ")[1]).decode("utf-8") for label, req, _, _ in items + if label == "known"] + sis = [int(req.split(" ")[1]) for label, req, _, _ in items if label == "fromsi"] + ours_k, problem = run_tests.run_tool("".join(f"known {run_tests.hexed(k)}\n" for k in knowns)) + if problem or len(ours_k) != len(knowns): + sys.exit(f"the tool failed: {problem}") + ours_s, problem = run_tests.run_tool("".join(f"fromsi {n}\n" for n in sis)) + if problem or len(ours_s) != len(sis): + sys.exit(f"the tool failed: {problem}") + b1, b2 = erfa.dtf2d("UTC", 1972, 1, 1, 0, 0, 0.0) + base = erfa.utctai(b1, b2) + k_checked, k_before, k_diff = 0, 0, [] + for s, ours in zip(knowns, ours_k): + if not ours.startswith("OK"): + continue + _, si, tai = ours.split("\t") + if tai == "-": + k_before += 1 + continue + f = run_tests.reference(s) + utc, _ = run_tests.utc_parts(f) + # utc_parts moves years `datetime` cannot hold by 400 years; move + # the UTC year back. + year = utc.year + f["year"] - run_tests.shifted(f["year"])[0] + theirs_tai = erfa.dat(year, utc.month, utc.day, + (utc.hour * 3600 + utc.minute * 60 + f["second"]) / 86400) + theirs_si = erfa_elapsed(erfa, year, utc.month, utc.day, utc.hour, utc.minute, + f["second"], base) + k_checked += 1 + if (int(si), int(tai)) != (theirs_si, round(theirs_tai)): + k_diff.append((s, ours, f"{theirs_si}\t{theirs_tai}")) + s_checked, s_leaps, s_diff = 0, 0, [] + for n, ours in zip(sis, ours_s): + if ours == "NONE": + continue + m = re.fullmatch(r"([0-9]{4})-([0-9]{2})-([0-9]{2})T([0-9]{2}):([0-9]{2}):([0-9]{2})Z", ours) + y, mo, d, h, mi, sec = map(int, m.groups()) + s_checked += 1 + s_leaps += sec == 60 + theirs = erfa_elapsed(erfa, y, mo, d, h, mi, sec, base) + if theirs != n: + s_diff.append((n, ours, theirs)) + lines = [ + "", + "## Leap seconds", + "", + f"- ERFA, through pyerfa {version('pyerfa')}, with its own leap second table", + f"- Timestamps known valid by the table, from 1972 on, given to ERFA: {k_checked}. " + f"Different SI seconds since 1972 or TAI - UTC: {len(k_diff)}. Before 1972, where " + f"TAI - UTC was not a whole number of seconds, not compared: {k_before}.", + f"- SI seconds turned back into timestamps, of which {s_leaps} leap seconds, and given " + f"to ERFA for their SI seconds: {s_checked}. Different: {len(s_diff)}.", + "", + ] + lines += [f"- `{s}`: this project `{o}`, ERFA `{t}`" for s, o, t in k_diff[:10]] + lines += [f"- `fromsi {n}`: this project `{o}`, ERFA's SI seconds `{t}`" for n, o, t in s_diff[:10]] + return lines + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=20261025) @@ -161,6 +250,7 @@ def main(): lines.append("") for s, theirs, ours in value_mismatch[:20]: lines.append(f"- Different instant: `{s!r}`: Go `{theirs}`, this project `{ours}`") + lines += leap_section(args) REPORT.write_text("\n".join(lines) + "\n", encoding="utf-8") print(f"{len(strings)} strings; report in {REPORT}") diff --git a/tests/run_tests.py b/tests/run_tests.py index b278528..85e8362 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -41,6 +41,16 @@ 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; +- for the leap second table, a third oracle: tzdata's + `leap-seconds.list`, read here line by line, apart from the Lean code. + `known` requests must give the SI seconds and TAI − UTC it implies, + or NOLEAP for a second 60 it does not list. The inputs are 23:59:58, + 23:59:59, 23:59:60 and the next 00:00:00 at every month end from 1970 + to 2030, in UTC and spelled under seven offsets, and random valid + timestamps, near misses and mutated strings, which `known` must refuse + wherever `parse` does. `fromsi` requests take every leap second's SI seconds and + the two seconds either side, the ends of the range and one past each, + random numbers, and the SI seconds of random timestamps; - malformed requests, which the tool must answer with `error`. Every seventh request ends in CR LF. The first 20,000 parsed strings @@ -110,6 +120,94 @@ def from_unix(n): f"{d.hour:02d}:{d.minute:02d}:{d.second:02d}Z") +# The leap second table: tzdata's leap-seconds.list, read here, apart from +# the Lean code. Each line: an NTP time, and TAI - UTC from then on. +LEAP_FILE = Path("/usr/share/zoneinfo/leap-seconds.list") +NTP_UNIX = 2208988800 +EPOCH_1972 = 63072000 + + +def leap_table(): + if not LEAP_FILE.exists(): + sys.exit(f"needs tzdata's {LEAP_FILE}, the leap second table the tests check against") + rows, expires = [], None + for line in LEAP_FILE.read_text().splitlines(): + if line.startswith("#$"): + LEAP_FILE_INFO["updated"] = int(line.split()[1]) + elif line.startswith("#h"): + LEAP_FILE_INFO["hash"] = " ".join(line.split()[1:]) + elif line.startswith("#@"): + expires = int(line.split()[1]) + elif line.strip() and not line.startswith("#"): + ntp, off = line.split()[:2] + rows.append((int(ntp), int(off))) + return rows, expires + + +LEAP_FILE_INFO = {} +LEAP_TABLE, LEAP_EXPIRES = leap_table() +# The Unix seconds of the midnight after each leap second, which is also +# what Unix seconds give the leap second itself. +LEAP_MIDNIGHTS = [ntp - NTP_UNIX for ntp, _ in LEAP_TABLE[1:]] +# The SI seconds since 1972 of each leap second. +LEAP_SI = [m - EPOCH_1972 + i for i, m in enumerate(LEAP_MIDNIGHTS)] + + +def known(s): + """The expected answer to `known`: SI seconds since 1972 and TAI - UTC + by the table, NOLEAP for a second 60 the table does not list, or + REJECT.""" + f = reference(s) + if f is None: + return "REJECT" + u = f["unix"] + if f["second"] == 60: + if u not in LEAP_MIDNIGHTS: + return "NOLEAP" + before = LEAP_MIDNIGHTS.index(u) + tai = LEAP_TABLE[before][1] + else: + before = sum(1 for m in LEAP_MIDNIGHTS if m <= u) + tai = max((off for ntp, off in LEAP_TABLE if ntp <= u + NTP_UNIX), default=None) + return f"OK\t{u - EPOCH_1972 + before}\t{tai if u >= EPOCH_1972 else '-'}" + + +def from_si(n): + """The expected answer to `fromsi n`, by the table and `from_unix`.""" + if n < 0: + return "NONE" + k = sum(1 for x in LEAP_SI if x < n) + if n in LEAP_SI: + r = from_unix(n + EPOCH_1972 - k - 1) + return r if r == "NONE" else r[:17] + "60" + r[19:] + return from_unix(n + EPOCH_1972 - k) + + +def month_end_grid(): + """23:59:58 to the next 00:00:00 at every month end from 1970 to 2030, + in UTC and spelled under other offsets.""" + for year in range(1970, 2031): + for month in range(1, 13): + last = month_length(year, month) + base = datetime(year, month, last, 23, 59) + for off in (0, 60, -480, 330, 1439, -1439, 765): + local = base + timedelta(minutes=off) + text = "Z" if off == 0 else (f"+{off // 60:02d}:{off % 60:02d}" if off > 0 else + f"-{-off // 60:02d}:{-off % 60:02d}") + for sec in (58, 59, 60): + yield stamp(local.year, local.month, local.day, local.hour, local.minute, + sec, "", text) + nxt = local + timedelta(minutes=1) + yield stamp(nxt.year, nxt.month, nxt.day, nxt.hour, nxt.minute, 0, "", text) + + +def si_grid(): + for x in LEAP_SI: + yield from (x - 2, x - 1, x, x + 1, x + 2) + top = LAST - EPOCH_1972 + len(LEAP_SI) + yield from (-1, 0, 1, top - 1, top, top + 1, 10 ** 20, -10 ** 20) + + 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 @@ -450,6 +548,34 @@ def same_instant_pair(rng): ("fromunix 1.5", "a fraction"), ("fromunix 0x10", "hex"), ("fromunix \u0663", "a digit that is not ASCII"), + ("known", "no argument"), + ("known 3", "an odd number of hex digits"), + ("known 30 30", "two arguments"), + ("known ff", "not UTF-8"), + ("fromsi", "no number"), + ("fromsi +1", "a plus sign"), + ("fromsi 1.5", "a fraction"), + ("fromsi 1 2", "two numbers"), + ("fromsi 1_000", "an underscore"), + ("fromsi -", "a sign alone"), + ("fromsi --1", "two signs"), + ("fromsi 0x10", "hex"), + ("fromsi \u0663", "a digit that is not ASCII"), + ("known 3G", "not a hex digit"), + ("known 3A", "hex digits are lower case"), + ("known c0af", "an overlong encoding, not UTF-8"), + ("known eda080", "a surrogate, not UTF-8"), +] + +# Strings `known` must answer REJECT, not NOLEAP: second 60 away from a +# UTC month end, second 61, an offset out of range, and no timestamp. +KNOWN_REJECT = [ + "1990-12-30T23:59:60Z", + "1990-12-31T23:59:61Z", + "1990-12-31T23:59:60+24:00", + "2015-02-30T00:00:00Z", + "", + "garbage", ] # A last line with no LF must still be answered. @@ -467,7 +593,11 @@ def hexed(s): def cases(seed, count): """(label, request, expected answer, mutated) for each input.""" rng = random.Random(seed) - fixed = [] + # The short lists first, so that a run with a small count has them. + fixed = [("error", req, "error", False) for req, _ in MALFORMED] + for s in KNOWN_REJECT: + assert known(s) == "REJECT", s + fixed.append(("known", f"known {hexed(s)}", "REJECT", False)) for s in itertools.chain(day_grid(), leap_grid(), edge_grid()): fixed.append(("grid", f"parse {hexed(s)}", answer(reference(s)), False)) edges = list(edge_grid()) @@ -475,15 +605,43 @@ def cases(seed, count): 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)) + for s in month_end_grid(): + fixed.append(("known", f"known {hexed(s)}", known(s), False)) + for n in si_grid(): + fixed.append(("fromsi", f"fromsi {n}", from_si(n), False)) made = 0 for item in fixed[:count]: yield item made += 1 while made < count: r = rng.random() + if r < 0.06: + r = rng.random() + if r < 0.65: + s = random_valid(rng) + elif r < 0.8: + s = leap_pair(rng)[0] + elif r < 0.9: + s = near_miss(rng) + else: + base = random_valid(rng) + s = mutate(rng, base) + yield ("known", f"known {hexed(s)}", known(s), False) + made += 1 + continue if r < 0.1: + r = rng.random() + if r < 0.4: + n = rng.randint(-10, LAST - EPOCH_1972 + 40) + elif r < 0.7: + n = rng.choice(LEAP_SI) + rng.randint(-86400, 86400) + else: + want = known(random_valid(rng)) + n = int(want.split("\t")[1]) if want.startswith("OK") else rng.randint(0, 10 ** 9) + yield ("fromsi", f"fromsi {n}", from_si(n), False) + made += 1 + continue + if r < 0.16: r = rng.random() if r < 0.3: n = rng.randint(FIRST - 10 ** 7, LAST + 10 ** 7) @@ -621,8 +779,9 @@ def check_mode(items, limit=20000, batch=500): def oracle(): - return (f"Python {platform.python_version()} `datetime` and `calendar`, and the " - f"RFC 3339 rules copied into this script") + return (f"Python {platform.python_version()} `datetime` and `calendar`, the " + f"RFC 3339 rules copied into this script, and for leap seconds tzdata's " + f"`{LEAP_FILE}`, read by this script") def lean_version(): @@ -713,6 +872,11 @@ def main(): 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"] + knowns = [want for label, _, want, _ in items if label == "known"] + known_leaps = sum(1 for label, req, want, _ in items if label == "known" and + want.startswith("OK") and reference(bytes.fromhex(req.split(" ")[1]).decode())["second"] == 60) + from_si_wants = [want for label, _, want, _ in items if label == "fromsi"] + expires = datetime(1900, 1, 1) + timedelta(seconds=LEAP_EXPIRES) if LEAP_EXPIRES else None mutated = sum(1 for item in items if item[3]) malformed = [got for item, got in zip(items, out) if item[0] == "error"] @@ -735,6 +899,16 @@ def main(): 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"- Leap second table: {LEAP_FILE}, {len(LEAP_TABLE)} lines, {len(LEAP_MIDNIGHTS)} leap " + f"seconds, expires {expires:%Y-%m-%d}, last updated at NTP time " + f"{LEAP_FILE_INFO.get('updated')}, hash line `{LEAP_FILE_INFO.get('hash')}`" + if expires else f"- Leap second table: {LEAP_FILE}", + f"- Timestamps checked against the table (`known`): {len(knowns)}, of which " + f"{known_leaps} leap seconds of the table, {knowns.count('NOLEAP')} with a second 60 it " + f"does not list, and {knowns.count('REJECT')} rejected", + f"- SI seconds turned back into timestamps (`fromsi`): {len(from_si_wants)}, of which " + f"{sum(1 for w in from_si_wants if w[17:19] == '60')} leap seconds and " + f"{from_si_wants.count('NONE')} outside 1972 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}",