Datetime grammar: definitions

This file gives a direct, parser-independent transcription of the datetime grammar, its component value function, and the declarative relation connecting a string to its epoch-millisecond value. Well-formedness takes the same shape as the decimal and duration grammars — the string is the rendering of well-formed components — but the datetime grammar describes a date optionally followed by a time, a fractional-seconds field, and a zone designator, so the components form a nested record rather than a flat sequence of fields. The Digit⁺ predicate IsDigits and its fixed-width refinement IsFixedDigits (the grammar's Digit{n}, used for every numeric field here) are shared with the decimal and duration grammars and live in Cedar.Thm.Data.String, together with the shared natOf numeric reader.

Numeric constraints

The grammar's Constraints block bounds each numeric field. These are pure arithmetic predicates over the field values; daysInMonth and isLeapYear transcribe the two auxiliary functions the day constraint depends on.

def Cedar.Thm.Datetime.isLeapYear (y : Nat) : Bool

The grammar's isLeapYear(y) = (4 | y) ∧ (¬(100 | y) ∨ (400 | y)), as a decidable Bool.

Equations

• Cedar.Thm.Datetime.isLeapYear y = (y % 4 == 0 && (y % 100 != 0 || y % 400 == 0))

def Cedar.Thm.Datetime.daysInMonth (y m : Nat) : Nat

The grammar's daysInMonth(y, m): 30 for April/June/September/November, 28 or 29 for February depending on the leap year, and 31 otherwise.

Equations

• Cedar.Thm.Datetime.daysInMonth y m = if (m == 4 || m == 6 || m == 9 || m == 11) = true then 30 else if (m == 2) = true then if Cedar.Thm.Datetime.isLeapYear y = true then 29 else 28 else 31

Components

Each nonterminal of the grammar becomes a record of its fixed-width digit fields. A syntaxWf predicate pins the field widths (Digit{n}) and a constraintsWf predicate imposes the numeric bounds from the grammar's Constraints block.

structure Cedar.Thm.Datetime.DateComponents : Type

The grammar's Date ::= YYYY '-' MM '-' DD.

• year : String
• month : String
• day : String

def Cedar.Thm.Datetime.DateComponents.syntaxWf (d : DateComponents) : Prop

YYYY is Digit{4}; MM and DD are Digit{2}.

Equations

• d.syntaxWf = (String.IsFixedDigits 4 d.year ∧ String.IsFixedDigits 2 d.month ∧ String.IsFixedDigits 2 d.day)

def Cedar.Thm.Datetime.DateComponents.constraintsWf (d : DateComponents) : Prop

The month/day bounds: 01 ≤ MM ≤ 12 and 01 ≤ DD ≤ daysInMonth(YYYY, MM).

Equations

• d.constraintsWf = (1 ≤ d.month.natOf ∧ d.month.natOf ≤ 12 ∧ 1 ≤ d.day.natOf ∧ d.day.natOf ≤ Cedar.Thm.Datetime.daysInMonth d.year.natOf d.month.natOf)

def Cedar.Thm.Datetime.DateComponents.asString (d : DateComponents) : String

Render a date as YYYY '-' MM '-' DD.

Equations

• d.asString = d.year ++ "-" ++ d.month ++ "-" ++ d.day

structure Cedar.Thm.Datetime.TimeComponents : Type

The grammar's Time ::= hh ':' mm ':' ss.

• hours : String
• minutes : String
• seconds : String

def Cedar.Thm.Datetime.TimeComponents.syntaxWf (t : TimeComponents) : Prop

hh, mm, and ss are each Digit{2}.

Equations

• t.syntaxWf = (String.IsFixedDigits 2 t.hours ∧ String.IsFixedDigits 2 t.minutes ∧ String.IsFixedDigits 2 t.seconds)

def Cedar.Thm.Datetime.TimeComponents.constraintsWf (t : TimeComponents) : Prop

The time bounds: 00 ≤ hh ≤ 23, 00 ≤ mm ≤ 59, 00 ≤ ss ≤ 59.

Equations

• t.constraintsWf = (t.hours.natOf ≤ 23 ∧ t.minutes.natOf ≤ 59 ∧ t.seconds.natOf ≤ 59)

def Cedar.Thm.Datetime.TimeComponents.asString (t : TimeComponents) : String

Render a time as hh ':' mm ':' ss.

Equations

• t.asString = t.hours ++ ":" ++ t.minutes ++ ":" ++ t.seconds

structure Cedar.Thm.Datetime.OffsetComponents : Type

The grammar's Offset ::= ('+' | '-') hh mm. negative records the sign character; hours and mm reuse the hh/mm nonterminals of Time.

• negative : Bool
• hours : String
• minutes : String

def Cedar.Thm.Datetime.OffsetComponents.syntaxWf (o : OffsetComponents) : Prop

The offset's hh and mm are each Digit{2}, matching the Time nonterminals.

Equations

• o.syntaxWf = (String.IsFixedDigits 2 o.hours ∧ String.IsFixedDigits 2 o.minutes)

def Cedar.Thm.Datetime.OffsetComponents.constraintsWf (o : OffsetComponents) : Prop

Because the offset reuses the hh/mm nonterminals, it inherits their bounds: 00 ≤ hh ≤ 23 and 00 ≤ mm ≤ 59.

Equations

• o.constraintsWf = (o.hours.natOf ≤ 23 ∧ o.minutes.natOf ≤ 59)

def Cedar.Thm.Datetime.OffsetComponents.asString (o : OffsetComponents) : String

Render an offset as ('+' | '-') hh mm.

Equations

• o.asString = (if o.negative = true then "-" else "+") ++ o.hours ++ o.minutes

inductive Cedar.Thm.Datetime.Zone : Type

The zone designator that terminates a datetime with a time: either the UTC marker 'Z' (Date 'T' Time 'Z' / Date 'T' Time '.' SSS 'Z') or an explicit Offset.

• utc : Zone
• offset (o : OffsetComponents) : Zone

def Cedar.Thm.Datetime.Zone.syntaxWf : Zone → Prop

A UTC marker imposes nothing; an offset must have well-formed digit fields.

Equations

• Cedar.Thm.Datetime.Zone.utc.syntaxWf = True
• (Cedar.Thm.Datetime.Zone.offset o).syntaxWf = o.syntaxWf

def Cedar.Thm.Datetime.Zone.constraintsWf : Zone → Prop

A UTC marker imposes nothing; an offset must satisfy the hh/mm bounds.

Equations

• Cedar.Thm.Datetime.Zone.utc.constraintsWf = True
• (Cedar.Thm.Datetime.Zone.offset o).constraintsWf = o.constraintsWf

def Cedar.Thm.Datetime.Zone.asString : Zone → String

Render the zone: 'Z' for UTC, otherwise the offset's ('+' | '-') hh mm.

Equations

• Cedar.Thm.Datetime.Zone.utc.asString = "Z"
• (Cedar.Thm.Datetime.Zone.offset o).asString = o.asString

structure Cedar.Thm.Datetime.TimePart : Type

The time-bearing tail of a datetime: a Time, an optional fractional-seconds field SSS ('.' SSS), and a Zone. Absent SSS (none) corresponds to the forms without a '.' SSS; some corresponds to the '.' SSS forms.

• time : TimeComponents
• millis : Option String
• zone : Zone

def Cedar.Thm.Datetime.IsWfOptionalMillis : Option String → Prop

Lift IsFixedDigits 3 (the grammar's SSS ::= Digit{3}) to the optional field: an absent SSS is trivially valid.

Equations

• Cedar.Thm.Datetime.IsWfOptionalMillis none = True
• Cedar.Thm.Datetime.IsWfOptionalMillis (some millis) = String.IsFixedDigits 3 millis

def Cedar.Thm.Datetime.TimePart.syntaxWf (tp : TimePart) : Prop

The time, the optional SSS, and the zone are each well-formed.

Equations

• tp.syntaxWf = (tp.time.syntaxWf ∧ Cedar.Thm.Datetime.IsWfOptionalMillis tp.millis ∧ tp.zone.syntaxWf)

def Cedar.Thm.Datetime.TimePart.constraintsWf (tp : TimePart) : Prop

The time and zone satisfy their numeric bounds. SSS is unconstrained (000–999 are all valid), so it contributes no numeric constraint.

Equations

• tp.constraintsWf = (tp.time.constraintsWf ∧ tp.zone.constraintsWf)

def Cedar.Thm.Datetime.TimePart.asString (tp : TimePart) : String

Render the tail: 'T' Time ['.' SSS] Zone, so some sss inserts '.' sss.

Equations

• tp.asString = ("T" ++ tp.time.asString ++ match tp.millis with | none => "" | some sss => "." ++ sss) ++ tp.zone.asString

structure Cedar.Thm.Datetime.DatetimeComponents : Type

A datetime is a Date optionally followed by a time-bearing tail. none is the date-only form Date; some tp covers the four Date 'T' Time … forms, with the presence of SSS and the choice of Zone selecting among them.

• date : DateComponents
• time : Option TimePart

def Cedar.Thm.Datetime.DatetimeComponents.syntaxWf (c : DatetimeComponents) : Prop

Every present component has well-formed digit fields.

Equations

• c.syntaxWf = (c.date.syntaxWf ∧ match c.time with | none => True | some tp => tp.syntaxWf)

def Cedar.Thm.Datetime.DatetimeComponents.constraintsWf (c : DatetimeComponents) : Prop

Every present component satisfies its numeric bounds.

Equations

• c.constraintsWf = (c.date.constraintsWf ∧ match c.time with | none => True | some tp => tp.constraintsWf)

def Cedar.Thm.Datetime.DatetimeComponents.asString (c : DatetimeComponents) : String

Canonical string representation: the date, followed by the time-bearing tail when present. Phrasing well-formedness existentially over asString (below) bakes the grammar's structure in for free — the separators, the fixed field order, and the choice among the five top-level forms all follow from the shape of the witnessing record.

Equations

• c.asString = c.date.asString ++ match c.time with | none => "" | some tp => tp.asString

def Cedar.Thm.Datetime.DatetimeProduction (str : String) (components : DatetimeComponents) : Prop

The datetime grammar production witnessed by a syntactically and numerically valid component record and its rendering.

Equations

• Cedar.Thm.Datetime.DatetimeProduction str components = (components.syntaxWf ∧ components.constraintsWf ∧ str = components.asString)

def Cedar.Thm.Datetime.IsWfDatetime (str : String) : Prop

A datetime string is well-formed exactly when it has a valid grammar production.

Equations

• Cedar.Thm.Datetime.IsWfDatetime str = ∃ (components : Cedar.Thm.Datetime.DatetimeComponents), Cedar.Thm.Datetime.DatetimeProduction str components

Value relation

The component value functions below transcribe the grammar's date/time → milliseconds-since-epoch formula. IsDatetimeValue str v then reuses the same witnesses as IsWfDatetime and states that their denotation is v. No second string parser is part of the trusted grammar specification.

def Cedar.Thm.Datetime.epochDays (year month day : Nat) : Int

Day count of a date since the Unix epoch (1970-01-01), via Howard Hinnant's days_from_civil algorithm. This transcribes Std.Time.PlainDate.toEpochDay over raw Nat fields, independently of the Std.Time date type.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.OffsetComponents.seconds (o : OffsetComponents) : Int

The offset's signed second count: ± (hh × 3600 + mm × 60). Positive offsets (+hhmm) are east of UTC, so the parser subtracts this to normalize to UTC.

Equations

• o.seconds = if o.negative = true then -(↑o.hours.natOf * 3600 + ↑o.minutes.natOf * 60) else ↑o.hours.natOf * 3600 + ↑o.minutes.natOf * 60

def Cedar.Thm.Datetime.Zone.offsetSeconds : Zone → Int

Signed UTC-normalization seconds contributed by a zone: 0 for the 'Z' marker, and the offset's second count otherwise.

Equations

• Cedar.Thm.Datetime.Zone.utc.offsetSeconds = 0
• (Cedar.Thm.Datetime.Zone.offset o).offsetSeconds = o.seconds

def Cedar.Thm.Datetime.DateComponents.toMillis (d : DateComponents) : Int

Milliseconds-since-epoch value of a well-formed date's midnight UTC.

Equations

• d.toMillis = Cedar.Thm.Datetime.epochDays d.year.natOf d.month.natOf d.day.natOf * 86400000

def Cedar.Thm.Datetime.TimePart.toMillis (tp : TimePart) : Int

Milliseconds-since-epoch value of a datetime's time-bearing tail relative to its date's midnight: the wall-clock time in milliseconds, less the zone offset (converting to UTC), plus the optional fractional-seconds field.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.DatetimeComponents.toMillis (c : DatetimeComponents) : Int

Milliseconds-since-epoch value of a whole datetime: the date's midnight plus the time-bearing tail's contribution (0 for the date-only form).

Equations

• c.toMillis = c.date.toMillis + match c.time with | none => 0 | some tp => tp.toMillis

def Cedar.Thm.Datetime.IsDatetimeValue (str : String) (v : Int) : Prop

v is the value of the datetime literal str: str is the rendering of syntactically and numerically well-formed datetime components, and v is their epoch-millisecond denotation.

The existential supplies the grammar decomposition directly, so this relation does not re-parse the string. It is total on well-formed syntax (wf_iff_exists_value) and single-valued (isDatetimeValue_unique).

Equations

• Cedar.Thm.Datetime.IsDatetimeValue str v = ∃ (components : Cedar.Thm.Datetime.DatetimeComponents), Cedar.Thm.Datetime.DatetimeProduction str components ∧ v = components.toMillis

Canonical serialization

Datetime stores an arbitrary Int64 millisecond value, while the concrete syntax restricts years to 0000 through 9999. Serialization is therefore partial. It always emits the most explicit grammar form, YYYY-MM-DDTHH:mm:ss.SSS±HHMM, using a zero offset when UTC is in range and the smallest minute offset needed at either endpoint. All decimal fields are rendered here rather than through Std.Time's formatter.

def Cedar.Thm.Datetime.MILLIS_PER_DAY : Int

Milliseconds in one day.

Equations

• Cedar.Thm.Datetime.MILLIS_PER_DAY = 86400000

def Cedar.Thm.Datetime.MIN_UTC_MILLIS : Int

Smallest millisecond value whose UTC civil date has a four-digit nonnegative year.

Equations

• Cedar.Thm.Datetime.MIN_UTC_MILLIS = -62167219200000

def Cedar.Thm.Datetime.MAX_UTC_MILLIS : Int

Largest millisecond value whose UTC civil date has a four-digit nonnegative year.

Equations

• Cedar.Thm.Datetime.MAX_UTC_MILLIS = 253402300799999

def Cedar.Thm.Datetime.MAX_OFFSET_MILLIS : Int

Largest legal timezone-offset magnitude, 23:59, in milliseconds.

Equations

• Cedar.Thm.Datetime.MAX_OFFSET_MILLIS = 86340000

def Cedar.Thm.Datetime.MIN_REPRESENTABLE_MILLIS : Int

Exact lower endpoint representable by the datetime grammar.

Equations

• Cedar.Thm.Datetime.MIN_REPRESENTABLE_MILLIS = Cedar.Thm.Datetime.MIN_UTC_MILLIS - Cedar.Thm.Datetime.MAX_OFFSET_MILLIS

def Cedar.Thm.Datetime.MAX_REPRESENTABLE_MILLIS : Int

Exact upper endpoint representable by the datetime grammar.

Equations

• Cedar.Thm.Datetime.MAX_REPRESENTABLE_MILLIS = Cedar.Thm.Datetime.MAX_UTC_MILLIS + Cedar.Thm.Datetime.MAX_OFFSET_MILLIS

def Cedar.Thm.Datetime.fixedWidthNat (width n : Nat) : String

Render a natural number as an ASCII decimal string padded with leading zeroes to width.

Equations

• Cedar.Thm.Datetime.fixedWidthNat width n = String.ofList (List.leftpad width '0' (toString n).toList)

structure Cedar.Thm.Datetime.CanonicalLocalTime : Type

The local millisecond value and explicit offset selected for canonical serialization.

• localMillis : Int
• offsetNegative : Bool
• offsetMinutes : Nat

def Cedar.Thm.Datetime.canonicalLocalTime? (value : Int) : Option CanonicalLocalTime

Select UTC whenever possible. Immediately outside the UTC civil range, select the smallest minute offset that moves the local civil time back into that range.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.canonicalComponents (localTime : CanonicalLocalTime) : DatetimeComponents

Build canonical grammar components from an in-range local millisecond value and its selected explicit offset. PlainDate.ofEpochDay supplies numeric calendar fields only; rendering is performed by fixedWidthNat.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.isFixedDigits (width : Nat) (s : String) : Bool

Executable mirror of IsFixedDigits.

Equations

• Cedar.Thm.Datetime.isFixedDigits width s = ((Cedar.Spec.Ext.toNat?' s).isSome && s.length == width)

def Cedar.Thm.Datetime.DatetimeComponents.syntaxWfB (components : DatetimeComponents) : Bool

Executable mirror of DatetimeComponents.syntaxWf.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.DatetimeComponents.constraintsWfB (components : DatetimeComponents) : Bool

Executable mirror of DatetimeComponents.constraintsWf.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.canonicalComponents? (d : Spec.Ext.Datetime) : Option DatetimeComponents

Produce certified canonical components for a datetime value. The final check is deliberately stated in terms of the owned grammar and value function, insulating serialization from Std.Time formatting behavior.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Datetime.toString? (d : Spec.Ext.Datetime) : Option String

Canonical partial serializer for datetime values. Every successful result has the fixed form YYYY-MM-DDTHH:mm:ss.SSS±HHMM.

Equations

• Cedar.Thm.Datetime.toString? d = Option.map Cedar.Thm.Datetime.DatetimeComponents.asString (Cedar.Thm.Datetime.canonicalComponents? d)

def Cedar.Thm.Datetime.normalize (str : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed inputs (mirror of the decimal and duration normalizers); because serialization is partial the re-serialization is a bind rather than the total map used there.

Equations

• Cedar.Thm.Datetime.normalize str = (Cedar.Spec.Ext.Datetime.parse str).bind Cedar.Thm.Datetime.toString?