Verified Cedar Extension Parsers in Lean 4

2.2. Formal Specification🔗

Following the same declarative structure as the decimal specification, we separate four ideas: DurationProduction relates a rendering to its grammar components, IsWfDuration hides those components existentially, value gives their denotation, and IsDurationValue str v combines the production with that denotation. Cedar already has the executable Duration.parse, so the public grammar does not define a second operational string decoder.

The building block is again IsDigits, the shared Digit⁺ predicate introduced in the Decimal Parsing chapter.

Each of the five components is optional. IsWfOptionalQuantity lifts IsDigits to optional strings — an absent component (none) is trivially valid, and a present one must be a non-empty digit string:

public def IsWfOptionalQuantity : Option String → Prop | none => True | some digits => IsDigits digits

A Components record holds the five optional digit strings, one per time unit:

public structure Components where days : Option String hours : Option String minutes : Option String seconds : Option String milliseconds : Option String

Two predicates constrain a record. nonempty enforces that at least one component is present — the body cannot be empty:

public def Components.nonempty (components : Components) : Prop := components.days ≠ none ∨ components.hours ≠ none ∨ components.minutes ≠ none ∨ components.seconds ≠ none ∨ components.milliseconds ≠ none

quantitiesWf enforces that every present component is a valid digit quantity:

public def Components.quantitiesWf (components : Components) : Prop := IsWfOptionalQuantity components.days ∧ IsWfOptionalQuantity components.hours ∧ IsWfOptionalQuantity components.minutes ∧ IsWfOptionalQuantity components.seconds ∧ IsWfOptionalQuantity components.milliseconds

asString renders a record back to a string by concatenating the present components in order d h m s ms, each absent component contributing "". This is what ties the abstract record to the concrete grammar's largest-to-smallest ordering:

public def Components.asString (components : Components) : String := durationChunk components.days "d" ++ durationChunk components.hours "h" ++ durationChunk components.minutes "m" ++ durationChunk components.seconds "s" ++ durationChunk components.milliseconds "ms"

A body is well-formed exactly when it is the rendering of some record that is both nonempty and has valid quantities. Phrasing well-formedness existentially over asString bakes the ordering constraint in for free: a string is well-formed only if it can be produced by concatenating components in the canonical order, so out-of-order strings have no witnessing record:

public def IsWfBody (body : String) : Prop := ∃ components : Components, components.nonempty ∧ components.quantitiesWf ∧ body = components.asString

The whole-string production combines that record with the optional leading '-'. The sign is its own production, Sign ::= ['-'], and reuses the shared IsWfSign predicate from the Decimal Parsing chapter:

public def DurationProduction (str sign : String) (components : Components) : Prop := str = sign ++ components.asString ∧ IsWfSign sign ∧ components.nonempty ∧ components.quantitiesWf

A duration string is well-formed exactly when some sign and component record witness that production:

public def IsWfDuration (str : String) : Prop := ∃ sign components, DurationProduction str sign components

The component record also gives a direct value formula. optionalNatOf interprets an absent quantity as zero and a present quantity through the shared natOf reader:

public def optionalNatOf : Option String → Nat | none => 0 | some digits => natOf digits

toMillis is then the grammar's unsigned weighted sum:

public def Components.toMillis (components : Components) : Int := (optionalNatOf components.days : Int) * MILLISECONDS_PER_DAY + (optionalNatOf components.hours : Int) * MILLISECONDS_PER_HOUR + (optionalNatOf components.minutes : Int) * MILLISECONDS_PER_MINUTE + (optionalNatOf components.seconds : Int) * MILLISECONDS_PER_SECOND + optionalNatOf components.milliseconds

The complete value formula applies the captured sign:

public def value (sign : String) (components : Components) : Int := signOf sign * components.toMillis

Finally, the relational specification extends the same grammar witnesses with their denotation:

public def IsDurationValue (str : String) (v : Int) : Prop := ∃ sign components, DurationProduction str sign components ∧ v = value sign components

The existential supplies the decomposition, so the public value specification never has to peel suffixes or represent malformed intermediate states with Option. The proof layer privately relates the parser's right-to-left extraction to this weighted sum once.

As with decimal, the syntax and value views agree: every well-formed rendering has a value, and every value witness contains a well-formed rendering.

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

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

Although the value specification is relational, it is still single-valued: every witness for the same string yields the same integer, including values outside the parser's Int64 range.

🔗theorem
Cedar.Thm.Duration.isDurationValue_unique {str : String} {v₁ v₂ : Int}
  (h₁ : IsDurationValue str v₁) (h₂ : IsDurationValue str v₂) : v₁ = v₂
Cedar.Thm.Duration.isDurationValue_unique
  {str : String} {v₁ v₂ : Int}
  (h₁ : IsDurationValue str v₁)
  (h₂ : IsDurationValue str v₂) : v₁ = v₂

The declarative value relation is single-valued: a duration string denotes at most one integer, including when that integer lies outside the parser's Int64 range.