std&logup

docs/cuda/_category_.json

@@ -1,4 +1,4 @@
 {
   "label": "zkCuda",
-  "position": 5
+  "position": 6
 }

docs/faq/_category_.json

@@ -1,4 +1,4 @@
 {
   "label": "Troubleshooting",
-  "position": 7
+  "position": 8
 }

docs/internal/_category_.json

@@ -1,4 +1,4 @@
 {
   "label": "Compiler Internals",
-  "position": 4
+  "position": 5
 }

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<C: Config>: Clone + Define<C> + DumpLoadTwoVariables<Variable> {
+    type Params: Clone + Debug;
+    type Assignment: Clone + DumpLoadTwoVariables<C::CircuitField>;
+
+    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<Cfg, Cir>(params: &Cir::Params)
+where
+    Cfg: Config,
+    Cir: StdCircuit<Cfg>,
+{
+    let mut rng = thread_rng();
+    let compile_result: CompileResult<Cfg> = compile(&Cir::new_circuit(&params)).unwrap();
+    let assignment = Cir::new_assignment(&params, &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.

docs/std/_category_.json

@@ -0,0 +1,4 @@
+{
+  "label": "Circuit Std",
+  "position": 4
+}

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::<BN254Config, LogUpCircuit>(&logup_params);
+    common::circuit_test_helper::<M31Config, LogUpCircuit>(&logup_params);
+    common::circuit_test_helper::<GF2Config, LogUpCircuit>(&logup_params);
+}
+```
+
+To see how ```circuit_test_helper``` is defined, please refer to our documentation of the [std library](../rust/std.md).

docs/supported_fields.md

@@ -1,5 +1,5 @@
 ---
-sidebar_position: 6
+sidebar_position: 7
 ---
 
 # Supported Fields