# Audit of Midnight Foreign Field, ECC & Hashing Circuits
- **Client**: Midnight
- **Date**: January 13th, 2025
- **Tags**: Halo2, Poseidon, SHA-256, Hash-to-curve, Merkle Trees, Circuits, Midnight
## Introduction
On November 18th, 2024, zkSecurity was commissioned to perform a security audit of IOG's circuits for the Midnight network at commit [dec9e46](https://github.com/midnightntwrk/midnight-zk/commit/dec9e464d7d8776b6b972666ba51156a7e090fd8); this code originally resided in an internal repository and was archived in the new repository prior to publication for transparency and future reference.
For the two weeks, four consultants reviewed the Midnight circuits written in Halo2 in search of bugs.
Further, starting on January 6th, 2025, two consultants focused on the SHA256 implementation for one additional week to cover the full scope.
A number of observations and findings have been reported to the IOG team.
The findings are detailed in the latter section of this report.
The Midnight circuits were found to be of high quality, accompanied by thorough documentation and tests.
Note that security audits are a valuable tool for identifying and mitigating security risks, but they are not a guarantee of perfect security. Security is a continuous process, and organizations should always be working to improve their security posture.
### Scope
The scope of the audit was divided into distinct parts:
- **Non-Native Arithmetic / Foreign Field Arithmetic Circuits** (`src/field`).
- **Other Circuit Gadgets**, including:
- Two SHA-256 circuits targeting different circuit sizes, using different lookup table sizes (`src/sha256`).
- **Poseidon Circuit** (`src/poseidon`).
- **Elliptic Curve Arithmetic**, covering both native (supporting an inner Edwards curve) and foreign/non-native implementations, as well as the hash-to-curve circuit (`src/ecc`).
- **Merkle Tree Circuit** (`src/map`), including a membership verifier (`examples/membership.rs`).
- A gadget for emulating arithmetic over large unsigned integers (`src/biguint`).
Additionally, we reviewed the API provided by the Midnight library (`src/compact_std_lib.rs` and `src/instructions`).
## Background on Midnight Circuits
This section provides an overview of the Midnight library and circuits.
### Overview of the Midnight Library
Midnight Circuits is a library designed for implementing circuits with Halo2. It is built on the PSE v0.4.0 release of the Halo2 fork. Midnight Circuits provides a variety of gadgets to build upon, including:
- Native and non-native field operations.
- Native and non-native elliptic-curve operations.
- Arithmetic over large unsigned integers.
- Native hash-to-curve operations.
- SHA256 and Poseidon hashing operations.
- Membership operations based on a Merkle tree implementation.
All of these functionalities are exposed as gadgets in `src/compact_std_lib.rs`, with their APIs defined in the traits located in `src/instructions`.
Using Midnight Circuits is straightforward, and numerous examples can be found in the `examples/` directory. However, users should take care to properly constrain the value cells passed to Midnight Circuits (e.g., via `std_lib.assign_many`) and ensure that values computed by Midnight Circuits and exposed as public inputs are correctly constrained (e.g., using `std_lib.constrain_as_public_input`).
## Range Checks
Range checks enforce that a field element $x \in \mathbb{F}_p$ belongs to a set of values $\{ 0, 1, 2, \ldots, B \} \subseteq \mathbb{F}_p$, i.e. it is "small".
For instance, in the foreign field emulation code, range checks ensure that the limbs of a field element are in the range $[0, B)$
and that integer relations being checked do not overflow the modulus of the field.
Let us describe how range checks are implemented in the Midnight circuits.
### Pow2RangeChip
The `Pow2RangeChip` chip handles range checking cells in small power-of-two ranges.
The ranges must be small (e.g. 8-bits) since the range check uses a lookup table:
a table contains all values from the range and a range check simply verifies that the value appears in the table.
To support multiple ranges (all powers of two smaller than some `max_bit_len`), a "table" is created for each.
To avoid allocating many columns, all tables are packed into a single larger table with rows separated by a "tag",
resulting in:
$$
\begin{align*}
T = \{ \\
&(0, 0), \\
&(1, 0), (1, 1), \\
&(2, 0), (2, 1), (2, 2), (2, 3), \\
&(3, 0), (3, 1), (3, 2), (3, 3), (3, 4), (3, 5), (3, 6), (3, 7), \\
&\\ldots \\
\}
\end{align*}
$$
In other words, checking that $(b, \mathsf{assigned\_limb}) \in T$ implies $\mathsf{assigned\_limb} \in \{ 0, 1, \ldots, 2^b - 1 \} \subseteq \mathbb{F}_p$.
The actual lookup constraint enforces a "vectorized" version of this lookup, checking that a vector of values $(b, \mathsf{assigned\_limb}_1, \mathsf{assigned\_limb}_2, \mathsf{assigned\_limb}_3, \mathsf{assigned\_limb}_4)$ satisfies:
$$
\begin{align*}
(b, \mathsf{assigned\_limb}_1) &\in T \\
(b, \mathsf{assigned\_limb}_2) &\in T \\
(b, \mathsf{assigned\_limb}_3) &\in T \\
(b, \mathsf{assigned\_limb}_4) &\in T \\
\end{align*}
$$
Note that the same range is enforced on all the values.
This is implemented by the "pow2range column check":
```rust
for val_col in val_cols {
meta.lookup("pow2range column check", |meta| {
let sel = meta.query_selector(q_pow2range);
let tag = meta.query_fixed(tag_col, Rotation::cur());
let val = meta.query_advice(val_col, Rotation::cur());
vec![(tag, t_tag), (sel * val, t_val)]
});
}
```
The lookup is "disabled" (made trivial) when `tag = q_pow2range = 0`, causing a lookup of the dummy all-zeroes vector in the first table row.
Note that the sub-table separators must be unique within the `tag` column if this lookup column is shared with another chip.
In the code, the column is used exclusively by the `Pow2RangeChip`.
### P2RDecompositionChip
The `P2RDecompositionChip` uses the `Pow2RangeChip` to combine multiple smaller range checks
using linear combinations (see the native chip section)
for checking larger ranges.
This is implemented by "superimposing" the `Pow2RangeChip` on top of the `NativeChip`—
enabling both gates at the same offset.
By configuring the `NativeChip` to compute a linear combination of the
limbs with coefficients $1, B, B^2, B^3$ and enabling the `Pow2RangeChip` at the same offset with a tag for range $[0, B)$,
we can verify that the linear combination is in range $[0, B^4)$:
$$
\mathsf{assigned\_result} = \sum_i B^i \cdot \mathsf{assigned\_limbs}_i
$$
**Smaller Range:** For smaller ranges (with fewer than 4 limbs), we simply set the coefficients of unused limbs to zero in the linear combination.
For example, for a range $[0, B)$ with 3 limbs the linear combination is: $\mathsf{assigned\_result} = \mathsf{assigned\_limbs}_0 + B \cdot \mathsf{assigned\_limbs}_1 + B^2 \cdot \mathsf{assigned\_limbs}_2$.
This technique works for proving ranges $[0, B^k)$ where $k \leq 4$.
For larger ranges, or ranges with a bit-size not divisible by $b$ where $B = 2^b$,
we extend the technique to split the range check across multiple rows with different bounds $B$.
This works well since the native gate supports carrying between rows,
allowing longer linear combinations across multiple rows without copy constraints.
The implementation is:
```rust
// assign terms for linear combination
let native_chip = self.native_chip();
let (assigned_limbs, assigned_result) = native_chip.assign_linear_combination_aux(
&mut region,
terms.as_slice(),
F::ZERO,
&x,
NB_POW2RANGE_COLS,
&mut offset,
)?;
offset += 1;
// enable the appropriate copy constraints in the rows where we assigned the
// linear combination terms
let pow2range_chip = self.pow2range_chip();
// get the lookup selector and tag columns
let range_selector_column = pow2range_chip.config().q_pow2range;
let range_tag_column = pow2range_chip.config().tag_col;
// we reverse since we do the rangechecks from higher end to start
for (i, tag) in tags.into_iter().rev().enumerate() {
let current_row = offset - (i + 1);
range_selector_column.enable(&mut region, current_row)?;
region.assign_fixed(
|| "assign decomposition tag",
range_tag_column,
current_row,
|| Value::known(F::from(tag as u64)),
)?;
}
```
The final task is computing the optimal number of rows needed to enforce the range.
This is done using a dynamic programming algorithm that calculates the optimal decomposition for increasingly larger ranges,
beginning with ranges enforceable in a single row.
## Native Field
### Native Chip
The native chip implements common arithmetic operations over the native field.
This is accomplished using one custom gate which checks the following relation
```python
q_arith * (
(sum_i coeff[i] * values[i])
+ q_next * value[0].next +
+ mul_ab * value[0] * value[1] +
+ mul_cd * value[2] * value[3] +
+ constant
) = 0
```
where `values` are stored in advice columns, and all the other terms are stored in fixed columns, and `values[0].next` is the value in the `values[0]` column at the next row.
The length of the `values` and `coeffs` array is a constant, and it is set to 5 in the current implementation.
```rust
pub const NB_ARITH_COLS: usize = 5;
```
By customizing the fixed terms, this gate is specialized to implement a lot of common arithmetic operations over the native field, which are used extensively throughout the library.
A lot of those operations eventually call into the `custom()` function, which implements a general application of the gate.
It assigns all the fixed values over some input region and enables the `q_arith` selector to enforce the constraint in the current region at the given offset.
Most of the operations are quite straight forward, but it is worth mentioning how the circuit can assert the result of a linear combination.
This is accomplished by the function `linear_combination()`, which calls into the`assign_linear_combination_aux()` function.
Given some coefficients, values, a constant and a result it asserts that:
$$
\mathsf{result} = \mathsf{constant} + \sum_{i=0}^{N-1}\left(\mathsf{coeff}_i \cdot \mathsf{value}_i\right)
$$
Since the length of the linear combination is arbitrary, this is accomplished using the custom gate over multiple rows, each row checking one part of the linear combination.
We decompose the sum into two parts, first computing the first $K$ terms, and then checking the rest:
$$
\mathsf{result} = \mathsf{constant} + \sum_{i=0}^{K-1}\left(\mathsf{coeff}_i \cdot \mathsf{value}_i\right) + \sum_{i = K}^{N}\left(\mathsf{coeff}_i \cdot \mathsf{value}_i\right)
$$
Notice that checking the remaining linear combination is a smaller instance of the original problem.
We enforce the constraints over the rows recursively as follows, using the linear combination part of the custom gate and taking $K$ to be the number of columns in the gate minus one.
```python
-res[0] + res[1] + c[0]*a[0] + c[1]*a[1] + ... + c[K-1]*a[K-1] = 0
-res[1] + res[2] + c[K]*a[K] + c[K+1]*a[K+1] + ... + c[2*K-1]*a[2*K-1] = 0
...
-res[L] + c[L*K]*a[L*K] + c[L*K+1]*a[L*K+1] [+ ...] = 0
```
At some point the number of remaining terms to check fit in one row, and we can check the relation directly with one application of the custom gate.
The current result is stored in the first value column, and the result in the next row is retrieved by setting `q_next` to one.
The constant is only added into the relation on the top-level call, all other recursive calls have the constant term set to zero.
### NativeGadget
The `NativeGadget` is a gadget that combines a `CoreDecomposition` and a `NativeArith` chips to provide common functionalities, like range checks, comparisons and decomposition of field elements.
As before, most functions are straight-forward, but it is worth mentioning how the `assert_lower_than_fixed()` function works.
This asserts that some assigned native is lower than a given constant bound.
The core decomposition chip provides a `assert_less_than_pow2()` function, which range checks some value in the range $[0, 2^t)$ for some $t$.
Checking that a number belongs to some arbitrary range $[0, b)$ where $b \in [2^k, 2^{k+1})$ is equivalent to check that
$$
x \in [0, 2^k) \quad\text{or}\quad (x - (b - 2^k)) \in [0, 2^k)
$$
The prover witnesses the bit $b$, that indicates which relation they want to prove.
Then they prove a valid range check with the corresponding power of two.
Two other functions worth mentioning are `lower_than()` and `lower_than_fixed()`, which return true if the given bounded element is strictly less than another field element.
We know that a bounded element (at the type-system level) has some bound $2^\mathsf{bound}$, so if $y \geq 2^\mathsf{bound}$ then the function returns true. ($x < 2^\mathsf{bound} \leq y$). Otherwise, we know that $y < 2^\mathsf{bound}$.
- If $x < y$ then $y - x > 0$, which implies that $y - x - 1 \in [0, 2^\mathsf{bound})$
- If $x \geq y$ then $x - y \in [0, 2^\mathsf{bound})$
Now witness a fresh bit $b$ and define
$$
z = b \cdot(2y - 1) + x -2bx -y
$$
Since $b$ is a bit, there are two cases:
- if $b=0$ then $z = x - y$, and
- if $b=1$ then $z = y - x - 1$.
Then we range check that $z \in [0, 2^\mathsf{bound})$ and the result of the comparison should be in the bit $b$.
Note that it is important that $\mathsf{bound}$ has to be constrained to be sufficiently small so that if $x \geq y$, the expression $y - x - 1$ do not underflow enough to land in the range $[0, 2^\mathsf{bound})$, rendering the comparison unsound.
This is accomplished by comparing the bound with the following constant
```rust
const MAX_BOUND_IN_BITS: u32 = F::NUM_BITS - 2;
```
in the `bounded_of_element()` function, which is the only safe constructor for `AssignedBounded`.
## Foreign Field
The goal of the foreign field emulation is to check relations over a foreign field: a field distinct from the field of the SNARK.
In other words, the SNARK can prove relations over a prime field $\mathbb{F}_p$ and
using only relations over $\mathbb{F}_p$ we wish to prove the satisfiability of relations over a different field $\mathbb{F}_q$.
As a concrete example, applications within the Midnight circuits include emulating the Secp256k1 elliptic curve,
which requires the emulation of the base field:
$$
{\small \mathbb{F}_q = \mathbb{Z} / (\mathtt{0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141})}
$$
Over the native field, e.g. the BLS12-381 scalar field:
$$
{\small \mathbb{F}_p = \mathbb{Z} / (\mathtt{0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001})}
$$
### How to Emulate a Field
The techniques used in the Midnight circuits are based on [Casting out Primes: Bignum Arithmetic for Zero-Knowledge Proofs](https://eprint.iacr.org/2022/1470),
but with some additional optimizations (notably the use of a "unique zero" encoding).
The following is a general introduction to checking relations over a foreign field in the context of the Midnight circuits.
This is used for both the foreign field circuits and the foreign field elliptic curve circuits.
By "verifying a foreign field relation" we mean checking that a polynomial over the foreign field vanishes:
$$
f(x_1, \ldots, x_n) = 0 \mod q
$$
Where $f(X_1, \ldots, X_n) \in \mathbb{F}_q[X_1, \ldots, X_n]$ and $x_1, \ldots, x_n \in \mathbb{F}_q$ is some purported witness.
For instance, a foreign field multiplication gate can be expressed as:
$$
f(x_1, x_2, x_3) = x_1 \cdot x_2 - x_3
$$
The first step towards proving such relations using $\mathbb{F}_p$ is lifting the polynomial $f(X_1, \ldots, X_n)$ to the integers:
interpreting each coefficient as an integer in the range $[0, q)$, i.e. now view $f(X_1, \ldots, X_n) \in \mathbb{Z}[X_1, \ldots, X_n]$.
By witnessing the quotient $k = f(x_1, \ldots, x_n) / q$ the equality can now be checked over the integers:
$$
f(x_1, \ldots, x_n) - k \cdot q = 0 \in \mathbb{Z}
$$
The next observation is that as long as the expression on the right has norm less than $N$:
$$
|f(x_1, \ldots, x_n) - k \cdot q| < N
$$
Vanishing over the ring $\mathbb{Z}_N$ implies vanishing over $\mathbb{Z}$:
$$
f(x_1, \ldots, x_n) - k \cdot q = 0 \mod N \implies f(x_1, \ldots, x_n) - k \cdot q = 0
$$
Intuitively, this is because there is a unique representative of zero in $\mathbb{Z}_N$ in the range $(-N, N)$.
Moreover, if $N = m_1 \cdot m_2 \cdots m_n$ where $m_i$ are pairwise coprime, then by the Chinese Remainder Theorem:
$$
\forall i. f(x_1, \ldots, x_n) - k \cdot q = 0 \bmod m_i
$$
$$\iff$$
$$
f(x_1, \ldots, x_n) - k \cdot q = 0 \bmod N
$$
This leaves us with the same problem that we started with: checking (multiple) relations over
(not necessarily prime) moduli.
However, each individual $m_i$ can be *much smaller* than $q$. Furthermore, by setting $m_1 = p$ (the native modulus) we can efficiently check the first relation
using constraints over the native field $\mathbb{F}_p$: since the reduction modulo $p$ happens "for free" in the native field emulation.
For the *remaining congruences* we *again* lift the relations to the integers:
1. Witness the quotient $v_i = (f(x_1, \ldots, x_n) - k \cdot q) / m_i$.
2. Check: $(f(x_1, \ldots, x_n) - k \cdot q) - v_i \cdot m_i = 0 \in \mathbb{Z}$.
To *reduce the norm of the intermediate result*, we can reduce $f(X_1, \ldots, X_n) \in \mathbb{Z}[X_1, \ldots, X_n]$
and $q$ modulo $m_i$ *before lifting* the relation to the integers: this makes all the coefficients smaller than $m_i$, a relatively small number.
We omit the explicit reduction in the following discussion for clarity however it affects the analysis of the bounds required.
Finally, as we did before, instead of checking these relations over the integers, we check the relation modulo a sufficiently big modulus,
the natural choice of which is $p$ (the native modulus):
$$
f(x_1, \ldots, x_n) - k \cdot q - v_i \cdot m_i = 0 \mod p
$$
$$\iff$$
$$
f(x_1, \ldots, x_n) - k \cdot q - v_i \cdot m_i = 0 \mod p
$$
Which again holds as long as $|f(x_1, \ldots, x_n) - k \cdot q - v_i \cdot m_i| < p$.
For all the implications to hold,
range checks must be applied to the variables $x_1, \ldots, x_n, k, v_1, \ldots, v_n$ to ensure that:
1. $|f(x_1, \ldots, x_n) - k \cdot q| < N$
1. $|f(x_1, \ldots, x_n) - k \cdot q - v_i \cdot m_i| < p$ (after reducing the relation modulo $m_i$).
This sequence of observations is the basis for all foreign field emulation in the Midnight circuits,
relations include limb-wise multiplication, addition, canonicalization, elliptic curve arithmetic, etc.
We cover these in more detail in the following sections.
### Representation
Within the Midnight foreign field circuits, a foreign field element is represented as a vector of (range checked) $B$-nary limbs:
$$
x = (x_0, x_1, \ldots, x_{n-1})
$$
Representing the field element:
$$
\left( \sum_{i=0}^{n-1} x_i \cdot B^i \right) + 1 \mod q
$$
Notice the $+1$ at the end: this means that $0$ is encoded as $-1$ and
bounds on individual limbs will be chosen such that this is the *only representative* of zero:
The range checks ensure that the integer $\sum_{i=0}^{n-1} x_i \cdot B^i$
is in the range $[0, 2q)$ which has a unique representative of minus one ($q - 1$) implying that exactly one set of limbs can represent the zero in $\mathbb{F}_q$.
This is achieved by having more restrictive bounds on the most significant limb.
The statement above applies to "normalized/canonicalized" representations,
however within the Midnight circuits, intermediate results may not be normalized:
each limb may be in the more relaxed range $[-B^2, B^2]$.
This allows for more efficient operation, since the modular reduction can be deferred until:
1. An equality check with zero is required.
1. The relaxed bounds could be exceeded.
1. A relation, necessitating tighter bounds, must be checked using the technique described earlier.
For instance when adding foreign field elements, we simply add the limbs coordinate-wise.
We may do so until the relaxed bounds would otherwise be exceeded, at which point we can normalize the result --
which has the implied effect of accounting for the carries across the limbs.
### Relation: Normalization
Let's give a brief overview of the normalization procedure: which takes a representative satisfying the limb bounds $[-B^2, B^2]$ and
produces a normalized representative with the limb bounds $[0, B)$ and a value over the integers in the range $[0, 2q)$.
It corresponds to checking the following relation over $\mathbb{F}_q$:
$$
f(x_0, \ldots, x_{n-1}, z_0, \ldots, z_{n-1}) =
\left(\sum_{i=0}^{n-1} x_i \cdot B^i + 1\right) - \left(\sum_{i=0}^{n-1} z_i \cdot B^i + 1\right) \in \mathbb{F}_q
$$
In other words, the limbs $(x_0, \ldots, x_{n-1})$ and $(z_0, \ldots, z_{n-1})$ represent the same field element.
But with more relaxed bounds on $(x_1, \ldots, x_{n-1})$ than on $(z_1, \ldots, z_{n-1})$.
**Precondition:**
All the limbs of the input are in the range $[-B^2, B^2]$. i.e. $\forall i. x_i \in [-B^2, B^2]$
To account for negative limbs, each limb will be shifted into the positive range:
$$
\forall i. x_i + B^2 \in [0, 2B^2]
$$
And we check the following (clearly equivalent) relation over the field instead:
$$
0 =
\left(\sum_{i=0}^{n-1} (x_i + B^2) \cdot B^i + 1\right) - \left(\sum_{i=0}^{n-1} z_i \cdot B^i + 1\right) - \left( \sum_{i=0}^{n-1} B^i \cdot B^2 \right) \in \mathbb{F}_q
$$
Note that when lifting this relation to the integers, as described in the previous section,
intermediate reductions can be applied to reduce the norm
e.g. $\left( \sum_i B^i \cdot B^2 \right)$
can be reduced modulo $q$.
### Relation: Multiplication
**Precondition:** The operands have been normalized prior to the multiplication. \
In particular, this means that the limbs are guaranteed to be in the range $[0, B)$.
Intuitively, we want to check the following relation over the field:
$$
\begin{align*}
f(x_0, \ldots, x_{n-1}, y_0, \ldots, y_{n-1}, z_0, \ldots, z_{n-1}) &= \\
\left(1 + \sum_i x_i \cdot B^i\right) \cdot \left(1 + \sum_i y_i \cdot B^i\right) - \left(1 + \sum_i z_i \cdot B^i\right) \in \mathbb{F}_q
\end{align*}
$$
Expanding the relation, we get:
$$
0 =
\left(
\sum_{i, j} x_i \cdot y_j \cdot B^{i+j}
\right)
+
\left(
\sum_i x_i \cdot B^i
\right)
+
\left(
\sum_i y_i \cdot B^i
\right)
-
\left(
\sum_i z_i \cdot B^i
\right)
\in \mathbb{F}_q
$$
Which is the relation that we check over the field.
Note that, as always, before lifting the relation to the integers, we can reduce the norm of the relation by reducing the coefficients modulo $q$,
e.g. each term $B^{i+j}$ can be reduced modulo $q$ -- narrowing the range of the right hand expression substantially.
### Automatically Validating Norms and Parameters
In addition to the manual review of the foreign field gates,
we used [a small Rust program](https://gist.github.com/rot256/8846fe2509bee1e596538f6aa6577c90)
to automatically check the bounds for each gate and every set of supported parameters:
to double check that each foreign field gate (including the foreign ECC gates)
satisfies the prerequisite norm bounds, and every set of concrete parameters
such that the sequence of implications described at the start of this section holds.
Find the code here:
[Gist](https://gist.github.com/rot256/8846fe2509bee1e596538f6aa6577c90)
## BigUInt
In addition to the foreign field emulation, it also has the `biguint` module to emulate arbitrary large integers. It is a useful module for the use cases like RSA verification.
Similarly, it has a normalization process to correct the overflowed limbs. The process is relatively simpler than the one for foreign field emulation.
### Limb Representation
The module `biguint` can represent an arbitrary large integer represented by decomposed limbs. The default bound for each limb is $0 \leq x_i < B$, where $B$ has 96 bits.
A `biguint` can be decomposed and encoded into a circuit using the `assign_bounded` function, which takes the `nb_bits` to decide how many limbs to create and the bounds for each limb.
$$
X = \sum_{i=0}^{n-1} x_i \cdot B^i
$$
The bounds for the limbs are the same as $B$, except for the most significant limb.
$$
x_i = \begin{cases} 0 \leq x_i < B, & 0 \leq i < n-1 \\ 0 \leq x_i < B_{\text{msl}}, & \text{}i = n-1 \end{cases}
$$
Code for the limb bounds:
```rust
let mut limb_size_bounds = vec![LOG2_BASE; nb_limbs - 1];
limb_size_bounds.push((nb_bits - 1).rem(LOG2_BASE) + 1); // msl bound
```
Code for range check the limbs:
```rust
let limbs = value
.map(|x| big_to_limbs(nb_limbs as u32, &(BigUint::one() << LOG2_BASE), &x))
.transpose_vec(nb_limbs)
.into_iter()
.zip(limb_size_bounds.iter())
.map(|(limb_value, size_bound)| {
self.native_gadget.assign_lower_than_fixed(
layouter,
limb_value.map(big_to_fe::),
&(BigUint::one() << *size_bound),
)
})
.collect::, Error>>()?;
```
During operations, such as Addition or Multiplication, the value can overflow its limb's bound. In `biguint` module, there is also a normalization process to correct these limb overflows. This procedure relies on the bound tracker at the compile time to determine whether or not to normalize a `biguint`.
### Bound Adjustment
The basic operations Addition, Subtraction and Multiplication also calculate the limb bounds for the resulted `biguint`.
#### Addition and Subtraction Operations
In addition operation, when two limbs sum up, the resulted value can overflow the upper bound of them.
$$
z_i = x_i + y_i
$$
So it needs to add one bit to the upper bound in order to represent the carry bit during normalization.
$$
b_{z_i} = 1 + \max(b_{x_i},\ b_{y_i})
$$
Where $b$ represents the bound for the limbs.
```rust
limbs.push(self.native_gadget.add(layouter, &x.limbs[i], &y.limbs[i])?);
limb_size_bounds.push(bound_of_addition(
x.limb_size_bounds[i],
y.limb_size_bounds[i],
));
```
On the other hand, the subtraction simply picks the bounds of the left hand side, as it assumes the LHS is always greater than or equal to the RHS.
$$
b_{z_i} = b_{x_i}
$$
```rust
let res = self.assign_bounded(layouter, res_value, x.nb_bits())?;
let z = self.add(layouter, &res, y)?; // (x - y) + y
self.assert_equal(layouter, x, &z)?;
Ok(res)
```
#### Multiplication Operation
Supposed there are two `biguint`, $X$ and $Y$, their multiplication can be represented as $Z$.
$$X = \sum_{i=0}^{n-1} x_i \cdot B^i, \quad Y = \sum_{j=0}^{m-1} y_j \cdot B^j$$
$$X \cdot Y = \sum_{i=0}^{n-1} \sum_{j=0}^{m-1} x_i \cdot y_j \cdot B^{i+j}$$
$$Z = X \cdot Y = \sum_{k=0}^{n+m-2} z_k \cdot B^k$$
Let $Z_k$ represents the resulted limbs:
$$z_k = \sum_{\substack{k=i+j}} x_i \cdot y_j$$
As the bound for the $z_k$ is $b_{z_k}=b_{x_i} + b_{y_j}$, and there are accumulations to $z_k$, thus the bound should be accumulated as:
$$
b_{z_k} = 1 + \max(z_k,\ b_{x_i} + b_{y_i})
$$
```rust
for i in 0..x.limbs.len() {
for j in 0..y.limbs.len() {
let p = native_gadget.mul(layouter, &x.limbs[i], &y.limbs[j], None)?;
let p_bound = x.limb_size_bounds[i] + y.limb_size_bounds[j];
limbs[i + j] = native_gadget.add(layouter, &limbs[i + j], &p)?;
limb_size_bounds[i + j] = bound_of_addition(limb_size_bounds[i + j], p_bound);
}
}
```
### Normalization Process
Similar to the normalization in the foreign field module, it also need to run normalization procedure to convert the limbs with overflow values to fall within the expected bound.
The limb overflow can happen during the basic operations addition and multiplication. These operations also update each bound of the limbs in order to keep track of whether it needs to be normalized and how to normalize.
Before starting the normalization procedure, the `normalize()` check if the limb bounds representing a `biguint` is within the default bound, 96 bits.
```rust
pub fn is_normalized(&self) -> bool {
self.limb_size_bounds
.iter()
.all(|bound| *bound <= LOG2_BASE)
}
```
_Note that this seems not strictly aligning with the actual bound of the most significant limb. Since the operations, involving updating the bounds, will update bounds for all the limbs. Thus, a single update to the limb bounds can lead the `biguint` to be hit by the normalization process eventually. So far, it is fine this `is_normalized` check doesn't strictly align with the actual bound of the most significant limb._
First, it calculates the number of limbs based on the number of bits, which are derived from the max limb bounds.
```rust
let nb_limbs_output = x.nb_bits().div_ceil(LOG2_BASE) as usize;
```
Second, it goes through each potential overflow limb to calculate the `payload` of the limb. Note that the $carry_0$ is 0.
$$
\text{payload}_i = x_i + \text{carry}_{i}
$$
```rust
let payload = native_gadget.add(layouter, &carry, &x.limbs[i])?;
let payload_bound = bound_of_addition(carry_size_bound, x.limb_size_bounds[i]);
```
Third, it normalizes the limb $x_i$:
$$
x_i' = \text{payload}_i \bmod B
$$
Before proceeding to the next limb, it calculates the $carry_{i+1}$.
$$
\text{carry}_{i+1} = \left\lfloor \dfrac{\text{payload}_i}{B} \right\rfloor
$$
```rust
let (q, limb) = self.div_rem_native_by_base(layouter, &payload, payload_bound)?;
// Prepare the carry and its bound for the next iteration.
carry_size_bound = max(payload_bound, LOG2_BASE) - LOG2_BASE;
carry = q;
```
The `div_rem_native_by_base` function is used to calculate the quotient `q` and the remainder `limb` of the division by the base $B$.
$$
payload_i = q \cdot B + limb_{normalized}
$$
It relies on the `payload_bound` to range check the `q`, the $carry_{i+1}$.
After all limbs are processed, it ensures the final $carry$ is 0
## Hashes in Midnight
Before examining the details of the two hash functions implemented in Midnight, we first present the main API exposed by the Midnight library.
Each hash implementation should conform to two traits:
- `SpongeCPU` for off-circuit computation (i.e., computing the hash of a preimage outside the circuit and providing it as an instance to the circuit).
- `SpongeInstructions` for in-circuit operations.
Both traits are defined in `src/instructions/sponge.rs` and include three main functions:
- `init`: Initializes the state of the hash.
- `absorb`: Adds inputs to the state.
- `squeeze`: Produces a new output from the state.
Depending on the implementation, both `absorb` and `squeeze` may digest inputs, or only `squeeze` might perform this operation.
Additionally, the traits `HashCPU` and `HashInstructions` (also in `src/instructions/sponge.rs`) implement the full hash function. These functions take input, absorb it, squeeze it, and finally return the computed hash.
The `ZkStdLib` (`src/compact_std_lib.rs`) provides implementations for both hash functions via the `poseidon_gadget` and `sha256_chip` (details on their implementations are in the following sections). The library also exposes two utility functions for computing the respective hashes:
- `poseidon`: Accepts a reference to an array of `AssignedNative` field elements as input, computes the Poseidon hash, and returns the result.
- `sha256`: Accepts a reference to an array of `AssignedByte` as input, computes the SHA256 hash, and returns the result.
## Poseidon
Poseidon is a ZK-friendly hash function designed specifically for efficient implementation in zero-knowledge proof systems ([source](https://eprint.iacr.org/2019/458.pdf)). In the Midnight protocol, the Poseidon gadget serves multiple crucial functions:
- Exposed as a hash function for users (e.g., computing and proving knowledge of Poseidon hashes from messages).
- The hash function used for the Map gadget (Merkle Tree implementation).
- The hash function used for the Hash-to-Curve gadget.
Poseidon's key advantage lies in its algebraic nature. Unlike other hash functions like SHA256, which rely heavily on bitwise operations (expensive in ZK circuits), Poseidon operates purely through field arithmetic (additions and multiplications in finite fields). This makes it more straightforward and efficient to implement in ZK circuits.
### Parameters and Structure
Poseidon is highly parameterizable, with the following key parameters:
- **Field Characteristic**: Operations occur in a scalar field of size $q = p^k$, where:
- $p$ is a prime number.
- $k$ is a positive integer.
- The field must be compatible with the target elliptic curve.
- In Midnight, Poseidon is parameterized with the scalar field of one of the supported curves.
- **State Width ($t$)**: The size of the internal state, where $t \geq 2$. Larger widths allow higher throughput but increase circuit size.
- **Round Numbers**:
- $R_F$: Number of full rounds (split between start and end).
- $R_P$: Number of partial rounds (in the middle).
- These are security parameters chosen based on the desired security level.
- **Sponge Parameters**:
- **Rate ($r$)**: Number of field elements that can be absorbed/squeezed per round.
- **Capacity ($c$)**: A security parameter where $t = r + c$.
Poseidon implements the Hades design strategy, which optimizes performance through a structured combination of rounds:
- **Full Rounds**:
- Apply S-box ($x^\alpha$, typically $x^5$) to every state element.
- Provide strong security guarantees.
- Split between the beginning and end of the permutation.
- **Partial Rounds**:
- Apply S-box only to a single state element.
- Maintain security while significantly reducing computation costs.
- Comprise the middle portion of the permutation.
- **Round Structure** (for each round):
1. Add round constants.
2. Apply S-box (full or partial).
3. Apply MDS matrix (linear mixing).
Note that round constants and the MDS matrix depend on the selection of $q$.
### Sponge Construction
Poseidon uses the sponge construction to build a hash function:
- **Absorption Phase**:
- The input is split into $r$-sized chunks.
- Each chunk is absorbed into the rate portion of the state.
- The state undergoes a permutation between absorptions.
- **Squeezing Phase**:
- The output is extracted from the rate portion.
- The state undergoes a permutation between extractions.
- This process continues until the desired output length is reached.
### Padding
Poseidon requires input messages to be properly padded to ensure security and consistent processing. In the specific implementation, padding occurs whenever a new element needs to be squeezed from the sponge. At that point, the length of the data since the last squeeze is padded to meet the required size.
The padding rule is as follows:
1. Append a single field element `1` to the data.
2. Append zero field elements until the total length matches the required size.
### Poseidon Configuration in Midnight
The Midnight implementation of Poseidon supports the following fields:
- **`blstrs::Scalar`**: The scalar field of the BLS12-381 curve (parameters in `src/hash/poseidon/params/bls.rs`).
- **`pallas::Base`**: The scalar field of the Pallas curve (parameters in `src/hash/poseidon/params/pallas.rs`).
- **`vesta::Base`**: The scalar field of the Vesta curve (parameters in `src/hash/poseidon/params/vesta.rs`).
All three fields are configured to have 64 rounds (8 full rounds and 56 partial rounds). Their parameters were computed using the scripts from [this repository](https://github.com/daira/pasta-hadeshash). The parameter files include the round constants, the MDS matrix, and the inverse MDS matrix.
The implementation allows configurable state width (`T`) and rate (`RATE`), defined using const generics:
```rust
impl, D: Domain, const WIDTH: usize, const RATE: usize>
```
In practice, `WIDTH` is set to 3, and `RATE` is set to 2, meaning the capacity is 1. The S-box used is the power of 5.
The implementation supports different domains through the `Domain` trait:
- **`ConstantLength`**: For fixed-length inputs, padding adds zeroes to the input until the total length is a multiple of the rate. Poseidon encodes the constant length into the capacity element, ensuring that inputs of different lengths do not share the same permutation.
- **`VariableLength`**: For variable-length inputs, the initial capacity element is set to zero. Padding ensures that inputs of different sizes do not share the same permutation.
### Implementation
The Poseidon gadget implementation (`src/hash/poseidon/poseidon_gadget.rs`) defines the circuit state:
```rust
pub struct AssignedPoseidonState {
register: [StateWord; WIDTH],
queue: Vec>,
squeeze_position: usize,
}
```
- **`register`**: A fixed-size array of `StateWord` representing the current state (`WIDTH = 3`). The last element serves as the capacity, and the first two elements are the rate used for absorption and squeezing.
- **`queue`**: Holds pending inputs as `PaddedWord` (either a message word provided by the prover or a padding word fixed in the circuit parameters), processed in chunks of rate size (i.e., 2).
- **`squeeze_position`**: Tracks the current position in the rate portion during squeezing, ranging from 0 to `RATE-1` (i.e., 1). It resets to 0 after absorption.
The gadget implements the following functions:
- **`init`**: Initializes the state with `register = [0, 0, 1<<64]`, `queue = []`, and `squeeze_position = 0`.
- **`absorb`**: Adds inputs to the `queue` and updates the `squeeze_position`.
- **`squeeze`**: Extracts output values from the sponge state. There are two scenarios:
1. **Fast Path** (available rate elements): If `squeeze_position > 0`, the previous permutation has already been applied. The function returns the next available element from the rate portion and increments the position (wrapping around at `RATE`).
2. **Main Path** (process remaining queue): Applies padding, processes the queue in rate-sized chunks (i.e., permutes), and returns the first rate element.
The core logic for Poseidon is implemented by the `Pow5Chip` in `src/hash/poseidon/pow5.rs`. This chip defines the constraints for Poseidon’s permutation and implements the `permute` function. This function takes an `initial_state`, applies a permutation (assigning regions, cells, and enabling the required gates for each round), and returns a new state.
On top of the `Pow5Chip`, the `Pow5SpongeChip` is configured. Beyond `permute` (which directly calls the `Pow5Chip`'s `permute`), it also provides:
- **`initial_state`**: Loads constants for the initial state.
- **`add_input`**: Absorbs input into the `initial_state` and uses the `pad-and-add` gate from the `Pow5Chip` to constrain the resulting `state`.
- **`get_output`**: A straightforward function to retrieve the output.
Finally, the `Pow5State` structure implements functions for assigning and loading advice and constants: `full_round`, `partial_round`, `load`, and `round`.
### Gates of the `Pow5Chip`
The following figure depicts the columns defined in the `Pow5Chip`. The chip's configuration includes parameters such as `half_full_rounds` (full rounds / 2), `half_partial_rounds` (partial rounds / 2), `round_constants`, and `m_reg` (MDS matrix).
The chip has three gates:
1. **Full Round**.
2. **Partial Round**.
3. **Pad-and-Add**.
The `permute` function applies the first half of the full rounds, processes the partial rounds (applying the gate for two rounds per assignment), and finishes with the rest of the full rounds.
Let’s start with the **full round**. For each state element $\{0, 1, 2\}$, the following constraint is applied:
```rust
state[i]::next = (state[0]::cur + rc_a[0]::cur)^5 * m_reg[i][0] +
(state[1]::cur + rc_a[1]::cur)^5 * m_reg[i][1] +
(state[2]::cur + rc_a[2]::cur)^5 * m_reg[i][2]
```
This enforces that:
1. Round constants are added to each element.
2. The S-box ($x^5$) is applied to **all** elements.
3. MDS matrix multiplication is applied correctly.
4. The result matches the next row’s values.
The selector for this gate is enabled in the `full_round` function. Additionally, the assignment of constant values to the fixed column is handled by the `round` function.
Next, let’s proceed to the **partial round** gate, which is the most complex gate in the `Pow5Chip`. In this gate, two partial rounds are processed, where the S-box is applied only to the first state element. We can break this gate into three constraints.
**S-box Constraint for Round A**
The S-box for the first element during round A is constrained as:
```rust
(state[0]::cur + rc_a[0])^5 - partial_sbox::cur = 0
```
**State After Round A: Closure Definitions**
To define constraints for:
1. The second S-box for the first element combined with MDS multiplication.
2. Linear constraints for the other two states $\{1, 2\}$ (addition of constants and MDS for both rounds).
We introduce the following closures:
1. **`mid(idx)`**: Represents the state after round A:
```rust
mid(idx) = partial_sbox * m_reg[idx][0] + // First element (after S-box)
(state[1]::cur + rc_a[1]) * m_reg[idx][1] + // Second element (linear)
(state[2]::cur + rc_a[2]) * m_reg[idx][2] // Third element (linear)
```
2. **`next(idx)`**: Computes the pre-MDS value for position `idx`:
```rust
next(idx) = state[0]::next * m_inv[idx][0] +
state[1]::next * m_inv[idx][1] +
state[2]::next * m_inv[idx][2]
```
Here’s why:
After both rounds, we have values in the next row $[x, y, z]$ produced by MDS multiplication:
$$
[a, b, c] \cdot \text{MDS} = [x, y, z]
$$
Thus:
$$
[a, b, c] = [x, y, z] \cdot \text{MDS}^{-1}
$$
**Constraints for Round B**
1. **S-box Constraint for the First Element**:
The second S-box, including MDS multiplication for round B, is constrained as:
```rust
(mid(0) + rc_b[0])^5 - next(0) = 0
```
2. **Linear Constraints for Other Elements**:
The constraints for the second and third state elements are:
```rust
mid(1) + rc_b[1] - next(1) = 0
mid(2) + rc_b[2] - next(2) = 0
```
These constraints enforce:
1. Round A: S-box applied only to the first element, followed by MDS multiplication.
2. Round B: S-box applied only to the first element, followed by MDS multiplication.
**Pad-and-Add Gate**
Lastly, the **pad-and-add** gate handles absorption of inputs into the state. The table structure is as follows:
| `state[0]` | `state[1]` | `state[2]` | Description |
|----------|----------|----------|-------------|
| `prev_0` | `prev_1` | `prev_2` | Initial state |
| `input_0` | `input_1` | - | Input (only RATE elements) |
| `next_0` | `next_1` | `next_2` | Output state |
The constraints for updating the rate portion of the state are:
```rust
state[idx]::prev + state[idx]::cur - state[idx]::next = 0
// Equivalent to:
next_0 = prev_0 + input_0
next_1 = prev_1 + input_1
```
#### Constraints for the Capacity Element
The capacity element remains unchanged:
```rust
state[RATE]::prev - state[RATE]::next = 0
// Equivalent to:
next_2 = prev_2 // Capacity remains unchanged
```
This gate enforces that:
1. The rate portion elements are correctly updated with inputs.
2. The capacity element remains unchanged.
This gate is used in the `add_input` function.
### Implementation Considerations
The Poseidon implementation in the Midnight circuits was designed to be parameterized, introducing an extra layer of abstraction in some parts of the code. However, the current implementation is specifically designed and tested to work with the three supported curves, with the `WIDTH` parameter set to 3 and the `RATE` set to 2.
If these parameters are modified, the implementation might fail to work correctly or even become insecure. For example, the following line ([poseidon_gadget.rs:181](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/poseidon/poseidon_gadget.rs#L181)) would be incorrect when `RATE=1`:
```rust
state.squeeze_position = 1
```
To ensure correctness and generalization, it should instead be updated to:
```rust
state.squeeze_position = (state.squeeze_position + 1) % RATE
```
This adjustment ensures compatibility with different `RATE` values and avoids potential implementation errors.
## Sha256
Midnight implements the SHA-256 hash function in `hash/sha256`. Most of it is adapted from [zcash halo2 lib](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html). The Midnight implementation completes the implementation from the zcash (e.g., implementing the padding function). The main difference is that Midnight uses a smaller lookup table (called table11) that has about $2^{11}$ (instead of $2^{16}$) rows.
The SHA-256 works in several stages: padding, message scheduling, and compression. During padding, the input message is appended with a `1` bit, followed by enough `0` bits and a 64-bit representation of the message length to make its size a multiple of `512` bits. Next, the padded message is divided into 512-bit blocks, and each block undergoes message scheduling, where `64` words (each `32` bits) are generated. These words are derived from the block's data and earlier words using bitwise operations and modular arithmetic. Finally, the compression stage processes each word through a series of rounds, using a state of eight 32-bit variables initialized to specific constants. Each round applies mathematical operations, mixing the input data with the current state until a final hash value is produced by combining the updated state variables.
The SHA-256 involves many bitwise operations, which are inefficient in modulo arithmetic. The circuit uses a "spread" technique to speed up the computation.
### Spread
The spread operation maps an n-bit value to a 2n-bit value interleaved with zero bits. For example, given a 4-bit value `a = 1011`, the spread value `a` is `01_00_01_01`.
The spread value is useful in transforming some bitwise operations into field element operations. For instance, in some functions of SHA-256, it is necessary to compute the bitwise `xor` of `a` and `b`: `c = a xor b`. We can transform this by spreading the value `a` and `b` to get `a'` and `b'`. Then calculate `c' = a' + b`, where the `+` here represents the modulo addition.
For example, let `a = 1011` and `b = 0110`, then we should have `c = a xor b = 1101`. Using the spread values, we have `a' = 01_00_01_01` and `b' = 00_01_01_00`. Then `c' = a' + b' = 01_01_10_01`. To get `c`, we need to extract the even bits (starting at `0` from right to left), which is exactly `1101`. In this example, the spread value has an odd bit of zero as a "buffer" to hold the possible carry from an even bit.
The circuit uses a witness-and-check method to extract the even bits of `c`. It will witness two 4-bit values `c_even` and `c_odd` and enforce that `c' = spread(c_even) + 2*spread(c_odd)`. Then, we will have `c = c_even`. With the example above, we will have `c_even = 1101` and `c_odd = 0010`, and `c_even` is what we want.
The question then arises: How can we efficiently compute a value's spread? The answer is to use a lookup table, as described below.
### Spread Lookup Table
The circuit builds a static table with the original and corresponding spread values. Whenever it's needed to do a spread, the circuit just performs a lookup into the table and gets the result.
Below is an example of the table:
| t_tag | t_dense | t_spread |
|-------|------------|-------------|
| `0` | `0b0` | `0b0` |
| `1` | `0b0` | `0b00` |
| `1` | `0b1` | `0b01` |
| `2` | `0b00` | `0b0000` |
| `2` | `0b01` | `0b0001` |
| `2` | `0b10` | `0b0100` |
| `2` | `0b11` | `0b0101` |
| `....` | `......` | `......` |
| `11` | `0b00...00` | `0b00...00` |
| `11` | `0b00...01` | `0b00...01` |
| `....` | `......` | `......` |
| `11` | `0b11...1` | `0b0101...01` |
The `t_tag` column marks the bit length of the value and ensures tables of different bit lengths are independent. The `t_dense` column is for the original value, and the `t_spread` is for the spread value.
Table 16 has about $2^{16}$ rows and supports 16-bit dense value lookup. In the `with_lookup` function, it assigns `tag`, `dense`, and `spread` into one row, forcing that row to exist in the lookup table. As the `tag` column is an advice column, the `tag` value needs to be range-checked to constrain the length of the dense value.
Table 11 has about $2^{11}$ rows and supports 11-bit dense value lookup. This efficiently reduces the row count in the table. To get the spread of a larger value, it will need to split the value into two pieces that are within 11-bit, do the lookup separately, and combine the spread pieces into one spread value. For example, in order to spread a 13-bit value, it will split it ([decomposition.rs:244](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/decomposition.rs#L244)) to 10-bit and 3-bit pieces and then do the lookup. As in Table 11, the `tag` column is a fixed column; the `tag` value doesn't need an extra range check.
### Implementation of SHA-256
In the following, we describe the implementation of SHA-256 using the Table 16 spread table. The main differences between Table 16 and Table 11 have been described previously. In the implementation, the logic of Table 11 is implemented in the file `src/hash/sha256/table11/decomposition.rs`. Furthermore, in Table 11 we don't require range checks in the tag column as it is a fixed column, and the checks of the validity of dense/spread are being saved in a postponed vector and checked later on.
#### Table 16 Tags
As already mentioned, Table 16 uses tags to range-check the number of bits for a dense value. The following code demonstrates the ranges supported and their respective tags.
```rust
pub fn get_tag(input: u16) -> u8 {
let input = input as usize;
if input < BITS_4 {
0
} else if input < BITS_7 {
1
} else if input < BITS_10 {
2
} else if input < BITS_11 {
3
} else if input < BITS_13 {
4
} else if input < BITS_14 {
5
} else {
6
}
}
```
If a value contains 11 bits, then the tag should be `0`, `1`, `2`, or `3`; thus, in the code, we will range-check it between `0` and `3`.
#### Spec Mapping
Here are the columns used in the code renamed to match the [spec](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html). This will help us map the implementation to the actual specification.
```rust
a_0 = lookup_inputs.tag;
a_1 = lookup_inputs.dense;
a_2 = lookup_inputs.spread;
a_3 = extras[0];
a_4 = extras[1];
a_5 = message_schedule;
a_6 = extras[2];
a_7 = extras[3];
a_8 = extras[4];
a_9 = extras[5];
```
#### Message Schedule
Next, we will cover the message schedule process. When we call the `compress` function ([table16.rs:239-240](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L239-L240)), we will provide as input some initial state and some inputs. The input is composed of `AssignedBlockWord`s (32-bit words), and we have 16 such words (i.e., a 512-bit chunk).
The first step is to call the `message_schedule.process` function ([message_schedule.rs:319](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L319)). This function aims to create a 64-entry message array where w[0..15] are the 16 input words, and the rest are computed using the following loop.
```python
for i from 16 to 63
s0 := (w[i-15] rightrotate 7) xor (w[i-15] rightrotate 18) xor (w[i-15] rightshift 3)
s1 := (w[i-2] rightrotate 17) xor (w[i-2] rightrotate 19) xor (w[i-2] rightshift 10)
w[i] := w[i-16] + s0 + w[i-7] + s1
```
The code's output will be an array of 64 `MessageWord`s and an array of tuples containing the halves of each word (16-bit low and high parts).
Let's proceed to understand how those rows will be assigned and constrained. Firstly, we need to understand how the region of the message schedule is split. The implementation ([schedule_util.rs:12-55](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_util.rs#L12-L55)) specifies how to split the region into subregions. In summary, we have the following subregions:
* Subregion 0: Handles $W_0$ (first word)
* Uses `DECOMPOSE_0_ROWS` (2 rows)
* Subregion 1: Handles $W_1$ to $W_{13}$
* Each word needs `DECOMPOSE_1_ROWS` + `SIGMA_0_V1_ROWS` (6 rows)
* Subregion 2: Handles $W_{14}$ to $W_{48}$
* Each word needs `DECOMPOSE_2_ROWS` + `SIGMA_0_V2_ROWS` + `SIGMA_1_V2_ROWS` (11 rows)
* Subregion 3: Handles $W_{49}$ to $W_{61}$
* Each word needs `DECOMPOSE_3_ROWS` + `SIGMA_1_V1_ROWS` (6 rows)
* Subregion 4: Would handle $W_{62}$ to $W_{63}$
* Each word needs `DECOMPOSE_0_ROWS` (2 rows)
In the process function, we first enable ([message_schedule.rs:339-371](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L339-L371)) all the appropriate gates based on the above separation. The `s_decompose_0` gate is enabled for every word, and then, for each region, we enable the extra gates we need. For example, for subregion 2 (words 14 to 49), we will enable `s_decompose_2`, `s_lower_sigma_0_v2`, `s_lower_sigma_1_v2`, and `s_word`. Before explaining the gates, let's explain how we perform the assignments and why we have split subregions this way.
**Note:** In the tables below that we demonstrate how cells are assigned and constraints are applied, we use the follow rules:
* Red cells represent cells used by the first gate.
* Green cells represent cells used by the second gate.
* Blue cells represent cells used by the third gate.
* Yellow cells represent cells used by the fourth gate.
* White cells represent cells that are not used by any gate but were assigned by one of the functions that enabled any of the gates that are involved.
* Grey cells represent cells that are assigned and used by functions/gates that were not described in the description of the specific section.
#### Assign the First 16 Words
The first step ([message_schedule.rs:374-378](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L374-L378)) is to assign the first 16 words and also split them into halves. To do so, we use the function `assign_word_and_halves` that will get the row of the current word and the word value and will assign `w_lo` to `a3`, `w_hi` to `a4`, and `word` to `a5`. Note that the values that were assigned are out-of-circuit. Therefore, we have to check these assignments against the original inputs (e.g., [table16.rs:267](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L267)). The `s_decompose_0` gate ([schedule_gates.rs:41-50](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L41-L50)) will also be responsible for checking that the decomposition of each word happened correctly. The following table depicts the row for the `s_decompose_0` gate.
#### Subregion 1 ($W_1$ to $W_{14}$)
Next is subregion 1. This subregion is required to decompose words and compute $\sigma_0$ values for the words from 1 to 14. The next subregion will handle the other words and computation of $\sigma_0$. We need this subregion because this is the only operation we apply in words $W_1$ to $W_{14}$. The function `assign_subregion1` ([subregion1.rs:87](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion1.rs#L87)) will first decompose a word into four pieces: `a` (3-bit), `b` (4-bit), `c` (11-bit), and `d` (14-bit), according to the spec. For `a` and `b`, we will keep their dense form; for `c` and `d`, we will keep their spread form. Specifically, `decompose_subregion1_word` ([subregion1.rs:113](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion1.rs#L113)) assigns `a` to column `a3` / `row + 1` (from the current `row` word), `b` to column `a4` / `row + 1`. Then, it will look up `c` into `a1` (tag) / `a2` (dense) / `a3` (spread) in `row + 1` and `d` in `row`.
The `lower_sigma_0` function ([subregion1.rs:171](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion1.rs#L171)) will take as input the index of the word, `a`, `b`, `spread_c`, and `spread_d`. It will skip three rows. It first copies `a` into `a5` in `row + 1` and witnesses its spread value into `a6` / `row + 1`. Then it copies `b` into `a6` in the current `row`, split it into `b_lo` (assigned into `a3` / `row - 1`) and `b_hi` (assigned into `a5` / `row - 1`) and witness its spread values into `a4` / `row - 1` and `a6` / `row - 1`. Next, it copies `spread_c` into `a4` in the current row and `spread_d` into `a5` in the same row. Then, it computes `r` using `xor_lower_sigma_0` ([subregion1.rs:47](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion1.rs#L47)) which is basically the output of the $\sigma_0$ function. Finally, it splits `r` into $R_0^{even}$, $R_0^{odd}$, $R_1^{even}$, $R_1^{odd}$ and uses `assign_sigma_outputs` ([table16.rs:463](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L463)) that calls `assign_spread_outputs` ([table16.rs:411](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L411)), which will do the following 4 lookups into columns `a1`, `a2`, and `a3`:
* lookup $R_0^{even}$ in `row - 1`
* lookup $R_0^{odd}$ in `row`
* lookup $R_1^{even}$ in `row + 1`
* lookup $R_1^{odd}$ in `row + 2`
Finally, it copies the spread format of $R_1^{odd}$ in column `a3` in the current `row` and returns `r_0` and `r_1` in their dense form.
Note that `lower_sigma_0` returns $R_0^{even}$ and $R_1^{even}$ in dense form.
The following gates are enforced in this subregion (on top of `s_decompose_0`):
* `s_decompose_1` ([schedule_gates.rs:54](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L54)) is used to check the correct decomposition of a word into pieces `a`, `b`, `c`, and `d`. Note that `a` and `b` are not range-checked as they have already been range-checked in `s_lower_sigma_0`.
* `s_lower_sigma_0` ([schedule_gates.rs:156](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L156)) first range-checks and checks the spreads of the variables a and b. Then, it checks if the spread witness values (spread values for `r0_even`, `r0_odd`, `r1_even`, and `r1_odd` that compose the output of `lower_sigma_0`) equals $(X \ggg 7) \oplus (X \lll 14) \oplus (X \gg 3)$, where $X$ is our word and we follow the equations described in the spec. Note that we provide a complete explanation of one of a Sigma functions later in this document. The others follow similar techniques and logic.
The table for the first row will look like this:
#### Subregion 2 ($W_{14}$ to $W_{49}$ -- produces $W_{16}$ to $W_{50}$)
Recall that from subregion 1, we have computed the $\sigma_0$ values for the words from 1 to 14, and we have returned $R_0^{even}$ and $R_1^{even}$ in dense form. In the function `assign_subregion2` ([subregion2.rs:164](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L164)), we pass those $\sigma_0$ values, we assign the new words from $W_{16}$ to $W_{49}$ along with their decomposed halves, we make all the assignments and add all the constraints required, and finally, we return the output of `sigma_0_v2` on $W_{36}$ to $W_{49}$ to use them in subregion 3.
In `assign_subregion2`, the closure to compute a new word is: $W_i = \sigma_1(W_{i - 2}) + W_{i - 7} + \sigma_0(W_{i - 15}) + W_{i - 16}$, e.g., $W_{16} = \sigma_1(W_{14}) + W_9 + \sigma_0(W_1) + W_0$.
To compute the new words, we are going to use the following:
* `sigma_0(W_[1..14])` (from subregion 1) will be used to get the new `W_[16..29]`
* `sigma_0_v2(W_[14..36])` will be used to get the new `W_[29..51]`
* `sigma_1_v2(W_[14..49])` will be used to get the `W_[16..51]`
The closure `new_word` ([subregion2.rs:190](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L190)) takes as input an index and `sigma_0_output`. This closure will create new words for `index + 2` ($W_{i+2}$). For example, when we are at index 14 (i.e., word at index 14 -- $W_{14}$), we will produce a new word for $W_{16}$. For the first 13 indexes, we are going to create new words. We will use the $\sigma_0$ values from subregion 1. Then, for each index, we will compute $\sigma_0$ that will be used to produce words at $W_{i+15}$ and $\sigma_1$ that will be used to produce $W_{i+2}$ (i.e., the word we are producing in the iteration). Note that for indexes `27..49`, we will use $\sigma_0$, which was produced when looping through indexes `14..27`.
The function `decompose_word` ([subregion2.rs:299](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L299)) is responsible for decomposing a word similar to the previous decompose functions. Specifically, it will assign the following cells:
* `a` will be assigned in column `a3` / `row - 1`
* `b` will be looked up at `row + 1`
* `c` will be assigned in column `a4` / `row - 1`
* `d` will be looked up at the current `row`
* `e` will be assigned in `a3 / row + 1`
* `f` will be assigned in `a4 / row + 1`
* `g` will be looked up at `row - 1`
Next, `lower_sigma_0_v2` ([subregion2.rs:426](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L426)) computes $\sigma_0$ values for the current word ($W_i$) -- that will be used in a next iteration. This function works at `row + 3` from the current row. First, it calls `assign_lower_sigma_v2_pieces` ([subregion2.rs:363](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L363)), which is responsible for copying and constraining the pieces of the decomposed word to use them in either `lower_sigma_0_v2` or `lower_sigma_1_v2`. This will lead to the following:
* `a` will be copied into `a3` / `row + 1`
* `spread_a` will be assigned into `a4` / `row + 1`
* `b` will be copied into `a6` / `row`
* `b_lo` will be assigned into `a3` / `row - 1`
* `spread_b_lo` will be assigned into `a4` / `row - 1`
* `b_hi` will be assigned into `a5` / `row - 1`
* `spread_b_hi` will be assigned into `a6` / `row - 1`
* `c` will be copied into `a5` / `row + 1`
* `spread_c` will be assigned into `a6` / `row + 1`
* `spread_d` will be copied into `a4` / `row`
* `e` will be copied into `a7` / `row`
* `f` will be copied into `a7` / `row + 1`
* `spread_g` will be copied into `a5` / `row`
Then, it will compute the output of $\sigma_0^{v2}$ according to the spec (`r`), calculate $R_0^{even}$, $R_0^{odd}$, $R_1^{even}$, $R_1^{odd}$, and will perform the following operations by using `assign_sigma_outputs`:
* It will lookup $R_0^{even}$ in `row - 1`
* It will lookup $R_0^{odd}$ in `row`
* It will lookup $R_1^{even}$ in `row + 1`
* It will lookup $R_1^{odd}$ in `row + 2`
* It will copy $\text{spread}(R_1^{odd})$ in `a3` / `row`
The exact same process will be followed for $\sigma_1^{v2}$ by calling `lower_sigma_1_v2`.
You can see the resulting table below.
Next, it will compute the new word and its carry, and it will witness it at:
* $W_{ni}$ in column `a5` at the row of $W_{ni-16}$ + 1
* E.g., $W_{16}$ in column `a5` at the row of $W_0$ + 1
* $\text{carry}_{ni}$ in column `a9` at the row of $W_{ni-16}$ + 1
* E.g., $\text{carry}_{16}$ in column `a9` at the row of $W_0$ + 1
Finally, it uses `assign_word_and_halves` ([schedule_util.rs:154](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_util.rs#L154)). This function will assign the new word and its halves in the `ni`. Specifically:
* It will assign $W_{ni}^{lo}$ in column `a3` of the row of the new word.
* It will assign $W_{ni}^{hi}$ in column `a4` of the row of the new word.
* It will assign $W_{ni}$ in column `a5` of the row of the new word.
Note that for words $W_0$ to $W_{16}$, this has happened in the `process` function ([message_schedule.rs:374](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L374)) of message schedule.
The following gates are enforced in this subregion (on top of `s_decompose_0`):
* `s_decompose_2` ([schedule_gates.rs:82](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L82)) is used to check the correct decomposition of a word to `a`, `b`, `c`, `d`, `e`, `f`, and `g` pieces. Note that `a` and `c` are range-checked in `s_lower_sigma_0_v2` and `s_lower_sigma_1_v2`.
* `s_lower_sigma_0_v2` ([schedule_gates.rs:274](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L274)) first range-checks `a`, `c`, `b_lo`, and `b_hi`while also checking their spread values. Next, it checks if the spread values we have witnessed in `r0_even`, `r0_odd`, `r1_even`, and `r1_odd` equal the expected result according to the spec.
* `s_lower_sigma_1_v2` ([schedule_gates.rs:340](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L340)) does pretty much the same as `s_lower_sigma_0_v2` but for $\sigma_1$.
* The `s_word` gate ([schedule_gates.rs:13](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L13)) checks if the computed words for $W_{16}$ to $W_{63}$ are correct according to the spec (i.e., $W_i = \sigma_1(W_{i-2}) \oplus W_{i-7} \oplus \sigma_0(W_{i-15}) \oplus W_{i-16}$) -- The cells for new word are depicted with gray color in the figure and are from index 30.
#### Subregion 3 ($W_{49}$ to $W_{62}$ -- produces $W_{51}$ to $W_{63}$)
The logic for `assign_subregion3` ([subregion3.rs:86](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion3.rs#L86)) is almost the same as for `assign_subregion2`. This function takes as input all the required $\sigma_0$ values. In the following, we will cover the differences with subregion 2.
Firstly, the `decompose_subregion3_word` ([subregion3.rs:202](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion3.rs#L202)) follows a logic similar to `decompose_subregion1_word`, but for different pieces.
Next, the logic of `lower_sigma_1` ([subregion3.rs:247](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion3.rs#L247)) closely follows the logic of `lower_sigma_0`, but implements a different function. The rest of the code closely follows the logic of the `assign_subregion2` function.
The following gates are enforced in this subregion on top of `s_decompose_0`:
* `s_decompose_3` ([schedule_gates.rs:121](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L121)) similar to `s_decompose_1`.
* `s_lower_sigma_1` ([schedule_gates.rs:209](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_gates.rs#L209)), similar to `s_lower_sigma_0`, but constraints the $\sigma_1$ function. Additionally, it range-checks and enforces the proper spread for `b_lo`, `b_mid`, `b_hi`, `c`, and checks `b`.
For reference, here is the table for $W_{49}$:
#### The Sigma Function
The sigma function is used both in the message schedule and compression process. Specifically, lower Sigma ($\sigma_0$ and $\sigma_1$) are used in the message schedule, and upper Sigma ($\Sigma_0$ and $\Sigma_1$) are used in compression. As these sigma functions work in the same way (only have a difference in the shifting number), here we only introduce $\sigma_0$. By definition:
$$
\sigma_0(X) = (X \ggg 7) \oplus (X \ggg 18) \oplus (X \gg 3)
$$
Where $X$ is the 32-bit word. It is equivalent to
$$
(X \ggg 7) \oplus (X \lll 14) \oplus (X \gg 3)
$$
To perform the shifting, we can split $X$ into smaller pieces. To perform $X \ggg 7$, we can split $X$ at the 7-th bit and get 7-bit number $x_1$ and 25-bit number $x_2$. Then we have $(X \ggg 7) = x_1 + 2^7x_2$. Similarly, for $X \lll 14$, we can split $X$ into 14-bit numbers and 18-bit numbers. For $X \gg 3$, we can split $X$ into 3-bit numbers and 29-bit numbers. Splitting three times together we will have 4 pieces: $(a, b, c, d)$ of lengths $(3, 4, 11, 14)$. The figure below is taken from the [halo2 book](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html#%CF%83_0-function):
Then we have
$$(X \ggg 7) = c + 2^{11}d + 2^{25}a + 2^{28}b$$
$$(X \lll 14) = d + 2^{14}a + 2^{17}b + 2^{21}c$$
$$(X \gg 3) = b + 2^{4}c + 2^{15}d$$
The last step is to compute the xor of the three shifted values. The code takes the spread form of $X$ and splits that into spread pieces: $(a', b', c', d')$. Then get the spread form of shifted values and perform the xor operation by adding these values: $spread(X \ggg 7) + spread(X \lll 14) + spread(X \gg 3)$.
Finally, it extracts the dense value from the spread result [in the way introduced before](#spread-lookup-table)
### Compression
In this section, we will review the spec and code for the compression phase of Sha256. Thus, compression has two phases.
#### Initialize
First, we need to initialize the state with the initialization vector (iv).
That is the role of the `initialization_vector` function ([table16.rs:217](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16.rs#L217)). This function will then call `initialize_with_iv` ([compression.rs:937](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression.rs#L937)) that will assign a new region for the initial state, will do the assignments by calling the `initialize_iv` function ([subregion_initial.rs:16](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_initial.rs#L16)), and will return a variable containing the state that is composed of `StateWord`s ([compression.rs:467](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression.rs#L467)).
#### Decompose Variables
The `initialize_iv` function is responsible for decomposing and assigning into the table the initial values for the variables `A`, `B`, `C`, `E`, `F`, `G`, and assigning the halves (low and high) of the dense format of the variables `D` and `H`. A neat reference for visualizing the result of this function is the table [Initial round](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html#initial-round) from the specification. This table has 31 rows. In row 0, we decompose variable `E`. Note that in the code, we select the rows by using the `get_round_row` function ([compression_util.rs:100](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L100)) and adding lines based on the variable we are handling. Now, to decompose variable `E`, we are calling the function `decompose_iv_e` ([compression_util.rs:390](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L390)). This function will first load the value of IV for `E`, then it will select the proper row, and then it will use the `assign_word_halves_fixed` function ([compression_util.rs:1064](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L1064)). This function will break the 32-bit word into two 16-bit variables (low and high), then it will compute the spread format for both of them, and it will assign to the cells at column `a7` and `a8` in the current row the dense and spread for the low part, and in the next row in the same columns for the high part. After calling `assign_word_halves_fixed`, we call the `decompose_efgh` function ([compression_util.rs:399](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L399)) that will enable the `s_decompose_efgh` gate ([compression_gates.rs:87](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L87)), do all the proper assignments and lookups, and will return an `EfghVar` ([compression.rs:179](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression.rs#L179)).
This will break the variable into `(6,5,14,7)` bit-chunks, respectively. The first part is split into 3 (low) and 3 (high), and the second into 2 (low) and 3 (high).
According to the docs, we need to break the variable into those pieces because:
- In `Σ_1(E)`, we need `E` to be split into pieces `(a,b,c,d)` of lengths `(6,5,14,7)` bits, respectively (counting from the little end), as well as their spread forms.
- `Ch(E,F,G)` requires the bits of each input to be in spread form. For `E`, we can reuse the pieces from `Σ_1(E)`. Since `F` and `G` are assigned from `E` and `F,` respectively, in each round, we also have the same pieces in earlier rows. We align the columns to make it efficient to copy-constrain these forms where they are needed.
We will see why this is the case later on.
The `s_decompose_efgh` gate is responsible for (1) range-checking the inputs, (2) checking if the spread value is correct, (3) checking for both the dense and spread formats if the sum of the pieces is equal to the dense and spread form of the original word. To do so, for `a_lo`/`a_hi`/`b_low`/`b_hi`, it uses `three_bit_spread_and_range` ([gates.rs:99-100](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/gates.rs#L99-L100)) and `two_bit_spread_and_range` ([gates.rs:73](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/gates.rs#L73)) which first checks if dense is in the correct range and then if the provided dense is the correct one for the spread. For `c` and `d`, we have performed two lookups ([compression_util.rs:337](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L337)) in `decompose_efgh.` This means that, indeed there exists a row in the lookup table that contains `tag,dense,spread.` What is missing here is that we use an appropriate tag to enforce the range check. This happens in the gate ([compression_gates.rs:126](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L126)). For `c`, we check that the tag is in `{0,1,2,3,4,5}` as a 14-bit value; for `d`, we check that the tag is in `{0,1}` as a 7-bit value.
The resulting table for `decompose_iv_e` will look like this:
Next, we call `decompose_iv_f` ([subregion_initial.rs:167](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_initial.rs#L167)) and `decompose_iv_g` ([subregion_initial.rs:195](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_initial.rs#L195)). Those functions are similar to `decompose_iv_e,` but they chose other rows and also return a simple `RoundWord` composed of dense and spread halves, instead of an `EfghVar`. Finally, for variable `h`, we just use `assign_word_halves_dense_fixed` to assign the low and high halves of its dense form in column `a7` in rows 10 and 11 of the region.
Similar logic is followed for variables `A`, `B`, `C`, and `D`. Note that `AbcdVar` ([compression.rs:88](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression.rs#L88)) is split accordingly:
- In `Σ_0(A)`, we need `A` to be split into pieces `(a,b,c,d)` of lengths `(2,11,9,10)` bits respectively (counting from the little end), as well as their spread forms. Note that c is split into three parts of 3 bits each (i.e., `lo,` `mid,` `hi`).
- `Maj(A,B,C)` requires the bits of each input to be in spread form. For `A`, we can reuse the pieces from `Σ_0(A)`. Since `B` and `C` are assigned from `A` and `B`, respectively, in each round. We, therefore, also have the same pieces in earlier rows. We align the columns to make it efficient to copy-constrain these forms where they are needed.
With that, we have finished the `initialize_iv` function, initialized the state with the original values, and assigned the values to the proper cells. The logic for `initialize_state` ([subregion_initial.rs:61](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_initial.rs#L61)) is pretty much the same, with the addition that this function consumes a previous state. Hence, equality constraints are applied between the dense values from the cells of the previous state and the values in the newly assigned cells. Specifically, what it changes is that the `decompose_{a,b,c,d,e,f,g,h}_iv` functions are using `assign_word_halves_fixed`, whereas `decompose_{a,b,c,d,e,f,g,h}` are using `assign_word_halves` and then constrain the cell that it gets the value from to equal the cell that assigns the values to (the dense halves). Note that for `decompose_{a,e}` this is required only in the first round because later it is enforced in the code ([subregion_main.rs:87](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_main.rs:88-93` and `src/hash/sha256/table16/compression/subregion_main.rs#L87)).
#### Compress
The `compress` function ([compression.rs:972](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression.rs#L972)) gets as input some initialized state and a message schedule (i.e., 64 words in halves). The function will first apply the initialized state, loop over the 64 words, and apply a compression round for each one. In the end, the resulting state is the output that we can then digest.
The main logic is implemented in the `assign_round` function ([subregion_main.rs:13](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_main.rs#L13)) that takes as input the round number, the previous state that we require in the last round, the current state (in the first round, it is the same as the previous state), and the halves of the word we are processing in this round. The function will return the new state that will be used in the next round as the state input.
Let's now analyze what is happening when assigning a round. The following operations are being applied.
#### $\Sigma_1$
First, the $\Sigma_1$ function is applied that inputs the pieces of `e` from the state (look at `decompose_efgh`), the round index, and computes `sigma_1`. The `assign_upper_sigma_1` function ([compression_util.rs:480](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L480)) does the following:
* It copies $\text{spread}E_0a^{lo}(6)$ into column `a3` / `row + 1`
* It copies $\text{spread}E_0a^{hi}(6)$ into column `a4` / `row + 1`
* It copies $\text{spread}E_0b^{lo}(5)$ into column `a3` / `row - 1`
* It copies $\text{spread}E_0b^{hi}(5)$ into column `a4` / `row - 1`
* It copies $\text{spread}E_0c^{hi}(14)$ into column `a5` / `row`
* It copies $\text{spread}E_0d^{hi}(7)$ into column `a4` / `row`
Next, it computes `r` by following the spec definition for $\Sigma_1$, and it calculates $R_0^{even}$, $R_0^{odd}$, $R_1^{even}$, $R_1^{odd}$. Then, it calls `assign_sigma_outputs` that calls `assign_spread_outputs` ([table16.rs:411](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16.rs#L411)) and performs the following operations:
* It will lookup $R_0^{even}$ in `row - 1`
* It will lookup $R_0^{odd}$ in `row`
* It will lookup $R_1^{even}$ in `row + 1`
* It will lookup $R_1^{odd}$ in `row + 2`
* It will copy $\text{spread}(R_1^{odd})$ in `a3` / `row`
Then, it will finally return $R_0^{even}$ and $R_1^{even}$ in dense form.
On top of that, for $\Sigma_1$, the `s_upper_sigma_1` gate ([compression_gates.rs:201](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L201)) will be enabled. This gate checks that the spread witnessed values of `r` equals $\Sigma_1$ according to the spec.
This assign function will result in the following table:
#### $Ch$ function
The $Ch$ function is defined as follows: $Ch(E,F,G) = (E \land F) \oplus (\neg E \land G)$. We refer the interested reader to the [spec](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html#ch-function) for understanding how we can implement $Ch$ efficiently. Here, we are going to discuss the implementation. So, first of all we have all $E,F,G$ in their spread form. To implement that operation we want to compute $Ch = P = \text{spread}(E) + \text{spread}(F)$ and $Ch_{neg} = Q = (evens - E) + G = ((\text{spread}(2^{32} - 1) - \text{spread}(E)) + \text{spread}(G)$.
The `assign_ch` function ([compression_util.rs:565](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L565)) performs the computation and the assignments for the first part (i.e., $P$). Specifically, it does the following:
* It copies $\text{spread}(E^{lo})$ into column `a3` / `row - 1`
* It copies $\text{spread}(E^{hi})$ into column `a4` / `row - 1`
* It copies $\text{spread}(F^{lo})$ into column `a3` / `row + 1`
* It copies $\text{spread}(F^{hi})$ into column `a4` / `row + 1`
Next, it computes `p` by following the spec definition (i.e., adding the spread halves of $E$ and $F$), and it calculates $P_0^{even}$, $P_0^{odd}$, $P_1^{even}$, $P_1^{odd}$. Then, it calls `assign_ch_outputs` which in turn calls `assign_spread_outputs` (it performs all the necessary lookups and assigns $P_1^{odd}$) and returns the tuple ($P_0^{odd}$, $P_1^{odd}$).
Additionally, the gate `s_ch` ([compression_gates.rs:244](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L244)) is enabled, which checks if the witnessed values have been computed correctly according to the spec.
The `assign_ch_neg` function ([compression_util.rs:611](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L611)) follows a similar logic. The main addition is that the implementation computes and assigns $\text{spread}(E_{neg}^{lo})$ and $\text{spread}(E_{neg}^{lo})$ ([compression_util.rs:642-668](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L642-L668)). Accordingly, in the respective gate, we have an additional check ([compression_gates.rs:287](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L287)).
#### $\Sigma_0$
We skip the explanation of $\Sigma_0$ as it is almost identical to $\Sigma_1$.
#### Maj function
The Maj function is defined as follows: $Maj(A,B,C) = (A \land B) \oplus (A \land C) \oplus (B \land C)$. As we already have $A,B,C$ in spread form, we can compute $M = \text{spread}(A) + \text{spread}(B) + \text{spread}(C)$, then we witness the $M_i^{even}$ and $M_i^{odd}$ bits of the halves of $M$, and the result of $Maj$ is $M_i^{odd}$. To make it work correctly, we also need a gate to constrain the witnessed values.
Let's see how this function is implemented. Firstly, we use the `assign_maj` function ([compression_util.rs:714](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L714)) which does the following:
* It copies $\text{spread}(A^{lo})$ into column `a4` / `row - 1`
* It copies $\text{spread}(A^{hi})$ into column `a5` / `row - 1`
* It copies $\text{spread}(B^{lo})$ into column `a4` / `row`
* It copies $\text{spread}(B^{hi})$ into column `a5` / `row`
* It copies $\text{spread}(C^{lo})$ into column `a4` / `row + 1`
* It copies $\text{spread}(C^{hi})$ into column `a5` / `row + 1`
Next, it computes `m` by following the spec definition (i.e., adding the spread halves of $A$, $B$, and $C$), and it calculates $M_0^{even}$, $M_0^{odd}$, $M_1^{even}$, $M_1^{odd}$. Then, it calls `assign_maj_outputs`, which in turn calls `assign_spread_outputs` (it performs all the necessary lookups and assigns $M_1^{odd}$). Lastly, it returns the tuple ($M_0^{odd}$, $M_1^{odd}$).
Additionally, the gate `s_maj` ([compression_gates.rs:312](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L312)) is enabled which checks if the witnessed maj values have been computed correctly according to the spec.
#### $H'$
In a round $i$, we compute $H'$ as $H + Ch(A,B,C) + \Sigma_1(E) + K_i + W_i$. This logic is implemented in function `assign_h_prime` ([compression_util.rs:772](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L772)) that takes as input the `round_idx` round number, `h` (from the `state`), `ch` (computed by `assign_ch`), `ch_neg` (computed by `assign_ch_neg`), `sigma_1` (as computed by `assign_upper_sigma_1`), `ROUND_CONSTANT[round_idx]` ($K_i$), and `schedule_word` ($W_i$). The function then performs the following operations:
* It copies $H^{lo}$ into column `a7` / `row - 1`
* It copies $H^{hi}$ into column `a7` / `row`
* It copies $\Sigma_1^{lo}$ into column `a4` / `row`
* It copies $\Sigma_1^{hi}$ into column `a5` / `row`
* It assigns $K^{lo}$ into column `a6` / `row - 1`
* It assigns $K^{hi}$ into column `a6` / `row`
* It copies $W^{lo}$ into column `a8` / `row - 1`
* It copies $W^{hi}$ into column `a8` / `row`
* It copies $Ch^{hi}$ into column `a6` / `row + 1`
* It copies $Ch_{neg}^{lo}$ into column `a5` / `row - 1`
* It copies $Ch_{neg}^{hi}$ into column `a5` / `row + 1`
* It computes `h_prime_low`, `h_prime_high`, and `h_prime_carry`
* It assigns $H'_{carry}$ into column `a9` / `row + 1`
* It assigns $H'^{lo}$ into column `a7` / `row + 1`
* It assigns $H'^{hi}$ into column `a8` / `row + 1`
Finally, it returns (`h_prime_low`, `h_prime_high`). Additionally, the `s_h_prime` gate ([compression_gates.rs:339](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L339)) performs a check to verify that `h_prime_low`, `h_prime_high`, and `h_prime_carry` have been computed correctly. The following table demonstrates the cells assigned by `assign_h_prime`.
Note that in this region, we also apply `assign_ch` and enforce the constraints of the gate `s_ch.` Hence, all the cells colored green are the cells used by `s_ch` gate, whereas the cells colored red are used by `s_h_prime` gate. Finally, the white cells in columns `a0` and `a1` are assigned by the lookups in `assign_ch` along with the cell at the last row in column `a2` (is copied at row 2 / column `a3`) while the cells at the last row in columns `a5` and `a6` are assigned and used by $E_{new}$ (gray color).
#### $E_{new}$
To compute $E_{new}$ we need to do $H' + D$. The function `assign_e_new` ([compression_util.rs:906](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L906)) is responsible for performing that operation. It does the following:
* It copies $D^{lo}$ into column `a7` / `row`
* It copies $D^{hi}$ into column `a7` / `row + 1`
* It computes `e_new` (dense form) and `e_new_carry`
* It assigns $E_{new}^{lo}$ into column `a8` / `row`
* It assigns $E_{new}^{hi}$ into column `a8` / `row + 1`
* It assigns $E_{carry}$ into column `a9` / `row + 1`
Additionally, it applies the gate `s_e_new` ([compression_gates.rs:418](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L418)) which checks if `e_new` has been computed correctly.
Note that only the red cells are being used by the gate `s_e_new`. The gray cells have been assigned by other parts of the code and used by other gates.
#### $A_{new}$
To compute $A_{new}$ we need to do $H' + Maj(A,B,C) + \Sigma_0(A)$. The function `assign_a_new` ([compression_util.rs:938](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L938)) is responsible for performing that operation. It does the following:
* It copies $Maj^{hi}$ into column `a3` / `row - 1`
* It copies $\Sigma_0^{lo}$ into column `a6` / `row`
* It copies $\Sigma_0^{hi}$ into column `a7` / `row + 1`
* It copies $H'^{lo}$ into column `a7` / `row - 1`
* It copies $H'^{hi}$ into column `a8` / `row - 1`
* It computes `a_new` (dense form) and `a_new_carry`
* It assigns $A_{new}^{lo}$ into column `a8` / `row`
* It assigns $A_{new}^{hi}$ into column `a8` / `row + 1`
* It assigns $A_{carry}$ into column `a9` / `row`
Additionally, it applies the gate `s_a_new` ([compression_gates.rs:394](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L394)) that checks if `a_new` has been computed correctly.
Note that in this region, we also apply `assign_maj` and enforce the constraints of the gate `s_maj.` Hence, all the cells colored green are the cells used by `s_maj` gate, whereas the cells colored red are used by `s_a_new` gate. Finally, the white cells in columns `a0` and `a1` are assigned by the lookups in `assign_maj` along with the cell at the last row in column `a2` (copied at row 2 / column `a3`).
#### round_idx < 63 Case (Not the Last Round)
If we are not in the last round, we need to prepare the state for the next round. To do so, we copy `a_new_dense` and `e_new_dense` to the respective cell in the rows of the next round ([subregion_main.rs:78](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_main.rs#L78)). Furthermore, we also decompose in the rows of the new round by employing `decompose_a` and `decompose_e`. Finally, we create a new state and return it. The new state is composed of the following:
* A := a_new
* B := A
* C := B
* D := C
* E := e_new
* F := E
* G := F
* H := G
#### The Last Round
In the last round, we want to achieve the following state
* A := h0 + A
* B := h1 + B
* C := h2 + C
* D := h3 + D
* E := h4 + E
* F := h5 + F
* G := h6 + G
* H := h7 + h
Where `h{0..7}` are the initial values in the initial state at round 0. The implementation ([subregion_main.rs:111](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_main.rs#L111)) is responsible for that and will perform the following operations:
* It assigns $A_{new}^{lo}$ into column `a3` / `abcd_row`
* It assigns $A_{new}^{hi}$ into column `a4` / `abcd_row`
* It assigns $E_{new}^{lo}$ into column `a3` / `efgh_row`
* It assigns $E_{new}^{hi}$ into column `a4` / `efgh_row`
Then, for `A` to `H`, it will use the `assign_state_addition` function ([compression_util.rs:873](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_util.rs#L873)), that will take as input two terms and a row. For example, for `A`, `term1` is `h0` (`prev_a.dense_halves` -- the dense halves of the initial `A` in round 0) and `term2` is $A_{new}$ (dense halves). For `B`, `term1` is `h1` (`prev_b.dense_halves`) and `term2` is `A` (`a.dense_halves`). The function performs the following operations:
* It assigns $term_1^{lo}$ into column `a3` / `row`
* It assigns $term_1^{hi}$ into column `a4` / `row`
* It assigns $term_2^{lo}$ into column `a5` / `row`
* It assigns $term_2^{hi}$ into column `a6` / `row`
It then computes the sum of the two terms into `st_new` and `st_carry` and does the following:
* It assigns $st_{new}^{lo}$ into column `a7` / `row`
* It assigns $st_{new}^{hi}$ into column `a8` / `row`
* It assigns $st_{carry}$ into column `9` / `row`
Additionally, it enables the gate `s_add_havles` ([compression_gates.rs:372](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L372)), which checks if the addition was performed correctly. Lastly, the final state is added to a new state and returned to the compress function. The table below depicts the cells assigned by `assign_state_addition` and used by `s_add_halves` gate.
### Digest
The last step of Sha256 is the digest step, which takes the state after the final round and converts it to the final digest. The main function that performs the digest is the `assign_digest` function ([subregion_digest.rs:16](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/subregion_digest.rs#L16)) which takes as input some final state. This function performs the following operations:
* It copies $A^{lo}$ into column `a3` / `abcd_row`
* It copies $A^{hi}$ into column `a4` / `abcd_row`
* It computes $A$ (field element) and assigns it into column `a5` / `abcd_row`
* It copies $B^{lo}$ into column `a6` / `abcd_row`
* It copies $B^{hi}$ into column `a7` / `abcd_row`
* It computes $B$ (field element) and assigns it into column `a8` / `abcd_row`
It does the same for $C$ and $D$ but in row `abcd_row + 1`, and it performs the equivalent operations for $E,F,G,H$ but in rows `efgh_row` and `efgh_row + 1`.
Moreover, it applies the `s_digest` gate ([compression_gates.rs:440](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/hash/sha256/table16/compression/compression_gates.rs#L440)) in both `abcd_row` and `efgh_row`. This gate checks that the word computation was performed correctly. Finally, it returns the final words. The table below depicts the rows used for `s_digest`.
#### Issues in the Spec
Here, we report inconsistencies between the code and the [specification](https://zcash.github.io/halo2/design/gadgets/sha256/table16.html) or issues found in the specification. Note that this is not an exhaustive list, as most tables in the specification contain issues.
- In the initial and steady table in row 0, $F_0d(7)$ should be $E_0d(7)$.
In the Message scheduling region part, in the table, in row 8, columns a3-a6, there are some values that are not described in the implementation or the spec.
- `s_e_new` is off by one row.
- Final digest table D values are switched by C values
## Map
The `MapGadget` (`src/map/map_gadget.rs`) is an implementation of a key-value store using Merkle trees. In the Midnight protocol, this gadget serves the following functions:
- Implementing efficient key-value storage with ZK proofs.
- Proving membership in sets (see `examples/membership.rs`).
The key advantage of this implementation lies in its succinct representation through Merkle trees. Instead of proving statements about the entire map, proofs require only logarithmic-sized paths through the tree, making it both space- and computation-efficient for ZK circuits. At a high level, keys are represented as the path from the root to a leaf where the respective value is stored. The height of the tree is predefined as 128, which is a critical security parameter, as we will see.
**Key Representation and Tree Traversal.**
Given a field element $k$, its index is computed by hashing $k$, transforming it into bytes, and extracting the first 128 bits. This produces a bit string such as `1000101...`, which is used to traverse the tree: move left for `0` and right for `1`, starting from the root node. The state maintained for the `Map` is as follows:
```rust
struct State {
succinct_repr: AssignedNative, // The Merkle root representing the map
map: Box> // The underlying map structure
}
```
The `succinct_repr` corresponds to the Merkle root, providing a compact representation of the map. For example, consider a tree with height 2. Initially, all leaves are set to 0. Setting the key `0` to the value `1` would involve the following:
```
Map[0] = 1
hash(0) = 0x1234...
bits(0x1234...) = 0b10010001...
path[0] = [leaf_1_1, node_0, root]
```
This maps to a Merkle tree as shown below:
```
root Hash(node_0, node_1)
/ \
/ \
node_0 node_1 Hash(leaf_1_0, leaf_1_1)
/ \ / \
/ \ / \
leaf_0_0 leaf_0_1 leaf_1_0 leaf_1_1
0 0 0 0
```
Here, `path[0]` contains the values needed to recompute the root, which must match the new `succinct_repr`. Verification logic is handled by the `verify_path` function:
```rust
fn verify_path(
&self,
layouter: &mut impl Layouter,
key: &AssignedNative,
value: &AssignedNative,
proof: &[AssignedNative; TREE_HEIGHT as usize]
) -> Result<(), Error>
{
// Compute path from key
let zero = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
let path = self.hash_chip.hash(layouter, &[key.clone(), zero])?;
let path_as_bits = self.native_gadget
.assigned_to_le_bits(layouter, &path, None, true)?;
// Reconstruct root from path
let mut node: AssignedNative = value.clone();
for (is_right, sibling) in path_as_bits[..TREE_HEIGHT as usize]
.iter()
.zip(proof.iter())
{
// Determine left/right positioning
let (left_sibling, right_sibling) = self
.native_gadget
.cond_swap(layouter, is_right, &node, sibling)?;
// Hash to get parent
node = self.hash_chip
.hash(layouter, &[left_sibling, right_sibling])?;
}
// Verify computed root matches stored root
self.native_gadget
.assert_equal(layouter, &node, &self.state().succinct_repr)?;
Ok(())
}
```
**Insert and Get Operations.**
If the `verify_path` operation passes, insertion and retrieval operations can be performed. For insertion:
1. Retrieve the path for the current value of the `key` and prove its correctness.
2. Update the state (in-circuit) to reflect the new root.
3. Prove the correctness of the new root using `verify_path`.
**Security Considerations.**
For a naive example with height 2, collisions are trivial to find. With a height of 128, as chosen in Midnight, the collision probability for any two keys is approximately $2^{-64}$. While this is sufficient for most use cases, it might not be adequate for applications requiring higher collision resistance.
## ECC Native
The `ecc/native` implements twisted Edwards curve over native field in the format of $-x^2 + y^2 = 1 + d \cdot x^2 \cdot y^2$ (i.e. with $a = -1$). On a twisted Edwards curve, the identity point has affine coordinates and the addition is complete. In `EccChip` the point is defined as `x` and `y` coordinates in native field.
```rust
/// A twisted Edwards curve point represented in affine (x, y) coordinates, the
/// identity represented as (0, 1).
#[derive(Clone, Debug)]
pub struct AssignedNativePoint {
x: AssignedNative,
y: AssignedNative,
}
```
The scalar field element is represented as a vector of assigned bits (of native field) in little endian:
```rust
/// Scalars are represented as a vector of assigned bits in little endian.
#[derive(Clone, Debug)]
pub struct ScalarVar(Vec>);
```
The chip uses `membership_gate` to enforce a point is on-curve. That's basically checking the equation of the curve.
```
Enforce P = (x, y) is on the curve, using columns:
---------------
| x | y |
---------------
We enforce:
-x^2 + y^2 = 1 + d * x^2 * y^2
```
The `assign` function assigns a point from an off-circuit value. It first assigns a point and ensures it is on-curve via the `membership_gate`. Then multiply the point with cofactor to get the result. This ensures that the result point always lies in the correct subgroup although the result might not be identical to the input.
The chip uses two gates to perform point addition and multiplication. The `double_gate` gate enforces that `Q(xq, yq) = [2]P(xp, yp)`:
```
Enforce Q = 2 * P, using columns:
-----------------------------
| xp | yp | xq | yq |
-----------------------------
```
The `cond_add_gate` enforces that `R(xr, yr) = Q(xq, yq) + b * S(xs, ys)` where `b` is `0` or `1`:
```
Enforce R = Q + b * S, using columns:
-------------------------------------------------
| | | xq | yq | xs | ys | b |
| xr | yr | | | | | |
-------------------------------------------------
```
Note that the arrangement of these two gates enables us to do one round "double-and-add" in one row: the output `Q` of the first gate can be the input of the second gate and then the output of the second gate can be the input of the first gate. This creates an efficient `mul` operation, which is basically multiple rounds of "double-and-add" operation.
## Hash-to-Curve
Hash-to-curve gadget (`src/ecc/hash_to_curve/htc_gadget.rs`) implements a standardized way to map arbitrary field elements into valid elliptic curve points.
Specifically, the implementation follows RFC 9380 specification (https://datatracker.ietf.org/doc/rfc9380/) of hash-to-curve for the JubJub curve using the Poseidon hash function.
The gadget implements `hash_to_curve` as follows:
```rust
// Section 3 from https://datatracker.ietf.org/doc/rfc9380/
fn hash_to_curve(&self, layouter: &mut impl Layouter, input: &I) -> Result {
let mut state = self.sponge_chip.init(layouter)?;
self.sponge_chip
.absorb(layouter, &mut state, &[input.clone()])?;
let x1 = self.sponge_chip.squeeze(layouter, &mut state)?;
let x2 = self.sponge_chip.squeeze(layouter, &mut state)?;
let p1 = self.ecc_chip.map_to_curve(layouter, &x1)?;
let p2 = self.ecc_chip.map_to_curve(layouter, &x2)?;
self.ecc_chip.add(layouter, &p1, &p2)
}
```
where the sponge chip is a Poseidon sponge, and the `map_to_curve` is the following:
```rust
// We skip many of the params from the following snippet (e.g., layouter)
// Section 6.8 from https://datatracker.ietf.org/doc/rfc9380/
fn map_to_curve(
&self,
layouter: &mut impl Layouter,
u: &Self::Coordinate,
) -> Result, Error> {
// F.1. Shallue-van de Woestijne Method
// (https://datatracker.ietf.org/doc/rfc9380/)
let (weierstrass_x, weierstrass_y) = svdw_map_to_weierstrass(u)?;
// D.2. Mapping from Weierstrass to Montgomery
// (https://datatracker.ietf.org/doc/rfc9380/)
let (montgomery_x, montgomery_y) = weierstrass_to_montgomery(
&weierstrass_x,
&weierstrass_y,
)?;
// D.3. Mapping from Montgomery to Edwards
// (https://datatracker.ietf.org/doc/rfc9380/)
let (edwards_x, edwards_y) = montgomery_to_edwards(
&montgomery_x,
&montgomery_y,
)?;
let point = self.point_from_coordinates(&edwards_x, &edwards_y)?;
if C::COFACTOR == 1u128 {
Ok(point)
} else {
// Map into subgroup
let cofactor = self.assign_fixed(C::Scalar::from_u128(C::COFACTOR))?;
self.mul(layouter, &cofactor, &point)
}
}
```
## ECC in Foreign Field
The `ecc/foreign` implements the Weierstrass elliptic curve ($y^2 = x^3 + b$ with $a=0$) on an emulated (foreign) field. While it's doable to implement all of that by only using the public interface of the emulated field, Midnight uses lower-level primitives in some gates for performance reasons.
The point is represented by `is_id`, `x` and `y`. `x` and `y` are the coordinates on the emulated field. `is_id` is one bit element in native field that represents if the point is identity. If `is_id` is `1`, the point represents the identity, and the `x` and `y` coordinates can be arbitrary values. However, an honest prover should set them as `0` by default otherwise some calculation may fail.
```rust
/// Type for foreign EC points.
/// The identity is represented with field `is_id`, whose value is `1` iff the
/// point is the identity. If `is_id` is set, the values of `x` and `y` are
/// irrelevant and can be anything.
#[derive(Clone, Debug)]
#[must_use]
pub struct AssignedForeignPoint
where
F: PrimeField,
C: WeierstrassCurve,
B: FieldEmulationParams,
{
point: Value, // off-circuit value
is_id: AssignedBit,
x: AssignedField,
y: AssignedField,
}
```
### ECC Foreign Gates
Here we introduce the four gates used in ECC foreign.
We are working over an elliptic curve with equation:
$$
y^2 = x^3 + b
$$
Recall that if we have two points $P$ and $Q$ over some elliptic curve, we can compute $R = P + Q$ in the following way: first compute the "slope" of the line between $P$ and $Q$
$$
\lambda = \frac{Q_{y} - P_{{y}}}{Q_{x} - P_{x}}
$$
then the coordinates of $R$ are as follows:
$$
R_{x} = \lambda^2 - P_{x} - P_{y}
$$
$$
R_{y} = \lambda \cdot (P_{x} - R_{x}) - P_{y}
$$
If we want to compute a point doubling $2P$ then we need to take $\lambda$ as the slope of the tangent, and compute the coordinates as above
$$
\lambda_{\text{tangent}} = \frac{3P_{x}}{2P_{y}}
$$
In the implementation, there are three gates that check those equations:
- the `slope` gate asserts that some $\lambda$ value is indeed the slope between two points,
- the `lambda_squared` gate check the relation between $\lambda$ and the x coordinates of the three points,
- the `tangent` gate asserts that the slope $\lambda_{\text{tangent}}$ in the case of a tangent line is computed correctly.
Finally, the last gate `on_curve` given some coordinates $(x, y)$ asserts that those represent a valid curve point, i.e. they satisfy the curve equation.
#### The Slope Gate
The purpose of the gate is asserting that some witnessed $\lambda$ is correctly computed as the slope between two points. Given two points $(P_x, P_y)$ and $(Q_x, Q_y)$, and a scalar $\lambda$, we want to enforce
$$
\text{sign} \cdot Q_{y} - P_{y} = \lambda \cdot (Q_{x} - P_{x}) \mod{q}
$$
where $\text{sign}$ is either $1$ or $-1$. The elements are given in the base field of the elliptic curve, thus are represented with limbs using the foreign field representation and gates. The implementation of the check uses very similar techniques of the foreign field multiplication. It is sufficient to check that the relation
$$
\text{sign} \cdot Q_{y} - P_{y} - \lambda \cdot (Q_{x} - P_{x}) = k \cdot q
$$
holds over the integers for some value of $k$, where $q$ is the base field of the curve. As for the multiplication gate, this is checked to be the case using the CRT method, asserting this equation to be holding modulo the native prime $p$ and some additional moduli $m_i$. Indeed the custom gate asserts the following
$$
\text{sign} \cdot (1 + S(Q_{y})) - (1 + S(P_{y})) - (1 + S(\lambda)) \cdot \left[ (1 + S(Q_{x})) - (1 + S(P_{x})) \right] = k \cdot m
$$
where $S(x) = \sum_{i} B^i x_{i}$ is the value for the linear combination of the limbs. The actual equation checked by the gate is an equivalent simplified version of the equation above.
#### The Lambda Squared Gate
As before, we want to enforce an equation modulo $q$ the base field of the curve, namely we want to enforce
$$
P_{x} + Q_{x} + R_{x} = \lambda^2 \mod{q}
$$
Recall that $\lambda$ is represented as $1 + \sum_{i}B^i \lambda_{i}$, so computing $\lambda^2$ requires to manipulate the limbs in the following manner:
$$
\begin{align*}
\lambda^2 &= \left( 1 + \sum_{i}B^i \lambda_{i} \right) \cdot \left( 1 + \sum_{i}B^i \lambda_{i} \right) \\
&= 1 + 2 \cdot \sum_{i}B^i \lambda_{i} + \sum_{i} \sum_{j} B^{i+j} \lambda_{i} \lambda_{j} \\
\end{align*}
$$
As before, we use the CRT method, so we enforce:
$$
(1 + S(P_{x})) + (1 + S(Q_{x})) + (1 + S(R_{x})) - \lambda^2 = k \cdot q
$$
over the integers for some $k$, where $\lambda^2$ is computed with the expression above.
#### The Tangent Gate
This gate is pretty similar to the ones above, given a point $(x, y)$ we want to enforce the equation
$$
3 \cdot x ^ 2 = 2 \cdot y \cdot \lambda \mod{q}
$$
We can compute $x^2$ using the limb representation
$$
\begin{align*}
x^2 &= \left( 1 + \sum_{i}B^i x_{i} \right) \cdot \left( 1 + \sum_{i}B^i x_{i} \right) \\
&= 1 + 2 \cdot \sum_{i}B^i x_{i} + \sum_{i} \sum_{j} B^{i+j} x_{i} x_{j} \\
\end{align*}
$$
So the constraint to enforce becomes
$$
\begin{align*}
3 \cdot \left(2 \cdot \sum_{i}B^i x_{i} + \sum_{i} \sum_{j} B^{i+j} x_{i} x_{j}\right) \\-2 \cdot \left(
\sum_{i}B^i y_{i} + \sum_{i}B^i \lambda_{i} + \sum_{i} \sum_{j} B^{i+j} \lambda_{i} x_{j}
\right) &= k \cdot q
\end{align*}
$$
for some integer $k$. Again, we can enforce that this holds over the integer using the CRT method.
#### The On-Curve Gate
The purpose of this gate is to enforce that some point $(x, y)$ satisfies the elliptic curve equation, which means that the following relation must hold
$$
y^2 - x^3+ b = 0 \mod{q}
$$
Suppose the prover witnesses some $z = x^2 \mod{q}$ and this relation is separately checked elsewhere in the circuit, the relation to check becomes
$$
y^2 - x \cdot z + b = 0 \mod{q}
$$
Using a similar approach as before, we can write $y^2$ as follows
$$
\begin{align*}
y^2 &= \left( 1 + \sum_{i}B^i y_{i} \right) \cdot \left( 1 + \sum_{i}B^i y_{i} \right) \\
&= 1 + 2 \cdot \sum_{i}B^i y_{i} + \sum_{i} \sum_{j} B^{i+j} y_{i} y_{j} \\
\end{align*}
$$
Similarly, we can express the product $x \cdot z$ as follows
$$
\begin{align*}
x \cdot z &= \left( 1 + \sum_{i}B^i x_{i} \right) \cdot \left( 1 + \sum_{i}B^i z_{i} \right) \\
&= 1 + \sum_{i}B^i x_{i} + \cdot \sum_{i}B^i z_{i} + \sum_{i} \sum_{j} B^{i+j} x_{i} z_{j} \\
\end{align*}
$$
After some simple algebraic manipulations, the equation to check becomes
$$
\begin{align*}
2 \cdot \sum_{i}B^i y_{i} + \sum_{i} \sum_{j} B^{i+j} y_{i} y_{j} \\ - \left(
\sum_{i} \sum_{j} B^{i+j} x_{i} z_{j} + \sum_{i}B^i x_{i} + \cdot \sum_{i}B^i z_{i} + b
\right) &= k \cdot q
\end{align*}
$$
for some integer $k$, which is checked to hold over the integers using the CRT method.
### ECC Foreign Operations
Most of the basic operation is implemented in an advice-and-verify way using the gates described before.
#### Assign
The `assign` function assigns a new point from an off-circuit point. It first assigns the `x` and `y` as the foreign field element and ensures they are normalized. Then it checks that the point is on curve using the on-curve gate if it is not identity.
```rust
fn assign(
&self,
layouter: &mut impl Layouter,
value: Value,
) -> Result, Error> {
let p = self.assign_point_unchecked(layouter, value)?;
let is_not_id = self.native_gadget.not(layouter, &p.is_id)?;
on_curve::assert_is_on_curve::(
layouter,
&is_not_id,
&p.x,
&p.y,
self.base_field_chip(),
&self.config.on_curve_config,
)?;
Ok(p)
}
```
#### Add
The `assert_add` function checks that the provided point `P`, `Q` and `R` satisfies`P + Q = R`:
1. Given the slope `λ`, assert `λ` is the correct slope between `P` and `Q` using the slope gate.
2. Assert `R.x` is correct according to the slope using the lambda squared gate.
3. Assert `R.y` is correct by checking the slope between `P` and `R` using the slope gate.
The `add` function implements a complete addition for any two points in the group (including identity point). It's basically providing the sum and checking it's correct under different circumstances:
1. If `P` is identity then the sum is `Q`. If `Q` is identity then the sum is `P`.
2. Otherwise if `P = -Q` then the sum is identity element.
3. Otherwise if `P = Q` then the sum is `[2]P`.
4. Otherwise assert that the sum is correct using the `assert_add` function.
#### Double
The `assert_double` function checks that the provided point `P` and `R` satisfies`[2]P = R`:
1. Given the slope `λ`, assert that `λ` is the correct slope of the tangent at `P` using the tangent gate.
2. Assert `R.x` is correct using the lambda squared gate.
3. Assert `R.y` is correct by checking the slope between `P` and `R` using the slope gate.
The complete `double` function then is straightforward:
1. If `P` is identity then the result is identity.
2. Otherwise assert that the result is correct using the `assert_double` function.
#### Dynamic Lookup
In order to speed up certain computation (like `msm`), a dynamic lookup table is built to support querying points from a table. Below is structure of the table:
```rust
// |q_selector| x | y |index|table_tag|
// | 0 | p1.x limbs | p1.y limbs | 0 | tag |
// | 0 | p2.x limbs | p2.y limbs | 1 | tag |
// | 0 | ... | ... | ... | tag |
// | 0 | pn.x limbs | pn.y limbs | n-1 | tag |
```
The `x` and `y` columns are for the point coordinates. The `table_tag` column is to enforce that different tables are independent. The `index` column is for the index of the point in the table. The `q_selector` column with `1` means that we should lookup for the current row. `q_selector` column with `0` means that the current row is an item of the table.
#### GLV Split
GLV is used to speed up multiplication operation in foreign ECC. In order to compute $[k]P$, it splits $k$ such that $k = k_1 + k_2 \cdot \zeta$, where $\zeta$ is a cube root of unity in the foreign field. Then we have $[k]P = [k_1]P + [k_2\zeta]P$ and $[k_2\zeta]P(x,y) = [k_2]P(\zeta x,y)$.
Given scalar $k$ and point $P$, the `glv_split` function returns $k_1, k_2, P, Q$ such that $k = k_1 + k_2 \cdot \zeta$ and $Q.x = \zeta \cdot P.x$ and $Q.y = P.y$. Then $[k]P$ can be computed as $[k]P=[k_1]P + [k_2]Q$. Note multiple $k_1$ and $k_2$ values may satisfy the equation and the prover can select any of them.
#### MSM
Given the scalars $s_i$ and base points $P_i$, the `msm` function computes batch multiplication $\sum_i[s_i]P_i$ in an efficient way. It uses various ways to speed up the computation:
1. If a scalar $s_i$ is too large, then use the `glv_split` function to split it into two smaller scalars.
2. Split scalar into chunks of 4-bit window size. Then the range of each chunk of the scalar is $[0, 2^{4} - 1)$. Then the program precomputes the multiplication result of $[0]P, [1]P, [2]P, ..., [2^{4} - 1]P$ and sets that into the lookup table. The program only needs to lookup the result in the table when it wants to calculate the multiplication of a chunk.
3. Batch the square-and-add process for different base points.
4. Use the incomplete function `incomplete_add` to perform the addition. However, the function requires that it won't produce an identity element. To avoid this, the function introduces a randomizer point $R$, adds it in the computation and cancels at the last step. It's possible that for some $R$ it will still produce an identity element and the computation will fail. However the probability is very small and if it happens the prover can always change another random point.
## Findings
### Ambiguous Zero
- **Severity**: High
- **Location**: foreign field
**Location**: `src/field/foreign/field_chip.rs`
**Description**.
The Midnight foreign field circuits make extensive use of the "unique zero trick" to allow efficient comparison with zero.
This is achieved by ensuring that the representative of any field element lies in the range $[0, 2q)$ and encoding the zero element as $-1$:
which has exactly one representation in the range $[0, 2q)$.
To ensure that the representative lie in this interval, we must ensure that the element is "normalized" prior to the identity comparison with the unique zero.
This is achieved by calling the `normalize` method which conditionally applies the canonicalization procedure:
```rust
impl FieldChip
where
F: PrimeField,
K: PrimeField,
P: FieldEmulationParams,
N: NativeInstructions,
{
/// Normalizes the given assigned field element, but only if its bounds
/// exceed the limits of the well-formed bounds.
pub(crate) fn normalize(
&self,
layouter: &mut impl Layouter,
x: &AssignedField,
) -> Result, Error> {
if x.is_well_formed() {
Ok(x.clone())
} else {
self.make_canonical(layouter, x)
}
}
...
```
Where the definition of `is_well_formed` is as follows:
```rust
/// Tells whether the given emulated field element is well-formed, i.e., the
/// limb_bounds match the range [0, base).
/// AssignedField whose range is more restricted but included in [0, base)
/// are also considered well-formed.
pub fn is_well_formed(&self) -> bool {
self.limb_bounds.iter().fold(true, |acc, (lower, upper)| {
debug_assert!(lower <= upper);
acc && !BI::is_negative(lower) && upper.bits() <= P::LOG2_BASE as u64
})
}
```
In other words: a reduction is enforced when any of the limbs exceed $2^{\mathsf{LOG2\_BASE}}$.
However, this enforces a bound $[0, 2^{\mathsf{LOG2\_BASE} \cdot \mathsf{LIMBS}})$ on the representative,
which for a number of parameters exceeds the range $[0, 2q)$, for instance:
```rust
/// Secp256k1's Scalar field over Pallas's Scalar field.
impl FieldEmulationParams for MultiEmulationParams {
const LOG2_BASE: u32 = 86;
const NB_LIMBS: u32 = 3;
fn moduli() -> Vec {
vec![
BigInt::from(2).pow(82),
BigInt::from(2).pow(82) - BigInt::from(52),
]
}
const RC_LIMB_SIZE: u32 = 15;
}
```
In this case, the representative is bounded by $[0, 2^{86 \cdot 3}) = [0, 2^{258})$
which is roughly four times the size of the prime `secp256k1::Fq`.
For instance, the following code creates an encoding of `3 * q` which is congruent to zero modulo `q`,
yet passes the `assert_non_zero` check:
```rust
// limbs of 3 * P = 0 mod p
let limbs = [
BigUint::from_str_radix("3ffffffffffffcfffff48c", 16).unwrap(),
BigUint::from_str_radix("3fffffffffffffffffffff", 16).unwrap(),
BigUint::from_str_radix("2fffffffffffffffffffff", 16).unwrap(),
];
fn add_limbs(
layouter: &mut impl Layouter,
gadget_field: &FieldChip<
pasta_curves::Fq,
Fp,
MultiEmulationParams,
NativeGadget<
pasta_curves::Fq,
P2RDecompositionChip,
NativeChip,
>,
>,
x: &AssignedField,
y: &AssignedField,
neg1: &AssignedField, // (-2, -2) bounds
) -> Result, Error> {
let v = gadget_field.add(layouter, x, y)?;
let res = gadget_field.add(layouter, &v, neg1)?;
Ok(res)
}
fn form_limb(
layouter: &mut impl Layouter,
gadget_field: &FieldChip<
pasta_curves::Fq,
Fp,
MultiEmulationParams,
NativeGadget<
pasta_curves::Fq,
P2RDecompositionChip,
NativeChip,
>,
>,
one: &AssignedField,
value: &BigUint,
neg1: &AssignedField, // (-2, -2) bounds
) -> Result, Error> {
let mut val: AssignedField =
gadget_field.assign_fixed(layouter, Fp::from_u128(1u128))?;
let bits = value.to_radix_be(2);
for bit in bits {
val = add_limbs(layouter, gadget_field, &val, &val, neg1)?;
if bit == 1 {
val = add_limbs(layouter, gadget_field, &val, &one, neg1)?;
}
}
assert!(val.is_well_formed());
Ok(val)
}
let enc1: AssignedField =
gadget_field.assign_fixed(&mut layouter, Fp::from(1u64))?;
let neg1: AssignedField =
gadget_field.neg(&mut layouter, &enc1)?;
let limb_bound = Fp::from_u128(1u128 << 86);
let one0: AssignedField =
gadget_field.assign_fixed(&mut layouter, Fp::from(2u64))?;
let limb0 = form_limb(&mut layouter, &gadget_field, &one0, &limbs[0], &neg1)?;
let one1: AssignedField =
gadget_field.assign_fixed(&mut layouter, limb_bound + Fp::one())?;
let limb1 = form_limb(&mut layouter, &gadget_field, &one1, &limbs[1], &neg1)?;
let one2: AssignedField =
gadget_field.assign_fixed(&mut layouter, limb_bound * limb_bound + Fp::one())?;
let limb2 = form_limb(&mut layouter, &gadget_field, &one2, &limbs[2], &neg1)?;
let zero = add_limbs(&mut layouter, &gadget_field, &limb0, &limb1, &neg1)?;
let zero = add_limbs(&mut layouter, &gadget_field, &zero, &limb2, &neg1)?;
assert!(zero.is_well_formed());
gadget_field.assert_non_zero(&mut layouter, &zero)?;
```
**Impact**.
The check against zero is used extensively and the soundness of the circuits depends on the uniqueness of the zero element.
For instance $z = x / y$ is enforced by checking:
$$
z \cdot y = x \land y \neq 0
$$
If the latter condition is not correctly enforced and $y$ can be a representative of zero, then $z$ is unconstrained.
**Recommendation**.
Use the bounds from `well_formedness_bounds::()` to check for "well-formedness",
these bounds are correct for the most-significant limb and ensures that the representative lies in the range $[0, 2q)$.
We note that the bounds enforced by `make_canonical` are correct for the most-significant limb.
**Client Response**. This issue has been acknowledged and successfully mitigated.
### Ambiguous Zero
- **Severity**: High
- **Location**: src/hash/
**Description**.
The Midnight foreign field circuits make extensive use of the "unique zero" technique to allow efficient comparison with zero.
This is achieved by ensuring that the representative of any field element lies in the range $[0, 2q)$ and encoding the zero element as $-1$:
which has exactly one representation in the range $[0, 2q)$.
To ensure that the representative lie in this interval, we must ensure that the element is "normalized" prior to the identity comparison with the unique zero.
This is achieved by calling the `normalize` method which conditionally applies the canonicalization procedure:
```rust
impl FieldChip
where
F: PrimeField,
K: PrimeField,
P: FieldEmulationParams,
N: NativeInstructions,
{
/// Normalizes the given assigned field element, but only if its bounds
/// exceed the limits of the well-formed bounds.
pub(crate) fn normalize(
&self,
layouter: &mut impl Layouter,
x: &AssignedField,
) -> Result, Error> {
if x.is_well_formed() {
Ok(x.clone())
} else {
self.make_canonical(layouter, x)
}
}
...
```
Where the definition of `is_well_formed` is as follows:
```rust
/// Tells whether the given emulated field element is well-formed, i.e., the
/// limb_bounds match the range [0, base).
/// AssignedField whose range is more restricted but included in [0, base)
/// are also considered well-formed.
pub fn is_well_formed(&self) -> bool {
self.limb_bounds.iter().fold(true, |acc, (lower, upper)| {
debug_assert!(lower <= upper);
acc && !BI::is_negative(lower) && upper.bits() <= P::LOG2_BASE as u64
})
}
```
In other words: a reduction is enforced when any of the limbs exceed $2^{\mathsf{LOG2\_BASE}}$.
However, this enforces a bound $[0, 2^{\mathsf{LOG2\_BASE} \cdot \mathsf{LIMBS}})$ on the representative,
which for a number of parameters exceeds the range $[0, 2q)$, for instance:
```rust
/// Secp256k1's Scalar field over Pallas's Scalar field.
impl FieldEmulationParams for MultiEmulationParams {
const LOG2_BASE: u32 = 86;
const NB_LIMBS: u32 = 3;
fn moduli() -> Vec {
vec![
BigInt::from(2).pow(82),
BigInt::from(2).pow(82) - BigInt::from(52),
]
}
const RC_LIMB_SIZE: u32 = 15;
}
```
In this case, the representative is bounded by $[0, 2^{86 \cdot 3}) = [0, 2^{258})$
which is roughly four times the size of the prime `secp256k1::Fq`.
For instance, the following code creates an encoding of `3 * q` which is congruent to zero modulo `q`,
yet passes the `assert_non_zero` check:
```rust
// limbs of 3 * P = 0 mod p
let limbs = [
BigUint::from_str_radix("3ffffffffffffcfffff48c", 16).unwrap(),
BigUint::from_str_radix("3fffffffffffffffffffff", 16).unwrap(),
BigUint::from_str_radix("2fffffffffffffffffffff", 16).unwrap(),
];
fn add_limbs(
layouter: &mut impl Layouter,
gadget_field: &FieldChip<
pasta_curves::Fq,
Fp,
MultiEmulationParams,
NativeGadget<
pasta_curves::Fq,
P2RDecompositionChip,
NativeChip,
>,
>,
x: &AssignedField,
y: &AssignedField,
neg1: &AssignedField, // (-2, -2) bounds
) -> Result, Error> {
let v = gadget_field.add(layouter, x, y)?;
let res = gadget_field.add(layouter, &v, neg1)?;
for ((xl, yl), vl) in x
.limb_values()
.into_iter()
.zip(y.limb_values())
.zip(res.limb_values())
{
assert_eq!(
*vl.value().assign().unwrap(),
xl.value().assign().unwrap() + yl.value().assign().unwrap()
);
}
Ok(res)
}
fn form_limb(
layouter: &mut impl Layouter,
gadget_field: &FieldChip<
pasta_curves::Fq,
Fp,
MultiEmulationParams,
NativeGadget<
pasta_curves::Fq,
P2RDecompositionChip,
NativeChip,
>,
>,
one: &AssignedField,
value: &BigUint,
neg1: &AssignedField, // (-2, -2) bounds
) -> Result, Error> {
let mut val: AssignedField =
gadget_field.assign_fixed(layouter, Fp::from_u128(1u128))?;
let bits = value.to_radix_be(2);
for bit in bits {
val = add_limbs(layouter, gadget_field, &val, &val, neg1)?;
if bit == 1 {
val = add_limbs(layouter, gadget_field, &val, &one, neg1)?;
}
}
assert!(val.is_well_formed());
Ok(val)
}
let enc1: AssignedField =
gadget_field.assign_fixed(&mut layouter, Fp::from(1u64))?;
let neg1: AssignedField =
gadget_field.neg(&mut layouter, &enc1)?;
let limb_bound = Fp::from_u128(1u128 << 86);
let one0: AssignedField =
gadget_field.assign_fixed(&mut layouter, Fp::from(2u64))?;
let limb0 = form_limb(&mut layouter, &gadget_field, &one0, &limbs[0], &neg1)?;
let one1: AssignedField =
gadget_field.assign_fixed(&mut layouter, limb_bound + Fp::one())?;
let limb1 = form_limb(&mut layouter, &gadget_field, &one1, &limbs[1], &neg1)?;
let one2: AssignedField =
gadget_field.assign_fixed(&mut layouter, limb_bound * limb_bound + Fp::one())?;
let limb2 = form_limb(&mut layouter, &gadget_field, &one2, &limbs[2], &neg1)?;
let zero = add_limbs(&mut layouter, &gadget_field, &limb0, &limb1, &neg1)?;
let zero = add_limbs(&mut layouter, &gadget_field, &zero, &limb2, &neg1)?;
assert!(zero.is_well_formed());
gadget_field.assert_non_zero(&mut layouter, &zero)?;
```
**Impact**.
The check against zero is used extensively and the soundness of the circuits depends on the uniqueness of the zero element.
For instance $z = x / y$ is enforced by checking:
$$
z \cdot y = x \land y \neq 0
$$
If the latter condition is not correctly enforced and $y$ can be a representative of zero, then $z$ is unconstrained.
**Recommendation**.
Use the bounds from `well_formedness_bounds::()` to check for "well-formedness",
these bounds are correct for the most-significant limb and ensures that the representative lies in the range $[0, 2q)$.
### The `incomplete_assert_different_x` Function Is Not Sound
- **Severity**: High
- **Location**: foreign ecc
**Location**: `src/ecc/foreign/ecc_chip.rs`
**Description**. In the `foreign/ecc` chip, it uses the `incomplete_assert_different_x` function to make sure that the x coordinates of two points are different. To make it efficient, the function only compares the most significant limb (MSB) of the coordinates at the cost of completeness. However, it turns out that this function is not sound and the same two coordinates may still pass the check.
```rust
fn incomplete_assert_different_x(
&self,
layouter: &mut impl Layouter,
p: &AssignedForeignPoint,
q: &AssignedForeignPoint,
) -> Result<(), Error> {
...
// get the most significant limb of p.x and q.x
let msl_px = px_limbs.last().unwrap();
let msl_qx = qx_limbs.last().unwrap();
// We assert that `(msl_px - msl_qx) not in {0, msl_modulus, -msl_modulus}`.
let diff = self.native_gadget.sub(layouter, msl_px, msl_qx)?;
self.native_gadget.assert_non_zero(layouter, &diff)?;
self.native_gadget
.assert_not_equal_to_fixed(layouter, &diff, msl_modulus)?;
self.native_gadget
.assert_not_equal_to_fixed(layouter, &diff, msl_modulus.neg())
}
```
The function above gets the `diff` of the MSB of the two points and then ensures that the `diff` is not in `{0, msl_modulus, -msl_modulus}`, where `msl_modulus` is the MSB of foreign field modulus. The intent is that if there is difference in one limb then the two (normalized) foreign field must be different. However, the issue rises when it compares `diff` with `msl_modulus`.
Suppose `q` is the foreign field. `a` is an element in field `q`. Suppose both `a` and `q + a` are valid normalized elements. Then the `diff` of the MSB of `a` and `q + a` is not necessarily equal to `msl_modulus` due to possible carry from the lower limbs. Here is a minimal example:
Let the foreign field `q` be `11`, `limb_size` be `2` and `number_of_limbs` be `2`. Then the limbs (little-endian) of `q` are `11 || 01`. So `msl_modulus=2`. Take the value as `3`. Then it has two normalized representatives: `3 = 11 || 00` and `14 = 01 || 11`. However we have `(00 - 11) = -3` and it's not a multiple of `msl_modulus`.
This means that the `incomplete_assert_different_x` function is not sound.
Besides, this function might cause completeness issues for some emulated field. This is because the range of the MSB might be small. For example, in extreme cases the valid range of MSB is just 1 bit. Then the `incomplete_assert_different_x` function will always fail.
**Impact**. The `windowed_msm` function uses the `incomplete_assert_different_x` function to avoid adding two points that have the same x coordinates and thus avoid getting an identity element. Due to this soundness issue, now a malicious prover is able to produce an identity element and then get an incorrect result in the `incomplete_add` function.
**Recommendation**. It's recommended to have a sound implementation for this function. For example, directly use the `assert_not_equal` API from the foreign field although it will be less efficient.
**Client Response**. This issue has been acknowledged and fixed. The `incomplete_assert_different_x` function has been reimplemented. The function now calculates the sum of the differences of all the limbs and ensures the result is not in `{0, m, -m}`, where `m` is the foreign field modulus. Note that the comparison is performed in the native field, making it incomplete but sound, which is the expected behavior.
### Missing Equality Constraint When Assigning Word Halves with `assign_word_halves_dense` in the Final Compression Round of SHA256
- **Severity**: High
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}/compression/subregion_main.rs`
**Description**.
When reaching the final round inside the `assign_round` function ([subregion_main.rs:111-120](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/subregion_main.rs#L111-L120)), it is required to assign the halves for the `a_new_val` and `e_new_val` to use them when computing the final state for $A$ and $E$. This happens with the following code:
```rust
let abcd_row = get_digest_abcd_row();
let efgh_row = get_digest_efgh_row();
let a_final =
self.assign_word_halves_dense(region, abcd_row, a_3, abcd_row, a_4, a_new_val)?;
let e_final =
self.assign_word_halves_dense(region, efgh_row, a_3, efgh_row, a_4, e_new_val)?;
```
The issue with that code is that does not apply equality constraints for `a_final` with `a_new_dense`, and `e_final` with `e_new_dense`.
Note that this issue also exists in Table 11 at [subregion_main.rs:125-134](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/subregion_main.rs#L125-L134).
**Impact**. Without proper equality constraints, a malicious prover may provide different values for the two words. This may cause the hash result to be incorrect.
**Recommendation**.
We recommend adding the constraints to check that the word halves are valid split of the word.
For example, you can use something like the following:
```rust
let a_final =
self.assign_word_halves_dense(region, abcd_row, a_3, abcd_row, a_4, a_new_val)?;
region.constrain_equal(a_final.0.cell(), a_new_dense.0.cell())?;
region.constrain_equal(a_final.1.cell(), a_new_dense.1.cell())?;
```
**Client Response**.
This issue has been acknowledged and fixed. This fix includes the missing equality constraints. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Missing Equality Constraints in SHA256 apply_padding Function
- **Severity**: High
- **Location**: sha256
**Location**: `src/hash/sha256/table16.rs and src/hash/sha256/table11.rs`
**Description**.
The `apply_padding` function have an issue with equality constraints for padded inputs. Here's a detailed breakdown of the observed behavior:
1. In the `compress` function ([table16.rs:239](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L239)), 16 `AssignedBlockWords` are passed as input.
2. The input is converted into `input_values` using `from_field_value`, resulting in 16 `BlockWords` (not `AssignedCells`).
3. These are passed to `message_schedule.process`, which outputs:
- `w`: 64 `MessageWords`.
- `w_halves`: 64 pairs of `(AssignedBits<16, F>, AssignedBits<16, F>)`, representing the split words (low and high).
4. Equality constraints are then applied ([table16.rs:262](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L262)) to enforce that the first 16 words in `w` are equal to the original input.
In `apply_padding` ([table16.rs:309](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L309)):
- The function handles two blocks (one optional), applying similar logic depending on the input. According to the SHA256 padding algorithm we might require an extra block if we can't finish the padding in the existing one.
- The rest of the logic of this function should be similar to the `compress` function. However, the equality constraints are applied only for the non-padded input ([table16.rs:369](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L369)). For example:
- If the input consists of 2 `BlockWords`, only `w[0]` and `w[1]` are checked against `input[0]` and `input[1]`.
- There seems to be no enforcement for `w[2..16]` to match the corresponding `input[2..16]`.
Without this, the prover could pass arbitrary values for `input[2..16]` in `message_schedule.process`.
The confusion might stem from the use of `assigned_fixed` for padding values ([mod.rs:561](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/mod.rs#L561)).
Nevertheless, at [table16.rs:360](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L360), values are extracted from assigned cells and passed as block words rather than assigned blocks.
**Impact**.
Without enforcing equality constraints for the padded words of the input, the prover can potentially supply arbitrary values for these words, leading to incorrect or insecure behavior in circuits relying on this logic.
**Recommendation**.
We recommend to extend the equality constraints in `apply_padding` to cover all `w[0..16]`, including the padded words similar to the `compress` function.
**Client Response**.
This issue has been acknowledged and fixed. This fix extends the equality constraints in the first 16 words instead of skipping the padded ones. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Round Constants in SHA256 Are Not Constrained
- **Severity**: High
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}/compression/compression_utils.rs`
**Description**.
During the compression phase of SHA256, we need to compute $H'$ in each round. The formula to compute $H'$ is $H + Ch(A,B,C) + \sum_1(E) + K_i + W_i$.
The $K_i$ value is coming from the round constants defined at [mod.rs:63](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/mod.rs#L63) in the implementation.
To compute and assign $H'$ the function `assign_h_prime` is called at [subregion_main.rs:57](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/subregion_main.rs#L57), where `ROUND_CONSTANTS[round_idx.as_usize()]` is passed as the parameter for $K_i$. The following code at [compression_util.rs:837-849](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/compression_util.rs#L837-L849) is responsible for assigning `k` into a cell.
```rust
let k: [bool; 32] = i2lebsp(k.into());
let k_lo: [bool; 16] = k[..16].try_into().unwrap();
let k_hi: [bool; 16] = k[16..].try_into().unwrap();
{
AssignedBits::<16, F>::assign_bits(
region,
|| "k_lo",
a_6,
row - 1,
Value::known(k_lo),
)?;
AssignedBits::<16, F>::assign_bits(region, || "k_hi", a_6, row, Value::known(k_hi))?;
}
```
The problem with this code is that `k` is assigned into advice columns without being constrained. Hence, a malicious prover can select whatever value he wants.
Note that the same issue exists in table 16 at [compression_util.rs:802-814](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L802-L814).
**Impact**. Without constraining `k`, a malicious prover may provide different values for the round constants. This may cause the hash result to be incorrect.
**Recommendation**.
We recommend using `assign_bits_fixed` instead of `assign_bits` to assign the round constants.
**Client Response**.
This issue has been acknowledged and fixed. This fix uses `assign_bits_fixed` instead of `assign_bits`. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Foreign Field Elements Equality Testing Is Incomplete
- **Severity**: Medium
- **Location**: foreign field
**Location**: `src/field/foreign/field_chip.rs`
**Description**.
The Midnight foreign field chip allows asserting that two elements are equal using the function `assert_equal`, and asserting that one element is equal to some constant using the function `assert_equal_to_fixed`.
Those functions are very similar, the implementation first normalizes the operand(s) and then asserts equality of the limbs pairwise.
However, some elements in the foreign field may have multiple valid representations.
In particular, assuming that $x$ has two representations, the numbers $x$ and $x + q$ having all the limbs in the correct ranges are both valid representations for the same element.
The normalization procedure is skipped if the elements are already well-formed, which may lead to some circuits being unsatisfiable.
In the example below, we compute the value $k_{\text{val}} = B^2 + 1$ where $B = 2^{86}$ is the base of the representation for the foreign field elements.
We compute $s = k_{\text{val}} + (-2)$ and then we assert that $s = k_{\text{val}} - 2$.
The computed value is constrained to land in one valid representation, in particular the one greater than $q$.
The comparison is however made with the same value in the other representation less than $q$, and the resulting circuit is thus unsatisfiable (even though the assertion is true).
```rust
// B is the base of the limb representation, in this case B = 2^86
// k_val = B^2 + 1, represented as limbs [0, 0, 1]
let k_val: Fp = bigint_to_fe(
&BigInt::from(2)
.pow(86 * 2)
.checked_add(&BigInt::from(1))
.unwrap(),
);
let k_val_assigned: AssignedField =
gadget_field.assign_fixed(&mut layouter, k_val)?;
let neg_two: AssignedField =
gadget_field.assign_fixed(&mut layouter, -Fp::from(2))?;
// compute k_val - 2, this will increase the most significant limb of neg_2 by 1
// but it is still in the range [0, B)
let s = gadget_field.add(&mut layouter, &neg_two, &k_val_assigned)?;
// the number is well-formed because every limb is in [0, B), so the normalization is skipped
// asserting that the value is equal to (k_val - 2) renders the circuit unsatisfiable
gadget_field.assert_equal_to_fixed(&mut layouter, &s, k_val - Fp::from(2))?;
```
**Impact**.
The equality assertion for foreign field elements is incomplete, and this could lead to correct circuits that are not provable for each possible input or even completely unsatisfiable circuits.
**Recommendation**.
In the equality assertion, check equality with both representations.
Otherwise, assert equality by computing a subtraction between the two values and asserting that the result is zero, since the zero value is guaranteed to have a unique representation.
**Client Response**. This issue has been acknowledged and fixed.
### Missing Range Check for `h_prime_carry`, `h_prime_lo`, `h_prime_hi` in SHA256
- **Severity**: Medium
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}/compression/compression_util.rs`
**Description**.
In each round of compression of SHA256 we need to compute `h_prime`. The `h_prime` value is computed in the `assign_h_prime` function. When it is computed the `h_prime_carry`, `h_prime_lo`, and `h_prime_hi` are assigned by the following code.
```rust
region.assign_advice(
|| "h_prime_carry",
a_9,
row + 1,
|| h_prime_carry.map(F::from),
)?;
let h_prime: Value<[bool; 32]> = h_prime.map(|w| i2lebsp(w.into()));
let h_prime_lo: Value<[bool; 16]> = h_prime.map(|w| w[..16].try_into().unwrap());
let h_prime_hi: Value<[bool; 16]> = h_prime.map(|w| w[16..].try_into().unwrap());
let h_prime_lo = AssignedBits::<16, F>::assign_bits(
region,
|| "h_prime_lo",
a_7,
row + 1,
h_prime_lo,
)?;
let h_prime_hi = AssignedBits::<16, F>::assign_bits(
region,
|| "h_prime_hi",
a_8,
row + 1,
h_prime_hi,
)?;
```
The gate of `h_prime` performs the following checks.
```rust
let lo = h_lo + ch_lo + ch_neg_lo + sigma_e_lo + k_lo + w_lo;
let hi = h_hi + ch_hi + ch_neg_hi + sigma_e_hi + k_hi + w_hi;
let sum = lo + hi * F::from(1 << 16);
let h_prime = h_prime_lo + h_prime_hi * F::from(1 << 16);
let check = sum - (h_prime_carry * F::from(1 << 32)) - h_prime;
Some(("s_h_prime", s_h_prime * check))
```
Yet, no range checks are applied in `h_prime_carry`, `h_prime_lo`, and `h_prime_hi`. Specifically `h_prime_carry` should be less than or equal to `4`, and `h_prime_lo`/`h_prime_hi` should be constrained to be 16-bit values.
Otherwise, in the equation below, you can have different combination of the values to get the same `h_prime` (mod native field).
```rust
let h_prime = h_prime_lo + h_prime_hi * F::from(1 << 16);
```
**Impact**. Without proper range checks a malicious prover may provide different values for `h_prime_carry`, `h_prime_lo`, and `h_prime_hi`. This may cause the hash result to be incorrect.
**Recommendation**.
We recommend adding the required range checks. Specifically, check `h_prime_carry` to be less than or equal to `4` and constrain `h_prime_lo` and `h_prime_hi` to be 16-bit values.
**Client Response**.
This issue has been acknowledged and fixed. This fix performs the missing range checks. For `h_prime_lo` and `h_prime_hi` the range16 gates are used. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Missing Range Check for `e` and `f` in SHA256
- **Severity**: Medium
- **Location**: sha256
**Location**: `src/hash/sha256/table11/*/subregion2.rs`
**Description**.
In the SHA256 implementation, it's often needed to decompose 32-bit word into pieces of shorter length. In the `decompose_word` function at [subregion2.rs:346-349](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/subregion2.rs#L346-L349) there appears to be no range check for `e` and `f` to ensure they are 1-bit numbers in the following code.
```rust
/// Pieces of length [3, 4, 3, 7, 1, 1, 13]
fn decompose_word(
&self,
region: &mut Region<'_, F>,
word: Value<&Bits<32>>,
index: usize,
postponed: &mut Vec>,
) -> Result, Error> {
let row = get_word_row(index);
let pieces = word.map(|word| {
vec![
word[0..3].to_vec(),
word[3..7].to_vec(),
word[7..10].to_vec(),
word[10..17].to_vec(),
vec![word[17]],
vec![word[18]],
word[19..32].to_vec(),
]
});
let pieces = pieces.transpose_vec(7);
...
// Assign `e` (1-bit piece)
let e = AssignedBits::<1, F>::assign_bits(region, || "e", a_3, row + 1, pieces[4].clone())?;
// Assign `f` (1-bit piece)
let f = AssignedBits::<1, F>::assign_bits(region, || "f", a_4, row + 1, pieces[5].clone())?;
...
}
```
Although the 1-bit cases for `e` and `f` do not require a spread check, it is essential to include a 1-bit range check for both to ensure no overflow occurs.
**Impact**. Without proper range check for `e` and `f`, a malicious prover may provide different values for the decomposition. This may cause the hash result to be incorrect.
**Recommendation**.
We recommend adding a 1-bit range check for both `e` and `f` to ensure they do not overflow.
**Client Response**.
This issue has been acknowledged and fixed. This fix includes the missing range checks by constraining `e` and `f` through `Gate::range_check(e/f, 0, 1)`. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Missing Equality Constraint When Assigning New Word with `assign_word_and_halves` in Message Schedule
- **Severity**: Medium
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}/message_schedule/subregion{2,3}.rs`
**Description**.
In the message schedule process in SHA256, we need to assign words $W_0$ ... $W_{63}$. The first 16 words are assigned at [message_schedule.rs:355](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule.rs#L355) as those were copied from the input. These words are constrained to the input at [table11.rs:334](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11.rs#L334). The next words, i.e., $W_{16}$ to $W_{63}$ need to be computed in subregions 2 and 3. When the new words are computed, they are assigned into $W_i$ and $carry_i$ in the `new_word_idx - 16 + 1` row and also computed their halves (i.e., low and high decomposition), and those halves are assigned in `new_word_idx`. Here is the relevant code:
```rust
region.assign_advice(
|| format!("W_{}", new_word_idx),
a_5,
get_word_row(new_word_idx - 16) + 1,
|| word.map(|word| F::from(word as u64)),
)?;
region.assign_advice(
|| format!("carry_{}", new_word_idx),
a_9,
get_word_row(new_word_idx - 16) + 1,
|| carry.map(F::from),
)?;
let (word, halves) = self.assign_word_and_halves(region, word, new_word_idx)?;
```
The issue with the above code is that the two cells have no equality constraint.
Note that this issue happens in the following parts of the code:
* Table 11 Subregion2: [subregion2.rs:268-281](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/subregion2.rs#L268-L281)
* Table 11 Subregion3: [subregion3.rs:178-190](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/subregion3.rs#L178-L190)
* Table 16 Subregion2: [subregion2.rs:262-274](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L262-L274)
* Table 16 Subregion3: [subregion3.rs:175-187](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion3.rs#L175-L187)
**Impact**. Without proper equality constraints, a malicious prover may provide different values for the two words. This may cause the hash result to be incorrect.
**Recommendation**.
We recommend adding the appropriate equality constraint between the two assigned cells of the same word.
**Client Response**.
This issue has been acknowledged and fixed. This fix includes the missing equality constraints for both subregions. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Missing Range Checks for e_new and a_new in SHA256
- **Severity**: Medium
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}.rs`
**Description**.
In each round of SHA256 we need to compute $A_{new}$ and $E_{new}$. The functions responsible for that in the implementation are `assign_a_new` ([compression_util.rs:938](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L938)) and `assign_e_new` ([compression_util.rs:906](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L906)). After computing the values, the code uses `assign_word_halves_dense` to assign the new word and its halves into advice columns. Further it assigns the carry using `assign_advice`. For example, here is the code from Table 16 for `e_new`.
```rust
let (e_new, e_new_carry) = sum_with_carry(vec![
(h_prime.0.value_u16(), h_prime.1.value_u16()),
(d.0.value_u16(), d.1.value_u16()),
]);
let e_new_dense = self.assign_word_halves_dense(region, row, a_8, row + 1, a_8, e_new)?;
region.assign_advice(|| "e_new_carry", a_9, row + 1, || e_new_carry.map(F::from))?;
```
The issue with the code above is that the `e_new_dense` halves are not range checked to be 16-bits values. Additionally, the `e_new_carry` is also not range checked. In the following is the gate `s_e_new`
```rust
let lo = h_prime_lo + d_lo;
let hi = h_prime_hi + d_hi;
let sum = lo + hi * F::from(1 << 16);
let e_new = e_new_lo + e_new_hi * F::from(1 << 16);
let check = sum - (e_new_carry * F::from(1 << 32)) - e_new;
```
The same issue exists for both Table 11 and Table 16 `a_new` and `e_new`. Below are references to the exact issues:
* Table 16 e_new: [compression_util.rs:931](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L931)
* Table 16 a_new: [compression_util.rs:980](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L980)
* Table 11 e_new: [compression_util.rs:966](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/compression_util.rs#L966)
* Table 11 a_new: [compression_util.rs:1015](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/compression_util.rs#L1015)
**Impact**. This could cause issues if a malicious prover can craft different values to satisfy the other constraints applied.
**Recommendation**.
We recommend adding a 16-bits range check for both `{a,e}_new_dense` and the respective carry.
**Client Response**.
This issue has been acknowledged and fixed. This fix performs the missing range checks. For `a_new_dense` and `e_new_dense` the range16 gates are used and the fix is applied. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Missing Check for Point `u` in `JubJub::from_xy`
- **Severity**: Low
- **Location**: ecc
**Location**: `src/ecc/curves.rs`
**Description**.
The `from_xy` function for the `JubJub` curve ([curves.rs:85](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/ecc/curves.rs#L85)) currently does not include a check for the validity of point `u`. This oversight could lead to accepting invalid points.
While this might not have a significant impact on the circuit implementation for the native curve, it is still a potential issue that could affect correctness in specific use cases.
**Impact**.
The absence of a check for `u` may allow invalid points to be used, potentially leading to incorrect or unexpected behavior. However, this does not seem to have a substantial impact on the circuit implementation for the native JubJub curve.
**Recommendation**.
We recommend adding a validation step in the `from_xy` function to ensure that the point `u` is valid. This would enhance the robustness and correctness of the implementation.
**Client Response**.
Acknowledged.
### No Domain Separator in Hash-to-Curve Implementation
- **Severity**: Low
- **Location**: hash-to-curve
**Location**: `src/ecc/hash_to_curve/htc_gadget.rs`
**Description**.
The current implementation of hash-to-curve in `htc_gadget.rs` ([htc_gadget.rs:86](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/ecc/hash_to_curve/htc_gadget.rs#L86)) does not allow users to explicitly provide a domain separator before the input. This limitation might prevent compliance with the domain separation requirement for hash-to-curve (RFC 9380, Section 3.1: Domain Separation Requirement).
For example, users cannot pass a domain separator along with their input using the `absorb` function as follows:
```rust
absorb(&[domain_separator, input.clone()])
```
Currently:
- The input is restricted to a single field element.
- However, the function documentation at [compact_std_lib.rs:349](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/compact_std_lib.rs#L349) mentions accepting a slice of field elements.
This inconsistency could confuse users and result in an inability to correctly implement domain separation for specific applications.
**Impact**.
The absence of proper support for a domain separator in the hash-to-curve logic might restrict flexibility for users needing to comply with the domain separation requirement. Additionally, the documentation inconsistency could lead to misunderstandings about the API's intended usage.
**Recommendation**.
1. Update the implementation to allow passing a slice of field elements as input, enabling users to include a domain separator explicitly.
2. Ensure the documentation is consistent across all relevant files (`htc_gadget.rs`, `compact_std_lib.rs`, `hash_to_curve.rs`) to reflect the updated behavior.
**Client Response**. This issue has been acknowledged and fixed. The `hash_to_curve` function ([htc_gadget.rs:89](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/ecc/hash_to_curve/htc_gadget.rs#L89)) now accepts a slice of field elements as input.
### Missing Parameter for Default Value in `Map::init` Function
- **Severity**: Low
- **Location**: map
**Location**: `src/map/map_gadget.rs`
**Description**.
The `init` function in the `Map` gadget ([map_gadget.rs:61](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/map/map_gadget.rs#L61)) does not accept a parameter for specifying a default value. Instead, it hardcodes the default value to `0`. This design restricts users from setting a custom default value for all keys in the map during initialization.
Note that the CPU version of the Map has a `default` parameter.
**Impact**.
This limitation forces all keys in the map to have a default value of `0`, preventing flexibility for users who may require a different default value.
**Recommendation**.
We recommend modifying the `init` function to accept an additional parameter for the default value. For instance:
This would allow users to specify their desired default value during initialization, improving the usability and flexibility of the `Map` gadget.
**Client Response**.
Acknowledged.
### Poseidon Parameters Generated by a Deprecated Script
- **Severity**: Low
- **Location**: poseidon
**Location**: `src/hash/poseidon/params/*`
**Description**.
The parameters (i.e., the round constants and the MDS matrix) for the three curves were generated using the [generate_parameters_grain.sage](https://github.com/daira/pasta-hadeshash/blob/master/code/generate_parameters_grain.sage) script from the [pasta-hadeshash](https://extgit.iaik.tugraz.at/krypto/hadeshash) repository. This repository is a fork of the [hadeshash repository](https://extgit.iaik.tugraz.at/krypto/hadeshash) that adds support for the Pasta curves. However, the fork relies on a deprecated version of the Hadeshash repository. It is recommended to migrate to the newer version, which includes several bug fixes and defenses against algebraic attacks, as described in this [paper](https://eprint.iacr.org/2023/537.pdf).
**Impact**.
The use of parameters generated by a deprecated script may expose the implementation to algebraic attacks.
**Recommendation**.
We recommend using the latest version of the script to regenerate the parameters, ensuring improved security and robustness.
**Client Response**.
Acknowledged.
### Spread Halves Are Not Range Checked in Decompose Functions in SHA256
- **Severity**: Low
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}/compression/`
**Description**.
In the implementation of SHA256, a lot of operations happen in the spread format of a variable to mainly efficiently perform the XOR operations required by SHA256. Furthermore, to correctly transform a number represented in bits, a spread lookup table is being used, as explained in the description of the SHA256 implementation in this report. The decompose functions are heavily used in the compression section for a few reasons. In this description, we are going to analyze the behavior of `decompose_e` ([compression_util.rs:403](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L403)) in Table 16, but a similar behavior exists in all decompose functions in Table 16 and Table 11. This function is responsible to:
1. Decompose $E$ word (32 bits) in low (16 bits) and high (16 bits) parts, computing the spread of $E$ by getting the spread of low (32 bits) and the spread of high (32 bits). These operations are happening by calling the `assign_word_halves` function ([compression_util.rs:1038](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L1038)).
2. The function is also responsible for splitting $E$ word into (a,b,c,d) pieces of (6,5,14,7) bit-chunks, respectively, by calling the `decompose_efgh` function ([compression_util.rs:289](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L289)). Note that `a` and `b` are further split into low and high parts. Further, it computes the spread of (a,b,c,d) -- e.g., `spread_a_lo` and `spread_a_hi` for `a_hi` and `a_lo`.
3. That function then makes sure that the new produced dense halves for $E$ are equal ([compression_util.rs:416-417](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L416-L417)) to the input of the function. Note that for $E$ (and $A$ in the respective code) this checks happens inside an if statement because for the rest of the rounds the check happens at [subregion_main.rs:78](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/subregion_main.rs#L78).
4. The `decompose_efgh` function ([compression_util.rs:289](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L289)) also range checks `c` and `d` pieces through the lookup. It also check that the spread values for `c` and `d` are the correct ones.
Next the assigned region from this function is used by the `s_decompose_efgh` gate ([compression_gates.rs:87](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_gates.rs#L87)). This gate performs the following checks.
1. Range checks `a_lo`, `a_hi`, `b_lo`, `b_hi` and checks that their spread values are correct (e.g., `spread_a_lo`).
2. Check that the tags for the lookups to `c` and `d` (to get their spreads) are in the correct range. This is important to actually range-check the dense form for `c` and `d` to be 14 and 7 bits.
3. Check that the (a,b,c,d) pieces indeed represent the $E$ word in its dense form (by summing up the dense halves of $E$).
4. Check that the spread pieces of (a,b,c,d) indeed represent the spread of $E$ word.
Something that is never explicitly checked is if the spread of $E$ word (i.e., `spread_word_lo` and `spread_word_hi`) are indeed the spread values of `word_lo` and `word_hi` (i.e. if the spread halves are the correct ones for the dense halves).
Nevertheless, this is implicitly enforced because we have the following:
1. The dense halves `word_lo` and `word_hi` are correctly constrained to the input (`assigned_e`).
2. The pieces (a,b,c,d) are equal to `word_lo` and `word_hi`.
3. The spread (`spread_a`,`spread_b`,`spread_c`,`spread_d`) is the correct spread of (a,b,c,d).
4. The `spread_word_lo` and `spread_word_hi` are equal to (`spread_a`,`spread_b`,`spread_c`,`spread_d`).
Hence, `spread_word_lo` and `spread_word_hi` should be the correct spread for `word_lo` and `word_hi`.
Yet, there is no range check for `spread_word_lo` and `spread_word_hi`. This means that someone could set `spread_word_hi` to zero and `spread_word_lo` to a 64-bit value and still pass all the checks. In summary, we have the freedom to put any values to `spread_word_hi` and `spread_word_lo` as long as they indeed represent the spread of word $E$.
We further, checked where the spread parts are used. This should be safe if they are always used to compute the complete spread value. If that is the case, then this is a benign, under-constrained issue.
Specifically, the `spread_word_lo` and `spread_word_hi` are used in the following:
* In the `s_upper_sigma_1` gate ([compression_gates.rs:201](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_gates.rs#L201)), only the pieces are used, so it should be safe.
* In the `s_ch` gate ([compression_gates.rs:244](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_gates.rs#L244)) `spread_e_lo`, `spread_e_hi`, `spread_f_lo` (`spread_e_lo` from the previous round), and `spread_f_hi` (`spread_e_hi` from the previous round) are used. Their sum is computed in the `lhs` variable. Thus, it is safe.
* Similarly, to the `s_ch` gate in the `s_ch_neg` we have a same behavior for spreads of $E$ and $G$ (it is the $E$ word from two rounds before). It is still safe because their sum is computed in the `lhs` variable.
A similar behavior exist in both Table 16, but also for the other words $A$, $B$, $C$, $F$, $G$.
**Impact**.
As explained in the description, this issue is not exploitable. Nevertheless, if the decompose functions are used in the future without considering this issue, subtle bugs might be introduced.
**Recommendation**.
We recommend documenting that behavior in the code to make it more maintainable and warn about potential issues.
**Client Response**.
This issue has been acknowledged and fixed. The fix documents why the lookup is skipped. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Identical SHA256 Hashes for Different Inputs with the Sponge API
- **Severity**: Low
- **Location**: sha256
**Location**: `src/hash/sha256/mod.rs`
**Description**.
Midnight circuit implements the `SpongeInstructions` for sha256 and supports `absorb` and `squeeze` multiple times. However, the `squeeze` function pads the total length of the input data since the start. This may cause producing identical hashes for different inputs.
```rust
fn squeeze(
&self,
layouter: &mut impl Layouter,
state: &mut Self::State,
) -> Result<[AssignedByte; 32], Error> {
// the total length of useful data hashed;
// this valued will need to be placed in the last two words of the final block
let input_length = state.msg_length;
let padding_data = self.chip.compute_padding(input_length as u64);
...
self.absorb(layouter, state, &assigned_digest_bytes)?;
Ok(assigned_digest_bytes.try_into().unwrap())
}
```
Consider the following scenarios:
1. **First Sequence**: Absorb `data1` → Squeeze `hash1` → Absorb `data2` → Squeeze `hash2`. Here, `hash2` will be calculated as `compress(data1 || padding1 || hash1 || data2 || padding2)`.
2. **Second Sequence**: Absorb `data1 || padding1 || hash1 || data2` → Squeeze `hash3`. In this case, `hash3` will also be calculated as `compress(data1 || padding1 || hash1 || data2 || padding2)`.
In these two sequences they absorb different input data (and squeeze) but produce the same hash.
**Impact**.
In circuits utilizing `SpongeInstructions`, it may be possible to produce identical hashes for different inputs. However, depending on the circuit's logic, exploiting this behavior might be challenging.
**Recommendation**.
We recommend either documenting this as expected behavior or addressing the issue to prevent such collisions.
**Client Response**. This issue has been acknowledged.
### No 16-Bit Range Check for W Halves in SHA256
- **Severity**: Low
- **Location**: sha256
**Location**: `src/hash/sha256/table{11,16}.rs`
**Description**.
The process function in message schedule returns 64 words and the halves for those words:
```rust
let (w, w_halves) = config.message_schedule.process(layouter, input_values)?;
```
The `w` should be a 32-bit word and the `w_halves` should be 16-bit values. However the `w_halves` are not range checked in the `process` function to be 16-bits values. They are later passed to the compression function. A malicious prover can assign `w_halves` values to be larger than 16-bit.
This will not affect the soundness of the circuit. It's because the halves are only used in two places ([subregion_main.rs:73](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/[subregion2.rs:262](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/subregion2.rs#L262) and src/hash/sha256/table11/compression/subregion_main.rs#L73)), which only uses the sum of the halves. However, it is very implicit and lacks documentation. It may cause unintended issues with future updates.
Note that this issue exists in both Table11 ([table11.rs:314](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11.rs#L314)) and Table16 ([table16.rs:256](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L256)).
**Impact**. This will not cause soundness issues. However, it is implicit and may lead to unintended problems in future updates.
**Recommendation**.
We recommend documenting that behavior in the code to make it more maintainable and warn about potential issues.
**Client Response**.
This issue has been acknowledged and fixed. The fix adds a comment to highlight why the range checks are not applied. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
### Dead Code in Poseidon Implementation
- **Severity**: Informational
- **Location**: poseidon
**Location**: `src/hash/poseidon/mod.rs`
**Description**.
The `Sponge` struct ([mod.rs:128-246](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/poseidon/mod.rs#L128-L246)) appears to be unused in the Midnight Circuits codebase.
**Impact**.
This issue has no security implications but unnecessarily increases the complexity of the codebase.
**Recommendation**.
We recommend removing the unused code to simplify the codebase.
**Client Response**.
Acknowledged.
### Code Robustness of Auxiliary Functions in SHA256
- **Severity**: Informational
- **Location**: sha256
**Location**: `src/hash/sha256`
**Description**.
Some parts of the SHA256 codebase could be written in a more comprehensive and robust manner. For example, both [gates.rs:20-26](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/gates.rs#L20-L26) and [gates.rs:20-26](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/gates.rs#L20-L26) use a `factorial(n)` helper function to compute a scaling factor. This function yields an overflow for arguments `n > 20`.
Another example is `compute_padding` (in both [table16.rs:278-305](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L278-L305) and [table11.rs:442-469](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11.rs#L442-L469)). It deviates from the spec by treating the length (`L`) incorrectly. The spec requires a 64-bit big-endian representation of `L`; however, if the hash input length exceeds $2^{32}$, the current implementation adds an extra byte of zero, producing non-standard padding.
**Impact**.
The current usage of `factorial(n)` is safe in the context of the SHA256 implementation (the only two relevant cases are `n = 3` and `n = 7`). The implementation of `compute_padding` does not have security implications, either.
**Recommendation**.
We recommend fixing the identified issues to improve long-term maintainability of the codebase.
For example, the `factorial(n)` would be more comprehensive with explicit bounds checking, e.g.:
```rust
fn factorial(n: u64) -> Result {
if n > 20 { // 20 is the max safe value for u64
return Err("Inputs > 20 cause the factorial to produce a u64 overflow");
}
if n < 2 {
Ok(1)
} else {
Ok(n * factorial(n - 1)?)
}
}
```
In fact, one could even just use an array of pre-calculated factorials for the relevant cases.
For `compute_padding`, we suggest keeping the implementation as close to the spec as possible or including an assertion that the length will not exceed $2^{32}$.
**Client Response**.
Acknowledged.
### Tags Are Hardcoded for Spread Table Range Checks in Table16 of SHA256
- **Severity**: Informational
- **Location**: sha256
**Location**: `src/hash/sha256/table16/*`
**Description**.
In the spread lookup table of tabl16, the tag column is an advice column. For every lookup it needs to range check the tag to ensure the dense value is in correct range. The tag range is hardcoded number in the gate. It would be better to use an enum for that. For example at [compression_gates.rs:126](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_gates.rs#L126) use `BITS_14` (meaning $< 2^{14}$) instead of `5`.
Besides, the tag column in table16 can be created as a fixed column (like that in table11). In this way for every lookup the tag value will be assigned as fixed value and won't need an extra range check in the gate.
**Impact**.
Although we did not find any potential issue in the hardcoded values, subtle bugs could be introduced if it uses the wrong tag or forgets to change the tags after an update to the number of tags provided.
**Recommendation**.
We recommend using an enum for the tag range check or creating the tag column as a fixed column.
**Client Response**.
Acknowledged
### Typos, Incorrect Documentation, and Redundant Code in SHA256
- **Severity**: Informational
- **Location**: sha256
**Location**: `src/hash/sha256`
**Description**.
The SHA256 codebase contains several minor issues, including typos, incorrect comments, and redundant code. These issues are detailed as follows:
- **Redundant Code**: A repeated `enable_equality` instruction in [table16.rs:135](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L135).
- **Typos**:
- In [message_schedule.rs:112](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L112) and [message_schedule.rs:362](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule.rs#L362), the variable `w_minus_9` should be named `w_minus_7`. While the naming is incorrect, the implementation is unaffected and uses the correct value of 7 as verified in [subregion2.rs:231](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L231) and [subregion3.rs:144](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion3.rs#L144). The same issue persist in Table 11 at [message_schedule.rs:111](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule.rs#L111).
- In both Table 11 ([compression_util.rs:856](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/compression_util.rs#L856)) and Table 16 ([compression_util.rs:821](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L821)) the annotation in `copy_advice` is wrong. It should be `ch_hi` instead of `ch_neg_hi`. Additionally, a comment explaining why it is not required to copy `ch_lo` will make the code easier to follow (the value already exist in the proper cell, i.e., row + 1 / a6).
- **Incorrect Comment**:
- The comment at [table16.rs:362](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16.rs#L362) is inaccurate. It states: "if the `w1` block is non-empty," while the code checks if `block1` is empty before proceeding with the required operations. The same issue exists at [table11.rs:406](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11.rs#L406).
- The comment at [subregion2.rs:202-203](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/subregion2.rs#L202-L203) is incorrect, as `sigma_0` values are produced in subregion 2 for words after index 30. A similar comment exists at [subregion2.rs:208](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/subregion2.rs#L208).
- **Variable Renaming**:
- It is suggested to always use the names of the columns from the specification (i.e., `a1`, `a2`, etc.). One example that this is not happening is in the `assign_word_and_halves` function in [schedule_util.rs:190](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_util.rs#L190) where instead of referring to the column as `a5`, `self.message_schedule` is used. The same issue exists in [schedule_util.rs:190](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/schedule_util.rs#L190).
- In both table 15 and table 11 it is suggested to rename all the functions called (or include in their name) `decompose_abcd` and `decompose_efgh` to `decompose_abc` and `decompose_efg`. This is because those functions are never applied to `d` and `h` respectively. Furthermore, there should be additional documentation on why the functions are applied to `b`, `c`, `f`, `g`, as the pieces are never used explicitly for those variables. In our understanding, the function is applied to all variables because it implicitly checks that `word_spread` is indeed the spread of `word_dense`. Similarly, the `AbcdVar` and `EfghVar`, maybe should be renamed to `AVar` and `EVar`, as those variables are only used for `A` and `E` words.
- We recommend verifying that all names include explicit units where relevant, e.g., `BLOCK_SIZE_IN_WORDS` instead of `BLOCK_SIZE` ([mod.rs:39](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/mod.rs#L39)) (or at least a relevant comment).
- **TODOs**: In the SHA256 codebase, there are four unresolved TODO comments. Three of them are related to small refactoring that will improve the code quality, and we suggest resolving them. The other is optimization, and it could stay there as future work.
- **Commented out Code**: In both Table 16 ([schedule_util.rs:34-35](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/message_schedule/schedule_util.rs#L34-L35)) and Table 11 ([schedule_util.rs:34-36](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/message_schedule/schedule_util.rs#L34-L36)) there is some code that has been commented out. We recommend removing those comments.
- **Duplicate Comments**: We also observed that some comments have been duplicated. For example, in [compression_util.rs:517-518](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/compression_util.rs#L517-L518) in Table 16.
- **Code Reuse**: In both Table 16 ([subregion_digest.rs:35-58](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table16/compression/subregion_digest.rs#L35-L58)) and Table 11 ([subregion_digest.rs:35-57](https://github.com/midnightntwrk/midnight-zk/blob/dec9e464d7d8776b6b972666ba51156a7e090fd8/src/hash/sha256/table11/compression/subregion_digest.rs#L35-L57)), the assign digest function could be used instead of manually copying and assigning words `a` and `e`. The function `assign_digest_word` could be used.
- **Code Format**: We also noted that the code is sometimes formatted inconsistently, e.g., missing line breaks, etc, which can easily be resolved by using an automatic code formatter.
**Impact**.
These issues do not have any security implications but addressing them will improve the readability and maintainability of the codebase.
**Recommendation**.
We recommend fixing the identified issues to enhance the code's clarity and correctness.
**Client Response**.
This issue has been acknowledged and partially fixed. The fix solves the `Commented out Code` and the `Typos` issues. Note that the fix has been applied to Table 11, and a similar fix will be applied to Table 16.
---
This report was published on the [zkSecurity Audit Reports](https://reports.zksecurity.xyz) site by [ZK Security](https://www.zksecurity.xyz), a leading security firm specialized in zero-knowledge proofs, MPC, FHE, and advanced cryptography. For the full list of audit reports, see [llms.txt](https://reports.zksecurity.xyz/llms.txt).