Advanced Topics

This section covers advanced features and internals of Ursus for expert users. These topics require deep understanding of Coq, formal verification, and the Ursus architecture.

Overview

The advanced topics include:

Ledger Model - Understanding the blockchain state model
Specification Language - Advanced specification techniques
Proof Kinds - Different types of proofs in Ursus
Code Generator - How code generation works
Elpi Integration - Using Elpi for metaprogramming

Who Should Read This

This section is for:

✅ Researchers working on formal verification
✅ Contributors to Ursus development
✅ Advanced users implementing custom features
✅ Those interested in Ursus internals

Prerequisites

Before diving into advanced topics, you should:

✅ Master all basic Ursus features
✅ Complete the Long Start tutorial
✅ Understand Coq proof tactics
✅ Be familiar with formal verification concepts

Topics

Ledger Model

The ledger model defines how blockchain state is represented and manipulated in Ursus:

State representation
Ledger types and classes
State transitions
Execution model
Gas and resources

Specification Language

Advanced specification techniques for complex contracts:

Temporal logic specifications
Invariant composition
Refinement relations
Simulation proofs
Abstraction techniques

Proof Kinds

Different approaches to proving contract correctness:

Direct proofs
Inductive proofs
Simulation proofs
Refinement proofs
Automated proof strategies

Code Generator

Understanding how Ursus generates target language code:

AST transformation
Code generation pipeline
Optimization passes
Target language specifics
Extending the generator

Elpi Integration

Using Elpi for metaprogramming and automation:

Elpi basics
Ursus Elpi predicates
Custom tactics
Code generation
Proof automation

Verification - Verification principles
Long Start - Complete tutorial
Programming Style - Development techniques

Contributing

If you're working on Ursus internals:

Check the solidity-monadic-language repository (contact Pruvendo for access)
Review existing proofs in ursus-patterns
Contact Pruvendo team to join development discussions

Resources

Coq Reference Manual: https://coq.inria.fr/refman/
Elpi Documentation: https://lpcic.github.io/coq-elpi/
Ursus Source Code: Contact Pruvendo for repository access

Note

⚠️ Work in Progress: This section is under active development. Some topics may be incomplete or subject to change as Ursus evolves.

URSUS language Documentation