JAR: JAM Axiomatic Reference

 JAR: JAM Axiomatic Reference🔗

JAR Contributors

JAR (JAM Axiomatic Reference) is a Lean 4 formalization of the JAM blockchain protocol as specified in the Gray Paper v0.7.2.

Each chapter corresponds to a section of the Gray Paper, presenting the formal Lean definitions alongside explanatory prose.

Contents

  1. 1. Notation and Conventions
  2. 2. Numeric Types
  3. 3. Protocol Constants
  4. 4. Type Definitions
  5. 5. Cryptographic Primitives
  6. 6. Safrole Consensus
  7. 7. State Transition
  8. 8. Service Invocations
  9. 9. Polkadot Virtual Machine
  10. 10. Accumulation
  11. 11. Serialization Codec
  12. 12. Merkle Structures
  13. 13. Erasure Coding