-
Notifications
You must be signed in to change notification settings - Fork 661
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
[Proposal] bits/bytes syntax #682
Comments
Thanks for writing this up @gluax! I have a few comments for discussion: Syntax 1 requires adding a Syntax 2 requires no additional imports - since every datatype where For these reasons I gravitate towards Syntax 2 but would like to hear others thoughts. |
Which types are we going to use for bits, bytes, and their sequences? A natural choice for bytes is I agree with @collinc97 that Syntax 2 may be preferable to Syntax 1. Among other things, overloading adds a bit of complication to type checking and inference (still doable of course, just a bit more complicated). I was thinking whether we might use the type cast syntax (#600) for converting from/to bits and bytes, since we'll want to add it anyways for other types (as exemplified in that proposal):
Note that we would have to specify the length of the array, but the length must be known at compile time anyhow. If we want to spare the user, we could introduce a type notation like This type notation |
The The first version of the Once that is finalized, we can extend syntax to aggregate types such as arrays. @acoglio I like the idea of extending type casting to arrays of bits and bytes but I do think that should be a separate feature. Similarly, the generic array length |
I'll make a separate RFC for type wildcards. (Not sure there's a strong use case, but it seems worth considering, maybe in the future.) Understood about the underlying Rust gadgets. But what's not clear to me is what is the Leo type of |
I was also wondering about endianness. Would the bits/bytes be big endian or little endian? Should both options be provided? E.g.:
|
This is a good point. The gadgets will return vectors in little endian form. Should we provide additional methods to specify target endianness? |
I would say a good approach is to have method default one, i.e. .bytes -> little-endian bytes and we document that. Then we can have another method .big_endian_bytes(). At least that's my thoughts on the matter! |
My first instinct would be to have "symmetry", e.g. |
By the way, having two possible conversions (big vs. little endian) reinforces the fact that this should not use a type cast syntax (against my proposal earlier in this message thread), because the latter implies just one conversion. |
@collinc97 @gluax I'm still unclear about what, say, the type of |
@acoglio On the rust side it returns a vec of u8 for the bytes gadget. So I believe on the Leo side it would an array of the appropriately sized array for the type of u8s. So for b1 I think the correct choice would be to have it typed as [u8; 4]. |
Implementation@gluax To finalize, this proposal can be closed by implementing:
|
Having chatted with both @Protryon and @collinc97 about this topic, as it currently stands there isn't a good way to implement these into Leo. The ideal way would be to have the Leo types as circuits or related to circuits, then have static/instance methods on that circuit that calls to some rust sided gadget implementation. However, I'd love to hear if anyone else has different ideas, but I will make this a separate proposal. |
Adding my thoughts on this thread, I think the However, from many first-hand encounters, I think the (slightly less attractive) convention of To add some evidence supporting this from other domains, we are adding this to our convention in |
I'll add an additional proposal: We could stick with the In my opinion, this approach could lead to unnecessary verbosity and hurt readability if the chaining sequence becomes too long. |
Blocked by #975. |
Due to the essence of time, the two proposed ways of implementing this quickly are:
|
Just to enhance the discussion, this would be a temporary solution for expediency. Just after DP3, we will revisit this. I also cast my vote for 2, as it seems to provide a more natural transition towards the use of scalar type methods. Type cast would have to pick either little or big endian, and do so implicitly. So my preference is to be explicit and symmetric. |
Will revisit after |
💥 Proposal bits/bytes syntax
Feature
Currently, many gadgets in Leo support a to_bit and to_bytes method on the rust side. The goal is to expose this side to Leo via some syntax. I would like to propose two different syntaxes so that we can decide between them or choose both.
Proposed Syntax 1
Coming from a rust background and something that is syntactically satisfying is the
From
implementations. So in Leo, we would have something as follows:I also believe this method would be easy to integrate into our stack. It's simply adding another statement, then at compile-time, we try actually converting the type to bits/bits with the methods provided it implements the trait. If it doesn't implement the method/trait, we can throw an error during the compiler.
Proposed Syntax 2
In contrast(or in conjunction), we could have the method approach. The goal syntactically would be to allow the call on any data type, the syntax would be as follows:
Not sure if we currently allow method calls on data types themselves, but that shouldn't be too bad. Similarly to above, we check at compile time the type can be properly converted and in the compiler, we throw an error if the type is not convertible.
The text was updated successfully, but these errors were encountered: