Temporal Mechanization

Our mission is to prove the correctness of a selection of the functions in the ECMAScript Temporal Proposal.

Changes to Specification

Based on our findings, the specification text of the proposal has been changed. Our mechanization is now updated without the inconsistencies we found, but there are links to the proofs of the inconsistencies in the Previous Inconsistencies section.

Developers

• Aria Bjørnbakken Eide
• Vebjørn Søreide Øiestad

Supervisor

• Mikhail Barash

Creating Makefile and Building Project

$ rocq makefile -f _CoqProject -o Makefile
$ make

or just

$ ./build.sh

Mechanized Functions

Section 3

• 3.5.1 ISO Date Records
• 3.5.2 CreateISODateRecord
• 3.5.6 RegulateISODate
• 3.5.7 IsValidISODate
• 3.5.9 PadISOYear
• 3.5.10 TemporalDateToString
• 3.5.12 CompareISODate

Section 4

• 4.5.1 Time Records
• 4.5.2 CreateTimeRecord
• 4.5.3 MidnightTimeRecord
• 4.5.4 NoonTimeRecord
• 4.5.5 DifferenceTime
• 4.5.8 RegulateTime
• 4.5.9 IsValidTime
• 4.5.10 BalanceTime
• 4.5.13 TimeRecordToString
• 4.5.14 CompareTimeRecord
• 4.5.15 AddTime

Section 5

• 5.5.1 ISO Date-Time Records
• 5.5.3 CombineISODateAndTimeRecord
• 5.5.9 ISODateTimeToString
• 5.5.10 CompareISODateTime

Section 7

• 7.5.1 Date Duration Records
• 7.5.14 DateDurationSign
• 7.5.21 TimeDurationFromComponents
• 7.5.22 AddTimeDuration
• 7.5.23 Add24HourDaysToTimeDuration
• 7.5.24 AddTimeDurationToEpochNanoseconds
• 7.5.25 CompareTimeDuration
• 7.5.26 TimeDurationFromEpochNanosecondsDifference
• 7.5.28 TimeDurationSign

Section 8

• 8.5.1 IsValidEpochNanoseconds
• 8.5.4 CompareEpochNanoseconds
• 8.5.5 AddInstant

Section 9

• 9.5.1 ISO Year-Month Records
• 9.5.3 ISOYearMonthWithinLimits
• 9.5.4 BalanceISOYearMonth

Section 11

• 11.1.5 FormatOffsetTimeZoneIdentifier
• 11.1.6 FormatUTCOffsetNanoseconds

Section 12

• 12.1 Calendar Types
• 12.3.15 FormatCalendarAnnotation
• 12.3.17 ISODaysInMonth

Section 13

• 13.2 EpochDaysToEpochMs
• 13.3 Date Equations
• 13.8 NegateRoundingMode
• 13.14 ValidateTemporalRoundingIncrement
• 13.16 ToSecondsStringPrecisionRecord
• 13.18 ValidateTemporalUnitValue
• 13.20 LargerOfTwoTemporalUnits
• 13.21 IsCalendarUnit
• 13.22 TemporalUnitCategory
• 13.23 MaximumTemporalDurationRoundingIncrement
• 13.25 FormatFractionalSeconds
• 13.26 FormatTimeString
• 13.27 GetUnsignedRoundingMode

Previous Inconsistencies

• 3.5.1 ISODateRecord_IsValidISODate_not_guaranteed
• 4.5.10 BalanceTime_creates_invalid_TimeRecord
• 11.1.5 FormatOffsetTimeZoneIdentifier_hour_outside_bounds_of_FormatTimeString
• 11.1.6 FormatUTCOffsetNanoseconds_hour_outside_bounds_of_FormatTimeString

Other Findings

• 7.5.21 TimeDurationFromComponents_nanoseconds'_outside_bounds_of_MaxTimeDuration
• 7.5.26 TimeDurationFromEpochNanosecondsDifference_result_outside_bounds_of_MaxTimeDuration

Notes

• 5.5.3 CombineISODateAndTimeRecord

Theorems

Proven

• RegulateISODate_never_throws_on_constrain
• PadISOYear_result_length_at_least_4
• BalanceTime_IsValidTime
• DateDurationSign_year_sign_dominates
• CompareISODate_eq_zero
• CompareISODate_eq_implies_eq_zero
• CompareTimeRecord_eq_zero
• AddTime_adding_zero_no_change

Unproven

• TemporalDateToString_without_calendar_satisfies_rfc3339
• ISODateTimeToString_without_calendar_satisfies_rfc3339
• CompareTimeRecord_eq_implies_eq_zero