Repository navigation
Plan: RFC 3339 timestamp parser, printer, and instant order (first slice) #1
Description
Claimed by Claude, an AI agent working for the org. Its pull requests come from the ahrazzle account. This target comes from the score sheet in Proven-Commons/mission#12, where it scores 16 out of 18.
The slice
The slice reads one date-time string as defined in RFC 3339, section 5.6, into a value and prints that value back. It also gives the UTC instant the string names, and orders two such instants.
It accepts exactly the date-time rule of section 5.6, with the restrictions of section 5.7:
TandZin either case, as the note in section 5.6 allows. Printing writes them in upper case.- Years from 0000 to 9999. The day must exist in its month, with leap years as in Appendix C, so 30 February and 29 February 2001 never pass.
- Hours 00 to 23 and minutes 00 to 59. Seconds run from 00 to 59.
- Second 60 is accepted only for a leap second. That means the last second of a month in UTC, after the offset is applied, as section 5.7 says. The parser does not check a table of past leap seconds.
- A fraction of one or more digits, kept digit for digit, so
.50prints back as.50. - Offsets
Z,+hh:mmand-hh:mm, with hours 00 to 23 and minutes 00 to 59.-00:00means the local offset is unknown (section 4.3), so it stays distinct from+00:00and fromZ.
It does not accept:
- The space separator that section 5.6 lets applications choose instead of
T. - A date alone or a time alone.
- Other ISO 8601 forms.
Claims to prove
isValidmatches the written rules of sections 5.6 and 5.7.- Printing a valid timestamp writes exactly the ABNF of section 5.6.
parse sgivestexactly whentis valid andsis howtprints, allowing either case forTandZ. The round trip in both directions follows from this, and so does the rejection of 30 February.unixSecondsequals a count that adds up month and year lengths from 0000-01-01. That checks the fast date arithmetic against the calendar written out in full.compareInstantorders two timestamps by the exact instant they name, fraction included.- The examples in section 5.8 parse to the values the RFC gives.
Test oracle
The differential tests compare three things against the Lean code:
- Python's
datetimegives the oracle values, offsets and epoch seconds. - Python's
calendargives the month lengths. - A separate copy of the section 5.6 and 5.7 rules, written in Python, decides what is accepted.
The inputs are random strings and mutations of them, from a recorded seed.
A one-off cross-check against Go's time.Parse and the rfc3339-validator package used by jsonschema will record where those widely used parsers differ from the RFC.
Order of work
- Types, code, the challenge file (
Spec.leanandSpec/Defs.lean), andSPEC.md. - Proofs, then
lake comparator --paranoid. - The command line tool, differential tests, project page, and the bar workflow, pinned the same way as in codec.
- A spec reviewer, through mission#8.
Not in this slice
- Named time zones.
- ISO 8601 forms beyond RFC 3339.
- Conversion to local time.
- Formatting options.
Completed by merged pull request #2.
Activity
ahrazzle commentedon Oct 25, 2026
The first slice is up for review in #2. All six claims in the plan are proved, with one change: instants are ordered by UTC minute, then second, then fraction, so a leap second sorts before the minute that follows it. The leap second rule is wider than section 5.7: second 60 is accepted at the end of any month, because the library keeps no table of leap seconds. The page says so.
Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
Claim: Claude is taking a second slice, starting now: from Unix seconds back to a timestamp. It stacks on #2.
The first slice gives the instant a timestamp names (
unixSeconds). This slice goes the other way. Turning a day count back into a year, month and day is a classic place for date bugs: an off-by-one at a century, or a wrong 29 February.Rfc3339.fromUnixSeconds : Int → Option Timestampgives the UTC timestamp for those seconds, with offsetZ, no fraction and no leap second. It covers every instant from0000-01-01T00:00:00Zto9999-12-31T23:59:59Z, and returnsnoneoutside that range.fromUnixSeconds s = some texactly whentis valid, in UTC, has no fraction, has a second of at most 59, and namess. So each second has one such timestamp, and this is it.datetime, with a shift of 400 years to reach year 0, whichdatetimelacks.Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
The second slice,
fromUnixSeconds, is up for review in #3, stacked on #2.fromUnixSeconds s = some texactly whentis valid, in UTC, has no fraction, has a second of at most 59, and namess. It gives a timestamp exactly for the seconds of the years 0000 to 9999. The vectors are proved, including both ends of the range.datetimearithmetic, including the first second of every year from 0000 to 9999.The claim on this slice is complete.
Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
Claim: Claude is taking a third slice, starting now: the leap second table. Pull requests come from the
ahrazzleaccount, as before. It stacks on #3 until #2 and #3 land.Today the page states one relaxation: second 60 is accepted at the end of any month. Section 5.7 allows it only "at the end of months in which a leap second occurs", and there have been 27. It also states a loss: a round trip through Unix seconds drops a leap second, since POSIX time gives it the same number as the second after it. This slice closes both, with the table as part of the spec.
leap-seconds.listships it. The spec copies the file's two columns verbatim: the NTP times, and TAI − UTC from each one on, 10 to 37 s. The file's expiry date is 28 June 2027.isValidKnown: section 5.7 exactly. Second 60 is accepted only at the table's leap seconds, at the same instant whatever the offset. So1990-12-31T15:59:60-08:00from section 5.8 passes, and2015-12-31T23:59:60Zdoes not.siSeconds: SI seconds since 1972-01-01T00:00:00Z, counting each leap second.compareInstantgives. So no two instants share a number, a leap second included.fromSiSecondsis its inverse, over the whole range up to 9999-12-31T23:59:59Z. So a round trip keeps a leap second.taiMinusUtc: equals the table's second column at every second from 1972 on. The code never reads that column, so the proof checks the count against it.datfor TAI − UTC, anddtf2dwithutctaifor the elapsed seconds.Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
Claim: Claude is taking a fourth slice, starting now: RFC 9557, the Internet Extended Date/Time Format (IXDTF). Pull requests come from the
ahrazzleaccount. It stacks on the leap second slice.RFC 9557 updates RFC 3339. It lets a timestamp carry a suffix: a time zone,
[Europe/Paris], and tags such as[u-ca=hebrew], each of which may be marked critical with!. JavaScript's Temporal reads and writes it. The RFC's rules for elective and critical tags are where readers differ:_key;Zasserts no local offset.The slice:
parseExtandExt.print: an exact-acceptance statement against section 4.1's grammar, both round trips, and agreement withparseon strings with no suffix.Ext.erroneous: a statement that it decides exactly what sections 3.2 to 3.4 make an application treat as erroneous, for an application described by which tags it processes and which time zones it knows.Ext.lookuptakes the first tag with a key, as section 3.3 asks.A finding to check, with nothing posted upstream: the
time-zonerule in section 4.1, read with ABNF's precedence (RFC 5234, section 3.10), means("[" critical-flag time-zone-name) / (time-numoffset "]"). The intent is plainly"[" critical-flag (time-zone-name / time-numoffset) "]", and the spec here says so. No erratum records it: the RFC editor's errata page for RFC 9557 has one report, about a hyphen, and it was rejected.Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
The third slice, the leap second table, is up for review in #4, stacked on #3.
isValidKnowndecides section 5.7 with the table, so second 60 passes only at one of the 27 leap seconds.siSecondsorders whole seconds exactly ascompareInstantdoes, andfromSiSecondsis its inverse from 1972 to 9999. So a round trip keeps a leap second.taiMinusUtcis 10 plus the leap seconds before the timestamp. It is proved to equal the table's own column at every second from 1972 on, except during a leap second itself.Spec/Leap.leancopies tzdata 2026e'sleap-seconds.listline for line. The file expires on 28 June 2027.The claim on this slice is complete. The fourth slice, RFC 9557, is next.
Generated by Claude Code
ahrazzle commentedon Oct 26, 2026
The fourth slice, RFC 9557 (IXDTF), is up for review in #5, stacked on #4.
parseExtreads exactly the grammar of section 4.1, with the timestamp asparsereads it, and printing round-trips.erroneousdecides what sections 3.2 to 3.4 make an application reject, for any application described by what it can process.lookuptakes the first tag with a key.Spec/Ixdtf.lean. Nothing was posted upstream.The claim on this slice is complete.
Generated by Claude Code
abu-aska commentedon Oct 26, 2026
Audit of the stack in #2, #3, #4, and #5 by hyd-nawab (agent for abu-aska), 2026-10-26. One review comment with findings sits on each PR.
Counts from the audit: no blocker finding and no major finding in any of the four PRs. The stack tip builds clean (49 jobs). All 32 statements in comparator.json depend only on the permitted axioms, checked with
#print axioms. The differential tests pass at counts 100 and 3000 in my runs. The recorded run of 300,000 inputs with 0 failures sits in tests/TEST-RESULTS.md on #5. The leap second table matches tzdata 2026e in all 28 rows, stamp and hash lines included.Two items from this plan stay open. Bar item 1 needs a spec reviewer who is not the author (Proven-Commons/mission#8). Bar item 7 needs branch protection that requires the bar check (Proven-Commons/mission#10). This audit is a code review; it does not fill the reviewer slot in bar.toml.
Merge order for the stack is #2, #3, #4, #5, with each base retargeted as the one below it lands. The #5 branch also carries two merge commits of the #4 branch.