From 6e40f628a87ab4b5e9e817b7b3a790920dc01683 Mon Sep 17 00:00:00 2001
From: Michael J Klein <michaeljklein@users.noreply.github.com>
Date: Wed, 9 Oct 2024 13:02:25 -0400
Subject: [PATCH] feat!: kind size checks (#6137)

# Description

## Problem\*

* Need to check that type constants fit into their `Kind`'s
* The sizes of results from `op.function` and `evaluate_to_u32` are
unchecked

## Summary\*

Split out from https://github.com/noir-lang/noir/pull/6094
- Some parts only work with its additional kind information
- Several follow up issues, including:
  * https://github.com/noir-lang/noir/issues/6247
  * https://github.com/noir-lang/noir/issues/6245
  * https://github.com/noir-lang/noir/issues/6238

## Additional Context

TODO:
- [x] Add this test and/or similar execution tests unless we already
have a similar one (sanity-check that global `Field` arithmetic works
past `u32::MAX`)

```noir
// 2^32 + 1
global A: Field = 4294967297;
global B: Field = 4294967297;
global C: Field = A + B;

fn main() {
    // 2 * (2^32 + 1)
    assert(C == 8589934594);

    let mut leading_zeroes = 0;
    let mut stop = false;
    let bits: [u1; 64] = C.to_be_bits();
    for i in 0..64 {
        if (bits[i] == 0) & !stop {
            leading_zeroes += 1;
        } else {
            stop = true;
        }
    }
    let size = 64 - leading_zeroes;

    // 8589934594 has 34 bits
    assert(size == 34);
}
```

## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** Documentation to be submitted in a
separate PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

---------

Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
Co-authored-by: Maxim Vezenov <mvezenov@gmail.com>
Co-authored-by: jfecher <jake@aztecprotocol.com>
---
 compiler/noirc_frontend/src/ast/mod.rs        |   8 +-
 .../src/elaborator/expressions.rs             |  11 +-
 .../noirc_frontend/src/elaborator/types.rs    |  56 +++-
 .../src/hir/comptime/hir_to_display_ast.rs    |   2 +-
 .../src/hir/comptime/interpreter.rs           | 315 ++++++++++++------
 .../src/hir/comptime/interpreter/builtin.rs   |  19 +-
 .../noirc_frontend/src/hir/comptime/tests.rs  |  19 +-
 .../noirc_frontend/src/hir/comptime/value.rs  |   2 +-
 .../src/hir/resolution/errors.rs              |   8 +-
 .../src/hir/type_check/errors.rs              |  26 +-
 compiler/noirc_frontend/src/hir_def/types.rs  | 192 +++++++++--
 .../src/hir_def/types/arithmetic.rs           |  38 ++-
 .../src/monomorphization/mod.rs               |  15 +-
 .../src/parser/parser/type_expression.rs      |  31 +-
 .../noirc_frontend/src/parser/parser/types.rs |  12 +-
 compiler/noirc_frontend/src/tests.rs          | 156 ++++++++-
 .../check_large_field_bits/Nargo.toml         |   7 +
 .../check_large_field_bits/src/main.nr        |  45 +++
 tooling/nargo_cli/build.rs                    |  21 +-
 .../tests/stdlib-props.proptest-regressions   |   1 +
 20 files changed, 767 insertions(+), 217 deletions(-)
 create mode 100644 test_programs/execution_success/check_large_field_bits/Nargo.toml
 create mode 100644 test_programs/execution_success/check_large_field_bits/src/main.nr

diff --git a/compiler/noirc_frontend/src/ast/mod.rs b/compiler/noirc_frontend/src/ast/mod.rs
index 94e81b19582..07f15f37c6e 100644
--- a/compiler/noirc_frontend/src/ast/mod.rs
+++ b/compiler/noirc_frontend/src/ast/mod.rs
@@ -19,6 +19,7 @@ pub use visitor::Visitor;
 pub use expression::*;
 pub use function::*;
 
+use acvm::FieldElement;
 pub use docs::*;
 use noirc_errors::Span;
 use serde::{Deserialize, Serialize};
@@ -219,7 +220,7 @@ pub struct UnaryRhsMethodCall {
 #[derive(Debug, PartialEq, Eq, Clone, Hash)]
 pub enum UnresolvedTypeExpression {
     Variable(Path),
-    Constant(u32, Span),
+    Constant(FieldElement, Span),
     BinaryOperation(
         Box<UnresolvedTypeExpression>,
         BinaryTypeOperator,
@@ -421,12 +422,13 @@ impl UnresolvedTypeExpression {
     fn from_expr_helper(expr: Expression) -> Result<UnresolvedTypeExpression, Expression> {
         match expr.kind {
             ExpressionKind::Literal(Literal::Integer(int, _)) => match int.try_to_u32() {
-                Some(int) => Ok(UnresolvedTypeExpression::Constant(int, expr.span)),
+                Some(int) => Ok(UnresolvedTypeExpression::Constant(int.into(), expr.span)),
                 None => Err(expr),
             },
             ExpressionKind::Variable(path) => Ok(UnresolvedTypeExpression::Variable(path)),
             ExpressionKind::Prefix(prefix) if prefix.operator == UnaryOp::Minus => {
-                let lhs = Box::new(UnresolvedTypeExpression::Constant(0, expr.span));
+                let lhs =
+                    Box::new(UnresolvedTypeExpression::Constant(FieldElement::zero(), expr.span));
                 let rhs = Box::new(UnresolvedTypeExpression::from_expr_helper(prefix.rhs)?);
                 let op = BinaryTypeOperator::Subtraction;
                 Ok(UnresolvedTypeExpression::BinaryOperation(lhs, op, rhs, expr.span))
diff --git a/compiler/noirc_frontend/src/elaborator/expressions.rs b/compiler/noirc_frontend/src/elaborator/expressions.rs
index 6dbf2cd9f3f..32c05ad00f4 100644
--- a/compiler/noirc_frontend/src/elaborator/expressions.rs
+++ b/compiler/noirc_frontend/src/elaborator/expressions.rs
@@ -1,3 +1,4 @@
+use acvm::{AcirField, FieldElement};
 use iter_extended::vecmap;
 use noirc_errors::{Location, Span};
 use regex::Regex;
@@ -161,7 +162,7 @@ impl<'context> Elaborator<'context> {
                 (Lit(int), self.polymorphic_integer_or_field())
             }
             Literal::Str(str) | Literal::RawStr(str, _) => {
-                let len = Type::Constant(str.len() as u32, Kind::u32());
+                let len = Type::Constant(str.len().into(), Kind::u32());
                 (Lit(HirLiteral::Str(str)), Type::String(Box::new(len)))
             }
             Literal::FmtStr(str) => self.elaborate_fmt_string(str, span),
@@ -203,7 +204,7 @@ impl<'context> Elaborator<'context> {
                     elem_id
                 });
 
-                let length = Type::Constant(elements.len() as u32, Kind::u32());
+                let length = Type::Constant(elements.len().into(), Kind::u32());
                 (HirArrayLiteral::Standard(elements), first_elem_type, length)
             }
             ArrayLiteral::Repeated { repeated_element, length } => {
@@ -211,7 +212,7 @@ impl<'context> Elaborator<'context> {
                 let length =
                     UnresolvedTypeExpression::from_expr(*length, span).unwrap_or_else(|error| {
                         self.push_err(ResolverError::ParserError(Box::new(error)));
-                        UnresolvedTypeExpression::Constant(0, span)
+                        UnresolvedTypeExpression::Constant(FieldElement::zero(), span)
                     });
 
                 let length = self.convert_expression_type(length, &Kind::u32(), span);
@@ -267,7 +268,7 @@ impl<'context> Elaborator<'context> {
             }
         }
 
-        let len = Type::Constant(str.len() as u32, Kind::u32());
+        let len = Type::Constant(str.len().into(), Kind::u32());
         let typ = Type::FmtString(Box::new(len), Box::new(Type::Tuple(capture_types)));
         (HirExpression::Literal(HirLiteral::FmtStr(str, fmt_str_idents)), typ)
     }
@@ -676,7 +677,7 @@ impl<'context> Elaborator<'context> {
     fn elaborate_cast(&mut self, cast: CastExpression, span: Span) -> (HirExpression, Type) {
         let (lhs, lhs_type) = self.elaborate_expression(cast.lhs);
         let r#type = self.resolve_type(cast.r#type);
-        let result = self.check_cast(&lhs_type, &r#type, span);
+        let result = self.check_cast(&lhs, &lhs_type, &r#type, span);
         let expr = HirExpression::Cast(HirCastExpression { lhs, r#type });
         (expr, result)
     }
diff --git a/compiler/noirc_frontend/src/elaborator/types.rs b/compiler/noirc_frontend/src/elaborator/types.rs
index ef06cfdaad8..82d14743428 100644
--- a/compiler/noirc_frontend/src/elaborator/types.rs
+++ b/compiler/noirc_frontend/src/elaborator/types.rs
@@ -417,7 +417,17 @@ impl<'context> Elaborator<'context> {
                     .map(|let_statement| Kind::Numeric(Box::new(let_statement.r#type)))
                     .unwrap_or(Kind::u32());
 
-                Some(Type::Constant(self.eval_global_as_array_length(id, path), kind))
+                // TODO(https://github.com/noir-lang/noir/issues/6238):
+                // support non-u32 generics here
+                if !kind.unifies(&Kind::u32()) {
+                    let error = TypeCheckError::EvaluatedGlobalIsntU32 {
+                        expected_kind: Kind::u32().to_string(),
+                        expr_kind: kind.to_string(),
+                        expr_span: path.span(),
+                    };
+                    self.push_err(error);
+                }
+                Some(Type::Constant(self.eval_global_as_array_length(id, path).into(), kind))
             }
             _ => None,
         }
@@ -833,12 +843,27 @@ impl<'context> Elaborator<'context> {
         }
     }
 
-    pub(super) fn check_cast(&mut self, from: &Type, to: &Type, span: Span) -> Type {
-        match from.follow_bindings() {
-            Type::Integer(..) | Type::FieldElement | Type::Bool => (),
+    pub(super) fn check_cast(
+        &mut self,
+        from_expr_id: &ExprId,
+        from: &Type,
+        to: &Type,
+        span: Span,
+    ) -> Type {
+        let from_follow_bindings = from.follow_bindings();
 
-            Type::TypeVariable(var) if var.is_integer() || var.is_integer_or_field() => (),
+        let from_value_opt = match self.interner.expression(from_expr_id) {
+            HirExpression::Literal(HirLiteral::Integer(int, false)) => Some(int),
 
+            // TODO(https://github.com/noir-lang/noir/issues/6247):
+            // handle negative literals
+            _ => None,
+        };
+
+        let from_is_polymorphic = match from_follow_bindings {
+            Type::Integer(..) | Type::FieldElement | Type::Bool => false,
+
+            Type::TypeVariable(ref var) if var.is_integer() || var.is_integer_or_field() => true,
             Type::TypeVariable(_) => {
                 // NOTE: in reality the expected type can also include bool, but for the compiler's simplicity
                 // we only allow integer types. If a bool is in `from` it will need an explicit type annotation.
@@ -846,13 +871,32 @@ impl<'context> Elaborator<'context> {
                 self.unify(from, &expected, || TypeCheckError::InvalidCast {
                     from: from.clone(),
                     span,
+                    reason: "casting from a non-integral type is unsupported".into(),
                 });
+                true
             }
             Type::Error => return Type::Error,
             from => {
-                self.push_err(TypeCheckError::InvalidCast { from, span });
+                let reason = "casting from this type is unsupported".into();
+                self.push_err(TypeCheckError::InvalidCast { from, span, reason });
                 return Type::Error;
             }
+        };
+
+        // TODO(https://github.com/noir-lang/noir/issues/6247):
+        // handle negative literals
+        // when casting a polymorphic value to a specifically sized type,
+        // check that it fits or throw a warning
+        if let (Some(from_value), Some(to_maximum_size)) =
+            (from_value_opt, to.integral_maximum_size())
+        {
+            if from_is_polymorphic && from_value > to_maximum_size {
+                let from = from.clone();
+                let to = to.clone();
+                let reason = format!("casting untyped value ({from_value}) to a type with a maximum size ({to_maximum_size}) that's smaller than it");
+                // we warn that the 'to' type is too small for the value
+                self.push_err(TypeCheckError::DownsizingCast { from, to, span, reason });
+            }
         }
 
         match to {
diff --git a/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs b/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
index 3542c724b30..97d90b905d4 100644
--- a/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
@@ -417,7 +417,7 @@ impl HirArrayLiteral {
                 let repeated_element = Box::new(repeated_element.to_display_ast(interner));
                 let length = match length {
                     Type::Constant(length, _kind) => {
-                        let literal = Literal::Integer((*length as u128).into(), false);
+                        let literal = Literal::Integer(*length, false);
                         let expr_kind = ExpressionKind::Literal(literal);
                         Box::new(Expression::new(expr_kind, span))
                     }
diff --git a/compiler/noirc_frontend/src/hir/comptime/interpreter.rs b/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
index 1690295ffda..ffb759e74a2 100644
--- a/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
@@ -586,12 +586,14 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
             DefinitionKind::NumericGeneric(type_variable, numeric_typ) => {
                 let value = match &*type_variable.borrow() {
                     TypeBinding::Unbound(_, _) => None,
-                    TypeBinding::Bound(binding) => binding.evaluate_to_u32(),
+                    TypeBinding::Bound(binding) => {
+                        binding.evaluate_to_field_element(&Kind::Numeric(numeric_typ.clone()))
+                    }
                 };
 
                 if let Some(value) = value {
                     let typ = self.elaborator.interner.id_type(id);
-                    self.evaluate_integer((value as u128).into(), false, id)
+                    self.evaluate_integer(value, false, id)
                 } else {
                     let location = self.elaborator.interner.expr_location(&id);
                     let typ = Type::TypeVariable(type_variable.clone());
@@ -895,71 +897,138 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
     }
 
     fn evaluate_infix(&mut self, infix: HirInfixExpression, id: ExprId) -> IResult<Value> {
-        let lhs = self.evaluate(infix.lhs)?;
-        let rhs = self.evaluate(infix.rhs)?;
+        let lhs_value = self.evaluate(infix.lhs)?;
+        let rhs_value = self.evaluate(infix.rhs)?;
 
         if self.elaborator.interner.get_selected_impl_for_expression(id).is_some() {
-            return self.evaluate_overloaded_infix(infix, lhs, rhs, id);
+            return self.evaluate_overloaded_infix(infix, lhs_value, rhs_value, id);
         }
 
-        let make_error = |this: &mut Self, lhs: Value, rhs: Value, operator| {
-            let location = this.elaborator.interner.expr_location(&id);
-            let lhs = lhs.get_type().into_owned();
-            let rhs = rhs.get_type().into_owned();
-            Err(InvalidValuesForBinary { lhs, rhs, location, operator })
+        let lhs_type = lhs_value.get_type().into_owned();
+        let rhs_type = rhs_value.get_type().into_owned();
+        let location = self.elaborator.interner.expr_location(&id);
+
+        let error = |operator| {
+            let lhs = lhs_type.clone();
+            let rhs = rhs_type.clone();
+            InterpreterError::InvalidValuesForBinary { lhs, rhs, location, operator }
         };
 
         use InterpreterError::InvalidValuesForBinary;
         match infix.operator.kind {
-            BinaryOpKind::Add => match (lhs, rhs) {
+            BinaryOpKind::Add => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Field(lhs + rhs)),
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs + rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs + rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs + rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs + rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs + rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs + rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs + rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs + rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "+"),
+                (Value::I8(lhs), Value::I8(rhs)) => {
+                    Ok(Value::I8(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::I16(lhs), Value::I16(rhs)) => {
+                    Ok(Value::I16(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::I32(lhs), Value::I32(rhs)) => {
+                    Ok(Value::I32(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::I64(lhs), Value::I64(rhs)) => {
+                    Ok(Value::I64(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => {
+                    Ok(Value::U64(lhs.checked_add(rhs).ok_or(error("+"))?))
+                }
+                (lhs, rhs) => Err(error("+")),
             },
-            BinaryOpKind::Subtract => match (lhs, rhs) {
+            BinaryOpKind::Subtract => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Field(lhs - rhs)),
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs - rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs - rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs - rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs - rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs - rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs - rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs - rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs - rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "-"),
+                (Value::I8(lhs), Value::I8(rhs)) => {
+                    Ok(Value::I8(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::I16(lhs), Value::I16(rhs)) => {
+                    Ok(Value::I16(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::I32(lhs), Value::I32(rhs)) => {
+                    Ok(Value::I32(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::I64(lhs), Value::I64(rhs)) => {
+                    Ok(Value::I64(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => {
+                    Ok(Value::U64(lhs.checked_sub(rhs).ok_or(error("-"))?))
+                }
+                (lhs, rhs) => Err(error("-")),
             },
-            BinaryOpKind::Multiply => match (lhs, rhs) {
+            BinaryOpKind::Multiply => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Field(lhs * rhs)),
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs * rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs * rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs * rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs * rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs * rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs * rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs * rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs * rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "*"),
+                (Value::I8(lhs), Value::I8(rhs)) => {
+                    Ok(Value::I8(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::I16(lhs), Value::I16(rhs)) => {
+                    Ok(Value::I16(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::I32(lhs), Value::I32(rhs)) => {
+                    Ok(Value::I32(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::I64(lhs), Value::I64(rhs)) => {
+                    Ok(Value::I64(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => {
+                    Ok(Value::U64(lhs.checked_mul(rhs).ok_or(error("*"))?))
+                }
+                (lhs, rhs) => Err(error("*")),
             },
-            BinaryOpKind::Divide => match (lhs, rhs) {
+            BinaryOpKind::Divide => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Field(lhs / rhs)),
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs / rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs / rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs / rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs / rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs / rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs / rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs / rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs / rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "/"),
+                (Value::I8(lhs), Value::I8(rhs)) => {
+                    Ok(Value::I8(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::I16(lhs), Value::I16(rhs)) => {
+                    Ok(Value::I16(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::I32(lhs), Value::I32(rhs)) => {
+                    Ok(Value::I32(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::I64(lhs), Value::I64(rhs)) => {
+                    Ok(Value::I64(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => {
+                    Ok(Value::U64(lhs.checked_div(rhs).ok_or(error("/"))?))
+                }
+                (lhs, rhs) => Err(error("/")),
             },
-            BinaryOpKind::Equal => match (lhs, rhs) {
+            BinaryOpKind::Equal => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs == rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs == rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs == rhs)),
@@ -970,9 +1039,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs == rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs == rhs)),
                 (Value::Bool(lhs), Value::Bool(rhs)) => Ok(Value::Bool(lhs == rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "=="),
+                (lhs, rhs) => Err(error("==")),
             },
-            BinaryOpKind::NotEqual => match (lhs, rhs) {
+            BinaryOpKind::NotEqual => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs != rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs != rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs != rhs)),
@@ -983,9 +1052,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs != rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs != rhs)),
                 (Value::Bool(lhs), Value::Bool(rhs)) => Ok(Value::Bool(lhs != rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "!="),
+                (lhs, rhs) => Err(error("!=")),
             },
-            BinaryOpKind::Less => match (lhs, rhs) {
+            BinaryOpKind::Less => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs < rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs < rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs < rhs)),
@@ -995,9 +1064,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::Bool(lhs < rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs < rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs < rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "<"),
+                (lhs, rhs) => Err(error("<")),
             },
-            BinaryOpKind::LessEqual => match (lhs, rhs) {
+            BinaryOpKind::LessEqual => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs <= rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs <= rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs <= rhs)),
@@ -1007,9 +1076,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::Bool(lhs <= rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs <= rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs <= rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "<="),
+                (lhs, rhs) => Err(error("<=")),
             },
-            BinaryOpKind::Greater => match (lhs, rhs) {
+            BinaryOpKind::Greater => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs > rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs > rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs > rhs)),
@@ -1019,9 +1088,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::Bool(lhs > rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs > rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs > rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, ">"),
+                (lhs, rhs) => Err(error(">")),
             },
-            BinaryOpKind::GreaterEqual => match (lhs, rhs) {
+            BinaryOpKind::GreaterEqual => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Field(lhs), Value::Field(rhs)) => Ok(Value::Bool(lhs >= rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::Bool(lhs >= rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::Bool(lhs >= rhs)),
@@ -1031,9 +1100,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::Bool(lhs >= rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::Bool(lhs >= rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::Bool(lhs >= rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, ">="),
+                (lhs, rhs) => Err(error(">=")),
             },
-            BinaryOpKind::And => match (lhs, rhs) {
+            BinaryOpKind::And => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Bool(lhs), Value::Bool(rhs)) => Ok(Value::Bool(lhs & rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs & rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs & rhs)),
@@ -1043,9 +1112,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs & rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs & rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs & rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "&"),
+                (lhs, rhs) => Err(error("&")),
             },
-            BinaryOpKind::Or => match (lhs, rhs) {
+            BinaryOpKind::Or => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Bool(lhs), Value::Bool(rhs)) => Ok(Value::Bool(lhs | rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs | rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs | rhs)),
@@ -1055,9 +1124,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs | rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs | rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs | rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "|"),
+                (lhs, rhs) => Err(error("|")),
             },
-            BinaryOpKind::Xor => match (lhs, rhs) {
+            BinaryOpKind::Xor => match (lhs_value.clone(), rhs_value.clone()) {
                 (Value::Bool(lhs), Value::Bool(rhs)) => Ok(Value::Bool(lhs ^ rhs)),
                 (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs ^ rhs)),
                 (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs ^ rhs)),
@@ -1067,40 +1136,88 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs ^ rhs)),
                 (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs ^ rhs)),
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs ^ rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "^"),
+                (lhs, rhs) => Err(error("^")),
             },
-            BinaryOpKind::ShiftRight => match (lhs, rhs) {
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs >> rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs >> rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs >> rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs >> rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs >> rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs >> rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs >> rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs >> rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, ">>"),
+            BinaryOpKind::ShiftRight => match (lhs_value.clone(), rhs_value.clone()) {
+                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(
+                    lhs.checked_shr(rhs.try_into().map_err(|_| error(">>"))?).ok_or(error(">>"))?,
+                )),
+                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(
+                    lhs.checked_shr(rhs.try_into().map_err(|_| error(">>"))?).ok_or(error(">>"))?,
+                )),
+                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(
+                    lhs.checked_shr(rhs.try_into().map_err(|_| error(">>"))?).ok_or(error(">>"))?,
+                )),
+                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(
+                    lhs.checked_shr(rhs.try_into().map_err(|_| error(">>"))?).ok_or(error(">>"))?,
+                )),
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_shr(rhs.into()).ok_or(error(">>"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_shr(rhs.into()).ok_or(error(">>"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_shr(rhs).ok_or(error(">>"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(
+                    lhs.checked_shr(rhs.try_into().map_err(|_| error(">>"))?).ok_or(error(">>"))?,
+                )),
+                (lhs, rhs) => Err(error(">>")),
             },
-            BinaryOpKind::ShiftLeft => match (lhs, rhs) {
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs << rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs << rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs << rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs << rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs << rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs << rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs << rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs << rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "<<"),
+            BinaryOpKind::ShiftLeft => match (lhs_value.clone(), rhs_value.clone()) {
+                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(
+                    lhs.checked_shl(rhs.try_into().map_err(|_| error("<<"))?).ok_or(error("<<"))?,
+                )),
+                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(
+                    lhs.checked_shl(rhs.try_into().map_err(|_| error("<<"))?).ok_or(error("<<"))?,
+                )),
+                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(
+                    lhs.checked_shl(rhs.try_into().map_err(|_| error("<<"))?).ok_or(error("<<"))?,
+                )),
+                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(
+                    lhs.checked_shl(rhs.try_into().map_err(|_| error("<<"))?).ok_or(error("<<"))?,
+                )),
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_shl(rhs.into()).ok_or(error("<<"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_shl(rhs.into()).ok_or(error("<<"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_shl(rhs).ok_or(error("<<"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(
+                    lhs.checked_shl(rhs.try_into().map_err(|_| error("<<"))?).ok_or(error("<<"))?,
+                )),
+                (lhs, rhs) => Err(error("<<")),
             },
-            BinaryOpKind::Modulo => match (lhs, rhs) {
-                (Value::I8(lhs), Value::I8(rhs)) => Ok(Value::I8(lhs % rhs)),
-                (Value::I16(lhs), Value::I16(rhs)) => Ok(Value::I16(lhs % rhs)),
-                (Value::I32(lhs), Value::I32(rhs)) => Ok(Value::I32(lhs % rhs)),
-                (Value::I64(lhs), Value::I64(rhs)) => Ok(Value::I64(lhs % rhs)),
-                (Value::U8(lhs), Value::U8(rhs)) => Ok(Value::U8(lhs % rhs)),
-                (Value::U16(lhs), Value::U16(rhs)) => Ok(Value::U16(lhs % rhs)),
-                (Value::U32(lhs), Value::U32(rhs)) => Ok(Value::U32(lhs % rhs)),
-                (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs % rhs)),
-                (lhs, rhs) => make_error(self, lhs, rhs, "%"),
+            BinaryOpKind::Modulo => match (lhs_value.clone(), rhs_value.clone()) {
+                (Value::I8(lhs), Value::I8(rhs)) => {
+                    Ok(Value::I8(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::I16(lhs), Value::I16(rhs)) => {
+                    Ok(Value::I16(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::I32(lhs), Value::I32(rhs)) => {
+                    Ok(Value::I32(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::I64(lhs), Value::I64(rhs)) => {
+                    Ok(Value::I64(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::U8(lhs), Value::U8(rhs)) => {
+                    Ok(Value::U8(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::U16(lhs), Value::U16(rhs)) => {
+                    Ok(Value::U16(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::U32(lhs), Value::U32(rhs)) => {
+                    Ok(Value::U32(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (Value::U64(lhs), Value::U64(rhs)) => {
+                    Ok(Value::U64(lhs.checked_rem(rhs).ok_or(error("%"))?))
+                }
+                (lhs, rhs) => Err(error("%")),
             },
         }
     }
@@ -1638,7 +1755,7 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 Value::Pointer(elem, true) => Ok(elem.borrow().clone()),
                 other => Ok(other),
             },
-            HirLValue::Dereference { lvalue, element_type: _, location } => {
+            HirLValue::Dereference { lvalue, element_type, location } => {
                 match self.evaluate_lvalue(lvalue)? {
                     Value::Pointer(value, _) => Ok(value.borrow().clone()),
                     value => {
diff --git a/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs b/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
index e5a20f1c160..170cd67e146 100644
--- a/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
@@ -315,7 +315,7 @@ fn str_as_bytes(
 
     let bytes: im::Vector<Value> = string.bytes().map(Value::U8).collect();
     let byte_array_type = Type::Array(
-        Box::new(Type::Constant(bytes.len() as u32, Kind::u32())),
+        Box::new(Type::Constant(bytes.len().into(), Kind::u32())),
         Box::new(Type::Integer(Signedness::Unsigned, IntegerBitSize::Eight)),
     );
     Ok(Value::Array(bytes, byte_array_type))
@@ -805,8 +805,12 @@ fn to_le_radix(
     let value = get_field(value)?;
     let radix = get_u32(radix)?;
     let limb_count = if let Type::Array(length, _) = return_type {
-        if let Type::Constant(limb_count, _kind) = *length {
-            limb_count
+        if let Type::Constant(limb_count, kind) = *length {
+            if kind.unifies(&Kind::u32()) {
+                limb_count
+            } else {
+                return Err(InterpreterError::TypeAnnotationsNeededForMethodCall { location });
+            }
         } else {
             return Err(InterpreterError::TypeAnnotationsNeededForMethodCall { location });
         }
@@ -816,10 +820,11 @@ fn to_le_radix(
 
     // Decompose the integer into its radix digits in little endian form.
     let decomposed_integer = compute_to_radix_le(value, radix);
-    let decomposed_integer = vecmap(0..limb_count as usize, |i| match decomposed_integer.get(i) {
-        Some(digit) => Value::U8(*digit),
-        None => Value::U8(0),
-    });
+    let decomposed_integer =
+        vecmap(0..limb_count.to_u128() as usize, |i| match decomposed_integer.get(i) {
+            Some(digit) => Value::U8(*digit),
+            None => Value::U8(0),
+        });
     Ok(Value::Array(
         decomposed_integer.into(),
         Type::Integer(Signedness::Unsigned, IntegerBitSize::Eight),
diff --git a/compiler/noirc_frontend/src/hir/comptime/tests.rs b/compiler/noirc_frontend/src/hir/comptime/tests.rs
index 458a186a3f8..e033ec6ddb9 100644
--- a/compiler/noirc_frontend/src/hir/comptime/tests.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/tests.rs
@@ -78,6 +78,23 @@ fn interpreter_works() {
     assert_eq!(result, Value::Field(3u128.into()));
 }
 
+#[test]
+fn interpreter_type_checking_works() {
+    let program = "comptime fn main() -> pub u8 { 3 }";
+    let result = interpret(program);
+    assert_eq!(result, Value::U8(3u8));
+}
+
+#[test]
+fn let_statement_works() {
+    let program = "comptime fn main() -> pub i8 {
+        let x = 4;
+        x
+    }";
+    let result = interpret(program);
+    assert_eq!(result, Value::I8(4));
+}
+
 #[test]
 fn mutation_works() {
     let program = "comptime fn main() -> pub i8 {
@@ -277,5 +294,5 @@ fn generic_functions() {
     }
     ";
     let result = interpret(program);
-    assert!(matches!(result, Value::U8(2)));
+    assert_eq!(result, Value::U8(2));
 }
diff --git a/compiler/noirc_frontend/src/hir/comptime/value.rs b/compiler/noirc_frontend/src/hir/comptime/value.rs
index 4b55735fcb1..945fb45026d 100644
--- a/compiler/noirc_frontend/src/hir/comptime/value.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/value.rs
@@ -120,7 +120,7 @@ impl Value {
             Value::U32(_) => Type::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo),
             Value::U64(_) => Type::Integer(Signedness::Unsigned, IntegerBitSize::SixtyFour),
             Value::String(value) => {
-                let length = Type::Constant(value.len() as u32, Kind::u32());
+                let length = Type::Constant(value.len().into(), Kind::u32());
                 Type::String(Box::new(length))
             }
             Value::FormatString(_, typ) => return Cow::Borrowed(typ),
diff --git a/compiler/noirc_frontend/src/hir/resolution/errors.rs b/compiler/noirc_frontend/src/hir/resolution/errors.rs
index e3f3d488c43..a6eb1864d13 100644
--- a/compiler/noirc_frontend/src/hir/resolution/errors.rs
+++ b/compiler/noirc_frontend/src/hir/resolution/errors.rs
@@ -1,3 +1,4 @@
+use acvm::FieldElement;
 pub use noirc_errors::Span;
 use noirc_errors::{CustomDiagnostic as Diagnostic, FileDiagnostic};
 use thiserror::Error;
@@ -125,7 +126,12 @@ pub enum ResolverError {
     #[error("Associated constants may only be a field or integer type")]
     AssociatedConstantsMustBeNumeric { span: Span },
     #[error("Overflow in `{lhs} {op} {rhs}`")]
-    OverflowInType { lhs: u32, op: crate::BinaryTypeOperator, rhs: u32, span: Span },
+    OverflowInType {
+        lhs: FieldElement,
+        op: crate::BinaryTypeOperator,
+        rhs: FieldElement,
+        span: Span,
+    },
     #[error("`quote` cannot be used in runtime code")]
     QuoteInRuntimeCode { span: Span },
     #[error("Comptime-only type `{typ}` cannot be used in runtime code")]
diff --git a/compiler/noirc_frontend/src/hir/type_check/errors.rs b/compiler/noirc_frontend/src/hir/type_check/errors.rs
index 54699792901..d8dae1f6549 100644
--- a/compiler/noirc_frontend/src/hir/type_check/errors.rs
+++ b/compiler/noirc_frontend/src/hir/type_check/errors.rs
@@ -48,12 +48,17 @@ pub enum TypeCheckError {
     TypeMismatchWithSource { expected: Type, actual: Type, span: Span, source: Source },
     #[error("Expected type {expected_kind:?} is not the same as {expr_kind:?}")]
     TypeKindMismatch { expected_kind: String, expr_kind: String, expr_span: Span },
+    // TODO(https://github.com/noir-lang/noir/issues/6238): implement handling for larger types
+    #[error("Expected type {expected_kind} when evaluating globals, but found {expr_kind} (this warning may become an error in the future)")]
+    EvaluatedGlobalIsntU32 { expected_kind: String, expr_kind: String, expr_span: Span },
     #[error("Expected {expected:?} found {found:?}")]
     ArityMisMatch { expected: usize, found: usize, span: Span },
     #[error("Return type in a function cannot be public")]
     PublicReturnType { typ: Type, span: Span },
     #[error("Cannot cast type {from}, 'as' is only for primitive field or integer types")]
-    InvalidCast { from: Type, span: Span },
+    InvalidCast { from: Type, span: Span, reason: String },
+    #[error("Casting value of type {from} to a smaller type ({to})")]
+    DownsizingCast { from: Type, to: Type, span: Span, reason: String },
     #[error("Expected a function, but found a(n) {found}")]
     ExpectedFunction { found: Type, span: Span },
     #[error("Type {lhs_type} has no member named {field_name}")]
@@ -227,6 +232,15 @@ impl<'a> From<&'a TypeCheckError> for Diagnostic {
                     *expr_span,
                 )
             }
+            // TODO(https://github.com/noir-lang/noir/issues/6238): implement
+            // handling for larger types
+            TypeCheckError::EvaluatedGlobalIsntU32 { expected_kind, expr_kind, expr_span } => {
+                Diagnostic::simple_warning(
+                    format!("Expected type {expected_kind} when evaluating globals, but found {expr_kind} (this warning may become an error in the future)"),
+                    String::new(),
+                    *expr_span,
+                )
+            }
             TypeCheckError::TraitMethodParameterTypeMismatch { method_name, expected_typ, actual_typ, parameter_index, parameter_span } => {
                 Diagnostic::simple_error(
                     format!("Parameter #{parameter_index} of method `{method_name}` must be of type {expected_typ}, not {actual_typ}"),
@@ -284,8 +298,14 @@ impl<'a> From<&'a TypeCheckError> for Diagnostic {
                 };
                 Diagnostic::simple_error(msg, String::new(), *span)
             }
-            TypeCheckError::InvalidCast { span, .. }
-            | TypeCheckError::ExpectedFunction { span, .. }
+            TypeCheckError::InvalidCast { span, reason, .. } => {
+                Diagnostic::simple_error(error.to_string(), reason.clone(), *span)
+            }
+            TypeCheckError::DownsizingCast { span, reason, .. } => {
+                Diagnostic::simple_warning(error.to_string(), reason.clone(), *span)
+            }
+
+            TypeCheckError::ExpectedFunction { span, .. }
             | TypeCheckError::AccessUnknownMember { span, .. }
             | TypeCheckError::UnsupportedCast { span }
             | TypeCheckError::TupleIndexOutOfBounds { span, .. }
diff --git a/compiler/noirc_frontend/src/hir_def/types.rs b/compiler/noirc_frontend/src/hir_def/types.rs
index f2845ac0af7..538b5553afd 100644
--- a/compiler/noirc_frontend/src/hir_def/types.rs
+++ b/compiler/noirc_frontend/src/hir_def/types.rs
@@ -5,6 +5,8 @@ use std::{
     rc::Rc,
 };
 
+use acvm::{AcirField, FieldElement};
+
 use crate::{
     ast::{IntegerBitSize, ItemVisibility},
     hir::type_check::{generics::TraitGenerics, TypeCheckError},
@@ -110,9 +112,11 @@ pub enum Type {
     /// will be and thus needs the full TypeVariable link.
     Forall(GenericTypeVars, Box<Type>),
 
-    /// A type-level integer. Included to let an Array's size type variable
-    /// bind to an integer without special checks to bind it to a non-type.
-    Constant(u32, Kind),
+    /// A type-level integer. Included to let
+    /// 1. an Array's size type variable
+    ///     bind to an integer without special checks to bind it to a non-type.
+    /// 2. values to be used at the type level
+    Constant(FieldElement, Kind),
 
     /// The type of quoted code in macros. This is always a comptime-only type
     Quoted(QuotedType),
@@ -158,14 +162,29 @@ pub enum Kind {
 
 impl Kind {
     pub(crate) fn is_error(&self) -> bool {
-        match self {
-            Self::Numeric(typ) => **typ == Type::Error,
+        match self.follow_bindings() {
+            Self::Numeric(typ) => *typ == Type::Error,
             _ => false,
         }
     }
 
     pub(crate) fn is_numeric(&self) -> bool {
-        matches!(self, Self::Numeric { .. })
+        matches!(self.follow_bindings(), Self::Numeric { .. })
+    }
+
+    pub(crate) fn is_type_level_field_element(&self) -> bool {
+        let type_level = false;
+        self.is_field_element(type_level)
+    }
+
+    /// If value_level, only check for Type::FieldElement,
+    /// else only check for a type-level FieldElement
+    fn is_field_element(&self, value_level: bool) -> bool {
+        match self.follow_bindings() {
+            Kind::Numeric(typ) => typ.is_field_element(value_level),
+            Kind::IntegerOrField => value_level,
+            _ => false,
+        }
     }
 
     pub(crate) fn u32() -> Self {
@@ -229,6 +248,21 @@ impl Kind {
             Kind::Numeric(typ) => Some(*typ.clone()),
         }
     }
+
+    fn integral_maximum_size(&self) -> Option<FieldElement> {
+        match self.follow_bindings() {
+            Kind::Any | Kind::IntegerOrField | Kind::Integer | Kind::Normal => None,
+            Self::Numeric(typ) => typ.integral_maximum_size(),
+        }
+    }
+
+    /// Ensure the given value fits in self.integral_maximum_size()
+    fn ensure_value_fits(&self, value: FieldElement) -> Option<FieldElement> {
+        match self.integral_maximum_size() {
+            None => Some(value),
+            Some(maximum_size) => (value <= maximum_size).then_some(value),
+        }
+    }
 }
 
 impl std::fmt::Display for Kind {
@@ -713,8 +747,10 @@ impl TypeVariable {
     /// and if unbound, that it's a Kind::Integer
     pub fn is_integer(&self) -> bool {
         match &*self.borrow() {
-            TypeBinding::Bound(binding) => matches!(binding, Type::Integer(..)),
-            TypeBinding::Unbound(_, type_var_kind) => matches!(type_var_kind, Kind::Integer),
+            TypeBinding::Bound(binding) => matches!(binding.follow_bindings(), Type::Integer(..)),
+            TypeBinding::Unbound(_, type_var_kind) => {
+                matches!(type_var_kind.follow_bindings(), Kind::Integer)
+            }
         }
     }
 
@@ -723,9 +759,20 @@ impl TypeVariable {
     pub fn is_integer_or_field(&self) -> bool {
         match &*self.borrow() {
             TypeBinding::Bound(binding) => {
-                matches!(binding, Type::Integer(..) | Type::FieldElement)
+                matches!(binding.follow_bindings(), Type::Integer(..) | Type::FieldElement)
+            }
+            TypeBinding::Unbound(_, type_var_kind) => {
+                matches!(type_var_kind.follow_bindings(), Kind::IntegerOrField)
             }
-            TypeBinding::Unbound(_, type_var_kind) => matches!(type_var_kind, Kind::IntegerOrField),
+        }
+    }
+
+    /// If value_level, only check for Type::FieldElement,
+    /// else only check for a type-level FieldElement
+    fn is_field_element(&self, value_level: bool) -> bool {
+        match &*self.borrow() {
+            TypeBinding::Bound(binding) => binding.is_field_element(value_level),
+            TypeBinding::Unbound(_, type_var_kind) => type_var_kind.is_field_element(value_level),
         }
     }
 }
@@ -956,6 +1003,17 @@ impl Type {
         matches!(self.follow_bindings(), Type::Integer(_, _))
     }
 
+    /// If value_level, only check for Type::FieldElement,
+    /// else only check for a type-level FieldElement
+    fn is_field_element(&self, value_level: bool) -> bool {
+        match self.follow_bindings() {
+            Type::FieldElement => value_level,
+            Type::TypeVariable(var) => var.is_field_element(value_level),
+            Type::Constant(_, kind) => !value_level && kind.is_field_element(true),
+            _ => false,
+        }
+    }
+
     pub fn is_signed(&self) -> bool {
         matches!(self.follow_bindings(), Type::Integer(Signedness::Signed, _))
     }
@@ -1668,8 +1726,7 @@ impl Type {
             }
 
             (Constant(value, kind), other) | (other, Constant(value, kind)) => {
-                // TODO(https://github.com/noir-lang/noir/pull/6137): replace evaluate_to_u32
-                if let Some(other_value) = other.evaluate_to_u32() {
+                if let Some(other_value) = other.evaluate_to_field_element(kind) {
                     if *value == other_value && kind.unifies(&other.kind()) {
                         Ok(())
                     } else {
@@ -1838,19 +1895,38 @@ impl Type {
     /// If this type is a Type::Constant (used in array lengths), or is bound
     /// to a Type::Constant, return the constant as a u32.
     pub fn evaluate_to_u32(&self) -> Option<u32> {
-        if let Some((binding, _kind)) = self.get_inner_type_variable() {
+        self.evaluate_to_field_element(&Kind::u32())
+            .and_then(|field_element| field_element.try_to_u32())
+    }
+
+    // TODO(https://github.com/noir-lang/noir/issues/6260): remove
+    // the unifies checks once all kinds checks are implemented?
+    pub(crate) fn evaluate_to_field_element(&self, kind: &Kind) -> Option<acvm::FieldElement> {
+        if let Some((binding, binding_kind)) = self.get_inner_type_variable() {
             if let TypeBinding::Bound(binding) = &*binding.borrow() {
-                return binding.evaluate_to_u32();
+                if kind.unifies(&binding_kind) {
+                    return binding.evaluate_to_field_element(&binding_kind);
+                }
             }
         }
 
         match self.canonicalize() {
-            Type::Array(len, _elem) => len.evaluate_to_u32(),
-            Type::Constant(x, _kind) => Some(x),
+            Type::Constant(x, constant_kind) => {
+                if kind.unifies(&constant_kind) {
+                    kind.ensure_value_fits(x)
+                } else {
+                    None
+                }
+            }
             Type::InfixExpr(lhs, op, rhs) => {
-                let lhs_u32 = lhs.evaluate_to_u32()?;
-                let rhs_u32 = rhs.evaluate_to_u32()?;
-                op.function(lhs_u32, rhs_u32, &lhs.infix_kind(&rhs))
+                let infix_kind = lhs.infix_kind(&rhs);
+                if kind.unifies(&infix_kind) {
+                    let lhs_value = lhs.evaluate_to_field_element(&infix_kind)?;
+                    let rhs_value = rhs.evaluate_to_field_element(&infix_kind)?;
+                    op.function(lhs_value, rhs_value, &infix_kind)
+                } else {
+                    None
+                }
             }
             _ => None,
         }
@@ -2227,7 +2303,6 @@ impl Type {
                 }
                 self.clone()
             }
-
             Function(args, ret, env, unconstrained) => {
                 let args = vecmap(args, |arg| arg.follow_bindings());
                 let ret = Box::new(ret.follow_bindings());
@@ -2352,6 +2427,51 @@ impl Type {
             _ => None,
         }
     }
+
+    pub(crate) fn integral_maximum_size(&self) -> Option<FieldElement> {
+        match self {
+            Type::FieldElement => None,
+            Type::Integer(sign, num_bits) => {
+                let mut max_bit_size = num_bits.bit_size();
+                if sign == &Signedness::Signed {
+                    max_bit_size -= 1;
+                }
+                Some(((1u128 << max_bit_size) - 1).into())
+            }
+            Type::Bool => Some(FieldElement::one()),
+            Type::TypeVariable(var) => {
+                let binding = &var.1;
+                match &*binding.borrow() {
+                    TypeBinding::Unbound(_, type_var_kind) => match type_var_kind {
+                        Kind::Any | Kind::Normal | Kind::Integer | Kind::IntegerOrField => None,
+                        Kind::Numeric(typ) => typ.integral_maximum_size(),
+                    },
+                    TypeBinding::Bound(typ) => typ.integral_maximum_size(),
+                }
+            }
+            Type::Alias(alias, args) => alias.borrow().get_type(args).integral_maximum_size(),
+            Type::NamedGeneric(binding, _name) => match &*binding.borrow() {
+                TypeBinding::Bound(typ) => typ.integral_maximum_size(),
+                TypeBinding::Unbound(_, kind) => kind.integral_maximum_size(),
+            },
+            Type::MutableReference(typ) => typ.integral_maximum_size(),
+            Type::InfixExpr(lhs, _op, rhs) => lhs.infix_kind(rhs).integral_maximum_size(),
+            Type::Constant(_, kind) => kind.integral_maximum_size(),
+
+            Type::Array(..)
+            | Type::Slice(..)
+            | Type::String(..)
+            | Type::FmtString(..)
+            | Type::Unit
+            | Type::Tuple(..)
+            | Type::Struct(..)
+            | Type::TraitAsType(..)
+            | Type::Function(..)
+            | Type::Forall(..)
+            | Type::Quoted(..)
+            | Type::Error => None,
+        }
+    }
 }
 
 /// Wraps a given `expression` in `expression.as_slice()`
@@ -2389,15 +2509,29 @@ fn convert_array_expression_to_slice(
 
 impl BinaryTypeOperator {
     /// Perform the actual rust numeric operation associated with this operator
-    // TODO(https://github.com/noir-lang/noir/pull/6137): the Kind is included
-    // since it'll be needed for size checks
-    pub fn function(self, a: u32, b: u32, _kind: &Kind) -> Option<u32> {
-        match self {
-            BinaryTypeOperator::Addition => a.checked_add(b),
-            BinaryTypeOperator::Subtraction => a.checked_sub(b),
-            BinaryTypeOperator::Multiplication => a.checked_mul(b),
-            BinaryTypeOperator::Division => a.checked_div(b),
-            BinaryTypeOperator::Modulo => a.checked_rem(b),
+    pub fn function(self, a: FieldElement, b: FieldElement, kind: &Kind) -> Option<FieldElement> {
+        match kind.follow_bindings().integral_maximum_size() {
+            None => match self {
+                BinaryTypeOperator::Addition => Some(a + b),
+                BinaryTypeOperator::Subtraction => Some(a - b),
+                BinaryTypeOperator::Multiplication => Some(a * b),
+                BinaryTypeOperator::Division => (b != FieldElement::zero()).then(|| a / b),
+                BinaryTypeOperator::Modulo => None,
+            },
+            Some(_maximum_size) => {
+                let a = a.to_i128();
+                let b = b.to_i128();
+
+                let result = match self {
+                    BinaryTypeOperator::Addition => a.checked_add(b)?,
+                    BinaryTypeOperator::Subtraction => a.checked_sub(b)?,
+                    BinaryTypeOperator::Multiplication => a.checked_mul(b)?,
+                    BinaryTypeOperator::Division => a.checked_div(b)?,
+                    BinaryTypeOperator::Modulo => a.checked_rem(b)?,
+                };
+
+                Some(result.into())
+            }
         }
     }
 
diff --git a/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs b/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
index af94ef27535..0eee7dbf824 100644
--- a/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
+++ b/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
@@ -1,5 +1,7 @@
 use std::collections::BTreeMap;
 
+use acvm::{AcirField, FieldElement};
+
 use crate::{BinaryTypeOperator, Type, TypeBindings, UnificationError};
 
 impl Type {
@@ -15,10 +17,11 @@ impl Type {
     pub fn canonicalize(&self) -> Type {
         match self.follow_bindings() {
             Type::InfixExpr(lhs, op, rhs) => {
-                // evaluate_to_u32 also calls canonicalize so if we just called
-                // `self.evaluate_to_u32()` we'd get infinite recursion.
+                let kind = lhs.infix_kind(&rhs);
+                // evaluate_to_field_element also calls canonicalize so if we just called
+                // `self.evaluate_to_field_element(..)` we'd get infinite recursion.
                 if let (Some(lhs_u32), Some(rhs_u32)) =
-                    (lhs.evaluate_to_u32(), rhs.evaluate_to_u32())
+                    (lhs.evaluate_to_field_element(&kind), rhs.evaluate_to_field_element(&kind))
                 {
                     let kind = lhs.infix_kind(&rhs);
                     if let Some(result) = op.function(lhs_u32, rhs_u32, &kind) {
@@ -58,7 +61,11 @@ impl Type {
         // Maps each term to the number of times that term was used.
         let mut sorted = BTreeMap::new();
 
-        let zero_value = if op == BinaryTypeOperator::Addition { 0 } else { 1 };
+        let zero_value = if op == BinaryTypeOperator::Addition {
+            FieldElement::zero()
+        } else {
+            FieldElement::one()
+        };
         let mut constant = zero_value;
 
         // Push each non-constant term to `sorted` to sort them. Recur on InfixExprs with the same operator.
@@ -175,14 +182,15 @@ impl Type {
     fn parse_partial_constant_expr(
         lhs: &Type,
         rhs: &Type,
-    ) -> Option<(Box<Type>, BinaryTypeOperator, u32, u32)> {
-        let rhs = rhs.evaluate_to_u32()?;
+    ) -> Option<(Box<Type>, BinaryTypeOperator, FieldElement, FieldElement)> {
+        let kind = lhs.infix_kind(rhs);
+        let rhs = rhs.evaluate_to_field_element(&kind)?;
 
         let Type::InfixExpr(l_type, l_op, l_rhs) = lhs.follow_bindings() else {
             return None;
         };
 
-        let l_rhs = l_rhs.evaluate_to_u32()?;
+        let l_rhs = l_rhs.evaluate_to_field_element(&kind)?;
         Some((l_type, l_op, l_rhs, rhs))
     }
 
@@ -215,8 +223,12 @@ impl Type {
                 if l_op == Division {
                     op = op.inverse()?;
                 }
+
+                let divides_evenly = !lhs.infix_kind(rhs).is_type_level_field_element()
+                    && l_const.to_i128().checked_rem(r_const.to_i128()) == Some(0);
+
                 // If op is a division we need to ensure it divides evenly
-                if op == Division && (r_const == 0 || l_const % r_const != 0) {
+                if op == Division && (r_const == FieldElement::zero() || !divides_evenly) {
                     None
                 } else {
                     let result = op.function(l_const, r_const, &lhs.infix_kind(rhs))?;
@@ -237,8 +249,9 @@ impl Type {
     ) -> Result<(), UnificationError> {
         if let Type::InfixExpr(lhs_a, op_a, rhs_a) = self {
             if let Some(inverse) = op_a.inverse() {
-                if let Some(rhs_a_u32) = rhs_a.evaluate_to_u32() {
-                    let rhs_a = Box::new(Type::Constant(rhs_a_u32, lhs_a.infix_kind(rhs_a)));
+                let kind = lhs_a.infix_kind(rhs_a);
+                if let Some(rhs_a_value) = rhs_a.evaluate_to_field_element(&kind) {
+                    let rhs_a = Box::new(Type::Constant(rhs_a_value, kind));
                     let new_other = Type::InfixExpr(Box::new(other.clone()), inverse, rhs_a);
 
                     let mut tmp_bindings = bindings.clone();
@@ -252,8 +265,9 @@ impl Type {
 
         if let Type::InfixExpr(lhs_b, op_b, rhs_b) = other {
             if let Some(inverse) = op_b.inverse() {
-                if let Some(rhs_b_u32) = rhs_b.evaluate_to_u32() {
-                    let rhs_b = Box::new(Type::Constant(rhs_b_u32, lhs_b.infix_kind(rhs_b)));
+                let kind = lhs_b.infix_kind(rhs_b);
+                if let Some(rhs_b_value) = rhs_b.evaluate_to_field_element(&kind) {
+                    let rhs_b = Box::new(Type::Constant(rhs_b_value, kind));
                     let new_self = Type::InfixExpr(Box::new(self.clone()), inverse, rhs_b);
 
                     let mut tmp_bindings = bindings.clone();
diff --git a/compiler/noirc_frontend/src/monomorphization/mod.rs b/compiler/noirc_frontend/src/monomorphization/mod.rs
index 295aa9056b6..beb0b8712b7 100644
--- a/compiler/noirc_frontend/src/monomorphization/mod.rs
+++ b/compiler/noirc_frontend/src/monomorphization/mod.rs
@@ -928,9 +928,11 @@ impl<'interner> Monomorphizer<'interner> {
                     TypeBinding::Unbound(_, _) => {
                         unreachable!("Unbound type variable used in expression")
                     }
-                    TypeBinding::Bound(binding) => binding.evaluate_to_u32().unwrap_or_else(|| {
-                        panic!("Non-numeric type variable used in expression expecting a value")
-                    }),
+                    TypeBinding::Bound(binding) => binding
+                        .evaluate_to_field_element(&Kind::Numeric(numeric_typ.clone()))
+                        .unwrap_or_else(|| {
+                            panic!("Non-numeric type variable used in expression expecting a value")
+                        }),
                 };
                 let location = self.interner.id_location(expr_id);
 
@@ -942,12 +944,7 @@ impl<'interner> Monomorphizer<'interner> {
                 }
 
                 let typ = Self::convert_type(&typ, ident.location)?;
-                ast::Expression::Literal(ast::Literal::Integer(
-                    (value as u128).into(),
-                    false,
-                    typ,
-                    location,
-                ))
+                ast::Expression::Literal(ast::Literal::Integer(value, false, typ, location))
             }
         };
 
diff --git a/compiler/noirc_frontend/src/parser/parser/type_expression.rs b/compiler/noirc_frontend/src/parser/parser/type_expression.rs
index c3f27d9d49a..7dd59aedb45 100644
--- a/compiler/noirc_frontend/src/parser/parser/type_expression.rs
+++ b/compiler/noirc_frontend/src/parser/parser/type_expression.rs
@@ -1,14 +1,11 @@
 use crate::{
-    ast::{
-        Expression, ExpressionKind, GenericTypeArgs, Literal, UnresolvedType, UnresolvedTypeData,
-        UnresolvedTypeExpression,
-    },
-    parser::{labels::ParsingRuleLabel, ParserError, ParserErrorReason},
+    ast::{GenericTypeArgs, UnresolvedType, UnresolvedTypeData, UnresolvedTypeExpression},
+    parser::{labels::ParsingRuleLabel, ParserError},
     token::Token,
     BinaryTypeOperator,
 };
 
-use acvm::acir::AcirField;
+use acvm::acir::{AcirField, FieldElement};
 use noirc_errors::Span;
 
 use super::{parse_many::separated_by_comma_until_right_paren, Parser};
@@ -119,7 +116,7 @@ impl<'a> Parser<'a> {
         if self.eat(Token::Minus) {
             return match self.parse_term_type_expression() {
                 Some(rhs) => {
-                    let lhs = UnresolvedTypeExpression::Constant(0, start_span);
+                    let lhs = UnresolvedTypeExpression::Constant(FieldElement::zero(), start_span);
                     let op = BinaryTypeOperator::Subtraction;
                     let span = self.span_since(start_span);
                     Some(UnresolvedTypeExpression::BinaryOperation(
@@ -165,20 +162,6 @@ impl<'a> Parser<'a> {
             return None;
         };
 
-        let int = if let Some(int) = int.try_to_u32() {
-            int
-        } else {
-            let err_expr = Expression {
-                kind: ExpressionKind::Literal(Literal::Integer(int, false)),
-                span: self.previous_token_span,
-            };
-            self.push_error(
-                ParserErrorReason::InvalidTypeExpression(err_expr),
-                self.previous_token_span,
-            );
-            0
-        };
-
         Some(UnresolvedTypeExpression::Constant(int, self.previous_token_span))
     }
 
@@ -267,7 +250,7 @@ impl<'a> Parser<'a> {
             // If we ate '-' what follows must be a type expression, never a type
             return match self.parse_term_type_expression() {
                 Some(rhs) => {
-                    let lhs = UnresolvedTypeExpression::Constant(0, start_span);
+                    let lhs = UnresolvedTypeExpression::Constant(FieldElement::zero(), start_span);
                     let op = BinaryTypeOperator::Subtraction;
                     let span = self.span_since(start_span);
                     let type_expr = UnresolvedTypeExpression::BinaryOperation(
@@ -444,7 +427,7 @@ mod tests {
         let UnresolvedTypeExpression::Constant(n, _) = expr else {
             panic!("Expected constant");
         };
-        assert_eq!(n, 42);
+        assert_eq!(n, 42_u32.into());
     }
 
     #[test]
@@ -496,7 +479,7 @@ mod tests {
         let UnresolvedTypeExpression::Constant(n, _) = expr else {
             panic!("Expected constant");
         };
-        assert_eq!(n, 42);
+        assert_eq!(n, 42_u32.into());
     }
 
     #[test]
diff --git a/compiler/noirc_frontend/src/parser/parser/types.rs b/compiler/noirc_frontend/src/parser/parser/types.rs
index 6702704d32c..42fae40f669 100644
--- a/compiler/noirc_frontend/src/parser/parser/types.rs
+++ b/compiler/noirc_frontend/src/parser/parser/types.rs
@@ -1,3 +1,5 @@
+use acvm::{AcirField, FieldElement};
+
 use crate::{
     ast::{UnresolvedType, UnresolvedTypeData, UnresolvedTypeExpression},
     parser::{labels::ParsingRuleLabel, ParserErrorReason},
@@ -137,7 +139,8 @@ impl<'a> Parser<'a> {
 
         if !self.eat_less() {
             self.expected_token(Token::Less);
-            let expr = UnresolvedTypeExpression::Constant(0, self.current_token_span);
+            let expr =
+                UnresolvedTypeExpression::Constant(FieldElement::zero(), self.current_token_span);
             return Some(UnresolvedTypeData::String(expr));
         }
 
@@ -145,7 +148,7 @@ impl<'a> Parser<'a> {
             Ok(expr) => expr,
             Err(error) => {
                 self.errors.push(error);
-                UnresolvedTypeExpression::Constant(0, self.current_token_span)
+                UnresolvedTypeExpression::Constant(FieldElement::zero(), self.current_token_span)
             }
         };
 
@@ -161,7 +164,8 @@ impl<'a> Parser<'a> {
 
         if !self.eat_less() {
             self.expected_token(Token::Less);
-            let expr = UnresolvedTypeExpression::Constant(0, self.current_token_span);
+            let expr =
+                UnresolvedTypeExpression::Constant(FieldElement::zero(), self.current_token_span);
             let typ = UnresolvedTypeData::Error.with_span(self.span_at_previous_token_end());
             return Some(UnresolvedTypeData::FormatString(expr, Box::new(typ)));
         }
@@ -170,7 +174,7 @@ impl<'a> Parser<'a> {
             Ok(expr) => expr,
             Err(error) => {
                 self.errors.push(error);
-                UnresolvedTypeExpression::Constant(0, self.current_token_span)
+                UnresolvedTypeExpression::Constant(FieldElement::zero(), self.current_token_span)
             }
         };
 
diff --git a/compiler/noirc_frontend/src/tests.rs b/compiler/noirc_frontend/src/tests.rs
index 3d099fe09c1..f190ef38bab 100644
--- a/compiler/noirc_frontend/src/tests.rs
+++ b/compiler/noirc_frontend/src/tests.rs
@@ -1946,6 +1946,125 @@ fn numeric_generic_used_in_turbofish() {
     assert_no_errors(src);
 }
 
+// TODO(https://github.com/noir-lang/noir/issues/6245):
+// allow u16 to be used as an array size
+#[test]
+fn numeric_generic_u16_array_size() {
+    let src = r#"
+    fn len<let N: u32>(_arr: [Field; N]) -> u32 {
+        N
+    }
+
+    pub fn foo<let N: u16>() -> u32 {
+        let fields: [Field; N] = [0; N];
+        len(fields)
+    }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 2);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
+    ));
+    assert!(matches!(
+        errors[1].0,
+        CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
+    ));
+}
+
+// TODO(https://github.com/noir-lang/noir/issues/6238):
+// The EvaluatedGlobalIsntU32 warning is a stopgap
+// (originally from https://github.com/noir-lang/noir/issues/6125)
+#[test]
+fn numeric_generic_field_larger_than_u32() {
+    let src = r#"
+        global A: Field = 4294967297;
+        
+        fn foo<let A: Field>() { }
+        
+        fn main() {
+            let _ = foo::<A>();
+        }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 2);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::EvaluatedGlobalIsntU32 { .. }),
+    ));
+    assert!(matches!(
+        errors[1].0,
+        CompilationError::ResolverError(ResolverError::IntegerTooLarge { .. })
+    ));
+}
+
+// TODO(https://github.com/noir-lang/noir/issues/6238):
+// The EvaluatedGlobalIsntU32 warning is a stopgap
+// (originally from https://github.com/noir-lang/noir/issues/6126)
+#[test]
+fn numeric_generic_field_arithmetic_larger_than_u32() {
+    let src = r#"
+        struct Foo<let F: Field> {}
+
+        impl<let F: Field> Foo<F> {
+            fn size(self) -> Field {
+                F
+            }
+        }
+        
+        // 2^32 - 1
+        global A: Field = 4294967295;
+        
+        fn foo<let A: Field>() -> Foo<A + A> {
+            Foo {}
+        }
+        
+        fn main() {
+            let _ = foo::<A>().size();
+        }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 2);
+
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::EvaluatedGlobalIsntU32 { .. }),
+    ));
+
+    assert!(matches!(
+        errors[1].0,
+        CompilationError::ResolverError(ResolverError::UnusedVariable { .. })
+    ));
+}
+
+#[test]
+fn cast_256_to_u8_size_checks() {
+    let src = r#"
+        fn main() {
+            assert(256 as u8 == 0);
+        }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 1);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::DownsizingCast { .. }),
+    ));
+}
+
+// TODO(https://github.com/noir-lang/noir/issues/6247):
+// add negative integer literal checks
+#[test]
+fn cast_negative_one_to_u8_size_checks() {
+    let src = r#"
+        fn main() {
+            assert((-1) as u8 != 0);
+        }
+    "#;
+    let errors = get_program_errors(src);
+    assert!(errors.is_empty());
+}
+
 #[test]
 fn constant_used_with_numeric_generic() {
     let src = r#"
@@ -2042,11 +2161,25 @@ fn numeric_generics_type_kind_mismatch() {
     }
     "#;
     let errors = get_program_errors(src);
-    assert_eq!(errors.len(), 1);
+    assert_eq!(errors.len(), 3);
+
+    // TODO(https://github.com/noir-lang/noir/issues/6238):
+    // The EvaluatedGlobalIsntU32 warning is a stopgap
     assert!(matches!(
         errors[0].0,
+        CompilationError::TypeError(TypeCheckError::EvaluatedGlobalIsntU32 { .. }),
+    ));
+
+    assert!(matches!(
+        errors[1].0,
         CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
     ));
+
+    // TODO(https://github.com/noir-lang/noir/issues/6238): see above
+    assert!(matches!(
+        errors[2].0,
+        CompilationError::TypeError(TypeCheckError::EvaluatedGlobalIsntU32 { .. }),
+    ));
 }
 
 #[test]
@@ -3116,8 +3249,10 @@ fn struct_array_len() {
     ));
 }
 
+// TODO(https://github.com/noir-lang/noir/issues/6245):
+// support u16 as an array size
 #[test]
-fn non_u32_in_array_length() {
+fn non_u32_as_array_length() {
     let src = r#"
         global ARRAY_LEN: u8 = 3;
 
@@ -3127,10 +3262,13 @@ fn non_u32_in_array_length() {
     "#;
 
     let errors = get_program_errors(src);
-    assert_eq!(errors.len(), 1);
-
+    assert_eq!(errors.len(), 2);
     assert!(matches!(
         errors[0].0,
+        CompilationError::TypeError(TypeCheckError::EvaluatedGlobalIsntU32 { .. })
+    ));
+    assert!(matches!(
+        errors[1].0,
         CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. })
     ));
 }
@@ -3185,17 +3323,17 @@ fn trait_unconstrained_methods_typechecked_correctly() {
                 self
             }
 
-            unconstrained fn foo(self) -> u64;
+            unconstrained fn foo(self) -> Field;
         }
 
-        impl Foo for Field {
-            unconstrained fn foo(self) -> u64 {
-                self as u64
+        impl Foo for u64 {
+            unconstrained fn foo(self) -> Field {
+                self as Field
             }
         }
 
         unconstrained fn main() {
-            assert_eq(2.foo() as Field, 2.identity());
+            assert_eq(2.foo(), 2.identity() as Field);
         }
     "#;
 
diff --git a/test_programs/execution_success/check_large_field_bits/Nargo.toml b/test_programs/execution_success/check_large_field_bits/Nargo.toml
new file mode 100644
index 00000000000..33d5dd66484
--- /dev/null
+++ b/test_programs/execution_success/check_large_field_bits/Nargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "check_large_field_bits"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]
diff --git a/test_programs/execution_success/check_large_field_bits/src/main.nr b/test_programs/execution_success/check_large_field_bits/src/main.nr
new file mode 100644
index 00000000000..1d65b342966
--- /dev/null
+++ b/test_programs/execution_success/check_large_field_bits/src/main.nr
@@ -0,0 +1,45 @@
+// 2^32 + 1
+global A: Field = 4294967297;
+global B: Field = 4294967297;
+
+// 2^33 + 2
+global C: Field = A + B;
+
+fn main() {
+    // 2 * (2^32 + 1) == 2^33 + 2
+    assert(C == 8589934594);
+
+    let mut leading_zeroes = 0;
+    let mut stop = false;
+    let bits: [u1; 64] = C.to_be_bits();
+    for i in 0..64 {
+        if (bits[i] == 0) & !stop {
+            leading_zeroes += 1;
+        } else {
+            stop = true;
+        }
+    }
+    let size = 64 - leading_zeroes;
+
+    // 8589934594 has 34 bits
+    assert(size == 34);
+    C.assert_max_bit_size(34);
+
+    assert(
+        C.to_be_bits() == [
+            1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0
+        ]
+    );
+
+    // leading big-endian bits past 34 are 0's
+    assert(
+        C.to_be_bits() == [
+            0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0
+        ]
+    );
+    assert(
+        C.to_be_bits() == [
+            0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0
+        ]
+    );
+}
diff --git a/tooling/nargo_cli/build.rs b/tooling/nargo_cli/build.rs
index 50f022f64ed..94f74a06149 100644
--- a/tooling/nargo_cli/build.rs
+++ b/tooling/nargo_cli/build.rs
@@ -59,6 +59,15 @@ const IGNORED_BRILLIG_TESTS: [&str; 11] = [
     "is_unconstrained",
 ];
 
+/// Some tests are expected to have warnings
+/// These should be fixed and removed from this list.
+const TESTS_WITH_EXPECTED_WARNINGS: [&str; 2] = [
+    // TODO(https://github.com/noir-lang/noir/issues/6238): remove from list once issue is closed
+    "brillig_cast",
+    // TODO(https://github.com/noir-lang/noir/issues/6238): remove from list once issue is closed
+    "macros_in_comptime",
+];
+
 fn read_test_cases(
     test_data_dir: &Path,
     test_sub_dir: &str,
@@ -234,15 +243,21 @@ fn generate_compile_success_empty_tests(test_file: &mut File, test_data_dir: &Pa
     for (test_name, test_dir) in test_cases {
         let test_dir = test_dir.display();
 
-        let assert_zero_opcodes = r#"
+        let mut assert_zero_opcodes = r#"
         let output = nargo.output().expect("Failed to execute command");
 
         if !output.status.success() {{
             panic!("`nargo info` failed with: {}", String::from_utf8(output.stderr).unwrap_or_default());
         }}
+        "#.to_string();
+
+        if !TESTS_WITH_EXPECTED_WARNINGS.contains(&test_name.as_str()) {
+            assert_zero_opcodes += r#"
+            nargo.assert().success().stderr(predicate::str::contains("warning:").not());
+            "#;
+        }
 
-        nargo.assert().success().stderr(predicate::str::contains("warning:").not());
-    
+        assert_zero_opcodes += r#"
         // `compile_success_empty` tests should be able to compile down to an empty circuit.
         let json: serde_json::Value = serde_json::from_slice(&output.stdout).unwrap_or_else(|e| {{
             panic!("JSON was not well-formatted {:?}\n\n{:?}", e, std::str::from_utf8(&output.stdout))
diff --git a/tooling/nargo_cli/tests/stdlib-props.proptest-regressions b/tooling/nargo_cli/tests/stdlib-props.proptest-regressions
index ab88db8b6c2..d41d504e530 100644
--- a/tooling/nargo_cli/tests/stdlib-props.proptest-regressions
+++ b/tooling/nargo_cli/tests/stdlib-props.proptest-regressions
@@ -5,3 +5,4 @@
 # It is recommended to check this file in to source control so that
 # everyone who runs the test benefits from these saved cases.
 cc 88db0227d5547742f771c14b1679f6783570b46bf7cf9e6897ee1aca4bd5034d # shrinks to io = SnippetInputOutput { description: "force_brillig = false, max_len = 200", inputs: {"input": Vec([Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(1), Field(5), Field(20), Field(133), Field(233), Field(99), Field(2⁶), Field(196), Field(232), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0)]), "message_size": Field(2⁶)}, expected_output: Vec([Field(102), Field(26), Field(94), Field(212), Field(102), Field(1), Field(215), Field(217), Field(167), Field(175), Field(158), Field(18), Field(20), Field(244), Field(158), Field(200), Field(2⁷), Field(186), Field(251), Field(243), Field(20), Field(207), Field(22), Field(3), Field(139), Field(81), Field(207), Field(2⁴), Field(50), Field(167), Field(1), Field(163)]) }
+cc 0f334fe0c29748e8d0964d63f0d1f3a4eee536afa665eabc838045d8e1c67792 # shrinks to io = SnippetInputOutput { description: "force_brillig = true, max_len = 135", inputs: {"input": Vec([Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(0), Field(29), Field(131), Field(217), Field(115), Field(221), Field(92), Field(23), Field(14), Field(58), Field(90), Field(232), Field(155), Field(59), Field(209), Field(2⁴×15), Field(137), Field(214), Field(129), Field(11), Field(140), Field(99), Field(131), Field(188), Field(159), Field(27), Field(206), Field(89), Field(137), Field(248), Field(30), Field(149), Field(194), Field(121), Field(127), Field(245), Field(202), Field(155), Field(203), Field(122), Field(2⁵), Field(209), Field(194), Field(214), Field(11), Field(82), Field(26), Field(244), Field(34), Field(30), Field(125), Field(83), Field(2⁴×13), Field(30), Field(2⁴×10), Field(85), Field(245), Field(220), Field(211), Field(190), Field(46), Field(159), Field(87), Field(74), Field(51), Field(42), Field(202), Field(230), Field(137), Field(127), Field(29), Field(126), Field(243), Field(106), Field(156), Field(2⁴×6), Field(154), Field(70), Field(100), Field(130)]), "message_size": Field(135)}, expected_output: Vec([Field(149), Field(114), Field(68), Field(219), Field(215), Field(147), Field(139), Field(34), Field(145), Field(204), Field(248), Field(145), Field(21), Field(119), Field(2⁵), Field(125), Field(181), Field(142), Field(106), Field(169), Field(202), Field(111), Field(110), Field(6), Field(210), Field(250), Field(2⁴), Field(110), Field(209), Field(2), Field(33), Field(104)]) }