1.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 decimal'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.toInt is always in Int64 range, since d is an Int64.)

theorem

Cedar.Thm.Decimal.parse_sound (s : String) (d : Cedar.Spec.Ext.Decimal)
  (h : Cedar.Spec.Ext.Decimal.parse s = some d) :
  IsDecimalValue s (Int64.toInt d)
Cedar.Thm.Decimal.parse_sound (s : String)
  (d : Cedar.Spec.Ext.Decimal)
  (h :
    Cedar.Spec.Ext.Decimal.parse s =
      some d) :
  IsDecimalValue s (Int64.toInt d)

Soundness of Decimal.parse: if parsing succeeds, then the input is a well-formed rendering whose grammar value is exactly the returned decimal's value. (The value is automatically in Int64 range, since d : Decimal = Int64, so no range conjunct is stated.)

Completeness is the converse: every string the grammar assigns the value d.toInt is accepted as that decimal. (Again the range constraint is implicit — d.toInt is always in range.)

theorem

Cedar.Thm.Decimal.parse_complete (s : String)
  (d : Cedar.Spec.Ext.Decimal)
  (hval : IsDecimalValue s (Int64.toInt d)) :
  Cedar.Spec.Ext.Decimal.parse s = some d
Cedar.Thm.Decimal.parse_complete
  (s : String)
  (d : Cedar.Spec.Ext.Decimal)
  (hval :
    IsDecimalValue s (Int64.toInt d)) :
  Cedar.Spec.Ext.Decimal.parse s = some d

Completeness of Decimal.parse: if the grammar assigns s the value d.toInt, then parsing accepts the string as d. Well-formedness is not a separate hypothesis — IsDecimalValue already asserts that s is a rendering of the grammar's productions.

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

theorem

Cedar.Thm.Decimal.parse_eq_some_iff_isDecimalValue (s : String)
  (d : Cedar.Spec.Ext.Decimal) :
  Cedar.Spec.Ext.Decimal.parse s = some d ↔
    IsDecimalValue s (Int64.toInt d)
Cedar.Thm.Decimal.parse_eq_some_iff_isDecimalValue
  (s : String)
  (d : Cedar.Spec.Ext.Decimal) :
  Cedar.Spec.Ext.Decimal.parse s =
      some d ↔
    IsDecimalValue s (Int64.toInt d)

Exact parser characterization: parsing succeeds with d precisely when the declarative grammar relation assigns the input the value d.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.Decimal.parse_eq_none_iff (s : String) :
  Cedar.Spec.Ext.Decimal.parse s = none ↔
    ¬IsWfDecimal s ∨
      ∃ v, IsDecimalValue s v ∧ (v < Int64.MIN ∨ v > Int64.MAX)
Cedar.Thm.Decimal.parse_eq_none_iff
  (s : String) :
  Cedar.Spec.Ext.Decimal.parse s = none ↔
    ¬IsWfDecimal s ∨
      ∃ v,
        IsDecimalValue s v ∧
          (v < Int64.MIN ∨ v > Int64.MAX)

Failure characterization for Decimal.parse: parsing rejects exactly malformed strings and well-formed strings whose grammar value overflows the Int64 range. The value relation is total on well-formed syntax, so these cases are exhaustive and mutually exclusive.