docs: cairo execution trace #214
Conversation
Codecov Report
@@ Coverage Diff @@
## main #214 +/- ##
=======================================
Coverage 94.87% 94.87%
=======================================
Files 33 33
Lines 7069 7069
=======================================
Hits 6707 6707
Misses 362 362 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
docs/src/starks/execution_trace.md
Outdated
|
|
||
| But there's a trick. If the last executed instruction is any instruction, and it's copied, the transition constraints won't be satisfied. To be able to do this, we need to use something called "proof mode". In proof mode, the main function of the program is wrapped in another one, which calls it and returns to an infinite loop. This loop is a jump relative 0. | ||
|
|
||
| Since this loop can be executed many times without changing the validity of the trace, it can be copied as many times as |
There was a problem hiding this comment.
it seems like the sentence is incomplete at the end
docs/src/starks/execution_trace.md
Outdated
|
|
||
| The first is critical for the verifier to not only know that something was executed correctly but to know what was executed. | ||
|
|
||
| To make this check, we need to add dummy accesses on the memory cells with address 0 and value 0, which helps us prove it was used by changing the final value of the constraints that ensure that the memory is continuous and read-only. |
There was a problem hiding this comment.
I would add that the (0, 0) dummy accesses are added to the unsorted memory accesses, and that before sorting when making the permutation argument, the dummy accesses are overwritten by the public memory ones. So at the end, for the permutation argument to work, we have two columns:
- the unsorted original memory accesses + holes + (0, 0) dummy acceseses
- the sorted full memory column
There was a problem hiding this comment.
The details of the calculation may be dispatched to the paper, but the (0, 0) accesses in the unsorted column is the reason why the final cumulative product is not 1
There was a problem hiding this comment.
I've added a more detailed explanation on how that works
|
@MauroToscano nice one, just a little comment on the whole holes filling/padding part. |
I'd do it more generic since we may change that. With sub columns we may change that layout. But, i'll mention how it can be done. |
|
|
||
| #### Trace extension / Padding | ||
|
|
||
| The last step is padding the trace to a power of two for efficiency. We may also need to pad the trace if for some reason some unbalance is given by the layout. |
There was a problem hiding this comment.
| The last step is padding the trace to a power of two for efficiency. We may also need to pad the trace if for some reason some unbalance is given by the layout. | |
| The last step is padding the trace to a power of two for efficiency. We may also need to pad the trace to balance the layout. |
| building components of the instruction interact to change the VM state, refer to the Cairo | ||
| whitepaper, sections 4.4 and 4.5. |
There was a problem hiding this comment.
I would add a link to the paper here
No description provided.