KMCD - Multi-Collateral Dai (MCD) KSpecification
- K-DSS bytecode verification: Reports and Repository
- DSS solidity sources: https://github.com/makerdao/dss
- Useful invariants: https://hackmd.io/lWCjLs9NSiORaEzaWRJdsQ (note:
takeis out of date is currently represented in code as a Collateral's
- MCD Documentation: https://docs.makerdao.com/
- MCD Wiki: https://github.com/makerdao/dss/wiki
The semantics is broken into several sub-modules.
- kmcd-driver - common functionality in all modules.
- kmcd - union all sub-modules.
- kmcd-props - statement of properties that we would like to hold for the model.
- kmcd-prelude - random testing harness.
- vat - tracks deposited collateral, open CDPs, and borrowed Dai.
- pot - interest accumulation for saved Dai.
- jug - stability fee collection.
- dai - Dai ERC20 token standard.
- spot - price feed for collateral.
- gem - abstract implementation of collateral.
- join - plug collateral into MCD system.
- cat - forcible liquidation of an over-leveraged CDP.
- vow - manage and trigger liquidations.
- flap - surplus auctions (Vat Dai for sale, bid increasing Gem MKR).
- flop - deficit auctions (Gem MKR for sale, lot decreasing Vat Dai).
- flip - general auction (Vat Gem for sale, bid increasing Vat Dai, lot decreasing Vat Dai).
- end - close out all CDPs and auctions, attempt to re-distribute gems fairly according to internal accounting.
After installing all the dependencies needed for K Framework, you can run:
make deps make build -j4
If you are on Arch Linux, add
make deps, as the
FastBuild versions do not work.
Whenever you update the K submodule (which happens regularly automatically on CI), you may need to do:
rm -rf deps git submodule update --init --recursive make deps make build -j4
Running Simple Tests
tests/, we have some example runs of the system.
You can run on these simulations directly to get an idea of what the output of the system looks like.
./kmcd run --backend llvm tests/attacks/lucash-flip-end.mcd
If you want to run all the attack tests (and check their output), run:
make test-execution -j4
Running Random Tester
Make sure that
pyk library is on
krun is on
export PYTHONPATH=./deps/k/k-distribution/target/release/k/lib export PATH=./deps/k/k-distribution/target/release/k/bin:$PATH
You can ask the random tester for help:
./mcd-pyk.py random-test --help
Then you can start the random tester running, with depth 100, up to 3000 times:
./mcd-pyk.py random-test 100 3000 &> random-test.out
Then you can watch
random-test.out for assertion violations it finds (search for
Additionally, the option
--emit-solidity is supported, which will make best-effort emissions of Solidity code:
./mcd-pyk.py random-test 100 3000 --emit-solidity &> random-test.out
This emitted Solidity code can be used for conformance testing the Solidity implementation.
Speed up with
By running KServer while working with
mcd-pyk.py, you will see about 4x the throughput in simulations.
This basically keeps a "warmed up" JVM around, so that we don't have to start over each time.
To start the KServer run:
And to stop the KServer, run:
You can make sure that the KServer is being used by running
tail -F kserver.log.
mcd-pyk.py is running, you should see entries like this being added:
NGSession 10: org.kframework.main.Main exited with status 0 NGSession 12: org.kframework.main.Main exited with status 0 NGSession 14: org.kframework.main.Main exited with status 0 NGSession 16: org.kframework.main.Main exited with status 0