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

Update KRYPTO hooks to use Bytes instead of String #3684

Merged
merged 10 commits into from
Jan 9, 2024
Merged

Conversation

Scott-Guest
Copy link
Contributor

@Scott-Guest Scott-Guest commented Oct 23, 2023

Fixes #3683

The KRYPTO hooks now use Bytes for raw strings instead of String, so this PR updates the evaluators here accordingly.

Additionally, I updated all tests that reference KRYPTO lest they give errors about hooked symbols having incorrect sorts. Specifically,

  • I regenerated the regression-evm tests by running generate-regression-tests.sh with my branch of KEVM that uses the updated hooks.
  • For all the tests that I couldn't regenerate, I manually patched them by changing the existing KRYPTO symbols into functions which wrap the new hooks with appropriate calls to String2Bytes and Bytes2String.

Corresponding PR testing this on the booster: runtimeverification/hs-backend-booster#370

@Scott-Guest Scott-Guest self-assigned this Oct 23, 2023
@Scott-Guest
Copy link
Contributor Author

Blocked on #3687 - the regression-evm tests need to be updated to account for the KRYPTO changes

@Scott-Guest Scott-Guest changed the title Update KRYPTO hooks to use Bytes instead of String [DO NOT MERGE YET] Update KRYPTO hooks to use Bytes instead of String Nov 9, 2023
@Scott-Guest Scott-Guest changed the title [DO NOT MERGE YET] Update KRYPTO hooks to use Bytes instead of String [DO NOT MERGE] Update KRYPTO hooks to use Bytes instead of String Nov 9, 2023
@Scott-Guest
Copy link
Contributor Author

Scott-Guest commented Nov 9, 2023

Holding off on actually merging this until I can locally test with KEVM and the booster

@yale-vinson
Copy link

@Scott-Guest Is this still blocked? This is blocking Semantics #2107 and I would like to get that one closed out as it has been aging in the backlog for quite a while.

@Scott-Guest
Copy link
Contributor Author

@yale-vinson Apologies, I had to shift to some higher-priority work in the middle of this.

I have the bandwidth now and will prioritize getting this unblocked.

@Scott-Guest Scott-Guest changed the title [DO NOT MERGE] Update KRYPTO hooks to use Bytes instead of String Update KRYPTO hooks to use Bytes instead of String Jan 8, 2024
Copy link
Contributor

@goodlyrottenapple goodlyrottenapple left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Do we need to modify stuff upstream once this is merged? If so, is everything else ready?

@rv-jenkins rv-jenkins merged commit 85b593e into master Jan 9, 2024
7 checks passed
@rv-jenkins rv-jenkins deleted the krypto-bytes branch January 9, 2024 21:23
@Scott-Guest
Copy link
Contributor Author

Scott-Guest commented Jan 9, 2024

@goodlyrottenapple There are a number of changes needed upstream, but they're all trivial and/or ready to go:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Update KRYPTO hooks to use Bytes
4 participants