cp526
commented
2 months ago Just to clarify, only the 'terms' section of the error report is specific to the SMT counter model, all the rest of the information is specific only to the control-flow path along which CN found the error (the constraints and resources are not specialised to the counterexamples values, although one may want to do some of that sometimes).
The very interactive option is interesting and requires a different setup. Currently the error reports, although animated, are static in that they are one-off generated once CN is done. The more interactive option requires tighter coupling of CN and the UI, so one can is viewing CN "live".
The choose-the-control-flow-path could be (implemented as) a special case of the more interactive version that supports adding constraints "live".
(not sure whether we want to have this kind of discussion here in the public github issues or in one or other mattermost, but let's see)
Musing on the proof-state UI: The steppable proof-state display is currently specific to an SMT-generated counterexample from a verification failure.
In order to understand what CN knows at each state, I imagine it would often be useful to show what it knows in general, without specialising to that counterexample. And, more interactively, to be able to force control-flow choices as one steps, e.g. to go down the left or right branch of a conditional. And, even more interactively, to be able to interactively add additional constraints, e.g. that some hitherto-unconstrained value is some particular concrete value (this can also be done by adding
requiresorasserts, but maybe one really wants to do it in something more like a REPL). Perhaps one would even want to be able to simultaneously show what it knows in general and what it knows from a concrete test case / counterexample / additional assumptions?