2.4. Soundness and Completeness🔗

The parser is characterized by two complementary guarantees stated in terms of the previous formal definitions.

Soundness says that whenever parsing succeeds, the input was genuinely valid: it is well-formed and computeValue yields exactly the returned duration's value. (The range constraint is implicit — d.val.toInt is always in Int64 range, since d.val is an Int64.)

theorem

Cedar.Thm.Duration.parse_sound (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration)
  (h : Cedar.Spec.Ext.Datetime.Duration.parse str = some d) :
  IsWfDuration str ∧ computeValue str = some d.val.toInt
Cedar.Thm.Duration.parse_sound
  (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration)
  (h :
    Cedar.Spec.Ext.Datetime.Duration.parse
        str =
      some d) :
  IsWfDuration str ∧
    computeValue str = some d.val.toInt

Soundness of Duration.parse: if parsing succeeds, then the input is well-formed and computeValue yields exactly the returned duration's value. (The value is automatically in Int64 range, since d.val : Int64, so no range conjunct is stated.)

Completeness is the converse: every well-formed string whose computed value is some d.val.toInt is accepted as that duration. (Again the range constraint is implicit — d.val.toInt is always in range.)

theorem

Cedar.Thm.Duration.parse_complete (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration) (hwf : IsWfDuration str)
  (hval : computeValue str = some d.val.toInt) :
  Cedar.Spec.Ext.Datetime.Duration.parse str = some d
Cedar.Thm.Duration.parse_complete
  (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration)
  (hwf : IsWfDuration str)
  (hval :
    computeValue str = some d.val.toInt) :
  Cedar.Spec.Ext.Datetime.Duration.parse
      str =
    some d

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

Together they also give a complete characterization of parsing failure — the parser rejects exactly those strings that are malformed or whose computed value overflows the Int64 range:

theorem

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

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