argumentcomputer / argumentcomputer/sphinx

Some field gadget tests do not verify lookups

Open
#19 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Rust
Stars
80
Forks
8
PR merge metrics
No merged PRs in 30d

Description

Tests that only verify a single chip's trace and proof, understandably but surprisingly, do not check for the correctness of lookups, since they are only checking an individual chip's trace for correctness.

This is particularly relevant for non-native field operation tests after the addition of range checking to the non-native field gadgets. That is, all of these tests: [1](https://github.com/wormhole-foundation/wp1/blob/c74dccf6811e1a8873951a0d94727358fe148b1f/core/src/operations/field/field_den.rs#L300), [2](https://github.com/wormhole-foundation/wp1/blob/c74dccf6811e1a8873951a0d94727358fe148b1f/core/src/operations/field/field_inner_product.rs#L281), [3](https://github.com/wormhole-foundation/wp1/blob/c74dccf6811e1a8873951a0d94727358fe148b1f/core/src/operations/field/field_op.rs#L396), [4](https://github.com/wormhole-foundation/wp1/blob/c74dccf6811e1a8873951a0d94727358fe148b1f/core/src/operations/field/extensions/quadratic/sqrt.rs#L230), [5](https://github.com/wormhole-foundation/wp1/blob/c74dccf6811e1a8873951a0d94727358fe148b1f/core/src/operations/field/extensions/quadratic/mod.rs#L501)), are not actually checking that the range checks are correct and that the lookup arguments and send/receives are also correct. This is a minor issue, but can cover up existing issues if any of those gadgets are not used and tested by other existing precompiles. Right now, after merging #160, I believe only the QuadField Sqrt gadget falls under this under-tested criteria.

Any test that makes use of those operations in an actual RISC-V precompile (i.e. any of the tests under the `tests/` directory) do not have this issue, since they emulate the entire machine and check the cumulative sum of the lookup arguments. However, some of the tests in the `tests/` directory use only hard-coded test values, while the field gadget tests fill the trace with random values as well as hardcoded values, so the test coverage is not perfect.

I'm not sure of the best way to approach this: modifying those tests to make a "full" proof seems difficult since the test chips are not in the `MachineAir` enum. Adding a test-only method for checking the generated byte lookup events for correctness might be a good compromise, to ensure that at least none of the gadgets are emitting invalid byte lookups. Alternatively, proper documentation to highlight that this is the case might be enough, since the full end-to-end tests with RISC-V programs exist for all precompiles.

Contributor guide

Open the contributing guide

Research direction

Start with the field gadget tests at core/src/operations/field/field_den.rs, field_inner_product.rs, field_op.rs, field/extensions/quadratic/sqrt.rs, and field/extensions/quadratic/mod.rs. Compare them with the end-to-end tests under tests/ and inspect how lookup arguments are checked. Done means the affected gadget tests validate their generated lookups, or the limitation is documented clearly if a full-proof test is not practical.

Written by the indexing model from the issue text.

Assessment

Tech stack
rust
Domain
cryptography, testing-qa
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.