Chapter 4: Fixed Signals, Lookup Tables, and Super Circuit

Chapter 4: Fixed Signals, Lookup Tables, and Super Circuit#

Lookup Tables#

It turns out that we have a whole different solution and new feature to introduce! “Lookup table” is a great feature enabled in proof systems with PLONKish arithmetization. They are composed of pre-computed constant values for circuits to “lookup to”. For example, suppose you have a single variable x and want to constrain that its value is an integer between 0 and n. While you can certainly create a constraint in the form of \((x-0)(x-1)(x-2)...(x-n) = 0\), you can alternatively create a single column lookup table with all integer values between 0 and n, and then “lookup” or try to find the value of x in the table. The witness will pass the circuit if and only if you can find x in the table, essentially constraining the value of x to between 0 to n without manually writing a lengthy constraint expression. This use case of lookup table is called range checking, and is used quite extensively in projects like the zkEVM.

Another common use of the lookup table is to provide pre-computed outputs given some inputs to a known function. A good example is bitwise operations such as xor. The following table is an example of a 2-bit xor lookup table, where a and b are two inputs and xor is the output column:

a	b	xor
00	00	00
00	01	01
00	10	10
00	11	11
01	00	01
01	01	00
01	10	11
01	11	10
10	00	10
10	01	11
10	10	00
10	11	01
11	00	11
11	01	10
11	10	01
11	11	00

When using this table, the user can lookup three columns in the witness to constrain them to one of the combinations of (a, b, xor) in the table, essentially constraining that the three witness columns satisfy the xor relationship. It’s well known that bitwise operations take many constraints in zero knowledge proofs to express. A simple operation such as xor would require decomposing the bits of a number before doing the xor. For example, an 8-bit xor would take 25-32 custom constraints. However, by using the lookup table, we can reduce this to one custom lookup constraint. Lookup tables are therefore widely used as a sub-routine in hash functions such as SHA-256, which require many bitwise operations.

Now back to why we need to use lookup table for the round constants in our MiMC7 circuit. Recall that we would need to create 92 different step types corresponding to 91 distinct round constants plus the output round. However, with the new feature, we can create a lookup table with each of the 91 round constants occupying a row and constrain that signal c for the round constant is equal to one of the 91 round constants in the table.

This still doesn’t fully satisfy our purpose, as it doesn’t constrain the order of the constants used. For example, an evil witness can pass in an arbitrary round constant or even use the same round constant across all rows, as long as it’s one of the 91 in the table.

That’s why we need to introduce another column to the table for the row number, so that the order of constants used is fixed. Together, we have a two column lookup table that looks like the following:

row number	round constant
0	0
1	20888961410941983456478427210666206549300505294776164667214940546594746570981
2	15265126113435022738560151911929040668591755459209400716467504685752745317193
3	8334177627492981984476504167502758309043212251641796197711684499645635709656
…	…
90	13602139229813231349386885113156901793661719180900395818909719758150455500533

Given this table, we need another signal row for the row number in the MiMC7 circuit. Then, we can constrain that the tuple of signals (row, c) is equal to one of the 91 rows in the lookup table. To fix the order of round constants, we need to additionally constrain that:

row == 0 for the first step instance
row + 1 = row.next for all step instances except the last

Fixed Signals#

Because lookup tables involves columns with pre-computed values that don’t change across witness assignments, they are constructed using a new type of signal called “fixed signal”, which is a concept parallel to “internal signal” and “forward signal” in Chiquito.

Super Circuits#

Furthermore, as a lookup table is fixed and can be used across multiple circuits, wouldn’t it be a waste to just construct it within one circuit? That’s why we also introduce the concept of “super circuit”, which essentially groups multiple circuits together so that they can share the inputs and outputs. You can write each circuit separately and group them as a super circuit with simple APIs in Chiquito, while we do all the backend work to convert the super circuit into one giant Halo2 circuit behind the scenes (with more backends to be enabled in the future).

Putting Them All Together#

