KEVM proof crash NoSuchElementException: key not found: #EmptyK

[fasapa]

I was attempting to prove basic properties of the OpenZeppelin ERC20 contract, more specifically the decimals() call, and some proofs crashes K. KEVM version 1.0.133.

Steps to reproduce:

1. kevm solc-to-k ERC20.sol ERC20 --pyk --main-module ERC20-VERIFICATION --verbose > erc20-bin-runtime.k
2. kevm kompile erc20-spec.md --pyk --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell (erc20-bin-runtime.k and erc20-spec.md)
3. kevm prove erc20-spec.md --backend haskell --definition erc20-spec/haskell --pyk --claim ERC20-SPEC.decimals

Expected result:

Proof passing or failing without a crash.

Actual result:

Proof is crashing:

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(NoSuchElementException: key not found: #EmptyK)

The output of kevm prove with --verbose flag: crash.txt. I have the same proof with --debug flag, but it is too big to upload it to github.

[fasapa]

Observed the same behavior in the newest KEVM version 1.0.168.

[fasapa]

changed the output from

<output> .Bytes   => #buf(8, 18) </output>

to

<output> .Bytes   => #buf(32, 18) </output>

and it didn't crash. It was a typo in the spec, but isn't supposed to crash.

[iFrostizz]

Just tested this and it has been fixed since.
The typo is correct though !
Note that the commands slightly changed now

kevm solc-to-k ERC20.sol ERC20 --pyk --main-module ERC20-VERIFICATION --verbose > erc20-bin-runtime.k

kevm kompile erc20-spec.md --pyk --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --output-definition erc20-spec/haskell

kevm prove erc20-spec.md --backend haskell --definition erc20-spec/haskell --pyk --claim ERC20-SPEC.decimals -v --save-directory .