Datetime parser correctness

Soundness, completeness, and failure characterization

theorem Cedar.Thm.Datetime.wf_iff_exists_value {str : String} : IsWfDatetime str ↔ ∃ (v : Int), IsDatetimeValue str v

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

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

Soundness of Datetime.parse: if parsing succeeds, the grammar assigns the input the returned datetime's value.

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

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

Failure characterization

theorem Cedar.Thm.Datetime.parse_eq_none_iff (str : String) : Spec.Ext.Datetime.parse str = none ↔ ¬IsWfDatetime str

Because the grammar bounds years to four digits and zone offsets to ±23:59, every well-formed datetime value fits in Int64. Parsing therefore rejects exactly malformed strings.

Canonical serialization

theorem Cedar.Thm.Datetime.parse_toString_roundtrip {d : Spec.Ext.Datetime} {str : String} (h : toString? d = some str) : Spec.Ext.Datetime.parse str = some d

parse ∘ toString? roundtrip: every successfully serialized datetime parses back to the original value.

theorem Cedar.Thm.Datetime.toString?_injective {d d' : Spec.Ext.Datetime} {str : String} (h : toString? d = some str) (h' : toString? d' = some str) : d = d'

toString? is injective on the values it serializes: datetimes with the same (defined) canonical string are equal. (Partial-serializer analogue of Decimal/Duration's toString_injective.)

Normalization

theorem Cedar.Thm.Datetime.normalize_eq_iff_parse_eq (s s' : String) (hs : ∀ (d : Spec.Ext.Datetime), Spec.Ext.Datetime.parse s = some d → (toString? d).isSome = true) (hs' : ∀ (d : Spec.Ext.Datetime), Spec.Ext.Datetime.parse s' = some d → (toString? d).isSome = true) : normalize s = normalize s' ↔ Spec.Ext.Datetime.parse s = Spec.Ext.Datetime.parse s'

Equal normal form iff equal parse — normalization decides datetime equality.

Datetime serialization is partial (toString?), so normalize = (parse ·).bind toString? can collapse two distinct parseable-but-unserializable values to the shared none. The forward direction therefore carries a serializability hypothesis on the parsed values; this is exactly what a full serialization-completeness result (parse s = some d → (toString? d).isSome, which needs the Std.Time civil-calendar round-trip) would discharge unconditionally, closing the gap with Decimal/Duration's total-toString versions. The backward direction is unconditional.