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 297601a98..d8eea7a20 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 5002188e8..07fa99533 100644
--- a/runtime/c/src/juvix/api.h
+++ b/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) \
diff --git a/runtime/rust/juvix/src/integer.rs b/runtime/rust/juvix/src/integer.rs
index 41282da4d..61aeecd8b 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 17e98ddc9..729940469 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 abeaae4f2..f51515a92 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 9749de1da..d312c8076 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 6ac25e5b8..274ab200d 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 87c92dda3..2648a6620 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 000000000..477398509
--- /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 9e3f3b288..1cac6232e 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 7c59b0564..6adf2536c 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 957860479..b30f90b58 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 9765916b7..d4b1bf607 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 042c354c2..5c4c573a0 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 3fd914cb3..c63684c1c 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 d12ff2565..c956a73a9 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 839d47b3a..ea008e0a0 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 b0f102a84..f90e30951 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 827987804..8b7b3fb7e 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 272dc8e8a..e79b027f4 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 8f496beb5..5746972dd 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 604291812..6551eb4b7 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 1bb09ffd4..259208727 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 7b8038fc2..2983361ad 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 0afe527cf..34c051b24 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 8a98ffc9a..44da1c09d 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 a605dd60a..677ec97b0 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 d8431233b..e8c7d8639 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 e598d192e..c3c79b2dd 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 e9ea9bd8b..58b8e5377 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 2425f0d2e..1dfc32409 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 f3711f8b1..99208bd70 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 7d99a3983..94b04cfa2 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 601d6e303..2e4387a6f 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 aeae737a2..bf5e665d0 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 e05f67a00..2565c7698 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 422ce1ecc..587b4241d 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 fd13d8d8f..df249563a 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 cffbf31ee..8d4acd47d 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 3843af88b..fea8d489c 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 941bbbab9..3a65505b6 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 05d4e38fa..c8ff0bc99 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 000000000..a34823b9b
--- /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 000000000..6224a0c85
--- /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 000000000..898160edb
--- /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 000000000..d00491fd7
--- /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 000000000..246b87d2c
--- /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 eb3e83f93..0cfbf0888 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 000000000..7ac631c51
--- /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);