Verified Cedar Extension Parsers in Lean 4

2. Duration Parsing🔗

Cedar durations are measured in milliseconds, stored as an Int64. A duration literal is a signed sequence of unit-tagged components — days, hours, minutes, seconds, and milliseconds — printed from the largest unit to the smallest. For example, 1d2h30m denotes one day, two hours, and thirty minutes.

  1. 2.1. Grammar
  2. 2.2. Formal Specification
  3. 2.3. Parser
  4. 2.4. Soundness and Completeness
  5. 2.5. Canonical String Representation
  6. 2.6. Roundtrip Theorem