# 通用零知识虚拟机与高效区块链累加器使用文档

本文档面向三个核心组件：`zawa` 通用零知识虚拟机及其链上部署流程、`Accumulator` 提供的三叉 Anemoi Merkle 累加器，以及 `AC4` 约束验证器（用于 Circom/Halo2 电路的约束健全性审计）。内容涵盖依赖、目录约定、命令行参数、产物位置与常见排障。

---

## 第一部分：ZAWA 通用零知识虚拟机与链上 Membership 示例

### 1. 框架概览与依赖
- **定位**：WASM → 零知识电路的通用 ZKVM，后端采用 HyperPlonk + ML-KZG（见 `zawa/README.md`）。
- **依赖**：系统需安装 `clang`、`lld`；Rust 环境使用项目根的 `rust-toolchain` 固定版本。
- **目录速览（`zawa/`）**  
  - `crates/zkwasm/...`：ZKVM 核心  
  - `contracts/`：示例合约与链上脚本  
  - `params/`、`output/`：默认参数与证明产物输出位置  
  - `test_cli.sh`、`test_membership.sh`：端到端示例脚本

### 2. CLI 总体用法
所有子命令共用全局入口（在 `zawa/` 运行）：
```bash
cargo run --release -- --params <PARAMS_DIR> <NAME> <SUBCOMMAND> [OPTIONS...]
# <NAME> 作为产物前缀（可空）；--params 指向参数缓存目录。
```
支持的核心子命令：
- `setup`：预计算并缓存多项式承诺参数，必要时根据 `--wasm` 探测电路形状。常用参数：`-k <K>` 电路规模，`--wasm <WASM>`。
- `prove`：执行 wasm、构造电路、生成证明与公开实例。参数：`--output <DIR>`、`--public/--private/--ctxin` 等输入、`--mock` 先行模拟、`--file` 大规模文件化跟踪。
- `verify`：离线验证，消费 `<NAME>-verifier_params.bincode`、`<NAME>-instances.bincode`、`<NAME>-proof.bin`。

典型示例（Fibonacci）：
```bash
cd zawa
cargo build --release
cargo run --release -- --params ./params wasm_output setup \
  --k 18 --wasm crates/zkwasm/wasm/fibonacci.wasm
cargo run --release -- --params ./params wasm_output prove \
  --wasm crates/zkwasm/wasm/fibonacci.wasm --output ./output \
  --public 10:i64 --k 18 --mock
cargo run --release -- --params ./params wasm_output verify --output ./output
```

### 3. Membership 场景（本地证明）
- **Guest 逻辑**：`contracts/membership_logic/src/lib.rs` 实现 20 层 4-limb SMT 路径校验。输入约定：
  - `flag`（公开，channel 1）：`1` 代表成员，`0` 代表非成员（叶子固定为 0）。
  - `expected_root`（公开，channel 1，4×u64）。
  - `user_key`（公开，channel 1，4×u64），通过 Poseidon 哈希得到叶子。
  - `siblings`（私有，channel 0，每层左右兄弟各 4×u64，共 20 组）。
  - 电路按路径位（来自 `user_key`）决定左右拼接，再滚动 Poseidon，最终 `require` 根一致。
- **自动化脚本**：`zawa/test_membership.sh` 提供 `setup / prove_mem / prove_nonmem / verify / all`。示例：
  ```bash
  cd zawa
  ./test_membership.sh setup      # 生成 params（默认 ./params）
  ./test_membership.sh prove_mem  # 用内置样例生成 membership 证明
  ./test_membership.sh verify     # 本地验证 output 下产物
  ```
  产物默认写入 `zawa/output/`：`membership-verifier_params.bincode`、`membership-instances.bincode`、`membership-proof.bin`；WASM 位于 `target/wasm32-unknown-unknown/release/membership_logic.wasm`。

### 4. Membership 链上合约与部署流程
- **合约逻辑**：`contracts/membership_verifier/src/lib.rs`
  - `init_contract`：读取参数 `vp_b64`（Base64 的 verifier_params.bincode），持久化到状态 `zkwasm_vp/vk`。
  - `upgrade`：可选覆盖 `vp_b64`，便于更新验证密钥。
  - `verify`：读取调用参数 `instances_b64`、`proof_b64`（均为 Base64，内部 bincode 结构与 CLI 输出一致），反序列化后调用 `zkwasm_verifier::verify_proof`，成功则通过事件 `zkwasm_membership` 记录 `{root,address,ok:true}`。