Well. Lookup tables, fixed signals, and super circuits. They are quite a mouthful! Putting these all together, we will first construct a lookup table in a singleton circuit, whose only content is the lookup table, so that it can be later shared across other circuits in the super circuit. For now, the super circuit will only contain this lookup table circuit (which we will call the MiMC7Constants circuit) AND the MiMC7Circuit main circuit that we constructed in prior chapters.

MiMC7Constants Sub-Circuit for Lookup Table#

Let’s construct the Mimc7Constants sub-circuit! A sub-circuit is no different from a regular circuit, except that we will group them to a super circuit at the end. Therefore, it also has the setup() and wg() functions we need to define. However, because there’s only a lookup table containing only fixed signals in the Mimc7Constants sub-circuit that we are creating, no wg() function is needed for witness generation. Instead, we need to define the fixed_gen() function that assigns values to the fixed signals, similar to how we assign values to internal and forward signals in wg() previously.

Now let’s first define the setup() function and you can refer to the code snippet below. Recall that we instantiated forward signals on the circuit level in the setup() function. We will also do the same for fixed signals, by invoking the self.fixed() function and appending it to the cicuit object like self.lookup_row = self.fixed("constant row"). Here, the signal object is named lookup_row and appended to the circuit, with “constant row” as its annotation. We create another fixed signal for the round constants and append it to the circuit as self.lookup_c.

Next, also under setup(), we need to group the two signals into a lookup table, by calling self.new_table(). The function takes a table object, which is initiated by calling table(). We can then append signals to the table using add(), which takes the signals to append. add() is called as many times as the number of signals to append and therefore is called twice for fixed signals self.lookup_row and self.lookup_c. Finally, we append the lookup table to the circuit as well by assigning it to self.lookup_table. In summary, table() initiates the lookup table, add() appends fixed signals to it, new_table() adds the lookup table, and we assign the result to self.lookup_table or any name you want to assign the table to.

Here’s the complete setup() function we defined for Mimc7Constants sub-circuit:

class Mimc7Constants(Circuit):
    def setup(self):
        self.pragma_num_steps(ROUNDS)
        self.lookup_row = self.fixed("constant row")
        self.lookup_c = self.fixed("constant value")
        self.lookup_table = self.new_table(
            table().add(self.lookup_row).add(self.lookup_c)
        )

    def fixed_gen(self):
        # TODO

Now let’s assign values to fixed signals in the lookup table by defining fixed_gen() for the sub-circuit. The assign function does exactly this via self.assign(offset, lhs, rhs). Here, offset is the index of the assignment in a fixed signal to assign value to. You can think of this as the row number of a fixed signal column in a lookup table. lhs is the fixed signal to assign to. rhs is the value to assign, i.e. a field element. The code snippet below loops through the ROUND_CONSTANTS array and calls self.assign for both self.lookup_row and self.lookup_c signals.

You might recall that self.assign() is also an API under the wg() witness generation function, and it only takes two parameters as self.assign(lhs, rhs) without the offset parameter. This is because wg() is specific to a step instance, and therefore we are assigning the rhs value to the lhs signal of a specific step instance. Contrarily, because lookup tables are on the circuit level, we require the offset parameter to assign a specific index of a fixed signal.

Here’s the fixed_gen() function we defined for Mimc7Constants sub-circuit:

class Mimc7Constants(Circuit):
    def setup(self):
        # ...

    def fixed_gen(self):
        for i, round_key in enumerate(ROUND_CONSTANTS):
            self.assign(i, self.lookup_row, F(i))
            self.assign(i, self.lookup_c, F(round_key))

Modifications to MiMC7Circuit Sub-Circuit#

Now, let’s make necessary modifications to the Mimc7Circuit sub-circuit, the circuit we created in prior chapters, so that we can lookup witness values to the lookup table we just created. We already have the c internal signal corresponding to the round constants that can lookup to the lookup_c fixed signal in the table. Therefore, we need another row signal to lookup to the lookup_row fixed signal in the table. Because recall that we also need to constrain that row = row.next for all step instances except the last, row needs to be a forward signal at the circuit level with transition constraints.

