diff --git a/nac3core/src/codegen/mod.rs b/nac3core/src/codegen/mod.rs
index f46b50d9..b96f3bd1 100644
--- a/nac3core/src/codegen/mod.rs
+++ b/nac3core/src/codegen/mod.rs
@@ -41,6 +41,7 @@ pub mod extern_fns;
 mod generator;
 pub mod irrt;
 pub mod llvm_intrinsics;
+pub mod model;
 pub mod numpy;
 pub mod stmt;
 
diff --git a/nac3core/src/codegen/model/any.rs b/nac3core/src/codegen/model/any.rs
new file mode 100644
index 00000000..9b7c9562
--- /dev/null
+++ b/nac3core/src/codegen/model/any.rs
@@ -0,0 +1,34 @@
+use inkwell::{
+    context::Context,
+    types::{BasicType, BasicTypeEnum},
+    values::BasicValueEnum,
+};
+
+use super::*;
+
+#[derive(Debug, Clone, Copy)]
+pub struct AnyModel<'ctx>(pub BasicTypeEnum<'ctx>);
+pub type Anything<'ctx> = Instance<'ctx, AnyModel<'ctx>>;
+
+impl<'ctx> Model<'ctx> for AnyModel<'ctx> {
+    type Value = BasicValueEnum<'ctx>;
+    type Type = BasicTypeEnum<'ctx>;
+
+    fn get_type(&self, _tyctx: TypeContext<'ctx>, _ctx: &'ctx Context) -> Self::Type {
+        self.0
+    }
+
+    fn check_type<T: BasicType<'ctx>>(
+        &self,
+        _tyctx: TypeContext<'ctx>,
+        _ctx: &'ctx Context,
+        ty: T,
+    ) -> Result<(), ModelError> {
+        let ty = ty.as_basic_type_enum();
+        if ty == self.0 {
+            Ok(())
+        } else {
+            Err(ModelError(format!("Expecting {}, but got {}", self.0, ty)))
+        }
+    }
+}
diff --git a/nac3core/src/codegen/model/core.rs b/nac3core/src/codegen/model/core.rs
new file mode 100644
index 00000000..deb5f036
--- /dev/null
+++ b/nac3core/src/codegen/model/core.rs
@@ -0,0 +1,146 @@
+use std::fmt;
+
+use inkwell::{context::Context, types::*, values::*};
+
+use super::*;
+use crate::codegen::{CodeGenContext, CodeGenerator};
+
+#[derive(Clone, Copy)]
+pub struct TypeContext<'ctx> {
+    pub size_type: IntType<'ctx>,
+}
+
+pub trait HasTypeContext {
+    fn type_context<'ctx>(&self, ctx: &'ctx Context) -> TypeContext<'ctx>;
+}
+
+impl<T: CodeGenerator + ?Sized> HasTypeContext for T {
+    fn type_context<'ctx>(&self, ctx: &'ctx Context) -> TypeContext<'ctx> {
+        TypeContext { size_type: self.get_size_type(ctx) }
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct ModelError(pub String);
+
+impl ModelError {
+    pub(super) fn under_context(mut self, context: &str) -> Self {
+        self.0.push_str(" ... in ");
+        self.0.push_str(context);
+        self
+    }
+}
+
+pub trait Model<'ctx>: fmt::Debug + Clone + Copy {
+    type Value: BasicValue<'ctx> + TryFrom<BasicValueEnum<'ctx>>;
+    type Type: BasicType<'ctx>;
+
+    /// Return the [`BasicType`] of this model.
+    fn get_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Self::Type;
+
+    /// Check if a [`BasicType`] is the same type of this model.
+    fn check_type<T: BasicType<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        ty: T,
+    ) -> Result<(), ModelError>;
+
+    /// Create an instance from a value with [`Instance::model`] being this model.
+    ///
+    /// Caller must make sure the type of `value` and the type of this `model` are equivalent.
+    fn believe_value(&self, value: Self::Value) -> Instance<'ctx, Self> {
+        Instance { model: *self, value }
+    }
+
+    /// Check if a [`BasicValue`]'s type is equivalent to the type of this model.
+    /// Wrap it into an [`Instance`] if it is.
+    fn check_value<V: BasicValue<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        value: V,
+    ) -> Result<Instance<'ctx, Self>, ModelError> {
+        let value = value.as_basic_value_enum();
+        self.check_type(tyctx, ctx, value.get_type())
+            .map_err(|err| err.under_context("the value {value:?}"))?;
+
+        let Ok(value) = Self::Value::try_from(value) else {
+            unreachable!("check_type() has bad implementation")
+        };
+        Ok(self.believe_value(value))
+    }
+
+    // Allocate a value on the stack and return its pointer.
+    fn alloca(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        name: &str,
+    ) -> Ptr<'ctx, Self> {
+        let pmodel = PtrModel(*self);
+        let p = ctx.builder.build_alloca(self.get_type(tyctx, ctx.ctx), name).unwrap();
+        pmodel.believe_value(p)
+    }
+
+    // Allocate an array on the stack and return its pointer.
+    fn array_alloca(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        len: IntValue<'ctx>,
+        name: &str,
+    ) -> Ptr<'ctx, Self> {
+        let pmodel = PtrModel(*self);
+        let p = ctx.builder.build_array_alloca(self.get_type(tyctx, ctx.ctx), len, name).unwrap();
+        pmodel.believe_value(p)
+    }
+
+    fn var_alloca<G: CodeGenerator + ?Sized>(
+        &self,
+        generator: &mut G,
+        ctx: &mut CodeGenContext<'ctx, '_>,
+        name: Option<&str>,
+    ) -> Result<Ptr<'ctx, Self>, String> {
+        let tyctx = generator.type_context(ctx.ctx);
+
+        let pmodel = PtrModel(*self);
+        let p = generator.gen_var_alloc(
+            ctx,
+            self.get_type(tyctx, ctx.ctx).as_basic_type_enum(),
+            name,
+        )?;
+        Ok(pmodel.believe_value(p))
+    }
+
+    fn array_var_alloca<G: CodeGenerator + ?Sized>(
+        &self,
+        generator: &mut G,
+        ctx: &mut CodeGenContext<'ctx, '_>,
+        len: IntValue<'ctx>,
+        name: Option<&'ctx str>,
+    ) -> Result<Ptr<'ctx, Self>, String> {
+        let tyctx = generator.type_context(ctx.ctx);
+
+        // TODO: Remove ArraySliceValue
+        let pmodel = PtrModel(*self);
+        let p = generator.gen_array_var_alloc(
+            ctx,
+            self.get_type(tyctx, ctx.ctx).as_basic_type_enum(),
+            len,
+            name,
+        )?;
+        Ok(pmodel.believe_value(PointerValue::from(p)))
+    }
+}
+
+#[derive(Debug, Clone, Copy)]
+pub struct Instance<'ctx, M: Model<'ctx>> {
+    /// The model of this instance.
+    pub model: M,
+    /// The value of this instance.
+    ///
+    /// Caller must make sure the type of `value` and the type of this `model` are equivalent,
+    /// down to having the same [`IntType::get_bit_width`] in case of [`IntType`] for example.
+    pub value: M::Value,
+}
diff --git a/nac3core/src/codegen/model/int.rs b/nac3core/src/codegen/model/int.rs
new file mode 100644
index 00000000..673641d9
--- /dev/null
+++ b/nac3core/src/codegen/model/int.rs
@@ -0,0 +1,231 @@
+use std::fmt;
+
+use inkwell::{context::Context, types::IntType, values::IntValue, IntPredicate};
+
+use crate::codegen::{CodeGenContext, CodeGenerator};
+
+use super::*;
+
+pub trait IntKind<'ctx>: fmt::Debug + Clone + Copy {
+    fn get_int_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> IntType<'ctx>;
+}
+
+#[derive(Debug, Clone, Copy, Default)]
+pub struct Bool;
+#[derive(Debug, Clone, Copy, Default)]
+pub struct Byte;
+#[derive(Debug, Clone, Copy, Default)]
+pub struct Int32;
+#[derive(Debug, Clone, Copy, Default)]
+pub struct Int64;
+#[derive(Debug, Clone, Copy, Default)]
+pub struct SizeT;
+
+impl<'ctx> IntKind<'ctx> for Bool {
+    fn get_int_type(&self, _tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> IntType<'ctx> {
+        ctx.bool_type()
+    }
+}
+
+impl<'ctx> IntKind<'ctx> for Byte {
+    fn get_int_type(&self, _tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> IntType<'ctx> {
+        ctx.i8_type()
+    }
+}
+
+impl<'ctx> IntKind<'ctx> for Int32 {
+    fn get_int_type(&self, _tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> IntType<'ctx> {
+        ctx.i32_type()
+    }
+}
+
+impl<'ctx> IntKind<'ctx> for Int64 {
+    fn get_int_type(&self, _tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> IntType<'ctx> {
+        ctx.i64_type()
+    }
+}
+
+impl<'ctx> IntKind<'ctx> for SizeT {
+    fn get_int_type(&self, tyctx: TypeContext<'ctx>, _ctx: &'ctx Context) -> IntType<'ctx> {
+        tyctx.size_type
+    }
+}
+
+#[derive(Debug, Clone, Copy)]
+pub struct AnyInt<'ctx>(pub IntType<'ctx>);
+
+impl<'ctx> IntKind<'ctx> for AnyInt<'ctx> {
+    fn get_int_type(&self, _tyctx: TypeContext<'ctx>, _ctx: &'ctx Context) -> IntType<'ctx> {
+        self.0
+    }
+}
+
+#[derive(Debug, Clone, Copy, Default)]
+pub struct IntModel<N>(pub N);
+pub type Int<'ctx, N> = Instance<'ctx, IntModel<N>>;
+
+impl<'ctx, N: IntKind<'ctx>> Model<'ctx> for IntModel<N> {
+    type Value = IntValue<'ctx>;
+    type Type = IntType<'ctx>;
+
+    #[must_use]
+    fn get_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Self::Type {
+        self.0.get_int_type(tyctx, ctx)
+    }
+
+    fn check_type<T: inkwell::types::BasicType<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        ty: T,
+    ) -> Result<(), ModelError> {
+        let ty = ty.as_basic_type_enum();
+        let Ok(ty) = IntType::try_from(ty) else {
+            return Err(ModelError(format!("Expecting IntType, but got {ty:?}")));
+        };
+
+        let exp_ty = self.0.get_int_type(tyctx, ctx);
+        if ty.get_bit_width() != exp_ty.get_bit_width() {
+            return Err(ModelError(format!(
+                "Expecting IntType to have {} bit(s), but got {} bit(s)",
+                exp_ty.get_bit_width(),
+                ty.get_bit_width()
+            )));
+        }
+
+        Ok(())
+    }
+}
+
+impl<'ctx, N: IntKind<'ctx>> IntModel<N> {
+    pub fn constant(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        value: u64,
+    ) -> Int<'ctx, N> {
+        let value = self.get_type(tyctx, ctx).const_int(value, false);
+        self.believe_value(value)
+    }
+
+    pub fn const_0(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Int<'ctx, N> {
+        self.constant(tyctx, ctx, 0)
+    }
+
+    pub fn const_1(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Int<'ctx, N> {
+        self.constant(tyctx, ctx, 1)
+    }
+
+    pub fn s_extend_or_bit_cast(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        value: IntValue<'ctx>,
+        name: &str,
+    ) -> Int<'ctx, N> {
+        let value = ctx
+            .builder
+            .build_int_s_extend_or_bit_cast(value, self.get_type(tyctx, ctx.ctx), name)
+            .unwrap();
+        self.believe_value(value)
+    }
+
+    pub fn truncate(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        value: IntValue<'ctx>,
+        name: &str,
+    ) -> Int<'ctx, N> {
+        let value =
+            ctx.builder.build_int_truncate(value, self.get_type(tyctx, ctx.ctx), name).unwrap();
+        self.believe_value(value)
+    }
+}
+
+impl IntModel<Bool> {
+    #[must_use]
+    pub fn const_false<'ctx>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+    ) -> Int<'ctx, Bool> {
+        self.constant(tyctx, ctx, 0)
+    }
+
+    #[must_use]
+    pub fn const_true<'ctx>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+    ) -> Int<'ctx, Bool> {
+        self.constant(tyctx, ctx, 1)
+    }
+}
+
+impl<'ctx, N: IntKind<'ctx>> Int<'ctx, N> {
+    pub fn s_extend_or_bit_cast<NewN: IntKind<'ctx>, G: CodeGenerator + ?Sized>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        to_int_kind: NewN,
+        name: &str,
+    ) -> Int<'ctx, NewN> {
+        IntModel(to_int_kind).s_extend_or_bit_cast(tyctx, ctx, self.value, name)
+    }
+
+    pub fn truncate<NewN: IntKind<'ctx>, G: CodeGenerator + ?Sized>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        to_int_kind: NewN,
+        name: &str,
+    ) -> Int<'ctx, NewN> {
+        IntModel(to_int_kind).truncate(tyctx, ctx, self.value, name)
+    }
+
+    #[must_use]
+    pub fn add<G: CodeGenerator + ?Sized>(
+        &self,
+        ctx: &CodeGenContext<'ctx, '_>,
+        other: Int<'ctx, N>,
+        name: &str,
+    ) -> Int<'ctx, N> {
+        let value = ctx.builder.build_int_add(self.value, other.value, name).unwrap();
+        self.model.believe_value(value)
+    }
+
+    #[must_use]
+    pub fn sub<G: CodeGenerator + ?Sized>(
+        &self,
+        ctx: &CodeGenContext<'ctx, '_>,
+        other: Int<'ctx, N>,
+        name: &str,
+    ) -> Int<'ctx, N> {
+        let value = ctx.builder.build_int_sub(self.value, other.value, name).unwrap();
+        self.model.believe_value(value)
+    }
+
+    #[must_use]
+    pub fn mul<G: CodeGenerator + ?Sized>(
+        &self,
+        ctx: &CodeGenContext<'ctx, '_>,
+        other: Int<'ctx, N>,
+        name: &str,
+    ) -> Int<'ctx, N> {
+        let value = ctx.builder.build_int_mul(self.value, other.value, name).unwrap();
+        self.model.believe_value(value)
+    }
+
+    pub fn compare<G: CodeGenerator + ?Sized>(
+        &self,
+        ctx: &CodeGenContext<'ctx, '_>,
+        op: IntPredicate,
+        other: Int<'ctx, N>,
+        name: &str,
+    ) -> Int<'ctx, Bool> {
+        let bool_model = IntModel(Bool);
+        let value = ctx.builder.build_int_compare(op, self.value, other.value, name).unwrap();
+        bool_model.believe_value(value)
+    }
+}
diff --git a/nac3core/src/codegen/model/mod.rs b/nac3core/src/codegen/model/mod.rs
new file mode 100644
index 00000000..c030f7cb
--- /dev/null
+++ b/nac3core/src/codegen/model/mod.rs
@@ -0,0 +1,11 @@
+mod any;
+mod core;
+mod int;
+mod ptr;
+mod structure;
+
+pub use any::*;
+pub use core::*;
+pub use int::*;
+pub use ptr::*;
+pub use structure::*;
diff --git a/nac3core/src/codegen/model/ptr.rs b/nac3core/src/codegen/model/ptr.rs
new file mode 100644
index 00000000..febac3c7
--- /dev/null
+++ b/nac3core/src/codegen/model/ptr.rs
@@ -0,0 +1,136 @@
+use inkwell::{
+    context::Context,
+    types::{BasicType, BasicTypeEnum, PointerType},
+    values::{IntValue, PointerValue},
+    AddressSpace,
+};
+
+use crate::codegen::CodeGenContext;
+
+use super::*;
+
+#[derive(Debug, Clone, Copy, Default)]
+pub struct PtrModel<Element>(pub Element);
+pub type Ptr<'ctx, Element> = Instance<'ctx, PtrModel<Element>>;
+
+impl<'ctx, Element: Model<'ctx>> Model<'ctx> for PtrModel<Element> {
+    type Value = PointerValue<'ctx>;
+    type Type = PointerType<'ctx>;
+
+    fn get_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Self::Type {
+        self.0.get_type(tyctx, ctx).ptr_type(AddressSpace::default())
+    }
+
+    fn check_type<T: BasicType<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        ty: T,
+    ) -> Result<(), ModelError> {
+        let ty = ty.as_basic_type_enum();
+        let Ok(ty) = PointerType::try_from(ty) else {
+            return Err(ModelError(format!("Expecting PointerType, but got {ty:?}")));
+        };
+
+        let elem_ty = ty.get_element_type();
+        let Ok(elem_ty) = BasicTypeEnum::try_from(elem_ty) else {
+            return Err(ModelError(format!(
+                "Expecting pointer element type to be a BasicTypeEnum, but got {elem_ty:?}"
+            )));
+        };
+
+        // TODO: inkwell `get_element_type()` will be deprecated.
+        // Remove the check for `get_element_type()` when the time comes.
+        self.0.check_type(tyctx, ctx, elem_ty).map_err(|err| err.under_context("a PointerType"))?;
+
+        Ok(())
+    }
+}
+
+impl<'ctx, Element: Model<'ctx>> PtrModel<Element> {
+    /// Return a ***constant*** nullptr.
+    pub fn nullptr(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Ptr<'ctx, Element> {
+        let ptr = self.get_type(tyctx, ctx).const_null();
+        self.believe_value(ptr)
+    }
+
+    /// Cast a pointer into this model with [`inkwell::builder::Builder::build_pointer_cast`]
+    pub fn pointer_cast(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        ptr: PointerValue<'ctx>,
+        name: &str,
+    ) -> Ptr<'ctx, Element> {
+        let ptr = ctx.builder.build_pointer_cast(ptr, self.get_type(tyctx, ctx.ctx), name).unwrap();
+        self.believe_value(ptr)
+    }
+}
+
+impl<'ctx, Element: Model<'ctx>> Ptr<'ctx, Element> {
+    /// Offset the pointer by [`inkwell::builder::Builder::build_in_bounds_gep`].
+    #[must_use]
+    pub fn offset(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        offset: IntValue<'ctx>,
+        name: &str,
+    ) -> Ptr<'ctx, Element> {
+        let new_ptr =
+            unsafe { ctx.builder.build_in_bounds_gep(self.value, &[offset], name).unwrap() };
+        self.model.check_value(tyctx, ctx.ctx, new_ptr).unwrap()
+    }
+
+    // Load the `i`-th element (0-based) on the array with [`inkwell::builder::Builder::build_in_bounds_gep`].
+    pub fn ix(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        i: IntValue<'ctx>,
+        name: &str,
+    ) -> Instance<'ctx, Element> {
+        self.offset(tyctx, ctx, i, name).load(tyctx, ctx, name)
+    }
+
+    /// Load the value with [`inkwell::builder::Builder::build_load`].
+    pub fn load(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        name: &str,
+    ) -> Instance<'ctx, Element> {
+        let value = ctx.builder.build_load(self.value, name).unwrap();
+        self.model.0.check_value(tyctx, ctx.ctx, value).unwrap() // If unwrap() panics, there is a logic error.
+    }
+
+    /// Store a value with [`inkwell::builder::Builder::build_store`].
+    pub fn store(&self, ctx: &CodeGenContext<'ctx, '_>, value: Instance<'ctx, Element>) {
+        ctx.builder.build_store(self.value, value.value).unwrap();
+    }
+
+    /// Return a casted pointer of element type `NewElement` with [`inkwell::builder::Builder::build_pointer_cast`].
+    pub fn transmute<NewElement: Model<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &CodeGenContext<'ctx, '_>,
+        new_model: NewElement,
+        name: &str,
+    ) -> Ptr<'ctx, NewElement> {
+        PtrModel(new_model).pointer_cast(tyctx, ctx, self.value, name)
+    }
+
+    /// Check if the pointer is null with [`inkwell::builder::Builder::build_is_null`].
+    pub fn is_null(&self, ctx: &CodeGenContext<'ctx, '_>, name: &str) -> Int<'ctx, Bool> {
+        let bool_model = IntModel(Bool);
+        let value = ctx.builder.build_is_null(self.value, name).unwrap();
+        bool_model.believe_value(value)
+    }
+
+    /// Check if the pointer is not null with [`inkwell::builder::Builder::build_is_not_null`].
+    pub fn is_not_null(&self, ctx: &CodeGenContext<'ctx, '_>, name: &str) -> Int<'ctx, Bool> {
+        let bool_model = IntModel(Bool);
+        let value = ctx.builder.build_is_not_null(self.value, name).unwrap();
+        bool_model.believe_value(value)
+    }
+}
diff --git a/nac3core/src/codegen/model/structure.rs b/nac3core/src/codegen/model/structure.rs
new file mode 100644
index 00000000..88b297af
--- /dev/null
+++ b/nac3core/src/codegen/model/structure.rs
@@ -0,0 +1,169 @@
+use std::fmt;
+
+use inkwell::{
+    context::Context,
+    types::{BasicType, BasicTypeEnum, StructType},
+    values::StructValue,
+};
+
+use crate::codegen::CodeGenContext;
+
+use super::*;
+
+#[derive(Debug, Clone, Copy)]
+pub struct GepField<M> {
+    pub gep_index: u64,
+    pub name: &'static str,
+    pub model: M,
+}
+
+pub trait FieldTraversal<'ctx> {
+    type Out<M>;
+
+    fn add<M: Model<'ctx>>(&mut self, name: &'static str, model: M) -> Self::Out<M>;
+
+    /// Like [`FieldTraversal::visit`] but [`Model`] is automatically inferred.
+    fn add_auto<M: Model<'ctx> + Default>(&mut self, name: &'static str) -> Self::Out<M> {
+        self.add(name, M::default())
+    }
+}
+
+pub struct GepFieldTraversal {
+    gep_index_counter: u64,
+}
+
+impl<'ctx> FieldTraversal<'ctx> for GepFieldTraversal {
+    type Out<M> = GepField<M>;
+
+    fn add<M: Model<'ctx>>(&mut self, name: &'static str, model: M) -> Self::Out<M> {
+        let gep_index = self.gep_index_counter;
+        self.gep_index_counter += 1;
+        Self::Out { gep_index, name, model }
+    }
+}
+
+struct TypeFieldTraversal<'ctx> {
+    tyctx: TypeContext<'ctx>,
+    ctx: &'ctx Context,
+    field_types: Vec<BasicTypeEnum<'ctx>>,
+}
+
+impl<'ctx> FieldTraversal<'ctx> for TypeFieldTraversal<'ctx> {
+    type Out<M> = ();
+
+    fn add<M: Model<'ctx>>(&mut self, _name: &'static str, model: M) -> Self::Out<M> {
+        let t = model.get_type(self.tyctx, self.ctx).as_basic_type_enum();
+        self.field_types.push(t);
+    }
+}
+
+struct CheckTypeFieldTraversal<'ctx> {
+    tyctx: TypeContext<'ctx>,
+    ctx: &'ctx Context,
+    index: u32,
+    scrutinee: StructType<'ctx>,
+    errors: Vec<ModelError>,
+}
+
+impl<'ctx> FieldTraversal<'ctx> for CheckTypeFieldTraversal<'ctx> {
+    type Out<M> = ();
+
+    fn add<M: Model<'ctx>>(&mut self, name: &'static str, model: M) -> Self::Out<M> {
+        let i = self.index;
+        self.index += 1;
+
+        if let Some(t) = self.scrutinee.get_field_type_at_index(i) {
+            if let Err(err) = model.check_type(self.tyctx, self.ctx, t) {
+                self.errors.push(err.under_context(format!("At field #{i} '{name}'").as_str()));
+            }
+        } // Otherwise, it will be caught
+    }
+}
+
+pub trait StructKind<'ctx>: fmt::Debug + Clone + Copy {
+    type Fields<F: FieldTraversal<'ctx>>;
+
+    fn traverse_fields<F: FieldTraversal<'ctx>>(&self, traversal: &mut F) -> Self::Fields<F>;
+
+    fn fields(&self) -> Self::Fields<GepFieldTraversal> {
+        self.traverse_fields(&mut GepFieldTraversal { gep_index_counter: 0 })
+    }
+
+    fn get_struct_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> StructType<'ctx> {
+        let mut traversal = TypeFieldTraversal { tyctx, ctx, field_types: Vec::new() };
+        self.traverse_fields(&mut traversal);
+
+        ctx.struct_type(&traversal.field_types, false)
+    }
+}
+
+#[derive(Debug, Clone, Copy, Default)]
+pub struct StructModel<S>(pub S);
+pub type Struct<'ctx, S> = Instance<'ctx, StructModel<S>>;
+
+impl<'ctx, S: StructKind<'ctx>> Model<'ctx> for StructModel<S> {
+    type Value = StructValue<'ctx>;
+    type Type = StructType<'ctx>;
+
+    fn get_type(&self, tyctx: TypeContext<'ctx>, ctx: &'ctx Context) -> Self::Type {
+        self.0.get_struct_type(tyctx, ctx)
+    }
+
+    fn check_type<T: BasicType<'ctx>>(
+        &self,
+        tyctx: TypeContext<'ctx>,
+        ctx: &'ctx Context,
+        ty: T,
+    ) -> Result<(), ModelError> {
+        let ty = ty.as_basic_type_enum();
+        let Ok(ty) = StructType::try_from(ty) else {
+            return Err(ModelError(format!("Expecting StructType, but got {ty:?}")));
+        };
+
+        let mut traversal =
+            CheckTypeFieldTraversal { tyctx, ctx, index: 0, errors: Vec::new(), scrutinee: ty };
+        self.0.traverse_fields(&mut traversal);
+
+        let exp_num_fields = traversal.index;
+        let got_num_fields = u32::try_from(ty.get_field_types().len()).unwrap();
+        if exp_num_fields != got_num_fields {
+            return Err(ModelError(format!(
+                "Expecting StructType with {exp_num_fields} field(s), but got {got_num_fields}"
+            )));
+        }
+
+        if !traversal.errors.is_empty() {
+            return Err(traversal.errors[0].clone()); // TODO: Return other errors as well
+        }
+
+        Ok(())
+    }
+}
+
+impl<'ctx, S: StructKind<'ctx>> Ptr<'ctx, StructModel<S>> {
+    pub fn gep<M, GetField>(
+        &self,
+        ctx: &CodeGenContext<'ctx, '_>,
+        get_field: GetField,
+    ) -> Ptr<'ctx, M>
+    where
+        M: Model<'ctx>,
+        GetField: FnOnce(S::Fields<GepFieldTraversal>) -> GepField<M>,
+    {
+        let field = get_field(self.model.0 .0.fields());
+        let llvm_i32 = ctx.ctx.i32_type(); // i64 would segfault
+
+        let ptr = unsafe {
+            ctx.builder
+                .build_in_bounds_gep(
+                    self.value,
+                    &[llvm_i32.const_zero(), llvm_i32.const_int(field.gep_index, false)],
+                    field.name,
+                )
+                .unwrap()
+        };
+
+        let ptr_model = PtrModel(field.model);
+        ptr_model.believe_value(ptr)
+    }
+}