3.1. Grammar🔗

The accepted syntax for datetime literals is:

grammar
  Datetime ::= Date
             | Date 'T' Time 'Z'
             | Date 'T' Time '.' SSS 'Z'
             | Date 'T' Time Offset
             | Date 'T' Time '.' SSS Offset

  Date     ::= YYYY '-' MM '-' DD
  Time     ::= hh ':' mm ':' ss
  SSS      ::= Digit{3}
  Offset   ::= ('+' | '-') hh mm
  YYYY     ::= Digit{4}
  MM       ::= Digit{2}
  DD       ::= Digit{2}
  hh       ::= Digit{2}
  mm       ::= Digit{2}
  ss       ::= Digit{2}
  Digit    ::= '0' | '1' | … | '9'

value
  value(Datetime) in milliseconds =
    epochDays(YYYY, MM, DD) × 86400000
    + (hh × 3600 + mm × 60 + ss - offsetSeconds) × 1000 + nat(SSS)
    where epochDays     = civil-calendar days since 1970-01-01
          offsetSeconds = 0 for 'Z'; ± (hh × 3600 + mm × 60) of the
                          Offset otherwise (+ is east of UTC)
          time fields   = 0 when the date-only form omits them

constraints
  - 01 ≤ MM ≤ 12
  - 01 ≤ DD ≤ daysInMonth(YYYY, MM)
  - 00 ≤ hh ≤ 23
  - 00 ≤ mm ≤ 59
  - 00 ≤ ss ≤ 59
  - value(Datetime) ∈ [Int64.min, Int64.max]   -- implied; see below

  daysInMonth(y, m) =
    30  if m ∈ {4, 6, 9, 11}
    28  if m = 2 ∧ ¬isLeapYear(y)
    29  if m = 2 ∧ isLeapYear(y)
    31  otherwise

  isLeapYear(y) =
    (4 | y) ∧ (¬(100 | y) ∨ (400 | y))

A datetime string is valid if and only if it satisfies the grammar and constraints above.

Like decimal and duration, a datetime is stored over Int64, so its value formally carries the constraint value(Datetime) ∈ [Int64.min, Int64.max]. Here the syntax already forces it: the 4-digit year and ±23:59 offset confine every valid string to the range 0000-01-01T00:00:00+2359 … 9999-12-31T23:59:59.999-2359 — values -62167305540000 to 253402387139999 ms, well inside Int64. We prove this bound (toMillis_int64_range), so the constraint is implied rather than separately checked; its payoff, a failure characterization with no overflow case, appears in Soundness and Completeness.

Values beyond this range are still reachable — the datetime.offset(duration) operator can shift a parsed instant anywhere in Int64 — they simply have no literal.

Note. The offset operator is distinct from the grammar's Offset nonterminal (the ±hhmm timezone suffix of a literal, consumed during parsing to normalize the instant to UTC); the Cedar documentation uses the one word for both.