-
Notifications
You must be signed in to change notification settings - Fork 4
feat(rt): support round-trip transmute bytes <> u64 casts #804
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
Conversation
jberthold
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work! Just A few details to adjust...
We should probably add a simplification for the round-trip with symbolic values, like the one I added for amount in the p-token module.
kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected
Outdated
Show resolved
Hide resolved
Co-authored-by: Jost Berthold <[email protected]>
Co-authored-by: Jost Berthold <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work.
| andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant) | ||
| ``` | ||
|
|
||
| Casting a byte array/slice to an integer reinterprets the bytes in little-endian order. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suspect this actually depends on architecture, and we do have access to that information in the configuration via the MachineInfo field Endian (link). Not sure if it is an easy inclusion but given we would then want to check it on different endian machines to ensure it works I think it's worth investigating right now. At least a note should be included as this should break on other architectures iiuc.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe we just add a TODO? We have a few more places where we assume little-endian byte order and machine word size 64bit.
|
I investigated this applied to p-token => |
Uh oh!
There was an error while loading. Please reload this page.