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.

Canonical strings are a special case of well-formed inputs. Their body has all five components present, and the weighted component sum equals the duration's stored value. The maximized representation guarantees that no single component's value exceeds the Int64 range, so the roundtrip never overflows.