[Feature] Implement snark.verify opcode

[raychu86]

Motivation

This PR implements the snark.verify and snark.verify.batch opcode, which are finalize-only operations that verifies a Varuna proof. In order to support this, the array size was also increased from 512 to 2048. These features will activate at ConsenusVersion::V14.

Examples:

snark.verify r0 r1 r2 into r3

r0 is the verifying key (represented by a byte array)
r1 is the verifier inputs (represented by an array of field elements)
r2 is the proof (represented by a byte array)
r3 is the verification results (represented by a boolean)

snark.verify.batch r0 r1 r2 into r3

r0 is the array of verifying keys (represented by a 2-D byte array)
r1 is the array of verifier inputs (represented by a 3-D array of field elements)
r2 is the batch proof (represented by a byte array)
r3 is the verification results (represented by a boolean)

Additional Notes

Currently this only supports the native Varuna proofs, but the opcode can be expanded to other proof systems in the future.

The user is required to add the default public input Field::one() into the verifier inputs.

TODO

• Determine proper fee pricing
• Implement verification for batch proofs
• Determine the required array size. 2048 is likely not sufficient (For batched proofs using the same circuit, proofs are 957 bytes + 144 bytes per additional proof in the batch)
• V14 Height needs to be properly set for the networks
• Determine if the first public "one" variable needs to be manually added by the user.

Test Plan

Tests have been added to check the proofs are properly verified and/or rejected.

[vicsn]

Do you have any recommendation for how explorers should display verifying keys (in e.g. mappings) to users/developers, for them to easily be able to verify their correctness?

Similar to ProvableHQ/leo#28664 which is on the roadmap for Q1, the explorer could verify and display the leo program source code for such stored verifying keys - which I assume we'll want to make effectively immutable.

CC @miazn

[mwyatt896]

Super exciting stuff y'all!

[raychu86]

Do you have any recommendation for how explorers should display verifying keys (in e.g. mappings) to users/developers, for them to easily be able to verify their correctness?

This should be up to the developer to parse manually since these are effectively generic byte arrays. We can in theory try to parse byte arrays of size 673u32 or create a custom VK type, but I don't see it being that useful.

Similar to ProvableHQ/leo#28664 which is on the roadmap for Q1, the explorer could verify and display the leo program source code for such stored verifying keys - which I assume we'll want to make effectively immutable.

Immutability of the mapping should be up to the program developer. We also can't really verify the VK because we don't necessarily know the circuit assignment.

[d0cd]

Disregard the above approval, meant to select "Request Changes"

[vicsn]

Because we had so many issues with external struct backwards compatibility, I went through every instance of the argument in the code and found two places to extend (nothing too serious):

• let mut length = (u16::try_from(result.len()).unwrap()).to_bytes_le().unwrap();, IMO just a single u32 test case would already be sufficient in test_deeply_nested_future.
• preimage.push(Field::from_u16(argument_locator.index()));, I guess we can just use from_u32?

My gut says it's not worth the effort at this to make all of this more strongly typed and tied to each other, because we may make arbitrary changes to the VM, so we will have to continue to rely on a consistent code style + greps.

[vicsn]

Can you also merge in origin/staging?

[raychu86]

Because we had so many issues with external struct backwards compatibility, I went through every instance of the argument in the code and found two places to extend (nothing too serious):

• let mut length = (u16::try_from(result.len()).unwrap()).to_bytes_le().unwrap();, IMO just a single u32 test case would already be sufficient in test_deeply_nested_future.
• preimage.push(Field::from_u16(argument_locator.index()));, I guess we can just use from_u32?

My gut says it's not worth the effort at this to make all of this more strongly typed and tied to each other, because we may make arbitrary changes to the VM, so we will have to continue to rely on a consistent code style + greps.

Thank you for doing a pass on this front. Regarding the two findings:

1. We are now constrained by the u16 for bytes, so u16 here is correct for let mut length = (u16::try_from(result.len()).unwrap()).to_bytes_le().unwrap();, since this is for byte (de)serialization.
2. preimage.push(Field::from_u16(argument_locator.index())); isn't for Futures, rather it is used for Restrictions. "Argument" is an overloaded term here.

If you agree, I don't think these require changing.

[d0cd]

Suggested change

	// Verify the signature.
	// Verify the proof.

[d0cd]

Suggested change

	// Sanity check that there are exactly three operands.
	// Sanity check that there are exactly four operands.

[d0cd]

current_block_height is available on L79

[d0cd]

LGTM, found some minor nits.