From e2fe830d280d2b07f8d95da726b82b6ff8af7831 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Fri, 2 Aug 2024 07:43:24 +0100
Subject: [PATCH] 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                                  |  2 +-
 runtime/c/src/juvix/api.h                     |  4 +++
 runtime/rust/juvix/src/integer.rs             | 17 +++++++++
 src/Juvix/Compiler/Asm/Extra/Memory.hs        |  1 +
 src/Juvix/Compiler/Asm/Extra/Recursors.hs     |  4 +++
 .../Compiler/Backend/C/Translation/FromReg.hs |  3 ++
 .../Backend/Rust/Translation/FromReg.hs       |  9 +++++
 src/Juvix/Compiler/Builtins.hs                |  2 ++
 src/Juvix/Compiler/Builtins/Byte.hs           | 32 +++++++++++++++++
 .../Compiler/Casm/Translation/FromReg.hs      |  3 ++
 src/Juvix/Compiler/Concrete/Data/Builtins.hs  | 12 +++++++
 src/Juvix/Compiler/Core/Evaluator.hs          | 34 ++++++++++++++++++
 src/Juvix/Compiler/Core/Extra/Base.hs         |  6 ++++
 src/Juvix/Compiler/Core/Extra/Utils.hs        |  2 ++
 src/Juvix/Compiler/Core/Language/Builtins.hs  |  9 +++++
 src/Juvix/Compiler/Core/Language/Nodes.hs     |  1 +
 .../Compiler/Core/Language/Primitives.hs      |  9 +++++
 src/Juvix/Compiler/Core/Pretty/Base.hs        | 12 +++++++
 .../Core/Transformation/Check/Cairo.hs        |  2 +-
 .../Core/Transformation/ComputeTypeInfo.hs    |  3 ++
 .../Transformation/ConvertBuiltinTypes.hs     |  1 +
 .../Compiler/Core/Translation/FromInternal.hs | 15 ++++++++
 .../Compiler/Core/Translation/FromSource.hs   |  6 ++++
 .../Core/Translation/FromSource/Lexer.hs      |  3 ++
 .../Core/Translation/Stripped/FromCore.hs     |  4 +++
 src/Juvix/Compiler/Internal/Language.hs       |  4 +--
 .../Internal/Translation/FromConcrete.hs      |  4 +++
 .../Compiler/Nockma/Translation/FromTree.hs   |  9 +++++
 src/Juvix/Compiler/Tree/Evaluator.hs          |  1 +
 src/Juvix/Compiler/Tree/Evaluator/Builtins.hs | 18 ++++++++++
 src/Juvix/Compiler/Tree/Extra/Type.hs         |  3 ++
 src/Juvix/Compiler/Tree/Language/Base.hs      |  1 +
 src/Juvix/Compiler/Tree/Language/Builtins.hs  |  4 +++
 src/Juvix/Compiler/Tree/Language/Value.hs     |  2 ++
 src/Juvix/Compiler/Tree/Pretty/Base.hs        |  6 ++++
 .../Compiler/Tree/Transformation/Validate.hs  |  3 ++
 .../Compiler/Tree/Translation/FromCore.hs     |  4 +++
 src/Juvix/Extra/Strings.hs                    | 24 +++++++++++++
 src/Juvix/Parser/Lexer.hs                     |  6 ++++
 test/Anoma/Compilation/Positive.hs            | 18 ++++++++++
 test/Compilation/Positive.hs                  |  7 +++-
 test/Rust/Compilation/Positive.hs             |  7 +++-
 .../Anoma/Compilation/positive/test081.juvix  | 35 +++++++++++++++++++
 tests/Compilation/positive/out/test078.out    | 11 ++++++
 tests/Compilation/positive/test078.juvix      | 34 ++++++++++++++++++
 tests/Core/positive/out/test063.out           |  1 +
 tests/Core/positive/test063.jvc               |  5 +++
 .../Rust/Compilation/positive/out/test074.out |  2 +-
 tests/Rust/Compilation/positive/test074.juvix |  7 ++++
 49 files changed, 405 insertions(+), 7 deletions(-)
 create mode 100644 src/Juvix/Compiler/Builtins/Byte.hs
 create mode 100644 tests/Anoma/Compilation/positive/test081.juvix
 create mode 100644 tests/Compilation/positive/out/test078.out
 create mode 100644 tests/Compilation/positive/test078.juvix
 create mode 100644 tests/Core/positive/out/test063.out
 create mode 100644 tests/Core/positive/test063.jvc
 create mode 100644 tests/Rust/Compilation/positive/test074.juvix

diff --git a/juvix-stdlib b/juvix-stdlib
index 297601a98d..d8eea7a203 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 297601a98dcace657aaff6e42945f1430647885b
+Subproject commit d8eea7a2038f93fa2f2100434742cd9773300b43
diff --git a/runtime/c/src/juvix/api.h b/runtime/c/src/juvix/api.h
index 5002188e89..07fa995336 100644
--- a/runtime/c/src/juvix/api.h
+++ b/runtime/c/src/juvix/api.h
@@ -100,6 +100,10 @@
 
 #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) \
diff --git a/runtime/rust/juvix/src/integer.rs b/runtime/rust/juvix/src/integer.rs
index 41282da4db..61aeecd8b0 100644
--- a/runtime/rust/juvix/src/integer.rs
+++ b/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);
+    }
 }
diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index 17e98ddc9a..729940469f 100644
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index abeaae4f22..f51515a925 100644
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
index 9749de1da0..d312c80762 100644
--- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
+++ b/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 {..} =
diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs
index 6ac25e5b84..274ab200dd 100644
--- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs
+++ b/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 {..} =
diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
index 87c92dda3f..2648a6620f 100644
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Builtins/Byte.hs b/src/Juvix/Compiler/Builtins/Byte.hs
new file mode 100644
index 0000000000..477398509e
--- /dev/null
+++ b/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)
diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs
index 9e3f3b2887..1cac6232ed 100644
--- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index 7c59b05647..6adf2536c3 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 957860479c..b30f90b581 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 9765916b77..d4b1bf6072 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/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)
 
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index 042c354c2a..5c4c573a05 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index 3fd914cb32..c63684c1cd 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/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]
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index d12ff25658..c956a73a94 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/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.
diff --git a/src/Juvix/Compiler/Core/Language/Primitives.hs b/src/Juvix/Compiler/Core/Language/Primitives.hs
index 839d47b3ab..ea008e0a08 100644
--- a/src/Juvix/Compiler/Core/Language/Primitives.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index b0f102a844..f90e309510 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs
index 8279878046..8b7b3fb7e9 100644
--- a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs
+++ b/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 =
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index 272dc8e8a2..e79b027f47 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
index 8f496beb55..5746972dd2 100644
--- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 6042918124..6551eb4b7d 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 1bb09ffd4e..2592087272 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 7b8038fc2a..2983361adc 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/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'
 
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 0afe527cf2..34c051b24e 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 8a98ffc9a0..44da1c09d0 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/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)
 
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index a605dd60a1..677ec97b02 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/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) =>
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index d8431233b3..e8c7d8639a 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs
index e598d192e5..c3c79b2ddf 100644
--- a/src/Juvix/Compiler/Tree/Evaluator.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
index e9ea9bd8bd..58b8e53772 100644
--- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Extra/Type.hs b/src/Juvix/Compiler/Tree/Extra/Type.hs
index 2425f0d2eb..1dfc32409a 100644
--- a/src/Juvix/Compiler/Tree/Extra/Type.hs
+++ b/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))
 
diff --git a/src/Juvix/Compiler/Tree/Language/Base.hs b/src/Juvix/Compiler/Tree/Language/Base.hs
index f3711f8b13..99208bd703 100644
--- a/src/Juvix/Compiler/Tree/Language/Base.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs
index 7d99a39839..94b04cfa2a 100644
--- a/src/Juvix/Compiler/Tree/Language/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Language/Value.hs b/src/Juvix/Compiler/Tree/Language/Value.hs
index 601d6e3036..2e4387a6f0 100644
--- a/src/Juvix/Compiler/Tree/Language/Value.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index aeae737a27..bf5e665d0e 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
index e05f67a00a..2565c76982 100644
--- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index 422ce1ecc7..587b4241df 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/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
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index fd13d8d8fc..df249563a9 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/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"
 
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index cffbf31ee1..8d4acd47d6 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/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
diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index 3843af88ba..fea8d489cf 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/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] |]
           ]
     ]
diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs
index 941bbbab93..3a65505b66 100644
--- a/test/Compilation/Positive.hs
+++ b/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")
     ]
diff --git a/test/Rust/Compilation/Positive.hs b/test/Rust/Compilation/Positive.hs
index 05d4e38fa7..c8ff0bc99d 100644
--- a/test/Rust/Compilation/Positive.hs
+++ b/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")
     ]
diff --git a/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix
new file mode 100644
index 0000000000..a34823b9b3
--- /dev/null
+++ b/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;
diff --git a/tests/Compilation/positive/out/test078.out b/tests/Compilation/positive/out/test078.out
new file mode 100644
index 0000000000..6224a0c855
--- /dev/null
+++ b/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)
diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix
new file mode 100644
index 0000000000..898160edb7
--- /dev/null
+++ b/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;
diff --git a/tests/Core/positive/out/test063.out b/tests/Core/positive/out/test063.out
new file mode 100644
index 0000000000..d00491fd7e
--- /dev/null
+++ b/tests/Core/positive/out/test063.out
@@ -0,0 +1 @@
+1
diff --git a/tests/Core/positive/test063.jvc b/tests/Core/positive/test063.jvc
new file mode 100644
index 0000000000..246b87d2c7
--- /dev/null
+++ b/tests/Core/positive/test063.jvc
@@ -0,0 +1,5 @@
+-- UInt8
+
+def f := \x x;
+
+f 257u8
diff --git a/tests/Rust/Compilation/positive/out/test074.out b/tests/Rust/Compilation/positive/out/test074.out
index eb3e83f932..0cfbf08886 100644
--- a/tests/Rust/Compilation/positive/out/test074.out
+++ b/tests/Rust/Compilation/positive/out/test074.out
@@ -1 +1 @@
--1085550836599839364109196834928521031686932164599479009991927616840761606155
+2
diff --git a/tests/Rust/Compilation/positive/test074.juvix b/tests/Rust/Compilation/positive/test074.juvix
new file mode 100644
index 0000000000..7ac631c51d
--- /dev/null
+++ b/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);