Duration parser theorem surface.

parse_sound and parse_complete characterize successful parsing against the declarative IsDurationValue relation. parse_eq_none_iff characterizes exactly when parsing rejects.

theorem Cedar.Thm.Duration.wf_iff_exists_value {str : String} : IsWfDuration str ↔ ∃ (v : Int), IsDurationValue str v

Well-formed duration syntax is exactly syntax to which the grammar assigns some value.

theorem Cedar.Thm.Duration.parse_complete (str : String) (d : Spec.Ext.Datetime.Duration) (hval : IsDurationValue str d.val.toInt) : Spec.Ext.Datetime.Duration.parse str = some d

Completeness of Duration.parse: if the grammar assigns str the value d.val.toInt, then parsing accepts the string as d.

theorem Cedar.Thm.Duration.parse_sound (str : String) (d : Spec.Ext.Datetime.Duration) (h : Spec.Ext.Datetime.Duration.parse str = some d) : IsDurationValue str d.val.toInt

Soundness of Duration.parse: if parsing succeeds, the declarative grammar relation assigns the input exactly the returned duration's value.

theorem Cedar.Thm.Duration.parse_eq_some_iff_isDurationValue (str : String) (d : Spec.Ext.Datetime.Duration) : Spec.Ext.Datetime.Duration.parse str = some d ↔ IsDurationValue str d.val.toInt

Exact parser characterization: parsing succeeds with d precisely when the declarative grammar relation assigns the input the value d.val.toInt.

theorem Cedar.Thm.Duration.parse_eq_none_iff (str : String) : Spec.Ext.Datetime.Duration.parse str = none ↔ ¬IsWfDuration str ∨ ∃ (v : Int), IsDurationValue str v ∧ (v < Int64.MIN ∨ v > Int64.MAX)

Failure characterization for Duration.parse: parsing rejects exactly malformed strings and well-formed strings whose grammar value overflows the Int64 range.

theorem Cedar.Thm.Duration.parse_neg (s : String) (d : Spec.Ext.Datetime.Duration) (hpos : ¬s.startsWith "-" = true) (h : Spec.Ext.Datetime.Duration.parse s = some d) : Spec.Ext.Datetime.Duration.parse ("-" ++ s) = Spec.Ext.Datetime.duration? (-d.val.toInt)

Parsing a negated duration string negates the underlying value.

theorem Cedar.Thm.Duration.offset_durationSince_inverse (dt : Spec.Ext.Datetime) (dur : Spec.Ext.Datetime.Duration) (dt' : Spec.Ext.Datetime) (h : dt.offset dur = some dt') : dt'.durationSince dt = some dur

offset and durationSince are inverses: adding a duration then computing the difference gives back the same duration.

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

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

theorem Cedar.Thm.Duration.toString_injective (d d' : Spec.Ext.Datetime.Duration) (h : d.toString = d'.toString) : d = d'

toString is injective: distinct durations produce distinct strings.

theorem Cedar.Thm.Duration.normalize_eq_iff_parse_eq (s s' : String) : normalize s = normalize s' ↔ Spec.Ext.Datetime.Duration.parse s = Spec.Ext.Datetime.Duration.parse s'

Equal normal form iff equal value: normalization decides duration equality.