Installing Pruvendo Libraries
Pruvendo libraries provide the Ursus language and verification tools.
Prerequisites
Make sure you have:
Ursus Libraries
The Ursus ecosystem consists of several libraries:
Core Libraries
coq-elpi-mod
- Modified Coq Elpi framework (based on LPCIC/coq-elpi)
- Enables code generation and automation
pruvendo-base
- Core primitive datatypes
- Monadic representation foundation
pruvendo-umlang
- The Ursus language itself
- Eval/Exec generators
- Formally verified semantics
Standard Libraries
pruvendo-base-lib
- Facts about primitive types
- Basic operations and proofs
ursus-standard-library
- Standard functions (integers, collections)
- Operators and notations
- See Standard Library
pruvendo-ursus-tvm
- Blockchain and VM abstractions
- State representation
- TVM-specific operations
- See TVM Library
Development Tools
ursus-contract-creator
- Elpi-based automation
- Contract scaffolding
- Proof code generation
ursus-proofs
- Proof automation helpers
- Common tactics
ursus-quickchick
- QuickChick integration for property-based testing
- Automated test generation
- See QuickChick Guide
ursus-environment
- Unified import interface
- Exports all Ursus resources
Installation
Option 1: Docker (Recommended)
Use pre-built Docker image:
docker pull pruvendo/ursus:latest
docker run -it pruvendo/ursus:latest
Option 2: From Source (NDA Required)
Contact Pruvendo for access:
# Clone repositories (requires access from Pruvendo)
git clone <ursus-repository-url>
cd ursus
# Install dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect
# Build and install
make -j4
make install
Verify Installation
Create a test file test.v:
Require Import UrsusEnvironment.
Contract Test ;
Sends To ;
Types ;
Constants ;
Record Contract := {
value: uint256
}.
Ursus Definition getValue: UExpression uint256 false.
{
::// _result := value |.
}
return.
Defined.
Compile it:
coqc -Q . Ursus test.v
# Should compile without errors
Distribution Status
Current availability:
- Closed source development
- Source code shared under NDA
- Docker images available for evaluation
- Contact: Pruvendo
Disclaimer
Ursus libraries are under active development. No warranties are provided. We welcome collaboration and feedback.
Next Steps
Installation complete! Now:
- Quick Start - Write your first contract
- Ursus Language - Learn the language
- Examples - Browse ursus-patterns repository for examples
Getting Help
- Issues: Contact Pruvendo support
- Documentation: This guide
- Examples: Check ursus-patterns repository