Add a new chapter for common types and expand the basic concepts #846
Conversation
|
The latest updates on your projects. Learn more about Vercel for Git ↗︎
|
|
@yunus433 is attempting to deploy a commit to the o1labs Team on Vercel. A member of the Team first needs to authorize it. |
|
|
||
| :::note | ||
|
|
||
| For the cryptography inclined, the exact max value that a field can store is: 28,948,022,309,329,048,855,892,746,252,171,976,963,363,056,481,941,560,715,954,676,764,349,967,630,336 | ||
| For the cryptography inclined, the prime order of the o1js `Field` is: 28,948,022,309,329,048,855,892,746,252,171,976,963,363,056,481,941,560,715,954,676,764,349,967,630,336 |
There was a problem hiding this comment.
This is an improvement to before. But what would also be interesting for cryptographically inclined readers is to know what kind of field this is (Pallas base field) with a link to more details.
Also, I suggest to write the modulus in hex format, because that visually shows the twoadicity
| const MAX_ITERATION_COUNT = 64; | ||
|
|
||
| pow.assertGreaterThanOrEqual(0); | ||
| pow.assertSmallerThanOrEqual(MAX_ITERATION_COUNT); // This code is to calculate up to 2^64, you can optimize this based on your needs |
There was a problem hiding this comment.
Use a 64 bit range check, or pass in a UInt64
| let loopEnded = Bool(false); // Checking if the loop has ended yet | ||
|
|
||
| for (let i = 0; i <= MAX_ITERATION_COUNT; i++) { // Static sized loop | ||
| loopEnded = Provable.if( // End Condition |
There was a problem hiding this comment.
I would do this:
loopEnded = power.equals(i).or(loopEnded);but yours is also ok
|
|
||
| for (let i = 0; i <= MAX_ITERATION_COUNT; i++) { // Static sized loop | ||
| loopEnded = Provable.if( // End Condition | ||
| Field(i).greaterThanOrEqual(power), |
There was a problem hiding this comment.
| Field(i).greaterThanOrEqual(power), | |
| power.equals(i), |
|
|
||
| # Functions | ||
|
|
||
| Functions work as you would expect in TS. However, your functions inside ZKPs must take provable arguments and return provable types, just like anything in o1js. For example: |
There was a problem hiding this comment.
That's not correct. It's common for functions to take parameters that define the circuit, not only variables.
| } | ||
| ``` | ||
|
|
||
| **Warning:** You should _not_ use recursion with functions in o1js. If you want to recurse a ZKP, you can use [o1js recursion](./recursion.mdx). |
There was a problem hiding this comment.
Incorrect, if the recursion terminates on a condition that's static it's fine to use (much like if statements with a static condition)
| const x = Provable.if( | ||
| Bool(foo), | ||
| (() => { // Here, we use arrow functions to return a Field element, but you can use any function that returns a provable type | ||
| return Field(5).div(3); |
There was a problem hiding this comment.
I'm not a big fan of how all our examples only ever use constant field elements as examples, where none of these circuit-writing rules and caveats actually apply
Explaining constants vs variables and then using variables in examples seems an important step in moving to more in-depth docs about circuit writing
| x.not().and(y).or(true); // True | ||
| ``` | ||
|
|
||
| **Important:** All logical expressions are executed in the method call order, as with any other regular language or framework. However, as these are logical statements inside ZKPs, all expressions are always evaluated regardless of the logical ordering. Please see conditionals chapter [below](./common-types-and-functions.md#conditionals) for more details. |
There was a problem hiding this comment.
| **Important:** All logical expressions are executed in the method call order, as with any other regular language or framework. However, as these are logical statements inside ZKPs, all expressions are always evaluated regardless of the logical ordering. Please see conditionals chapter [below](./common-types-and-functions.md#conditionals) for more details. | |
| **Important:** All logical expressions are executed in the method call order, as with any other regular language or framework. However, as these are logical statements inside ZKPs, all expressions are always evaluated regardless of the logical ordering. See [Conditionals](./common-types-and-functions.md#conditionals) for more details. |
There was a problem hiding this comment.
I agree with Gregor, nice work @yunus433 !
Guidance is to omit "please", see Politeness and use of please
Instead of "below" or "here" be sure to use short descriptive link text that helps provide context for the material that you're linking to.
See the new links section in the docs style guide.
|
|
||
| `Provable.if()` allows you to include any logical computation you need inside your ZKP. There is nothing wrong with evaluating more complex expressions inside `Provable.if()` and returning the final result. | ||
|
|
||
| However, it works differently from ternary statements in the other languages and frameworks. Both arguments of `Provable.if()` _always_ executes, regardless of the truth value of the condition. `Provable.if()` choses which one to return based on the truth value and sets the new variable. This is why you should never assign anything outside of the if scope or assert anything. |
There was a problem hiding this comment.
| However, it works differently from ternary statements in the other languages and frameworks. Both arguments of `Provable.if()` _always_ executes, regardless of the truth value of the condition. `Provable.if()` choses which one to return based on the truth value and sets the new variable. This is why you should never assign anything outside of the if scope or assert anything. | |
| However, it works differently from ternary statements in the other languages and frameworks. Both arguments of `Provable.if()` _always_ execute, regardless of the truth value of the condition. `Provable.if()` chooses which one to return based on the truth value and sets the new variable. This is why you should never assign anything outside of the scope or assert anything. |
| @@ -27,109 +27,205 @@ zkApp programmability is not yet available on the Mina Mainnet. You can get star | |||
|
|
|||
| # o1js Basic Concepts | |||
|
|
|||
| o1js, fka. SnarkyJS, is a TypeScript (TS) library for writing general-purpose zk programs and writing zk smart contracts for Mina. | |||
| o1js, fka. SnarkyJS, is a TypeScript (TS) library for writing general-purpose ZK programs and writing ZK smart contracts for the Mina Blockchain. In order to create a ZKP (zero knowledge proof), you should use types and operations that can be converted into a ZKP. o1js gives you a lot of different built in types and customizable structures that you can use to create ZKPs. | |||
There was a problem hiding this comment.
| o1js, fka. SnarkyJS, is a TypeScript (TS) library for writing general-purpose ZK programs and writing ZK smart contracts for the Mina Blockchain. In order to create a ZKP (zero knowledge proof), you should use types and operations that can be converted into a ZKP. o1js gives you a lot of different built in types and customizable structures that you can use to create ZKPs. | |
| o1js, fka. SnarkyJS, is a TypeScript (TS) library for writing general-purpose ZK programs and writing ZK smart contracts for the Mina Blockchain. To create a ZKP (zero knowledge proof), you use types and operations that can be converted into a ZKP. o1js provides different built-in types and customizable structures that you can use to create ZKPs. |
|
|
||
| <!-- prettier-ignore --> | ||
| ```ts | ||
| const x = new Field(42); | ||
| const y = Field(923); // Best practice | ||
| let x = Field(42); | ||
| ``` | ||
|
|
||
| You can create a `Field` from anything that is "field-like": `number`, `string`, `bigint`, or another `Field`. Note that the argument you give must be an integer in the `Field` range. |
There was a problem hiding this comment.
Note that the argument you give must be an integer in the
Fieldrange.
Can you remove the second sentence here? It's not true, an integer outside the field range is also accepted and reduced modulo the field size (as you show below, with negative inputs)
There was a problem hiding this comment.
Or replace it with just "Note that the argument you give must be an integer."
|
|
||
| ## Deeper into the Field Type | ||
|
|
||
| `Field` element is a positive integer in a prime order [finite field](https://en.wikipedia.org/wiki/Finite_field), which is a set of integers in between 1 and the prime order of the field (a.k.a. an arbitrary prime number describing the field). |
There was a problem hiding this comment.
Actually it's the set of integers between 0 and p-1, where p is the prime order!
There was a problem hiding this comment.
| `Field` element is a positive integer in a prime order [finite field](https://en.wikipedia.org/wiki/Finite_field), which is a set of integers in between 1 and the prime order of the field (a.k.a. an arbitrary prime number describing the field). | |
| A `Field` represents a positive integer in a prime order [finite field](https://en.wikipedia.org/wiki/Finite_field), which is the set of integers $0,...,p-1$, where $p$ is the field order. | |
| Concretely, `Field` refers to the [Pallas base field](TODO), which is the native circuit field of the proof system underlying o1js. |
@yunus433 this is how I would describe the field
| However, note that these methods are _not_ provable, meaning you cannot use them in your final zkApp as a part of the ZKP. Use them only to debug your code. | ||
| When you perform an operation inside a finite field, the result always stays in the range. This is achieved through [modular arithmetic](https://en.wikipedia.org/wiki/Modular_arithmetic). This behaviour may be unfamiliar to you if you have not worked with ZKPs before. Let us explain more with some examples. | ||
|
|
||
| In the addition or multiplication operations where the result is bigger than the order of the finite field, you receive the modulus of the result with the prime order of the field. |
There was a problem hiding this comment.
- you receive the modulus of the result with the prime order of the field.
+ you receive the remainder of the result modulo the prime order of the field.| ``` | ||
|
|
||
| However, note that these methods are _not_ provable, meaning you cannot use them in your final zkApp as a part of the ZKP. Use them only to debug your code. | ||
| When you perform an operation inside a finite field, the result always stays in the range. This is achieved through [modular arithmetic](https://en.wikipedia.org/wiki/Modular_arithmetic). This behaviour may be unfamiliar to you if you have not worked with ZKPs before. Let us explain more with some examples. |
| If you try creating a `Field` from a negative number you will receive the modular additive inverse of the number. For instance `(1 + (Field.ORDER - 1)) % Field.ORDER` is 0, so the additive inverse of 1 is `Field.ORDER - 1` in this field. | ||
|
|
||
| In addition to the `Field` type, o1js gives you a variety structures to help you build a powerful zkApp. You can learn more about them in the next chapter, [Common Types and Functions](./common-types-and-functions.md). | ||
| <!-- prettier-ignore --> | ||
| ```ts | ||
| Provable.log(Field(-1)); // This will print `Field.ORDER - 1` | ||
| ``` | ||
|
|
||
| Similarly, if your substraction results in a negative number you will get the modular additive inverse. |
There was a problem hiding this comment.
it's confusing to me that you describe negative numbers / subtraction results in different language than positive overflow. it's the same so should be described in the same language:
"Similarly, if your subtraction results in a negative number, you receive the positive remainder of the result modulo the prime order of the field."
|
|
||
| Similarly, if your substraction results in a negative number you will get the modular additive inverse. | ||
|
|
||
| For division, if the result is not an integer, you receive the [modular multiplicative inverse](https://en.wikipedia.org/wiki/Modular_multiplicative_inverse) of the division: If `(x * y) % p` is `z` (where `p` is the order of the finite field), then the modular multiplicative inverse of the division `z / x` equals `y`. Note that `x`, `y`, and `z` are all integers. |
There was a problem hiding this comment.
- For division, if the result is not an integer, you receive the
+ For division, you receive the of course, if the result is an integer, it's still the modular inverse
| Because of this behaviour, it is usually not very useful to use the final result of an uneven division. Instead, you can prove the result with multiplication. | ||
|
|
||
| <!-- prettier-ignore --> | ||
| ```ts | ||
| // We want x, an argument of the smart contract, to be equal to 7 / 3 | ||
| x.mul(Field(3)).assertEquals(Field(7)); | ||
| ``` |
There was a problem hiding this comment.
I don't see how this is "more useful" than doing let x = Field(7).div(3)
|
|
||
| <!-- prettier-ignore --> | ||
| ```ts | ||
| Provable.log(Field(3).div(Field(5))); // This will print a very big integer |
There was a problem hiding this comment.
we should always use number inputs to methods instead of Field(number), looks cleaner:
Provable.log(Field(3).div(5)); // This will print a very big integerthis applies to the entire PR!
|
|
||
| We have stated many times above that all the code you write in o1js must be provable, but what is provability? | ||
|
|
||
| A provable code can be thought as a code that o1js compiler can convert into a ZKP. Just because you write something with o1js, it does not become automatically provable. You must follow all the rules above and always use provable types in your code. |
There was a problem hiding this comment.
o1js compiler
let's not use the term "compiler", it's a confusion already that people think we compile TS to circuits
| let x_provable = Field(x); // This code is perfectly valid | ||
| ``` | ||
|
|
||
| In reality, the `x_provable` variable in the example above is a _constant_ `Field` variable. By constant, we do not mean that it is a TS constant (which you define by using `const`), but we say that the value of `x_provable` is known at the compilation time. When you receive an argument to your smart contract method, then the argument is not a constant, thus you should only use provable methods on it. |
| Always remember that o1js is used for writing ZKPs, and what you write with o1js must have a sense in the final proof. The public or private inputs of a ZKP may change depending on the user input, but once the inputs are provided, the final ZKP must make sure they are not changed. By using provable o1js variables, you make sure that your variables are always consistent with your proof logic. | ||
|
|
||
| <!-- prettier-ignore --> | ||
| ```ts | ||
| @method foo(x: Field, y: Field) { | ||
| x.add(y).assertEquals(5); // we know neither the value of x, nor of the y, but we are sure that (x + y) % Field.ORDER equals 5 | ||
| } | ||
| ``` |
There was a problem hiding this comment.
all this is really good and important to add, thanks @yunus433
The first commit to update o1js docs based on the O(1) Labs feedback. Changed common types chapter and expanded basic concepts. Added the following information: