Ergo Contracts
Source code of the Ergo smart contracts with compilation, testing, and formal verification tooling.
List of contracts:
Certified(ErgoScala):
- Assets Atomic Exchange src , verified properties
- Crowd Funding src, verified properties
- ICO Funding src, verified properties
ErgoScript:
How to add a new certified contract
Certified contracts are written in ErgoScala (a subset of Scala, compiled with ErgoScala compiler) and have their properties verified using formal verification with Stainless.
Prerequisites for certified contracts:
- Install Z3 SMT solver from https://github.com/Z3Prover/z3
Create a method for the contract
Subclass SigmaContract
in the verified-contracts
project and put a contract code in a method. The first parameter has to be ctx: Context
, and subsequent parameters may be contract parameters. The return value has to be SigmaProp
. Make the first line of the contract code import ctx._
to improve readability.
Write contract code in the method.
See DEX buy order for an example.
Contract compilation (ErgoScala)
Create a subclass (object) of the class with contract code to make an "instance" method to compile the contract's code.
It'll invoke the compiler (macros) and returns a compiled contract with embedded contract parameters. Create a method with parameters from the contract (without the Context
parameter) and invoke ErgoContractCompiler.compile
. See DEX buy order for an example.
Mark this method with @ignore
annotation to hide it from Stainless.
How to use compiled contract
Call the "instance" method in another module/project, and it'll return 'ErgoContract'(compiled contract).
Call ErgoContract.scalaFunc
to run the contract with given Context
. See DEX buy order for an example.
Verifying contract properties
Verification is done using Stainless. Create a subclass(object) of the class where you put contracts (as methods). Use a method for each property you want to verify. Put pre-conditions in require()
call, call the contract, and verify post-conditions. See DEX buy order verified properties for an example.