Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Issues running kclaim style proofs #2088

Open
1 of 3 tasks
ehildenb opened this issue Sep 25, 2023 · 5 comments
Open
1 of 3 tasks

Issues running kclaim style proofs #2088

ehildenb opened this issue Sep 25, 2023 · 5 comments
Labels
enhancement New feature or request

Comments

@ehildenb
Copy link
Member

ehildenb commented Sep 25, 2023

  • 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?
@ehildenb ehildenb changed the title Re-executing a kclaim style proof does not correctly detect out of date proof Issues running kclaim style proofs Sep 26, 2023
@nwatson22 nwatson22 self-assigned this Sep 29, 2023
@yale-vinson
Copy link

yale-vinson commented Oct 2, 2023

@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
Copy link

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

@palinatolmach
Copy link
Contributor

@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
Copy link

yale-vinson commented Dec 5, 2023

Issue blocked by Booster #383

@palinatolmach
Copy link
Contributor

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

4 participants