From 9d62a8da24b09f44c7b2f6dfbd2e51acbc92ee33 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 09:07:00 +0000 Subject: [PATCH 1/7] Work in progress: RFC 9557, the Internet Extended Date/Time Format Types, code, the spec from RFC 9557's grammar and rules, seven statements and a proof skeleton. The proofs, the command-line request, the tests and the page are still to come. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs.lean | 1 + Proofs/Ixdtf/Main.lean | 85 ++++++++++++++++++ Proofs/Ixdtf/Parse.lean | 29 ++++++ Proofs/Ixdtf/Rules.lean | 21 +++++ Proofs/Ixdtf/Suffix.lean | 32 +++++++ Rfc3339.lean | 2 + Rfc3339/Ixdtf.lean | 155 ++++++++++++++++++++++++++++++++ Rfc3339/IxdtfTypes.lean | 43 +++++++++ Spec.lean | 89 ++++++++++++++++++ Spec/Ixdtf.lean | 190 +++++++++++++++++++++++++++++++++++++++ comparator.json | 9 +- 11 files changed, 655 insertions(+), 1 deletion(-) create mode 100644 Proofs/Ixdtf/Main.lean create mode 100644 Proofs/Ixdtf/Parse.lean create mode 100644 Proofs/Ixdtf/Rules.lean create mode 100644 Proofs/Ixdtf/Suffix.lean create mode 100644 Rfc3339/Ixdtf.lean create mode 100644 Rfc3339/IxdtfTypes.lean create mode 100644 Spec/Ixdtf.lean 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..016c6d5 --- /dev/null +++ b/Proofs/Ixdtf/Main.lean @@ -0,0 +1,85 @@ +/- + 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 + +theorem Spec.ixdtf_vectors : + (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]⟩]⟩) ∧ + -- Elective: an inconsistent zone, 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: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]⟩) ∧ + -- Critical: the four of section 3.3 + ((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) ∧ + -- Figures 1 and 2 of section 3.4 + ((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) ∧ + -- 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) ∧ + -- Refused by the grammar: an empty item, `.` and `..`, an upper case + -- key, an empty value, a time zone after a tag, `Z` as an offset + -- (it reads as a zone name), 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 <;> decide +kernel diff --git a/Proofs/Ixdtf/Parse.lean b/Proofs/Ixdtf/Parse.lean new file mode 100644 index 0000000..b1ba247 --- /dev/null +++ b/Proofs/Ixdtf/Parse.lean @@ -0,0 +1,29 @@ +/- + `parseExt` and `Ext.print` against the grammar. +-/ + +import Proofs.Ixdtf.Suffix +import Proofs.Main + +open Rfc3339 + +namespace Rfc3339.Proofs.Ixdtf + +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 + sorry + +theorem printExt_eq (e : Ext) (h : Spec.ExtValid e) : + e.print.toList = Spec.render e.stamp ++ Spec.renderSuffix e := by + sorry + +theorem parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e := by + sorry + +theorem parseExt_plain (s : String) (h : '[' ∉ s.toList) : + parseExt s = (parse s).map fun t => ⟨t, none, []⟩ := by + sorry + +end Rfc3339.Proofs.Ixdtf diff --git a/Proofs/Ixdtf/Rules.lean b/Proofs/Ixdtf/Rules.lean new file mode 100644 index 0000000..1e1f915 --- /dev/null +++ b/Proofs/Ixdtf/Rules.lean @@ -0,0 +1,21 @@ +/- + `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 + +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 + sorry + +theorem erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Spec.MustReject p e := by + sorry + +end Rfc3339.Proofs.Ixdtf diff --git a/Proofs/Ixdtf/Suffix.lean b/Proofs/Ixdtf/Suffix.lean new file mode 100644 index 0000000..1545036 --- /dev/null +++ b/Proofs/Ixdtf/Suffix.lean @@ -0,0 +1,32 @@ +/- + The suffix parser against the grammar of RFC 9557, section 4.1. +-/ + +import Rfc3339 +import Spec.Ixdtf + +open Rfc3339 + +namespace Rfc3339.Proofs.Ixdtf + +/-- `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 + sorry + +/-- 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 + sorry + +/-- 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 + sorry + +end Rfc3339.Proofs.Ixdtf 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.lean b/Spec.lean index 62189b7..201fbf1 100644 --- a/Spec.lean +++ b/Spec.lean @@ -15,6 +15,7 @@ import Rfc3339 import Spec.Defs import Spec.Leap +import Spec.Ixdtf open Rfc3339 @@ -246,3 +247,91 @@ 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 + +/-- The examples of sections 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. And strings the grammar + refuses. -/ +theorem Spec.ixdtf_vectors : + (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]⟩]⟩) ∧ + -- Elective: an inconsistent zone, 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: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]⟩) ∧ + -- Critical: the four of section 3.3 + ((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) ∧ + -- Figures 1 and 2 of section 3.4 + ((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) ∧ + -- 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) ∧ + -- Refused by the grammar: an empty item, `.` and `..`, an upper case + -- key, an empty value, a time zone after a tag, `Z` as an offset + -- (it reads as a zone name), 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/comparator.json b/comparator.json index 62d4328..38f57ef 100644 --- a/comparator.json +++ b/comparator.json @@ -25,7 +25,14 @@ "Spec.fromSiSeconds_iff", "Spec.fromSiSeconds_isSome", "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", From ba79dc86d73351740586475c468d86a096047f8c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 09:12:09 +0000 Subject: [PATCH 2/7] IXDTF: command-line request, differential tests, Temporal cross-check; two of three proof files The ixdtf request prints the printed form, the erroneous verdict for the example application and the first u-ca tag. The tests write RFC 9557's grammar and rules again in Python: 300,000 inputs with 0 failures, 6,992 of them IXDTF strings. The suffix parser's proofs are still open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Main.lean | 19 +++- Proofs/Ixdtf/Parse.lean | 99 ++++++++++++++++++-- Proofs/Ixdtf/Rules.lean | 72 ++++++++++++++- tests/CROSS-CHECK.md | 47 +++++++--- tests/TEST-RESULTS.md | 21 ++--- tests/cross_check.py | 82 +++++++++++++++++ tests/cross_check/ixdtf.js | 14 +++ tests/run_tests.py | 179 ++++++++++++++++++++++++++++++++++++- 8 files changed, 500 insertions(+), 33 deletions(-) create mode 100644 tests/cross_check/ixdtf.js diff --git a/Main.lean b/Main.lean index 84d2814..aaaad17 100644 --- a/Main.lean +++ b/Main.lean @@ -31,6 +31,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 @@ -41,11 +47,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 @@ -113,6 +121,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/Ixdtf/Parse.lean b/Proofs/Ixdtf/Parse.lean index b1ba247..85cb4c3 100644 --- a/Proofs/Ixdtf/Parse.lean +++ b/Proofs/Ixdtf/Parse.lean @@ -9,21 +9,110 @@ 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 - sorry + 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 - sorry + 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 := by - sorry +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 - sorry + 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 index 1e1f915..11205f9 100644 --- a/Proofs/Ixdtf/Rules.lean +++ b/Proofs/Ixdtf/Rules.lean @@ -10,12 +10,80 @@ 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 - sorry + 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 - sorry + 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/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index db3aa75..1f1e4b6 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -6,27 +6,48 @@ 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: 182162 +- Strings: 182091 - 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 | 3786 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| Go | accepts | offset hour above 23 or minute above 59 | 1986 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | -| Go | accepts | a field with one digit | 419 | `'0099-09-29T8:05:14.9-13:23'`, `'9972-03-01T8:16:47+02:02'` | -| Go | accepts | comma before the fraction | 3 | `'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 | 3786 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| rfc3339-validator | rejects | year 0000 | 1243 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | -| rfc3339-validator | accepts | line break at the end | 869 | `'4244-06-01T08:05:55.054876690884+00:00\n'`, `'5263-10-30T07:22:33.52-07:24\n'` | +| Go | rejects | lower case t or z | 19027 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| Go | rejects | second 60 | 3680 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| Go | accepts | offset hour above 23 or minute above 59 | 1970 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | +| Go | accepts | a field with one digit | 435 | `'0099-09-29T8:05:14.9-13:23'`, `'6796-03-01T8:13:08+17:53'` | +| 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 | 19027 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | +| rfc3339-validator | rejects | second 60 | 3680 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | +| rfc3339-validator | rejects | year 0000 | 1224 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | +| rfc3339-validator | accepts | line break at the end | 855 | `'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: 24191. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 3390. -- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8700. Different: 0. - +- Timestamps known valid by the table, from 1972 on, given to ERFA: 19637. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 1965. +- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8666. 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: 6992, of which this project reads 5193. The same answer, read or refused: 2737. + +Where Temporal differs from this project, by the first category that fits the string: + +| Temporal | Category | Strings | Example | +| --- | --- | --- | --- | +| refuses | a critical item, which Temporal refuses when it does not act on it | 2291 | `'2022-07-08T00:14:07+01:00[!Europe/Paris]'`, `'2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]'` | +| refuses | an experimental key | 676 | `'1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]'`, `'1972-02-01T13:53:54-10:37[_=X1][u-ca=hebrew]'` | +| refuses | an unknown elective key | 645 | `'2022-07-08T00:14:07+01:00[knort=blargel]'`, `'4960-06-30T10:33:21-04:31[knort=gregory]'` | +| refuses | a fraction of more than nine digits, finer than Temporal's nanoseconds | 418 | `'5720-01-31T23:59:60.26153083810657+00:00[Etc/GMT+5][!_=a-b][_foo=japanese]'`, `'2490-07-01t16:59:07.026416563048384470366623+04:19[a-b_c9=chinese]'` | +| refuses | a calendar Temporal does not know | 119 | `'3221-10-31T23:59:60+00:00[a.b-c+d_e][u-ca=blargel]'`, `'2022-07-08T00:14:07+00:00[u-ca=0]'` | +| refuses | a repeated elective `u-ca` | 64 | `'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 one-part time zone name | 32 | `'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]'` | +| refuses | another time zone name | 7 | `'2022-07-08T00:14:07Z[Etc/G.T+5]'`, `'9167-04-30T21:08:20.7+11:30[Etc/GMT+Z]'` | +| accepts | a `[` inside an item | 1 | `'1019-06-30T05:31:37+00:34[+23:59][u-ca=blargel[]'` | +| 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 c2a5a65..6b5d002 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: 67969 of the inputs are mutated timestamps -- By kind: compare 29344, error 35, fromsi 9381, fromunix 44688, grid 16998, known 34402, mutated 67969, near miss 29160, valid 68023 -- Strings parsed: 182150, of which 83488 accepted (4661 with a leap second) and 98662 rejected -- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77297 -- Pairs ordered: 29344 (9831 before, 8253 same instant, 9780 after, 1480 with a string rejected) -- Unix seconds turned back into timestamps: 44688, of which 704 outside years 0000 to 9999 +- Mutated: 67687 of the inputs are mutated timestamps +- By kind: compare 29458, error 39, fromsi 9356, fromunix 44579, grid 16998, ixdtf 6992, known 27497, mutated 67687, near miss 29289, valid 68105 +- Strings parsed: 182079, of which 83586 accepted (4568 with a leap second) and 98493 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77505 +- Pairs ordered: 29458 (9861 before, 8209 same instant, 9923 after, 1465 with a string rejected) +- Unix seconds turned back into timestamps: 44579, of which 657 outside years 0000 to 9999 - Leap second table: /usr/share/zoneinfo/leap-seconds.list, 28 lines, 27 leap seconds, expires 2027-06-28 -- Timestamps checked against the table (`known`): 34402, of which 303 leap seconds of the table, 6821 with a second 60 it does not list, and 0 rejected -- SI seconds turned back into timestamps (`fromsi`): 9381, of which 27 leap seconds and 681 outside 1972 to 9999 -- Malformed requests answered `error`: 35 of 35 +- Timestamps checked against the table (`known`): 27497, of which 236 leap seconds of the table, 5895 with a second 60 it does not list, and 0 rejected +- SI seconds turned back into timestamps (`fromsi`): 9356, of which 27 leap seconds and 690 outside 1972 to 9999 +- RFC 9557 strings (`ixdtf`): 6992, of which 5193 read, 3083 of them erroneous for the example application, and 1799 refused +- Malformed requests answered `error`: 39 of 39 - 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 ef0e9b5..59a5ae2 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,81 @@ 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 item, which Temporal refuses when it does not act on it" + 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 tags[0][2] not in run_tests.IX_CALENDARS: + return "a calendar Temporal does not know" + if zone and zone[1][0] == "name" and "/" not in zone[1][1]: + return "a one-part time zone name" + if zone and zone[1][0] == "name": + 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 +332,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 a26e2a8..aebc857 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -50,6 +50,18 @@ timestamps. `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 3.3, 3.4 and 4.2, + 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, a bracket or `!` moved, 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 @@ -200,6 +212,152 @@ 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]", +] +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"]] + + +def ix_offset_text(rng): + m = rng.choice([0, 60, 120, -480, 330, -1439, 1439]) + return ("+" if m >= 0 else "-") + 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 @@ -548,6 +706,10 @@ def same_instant_pair(rng): ("fromsi +1", "a plus sign"), ("fromsi 1.5", "a fraction"), ("fromsi 1 2", "two numbers"), + ("ixdtf", "no argument"), + ("ixdtf 3", "an odd number of hex digits"), + ("ixdtf 30 30", "two arguments"), + ("ixdtf ff", "not UTF-8"), ] # A last line with no LF must still be answered. @@ -577,6 +739,8 @@ def cases(seed, count): fixed.append(("known", f"known {hexed(s)}", known(s), False)) for n in si_grid(): fixed.append(("fromsi", f"fromsi {n}", from_si(n), False)) + for s in IX_EXAMPLES: + fixed.append(("ixdtf", f"ixdtf {hexed(s)}", ixdtf(s), False)) for req, _ in MALFORMED: fixed.append(("error", req, "error", False)) made = 0 @@ -585,6 +749,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: s = random_valid(rng) if rng.random() < 0.8 else leap_pair(rng)[0] yield ("known", f"known {hexed(s)}", known(s), False) @@ -741,8 +910,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(): @@ -837,6 +1007,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"] @@ -868,6 +1039,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}", From 18487604d325af03daf04eef0e13b0337c6cb57c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 09:13:39 +0000 Subject: [PATCH 3/7] IXDTF tests: write out the edges of the grammar and the rules Planted bugs that the random inputs caught only a few times (a zone part of .., an offset out of range, -00:00, a critical tag repeated with the same values) now each have fixed cases, with 48 edge strings in all. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- tests/TEST-RESULTS.md | 16 ++++++++-------- tests/run_tests.py | 27 +++++++++++++++++++++++++-- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 6b5d002..8873547 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,16 +6,16 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 300000 -- Mutated: 67687 of the inputs are mutated timestamps -- By kind: compare 29458, error 39, fromsi 9356, fromunix 44579, grid 16998, ixdtf 6992, known 27497, mutated 67687, near miss 29289, valid 68105 -- Strings parsed: 182079, of which 83586 accepted (4568 with a leap second) and 98493 rejected -- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77505 -- Pairs ordered: 29458 (9861 before, 8209 same instant, 9923 after, 1465 with a string rejected) -- Unix seconds turned back into timestamps: 44579, of which 657 outside years 0000 to 9999 +- Mutated: 67675 of the inputs are mutated timestamps +- By kind: compare 29452, error 39, fromsi 9355, fromunix 44573, grid 16998, ixdtf 7038, known 27497, mutated 67675, near miss 29283, valid 68090 +- Strings parsed: 182046, of which 83570 accepted (4568 with a leap second) and 98476 rejected +- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77491 +- Pairs ordered: 29452 (9859 before, 8207 same instant, 9921 after, 1465 with a string rejected) +- Unix seconds turned back into timestamps: 44573, of which 657 outside years 0000 to 9999 - Leap second table: /usr/share/zoneinfo/leap-seconds.list, 28 lines, 27 leap seconds, expires 2027-06-28 - Timestamps checked against the table (`known`): 27497, of which 236 leap seconds of the table, 5895 with a second 60 it does not list, and 0 rejected -- SI seconds turned back into timestamps (`fromsi`): 9356, of which 27 leap seconds and 690 outside 1972 to 9999 -- RFC 9557 strings (`ixdtf`): 6992, of which 5193 read, 3083 of them erroneous for the example application, and 1799 refused +- SI seconds turned back into timestamps (`fromsi`): 9355, of which 27 leap seconds and 690 outside 1972 to 9999 +- RFC 9557 strings (`ixdtf`): 7038, of which 5216 read, 3089 of them erroneous for the example application, and 1822 refused - Malformed requests answered `error`: 39 of 39 - 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 diff --git a/tests/run_tests.py b/tests/run_tests.py index aebc857..02684e0 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -55,7 +55,8 @@ 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 3.3, 3.4 and 4.2, + tag. The inputs are every example of sections 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 @@ -299,6 +300,28 @@ def ixdtf(s): "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]", "1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]", ] +# 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]", +] 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", "_"] @@ -739,7 +762,7 @@ def cases(seed, count): fixed.append(("known", f"known {hexed(s)}", known(s), False)) for n in si_grid(): fixed.append(("fromsi", f"fromsi {n}", from_si(n), False)) - for s in IX_EXAMPLES: + for s in IX_EXAMPLES + IX_EDGES: fixed.append(("ixdtf", f"ixdtf {hexed(s)}", ixdtf(s), False)) for req, _ in MALFORMED: fixed.append(("error", req, "error", False)) From 76bd131ee3a1a1d4534b1d3706d051aeb2643895 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 09:21:37 +0000 Subject: [PATCH 4/7] Prove the IXDTF suffix parser: all seven IXDTF statements are proved Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs/Ixdtf/Suffix.lean | 583 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 580 insertions(+), 3 deletions(-) diff --git a/Proofs/Ixdtf/Suffix.lean b/Proofs/Ixdtf/Suffix.lean index 1545036..f3a5ad5 100644 --- a/Proofs/Ixdtf/Suffix.lean +++ b/Proofs/Ixdtf/Suffix.lean @@ -4,29 +4,606 @@ 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 - sorry + 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 - sorry + 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 - sorry + 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 From 7294c517e44788533dd9b96ad6db0629468f9a01 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 10:11:33 +0000 Subject: [PATCH 5/7] Check the IXDTF vectors through parseExt_iff, and write the RFC 9557 docs nanoda ran out of stack evaluating parseSuffix on the long examples. The vectors that read a string now get their Ext from parseExt_iff, with the grammar's checks made by the code's own functions, so no kernel runs the whole parser. All six kernels accept. README, SPEC.md and bar.toml now cover parseExt, Ext.print, Ext.lookup and Ext.erroneous, and list Spec/Ixdtf.lean and Rfc3339/IxdtfTypes.lean as part of the specification. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs/Ixdtf/Main.lean | 90 +++++++++++++++++++++++++++++++++++++++++- README.md | 31 +++++++++++---- SPEC.md | 46 +++++++++++++++++++-- bar.toml | 12 ++++-- 4 files changed, 162 insertions(+), 17 deletions(-) diff --git a/Proofs/Ixdtf/Main.lean b/Proofs/Ixdtf/Main.lean index 016c6d5..495469c 100644 --- a/Proofs/Ixdtf/Main.lean +++ b/Proofs/Ixdtf/Main.lean @@ -34,6 +34,44 @@ 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⟩ + theorem Spec.ixdtf_vectors : (parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" = some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, @@ -82,4 +120,54 @@ theorem Spec.ixdtf_vectors : 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 <;> decide +kernel + and_intros + · 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 "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: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: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[_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 + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel + · decide +kernel diff --git a/README.md b/README.md index 484b59a..e9954f5 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, 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: an RFC 3339 timestamp, as `parse` reads it, 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` | +| The examples of sections 3.3, 3.4 and 4.2, read and judged by an example application, and 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. +- 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` and `parse`. They accept second 60 at 23:59 UTC at the end of any month, where section 5.7 allows it only at the end of months in which a leap second occurs; `isValidKnown` checks that against the table. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. - The table after its expiry date, 28 June 2027. `isValidKnown` refuses second 60 at any month end the table does not list, and `siSeconds` and `taiMinusUtc` count no leap second after 2016. If one is ever announced, the table in the spec and the code's list must change together, and the spec approved again. The table is what tzdata publishes from IERS Bulletin C; that it matches the IERS record is trusted, not proved. - SI seconds and TAI − UTC before 1972. UTC then ran on seconds of varying length, with TAI − UTC not a whole number of seconds. Before 1972, `Spec.siSeconds_eq` makes `siSeconds` Unix seconds less 63072000, 86400 to a day, which are not SI seconds there, and `taiMinusUtc` gives 10, which means nothing there; the tool's `known` request prints `-` for TAI − UTC. - The table itself. `Spec/Leap.lean` copies tzdata's `leap-seconds.list` (tzdata 2026e, updated through IERS Bulletin C, expiring 28 June 2027) line for line. That copy is part of the specification: the reviewer checks it against the file, and the differential tests check the code against the copy of the file on the test machine, but no proof does. - Unix seconds at a leap second. They count second 60 as the first second of the next minute, as POSIX time does, so a leap second and the second after it give the same number. `compareInstant` does not use them, and puts the leap second first. `fromUnixSeconds` turns that number into the second after the leap second, so a round trip through Unix seconds loses a leap second, and `9999-12-31T23:59:60Z` gives `none`. -- Forms outside RFC 3339 are not supported, by design: +- 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. Temporal refuses what it does not act on: critical items, experimental and unknown keys, calendars it does not know, a repeated `u-ca`, and fractions finer than nanoseconds. Of the strings this project reads, it also refuses one-part time zone names and names that are not in its time zone database. It accepts three kinds of string that this project refuses as RFC 9557 does: a `[` inside an item, 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/SPEC.md b/SPEC.md index 08736c3..24f844e 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, 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,12 +133,20 @@ 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` | +| The examples of sections 3.3, 3.4 and 4.2 are read, and are erroneous for the example application exactly where the RFC says; 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`. @@ -121,3 +158,4 @@ The differential tests compare the tool with two oracles: - Python's `datetime` and `calendar` modules: month lengths, offset arithmetic, seconds since the epoch, `datetime.fromisoformat` on every accepted string it can hold, and the UTC timestamp for a number of seconds. `datetime` holds no year 0, so dates there are moved by 400 years, one cycle of the Gregorian calendar, for the arithmetic. - A copy of the rules above, written in Python from the RFC. - For leap seconds, tzdata's `leap-seconds.list` on the test machine, read by the test script itself, with the SI seconds and TAI − UTC worked out from it in Python. +- 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/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. From c545a9d4a55d278f1353fd5778b9469044d51097 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 10:51:15 +0000 Subject: [PATCH 6/7] Fix what the IXDTF pre-review found: every RFC example as a vector, test gaps, wording Spec.ixdtf_vectors now has every example of RFC 9557, sections 1.2, 3.3, 3.4 and 4.2, critical zones that agree with the offset, a critical -00:00 zone that does not, and [Z] read as a zone name. The page says parseExt keeps parse's relaxation on second 60. The tests add -00:00 zones, a value list sharing a first part, and two critical tags with one key. The Temporal categories follow what that Temporal refuses. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs/Ixdtf/Main.lean | 98 ++++++++++++++++++++++++++++++++++++------ README.md | 8 ++-- SPEC.md | 6 +-- Spec.lean | 64 ++++++++++++++++++++------- tests/cross_check.py | 13 +++--- tests/run_tests.py | 32 ++++++++++---- 6 files changed, 172 insertions(+), 49 deletions(-) diff --git a/Proofs/Ixdtf/Main.lean b/Proofs/Ixdtf/Main.lean index 495469c..622cff6 100644 --- a/Proofs/Ixdtf/Main.lean +++ b/Proofs/Ixdtf/Main.lean @@ -72,24 +72,54 @@ theorem vx_parseExt (s : String) (e : Ext) (dt : List Char) (hv : vx_validB e = 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 : - (parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" = + -- 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]" = + [⟨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]⟩]⟩) ∧ - -- Elective: an inconsistent zone, an unknown key, repeated keys + [⟨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]⟩) ∧ - -- Critical: the four of section 3.3 + ((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 @@ -98,7 +128,7 @@ theorem Spec.ixdtf_vectors : (·.erroneous Spec.exampleProcessor) = some true) ∧ ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Spec.exampleProcessor) = some true) ∧ - -- Figures 1 and 2 of section 3.4 + -- 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) = @@ -107,12 +137,18 @@ theorem Spec.ixdtf_vectors : some false) ∧ ((parseExt "2022-07-08T00:14:07Z[Europe/London]").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) ∧ + -- 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, `Z` as an offset - -- (it reads as a zone name), an offset out of range + -- 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 ∧ @@ -121,13 +157,37 @@ theorem Spec.ixdtf_vectors : 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 @@ -137,6 +197,9 @@ theorem Spec.ixdtf_vectors : · 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 @@ -161,9 +224,18 @@ theorem Spec.ixdtf_vectors : · 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[_foo=bar][_baz=bat]" ⟨⟨1996, 12, 19, 16, 39, 57, [], (.minus 8 0)⟩, none, [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ + · 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 diff --git a/README.md b/README.md index 7c2c975..a6b1ad7 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. 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, 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. +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. @@ -59,19 +59,19 @@ 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: an RFC 3339 timestamp, as `parse` reads it, 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` | +| `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` | -| The examples of sections 3.3, 3.4 and 4.2, read and judged by an example application, and 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` | +| 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, 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` 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. +- 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. diff --git a/SPEC.md b/SPEC.md index 24f844e..839b401 100644 --- a/SPEC.md +++ b/SPEC.md @@ -79,7 +79,7 @@ RFC 9557, the Internet Extended Date/Time Format (IXDTF), updates RFC 3339. Afte - 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, and a string with no suffix exactly as `parse` reads it. `Ext.print` writes an `Ext` back, with `T` and `Z` in upper case. +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. @@ -139,7 +139,7 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | 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` | -| The examples of sections 3.3, 3.4 and 4.2 are read, and are erroneous for the example application exactly where the RFC says; strings the grammar refuses are not read. | `Spec.ixdtf_vectors` | +| 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. @@ -153,7 +153,7 @@ Together, these fix every output for valid input. ## 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. diff --git a/Spec.lean b/Spec.lean index f754f2c..e33771a 100644 --- a/Spec.lean +++ b/Spec.lean @@ -298,28 +298,54 @@ theorem Spec.lookup_iff (e : Ext) (k : List Char) (t : Tag) : theorem Spec.erroneous_iff (p : Processor) (e : Ext) : e.erroneous p = true ↔ Spec.MustReject p e := sorry -/-- The examples of sections 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. And strings the grammar - refuses. -/ +/-- 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 : - (parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]" = + -- 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]" = + [⟨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]⟩]⟩) ∧ - -- Elective: an inconsistent zone, an unknown key, repeated keys + [⟨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]⟩) ∧ - -- Critical: the four of section 3.3 + ((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 @@ -328,7 +354,7 @@ theorem Spec.ixdtf_vectors : (·.erroneous Spec.exampleProcessor) = some true) ∧ ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Spec.exampleProcessor) = some true) ∧ - -- Figures 1 and 2 of section 3.4 + -- 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) = @@ -337,12 +363,18 @@ theorem Spec.ixdtf_vectors : some false) ∧ ((parseExt "2022-07-08T00:14:07Z[Europe/London]").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) ∧ + -- 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, `Z` as an offset - -- (it reads as a zone name), an offset out of range + -- 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 ∧ diff --git a/tests/cross_check.py b/tests/cross_check.py index f7e88ea..b74ebdf 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -195,18 +195,21 @@ def ix_category(s, ours_ok): 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 item, which Temporal refuses when it does not act on it" + 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 tags[0][2] not in run_tests.IX_CALENDARS: - return "a calendar Temporal does not know" - if zone and zone[1][0] == "name" and "/" not in zone[1][1]: - return "a one-part time zone name" + 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("[") diff --git a/tests/run_tests.py b/tests/run_tests.py index 9424962..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 @@ -56,14 +56,15 @@ 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 3.3, 3.4 and 4.2, the + 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, a bracket or `!` moved, a key in - upper case, `.` or `..` as a zone part, an empty item or value, a - time zone after a tag; + 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 @@ -306,7 +307,7 @@ def ixdtf(s): "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]", + "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 = [ @@ -329,16 +330,31 @@ def ixdtf(s): "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"]] +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]) - return ("+" if m >= 0 else "-") + f"{abs(m) // 60:02d}:{abs(m) % 60:02d}" + 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): From 83d4ba8b5340e564db03382dba942d8eb5b3abe1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 10:51:34 +0000 Subject: [PATCH 7/7] Rerun the tests and the cross-check, and give Temporal's reasons as observed Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 +- tests/CROSS-CHECK.md | 38 ++++++++++++++++++-------------------- tests/TEST-RESULTS.md | 18 +++++++++--------- 3 files changed, 28 insertions(+), 30 deletions(-) diff --git a/README.md b/README.md index a6b1ad7..f461fb1 100644 --- a/README.md +++ b/README.md @@ -107,7 +107,7 @@ 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. Temporal refuses what it does not act on: critical items, experimental and unknown keys, calendars it does not know, a repeated `u-ca`, and fractions finer than nanoseconds. Of the strings this project reads, it also refuses time zone names that are not in its time zone database, such as `a.b-c+d_e` and `Etc/G.T+5`. It accepts three kinds of string that this project refuses as RFC 9557 does: a `[` inside an item, a zone offset with no colon, and a stray `]`. +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. diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 445ce86..dd0b090 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -6,48 +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: 181892 +- 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 | 19069 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | -| Go | rejects | second 60 | 3679 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| Go | accepts | offset hour above 23 or minute above 59 | 1947 | `'2000-01-01T00:00:00+24:00'`, `'2000-01-01T00:00:00+23:60'` | -| Go | accepts | a field with one digit | 444 | `'6796-03-01T8:13:08+17:53'`, `'2289-10-02T3:10:29.2-00:00'` | +| 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 | 19069 | `'1985-04-12t23:20:50.52z'`, `'2100-10-31t02:52:09+00:50'` | -| rfc3339-validator | rejects | second 60 | 3679 | `'1990-12-31T23:59:60Z'`, `'1990-12-31T15:59:60-08:00'` | -| rfc3339-validator | rejects | year 0000 | 1222 | `'0000-01-01T00:00:00Z'`, `'0000-01-01T12:00:00Z'` | -| rfc3339-validator | accepts | line break at the end | 878 | `'4244-06-01T08:05:55.054876690884+00:00\n'`, `'5263-10-30T07:22:33.52-07:24\n'` | +| 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: 18819. Different SI seconds since 1972 or TAI - UTC: 0. Before 1972, where TAI - UTC was not a whole number of seconds, not compared: 1716. -- SI seconds turned back into timestamps, of which 27 leap seconds, and given to ERFA for their SI seconds: 8656. 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: 7157, of which this project reads 5299. The same answer, read or refused: 2822. +- 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 item, which Temporal refuses when it does not act on it | 2343 | `'2022-07-08T00:14:07+01:00[!Europe/Paris]'`, `'2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]'` | -| refuses | an experimental key | 682 | `'1996-12-19T16:39:57-08:00[_foo=bar][_baz=bat]'`, `'2022-07-08T00:14:07Z[_=x]'` | +| 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 | 418 | `'5720-01-31T23:59:60.26153083810657+00:00[Etc/GMT+5][!_=a-b][_foo=japanese]'`, `'3938-05-31T07:00:58.533659862016880639560673568684585171z[_x]'` | -| refuses | a calendar Temporal does not know | 124 | `'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` | 68 | `'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 one-part time zone name | 31 | `'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]'` | -| refuses | another time zone name | 6 | `'2022-07-08T00:14:07Z[Etc/G.T+5]'`, `'9167-04-30T21:08:20.7+11:30[Etc/GMT+Z]'` | -| accepts | a `[` inside an item | 1 | `'1019-06-30T05:31:37+00:34[+23:59][u-ca=blargel[]'` | +| 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 9694fe8..4a7fa4c 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,16 +6,16 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 300000 -- Mutated: 67662 of the inputs are mutated timestamps -- By kind: compare 29524, error 48, fromsi 9358, fromunix 44565, grid 16998, ixdtf 7157, known 27468, mutated 67662, near miss 29208, valid 68012 -- Strings parsed: 181880, of which 83519 accepted (4589 with a leap second) and 98361 rejected -- Accepted strings also read by `datetime.fromisoformat`, with the same fields, offset and seconds: 77424 -- Pairs ordered: 29524 (9906 before, 8293 same instant, 9859 after, 1466 with a string rejected) -- Unix seconds turned back into timestamps: 44565, of which 648 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`): 27468, of which 224 leap seconds of the table, 5703 with a second 60 it does not list, and 1230 rejected -- SI seconds turned back into timestamps (`fromsi`): 9358, of which 27 leap seconds and 702 outside 1972 to 9999 -- RFC 9557 strings (`ixdtf`): 7157, of which 5299 read, 3126 of them erroneous for the example application, and 1858 refused +- 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