Integrate KCFG into `kavm`

[geo2a]

Implements #283

• [x] Needs pyk#200

One of the simplest claims to try is the tests/specs/transactions/pay-spec.k

Steps to reproduce the failure:

git clone git@github.com:runtimeverification/avm-semantics.git
cd avm-semantics
# build the verification definition
make build-avm-verification
# bind the kompiled verification definition to a variable for convenience
export KAVM_VERIFICATION_DEFINITION_DIR=$(realpath .build/usr/lib/kavm/avm-haskell/verification-kompiled)
# install Python deps and the 'kavm' package
poetry -C kavm/ install
# run the prover on a simple spec
# NOTE: make sure to sue the project-local 'kavm', not the one that may have been installed with kup! 
poetry -C kavm run kavm kcfg-prove --port 7777 --definition-dir $KAVM_VERIFICATION_DEFINITION_DIR  --claim-id pay tests/specs/transactions/pay-spec.k

For me, the proof fails due to kore-rpc returning ErrorDecidePredicateUnknown and hanging . The output should look something like this:

WARNING 2023-02-10 18:30:40,686 pyk.kcfg.explore - Falling back to manual branch extraction PAY-SPEC.pay.kfcg: b4e020..31f74e
WARNING 2023-02-10 18:31:37,277 pyk.kcfg.explore - Falling back to manual branch extraction PAY-SPEC.pay.kfcg: 51192e..a8b340
WARNING 2023-02-10 18:31:47,360 pyk.kcfg.explore - Falling back to manual branch extraction PAY-SPEC.pay.kfcg: c42624..3c05be
WARNING 2023-02-10 18:32:33,091 pyk.kcfg.explore - Falling back to manual branch extraction PAY-SPEC.pay.kfcg: da4720..7cb808
kore-rpc: DecidePredicateUnknown {action = ErrorDecidePredicateUnknown ...

The resulting KCFG will be written into '.kavm/'. Browse it in the terminal:

poetry -C kavm run kavm kcfg-view --definition-dir $KAVM_VERIFICATION_DEFINITION_DIR  .kavm/1d67cc1f940746e0a20ec219fa85a5b9f2c2296912eb30693cd664db88e8128f.json

The cfg contains many nodes that result from branches that seem to be obviously infeasible. Looking at the configurations suggests that some of them may be over-abstracted, i.e. contain variables instead of previously concrete values.

To verify the same spec with plain KProve, run:

poetry -C kavm run kavm prove --definition-dir $KAVM_VERIFICATION_DEFINITION_DIR tests/specs/transactions/pay-spec.k

That should return #Top.

The implementation of kavm kcfg-prove can be found here: https://github.com/runtimeverification/avm-semantics/blob/bb2a68b99da8b25ecd8db4bd3d98e60cc3a19de1/kavm/src/kavm/__main__.py#L271

[ehildenb]

I had to:

• Cleaned out all submodules (running using kup K and kup kore-rpc).
• Run make plugin-deps first.
• Run make -C ./kavm first.

[ehildenb]

I've added command kavm kcfg-show .... [--node NODE_ID]* for getting more detailed output about each node.

I've also adjusted all the kavm kcfg-* ... commands to take arguments in the same format (spec file, spec module, claim id).

[ehildenb]

@geo2a I've root-caused the issue I believe.

The frontend, when compiling the definition, turns a rule that says this:

rule <transactions> <transaction> <txID> ID </txID> REST </transaction> REST_TRANSACTIONS </transactions> ...

Into something like this:

`<transactions>`(`_TransactionCellMap_`(`TransactionCellMapItem`(`<txID>`(ID), `<transaction>`(`<txID>`(ID), REST)), REST_TRANSACTIONS)) ...

But when it generates the spec obiligations, we're getting something more like this:

`<transactions>`(`_TransactionCellMap_`(`<transaction>`(`<txID>`(ID), REST)), REST_TRANSACTIONS)) ...

This latter one requires an injection to be generated from SortTransactionCell to SortTransactionCellMapItem, but the former does not (because it uses constructor TransactionCellMapItem). So the Kore generated ends up looking very different. The problem could be in pyks kast-to-kore routines too.

I need to investigate more, but basically, the result is that the rules you expect to match which do transaction lookups are not matching, and so the backend is guessing that any of them can match.

I believe I can make a minimal example and use that for debugging the issue in pyk.

[ehildenb]

I've threaded through BugReport and hardcoded it to produce one. I have a script called doit that I'm using to test things:

set -euxo pipefail

poetry_run() {
    poetry -C ./kavm -- run "$@"
}

clean() {
    rm -rf .build
    make plugin-deps
    make build-avm-verification
}

build_pyk() {
    cd kavm
    poetry update
    make
    cd -
}

prove() {
    poetry_run kavm kcfg-prove --port 7777                   \
        --definition-dir ${KAVM_VERIFICATION_DEFINITION_DIR} \
        ${claim_file} ${claim}                               \
        --verbose                                            \
        "$@"
}

view() {
    poetry_run kavm kcfg-view                                \
        --definition-dir ${KAVM_VERIFICATION_DEFINITION_DIR} \
        ${claim_file} ${claim}                               \
        --verbose                                            \
        "$@"
}

show() {
    poetry_run kavm kcfg-show                                \
        --definition-dir ${KAVM_VERIFICATION_DEFINITION_DIR} \
        ${claim_file} ${claim}                               \
        --verbose                                            \
        "$@"
}

claim=pay
claim_file=tests/specs/transactions/pay-spec.k
export KAVM_VERIFICATION_DEFINITION_DIR=$(realpath .build/usr/lib/kavm/avm-haskell/verification-kompiled)

# pkill kore-rpc || true
# clean
# build_pyk
prove --verbose
# view
# show --no-minimize --node 1c5073..077d08

With branch cell-map-to-kore of pyk (https://github.com/runtimeverification/pyk/pull/200), I'm able to take more steps, and get something that looks like this:

Before it crashes with this error: https://github.com/runtimeverification/haskell-backend/issues/3496

[ehildenb]

Actually the proof is passing now:

I had made some modifications to the proof for debugging which caused it to fail.

I also changed it to add execute_depth=1 to the call to all_path_reachability_prove. This ensures we don't execute off the end of the proof (and we check implication every step), but it makes it very slow, because we're storing every state.

Better would be to make sure that every transaction inserts a dummy #endTx() marker, with a simple rule like this:

rule [endtx]: <k> endTx() => . ... </k>

Then we can supply that as a terminal_rule argument to all_path_reachability_prove, and it will make sure to save final states that we need to compare against the target node.

[geo2a]

Thanks @ehildenb! I've added terminal rules and I tried the prover with a couple more claims. That's a really good start, I think performance-wise it's as good as plain KProve! I'll be merging that

[ehildenb]

@geo2a do not forget to unpin the pyk version like you have in https://github.com/runtimeverification/avm-semantics/pull/284/commits/50f8d2db779d09f2ebe44bfe9343ac7c43ee015b commit! I strongly recommend you do not commit pinned versions like this without setting yourself a reminder to unpin it! Very dangerous, that branch will go away once it's merged!

[geo2a]

Thanks @ehildenb, I've already made sure the pyk changes will be merged soon. I'll unpin before merging.