Issues running kclaim style proofs

ehildenb commented 9 months ago

[x] Re-executing a KClaim (with --save-directory) where a proof changes or a dependency changes, does not trigger --reinit behavior. We should be parsing the claims, and invalidating any claims where the claim itself or a dependency has changed.
[ ] Parallel proof discharge waits for each batch of proofs instead of adding to the queue of tasks asynchronously. This means that if there a few really long running proofs in one layer of proofs, we won't move on to the proofs in the next layer who's dependencies are already discharged.
[ ] Proofs whos dependencies are not discharged should not be run unless the dependency is admitted or the user specifies to admit dependencies. Perhaps?

yale-vinson commented 9 months ago

@nwatson22 what is the relative priority of this? I am assuming that #2009 has priority, but I want to make sure things are aligned across Kontrol.

yale-vinson commented 8 months ago

Closing evm-semantics PR #2099 closes the first bullet point of this one. The others will be addressed once this PR closes.

palinatolmach commented 8 months ago

@anvacaru @PetarMax do you think these changes might help order proofs for compositional symbolic execution? Or do you have another solution in mind?

yale-vinson commented 7 months ago

Issue blocked by Booster #383

palinatolmach commented 1 month ago

Moved to backlog with Medium High priority, since we haven't got to work on it since November, and it doesn't seem to be a priority now. Please bring it back if I'm wrong!

runtimeverification / evm-semantics

Issues running kclaim style proofs #2088