Leap seconds: the table, SI seconds, fromSiSeconds and TAI − UTC, proved

Main.lean

@@ -22,6 +22,16 @@
                       seconds since the epoch, or NONE when it falls
                       outside the years 0000 to 9999; N is decimal, with
                       an optional leading `-`
+    known HEX         prints  OK, then tab-separated: SI seconds since
+                      1972-01-01T00:00:00Z (before 1972, Unix seconds
+                      less 63072000) and TAI - UTC (`-` before
+                      1972, when TAI - UTC was not a whole number of
+                      seconds); NOLEAP when the timestamp is valid but
+                      its second 60 is not a leap second of the table;
+                      or REJECT
+    fromsi N          prints  the printed form of the UTC timestamp N SI
+                      seconds after 1972-01-01T00:00:00Z, with second 60
+                      at a leap second, or NONE outside 1972 to 9999
 
   A malformed request prints `error`: an unknown operation, hex digits
   that are not in pairs, bytes that are not UTF-8, or a number that is
@@ -30,7 +40,9 @@
 
   Every answer comes from the proved functions in `Rfc3339/`: `parse`,
   `Timestamp.print`, `Timestamp.unixSeconds`,
-  `Timestamp.compareInstant` and `fromUnixSeconds`. The hex decoding and the request handling
+  `Timestamp.compareInstant`, `fromUnixSeconds`,
+  `Timestamp.isValidKnown`, `Timestamp.siSeconds`,
+  `Timestamp.taiMinusUtc` and `fromSiSeconds`. The hex decoding and the request handling
   here are covered by the tests, not by a proof.
 -/
 
@@ -93,6 +105,20 @@ def request (line : String) : Option String :=
     pure <| match fromUnixSeconds s with
       | some t => t.print
       | none => "NONE"
+  | ["known", h] => do
+    let s ← fromHex h
+    pure <| match parse s with
+      | some t =>
+        if t.isValidKnown then
+          let tai := if 63072000 ≤ t.unixSeconds then toString t.taiMinusUtc else "-"
+          s!"OK\t{t.siSeconds}\t{tai}"
+        else "NOLEAP"
+      | none => "REJECT"
+  | ["fromsi", n] => do
+    let s ← decimal n
+    pure <| match fromSiSeconds s with
+      | some t => t.print
+      | none => "NONE"
   | _ => none
 
 /-- The line without its line ending: LF, or CR LF. -/

Proofs.lean

@@ -6,3 +6,4 @@
 
 import Proofs.Main
 import Proofs.FromUnix.Main
+import Proofs.Leap.Main