Skip to content
This repository has been archived by the owner on Nov 4, 2024. It is now read-only.

Commit

Permalink
some small fixes on the docs (#182)
Browse files Browse the repository at this point in the history
Did some minor fixes on the first chapters
  • Loading branch information
rutefig authored Nov 27, 2023
1 parent 69745a5 commit 802615f
Show file tree
Hide file tree
Showing 5 changed files with 16 additions and 16 deletions.
2 changes: 1 addition & 1 deletion book/appendix_chapter3.md
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ Circuit {
}
```

## Plonkish arithmetization
## Plonkish arithmatization

This is the arithmetization used by Halo2.

Expand Down
2 changes: 1 addition & 1 deletion book/landing_page.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Meet Chiquito

Chiquito is a high-level structured language for implementing zero knowledge proof circuits, currently being implemented in the DSL Working Group of PSE, Ethereum Foundation. It is a step-based zk-language that provides better syntax and abstraction for features like constraint building and column placement. Chiquito has a Halo2 backend, which is a low level zkDSL that writes circuits using the PLONKish arithemtization and is working on supporting additional backends.
Chiquito is a high-level structured language for implementing zero knowledge proof circuits, currently being implemented in the DSL Working Group of PSE, Ethereum Foundation. It is a step-based zk-language that provides better syntax and abstraction for features like constraint building and column placement. Chiquito has a Halo2 backend, which is a low level zkDSL that writes circuits using the PLONKish arithmetization and is working on supporting additional backends.

Chiquito circuits can be written using both Python and Rust. This book focuses on Python.

Expand Down
16 changes: 8 additions & 8 deletions book/part1_chapter1.md
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
# What is Zero Knowledge Proof (Developer POV)?

Zero Knowledge proofs (or ZKP) allow developers to create mathematical proofs that a computation have been executed correctly, while not having to reveal all the data of this computation.
Zero Knowledge proofs (or ZKP) allow developers to create mathematical proofs that a computation has been executed correctly, while not having to reveal all the data of this computation.

## What are the applications of ZKP?

There are three main areas of application:
+ Privacy: because not all data has to be reveal we can proof computations and facts while preserving privacy or secrecy of some part of the data.
+ Privacy: because not all data has to be revealed we can proof computations and facts while preserving privacy or secrecy of some part of the data.
+ Scalability and verified computation: usually to check that a computation has been executed correctly you would need to execute it and check the results are the same. With ZKP you can validate the mathematical proof of the computation, and in some systems this could require less time and space resources than executing the computation itself.
+ Interoperability and trustlessness: because ZKPs are based on mathematical proofs, an organisation or individual can trust a ZKP proof without trusting other participants.
+ Interoperability and trustlessness: because ZKPs are based on mathematical proofs, an organisation or individual can trust a ZK proof without trusting other participants.

## What are ZKP proving systems?

Expand All @@ -19,25 +19,25 @@ The main elements are:
+ The witness: which is the data of the computation. The witness is made of many elements, sometimes called signals or cells. Some signals are public and other private, the public part is sometimes called the **instance** and the private part is sometimes called the **advice**. The witness usually contains the input and output of the computation, but also most or all its intermediate values (the trace).
+ Setup: it is a series of constraints or assertions over the witness data, that define which computations are valid.
+ Witness generation: an algorithm that helps calculating the right values for all the signals.
+ Proving and validation key: given a setup the proving system can generate proving and validation pair of keys. Both can be made public.
+ Proving and validation key: given a setup the proving system can generate a proving and validation pair of keys. Both can be made public.
+ Proof and prover: given a setup and a witness, the prover using the proving key can generate a proof. This proof will be valid if and only if the witness follows the setup constraints.
+ Validator: given a proof and the public part of the witness and a validation key, the validator using the proving system can check that the proof is valid. That is, to generate that proof the prover had to have a witness (if which this public part is part of) that followed the setup.
+ Validator: given a proof, the public part of the witness and a validation key, the validator can check the proof is valid using the proving system. Which means, to generate that proof the prover had to have a witness (in which this public part is part of) that followed the setup.

It is important to note that if the prover and validator have agreed on the setup will have the same proving and validation keys, and will not have to trust each other.
It is important to note that, if the prover and validator have agreed on the setup, they will have the same proving and validation keys, and they will not need to trust on each other.

![](images/zkp-process-diagram.png)

## What is a ZKP arithmetization?

An arithmetization is the way to represent the setup to the proving system. They are very low level and based on polynomials. As a simile, if the proving system is a CPU, the arithmetization is its machine code.
An arithmetization is the way to represent the setup to the proving system. It is very low level and based on polynomials. As a simile, if the proving system is a CPU, the arithmetization is its machine code.

## What is a ZKP low-level DSL?

It is a tool to write arithmetization in a more developer friendly way, but still very close to the arithmetization. If arithmetization is machine code, a ZKP low-level DSL is like assembly.

## What is a ZKP high-level structured language?

They allow to write the setup in a way that is closer to the way a developer thinks about the computation, and they get compiled to the arithmetization. Following the previous simile a ZKP high-level structured language is like Python.
It allows to write the setup in a way that is closer to the way a developer thinks about the computation, and it gets compiled to the arithmetization. Following the previous simile a ZKP high-level structured language is like Python.

Chiquito is an example of ZKP high-level structured language that is based on steps.

Expand Down
10 changes: 5 additions & 5 deletions book/part1_chapter3.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

## ZKP as trace

ZKP generates proofs that an algorithm has been execute correctly.
ZKP generates proofs that an algorithm has been executed correctly.

The best way we can analyse a particular execution of an algorithm is by its trace.

Expand Down Expand Up @@ -64,21 +64,21 @@ For example, we can have the step type `set $variable to $value` and the constra

## ZKP witness as a trace

In the same way, we can see the witness as a the trace of a computation plus some information about the states between the steps.
In the same way, we can see the witness as the trace of a computation plus some information about the states between the steps.

The programming model in chiquito follows the idea that every zero knowledge proof represents a program (the setup), which can have many computations (the trace) that is proven for a certain input, output and intermediate values (the witness).

## Step types and step instances

A trace is made of a sequence of step instances or trace steps, that contains the data about that step instance.

Each step instance belong to a step type. A step types contains rules (or constraints) about whether a step instance is valid in relation to its data and the data of other step instances relative to it.
Each step instance belongs to a step type. A step type contains rules (or constraints) about whether a step instance is valid in relation to its data and the data of other step instances relative to it.

Step types are part of the setup, which means that they cannot change between proofs, but this circuit can proof all possible traces, as they are part of the witness.

## Signals and rotations

Signals represent are elements of the witness that have a independent value for each trace step, but in chiquito paradigm you can see them as variables on the trace steps.
Signals represent elements of the witness that have an independent value for each trace step, but in chiquito paradigm you can see them as variables on the trace steps.

Rotation refer to the capability of creating rules that involved the value of signals in other trace steps with an offset relative to the trace step, not just the value of a signal. A rotation of 0, represent the value of the signal in the same trace step, a rotation of 1 in the next step, a rotation of -1 in the previous step, in general any rotation number is posible.

Expand All @@ -88,7 +88,7 @@ There are two types of signals that are shared between the step types, **forward

**Internal** signals are not shared between step types, and belong to a specific step type and cannot be rotated.

There is a special type of signal called **fixed**, that is not part of the witness and it is used to contain constants.
There is a special type of signal called **fixed**, that is not part of the witness and it is used to define constants.

| | Scope | Rotation | Role |
| -------- | ---------------- | --------- | ------- |
Expand Down
2 changes: 1 addition & 1 deletion book/part1_chapter4.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ When you need to do a rotation on a signal you can use the operators `.next()`,
+ `when(selector, when_true)`: Logical imply.
+ `unless(selector, when_false)`: Logical imply when !selector.
+ `cb_not(a)`: Not operator.
+ isz(a): Equal to zero.
+ `isz(a)`: Equal to zero.
+ `if_next_step(step_type, a)`: If next step is step_type, implies a.
+ `next_step_must_be(step_type)`: Enforces next step must be step_type.
+ `next_step_must_not_be(step_type)`: Enforces next step must not be step_type.
Expand Down

0 comments on commit 802615f

Please sign in to comment.