[KIP] - Tool for proving functional lemmas sound

ehildenb commented 3 years ago

Motivation

When doing proofs, it's necessary to write a (usually large) body of lemmas for simplifying out functional terms. These lemmas are fed to the backend as axioms, without checking their validity. This increases our trust base (sometimes dramatically) for formal verification engagements).

If we can mechanically prove these lemmas are consistent with the definition (and the other lemmas), then our trust base gets smaller and we can have more confidence when reviewing PRs for verification efforts that the lemmas supplied are sound.

Existing Approach

@ttuegel has helped me develop a way to automatically discharge these lemmas using the haskell backend's ability to encode lemmas to SMT. The procedure is as follows:

Build this branch of K: https://github.com/kframework/k/tree/pyk-prove-lemmas (includes a modified haskell backend, and support for emitting json definitions of kprove specs).
Add the smt-lemma and simplification attributes to any rules in the original definition you want to be able to use to discharge the lemmas. Kompile the new definition.
Add the smt-lemma attribute to all simplification lemmas used for proving (usually in a module named VERIFICATION).
Call kprove --emit-json --dry-run --def-module VERIFICATION on a dummy proof module, to produce the file def-module.json.
Run the pyk script pyk-prove-lemmas.sh, supplying the lemma module names you're interested in and what k files should be required. This generates a single file which contains all the claims needed to feed into Haskell backend.
Run each proof in the new claims file individually.

Example Run

Build modified KEVM:

git clone 'https://github.com/kframework/evm-semantics'
cd evm-semantics
git checkout pyk-prove-lemmas
git submodule update --init --recursive
make deps RELEASE=true
make build-haskell

Dummy proof to generate the required def-module.json file:

./kevm prove --backend haskell tests/specs/functional/lemmas-spec.k VERIFICATION --dry-run --emit-json

Generate the proof obligations (in this case, we are trying to prove every lemma in tests/specs/lemmas.k sound):

export PYTHONPATH=./deps/k/k-distribution/target/release/k/lib/kframework
python3 pyk-prove-lemmas.py LEMMAS-HASKELL,LEMMAS evm.md,edsl.md > tests/specs/functional/lemmas-verification-spec.k

This produces a file tests/specs/functional/lemmas-verification-spec.k with 59 VERIFICATION-i modules and 59 CLAIM-i modules. The VERIFICATION-i modules contain all the lemmas from LEMMAS and LEMMAS-HASKELL except the ith lemma, and the CLAIM-i module contains the ith lemma.

So we prove each CLAIM-i module in sequence:

for i in $(seq 0 58); do
    rm transcript_lemmas-verification_VERIFICATION-$i.smt2
    if ./kevm prove --backend haskell --log-z3 tests/specs/functional/lemmas-verification-spec.k VERIFICATION-$i --spec-module CLAIM-$i-SPEC; then
        echo "success: $i"
    else
        echo "failure: $i"
    fi
done

This results in:

18 lemmas being proven automatically without any apparent issue.
19 lemmas legitimately failing (either due to lack of enough smt-lemma attributes in the original semantics, or something else).
13 lemmas failing (but reporting passing) without even taking a single rewrite step.
9 lemmas failing (but reporting passing) during initialization.

ehildenb commented 3 years ago

What I would like to do is discuss how to automate this more. The frontend can continue to be handled by pyk, but I'd like to avoid having to mangle the definition to make this whole process go through.

The biggest changes I have to make to the definition are:

Make sure every symbol that shows up in the lemmas has smtlib and simplification attribute.
Make sure that every lemma in the lemmas file has smt-lemma and simplification attribute.

The backend has to make the following changes:

Turn off erroring out if Z3 returns unknown
Turn off the function evaluator (and rely only on Z3).

To simplify the process, I would propose adding a way to send all function definitions as smt-lemma, without having to manuallly annotate each one. The backend can hide it's new behavior behind a flag. Then pyk (and addition to --emit-json) can take care of the rest for a prototype.

ehildenb commented 3 years ago

The branch pyk-prove-lemmas on KEVM now has all the infrastructure in place for doing this, with just the submodule pegged version of K there. It does not succeed very often, because of the "turning off Z3 unknown errors" issue in the haskell backend.

ehildenb commented 3 years ago

We will wait and see what other needs for this arise (other than KEVM) to have a better idea of what is needed.

ehildenb commented 1 year ago

runtimeverification / k