Add support for unsigned 8-bit integer type Byte #2918
Conversation
paulcadman
force-pushed
the
support-uint8
branch
5 times, most recently
from
43f4fd5 to
5bba06b
Compare
paulcadman
changed the title
paulcadman
force-pushed
the
support-uint8
branch
from
17872b0 to
53aab60
Compare
paulcadman
force-pushed
the
support-uint8
branch
from
683e77f to
6126fe1
Compare
paulcadman
force-pushed
the
support-uint8
branch
from
219c43b to
da033e4
Compare
paulcadman
requested review from
lukaszcz and
janmasrovira
and removed request for
lukaszcz
Support is only provided in the Core and Anoma backends currently
The IntMod op is not availble in the Cairo VM
paulcadman
force-pushed
the
support-uint8
branch
from
cb49398 to
04b0df9
Compare
src/Juvix/Compiler/Core/Evaluator.hs
Outdated
| let !v = eval' env node | ||
| in nodeFromInteger | ||
| . toInteger | ||
| . fromMaybe (evalError "expected field element" v) |
| LitInteger Integer | ||
| | -- | `LitNatural` represents a literal of type `Nat` | ||
| | -- | `LitNatural` represents a literal with trait `Natural` | ||
| LitNatural Integer |
There was a problem hiding this comment.
So what happens with numeric literals that are bytes? What are they converted to during type checking?
There was a problem hiding this comment.
The way that literals work in type checking is here:
For a non-negative literal n the typechecker runs type inference on the literal wrapped in fromNat from the FromNatural trait:
fromNat {_} {{_}} `n`
The Byte type is then obtained via instance resolution.
This is why I updated the documentation for LitInteger and LitNatural to refer to traits rather than to types.
There was a problem hiding this comment.
Ah, OK, they have an instance of Natural?
There was a problem hiding this comment.
The trait name in the comment should be FromNatural then.
|
|
||
| n1 : Byte := fromNat 1; | ||
|
|
||
| n2 : Byte := fromNat 0xff; |
There was a problem hiding this comment.
Do we need fromNat here? Isn't it supposed to be inserted automatically?
There was a problem hiding this comment.
It's not needed - just below these are examples without fromNat. I wanted to cover using fromNat explicitly in the test.
>⚠️ Depends on: > * #117 > * anoma/juvix#2918 Adds support for the builtin Byte type introduced in: * anoma/juvix#2918
This PR adds
Byteas a builtin with builtin functions for equality,byte-from-natandbyte-to-nat. The standard library is updated to include this definition with instances forFromNatural,ShowandEqtraits.The
FromNaturaltrait means that you can assignBytevalues using non-negative numeric literals.You can use byte literals in jvc files by adding the u8 suffix to a numeric value. For example, 1u8 represents a byte literal.
Arithmetic is not supported as the intention is for this type to be used to construct ByteArrays of data where isn't not appropriate to modify using arithmetic operations. We may add a separate
UInt8type in the future which supports arithmetic.The Byte is supported in the native, rust and Anoma backend. Byte is not supported in the Cairo backend because
byte-from-natcannot be defined.The primitive builtin ops for
Byteare calledOpUInt8ToIntandOpUInt8FromInt, named because these ops work on integers and in future we may reuse these for a separate unsigned 8-bit integer type that supports arithmetic.Part of: