From 356426b3dece80cba3a71bf962ddb69aef7a0f88 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:45:00 -0500 Subject: [PATCH 1/3] Prove early calendar vector and record verification boundaries --- Proofs/FromUnix/Main.lean | 1 + SPEC.md | 26 ++++++++++++++++++++++++++ Spec.lean | 1 + 3 files changed, 28 insertions(+) diff --git a/Proofs/FromUnix/Main.lean b/Proofs/FromUnix/Main.lean index 39cb49d..442be69 100644 --- a/Proofs/FromUnix/Main.lean +++ b/Proofs/FromUnix/Main.lean @@ -119,6 +119,7 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) : omega theorem Spec.fromUnixSeconds_vectors : + Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧ diff --git a/SPEC.md b/SPEC.md index 839b401..075dbc9 100644 --- a/SPEC.md +++ b/SPEC.md @@ -159,3 +159,29 @@ The differential tests compare the tool with these oracles: - 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. + +## Follow-up verification record + +`Rfc3339.Proofs.Leap.leapKey_table` in `Proofs/Leap/Table.lean` +proves that the implementation's ordered list of leap-second keys equals +the keys derived from `Spec.leapTable.tail`. `Spec.isValidKnown_iff` uses +that equality. The literal table's agreement with IERS remains trusted. + +Before the table expires on 28 June 2027, obtain the current IERS Bulletin C +and tzdata leap-seconds.list, compare the literal table in `Spec/Leap.lean`, +and update its source and expiry record. If an entry changes, update +`Rfc3339/Leap.lean` in the same change, rebuild the table equality proof, +and rerun the full bar and differential suite. Have a spec reviewer check +the replacement source. Expiry alone does not announce a leap second. + +The external Go, Temporal and ERFA cross-check remains a one-off comparison +(`tests/CROSS-CHECK.md`), outside the verified bar. The 0096-12-31 UTC +midnight case is now also a kernel-computed `Spec.fromUnixSeconds_vectors` +case, rather than only a differential calendar-grid case. + +The long IXDTF vectors in `Proofs/Ixdtf/Main.lean` use `vx_validB_sound` +and the parser equivalence proof; they do not directly execute the whole +parser in the kernel. Their shorter timestamp components and grammar +checks are kernel-computed. The existing processor vectors are examples +of one tag policy; this slice provides no worked alternative tag-set +application. `Spec.erroneous_iff` quantifies over every `Processor`. diff --git a/Spec.lean b/Spec.lean index e33771a..50fe725 100644 --- a/Spec.lean +++ b/Spec.lean @@ -166,6 +166,7 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) : signed 32-bit count reaches; the second before the epoch; the ends of the range, and one second past each. -/ theorem Spec.fromUnixSeconds_vectors : + Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧ From 68241992c7c421ca246ee6d78e05c39ac8723d8e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 20:01:15 +0000 Subject: [PATCH 2/3] List the 0096-12-31 vector wherever the vectors are listed README.md, SPEC.md and the docstring of Spec.fromUnixSeconds_vectors now name the new year-start case, so the claims match the theorem. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf --- README.md | 2 +- SPEC.md | 2 +- Spec.lean | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index f461fb1..262d945 100644 --- a/README.md +++ b/README.md @@ -50,7 +50,7 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF | A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` | | `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one, at most one, that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` | | `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Spec.fromUnixSeconds_isSome` | -| `fromUnixSeconds` gives the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` | +| `fromUnixSeconds` gives 0096-12-31T00:00:00Z, the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` | | The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` | | `isValidKnown` decides section 5.7 with the table of leap seconds. It allows second 60 only at one of the table's leap seconds, at the same instant whatever the offset. The table is the one in `Spec/Leap.lean`. The code keeps its own list of months, and the proof shows the two agree. | `Spec.isValidKnown_iff` | | `siSeconds` is the Unix seconds since 1972-01-01T00:00:00Z, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds; so a leap second, the second before it and the second after it get three numbers in a row. Before 1972 the number is Unix seconds, 86400 to a day. | `Spec.siSeconds_eq` | diff --git a/SPEC.md b/SPEC.md index 075dbc9..4f72cb6 100644 --- a/SPEC.md +++ b/SPEC.md @@ -125,7 +125,7 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Spec.syntax_vectors` | | `fromUnixSeconds s` is `t` exactly when `t` is valid, in UTC, with no fraction and a second of at most 59, and names `s`. | `Spec.fromUnixSeconds_iff` | | `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z. | `Spec.fromUnixSeconds_isSome` | -| The epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` | +| 0096-12-31 at midnight, the epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` | | `isValidKnown` decides `Spec.ValidKnown`: `Spec.Valid`, with second 60 only at a leap second of the table. | `Spec.isValidKnown_iff` | | `siSeconds` is Unix seconds since 1972 and one more for each leap second of the table before the timestamp. | `Spec.siSeconds_eq` | | On whole seconds valid by the table, `siSeconds` gives the order of the instants. | `Spec.siSeconds_order` | diff --git a/Spec.lean b/Spec.lean index 50fe725..8d53160 100644 --- a/Spec.lean +++ b/Spec.lean @@ -162,7 +162,8 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) : Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧ s ≤ Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry -/-- The epoch; the example of section 5.8; a leap day; the last second a +/-- 0096-12-31 at midnight, from the year-start grid; the epoch; the + example of section 5.8; a leap day; the last second a signed 32-bit count reaches; the second before the epoch; the ends of the range, and one second past each. -/ theorem Spec.fromUnixSeconds_vectors : From ceea62695e207209dadfd34bbe592d00ad73164a Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:51:07 -0500 Subject: [PATCH 3/3] Move proof modules and spec names under Rfc3339 --- Main.lean | 6 +- Proofs.lean | 10 -- README.md | 76 ++++---- Rfc3339/IxdtfTypes.lean | 2 +- Rfc3339/Proofs.lean | 10 ++ {Proofs => Rfc3339/Proofs}/DayNumber.lean | 38 ++-- {Proofs => Rfc3339/Proofs}/Format.lean | 38 ++-- {Proofs => Rfc3339/Proofs}/Fraction.lean | 32 ++-- {Proofs => Rfc3339/Proofs}/FromUnix/Day.lean | 30 ++-- {Proofs => Rfc3339/Proofs}/FromUnix/Main.lean | 42 ++--- {Proofs => Rfc3339/Proofs}/Instant.lean | 42 ++--- {Proofs => Rfc3339/Proofs}/Ixdtf/Main.lean | 78 ++++---- {Proofs => Rfc3339/Proofs}/Ixdtf/Parse.lean | 46 ++--- {Proofs => Rfc3339/Proofs}/Ixdtf/Rules.lean | 22 +-- {Proofs => Rfc3339/Proofs}/Ixdtf/Suffix.lean | 148 ++++++++-------- {Proofs => Rfc3339/Proofs}/Leap/FromSi.lean | 58 +++--- {Proofs => Rfc3339/Proofs}/Leap/Main.lean | 44 ++--- {Proofs => Rfc3339/Proofs}/Leap/Order.lean | 8 +- {Proofs => Rfc3339/Proofs}/Leap/Si.lean | 44 ++--- {Proofs => Rfc3339/Proofs}/Leap/Table.lean | 56 +++--- {Proofs => Rfc3339/Proofs}/Main.lean | 100 +++++------ {Proofs => Rfc3339/Proofs}/Valid.lean | 74 ++++---- Spec.lean => Rfc3339/Spec.lean | 166 +++++++++--------- {Spec => Rfc3339/Spec}/Defs.lean | 116 ++++++------ {Spec => Rfc3339/Spec}/Ixdtf.lean | 68 +++---- {Spec => Rfc3339/Spec}/Leap.lean | 44 ++--- Rfc3339/Types.lean | 4 +- SPEC.md | 123 ++++++------- bar.toml | 2 +- comparator.json | 68 +++---- lakefile.toml | 8 +- tests/run_tests.py | 2 +- 32 files changed, 805 insertions(+), 800 deletions(-) delete mode 100644 Proofs.lean create mode 100644 Rfc3339/Proofs.lean rename {Proofs => Rfc3339/Proofs}/DayNumber.lean (56%) rename {Proofs => Rfc3339/Proofs}/Format.lean (85%) rename {Proofs => Rfc3339/Proofs}/Fraction.lean (85%) rename {Proofs => Rfc3339/Proofs}/FromUnix/Day.lean (85%) rename {Proofs => Rfc3339/Proofs}/FromUnix/Main.lean (76%) rename {Proofs => Rfc3339/Proofs}/Instant.lean (72%) rename {Proofs => Rfc3339/Proofs}/Ixdtf/Main.lean (85%) rename {Proofs => Rfc3339/Proofs}/Ixdtf/Parse.lean (64%) rename {Proofs => Rfc3339/Proofs}/Ixdtf/Rules.lean (79%) rename {Proofs => Rfc3339/Proofs}/Ixdtf/Suffix.lean (77%) rename {Proofs => Rfc3339/Proofs}/Leap/FromSi.lean (86%) rename {Proofs => Rfc3339/Proofs}/Leap/Main.lean (63%) rename {Proofs => Rfc3339/Proofs}/Leap/Order.lean (90%) rename {Proofs => Rfc3339/Proofs}/Leap/Si.lean (61%) rename {Proofs => Rfc3339/Proofs}/Leap/Table.lean (74%) rename {Proofs => Rfc3339/Proofs}/Main.lean (55%) rename {Proofs => Rfc3339/Proofs}/Valid.lean (65%) rename Spec.lean => Rfc3339/Spec.lean (74%) rename {Spec => Rfc3339/Spec}/Defs.lean (57%) rename {Spec => Rfc3339/Spec}/Ixdtf.lean (71%) rename {Spec => Rfc3339/Spec}/Leap.lean (71%) diff --git a/Main.lean b/Main.lean index 865ff9e..842a0dc 100644 --- a/Main.lean +++ b/Main.lean @@ -34,7 +34,7 @@ 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 + application of `Rfc3339.Spec.exampleProcessor` must treat it as erroneous (`true` or `false`), and the values of the first `u-ca` tag joined by `-`, or `-`; or REJECT @@ -54,7 +54,7 @@ -/ import Rfc3339 -import Spec.Ixdtf +import Rfc3339.Spec.Ixdtf open Rfc3339 @@ -129,7 +129,7 @@ def request (line : String) : Option String := 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}" + s!"OK\t{e.print}\t{e.erroneous Rfc3339.Spec.exampleProcessor}\t{cal}" | none => "REJECT" | ["fromsi", n] => do let s ← decimal n diff --git a/Proofs.lean b/Proofs.lean deleted file mode 100644 index 1eedfed..0000000 --- a/Proofs.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - The proofs, under the names the challenge file gives them. The - theorems themselves are in `Proofs/Main.lean`, from the lemmas in the - other files. --/ - -import Proofs.Main -import Proofs.FromUnix.Main -import Proofs.Leap.Main -import Proofs.Ixdtf.Main diff --git a/README.md b/README.md index 262d945..b5d2184 100644 --- a/README.md +++ b/README.md @@ -34,50 +34,50 @@ For each timestamp it prints the timestamp as written, with `T` and `Z` in upper ## 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`; 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/`. +The statements are in `Rfc3339/Spec.lean`. The definitions they use, written from the RFC, are in `Rfc3339/Spec/Defs.lean`; those for the leap second table, with the table itself, are in `Rfc3339/Spec/Leap.lean`; those for RFC 9557, with its grammar, are in `Rfc3339/Spec/Ixdtf.lean`; and the types are in `Rfc3339/Types.lean` and `Rfc3339/IxdtfTypes.lean`. The proofs are in `Rfc3339/Proofs/`. | Claim | Theorem | |-------|---------| -| `isValid` decides the rules of RFC 3339, sections 5.6 and 5.7. Every field is in its range. The day exists in its month, with the leap years of Appendix C. Second 60 falls only at 23:59 UTC on the last day of a month. Section 5.7 allows it only in months that had a leap second; `isValid` uses no table of them, so any month is accepted. | `Spec.isValid_iff` | -| A valid timestamp prints as the grammar of section 5.6 writes it, with `T` and `Z` in upper case. | `Spec.print_eq` | -| `parse` returns a timestamp exactly when the timestamp is valid and the string is how it prints, with `T` and `Z` in either case. So `parse` accepts nothing outside the grammar and those rules, rejects nothing inside them, and returns the fields as written. | `Spec.parse_iff` | -| What `parse` returns is valid; for example, 30 February never passes. | `Spec.parse_valid` | -| Printing then parsing gives the timestamp back. | `Spec.parse_print` | -| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Spec.print_parse` | -| `unixSeconds` counts the whole seconds from 1970-01-01T00:00:00Z, with the offset applied. Its fast day arithmetic equals a day count that adds up month and year lengths. | `Spec.unixSeconds_eq` | -| `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction, compared exactly. | `Spec.compareInstant_eq` | -| The examples of section 5.8 parse to the fields the RFC gives. What the RFC says about them holds: `1996-12-19T16:39:57-08:00` is the instant `1996-12-20T00:39:57Z`, and `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. Separately, `1985-04-12T23:20:50.52Z` is 482196050 seconds after the epoch, as Python's `calendar.timegm` also gives. | `Spec.rfc3339_examples`, `Spec.rfc3339_example_instants` | -| A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` | -| `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one, at most one, that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` | -| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Spec.fromUnixSeconds_isSome` | -| `fromUnixSeconds` gives 0096-12-31T00:00:00Z, the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` | -| The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` | -| `isValidKnown` decides section 5.7 with the table of leap seconds. It allows second 60 only at one of the table's leap seconds, at the same instant whatever the offset. The table is the one in `Spec/Leap.lean`. The code keeps its own list of months, and the proof shows the two agree. | `Spec.isValidKnown_iff` | -| `siSeconds` is the Unix seconds since 1972-01-01T00:00:00Z, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds; so a leap second, the second before it and the second after it get three numbers in a row. Before 1972 the number is Unix seconds, 86400 to a day. | `Spec.siSeconds_eq` | -| On whole seconds valid by the table, `siSeconds` orders timestamps exactly as `compareInstant` does. So no two instants share a number, a leap second and the second after it included. | `Spec.siSeconds_order` | -| `fromSiSeconds` turns SI seconds back into the one UTC timestamp from 1972 on, valid by the table, that has them, a leap second included. It gives a timestamp for every second from 1972-01-01T00:00:00Z to 9999-12-31T23:59:59Z and `none` outside. | `Spec.fromSiSeconds_iff`, `Spec.fromSiSeconds_isSome` | -| `taiMinusUtc` is 10, and one more for each leap second of the table before the timestamp, so during a leap second it is still the value from before it. | `Spec.taiMinusUtc_leapsBefore` | -| TAI − UTC at each second from 1972 on, other than a leap second, is the value in the table's second column, 10 to 37. The code never reads that column; it counts leap seconds. | `Spec.taiMinusUtc_eq` | -| Section 5.8's leap seconds, the table's first and last, one seen from another offset, and second 60 in months that had none. SI seconds and TAI − UTC around the first and the last leap second. And the round trip that Unix seconds lose and SI seconds keep. | `Spec.leap_table_vectors` | -| `parseExt` reads exactly the strings of RFC 9557's `date-time-ext` rule, with one relaxation: an RFC 3339 timestamp, as `parse` reads it, so with second 60 at the end of any month, then a time zone, a name or a numeric offset, if there is one, and the tags, each perhaps marked critical with `!`. It returns the timestamp, the zone and the tags as written. | `Spec.parseExt_iff` | -| A valid IXDTF timestamp prints as the grammar writes it, and printing then parsing gives it back. | `Spec.printExt_eq`, `Spec.parseExt_print` | -| A string with no suffix reads as `parse` reads it, with no time zone and no tags. | `Spec.parseExt_plain` | -| `lookup` gives the first tag with a key, which section 3.3 has an application choose when an elective key is repeated. | `Spec.lookup_iff` | -| `erroneous` decides what sections 3.2 to 3.4 make an application treat as erroneous, for an application described by the tags it processes and the zone offsets it knows: a critical time zone it does not know or that disagrees with the offset, a critical tag it cannot process or whose key is repeated with other values, and an experimental key, one starting with `_`, it does not take part in. | `Spec.erroneous_iff` | -| Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, read and judged by an example application, as the RFC judges them. Critical time zones that agree with the offset, a critical `-00:00` zone that does not, and `[Z]` read as a zone name. Strings the grammar refuses: an empty item, `.` and `..` as zone parts, an upper case key, an empty value, a time zone after a tag, and an offset out of range. | `Spec.ixdtf_vectors` | +| `isValid` decides the rules of RFC 3339, sections 5.6 and 5.7. Every field is in its range. The day exists in its month, with the leap years of Appendix C. Second 60 falls only at 23:59 UTC on the last day of a month. Section 5.7 allows it only in months that had a leap second; `isValid` uses no table of them, so any month is accepted. | `Rfc3339.Spec.isValid_iff` | +| A valid timestamp prints as the grammar of section 5.6 writes it, with `T` and `Z` in upper case. | `Rfc3339.Spec.print_eq` | +| `parse` returns a timestamp exactly when the timestamp is valid and the string is how it prints, with `T` and `Z` in either case. So `parse` accepts nothing outside the grammar and those rules, rejects nothing inside them, and returns the fields as written. | `Rfc3339.Spec.parse_iff` | +| What `parse` returns is valid; for example, 30 February never passes. | `Rfc3339.Spec.parse_valid` | +| Printing then parsing gives the timestamp back. | `Rfc3339.Spec.parse_print` | +| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Rfc3339.Spec.print_parse` | +| `unixSeconds` counts the whole seconds from 1970-01-01T00:00:00Z, with the offset applied. Its fast day arithmetic equals a day count that adds up month and year lengths. | `Rfc3339.Spec.unixSeconds_eq` | +| `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction, compared exactly. | `Rfc3339.Spec.compareInstant_eq` | +| The examples of section 5.8 parse to the fields the RFC gives. What the RFC says about them holds: `1996-12-19T16:39:57-08:00` is the instant `1996-12-20T00:39:57Z`, and `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. Separately, `1985-04-12T23:20:50.52Z` is 482196050 seconds after the epoch, as Python's `calendar.timegm` also gives. | `Rfc3339.Spec.rfc3339_examples`, `Rfc3339.Spec.rfc3339_example_instants` | +| A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Rfc3339.Spec.leap_second_order` | +| `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one, at most one, that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Rfc3339.Spec.fromUnixSeconds_iff` | +| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Rfc3339.Spec.fromUnixSeconds_isSome` | +| `fromUnixSeconds` gives 0096-12-31T00:00:00Z, the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Rfc3339.Spec.fromUnixSeconds_vectors` | +| The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Rfc3339.Spec.calendar_vectors`, `Rfc3339.Spec.leap_second_vectors`, `Rfc3339.Spec.syntax_vectors` | +| `isValidKnown` decides section 5.7 with the table of leap seconds. It allows second 60 only at one of the table's leap seconds, at the same instant whatever the offset. The table is the one in `Rfc3339/Spec/Leap.lean`. The code keeps its own list of months, and the proof shows the two agree. | `Rfc3339.Spec.isValidKnown_iff` | +| `siSeconds` is the Unix seconds since 1972-01-01T00:00:00Z, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds; so a leap second, the second before it and the second after it get three numbers in a row. Before 1972 the number is Unix seconds, 86400 to a day. | `Rfc3339.Spec.siSeconds_eq` | +| On whole seconds valid by the table, `siSeconds` orders timestamps exactly as `compareInstant` does. So no two instants share a number, a leap second and the second after it included. | `Rfc3339.Spec.siSeconds_order` | +| `fromSiSeconds` turns SI seconds back into the one UTC timestamp from 1972 on, valid by the table, that has them, a leap second included. It gives a timestamp for every second from 1972-01-01T00:00:00Z to 9999-12-31T23:59:59Z and `none` outside. | `Rfc3339.Spec.fromSiSeconds_iff`, `Rfc3339.Spec.fromSiSeconds_isSome` | +| `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. | `Rfc3339.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. | `Rfc3339.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. | `Rfc3339.Spec.leap_table_vectors` | +| `parseExt` reads exactly the strings of RFC 9557's `date-time-ext` rule, with one relaxation: an RFC 3339 timestamp, as `parse` reads it, so with second 60 at the end of any month, then a time zone, a name or a numeric offset, if there is one, and the tags, each perhaps marked critical with `!`. It returns the timestamp, the zone and the tags as written. | `Rfc3339.Spec.parseExt_iff` | +| A valid IXDTF timestamp prints as the grammar writes it, and printing then parsing gives it back. | `Rfc3339.Spec.printExt_eq`, `Rfc3339.Spec.parseExt_print` | +| A string with no suffix reads as `parse` reads it, with no time zone and no tags. | `Rfc3339.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. | `Rfc3339.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. | `Rfc3339.Spec.erroneous_iff` | +| Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, read and judged by an example application, as the RFC judges them. Critical time zones that agree with the offset, a critical `-00:00` zone that does not, and `[Z]` read as a zone name. Strings the grammar refuses: an empty item, `.` and `..` as zone parts, an upper case key, an empty value, a time zone after a tag, and an offset out of range. | `Rfc3339.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. +- 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 `Rfc3339.Spec.exampleProcessor`. The differential tests cover them, with malformed requests and CR LF line endings. - Whether a leap second was announced, in `isValid`, `parse` and `parseExt`. They accept second 60 at 23:59 UTC at the end of any month, where section 5.7 allows it only at the end of months in which a leap second occurs; `isValidKnown` checks that against the table. Second 59 is always accepted, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. - The table after its expiry date, 28 June 2027. `isValidKnown` refuses second 60 at any month end the table does not list, and `siSeconds` and `taiMinusUtc` count no leap second after 2016. If one is ever announced, the table in the spec and the code's list must change together, and the spec approved again. The table is what tzdata publishes from IERS Bulletin C; that it matches the IERS record is trusted, not proved. -- SI seconds and TAI − UTC before 1972. UTC then ran on seconds of varying length, with TAI − UTC not a whole number of seconds. Before 1972, `Spec.siSeconds_eq` makes `siSeconds` Unix seconds less 63072000, 86400 to a day, which are not SI seconds there, and `taiMinusUtc` gives 10, which means nothing there; the tool's `known` request prints `-` for TAI − UTC. -- The table itself. `Spec/Leap.lean` copies tzdata's `leap-seconds.list` (tzdata 2026e, updated through IERS Bulletin C, expiring 28 June 2027) line for line. That copy is part of the specification: the reviewer checks it against the file, and the differential tests check the code against the copy of the file on the test machine, but no proof does. +- 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, `Rfc3339.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. `Rfc3339/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`. - 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. +- 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 "]")`. `Rfc3339/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, such as an offset with no colon in a time zone suffix; @@ -121,7 +121,7 @@ lake comparator --paranoid python3 tests/run_tests.py ``` -`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. +`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Rfc3339/Proofs/` proves exactly the statement in `Rfc3339/Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script compares the tool with Python's `datetime` and `calendar` modules, with the RFC's rules copied into the script, and with tzdata's `leap-seconds.list`, which the script reads itself, on inputs from a recorded seed. It then rewrites `tests/TEST-RESULTS.md`. @@ -130,11 +130,11 @@ The test script compares the tool with Python's `datetime` and `calendar` module - `Rfc3339/Types.lean`: the timestamp and offset types. It is part of the specification. - `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. +- `Rfc3339/Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. +- `Rfc3339/Spec/Defs.lean`: the definitions the statements use, written from the RFC, with checks against its tables and known day counts. +- `Rfc3339/Spec/Leap.lean`: the leap second table, line for line from tzdata's `leap-seconds.list`, and the definitions the leap second statements use. +- `Rfc3339/Spec/Ixdtf.lean`: RFC 9557's grammar, the rules for what an application must reject, and the example application. +- `Rfc3339/Proofs.lean` and `Rfc3339/Proofs/`: the proofs, under the same names. - `Main.lean`: the command-line tool. - `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else. - `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows. diff --git a/Rfc3339/IxdtfTypes.lean b/Rfc3339/IxdtfTypes.lean index c28c76c..2f07eac 100644 --- a/Rfc3339/IxdtfTypes.lean +++ b/Rfc3339/IxdtfTypes.lean @@ -1,7 +1,7 @@ /- 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 + with `Rfc3339/Spec.lean` and `Spec/Ixdtf.lean`, since the IXDTF statements are about these types. -/ diff --git a/Rfc3339/Proofs.lean b/Rfc3339/Proofs.lean new file mode 100644 index 0000000..ca13200 --- /dev/null +++ b/Rfc3339/Proofs.lean @@ -0,0 +1,10 @@ +/- + The proofs, under the names the challenge file gives them. The + theorems themselves are in `Rfc3339/Proofs/Main.lean`, from the lemmas in the + other files. +-/ + +import Rfc3339.Proofs.Main +import Rfc3339.Proofs.FromUnix.Main +import Rfc3339.Proofs.Leap.Main +import Rfc3339.Proofs.Ixdtf.Main diff --git a/Proofs/DayNumber.lean b/Rfc3339/Proofs/DayNumber.lean similarity index 56% rename from Proofs/DayNumber.lean rename to Rfc3339/Proofs/DayNumber.lean index 9a9627b..071c402 100644 --- a/Proofs/DayNumber.lean +++ b/Rfc3339/Proofs/DayNumber.lean @@ -5,19 +5,19 @@ -/ import Rfc3339 -import Spec.Defs +import Rfc3339.Spec.Defs namespace Rfc3339.Proofs.DayNumber open Rfc3339 -theorem isLeapYear_eq (y : Nat) : isLeapYear y = Spec.isLeapYear y := by - unfold isLeapYear Spec.isLeapYear +theorem isLeapYear_eq (y : Nat) : isLeapYear y = Rfc3339.Spec.isLeapYear y := by + unfold isLeapYear Rfc3339.Spec.isLeapYear by_cases h4 : y % 4 = 0 <;> by_cases h100 : y % 100 = 0 <;> by_cases h400 : y % 400 = 0 <;> simp [h4, h100, h400] -theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := by - unfold daysInMonth Spec.daysInMonth +theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Rfc3339.Spec.daysInMonth y m := by + unfold daysInMonth Rfc3339.Spec.daysInMonth rw [isLeapYear_eq] match m with | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 => simp @@ -27,31 +27,31 @@ theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := b have : ¬ (1 ≤ n + 13 ∧ n + 13 ≤ 12) := by omega simp_all -theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Spec.offsetMinutes o := by - cases o <;> simp [offsetMinutes, Spec.offsetMinutes] +theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Rfc3339.Spec.offsetMinutes o := by + cases o <;> simp [offsetMinutes, Rfc3339.Spec.offsetMinutes] /-- One more year adds that year's length. -/ theorem daysBeforeYear_succ (y : Nat) : - daysBeforeYear (y + 1) = daysBeforeYear y + Spec.yearLength y := by - unfold daysBeforeYear Spec.yearLength + daysBeforeYear (y + 1) = daysBeforeYear y + Rfc3339.Spec.yearLength y := by + unfold daysBeforeYear Rfc3339.Spec.yearLength by_cases h4 : y % 4 = 0 · by_cases h100 : y % 100 = 0 · by_cases h400 : y % 400 = 0 - · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h400] + · have hl : Rfc3339.Spec.isLeapYear y = true := by simp [Rfc3339.Spec.isLeapYear, h4, h400] simp only [hl, ite_true] omega - · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h100, h400] + · have hl : Rfc3339.Spec.isLeapYear y = false := by simp [Rfc3339.Spec.isLeapYear, h100, h400] simp only [hl, Bool.false_eq_true, ite_false] omega - · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h100] + · have hl : Rfc3339.Spec.isLeapYear y = true := by simp [Rfc3339.Spec.isLeapYear, h4, h100] simp only [hl, ite_true] omega - · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h4] + · have hl : Rfc3339.Spec.isLeapYear y = false := by simp [Rfc3339.Spec.isLeapYear, h4] simp only [hl, Bool.false_eq_true, ite_false] omega theorem daysBeforeYear_eq (y : Nat) : - daysBeforeYear y = ((List.range y).map Spec.yearLength).sum := by + daysBeforeYear y = ((List.range y).map Rfc3339.Spec.yearLength).sum := by induction y with | zero => rfl | succ y ih => @@ -59,18 +59,18 @@ theorem daysBeforeYear_eq (y : Nat) : simp theorem daysBeforeMonth_eq (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : - daysBeforeMonth y m = ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum := by + daysBeforeMonth y m = ((List.range (m - 1)).map fun i => Rfc3339.Spec.daysInMonth y (i + 1)).sum := by unfold daysBeforeMonth rw [isLeapYear_eq] - cases hl : Spec.isLeapYear y <;> + cases hl : Rfc3339.Spec.isLeapYear y <;> match m, h1, h2 with | 1, _, _ | 2, _, _ | 3, _, _ | 4, _, _ | 5, _, _ | 6, _, _ | 7, _, _ | 8, _, _ | 9, _, _ | 10, _, _ | 11, _, _ | 12, _, _ => - simp [List.range_succ, Spec.daysInMonth, hl] + simp [List.range_succ, Rfc3339.Spec.daysInMonth, hl] theorem dayNumber_eq (y m d : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : - dayNumber y m d = Spec.dayNumber y m d := by - unfold dayNumber Spec.dayNumber + dayNumber y m d = Rfc3339.Spec.dayNumber y m d := by + unfold dayNumber Rfc3339.Spec.dayNumber rw [daysBeforeYear_eq, daysBeforeMonth_eq y m h1 h2] end Rfc3339.Proofs.DayNumber diff --git a/Proofs/Format.lean b/Rfc3339/Proofs/Format.lean similarity index 85% rename from Proofs/Format.lean rename to Rfc3339/Proofs/Format.lean index 21f214f..ff16192 100644 --- a/Proofs/Format.lean +++ b/Rfc3339/Proofs/Format.lean @@ -1,12 +1,12 @@ /- The printer and the parser of `Rfc3339/Format.lean` against the spec: - `asciiUpper` is `Spec.asciiUpper`, a valid timestamp renders as - `Spec.render` writes it, and `parseUpper` returns `t` exactly when `t` + `asciiUpper` is `Rfc3339.Spec.asciiUpper`, a valid timestamp renders as + `Rfc3339.Spec.render` writes it, and `parseUpper` returns `t` exactly when `t` is valid and the input is `t.render`. From these, `parse_iff'`. -/ import Rfc3339 -import Spec.Defs +import Rfc3339.Spec.Defs namespace Rfc3339.Proofs.Format @@ -17,24 +17,24 @@ open Rfc3339 /-- `Char` order is the order of code points. -/ theorem le_iff_toNat (a b : Char) : a ≤ b ↔ a.toNat ≤ b.toNat := Iff.rfl -theorem asciiUpper_eq (c : Char) : asciiUpper c = Spec.asciiUpper c := by - unfold asciiUpper Spec.asciiUpper +theorem asciiUpper_eq (c : Char) : asciiUpper c = Rfc3339.Spec.asciiUpper c := by + unfold asciiUpper Rfc3339.Spec.asciiUpper simp only [le_iff_toNat] rfl theorem print_toList (t : Timestamp) : t.print.toList = t.render := by simp [Timestamp.print] -theorem digitChar_eq (n : Nat) (h : n < 10) : Spec.digitChar n = digitChar n := by - have : ∀ i : Fin 10, Spec.digitChar i.val = digitChar i.val := by decide +theorem digitChar_eq (n : Nat) (h : n < 10) : Rfc3339.Spec.digitChar n = digitChar n := by + have : ∀ i : Fin 10, Rfc3339.Spec.digitChar i.val = digitChar i.val := by decide exact this ⟨n, h⟩ -/-- `pad4` and `pad2` write the last digits of any number, as `Spec.digits` does. -/ -theorem digits4 (n : Nat) : Spec.digits 4 n = pad4 n := by - simp [Spec.digits, pad4, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] +/-- `pad4` and `pad2` write the last digits of any number, as `Rfc3339.Spec.digits` does. -/ +theorem digits4 (n : Nat) : Rfc3339.Spec.digits 4 n = pad4 n := by + simp [Rfc3339.Spec.digits, pad4, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] -theorem digits2 (n : Nat) : Spec.digits 2 n = pad2 n := by - simp [Spec.digits, pad2, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] +theorem digits2 (n : Nat) : Rfc3339.Spec.digits 2 n = pad2 n := by + simp [Rfc3339.Spec.digits, pad2, List.range, List.range.loop, digitChar_eq, Nat.mod_lt] theorem daysInMonth_le (y m : Nat) : daysInMonth y m ≤ 31 := by unfold daysInMonth @@ -49,7 +49,7 @@ theorem isValid_bounds {t : Timestamp} (h : t.isValid = true) : refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> first | omega | simp_all theorem renderFraction_eq (f : List Nat) (h : ∀ d ∈ f, d < 10) : - renderFraction f = if f = [] then [] else ['.'] ++ f.map Spec.digitChar := by + renderFraction f = if f = [] then [] else ['.'] ++ f.map Rfc3339.Spec.digitChar := by cases f with | nil => rfl | cons d ds => @@ -59,12 +59,12 @@ theorem renderFraction_eq (f : List Nat) (h : ∀ d ∈ f, d < 10) : intro x hx exact (digitChar_eq x (h x hx)).symm -theorem offset_render_eq (o : Offset) : o.render = Spec.renderOffset o := by - cases o <;> simp [Offset.render, Spec.renderOffset, digits2] +theorem offset_render_eq (o : Offset) : o.render = Rfc3339.Spec.renderOffset o := by + cases o <;> simp [Offset.render, Rfc3339.Spec.renderOffset, digits2] -theorem render_eq (t : Timestamp) (h : t.isValid = true) : t.render = Spec.render t := by +theorem render_eq (t : Timestamp) (h : t.isValid = true) : t.render = Rfc3339.Spec.render t := by have hb := isValid_bounds h - simp [Timestamp.render, Spec.render, digits4, digits2, renderFraction_eq t.fraction hb.2.2.2.2.2.2.1, + simp [Timestamp.render, Rfc3339.Spec.render, digits4, digits2, renderFraction_eq t.fraction hb.2.2.2.2.2.2.1, offset_render_eq] /-! ## Parsing -/ @@ -252,8 +252,8 @@ theorem parseUpper_iff (u : List Char) (t : Timestamp) : exact parseUpper_render h theorem parse_iff' (s : String) (t : Timestamp) : - parse s = some t ↔ t.isValid = true ∧ s.toList.map Spec.asciiUpper = Spec.render t := by - have hmap : s.toList.map asciiUpper = s.toList.map Spec.asciiUpper := + parse s = some t ↔ t.isValid = true ∧ s.toList.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render t := by + have hmap : s.toList.map asciiUpper = s.toList.map Rfc3339.Spec.asciiUpper := List.map_congr_left (fun c _ => asciiUpper_eq c) rw [parse, hmap, parseUpper_iff] constructor diff --git a/Proofs/Fraction.lean b/Rfc3339/Proofs/Fraction.lean similarity index 85% rename from Proofs/Fraction.lean rename to Rfc3339/Proofs/Fraction.lean index 44ab6f0..3e69a0d 100644 --- a/Proofs/Fraction.lean +++ b/Rfc3339/Proofs/Fraction.lean @@ -5,7 +5,7 @@ -/ import Rfc3339 -import Spec.Defs +import Rfc3339.Spec.Defs namespace Rfc3339.Proofs.Fraction @@ -14,30 +14,30 @@ open Rfc3339 /-- Reading digits after a value `x` already read: `x` is shifted left by the number of digits still to come. -/ theorem foldl_digits (x : Nat) (ds : List Nat) : - List.foldl (fun acc d => 10 * acc + d) x ds = x * 10 ^ ds.length + Spec.fractionValue ds := by + List.foldl (fun acc d => 10 * acc + d) x ds = x * 10 ^ ds.length + Rfc3339.Spec.fractionValue ds := by induction ds generalizing x with - | nil => simp [Spec.fractionValue] + | nil => simp [Rfc3339.Spec.fractionValue] | cons d ds ih => - simp only [Spec.fractionValue, List.foldl_cons, List.length_cons] at * + simp only [Rfc3339.Spec.fractionValue, List.foldl_cons, List.length_cons] at * rw [ih, ih (10 * 0 + d), Nat.pow_succ, Nat.mul_zero, Nat.zero_add, Nat.add_mul, Nat.add_assoc] congr 1 rw [Nat.mul_comm 10 x, Nat.mul_assoc, Nat.mul_comm 10 (10 ^ ds.length)] -theorem fractionValue_nil : Spec.fractionValue [] = 0 := rfl +theorem fractionValue_nil : Rfc3339.Spec.fractionValue [] = 0 := rfl theorem fractionValue_cons (d : Nat) (ds : List Nat) : - Spec.fractionValue (d :: ds) = d * 10 ^ ds.length + Spec.fractionValue ds := by + Rfc3339.Spec.fractionValue (d :: ds) = d * 10 ^ ds.length + Rfc3339.Spec.fractionValue ds := by have h := foldl_digits d ds - simpa [Spec.fractionValue] using h + simpa [Rfc3339.Spec.fractionValue] using h theorem fractionValue_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) : - Spec.fractionValue a < 10 ^ a.length := by + Rfc3339.Spec.fractionValue a < 10 ^ a.length := by induction a with | nil => simp [fractionValue_nil] | cons d ds ih => have hd : d ≤ 9 := ha d (by simp) - have hds : Spec.fractionValue ds < 10 ^ ds.length := ih (fun e he => ha e (by simp [he])) + have hds : Rfc3339.Spec.fractionValue ds < 10 ^ ds.length := ih (fun e he => ha e (by simp [he])) rw [fractionValue_cons, List.length_cons, Nat.pow_succ] have h1 : d * 10 ^ ds.length + 10 ^ ds.length ≤ 10 ^ ds.length * 10 := by rw [Nat.mul_comm (10 ^ ds.length) 10, ← Nat.succ_mul] @@ -46,15 +46,15 @@ theorem fractionValue_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) : /-- A digit list scaled to `k` digits stays below `10 ^ k`. -/ theorem scaled_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (k : Nat) (hk : a.length ≤ k) : - Spec.fractionValue a * 10 ^ (k - a.length) < 10 ^ k := by + Rfc3339.Spec.fractionValue a * 10 ^ (k - a.length) < 10 ^ k := by have h := Nat.mul_lt_mul_of_pos_right (fractionValue_lt a ha) ((Nat.pow_pos (n := k - a.length) (by decide : 0 < 10))) rwa [← Nat.pow_add, Nat.add_sub_cancel' hk] at h /-- Scaling a list with a leading digit: the digit takes the top place. -/ theorem scaled_cons (d : Nat) (ds : List Nat) (k : Nat) (hk : ds.length ≤ k) : - Spec.fractionValue (d :: ds) * 10 ^ (k + 1 - (d :: ds).length) = - d * 10 ^ k + Spec.fractionValue ds * 10 ^ (k - ds.length) := by + Rfc3339.Spec.fractionValue (d :: ds) * 10 ^ (k + 1 - (d :: ds).length) = + d * 10 ^ k + Rfc3339.Spec.fractionValue ds * 10 ^ (k - ds.length) := by have e : k + 1 - (d :: ds).length = k - ds.length := by simp only [List.length_cons]; omega rw [e, fractionValue_cons, Nat.add_mul, Nat.mul_assoc, ← Nat.pow_add, Nat.add_sub_cancel' hk] @@ -68,8 +68,8 @@ theorem compare_add_left (p x y : Nat) : compare (p + x) (p + y) = compare x y : theorem compareFraction_scaled (a b : List Nat) : (∀ d ∈ a, d ≤ 9) → (∀ d ∈ b, d ≤ 9) → ∀ k, a.length ≤ k → b.length ≤ k → compareFraction a b = - compare (Spec.fractionValue a * 10 ^ (k - a.length)) - (Spec.fractionValue b * 10 ^ (k - b.length)) := by + compare (Rfc3339.Spec.fractionValue a * 10 ^ (k - a.length)) + (Rfc3339.Spec.fractionValue b * 10 ^ (k - b.length)) := by induction a, b using compareFraction.induct with | case1 => intro _ _ k _ _ @@ -161,8 +161,8 @@ theorem compareFraction_scaled (a b : List Nat) : theorem compareFraction_eq (a b : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (hb : ∀ d ∈ b, d ≤ 9) : compareFraction a b = - compare (Spec.fractionValue a * 10 ^ (max a.length b.length - a.length)) - (Spec.fractionValue b * 10 ^ (max a.length b.length - b.length)) := + compare (Rfc3339.Spec.fractionValue a * 10 ^ (max a.length b.length - a.length)) + (Rfc3339.Spec.fractionValue b * 10 ^ (max a.length b.length - b.length)) := compareFraction_scaled a b ha hb _ (Nat.le_max_left _ _) (Nat.le_max_right _ _) end Rfc3339.Proofs.Fraction diff --git a/Proofs/FromUnix/Day.lean b/Rfc3339/Proofs/FromUnix/Day.lean similarity index 85% rename from Proofs/FromUnix/Day.lean rename to Rfc3339/Proofs/FromUnix/Day.lean index 51acbe1..52a1f58 100644 --- a/Proofs/FromUnix/Day.lean +++ b/Rfc3339/Proofs/FromUnix/Day.lean @@ -4,8 +4,8 @@ -/ import Rfc3339 -import Spec.Defs -import Proofs.DayNumber +import Rfc3339.Spec.Defs +import Rfc3339.Proofs.DayNumber namespace Rfc3339.Proofs.FromUnix @@ -49,8 +49,8 @@ theorem yearOfDay_spec (n : Nat) : · omega /-- The length of year `y`, from the code's leap year rule. -/ -theorem dy_yearLength (y : Nat) : Spec.yearLength y = if isLeapYear y then 366 else 365 := by - unfold Spec.yearLength; rw [DayNumber.isLeapYear_eq] +theorem dy_yearLength (y : Nat) : Rfc3339.Spec.yearLength y = if isLeapYear y then 366 else 365 := by + unfold Rfc3339.Spec.yearLength; rw [DayNumber.isLeapYear_eq] /-! ### Months -/ @@ -94,7 +94,7 @@ theorem dy_end_common : ∀ m, m < 13 → 1 ≤ m → daysBeforeMonth 1 m + days decide +kernel /-- `monthOfDay` gives the month that day `doy` of year `y` falls in. -/ -theorem dy_month (y doy : Nat) (h : doy < Spec.yearLength y) : +theorem dy_month (y doy : Nat) (h : doy < Rfc3339.Spec.yearLength y) : 1 ≤ monthOfDay y doy ∧ monthOfDay y doy ≤ 12 ∧ daysBeforeMonth y (monthOfDay y doy) ≤ doy ∧ doy < daysBeforeMonth y (monthOfDay y doy) + daysInMonth y (monthOfDay y doy) := by @@ -124,7 +124,7 @@ theorem dy_month_uniq (y m k : Nat) (hm : 1 ≤ m ∧ m ≤ 12) (hk : k < daysIn /-- A month ends within its year. -/ theorem dy_month_end (y m : Nat) (hm : 1 ≤ m ∧ m ≤ 12) : - daysBeforeMonth y m + daysInMonth y m ≤ Spec.yearLength y := by + daysBeforeMonth y m + daysInMonth y m ≤ Rfc3339.Spec.yearLength y := by rw [dy_yearLength] cases hl : isLeapYear y · have e : isLeapYear y = isLeapYear 1 := by rw [hl]; rfl @@ -142,15 +142,15 @@ theorem fromDayNumber_spec (n : Nat) (h : n < daysBeforeYear 10000) : (fromDayNumber n).1 ≤ 9999 ∧ 1 ≤ (fromDayNumber n).2.1 ∧ (fromDayNumber n).2.1 ≤ 12 ∧ 1 ≤ (fromDayNumber n).2.2 ∧ - (fromDayNumber n).2.2 ≤ Spec.daysInMonth (fromDayNumber n).1 (fromDayNumber n).2.1 ∧ - Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 (fromDayNumber n).2.2 = n := by + (fromDayNumber n).2.2 ≤ Rfc3339.Spec.daysInMonth (fromDayNumber n).1 (fromDayNumber n).2.1 ∧ + Rfc3339.Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 (fromDayNumber n).2.2 = n := by obtain ⟨h1, h2⟩ := yearOfDay_spec n have hy : yearOfDay n ≤ 9999 := by apply Nat.le_of_not_lt intro c have := dy_mono (show 10000 ≤ yearOfDay n by omega) omega - have hdoy : n - daysBeforeYear (yearOfDay n) < Spec.yearLength (yearOfDay n) := by + have hdoy : n - daysBeforeYear (yearOfDay n) < Rfc3339.Spec.yearLength (yearOfDay n) := by rw [DayNumber.daysBeforeYear_succ] at h2; omega obtain ⟨hm1, hm2, hm3, hm4⟩ := dy_month _ _ hdoy simp only [fromDayNumber] @@ -160,8 +160,8 @@ theorem fromDayNumber_spec (n : Nat) (h : n < daysBeforeYear 10000) : /-- A valid date's day number lies in its year. -/ theorem dy_dayNumber_bounds (y m d : Nat) (hm : 1 ≤ m ∧ m ≤ 12) - (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m) : - daysBeforeYear y ≤ Spec.dayNumber y m d ∧ Spec.dayNumber y m d < daysBeforeYear (y + 1) := by + (hd : 1 ≤ d ∧ d ≤ Rfc3339.Spec.daysInMonth y m) : + daysBeforeYear y ≤ Rfc3339.Spec.dayNumber y m d ∧ Rfc3339.Spec.dayNumber y m d < daysBeforeYear (y + 1) := by rw [← DayNumber.dayNumber_eq _ _ _ hm.1 hm.2, DayNumber.daysBeforeYear_succ] rw [← DayNumber.daysInMonth_eq] at hd have := dy_month_end y m hm @@ -170,9 +170,9 @@ theorem dy_dayNumber_bounds (y m d : Nat) (hm : 1 ≤ m ∧ m ≤ 12) /-- Two valid dates with the same day number are the same date. -/ theorem dayNumber_inj (y m d y' m' d' : Nat) - (hm : 1 ≤ m ∧ m ≤ 12) (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m) - (hm' : 1 ≤ m' ∧ m' ≤ 12) (hd' : 1 ≤ d' ∧ d' ≤ Spec.daysInMonth y' m') - (h : Spec.dayNumber y m d = Spec.dayNumber y' m' d') : y = y' ∧ m = m' ∧ d = d' := by + (hm : 1 ≤ m ∧ m ≤ 12) (hd : 1 ≤ d ∧ d ≤ Rfc3339.Spec.daysInMonth y m) + (hm' : 1 ≤ m' ∧ m' ≤ 12) (hd' : 1 ≤ d' ∧ d' ≤ Rfc3339.Spec.daysInMonth y' m') + (h : Rfc3339.Spec.dayNumber y m d = Rfc3339.Spec.dayNumber y' m' d') : y = y' ∧ m = m' ∧ d = d' := by have b := dy_dayNumber_bounds y m d hm hd have b' := dy_dayNumber_bounds y' m' d' hm' hd' have hy : y = y' := by @@ -197,7 +197,7 @@ theorem dayNumber_inj (y m d y' m' d' : Nat) /-- A valid date in a year no later than 9999 falls before 10000-01-01. -/ theorem dayNumber_lt (y m d : Nat) (hy : y ≤ 9999) (hm : 1 ≤ m ∧ m ≤ 12) - (hd : 1 ≤ d ∧ d ≤ Spec.daysInMonth y m) : Spec.dayNumber y m d < daysBeforeYear 10000 := by + (hd : 1 ≤ d ∧ d ≤ Rfc3339.Spec.daysInMonth y m) : Rfc3339.Spec.dayNumber y m d < daysBeforeYear 10000 := by have b := dy_dayNumber_bounds y m d hm hd have := dy_mono (show y + 1 ≤ 10000 by omega) omega diff --git a/Proofs/FromUnix/Main.lean b/Rfc3339/Proofs/FromUnix/Main.lean similarity index 76% rename from Proofs/FromUnix/Main.lean rename to Rfc3339/Proofs/FromUnix/Main.lean index 442be69..a4aea0a 100644 --- a/Proofs/FromUnix/Main.lean +++ b/Rfc3339/Proofs/FromUnix/Main.lean @@ -4,10 +4,10 @@ -/ import Rfc3339 -import Spec.Defs -import Proofs.DayNumber -import Proofs.Instant -import Proofs.FromUnix.Day +import Rfc3339.Spec.Defs +import Rfc3339.Proofs.DayNumber +import Rfc3339.Proofs.Instant +import Rfc3339.Proofs.FromUnix.Day namespace Rfc3339.Proofs.FromUnix @@ -19,31 +19,31 @@ theorem fu_daysBeforeYear_10000 : daysBeforeYear 10000 = 3652425 := by decide /-- A UTC timestamp's Unix seconds, shifted to count from 0000-01-01: its day number in seconds, plus the time of day. -/ theorem fu_unixSeconds_z (t : Timestamp) (hz : t.offset = .z) : - Spec.unixSeconds t + 719528 * 86400 = - ((Spec.dayNumber t.year t.month t.day * 86400 + t.hour * 3600 + t.minute * 60 + + Rfc3339.Spec.unixSeconds t + 719528 * 86400 = + ((Rfc3339.Spec.dayNumber t.year t.month t.day * 86400 + t.hour * 3600 + t.minute * 60 + t.second : Nat) : Int) := by - unfold Spec.unixSeconds Spec.utcMinute + unfold Rfc3339.Spec.unixSeconds Rfc3339.Spec.utcMinute rw [hz, Instant.dayNumber_epoch] - simp only [Spec.offsetMinutes] + simp only [Rfc3339.Spec.offsetMinutes] omega /-- The first second of the range. -/ -theorem fu_unixSeconds_lo : Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 := by +theorem fu_unixSeconds_lo : Rfc3339.Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 := by decide +kernel /-- The last second of the range. -/ theorem fu_unixSeconds_hi : - Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 := by + Rfc3339.Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 := by decide +kernel end Rfc3339.Proofs.FromUnix open Rfc3339 -theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : +theorem Rfc3339.Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : Rfc3339.fromUnixSeconds s = some t ↔ - Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧ - Spec.unixSeconds t = s := by + Rfc3339.Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧ + Rfc3339.Spec.unixSeconds t = s := by have hD := Proofs.FromUnix.fu_daysBeforeYear_10000 constructor · intro h @@ -87,11 +87,11 @@ theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : dsimp only split case isFalse hr => exfalso; omega - have hn : (s + 719528 * 86400).toNat / 86400 = Spec.dayNumber y m d := by omega + have hn : (s + 719528 * 86400).toNat / 86400 = Rfc3339.Spec.dayNumber y m d := by omega have hsec : (s + 719528 * 86400).toNat % 86400 = hh * 3600 + mi * 60 + sec := by omega rw [hn, hsec] have hs := Proofs.FromUnix.fromDayNumber_spec _ hN - generalize fromDayNumber (Spec.dayNumber y m d) = p at hs ⊢ + generalize fromDayNumber (Rfc3339.Spec.dayNumber y m d) = p at hs ⊢ obtain ⟨y', m', d'⟩ := p obtain ⟨-, h2, h3, h4, h5, h6⟩ := hs simp only at h2 h3 h4 h5 h6 @@ -100,10 +100,10 @@ theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : simp only [Option.some.injEq, Timestamp.mk.injEq, true_and, and_true] and_intros <;> omega -theorem Spec.fromUnixSeconds_isSome (s : Int) : +theorem Rfc3339.Spec.fromUnixSeconds_isSome (s : Int) : (Rfc3339.fromUnixSeconds s).isSome ↔ - Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧ - s ≤ Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by + Rfc3339.Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧ + s ≤ Rfc3339.Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by rw [Proofs.FromUnix.fu_unixSeconds_lo, Proofs.FromUnix.fu_unixSeconds_hi] have hD := Proofs.FromUnix.fu_daysBeforeYear_10000 unfold Rfc3339.fromUnixSeconds @@ -118,15 +118,15 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) : simp only [Option.isSome_none, Bool.false_eq_true, false_iff] omega -theorem Spec.fromUnixSeconds_vectors : +theorem Rfc3339.Spec.fromUnixSeconds_vectors : Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 2147483647 = some ⟨2038, 1, 19, 3, 14, 7, [], .z⟩ ∧ Rfc3339.fromUnixSeconds (-1) = some ⟨1969, 12, 31, 23, 59, 59, [], .z⟩ ∧ - Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 ∧ - Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 ∧ + Rfc3339.Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 ∧ + Rfc3339.Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 ∧ Rfc3339.fromUnixSeconds (-62167219200) = some ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 253402300799 = some ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ ∧ Rfc3339.fromUnixSeconds (-62167219201) = none ∧ diff --git a/Proofs/Instant.lean b/Rfc3339/Proofs/Instant.lean similarity index 72% rename from Proofs/Instant.lean rename to Rfc3339/Proofs/Instant.lean index a644e6f..d571938 100644 --- a/Proofs/Instant.lean +++ b/Rfc3339/Proofs/Instant.lean @@ -1,33 +1,33 @@ /- The instant code in `Rfc3339/Instant.lean` agrees with the definitions in `Spec/Defs.lean`: `unixSeconds` counts the same whole seconds as - `Spec.unixSeconds`, `utcMinute` is `Spec.utcMinute`, and + `Rfc3339.Spec.unixSeconds`, `utcMinute` is `Rfc3339.Spec.utcMinute`, and `compareInstant` orders two valid timestamps the same way as - `Spec.compareInstants`. + `Rfc3339.Spec.compareInstants`. -/ import Rfc3339 -import Spec.Defs -import Proofs.DayNumber -import Proofs.Fraction +import Rfc3339.Spec.Defs +import Rfc3339.Proofs.DayNumber +import Rfc3339.Proofs.Fraction namespace Rfc3339.Proofs.Instant open Rfc3339 /-- 1970-01-01 is day 719528. -/ -theorem dayNumber_epoch : Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel +theorem dayNumber_epoch : Rfc3339.Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel -theorem utcMinute_eq (t : Timestamp) (h : Spec.Valid t) : - t.utcMinute = Spec.utcMinute t := by +theorem utcMinute_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.utcMinute = Rfc3339.Spec.utcMinute t := by obtain ⟨_, hm1, hm2, _⟩ := h - unfold Timestamp.utcMinute Spec.utcMinute + unfold Timestamp.utcMinute Rfc3339.Spec.utcMinute rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.offsetMinutes_eq] -theorem unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : - t.unixSeconds = Spec.unixSeconds t := by +theorem unixSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.unixSeconds = Rfc3339.Spec.unixSeconds t := by obtain ⟨_, hm1, hm2, _⟩ := h - unfold Timestamp.unixSeconds Spec.unixSeconds Spec.utcMinute + unfold Timestamp.unixSeconds Rfc3339.Spec.unixSeconds Rfc3339.Spec.utcMinute rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.offsetMinutes_eq, dayNumber_epoch] omega @@ -68,33 +68,33 @@ theorem compare_scaled (u v P x y : Int) (hx0 : 0 ≤ x) (hxP : x < P) (hy0 : 0 rw [Int.add_mul, Int.one_mul] at hle omega -theorem compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : - a.compareInstant b = Spec.compareInstants a b := by +theorem compareInstant_eq (a b : Timestamp) (ha : Rfc3339.Spec.Valid a) (hb : Rfc3339.Spec.Valid b) : + a.compareInstant b = Rfc3339.Spec.compareInstants a b := by have hfa : ∀ d ∈ a.fraction, d ≤ 9 := ha.2.2.2.2.2.2.2.2.2.1 have hfb : ∀ d ∈ b.fraction, d ≤ 9 := hb.2.2.2.2.2.2.2.2.2.1 have la := Fraction.scaled_lt a.fraction hfa (max a.fraction.length b.fraction.length) (Nat.le_max_left _ _) have lb := Fraction.scaled_lt b.fraction hfb (max a.fraction.length b.fraction.length) (Nat.le_max_right _ _) - have ea : (Spec.fractionValue a.fraction : Int) * + have ea : (Rfc3339.Spec.fractionValue a.fraction : Int) * 10 ^ (max a.fraction.length b.fraction.length - a.fraction.length) = - ((Spec.fractionValue a.fraction * + ((Rfc3339.Spec.fractionValue a.fraction * 10 ^ (max a.fraction.length b.fraction.length - a.fraction.length) : Nat) : Int) := by push_cast; rfl - have eb : (Spec.fractionValue b.fraction : Int) * + have eb : (Rfc3339.Spec.fractionValue b.fraction : Int) * 10 ^ (max a.fraction.length b.fraction.length - b.fraction.length) = - ((Spec.fractionValue b.fraction * + ((Rfc3339.Spec.fractionValue b.fraction * 10 ^ (max a.fraction.length b.fraction.length - b.fraction.length) : Nat) : Int) := by push_cast; rfl have eP : ((10 ^ max a.fraction.length b.fraction.length : Nat) : Int) = (10 : Int) ^ max a.fraction.length b.fraction.length := by push_cast; rfl - unfold Timestamp.compareInstant Spec.compareInstants Spec.instantKey + unfold Timestamp.compareInstant Rfc3339.Spec.compareInstants Rfc3339.Spec.instantKey simp only rw [utcMinute_eq a ha, utcMinute_eq b hb, Fraction.compareFraction_eq _ _ hfa hfb, ea, eb, - compare_scaled (Spec.utcMinute a * 61 + a.second) (Spec.utcMinute b * 61 + b.second) + compare_scaled (Rfc3339.Spec.utcMinute a * 61 + a.second) (Rfc3339.Spec.utcMinute b * 61 + b.second) ((10 : Int) ^ max a.fraction.length b.fraction.length) _ _ (by omega) (by rw [← eP]; omega) (by omega) (by rw [← eP]; omega), compare_natCast] - cases compare (Spec.utcMinute a * 61 + a.second) (Spec.utcMinute b * 61 + b.second) <;> rfl + cases compare (Rfc3339.Spec.utcMinute a * 61 + a.second) (Rfc3339.Spec.utcMinute b * 61 + b.second) <;> rfl end Rfc3339.Proofs.Instant diff --git a/Proofs/Ixdtf/Main.lean b/Rfc3339/Proofs/Ixdtf/Main.lean similarity index 85% rename from Proofs/Ixdtf/Main.lean rename to Rfc3339/Proofs/Ixdtf/Main.lean index 622cff6..51a568e 100644 --- a/Proofs/Ixdtf/Main.lean +++ b/Rfc3339/Proofs/Ixdtf/Main.lean @@ -1,41 +1,41 @@ /- - The IXDTF statements of `Spec.lean`, under the same names, from the - lemmas in the other files of `Proofs/Ixdtf/`. The test vectors are + The IXDTF statements of `Rfc3339/Spec.lean`, under the same names, from the + lemmas in the other files of `Rfc3339/Proofs/Ixdtf/`. The test vectors are checked by evaluation. -/ -import Proofs.Ixdtf.Parse -import Proofs.Ixdtf.Rules +import Rfc3339.Proofs.Ixdtf.Parse +import Rfc3339.Proofs.Ixdtf.Rules open Rfc3339 -theorem Spec.parseExt_iff (s : String) (e : Ext) : +theorem Rfc3339.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.Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Rfc3339.Spec.renderSuffix e ∧ + dt.map Rfc3339.Spec.asciiUpper = Rfc3339.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 := +theorem Rfc3339.Spec.printExt_eq (e : Ext) (h : Rfc3339.Spec.ExtValid e) : + e.print.toList = Rfc3339.Spec.render e.stamp ++ Rfc3339.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 := +theorem Rfc3339.Spec.parseExt_print (e : Ext) (h : Rfc3339.Spec.ExtValid e) : parseExt e.print = some e := Rfc3339.Proofs.Ixdtf.parseExt_print e h -theorem Spec.parseExt_plain (s : String) (h : '[' ∉ s.toList) : +theorem Rfc3339.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) : +theorem Rfc3339.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 := +theorem Rfc3339.Spec.erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Rfc3339.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 + functions, which the lemmas of `Rfc3339/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. -/ @@ -47,7 +47,7 @@ def vx_validB (e : Ext) : Bool := | 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 +theorem vx_validB_sound (e : Ext) (h : vx_validB e = true) : Rfc3339.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 @@ -68,16 +68,16 @@ theorem vx_validB_sound (e : Ext) (h : vx_validB e = true) : Spec.ExtValid e := 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) : + (hs : s.toList = dt ++ Rfc3339.Spec.renderSuffix e) (hd : dt.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render e.stamp) : parseExt s = some e := (Rfc3339.Proofs.Ixdtf.parseExt_iff s e).2 ⟨vx_validB_sound e hv, dt, hs, hd⟩ /-- Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, with - the application of `Spec.exampleProcessor`: each one is read, and is + the application of `Rfc3339.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 : +theorem Rfc3339.Spec.ixdtf_vectors : -- Section 4.2, Figures 4 to 7 parseExt "1996-12-19T16:39:57-08:00" = some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, []⟩ ∧ @@ -92,58 +92,58 @@ theorem Spec.ixdtf_vectors : some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ ∧ ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.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) ∧ + (·.erroneous Rfc3339.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) = + ((parseExt "2022-07-08T00:14:07+08:45[!+08:45]").map (·.erroneous Rfc3339.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) = + ((parseExt "2022-07-08T00:14:07+01:00[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").bind (·.lookup "u-ca".toList) = some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese]").bind (·.lookup "u-ca".toList) = some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ -- Section 3.3, critical: the four examples - ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ ((parseExt "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]").map - (·.erroneous Spec.exampleProcessor) = some true) ∧ + (·.erroneous Rfc3339.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) = + (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ -- Section 3.4, Figures 1 and 2 - ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ - ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ -- Critical zones that agree with the offset, and a critical `-00:00` -- zone, offset 0, under an offset of +01:00 ((parseExt "1996-12-19T16:39:57-08:00[!America/Los_Angeles]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Rfc3339.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]))) ∧ diff --git a/Proofs/Ixdtf/Parse.lean b/Rfc3339/Proofs/Ixdtf/Parse.lean similarity index 64% rename from Proofs/Ixdtf/Parse.lean rename to Rfc3339/Proofs/Ixdtf/Parse.lean index 85cb4c3..45d43cb 100644 --- a/Proofs/Ixdtf/Parse.lean +++ b/Rfc3339/Proofs/Ixdtf/Parse.lean @@ -2,36 +2,36 @@ `parseExt` and `Ext.print` against the grammar. -/ -import Proofs.Ixdtf.Suffix -import Proofs.Main +import Rfc3339.Proofs.Ixdtf.Suffix +import Rfc3339.Proofs.Main open Rfc3339 namespace Rfc3339.Proofs.Ixdtf -theorem px_digitChar_lt (n : Nat) : (Spec.digitChar n).toNat < 91 := by - unfold Spec.digitChar +theorem px_digitChar_lt (n : Nat) : (Rfc3339.Spec.digitChar n).toNat < 91 := by + unfold Rfc3339.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 +theorem px_digits_lt (k n : Nat) : ∀ c ∈ Rfc3339.Spec.digits k n, c.toNat < 91 := by intro c hc - simp only [Spec.digits, List.mem_map] at hc + simp only [Rfc3339.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 +theorem px_renderOffset_lt (o : Offset) : ∀ c ∈ Rfc3339.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] + simp only [Rfc3339.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] +theorem px_render_lt (t : Timestamp) : ∀ c ∈ Rfc3339.Spec.render t, c.toNat < 91 := by + simp only [Rfc3339.Spec.render, List.forall_mem_append, List.forall_mem_cons] and_intros all_goals first | exact px_digits_lt _ _ @@ -47,11 +47,11 @@ theorem px_render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 91 := /-- 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 + (h : dt.map Rfc3339.Spec.asciiUpper = Rfc3339.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 + have hm : Rfc3339.Spec.asciiUpper '[' ∈ Rfc3339.Spec.render t := h ▸ List.mem_map_of_mem hc + have : Rfc3339.Spec.asciiUpper '[' = '[' := by decide rw [this] at hm have := px_render_lt t _ hm simp at this @@ -70,15 +70,15 @@ theorem px_takeWhile_split {dt r : List Char} (hd : ∀ c ∈ dt, c ≠ '[') 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 + Rfc3339.Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Rfc3339.Spec.renderSuffix e ∧ + dt.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render e.stamp := by constructor · intro h simp only [parseExt, bind, Option.bind_eq_some_iff] at h obtain ⟨t, ht, ⟨zone, tags⟩, hs, he⟩ := h simp only [pure, Option.some.injEq] at he subst he - obtain ⟨hv, hu⟩ := (Spec.parse_iff _ t).mp ht + obtain ⟨hv, hu⟩ := (Rfc3339.Spec.parse_iff _ t).mp ht rw [String.toList_ofList] at hu obtain ⟨⟨hz, htags⟩, hsuf⟩ := (parseSuffix_iff _ ⟨t, zone, tags⟩).mp hs @@ -91,20 +91,20 @@ theorem parseExt_iff (s : String) (e : Ext) : 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) := + (Rfc3339.Spec.parse_iff _ _).mpr ⟨hv, by rw [String.toList_ofList]; exact hu⟩ + have hsuf : parseSuffix (Rfc3339.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 +theorem printExt_eq (e : Ext) (h : Rfc3339.Spec.ExtValid e) : + e.print.toList = Rfc3339.Spec.render e.stamp ++ Rfc3339.Spec.renderSuffix e := by rw [Ext.print, String.toList_ofList, - Format.render_eq _ ((Spec.isValid_iff _).mpr h.1), renderSuffix_eq e h.2.1] + Format.render_eq _ ((Rfc3339.Spec.isValid_iff _).mpr h.1), renderSuffix_eq e h.2.1] -theorem parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e := - (parseExt_iff _ e).mpr ⟨h, Spec.render e.stamp, printExt_eq e h, Main.upper_render _⟩ +theorem parseExt_print (e : Ext) (h : Rfc3339.Spec.ExtValid e) : parseExt e.print = some e := + (parseExt_iff _ e).mpr ⟨h, Rfc3339.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 diff --git a/Proofs/Ixdtf/Rules.lean b/Rfc3339/Proofs/Ixdtf/Rules.lean similarity index 79% rename from Proofs/Ixdtf/Rules.lean rename to Rfc3339/Proofs/Ixdtf/Rules.lean index 11205f9..d9eeb7c 100644 --- a/Proofs/Ixdtf/Rules.lean +++ b/Rfc3339/Proofs/Ixdtf/Rules.lean @@ -3,8 +3,8 @@ -/ import Rfc3339 -import Spec.Ixdtf -import Proofs.Valid +import Rfc3339.Spec.Ixdtf +import Rfc3339.Proofs.Valid open Rfc3339 @@ -52,23 +52,23 @@ theorem lookup_iff (e : Ext) (k : List Char) (t : Tag) : exact rx_find_iff k t e.tags -private theorem rx_assertsOffset_iff (o : Offset) : assertsOffset o = true ↔ Spec.AssertsOffset o := by +private theorem rx_assertsOffset_iff (o : Offset) : assertsOffset o = true ↔ Rfc3339.Spec.AssertsOffset o := by cases o with - | z => simp [assertsOffset, Spec.AssertsOffset] - | plus h m => simp [assertsOffset, Spec.AssertsOffset] + | z => simp [assertsOffset, Rfc3339.Spec.AssertsOffset] + | plus h m => simp [assertsOffset, Rfc3339.Spec.AssertsOffset] | minus h m => by_cases hh : h = 0 <;> by_cases hm : m = 0 <;> subst_vars <;> - simp_all [assertsOffset, Spec.AssertsOffset] + simp_all [assertsOffset, Rfc3339.Spec.AssertsOffset] private theorem rx_zoneAgrees_iff (p : Processor) (t : Timestamp) (z : Zone) : - zoneAgrees p t z = true ↔ Spec.ZoneConsistent p t z := by + zoneAgrees p t z = true ↔ Rfc3339.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, + simp only [zoneAgrees, Rfc3339.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] + simp only [zoneAgrees, Rfc3339.Spec.ZoneConsistent] cases hz : p.zoneOffset parts t with | none => simp | some m => @@ -77,8 +77,8 @@ private theorem rx_zoneAgrees_iff (p : Processor) (t : Timestamp) (z : Zone) : cases assertsOffset t.offset <;> simp theorem erroneous_iff (p : Processor) (e : Ext) : - e.erroneous p = true ↔ Spec.MustReject p e := by - simp only [Ext.erroneous, Spec.MustReject, Bool.or_eq_true, List.any_eq_true, + e.erroneous p = true ↔ Rfc3339.Spec.MustReject p e := by + simp only [Ext.erroneous, Rfc3339.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⟩ diff --git a/Proofs/Ixdtf/Suffix.lean b/Rfc3339/Proofs/Ixdtf/Suffix.lean similarity index 77% rename from Proofs/Ixdtf/Suffix.lean rename to Rfc3339/Proofs/Ixdtf/Suffix.lean index f3a5ad5..fc9b476 100644 --- a/Proofs/Ixdtf/Suffix.lean +++ b/Rfc3339/Proofs/Ixdtf/Suffix.lean @@ -3,9 +3,9 @@ -/ import Rfc3339 -import Spec.Ixdtf -import Proofs.Format -import Proofs.Valid +import Rfc3339.Spec.Ixdtf +import Rfc3339.Proofs.Format +import Rfc3339.Proofs.Valid open Rfc3339 @@ -13,21 +13,21 @@ namespace Rfc3339.Proofs.Ixdtf /-! ## Characters -/ -theorem sx_alpha_ne {c : Char} (h : Spec.Alpha c) : +theorem sx_alpha_ne {c : Char} (h : Rfc3339.Spec.Alpha c) : c ≠ ']' ∧ c ≠ '=' ∧ c ≠ '/' ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by - unfold Spec.Alpha at h + unfold Rfc3339.Spec.Alpha at h refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> rintro rfl <;> revert h <;> decide -theorem sx_digit_ne {c : Char} (h : Spec.Digit c) : +theorem sx_digit_ne {c : Char} (h : Rfc3339.Spec.Digit c) : c ≠ ']' ∧ c ≠ '=' ∧ c ≠ '/' ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by - unfold Spec.Digit at h + unfold Rfc3339.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) : +theorem sx_zonePart_chars {p : List Char} (hp : Rfc3339.Spec.ZonePart p) : ∀ x ∈ p, x ≠ ']' ∧ x ≠ '=' ∧ x ≠ '/' := by obtain ⟨c, cs, rfl, hc, hcs, -, -⟩ := hp intro x hx @@ -42,7 +42,7 @@ theorem sx_zonePart_chars {p : List Char} (hp : Spec.ZonePart p) : · 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) : +theorem sx_zonePart_head {p : List Char} (hp : Rfc3339.Spec.ZonePart p) : ∃ c cs, p = c :: cs ∧ c ≠ '!' ∧ c ≠ '+' ∧ c ≠ '-' := by obtain ⟨c, cs, rfl, hc, -, -, -⟩ := hp refine ⟨c, cs, rfl, ?_⟩ @@ -50,7 +50,7 @@ theorem sx_zonePart_head {p : List Char} (hp : Spec.ZonePart p) : · 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 +theorem sx_key_chars {k : List Char} (hk : Rfc3339.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 @@ -63,32 +63,32 @@ theorem sx_key_chars {k : List Char} (hk : Spec.SuffixKey k) : ∀ x ∈ k, x · 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 +theorem sx_key_head {k : List Char} (hk : Rfc3339.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) : +theorem sx_value_chars {v : List Char} (hv : Rfc3339.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 +theorem sx_alpha_iff (c : Char) : isAlpha c = true ↔ Rfc3339.Spec.Alpha c := by + simp [isAlpha, Rfc3339.Spec.Alpha] +theorem sx_digit_iff (c : Char) : isDigitChar c = true ↔ Rfc3339.Spec.Digit c := by + simp [isDigitChar, Rfc3339.Spec.Digit] +theorem sx_keyOK_iff (k : List Char) : keyOK k = true ↔ Rfc3339.Spec.SuffixKey k := by cases k with - | nil => simp [keyOK, Spec.SuffixKey] + | nil => simp [keyOK, Rfc3339.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] + simp only [keyOK, Rfc3339.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_valueOK_iff (v : List Char) : valueOK v = true ↔ Rfc3339.Spec.SuffixValue v := by + simp only [valueOK, Rfc3339.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 @@ -102,8 +102,8 @@ theorem sx_takeWhile_append {p : α → Bool} (xs : List α) (y : α) (ys : List | 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 +theorem sx_digitChar_mem (n : Nat) : Rfc3339.Spec.digitChar n ∈ "0123456789?".toList := by + unfold Rfc3339.Spec.digitChar rw [List.getD_eq_getElem?_getD] cases h : "0123456789".toList[n]? with | none => decide @@ -111,8 +111,8 @@ theorem sx_digitChar_mem (n : Nat) : Spec.digitChar n ∈ "0123456789?".toList : 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 +theorem sx_digits_mem {k n : Nat} {c : Char} (h : c ∈ Rfc3339.Spec.digits k n) : c ∈ "0123456789?".toList := by + unfold Rfc3339.Spec.digits at h simp only [List.mem_map] at h obtain ⟨i, _, rfl⟩ := h exact sx_digitChar_mem _ @@ -142,11 +142,11 @@ theorem sx_join_cons {α : Type} (s p : List α) (rest : List (List α)) : 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 +theorem sx_zonePartOK_iff (p : List Char) : zonePartOK p = true ↔ Rfc3339.Spec.ZonePart p := by cases p with - | nil => simp [zonePartOK, Spec.ZonePart] + | nil => simp [zonePartOK, Rfc3339.Spec.ZonePart] | cons c cs => - simp only [zonePartOK, Spec.ZonePart, sx_alpha_iff, sx_digit_iff, Bool.and_eq_true, + simp only [zonePartOK, Rfc3339.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 @@ -154,10 +154,10 @@ theorem sx_zonePartOK_iff (p : List Char) : zonePartOK p = true ↔ Spec.ZonePar 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 ++ [']'] +def sx_item (c : Bool) (b : List Char) : List Char := ['['] ++ Rfc3339.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 + Rfc3339.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)) @@ -177,7 +177,7 @@ theorem sx_parseTag_sound {c : Bool} {b : List Char} {t : Tag} (h : parseTag c b · simp at h · simp at h -theorem sx_parseTag_render {t : Tag} (h : Spec.TagValid t) : +theorem sx_parseTag_render {t : Tag} (h : Rfc3339.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 @@ -197,7 +197,7 @@ theorem sx_parseTag_render {t : Tag} (h : Spec.TagValid t) : 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 + Rfc3339.Spec.ZoneValid z ∧ b = Rfc3339.Spec.renderZone z := by unfold parseZone at h split at h · rename_i x @@ -236,8 +236,8 @@ theorem sx_parseZone_sound {b : List Char} {z : Zone} (h : parseZone b = some z) 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 +theorem sx_parseZone_render {z : Zone} (h : Rfc3339.Spec.ZoneValid z) : + parseZone (Rfc3339.Spec.renderZone z) = some z := by cases z with | name parts => obtain ⟨hne, hp⟩ := h @@ -267,7 +267,7 @@ theorem sx_parseZone_render {z : Zone} (h : Spec.ZoneValid z) : 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) = _ + show parseZone (Rfc3339.Spec.renderOffset o) = _ rw [← Rfc3339.Proofs.Format.offset_render_eq] cases o with | z => exact absurd rfl hz @@ -283,11 +283,11 @@ theorem sx_parseZone_render {z : Zone} (h : Spec.ZoneValid z) : simp only [hr, hvalid, ↓reduceIte] -theorem sx_digits_ne {k n : Nat} {c : Char} (h : c ∈ Spec.digits k n) : c ≠ ']' ∧ c ≠ '=' := by +theorem sx_digits_ne {k n : Nat} {c : Char} (h : c ∈ Rfc3339.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) : +theorem sx_tagBody_facts {t : Tag} (h : Rfc3339.Spec.TagValid t) : ']' ∉ sx_tagBody t ∧ (sx_tagBody t).head? ≠ some '!' ∧ '=' ∈ sx_tagBody t := by obtain ⟨hk, hne, hv⟩ := h refine ⟨?_, ?_, ?_⟩ @@ -304,8 +304,8 @@ theorem sx_tagBody_facts {t : Tag} (h : Spec.TagValid t) : · 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 +theorem sx_zoneBody_facts {z : Zone} (h : Rfc3339.Spec.ZoneValid z) : + ']' ∉ Rfc3339.Spec.renderZone z ∧ (Rfc3339.Spec.renderZone z).head? ≠ some '!' ∧ '=' ∉ Rfc3339.Spec.renderZone z := by cases z with | name parts => obtain ⟨hne, hp⟩ := h @@ -327,16 +327,16 @@ theorem sx_zoneBody_facts {z : Zone} (h : Spec.ZoneValid z) : 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 + refine ⟨fun hm => ?_, by simp [Rfc3339.Spec.renderZone, Rfc3339.Spec.renderOffset], fun hm => ?_⟩ <;> + · simp only [Rfc3339.Spec.renderZone, Rfc3339.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 + refine ⟨fun hm => ?_, by simp [Rfc3339.Spec.renderZone, Rfc3339.Spec.renderOffset], fun hm => ?_⟩ <;> + · simp only [Rfc3339.Spec.renderZone, Rfc3339.Spec.renderOffset, List.mem_append] at hm rcases hm with ((h | h) | h) | h <;> first | exact absurd h (by decide) @@ -346,14 +346,14 @@ theorem sx_zoneBody_facts {z : Zone} (h : Spec.ZoneValid z) : 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 + have hB : ∀ x ∈ Rfc3339.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 + · cases c <;> simp [Rfc3339.Spec.renderFlag] at h · exact hb h - have e1 : sx_item c b ++ R = '[' :: ((Spec.renderFlag c ++ b) ++ ']' :: R) := by simp [sx_item] + have e1 : sx_item c b ++ R = '[' :: ((Rfc3339.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] @@ -365,7 +365,7 @@ theorem sx_suffixItems_cons (f : Nat) (c : Bool) (b R : List Char) (hb : ']' ∉ 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] + simp only [Rfc3339.Spec.renderFlag, Bool.false_eq_true, ↓reduceIte, List.nil_append, Option.map_some] split · simp at hh · rfl @@ -424,20 +424,20 @@ theorem sx_suffixItems_sound (fuel : Nat) (cs : List Char) (items : List (Bool subst h2 rw [hbody] at hr subst hr - simp [sx_item, Spec.renderFlag] + simp [sx_item, Rfc3339.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 [sx_item, Rfc3339.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 + (∀ t ∈ tags, Rfc3339.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 @@ -455,7 +455,7 @@ theorem sx_mapM_sound (rest : List (Bool × List Char)) (tags : List Tag) · exact htv · exact hv u hu -theorem sx_mapM_render (tags : List Tag) (h : ∀ t ∈ tags, Spec.TagValid t) : +theorem sx_mapM_render (tags : List Tag) (h : ∀ t ∈ tags, Rfc3339.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 @@ -468,26 +468,26 @@ theorem sx_mapM_render (tags : List Tag) (h : ∀ t ∈ tags, Spec.TagValid t) : /-- 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)] + | some (c, z) => [(c, Rfc3339.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_renderTag_eq (t : Tag) : Rfc3339.Spec.renderTag t = sx_item t.critical (sx_tagBody t) := by + simp [Rfc3339.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 + Rfc3339.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 = + have htags : (tags.map Rfc3339.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] + · simp only [Rfc3339.Spec.renderSuffix, sx_items, List.nil_append, htags] + · simp only [Rfc3339.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) : +theorem sx_items_facts (e : Ext) (hz : ∀ c z, e.zone = some (c, z) → Rfc3339.Spec.ZoneValid z) + (ht : ∀ t ∈ e.tags, Rfc3339.Spec.TagValid t) : ∀ p ∈ sx_items e, ']' ∉ p.2 ∧ p.2.head? ≠ some '!' := by obtain ⟨stamp, zone, tags⟩ := e intro p hp @@ -503,11 +503,11 @@ theorem sx_items_facts (e : Ext) (hz : ∀ c z, e.zone = some (c, z) → Spec.Zo exact ⟨this.1, this.2.1⟩ /-- `parseSuffix` reads exactly the suffixes of the grammar, as - `Spec.renderSuffix` writes them. -/ + `Rfc3339.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 + ((∀ c z, e.zone = some (c, z) → Rfc3339.Spec.ZoneValid z) ∧ ∀ t ∈ e.tags, Rfc3339.Spec.TagValid t) ∧ + cs = Rfc3339.Spec.renderSuffix e := by constructor · intro h unfold parseSuffix at h @@ -561,15 +561,15 @@ theorem parseSuffix_iff (cs : List Char) (e : Ext) : | 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 hts : ∀ u ∈ ts, Rfc3339.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 + have hc : (Rfc3339.Spec.renderZone z).contains '=' = false := by + cases h : (Rfc3339.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] @@ -578,16 +578,16 @@ theorem parseSuffix_iff (cs : List Char) (e : Ext) : 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 +theorem renderSuffix_eq (e : Ext) (h : ∀ c z, e.zone = some (c, z) → Rfc3339.Spec.ZoneValid z) : + e.renderSuffix = Rfc3339.Spec.renderSuffix e := by obtain ⟨stamp, zone, tags⟩ := e - have hz : ∀ z : Zone, z.render = Spec.renderZone z := by + have hz : ∀ z : Zone, z.render = Rfc3339.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] + have ht : (Tag.render : Tag → List Char) = Rfc3339.Spec.renderTag := funext fun t => rfl + simp only [Ext.renderSuffix, Rfc3339.Spec.renderSuffix, List.flatMap_def, ht] rcases zone with _ | ⟨c, z⟩ · rfl · simp only [hz] @@ -597,13 +597,13 @@ theorem renderSuffix_eq (e : Ext) (h : ∀ c z, e.zone = some (c, z) → Spec.Zo 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 + Rfc3339.Spec.renderSuffix e = [] ∨ (Rfc3339.Spec.renderSuffix e).head? = some '[' := by obtain ⟨stamp, zone, tags⟩ := e rcases zone with _ | ⟨c, z⟩ · cases tags with | nil => left; rfl - | cons t ts => right; simp [Spec.renderSuffix, Spec.renderTag] + | cons t ts => right; simp [Rfc3339.Spec.renderSuffix, Rfc3339.Spec.renderTag] · right - simp [Spec.renderSuffix] + simp [Rfc3339.Spec.renderSuffix] end Rfc3339.Proofs.Ixdtf diff --git a/Proofs/Leap/FromSi.lean b/Rfc3339/Proofs/Leap/FromSi.lean similarity index 86% rename from Proofs/Leap/FromSi.lean rename to Rfc3339/Proofs/Leap/FromSi.lean index 6d33141..8f3f1f1 100644 --- a/Proofs/Leap/FromSi.lean +++ b/Rfc3339/Proofs/Leap/FromSi.lean @@ -2,9 +2,9 @@ From SI seconds back to a timestamp. -/ -import Proofs.Leap.Si -import Proofs.Leap.Order -import Proofs.FromUnix.Main +import Rfc3339.Proofs.Leap.Si +import Rfc3339.Proofs.Leap.Order +import Rfc3339.Proofs.FromUnix.Main open Rfc3339 @@ -175,18 +175,18 @@ theorem fs_check_leap : ∀ n ∈ leapSiSeconds, fs_check n = true := by decide /-! ## Bounds -/ -theorem fs_unix_1972 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by +theorem fs_unix_1972 : Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by decide +kernel theorem fs_dby_1972 : daysBeforeYear 1972 = 720258 := by decide -theorem fs_si_max : Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253339228826 := by +theorem fs_si_max : Rfc3339.Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253339228826 := by decide +kernel /-- A valid UTC second other than 60, at or after 1972-01-01T00:00:00Z, is in 1972 or later. -/ -theorem fs_year_of_unix (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) - (h59 : t.second ≤ 59) (hu : 63072000 ≤ Spec.unixSeconds t) : 1972 ≤ t.year := by +theorem fs_year_of_unix (t : Timestamp) (hv : Rfc3339.Spec.Valid t) (hz : t.offset = .z) + (h59 : t.second ≤ 59) (hu : 63072000 ≤ Rfc3339.Spec.unixSeconds t) : 1972 ≤ t.year := by apply Nat.le_of_not_lt intro hy obtain ⟨_, hm1, hm2, hd1, hd2, hh, hmi, _⟩ := hv @@ -198,8 +198,8 @@ theorem fs_year_of_unix (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) /-- A valid UTC timestamp in 1972 or later is at or after 1972-01-01T00:00:00Z. -/ -theorem fs_unix_of_year (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) - (hy : 1972 ≤ t.year) : 63072000 ≤ Spec.unixSeconds t := by +theorem fs_unix_of_year (t : Timestamp) (hv : Rfc3339.Spec.Valid t) (hz : t.offset = .z) + (hy : 1972 ≤ t.year) : 63072000 ≤ Rfc3339.Spec.unixSeconds t := by obtain ⟨_, hm1, hm2, hd1, hd2, _⟩ := hv have e := FromUnix.fu_unixSeconds_z t hz have b := FromUnix.dy_dayNumber_bounds t.year t.month t.day ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ @@ -207,14 +207,14 @@ theorem fs_unix_of_year (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) rw [fs_dby_1972] at m omega -theorem fs_si_nonneg (t : Timestamp) (hv : Spec.Valid t) (hz : t.offset = .z) - (hy : 1972 ≤ t.year) : 0 ≤ Spec.siSeconds t := by - unfold Spec.siSeconds +theorem fs_si_nonneg (t : Timestamp) (hv : Rfc3339.Spec.Valid t) (hz : t.offset = .z) + (hy : 1972 ≤ t.year) : 0 ≤ Rfc3339.Spec.siSeconds t := by + unfold Rfc3339.Spec.siSeconds rw [fs_unix_1972] have := fs_unix_of_year t hv hz hy omega -theorem fs_Tmax_known : Spec.ValidKnown ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := +theorem fs_Tmax_known : Rfc3339.Spec.ValidKnown ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := (isValidKnown_iff _).mp (by decide +kernel) theorem fs_Tmax_utcMinute : @@ -223,7 +223,7 @@ theorem fs_Tmax_utcMinute : theorem fs_leapKey_lt_max : ∀ ym ∈ leapMonths, leapKey ym < 5259491999 * 61 + 59 := by decide +kernel -theorem fs_key_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = .z) : +theorem fs_key_le_max (t : Timestamp) (hk : Rfc3339.Spec.ValidKnown t) (hz : t.offset = .z) : t.utcMinute * 61 + t.second ≤ 5259491999 * 61 + 59 := by obtain ⟨hy, hm1, hm2, hd1, hd2, hh, hmi, hs, _⟩ := hk.1 by_cases h60 : t.second = 60 @@ -239,9 +239,9 @@ theorem fs_key_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = /-- A known-valid UTC whole second is no later than 9999-12-31T23:59:59Z, in SI seconds. -/ -theorem fs_si_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = .z) +theorem fs_si_le_max (t : Timestamp) (hk : Rfc3339.Spec.ValidKnown t) (hz : t.offset = .z) (hf : t.fraction = []) : - Spec.siSeconds t ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by + Rfc3339.Spec.siSeconds t ≤ Rfc3339.Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by have ho := siSeconds_order t _ hk fs_Tmax_known hf rfl rw [siSeconds_eq t hk.1, siSeconds_eq _ fs_Tmax_known.1] at ho have hkey : t.utcMinute * 61 + (t.second : Int) ≤ @@ -261,7 +261,7 @@ theorem fs_si_le_max (t : Timestamp) (hk : Spec.ValidKnown t) (hz : t.offset = . /-! ## Uniqueness -/ -theorem fs_eq_of_key (t t' : Timestamp) (hv : Spec.Valid t) (hv' : Spec.Valid t') +theorem fs_eq_of_key (t t' : Timestamp) (hv : Rfc3339.Spec.Valid t) (hv' : Rfc3339.Spec.Valid t') (hz : t.offset = .z) (hz' : t'.offset = .z) (hf : t.fraction = []) (hf' : t'.fraction = []) (h : t.utcMinute * 61 + t.second = t'.utcMinute * 61 + t'.second) : t = t' := by obtain ⟨y, m, d, hh, mi, s, fr, off⟩ := t @@ -274,16 +274,16 @@ theorem fs_eq_of_key (t t' : Timestamp) (hv : Spec.Valid t) (hv' : Spec.Valid t' unfold Timestamp.utcMinute at h simp only [offsetMinutes] at h rw [DayNumber.dayNumber_eq _ _ _ hm1 hm2, DayNumber.dayNumber_eq _ _ _ hm1' hm2'] at h - have hdn : Spec.dayNumber y m d = Spec.dayNumber y' m' d' := by omega + have hdn : Rfc3339.Spec.dayNumber y m d = Rfc3339.Spec.dayNumber y' m' d' := by omega obtain ⟨rfl, rfl, rfl⟩ := FromUnix.dayNumber_inj y m d y' m' d' ⟨hm1, hm2⟩ ⟨hd1, hd2⟩ ⟨hm1', hm2'⟩ ⟨hd1', hd2'⟩ hdn have : hh = hh' ∧ mi = mi' ∧ s = s' := by omega obtain ⟨rfl, rfl, rfl⟩ := this rfl -theorem fs_eq_of_si (t t' : Timestamp) (hk : Spec.ValidKnown t) (hk' : Spec.ValidKnown t') +theorem fs_eq_of_si (t t' : Timestamp) (hk : Rfc3339.Spec.ValidKnown t) (hk' : Rfc3339.Spec.ValidKnown t') (hz : t.offset = .z) (hz' : t'.offset = .z) (hf : t.fraction = []) (hf' : t'.fraction = []) - (h : Spec.siSeconds t = Spec.siSeconds t') : t = t' := by + (h : Rfc3339.Spec.siSeconds t = Rfc3339.Spec.siSeconds t') : t = t' := by have ho := siSeconds_order t t' hk hk' hf hf' rw [siSeconds_eq t hk.1, siSeconds_eq t' hk'.1, h, Int.compare_eq_eq.mpr rfl] at ho apply fs_eq_of_key t t' hk.1 hk'.1 hz hz' hf hf' @@ -298,8 +298,8 @@ theorem fs_eq_of_si (t t' : Timestamp) (hk : Spec.ValidKnown t) (hk' : Spec.Vali /-! ## The two directions -/ theorem fs_forward (n : Int) (t : Timestamp) (h : fromSiSeconds n = some t) : - t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ - Spec.siSeconds t = n := by + t.offset = .z ∧ t.fraction = [] ∧ Rfc3339.Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Rfc3339.Spec.siSeconds t = n := by by_cases hl : n ∈ leapSiSeconds · have hc := fs_check_leap n hl unfold fs_check at hc @@ -317,7 +317,7 @@ theorem fs_forward (n : Int) (t : Timestamp) (h : fromSiSeconds n = some t) : · contradiction rename_i hn0 simp only [hcont, Bool.false_eq_true, ite_false] at h - obtain ⟨hv, hz, hf, h59, hu⟩ := (Spec.fromUnixSeconds_iff _ _).mp h + obtain ⟨hv, hz, hf, h59, hu⟩ := (Rfc3339.Spec.fromUnixSeconds_iff _ _).mp h have hU : t.unixSeconds = n + 63072000 - (leapSiSeconds.filter (· < n)).length := by rw [Instant.unixSeconds_eq t hv]; exact hu obtain ⟨hk27, hc⟩ := fs_k_char n @@ -341,7 +341,7 @@ theorem fs_forward (n : Int) (t : Timestamp) (h : fromSiSeconds n = some t) : rw [fs_V_zero] at h2 omega exact key _ hk27 hc - have hs : Spec.siSeconds t = n := by + have hs : Rfc3339.Spec.siSeconds t = n := by rw [← siSeconds_eq t hv] unfold Timestamp.siSeconds rw [hU, hlb] @@ -364,17 +364,17 @@ theorem fs_isSome_of_bounds (n : Int) (h0 : 0 ≤ n) (h1 : n ≤ 253339228826) : dsimp only split · rw [Option.isSome_map] - apply (Spec.fromUnixSeconds_isSome _).mpr + apply (Rfc3339.Spec.fromUnixSeconds_isSome _).mpr rw [FromUnix.fu_unixSeconds_lo, FromUnix.fu_unixSeconds_hi] omega - · apply (Spec.fromUnixSeconds_isSome _).mpr + · apply (Rfc3339.Spec.fromUnixSeconds_isSome _).mpr rw [FromUnix.fu_unixSeconds_lo, FromUnix.fu_unixSeconds_hi] omega theorem fromSiSeconds_iff (n : Int) (t : Timestamp) : fromSiSeconds n = some t ↔ - t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ - Spec.siSeconds t = n := by + t.offset = .z ∧ t.fraction = [] ∧ Rfc3339.Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Rfc3339.Spec.siSeconds t = n := by constructor · exact fs_forward n t · rintro ⟨hz, hf, hk, hy, hs⟩ @@ -388,7 +388,7 @@ theorem fromSiSeconds_iff (n : Int) (t : Timestamp) : theorem fromSiSeconds_isSome (n : Int) : (fromSiSeconds n).isSome ↔ - 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by + 0 ≤ n ∧ n ≤ Rfc3339.Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := by constructor · intro h obtain ⟨t, ht⟩ := Option.isSome_iff_exists.mp h diff --git a/Proofs/Leap/Main.lean b/Rfc3339/Proofs/Leap/Main.lean similarity index 63% rename from Proofs/Leap/Main.lean rename to Rfc3339/Proofs/Leap/Main.lean index c9540f6..8124bcd 100644 --- a/Proofs/Leap/Main.lean +++ b/Rfc3339/Proofs/Leap/Main.lean @@ -1,51 +1,51 @@ /- - The leap second statements of `Spec.lean`, under the same names, from - the lemmas in the other files of `Proofs/Leap/`. The test vectors are + The leap second statements of `Rfc3339/Spec.lean`, under the same names, from + the lemmas in the other files of `Rfc3339/Proofs/Leap/`. The test vectors are checked by evaluation. -/ -import Proofs.Leap.Table -import Proofs.Leap.Si -import Proofs.Leap.Order -import Proofs.Leap.FromSi +import Rfc3339.Proofs.Leap.Table +import Rfc3339.Proofs.Leap.Si +import Rfc3339.Proofs.Leap.Order +import Rfc3339.Proofs.Leap.FromSi open Rfc3339 -theorem Spec.isValidKnown_iff (t : Timestamp) : - t.isValidKnown = true ↔ Spec.ValidKnown t := +theorem Rfc3339.Spec.isValidKnown_iff (t : Timestamp) : + t.isValidKnown = true ↔ Rfc3339.Spec.ValidKnown t := Rfc3339.Proofs.Leap.isValidKnown_iff t -theorem Spec.siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : - t.siSeconds = Spec.siSeconds t := +theorem Rfc3339.Spec.siSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.siSeconds = Rfc3339.Spec.siSeconds t := Rfc3339.Proofs.Leap.siSeconds_eq t h -theorem Spec.siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) +theorem Rfc3339.Spec.siSeconds_order (a b : Timestamp) (ha : Rfc3339.Spec.ValidKnown a) (hb : Rfc3339.Spec.ValidKnown b) (fa : a.fraction = []) (fb : b.fraction = []) : compare a.siSeconds b.siSeconds = a.compareInstant b := Rfc3339.Proofs.Leap.siSeconds_order a b ha hb fa fb -theorem Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : +theorem Rfc3339.Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : fromSiSeconds n = some t ↔ - t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ - Spec.siSeconds t = n := + t.offset = .z ∧ t.fraction = [] ∧ Rfc3339.Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Rfc3339.Spec.siSeconds t = n := Rfc3339.Proofs.Leap.fromSiSeconds_iff n t -theorem Spec.fromSiSeconds_isSome (n : Int) : +theorem Rfc3339.Spec.fromSiSeconds_isSome (n : Int) : (fromSiSeconds n).isSome ↔ - 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := + 0 ≤ n ∧ n ≤ Rfc3339.Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := Rfc3339.Proofs.Leap.fromSiSeconds_isSome n -theorem Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Spec.Valid t) : - t.taiMinusUtc = 10 + Spec.leapsBefore t := by +theorem Rfc3339.Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.taiMinusUtc = 10 + Rfc3339.Spec.leapsBefore t := by unfold Timestamp.taiMinusUtc rw [Rfc3339.Proofs.Leap.leapsBefore_eq t h] -theorem Spec.taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) - (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : - t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := +theorem Rfc3339.Spec.taiMinusUtc_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Rfc3339.Spec.unixSeconds t) : + t.taiMinusUtc = Rfc3339.Spec.taiMinusUtcAt (Rfc3339.Spec.ntpOfUnix (Rfc3339.Spec.unixSeconds t)) := Rfc3339.Proofs.Leap.taiMinusUtc_eq t h h60 h72 -theorem Spec.leap_table_vectors : +theorem Rfc3339.Spec.leap_table_vectors : Timestamp.isValidKnown ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ Timestamp.isValidKnown ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = true ∧ Timestamp.isValidKnown ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = true ∧ diff --git a/Proofs/Leap/Order.lean b/Rfc3339/Proofs/Leap/Order.lean similarity index 90% rename from Proofs/Leap/Order.lean rename to Rfc3339/Proofs/Leap/Order.lean index 9d1d136..a0c0681 100644 --- a/Proofs/Leap/Order.lean +++ b/Rfc3339/Proofs/Leap/Order.lean @@ -2,7 +2,7 @@ SI seconds order known-valid whole seconds as their instants. -/ -import Proofs.Leap.Table +import Rfc3339.Proofs.Leap.Table open Rfc3339 @@ -55,7 +55,7 @@ private theorem or_si (t : Timestamp) : unfold Timestamp.siSeconds rw [or_unix] -private theorem or_lt (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) +private theorem or_lt (a b : Timestamp) (ha : Rfc3339.Spec.ValidKnown a) (hb : Rfc3339.Spec.ValidKnown b) (h : a.utcMinute * 61 + a.second < b.utcMinute * 61 + b.second) : a.siSeconds < b.siSeconds := by obtain ⟨_, _, _, _, _, _, _, hsa, _⟩ := ha.1 @@ -72,7 +72,7 @@ private theorem or_lt (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.Vali omega · omega -private theorem or_eq (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) +private theorem or_eq (a b : Timestamp) (ha : Rfc3339.Spec.ValidKnown a) (hb : Rfc3339.Spec.ValidKnown b) (h : a.utcMinute * 61 + a.second = b.utcMinute * 61 + b.second) : a.siSeconds = b.siSeconds := by obtain ⟨_, _, _, _, _, _, _, hsa, _⟩ := ha.1 @@ -83,7 +83,7 @@ private theorem or_eq (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.Vali rw [or_si, or_si, hL] omega -theorem siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) +theorem siSeconds_order (a b : Timestamp) (ha : Rfc3339.Spec.ValidKnown a) (hb : Rfc3339.Spec.ValidKnown b) (fa : a.fraction = []) (fb : b.fraction = []) : compare a.siSeconds b.siSeconds = a.compareInstant b := by unfold Timestamp.compareInstant diff --git a/Proofs/Leap/Si.lean b/Rfc3339/Proofs/Leap/Si.lean similarity index 61% rename from Proofs/Leap/Si.lean rename to Rfc3339/Proofs/Leap/Si.lean index a298d9a..51dc616 100644 --- a/Proofs/Leap/Si.lean +++ b/Rfc3339/Proofs/Leap/Si.lean @@ -2,7 +2,7 @@ SI seconds and TAI − UTC against the spec. -/ -import Proofs.Leap.Table +import Rfc3339.Proofs.Leap.Table open Rfc3339 @@ -15,23 +15,23 @@ theorem si_length_filter_map {α β : Type} (l : List α) (f : α → β) (p : rw [List.filter_map, List.length_map] rfl -theorem leapsBefore_eq (t : Timestamp) (h : Spec.Valid t) : - t.leapsBefore = Spec.leapsBefore t := by - unfold Timestamp.leapsBefore Spec.leapsBefore +theorem leapsBefore_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.leapsBefore = Rfc3339.Spec.leapsBefore t := by + unfold Timestamp.leapsBefore Rfc3339.Spec.leapsBefore rw [Instant.utcMinute_eq t h] have h1 := si_length_filter_map leapMonths leapKey - (fun k => decide (k < Spec.utcMinute t * 61 + (t.second : Int))) - have h2 := si_length_filter_map Spec.leapTable.tail (fun e => Spec.leapSecondKey e.1) - (fun k => decide (k < Spec.utcMinute t * 61 + (t.second : Int))) + (fun k => decide (k < Rfc3339.Spec.utcMinute t * 61 + (t.second : Int))) + have h2 := si_length_filter_map Rfc3339.Spec.leapTable.tail (fun e => Rfc3339.Spec.leapSecondKey e.1) + (fun k => decide (k < Rfc3339.Spec.utcMinute t * 61 + (t.second : Int))) rw [leapKey_table] at h1 rw [← h1, h2] rfl -theorem si_unix1972 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by +theorem si_unix1972 : Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ = 63072000 := by decide +kernel -theorem siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : t.siSeconds = Spec.siSeconds t := by - unfold Timestamp.siSeconds Spec.siSeconds +theorem siSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : t.siSeconds = Rfc3339.Spec.siSeconds t := by + unfold Timestamp.siSeconds Rfc3339.Spec.siSeconds rw [Instant.unixSeconds_eq t h, si_unix1972, leapsBefore_eq t h] /-- The shape of the table after its first line: NTP times strictly @@ -81,33 +81,33 @@ theorem si_lastLine (l : List (Nat × Nat)) : omega simp [hx, hx', hnil] -theorem si_table_shape : si_shape 2272060800 10 Spec.leapTable.tail = true := by +theorem si_table_shape : si_shape 2272060800 10 Rfc3339.Spec.leapTable.tail = true := by decide +kernel -theorem si_table_mod : ∀ e ∈ Spec.leapTable.tail, e.1 % 60 = 0 := by +theorem si_table_mod : ∀ e ∈ Rfc3339.Spec.leapTable.tail, e.1 % 60 = 0 := by decide +kernel theorem si_taiMinusUtcAt (x : Int) (hx : 2272060800 ≤ x) : - Spec.taiMinusUtcAt x = 10 + (Spec.leapTable.tail.filter fun e => decide ((e.1 : Int) ≤ x)).length := by - unfold Spec.taiMinusUtcAt - have hl : Spec.leapTable = (2272060800, 10) :: Spec.leapTable.tail := rfl + Rfc3339.Spec.taiMinusUtcAt x = 10 + (Rfc3339.Spec.leapTable.tail.filter fun e => decide ((e.1 : Int) ≤ x)).length := by + unfold Rfc3339.Spec.taiMinusUtcAt + have hl : Rfc3339.Spec.leapTable = (2272060800, 10) :: Rfc3339.Spec.leapTable.tail := rfl rw [hl] - exact si_lastLine Spec.leapTable.tail 2272060800 10 x si_table_shape (by omega) + exact si_lastLine Rfc3339.Spec.leapTable.tail 2272060800 10 x si_table_shape (by omega) -theorem taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) - (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : - t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := by +theorem taiMinusUtc_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Rfc3339.Spec.unixSeconds t) : + t.taiMinusUtc = Rfc3339.Spec.taiMinusUtcAt (Rfc3339.Spec.ntpOfUnix (Rfc3339.Spec.unixSeconds t)) := by have hs : t.second ≤ 60 := h.2.2.2.2.2.2.2.1 rw [si_unix1972] at h72 unfold Timestamp.taiMinusUtc - rw [leapsBefore_eq t h, si_taiMinusUtcAt _ (by unfold Spec.ntpOfUnix; omega)] + rw [leapsBefore_eq t h, si_taiMinusUtcAt _ (by unfold Rfc3339.Spec.ntpOfUnix; omega)] congr 1 - unfold Spec.leapsBefore + unfold Rfc3339.Spec.leapsBefore congr 1 apply List.filter_congr intro e he have hm := si_table_mod e he - unfold Spec.leapSecondKey Spec.secondKey Spec.ntpOfUnix Spec.unixSeconds + unfold Rfc3339.Spec.leapSecondKey Rfc3339.Spec.secondKey Rfc3339.Spec.ntpOfUnix Rfc3339.Spec.unixSeconds rw [Instant.dayNumber_epoch] simp only [decide_eq_decide] omega diff --git a/Proofs/Leap/Table.lean b/Rfc3339/Proofs/Leap/Table.lean similarity index 74% rename from Proofs/Leap/Table.lean rename to Rfc3339/Proofs/Leap/Table.lean index 22a091a..f7d4899 100644 --- a/Proofs/Leap/Table.lean +++ b/Rfc3339/Proofs/Leap/Table.lean @@ -1,13 +1,13 @@ /- The leap second table: the code's (year, month) list against the - spec's NTP times, and `isValidKnown` against `Spec.ValidKnown`. + spec's NTP times, and `isValidKnown` against `Rfc3339.Spec.ValidKnown`. -/ import Rfc3339 -import Spec.Leap -import Proofs.Valid -import Proofs.Instant -import Proofs.FromUnix.Day +import Rfc3339.Spec.Leap +import Rfc3339.Proofs.Valid +import Rfc3339.Proofs.Instant +import Rfc3339.Proofs.FromUnix.Day open Rfc3339 @@ -16,7 +16,7 @@ namespace Rfc3339.Proofs.Leap /-- The leap seconds of the code's list, in order, are those of the table's lines after the first. -/ theorem leapKey_table : - leapMonths.map leapKey = Spec.leapTable.tail.map (fun e => Spec.leapSecondKey e.1) := by + leapMonths.map leapKey = Rfc3339.Spec.leapTable.tail.map (fun e => Rfc3339.Spec.leapSecondKey e.1) := by decide +kernel /-- The day number of the first day of the month after `ym`, as @@ -29,7 +29,7 @@ theorem tb_leapKey_eq (ym : Nat × Nat) : /-- Each NTP time of the table after the first line is a whole number of minutes after the Unix epoch. -/ -theorem tb_table_div : ∀ e ∈ Spec.leapTable.tail, ((e.1 : Int) - Spec.ntpOfUnix 0) % 60 = 0 := by +theorem tb_table_div : ∀ e ∈ Rfc3339.Spec.leapTable.tail, ((e.1 : Int) - Rfc3339.Spec.ntpOfUnix 0) % 60 = 0 := by decide +kernel /-- Facts about each month of the code's list: its range, and that the @@ -41,14 +41,14 @@ theorem tb_months : ∀ ym ∈ leapMonths, 1972 ≤ ym.1 ∧ ym.1 ≤ 2016 ∧ 1 /-- The month after `(y, m)` starts `daysInMonth y m` days after it. -/ theorem tb_next_eq (y m : Nat) (hm1 : 1 ≤ m) (hm2 : m ≤ 12) : - tb_next (y, m) = Spec.dayNumber y m 1 + Spec.daysInMonth y m := by + tb_next (y, m) = Rfc3339.Spec.dayNumber y m 1 + Rfc3339.Spec.daysInMonth y m := by unfold tb_next simp only split · rename_i h12 subst h12 rw [DayNumber.dayNumber_eq _ _ _ (by decide) (by decide), ← Valid.next_year y] - simp [Spec.daysInMonth] + simp [Rfc3339.Spec.daysInMonth] · rw [DayNumber.dayNumber_eq _ _ _ (by omega) (by omega), Valid.next_month y m hm1] theorem tb_utcMonth_eq (t : Timestamp) : @@ -56,41 +56,41 @@ theorem tb_utcMonth_eq (t : Timestamp) : (fromDayNumber (t.utcMinute / 1440).toNat).2.1) := rfl /-- At second 60, a leap second of the code's list is one of the table's. -/ -theorem tb_key_iff_table (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) : - (∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second) ↔ Spec.TableLeapSecond t := by +theorem tb_key_iff_table (t : Timestamp) (h : Rfc3339.Spec.Valid t) (h60 : t.second = 60) : + (∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second) ↔ Rfc3339.Spec.TableLeapSecond t := by have e1 : (∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second) ↔ - ∃ e ∈ Spec.leapTable.tail, Spec.leapSecondKey e.1 = t.utcMinute * 61 + t.second := by + ∃ e ∈ Rfc3339.Spec.leapTable.tail, Rfc3339.Spec.leapSecondKey e.1 = t.utcMinute * 61 + t.second := by have := congrArg (fun l => t.utcMinute * 61 + t.second ∈ l) leapKey_table simp only [List.mem_map] at this exact Iff.of_eq this rw [e1, Instant.utcMinute_eq t h] - unfold Spec.TableLeapSecond + unfold Rfc3339.Spec.TableLeapSecond simp only [h60, true_and] constructor · rintro ⟨e, he, hk⟩ refine ⟨e, he, ?_⟩ have hd := tb_table_div e he - unfold Spec.leapSecondKey at hk - unfold Spec.unixSeconds + unfold Rfc3339.Spec.leapSecondKey at hk + unfold Rfc3339.Spec.unixSeconds rw [Instant.dayNumber_epoch] at hk ⊢ - simp only [Spec.ntpOfUnix] at hk hd ⊢ + simp only [Rfc3339.Spec.ntpOfUnix] at hk hd ⊢ omega · rintro ⟨e, he, hk⟩ refine ⟨e, he, ?_⟩ - unfold Spec.leapSecondKey - unfold Spec.unixSeconds at hk + unfold Rfc3339.Spec.leapSecondKey + unfold Rfc3339.Spec.unixSeconds at hk rw [Instant.dayNumber_epoch] at hk ⊢ - simp only [Spec.ntpOfUnix] at hk ⊢ + simp only [Rfc3339.Spec.ntpOfUnix] at hk ⊢ omega /-- At a valid second 60, the code's month test is the leap second key test. -/ -theorem tb_contains_iff (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) : +theorem tb_contains_iff (t : Timestamp) (h : Rfc3339.Spec.Valid t) (h60 : t.second = 60) : leapMonths.contains t.utcMonth = true ↔ ∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second := by obtain ⟨y, m, hm1, hm2, hD⟩ := h.2.2.2.2.2.2.2.2.1 h60 rw [← Instant.utcMinute_eq t h] at hD have hkey : ∀ ym, leapKey ym = t.utcMinute * 61 + t.second ↔ - tb_next ym = Spec.dayNumber y m 1 := by + tb_next ym = Rfc3339.Spec.dayNumber y m 1 := by intro ym rw [tb_leapKey_eq, h60] omega @@ -112,14 +112,14 @@ theorem tb_contains_iff (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) have := FromUnix.dy_mono hp1 omega have h72' : 0 < daysBeforeYear 1972 := by decide - have hnD : n + 1 = Spec.dayNumber y m 1 := by omega + have hnD : n + 1 = Rfc3339.Spec.dayNumber y m 1 := by omega obtain ⟨-, hm1', hm2', hd1', hd2', hdn⟩ := FromUnix.fromDayNumber_spec n h10 refine ⟨_, hmem, ?_⟩ rw [tb_next_eq _ _ hm1' hm2'] have hday := Valid.dayNumber_day (fromDayNumber n).1 (fromDayNumber n).2.1 (fromDayNumber n).2.2 have hsp := Valid.month_start_spaced hm1' hm2' hm1 hm2 (show - Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 1 < Spec.dayNumber y m 1 by omega) + Rfc3339.Spec.dayNumber (fromDayNumber n).1 (fromDayNumber n).2.1 1 < Rfc3339.Spec.dayNumber y m 1 by omega) omega · rintro ⟨ym, hmem, hk⟩ obtain ⟨-, -, -, -, hn1, hy, hm⟩ := tb_months ym hmem @@ -127,8 +127,8 @@ theorem tb_contains_iff (t : Timestamp) (h : Spec.Valid t) (h60 : t.second = 60) rw [hn, hy, hm] exact hmem -theorem isValidKnown_iff (t : Timestamp) : t.isValidKnown = true ↔ Spec.ValidKnown t := by - unfold Timestamp.isValidKnown Spec.ValidKnown +theorem isValidKnown_iff (t : Timestamp) : t.isValidKnown = true ↔ Rfc3339.Spec.ValidKnown t := by + unfold Timestamp.isValidKnown Rfc3339.Spec.ValidKnown simp only [Bool.and_eq_true, Bool.or_eq_true, bne_iff_ne, ne_eq, Valid.isValid_iff] constructor · rintro ⟨hv, hl⟩ @@ -143,15 +143,15 @@ theorem isValidKnown_iff (t : Timestamp) : t.isValidKnown = true ↔ Spec.ValidK · exact Or.inl h60 /-- A known-valid second 60 sits at one of the list's leap seconds. -/ -theorem leapKey_of_known (t : Timestamp) (h : Spec.ValidKnown t) (h60 : t.second = 60) : +theorem leapKey_of_known (t : Timestamp) (h : Rfc3339.Spec.ValidKnown t) (h60 : t.second = 60) : ∃ ym ∈ leapMonths, leapKey ym = t.utcMinute * 61 + t.second := (tb_key_iff_table t h.1 h60).2 (h.2 h60) /-- And a valid second 60 at one of the list's leap seconds is known valid. -/ -theorem known_of_leapKey (t : Timestamp) (h : Spec.Valid t) (ym : Nat × Nat) +theorem known_of_leapKey (t : Timestamp) (h : Rfc3339.Spec.Valid t) (ym : Nat × Nat) (hym : ym ∈ leapMonths) (hk : leapKey ym = t.utcMinute * 61 + t.second) : - Spec.ValidKnown t := + Rfc3339.Spec.ValidKnown t := ⟨h, fun h60 => (tb_key_iff_table t h h60).1 ⟨ym, hym, hk⟩⟩ end Rfc3339.Proofs.Leap diff --git a/Proofs/Main.lean b/Rfc3339/Proofs/Main.lean similarity index 55% rename from Proofs/Main.lean rename to Rfc3339/Proofs/Main.lean index 0870fe6..cf19d8d 100644 --- a/Proofs/Main.lean +++ b/Rfc3339/Proofs/Main.lean @@ -1,49 +1,49 @@ /- - The statements of `Spec.lean`, under the same names, from the lemmas - in the other files of `Proofs/`. The test vectors are checked by + The statements of `Rfc3339/Spec.lean`, under the same names, from the lemmas + in the other files of `Rfc3339/Proofs/`. The test vectors are checked by evaluation. -/ import Rfc3339 -import Spec.Defs -import Proofs.Valid -import Proofs.Format -import Proofs.Instant +import Rfc3339.Spec.Defs +import Rfc3339.Proofs.Valid +import Rfc3339.Proofs.Format +import Rfc3339.Proofs.Instant open Rfc3339 namespace Rfc3339.Proofs.Main -/-- Every character `Spec.render` writes is below `a`, so upper case +/-- Every character `Rfc3339.Spec.render` writes is below `a`, so upper case leaves it alone. -/ -theorem upper_fixed (c : Char) (h : c.toNat < 97) : Spec.asciiUpper c = c := by - unfold Spec.asciiUpper +theorem upper_fixed (c : Char) (h : c.toNat < 97) : Rfc3339.Spec.asciiUpper c = c := by + unfold Rfc3339.Spec.asciiUpper simp only [ite_eq_right_iff] omega -theorem digitChar_lt (n : Nat) : (Spec.digitChar n).toNat < 97 := by - unfold Spec.digitChar +theorem digitChar_lt (n : Nat) : (Rfc3339.Spec.digitChar n).toNat < 97 := by + unfold Rfc3339.Spec.digitChar rcases Nat.lt_or_ge n 10 with h | h · have : ∀ i : Fin 10, ("0123456789".toList.getD i.val '?').toNat < 97 := by decide exact this ⟨n, h⟩ · obtain ⟨k, rfl⟩ : ∃ k, n = k + 10 := ⟨n - 10, by omega⟩ simp [List.getD_eq_getElem?_getD] -theorem digits_lt (k n : Nat) : ∀ c ∈ Spec.digits k n, c.toNat < 97 := by +theorem digits_lt (k n : Nat) : ∀ c ∈ Rfc3339.Spec.digits k n, c.toNat < 97 := by intro c hc - simp only [Spec.digits, List.mem_map] at hc + simp only [Rfc3339.Spec.digits, List.mem_map] at hc obtain ⟨_, _, rfl⟩ := hc exact digitChar_lt _ -theorem renderOffset_lt (o : Offset) : ∀ c ∈ Spec.renderOffset o, c.toNat < 97 := by +theorem renderOffset_lt (o : Offset) : ∀ c ∈ Rfc3339.Spec.renderOffset o, c.toNat < 97 := by cases o with | z => decide | plus h m | minus h m => - simp only [Spec.renderOffset, List.forall_mem_append, List.forall_mem_cons] + simp only [Rfc3339.Spec.renderOffset, List.forall_mem_append, List.forall_mem_cons] exact ⟨⟨⟨⟨by decide, by simp⟩, digits_lt _ _⟩, ⟨by decide, by simp⟩⟩, digits_lt _ _⟩ -theorem render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 97 := by - simp only [Spec.render, List.forall_mem_append, List.forall_mem_cons] +theorem render_lt (t : Timestamp) : ∀ c ∈ Rfc3339.Spec.render t, c.toNat < 97 := by + simp only [Rfc3339.Spec.render, List.forall_mem_append, List.forall_mem_cons] and_intros all_goals first | exact digits_lt _ _ @@ -57,47 +57,47 @@ theorem render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 97 := by List.forall_mem_map] exact ⟨⟨by decide, by simp⟩, fun _ _ => digitChar_lt _⟩ -theorem upper_render (t : Timestamp) : (Spec.render t).map Spec.asciiUpper = Spec.render t := by - conv => rhs; rw [← List.map_id (Spec.render t)] +theorem upper_render (t : Timestamp) : (Rfc3339.Spec.render t).map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render t := by + conv => rhs; rw [← List.map_id (Rfc3339.Spec.render t)] exact List.map_congr_left fun c hc => upper_fixed c (render_lt t c hc) end Rfc3339.Proofs.Main open Rfc3339.Proofs -theorem Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := +theorem Rfc3339.Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Rfc3339.Spec.Valid t := Valid.isValid_iff t -theorem Spec.print_eq (t : Timestamp) (h : Spec.Valid t) : - t.print.toList = Spec.render t := by - rw [Format.print_toList, Format.render_eq t ((Spec.isValid_iff t).mpr h)] +theorem Rfc3339.Spec.print_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.print.toList = Rfc3339.Spec.render t := by + rw [Format.print_toList, Format.render_eq t ((Rfc3339.Spec.isValid_iff t).mpr h)] -theorem Spec.parse_iff (s : String) (t : Timestamp) : - parse s = some t ↔ Spec.Valid t ∧ s.toList.map Spec.asciiUpper = Spec.render t := by - rw [Format.parse_iff', Spec.isValid_iff] +theorem Rfc3339.Spec.parse_iff (s : String) (t : Timestamp) : + parse s = some t ↔ Rfc3339.Spec.Valid t ∧ s.toList.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render t := by + rw [Format.parse_iff', Rfc3339.Spec.isValid_iff] -theorem Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : - Spec.Valid t := - ((Spec.parse_iff s t).mp h).1 +theorem Rfc3339.Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : + Rfc3339.Spec.Valid t := + ((Rfc3339.Spec.parse_iff s t).mp h).1 -theorem Spec.parse_print (t : Timestamp) (h : Spec.Valid t) : parse t.print = some t := by - rw [Spec.parse_iff, Spec.print_eq t h] +theorem Rfc3339.Spec.parse_print (t : Timestamp) (h : Rfc3339.Spec.Valid t) : parse t.print = some t := by + rw [Rfc3339.Spec.parse_iff, Rfc3339.Spec.print_eq t h] exact ⟨h, Main.upper_render t⟩ -theorem Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : - t.print.toList = s.toList.map Spec.asciiUpper := by - obtain ⟨hv, hs⟩ := (Spec.parse_iff s t).mp h - rw [Spec.print_eq t hv, hs] +theorem Rfc3339.Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : + t.print.toList = s.toList.map Rfc3339.Spec.asciiUpper := by + obtain ⟨hv, hs⟩ := (Rfc3339.Spec.parse_iff s t).mp h + rw [Rfc3339.Spec.print_eq t hv, hs] -theorem Spec.unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : - t.unixSeconds = Spec.unixSeconds t := +theorem Rfc3339.Spec.unixSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.unixSeconds = Rfc3339.Spec.unixSeconds t := Instant.unixSeconds_eq t h -theorem Spec.compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : - a.compareInstant b = Spec.compareInstants a b := +theorem Rfc3339.Spec.compareInstant_eq (a b : Timestamp) (ha : Rfc3339.Spec.Valid a) (hb : Rfc3339.Spec.Valid b) : + a.compareInstant b = Rfc3339.Spec.compareInstants a b := Instant.compareInstant_eq a b ha hb -theorem Spec.rfc3339_examples : +theorem Rfc3339.Spec.rfc3339_examples : parse "1985-04-12T23:20:50.52Z" = some ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ ∧ parse "1996-12-19T16:39:57-08:00" = some ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ∧ parse "1990-12-31T23:59:60Z" = some ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ ∧ @@ -106,21 +106,21 @@ theorem Spec.rfc3339_examples : some ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ := by decide -theorem Spec.rfc3339_example_instants : +theorem Rfc3339.Spec.rfc3339_example_instants : (Timestamp.compareInstant ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ⟨1996, 12, 20, 0, 39, 57, [], .z⟩ = .eq) ∧ (Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = .eq) ∧ Timestamp.unixSeconds ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = 482196050 := by -- `compareFraction` is defined by well-founded recursion, which `decide` - -- does not unfold, so the orders go through `Spec.compareInstant_eq`. + -- does not unfold, so the orders go through `Rfc3339.Spec.compareInstant_eq`. refine ⟨?_, ?_, by decide⟩ all_goals - rw [Spec.compareInstant_eq _ _ ((Spec.isValid_iff _).mp (by decide)) - ((Spec.isValid_iff _).mp (by decide))] + rw [Rfc3339.Spec.compareInstant_eq _ _ ((Rfc3339.Spec.isValid_iff _).mp (by decide)) + ((Rfc3339.Spec.isValid_iff _).mp (by decide))] decide +kernel -theorem Spec.leap_second_order : +theorem Rfc3339.Spec.leap_second_order : Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 59, [9], .z⟩ ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = .lt ∧ Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [5], .z⟩ @@ -131,11 +131,11 @@ theorem Spec.leap_second_order : Timestamp.unixSeconds ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ := by refine ⟨?_, ?_, ?_, by decide⟩ all_goals - rw [Spec.compareInstant_eq _ _ ((Spec.isValid_iff _).mp (by decide)) - ((Spec.isValid_iff _).mp (by decide))] + rw [Rfc3339.Spec.compareInstant_eq _ _ ((Rfc3339.Spec.isValid_iff _).mp (by decide)) + ((Rfc3339.Spec.isValid_iff _).mp (by decide))] decide +kernel -theorem Spec.calendar_vectors : +theorem Rfc3339.Spec.calendar_vectors : (parse "2000-02-29T00:00:00Z").isSome ∧ (parse "2004-02-29T00:00:00Z").isSome ∧ parse "1900-02-29T00:00:00Z" = none ∧ @@ -148,7 +148,7 @@ theorem Spec.calendar_vectors : parse "2001-13-01T00:00:00Z" = none := by decide -theorem Spec.leap_second_vectors : +theorem Rfc3339.Spec.leap_second_vectors : (parse "1990-06-30T23:59:60Z").isSome ∧ (parse "1991-01-01T00:59:60+01:00").isSome ∧ parse "1990-12-31T23:59:61Z" = none ∧ @@ -157,7 +157,7 @@ theorem Spec.leap_second_vectors : parse "1990-12-31T23:59:60+01:00" = none := by decide -theorem Spec.syntax_vectors : +theorem Rfc3339.Spec.syntax_vectors : parse "1985-04-12t23:20:50.52z" = parse "1985-04-12T23:20:50.52Z" ∧ parse "1985-04-12 23:20:50.52Z" = none ∧ parse "1985-04-12T23:20:50.Z" = none ∧ diff --git a/Proofs/Valid.lean b/Rfc3339/Proofs/Valid.lean similarity index 65% rename from Proofs/Valid.lean rename to Rfc3339/Proofs/Valid.lean index 6bbba4a..96015b9 100644 --- a/Proofs/Valid.lean +++ b/Rfc3339/Proofs/Valid.lean @@ -1,12 +1,12 @@ /- - `Timestamp.isValid` decides exactly `Spec.Valid`. The hard part is + `Timestamp.isValid` decides exactly `Rfc3339.Spec.Valid`. The hard part is the leap second rule: the code's check on the local date and time agrees with the spec's rule that the UTC minute is the last one before a month begins. -/ import Rfc3339 -import Spec.Defs +import Rfc3339.Spec.Defs namespace Rfc3339.Proofs.Valid @@ -14,20 +14,20 @@ open Rfc3339 /-! ## Small facts: the code's helpers agree with the spec's -/ -theorem isLeapYear_eq (y : Nat) : isLeapYear y = Spec.isLeapYear y := by - unfold isLeapYear Spec.isLeapYear +theorem isLeapYear_eq (y : Nat) : isLeapYear y = Rfc3339.Spec.isLeapYear y := by + unfold isLeapYear Rfc3339.Spec.isLeapYear by_cases h4 : y % 4 = 0 <;> by_cases h100 : y % 100 = 0 <;> by_cases h400 : y % 400 = 0 <;> simp [h4, h100, h400] -theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := by - unfold daysInMonth Spec.daysInMonth +theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Rfc3339.Spec.daysInMonth y m := by + unfold daysInMonth Rfc3339.Spec.daysInMonth split <;> simp_all [isLeapYear_eq] <;> omega -theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Spec.offsetMinutes o := by - cases o <;> simp [offsetMinutes, Spec.offsetMinutes] +theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Rfc3339.Spec.offsetMinutes o := by + cases o <;> simp [offsetMinutes, Rfc3339.Spec.offsetMinutes] -theorem offset_isValid_iff (o : Offset) : o.isValid = true ↔ Spec.OffsetValid o := by - cases o <;> simp [Offset.isValid, Spec.OffsetValid] +theorem offset_isValid_iff (o : Offset) : o.isValid = true ↔ Rfc3339.Spec.OffsetValid o := by + cases o <;> simp [Offset.isValid, Rfc3339.Spec.OffsetValid] theorem all_lt_iff (l : List Nat) : l.all (· < 10) = true ↔ ∀ d ∈ l, d ≤ 9 := by simp only [List.all_eq_true, decide_eq_true_eq] @@ -54,28 +54,28 @@ theorem sum_range_mono (g : Nat → Nat) (a b : Nat) (h : a ≤ b) : /-! ## Day numbers -/ /-- Days in the years before `y`. -/ -def yearsBefore (y : Nat) : Nat := ((List.range y).map Spec.yearLength).sum +def yearsBefore (y : Nat) : Nat := ((List.range y).map Rfc3339.Spec.yearLength).sum /-- Days in the months before `m` of year `y`. -/ def monthsBefore (y m : Nat) : Nat := - ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum + ((List.range (m - 1)).map fun i => Rfc3339.Spec.daysInMonth y (i + 1)).sum theorem dayNumber_eq (y m d : Nat) : - Spec.dayNumber y m d = yearsBefore y + monthsBefore y m + (d - 1) := rfl + Rfc3339.Spec.dayNumber y m d = yearsBefore y + monthsBefore y m + (d - 1) := rfl theorem dayNumber_day (y m d : Nat) : - Spec.dayNumber y m d = Spec.dayNumber y m 1 + (d - 1) := by + Rfc3339.Spec.dayNumber y m d = Rfc3339.Spec.dayNumber y m 1 + (d - 1) := by simp only [dayNumber_eq]; omega -theorem yearsBefore_succ (y : Nat) : yearsBefore (y + 1) = yearsBefore y + Spec.yearLength y := by +theorem yearsBefore_succ (y : Nat) : yearsBefore (y + 1) = yearsBefore y + Rfc3339.Spec.yearLength y := by unfold yearsBefore; rw [sum_range_succ] theorem yearsBefore_mono {y y' : Nat} (h : y < y') : - yearsBefore y + Spec.yearLength y ≤ yearsBefore y' := by + yearsBefore y + Rfc3339.Spec.yearLength y ≤ yearsBefore y' := by rw [← yearsBefore_succ]; exact sum_range_mono _ _ _ h theorem monthsBefore_succ (y m : Nat) (hm : 1 ≤ m) : - monthsBefore y (m + 1) = monthsBefore y m + Spec.daysInMonth y m := by + monthsBefore y (m + 1) = monthsBefore y m + Rfc3339.Spec.daysInMonth y m := by unfold monthsBefore obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hm simp only [Nat.add_sub_cancel, Nat.add_comm 1 k] @@ -85,13 +85,13 @@ theorem monthsBefore_mono (y : Nat) {m m' : Nat} (h : m ≤ m') : monthsBefore y m ≤ monthsBefore y m' := sum_range_mono _ _ _ (by omega) -theorem monthsBefore_twelve (y : Nat) : monthsBefore y 12 + 31 = Spec.yearLength y := by - cases h : Spec.isLeapYear y <;> - simp [monthsBefore, List.range_succ, Spec.daysInMonth, Spec.yearLength, h] +theorem monthsBefore_twelve (y : Nat) : monthsBefore y 12 + 31 = Rfc3339.Spec.yearLength y := by + cases h : Rfc3339.Spec.isLeapYear y <;> + simp [monthsBefore, List.range_succ, Rfc3339.Spec.daysInMonth, Rfc3339.Spec.yearLength, h] theorem daysInMonth_bounds (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : - 28 ≤ Spec.daysInMonth y m ∧ Spec.daysInMonth y m ≤ 31 := by - unfold Spec.daysInMonth + 28 ≤ Rfc3339.Spec.daysInMonth y m ∧ Rfc3339.Spec.daysInMonth y m ≤ 31 := by + unfold Rfc3339.Spec.daysInMonth split · split <;> omega · split @@ -100,28 +100,28 @@ theorem daysInMonth_bounds (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : /-- A month ends within its year. -/ theorem month_end_le (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) : - monthsBefore y m + Spec.daysInMonth y m ≤ Spec.yearLength y := by + monthsBefore y m + Rfc3339.Spec.daysInMonth y m ≤ Rfc3339.Spec.yearLength y := by rw [← monthsBefore_succ y m h1, ← monthsBefore_twelve] have := monthsBefore_mono y (show m + 1 ≤ 13 by omega) rw [show 13 = 12 + 1 from rfl, monthsBefore_succ y 12 (by decide)] at this - have h12 : Spec.daysInMonth y 12 = 31 := by simp [Spec.daysInMonth] + have h12 : Rfc3339.Spec.daysInMonth y 12 = 31 := by simp [Rfc3339.Spec.daysInMonth] omega /-- The day after the last day of month `m` is the first of month `m + 1` (for `m < 12`, the next month). -/ theorem next_month (y m : Nat) (h1 : 1 ≤ m) : - Spec.dayNumber y m 1 + Spec.daysInMonth y m = Spec.dayNumber y (m + 1) 1 := by + Rfc3339.Spec.dayNumber y m 1 + Rfc3339.Spec.daysInMonth y m = Rfc3339.Spec.dayNumber y (m + 1) 1 := by simp only [dayNumber_eq, monthsBefore_succ y m h1]; omega theorem next_year (y : Nat) : - Spec.dayNumber y 12 1 + 31 = Spec.dayNumber (y + 1) 1 1 := by + Rfc3339.Spec.dayNumber y 12 1 + 31 = Rfc3339.Spec.dayNumber (y + 1) 1 1 := by simp only [dayNumber_eq, yearsBefore_succ, ← monthsBefore_twelve y] simp [monthsBefore]; omega /-- No month starts strictly inside another month. -/ theorem month_start_spaced {y m y' m' : Nat} (h1 : 1 ≤ m) (h2 : m ≤ 12) (h1' : 1 ≤ m') - (h2' : m' ≤ 12) (hlt : Spec.dayNumber y m 1 < Spec.dayNumber y' m' 1) : - Spec.dayNumber y m 1 + Spec.daysInMonth y m ≤ Spec.dayNumber y' m' 1 := by + (h2' : m' ≤ 12) (hlt : Rfc3339.Spec.dayNumber y m 1 < Rfc3339.Spec.dayNumber y' m' 1) : + Rfc3339.Spec.dayNumber y m 1 + Rfc3339.Spec.daysInMonth y m ≤ Rfc3339.Spec.dayNumber y' m' 1 := by simp only [dayNumber_eq] at * rcases Nat.lt_trichotomy y y' with hy | rfl | hy · have := yearsBefore_mono hy @@ -143,14 +143,14 @@ theorem month_start_spaced {y m y' m' : Nat} (h1 : 1 ≤ m) (h2 : m ≤ 12) (h1' /-- With the other fields in range, the code's leap second check is the spec's rule: the UTC minute is the last one before a month begins. -/ theorem leapSecondOK_iff (t : Timestamp) (hm1 : 1 ≤ t.month) (hm2 : t.month ≤ 12) - (hd1 : 1 ≤ t.day) (hd2 : t.day ≤ Spec.daysInMonth t.year t.month) - (hh : t.hour ≤ 23) (hmi : t.minute ≤ 59) (ho : Spec.OffsetValid t.offset) : - leapSecondOK t = true ↔ Spec.LeapSecondAllowed t := by + (hd1 : 1 ≤ t.day) (hd2 : t.day ≤ Rfc3339.Spec.daysInMonth t.year t.month) + (hh : t.hour ≤ 23) (hmi : t.minute ≤ 59) (ho : Rfc3339.Spec.OffsetValid t.offset) : + leapSecondOK t = true ↔ Rfc3339.Spec.LeapSecondAllowed t := by obtain ⟨y, m, d, h, mi, s, f, o⟩ := t simp only at * - have hob : -1439 ≤ Spec.offsetMinutes o ∧ Spec.offsetMinutes o ≤ 1439 := by - cases o <;> simp [Spec.offsetMinutes, Spec.OffsetValid] at ho ⊢ <;> omega - simp only [leapSecondOK, Spec.LeapSecondAllowed, Spec.utcMinute, Bool.or_eq_true, + have hob : -1439 ≤ Rfc3339.Spec.offsetMinutes o ∧ Rfc3339.Spec.offsetMinutes o ≤ 1439 := by + cases o <;> simp [Rfc3339.Spec.offsetMinutes, Rfc3339.Spec.OffsetValid] at ho ⊢ <;> omega + simp only [leapSecondOK, Rfc3339.Spec.LeapSecondAllowed, Rfc3339.Spec.utcMinute, Bool.or_eq_true, Bool.and_eq_true, beq_iff_eq, daysInMonth_eq, offsetMinutes_eq] have hN := dayNumber_day y m d have hdim := daysInMonth_bounds y m hm1 hm2 @@ -164,7 +164,7 @@ theorem leapSecondOK_iff (t : Timestamp) (hm1 : 1 ≤ t.month) (hm2 : t.month subst hm12 refine ⟨y + 1, 1, by omega, by omega, ?_⟩ have := next_year y - have : Spec.daysInMonth y 12 = 31 := by simp [Spec.daysInMonth] + have : Rfc3339.Spec.daysInMonth y 12 = 31 := by simp [Rfc3339.Spec.daysInMonth] omega · exact ⟨y, m, hm1, hm2, by omega⟩ · rintro ⟨y', m', h1', h2', heq⟩ @@ -173,8 +173,8 @@ theorem leapSecondOK_iff (t : Timestamp) (hm1 : 1 ≤ t.month) (hm2 : t.month /-! ## Validity -/ -theorem isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := by - simp only [Timestamp.isValid, Spec.Valid, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq, +theorem isValid_iff (t : Timestamp) : t.isValid = true ↔ Rfc3339.Spec.Valid t := by + simp only [Timestamp.isValid, Rfc3339.Spec.Valid, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq, bne_iff_ne, ne_eq, daysInMonth_eq, all_lt_iff, offset_isValid_iff] constructor · rintro ⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨hy, hm1⟩, hm2⟩, hd1⟩, hd2⟩, hh⟩, hmi⟩, hs⟩, hleap⟩, hf⟩, ho⟩ diff --git a/Spec.lean b/Rfc3339/Spec.lean similarity index 74% rename from Spec.lean rename to Rfc3339/Spec.lean index 8d53160..edd847a 100644 --- a/Spec.lean +++ b/Rfc3339/Spec.lean @@ -2,7 +2,7 @@ The specification as Lean statements: the challenge file. A reviewer who did not write this file approves it, and `bar.toml` - records the hash it had then. The proofs live in `Proofs.lean`, under + records the hash it had then. The proofs live in `Rfc3339/Proofs.lean`, under the same names; `lake comparator` checks that each one proves exactly the statement written here. The `sorry`s below are expected in this file only. @@ -13,68 +13,68 @@ -/ import Rfc3339 -import Spec.Defs -import Spec.Leap -import Spec.Ixdtf +import Rfc3339.Spec.Defs +import Rfc3339.Spec.Leap +import Rfc3339.Spec.Ixdtf open Rfc3339 /-! ## Validity -/ -/-- `isValid` decides exactly `Spec.Valid`: the rules of sections 5.6 +/-- `isValid` decides exactly `Rfc3339.Spec.Valid`: the rules of sections 5.6 and 5.7, except that second 60 is allowed at the end of every month in UTC, since no table of the months that had a leap second is kept. -/ -theorem Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Spec.Valid t := sorry +theorem Rfc3339.Spec.isValid_iff (t : Timestamp) : t.isValid = true ↔ Rfc3339.Spec.Valid t := sorry /-! ## Printing -/ /-- A valid timestamp prints as the grammar of section 5.6 writes it, with `T` and `Z` in upper case. -/ -theorem Spec.print_eq (t : Timestamp) (h : Spec.Valid t) : - t.print.toList = Spec.render t := sorry +theorem Rfc3339.Spec.print_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.print.toList = Rfc3339.Spec.render t := sorry /-! ## Parsing -/ /-- `parse` returns `t` exactly when `t` is valid and the string is how `t` is written, with `T` and `Z` in either case. So it accepts - nothing outside the grammar of section 5.6 and `Spec.Valid`, rejects + nothing outside the grammar of section 5.6 and `Rfc3339.Spec.Valid`, rejects nothing inside them, and returns the fields as written. -/ -theorem Spec.parse_iff (s : String) (t : Timestamp) : - parse s = some t ↔ Spec.Valid t ∧ s.toList.map Spec.asciiUpper = Spec.render t := sorry +theorem Rfc3339.Spec.parse_iff (s : String) (t : Timestamp) : + parse s = some t ↔ Rfc3339.Spec.Valid t ∧ s.toList.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render t := sorry /-- What `parse` returns is valid: among other things, the day exists in its month, so 30 February never passes. -/ -theorem Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : - Spec.Valid t := sorry +theorem Rfc3339.Spec.parse_valid (s : String) (t : Timestamp) (h : parse s = some t) : + Rfc3339.Spec.Valid t := sorry /-- Round trip: printing a valid timestamp and parsing the result gives it back. -/ -theorem Spec.parse_print (t : Timestamp) (h : Spec.Valid t) : parse t.print = some t := sorry +theorem Rfc3339.Spec.parse_print (t : Timestamp) (h : Rfc3339.Spec.Valid t) : parse t.print = some t := sorry /-- Round trip: parsing a string and printing the result gives the string back, with `T` and `Z` in upper case. -/ -theorem Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : - t.print.toList = s.toList.map Spec.asciiUpper := sorry +theorem Rfc3339.Spec.print_parse (s : String) (t : Timestamp) (h : parse s = some t) : + t.print.toList = s.toList.map Rfc3339.Spec.asciiUpper := sorry /-! ## Instants -/ /-- `unixSeconds` counts the whole seconds from 1970-01-01T00:00:00Z, by the calendar of section 5.7, with the offset applied. -/ -theorem Spec.unixSeconds_eq (t : Timestamp) (h : Spec.Valid t) : - t.unixSeconds = Spec.unixSeconds t := sorry +theorem Rfc3339.Spec.unixSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.unixSeconds = Rfc3339.Spec.unixSeconds t := sorry /-- `compareInstant` orders two timestamps by the instants they name, whatever their offsets: by UTC minute, then by the second within it, where a leap second comes after 59, then by the fraction. -/ -theorem Spec.compareInstant_eq (a b : Timestamp) (ha : Spec.Valid a) (hb : Spec.Valid b) : - a.compareInstant b = Spec.compareInstants a b := sorry +theorem Rfc3339.Spec.compareInstant_eq (a b : Timestamp) (ha : Rfc3339.Spec.Valid a) (hb : Rfc3339.Spec.Valid b) : + a.compareInstant b = Rfc3339.Spec.compareInstants a b := sorry /-! ## Test vectors -/ /-- The examples of section 5.8, with the fields the RFC reads them as. -/ -theorem Spec.rfc3339_examples : +theorem Rfc3339.Spec.rfc3339_examples : parse "1985-04-12T23:20:50.52Z" = some ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ ∧ parse "1996-12-19T16:39:57-08:00" = some ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ∧ parse "1990-12-31T23:59:60Z" = some ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ ∧ @@ -86,7 +86,7 @@ theorem Spec.rfc3339_examples : to 1996-12-20T00:39:57Z", and the fourth is "the same leap second" as the third. And a count worked out apart from the RFC, by Python's `calendar.timegm`: the first is 482196050 seconds after the epoch. -/ -theorem Spec.rfc3339_example_instants : +theorem Rfc3339.Spec.rfc3339_example_instants : (Timestamp.compareInstant ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ ⟨1996, 12, 20, 0, 39, 57, [], .z⟩ = .eq) ∧ (Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ @@ -96,7 +96,7 @@ theorem Spec.rfc3339_example_instants : /-- A leap second comes after second 59 of its minute and before the next minute, fraction included. Unix seconds, as in POSIX time, give it the same count as the second after it. -/ -theorem Spec.leap_second_order : +theorem Rfc3339.Spec.leap_second_order : Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 59, [9], .z⟩ ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = .lt ∧ Timestamp.compareInstant ⟨1990, 12, 31, 23, 59, 60, [5], .z⟩ @@ -107,7 +107,7 @@ theorem Spec.leap_second_order : Timestamp.unixSeconds ⟨1991, 1, 1, 0, 0, 0, [], .z⟩ := sorry /-- Days outside their month, and the leap year rule of Appendix C. -/ -theorem Spec.calendar_vectors : +theorem Rfc3339.Spec.calendar_vectors : (parse "2000-02-29T00:00:00Z").isSome ∧ (parse "2004-02-29T00:00:00Z").isSome ∧ parse "1900-02-29T00:00:00Z" = none ∧ @@ -120,7 +120,7 @@ theorem Spec.calendar_vectors : parse "2001-13-01T00:00:00Z" = none := sorry /-- Second 60 only at the end of a month in UTC. -/ -theorem Spec.leap_second_vectors : +theorem Rfc3339.Spec.leap_second_vectors : (parse "1990-06-30T23:59:60Z").isSome ∧ (parse "1991-01-01T00:59:60+01:00").isSome ∧ parse "1990-12-31T23:59:61Z" = none ∧ @@ -129,7 +129,7 @@ theorem Spec.leap_second_vectors : parse "1990-12-31T23:59:60+01:00" = none := sorry /-- Lower case `t` and `z` are read; other spellings are not. -/ -theorem Spec.syntax_vectors : +theorem Rfc3339.Spec.syntax_vectors : parse "1985-04-12t23:20:50.52z" = parse "1985-04-12T23:20:50.52Z" ∧ parse "1985-04-12 23:20:50.52Z" = none ∧ parse "1985-04-12T23:20:50.Z" = none ∧ @@ -149,32 +149,32 @@ theorem Spec.syntax_vectors : UTC (offset `Z`), with no fraction and no leap second, and that names the second `s`. There is at most one; the next statement says for which `s` there is one. -/ -theorem Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : +theorem Rfc3339.Spec.fromUnixSeconds_iff (s : Int) (t : Timestamp) : Rfc3339.fromUnixSeconds s = some t ↔ - Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧ - Spec.unixSeconds t = s := sorry + Rfc3339.Spec.Valid t ∧ t.offset = .z ∧ t.fraction = [] ∧ t.second ≤ 59 ∧ + Rfc3339.Spec.unixSeconds t = s := sorry /-- It gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, the years RFC 3339 allows. -/ -theorem Spec.fromUnixSeconds_isSome (s : Int) : +theorem Rfc3339.Spec.fromUnixSeconds_isSome (s : Int) : (Rfc3339.fromUnixSeconds s).isSome ↔ - Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧ - s ≤ Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry + Rfc3339.Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧ + s ≤ Rfc3339.Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry /-- 0096-12-31 at midnight, from the year-start grid; the epoch; the example of section 5.8; a leap day; the last second a signed 32-bit count reaches; the second before the epoch; the ends of the range, and one second past each. -/ -theorem Spec.fromUnixSeconds_vectors : +theorem Rfc3339.Spec.fromUnixSeconds_vectors : Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 2147483647 = some ⟨2038, 1, 19, 3, 14, 7, [], .z⟩ ∧ Rfc3339.fromUnixSeconds (-1) = some ⟨1969, 12, 31, 23, 59, 59, [], .z⟩ ∧ - Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 ∧ - Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 ∧ + Rfc3339.Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ = -62167219200 ∧ + Rfc3339.Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ = 253402300799 ∧ Rfc3339.fromUnixSeconds (-62167219200) = some ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ∧ Rfc3339.fromUnixSeconds 253402300799 = some ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ ∧ Rfc3339.fromUnixSeconds (-62167219201) = none ∧ @@ -185,21 +185,21 @@ theorem Spec.fromUnixSeconds_vectors : /-- `isValidKnown` decides section 5.7 with the table of leap seconds: as `isValid`, but second 60 only at one of the table's leap seconds, at the same instant whatever the offset. -/ -theorem Spec.isValidKnown_iff (t : Timestamp) : - t.isValidKnown = true ↔ Spec.ValidKnown t := sorry +theorem Rfc3339.Spec.isValidKnown_iff (t : Timestamp) : + t.isValidKnown = true ↔ Rfc3339.Spec.ValidKnown t := sorry /-- `siSeconds` is the Unix seconds from 1972-01-01T00:00:00Z to the timestamp, leaving out the fraction, and one more for each leap second of the table before it. From 1972 on, those are the SI seconds between them; before 1972 there are no leap seconds, and the number is Unix seconds, 86400 to a day, not SI seconds. -/ -theorem Spec.siSeconds_eq (t : Timestamp) (h : Spec.Valid t) : - t.siSeconds = Spec.siSeconds t := sorry +theorem Rfc3339.Spec.siSeconds_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.siSeconds = Rfc3339.Spec.siSeconds t := sorry /-- On whole seconds, valid by the table, `siSeconds` orders timestamps exactly as the instants they name. So no two instants share a number, a leap second and the second after it included. -/ -theorem Spec.siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Spec.ValidKnown b) +theorem Rfc3339.Spec.siSeconds_order (a b : Timestamp) (ha : Rfc3339.Spec.ValidKnown a) (hb : Rfc3339.Spec.ValidKnown b) (fa : a.fraction = []) (fb : b.fraction = []) : compare a.siSeconds b.siSeconds = a.compareInstant b := sorry @@ -207,36 +207,36 @@ theorem Spec.siSeconds_order (a b : Timestamp) (ha : Spec.ValidKnown a) (hb : Sp a timestamp: the one, at most one, in UTC, with no fraction, valid by the table and from 1972 on, that has those SI seconds. A leap second comes back as second 60. -/ -theorem Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : +theorem Rfc3339.Spec.fromSiSeconds_iff (n : Int) (t : Timestamp) : fromSiSeconds n = some t ↔ - t.offset = .z ∧ t.fraction = [] ∧ Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ - Spec.siSeconds t = n := sorry + t.offset = .z ∧ t.fraction = [] ∧ Rfc3339.Spec.ValidKnown t ∧ 1972 ≤ t.year ∧ + Rfc3339.Spec.siSeconds t = n := sorry /-- `fromSiSeconds` gives a timestamp exactly for the seconds from 1972-01-01T00:00:00Z to 9999-12-31T23:59:59Z. -/ -theorem Spec.fromSiSeconds_isSome (n : Int) : +theorem Rfc3339.Spec.fromSiSeconds_isSome (n : Int) : (fromSiSeconds n).isSome ↔ - 0 ≤ n ∧ n ≤ Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry + 0 ≤ n ∧ n ≤ Rfc3339.Spec.siSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry /-- `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. (Before 1972, UTC was not a whole number of seconds from TAI, and the 10 there means nothing.) -/ -theorem Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Spec.Valid t) : - t.taiMinusUtc = 10 + Spec.leapsBefore t := sorry +theorem Rfc3339.Spec.taiMinusUtc_leapsBefore (t : Timestamp) (h : Rfc3339.Spec.Valid t) : + t.taiMinusUtc = 10 + Rfc3339.Spec.leapsBefore t := sorry /-- TAI − UTC at each second from 1972 on, other than a leap second, is the value the table's second column gives for it. The code never reads that column: it counts leap seconds. -/ -theorem Spec.taiMinusUtc_eq (t : Timestamp) (h : Spec.Valid t) (h60 : t.second ≠ 60) - (h72 : Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Spec.unixSeconds t) : - t.taiMinusUtc = Spec.taiMinusUtcAt (Spec.ntpOfUnix (Spec.unixSeconds t)) := sorry +theorem Rfc3339.Spec.taiMinusUtc_eq (t : Timestamp) (h : Rfc3339.Spec.Valid t) (h60 : t.second ≠ 60) + (h72 : Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ ≤ Rfc3339.Spec.unixSeconds t) : + t.taiMinusUtc = Rfc3339.Spec.taiMinusUtcAt (Rfc3339.Spec.ntpOfUnix (Rfc3339.Spec.unixSeconds t)) := sorry /-- The leap seconds of section 5.8, the first and the last of the table, one seen from another offset, and second 60 in months that had none; SI seconds and TAI − UTC around the first and the last; and the round trip that Unix seconds lose and SI seconds keep. -/ -theorem Spec.leap_table_vectors : +theorem Rfc3339.Spec.leap_table_vectors : Timestamp.isValidKnown ⟨1990, 12, 31, 23, 59, 60, [], .z⟩ = true ∧ Timestamp.isValidKnown ⟨1990, 12, 31, 15, 59, 60, [], .minus 8 0⟩ = true ∧ Timestamp.isValidKnown ⟨1972, 6, 30, 23, 59, 60, [], .z⟩ = true ∧ @@ -272,40 +272,40 @@ theorem Spec.leap_table_vectors : 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) : +theorem Rfc3339.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 + Rfc3339.Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Rfc3339.Spec.renderSuffix e ∧ + dt.map Rfc3339.Spec.asciiUpper = Rfc3339.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 +theorem Rfc3339.Spec.printExt_eq (e : Ext) (h : Rfc3339.Spec.ExtValid e) : + e.print.toList = Rfc3339.Spec.render e.stamp ++ Rfc3339.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 +theorem Rfc3339.Spec.parseExt_print (e : Ext) (h : Rfc3339.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) : +theorem Rfc3339.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) : +theorem Rfc3339.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 +theorem Rfc3339.Spec.erroneous_iff (p : Processor) (e : Ext) : + e.erroneous p = true ↔ Rfc3339.Spec.MustReject p e := sorry /-- Every example of RFC 9557, in sections 1.2, 3.3, 3.4 and 4.2, with - the application of `Spec.exampleProcessor`: each one is read, and is + the application of `Rfc3339.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 : +theorem Rfc3339.Spec.ixdtf_vectors : -- Section 4.2, Figures 4 to 7 parseExt "1996-12-19T16:39:57-08:00" = some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, []⟩ ∧ @@ -320,58 +320,58 @@ theorem Spec.ixdtf_vectors : some ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, none, [⟨false, "_foo".toList, ["bar".toList]⟩, ⟨false, "_baz".toList, ["bat".toList]⟩]⟩ ∧ ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "1996-12-19T16:39:57-08:00[America/Los_Angeles][u-ca=hebrew]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.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) ∧ + (·.erroneous Rfc3339.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) = + ((parseExt "2022-07-08T00:14:07+08:45[!+08:45]").map (·.erroneous Rfc3339.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) = + ((parseExt "2022-07-08T00:14:07+01:00[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T02:14:07+02:00[Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+01:00[knort=blargel]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese][u-ca=japanese]").bind (·.lookup "u-ca".toList) = some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ ((parseExt "2022-07-08T00:14:07Z[u-ca=chinese]").bind (·.lookup "u-ca".toList) = some ⟨false, "u-ca".toList, ["chinese".toList]⟩) ∧ -- Section 3.3, critical: the four examples - ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+01:00[!Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ ((parseExt "2022-07-08T00:14:07Z[!u-ca=chinese][u-ca=japanese]").map - (·.erroneous Spec.exampleProcessor) = some true) ∧ + (·.erroneous Rfc3339.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) = + (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ + ((parseExt "2022-07-08T00:14:07Z[!knort=blargel]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ -- Section 3.4, Figures 1 and 2 - ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+00:00[!Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some true) ∧ - ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07+00:00[Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[!Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T00:14:07Z[Europe/London]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ -- Critical zones that agree with the offset, and a critical `-00:00` -- zone, offset 0, under an offset of +01:00 ((parseExt "1996-12-19T16:39:57-08:00[!America/Los_Angeles]").map - (·.erroneous Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Spec.exampleProcessor) = + (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ + ((parseExt "2022-07-08T02:14:07+02:00[!Europe/Paris]").map (·.erroneous Rfc3339.Spec.exampleProcessor) = some false) ∧ - ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Spec.exampleProcessor) = + ((parseExt "2022-07-08T01:14:07+01:00[!-00:00]").map (·.erroneous Rfc3339.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]))) ∧ diff --git a/Spec/Defs.lean b/Rfc3339/Spec/Defs.lean similarity index 57% rename from Spec/Defs.lean rename to Rfc3339/Spec/Defs.lean index 7720bfe..3273d0f 100644 --- a/Spec/Defs.lean +++ b/Rfc3339/Spec/Defs.lean @@ -1,7 +1,7 @@ /- The definitions the specification uses, written from RFC 3339 independently of the code in `Rfc3339/`. Part of the approved - specification, with `Spec.lean` and `Rfc3339/Types.lean`. + specification, with `Rfc3339/Spec.lean` and `Rfc3339/Types.lean`. Both the challenge file and the proofs import this file, so each statement means the same thing on both sides. The `example`s check @@ -17,22 +17,22 @@ open Rfc3339 /-- ASCII upper case: `a` to `z` (code points 97 to 122) become `A` to `Z`; nothing else changes. -/ -def Spec.asciiUpper (c : Char) : Char := +def Rfc3339.Spec.asciiUpper (c : Char) : Char := if 97 ≤ c.toNat ∧ c.toNat ≤ 122 then Char.ofNat (c.toNat - 32) else c -example : "azAZ09-:.+tz".toList.map Spec.asciiUpper = "AZAZ09-:.+TZ".toList := by decide +example : "azAZ09-:.+tz".toList.map Rfc3339.Spec.asciiUpper = "AZAZ09-:.+TZ".toList := by decide /-- The decimal digit for `n`, for `n` from 0 to 9. -/ -def Spec.digitChar (n : Nat) : Char := "0123456789".toList.getD n '?' +def Rfc3339.Spec.digitChar (n : Nat) : Char := "0123456789".toList.getD n '?' /-- The last `k` decimal digits of `n`, most significant first, with leading zeros. -/ -def Spec.digits (k n : Nat) : List Char := - (List.range k).reverse.map fun i => Spec.digitChar (n / 10 ^ i % 10) +def Rfc3339.Spec.digits (k n : Nat) : List Char := + (List.range k).reverse.map fun i => Rfc3339.Spec.digitChar (n / 10 ^ i % 10) -example : Spec.digits 4 1985 = "1985".toList := by decide -example : Spec.digits 4 7 = "0007".toList := by decide -example : Spec.digits 2 9 = "09".toList := by decide +example : Rfc3339.Spec.digits 4 1985 = "1985".toList := by decide +example : Rfc3339.Spec.digits 4 7 = "0007".toList := by decide +example : Rfc3339.Spec.digits 2 9 = "09".toList := by decide /-! ## The format: RFC 3339, section 5.6 @@ -58,86 +58,86 @@ date-time = full-date "T" full-time ``` The note under the grammar lets `T` and `Z` be written in lower case -too. `render` writes them in upper case; `Spec.parse_iff` in -`Spec.lean` says how the parser treats the lower case forms. -/ +too. `render` writes them in upper case; `Rfc3339.Spec.parse_iff` in +`Rfc3339/Spec.lean` says how the parser treats the lower case forms. -/ /-- `time-offset`. -/ -def Spec.renderOffset : Offset → List Char +def Rfc3339.Spec.renderOffset : Offset → List Char | .z => ['Z'] - | .plus h m => ['+'] ++ Spec.digits 2 h ++ [':'] ++ Spec.digits 2 m - | .minus h m => ['-'] ++ Spec.digits 2 h ++ [':'] ++ Spec.digits 2 m + | .plus h m => ['+'] ++ Rfc3339.Spec.digits 2 h ++ [':'] ++ Rfc3339.Spec.digits 2 m + | .minus h m => ['-'] ++ Rfc3339.Spec.digits 2 h ++ [':'] ++ Rfc3339.Spec.digits 2 m /-- `date-time`, with `T` and `Z` in upper case. The fraction is written when there is at least one digit. -/ -def Spec.render (t : Timestamp) : List Char := - Spec.digits 4 t.year ++ ['-'] ++ Spec.digits 2 t.month ++ ['-'] ++ Spec.digits 2 t.day ++ - ['T'] ++ Spec.digits 2 t.hour ++ [':'] ++ Spec.digits 2 t.minute ++ [':'] ++ - Spec.digits 2 t.second ++ - (if t.fraction = [] then [] else ['.'] ++ t.fraction.map Spec.digitChar) ++ - Spec.renderOffset t.offset - -example : Spec.render ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = +def Rfc3339.Spec.render (t : Timestamp) : List Char := + Rfc3339.Spec.digits 4 t.year ++ ['-'] ++ Rfc3339.Spec.digits 2 t.month ++ ['-'] ++ Rfc3339.Spec.digits 2 t.day ++ + ['T'] ++ Rfc3339.Spec.digits 2 t.hour ++ [':'] ++ Rfc3339.Spec.digits 2 t.minute ++ [':'] ++ + Rfc3339.Spec.digits 2 t.second ++ + (if t.fraction = [] then [] else ['.'] ++ t.fraction.map Rfc3339.Spec.digitChar) ++ + Rfc3339.Spec.renderOffset t.offset + +example : Rfc3339.Spec.render ⟨1985, 4, 12, 23, 20, 50, [5, 2], .z⟩ = "1985-04-12T23:20:50.52Z".toList := by decide -example : Spec.render ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ = +example : Rfc3339.Spec.render ⟨1937, 1, 1, 12, 0, 27, [8, 7], .plus 0 20⟩ = "1937-01-01T12:00:27.87+00:20".toList := by decide -example : Spec.render ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ = +example : Rfc3339.Spec.render ⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩ = "1996-12-19T16:39:57-08:00".toList := by decide /-! ## The calendar: RFC 3339, section 5.7 and Appendix C -/ /-- Appendix C: a year divisible by 4 is a leap year, except one divisible by 100, except one divisible by 400. -/ -def Spec.isLeapYear (y : Nat) : Bool := +def Rfc3339.Spec.isLeapYear (y : Nat) : Bool := decide (y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0)) -example : [1900, 1996, 1997, 2000, 2100, 2400, 0].map Spec.isLeapYear = +example : [1900, 1996, 1997, 2000, 2100, 2400, 0].map Rfc3339.Spec.isLeapYear = [false, true, false, true, false, true, true] := by decide /-- Section 5.7, the maximum value of `date-mday` for month `m` of year `y`; 0 when `m` is not a month. -/ -def Spec.daysInMonth (y m : Nat) : Nat := - if m = 2 then (if Spec.isLeapYear y then 29 else 28) +def Rfc3339.Spec.daysInMonth (y m : Nat) : Nat := + if m = 2 then (if Rfc3339.Spec.isLeapYear y then 29 else 28) else if m = 4 ∨ m = 6 ∨ m = 9 ∨ m = 11 then 30 else if 1 ≤ m ∧ m ≤ 12 then 31 else 0 -- The table of section 5.7, month by month, for a common year and a -- leap year. -example : (List.range 14).map (Spec.daysInMonth 2001) = +example : (List.range 14).map (Rfc3339.Spec.daysInMonth 2001) = [0, 31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31, 0] := by decide -example : (List.range 14).map (Spec.daysInMonth 2004) = +example : (List.range 14).map (Rfc3339.Spec.daysInMonth 2004) = [0, 31, 29, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31, 0] := by decide -def Spec.yearLength (y : Nat) : Nat := if Spec.isLeapYear y then 366 else 365 +def Rfc3339.Spec.yearLength (y : Nat) : Nat := if Rfc3339.Spec.isLeapYear y then 366 else 365 /-- The number of days from 0000-01-01 to the date `y`-`m`-`d`, in the Gregorian calendar extended back to year 0, which RFC 3339 uses (section 5.7 and Appendix C): the lengths of the years before `y`, then of the months before `m` in year `y`, then the days before `d`. -/ -def Spec.dayNumber (y m d : Nat) : Nat := - ((List.range y).map Spec.yearLength).sum + - ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum + (d - 1) +def Rfc3339.Spec.dayNumber (y m d : Nat) : Nat := + ((List.range y).map Rfc3339.Spec.yearLength).sum + + ((List.range (m - 1)).map fun i => Rfc3339.Spec.daysInMonth y (i + 1)).sum + (d - 1) -- Known counts: 1970-01-01 is day 719528 (Python's -- `date(1970, 1, 1).toordinal()`, 719163, counts from 0001-01-01 as day -- 1, and year 0 is a leap year of 366 days), and 2000-03-01 is 11017 -- days later. -example : Spec.dayNumber 0 1 1 = 0 := by decide -example : Spec.dayNumber 1 1 1 = 366 := by decide -example : Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel -example : Spec.dayNumber 2000 3 1 = 719528 + 11017 := by decide +kernel +example : Rfc3339.Spec.dayNumber 0 1 1 = 0 := by decide +example : Rfc3339.Spec.dayNumber 1 1 1 = 366 := by decide +example : Rfc3339.Spec.dayNumber 1970 1 1 = 719528 := by decide +kernel +example : Rfc3339.Spec.dayNumber 2000 3 1 = 719528 + 11017 := by decide +kernel /-! ## Validity -/ /-- `time-numoffset`: hours 00 to 23 and minutes 00 to 59. -/ -def Spec.OffsetValid : Offset → Prop +def Rfc3339.Spec.OffsetValid : Offset → Prop | .z => True | .plus h m => h ≤ 23 ∧ m ≤ 59 | .minus h m => h ≤ 23 ∧ m ≤ 59 /-- The offset in minutes: local time minus UTC. -/ -def Spec.offsetMinutes : Offset → Int +def Rfc3339.Spec.offsetMinutes : Offset → Int | .z => 0 | .plus h m => (h : Int) * 60 + m | .minus h m => -((h : Int) * 60 + m) @@ -145,9 +145,9 @@ def Spec.offsetMinutes : Offset → Int /-- The minute the timestamp falls in, counted in UTC from 0000-01-01T00:00Z. Local time is UTC plus the offset, so the offset is subtracted. -/ -def Spec.utcMinute (t : Timestamp) : Int := - ((Spec.dayNumber t.year t.month t.day * 1440 + t.hour * 60 + t.minute : Nat) : Int) - - Spec.offsetMinutes t.offset +def Rfc3339.Spec.utcMinute (t : Timestamp) : Int := + ((Rfc3339.Spec.dayNumber t.year t.month t.day * 1440 + t.hour * 60 + t.minute : Nat) : Int) - + Rfc3339.Spec.offsetMinutes t.offset /-- Section 5.7: `time-second` may be 60 "at the end of months in which a leap second occurs", and in other time zones "the leap second point @@ -155,46 +155,46 @@ def Spec.utcMinute (t : Timestamp) : Int := around the globe)". So the minute the leap second falls in, in UTC, is the last one before a month begins. No table of the months that had a leap second is kept, so every month is allowed. -/ -def Spec.LeapSecondAllowed (t : Timestamp) : Prop := - ∃ y m, 1 ≤ m ∧ m ≤ 12 ∧ Spec.utcMinute t + 1 = ((Spec.dayNumber y m 1 * 1440 : Nat) : Int) +def Rfc3339.Spec.LeapSecondAllowed (t : Timestamp) : Prop := + ∃ y m, 1 ≤ m ∧ m ≤ 12 ∧ Rfc3339.Spec.utcMinute t + 1 = ((Rfc3339.Spec.dayNumber y m 1 * 1440 : Nat) : Int) /-- A timestamp RFC 3339 allows: every field in the range section 5.6 gives it, the day within its month (section 5.7), and second 60 only for a leap second. -/ -def Spec.Valid (t : Timestamp) : Prop := +def Rfc3339.Spec.Valid (t : Timestamp) : Prop := t.year ≤ 9999 ∧ 1 ≤ t.month ∧ t.month ≤ 12 ∧ - 1 ≤ t.day ∧ t.day ≤ Spec.daysInMonth t.year t.month ∧ + 1 ≤ t.day ∧ t.day ≤ Rfc3339.Spec.daysInMonth t.year t.month ∧ t.hour ≤ 23 ∧ t.minute ≤ 59 ∧ t.second ≤ 60 ∧ - (t.second = 60 → Spec.LeapSecondAllowed t) ∧ + (t.second = 60 → Rfc3339.Spec.LeapSecondAllowed t) ∧ (∀ d ∈ t.fraction, d ≤ 9) ∧ - Spec.OffsetValid t.offset + Rfc3339.Spec.OffsetValid t.offset /-! ## Instants -/ /-- Whole seconds from 1970-01-01T00:00:00Z to the timestamp. Second 60 counts as 60 seconds into its minute, so a leap second gives the same number as the second after it, as POSIX time does. -/ -def Spec.unixSeconds (t : Timestamp) : Int := - (Spec.utcMinute t - ((Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int)) * 60 + t.second +def Rfc3339.Spec.unixSeconds (t : Timestamp) : Int := + (Rfc3339.Spec.utcMinute t - ((Rfc3339.Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int)) * 60 + t.second /-- The fraction's digits read as a whole number: `[5, 2]` is 52. -/ -def Spec.fractionValue (ds : List Nat) : Nat := +def Rfc3339.Spec.fractionValue (ds : List Nat) : Nat := ds.foldl (fun acc d => 10 * acc + d) 0 -example : Spec.fractionValue [0, 5, 2] = 52 := by decide +example : Rfc3339.Spec.fractionValue [0, 5, 2] = 52 := by decide /-- The place of the timestamp's instant in UTC order, in units of `10 ^ (-k)` seconds, for `k` at least the number of fraction digits. Each UTC minute has 61 places for seconds 0 to 60, so a leap second comes after second 59 of its minute and before the next minute. Only the order of these numbers is used, not their size. -/ -def Spec.instantKey (t : Timestamp) (k : Nat) : Int := - (Spec.utcMinute t * 61 + t.second) * 10 ^ k + - Spec.fractionValue t.fraction * 10 ^ (k - t.fraction.length) +def Rfc3339.Spec.instantKey (t : Timestamp) (k : Nat) : Int := + (Rfc3339.Spec.utcMinute t * 61 + t.second) * 10 ^ k + + Rfc3339.Spec.fractionValue t.fraction * 10 ^ (k - t.fraction.length) /-- The order of the instants two timestamps name: by UTC minute, then by the second within it, then by the fraction, compared exactly. -/ -def Spec.compareInstants (a b : Timestamp) : Ordering := +def Rfc3339.Spec.compareInstants (a b : Timestamp) : Ordering := let k := max a.fraction.length b.fraction.length - compare (Spec.instantKey a k) (Spec.instantKey b k) + compare (Rfc3339.Spec.instantKey a k) (Rfc3339.Spec.instantKey b k) diff --git a/Spec/Ixdtf.lean b/Rfc3339/Spec/Ixdtf.lean similarity index 71% rename from Spec/Ixdtf.lean rename to Rfc3339/Spec/Ixdtf.lean index 8b43732..9fadd2e 100644 --- a/Spec/Ixdtf.lean +++ b/Rfc3339/Spec/Ixdtf.lean @@ -2,10 +2,10 @@ 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`. + `Rfc3339/Spec.lean`, `Spec/Defs.lean` and `Rfc3339/IxdtfTypes.lean`. -/ -import Spec.Defs +import Rfc3339.Spec.Defs import Rfc3339.IxdtfTypes open Rfc3339 @@ -51,63 +51,63 @@ what is written here. -/ /-- `ALPHA`. -/ -def Spec.Alpha (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') +def Rfc3339.Spec.Alpha (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') /-- `DIGIT`. -/ -def Spec.Digit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9' +def Rfc3339.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 = '+') ∧ +def Rfc3339.Spec.ZonePart (p : List Char) : Prop := + ∃ c cs, p = c :: cs ∧ (Rfc3339.Spec.Alpha c ∨ c = '.' ∨ c = '_') ∧ + (∀ d ∈ cs, Rfc3339.Spec.Alpha d ∨ d = '.' ∨ d = '_' ∨ Rfc3339.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 +def Rfc3339.Spec.ZoneValid : Zone → Prop + | .name parts => parts ≠ [] ∧ ∀ p ∈ parts, Rfc3339.Spec.ZonePart p + | .offset o => o ≠ .z ∧ Rfc3339.Spec.OffsetValid o /-- `suffix-key`. -/ -def Spec.SuffixKey (k : List Char) : Prop := +def Rfc3339.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 = '-' + ∀ d ∈ cs, ('a' ≤ d ∧ d ≤ 'z') ∨ d = '_' ∨ Rfc3339.Spec.Digit d ∨ d = '-' /-- `suffix-value`. -/ -def Spec.SuffixValue (v : List Char) : Prop := v ≠ [] ∧ ∀ c ∈ v, Spec.Alpha c ∨ Spec.Digit c +def Rfc3339.Spec.SuffixValue (v : List Char) : Prop := v ≠ [] ∧ ∀ c ∈ v, Rfc3339.Spec.Alpha c ∨ Rfc3339.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 +def Rfc3339.Spec.TagValid (t : Tag) : Prop := + Rfc3339.Spec.SuffixKey t.key ∧ t.values ≠ [] ∧ ∀ v ∈ t.values, Rfc3339.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 +def Rfc3339.Spec.ExtValid (e : Ext) : Prop := + Rfc3339.Spec.Valid e.stamp ∧ (∀ c z, e.zone = some (c, z) → Rfc3339.Spec.ZoneValid z) ∧ + ∀ t ∈ e.tags, Rfc3339.Spec.TagValid t /-- `critical-flag`. -/ -def Spec.renderFlag (c : Bool) : List Char := if c then ['!'] else [] +def Rfc3339.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 +def Rfc3339.Spec.renderZone : Zone → List Char | .name parts => (parts.intersperse ['/']).flatten - | .offset o => Spec.renderOffset o + | .offset o => Rfc3339.Spec.renderOffset o /-- `suffix-tag`. -/ -def Spec.renderTag (t : Tag) : List Char := - ['['] ++ Spec.renderFlag t.critical ++ t.key ++ ['='] ++ (t.values.intersperse ['-']).flatten ++ +def Rfc3339.Spec.renderTag (t : Tag) : List Char := + ['['] ++ Rfc3339.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 := +def Rfc3339.Spec.renderSuffix (e : Ext) : List Char := (match e.zone with - | some (c, z) => ['['] ++ Spec.renderFlag c ++ Spec.renderZone z ++ [']'] + | some (c, z) => ['['] ++ Rfc3339.Spec.renderFlag c ++ Rfc3339.Spec.renderZone z ++ [']'] | none => []) ++ - (e.tags.map Spec.renderTag).flatten + (e.tags.map Rfc3339.Spec.renderTag).flatten -example : Spec.renderSuffix ⟨⟨1996, 12, 19, 16, 39, 57, [], .minus 8 0⟩, +example : Rfc3339.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 @@ -151,24 +151,24 @@ 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 +def Rfc3339.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 +def Rfc3339.Spec.ZoneConsistent (p : Processor) (t : Timestamp) : Zone → Prop + | .offset o => Rfc3339.Spec.AssertsOffset t.offset → Rfc3339.Spec.offsetMinutes o = Rfc3339.Spec.offsetMinutes t.offset | .name parts => ∃ m, p.zoneOffset parts t = some m ∧ - (Spec.AssertsOffset t.offset → m = Spec.offsetMinutes t.offset) + (Rfc3339.Spec.AssertsOffset t.offset → m = Rfc3339.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) ∨ +def Rfc3339.Spec.MustReject (p : Processor) (e : Ext) : Prop := + (∃ z, e.zone = some (true, z) ∧ ¬ Rfc3339.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) @@ -179,7 +179,7 @@ def Spec.MustReject (p : Processor) (e : Ext) : Prop := 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 +def Rfc3339.Spec.exampleProcessor : Processor where processes t := t.key = "u-ca".toList ∧ (t.values = ["chinese".toList] ∨ t.values = ["japanese".toList] ∨ t.values = ["hebrew".toList]) diff --git a/Spec/Leap.lean b/Rfc3339/Spec/Leap.lean similarity index 71% rename from Spec/Leap.lean rename to Rfc3339/Spec/Leap.lean index 85698c8..55e5756 100644 --- a/Spec/Leap.lean +++ b/Rfc3339/Spec/Leap.lean @@ -2,12 +2,12 @@ The definitions the leap second statements use: the table of leap seconds and TAI − UTC as tzdata's `leap-seconds.list` publishes it, from IERS Bulletin C, and section 5.7 of RFC 3339 with that table. - Part of the approved specification, with `Spec.lean` and + Part of the approved specification, with `Rfc3339/Spec.lean` and `Spec/Defs.lean`, and written independently of the code in `Rfc3339/`. -/ -import Spec.Defs +import Rfc3339.Spec.Defs open Rfc3339 @@ -62,7 +62,7 @@ been added to UTC)". -/ /-- The table, line for line: NTP time, and TAI − UTC from then on. -/ -def Spec.leapTable : List (Nat × Nat) := +def Rfc3339.Spec.leapTable : List (Nat × Nat) := [(2272060800, 10), (2287785600, 11), (2303683200, 12), (2335219200, 13), (2366755200, 14), (2398291200, 15), (2429913600, 16), (2461449600, 17), (2492985600, 18), (2524521600, 19), (2571782400, 20), (2603318400, 21), @@ -74,9 +74,9 @@ def Spec.leapTable : List (Nat × Nat) := /-- NTP time from Unix seconds: NTP counts from 1900-01-01T00:00:00Z, 70 years of 86400-second days, 17 of them leap years, before the Unix epoch. -/ -def Spec.ntpOfUnix (u : Int) : Int := u + (70 * 365 + 17) * 86400 +def Rfc3339.Spec.ntpOfUnix (u : Int) : Int := u + (70 * 365 + 17) * 86400 -example : Spec.ntpOfUnix 0 = 2208988800 := by decide +example : Rfc3339.Spec.ntpOfUnix 0 = 2208988800 := by decide /-! ## Section 5.7, with the table @@ -89,41 +89,41 @@ as the start of the next minute, are those of a line after the first. /-- `t` names one of the table's leap seconds: its second is 60, and the time just after it, in NTP time, is that of a line of the table after the first. -/ -def Spec.TableLeapSecond (t : Timestamp) : Prop := - t.second = 60 ∧ ∃ e ∈ Spec.leapTable.tail, Spec.ntpOfUnix (Spec.unixSeconds t) = e.1 +def Rfc3339.Spec.TableLeapSecond (t : Timestamp) : Prop := + t.second = 60 ∧ ∃ e ∈ Rfc3339.Spec.leapTable.tail, Rfc3339.Spec.ntpOfUnix (Rfc3339.Spec.unixSeconds t) = e.1 -/-- Valid, by section 5.7 with the table: as `Spec.Valid`, and second 60 +/-- Valid, by section 5.7 with the table: as `Rfc3339.Spec.Valid`, and second 60 only at a leap second of the table. -/ -def Spec.ValidKnown (t : Timestamp) : Prop := - Spec.Valid t ∧ (t.second = 60 → Spec.TableLeapSecond t) +def Rfc3339.Spec.ValidKnown (t : Timestamp) : Prop := + Rfc3339.Spec.Valid t ∧ (t.second = 60 → Rfc3339.Spec.TableLeapSecond t) /-! ## SI seconds and TAI − UTC -/ /-- The place of a timestamp's whole second in UTC order: its UTC minute - and its second, with 61 places to a minute, as `Spec.instantKey` + and its second, with 61 places to a minute, as `Rfc3339.Spec.instantKey` with no fraction. -/ -def Spec.secondKey (t : Timestamp) : Int := Spec.utcMinute t * 61 + t.second +def Rfc3339.Spec.secondKey (t : Timestamp) : Int := Rfc3339.Spec.utcMinute t * 61 + t.second /-- The same place for the leap second just before NTP time `ntp`: second 60 of the minute before it. -/ -def Spec.leapSecondKey (ntp : Nat) : Int := - (((ntp : Int) - Spec.ntpOfUnix 0) / 60 + ((Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int) - 1) * 61 + 60 +def Rfc3339.Spec.leapSecondKey (ntp : Nat) : Int := + (((ntp : Int) - Rfc3339.Spec.ntpOfUnix 0) / 60 + ((Rfc3339.Spec.dayNumber 1970 1 1 * 1440 : Nat) : Int) - 1) * 61 + 60 /-- How many leap seconds of the table come before the second `t` falls in. -/ -def Spec.leapsBefore (t : Timestamp) : Nat := - (Spec.leapTable.tail.filter fun e => Spec.leapSecondKey e.1 < Spec.secondKey t).length +def Rfc3339.Spec.leapsBefore (t : Timestamp) : Nat := + (Rfc3339.Spec.leapTable.tail.filter fun e => Rfc3339.Spec.leapSecondKey e.1 < Rfc3339.Spec.secondKey t).length /-- SI seconds from 1972-01-01T00:00:00Z to `t`, without its fraction: the Unix seconds between them, which count 86400 to every day, and one more for each leap second of the table between them. -/ -def Spec.siSeconds (t : Timestamp) : Int := - Spec.unixSeconds t - Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ + Spec.leapsBefore t +def Rfc3339.Spec.siSeconds (t : Timestamp) : Int := + Rfc3339.Spec.unixSeconds t - Rfc3339.Spec.unixSeconds ⟨1972, 1, 1, 0, 0, 0, [], .z⟩ + Rfc3339.Spec.leapsBefore t /-- TAI − UTC at NTP time `ntp`: the value on the table's last line at or before it. -/ -def Spec.taiMinusUtcAt (ntp : Int) : Nat := - ((Spec.leapTable.filter fun e => (e.1 : Int) ≤ ntp).getLast?.map (·.2)).getD 0 +def Rfc3339.Spec.taiMinusUtcAt (ntp : Int) : Nat := + ((Rfc3339.Spec.leapTable.filter fun e => (e.1 : Int) ≤ ntp).getLast?.map (·.2)).getD 0 -example : Spec.taiMinusUtcAt 2272060800 = 10 ∧ Spec.taiMinusUtcAt 3692217599 = 36 ∧ - Spec.taiMinusUtcAt 3692217600 = 37 := by decide +example : Rfc3339.Spec.taiMinusUtcAt 2272060800 = 10 ∧ Rfc3339.Spec.taiMinusUtcAt 3692217599 = 36 ∧ + Rfc3339.Spec.taiMinusUtcAt 3692217600 = 37 := by decide diff --git a/Rfc3339/Types.lean b/Rfc3339/Types.lean index 42c6c8f..19abea3 100644 --- a/Rfc3339/Types.lean +++ b/Rfc3339/Types.lean @@ -1,10 +1,10 @@ /- What a timestamp is: the values the parser produces and the printer - takes. Part of the approved specification, with `Spec.lean` and + takes. Part of the approved specification, with `Rfc3339/Spec.lean` and `Spec/Defs.lean`, since every statement is about these types. A value holds each field of an RFC 3339 `date-time` as a number, - exactly as written. Which values are valid is `Spec.Valid`, in + exactly as written. Which values are valid is `Rfc3339.Spec.Valid`, in `Spec/Defs.lean`. -/ diff --git a/SPEC.md b/SPEC.md index 4f72cb6..94be736 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. 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. +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 `Rfc3339/Spec.lean`, `Rfc3339/Spec/Defs.lean`, `Rfc3339/Types.lean`, `Rfc3339/Spec/Leap.lean`, `Rfc3339/Spec/Ixdtf.lean`, `Rfc3339/IxdtfTypes.lean`, and the other files `bar.toml` lists. ## The format @@ -18,7 +18,7 @@ time-offset = "Z" / ("+" / "-") time-hour ":" time-minute - Every field has exactly the number of digits the grammar gives. A digit is an ASCII digit, `0` to `9`. The parser rejects digits from other scripts, such as `٣` and `0`. - The year runs from 0000 to 9999 and the month from 01 to 12. The day runs from 01 to the length of its month, as in the table of section 5.7. February has 29 days in a leap year and 28 otherwise. A leap year is one divisible by 4, unless it is divisible by 100 and not by 400 (Appendix C). - The hour runs from 00 to 23 and the minute from 00 to 59. The second runs from 00 to 59. It may be 60 only for a leap second, which section 5.7 places at the end of a month in UTC. With the offset applied, the time must be 23:59 UTC on the last day of a month. Because the leap second is shifted by the offset, `1990-12-31T15:59:60-08:00` is the same leap second as `1990-12-31T23:59:60Z`. -- Section 5.7 allows second 60 only at the end of months in which a leap second occurs. `isValid` and `parse` use no table of them, so they allow second 60 at the end of every month, which is more than section 5.7 allows; `isValidKnown`, below, checks it against the table. It also allows second 59 everywhere, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. `Spec.Valid` states the rule as this library applies it. +- Section 5.7 allows second 60 only at the end of months in which a leap second occurs. `isValid` and `parse` use no table of them, so they allow second 60 at the end of every month, which is more than section 5.7 allows; `isValidKnown`, below, checks it against the table. It also allows second 59 everywhere, although section 5.7 makes 58 the last second of a month after a negative leap second, which has never happened. `Rfc3339.Spec.Valid` states the rule as this library applies it. - The fraction is optional. When present it is a point and at least one digit, with no upper limit on the digits. The parser keeps every digit as written. - The offset is `Z`, `+hh:mm` or `-hh:mm`, with hours from 00 to 23 and minutes from 00 to 59. Section 4.3 gives `-00:00` its own meaning, an unknown local offset. It is therefore kept apart from `+00:00` and from `Z`, although all three name the same instant. - The note under the grammar lets `T` and `Z` be written in lower case. The parser accepts `t` and `z`, and printing writes upper case. @@ -32,7 +32,7 @@ time-offset = "Z" / ("+" / "-") time-hour ":" time-minute ## The value -`parse` returns a `Timestamp`: the year, month, day, hour, minute and second as numbers, the fraction as a list of digits, and the offset (`Z`, plus, or minus, with hours and minutes). The fields are those of the string as written, in its local time. `Spec.Valid` says which values the rules above allow. `Timestamp.isValid` decides it for a value built some other way. +`parse` returns a `Timestamp`: the year, month, day, hour, minute and second as numbers, the fraction as a list of digits, and the offset (`Z`, plus, or minus, with hours and minutes). The fields are those of the string as written, in its local time. `Rfc3339.Spec.Valid` says which values the rules above allow. `Timestamp.isValid` decides it for a value built some other way. `Timestamp.print` writes a valid timestamp in the form above, with `T` and `Z` in upper case. @@ -52,18 +52,18 @@ Every second from `0000-01-01T00:00:00Z` (-62167219200) to `9999-12-31T23:59:59Z ## Leap seconds, with the table -Section 5.7 allows second 60 only "at the end of months in which a leap second occurs". `isValid` cannot know those months; `isValidKnown` uses a table of them. The table is tzdata's `leap-seconds.list`, which publishes IERS Bulletin C. `Spec/Leap.lean` copies it line for line: 28 NTP times, from 1 January 1972 to 1 January 2017, each with TAI − UTC from that time on, 10 to 37 seconds. Each line after the first follows a leap second, the second `23:59:60` UTC just before it, so there have been 27. The file expires on 28 June 2027: until then, no leap second comes that it does not list. +Section 5.7 allows second 60 only "at the end of months in which a leap second occurs". `isValid` cannot know those months; `isValidKnown` uses a table of them. The table is tzdata's `leap-seconds.list`, which publishes IERS Bulletin C. `Rfc3339/Spec/Leap.lean` copies it line for line: 28 NTP times, from 1 January 1972 to 1 January 2017, each with TAI − UTC from that time on, 10 to 37 seconds. Each line after the first follows a leap second, the second `23:59:60` UTC just before it, so there have been 27. The file expires on 28 June 2027: until then, no leap second comes that it does not list. - `isValidKnown` is `isValid`, with second 60 allowed only at one of the table's leap seconds. The instant is what counts, whatever the offset: `1990-12-31T15:59:60-08:00` is the leap second at the end of 1990, and `2017-01-01T00:59:60+01:00` the one at the end of 2016. `2015-12-31T23:59:60Z` is refused, since that leap second came at the end of June 2015. - `siSeconds` gives the Unix seconds from `1972-01-01T00:00:00Z`, ignoring the fraction, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds between them. So `2016-12-31T23:59:59Z`, `2016-12-31T23:59:60Z` and `2017-01-01T00:00:00Z` get three numbers in a row, where Unix seconds give the last two the same one. On whole seconds valid by the table, these numbers are in the order of the instants, as `compareInstant` gives it. - `fromSiSeconds` goes back: from SI seconds to the UTC timestamp, a leap second as second 60. It gives one for every number from 0, `1972-01-01T00:00:00Z`, to that of `9999-12-31T23:59:59Z`, and `none` outside. - `taiMinusUtc` gives TAI − UTC: 10, and one more for each leap second before the timestamp. At every second from 1972 on, a leap second aside, it is the table's second column. During a leap second it is still the value from before it. -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. +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 `Rfc3339.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. +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]`. `Rfc3339/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 `..`. @@ -101,55 +101,55 @@ 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`, `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. +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 `Rfc3339.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`, 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. +Each property is a theorem in `Rfc3339/Spec.lean`, under the name given. The definitions the statements use are in `Rfc3339/Spec/Defs.lean`, for the leap second table in `Rfc3339/Spec/Leap.lean`, and for RFC 9557 in `Rfc3339/Spec/Ixdtf.lean`. They are written from the RFC and checked against its tables and against known day counts. | Property | Theorem | |----------|---------| -| `isValid` decides exactly `Spec.Valid`: the rules of sections 5.6 and 5.7, with second 60 allowed at the end of every month. | `Spec.isValid_iff` | -| A valid timestamp prints as the grammar writes it. | `Spec.print_eq` | -| `parse` returns `t` exactly when `t` is valid and the string is how `t` prints, with `T` and `Z` in either case. | `Spec.parse_iff` | -| What `parse` returns is valid: the day exists in its month, a leap second ends a month in UTC, and so on. | `Spec.parse_valid` | -| Printing then parsing gives the timestamp back. | `Spec.parse_print` | -| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Spec.print_parse` | -| `unixSeconds` counts the seconds from the epoch by the calendar, with the offset applied. | `Spec.unixSeconds_eq` | -| `compareInstant` orders timestamps by the instants they name: UTC minute, then second, then fraction. | `Spec.compareInstant_eq` | -| The examples of section 5.8 parse to the fields the RFC reads them as. | `Spec.rfc3339_examples` | -| What section 5.8 says about those examples holds: two pairs name the same instant. Separately, the first is 482196050 seconds after the epoch, as Python's `calendar.timegm` gives. | `Spec.rfc3339_example_instants` | -| A leap second comes after second 59 and before the next minute; its Unix seconds equal those of the next second. | `Spec.leap_second_order` | -| Days outside their month are rejected, with the leap year rule of Appendix C. | `Spec.calendar_vectors` | -| Second 60 is accepted only at the end of a month in UTC. | `Spec.leap_second_vectors` | -| Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Spec.syntax_vectors` | -| `fromUnixSeconds s` is `t` exactly when `t` is valid, in UTC, with no fraction and a second of at most 59, and names `s`. | `Spec.fromUnixSeconds_iff` | -| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z. | `Spec.fromUnixSeconds_isSome` | -| 0096-12-31 at midnight, the epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` | -| `isValidKnown` decides `Spec.ValidKnown`: `Spec.Valid`, with second 60 only at a leap second of the table. | `Spec.isValidKnown_iff` | -| `siSeconds` is Unix seconds since 1972 and one more for each leap second of the table before the timestamp. | `Spec.siSeconds_eq` | -| On whole seconds valid by the table, `siSeconds` gives the order of the instants. | `Spec.siSeconds_order` | -| `fromSiSeconds n` is `t` exactly when `t` is in UTC, with no fraction, valid by the table, from 1972 on, and has SI seconds `n`; it gives one for every second from 1972 to 9999. | `Spec.fromSiSeconds_iff`, `Spec.fromSiSeconds_isSome` | -| `taiMinusUtc` is 10 and one more for each leap second of the table before the timestamp. | `Spec.taiMinusUtc_leapsBefore` | -| TAI − UTC from 1972 on, at each second but a leap second, is the table's value. | `Spec.taiMinusUtc_eq` | -| Leap seconds of the table and months without one; SI seconds and TAI − UTC around the first and the last; the round trip Unix seconds lose. | `Spec.leap_table_vectors` | -| `parseExt s` is `e` exactly when `e` is valid by the RFC 9557 grammar and `s` is a timestamp `parse` reads as `e`'s, then `e`'s suffix as the grammar writes it. | `Spec.parseExt_iff` | -| A valid `Ext` prints as the grammar writes it. | `Spec.printExt_eq` | -| Printing then parsing gives a valid `Ext` back. | `Spec.parseExt_print` | -| A string with no `[` reads as `parse` reads it, with no time zone and no tags. | `Spec.parseExt_plain` | -| `lookup` gives the first tag with the key. | `Spec.lookup_iff` | -| `erroneous` decides `Spec.MustReject`: the rules of sections 3.2 to 3.4, for any application. | `Spec.erroneous_iff` | -| Every example of RFC 9557 is read, and is erroneous for the example application exactly where the RFC says; so are critical zones that agree with the offset and a critical `-00:00` zone that does not; strings the grammar refuses are not read. | `Spec.ixdtf_vectors` | +| `isValid` decides exactly `Rfc3339.Spec.Valid`: the rules of sections 5.6 and 5.7, with second 60 allowed at the end of every month. | `Rfc3339.Spec.isValid_iff` | +| A valid timestamp prints as the grammar writes it. | `Rfc3339.Spec.print_eq` | +| `parse` returns `t` exactly when `t` is valid and the string is how `t` prints, with `T` and `Z` in either case. | `Rfc3339.Spec.parse_iff` | +| What `parse` returns is valid: the day exists in its month, a leap second ends a month in UTC, and so on. | `Rfc3339.Spec.parse_valid` | +| Printing then parsing gives the timestamp back. | `Rfc3339.Spec.parse_print` | +| Parsing then printing gives the string back, with `T` and `Z` in upper case. | `Rfc3339.Spec.print_parse` | +| `unixSeconds` counts the seconds from the epoch by the calendar, with the offset applied. | `Rfc3339.Spec.unixSeconds_eq` | +| `compareInstant` orders timestamps by the instants they name: UTC minute, then second, then fraction. | `Rfc3339.Spec.compareInstant_eq` | +| The examples of section 5.8 parse to the fields the RFC reads them as. | `Rfc3339.Spec.rfc3339_examples` | +| What section 5.8 says about those examples holds: two pairs name the same instant. Separately, the first is 482196050 seconds after the epoch, as Python's `calendar.timegm` gives. | `Rfc3339.Spec.rfc3339_example_instants` | +| A leap second comes after second 59 and before the next minute; its Unix seconds equal those of the next second. | `Rfc3339.Spec.leap_second_order` | +| Days outside their month are rejected, with the leap year rule of Appendix C. | `Rfc3339.Spec.calendar_vectors` | +| Second 60 is accepted only at the end of a month in UTC. | `Rfc3339.Spec.leap_second_vectors` | +| Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Rfc3339.Spec.syntax_vectors` | +| `fromUnixSeconds s` is `t` exactly when `t` is valid, in UTC, with no fraction and a second of at most 59, and names `s`. | `Rfc3339.Spec.fromUnixSeconds_iff` | +| `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z. | `Rfc3339.Spec.fromUnixSeconds_isSome` | +| 0096-12-31 at midnight, the epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Rfc3339.Spec.fromUnixSeconds_vectors` | +| `isValidKnown` decides `Rfc3339.Spec.ValidKnown`: `Rfc3339.Spec.Valid`, with second 60 only at a leap second of the table. | `Rfc3339.Spec.isValidKnown_iff` | +| `siSeconds` is Unix seconds since 1972 and one more for each leap second of the table before the timestamp. | `Rfc3339.Spec.siSeconds_eq` | +| On whole seconds valid by the table, `siSeconds` gives the order of the instants. | `Rfc3339.Spec.siSeconds_order` | +| `fromSiSeconds n` is `t` exactly when `t` is in UTC, with no fraction, valid by the table, from 1972 on, and has SI seconds `n`; it gives one for every second from 1972 to 9999. | `Rfc3339.Spec.fromSiSeconds_iff`, `Rfc3339.Spec.fromSiSeconds_isSome` | +| `taiMinusUtc` is 10 and one more for each leap second of the table before the timestamp. | `Rfc3339.Spec.taiMinusUtc_leapsBefore` | +| TAI − UTC from 1972 on, at each second but a leap second, is the table's value. | `Rfc3339.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. | `Rfc3339.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. | `Rfc3339.Spec.parseExt_iff` | +| A valid `Ext` prints as the grammar writes it. | `Rfc3339.Spec.printExt_eq` | +| Printing then parsing gives a valid `Ext` back. | `Rfc3339.Spec.parseExt_print` | +| A string with no `[` reads as `parse` reads it, with no time zone and no tags. | `Rfc3339.Spec.parseExt_plain` | +| `lookup` gives the first tag with the key. | `Rfc3339.Spec.lookup_iff` | +| `erroneous` decides `Rfc3339.Spec.MustReject`: the rules of sections 3.2 to 3.4, for any application. | `Rfc3339.Spec.erroneous_iff` | +| Every example of RFC 9557 is read, and is erroneous for the example application exactly where the RFC says; so are critical zones that agree with the offset and a critical `-00:00` zone that does not; strings the grammar refuses are not read. | `Rfc3339.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. +- `fromUnixSeconds` is fixed for every number, by `Rfc3339.Spec.fromUnixSeconds_iff` and `Rfc3339.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`. +- `isValidKnown` is fixed for every timestamp, and `siSeconds` for every valid one. `taiMinusUtc` is fixed for every valid timestamp, by `Rfc3339.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 `Rfc3339.Spec.parse_valid`, but it would fail `Rfc3339.Spec.parse_iff` and `Rfc3339.Spec.parse_print`. +- A parser that accepted too much would fail `Rfc3339.Spec.parse_iff`. ## Oracle @@ -162,26 +162,29 @@ The differential tests compare the tool with these oracles: ## Follow-up verification record -`Rfc3339.Proofs.Leap.leapKey_table` in `Proofs/Leap/Table.lean` +`Rfc3339.Proofs.Leap.leapKey_table` in `Rfc3339/Proofs/Leap/Table.lean` proves that the implementation's ordered list of leap-second keys equals -the keys derived from `Spec.leapTable.tail`. `Spec.isValidKnown_iff` uses -that equality. The literal table's agreement with IERS remains trusted. +the keys derived from `Rfc3339.Spec.leapTable.tail`. +`Rfc3339.Spec.isValidKnown_iff` uses that equality. The literal table's +agreement with IERS remains trusted. Before the table expires on 28 June 2027, obtain the current IERS Bulletin C -and tzdata leap-seconds.list, compare the literal table in `Spec/Leap.lean`, -and update its source and expiry record. If an entry changes, update -`Rfc3339/Leap.lean` in the same change, rebuild the table equality proof, -and rerun the full bar and differential suite. Have a spec reviewer check -the replacement source. Expiry alone does not announce a leap second. +and tzdata leap-seconds.list, compare the literal table in +`Rfc3339/Spec/Leap.lean`, and update its source and expiry record. If an +entry changes, update `Rfc3339/Leap.lean` in the same change, rebuild the +table equality proof, and rerun the full bar and differential suite. Have a +spec reviewer check the replacement source. Expiry alone does not announce a +leap second. The external Go, Temporal and ERFA cross-check remains a one-off comparison (`tests/CROSS-CHECK.md`), outside the verified bar. The 0096-12-31 UTC -midnight case is now also a kernel-computed `Spec.fromUnixSeconds_vectors` -case, rather than only a differential calendar-grid case. - -The long IXDTF vectors in `Proofs/Ixdtf/Main.lean` use `vx_validB_sound` -and the parser equivalence proof; they do not directly execute the whole -parser in the kernel. Their shorter timestamp components and grammar -checks are kernel-computed. The existing processor vectors are examples -of one tag policy; this slice provides no worked alternative tag-set -application. `Spec.erroneous_iff` quantifies over every `Processor`. +midnight case is now also a kernel-computed +`Rfc3339.Spec.fromUnixSeconds_vectors` case, rather than only a differential +calendar-grid case. + +The long IXDTF vectors in `Rfc3339/Proofs/Ixdtf/Main.lean` use +`vx_validB_sound` and the parser equivalence proof; they do not directly +execute the whole parser in the kernel. Their shorter timestamp components +and grammar checks are kernel-computed. The existing processor vectors are +examples of one tag policy; this slice provides no worked alternative tag-set +application. `Rfc3339.Spec.erroneous_iff` quantifies over every `Processor`. diff --git a/bar.toml b/bar.toml index 744cf5d..93257a3 100644 --- a/bar.toml +++ b/bar.toml @@ -16,7 +16,7 @@ entry_points = ["Main.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", + "SPEC.md", "Rfc3339/Spec.lean", "Rfc3339/Spec/Defs.lean", "Rfc3339/Spec/Leap.lean", "Rfc3339/Spec/Ixdtf.lean", "Rfc3339/Types.lean", "Rfc3339/IxdtfTypes.lean", ] # The code under proof: the functions the statements are about. diff --git a/comparator.json b/comparator.json index 5b58b19..a8e9503 100644 --- a/comparator.json +++ b/comparator.json @@ -1,39 +1,39 @@ { - "challenge_module": "Spec", - "solution_module": "Proofs", + "challenge_module": "Rfc3339.Spec", + "solution_module": "Rfc3339.Proofs", "theorem_names": [ - "Spec.isValid_iff", - "Spec.print_eq", - "Spec.parse_iff", - "Spec.parse_valid", - "Spec.parse_print", - "Spec.print_parse", - "Spec.unixSeconds_eq", - "Spec.compareInstant_eq", - "Spec.rfc3339_examples", - "Spec.rfc3339_example_instants", - "Spec.leap_second_order", - "Spec.calendar_vectors", - "Spec.leap_second_vectors", - "Spec.syntax_vectors", - "Spec.fromUnixSeconds_iff", - "Spec.fromUnixSeconds_isSome", - "Spec.fromUnixSeconds_vectors", - "Spec.isValidKnown_iff", - "Spec.siSeconds_eq", - "Spec.siSeconds_order", - "Spec.fromSiSeconds_iff", - "Spec.fromSiSeconds_isSome", - "Spec.taiMinusUtc_leapsBefore", - "Spec.taiMinusUtc_eq", - "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" + "Rfc3339.Spec.isValid_iff", + "Rfc3339.Spec.print_eq", + "Rfc3339.Spec.parse_iff", + "Rfc3339.Spec.parse_valid", + "Rfc3339.Spec.parse_print", + "Rfc3339.Spec.print_parse", + "Rfc3339.Spec.unixSeconds_eq", + "Rfc3339.Spec.compareInstant_eq", + "Rfc3339.Spec.rfc3339_examples", + "Rfc3339.Spec.rfc3339_example_instants", + "Rfc3339.Spec.leap_second_order", + "Rfc3339.Spec.calendar_vectors", + "Rfc3339.Spec.leap_second_vectors", + "Rfc3339.Spec.syntax_vectors", + "Rfc3339.Spec.fromUnixSeconds_iff", + "Rfc3339.Spec.fromUnixSeconds_isSome", + "Rfc3339.Spec.fromUnixSeconds_vectors", + "Rfc3339.Spec.isValidKnown_iff", + "Rfc3339.Spec.siSeconds_eq", + "Rfc3339.Spec.siSeconds_order", + "Rfc3339.Spec.fromSiSeconds_iff", + "Rfc3339.Spec.fromSiSeconds_isSome", + "Rfc3339.Spec.taiMinusUtc_leapsBefore", + "Rfc3339.Spec.taiMinusUtc_eq", + "Rfc3339.Spec.leap_table_vectors", + "Rfc3339.Spec.parseExt_iff", + "Rfc3339.Spec.printExt_eq", + "Rfc3339.Spec.parseExt_print", + "Rfc3339.Spec.parseExt_plain", + "Rfc3339.Spec.lookup_iff", + "Rfc3339.Spec.erroneous_iff", + "Rfc3339.Spec.ixdtf_vectors" ], "permitted_axioms": [ "propext", diff --git a/lakefile.toml b/lakefile.toml index 4365b81..c16ada2 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,16 +1,18 @@ name = "rfc3339" version = "0.1.0" license = "Apache-2.0" -defaultTargets = ["Rfc3339", "Spec", "Proofs", "rfc3339"] +defaultTargets = ["Rfc3339", "Rfc3339Spec", "Rfc3339Proofs", "rfc3339"] [[lean_lib]] name = "Rfc3339" [[lean_lib]] -name = "Spec" +name = "Rfc3339Spec" +roots = ["Rfc3339.Spec"] [[lean_lib]] -name = "Proofs" +name = "Rfc3339Proofs" +roots = ["Rfc3339.Proofs"] [[lean_exe]] name = "rfc3339" diff --git a/tests/run_tests.py b/tests/run_tests.py index 219b5e9..14bd30b 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -228,7 +228,7 @@ def si_grid(): 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. +# The example application of Rfc3339.Spec.exampleProcessor. IX_CALENDARS = (["chinese"], ["japanese"], ["hebrew"]) IX_ZONES = {"Europe/Paris": 120, "Europe/London": 60, "America/Los_Angeles": -480}