You might be wondering why do we need two fixed signals lookup_c lookup_row for the lookup table AND two internal/forward signals c row for the main circuit. Isn’t that duplicated? The reason is that c and row are signals for the witness where as lookup_c and lookup_row are signals for the table and we are constraining that (c, row) tuples we see in the witness appear in (lookup_c, lookup_row) tuples in the lookup table. In general, for n signals to lookup, we need n signals in the witness and another n signals in the lookup table, for a total of 2n signals.

With that settled, recall that from prior chapters, we have two step types, Mimc7Step and Mimc7LastStep. However, we need the additional constraint that row == 0 for the first step instance only. Therefore, we need another step type Mimc7FirstStep, which is the same as Mimc7Step plus this additional constraint. We also need to constrain that row == row.next for both Mimc7FirstStep and Mimc7Step, not to mention that we also need to assign value for this new row signal in wg() for both step types. New contents for Mimc7FirstStep compared to our prior chapters is listed in the code snippet below with prior contents abbreviated:

class Mimc7FirstStep(StepType):
    def setup(self):
        # ...
        self.transition(eq(self.circuit.row, 0))
        self.transition(eq(self.circuit.row + 1, self.circuit.row.next()))

        # TODO: lookup to table

    def wg(self, x_value, k_value, c_value, row_value):
        # ...
        self.assign(self.circuit.row, F(row_value))

Take a look at the code snippet below for the following contents. Now, although we have constructed the lookup table in another Mimc7Constants sub-circuit, we still need to “lookup” to that table from this Mimc7Circuits sub-circuit, because creating the table is different from using the table. The self.add_lookup() function accomplishes this by taking one parameter. Inside this parameter, we need to first grab the lookup table we created in Mimc7Constants sub-circuit, but how to refer to a variable from another sub-circuit? The answer is that we cannot yet and would need the super circuit to do the trick. However, we do intend to grab this lookup table from another sub-circuit and store it as a circuit-level variable in the Mimc7Constants circuit that our step type resides in. Let’s say that we eventually call this circuit-level lookup table variable constants_table. Therefore, inside the setup() for Mimc7FirstStep, we can refer to it as self.circuit.constants_table.

Next, we need to “lookup” the witness signals to the fixed signals in the table, accomplished through the apply() function. apply() function takes one parameter that’s the witness signal to lookup, and can be chain-called multiple times. apply() is called twice for the witness forward signal self.circuit.row and the witness internal signal self.c. Make sure to call apply() the same order that the fixed signals were added in the table. That is, we added fixed signals lookup_row first and then lookup_c by calling table().add(self.lookup_row).add(self.lookup_c) and therefore we need to apply signals row first and then c.

See below for the full syntax. These APIs for looking up the lookup table are quite convenient, as we can lookup to the same lookup table multiple times, even with different witness signals. Note that we need to call self.add_lookup() for both Mimc7FirstStep and Mimc7Step. The following only spelled out the lookup for Mimc7FirstStep because it’s identical in Mimc7Step.

class Mimc7FirstStep(StepType):
    def setup(self):
        # ...

        self.add_lookup(
            self.circuit.constants_table.apply(self.circuit.row).apply(self.c)
        )

Putting together constraints and assignments for the new row signal as well as looking up to the lookup table, we have the complete Mimc7FirstStep as the following. Mimc7Step is the same except that it doesn’t have the row == 0 constraint:

class Mimc7FirstStep(StepType):
    def setup(self):
        self.xkc = self.internal("xkc")
        self.y = self.internal("y")
        self.c = self.internal("c")

        self.constr(eq(self.circuit.x + self.circuit.k + self.c, self.xkc))
        self.constr(
            eq(
                self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc,
                self.y,
            )
        )

        self.transition(eq(self.y, self.circuit.x.next()))
        self.transition(eq(self.circuit.k, self.circuit.k.next()))
        self.transition(eq(self.circuit.row, 0))
        self.transition(eq(self.circuit.row + 1, self.circuit.row.next()))

        self.add_lookup(
            self.circuit.constants_table.apply(self.circuit.row).apply(self.c)
        )

    def wg(self, x_value, k_value, c_value, row_value):
        self.assign(self.circuit.x, F(x_value))
        self.assign(self.circuit.k, F(k_value))
        self.assign(self.c, F(c_value))
        self.assign(self.circuit.row, F(row_value))

        xkc_value = F(x_value + k_value + c_value)
        self.assign(self.xkc, F(xkc_value))
        self.assign(self.y, F(xkc_value**7))

We also need to modify Mimc7LastStep, the step type for the output row, by assigning value to the row signal. You might wonder why this is needed even though Mimc7LastStep has no constraints for row? This is because we have the constraint row + 1 == row.next in the prior step instance and therefore need to assign an incremental value for row in the last step instance.

The modified Mimc7LastStep is as the following:

class Mimc7LastStep(StepType):
    def setup(self):
        self.out = self.internal("out")

        self.constr(eq(self.circuit.x + self.circuit.k, self.out))

    def wg(self, x_value, k_value, _, row_value):
        self.assign(self.circuit.x, F(x_value))
        self.assign(self.circuit.k, F(k_value))
        self.assign(self.circuit.row, F(row_value))
        self.assign(self.out, F(x_value + k_value))

Finally, we need to add the row forward signal at the circuit level, instantiate and append Mimc7FirstStep to the circuit, and constrain the first step instance to self.mimc7_first_step. We also need to modify the trace function to feed in assignments for the row forward signal as well. All changes are documented below, with prior contents abbreviated.

class Mimc7Circuit(Circuit):
    def setup(self):
        # ...

        self.row = self.forward("row")

        self.mimc7_first_step = self.step_type(Mimc7FirstStep(self, "mimc7_first_step"))

        self.pragma_first_step(self.mimc7_first_step)

    def trace(self, x_in_value, k_value):
        # ...
        row_value = F(0)

        self.add(self.mimc7_first_step, x_value, k_value, c_value, row_value)

        for i in range(1, ROUNDS):
            # ...
            row_value += F(1)

            self.add(self.mimc7_step, x_value, k_value, c_value, row_value)

        # ...
        row_value += F(1)

        self.add(self.mimc7_last_step, x_value, k_value, c_value, row_value)

Constructing the Super Circuit#

So far, we are done implementing two sub-circuits, Mimc7Constants which has the lookup table and Mimc7Circuit which wires up the core circuit logics. It’s time to combine them into a super circuit!

Recall at the start of the chapter that super circuit is useful for wiring inputs and outputs among multiple sub-circuits and in our case of using a lookup table, it’s often the best practice to store the table in one sub-circuit, so that it can be used across multiple other sub-circuits.

Refer to the code snippet below for the following contents. First we need to create the super circuit. Chiquito again provides convenient APIs, so that you can just inherit the SuperCircuit class, just as how you created a Circuit. Similarly, SuperCircuit requires the user to define two functions:

setup() instantiates sub-circuits and append them to the super circuit.
mapping() generates a super-witness which contains multiple witnesses, each for a sub-circuit that require a witness.

Let’s talk about setup() first. TO create a sub-circuit, we call the self.sub_circuit() function, which takes one parameter that’s the instantiated sub-circuit. Sub-circuit instantiation takes an unlimited number of optional parameters. The first optional parameter must be super_circuit and all other optional parameters can be arbitrary named inputs to be stored under the sub-circuit.

Taking the sub-circuit instantiation Mimc7Constants(self) for example, it only takes one optional parameter, and therefore must be the super_circuit. Because it’s instantiated under the Mimc7SuperCircuit, self simply refers to the super circuit.

Taking the other sub-circuit instantiation Mimc7Circuit(self, constants_table=self.mimc7_constants.lookup_table) for example, it takes two optional parameters, the first again being the super_circuit=self, and the second a named parameter constants_table, which points to self.lookup_table from the Mimc7Constants sub-circuit that we defined at the start of this chapter. Because we named the lookup table constants_table when instantiating Mimc7Circuit, constants_table is the name that the lookup table will be referred to within Mimc7Circuit. It’s a circuit level variable that is referred to as self.constants_table at the circuit level or self.circuit.constants_table at the step type level, which is indeed what we did when looking up to the lookup table inside a step type, i.e. self.add_lookup(self.circuit.constants_table.apply(self.circuit.row).apply(self.c)).

