Source code of the Ergo smart contracts with compilation, testing, and formal verification tooling.
List of contracts:
- Assets Atomic Exchange src , verified properties
- Crowd Funding src, verified properties
- ICO Funding src, verified properties
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
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).
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.