1. Notation and Conventions🔗

The Gray Paper defines a rich mathematical notation for specifying the JAM protocol. JAR maps these to Lean 4 types as closely as possible (GP §3).

1. 1.1. Optional Substitution
2. 1.2. Exceptional Values
3. 1.3. Dictionaries
4. 1.4. Sequences
5. 1.5. Octet Sequences
6. 1.6. Cryptographic Key Types
7. 1.7. Signature Types