- **一键脚本**：`contracts/run_membership_chain.sh`
  - 默认目录假设：项目根下有 `zawa/` 与 `chainmaker-go/`。可修改脚本顶部变量：`ZAWA_DIR`、`CHAIN_DIR`、`SDK_CFG`、`WASM_PATH`、`OUTPUT_DIR`。
  - 作用：检查/启动本地 ChainMaker 集群 → Base64 编码 `output` 产物到 `/tmp/zawa_chainmaker/` → 尝试 `upgrade`，失败则 `create` 合约 `zkwasm_membership` → 调用 `verify` 并打印返回与日志耗时。
  - 快速使用：
    ```bash
    cd zawa/contracts
    chmod +x run_membership_chain.sh
    ./run_membership_chain.sh
    ```
    运行前需确保：
    - `chainmaker-go/tools/cmc/cmc` 存在，`build/release/chainmaker-*/` 节点可启动；
    - `zawa/target/wasm32-unknown-unknown/release/membership_verifier.wasm` 与 `zawa/output` 三个产物已生成；
    - SDK 配置默认读取 `chainmaker-go/tools/cmc/testdata/sdk_config_pk.yml`（根目录也有副本 `sdk_config_pk.yml`，如自定义证书/端口需同步调整）。
  - 常见排障（源自 README）：  
    - “connection error ... 12301” → 确认节点已启动且端口放行。  
    - “decode byteCode string failed” → 检查 `WASM_PATH` 指向实际文件。  
    - 日志无 “used time ...” → 调整脚本 `print_exec_time` 的系统日志路径。

### 5. 产物与路径速查
- CLI 生成：`<OUTPUT>/<NAME>-verifier_params.bincode`、`<NAME>-instances.bincode`、`<NAME>-proof.bin`。
- Membership 示例固定命名前缀：`membership-*`，输出在 `zawa/output/`。
- 合约 WASM：`zawa/target/wasm32-unknown-unknown/release/membership_verifier.wasm`。
- 临时 Base64 文本：`/tmp/zawa_chainmaker/*.txt`（由一键脚本生成，可清理）。

---

## 第二部分：Accumulator 三叉 Merkle 累加器

### 1. 功能概览
- Halo2/SHPLONK/KZG 实现的三叉 Merkle 成员电路，使用 ZK 友好的 Anemoi Jive 哈希。
- 提供链下 Merkle 根计算、输入格式校验、分步 CLI（`examples/zk_cli.rs`）与输入转换工具（`examples/build_input_bin.rs`）。

### 2. 输入格式与辅助工具
- 核心结构 `MerkleInput`（`examples/common/input_format.rs`）：
  - `leaf: Fr`
  - `siblings: Vec<(Fr, Fr)>`（每层两个兄弟）
  - `positions: Vec<usize>`（0/1/2 对应 Left/Middle/Right，长度需与 siblings 一致）
  - `expected_root: Option<Fr>`（可空，空则链下计算）
- JSON → 二进制：使用示例工具
  ```bash
  cargo run --example build_input_bin --release -- <input.json> <output.bin>
  # JSON 示例：
  # { "leaf":"42", "siblings":[["100","0"]], "positions":[0], "expected_root":null }
  ```
  生成的 `<output.bin>` 即 `MerkleInput` 的 bincode 序列化，可供 prove/verify 直接读取。

### 3. 分步 CLI（`examples/zk_cli.rs`）
1) **构建**  
   ```bash
   cd Accumulator
   cargo build --release
   ```
2) **setup**：生成公共参数与密钥  
   ```bash
   cargo run --example zk_cli --release -- setup <k> [output_dir=./output]
   ```
   - 自动推导最大支持深度（默认每层 64 行、预留 64 行；`depth ≈ (2^k - 64)/64`）。  
   - 产物：`params.bin`、`vk.bin`、`pk.bin`（均写入 `output_dir`）。若未提供 `input.bin`，使用虚拟路径锁定电路规模。
3) **prove**：读取输入与密钥生成证明  
   ```bash
   cargo run --example zk_cli --release -- prove <setup_dir> [input.bin] [output_dir=setup_dir]
   ```
   - `input.bin` 可显式传入；否则默认查找 `<setup_dir>/../input.bin`。  
   - 会检查输入深度是否超出 setup 的 `k` 支持范围，超出需用更大 `k` 重做 setup。  
   - 产物：`proof.bin`、`public_inputs.bin`（公共输入包含 `expected_root` 与 `leaf`，便于 verify 不依赖原始输入），重用 `params.bin`、`pk.bin`。
4) **verify**：消费公共输入与证明  
   ```bash
   cargo run --example zk_cli --release -- verify <setup_dir> [input.bin]
   ```
   - 默认读取 `<setup_dir>/public_inputs.bin`，也可通过额外参数指定另一份 `input.bin`。  
   - 依赖文件：`params.bin`、`vk.bin`、`proof.bin`。

