1.6. Roundtrip Theorem🔗

Parsing the canonical string representation of any decimal recovers the original value.

theorem

Cedar.Thm.Decimal.parse_toString_roundtrip
  (d : Cedar.Spec.Ext.Decimal) :
  Cedar.Spec.Ext.Decimal.parse (toString d) = some d
Cedar.Thm.Decimal.parse_toString_roundtrip
  (d : Cedar.Spec.Ext.Decimal) :
  Cedar.Spec.Ext.Decimal.parse
      (toString d) =
    some d

Parsing the canonical string representation of a decimal returns the same decimal.

It is a direct corollary of completeness: canonical strings are just a special case of well-formed inputs, so we only need to check that toString d is well-formed and that its computed value is d.toInt, then hand both to parse_complete.

theorem

Cedar.Thm.Decimal.toString_isWfDecimal (d : Cedar.Spec.Ext.Decimal) :
  IsWfDecimal (toString d)
Cedar.Thm.Decimal.toString_isWfDecimal
  (d : Cedar.Spec.Ext.Decimal) :
  IsWfDecimal (toString d)

The string produced by toString d is well-formed for parsing.

theorem

Cedar.Thm.Decimal.computeValue_toString (d : Cedar.Spec.Ext.Decimal) :
  computeValue (toString d) = some (Int64.toInt d)
Cedar.Thm.Decimal.computeValue_toString
  (d : Cedar.Spec.Ext.Decimal) :
  computeValue (toString d) =
    some (Int64.toInt d)

The canonical string representation of a decimal encodes the same integer value.

Though only a corollary, roundtrip guards against parser bugs on valid inputs — cases soundness and the failure characterization, aimed at rejecting invalid inputs, never exercise. For example, every decimal in (-1, 0) serializes to a -0.xxxx string (value -5000 becomes "-0.5000"), so roundtrip must parse these back exactly. An earlier parser derived the sign from the integer part's value, where int("-0") = 0 dropped the negative and turned -0.5000 into +0.5000. The existence of such a bug would have violated the roundtrip property; in other words, the proof we now have rules it out.