RFC 3339 timestamps: parse, print, validity, Unix seconds and instant order, with proofs

.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

.gitignore

@@ -0,0 +1,2 @@
+.lake/
+__pycache__/

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

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

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