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:

• DEX with limit orders and partial matching src docs

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.