rpow_proof_guide.md

Installing klab (assuming you already have everything you need to build K installed)

1. git clone https://github.com/dapphub/klab
2. cd klab/
3. make deps
4. make deps-haskell
5. sudo make link
6. source ./env # <--you might need to chmod this to make it executable, it relies on pwd so you must run it in the klab directory, and you need to run it in any shell you want to use klab in--I like to add it to my .bashrc
7. the command-line tools jq and jshon 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.

Installing dapptools

Follow instructions: https://github.com/dapphub/dapptools/

Running the Pot_rpow_pass proof

1. git clone https://github.com/makerdao/k-dss.git
2. cd k-dss/
3. git checkout pot-rpow # this branch has updated pc values for the Pot.rpow-loop lemma
4. cd dss/
5. dapp update
6. dapp build
7. cd ..
8. klab build
9. klab focus Pot_rpow-loop_pass
10. klab prove --dump
11. klab get-gas && klab solve-gas && klab build
12. klab focus Pot_rpow_pass
13. 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

Reproducing last accepting run [UNTESTED!]

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:

1. Clone klab repo, checkout commit aeb0e08a81969f3f33a4e1ec0fe1b8cb2d58b969, build and install (this should automatically pull in the correct EVM semantics)
2. git clone https://github.com/dapphub/k-dss.git # <--- this is now at DappHub, not MakerDao!
3. 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)
4. 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)
5. klab build
6. 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)
7. klab focus Pot_rpow-loop_pass
8. klab prove --dump
9. klab get-gas && klab solve-gas && klab build
10. klab focus Pot_rpow_pass
11. klab prove --dump