Verified Cedar Extension Parsers in Lean 4

1.1. Grammar🔗

The accepted syntax for decimal literals is:

grammar
  Decimal  ::= Sign Natural '.' Fraction
  Sign     ::= ['-']
  Natural  ::= Digit⁺
  Fraction ::= Digit{1,4}
  Digit    ::= '0' | '1' | … | '9'

value
  value(Decimal) =
    sign × (nat(Natural) × 10⁴
            + nat(Fraction) × 10^(4 - |Fraction|))
    where sign   = -1 if Sign is '-', else 1
          nat(s) = natural number value of s (e.g., nat("03") = 3)
          |s|    = length of s

constraints
  value(Decimal) ∈ [Int64.min, Int64.max]

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