diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: bar v2, as + # proposed in its pull request #2. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ae73679 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.lake/ +__pycache__/ diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..3767388 --- /dev/null +++ b/Main.lean @@ -0,0 +1,116 @@ +/- + Command line front end. + + rfc3339 check TIMESTAMP... + + prints, for each timestamp, its RFC 3339 form and its Unix seconds, + or `invalid`, and exits with 1 when any is invalid. + + rfc3339 serve + + answers requests on standard input, one per line, for the + differential tests. A string is sent as the hex digits of its UTF-8 + bytes, so that any character, a line break included, can be sent. + + parse HEX prints OK, then tab-separated: the printed form, + Unix seconds, year, month, day, hour, minute, + second, fraction digits, and offset; + or REJECT + compare HEX HEX prints <, = or >, or REJECT when either string + is not a timestamp + + A malformed request prints `error`: an unknown operation, hex digits + that are not in pairs, or bytes that are not UTF-8. A request line + may end in LF or CR LF. + + Every answer comes from the proved functions in `Rfc3339/`: `parse`, + `Timestamp.print`, `Timestamp.unixSeconds` and + `Timestamp.compareInstant`. The hex decoding and the request handling + here are covered by the tests, not by a proof. +-/ + +import Rfc3339 + +open Rfc3339 + +def hexValue (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat) + else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10) + else none + +def hexBytes : List Char → Option (List UInt8) + | [] => some [] + | a :: b :: rest => do + let hi ← hexValue a + let lo ← hexValue b + let bs ← hexBytes rest + pure ((hi * 16 + lo).toUInt8 :: bs) + | [_] => none + +/-- The string whose UTF-8 bytes the hex digits give. -/ +def fromHex (h : String) : Option String := do + let bs ← hexBytes h.toList + String.fromUTF8? ⟨bs.toArray⟩ + +def offsetText (o : Offset) : String := String.ofList o.render + +def fields (t : Timestamp) : List String := + [t.print, toString t.unixSeconds, toString t.year, toString t.month, toString t.day, + toString t.hour, toString t.minute, toString t.second, + String.join (t.fraction.map toString), offsetText t.offset] + +def showOrdering : Ordering → String + | .lt => "<" + | .eq => "=" + | .gt => ">" + +/-- The answer to one request line, or `none` when it is malformed. -/ +def request (line : String) : Option String := + match line.splitOn " " with + | ["parse", h] => do + let s ← fromHex h + pure <| match parse s with + | some t => "\t".intercalate ("OK" :: fields t) + | none => "REJECT" + | ["compare", ha, hb] => do + let a ← fromHex ha + let b ← fromHex hb + pure <| match parse a, parse b with + | some ta, some tb => showOrdering (ta.compareInstant tb) + | _, _ => "REJECT" + | _ => none + +/-- The line without its line ending: LF, or CR LF. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +def serve : IO Unit := do + let stdin ← IO.getStdin + let stdout ← IO.getStdout + repeat + let line ← stdin.getLine + if line.isEmpty then break + stdout.putStrLn ((request (chomp line)).getD "error") + +def check (args : List String) : IO UInt32 := do + let mut code : UInt32 := 0 + for s in args do + match parse s with + | some t => IO.println s!"{t.print}\t{t.unixSeconds}" + | none => + IO.println s!"invalid\t{s}" + code := 1 + return code + +def usage : String := + "usage: rfc3339 check TIMESTAMP...\n rfc3339 serve" + +def main (args : List String) : IO UInt32 := do + match args with + | "check" :: rest@(_ :: _) => check rest + | ["serve"] => serve; return 0 + | _ => IO.eprintln usage; return 2 diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..a0c5328 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,7 @@ +/- + The proofs, under the names the challenge file gives them. The + theorems themselves are in `Proofs/Main.lean`, from the lemmas in the + other files. +-/ + +import Proofs.Main diff --git a/Proofs/DayNumber.lean b/Proofs/DayNumber.lean new file mode 100644 index 0000000..9a9627b --- /dev/null +++ b/Proofs/DayNumber.lean @@ -0,0 +1,76 @@ +/- + The calendar code in `Rfc3339/Calendar.lean` and `Rfc3339/Instant.lean` + agrees with the definitions in `Spec/Defs.lean`: leap years, month + lengths, offsets in minutes, and the closed form of the day number. +-/ + +import Rfc3339 +import Spec.Defs + +namespace Rfc3339.Proofs.DayNumber + +open Rfc3339 + +theorem isLeapYear_eq (y : Nat) : isLeapYear y = Spec.isLeapYear y := by + unfold isLeapYear Spec.isLeapYear + by_cases h4 : y % 4 = 0 <;> by_cases h100 : y % 100 = 0 <;> by_cases h400 : y % 400 = 0 <;> + simp [h4, h100, h400] + +theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := by + unfold daysInMonth Spec.daysInMonth + rw [isLeapYear_eq] + match m with + | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 => simp + | n + 13 => + have : ¬ (n + 13 = 2) := by omega + have : ¬ (n + 13 = 4 ∨ n + 13 = 6 ∨ n + 13 = 9 ∨ n + 13 = 11) := by omega + have : ¬ (1 ≤ n + 13 ∧ n + 13 ≤ 12) := by omega + simp_all + +theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Spec.offsetMinutes o := by + cases o <;> simp [offsetMinutes, Spec.offsetMinutes] + +/-- One more year adds that year's length. -/ +theorem daysBeforeYear_succ (y : Nat) : + daysBeforeYear (y + 1) = daysBeforeYear y + Spec.yearLength y := by + unfold daysBeforeYear Spec.yearLength + by_cases h4 : y % 4 = 0 + · by_cases h100 : y % 100 = 0 + · by_cases h400 : y % 400 = 0 + · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h400] + simp only [hl, ite_true] + omega + · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h100, h400] + simp only [hl, Bool.false_eq_true, ite_false] + omega + · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h100] + simp only [hl, ite_true] + omega + · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h4] + simp only [hl, Bool.false_eq_true, ite_false] + omega + +theorem daysBeforeYear_eq (y : Nat) : + daysBeforeYear y = ((List.range y).map Spec.yearLength).sum := by + induction y with + | zero => rfl + | succ y ih => + rw [daysBeforeYear_succ, ih, List.range_succ, List.map_append, List.sum_append] + simp + +theorem daysBeforeMonth_eq (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : + daysBeforeMonth y m = ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum := by + unfold daysBeforeMonth + rw [isLeapYear_eq] + cases hl : Spec.isLeapYear y <;> + match m, h1, h2 with + | 1, _, _ | 2, _, _ | 3, _, _ | 4, _, _ | 5, _, _ | 6, _, _ + | 7, _, _ | 8, _, _ | 9, _, _ | 10, _, _ | 11, _, _ | 12, _, _ => + simp [List.range_succ, Spec.daysInMonth, hl] + +theorem dayNumber_eq (y m d : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : + dayNumber y m d = Spec.dayNumber y m d := by + unfold dayNumber Spec.dayNumber + rw [daysBeforeYear_eq, daysBeforeMonth_eq y m h1 h2] + +end Rfc3339.Proofs.DayNumber diff --git a/Proofs/Format.lean b/Proofs/Format.lean new file mode 100644 index 0000000..21f214f --- /dev/null +++ b/Proofs/Format.lean @@ -0,0 +1,265 @@ +/- + The printer and the parser of `Rfc3339/Format.lean` against the spec: + `asciiUpper` is `Spec.asciiUpper`, a valid timestamp renders as + `Spec.render` writes it, and `parseUpper` returns `t` exactly when `t` + is valid and the input is `t.render`. From these, `parse_iff'`. +-/ + +import Rfc3339 +import Spec.Defs + +namespace Rfc3339.Proofs.Format + +open Rfc3339 + +/-! ## Characters and printing -/ + +/-- `Char` order is the order of code points. -/ +theorem le_iff_toNat (a b : Char) : a ≤ b ↔ a.toNat ≤ b.toNat := Iff.rfl + +theorem asciiUpper_eq (c : Char) : asciiUpper c = Spec.asciiUpper c := by + unfold asciiUpper Spec.asciiUpper + simp only [le_iff_toNat] + rfl + +theorem print_toList (t : Timestamp) : t.print.toList = t.render := by + simp [Timestamp.print] + +theorem digitChar_eq (n : Nat) (h : n < 10) : Spec.digitChar n = digitChar n := by + have : ∀ i : Fin 10, Spec.digitChar i.val = digitChar i.val := by decide + exact this ⟨n, h⟩ + +/-- `pad4` and `pad2` write the last digits of any number, as `Spec.digits` does. -/ +theorem digits4 (n : Nat) : Spec.digits 4 n = pad4 n := by + simp [Spec.digits, pad4, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] + +theorem digits2 (n : Nat) : Spec.digits 2 n = pad2 n := by + simp [Spec.digits, pad2, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] + +theorem daysInMonth_le (y m : Nat) : daysInMonth y m ≤ 31 := by + unfold daysInMonth + split <;> (try split) <;> omega + +/-- The bounds on the fields that printing and parsing need. -/ +theorem isValid_bounds {t : Timestamp} (h : t.isValid = true) : + t.year ≤ 9999 ∧ t.month ≤ 12 ∧ t.day ≤ 31 ∧ t.hour ≤ 23 ∧ t.minute ≤ 59 ∧ t.second ≤ 60 ∧ + (∀ d ∈ t.fraction, d < 10) ∧ t.offset.isValid = true := by + simp only [Timestamp.isValid, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true] at h + have := daysInMonth_le t.year t.month + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> first | omega | simp_all + +theorem renderFraction_eq (f : List Nat) (h : ∀ d ∈ f, d < 10) : + renderFraction f = if f = [] then [] else ['.'] ++ f.map Spec.digitChar := by + cases f with + | nil => rfl + | cons d ds => + simp only [renderFraction, reduceCtorEq, ite_false, List.singleton_append, List.cons.injEq, + true_and] + apply List.map_congr_left + intro x hx + exact (digitChar_eq x (h x hx)).symm + +theorem offset_render_eq (o : Offset) : o.render = Spec.renderOffset o := by + cases o <;> simp [Offset.render, Spec.renderOffset, digits2] + +theorem render_eq (t : Timestamp) (h : t.isValid = true) : t.render = Spec.render t := by + have hb := isValid_bounds h + simp [Timestamp.render, Spec.render, digits4, digits2, renderFraction_eq t.fraction hb.2.2.2.2.2.2.1, + offset_render_eq] + +/-! ## Parsing -/ + +theorem digitValue_digitChar (n : Nat) (h : n < 10) : digitValue (digitChar n) = some n := by + have : ∀ i : Fin 10, digitValue (digitChar i.val) = some i.val := by decide + exact this ⟨n, h⟩ + +theorem digitValue_some {c : Char} {v : Nat} (h : digitValue c = some v) : + v < 10 ∧ digitChar v = c := by + unfold digitValue at h + split at h + · rename_i hc + simp only [le_iff_toNat] at hc + have h0 : ('0' : Char).toNat = 48 := rfl + have h9 : ('9' : Char).toNat = 57 := rfl + rw [h0, h9] at hc + injection h with h + subst h + refine ⟨by omega, ?_⟩ + unfold digitChar + rw [Nat.sub_add_cancel hc.1] + exact Char.ofNat_toNat c + · simp at h + +theorem two_pad2 (n : Nat) (h : n < 100) : + two (digitChar (n / 10 % 10)) (digitChar (n % 10)) = some n := by + simp [two, digitValue_digitChar, Nat.mod_lt] + omega + +theorem four_pad4 (n : Nat) (h : n < 10000) : + four (digitChar (n / 1000 % 10)) (digitChar (n / 100 % 10)) (digitChar (n / 10 % 10)) + (digitChar (n % 10)) = some n := by + simp [four, digitValue_digitChar, Nat.mod_lt] + omega + +theorem two_some {a b : Char} {n : Nat} (h : two a b = some n) : pad2 n = [a, b] := by + simp only [two, bind, Option.bind_eq_some_iff, pure] at h + obtain ⟨x, hx, y, hy, h⟩ := h + injection h with h + subst h + obtain ⟨hx1, hx2⟩ := digitValue_some hx + obtain ⟨hy1, hy2⟩ := digitValue_some hy + simp only [pad2] + rw [show (10 * x + y) / 10 % 10 = x by omega, show (10 * x + y) % 10 = y by omega, hx2, hy2] + +theorem four_some {a b c d : Char} {n : Nat} (h : four a b c d = some n) : pad4 n = [a, b, c, d] := by + simp only [four, bind, Option.bind_eq_some_iff, pure] at h + obtain ⟨w, hw, x, hx, y, hy, z, hz, h⟩ := h + injection h with h + subst h + obtain ⟨hw1, hw2⟩ := digitValue_some hw + obtain ⟨hx1, hx2⟩ := digitValue_some hx + obtain ⟨hy1, hy2⟩ := digitValue_some hy + obtain ⟨hz1, hz2⟩ := digitValue_some hz + simp only [pad4] + rw [show (1000 * w + 100 * x + 10 * y + z) / 1000 % 10 = w by omega, + show (1000 * w + 100 * x + 10 * y + z) / 100 % 10 = x by omega, + show (1000 * w + 100 * x + 10 * y + z) / 10 % 10 = y by omega, + show (1000 * w + 100 * x + 10 * y + z) % 10 = z by omega, hw2, hx2, hy2, hz2] + +/-- `takeDigits` splits its input: the digits it read, then the rest. -/ +theorem takeDigits_spec (l : List Char) : + l = (takeDigits l).1.map digitChar ++ (takeDigits l).2 := by + induction l with + | nil => rfl + | cons c cs ih => + simp only [takeDigits] + split + · rename_i v hv + simp only [List.map_cons, List.cons_append] + rw [(digitValue_some hv).2, ← ih] + · rfl + +theorem takeDigits_digits (ds : List Nat) (r : List Char) (hd : ∀ d ∈ ds, d < 10) + (hr : takeDigits r = ([], r)) : takeDigits (ds.map digitChar ++ r) = (ds, r) := by + induction ds with + | nil => exact hr + | cons d ds ih => + simp only [List.map_cons, List.cons_append, takeDigits] + rw [digitValue_digitChar d (hd d (by simp))] + simp only + rw [ih (fun x hx => hd x (by simp [hx]))] + +theorem takeDigits_offset (o : Offset) : takeDigits o.render = ([], o.render) := by + cases o <;> rfl + +/-- Whatever `parseFraction` reads is a rendered fraction. -/ +theorem parseFraction_spec {l r : List Char} {ds : List Nat} (h : parseFraction l = some (ds, r)) : + l = renderFraction ds ++ r := by + unfold parseFraction at h + split at h + · rename_i cs + simp only at h + split at h + · simp at h + · rename_i hne + injection h with h + have hs := takeDigits_spec cs + rw [h] at hs + cases ds with + | nil => rw [h] at hne; simp at hne + | cons d ds => simp only [renderFraction, List.cons_append, ← hs] + · injection h with h + injection h with h1 h2 + subst h1 h2 + rfl + +/-- The fraction digits stop at the offset, which never starts with a digit. -/ +theorem parseFraction_render (f : List Nat) (o : Offset) (hf : ∀ d ∈ f, d < 10) : + parseFraction (renderFraction f ++ o.render) = some (f, o.render) := by + cases f with + | nil => cases o <;> rfl + | cons d ds => + simp only [renderFraction, List.cons_append, parseFraction] + rw [takeDigits_digits (d :: ds) o.render hf (takeDigits_offset o)] + rfl + +theorem parseOffset_spec {l : List Char} {o : Offset} (h : parseOffset l = some o) : l = o.render := by + unfold parseOffset at h + split at h + · injection h with h + subst h + rfl + all_goals first + | (simp at h; done) + | simp only [bind, Option.bind_eq_some_iff, pure] at h + obtain ⟨x, hx, y, hy, h⟩ := h + injection h with h + subst h + simp only [Offset.render, two_some hx, two_some hy] + rfl + +theorem parseOffset_render (o : Offset) (h : o.isValid = true) : parseOffset o.render = some o := by + cases o with + | z => rfl + | plus a b => + simp only [Offset.isValid, Bool.and_eq_true, decide_eq_true_eq] at h + show parseOffset ['+', _, _, ':', _, _] = _ + simp only [parseOffset, two_pad2 a (by omega), two_pad2 b (by omega)] + rfl + | minus a b => + simp only [Offset.isValid, Bool.and_eq_true, decide_eq_true_eq] at h + show parseOffset ['-', _, _, ':', _, _] = _ + simp only [parseOffset, two_pad2 a (by omega), two_pad2 b (by omega)] + rfl + +/-! ## The parser -/ + +theorem parseUpper_sound {u : List Char} {t : Timestamp} (h : parseUpper u = some t) : + t.isValid = true ∧ u = t.render := by + unfold parseUpper at h + split at h + · simp only [bind, Option.bind_eq_some_iff] at h + obtain ⟨year, hy, month, hm, day, hd, hour, hh, minute, hn, second, hs, ⟨f, r⟩, hr, offset, ho, + hv⟩ := h + simp only at hv + split at hv + · rename_i hval + injection hv with hv + subst hv + refine ⟨hval, ?_⟩ + simp only at ho + rw [parseFraction_spec hr, parseOffset_spec ho] + simp only [Timestamp.render, four_some hy, two_some hm, two_some hd, two_some hh, two_some hn, + two_some hs, List.cons_append, List.nil_append] + · simp at hv + · simp at h + +theorem parseUpper_render {t : Timestamp} (h : t.isValid = true) : parseUpper t.render = some t := by + obtain ⟨hy, hm, hd, hh, hn, hs, hf, ho⟩ := isValid_bounds h + obtain ⟨year, month, day, hour, minute, second, fraction, offset⟩ := t + simp only at hy hm hd hh hn hs hf ho + simp only [Timestamp.render, pad4, pad2, List.cons_append, List.nil_append] + rw [parseUpper.eq_1] + simp only [four_pad4 year (by omega), two_pad2 month (by omega), two_pad2 day (by omega), + two_pad2 hour (by omega), two_pad2 minute (by omega), two_pad2 second (by omega)] + simp [parseFraction_render fraction offset hf, parseOffset_render offset ho, h] + +theorem parseUpper_iff (u : List Char) (t : Timestamp) : + parseUpper u = some t ↔ t.isValid = true ∧ u = t.render := by + constructor + · exact parseUpper_sound + · rintro ⟨h, rfl⟩ + exact parseUpper_render h + +theorem parse_iff' (s : String) (t : Timestamp) : + parse s = some t ↔ t.isValid = true ∧ s.toList.map Spec.asciiUpper = Spec.render t := by + have hmap : s.toList.map asciiUpper = s.toList.map Spec.asciiUpper := + List.map_congr_left (fun c _ => asciiUpper_eq c) + rw [parse, hmap, parseUpper_iff] + constructor + · rintro ⟨h, he⟩ + exact ⟨h, he.trans (render_eq t h)⟩ + · rintro ⟨h, he⟩ + exact ⟨h, he.trans (render_eq t h).symm⟩ + +end Rfc3339.Proofs.Format diff --git a/Proofs/Fraction.lean b/Proofs/Fraction.lean new file mode 100644 index 0000000..44ab6f0 --- /dev/null +++ b/Proofs/Fraction.lean @@ -0,0 +1,168 @@ +/- + The fraction comparison: `compareFraction` orders two digit lists the + same way as their values, each scaled to the longer list's length. + Also: a list of decimal digits reads as a number below `10 ^ length`. +-/ + +import Rfc3339 +import Spec.Defs + +namespace Rfc3339.Proofs.Fraction + +open Rfc3339 + +/-- Reading digits after a value `x` already read: `x` is shifted left + by the number of digits still to come. -/ +theorem foldl_digits (x : Nat) (ds : List Nat) : + List.foldl (fun acc d => 10 * acc + d) x ds = x * 10 ^ ds.length + Spec.fractionValue ds := by + induction ds generalizing x with + | nil => simp [Spec.fractionValue] + | cons d ds ih => + simp only [Spec.fractionValue, List.foldl_cons, List.length_cons] at * + rw [ih, ih (10 * 0 + d), Nat.pow_succ, Nat.mul_zero, Nat.zero_add, Nat.add_mul, + Nat.add_assoc] + congr 1 + rw [Nat.mul_comm 10 x, Nat.mul_assoc, Nat.mul_comm 10 (10 ^ ds.length)] + +theorem fractionValue_nil : Spec.fractionValue [] = 0 := rfl + +theorem fractionValue_cons (d : Nat) (ds : List Nat) : + Spec.fractionValue (d :: ds) = d * 10 ^ ds.length + Spec.fractionValue ds := by + have h := foldl_digits d ds + simpa [Spec.fractionValue] using h + +theorem fractionValue_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) : + Spec.fractionValue a < 10 ^ a.length := by + induction a with + | nil => simp [fractionValue_nil] + | cons d ds ih => + have hd : d ≤ 9 := ha d (by simp) + have hds : Spec.fractionValue ds < 10 ^ ds.length := ih (fun e he => ha e (by simp [he])) + rw [fractionValue_cons, List.length_cons, Nat.pow_succ] + have h1 : d * 10 ^ ds.length + 10 ^ ds.length ≤ 10 ^ ds.length * 10 := by + rw [Nat.mul_comm (10 ^ ds.length) 10, ← Nat.succ_mul] + exact Nat.mul_le_mul_right _ (by omega) + omega + +/-- A digit list scaled to `k` digits stays below `10 ^ k`. -/ +theorem scaled_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (k : Nat) (hk : a.length ≤ k) : + Spec.fractionValue a * 10 ^ (k - a.length) < 10 ^ k := by + have h := Nat.mul_lt_mul_of_pos_right (fractionValue_lt a ha) + ((Nat.pow_pos (n := k - a.length) (by decide : 0 < 10))) + rwa [← Nat.pow_add, Nat.add_sub_cancel' hk] at h + +/-- Scaling a list with a leading digit: the digit takes the top place. -/ +theorem scaled_cons (d : Nat) (ds : List Nat) (k : Nat) (hk : ds.length ≤ k) : + Spec.fractionValue (d :: ds) * 10 ^ (k + 1 - (d :: ds).length) = + d * 10 ^ k + Spec.fractionValue ds * 10 ^ (k - ds.length) := by + have e : k + 1 - (d :: ds).length = k - ds.length := by simp only [List.length_cons]; omega + rw [e, fractionValue_cons, Nat.add_mul, Nat.mul_assoc, ← Nat.pow_add, Nat.add_sub_cancel' hk] + +theorem compare_add_left (p x y : Nat) : compare (p + x) (p + y) = compare x y := by + rcases Nat.lt_trichotomy x y with h | h | h + · rw [Nat.compare_eq_lt.mpr h, Nat.compare_eq_lt.mpr (by omega)] + · subst h; rw [Nat.compare_eq_eq.mpr rfl, Nat.compare_eq_eq.mpr rfl] + · rw [Nat.compare_eq_gt.mpr h, Nat.compare_eq_gt.mpr (by omega)] + +/-- The general form: any common length `k` at least both lengths will do. -/ +theorem compareFraction_scaled (a b : List Nat) : + (∀ d ∈ a, d ≤ 9) → (∀ d ∈ b, d ≤ 9) → ∀ k, a.length ≤ k → b.length ≤ k → + compareFraction a b = + compare (Spec.fractionValue a * 10 ^ (k - a.length)) + (Spec.fractionValue b * 10 ^ (k - b.length)) := by + induction a, b using compareFraction.induct with + | case1 => + intro _ _ k _ _ + simp [compareFraction, fractionValue_nil] + | case2 as ih => + intro ha _ k hka _ + cases k with + | zero => simp at hka + | succ k => + have has : ∀ d ∈ as, d ≤ 9 := fun e he => ha e (by simp [he]) + have hk : as.length ≤ k := by simp at hka; omega + rw [compareFraction, ite_eq_left rfl, scaled_cons 0 as k hk, ih has (by simp) k hk (by simp)] + simp [fractionValue_nil] + | case3 a as h0 => + intro ha _ k hka _ + cases k with + | zero => simp at hka + | succ k => + have hk : as.length ≤ k := by simp at hka; omega + rw [compareFraction, ite_eq_right h0, scaled_cons a as k hk, fractionValue_nil, Nat.zero_mul] + symm + apply Nat.compare_eq_gt.mpr + have : 0 < a * 10 ^ k := Nat.mul_pos (by omega) (Nat.pow_pos (n := k) (by decide)) + omega + | case4 bs ih => + intro _ hb k _ hkb + cases k with + | zero => simp at hkb + | succ k => + have hbs : ∀ d ∈ bs, d ≤ 9 := fun e he => hb e (by simp [he]) + have hk : bs.length ≤ k := by simp at hkb; omega + rw [compareFraction, ite_eq_left rfl, scaled_cons 0 bs k hk, ih (by simp) hbs k (by simp) hk] + simp [fractionValue_nil] + | case5 b bs h0 => + intro _ hb k _ hkb + cases k with + | zero => simp at hkb + | succ k => + have hk : bs.length ≤ k := by simp at hkb; omega + rw [compareFraction, ite_eq_right h0, scaled_cons b bs k hk, fractionValue_nil, Nat.zero_mul] + symm + apply Nat.compare_eq_lt.mpr + have : 0 < b * 10 ^ k := Nat.mul_pos (by omega) (Nat.pow_pos (n := k) (by decide)) + omega + | case6 a as b bs hab => + intro ha hb k hka hkb + cases k with + | zero => simp at hka + | succ k => + have has : ∀ d ∈ as, d ≤ 9 := fun e he => ha e (by simp [he]) + have hka' : as.length ≤ k := by simp at hka; omega + have hkb' : bs.length ≤ k := by simp at hkb; omega + rw [compareFraction, ite_eq_left hab, scaled_cons a as k hka', scaled_cons b bs k hkb'] + symm + apply Nat.compare_eq_lt.mpr + have hx := scaled_lt as has k hka' + have hle : (a + 1) * 10 ^ k ≤ b * 10 ^ k := Nat.mul_le_mul_right _ hab + rw [Nat.succ_mul] at hle + omega + | case7 a as b bs _ hba => + intro ha hb k hka hkb + cases k with + | zero => simp at hka + | succ k => + have hbs : ∀ d ∈ bs, d ≤ 9 := fun e he => hb e (by simp [he]) + have hka' : as.length ≤ k := by simp at hka; omega + have hkb' : bs.length ≤ k := by simp at hkb; omega + rw [compareFraction, ite_eq_right (by omega), ite_eq_left hba, scaled_cons a as k hka', + scaled_cons b bs k hkb'] + symm + apply Nat.compare_eq_gt.mpr + have hy := scaled_lt bs hbs k hkb' + have hle : (b + 1) * 10 ^ k ≤ a * 10 ^ k := Nat.mul_le_mul_right _ hba + rw [Nat.succ_mul] at hle + omega + | case8 a as b bs h1 h2 ih => + intro ha hb k hka hkb + cases k with + | zero => simp at hka + | succ k => + have has : ∀ d ∈ as, d ≤ 9 := fun e he => ha e (by simp [he]) + have hbs : ∀ d ∈ bs, d ≤ 9 := fun e he => hb e (by simp [he]) + have hka' : as.length ≤ k := by simp at hka; omega + have hkb' : bs.length ≤ k := by simp at hkb; omega + have hab : a = b := by omega + subst hab + rw [compareFraction, ite_eq_right h1, ite_eq_right h2, scaled_cons a as k hka', + scaled_cons a bs k hkb', compare_add_left, ih has hbs k hka' hkb'] + +theorem compareFraction_eq (a b : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (hb : ∀ d ∈ b, d ≤ 9) : + compareFraction a b = + compare (Spec.fractionValue a * 10 ^ (max a.length b.length - a.length)) + (Spec.fractionValue b * 10 ^ (max a.length b.length - b.length)) := + compareFraction_scaled a b ha hb _ (Nat.le_max_left _ _) (Nat.le_max_right _ _) + +end Rfc3339.Proofs.Fraction diff --git a/Proofs/Instant.lean b/Proofs/Instant.lean new file mode 100644 index 0000000..a644e6f --- /dev/null +++ b/Proofs/Instant.lean @@ -0,0 +1,100 @@ +/- + The instant code in `Rfc3339/Instant.lean` agrees with the definitions + in `Spec/Defs.lean`: `unixSeconds` counts the same whole seconds as + `Spec.unixSeconds`, `utcMinute` is `Spec.utcMinute`, and + `compareInstant` orders two valid timestamps the same way as + `Spec.compareInstants`. +-/ + +import Rfc3339 +import Spec.Defs +import Proofs.DayNumber +import Proofs.Fraction + +namespace Rfc3339.Proofs.Instant + +open Rfc3339 + +/-- 1970-01-01 is day 719528. -/ +theorem dayNumber_epoch : Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel + +theorem utcMinute_eq (t : Timestamp) (h : Spec.Valid t) : + t.utcMinute = Spec.utcMinute t := by + obtain ⟨_, hm1, hm2, _⟩ := h + unfold Timestamp.utcMinute Spec.utcMinute + rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.offsetMinutes_eq] + +theorem unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : + t.unixSeconds = Spec.unixSeconds t := by + obtain ⟨_, hm1, hm2, _⟩ := h + unfold Timestamp.unixSeconds Spec.unixSeconds Spec.utcMinute + rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.offsetMinutes_eq, dayNumber_epoch] + omega + +/-- Comparing natural numbers gives the same answer as integers. -/ +theorem compare_natCast (m n : Nat) : compare (m : Int) (n : Int) = compare m n := by + rcases Nat.lt_trichotomy m n with h | h | h + · rw [Nat.compare_eq_lt.mpr h, Int.compare_eq_lt.mpr (by omega)] + · subst h; rw [Nat.compare_eq_eq.mpr rfl, Int.compare_eq_eq.mpr rfl] + · rw [Nat.compare_eq_gt.mpr h, Int.compare_eq_gt.mpr (by omega)] + +/-- Adding the same number to both sides leaves the comparison alone. -/ +theorem compare_add_left (p x y : Int) : compare (p + x) (p + y) = compare x y := by + rcases Int.lt_trichotomy x y with h | h | h + · rw [Int.compare_eq_lt.mpr h, Int.compare_eq_lt.mpr (by omega)] + · subst h; rw [Int.compare_eq_eq.mpr rfl, Int.compare_eq_eq.mpr rfl] + · rw [Int.compare_eq_gt.mpr h, Int.compare_eq_gt.mpr (by omega)] + +/-- `u * P + x` against `v * P + y`, with `x` and `y` from 0 to below + `P`: the whole parts `u` and `v` decide, unless they are equal, and + then `x` and `y` do. -/ +theorem compare_scaled (u v P x y : Int) (hx0 : 0 ≤ x) (hxP : x < P) (hy0 : 0 ≤ y) + (hyP : y < P) : + compare (u * P + x) (v * P + y) = + match compare u v with + | .eq => compare x y + | o => o := by + rcases Int.lt_trichotomy u v with h | h | h + · rw [Int.compare_eq_lt.mpr h] + apply Int.compare_eq_lt.mpr + have hle : (u + 1) * P ≤ v * P := Int.mul_le_mul_of_nonneg_right (by omega) (by omega) + rw [Int.add_mul, Int.one_mul] at hle + omega + · subst h + rw [Int.compare_eq_eq.mpr rfl, compare_add_left] + · rw [Int.compare_eq_gt.mpr h] + apply Int.compare_eq_gt.mpr + have hle : (v + 1) * P ≤ u * P := Int.mul_le_mul_of_nonneg_right (by omega) (by omega) + rw [Int.add_mul, Int.one_mul] at hle + omega + +theorem compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : + a.compareInstant b = Spec.compareInstants a b := by + have hfa : ∀ d ∈ a.fraction, d ≤ 9 := ha.2.2.2.2.2.2.2.2.2.1 + have hfb : ∀ d ∈ b.fraction, d ≤ 9 := hb.2.2.2.2.2.2.2.2.2.1 + have la := Fraction.scaled_lt a.fraction hfa (max a.fraction.length b.fraction.length) + (Nat.le_max_left _ _) + have lb := Fraction.scaled_lt b.fraction hfb (max a.fraction.length b.fraction.length) + (Nat.le_max_right _ _) + have ea : (Spec.fractionValue a.fraction : Int) * + 10 ^ (max a.fraction.length b.fraction.length - a.fraction.length) = + ((Spec.fractionValue a.fraction * + 10 ^ (max a.fraction.length b.fraction.length - a.fraction.length) : Nat) : Int) := by + push_cast; rfl + have eb : (Spec.fractionValue b.fraction : Int) * + 10 ^ (max a.fraction.length b.fraction.length - b.fraction.length) = + ((Spec.fractionValue b.fraction * + 10 ^ (max a.fraction.length b.fraction.length - b.fraction.length) : Nat) : Int) := by + push_cast; rfl + have eP : ((10 ^ max a.fraction.length b.fraction.length : Nat) : Int) = + (10 : Int) ^ max a.fraction.length b.fraction.length := by + push_cast; rfl + unfold Timestamp.compareInstant Spec.compareInstants Spec.instantKey + simp only + rw [utcMinute_eq a ha, utcMinute_eq b hb, Fraction.compareFraction_eq _ _ hfa hfb, ea, eb, + compare_scaled (Spec.utcMinute a * 61 + a.second) (Spec.utcMinute b * 61 + b.second) + ((10 : Int) ^ max a.fraction.length b.fraction.length) _ _ (by omega) + (by rw [← eP]; omega) (by omega) (by rw [← eP]; omega), compare_natCast] + cases compare (Spec.utcMinute a * 61 + a.second) (Spec.utcMinute b * 61 + b.second) <;> rfl + +end Rfc3339.Proofs.Instant diff --git a/Proofs/Main.lean b/Proofs/Main.lean new file mode 100644 index 0000000..0870fe6 --- /dev/null +++ b/Proofs/Main.lean @@ -0,0 +1,173 @@ +/- + The statements of `Spec.lean`, under the same names, from the lemmas + in the other files of `Proofs/`. The test vectors are checked by + evaluation. +-/ + +import Rfc3339 +import Spec.Defs +import Proofs.Valid +import Proofs.Format +import Proofs.Instant + +open Rfc3339 + +namespace Rfc3339.Proofs.Main + +/-- Every character `Spec.render` writes is below `a`, so upper case + leaves it alone. -/ +theorem upper_fixed (c : Char) (h : c.toNat < 97) : Spec.asciiUpper c = c := by + unfold Spec.asciiUpper + simp only [ite_eq_right_iff] + omega + +theorem digitChar_lt (n : Nat) : (Spec.digitChar n).toNat < 97 := by + unfold Spec.digitChar + rcases Nat.lt_or_ge n 10 with h | h + · have : ∀ i : Fin 10, ("0123456789".toList.getD i.val '?').toNat < 97 := by decide + exact this ⟨n, h⟩ + · obtain ⟨k, rfl⟩ : ∃ k, n = k + 10 := ⟨n - 10, by omega⟩ + simp [List.getD_eq_getElem?_getD] + +theorem digits_lt (k n : Nat) : ∀ c ∈ Spec.digits k n, c.toNat < 97 := by + intro c hc + simp only [Spec.digits, List.mem_map] at hc + obtain ⟨_, _, rfl⟩ := hc + exact digitChar_lt _ + +theorem renderOffset_lt (o : Offset) : ∀ c ∈ Spec.renderOffset o, c.toNat < 97 := by + cases o with + | z => decide + | plus h m | minus h m => + simp only [Spec.renderOffset, List.forall_mem_append, List.forall_mem_cons] + exact ⟨⟨⟨⟨by decide, by simp⟩, digits_lt _ _⟩, ⟨by decide, by simp⟩⟩, digits_lt _ _⟩ + +theorem render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 97 := by + simp only [Spec.render, List.forall_mem_append, List.forall_mem_cons] + and_intros + all_goals first + | exact digits_lt _ _ + | exact renderOffset_lt _ + | decide + | (intro _ h; cases h) + | skip + split + · simp + · simp only [List.forall_mem_append, List.forall_mem_cons, + List.forall_mem_map] + exact ⟨⟨by decide, by simp⟩, fun _ _ => digitChar_lt _⟩ + +theorem upper_render (t : Timestamp) : (Spec.render t).map Spec.asciiUpper = Spec.render t := by + conv => rhs; rw [← List.map_id (Spec.render t)] + exact List.map_congr_left fun c hc => upper_fixed c (render_lt t c hc) + +end Rfc3339.Proofs.Main + +open Rfc3339.Proofs + +theorem Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := + Valid.isValid_iff t + +theorem Spec.print_eq (t : Timestamp) (h : Spec.Valid t) : + t.print.toList = Spec.render t := by + rw [Format.print_toList, Format.render_eq t ((Spec.isValid_iff t).mpr h)] + +theorem Spec.parse_iff (s : String) (t : Timestamp) : + parse s = some t ↔ Spec.Valid t ∧ s.toList.map Spec.asciiUpper = Spec.render t := by + rw [Format.parse_iff', Spec.isValid_iff] + +theorem Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : + Spec.Valid t := + ((Spec.parse_iff s t).mp h).1 + +theorem Spec.parse_print (t : Timestamp) (h : Spec.Valid t) : parse t.print = some t := by + rw [Spec.parse_iff, Spec.print_eq t h] + exact ⟨h, Main.upper_render t⟩ + +theorem Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : + t.print.toList = s.toList.map Spec.asciiUpper := by + obtain ⟨hv, hs⟩ := (Spec.parse_iff s t).mp h + rw [Spec.print_eq t hv, hs] + +theorem Spec.unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : + t.unixSeconds = Spec.unixSeconds t := + Instant.unixSeconds_eq t h + +theorem Spec.compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : + a.compareInstant b = Spec.compareInstants a b := + Instant.compareInstant_eq a b ha hb + +theorem Spec.rfc3339_examples : + parse "1985-04-12T23:20:50.52Z" = some ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ ∧ + parse "1996-12-19T16:39:57-08:00" = some ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ∧ + parse "1990-12-31T23:59:60Z" = some ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ ∧ + parse "1990-12-31T15:59:60-08:00" = some ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ ∧ + parse "1937-01-01T12:00:27.87+00:20" = + some ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ := by + decide + +theorem Spec.rfc3339_example_instants : + (Timestamp.compareInstant ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ + ⟨1996, 12, 20, 0, 39, 57, [], .z⟩ = .eq) ∧ + (Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ + ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = .eq) ∧ + Timestamp.unixSeconds ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = 482196050 := by + -- `compareFraction` is defined by well-founded recursion, which `decide` + -- does not unfold, so the orders go through `Spec.compareInstant_eq`. + refine ⟨?_, ?_, by decide⟩ + all_goals + rw [Spec.compareInstant_eq _ _ ((Spec.isValid_iff _).mp (by decide)) + ((Spec.isValid_iff _).mp (by decide))] + decide +kernel + +theorem Spec.leap_second_order : + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 59, [9], .z⟩ + ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = .lt ∧ + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [5], .z⟩ + ⟨1991, 1, 1, 0, 0, 0, [2], .z⟩ = .lt ∧ + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ + ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ = .lt ∧ + Timestamp.unixSeconds ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = + Timestamp.unixSeconds ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ := by + refine ⟨?_, ?_, ?_, by decide⟩ + all_goals + rw [Spec.compareInstant_eq _ _ ((Spec.isValid_iff _).mp (by decide)) + ((Spec.isValid_iff _).mp (by decide))] + decide +kernel + +theorem Spec.calendar_vectors : + (parse "2000-02-29T00:00:00Z").isSome ∧ + (parse "2004-02-29T00:00:00Z").isSome ∧ + parse "1900-02-29T00:00:00Z" = none ∧ + parse "2001-02-29T00:00:00Z" = none ∧ + parse "2000-02-30T00:00:00Z" = none ∧ + parse "2001-04-31T00:00:00Z" = none ∧ + parse "2001-01-32T00:00:00Z" = none ∧ + parse "2001-01-00T00:00:00Z" = none ∧ + parse "2001-00-01T00:00:00Z" = none ∧ + parse "2001-13-01T00:00:00Z" = none := by + decide + +theorem Spec.leap_second_vectors : + (parse "1990-06-30T23:59:60Z").isSome ∧ + (parse "1991-01-01T00:59:60+01:00").isSome ∧ + parse "1990-12-31T23:59:61Z" = none ∧ + parse "1990-12-31T23:58:60Z" = none ∧ + parse "1990-12-30T23:59:60Z" = none ∧ + parse "1990-12-31T23:59:60+01:00" = none := by + decide + +theorem Spec.syntax_vectors : + parse "1985-04-12t23:20:50.52z" = parse "1985-04-12T23:20:50.52Z" ∧ + parse "1985-04-12 23:20:50.52Z" = none ∧ + parse "1985-04-12T23:20:50.Z" = none ∧ + parse "1985-04-12T23:20:50,52Z" = none ∧ + parse "1985-04-12T23:20Z" = none ∧ + parse "85-04-12T23:20:50Z" = none ∧ + parse "1985-04-12T23:20:50+24:00" = none ∧ + parse "1985-04-12T23:20:50+23:60" = none ∧ + parse "1985-04-12T23:20:50+0100" = none ∧ + parse "1985-04-12T23:20:50" = none ∧ + parse "1985-04-12T23:20:50Z " = none ∧ + parse "1985-04-12T24:00:00Z" = none := by + decide diff --git a/Proofs/Valid.lean b/Proofs/Valid.lean new file mode 100644 index 0000000..6bbba4a --- /dev/null +++ b/Proofs/Valid.lean @@ -0,0 +1,192 @@ +/- + `Timestamp.isValid` decides exactly `Spec.Valid`. The hard part is + the leap second rule: the code's check on the local date and time + agrees with the spec's rule that the UTC minute is the last one + before a month begins. +-/ + +import Rfc3339 +import Spec.Defs + +namespace Rfc3339.Proofs.Valid + +open Rfc3339 + +/-! ## Small facts: the code's helpers agree with the spec's -/ + +theorem isLeapYear_eq (y : Nat) : isLeapYear y = Spec.isLeapYear y := by + unfold isLeapYear Spec.isLeapYear + by_cases h4 : y % 4 = 0 <;> by_cases h100 : y % 100 = 0 <;> by_cases h400 : y % 400 = 0 <;> + simp [h4, h100, h400] + +theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := by + unfold daysInMonth Spec.daysInMonth + split <;> simp_all [isLeapYear_eq] <;> omega + +theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Spec.offsetMinutes o := by + cases o <;> simp [offsetMinutes, Spec.offsetMinutes] + +theorem offset_isValid_iff (o : Offset) : o.isValid = true ↔ Spec.OffsetValid o := by + cases o <;> simp [Offset.isValid, Spec.OffsetValid] + +theorem all_lt_iff (l : List Nat) : l.all (· < 10) = true ↔ ∀ d ∈ l, d ≤ 9 := by + simp only [List.all_eq_true, decide_eq_true_eq] + constructor + · intro h d hd; have := h d hd; omega + · intro h d hd; have := h d hd; omega + +/-! ## Sums over ranges -/ + +theorem sum_range_succ (g : Nat → Nat) (k : Nat) : + ((List.range (k + 1)).map g).sum = ((List.range k).map g).sum + g k := by + simp [List.range_succ, List.sum_append] + +theorem sum_range_mono (g : Nat → Nat) (a b : Nat) (h : a ≤ b) : + ((List.range a).map g).sum ≤ ((List.range b).map g).sum := by + obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le h + induction j with + | zero => simp + | succ j ih => + rw [← Nat.add_assoc, sum_range_succ] + have := ih (Nat.le_add_right _ _) + omega + +/-! ## Day numbers -/ + +/-- Days in the years before `y`. -/ +def yearsBefore (y : Nat) : Nat := ((List.range y).map Spec.yearLength).sum + +/-- Days in the months before `m` of year `y`. -/ +def monthsBefore (y m : Nat) : Nat := + ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum + +theorem dayNumber_eq (y m d : Nat) : + Spec.dayNumber y m d = yearsBefore y + monthsBefore y m + (d - 1) := rfl + +theorem dayNumber_day (y m d : Nat) : + Spec.dayNumber y m d = Spec.dayNumber y m 1 + (d - 1) := by + simp only [dayNumber_eq]; omega + +theorem yearsBefore_succ (y : Nat) : yearsBefore (y + 1) = yearsBefore y + Spec.yearLength y := by + unfold yearsBefore; rw [sum_range_succ] + +theorem yearsBefore_mono {y y' : Nat} (h : y < y') : + yearsBefore y + Spec.yearLength y ≤ yearsBefore y' := by + rw [← yearsBefore_succ]; exact sum_range_mono _ _ _ h + +theorem monthsBefore_succ (y m : Nat) (hm : 1 ≤ m) : + monthsBefore y (m + 1) = monthsBefore y m + Spec.daysInMonth y m := by + unfold monthsBefore + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hm + simp only [Nat.add_sub_cancel, Nat.add_comm 1 k] + rw [sum_range_succ] + +theorem monthsBefore_mono (y : Nat) {m m' : Nat} (h : m ≤ m') : + monthsBefore y m ≤ monthsBefore y m' := + sum_range_mono _ _ _ (by omega) + +theorem monthsBefore_twelve (y : Nat) : monthsBefore y 12 + 31 = Spec.yearLength y := by + cases h : Spec.isLeapYear y <;> + simp [monthsBefore, List.range_succ, Spec.daysInMonth, Spec.yearLength, h] + +theorem daysInMonth_bounds (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : + 28 ≤ Spec.daysInMonth y m ∧ Spec.daysInMonth y m ≤ 31 := by + unfold Spec.daysInMonth + split + · split <;> omega + · split + · omega + · split <;> omega + +/-- A month ends within its year. -/ +theorem month_end_le (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : + monthsBefore y m + Spec.daysInMonth y m ≤ Spec.yearLength y := by + rw [← monthsBefore_succ y m h1, ← monthsBefore_twelve] + have := monthsBefore_mono y (show m + 1 ≤ 13 by omega) + rw [show 13 = 12 + 1 from rfl, monthsBefore_succ y 12 (by decide)] at this + have h12 : Spec.daysInMonth y 12 = 31 := by simp [Spec.daysInMonth] + omega + +/-- The day after the last day of month `m` is the first of month `m + 1` + (for `m < 12`, the next month). -/ +theorem next_month (y m : Nat) (h1 : 1 ≤ m) : + Spec.dayNumber y m 1 + Spec.daysInMonth y m = Spec.dayNumber y (m + 1) 1 := by + simp only [dayNumber_eq, monthsBefore_succ y m h1]; omega + +theorem next_year (y : Nat) : + Spec.dayNumber y 12 1 + 31 = Spec.dayNumber (y + 1) 1 1 := by + simp only [dayNumber_eq, yearsBefore_succ, ← monthsBefore_twelve y] + simp [monthsBefore]; omega + +/-- No month starts strictly inside another month. -/ +theorem month_start_spaced {y m y' m' : Nat} (h1 : 1 ≤ m) (h2 : m ≤ 12) (h1' : 1 ≤ m') + (h2' : m' ≤ 12) (hlt : Spec.dayNumber y m 1 < Spec.dayNumber y' m' 1) : + Spec.dayNumber y m 1 + Spec.daysInMonth y m ≤ Spec.dayNumber y' m' 1 := by + simp only [dayNumber_eq] at * + rcases Nat.lt_trichotomy y y' with hy | rfl | hy + · have := yearsBefore_mono hy + have := month_end_le y m h1 h2 + omega + · rcases Nat.lt_or_ge m m' with hm | hm + · have := monthsBefore_mono y (show m + 1 ≤ m' from hm) + rw [monthsBefore_succ y m h1] at this + omega + · have := monthsBefore_mono y hm + omega + · have := yearsBefore_mono hy + have := month_end_le y' m' h1' h2' + have := daysInMonth_bounds y' m' h1' h2' + omega + +/-! ## The leap second rule -/ + +/-- With the other fields in range, the code's leap second check is the + spec's rule: the UTC minute is the last one before a month begins. -/ +theorem leapSecondOK_iff (t : Timestamp) (hm1 : 1 ≤ t.month) (hm2 : t.month ≤ 12) + (hd1 : 1 ≤ t.day) (hd2 : t.day ≤ Spec.daysInMonth t.year t.month) + (hh : t.hour ≤ 23) (hmi : t.minute ≤ 59) (ho : Spec.OffsetValid t.offset) : + leapSecondOK t = true ↔ Spec.LeapSecondAllowed t := by + obtain ⟨y, m, d, h, mi, s, f, o⟩ := t + simp only at * + have hob : -1439 ≤ Spec.offsetMinutes o ∧ Spec.offsetMinutes o ≤ 1439 := by + cases o <;> simp [Spec.offsetMinutes, Spec.OffsetValid] at ho ⊢ <;> omega + simp only [leapSecondOK, Spec.LeapSecondAllowed, Spec.utcMinute, Bool.or_eq_true, + Bool.and_eq_true, beq_iff_eq, daysInMonth_eq, offsetMinutes_eq] + have hN := dayNumber_day y m d + have hdim := daysInMonth_bounds y m hm1 hm2 + constructor + · rintro (⟨hu, rfl⟩ | ⟨hu, rfl⟩) + · rcases Nat.lt_or_ge m 12 with hm | hm + · refine ⟨y, m + 1, by omega, by omega, ?_⟩ + have := next_month y m hm1 + omega + · have hm12 : m = 12 := by omega + subst hm12 + refine ⟨y + 1, 1, by omega, by omega, ?_⟩ + have := next_year y + have : Spec.daysInMonth y 12 = 31 := by simp [Spec.daysInMonth] + omega + · exact ⟨y, m, hm1, hm2, by omega⟩ + · rintro ⟨y', m', h1', h2', heq⟩ + have hsp := @month_start_spaced y m y' m' hm1 hm2 h1' h2' + omega + +/-! ## Validity -/ + +theorem isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := by + simp only [Timestamp.isValid, Spec.Valid, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq, + bne_iff_ne, ne_eq, daysInMonth_eq, all_lt_iff, offset_isValid_iff] + constructor + · rintro ⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨hy, hm1⟩, hm2⟩, hd1⟩, hd2⟩, hh⟩, hmi⟩, hs⟩, hleap⟩, hf⟩, ho⟩ + refine ⟨hy, hm1, hm2, hd1, hd2, hh, hmi, hs, ?_, hf, ho⟩ + intro h60 + rcases hleap with h | h + · exact absurd h60 h + · exact (leapSecondOK_iff t hm1 hm2 hd1 hd2 hh hmi ho).1 h + · rintro ⟨hy, hm1, hm2, hd1, hd2, hh, hmi, hs, hleap, hf, ho⟩ + refine ⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨hy, hm1⟩, hm2⟩, hd1⟩, hd2⟩, hh⟩, hmi⟩, hs⟩, ?_⟩, hf⟩, ho⟩ + by_cases h60 : t.second = 60 + · exact Or.inr ((leapSecondOK_iff t hm1 hm2 hd1 hd2 hh hmi ho).2 (hleap h60)) + · exact Or.inl h60 + +end Rfc3339.Proofs.Valid diff --git a/README.md b/README.md index 21949ff..d3ace0d 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,108 @@ -# rfc -lean RFC 3339 timestamp parser +# 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. + +It is a project of [Proven Commons](https://github.com/Proven-Commons/mission), built to the verified bar published there. + +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. + +## Use it + +``` +lake build +.lake/build/bin/rfc3339 check 1985-04-12T23:20:50.52Z 2001-02-29T00:00:00Z +``` + +For each timestamp it prints the timestamp as written, with `T` and `Z` in upper case, and its Unix seconds. A timestamp the RFC does not allow prints `invalid`, and the tool then exits with 1. From Lean, the functions are these: + +- `Rfc3339.parse` +- `Timestamp.print` +- `Timestamp.isValid` +- `Timestamp.unixSeconds` +- `Timestamp.compareInstant` + +`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/`. + +| 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` | +| 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` | +| Printing then parsing gives the timestamp back. | `Spec.parse_print` | +| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Spec.print_parse` | +| `unixSeconds` counts the whole seconds from 1970-01-01T00:00:00Z, with the offset applied. Its fast day arithmetic equals a day count that adds up month and year lengths. | `Spec.unixSeconds_eq` | +| `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction, compared exactly. | `Spec.compareInstant_eq` | +| The examples of section 5.8 parse to the fields the RFC gives. What the RFC says about them holds: `1996-12-19T16:39:57-08:00` is the instant `1996-12-20T00:39:57Z`, and `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. Separately, `1985-04-12T23:20:50.52Z` is 482196050 seconds after the epoch, as Python's `calendar.timegm` also gives. | `Spec.rfc3339_examples`, `Spec.rfc3339_example_instants` | +| A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` | +| The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` | + +The command-line tool in `Main.lean` calls these functions directly. + +## What is not proved + +- Reading requests and printing answers in `Main.lean`: the hex decoding and UTF-8 check in `serve` mode, the arguments, output and exit codes of `check` mode, and the decimal printing of numbers. The differential tests cover them, with malformed requests and CR LF line endings. +- Whether a leap second was announced. Second 60 is accepted at 23:59 UTC at the end of any month, without a table of leap seconds, where section 5.7 allows it only at the end of months in which a leap second occurs. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. +- Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. +- Forms outside RFC 3339 are not supported, by design: + - a space in place of `T`, which section 5.6 lets applications choose; + - other ISO 8601 forms; + - named time zones; + - years outside 0000 to 9999. +- Speed. The code works on lists of characters, which suits proofs, not bulk data. + +## What you must trust + +- The Lean kernel and the five external kernels shipped with Lean, which all check the proofs. +- `lake comparator`, which builds the statements and the proofs in a sandbox, exports them, and checks that each proof proves exactly its statement. +- bubblewrap and the Linux kernel's namespaces, which keep the untrusted build from tampering with that check. +- 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. + +This project has no dependencies beyond Lean itself. + +## Other parsers + +`tests/CROSS-CHECK.md` records a one-off comparison with Go's `time.Parse` and with `rfc3339-validator`. That package is the one the Python `jsonschema` package calls for its `date-time` check, after upper-casing the string. The comparison is not part of the verified bar. The differences it found: + +- Both reject lower case `t` and `z`, which section 5.6 allows, and second 60. jsonschema upper-cases the string first, so it does accept lower case. +- `rfc3339-validator` rejects year 0000; Go accepts it. +- Go accepts offsets such as `+24:00` and `+23:60`. +- Go accepts fields with one digit, such as `T0:44:28`. +- Go accepts a comma before the fraction. +- `rfc3339-validator` accepts a timestamp followed by a line break. + +## Re-check it + +Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), and Python 3.11 or later. + +``` +lake build +lake comparator --paranoid +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`. + +## Layout + +- `Rfc3339/Types.lean`: the timestamp and offset types. It is part of the specification. +- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`: the code under proof. +- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. +- `Spec/Defs.lean`: the definitions the statements use, written from the RFC, with checks against its tables and known day counts. +- `Proofs.lean` and `Proofs/`: the proofs, under the same names. +- `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. +- `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows. +- `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. diff --git a/Rfc3339.lean b/Rfc3339.lean new file mode 100644 index 0000000..4945aaa --- /dev/null +++ b/Rfc3339.lean @@ -0,0 +1,9 @@ +/- + RFC 3339 timestamps: parse, print, validity, and the instant they + name. +-/ + +import Rfc3339.Types +import Rfc3339.Calendar +import Rfc3339.Format +import Rfc3339.Instant diff --git a/Rfc3339/Calendar.lean b/Rfc3339/Calendar.lean new file mode 100644 index 0000000..efceb30 --- /dev/null +++ b/Rfc3339/Calendar.lean @@ -0,0 +1,52 @@ +/- + The calendar rules of RFC 3339, section 5.7, and the checks that + decide which timestamps are valid. +-/ + +import Rfc3339.Types + +namespace Rfc3339 + +/-- Leap years of the Gregorian calendar, as in RFC 3339, Appendix C. -/ +def isLeapYear (y : Nat) : Bool := + y % 4 == 0 && (y % 100 != 0 || y % 400 == 0) + +/-- The number of days in month `m` (1 to 12) of year `y`, and 0 for any + other `m`. -/ +def daysInMonth (y m : Nat) : Nat := + match m with + | 1 => 31 | 2 => if isLeapYear y then 29 else 28 | 3 => 31 | 4 => 30 + | 5 => 31 | 6 => 30 | 7 => 31 | 8 => 31 | 9 => 30 | 10 => 31 | 11 => 30 + | 12 => 31 | _ => 0 + +/-- The offset in minutes east of UTC. -/ +def offsetMinutes : Offset → Int + | .z => 0 + | .plus h m => (h * 60 + m : Nat) + | .minus h m => -((h * 60 + m : Nat) : Int) + +def Offset.isValid : Offset → Bool + | .z => true + | .plus h m => h ≤ 23 && m ≤ 59 + | .minus h m => h ≤ 23 && m ≤ 59 + +/-- Second 60 is a leap second, which section 5.7 puts 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. Since an offset is less than a day, that is + either the same day as the local date, at its end, or the day + before, when the local date is the first of a month. -/ +def leapSecondOK (t : Timestamp) : Bool := + let u : Int := ((t.hour * 60 + t.minute : Nat) : Int) - offsetMinutes t.offset + (u == 1439 && t.day == daysInMonth t.year t.month) || (u == -1 && t.day == 1) + +/-- Whether `t` is a timestamp RFC 3339 allows: each field in its range + (section 5.6), the day within its month, and second 60 only for a + leap second (section 5.7). -/ +def Timestamp.isValid (t : Timestamp) : Bool := + t.year ≤ 9999 && 1 ≤ t.month && t.month ≤ 12 && + 1 ≤ t.day && t.day ≤ daysInMonth t.year t.month && + t.hour ≤ 23 && t.minute ≤ 59 && t.second ≤ 60 && + (t.second != 60 || leapSecondOK t) && + t.fraction.all (· < 10) && t.offset.isValid + +end Rfc3339 diff --git a/Rfc3339/Format.lean b/Rfc3339/Format.lean new file mode 100644 index 0000000..3a0e63b --- /dev/null +++ b/Rfc3339/Format.lean @@ -0,0 +1,115 @@ +/- + Reading and writing the `date-time` format of RFC 3339, section 5.6. +-/ + +import Rfc3339.Calendar + +namespace Rfc3339 + +/-! ## Printing -/ + +/-- The ASCII digit for `n`, for `n` from 0 to 9. -/ +def digitChar (n : Nat) : Char := Char.ofNat (n + 48) + +/-- `n` in two digits, for `n` below 100. -/ +def pad2 (n : Nat) : List Char := + [digitChar (n / 10 % 10), digitChar (n % 10)] + +/-- `n` in four digits, for `n` below 10000. -/ +def pad4 (n : Nat) : List Char := + [digitChar (n / 1000 % 10), digitChar (n / 100 % 10), digitChar (n / 10 % 10), + digitChar (n % 10)] + +def Offset.render : Offset → List Char + | .z => ['Z'] + | .plus h m => '+' :: pad2 h ++ ':' :: pad2 m + | .minus h m => '-' :: pad2 h ++ ':' :: pad2 m + +def renderFraction : List Nat → List Char + | [] => [] + | ds => '.' :: ds.map digitChar + +def Timestamp.render (t : Timestamp) : List Char := + pad4 t.year ++ '-' :: pad2 t.month ++ '-' :: pad2 t.day ++ 'T' :: + pad2 t.hour ++ ':' :: pad2 t.minute ++ ':' :: pad2 t.second ++ + renderFraction t.fraction ++ t.offset.render + +/-- The timestamp in RFC 3339 form, with `T` and `Z` in upper case and + the fraction digit for digit. -/ +def Timestamp.print (t : Timestamp) : String := + String.ofList t.render + +/-! ## Parsing -/ + +/-- The value of an ASCII digit. -/ +def digitValue (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - 48) else none + +/-- ASCII upper case: `a` to `z` become `A` to `Z`, nothing else + changes. -/ +def asciiUpper (c : Char) : Char := + if 'a' ≤ c ∧ c ≤ 'z' then Char.ofNat (c.toNat - 32) else c + +def two (a b : Char) : Option Nat := do + let x ← digitValue a + let y ← digitValue b + pure (10 * x + y) + +def four (a b c d : Char) : Option Nat := do + let w ← digitValue a + let x ← digitValue b + let y ← digitValue c + let z ← digitValue d + pure (1000 * w + 100 * x + 10 * y + z) + +/-- The digits at the front of the list, and what follows them. -/ +def takeDigits : List Char → List Nat × List Char + | [] => ([], []) + | c :: cs => + match digitValue c with + | some v => let r := takeDigits cs; (v :: r.1, r.2) + | none => ([], c :: cs) + +/-- `time-secfrac`, if present: a point and one or more digits. -/ +def parseFraction : List Char → Option (List Nat × List Char) + | '.' :: cs => + let r := takeDigits cs + if r.1.isEmpty then none else some r + | cs => some ([], cs) + +/-- `time-offset`, which must end the input. -/ +def parseOffset : List Char → Option Offset + | ['Z'] => some .z + | ['+', h1, h2, ':', m1, m2] => do + let h ← two h1 h2 + let m ← two m1 m2 + pure (.plus h m) + | ['-', h1, h2, ':', m1, m2] => do + let h ← two h1 h2 + let m ← two m1 m2 + pure (.minus h m) + | _ => none + +/-- `date-time`, with `T` and `Z` in upper case. -/ +def parseUpper : List Char → Option Timestamp + | y1 :: y2 :: y3 :: y4 :: '-' :: m1 :: m2 :: '-' :: d1 :: d2 :: 'T' :: + h1 :: h2 :: ':' :: n1 :: n2 :: ':' :: s1 :: s2 :: rest => do + let year ← four y1 y2 y3 y4 + let month ← two m1 m2 + let day ← two d1 d2 + let hour ← two h1 h2 + let minute ← two n1 n2 + let second ← two s1 s2 + let r ← parseFraction rest + let offset ← parseOffset r.2 + let t : Timestamp := { year, month, day, hour, minute, second, fraction := r.1, offset } + if t.isValid then some t else none + | _ => none + +/-- Reads an RFC 3339 `date-time`. `T` and `Z` may be in either case, as + the note in section 5.6 allows; nothing else is accepted, and the + whole string must be the timestamp. -/ +def parse (s : String) : Option Timestamp := + parseUpper (s.toList.map asciiUpper) + +end Rfc3339 diff --git a/Rfc3339/Instant.lean b/Rfc3339/Instant.lean new file mode 100644 index 0000000..484a550 --- /dev/null +++ b/Rfc3339/Instant.lean @@ -0,0 +1,61 @@ +/- + The instant a timestamp names: whole seconds since the Unix epoch, + and an order on instants that counts the fraction. +-/ + +import Rfc3339.Calendar + +namespace Rfc3339 + +/-- Days from 0000-01-01 to the first day of year `y`, in the proleptic + Gregorian calendar: 365 a year, and one more for each year below `y` + that is a multiple of 4, less those that are multiples of 100, plus + those that are multiples of 400. -/ +def daysBeforeYear (y : Nat) : Nat := + 365 * y + (y + 3) / 4 - (y + 99) / 100 + (y + 399) / 400 + +/-- Days from the first of the year to the first of month `m`, for `m` + from 1 to 12. -/ +def daysBeforeMonth (y m : Nat) : Nat := + let base := match m with + | 1 => 0 | 2 => 31 | 3 => 59 | 4 => 90 | 5 => 120 | 6 => 151 + | 7 => 181 | 8 => 212 | 9 => 243 | 10 => 273 | 11 => 304 | _ => 334 + if 2 < m && isLeapYear y then base + 1 else base + +/-- Days from 0000-01-01 to the date. -/ +def dayNumber (y m d : Nat) : Nat := + daysBeforeYear y + daysBeforeMonth y m + (d - 1) + +/-- Seconds from 1970-01-01T00:00:00Z to the timestamp, leaving out the + fraction. 719528 is `dayNumber 1970 1 1`. A leap second counts as + the first second of the next minute, as in POSIX time, so + `23:59:60Z` gives the same number as the midnight after it. -/ +def Timestamp.unixSeconds (t : Timestamp) : Int := + ((dayNumber t.year t.month t.day : Nat) - 719528 : Int) * 86400 + + ((t.hour * 3600 + t.minute * 60 + t.second : Nat) : Int) - offsetMinutes t.offset * 60 + +/-- Compares two digit strings as fractions: a missing digit counts as + 0. -/ +def compareFraction : List Nat → List Nat → Ordering + | [], [] => .eq + | a :: as, [] => if a = 0 then compareFraction as [] else .gt + | [], b :: bs => if b = 0 then compareFraction [] bs else .lt + | a :: as, b :: bs => + if a < b then .lt else if b < a then .gt else compareFraction as bs + +/-- The minute the timestamp falls in, counted in UTC from + 0000-01-01T00:00Z: local time less the offset. -/ +def Timestamp.utcMinute (t : Timestamp) : Int := + ((dayNumber t.year t.month t.day * 1440 + t.hour * 60 + t.minute : Nat) : Int) - + offsetMinutes t.offset + +/-- Orders two timestamps by the instants they name, whatever their + offsets: by UTC minute, then by the second within it, where a leap + second, 60, comes after 59, then by the fraction. A minute has at + most 61 seconds, so `utcMinute * 61 + second` keeps that order. -/ +def Timestamp.compareInstant (a b : Timestamp) : Ordering := + match compare (a.utcMinute * 61 + a.second) (b.utcMinute * 61 + b.second) with + | .eq => compareFraction a.fraction b.fraction + | o => o + +end Rfc3339 diff --git a/Rfc3339/Types.lean b/Rfc3339/Types.lean new file mode 100644 index 0000000..42c6c8f --- /dev/null +++ b/Rfc3339/Types.lean @@ -0,0 +1,40 @@ +/- + What a timestamp is: the values the parser produces and the printer + takes. Part of the approved specification, with `Spec.lean` and + `Spec/Defs.lean`, since every statement is about these types. + + A value holds each field of an RFC 3339 `date-time` as a number, + exactly as written. Which values are valid is `Spec.Valid`, in + `Spec/Defs.lean`. +-/ + +namespace Rfc3339 + +/-- The `time-offset` of RFC 3339, section 5.6. `-00:00` is kept apart + from `+00:00` and `Z`: section 4.3 gives it its own meaning, an + unknown local offset. -/ +inductive Offset where + /-- `Z`: UTC. -/ + | z + /-- `+hh:mm`: local time is ahead of UTC by this much. -/ + | plus (hour minute : Nat) + /-- `-hh:mm`: local time is behind UTC by this much. -/ + | minus (hour minute : Nat) + deriving DecidableEq, Repr + +/-- An RFC 3339 `date-time`: the date and time as written, in the local + time of its offset. -/ +structure Timestamp where + year : Nat + month : Nat + day : Nat + hour : Nat + minute : Nat + second : Nat + /-- The digits after the decimal point, most significant first, each + 0 to 9. Empty when the string has no fraction. -/ + fraction : List Nat + offset : Offset + deriving DecidableEq, Repr + +end Rfc3339 diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..fde8296 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,93 @@ +# Specification: rfc + +This library reads and writes RFC 3339 timestamps, such as `1985-04-12T23:20:50.52Z`. It also gives the instant a timestamp names, as whole seconds since 1970-01-01T00:00:00Z, and puts two timestamps in order by instant. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `Rfc3339/Types.lean`, and the other files `bar.toml` lists. + +## The format + +The scope is the `date-time` rule of RFC 3339, section 5.6, with the restrictions of section 5.7: + +``` +date-time = full-date "T" full-time +full-date = date-fullyear "-" date-month "-" date-mday +full-time = partial-time time-offset +partial-time = time-hour ":" time-minute ":" time-second [time-secfrac] +time-secfrac = "." 1*DIGIT +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. +- 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. +- The parser reads nothing else. That includes: + - a space in place of `T`, which section 5.6 lets applications choose; + - a comma before the fraction; + - offsets without a colon; + - a date or time on its own; + - any other ISO 8601 form; + - spaces or a line break before or after the timestamp. + +## The value + +`parse` returns a `Timestamp`: the year, month, day, hour, minute and second as numbers, the fraction as a list of digits, and the offset (`Z`, plus, or minus, with hours and minutes). The fields are those of the string as written, in its local time. `Spec.Valid` says which values the rules above allow. `Timestamp.isValid` decides it for a value built some other way. + +`Timestamp.print` writes a valid timestamp in the form above, with `T` and `Z` in upper case. + +## Instants + +`Timestamp.unixSeconds` gives the whole seconds from 1970-01-01T00:00:00Z to the instant a valid timestamp names, with the offset subtracted, ignoring the fraction. Dates before 1970 give negative numbers. Days are counted in the Gregorian calendar extended back to year 0, which RFC 3339 uses. + +POSIX time has no number for a leap second. As in POSIX time, second 60 is counted as 60 seconds into its minute, so `1990-12-31T23:59:60Z` and `1991-01-01T00:00:00Z` give the same number. + +`Timestamp.compareInstant` orders two valid timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second, 60, comes after 59, then by the fraction, compared exactly. It does not use Unix seconds, so `1990-12-31T23:59:60Z` comes before `1991-01-01T00:00:00Z`. It gives `eq` when the instants are equal, as for `2000-01-01T00:00:00.5Z` and `2000-01-01T01:00:00.500+01:00`. + +## Errors + +`parse` returns `none` for any string it does not accept. No function can fail any other way. + +## The command-line tool + +The command-line tool in `Main.lean` has two modes: + +- `rfc3339 check TIMESTAMP...` prints each timestamp's printed form and its Unix seconds, or `invalid`. It exits with 1 when any timestamp is invalid. +- `rfc3339 serve` answers requests from the differential tests, one per line. Each string is sent as the hex digits of its UTF-8 bytes. The header comment of `Main.lean` gives the protocol. + +Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds` and `Timestamp.compareInstant`. + +## 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. + +| Property | Theorem | +|----------|---------| +| `isValid` decides exactly `Spec.Valid`: the rules of sections 5.6 and 5.7, with second 60 allowed at the end of every month. | `Spec.isValid_iff` | +| A valid timestamp prints as the grammar writes it. | `Spec.print_eq` | +| `parse` returns `t` exactly when `t` is valid and the string is how `t` prints, with `T` and `Z` in either case. | `Spec.parse_iff` | +| What `parse` returns is valid: the day exists in its month, a leap second ends a month in UTC, and so on. | `Spec.parse_valid` | +| Printing then parsing gives the timestamp back. | `Spec.parse_print` | +| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Spec.print_parse` | +| `unixSeconds` counts the seconds from the epoch by the calendar, with the offset applied. | `Spec.unixSeconds_eq` | +| `compareInstant` orders timestamps by the instants they name: UTC minute, then second, then fraction. | `Spec.compareInstant_eq` | +| The examples of section 5.8 parse to the fields the RFC reads them as. | `Spec.rfc3339_examples` | +| What section 5.8 says about those examples holds: two pairs name the same instant. Separately, the first is 482196050 seconds after the epoch, as Python's `calendar.timegm` gives. | `Spec.rfc3339_example_instants` | +| A leap second comes after second 59 and before the next minute; its Unix seconds equal those of the next second. | `Spec.leap_second_order` | +| Days outside their month are rejected, with the leap year rule of Appendix C. | `Spec.calendar_vectors` | +| Second 60 is accepted only at the end of a month in UTC. | `Spec.leap_second_vectors` | +| Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Spec.syntax_vectors` | + +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. +- 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`. + +## Oracle + +The differential tests compare the tool with two oracles: + +- Python's `datetime` and `calendar` modules: month lengths, offset arithmetic, seconds since the epoch, and `datetime.fromisoformat` on every accepted string it can hold. +- A copy of the rules above, written in Python from the RFC. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..e2c8bab --- /dev/null +++ b/Spec.lean @@ -0,0 +1,142 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the hash it had then. The proofs live in `Proofs.lean`, under + the same names; `lake comparator` checks that each one proves exactly + the statement written here. The `sorry`s below are expected in this + file only. + + The definitions the statements use, written from RFC 3339, are in + `Spec/Defs.lean`, and the types in `Rfc3339/Types.lean`. Both are part + of the specification too. +-/ + +import Rfc3339 +import Spec.Defs + +open Rfc3339 + +/-! ## Validity -/ + +/-- `isValid` decides exactly `Spec.Valid`: the rules of sections 5.6 + and 5.7, except that second 60 is allowed at the end of every month + in UTC, since no table of the months that had a leap second is + kept. -/ +theorem Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := sorry + +/-! ## Printing -/ + +/-- A valid timestamp prints as the grammar of section 5.6 writes it, + with `T` and `Z` in upper case. -/ +theorem Spec.print_eq (t : Timestamp) (h : Spec.Valid t) : + t.print.toList = Spec.render t := sorry + +/-! ## Parsing -/ + +/-- `parse` returns `t` exactly when `t` is valid and the string is how + `t` is written, with `T` and `Z` in either case. So it accepts + nothing outside the grammar of section 5.6 and `Spec.Valid`, rejects + nothing inside them, and returns the fields as written. -/ +theorem Spec.parse_iff (s : String) (t : Timestamp) : + parse s = some t ↔ Spec.Valid t ∧ s.toList.map Spec.asciiUpper = Spec.render t := sorry + +/-- What `parse` returns is valid: among other things, the day exists + in its month, so 30 February never passes. -/ +theorem Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : + Spec.Valid t := sorry + +/-- Round trip: printing a valid timestamp and parsing the result gives + it back. -/ +theorem Spec.parse_print (t : Timestamp) (h : Spec.Valid t) : parse t.print = some t := sorry + +/-- Round trip: parsing a string and printing the result gives the + string back, with `T` and `Z` in upper case. -/ +theorem Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : + t.print.toList = s.toList.map Spec.asciiUpper := sorry + +/-! ## Instants -/ + +/-- `unixSeconds` counts the whole seconds from 1970-01-01T00:00:00Z, by + the calendar of section 5.7, with the offset applied. -/ +theorem Spec.unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : + t.unixSeconds = Spec.unixSeconds t := sorry + +/-- `compareInstant` orders two timestamps by the instants they name, + whatever their offsets: by UTC minute, then by the second within it, + where a leap second comes after 59, then by the fraction. -/ +theorem Spec.compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : + a.compareInstant b = Spec.compareInstants a b := sorry + +/-! ## Test vectors -/ + +/-- The examples of section 5.8, with the fields the RFC reads them + as. -/ +theorem Spec.rfc3339_examples : + parse "1985-04-12T23:20:50.52Z" = some ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ ∧ + parse "1996-12-19T16:39:57-08:00" = some ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ∧ + parse "1990-12-31T23:59:60Z" = some ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ ∧ + parse "1990-12-31T15:59:60-08:00" = some ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ ∧ + parse "1937-01-01T12:00:27.87+00:20" = + some ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ := sorry + +/-- What section 5.8 says about those examples: the second is "equivalent + to 1996-12-20T00:39:57Z", and the fourth is "the same leap second" as + the third. And a count worked out apart from the RFC, by Python's + `calendar.timegm`: the first is 482196050 seconds after the epoch. -/ +theorem Spec.rfc3339_example_instants : + (Timestamp.compareInstant ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ + ⟨1996, 12, 20, 0, 39, 57, [], .z⟩ = .eq) ∧ + (Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ + ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = .eq) ∧ + Timestamp.unixSeconds ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = 482196050 := sorry + +/-- A leap second comes after second 59 of its minute and before the + next minute, fraction included. Unix seconds, as in POSIX time, give + it the same count as the second after it. -/ +theorem Spec.leap_second_order : + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 59, [9], .z⟩ + ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = .lt ∧ + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [5], .z⟩ + ⟨1991, 1, 1, 0, 0, 0, [2], .z⟩ = .lt ∧ + Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ + ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ = .lt ∧ + Timestamp.unixSeconds ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = + Timestamp.unixSeconds ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ := sorry + +/-- Days outside their month, and the leap year rule of Appendix C. -/ +theorem Spec.calendar_vectors : + (parse "2000-02-29T00:00:00Z").isSome ∧ + (parse "2004-02-29T00:00:00Z").isSome ∧ + parse "1900-02-29T00:00:00Z" = none ∧ + parse "2001-02-29T00:00:00Z" = none ∧ + parse "2000-02-30T00:00:00Z" = none ∧ + parse "2001-04-31T00:00:00Z" = none ∧ + parse "2001-01-32T00:00:00Z" = none ∧ + parse "2001-01-00T00:00:00Z" = none ∧ + parse "2001-00-01T00:00:00Z" = none ∧ + parse "2001-13-01T00:00:00Z" = none := sorry + +/-- Second 60 only at the end of a month in UTC. -/ +theorem Spec.leap_second_vectors : + (parse "1990-06-30T23:59:60Z").isSome ∧ + (parse "1991-01-01T00:59:60+01:00").isSome ∧ + parse "1990-12-31T23:59:61Z" = none ∧ + parse "1990-12-31T23:58:60Z" = none ∧ + parse "1990-12-30T23:59:60Z" = none ∧ + parse "1990-12-31T23:59:60+01:00" = none := sorry + +/-- Lower case `t` and `z` are read; other spellings are not. -/ +theorem Spec.syntax_vectors : + parse "1985-04-12t23:20:50.52z" = parse "1985-04-12T23:20:50.52Z" ∧ + parse "1985-04-12 23:20:50.52Z" = none ∧ + parse "1985-04-12T23:20:50.Z" = none ∧ + parse "1985-04-12T23:20:50,52Z" = none ∧ + parse "1985-04-12T23:20Z" = none ∧ + parse "85-04-12T23:20:50Z" = none ∧ + parse "1985-04-12T23:20:50+24:00" = none ∧ + parse "1985-04-12T23:20:50+23:60" = none ∧ + parse "1985-04-12T23:20:50+0100" = none ∧ + parse "1985-04-12T23:20:50" = none ∧ + parse "1985-04-12T23:20:50Z " = none ∧ + parse "1985-04-12T24:00:00Z" = none := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean new file mode 100644 index 0000000..7720bfe --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,200 @@ +/- + The definitions the specification uses, written from RFC 3339 + independently of the code in `Rfc3339/`. Part of the approved + specification, with `Spec.lean` and `Rfc3339/Types.lean`. + + Both the challenge file and the proofs import this file, so each + statement means the same thing on both sides. The `example`s check + the definitions against the RFC's tables and against dates whose day + counts are known. A mistake in either fails the build. +-/ + +import Rfc3339 + +open Rfc3339 + +/-! ## Characters -/ + +/-- ASCII upper case: `a` to `z` (code points 97 to 122) become `A` to + `Z`; nothing else changes. -/ +def Spec.asciiUpper (c : Char) : Char := + if 97 ≤ c.toNat ∧ c.toNat ≤ 122 then Char.ofNat (c.toNat - 32) else c + +example : "azAZ09-:.+tz".toList.map Spec.asciiUpper = "AZAZ09-:.+TZ".toList := by decide + +/-- The decimal digit for `n`, for `n` from 0 to 9. -/ +def Spec.digitChar (n : Nat) : Char := "0123456789".toList.getD n '?' + +/-- The last `k` decimal digits of `n`, most significant first, with + leading zeros. -/ +def Spec.digits (k n : Nat) : List Char := + (List.range k).reverse.map fun i => Spec.digitChar (n / 10 ^ i % 10) + +example : Spec.digits 4 1985 = "1985".toList := by decide +example : Spec.digits 4 7 = "0007".toList := by decide +example : Spec.digits 2 9 = "09".toList := by decide + +/-! ## The format: RFC 3339, section 5.6 + +``` +date-fullyear = 4DIGIT +date-month = 2DIGIT ; 01-12 +date-mday = 2DIGIT ; 01-28, 01-29, 01-30, 01-31 based on + ; month/year +time-hour = 2DIGIT ; 00-23 +time-minute = 2DIGIT ; 00-59 +time-second = 2DIGIT ; 00-58, 00-59, 00-60 based on leap second + ; rules +time-secfrac = "." 1*DIGIT +time-numoffset = ("+" / "-") time-hour ":" time-minute +time-offset = "Z" / time-numoffset + +partial-time = time-hour ":" time-minute ":" time-second + [time-secfrac] +full-date = date-fullyear "-" date-month "-" date-mday +full-time = partial-time time-offset + +date-time = full-date "T" full-time +``` + +The note under the grammar lets `T` and `Z` be written in lower case +too. `render` writes them in upper case; `Spec.parse_iff` in +`Spec.lean` says how the parser treats the lower case forms. -/ + +/-- `time-offset`. -/ +def Spec.renderOffset : Offset → List Char + | .z => ['Z'] + | .plus h m => ['+'] ++ Spec.digits 2 h ++ [':'] ++ Spec.digits 2 m + | .minus h m => ['-'] ++ Spec.digits 2 h ++ [':'] ++ Spec.digits 2 m + +/-- `date-time`, with `T` and `Z` in upper case. The fraction is written + when there is at least one digit. -/ +def Spec.render (t : Timestamp) : List Char := + Spec.digits 4 t.year ++ ['-'] ++ Spec.digits 2 t.month ++ ['-'] ++ Spec.digits 2 t.day ++ + ['T'] ++ Spec.digits 2 t.hour ++ [':'] ++ Spec.digits 2 t.minute ++ [':'] ++ + Spec.digits 2 t.second ++ + (if t.fraction = [] then [] else ['.'] ++ t.fraction.map Spec.digitChar) ++ + Spec.renderOffset t.offset + +example : Spec.render ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = + "1985-04-12T23:20:50.52Z".toList := by decide +example : Spec.render ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ = + "1937-01-01T12:00:27.87+00:20".toList := by decide +example : Spec.render ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ = + "1996-12-19T16:39:57-08:00".toList := by decide + +/-! ## The calendar: RFC 3339, section 5.7 and Appendix C -/ + +/-- Appendix C: a year divisible by 4 is a leap year, except one + divisible by 100, except one divisible by 400. -/ +def Spec.isLeapYear (y : Nat) : Bool := + decide (y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0)) + +example : [1900, 1996, 1997, 2000, 2100, 2400, 0].map Spec.isLeapYear = + [false, true, false, true, false, true, true] := by decide + +/-- Section 5.7, the maximum value of `date-mday` for month `m` of year + `y`; 0 when `m` is not a month. -/ +def Spec.daysInMonth (y m : Nat) : Nat := + if m = 2 then (if Spec.isLeapYear y then 29 else 28) + else if m = 4 ∨ m = 6 ∨ m = 9 ∨ m = 11 then 30 + else if 1 ≤ m ∧ m ≤ 12 then 31 + else 0 + +-- The table of section 5.7, month by month, for a common year and a +-- leap year. +example : (List.range 14).map (Spec.daysInMonth 2001) = + [0, 31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31, 0] := by decide +example : (List.range 14).map (Spec.daysInMonth 2004) = + [0, 31, 29, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31, 0] := by decide + +def Spec.yearLength (y : Nat) : Nat := if Spec.isLeapYear y then 366 else 365 + +/-- The number of days from 0000-01-01 to the date `y`-`m`-`d`, in the + Gregorian calendar extended back to year 0, which RFC 3339 uses + (section 5.7 and Appendix C): the lengths of the years before `y`, + then of the months before `m` in year `y`, then the days before + `d`. -/ +def Spec.dayNumber (y m d : Nat) : Nat := + ((List.range y).map Spec.yearLength).sum + + ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum + (d - 1) + +-- Known counts: 1970-01-01 is day 719528 (Python's +-- `date(1970, 1, 1).toordinal()`, 719163, counts from 0001-01-01 as day +-- 1, and year 0 is a leap year of 366 days), and 2000-03-01 is 11017 +-- days later. +example : Spec.dayNumber 0 1 1 = 0 := by decide +example : Spec.dayNumber 1 1 1 = 366 := by decide +example : Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel +example : Spec.dayNumber 2000 3 1 = 719528 + 11017 := by decide +kernel + +/-! ## Validity -/ + +/-- `time-numoffset`: hours 00 to 23 and minutes 00 to 59. -/ +def Spec.OffsetValid : Offset → Prop + | .z => True + | .plus h m => h ≤ 23 ∧ m ≤ 59 + | .minus h m => h ≤ 23 ∧ m ≤ 59 + +/-- The offset in minutes: local time minus UTC. -/ +def Spec.offsetMinutes : Offset → Int + | .z => 0 + | .plus h m => (h : Int) * 60 + m + | .minus h m => -((h : Int) * 60 + m) + +/-- The minute the timestamp falls in, counted in UTC from + 0000-01-01T00:00Z. Local time is UTC plus the offset, so the offset + is subtracted. -/ +def Spec.utcMinute (t : Timestamp) : Int := + ((Spec.dayNumber t.year t.month t.day * 1440 + t.hour * 60 + t.minute : Nat) : Int) - + Spec.offsetMinutes t.offset + +/-- Section 5.7: `time-second` may be 60 "at the end of months in which + a leap second occurs", and in other time zones "the leap second point + is shifted by the zone offset (so it happens at the same instant + around the globe)". So the minute the leap second falls in, in UTC, + is the last one before a month begins. No table of the months that + had a leap second is kept, so every month is allowed. -/ +def Spec.LeapSecondAllowed (t : Timestamp) : Prop := + ∃ y m, 1 ≤ m ∧ m ≤ 12 ∧ Spec.utcMinute t + 1 = ((Spec.dayNumber y m 1 * 1440 : Nat) : Int) + +/-- A timestamp RFC 3339 allows: every field in the range section 5.6 + gives it, the day within its month (section 5.7), and second 60 only + for a leap second. -/ +def Spec.Valid (t : Timestamp) : Prop := + t.year ≤ 9999 ∧ + 1 ≤ t.month ∧ t.month ≤ 12 ∧ + 1 ≤ t.day ∧ t.day ≤ Spec.daysInMonth t.year t.month ∧ + t.hour ≤ 23 ∧ t.minute ≤ 59 ∧ t.second ≤ 60 ∧ + (t.second = 60 → Spec.LeapSecondAllowed t) ∧ + (∀ d ∈ t.fraction, d ≤ 9) ∧ + Spec.OffsetValid t.offset + +/-! ## Instants -/ + +/-- Whole seconds from 1970-01-01T00:00:00Z to the timestamp. Second 60 + counts as 60 seconds into its minute, so a leap second gives the + same number as the second after it, as POSIX time does. -/ +def Spec.unixSeconds (t : Timestamp) : Int := + (Spec.utcMinute t - ((Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int)) * 60 + t.second + +/-- The fraction's digits read as a whole number: `[5, 2]` is 52. -/ +def Spec.fractionValue (ds : List Nat) : Nat := + ds.foldl (fun acc d => 10 * acc + d) 0 + +example : Spec.fractionValue [0, 5, 2] = 52 := by decide + +/-- The place of the timestamp's instant in UTC order, in units of + `10 ^ (-k)` seconds, for `k` at least the number of fraction digits. + Each UTC minute has 61 places for seconds 0 to 60, so a leap second + comes after second 59 of its minute and before the next minute. + Only the order of these numbers is used, not their size. -/ +def Spec.instantKey (t : Timestamp) (k : Nat) : Int := + (Spec.utcMinute t * 61 + t.second) * 10 ^ k + + Spec.fractionValue t.fraction * 10 ^ (k - t.fraction.length) + +/-- The order of the instants two timestamps name: by UTC minute, then + by the second within it, then by the fraction, compared exactly. -/ +def Spec.compareInstants (a b : Timestamp) : Ordering := + let k := max a.fraction.length b.fraction.length + compare (Spec.instantKey a k) (Spec.instantKey b k) diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..628cd30 --- /dev/null +++ b/bar.toml @@ -0,0 +1,35 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "rfc" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. It was drafted +# by Claude, an AI agent, for the org. +spec_authors = ["claude"] +# The program people run. A change to it voids the approval. +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"] +# 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", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/rfc/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..c9b283c --- /dev/null +++ b/comparator.json @@ -0,0 +1,11 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.isValid_iff", "Spec.print_eq", "Spec.parse_iff", "Spec.parse_valid", + "Spec.parse_print", "Spec.print_parse", "Spec.unixSeconds_eq", "Spec.compareInstant_eq", + "Spec.rfc3339_examples", "Spec.rfc3339_example_instants", "Spec.leap_second_order", "Spec.calendar_vectors", + "Spec.leap_second_vectors", "Spec.syntax_vectors" + ], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..d447d85 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "rfc3339", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..61a658f --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "rfc3339" +version = "0.1.0" +defaultTargets = ["Rfc3339", "Spec", "Proofs", "rfc3339"] + +[[lean_lib]] +name = "Rfc3339" + +[[lean_lib]] +name = "Spec" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "rfc3339" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a6aff06 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md new file mode 100644 index 0000000..4cbdf35 --- /dev/null +++ b/tests/CROSS-CHECK.md @@ -0,0 +1,25 @@ +# Cross-check with other parsers + +Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. + +- This project: the `rfc3339` tool, as tested in TEST-RESULTS.md +- 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 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'` | + diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md new file mode 100644 index 0000000..cea4270 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,18 @@ +# Test results + +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 +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261025 +- Inputs: 300000 +- Mutated: 98931 of the inputs are mutated timestamps +- By kind: compare 42725, error 18, grid 16998, mutated 98931, near miss 42347, valid 98981 +- Strings parsed: 257257, of which 118758 accepted (6407 with a leap second) and 138499 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 110381 +- Pairs ordered: 42725 (14309 before, 12000 same instant, 14324 after, 2092 with a string rejected) +- Malformed requests answered `error`: 18 of 18 +- 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 +- Failures: 0 diff --git a/tests/cross_check.py b/tests/cross_check.py new file mode 100644 index 0000000..6cfd605 --- /dev/null +++ b/tests/cross_check.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""A one-off comparison of this parser with two widely used ones. + +Unlike tests/run_tests.py, this is not part of the verified bar and is +not run in CI. It records where other parsers read RFC 3339 differently, +which is the reason the RFC's rules are proved here. It needs Go, and +the `rfc3339-validator` package, which `jsonschema` calls on the +upper-cased string to check the `date-time` format: + + pip install rfc3339-validator==0.1.4 + python3 tests/cross_check.py [--seed N] [--count N] + +The strings are the ones tests/run_tests.py parses, from the same seed, +plus a few written out below. Each is given to this project's tool, to +Go's `time.Parse` with the `time.RFC3339Nano` layout, and to +`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. +""" + +import argparse +import platform +import re +import subprocess +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import run_tests # noqa: E402 + +ROOT = run_tests.ROOT +REPORT = ROOT / "tests" / "CROSS-CHECK.md" +GO_DIR = ROOT / "tests" / "cross_check" + +PROBES = [ + "1985-04-12T23:20:50.52Z", + "1985-04-12t23:20:50.52z", + "1990-12-31T23:59:60Z", + "1990-12-31T15:59:60-08:00", + "0000-01-01T00:00:00Z", + "2000-01-01T00:00:00+24:00", + "2000-01-01T00:00:00+23:60", + "2000-01-01T00:00:00,5Z", + "2000-01-01T00:00:00.1234567891Z", + "2000-02-30T00:00:00Z", + "2000-01-01 00:00:00Z", +] + +FIELDS = re.compile(r"([0-9]{4})-[0-9]{2}-[0-9]{2}.[0-9]{2}:[0-9]{2}:([0-9]{2})") + + +def category(s, ours_ok): + """The first reason that fits why another parser reads `s` + differently. `ours_ok` is whether the RFC's rules allow `s`.""" + m = FIELDS.match(s) + if ours_ok: + # The other parser rejects what the RFC allows. + if any(c in s for c in "tz"): + return "lower case t or z" + if m and m.group(2) == "60": + return "second 60" + if m and m.group(1) == "0000": + return "year 0000" + return "other" + # The other parser accepts what the RFC does not allow. + if s.endswith("\n"): + return "line break at the end" + if re.search(r"[+-](2[4-9]|[3-9][0-9]):[0-9]{2}$|[+-][0-9]{2}:([6-9][0-9])$", s): + return "offset hour above 23 or minute above 59" + if re.search(r"[0-9],[0-9]", s): + return "comma before the fraction" + if re.fullmatch(r"[0-9]{4}-[0-9]{1,2}-[0-9]{1,2}[Tt][0-9]{1,2}:[0-9]{1,2}:[0-9]{1,2}.*", s) and not m: + return "a field with one digit" + if m and m.group(2) == "60": + return "second 60 outside the last minute of a month in UTC" + return "other" + + +def go_tool(strings): + exe = ROOT / ".lake" / "cross_check_go" + subprocess.run(["go", "build", "-o", str(exe), "main.go"], cwd=GO_DIR, check=True, + env={**__import__("os").environ, "GO111MODULE": "off"}) + data = "".join(s.encode("utf-8").hex() + "\n" for s in strings) + out = subprocess.run([str(exe)], input=data, capture_output=True, text=True, check=True) + return out.stdout.split("\n")[: len(strings)] + + +def go_version(): + out = subprocess.run(["go", "version"], capture_output=True, text=True) + return out.stdout.strip() + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=int, default=300_000) + args = ap.parse_args() + try: + from rfc3339_validator import validate_rfc3339 + except ImportError: + sys.exit("needs the rfc3339-validator package: pip install rfc3339-validator==0.1.4") + from importlib.metadata import version + + strings = list(PROBES) + for _, req, _, _ in run_tests.cases(args.seed, args.count): + if req.startswith("parse ") and len(req.split(" ")) == 2: + try: + strings.append(bytes.fromhex(req.split(" ")[1]).decode("utf-8")) + except ValueError: + pass + lean, problem = run_tests.run_tool("".join(f"parse {run_tests.hexed(s)}\n" for s in strings)) + if problem or len(lean) != len(strings): + sys.exit(f"the tool failed: {problem}") + go = go_tool(strings) + + tallies = {"Go": {}, "rfc3339-validator": {}} + examples = {"Go": {}, "rfc3339-validator": {}} + value_mismatch = [] + for s, ours, theirs in zip(strings, lean, go): + ok = ours.startswith("OK") + for name, other_ok in (("Go", theirs.startswith("OK")), ("rfc3339-validator", validate_rfc3339(s))): + if other_ok == ok: + continue + key = ("accepts" if other_ok else "rejects", category(s, ok)) + tallies[name][key] = tallies[name].get(key, 0) + 1 + examples[name].setdefault(key, []) + if len(examples[name][key]) < 3: + examples[name][key].append(s) + if ok and theirs.startswith("OK"): + _, secs, nanos = theirs.split("\t") + f = ours.split("\t") + frac = (f[9] + "0" * 9)[:9] + if (int(secs), int(nanos)) != (int(f[2]), int(frac)): + value_mismatch.append((s, theirs, ours)) + + lines = [ + "# Cross-check with other parsers", + "", + "Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar.", + "", + f"- This project: the `rfc3339` tool, as tested in TEST-RESULTS.md", + f"- Go: `time.Parse(time.RFC3339Nano, s)`, {go_version()}", + f"- rfc3339-validator {version('rfc3339-validator')} (Python {platform.python_version()}), " + "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`.", + f"- Seed: {args.seed}", + f"- Strings: {len(strings)}", + f"- Strings both this project and Go accept, read to a different instant: {len(value_mismatch)}", + "", + "Where each parser differs from this one, by the first category that fits the string:", + "", + "| Parser | Differs by | Category | Strings | Example |", + "| --- | --- | --- | --- | --- |", + ] + for name in tallies: + for (how, cat), n in sorted(tallies[name].items(), key=lambda kv: (-kv[1], kv[0])): + ex = ", ".join(f"`{e!r}`" for e in examples[name][(how, cat)][:2]) + lines.append(f"| {name} | {how} | {cat} | {n} | {ex} |") + lines.append("") + for s, theirs, ours in value_mismatch[:20]: + lines.append(f"- Different instant: `{s!r}`: Go `{theirs}`, this project `{ours}`") + REPORT.write_text("\n".join(lines) + "\n", encoding="utf-8") + print(f"{len(strings)} strings; report in {REPORT}") + + +if __name__ == "__main__": + main() diff --git a/tests/cross_check/main.go b/tests/cross_check/main.go new file mode 100644 index 0000000..79948ef --- /dev/null +++ b/tests/cross_check/main.go @@ -0,0 +1,32 @@ +// Reads one hex-encoded string per line and prints how Go's time.Parse +// reads it with the time.RFC3339Nano layout: "OK", the Unix seconds and +// the nanoseconds, or "ERR". Used by tests/cross_check.py. +package main + +import ( + "bufio" + "encoding/hex" + "fmt" + "os" + "time" +) + +func main() { + in := bufio.NewScanner(os.Stdin) + in.Buffer(make([]byte, 1<<20), 1<<20) + out := bufio.NewWriter(os.Stdout) + defer out.Flush() + for in.Scan() { + b, err := hex.DecodeString(in.Text()) + if err != nil { + fmt.Fprintln(out, "BADHEX") + continue + } + t, err := time.Parse(time.RFC3339Nano, string(b)) + if err != nil { + fmt.Fprintln(out, "ERR") + continue + } + fmt.Fprintf(out, "OK\t%d\t%d\n", t.Unix(), t.Nanosecond()) + } +} diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..21493b8 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,678 @@ +#!/usr/bin/env python3 +"""Differential tests: the Lean parser against Python's date code. + +There are two oracles: + +- Python's `datetime` and `calendar` modules. `calendar.isleap` and + `calendar.mdays` give the month lengths, `datetime` arithmetic applies + offsets and counts seconds since the epoch, and + `datetime.fromisoformat` reads every accepted timestamp it can + represent (years 1 to 9999, seconds 0 to 59) and must agree on every + field. +- A copy of the rules of RFC 3339, sections 5.6 and 5.7, written here + from the RFC: a regular expression for the grammar, then the ranges, + the month lengths and the leap second rule. It decides which strings + are accepted, since `fromisoformat` also reads ISO 8601 forms that + RFC 3339 does not allow. + +Inputs come from a recorded seed: + +- valid timestamps with random fields, weighted toward month ends, + 29 February, leap seconds, long fractions, and every offset form; +- near misses: one field just out of range; +- mutations of valid timestamps: a character replaced, deleted, + inserted or swapped, the string cut short or extended, a digit + replaced by a non-ASCII digit, a line break or NUL put in. A mutation + that leaves the string unchanged is drawn again; +- every day from 0 to 32 of every month from 0 to 13 in years chosen + for the leap year rule, and second 60 at every month end of five + years, 0000 and 9999 among them, under 15 offsets, at the one local + minute that can be a leap second and at the minutes either side; +- 0000-01-01 and 9999-12-31 under offsets that move the UTC date out + of years 0000 to 9999, near both ends of the day, with seconds 0, 59 + and 60, each parsed and each compared with the next; +- pairs of timestamps to order, including pairs that name the same + instant with different offsets or fractions, leap seconds next to + the seconds around them, and pairs with a string that is rejected; +- malformed requests, which the tool must answer with `error`. + +Every seventh request ends in CR LF. The first 20,000 parsed strings +that can be command-line arguments are also given to `rfc3339 check`. +For every input the Lean answer must equal the oracle's. + + python3 tests/run_tests.py [--seed N] [--count N] + +It builds the executable first, writes tests/TEST-RESULTS.md, and exits +non-zero if any input disagrees. +""" + +import argparse +import calendar +import itertools +import platform +import random +import re +import subprocess +import sys +import threading +from datetime import datetime, timedelta, timezone +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "rfc3339" +RESULTS = ROOT / "tests" / "TEST-RESULTS.md" +TIMEOUT = 1800 +BUILD_TIMEOUT = 3600 + +# The grammar of RFC 3339, section 5.6, in ASCII digits only. `T` and `Z` +# may be lower case (the note under the grammar). +GRAMMAR = re.compile( + r"([0-9]{4})-([0-9]{2})-([0-9]{2})[Tt]([0-9]{2}):([0-9]{2}):([0-9]{2})" + r"(?:\.([0-9]+))?([Zz]|([+-])([0-9]{2}):([0-9]{2}))") + +EPOCH = datetime(1970, 1, 1, tzinfo=timezone.utc) +# The Gregorian calendar repeats every 400 years, which are 146097 days. +# Years 0, 1 and 9999, where `datetime` cannot hold the date or the UTC +# date a day away, are moved by 400 years for the arithmetic, and the +# seconds moved back. +CYCLE_DAYS = 146097 + + +def month_length(year, month): + if month == 2 and calendar.isleap(year): + return 29 + return calendar.mdays[month] + + +def shifted(year): + """A year `datetime` can hold with the same calendar, and the days + the move adds.""" + if year < 2: + return year + 400, CYCLE_DAYS + if year > 9998: + return year - 400, -CYCLE_DAYS + return year, 0 + + +def utc_parts(f): + """The UTC date and time of the minute the timestamp falls in, and + the whole seconds since the epoch, by `datetime` arithmetic.""" + year, days = shifted(f["year"]) + tz = timezone(timedelta(minutes=f["offset_minutes"])) + local = datetime(year, f["month"], f["day"], f["hour"], f["minute"], tzinfo=tz) + utc = local.astimezone(timezone.utc) + delta = local - EPOCH + seconds = (delta.days - days) * 86400 + delta.seconds + f["second"] + return utc, seconds + + +def reference(s): + """The RFC 3339 rules: the fields of `s`, or None when RFC 3339 does + not allow it.""" + m = GRAMMAR.fullmatch(s) + if not m: + return None + year, month, day, hour, minute, second = (int(m.group(i)) for i in range(1, 7)) + frac = m.group(7) or "" + if m.group(8) in "Zz": + off_text, off = "Z", 0 + else: + oh, om = int(m.group(10)), int(m.group(11)) + if oh > 23 or om > 59: + return None + off_text = m.group(8) + off = (oh * 60 + om) * (1 if m.group(9) == "+" else -1) + if not (1 <= month <= 12 and 1 <= day <= month_length(year, month)): + return None + if hour > 23 or minute > 59 or second > 60: + return None + f = dict(year=year, month=month, day=day, hour=hour, minute=minute, second=second, + fraction=frac, offset=off_text, offset_minutes=off) + utc, seconds = utc_parts(f) + if second == 60: + # Section 5.7: at the end of a month, in UTC. + if not (utc.hour == 23 and utc.minute == 59 and (utc + timedelta(days=1)).day == 1): + return None + f["unix"] = seconds + f["print"] = s.upper() + return f + + +def answer(f): + if f is None: + return "REJECT" + return "\t".join(["OK", f["print"], str(f["unix"])] + + [str(f[k]) for k in ("year", "month", "day", "hour", "minute", "second")] + + [f["fraction"], f["offset"]]) + + +def fromisoformat_agrees(f): + """Whether `datetime.fromisoformat` reads the upper case form to the + same fields, offset and instant. Only for what it can hold.""" + if f["year"] < 1 or f["second"] == 60: + return None + try: + dt = datetime.fromisoformat(f["print"]) + except ValueError: + return False + micro = int((f["fraction"] + "000000")[:6]) + return ((dt.year, dt.month, dt.day, dt.hour, dt.minute, dt.second, dt.microsecond) == + (f["year"], f["month"], f["day"], f["hour"], f["minute"], f["second"], micro) and + dt.utcoffset() == timedelta(minutes=f["offset_minutes"]) and + (dt.replace(microsecond=0) - EPOCH) == timedelta(seconds=f["unix"])) + + +def instant(f): + """The place of the instant in UTC order: the UTC minute, the second + within it (a leap second, 60, after 59), then the exact fraction.""" + minute = (f["unix"] - f["second"]) // 60 + return (minute, f["second"], Fraction(int(f["fraction"] or "0"), 10 ** len(f["fraction"]))) + + +def order(a, b): + fa, fb = reference(a), reference(b) + if fa is None or fb is None: + return "REJECT" + x, y = instant(fa), instant(fb) + return "<" if x < y else ">" if x > y else "=" + + +# Generators. + +def offset_text(minutes, rng, zulu_ok=True): + if minutes == 0 and zulu_ok and rng.random() < 0.5: + return rng.choice("Zz") + sign = "-" if minutes < 0 or (minutes == 0 and rng.random() < 0.3) else "+" + m = abs(minutes) + return f"{sign}{m // 60:02d}:{m % 60:02d}" + + +def stamp(year, month, day, hour, minute, second, frac, off, t="T"): + return (f"{year:04d}-{month:02d}-{day:02d}{t}{hour:02d}:{minute:02d}:{second:02d}" + + (f".{frac}" if frac else "") + off) + + +def random_fraction(rng): + r = rng.random() + if r < 0.4: + return "" + n = rng.choice([1, 1, 2, 3, 3, 6, 6, 9, 12]) if r < 0.95 else rng.randint(13, 40) + return "".join(rng.choice("0123456789") for _ in range(n)) + + +def random_offset_minutes(rng): + r = rng.random() + if r < 0.3: + return 0 + if r < 0.4: + return rng.choice([-1439, 1439, -1, 1, -60, 60, 330, 345, -570, 840, -720, 720]) + return rng.randint(-1439, 1439) + + +def random_year(rng): + if rng.random() < 0.2: + return rng.choice([0, 1, 4, 99, 100, 400, 1900, 1970, 1972, 2000, 2024, 2100, 9998, 9999]) + return rng.randint(0, 9999) + + +def random_valid(rng): + year, month = random_year(rng), rng.randint(1, 12) + last = month_length(year, month) + day = rng.choice([1, 2, last - 1, last, rng.randint(1, last)]) + hour, minute = rng.randint(0, 23), rng.randint(0, 59) + off = random_offset_minutes(rng) + second = rng.randint(0, 59) + t = "T" if rng.random() < 0.85 else "t" + if rng.random() < 0.05: + # A leap second: 23:59 UTC on a month's last day, in local time. + utc = datetime(shifted(year)[0], month, last, 23, 59) + timedelta(minutes=off) + year = utc.year - (shifted(year)[0] - year) + if not 0 <= year <= 9999: + year, utc, off = 1990, datetime(1990, 12, 31, 23, 59), 0 + month, day, hour, minute, second = utc.month, utc.day, utc.hour, utc.minute, 60 + return stamp(year, month, day, hour, minute, second, random_fraction(rng), + offset_text(off, rng), t) + + +def near_miss(rng): + year, month = random_year(rng), rng.randint(1, 12) + day, hour, minute, second = rng.randint(1, 28), rng.randint(0, 23), rng.randint(0, 59), rng.randint(0, 59) + oh, om, sign = rng.randint(0, 23), rng.randint(0, 59), rng.choice("+-") + which = rng.randrange(10) + if which == 0: + month = rng.choice([0, 13, 19, 99]) + elif which == 1: + day = month_length(year, month) + rng.choice([1, 2, 69]) + elif which == 2: + day = 0 + elif which == 3: + hour = rng.choice([24, 25, 99]) + elif which == 4: + minute = rng.choice([60, 99]) + elif which == 5: + second = rng.choice([60, 61, 99]) + elif which == 6: + oh = rng.choice([24, 99]) + elif which == 7: + om = rng.choice([60, 99]) + elif which == 8: + year, month, day = rng.choice([1900, 2100, 2001, 1999, 2200, 1800]), 2, 29 + else: + second = 60 + day = month_length(year, month) + off = f"{sign}{oh:02d}:{om:02d}" if rng.random() < 0.7 else "Z" + return stamp(year, month, day, hour, minute, second, random_fraction(rng), off) + + +ODD_CHARS = ["0", "9", "-", ":", ".", "+", "T", "t", "Z", "z", " ", "_", "/", ",", "a", "Y", + "\n", "\r", "\t", "\x00", "٠", "৪", "０", "\U0001d7d8", "é", + "−", "‐", " ", ""] + + +def mutate(rng, s): + cs = list(s) + op = rng.randrange(8) + if op == 0 and cs: + cs[rng.randrange(len(cs))] = rng.choice(ODD_CHARS) + elif op == 1 and cs: + del cs[rng.randrange(len(cs))] + elif op == 2: + cs.insert(rng.randint(0, len(cs)), rng.choice(ODD_CHARS)) + elif op == 3 and len(cs) > 1: + i = rng.randrange(len(cs) - 1) + cs[i], cs[i + 1] = cs[i + 1], cs[i] + elif op == 4 and cs: + cs = cs[: rng.randrange(len(cs))] + elif op == 5: + cs += list(rng.choice(["Z", "0", ".5", " ", "\n", "+00:00", "Zz"])) + elif op == 6: + digits = [i for i, c in enumerate(cs) if c.isdigit()] + if digits: + i = rng.choice(digits) + cs[i] = chr(rng.choice([0x0660, 0x09E6, 0xFF10, 0x1D7CE]) + int(cs[i])) + else: + cs = list(s.swapcase() if rng.random() < 0.5 else s.replace("T", " ").replace("t", " ")) + return "".join(cs) + + +def day_grid(): + for year in [0, 1, 4, 100, 400, 1900, 1996, 2000, 2001, 2004, 2100, 2400, 9999]: + for month in range(14): + for day in range(33): + yield stamp(year, month, day, 12, 0, 0, "", "Z") + + +def leap_grid(): + offsets = [-1439, -720, -481, -480, -60, -1, 0, 1, 60, 330, 345, 720, 1439] + for year in [0, 1990, 2000, 2001, 9999]: + for month in range(1, 13): + last = month_length(year, month) + for day in sorted({1, 2, last - 1, last}): + for off in offsets: + # The local minute that is 23:59 UTC on this date's day, + # and the minutes either side of it. + base = (23 * 60 + 59 + off) % 1440 + for minute_of_day in {base, (base - 1) % 1440, (base + 1) % 1440}: + h, m = divmod(minute_of_day, 60) + for text in {f"+{off // 60:02d}:{off % 60:02d}" if off >= 0 else + f"-{-off // 60:02d}:{-off % 60:02d}", + *(["Z", "-00:00"] if off == 0 else [])}: + yield stamp(year, month, day, h, m, 60, "", text) + + +def leap_pair(rng): + """A leap second and a nearby second: second 59 before it, or the + first second of the next minute, in the same or another offset.""" + year, month = rng.randint(1972, 2100), rng.choice([6, 12, rng.randint(1, 12)]) + last = month_length(year, month) + frac_a, frac_b = random_fraction(rng), random_fraction(rng) + off_a, off_b = random_offset_minutes(rng), random_offset_minutes(rng) + leap = datetime(year, month, last, 23, 59) + timedelta(minutes=off_a) + a = stamp(leap.year, leap.month, leap.day, leap.hour, leap.minute, 60, frac_a, + offset_text(off_a, rng)) + if rng.random() < 0.5: + other, sec = datetime(year, month, last, 23, 59) + timedelta(minutes=off_b), 59 + else: + other, sec = datetime(year, month, last, 23, 59) + timedelta(minutes=1 + off_b), 0 + b = stamp(other.year, other.month, other.day, other.hour, other.minute, sec, frac_b, + offset_text(off_b, rng)) + return (a, b) if rng.random() < 0.5 else (b, a) + + +def edge_grid(): + """The first and last days of the range, where an offset moves the + UTC date outside years 0000 to 9999: local minutes near each end of + the day and near the offset, with seconds 0, 59 and 60.""" + for year, month, day in [(0, 1, 1), (9999, 12, 31)]: + for off in [1, -1, 61, -61, 1439, -1439]: + a = abs(off) + for minute_of_day in sorted({0, 1, a - 1, a, 1440 - a - 1, 1440 - a, 1438, 1439}): + h, m = divmod(minute_of_day % 1440, 60) + for second in (0, 59, 60): + sign = "+" if off > 0 else "-" + yield stamp(year, month, day, h, m, second, "", + f"{sign}{a // 60:02d}:{a % 60:02d}") + + +def same_instant_pair(rng): + """Two spellings of one instant: different offsets, or a fraction + with trailing zeros.""" + year, month = rng.randint(1, 9998), rng.randint(1, 12) + day = rng.randint(1, month_length(year, month)) + base = datetime(year, month, day, rng.randint(0, 23), rng.randint(0, 59), rng.randint(0, 59)) + frac = random_fraction(rng) + o1, o2 = random_offset_minutes(rng), random_offset_minutes(rng) + l1, l2 = base + timedelta(minutes=o1), base + timedelta(minutes=o2) + f2 = frac + "0" * rng.randint(0, 3) if frac else rng.choice(["", "0", "000"]) + if rng.random() < 0.3: + # Nudge the second fraction by one unit in its last place. + f2 = (frac or "0") + "1" + a = stamp(l1.year, l1.month, l1.day, l1.hour, l1.minute, l1.second, frac, offset_text(o1, rng)) + b = stamp(l2.year, l2.month, l2.day, l2.hour, l2.minute, l2.second, f2, offset_text(o2, rng)) + return (a, b) if rng.random() < 0.5 else (b, a) + + +MALFORMED = [ + ("frob 30", "unknown operation"), + ("PARSE 30", "operations are lower case"), + ("parse", "no argument"), + ("parse 3", "an odd number of hex digits"), + ("parse 3G", "not a hex digit"), + ("parse 3A", "hex digits are lower case"), + ("parse ff", "not UTF-8"), + ("parse c0af", "an overlong encoding, not UTF-8"), + ("parse eda080", "a surrogate, not UTF-8"), + ("parse 30 30", "two arguments to parse"), + ("compare 30", "one argument to compare"), + ("compare 30 30 30", "three arguments to compare"), + ("compare 3 30", "odd hex in the first string to compare"), + ("compare 30 3A", "upper case hex in the second string to compare"), + ("compare 30 ff", "not UTF-8 in the second string to compare"), + ("compare c0af 30", "an overlong encoding in the first string to compare"), + (" parse 30", "a leading space"), + ("parse 30", "two spaces"), +] + +# A last line with no LF must still be answered. +AT_EOF = [ + ("parse " + "1985-04-12T23:20:50.52Z".encode().hex(), None), + ("compare " + "1990-12-31T23:59:60Z".encode().hex() + " " + + "1991-01-01T00:00:00Z".encode().hex(), "<"), +] + + +def hexed(s): + return s.encode("utf-8").hex() + + +def cases(seed, count): + """(label, request, expected answer, mutated) for each input.""" + rng = random.Random(seed) + fixed = [] + 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()) + for a, b in zip(edges, edges[1:]): + fixed.append(("compare", f"compare {hexed(a)} {hexed(b)}", order(a, b), False)) + for req, _ in MALFORMED: + fixed.append(("error", req, "error", False)) + made = 0 + for item in fixed[:count]: + yield item + made += 1 + while made < count: + r = rng.random() + if r < 0.35: + s, label, mutated = random_valid(rng), "valid", False + elif r < 0.5: + s, label, mutated = near_miss(rng), "near miss", False + elif r < 0.85: + base = random_valid(rng) + s = mutate(rng, base) + while s == base: + s = mutate(rng, base) + label, mutated = "mutated", True + else: + r = rng.random() + if r < 0.4: + a, b = same_instant_pair(rng) + elif r < 0.6: + a, b = leap_pair(rng) + elif r < 0.65: + a, b = (near_miss(rng), random_valid(rng))[:: rng.choice([1, -1])] + else: + a, b = random_valid(rng), random_valid(rng) + yield ("compare", f"compare {hexed(a)} {hexed(b)}", order(a, b), False) + made += 1 + continue + yield (label, f"parse {hexed(s)}", answer(reference(s)), mutated) + made += 1 + + +def run_tool(data, timeout=TIMEOUT): + """The tool's answer lines for `data`, and a note on how the run + failed, or None. No right answer is longer than its request plus 64 + bytes, so a tool that writes more than that is stopped.""" + raw = data.encode("utf-8") + limit = 2 * len(raw) + 64 * (data.count("\n") + 1) + try: + proc = subprocess.Popen([str(EXE), "serve"], stdin=subprocess.PIPE, + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + except OSError as e: + return [], f"could not run {EXE.relative_to(ROOT)}: {e.strerror or e}" + out, err = bytearray(), bytearray() + + def feed(): + try: + proc.stdin.write(raw) + proc.stdin.close() + except (BrokenPipeError, ValueError): + pass + + def drain(stream, buf, cap): + while chunk := stream.read1(1 << 16): + buf += chunk + if len(buf) > cap: + proc.kill() + return + + threads = [threading.Thread(target=feed), + threading.Thread(target=drain, args=(proc.stdout, out, limit)), + threading.Thread(target=drain, args=(proc.stderr, err, 1 << 20))] + for t in threads: + t.start() + problem = None + try: + proc.wait(timeout=timeout) + except subprocess.TimeoutExpired: + proc.kill() + problem = f"no end after {timeout} seconds" + for t in threads: + t.join() + proc.wait() + if len(out) > limit: + problem = problem or f"more than {limit} bytes of output, stopped" + elif proc.returncode != 0 and not problem: + tail = " / ".join(err.decode("utf-8", "backslashreplace").splitlines()[-3:]) + problem = f"exit status {proc.returncode}: {tail}" + text = bytes(out).decode("utf-8", "backslashreplace") + if text and not text.endswith("\n"): + problem = problem or "the last answer has no LF" + lines = text.split("\n") + if lines and lines[-1] == "": + lines.pop() + return lines, problem + + +def run_check(args, timeout=300): + """Output lines and exit code of `rfc3339 check ARGS`.""" + run = subprocess.run([str(EXE), "check", *args], capture_output=True, timeout=timeout) + return run.stdout.decode("utf-8", "backslashreplace").split("\n")[:-1], run.returncode + + +def check_mode(items, limit=20000, batch=500): + """Runs `check` mode on the first `limit` parsed strings that can be + command-line arguments, in batches, and on no arguments at all. Each + output line must be the printed form and Unix seconds, or `invalid` + and the string, and the exit code 1 when any string is invalid.""" + strings = [] + for label, req, _, _ in items: + if label != "error" and req.startswith("parse ") and len(strings) < limit: + s = bytes.fromhex(req.split(" ")[1]).decode("utf-8") + if s and not any(c in s for c in "\x00\n\r"): + strings.append(s) + problems = [] + for i in range(0, len(strings), batch): + args = strings[i:i + batch] + want = [] + for s in args: + f = reference(s) + want.append(f"{f['print']}\t{f['unix']}" if f else f"invalid\t{s}") + code_want = 1 if any(w.startswith("invalid\t") for w in want) else 0 + got, code = run_check(args) + if got != want or code != code_want: + bad = next((j for j, (g, w) in enumerate(zip(got, want)) if g != w), None) + where = f"line {bad}: got {got[bad]!r}, expected {want[bad]!r}" if bad is not None else "" + problems.append((f"check with {len(args)} arguments from {args[0]!r}", + f"exit {code_want}", f"exit {code} {where}".strip())) + got, code = run_check([]) + if code != 2 or got: + problems.append(("check with no arguments", "usage and exit 2", f"exit {code}, {got[:2]}")) + return len(strings), problems + + +def oracle(): + return (f"Python {platform.python_version()} `datetime` and `calendar`, and the " + f"RFC 3339 rules copied into this script") + + +def lean_version(): + try: + out = subprocess.run(["lake", "env", "lean", "--version"], cwd=ROOT, + capture_output=True, text=True, errors="backslashreplace", + timeout=300) + first = out.stdout.strip().splitlines()[:1] + return first[0] if first else "unknown" + except (OSError, subprocess.TimeoutExpired): + return "unknown" + + +def count(text): + n = int(text) + if n < 1: + raise argparse.ArgumentTypeError("the count must be at least 1") + return n + + +def write(lines): + RESULTS.write_text("\n".join(lines), encoding="utf-8") + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=count, default=300_000) + args = ap.parse_args() + if sys.version_info < (3, 11): + sys.exit("needs Python 3.11 or later, for datetime.fromisoformat with offsets and Z") + + # Always build, so the tests never run an executable older than the code. + try: + build = subprocess.run(["lake", "build", "rfc3339"], cwd=ROOT, capture_output=True, + text=True, errors="backslashreplace", timeout=BUILD_TIMEOUT) + built, log = build.returncode == 0, build.stdout + build.stderr + except (OSError, subprocess.TimeoutExpired) as e: + built, log = False, str(e) + if not built: + write(["# Test results", "", f"- Oracle: {oracle()}", f"- Seed: {args.seed}", + "- Inputs: 0", "- Failures: 1 (`lake build rfc3339` failed)", ""]) + sys.exit("lake build rfc3339 failed:\n" + log) + + items = list(cases(args.seed, args.count)) + # Every seventh request ends in CR LF, which the tool must take as LF. + out, problem = run_tool("".join(req + ("\r\n" if i % 7 == 6 else "\n") + for i, (_, req, _, _) in enumerate(items))) + failures = [("(whole run)", "a clean run", problem)] if problem else [] + for item, got in itertools.zip_longest(items, out): + if item is None: + failures.append(("(no request)", "nothing", got)) + elif got != item[2]: + failures.append((item[1], item[2], "(no answer)" if got is None else got)) + + # The second oracle: every accepted timestamp that `datetime` can + # hold must read the same there. + checked = 0 + for label, req, want, _ in items: + if req.startswith("parse ") and want.startswith("OK"): + s = bytes.fromhex(req.split(" ")[1]).decode("utf-8") + agrees = fromisoformat_agrees(reference(s)) + if agrees is None: + continue + checked += 1 + if not agrees: + failures.append((req, "datetime.fromisoformat to agree", s)) + + check_args, check_problems = check_mode(items) + failures += check_problems + + eof_right = 0 + for req, want in AT_EOF: + if want is None: + s = bytes.fromhex(req.split(" ")[1]).decode("utf-8") + want = answer(reference(s)) + got, problem = run_tool(req, timeout=60) + if got == [want] and not problem: + eof_right += 1 + else: + failures.append((req + " (at end of input)", want, f"{got} {problem or ''}".strip())) + + by_label = {} + for label, _, _, _ in items: + by_label[label] = by_label.get(label, 0) + 1 + parsed = [want for label, req, want, _ in items if label != "error" and req.startswith("parse ")] + accepted = sum(1 for w in parsed if w.startswith("OK")) + leap = sum(1 for w in parsed if w.startswith("OK") and w.split("\t")[8] == "60") + orders = [want for label, _, want, _ in items if label == "compare"] + mutated = sum(1 for item in items if item[3]) + malformed = [got for item, got in zip(items, out) if item[0] == "error"] + + lines = [ + "# Test results", + "", + "Written by `tests/run_tests.py`. Rerun it to check these numbers.", + "", + f"- Oracle: {oracle()}", + f"- Lean: {lean_version()}", + f"- Seed: {args.seed}", + f"- Inputs: {len(items)}", + f"- Mutated: {mutated} of the inputs are mutated timestamps", + f"- By kind: " + ", ".join(f"{k} {v}" for k, v in sorted(by_label.items())), + f"- Strings parsed: {len(parsed)}, of which {accepted} accepted " + f"({leap} with a leap second) and {len(parsed) - accepted} rejected", + f"- Accepted strings also read by `datetime.fromisoformat`, with the same fields, " + f"offset and seconds: {checked}", + f"- Pairs ordered: {len(orders)} ({orders.count('<')} before, {orders.count('=')} same " + f"instant, {orders.count('>')} after, {orders.count('REJECT')} with a string rejected)", + f"- 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}", + f"- Strings also given to `rfc3339 check` as arguments, in batches of 500: {check_args}, " + f"and once with no arguments", + f"- Last lines with no LF, sent alone, answered right: {eof_right} of {len(AT_EOF)}", + f"- Failures: {len(failures)}", + "", + ] + if failures: + lines += ["## Failures", ""] + lines += [f"- `{req[:160]!r}`: expected `{want[:120]!r}`, got `{got[:120]!r}`" + for req, want, got in failures[:50]] + lines.append("") + write(lines) + agree = sum(1 for item, got in zip(items, out) if got == item[2]) + print(f"{agree}/{len(items)} inputs agree, {len(failures)} failures; results in {RESULTS}") + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main())