Debugging proofs

The following document assumes that the K front-end is cloned into ~/Documents/k and that the Haskell back-end is cloned into ~/Documents/kore.

Moreover, currently one would have to use the traiansf:issue-1137 branch for K as it allows conversion from .kore to .k (introducing the --save-proof-definition-to command).

Assume we would like to debug the proof for tests/proofs/wrc20-spec.k. Then, we can start with

make defn-haskell
rm -rf .prove .kprove
K_RELEASE=~/Documents/k/k-distribution/target/release/k \
  ./kwasm prove --backend haskell tests/proofs/wrc20-spec.k \
  --format-failures --def-module WRC20-LEMMAS --debug --dry-run \
  --save-proof-definition-to .prove
mv .kprove* .kprove

This script does the following:

• runs the pandoc scripts for converting the latest changes in kwasm-lemmas.md into .k
• cleans up the working directory
• compiles the proof definition and specification into the .kore format
• renames the kprove working directory to access it conveniently in later stages

Once this is done, we can invoke the KROE proof REPL with

PATH=~/Documents/k/k-distribution/target/release/k/bin:$PATH \
  rlwrap ~/Documents/kore/.build/kore/bin/kore-repl \
  .kprove/vdefinition.kore --module WRC20-LEMMAS \
  --prove .kprove/spec.kore  --spec-module WRC20-SPEC \
  --repl-script ~/kore/dist/kast.kscript

Within the REPL, use the usual commands: step N, leafs, select ...

To visualize a (large) configuration, one can do the following:

REPL> config > config.kore

This saves the KORE configuration into a file config.kore. Now we can convert it to K by using

sed -i 1d config.kore  # to remove the first line
~/Documents/k/k-distribution/target/release/k/bin/kast \
  -i kore -o pretty -d .prove config.kore >config.k

and inspect the K configuration in config.k.

To save a partial proof branch and restart it later, one can use:

REPL> save-partial-proof current-claim

to save the current goal into a file current-claim.kore

Then, the proof can be later restarted by using:

PATH=~/Documents/k/k-distribution/target/release/k/bin:$PATH \
  rlwrap ~/Documents/kore/.build/kore/bin/kore-repl \
  .kprove/vdefinition.kore --module WRC20-LEMMAS \
  --prove current-claim.kore  --spec-module CURRENT-CLAIM-SPEC \
  --repl-script ~/Documents/kore/dist/kast.kscript