Additional Resources
This section contains supplementary information and resources for Ursus development.
FAQ
General Questions
Q: What is Ursus?
A: Ursus is a Coq embedded DSL for writing and verifying smart contracts. See Introduction.
Q: Do I need to know Coq?
A: Basic Coq knowledge helps, but you can start with Quick Start and learn as you go.
Q: Which blockchains does Ursus support?
A: Ursus can extract to Solidity (EVM), C++ (TON), and Rust. See Compilation.
Installation
Q: Which Coq version should I use?
A: Coq 8.16.1 is recommended. See Installation.
Q: Can I use Docker?
A: Yes, Docker images are available. See Installation.
Q: Installation fails with "Cannot find library"
A: Check your _CoqProject paths. See Troubleshooting.
Development
Q: How do I debug my contract?
A: Use Coq's proof mode to inspect goals and context. See Programming Style.
Q: Can I test my contract before deployment?
A: Yes, use QuickChick for property-based testing. See QuickChick.
Q: How do I prove my contract is correct?
A: Write specifications and prove them in Coq. See Verification.
Extraction
Q: How do I generate Solidity code?
A: Set #[translation = on] and #[language = solidity]. See Compilation.
Q: Can I customize the generated code?
A: Limited customization is available through attributes. See Attributes.
Q: The generated code doesn't compile
A: Check Solidity version compatibility and dependencies. See Compiling Solidity.
Glossary
eDSL - Embedded Domain-Specific Language. A language implemented within another language (Coq).
Coq - A proof assistant for formal verification.
Gallina - Coq's specification language.
Tactic - A command that constructs proofs or programs in Coq.
UExpression - Ursus expression type, representing computations.
URValue - Ursus right-value (readable value).
ULValue - Ursus left-value (assignable location).
Monadic - Programming style using monads to handle state and effects.
Extraction - Process of generating executable code from Coq definitions.
QuickChick - Property-based testing framework for Coq.
TVM - TON Virtual Machine.
EVM - Ethereum Virtual Machine.
Common Patterns
Initialization Pattern
Ursus Definition init (initialSupply: uint256): UExpression PhantomType false.
{
::// totalSupply := initialSupply .
::// balances[[msg->sender]] := initialSupply |.
}
return.
Defined.
Validation Pattern
Ursus Definition require (condition: boolean) (message: string): UExpression unit false.
{
::// if !condition then { revert_(message) } |.
}
return.
Defined.
Access Control Pattern
Ursus Definition onlyOwner: UExpression unit false.
{
::// require(msg->sender == owner, "Not owner") |.
}
return.
Defined.
Safe Math Pattern
Ursus Definition safeAdd (a b: uint256): UExpression uint256 false.
{
::// var 'result : uint256 := a + b .
::// require(result >= a, "Overflow") |.
}
return result.
Defined.
Code Style Guide
Naming Conventions
- Contracts: PascalCase (
ERC20,TokenSale) - Functions: camelCase (
transfer,balanceOf) - Variables: camelCase (
totalSupply,senderBalance) - Constants: UPPER_CASE (
MAX_SUPPLY,DECIMALS)
Formatting
(* Good: Clear structure *)
Ursus Definition transfer (to: address) (amount: uint256):
UExpression boolean false.
{
::// var 'senderBalance : uint256 := balances[[msg->sender]] .
::// require(senderBalance >= amount, "Insufficient balance") .
::// balances[[msg->sender]] := senderBalance - amount .
::// balances[[to]] := balances[[to]] + amount |.
}
return @true.
Defined.
Comments
(* Contract-level documentation *)
Contract ERC20 ;
(* Function documentation *)
(* @dev Transfers tokens to recipient
@param to Recipient address
@param amount Amount to transfer
@return Success boolean *)
Ursus Definition transfer (to: address) (amount: uint256):
UExpression boolean false.
Performance Tips
Minimize State Access
(* Good: Read once *)
::// var 'balance : uint256 := balances[[addr]] .
::// balance := balance + {1} .
::// balances[[addr]] := balance |.
(* Bad: Multiple reads *)
::// balances[[addr]] := balances[[addr]] + {1} |.
Use Local Variables
(* Good: Cache in local variable *)
::// var 'sender : address := msg->sender .
::// balances[[sender]] := balances[[sender]] - amount |.
(* Bad: Repeated access *)
::// balances[[msg->sender]] := balances[[msg->sender]] - amount |.
External Resources
Official Documentation
Learning Resources
Community
Related Projects
- ursus-patterns - Example contracts and patterns
- ursus-standard-library - Standard library implementation
- pruvendo-ursus-tvm - TVM-specific functions library
Contact Pruvendo for access to these repositories.
Contributing
Ursus is under active development. For contributions or feedback, contact Pruvendo.
License
Ursus libraries are proprietary. See Installation for access information.