chore: add documents

Author: alannotnerd

Cargo.lock

@@ -7,4 +7,4 @@ edition = "2021"
 
 [dependencies]
 halo2_proofs = { git = "https://github.com/scroll-tech/halo2", branch="develop" }
-regex-automata = { path = "../../alannotnerd/regex/regex-automata" }
+regex-automata = { git = "https://github.com/alannotnerd/regex" }

Cargo.toml

@@ -0,0 +1,34 @@
+# zkregex(WIP)
+
+## Overview
+This repository showcases a Proof of Concept (POC) demonstrating the use of halo2 for validating regular expression (regex) matching processes. By transforming regex into Deterministic Finite Automata (DFA) using the regex_automata crate, this project demonstrates an innovative approach to regex matching verification.
+
+## Limitation
+This crate is WIP, and has some limitations:
+
+- Support only ASCII code
+- `Unanchored` mode only
+- Only support full text matching
+
+## Getting Start
+### Prerequisites
+- rustc (only tested in latest nightly version)
+
+### Installation
+1. Clone the repository
+```bash
+git clone https://github.com/alannotnerd/zkregex
+```
+
+2. Navigate to the project directory
+```bash
+cd zkregex
+```
+
+3. Build the project
+```bash
+cargo run --release
+```
+Note: This runs with `MockProver` which doen't create a real proof.
+
+

README.md

@@ -1 +1,2 @@
-pub(crate) const MAX_STATE: u64 = 1000u64;
+//TODO(alan): It should be corresponding to the DFA budler, which still needs effort.
+pub(crate) const MAX_STATE: u64 = 65536u64;

src/constants.rs

@@ -10,6 +10,8 @@ use regex_automata::{
 
 use crate::regex::DFADef;
 
+/// Convert the regular expressions into a DFA. It only supports the `Unanchored` mode, which means
+/// the position matchers, like '^', '&', will lead to an error.
 pub fn gen_regex_dfa_def(regex: &str) -> DFADef {
     let dfa = Builder::new()
         .configure(
@@ -48,6 +50,7 @@ pub fn gen_regex_dfa_def(regex: &str) -> DFADef {
     }
 }
 
+/// A helper function that generates the matching process traces step by step.
 pub fn gen_traces(regex: &str, input: &[u8]) -> Vec<(u16, u8, u64)> {
     let dfa = Builder::new()
         .configure(
@@ -72,7 +75,7 @@ pub fn gen_traces(regex: &str, input: &[u8]) -> Vec<(u16, u8, u64)> {
     traces.push((0, 0, state.as_u64()));
     state = dfa.next_eoi_state(state);
     traces.push((0, 0, state.as_u64()));
-    
+
     traces
 }
 

src/dfa.rs

@@ -1,7 +1,4 @@
-use std::{
-    collections::{BTreeSet, HashMap, HashSet},
-    marker::PhantomData,
-};
+use std::{collections::BTreeSet, marker::PhantomData};
 
 use halo2_proofs::{
     circuit::{Layouter, Value},
@@ -37,6 +34,8 @@ pub struct DFADef {
     pub accepted_state_val: u64,
 }
 
+/// Table that contains all valid transitions. It doesn't contains travil transitions, eg, from
+/// `DEAD` state to `DEAD` state.
 #[derive(Clone)]
 pub struct DFATable<F> {
     pub class_id: TableColumn,
@@ -108,15 +107,22 @@ impl<F: PrimeField> DFATable<F> {
 
 /// Table layout
 /// | character | class_id | state | q_state_check | q_enable |
+///
+/// NOTE: We should also add constraints for ``(character, class_id)`, which is trivial.`
 
 #[derive(Clone)]
 pub struct RegexCircuitConfig<F> {
+    /// Only enabled at the begin and the end row. In this stage, we need to check the state equals
+    /// to init state or accepted state
     q_state_check: Selector,
     state: Column<Advice>,
     character: Column<Advice>,
     class_id: Column<Advice>,
+    /// Points out the expected matching state.  
     expected_state: Column<Advice>,
+    /// Deactive in padding rows, otherwise active.
     q_enable: Selector,
+    /// Transition table
     dfa_table: DFATable<F>,
 }