Make CSE more useful by reusing the previous proof

[Stevengre]

Currently, the proof will re-run all the things when using --reinit and unchange if there is a proof. Therefore, the CSE won't bring a lot of improvement for the tests which just call a function once.

My idea is to provide incremental verification: If only the tests changes, don't re-generate the summary for the external callee functions. Intead, use the summary directly. I think this will significantly enhance the verification experience, especially in scenarios where only the tests will be modified during the audit.

[Stevengre]

Idea 4 incremental CSE:

• Store the summaries separately.
• Change the summaries only the file changes (digest changes) or Kontrol/KEVM/K changes.
• if summary exists, use the summary directly.

Improvement:

• Reduce the verification time for tests calling the same function. It may happen to a lot of utility functions.
• Reduce the verification time when only the tests change. This might be the most common situation we faced during auditing.
• Reduce the verification time when tests use lib functions that are already available in KaaS.

[ehildenb]

On this line:

kontrol/src/kontrol/prove.py

Line 86 in b5a3f17

for include_summary in collect_tests(foundry, options.include_summaries, reinit=False)

, we are collecting the subproofs as summaries to use for CSE, but setting reinit=False to do it, so I'm surprised it's re-executing the summaries hwen you pass --reinit.

[Stevengre]

Sorry, I think I may not get the point. But I think that line is provided for --include-summary and will not contribute the --cse option. The automatic cse process always re-prove the callee functions, here:

kontrol/src/kontrol/prove.py

Line 115 in b5a3f17

summary_ids.extend(p.id for p in foundry_prove(new_prove_options, foundry, recorded_state_entries))