Because sub-circuit instantiation can take as many arbitrary parameters as we want, we can even pass in additional lookup tables or any input types, as long as they are named arguments, which is required because we need to refer to some name inside the sub-circuit.

In summary, the super circuit setup() is constructed as such:

class Mimc7SuperCircuit(SuperCircuit):
    def setup(self):
        self.mimc7_constants = self.sub_circuit(Mimc7Constants(self))
        self.mimc7_circuit = self.sub_circuit(
            Mimc7Circuit(self, constants_table=self.mimc7_constants.lookup_table)
        )

    def mapping(self, x_in_value, k_value):
        # TODO

Now we define mapping() for the super circuit, which generates a super-witness that contains multiple witnesses, each for a sub-circuit that requires a witness. Again, refer to the code snippet below. Inside mapping(), we call map() for each sub-circuit that needs a witness, and this map() function essentially calls the trace() function defined under the sub-circuit. If we further go down the pipeline and recall from the Fibonacci tutorial, inside trace(), we call add() each time we add a step instance, and this add() function essentially calls the wg() function defined under the corresponding step type. In summary:

super circuit level:

mapping() is defined by the user
mapping() calls map() for each sub-circuit that requires a witness
map() invokes trace() under sub-circuit
Therefore, map() and trace() must have the same optional parameters

sub-circuit level:

trace() is defined by the user
trace() calls add() for each step instance added
add() invokes wg() under step type
Therefore, add() and wg() must have the same optional parameters

step-type level:

wg() is defined by the user
wg() calls assign() for each signal value assigned

Because we call map() for each sub-circuit that requires a witness and because Mimc7Constants simply constructs the lookup table with fixed signals but no witness, we only need to call map() once for Mimc7Circuit, which we appended to the super circuit as self.mimc7_circuit in setup(). Because map() invokes trace() under sub-circuit, we need to make sure that they have the same optional parameters, i.e. x_in_value and k_value. Scroll above or to the prior chapter to confirm that trace() indeed only have x_in_value and k_value as the optional parameters. Similarly, because add() invokes wg() under step type, we need to make sure that they have the same optional parameters as well for the same step type. Again, you can confirm this with any circuits from this or prior chapters.

Here’s our mapping() implementation for Mimc7SuperCircuit:

class Mimc7SuperCircuit(SuperCircuit):
    def setup(self):
        # ...

    def mapping(self, x_in_value, k_value):
        self.map(self.mimc7_circuit, x_in_value, k_value)

Putting Everything Together#

You’ve progressed this far! Finally, it’s time to put everything, lookup tables, fixed signals, new sub-circuit, and super circuit, together.

from __future__ import annotations
from chiquito.dsl import SuperCircuit, Circuit, StepType
from chiquito.cb import eq, table
from chiquito.util import F


ROUNDS = 91

