diff --git a/docs/cuda/_category_.json b/docs/cuda/_category_.json index 74e1b70..34dd705 100644 --- a/docs/cuda/_category_.json +++ b/docs/cuda/_category_.json @@ -1,4 +1,4 @@ { "label": "zkCuda", - "position": 5 + "position": 6 } \ No newline at end of file diff --git a/docs/faq/_category_.json b/docs/faq/_category_.json index dbfed68..535f466 100644 --- a/docs/faq/_category_.json +++ b/docs/faq/_category_.json @@ -1,4 +1,4 @@ { "label": "Troubleshooting", - "position": 7 + "position": 8 } \ No newline at end of file diff --git a/docs/internal/_category_.json b/docs/internal/_category_.json index ead813a..fb0ef00 100644 --- a/docs/internal/_category_.json +++ b/docs/internal/_category_.json @@ -1,4 +1,4 @@ { "label": "Compiler Internals", - "position": 4 + "position": 5 } \ No newline at end of file diff --git a/docs/rust/std.md b/docs/rust/std.md new file mode 100644 index 0000000..071984d --- /dev/null +++ b/docs/rust/std.md @@ -0,0 +1,53 @@ +--- +sidebar_position: 6 +--- + +# Std +We're supporting some standard circuits in our std library, all of which will implement the following trait: + +```rust +pub trait StdCircuit: Clone + Define + DumpLoadTwoVariables { + type Params: Clone + Debug; + type Assignment: Clone + DumpLoadTwoVariables; + + fn new_circuit(params: &Self::Params) -> Self; + + fn new_assignment(params: &Self::Params, rng: impl RngCore) -> Self::Assignment; +} +``` + +- ```Params``` refers to the parameters used to define a circuit. For example, to build a Merkle Tree circuit, we need to know what's the depth of the tree, and which hash function to use. +- ```Assignment``` refers to the assignment of the private and public input, represented as field elements. In the Merkle Tree example, if we're checking the membership of a leaf, the assignment will consist of the root hash, the leaf hash, and the Merkle path. +- ```new_circuit``` will return a circuit according to ```params```. Note that there are no concrete values in the returned circuit, all variables are placeholders, faciliting the compilation of the circuit structure. +- ```new_assignment```, as the name suggests, returns a group of **correct** assignment. + +## Example usage +We create a ```circuit_test_helper``` in our std library, which can be referred to as an example. + +```rust +use circuit_std_rs::StdCircuit; +use expander_compiler::frontend::*; +use extra::Serde; +use rand::thread_rng; + +pub fn circuit_test_helper(params: &Cir::Params) +where + Cfg: Config, + Cir: StdCircuit, +{ + let mut rng = thread_rng(); + let compile_result: CompileResult = compile(&Cir::new_circuit(¶ms)).unwrap(); + let assignment = Cir::new_assignment(¶ms, &mut rng); + let witness = compile_result + .witness_solver + .solve_witness(&assignment) + .unwrap(); + let output = compile_result.layered_circuit.run(&witness); + assert_eq!(output, vec![true]); +} +``` + +```Cfg``` here can be one of ```BN254Config, M31Config, GF2Config```, and all circuits in the std library can be used as ```Cir```. + +## Supported Circuits +[LogUp](../std/logup.md). A circuit attesting to the correctness of table look up. diff --git a/docs/std/_category_.json b/docs/std/_category_.json new file mode 100644 index 0000000..0879706 --- /dev/null +++ b/docs/std/_category_.json @@ -0,0 +1,4 @@ +{ + "label": "Circuit Std", + "position": 4 +} \ No newline at end of file diff --git a/docs/std/logup.md b/docs/std/logup.md new file mode 100644 index 0000000..8e6b482 --- /dev/null +++ b/docs/std/logup.md @@ -0,0 +1,72 @@ +--- +sidebar_position: 1 +--- + +# LogUp +A LogUp circuit verifies the query of a table, ensuring the result is correct, as illustrated below: + +![lookup](../../static/img/lookup.png) + +Let's say we have a table of $N$ values, denoted as $t_i, i\in [N]$, and we have $M$ queries of the table, whose results are denoted as $q_j, j\in [M]$. To check all the query results are correct, we'd like to prove the following relationship: + +There exists $c_i, i\in [T]$, s.t. + +$$ +\sum_{i\in [T]} \frac{c_i}{X - t_i} = \sum_{j\in [M]} \frac{1}{X - q_j} +$$ + +Thanks to the Schwartz–Zippel lemma, we can sample a random value $\alpha\in\mathbb{F}$ and conclude that the two polynomials are equal with high probability if they agree at $\alpha$. + +## Concrete Definition +In practice, things get a little more complex since the query key can be arbitrarily long, and there might be more than one values in the row of a table. + +```rust +pub struct LogUpParams { + pub key_len: usize, + pub value_len: usize, + pub n_table_rows: usize, + pub n_queries: usize, +} + +declare_circuit!(_LogUpCircuit { + table_keys: [[Variable]], + table_values: [[Variable]], + + query_keys: [[Variable]], + query_results: [[Variable]], + + // counting the number of occurences for each row of the table + query_count: [Variable], +}); + +``` + +We fully parameterized this, allowing arbitrary ```key_len```, ```value_len```, ```n_table_rows```, and ```n_queries```. + +## Circuit Structure: Short Explaination +1. ```table_keys``` and ```table_values``` are concated in the second dimension. +2. ```query_keys``` and ```query_values``` are concated in the second dimension. +3. The second dimension will be reduced to a single value with randomness. +4. At this point, we have a list of $t_i$ and $q_j$ now, and we proceed with the LogUp argument. + +Thanks to the [Expander](https://github.com/PolyhedraZK/Expander) prover, we're able to use random gate in the construction of the ciruict, whose value will be filled via fiat-shamir hash in proving. + +## Test +Below is a small test of the logup circuit: +```rust +#[test] +fn logup_test() { + let logup_params = LogUpParams { + key_len: 7, + value_len: 7, + n_table_rows: 123, + n_queries: 456, + }; + + common::circuit_test_helper::(&logup_params); + common::circuit_test_helper::(&logup_params); + common::circuit_test_helper::(&logup_params); +} +``` + +To see how ```circuit_test_helper``` is defined, please refer to our documentation of the [std library](../rust/std.md). \ No newline at end of file diff --git a/docs/supported_fields.md b/docs/supported_fields.md index 076e2e7..3a0d5ca 100644 --- a/docs/supported_fields.md +++ b/docs/supported_fields.md @@ -1,5 +1,5 @@ --- -sidebar_position: 6 +sidebar_position: 7 --- # Supported Fields diff --git a/static/img/lookup.png b/static/img/lookup.png new file mode 100644 index 0000000..7298c12 Binary files /dev/null and b/static/img/lookup.png differ