Conversation
This is easier for symbolic execution and likely faster as well.
This will likely have a small performance hit, but it will be recovered using CSE.
nishantjr
force-pushed
the
njr/tweaks-for-cse
branch
from
66a7bd3 to
25679d7
Compare
nishantjr
force-pushed
the
njr/tweaks-for-cse
branch
from
25679d7 to
f0257cd
Compare
During concrete execution these hooks execute to `.K`. This does not work during symbolic execution, as the side-effects of the hooks would not be accounted for. In the VLM repo, we have modified the VLM hooks for symbolic execution to instead be uninterpreted functions that return the WorldState sort. Here, we create a <worldState> cell to store the side-effects, while unblocking execution in the <k> cell.
We introduce the ==Bytes construct, because K seems to have difficulty figuring out that a term of sort K passed reached via executing the semantics is the same as that introduced via pyk. The reason for this seems related to the first being parsed as a KSequence, i.e. giveing us `X:Bytes ~> .K`. I am not sure which is "correct", given the dual nature of the K sort as the top sort, vs as a sequence. We also change the requires clause for KZGPOINTEVAL's unhappy path to make it obvious to the backend that is the negation of that for the happy path.
Author
|
@Robertorosmaninho Sorry, should have mentioned: The individual commits have more information about each change. |
|
@nishantjr I left a new comment on our thread |
|
@nishantjr, if your changes are also compatible with |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.