Steve/jupyter notebook tutorial part 4

pychiquito/dsl.py

@@ -22,6 +22,7 @@ def __init__(self: Circuit):
         self.ast = ASTCircuit()
         self.witness = TraceWitness()
         self.rust_ast_id = 0
+        self.num_step_instances = 0
         self.mode = CircuitMode.SETUP
         self.setup()
 
@@ -82,10 +83,21 @@ def pragma_disable_q_enable(self: Circuit) -> None:
 
     def add(self: Circuit, step_type: StepType, args: Any):
         assert self.mode == CircuitMode.Trace
+        if self.num_step_instances >= self.ast.num_steps:
+            raise ValueError(f"Number of step instances exceeds {self.ast.num_steps}")
+        self.num_step_instances += 1
         step_instance: StepInstance = step_type.gen_step_instance(args)
         self.witness.step_instances.append(step_instance)
+
+    def needs_padding(self: Circuit) -> bool:
+        return self.num_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.num_step_instances = 0
         self.mode = CircuitMode.Trace
         self.witness = TraceWitness()
         self.trace(args)

pychiquito/fibonacci.py

@@ -1,67 +1,80 @@
-from __future__ import annotations
-from typing import Tuple
-
 from dsl import Circuit, StepType
 from cb import eq
-from query import Queriable
 from util import F
+from 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))
-
-    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))
-
-
-class FiboStep(StepType):
-    def setup(self: FiboStep):
+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 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):
+class FiboStep(StepType):
+    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: 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 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, 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.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)

pychiquito/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",