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

Update KRYPTO hooks to use Bytes #3683

Closed
Scott-Guest opened this issue Oct 23, 2023 · 1 comment · Fixed by #3684
Closed

Update KRYPTO hooks to use Bytes #3683

Scott-Guest opened this issue Oct 23, 2023 · 1 comment · Fixed by #3684
Assignees
@Scott-Guest

Comments

@Scott-Guest
Copy link
Contributor

All of the KRYPTO hooks now use Bytes instead of String to represent raw byte strings (runtimeverification/blockchain-k-plugin#163). We need to update everything here accordingly.
@Scott-Guest Scott-Guest self-assigned this Oct 23, 2023
@Scott-Guest Scott-Guest mentioned this issue Oct 23, 2023
Merged
@Scott-Guest Scott-Guest mentioned this issue Nov 9, 2023
Open
1 task
@Baltoli
Copy link
Contributor

Baltoli commented Nov 9, 2023

Similarly runtimeverification/k#3801 (comment)

rv-jenkins pushed a commit that referenced this issue Jan 9, 2024
@Scott-Guest
Update KRYPTO hooks to use Bytes instead of String (#3684)
85b593e 
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Scott-Guest Scott-Guest

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Update KRYPTO hooks to use Bytes instead of String runtimeverification/haskell-backend
2 participants
@Baltoli @Scott-Guest