diff --git a/crates/nargo_cli/tests/test_data/assert/Nargo.toml b/crates/nargo_cli/tests/test_data/assert/Nargo.toml
new file mode 100644
index 00000000000..e0b467ce5da
--- /dev/null
+++ b/crates/nargo_cli/tests/test_data/assert/Nargo.toml
@@ -0,0 +1,5 @@
+[package]
+authors = [""]
+compiler_version = "0.1"
+
+[dependencies]
\ No newline at end of file
diff --git a/crates/nargo_cli/tests/test_data/assert/Prover.toml b/crates/nargo_cli/tests/test_data/assert/Prover.toml
new file mode 100644
index 00000000000..4dd6b405159
--- /dev/null
+++ b/crates/nargo_cli/tests/test_data/assert/Prover.toml
@@ -0,0 +1 @@
+x = "1"
diff --git a/crates/nargo_cli/tests/test_data/assert/src/main.nr b/crates/nargo_cli/tests/test_data/assert/src/main.nr
new file mode 100644
index 00000000000..00e94414c0b
--- /dev/null
+++ b/crates/nargo_cli/tests/test_data/assert/src/main.nr
@@ -0,0 +1,3 @@
+fn main(x: Field) {
+    assert(x == 1);
+}
diff --git a/crates/noirc_abi/src/lib.rs b/crates/noirc_abi/src/lib.rs
index dbd935dcde0..191128b9407 100644
--- a/crates/noirc_abi/src/lib.rs
+++ b/crates/noirc_abi/src/lib.rs
@@ -85,6 +85,30 @@ impl std::fmt::Display for AbiVisibility {
     }
 }
 
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "lowercase")]
+/// Represents whether the return value should compromise of unique witness indices such that no
+/// index occurs within the program's abi more than once.
+///
+/// This is useful for application stacks that require an uniform abi across across multiple
+/// circuits. When index duplication is allowed, the compiler may identify that a public input
+/// reaches the output unaltered and is thus referenced directly, causing the input and output
+/// witness indices to overlap. Similarly, repetitions of copied values in the output may be
+/// optimized away.
+pub enum AbiDistinctness {
+    Distinct,
+    DuplicationAllowed,
+}
+
+impl std::fmt::Display for AbiDistinctness {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            AbiDistinctness::Distinct => write!(f, "distinct"),
+            AbiDistinctness::DuplicationAllowed => write!(f, "duplication-allowed"),
+        }
+    }
+}
+
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(rename_all = "lowercase")]
 pub enum Sign {
diff --git a/crates/noirc_evaluator/src/lib.rs b/crates/noirc_evaluator/src/lib.rs
index a94bc45dbf6..438ada0167c 100644
--- a/crates/noirc_evaluator/src/lib.rs
+++ b/crates/noirc_evaluator/src/lib.rs
@@ -54,6 +54,9 @@ pub struct Evaluator {
     // and increasing as for `public_parameters`. We then use a `Vec` rather
     // than a `BTreeSet` to preserve this order for the ABI.
     return_values: Vec<Witness>,
+    // If true, indicates that the resulting ACIR should enforce that all inputs and outputs are
+    // comprised of unique witness indices by having extra constraints if necessary.
+    return_is_distinct: bool,
 
     opcodes: Vec<AcirOpcode>,
 }
@@ -102,6 +105,11 @@ pub fn create_circuit(
 }
 
 impl Evaluator {
+    // Returns true if the `witness_index` appears in the program's input parameters.
+    fn is_abi_input(&self, witness_index: Witness) -> bool {
+        witness_index.as_usize() <= self.num_witnesses_abi_len
+    }
+
     // Returns true if the `witness_index`
     // was created in the ABI as a private input.
     //
@@ -111,11 +119,17 @@ impl Evaluator {
         // If the `witness_index` is more than the `num_witnesses_abi_len`
         // then it was created after the ABI was processed and is therefore
         // an intermediate variable.
-        let is_intermediate_variable = witness_index.as_usize() > self.num_witnesses_abi_len;
 
         let is_public_input = self.public_parameters.contains(&witness_index);
 
-        !is_intermediate_variable && !is_public_input
+        self.is_abi_input(witness_index) && !is_public_input
+    }
+
+    // True if the main function return has the `distinct` keyword and this particular witness
+    // index has already occurred elsewhere in the abi's inputs and outputs.
+    fn should_proxy_witness_for_abi_output(&self, witness_index: Witness) -> bool {
+        self.return_is_distinct
+            && (self.is_abi_input(witness_index) || self.return_values.contains(&witness_index))
     }
 
     // Creates a new Witness index
@@ -139,6 +153,8 @@ impl Evaluator {
         enable_logging: bool,
         show_output: bool,
     ) -> Result<(), RuntimeError> {
+        self.return_is_distinct =
+            program.return_distinctness == noirc_abi::AbiDistinctness::Distinct;
         let mut ir_gen = IrGenerator::new(program);
         self.parse_abi_alt(&mut ir_gen);
 
diff --git a/crates/noirc_evaluator/src/ssa/acir_gen/operations/return.rs b/crates/noirc_evaluator/src/ssa/acir_gen/operations/return.rs
index 3269af06d16..6aaa3b2fbbd 100644
--- a/crates/noirc_evaluator/src/ssa/acir_gen/operations/return.rs
+++ b/crates/noirc_evaluator/src/ssa/acir_gen/operations/return.rs
@@ -1,3 +1,5 @@
+use acvm::acir::native_types::Expression;
+
 use crate::{
     errors::RuntimeErrorKind,
     ssa::{
@@ -46,7 +48,15 @@ pub(crate) fn evaluate(
                     "we do not allow private ABI inputs to be returned as public outputs",
                 )));
             }
-            evaluator.return_values.push(witness);
+            // Check if the outputted witness needs separating from an existing occurrence in the
+            // abi. This behavior stems from usage of the `distinct` keyword.
+            let return_witness = if evaluator.should_proxy_witness_for_abi_output(witness) {
+                let proxy_constraint = Expression::from(witness);
+                evaluator.create_intermediate_variable(proxy_constraint)
+            } else {
+                witness
+            };
+            evaluator.return_values.push(return_witness);
         }
     }
 
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/cfg.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/cfg.rs
index 05b64e30ed8..d443d574ca8 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/cfg.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/cfg.rs
@@ -115,13 +115,14 @@ impl ControlFlowGraph {
 
 #[cfg(test)]
 mod tests {
-    use crate::ssa_refactor::ir::{instruction::TerminatorInstruction, types::Type};
+    use crate::ssa_refactor::ir::{instruction::TerminatorInstruction, map::Id, types::Type};
 
     use super::{super::function::Function, ControlFlowGraph};
 
     #[test]
     fn empty() {
-        let mut func = Function::new("func".into());
+        let func_id = Id::test_new(0);
+        let mut func = Function::new("func".into(), func_id);
         let block_id = func.entry_block();
         func.dfg[block_id].set_terminator(TerminatorInstruction::Return { return_values: vec![] });
 
@@ -133,74 +134,74 @@ mod tests {
         // Build function of form
         // fn func {
         // block0(cond: u1):
-        //     jmpif cond(), then: block2, else: block1
+        //     jmpif cond, then: block2, else: block1
         // block1():
-        //     jmpif cond(), then: block1, else: block2
+        //     jmpif cond, then: block1, else: block2
         // block2():
-        //     return
+        //     return ()
         // }
-        let mut func = Function::new("func".into());
+        let func_id = Id::test_new(0);
+        let mut func = Function::new("func".into(), func_id);
         let block0_id = func.entry_block();
         let cond = func.dfg.add_block_parameter(block0_id, Type::unsigned(1));
-        let block1_id = func.dfg.new_block();
-        let block2_id = func.dfg.new_block();
+        let block1_id = func.dfg.make_block();
+        let block2_id = func.dfg.make_block();
 
         func.dfg[block0_id].set_terminator(TerminatorInstruction::JmpIf {
             condition: cond,
             then_destination: block2_id,
             else_destination: block1_id,
-            arguments: vec![],
         });
         func.dfg[block1_id].set_terminator(TerminatorInstruction::JmpIf {
             condition: cond,
             then_destination: block1_id,
             else_destination: block2_id,
-            arguments: vec![],
         });
         func.dfg[block2_id].set_terminator(TerminatorInstruction::Return { return_values: vec![] });
 
         let mut cfg = ControlFlowGraph::with_function(&func);
 
+        #[allow(clippy::needless_collect)]
         {
-            let block0_predecessors = cfg.pred_iter(block0_id).collect::<Vec<_>>();
-            let block1_predecessors = cfg.pred_iter(block1_id).collect::<Vec<_>>();
-            let block2_predecessors = cfg.pred_iter(block2_id).collect::<Vec<_>>();
+            let block0_predecessors: Vec<_> = cfg.pred_iter(block0_id).collect();
+            let block1_predecessors: Vec<_> = cfg.pred_iter(block1_id).collect();
+            let block2_predecessors: Vec<_> = cfg.pred_iter(block2_id).collect();
 
-            let block0_successors = cfg.succ_iter(block0_id).collect::<Vec<_>>();
-            let block1_successors = cfg.succ_iter(block1_id).collect::<Vec<_>>();
-            let block2_successors = cfg.succ_iter(block2_id).collect::<Vec<_>>();
+            let block0_successors: Vec<_> = cfg.succ_iter(block0_id).collect();
+            let block1_successors: Vec<_> = cfg.succ_iter(block1_id).collect();
+            let block2_successors: Vec<_> = cfg.succ_iter(block2_id).collect();
 
             assert_eq!(block0_predecessors.len(), 0);
             assert_eq!(block1_predecessors.len(), 2);
             assert_eq!(block2_predecessors.len(), 2);
 
-            assert_eq!(block1_predecessors.contains(&block0_id), true);
-            assert_eq!(block1_predecessors.contains(&block1_id), true);
-            assert_eq!(block2_predecessors.contains(&block0_id), true);
-            assert_eq!(block2_predecessors.contains(&block1_id), true);
+            assert!(block1_predecessors.contains(&block0_id));
+            assert!(block1_predecessors.contains(&block1_id));
+            assert!(block2_predecessors.contains(&block0_id));
+            assert!(block2_predecessors.contains(&block1_id));
 
             assert_eq!(block0_successors.len(), 2);
             assert_eq!(block1_successors.len(), 2);
             assert_eq!(block2_successors.len(), 0);
 
-            assert_eq!(block0_successors.contains(&block1_id), true);
-            assert_eq!(block0_successors.contains(&block2_id), true);
-            assert_eq!(block1_successors.contains(&block1_id), true);
-            assert_eq!(block1_successors.contains(&block2_id), true);
+            assert!(block0_successors.contains(&block1_id));
+            assert!(block0_successors.contains(&block2_id));
+            assert!(block1_successors.contains(&block1_id));
+            assert!(block1_successors.contains(&block2_id));
         }
 
         // Modify function to form:
         // fn func {
         // block0(cond: u1):
-        //     jmpif cond(), then: block1, else: ret_block
+        //     jmpif cond, then: block1, else: ret_block
         // block1():
-        //     jmpif cond(), then: block1, else: block2
+        //     jmpif cond, then: block1, else: block2
         // block2():
-        //     jmp ret_block
+        //     jmp ret_block()
         // ret_block():
-        //     return
+        //     return ()
         // }
-        let ret_block_id = func.dfg.new_block();
+        let ret_block_id = func.dfg.make_block();
         func.dfg[ret_block_id]
             .set_terminator(TerminatorInstruction::Return { return_values: vec![] });
         func.dfg[block2_id].set_terminator(TerminatorInstruction::Jmp {
@@ -211,41 +212,41 @@ mod tests {
             condition: cond,
             then_destination: block1_id,
             else_destination: ret_block_id,
-            arguments: vec![],
         });
 
         // Recompute new and changed blocks
-        cfg.recompute_block(&mut func, block0_id);
-        cfg.recompute_block(&mut func, block2_id);
-        cfg.recompute_block(&mut func, ret_block_id);
+        cfg.recompute_block(&func, block0_id);
+        cfg.recompute_block(&func, block2_id);
+        cfg.recompute_block(&func, ret_block_id);
 
+        #[allow(clippy::needless_collect)]
         {
-            let block0_predecessors = cfg.pred_iter(block0_id).collect::<Vec<_>>();
-            let block1_predecessors = cfg.pred_iter(block1_id).collect::<Vec<_>>();
-            let block2_predecessors = cfg.pred_iter(block2_id).collect::<Vec<_>>();
+            let block0_predecessors: Vec<_> = cfg.pred_iter(block0_id).collect();
+            let block1_predecessors: Vec<_> = cfg.pred_iter(block1_id).collect();
+            let block2_predecessors: Vec<_> = cfg.pred_iter(block2_id).collect();
 
-            let block0_successors = cfg.succ_iter(block0_id).collect::<Vec<_>>();
-            let block1_successors = cfg.succ_iter(block1_id).collect::<Vec<_>>();
-            let block2_successors = cfg.succ_iter(block2_id).collect::<Vec<_>>();
+            let block0_successors: Vec<_> = cfg.succ_iter(block0_id).collect();
+            let block1_successors: Vec<_> = cfg.succ_iter(block1_id).collect();
+            let block2_successors: Vec<_> = cfg.succ_iter(block2_id).collect();
 
             assert_eq!(block0_predecessors.len(), 0);
             assert_eq!(block1_predecessors.len(), 2);
             assert_eq!(block2_predecessors.len(), 1);
 
-            assert_eq!(block1_predecessors.contains(&block0_id), true);
-            assert_eq!(block1_predecessors.contains(&block1_id), true);
-            assert_eq!(block2_predecessors.contains(&block0_id), false);
-            assert_eq!(block2_predecessors.contains(&block1_id), true);
+            assert!(block1_predecessors.contains(&block0_id));
+            assert!(block1_predecessors.contains(&block1_id));
+            assert!(!block2_predecessors.contains(&block0_id));
+            assert!(block2_predecessors.contains(&block1_id));
 
             assert_eq!(block0_successors.len(), 2);
             assert_eq!(block1_successors.len(), 2);
             assert_eq!(block2_successors.len(), 1);
 
-            assert_eq!(block0_successors.contains(&block1_id), true);
-            assert_eq!(block0_successors.contains(&ret_block_id), true);
-            assert_eq!(block1_successors.contains(&block1_id), true);
-            assert_eq!(block1_successors.contains(&block2_id), true);
-            assert_eq!(block2_successors.contains(&ret_block_id), true);
+            assert!(block0_successors.contains(&block1_id));
+            assert!(block0_successors.contains(&ret_block_id));
+            assert!(block1_successors.contains(&block1_id));
+            assert!(block1_successors.contains(&block2_id));
+            assert!(block2_successors.contains(&ret_block_id));
         }
     }
 }
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/constant.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/constant.rs
index 6d5538d3410..4c793a144da 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/constant.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/constant.rs
@@ -16,8 +16,8 @@ impl NumericConstant {
         Self(value)
     }
 
-    pub(crate) fn value(&self) -> &FieldElement {
-        &self.0
+    pub(crate) fn value(&self) -> FieldElement {
+        self.0
     }
 }
 
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/dfg.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/dfg.rs
index 54ffd5a05f6..ab2018b1df8 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/dfg.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/dfg.rs
@@ -2,7 +2,7 @@ use super::{
     basic_block::{BasicBlock, BasicBlockId},
     constant::{NumericConstant, NumericConstantId},
     function::Signature,
-    instruction::{Instruction, InstructionId, InstructionResultType},
+    instruction::{Instruction, InstructionId, InstructionResultType, TerminatorInstruction},
     map::{DenseMap, Id, SecondaryMap, TwoWayMap},
     types::Type,
     value::{Value, ValueId},
@@ -75,14 +75,14 @@ impl DataFlowGraph {
     /// Creates a new basic block with no parameters.
     /// After being created, the block is unreachable in the current function
     /// until another block is made to jump to it.
-    pub(crate) fn new_block(&mut self) -> BasicBlockId {
+    pub(crate) fn make_block(&mut self) -> BasicBlockId {
         self.blocks.insert(BasicBlock::new(Vec::new()))
     }
 
     /// Creates a new basic block with the given parameters.
     /// After being created, the block is unreachable in the current function
     /// until another block is made to jump to it.
-    pub(crate) fn new_block_with_parameters(
+    pub(crate) fn make_block_with_parameters(
         &mut self,
         parameter_types: impl Iterator<Item = Type>,
     ) -> BasicBlockId {
@@ -126,6 +126,17 @@ impl DataFlowGraph {
         id
     }
 
+    /// Replace an instruction id with another.
+    ///
+    /// This function should generally be avoided if possible in favor of inserting new
+    /// instructions since it does not check whether the instruction results of the removed
+    /// instruction are still in use. Users of this function thus need to ensure the old
+    /// instruction's results are no longer in use or are otherwise compatible with the
+    /// new instruction's result count and types.
+    pub(crate) fn replace_instruction(&mut self, id: Id<Instruction>, instruction: Instruction) {
+        self.instructions[id] = instruction;
+    }
+
     /// Insert a value into the dfg's storage and return an id to reference it.
     /// Until the value is used in an instruction it is unreachable.
     pub(crate) fn make_value(&mut self, value: Value) -> ValueId {
@@ -141,8 +152,11 @@ impl DataFlowGraph {
 
     /// Attaches results to the instruction, clearing any previous results.
     ///
+    /// This does not normally need to be called manually as it is called within
+    /// make_instruction automatically.
+    ///
     /// Returns the results of the instruction
-    fn make_instruction_results(
+    pub(crate) fn make_instruction_results(
         &mut self,
         instruction_id: InstructionId,
         ctrl_typevars: Option<Vec<Type>>,
@@ -230,6 +244,33 @@ impl DataFlowGraph {
     ) {
         self.blocks[block].insert_instruction(instruction);
     }
+
+    /// Returns the field element represented by this value if it is a numeric constant.
+    /// Returns None if the given value is not a numeric constant.
+    pub(crate) fn get_numeric_constant(&self, value: Id<Value>) -> Option<FieldElement> {
+        self.get_numeric_constant_with_type(value).map(|(value, _typ)| value)
+    }
+
+    /// Returns the field element and type represented by this value if it is a numeric constant.
+    /// Returns None if the given value is not a numeric constant.
+    pub(crate) fn get_numeric_constant_with_type(
+        &self,
+        value: Id<Value>,
+    ) -> Option<(FieldElement, Type)> {
+        match self.values[value] {
+            Value::NumericConstant { constant, typ } => Some((self[constant].value(), typ)),
+            _ => None,
+        }
+    }
+
+    /// Sets the terminator instruction for the given basic block
+    pub(crate) fn set_block_terminator(
+        &mut self,
+        block: BasicBlockId,
+        terminator: TerminatorInstruction,
+    ) {
+        self.blocks[block].set_terminator(terminator);
+    }
 }
 
 impl std::ops::Index<InstructionId> for DataFlowGraph {
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/function.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/function.rs
index 63cd31142c4..ca486d0258a 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/function.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/function.rs
@@ -18,10 +18,12 @@ pub(crate) struct Function {
     source_locations: SecondaryMap<Instruction, Location>,
 
     /// The first basic block in the function
-    pub(super) entry_block: BasicBlockId,
+    entry_block: BasicBlockId,
 
     /// Name of the function for debugging only
-    pub(super) name: String,
+    name: String,
+
+    id: FunctionId,
 
     pub(crate) dfg: DataFlowGraph,
 }
@@ -30,10 +32,18 @@ impl Function {
     /// Creates a new function with an automatically inserted entry block.
     ///
     /// Note that any parameters to the function must be manually added later.
-    pub(crate) fn new(name: String) -> Self {
+    pub(crate) fn new(name: String, id: FunctionId) -> Self {
         let mut dfg = DataFlowGraph::default();
-        let entry_block = dfg.new_block();
-        Self { name, source_locations: SecondaryMap::new(), entry_block, dfg }
+        let entry_block = dfg.make_block();
+        Self { name, source_locations: SecondaryMap::new(), id, entry_block, dfg }
+    }
+
+    pub(crate) fn name(&self) -> &str {
+        &self.name
+    }
+
+    pub(crate) fn id(&self) -> FunctionId {
+        self.id
     }
 
     pub(crate) fn entry_block(&self) -> BasicBlockId {
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/instruction.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/instruction.rs
index dcab6e04006..11c6b8dc05f 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/instruction.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/instruction.rs
@@ -150,14 +150,9 @@ pub(crate) enum TerminatorInstruction {
     ///
     /// Jump If
     ///
-    /// If the condition is true: jump to the specified `then_destination` with `arguments`.
-    /// Otherwise, jump to the specified `else_destination` with `arguments`.
-    JmpIf {
-        condition: ValueId,
-        then_destination: BasicBlockId,
-        else_destination: BasicBlockId,
-        arguments: Vec<ValueId>,
-    },
+    /// If the condition is true: jump to the specified `then_destination`.
+    /// Otherwise, jump to the specified `else_destination`.
+    JmpIf { condition: ValueId, then_destination: BasicBlockId, else_destination: BasicBlockId },
 
     /// Unconditional Jump
     ///
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/map.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/map.rs
index 5937b374726..24b30241293 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/map.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/map.rs
@@ -69,9 +69,21 @@ impl<T> std::fmt::Debug for Id<T> {
     }
 }
 
-impl<T> std::fmt::Display for Id<T> {
+impl std::fmt::Display for Id<super::basic_block::BasicBlock> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "${}", self.index)
+        write!(f, "b{}", self.index)
+    }
+}
+
+impl std::fmt::Display for Id<super::value::Value> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "v{}", self.index)
+    }
+}
+
+impl std::fmt::Display for Id<super::function::Function> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "f{}", self.index)
     }
 }
 
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ir/printer.rs b/crates/noirc_evaluator/src/ssa_refactor/ir/printer.rs
index 1a7737e97b0..ff46b49b9b4 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ir/printer.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ir/printer.rs
@@ -1,5 +1,8 @@
 //! This file is for pretty-printing the SSA IR in a human-readable form for debugging.
-use std::fmt::{Formatter, Result};
+use std::{
+    collections::HashSet,
+    fmt::{Formatter, Result},
+};
 
 use iter_extended::vecmap;
 
@@ -11,20 +14,27 @@ use super::{
 };
 
 pub(crate) fn display_function(function: &Function, f: &mut Formatter) -> Result {
-    writeln!(f, "fn {} {{", function.name)?;
-    display_block_with_successors(function, function.entry_block, f)?;
+    writeln!(f, "fn {} {} {{", function.name(), function.id())?;
+    display_block_with_successors(function, function.entry_block(), &mut HashSet::new(), f)?;
     write!(f, "}}")
 }
 
+/// Displays a block followed by all of its successors recursively.
+/// This uses a HashSet to keep track of the visited blocks. Otherwise,
+/// there would be infinite recursion for any loops in the IR.
 pub(crate) fn display_block_with_successors(
     function: &Function,
     block_id: BasicBlockId,
+    visited: &mut HashSet<BasicBlockId>,
     f: &mut Formatter,
 ) -> Result {
     display_block(function, block_id, f)?;
+    visited.insert(block_id);
 
     for successor in function.dfg[block_id].successors() {
-        display_block(function, successor, f)?;
+        if !visited.contains(&successor) {
+            display_block_with_successors(function, successor, visited, f)?;
+        }
     }
     Ok(())
 }
@@ -36,42 +46,46 @@ pub(crate) fn display_block(
 ) -> Result {
     let block = &function.dfg[block_id];
 
-    writeln!(f, "{}({}):", block_id, value_list(block.parameters()))?;
+    writeln!(f, "  {}({}):", block_id, value_list(function, block.parameters()))?;
 
     for instruction in block.instructions() {
         display_instruction(function, *instruction, f)?;
     }
 
-    display_terminator(block.terminator(), f)
+    display_terminator(function, block.terminator(), f)
+}
+
+/// Specialize displaying value ids so that if they refer to constants we
+/// print the constant directly
+fn value(function: &Function, id: ValueId) -> String {
+    match function.dfg.get_numeric_constant_with_type(id) {
+        Some((value, typ)) => format!("{} {}", value, typ),
+        None => id.to_string(),
+    }
 }
 
-fn value_list(values: &[ValueId]) -> String {
-    vecmap(values, ToString::to_string).join(", ")
+fn value_list(function: &Function, values: &[ValueId]) -> String {
+    vecmap(values, |id| value(function, *id)).join(", ")
 }
 
 pub(crate) fn display_terminator(
+    function: &Function,
     terminator: Option<&TerminatorInstruction>,
     f: &mut Formatter,
 ) -> Result {
     match terminator {
         Some(TerminatorInstruction::Jmp { destination, arguments }) => {
-            writeln!(f, "    jmp {}({})", destination, value_list(arguments))
+            writeln!(f, "    jmp {}({})", destination, value_list(function, arguments))
         }
-        Some(TerminatorInstruction::JmpIf {
-            condition,
-            arguments,
-            then_destination,
-            else_destination,
-        }) => {
-            let args = value_list(arguments);
+        Some(TerminatorInstruction::JmpIf { condition, then_destination, else_destination }) => {
             writeln!(
                 f,
-                "    jmpif {}({}) then: {}, else: {}",
-                condition, args, then_destination, else_destination
+                "    jmpif {} then: {}, else: {}",
+                condition, then_destination, else_destination
             )
         }
         Some(TerminatorInstruction::Return { return_values }) => {
-            writeln!(f, "    return {}", value_list(return_values))
+            writeln!(f, "    return {}", value_list(function, return_values))
         }
         None => writeln!(f, "    (no terminator instruction)"),
     }
@@ -87,29 +101,34 @@ pub(crate) fn display_instruction(
 
     let results = function.dfg.instruction_results(instruction);
     if !results.is_empty() {
-        write!(f, "{} = ", value_list(results))?;
+        write!(f, "{} = ", value_list(function, results))?;
     }
 
+    let show = |id| value(function, id);
+
     match &function.dfg[instruction] {
         Instruction::Binary(binary) => {
-            writeln!(f, "{} {}, {}", binary.operator, binary.lhs, binary.rhs)
+            writeln!(f, "{} {}, {}", binary.operator, show(binary.lhs), show(binary.rhs))
         }
-        Instruction::Cast(value, typ) => writeln!(f, "cast {value} as {typ}"),
-        Instruction::Not(value) => writeln!(f, "not {value}"),
+        Instruction::Cast(lhs, typ) => writeln!(f, "cast {} as {typ}", show(*lhs)),
+        Instruction::Not(rhs) => writeln!(f, "not {}", show(*rhs)),
         Instruction::Truncate { value, bit_size, max_bit_size } => {
-            writeln!(f, "truncate {value} to {bit_size} bits, max_bit_size: {max_bit_size}")
+            let value = show(*value);
+            writeln!(f, "truncate {value} to {bit_size} bits, max_bit_size: {max_bit_size}",)
         }
         Instruction::Constrain(value) => {
-            writeln!(f, "constrain {value}")
+            writeln!(f, "constrain {}", show(*value))
         }
         Instruction::Call { func, arguments } => {
-            writeln!(f, "call {func}({})", value_list(arguments))
+            writeln!(f, "call {func}({})", value_list(function, arguments))
         }
         Instruction::Intrinsic { func, arguments } => {
-            writeln!(f, "intrinsic {func}({})", value_list(arguments))
+            writeln!(f, "intrinsic {func}({})", value_list(function, arguments))
         }
         Instruction::Allocate { size } => writeln!(f, "alloc {size} fields"),
-        Instruction::Load { address } => writeln!(f, "load {address}"),
-        Instruction::Store { address, value } => writeln!(f, "store {value} at {address}"),
+        Instruction::Load { address } => writeln!(f, "load {}", show(*address)),
+        Instruction::Store { address, value } => {
+            writeln!(f, "store {} at {}", show(*address), show(*value))
+        }
     }
 }
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/function_builder.rs b/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/function_builder.rs
deleted file mode 100644
index b30ff11c2e1..00000000000
--- a/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/function_builder.rs
+++ /dev/null
@@ -1,122 +0,0 @@
-use acvm::FieldElement;
-
-use crate::ssa_refactor::ir::{
-    basic_block::BasicBlockId,
-    function::{Function, FunctionId},
-    instruction::{Binary, BinaryOp, Instruction},
-    types::Type,
-    value::ValueId,
-};
-
-use super::SharedBuilderContext;
-
-/// The per-function context for each ssa function being generated.
-///
-/// This is split from the global SsaBuilder context to allow each function
-/// to be potentially built concurrently.
-///
-/// Contrary to the name, this struct has the capacity to build as many
-/// functions as needed, although it is limited to one function at a time.
-pub(crate) struct FunctionBuilder<'ssa> {
-    global_context: &'ssa SharedBuilderContext,
-
-    current_function: Function,
-    current_function_id: FunctionId,
-
-    current_block: BasicBlockId,
-
-    finished_functions: Vec<(FunctionId, Function)>,
-}
-
-impl<'ssa> FunctionBuilder<'ssa> {
-    pub(crate) fn new(function_name: String, context: &'ssa SharedBuilderContext) -> Self {
-        let new_function = Function::new(function_name);
-        let current_block = new_function.entry_block();
-
-        Self {
-            global_context: context,
-            current_function: new_function,
-            current_function_id: context.next_function(),
-            current_block,
-            finished_functions: Vec::new(),
-        }
-    }
-
-    /// Finish the current function and create a new function
-    pub(crate) fn new_function(&mut self, name: String) {
-        let new_function = Function::new(name);
-        let old_function = std::mem::replace(&mut self.current_function, new_function);
-
-        self.finished_functions.push((self.current_function_id, old_function));
-        self.current_function_id = self.global_context.next_function();
-    }
-
-    pub(crate) fn finish(mut self) -> Vec<(FunctionId, Function)> {
-        self.finished_functions.push((self.current_function_id, self.current_function));
-        self.finished_functions
-    }
-
-    pub(crate) fn add_parameter(&mut self, typ: Type) -> ValueId {
-        let entry = self.current_function.entry_block();
-        self.current_function.dfg.add_block_parameter(entry, typ)
-    }
-
-    /// Insert a numeric constant into the current function
-    pub(crate) fn numeric_constant(&mut self, value: FieldElement, typ: Type) -> ValueId {
-        self.current_function.dfg.make_constant(value, typ)
-    }
-
-    /// Insert a numeric constant into the current function of type Field
-    pub(crate) fn field_constant(&mut self, value: impl Into<FieldElement>) -> ValueId {
-        self.numeric_constant(value.into(), Type::field())
-    }
-
-    fn insert_instruction(
-        &mut self,
-        instruction: Instruction,
-        ctrl_typevars: Option<Vec<Type>>,
-    ) -> &[ValueId] {
-        let id = self.current_function.dfg.make_instruction(instruction, ctrl_typevars);
-        self.current_function.dfg.insert_instruction_in_block(self.current_block, id);
-        self.current_function.dfg.instruction_results(id)
-    }
-
-    /// Insert an allocate instruction at the end of the current block, allocating the
-    /// given amount of field elements. Returns the result of the allocate instruction,
-    /// which is always a Reference to the allocated data.
-    pub(crate) fn insert_allocate(&mut self, size_to_allocate: u32) -> ValueId {
-        self.insert_instruction(Instruction::Allocate { size: size_to_allocate }, None)[0]
-    }
-
-    /// Insert a Load instruction at the end of the current block, loading from the given address
-    /// which should point to a previous Allocate instruction. Note that this is limited to loading
-    /// a single value. Loading multiple values (such as a tuple) will require multiple loads.
-    /// Returns the element that was loaded.
-    pub(crate) fn insert_load(&mut self, address: ValueId, type_to_load: Type) -> ValueId {
-        self.insert_instruction(Instruction::Load { address }, Some(vec![type_to_load]))[0]
-    }
-
-    /// Insert a Store instruction at the end of the current block, storing the given element
-    /// at the given address. Expects that the address points to a previous Allocate instruction.
-    pub(crate) fn insert_store(&mut self, address: ValueId, value: ValueId) {
-        self.insert_instruction(Instruction::Store { address, value }, None);
-    }
-
-    /// Insert a binary instruction at the end of the current block.
-    /// Returns the result of the binary instruction.
-    pub(crate) fn insert_binary(
-        &mut self,
-        lhs: ValueId,
-        operator: BinaryOp,
-        rhs: ValueId,
-    ) -> ValueId {
-        let instruction = Instruction::Binary(Binary { lhs, rhs, operator });
-        self.insert_instruction(instruction, None)[0]
-    }
-
-    /// Insert a not instruction at the end of the current block.
-    /// Returns the result of the instruction.
-    pub(crate) fn insert_not(&mut self, rhs: ValueId) -> ValueId {
-        self.insert_instruction(Instruction::Not(rhs), None)[0]
-    }
-}
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/mod.rs
index 8f9ceed800e..fdbaa36308b 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/mod.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ssa_builder/mod.rs
@@ -1,19 +1,230 @@
-pub(crate) mod function_builder;
+use acvm::FieldElement;
 
 use crate::ssa_refactor::ir::{
+    basic_block::BasicBlockId,
     function::{Function, FunctionId},
-    map::AtomicCounter,
+    instruction::{Binary, BinaryOp, Instruction, TerminatorInstruction},
+    types::Type,
+    value::{Value, ValueId},
 };
 
-/// The global context while building the ssa representation.
-/// Because this may be shared across threads, it is synchronized internally as necessary.
-#[derive(Default)]
-pub(crate) struct SharedBuilderContext {
-    function_count: AtomicCounter<Function>,
+/// The per-function context for each ssa function being generated.
+///
+/// This is split from the global SsaBuilder context to allow each function
+/// to be potentially built concurrently.
+///
+/// Contrary to the name, this struct has the capacity to build as many
+/// functions as needed, although it is limited to one function at a time.
+pub(crate) struct FunctionBuilder {
+    current_function: Function,
+    current_block: BasicBlockId,
+    finished_functions: Vec<(FunctionId, Function)>,
 }
 
-impl SharedBuilderContext {
-    pub(super) fn next_function(&self) -> FunctionId {
-        self.function_count.next()
+impl FunctionBuilder {
+    pub(crate) fn new(function_name: String, function_id: FunctionId) -> Self {
+        let new_function = Function::new(function_name, function_id);
+        let current_block = new_function.entry_block();
+
+        Self { current_function: new_function, current_block, finished_functions: Vec::new() }
+    }
+
+    /// Finish the current function and create a new function
+    pub(crate) fn new_function(&mut self, name: String, function_id: FunctionId) {
+        let new_function = Function::new(name, function_id);
+        let old_function = std::mem::replace(&mut self.current_function, new_function);
+
+        self.finished_functions.push((self.current_function.id(), old_function));
+    }
+
+    pub(crate) fn finish(mut self) -> Vec<(FunctionId, Function)> {
+        self.finished_functions.push((self.current_function.id(), self.current_function));
+        self.finished_functions
+    }
+
+    pub(crate) fn add_parameter(&mut self, typ: Type) -> ValueId {
+        let entry = self.current_function.entry_block();
+        self.current_function.dfg.add_block_parameter(entry, typ)
+    }
+
+    /// Insert a numeric constant into the current function
+    pub(crate) fn numeric_constant(
+        &mut self,
+        value: impl Into<FieldElement>,
+        typ: Type,
+    ) -> ValueId {
+        self.current_function.dfg.make_constant(value.into(), typ)
+    }
+
+    /// Insert a numeric constant into the current function of type Field
+    pub(crate) fn field_constant(&mut self, value: impl Into<FieldElement>) -> ValueId {
+        self.numeric_constant(value.into(), Type::field())
+    }
+
+    pub(crate) fn type_of_value(&self, value: ValueId) -> Type {
+        self.current_function.dfg.type_of_value(value)
+    }
+
+    pub(crate) fn insert_block(&mut self) -> BasicBlockId {
+        self.current_function.dfg.make_block()
+    }
+
+    pub(crate) fn add_block_parameter(&mut self, block: BasicBlockId, typ: Type) -> ValueId {
+        self.current_function.dfg.add_block_parameter(block, typ)
+    }
+
+    /// Inserts a new instruction at the end of the current block and returns its results
+    fn insert_instruction(
+        &mut self,
+        instruction: Instruction,
+        ctrl_typevars: Option<Vec<Type>>,
+    ) -> &[ValueId] {
+        let id = self.current_function.dfg.make_instruction(instruction, ctrl_typevars);
+        self.current_function.dfg.insert_instruction_in_block(self.current_block, id);
+        self.current_function.dfg.instruction_results(id)
+    }
+
+    /// Switch to inserting instructions in the given block.
+    /// Expects the given block to be within the same function. If you want to insert
+    /// instructions into a new function, call new_function instead.
+    pub(crate) fn switch_to_block(&mut self, block: BasicBlockId) {
+        self.current_block = block;
+    }
+
+    /// Insert an allocate instruction at the end of the current block, allocating the
+    /// given amount of field elements. Returns the result of the allocate instruction,
+    /// which is always a Reference to the allocated data.
+    pub(crate) fn insert_allocate(&mut self, size_to_allocate: u32) -> ValueId {
+        self.insert_instruction(Instruction::Allocate { size: size_to_allocate }, None)[0]
+    }
+
+    /// Insert a Load instruction at the end of the current block, loading from the given offset
+    /// of the given address which should point to a previous Allocate instruction. Note that
+    /// this is limited to loading a single value. Loading multiple values (such as a tuple)
+    /// will require multiple loads.
+    /// 'offset' is in units of FieldElements here. So loading the fourth FieldElement stored in
+    /// an array will have an offset of 3.
+    /// Returns the element that was loaded.
+    pub(crate) fn insert_load(
+        &mut self,
+        mut address: ValueId,
+        offset: ValueId,
+        type_to_load: Type,
+    ) -> ValueId {
+        if let Some(offset) = self.current_function.dfg.get_numeric_constant(offset) {
+            if !offset.is_zero() {
+                let offset = self.field_constant(offset);
+                address = self.insert_binary(address, BinaryOp::Add, offset);
+            }
+        };
+        self.insert_instruction(Instruction::Load { address }, Some(vec![type_to_load]))[0]
+    }
+
+    /// Insert a Store instruction at the end of the current block, storing the given element
+    /// at the given address. Expects that the address points somewhere
+    /// within a previous Allocate instruction.
+    pub(crate) fn insert_store(&mut self, address: ValueId, value: ValueId) {
+        self.insert_instruction(Instruction::Store { address, value }, None);
+    }
+
+    /// Insert a binary instruction at the end of the current block.
+    /// Returns the result of the binary instruction.
+    pub(crate) fn insert_binary(
+        &mut self,
+        lhs: ValueId,
+        operator: BinaryOp,
+        rhs: ValueId,
+    ) -> ValueId {
+        let instruction = Instruction::Binary(Binary { lhs, rhs, operator });
+        self.insert_instruction(instruction, None)[0]
+    }
+
+    /// Insert a not instruction at the end of the current block.
+    /// Returns the result of the instruction.
+    pub(crate) fn insert_not(&mut self, rhs: ValueId) -> ValueId {
+        self.insert_instruction(Instruction::Not(rhs), None)[0]
+    }
+
+    /// Insert a cast instruction at the end of the current block.
+    /// Returns the result of the cast instruction.
+    pub(crate) fn insert_cast(&mut self, value: ValueId, typ: Type) -> ValueId {
+        self.insert_instruction(Instruction::Cast(value, typ), None)[0]
+    }
+
+    /// Insert a constrain instruction at the end of the current block.
+    pub(crate) fn insert_constrain(&mut self, boolean: ValueId) {
+        self.insert_instruction(Instruction::Constrain(boolean), None);
+    }
+
+    /// Insert a call instruction a the end of the current block and return
+    /// the results of the call.
+    pub(crate) fn insert_call(
+        &mut self,
+        func: FunctionId,
+        arguments: Vec<ValueId>,
+        result_types: Vec<Type>,
+    ) -> &[ValueId] {
+        self.insert_instruction(Instruction::Call { func, arguments }, Some(result_types))
+    }
+
+    /// Terminates the current block with the given terminator instruction
+    fn terminate_block_with(&mut self, terminator: TerminatorInstruction) {
+        self.current_function.dfg.set_block_terminator(self.current_block, terminator);
+    }
+
+    /// Terminate the current block with a jmp instruction to jmp to the given
+    /// block with the given arguments.
+    pub(crate) fn terminate_with_jmp(
+        &mut self,
+        destination: BasicBlockId,
+        arguments: Vec<ValueId>,
+    ) {
+        self.terminate_block_with(TerminatorInstruction::Jmp { destination, arguments });
+    }
+
+    /// Terminate the current block with a jmpif instruction to jmp with the given arguments
+    /// block with the given arguments.
+    pub(crate) fn terminate_with_jmpif(
+        &mut self,
+        condition: ValueId,
+        then_destination: BasicBlockId,
+        else_destination: BasicBlockId,
+    ) {
+        self.terminate_block_with(TerminatorInstruction::JmpIf {
+            condition,
+            then_destination,
+            else_destination,
+        });
+    }
+
+    /// Terminate the current block with a return instruction
+    pub(crate) fn terminate_with_return(&mut self, return_values: Vec<ValueId>) {
+        self.terminate_block_with(TerminatorInstruction::Return { return_values });
+    }
+
+    /// Mutates a load instruction into a store instruction.
+    ///
+    /// This function is used while generating ssa-form for assignments currently.
+    /// To re-use most of the expression infrastructure, the lvalue of an assignment
+    /// is compiled as an expression and to assign to it we replace the final load
+    /// (which should always be present to load a mutable value) with a store of the
+    /// assigned value.
+    pub(crate) fn mutate_load_into_store(&mut self, load_result: ValueId, value_to_store: ValueId) {
+        let (instruction, address) = match &self.current_function.dfg[load_result] {
+            Value::Instruction { instruction, .. } => {
+                match &self.current_function.dfg[*instruction] {
+                    Instruction::Load { address } => (*instruction, *address),
+                    other => {
+                        panic!("mutate_load_into_store: Expected Load instruction, found {other:?}")
+                    }
+                }
+            }
+            other => panic!("mutate_load_into_store: Expected Load instruction, found {other:?}"),
+        };
+
+        let store = Instruction::Store { address, value: value_to_store };
+        self.current_function.dfg.replace_instruction(instruction, store);
+        // Clear the results of the previous load for safety
+        self.current_function.dfg.make_instruction_results(instruction, None);
     }
 }
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/context.rs b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/context.rs
index f76a6675077..df5329fed92 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/context.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/context.rs
@@ -6,13 +6,13 @@ use noirc_frontend::monomorphization::ast::{self, LocalId, Parameters};
 use noirc_frontend::monomorphization::ast::{FuncId, Program};
 use noirc_frontend::Signedness;
 
+use crate::ssa_refactor::ir::function::Function;
+use crate::ssa_refactor::ir::function::FunctionId as IrFunctionId;
 use crate::ssa_refactor::ir::instruction::BinaryOp;
+use crate::ssa_refactor::ir::map::AtomicCounter;
 use crate::ssa_refactor::ir::types::Type;
 use crate::ssa_refactor::ir::value::ValueId;
-use crate::ssa_refactor::ssa_builder::SharedBuilderContext;
-use crate::ssa_refactor::{
-    ir::function::FunctionId as IrFunctionId, ssa_builder::function_builder::FunctionBuilder,
-};
+use crate::ssa_refactor::ssa_builder::FunctionBuilder;
 
 use super::value::{Tree, Values};
 
@@ -21,7 +21,8 @@ type FunctionQueue = Vec<(ast::FuncId, IrFunctionId)>;
 
 pub(super) struct FunctionContext<'a> {
     definitions: HashMap<LocalId, Values>,
-    pub(super) builder: FunctionBuilder<'a>,
+
+    pub(super) builder: FunctionBuilder,
     shared_context: &'a SharedContext,
 }
 
@@ -29,28 +30,32 @@ pub(super) struct FunctionContext<'a> {
 pub(super) struct SharedContext {
     functions: RwLock<HashMap<FuncId, IrFunctionId>>,
     function_queue: Mutex<FunctionQueue>,
+    function_counter: AtomicCounter<Function>,
+
     pub(super) program: Program,
 }
 
 impl<'a> FunctionContext<'a> {
     pub(super) fn new(
+        function_id: FuncId,
         function_name: String,
         parameters: &Parameters,
         shared_context: &'a SharedContext,
-        shared_builder_context: &'a SharedBuilderContext,
     ) -> Self {
+        let new_id = shared_context.get_or_queue_function(function_id);
+
         let mut this = Self {
             definitions: HashMap::new(),
-            builder: FunctionBuilder::new(function_name, shared_builder_context),
+            builder: FunctionBuilder::new(function_name, new_id),
             shared_context,
         };
         this.add_parameters_to_scope(parameters);
         this
     }
 
-    pub(super) fn new_function(&mut self, name: String, parameters: &Parameters) {
+    pub(super) fn new_function(&mut self, id: IrFunctionId, name: String, parameters: &Parameters) {
         self.definitions.clear();
-        self.builder.new_function(name);
+        self.builder.new_function(name, id);
         self.add_parameters_to_scope(parameters);
     }
 
@@ -71,7 +76,7 @@ impl<'a> FunctionContext<'a> {
     fn add_parameter_to_scope(&mut self, parameter_id: LocalId, parameter_type: &ast::Type) {
         // Add a separate parameter for each field type in 'parameter_type'
         let parameter_value =
-            self.map_type(parameter_type, |this, typ| this.builder.add_parameter(typ).into());
+            Self::map_type(parameter_type, |typ| self.builder.add_parameter(typ).into());
 
         self.definitions.insert(parameter_id, parameter_value);
     }
@@ -80,12 +85,8 @@ impl<'a> FunctionContext<'a> {
     ///
     /// This can be used to (for example) flatten a tuple type, creating
     /// and returning a new parameter for each field type.
-    pub(super) fn map_type<T>(
-        &mut self,
-        typ: &ast::Type,
-        mut f: impl FnMut(&mut Self, Type) -> T,
-    ) -> Tree<T> {
-        Self::map_type_helper(typ, &mut |typ| f(self, typ))
+    pub(super) fn map_type<T>(typ: &ast::Type, mut f: impl FnMut(Type) -> T) -> Tree<T> {
+        Self::map_type_helper(typ, &mut f)
     }
 
     // This helper is needed because we need to take f by mutable reference,
@@ -129,7 +130,7 @@ impl<'a> FunctionContext<'a> {
     /// Insert a unit constant into the current function if not already
     /// present, and return its value
     pub(super) fn unit_value(&mut self) -> Values {
-        self.builder.numeric_constant(0u128.into(), Type::Unit).into()
+        self.builder.numeric_constant(0u128, Type::Unit).into()
     }
 
     /// Insert a binary instruction at the end of the current block.
@@ -155,6 +156,96 @@ impl<'a> FunctionContext<'a> {
         }
         result.into()
     }
+
+    /// Inserts a call instruction at the end of the current block and returns the results
+    /// of the call.
+    ///
+    /// Compared to self.builder.insert_call, this version will reshape the returned Vec<ValueId>
+    /// back into a Values tree of the proper shape.
+    pub(super) fn insert_call(
+        &mut self,
+        function: IrFunctionId,
+        arguments: Vec<ValueId>,
+        result_type: &ast::Type,
+    ) -> Values {
+        let result_types = Self::convert_type(result_type).flatten();
+        let results = self.builder.insert_call(function, arguments, result_types);
+
+        let mut i = 0;
+        let reshaped_return_values = Self::map_type(result_type, |_| {
+            let result = results[i].into();
+            i += 1;
+            result
+        });
+        assert_eq!(i, results.len());
+        reshaped_return_values
+    }
+
+    /// Create a const offset of an address for an array load or store
+    pub(super) fn make_offset(&mut self, mut address: ValueId, offset: u128) -> ValueId {
+        if offset != 0 {
+            let offset = self.builder.field_constant(offset);
+            address = self.builder.insert_binary(address, BinaryOp::Add, offset);
+        }
+        address
+    }
+
+    /// Define a local variable to be some Values that can later be retrieved
+    /// by calling self.lookup(id)
+    pub(super) fn define(&mut self, id: LocalId, value: Values) {
+        let existing = self.definitions.insert(id, value);
+        assert!(existing.is_none(), "Variable {id:?} was defined twice in ssa-gen pass");
+    }
+
+    /// Looks up the value of a given local variable. Expects the variable to have
+    /// been previously defined or panics otherwise.
+    pub(super) fn lookup(&self, id: LocalId) -> Values {
+        self.definitions.get(&id).expect("lookup: variable not defined").clone()
+    }
+
+    /// Extract the given field of the tuple. Panics if the given Values is not
+    /// a Tree::Branch or does not have enough fields.
+    pub(super) fn get_field(tuple: Values, field_index: usize) -> Values {
+        match tuple {
+            Tree::Branch(mut trees) => trees.remove(field_index),
+            Tree::Leaf(value) => {
+                unreachable!("Tried to extract tuple index {field_index} from non-tuple {value:?}")
+            }
+        }
+    }
+
+    /// Mutate lhs to equal rhs
+    pub(crate) fn assign(&mut self, lhs: Values, rhs: Values) {
+        match (lhs, rhs) {
+            (Tree::Branch(lhs_branches), Tree::Branch(rhs_branches)) => {
+                assert_eq!(lhs_branches.len(), rhs_branches.len());
+
+                for (lhs, rhs) in lhs_branches.into_iter().zip(rhs_branches) {
+                    self.assign(lhs, rhs);
+                }
+            }
+            (Tree::Leaf(lhs), Tree::Leaf(rhs)) => {
+                // Re-evaluating these should have no effect
+                let (lhs, rhs) = (lhs.eval(self), rhs.eval(self));
+
+                // Expect lhs to be previously evaluated. If it is a load we need to undo
+                // the load to get the address to store to.
+                self.builder.mutate_load_into_store(lhs, rhs);
+            }
+            (lhs, rhs) => {
+                unreachable!(
+                    "assign: Expected lhs and rhs values to match but found {lhs:?} and {rhs:?}"
+                )
+            }
+        }
+    }
+
+    /// Retrieves the given function, adding it to the function queue
+    /// if it is not yet compiled.
+    pub(super) fn get_or_queue_function(&self, id: FuncId) -> Values {
+        let function = self.shared_context.get_or_queue_function(id);
+        Values::Leaf(super::value::Value::Function(function))
+    }
 }
 
 /// True if the given operator cannot be encoded directly and needs
@@ -200,10 +291,38 @@ fn convert_operator(op: noirc_frontend::BinaryOpKind) -> BinaryOp {
 
 impl SharedContext {
     pub(super) fn new(program: Program) -> Self {
-        Self { functions: Default::default(), function_queue: Default::default(), program }
+        Self {
+            functions: Default::default(),
+            function_queue: Default::default(),
+            function_counter: Default::default(),
+            program,
+        }
     }
 
     pub(super) fn pop_next_function_in_queue(&self) -> Option<(ast::FuncId, IrFunctionId)> {
         self.function_queue.lock().expect("Failed to lock function_queue").pop()
     }
+
+    /// Return the matching id for the given function if known. If it is not known this
+    /// will add the function to the queue of functions to compile, assign it a new id,
+    /// and return this new id.
+    pub(super) fn get_or_queue_function(&self, id: ast::FuncId) -> IrFunctionId {
+        // Start a new block to guarantee the destructor for the map lock is released
+        // before map needs to be aquired again in self.functions.write() below
+        {
+            let map = self.functions.read().expect("Failed to read self.functions");
+            if let Some(existing_id) = map.get(&id) {
+                return *existing_id;
+            }
+        }
+
+        let next_id = self.function_counter.next();
+
+        let mut queue = self.function_queue.lock().expect("Failed to lock function queue");
+        queue.push((id, next_id));
+
+        self.functions.write().expect("Failed to write to self.functions").insert(id, next_id);
+
+        next_id
+    }
 }
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/mod.rs
index 553b5eb2218..4aad2aafec1 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/mod.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/mod.rs
@@ -1,7 +1,6 @@
 mod context;
 mod value;
 
-use acvm::FieldElement;
 use context::SharedContext;
 use iter_extended::vecmap;
 use noirc_errors::Location;
@@ -12,25 +11,21 @@ use self::{
     value::{Tree, Values},
 };
 
-use super::{
-    ir::{instruction::BinaryOp, types::Type, value::ValueId},
-    ssa_builder::SharedBuilderContext,
-};
+use super::ir::{function::FunctionId, instruction::BinaryOp, types::Type, value::ValueId};
 
 pub(crate) fn generate_ssa(program: Program) {
     let context = SharedContext::new(program);
-    let builder_context = SharedBuilderContext::default();
 
     let main = context.program.main();
-    let mut function_context =
-        FunctionContext::new(main.name.clone(), &main.parameters, &context, &builder_context);
+    let main_id = Program::main_id();
+    let main_name = main.name.clone();
 
+    let mut function_context = FunctionContext::new(main_id, main_name, &main.parameters, &context);
     function_context.codegen_expression(&main.body);
 
-    while let Some((src_function_id, _new_id)) = context.pop_next_function_in_queue() {
+    while let Some((src_function_id, dest_id)) = context.pop_next_function_in_queue() {
         let function = &context.program[src_function_id];
-        // TODO: Need to ensure/assert the new function's id == new_id
-        function_context.new_function(function.name.clone(), &function.parameters);
+        function_context.new_function(dest_id, function.name.clone(), &function.parameters);
         function_context.codegen_expression(&function.body);
     }
 }
@@ -64,16 +59,16 @@ impl<'a> FunctionContext<'a> {
     /// Codegen any non-tuple expression so that we can unwrap the Values
     /// tree to return a single value for use with most SSA instructions.
     fn codegen_non_tuple_expression(&mut self, expr: &Expression) -> ValueId {
-        match self.codegen_expression(expr) {
-            Tree::Branch(branches) => {
-                panic!("codegen_non_tuple_expression called on tuple {branches:?}")
-            }
-            Tree::Leaf(value) => value.eval(),
-        }
+        self.codegen_expression(expr).into_leaf().eval(self)
     }
 
-    fn codegen_ident(&mut self, _ident: &ast::Ident) -> Values {
-        todo!()
+    fn codegen_ident(&mut self, ident: &ast::Ident) -> Values {
+        match &ident.definition {
+            ast::Definition::Local(id) => self.lookup(*id).map(|value| value.eval(self).into()),
+            ast::Definition::Function(id) => self.get_or_queue_function(*id),
+            ast::Definition::Builtin(_) => todo!(),
+            ast::Definition::LowLevel(_) => todo!(),
+        }
     }
 
     fn codegen_literal(&mut self, literal: &ast::Literal) -> Values {
@@ -88,15 +83,11 @@ impl<'a> FunctionContext<'a> {
                 self.builder.numeric_constant(*value, typ).into()
             }
             ast::Literal::Bool(value) => {
-                // Booleans are represented as u1s with 0 = false, 1 = true
-                let typ = Type::unsigned(1);
-                let value = FieldElement::from(*value as u128);
-                self.builder.numeric_constant(value, typ).into()
+                self.builder.numeric_constant(*value as u128, Type::bool()).into()
             }
             ast::Literal::Str(string) => {
                 let elements = vecmap(string.as_bytes(), |byte| {
-                    let value = FieldElement::from(*byte as u128);
-                    self.builder.numeric_constant(value, Type::field()).into()
+                    self.builder.numeric_constant(*byte as u128, Type::field()).into()
                 });
                 self.codegen_array(elements, Tree::Leaf(Type::field()))
             }
@@ -110,16 +101,12 @@ impl<'a> FunctionContext<'a> {
         }));
 
         // Now we must manually store all the elements into the array
-        let mut i = 0;
+        let mut i = 0u128;
         for element in elements {
-            element.for_each(|value| {
-                let address = if i == 0 {
-                    array
-                } else {
-                    let offset = self.builder.field_constant(i as u128);
-                    self.builder.insert_binary(array, BinaryOp::Add, offset)
-                };
-                self.builder.insert_store(address, value.eval());
+            element.for_each(|element| {
+                let address = self.make_offset(array, i);
+                let element = element.eval(self);
+                self.builder.insert_store(address, element);
                 i += 1;
             });
         }
@@ -135,8 +122,16 @@ impl<'a> FunctionContext<'a> {
         result
     }
 
-    fn codegen_unary(&mut self, _unary: &ast::Unary) -> Values {
-        todo!()
+    fn codegen_unary(&mut self, unary: &ast::Unary) -> Values {
+        let rhs = self.codegen_non_tuple_expression(&unary.rhs);
+        match unary.operator {
+            noirc_frontend::UnaryOp::Not => self.builder.insert_not(rhs).into(),
+            noirc_frontend::UnaryOp::Minus => {
+                let typ = self.builder.type_of_value(rhs);
+                let zero = self.builder.numeric_constant(0u128, typ);
+                self.builder.insert_binary(zero, BinaryOp::Sub, rhs).into()
+            }
+        }
     }
 
     fn codegen_binary(&mut self, binary: &ast::Binary) -> Values {
@@ -145,49 +140,185 @@ impl<'a> FunctionContext<'a> {
         self.insert_binary(lhs, binary.operator, rhs)
     }
 
-    fn codegen_index(&mut self, _index: &ast::Index) -> Values {
-        todo!()
+    fn codegen_index(&mut self, index: &ast::Index) -> Values {
+        let array = self.codegen_non_tuple_expression(&index.collection);
+        self.codegen_array_index(array, &index.index, &index.element_type)
     }
 
-    fn codegen_cast(&mut self, _cast: &ast::Cast) -> Values {
-        todo!()
+    /// This is broken off from codegen_index so that it can also be
+    /// used to codegen a LValue::Index
+    fn codegen_array_index(
+        &mut self,
+        array: super::ir::value::ValueId,
+        index: &ast::Expression,
+        element_type: &ast::Type,
+    ) -> Values {
+        let base_offset = self.codegen_non_tuple_expression(index);
+
+        // base_index = base_offset * type_size
+        let type_size = Self::convert_type(element_type).size_of_type();
+        let type_size = self.builder.field_constant(type_size as u128);
+        let base_index = self.builder.insert_binary(base_offset, BinaryOp::Mul, type_size);
+
+        let mut field_index = 0u128;
+        Self::map_type(element_type, |typ| {
+            let offset = self.make_offset(base_index, field_index);
+            field_index += 1;
+            self.builder.insert_load(array, offset, typ).into()
+        })
     }
 
-    fn codegen_for(&mut self, _for_expr: &ast::For) -> Values {
-        todo!()
+    fn codegen_cast(&mut self, cast: &ast::Cast) -> Values {
+        let lhs = self.codegen_non_tuple_expression(&cast.lhs);
+        let typ = Self::convert_non_tuple_type(&cast.r#type);
+        self.builder.insert_cast(lhs, typ).into()
     }
 
-    fn codegen_if(&mut self, _if_expr: &ast::If) -> Values {
-        todo!()
+    fn codegen_for(&mut self, for_expr: &ast::For) -> Values {
+        let loop_entry = self.builder.insert_block();
+        let loop_body = self.builder.insert_block();
+        let loop_end = self.builder.insert_block();
+
+        // this is the 'i' in `for i in start .. end { block }`
+        let loop_index = self.builder.add_block_parameter(loop_entry, Type::field());
+
+        let start_index = self.codegen_non_tuple_expression(&for_expr.start_range);
+        let end_index = self.codegen_non_tuple_expression(&for_expr.end_range);
+
+        self.builder.terminate_with_jmp(loop_entry, vec![start_index]);
+
+        // Compile the loop entry block
+        self.builder.switch_to_block(loop_entry);
+        let jump_condition = self.builder.insert_binary(loop_index, BinaryOp::Lt, end_index);
+        self.builder.terminate_with_jmpif(jump_condition, loop_body, loop_end);
+
+        // Compile the loop body
+        self.builder.switch_to_block(loop_body);
+        self.define(for_expr.index_variable, loop_index.into());
+        self.codegen_expression(&for_expr.block);
+        let new_loop_index = self.make_offset(loop_index, 1);
+        self.builder.terminate_with_jmp(loop_entry, vec![new_loop_index]);
+
+        // Finish by switching back to the end of the loop
+        self.builder.switch_to_block(loop_end);
+        self.unit_value()
+    }
+
+    fn codegen_if(&mut self, if_expr: &ast::If) -> Values {
+        let condition = self.codegen_non_tuple_expression(&if_expr.condition);
+
+        let then_block = self.builder.insert_block();
+        let else_block = self.builder.insert_block();
+
+        self.builder.terminate_with_jmpif(condition, then_block, else_block);
+
+        self.builder.switch_to_block(then_block);
+        let then_value = self.codegen_expression(&if_expr.consequence);
+
+        let mut result = self.unit_value();
+
+        if let Some(alternative) = &if_expr.alternative {
+            self.builder.switch_to_block(else_block);
+            let else_value = self.codegen_expression(alternative);
+
+            let end_block = self.builder.insert_block();
+
+            // Create block arguments for the end block as needed to branch to
+            // with our then and else value.
+            result = Self::map_type(&if_expr.typ, |typ| {
+                self.builder.add_block_parameter(end_block, typ).into()
+            });
+
+            let else_values = else_value.into_value_list(self);
+            self.builder.terminate_with_jmp(end_block, else_values);
+
+            // Must also set the then block to jmp to the end now
+            self.builder.switch_to_block(then_block);
+            let then_values = then_value.into_value_list(self);
+            self.builder.terminate_with_jmp(end_block, then_values);
+            self.builder.switch_to_block(end_block);
+        } else {
+            // In the case we have no 'else', the 'else' block is actually the end block.
+            self.builder.terminate_with_jmp(else_block, vec![]);
+            self.builder.switch_to_block(else_block);
+        }
+
+        result
     }
 
     fn codegen_tuple(&mut self, tuple: &[Expression]) -> Values {
         Tree::Branch(vecmap(tuple, |expr| self.codegen_expression(expr)))
     }
 
-    fn codegen_extract_tuple_field(&mut self, tuple: &Expression, index: usize) -> Values {
-        match self.codegen_expression(tuple) {
-            Tree::Branch(mut trees) => trees.remove(index),
-            Tree::Leaf(value) => {
-                unreachable!("Tried to extract tuple index {index} from non-tuple {value:?}")
+    fn codegen_extract_tuple_field(&mut self, tuple: &Expression, field_index: usize) -> Values {
+        let tuple = self.codegen_expression(tuple);
+        Self::get_field(tuple, field_index)
+    }
+
+    fn codegen_function(&mut self, function: &Expression) -> FunctionId {
+        use crate::ssa_refactor::ssa_gen::value::Value;
+        match self.codegen_expression(function) {
+            Tree::Leaf(Value::Function(id)) => id,
+            other => {
+                panic!("codegen_function: expected function value, found {other:?}")
             }
         }
     }
 
-    fn codegen_call(&mut self, _call: &ast::Call) -> Values {
-        todo!()
+    fn codegen_call(&mut self, call: &ast::Call) -> Values {
+        let function = self.codegen_function(&call.func);
+
+        let arguments = call
+            .arguments
+            .iter()
+            .flat_map(|argument| self.codegen_expression(argument).into_value_list(self))
+            .collect();
+
+        self.insert_call(function, arguments, &call.return_type)
     }
 
-    fn codegen_let(&mut self, _let_expr: &ast::Let) -> Values {
-        todo!()
+    fn codegen_let(&mut self, let_expr: &ast::Let) -> Values {
+        let mut values = self.codegen_expression(&let_expr.expression);
+
+        if let_expr.mutable {
+            values.map_mut(|value| {
+                let value = value.eval(self);
+                // Size is always 1 here since we're recursively unpacking tuples
+                let alloc = self.builder.insert_allocate(1);
+                self.builder.insert_store(alloc, value);
+                alloc.into()
+            });
+        }
+
+        self.define(let_expr.id, values);
+        self.unit_value()
     }
 
-    fn codegen_constrain(&mut self, _constrain: &Expression, _location: Location) -> Values {
-        todo!()
+    fn codegen_constrain(&mut self, expr: &Expression, _location: Location) -> Values {
+        let boolean = self.codegen_non_tuple_expression(expr);
+        self.builder.insert_constrain(boolean);
+        self.unit_value()
     }
 
-    fn codegen_assign(&mut self, _assign: &ast::Assign) -> Values {
-        todo!()
+    fn codegen_assign(&mut self, assign: &ast::Assign) -> Values {
+        let lhs = self.codegen_lvalue(&assign.lvalue);
+        let rhs = self.codegen_expression(&assign.expression);
+        self.assign(lhs, rhs);
+        self.unit_value()
+    }
+
+    fn codegen_lvalue(&mut self, lvalue: &ast::LValue) -> Values {
+        match lvalue {
+            ast::LValue::Ident(ident) => self.codegen_ident(ident),
+            ast::LValue::Index { array, index, element_type, location: _ } => {
+                let array = self.codegen_lvalue(array).into_leaf().eval(self);
+                self.codegen_array_index(array, index, element_type)
+            }
+            ast::LValue::MemberAccess { object, field_index } => {
+                let object = self.codegen_lvalue(object);
+                Self::get_field(object, *field_index)
+            }
+        }
     }
 
     fn codegen_semi(&mut self, expr: &Expression) -> Values {
diff --git a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/value.rs b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/value.rs
index 83a5d15c904..52ff52d75f2 100644
--- a/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/value.rs
+++ b/crates/noirc_evaluator/src/ssa_refactor/ssa_gen/value.rs
@@ -1,26 +1,37 @@
+use iter_extended::vecmap;
+
 use crate::ssa_refactor::ir::function::FunctionId as IrFunctionId;
 use crate::ssa_refactor::ir::types::Type;
 use crate::ssa_refactor::ir::value::ValueId as IrValueId;
 
-#[derive(Debug)]
+use super::context::FunctionContext;
+
+#[derive(Debug, Clone)]
 pub(super) enum Tree<T> {
     Branch(Vec<Tree<T>>),
     Leaf(T),
 }
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Copy, Clone)]
 pub(super) enum Value {
     Normal(IrValueId),
     Function(IrFunctionId),
+
+    /// A mutable variable that must be loaded as the given type before being used
+    Mutable(IrValueId, Type),
 }
 
 impl Value {
     /// Evaluate a value, returning an IrValue from it.
-    /// This has no effect on Value::Normal, but any variables will be updated with their latest
-    /// use.
-    pub(super) fn eval(self) -> IrValueId {
+    /// This has no effect on Value::Normal, but any variables will
+    /// need to be loaded from memory
+    pub(super) fn eval(self, ctx: &mut FunctionContext) -> IrValueId {
         match self {
             Value::Normal(value) => value,
+            Value::Mutable(address, typ) => {
+                let offset = ctx.builder.field_constant(0u128);
+                ctx.builder.insert_load(address, offset, typ)
+            }
             Value::Function(_) => panic!("Tried to evaluate a function value"),
         }
     }
@@ -54,6 +65,37 @@ impl<T> Tree<T> {
             Tree::Leaf(value) => f(value),
         }
     }
+
+    pub(super) fn map_mut(&mut self, mut f: impl FnMut(&T) -> Tree<T>) {
+        self.map_mut_helper(&mut f);
+    }
+
+    fn map_mut_helper(&mut self, f: &mut impl FnMut(&T) -> Tree<T>) {
+        match self {
+            Tree::Branch(trees) => trees.iter_mut().for_each(|tree| tree.map_mut_helper(f)),
+            Tree::Leaf(value) => *self = f(value),
+        }
+    }
+
+    pub(super) fn map<U>(self, mut f: impl FnMut(T) -> Tree<U>) -> Tree<U> {
+        self.map_helper(&mut f)
+    }
+
+    fn map_helper<U>(self, f: &mut impl FnMut(T) -> Tree<U>) -> Tree<U> {
+        match self {
+            Tree::Branch(trees) => Tree::Branch(vecmap(trees, |tree| tree.map_helper(f))),
+            Tree::Leaf(value) => f(value),
+        }
+    }
+
+    /// Unwraps this Tree into the value of the leaf node. Panics if
+    /// this Tree is a Branch
+    pub(super) fn into_leaf(self) -> T {
+        match self {
+            Tree::Branch(_) => panic!("into_leaf called on a Tree::Branch"),
+            Tree::Leaf(value) => value,
+        }
+    }
 }
 
 impl From<IrValueId> for Values {
@@ -76,3 +118,11 @@ impl Tree<Type> {
         self.count_leaves()
     }
 }
+
+impl Tree<Value> {
+    /// Flattens and evaluates this Tree<Value> into a list of ir values
+    /// for return statements, branching instructions, or function parameters.
+    pub(super) fn into_value_list(self, ctx: &mut FunctionContext) -> Vec<IrValueId> {
+        vecmap(self.flatten(), |value| value.eval(ctx))
+    }
+}
diff --git a/crates/noirc_frontend/src/ast/expression.rs b/crates/noirc_frontend/src/ast/expression.rs
index ac6161ddac1..9be6f715a14 100644
--- a/crates/noirc_frontend/src/ast/expression.rs
+++ b/crates/noirc_frontend/src/ast/expression.rs
@@ -325,6 +325,7 @@ pub struct FunctionDefinition {
     pub span: Span,
     pub return_type: UnresolvedType,
     pub return_visibility: noirc_abi::AbiVisibility,
+    pub return_distinctness: noirc_abi::AbiDistinctness,
 }
 
 /// Describes the types of smart contract functions that are allowed.
diff --git a/crates/noirc_frontend/src/hir/def_map/mod.rs b/crates/noirc_frontend/src/hir/def_map/mod.rs
index 25e0488a7b6..fdaf2dd3acc 100644
--- a/crates/noirc_frontend/src/hir/def_map/mod.rs
+++ b/crates/noirc_frontend/src/hir/def_map/mod.rs
@@ -18,6 +18,9 @@ pub use module_data::*;
 mod namespace;
 pub use namespace::*;
 
+/// The name that is used for a non-contract program's entry-point function.
+pub const MAIN_FUNCTION: &str = "main";
+
 // XXX: Ultimately, we want to constrain an index to be of a certain type just like in RA
 /// Lets first check if this is offered by any external crate
 /// XXX: RA has made this a crate on crates.io
@@ -104,8 +107,6 @@ impl CrateDefMap {
 
     /// Find the main function for this crate
     pub fn main_function(&self) -> Option<FuncId> {
-        const MAIN_FUNCTION: &str = "main";
-
         let root_module = &self.modules()[self.root.0];
 
         // This function accepts an Ident, so we attach a dummy span to
diff --git a/crates/noirc_frontend/src/hir/resolution/errors.rs b/crates/noirc_frontend/src/hir/resolution/errors.rs
index 9406474a226..c57e4c890d2 100644
--- a/crates/noirc_frontend/src/hir/resolution/errors.rs
+++ b/crates/noirc_frontend/src/hir/resolution/errors.rs
@@ -32,6 +32,8 @@ pub enum ResolverError {
     UnnecessaryPub { ident: Ident },
     #[error("Required 'pub', main function must return public value")]
     NecessaryPub { ident: Ident },
+    #[error("'distinct' keyword can only be used with main method")]
+    DistinctNotAllowed { ident: Ident },
     #[error("Expected const value where non-constant value was used")]
     ExpectedComptimeVariable { name: String, span: Span },
     #[error("Missing expression for declared constant")]
@@ -176,6 +178,18 @@ impl From<ResolverError> for Diagnostic {
                 diag.add_note("The `pub` keyword is mandatory for the entry-point function return type because the verifier cannot retrieve private witness and thus the function will not be able to return a 'priv' value".to_owned());
                 diag
             }
+            ResolverError::DistinctNotAllowed { ident } => {
+                let name = &ident.0.contents;
+
+                let mut diag = Diagnostic::simple_error(
+                    format!("Invalid `distinct` keyword on return type of function {name}"),
+                    "Invalid distinct on return type".to_string(),
+                    ident.0.span(),
+                );
+
+                diag.add_note("The `distinct` keyword is only valid when used on the main function of a program, as its only purpose is to ensure that all witness indices that occur in the abi are unique".to_owned());
+                diag
+            }
             ResolverError::ExpectedComptimeVariable { name, span } => Diagnostic::simple_error(
                 format!("expected constant variable where non-constant variable {name} was used"),
                 "expected const variable".to_string(),
diff --git a/crates/noirc_frontend/src/hir/resolution/resolver.rs b/crates/noirc_frontend/src/hir/resolution/resolver.rs
index cfb354498ab..98cf5993edf 100644
--- a/crates/noirc_frontend/src/hir/resolution/resolver.rs
+++ b/crates/noirc_frontend/src/hir/resolution/resolver.rs
@@ -22,7 +22,7 @@ use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::rc::Rc;
 
 use crate::graph::CrateId;
-use crate::hir::def_map::{ModuleDefId, TryFromModuleDefId};
+use crate::hir::def_map::{ModuleDefId, TryFromModuleDefId, MAIN_FUNCTION};
 use crate::hir_def::stmt::{HirAssignStatement, HirLValue, HirPattern};
 use crate::node_interner::{
     DefinitionId, DefinitionKind, ExprId, FuncId, NodeInterner, StmtId, StructId,
@@ -637,6 +637,12 @@ impl<'a> Resolver<'a> {
             self.push_err(ResolverError::NecessaryPub { ident: func.name_ident().clone() });
         }
 
+        if !self.distinct_allowed(func)
+            && func.def.return_distinctness != noirc_abi::AbiDistinctness::DuplicationAllowed
+        {
+            self.push_err(ResolverError::DistinctNotAllowed { ident: func.name_ident().clone() });
+        }
+
         if attributes == Some(Attribute::Test) && !parameters.is_empty() {
             self.push_err(ResolverError::TestFunctionHasParameters {
                 span: func.name_ident().span(),
@@ -661,6 +667,7 @@ impl<'a> Resolver<'a> {
             typ,
             parameters: parameters.into(),
             return_visibility: func.def.return_visibility,
+            return_distinctness: func.def.return_distinctness,
             has_body: !func.def.body.is_empty(),
         }
     }
@@ -670,7 +677,18 @@ impl<'a> Resolver<'a> {
         if self.in_contract() {
             !func.def.is_unconstrained && !func.def.is_open
         } else {
-            func.name() == "main"
+            func.name() == MAIN_FUNCTION
+        }
+    }
+
+    /// True if the `distinct` keyword is allowed on a function's return type
+    fn distinct_allowed(&self, func: &NoirFunction) -> bool {
+        if self.in_contract() {
+            // "open" and "unconstrained" functions are compiled to brillig and thus duplication of
+            // witness indices in their abis is not a concern.
+            !func.def.is_unconstrained && !func.def.is_open
+        } else {
+            func.name() == MAIN_FUNCTION
         }
     }
 
diff --git a/crates/noirc_frontend/src/hir/type_check/mod.rs b/crates/noirc_frontend/src/hir/type_check/mod.rs
index 97b1c71a0bc..5ebac6de9a3 100644
--- a/crates/noirc_frontend/src/hir/type_check/mod.rs
+++ b/crates/noirc_frontend/src/hir/type_check/mod.rs
@@ -219,6 +219,7 @@ mod test {
             ]
             .into(),
             return_visibility: noirc_abi::AbiVisibility::Private,
+            return_distinctness: noirc_abi::AbiDistinctness::DuplicationAllowed,
             has_body: true,
         };
         interner.push_fn_meta(func_meta, func_id);
diff --git a/crates/noirc_frontend/src/hir_def/function.rs b/crates/noirc_frontend/src/hir_def/function.rs
index a9fafffe159..1f7399e5547 100644
--- a/crates/noirc_frontend/src/hir_def/function.rs
+++ b/crates/noirc_frontend/src/hir_def/function.rs
@@ -1,5 +1,5 @@
 use iter_extended::vecmap;
-use noirc_abi::{AbiParameter, AbiType, AbiVisibility};
+use noirc_abi::{AbiDistinctness, AbiParameter, AbiType, AbiVisibility};
 use noirc_errors::{Location, Span};
 
 use super::expr::{HirBlockExpression, HirExpression, HirIdent};
@@ -131,6 +131,8 @@ pub struct FuncMeta {
 
     pub return_visibility: AbiVisibility,
 
+    pub return_distinctness: AbiDistinctness,
+
     /// The type of this function. Either a Type::Function
     /// or a Type::Forall for generic functions.
     pub typ: Type,
diff --git a/crates/noirc_frontend/src/lexer/lexer.rs b/crates/noirc_frontend/src/lexer/lexer.rs
index c1ff328a3ed..5e0d99cfed9 100644
--- a/crates/noirc_frontend/src/lexer/lexer.rs
+++ b/crates/noirc_frontend/src/lexer/lexer.rs
@@ -560,6 +560,7 @@ fn test_basic_language_syntax() {
             x * y;
         };
         constrain mul(five, ten) == 50;
+        assert(ten + five == 15);
     ";
 
     let expected = vec![
@@ -601,6 +602,15 @@ fn test_basic_language_syntax() {
         Token::Equal,
         Token::Int(50_i128.into()),
         Token::Semicolon,
+        Token::Keyword(Keyword::Assert),
+        Token::LeftParen,
+        Token::Ident("ten".to_string()),
+        Token::Plus,
+        Token::Ident("five".to_string()),
+        Token::Equal,
+        Token::Int(15_i128.into()),
+        Token::RightParen,
+        Token::Semicolon,
         Token::EOF,
     ];
     let mut lexer = Lexer::new(input);
diff --git a/crates/noirc_frontend/src/lexer/token.rs b/crates/noirc_frontend/src/lexer/token.rs
index 0df1fc39938..bfcd0f4be51 100644
--- a/crates/noirc_frontend/src/lexer/token.rs
+++ b/crates/noirc_frontend/src/lexer/token.rs
@@ -414,6 +414,7 @@ impl AsRef<str> for Attribute {
 #[cfg_attr(test, derive(strum_macros::EnumIter))]
 pub enum Keyword {
     As,
+    Assert,
     Bool,
     Char,
     CompTime,
@@ -421,6 +422,7 @@ pub enum Keyword {
     Contract,
     Crate,
     Dep,
+    Distinct,
     Else,
     Field,
     Fn,
@@ -447,6 +449,7 @@ impl fmt::Display for Keyword {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match *self {
             Keyword::As => write!(f, "as"),
+            Keyword::Assert => write!(f, "assert"),
             Keyword::Bool => write!(f, "bool"),
             Keyword::Char => write!(f, "char"),
             Keyword::CompTime => write!(f, "comptime"),
@@ -454,6 +457,7 @@ impl fmt::Display for Keyword {
             Keyword::Contract => write!(f, "contract"),
             Keyword::Crate => write!(f, "crate"),
             Keyword::Dep => write!(f, "dep"),
+            Keyword::Distinct => write!(f, "distinct"),
             Keyword::Else => write!(f, "else"),
             Keyword::Field => write!(f, "Field"),
             Keyword::Fn => write!(f, "fn"),
@@ -483,6 +487,7 @@ impl Keyword {
     pub(crate) fn lookup_keyword(word: &str) -> Option<Token> {
         let keyword = match word {
             "as" => Keyword::As,
+            "assert" => Keyword::Assert,
             "bool" => Keyword::Bool,
             "char" => Keyword::Char,
             "comptime" => Keyword::CompTime,
@@ -490,6 +495,7 @@ impl Keyword {
             "contract" => Keyword::Contract,
             "crate" => Keyword::Crate,
             "dep" => Keyword::Dep,
+            "distinct" => Keyword::Distinct,
             "else" => Keyword::Else,
             "Field" => Keyword::Field,
             "fn" => Keyword::Fn,
diff --git a/crates/noirc_frontend/src/monomorphization/ast.rs b/crates/noirc_frontend/src/monomorphization/ast.rs
index e4339c8e367..bad88885749 100644
--- a/crates/noirc_frontend/src/monomorphization/ast.rs
+++ b/crates/noirc_frontend/src/monomorphization/ast.rs
@@ -131,6 +131,7 @@ pub struct Call {
 pub struct Index {
     pub collection: Box<Expression>,
     pub index: Box<Expression>,
+    pub element_type: Type,
     pub location: Location,
 }
 
@@ -221,11 +222,20 @@ impl Type {
 pub struct Program {
     pub functions: Vec<Function>,
     pub main_function_signature: FunctionSignature,
+    /// Indicates whether witness indices are allowed to reoccur in the ABI of the resulting ACIR.
+    ///
+    /// Note: this has no impact on monomorphization, and is simply attached here for ease of
+    /// forwarding to the next phase.
+    pub return_distinctness: noirc_abi::AbiDistinctness,
 }
 
 impl Program {
-    pub fn new(functions: Vec<Function>, main_function_signature: FunctionSignature) -> Program {
-        Program { functions, main_function_signature }
+    pub fn new(
+        functions: Vec<Function>,
+        main_function_signature: FunctionSignature,
+        return_distinctness: noirc_abi::AbiDistinctness,
+    ) -> Program {
+        Program { functions, main_function_signature, return_distinctness }
     }
 
     pub fn main(&self) -> &Function {
diff --git a/crates/noirc_frontend/src/monomorphization/mod.rs b/crates/noirc_frontend/src/monomorphization/mod.rs
index bfce292d2eb..3c3c602d132 100644
--- a/crates/noirc_frontend/src/monomorphization/mod.rs
+++ b/crates/noirc_frontend/src/monomorphization/mod.rs
@@ -17,7 +17,7 @@ use std::collections::{BTreeMap, HashMap, VecDeque};
 use crate::{
     hir_def::{
         expr::*,
-        function::{Param, Parameters},
+        function::{FuncMeta, Param, Parameters},
         stmt::{HirAssignStatement, HirLValue, HirLetStatement, HirPattern, HirStatement},
     },
     node_interner::{self, DefinitionKind, NodeInterner, StmtId},
@@ -88,7 +88,8 @@ pub fn monomorphize(main: node_interner::FuncId, interner: &NodeInterner) -> Pro
     }
 
     let functions = vecmap(monomorphizer.finished_functions, |(_, f)| f);
-    Program::new(functions, function_sig)
+    let FuncMeta { return_distinctness, .. } = interner.function_meta(&main);
+    Program::new(functions, function_sig, return_distinctness)
 }
 
 impl<'interner> Monomorphizer<'interner> {
@@ -411,7 +412,7 @@ impl<'interner> Monomorphizer<'interner> {
             | ast::Type::Bool
             | ast::Type::Unit
             | ast::Type::Function(_, _) => {
-                ast::Expression::Index(ast::Index { collection, index, location })
+                ast::Expression::Index(ast::Index { collection, index, element_type, location })
             }
 
             ast::Type::Tuple(elements) => {
diff --git a/crates/noirc_frontend/src/parser/parser.rs b/crates/noirc_frontend/src/parser/parser.rs
index f4793d06368..575a9403ea8 100644
--- a/crates/noirc_frontend/src/parser/parser.rs
+++ b/crates/noirc_frontend/src/parser/parser.rs
@@ -40,7 +40,7 @@ use crate::{
 
 use chumsky::prelude::*;
 use iter_extended::vecmap;
-use noirc_abi::AbiVisibility;
+use noirc_abi::{AbiDistinctness, AbiVisibility};
 use noirc_errors::{CustomDiagnostic, Span, Spanned};
 
 /// Entry function for the parser - also handles lexing internally.
@@ -162,7 +162,7 @@ fn function_definition(allow_self: bool) -> impl NoirParser<NoirFunction> {
             |(
                 (
                     ((((attribute, (is_unconstrained, is_open)), name), generics), parameters),
-                    (return_visibility, return_type),
+                    ((return_distinctness, return_visibility), return_type),
                 ),
                 body,
             )| {
@@ -177,6 +177,7 @@ fn function_definition(allow_self: bool) -> impl NoirParser<NoirFunction> {
                     body,
                     return_type,
                     return_visibility,
+                    return_distinctness,
                 }
                 .into()
             },
@@ -235,12 +236,18 @@ fn lambda_return_type() -> impl NoirParser<UnresolvedType> {
         .map(|ret| ret.unwrap_or(UnresolvedType::Unspecified))
 }
 
-fn function_return_type() -> impl NoirParser<(AbiVisibility, UnresolvedType)> {
+fn function_return_type() -> impl NoirParser<((AbiDistinctness, AbiVisibility), UnresolvedType)> {
     just(Token::Arrow)
-        .ignore_then(optional_visibility())
+        .ignore_then(optional_distinctness())
+        .then(optional_visibility())
         .then(parse_type())
         .or_not()
-        .map(|ret| ret.unwrap_or((AbiVisibility::Private, UnresolvedType::Unit)))
+        .map(|ret| {
+            ret.unwrap_or((
+                (AbiDistinctness::DuplicationAllowed, AbiVisibility::Private),
+                UnresolvedType::Unit,
+            ))
+        })
 }
 
 fn attribute() -> impl NoirParser<Attribute> {
@@ -428,6 +435,7 @@ where
 {
     choice((
         constrain(expr_parser.clone()),
+        assertion(expr_parser.clone()),
         declaration(expr_parser.clone()),
         assignment(expr_parser.clone()),
         expr_parser.map(Statement::Expression),
@@ -442,6 +450,15 @@ where
         .map(|expr| Statement::Constrain(ConstrainStatement(expr)))
 }
 
+fn assertion<'a, P>(expr_parser: P) -> impl NoirParser<Statement> + 'a
+where
+    P: ExprParser + 'a,
+{
+    ignore_then_commit(keyword(Keyword::Assert), parenthesized(expr_parser))
+        .labelled("statement")
+        .map(|expr| Statement::Constrain(ConstrainStatement(expr)))
+}
+
 fn declaration<'a, P>(expr_parser: P) -> impl NoirParser<Statement> + 'a
 where
     P: ExprParser + 'a,
@@ -554,6 +571,13 @@ fn optional_visibility() -> impl NoirParser<AbiVisibility> {
     })
 }
 
+fn optional_distinctness() -> impl NoirParser<AbiDistinctness> {
+    keyword(Keyword::Distinct).or_not().map(|opt| match opt {
+        Some(_) => AbiDistinctness::Distinct,
+        None => AbiDistinctness::DuplicationAllowed,
+    })
+}
+
 fn maybe_comp_time() -> impl NoirParser<CompTime> {
     keyword(Keyword::CompTime).or_not().map(|opt| match opt {
         Some(_) => CompTime::Yes(None),
@@ -1214,6 +1238,47 @@ mod test {
         );
     }
 
+    #[test]
+    fn parse_assert() {
+        parse_with(assertion(expression()), "assert(x == y)").unwrap();
+
+        // Currently we disallow constrain statements where the outer infix operator
+        // produces a value. This would require an implicit `==` which
+        // may not be intuitive to the user.
+        //
+        // If this is deemed useful, one would either apply a transformation
+        // or interpret it with an `==` in the evaluator
+        let disallowed_operators = vec![
+            BinaryOpKind::And,
+            BinaryOpKind::Subtract,
+            BinaryOpKind::Divide,
+            BinaryOpKind::Multiply,
+            BinaryOpKind::Or,
+        ];
+
+        for operator in disallowed_operators {
+            let src = format!("assert(x {} y);", operator.as_string());
+            parse_with(assertion(expression()), &src).unwrap_err();
+        }
+
+        // These are general cases which should always work.
+        //
+        // The first case is the most noteworthy. It contains two `==`
+        // The first (inner) `==` is a predicate which returns 0/1
+        // The outer layer is an infix `==` which is
+        // associated with the Constrain statement
+        parse_all(
+            assertion(expression()),
+            vec![
+                "assert(((x + y) == k) + z == y)",
+                "assert((x + !y) == y)",
+                "assert((x ^ y) == y)",
+                "assert((x ^ y) == (y + m))",
+                "assert(x + x ^ x == y | m)",
+            ],
+        );
+    }
+
     #[test]
     fn parse_let() {
         // Why is it valid to specify a let declaration as having type u8?
@@ -1257,6 +1322,7 @@ mod test {
                 "fn f(f: pub Field, y : Field, z : comptime Field) -> u8 { x + a }",
                 "fn func_name(f: Field, y : pub Field, z : pub [u8;5],) {}",
                 "fn func_name(x: [Field], y : [Field;2],y : pub [Field;2], z : pub [u8;5])  {}",
+                "fn main(x: pub u8, y: pub u8) -> distinct pub [u8; 2] { [x, y] }",
             ],
         );
 
@@ -1468,7 +1534,9 @@ mod test {
             ("let", 3, "let $error: unspecified = Error"),
             ("foo = one two three", 1, "foo = plain::one"),
             ("constrain", 1, "constrain Error"),
+            ("assert", 1, "constrain Error"),
             ("constrain x ==", 1, "constrain (plain::x == Error)"),
+            ("assert(x ==)", 1, "constrain (plain::x == Error)"),
         ];
 
         let show_errors = |v| vecmap(v, ToString::to_string).join("\n");