Verified Cedar Extension Parsers in Lean 4

1. Decimal Parsing🔗

Cedar decimals use a fixed-point representation over Int64, with a scale factor of 10⁴ (4 digits after the decimal point). For example, the value 1.2345 is stored as the integer 12345.

  1. 1.1. Grammar
  2. 1.2. Formal Specification
  3. 1.3. Parser
  4. 1.4. Soundness and Completeness
  5. 1.5. Canonical String Representation
  6. 1.6. Roundtrip Theorem