Add support for unsigned 8-bit integer type Byte (#2918)

This PR adds `Byte` as a builtin with builtin functions for equality,
`byte-from-nat` and `byte-to-nat`. The standard library is updated to
include this definition with instances for `FromNatural`, `Show` and
`Eq` traits.

The `FromNatural` trait means that you can assign `Byte` values 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 `UInt8` type 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-nat` cannot be
defined.

The primitive builtin ops for `Byte` are called `OpUInt8ToInt` and
`OpUInt8FromInt`, 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:

* https://github.com/anoma/juvix/issues/2865

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 297601a98dcace657aaff6e42945f1430647885b
+Subproject commit d8eea7a2038f93fa2f2100434742cd9773300b43

runtime/c/src/juvix/api.h

@@ -100,6 +100,10 @@ closure_label:
 
 #define JUVIX_ASSIGN(var0, val) (var0 = val)
 
+#define JUVIX_UINT8_TO_INT(var0, var1) (var0 = var1)
+#define JUVIX_INT_TO_UINT8(var0, var1) \
+    (var0 = make_smallint((word_t)((uint8_t)(get_unboxed_int(var1) & 0xFF))))
+
 #define JUVIX_TRACE(val) (io_trace(val))
 #define JUVIX_DUMP (stacktrace_dump())
 #define JUVIX_FAILURE(val) \

runtime/rust/juvix/src/integer.rs

@@ -38,6 +38,15 @@ pub fn smallint_le(x: Word, y: Word) -> Word {
     bool_to_word(smallint_value(x) <= smallint_value(y))
 }
 
+
+pub fn uint8_to_int(x : Word) -> Word {
+    x
+}
+
+pub fn int_to_uint8(x : Word) -> Word {
+    make_smallint(smallint_value(x).rem_euclid(256))
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -65,4 +74,12 @@ mod tests {
             assert_eq!(make_smallint(x), y);
         }
     }
+
+    #[test]
+    fn test_int_to_uint8() {
+        assert_eq!(smallint_value(int_to_uint8(make_smallint(-1))), 255);
+        assert_eq!(smallint_value(int_to_uint8(make_smallint(255))), 255);
+        assert_eq!(smallint_value(int_to_uint8(make_smallint(-256))), 0);
+        assert_eq!(smallint_value(int_to_uint8(make_smallint(256))), 0);
+    }
 }

src/Juvix/Compiler/Asm/Extra/Memory.hs

@@ -109,6 +109,7 @@ getConstantType = \case
   ConstString {} -> TyString
   ConstUnit -> TyUnit
   ConstVoid -> TyVoid
+  ConstUInt8 {} -> mkTypeUInt8
 
 getValueType' :: (Member (Error AsmError) r) => Maybe Location -> InfoTable -> Memory -> Value -> Sem r Type
 getValueType' loc tab mem = \case

src/Juvix/Compiler/Asm/Extra/Recursors.hs

@@ -189,6 +189,10 @@ recurse' sig = go True
             checkUnop mkTypeInteger TyField
           OpFieldToInt ->
             checkUnop TyField mkTypeInteger
+          OpUInt8ToInt ->
+            checkUnop mkTypeUInt8 mkTypeInteger
+          OpIntToUInt8 ->
+            checkUnop mkTypeInteger mkTypeUInt8
           where
             checkUnop :: Type -> Type -> Sem r Memory
             checkUnop ty1 ty2 = do

src/Juvix/Compiler/Backend/C/Translation/FromReg.hs

@@ -311,6 +311,8 @@ fromRegInstr bNoStack info = \case
       Reg.OpArgsNum -> "JUVIX_ARGS_NUM"
       Reg.OpFieldToInt -> unsupported "field type"
       Reg.OpIntToField -> unsupported "field type"
+      Reg.OpUInt8ToInt -> "JUVIX_UINT8_TO_INT"
+      Reg.OpIntToUInt8 -> "JUVIX_INT_TO_UINT8"
 
     fromVarRef :: Reg.VarRef -> Expression
     fromVarRef Reg.VarRef {..} =
@@ -347,6 +349,7 @@ fromRegInstr bNoStack info = \case
       Reg.ConstString x -> macroCall "GET_CONST_CSTRING" [integer (getStringId info x)]
       Reg.ConstUnit -> macroVar "OBJ_UNIT"
       Reg.ConstVoid -> macroVar "OBJ_VOID"
+      Reg.ConstUInt8 x -> macroCall "make_smallint" [integer x]
 
     fromPrealloc :: Reg.InstrPrealloc -> Statement
     fromPrealloc Reg.InstrPrealloc {..} =

src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs

@@ -205,6 +205,14 @@ fromRegInstr info = \case
           (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg])
       Reg.OpFieldToInt -> unsupported "field type"
       Reg.OpIntToField -> unsupported "field type"
+      Reg.OpUInt8ToInt ->
+        stmtAssign
+          (mkVarRef _instrUnopResult)
+          (mkCall "uint8_to_int" [fromValue _instrUnopArg])
+      Reg.OpIntToUInt8 ->
+        stmtAssign
+          (mkVarRef _instrUnopResult)
+          (mkCall "int_to_uint8" [fromValue _instrUnopArg])
 
     mkVarRef :: Reg.VarRef -> Text
     mkVarRef Reg.VarRef {..} = case _varRefGroup of
@@ -242,6 +250,7 @@ fromRegInstr info = \case
       Reg.ConstString {} -> unsupported "strings"
       Reg.ConstUnit -> mkVar "OBJ_UNIT"
       Reg.ConstVoid -> mkVar "OBJ_VOID"
+      Reg.ConstUInt8 x -> mkCall "make_smallint" [mkInteger x]
 
     fromAlloc :: Reg.InstrAlloc -> [Statement]
     fromAlloc Reg.InstrAlloc {..} =

src/Juvix/Compiler/Builtins.hs

@@ -12,11 +12,13 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.Control,
     module Juvix.Compiler.Builtins.Anoma,
     module Juvix.Compiler.Builtins.Cairo,
+    module Juvix.Compiler.Builtins.Byte,
   )
 where
 
 import Juvix.Compiler.Builtins.Anoma
 import Juvix.Compiler.Builtins.Bool
+import Juvix.Compiler.Builtins.Byte
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug

src/Juvix/Compiler/Builtins/Byte.hs

@@ -0,0 +1,32 @@
+module Juvix.Compiler.Builtins.Byte where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerByte :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByte d = do
+  unless (isSmallUniverse' (d ^. axiomType)) (error "Byte should be in the small universe")
+  registerBuiltin BuiltinByte (d ^. axiomName)
+
+registerByteEq :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteEq f = do
+  byte_ <- getBuiltinName (getLoc f) BuiltinByte
+  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  unless (f ^. axiomType === (byte_ --> byte_ --> bool_)) (error "Byte equality has the wrong type signature")
+  registerBuiltin BuiltinByteEq (f ^. axiomName)
+
+registerByteFromNat :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteFromNat d = do
+  let l = getLoc d
+  byte_ <- getBuiltinName l BuiltinByte
+  nat <- getBuiltinName l BuiltinNat
+  unless (d ^. axiomType === (nat --> byte_)) (error "byte-from-nat has the wrong type signature")
+  registerBuiltin BuiltinByteFromNat (d ^. axiomName)
+
+registerByteToNat :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerByteToNat f = do
+  byte_ <- getBuiltinName (getLoc f) BuiltinByte
+  nat_ <- getBuiltinName (getLoc f) BuiltinNat
+  unless (f ^. axiomType === (byte_ --> nat_)) (error "byte-to-nat has the wrong type signature")
+  registerBuiltin BuiltinByteToNat (f ^. axiomName)

src/Juvix/Compiler/Casm/Translation/FromReg.hs

@@ -249,6 +249,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           Reg.ConstUnit -> 0
           Reg.ConstVoid -> 0
           Reg.ConstString {} -> unsupported "strings"
+          Reg.ConstUInt8 {} -> unsupported "uint8"
 
         mkLoad :: Reg.ConstrField -> Sem r RValue
         mkLoad Reg.ConstrField {..} = do
@@ -458,6 +459,8 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI
           Reg.OpFieldToInt -> goAssignValue _instrUnopResult _instrUnopArg
           Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg
           Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg
+          Reg.OpUInt8ToInt -> unsupported "OpUInt8ToInt"
+          Reg.OpIntToUInt8 -> unsupported "OpIntToUInt8"
 
         goCairo :: Reg.InstrCairo -> Sem r ()
         goCairo Reg.InstrCairo {..} = case _instrCairoOpcode of

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -218,6 +218,10 @@ data BuiltinAxiom
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
+  | BuiltinByte
+  | BuiltinByteEq
+  | BuiltinByteToNat
+  | BuiltinByteFromNat
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance HasNameKind BuiltinAxiom where
@@ -255,6 +259,10 @@ instance HasNameKind BuiltinAxiom where
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
+    BuiltinByte -> KNameInductive
+    BuiltinByteEq -> KNameFunction
+    BuiltinByteToNat -> KNameFunction
+    BuiltinByteFromNat -> KNameFunction
 
   getNameKindPretty :: BuiltinAxiom -> NameKind
   getNameKindPretty = getNameKind
@@ -300,6 +308,10 @@ instance Pretty BuiltinAxiom where
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint
+    BuiltinByte -> Str.byte_
+    BuiltinByteEq -> Str.byteEq
+    BuiltinByteToNat -> Str.byteToNat
+    BuiltinByteFromNat -> Str.byteFromNat
 
 data BuiltinType
   = BuiltinTypeInductive BuiltinInductive

src/Juvix/Compiler/Core/Evaluator.hs

@@ -213,6 +213,8 @@ geval opts herr tab env0 = eval' env0
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
+      OpUInt8ToInt -> uint8ToIntOp
+      OpUInt8FromInt -> uint8FromIntOp
       where
         err :: Text -> a
         err msg = evalError msg n
@@ -509,6 +511,28 @@ geval opts herr tab env0 = eval' env0
               !publicKey = publicKeyFromInteger publicKeyInt
            in nodeFromBool (E.dverify publicKey message sig)
         {-# INLINE verifyDetached #-}
+
+        uint8FromIntOp :: [Node] -> Node
+        uint8FromIntOp =
+          unary $ \node ->
+            let !v = eval' env node
+             in nodeFromUInt8
+                  . fromIntegral
+                  . fromMaybe (evalError "expected integer" v)
+                  . integerFromNode
+                  $ v
+        {-# INLINE uint8FromIntOp #-}
+
+        uint8ToIntOp :: [Node] -> Node
+        uint8ToIntOp =
+          unary $ \node ->
+            let !v = eval' env node
+             in nodeFromInteger
+                  . toInteger
+                  . fromMaybe (evalError "expected uint8" v)
+                  . uint8FromNode
+                  $ v
+        {-# INLINE uint8ToIntOp #-}
     {-# INLINE applyBuiltin #-}
 
     -- secretKey, publicKey are not encoded with their length as
@@ -530,6 +554,10 @@ geval opts herr tab env0 = eval' env0
     nodeFromField !fld = mkConstant' (ConstField fld)
     {-# INLINE nodeFromField #-}
 
+    nodeFromUInt8 :: Word8 -> Node
+    nodeFromUInt8 !w = mkConstant' (ConstUInt8 w)
+    {-# INLINE nodeFromUInt8 #-}
+
     nodeFromBool :: Bool -> Node
     nodeFromBool b = mkConstr' (BuiltinTag tag) []
       where
@@ -577,6 +605,12 @@ geval opts herr tab env0 = eval' env0
       _ -> Nothing
     {-# INLINE fieldFromNode #-}
 
+    uint8FromNode :: Node -> Maybe Word8
+    uint8FromNode = \case
+      NCst (Constant _ (ConstUInt8 i)) -> Just i
+      _ -> Nothing
+    {-# INLINE uint8FromNode #-}
+
     printNode :: Node -> Text
     printNode = \case
       NCst (Constant _ (ConstString s)) -> s

src/Juvix/Compiler/Core/Extra/Base.hs

@@ -194,6 +194,12 @@ mkTypeField i = mkTypePrim i PrimField
 mkTypeField' :: Type
 mkTypeField' = mkTypeField Info.empty
 
+mkTypeUInt8 :: Info -> Type
+mkTypeUInt8 i = mkTypePrim i primitiveUInt8
+
+mkTypeUInt8' :: Type
+mkTypeUInt8' = mkTypeUInt8 Info.empty
+
 mkDynamic :: Info -> Type
 mkDynamic i = NDyn (DynamicTy i)
 

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -433,6 +433,8 @@ builtinOpArgTypes = \case
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []
+  OpUInt8ToInt -> [mkTypeUInt8']
+  OpUInt8FromInt -> [mkTypeInteger']
 
 translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
 translateCase translateIfFun dflt Case {..} = case _caseBranches of

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -36,6 +36,8 @@ data BuiltinOp
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
+  | OpUInt8ToInt
+  | OpUInt8FromInt
   deriving stock (Eq, Generic)
 
 instance Serialize BuiltinOp
@@ -90,6 +92,8 @@ builtinOpArgsNum = \case
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
+  OpUInt8ToInt -> 1
+  OpUInt8FromInt -> 1
 
 builtinConstrArgsNum :: BuiltinDataTag -> Int
 builtinConstrArgsNum = \case
@@ -133,6 +137,8 @@ builtinIsFoldable = \case
   OpPoseidonHash -> False
   OpEc -> False
   OpRandomEcPoint -> False
+  OpUInt8ToInt -> True
+  OpUInt8FromInt -> True
 
 builtinIsCairo :: BuiltinOp -> Bool
 builtinIsCairo op = op `elem` builtinsCairo
@@ -156,3 +162,6 @@ builtinsAnoma =
     OpAnomaVerifyWithMessage,
     OpAnomaSignDetached
   ]
+
+builtinsUInt8 :: [BuiltinOp]
+builtinsUInt8 = [OpUInt8FromInt, OpUInt8ToInt]

src/Juvix/Compiler/Core/Language/Nodes.hs

@@ -38,6 +38,7 @@ data ConstantValue
   = ConstInteger !Integer
   | ConstField !FField
   | ConstString !Text
+  | ConstUInt8 !Word8
   deriving stock (Eq, Generic)
 
 -- | Info about a single binder. Associated with Lambda, Pi, Let, Case or Match.

src/Juvix/Compiler/Core/Language/Primitives.hs

@@ -17,6 +17,15 @@ data Primitive
   | PrimField
   deriving stock (Eq, Generic)
 
+primitiveUInt8 :: Primitive
+primitiveUInt8 =
+  PrimInteger
+    ( PrimIntegerInfo
+        { _infoMinValue = Just 0,
+          _infoMaxValue = Just 255
+        }
+    )
+
 -- | Info about a type represented as an integer.
 data PrimIntegerInfo = PrimIntegerInfo
   { _infoMinValue :: Maybe Integer,

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -62,6 +62,8 @@ instance PrettyCode BuiltinOp where
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
+    OpUInt8ToInt -> return primUInt8ToInt
+    OpUInt8FromInt -> return primFieldFromInt
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case
@@ -107,6 +109,8 @@ instance PrettyCode ConstantValue where
       return $ annotate AnnLiteralInteger (pretty int)
     ConstField fld ->
       return $ annotate AnnLiteralInteger (pretty fld)
+    ConstUInt8 i ->
+      return $ annotate AnnLiteralInteger (pretty i)
     ConstString txt ->
       return $ annotate AnnLiteralString (pretty (show txt :: String))
 
@@ -114,6 +118,8 @@ instance PrettyCode (Constant' i) where
   ppCode Constant {..} = case _constantValue of
     ConstField fld ->
       return $ annotate AnnLiteralInteger (pretty fld <> "F")
+    ConstUInt8 i ->
+      return $ annotate AnnLiteralInteger (pretty i <> "u8")
     _ -> ppCode _constantValue
 
 instance (PrettyCode a, HasAtomicity a) => PrettyCode (App' i a) where
@@ -732,6 +738,12 @@ primFieldDiv = primitive Str.fdiv
 primFieldFromInt :: Doc Ann
 primFieldFromInt = primitive Str.itof
 
+primUInt8ToInt :: Doc Ann
+primUInt8ToInt = primitive Str.u8toi
+
+primUInt8FromInt :: Doc Ann
+primUInt8FromInt = primitive Str.itou8
+
 primFieldToInt :: Doc Ann
 primFieldToInt = primitive Str.ftoi
 

src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs

@@ -12,7 +12,7 @@ checkCairo md = do
   checkMainType
   checkNoAxioms md
   mapAllNodesM checkNoIO md
-  mapAllNodesM (checkBuiltins' builtinsString [PrimString]) md
+  mapAllNodesM (checkBuiltins' (builtinsString ++ builtinsUInt8) [PrimString, primitiveUInt8]) md
   where
     checkMainType :: Sem r ()
     checkMainType =

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -34,6 +34,7 @@ computeNodeTypeInfo md = umapL go
           ConstInteger {} -> mkTypeInteger'
           ConstField {} -> mkTypeField'
           ConstString {} -> mkTypeString'
+          ConstUInt8 {} -> mkTypeUInt8'
       NApp {} ->
         let (fn, args) = unfoldApps' node
             fty = Info.getNodeType fn
@@ -82,6 +83,8 @@ computeNodeTypeInfo md = umapL go
           OpRandomEcPoint -> case _builtinAppArgs of
             [] -> mkDynamic'
             _ -> error "incorrect random_ec_point builtin application"
+          OpUInt8ToInt -> mkTypeInteger'
+          OpUInt8FromInt -> mkTypeUInt8'
       NCtr Constr {..} ->
         let ci = lookupConstructorInfo md _constrTag
             ii = lookupInductiveInfo md (ci ^. constructorInductive)

src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs

@@ -19,6 +19,7 @@ convertNode md = umap go
           Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger'
           Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString'
           Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField'
+          Just (BuiltinTypeAxiom BuiltinByte) -> mkTypeUInt8'
           _ -> node
         where
           ii = lookupInductiveInfo md _typeConstrSymbol

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -614,6 +614,10 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
+      Internal.BuiltinByte -> registerInductiveAxiom (Just BuiltinByte) []
+      Internal.BuiltinByteEq -> return ()
+      Internal.BuiltinByteToNat -> return ()
+      Internal.BuiltinByteFromNat -> return ()
 
     registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
     registerInductiveAxiom ax ctrs = do
@@ -815,6 +819,13 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
           $ mkBuiltinApp' OpEc [mkVar' 2, mkVar' 1, mkVar' 0]
       Internal.BuiltinRandomEcPoint -> do
         registerAxiomDef (mkBuiltinApp' OpRandomEcPoint [])
+      Internal.BuiltinByte -> return ()
+      Internal.BuiltinByteEq ->
+        registerAxiomDef (mkLambda' mkTypeUInt8' (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinByteToNat ->
+        registerAxiomDef (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpUInt8ToInt [mkVar' 0]))
+      Internal.BuiltinByteFromNat ->
+        registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpUInt8FromInt [mkVar' 0]))
 
     axiomType' :: Sem r Type
     axiomType' = fromTopIndex (goType (a ^. Internal.axiomType))
@@ -1212,6 +1223,10 @@ goApplication a = do
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app
+        Just Internal.BuiltinByte -> app
+        Just Internal.BuiltinByteEq -> app
+        Just Internal.BuiltinByteToNat -> app
+        Just Internal.BuiltinByteFromNat -> app
         Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
       funInfoBuiltin <- Internal.getFunctionBuiltinInfo n

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -599,6 +599,7 @@ atom ::
   ParsecS r Node
 atom varsNum vars =
   exprConstField
+    <|> exprConstUInt8
     <|> exprConstInt
     <|> exprConstString
     <|> exprUniverse
@@ -630,6 +631,11 @@ exprConstField = P.try $ do
   (n, i) <- field
   return $ mkConstant (Info.singleton (LocationInfo i)) (ConstField (fieldFromInteger defaultFieldSize n))
 
+exprConstUInt8 :: ParsecS r Node
+exprConstUInt8 = P.try $ do
+  (n, i) <- uint8
+  return $ mkConstant (Info.singleton (LocationInfo i)) (ConstUInt8 (fromIntegral n))
+
 exprUniverse :: ParsecS r Type
 exprUniverse = do
   kw kwType

src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs

@@ -30,6 +30,9 @@ kw = void . lexeme . kw'
 field :: ParsecS r (Integer, Interval)
 field = lexemeInterval field'
 
+uint8 :: ParsecS r (Integer, Interval)
+uint8 = lexemeInterval uint8'
+
 integer :: ParsecS r (WithLoc Integer)
 integer = lexeme integer'
 

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -108,6 +108,10 @@ fromCore fsize tab =
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False
+        BuiltinByte -> False
+        BuiltinByteEq -> False
+        BuiltinByteToNat -> False
+        BuiltinByteFromNat -> False
       BuiltinTypeInductive i -> case i of
         BuiltinList -> True
         BuiltinMaybe -> True

src/Juvix/Compiler/Internal/Language.hs

@@ -170,9 +170,9 @@ data Literal
   = LitString Text
   | -- | `LitNumeric` represents a numeric literal of undetermined type
     LitNumeric Integer
-  | -- | `LitInteger` represents a literal of type `Int`
+  | -- | `LitInteger` represents a literal with trait `Integral`
     LitInteger Integer
-  | -- | `LitNatural` represents a literal of type `Nat`
+  | -- | `LitNatural` represents a literal with trait `FromNatural`
     LitNatural Integer
   deriving stock (Show, Eq, Ord, Generic, Data)
 

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -587,6 +587,10 @@ registerBuiltinAxiom d = \case
   BuiltinPoseidon -> registerPoseidon d
   BuiltinEcOp -> registerEcOp d
   BuiltinRandomEcPoint -> registerRandomEcPoint d
+  BuiltinByte -> registerByte d
+  BuiltinByteEq -> registerByteEq d
+  BuiltinByteToNat -> registerByteToNat d
+  BuiltinByteFromNat -> registerByteFromNat d
 
 goInductive ::
   (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) =>

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -440,6 +440,7 @@ compile = \case
       Tree.ConstUnit -> OpQuote # constUnit
       Tree.ConstVoid -> OpQuote # constVoid
       Tree.ConstField {} -> fieldErr
+      Tree.ConstUInt8 i -> nockIntegralLiteral i
 
     goConstString :: Text -> Term Natural
     goConstString t =
@@ -508,6 +509,8 @@ compile = \case
          in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum)
       Tree.OpIntToField -> fieldErr
       Tree.OpFieldToInt -> fieldErr
+      Tree.OpIntToUInt8 -> intToUInt8 arg
+      Tree.OpUInt8ToInt -> arg
 
     goAnomaGet :: [Term Natural] -> Sem r (Term Natural)
     goAnomaGet key = do
@@ -1183,3 +1186,9 @@ add a b = callStdlib StdlibAdd [a, b]
 
 dec :: Term Natural -> Term Natural
 dec = callStdlib StdlibDec . pure
+
+intToUInt8 :: Term Natural -> Term Natural
+intToUInt8 i = callStdlib StdlibMod [i, nockIntegralLiteral @Natural (2 ^ uint8Size)]
+  where
+    uint8Size :: Natural
+    uint8Size = 8

src/Juvix/Compiler/Tree/Evaluator.hs

@@ -231,6 +231,7 @@ valueToNode = \case
           _nodeAllocClosureFunSymbol = _closureSymbol,
           _nodeAllocClosureArgs = map valueToNode _closureArgs
         }
+  ValUInt8 i -> mkConst $ ConstUInt8 i
 
 hEvalIO :: (MonadIO m) => Handle -> Handle -> InfoTable -> FunctionInfo -> m Value
 hEvalIO hin hout infoTable funInfo = do

src/Juvix/Compiler/Tree/Evaluator/Builtins.hs

@@ -63,6 +63,8 @@ evalUnop tab op v = case op of
   OpFieldToInt -> goFieldToInt v
   OpIntToField -> goIntToField v
   OpArgsNum -> goArgsNum v
+  OpUInt8ToInt -> goUInt8ToInt v
+  OpIntToUInt8 -> goIntToUInt8 v
   where
     strToInt :: Text -> Either ErrorMsg Value
     strToInt s = case T.readMaybe (fromText s) of
@@ -100,6 +102,20 @@ evalUnop tab op v = case op of
       _ ->
         Left "expected an integer"
 
+    goIntToUInt8 :: Value -> Either ErrorMsg Value
+    goIntToUInt8 = \case
+      ValInteger i ->
+        Right $ ValUInt8 $ fromIntegral i
+      _ ->
+        Left "expected an integer"
+
+    goUInt8ToInt :: Value -> Either ErrorMsg Value
+    goUInt8ToInt = \case
+      ValUInt8 i ->
+        Right $ ValInteger $ toInteger i
+      _ ->
+        Left "expected a uint8"
+
 printValue :: InfoTable' t e -> Value -> Text
 printValue tab = \case
   ValString s -> s
@@ -113,6 +129,7 @@ constantToValue = \case
   ConstString s -> ValString s
   ConstUnit -> ValUnit
   ConstVoid -> ValVoid
+  ConstUInt8 i -> ValUInt8 i
 
 valueToConstant :: Value -> Constant
 valueToConstant = \case
@@ -122,6 +139,7 @@ valueToConstant = \case
   ValString s -> ConstString s
   ValUnit -> ConstUnit
   ValVoid -> ConstVoid
+  ValUInt8 i -> ConstUInt8 i
   _ -> impossible
 
 evalBinop' :: BinaryOp -> Constant -> Constant -> Either ErrorMsg Constant

src/Juvix/Compiler/Tree/Extra/Type.hs

@@ -14,6 +14,9 @@ import Juvix.Compiler.Tree.Pretty
 mkTypeInteger :: Type
 mkTypeInteger = TyInteger (TypeInteger Nothing Nothing)
 
+mkTypeUInt8 :: Type
+mkTypeUInt8 = TyInteger (TypeInteger (Just 0) (Just 255))
+
 mkTypeBool :: Type
 mkTypeBool = TyBool (TypeBool (BuiltinTag TagTrue) (BuiltinTag TagFalse))
 

src/Juvix/Compiler/Tree/Language/Base.hs

@@ -18,6 +18,7 @@ data Constant
   | ConstField FField
   | ConstUnit
   | ConstVoid
+  | ConstUInt8 Word8
   deriving stock (Eq, Generic)
 
 instance (Hashable Constant)

src/Juvix/Compiler/Tree/Language/Builtins.hs

@@ -47,6 +47,10 @@ data UnaryOp
     OpIntToField
   | -- | Convert a field element to an integer. JV* opcode: `ftoi`.
     OpFieldToInt
+  | -- | Convert an integer to a UInt8. JV* opcode: `itou8`
+    OpIntToUInt8
+  | -- | Convert an UInt8 to an integer. JV* opcode: `u8toi`
+    OpUInt8ToInt
   | -- | Compute the number of expected arguments for the given closure. JV*
     -- opcode: `argsnum`.
     OpArgsNum

src/Juvix/Compiler/Tree/Language/Value.hs

@@ -23,6 +23,7 @@ data Value
   | ValVoid
   | ValConstr Constr
   | ValClosure Closure
+  | ValUInt8 Word8
   deriving stock (Eq)
 
 data Constr = Constr
@@ -60,3 +61,4 @@ instance HasAtomicity Value where
     ValVoid -> Atom
     ValConstr c -> atomicity c
     ValClosure cl -> atomicity cl
+    ValUInt8 {} -> Atom

src/Juvix/Compiler/Tree/Pretty/Base.hs

@@ -99,6 +99,8 @@ instance PrettyCode Value where
       ppCode c
     ValClosure cl ->
       ppCode cl
+    ValUInt8 i ->
+      return $ integer i
 
 instance PrettyCode TypeInductive where
   ppCode :: (Member (Reader Options) r) => TypeInductive -> Sem r (Doc Ann)
@@ -197,6 +199,8 @@ instance PrettyCode Constant where
       return $ annotate (AnnKind KNameConstructor) Str.unit
     ConstVoid {} ->
       return $ annotate (AnnKind KNameConstructor) Str.void
+    ConstUInt8 v ->
+      return $ annotate AnnLiteralInteger (pretty v)
 
 instance PrettyCode BoolOp where
   ppCode op = return $ primitive $ case op of
@@ -239,6 +243,8 @@ instance PrettyCode UnaryOp where
     OpFieldToInt -> Str.instrFieldToInt
     OpIntToField -> Str.instrIntToField
     OpArgsNum -> Str.instrArgsNum
+    OpIntToUInt8 -> Str.instrIntToUInt8
+    OpUInt8ToInt -> Str.instrUInt8ToInt
 
 instance PrettyCode CairoOp where
   ppCode op = return $ primitive $ case op of

src/Juvix/Compiler/Tree/Transformation/Validate.hs

@@ -82,6 +82,8 @@ inferType tab funInfo = goInfer mempty
           OpArgsNum -> checkUnop TyDynamic mkTypeInteger
           OpIntToField -> checkUnop mkTypeInteger TyField
           OpFieldToInt -> checkUnop TyField mkTypeInteger
+          OpUInt8ToInt -> checkUnop mkTypeUInt8 mkTypeInteger
+          OpIntToUInt8 -> checkUnop mkTypeInteger mkTypeUInt8
 
     goCairo :: BinderList Type -> NodeCairo -> Sem r Type
     goCairo bl NodeCairo {..} = do
@@ -101,6 +103,7 @@ inferType tab funInfo = goInfer mempty
       ConstField {} -> return TyField
       ConstUnit {} -> return TyUnit
       ConstVoid {} -> return TyVoid
+      ConstUInt8 {} -> return mkTypeUInt8
 
     goMemRef :: BinderList Type -> NodeMemRef -> Sem r Type
     goMemRef bl NodeMemRef {..} = case _nodeMemRef of

src/Juvix/Compiler/Tree/Translation/FromCore.hs

@@ -85,6 +85,8 @@ genCode infoTable fi =
         mkConst (ConstString s)
       Core.Constant _ (Core.ConstField fld) ->
         mkConst (ConstField fld)
+      Core.Constant _ (Core.ConstUInt8 i) ->
+        mkConst (ConstUInt8 i)
 
     goApps :: Int -> BinderList MemRef -> Core.Apps -> Node
     goApps tempSize refs Core.Apps {..} =
@@ -302,6 +304,8 @@ genCode infoTable fi =
       Core.OpFieldToInt -> PrimUnop OpFieldToInt
       Core.OpTrace -> OpTrace
       Core.OpFail -> OpFail
+      Core.OpUInt8FromInt -> PrimUnop OpIntToUInt8
+      Core.OpUInt8ToInt -> PrimUnop OpUInt8ToInt
       _ -> impossible
 
     genCairoOp :: Core.BuiltinOp -> CairoOp

src/Juvix/Extra/Strings.hs

@@ -173,6 +173,18 @@ error = "error"
 string :: (IsString s) => s
 string = "string"
 
+byte_ :: (IsString s) => s
+byte_ = "byte"
+
+byteEq :: (IsString s) => s
+byteEq = "byte-eq"
+
+byteToNat :: (IsString s) => s
+byteToNat = "byte-to-nat"
+
+byteFromNat :: (IsString s) => s
+byteFromNat = "byte-from-nat"
+
 nat :: (IsString s) => s
 nat = "nat"
 
@@ -389,6 +401,12 @@ ftoi = "ftoi"
 itof :: (IsString s) => s
 itof = "itof"
 
+u8toi :: (IsString s) => s
+u8toi = "u8toi"
+
+itou8 :: (IsString s) => s
+itou8 = "itou8"
+
 delimiter :: (IsString s) => s
 delimiter = "delimiter"
 
@@ -770,6 +788,12 @@ instrFieldToInt = "ftoi"
 instrIntToField :: (IsString s) => s
 instrIntToField = "itof"
 
+instrUInt8ToInt :: (IsString s) => s
+instrUInt8ToInt = "u8toi"
+
+instrIntToUInt8 :: (IsString s) => s
+instrIntToUInt8 = "itou8"
+
 instrShow :: (IsString s) => s
 instrShow = "show"
 

src/Juvix/Parser/Lexer.hs

@@ -166,6 +166,12 @@ field' = do
   P.chunk "F"
   return d
 
+uint8' :: ParsecS r Integer
+uint8' = do
+  d <- L.decimal
+  P.chunk "u8"
+  return d
+
 -- | The caller is responsible of consuming space after it.
 delim' :: Text -> ParsecS r Interval
 delim' d = P.label (unpack d) . fmap snd . interval $ chunk d

test/Anoma/Compilation/Positive.hs

@@ -594,5 +594,23 @@ allTests =
             [nock| 2 |],
             [nock| 3 |],
             [nock| nil |]
+          ],
+      mkAnomaCallTest
+        "Test081: UInt8"
+        $(mkRelDir ".")
+        $(mkRelFile "test081.juvix")
+        []
+        $ checkOutput
+          [ [nock| 1 |],
+            [nock| 255 |],
+            [nock| 2 |],
+            [nock| true |],
+            [nock| true |],
+            [nock| false |],
+            [nock| 1 |],
+            [nock| 238 |],
+            [nock| 3 |],
+            [nock| 240 |],
+            [nock| [1 238 3 2 nil] |]
           ]
     ]

test/Compilation/Positive.hs

@@ -460,5 +460,10 @@ tests =
         "Test077: Instance fields"
         $(mkRelDir ".")
         $(mkRelFile "test077.juvix")
-        $(mkRelFile "out/test077.out")
+        $(mkRelFile "out/test077.out"),
+      posTestEval
+        "Test078: Builtin Byte"
+        $(mkRelDir ".")
+        $(mkRelFile "test078.juvix")
+        $(mkRelFile "out/test078.out")
     ]

test/Rust/Compilation/Positive.hs

@@ -344,5 +344,10 @@ tests =
         "Test073: Import and use a syntax alias"
         $(mkRelDir "test073")
         $(mkRelFile "test073.juvix")
-        $(mkRelFile "out/test073.out")
+        $(mkRelFile "out/test073.out"),
+      posTest
+        "Test074: Builtin Byte"
+        $(mkRelDir ".")
+        $(mkRelFile "test074.juvix")
+        $(mkRelFile "out/test074.out")
     ]

tests/Anoma/Compilation/positive/test081.juvix

@@ -0,0 +1,35 @@
+module test081;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Trace open;
+
+n1 : Byte := fromNat 1;
+
+n2 : Byte := fromNat 0xff;
+
+n3 : Byte := fromNat 0x102;
+
+l1 : Byte := 1;
+
+l2 : Byte := 0xee;
+
+l3 : Byte := 0x103;
+
+xs : List Byte := [l1; l2; l3; 2];
+
+printByteLn : Byte -> IO := Show.show >> printStringLn;
+
+printListByteLn : List Byte -> IO := Show.show >> printStringLn;
+
+main : List Byte :=
+  trace n1
+    >-> trace n2
+    >-> trace n3
+    >-> trace (n1 == l1)
+    >-> trace (l1 == 0x101)
+    >-> trace (l2 == n2)
+    >-> trace (Byte.toNat l1)
+    >-> trace (Byte.toNat l2)
+    >-> trace (Byte.toNat l3)
+    >-> trace (Byte.toNat 0xf0)
+    >-> xs;

tests/Compilation/positive/out/test078.out

@@ -0,0 +1,11 @@
+1
+255
+2
+true
+true
+false
+1
+238
+3
+240
+(1 :: 238 :: 3 :: 2 :: nil)

tests/Compilation/positive/test078.juvix

@@ -0,0 +1,34 @@
+module test078;
+
+import Stdlib.Prelude open;
+
+n1 : Byte := fromNat 1;
+
+n2 : Byte := fromNat 0xff;
+
+n3 : Byte := fromNat 0x102;
+
+l1 : Byte := 1;
+
+l2 : Byte := 0xee;
+
+l3 : Byte := 0x103;
+
+xs : List Byte := [l1; l2; l3; 2];
+
+printByteLn : Byte -> IO := Show.show >> printStringLn;
+
+printListByteLn : List Byte -> IO := Show.show >> printStringLn;
+
+main : IO :=
+  printByteLn n1
+    >>> printByteLn n2
+    >>> printByteLn n3
+    >>> printBoolLn (n1 == l1)
+    >>> printBoolLn (l1 == 0x101)
+    >>> printBoolLn (l2 == n2)
+    >>> printNatLn (Byte.toNat l1)
+    >>> printNatLn (Byte.toNat l2)
+    >>> printNatLn (Byte.toNat l3)
+    >>> printNatLn (Byte.toNat 0xf0)
+    >>> printListByteLn xs;

tests/Core/positive/out/test063.out

@@ -0,0 +1 @@
+1

tests/Core/positive/test063.jvc

@@ -0,0 +1,5 @@
+-- UInt8
+
+def f := \x x;
+
+f 257u8

tests/Rust/Compilation/positive/out/test074.out

@@ -1 +1 @@
--1085550836599839364109196834928521031686932164599479009991927616840761606155
+2

tests/Rust/Compilation/positive/test074.juvix

@@ -0,0 +1,7 @@
+module test074;
+
+import Stdlib.Prelude open;
+
+n1 : Byte := Byte.fromNat 0xff;
+
+main : Byte := Byte.fromNat (Byte.toNat 0x103 + Byte.toNat n1);