An implementation of multicollateral dai core

This is an implementation of the multicollateral dai system's core smart contracts.

The contracts are formulated in a simple and concise domain-specific language called Sic.

The sicc compiler translates Sic code to EVM bytecode via Solidity assembly. The compiler code also has the ability to directly interpret Sic code.

We also intend to generate other useful artifacts from Sic code, most importantly:

• documentation,
• formal verification conditions, and
• simulation tools.

This repository will also hold our formal verification process, test suites, and automated testing tools.

Building the contracts

Only two programs are prerequisites for installation: Make and the Nix package manager. The following command will build and test the contracts, leaving artifacts in ./out:

make dai

The first invocation might take a while as Nix downloads and compiles some dependencies.

Using the Sic compiler

To install the sicc program, run

make -C sicc install

which uses nix-env to put the program in your ~/.nix-profile.

You can now run sicc to see the usage. The user interface for this tool is very rudimentary.

Is the implementation correct?

Full correctness of the dai system cannot yet be established, since we have neither a full specification nor a complete implementation. Still, we propose a sketch for attaining verification.

Bytecode-level correctness

We need to know that the hexadecimal bytecode artifact does what we expect it to do. Moreover, these expectations should be in a form that allows us to take them as assumptions when proceeding with higher-level verification.

Therefore, we consider the Sic source code and the Sic semantics as being the functional specification for each smart contract. We then verify that the bytecode artifact, as interpreted by an EVM, exactly implements this functional specification.

This verification can and should be done redundantly for maximal assurance. Thus, we intend to

1. use KEVM's operational semantics combined with verification conditions generated from the Sic specification;
2. use our own SMT embedding based on decompilation;
3. use randomized testing to verify that the bytecode as executed matches the behavior of the Sic code as interpreted; and
4. audit the bytecode and overall process with an external auditing firm.

(Note that our code generation process is designed for easy auditing: the Solidity assembly is straightforward to relate both to the Sic code and the generated bytecode, and our compilation scheme is very straightforward.)

Higher-level correctness

Assuming we have compiled artifacts that correctly implement the Sic specifications, we can use the Sic specifications as assumptions in one or more formal proof systems, letting us verify invariants and claims about the system's behavior.

The goal is to formulate legible properties that users and stakeholders can understand as encoding safe, fair, and equitable behavior, and to have these verified using trustworthy formalisms such as Isabelle, Agda, Coq, or TLA+.

System testing

We intend to create a comprehensive test suite with 100% branch coverage, as well as to do random testing based on a system model.

Simulation

We intend to create an interactive simulation environment that lets you step through and see the behavior of the system—for example, going through a test suite step by step to see exactly how the smart contracts process realistic requests.

Sic syntax

Syntax	Meaning
iff e	Revert if e false
set x...	Update data with clauses x...
v=e	Set v to e
v↑w↓e	Try increasing v and decreasing w by e, result nonnegative
v↑w↑e	Try increasing both v and w by e, result nonnegative
x+y	Sum of x and y
x★y	Integer product of x and y
¬x	Negation of x
x ≤ y	Whether x is less than or equal to y
x ≥ y	Whether x is greater than or equal to y
x or y	Whether either x or y is true
x ∧ y	Whether both x or y are true

We will specify a formal semantics of Sic at a later stage.