3.4. Soundness and Completeness🔗

The parser is characterized by the same relational guarantees as the decimal and duration parsers. Datetime.parse delegates to Std.Time.GenericFormat.parse, so the proof layer contains a parser-inversion library that evaluates those combinators once and shows that a successful parse is exactly the rendering of well-formed witnessing components.

Soundness: whenever parsing succeeds, the grammar relation assigns the input exactly the returned datetime's value. By wf_iff_exists_value, this also certifies well-formedness.

theorem

Cedar.Thm.Datetime.parse_sound (str : String) (d : Datetime)
  (h : Datetime.parse str = some d) : IsDatetimeValue str d.val.toInt
Cedar.Thm.Datetime.parse_sound
  (str : String) (d : Datetime)
  (h : Datetime.parse str = some d) :
  IsDatetimeValue str d.val.toInt

Soundness of Datetime.parse: if parsing succeeds, the grammar assigns the input the returned datetime's value.

Completeness is the converse: every string assigned d.val.toInt by the grammar relation is accepted as that datetime.

theorem

Cedar.Thm.Datetime.parse_complete (str : String) (d : Datetime)
  (hval : IsDatetimeValue str d.val.toInt) : Datetime.parse str = some d
Cedar.Thm.Datetime.parse_complete
  (str : String) (d : Datetime)
  (hval :
    IsDatetimeValue str d.val.toInt) :
  Datetime.parse str = some d

Completeness of Datetime.parse: if the grammar assigns a string the value d.val.toInt, then parsing accepts the string as d.

Together they give an exact success characterization:

theorem

Cedar.Thm.Datetime.parse_eq_some_iff_isDatetimeValue (str : String)
  (d : Datetime) :
  Datetime.parse str = some d ↔ IsDatetimeValue str d.val.toInt
Cedar.Thm.Datetime.parse_eq_some_iff_isDatetimeValue
  (str : String) (d : Datetime) :
  Datetime.parse str = some d ↔
    IsDatetimeValue str d.val.toInt

Exact parser characterization derived from soundness and completeness: parsing succeeds with d precisely when the declarative grammar relation assigns the input the value d.val.toInt.

The grammar's range bound lies well inside Int64, so unlike decimal and duration there is no overflow failure case: parsing rejects exactly the malformed strings.

theorem

Cedar.Thm.Datetime.parse_eq_none_iff (str : String) :
  Datetime.parse str = none ↔ ¬IsWfDatetime str
Cedar.Thm.Datetime.parse_eq_none_iff
  (str : String) :
  Datetime.parse str = none ↔
    ¬IsWfDatetime str

Because the grammar bounds years to four digits and zone offsets to ±23:59, every well-formed datetime value fits in Int64. Parsing therefore rejects exactly malformed strings.