3.2. Formal Specification🔗

As in the decimal and duration specifications, we separate productions, well-formedness, component denotation, and the relation between a string and its value. DatetimeProduction relates a rendering to its components, IsWfDatetime hides those components existentially, DatetimeComponents.toMillis evaluates them, and IsDatetimeValue str v combines the production with its denotation. The range constraint needs no separate clause because it follows from the grammar.

Every numeric field of this grammar is a digit run of an exact width, so the building block is IsFixedDigits — the Digit{n} refinement of the shared IsDigits predicate (introduced in the Decimal Parsing chapter). It too lives in Cedar.Thm.Data.String:

public def IsFixedDigits (n : Nat) (s : String) : Prop :=
  IsDigits s ∧ s.length = n

Each nonterminal of the grammar becomes a record of its digit fields, with a syntaxWf predicate pinning field widths and a constraintsWf predicate imposing the numeric bounds. For the Date ::= YYYY '-' MM '-' DD production:

public structure DateComponents where
  year : String
  month : String
  day : String

public def DateComponents.syntaxWf (d : DateComponents) : Prop :=
  IsFixedDigits 4 d.year ∧
  IsFixedDigits 2 d.month ∧
  IsFixedDigits 2 d.day

public def DateComponents.constraintsWf (d : DateComponents) : Prop :=
  let mm := natOf d.month
  1 ≤ mm ∧ mm ≤ 12 ∧
  1 ≤ natOf d.day ∧ natOf d.day ≤ daysInMonth (natOf d.year) mm

The month/day bounds refer to daysInMonth and isLeapYear, the two auxiliary grammar functions:

public def daysInMonth (y m : Nat) : Nat :=
  if m == 4 || m == 6 || m == 9 || m == 11 then 30
  else if m == 2 then (if isLeapYear y then 29 else 28)
  else 31

public def isLeapYear (y : Nat) : Bool :=
  y % 4 == 0 && (y % 100 != 0 || y % 400 == 0)

The Time, Offset, and Zone nonterminals are modelled the same way; the time-bearing tail (Time ['.' SSS] Zone) is a TimePart combining a TimeComponents, an optional millisecond field, and a Zone:

public structure TimePart where
  time : TimeComponents
  millis : Option String
  zone : Zone

A datetime is then a Date optionally followed by such a tail. The top-level production relates the complete rendering to a record that is both syntactically well-formed and satisfies the numeric constraints. Using asString here bakes in the separators, field order, and choice among the five top-level forms:

public structure DatetimeComponents where
  date : DateComponents
  time : Option TimePart

public def DatetimeProduction (str : String) (components : DatetimeComponents) : Prop :=
  components.syntaxWf ∧
  components.constraintsWf ∧
  str = components.asString

Well-formedness existentially hides that production's component witness:

public def IsWfDatetime (str : String) : Prop :=
  ∃ components : DatetimeComponents, DatetimeProduction str components

The component denotation evaluates the grammar's value formula directly: days since the epoch (epochDays, the standard civil-calendar day count) scaled to milliseconds, plus the time-of-day, fractional, and zone contributions.

public def DatetimeComponents.toMillis (c : DatetimeComponents) : Int :=
  c.date.toMillis + (match c.time with | none => 0 | some tp => tp.toMillis)

The declarative value relation extends the same well-formed component witness with that denotation. It does not re-parse the string or introduce an Option-valued second decoder:

public def IsDatetimeValue (str : String) (v : Int) : Prop :=
  ∃ components : DatetimeComponents,
    DatetimeProduction str components ∧
    v = components.toMillis

The value relation is total on well-formed syntax and single-valued:

theorem

Cedar.Thm.Datetime.wf_iff_exists_value {str : String} :
  IsWfDatetime str ↔ ∃ v, IsDatetimeValue str v
Cedar.Thm.Datetime.wf_iff_exists_value
  {str : String} :
  IsWfDatetime str ↔
    ∃ v, IsDatetimeValue str v

Well-formed datetime syntax is exactly syntax to which the grammar assigns some value.

theorem

Cedar.Thm.Datetime.isDatetimeValue_unique {str : String} {v₁ v₂ : Int}
  (h₁ : IsDatetimeValue str v₁) (h₂ : IsDatetimeValue str v₂) : v₁ = v₂
Cedar.Thm.Datetime.isDatetimeValue_unique
  {str : String} {v₁ v₂ : Int}
  (h₁ : IsDatetimeValue str v₁)
  (h₂ : IsDatetimeValue str v₂) : v₁ = v₂

The declarative value relation is single-valued: a datetime string denotes at most one epoch-millisecond value.