Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix the memory CTL and implement the verifier memory bus #1026

Merged

Conversation

hratoanina
Copy link
Contributor

This pull request fixes the memory CTL so that it doesn't have to be disabled anymore.
It also introduces a verifier-only memory bus to check a small set of memory operations.

KeccakSponge endianness

Related issue: #1004
In the KeccakSponge STARK, the output of the hash is stored in u32 columns written in big endian format. This introduces a discrepancy with how the columns are written in the Memory STARK, and makes the CTL check fail. The easiest solution to implement we found was to add columns in KeccakSponge for individual bytes of the output, which can be recombined in little endian format.

Verifier-only memory bus

Following Daniel's advice here, we introduced a set of memory operations which can be directly checked by the verifier by multiplying their contribution to the looked product. For the sake of generality, these extra values can be added to any CTL product though we only need it for memory.
For now, the operations checked by the verifier are the block metadata writes before kernel bootstrapping and the trie hash roots reads at the end of the execution.

Further work:

  • To make sure they are consistent, the trie hash roots should be public inputs of the SNARK wrapper. I believe this is not the case yet.
  • For the trie hash roots reads, we need the CPU trace length of the underlying CPU STARK. For now it's provided manually, but it should be propagated from the base CPU STARK to its SNARK wrapper, and all the way through the SNARK recursion chain to the root circuit. It could be handled with public inputs, or maybe with another verifier-only read of a global variable keeping track of the number of steps of the CPU?

evm/src/cross_table_lookup.rs Outdated Show resolved Hide resolved
evm/src/fixed_recursive_verifier.rs Outdated Show resolved Hide resolved
evm/src/generation/mod.rs Outdated Show resolved Hide resolved
}

// Arithmetic
for _ in 0..stark_config.num_challenges {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can this be done using extra_looking_products.push(vec![builder.constant(F::ONE); stark_config.num_challenges]);? Or even combining the four loops into one vec![vec![...]] expression?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It could be, the idea is that specific functions for the other CTLs could be added here. I can't see any use case now or in the future but I wanted to leave the option to.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm I see, but I think for now it should be written in a more idiomatic way

If more functions are added later, the loops can be written then

@hratoanina
Copy link
Contributor Author

@npwardberkeley Hi Nick, just checking up on this PR. Is there anything you need from us?

}

// Arithmetic
for _ in 0..config.num_challenges {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same with here

builder.connect(row[3], field_target);
// values
for j in 0..VALUE_LIMBS {
builder.connect(row[j + 4], targets[j]);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: 4 + j for consistency

@npwardberkeley
Copy link
Contributor

npwardberkeley commented Jun 16, 2023

Ah sorry! No it looks ready to go, except for a few really nitpicky comments I left!

@hratoanina
Copy link
Contributor Author

@npwardberkeley We realized that with the original design the recursive circuits were not generic and were depending on the public values (because of hardsetting them in get_memory_extra_looking_products_circuit). We turned them into public inputs to solve that problem. For convenience we also propagate a PublicValues struct from the root proof to the aggregation proof and the block proof, but we can do without if needed.

Note that this PR doesn't connect these newly created public inputs between proofs, since this is already what @Nashtare's PR (#989) is about.

@Nashtare Nashtare mentioned this pull request Jul 27, 2023
5 tasks
@npwardberkeley npwardberkeley merged commit 5b8740a into 0xPolygonZero:main Jul 28, 2023
2 checks passed
@Nashtare Nashtare mentioned this pull request Aug 1, 2023
@Nashtare Nashtare deleted the memory-ctl-verifier-bus branch August 10, 2023 17:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants