diff --git a/examples/fibonacci.py b/examples/fibonacci.py
index 9274733..5d90614 100644
--- a/examples/fibonacci.py
+++ b/examples/fibonacci.py
@@ -1,73 +1,85 @@
-from __future__ import annotations
-from typing import Tuple
-
-# from chiquito import (dsl, cb, query, util)
-# from dsl import Circuit, StepType
-# from cb import eq
-# from query import Queriable
-# from util import F
-
 from chiquito.dsl import Circuit, StepType
 from chiquito.cb import eq
-from chiquito.query import Queriable
 from chiquito.util import F
+from chiquito.chiquito_ast import Last
 
 
-class Fibonacci(Circuit):
-    def setup(self: Fibonacci):
-        self.a: Queriable = self.forward("a")
-        self.b: Queriable = self.forward("b")
-
-        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
-        self.fibo_last_step = self.step_type(FiboLastStep(self, "fibo_last_step"))
-
-        self.pragma_first_step(self.fibo_step)
-        self.pragma_last_step(self.fibo_last_step)
-        self.pragma_num_steps(11)
-        # self.pragma_disable_q_enable()
-
-        # self.expose(self.b, First())
-        # self.expose(self.a, Last())
-        # self.expose(self.a, Step(1))
+class FiboFirstStep(StepType):
+    def setup(self):
+        self.c = self.internal("c")
+        self.constr(eq(self.circuit.a, 1))
+        self.constr(eq(self.circuit.b, 1))
+        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
+        self.transition(eq(self.circuit.b, self.circuit.a.next()))
+        self.transition(eq(self.c, self.circuit.b.next()))
+        self.transition(eq(self.circuit.n, self.circuit.n.next()))
 
-    def trace(self: Fibonacci, args: Any):
-        self.add(self.fibo_step, (1, 1))
-        a = 1
-        b = 2
-        for i in range(1, 10):
-            self.add(self.fibo_step, (a, b))
-            prev_a = a
-            a = b
-            b += prev_a
-        self.add(self.fibo_last_step, (a, b))
+    def wg(self, args):
+        a_value, b_value, n_value = args
+        self.assign(self.circuit.a, F(a_value))
+        self.assign(self.circuit.b, F(b_value))
+        self.assign(self.c, F(a_value + b_value))
+        self.assign(self.circuit.n, F(n_value))
 
 
 class FiboStep(StepType):
-    def setup(self: FiboStep):
+    def setup(self):
         self.c = self.internal("c")
         self.constr(eq(self.circuit.a + self.circuit.b, self.c))
         self.transition(eq(self.circuit.b, self.circuit.a.next()))
         self.transition(eq(self.c, self.circuit.b.next()))
+        self.transition(eq(self.circuit.n, self.circuit.n.next()))
 
-    def wg(self: FiboStep, args: Tuple[int, int]):
-        a_value, b_value = args
+    def wg(self, args):
+        a_value, b_value, n_value = args
         self.assign(self.circuit.a, F(a_value))
         self.assign(self.circuit.b, F(b_value))
         self.assign(self.c, F(a_value + b_value))
+        self.assign(self.circuit.n, F(n_value))
 
 
-class FiboLastStep(StepType):
-    def setup(self: FiboLastStep):
-        self.c = self.internal("c")
-        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
+class Padding(StepType):
+    def setup(self):
+        self.transition(eq(self.circuit.b, self.circuit.b.next()))
+        self.transition(eq(self.circuit.n, self.circuit.n.next()))
 
-    def wg(self: FiboLastStep, values=Tuple[int, int]):
-        a_value, b_value = values
+    def wg(self, args):
+        a_value, b_value, n_value = args
         self.assign(self.circuit.a, F(a_value))
         self.assign(self.circuit.b, F(b_value))
-        self.assign(self.c, F(a_value + b_value))
+        self.assign(self.circuit.n, F(n_value))
+
+
+class Fibonacci(Circuit):
+    def setup(self):
+        self.a = self.forward("a")
+        self.b = self.forward("b")
+        self.n = self.forward("n")
+
+        self.fibo_first_step = self.step_type(FiboFirstStep(self, "fibo_first_step"))
+        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
+        self.padding = self.step_type(Padding(self, "padding"))
+
+        self.pragma_num_steps(10)
+        self.pragma_first_step(self.fibo_first_step)
+        self.pragma_last_step(self.padding)
+
+        self.expose(self.b, Last())
+        self.expose(self.n, Last())
+
+    def trace(self, n):
+        self.add(self.fibo_first_step, (1, 1, n))
+        a = 1
+        b = 2
+        for i in range(1, n):
+            self.add(self.fibo_step, (a, b, n))
+            prev_a = a
+            a = b
+            b += prev_a
+        while self.needs_padding():
+            self.add(self.padding, (a, b, n))
 
 
 fibo = Fibonacci()
-fibo_witness = fibo.gen_witness(None)
+fibo_witness = fibo.gen_witness(7)
 fibo.halo2_mock_prover(fibo_witness)
diff --git a/examples/simple.py b/examples/simple.py
deleted file mode 100644
index 6a10b14..0000000
--- a/examples/simple.py
+++ /dev/null
@@ -1,19 +0,0 @@
-from __future__ import annotations
-from typing import Tuple
-
-from chiquito.dsl import Circuit, StepType
-from chiquito.cb import eq
-from chiquito.query import Queriable
-from chiquito.util import F
-import chiquito
-# from chiquito import chiquito
-
-
-# def main():
-print("Hello, world!")
-# print(Circuit)
-# print(StepType)
-# print(eq)
-# print(Queriable)
-# print(chiquito.__all__)
-print(dir(chiquito))
\ No newline at end of file
diff --git a/examples/tutorial_pt2.ipynb b/examples/tutorial_pt2.ipynb
index d76ea96..d2b04a1 100644
--- a/examples/tutorial_pt2.ipynb
+++ b/examples/tutorial_pt2.ipynb
@@ -8,15 +8,14 @@
     "# Part 2: Quick Start\n",
     "PyChiquito requires using a Python virtual environment for its dependencies, which you should have setup following the [PyChiquito README](https://github.com/qwang98/PyChiquito#readme).\n",
     "\n",
-    "Specifically, after cloning PyChiquito, you need to run the following commands in your local repo (NOT in this Jupyter Notebook), till you see `(.env)` at the start of your command line, which means that you've successfully enabled the virtual environment. You also need to install `maturin` and `py_ecc` dependencies to your local environment and build the project using `maturin develop`. Again, these are all done in your local command line.\n",
+    "Specifically, after cloning PyChiquito, you need to run the following commands in your local repo (NOT in this Jupyter Notebook), till you see `(.env)` at the start of your command line, which means that you've successfully enabled the virtual environment. You also need to install required dependencies to your local environment and build the project using `maturin develop`. Again, these are all done in your local command line.\n",
     "\n",
     "```\n",
     "python3 -m venv .env\n",
     "\n",
     "source .env/bin/activate\n",
     "\n",
-    "pip install maturin\n",
-    "pip install py_ecc\n",
+    "pip install -r requirements.txt\n",
     "\n",
     "maturin develop\n",
     "```\n",
diff --git a/examples/tutorial_pt3_ch1.ipynb b/examples/tutorial_pt3_ch1.ipynb
index 1f9abf0..01325c7 100644
--- a/examples/tutorial_pt3_ch1.ipynb
+++ b/examples/tutorial_pt3_ch1.ipynb
@@ -26,7 +26,7 @@
     "| 3 | 5 | 8 |\n",
     "|| ... ||\n",
     "\n",
-    "Besides assigning values to these signals, we also need to define the mathematical relationships among them, which we call \"constraints: in Chiquito. For each row:\n",
+    "Besides assigning values to these signals, we also need to define the mathematical relationships among them, which we call \"constraints\" in Chiquito. For each row:\n",
     "- a + b == c\n",
     "- b = a in the next row\n",
     "- c = b in the next row\n",
diff --git a/examples/tutorial_pt3_ch2.ipynb b/examples/tutorial_pt3_ch2.ipynb
index a763a72..4110317 100644
--- a/examples/tutorial_pt3_ch2.ipynb
+++ b/examples/tutorial_pt3_ch2.ipynb
@@ -8,19 +8,7 @@
     "# Part 3: Fibonacci Example\n",
     "# Chapter 2: StepType and Circuit\n",
     "In this Chapter, we code out the concepts learned in Chapter 1 in PyChiquito, but before that, let's import the dependencies first.\n",