ROUND_CONSTANTS = [
    0,
    20888961410941983456478427210666206549300505294776164667214940546594746570981,
    15265126113435022738560151911929040668591755459209400716467504685752745317193,
    8334177627492981984476504167502758309043212251641796197711684499645635709656,
    1374324219480165500871639364801692115397519265181803854177629327624133579404,
    11442588683664344394633565859260176446561886575962616332903193988751292992472,
    2558901189096558760448896669327086721003508630712968559048179091037845349145,
    11189978595292752354820141775598510151189959177917284797737745690127318076389,
    3262966573163560839685415914157855077211340576201936620532175028036746741754,
    17029914891543225301403832095880481731551830725367286980611178737703889171730,
    4614037031668406927330683909387957156531244689520944789503628527855167665518,
    19647356996769918391113967168615123299113119185942498194367262335168397100658,
    5040699236106090655289931820723926657076483236860546282406111821875672148900,
    2632385916954580941368956176626336146806721642583847728103570779270161510514,
    17691411851977575435597871505860208507285462834710151833948561098560743654671,
    11482807709115676646560379017491661435505951727793345550942389701970904563183,
    8360838254132998143349158726141014535383109403565779450210746881879715734773,
    12663821244032248511491386323242575231591777785787269938928497649288048289525,
    3067001377342968891237590775929219083706800062321980129409398033259904188058,
    8536471869378957766675292398190944925664113548202769136103887479787957959589,
    19825444354178182240559170937204690272111734703605805530888940813160705385792,
    16703465144013840124940690347975638755097486902749048533167980887413919317592,
    13061236261277650370863439564453267964462486225679643020432589226741411380501,
    10864774797625152707517901967943775867717907803542223029967000416969007792571,
    10035653564014594269791753415727486340557376923045841607746250017541686319774,
    3446968588058668564420958894889124905706353937375068998436129414772610003289,
    4653317306466493184743870159523234588955994456998076243468148492375236846006,
    8486711143589723036499933521576871883500223198263343024003617825616410932026,
    250710584458582618659378487568129931785810765264752039738223488321597070280,
    2104159799604932521291371026105311735948154964200596636974609406977292675173,
    16313562605837709339799839901240652934758303521543693857533755376563489378839,
    6032365105133504724925793806318578936233045029919447519826248813478479197288,
    14025118133847866722315446277964222215118620050302054655768867040006542798474,
    7400123822125662712777833064081316757896757785777291653271747396958201309118,
    1744432620323851751204287974553233986555641872755053103823939564833813704825,
    8316378125659383262515151597439205374263247719876250938893842106722210729522,
    6739722627047123650704294650168547689199576889424317598327664349670094847386,
    21211457866117465531949733809706514799713333930924902519246949506964470524162,
    13718112532745211817410303291774369209520657938741992779396229864894885156527,
    5264534817993325015357427094323255342713527811596856940387954546330728068658,
    18884137497114307927425084003812022333609937761793387700010402412840002189451,
    5148596049900083984813839872929010525572543381981952060869301611018636120248,
    19799686398774806587970184652860783461860993790013219899147141137827718662674,
    19240878651604412704364448729659032944342952609050243268894572835672205984837,
    10546185249390392695582524554167530669949955276893453512788278945742408153192,
    5507959600969845538113649209272736011390582494851145043668969080335346810411,
    18177751737739153338153217698774510185696788019377850245260475034576050820091,
    19603444733183990109492724100282114612026332366576932662794133334264283907557,
    10548274686824425401349248282213580046351514091431715597441736281987273193140,
    1823201861560942974198127384034483127920205835821334101215923769688644479957,
    11867589662193422187545516240823411225342068709600734253659804646934346124945,
    18718569356736340558616379408444812528964066420519677106145092918482774343613,
    10530777752259630125564678480897857853807637120039176813174150229243735996839,
    20486583726592018813337145844457018474256372770211860618687961310422228379031,
    12690713110714036569415168795200156516217175005650145422920562694422306200486,
    17386427286863519095301372413760745749282643730629659997153085139065756667205,
    2216432659854733047132347621569505613620980842043977268828076165669557467682,
    6309765381643925252238633914530877025934201680691496500372265330505506717193,
    20806323192073945401862788605803131761175139076694468214027227878952047793390,
    4037040458505567977365391535756875199663510397600316887746139396052445718861,
    19948974083684238245321361840704327952464170097132407924861169241740046562673,
    845322671528508199439318170916419179535949348988022948153107378280175750024,
    16222384601744433420585982239113457177459602187868460608565289920306145389382,
    10232118865851112229330353999139005145127746617219324244541194256766741433339,
    6699067738555349409504843460654299019000594109597429103342076743347235369120,
    6220784880752427143725783746407285094967584864656399181815603544365010379208,
    6129250029437675212264306655559561251995722990149771051304736001195288083309,
    10773245783118750721454994239248013870822765715268323522295722350908043393604,
    4490242021765793917495398271905043433053432245571325177153467194570741607167,
    19596995117319480189066041930051006586888908165330319666010398892494684778526,
    837850695495734270707668553360118467905109360511302468085569220634750561083,
    11803922811376367215191737026157445294481406304781326649717082177394185903907,
    10201298324909697255105265958780781450978049256931478989759448189112393506592,
    13564695482314888817576351063608519127702411536552857463682060761575100923924,
    9262808208636973454201420823766139682381973240743541030659775288508921362724,
    173271062536305557219323722062711383294158572562695717740068656098441040230,
    18120430890549410286417591505529104700901943324772175772035648111937818237369,
    20484495168135072493552514219686101965206843697794133766912991150184337935627,
    19155651295705203459475805213866664350848604323501251939850063308319753686505,
    11971299749478202793661982361798418342615500543489781306376058267926437157297,
    18285310723116790056148596536349375622245669010373674803854111592441823052978,
    7069216248902547653615508023941692395371990416048967468982099270925308100727,
    6465151453746412132599596984628739550147379072443683076388208843341824127379,
    16143532858389170960690347742477978826830511669766530042104134302796355145785,
    19362583304414853660976404410208489566967618125972377176980367224623492419647,
    1702213613534733786921602839210290505213503664731919006932367875629005980493,
    10781825404476535814285389902565833897646945212027592373510689209734812292327,
    4212716923652881254737947578600828255798948993302968210248673545442808456151,
    7594017890037021425366623750593200398174488805473151513558919864633711506220,
    18979889247746272055963929241596362599320706910852082477600815822482192194401,
    13602139229813231349386885113156901793661719180900395818909719758150455500533,
]


