Skip to content

CSE: handle non-zero slot offset for contract variables #622

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
Closed
palinatolmach opened this issue Jun 12, 2024 · 0 comments · Fixed by #663
Closed

CSE: handle non-zero slot offset for contract variables #622

palinatolmach opened this issue Jun 12, 2024 · 0 comments · Fixed by #663
Assignees
@nwatson22
Labels
cse engagement

Comments

@palinatolmach
Copy link
Collaborator

palinatolmach commented Jun 12, 2024 •
edited
Loading

Follow-up to #600.

#600 adds support for generating new accounts corresponding to contract fields during CSE. We should improve the related constraint generation to account for cases where the contract variable has a non-zero offset in a storage slot.

Right now, the constraint look similar to:

maxUInt160 &Int #lookup(contract_storage, slot) ==Int KVariable(contract_account_name + '_ID')

assuming there is no offset, but we should apply an appropriate mask if there is.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nwatson22 nwatson22

Labels
cse engagement
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support symbolic contract storage slots with nonzero offsets runtimeverification/kontrol
2 participants
@palinatolmach @nwatson22