Issues with generation of header and proof hints

[jinxinglim]

During proof generation (from MPG), here are the commands that we usually run to generate the proof hints from the semantics:

1. kompile with just the following flags --backend llvm --llvm-proof-hint-instrumentation

2. Generate the header file from the definition.kore of the kompiled definition, e.g., kore-rich-header solidity-kompiled/definition.kore > solidity.header

3. krun with just the --proof-hint flag

4. Pretty printing the hints file via kore-proof-trace --verbose --streaming-parser --expand-terms [header_file] ...

Issues/Questions/Feedback

I tried to add the appropriate flags in the commands in the Makefile from this repo and tested them locally. Here are what I found and also some questions and feedback regarding them:

1. Adding the 2 flags --backend llvm --llvm-proof-hint-instrumentation on line 26 has no issue, which is great!

2. Generating the header file from the definition.kore of the kompiled definition, e.g., kore-rich-header solidity-kompiled/definition.kore > solidity.header terminated with the following output and I also attached the incomplete header file output:

   terminate called after throwing an instance of 'std::runtime_error'
   what():  cannot yet serialize sorts with sort parameters
   Aborted (core dumped)

   Incomplete header file: solidity.header.zip

3. Adding --proof-hint flag on line 14 and run make test-regression but terminated due to the following error:

   ulimit -s 65536 && bin/krun-sol test/regression/addliquidity.sol test/regression/addliquidity.txn > test/regression/addliquidity.out 2>&1
   make: *** [Makefile:81: test/regression/addliquidity.out] Error 139

   Incomplete hint file: addliquidity.zip

4. kore-proof-trace cannot be run as we do not have teh header file.

5. For kompiling definitions, the MPG team usually kompile with just the following flags: --backend llvm --llvm-proof-hint-instrumentation. However, for the kompile command in the Makefile of the repo, it is run with flags: --gen-glr-bison-parser -O2 --heuristic pbaL. Just want to check if they are necessary.

6. For krun-ing programs, we use krun with some flags as seen here: krun temp.pgm --definition $4 --proof-hint --output-file $2/$filename.kwasm.hints. However, on this repo, krun is run with these additional flags: -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="false" --no-expand-macros. Just want to check if they are necessary. And what does ISUNISWAP actually do?

7. It would be good to have some guide on running kompile/krun with appropriate flags.

[mariaKt]

@jinxinglim

5. -O2 --heuristic pbaL are for performance reasons.
6. The additional flags are necessary. ISUNISWAP is the name of a configuration variable (boolean) specific to the solidity demo semantics. Here you see a run of krun with that configuration variable being passed the value false. This configuration variable indicates whether to do summarization (true) or not (false). Please keep in mind that at the moment we only do summarization for the the test UniswapV2SwapRenamed.sol, this is the only test for which you may use the value true.
7. It should be possible for you to run bin/krun-sol instead of krun. It is a wrapper around krun for the solidity demo semantics. It accepts
   • the contract file (.sol)
   • the transactions (.txn)
   • an optional 3rd parameter that is a file, containing either true of false, used to initialize the ISUNISWAP configuration variable mentioned above. If no 3rd argument is provided, the default is false.
   • It passes through other flags to krun.
   • Otherwise, you can run krun as follows:

     krun -d location_of_compiled_definition contract.sol -cTXN=transactions.txn -pTXN=path-to/kparse-txn -cISUNISWAP="false"/"true" --no-expand-macros

     plus any other flags you need.

[jinxinglim]

Thank you @mariaKt for the detailed answers for point 5, 6 and 7.

Regarding the -pTXN option, can I check with you if it must be on a separate standalone bash script as seen for bin/kparse-txn? Can the kparse command be on the same script with the krun command? If yes, how can we make the kparse command within the same script as the one running krun?

Thank you!

[jinxinglim]

Thanks to @theo25 for addressing this issue. I have tested the change made in this PR https://github.com/runtimeverification/llvm-backend/pull/1154 and I am able to generate proof hints for solidity-demo-semantics. Thank you once again!

[dlucanu]

I followed the above steps, everything worked OK except the kore-proof-trace commands that displays

zsh: killed     kore-proof-trace --expand-terms --verbose hints/UniswapV2Swap.header   > 

The used command is:

% kore-proof-trace --expand-terms --verbose hints/UniswapV2Swap.header hints/UniswapV2Swap.hints solidity-kompiled/definition.kore > hints/UniswapV2Swap.hints.txt

The file hints/UniswapV2Swap.hints.txt is empty.