Verified Cedar Extension Parsers in Lean 4

2.6. Roundtrip Theorem🔗

Parsing the canonical string representation of any duration recovers the original value. This is the headline user-facing property — parse and toString are mutually inverse on durations — and it is what underpins toString_injective above.

🔗theorem
Cedar.Thm.Duration.parse_toString_roundtrip
  (d : Cedar.Spec.Ext.Datetime.Duration) :
  Cedar.Spec.Ext.Datetime.Duration.parse d.toString = some d
Cedar.Thm.Duration.parse_toString_roundtrip
  (d : Cedar.Spec.Ext.Datetime.Duration) :
  Cedar.Spec.Ext.Datetime.Duration.parse
      d.toString =
    some d

parse ∘ toString roundtrip: parsing the string representation recovers the original.

It is a direct corollary of completeness: canonical strings are just a special case of well-formed inputs. The canonical body always has all five components present (so it is trivially nonempty), and its computed value equals the duration's stored value, so parse_complete applies. The maximized representation guarantees that no single component's value ever exceeds the Int64 range, so the roundtrip never overflows.