-    "## Imports\n",
-    "These imports are for the typing hints included in this example. They are not required, because Python is a dynamically typed interpreted language and typings aren't enforced."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "id": "88bf1890-2e87-4aeb-967c-809fa1ddb6e6",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "from __future__ import annotations\n",
-    "from typing import Tuple"
+    "## Imports"
    ]
   },
   {
@@ -36,7 +24,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 1,
    "id": "bf77f66c-2e81-4b51-b7f1-24c1be6c9b99",
    "metadata": {},
    "outputs": [],
@@ -95,11 +83,11 @@
     "## FiboStep Witness Generation\n",
     "```\n",
     "class FiboStep(StepType):\n",
-    "    def setup(self: FiboStep):\n",
+    "    def setup(self):\n",
     "        # ...\n",
     "\n",
-    "    def wg(self: FiboStep, args: Tuple[int, int]):\n",
-    "        a_value, b_value = args\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value = args # `args` is a tuple of (int, int)\n",
     "        self.assign(self.circuit.a, F(a_value))\n",
     "        self.assign(self.circuit.b, F(b_value))\n",
     "        self.assign(self.c, F(a_value + b_value))\n",
@@ -138,6 +126,7 @@
     "        self.b = self.forward(\"b\")\n",
     "        \n",
     "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.pragma_num_steps(4)\n",
     "\n",
     "    def trace(self):\n",
     "        # TODO\n",
@@ -146,6 +135,8 @@
     "\n",
     "Next, we append the only step type to the circuit by defining it as `self.fibo_step`. `step_type` function only has one argument, which is the `FiboStep` object created using its class constructor.\n",
     "\n",
+    "Finally, we constrain the total number of step instances to 4, by using `self.pragma_num_steps`.\n",
+    "\n",
     "## Circuit Trace\n",
     "Now we instantiate step types and assign witness values using `trace`:\n",
     "```\n",
@@ -165,18 +156,18 @@
     "```\n",
     "`trace` takes two arguments, the `Fibonacci` circuit itself and the witness value assignment arguments `args`. We call `self.add` to instantiate `fibo_step` we defined and pass in the witness values for \"a\" and \"b\". Note that we only hardcoded witness values for the first step instance as `(1, 1)`, because all other witness values can be calculated given the nature of Fibonacci. \n",
     "\n",
-    "Note that `self.add` creates step instance by calling `wg` associated with the step type. Therefore, the second input of `self.add`, e.g. `(a, b)` in `self.add(self.fibo_step, (a, b))`, needs to match `args` in `FiboStep` `wg`, i.e. tuple of `a_value, b_value`.\n",
+    "Note that `self.add` creates step instance by calling `wg` function associated with the step type, which we defined earlier. The second argument of `self.add`, e.g. `(a, b)` in `self.add(self.fibo_step, (a, b))`, is actually the input for `wg`. Therefore, `(a, b)` needs to match `args` in `FiboStep` `wg`, i.e. tuple of `a_value, b_value`.\n",
     "\n",
     "We didn't pass in witness values for \"c\", because they are calculated in `FiboStep` `wg`.\n",
     "\n",
     "Note that we need to pass in witness value assignments in a single argument `args` and therefore we use a tuple in this case. `args` can really be any data type as long as it's one single argument.\n",
-    "FiboStep\n",
+    "\n",
     "After creating the first `FiboStep` instance, we loop over `FiboStep` instantiation for 3 more times, each time calculating and passing in a different tuple of assignments. Voila, here's our Fibonacci circuit with 4 `FiboStep` instances:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 2,
    "id": "d7c21e5d-5a9c-47b8-8c18-ed59fe885709",
    "metadata": {},
    "outputs": [],
@@ -200,6 +191,7 @@
     "        self.b = self.forward(\"b\")\n",
     "        \n",
     "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.pragma_num_steps(4)\n",
     "        \n",
     "    def trace(self, args):\n",
     "        self.add(self.fibo_step, (1, 1))\n",
@@ -223,7 +215,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 3,
    "id": "c0c9db95-8da8-49d6-a403-895491c833fe",
    "metadata": {},
    "outputs": [],
@@ -241,7 +233,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 4,
    "id": "d259b3b8-a15c-416c-9076-24c06f5b22e6",
    "metadata": {},
    "outputs": [
@@ -251,11 +243,11 @@
      "text": [
       "ASTCircuit(\n",
       "\tstep_types={\n",
-      "\t\t175487786213455723101965983777064356362: ASTStepType(\n",
-      "\t\t\tid=175487786213455723101965983777064356362,\n",
+      "\t\t142788599383371455194542612232465418762: ASTStepType(\n",
+      "\t\t\tid=142788599383371455194542612232465418762,\n",
       "\t\t\tname='fibo_step',\n",
       "\t\t\tsignals=[\n",
-      "\t\t\t\tInternalSignal(id=175487817112439103662857355366257789450, annotation='c')\n",
+      "\t\t\t\tInternalSignal(id=142788636620607836899675527199131830794, annotation='c')\n",
       "\t\t\t],\n",
       "\t\t\tconstraints=[\n",
       "\t\t\t\tConstraint(\n",
@@ -268,26 +260,26 @@
       "\t\t\t\tTransitionConstraint((c == next(b)))\n",
       "\t\t\t],\n",
       "\t\t\tannotations={\n",
-      "\t\t\t\t175487817112439103662857355366257789450: c\n",
+      "\t\t\t\t142788636620607836899675527199131830794: c\n",
       "\t\t\t}\n",
       "\t\t)\n",
       "\t},\n",
       "\tforward_signals=[\n",
-      "\t\tForwardSignal(id=175487708569856459120001313145084316170, phase=0, annotation='a'),\n",
-      "\t\tForwardSignal(id=175487756106753967678767124757946698250, phase=0, annotation='b')\n",
+      "\t\tForwardSignal(id=142788527285743567215743361712843786762, phase=0, annotation='a'),\n",
+      "\t\tForwardSignal(id=142788567692106449489348851195099875850, phase=0, annotation='b')\n",
       "\t],\n",
       "\tshared_signals=[],\n",
       "\tfixed_signals=[],\n",
       "\texposed=[],\n",
       "\tannotations={\n",
-      "\t\t175487708569856459120001313145084316170: a,\n",
-      "\t\t175487756106753967678767124757946698250: b,\n",
-      "\t\t175487786213455723101965983777064356362: fibo_step\n",
+      "\t\t142788527285743567215743361712843786762: a,\n",
+      "\t\t142788567692106449489348851195099875850: b,\n",
+      "\t\t142788599383371455194542612232465418762: fibo_step\n",
       "\t},\n",
       "\tfixed_gen=None,\n",
       "\tfirst_step=None,\n",
       "\tlast_step=None,\n",
-      "\tnum_steps=0\n",
+      "\tnum_steps=4\n",
       "\tq_enable=True\n",
       ")\n"
      ]
@@ -307,7 +299,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 5,
    "id": "24a0d3d8-710e-42fe-99ae-7491b50d7cd7",
    "metadata": {},
    "outputs": [],
@@ -325,7 +317,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 6,
    "id": "d1aaca8a-35eb-4c9d-8794-56869f696849",
    "metadata": {},
    "outputs": [
@@ -336,7 +328,7 @@
       "TraceWitness(\n",
       "\tstep_instances={\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n",
+      "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 1,\n",
       "\t\t\t\tb = 1,\n",
@@ -344,7 +336,7 @@
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n",
+      "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 1,\n",
       "\t\t\t\tb = 2,\n",
@@ -352,7 +344,7 @@
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n",
+      "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 2,\n",
       "\t\t\t\tb = 3,\n",
@@ -360,7 +352,7 @@
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n",
+      "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 3,\n",
       "\t\t\t\tb = 5,\n",
@@ -386,28 +378,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 7,
    "id": "a3f8d245-adab-4e68-9ee6-5f6bafc12bd1",
    "metadata": {},
    "outputs": [
     {
-     "name": "stderr",
+     "name": "stdout",
      "output_type": "stream",
      "text": [
-      "thread '<unnamed>' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n",
-      "note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace\n"
-     ]
-    },
-    {
-     "ename": "PanicException",
-     "evalue": "attempt to subtract with overflow",
-     "output_type": "error",
-     "traceback": [
-      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[0;31mPanicException\u001b[0m                            Traceback (most recent call last)",
-      "Cell \u001b[0;32mIn[8], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfibo_witness\u001b[49m\u001b[43m)\u001b[49m\n",
-      "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m    101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m    102\u001b[0m     ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m     \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m    104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m    105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n",
-      "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow"
+      "145806696406867587164175801408658475530\n",
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
      ]
     }
    ],
@@ -428,7 +410,7 @@
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": ".env",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   },
diff --git a/examples/tutorial_pt3_ch3.ipynb b/examples/tutorial_pt3_ch3.ipynb
index 872bfab..dfa914d 100644
--- a/examples/tutorial_pt3_ch3.ipynb
+++ b/examples/tutorial_pt3_ch3.ipynb
@@ -28,33 +28,20 @@
    "metadata": {},
    "outputs": [
     {
-     "name": "stderr",
+     "name": "stdout",
      "output_type": "stream",
      "text": [
-      "thread '<unnamed>' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n",
-      "note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace\n"
-     ]
-    },
-    {
-     "ename": "PanicException",
-     "evalue": "attempt to subtract with overflow",
-     "output_type": "error",
-     "traceback": [
-      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[0;31mPanicException\u001b[0m                            Traceback (most recent call last)",
-      "Cell \u001b[0;32mIn[1], line 40\u001b[0m\n\u001b[1;32m     38\u001b[0m fibo \u001b[38;5;241m=\u001b[39m Fibonacci()\n\u001b[1;32m     39\u001b[0m fibo_witness \u001b[38;5;241m=\u001b[39m fibo\u001b[38;5;241m.\u001b[39mgen_witness(\u001b[38;5;28;01mNone\u001b[39;00m)\n\u001b[0;32m---> 40\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfibo_witness\u001b[49m\u001b[43m)\u001b[49m\n",
-      "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m    101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m    102\u001b[0m     ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m     \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m    104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m    105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n",
-      "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow"
+      "167511621523169244061366759362598144522\n",
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
      ]
     }
    ],
    "source": [
-    "from __future__ import annotations\n",
-    "from typing import Tuple\n",
-    "\n",
-    "from dsl import Circuit, StepType\n",
-    "from cb import eq\n",
-    "from util import F\n",
+    "from chiquito.dsl import Circuit, StepType\n",
+    "from chiquito.cb import eq\n",
+    "from chiquito.util import F\n",
     "\n",
     "class FiboStep(StepType):\n",
     "    def setup(self):\n",
@@ -75,6 +62,7 @@
     "        self.b = self.forward(\"b\")\n",
     "        \n",
     "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.pragma_num_steps(4)\n",
     "        \n",
     "    def trace(self, args):\n",
     "        self.add(self.fibo_step, (1, 1))\n",
@@ -96,7 +84,7 @@
    "id": "182101e0-f5ee-4c16-a7c1-d09909dcbb3b",
    "metadata": {},
    "source": [
-    "Now we swap the first step instance from `(1, 1, 2)` to `(0, 2, 2)`. We use the `evil_witness` function to swap step index 0 assignment index 0 to `F(0)` and step index 0 assignment index 0 to `F(2)`."
+    "Now we swap the first step instance from `(1, 1, 2)` to `(0, 2, 2)`. We use the `evil_witness_test` function to swap step index 0 assignment index 0 to `F(0)` and step index 0 assignment index 0 to `F(2)`."
    ]
   },
   {
@@ -109,6 +97,35 @@
     "evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0], assignment_indices=[0, 1], rhs=[F(0), F(2)])"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "a9291c66-5fd9-48a1-8980-7b4283cc3ca8",
+   "metadata": {},
+   "source": [
+    "According to the three constraints `a + b == c`, `b == a.next`, and `c == b.next`, we swap the second step instance from `(1, 2, 3)` to `(2, 2, 4)` and modify the third and fourth step instances likewise, resulting in a new witness displayed below:\n",
+    "\n",
+    "||Signals||\n",
+    "| :-: | :-: | :-: |\n",
+    "| a | b | c |\n",
+    "| 0 | 2 | 2 |\n",
+    "| 2 | 2 | 4 |\n",
+    "| 2 | 4 | 6 |\n",
+    "| 4 | 6 | 10 |\n",
+    "|| ... ||\n",
+    "\n",
+    "We use the `evil_witness_test` function to further modify the `evil_witness`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "77168c22-aaea-4890-89ba-b3b3cf37c86d",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "evil_witness = evil_witness.evil_witness_test(step_instance_indices=[1, 1, 2, 2, 3, 3, 3], assignment_indices=[0, 2, 1, 2, 0, 1, 2], rhs=[F(2), F(4), F(4), F(6), F(4), F(6), F(10)])"
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "19c5a476-e31e-4bc6-9bb2-7635c16b37ba",
@@ -119,7 +136,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 4,
    "id": "dcd26089-ecb0-4a5e-8296-318a7b644b98",
    "metadata": {},
    "outputs": [
@@ -130,7 +147,7 @@
       "TraceWitness(\n",
       "\tstep_instances={\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n",
+      "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 0,\n",
       "\t\t\t\tb = 2,\n",
@@ -138,27 +155,27 @@
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n",
+      "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
       "\t\t\tassignments={\n",
-      "\t\t\t\ta = 1,\n",
+      "\t\t\t\ta = 2,\n",
       "\t\t\t\tb = 2,\n",
-      "\t\t\t\tc = 3\n",
+      "\t\t\t\tc = 4\n",
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n",
+      "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
       "\t\t\tassignments={\n",
       "\t\t\t\ta = 2,\n",
-      "\t\t\t\tb = 3,\n",
-      "\t\t\t\tc = 5\n",
+      "\t\t\t\tb = 4,\n",
+      "\t\t\t\tc = 6\n",
       "\t\t\t},\n",
       "\t\t),\n",
       "\t\tStepInstance(\n",
-      "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n",
+      "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
       "\t\t\tassignments={\n",
-      "\t\t\t\ta = 3,\n",
-      "\t\t\t\tb = 5,\n",
-      "\t\t\t\tc = 8\n",
+      "\t\t\t\ta = 4,\n",
+      "\t\t\t\tb = 6,\n",
+      "\t\t\t\tc = 10\n",
       "\t\t\t},\n",
       "\t\t)\n",
       "\t},\n",
@@ -180,27 +197,17 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 5,
    "id": "044e067e-77fa-4027-94dd-e39a35e87de8",
    "metadata": {},
    "outputs": [
     {
-     "name": "stderr",
+     "name": "stdout",
      "output_type": "stream",
      "text": [
-      "thread '<unnamed>' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n"
-     ]
-    },
-    {
-     "ename": "PanicException",
-     "evalue": "attempt to subtract with overflow",
-     "output_type": "error",
-     "traceback": [
-      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
-      "\u001b[0;31mPanicException\u001b[0m                            Traceback (most recent call last)",
-      "Cell \u001b[0;32mIn[4], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mevil_witness\u001b[49m\u001b[43m)\u001b[49m\n",
-      "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m    101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m    102\u001b[0m     ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m     \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m    104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m    105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n",
-      "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow"
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
      ]
     }
    ],
@@ -215,7 +222,7 @@
    "source": [
     "Surprisingly, `evil_witness` generated a proof that passed verification. This constitutes a soundness error, because the first step instance isn't `(1, 1, 2)` as we initially specified, so why can the witness still pass the constraints?\n",
     "\n",
-    "The answer is simple, because in the first step instance, we never constrained the values of \"a\" and \"b\" to 1 and 1 in `setup` of `FiboStep`. We also didn't constrain the first step instance to be `FiboStep`.\n",
+    "The answer is simple, because in the first step instance, we never constrained the values of \"a\" and \"b\" to 1 and 1 in `setup` of `FiboStep`.\n",
     "\n",
     "You might be wondering: in `trace`, didn't we set \"a\" and \"b\" to `(1, 1)` and added `FiboStep` as the first step instance? In fact, `trace` and `wg` are really helper functions for the prover to easily generate a witness, whose data can be tampered with as shown in `evil_witness_test`. The only conditions enforced are defined in circuit and step type `setup`. Therefore, to fix the soundness error, we need to add more constraints, in Chapter 4."
    ]
diff --git a/examples/tutorial_pt3_ch4.ipynb b/examples/tutorial_pt3_ch4.ipynb
new file mode 100644
index 0000000..36b6d82
--- /dev/null
+++ b/examples/tutorial_pt3_ch4.ipynb
@@ -0,0 +1,322 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "291ef2c6-bce5-4166-973d-d34d04f31bfb",
+   "metadata": {},
+   "source": [
+    "# Part 3: Fibonacci Example\n",
+    "# Chapter 4: Multiple StepTypes"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d7a26b56-e0c7-4e35-a064-5899aa2ef6b7",
+   "metadata": {},
+   "source": [
+    "To avoid the soundness error from `evil_witness` in Chapter 3, we need to constrain that forward signals \"a\" and \"b\" are both 1 in the first step instance. Because this isn't true for all step instances, we need to create a new step type, called `FiboFirstStep`, which is idential to `FiboStep` except two additional constraints for \"a\" and \"b\":\n",
+    "\n",
+    "| Step Type | Step Instance Index || Signals |||| Setups |||\n",
+    "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
+    "||| a | b | c | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 |\n",
+    "| fibo first step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 |\n",
+    "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| ... | ... || ... |||| ... |||\n",
+    "\n",
+    "The following shows the incremental code of `FiboFirstStep` compared to `FiboStep`:\n",
+    "\n",
+    "```\n",
+    "class FiboFirstStep(StepType):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        self.constr(eq(self.circuit.a, 1))\n",
+    "        self.constr(eq(self.circuit.b, 1))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        # ...\n",
+    "```\n",
+    "\n",
+    "Next, in circuit `setup`, we need to append this step type and constrain that the first step instance is `FiboFirstStep`. Otherwise `setup` is identical to that in Chapter 3:\n",
+    "\n",
+    "```\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.pragma_first_step(self.fibo_first_step)\n",
+    "        \n",
+    "    def trace(self, args):\n",
+    "        # TODO\n",
+    "```\n",
+    "\n",
+    "Finally, in circuit `trace`, we need to instantiate `FiboFirstStep` for the first step instance. Otherwise `trace` is identical to that in Chapter 3:\n",
+    "\n",
+    "```\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        \n",
+    "    def trace(self, args):\n",
+    "        self.add(self.fibo_first_step, (1, 1))\n",
+    "        # ...\n",
+    "```\n",
+    "\n",
+    "Putting everything together, we have the following circuit with two step types:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "10ce06ce-1345-4c00-9265-d59cb93a8014",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "186650748934699451528647048735450860042\n",
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
+     ]
+    }
+   ],
+   "source": [
+    "from chiquito.dsl import Circuit, StepType\n",
+    "from chiquito.cb import eq\n",
+    "from chiquito.util import F\n",
+    "\n",
+    "class FiboFirstStep(StepType):\n",
+    "    def setup(self):\n",
+    "        self.c = self.internal(\"c\")\n",
+    "        self.constr(eq(self.circuit.a, 1))\n",
+    "        self.constr(eq(self.circuit.b, 1))\n",
+    "        self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.a.next()))\n",
+    "        self.transition(eq(self.c, self.circuit.b.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.c, F(a_value + b_value))\n",
+    "\n",
+    "class FiboStep(StepType):\n",
+    "    def setup(self):\n",
+    "        self.c = self.internal(\"c\")\n",
+    "        self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.a.next()))\n",
+    "        self.transition(eq(self.c, self.circuit.b.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.c, F(a_value + b_value))\n",
+    "\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        self.a = self.forward(\"a\")\n",
+    "        self.b = self.forward(\"b\")\n",
+    "        \n",
+    "        self.fibo_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n",
+    "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.pragma_num_steps(4)\n",
+    "        self.pragma_first_step(self.fibo_first_step)\n",
+    "        \n",
+    "    def trace(self, args):\n",
+    "        self.add(self.fibo_first_step, (1, 1))\n",
+    "        a = 1\n",
+    "        b = 2\n",
+    "        for i in range(1, 4):\n",
+    "            self.add(self.fibo_step, (a, b))\n",
+    "            prev_a = a\n",
+    "            a = b\n",
+    "            b += prev_a\n",
+    "\n",
+    "fibo = Fibonacci()\n",
+    "fibo_witness = fibo.gen_witness(None)\n",
+    "fibo.halo2_mock_prover(fibo_witness)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "5571eca6-af48-419f-8a87-2c472b3f246f",
+   "metadata": {},
+   "source": [
+    "We construct and pass over the same `evil_witness` from Chapter 3. This time `evil_witness` fails at the two new constraints we wrote, e.g. `a == 1` and `b == 1` from `FiboFirstStep`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "5a615f38-417f-4928-bc24-5578bc5d92f3",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Err(\n",
+      "    [\n",
+      "        ConstraintCaseDebug {\n",
+      "            constraint: Constraint {\n",
+      "                gate: Gate {\n",
+      "                    index: 0,\n",
+      "                    name: \"main\",\n",
+      "                },\n",
+      "                index: 0,\n",
+      "                name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n",
+      "            },\n",
+      "            location: InRegion {\n",
+      "                region: Region 0 ('circuit'),\n",
+      "                offset: 0,\n",
+      "            },\n",
+      "            cell_values: [\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Advice,\n",
+      "                            index: 0,\n",
+      "                            annotation: \"srcm forward a\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"0\",\n",
+      "                ),\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Advice,\n",
+      "                            index: 3,\n",
+      "                            annotation: \"'step selector for fibo_first_step'\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"1\",\n",
+      "                ),\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Fixed,\n",
+      "                            index: 0,\n",
+      "                            annotation: \"q_enable\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"1\",\n",
+      "                ),\n",
+      "            ],\n",
+      "        },\n",
+      "        ConstraintCaseDebug {\n",
+      "            constraint: Constraint {\n",
+      "                gate: Gate {\n",
+      "                    index: 0,\n",
+      "                    name: \"main\",\n",
+      "                },\n",
+      "                index: 1,\n",
+      "                name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n",
+      "            },\n",
+      "            location: InRegion {\n",
+      "                region: Region 0 ('circuit'),\n",
+      "                offset: 0,\n",
+      "            },\n",
+      "            cell_values: [\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Advice,\n",
+      "                            index: 1,\n",
+      "                            annotation: \"srcm forward b\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\",\n",
+      "                ),\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Advice,\n",
+      "                            index: 3,\n",
+      "                            annotation: \"'step selector for fibo_first_step'\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"1\",\n",
+      "                ),\n",
+      "                (\n",
+      "                    DebugVirtualCell {\n",
+      "                        name: \"\",\n",
+      "                        column: DebugColumn {\n",
+      "                            column_type: Fixed,\n",
+      "                            index: 0,\n",
+      "                            annotation: \"q_enable\",\n",
+      "                        },\n",
+      "                        rotation: 0,\n",
+      "                    },\n",
+      "                    \"1\",\n",
+      "                ),\n",
+      "            ],\n",
+      "        },\n",
+      "    ],\n",
+      ")\n",
+      "Constraint 0 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n",
+      "- Column('Advice', 0 - srcm forward a)@0 = 0\n",
+      "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n",
+      "- Column('Fixed', 0 - q_enable)@0 = 1\n",
+      "\n",
+      "Constraint 1 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n",
+      "- Column('Advice', 1 - srcm forward b)@0 = 0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\n",
+      "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n",
+      "- Column('Fixed', 0 - q_enable)@0 = 1\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0, 1, 1, 2, 2, 3, 3, 3], assignment_indices=[0, 1, 0, 2, 1, 2, 0, 1, 2], rhs=[F(0), F(2), F(2), F(4), F(4), F(6), F(4), F(6), F(10)])\n",
+    "fibo.halo2_mock_prover(evil_witness)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "10ba5900-2619-4c87-8351-1cbdc8f5628b",
+   "metadata": {},
+   "source": [
+    "By adding new constraints to eliminate soundness errors, this chapter demonstrated an iterative way of developing zero knowledge circuits. Circuit engineer can proactively generate witnesses in edge cases and if a false positive passes the circuit, add more constraints to prevent these edge cases. \n",
+    "\n",
+    "Besides, we learned that with multiple step types, Chiquito can create step instances with different signals and constraints, thereby allowing great versatility in circuit design.\n",
+    "\n",
+    "Finally, this example shows again that circuit setup and witness generation are separate processes. There can be multiple witnesses for the same circuit setup. As a great analogy, a circuit can be considered a piece of \"hardware\" whereas its witnesses \"softwares\" that are compatible with the hardware."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "pychiquito_kernel",
+   "language": "python",
+   "name": "pychiquito_kernel"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.11.4"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/examples/tutorial_pt3_ch5.ipynb b/examples/tutorial_pt3_ch5.ipynb
new file mode 100644
index 0000000..90d110a
--- /dev/null
+++ b/examples/tutorial_pt3_ch5.ipynb
@@ -0,0 +1,474 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "5ec470ae-aca1-4c7e-a048-d115633531d8",
+   "metadata": {},
+   "source": [
+    "# Part 3: Fibonacci Example\n",
+    "# Chapter 5: Padding and Exposing Signals\n",
+    "In prior examples, all Fibonacci circuit witnesses have the same number of step instances. According to our analogy where a circuit is considered a piece of hardware and its witnesses compatible softwares, it's natural to think that we'd allow for more flexibility for our witnesses. Most immediately, and we shouldn't limit all Fibonacci circuit witnesses to have the same number of step instances.\n",
+    "\n",
+    "However, you might wonder, doesn't `self.pragma_num_steps(4)` limit the number of step instances to 4? Besides, doesn't this function guarantee the Fibonacci circuit's security, such that we have a fixed circuit setup with a specific number of step instances, thereby making the circuit a piece of \"hardware\" that cannot be tampered with? How can we allow for BOTH a fixed circuit setup AND flexible witnesses? This problem is frequently encountered in projects like PSE's zkEVM, where witnesses with very different sizes are passed into the same circuit.\n",
+    "\n",
+    "## Padding\n",
+    "In Chiquito, you can achieve fixed circuit setup with flexible witnesses through a technique called \"padding\":\n",
+    "- To have a fixed circuit setup, we specify a maximum number of steps that won't be exceeded by all plausible witnesses. For example, we can set this number to 10 for the Fibonacci circuit, but it's really up to you.\n",
+    "- To have flexible witnesses that still pass the same circuit setup, we add \"padding step instances\" towards the end of the witness.\n",
+    "- For example, if we want to calculate 4 rounds for the Fibonacci series, we add 6 padding step instances:\n",
+    "\n",
+    "| Step Type | Step Instance Index || Signals |||| Setups |||\n",
+    "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
+    "||| a | b | c | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 |\n",
+    "| fibo first step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 |\n",
+    "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| padding | 4 |||||||||\n",
+    "| padding | 5 |||||||||\n",
+    "| padding | 6 |||||||||\n",
+    "| padding | 7 |||||||||\n",
+    "| padding | 8 |||||||||\n",
+    "| padding | 9 |||||||||\n",
+    "\n",
+    "- If we want 7 rounds, we add 3 padding step instances.\n",
+    "\n",
+    "| Step Type | Step Instance Index || Signals |||| Setups |||\n",
+    "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
+    "||| a | b | c | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 |\n",
+    "| fibo first step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 |\n",
+    "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 4 | 5 | 8 | 13 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 5 | 8 | 13 | 21 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| fibo step | 6 | 13 | 21 | 34 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
+    "| padding | 7 |||||||||\n",
+    "| padding | 8 |||||||||\n",
+    "| padding | 9 |||||||||\n",
+    "\n",
+    "## Exposing Signals\n",
+    "In prior examples, the witnesses we generate are all PRIVATE by default. While they are visible to the prover, or in the context of Chiquito, the writer of `trace` function, they are not visible to the verifier. However, it's common in zero knowledge proof systems to expose some witness values to both the prover and the verifier. Common examples include output of a hash function or the root of a Merkle tree.\n",
+    "\n",
+    "For pure demonstration purpose, say that we want to expose the result of our Fibonacci calculation after an arbitrary number of `n` rounds (where n <= 10). We also want to expose the round number `n`. Because we need to specify which instance of the signal to expose and because we want to allow for witnesses with arbitrary number of step instances, we cannot expose a specific step instance. Rather, the best practice is to copy over the Fibonacci result for all padding steps and `n` for all steps through the last step and expose the last step instance.\n",
+    "\n",
+    "Building on top of the table example above where `n == 7`, we create a new signal `n` and populate the three padding step instances:\n",
+    "\n",
+    "| Step Type | Step Instance Index || Signals ||||| Setups ||||\n",
+    "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
+    "||| a | b | c | n | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 | constraint 6 |\n",
+    "| fibo first step | 0 | 1 | 1 | 2 | 7 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 | n == n.next |\n",
+    "| fibo step | 1 | 1 | 2 | 3 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| fibo step | 2 | 2 | 3 | 5 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| fibo step | 3 | 3 | 5 | 8 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| fibo step | 4 | 5 | 8 | 13 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| fibo step | 5 | 8 | 13 | 21 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| fibo step | 6 | 13 | 21 | 34 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
+    "| padding | 7 | 21 | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
+    "| padding | 8 | n.a. | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
+    "| padding | 9 | n.a. | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
+    "\n",
+    "## Coding up the Concepts\n",
+    "Now that we introduced padding and exposing signals, let's express the table above in a Chiquito circuit.\n",
+    "\n",
+    "First, let's add the padding step type: \n",
+    "\n",
+    "```\n",
+    "class Padding(StepType):\n",
+    "    def setup(self):\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.b.next()))\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "```\n",
+    "\n",
+    "In `setup`, we added two transition constraints. \n",
+    "- `b == b.next` copies the Fibonacci result after `n` rounds through the last padding step. Note that \"b\" in the first `Padding` step instance equals \"c\" in the last `FiboStep` instance, which is the final result.\n",
+    "- `n == n.next` copies the `n` for exposing at the last step instance. Note that exposing `b` and `n` is done at the circuit level `setup`, which we leave for later.\n",
+    "\n",
+    "Note that the new signal `n` is not added in `setup`, because it'll be a forward signal to be added in circuit level `setup`.\n",
+    "\n",
+    "In `wg`, we assign `a_value`, `b_value`, and `n_value` to their corresponding signals. We assign `a_value`, although it's not exposed in the last padding step, because the last `FiboStep` instance constraints `b == a.next`.\n",
+    "\n",
+    "Second, let's modify all existing step types to account for the new signal `n`, basically adding a new constraint `n == n.next` in `setup` and assigning `n_value` in `wg`:\n",
+    "\n",
+    "```\n",
+    "class FiboFirstStep(StepType):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        # ...\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "\n",
+    "class FiboStep(StepType):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        # ...\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "```\n",
+    "\n",
+    "Third, let's modify the circuit `setup`:\n",
+    "\n",
+    "```\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        self.a = self.forward(\"a\")\n",
+    "        self.n = self.forward(\"n\")\n",
+    "        \n",
+    "        self.fibo_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n",
+    "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.padding = self.step_type(Padding(self, \"padding\"))\n",
+    "\n",
+    "        self.pragma_num_steps(10)\n",
+    "        self.pragma_first_step(self.fibo_first_step)\n",
+    "        self.pragma_last_step(self.padding)\n",
+    "\n",
+    "        self.expose(self.b, Last())\n",
+    "        self.expose(self.n, Last())\n",
+    "        \n",
+    "    def trace(self, n):\n",
+    "        # TODO\n",
+    "```\n",
+    "\n",
+    "The code above did a few things:\n",
+    "- Add forward signal `n` and append it to the circuit\n",
+    "- Add padding step and append it to the circuit\n",
+    "- Modify `pragma_num_steps` to `10`, the maximum number of steps that won't be exceeded by all plausible witnesses\n",
+    "- Constrain that the last step instance is `Padding`\n",
+    "- Expose the last instances of signals `b` (the final Fibonacci result) and `n` (the number of non-padding step instances). `self.expose` takes two parameters: the signal to expose and the step instance of the signal to expose. In the example above `Last()` means the last step instance. In Chiquito, you can also specify `First()` for the first step instance or `Step(index)` for the step instance at a specific `index`.\n",
+    "\n",
+    "Finally, we instantiate step instances and generate witness using `trace`, with the following step instance combination:\n",
+    "- `FiboFirstStep` for the 1st step instance\n",
+    "- `FiboStep` for the 2nd through n-th step instance\n",
+    "- `Padding` for the rest step instances such that there are 10 step instances in total, as specified by `self.pragma_num_steps(10)`\n",
+    "\n",
+    "```\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        # ...\n",
+    "        \n",
+    "    def trace(self, n):\n",
+    "        self.add(self.fibo_first_step, (1, 1, n))\n",
+    "        a = 1\n",
+    "        b = 2\n",
+    "        for i in range(1, n):\n",
+    "            self.add(self.fibo_step, (a, b, n))\n",
+    "            prev_a = a\n",
+    "            a = b\n",
+    "            b += prev_a\n",
+    "        while(self.needs_padding()):\n",
+    "            self.add(self.padding, (a, b, n))\n",
+    "```\n",
+    "\n",
+    "In the code above, we added a new parameter `n` for `trace`, which is the user's input when calling `gen_witness`. `n` is passed into `self.add` as an input parameter to instantiate different step types. Again, note the matching relationship of witness generation parameters between `self.add` and `wg`:\n",
+    "- In `self.add(self.fibo_first_step, (1, 1, n))`, `(1, 1, n)` correspond to `a_value, b_value, n_value` in `FiboFirstStep` `wg`\n",
+    "- In `self.add(self.fibo_step, (a, b, n))`, `(a, b, n)` correspond to `a_value, b_value, n_value` in `FiboStep` `wg`\n",
+    "- In `self.add(self.padding, (a, b, n))`, `(a, b, n)` correspond to `a_value, b_value, n_value` in `Padding` `wg`\n",
+    "\n",
+    "## Putting Everything Together\n",
+    "Putting all pieces together, we have the following circuit, which allows for a fixed circuit setup with 10 step instances, as well as flexible witnesses with an arbitrary number of `n` step instances up to 10, filled with `Padding` step instances if fewer than 10:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "525c00f0-210f-4328-85a6-eac0beeb3124",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from chiquito.dsl import Circuit, StepType\n",
+    "from chiquito.cb import eq\n",
+    "from chiquito.util import F\n",
+    "from chiquito.chiquito_ast import Last\n",
+    "\n",
+    "class FiboFirstStep(StepType):\n",
+    "    def setup(self):\n",
+    "        self.c = self.internal(\"c\")\n",
+    "        self.constr(eq(self.circuit.a, 1))\n",
+    "        self.constr(eq(self.circuit.b, 1))\n",
+    "        self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.a.next()))\n",
+    "        self.transition(eq(self.c, self.circuit.b.next()))\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.c, F(a_value + b_value))\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "\n",
+    "class FiboStep(StepType):\n",
+    "    def setup(self):\n",
+    "        self.c = self.internal(\"c\")\n",
+    "        self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.a.next()))\n",
+    "        self.transition(eq(self.c, self.circuit.b.next()))\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.c, F(a_value + b_value))\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "\n",
+    "class Padding(StepType):\n",
+    "    def setup(self):\n",
+    "        self.transition(eq(self.circuit.b, self.circuit.b.next()))\n",
+    "        self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
+    "\n",
+    "    def wg(self, args):\n",
+    "        a_value, b_value, n_value = args\n",
+    "        self.assign(self.circuit.a, F(a_value))\n",
+    "        self.assign(self.circuit.b, F(b_value))\n",
+    "        self.assign(self.circuit.n, F(n_value))\n",
+    "\n",
+    "class Fibonacci(Circuit):\n",
+    "    def setup(self):\n",
+    "        self.a = self.forward(\"a\")\n",
+    "        self.b = self.forward(\"b\")\n",
+    "        self.n = self.forward(\"n\")\n",
+    "        \n",
+    "        self.fibo_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n",
+    "        self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
+    "        self.padding = self.step_type(Padding(self, \"padding\"))\n",
+    "\n",
+    "        self.pragma_num_steps(10)\n",
+    "        self.pragma_first_step(self.fibo_first_step)\n",
+    "        self.pragma_last_step(self.padding)\n",
+    "\n",
+    "        self.expose(self.b, Last())\n",
+    "        self.expose(self.n, Last())\n",
+    "        \n",
+    "    def trace(self, n):\n",
+    "        self.add(self.fibo_first_step, (1, 1, n))\n",
+    "        a = 1\n",
+    "        b = 2\n",
+    "        for i in range(1, n):\n",
+    "            self.add(self.fibo_step, (a, b, n))\n",
+    "            prev_a = a\n",
+    "            a = b\n",
+    "            b += prev_a\n",
+    "        while(self.needs_padding()):\n",
+    "            self.add(self.padding, (a, b, n))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "048c2b46-fa2c-4e5d-afe6-4c47df8520ce",
+   "metadata": {},
+   "source": [
+    "We initialize the circuit, generate a witness with 7 fibo first and fibo step instances (plus 3 padding step instances), and print the witness:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "39763670-a983-49cc-b812-164be8535997",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "TraceWitness(\n",
+      "\tstep_instances={\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218549979944188879026240919924757891594,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 1,\n",
+      "\t\t\t\tb = 1,\n",
+      "\t\t\t\tc = 2,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 1,\n",
+      "\t\t\t\tb = 2,\n",
+      "\t\t\t\tc = 3,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 2,\n",
+      "\t\t\t\tb = 3,\n",
+      "\t\t\t\tc = 5,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 3,\n",
+      "\t\t\t\tb = 5,\n",
+      "\t\t\t\tc = 8,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 5,\n",
+      "\t\t\t\tb = 8,\n",
+      "\t\t\t\tc = 13,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 8,\n",
+      "\t\t\t\tb = 13,\n",
+      "\t\t\t\tc = 21,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 13,\n",
+      "\t\t\t\tb = 21,\n",
+      "\t\t\t\tc = 34,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 21,\n",
+      "\t\t\t\tb = 34,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 21,\n",
+      "\t\t\t\tb = 34,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t),\n",
+      "\t\tStepInstance(\n",
+      "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n",
+      "\t\t\tassignments={\n",
+      "\t\t\t\ta = 21,\n",
+      "\t\t\t\tb = 34,\n",
+      "\t\t\t\tn = 7\n",
+      "\t\t\t},\n",
+      "\t\t)\n",
+      "\t},\n",
+      ")\n"
+     ]
+    }
+   ],
+   "source": [
+    "fibo = Fibonacci()\n",
+    "fibo_witness = fibo.gen_witness(7)\n",
+    "print(fibo_witness)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3aeae320-256c-4cf9-8ee2-92a5d7e58c07",
+   "metadata": {},
+   "source": [
+    "Generate and verify proof with this witness. Should return `Ok(())`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "3c429c18-a38e-48ed-b547-e0a9823a663a",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "219491840378750327758403926198542010890\n",
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
+     ]
+    }
+   ],
+   "source": [
+    "fibo.halo2_mock_prover(fibo_witness)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ed1c45e6-4f4d-434a-a061-18193af3ba44",
+   "metadata": {},
+   "source": [
+    "Generate another witness with 4 fibo first and fibo step instances (plus 6 padding step instances) and verify. Should return `Ok(())`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "id": "3039a36e-30f0-4a81-b1a3-e22ffe1ce39f",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Ok(\n",
+      "    (),\n",
+      ")\n"
+     ]
+    }
+   ],
+   "source": [
+    "another_fibo_witness = fibo.gen_witness(4)\n",
+    "fibo.halo2_mock_prover(another_fibo_witness)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "20d3d27c-6a3e-41f7-a476-5d589afe7247",
+   "metadata": {},
+   "source": [
+    "In this chapter, we learned how to construct a circuit with a fixed setup but flexible witnesses. Specifically, we fixed the number of step instances for the circuit setup but allowed for arbitrary numbers of step instances for the witnesses, by allowing the user to customize witnesses with parameter `n`."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "pychiquito_kernel",
+   "language": "python",
+   "name": "pychiquito_kernel"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.11.4"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/python/chiquito/chiquito_ast.py b/python/chiquito/chiquito_ast.py
index 1f4b28c..1fbbcf1 100644
--- a/python/chiquito/chiquito_ast.py
+++ b/python/chiquito/chiquito_ast.py
@@ -1,9 +1,8 @@
 from __future__ import annotations
-from typing import Callable, List, Dict, Optional, Any, Tuple
+from typing import Callable, List, Dict, Optional, Tuple
 from dataclasses import dataclass, field, asdict
-# from chiquito import wit_gen, expr, query, util
 
-from chiquito.wit_gen import FixedGenContext, StepInstance
+from chiquito.wit_gen import FixedGenContext
 from chiquito.expr import Expr
 from chiquito.util import uuid
 from chiquito.query import Queriable
diff --git a/python/chiquito/dsl.py b/python/chiquito/dsl.py
index ef4cdc4..45be3ec 100644
--- a/python/chiquito/dsl.py
+++ b/python/chiquito/dsl.py
@@ -1,15 +1,14 @@
 from __future__ import annotations
 from enum import Enum
 from typing import Callable, Any
-from  chiquito import rust_chiquito  # rust bindings
 import json
-from chiquito import (chiquito_ast, wit_gen)
 
 from chiquito.chiquito_ast import ASTCircuit, ASTStepType, ExposeOffset
 from chiquito.query import Internal, Forward, Queriable, Shared, Fixed
 from chiquito.wit_gen import FixedGenContext, StepInstance, TraceWitness
 from chiquito.cb import Constraint, Typing, ToConstraint, to_constraint
 from chiquito.util import CustomEncoder, F
+from chiquito.rust_chiquito import ast_to_halo2, halo2_mock_prover
 
 
 class CircuitMode(Enum):
@@ -83,9 +82,18 @@ def pragma_disable_q_enable(self: Circuit) -> None:
 
     def add(self: Circuit, step_type: StepType, args: Any):
         assert self.mode == CircuitMode.Trace
+        if len(self.witness.step_instances) >= self.ast.num_steps:
+            raise ValueError(f"Number of step instances exceeds {self.ast.num_steps}")
         step_instance: StepInstance = step_type.gen_step_instance(args)
         self.witness.step_instances.append(step_instance)
 
+    def needs_padding(self: Circuit) -> bool:
+        return len(self.witness.step_instances) < self.ast.num_steps
+
+    def padding(self: Circuit, step_type: StepType, args: Any):
+        while self.needs_padding():
+            self.add(step_type, args)
+
     def gen_witness(self: Circuit, args: Any) -> TraceWitness:
         self.mode = CircuitMode.Trace
         self.witness = TraceWitness()
@@ -101,9 +109,9 @@ def get_ast_json(self: Circuit) -> str:
     def halo2_mock_prover(self: Circuit, witness: TraceWitness):
         if self.rust_ast_id == 0:
             ast_json: str = self.get_ast_json()
-            self.rust_ast_id: int = rust_chiquito.ast_to_halo2(ast_json)
+            self.rust_ast_id: int = ast_to_halo2(ast_json)
         witness_json: str = witness.get_witness_json()
-        rust_chiquito.halo2_mock_prover(witness_json, self.rust_ast_id)
+        halo2_mock_prover(witness_json, self.rust_ast_id)
 
     def __str__(self: Circuit) -> str:
         return self.ast.__str__()
diff --git a/python/chiquito/wit_gen.py b/python/chiquito/wit_gen.py
index b740875..2b8af91 100644
--- a/python/chiquito/wit_gen.py
+++ b/python/chiquito/wit_gen.py
@@ -1,6 +1,6 @@
 from __future__ import annotations
 from dataclasses import dataclass, field
-from typing import Dict, List, Callable, Any
+from typing import Dict, List
 import json
 
 from chiquito.query import Queriable, Fixed
diff --git a/src/chiquito b/src/chiquito
index 4866c8f..f6a4cb0 160000
--- a/src/chiquito
+++ b/src/chiquito
@@ -1 +1 @@
-Subproject commit 4866c8f7bded04cfa7c3a21607fb28183d2230ab
+Subproject commit f6a4cb0f494d24ad6251bd13ba0d4064a42539a0