### 4. 示例最小闭环
```bash
cd Accumulator

# 1) 生成示例输入（JSON -> bincode）
cargo run --example build_input_bin --release -- examples/data/sample_input.json examples/data/input.bin

# 2) setup（使用示例目录）
cargo run --example zk_cli --release -- setup 14 examples/data/output

# 3) prove（显式输入路径）
cargo run --example zk_cli --release -- prove examples/data/output examples/data/input.bin

# 4) verify
cargo run --example zk_cli --release -- verify examples/data/output
```
产物集中在 `examples/data/output`：`params.bin`、`vk.bin`、`pk.bin`、`proof.bin`、`public_inputs.bin`。

### 5. 关键提示与排障
- `positions` 值必须在 {0,1,2}，长度与 `siblings` 匹配，否则解析时报错（由 `MerkleInput::validate` 触发）。
- 若 prove 报“输入路径长度超出最大深度”，需提高 `k` 重新执行 setup。
- `input.bin` 与 `public_inputs.bin` 存在时，verify 不再需要原始 JSON；缺失 `public_inputs.bin` 会直接报错提示补齐。
- 所有文件为原始二进制格式（RawBytes 序列化），不同目录间复制需保持成对一致：`params.bin` 与 `vk.bin/pk.bin/proof.bin/public_inputs.bin` 必须来自同一轮 setup。

---

## 第三部分：AC4 约束验证器（Circom/Halo2 电路约束审计）

### 1. 功能概览
- **定位**：对零知识电路的约束进行健全性审计，识别输出信号是否存在欠约束（under-constrained）或过约束（over-constrained）风险。  
- **支持对象**：Circom（R1CS）与 Halo2（通过 halo2-analyzer 转写得到的中间约束）。  
- **目录速览（`AC4/`）**  
  - `src/frontend/`：Circom / Halo2 约束转写器与统一 JSON 格式  
  - `src/solvers/`：后端求解与分类器  
  - `benchmarks/`：Circom/Halo2 示例数据与样例电路  
  - `scripts/`：批量与单例运行脚本、结果汇总脚本

### 2. Python 环境（推荐虚拟环境）
AC4 的求解器与测试脚本依赖 Python 包。建议在项目根目录创建虚拟环境（例如 `./.venv`），并安装依赖：
```bash
python3 -m venv .venv
. .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install sympy frozendict tqdm galois
```

### 3. Circom：单电路验证（最小闭环）
Circom 路线会执行：`circom` 编译 → R1CS 转 JSON → 求解判定。示例（使用仓库内置样例）：
```bash
cd AC4
. ../.venv/bin/activate
./scripts/run_single_circom.sh benchmarks/circom/utils_circom/AND@gates.circom
```
输出位置：
- 工作目录：`AC4/downloads/<circuit>_circuit_processing_<timestamp>/`
- 结果日志：同目录下 `*_result.txt`（包含 `PURE_EXACT_CONSTRAINED` / `UNDER_CONSTRAINED` 等判定）

### 4. Circom：批量示例集验证
对内置 JSON 数据集进行批量求解（不依赖 Circom 编译器）：
```bash
cd AC4
. ../.venv/bin/activate
./scripts/run_benchmarks.sh
```
结果文件位于 `AC4/benchmarks/results/`。

### 5. Halo2：单 case 验证（生成中间表示 + AC4 判定）
Halo2 路线需要先生成 `halo2intermediate`（每个 case 对应一个 JSON），再用 AC4 对该中间表示求解判定。

1) 生成 `halo2intermediate`（以 `fibonacci_1` 为例）：
```bash
cd AC4
. ../.venv/bin/activate
mkdir -p halo2-analyzer/halo2intermediate
cd halo2-analyzer
AC4_HALO2_EXPERIMENT="$(pwd)/.." AC4_HALO2_CASES="fibonacci_1" cargo run --release
```

2) 运行 AC4（只跑该 case）：
```bash
cd AC4
. ../.venv/bin/activate
./scripts/run_halo2_ac4_only.sh --cases fibonacci_1
```

输出位置：
- 中间文件：`AC4/halo2-analyzer/halo2intermediate/*.json`
- AC4 运行日志：`AC4/logs/halo2_ac4_only/ac4_run.log`
- 判定汇总：`AC4/logs/halo2_ac4_only/summary.txt`
- 细粒度结果：`AC4/scripts/1_ac4_halo2_eval/constrain_log/*.txt`

### 6. Halo2：全流程批量评估（可选）
若希望一键跑 halo2-analyzer + AC4 + 汇总（默认全量 case）：
```bash
cd AC4
. ../.venv/bin/activate
source ./scripts/1_ac4_halo2_eval/bash.sh
```