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.

Sign up for GitHub

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

Jump to bottom

Add counterexample to interactive KCFG viewer #46

Closed
palinatolmach opened this issue Jul 5, 2023 · 2 comments
Closed

Add counterexample to interactive KCFG viewer #46

palinatolmach opened this issue Jul 5, 2023 · 2 comments
Labels
enhancement New feature or request

Comments

@palinatolmach
Copy link
Collaborator

palinatolmach commented Jul 5, 2023 •
edited
Loading

Related: runtimeverification/evm-semantics#1946
Similarly to how we output a counterexample (i.e., concrete assignment to variables) for the failing proof of a Foundry test in runtimeverification/evm-semantics#1927, we should use the get-model endpoint introduced in the Haskell backend to show the model of a specific node when kevm foundry-show --node is executed. Consider adding the model to the interactive KCFG viewer.
@palinatolmach palinatolmach self-assigned this Jul 5, 2023
@palinatolmach palinatolmach changed the title foundry-show: output model for a specific node Output model for a specific node in foundry-show, interactive KCFG viewer Jul 12, 2023
@palinatolmach
Copy link
Collaborator Author

The issue is partially addressed by runtimeverification/evm-semantics#1946, which shows the model for a node in foundry-show --node when called with the --failure-information --counterexample-information.

@palinatolmach palinatolmach changed the title Output model for a specific node in foundry-show, interactive KCFG viewer Add counterexample to interactive KCFG viewer Aug 22, 2023
@palinatolmach palinatolmach removed their assignment Aug 22, 2023
@palinatolmach palinatolmach transferred this issue from runtimeverification/evm-semantics Sep 26, 2023
@yale-vinson yale-vinson added the enhancement New feature or request label Nov 30, 2023
@anvacaru
Copy link
Contributor

We should sepparate counterexamples from the kcfg viewer, as the kcfg viewer is intended to inspect nodes of the proof. I don't see a point to display the counter example for/in each node.

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

No branches or pull requests
3 participants
@palinatolmach @anvacaru @yale-vinson