[alireza-shirzad]

Fixes #203.

Problem

Since #184, x IN (v1, .., vk) became x = v1 OR .. OR x = vk. OR stays virtual (a + b − ab), so a 4-value list is 15 terms, and Q19 ORs three branches that each hold one. Degree reduction expands the whole claim before it reduces anything: Q19's claim had 4,882 terms of degree up to 27, and 787 chunk commitments were needed to bring the degree down. That took Q19's verifier from 42 ms to 173 ms. The September proof is not a sound baseline: its IN lists were committed without any check.

Change

• Membership gadget (irs/nodes/plan/exprs/in_list/gadget.rs). A list of literal values is proved directly. The result b is committed. The data columns of x and of every value are folded with the same challenges into f and gᵢ. The gadget checks:

  • m·P(f) = 0 with P = ∏(f − gᵢ), where m is the rows in the list (b, or act − b for NOT IN);
  • P(f) + γ·(1 − (act − m)) is nonzero, so no active row outside m matches a value;
  • b is boolean, and 0 on inactive rows.

  P is built in Horner form from its public coefficients. It expands to one term per power of f (k + 1 terms for a number column), not one per subset of the list.

• InList IR node (in_list/mod.rs), which commits the result and wires the gadget.

• InListAsComparisons rule: now rewrites only lists that hold a value other than a non-null literal. ensure_supported refuses such a list if it reaches the IR.

• Shared helper: activator_expr moves from BinaryExpr to hints, shared by both nodes.

Soundness

• The fold challenges are drawn after x and b are committed. A row with x ≠ vᵢ folds to gᵢ with probability at most 1/|F| per value.
• A row with x = vᵢ always makes P = 0, so the nonzero check rejects marking it "not in the list".

Measurements (TPC-H Q19 _tt, SF 0.1, 1 thread)

	before (Nov 9)	after
verifier, total	173.4 ms	48.2 ms
verifier, crypto only	144.7 ms	26.2 ms
prover (one sample)	45.8 s	42.9 s
proof, compressed	45,573 B	39,682 B

On test data, the largest sumcheck claim goes from 4,882 terms (4,096 over the degree limit) to 836 (56 over).

Tests

• tests/in_list.rs: three new cases (an expression as input, a string NOT IN, a list matching no row), 8 cases in all. Each was checked to reach the membership gadget, and all pass with and without honest-prover.
• tests/in_list_forgery.rs: the prover commits the negated result of a string IN list and claims it. Verification rejects it. With the gadget's two membership checks removed, the same forgery verifies.
• rewritten_in_list_matches_datafusion: lists with a column value are rewritten; literal lists are kept by this rule and by the full rule set.
• tpch_q19 passes with and without honest-prover.
• The full e2e suite (cargo test --release -p tt-exec --features test-utils --no-fail-fast) has 225 passed and 1 failed. The failure is bench_like_infix_lineitem, which passes when run alone. It fails only when it shares a process with the test-data LIKE tests, because the two give l_comment different fingerprint rules; it already failed this way before this change.
• Also passing: debug cargo test --workspace --lib, just test, clippy with CI flags, and cargo fmt --check.

Open

#183: a long list still grows. It is k + 1 terms for a number column and about 2^(k+1) for a string (hash and length folded together). That is never more than the OR form it replaces. The TODO in the rule points there.

🤖 Generated with Claude Code