Specifications
This section contains the formal specifications and technical documentation for the Ora smart contract language.
Language Specifications
Grammar
Complete BNF and EBNF grammar specifications for the Ora language, including:
- Formal syntax rules
- Operator precedence
- Language constructs
- Reserved keywords
- Memory region annotations
MLIR Integration
Comprehensive documentation of Ora's MLIR lowering system, covering:
- LLVM MLIR integration
- Type mapping strategies
- Memory region semantics
- Expression and statement lowering
- Pass management and optimization
Formal Verification
Z3 SMT solver integration for mathematical proof of contract properties:
- Preconditions and postconditions (
requires,ensures) - Contract and loop invariants
- Quantified expressions (
forall,exists) - Ghost code for specification
- Verification condition generation
API Documentation
Complete API reference for the Ora compiler:
- CLI commands and flags
- Library interfaces
- Compilation pipeline
- Error handling
- Performance benchmarks
State Analysis
Automatic storage access tracking and optimization:
- Function property detection (stateless, readonly, state-modifying)
- Dead store detection (contract-level analysis)
- Missing validation warnings
- Constructor-specific checks
- Gas optimization insights
Implementation Status
Each specification includes implementation status indicators:
- ✅ Complete: Feature is fully implemented and tested (79% success rate - 76/96 examples)
- 🚧 In Progress: Partially implemented, actively being developed
- 📋 Planned: Designed but not yet started
Current Status Summary
| Component | Status | Notes |
|---|---|---|
| Lexer | ✅ Complete | All tokens, trivia support |
| Parser | ✅ Complete | 79% success rate (76/96 examples) |
| Type System | ✅ Complete | Full type checking and validation |
| Semantics | ✅ Complete | Region and error validation |
| MLIR | ✅ Complete | 81 operations, lowering and optimization |
| State Analysis | ✅ Complete | Automatic tracking & warnings |
| Structs | ✅ Complete | Declaration, instantiation, field operations |
| Enums | ✅ Complete | Declaration with explicit values |
| Control Flow | ✅ Complete | if/else, switch statements |
| Arithmetic | ✅ Complete | All operations (add, sub, mul, div, rem, power) |
| Memory Ops | ✅ Complete | mload, mstore, mload8, mstore8 |
| Transient Storage | ✅ Complete | tload, tstore operations |
| Maps | ✅ Complete | Map get/store operations |
| sensei-ir Backend | 🚧 In Progress | Lowering to sensei-ir (SIR) in development |
| For Loops | 🚧 In Progress | Capture syntax in development |
| Error Handling | 🚧 In Progress | Try-catch improvements needed |
| Type Inference | 🚧 In Progress | Currently requires explicit types |
| Standard Lib | 🚧 In Progress | Basic utilities |
| Z3 Verification | 🚧 In Progress | Grammar & AST complete, VC generation in progress |
Contributing
These specifications are living documents that evolve with the language. Contributions are welcome:
- Grammar improvements: Help refine language syntax
- HIR enhancements: Extend the intermediate representation
- Verification advances: Improve formal verification capabilities
- API extensions: Add new compiler features
Quick Navigation
- New to Ora? Start with the Grammar specification
- Writing contracts? Check out State Analysis for automatic optimization
- Formal verification? See the Formal Verification guide for Z3 integration
- Compiler development? Explore MLIR Integration and API docs
- Language implementation? All specifications work together
These specifications provide the foundation for understanding and extending the Ora language.