diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 4e4e003..7e611d7 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -11,3 +11,6 @@ - [Multipoint opening argument](design/multipoint-opening.md) - [Permutation argument](design/permutation.md) - [Lookup argument](design/lookup-argument.md) + - [Gadgets](design/gadgets.md) + - [SHA-256](design/gadgets/sha256.md) + - [16-bit table chip](design/gadgets/sha256/table16.md) diff --git a/book/src/design/gadgets.md b/book/src/design/gadgets.md new file mode 100644 index 0000000..a4bab16 --- /dev/null +++ b/book/src/design/gadgets.md @@ -0,0 +1,3 @@ +# Gadgets + +In this section we document the gadgets and chip designs provided by halo2. diff --git a/book/src/design/gadgets/sha256.md b/book/src/design/gadgets/sha256.md new file mode 100644 index 0000000..daff12f --- /dev/null +++ b/book/src/design/gadgets/sha256.md @@ -0,0 +1,56 @@ +# SHA-256 + +## Specification + +SHA-256 is specified in [NIST FIPS PUB 180-4](https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf). + +Unlike the specification, we use $\boxplus$ for addition modulo $2^{32}$, and $+$ for +field addition. $\oplus$ is used for XOR. + +## Gadget interface + +SHA-256 maintains state in eight 32-bit variables. It processes input as 512-bit blocks, +but internally splits these blocks into 32-bit chunks. We therefore designed the SHA-256 +gadget to consume input in 32-bit chunks. + +## Chip instructions + +The SHA-256 gadget requires a chip with the following instructions: + +```rust +pub trait Sha256Instructions: Chip { + /// Variable representing the SHA-256 internal state. + type State: Clone + fmt::Debug; + /// Variable representing a 32-bit word of the input block to the SHA-256 compression + /// function. + type BlockWord: Copy + fmt::Debug; + + /// Places the SHA-256 IV in the circuit, returning the initial state variable. + fn initialization_vector(layouter: &mut impl Layouter) -> Result; + + /// Starting from the given initial state, processes a block of input and returns the + /// final state. + fn compress( + layouter: &mut impl Layouter, + initial_state: &Self::State, + input: [Self::BlockWord; BLOCK_SIZE], + ) -> Result; + + /// Converts the given state into a message digest. + fn digest( + layouter: &mut impl Layouter, + state: &Self::State, + ) -> Result<[Self::BlockWord; DIGEST_SIZE], Error>; +} +``` + +TODO: Add instruction for computing padding. + +This set of instructions was chosen to strike a balance between the reusability of the +instructions, and the scope for chips to internally optimise them. In particular, we +considered splitting the compression function into its constituent parts (Ch, Maj etc), +and providing a compression function gadget that implemented the round logic. However, +this would prevent chips from using relative references between the various parts of a +compression round. Having an instruction that implements all compression rounds is also +similar to the Intel SHA extensions, which provide an instruction that performs multiple +compression rounds. diff --git a/book/src/design/gadgets/sha256/bit_reassignment.png b/book/src/design/gadgets/sha256/bit_reassignment.png new file mode 100644 index 0000000..faf495c Binary files /dev/null and b/book/src/design/gadgets/sha256/bit_reassignment.png differ diff --git a/book/src/design/gadgets/sha256/compression.png b/book/src/design/gadgets/sha256/compression.png new file mode 100644 index 0000000..fc0c4a3 Binary files /dev/null and b/book/src/design/gadgets/sha256/compression.png differ diff --git a/book/src/design/gadgets/sha256/low_sigma_0.png b/book/src/design/gadgets/sha256/low_sigma_0.png new file mode 100644 index 0000000..60a3236 Binary files /dev/null and b/book/src/design/gadgets/sha256/low_sigma_0.png differ diff --git a/book/src/design/gadgets/sha256/low_sigma_1.png b/book/src/design/gadgets/sha256/low_sigma_1.png new file mode 100644 index 0000000..1624182 Binary files /dev/null and b/book/src/design/gadgets/sha256/low_sigma_1.png differ diff --git a/book/src/design/gadgets/sha256/table16.md b/book/src/design/gadgets/sha256/table16.md new file mode 100644 index 0000000..2f8264c --- /dev/null +++ b/book/src/design/gadgets/sha256/table16.md @@ -0,0 +1,901 @@ +# 16-bit table chip for SHA-256 + +This chip implementation is based around a single 16-bit lookup table. It requires a +minimum of $2^{16}$ circuit rows, and is therefore suitable for use in larger circuits. + +We target a maximum constraint degree of $9$. That will allow us to handle constraining +carries and "small pieces" to a range of up to $\{0..7\}$ in one row. + +## Compression round + +There are $64$ compression rounds. Each round takes 32-bit values $A, B, C, D, E, F, G, H$ +as input, and performs the following operations: + +$$ +\begin{array}{rcl} +Ch(E, F, G) &=& (E \wedge F) \oplus (¬E \wedge G) \\ +Maj(A, B, C) &=& (A \wedge B) \oplus (A \wedge C) \oplus (B \wedge C) \\ + &=& count(A, B, C) \geq 2 \\ +\Sigma_0(A) &=& (A ⋙ 2) \oplus (A ⋙ 13) \oplus (A ⋙ 22) \\ +\Sigma_1(E) &=& (E ⋙ 6) \oplus (E ⋙ 11) \oplus (E ⋙ 25) \\ +H' &=& H + Ch(E, F, G) + \Sigma_1(E) + K_t + W_t \\ +E_{new} &=& reduce_6(H' + D) \\ +A_{new} &=& reduce_7(H' + Maj(A, B, C) + \Sigma_0(A)) +\end{array} +$$ + +where $reduce_i$ must handle a carry in $\{0, \ldots, i-1\}$. + +![The SHA-256 compression function](./compression.png) + +Define $\mathtt{spread}$ as a table mapping a $16$-bit input to an output interleaved with +zero bits. We do not require a separate table for range checks because $\mathtt{spread}$ +can be used. + +### Modular addition + +To implement addition modulo $2^{32}$, we note that this is equivalent to adding the +operands using field addition, and then masking away all but the lowest 32 bits of the +result. For example, if we have two operands $a$ and $b$: + +$$a \boxplus b = c,$$ + +we decompose each operand (along with the result) into 16-bit chunks: + +$$(a_L : \mathbb{Z}_{2^{16}}, a_H : \mathbb{Z}_{2^{16}}) \boxplus (b_L : \mathbb{Z}_{2^{16}}, b_H : \mathbb{Z}_{2^{16}}) = (c_L : \mathbb{Z}_{2^{16}}, c_H : \mathbb{Z}_{2^{16}}),$$ + +and then reformulate the constraint using field addition: + +$$\mathsf{carry} \cdot 2^{32} + c_H \cdot 2^{16} + c_L = (a_H + b_H) \cdot 2^{16} + a_L + b_L.$$ + +More generally, any bit-decomposition of the output can be used, not just a decomposition +into 16-bit chunks. Note that this correctly handles the carry from $a_L + b_L$. + +This constraint requires that each chunk is correctly range-checked (or else an assignment +could overflow the field). + +- The operand and result chunks can be constrained using $\mathtt{spread}$, by looking up + each chunk in the "dense" column within a subset of the table. This way we additionally + get the "spread" form of the output for free; in particular this is true for the output + of the bottom-right $\boxplus$ which becomes $A_{new}$, and the output of the leftmost + $\boxplus$ which becomes $E_{new}$. We will use this below to optimize $Maj$ and $Ch$. + +- $\mathsf{carry}$ must be constrained to the precise range of allowed carry values for + the number of operands. We do this with a + [small range constraint](../../../user/tips-and-tricks.md#small-range-constraints). + +### Maj function + +$Maj$ can be done in $4$ lookups: $2\; \mathtt{spread} * 2$ chunks + +- As mentioned above, after the first round we already have $A$ in spread form $A'$. + Similarly, $B$ and $C$ are equal to the $A$ and $B$ respectively of the previous round, + and therefore in the steady state we already have them in spread form $B'$ and $C'$. In + fact we can also assume we have them in spread form in the first round, either from the + fixed IV or from the use of $\mathtt{spread}$ to reduce the output of the feedforward in + the previous block. +- Add the spread forms in the field: $M' = A' + B' + C'$; + - We can add them as $32$-bit words or in pieces; it's equivalent +- Witness the compressed even bits $M^{even}_i$ and the compressed odd bits $M^{odd}_i$ for $i = \{0..1\}$; +- Constrain $M' = \mathtt{spread}(M^{even}_0) + 2 \cdot \mathtt{spread}(M^{odd}_0) + 2^{32} \cdot \mathtt{spread}(M^{even}_1) + 2^{33} \cdot \mathtt{spread}(M^{odd}_1)$, where $M^{odd}_i$ is the $Maj$ function output. + +> Note: by "even" bits we mean the bits of weight an even-power of $2$, i.e. of weight +> $2^0, 2^2, \ldots$. Similarly by "odd" bits we mean the bits of weight an odd-power of +> $2$. + +### Ch function +> TODO: can probably be optimised to $4$ or $5$ lookups using an additional table. +> +$Ch$ can be done in $8$ lookups: $4\; \mathtt{spread} * 2$ chunks + +- As mentioned above, after the first round we already have $E$ in spread form $E'$. + Similarly, $F$ and $G$ are equal to the $E$ and $F$ respectively of the previous round, + and therefore in the steady state we already have them in spread form $F'$ and $G'$. In + fact we can also assume we have them in spread form in the first round, either from the + fixed IV or from the use of $\mathtt{spread}$ to reduce the output of the feedforward in + the previous block. +- Calculate $P' = E' + F'$ and $Q' = (evens - E') + G'$, where $evens = \mathtt{spread}(2^{32} - 1)$. + - We can add them as $32$-bit words or in pieces; it's equivalent. + - $evens - E'$ works to compute the spread of $¬E$ even though negation and + $\mathtt{spread}$ do not commute in general. It works because each spread bit in $E'$ + is subtracted from $1$, so there are no borrows. +- Witness $P^{even}_i, P^{odd}_i, Q^{even}_i, Q^{odd}_i$ such that + $P' = \mathtt{spread}(P^{even}_0) + 2 \cdot \mathtt{spread}(P^{odd}_0) + 2^{32} \cdot \mathtt{spread}(P^{even}_1) + 2^{33} \cdot \mathtt{spread}(P^{odd}_1)$, and similarly for $Q'$. +- $\{P^{odd}_i + Q^{odd}_i\}_{i=0..1}$ is the $Ch$ function output. + +### Σ_0 function + +$\Sigma_0(A)$ can be done in $6$ lookups. + +To achieve this we first split $A$ into pieces $(a, b, c, d)$, of lengths $(2, 11, 9, 10)$ +bits respectively counting from the little end. At the same time we obtain the spread +forms of these pieces. This can all be done in two PLONK rows, because the $10$ and +$11$-bit pieces can be handled using $\mathtt{spread}$ lookups, and the $9$-bit piece can +be split into $3 * 3$-bit subpieces. The latter and the remaining $2$-bit piece can be +range-checked by polynomial constraints in parallel with the two lookups, two small pieces +in each row. The spread forms of these small pieces are found by interpolation. + +Note that the splitting into pieces can be combined with the reduction of $A_{new}$, i.e. +no extra lookups are needed for the latter. In the last round we reduce $A_{new}$ after +adding the feedforward (requiring a carry of $\{0, \ldots, 7\}$ which is fine). + +$(A ⋙ 2) \oplus (A ⋙ 13) \oplus (A ⋙ 22)$ is equivalent to +$(A ⋙ 2) \oplus (A ⋙ 13) \oplus (A ⋘ 10)$: + +![](./upp_sigma_0.png) + +Then, using $4$ more $\mathtt{spread}$ lookups we obtain the result as the even bits of a +linear combination of the pieces: + +$$ +\begin{array}{rcccccccl} + & (a &||& d &||& c &||& b) & \oplus \\ + & (b &||& a &||& d &||& c) & \oplus \\ + & (c &||& b &||& a &||& d) & \\ +&&&&\Downarrow \\ +R' = & 4^{30} a &+& 4^{20} d &+& 4^{11} c &+& b\;&+ \\ + & 4^{21} b &+& 4^{19} a &+& 4^{ 9} d &+& c\;&+ \\ + & 4^{23} c &+& 4^{12} b &+& 4^{10} a &+& d\;& +\end{array} +$$ + +That is, we witness the compressed even bits $R^{even}_i$ and the compressed odd bits +$R^{odd}_i$, and constrain +$$R' = \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1)$$ +where $\{R^{even}_i\}_{i=0..1}$ is the $\Sigma_0$ function output. + +### Σ_1 function + +$\Sigma_1(E)$ can be done in $6$ lookups. + +To achieve this we first split $E$ into pieces $(a, b, c, d)$, of lengths $(6, 5, 14, 7)$ +bits respectively counting from the little end. At the same time we obtain the spread +forms of these pieces. This can all be done in two PLONK rows, because the $7$ and +$14$-bit pieces can be handled using $\mathtt{spread}$ lookups, the $5$-bit piece can be +split into $3$ and $2$-bit subpieces, and the $6$-bit piece can be split into $2 * 3$-bit +subpieces. The four small pieces can be range-checked by polynomial constraints in +parallel with the two lookups, two small pieces in each row. The spread forms of these +small pieces are found by interpolation. + +Note that the splitting into pieces can be combined with the reduction of $E_{new}$, i.e. +no extra lookups are needed for the latter. In the last round we reduce $E_{new}$ after +adding the feedforward (requiring a carry of $\{0, \ldots, 6\}$ which is fine). + +$(E ⋙ 6) \oplus (E ⋙ 11) \oplus (E ⋙ 25)$ is equivalent to +$(E ⋙ 6) \oplus (E ⋙ 11) \oplus (E ⋘ 7)$. + +![](./upp_sigma_1.png) + +Then, using $4$ more $\mathtt{spread}$ lookups we obtain the result as the even bits of a +linear combination of the pieces, in the same way we did for $\Sigma_0$: + +$$ +\begin{array}{rcccccccl} + & (a &||& d &||& c &||& b) & \oplus \\ + & (b &||& a &||& d &||& c) & \oplus \\ + & (c &||& b &||& a &||& d) & \\ +&&&&\Downarrow \\ +R' = & 4^{26} a &+& 4^{19} d &+& 4^{ 5} c &+& b\;&+ \\ + & 4^{27} b &+& 4^{21} a &+& 4^{14} d &+& c\;&+ \\ + & 4^{18} c &+& 4^{13} b &+& 4^{ 7} a &+& d\;& +\end{array} +$$ + +That is, we witness the compressed even bits $R^{even}_i$ and the compressed odd bits +$R^{odd}_i$, and constrain +$$R' = \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1)$$ +where $\{R^{even}_i\}_{i=0..1}$ is the $\Sigma_1$ function output. + +## Block decomposition + +For each block $M \in \{0,1\}^{512}$ of the padded message, $64$ words of $32$ bits each +are constructed as follows: +- The first $16$ are obtained by splitting $M$ into $32$-bit blocks $$M = W_0 || W_1 || \cdots || W_{14} || W_{15};$$ +- The remaining $48$ words are constructed using the formula: +$$W_i = \sigma_1(W_{i-2}) \boxplus W_{i-7} \boxplus \sigma_0(W_{i-15}) \boxplus W_{i-16},$$ for $i = 17, \ldots, 64$. + +> Note: $0$-based numbering is used for the $W$ word indices. + +$$ +\begin{array}{ccc} +\sigma_0(X) &=& (X ⋙ 7) \oplus (X ⋙ 18) \oplus (X ≫ 3) \\ +\sigma_1(X) &=& (X ⋙ 17) \oplus (X ⋙ 19) \oplus (X ≫ 10) \\ +\end{array} +$$ + +> Note: $≫$ is a right-**shift**, not a rotation. + +### σ_0 function + +$(X ⋙ 7) \oplus (X ⋙ 18) \oplus (X ≫ 3)$ is equivalent to +$(X ⋙ 7) \oplus (X ⋘ 14) \oplus (X ≫ 3)$. + +![](./low_sigma_0.png) + +As above but with pieces $(a, b, c, d)$ of lengths $(3, 4, 11, 14)$ counting from the +little end. Split $b$ into two $2$-bit subpieces. + +$$ +\begin{array}{rcccccccl} + & (0^{[3]} &||& d &||& c &||& b) & \oplus \\ + & (\;\;\;b &||& a &||& d &||& c) & \oplus \\ + & (\;\;\;c &||& b &||& a &||& d) & \\ +&&&&\Downarrow \\ +R' = & & & 4^{15} d &+& 4^{ 4} c &+& b\;&+ \\ + & 4^{28} b &+& 4^{25} a &+& 4^{11} d &+& c\;&+ \\ + & 4^{21} c &+& 4^{17} b &+& 4^{14} a &+& d\;& +\end{array} +$$ + +### σ_1 function + +$(X ⋙ 17) \oplus (X ⋙ 19) \oplus (X ≫ 10)$ is equivalent to +$(X ⋘ 15) \oplus (X ⋘ 13) \oplus (X ≫ 10)$. + +![](./low_sigma_1.png) + +TODO: this diagram doesn't match the expression on the right. This is just for consistency +with the other diagrams. + +As above but with pieces $(a, b, c, d)$ of lengths $(10, 7, 2, 13)$ counting from the +little end. Split $b$ into $(3, 2, 2)$-bit subpieces. + +$$ +\begin{array}{rcccccccl} + & (0^{[10]}&||& d &||& c &||& b) & \oplus \\ + & (\;\;\;b &||& a &||& d &||& c) & \oplus \\ + & (\;\;\;c &||& b &||& a &||& d) & \\ +&&&&\Downarrow \\ +R' = & & & 4^{ 9} d &+& 4^{ 7} c &+& b\;&+ \\ + & 4^{25} b &+& 4^{15} a &+& 4^{ 2} d &+& c\;&+ \\ + & 4^{30} c &+& 4^{23} b &+& 4^{13} a &+& d\;& +\end{array} +$$ + +### Message scheduling + +We apply $\sigma_0$ to $W_{1..48}$, and $\sigma_1$ to $W_{14..61}$. In order to avoid +redundant applications of $\mathtt{spread}$, we can merge the splitting into pieces for +$\sigma_0$ and $\sigma_1$ in the case of $W_{14..48}$. Merging the piece lengths +$(3, 4, 11, 14)$ and $(10, 7, 2, 13)$ gives pieces of lengths $(3, 4, 3, 7, 1, 1, 13)$. + +![](./bit_reassignment.png) + +If we can do the merged split in $3$ rows (as opposed to a total of $4$ rows when +splitting for $\sigma_0$ and $\sigma_1$ separately), we save $35$ rows. + +> These might even be doable in $2$ rows; not sure. +> [name=Daira] + +We can merge the reduction mod $2^{32}$ of $W_{16..61}$ into their splitting when they are +used to compute subsequent words, similarly to what we did for $A$ and $E$ in the round +function. + +We will still need to reduce $W_{62..63}$ since they are not split. (Technically we could +leave them unreduced since they will be reduced later when they are used to compute +$A_{new}$ and $E_{new}$ -- but that would require handling a carry of up to $10$ rather +than $6$, so it's not worth the complexity.) + +The resulting message schedule cost is: +- $2$ rows to constrain $W_0$ to $32$ bits + - This is technically optional, but let's do it for robustness, since the rest of the + input is constrained for free. +- $13*2$ rows to split $W_{1..13}$ into $(3, 4, 11, 14)$-bit pieces +- $35*3$ rows to split $W_{14..48}$ into $(3, 4, 3, 7, 1, 1, 13)$-bit pieces (merged with + a reduction for $W_{16..48}$) +- $13*2$ rows to split $W_{49..61}$ into $(10, 7, 2, 13)$-bit pieces (merged with a + reduction) +- $4*48$ rows to extract the results of $\sigma_0$ for $W_{1..48}$ +- $4*48$ rows to extract the results of $\sigma_1$ for $W_{14..61}$ +- $2*2$ rows to reduce $W_{62..63}$ +- $= 547$ rows. + +## Overall cost + +For each round: +- $8$ rows for $Ch$ +- $4$ rows for $Maj$ +- $6$ rows for $\Sigma_0$ +- $6$ rows for $\Sigma_1$ +- $reduce_6$ and $reduce_7$ are always free +- $= 24$ per round + +This gives $24*64 = 1792$ rows for all of "step 3", to which we need to add: + +- $547$ rows for message scheduling +- $2*8$ rows for $8$ reductions mod $2^{32}$ in "step 4" + +giving a total of $2099$ rows. + +## Tables + +We only require one table $\mathtt{spread}$, with $2^{16}$ rows and $3$ columns. We need a +tag column to allow selecting $(7, 10, 11, 13, 14)$-bit subsets of the table for +$\Sigma_{0..1}$ and $\sigma_{0..1}$. + +### `spread` table + +| row | tag | table (16b) | spread (32b) | +|--------------|-----|------------------|----------------------------------| +| $0$ | 0 | 0000000000000000 | 00000000000000000000000000000000 | +| $1$ | 0 | 0000000000000001 | 00000000000000000000000000000001 | +| $2$ | 0 | 0000000000000010 | 00000000000000000000000000000100 | +| $3$ | 0 | 0000000000000011 | 00000000000000000000000000000101 | +| ... | 0 | ... | ... | +| $2^{7} - 1$ | 0 | 0000000001111111 | 00000000000000000001010101010101 | +| $2^{7}$ | 1 | 0000000010000000 | 00000000000000000100000000000000 | +| ... | 1 | ... | ... | +| $2^{10} - 1$ | 1 | 0000001111111111 | 00000000000001010101010101010101 | +| ... | 2 | ... | ... | +| $2^{11} - 1$ | 2 | 0000011111111111 | 00000000010101010101010101010101 | +| ... | 3 | ... | ... | +| $2^{13} - 1$ | 3 | 0001111111111111 | 00000001010101010101010101010101 | +| ... | 4 | ... | ... | +| $2^{14} - 1$ | 4 | 0011111111111111 | 00000101010101010101010101010101 | +| ... | 5 | ... | ... | +| $2^{16} - 1$ | 5 | 1111111111111111 | 01010101010101010101010101010101 | + +For example, to do an $11$-bit $\mathtt{spread}$ lookup, we polynomial-constrain the tag +to be in $\{0, 1, 2\}$. For the most common case of a $16$-bit lookup, we don't need to +constrain the tag. Note that we can fill any unused rows beyond $2^{16}$ with a duplicate +entry, e.g. all-zeroes. + +## Gates + +### Choice gate +Input from previous operations: +- $E', F', G',$ 64-bit spread forms of 32-bit words $E, F, G$, assumed to be constrained by previous operations + - in practice, we'll have the spread forms of $E', F', G'$ after they've been decomposed into 16-bit subpieces +- $evens$ is defined as $\mathtt{spread}(2^{32} - 1)$ + - $evens_0 = evens_1 = \mathtt{spread}(2^{16} - 1)$ + +sn|sc| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | +--|--|-------------|-------------|-----------------------------|------------------------------------|------------------------------------| +0 |0 |{0,1,2,3,4,5}|$P_0^{even}$ |$\texttt{spread}(P_0^{even})$| $\mathtt{spread}(E^{lo})$ | $\mathtt{spread}(E^{hi})$ | +0 |1 |{0,1,2,3,4,5}|$P_0^{odd}$ |$\texttt{spread}(P_0^{odd})$ |$\texttt{spread}(P_1^{odd})$ | | +0 |0 |{0,1,2,3,4,5}|$P_1^{even}$ |$\texttt{spread}(P_1^{even})$| $\mathtt{spread}(F^{lo})$ | $\mathtt{spread}(F^{hi})$ | +0 |0 |{0,1,2,3,4,5}|$P_1^{odd}$ |$\texttt{spread}(P_1^{odd})$ | $evens_0$ | $evens_1$ | +1 |0 |{0,1,2,3,4,5}|$Q_0^{even}$ |$\texttt{spread}(Q_0^{even})$|$\mathtt{spread}(E^{lo})$ | $\mathtt{spread}(E^{hi})$ | +0 |0 |{0,1,2,3,4,5}|$Q_0^{odd}$ |$\texttt{spread}(Q_0^{odd})$ |$evens_0 - \mathtt{spread}(E^{lo})$ |$evens_1 - \mathtt{spread}(E^{hi})$ | +0 |1 |{0,1,2,3,4,5}|$Q_1^{even}$ |$\texttt{spread}(Q_1^{even})$|$\texttt{spread}(Q_1^{odd})$ | | +0 |0 |{0,1,2,3,4,5}|$Q_1^{odd}$ |$\texttt{spread}(Q_1^{odd})$ |$\mathtt{spread}(G^{lo})$ | $\mathtt{spread}(G^{hi})$ | + +Constraints: +- `sc` (choice): $LHS - RHS = 0$ + - $LHS = a_3 \omega^{-1} + a_3 \omega + 2^{32}(a_4 \omega^{-1} + a_4 \omega)$ + - $RHS = a_2 \omega^{-1} + 2* a_2 + 2^{32}(a_2 \omega + 2* a_3)$ +- `sn` (negation): + - $a_3\omega^{-1} - a_3 - a_3\omega = 0$ + - $a_4\omega^{-1} - a_4 - a_4\omega = 0$ +- $\mathtt{spread}$ lookup on $(a_0, a_1, a_2)$ +- permutation between $(a_2, a_3)$ + +Output: $Ch(E, F, G) = P^{odd} + Q^{odd} = (P_0^{odd} + Q_0^{odd}) + 2^{16} (P_1^{odd} + Q_1^{odd})$ + +### Majority gate + +Input from previous operations: +- $A', B', C',$ 64-bit spread forms of 32-bit words $A, B, C$, assumed to be constrained by previous operations + - in practice, we'll have the spread forms of $A', B', C'$ after they've been decomposed into $16$-bit subpieces + +sm| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | +--|-------------|------------|-----------------------------|----------------------------|--------------------------|--------------------------| +0 |{0,1,2,3,4,5}|$M_0^{even}$|$\texttt{spread}(M_0^{even})$| |$\mathtt{spread}(A^{lo})$ |$\mathtt{spread}(A^{hi})$ | +1 |{0,1,2,3,4,5}|$M_0^{odd}$ |$\texttt{spread}(M_0^{odd})$ |$\texttt{spread}(M_1^{odd})$|$\mathtt{spread}(B^{lo})$ |$\mathtt{spread}(B^{hi})$ | +0 |{0,1,2,3,4,5}|$M_1^{even}$|$\texttt{spread}(M_1^{even})$| |$\mathtt{spread}(C^{lo})$ |$\mathtt{spread}(C^{hi})$ | +0 |{0,1,2,3,4,5}|$M_1^{odd}$ |$\texttt{spread}(M_1^{odd})$ | | | | + +Constraints: +- `sm` (majority): $LHS - RHS = 0$ + - $LHS = \mathtt{spread}(M^{even}_0) + 2 \cdot \mathtt{spread}(M^{odd}_0) + 2^{32} \cdot \mathtt{spread}(M^{even}_1) + 2^{33} \cdot \mathtt{spread}(M^{odd}_1)$ + - $RHS = A' + B' + C'$ +- $\mathtt{spread}$ lookup on $(a_0, a_1, a_2)$ +- permutation between $(a_2, a_3)$ + +Output: $Maj(A,B,C) = M^{odd} = M_0^{odd} + 2^{16} M_1^{odd}$ + +### Σ_0 gate + +$A$ is a 32-bit word split into $(2,11,9,10)$-bit chunks, starting from the little end. We refer to these chunks as $(a,b,c,d)$ respectively, and further split $c$ into three 3-bit chunks $c_0, c_1, c_2$. $a'$ and $\{c'_i\}_{i=0}^2$ are the spread versions of the small chunks. + +$$ +\begin{array}{ccc} +\Sigma_0(A) &=& (A ⋙ 2) \oplus (A ⋙ 13) \oplus (A ⋙ 22) \\ +&=& (A ⋙ 2) \oplus (A ⋙ 13) \oplus (A ⋘ 10) +\end{array} +$$ + +ss|s23|s33| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | +--|---|---|-------------|------------|-----------------------------|------------|------------|------------|------------| +0 | 1 | 0 | {0,1} | $d$ | $\texttt{spread}(d)$ | $a$ | $a'$ | $c_0$ | $c'_0$ | +1 | 0 | 0 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $A$ | $\texttt{spread}(R_0^{odd})$|$\texttt{spread}(R_1^{even})$| $\texttt{spread}(R_1^{odd})$| +0 | 0 | 1 | {0,1,2} | $b$ | $\texttt{spread}(b)$ | $c_1$ | $c'_1$ | $c_2$ | $c'_2$ | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ | | | | | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| | | | | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | | | | | + +Constraints: +- `ss` ($\Sigma_0$ constraint): $LHS - RHS + tag + decompose = 0$ + +$$ +\begin{array}{ccc} +tag &=& constrain_1(a_0\omega^{-1}) + constrain_2(a_0\omega) \\ +decompose &=& a + 2^2 b + 2^{13} c_0 + 2^{16} c_1 + 2^{19} c_2 + 2^{22} d- A\\ +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rcccccccccl} +RHS = & 4^{30} a' &+& 4^{20} \texttt{spread}(d) &+& 4^{17} c'_2 &+& 4^{14} c'_1 &+& 4^{11} c'_0 &+& \texttt{spread}(b)\;&+ \\ + & 4^{21} \texttt{spread}(b) &+& 4^{19} a' &+& 4^{9} \texttt{spread}(d) &+& 4^{6} c'_2 &+& 4^{3} c'_1 &+& c'_0\;&+ \\ + & 4^{29} c'_2 &+& 4^{26} c'_1 &+& 4^{23} c'_0 &+& 4^{12} \texttt{spread}(b) &+& 4^{10} a' &+& \texttt{spread}(d)\;& +\end{array} +$$ + +- $\mathtt{spread}$ lookup on $a_0, a_1, a_2$ +- `s22`: + - `sr2` and `sr2` (two 2-bit range checks) + - `ss2` and `ss2` (two 2-bit spreads) +- `s23`: + - `sr2` (2-bit range check) and `sr3` (3-bit range check) + - `ss2` (2-bit spread) and `ss3` (3-bit spread) +(see section [Helper gates](#helper-gates)) + +Output: $\Sigma_0(A) = R^{even} = R_0^{even} + 2^{16} R_1^{even}$ + +### Σ_1 gate +$E$ is a 32-bit word split into $(6,5,14,7)$-bit chunks, starting from the little end. We refer to these chunks as $(a,b,c,d)$ respectively, and further split $a$ into two 3-bit chunks $a_0, a_1$ and $b$ into (2,3)-bit chunks $b_0, b_1$. $\{a'_i\}_{i=0}^1,\{b'_j\}_{j=0}^1$ are the spread versions of the small chunks. + +$$ +\begin{array}{ccc} +\Sigma_1(E) &=& (E ⋙ 6) \oplus (E ⋙ 11) \oplus (E ⋙ 25) \\ +&=& (E ⋙ 6) \oplus (E ⋙ 11) \oplus (E ⋘ 7) +\end{array} +$$ + +ss|s23|s33| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | +--|---|---|-------------|------------|-----------------------------|------------|------------|------------|------------| +0 | 1 | 0 | 0 | $d$ | $\texttt{spread}(d)$ | $b_0$ | $b'_0$ | $b_1$ | $b'_1$ | +1 | 0 | 0 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $E$ | $\texttt{spread}(R_0^{odd})$|$\texttt{spread}(R_1^{even})$| $\texttt{spread}(R_1^{odd})$| +0 | 0 | 1 | {0,1,2,3,4} | $c$ | $\texttt{spread}(c)$ | $a_0$ | $a'_0$ | $a_1$ | $a'_1$ | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ | | | | | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| | | | | +0 | 0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | | | | | + +Constraints: +- `ss` ($\Sigma_1$ constraint): $LHS - RHS + tag + decompose = 0$ + +$$ +\begin{array}{ccc} +tag &=& a_0\omega^{-1} + constrain_4(a_0\omega) \\ +decompose &=& a_0 + 2^3 a_1 + 2^6 b_0 + 2^8 b_1 + 2^{11} c + 2^{25} d - E \\ +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rcccccccccl} +RHS = & 4^{29} a'_1 &+& 4^{26} a'_0 &+& 4^{19} \texttt{spread}(d) &+& 4^{ 5} \texttt{spread}(c) &+& 4^{2} b'_1 &+& b'_0\;&+ \\ + & 4^{29} b'_1 &+& 4^{27} b'_0 &+& 4^{24} a'_1 &+& 4^{21} a'_0 &+& 4^{14} \texttt{spread}(d) &+& \texttt{spread}(c)\;&+ \\ + & 4^{18} \texttt{spread}(c) &+& 4^{15} b'_1 &+& 4^{13} b'_0 &+& 4^{10} a'_1 &+& 4^{7} a'_0 &+& \texttt{spread}(d)\;& +\end{array} +$$ + +- $\mathtt{spread}$ lookup on $a_0, a_1, a_2$ +- `s23`: + - `sr2` (2-bit range check) and `sr3` (3-bit range check) + - `ss2` (2-bit spread) and `ss3` (3-bit spread) +- `s33`: + - `sr3` and `sr3` (two 3-bit range checks) + - `ss3` and `ss3` (two 3-bit spreads) +(see section [Helper gates](#helper-gates)) + +Output: $\Sigma_1(E) = R^{even} = R_0^{even} + 2^{16} R_1^{even}$ + +### σ_0 gate +#### v1 +v1 of the $\sigma_0$ gate takes in a word that's split into $(3, 4, 11, 14)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a, b, c, d).$ $b$ is further split into two 2-bit chunks $b_0,b_1.$ $a',\{b'_i\}_{i=0}^1$ are the spread versions of the small chunks. We already have $\texttt{spread}(c)$ and $\texttt{spread}(d)$ from the message scheduling. + +sr|ss|s22|s23| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | +--|--|---|---|-------------|------------|-----------------------------|--------------|--------------|--------------|--------------| + 0| 0| 1 | 0 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $b_0$ | $b'_0$ | $b_1$ | $b'_1$ | + 0| 1| 0 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ |$\texttt{spread}(R_1^{odd})$ |$\texttt{spread}(c)$|$\texttt{spread}(d)$| + 0| 0| 0 | 1 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| $b_1$ | $b'_1$ | $a$ | $a'$ | + 1| 0| 0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | $R_1$ | $R_0$ | $R_0^{even}$ | $R_0^{odd}$ | + +Constraints: +- `ss` ($\sigma_0$ v1 constraint): $LHS - RHS = 0$ + +$$ +\begin{array}{ccc} +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rccccccccl} +RHS = & & & 4^{15} d &+& 4^{ 4} c &+& 4^2 b_1 &+& b_0\;&+ \\ + & 4^{30} b_1 &+& 4^{28} b_0 &+& 4^{25} a &+& 4^{11} d &+& c\;&+ \\ + & 4^{21} c &+& 4^{19} b_1 &+& 4^{17} b_0 &+& 4^{14} a &+& d\;& +\end{array} +$$ + +- `sr` (reduce): + - $R_1^{even} + 2*R_1^{odd} - R_1 = 0$ + - $R_0^{even} + 2*R_0^{odd} - R_0 = 0$ +- $\mathtt{spread}$ lookup on $a_0, a_1, a_2$ +- `s2`: + - `sr2` (2-bit range check) + - `ss2` (2-bit spread) +- `s3`: + - `sr3` (3-bit range check) + - `ss3` (3-bit spread) +(see section [Helper gates](#helper-gates)) + +#### v2 +v2 of the $\sigma_0$ gate takes in a word that's split into $(3, 4, 3, 7, 1, 1, 13)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a, b, c, d, e, f, g).$ We already have $\mathtt{spread}(e), \mathtt{spread}(g)$ from the message scheduling. The 1-bit $e,f$ remain unchanged by the spread operation and can be used directly. We further split $b$ into two 2-bit chunks $b_0, b_1.$ $a', b'_0, b'_1, c'$ are the spread versions of the small chunks. + +sr|ss|s23| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | $a_7$ | +--|--|---|-------------|------------|-----------------------------|------------|------------|------------|------------|------------| +0 |0 | 1 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $b_0$ | $b'_0$ | $a$ | $a'$ | $e$ | +0 |1 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$| $\texttt{spread}(d)$| $\texttt{spread}(g)$ | +0 |0 | 1 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| $b_1$ | $b'_1$ | $c$ | $c'$ | $f$ | +1 |0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | $R_1$ | $R_0$ |$R_0^{even}$|$R_0^{odd}$ | | + +Constraints: +- `ss` ($\sigma_0$ v2 constraint): $LHS - RHS = 0$ + +$$ +\begin{array}{ccc} +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rcccccccccccl} +RHS = & & & 4^{16} g &+& 4^{15} f &+& 4^{ 14} e &+& 4^{ 7} d &+& 4^{ 4} c &+& 4^2 b_1 &+& b_0\;&+ \\ + & 4^{30} b_1 &+& 4^{28} b_0 &+& 4^{25} a &+& 4^{12} g &+& 4^{11} f &+& 4^{10} e &+& 4^{3} d &+& c\;&+ \\ + & 4^{31} e &+& 4^{24} d &+& 4^{21} c &+& 4^{19} b_1 &+& 4^{17} b_0 &+& 4^{14} a &+& 4^{1} g &+& f\;& +\end{array} +$$ + +- `sr` (reduce): + - $R_1^{even} + 2*R_1^{odd} - R_1 = 0$ + - $R_0^{even} + 2*R_0^{odd} - R_0 = 0$ +- `s23`: + - `sr2` (2-bit range check) and `sr3` (3-bit range check) + - `ss2` (2-bit spread) and `ss3` (3-bit spread) + +### σ_1 gate +#### v1 +v1 of the $\sigma_1$ gate takes in a word that's split into $(10,7,2,13)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a, b, c, d).$ $b$ is further split into (2,2,3)-bit chunks $b_0,b_1,b_2.$ $\{b'_i\}_{i=0}^2, c'$ are the spread versions of the small chunks. We already have $\texttt{spread}(a)$ and $\texttt{spread}(d)$ from the message scheduling. + +sr|ss|s22|s23| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | +--|--|---|---|-------------|------------|-----------------------------|------------|------------|------------|------------| +0 |0 | 1 | 0 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $b_0$ | $b'_0$ | $b_1$ | $b'_1$ | +0 |1 | 0 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$| $\texttt{spread}(a)$| $\texttt{spread}(d)$ | +0 |0 | 0 | 1 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| $b_2$ | $b'_2$ | $c$ | $c'$ | +1 |0 | 0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | $R_0$ | $R_1$ |$R_0^{even}$|$R_0^{odd}$ | + +Constraints: +- `ss` ($\sigma_1$ v1 constraint): $LHS - RHS = 0$ + +$$ +\begin{array}{ccc} +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rcccccccccl} +RHS = & & & 4^{ 9} d &+& 4^{ 7} c &+& 4^{4} b_2 &+& 4^{2} b_1 &+& b_0\;&+ \\ + & 4^{29} b_2 &+& 4^{27} b_1 &+& 4^{25} b_0 &+& 4^{15} a &+& 4^{ 2} d &+& c\;&+ \\ + & 4^{30} c &+& 4^{27} b_2 &+& 4^{25} b_1 &+& 4^{23} b_0 &+& 4^{13} a &+& d\;& +\end{array} +$$ + +- `sr` (reduce): + - $R_1^{even} + 2*R_1^{odd} - R_1 = 0$ + - $R_0^{even} + 2*R_0^{odd} - R_0 = 0$ +- `s23`: + - `sr2` (2-bit range check) and `sr3` (3-bit range check) + - `ss2` (2-bit spread) and `ss3` (3-bit spread) +- `s22`: + - `sr2` and `sr2` (two 2-bit range checks) + - `ss2` and `ss2` (two 2-bit spreads) + +#### v2 +v2 of the $\sigma_1$ gate takes in a word that's split into $(3, 4, 3, 7, 1, 1, 13)$-bit chunks (already constrained by message scheduling). We refer to these chunks respectively as $(a, b, c, d, e, f, g).$ We already have $\mathtt{spread}(e), \mathtt{spread}(g)$ from the message scheduling. The 1-bit $e,f$ remain unchanged by the spread operation and can be used directly. We further split $b$ into two 2-bit chunks $b_0, b_1.$ $a', b'_0, b'_1, c'$ are the spread versions of the small chunks. + +ss|s23| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | $a_7$ | +--|---|-------------|------------|-----------------------------|------------|------------|------------|------------|------------| +0 | 1 |{0,1,2,3,4,5}|$R_0^{even}$|$\texttt{spread}(R_0^{even})$| $b_0$ | $b'_0$ | $a$ | $a'$ | $e$ +1 | 0 |{0,1,2,3,4,5}|$R_0^{odd}$ |$\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$| $\texttt{spread}(d)$| $\texttt{spread}(g)$ | +0 | 1 |{0,1,2,3,4,5}|$R_1^{even}$|$\texttt{spread}(R_1^{even})$| $b_1$ | $b'_1$ | $c$ | $c'$ | $f$ +0 | 0 |{0,1,2,3,4,5}|$R_1^{odd}$ |$\texttt{spread}(R_1^{odd})$ | $R_0$ | $R_1$ |$R_0^{even}$|$R_0^{odd}$ | + +Constraints: +- `ss` ($\sigma_1$ v2 constraint): $LHS - RHS = 0$ + +$$ +\begin{array}{ccc} +LHS &=& \mathtt{spread}(R^{even}_0) + 2 \cdot \mathtt{spread}(R^{odd}_0) + 2^{32} \cdot \mathtt{spread}(R^{even}_1) + 2^{33} \cdot \mathtt{spread}(R^{odd}_1) +\end{array} +$$ +$$ +\begin{array}{rccccccccccccl} +RHS = & &&&& & & 4^{ 9} g &+& 4^{ 7} f &+& 4^{ 7} e &+& d\;&+ \\ + & 4^{25} d &+& 4^{22} c &+& 4^{18} b &+& 4^{15} a &+& 4^{ 2} g &+& 4^{1}f &+& e\;&+ \\ + & 4^{31} f &+& 4^{30} e &+& 4^{23} d &+& 4^{20} c &+& 4^{16} b &+& 4^{13} a &+& g\;& +\end{array} +$$ + +- `sr` (reduce): + - $R_1^{even} + 2*R_1^{odd} - R_1 = 0$ + - $R_0^{even} + 2*R_0^{odd} - R_0 = 0$ +- `s23`: + - `sr2` (2-bit range check) and `sr3` (3-bit range check) + - `ss2` (2-bit spread) and `ss3` (3-bit spread) + + +### Helper gates + +#### Small range constraints +Let $constrain_n(x) = \prod_{i=0}^n (x-i)$. Constraining this expression to equal zero enforces that $x$ is in $[0..n].$ + +#### 2-bit range check +`sr2`: $(a - 3)(a - 2)(a - 1)(a) = 0$ + +sr2| $a_0$ | +---|-------| + 1 | a | + +#### 2-bit spread +`ss2`: $l_1(a) + 4*l_2(a) + 5*l_3(a) - a' = 0$ + +ss2| $a_0$ | $a_1$ +---|-------|------ + 1 | a | a' + +with interpolation polynomials: +- $l_0(a) = \frac{(a - 3)(a - 2)(a - 1)}{(-3)(-2)(-1)}$ ($\mathtt{spread}(00) = 0000$) +- $l_1(a) = \frac{(a - 3)(a - 2)(a)}{(-2)(-1)(1)}$ ($\mathtt{spread}(01) = 0001$) +- $l_2(a) = \frac{(a - 3)(a - 1)(a)}{(-1)(1)(2)}$ ($\mathtt{spread}(10) = 0100$) +- $l_3(a) = \frac{(a - 2)(a - 1)(a)}{(1)(2)(3)}$ ($\mathtt{spread}(11) = 0101$) + +#### 3-bit range check +`sr3`: $(a - 7)(a - 6)(a - 5)(a - 4)(a - 3)(a - 2)(a - 1)(a) = 0$ + +sr3| $a_0$ | +---|-------| + 1 | a | + +#### 3-bit spread +`ss3`: $l_1(a) + 4*l_2(a) + 5*l_3(a) + 16*l_4(a) + 17*l_5(a) + 20*l_6(a) + 21*l_7(a) - a' = 0$ + +ss3| $a_0$ | $a_1$ +---|-------|------ + 1 | a | a' + +with interpolation polynomials: +- $l_0(a) = \frac{(a - 7)(a - 6)(a - 5)(a - 4)(a - 3)(a - 2)(a - 1)}{(-7)(-6)(-5)(-4)(-3)(-2)(-1)}$ ($\mathtt{spread}(000) = 000000$) +- $l_1(a) = \frac{(a - 7)(a - 6)(a - 5)(a - 4)(a - 3)(a - 2)(a)}{(-6)(-5)(-4)(-3)(-2)(-1)(1)}$ ($\mathtt{spread}(001) = 000001$) +- $l_2(a) = \frac{(a - 7)(a - 6)(a - 5)(a - 4)(a - 3)(a - 1)(a)}{(-5)(-4)(-3)(-2)(-1)(1)(2)}$ ($\mathtt{spread}(010) = 000100$) +- $l_3(a) = \frac{(a - 7)(a - 6)(a - 5)(a - 3)(a - 2)(a - 1)(a)}{(-4)(-3)(-2)(-1)(1)(2)(3)}$ ($\mathtt{spread}(011) = 000101$) +- $l_4(a) = \frac{(a - 7)(a - 6)(a - 5)(a - 3)(a - 2)(a - 1)(a)}{(-3)(-2)(-1)(1)(2)(3)(4)}$ ($\mathtt{spread}(100) = 010000$) +- $l_5(a) = \frac{(a - 7)(a - 6)(a - 4)(a - 3)(a - 2)(a - 1)(a)}{(-2)(-1)(1)(2)(3)(4)(5)}$ ($\mathtt{spread}(101) = 010001$) +- $l_6(a) = \frac{(a - 7)(a - 5)(a - 4)(a - 3)(a - 2)(a - 1)(a)}{(-1)(1)(2)(3)(4)(5)(6)}$ ($\mathtt{spread}(110) = 010100$) +- $l_7(a) = \frac{(a - 6)(a - 5)(a - 4)(a - 3)(a - 2)(a - 1)(a)}{(1)(2)(3)(4)(5)(6)(7)}$ ($\mathtt{spread}(111) = 010101$) + +#### reduce_6 gate +Addition $\pmod{2^{32}}$ of 6 elements + +Input: +- $E$ +- $\{e_i^{lo}, e_i^{hi}\}_{i=0}^5$ +- $carry$ + +Check: $E = e_0 + e_1 + e_2 + e_3 + e_4 + e_5 \pmod{32}$ + +Assume inputs are constrained to 16 bits. +- Addition gate (sa): + - $a_0 + a_1 + a_2 + a_3 + a_4 + a_5 + a_6 - a_7 = 0$ +- Carry gate (sc): + - $2^{16} a_6 \omega^{-1} + a_6 + [(a_6 - 5)(a_6 - 4)(a_6 -3)(a_6 - 2)(a_6 - 1)(a_6)] = 0$ + +sa|sc| $a_0$ | $a_1$ |$a_2$ |$a_3$ |$a_4$ |$a_5$ |$a_6$ |$a_7$ | +--|--|----------|----------|----------|----------|----------|----------|---------------|--------| +1 |0 |$e_0^{lo}$|$e_1^{lo}$|$e_2^{lo}$|$e_3^{lo}$|$e_4^{lo}$|$e_5^{lo}$|$-carry*2^{16}$|$E^{lo}$| +1 |1 |$e_0^{hi}$|$e_1^{hi}$|$e_2^{hi}$|$e_3^{hi}$|$e_4^{hi}$|$e_5^{hi}$|$carry$ |$E^{hi}$| + +Assume inputs are constrained to 16 bits. +- Addition gate (sa): + - $a_0 \omega^{-1} + a_1 \omega^{-1} + a_2 \omega^{-1} + a_0 + a_1 + a_2 + a_3 \omega^{-1} - a_3 = 0$ +- Carry gate (sc): + - $2^{16} a_3 \omega + a_3 \omega^{-1} = 0$ + + +sa|sc| $a_0$ | $a_1$ |$a_2$ |$a_3$ | +--|--|----------|----------|----------|---------------| +0 |0 |$e_0^{lo}$|$e_1^{lo}$|$e_2^{lo}$|$-carry*2^{16}$| +1 |1 |$e_3^{lo}$|$e_4^{lo}$|$e_5^{lo}$|$E^{lo}$ | +0 |0 |$e_0^{hi}$|$e_1^{hi}$|$e_2^{hi}$|$carry$ | +1 |0 |$e_3^{hi}$|$e_4^{hi}$|$e_5^{hi}$|$E^{hi}$ | + +#### reduce_7 gate +Addition $\pmod{2^{32}}$ of 7 elements + +Input: +- $E$ +- $\{e_i^{lo}, e_i^{hi}\}_{i=0}^6$ +- $carry$ + +Check: $E = e_0 + e_1 + e_2 + e_3 + e_4 + e_5 + e_6 \pmod{32}$ + +Assume inputs are constrained to 16 bits. +- Addition gate (sa): + - $a_0 + a_1 + a_2 + a_3 + a_4 + a_5 + a_6 + a_7 - a_8 = 0$ +- Carry gate (sc): + - $2^{16} a_7 \omega^{-1} + a_7 + [(a_7 - 6)(a_7 - 5)(a_7 - 4)(a_7 -3)(a_7 - 2)(a_7 - 1)(a_7)] = 0$ + +sa|sc| $a_0$ | $a_1$ |$a_2$ |$a_3$ |$a_4$ |$a_5$ |$a_6$ |$a_7$ |$a_8$ | +--|--|----------|----------|----------|----------|----------|----------|----------|---------------|--------| +1 |0 |$e_0^{lo}$|$e_1^{lo}$|$e_2^{lo}$|$e_3^{lo}$|$e_4^{lo}$|$e_5^{lo}$|$e_6^{lo}$|$-carry*2^{16}$|$E^{lo}$| +1 |1 |$e_0^{hi}$|$e_1^{hi}$|$e_2^{hi}$|$e_3^{hi}$|$e_4^{hi}$|$e_5^{hi}$|$e_6^{hi}$|$carry$ |$E^{hi}$| + + +### Message scheduling region +For each block $M \in \{0,1\}^{512}$ of the padded message, $64$ words of $32$ bits each are constructed as follows: +- the first $16$ are obtained by splitting $M$ into $32$-bit blocks $$M = W_0 || W_1 || \cdots || W_{14} || W_{15};$$ +- the remaining $48$ words are constructed using the formula: +$$W_i = \sigma_1(W_{i-2}) \boxplus W_{i-7} \boxplus \sigma_0(W_{i-15}) \boxplus W_{i-16},$$ for $i = 16, \ldots, 63$. + +sw|sd0|sd1|sd2|sd3|sr |ss0|ss0_v2|ss1|ss1_v2|s22|s23| $a_0$ | $a_1$ | $a_2$ | $a_3$ | $a_4$ | $a_5$ | $a_6$ | $a_7$ | $a_8$ | +--|---|---|---|---|---|---|------|---|------|---|---|---------------|------------------|-----------------------------------|------------------------------|----------------------------------|---------------------------------|--------------------------------- |------------------------|------------------------| +0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{0}^{lo}$ | $\texttt{spread}(W_{0}^{lo})$ | | | $W_{0}$ |$\sigma_0(W_1)^{lo}$ |$\sigma_1(W_{14})^{lo}$ | $W_{9}^{lo}$ | +1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{0}^{hi}$ | $\texttt{spread}(W_{0}^{hi})$ | $W_{0}^{lo}$ | $W_{0}^{hi}$ | $W_{16}$ |$\sigma_0(W_1)^{hi}$ |$\sigma_1(W_{14})^{hi}$ | $W_{9}^{hi}$ | +0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4} | $W_{1}^{d(14)}$ | $\texttt{spread}(W_{1}^{d(14)})$ | $W_{1}^{a(3)}$ | $W_{1}^{b(4)}$ | $W_{1}$ |$\sigma_0(W_2)^{lo}$ |$\sigma_1(W_{15})^{lo}$ | $W_{10}^{lo}$ | +1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2} | $W_{1}^{c(11)}$ | $\texttt{spread}(W_{1}^{c(11)})$ | $W_{1}^{lo}$ | $W_{1}^{hi}$ | $W_{17}$ |$\sigma_0(W_2)^{hi}$ |$\sigma_1(W_{15})^{hi}$ | $W_{10}^{hi}$ | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | {0,1,2,3,4,5} | $R_0^{even}$ | $\texttt{spread}(R_0^{even})$ | $W_{1}^{b(4)lo}$ |$\texttt{spread}(W_{1}^{b(4)lo})$ | $W_{1}^{b(4) hi}$ |$\texttt{spread}(W_{1}^{b(4)hi})$ | | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $R_1^{odd}$ | $\texttt{spread}(R_1^{odd})$ | $\sigma_0 v1 R_1$ | $\sigma_0 v1 R_0$ | $\sigma_0 v1 R_0^{even}$ | $\sigma_0 v1 R_0^{odd}$ | | | +0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $R_0^{odd}$ | $\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$ |$\texttt{spread}(W_{1}^{c(11)})$ |$\texttt{spread}(W_{1}^{d(14)})$ | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | {0,1,2,3,4,5} | $R_1^{even}$ | $\texttt{spread}(R_1^{even})$ | $W_{1}^{b(4)hi}$ |$\texttt{spread}(W_{1}^{b(4)hi})$ | $W_{1}^{a(3)}$ |$\texttt{spread}(W_{1}^{a(3)})$ | | | +..|...|...|...|...|...|...|... |...|... |...|...| ... | ... | ... | ... | ... | ... | ... | ... | ... | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3} | $W_{14}^{g(13)}$ | $\texttt{spread}(W_{14}^{g(13)})$ | $W_{14}^{a(3)}$ | $W_{14}^{c(3)}$ | | | | | +0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | $W_{14}^{d(7)}$ | $\texttt{spread}(W_{14}^{d(7)})$ | $W_{14}^{e(1)}$ | $W_{14}^{f(1)}$ | $W_{14}$ |$\sigma_0(W_{15})^{lo}$ |$\sigma_1(W_{28})^{lo}$ | $W_{23}^{lo}$ | +1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | $W_{14}^{b(4)}$ | $\texttt{spread}(W_{14}^{b(4)})$ | $W_{14}^{lo}$ | $W_{14}^{hi}$ | $W_{30}$ |$\sigma_0(W_{15})^{hi}$ |$\sigma_1(W_{28})^{hi}$ | $W_{23}^{hi}$ | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | {0,1,2,3,4,5} | $R_0^{even}$ | $\texttt{spread}(R_0^{even})$ | $W_{14}^{b(4)lo}$ |$\texttt{spread}(W_{14}^{b(4)lo})$| $W_{14}^{a(3)}$ |$\texttt{spread}(W_{14}^{a(3)})$ | $W_{14}^{e(1)}$ | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $R_0^{odd}$ | $\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$ |$\texttt{spread}(W_{14}^{d(7)})$ |$\texttt{spread}(W_{14}^{g(13)})$| | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | {0,1,2,3,4,5} | $R_1^{even}$ | $\texttt{spread}(R_1^{even})$ | $W_{14}^{b(4) hi}$ |$\texttt{spread}(W_{14}^{b(4)hi})$| $W_{14}^{c(3)}$ |$\texttt{spread}(W_{14}^{c(3)})$ | $W_{14}^{f(1)}$ | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $R_1^{odd}$ | $\texttt{spread}(R_1^{odd})$ | $\sigma_0 v2 R_0$ | $\sigma_0 v2 R_1$ |$\sigma_0 v2 R_0^{even}$ |$\sigma_0 v2 R_0^{odd}$ | | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | {0,1,2,3,4,5} | $R_0^{even}$ | $\texttt{spread}(R_0^{even})$ | $W_{14}^{b(4)lo}$ |$\texttt{spread}(W_{14}^{b(4)lo})$| $W_{14}^{a(3)}$ |$\texttt{spread}(W_{14}^{a(3)})$ | $W_{14}^{e(1)}$ | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | {0,1,2,3,4,5} | $R_0^{odd}$ | $\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$ | $\texttt{spread}(d)$ | $\texttt{spread}(g)$ | | | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | {0,1,2,3,4,5} | $R_1^{even}$ | $\texttt{spread}(R_1^{even})$ | $W_{14}^{b(4) hi}$ |$\texttt{spread}(W_{14}^{b(4)hi})$| $W_{14}^{c(3)}$ |$\texttt{spread}(W_{14}^{c(3)})$ | $W_{14}^{f(1)}$ | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $R_1^{odd}$ | $\texttt{spread}(R_1^{odd})$ | $\sigma_1 v2 R_0$ | $\sigma_1 v2 R_1$ |$\sigma_1 v2 R_0^{even}$ |$\sigma_1 v2 R_0^{odd}$ | | | +..|...|...|...|...|...|...|... |...|... |...|...| ... | ... | ... | ... | ... | ... | ... | ... | ... | +0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3} | $W_{49}^{d(13)}$ | $\texttt{spread}(W_{49}^{d(13)})$ | $W_{49}^{c(2}$ | $W_{49}^{b(7)}$ | $W_{49}$ | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1} | $W_{49}^{a(10)}$ | $\texttt{spread}(W_{49}^{a(10)})$ | $W_{49}^{lo}$ | $W_{49}^{hi}$ | | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 |{0,1,2,3,4,5} | $R_0^{even}$ | $\texttt{spread}(R_0^{even})$ | $W_{49}^{b(7)lo}$ |$\texttt{spread}(W_{49}^{b(7)lo})$| $W_{49}^{b(7)mid}$ |$\texttt{spread}(W_{49}^{b(7)mid})$| | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 |{0,1,2,3,4,5} | $R_0^{odd}$ | $\texttt{spread}(R_0^{odd})$ | $\texttt{spread}(R_1^{odd})$ | $\texttt{spread}(a)$ | $\texttt{spread}(d)$ | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 |{0,1,2,3,4,5} | $R_1^{even}$ | $\texttt{spread}(R_1^{even})$ | $W_{49}^{b(7)hi}$ |$\texttt{spread}(W_{49}^{b(7)hi})$| $W_{49}^{c(2)}$ |$\texttt{spread}(W_{49}^{c(2)})$ | | | +0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 | 0 | 0 |{0,1,2,3,4,5} | $R_1^{odd}$ | $\texttt{spread}(R_1^{odd})$ | $\sigma_1 v1 R_0$ | $\sigma_1 v1 R_1$ |$R_0^{even}$ |$R_0^{odd}$ | | | +..|...|...|...|...|...|...|... |...|... |...|...| ... | ... | ... | ... | ... | ... | ... | ... | ... | +0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{62}^{lo}$ | $\texttt{spread}(W_{62}^{lo})$ | | | $W_{62}$ | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{62}^{hi}$ | $\texttt{spread}(W_{62}^{hi})$ | | | | | | | +0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{63}^{lo}$ | $\texttt{spread}(W_{63}^{lo})$ | | | $W_{63}$ | | | | +0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | {0,1,2,3,4,5} | $W_{63}^{hi}$ | $\texttt{spread}(W_{63}^{hi})$ | | | | | | | + +Constraints: +- `sw`: construct word using $reduce_4$ +- `sd0`: decomposition gate for $W_0, W_{62}, W_{63}$ + - $W^{lo} + 2^{16} W^{hi} - W = 0$ +- `sd1`: decomposition gate for $W_{1..13}$ (split into $(3,4,11,14)$-bit pieces) + - $W^{3b} + 2^3 W^{4b} + 2^7 W^{11b} + 2^{18} W^{14b} - W = 0$ + - $W^{lo} + 2^{16} W^{hi} - W = 0$ +- `sd2`: decomposition gate for $W_{14..48}$ (split into $(3,4,3,7,1,1 ,13)$-bit pieces) +- `sd3`: decomposition gate for $W_{49..61}$ (split into $(10,7,2,13)$-bit pieces) + + +### Compression region + +```plaintext ++----------------------------------------------------------+ +| | +| | +| | +| Σ_0(A) | +| | +| | +| | +| +---------------------------------------+ +| | | +| | | +| | | +| | reduce_7() to get A | +| | | +| | | +| | | ++------------------+---------------------------------------+ +| | +| Maj(A,B,C) | +| | ++----------------------------------------------------------+ +| | +| | +| | +| Σ_1(E) | +| | +| | +| | +| +---------------------------------------+ +| | | +| | | +| | | +| | reduce_6() to get E | +| | | +| | | +| | | ++------------------+---------------------------------------+ +| | +| Ch(E,F,G) | +| | ++----------------------------------------------------------+ +``` + + +#### Round 1 + +1. decompose $A$ into $A_0, A_1$ 16-bit subpieces +2. $\Sigma_0(A)$ + - decomposes $A$ into $(2, 11, 3, 3, 3, 10)$-bit subpieces + - spreads each of the subpieces + - outputs $R_0^{even}, R_1^{even}$ +3. decompose $B$ + - into $16$-bit subpieces + - spread each of the subpieces +4. decompose $C$ + - into $16$-bit subpieces + - spread each of the subpieces +5. $Maj(A,B,C)$ + - takes in the 16-bit spread subpieces of $A,B,C$ + - outputs $M_0^{odd}, M_1^{odd}$ +6. decompose $E$ into $E_0, E_1$ 16-bit subpieces +7. $\Sigma_1(E)$ + - decomposes $E$ into $(3, 3, 2, 3, 13, 7)$-bit subpieces + - spreads each of the subpieces + - outputs $R_0^{even}, R_1^{even}$ +8. decompose $F$ + - into $16$-bit subpieces + - spread each of the subpieces +9. decompose $G$ + - into $16$-bit subpieces + - spread each of the subpieces +10. $Ch(E,F,G)$ + - takes in the 16-bit spread subpieces of $E,F,G$ + - outputs $P_0^{odd}, Q_0^{odd}, P_1^{odd}, Q_1^{odd}$ +11. decompose $H$ into $16$-bit subpieces + +#### Round 2 (steady-state) +1. $reduce_7$ to get $A$ + - $H' = H_{prev} + Ch(E_{prev}, F_{prev}, G_{prev}) + \Sigma_1(E_{prev}) + K_1 + W_1$ + - $reduce_7(H' + Maj(A_{prev}, B_{prev}, C_{prev}) + \Sigma_0(A_{prev}))$ + - outputs $A_0, A_1$ 16-bit subpieces +2. $\Sigma_0(A)$ + - decomposes $A$ into $(2, 11, 3, 3, 3, 10)$-bit subpieces + - spreads each of the subpieces + - outputs $R_0^{even}, R_1^{even}$ +3. $B = A_{prev}$ +4. $C = B_{prev}$ +5. $Maj(A,B,C)$ + - takes in the 16-bit spread subpieces of $A,B,C$ + - outputs $M_0^{odd}, M_1^{odd}$ +6. $reduce_6$ to get $E$ + - $H' = H_{prev} + Ch(E_{prev}, F_{prev}, G_{prev}) + \Sigma_1(E_{prev}) + K_1 + W_1$ + - $reduce_6(H' + D_{prev})$ + - outputs $E_0, E_1$ 16-bit subpieces +7. $\Sigma_1(E)$ + - decomposes $E$ into $(3, 3, 2, 3, 13, 7)$-bit subpieces + - spreads each of the subpieces + - outputs $R_0^{even}, R_1^{even}$ +8. $F = E_{prev}$ +9. $G = F_{prev}$ +10. $Ch(E,F,G)$ + - takes in the 16-bit spread subpieces of $E,F,G$ + - outputs $P_0^{odd}, Q_0^{odd}, P_1^{odd}, Q_1^{odd}$ +11. $H = G_{prev}$ diff --git a/book/src/design/gadgets/sha256/upp_sigma_0.png b/book/src/design/gadgets/sha256/upp_sigma_0.png new file mode 100644 index 0000000..f509e5d Binary files /dev/null and b/book/src/design/gadgets/sha256/upp_sigma_0.png differ diff --git a/book/src/design/gadgets/sha256/upp_sigma_1.png b/book/src/design/gadgets/sha256/upp_sigma_1.png new file mode 100644 index 0000000..6f80dc7 Binary files /dev/null and b/book/src/design/gadgets/sha256/upp_sigma_1.png differ