class Mimc7Constants(Circuit):
    def setup(self):
        self.pragma_num_steps(ROUNDS)
        self.lookup_row = self.fixed("constant row")
        self.lookup_c = self.fixed("constant value")
        self.lookup_table = self.new_table(
            table().add(self.lookup_row).add(self.lookup_c)
        )

    def fixed_gen(self):
        for i, round_key in enumerate(ROUND_CONSTANTS):
            self.assign(i, self.lookup_row, F(i))
            self.assign(i, self.lookup_c, F(round_key))


class Mimc7FirstStep(StepType):
    def setup(self):
        self.xkc = self.internal("xkc")
        self.y = self.internal("y")
        self.c = self.internal("c")

        self.constr(eq(self.circuit.x + self.circuit.k + self.c, self.xkc))
        self.constr(
            eq(
                self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc,
                self.y,
            )
        )

        self.transition(eq(self.y, self.circuit.x.next()))
        self.transition(eq(self.circuit.k, self.circuit.k.next()))
        self.transition(eq(self.circuit.row, 0))
        self.transition(eq(self.circuit.row + 1, self.circuit.row.next()))

        self.add_lookup(
            self.circuit.constants_table.apply(self.circuit.row).apply(self.c)
        )

    def wg(self, x_value, k_value, c_value, row_value):
        self.assign(self.circuit.x, F(x_value))
        self.assign(self.circuit.k, F(k_value))
        self.assign(self.c, F(c_value))
        self.assign(self.circuit.row, F(row_value))

        xkc_value = F(x_value + k_value + c_value)
        self.assign(self.xkc, F(xkc_value))
        self.assign(self.y, F(xkc_value**7))


class Mimc7Step(StepType):
    def setup(self):
        self.xkc = self.internal("xkc")
        self.y = self.internal("y")
        self.c = self.internal("c")

        self.constr(eq(self.circuit.x + self.circuit.k + self.c, self.xkc))
        self.constr(
            eq(
                self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc
                * self.xkc,
                self.y,
            )
        )

        self.transition(eq(self.y, self.circuit.x.next()))
        self.transition(eq(self.circuit.k, self.circuit.k.next()))
        self.transition(eq(self.circuit.row + 1, self.circuit.row.next()))

        self.add_lookup(
            self.circuit.constants_table.apply(self.circuit.row).apply(self.c)
        )

    def wg(self, x_value, k_value, c_value, row_value):
        self.assign(self.circuit.x, F(x_value))
        self.assign(self.circuit.k, F(k_value))
        self.assign(self.c, F(c_value))
        self.assign(self.circuit.row, F(row_value))

        xkc_value = F(x_value + k_value + c_value)
        self.assign(self.xkc, F(xkc_value))
        self.assign(self.y, F(xkc_value**7))


