take
is out of date is currently represented in code as a Collateral's spot
price)The semantics is broken into several sub-modules.
After installing all the dependencies needed for K Framework, you can run:
make deps
make build -j4
If you are on Arch Linux, add K_BUILD_TYPE=Release
to make deps
, as the Debug
and 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
In directory 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
Make sure that pyk
library is on PYTHONPATH
, and krun
is on PATH
:
export PYTHONPATH=./deps/k/k-distribution/target/release/k/lib/kframework
export PATH=./deps/k/k-distribution/target/release/k/bin:$PATH
mcd-pyk.py
UsageYou 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 Violation Found
).
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.
kserver
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:
spawn-kserver kserver.log
And to stop the KServer, run:
stop-kserver
You can make sure that the KServer is being used by running tail -F kserver.log
.
As 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