diff --git a/Main.lean b/Main.lean index 1b56fcd..865ff9e 100644 --- a/Main.lean +++ b/Main.lean @@ -32,6 +32,12 @@ 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 + ixdtf HEX prints OK, then tab-separated: the printed form of + the RFC 9557 string, whether the example + application of `Spec.exampleProcessor` must treat + it as erroneous (`true` or `false`), and the values + of the first `u-ca` tag joined by `-`, or `-`; + or REJECT 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 @@ -42,11 +48,13 @@ `Timestamp.print`, `Timestamp.unixSeconds`, `Timestamp.compareInstant`, `fromUnixSeconds`, `Timestamp.isValidKnown`, `Timestamp.siSeconds`, - `Timestamp.taiMinusUtc` and `fromSiSeconds`. The hex decoding and the request handling + `Timestamp.taiMinusUtc`, `fromSiSeconds`, `parseExt`, `Ext.print`, + `Ext.erroneous` and `Ext.lookup`. The hex decoding and the request handling here are covered by the tests, not by a proof. -/ import Rfc3339 +import Spec.Ixdtf open Rfc3339 @@ -114,6 +122,15 @@ def request (line : String) : Option String := s!"OK\t{t.siSeconds}\t{tai}" else "NOLEAP" | none => "REJECT" + | ["ixdtf", h] => do + let s ← fromHex h + pure <| match parseExt s with + | some e => + let cal := match e.lookup "u-ca".toList with + | some t => String.ofList (['-'].intercalate t.values) + | none => "-" + s!"OK\t{e.print}\t{e.erroneous Spec.exampleProcessor}\t{cal}" + | none => "REJECT" | ["fromsi", n] => do let s ← decimal n pure <| match fromSiSeconds s with diff --git a/Proofs.lean b/Proofs.lean index 80f7eb1..1eedfed 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -7,3 +7,4 @@ import Proofs.Main import Proofs.FromUnix.Main import Proofs.Leap.Main +import Proofs.Ixdtf.Main diff --git a/Proofs/Ixdtf/Main.lean b/Proofs/Ixdtf/Main.lean new file mode 100644 index 0000000..622cff6 --- /dev/null +++ b/Proofs/Ixdtf/Main.lean @@ -0,0 +1,245 @@ +/- + The IXDTF statements of `Spec.lean`, under the same names, from the + lemmas in the other files of `Proofs/Ixdtf/`. The test vectors are + checked by evaluation. +-/ + +import Proofs.Ixdtf.Parse +import Proofs.Ixdtf.Rules + +open Rfc3339 + +theorem Spec.parseExt_iff (s : String) (e : Ext) : + parseExt s = some e ↔ + Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Spec.renderSuffix e ∧ + dt.map Spec.asciiUpper = Spec.render e.stamp := + Rfc3339.Proofs.Ixdtf.parseExt_iff s e + +theorem Spec.printExt_eq (e : Ext) (h : Spec.ExtValid e) : + e.print.toList = Spec.render e.stamp ++ Spec.renderSuffix e := + Rfc3339.Proofs.Ixdtf.printExt_eq e h + +theorem Spec.parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e := + Rfc3339.Proofs.Ixdtf.parseExt_print e h + +theorem Spec.parseExt_plain (s : String) (h : '[' ∉ s.toList) : + parseExt s = (parse s).map fun t => ⟨t, none, []⟩ := + Rfc3339.Proofs.Ixdtf.parseExt_plain s h + +theorem Spec.lookup_iff (e : Ext) (k : List Char) (t : Tag) : + e.lookup k = some t ↔ ∃ l r, e.tags = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k := + Rfc3339.Proofs.Ixdtf.lookup_iff e k t + +theorem Spec.erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Spec.MustReject p e := + Rfc3339.Proofs.Ixdtf.erroneous_iff p e + +/-- The grammar's checks on an IXDTF timestamp, made by the code's own + functions, which the lemmas of `Proofs/Ixdtf/Suffix.lean` tie to the + spec. Used to check the long test vectors without running the whole + parser in the kernel, which one of the external kernels cannot do in + its stack. -/ +def vx_validB (e : Ext) : Bool := + e.stamp.isValid && + (match e.zone with + | some (_, .name parts) => !parts.isEmpty && parts.all zonePartOK + | some (_, .offset o) => o != .z && o.isValid + | none => true) && + e.tags.all (fun t => keyOK t.key && !t.values.isEmpty && t.values.all valueOK) + +theorem vx_validB_sound (e : Ext) (h : vx_validB e = true) : Spec.ExtValid e := by + obtain ⟨stamp, zone, tags⟩ := e + simp only [vx_validB, Bool.and_eq_true, List.all_eq_true] at h + obtain ⟨⟨hs, hz⟩, ht⟩ := h + refine ⟨(Rfc3339.Proofs.Valid.isValid_iff stamp).mp hs, ?_, ?_⟩ + · intro c z hcz + subst hcz + cases z with + | name parts => + simp only [Bool.and_eq_true, Bool.not_eq_true', List.isEmpty_eq_false_iff, List.all_eq_true] at hz + exact ⟨hz.1, fun p hp => (Rfc3339.Proofs.Ixdtf.sx_zonePartOK_iff p).mp (hz.2 p hp)⟩ + | offset o => + simp only [Bool.and_eq_true, bne_iff_ne, ne_eq] at hz + exact ⟨hz.1, (Rfc3339.Proofs.Valid.offset_isValid_iff o).mp hz.2⟩ + · intro t htm + have h3 := ht t htm + simp only [Bool.not_eq_true', List.isEmpty_eq_false_iff] at h3 + exact ⟨(Rfc3339.Proofs.Ixdtf.sx_keyOK_iff _).mp h3.1.1, h3.1.2, + fun v hv => (Rfc3339.Proofs.Ixdtf.sx_valueOK_iff v).mp (h3.2 v hv)⟩ + +theorem vx_parseExt (s : String) (e : Ext) (dt : List Char) (hv : vx_validB e = true) + (hs : s.toList = dt ++ Spec.renderSuffix e) (hd : dt.map Spec.asciiUpper = Spec.render e.stamp) : + parseExt s = some e := + (Rfc3339.Proofs.Ixdtf.parseExt_iff s e).2 ⟨vx_validB_sound e hv, dt, hs, hd⟩ + +/-- Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, with + the application of `Spec.exampleProcessor`: each one is read, and is + erroneous exactly where the RFC says it must be treated so. Also + critical time zones that agree with the offset, a critical `-00:00` + zone that does not, and strings the grammar refuses. -/ +theorem Spec.ixdtf_vectors : + -- Section 4.2, Figures 4 to 7 + parseExt "1996-12-19T16:39:57-08:00" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, []⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, + some (false, .name ["America".toList, "Los_Angeles".toList]), []⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, + some (false, .name ["America".toList, "Los_Angeles".toList]), + [⟨false, "u-ca".toList, ["hebrew".toList]⟩]⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, + [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ ∧ + ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + -- An experiment the application does not take part in + ((parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + -- Section 1.2: an offset time zone + parseExt "2022-07-08T00:14:07+08:45[+08:45]" = + some ⟨⟨2022, 7, 8, 0, 14, 7, [], .plus 8 45⟩, some (false, .offset (.plus 8 45)), []⟩ ∧ + ((parseExt "2022-07-08T00:14:07+08:45[!+08:45]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + -- Section 3.3, elective: an inconsistent zone, the zones of the note, + -- an unknown key, repeated keys + ((parseExt "2022-07-08T00:14:07+01:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").bind (·.lookup "u-ca".toList) = + some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese]").bind (·.lookup "u-ca".toList) = + some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ + -- Section 3.3, critical: the four examples + ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][!u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + -- Section 3.4, Figures 1 and 2 + ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + -- Critical zones that agree with the offset, and a critical `-00:00` + -- zone, offset 0, under an offset of +01:00 + ((parseExt "1996-12-19T16:39:57-08:00[!America/Los_Angeles]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + -- `Z` in brackets is a zone name, not an offset + ((parseExt "2022-07-08T00:14:07Z[Z]").map (·.zone) = some (some (false, .name ["Z".toList]))) ∧ + -- Refused by the grammar: an empty item, `.` and `..`, an upper case + -- key, an empty value, a time zone after a tag, an offset out of range + parseExt "2022-07-08T00:14:07Z[]" = none ∧ + parseExt "2022-07-08T00:14:07Z[.]" = none ∧ + parseExt "2022-07-08T00:14:07Z[a/..]" = none ∧ + parseExt "2022-07-08T00:14:07Z[U-ca=x]" = none ∧ + parseExt "2022-07-08T00:14:07Z[u-ca=a--b]" = none ∧ + parseExt "2022-07-08T00:14:07Z[u-ca=x][Europe/Paris]" = none ∧ + parseExt "2022-07-08T00:14:07Z[+24:00]" = none := by + and_intros + · exact vx_parseExt "1996-12-19T16:39:57-08:00" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, none, []⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel) + · exact vx_parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, some (false, .name ["America".toList, "Los_Angeles".toList]), []⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel) + · exact vx_parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, some (false, .name ["America".toList, "Los_Angeles".toList]), [⟨false, "u-ca".toList, ["hebrew".toList]⟩]⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel) + · exact vx_parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, none, [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel) + · rw [vx_parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, some (false, .name ["America".toList, "Los_Angeles".toList]), []⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, some (false, .name ["America".toList, "Los_Angeles".toList]), [⟨false, "u-ca".toList, ["hebrew".toList]⟩]⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, none, [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · exact vx_parseExt "2022-07-08T00:14:07+08:45[+08:45]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 8 45)⟩, some (false, .offset (.plus 8 45)), []⟩ + "2022-07-08T00:14:07+08:45".toList (by decide +kernel) (by decide +kernel) (by decide +kernel) + · rw [vx_parseExt "2022-07-08T00:14:07+08:45[!+08:45]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 8 45)⟩, some (true, .offset (.plus 8 45)), []⟩ + "2022-07-08T00:14:07+08:45".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07+01:00[Europe/Paris]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 1 0)⟩, some (false, .name ["Europe".toList, "Paris".toList]), []⟩ + "2022-07-08T00:14:07+01:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[Europe/Paris]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, some (false, .name ["Europe".toList, "Paris".toList]), []⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]" ⟨⟨2022, 7, 8, 2, 14, 7, [], (.plus 2 0)⟩, some (false, .name ["Europe".toList, "Paris".toList]), []⟩ + "2022-07-08T02:14:07+02:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07+01:00[knort=blargel]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 1 0)⟩, none, [⟨false, "knort".toList, ["blargel".toList]⟩]⟩ + "2022-07-08T00:14:07+01:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨false, "u-ca".toList, ["chinese".toList]⟩, ⟨false, "u-ca".toList, ["japanese".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨false, "u-ca".toList, ["chinese".toList]⟩, ⟨false, "u-ca".toList, ["japanese".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[u-ca=chinese]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨false, "u-ca".toList, ["chinese".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 1 0)⟩, some (true, .name ["Europe".toList, "Paris".toList]), []⟩ + "2022-07-08T00:14:07+01:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨true, "u-ca".toList, ["chinese".toList]⟩, ⟨false, "u-ca".toList, ["japanese".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[u-ca=chinese][!u-ca=japanese]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨false, "u-ca".toList, ["chinese".toList]⟩, ⟨true, "u-ca".toList, ["japanese".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[!knort=blargel]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, none, [⟨true, "knort".toList, ["blargel".toList]⟩]⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07+00:00[!Europe/London]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 0 0)⟩, some (true, .name ["Europe".toList, "London".toList]), []⟩ + "2022-07-08T00:14:07+00:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07+00:00[Europe/London]" ⟨⟨2022, 7, 8, 0, 14, 7, [], (.plus 0 0)⟩, some (false, .name ["Europe".toList, "London".toList]), []⟩ + "2022-07-08T00:14:07+00:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[!Europe/London]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, some (true, .name ["Europe".toList, "London".toList]), []⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[Europe/London]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, some (false, .name ["Europe".toList, "London".toList]), []⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "1996-12-19T16:39:57-08:00[!America/Los_Angeles]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, some (true, .name ["America".toList, "Los_Angeles".toList]), []⟩ + "1996-12-19T16:39:57-08:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]" ⟨⟨2022, 7, 8, 2, 14, 7, [], (.plus 2 0)⟩, some (true, .name ["Europe".toList, "Paris".toList]), []⟩ + "2022-07-08T02:14:07+02:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T01:14:07+01:00[!-00:00]" ⟨⟨2022, 7, 8, 1, 14, 7, [], (.plus 1 0)⟩, some (true, .offset (.minus 0 0)), []⟩ + "2022-07-08T01:14:07+01:00".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · rw [vx_parseExt "2022-07-08T00:14:07Z[Z]" ⟨⟨2022, 7, 8, 0, 14, 7, [], .z⟩, some (false, .name ["Z".toList]), []⟩ + "2022-07-08T00:14:07Z".toList (by decide +kernel) (by decide +kernel) (by decide +kernel)] + decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel diff --git a/Proofs/Ixdtf/Parse.lean b/Proofs/Ixdtf/Parse.lean new file mode 100644 index 0000000..85cb4c3 --- /dev/null +++ b/Proofs/Ixdtf/Parse.lean @@ -0,0 +1,118 @@ +/- + `parseExt` and `Ext.print` against the grammar. +-/ + +import Proofs.Ixdtf.Suffix +import Proofs.Main + +open Rfc3339 + +namespace Rfc3339.Proofs.Ixdtf + +theorem px_digitChar_lt (n : Nat) : (Spec.digitChar n).toNat < 91 := by + unfold Spec.digitChar + rcases Nat.lt_or_ge n 10 with h | h + · have : ∀ i : Fin 10, ("0123456789".toList.getD i.val '?').toNat < 91 := by decide + exact this ⟨n, h⟩ + · obtain ⟨k, rfl⟩ : ∃ k, n = k + 10 := ⟨n - 10, by omega⟩ + simp [List.getD_eq_getElem?_getD] + +theorem px_digits_lt (k n : Nat) : ∀ c ∈ Spec.digits k n, c.toNat < 91 := by + intro c hc + simp only [Spec.digits, List.mem_map] at hc + obtain ⟨_, _, rfl⟩ := hc + exact px_digitChar_lt _ + +theorem px_renderOffset_lt (o : Offset) : ∀ c ∈ Spec.renderOffset o, c.toNat < 91 := 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⟩, px_digits_lt _ _⟩, ⟨by decide, by simp⟩⟩, px_digits_lt _ _⟩ + +theorem px_render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 91 := by + simp only [Spec.render, List.forall_mem_append, List.forall_mem_cons] + and_intros + all_goals first + | exact px_digits_lt _ _ + | exact px_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 _ _ => px_digitChar_lt _⟩ + +/-- A list whose upper case is a rendered timestamp has no `[`. -/ +theorem px_no_bracket {dt : List Char} {t : Timestamp} + (h : dt.map Spec.asciiUpper = Spec.render t) : ∀ c ∈ dt, c ≠ '[' := by + intro c hc hb + subst hb + have hm : Spec.asciiUpper '[' ∈ Spec.render t := h ▸ List.mem_map_of_mem hc + have : Spec.asciiUpper '[' = '[' := by decide + rw [this] at hm + have := px_render_lt t _ hm + simp at this + +theorem px_takeWhile_split {dt r : List Char} (hd : ∀ c ∈ dt, c ≠ '[') + (hr : r = [] ∨ r.head? = some '[') : + (dt ++ r).takeWhile (fun x => decide (x ≠ '[')) = dt := by + rw [List.takeWhile_append_of_pos (by simpa using hd)] + rcases hr with rfl | hr + · simp + · match r, hr with + | _ :: _, hr => + simp only [List.head?_cons, Option.some.injEq] at hr + subst hr + simp + +theorem parseExt_iff (s : String) (e : Ext) : + parseExt s = some e ↔ + Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Spec.renderSuffix e ∧ + dt.map Spec.asciiUpper = Spec.render e.stamp := by + constructor + · intro h + simp only [parseExt, bind, Option.bind_eq_some_iff] at h + obtain ⟨t, ht, ⟨zone, tags⟩, hs, he⟩ := h + simp only [pure, Option.some.injEq] at he + subst he + obtain ⟨hv, hu⟩ := (Spec.parse_iff _ t).mp ht + rw [String.toList_ofList] at hu + obtain ⟨⟨hz, htags⟩, hsuf⟩ := + (parseSuffix_iff _ ⟨t, zone, tags⟩).mp hs + refine ⟨⟨hv, hz, htags⟩, _, ?_, hu⟩ + obtain ⟨r, hr⟩ := List.takeWhile_prefix (fun x => decide (x ≠ '[')) (l := s.toList) + rw [← hsuf] + generalize s.toList.takeWhile (fun x => decide (x ≠ '[')) = tw at hr ⊢ + rw [← hr, List.drop_left] + · rintro ⟨⟨hv, hz, htags⟩, dt, hs, hu⟩ + have htw : s.toList.takeWhile (fun x => decide (x ≠ '[')) = dt := by + rw [hs]; exact px_takeWhile_split (px_no_bracket hu) (renderSuffix_head e) + have hp : parse (String.ofList dt) = some e.stamp := + (Spec.parse_iff _ _).mpr ⟨hv, by rw [String.toList_ofList]; exact hu⟩ + have hsuf : parseSuffix (Spec.renderSuffix e) = some (e.zone, e.tags) := + (parseSuffix_iff _ e).mpr ⟨⟨hz, htags⟩, rfl⟩ + simp only [parseExt, htw, hp] + rw [hs, List.drop_left, hsuf] + rfl + +theorem printExt_eq (e : Ext) (h : Spec.ExtValid e) : + e.print.toList = Spec.render e.stamp ++ Spec.renderSuffix e := by + rw [Ext.print, String.toList_ofList, + Format.render_eq _ ((Spec.isValid_iff _).mpr h.1), renderSuffix_eq e h.2.1] + +theorem parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e := + (parseExt_iff _ e).mpr ⟨h, Spec.render e.stamp, printExt_eq e h, Main.upper_render _⟩ + +theorem parseExt_plain (s : String) (h : '[' ∉ s.toList) : + parseExt s = (parse s).map fun t => ⟨t, none, []⟩ := by + have htw : s.toList.takeWhile (fun x => decide (x ≠ '[')) = s.toList := by + have := px_takeWhile_split (dt := s.toList) (r := []) + (fun c hc hb => h (hb ▸ hc)) (Or.inl rfl) + simpa using this + simp only [parseExt, htw, String.ofList_toList, List.drop_length] + cases parse s <;> rfl + +end Rfc3339.Proofs.Ixdtf diff --git a/Proofs/Ixdtf/Rules.lean b/Proofs/Ixdtf/Rules.lean new file mode 100644 index 0000000..11205f9 --- /dev/null +++ b/Proofs/Ixdtf/Rules.lean @@ -0,0 +1,89 @@ +/- + `Ext.lookup` and `Ext.erroneous` against sections 3.2 to 3.4. +-/ + +import Rfc3339 +import Spec.Ixdtf +import Proofs.Valid + +open Rfc3339 + +namespace Rfc3339.Proofs.Ixdtf + +private theorem rx_find_iff (k : List Char) (t : Tag) : ∀ (ts : List Tag), + ts.find? (fun u => u.key == k) = some t ↔ ∃ l r, ts = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k + | [] => by simp + | u :: us => by + rw [List.find?_cons] + by_cases h : u.key = k + · simp only [h, beq_self_eq_true, Option.some.injEq] + constructor + · rintro rfl + exact ⟨[], us, by simp, h, by simp⟩ + · rintro ⟨l, r, hl, hk, hu⟩ + cases l with + | nil => simp at hl; exact hl.1 + | cons a l => + simp at hl + exact absurd (hl.1 ▸ h) (hu a (by simp)) + · have hb : (u.key == k) = false := by simpa using h + rw [hb] + simp only + rw [rx_find_iff k t us] + constructor + · rintro ⟨l, r, hl, hk, hu⟩ + refine ⟨u :: l, r, by simp [hl], hk, ?_⟩ + intro v hv + simp at hv + rcases hv with rfl | hv + · exact h + · exact hu v hv + · rintro ⟨l, r, hl, hk, hu⟩ + cases l with + | nil => + simp at hl + exact absurd (hl.1 ▸ hk) h + | cons a l => + simp at hl + exact ⟨l, r, hl.2, hk, fun v hv => hu v (by simp [hv])⟩ + +theorem lookup_iff (e : Ext) (k : List Char) (t : Tag) : + e.lookup k = some t ↔ ∃ l r, e.tags = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k := by + exact rx_find_iff k t e.tags + + +private theorem rx_assertsOffset_iff (o : Offset) : assertsOffset o = true ↔ Spec.AssertsOffset o := by + cases o with + | z => simp [assertsOffset, Spec.AssertsOffset] + | plus h m => simp [assertsOffset, Spec.AssertsOffset] + | minus h m => + by_cases hh : h = 0 <;> by_cases hm : m = 0 <;> subst_vars <;> + simp_all [assertsOffset, Spec.AssertsOffset] + +private theorem rx_zoneAgrees_iff (p : Processor) (t : Timestamp) (z : Zone) : + zoneAgrees p t z = true ↔ Spec.ZoneConsistent p t z := by + cases z with + | offset o => + simp only [zoneAgrees, Spec.ZoneConsistent, Bool.or_eq_true, Bool.not_eq_true', beq_iff_eq, + Rfc3339.Proofs.Valid.offsetMinutes_eq, ← rx_assertsOffset_iff] + cases assertsOffset t.offset <;> simp + | name parts => + simp only [zoneAgrees, Spec.ZoneConsistent] + cases hz : p.zoneOffset parts t with + | none => simp + | some m => + simp only [Bool.or_eq_true, Bool.not_eq_true', beq_iff_eq, Rfc3339.Proofs.Valid.offsetMinutes_eq, + ← rx_assertsOffset_iff, Option.some.injEq, exists_eq_left'] + cases assertsOffset t.offset <;> simp + +theorem erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Spec.MustReject p e := by + simp only [Ext.erroneous, Spec.MustReject, Bool.or_eq_true, List.any_eq_true, + Bool.and_eq_true, Bool.not_eq_true', beq_iff_eq, bne_iff_ne, ne_eq, or_assoc] + apply or_congr _ Iff.rfl + rcases h : e.zone with _ | ⟨_ | _, z⟩ + · simp + · simp + · simp [← rx_zoneAgrees_iff] + +end Rfc3339.Proofs.Ixdtf diff --git a/Proofs/Ixdtf/Suffix.lean b/Proofs/Ixdtf/Suffix.lean new file mode 100644 index 0000000..f3a5ad5 --- /dev/null +++ b/Proofs/Ixdtf/Suffix.lean @@ -0,0 +1,609 @@ +/- + The suffix parser against the grammar of RFC 9557, section 4.1. +-/ + +import Rfc3339 +import Spec.Ixdtf +import Proofs.Format +import Proofs.Valid + +open Rfc3339 + +namespace Rfc3339.Proofs.Ixdtf + +/-! ## Characters -/ + +theorem sx_alpha_ne {c : Char} (h : Spec.Alpha c) : + c ≠ ']' ∧ c ≠ '=' ∧ c ≠ '/' ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by + unfold Spec.Alpha at h + refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> rintro rfl <;> revert h <;> decide + +theorem sx_digit_ne {c : Char} (h : Spec.Digit c) : + c ≠ ']' ∧ c ≠ '=' ∧ c ≠ '/' ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by + unfold Spec.Digit at h + refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> rintro rfl <;> revert h <;> decide + +theorem sx_lower_ne {c : Char} (h : 'a' ≤ c ∧ c ≤ 'z') : + c ≠ ']' ∧ c ≠ '=' ∧ c ≠ '/' ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by + refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> rintro rfl <;> revert h <;> decide + +theorem sx_zonePart_chars {p : List Char} (hp : Spec.ZonePart p) : + ∀ x ∈ p, x ≠ ']' ∧ x ≠ '=' ∧ x ≠ '/' := by + obtain ⟨c, cs, rfl, hc, hcs, -, -⟩ := hp + intro x hx + rcases List.mem_cons.mp hx with rfl | hx + · rcases hc with h | rfl | rfl + · have := sx_alpha_ne h; exact ⟨this.1, this.2.1, this.2.2.1⟩ + all_goals decide + · rcases hcs x hx with h | rfl | rfl | h | rfl | rfl + · have := sx_alpha_ne h; exact ⟨this.1, this.2.1, this.2.2.1⟩ + · decide + · decide + · have := sx_digit_ne h; exact ⟨this.1, this.2.1, this.2.2.1⟩ + all_goals decide + +theorem sx_zonePart_head {p : List Char} (hp : Spec.ZonePart p) : + ∃ c cs, p = c :: cs ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by + obtain ⟨c, cs, rfl, hc, -, -, -⟩ := hp + refine ⟨c, cs, rfl, ?_⟩ + rcases hc with h | rfl | rfl + · have := sx_alpha_ne h; exact ⟨this.2.2.2.1, this.2.2.2.2.1, this.2.2.2.2.2⟩ + all_goals decide + +theorem sx_key_chars {k : List Char} (hk : Spec.SuffixKey k) : ∀ x ∈ k, x ≠ ']' ∧ x ≠ '=' := by + obtain ⟨c, cs, rfl, hc, hcs⟩ := hk + intro x hx + rcases List.mem_cons.mp hx with rfl | hx + · rcases hc with h | rfl + · have := sx_lower_ne h; exact ⟨this.1, this.2.1⟩ + · decide + · rcases hcs x hx with h | rfl | h | rfl + · have := sx_lower_ne h; exact ⟨this.1, this.2.1⟩ + · decide + · have := sx_digit_ne h; exact ⟨this.1, this.2.1⟩ + · decide + +theorem sx_key_head {k : List Char} (hk : Spec.SuffixKey k) : ∃ c cs, k = c :: cs ∧ c ≠ '!' := by + obtain ⟨c, cs, rfl, hc, -⟩ := hk + refine ⟨c, cs, rfl, ?_⟩ + rcases hc with h | rfl + · exact (sx_lower_ne h).2.2.2.1 + · decide + +theorem sx_value_chars {v : List Char} (hv : Spec.SuffixValue v) : + ∀ x ∈ v, x ≠ ']' ∧ x ≠ '=' ∧ x ≠ '-' := by + intro x hx + rcases hv.2 x hx with h | h + · have := sx_alpha_ne h; exact ⟨this.1, this.2.1, this.2.2.2.2.2⟩ + · have := sx_digit_ne h; exact ⟨this.1, this.2.1, this.2.2.2.2.2⟩ + +theorem sx_alpha_iff (c : Char) : isAlpha c = true ↔ Spec.Alpha c := by + simp [isAlpha, Spec.Alpha] +theorem sx_digit_iff (c : Char) : isDigitChar c = true ↔ Spec.Digit c := by + simp [isDigitChar, Spec.Digit] +theorem sx_keyOK_iff (k : List Char) : keyOK k = true ↔ Spec.SuffixKey k := by + cases k with + | nil => simp [keyOK, Spec.SuffixKey] + | cons c cs => + simp only [keyOK, Spec.SuffixKey, sx_digit_iff, Bool.and_eq_true, Bool.or_eq_true, List.all_eq_true, beq_iff_eq, decide_eq_true_eq, List.cons.injEq] + grind +theorem sx_valueOK_iff (v : List Char) : valueOK v = true ↔ Spec.SuffixValue v := by + simp only [valueOK, Spec.SuffixValue, sx_digit_iff, sx_alpha_iff, Bool.and_eq_true, Bool.or_eq_true, List.all_eq_true, Bool.not_eq_true', List.isEmpty_eq_false_iff, ne_eq] +theorem sx_drop_takeWhile (p : α → Bool) (xs : List α) : xs.drop (xs.takeWhile p).length = xs.dropWhile p := by + induction xs with + | nil => rfl + | cons x xs ih => + simp only [List.takeWhile_cons, List.dropWhile_cons] + cases p x <;> simp [ih] +theorem sx_takeWhile_append {p : α → Bool} (xs : List α) (y : α) (ys : List α) + (hx : ∀ x ∈ xs, p x = true) (hy : p y = false) : (xs ++ y :: ys).takeWhile p = xs := by + induction xs with + | nil => simp [hy] + | cons x xs ih => + simp only [List.cons_append, List.takeWhile_cons, hx x (by simp), ↓reduceIte] + rw [ih (fun z hz => hx z (by simp [hz]))] +theorem sx_digitChar_mem (n : Nat) : Spec.digitChar n ∈ "0123456789?".toList := by + unfold Spec.digitChar + rw [List.getD_eq_getElem?_getD] + cases h : "0123456789".toList[n]? with + | none => decide + | some x => + have := List.mem_of_getElem? h + simp only [Option.getD_some] + revert this; generalize x = y; revert y; decide +theorem sx_digits_mem {k n : Nat} {c : Char} (h : c ∈ Spec.digits k n) : c ∈ "0123456789?".toList := by + unfold Spec.digits at h + simp only [List.mem_map] at h + obtain ⟨i, _, rfl⟩ := h + exact sx_digitChar_mem _ +theorem sx_mem_join {α : Type} {s : List α} {ls : List (List α)} {x : α} + (h : x ∈ (ls.intersperse s).flatten) : x ∈ s ∨ ∃ l ∈ ls, x ∈ l := by + induction ls with + | nil => simp at h + | cons a tl ih => + cases tl with + | nil => exact Or.inr ⟨a, by simp, by simpa using h⟩ + | cons b rest => + rw [List.intersperse_cons_cons, List.flatten_cons, List.flatten_cons, List.mem_append, + List.mem_append] at h + rcases h with h | h | h + · exact Or.inr ⟨a, by simp, h⟩ + · exact Or.inl h + · rcases ih h with h' | ⟨l, hl, hx⟩ + · exact Or.inl h' + · exact Or.inr ⟨l, List.mem_cons_of_mem _ hl, hx⟩ + +theorem sx_join_cons {α : Type} (s p : List α) (rest : List (List α)) : + ∃ X, ((p :: rest).intersperse s).flatten = p ++ X := by + cases rest with + | nil => exact ⟨[], by simp⟩ + | cons b rest => exact ⟨_, by rw [List.intersperse_cons_cons, List.flatten_cons]⟩ + +theorem sx_intercalate_eq {α : Type} (s : List α) (ls : List (List α)) : + s.intercalate ls = (ls.intersperse s).flatten := rfl + +theorem sx_zonePartOK_iff (p : List Char) : zonePartOK p = true ↔ Spec.ZonePart p := by + cases p with + | nil => simp [zonePartOK, Spec.ZonePart] + | cons c cs => + simp only [zonePartOK, Spec.ZonePart, sx_alpha_iff, sx_digit_iff, Bool.and_eq_true, + Bool.or_eq_true, List.all_eq_true, beq_iff_eq, bne_iff_ne, ne_eq, List.cons.injEq] + grind + +/-- The body of a tag item, after the flag. -/ +def sx_tagBody (t : Tag) : List Char := t.key ++ ['='] ++ (t.values.intersperse ['-']).flatten + +/-- An item: brackets around the flag and the body. -/ +def sx_item (c : Bool) (b : List Char) : List Char := ['['] ++ Spec.renderFlag c ++ b ++ [']'] + +theorem sx_parseTag_sound {c : Bool} {b : List Char} {t : Tag} (h : parseTag c b = some t) : + Spec.TagValid t ∧ t.critical = c ∧ b = sx_tagBody t := by + unfold parseTag at h + have hb := (sx_drop_takeWhile (fun x => decide (x ≠ '=')) b).symm ▸ + (List.takeWhile_append_dropWhile (p := fun x => decide (x ≠ '=')) (l := b)) + dsimp only at h + split at h + · rename_i vs hvs + split at h + · rename_i hok + injection h with h + subst h + simp only [Bool.and_eq_true, List.all_eq_true, sx_keyOK_iff, sx_valueOK_iff] at hok + refine ⟨⟨hok.1, List.splitOn_ne_nil _ _, hok.2⟩, rfl, ?_⟩ + rw [hvs] at hb + simp only [sx_tagBody, ← sx_intercalate_eq, List.intercalate_splitOn] + rw [List.append_assoc, List.singleton_append] + exact hb.symm + · simp at h + · simp at h + +theorem sx_parseTag_render {t : Tag} (h : Spec.TagValid t) : + parseTag t.critical (sx_tagBody t) = some t := by + obtain ⟨hk, hne, hv⟩ := h + have hkey : (sx_tagBody t).takeWhile (fun x => decide (x ≠ '=')) = t.key := by + unfold sx_tagBody + rw [List.append_assoc, List.singleton_append] + exact sx_takeWhile_append _ _ _ (fun x hx => by simpa using (sx_key_chars hk x hx).2) + (by simp) + unfold parseTag + simp only [hkey] + unfold sx_tagBody + rw [List.append_assoc, List.drop_left, List.singleton_append] + simp only + rw [← sx_intercalate_eq, List.splitOn_intercalate _ (fun l hl => by + intro hm; exact (sx_value_chars (hv l hl) _ hm).2.2 rfl) hne] + have hkok : keyOK t.key = true := (sx_keyOK_iff _).mpr hk + have hvok : t.values.all valueOK = true := List.all_eq_true.mpr fun v hv' => (sx_valueOK_iff v).mpr (hv v hv') + simp [hkok, hvok] + +theorem sx_parseZone_sound {b : List Char} {z : Zone} (h : parseZone b = some z) : + Spec.ZoneValid z ∧ b = Spec.renderZone z := by + unfold parseZone at h + split at h + · rename_i x + split at h + · rename_i o ho + split at h + · rename_i hvo + injection h with h + subst h + have hb := Rfc3339.Proofs.Format.parseOffset_spec ho + refine ⟨⟨?_, (Rfc3339.Proofs.Valid.offset_isValid_iff o).mp hvo⟩, ?_⟩ + · rintro rfl; simp [Offset.render] at hb + · rw [hb]; exact Rfc3339.Proofs.Format.offset_render_eq o + · simp at h + · simp at h + · rename_i x + split at h + · rename_i o ho + split at h + · rename_i hvo + injection h with h + subst h + have hb := Rfc3339.Proofs.Format.parseOffset_spec ho + refine ⟨⟨?_, (Rfc3339.Proofs.Valid.offset_isValid_iff o).mp hvo⟩, ?_⟩ + · rintro rfl; simp [Offset.render] at hb + · rw [hb]; exact Rfc3339.Proofs.Format.offset_render_eq o + · simp at h + · simp at h + · dsimp only at h + split at h + · rename_i hall + injection h with h + subst h + refine ⟨⟨List.splitOn_ne_nil _ _, fun p hp => (sx_zonePartOK_iff p).mp (List.all_eq_true.mp hall p hp)⟩, ?_⟩ + show b = ((b.splitOn '/').intersperse ['/']).flatten + rw [← sx_intercalate_eq, List.intercalate_splitOn] + · simp at h + +theorem sx_parseZone_render {z : Zone} (h : Spec.ZoneValid z) : + parseZone (Spec.renderZone z) = some z := by + cases z with + | name parts => + obtain ⟨hne, hp⟩ := h + obtain ⟨p, rest, rfl⟩ := List.exists_cons_of_ne_nil hne + obtain ⟨c, cs, hpc, hc1, hc2, hc3⟩ := sx_zonePart_head (hp p (by simp)) + obtain ⟨X, hX⟩ := sx_join_cons ['/'] p rest + have hsplit : ((p :: rest).intersperse ['/']).flatten.splitOn '/' = p :: rest := by + rw [← sx_intercalate_eq] + exact List.splitOn_intercalate _ + (fun l hl hm => (sx_zonePart_chars (hp l hl) _ hm).2.2 rfl) (by simp) + have hall : (p :: rest).all zonePartOK = true := + List.all_eq_true.mpr fun l hl => (sx_zonePartOK_iff l).mpr (hp l hl) + show parseZone ((p :: rest).intersperse ['/']).flatten = _ + unfold parseZone + split + · rename_i x heq + rw [hX, hpc] at heq + simp at heq + exact absurd heq.1 hc2 + · rename_i x heq + rw [hX, hpc] at heq + simp at heq + exact absurd heq.1 hc3 + · simp only [hsplit, hall] + rfl + | offset o => + obtain ⟨hz, hv⟩ := h + have hvalid : o.isValid = true := (Rfc3339.Proofs.Valid.offset_isValid_iff o).mpr hv + have hr := Rfc3339.Proofs.Format.parseOffset_render o hvalid + show parseZone (Spec.renderOffset o) = _ + rw [← Rfc3339.Proofs.Format.offset_render_eq] + cases o with + | z => exact absurd rfl hz + | plus a m => + have hcons : (Offset.plus a m).render = '+' :: (pad2 a ++ ':' :: pad2 m) := rfl + rw [hcons] at hr ⊢ + unfold parseZone + simp only [hr, hvalid, ↓reduceIte] + | minus a m => + have hcons : (Offset.minus a m).render = '-' :: (pad2 a ++ ':' :: pad2 m) := rfl + rw [hcons] at hr ⊢ + unfold parseZone + simp only [hr, hvalid, ↓reduceIte] + + +theorem sx_digits_ne {k n : Nat} {c : Char} (h : c ∈ Spec.digits k n) : c ≠ ']' ∧ c ≠ '=' := by + have key : ∀ d ∈ "0123456789?".toList, d ≠ ']' ∧ d ≠ '=' := by decide + exact key c (sx_digits_mem h) + +theorem sx_tagBody_facts {t : Tag} (h : Spec.TagValid t) : + ']' ∉ sx_tagBody t ∧ (sx_tagBody t).head? ≠ some '!' ∧ '=' ∈ sx_tagBody t := by + obtain ⟨hk, hne, hv⟩ := h + refine ⟨?_, ?_, ?_⟩ + · unfold sx_tagBody + simp only [List.mem_append, not_or] + refine ⟨⟨fun hm => (sx_key_chars hk _ hm).1 rfl, by decide⟩, fun hm => ?_⟩ + rcases sx_mem_join hm with h | ⟨l, hl, hx⟩ + · simp at h + · exact (sx_value_chars (hv l hl) _ hx).1 rfl + · obtain ⟨c, cs, hkc, hc⟩ := sx_key_head hk + unfold sx_tagBody + rw [hkc] + simpa using hc + · unfold sx_tagBody + simp + +theorem sx_zoneBody_facts {z : Zone} (h : Spec.ZoneValid z) : + ']' ∉ Spec.renderZone z ∧ (Spec.renderZone z).head? ≠ some '!' ∧ '=' ∉ Spec.renderZone z := by + cases z with + | name parts => + obtain ⟨hne, hp⟩ := h + refine ⟨fun hm => ?_, ?_, fun hm => ?_⟩ + · rcases sx_mem_join hm with h | ⟨l, hl, hx⟩ + · simp at h + · exact (sx_zonePart_chars (hp l hl) _ hx).1 rfl + · obtain ⟨p, rest, rfl⟩ := List.exists_cons_of_ne_nil hne + obtain ⟨c, cs, hpc, hc1, -, -⟩ := sx_zonePart_head (hp p (by simp)) + obtain ⟨X, hX⟩ := sx_join_cons ['/'] p rest + show (((p :: rest).intersperse ['/']).flatten).head? ≠ _ + rw [hX, hpc] + simpa using hc1 + · rcases sx_mem_join hm with h | ⟨l, hl, hx⟩ + · simp at h + · exact (sx_zonePart_chars (hp l hl) _ hx).2.1 rfl + | offset o => + obtain ⟨hz, -⟩ := h + cases o with + | z => exact absurd rfl hz + | plus a m => + refine ⟨fun hm => ?_, by simp [Spec.renderZone, Spec.renderOffset], fun hm => ?_⟩ <;> + · simp only [Spec.renderZone, Spec.renderOffset, List.mem_append] at hm + rcases hm with ((h | h) | h) | h <;> + first + | exact absurd h (by decide) + | exact (sx_digits_ne h).1 rfl + | exact (sx_digits_ne h).2 rfl + | minus a m => + refine ⟨fun hm => ?_, by simp [Spec.renderZone, Spec.renderOffset], fun hm => ?_⟩ <;> + · simp only [Spec.renderZone, Spec.renderOffset, List.mem_append] at hm + rcases hm with ((h | h) | h) | h <;> + first + | exact absurd h (by decide) + | exact (sx_digits_ne h).1 rfl + | exact (sx_digits_ne h).2 rfl + +theorem sx_suffixItems_cons (f : Nat) (c : Bool) (b R : List Char) (hb : ']' ∉ b) + (hh : b.head? ≠ some '!') : + suffixItems (f + 1) (sx_item c b ++ R) = (suffixItems f R).map (fun tail => (c, b) :: tail) := by + have hB : ∀ x ∈ Spec.renderFlag c ++ b, decide (x ≠ ']') = true := by + intro x hx + simp only [decide_eq_true_eq] + rintro rfl + rcases List.mem_append.mp hx with h | h + · cases c <;> simp [Spec.renderFlag] at h + · exact hb h + have e1 : sx_item c b ++ R = '[' :: ((Spec.renderFlag c ++ b) ++ ']' :: R) := by simp [sx_item] + rw [e1] + simp only [suffixItems, ↓reduceIte] + rw [sx_takeWhile_append _ _ _ hB (by simp), List.drop_left] + simp only + cases c with + | true => + cases suffixItems f R <;> rfl + | false => + cases hs : suffixItems f R with + | none => rfl + | some tail => + simp only [Spec.renderFlag, Bool.false_eq_true, ↓reduceIte, List.nil_append, Option.map_some] + split + · simp at hh + · rfl + + +theorem sx_suffixItems_render (items : List (Bool × List Char)) (fuel : Nat) + (h : ∀ p ∈ items, ']' ∉ p.2 ∧ p.2.head? ≠ some '!') + (hf : (items.flatMap (fun p => sx_item p.1 p.2)).length ≤ fuel) : + suffixItems fuel (items.flatMap (fun p => sx_item p.1 p.2)) = some items := by + induction items generalizing fuel with + | nil => cases fuel <;> rfl + | cons p rest ih => + obtain ⟨c, b⟩ := p + simp only [List.flatMap_cons] at hf ⊢ + have hlen : (sx_item c b).length ≥ 2 := by simp [sx_item]; omega + simp only [List.length_append] at hf + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hp := h (c, b) (by simp) + rw [sx_suffixItems_cons f c b _ hp.1 hp.2, + ih f (fun q hq => h q (List.mem_cons_of_mem _ hq)) (by omega)] + rfl + +theorem sx_suffixItems_sound (fuel : Nat) (cs : List Char) (items : List (Bool × List Char)) + (h : suffixItems fuel cs = some items) : + cs = items.flatMap (fun p => sx_item p.1 p.2) := by + induction fuel generalizing cs items with + | zero => + cases cs with + | nil => + simp only [suffixItems, Option.some.injEq] at h + subst h; rfl + | cons c rest => simp [suffixItems] at h + | succ f ih => + cases cs with + | nil => + simp only [suffixItems, Option.some.injEq] at h + subst h; rfl + | cons c rest => + have hr := (sx_drop_takeWhile (fun x => decide (x ≠ ']')) rest).symm ▸ + (List.takeWhile_append_dropWhile (p := fun x => decide (x ≠ ']')) (l := rest)) + unfold suffixItems at h + split at h + · rename_i hc + subst hc + dsimp only at h + split at h + · rename_i more hmore + rw [hmore] at hr + obtain ⟨tail, ht, h2⟩ := Option.bind_eq_some_iff.mp h + clear h + have := ih more tail ht + subst this + split at h2 + · rename_i b hbody + simp only [pure, Option.some.injEq] at h2 + subst h2 + rw [hbody] at hr + subst hr + simp [sx_item, Spec.renderFlag] + · simp only [pure, Option.some.injEq] at h2 + subst h2 + obtain ⟨B, hB⟩ : ∃ B, List.takeWhile (fun x => decide (x ≠ ']')) rest = B := ⟨_, rfl⟩ + rw [hB] at hr ⊢ + subst hr + simp [sx_item, Spec.renderFlag] + · simp at h + · simp at h + + +theorem sx_mapM_sound (rest : List (Bool × List Char)) (tags : List Tag) + (h : rest.mapM (fun (c, b) => parseTag c b) = some tags) : + (∀ t ∈ tags, Spec.TagValid t) ∧ rest = tags.map (fun t => (t.critical, sx_tagBody t)) := by + induction rest generalizing tags with + | nil => + simp only [List.mapM_nil, pure, Option.some.injEq] at h + subst h + simp + | cons p rest ih => + obtain ⟨c, b⟩ := p + simp only [List.mapM_cons, bind, Option.bind_eq_some_iff, pure, Option.some.injEq] at h + obtain ⟨t, ht, ts, hts, rfl⟩ := h + obtain ⟨htv, rfl, rfl⟩ := sx_parseTag_sound ht + obtain ⟨hv, rfl⟩ := ih ts hts + refine ⟨?_, rfl⟩ + intro u hu + rcases List.mem_cons.mp hu with rfl | hu + · exact htv + · exact hv u hu + +theorem sx_mapM_render (tags : List Tag) (h : ∀ t ∈ tags, Spec.TagValid t) : + (tags.map (fun t => (t.critical, sx_tagBody t))).mapM (fun (c, b) => parseTag c b) = + some tags := by + induction tags with + | nil => rfl + | cons t ts ih => + simp only [List.map_cons, List.mapM_cons, sx_parseTag_render (h t (by simp)), + ih (fun u hu => h u (List.mem_cons_of_mem _ hu))] + rfl + +/-- The items of a suffix: the time zone, if any, then the tags. -/ +def sx_items (e : Ext) : List (Bool × List Char) := + (match e.zone with + | some (c, z) => [(c, Spec.renderZone z)] + | none => []) ++ e.tags.map (fun t => (t.critical, sx_tagBody t)) + +theorem sx_renderTag_eq (t : Tag) : Spec.renderTag t = sx_item t.critical (sx_tagBody t) := by + simp [Spec.renderTag, sx_item, sx_tagBody] + +theorem sx_renderSuffix_items (e : Ext) : + Spec.renderSuffix e = (sx_items e).flatMap (fun p => sx_item p.1 p.2) := by + obtain ⟨stamp, zone, tags⟩ := e + have htags : (tags.map Spec.renderTag).flatten = + (tags.map (fun t => (t.critical, sx_tagBody t))).flatMap (fun p => sx_item p.1 p.2) := by + induction tags with + | nil => rfl + | cons t ts ih => simp only [List.map_cons, List.flatten_cons, List.flatMap_cons, ih, sx_renderTag_eq] + rcases zone with _ | ⟨c, z⟩ + · simp only [Spec.renderSuffix, sx_items, List.nil_append, htags] + · simp only [Spec.renderSuffix, sx_items, htags, List.singleton_append, List.flatMap_cons, sx_item] + +theorem sx_items_facts (e : Ext) (hz : ∀ c z, e.zone = some (c, z) → Spec.ZoneValid z) + (ht : ∀ t ∈ e.tags, Spec.TagValid t) : + ∀ p ∈ sx_items e, ']' ∉ p.2 ∧ p.2.head? ≠ some '!' := by + obtain ⟨stamp, zone, tags⟩ := e + intro p hp + simp only [sx_items, List.mem_append, List.mem_map] at hp + rcases hp with hp | ⟨t, htm, rfl⟩ + · rcases zone with _ | ⟨c, z⟩ + · simp at hp + · simp only [List.mem_singleton] at hp + subst hp + have := sx_zoneBody_facts (hz c z rfl) + exact ⟨this.1, this.2.1⟩ + · have := sx_tagBody_facts (ht t htm) + exact ⟨this.1, this.2.1⟩ + +/-- `parseSuffix` reads exactly the suffixes of the grammar, as + `Spec.renderSuffix` writes them. -/ +theorem parseSuffix_iff (cs : List Char) (e : Ext) : + parseSuffix cs = some (e.zone, e.tags) ↔ + ((∀ c z, e.zone = some (c, z) → Spec.ZoneValid z) ∧ ∀ t ∈ e.tags, Spec.TagValid t) ∧ + cs = Spec.renderSuffix e := by + constructor + · intro h + unfold parseSuffix at h + obtain ⟨items, hitems, h2⟩ := Option.bind_eq_some_iff.mp h + clear h + have hcs := sx_suffixItems_sound _ _ _ hitems + clear hitems + subst hcs + rw [sx_renderSuffix_items] + obtain ⟨stamp, zone, tags⟩ := e + simp only at h2 ⊢ + match items, h2 with + | [], h => + simp only [pure, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + simp [sx_items] + | (crit, body) :: rest, h => + obtain ⟨tags', htags, h3⟩ := Option.bind_eq_some_iff.mp h + clear h + obtain ⟨hv', rfl⟩ := sx_mapM_sound rest tags' htags + split at h3 + · obtain ⟨t, ht, h⟩ := Option.bind_eq_some_iff.mp h3 + clear h3 + obtain ⟨htv, rfl, rfl⟩ := sx_parseTag_sound ht + simp only [pure, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨⟨by simp, ?_⟩, by simp [sx_items]⟩ + intro u hu + rcases List.mem_cons.mp hu with rfl | hu + · exact htv + · exact hv' u hu + · obtain ⟨z, hz, h⟩ := Option.bind_eq_some_iff.mp h3 + clear h3 + obtain ⟨hzv, rfl⟩ := sx_parseZone_sound hz + simp only [pure, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨⟨?_, hv'⟩, by simp [sx_items]⟩ + intro c z' hcz + simp only [Option.some.injEq, Prod.mk.injEq] at hcz + obtain ⟨rfl, rfl⟩ := hcz + exact hzv + · rintro ⟨⟨hz, ht⟩, rfl⟩ + have hf := sx_items_facts e hz ht + rw [sx_renderSuffix_items] + unfold parseSuffix + rw [sx_suffixItems_render _ _ hf (Nat.le_refl _)] + obtain ⟨stamp, zone, tags⟩ := e + simp only at hz ht ⊢ + rcases zone with _ | ⟨c, z⟩ + · cases tags with + | nil => rfl + | cons t ts => + have htv := ht t (by simp) + have hts : ∀ u ∈ ts, Spec.TagValid u := fun u hu => ht u (List.mem_cons_of_mem _ hu) + have hc : (sx_tagBody t).contains '=' = true := + List.contains_iff_mem.mpr (sx_tagBody_facts htv).2.2 + simp only [sx_items, List.nil_append, List.map_cons, Option.bind_eq_bind, Option.bind_some] + simp only [Option.bind_some, sx_mapM_render ts hts, hc, ↓reduceIte, sx_parseTag_render htv] + rfl + · have hzv := hz c z rfl + have hc : (Spec.renderZone z).contains '=' = false := by + cases h : (Spec.renderZone z).contains '=' with + | false => rfl + | true => exact absurd (List.contains_iff_mem.mp h) (sx_zoneBody_facts hzv).2.2 + simp only [sx_items, List.singleton_append] + simp only [bind, Option.bind_some, sx_mapM_render tags ht, hc, Bool.false_eq_true, ↓reduceIte, + sx_parseZone_render hzv] + rfl + +/-- The code's rendering of the suffix is the spec's. -/ +theorem renderSuffix_eq (e : Ext) (h : ∀ c z, e.zone = some (c, z) → Spec.ZoneValid z) : + e.renderSuffix = Spec.renderSuffix e := by + obtain ⟨stamp, zone, tags⟩ := e + have hz : ∀ z : Zone, z.render = Spec.renderZone z := by + intro z + cases z with + | name parts => rfl + | offset o => exact Rfc3339.Proofs.Format.offset_render_eq o + have ht : (Tag.render : Tag → List Char) = Spec.renderTag := funext fun t => rfl + simp only [Ext.renderSuffix, Spec.renderSuffix, List.flatMap_def, ht] + rcases zone with _ | ⟨c, z⟩ + · rfl + · simp only [hz] + rfl + +/-- A suffix of the grammar is empty or starts with `[`, and holds no + other `[` than at the start of each item; in particular a rendered + suffix starts with `[` when it is not empty. -/ +theorem renderSuffix_head (e : Ext) : + Spec.renderSuffix e = [] ∨ (Spec.renderSuffix e).head? = some '[' := by + obtain ⟨stamp, zone, tags⟩ := e + rcases zone with _ | ⟨c, z⟩ + · cases tags with + | nil => left; rfl + | cons t ts => right; simp [Spec.renderSuffix, Spec.renderTag] + · right + simp [Spec.renderSuffix] + +end Rfc3339.Proofs.Ixdtf diff --git a/README.md b/README.md index 484b59a..f461fb1 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # rfc: RFC 3339 timestamps, proved -This library reads, checks and writes RFC 3339 timestamps, such as `1985-04-12T23:20:50.52Z`, in Lean. Machine-checked proofs show that it accepts exactly the strings that the RFC's grammar and calendar rules allow, including the day ranges and leap years of the calendar. `isValid` has one relaxation: it accepts a leap second at the end of any month. `isValidKnown` is exact: it checks second 60 against the table of the 27 leap seconds there have been, as tzdata publishes it. The proofs also cover the round trip from text to value and back, the count of seconds since the Unix epoch, and the order of two timestamps by the instant they name. A count of SI seconds since 1972 gives each leap second its own number, so a round trip through it keeps a leap second, as one through Unix seconds cannot. TAI − UTC is also given, as 10 plus the leap seconds before the timestamp, and proved to agree with the table's own TAI − UTC column at every second from 1972 on but a leap second. The library is tested against Python's date and time code; `tests/TEST-RESULTS.md` has the record. +This library reads, checks and writes RFC 3339 timestamps, such as `1985-04-12T23:20:50.52Z`, in Lean. Machine-checked proofs show that it accepts exactly the strings that the RFC's grammar and calendar rules allow, including the day ranges and leap years of the calendar. `isValid` has one relaxation: it accepts a leap second at the end of any month. `isValidKnown` is exact: it checks second 60 against the table of the 27 leap seconds there have been, as tzdata publishes it. The proofs also cover the round trip from text to value and back, the count of seconds since the Unix epoch, and the order of two timestamps by the instant they name. A count of SI seconds since 1972 gives each leap second its own number, so a round trip through it keeps a leap second, as one through Unix seconds cannot. TAI − UTC is also given, as 10 plus the leap seconds before the timestamp, and proved to agree with the table's own TAI − UTC column at every second from 1972 on but a leap second. It also reads and writes the extended form of RFC 9557, which adds a time zone and tagged values after the timestamp, as in `1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]`. The proofs show that it accepts exactly that grammar, with RFC 3339 timestamps as `parse` reads them, and that it decides which strings an application must treat as erroneous by sections 3.2 to 3.4, given what the application can process. The library is tested against Python's date and time code and a Python copy of the RFC 9557 grammar; `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. @@ -25,12 +25,16 @@ For each timestamp it prints the timestamp as written, with `T` and `Z` in upper - `Timestamp.siSeconds` - `Timestamp.taiMinusUtc` - `Rfc3339.fromSiSeconds` +- `Rfc3339.parseExt` +- `Ext.print` +- `Ext.lookup` +- `Ext.erroneous` `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`; those for the leap second table, with the table itself, are in `Spec/Leap.lean`; and the types are in `Rfc3339/Types.lean`. The proofs are in `Proofs/`. +The statements are in `Spec.lean`. The definitions they use, written from the RFC, are in `Spec/Defs.lean`; those for the leap second table, with the table itself, are in `Spec/Leap.lean`; those for RFC 9557, with its grammar, are in `Spec/Ixdtf.lean`; and the types are in `Rfc3339/Types.lean` and `Rfc3339/IxdtfTypes.lean`. The proofs are in `Proofs/`. | Claim | Theorem | |-------|---------| @@ -55,21 +59,28 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF | `taiMinusUtc` is 10, and one more for each leap second of the table before the timestamp, so during a leap second it is still the value from before it. | `Spec.taiMinusUtc_leapsBefore` | | TAI − UTC at each second from 1972 on, other than a leap second, is the value in the table's second column, 10 to 37. The code never reads that column; it counts leap seconds. | `Spec.taiMinusUtc_eq` | | Section 5.8's leap seconds, the table's first and last, one seen from another offset, and second 60 in months that had none. SI seconds and TAI − UTC around the first and the last leap second. And the round trip that Unix seconds lose and SI seconds keep. | `Spec.leap_table_vectors` | +| `parseExt` reads exactly the strings of RFC 9557's `date-time-ext` rule, with one relaxation: an RFC 3339 timestamp, as `parse` reads it, so with second 60 at the end of any month, then a time zone, a name or a numeric offset, if there is one, and the tags, each perhaps marked critical with `!`. It returns the timestamp, the zone and the tags as written. | `Spec.parseExt_iff` | +| A valid IXDTF timestamp prints as the grammar writes it, and printing then parsing gives it back. | `Spec.printExt_eq`, `Spec.parseExt_print` | +| A string with no suffix reads as `parse` reads it, with no time zone and no tags. | `Spec.parseExt_plain` | +| `lookup` gives the first tag with a key, which section 3.3 has an application choose when an elective key is repeated. | `Spec.lookup_iff` | +| `erroneous` decides what sections 3.2 to 3.4 make an application treat as erroneous, for an application described by the tags it processes and the zone offsets it knows: a critical time zone it does not know or that disagrees with the offset, a critical tag it cannot process or whose key is repeated with other values, and an experimental key, one starting with `_`, it does not take part in. | `Spec.erroneous_iff` | +| Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, read and judged by an example application, as the RFC judges them. Critical time zones that agree with the offset, a critical `-00:00` zone that does not, and `[Z]` read as a zone name. Strings the grammar refuses: an empty item, `.` and `..` as zone parts, an upper case key, an empty value, a time zone after a tag, and an offset out of range. | `Spec.ixdtf_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, the decimal printing of numbers and reading of the numbers `fromunix` and `fromsi` take, and the layout of the `known` answer, with `-` for TAI − UTC before 1972. The differential tests cover them, with malformed requests and CR LF line endings. -- Whether a leap second was announced, in `isValid` and `parse`. They accept second 60 at 23:59 UTC at the end of any month, where section 5.7 allows it only at the end of months in which a leap second occurs; `isValidKnown` checks that against the table. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. +- Reading requests and printing answers in `Main.lean`: the hex decoding and UTF-8 check in `serve` mode, the arguments, output and exit codes of `check` mode, the decimal printing of numbers and reading of the numbers `fromunix` and `fromsi` take, the layout of the `known` answer, with `-` for TAI − UTC before 1972, and the layout of the `ixdtf` answer, which judges each string with the example application of `Spec.exampleProcessor`. The differential tests cover them, with malformed requests and CR LF line endings. +- Whether a leap second was announced, in `isValid`, `parse` and `parseExt`. They accept second 60 at 23:59 UTC at the end of any month, where section 5.7 allows it only at the end of months in which a leap second occurs; `isValidKnown` checks that against the table. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. - The table after its expiry date, 28 June 2027. `isValidKnown` refuses second 60 at any month end the table does not list, and `siSeconds` and `taiMinusUtc` count no leap second after 2016. If one is ever announced, the table in the spec and the code's list must change together, and the spec approved again. The table is what tzdata publishes from IERS Bulletin C; that it matches the IERS record is trusted, not proved. - SI seconds and TAI − UTC before 1972. UTC then ran on seconds of varying length, with TAI − UTC not a whole number of seconds. Before 1972, `Spec.siSeconds_eq` makes `siSeconds` Unix seconds less 63072000, 86400 to a day, which are not SI seconds there, and `taiMinusUtc` gives 10, which means nothing there; the tool's `known` request prints `-` for TAI − UTC. - The table itself. `Spec/Leap.lean` copies tzdata's `leap-seconds.list` (tzdata 2026e, updated through IERS Bulletin C, expiring 28 June 2027) line for line. That copy is part of the specification: the reviewer checks it against the file, and the differential tests check the code against the copy of the file on the test machine, but no proof does. - Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. `fromUnixSeconds` turns that number into the second after the leap second, so a round trip through Unix seconds loses a leap second, and `9999-12-31T23:59:60Z` gives `none`. -- Forms outside RFC 3339 are not supported, by design: +- Time zone rules. `parseExt` reads a time zone name by the grammar, but this library holds no time zone database: it does not know whether `Europe/Paris` exists or what its offset is. `erroneous` asks the application, through its `Processor`, for the offset a named zone has at an instant, and which tags it can process. What the application does with a tag, such as a calendar, is its own. +- RFC 9557's `time-zone` rule read literally. In ABNF, alternation binds more loosely than concatenation, so the rule as written reads `("[" critical-flag time-zone-name) / (time-numoffset "]")`. `Spec/Ixdtf.lean` follows the intent, which the RFC's note and every example show: a name or an offset between the brackets. +- Forms outside RFC 3339 and RFC 9557 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; + - other ISO 8601 forms, such as an offset with no colon in a time zone suffix; - years outside 0000 to 9999. - Speed. The code works on lists of characters, which suits proofs, not bulk data. @@ -96,6 +107,8 @@ This project has no dependencies beyond Lean itself. - Go accepts a comma before the fraction. - `rfc3339-validator` accepts a timestamp followed by a line break. +For RFC 9557, it compares `parseExt` with `Temporal.Instant.from` in Node's built-in Temporal, which is behind a flag and older than the current proposal. This Temporal refuses every critical flag, even on an item it acts on. It also refuses experimental and unknown keys, a repeated `u-ca`, and fractions finer than nanoseconds. Its older grammar also refuses a calendar with a part outside 3 to 8 characters, and a time zone name with a digit or `+`, other than the `Etc/GMT` forms, or with a part over 14 characters. It reads calendars and zone names it does not know. It accepts a few strings this project refuses, as RFC 9557 does, such as a zone offset with no colon and a stray `]`. + For leap seconds, it compares `siSeconds`, `taiMinusUtc` and `fromSiSeconds` with ERFA, a BSD-licensed C library derived from the IAU's SOFA, through pyerfa, which keeps its own leap second table. `tests/CROSS-CHECK.md` gives the counts. ## Re-check it @@ -115,10 +128,12 @@ The test script compares the tool with Python's `datetime` and `calendar` module ## Layout - `Rfc3339/Types.lean`: the timestamp and offset types. It is part of the specification. -- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`, `Rfc3339/FromUnix.lean`, `Rfc3339/Leap.lean`: the code under proof. +- `Rfc3339/IxdtfTypes.lean`: the RFC 9557 types, the time zone, the tags, and what an application can process. It is part of the specification. +- `Rfc3339/Calendar.lean`, `Rfc3339/Format.lean`, `Rfc3339/Instant.lean`, `Rfc3339/FromUnix.lean`, `Rfc3339/Leap.lean`, `Rfc3339/Ixdtf.lean`: the code under proof. - `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. - `Spec/Defs.lean`: the definitions the statements use, written from the RFC, with checks against its tables and known day counts. - `Spec/Leap.lean`: the leap second table, line for line from tzdata's `leap-seconds.list`, and the definitions the leap second statements use. +- `Spec/Ixdtf.lean`: RFC 9557's grammar, the rules for what an application must reject, and the example application. - `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. @@ -126,4 +141,4 @@ The test script compares the tool with Python's `datetime` and `calendar` module - `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. -- `tests/cross_check.py` and `tests/cross_check/main.go`: the one-off comparison with other parsers, and with ERFA for leap seconds. +- `tests/cross_check.py`, `tests/cross_check/main.go` and `tests/cross_check/ixdtf.js`: the one-off comparison with other parsers, with ERFA for leap seconds, and with Temporal for RFC 9557. diff --git a/Rfc3339.lean b/Rfc3339.lean index 70cee98..96ce4d0 100644 --- a/Rfc3339.lean +++ b/Rfc3339.lean @@ -9,3 +9,5 @@ import Rfc3339.Format import Rfc3339.Instant import Rfc3339.FromUnix import Rfc3339.Leap +import Rfc3339.IxdtfTypes +import Rfc3339.Ixdtf diff --git a/Rfc3339/Ixdtf.lean b/Rfc3339/Ixdtf.lean new file mode 100644 index 0000000..2a23618 --- /dev/null +++ b/Rfc3339/Ixdtf.lean @@ -0,0 +1,155 @@ +/- + RFC 9557, the Internet Extended Date/Time Format (IXDTF): reading and + writing the suffix, and the rules for elective and critical tags. +-/ + +import Rfc3339.IxdtfTypes +import Rfc3339.Format + +namespace Rfc3339 + +def isAlpha (c : Char) : Bool := ('A' ≤ c && c ≤ 'Z') || ('a' ≤ c && c ≤ 'z') + +def isDigitChar (c : Char) : Bool := '0' ≤ c && c ≤ '9' + +/-- `time-zone-part`: a letter, `.` or `_`, then letters, digits, `.`, + `_`, `-` and `+`; but not `.` or `..`. -/ +def zonePartOK : List Char → Bool + | [] => false + | c :: cs => + (isAlpha c || c == '.' || c == '_') && + cs.all (fun d => isAlpha d || isDigitChar d || d == '.' || d == '_' || d == '-' || d == '+') && + c :: cs != ['.'] && c :: cs != ['.', '.'] + +/-- `suffix-key`: a lower case letter or `_`, then lower case letters, + digits, `_` and `-`. -/ +def keyOK : List Char → Bool + | [] => false + | c :: cs => + (('a' ≤ c && c ≤ 'z') || c == '_') && + cs.all (fun d => ('a' ≤ d && d ≤ 'z') || d == '_' || isDigitChar d || d == '-') + +/-- `suffix-value`: one or more letters and digits. -/ +def valueOK (v : List Char) : Bool := !v.isEmpty && v.all (fun c => isAlpha c || isDigitChar c) + +/-- The body of a time zone item, after any `!`: a numeric offset, with + hours 00 to 23 and minutes 00 to 59, or a name. -/ +def parseZone (body : List Char) : Option Zone := + match body with + | '+' :: _ | '-' :: _ => + match parseOffset body with + | some o => if o.isValid then some (.offset o) else none + | none => none + | _ => + let parts := body.splitOn '/' + if parts.all zonePartOK then some (.name parts) else none + +/-- The body of a tag, after any `!`: the key, `=`, and the values, + separated by `-`. -/ +def parseTag (critical : Bool) (body : List Char) : Option Tag := + let key := body.takeWhile (· ≠ '=') + match body.drop key.length with + | '=' :: vs => + let values := vs.splitOn '-' + if keyOK key && values.all valueOK then some ⟨critical, key, values⟩ else none + | _ => none + +/-- The bracketed items of a suffix, each with its critical flag and its + body. Each item takes at least two characters, so `fuel` equal to + the length is enough. -/ +def suffixItems : Nat → List Char → Option (List (Bool × List Char)) + | _, [] => some [] + | 0, _ :: _ => none + | fuel + 1, c :: rest => + if c = '[' then + let body := rest.takeWhile (· ≠ ']') + match rest.drop body.length with + | ']' :: more => do + let tail ← suffixItems fuel more + match body with + | '!' :: b => pure ((true, b) :: tail) + | b => pure ((false, b) :: tail) + | _ => none + else none + +/-- Reads a suffix: a time zone first, if the first item has no `=`, + then tags. -/ +def parseSuffix (s : List Char) : Option (Option (Bool × Zone) × List Tag) := do + let items ← suffixItems s.length s + match items with + | [] => pure (none, []) + | (crit, body) :: rest => + let tags ← rest.mapM fun (c, b) => parseTag c b + if body.contains '=' then + let t ← parseTag crit body + pure (none, t :: tags) + else + let z ← parseZone body + pure (some (crit, z), tags) + +/-- Reads an IXDTF string: an RFC 3339 `date-time`, which `parse` reads, + then the suffix. The suffix starts at the first `[`. -/ +def parseExt (s : String) : Option Ext := do + let cs := s.toList + let dt := cs.takeWhile (· ≠ '[') + let stamp ← parse (String.ofList dt) + let (zone, tags) ← parseSuffix (cs.drop dt.length) + pure ⟨stamp, zone, tags⟩ + +/-- The critical flag. -/ +def renderFlag (critical : Bool) : List Char := if critical then ['!'] else [] + +def Zone.render : Zone → List Char + | .name parts => ['/'].intercalate parts + | .offset o => o.render + +def Tag.render (t : Tag) : List Char := + ['['] ++ renderFlag t.critical ++ t.key ++ ['='] ++ ['-'].intercalate t.values ++ [']'] + +/-- The suffix: the time zone, then the tags. -/ +def Ext.renderSuffix (e : Ext) : List Char := + (match e.zone with + | some (c, z) => ['['] ++ renderFlag c ++ z.render ++ [']'] + | none => []) ++ + e.tags.flatMap Tag.render + +/-- The IXDTF string, with `T` and `Z` in upper case. -/ +def Ext.print (e : Ext) : String := String.ofList (e.stamp.render ++ e.renderSuffix) + +/-- The first tag with the key: section 3.3 has an application that does + not handle a repeated elective key choose the first. -/ +def Ext.lookup (e : Ext) (key : List Char) : Option Tag := + e.tags.find? (·.key == key) + +/-- Whether the timestamp's offset asserts a local offset. Section 2 + makes `Z` mean the same as `-00:00`: the time in UTC is known, the + local offset is not. -/ +def assertsOffset : Offset → Bool + | .z => false + | .minus 0 0 => false + | _ => true + +/-- Whether the time zone agrees with the timestamp, for section 3.4: + the zone is known, and if the timestamp asserts a local offset, the + zone has that offset at that instant. -/ +def zoneAgrees (p : Processor) (t : Timestamp) : Zone → Bool + | .offset o => !assertsOffset t.offset || offsetMinutes o == offsetMinutes t.offset + | .name parts => + match p.zoneOffset parts t with + | some m => !assertsOffset t.offset || m == offsetMinutes t.offset + | none => false + +/-- Whether an application must treat the string as erroneous, by + sections 3.2 to 3.4: a critical time zone that is unknown or does not + agree with the offset; a critical tag it cannot process; a critical + tag whose key another tag gives other values; or an experimental + key, starting with `_`, that it does not take part in. -/ +def Ext.erroneous (p : Processor) (e : Ext) : Bool := + (match e.zone with + | some (true, z) => !zoneAgrees p e.stamp z + | _ => false) || + e.tags.any (fun t => t.critical && !p.processes t) || + e.tags.any (fun t => t.critical && e.tags.any fun u => u.key == t.key && u.values != t.values) || + e.tags.any (fun t => t.key.head? == some '_' && !p.processes t) + +end Rfc3339 diff --git a/Rfc3339/IxdtfTypes.lean b/Rfc3339/IxdtfTypes.lean new file mode 100644 index 0000000..c28c76c --- /dev/null +++ b/Rfc3339/IxdtfTypes.lean @@ -0,0 +1,43 @@ +/- + What an RFC 9557 (IXDTF) timestamp is: an RFC 3339 timestamp, then a + time zone and tags in brackets. Part of the approved specification, + with `Spec.lean` and `Spec/Ixdtf.lean`, since the IXDTF statements are + about these types. +-/ + +import Rfc3339.Types + +namespace Rfc3339 + +/-- The time zone in a suffix: a time zone name, kept as the parts + between its slashes, or a numeric offset (`time-numoffset`). -/ +inductive Zone where + | name (parts : List (List Char)) + | offset (o : Offset) + deriving DecidableEq, Repr + +/-- A suffix tag: whether it is marked critical with `!`, its key, and + its values, the parts between its hyphens. -/ +structure Tag where + critical : Bool + key : List Char + values : List (List Char) + deriving DecidableEq, Repr + +/-- An IXDTF timestamp: the RFC 3339 timestamp, the time zone if there + is one with whether it is critical, and the tags in order. -/ +structure Ext where + stamp : Timestamp + zone : Option (Bool × Zone) + tags : List Tag + deriving DecidableEq, Repr + +/-- What an application can act on, for the rules of sections 3.3 and + 3.4: the tags it can process, and for a time zone name, the offset in + minutes the zone has at a given instant, or `none` when it does not + know the zone. -/ +structure Processor where + processes : Tag → Bool + zoneOffset : List (List Char) → Timestamp → Option Int + +end Rfc3339 diff --git a/SPEC.md b/SPEC.md index 08736c3..839b401 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # 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. +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. It reads and writes the extended form of RFC 9557, with a time zone and tags after the timestamp. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `Rfc3339/Types.lean`, `Spec/Leap.lean`, `Spec/Ixdtf.lean`, `Rfc3339/IxdtfTypes.lean`, and the other files `bar.toml` lists. ## The format @@ -61,9 +61,38 @@ Section 5.7 allows second 60 only "at the end of months in which a leap second o Before 1972, UTC ran on seconds of varying length, with TAI − UTC not a whole number of seconds. There `siSeconds` is Unix seconds less 63072000, 86400 to a day, as `Spec.siSeconds_eq` says, which are not SI seconds, and `taiMinusUtc` gives 10, which means nothing. A leap second announced after the table's date would need a new table, in the spec and in the code, and a new approval. +## RFC 9557: time zones and tags + +RFC 9557, the Internet Extended Date/Time Format (IXDTF), updates RFC 3339. After the timestamp may come a suffix: a time zone in brackets, then tags in brackets. Each may be marked critical with `!`. An example is `1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]`. `Spec/Ixdtf.lean` quotes the grammar of section 4.1. + +- The time zone is a name or a numeric offset: + - A name is one or more parts joined by `/`. Each part starts with a letter, `.` or `_`, and goes on with letters, digits, `.`, `_`, `-` and `+`. It may not be `.` or `..`. + - An offset is RFC 3339's `+hh:mm` or `-hh:mm`, in range. It may not be `Z`, which in brackets reads as a one-letter zone name. +- A tag is a key, `=`, and one or more values joined by `-`: + - The key starts with a lower case letter or `_`, and goes on with lower case letters, digits, `_` and `-`. + - A value is one or more ASCII letters or digits. +- The time zone, when there is one, comes before every tag. +- In ABNF, alternation binds more loosely than concatenation, so the `time-zone` rule as written reads `("[" critical-flag time-zone-name) / (time-numoffset "]")`. The spec follows the intent, which section 4.1's note and every example show: a name or an offset between the brackets. + +`parseExt` reads such a string. It returns an `Ext`: +- the timestamp, as `parse` reads it; +- the time zone, if there is one, with whether it is critical, its name as the parts between the slashes, or its offset; +- the tags in order, each with whether it is critical, its key, and its values as the parts between the hyphens. + +It reads exactly the strings of the grammar, with the timestamp as `parse` reads it, second 60 at the end of any month included, and a string with no suffix exactly as `parse` reads it. `Ext.print` writes an `Ext` back, with `T` and `Z` in upper case. + +`Ext.lookup` gives the first tag with a key. Section 3.3 has an application that does not handle a repeated elective key choose the first. + +`Ext.erroneous` says whether an application must treat the string as erroneous. That depends on the application, so it takes a `Processor`: which tags the application can process, and the offset a named time zone has at an instant, or `none` for a zone it does not know. The string is erroneous when any of these holds: +- **Section 3.4:** the time zone is critical and does not agree with the timestamp. A named zone the application does not know never agrees, as section 4.1 asks. Otherwise the zone's offset at that instant must be the timestamp's offset. `Z` and `-00:00` assert no local offset, so a numeric offset or a zone the application knows agrees with them, as Figure 2 shows for `2022-07-08T00:14:07Z[!Europe/London]`. +- **Section 3.3:** a critical tag the application cannot process, or a critical tag whose key another tag uses with other values. +- **Section 3.2:** a key that starts with `_`, for an experiment, that the application does not process. + +Everything else is elective: an application may ignore a tag it does not know, or a time zone that disagrees with the offset when the zone is not critical. This library holds no time zone database, and does not judge what a tag such as a calendar means. Those are the application's, through its `Processor`. + ## Errors -`parse` returns `none` for any string it does not accept, `fromUnixSeconds` for any number outside the years 0000 to 9999, and `fromSiSeconds` for any number outside 1972 to 9999. No function can fail any other way. +`parse` and `parseExt` return `none` for any string they do not accept, `fromUnixSeconds` for any number outside the years 0000 to 9999, and `fromSiSeconds` for any number outside 1972 to 9999. No function can fail any other way. ## The command-line tool @@ -72,11 +101,11 @@ The command-line tool in `Main.lean` has two modes: - `rfc3339 check TIMESTAMP...` prints each timestamp's printed form and its Unix seconds, or `invalid`. It exits with 1 when any timestamp is invalid. - `rfc3339 serve` answers requests from the differential tests, one per line. Each string is sent as the hex digits of its UTF-8 bytes. The header comment of `Main.lean` gives the protocol. -Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds`, `Timestamp.compareInstant`, `fromUnixSeconds`, `Timestamp.isValidKnown`, `Timestamp.siSeconds`, `Timestamp.taiMinusUtc` and `fromSiSeconds`. The `known` request prints `-` for TAI − UTC before 1972. +Every answer comes from `parse`, `Timestamp.print`, `Timestamp.unixSeconds`, `Timestamp.compareInstant`, `fromUnixSeconds`, `Timestamp.isValidKnown`, `Timestamp.siSeconds`, `Timestamp.taiMinusUtc`, `fromSiSeconds`, `parseExt`, `Ext.print`, `Ext.lookup` and `Ext.erroneous`. The `known` request prints `-` for TAI − UTC before 1972. The `ixdtf` request judges each string with the example application of `Spec.exampleProcessor`, and gives the values of its first `u-ca` tag. ## 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` and, for the leap second table, `Spec/Leap.lean`. They are written from the RFC and checked against its tables and against known day counts. +Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`, for the leap second table in `Spec/Leap.lean`, and for RFC 9557 in `Spec/Ixdtf.lean`. They are written from the RFC and checked against its tables and against known day counts. | Property | Theorem | |----------|---------| @@ -104,20 +133,29 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | `taiMinusUtc` is 10 and one more for each leap second of the table before the timestamp. | `Spec.taiMinusUtc_leapsBefore` | | TAI − UTC from 1972 on, at each second but a leap second, is the table's value. | `Spec.taiMinusUtc_eq` | | Leap seconds of the table and months without one; SI seconds and TAI − UTC around the first and the last; the round trip Unix seconds lose. | `Spec.leap_table_vectors` | +| `parseExt s` is `e` exactly when `e` is valid by the RFC 9557 grammar and `s` is a timestamp `parse` reads as `e`'s, then `e`'s suffix as the grammar writes it. | `Spec.parseExt_iff` | +| A valid `Ext` prints as the grammar writes it. | `Spec.printExt_eq` | +| Printing then parsing gives a valid `Ext` back. | `Spec.parseExt_print` | +| A string with no `[` reads as `parse` reads it, with no time zone and no tags. | `Spec.parseExt_plain` | +| `lookup` gives the first tag with the key. | `Spec.lookup_iff` | +| `erroneous` decides `Spec.MustReject`: the rules of sections 3.2 to 3.4, for any application. | `Spec.erroneous_iff` | +| Every example of RFC 9557 is read, and is erroneous for the example application exactly where the RFC says; so are critical zones that agree with the offset and a critical `-00:00` zone that does not; strings the grammar refuses are not read. | `Spec.ixdtf_vectors` | Together, these fix every output for valid input. - `parse` is fixed for every string. - `print`, `unixSeconds` and `compareInstant` are fixed for every valid timestamp. The parser gives only valid timestamps. - `fromUnixSeconds` is fixed for every number, by `Spec.fromUnixSeconds_iff` and `Spec.fromUnixSeconds_isSome`, and `fromSiSeconds` likewise by its two statements. +- `parseExt` is fixed for every string, `Ext.print` for every valid `Ext`, `Ext.lookup` for every `Ext` and key, and `Ext.erroneous` for every application and `Ext`. - `isValidKnown` is fixed for every timestamp, and `siSeconds` for every valid one. `taiMinusUtc` is fixed for every valid timestamp, by `Spec.taiMinusUtc_leapsBefore`, and agrees with the table's column from 1972 on but at a leap second. - A parser that accepted nothing would meet `Spec.parse_valid`, but it would fail `Spec.parse_iff` and `Spec.parse_print`. - A parser that accepted too much would fail `Spec.parse_iff`. ## Oracle -The differential tests compare the tool with two oracles: +The differential tests compare the tool with these oracles: - Python's `datetime` and `calendar` modules: month lengths, offset arithmetic, seconds since the epoch, `datetime.fromisoformat` on every accepted string it can hold, and the UTC timestamp for a number of seconds. `datetime` holds no year 0, so dates there are moved by 400 years, one cycle of the Gregorian calendar, for the arithmetic. - A copy of the rules above, written in Python from the RFC. - For leap seconds, tzdata's `leap-seconds.list` on the test machine, read by the test script itself, with the SI seconds and TAI − UTC worked out from it in Python. +- For RFC 9557, the grammar of section 4.1 and the rules of sections 3.2 to 3.4, written in Python from the RFC, with the same example application. diff --git a/Spec.lean b/Spec.lean index bb85987..e33771a 100644 --- a/Spec.lean +++ b/Spec.lean @@ -15,6 +15,7 @@ import Rfc3339 import Spec.Defs import Spec.Leap +import Spec.Ixdtf open Rfc3339 @@ -261,3 +262,123 @@ theorem Spec.leap_table_vectors : fromSiSeconds 1420156827 = some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ ∧ fromUnixSeconds (Timestamp.unixSeconds ⟨2016, 12, 31, 23, 59, 60, [], .z⟩) = some ⟨2017, 1, 1, 0, 0, 0, [], .z⟩ := sorry + +/-! ## RFC 9557: the Internet Extended Date/Time Format -/ + +/-- `parseExt` returns `e` exactly when `e` is an IXDTF timestamp the + grammar of section 4.1 allows and the string is how it is written: + the RFC 3339 part with `T` and `Z` in either case, then the suffix + as written. So it accepts nothing outside the grammar, rejects + nothing inside it, and returns the time zone and tags as written. -/ +theorem Spec.parseExt_iff (s : String) (e : Ext) : + parseExt s = some e ↔ + Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Spec.renderSuffix e ∧ + dt.map Spec.asciiUpper = Spec.render e.stamp := sorry + +/-- An IXDTF timestamp prints as the grammar writes it, with `T` and `Z` + in upper case. -/ +theorem Spec.printExt_eq (e : Ext) (h : Spec.ExtValid e) : + e.print.toList = Spec.render e.stamp ++ Spec.renderSuffix e := sorry + +/-- Round trip: printing then parsing gives the IXDTF timestamp back. -/ +theorem Spec.parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e := sorry + +/-- IXDTF extends RFC 3339: a string with no suffix reads as `parse` + reads it, with no time zone and no tags. -/ +theorem Spec.parseExt_plain (s : String) (h : '[' ∉ s.toList) : + parseExt s = (parse s).map fun t => ⟨t, none, []⟩ := sorry + +/-- `lookup` gives the first tag with the key, which section 3.3 has an + application choose when an elective key is repeated. -/ +theorem Spec.lookup_iff (e : Ext) (k : List Char) (t : Tag) : + e.lookup k = some t ↔ ∃ l r, e.tags = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k := sorry + +/-- `erroneous` decides what sections 3.2 to 3.4 make an application + treat as erroneous. -/ +theorem Spec.erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Spec.MustReject p e := sorry + +/-- Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, with + the application of `Spec.exampleProcessor`: each one is read, and is + erroneous exactly where the RFC says it must be treated so. Also + critical time zones that agree with the offset, a critical `-00:00` + zone that does not, and strings the grammar refuses. -/ +theorem Spec.ixdtf_vectors : + -- Section 4.2, Figures 4 to 7 + parseExt "1996-12-19T16:39:57-08:00" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, []⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, + some (false, .name ["America".toList, "Los_Angeles".toList]), []⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, + some (false, .name ["America".toList, "Los_Angeles".toList]), + [⟨false, "u-ca".toList, ["hebrew".toList]⟩]⟩ ∧ + parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]" = + some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, + [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ ∧ + ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + -- An experiment the application does not take part in + ((parseExt "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + -- Section 1.2: an offset time zone + parseExt "2022-07-08T00:14:07+08:45[+08:45]" = + some ⟨⟨2022, 7, 8, 0, 14, 7, [], .plus 8 45⟩, some (false, .offset (.plus 8 45)), []⟩ ∧ + ((parseExt "2022-07-08T00:14:07+08:45[!+08:45]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + -- Section 3.3, elective: an inconsistent zone, the zones of the note, + -- an unknown key, repeated keys + ((parseExt "2022-07-08T00:14:07+01:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").bind (·.lookup "u-ca".toList) = + some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese]").bind (·.lookup "u-ca".toList) = + some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ + -- Section 3.3, critical: the four examples + ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][!u-ca=japanese]").map + (·.erroneous Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + -- Section 3.4, Figures 1 and 2 + ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + -- Critical zones that agree with the offset, and a critical `-00:00` + -- zone, offset 0, under an offset of +01:00 + ((parseExt "1996-12-19T16:39:57-08:00[!America/Los_Angeles]").map + (·.erroneous Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + some false) ∧ + ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Spec.exampleProcessor) = + some true) ∧ + -- `Z` in brackets is a zone name, not an offset + ((parseExt "2022-07-08T00:14:07Z[Z]").map (·.zone) = some (some (false, .name ["Z".toList]))) ∧ + -- Refused by the grammar: an empty item, `.` and `..`, an upper case + -- key, an empty value, a time zone after a tag, an offset out of range + parseExt "2022-07-08T00:14:07Z[]" = none ∧ + parseExt "2022-07-08T00:14:07Z[.]" = none ∧ + parseExt "2022-07-08T00:14:07Z[a/..]" = none ∧ + parseExt "2022-07-08T00:14:07Z[U-ca=x]" = none ∧ + parseExt "2022-07-08T00:14:07Z[u-ca=a--b]" = none ∧ + parseExt "2022-07-08T00:14:07Z[u-ca=x][Europe/Paris]" = none ∧ + parseExt "2022-07-08T00:14:07Z[+24:00]" = none := sorry diff --git a/Spec/Ixdtf.lean b/Spec/Ixdtf.lean new file mode 100644 index 0000000..8b43732 --- /dev/null +++ b/Spec/Ixdtf.lean @@ -0,0 +1,190 @@ +/- + The definitions the IXDTF statements use, written from RFC 9557, the + Internet Extended Date/Time Format, independently of the code in + `Rfc3339/Ixdtf.lean`. Part of the approved specification, with + `Spec.lean`, `Spec/Defs.lean` and `Rfc3339/IxdtfTypes.lean`. +-/ + +import Spec.Defs +import Rfc3339.IxdtfTypes + +open Rfc3339 + +/-! ## Section 4.1, the grammar + +``` +time-zone-initial = ALPHA / "." / "_" +time-zone-char = time-zone-initial / DIGIT / "-" / "+" +time-zone-part = time-zone-initial *time-zone-char + ; but not "." or ".." +time-zone-name = time-zone-part *("/" time-zone-part) +time-zone = "[" critical-flag + time-zone-name / time-numoffset "]" + +key-initial = lcalpha / "_" +key-char = key-initial / DIGIT / "-" +suffix-key = key-initial *key-char + +suffix-value = 1*alphanum +suffix-values = suffix-value *("-" suffix-value) +suffix-tag = "[" critical-flag + suffix-key "=" suffix-values "]" + +suffix = [time-zone] *suffix-tag + +date-time-ext = date-time suffix + +critical-flag = [ "!" ] + +alphanum = ALPHA / DIGIT +lcalpha = %x61-7A +``` + +`date-time` and `time-numoffset` are RFC 3339's, as `Spec/Defs.lean` +gives them. In ABNF (RFC 5234, section 3.10) alternation binds more +loosely than concatenation, so the `time-zone` rule read literally is +`("[" critical-flag time-zone-name) / (time-numoffset "]")`. The intent, +which section 4.1's note ("a time-zone is syntactically similar to a +suffix-tag") and every example show, is +`"[" critical-flag (time-zone-name / time-numoffset) "]"`, and that is +what is written here. +-/ + +/-- `ALPHA`. -/ +def Spec.Alpha (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') + +/-- `DIGIT`. -/ +def Spec.Digit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9' + +/-- `time-zone-part`, but not `.` or `..`. -/ +def Spec.ZonePart (p : List Char) : Prop := + ∃ c cs, p = c :: cs ∧ (Spec.Alpha c ∨ c = '.' ∨ c = '_') ∧ + (∀ d ∈ cs, Spec.Alpha d ∨ d = '.' ∨ d = '_' ∨ Spec.Digit d ∨ d = '-' ∨ d = '+') ∧ + p ≠ ['.'] ∧ p ≠ ['.', '.'] + +/-- What may stand in a `time-zone`: a `time-zone-name`, one or more + parts, or a `time-numoffset`, which is RFC 3339's numeric offset, not + `Z`. -/ +def Spec.ZoneValid : Zone → Prop + | .name parts => parts ≠ [] ∧ ∀ p ∈ parts, Spec.ZonePart p + | .offset o => o ≠ .z ∧ Spec.OffsetValid o + +/-- `suffix-key`. -/ +def Spec.SuffixKey (k : List Char) : Prop := + ∃ c cs, k = c :: cs ∧ (('a' ≤ c ∧ c ≤ 'z') ∨ c = '_') ∧ + ∀ d ∈ cs, ('a' ≤ d ∧ d ≤ 'z') ∨ d = '_' ∨ Spec.Digit d ∨ d = '-' + +/-- `suffix-value`. -/ +def Spec.SuffixValue (v : List Char) : Prop := v ≠ [] ∧ ∀ c ∈ v, Spec.Alpha c ∨ Spec.Digit c + +/-- A `suffix-tag`'s key and values. -/ +def Spec.TagValid (t : Tag) : Prop := + Spec.SuffixKey t.key ∧ t.values ≠ [] ∧ ∀ v ∈ t.values, Spec.SuffixValue v + +/-- An IXDTF timestamp the grammar allows: a valid RFC 3339 timestamp, a + time zone of the grammar if there is one, and tags of the grammar. -/ +def Spec.ExtValid (e : Ext) : Prop := + Spec.Valid e.stamp ∧ (∀ c z, e.zone = some (c, z) → Spec.ZoneValid z) ∧ + ∀ t ∈ e.tags, Spec.TagValid t + +/-- `critical-flag`. -/ +def Spec.renderFlag (c : Bool) : List Char := if c then ['!'] else [] + +/-- A `time-zone-name`, its parts joined by `/`, or a `time-numoffset`. -/ +def Spec.renderZone : Zone → List Char + | .name parts => (parts.intersperse ['/']).flatten + | .offset o => Spec.renderOffset o + +/-- `suffix-tag`. -/ +def Spec.renderTag (t : Tag) : List Char := + ['['] ++ Spec.renderFlag t.critical ++ t.key ++ ['='] ++ (t.values.intersperse ['-']).flatten ++ + [']'] + +/-- `suffix`: the `time-zone`, if any, then the tags. -/ +def Spec.renderSuffix (e : Ext) : List Char := + (match e.zone with + | some (c, z) => ['['] ++ Spec.renderFlag c ++ Spec.renderZone z ++ [']'] + | none => []) ++ + (e.tags.map Spec.renderTag).flatten + +example : Spec.renderSuffix ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, + some (false, .name ["America".toList, "Los_Angeles".toList]), + [⟨false, "u-ca".toList, ["hebrew".toList]⟩]⟩ = + "[America/Los_Angeles][u-ca=hebrew]".toList := by decide + +/-! ## Sections 2, 3.2, 3.3 and 3.4: what an application must reject + +Section 2 updates RFC 3339: "If the time in UTC is known, but the offset +to local time is unknown, this can be represented with an offset of +`Z`", and section 3.4 adds that "-00:00 may be used instead of Z because +they have the same meaning". So `Z` and `-00:00` assert no local offset. + +Section 3.4: "In case of an inconsistency between time-offset and time +zone suffix, if the critical flag is used on the time zone suffix, an +application MUST act on the inconsistency." Figure 2's +`2022-07-08T00:14:07Z[!Europe/London]` is "not inconsistent because +[it does] not assert any particular local time nor local offset". +Section 4.1: recipients "may not be aware of such an IANA Time Zone name +and should treat such a situation as any other inconsistency." + +Section 3.3: "A suffix tag may also indicate that it is critical: The +recipient is advised that it MUST NOT act on the IXDTF string unless it +can process the suffix tag as specified." Its examples +`2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]` and +`2022-07-08T00:14:07Z[u-ca=chinese][!u-ca=japanese]` "have an internal +inconsistency ... that is marked as critical, so a recipient MUST treat +these IXDTF strings as erroneous". And: "An application that encounters +duplicate use of a suffix key in elective suffixes and does not want to +perform additional processing on this inconsistency MUST choose the +first suffix that has that key". + +Section 3.2: "Key names that start with an underscore are intended for +experiments in controlled environments and cannot be registered; such +keys MUST NOT be used for interchange and MUST be rejected by +implementations not specifically configured to take part in such an +experiment." + +Below, what the application can act on is a `Processor`: which tags it +processes, which taking part in an experiment means for a key that +starts with `_`, and the offset a named time zone has at an instant. +-/ + +/-- The timestamp's offset asserts a local offset: it is not `Z` or + `-00:00`. -/ +def Spec.AssertsOffset (o : Offset) : Prop := o ≠ .z ∧ o ≠ .minus 0 0 + +/-- The time zone is consistent with the timestamp, for an application + that knows the zone offsets `p` gives: the zone is known and, where + the timestamp asserts a local offset, has that offset. -/ +def Spec.ZoneConsistent (p : Processor) (t : Timestamp) : Zone → Prop + | .offset o => Spec.AssertsOffset t.offset → Spec.offsetMinutes o = Spec.offsetMinutes t.offset + | .name parts => + ∃ m, p.zoneOffset parts t = some m ∧ + (Spec.AssertsOffset t.offset → m = Spec.offsetMinutes t.offset) + +/-- The application must treat the string as erroneous: by section 3.4, + a critical time zone that is not consistent with the timestamp; by + section 3.3, a critical tag it cannot process, or a critical tag + whose key a tag uses with other values; by section 3.2, a key for an + experiment it does not take part in. -/ +def Spec.MustReject (p : Processor) (e : Ext) : Prop := + (∃ z, e.zone = some (true, z) ∧ ¬ Spec.ZoneConsistent p e.stamp z) ∨ + (∃ t ∈ e.tags, t.critical = true ∧ p.processes t = false) ∨ + (∃ t ∈ e.tags, t.critical = true ∧ ∃ u ∈ e.tags, u.key = t.key ∧ u.values ≠ t.values) ∨ + (∃ t ∈ e.tags, t.key.head? = some '_' ∧ p.processes t = false) + +/-- An application for the examples of sections 3.3, 3.4 and 4.2: it + processes `u-ca` with the calendars `chinese`, `japanese` and + `hebrew`, takes part in no experiment, and knows three zones, with + the offsets they had at the examples' instants: Europe/Paris +02:00 + and Europe/London +01:00 in July 2022, America/Los_Angeles -08:00 in + December 1996. -/ +def Spec.exampleProcessor : Processor where + processes t := t.key = "u-ca".toList ∧ + (t.values = ["chinese".toList] ∨ t.values = ["japanese".toList] ∨ + t.values = ["hebrew".toList]) + zoneOffset parts _ := + if parts = ["Europe".toList, "Paris".toList] then some 120 + else if parts = ["Europe".toList, "London".toList] then some 60 + else if parts = ["America".toList, "Los_Angeles".toList] then some (-480) + else none diff --git a/bar.toml b/bar.toml index 7baee02..744cf5d 100644 --- a/bar.toml +++ b/bar.toml @@ -13,15 +13,19 @@ spec_authors = ["claude"] 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", "Spec/Leap.lean", "Rfc3339/Types.lean"] +# Rfc3339/Types.lean and Rfc3339/IxdtfTypes.lean hold the types the +# statements are about, so they are part of the specification. +files = [ + "SPEC.md", "Spec.lean", "Spec/Defs.lean", "Spec/Leap.lean", "Spec/Ixdtf.lean", + "Rfc3339/Types.lean", "Rfc3339/IxdtfTypes.lean", +] # The code under proof: the functions the statements are about. code = [ "Rfc3339.parse", "Rfc3339.Timestamp.print", "Rfc3339.Timestamp.isValid", "Rfc3339.Timestamp.unixSeconds", "Rfc3339.Timestamp.compareInstant", "Rfc3339.fromUnixSeconds", "Rfc3339.Timestamp.isValidKnown", "Rfc3339.Timestamp.siSeconds", - "Rfc3339.Timestamp.taiMinusUtc", "Rfc3339.fromSiSeconds", + "Rfc3339.Timestamp.taiMinusUtc", "Rfc3339.fromSiSeconds", "Rfc3339.parseExt", + "Rfc3339.Ext.print", "Rfc3339.Ext.lookup", "Rfc3339.Ext.erroneous", ] # One entry per approval, added in a pull request the reviewer approves. diff --git a/comparator.json b/comparator.json index 2924454..5b58b19 100644 --- a/comparator.json +++ b/comparator.json @@ -26,7 +26,14 @@ "Spec.fromSiSeconds_isSome", "Spec.taiMinusUtc_leapsBefore", "Spec.taiMinusUtc_eq", - "Spec.leap_table_vectors" + "Spec.leap_table_vectors", + "Spec.parseExt_iff", + "Spec.printExt_eq", + "Spec.parseExt_print", + "Spec.parseExt_plain", + "Spec.lookup_iff", + "Spec.erroneous_iff", + "Spec.ixdtf_vectors" ], "permitted_axioms": [ "propext", diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 2eb1491..dd0b090 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -6,27 +6,46 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified - Go: `time.Parse(time.RFC3339Nano, s)`, go version go1.24.7 linux/amd64 - rfc3339-validator 0.1.4 (Python 3.13.17), called on the string as given. `jsonschema` calls it for its `date-time` check on the upper-cased string, so the lower case rows below do not apply to `jsonschema`. - Seed: 20261025 -- Strings: 182166 +- Strings: 181849 - 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 | 18971 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | -| Go | rejects | second 60 | 3784 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| Go | accepts | offset hour above 23 or minute above 59 | 1978 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | -| Go | accepts | a field with one digit | 448 | `'0099-09-29T8:05:14.9-13:23'`, `'0508-04-01T2:41:06.3-08:38'` | -| Go | accepts | comma before the fraction | 4 | `'2000-01-01T00:00:00,5Z'`, `'1900-01-02T22:19:55,9-00:00'` | -| rfc3339-validator | rejects | lower case t or z | 18971 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | -| rfc3339-validator | rejects | second 60 | 3784 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| rfc3339-validator | rejects | year 0000 | 1248 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | -| rfc3339-validator | accepts | line break at the end | 891 | `'4244-06-01T08:05:55.054876690884+00:00\n'`, `'8593-06-30T13:42:25+05:44\n'` | +| Go | rejects | lower case t or z | 19086 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| Go | rejects | second 60 | 3696 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| Go | accepts | offset hour above 23 or minute above 59 | 1918 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | +| Go | accepts | a field with one digit | 440 | `'6796-03-01T8:13:08+17:53'`, `'2289-10-02T3:10:29.2-00:00'` | +| Go | accepts | comma before the fraction | 6 | `'2000-01-01T00:00:00,5Z'`, `'1900-01-02T22:19:55,9-00:00'` | +| rfc3339-validator | rejects | lower case t or z | 19086 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| rfc3339-validator | rejects | second 60 | 3696 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| rfc3339-validator | rejects | year 0000 | 1226 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | +| rfc3339-validator | accepts | line break at the end | 885 | `'4244-06-01T08:05:55.054876690884+00:00\n'`, `'5263-10-30T07:22:33.52-07:24\n'` | ## Leap seconds - ERFA, through pyerfa 2.0.1.5, with its own leap second table -- Timestamps known valid by the table, from 1972 on, given to ERFA: 22611. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 2949. -- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8666. Different: 0. +- Timestamps known valid by the table, from 1972 on, given to ERFA: 18834. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 1717. +- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8695. Different: 0. + +## RFC 9557 + +- Node v22.22.0, `Temporal.Instant.from`, with `--harmony-temporal`: V8's Temporal behind a flag, older than the current proposal +- Strings: 7143, of which this project reads 5302. The same answer, read or refused: 2833. + +Where Temporal differs from this project, by the first category that fits the string: + +| Temporal | Category | Strings | Example | +| --- | --- | --- | --- | +| refuses | a critical flag, which this Temporal refuses on any item | 2338 | `'2022-07-08T00:14:07+01:00[!Europe/Paris]'`, `'2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]'` | +| refuses | an experimental key | 681 | `'1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]'`, `'2022-07-08T00:14:07Z[_=x]'` | +| refuses | an unknown elective key | 660 | `'2022-07-08T00:14:07+01:00[knort=blargel]'`, `'2022-07-08T00:14:07Z[x_=y]'` | +| refuses | a fraction of more than nine digits, finer than Temporal's nanoseconds | 407 | `'5720-01-31T23:59:60.26153083810657+00:00[Etc/G_T+5][!_=chinese-japanese][_foo=0]'`, `'3938-05-31T07:00:58.533659862016880639560673568684585171z[_x]'` | +| refuses | a calendar with a part outside 3 to 8 characters, which the older proposal refuses | 111 | `'2022-07-08T00:14:07+00:00[u-ca=0]'`, `'2022-07-08T00:14:07+00:00[+01:00][u-ca=a-b]'` | +| refuses | a repeated elective `u-ca` | 70 | `'2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]'`, `'2024-02-04T15:17:00+23:59[+01:00][x=a-b][u-ca=a-b][u-ca=blargel]'` | +| refuses | a time zone name with a digit or `+`, or a part over 14 characters, which the older proposal refuses | 41 | `'2404-02-29T00:37:44.236447+18:26[a.b-c+d_e]'`, `'3793-03-02T15:50:39.27-20:39[a.b-c+d_e]'` | +| accepts | a time zone offset with no colon, as ISO 8601's basic format writes it | 1 | `'6121-04-02t21:22:26.9+05:04[+0530]'` | +| accepts | another suffix the grammar refuses | 1 | `'5984-06-01T02:30:25.893247-11:17[u-ca=gregory]]'` | diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 103614d..4a7fa4c 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,20 +2,21 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `datetime` and `calendar`, the RFC 3339 rules copied into this script, and for leap seconds tzdata's `/usr/share/zoneinfo/leap-seconds.list`, read by this script +- Oracle: Python 3.13.17 `datetime` and `calendar`, the RFC 3339 rules copied into this script, for leap seconds tzdata's `/usr/share/zoneinfo/leap-seconds.list`, read by this script, and for RFC 9557 its grammar and rules written in this script - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 300000 -- Mutated: 67878 of the inputs are mutated timestamps -- By kind: compare 29413, error 44, fromsi 9360, fromunix 44543, grid 16998, known 34497, mutated 67878, near miss 29254, valid 68013 -- Strings parsed: 182143, of which 83519 accepted (4666 with a leap second) and 98624 rejected -- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77331 -- Pairs ordered: 29413 (9874 before, 8322 same instant, 9754 after, 1463 with a string rejected) -- Unix seconds turned back into timestamps: 44543, of which 679 outside years 0000 to 9999 +- Mutated: 67589 of the inputs are mutated timestamps +- By kind: compare 29508, error 48, fromsi 9393, fromunix 44578, grid 16998, ixdtf 7143, known 27493, mutated 67589, near miss 29155, valid 68095 +- Strings parsed: 181837, of which 83546 accepted (4617 with a leap second) and 98291 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77425 +- Pairs ordered: 29508 (9918 before, 8280 same instant, 9846 after, 1464 with a string rejected) +- Unix seconds turned back into timestamps: 44578, of which 671 outside years 0000 to 9999 - Leap second table: /usr/share/zoneinfo/leap-seconds.list, 28 lines, 27 leap seconds, expires 2027-06-28, last updated at NTP time 3992312697, hash line `a9bad145 84c31c70 758402aa b37bfd54 5923836a` -- Timestamps checked against the table (`known`): 34497, of which 267 leap seconds of the table, 6367 with a second 60 it does not list, and 2570 rejected -- SI seconds turned back into timestamps (`fromsi`): 9360, of which 27 leap seconds and 695 outside 1972 to 9999 -- Malformed requests answered `error`: 44 of 44 +- Timestamps checked against the table (`known`): 27493, of which 224 leap seconds of the table, 5700 with a second 60 it does not list, and 1242 rejected +- SI seconds turned back into timestamps (`fromsi`): 9393, of which 27 leap seconds and 698 outside 1972 to 9999 +- RFC 9557 strings (`ixdtf`): 7143, of which 5302 read, 3122 of them erroneous for the example application, and 1841 refused +- Malformed requests answered `error`: 48 of 48 - Requests ending in CR LF: every seventh, 42857 - Strings also given to `rfc3339 check` as arguments, in batches of 500: 20000, and once with no arguments - Last lines with no LF, sent alone, answered right: 2 of 2 diff --git a/tests/cross_check.py b/tests/cross_check.py index f2182b4..b74ebdf 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -27,6 +27,12 @@ pip install --target .lake/oracle-packages pyerfa==2.0.1.5 +For RFC 9557, the strings tests/run_tests.py sends as `ixdtf` requests go +to `Temporal.Instant.from` in Node, with `--harmony-temporal`. That is +V8's own Temporal behind a flag, an older one than the current proposal: +it refuses some strings the proposal now reads. Each difference is put in +the first category below that fits it. + The counts go to tests/CROSS-CHECK.md. """ @@ -181,6 +187,84 @@ def leap_section(args): return lines +def ix_category(s, ours_ok): + """Why Temporal reads `s` differently: the first reason that fits.""" + r = run_tests.ix_reference(s) + if ours_ok: + f, _, zone, tags = r + if len(f["fraction"]) > 9: + return "a fraction of more than nine digits, finer than Temporal's nanoseconds" + if (zone and zone[0]) or any(c for c, _, _ in tags): + return "a critical flag, which this Temporal refuses on any item" + if any(k.startswith("_") for _, k, _ in tags): + return "an experimental key" + if len([k for _, k, _ in tags if k == "u-ca"]) > 1: + return "a repeated elective `u-ca`" + if any(k != "u-ca" for _, k, _ in tags): + return "an unknown elective key" + if tags and any(not 3 <= len(p) <= 8 for p in tags[0][2]): + return "a calendar with a part outside 3 to 8 characters, which the older proposal refuses" + if zone and zone[1][0] == "name": + parts = zone[1][1].split("/") + etc_gmt = re.fullmatch(r"Etc/GMT[+-](?:[0-9]|1[0-4])", zone[1][1]) + if not etc_gmt and any(re.search(r"[0-9+]", q) or len(q) > 14 for q in parts): + return ("a time zone name with a digit or `+`, or a part over 14 characters, " + "which the older proposal refuses") + return "another time zone name" + return "other" + i = s.find("[") + if run_tests.reference(s if i < 0 else s[:i]) is None: + return "an RFC 3339 part the RFC does not allow" + if re.search(r"\[!?[+-][0-9]{4}\]", s): + return "a time zone offset with no colon, as ISO 8601's basic format writes it" + if re.search(r"\[[^\]]*\[", s): + return "a `[` inside an item" + return "another suffix the grammar refuses" + + +def ixdtf_section(args): + import os + strings = [bytes.fromhex(req.split(" ")[1]).decode("utf-8") + for label, req, _, _ in run_tests.cases(args.seed, args.count) if label == "ixdtf"] + ours, problem = run_tests.run_tool("".join(f"ixdtf {run_tests.hexed(x)}\n" for x in strings)) + if problem or len(ours) != len(strings): + sys.exit(f"the tool failed: {problem}") + out = subprocess.run(["node", "--harmony-temporal", str(GO_DIR / "ixdtf.js")], + input="".join(run_tests.hexed(x) + "\n" for x in strings), + capture_output=True, text=True, check=True) + theirs = out.stdout.split("\n")[: len(strings)] + node = subprocess.run(["node", "--version"], capture_output=True, text=True).stdout.strip() + tallies, examples = {}, {} + for x, o, t in zip(strings, ours, theirs): + ok, tok = o.startswith("OK"), t == "OK" + if ok == tok: + continue + key = ("accepts" if tok else "refuses", ix_category(x, ok)) + tallies[key] = tallies.get(key, 0) + 1 + examples.setdefault(key, []) + if len(examples[key]) < 2: + examples[key].append(x) + same = sum(1 for o, t in zip(ours, theirs) if o.startswith("OK") == (t == "OK")) + lines = [ + "", + "## RFC 9557", + "", + f"- Node {node}, `Temporal.Instant.from`, with `--harmony-temporal`: V8's Temporal behind a " + "flag, older than the current proposal", + f"- Strings: {len(strings)}, of which this project reads " + f"{sum(1 for o in ours if o.startswith('OK'))}. The same answer, read or refused: {same}.", + "", + "Where Temporal differs from this project, by the first category that fits the string:", + "", + "| Temporal | Category | Strings | Example |", + "| --- | --- | --- | --- |", + ] + for (how, cat), n in sorted(tallies.items(), key=lambda kv: (-kv[1], kv[0])): + ex = ", ".join(f"`{e!r}`" for e in examples[(how, cat)]) + lines.append(f"| {how} | {cat} | {n} | {ex} |") + return lines + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=20261025) @@ -251,6 +335,7 @@ def main(): for s, theirs, ours in value_mismatch[:20]: lines.append(f"- Different instant: `{s!r}`: Go `{theirs}`, this project `{ours}`") lines += leap_section(args) + lines += ixdtf_section(args) REPORT.write_text("\n".join(lines) + "\n", encoding="utf-8") print(f"{len(strings)} strings; report in {REPORT}") diff --git a/tests/cross_check/ixdtf.js b/tests/cross_check/ixdtf.js new file mode 100644 index 0000000..0a5e176 --- /dev/null +++ b/tests/cross_check/ixdtf.js @@ -0,0 +1,14 @@ +// RFC 9557 in Node's Temporal, for tests/cross_check.py. Run with +// `node --harmony-temporal`. Reads one hex-encoded UTF-8 string per line +// and prints OK when Temporal.Instant.from reads it, or ERR. +const readline = require("readline"); +const out = []; +readline.createInterface({ input: process.stdin }).on("line", (line) => { + const s = Buffer.from(line, "hex").toString("utf8"); + try { + Temporal.Instant.from(s); + out.push("OK"); + } catch (e) { + out.push("ERR"); + } +}).on("close", () => process.stdout.write(out.map((l) => l + "\n").join(""))); diff --git a/tests/run_tests.py b/tests/run_tests.py index 85e8362..219b5e9 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1,7 +1,7 @@ #!/usr/bin/env python3 """Differential tests: the Lean parser against Python's date code. -There are two oracles: +For RFC 3339 itself there are two oracles: - Python's `datetime` and `calendar` modules. `calendar.isleap` and `calendar.mdays` give the month lengths, `datetime` arithmetic applies @@ -51,6 +51,20 @@ wherever `parse` does. `fromsi` requests take every leap second's SI seconds and the two seconds either side, the ends of the range and one past each, random numbers, and the SI seconds of random timestamps; +- for RFC 9557, the Internet Extended Date/Time Format, a fourth + oracle: its grammar (section 4.1) and its rules for elective and + critical tags (sections 3.2 to 3.4), written again in this script. + `ixdtf` requests must give the printed form, whether the example + application must treat the string as erroneous, and the first `u-ca` + tag. The inputs are every example of sections 1.2, 3.3, 3.4 and 4.2, the + edges of the grammar and rules written out below, + random timestamps with random suffixes (time zones by name and by + offset, tags with known, unknown and experimental keys, each item + elective or critical, keys repeated), and those suffixes mutated: a + character changed, dropped or added, brackets, `!` and `=` among them, + the first bracket dropped or a last one left open, a key in upper + case, `.` or `..` as a zone part, an empty item or value, a time zone + after a tag; - malformed requests, which the tool must answer with `error`. Every seventh request ends in CR LF. The first 20,000 parsed strings @@ -208,6 +222,189 @@ def si_grid(): yield from (-1, 0, 1, top - 1, top, top + 1, 10 ** 20, -10 ** 20) +# RFC 9557: the grammar of section 4.1 and the rules of sections 3.2 to +# 3.4, written here apart from the Lean code. +IX_ITEMS = re.compile(r"(?:\[[^\[\]]*\])*") +IX_ZONE_PART = re.compile(r"[A-Za-z._][A-Za-z0-9._+\-]*") +IX_OFFSET = re.compile(r"[+-]([0-9]{2}):([0-9]{2})") +IX_TAG = re.compile(r"([a-z_][a-z0-9_\-]*)=([A-Za-z0-9]+(?:-[A-Za-z0-9]+)*)") +# The example application of Spec.exampleProcessor. +IX_CALENDARS = (["chinese"], ["japanese"], ["hebrew"]) +IX_ZONES = {"Europe/Paris": 120, "Europe/London": 60, "America/Los_Angeles": -480} + + +def ix_zone(body): + """The offset in minutes of a numeric time zone, the name of a named + one, or None when the grammar refuses it.""" + m = IX_OFFSET.fullmatch(body) + if m: + h, mi = int(m.group(1)), int(m.group(2)) + if h > 23 or mi > 59: + return None + return ("offset", (h * 60 + mi) * (1 if body[0] == "+" else -1)) + parts = body.split("/") + if all(IX_ZONE_PART.fullmatch(q) and q not in (".", "..") for q in parts): + return ("name", body) + return None + + +def ix_reference(s): + """The fields of an IXDTF string, or None when the grammar refuses it.""" + i = s.find("[") + dt, sfx = (s, "") if i < 0 else (s[:i], s[i:]) + f = reference(dt) + if f is None or not IX_ITEMS.fullmatch(sfx): + return None + zone, tags = None, [] + for k, body in enumerate(re.findall(r"\[([^\[\]]*)\]", sfx)): + crit = body.startswith("!") + b = body[1:] if crit else body + if k == 0 and "=" not in b: + z = ix_zone(b) + if z is None: + return None + zone = (crit, z) + else: + m = IX_TAG.fullmatch(b) + if not m: + return None + tags.append((crit, m.group(1), m.group(2).split("-"))) + return f, sfx, zone, tags + + +def ixdtf(s): + """The expected answer to `ixdtf`.""" + r = ix_reference(s) + if r is None: + return "REJECT" + f, sfx, zone, tags = r + asserts = f["offset"] not in ("Z", "-00:00") + bad = False + if zone and zone[0]: + kind, z = zone[1] + m = z if kind == "offset" else IX_ZONES.get(z) + if m is None or (asserts and m != f["offset_minutes"]): + bad = True + for crit, key, values in tags: + known = key == "u-ca" and values in IX_CALENDARS + if crit and not known: + bad = True + if crit and any(k == key and v != values for _, k, v in tags): + bad = True + if key.startswith("_") and not known: + bad = True + cal = next(("-".join(v) for _, k, v in tags if k == "u-ca"), "-") + return f"OK\t{f['print']}{sfx}\t{'true' if bad else 'false'}\t{cal}" + + +IX_EXAMPLES = [ + "2022-07-08T00:14:07+01:00[Europe/Paris]", "2022-07-08T00:14:07Z[Europe/Paris]", + "2022-07-08T02:14:07+02:00[Europe/Paris]", "2022-07-08T00:14:07+01:00[knort=blargel]", + "2022-07-08T00:14:07+01:00[!Europe/Paris]", "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]", + "2022-07-08T00:14:07Z[u-ca=chinese][!u-ca=japanese]", "2022-07-08T00:14:07Z[!knort=blargel]", + "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]", "2022-07-08T00:14:07Z[u-ca=chinese]", + "2022-07-08T00:14:07+00:00[!Europe/London]", "2022-07-08T00:14:07+00:00[Europe/London]", + "2022-07-08T00:14:07Z[!Europe/London]", "2022-07-08T00:14:07Z[Europe/London]", + "1996-12-19T16:39:57-08:00", "1996-12-19T16:39:57-08:00[America/Los_Angeles]", + "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]", + "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]", "2022-07-08T00:14:07+08:45[+08:45]", +] +# The edges of the grammar and the rules, each written once. +IX_EDGES = [ + "2022-07-08T00:14:07Z[..]", "2022-07-08T00:14:07Z[a/..]", "2022-07-08T00:14:07Z[../a]", + "2022-07-08T00:14:07Z[...]", "2022-07-08T00:14:07Z[.a]", "2022-07-08T00:14:07Z[a/./b]", + "2022-07-08T00:14:07Z[+23:59]", "2022-07-08T00:14:07Z[+24:00]", "2022-07-08T00:14:07Z[-00:60]", + "2022-07-08T00:14:07Z[!+01:00]", "2022-07-08T00:14:07+01:00[!+01:00]", + "2022-07-08T00:14:07+02:00[!+01:00]", "2022-07-08T00:14:07-00:00[!+01:00]", + "2022-07-08T00:14:07+00:00[!-00:00]", "2022-07-08T00:14:07-00:00[!Europe/Paris]", + "2022-07-08T00:14:07+02:00[!Europe/Paris]", "2022-07-08T00:14:07Z[!Nowhere/Fake]", + "2022-07-08T00:14:07Z[!u-ca=hebrew][!u-ca=hebrew]", "2022-07-08T00:14:07Z[!u-ca=hebrew][u-ca=hebrew]", + "2022-07-08T00:14:07Z[u-ca=hebrew][u-ca=chinese][!u-ca=hebrew]", "2022-07-08T00:14:07Z[!u-ca=a-b]", + "2022-07-08T00:14:07Z[_=x]", "2022-07-08T00:14:07Z[!_x=y]", "2022-07-08T00:14:07Z[x_=y]", + "2022-07-08T00:14:07Z[u-ca=]", "2022-07-08T00:14:07Z[=x]", "2022-07-08T00:14:07Z[u-ca==x]", + "2022-07-08T00:14:07Z[u-ca=x-]", "2022-07-08T00:14:07Z[u-ca=-x]", "2022-07-08T00:14:07Z[Ab=x]", + "2022-07-08T00:14:07Z[0a=x]", "2022-07-08T00:14:07Z[-a=x]", "2022-07-08T00:14:07Z[!!u-ca=x]", + "2022-07-08T00:14:07Z[!]", "2022-07-08T00:14:07Z[]", "2022-07-08T00:14:07Z[Europe/Paris][Europe/Paris]", + "2022-07-08T00:14:07Z[u-ca=hebrew][Europe/Paris]", "2022-07-08T00:14:07Z[Europe/Paris]x", + "2022-07-08T00:14:07Z [Europe/Paris]", "2022-07-08T00:14:07Z[Europe//Paris]", + "2022-07-08T00:14:07Z[/Europe]", "2022-07-08T00:14:07Z[Europe/]", "2022-07-08T00:14:07Z[Z]", + "2022-07-08T00:14:07Z[UTC][u-ca=hebrew]", "2022-07-08T00:14:07Z[u-ca=Hebrew]", + "1990-12-31T23:59:60Z[u-ca=hebrew]", "2022-07-08t00:14:07z[u-ca=hebrew]", + # A critical -00:00 zone is offset 0, whatever the timestamp's offset + "2022-07-08T01:14:07+01:00[!-00:00]", "2022-07-07T16:14:07-08:00[!-00:00]", + "2022-07-08T00:14:07Z[!-00:00]", + # Critical zones that agree with an asserted offset + "1996-12-19T16:39:57-08:00[!America/Los_Angeles]", "2022-07-08T00:14:07+08:45[!+08:45]", + "2022-07-08T00:14:07+01:00[!+08:45]", + # A critical tag whose key another tag uses with values that share + # its first part, and two critical tags with one key + "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=chinese-japanese]", + "2022-07-08T00:14:07Z[u-ca=chinese-japanese][!u-ca=chinese]", + "2022-07-08T00:14:07Z[!u-ca=chinese][!u-ca=japanese]", + "2022-07-08T00:14:07Z[!u-ca=chinese][!u-ca=chinese]", +] +IX_NAMES = ["Europe/Paris", "Europe/London", "America/Los_Angeles", "Asia/Tokyo", "UTC", "Etc/GMT+5", + "America/Argentina/Buenos_Aires", "_x", ".a", "a.b-c+d_e", "Z", "z"] +IX_KEYS = ["u-ca", "u-ca", "knort", "_foo", "x", "a-b_c9", "_"] +IX_VALUES = [["chinese"], ["japanese"], ["hebrew"], ["gregory"], ["blargel"], ["a", "b"], ["X1"], ["0"], + ["chinese", "japanese"]] + + +def ix_offset_text(rng): + """An offset as RFC 3339 writes it; 0 as `+00:00` or `-00:00`.""" + m = rng.choice([0, 60, 120, -480, 330, -1439, 1439]) + sign = "+" if m > 0 or (m == 0 and rng.random() < 0.5) else "-" + return sign + f"{abs(m) // 60:02d}:{abs(m) % 60:02d}" + + +def random_suffix(rng): + items = [] + if rng.random() < 0.6: + flag = "!" if rng.random() < 0.3 else "" + body = ix_offset_text(rng) if rng.random() < 0.2 else rng.choice(IX_NAMES) + items.append(f"[{flag}{body}]") + for _ in range(rng.choice([0, 1, 1, 2, 3])): + flag = "!" if rng.random() < 0.3 else "" + items.append(f"[{flag}{rng.choice(IX_KEYS)}={'-'.join(rng.choice(IX_VALUES))}]") + return "".join(items) + + +def mutate_suffix(rng, sfx): + """A suffix with one change that is likely to break the grammar.""" + op = rng.randrange(10) + c = list(sfx) + if op == 0 and c: + c[rng.randrange(len(c))] = rng.choice("[]!=-/.+_aZ0 ") + elif op == 1 and c: + del c[rng.randrange(len(c))] + elif op == 2: + c.insert(rng.randint(0, len(c)), rng.choice("[]!=-/.+_aZ0")) + elif op == 3: + return sfx + rng.choice(["[]", "[!]", "[=x]", "[x=]", "[.]", "[..]", "[a/..]", "[a//b]"]) + elif op == 4: + return sfx + "[U-ca=x]" + elif op == 5: + return sfx + "[u-ca=a--b]" + elif op == 6: + return sfx + "[" + rng.choice(IX_NAMES) + "]" + elif op == 7: + return sfx + rng.choice(["[+24:00]", "[+23:60]", "[Z]", "[+1:00]", "[!!u-ca=x]"]) + elif op == 8: + return sfx.replace("[", "", 1) + else: + return sfx + "[" + return "".join(c) + + +def random_ixdtf(rng): + base = random_valid(rng) if rng.random() < 0.7 else stamp( + 2022, 7, 8, 0, 14, 7, "", rng.choice(["Z", "-00:00", "+00:00", "+01:00", "+02:00", "-08:00"])) + sfx = random_suffix(rng) + if rng.random() < 0.3: + sfx = mutate_suffix(rng, sfx) + return base + sfx + + def unix_grid(): """The ends of the range and one second past each, numbers at the edges of 32-bit counts, and the first second of every month of years @@ -565,6 +762,10 @@ def same_instant_pair(rng): ("known 3A", "hex digits are lower case"), ("known c0af", "an overlong encoding, not UTF-8"), ("known eda080", "a surrogate, not UTF-8"), + ("ixdtf", "no argument"), + ("ixdtf 3", "an odd number of hex digits"), + ("ixdtf 30 30", "two arguments"), + ("ixdtf ff", "not UTF-8"), ] # Strings `known` must answer REJECT, not NOLEAP: second 60 away from a @@ -598,6 +799,8 @@ def cases(seed, count): for s in KNOWN_REJECT: assert known(s) == "REJECT", s fixed.append(("known", f"known {hexed(s)}", "REJECT", False)) + for s in IX_EXAMPLES + IX_EDGES: + fixed.append(("ixdtf", f"ixdtf {hexed(s)}", ixdtf(s), False)) for s in itertools.chain(day_grid(), leap_grid(), edge_grid()): fixed.append(("grid", f"parse {hexed(s)}", answer(reference(s)), False)) edges = list(edge_grid()) @@ -615,6 +818,11 @@ def cases(seed, count): made += 1 while made < count: r = rng.random() + if r < 0.03: + s = random_ixdtf(rng) + yield ("ixdtf", f"ixdtf {hexed(s)}", ixdtf(s), False) + made += 1 + continue if r < 0.06: r = rng.random() if r < 0.65: @@ -780,8 +988,9 @@ def check_mode(items, limit=20000, batch=500): def oracle(): return (f"Python {platform.python_version()} `datetime` and `calendar`, the " - f"RFC 3339 rules copied into this script, and for leap seconds tzdata's " - f"`{LEAP_FILE}`, read by this script") + f"RFC 3339 rules copied into this script, for leap seconds tzdata's " + f"`{LEAP_FILE}`, read by this script, and for RFC 9557 its grammar and rules " + f"written in this script") def lean_version(): @@ -876,6 +1085,7 @@ def main(): known_leaps = sum(1 for label, req, want, _ in items if label == "known" and want.startswith("OK") and reference(bytes.fromhex(req.split(" ")[1]).decode())["second"] == 60) from_si_wants = [want for label, _, want, _ in items if label == "fromsi"] + ix_wants = [want for label, _, want, _ in items if label == "ixdtf"] expires = datetime(1900, 1, 1) + timedelta(seconds=LEAP_EXPIRES) if LEAP_EXPIRES else None mutated = sum(1 for item in items if item[3]) malformed = [got for item, got in zip(items, out) if item[0] == "error"] @@ -909,6 +1119,10 @@ def main(): f"- SI seconds turned back into timestamps (`fromsi`): {len(from_si_wants)}, of which " f"{sum(1 for w in from_si_wants if w[17:19] == '60')} leap seconds and " f"{from_si_wants.count('NONE')} outside 1972 to 9999", + f"- RFC 9557 strings (`ixdtf`): {len(ix_wants)}, of which " + f"{sum(1 for w in ix_wants if w.startswith('OK'))} read, " + f"{sum(1 for w in ix_wants if w.startswith('OK') and w.split(chr(9))[2] == 'true')} of them " + f"erroneous for the example application, and {ix_wants.count('REJECT')} refused", 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}",