- git clone https://github.com/dapphub/klab
- cd klab/
- make deps
- make deps-haskell
- sudo make link
- source ./env # <--you might need to
chmod
this to make it executable, it relies onpwd
so you must run it in theklab
directory, and you need to run it in any shell you want to useklab
in--I like to add it to my .bashrc - the command-line tools
jq
andjshon
are needed if you don't already have them
klab
will fetch and compile the versions of K and KEVM that it needs, and the environment variables set by the env script will automatically cause klab
to use these.
Follow instructions: https://github.com/dapphub/dapptools/
- git clone https://github.com/makerdao/k-dss.git
- cd k-dss/
- git checkout pot-rpow # this branch has updated
pc
values for thePot.rpow-loop
lemma - cd dss/
- dapp update
- dapp build
- cd ..
- klab build
- klab focus Pot_rpow-loop_pass
- klab prove --dump
- klab get-gas && klab solve-gas && klab build
- klab focus Pot_rpow_pass
- klab prove --dump
The current behavior I'm observing is that this proof hangs and never completes.
The generated K spec can be found in out/specs/.k, where can be found by running klab hash Pot_rpow_pass
You can see that act
that generates the spec here:
https://github.com/makerdao/k-dss/blob/pot-rpow/src/dss.md
(search for "rpow of Pot")
The K log file can be found at: out/data/.log
The needed information can be found here: https://dapp.ci/k-dss/1bf8c47b9f7afa2c89ca/#Pot_rpow(uint256,uint256,uint256)
At the top of that page, commits of various repos and hashes of certain files associated with the CI invocation are specified:
Klab version aeb0e08a81969f3f33a4e1ec0fe1b8cb2d58b969
EVM-semantics version 8e0403ab6fc89113d1025d7dae503e445c86fe30
bin_runtime f9305561e3cd5a1bdf1131f655023dae65657fab
k-dss version 87935ec6091467267a088a457473495cfe7ed3d7
storage.k.md f030d3bfa216f1eaa0a47327048c7233d737aa5c
lemmas.k.md 83ee67ca929d1af97fcfe2e3bef7d8f87788df1f
prelude.smt2.md 3a30ec95e55dd15bd726e6238c3a721f5e8c0b51
This information can be used to reconstruct the conditions of the passing proof. I haven't actually attempted this, but the sequence of steps would look something like:
- Clone
klab
repo, checkout commit aeb0e08a81969f3f33a4e1ec0fe1b8cb2d58b969, build and install (this should automatically pull in the correct EVM semantics) - git clone https://github.com/dapphub/k-dss.git # <--- this is now at DappHub, not MakerDao!
- cd k-dss/, checkout commit ca582e04335d1a627f5f9bcf958a48fbc3025473 (NOT the one specified in the CI header, that one got removed, but this one has all the same meaningful code)
- fetch and build
dss
submodule, following steps from previous section (technically should use a historical Solidity version, but we'll circumvent this in a later step) - klab build
- replace out/bin_runtime.k with the following file: https://dapp.ci/k-dss/1bf8c47b9f7afa2c89ca/bin_runtime.k (this contains the bytecode for all of the contracts, hence why we didn't bother to adjust the compiler version earlier)
- klab focus Pot_rpow-loop_pass
- klab prove --dump
- klab get-gas && klab solve-gas && klab build
- klab focus Pot_rpow_pass
- klab prove --dump