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 grammar assigns the input exactly the returned duration's value. The preceding wf_iff_exists_value theorem makes explicit that any such value witness contains a well-formed rendering. (The range constraint is implicit — d.val.toInt is always in Int64 range.)

theorem

Cedar.Thm.Duration.parse_sound (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration)
  (h : Cedar.Spec.Ext.Datetime.Duration.parse str = some d) :
  IsDurationValue str 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) :
  IsDurationValue str d.val.toInt

Soundness of Duration.parse: if parsing succeeds, the declarative grammar relation assigns the input exactly the returned duration's value.

Completeness is the converse: every string the grammar assigns the value d.val.toInt is accepted as that duration.

theorem

Cedar.Thm.Duration.parse_complete (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration)
  (hval : IsDurationValue str 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)
  (hval :
    IsDurationValue str d.val.toInt) :
  Cedar.Spec.Ext.Datetime.Duration.parse
      str =
    some d

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

Together, soundness and completeness give a direct equivalence between the executable parser and the declarative relation:

theorem

Cedar.Thm.Duration.parse_eq_some_iff_isDurationValue (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration) :
  Cedar.Spec.Ext.Datetime.Duration.parse str = some d ↔
    IsDurationValue str d.val.toInt
Cedar.Thm.Duration.parse_eq_some_iff_isDurationValue
  (str : String)
  (d : Cedar.Spec.Ext.Datetime.Duration) :
  Cedar.Spec.Ext.Datetime.Duration.parse
        str =
      some d ↔
    IsDurationValue str d.val.toInt

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

They also give a complete characterization of parsing failure — the parser rejects exactly malformed strings and well-formed strings whose 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, IsDurationValue str 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,
        IsDurationValue str v ∧
          (v < Int64.MIN ∨ v > Int64.MAX)

Failure characterization for Duration.parse: parsing rejects exactly malformed strings and well-formed strings whose grammar value overflows the Int64 range.