Verified Cedar Extension Parsers in Lean 4

 Verified Cedar Extension Parsers in Lean 4🔗

Cruise Song (Amazon Web Services)

This document specifies Cedar's extension parsers and proves their correctness properties. All theorems are machine-checked in Lean 4.

Contents

  1. 1. Decimal Parsing
  2. 2. Duration Parsing
  3. 3. Datetime Parsing
  4. 4. IP Address Parsing