# ZK-Email Halo2 Circuit Design
## Deterministic Finite Automaton (DFA) Chip
A deterministic finite automaton (DFA) chip verifies that state transitions of DFA are valid for a given input string. In ZK-Email, it will be used to confirm that the given email string matches with the regular expression corresponding to the DFA.

The DFA chip consists of the following tables and constraints, where $q$ denotes a state of DFA, $Q, t$ represent the number of states and input patterns, respectively, and $n$ is the number of state transitions to be proved. Notably, the following tables are combined and a selector column is also defined in the actual implementation.

Witness table:
| `cur_state` | `next_state` | `input` |
| ----------- | ------------ | ------- |
| $q_1^{cur}$ | $q_2^{next}$ | $x_1$ |
| $q_2^{cur}$ | $q_3^{next}$ | $x_2$ |
| $\vdots$ | $\vdots$ | $\vdots$|
| $q_n^{cur}$ | $q_{n+1}^{next}$| $x_n$|

Lookup table:
| `valid_cur_state` | `valid_next_state` | `valid_input` |
| ----------------- | -------------------- | ---------------|
|$q_1^{cur*}$ | $q_{1,1}^{next*}$ | $x_{1}^*$ |
|$q_1^{cur*}$ | $q_{1,2}^{next*}$ | $x_{2}^*$ |
|$\vdots$ | $\vdots$ | $\vdots$ |
|$q_1^{cur*}$ | $q_{1,t}^{next*}$ | $x_{t}^*$ |
|$q_2^{cur*}$ | $q_{2,1}^{next*}$ | $x_{1}^*$ |
|$q_2^{cur*}$ | $q_{2,2}^{next*}$ | $x_{2}^*$ |
|$\vdots$ | $\vdots$ | $\vdots$ |
|$q_2^{cur*}$ | $q_{2,t}^{next*}$ | $x_{t}^*$ |
|$\vdots$ | $\vdots$ | $\vdots$ |
|$q_{Q}^{cur*}$ | $q_{Q,1}^{next*}$ | $x_{1}^*$ |
|$q_{Q}^{cur*}$ | $q_{Q,2}^{next*}$ | $x_{2}^*$ |
|$\vdots$ | $\vdots$ | $\vdots$ |
|$q_{Q}^{cur*}$ | $q_{Q,t}^{next*}$ | $x_{t}^*$ |

Constraints:
1. $q_1^{cur}=q_1^{cur*}$, where $q_1^{cur*}$ is the fixed initial state in the DFA.
1. For $i\in [n-1]/\{1\}$, $q_i^{next}=q_{i+1}^{cur}$.
1. For $i\in [n]$, there is a row $(q^{cur*},q^{next*},x^*)$ in the lookup table such that $q_i^{cur}-q^{cur*}=0$, $q_i^{next}-q^{next*}=0$, and $x_i-x^*=0$ hold.
1. When $\mathcal{F}=(f_1,f_2,\dots,f_F)$ is a set of accept states, $q_{n+1}^{next} \in \mathcal{F}$ is satisfied.

In a nutshell, the valid patterns of the state transitions are fixed in the lookup table, and the actual state transitions to be proved are written in the witness table. The third constraint requires that each state transition in the witness table is included in the valid patterns. The second constraint confirms that the next state $q_i^{next}$ is used as the current state $q_{i+1}^{cur}$ in the next state transition. The first and the fourth constraints correspond to the initial and final conditions, respectively.