facebook / winterfell

A STARK prover and verifier for arbitrary computations
MIT License
758 stars 172 forks source link

Implementing Keccak256 #227

Open Bisht13 opened 8 months ago

Bisht13 commented 8 months ago

I want to implement keccak256 as I want to create a zk proof of "I know the preimage of the keccak256 hash".

I'm unable to implement bit operations. I'm converting current_state (type E: Field Element) to bytes and then doing the bit operation and then converting it back to type E (using E::from()). But this seems to break the code as the proof is not verifying. Currently, I'm trying a very small trace of length 8 with elements (2,4,6,8,10,12,14,16) and my transition constraint is (result[0] = next_state - OR(current_state, E::ONE) - E::ONE). But the proof is not verifying. Can you help me to figure out where did I go wrong? @irakliyk

image image image image image
Nashtare commented 8 months ago

Hi @Bisht13!

Your constraint evaluation is failing, because your "or" method isn't algebraic. When writing constraints, we can only represent arithmetic operations in the field we're working on. That is, only things with ADD, SUB, MUL, etc.. Here, you're going outside of the field by looking at the byte sequences, consider them as U256, and operate on those, which cannot be interpreted as valid field-only operations.

Similarly, expressions like an if/else assignment let a = if foo { bar } else { baz }; when expressed as constraints, requires your condition to be stored in a register, constrained to be boolean (i.e. 0 or 1), and then you can constrain the register for a as foo * bar + (1-foo) * baz where 1 - foo behaves as NOT foo.

Hope this helps! By the way there are various implementations of Keccak for STARKs, you may want to look at how implementors have done to get some good insights!

Bisht13 commented 8 months ago

Thanks! @Nashtare, I resolved the issue by adding an upper bound in constraints. Also, can you please provide links for the same as I was unable to find them.

Nashtare commented 8 months ago

You can look at Polygon Zero's zkEVM implementation, for an example of a Keccak STARK: https://github.com/0xPolygonZero/plonky2/blob/main/evm/src/keccak/keccak_stark.rs

Bisht13 commented 8 months ago

Is there a way I can get the verifier as a solidity file? I want to verify the proof on chain.