3.4. Soundness and Completeness🔗

The parser is characterized by the same two guarantees as the decimal and duration parsers, stated against IsWfDatetime and computeValue. Those two are hand-written and reasoned about directly; Datetime.parse instead delegates to Std.Time.GenericFormat.parse. The extra work is a parser-inversion library that evaluates Std.Time's combinator parsers once and shows a successful parse is exactly the rendering of well-formed witnessing components — reducing both proofs to reasoning about components rather than the parser's recursion.

Soundness: whenever parsing succeeds, the input is well-formed and computeValue yields exactly the returned datetime's value.

theorem

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

Soundness of Datetime.parse: if parsing succeeds, then the input is well-formed and computeValue yields exactly the returned datetime's value. (The value is in Int64 range automatically, since it equals d.val.toInt for d.val : Int64.)

Idea: read the successful parse backwards to recover the witnessing components, which are well-formed by construction — that gives IsWfDatetime. Both the parser and computeValue then evaluate those same components with the same value formula, so the value the parser returned is exactly the one computeValue computes.

Completeness is the converse: every well-formed string whose computed value is some d.val.toInt is accepted as that datetime.

theorem

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

Completeness of Datetime.parse: if a string is well-formed and its computed value matches d.val.toInt, then parsing accepts the string as d.

Idea: well-formedness gives witnessing components whose rendering is the input. On such a rendering every guard passes (a well-formed time can't spell a leap second, the fixed widths satisfy the length check, the offset is grammar-bounded) and the Std.Time parse succeeds with the components' value. That value is d's, so parsing lands on d.

Together they characterize failure completely — the parser rejects exactly the strings that are malformed or whose computed value overflows Int64:

theorem

Cedar.Thm.Datetime.parse_eq_none_iff (str : String) :
  Datetime.parse str = none ↔
    ¬IsWfDatetime str ∨
      ∃ v, computeValue str = some v ∧ (v < Int64.MIN ∨ v > Int64.MAX)
Cedar.Thm.Datetime.parse_eq_none_iff
  (str : String) :
  Datetime.parse str = none ↔
    ¬IsWfDatetime str ∨
      ∃ v,
        computeValue str = some v ∧
          (v < Int64.MIN ∨ v > Int64.MAX)

Failure characterization for Datetime.parse: parsing rejects exactly strings that are not well-formed or whose computed value overflows the Int64 range.

Idea: the Option contrapositive of soundness and completeness, with no Std.Time reasoning of its own. If parsing fails yet the string is well-formed, its value must be out of range — otherwise completeness would have accepted it. Conversely a successful parse is well-formed with an in-range value (it is stored in an Int64), so it can meet neither failure clause.

For datetimes the overflow branch is vacuous: the grammar's range bound (from the Grammar section) lies well inside Int64, so the characterization sharpens to reject exactly the malformed strings:

theorem

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

Sharpened failure characterization: because the grammar bounds years to four digits and zone offsets to ±23:59, a well-formed datetime's value always fits in Int64, so the overflow branch of parse_eq_none_iff is vacuous and parsing rejects exactly the malformed strings.

Idea: take the previous characterization and discharge its overflow disjunct using the proven range bound on well-formed values.