feat: Dynamic Address for Out-of-Domain Row in TASM AIR Evaluation #314
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jan-ferdinand
force-pushed
the
asz/addi
branch
from
3eb6b39
to
ebeb001
Compare
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
9ea388b
to
1c61577
Compare
jan-ferdinand
force-pushed
the
asz/addi
branch
from
ebeb001
to
3b5bc12
Compare
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
1c61577
to
14c270c
Compare
jan-ferdinand
requested changes
Aug 12, 2024
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
4302961
to
7a9102a
Compare
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
2 times, most recently
from
e2541de
to
dab8af8
Compare
Copy and paste is a root of evil. Also, repair the broken abstraction of the `Codegen` trait. changelog: ignore
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
dab8af8
to
7d6ea51
Compare
changelog: ignore
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
7d6ea51
to
9b6bf58
Compare
If the constraints are not in place, the corresponding error message is well suited to figure out what is going on. Since this is a test, not a piece of production code, that's all that's needed. Adding special error handling logic, especially with the to-be-avoided “catch_unwind”, is overkill. changelog: ignore
- introduce `const`s to remove random magic numbers - replace copy-pasted code with closures - use canonical methods of ad-hoc interpretation - reduce nesting level on happy path through early returns - etc. changelog: ignore
jan-ferdinand
force-pushed
the
asz/dynamic-ood-location-2
branch
from
9b6bf58
to
89aa21d
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The current TASM AIR evaluation code is very efficient but has a major drawback: the location of the inputs to the circuit (i.e., the {current, next} {main, aux} out-of-domain (OOD) rows) are statically defined and hence must be known at compile time. As a result, one runs into complications when verifying multiple STARK proofs in a single TASM program; and verifying a dynamic number of them is all but impossible. Moreover, the static location of the OOD rows are baked into the computer program, meaning that even if you do compile a TASM program that verifies multiple proofs, you get different programs (and different digests!) depending on how many proofs you actually need to verify.
This PR adds a second function for evaluating the AIR in tasm. It is a dynamic counterpart to the static one that's already there.
The new function does take a memory layout object, just like the old function does. But the difference is that this new memory layout object only specifies where to find the challenges and where to find free memory. The locations of the OOD rows is given as arguments on the stack. The method then stores these locations in the first few words of the free memory region. Whenever an input needs to be read, the relevant pointer-pointer is read and dereferenced twice -- the second time with the appropriate offset. (In contrast, the static code derefences a regular pointer once.)
In more detail, here are the changes introduced by this PR:
air.rsand directoryaircontain logic related to evaluating AIR.