Verified Cedar Extension Parsers in Lean 4

2.1. Grammar🔗

The accepted syntax for duration literals is:

grammar
  Duration   ::= ['-'] Components
  Components ::= [Days] [Hours] [Minutes] [Seconds] [Millis]

  Days       ::= Digit⁺ 'd'
  Hours      ::= Digit⁺ 'h'
  Minutes    ::= Digit⁺ 'm'
  Seconds    ::= Digit⁺ 's'
  Millis     ::= Digit⁺ 'ms'
  Digit      ::= '0' | '1' | … | '9'

value
  value(Duration) in milliseconds =
    sign × (d × 86400000 + h × 3600000 + m × 60000
            + s × 1000 + ms)
    where sign        = -1 if '-' is present, else 1
          d, h, m, s, ms = nat value of each component
                           (0 if omitted)

constraints
  - At least one component must be present
  - value(Duration) ∈ [Int64.min, Int64.max]

A string is valid if and only if it satisfies both the grammar and the constraints above.