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 input was genuinely valid: it is well-formed and computeValue yields exactly the returned decimal's value. (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) :
  IsWfDecimal s ∧ computeValue s = some (Int64.toInt d)
Cedar.Thm.Decimal.parse_sound (s : String)
  (d : Cedar.Spec.Ext.Decimal)
  (h :
    Cedar.Spec.Ext.Decimal.parse s =
      some d) :
  IsWfDecimal s ∧
    computeValue s = some (Int64.toInt d)

Soundness of Decimal.parse: if parsing succeeds, then the input is well-formed and its computed 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 well-formed string whose computed value is some 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) (hwf : IsWfDecimal s)
  (hval : computeValue s = some (Int64.toInt d)) :
  Cedar.Spec.Ext.Decimal.parse s = some d
Cedar.Thm.Decimal.parse_complete
  (s : String)
  (d : Cedar.Spec.Ext.Decimal)
  (hwf : IsWfDecimal s)
  (hval :
    computeValue s =
      some (Int64.toInt d)) :
  Cedar.Spec.Ext.Decimal.parse s = some d

Completeness of Decimal.parse: if a string is well-formed and its computed value matches d.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.Decimal.parse_eq_none_iff (s : String) :
  Cedar.Spec.Ext.Decimal.parse s = none ↔
    ¬IsWfDecimal s ∨
      ∃ v, computeValue s = some 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,
        computeValue s = some v ∧
          (v < Int64.MIN ∨ v > Int64.MAX)

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