owned this note
owned this note
Published
Linked with GitHub
# Branch overview: `feature/memory_permutation_check`
# Circuit (Theo code của PSE/Halo2)
+ `ShuffleConfig`:
+ ***Inputs***: `input_0, input_1` (cho dãy trước hoán vị), `shuffle_0, shuffle_1` (cho dãy sau hoán vị), và 2 selector `s_input, s_shuffle`.
+ ***Methods***: `construct` và `configure` sử dụng API `shuffle` của PSE
+ `PermutationCircuit`:
+ ***Inputs***: `input_idx, input` (index và giá trị của dãy trước hoán vị - sửa tên input để dễ hiểu hơn), `shuffle_idx, shuffle` (index và giá trị của dãy sau hoán vị).
+ ***Methods***:
+ `new()`: khởi tạo struct với input là 2 trace records được gắn với index tương ứng thành type `Vec<(F, TraceRecord<K, V, S, T>)>`.
+ `configure()` và `synthesize()`: sử dụng lại code của PSE với API `shuffle()`.
# Prover (theo hàm `test_prover()` của PSE)
+ `PermutationProver`:
+ ***Struct members***:
```Rust
params: ParamsIPA<C>
pk: ProvingKey<C>, // Không lưu verify_key vì từ pk có thể lấy được vk: pk.get_vk().
circuit: PermutationCircuit<C::Scalar>,
expected: bool, // Giá trị kì vọng của mạch (trong project sử dụng expected = true)
```
+ ***Methods***: `new(), create_proof() -> Vec<u8>`, và `verify_proof() -> bool`
+ Method mới cho `TraceRecord`: `compress(seed: [u64; 5]) -> F`, map một trace record (5-tuple) thành một field element. Phương pháp map được sử dụng là *dot product* với một random vector `seed`.
# Helper functions
+ `pub fn successive_powers<F: Field + PrimeField>(size: u64) -> Vec<F>`: tạo một vector $\{\omega^i\}: i = 0..size$ dùng làm index cho dãy của mạch permutation.
# Testcases
+ `test_functionality()`: test chức năng của mạch với input cơ bản: Khởi tạo Vec<F, F> làm `input`, hoán vị `input` thành `shuffle`, và đưa vào mạch để kiểm tra.
+ `check_trace_record_mapping()`: test chức năng mapping của trace record: random một trace record, sử dụng hàm `compress()` và so kết quả với công thức tính dot product trực tiếp.
+ `check_permutation_with_trace_record()`: test chức năng của mạch với input là 2 dãy trace record
+ `check_wrong_permutation()` (should panic): check chức năng của mạch khi input bị sai: lấy 1 phần tử bất kì của `shuffle` và thay bằng 1 giá trị random khác.
# Example use
```Rust
const K: u32 = 6;
// Create a tuple vector of (index, trace_element)
let input_trace: Vec<(Fp, TraceRecord<B256, B256, 32, 32>)> =
successive_powers::<Fp>(machine.trace().len() as u64)
.into_iter()
.zip(machine.trace())
.collect();
// Sort the trace by ascending time_log
let sorted_trace = sort_chronologically(input_trace.clone());
// Form the circuit
let circuit = PermutationCircuit::new(input_trace, sorted_trace);
// Test with IPA prover
let mut ipa_prover = PermutationProver::<EqAffine>::new(K, circuit, true);
// Create a proof for the circuit satisfiability
let proof = ipa_prover.create_proof();
// Verify the proof
assert!(ipa_prover.verify(proof));
```
# Adjusts to previous works
+ Sửa order sort trace thành: `address -> time_log -> instruction`.
# Implementation link
+ [Branch `feature/memory_permutation_check`](https://github.com/orochi-network/orochimaru/pull/57)
+ [PSE circuit implementation](https://github.com/privacy-scaling-explorations/halo2/blob/1650a0b07fbbfeebab71f5650ccb62ccd20de0ff/halo2_proofs/examples/shuffle_api.rs#L33-L149)
+ [PSE `test_prover()` function](https://github.com/privacy-scaling-explorations/halo2/blob/1650a0b07fbbfeebab71f5650ccb62ccd20de0ff/halo2_proofs/examples/shuffle_api.rs#L151-L191)