class Mimc7LastStep(StepType):
    def setup(self):
        self.out = self.internal("out")

        self.constr(eq(self.circuit.x + self.circuit.k, self.out))

    def wg(self, x_value, k_value, _, row_value):
        self.assign(self.circuit.x, F(x_value))
        self.assign(self.circuit.k, F(k_value))
        self.assign(self.circuit.row, F(row_value))
        self.assign(self.out, F(x_value + k_value))


class Mimc7Circuit(Circuit):
    def setup(self):
        self.x = self.forward("x")
        self.k = self.forward("k")
        self.row = self.forward("row")

        self.mimc7_first_step = self.step_type(Mimc7FirstStep(self, "mimc7_first_step"))
        self.mimc7_step = self.step_type(Mimc7Step(self, "mimc7_step"))
        self.mimc7_last_step = self.step_type(Mimc7LastStep(self, "mimc7_last_step"))

        self.pragma_first_step(self.mimc7_first_step)
        self.pragma_last_step(self.mimc7_last_step)
        self.pragma_num_steps(ROUNDS + 2 - 1)

    def trace(self, x_in_value, k_value):
        c_value = F(ROUND_CONSTANTS[0])
        x_value = F(x_in_value)
        row_value = F(0)

        self.add(self.mimc7_first_step, x_value, k_value, c_value, row_value)

        for i in range(1, ROUNDS):
            row_value += F(1)
            x_value += F(k_value + c_value)
            x_value = F(x_value**7)
            c_value = F(ROUND_CONSTANTS[i])

            self.add(self.mimc7_step, x_value, k_value, c_value, row_value)

        row_value += F(1)
        x_value += F(k_value + c_value)
        x_value = F(x_value**7)

        self.add(self.mimc7_last_step, x_value, k_value, c_value, row_value)


class Mimc7SuperCircuit(SuperCircuit):
    def setup(self):
        self.mimc7_constants = self.sub_circuit(Mimc7Constants(self))
        self.mimc7_circuit = self.sub_circuit(
            Mimc7Circuit(self, constants_table=self.mimc7_constants.lookup_table)
        )

    def mapping(self, x_in_value, k_value):
        self.map(self.mimc7_circuit, x_in_value, k_value)

Similar to a regular circuit, we first instantiate the supercircuit, then invoke the gen_witness function with parameters that match the mapping() function to create the super witness, and finally feed the super witness to the halo2_mock_prover. Here we are feeding in an input message value of x_in_value = F(1) and the key value of k_value = F(2). A successful run should give you an Ok(()) print out.

mimc7 = Mimc7SuperCircuit()
mimc7_super_witness = mimc7.gen_witness(F(1), F(2))
mimc7.halo2_mock_prover(mimc7_super_witness)

Voila! In this chapter, we started from the hypothetical scenario where the evil witness inputs arbitrary round constant value. We constructed a lookup table with 2 columns using 2 fixed signals and put this lookup table within a sub-circuit so that it can be used across other sub-circuits. We added the row signal to our original circuit, now also a sub-circuit, so that the ordering of the round constants are ensured. To achieve this, we are required to add an additional step type for the first step instance to constrain row == 0, and added additional constraints for row in other step types. We additionally also needed to modify the wg() and trace() function to reflect the row signal addition in witness assignment and step instantiation. Finally, we grouped both sub-circuits in a super circuit, and invoked the mapping() function to create a super witness, which only contains a witness for the Mimc7Circuit sub-circuit.

That’s a lot you’ve learned from this chapter alone! Now that you finished the entire Chiquito tutorial series and just became a newly minted Chiquito expert :)

a	b	xor
00	00	00
00	01	01
00	10	10
00	11	11
01	00	01
01	01	00
01	10	11
01	11	10
10	00	10
10	01	11
10	10	00
10	11	01
11	00	11
11	01	10
11	10	01
11	11	00

a	b	xor
00	00	00
00	01	01
00	10	10
00	11	11
01	00	01
01	01	00
01	10	11
01	11	10
10	00	10
10	01	11
10	10	00
10	11	01
11	00	11
11	01	10
11	10	01
11	11	00