Add BIP340 example #1531
Add BIP340 example #1531
Conversation
W95Psp
requested review from
karthikbhargavan
and removed request for
maximebuyse
hax-lib/src/int/mod.rs
Outdated
| pub fn _unsafe_from_hex(s: &str) -> Self { | ||
| Self::new(num_bigint::BigInt::from_str_radix(s, 16).unwrap()) | ||
| } | ||
|
|
There was a problem hiding this comment.
Ah, the _unsafe_from_str method is treated specially by the engine, and this should not be used directly.
We have troubles with the documentation of hax-lib, so it's hard to discover. You can run RUSTCFLAGS="--cfg hax" cargo doc on the hax-lib folder to get the proper documentation.
But basically, here you should use the int! macro, which, unfortunately, doesn't supports hex. I opened issue #1532.
Let me fix this issue so that you can get rid of this.
There was a problem hiding this comment.
This is merged in main now, could you drop _unsafe_from_hex and use the int macro now?
There was a problem hiding this comment.
Yes, that seem to work, thanks a lot for the quick change! I will take a look at the locally generated docs as you suggested to see if I can find more stuff that makes sense for me to use. Thanks a lot for the hint!
|
This PR has been marked as stale due to a lack of activity for 60 days. If you believe this pull request is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days. |
I will get back to this for further improvements but it would be nice to receive some initial feedback. I understand this is not the highest priority though... |
clementblaudeau
added
waiting-on-reviewer
|
@spitters would you or one of your students have time to look at this PR? |
3 participants
This is an attempt to port the BIP340 example that was already present in hacspec previously to hax.
This is partly a learning project to learn hax myself and I also need this as a dependency for some follow-up BIPs where I want to use hax as well. So it's not super relevant for me that this gets merged into the hax repository in the end but if it does I would be happy to help maintain it.
For now I am looking for feedback on if this is very roughly going in the right direction. I have been looking into documentation and examples that I could find but I have been struggling a bit with the scope of this new approach of hax vs. hacspec previously. I have a bunch of different versions of this, for example in this one here I am making some minor edits to the int code of
hax-libitself but I also had a version that worked without that.Any kind of feedback/hints is very much appreciated! I am planning to add some conditions etc. when I have a bit more confidence in what is already there :)